:: AMISTD_1 semantic presentation begin registration let N be with_zero set ; let S be with_non-empty_values AMI-Struct over N; let i be Element of the InstructionsF of S; let s be State of S; cluster( the Execution of S . i) . s -> Relation-like Function-like ; coherence ( ( the Execution of S . i) . s is Function-like & ( the Execution of S . i) . s is Relation-like ) proof reconsider A = the Execution of S . i as Function of (product (the_Values_of S)),(product (the_Values_of S)) by FUNCT_2:66; reconsider s = s as Element of product (the_Values_of S) by CARD_3:107; A . s in product (the_Values_of S) ; hence ( ( the Execution of S . i) . s is Function-like & ( the Execution of S . i) . s is Relation-like ) ; ::_thesis: verum end; end; registration let N be with_zero set ; cluster non empty with_non-empty_values for AMI-Struct over N; existence ex b1 being AMI-Struct over N st ( not b1 is empty & b1 is with_non-empty_values ) proof take Trivial-AMI N ; ::_thesis: ( not Trivial-AMI N is empty & Trivial-AMI N is with_non-empty_values ) thus ( not Trivial-AMI N is empty & Trivial-AMI N is with_non-empty_values ) ; ::_thesis: verum end; end; definition let N be with_zero set ; let S be non empty with_non-empty_values AMI-Struct over N; let T be InsType of the InstructionsF of S; attrT is jump-only means :: AMISTD_1:def 1 for s being State of S for o being Object of S for I being Instruction of S st InsCode I = T & o in Data-Locations holds (Exec (I,s)) . o = s . o; end; :: deftheorem defines jump-only AMISTD_1:def_1_:_ for N being with_zero set for S being non empty with_non-empty_values AMI-Struct over N for T being InsType of the InstructionsF of S holds ( T is jump-only iff for s being State of S for o being Object of S for I being Instruction of S st InsCode I = T & o in Data-Locations holds (Exec (I,s)) . o = s . o ); definition let N be with_zero set ; let S be non empty with_non-empty_values AMI-Struct over N; let I be Instruction of S; attrI is jump-only means :: AMISTD_1:def 2 InsCode I is jump-only ; end; :: deftheorem defines jump-only AMISTD_1:def_2_:_ for N being with_zero set for S being non empty with_non-empty_values AMI-Struct over N for I being Instruction of S holds ( I is jump-only iff InsCode I is jump-only ); definition let N be with_zero set ; let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; let l be Nat; let i be Element of the InstructionsF of S; func NIC (i,l) -> Subset of NAT equals :: AMISTD_1:def 3 { (IC (Exec (i,ss))) where ss is Element of product (the_Values_of S) : IC ss = l } ; coherence { (IC (Exec (i,ss))) where ss is Element of product (the_Values_of S) : IC ss = l } is Subset of NAT proof { (IC (Exec (i,ss))) where ss is Element of product (the_Values_of S) : IC ss = l } c= NAT proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (IC (Exec (i,ss))) where ss is Element of product (the_Values_of S) : IC ss = l } or e in NAT ) assume e in { (IC (Exec (i,ss))) where ss is Element of product (the_Values_of S) : IC ss = l } ; ::_thesis: e in NAT then ex ss being Element of product (the_Values_of S) st ( e = IC (Exec (i,ss)) & IC ss = l ) ; hence e in NAT ; ::_thesis: verum end; hence { (IC (Exec (i,ss))) where ss is Element of product (the_Values_of S) : IC ss = l } is Subset of NAT ; ::_thesis: verum end; end; :: deftheorem defines NIC AMISTD_1:def_3_:_ for N being with_zero set for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N for l being Nat for i being Element of the InstructionsF of S holds NIC (i,l) = { (IC (Exec (i,ss))) where ss is Element of product (the_Values_of S) : IC ss = l } ; Lm1: now__::_thesis:_for_N_being_with_zero_set_ for_S_being_non_empty_with_non-empty_values_IC-Ins-separated_AMI-Struct_over_N for_i_being_Element_of_the_InstructionsF_of_S for_l_being_Element_of_NAT_ for_s_being_State_of_S for_P_being_Instruction-Sequence_of_S_holds_IC_(Following_((P_+*_(l,i)),(s_+*_((IC_),l))))_in_NIC_(i,l) let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N for i being Element of the InstructionsF of S for l being Element of NAT for s being State of S for P being Instruction-Sequence of S holds IC (Following ((P +* (l,i)),(s +* ((IC ),l)))) in NIC (i,l) let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; ::_thesis: for i being Element of the InstructionsF of S for l being Element of NAT for s being State of S for P being Instruction-Sequence of S holds IC (Following ((P +* (l,i)),(s +* ((IC ),l)))) in NIC (i,l) let i be Element of the InstructionsF of S; ::_thesis: for l being Element of NAT for s being State of S for P being Instruction-Sequence of S holds IC (Following ((P +* (l,i)),(s +* ((IC ),l)))) in NIC (i,l) let l be Element of NAT ; ::_thesis: for s being State of S for P being Instruction-Sequence of S holds IC (Following ((P +* (l,i)),(s +* ((IC ),l)))) in NIC (i,l) let s be State of S; ::_thesis: for P being Instruction-Sequence of S holds IC (Following ((P +* (l,i)),(s +* ((IC ),l)))) in NIC (i,l) let P be Instruction-Sequence of S; ::_thesis: IC (Following ((P +* (l,i)),(s +* ((IC ),l)))) in NIC (i,l) reconsider t = s +* ((IC ),l) as Element of product (the_Values_of S) by CARD_3:107; l in NAT ; then A1: l in dom P by PARTFUN1:def_2; IC in dom s by MEMSTR_0:2; then A2: IC t = l by FUNCT_7:31; then CurInstr ((P +* (l,i)),t) = (P +* (l,i)) . l by PBOOLE:143 .= i by A1, FUNCT_7:31 ; hence IC (Following ((P +* (l,i)),(s +* ((IC ),l)))) in NIC (i,l) by A2; ::_thesis: verum end; registration let N be with_zero set ; let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; let i be Element of the InstructionsF of S; let l be Element of NAT ; cluster NIC (i,l) -> non empty ; coherence not NIC (i,l) is empty by Lm1; end; definition let N be with_zero set ; let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; let i be Element of the InstructionsF of S; func JUMP i -> Subset of NAT equals :: AMISTD_1:def 4 meet { (NIC (i,l)) where l is Element of NAT : verum } ; coherence meet { (NIC (i,l)) where l is Element of NAT : verum } is Subset of NAT proof set X = { (NIC (i,l)) where l is Element of NAT : verum } ; { (NIC (i,l)) where l is Element of NAT : verum } c= bool NAT proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (NIC (i,l)) where l is Element of NAT : verum } or x in bool NAT ) assume x in { (NIC (i,l)) where l is Element of NAT : verum } ; ::_thesis: x in bool NAT then ex l being Element of NAT st x = NIC (i,l) ; hence x in bool NAT ; ::_thesis: verum end; then reconsider X = { (NIC (i,l)) where l is Element of NAT : verum } as Subset-Family of NAT ; meet X c= NAT ; hence meet { (NIC (i,l)) where l is Element of NAT : verum } is Subset of NAT ; ::_thesis: verum end; end; :: deftheorem defines JUMP AMISTD_1:def_4_:_ for N being with_zero set for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N for i being Element of the InstructionsF of S holds JUMP i = meet { (NIC (i,l)) where l is Element of NAT : verum } ; definition let N be with_zero set ; let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; let l be Nat; func SUCC (l,S) -> Subset of NAT equals :: AMISTD_1:def 5 union { ((NIC (i,l)) \ (JUMP i)) where i is Element of the InstructionsF of S : verum } ; coherence union { ((NIC (i,l)) \ (JUMP i)) where i is Element of the InstructionsF of S : verum } is Subset of NAT proof set X = { ((NIC (i,l)) \ (JUMP i)) where i is Element of the InstructionsF of S : verum } ; { ((NIC (i,l)) \ (JUMP i)) where i is Element of the InstructionsF of S : verum } c= bool NAT proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { ((NIC (i,l)) \ (JUMP i)) where i is Element of the InstructionsF of S : verum } or x in bool NAT ) assume x in { ((NIC (i,l)) \ (JUMP i)) where i is Element of the InstructionsF of S : verum } ; ::_thesis: x in bool NAT then ex i being Element of the InstructionsF of S st x = (NIC (i,l)) \ (JUMP i) ; hence x in bool NAT ; ::_thesis: verum end; then reconsider X = { ((NIC (i,l)) \ (JUMP i)) where i is Element of the InstructionsF of S : verum } as Subset-Family of NAT ; union X c= NAT ; hence union { ((NIC (i,l)) \ (JUMP i)) where i is Element of the InstructionsF of S : verum } is Subset of NAT ; ::_thesis: verum end; end; :: deftheorem defines SUCC AMISTD_1:def_5_:_ for N being with_zero set for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N for l being Nat holds SUCC (l,S) = union { ((NIC (i,l)) \ (JUMP i)) where i is Element of the InstructionsF of S : verum } ; theorem Th1: :: AMISTD_1:1 for N being with_zero set for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N for i being Element of the InstructionsF of S st ( for l being Element of NAT holds NIC (i,l) = {l} ) holds JUMP i is empty proof let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N for i being Element of the InstructionsF of S st ( for l being Element of NAT holds NIC (i,l) = {l} ) holds JUMP i is empty let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; ::_thesis: for i being Element of the InstructionsF of S st ( for l being Element of NAT holds NIC (i,l) = {l} ) holds JUMP i is empty let i be Element of the InstructionsF of S; ::_thesis: ( ( for l being Element of NAT holds NIC (i,l) = {l} ) implies JUMP i is empty ) set p = 0 ; set q = 1; set X = { (NIC (i,l)) where l is Element of NAT : verum } ; reconsider p = 0 , q = 1 as Element of NAT ; assume A1: for l being Element of NAT holds NIC (i,l) = {l} ; ::_thesis: JUMP i is empty assume not JUMP i is empty ; ::_thesis: contradiction then consider x being set such that A2: x in meet { (NIC (i,l)) where l is Element of NAT : verum } by XBOOLE_0:def_1; NIC (i,p) = {p} by A1; then {p} in { (NIC (i,l)) where l is Element of NAT : verum } ; then A3: x in {p} by A2, SETFAM_1:def_1; NIC (i,q) = {q} by A1; then {q} in { (NIC (i,l)) where l is Element of NAT : verum } ; then x in {q} by A2, SETFAM_1:def_1; hence contradiction by A3, TARSKI:def_1; ::_thesis: verum end; theorem Th2: :: AMISTD_1:2 for N being with_zero set for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N for il being Element of NAT for i being Instruction of S st i is halting holds NIC (i,il) = {il} proof let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N for il being Element of NAT for i being Instruction of S st i is halting holds NIC (i,il) = {il} let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; ::_thesis: for il being Element of NAT for i being Instruction of S st i is halting holds NIC (i,il) = {il} let il be Element of NAT ; ::_thesis: for i being Instruction of S st i is halting holds NIC (i,il) = {il} let i be Instruction of S; ::_thesis: ( i is halting implies NIC (i,il) = {il} ) assume A1: for s being State of S holds Exec (i,s) = s ; :: according to EXTPRO_1:def_3 ::_thesis: NIC (i,il) = {il} hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: {il} c= NIC (i,il) let n be set ; ::_thesis: ( n in NIC (i,il) implies n in {il} ) assume n in NIC (i,il) ; ::_thesis: n in {il} then ex s being Element of product (the_Values_of S) st ( n = IC (Exec (i,s)) & IC s = il ) ; then n = il by A1; hence n in {il} by TARSKI:def_1; ::_thesis: verum end; set s = the State of S; set P = the Instruction-Sequence of S; let n be set ; :: according to TARSKI:def_3 ::_thesis: ( not n in {il} or n in NIC (i,il) ) assume n in {il} ; ::_thesis: n in NIC (i,il) then A2: n = il by TARSKI:def_1; il in NAT ; then A3: il in dom the Instruction-Sequence of S by PARTFUN1:def_2; A4: IC in dom the State of S by MEMSTR_0:2; then IC ( the State of S +* ((IC ),il)) = il by FUNCT_7:31; then CurInstr (( the Instruction-Sequence of S +* (il,i)),( the State of S +* ((IC ),il))) = ( the Instruction-Sequence of S +* (il,i)) . il by PBOOLE:143 .= i by A3, FUNCT_7:31 ; then IC (Following (( the Instruction-Sequence of S +* (il,i)),( the State of S +* ((IC ),il)))) = IC ( the State of S +* ((IC ),il)) by A1 .= n by A2, A4, FUNCT_7:31 ; hence n in NIC (i,il) by Lm1; ::_thesis: verum end; begin definition let N be with_zero set ; let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; attrS is standard means :Def6: :: AMISTD_1:def 6 for m, n being Element of NAT holds ( m <= n iff ex f being non empty FinSequence of NAT st ( f /. 1 = m & f /. (len f) = n & ( for n being Element of NAT st 1 <= n & n < len f holds f /. (n + 1) in SUCC ((f /. n),S) ) ) ); end; :: deftheorem Def6 defines standard AMISTD_1:def_6_:_ for N being with_zero set for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N holds ( S is standard iff for m, n being Element of NAT holds ( m <= n iff ex f being non empty FinSequence of NAT st ( f /. 1 = m & f /. (len f) = n & ( for n being Element of NAT st 1 <= n & n < len f holds f /. (n + 1) in SUCC ((f /. n),S) ) ) ) ); Lm2: for k being Element of NAT for N being with_zero set for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N ex f being non empty FinSequence of NAT st ( f /. 1 = k & f /. (len f) = k & ( for n being Element of NAT st 1 <= n & n < len f holds f /. (n + 1) in SUCC ((f /. n),S) ) ) proof let k be Element of NAT ; ::_thesis: for N being with_zero set for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N ex f being non empty FinSequence of NAT st ( f /. 1 = k & f /. (len f) = k & ( for n being Element of NAT st 1 <= n & n < len f holds f /. (n + 1) in SUCC ((f /. n),S) ) ) let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N ex f being non empty FinSequence of NAT st ( f /. 1 = k & f /. (len f) = k & ( for n being Element of NAT st 1 <= n & n < len f holds f /. (n + 1) in SUCC ((f /. n),S) ) ) let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; ::_thesis: ex f being non empty FinSequence of NAT st ( f /. 1 = k & f /. (len f) = k & ( for n being Element of NAT st 1 <= n & n < len f holds f /. (n + 1) in SUCC ((f /. n),S) ) ) reconsider l = k as Element of NAT ; reconsider f = <*l*> as non empty FinSequence of NAT ; take f ; ::_thesis: ( f /. 1 = k & f /. (len f) = k & ( for n being Element of NAT st 1 <= n & n < len f holds f /. (n + 1) in SUCC ((f /. n),S) ) ) thus f /. 1 = k by FINSEQ_4:16; ::_thesis: ( f /. (len f) = k & ( for n being Element of NAT st 1 <= n & n < len f holds f /. (n + 1) in SUCC ((f /. n),S) ) ) hence ( f /. (len f) = k & ( for n being Element of NAT st 1 <= n & n < len f holds f /. (n + 1) in SUCC ((f /. n),S) ) ) by FINSEQ_1:39; ::_thesis: verum end; theorem Th3: :: AMISTD_1:3 for N being with_zero set for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N holds ( S is standard iff for k being Element of NAT holds ( k + 1 in SUCC (k,S) & ( for j being Element of NAT st j in SUCC (k,S) holds k <= j ) ) ) proof let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N holds ( S is standard iff for k being Element of NAT holds ( k + 1 in SUCC (k,S) & ( for j being Element of NAT st j in SUCC (k,S) holds k <= j ) ) ) let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; ::_thesis: ( S is standard iff for k being Element of NAT holds ( k + 1 in SUCC (k,S) & ( for j being Element of NAT st j in SUCC (k,S) holds k <= j ) ) ) hereby ::_thesis: ( ( for k being Element of NAT holds ( k + 1 in SUCC (k,S) & ( for j being Element of NAT st j in SUCC (k,S) holds k <= j ) ) ) implies S is standard ) assume A1: S is standard ; ::_thesis: for k being Element of NAT holds ( k + 1 in SUCC (k,S) & ( for j being Element of NAT st j in SUCC (k,S) holds k <= j ) ) let k be Element of NAT ; ::_thesis: ( k + 1 in SUCC (k,S) & ( for j being Element of NAT st j in SUCC (k,S) holds k <= j ) ) k <= k + 1 by NAT_1:11; then consider F being non empty FinSequence of NAT such that A2: F /. 1 = k and A3: F /. (len F) = k + 1 and A4: for n being Element of NAT st 1 <= n & n < len F holds F /. (n + 1) in SUCC ((F /. n),S) by A1, Def6; set F1 = F -| (k + 1); set x = (k + 1) .. F; A5: k + 1 in rng F by A3, REVROT_1:3; then A6: len (F -| (k + 1)) = ((k + 1) .. F) - 1 by FINSEQ_4:34; then A7: (len (F -| (k + 1))) + 1 = (k + 1) .. F ; A8: (k + 1) .. F in dom F by A5, FINSEQ_4:20; then A9: F /. ((len (F -| (k + 1))) + 1) = F . ((k + 1) .. F) by A6, PARTFUN1:def_6 .= k + 1 by A5, FINSEQ_4:19 ; (k + 1) .. F <= len F by A8, FINSEQ_3:25; then A10: len (F -| (k + 1)) < len F by A7, NAT_1:13; 1 <= len F by NAT_1:14; then A11: 1 in dom F by FINSEQ_3:25; then A12: F /. 1 = F . 1 by PARTFUN1:def_6; A13: F . ((k + 1) .. F) = k + 1 by A5, FINSEQ_4:19; A14: k <> k + 1 ; then A15: len (F -| (k + 1)) <> 0 by A2, A13, A11, A6, PARTFUN1:def_6; 1 <= (k + 1) .. F by A8, FINSEQ_3:25; then 1 < (k + 1) .. F by A2, A14, A13, A12, XXREAL_0:1; then A16: 1 <= len (F -| (k + 1)) by A7, NAT_1:13; reconsider F1 = F -| (k + 1) as non empty FinSequence of NAT by A15, A5, FINSEQ_4:41; set m = F /. (len F1); reconsider m = F /. (len F1) as Element of NAT ; A17: len F1 in dom F by A16, A10, FINSEQ_3:25; A18: len F1 in dom F1 by A16, FINSEQ_3:25; then A19: F1 /. (len F1) = F1 . (len F1) by PARTFUN1:def_6 .= F . (len F1) by A5, A18, FINSEQ_4:36 .= F /. (len F1) by A17, PARTFUN1:def_6 ; A20: now__::_thesis:_not_m_=_k_+_1 rng F1 misses {(k + 1)} by A5, FINSEQ_4:38; then (rng F1) /\ {(k + 1)} = {} by XBOOLE_0:def_7; then A21: ( not k + 1 in rng F1 or not k + 1 in {(k + 1)} ) by XBOOLE_0:def_4; assume A22: m = k + 1 ; ::_thesis: contradiction A23: len F1 in dom F1 by A16, FINSEQ_3:25; then F1 /. (len F1) = F1 . (len F1) by PARTFUN1:def_6; hence contradiction by A19, A22, A21, A23, FUNCT_1:def_3, TARSKI:def_1; ::_thesis: verum end; reconsider F2 = <*(F /. (len F1)),(F /. ((k + 1) .. F))*> as non empty FinSequence of NAT ; A24: len F2 = 2 by FINSEQ_1:44; then A25: 2 in dom F2 by FINSEQ_3:25; then A26: F2 /. (len F2) = F2 . 2 by A24, PARTFUN1:def_6 .= F /. ((k + 1) .. F) by FINSEQ_1:44 .= k + 1 by A13, A8, PARTFUN1:def_6 ; A27: 1 in dom F2 by A24, FINSEQ_3:25; A28: now__::_thesis:_for_n_being_Element_of_NAT_st_1_<=_n_&_n_<_len_F2_holds_ F2_/._(n_+_1)_in_SUCC_((F2_/._n),S) let n be Element of NAT ; ::_thesis: ( 1 <= n & n < len F2 implies F2 /. (n + 1) in SUCC ((F2 /. n),S) ) assume ( 1 <= n & n < len F2 ) ; ::_thesis: F2 /. (n + 1) in SUCC ((F2 /. n),S) then ( n <> 0 & n < 2 ) by FINSEQ_1:44; then A29: n = 1 by NAT_1:26; then A30: F2 /. n = F2 . 1 by A27, PARTFUN1:def_6 .= F /. (len F1) by FINSEQ_1:44 ; F2 /. (n + 1) = F2 . 2 by A25, A29, PARTFUN1:def_6 .= F /. ((len F1) + 1) by A6, FINSEQ_1:44 ; hence F2 /. (n + 1) in SUCC ((F2 /. n),S) by A4, A16, A10, A30; ::_thesis: verum end; A31: now__::_thesis:_for_n_being_Element_of_NAT_st_1_<=_n_&_n_<_len_F1_holds_ F1_/._(n_+_1)_in_SUCC_((F1_/._n),S) let n be Element of NAT ; ::_thesis: ( 1 <= n & n < len F1 implies F1 /. (n + 1) in SUCC ((F1 /. n),S) ) assume that A32: 1 <= n and A33: n < len F1 ; ::_thesis: F1 /. (n + 1) in SUCC ((F1 /. n),S) A34: 1 <= n + 1 by A32, NAT_1:13; A35: n + 1 <= len F1 by A33, NAT_1:13; then n + 1 <= len F by A10, XXREAL_0:2; then A36: n + 1 in dom F by A34, FINSEQ_3:25; n <= len F by A10, A33, XXREAL_0:2; then A37: n in dom F by A32, FINSEQ_3:25; A38: n in dom F1 by A32, A33, FINSEQ_3:25; then A39: F1 /. n = F1 . n by PARTFUN1:def_6 .= F . n by A5, A38, FINSEQ_4:36 .= F /. n by A37, PARTFUN1:def_6 ; A40: n < len F by A10, A33, XXREAL_0:2; A41: n + 1 in dom F1 by A34, A35, FINSEQ_3:25; then F1 /. (n + 1) = F1 . (n + 1) by PARTFUN1:def_6 .= F . (n + 1) by A5, A41, FINSEQ_4:36 .= F /. (n + 1) by A36, PARTFUN1:def_6 ; hence F1 /. (n + 1) in SUCC ((F1 /. n),S) by A4, A32, A39, A40; ::_thesis: verum end; F2 /. 1 = F2 . 1 by A27, PARTFUN1:def_6 .= m by FINSEQ_1:44 ; then A42: m <= k + 1 by A1, A26, A28, Def6; A43: 1 in dom F1 by A16, FINSEQ_3:25; then F1 /. 1 = F1 . 1 by PARTFUN1:def_6 .= F . 1 by A5, A43, FINSEQ_4:36 .= k by A2, A11, PARTFUN1:def_6 ; then k <= m by A1, A19, A31, Def6; then ( m = k or m = k + 1 ) by A42, NAT_1:9; hence k + 1 in SUCC (k,S) by A4, A16, A10, A9, A20; ::_thesis: for j being Element of NAT st j in SUCC (k,S) holds k <= j let j be Element of NAT ; ::_thesis: ( j in SUCC (k,S) implies k <= j ) reconsider fk = k, fj = j as Element of NAT ; reconsider F = <*fk,fj*> as non empty FinSequence of NAT ; A44: len F = 2 by FINSEQ_1:44; then A45: 2 in dom F by FINSEQ_3:25; A46: 1 in dom F by A44, FINSEQ_3:25; then A47: F /. 1 = F . 1 by PARTFUN1:def_6 .= k by FINSEQ_1:44 ; assume A48: j in SUCC (k,S) ; ::_thesis: k <= j A49: now__::_thesis:_for_n_being_Element_of_NAT_st_1_<=_n_&_n_<_len_F_holds_ F_/._(n_+_1)_in_SUCC_((F_/._n),S) let n be Element of NAT ; ::_thesis: ( 1 <= n & n < len F implies F /. (n + 1) in SUCC ((F /. n),S) ) assume ( 1 <= n & n < len F ) ; ::_thesis: F /. (n + 1) in SUCC ((F /. n),S) then ( n <> 0 & n < 2 ) by FINSEQ_1:44; then A50: n = 1 by NAT_1:26; then A51: F /. n = F . 1 by A46, PARTFUN1:def_6 .= k by FINSEQ_1:44 ; F /. (n + 1) = F . 2 by A45, A50, PARTFUN1:def_6 .= j by FINSEQ_1:44 ; hence F /. (n + 1) in SUCC ((F /. n),S) by A48, A51; ::_thesis: verum end; F /. (len F) = F . 2 by A44, A45, PARTFUN1:def_6 .= j by FINSEQ_1:44 ; hence k <= j by A1, A47, A49, Def6; ::_thesis: verum end; assume A52: for k being Element of NAT holds ( k + 1 in SUCC (k,S) & ( for j being Element of NAT st j in SUCC (k,S) holds k <= j ) ) ; ::_thesis: S is standard thus S is standard ::_thesis: verum proof let m, n be Element of NAT ; :: according to AMISTD_1:def_6 ::_thesis: ( m <= n iff ex f being non empty FinSequence of NAT st ( f /. 1 = m & f /. (len f) = n & ( for n being Element of NAT st 1 <= n & n < len f holds f /. (n + 1) in SUCC ((f /. n),S) ) ) ) thus ( m <= n implies ex f being non empty FinSequence of NAT st ( f /. 1 = m & f /. (len f) = n & ( for k being Element of NAT st 1 <= k & k < len f holds f /. (k + 1) in SUCC ((f /. k),S) ) ) ) ::_thesis: ( ex f being non empty FinSequence of NAT st ( f /. 1 = m & f /. (len f) = n & ( for n being Element of NAT st 1 <= n & n < len f holds f /. (n + 1) in SUCC ((f /. n),S) ) ) implies m <= n ) proof assume A53: m <= n ; ::_thesis: ex f being non empty FinSequence of NAT st ( f /. 1 = m & f /. (len f) = n & ( for k being Element of NAT st 1 <= k & k < len f holds f /. (k + 1) in SUCC ((f /. k),S) ) ) percases ( m = n or m < n ) by A53, XXREAL_0:1; suppose m = n ; ::_thesis: ex f being non empty FinSequence of NAT st ( f /. 1 = m & f /. (len f) = n & ( for k being Element of NAT st 1 <= k & k < len f holds f /. (k + 1) in SUCC ((f /. k),S) ) ) hence ex f being non empty FinSequence of NAT st ( f /. 1 = m & f /. (len f) = n & ( for n being Element of NAT st 1 <= n & n < len f holds f /. (n + 1) in SUCC ((f /. n),S) ) ) by Lm2; ::_thesis: verum end; supposeA54: m < n ; ::_thesis: ex f being non empty FinSequence of NAT st ( f /. 1 = m & f /. (len f) = n & ( for k being Element of NAT st 1 <= k & k < len f holds f /. (k + 1) in SUCC ((f /. k),S) ) ) thus ex f being non empty FinSequence of NAT st ( f /. 1 = m & f /. (len f) = n & ( for n being Element of NAT st 1 <= n & n < len f holds f /. (n + 1) in SUCC ((f /. n),S) ) ) ::_thesis: verum proof set mn = n -' m; deffunc H1( Nat) -> Element of NAT = (m + $1) -' 1; consider F being FinSequence of NAT such that A55: len F = (n -' m) + 1 and A56: for j being Nat st j in dom F holds F . j = H1(j) from FINSEQ_2:sch_1(); reconsider F = F as non empty FinSequence of NAT by A55; take F ; ::_thesis: ( F /. 1 = m & F /. (len F) = n & ( for n being Element of NAT st 1 <= n & n < len F holds F /. (n + 1) in SUCC ((F /. n),S) ) ) A57: 1 <= (n -' m) + 1 by NAT_1:11; then A58: 1 in dom F by A55, FINSEQ_3:25; hence F /. 1 = F . 1 by PARTFUN1:def_6 .= (m + 1) -' 1 by A56, A58 .= m by NAT_D:34 ; ::_thesis: ( F /. (len F) = n & ( for n being Element of NAT st 1 <= n & n < len F holds F /. (n + 1) in SUCC ((F /. n),S) ) ) m + 1 <= n by A54, INT_1:7; then 1 <= n - m by XREAL_1:19; then 0 <= n - m by XXREAL_0:2; then A59: n -' m = n - m by XREAL_0:def_2; A60: len F in dom F by A55, A57, FINSEQ_3:25; hence F /. (len F) = F . (len F) by PARTFUN1:def_6 .= (m + ((n -' m) + 1)) -' 1 by A55, A56, A60 .= ((m + (n -' m)) + 1) -' 1 .= n by A59, NAT_D:34 ; ::_thesis: for n being Element of NAT st 1 <= n & n < len F holds F /. (n + 1) in SUCC ((F /. n),S) let p be Element of NAT ; ::_thesis: ( 1 <= p & p < len F implies F /. (p + 1) in SUCC ((F /. p),S) ) assume that A61: 1 <= p and A62: p < len F ; ::_thesis: F /. (p + 1) in SUCC ((F /. p),S) A63: p in dom F by A61, A62, FINSEQ_3:25; then A64: F /. p = F . p by PARTFUN1:def_6 .= (m + p) -' 1 by A56, A63 ; A65: p <= m + p by NAT_1:11; ( 1 <= p + 1 & p + 1 <= len F ) by A61, A62, NAT_1:13; then A66: p + 1 in dom F by FINSEQ_3:25; then F /. (p + 1) = F . (p + 1) by PARTFUN1:def_6 .= (m + (p + 1)) -' 1 by A56, A66 .= ((m + p) + 1) -' 1 .= ((m + p) -' 1) + 1 by A61, A65, NAT_D:38, XXREAL_0:2 ; hence F /. (p + 1) in SUCC ((F /. p),S) by A52, A64; ::_thesis: verum end; end; end; end; given F being non empty FinSequence of NAT such that A67: F /. 1 = m and A68: F /. (len F) = n and A69: for n being Element of NAT st 1 <= n & n < len F holds F /. (n + 1) in SUCC ((F /. n),S) ; ::_thesis: m <= n defpred S1[ Element of NAT ] means ( 1 <= $1 & $1 <= len F implies ex l being Element of NAT st ( F /. $1 = l & m <= l ) ); A70: now__::_thesis:_for_k_being_Element_of_NAT_st_S1[k]_holds_ S1[k_+_1] let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A71: S1[k] ; ::_thesis: S1[k + 1] now__::_thesis:_(_1_<=_k_+_1_&_k_+_1_<=_len_F_implies_ex_l_being_Element_of_NAT_st_ (_F_/._(k_+_1)_=_l_&_m_<=_l_)_) assume that 1 <= k + 1 and A72: k + 1 <= len F ; ::_thesis: ex l being Element of NAT st ( F /. (k + 1) = l & m <= l ) percases ( k = 0 or k > 0 ) by NAT_1:3; suppose k = 0 ; ::_thesis: ex l being Element of NAT st ( F /. (k + 1) = l & m <= l ) hence ex l being Element of NAT st ( F /. (k + 1) = l & m <= l ) by A67; ::_thesis: verum end; supposeA73: k > 0 ; ::_thesis: ex l being Element of NAT st ( F /. (k + 1) = l & m <= l ) set l1 = F /. (k + 1); consider l being Element of NAT such that A74: F /. k = l and A75: m <= l by A71, A72, A73, NAT_1:13, NAT_1:14; reconsider l1 = F /. (k + 1) as Element of NAT ; k < len F by A72, NAT_1:13; then F /. (k + 1) in SUCC ((F /. k),S) by A69, A73, NAT_1:14; then l <= l1 by A52, A74; hence ex l being Element of NAT st ( F /. (k + 1) = l & m <= l ) by A75, XXREAL_0:2; ::_thesis: verum end; end; end; hence S1[k + 1] ; ::_thesis: verum end; A76: 1 <= len F by NAT_1:14; A77: S1[ 0 ] ; for k being Element of NAT holds S1[k] from NAT_1:sch_1(A77, A70); then ex l being Element of NAT st ( F /. (len F) = l & m <= l ) by A76; hence m <= n by A68; ::_thesis: verum end; end; set III = {[1,0,0],[0,0,0]}; begin definition let N be with_zero set ; func STC N -> strict AMI-Struct over N means :Def7: :: AMISTD_1:def 7 ( the carrier of it = {0} & the ZeroF of it = 0 & the InstructionsF of it = {[0,0,0],[1,0,0]} & the Object-Kind of it = 0 .--> 0 & the ValuesF of it = N --> NAT & ex f being Function of (product (the_Values_of it)),(product (the_Values_of it)) st ( ( for s being Element of product (the_Values_of it) holds f . s = s +* (0 .--> (succ (s . 0))) ) & the Execution of it = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product (the_Values_of it)))) ) ); existence ex b1 being strict AMI-Struct over N st ( the carrier of b1 = {0} & the ZeroF of b1 = 0 & the InstructionsF of b1 = {[0,0,0],[1,0,0]} & the Object-Kind of b1 = 0 .--> 0 & the ValuesF of b1 = N --> NAT & ex f being Function of (product (the_Values_of b1)),(product (the_Values_of b1)) st ( ( for s being Element of product (the_Values_of b1) holds f . s = s +* (0 .--> (succ (s . 0))) ) & the Execution of b1 = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product (the_Values_of b1)))) ) ) proof set O = {0}; set V = N --> NAT; reconsider IC1 = 0 as Element of {0} by TARSKI:def_1; reconsider i = [0,0,0] as Element of {[1,0,0],[0,0,0]} by TARSKI:def_2; A1: 0 in N by MEASURE6:def_2; then A2: (N --> NAT) * (0 .--> 0) = 0 .--> NAT by FUNCOP_1:89; then A3: dom ((N --> NAT) * (0 .--> 0)) = {0} by FUNCOP_1:13; A4: dom (0 .--> 0) = {0} by FUNCOP_1:13; rng (0 .--> 0) = {0} by FUNCOP_1:88; then rng (0 .--> 0) c= N by A1, ZFMISC_1:31; then reconsider Ok = 0 .--> 0 as Function of {0},N by A4, RELSET_1:4; deffunc H1( Element of product ((N --> NAT) * Ok)) -> set = $1 +* (0 .--> (succ ($1 . 0))); A5: now__::_thesis:_for_s_being_Element_of_product_((N_-->_NAT)_*_Ok)_holds_H1(s)_in_product_((N_-->_NAT)_*_Ok) let s be Element of product ((N --> NAT) * Ok); ::_thesis: H1(s) in product ((N --> NAT) * Ok) now__::_thesis:_(_dom_(s_+*_(0_.-->_(succ_(s_._0))))_=_dom_((N_-->_NAT)_*_Ok)_&_(_for_o_being_set_st_o_in_dom_((N_-->_NAT)_*_Ok)_holds_ (s_+*_(0_.-->_(succ_(s_._0))))_._o_in_((N_-->_NAT)_*_Ok)_._o_)_) thus dom (s +* (0 .--> (succ (s . 0)))) = (dom s) \/ (dom (0 .--> (succ (s . 0)))) by FUNCT_4:def_1 .= (dom s) \/ {0} by FUNCOP_1:13 .= {0} \/ {0} by PARTFUN1:def_2 .= dom ((N --> NAT) * Ok) by A3 ; ::_thesis: for o being set st o in dom ((N --> NAT) * Ok) holds (s +* (0 .--> (succ (s . 0)))) . o in ((N --> NAT) * Ok) . o let o be set ; ::_thesis: ( o in dom ((N --> NAT) * Ok) implies (s +* (0 .--> (succ (s . 0)))) . o in ((N --> NAT) * Ok) . o ) A6: dom (0 .--> (succ (s . 0))) = {0} by FUNCOP_1:13; assume A7: o in dom ((N --> NAT) * Ok) ; ::_thesis: (s +* (0 .--> (succ (s . 0)))) . o in ((N --> NAT) * Ok) . o A8: o = 0 by A7, TARSKI:def_1; A9: ((N --> NAT) * Ok) . o = NAT by A7, A2, FUNCOP_1:7; A10: (s +* (0 .--> (succ (s . 0)))) . o = (0 .--> (succ (s . 0))) . o by A6, A7, FUNCT_4:13 .= succ (s . 0) by A7, FUNCOP_1:7 ; 0 in dom ((N --> NAT) * Ok) by A3, TARSKI:def_1; then reconsider k = s . 0 as Element of NAT by A8, A9, CARD_3:9; succ k in NAT ; hence (s +* (0 .--> (succ (s . 0)))) . o in ((N --> NAT) * Ok) . o by A9, A10; ::_thesis: verum end; hence H1(s) in product ((N --> NAT) * Ok) by CARD_3:9; ::_thesis: verum end; consider f being Function of (product ((N --> NAT) * Ok)),(product ((N --> NAT) * Ok)) such that A11: for s being Element of product ((N --> NAT) * Ok) holds f . s = H1(s) from FUNCT_2:sch_8(A5); set E = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product ((N --> NAT) * Ok)))); A12: dom (([1,0,0] .--> f) +* ([0,0,0] .--> (id (product ((N --> NAT) * Ok))))) = (dom ([1,0,0] .--> f)) \/ (dom ([0,0,0] .--> (id (product ((N --> NAT) * Ok))))) by FUNCT_4:def_1 .= {[1,0,0]} \/ (dom ([0,0,0] .--> (id (product ((N --> NAT) * Ok))))) by FUNCOP_1:13 .= {[1,0,0]} \/ {[0,0,0]} by FUNCOP_1:13 .= {[1,0,0],[0,0,0]} by ENUMSET1:1 ; A13: ( rng ([1,0,0] .--> f) c= {f} & rng ([0,0,0] .--> (id (product ((N --> NAT) * Ok)))) c= {(id (product ((N --> NAT) * Ok)))} ) by FUNCOP_1:13; A14: rng (([1,0,0] .--> f) +* ([0,0,0] .--> (id (product ((N --> NAT) * Ok))))) c= (rng ([1,0,0] .--> f)) \/ (rng ([0,0,0] .--> (id (product ((N --> NAT) * Ok))))) by FUNCT_4:17; rng (([1,0,0] .--> f) +* ([0,0,0] .--> (id (product ((N --> NAT) * Ok))))) c= Funcs ((product ((N --> NAT) * Ok)),(product ((N --> NAT) * Ok))) proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in rng (([1,0,0] .--> f) +* ([0,0,0] .--> (id (product ((N --> NAT) * Ok))))) or e in Funcs ((product ((N --> NAT) * Ok)),(product ((N --> NAT) * Ok))) ) assume e in rng (([1,0,0] .--> f) +* ([0,0,0] .--> (id (product ((N --> NAT) * Ok))))) ; ::_thesis: e in Funcs ((product ((N --> NAT) * Ok)),(product ((N --> NAT) * Ok))) then ( e in rng ([1,0,0] .--> f) or e in rng ([0,0,0] .--> (id (product ((N --> NAT) * Ok)))) ) by A14, XBOOLE_0:def_3; then ( e = f or e = id (product ((N --> NAT) * Ok)) ) by A13, TARSKI:def_1; hence e in Funcs ((product ((N --> NAT) * Ok)),(product ((N --> NAT) * Ok))) by FUNCT_2:9; ::_thesis: verum end; then reconsider E = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product ((N --> NAT) * Ok)))) as Function of {[1,0,0],[0,0,0]},(Funcs ((product ((N --> NAT) * Ok)),(product ((N --> NAT) * Ok)))) by A12, FUNCT_2:def_1, RELSET_1:4; set V = N --> NAT; set M = AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #); take AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #) ; ::_thesis: ( the carrier of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #) = {0} & the ZeroF of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #) = 0 & the InstructionsF of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #) = {[0,0,0],[1,0,0]} & the Object-Kind of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #) = 0 .--> 0 & the ValuesF of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #) = N --> NAT & ex f being Function of (product (the_Values_of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #))),(product (the_Values_of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #))) st ( ( for s being Element of product (the_Values_of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #)) holds f . s = s +* (0 .--> (succ (s . 0))) ) & the Execution of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #) = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product (the_Values_of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #))))) ) ) thus the carrier of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #) = {0} ; ::_thesis: ( the ZeroF of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #) = 0 & the InstructionsF of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #) = {[0,0,0],[1,0,0]} & the Object-Kind of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #) = 0 .--> 0 & the ValuesF of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #) = N --> NAT & ex f being Function of (product (the_Values_of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #))),(product (the_Values_of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #))) st ( ( for s being Element of product (the_Values_of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #)) holds f . s = s +* (0 .--> (succ (s . 0))) ) & the Execution of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #) = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product (the_Values_of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #))))) ) ) thus the ZeroF of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #) = 0 ; ::_thesis: ( the InstructionsF of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #) = {[0,0,0],[1,0,0]} & the Object-Kind of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #) = 0 .--> 0 & the ValuesF of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #) = N --> NAT & ex f being Function of (product (the_Values_of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #))),(product (the_Values_of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #))) st ( ( for s being Element of product (the_Values_of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #)) holds f . s = s +* (0 .--> (succ (s . 0))) ) & the Execution of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #) = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product (the_Values_of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #))))) ) ) thus the InstructionsF of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #) = {[0,0,0],[1,0,0]} ; ::_thesis: ( the Object-Kind of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #) = 0 .--> 0 & the ValuesF of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #) = N --> NAT & ex f being Function of (product (the_Values_of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #))),(product (the_Values_of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #))) st ( ( for s being Element of product (the_Values_of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #)) holds f . s = s +* (0 .--> (succ (s . 0))) ) & the Execution of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #) = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product (the_Values_of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #))))) ) ) thus the Object-Kind of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #) = 0 .--> 0 ; ::_thesis: ( the ValuesF of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #) = N --> NAT & ex f being Function of (product (the_Values_of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #))),(product (the_Values_of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #))) st ( ( for s being Element of product (the_Values_of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #)) holds f . s = s +* (0 .--> (succ (s . 0))) ) & the Execution of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #) = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product (the_Values_of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #))))) ) ) thus the ValuesF of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #) = N --> NAT ; ::_thesis: ex f being Function of (product (the_Values_of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #))),(product (the_Values_of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #))) st ( ( for s being Element of product (the_Values_of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #)) holds f . s = s +* (0 .--> (succ (s . 0))) ) & the Execution of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #) = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product (the_Values_of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #))))) ) reconsider f = f as Function of (product (the_Values_of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #))),(product (the_Values_of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #))) ; take f ; ::_thesis: ( ( for s being Element of product (the_Values_of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #)) holds f . s = s +* (0 .--> (succ (s . 0))) ) & the Execution of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #) = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product (the_Values_of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #))))) ) thus for s being Element of product (the_Values_of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #)) holds f . s = s +* (0 .--> (succ (s . 0))) by A11; ::_thesis: the Execution of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #) = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product (the_Values_of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #))))) thus the Execution of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #) = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product (the_Values_of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #))))) ; ::_thesis: verum end; uniqueness for b1, b2 being strict AMI-Struct over N st the carrier of b1 = {0} & the ZeroF of b1 = 0 & the InstructionsF of b1 = {[0,0,0],[1,0,0]} & the Object-Kind of b1 = 0 .--> 0 & the ValuesF of b1 = N --> NAT & ex f being Function of (product (the_Values_of b1)),(product (the_Values_of b1)) st ( ( for s being Element of product (the_Values_of b1) holds f . s = s +* (0 .--> (succ (s . 0))) ) & the Execution of b1 = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product (the_Values_of b1)))) ) & the carrier of b2 = {0} & the ZeroF of b2 = 0 & the InstructionsF of b2 = {[0,0,0],[1,0,0]} & the Object-Kind of b2 = 0 .--> 0 & the ValuesF of b2 = N --> NAT & ex f being Function of (product (the_Values_of b2)),(product (the_Values_of b2)) st ( ( for s being Element of product (the_Values_of b2) holds f . s = s +* (0 .--> (succ (s . 0))) ) & the Execution of b2 = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product (the_Values_of b2)))) ) holds b1 = b2 proof let it1, it2 be strict AMI-Struct over N; ::_thesis: ( the carrier of it1 = {0} & the ZeroF of it1 = 0 & the InstructionsF of it1 = {[0,0,0],[1,0,0]} & the Object-Kind of it1 = 0 .--> 0 & the ValuesF of it1 = N --> NAT & ex f being Function of (product (the_Values_of it1)),(product (the_Values_of it1)) st ( ( for s being Element of product (the_Values_of it1) holds f . s = s +* (0 .--> (succ (s . 0))) ) & the Execution of it1 = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product (the_Values_of it1)))) ) & the carrier of it2 = {0} & the ZeroF of it2 = 0 & the InstructionsF of it2 = {[0,0,0],[1,0,0]} & the Object-Kind of it2 = 0 .--> 0 & the ValuesF of it2 = N --> NAT & ex f being Function of (product (the_Values_of it2)),(product (the_Values_of it2)) st ( ( for s being Element of product (the_Values_of it2) holds f . s = s +* (0 .--> (succ (s . 0))) ) & the Execution of it2 = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product (the_Values_of it2)))) ) implies it1 = it2 ) assume that A15: ( the carrier of it1 = {0} & the ZeroF of it1 = 0 & the InstructionsF of it1 = {[0,0,0],[1,0,0]} ) and A16: the Object-Kind of it1 = 0 .--> 0 and A17: the ValuesF of it1 = N --> NAT ; ::_thesis: ( for f being Function of (product (the_Values_of it1)),(product (the_Values_of it1)) holds ( ex s being Element of product (the_Values_of it1) st not f . s = s +* (0 .--> (succ (s . 0))) or not the Execution of it1 = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product (the_Values_of it1)))) ) or not the carrier of it2 = {0} or not the ZeroF of it2 = 0 or not the InstructionsF of it2 = {[0,0,0],[1,0,0]} or not the Object-Kind of it2 = 0 .--> 0 or not the ValuesF of it2 = N --> NAT or for f being Function of (product (the_Values_of it2)),(product (the_Values_of it2)) holds ( ex s being Element of product (the_Values_of it2) st not f . s = s +* (0 .--> (succ (s . 0))) or not the Execution of it2 = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product (the_Values_of it2)))) ) or it1 = it2 ) given f1 being Function of (product (the_Values_of it1)),(product (the_Values_of it1)) such that A18: for s being Element of product (the_Values_of it1) holds f1 . s = s +* (0 .--> (succ (s . 0))) and A19: the Execution of it1 = ([1,0,0] .--> f1) +* ([0,0,0] .--> (id (product (the_Values_of it1)))) ; ::_thesis: ( not the carrier of it2 = {0} or not the ZeroF of it2 = 0 or not the InstructionsF of it2 = {[0,0,0],[1,0,0]} or not the Object-Kind of it2 = 0 .--> 0 or not the ValuesF of it2 = N --> NAT or for f being Function of (product (the_Values_of it2)),(product (the_Values_of it2)) holds ( ex s being Element of product (the_Values_of it2) st not f . s = s +* (0 .--> (succ (s . 0))) or not the Execution of it2 = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product (the_Values_of it2)))) ) or it1 = it2 ) assume that A20: ( the carrier of it2 = {0} & the ZeroF of it2 = 0 & the InstructionsF of it2 = {[0,0,0],[1,0,0]} ) and A21: the Object-Kind of it2 = 0 .--> 0 and A22: the ValuesF of it2 = N --> NAT ; ::_thesis: ( for f being Function of (product (the_Values_of it2)),(product (the_Values_of it2)) holds ( ex s being Element of product (the_Values_of it2) st not f . s = s +* (0 .--> (succ (s . 0))) or not the Execution of it2 = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product (the_Values_of it2)))) ) or it1 = it2 ) given f2 being Function of (product (the_Values_of it2)),(product (the_Values_of it2)) such that A23: for s being Element of product (the_Values_of it2) holds f2 . s = s +* (0 .--> (succ (s . 0))) and A24: the Execution of it2 = ([1,0,0] .--> f2) +* ([0,0,0] .--> (id (product (the_Values_of it2)))) ; ::_thesis: it1 = it2 A25: the_Values_of it1 = the_Values_of it2 by A16, A17, A21, A22; now__::_thesis:_for_c_being_Element_of_product_(the_Values_of_it1)_holds_f1_._c_=_f2_._c let c be Element of product (the_Values_of it1); ::_thesis: f1 . c = f2 . c thus f1 . c = c +* (0 .--> (succ (c . 0))) by A18 .= f2 . c by A23, A25 ; ::_thesis: verum end; hence it1 = it2 by A15, A16, A19, A20, A21, A24, A17, A22, FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def7 defines STC AMISTD_1:def_7_:_ for N being with_zero set for b2 being strict AMI-Struct over N holds ( b2 = STC N iff ( the carrier of b2 = {0} & the ZeroF of b2 = 0 & the InstructionsF of b2 = {[0,0,0],[1,0,0]} & the Object-Kind of b2 = 0 .--> 0 & the ValuesF of b2 = N --> NAT & ex f being Function of (product (the_Values_of b2)),(product (the_Values_of b2)) st ( ( for s being Element of product (the_Values_of b2) holds f . s = s +* (0 .--> (succ (s . 0))) ) & the Execution of b2 = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product (the_Values_of b2)))) ) ) ); registration let N be with_zero set ; cluster STC N -> non empty finite strict ; coherence ( STC N is finite & not STC N is empty ) by Def7; end; registration let N be with_zero set ; cluster STC N -> with_non-empty_values strict ; coherence STC N is with_non-empty_values proof let n be set ; :: according to MEMSTR_0:def_3,FUNCT_1:def_9 ::_thesis: ( not n in dom (the_Values_of (STC N)) or not (the_Values_of (STC N)) . n is empty ) set S = STC N; set F = the_Values_of (STC N); assume A1: n in dom (the_Values_of (STC N)) ; ::_thesis: not (the_Values_of (STC N)) . n is empty then A2: the Object-Kind of (STC N) . n in dom the ValuesF of (STC N) by FUNCT_1:11; A3: the ValuesF of (STC N) = N --> NAT by Def7; A4: the Object-Kind of (STC N) . n in N by A2; (the_Values_of (STC N)) . n = the ValuesF of (STC N) . ( the Object-Kind of (STC N) . n) by A1, FUNCT_1:12 .= NAT by A4, A3, FUNCOP_1:7 ; hence not (the_Values_of (STC N)) . n is empty ; ::_thesis: verum end; end; registration let N be with_zero set ; cluster STC N -> IC-Ins-separated strict ; coherence STC N is IC-Ins-separated proof set IT = STC N; set Ok = the_Values_of (STC N); A1: 0 in {0} by TARSKI:def_1; A2: the_Values_of (STC N) = the ValuesF of (STC N) * the Object-Kind of (STC N) .= the ValuesF of (STC N) * (0 .--> 0) by Def7 .= (N --> NAT) * (0 .--> 0) by Def7 ; 0 in N by MEASURE6:def_2; then (the_Values_of (STC N)) . 0 = (0 .--> NAT) . 0 by A2, FUNCOP_1:89 .= NAT by A1, FUNCOP_1:7 ; then Values (IC ) = NAT by Def7; hence STC N is IC-Ins-separated by MEMSTR_0:def_6; ::_thesis: verum end; end; Lm3: for N being with_zero set for i being Instruction of (STC N) for s being State of (STC N) st InsCode i = 1 holds (Exec (i,s)) . (IC ) = succ (IC s) proof let N be with_zero set ; ::_thesis: for i being Instruction of (STC N) for s being State of (STC N) st InsCode i = 1 holds (Exec (i,s)) . (IC ) = succ (IC s) let i be Instruction of (STC N); ::_thesis: for s being State of (STC N) st InsCode i = 1 holds (Exec (i,s)) . (IC ) = succ (IC s) let s be State of (STC N); ::_thesis: ( InsCode i = 1 implies (Exec (i,s)) . (IC ) = succ (IC s) ) set M = STC N; assume A1: InsCode i = 1 ; ::_thesis: (Exec (i,s)) . (IC ) = succ (IC s) A2: now__::_thesis:_not_i_in_{[0,0,0]} assume i in {[0,0,0]} ; ::_thesis: contradiction then i = [0,0,0] by TARSKI:def_1; hence contradiction by A1, RECDEF_2:def_1; ::_thesis: verum end; the InstructionsF of (STC N) = {[1,0,0],[0,0,0]} by Def7; then ( i = [1,0,0] or i = [0,0,0] ) by TARSKI:def_2; then A3: i in {[1,0,0]} by A1, RECDEF_2:def_1, TARSKI:def_1; A4: 0 in {0} by TARSKI:def_1; then A5: 0 in dom (0 .--> (succ (s . 0))) by FUNCOP_1:13; consider f being Function of (product (the_Values_of (STC N))),(product (the_Values_of (STC N))) such that A6: for s being Element of product (the_Values_of (STC N)) holds f . s = s +* (0 .--> (succ (s . 0))) and A7: the Execution of (STC N) = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product (the_Values_of (STC N))))) by Def7; A8: for s being State of (STC N) holds f . s = s +* (0 .--> (succ (s . 0))) proof let s be State of (STC N); ::_thesis: f . s = s +* (0 .--> (succ (s . 0))) reconsider s = s as Element of product (the_Values_of (STC N)) by CARD_3:107; f . s = s +* (0 .--> (succ (s . 0))) by A6; hence f . s = s +* (0 .--> (succ (s . 0))) ; ::_thesis: verum end; A9: the ZeroF of (STC N) = 0 by Def7; dom ([0,0,0] .--> (id (product (the_Values_of (STC N))))) = {[0,0,0]} by FUNCOP_1:13; then the Execution of (STC N) . i = ([1,0,0] .--> f) . i by A7, A2, FUNCT_4:11 .= f by A3, FUNCOP_1:7 ; hence (Exec (i,s)) . (IC ) = (s +* (0 .--> (succ (s . 0)))) . 0 by A9, A8 .= (0 .--> (succ (s . 0))) . 0 by A5, FUNCT_4:13 .= succ (IC s) by A9, A4, FUNCOP_1:7 ; ::_thesis: verum end; theorem Th4: :: AMISTD_1:4 for N being with_zero set for i being Instruction of (STC N) st InsCode i = 0 holds i is halting proof let N be with_zero set ; ::_thesis: for i being Instruction of (STC N) st InsCode i = 0 holds i is halting let i be Instruction of (STC N); ::_thesis: ( InsCode i = 0 implies i is halting ) set M = STC N; the InstructionsF of (STC N) = {[1,0,0],[0,0,0]} by Def7; then A1: ( i = [1,0,0] or i = [0,0,0] ) by TARSKI:def_2; assume InsCode i = 0 ; ::_thesis: i is halting then A2: i in {[0,0,0]} by A1, RECDEF_2:def_1, TARSKI:def_1; let s be State of (STC N); :: according to EXTPRO_1:def_3 ::_thesis: Exec (i,s) = s reconsider s = s as Element of product (the_Values_of (STC N)) by CARD_3:107; ( ex f being Function of (product (the_Values_of (STC N))),(product (the_Values_of (STC N))) st ( ( for s being Element of product (the_Values_of (STC N)) holds f . s = s +* (0 .--> (succ (s . 0))) ) & the Execution of (STC N) = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product (the_Values_of (STC N))))) ) & dom ([0,0,0] .--> (id (product (the_Values_of (STC N))))) = {[0,0,0]} ) by Def7, FUNCOP_1:13; then the Execution of (STC N) . i = ({[0,0,0]} --> (id (product (the_Values_of (STC N))))) . i by A2, FUNCT_4:13 .= id (product (the_Values_of (STC N))) by A2, FUNCOP_1:7 ; then ( the Execution of (STC N) . i) . s = s by FUNCT_1:18; hence Exec (i,s) = s ; ::_thesis: verum end; theorem :: AMISTD_1:5 for N being with_zero set for i being Instruction of (STC N) st InsCode i = 1 holds not i is halting proof let N be with_zero set ; ::_thesis: for i being Instruction of (STC N) st InsCode i = 1 holds not i is halting let i be Instruction of (STC N); ::_thesis: ( InsCode i = 1 implies not i is halting ) set M = STC N; set s = the State of (STC N); assume InsCode i = 1 ; ::_thesis: not i is halting then A1: (Exec (i, the State of (STC N))) . (IC ) = succ (IC the State of (STC N)) by Lm3; assume for s being State of (STC N) holds Exec (i,s) = s ; :: according to EXTPRO_1:def_3 ::_thesis: contradiction then (Exec (i, the State of (STC N))) . (IC ) = IC the State of (STC N) ; hence contradiction by A1; ::_thesis: verum end; theorem Th6: :: AMISTD_1:6 for N being with_zero set for i being Element of the InstructionsF of (STC N) holds ( InsCode i = 1 or InsCode i = 0 ) proof let N be with_zero set ; ::_thesis: for i being Element of the InstructionsF of (STC N) holds ( InsCode i = 1 or InsCode i = 0 ) let i be Element of the InstructionsF of (STC N); ::_thesis: ( InsCode i = 1 or InsCode i = 0 ) the InstructionsF of (STC N) = {[1,0,0],[0,0,0]} by Def7; then ( i = [1,0,0] or i = [0,0,0] ) by TARSKI:def_2; hence ( InsCode i = 1 or InsCode i = 0 ) by RECDEF_2:def_1; ::_thesis: verum end; theorem :: AMISTD_1:7 for N being with_zero set for i being Instruction of (STC N) holds i is jump-only proof let N be with_zero set ; ::_thesis: for i being Instruction of (STC N) holds i is jump-only let i be Instruction of (STC N); ::_thesis: i is jump-only set M = STC N; let s be State of (STC N); :: according to AMISTD_1:def_1,AMISTD_1:def_2 ::_thesis: for o being Object of (STC N) for I being Instruction of (STC N) st InsCode I = InsCode i & o in Data-Locations holds (Exec (I,s)) . o = s . o let o be Object of (STC N); ::_thesis: for I being Instruction of (STC N) st InsCode I = InsCode i & o in Data-Locations holds (Exec (I,s)) . o = s . o let I be Instruction of (STC N); ::_thesis: ( InsCode I = InsCode i & o in Data-Locations implies (Exec (I,s)) . o = s . o ) assume that InsCode I = InsCode i and A1: o in Data-Locations ; ::_thesis: (Exec (I,s)) . o = s . o A2: the ZeroF of (STC N) = 0 by Def7; Data-Locations = {0} \ {0} by A2, Def7 .= {} by XBOOLE_1:37 ; hence (Exec (I,s)) . o = s . o by A1; ::_thesis: verum end; registration let N be with_zero set ; cluster -> ins-loc-free for Element of the InstructionsF of (STC N); coherence for b1 being Instruction of (STC N) holds b1 is ins-loc-free proof let I be Instruction of (STC N); ::_thesis: I is ins-loc-free I in the InstructionsF of (STC N) ; then I in {[0,0,0],[1,0,0]} by Def7; then ( I = [0,0,0] or I = [1,0,0] ) by TARSKI:def_2; hence JumpPart I is empty by RECDEF_2:def_2; :: according to COMPOS_0:def_8 ::_thesis: verum end; end; Lm4: for z being Nat for N being with_zero set for l being Element of NAT for i being Element of the InstructionsF of (STC N) st l = z & InsCode i = 1 holds NIC (i,l) = {(z + 1)} proof let z be Nat; ::_thesis: for N being with_zero set for l being Element of NAT for i being Element of the InstructionsF of (STC N) st l = z & InsCode i = 1 holds NIC (i,l) = {(z + 1)} let N be with_zero set ; ::_thesis: for l being Element of NAT for i being Element of the InstructionsF of (STC N) st l = z & InsCode i = 1 holds NIC (i,l) = {(z + 1)} let l be Element of NAT ; ::_thesis: for i being Element of the InstructionsF of (STC N) st l = z & InsCode i = 1 holds NIC (i,l) = {(z + 1)} let i be Element of the InstructionsF of (STC N); ::_thesis: ( l = z & InsCode i = 1 implies NIC (i,l) = {(z + 1)} ) assume that A1: l = z and A2: InsCode i = 1 ; ::_thesis: NIC (i,l) = {(z + 1)} set M = STC N; set F = { (IC (Exec (i,ss))) where ss is Element of product (the_Values_of (STC N)) : IC ss = l } ; now__::_thesis:_for_y_being_set_holds_ (_(_y_in__{__(IC_(Exec_(i,ss)))_where_ss_is_Element_of_product_(the_Values_of_(STC_N))_:_IC_ss_=_l__}__implies_y_in_{(z_+_1)}_)_&_(_y_in_{(z_+_1)}_implies_y_in__{__(IC_(Exec_(i,ss)))_where_ss_is_Element_of_product_(the_Values_of_(STC_N))_:_IC_ss_=_l__}__)_) set f = NAT --> i; set w = the State of (STC N); reconsider l9 = l as Element of Values (IC ) by MEMSTR_0:def_6; set u = (IC ) .--> l9; A3: dom ((IC ) .--> l9) = {(IC )} by FUNCOP_1:13; let y be set ; ::_thesis: ( ( y in { (IC (Exec (i,ss))) where ss is Element of product (the_Values_of (STC N)) : IC ss = l } implies y in {(z + 1)} ) & ( y in {(z + 1)} implies y in { (IC (Exec (i,ss))) where ss is Element of product (the_Values_of (STC N)) : IC ss = l } ) ) reconsider t = the State of (STC N) +* ((IC ) .--> l9) as Element of product (the_Values_of (STC N)) by CARD_3:107; A4: (NAT --> i) /. l = i by FUNCOP_1:7; hereby ::_thesis: ( y in {(z + 1)} implies y in { (IC (Exec (i,ss))) where ss is Element of product (the_Values_of (STC N)) : IC ss = l } ) assume y in { (IC (Exec (i,ss))) where ss is Element of product (the_Values_of (STC N)) : IC ss = l } ; ::_thesis: y in {(z + 1)} then ex s being Element of product (the_Values_of (STC N)) st ( y = IC (Exec (i,s)) & IC s = l ) ; then y = succ z by A1, A2, Lm3 .= z + 1 ; hence y in {(z + 1)} by TARSKI:def_1; ::_thesis: verum end; assume y in {(z + 1)} ; ::_thesis: y in { (IC (Exec (i,ss))) where ss is Element of product (the_Values_of (STC N)) : IC ss = l } then A5: y = succ z by TARSKI:def_1; IC in dom ((IC ) .--> l9) by A3, TARSKI:def_1; then A6: IC t = ((IC ) .--> l9) . (IC ) by FUNCT_4:13 .= z by A1, FUNCOP_1:72 ; then IC (Following ((NAT --> i),t)) = succ z by A1, A2, A4, Lm3; hence y in { (IC (Exec (i,ss))) where ss is Element of product (the_Values_of (STC N)) : IC ss = l } by A1, A5, A6, A4; ::_thesis: verum end; hence NIC (i,l) = {(z + 1)} by TARSKI:1; ::_thesis: verum end; Lm5: for N being with_zero set for i being Element of the InstructionsF of (STC N) holds JUMP i is empty proof let N be with_zero set ; ::_thesis: for i being Element of the InstructionsF of (STC N) holds JUMP i is empty let i be Element of the InstructionsF of (STC N); ::_thesis: JUMP i is empty percases ( InsCode i = 1 or InsCode i = 0 ) by Th6; supposeA1: InsCode i = 1 ; ::_thesis: JUMP i is empty reconsider l1 = 0 , l2 = 1 as Element of NAT ; set X = { (NIC (i,l)) where l is Element of NAT : verum } ; assume not JUMP i is empty ; ::_thesis: contradiction then consider x being set such that A2: x in meet { (NIC (i,l)) where l is Element of NAT : verum } by XBOOLE_0:def_1; NIC (i,l1) in { (NIC (i,l)) where l is Element of NAT : verum } ; then {(0 + 1)} in { (NIC (i,l)) where l is Element of NAT : verum } by A1, Lm4; then x in {1} by A2, SETFAM_1:def_1; then A3: x = 1 by TARSKI:def_1; NIC (i,l2) in { (NIC (i,l)) where l is Element of NAT : verum } ; then {(1 + 1)} in { (NIC (i,l)) where l is Element of NAT : verum } by A1, Lm4; then x in {2} by A2, SETFAM_1:def_1; hence contradiction by A3, TARSKI:def_1; ::_thesis: verum end; supposeA4: InsCode i = 0 ; ::_thesis: JUMP i is empty reconsider i = i as Instruction of (STC N) ; for l being Element of NAT holds NIC (i,l) = {l} by A4, Th2, Th4; hence JUMP i is empty by Th1; ::_thesis: verum end; end; end; theorem Th8: :: AMISTD_1:8 for z being Nat for N being with_zero set for l being Element of NAT st l = z holds SUCC (l,(STC N)) = {z,(z + 1)} proof let z be Nat; ::_thesis: for N being with_zero set for l being Element of NAT st l = z holds SUCC (l,(STC N)) = {z,(z + 1)} let N be with_zero set ; ::_thesis: for l being Element of NAT st l = z holds SUCC (l,(STC N)) = {z,(z + 1)} let l be Element of NAT ; ::_thesis: ( l = z implies SUCC (l,(STC N)) = {z,(z + 1)} ) assume A1: l = z ; ::_thesis: SUCC (l,(STC N)) = {z,(z + 1)} set M = STC N; set K = { ((NIC (i,l)) \ (JUMP i)) where i is Element of the InstructionsF of (STC N) : verum } ; now__::_thesis:_for_y_being_set_holds_ (_(_y_in__{__((NIC_(i,l))_\_(JUMP_i))_where_i_is_Element_of_the_InstructionsF_of_(STC_N)_:_verum__}__implies_y_in_{{z},{(z_+_1)}}_)_&_(_y_in_{{z},{(z_+_1)}}_implies_y_in__{__((NIC_(i,l))_\_(JUMP_i))_where_i_is_Element_of_the_InstructionsF_of_(STC_N)_:_verum__}__)_) let y be set ; ::_thesis: ( ( y in { ((NIC (i,l)) \ (JUMP i)) where i is Element of the InstructionsF of (STC N) : verum } implies y in {{z},{(z + 1)}} ) & ( y in {{z},{(z + 1)}} implies b1 in { ((NIC (b2,l)) \ (JUMP b2)) where i is Element of the InstructionsF of (STC N) : verum } ) ) hereby ::_thesis: ( y in {{z},{(z + 1)}} implies b1 in { ((NIC (b2,l)) \ (JUMP b2)) where i is Element of the InstructionsF of (STC N) : verum } ) assume y in { ((NIC (i,l)) \ (JUMP i)) where i is Element of the InstructionsF of (STC N) : verum } ; ::_thesis: y in {{z},{(z + 1)}} then consider ii being Element of the InstructionsF of (STC N) such that A2: y = (NIC (ii,l)) \ (JUMP ii) and verum ; reconsider ii = ii as Instruction of (STC N) ; now__::_thesis:_y_in_{{z},{(z_+_1)}} percases ( InsCode ii = 1 or InsCode ii = 0 ) by Th6; supposeA3: InsCode ii = 1 ; ::_thesis: y in {{z},{(z + 1)}} JUMP ii = {} by Lm5; then y = {(z + 1)} by A1, A2, A3, Lm4; hence y in {{z},{(z + 1)}} by TARSKI:def_2; ::_thesis: verum end; supposeA4: InsCode ii = 0 ; ::_thesis: y in {{z},{(z + 1)}} JUMP ii = {} by Lm5; then y = {z} by A1, A2, A4, Th2, Th4; hence y in {{z},{(z + 1)}} by TARSKI:def_2; ::_thesis: verum end; end; end; hence y in {{z},{(z + 1)}} ; ::_thesis: verum end; assume A5: y in {{z},{(z + 1)}} ; ::_thesis: b1 in { ((NIC (b2,l)) \ (JUMP b2)) where i is Element of the InstructionsF of (STC N) : verum } percases ( y = {z} or y = {(z + 1)} ) by A5, TARSKI:def_2; supposeA6: y = {z} ; ::_thesis: b1 in { ((NIC (b2,l)) \ (JUMP b2)) where i is Element of the InstructionsF of (STC N) : verum } halt (STC N) = [0,{},{}] ; then reconsider i = [0,0,0] as Instruction of (STC N) ; ( JUMP i = {} & InsCode i = 0 ) by Lm5, RECDEF_2:def_1; then (NIC (i,l)) \ (JUMP i) = y by A1, A6, Th2, Th4; hence y in { ((NIC (i,l)) \ (JUMP i)) where i is Element of the InstructionsF of (STC N) : verum } ; ::_thesis: verum end; supposeA7: y = {(z + 1)} ; ::_thesis: b1 in { ((NIC (b2,l)) \ (JUMP b2)) where i is Element of the InstructionsF of (STC N) : verum } set i = [1,0,0]; [1,0,0] in {[1,0,0],[0,0,0]} by TARSKI:def_2; then reconsider i = [1,0,0] as Instruction of (STC N) by Def7; ( JUMP i = {} & InsCode i = 1 ) by Lm5, RECDEF_2:def_1; then (NIC (i,l)) \ (JUMP i) = y by A1, A7, Lm4; hence y in { ((NIC (i,l)) \ (JUMP i)) where i is Element of the InstructionsF of (STC N) : verum } ; ::_thesis: verum end; end; end; then { ((NIC (i,l)) \ (JUMP i)) where i is Element of the InstructionsF of (STC N) : verum } = {{z},{(z + 1)}} by TARSKI:1; hence SUCC (l,(STC N)) = {z,(z + 1)} by ZFMISC_1:26; ::_thesis: verum end; registration let N be with_zero set ; cluster STC N -> strict standard ; coherence STC N is standard proof set M = STC N; now__::_thesis:_for_k_being_Element_of_NAT_holds_ (_k_+_1_in_SUCC_(k,(STC_N))_&_(_for_j_being_Element_of_NAT_st_j_in_SUCC_(k,(STC_N))_holds_ k_<=_j_)_) let k be Element of NAT ; ::_thesis: ( k + 1 in SUCC (k,(STC N)) & ( for j being Element of NAT st j in SUCC (k,(STC N)) holds k <= j ) ) A1: SUCC (k,(STC N)) = {k,(k + 1)} by Th8; thus k + 1 in SUCC (k,(STC N)) by A1, TARSKI:def_2; ::_thesis: for j being Element of NAT st j in SUCC (k,(STC N)) holds k <= j let j be Element of NAT ; ::_thesis: ( j in SUCC (k,(STC N)) implies k <= j ) assume j in SUCC (k,(STC N)) ; ::_thesis: k <= j then ( j = k or j = k + 1 ) by A1, TARSKI:def_2; hence k <= j by NAT_1:11; ::_thesis: verum end; hence STC N is standard by Th3; ::_thesis: verum end; end; registration let N be with_zero set ; cluster STC N -> strict halting ; coherence STC N is halting proof set I = halt (STC N); InsCode (halt (STC N)) = 0 by RECDEF_2:def_1; hence halt (STC N) is halting by Th4; :: according to EXTPRO_1:def_4 ::_thesis: verum end; end; registration let N be with_zero set ; cluster non empty with_non-empty_values IC-Ins-separated halting 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 & b1 is halting ) proof take STC N ; ::_thesis: ( STC N is standard & STC N is halting ) thus ( STC N is standard & STC N is halting ) ; ::_thesis: verum end; end; theorem :: AMISTD_1:9 for N being with_zero set for i being Instruction of (STC N) for s being State of (STC N) st InsCode i = 1 holds (Exec (i,s)) . (IC ) = succ (IC s) by Lm3; theorem :: AMISTD_1:10 for N being with_zero set for l being Element of NAT for i being Element of the InstructionsF of (STC N) st InsCode i = 1 holds NIC (i,l) = {(succ l)} by Lm4; theorem :: AMISTD_1:11 for N being with_zero set for l being Element of NAT holds SUCC (l,(STC N)) = {l,(succ l)} by Th8; definition let N be with_zero set ; let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; let i be Instruction of S; attri is sequential means :: AMISTD_1:def 8 for s being State of S holds (Exec (i,s)) . (IC ) = succ (IC s); end; :: deftheorem defines sequential AMISTD_1:def_8_:_ for N being with_zero set for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N for i being Instruction of S holds ( i is sequential iff for s being State of S holds (Exec (i,s)) . (IC ) = succ (IC s) ); theorem Th12: :: AMISTD_1:12 for N being with_zero set for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N for il being Element of NAT for i being Instruction of S st i is sequential holds NIC (i,il) = {(succ il)} proof let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N for il being Element of NAT for i being Instruction of S st i is sequential holds NIC (i,il) = {(succ il)} let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; ::_thesis: for il being Element of NAT for i being Instruction of S st i is sequential holds NIC (i,il) = {(succ il)} let il be Element of NAT ; ::_thesis: for i being Instruction of S st i is sequential holds NIC (i,il) = {(succ il)} let i be Instruction of S; ::_thesis: ( i is sequential implies NIC (i,il) = {(succ il)} ) assume A1: for s being State of S holds (Exec (i,s)) . (IC ) = succ (IC s) ; :: according to AMISTD_1:def_8 ::_thesis: NIC (i,il) = {(succ il)} now__::_thesis:_for_x_being_set_holds_ (_x_in_{(succ_il)}_iff_x_in__{__(IC_(Exec_(i,ss)))_where_ss_is_Element_of_product_(the_Values_of_S)_:_IC_ss_=_il__}__) let x be set ; ::_thesis: ( x in {(succ il)} iff x in { (IC (Exec (i,ss))) where ss is Element of product (the_Values_of S) : IC ss = il } ) A2: now__::_thesis:_(_x_=_succ_il_implies_x_in__{__(IC_(Exec_(i,ss)))_where_ss_is_Element_of_product_(the_Values_of_S)_:_IC_ss_=_il__}__) reconsider il1 = il as Element of Values (IC ) by MEMSTR_0:def_6; set I = i; set t = the State of S; set P = the Instruction-Sequence of S; assume A3: x = succ il ; ::_thesis: x in { (IC (Exec (i,ss))) where ss is Element of product (the_Values_of S) : IC ss = il } reconsider u = the State of S +* ((IC ),il1) as Element of product (the_Values_of S) by CARD_3:107; il in NAT ; then A4: il in dom the Instruction-Sequence of S by PARTFUN1:def_2; A5: ( the Instruction-Sequence of S +* (il,i)) /. il = ( the Instruction-Sequence of S +* (il,i)) . il by PBOOLE:143 .= i by A4, FUNCT_7:31 ; IC in dom the State of S by MEMSTR_0:2; then A6: IC u = il by FUNCT_7:31; then IC (Following (( the Instruction-Sequence of S +* (il,i)),u)) = succ il by A1, A5; hence x in { (IC (Exec (i,ss))) where ss is Element of product (the_Values_of S) : IC ss = il } by A3, A6, A5; ::_thesis: verum end; now__::_thesis:_(_x_in__{__(IC_(Exec_(i,ss)))_where_ss_is_Element_of_product_(the_Values_of_S)_:_IC_ss_=_il__}__implies_x_=_succ_il_) assume x in { (IC (Exec (i,ss))) where ss is Element of product (the_Values_of S) : IC ss = il } ; ::_thesis: x = succ il then ex s being Element of product (the_Values_of S) st ( x = IC (Exec (i,s)) & IC s = il ) ; hence x = succ il by A1; ::_thesis: verum end; hence ( x in {(succ il)} iff x in { (IC (Exec (i,ss))) where ss is Element of product (the_Values_of S) : IC ss = il } ) by A2, TARSKI:def_1; ::_thesis: verum end; hence NIC (i,il) = {(succ il)} by TARSKI:1; ::_thesis: verum end; registration let N be with_zero set ; let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; cluster sequential -> non halting for Element of the InstructionsF of S; coherence for b1 being Instruction of S st b1 is sequential holds not b1 is halting proof let i be Instruction of S; ::_thesis: ( i is sequential implies not i is halting ) assume A1: i is sequential ; ::_thesis: not i is halting set s = the State of S; NIC (i,(IC the State of S)) = {(succ (IC the State of S))} by A1, Th12; then NIC (i,(IC the State of S)) <> {(IC the State of S)} by ORDINAL1:9, ZFMISC_1:3; hence not i is halting by Th2; ::_thesis: verum end; cluster halting -> non sequential for Element of the InstructionsF of S; coherence for b1 being Instruction of S st b1 is halting holds not b1 is sequential ; end; theorem :: AMISTD_1:13 for N being with_zero set for T being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N for i being Instruction of T st not JUMP i is empty holds not i is sequential proof let N be with_zero set ; ::_thesis: for T being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N for i being Instruction of T st not JUMP i is empty holds not i is sequential let T be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; ::_thesis: for i being Instruction of T st not JUMP i is empty holds not i is sequential let i be Instruction of T; ::_thesis: ( not JUMP i is empty implies not i is sequential ) set X = { (NIC (i,l1)) where l1 is Element of NAT : verum } ; assume not JUMP i is empty ; ::_thesis: not i is sequential then consider l being set such that A1: l in JUMP i by XBOOLE_0:def_1; reconsider l = l as Element of NAT by A1; NIC (i,l) in { (NIC (i,l1)) where l1 is Element of NAT : verum } ; then l in NIC (i,l) by A1, SETFAM_1:def_1; then consider s being Element of product (the_Values_of T) such that A2: ( l = IC (Exec (i,s)) & IC s = l ) ; take s ; :: according to AMISTD_1:def_8 ::_thesis: not (Exec (i,s)) . (IC ) = succ (IC s) thus not (Exec (i,s)) . (IC ) = succ (IC s) by A2; ::_thesis: verum end; begin definition let N be with_zero set ; let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; let F be preProgram of S; attrF is really-closed means :Def9: :: AMISTD_1:def 9 for l being Element of NAT st l in dom F holds NIC ((F /. l),l) c= dom F; end; :: deftheorem Def9 defines really-closed AMISTD_1:def_9_:_ for N being with_zero set for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N for F being preProgram of S holds ( F is really-closed iff for l being Element of NAT st l in dom F holds NIC ((F /. l),l) c= dom F ); definition let N be with_zero set ; let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; let F be NAT -defined the InstructionsF of S -valued Function; attrF is paraclosed means :: AMISTD_1:def 10 for s being 0 -started State of S for P being Instruction-Sequence of S st F c= P holds for k being Element of NAT holds IC (Comput (P,s,k)) in dom F; end; :: deftheorem defines paraclosed AMISTD_1:def_10_:_ for N being with_zero set for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N for F being NAT -defined the InstructionsF of b2 -valued Function holds ( F is paraclosed iff for s being 0 -started State of S for P being Instruction-Sequence of S st F c= P holds for k being Element of NAT holds IC (Comput (P,s,k)) in dom F ); definition let N be with_zero set ; let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N; let F be NAT -defined the InstructionsF of S -valued Function; attrF is parahalting means :: AMISTD_1:def 11 for s being 0 -started State of S for P being Instruction-Sequence of S st F c= P holds P halts_on s; end; :: deftheorem defines parahalting AMISTD_1:def_11_:_ for N being with_zero set for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for F being NAT -defined the InstructionsF of b2 -valued Function holds ( F is parahalting iff for s being 0 -started State of S for P being Instruction-Sequence of S st F c= P holds P halts_on s ); theorem Th14: :: AMISTD_1:14 for N being with_zero set for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N for F being preProgram of S holds ( F is really-closed iff for s being State of S st IC s in dom F holds for k being Element of NAT holds IC (Comput (F,s,k)) in dom F ) proof let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N for F being preProgram of S holds ( F is really-closed iff for s being State of S st IC s in dom F holds for k being Element of NAT holds IC (Comput (F,s,k)) in dom F ) let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; ::_thesis: for F being preProgram of S holds ( F is really-closed iff for s being State of S st IC s in dom F holds for k being Element of NAT holds IC (Comput (F,s,k)) in dom F ) let F be preProgram of S; ::_thesis: ( F is really-closed iff for s being State of S st IC s in dom F holds for k being Element of NAT holds IC (Comput (F,s,k)) in dom F ) thus ( F is really-closed implies for s being State of S st IC s in dom F holds for k being Element of NAT holds IC (Comput (F,s,k)) in dom F ) ::_thesis: ( ( for s being State of S st IC s in dom F holds for k being Element of NAT holds IC (Comput (F,s,k)) in dom F ) implies F is really-closed ) proof assume A1: F is really-closed ; ::_thesis: for s being State of S st IC s in dom F holds for k being Element of NAT holds IC (Comput (F,s,k)) in dom F let s be State of S; ::_thesis: ( IC s in dom F implies for k being Element of NAT holds IC (Comput (F,s,k)) in dom F ) assume A2: IC s in dom F ; ::_thesis: for k being Element of NAT holds IC (Comput (F,s,k)) in dom F defpred S1[ Element of NAT ] means IC (Comput (F,s,$1)) in dom F; A3: now__::_thesis:_for_k_being_Element_of_NAT_st_S1[k]_holds_ S1[k_+_1] let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A4: S1[k] ; ::_thesis: S1[k + 1] reconsider t = Comput (F,s,k) as Element of product (the_Values_of S) by CARD_3:107; set l = IC (Comput (F,s,k)); A5: IC (Following (F,t)) in NIC ((F /. (IC (Comput (F,s,k)))),(IC (Comput (F,s,k)))) ; A6: Comput (F,s,(k + 1)) = Following (F,t) by EXTPRO_1:3; NIC ((F /. (IC (Comput (F,s,k)))),(IC (Comput (F,s,k)))) c= dom F by A1, A4, Def9; hence S1[k + 1] by A5, A6; ::_thesis: verum end; A7: S1[ 0 ] by A2; thus for k being Element of NAT holds S1[k] from NAT_1:sch_1(A7, A3); ::_thesis: verum end; assume A8: for s being State of S st IC s in dom F holds for k being Element of NAT holds IC (Comput (F,s,k)) in dom F ; ::_thesis: F is really-closed let l be Element of NAT ; :: according to AMISTD_1:def_9 ::_thesis: ( l in dom F implies NIC ((F /. l),l) c= dom F ) assume A9: l in dom F ; ::_thesis: NIC ((F /. l),l) c= dom F let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in NIC ((F /. l),l) or x in dom F ) assume x in NIC ((F /. l),l) ; ::_thesis: x in dom F then consider ss being Element of product (the_Values_of S) such that A10: x = IC (Exec ((F /. l),ss)) and A11: IC ss = l ; reconsider ss = ss as State of S ; IC (Comput (F,ss,(0 + 1))) = IC (Following (F,(Comput (F,ss,0)))) by EXTPRO_1:3 .= IC (Following (F,ss)) .= IC (Exec ((F /. (IC ss)),ss)) ; hence x in dom F by A10, A11, A8, A9; ::_thesis: verum end; Lm6: for N being with_zero set for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N for F being preProgram of S holds ( F is really-closed iff for s being State of S st IC s in dom F holds for P being Instruction-Sequence of S st F c= P holds for k being Element of NAT holds IC (Comput (P,s,k)) in dom F ) proof let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N for F being preProgram of S holds ( F is really-closed iff for s being State of S st IC s in dom F holds for P being Instruction-Sequence of S st F c= P holds for k being Element of NAT holds IC (Comput (P,s,k)) in dom F ) let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; ::_thesis: for F being preProgram of S holds ( F is really-closed iff for s being State of S st IC s in dom F holds for P being Instruction-Sequence of S st F c= P holds for k being Element of NAT holds IC (Comput (P,s,k)) in dom F ) let F be preProgram of S; ::_thesis: ( F is really-closed iff for s being State of S st IC s in dom F holds for P being Instruction-Sequence of S st F c= P holds for k being Element of NAT holds IC (Comput (P,s,k)) in dom F ) thus ( F is really-closed implies for s being State of S st IC s in dom F holds for P being Instruction-Sequence of S st F c= P holds for k being Element of NAT holds IC (Comput (P,s,k)) in dom F ) ::_thesis: ( ( for s being State of S st IC s in dom F holds for P being Instruction-Sequence of S st F c= P holds for k being Element of NAT holds IC (Comput (P,s,k)) in dom F ) implies F is really-closed ) proof assume A1: F is really-closed ; ::_thesis: for s being State of S st IC s in dom F holds for P being Instruction-Sequence of S st F c= P holds for k being Element of NAT holds IC (Comput (P,s,k)) in dom F let s be State of S; ::_thesis: ( IC s in dom F implies for P being Instruction-Sequence of S st F c= P holds for k being Element of NAT holds IC (Comput (P,s,k)) in dom F ) assume A2: IC s in dom F ; ::_thesis: for P being Instruction-Sequence of S st F c= P holds for k being Element of NAT holds IC (Comput (P,s,k)) in dom F let P be Instruction-Sequence of S; ::_thesis: ( F c= P implies for k being Element of NAT holds IC (Comput (P,s,k)) in dom F ) assume A3: F c= P ; ::_thesis: for k being Element of NAT holds IC (Comput (P,s,k)) in dom F defpred S1[ Element of NAT ] means IC (Comput (P,s,$1)) in dom F; A4: now__::_thesis:_for_k_being_Element_of_NAT_st_S1[k]_holds_ S1[k_+_1] let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A5: S1[k] ; ::_thesis: S1[k + 1] reconsider t = Comput (P,s,k) as Element of product (the_Values_of S) by CARD_3:107; set l = IC (Comput (P,s,k)); A6: IC (Following (P,t)) in NIC ((P /. (IC (Comput (P,s,k)))),(IC (Comput (P,s,k)))) ; A7: Comput (P,s,(k + 1)) = Following (P,t) by EXTPRO_1:3; P /. (IC (Comput (P,s,k))) = F /. (IC (Comput (P,s,k))) by A5, A3, PARTFUN2:61; then NIC ((P /. (IC (Comput (P,s,k)))),(IC (Comput (P,s,k)))) c= dom F by A1, A5, Def9; hence S1[k + 1] by A6, A7; ::_thesis: verum end; A8: S1[ 0 ] by A2; thus for k being Element of NAT holds S1[k] from NAT_1:sch_1(A8, A4); ::_thesis: verum end; assume A9: for s being State of S st IC s in dom F holds for P being Instruction-Sequence of S st F c= P holds for k being Element of NAT holds IC (Comput (P,s,k)) in dom F ; ::_thesis: F is really-closed for s being State of S st IC s in dom F holds for k being Element of NAT holds IC (Comput (F,s,k)) in dom F proof let s be State of S; ::_thesis: ( IC s in dom F implies for k being Element of NAT holds IC (Comput (F,s,k)) in dom F ) assume A10: IC s in dom F ; ::_thesis: for k being Element of NAT holds IC (Comput (F,s,k)) in dom F consider P being Instruction-Sequence of S such that A11: F c= P by PBOOLE:145; let k be Element of NAT ; ::_thesis: IC (Comput (F,s,k)) in dom F A12: IC (Comput (P,s,k)) in dom F by A9, A10, A11; defpred S1[ Nat] means Comput (P,s,$1) = Comput (F,s,$1); A13: S1[ 0 ] ; A14: for k being Nat st S1[k] holds S1[k + 1] proof let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A15: S1[k] ; ::_thesis: S1[k + 1] reconsider kk = k as Element of NAT by ORDINAL1:def_12; A16: IC (Comput (P,s,kk)) in dom F by A9, A10, A11; Comput (P,s,(k + 1)) = Following (P,(Comput (F,s,k))) by A15, EXTPRO_1:3 .= Following (F,(Comput (F,s,k))) by A16, A11, A15, PARTFUN2:61 .= Comput (F,s,(k + 1)) by EXTPRO_1:3 ; hence S1[k + 1] ; ::_thesis: verum end; for k being Nat holds S1[k] from NAT_1:sch_2(A13, A14); hence IC (Comput (F,s,k)) in dom F by A12; ::_thesis: verum end; hence F is really-closed by Th14; ::_thesis: verum end; theorem Th15: :: AMISTD_1:15 for N being with_zero set for S being non empty with_non-empty_values IC-Ins-separated standard AMI-Struct over N for F being NAT -defined the InstructionsF of b2 -valued finite Function st F is really-closed & 0 in dom F holds F is paraclosed proof let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated standard AMI-Struct over N for F being NAT -defined the InstructionsF of b1 -valued finite Function st F is really-closed & 0 in dom F holds F is paraclosed let S be non empty with_non-empty_values IC-Ins-separated standard AMI-Struct over N; ::_thesis: for F being NAT -defined the InstructionsF of S -valued finite Function st F is really-closed & 0 in dom F holds F is paraclosed let F be NAT -defined the InstructionsF of S -valued finite Function; ::_thesis: ( F is really-closed & 0 in dom F implies F is paraclosed ) assume A1: F is really-closed ; ::_thesis: ( not 0 in dom F or F is paraclosed ) assume A2: 0 in dom F ; ::_thesis: F is paraclosed let s be 0 -started State of S; :: according to AMISTD_1:def_10 ::_thesis: for P being Instruction-Sequence of S st F c= P holds for k being Element of NAT holds IC (Comput (P,s,k)) in dom F A3: IC s = 0 by MEMSTR_0:def_11; let P be Instruction-Sequence of S; ::_thesis: ( F c= P implies for k being Element of NAT holds IC (Comput (P,s,k)) in dom F ) assume A4: F c= P ; ::_thesis: for k being Element of NAT holds IC (Comput (P,s,k)) in dom F let k be Element of NAT ; ::_thesis: IC (Comput (P,s,k)) in dom F thus IC (Comput (P,s,k)) in dom F by A1, A3, A4, Lm6, A2; ::_thesis: verum end; theorem Th16: :: AMISTD_1:16 for N being with_zero set for S being non empty with_non-empty_values IC-Ins-separated halting standard AMI-Struct over N holds 0 .--> (halt S) is really-closed proof let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated halting standard AMI-Struct over N holds 0 .--> (halt S) is really-closed let S be non empty with_non-empty_values IC-Ins-separated halting standard AMI-Struct over N; ::_thesis: 0 .--> (halt S) is really-closed reconsider F = 0 .--> (halt S) as NAT -defined the InstructionsF of S -valued finite Function ; let l be Element of NAT ; :: according to AMISTD_1:def_9 ::_thesis: ( l in dom (0 .--> (halt S)) implies NIC (((0 .--> (halt S)) /. l),l) c= dom (0 .--> (halt S)) ) assume A1: l in dom (0 .--> (halt S)) ; ::_thesis: NIC (((0 .--> (halt S)) /. l),l) c= dom (0 .--> (halt S)) A2: dom F = {0} by FUNCOP_1:13; A3: l = 0 by A1, TARSKI:def_1; F /. l = F . l by A1, PARTFUN1:def_6 .= halt S by A3, FUNCOP_1:72 ; hence NIC (((0 .--> (halt S)) /. l),l) c= dom (0 .--> (halt S)) by A2, A3, Th2; ::_thesis: verum end; registration let N be with_zero set ; let S be non empty with_non-empty_values IC-Ins-separated standard AMI-Struct over N; cluster Relation-like NAT -defined the InstructionsF of S -valued non empty Function-like finite initial really-closed -> NAT -defined the InstructionsF of S -valued finite paraclosed for set ; coherence for b1 being NAT -defined the InstructionsF of S -valued finite Function st b1 is really-closed & b1 is initial & not b1 is empty holds b1 is paraclosed proof let F be NAT -defined the InstructionsF of S -valued finite Function; ::_thesis: ( F is really-closed & F is initial & not F is empty implies F is paraclosed ) assume A1: F is really-closed ; ::_thesis: ( not F is initial or F is empty or F is paraclosed ) assume ( F is initial & not F is empty ) ; ::_thesis: F is paraclosed then 0 in dom F by AFINSQ_1:65; hence F is paraclosed by A1, Th15; ::_thesis: verum end; end; Lm7: now__::_thesis:_for_N_being_with_zero_set_ for_S_being_non_empty_with_non-empty_values_IC-Ins-separated_halting_standard_AMI-Struct_over_N_holds_ (_<%(halt_S)%>_._(LastLoc_<%(halt_S)%>)_=_halt_S_&_(_for_l_being_Nat_st_<%(halt_S)%>_._l_=_halt_S_&_l_in_dom_<%(halt_S)%>_holds_ l_=_LastLoc_<%(halt_S)%>_)_) let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated halting standard AMI-Struct over N holds ( <%(halt S)%> . (LastLoc <%(halt S)%>) = halt S & ( for l being Nat st <%(halt S)%> . l = halt S & l in dom <%(halt S)%> holds l = LastLoc <%(halt S)%> ) ) let S be non empty with_non-empty_values IC-Ins-separated halting standard AMI-Struct over N; ::_thesis: ( <%(halt S)%> . (LastLoc <%(halt S)%>) = halt S & ( for l being Nat st <%(halt S)%> . l = halt S & l in dom <%(halt S)%> holds l = LastLoc <%(halt S)%> ) ) set F = <%(halt S)%>; A1: dom <%(halt S)%> = {0} by FUNCOP_1:13; then A2: card (dom <%(halt S)%>) = 1 by CARD_1:30; A3: LastLoc <%(halt S)%> = (card <%(halt S)%>) -' 1 by AFINSQ_1:70 .= 0 by A2, XREAL_1:232 ; hence <%(halt S)%> . (LastLoc <%(halt S)%>) = halt S by FUNCOP_1:72; ::_thesis: for l being Nat st <%(halt S)%> . l = halt S & l in dom <%(halt S)%> holds l = LastLoc <%(halt S)%> let l be Nat; ::_thesis: ( <%(halt S)%> . l = halt S & l in dom <%(halt S)%> implies l = LastLoc <%(halt S)%> ) assume <%(halt S)%> . l = halt S ; ::_thesis: ( l in dom <%(halt S)%> implies l = LastLoc <%(halt S)%> ) assume l in dom <%(halt S)%> ; ::_thesis: l = LastLoc <%(halt S)%> hence l = LastLoc <%(halt S)%> by A1, A3, TARSKI:def_1; ::_thesis: verum end; registration let N be with_zero set ; let S be non empty with_non-empty_values IC-Ins-separated halting standard AMI-Struct over N; cluster Relation-like NAT -defined the InstructionsF of S -valued non empty trivial Function-like finite initial countable V139() really-closed for set ; existence ex b1 being NAT -defined the InstructionsF of S -valued finite Function st ( b1 is trivial & b1 is really-closed & b1 is initial & not b1 is empty ) proof reconsider F = <%(halt S)%> as NAT -defined the InstructionsF of S -valued non empty finite initial Function ; take F ; ::_thesis: ( F is trivial & F is really-closed & F is initial & not F is empty ) thus ( F is trivial & F is really-closed & F is initial & not F is empty ) by Th16; ::_thesis: verum end; end; registration let N be with_zero set ; let S be non empty with_non-empty_values IC-Ins-separated halting standard AMI-Struct over N; cluster Relation-like NAT -defined the InstructionsF of S -valued T-Sequence-like non empty trivial Function-like finite initial halt-ending unique-halt countable V139() really-closed for set ; existence ex b1 being NAT -defined the InstructionsF of S -valued non empty finite initial Function st ( b1 is halt-ending & b1 is unique-halt & b1 is trivial & b1 is really-closed ) proof reconsider F = <%(halt S)%> as NAT -defined the InstructionsF of S -valued non empty finite initial Function ; take F ; ::_thesis: ( F is halt-ending & F is unique-halt & F is trivial & F is really-closed ) thus F . (LastLoc F) = halt S by Lm7; :: according to COMPOS_1:def_14 ::_thesis: ( F is unique-halt & F is trivial & F is really-closed ) thus for f being Nat st F . f = halt S & f in dom F holds f = LastLoc F by Lm7; :: according to COMPOS_1:def_15 ::_thesis: ( F is trivial & F is really-closed ) thus ( F is trivial & F is really-closed ) by Th16; ::_thesis: verum end; end; registration let N be with_zero set ; let S be non empty with_non-empty_values IC-Ins-separated halting standard AMI-Struct over N; cluster Relation-like NAT -defined the InstructionsF of S -valued T-Sequence-like non empty Function-like finite initial halt-ending unique-halt countable V139() really-closed for set ; existence ex b1 being MacroInstruction of S st b1 is really-closed proof reconsider F = <%(halt S)%> as Program of ; ( F . (LastLoc F) = halt S & ( for l being Element of NAT st F . l = halt S & l in dom F holds l = LastLoc F ) ) by Lm7; then reconsider F = F as MacroInstruction of S by COMPOS_1:def_14; take F ; ::_thesis: F is really-closed thus F is really-closed by Th16; ::_thesis: verum end; end; theorem :: AMISTD_1:17 for N being with_zero set for i being Instruction of (Trivial-AMI N) holds i is halting proof let N be with_zero set ; ::_thesis: for i being Instruction of (Trivial-AMI N) holds i is halting let i be Instruction of (Trivial-AMI N); ::_thesis: i is halting set M = Trivial-AMI N; A1: the InstructionsF of (Trivial-AMI N) = {[0,{},{}]} by EXTPRO_1:def_1; let s be State of (Trivial-AMI N); :: according to EXTPRO_1:def_3 ::_thesis: Exec (i,s) = s reconsider s = s as Element of product (the_Values_of (Trivial-AMI N)) by CARD_3:107; A2: ( the Object-Kind of (Trivial-AMI N) = 0 .--> 0 & the ValuesF of (Trivial-AMI N) = N --> NAT ) by EXTPRO_1:def_1; the Execution of (Trivial-AMI N) . i = ([0,{},{}] .--> (id (product (the_Values_of (Trivial-AMI N))))) . i by A2, EXTPRO_1:def_1 .= id (product (the_Values_of (Trivial-AMI N))) by A1, FUNCOP_1:7 ; then ( the Execution of (Trivial-AMI N) . i) . s = s by FUNCT_1:18; hence Exec (i,s) = s ; ::_thesis: verum end; theorem :: AMISTD_1:18 for N being with_zero set for i being Element of the InstructionsF of (Trivial-AMI N) holds InsCode i = 0 proof let N be with_zero set ; ::_thesis: for i being Element of the InstructionsF of (Trivial-AMI N) holds InsCode i = 0 let i be Element of the InstructionsF of (Trivial-AMI N); ::_thesis: InsCode i = 0 the InstructionsF of (Trivial-AMI N) = {[0,{},{}]} by EXTPRO_1:def_1; then i = [0,{},{}] by TARSKI:def_1; hence InsCode i = 0 by RECDEF_2:def_1; ::_thesis: verum end; begin theorem :: AMISTD_1:19 for N being with_zero set for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N for i being Instruction of S for l being Element of NAT holds JUMP i c= NIC (i,l) proof let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N for i being Instruction of S for l being Element of NAT holds JUMP i c= NIC (i,l) let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; ::_thesis: for i being Instruction of S for l being Element of NAT holds JUMP i c= NIC (i,l) let i be Instruction of S; ::_thesis: for l being Element of NAT holds JUMP i c= NIC (i,l) let l be Element of NAT ; ::_thesis: JUMP i c= NIC (i,l) set X = { (NIC (i,k)) where k is Element of NAT : verum } ; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in JUMP i or x in NIC (i,l) ) A1: NIC (i,l) in { (NIC (i,k)) where k is Element of NAT : verum } ; assume x in JUMP i ; ::_thesis: x in NIC (i,l) hence x in NIC (i,l) by A1, SETFAM_1:def_1; ::_thesis: verum end; theorem :: AMISTD_1:20 for N being with_zero set for i being Instruction of (STC N) for s being State of (STC N) st InsCode i = 1 holds Exec (i,s) = IncIC (s,1) proof let N be with_zero set ; ::_thesis: for i being Instruction of (STC N) for s being State of (STC N) st InsCode i = 1 holds Exec (i,s) = IncIC (s,1) let i be Instruction of (STC N); ::_thesis: for s being State of (STC N) st InsCode i = 1 holds Exec (i,s) = IncIC (s,1) let s be State of (STC N); ::_thesis: ( InsCode i = 1 implies Exec (i,s) = IncIC (s,1) ) set M = STC N; assume A1: InsCode i = 1 ; ::_thesis: Exec (i,s) = IncIC (s,1) A2: now__::_thesis:_not_i_in_{[0,0,0]} assume i in {[0,0,0]} ; ::_thesis: contradiction then i = [0,0,0] by TARSKI:def_1; hence contradiction by A1, RECDEF_2:def_1; ::_thesis: verum end; the InstructionsF of (STC N) = {[1,0,0],[0,0,0]} by Def7; then ( i = [1,0,0] or i = [0,0,0] ) by TARSKI:def_2; then A3: i in {[1,0,0]} by A1, RECDEF_2:def_1, TARSKI:def_1; consider f being Function of (product (the_Values_of (STC N))),(product (the_Values_of (STC N))) such that A4: for s being Element of product (the_Values_of (STC N)) holds f . s = s +* (0 .--> (succ (s . 0))) and A5: the Execution of (STC N) = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product (the_Values_of (STC N))))) by Def7; A6: for s being State of (STC N) holds f . s = s +* (0 .--> (succ (s . 0))) proof let s be State of (STC N); ::_thesis: f . s = s +* (0 .--> (succ (s . 0))) reconsider s = s as Element of product (the_Values_of (STC N)) by CARD_3:107; f . s = s +* (0 .--> (succ (s . 0))) by A4; hence f . s = s +* (0 .--> (succ (s . 0))) ; ::_thesis: verum end; A7: the ZeroF of (STC N) = 0 by Def7; A8: Start-At (((IC s) + 1),(STC N)) = 0 .--> (succ (s . 0)) by A7, NAT_1:38; dom ([0,0,0] .--> (id (product (the_Values_of (STC N))))) = {[0,0,0]} by FUNCOP_1:13; then the Execution of (STC N) . i = ([1,0,0] .--> f) . i by A5, A2, FUNCT_4:11 .= f by A3, FUNCOP_1:7 ; hence Exec (i,s) = IncIC (s,1) by A8, A6; ::_thesis: verum end; registration let N be with_zero set ; let p be PartState of (STC N); cluster DataPart p -> empty ; coherence DataPart p is empty proof Data-Locations = the carrier of (STC N) \ {0} by Def7 .= {0} \ {0} by Def7 .= {} by XBOOLE_1:37 ; hence DataPart p is empty ; ::_thesis: verum end; end; theorem :: AMISTD_1:21 for N being with_zero set for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N for F being preProgram of S holds ( F is really-closed iff for s being State of S st IC s in dom F holds for P being Instruction-Sequence of S st F c= P holds for k being Element of NAT holds IC (Comput (P,s,k)) in dom F ) by Lm6; registration let N be with_zero set ; let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N; cluster Relation-like NAT -defined the InstructionsF of S -valued non empty Function-like finite non halt-free countable V139() parahalting for set ; existence ex b1 being NAT -defined the InstructionsF of S -valued non empty finite non halt-free Function st b1 is parahalting proof take Stop S ; ::_thesis: Stop S is parahalting let s be 0 -started State of S; :: according to AMISTD_1:def_11 ::_thesis: for P being Instruction-Sequence of S st Stop S c= P holds P halts_on s let P be Instruction-Sequence of S; ::_thesis: ( Stop S c= P implies P halts_on s ) assume A1: Stop S c= P ; ::_thesis: P halts_on s take 0 ; :: according to EXTPRO_1:def_8 ::_thesis: ( IC (Comput (P,s,0)) in dom P & CurInstr (P,(Comput (P,s,0))) = halt S ) A2: 0 in dom (Stop S) by COMPOS_1:3; dom (Stop S) c= dom P by A1, RELAT_1:11; then A3: 0 in dom P by A2; A4: IC s = 0 by MEMSTR_0:def_11; hence IC (Comput (P,s,0)) in dom P by A3; ::_thesis: CurInstr (P,(Comput (P,s,0))) = halt S thus CurInstr (P,(Comput (P,s,0))) = P /. 0 by A4 .= P . 0 by A3, PARTFUN1:def_6 .= (Stop S) . 0 by A1, A2, GRFUNC_1:2 .= halt S by AFINSQ_1:34 ; ::_thesis: verum end; end;