let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite realistic halting standard AMI-Struct of N holds ExecTree (Stop S) = TrivialInfiniteTree --> 0
set D = TrivialInfiniteTree ;
let S be non empty stored-program IC-Ins-separated definite realistic halting standard AMI-Struct of N; :: thesis: ExecTree (Stop S) = TrivialInfiniteTree --> 0
set M = Stop S;
set E = ExecTree (Stop S);
defpred S1[ set ] means (ExecTree (Stop S)) . $1 in dom (Stop S);
defpred S2[ Element of NAT ] means (dom (ExecTree (Stop S))) -level $1 = TrivialInfiniteTree -level $1;
A1: Stop S = <%(halt S)%> by COMPOS_1:def 27;
then A2: dom (Stop S) = {0} by FUNCOP_1:19;
A3: (Stop S) . 0 = halt S by A1, FUNCOP_1:87;
A4: 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}
reconsider Et = (ExecTree (Stop S)) . t as Element of NAT ;
NIC ((halt S),Et) = {Et} by AMISTD_1:15;
hence card (NIC ((halt S),((ExecTree (Stop S)) . t))) = {0} by CARD_1:50, CARD_1:87; :: thesis: verum
end;
A5: 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 A6: S1[f] ; :: thesis: for a being Element of NAT st f ^ <*a*> in dom (ExecTree (Stop S)) holds
S1[f ^ <*a*>]
A7: (Stop S) /. ((ExecTree (Stop S)) . f) = (Stop S) . ((ExecTree (Stop S)) . f) by A6, PARTFUN1:def 8;
reconsider Ef = (ExecTree (Stop S)) . f as Element of NAT ;
A8: (ExecTree (Stop S)) . f = 0 by A2, A6, TARSKI:def 1;
then NIC ((halt S),((ExecTree (Stop S)) . f)) = {0} by AMISTD_1:15;
then canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl (NIC (((Stop S) /. ((ExecTree (Stop S)) . f)),((ExecTree (Stop S)) . f)))))),(RelIncl (NIC (((Stop S) /. ((ExecTree (Stop S)) . f)),((ExecTree (Stop S)) . f))))) = 0 .--> Ef by A3, A8, A7, CARD_5:50;
then A10: (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl (NIC (((Stop S) /. ((ExecTree (Stop S)) . f)),((ExecTree (Stop S)) . f)))))),(RelIncl (NIC (((Stop S) /. ((ExecTree (Stop S)) . f)),((ExecTree (Stop S)) . f)))))) . 0 = Ef by FUNCOP_1:87
.= 0 by A2, A6, TARSKI:def 1 ;
A11: card (NIC ((halt S),((ExecTree (Stop S)) . f))) = {0} by A4;
then A12: 0 in card (NIC (((Stop S) /. ((ExecTree (Stop S)) . f)),((ExecTree (Stop S)) . f))) by A3, A8, A7, TARSKI:def 1;
A13: succ f = { (f ^ <*k*>) where k is Element of NAT : k in card (NIC (((Stop S) /. ((ExecTree (Stop S)) . f)),((ExecTree (Stop S)) . f))) } by Def5;
A14: 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
A15: s = f ^ <*k*> and
A16: k in card (NIC (((Stop S) /. ((ExecTree (Stop S)) . f)),((ExecTree (Stop S)) . f))) by A13;
k = 0 by A3, A11, A8, A7, A16, TARSKI:def 1;
hence s in {(f ^ <*0*>)} by A15, 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 A13, A12; :: thesis: verum
end;
let a be Element of NAT ; :: thesis: ( f ^ <*a*> in dom (ExecTree (Stop S)) implies S1[f ^ <*a*>] )
assume f ^ <*a*> in dom (ExecTree (Stop S)) ; :: thesis: S1[f ^ <*a*>]
then f ^ <*a*> in succ f by TREES_2:14;
then f ^ <*a*> = f ^ <*0*> by A14, TARSKI:def 1;
then (ExecTree (Stop S)) . (f ^ <*a*>) = (LocSeq ((NIC (((Stop S) /. ((ExecTree (Stop S)) . f)),((ExecTree (Stop S)) . f))),S)) . 0 by A12, Def5
.= 0 by A12, A10, Def4 ;
hence S1[f ^ <*a*>] by A2, TARSKI:def 1; :: thesis: verum
end;
(ExecTree (Stop S)) . {} = FirstLoc (Stop S) by Def5;
then A17: S1[ <*> NAT] by VALUED_1:34;
A18: for f being Element of dom (ExecTree (Stop S)) holds S1[f] from HILBERT2:sch 1(A17, A5);
 A19: for x being set st x in dom (ExecTree (Stop S)) holds
(ExecTree (Stop S)) . x = 0
proof
let x be set ; :: thesis: ( x in dom (ExecTree (Stop S)) implies (ExecTree (Stop S)) . x = 0 )
assume x in dom (ExecTree (Stop S)) ; :: thesis: (ExecTree (Stop S)) . x = 0
then reconsider x = x as Element of dom (ExecTree (Stop S)) ;
(ExecTree (Stop S)) . x in dom (Stop S) by A18;
then (ExecTree (Stop S)) . x in {0} by A2;
hence (ExecTree (Stop S)) . x = 0 by TARSKI:def 1; :: thesis: verum
end;
A20: 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] )
set f0 = n |-> 0;
set f1 = (n + 1) |-> 0;
A21: (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;
A22: len ((n + 1) |-> 0) = n + 1 by FINSEQ_1:def 18;
assume A23: S2[n] ; :: thesis: S2[n + 1]
(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
A24: a = t1 and
A25: len t1 = n + 1 by A21;
reconsider t0 = t1 | (Seg n) as Element of dom (ExecTree (Stop S)) by RELAT_1:88, TREES_1:45;
A26: succ t0 = { (t0 ^ <*k*>) where k is Element of NAT : k in card (NIC (((Stop S) /. ((ExecTree (Stop S)) . t0)),((ExecTree (Stop S)) . t0))) } by Def5;
(ExecTree (Stop S)) . t0 in dom (Stop S) by A18;
then A27: (ExecTree (Stop S)) . t0 = 0 by A2, TARSKI:def 1;
A28: ( card (NIC ((halt S),((ExecTree (Stop S)) . t0))) = {0} & (Stop S) /. ((ExecTree (Stop S)) . t0) = (Stop S) . ((ExecTree (Stop S)) . t0) ) by A4, A18, PARTFUN1:def 8;
then A29: 0 in card (NIC (((Stop S) /. ((ExecTree (Stop S)) . t0)),((ExecTree (Stop S)) . t0))) by A3, A27, TARSKI:def 1;
A30: 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
A31: s = t0 ^ <*k*> and
A32: k in card (NIC (((Stop S) /. ((ExecTree (Stop S)) . t0)),((ExecTree (Stop S)) . t0))) by A26;
k = 0 by A3, A27, A28, A32, TARSKI:def 1;
hence s in {(t0 ^ <*0*>)} by A31, 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 A26, A29; :: thesis: verum
end;
( t1 . (n + 1) is Element of NAT & t1 = t0 ^ <*(t1 . (n + 1))*> ) by A25, FINSEQ_3:61, ORDINAL1:def 13;
then t0 ^ <*(t1 . (n + 1))*> in succ t0 by TREES_2:14;
then A33: t0 ^ <*(t1 . (n + 1))*> = t0 ^ <*0*> by A30, TARSKI:def 1;
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 A25, FINSEQ_1:def 3;
then dom t0 = Seg n by RELAT_1:91;
then ( (dom (ExecTree (Stop S))) -level n = { w where w is Element of dom (ExecTree (Stop S)) : len w = n } & len t0 = n ) by FINSEQ_1:def 3, TREES_2:def 6;
then A34: t0 in (dom (ExecTree (Stop S))) -level n ;
A35: (dom (ExecTree (Stop S))) -level n = {(n |-> 0)} by A23, TREES_2:41;
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 ( 1 <= k & k <= len t1 ) ; :: thesis: t1 . k = ((n + 1) |-> 0) . k
then A36: k in Seg (n + 1) by A25, FINSEQ_1:3;
now
per cases ( k in Seg n or k = n + 1 ) by A36, FINSEQ_2:8;
suppose A37: k in Seg n ; :: thesis: t1 . k = 0
hence t1 . k = t0 . k by FUNCT_1:72
.= (n |-> 0) . k by A35, A34, TARSKI:def 1
.= 0 by A37, FUNCOP_1:13 ;
:: thesis: verum
end;
suppose k = n + 1 ; :: thesis: t1 . k = 0
hence t1 . k = 0 by A33, FINSEQ_2:20; :: thesis: verum
end;
end;
end;
hence t1 . k = ((n + 1) |-> 0) . k by A36, FUNCOP_1:13; :: thesis: verum
end;
then t1 = (n + 1) |-> 0 by A22, A25, FINSEQ_1:18;
hence a in {((n + 1) |-> 0)} by A24, TARSKI:def 1; :: thesis: verum
end;
defpred S3[ Element of NAT ] means $1 |-> 0 in dom (ExecTree (Stop S));
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) )
A38: 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)) ;
A39: succ t = { (t ^ <*k*>) where k is Element of NAT : k in card (NIC (((Stop S) /. ((ExecTree (Stop S)) . t)),((ExecTree (Stop S)) . t))) } by Def5;
(ExecTree (Stop S)) . t in dom (Stop S) by A18;
then A40: (ExecTree (Stop S)) . t = 0 by A2, TARSKI:def 1;
( card (NIC ((halt S),((ExecTree (Stop S)) . t))) = {0} & (Stop S) /. ((ExecTree (Stop S)) . t) = (Stop S) . ((ExecTree (Stop S)) . t) ) by A4, A18, PARTFUN1:def 8;
then 0 in card (NIC (((Stop S) /. ((ExecTree (Stop S)) . t)),((ExecTree (Stop S)) . t))) by A3, A40, TARSKI:def 1;
then t ^ <*0*> in succ t by A39;
then t ^ <*0*> in dom (ExecTree (Stop S)) ;
hence S3[n + 1] by FINSEQ_2:74; :: thesis: verum
end;
A41: S3[ 0 ] by TREES_1:47;
for n being Element of NAT holds S3[n] from NAT_1:sch 1(A41, A38);
 then A42: (n + 1) |-> 0 is Element of dom (ExecTree (Stop S)) ;
assume a in {((n + 1) |-> 0)} ; :: thesis: a in (dom (ExecTree (Stop S))) -level (n + 1)
then a = (n + 1) |-> 0 by TARSKI:def 1;
hence a in (dom (ExecTree (Stop S))) -level (n + 1) by A21, A22, A42; :: thesis: verum
end;
hence S2[n + 1] by TREES_2:41; :: thesis: verum
end;
(dom (ExecTree (Stop S))) -level 0 = {{}} by TREES_9:45
.= TrivialInfiniteTree -level 0 by TREES_9:45 ;
then A43: S2[ 0 ] ;
for x being Element of NAT holds S2[x] from NAT_1:sch 1(A43, A20);
 then dom (ExecTree (Stop S)) = TrivialInfiniteTree by TREES_2:40;
hence ExecTree (Stop S) = TrivialInfiniteTree --> 0 by A19, FUNCOP_1:17; :: thesis: verum