:: AMISTD_4 semantic presentation begin definition let N be with_zero set ; let A be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; let s be State of A; let o be Object of A; let a be Element of Values o; :: original: +* redefine funcs +* (o,a) -> State of A; coherence s +* (o,a) is State of A proof dom s = the carrier of A by PARTFUN1:def_2; then s +* (o,a) = s +* (o .--> a) by FUNCT_7:def_3; hence s +* (o,a) is State of A ; ::_thesis: verum end; end; theorem Th1: :: AMISTD_4:1 for N being with_zero set for A being non empty with_non-empty_values IC-Ins-separated standard AMI-Struct over N for I being Instruction of A for s being State of A for o being Object of A for w being Element of Values o st I is sequential & o <> IC holds IC (Exec (I,s)) = IC (Exec (I,(s +* (o,w)))) proof let N be with_zero set ; ::_thesis: for A being non empty with_non-empty_values IC-Ins-separated standard AMI-Struct over N for I being Instruction of A for s being State of A for o being Object of A for w being Element of Values o st I is sequential & o <> IC holds IC (Exec (I,s)) = IC (Exec (I,(s +* (o,w)))) let A be non empty with_non-empty_values IC-Ins-separated standard AMI-Struct over N; ::_thesis: for I being Instruction of A for s being State of A for o being Object of A for w being Element of Values o st I is sequential & o <> IC holds IC (Exec (I,s)) = IC (Exec (I,(s +* (o,w)))) let I be Instruction of A; ::_thesis: for s being State of A for o being Object of A for w being Element of Values o st I is sequential & o <> IC holds IC (Exec (I,s)) = IC (Exec (I,(s +* (o,w)))) let s be State of A; ::_thesis: for o being Object of A for w being Element of Values o st I is sequential & o <> IC holds IC (Exec (I,s)) = IC (Exec (I,(s +* (o,w)))) let o be Object of A; ::_thesis: for w being Element of Values o st I is sequential & o <> IC holds IC (Exec (I,s)) = IC (Exec (I,(s +* (o,w)))) let w be Element of Values o; ::_thesis: ( I is sequential & o <> IC implies IC (Exec (I,s)) = IC (Exec (I,(s +* (o,w)))) ) assume that A1: for s being State of A holds (Exec (I,s)) . (IC ) = succ (IC s) and A2: o <> IC ; :: according to AMISTD_1:def_8 ::_thesis: IC (Exec (I,s)) = IC (Exec (I,(s +* (o,w)))) thus IC (Exec (I,s)) = succ (IC s) by A1 .= succ (IC (s +* (o,w))) by A2, FUNCT_7:32 .= IC (Exec (I,(s +* (o,w)))) by A1 ; ::_thesis: verum end; theorem :: AMISTD_4:2 for N being with_zero set for A being non empty with_non-empty_values IC-Ins-separated standard AMI-Struct over N for I being Instruction of A for s being State of A for o being Object of A for w being Element of Values o st I is sequential & o <> IC holds IC (Exec (I,(s +* (o,w)))) = IC ((Exec (I,s)) +* (o,w)) proof let N be with_zero set ; ::_thesis: for A being non empty with_non-empty_values IC-Ins-separated standard AMI-Struct over N for I being Instruction of A for s being State of A for o being Object of A for w being Element of Values o st I is sequential & o <> IC holds IC (Exec (I,(s +* (o,w)))) = IC ((Exec (I,s)) +* (o,w)) let A be non empty with_non-empty_values IC-Ins-separated standard AMI-Struct over N; ::_thesis: for I being Instruction of A for s being State of A for o being Object of A for w being Element of Values o st I is sequential & o <> IC holds IC (Exec (I,(s +* (o,w)))) = IC ((Exec (I,s)) +* (o,w)) let I be Instruction of A; ::_thesis: for s being State of A for o being Object of A for w being Element of Values o st I is sequential & o <> IC holds IC (Exec (I,(s +* (o,w)))) = IC ((Exec (I,s)) +* (o,w)) let s be State of A; ::_thesis: for o being Object of A for w being Element of Values o st I is sequential & o <> IC holds IC (Exec (I,(s +* (o,w)))) = IC ((Exec (I,s)) +* (o,w)) let o be Object of A; ::_thesis: for w being Element of Values o st I is sequential & o <> IC holds IC (Exec (I,(s +* (o,w)))) = IC ((Exec (I,s)) +* (o,w)) let w be Element of Values o; ::_thesis: ( I is sequential & o <> IC implies IC (Exec (I,(s +* (o,w)))) = IC ((Exec (I,s)) +* (o,w)) ) assume that A1: I is sequential and A2: o <> IC ; ::_thesis: IC (Exec (I,(s +* (o,w)))) = IC ((Exec (I,s)) +* (o,w)) thus IC (Exec (I,(s +* (o,w)))) = IC (Exec (I,s)) by A1, A2, Th1 .= IC ((Exec (I,s)) +* (o,w)) by A2, FUNCT_7:32 ; ::_thesis: verum end; begin definition let A be COM-Struct ; attrA is with_non_trivial_Instructions means :Def1: :: AMISTD_4:def 1 not the InstructionsF of A is trivial ; end; :: deftheorem Def1 defines with_non_trivial_Instructions AMISTD_4:def_1_:_ for A being COM-Struct holds ( A is with_non_trivial_Instructions iff not the InstructionsF of A is trivial ); definition let N be with_zero set ; let A be non empty with_non-empty_values AMI-Struct over N; attrA is with_non_trivial_ObjectKinds means :Def2: :: AMISTD_4:def 2 for o being Object of A holds not Values o is trivial ; end; :: deftheorem Def2 defines with_non_trivial_ObjectKinds AMISTD_4:def_2_:_ for N being with_zero set for A being non empty with_non-empty_values AMI-Struct over N holds ( A is with_non_trivial_ObjectKinds iff for o being Object of A holds not Values o is trivial ); registration let N be with_zero set ; cluster STC N -> with_non_trivial_ObjectKinds ; coherence STC N is with_non_trivial_ObjectKinds proof let o be Object of (STC N); :: according to AMISTD_4:def_2 ::_thesis: not Values o is trivial A1: the carrier of (STC N) = {0} by AMISTD_1:def_7; A2: the Object-Kind of (STC N) = 0 .--> 0 by AMISTD_1:def_7; percases o in {0} by A1; supposeA3: o in {0} ; ::_thesis: not Values o is trivial A4: the ValuesF of (STC N) = N --> NAT by AMISTD_1:def_7; 0 in N by MEASURE6:def_2; then the_Values_of (STC N) = 0 .--> NAT by A2, A4, FUNCOP_1:89; then Values o = (0 .--> NAT) . o .= NAT by A3, FUNCOP_1:7 ; hence not Values o is trivial ; ::_thesis: verum end; end; end; end; registration let N be with_zero set ; cluster non empty with_non-empty_values IC-Ins-separated halting with_explicit_jumps IC-relocable standard with_non_trivial_Instructions with_non_trivial_ObjectKinds for AMI-Struct over N; existence ex b1 being non empty with_non-empty_values IC-Ins-separated halting standard AMI-Struct over N st ( b1 is with_explicit_jumps & b1 is IC-relocable & b1 is with_non_trivial_ObjectKinds & b1 is with_non_trivial_Instructions ) proof take STC N ; ::_thesis: ( STC N is with_explicit_jumps & STC N is IC-relocable & STC N is with_non_trivial_ObjectKinds & STC N is with_non_trivial_Instructions ) A1: ( [1,0,0] in {[1,0,0],[0,0,0]} & [0,0,0] in {[1,0,0],[0,0,0]} ) by TARSKI:def_2; ( the InstructionsF of (STC N) = {[0,0,0],[1,0,0]} & [1,0,0] <> [0,0,0] ) by AMISTD_1:def_7, XTUPLE_0:3; then not the InstructionsF of (STC N) is trivial by A1, ZFMISC_1:def_10; hence ( STC N is with_explicit_jumps & STC N is IC-relocable & STC N is with_non_trivial_ObjectKinds & STC N is with_non_trivial_Instructions ) by Def1; ::_thesis: verum end; end; registration let N be with_zero set ; cluster STC N -> with_non_trivial_Instructions ; coherence STC N is with_non_trivial_Instructions proof A1: [0,0,0] <> [1,0,0] by XTUPLE_0:3; the InstructionsF of (STC N) = {[0,0,0],[1,0,0]} by AMISTD_1:def_7; then ( [0,0,0] in the InstructionsF of (STC N) & [1,0,0] in the InstructionsF of (STC N) ) by TARSKI:def_2; hence not the InstructionsF of (STC N) is trivial by A1, ZFMISC_1:def_10; :: according to AMISTD_4:def_1 ::_thesis: verum end; end; registration let N be with_zero set ; cluster non empty with_non-empty_values IC-Ins-separated with_non_trivial_Instructions with_non_trivial_ObjectKinds for AMI-Struct over N; existence ex b1 being non empty with_non-empty_values AMI-Struct over N st ( b1 is with_non_trivial_ObjectKinds & b1 is with_non_trivial_Instructions & b1 is IC-Ins-separated ) proof take STC N ; ::_thesis: ( STC N is with_non_trivial_ObjectKinds & STC N is with_non_trivial_Instructions & STC N is IC-Ins-separated ) thus ( STC N is with_non_trivial_ObjectKinds & STC N is with_non_trivial_Instructions & STC N is IC-Ins-separated ) ; ::_thesis: verum end; end; registration let N be with_zero set ; let A be non empty with_non-empty_values with_non_trivial_ObjectKinds AMI-Struct over N; let o be Object of A; cluster Values o -> non trivial ; coherence not Values o is trivial by Def2; end; registration let N be with_zero set ; let A be with_non-empty_values with_non_trivial_Instructions AMI-Struct over N; cluster the InstructionsF of A -> non trivial ; coherence not the InstructionsF of A is trivial by Def1; end; registration let N be with_zero set ; let A be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; cluster Values (IC ) -> non trivial ; coherence not Values (IC ) is trivial by MEMSTR_0:def_6; end; definition let N be with_zero set ; let A be non empty with_non-empty_values AMI-Struct over N; let I be Instruction of A; func Output I -> Subset of A means :Def3: :: AMISTD_4:def 3 for o being Object of A holds ( o in it iff ex s being State of A st s . o <> (Exec (I,s)) . o ); 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 st s . o <> (Exec (I,s)) . o ) proof defpred S1[ set ] means ex s being State of A st s . \$1 <> (Exec (I,s)) . \$1; consider X being Subset of A such that A1: for x being set holds ( x in X iff ( x in the carrier of A & S1[x] ) ) from SUBSET_1:sch_1(); take X ; ::_thesis: for o being Object of A holds ( o in X iff ex s being State of A st s . o <> (Exec (I,s)) . o ) thus for o being Object of A holds ( o in X iff ex s being State of A st s . o <> (Exec (I,s)) . o ) by A1; ::_thesis: verum end; 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 st s . o <> (Exec (I,s)) . o ) ) & ( for o being Object of A holds ( o in b2 iff ex s being State of A st s . o <> (Exec (I,s)) . o ) ) holds b1 = b2 proof defpred S1[ set ] means ex s being State of A st s . \$1 <> (Exec (I,s)) . \$1; let a, b be Subset of A; ::_thesis: ( ( for o being Object of A holds ( o in a iff ex s being State of A st s . o <> (Exec (I,s)) . o ) ) & ( for o being Object of A holds ( o in b iff ex s being State of A st s . o <> (Exec (I,s)) . o ) ) implies a = b ) assume that A2: for o being Object of A holds ( o in a iff S1[o] ) and A3: for o being Object of A holds ( o in b iff S1[o] ) ; ::_thesis: a = b thus a = b from SUBSET_1:sch_2(A2, A3); ::_thesis: verum end; end; :: deftheorem Def3 defines Output AMISTD_4:def_3_:_ for N being with_zero set for A being non empty with_non-empty_values AMI-Struct over 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 with_zero set ; let A be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; let I be Instruction of A; func Out_\_Inp I -> Subset of A means :Def4: :: AMISTD_4:def 4 for o being Object of A holds ( o in it iff for s being State of A for a being Element of Values 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 Values o holds Exec (I,s) = Exec (I,(s +* (o,a))) ) proof defpred S1[ set ] means ex l being Object of A st ( l = \$1 & ( for s being State of A for a being Element of Values l holds Exec (I,s) = Exec (I,(s +* (l,a))) ) ); consider X being Subset of A such that A1: for x being set holds ( x in X iff ( x in the carrier of A & S1[x] ) ) from SUBSET_1:sch_1(); take X ; ::_thesis: for o being Object of A holds ( o in X iff for s being State of A for a being Element of Values o holds Exec (I,s) = Exec (I,(s +* (o,a))) ) let l be Object of A; ::_thesis: ( l in X iff for s being State of A for a being Element of Values l holds Exec (I,s) = Exec (I,(s +* (l,a))) ) hereby ::_thesis: ( ( for s being State of A for a being Element of Values l holds Exec (I,s) = Exec (I,(s +* (l,a))) ) implies l in X ) assume l in X ; ::_thesis: for s being State of A for a being Element of Values l holds Exec (I,s) = Exec (I,(s +* (l,a))) then S1[l] by A1; hence for s being State of A for a being Element of Values l holds Exec (I,s) = Exec (I,(s +* (l,a))) ; ::_thesis: verum end; thus ( ( for s being State of A for a being Element of Values l holds Exec (I,s) = Exec (I,(s +* (l,a))) ) implies l in X ) by A1; ::_thesis: verum end; 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 Values 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 Values o holds Exec (I,s) = Exec (I,(s +* (o,a))) ) ) holds b1 = b2 proof defpred S1[ Object of A] means for s being State of A for a being Element of Values \$1 holds Exec (I,s) = Exec (I,(s +* (\$1,a))); let a, b be Subset of A; ::_thesis: ( ( for o being Object of A holds ( o in a iff for s being State of A for a being Element of Values o holds Exec (I,s) = Exec (I,(s +* (o,a))) ) ) & ( for o being Object of A holds ( o in b iff for s being State of A for a being Element of Values o holds Exec (I,s) = Exec (I,(s +* (o,a))) ) ) implies a = b ) assume that A2: for o being Object of A holds ( o in a iff S1[o] ) and A3: for o being Object of A holds ( o in b iff S1[o] ) ; ::_thesis: a = b thus a = b from SUBSET_1:sch_2(A2, A3); ::_thesis: verum end; func Out_U_Inp I -> Subset of A means :Def5: :: AMISTD_4:def 5 for o being Object of A holds ( o in it iff ex s being State of A ex a being Element of Values 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 Values o st Exec (I,(s +* (o,a))) <> (Exec (I,s)) +* (o,a) ) proof defpred S1[ set ] means ex l being Object of A st ( l = \$1 & ex s being State of A ex a being Element of Values l st Exec (I,(s +* (l,a))) <> (Exec (I,s)) +* (l,a) ); consider X being Subset of A such that A4: for x being set holds ( x in X iff ( x in the carrier of A & S1[x] ) ) from SUBSET_1:sch_1(); take X ; ::_thesis: for o being Object of A holds ( o in X iff ex s being State of A ex a being Element of Values o st Exec (I,(s +* (o,a))) <> (Exec (I,s)) +* (o,a) ) let l be Object of A; ::_thesis: ( l in X iff ex s being State of A ex a being Element of Values l st Exec (I,(s +* (l,a))) <> (Exec (I,s)) +* (l,a) ) hereby ::_thesis: ( ex s being State of A ex a being Element of Values l st Exec (I,(s +* (l,a))) <> (Exec (I,s)) +* (l,a) implies l in X ) assume l in X ; ::_thesis: ex s being State of A ex a being Element of Values l st Exec (I,(s +* (l,a))) <> (Exec (I,s)) +* (l,a) then S1[l] by A4; hence ex s being State of A ex a being Element of Values l st Exec (I,(s +* (l,a))) <> (Exec (I,s)) +* (l,a) ; ::_thesis: verum end; thus ( ex s being State of A ex a being Element of Values l st Exec (I,(s +* (l,a))) <> (Exec (I,s)) +* (l,a) implies l in X ) by A4; ::_thesis: verum end; 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 Values 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 Values o st Exec (I,(s +* (o,a))) <> (Exec (I,s)) +* (o,a) ) ) holds b1 = b2 proof defpred S1[ Object of A] means ex s being State of A ex a being Element of Values \$1 st Exec (I,(s +* (\$1,a))) <> (Exec (I,s)) +* (\$1,a); let a, b be Subset of A; ::_thesis: ( ( for o being Object of A holds ( o in a iff ex s being State of A ex a being Element of Values o st Exec (I,(s +* (o,a))) <> (Exec (I,s)) +* (o,a) ) ) & ( for o being Object of A holds ( o in b iff ex s being State of A ex a being Element of Values o st Exec (I,(s +* (o,a))) <> (Exec (I,s)) +* (o,a) ) ) implies a = b ) assume that A5: for o being Object of A holds ( o in a iff S1[o] ) and A6: for o being Object of A holds ( o in b iff S1[o] ) ; ::_thesis: a = b thus a = b from SUBSET_1:sch_2(A5, A6); ::_thesis: verum end; end; :: deftheorem Def4 defines Out_\_Inp AMISTD_4:def_4_:_ for N being with_zero set for A being non empty with_non-empty_values IC-Ins-separated AMI-Struct over 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 Values o holds Exec (I,s) = Exec (I,(s +* (o,a))) ) ); :: deftheorem Def5 defines Out_U_Inp AMISTD_4:def_5_:_ for N being with_zero set for A being non empty with_non-empty_values IC-Ins-separated AMI-Struct over 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 Values o st Exec (I,(s +* (o,a))) <> (Exec (I,s)) +* (o,a) ) ); definition let N be with_zero set ; let A be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; let I be Instruction of A; func Input I -> Subset of A equals :: AMISTD_4:def 6 (Out_U_Inp I) \ (Out_\_Inp I); coherence (Out_U_Inp I) \ (Out_\_Inp I) is Subset of A ; end; :: deftheorem defines Input AMISTD_4:def_6_:_ for N being with_zero set for A being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N for I being Instruction of A holds Input I = (Out_U_Inp I) \ (Out_\_Inp I); theorem Th3: :: AMISTD_4:3 for N being with_zero set for A being non empty with_non-empty_values IC-Ins-separated with_non_trivial_ObjectKinds AMI-Struct over N for I being Instruction of A holds Out_\_Inp I c= Output I proof let N be with_zero set ; ::_thesis: for A being non empty with_non-empty_values IC-Ins-separated with_non_trivial_ObjectKinds AMI-Struct over N for I being Instruction of A holds Out_\_Inp I c= Output I let A be non empty with_non-empty_values IC-Ins-separated with_non_trivial_ObjectKinds AMI-Struct over N; ::_thesis: for I being Instruction of A holds Out_\_Inp I c= Output I let I be Instruction of A; ::_thesis: Out_\_Inp I c= Output I for o being Object of A st o in Out_\_Inp I holds o in Output I proof let o be Object of A; ::_thesis: ( o in Out_\_Inp I implies o in Output I ) set s = the State of A; set a = the Element of Values o; consider w being set such that A1: w in Values o and A2: w <> the Element of Values o by SUBSET_1:48; reconsider w = w as Element of Values o by A1; set t = the State of A +* (o,w); A3: dom ( the State of A +* (o,w)) = the carrier of A by PARTFUN1:def_2; A4: dom the State of A = the carrier of A by PARTFUN1:def_2; assume A5: ( o in Out_\_Inp I & not o in Output I ) ; ::_thesis: contradiction then A6: (Exec (I,(( the State of A +* (o,w)) +* (o, the Element of Values o)))) . o = (( the State of A +* (o,w)) +* (o, the Element of Values o)) . o by Def3 .= the Element of Values o by A3, FUNCT_7:31 ; (Exec (I,( the State of A +* (o,w)))) . o = ( the State of A +* (o,w)) . o by A5, Def3 .= w by A4, FUNCT_7:31 ; hence contradiction by A5, A2, A6, Def4; ::_thesis: verum end; hence Out_\_Inp I c= Output I by SUBSET_1:2; ::_thesis: verum end; theorem Th4: :: AMISTD_4:4 for N being with_zero set for A being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N for I being Instruction of A holds Output I c= Out_U_Inp I proof let N be with_zero set ; ::_thesis: for A being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N for I being Instruction of A holds Output I c= Out_U_Inp I let A be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; ::_thesis: for I being Instruction of A holds Output I c= Out_U_Inp I let I be Instruction of A; ::_thesis: Output I c= Out_U_Inp I for o being Object of A st o in Output I holds o in Out_U_Inp I proof let o be Object of A; ::_thesis: ( o in Output I implies o in Out_U_Inp I ) assume A1: ( o in Output I & not o in Out_U_Inp I ) ; ::_thesis: contradiction for s being State of A holds s . o = (Exec (I,s)) . o proof let s be State of A; ::_thesis: s . o = (Exec (I,s)) . o reconsider so = s . o as Element of Values o by MEMSTR_0:77; A2: Exec (I,(s +* (o,so))) = (Exec (I,s)) +* (o,so) by A1, Def5; dom (Exec (I,s)) = the carrier of A by PARTFUN1:def_2; hence s . o = ((Exec (I,s)) +* (o,so)) . o by FUNCT_7:31 .= (Exec (I,s)) . o by A2, FUNCT_7:35 ; ::_thesis: verum end; hence contradiction by A1, Def3; ::_thesis: verum end; hence Output I c= Out_U_Inp I by SUBSET_1:2; ::_thesis: verum end; theorem :: AMISTD_4:5 for N being with_zero set for A being non empty with_non-empty_values IC-Ins-separated with_non_trivial_ObjectKinds AMI-Struct over N for I being Instruction of A holds Out_\_Inp I = (Output I) \ (Input I) proof let N be with_zero set ; ::_thesis: for A being non empty with_non-empty_values IC-Ins-separated with_non_trivial_ObjectKinds AMI-Struct over N for I being Instruction of A holds Out_\_Inp I = (Output I) \ (Input I) let A be non empty with_non-empty_values IC-Ins-separated with_non_trivial_ObjectKinds AMI-Struct over N; ::_thesis: for I being Instruction of A holds Out_\_Inp I = (Output I) \ (Input I) let I be Instruction of A; ::_thesis: Out_\_Inp I = (Output I) \ (Input I) for o being Object of A holds ( o in Out_\_Inp I iff o in (Output I) \ (Input I) ) proof let o be Object of A; ::_thesis: ( o in Out_\_Inp I iff o in (Output I) \ (Input I) ) hereby ::_thesis: ( o in (Output I) \ (Input I) implies o in Out_\_Inp I ) A1: Out_\_Inp I c= Output I by Th3; assume A2: o in Out_\_Inp I ; ::_thesis: o in (Output I) \ (Input I) Out_\_Inp I misses Input I by XBOOLE_1:85; then not o in Input I by A2, XBOOLE_0:3; hence o in (Output I) \ (Input I) by A2, A1, XBOOLE_0:def_5; ::_thesis: verum end; assume A3: o in (Output I) \ (Input I) ; ::_thesis: o in Out_\_Inp I then A4: not o in Input I by XBOOLE_0:def_5; percases ( not o in Out_U_Inp I or o in Out_\_Inp I ) by A4, XBOOLE_0:def_5; supposeA5: not o in Out_U_Inp I ; ::_thesis: o in Out_\_Inp I Output I c= Out_U_Inp I by Th4; then not o in Output I by A5; hence o in Out_\_Inp I by A3, XBOOLE_0:def_5; ::_thesis: verum end; suppose o in Out_\_Inp I ; ::_thesis: o in Out_\_Inp I hence o in Out_\_Inp I ; ::_thesis: verum end; end; end; hence Out_\_Inp I = (Output I) \ (Input I) by SUBSET_1:3; ::_thesis: verum end; theorem :: AMISTD_4:6 for N being with_zero set for A being non empty with_non-empty_values IC-Ins-separated with_non_trivial_ObjectKinds AMI-Struct over N for I being Instruction of A holds Out_U_Inp I = (Output I) \/ (Input I) proof let N be with_zero set ; ::_thesis: for A being non empty with_non-empty_values IC-Ins-separated with_non_trivial_ObjectKinds AMI-Struct over N for I being Instruction of A holds Out_U_Inp I = (Output I) \/ (Input I) let A be non empty with_non-empty_values IC-Ins-separated with_non_trivial_ObjectKinds AMI-Struct over N; ::_thesis: for I being Instruction of A holds Out_U_Inp I = (Output I) \/ (Input I) let I be Instruction of A; ::_thesis: Out_U_Inp I = (Output I) \/ (Input I) for o being Object of A st o in Out_U_Inp I holds o in (Output I) \/ (Input I) proof let o be Object of A; ::_thesis: ( o in Out_U_Inp I implies o in (Output I) \/ (Input I) ) assume A1: o in Out_U_Inp I ; ::_thesis: o in (Output I) \/ (Input I) ( o in Input I or o in Output I ) proof assume A2: not o in Input I ; ::_thesis: o in Output I percases ( not o in Out_U_Inp I or o in Out_\_Inp I ) by A2, XBOOLE_0:def_5; suppose not o in Out_U_Inp I ; ::_thesis: o in Output I hence o in Output I by A1; ::_thesis: verum end; supposeA3: o in Out_\_Inp I ; ::_thesis: o in Output I Out_\_Inp I c= Output I by Th3; hence o in Output I by A3; ::_thesis: verum end; end; end; hence o in (Output I) \/ (Input I) by XBOOLE_0:def_3; ::_thesis: verum end; hence Out_U_Inp I c= (Output I) \/ (Input I) by SUBSET_1:2; :: according to XBOOLE_0:def_10 ::_thesis: (Output I) \/ (Input I) c= Out_U_Inp I ( Output I c= Out_U_Inp I & Input I c= Out_U_Inp I ) by Th4, XBOOLE_1:36; hence (Output I) \/ (Input I) c= Out_U_Inp I by XBOOLE_1:8; ::_thesis: verum end; theorem Th7: :: AMISTD_4:7 for N being with_zero set for A being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N for I being Instruction of A for o being Object of A st Values o is trivial holds not o in Out_U_Inp I proof let N be with_zero set ; ::_thesis: for A being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N for I being Instruction of A for o being Object of A st Values o is trivial holds not o in Out_U_Inp I let A be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; ::_thesis: for I being Instruction of A for o being Object of A st Values o is trivial holds not o in Out_U_Inp I let I be Instruction of A; ::_thesis: for o being Object of A st Values o is trivial holds not o in Out_U_Inp I let o be Object of A; ::_thesis: ( Values o is trivial implies not o in Out_U_Inp I ) assume A1: Values o is trivial ; ::_thesis: not o in Out_U_Inp I assume o in Out_U_Inp I ; ::_thesis: contradiction then consider s being State of A, a being Element of Values o such that A2: Exec (I,(s +* (o,a))) <> (Exec (I,s)) +* (o,a) by Def5; s . o is Element of Values o by MEMSTR_0:77; then s . o = a by A1, ZFMISC_1:def_10; then A3: Exec (I,(s +* (o,a))) = Exec (I,s) by FUNCT_7:35; A4: dom (Exec (I,s)) = the carrier of A by PARTFUN1:def_2; A5: for x being set st x in the carrier of A holds ((Exec (I,s)) +* (o,a)) . x = (Exec (I,s)) . x proof let x be set ; ::_thesis: ( x in the carrier of A implies ((Exec (I,s)) +* (o,a)) . x = (Exec (I,s)) . x ) assume x in the carrier of A ; ::_thesis: ((Exec (I,s)) +* (o,a)) . x = (Exec (I,s)) . x percases ( x = o or x <> o ) ; supposeA6: x = o ; ::_thesis: ((Exec (I,s)) +* (o,a)) . x = (Exec (I,s)) . x A7: (Exec (I,s)) . o is Element of Values o by MEMSTR_0:77; thus ((Exec (I,s)) +* (o,a)) . x = a by A4, A6, FUNCT_7:31 .= (Exec (I,s)) . x by A1, A6, A7, ZFMISC_1:def_10 ; ::_thesis: verum end; suppose x <> o ; ::_thesis: ((Exec (I,s)) +* (o,a)) . x = (Exec (I,s)) . x hence ((Exec (I,s)) +* (o,a)) . x = (Exec (I,s)) . x by FUNCT_7:32; ::_thesis: verum end; end; end; dom ((Exec (I,s)) +* (o,a)) = the carrier of A by PARTFUN1:def_2; hence contradiction by A2, A3, A4, A5, FUNCT_1:2; ::_thesis: verum end; theorem :: AMISTD_4:8 for N being with_zero set for A being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N for I being Instruction of A for o being Object of A st Values o is trivial holds not o in Input I proof let N be with_zero set ; ::_thesis: for A being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N for I being Instruction of A for o being Object of A st Values o is trivial holds not o in Input I let A be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; ::_thesis: for I being Instruction of A for o being Object of A st Values o is trivial holds not o in Input I let I be Instruction of A; ::_thesis: for o being Object of A st Values o is trivial holds not o in Input I let o be Object of A; ::_thesis: ( Values o is trivial implies not o in Input I ) A1: Input I c= Out_U_Inp I by XBOOLE_1:36; assume Values o is trivial ; ::_thesis: not o in Input I hence not o in Input I by A1, Th7; ::_thesis: verum end; theorem :: AMISTD_4:9 for N being with_zero set for A being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N for I being Instruction of A for o being Object of A st Values o is trivial holds not o in Output I proof let N be with_zero set ; ::_thesis: for A being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N for I being Instruction of A for o being Object of A st Values o is trivial holds not o in Output I let A be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; ::_thesis: for I being Instruction of A for o being Object of A st Values o is trivial holds not o in Output I let I be Instruction of A; ::_thesis: for o being Object of A st Values o is trivial holds not o in Output I let o be Object of A; ::_thesis: ( Values o is trivial implies not o in Output I ) assume A1: Values o is trivial ; ::_thesis: not o in Output I Output I c= Out_U_Inp I by Th4; hence not o in Output I by A1, Th7; ::_thesis: verum end; theorem Th10: :: AMISTD_4:10 for N being with_zero set for A being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N for I being Instruction of A holds ( I is halting iff Output I is empty ) proof let N be with_zero set ; ::_thesis: for A being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N for I being Instruction of A holds ( I is halting iff Output I is empty ) let A be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; ::_thesis: for I being Instruction of A holds ( I is halting iff Output I is empty ) let I be Instruction of A; ::_thesis: ( I is halting iff Output I is empty ) thus ( I is halting implies Output I is empty ) ::_thesis: ( Output I is empty implies I is halting ) proof assume A1: for s being State of A holds Exec (I,s) = s ; :: according to EXTPRO_1:def_3 ::_thesis: Output I is empty assume not Output I is empty ; ::_thesis: contradiction then consider o being Object of A such that A2: o in Output I by SUBSET_1:4; ex s being State of A st s . o <> (Exec (I,s)) . o by A2, Def3; hence contradiction by A1; ::_thesis: verum end; assume A3: Output I is empty ; ::_thesis: I is halting let s be State of A; :: according to EXTPRO_1:def_3 ::_thesis: Exec (I,s) = s assume A4: Exec (I,s) <> s ; ::_thesis: contradiction ( dom s = the carrier of A & dom (Exec (I,s)) = the carrier of A ) by PARTFUN1:def_2; then ex x being set st ( x in the carrier of A & (Exec (I,s)) . x <> s . x ) by A4, FUNCT_1:2; hence contradiction by A3, Def3; ::_thesis: verum end; theorem Th11: :: AMISTD_4:11 for N being with_zero set for A being non empty with_non-empty_values IC-Ins-separated with_non_trivial_ObjectKinds AMI-Struct over N for I being Instruction of A st I is halting holds Out_\_Inp I is empty proof let N be with_zero set ; ::_thesis: for A being non empty with_non-empty_values IC-Ins-separated with_non_trivial_ObjectKinds AMI-Struct over N for I being Instruction of A st I is halting holds Out_\_Inp I is empty let A be non empty with_non-empty_values IC-Ins-separated with_non_trivial_ObjectKinds AMI-Struct over N; ::_thesis: for I being Instruction of A st I is halting holds Out_\_Inp I is empty let I be Instruction of A; ::_thesis: ( I is halting implies Out_\_Inp I is empty ) assume A1: I is halting ; ::_thesis: Out_\_Inp I is empty Out_\_Inp I c= Output I by Th3; then Out_\_Inp I c= {} by A1, Th10; hence Out_\_Inp I is empty by XBOOLE_1:3; ::_thesis: verum end; theorem Th12: :: AMISTD_4:12 for N being with_zero set for A being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N for I being Instruction of A st I is halting holds Out_U_Inp I is empty proof let N be with_zero set ; ::_thesis: for A being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N for I being Instruction of A st I is halting holds Out_U_Inp I is empty let A be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; ::_thesis: for I being Instruction of A st I is halting holds Out_U_Inp I is empty let I be Instruction of A; ::_thesis: ( I is halting implies Out_U_Inp I is empty ) assume A1: for s being State of A holds Exec (I,s) = s ; :: according to EXTPRO_1:def_3 ::_thesis: Out_U_Inp I is empty assume not Out_U_Inp I is empty ; ::_thesis: contradiction then consider o being Object of A such that A2: o in Out_U_Inp I by SUBSET_1:4; consider s being State of A, a being Element of Values o such that A3: Exec (I,(s +* (o,a))) <> (Exec (I,s)) +* (o,a) by A2, Def5; Exec (I,(s +* (o,a))) = s +* (o,a) by A1 .= (Exec (I,s)) +* (o,a) by A1 ; hence contradiction by A3; ::_thesis: verum end; theorem Th13: :: AMISTD_4:13 for N being with_zero set for A being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N for I being Instruction of A st I is halting holds Input I is empty proof let N be with_zero set ; ::_thesis: for A being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N for I being Instruction of A st I is halting holds Input I is empty let A be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; ::_thesis: for I being Instruction of A st I is halting holds Input I is empty let I be Instruction of A; ::_thesis: ( I is halting implies Input I is empty ) assume I is halting ; ::_thesis: Input I is empty then Input I = {} \ (Out_\_Inp I) by Th12 .= {} ; hence Input I is empty ; ::_thesis: verum end; registration let N be with_zero set ; let A be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N; let I be halting Instruction of A; cluster Input I -> empty ; coherence Input I is empty by Th13; cluster Output I -> empty ; coherence Output I is empty by Th10; cluster Out_U_Inp I -> empty ; coherence Out_U_Inp I is empty by Th12; end; registration let N be with_zero set ; cluster non empty with_non-empty_values IC-Ins-separated halting with_non_trivial_ObjectKinds for AMI-Struct over N; existence ex b1 being non empty with_non-empty_values AMI-Struct over N st ( b1 is halting & b1 is with_non_trivial_ObjectKinds & b1 is IC-Ins-separated ) proof take STC N ; ::_thesis: ( STC N is halting & STC N is with_non_trivial_ObjectKinds & STC N is IC-Ins-separated ) thus ( STC N is halting & STC N is with_non_trivial_ObjectKinds & STC N is IC-Ins-separated ) ; ::_thesis: verum end; end; registration let N be with_zero set ; let A be non empty with_non-empty_values IC-Ins-separated halting with_non_trivial_ObjectKinds AMI-Struct over N; let I be halting Instruction of A; cluster Out_\_Inp I -> empty ; coherence Out_\_Inp I is empty by Th11; end; registration let N be with_zero set ; cluster non empty with_non-empty_values IC-Ins-separated with_non_trivial_Instructions for AMI-Struct over N; existence ex b1 being non empty with_non-empty_values AMI-Struct over N st ( b1 is with_non_trivial_Instructions & b1 is IC-Ins-separated ) proof take STC N ; ::_thesis: ( STC N is with_non_trivial_Instructions & STC N is IC-Ins-separated ) thus ( STC N is with_non_trivial_Instructions & STC N is IC-Ins-separated ) ; ::_thesis: verum end; end; theorem :: AMISTD_4:14 for N being with_zero set for A being non empty with_non-empty_values IC-Ins-separated standard AMI-Struct over N for I being Instruction of A st I is sequential holds not IC in Out_\_Inp I proof let N be with_zero set ; ::_thesis: for A being non empty with_non-empty_values IC-Ins-separated standard AMI-Struct over N for I being Instruction of A st I is sequential holds not IC in Out_\_Inp I let A be non empty with_non-empty_values IC-Ins-separated standard AMI-Struct over N; ::_thesis: for I being Instruction of A st I is sequential holds not IC in Out_\_Inp I let I be Instruction of A; ::_thesis: ( I is sequential implies not IC in Out_\_Inp I ) set t = the State of A; set l = IC ; reconsider sICt = succ (IC the State of A) as Element of NAT by ORDINAL1:def_12; reconsider w = sICt as Element of Values (IC ) by MEMSTR_0:def_6; set s = the State of A +* ((IC ),w); assume for s being State of A holds (Exec (I,s)) . (IC ) = succ (IC s) ; :: according to AMISTD_1:def_8 ::_thesis: not IC in Out_\_Inp I then A1: ( (Exec (I, the State of A)) . (IC ) = succ (IC the State of A) & (Exec (I,( the State of A +* ((IC ),w)))) . (IC ) = succ (IC ( the State of A +* ((IC ),w))) ) ; dom the State of A = the carrier of A by PARTFUN1:def_2; then Exec (I, the State of A) <> Exec (I,( the State of A +* ((IC ),w))) by A1, FUNCT_7:31, ORDINAL1:9; hence not IC in Out_\_Inp I by Def4; ::_thesis: verum end; theorem :: AMISTD_4:15 for N being with_zero set for A being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N for I being Instruction of A st ex s being State of A st (Exec (I,s)) . (IC ) <> IC s holds IC in Output I by Def3; registration let N be with_zero set ; cluster non empty with_non-empty_values IC-Ins-separated standard for AMI-Struct over N; existence ex b1 being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N st b1 is standard proof take STC N ; ::_thesis: STC N is standard thus STC N is standard ; ::_thesis: verum end; end; theorem :: AMISTD_4:16 for N being with_zero set for A being non empty with_non-empty_values IC-Ins-separated standard AMI-Struct over N for I being Instruction of A st I is sequential holds IC in Output I proof let N be with_zero set ; ::_thesis: for A being non empty with_non-empty_values IC-Ins-separated standard AMI-Struct over N for I being Instruction of A st I is sequential holds IC in Output I let A be non empty with_non-empty_values IC-Ins-separated standard AMI-Struct over N; ::_thesis: for I being Instruction of A st I is sequential holds IC in Output I let I be Instruction of A; ::_thesis: ( I is sequential implies IC in Output I ) assume A1: for s being State of A holds (Exec (I,s)) . (IC ) = succ (IC s) ; :: according to AMISTD_1:def_8 ::_thesis: IC in Output I set s = the State of A; (Exec (I, the State of A)) . (IC ) = succ (IC the State of A) by A1; then (Exec (I, the State of A)) . (IC ) <> IC the State of A by ORDINAL1:9; hence IC in Output I by Def3; ::_thesis: verum end; theorem Th17: :: AMISTD_4:17 for N being with_zero set for A being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N for I being Instruction of A st ex s being State of A st (Exec (I,s)) . (IC ) <> IC s holds IC in Out_U_Inp I proof let N be with_zero set ; ::_thesis: for A being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N for I being Instruction of A st ex s being State of A st (Exec (I,s)) . (IC ) <> IC s holds IC in Out_U_Inp I let A be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; ::_thesis: for I being Instruction of A st ex s being State of A st (Exec (I,s)) . (IC ) <> IC s holds IC in Out_U_Inp I let I be Instruction of A; ::_thesis: ( ex s being State of A st (Exec (I,s)) . (IC ) <> IC s implies IC in Out_U_Inp I ) assume ex s being State of A st (Exec (I,s)) . (IC ) <> IC s ; ::_thesis: IC in Out_U_Inp I then A1: IC in Output I by Def3; Output I c= Out_U_Inp I by Th4; hence IC in Out_U_Inp I by A1; ::_thesis: verum end; theorem :: AMISTD_4:18 for N being with_zero set for A being non empty with_non-empty_values IC-Ins-separated standard AMI-Struct over N for I being Instruction of A st I is sequential holds IC in Out_U_Inp I proof let N be with_zero set ; ::_thesis: for A being non empty with_non-empty_values IC-Ins-separated standard AMI-Struct over N for I being Instruction of A st I is sequential holds IC in Out_U_Inp I let A be non empty with_non-empty_values IC-Ins-separated standard AMI-Struct over N; ::_thesis: for I being Instruction of A st I is sequential holds IC in Out_U_Inp I let I be Instruction of A; ::_thesis: ( I is sequential implies IC in Out_U_Inp I ) set s = the State of A; assume for s being State of A holds (Exec (I,s)) . (IC ) = succ (IC s) ; :: according to AMISTD_1:def_8 ::_thesis: IC in Out_U_Inp I then (Exec (I, the State of A)) . (IC ) = succ (IC the State of A) ; then (Exec (I, the State of A)) . (IC ) <> IC the State of A by ORDINAL1:9; hence IC in Out_U_Inp I by Th17; ::_thesis: verum end; theorem :: AMISTD_4:19 for N being with_zero set for A being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N for I being Instruction of A for o being Object of A st I is jump-only & o in Output I holds o = IC proof let N be with_zero set ; ::_thesis: for A being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N for I being Instruction of A for o being Object of A st I is jump-only & o in Output I holds o = IC let A be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; ::_thesis: for I being Instruction of A for o being Object of A st I is jump-only & o in Output I holds o = IC let I be Instruction of A; ::_thesis: for o being Object of A st I is jump-only & o in Output I holds o = IC let o be Object of A; ::_thesis: ( I is jump-only & o in Output I implies o = IC ) assume A1: for s being State of A for o being Object of A for J being Instruction of A st InsCode I = InsCode J & o in Data-Locations holds (Exec (J,s)) . o = s . o ; :: according to AMISTD_1:def_1,AMISTD_1:def_2 ::_thesis: ( not o in Output I or o = IC ) assume o in Output I ; ::_thesis: o = IC then ex s being State of A st s . o <> (Exec (I,s)) . o by Def3; then A2: not o in Data-Locations by A1; o in the carrier of A ; then o in {(IC )} \/ (Data-Locations ) by STRUCT_0:4; then o in {(IC )} by A2, XBOOLE_0:def_3; hence o = IC by TARSKI:def_1; ::_thesis: verum end;