begin
theorem
canceled;
theorem Th2:
theorem
theorem
canceled;
theorem
canceled;
theorem Th6:
theorem
begin
:: deftheorem Def1 defines with_non_trivial_Instructions AMISTD_4:def 1 :
for N being set
for A being AMI-Struct of N holds
( A is with_non_trivial_Instructions iff not the Instructions of A is trivial );
:: deftheorem Def2 defines with_non_trivial_ObjectKinds AMISTD_4:def 2 :
for N being set
for A being non empty AMI-Struct of N holds
( A is with_non_trivial_ObjectKinds iff for o being Object of A holds not ObjectKind o is trivial );
:: deftheorem Def3 defines Output AMISTD_4:def 3 :
for N being with_non-empty_elements set
for A being non empty stored-program AMI-Struct of N
for I being Instruction of A
for b4 being Subset of A holds
( b4 = Output I iff for o being Object of A holds
( o in b4 iff ex s being State of A st s . o <> (Exec (I,s)) . o ) );
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 AMISTD_4:def 4 :
for N being non empty with_non-empty_elements set
for A being non empty stored-program IC-Ins-separated definite AMI-Struct of N
for I being Instruction of A
for b4 being Subset of A holds
( b4 = Out_\_Inp I iff for o being Object of A holds
( o in b4 iff for s being State of A
for a being Element of ObjectKind o holds Exec (I,s) = Exec (I,(s +* (o,a))) ) );
:: deftheorem Def5 defines Out_U_Inp AMISTD_4:def 5 :
for N being non empty with_non-empty_elements set
for A being non empty stored-program IC-Ins-separated definite AMI-Struct of N
for I being Instruction of A
for b4 being Subset of A holds
( b4 = Out_U_Inp I iff for o being Object of A holds
( o in b4 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) ) );
:: deftheorem defines Input AMISTD_4:def 6 :
for N being non empty with_non-empty_elements set
for A being non empty stored-program IC-Ins-separated definite AMI-Struct of N
for I being Instruction of A holds Input I = (Out_U_Inp I) \ (Out_\_Inp I);
theorem
canceled;
theorem
canceled;
theorem Th10:
theorem Th11:
theorem
canceled;
theorem
theorem
theorem Th15:
theorem
theorem
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
theorem
canceled;
theorem
theorem
theorem
theorem Th26:
theorem
theorem