let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty IC-Ins-separated halting standard AMI-Struct of N holds ExecTree (Stop S) = TrivialInfiniteTree --> 0
set D = TrivialInfiniteTree ;
let S be non empty IC-Ins-separated 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 10;
then A2: dom (Stop S) = {0} by FUNCOP_1:13;
A3: (Stop S) . 0 = halt S by A1, FUNCOP_1:72;
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:2;
hence card (NIC ((halt S),((ExecTree (Stop S)) . t))) = {0} by CARD_1:30, CARD_1:49; :: 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 6;
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:2;
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:38;
then A9: (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:72
.= 0 by A2, A6, TARSKI:def 1 ;
A10: card (NIC ((halt S),((ExecTree (Stop S)) . f))) = {0} by A4;
then A11: 0 in card (NIC (((Stop S) /. ((ExecTree (Stop S)) . f)),((ExecTree (Stop S)) . f))) by A3, A8, A7, TARSKI:def 1;
A12: 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 Def4;
A13: 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
A14: s = f ^ <*k*> and
A15: k in card (NIC (((Stop S) /. ((ExecTree (Stop S)) . f)),((ExecTree (Stop S)) . f))) by A12;
k = 0 by A3, A10, A8, A7, A15, TARSKI:def 1;
hence s in {(f ^ <*0*>)} by A14, 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 A12, A11; :: 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:12;
then f ^ <*a*> = f ^ <*0*> by A13, TARSKI:def 1;
then (ExecTree (Stop S)) . (f ^ <*a*>) = (LocSeq ((NIC (((Stop S) /. ((ExecTree (Stop S)) . f)),((ExecTree (Stop S)) . f))),S)) . 0 by A11, Def4
.= 0 by A11, A9, Def3 ;
hence S1[f ^ <*a*>] by A2, TARSKI:def 1; :: thesis: verum
end;
(ExecTree (Stop S)) . {} = FirstLoc (Stop S) by Def4;
then A16: S1[ <*> NAT] by VALUED_1:33;
A17: for f being Element of dom (ExecTree (Stop S)) holds S1[f] from HILBERT2:sch 1(A16, A5);
 A18: 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 A17;
then (ExecTree (Stop S)) . x in {0} by A2;
hence (ExecTree (Stop S)) . x = 0 by TARSKI:def 1; :: thesis: verum
end;
A19: 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;
A20: (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;
A21: len ((n + 1) |-> 0) = n + 1 by CARD_1:def 7;
assume A22: 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
A23: a = t1 and
A24: len t1 = n + 1 by A20;
reconsider t0 = t1 | (Seg n) as Element of dom (ExecTree (Stop S)) by RELAT_1:59, TREES_1:20;
A25: 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 Def4;
(ExecTree (Stop S)) . t0 in dom (Stop S) by A17;
then A26: (ExecTree (Stop S)) . t0 = 0 by A2, TARSKI:def 1;
A27: ( card (NIC ((halt S),((ExecTree (Stop S)) . t0))) = {0} & (Stop S) /. ((ExecTree (Stop S)) . t0) = (Stop S) . ((ExecTree (Stop S)) . t0) ) by A4, A17, PARTFUN1:def 6;
then A28: 0 in card (NIC (((Stop S) /. ((ExecTree (Stop S)) . t0)),((ExecTree (Stop S)) . t0))) by A3, A26, TARSKI:def 1;
A29: 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
A30: s = t0 ^ <*k*> and
A31: k in card (NIC (((Stop S) /. ((ExecTree (Stop S)) . t0)),((ExecTree (Stop S)) . t0))) by A25;
k = 0 by A3, A26, A27, A31, TARSKI:def 1;
hence s in {(t0 ^ <*0*>)} by A30, 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 A25, A28; :: thesis: verum
end;
( t1 . (n + 1) is Element of NAT & t1 = t0 ^ <*(t1 . (n + 1))*> ) by A24, FINSEQ_3:55, ORDINAL1:def 12;
then t0 ^ <*(t1 . (n + 1))*> in succ t0 by TREES_2:12;
then A32: t0 ^ <*(t1 . (n + 1))*> = t0 ^ <*0*> by A29, TARSKI:def 1;
n <= n + 1 by NAT_1:11;
then Seg n c= Seg (n + 1) by FINSEQ_1:5;
then Seg n c= dom t1 by A24, FINSEQ_1:def 3;
then dom t0 = Seg n by RELAT_1:62;
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 A33: t0 in (dom (ExecTree (Stop S))) -level n ;
A34: (dom (ExecTree (Stop S))) -level n = {(n |-> 0)} by A22, TREES_2:39;
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 A35: k in Seg (n + 1) by A24, FINSEQ_1:1;
now
per cases ( k in Seg n or k = n + 1 ) by A35, FINSEQ_2:7;
suppose A36: k in Seg n ; :: thesis: t1 . k = 0
hence t1 . k = t0 . k by FUNCT_1:49
.= (n |-> 0) . k by A34, A33, TARSKI:def 1
.= 0 by A36, FUNCOP_1:7 ;
:: thesis: verum
end;
suppose k = n + 1 ; :: thesis: t1 . k = 0
hence t1 . k = 0 by A32, FINSEQ_2:17; :: thesis: verum
end;
end;
end;
hence t1 . k = ((n + 1) |-> 0) . k by A35, FUNCOP_1:7; :: thesis: verum
end;
then t1 = (n + 1) |-> 0 by A21, A24, FINSEQ_1:14;
hence a in {((n + 1) |-> 0)} by A23, 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) )
A37: 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)) ;
A38: 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 Def4;
(ExecTree (Stop S)) . t in dom (Stop S) by A17;
then A39: (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, A17, PARTFUN1:def 6;
then 0 in card (NIC (((Stop S) /. ((ExecTree (Stop S)) . t)),((ExecTree (Stop S)) . t))) by A3, A39, TARSKI:def 1;
then t ^ <*0*> in succ t by A38;
then t ^ <*0*> in dom (ExecTree (Stop S)) ;
hence S3[n + 1] by FINSEQ_2:60; :: thesis: verum
end;
A40: S3[ 0 ] by TREES_1:22;
for n being Element of NAT holds S3[n] from NAT_1:sch 1(A40, A37);
 then A41: (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 A20, A21, A41; :: thesis: verum
end;
hence S2[n + 1] by TREES_2:39; :: thesis: verum
end;
(dom (ExecTree (Stop S))) -level 0 = {{}} by TREES_9:44
.= TrivialInfiniteTree -level 0 by TREES_9:44 ;
then A42: S2[ 0 ] ;
for x being Element of NAT holds S2[x] from NAT_1:sch 1(A42, A19);
 then dom (ExecTree (Stop S)) = TrivialInfiniteTree by TREES_2:38;
hence ExecTree (Stop S) = TrivialInfiniteTree --> 0 by A18, FUNCOP_1:11; :: thesis: verum