let N be with_non-empty_elements set ; :: thesis: for S being non empty stored-program halting IC-Ins-separated definite realistic standard AMI-Struct of NAT ,N holds ExecTree (Stop S) = TrivialInfiniteTree --> (il. S,0 )
let S be non empty stored-program halting IC-Ins-separated definite realistic standard AMI-Struct of NAT ,N; :: thesis: ExecTree (Stop S) = TrivialInfiniteTree --> (il. S,0 )
set D = TrivialInfiniteTree ;
set M = Stop S;
set E = ExecTree (Stop S);
A1: Stop S = (il. S,0 ) .--> (halt S) by AMISTD_2:def 13;
then A2: dom (Stop S) = {(il. S,0 )} by FUNCOP_1:19;
A3: (Stop S) . (il. S,0 ) = halt S by A1, FUNCOP_1:87;
A4: (ExecTree (Stop S)) . {} = FirstLoc (Stop S) by Def5;
A5: for t being Element of dom (ExecTree (Stop S)) holds card (NIC (halt S),((ExecTree (Stop S)) . t)) = {0 }
proof
let t be Element of dom (ExecTree (Stop S)); :: thesis: card (NIC (halt S),((ExecTree (Stop S)) . t)) = {0 }
NIC (halt S),((ExecTree (Stop S)) . t) = {((ExecTree (Stop S)) . t)} by AMISTD_1:15;
hence card (NIC (halt S),((ExecTree (Stop S)) . t)) = {0 } by CARD_1:50, CARD_1:87; :: thesis: verum
end;
defpred S1[ set ] means (ExecTree (Stop S)) . $1 in dom (Stop S);
A6: S1[ <*> NAT ] by A4, Th21;
A7: for f being Element of dom (ExecTree (Stop S)) st S1[f] holds
for a being Element of NAT st f ^ <*a*> in dom (ExecTree (Stop S)) holds
S1[f ^ <*a*>]
proof
let f be Element of dom (ExecTree (Stop S)); :: thesis: ( S1[f] implies for a being Element of NAT st f ^ <*a*> in dom (ExecTree (Stop S)) holds
S1[f ^ <*a*>] )
assume A8: S1[f] ; :: thesis: for a being Element of NAT st f ^ <*a*> in dom (ExecTree (Stop S)) holds
S1[f ^ <*a*>]
let a be Element of NAT ; :: thesis: ( f ^ <*a*> in dom (ExecTree (Stop S)) implies S1[f ^ <*a*>] )
assume A9: f ^ <*a*> in dom (ExecTree (Stop S)) ; :: thesis: S1[f ^ <*a*>]
A10: card (NIC (halt S),((ExecTree (Stop S)) . f)) = {0 } by A5;
A11: succ f = { (f ^ <*k*>) where k is Element of NAT : k in card (NIC (pi (Stop S),((ExecTree (Stop S)) . f)),((ExecTree (Stop S)) . f)) } by Def5;
A12: (ExecTree (Stop S)) . f = il. S,0 by A2, A8, TARSKI:def 1;
then A13: locnum ((ExecTree (Stop S)) . f) = 0 by AMISTD_1:def 13;
A14: pi (Stop S),((ExecTree (Stop S)) . f) = (Stop S) . ((ExecTree (Stop S)) . f) by A8, AMI_1:def 47;
then A15: 0 in card (NIC (pi (Stop S),((ExecTree (Stop S)) . f)),((ExecTree (Stop S)) . f)) by A3, A10, A12, TARSKI:def 1;
A16: succ f = {(f ^ <*0 *>)}
proof
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: {(f ^ <*0 *>)} c= succ f
let s be set ; :: thesis: ( s in succ f implies s in {(f ^ <*0 *>)} )
assume s in succ f ; :: thesis: s in {(f ^ <*0 *>)}
then consider k being Element of NAT such that
A17: s = f ^ <*k*> and
A18: k in card (NIC (pi (Stop S),((ExecTree (Stop S)) . f)),((ExecTree (Stop S)) . f)) by A11;
k = 0 by A3, A10, A12, A14, A18, TARSKI:def 1;
hence s in {(f ^ <*0 *>)} by A17, TARSKI:def 1; :: thesis: verum
end;
let s be set ; :: according to TARSKI:def 3 :: thesis: ( not s in {(f ^ <*0 *>)} or s in succ f )
assume s in {(f ^ <*0 *>)} ; :: thesis: s in succ f
then s = f ^ <*0 *> by TARSKI:def 1;
hence s in succ f by A11, A15; :: thesis: verum
end;
f ^ <*a*> in succ f by A9, TREES_2:14;
then A19: f ^ <*a*> = f ^ <*0 *> by A16, TARSKI:def 1;
LocNums (NIC (halt S),((ExecTree (Stop S)) . f)) = {0 } by A13, Th29;
then canonical_isomorphism_of (RelIncl (order_type_of (RelIncl (LocNums (NIC (pi (Stop S),((ExecTree (Stop S)) . f)),((ExecTree (Stop S)) . f)))))),(RelIncl (LocNums (NIC (pi (Stop S),((ExecTree (Stop S)) . f)),((ExecTree (Stop S)) . f)))) = 0 .--> (locnum ((ExecTree (Stop S)) . f)) by A3, A12, A13, A14, Th15;
then A20: (canonical_isomorphism_of (RelIncl (order_type_of (RelIncl (LocNums (NIC (pi (Stop S),((ExecTree (Stop S)) . f)),((ExecTree (Stop S)) . f)))))),(RelIncl (LocNums (NIC (pi (Stop S),((ExecTree (Stop S)) . f)),((ExecTree (Stop S)) . f))))) . 0 = locnum ((ExecTree (Stop S)) . f) by FUNCOP_1:87
.= 0 by A12, AMISTD_1:def 13 ;
(ExecTree (Stop S)) . (f ^ <*a*>) = (LocSeq (NIC (pi (Stop S),((ExecTree (Stop S)) . f)),((ExecTree (Stop S)) . f))) . 0 by A15, A19, Def5
.= il. S,0 by A15, A20, Def4 ;
hence S1[f ^ <*a*>] by A2, TARSKI:def 1; :: thesis: verum
end;
A21: for f being Element of dom (ExecTree (Stop S)) holds S1[f] from HILBERT2:sch 1(A6, A7);
 defpred S2[ Element of NAT ] means (dom (ExecTree (Stop S))) -level $1 = TrivialInfiniteTree -level $1;
A22: S2[ 0 ]
proof
thus (dom (ExecTree (Stop S))) -level 0 = {{} } by QC_LANG4:17
.= TrivialInfiniteTree -level 0 by QC_LANG4:17 ; :: thesis: verum
end;
A23: for n being Element of NAT st S2[n] holds
S2[n + 1]
proof
let n be Element of NAT ; :: thesis: ( S2[n] implies S2[n + 1] )
assume A24: S2[n] ; :: thesis: S2[n + 1]
set f0 = n |-> 0 ;
set f1 = (n + 1) |-> 0 ;
A25: (dom (ExecTree (Stop S))) -level (n + 1) = { w where w is Element of dom (ExecTree (Stop S)) : len w = n + 1 } by TREES_2:def 6;
A26: len ((n + 1) |-> 0 ) = n + 1 by FINSEQ_2:69;
(dom (ExecTree (Stop S))) -level (n + 1) = {((n + 1) |-> 0 )}
proof
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: {((n + 1) |-> 0 )} c= (dom (ExecTree (Stop S))) -level (n + 1)
let a be set ; :: thesis: ( a in (dom (ExecTree (Stop S))) -level (n + 1) implies a in {((n + 1) |-> 0 )} )
assume a in (dom (ExecTree (Stop S))) -level (n + 1) ; :: thesis: a in {((n + 1) |-> 0 )}
then consider t1 being Element of dom (ExecTree (Stop S)) such that
A27: a = t1 and
A28: len t1 = n + 1 by A25;
reconsider t0 = t1 | (Seg n) as Element of dom (ExecTree (Stop S)) by RELAT_1:88, TREES_1:45;
A29: (dom (ExecTree (Stop S))) -level n = { w where w is Element of dom (ExecTree (Stop S)) : len w = n } by TREES_2:def 6;
A30: succ t0 = { (t0 ^ <*k*>) where k is Element of NAT : k in card (NIC (pi (Stop S),((ExecTree (Stop S)) . t0)),((ExecTree (Stop S)) . t0)) } by Def5;
A31: card (NIC (halt S),((ExecTree (Stop S)) . t0)) = {0 } by A5;
(ExecTree (Stop S)) . t0 in dom (Stop S) by A21;
then A32: (ExecTree (Stop S)) . t0 = il. S,0 by A2, TARSKI:def 1;
A33: pi (Stop S),((ExecTree (Stop S)) . t0) = (Stop S) . ((ExecTree (Stop S)) . t0) by A21, AMI_1:def 47;
then A34: 0 in card (NIC (pi (Stop S),((ExecTree (Stop S)) . t0)),((ExecTree (Stop S)) . t0)) by A3, A31, A32, TARSKI:def 1;
A35: t1 . (n + 1) is Element of NAT by ORDINAL1:def 13;
A36: (dom (ExecTree (Stop S))) -level n = {(n |-> 0 )} by A24, Th20;
n <= n + 1 by NAT_1:11;
then Seg n c= Seg (n + 1) by FINSEQ_1:7;
then Seg n c= dom t1 by A28, FINSEQ_1:def 3;
then dom t0 = Seg n by RELAT_1:91;
then len t0 = n by FINSEQ_1:def 3;
then A37: t0 in (dom (ExecTree (Stop S))) -level n by A29;
t1 = t0 ^ <*(t1 . (n + 1))*> by A28, FINSEQ_3:61;
then A38: t0 ^ <*(t1 . (n + 1))*> in succ t0 by A35, TREES_2:14;
succ t0 = {(t0 ^ <*0 *>)}
proof
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: {(t0 ^ <*0 *>)} c= succ t0
let s be set ; :: thesis: ( s in succ t0 implies s in {(t0 ^ <*0 *>)} )
assume s in succ t0 ; :: thesis: s in {(t0 ^ <*0 *>)}
then consider k being Element of NAT such that
A39: s = t0 ^ <*k*> and
A40: k in card (NIC (pi (Stop S),((ExecTree (Stop S)) . t0)),((ExecTree (Stop S)) . t0)) by A30;
k = 0 by A3, A31, A32, A33, A40, TARSKI:def 1;
hence s in {(t0 ^ <*0 *>)} by A39, TARSKI:def 1; :: thesis: verum
end;
let s be set ; :: according to TARSKI:def 3 :: thesis: ( not s in {(t0 ^ <*0 *>)} or s in succ t0 )
assume s in {(t0 ^ <*0 *>)} ; :: thesis: s in succ t0
then s = t0 ^ <*0 *> by TARSKI:def 1;
hence s in succ t0 by A30, A34; :: thesis: verum
end;
then A41: t0 ^ <*(t1 . (n + 1))*> = t0 ^ <*0 *> by A38, TARSKI:def 1;
for k being Nat st 1 <= k & k <= len t1 holds
t1 . k = ((n + 1) |-> 0 ) . k
proof
let k be Nat; :: thesis: ( 1 <= k & k <= len t1 implies t1 . k = ((n + 1) |-> 0 ) . k )
assume A42: ( 1 <= k & k <= len t1 ) ; :: thesis: t1 . k = ((n + 1) |-> 0 ) . k
A43: k in Seg (n + 1) by A28, A42, FINSEQ_1:3;
now
per cases ( k in Seg n or k = n + 1 ) by A43, FINSEQ_2:8;
suppose A44: k in Seg n ; :: thesis: t1 . k = 0
hence t1 . k = t0 . k by FUNCT_1:72
.= (n |-> 0 ) . k by A36, A37, TARSKI:def 1
.= 0 by A44, FUNCOP_1:13 ;
:: thesis: verum
end;
suppose k = n + 1 ; :: thesis: t1 . k = 0
hence t1 . k = 0 by A41, FINSEQ_2:20; :: thesis: verum
end;
end;
end;
hence t1 . k = ((n + 1) |-> 0 ) . k by A43, FUNCOP_1:13; :: thesis: verum
end;
then t1 = (n + 1) |-> 0 by A26, A28, FINSEQ_1:18;
hence a in {((n + 1) |-> 0 )} by A27, TARSKI:def 1; :: thesis: verum
end;
let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in {((n + 1) |-> 0 )} or a in (dom (ExecTree (Stop S))) -level (n + 1) )
assume a in {((n + 1) |-> 0 )} ; :: thesis: a in (dom (ExecTree (Stop S))) -level (n + 1)
then A45: a = (n + 1) |-> 0 by TARSKI:def 1;
defpred S3[ Element of NAT ] means $1 |-> 0 in dom (ExecTree (Stop S));
A46: S3[ 0 ] by TREES_1:47;
A47: for n being Element of NAT st S3[n] holds
S3[n + 1]
proof
let n be Element of NAT ; :: thesis: ( S3[n] implies S3[n + 1] )
assume S3[n] ; :: thesis: S3[n + 1]
then reconsider t = n |-> 0 as Element of dom (ExecTree (Stop S)) ;
A48: succ t = { (t ^ <*k*>) where k is Element of NAT : k in card (NIC (pi (Stop S),((ExecTree (Stop S)) . t)),((ExecTree (Stop S)) . t)) } by Def5;
A49: card (NIC (halt S),((ExecTree (Stop S)) . t)) = {0 } by A5;
(ExecTree (Stop S)) . t in dom (Stop S) by A21;
then A50: (ExecTree (Stop S)) . t = il. S,0 by A2, TARSKI:def 1;
pi (Stop S),((ExecTree (Stop S)) . t) = (Stop S) . ((ExecTree (Stop S)) . t) by A21, AMI_1:def 47;
then 0 in card (NIC (pi (Stop S),((ExecTree (Stop S)) . t)),((ExecTree (Stop S)) . t)) by A3, A49, A50, TARSKI:def 1;
then t ^ <*0 *> in succ t by A48;
then t ^ <*0 *> in dom (ExecTree (Stop S)) ;
hence S3[n + 1] by FINSEQ_2:74; :: thesis: verum
end;
for n being Element of NAT holds S3[n] from NAT_1:sch 1(A46, A47);
 then (n + 1) |-> 0 is Element of dom (ExecTree (Stop S)) ;
hence a in (dom (ExecTree (Stop S))) -level (n + 1) by A25, A26, A45; :: thesis: verum
end;
hence S2[n + 1] by Th20; :: thesis: verum
end;
for x being Element of NAT holds S2[x] from NAT_1:sch 1(A22, A23);
 then A51: dom (ExecTree (Stop S)) = TrivialInfiniteTree by Th18;
for x being set st x in dom (ExecTree (Stop S)) holds
(ExecTree (Stop S)) . x = il. S,0
proof
let x be set ; :: thesis: ( x in dom (ExecTree (Stop S)) implies (ExecTree (Stop S)) . x = il. S,0 )
assume x in dom (ExecTree (Stop S)) ; :: thesis: (ExecTree (Stop S)) . x = il. S,0
then reconsider x = x as Element of dom (ExecTree (Stop S)) ;
(ExecTree (Stop S)) . x in dom (Stop S) by A21;
then (ExecTree (Stop S)) . x in {(il. S,0 )} by A1, FUNCOP_1:19;
then (ExecTree (Stop S)) . x = il. S,0 by TARSKI:def 1;
hence (ExecTree (Stop S)) . x = il. S,0 by AMI_1:def 38; :: thesis: verum
end;
hence ExecTree (Stop S) = TrivialInfiniteTree --> (il. S,0 ) by A51, FUNCOP_1:17; :: thesis: verum