let N be with_zero set ; :: thesis:
set D = TrivialInfiniteTree ;
let S be non empty with_non-empty_values IC-Ins-separated halting standard AMI-Struct over N; :: thesis:
set M = Stop S;
set E = ExecTree (Stop S);
defpred S₁[ set ] means (ExecTree (Stop S)) . $1 in dom (Stop S);
defpred S₂[ Nat] means (dom (ExecTree (Stop S))) -level $1 = TrivialInfiniteTree -level $1;
A2: (Stop S) . 0 = halt S by FUNCOP_1:72;
A3: 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:
reconsider Et = (ExecTree (Stop S)) . t as 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:

end;

A4: for f being Element of dom (ExecTree (Stop S)) st S₁[f] holds
for a being Element of NAT st f ^ <*a*> in dom (ExecTree (Stop S)) holds
S₁[f ^ <*a*>]

proof

proof

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis:

let s be object ; :: thesis:
assume s in succ f ; :: thesis:
then consider k being Nat such that
A13: s = f ^ <*k*> and
A14: k in card (NIC (((Stop S) /. ((ExecTree (Stop S)) . f)),((ExecTree (Stop S)) . f))) by A11;
k = 0 by A2, A9, A7, A6, A14, TARSKI:def 1;
hence s in {(f ^ <*0*>)} by A13, TARSKI:def 1; :: thesis:

end;

let s be object ; :: according to TARSKI:def 3 :: thesis:
assume s in {(f ^ <*0*>)} ; :: thesis:
then s = f ^ <*0*> by TARSKI:def 1;
hence s in succ f by A11, A10; :: thesis:

end;

let a be Element of NAT ; :: thesis:
assume f ^ <*a*> in dom (ExecTree (Stop S)) ; :: thesis:
then f ^ <*a*> in succ f by TREES_2:12;
then f ^ <*a*> = f ^ <*0*> by A12, TARSKI:def 1;
then (ExecTree (Stop S)) . (f ^ <*a*>) = (LocSeq ((NIC (((Stop S) /. ((ExecTree (Stop S)) . f)),((ExecTree (Stop S)) . f))),S)) . 0 by A10, Def2
.= 0 by A10, A8, Def1 ;
hence S₁[f ^ <*a*>] by TARSKI:def 1; :: thesis:

end;

(ExecTree (Stop S)) . {} = FirstLoc (Stop S) by Def2;
then A15: S₁[ <*> NAT] by VALUED_1:33;
A16: for f being Element of dom (ExecTree (Stop S)) holds S₁[f] from HILBERT2:sch 1(A15, A4);
A17: for x being object st x in dom (ExecTree (Stop S)) holds
(ExecTree (Stop S)) . x = 0

proof

let x be object ; :: thesis:
assume x in dom (ExecTree (Stop S)) ; :: thesis:
then reconsider x = x as Element of dom (ExecTree (Stop S)) ;
(ExecTree (Stop S)) . x in dom (Stop S) by A16;
hence (ExecTree (Stop S)) . x = 0 by TARSKI:def 1; :: thesis:

end;

A18: for n being Nat st S₂[n] holds
S₂[n + 1]

proof

let n be Nat; :: thesis:
set f0 = n |-> 0;
set f1 = (n + 1) |-> 0;
A19: (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;
A20: len ((n + 1) |-> 0) = n + 1 by CARD_1:def 7;
assume A21: S₂[n] ; :: thesis:
(dom (ExecTree (Stop S))) -level (n + 1) = {((n + 1) |-> 0)}

proof

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis:

proof

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis:

let s be object ; :: thesis:
assume s in succ t0 ; :: thesis:
then consider k being Nat such that
A29: s = t0 ^ <*k*> and
A30: k in card (NIC (((Stop S) /. ((ExecTree (Stop S)) . t0)),((ExecTree (Stop S)) . t0))) by A24;
k = 0 by A2, A25, A26, A30, TARSKI:def 1;
hence s in {(t0 ^ <*0*>)} by A29, TARSKI:def 1; :: thesis:

end;

let s be object ; :: according to TARSKI:def 3 :: thesis:
assume s in {(t0 ^ <*0*>)} ; :: thesis:
then s = t0 ^ <*0*> by TARSKI:def 1;
hence s in succ t0 by A24, A27; :: thesis:

end;

( t1 . (n + 1) is Nat & t1 = t0 ^ <*(t1 . (n + 1))*> ) by A23, FINSEQ_3:55;
then t0 ^ <*(t1 . (n + 1))*> in succ t0 by TREES_2:12;
then A31: t0 ^ <*(t1 . (n + 1))*> = t0 ^ <*0*> by A28, TARSKI:def 1;
A32: n in NAT by ORDINAL1:def 12;
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 A23, 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, A32;
then A33: t0 in (dom (ExecTree (Stop S))) -level n ;
A34: (dom (ExecTree (Stop S))) -level n = {(n |-> 0)} by A21, 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:
assume ( 1 <= k & k <= len t1 ) ; :: thesis:
then A35: k in Seg (n + 1) by A23, FINSEQ_1:1;

now :: thesis:

per cases by A35, FINSEQ_2:7;

suppose A36: k in Seg n ; :: thesis:

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:

end;

suppose k = n + 1 ; :: thesis:

hence t1 . k = 0 by A31, FINSEQ_2:17; :: thesis:

end;

hence t1 . k = ((n + 1) |-> 0) . k by A35, FUNCOP_1:7; :: thesis:

end;

then t1 = (n + 1) |-> 0 by A20, A23, FINSEQ_1:14;
hence a in {((n + 1) |-> 0)} by A22, TARSKI:def 1; :: thesis:

end;

defpred S₃[ Nat] means $1 |-> 0 in dom (ExecTree (Stop S));
let a be object ; :: according to TARSKI:def 3 :: thesis:
A37: for n being Nat st S₃[n] holds
S₃[n + 1]

proof

end;

A40: S₃[ 0 ] by TREES_1:22;
for n being Nat holds S₃[n] from NAT_1:sch 2(A40, A37);
then A41: (n + 1) |-> 0 is Element of dom (ExecTree (Stop S)) ;
assume a in {((n + 1) |-> 0)} ; :: thesis:
then a = (n + 1) |-> 0 by TARSKI:def 1;
hence a in (dom (ExecTree (Stop S))) -level (n + 1) by A19, A20, A41; :: thesis:

end;

hence S₂[n + 1] by TREES_2:39; :: thesis:

end;

(dom (ExecTree (Stop S))) -level 0 = {{}} by TREES_9:44
.= TrivialInfiniteTree -level 0 by TREES_9:44 ;
then A42: S₂[ 0 ] ;
for x being Nat holds S₂[x] from NAT_1:sch 2(A42, A18);
then dom (ExecTree (Stop S)) = TrivialInfiniteTree by TREES_2:38;
hence ExecTree (Stop S) = TrivialInfiniteTree --> 0 by A17, FUNCOP_1:11; :: thesis: