scheme
    AUTO_ABSTRACT =
class
    type
        Owner = Nat,
        Auto = Nat,
        TrustedMan = Nat,
	AutoMap = Auto -m-> Owner,
	AutoMap2 = Auto -m-> TrustedMan-set,
        AutoInfo = AutoMap >< AutoMap2
/*---------------------------------------------------------------------------------*/
    value
        Empty: AutoInfo,
        AddAuto: AutoInfo >< Owner >< Auto -~-> AutoInfo,
        DropAuto: AutoInfo >< Auto -~-> AutoInfo,
	SellAuto: AutoInfo >< Owner >< Auto -~-> AutoInfo,
        AddTrustedMan: AutoInfo >< Auto >< TrustedMan -~-> AutoInfo,
        DropTrustedMan: AutoInfo >< Auto >< TrustedMan -~-> AutoInfo,
        GetOwner: AutoInfo >< Auto -~-> Owner,
        GetAutos: AutoInfo >< Owner -> Auto-set,
        GetTrustedMen: AutoInfo >< Auto -~-> TrustedMan-set,
        ShowAutos: AutoInfo -> Auto-set

    axiom
        /*AddAuto*/
	all o: Owner, a: Auto 
		:- AddAuto(Empty, o, a) is ([a +> o], [a +> {}]),
	all ai: AutoInfo, o1, o2: Owner, a1, a2: Auto
		:- AddAuto(AddAuto(ai, o1, a1), o2, a2) is AddAuto(AddAuto(ai, o2, a2), o1, a1),
	all ai: AutoInfo, o: Owner, a: Auto
		:- DropAuto(AddAuto(ai, o, a), a) is ai,

	/*DropAuto*/
	all ai: AutoInfo, a1, a2: Auto
		:- DropAuto(DropAuto(ai, a1), a2) is DropAuto(DropAuto(ai, a2), a1),

	/*SellAuto*/
	all ai: AutoInfo, o1, o2: Owner, a: Auto
		:- SellAuto(SellAuto(ai, o1, a), o2, a) is SellAuto(ai, o2, a),
	all ai: AutoInfo, o1, o2: Owner, a: Auto
		:- SellAuto(AddAuto(ai, o1, a), o2, a) is AddAuto(ai, o2, a),
	all ai: AutoInfo, o: Owner, a: Auto
		:- DropAuto(SellAuto(ai, o, a), a) is DropAuto(ai, a),

	/*AddTrustedMan*/
	all o: Owner, a: Auto, t: TrustedMan 
		:- AddTrustedMan(AddAuto(Empty, o, a), a, t) is ([a +> o], [a +> {t}]),
	all ai: AutoInfo, t1, t2: TrustedMan, a: Auto
		:- AddTrustedMan(AddTrustedMan(ai, a, t1), a, t2) is AddTrustedMan(AddTrustedMan(ai, a, t2), a, t1),
	all ai: AutoInfo, o: Owner, a: Auto, t: TrustedMan
		:- DropAuto(AddTrustedMan(AddAuto(ai, o, a), a, t), a) is ai,
	all ai: AutoInfo, o: Owner, a: Auto, t: TrustedMan
		:- SellAuto(AddTrustedMan(ai, a, t), o ,a) is SellAuto(ai, o, a),

	/*DropTrustedMan*/
	all ai: AutoInfo, a: Auto, t: TrustedMan
		:- DropTrustedMan(AddTrustedMan(ai, a, t), a, t) is ai,

	/*GetOwner*/
	all ai: AutoInfo, o: Owner, a: Auto
		:- GetOwner(AddAuto(ai, o, a), a) is o,
	all ai: AutoInfo, o: Owner, a: Auto
		:- GetOwner(SellAuto(ai, o, a), a) is o,

	/*GetAutos*/
	all o: Owner, a: Auto
		:- GetAutos(AddAuto(Empty, o, a), o) is {a},
	all ai: AutoInfo, o: Owner, a: Auto
		:- GetAutos(SellAuto(ai, o, a), o) is GetAutos(ai, o) union {a},

	/*GetTrustedMen*/
	all ai: AutoInfo, o: Owner, a: Auto
		:- GetTrustedMen(AddAuto(ai, o, a), a) is {},
	all ai: AutoInfo, o: Owner, a: Auto
		:- GetTrustedMen(SellAuto(ai, o, a), a) is {},
	all ai: AutoInfo, a: Auto, t: TrustedMan
		:- GetTrustedMen(AddTrustedMan(ai, a, t), a) is GetTrustedMen(ai, a) union {t},
	all ai: AutoInfo, a: Auto, t: TrustedMan
		:- GetTrustedMen(DropTrustedMan(ai, a, t), a) is (GetTrustedMen(ai, a) \ {t}),
	
	/*ShowAutos*/
	all o: Owner, a: Auto
		:- ShowAutos(AddAuto(Empty, o, a)) is {a},
	all ai: AutoInfo, o: Owner, a: Auto
		:- ShowAutos(SellAuto(ai, o, a)) is ShowAutos(ai),
	all ai: AutoInfo, o: Owner, a: Auto
		:- ShowAutos(DropAuto(ai, a)) is ShowAutos(ai) \ {a},
	all ai: AutoInfo, o: Owner, a: Auto
		:- ShowAutos(AddAuto(ai, o, a)) is ShowAutos(ai) union {a}
end