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