:: 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;