begin
theorem
canceled;
theorem Th2:
theorem
theorem
theorem
canceled;
theorem Th6:
theorem
theorem
begin
:: deftheorem Def1 defines with_non_trivial_Instructions AMI_7:def 1 :
:: deftheorem Def2 defines with_non_trivial_ObjectKinds AMI_7:def 2 :
:: deftheorem Def3 defines Output AMI_7:def 3 :
definition
let N be non
empty with_non-empty_elements set ;
let A be non
empty stored-program IC-Ins-separated definite AMI-Struct of
N;
let I be
Instruction of
A;
func Out_\_Inp I -> Subset of
A means :
Def4:
for
o being
Object of
A holds
(
o in it iff for
s being
State of
A for
a being
Element of
ObjectKind o holds
Exec I,
s = Exec I,
(s +* o,a) );
existence
ex b1 being Subset of A st
for o being Object of A holds
( o in b1 iff for s being State of A
for a being Element of ObjectKind o holds Exec I,s = Exec I,(s +* o,a) )
uniqueness
for b1, b2 being Subset of A st ( for o being Object of A holds
( o in b1 iff for s being State of A
for a being Element of ObjectKind o holds Exec I,s = Exec I,(s +* o,a) ) ) & ( for o being Object of A holds
( o in b2 iff for s being State of A
for a being Element of ObjectKind o holds Exec I,s = Exec I,(s +* o,a) ) ) holds
b1 = b2
func Out_U_Inp I -> Subset of
A means :
Def5:
for
o being
Object of
A holds
(
o in it iff ex
s being
State of
A ex
a being
Element of
ObjectKind o st
Exec I,
(s +* o,a) <> (Exec I,s) +* o,
a );
existence
ex b1 being Subset of A st
for o being Object of A holds
( o in b1 iff ex s being State of A ex a being Element of ObjectKind o st Exec I,(s +* o,a) <> (Exec I,s) +* o,a )
uniqueness
for b1, b2 being Subset of A st ( for o being Object of A holds
( o in b1 iff ex s being State of A ex a being Element of ObjectKind o st Exec I,(s +* o,a) <> (Exec I,s) +* o,a ) ) & ( for o being Object of A holds
( o in b2 iff ex s being State of A ex a being Element of ObjectKind o st Exec I,(s +* o,a) <> (Exec I,s) +* o,a ) ) holds
b1 = b2
end;
:: deftheorem Def4 defines Out_\_Inp AMI_7:def 4 :
:: deftheorem Def5 defines Out_U_Inp AMI_7:def 5 :
:: deftheorem defines Input AMI_7:def 6 :
theorem
canceled;
theorem Th10:
theorem Th11:
theorem
canceled;
theorem
theorem
theorem Th15:
theorem
theorem
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
theorem
theorem
theorem
theorem
theorem Th26:
theorem
theorem
theorem