:: AMI_WSTD semantic presentation begin 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 l1, l2 be Nat; predl1 <= l2,S means :Def1: :: AMI_WSTD:def 1 ex f being non empty FinSequence of NAT st ( f /. 1 = l1 & f /. (len f) = l2 & ( for n being Element of NAT st 1 <= n & n < len f holds f /. (n + 1) in SUCC ((f /. n),S) ) ); end; :: deftheorem Def1 defines <= AMI_WSTD:def_1_:_ for N being with_zero set for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N for l1, l2 being Nat holds ( l1 <= l2,S iff ex f being non empty FinSequence of NAT st ( f /. 1 = l1 & f /. (len f) = l2 & ( for n being Element of NAT st 1 <= n & n < len f holds f /. (n + 1) in SUCC ((f /. n),S) ) ) ); theorem :: AMI_WSTD:1 for l3 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 for l1, l2 being Nat st l1 <= l2,S & l2 <= l3,S holds l1 <= l3,S proof let l3 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 for l1, l2 being Nat st l1 <= l2,S & l2 <= l3,S holds l1 <= l3,S let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N for l1, l2 being Nat st l1 <= l2,S & l2 <= l3,S holds l1 <= l3,S let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; ::_thesis: for l1, l2 being Nat st l1 <= l2,S & l2 <= l3,S holds l1 <= l3,S let l1, l2 be Nat; ::_thesis: ( l1 <= l2,S & l2 <= l3,S implies l1 <= l3,S ) given f1 being non empty FinSequence of NAT such that A1: f1 /. 1 = l1 and A2: f1 /. (len f1) = l2 and A3: for n being Element of NAT st 1 <= n & n < len f1 holds f1 /. (n + 1) in SUCC ((f1 /. n),S) ; :: according to AMI_WSTD:def_1 ::_thesis: ( not l2 <= l3,S or l1 <= l3,S ) given f2 being non empty FinSequence of NAT such that A4: f2 /. 1 = l2 and A5: f2 /. (len f2) = l3 and A6: for n being Element of NAT st 1 <= n & n < len f2 holds f2 /. (n + 1) in SUCC ((f2 /. n),S) ; :: according to AMI_WSTD:def_1 ::_thesis: l1 <= l3,S take f1 ^' f2 ; :: according to AMI_WSTD:def_1 ::_thesis: ( (f1 ^' f2) /. 1 = l1 & (f1 ^' f2) /. (len (f1 ^' f2)) = l3 & ( for n being Element of NAT st 1 <= n & n < len (f1 ^' f2) holds (f1 ^' f2) /. (n + 1) in SUCC (((f1 ^' f2) /. n),S) ) ) thus (f1 ^' f2) /. 1 = l1 by A1, GRAPH_2:53; ::_thesis: ( (f1 ^' f2) /. (len (f1 ^' f2)) = l3 & ( for n being Element of NAT st 1 <= n & n < len (f1 ^' f2) holds (f1 ^' f2) /. (n + 1) in SUCC (((f1 ^' f2) /. n),S) ) ) now__::_thesis:_(f1_^'_f2)_/._(len_(f1_^'_f2))_=_l3 percases ( f2 is trivial or not f2 is trivial ) ; suppose f2 is trivial ; ::_thesis: (f1 ^' f2) /. (len (f1 ^' f2)) = l3 then A7: ex x being Element of NAT st f2 = <*x*> by FINSEQ_6:107; then f1 ^' f2 = f1 by GRAPH_2:56; hence (f1 ^' f2) /. (len (f1 ^' f2)) = l3 by A2, A4, A5, A7, FINSEQ_1:39; ::_thesis: verum end; suppose not f2 is trivial ; ::_thesis: (f1 ^' f2) /. (len (f1 ^' f2)) = l3 hence (f1 ^' f2) /. (len (f1 ^' f2)) = l3 by A5, GRAPH_2:54; ::_thesis: verum end; end; end; hence (f1 ^' f2) /. (len (f1 ^' f2)) = l3 ; ::_thesis: for n being Element of NAT st 1 <= n & n < len (f1 ^' f2) holds (f1 ^' f2) /. (n + 1) in SUCC (((f1 ^' f2) /. n),S) let n be Element of NAT ; ::_thesis: ( 1 <= n & n < len (f1 ^' f2) implies (f1 ^' f2) /. (n + 1) in SUCC (((f1 ^' f2) /. n),S) ) assume that A8: 1 <= n and A9: n < len (f1 ^' f2) ; ::_thesis: (f1 ^' f2) /. (n + 1) in SUCC (((f1 ^' f2) /. n),S) A10: (len (f1 ^' f2)) + 1 = (len f1) + (len f2) by GRAPH_2:13; percases ( n < len f1 or n = len f1 or n > len f1 ) by XXREAL_0:1; supposeA11: n < len f1 ; ::_thesis: (f1 ^' f2) /. (n + 1) in SUCC (((f1 ^' f2) /. n),S) then n + 1 <= len f1 by NAT_1:13; then A12: (f1 ^' f2) /. (n + 1) = f1 /. (n + 1) by GRAPH_2:57, NAT_1:11; (f1 ^' f2) /. n = f1 /. n by A8, A11, GRAPH_2:57; hence (f1 ^' f2) /. (n + 1) in SUCC (((f1 ^' f2) /. n),S) by A3, A8, A11, A12; ::_thesis: verum end; supposeA13: n = len f1 ; ::_thesis: (f1 ^' f2) /. (n + 1) in SUCC (((f1 ^' f2) /. n),S) then A14: (f1 ^' f2) /. n = f2 /. 1 by A2, A4, A8, GRAPH_2:57; n + 1 < (len (f1 ^' f2)) + 1 by A9, XREAL_1:6; then A15: 1 < len f2 by A10, A13, XREAL_1:6; then (f1 ^' f2) /. (n + 1) = f2 /. (1 + 1) by A13, GRAPH_2:58; hence (f1 ^' f2) /. (n + 1) in SUCC (((f1 ^' f2) /. n),S) by A6, A14, A15; ::_thesis: verum end; supposeA16: n > len f1 ; ::_thesis: (f1 ^' f2) /. (n + 1) in SUCC (((f1 ^' f2) /. n),S) then consider m being Nat such that A17: (len f1) + m = n by NAT_1:10; reconsider m = m as Element of NAT by ORDINAL1:def_12; A18: (len f1) + m > (len f1) + 0 by A16, A17; ((len f1) + m) + 1 < (len f1) + (len f2) by A9, A10, A17, XREAL_1:6; then (len f1) + (m + 1) < (len f1) + (len f2) ; then A19: m + 1 < len f2 by XREAL_1:6; A20: (f1 ^' f2) /. (n + 1) = (f1 ^' f2) /. ((len f1) + (m + 1)) by A17 .= f2 /. ((m + 1) + 1) by A19, GRAPH_2:58, NAT_1:11 ; m <= m + 1 by NAT_1:11; then m < len f2 by A19, XXREAL_0:2; then (f1 ^' f2) /. n = f2 /. (m + 1) by A17, A18, GRAPH_2:58, NAT_1:14; hence (f1 ^' f2) /. (n + 1) in SUCC (((f1 ^' f2) /. n),S) by A6, A19, A20, NAT_1:11; ::_thesis: verum end; end; end; 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 InsLoc-antisymmetric means :: AMI_WSTD:def 2 for l1, l2 being Element of NAT st l1 <= l2,S & l2 <= l1,S holds l1 = l2; end; :: deftheorem defines InsLoc-antisymmetric AMI_WSTD:def_2_:_ 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 InsLoc-antisymmetric iff for l1, l2 being Element of NAT st l1 <= l2,S & l2 <= l1,S holds l1 = l2 ); 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 weakly_standard means :Def3: :: AMI_WSTD:def 3 ex f being Function of NAT,NAT st ( f is bijective & ( for m, n being Element of NAT holds ( m <= n iff f . m <= f . n,S ) ) ); end; :: deftheorem Def3 defines weakly_standard AMI_WSTD:def_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 weakly_standard iff ex f being Function of NAT,NAT st ( f is bijective & ( for m, n being Element of NAT holds ( m <= n iff f . m <= f . n,S ) ) ) ); theorem Th2: :: AMI_WSTD:2 for N being with_zero set for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N for f1, f2 being Function of NAT,NAT st f1 is bijective & ( for m, n being Element of NAT holds ( m <= n iff f1 . m <= f1 . n,S ) ) & f2 is bijective & ( for m, n being Element of NAT holds ( m <= n iff f2 . m <= f2 . n,S ) ) holds f1 = f2 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 f1, f2 being Function of NAT,NAT st f1 is bijective & ( for m, n being Element of NAT holds ( m <= n iff f1 . m <= f1 . n,S ) ) & f2 is bijective & ( for m, n being Element of NAT holds ( m <= n iff f2 . m <= f2 . n,S ) ) holds f1 = f2 let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; ::_thesis: for f1, f2 being Function of NAT,NAT st f1 is bijective & ( for m, n being Element of NAT holds ( m <= n iff f1 . m <= f1 . n,S ) ) & f2 is bijective & ( for m, n being Element of NAT holds ( m <= n iff f2 . m <= f2 . n,S ) ) holds f1 = f2 let f1, f2 be Function of NAT,NAT; ::_thesis: ( f1 is bijective & ( for m, n being Element of NAT holds ( m <= n iff f1 . m <= f1 . n,S ) ) & f2 is bijective & ( for m, n being Element of NAT holds ( m <= n iff f2 . m <= f2 . n,S ) ) implies f1 = f2 ) assume that A1: f1 is bijective and A2: for m, n being Element of NAT holds ( m <= n iff f1 . m <= f1 . n,S ) and A3: f2 is bijective and A4: for m, n being Element of NAT holds ( m <= n iff f2 . m <= f2 . n,S ) ; ::_thesis: f1 = f2 A5: dom f1 = NAT by FUNCT_2:def_1; A6: dom f2 = NAT by FUNCT_2:def_1; defpred S1[ Nat] means f1 . $1 <> f2 . $1; assume f1 <> f2 ; ::_thesis: contradiction then ex c being Element of NAT st S1[c] by FUNCT_2:63; then A7: ex c being Nat st S1[c] ; consider d being Nat such that A8: S1[d] and A9: for n being Nat st S1[n] holds d <= n from NAT_1:sch_5(A7); reconsider d = d as Element of NAT by ORDINAL1:def_12; A10: rng f1 = NAT by A1, FUNCT_2:def_3; A11: rng f2 = NAT by A3, FUNCT_2:def_3; consider d1 being set such that A12: d1 in dom f1 and A13: f2 . d = f1 . d1 by A10, FUNCT_1:def_3; reconsider d1 = d1 as Element of NAT by A12; consider d2 being set such that A14: d2 in dom f2 and A15: f1 . d = f2 . d2 by A11, FUNCT_1:def_3; reconsider d2 = d2 as Element of NAT by A14; percases ( ( d1 <= d & d2 <= d ) or ( d <= d1 & d2 <= d ) or ( d1 <= d & d <= d2 ) or ( d <= d1 & d <= d2 ) ) ; supposeA16: ( d1 <= d & d2 <= d ) ; ::_thesis: contradiction then f2 . d2 <= f2 . d,S by A4; then d <= d1 by A2, A15, A13; hence contradiction by A8, A13, A16, XXREAL_0:1; ::_thesis: verum end; supposeA17: ( d <= d1 & d2 <= d ) ; ::_thesis: contradiction f2 . d2 = f1 . d2 proof assume not f2 . d2 = f1 . d2 ; ::_thesis: contradiction then d <= d2 by A9; hence contradiction by A8, A15, A17, XXREAL_0:1; ::_thesis: verum end; hence contradiction by A1, A8, A15, A5, FUNCT_1:def_4; ::_thesis: verum end; supposeA18: ( d1 <= d & d <= d2 ) ; ::_thesis: contradiction f1 . d1 = f2 . d1 proof assume not f1 . d1 = f2 . d1 ; ::_thesis: contradiction then d <= d1 by A9; hence contradiction by A8, A13, A18, XXREAL_0:1; ::_thesis: verum end; hence contradiction by A3, A8, A13, A6, FUNCT_1:def_4; ::_thesis: verum end; supposeA19: ( d <= d1 & d <= d2 ) ; ::_thesis: contradiction then f2 . d <= f2 . d2,S by A4; then d1 <= d by A2, A15, A13; hence contradiction by A8, A13, A19, XXREAL_0:1; ::_thesis: verum end; end; end; Lm1: 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 holds k <= k,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 holds k <= k,S let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N holds k <= k,S let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; ::_thesis: k <= k,S reconsider l = k as Element of NAT ; reconsider f = <*l*> as non empty FinSequence of NAT ; take f ; :: according to AMI_WSTD:def_1 ::_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: :: AMI_WSTD:3 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 Function of NAT,NAT st f is bijective holds ( ( for m, n being Element of NAT holds ( m <= n iff f . m <= f . n,S ) ) iff for k being Element of NAT holds ( f . (k + 1) in SUCC ((f . k),S) & ( for j being Element of NAT st f . j in SUCC ((f . 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 for f being Function of NAT,NAT st f is bijective holds ( ( for m, n being Element of NAT holds ( m <= n iff f . m <= f . n,S ) ) iff for k being Element of NAT holds ( f . (k + 1) in SUCC ((f . k),S) & ( for j being Element of NAT st f . j in SUCC ((f . k),S) holds k <= j ) ) ) let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; ::_thesis: for f being Function of NAT,NAT st f is bijective holds ( ( for m, n being Element of NAT holds ( m <= n iff f . m <= f . n,S ) ) iff for k being Element of NAT holds ( f . (k + 1) in SUCC ((f . k),S) & ( for j being Element of NAT st f . j in SUCC ((f . k),S) holds k <= j ) ) ) let f be Function of NAT,NAT; ::_thesis: ( f is bijective implies ( ( for m, n being Element of NAT holds ( m <= n iff f . m <= f . n,S ) ) iff for k being Element of NAT holds ( f . (k + 1) in SUCC ((f . k),S) & ( for j being Element of NAT st f . j in SUCC ((f . k),S) holds k <= j ) ) ) ) assume A1: f is bijective ; ::_thesis: ( ( for m, n being Element of NAT holds ( m <= n iff f . m <= f . n,S ) ) iff for k being Element of NAT holds ( f . (k + 1) in SUCC ((f . k),S) & ( for j being Element of NAT st f . j in SUCC ((f . k),S) holds k <= j ) ) ) hereby ::_thesis: ( ( for k being Element of NAT holds ( f . (k + 1) in SUCC ((f . k),S) & ( for j being Element of NAT st f . j in SUCC ((f . k),S) holds k <= j ) ) ) implies for m, n being Element of NAT holds ( m <= n iff f . m <= f . n,S ) ) assume A2: for m, n being Element of NAT holds ( m <= n iff f . m <= f . n,S ) ; ::_thesis: for k being Element of NAT holds ( f . (k + 1) in SUCC ((f . k),S) & ( for j being Element of NAT st f . j in SUCC ((f . k),S) holds k <= j ) ) let k be Element of NAT ; ::_thesis: ( f . (k + 1) in SUCC ((f . k),S) & ( for j being Element of NAT st f . j in SUCC ((f . k),S) holds k <= j ) ) k <= k + 1 by NAT_1:11; then f . k <= f . (k + 1),S by A2; then consider F being non empty FinSequence of NAT such that A3: F /. 1 = f . k and A4: F /. (len F) = f . (k + 1) and A5: for n being Element of NAT st 1 <= n & n < len F holds F /. (n + 1) in SUCC ((F /. n),S) by Def1; set F1 = F -| (f . (k + 1)); set x = (f . (k + 1)) .. F; A6: f . (k + 1) in rng F by A4, REVROT_1:3; then A7: len (F -| (f . (k + 1))) = ((f . (k + 1)) .. F) - 1 by FINSEQ_4:34; then A8: (len (F -| (f . (k + 1)))) + 1 = (f . (k + 1)) .. F ; A9: (f . (k + 1)) .. F in dom F by A6, FINSEQ_4:20; then A10: F /. ((len (F -| (f . (k + 1)))) + 1) = F . ((f . (k + 1)) .. F) by A7, PARTFUN1:def_6 .= f . (k + 1) by A6, FINSEQ_4:19 ; (f . (k + 1)) .. F <= len F by A9, FINSEQ_3:25; then A11: len (F -| (f . (k + 1))) < len F by A8, NAT_1:13; 1 <= len F by NAT_1:14; then A12: 1 in dom F by FINSEQ_3:25; then A13: F /. 1 = F . 1 by PARTFUN1:def_6; A14: F . ((f . (k + 1)) .. F) = f . (k + 1) by A6, FINSEQ_4:19; A15: dom f = NAT by FUNCT_2:def_1; A16: f . k <> f . (k + 1) proof assume not f . k <> f . (k + 1) ; ::_thesis: contradiction then 0 + k = k + 1 by A1, A15, FUNCT_1:def_4; hence contradiction ; ::_thesis: verum end; then A17: len (F -| (f . (k + 1))) <> 0 by A3, A14, A12, A7, PARTFUN1:def_6; 1 <= (f . (k + 1)) .. F by A9, FINSEQ_3:25; then 1 < (f . (k + 1)) .. F by A3, A16, A14, A13, XXREAL_0:1; then A18: 1 <= len (F -| (f . (k + 1))) by A8, NAT_1:13; reconsider F1 = F -| (f . (k + 1)) as non empty FinSequence of NAT by A17, A6, FINSEQ_4:41; rng f = NAT by A1, FUNCT_2:def_3; then consider m being set such that A19: m in dom f and A20: f . m = F /. (len F1) by FUNCT_1:def_3; reconsider m = m as Element of NAT by A19; A21: len F1 in dom F by A18, A11, FINSEQ_3:25; A22: len F1 in dom F1 by A18, FINSEQ_3:25; then A23: F1 /. (len F1) = F1 . (len F1) by PARTFUN1:def_6 .= F . (len F1) by A6, A22, FINSEQ_4:36 .= F /. (len F1) by A21, PARTFUN1:def_6 ; A24: now__::_thesis:_not_m_=_k_+_1 rng F1 misses {(f . (k + 1))} by A6, FINSEQ_4:38; then (rng F1) /\ {(f . (k + 1))} = {} by XBOOLE_0:def_7; then A25: ( not f . (k + 1) in rng F1 or not f . (k + 1) in {(f . (k + 1))} ) by XBOOLE_0:def_4; assume A26: m = k + 1 ; ::_thesis: contradiction A27: len F1 in dom F1 by A18, FINSEQ_3:25; then F1 /. (len F1) = F1 . (len F1) by PARTFUN1:def_6; hence contradiction by A20, A23, A26, A25, A27, FUNCT_1:def_3, TARSKI:def_1; ::_thesis: verum end; reconsider F2 = <*(F /. (len F1)),(F /. ((f . (k + 1)) .. F))*> as non empty FinSequence of NAT ; A28: len F2 = 2 by FINSEQ_1:44; then A29: 2 in dom F2 by FINSEQ_3:25; then A30: F2 /. (len F2) = F2 . 2 by A28, PARTFUN1:def_6 .= F /. ((f . (k + 1)) .. F) by FINSEQ_1:44 .= f . (k + 1) by A14, A9, PARTFUN1:def_6 ; A31: 1 in dom F2 by A28, FINSEQ_3:25; A32: 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 A33: n = 1 by NAT_1:26; then A34: F2 /. n = F2 . 1 by A31, PARTFUN1:def_6 .= F /. (len F1) by FINSEQ_1:44 ; F2 /. (n + 1) = F2 . 2 by A29, A33, PARTFUN1:def_6 .= F /. ((len F1) + 1) by A7, FINSEQ_1:44 ; hence F2 /. (n + 1) in SUCC ((F2 /. n),S) by A5, A18, A11, A34; ::_thesis: verum end; A35: 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 A36: 1 <= n and A37: n < len F1 ; ::_thesis: F1 /. (n + 1) in SUCC ((F1 /. n),S) A38: 1 <= n + 1 by A36, NAT_1:13; A39: n + 1 <= len F1 by A37, NAT_1:13; then n + 1 <= len F by A11, XXREAL_0:2; then A40: n + 1 in dom F by A38, FINSEQ_3:25; n <= len F by A11, A37, XXREAL_0:2; then A41: n in dom F by A36, FINSEQ_3:25; A42: n in dom F1 by A36, A37, FINSEQ_3:25; then A43: F1 /. n = F1 . n by PARTFUN1:def_6 .= F . n by A6, A42, FINSEQ_4:36 .= F /. n by A41, PARTFUN1:def_6 ; A44: n < len F by A11, A37, XXREAL_0:2; A45: n + 1 in dom F1 by A38, A39, FINSEQ_3:25; then F1 /. (n + 1) = F1 . (n + 1) by PARTFUN1:def_6 .= F . (n + 1) by A6, A45, FINSEQ_4:36 .= F /. (n + 1) by A40, PARTFUN1:def_6 ; hence F1 /. (n + 1) in SUCC ((F1 /. n),S) by A5, A36, A43, A44; ::_thesis: verum end; F2 /. 1 = F2 . 1 by A31, PARTFUN1:def_6 .= f . m by A20, FINSEQ_1:44 ; then f . m <= f . (k + 1),S by A30, A32, Def1; then A46: m <= k + 1 by A2; A47: 1 in dom F1 by A18, FINSEQ_3:25; then F1 /. 1 = F1 . 1 by PARTFUN1:def_6 .= F . 1 by A6, A47, FINSEQ_4:36 .= f . k by A3, A12, PARTFUN1:def_6 ; then f . k <= f . m,S by A20, A23, A35, Def1; then k <= m by A2; then ( m = k or m = k + 1 ) by A46, NAT_1:9; hence f . (k + 1) in SUCC ((f . k),S) by A5, A18, A11, A10, A20, A24; ::_thesis: for j being Element of NAT st f . j in SUCC ((f . k),S) holds k <= j let j be Element of NAT ; ::_thesis: ( f . j in SUCC ((f . k),S) implies k <= j ) reconsider fk = f . k, fj = f . j as Element of NAT ; reconsider F = <*fk,fj*> as non empty FinSequence of NAT ; A48: len F = 2 by FINSEQ_1:44; then A49: 2 in dom F by FINSEQ_3:25; A50: 1 in dom F by A48, FINSEQ_3:25; then A51: F /. 1 = F . 1 by PARTFUN1:def_6 .= f . k by FINSEQ_1:44 ; assume A52: f . j in SUCC ((f . k),S) ; ::_thesis: k <= j A53: 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 A54: n = 1 by NAT_1:26; then A55: F /. n = F . 1 by A50, PARTFUN1:def_6 .= f . k by FINSEQ_1:44 ; F /. (n + 1) = F . 2 by A49, A54, PARTFUN1:def_6 .= f . j by FINSEQ_1:44 ; hence F /. (n + 1) in SUCC ((F /. n),S) by A52, A55; ::_thesis: verum end; F /. (len F) = F . 2 by A48, A49, PARTFUN1:def_6 .= f . j by FINSEQ_1:44 ; then f . k <= f . j,S by A51, A53, Def1; hence k <= j by A2; ::_thesis: verum end; assume A56: for k being Element of NAT holds ( f . (k + 1) in SUCC ((f . k),S) & ( for j being Element of NAT st f . j in SUCC ((f . k),S) holds k <= j ) ) ; ::_thesis: for m, n being Element of NAT holds ( m <= n iff f . m <= f . n,S ) let m, n be Element of NAT ; ::_thesis: ( m <= n iff f . m <= f . n,S ) hereby ::_thesis: ( f . m <= f . n,S implies m <= n ) assume A57: m <= n ; ::_thesis: f . m <= f . n,S percases ( m = n or m < n ) by A57, XXREAL_0:1; suppose m = n ; ::_thesis: f . m <= f . n,S hence f . m <= f . n,S by Lm1; ::_thesis: verum end; supposeA58: m < n ; ::_thesis: f . m <= f . n,S thus f . m <= f . n,S ::_thesis: verum proof reconsider f9 = f as Function of NAT,NAT ; set mn = n -' m; deffunc H1( Nat) -> Element of NAT = f9 . ((m + $1) -' 1); consider F being FinSequence of NAT such that A59: len F = (n -' m) + 1 and A60: 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 A59; take F ; :: according to AMI_WSTD:def_1 ::_thesis: ( F /. 1 = f . m & F /. (len F) = f . n & ( for n being Element of NAT st 1 <= n & n < len F holds F /. (n + 1) in SUCC ((F /. n),S) ) ) A61: 1 <= (n -' m) + 1 by NAT_1:11; then A62: 1 in dom F by A59, FINSEQ_3:25; hence F /. 1 = F . 1 by PARTFUN1:def_6 .= f . ((m + 1) -' 1) by A60, A62 .= f . m by NAT_D:34 ; ::_thesis: ( F /. (len F) = 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 A58, INT_1:7; then 1 <= n - m by XREAL_1:19; then 0 <= n - m by XXREAL_0:2; then A63: n -' m = n - m by XREAL_0:def_2; A64: len F in dom F by A59, A61, FINSEQ_3:25; hence F /. (len F) = F . (len F) by PARTFUN1:def_6 .= f . ((m + ((n -' m) + 1)) -' 1) by A59, A60, A64 .= f . (((m + (n -' m)) + 1) -' 1) .= f . n by A63, 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 A65: 1 <= p and A66: p < len F ; ::_thesis: F /. (p + 1) in SUCC ((F /. p),S) A67: p in dom F by A65, A66, FINSEQ_3:25; then A68: F /. p = F . p by PARTFUN1:def_6 .= f . ((m + p) -' 1) by A60, A67 ; A69: p <= m + p by NAT_1:11; ( 1 <= p + 1 & p + 1 <= len F ) by A65, A66, NAT_1:13; then A70: p + 1 in dom F by FINSEQ_3:25; then F /. (p + 1) = F . (p + 1) by PARTFUN1:def_6 .= f . ((m + (p + 1)) -' 1) by A60, A70 .= f . (((m + p) + 1) -' 1) .= f . (((m + p) -' 1) + 1) by A65, A69, NAT_D:38, XXREAL_0:2 ; hence F /. (p + 1) in SUCC ((F /. p),S) by A56, A68; ::_thesis: verum end; end; end; end; assume f . m <= f . n,S ; ::_thesis: m <= n then consider F being non empty FinSequence of NAT such that A71: F /. 1 = f . m and A72: F /. (len F) = f . n and A73: for n being Element of NAT st 1 <= n & n < len F holds F /. (n + 1) in SUCC ((F /. n),S) by Def1; defpred S1[ Element of NAT ] means ( 1 <= $1 & $1 <= len F implies ex l being Element of NAT st ( F /. $1 = f . l & m <= l ) ); A74: 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 A75: 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)_=_f_._l_&_m_<=_l_)_) assume that 1 <= k + 1 and A76: k + 1 <= len F ; ::_thesis: ex l being Element of NAT st ( F /. (k + 1) = f . 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) = f . l & m <= l ) hence ex l being Element of NAT st ( F /. (k + 1) = f . l & m <= l ) by A71; ::_thesis: verum end; supposeA77: k > 0 ; ::_thesis: ex l being Element of NAT st ( F /. (k + 1) = f . l & m <= l ) rng f = NAT by A1, FUNCT_2:def_3; then consider l1 being set such that A78: l1 in dom f and A79: f . l1 = F /. (k + 1) by FUNCT_1:def_3; consider l being Element of NAT such that A80: F /. k = f . l and A81: m <= l by A75, A76, A77, NAT_1:13, NAT_1:14; reconsider l1 = l1 as Element of NAT by A78; k < len F by A76, NAT_1:13; then F /. (k + 1) in SUCC ((F /. k),S) by A73, A77, NAT_1:14; then l <= l1 by A56, A80, A79; hence ex l being Element of NAT st ( F /. (k + 1) = f . l & m <= l ) by A81, A79, XXREAL_0:2; ::_thesis: verum end; end; end; hence S1[k + 1] ; ::_thesis: verum end; A82: 1 <= len F by NAT_1:14; A83: S1[ 0 ] ; for k being Element of NAT holds S1[k] from NAT_1:sch_1(A83, A74); then ( dom f = NAT & ex l being Element of NAT st ( F /. (len F) = f . l & m <= l ) ) by A82, FUNCT_2:def_1; hence m <= n by A1, A72, FUNCT_1:def_4; ::_thesis: verum end; theorem Th4: :: AMI_WSTD:4 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 weakly_standard iff ex f being Function of NAT,NAT st ( f is bijective & ( for k being Element of NAT holds ( f . (k + 1) in SUCC ((f . k),S) & ( for j being Element of NAT st f . j in SUCC ((f . 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 weakly_standard iff ex f being Function of NAT,NAT st ( f is bijective & ( for k being Element of NAT holds ( f . (k + 1) in SUCC ((f . k),S) & ( for j being Element of NAT st f . j in SUCC ((f . k),S) holds k <= j ) ) ) ) ) let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; ::_thesis: ( S is weakly_standard iff ex f being Function of NAT,NAT st ( f is bijective & ( for k being Element of NAT holds ( f . (k + 1) in SUCC ((f . k),S) & ( for j being Element of NAT st f . j in SUCC ((f . k),S) holds k <= j ) ) ) ) ) hereby ::_thesis: ( ex f being Function of NAT,NAT st ( f is bijective & ( for k being Element of NAT holds ( f . (k + 1) in SUCC ((f . k),S) & ( for j being Element of NAT st f . j in SUCC ((f . k),S) holds k <= j ) ) ) ) implies S is weakly_standard ) assume S is weakly_standard ; ::_thesis: ex f being Function of NAT,NAT st ( f is bijective & ( for k being Element of NAT holds ( f . (k + 1) in SUCC ((f . k),S) & ( for j being Element of NAT st f . j in SUCC ((f . k),S) holds k <= j ) ) ) ) then consider f being Function of NAT,NAT such that A1: f is bijective and A2: for m, n being Element of NAT holds ( m <= n iff f . m <= f . n,S ) by Def3; thus ex f being Function of NAT,NAT st ( f is bijective & ( for k being Element of NAT holds ( f . (k + 1) in SUCC ((f . k),S) & ( for j being Element of NAT st f . j in SUCC ((f . k),S) holds k <= j ) ) ) ) ::_thesis: verum proof take f ; ::_thesis: ( f is bijective & ( for k being Element of NAT holds ( f . (k + 1) in SUCC ((f . k),S) & ( for j being Element of NAT st f . j in SUCC ((f . k),S) holds k <= j ) ) ) ) thus f is bijective by A1; ::_thesis: for k being Element of NAT holds ( f . (k + 1) in SUCC ((f . k),S) & ( for j being Element of NAT st f . j in SUCC ((f . k),S) holds k <= j ) ) thus for k being Element of NAT holds ( f . (k + 1) in SUCC ((f . k),S) & ( for j being Element of NAT st f . j in SUCC ((f . k),S) holds k <= j ) ) by A1, A2, Th3; ::_thesis: verum end; end; given f being Function of NAT,NAT such that A3: f is bijective and A4: for k being Element of NAT holds ( f . (k + 1) in SUCC ((f . k),S) & ( for j being Element of NAT st f . j in SUCC ((f . k),S) holds k <= j ) ) ; ::_thesis: S is weakly_standard take f ; :: according to AMI_WSTD:def_3 ::_thesis: ( f is bijective & ( for m, n being Element of NAT holds ( m <= n iff f . m <= f . n,S ) ) ) thus f is bijective by A3; ::_thesis: for m, n being Element of NAT holds ( m <= n iff f . m <= f . n,S ) thus for m, n being Element of NAT holds ( m <= n iff f . m <= f . n,S ) by A3, A4, Th3; ::_thesis: verum end; set III = {[1,0,0],[0,0,0]}; begin Lm2: 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 IC (Exec (i,s)) = 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 IC (Exec (i,s)) = succ (IC s) let i be Instruction of (STC N); ::_thesis: for s being State of (STC N) st InsCode i = 1 holds IC (Exec (i,s)) = succ (IC s) let s be State of (STC N); ::_thesis: ( InsCode i = 1 implies IC (Exec (i,s)) = succ (IC s) ) set M = STC N; assume A1: InsCode i = 1 ; ::_thesis: IC (Exec (i,s)) = 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 AMISTD_1:def_7; 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 AMISTD_1:def_7; 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 AMISTD_1:def_7; 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 IC (Exec (i,s)) = (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; Lm3: 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__}__)_) reconsider f = NAT --> i as Instruction-Sequence of (STC N) ; reconsider l9 = l as Element of Values (IC ) by MEMSTR_0:def_6; reconsider w = the l -started State of (STC N) as Element of product (the_Values_of (STC N)) by CARD_3:107; 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 = w +* ((IC ) .--> l9) as Element of product (the_Values_of (STC N)) by CARD_3:107; 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, Lm2 .= 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 A4: y = succ z by TARSKI:def_1; IC in dom ((IC ) .--> l9) by A3, TARSKI:def_1; then A5: IC t = ((IC ) .--> l9) . (IC ) by FUNCT_4:13 .= z by A1, FUNCOP_1:72 ; then IC (Exec (i,t)) = succ z by A2, Lm2; hence y in { (IC (Exec (i,ss))) where ss is Element of product (the_Values_of (STC N)) : IC ss = l } by A1, A4, A5; ::_thesis: verum end; hence NIC (i,l) = {(z + 1)} by TARSKI:1; ::_thesis: verum end; registration let N be with_zero set ; cluster STC N -> weakly_standard ; coherence STC N is weakly_standard proof reconsider f = id NAT as Function of NAT,NAT ; set M = STC N; now__::_thesis:_for_k_being_Element_of_NAT_holds_ (_f_._(k_+_1)_in_SUCC_((f_._k),(STC_N))_&_(_for_j_being_Element_of_NAT_st_f_._j_in_SUCC_((f_._k),(STC_N))_holds_ k_<=_j_)_) let k be Element of NAT ; ::_thesis: ( f . (k + 1) in SUCC ((f . k),(STC N)) & ( for j being Element of NAT st f . j in SUCC ((f . k),(STC N)) holds k <= j ) ) reconsider fk = f . k as Element of NAT ; A1: SUCC (fk,(STC N)) = {k,(k + 1)} by AMISTD_1:8, FUNCT_1:18; f . (k + 1) = k + 1 by FUNCT_1:18; hence f . (k + 1) in SUCC ((f . k),(STC N)) by A1, TARSKI:def_2; ::_thesis: for j being Element of NAT st f . j in SUCC ((f . k),(STC N)) holds k <= j let j be Element of NAT ; ::_thesis: ( f . j in SUCC ((f . k),(STC N)) implies k <= j ) assume f . j in SUCC ((f . k),(STC N)) ; ::_thesis: k <= j then ( f . j = k or f . j = k + 1 ) by A1, TARSKI:def_2; then ( j = k + 1 or j = k ) by FUNCT_1:18; hence k <= j by NAT_1:11; ::_thesis: verum end; hence STC N is weakly_standard by Th4; ::_thesis: verum end; end; registration let N be with_zero set ; cluster non empty with_non-empty_values IC-Ins-separated halting weakly_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 weakly_standard & b1 is halting ) proof take STC N ; ::_thesis: ( STC N is weakly_standard & STC N is halting ) thus ( STC N is weakly_standard & STC N is halting ) ; ::_thesis: verum end; end; definition let N be with_zero set ; let S be non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N; let k be Nat; func il. (S,k) -> Element of NAT means :Def4: :: AMI_WSTD:def 4 ex f being Function of NAT,NAT st ( f is bijective & ( for m, n being Element of NAT holds ( m <= n iff f . m <= f . n,S ) ) & it = f . k ); existence ex b1 being Element of NAT ex f being Function of NAT,NAT st ( f is bijective & ( for m, n being Element of NAT holds ( m <= n iff f . m <= f . n,S ) ) & b1 = f . k ) proof reconsider k = k as Element of NAT by ORDINAL1:def_12; consider f being Function of NAT,NAT such that A1: ( f is bijective & ( for m, n being Element of NAT holds ( m <= n iff f . m <= f . n,S ) ) ) by Def3; reconsider fk = f . k as Element of NAT ; take fk ; ::_thesis: ex f being Function of NAT,NAT st ( f is bijective & ( for m, n being Element of NAT holds ( m <= n iff f . m <= f . n,S ) ) & fk = f . k ) take f ; ::_thesis: ( f is bijective & ( for m, n being Element of NAT holds ( m <= n iff f . m <= f . n,S ) ) & fk = f . k ) thus ( f is bijective & ( for m, n being Element of NAT holds ( m <= n iff f . m <= f . n,S ) ) & fk = f . k ) by A1; ::_thesis: verum end; uniqueness for b1, b2 being Element of NAT st ex f being Function of NAT,NAT st ( f is bijective & ( for m, n being Element of NAT holds ( m <= n iff f . m <= f . n,S ) ) & b1 = f . k ) & ex f being Function of NAT,NAT st ( f is bijective & ( for m, n being Element of NAT holds ( m <= n iff f . m <= f . n,S ) ) & b2 = f . k ) holds b1 = b2 by Th2; end; :: deftheorem Def4 defines il. AMI_WSTD:def_4_:_ for N being with_zero set for S being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N for k being Nat for b4 being Element of NAT holds ( b4 = il. (S,k) iff ex f being Function of NAT,NAT st ( f is bijective & ( for m, n being Element of NAT holds ( m <= n iff f . m <= f . n,S ) ) & b4 = f . k ) ); theorem Th5: :: AMI_WSTD:5 for N being with_zero set for T being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N for k1, k2 being Nat st il. (T,k1) = il. (T,k2) holds k1 = k2 proof let N be with_zero set ; ::_thesis: for T being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N for k1, k2 being Nat st il. (T,k1) = il. (T,k2) holds k1 = k2 let T be non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N; ::_thesis: for k1, k2 being Nat st il. (T,k1) = il. (T,k2) holds k1 = k2 let k1, k2 be Nat; ::_thesis: ( il. (T,k1) = il. (T,k2) implies k1 = k2 ) assume A1: il. (T,k1) = il. (T,k2) ; ::_thesis: k1 = k2 A2: ( k1 is Element of NAT & k2 is Element of NAT ) by ORDINAL1:def_12; consider f2 being Function of NAT,NAT such that A3: ( f2 is bijective & ( for m, n being Element of NAT holds ( m <= n iff f2 . m <= f2 . n,T ) ) ) and A4: il. (T,k2) = f2 . k2 by Def4; consider f1 being Function of NAT,NAT such that A5: f1 is bijective and A6: for m, n being Element of NAT holds ( m <= n iff f1 . m <= f1 . n,T ) and A7: il. (T,k1) = f1 . k1 by Def4; A8: dom f1 = NAT by FUNCT_2:def_1; f1 = f2 by A5, A6, A3, Th2; hence k1 = k2 by A1, A2, A5, A7, A4, A8, FUNCT_1:def_4; ::_thesis: verum end; theorem Th6: :: AMI_WSTD:6 for N being with_zero set for T being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N for l being Nat ex k being Nat st l = il. (T,k) proof let N be with_zero set ; ::_thesis: for T being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N for l being Nat ex k being Nat st l = il. (T,k) let T be non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N; ::_thesis: for l being Nat ex k being Nat st l = il. (T,k) let l be Nat; ::_thesis: ex k being Nat st l = il. (T,k) consider f1 being Function of NAT,NAT such that A1: f1 is bijective and A2: for m, n being Element of NAT holds ( m <= n iff f1 . m <= f1 . n,T ) and il. (T,0) = f1 . 0 by Def4; ( l in NAT & rng f1 = NAT ) by A1, FUNCT_2:def_3, ORDINAL1:def_12; then consider k being set such that A3: k in dom f1 and A4: f1 . k = l by FUNCT_1:def_3; reconsider k = k as Nat by A3; take k ; ::_thesis: l = il. (T,k) reconsider l = l as Element of NAT by ORDINAL1:def_12; l = il. (T,k) by A1, A2, A4, Def4; hence l = il. (T,k) ; ::_thesis: verum end; definition let N be with_zero set ; let S be non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N; let l be Nat; func locnum (l,S) -> Nat means :Def5: :: AMI_WSTD:def 5 il. (S,it) = l; existence ex b1 being Nat st il. (S,b1) = l by Th6; uniqueness for b1, b2 being Nat st il. (S,b1) = l & il. (S,b2) = l holds b1 = b2 by Th5; end; :: deftheorem Def5 defines locnum AMI_WSTD:def_5_:_ for N being with_zero set for S being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N for l, b4 being Nat holds ( b4 = locnum (l,S) iff il. (S,b4) = l ); definition let N be with_zero set ; let S be non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N; let l be Nat; :: original: locnum redefine func locnum (l,S) -> Element of NAT ; coherence locnum (l,S) is Element of NAT by ORDINAL1:def_12; end; theorem Th7: :: AMI_WSTD:7 for N being with_zero set for T being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N for l1, l2 being Element of NAT st locnum (l1,T) = locnum (l2,T) holds l1 = l2 proof let N be with_zero set ; ::_thesis: for T being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N for l1, l2 being Element of NAT st locnum (l1,T) = locnum (l2,T) holds l1 = l2 let T be non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N; ::_thesis: for l1, l2 being Element of NAT st locnum (l1,T) = locnum (l2,T) holds l1 = l2 let l1, l2 be Element of NAT ; ::_thesis: ( locnum (l1,T) = locnum (l2,T) implies l1 = l2 ) assume A1: locnum (l1,T) = locnum (l2,T) ; ::_thesis: l1 = l2 il. (T,(locnum (l1,T))) = l1 by Def5; hence l1 = l2 by A1, Def5; ::_thesis: verum end; theorem Th8: :: AMI_WSTD:8 for N being with_zero set for T being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N for k1, k2 being Nat holds ( il. (T,k1) <= il. (T,k2),T iff k1 <= k2 ) proof let N be with_zero set ; ::_thesis: for T being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N for k1, k2 being Nat holds ( il. (T,k1) <= il. (T,k2),T iff k1 <= k2 ) let T be non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N; ::_thesis: for k1, k2 being Nat holds ( il. (T,k1) <= il. (T,k2),T iff k1 <= k2 ) let k1, k2 be Nat; ::_thesis: ( il. (T,k1) <= il. (T,k2),T iff k1 <= k2 ) A1: ( k1 is Element of NAT & k2 is Element of NAT ) by ORDINAL1:def_12; consider f2 being Function of NAT,NAT such that A2: ( f2 is bijective & ( for m, n being Element of NAT holds ( m <= n iff f2 . m <= f2 . n,T ) ) ) and A3: il. (T,k2) = f2 . k2 by Def4; consider f1 being Function of NAT,NAT such that A4: f1 is bijective and A5: for m, n being Element of NAT holds ( m <= n iff f1 . m <= f1 . n,T ) and A6: il. (T,k1) = f1 . k1 by Def4; f1 = f2 by A4, A5, A2, Th2; hence ( il. (T,k1) <= il. (T,k2),T iff k1 <= k2 ) by A1, A5, A6, A3; ::_thesis: verum end; theorem Th9: :: AMI_WSTD:9 for N being with_zero set for T being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N for l1, l2 being Element of NAT holds ( locnum (l1,T) <= locnum (l2,T) iff l1 <= l2,T ) proof let N be with_zero set ; ::_thesis: for T being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N for l1, l2 being Element of NAT holds ( locnum (l1,T) <= locnum (l2,T) iff l1 <= l2,T ) let T be non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N; ::_thesis: for l1, l2 being Element of NAT holds ( locnum (l1,T) <= locnum (l2,T) iff l1 <= l2,T ) let l1, l2 be Element of NAT ; ::_thesis: ( locnum (l1,T) <= locnum (l2,T) iff l1 <= l2,T ) ( il. (T,(locnum (l1,T))) = l1 & il. (T,(locnum (l2,T))) = l2 ) by Def5; hence ( locnum (l1,T) <= locnum (l2,T) iff l1 <= l2,T ) by Th8; ::_thesis: verum end; theorem Th10: :: AMI_WSTD:10 for N being with_zero set for T being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N holds T is InsLoc-antisymmetric proof let N be with_zero set ; ::_thesis: for T being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N holds T is InsLoc-antisymmetric let T be non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N; ::_thesis: T is InsLoc-antisymmetric let l1, l2 be Element of NAT ; :: according to AMI_WSTD:def_2 ::_thesis: ( l1 <= l2,T & l2 <= l1,T implies l1 = l2 ) assume A1: ( l1 <= l2,T & l2 <= l1,T ) ; ::_thesis: l1 = l2 reconsider T = T as non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N ; reconsider l1 = l1, l2 = l2 as Element of NAT ; ( locnum (l1,T) <= locnum (l2,T) & locnum (l2,T) <= locnum (l1,T) ) by A1, Th9; hence l1 = l2 by Th7, XXREAL_0:1; ::_thesis: verum end; registration let N be with_zero set ; cluster non empty with_non-empty_values IC-Ins-separated weakly_standard -> non empty with_non-empty_values IC-Ins-separated InsLoc-antisymmetric for AMI-Struct over N; coherence for b1 being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N st b1 is weakly_standard holds b1 is InsLoc-antisymmetric by Th10; end; definition let N be with_zero set ; let S be non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N; let f be Element of NAT ; let k be Nat; funcf + (k,S) -> Element of NAT equals :: AMI_WSTD:def 6 il. (S,((locnum (f,S)) + k)); coherence il. (S,((locnum (f,S)) + k)) is Element of NAT ; end; :: deftheorem defines + AMI_WSTD:def_6_:_ for N being with_zero set for S being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N for f being Element of NAT for k being Nat holds f + (k,S) = il. (S,((locnum (f,S)) + k)); theorem :: AMI_WSTD:11 for N being with_zero set for T being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N for f being Element of NAT holds f + (0,T) = f by Def5; theorem :: AMI_WSTD:12 for z being Nat for N being with_zero set for T being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N for f, g being Element of NAT st f + (z,T) = g + (z,T) holds f = g proof let z be Nat; ::_thesis: for N being with_zero set for T being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N for f, g being Element of NAT st f + (z,T) = g + (z,T) holds f = g let N be with_zero set ; ::_thesis: for T being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N for f, g being Element of NAT st f + (z,T) = g + (z,T) holds f = g let T be non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N; ::_thesis: for f, g being Element of NAT st f + (z,T) = g + (z,T) holds f = g let f, g be Element of NAT ; ::_thesis: ( f + (z,T) = g + (z,T) implies f = g ) assume f + (z,T) = g + (z,T) ; ::_thesis: f = g then (locnum (f,T)) + z = (locnum (g,T)) + z by Th5; hence f = g by Th7; ::_thesis: verum end; theorem :: AMI_WSTD:13 for z being Nat for N being with_zero set for T being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N for f being Element of NAT holds (locnum (f,T)) + z = locnum ((f + (z,T)),T) by Def5; definition let N be with_zero set ; let S be non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N; let f be Element of NAT ; func NextLoc (f,S) -> Element of NAT equals :: AMI_WSTD:def 7 f + (1,S); coherence f + (1,S) is Element of NAT ; end; :: deftheorem defines NextLoc AMI_WSTD:def_7_:_ for N being with_zero set for S being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N for f being Element of NAT holds NextLoc (f,S) = f + (1,S); theorem :: AMI_WSTD:14 for N being with_zero set for T being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N for f being Element of NAT holds NextLoc (f,T) = il. (T,((locnum (f,T)) + 1)) ; theorem Th15: :: AMI_WSTD:15 for N being with_zero set for T being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N for f being Element of NAT holds f <> NextLoc (f,T) proof let N be with_zero set ; ::_thesis: for T being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N for f being Element of NAT holds f <> NextLoc (f,T) let T be non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N; ::_thesis: for f being Element of NAT holds f <> NextLoc (f,T) let f be Element of NAT ; ::_thesis: f <> NextLoc (f,T) assume f = NextLoc (f,T) ; ::_thesis: contradiction then locnum (f,T) = (locnum (f,T)) + 1 by Def5; hence contradiction ; ::_thesis: verum end; theorem :: AMI_WSTD:16 for N being with_zero set for T being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N for f, g being Element of NAT st NextLoc (f,T) = NextLoc (g,T) holds f = g proof let N be with_zero set ; ::_thesis: for T being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N for f, g being Element of NAT st NextLoc (f,T) = NextLoc (g,T) holds f = g let T be non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N; ::_thesis: for f, g being Element of NAT st NextLoc (f,T) = NextLoc (g,T) holds f = g let f, g be Element of NAT ; ::_thesis: ( NextLoc (f,T) = NextLoc (g,T) implies f = g ) assume A1: NextLoc (f,T) = NextLoc (g,T) ; ::_thesis: f = g set m = locnum (g,T); set k = locnum (f,T); (locnum (f,T)) + 0 = ((locnum (f,T)) + 1) - 1 .= ((locnum (g,T)) + 1) - 1 by A1, Th5 .= (locnum (g,T)) + 0 ; hence f = g by Th7; ::_thesis: verum end; theorem Th17: :: AMI_WSTD:17 for z being Nat for N being with_zero set holds il. ((STC N),z) = z proof let z be Nat; ::_thesis: for N being with_zero set holds il. ((STC N),z) = z let N be with_zero set ; ::_thesis: il. ((STC N),z) = z set M = STC N; reconsider f2 = id NAT as Function of NAT,NAT ; consider f being Function of NAT,NAT such that A1: ( f is bijective & ( for m, n being Element of NAT holds ( m <= n iff f . m <= f . n, STC N ) ) ) and A2: il. ((STC N),z) = f . z by Def4; now__::_thesis:_for_k_being_Element_of_NAT_holds_ (_f2_._(k_+_1)_in_SUCC_((f2_._k),(STC_N))_&_(_for_j_being_Element_of_NAT_st_f2_._j_in_SUCC_((f2_._k),(STC_N))_holds_ k_<=_j_)_) let k be Element of NAT ; ::_thesis: ( f2 . (k + 1) in SUCC ((f2 . k),(STC N)) & ( for j being Element of NAT st f2 . j in SUCC ((f2 . k),(STC N)) holds k <= j ) ) reconsider fk = f2 . k as Element of NAT ; A3: SUCC (fk,(STC N)) = {k,(k + 1)} by AMISTD_1:8, FUNCT_1:18; f2 . (k + 1) = k + 1 by FUNCT_1:18; hence f2 . (k + 1) in SUCC ((f2 . k),(STC N)) by A3, TARSKI:def_2; ::_thesis: for j being Element of NAT st f2 . j in SUCC ((f2 . k),(STC N)) holds k <= j let j be Element of NAT ; ::_thesis: ( f2 . j in SUCC ((f2 . k),(STC N)) implies k <= j ) A4: j = f2 . j by FUNCT_1:18; assume f2 . j in SUCC ((f2 . k),(STC N)) ; ::_thesis: k <= j then ( j = k or j = k + 1 ) by A3, A4, TARSKI:def_2; hence k <= j by NAT_1:11; ::_thesis: verum end; then for m, n being Element of NAT holds ( m <= n iff f2 . m <= f2 . n, STC N ) by Th3; then ( z is Element of NAT & f = f2 ) by A1, Th2, ORDINAL1:def_12; hence il. ((STC N),z) = z by A2, FUNCT_1:18; ::_thesis: verum end; theorem :: AMI_WSTD:18 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 IC (Exec (i,s)) = NextLoc ((IC s),(STC N)) 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 IC (Exec (i,s)) = NextLoc ((IC s),(STC N)) let i be Instruction of (STC N); ::_thesis: for s being State of (STC N) st InsCode i = 1 holds IC (Exec (i,s)) = NextLoc ((IC s),(STC N)) let s be State of (STC N); ::_thesis: ( InsCode i = 1 implies IC (Exec (i,s)) = NextLoc ((IC s),(STC N)) ) set M = STC N; set k = locnum ((IC s),(STC N)); reconsider K = IC s as Element of NAT ; assume InsCode i = 1 ; ::_thesis: IC (Exec (i,s)) = NextLoc ((IC s),(STC N)) then A1: IC (Exec (i,s)) = succ (IC s) by Lm2 .= K + 1 ; ( il. ((STC N),(locnum ((IC s),(STC N)))) = locnum ((IC s),(STC N)) & il. ((STC N),((locnum ((IC s),(STC N))) + 1)) = (locnum ((IC s),(STC N))) + 1 ) by Th17; hence IC (Exec (i,s)) = NextLoc ((IC s),(STC N)) by A1, Def5; ::_thesis: verum end; theorem :: AMI_WSTD:19 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) = {(NextLoc (l,(STC N)))} proof let N be with_zero set ; ::_thesis: for l being Element of NAT for i being Element of the InstructionsF of (STC N) st InsCode i = 1 holds NIC (i,l) = {(NextLoc (l,(STC N)))} let l be Element of NAT ; ::_thesis: for i being Element of the InstructionsF of (STC N) st InsCode i = 1 holds NIC (i,l) = {(NextLoc (l,(STC N)))} let i be Element of the InstructionsF of (STC N); ::_thesis: ( InsCode i = 1 implies NIC (i,l) = {(NextLoc (l,(STC N)))} ) assume A1: InsCode i = 1 ; ::_thesis: NIC (i,l) = {(NextLoc (l,(STC N)))} set M = STC N; consider k being Nat such that A2: l = il. ((STC N),k) by Th6; k = locnum (l,(STC N)) by A2, Def5; then NextLoc (l,(STC N)) = k + 1 by Th17; hence NIC (i,l) = {(NextLoc (l,(STC N)))} by A1, A2, Lm3, Th17; ::_thesis: verum end; theorem :: AMI_WSTD:20 for N being with_zero set for l being Element of NAT holds SUCC (l,(STC N)) = {l,(NextLoc (l,(STC N)))} proof let N be with_zero set ; ::_thesis: for l being Element of NAT holds SUCC (l,(STC N)) = {l,(NextLoc (l,(STC N)))} let l be Element of NAT ; ::_thesis: SUCC (l,(STC N)) = {l,(NextLoc (l,(STC N)))} set M = STC N; consider k being Nat such that A1: l = il. ((STC N),k) by Th6; A2: k = locnum (l,(STC N)) by A1, Def5; thus SUCC (l,(STC N)) = {k,(k + 1)} by A1, Th17, AMISTD_1:8 .= {k,(il. ((STC N),(k + 1)))} by Th17 .= {l,(NextLoc (l,(STC N)))} by A1, A2, Th17 ; ::_thesis: verum end; definition let N be with_zero set ; let S be non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N; let i be Instruction of S; attri is sequential means :: AMI_WSTD:def 8 for s being State of S holds (Exec (i,s)) . (IC ) = NextLoc ((IC s),S); end; :: deftheorem defines sequential AMI_WSTD:def_8_:_ for N being with_zero set for S being non empty with_non-empty_values IC-Ins-separated weakly_standard 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 ) = NextLoc ((IC s),S) ); theorem Th21: :: AMI_WSTD:21 for N being with_zero set for S being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N for il being Element of NAT for i being Instruction of S st i is sequential holds NIC (i,il) = {(NextLoc (il,S))} proof let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N for il being Element of NAT for i being Instruction of S st i is sequential holds NIC (i,il) = {(NextLoc (il,S))} let S be non empty with_non-empty_values IC-Ins-separated weakly_standard 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) = {(NextLoc (il,S))} let il be Element of NAT ; ::_thesis: for i being Instruction of S st i is sequential holds NIC (i,il) = {(NextLoc (il,S))} let i be Instruction of S; ::_thesis: ( i is sequential implies NIC (i,il) = {(NextLoc (il,S))} ) assume A1: for s being State of S holds (Exec (i,s)) . (IC ) = NextLoc ((IC s),S) ; :: according to AMI_WSTD:def_8 ::_thesis: NIC (i,il) = {(NextLoc (il,S))} now__::_thesis:_for_x_being_set_holds_ (_x_in_{(NextLoc_(il,S))}_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 {(NextLoc (il,S))} iff x in { (IC (Exec (i,ss))) where ss is Element of product (the_Values_of S) : IC ss = il } ) A2: now__::_thesis:_(_x_=_NextLoc_(il,S)_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 = NextLoc (il,S) ; ::_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)) = NextLoc (il,S) 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_=_NextLoc_(il,S)_) assume x in { (IC (Exec (i,ss))) where ss is Element of product (the_Values_of S) : IC ss = il } ; ::_thesis: x = NextLoc (il,S) then ex s being Element of product (the_Values_of S) st ( x = IC (Exec (i,s)) & IC s = il ) ; hence x = NextLoc (il,S) by A1; ::_thesis: verum end; hence ( x in {(NextLoc (il,S))} 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) = {(NextLoc (il,S))} by TARSKI:1; ::_thesis: verum end; theorem Th22: :: AMI_WSTD:22 for N being with_zero set for S being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N for i being Instruction of S st i is sequential holds not i is halting proof let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N for i being Instruction of S st i is sequential holds not i is halting let S be non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N; ::_thesis: for i being Instruction of S st i is sequential holds not i is halting 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)) = {(NextLoc ((IC the State of S),S))} by A1, Th21; then NIC (i,(IC the State of S)) <> {(IC the State of S)} by Th15, ZFMISC_1:3; hence not i is halting by AMISTD_1:2; ::_thesis: verum end; registration let N be with_zero set ; let S be non empty with_non-empty_values IC-Ins-separated weakly_standard 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 by Th22; 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; begin definition let N be with_zero set ; let S be non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N; let F be NAT -defined the InstructionsF of S -valued Function; attrF is para-closed means :: AMI_WSTD:def 9 for s being State of S st IC s = il. (S,0) holds for k being Element of NAT holds IC (Comput (F,s,k)) in dom F; end; :: deftheorem defines para-closed AMI_WSTD:def_9_:_ for N being with_zero set for S being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N for F being NAT -defined the InstructionsF of b2 -valued Function holds ( F is para-closed iff for s being State of S st IC s = il. (S,0) holds for k being Element of NAT holds IC (Comput (F,s,k)) in dom F ); theorem Th23: :: AMI_WSTD:23 for N being with_zero set for S being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N for F being NAT -defined the InstructionsF of b2 -valued finite Function st F is really-closed & il. (S,0) in dom F holds F is para-closed proof let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N for F being NAT -defined the InstructionsF of b1 -valued finite Function st F is really-closed & il. (S,0) in dom F holds F is para-closed let S be non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N; ::_thesis: for F being NAT -defined the InstructionsF of S -valued finite Function st F is really-closed & il. (S,0) in dom F holds F is para-closed let F be NAT -defined the InstructionsF of S -valued finite Function; ::_thesis: ( F is really-closed & il. (S,0) in dom F implies F is para-closed ) assume F is really-closed ; ::_thesis: ( not il. (S,0) in dom F or F is para-closed ) then A1: 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 by AMISTD_1:14; assume A2: il. (S,0) in dom F ; ::_thesis: F is para-closed let s be State of S; :: according to AMI_WSTD:def_9 ::_thesis: ( IC s = il. (S,0) implies for k being Element of NAT holds IC (Comput (F,s,k)) in dom F ) assume IC s = il. (S,0) ; ::_thesis: for k being Element of NAT holds IC (Comput (F,s,k)) in dom F hence for k being Element of NAT holds IC (Comput (F,s,k)) in dom F by A1, A2; ::_thesis: verum end; theorem Th24: :: AMI_WSTD:24 for N being with_zero set for S being non empty with_non-empty_values IC-Ins-separated halting weakly_standard AMI-Struct over N holds (il. (S,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 weakly_standard AMI-Struct over N holds (il. (S,0)) .--> (halt S) is really-closed let S be non empty with_non-empty_values IC-Ins-separated halting weakly_standard AMI-Struct over N; ::_thesis: (il. (S,0)) .--> (halt S) is really-closed reconsider F = (il. (S,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: ( not l in dom ((il. (S,0)) .--> (halt S)) or NIC ((((il. (S,0)) .--> (halt S)) /. l),l) c= dom ((il. (S,0)) .--> (halt S)) ) assume A1: l in dom ((il. (S,0)) .--> (halt S)) ; ::_thesis: NIC ((((il. (S,0)) .--> (halt S)) /. l),l) c= dom ((il. (S,0)) .--> (halt S)) A2: dom F = {(il. (S,0))} by FUNCOP_1:13; A3: l = il. (S,0) by A1, TARSKI:def_1; F /. l = F . l by A1, PARTFUN1:def_6 .= halt S by A3, FUNCOP_1:72 ; hence NIC ((((il. (S,0)) .--> (halt S)) /. l),l) c= dom ((il. (S,0)) .--> (halt S)) by A2, A3, AMISTD_1:2; ::_thesis: verum 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 F be NAT -defined the InstructionsF of S -valued finite Function; attrF is lower means :Def10: :: AMI_WSTD:def 10 for l being Element of NAT st l in dom F holds for m being Element of NAT st m <= l,S holds m in dom F; end; :: deftheorem Def10 defines lower AMI_WSTD: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 finite Function holds ( F is lower iff for l being Element of NAT st l in dom F holds for m being Element of NAT st m <= l,S holds m in dom F ); registration let N be with_zero set ; let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; cluster Relation-like NAT -defined the InstructionsF of S -valued empty Function-like finite -> NAT -defined the InstructionsF of S -valued finite lower for set ; coherence for b1 being NAT -defined the InstructionsF of S -valued finite Function st b1 is empty holds b1 is lower proof let F be NAT -defined the InstructionsF of S -valued finite Function; ::_thesis: ( F is empty implies F is lower ) assume A1: F is empty ; ::_thesis: F is lower let l be Element of NAT ; :: according to AMI_WSTD:def_10 ::_thesis: ( l in dom F implies for m being Element of NAT st m <= l,S holds m in dom F ) assume l in dom F ; ::_thesis: for m being Element of NAT st m <= l,S holds m in dom F hence for m being Element of NAT st m <= l,S holds m in dom F by A1; ::_thesis: verum end; end; theorem Th25: :: AMI_WSTD:25 for N being with_zero set for T being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N for i being Element of the InstructionsF of T holds (il. (T,0)) .--> i is lower proof let N be with_zero set ; ::_thesis: for T being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N for i being Element of the InstructionsF of T holds (il. (T,0)) .--> i is lower let T be non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N; ::_thesis: for i being Element of the InstructionsF of T holds (il. (T,0)) .--> i is lower let i be Element of the InstructionsF of T; ::_thesis: (il. (T,0)) .--> i is lower set F = (il. (T,0)) .--> i; let l be Element of NAT ; :: according to AMI_WSTD:def_10 ::_thesis: ( l in dom ((il. (T,0)) .--> i) implies for m being Element of NAT st m <= l,T holds m in dom ((il. (T,0)) .--> i) ) assume A1: l in dom ((il. (T,0)) .--> i) ; ::_thesis: for m being Element of NAT st m <= l,T holds m in dom ((il. (T,0)) .--> i) let m be Element of NAT ; ::_thesis: ( m <= l,T implies m in dom ((il. (T,0)) .--> i) ) assume A2: m <= l,T ; ::_thesis: m in dom ((il. (T,0)) .--> i) consider k being Nat such that A3: m = il. (T,k) by Th6; A4: l = il. (T,0) by A1, TARSKI:def_1; then ( 0 <= k & k <= 0 ) by A2, A3, Th8, NAT_1:2; hence m in dom ((il. (T,0)) .--> i) by A1, A4, A3, XXREAL_0:1; ::_thesis: verum end; registration let N be with_zero set ; let S be non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N; cluster Relation-like NAT -defined the InstructionsF of S -valued Function-like finite 1 -element countable V94() lower for set ; existence ex b1 being NAT -defined the InstructionsF of S -valued finite Function st ( b1 is lower & b1 is 1 -element ) proof set i = the Instruction of S; take (il. (S,0)) .--> the Instruction of S ; ::_thesis: ( (il. (S,0)) .--> the Instruction of S is lower & (il. (S,0)) .--> the Instruction of S is 1 -element ) thus ( (il. (S,0)) .--> the Instruction of S is lower & (il. (S,0)) .--> the Instruction of S is 1 -element ) by Th25; ::_thesis: verum end; end; theorem Th26: :: AMI_WSTD:26 for N being with_zero set for T being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N for F being NAT -defined the InstructionsF of b2 -valued non empty finite lower Function holds il. (T,0) in dom F proof let N be with_zero set ; ::_thesis: for T being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N for F being NAT -defined the InstructionsF of b1 -valued non empty finite lower Function holds il. (T,0) in dom F let T be non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N; ::_thesis: for F being NAT -defined the InstructionsF of T -valued non empty finite lower Function holds il. (T,0) in dom F let F be NAT -defined the InstructionsF of T -valued non empty finite lower Function; ::_thesis: il. (T,0) in dom F consider l being set such that A1: l in dom F by XBOOLE_0:def_1; reconsider l = l as Element of NAT by A1; consider f being Function of NAT,NAT such that A2: f is bijective and A3: for m, n being Element of NAT holds ( m <= n iff f . m <= f . n,T ) and A4: il. (T,0) = f . 0 by Def4; rng f = NAT by A2, FUNCT_2:def_3; then consider x being set such that A5: x in dom f and A6: l = f . x by FUNCT_1:def_3; reconsider x = x as Element of NAT by A5; 0 <= x by NAT_1:2; then f . 0 <= f . x,T by A3; hence il. (T,0) in dom F by A1, A4, A6, Def10; ::_thesis: verum end; theorem Th27: :: AMI_WSTD:27 for z being Nat for N being with_zero set for T being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N for P being NAT -defined the InstructionsF of b3 -valued finite lower Function holds ( z < card P iff il. (T,z) in dom P ) proof let z be Nat; ::_thesis: for N being with_zero set for T being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N for P being NAT -defined the InstructionsF of b2 -valued finite lower Function holds ( z < card P iff il. (T,z) in dom P ) let N be with_zero set ; ::_thesis: for T being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N for P being NAT -defined the InstructionsF of b1 -valued finite lower Function holds ( z < card P iff il. (T,z) in dom P ) let T be non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N; ::_thesis: for P being NAT -defined the InstructionsF of T -valued finite lower Function holds ( z < card P iff il. (T,z) in dom P ) let P be NAT -defined the InstructionsF of T -valued finite lower Function; ::_thesis: ( z < card P iff il. (T,z) in dom P ) deffunc H1( Element of NAT ) -> Element of NAT = il. (T,$1); defpred S1[ Element of NAT ] means H1($1) in dom P; set A = { k where k is Element of NAT : S1[k] } ; A1: { k where k is Element of NAT : S1[k] } is Subset of NAT from DOMAIN_1:sch_7(); A2: now__::_thesis:_for_a,_b_being_Element_of_NAT_st_a_in__{__k_where_k_is_Element_of_NAT_:_S1[k]__}__&_b_<_a_holds_ b_in__{__k_where_k_is_Element_of_NAT_:_S1[k]__}_ let a, b be Element of NAT ; ::_thesis: ( a in { k where k is Element of NAT : S1[k] } & b < a implies b in { k where k is Element of NAT : S1[k] } ) assume a in { k where k is Element of NAT : S1[k] } ; ::_thesis: ( b < a implies b in { k where k is Element of NAT : S1[k] } ) then A3: ex l being Element of NAT st ( l = a & il. (T,l) in dom P ) ; assume b < a ; ::_thesis: b in { k where k is Element of NAT : S1[k] } then il. (T,b) <= il. (T,a),T by Th8; then il. (T,b) in dom P by A3, Def10; hence b in { k where k is Element of NAT : S1[k] } ; ::_thesis: verum end; A4: now__::_thesis:_for_x_being_set_st_x_in_dom_P_holds_ ex_n_being_Element_of_NAT_st_x_=_H1(n) let x be set ; ::_thesis: ( x in dom P implies ex n being Element of NAT st x = H1(n) ) assume x in dom P ; ::_thesis: ex n being Element of NAT st x = H1(n) then reconsider l = x as Element of NAT ; consider n being Nat such that A5: l = il. (T,n) by Th6; reconsider n = n as Element of NAT by ORDINAL1:def_12; take n = n; ::_thesis: x = H1(n) thus x = H1(n) by A5; ::_thesis: verum end; reconsider A = { k where k is Element of NAT : S1[k] } as Cardinal by A1, A2, FUNCT_7:20; set A1 = { k where k is Element of NAT : H1(k) in dom P } ; A6: z is Element of NAT by ORDINAL1:def_12; A7: card A = A by CARD_1:def_2; A8: for k1, k2 being Element of NAT st H1(k1) = H1(k2) holds k1 = k2 by Th5; A9: dom P, { k where k is Element of NAT : H1(k) in dom P } are_equipotent from FUNCT_7:sch_3(A4, A8); A10: card z = z by CARD_1:def_2; hereby ::_thesis: ( il. (T,z) in dom P implies z < card P ) assume z < card P ; ::_thesis: il. (T,z) in dom P then card z in card (card P) by NAT_1:41; then z in card (dom P) by A10, CARD_1:62; then z in card A by A9, CARD_1:5; then ex d being Element of NAT st ( d = z & il. (T,d) in dom P ) by A7; hence il. (T,z) in dom P ; ::_thesis: verum end; assume il. (T,z) in dom P ; ::_thesis: z < card P then z in card A by A6, A7; then z in card (dom P) by A9, CARD_1:5; then card z in card (card P) by A10, CARD_1:62; hence z < card P by NAT_1:41; ::_thesis: verum end; definition let N be with_zero set ; let S be non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N; let F be NAT -defined the InstructionsF of S -valued non empty finite Function; func LastLoc F -> Element of NAT means :Def11: :: AMI_WSTD:def 11 ex M being non empty finite natural-membered set st ( M = { (locnum (l,S)) where l is Element of NAT : l in dom F } & it = il. (S,(max M)) ); existence ex b1 being Element of NAT ex M being non empty finite natural-membered set st ( M = { (locnum (l,S)) where l is Element of NAT : l in dom F } & b1 = il. (S,(max M)) ) proof deffunc H1( Element of NAT ) -> Element of NAT = locnum ($1,S); set M = { H1(l) where l is Element of NAT : l in dom F } ; set l = the Element of dom F; reconsider l = the Element of dom F as Element of NAT ; A1: locnum (l,S) in { H1(l) where l is Element of NAT : l in dom F } ; A2: { H1(l) where l is Element of NAT : l in dom F } c= NAT proof let k be set ; :: according to TARSKI:def_3 ::_thesis: ( not k in { H1(l) where l is Element of NAT : l in dom F } or k in NAT ) assume k in { H1(l) where l is Element of NAT : l in dom F } ; ::_thesis: k in NAT then ex l being Element of NAT st ( k = locnum (l,S) & l in dom F ) ; hence k in NAT ; ::_thesis: verum end; A3: dom F is finite ; { H1(l) where l is Element of NAT : l in dom F } is finite from FRAENKEL:sch_21(A3); then reconsider M = { H1(l) where l is Element of NAT : l in dom F } as non empty finite Subset of NAT by A1, A2; take il. (S,(max M)) ; ::_thesis: ex M being non empty finite natural-membered set st ( M = { (locnum (l,S)) where l is Element of NAT : l in dom F } & il. (S,(max M)) = il. (S,(max M)) ) take M ; ::_thesis: ( M = { (locnum (l,S)) where l is Element of NAT : l in dom F } & il. (S,(max M)) = il. (S,(max M)) ) thus ( M = { (locnum (l,S)) where l is Element of NAT : l in dom F } & il. (S,(max M)) = il. (S,(max M)) ) ; ::_thesis: verum end; uniqueness for b1, b2 being Element of NAT st ex M being non empty finite natural-membered set st ( M = { (locnum (l,S)) where l is Element of NAT : l in dom F } & b1 = il. (S,(max M)) ) & ex M being non empty finite natural-membered set st ( M = { (locnum (l,S)) where l is Element of NAT : l in dom F } & b2 = il. (S,(max M)) ) holds b1 = b2 ; end; :: deftheorem Def11 defines LastLoc AMI_WSTD:def_11_:_ for N being with_zero set for S being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N for F being NAT -defined the InstructionsF of b2 -valued non empty finite Function for b4 being Element of NAT holds ( b4 = LastLoc F iff ex M being non empty finite natural-membered set st ( M = { (locnum (l,S)) where l is Element of NAT : l in dom F } & b4 = il. (S,(max M)) ) ); theorem Th28: :: AMI_WSTD:28 for N being with_zero set for T being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N for F being NAT -defined the InstructionsF of b2 -valued non empty finite Function holds LastLoc F in dom F proof let N be with_zero set ; ::_thesis: for T being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N for F being NAT -defined the InstructionsF of b1 -valued non empty finite Function holds LastLoc F in dom F let T be non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N; ::_thesis: for F being NAT -defined the InstructionsF of T -valued non empty finite Function holds LastLoc F in dom F let F be NAT -defined the InstructionsF of T -valued non empty finite Function; ::_thesis: LastLoc F in dom F consider M being non empty finite natural-membered set such that A1: M = { (locnum (l,T)) where l is Element of NAT : l in dom F } and A2: LastLoc F = il. (T,(max M)) by Def11; max M in M by XXREAL_2:def_8; then ex l being Element of NAT st ( max M = locnum (l,T) & l in dom F ) by A1; hence LastLoc F in dom F by A2, Def5; ::_thesis: verum end; theorem :: AMI_WSTD:29 for N being with_zero set for T being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N for F, G being NAT -defined the InstructionsF of b2 -valued non empty finite Function st F c= G holds LastLoc F <= LastLoc G,T proof let N be with_zero set ; ::_thesis: for T being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N for F, G being NAT -defined the InstructionsF of b1 -valued non empty finite Function st F c= G holds LastLoc F <= LastLoc G,T let T be non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N; ::_thesis: for F, G being NAT -defined the InstructionsF of T -valued non empty finite Function st F c= G holds LastLoc F <= LastLoc G,T let F, G be NAT -defined the InstructionsF of T -valued non empty finite Function; ::_thesis: ( F c= G implies LastLoc F <= LastLoc G,T ) assume A1: F c= G ; ::_thesis: LastLoc F <= LastLoc G,T consider N being non empty finite natural-membered set such that A2: N = { (locnum (l,T)) where l is Element of NAT : l in dom G } and A3: LastLoc G = il. (T,(max N)) by Def11; consider M being non empty finite natural-membered set such that A4: M = { (locnum (l,T)) where l is Element of NAT : l in dom F } and A5: LastLoc F = il. (T,(max M)) by Def11; reconsider MM = M, NN = N as non empty finite Subset of REAL by MEMBERED:3; M c= N proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in M or a in N ) assume a in M ; ::_thesis: a in N then A6: ex l being Element of NAT st ( a = locnum (l,T) & l in dom F ) by A4; dom F c= dom G by A1, GRFUNC_1:2; hence a in N by A2, A6; ::_thesis: verum end; then max MM <= max NN by XXREAL_2:59; hence LastLoc F <= LastLoc G,T by A5, A3, Th8; ::_thesis: verum end; theorem Th30: :: AMI_WSTD:30 for N being with_zero set for T being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N for F being NAT -defined the InstructionsF of b2 -valued non empty finite Function for l being Element of NAT st l in dom F holds l <= LastLoc F,T proof let N be with_zero set ; ::_thesis: for T being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N for F being NAT -defined the InstructionsF of b1 -valued non empty finite Function for l being Element of NAT st l in dom F holds l <= LastLoc F,T let T be non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N; ::_thesis: for F being NAT -defined the InstructionsF of T -valued non empty finite Function for l being Element of NAT st l in dom F holds l <= LastLoc F,T let F be NAT -defined the InstructionsF of T -valued non empty finite Function; ::_thesis: for l being Element of NAT st l in dom F holds l <= LastLoc F,T let l be Element of NAT ; ::_thesis: ( l in dom F implies l <= LastLoc F,T ) assume A1: l in dom F ; ::_thesis: l <= LastLoc F,T consider M being non empty finite natural-membered set such that A2: M = { (locnum (w,T)) where w is Element of NAT : w in dom F } and A3: LastLoc F = il. (T,(max M)) by Def11; locnum (l,T) in M by A1, A2; then A4: locnum (l,T) <= max M by XXREAL_2:def_8; locnum ((LastLoc F),T) = max M by A3, Def5; hence l <= LastLoc F,T by A4, Th9; ::_thesis: verum end; theorem :: AMI_WSTD:31 for N being with_zero set for T being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N for F being NAT -defined the InstructionsF of b2 -valued non empty finite lower Function for G being NAT -defined the InstructionsF of b2 -valued non empty finite Function st F c= G & LastLoc F = LastLoc G holds F = G proof let N be with_zero set ; ::_thesis: for T being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N for F being NAT -defined the InstructionsF of b1 -valued non empty finite lower Function for G being NAT -defined the InstructionsF of b1 -valued non empty finite Function st F c= G & LastLoc F = LastLoc G holds F = G let T be non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N; ::_thesis: for F being NAT -defined the InstructionsF of T -valued non empty finite lower Function for G being NAT -defined the InstructionsF of T -valued non empty finite Function st F c= G & LastLoc F = LastLoc G holds F = G let F be NAT -defined the InstructionsF of T -valued non empty finite lower Function; ::_thesis: for G being NAT -defined the InstructionsF of T -valued non empty finite Function st F c= G & LastLoc F = LastLoc G holds F = G let G be NAT -defined the InstructionsF of T -valued non empty finite Function; ::_thesis: ( F c= G & LastLoc F = LastLoc G implies F = G ) assume that A1: F c= G and A2: LastLoc F = LastLoc G ; ::_thesis: F = G dom F = dom G proof thus dom F c= dom G by A1, GRFUNC_1:2; :: according to XBOOLE_0:def_10 ::_thesis: dom G c= dom F let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom G or x in dom F ) assume A3: x in dom G ; ::_thesis: x in dom F reconsider x = x as Element of NAT by A3; A4: LastLoc F in dom F by Th28; x <= LastLoc F,T by A2, A3, Th30; hence x in dom F by A4, Def10; ::_thesis: verum end; hence F = G by A1, GRFUNC_1:3; ::_thesis: verum end; theorem Th32: :: AMI_WSTD:32 for N being with_zero set for T being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N for F being NAT -defined the InstructionsF of b2 -valued non empty finite lower Function holds LastLoc F = il. (T,((card F) -' 1)) proof let N be with_zero set ; ::_thesis: for T being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N for F being NAT -defined the InstructionsF of b1 -valued non empty finite lower Function holds LastLoc F = il. (T,((card F) -' 1)) let T be non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N; ::_thesis: for F being NAT -defined the InstructionsF of T -valued non empty finite lower Function holds LastLoc F = il. (T,((card F) -' 1)) let F be NAT -defined the InstructionsF of T -valued non empty finite lower Function; ::_thesis: LastLoc F = il. (T,((card F) -' 1)) consider k being Nat such that A1: LastLoc F = il. (T,k) by Th6; reconsider k = k as Element of NAT by ORDINAL1:def_12; LastLoc F in dom F by Th28; then k < card F by A1, Th27; then A2: k <= (card F) -' 1 by NAT_D:49; percases ( k < (card F) -' 1 or k = (card F) -' 1 ) by A2, XXREAL_0:1; suppose k < (card F) -' 1 ; ::_thesis: LastLoc F = il. (T,((card F) -' 1)) then k + 1 < ((card F) -' 1) + 1 by XREAL_1:6; then k + 1 < card F by NAT_1:14, XREAL_1:235; then il. (T,(k + 1)) in dom F by Th27; then il. (T,(k + 1)) <= LastLoc F,T by Th30; then A3: k + 1 <= k by A1, Th8; k <= k + 1 by NAT_1:11; then k + 0 = k + 1 by A3, XXREAL_0:1; hence LastLoc F = il. (T,((card F) -' 1)) ; ::_thesis: verum end; suppose k = (card F) -' 1 ; ::_thesis: LastLoc F = il. (T,((card F) -' 1)) hence LastLoc F = il. (T,((card F) -' 1)) by A1; ::_thesis: verum end; end; end; registration let N be with_zero set ; let S be non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N; cluster Relation-like NAT -defined the InstructionsF of S -valued non empty Function-like finite really-closed lower -> NAT -defined the InstructionsF of S -valued finite para-closed for set ; coherence for b1 being NAT -defined the InstructionsF of S -valued finite Function st b1 is really-closed & b1 is lower & not b1 is empty holds b1 is para-closed proof let F be NAT -defined the InstructionsF of S -valued finite Function; ::_thesis: ( F is really-closed & F is lower & not F is empty implies F is para-closed ) assume A1: F is really-closed ; ::_thesis: ( not F is lower or F is empty or F is para-closed ) assume ( F is lower & not F is empty ) ; ::_thesis: F is para-closed then il. (S,0) in dom F by Th26; hence F is para-closed by A1, Th23; ::_thesis: verum end; end; Lm4: now__::_thesis:_for_N_being_with_zero_set_ for_S_being_non_empty_with_non-empty_values_IC-Ins-separated_halting_weakly_standard_AMI-Struct_over_N_holds_ (_((il._(S,0))_.-->_(halt_S))_._(LastLoc_((il._(S,0))_.-->_(halt_S)))_=_halt_S_&_(_for_l_being_Element_of_NAT_st_((il._(S,0))_.-->_(halt_S))_._l_=_halt_S_&_l_in_dom_((il._(S,0))_.-->_(halt_S))_holds_ l_=_LastLoc_((il._(S,0))_.-->_(halt_S))_)_) let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated halting weakly_standard AMI-Struct over N holds ( ((il. (S,0)) .--> (halt S)) . (LastLoc ((il. (S,0)) .--> (halt S))) = halt S & ( for l being Element of NAT st ((il. (S,0)) .--> (halt S)) . l = halt S & l in dom ((il. (S,0)) .--> (halt S)) holds l = LastLoc ((il. (S,0)) .--> (halt S)) ) ) let S be non empty with_non-empty_values IC-Ins-separated halting weakly_standard AMI-Struct over N; ::_thesis: ( ((il. (S,0)) .--> (halt S)) . (LastLoc ((il. (S,0)) .--> (halt S))) = halt S & ( for l being Element of NAT st ((il. (S,0)) .--> (halt S)) . l = halt S & l in dom ((il. (S,0)) .--> (halt S)) holds l = LastLoc ((il. (S,0)) .--> (halt S)) ) ) set F = (il. (S,0)) .--> (halt S); dom ((il. (S,0)) .--> (halt S)) = {(il. (S,0))} by FUNCOP_1:13; then A1: card (dom ((il. (S,0)) .--> (halt S))) = 1 by CARD_1:30; (il. (S,0)) .--> (halt S) is NAT -defined the InstructionsF of S -valued finite lower Function by Th25; then A2: LastLoc ((il. (S,0)) .--> (halt S)) = il. (S,((card ((il. (S,0)) .--> (halt S))) -' 1)) by Th32 .= il. (S,((card (dom ((il. (S,0)) .--> (halt S)))) -' 1)) by CARD_1:62 .= il. (S,0) by A1, XREAL_1:232 ; hence ((il. (S,0)) .--> (halt S)) . (LastLoc ((il. (S,0)) .--> (halt S))) = halt S by FUNCOP_1:72; ::_thesis: for l being Element of NAT st ((il. (S,0)) .--> (halt S)) . l = halt S & l in dom ((il. (S,0)) .--> (halt S)) holds l = LastLoc ((il. (S,0)) .--> (halt S)) let l be Element of NAT ; ::_thesis: ( ((il. (S,0)) .--> (halt S)) . l = halt S & l in dom ((il. (S,0)) .--> (halt S)) implies l = LastLoc ((il. (S,0)) .--> (halt S)) ) assume ((il. (S,0)) .--> (halt S)) . l = halt S ; ::_thesis: ( l in dom ((il. (S,0)) .--> (halt S)) implies l = LastLoc ((il. (S,0)) .--> (halt S)) ) assume l in dom ((il. (S,0)) .--> (halt S)) ; ::_thesis: l = LastLoc ((il. (S,0)) .--> (halt S)) hence l = LastLoc ((il. (S,0)) .--> (halt S)) by A2, TARSKI:def_1; ::_thesis: verum end; definition let N be with_zero set ; let S be non empty with_non-empty_values IC-Ins-separated halting weakly_standard AMI-Struct over N; let F be NAT -defined the InstructionsF of S -valued non empty finite Function; attrF is halt-ending means :Def12: :: AMI_WSTD:def 12 F . (LastLoc F) = halt S; attrF is unique-halt means :Def13: :: AMI_WSTD:def 13 for f being Element of NAT st F . f = halt S & f in dom F holds f = LastLoc F; end; :: deftheorem Def12 defines halt-ending AMI_WSTD:def_12_:_ for N being with_zero set for S being non empty with_non-empty_values IC-Ins-separated halting weakly_standard AMI-Struct over N for F being NAT -defined the InstructionsF of b2 -valued non empty finite Function holds ( F is halt-ending iff F . (LastLoc F) = halt S ); :: deftheorem Def13 defines unique-halt AMI_WSTD:def_13_:_ for N being with_zero set for S being non empty with_non-empty_values IC-Ins-separated halting weakly_standard AMI-Struct over N for F being NAT -defined the InstructionsF of b2 -valued non empty finite Function holds ( F is unique-halt iff for f being Element of NAT st F . f = halt S & f in dom F holds f = LastLoc F ); registration let N be with_zero set ; let S be non empty with_non-empty_values IC-Ins-separated halting weakly_standard AMI-Struct over N; cluster Relation-like NAT -defined the InstructionsF of S -valued non empty trivial Function-like finite countable V94() lower halt-ending unique-halt for set ; existence ex b1 being NAT -defined the InstructionsF of S -valued non empty finite lower Function st ( b1 is halt-ending & b1 is unique-halt & b1 is trivial ) proof reconsider F = (il. (S,0)) .--> (halt S) as NAT -defined the InstructionsF of S -valued non empty finite lower Function by Th25; take F ; ::_thesis: ( F is halt-ending & F is unique-halt & F is trivial ) thus F . (LastLoc F) = halt S by Lm4; :: according to AMI_WSTD:def_12 ::_thesis: ( F is unique-halt & F is trivial ) thus for f being Element of NAT st F . f = halt S & f in dom F holds f = LastLoc F by Lm4; :: according to AMI_WSTD:def_13 ::_thesis: F is trivial thus F is trivial ; ::_thesis: verum end; end; registration let N be with_zero set ; let S be non empty with_non-empty_values IC-Ins-separated halting weakly_standard AMI-Struct over N; cluster Relation-like NAT -defined the InstructionsF of S -valued non empty trivial Function-like finite countable V94() really-closed lower 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 lower & not b1 is empty ) proof reconsider F = (il. (S,0)) .--> (halt S) as NAT -defined the InstructionsF of S -valued non empty finite lower Function by Th25; take F ; ::_thesis: ( F is trivial & F is really-closed & F is lower & not F is empty ) thus ( F is trivial & F is really-closed & F is lower & not F is empty ) by Th24; ::_thesis: verum end; end; registration let N be with_zero set ; let S be non empty with_non-empty_values IC-Ins-separated halting weakly_standard AMI-Struct over N; cluster Relation-like NAT -defined the InstructionsF of S -valued non empty trivial Function-like finite countable V94() really-closed lower halt-ending unique-halt for set ; existence ex b1 being NAT -defined the InstructionsF of S -valued non empty finite lower Function st ( b1 is halt-ending & b1 is unique-halt & b1 is trivial & b1 is really-closed ) proof reconsider F = (il. (S,0)) .--> (halt S) as NAT -defined the InstructionsF of S -valued non empty finite lower Function by Th25; 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 Lm4; :: according to AMI_WSTD:def_12 ::_thesis: ( F is unique-halt & F is trivial & F is really-closed ) thus for f being Element of NAT st F . f = halt S & f in dom F holds f = LastLoc F by Lm4; :: according to AMI_WSTD:def_13 ::_thesis: ( F is trivial & F is really-closed ) thus ( F is trivial & F is really-closed ) by Th24; ::_thesis: verum end; end; definition let N be with_zero set ; let S be non empty with_non-empty_values IC-Ins-separated halting weakly_standard AMI-Struct over N; mode pre-Macro of S is NAT -defined the InstructionsF of S -valued non empty finite lower halt-ending unique-halt Function; end; registration let N be with_zero set ; let S be non empty with_non-empty_values IC-Ins-separated halting weakly_standard AMI-Struct over N; cluster Relation-like NAT -defined the InstructionsF of S -valued non empty Function-like finite countable V94() really-closed lower halt-ending unique-halt for set ; existence ex b1 being pre-Macro of S st b1 is really-closed proof reconsider F = (il. (S,0)) .--> (halt S) as NAT -defined the InstructionsF of S -valued non empty finite lower Function by Th25; ( 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 Lm4; then reconsider F = F as pre-Macro of S by Def12, Def13; take F ; ::_thesis: F is really-closed thus F is really-closed by Th24; ::_thesis: verum end; end; theorem :: AMI_WSTD:33 for N being with_zero set for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N for l1, l2 being Element of NAT st SUCC (l1,S) = NAT holds l1 <= l2,S 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 l1, l2 being Element of NAT st SUCC (l1,S) = NAT holds l1 <= l2,S let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; ::_thesis: for l1, l2 being Element of NAT st SUCC (l1,S) = NAT holds l1 <= l2,S let l1, l2 be Element of NAT ; ::_thesis: ( SUCC (l1,S) = NAT implies l1 <= l2,S ) assume A1: SUCC (l1,S) = NAT ; ::_thesis: l1 <= l2,S defpred S1[ set , set ] means ( ( $1 = 1 implies $2 = l1 ) & ( $1 = 2 implies $2 = l2 ) ); A2: for n being Nat st n in Seg 2 holds ex d being Element of NAT st S1[n,d] proof let n be Nat; ::_thesis: ( n in Seg 2 implies ex d being Element of NAT st S1[n,d] ) assume A3: n in Seg 2 ; ::_thesis: ex d being Element of NAT st S1[n,d] percases ( n = 1 or n = 2 ) by A3, FINSEQ_1:2, TARSKI:def_2; supposeA4: n = 1 ; ::_thesis: ex d being Element of NAT st S1[n,d] reconsider l1 = l1 as Element of NAT ; take l1 ; ::_thesis: S1[n,l1] thus S1[n,l1] by A4; ::_thesis: verum end; supposeA5: n = 2 ; ::_thesis: ex d being Element of NAT st S1[n,d] reconsider l2 = l2 as Element of NAT ; take l2 ; ::_thesis: S1[n,l2] thus S1[n,l2] by A5; ::_thesis: verum end; end; end; consider f being FinSequence of NAT such that A6: len f = 2 and A7: for n being Nat st n in Seg 2 holds S1[n,f /. n] from FINSEQ_4:sch_1(A2); A8: 1 in Seg 2 by FINSEQ_1:2, TARSKI:def_2; then A9: f /. 1 = l1 by A7; reconsider f = f as non empty FinSequence of NAT by A6; take f ; :: according to AMI_WSTD:def_1 ::_thesis: ( f /. 1 = l1 & f /. (len f) = l2 & ( for n being Element of NAT st 1 <= n & n < len f holds f /. (n + 1) in SUCC ((f /. n),S) ) ) 2 in Seg 2 by FINSEQ_1:2, TARSKI:def_2; hence ( f /. 1 = l1 & f /. (len f) = l2 ) by A6, A7, A8; ::_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 A10: 1 <= n ; ::_thesis: ( not n < len f or f /. (n + 1) in SUCC ((f /. n),S) ) assume n < len f ; ::_thesis: f /. (n + 1) in SUCC ((f /. n),S) then n < 1 + 1 by A6; then n <= 1 by NAT_1:13; then n = 1 by A10, XXREAL_0:1; hence f /. (n + 1) in SUCC ((f /. n),S) by A1, A9; ::_thesis: verum end; definition let N be with_zero set ; let S be non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N; let loc be Element of NAT ; let k be Nat; funcloc -' (k,S) -> Element of NAT equals :: AMI_WSTD:def 14 il. (S,((locnum (loc,S)) -' k)); coherence il. (S,((locnum (loc,S)) -' k)) is Element of NAT ; end; :: deftheorem defines -' AMI_WSTD:def_14_:_ for N being with_zero set for S being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N for loc being Element of NAT for k being Nat holds loc -' (k,S) = il. (S,((locnum (loc,S)) -' k)); theorem :: AMI_WSTD:34 for N being with_zero set for S being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N for l being Element of NAT holds l -' (0,S) = l proof let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N for l being Element of NAT holds l -' (0,S) = l let S be non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N; ::_thesis: for l being Element of NAT holds l -' (0,S) = l let l be Element of NAT ; ::_thesis: l -' (0,S) = l thus l -' (0,S) = il. (S,(locnum (l,S))) by NAT_D:40 .= l by Def5 ; ::_thesis: verum end; theorem :: AMI_WSTD:35 for k being Nat for N being with_zero set for S being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N for l being Element of NAT holds (l + (k,S)) -' (k,S) = l proof let k be Nat; ::_thesis: for N being with_zero set for S being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N for l being Element of NAT holds (l + (k,S)) -' (k,S) = l let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N for l being Element of NAT holds (l + (k,S)) -' (k,S) = l let S be non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N; ::_thesis: for l being Element of NAT holds (l + (k,S)) -' (k,S) = l let l be Element of NAT ; ::_thesis: (l + (k,S)) -' (k,S) = l thus (l + (k,S)) -' (k,S) = il. (S,(((locnum (l,S)) + k) -' k)) by Def5 .= il. (S,(locnum (l,S))) by NAT_D:34 .= l by Def5 ; ::_thesis: verum end;