let N be non empty with_non-empty_elements set ; :: thesis:
set D = TrivialInfiniteTree ;
let S be non empty stored-program halting IC-Ins-separated steady-programmed definite realistic standard AMI-Struct of 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₂[ Element of NAT ] means (dom (ExecTree (Stop S))) -level $1 = TrivialInfiniteTree -level $1;
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: 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 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:

end;

A5: 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 set ; :: thesis:
assume s in succ f ; :: thesis:
then consider k being Element of NAT such that
A15: s = f ^ <*k*> and
A16: k in card (NIC (pi (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:

end;

let s be set ; :: 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 A13, A12; :: 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:14;
then f ^ <*a*> = f ^ <*0 *> by A14, TARSKI:def 1;
then (ExecTree (Stop S)) . (f ^ <*a*>) = (LocSeq (NIC (pi (Stop S),((ExecTree (Stop S)) . f)),((ExecTree (Stop S)) . f)),S) . 0 by A12, Def5
.= il. S,0 by A12, A10, Def4 ;
hence S₁[f ^ <*a*>] by A2, TARSKI:def 1; :: thesis:

end;

(ExecTree (Stop S)) . {} = FirstLoc (Stop S) by Def5;
then A17: S₁[ <*> NAT ] by Th21;
A18: for f being Element of dom (ExecTree (Stop S)) holds S₁[f] from HILBERT2:sch 1(A17, A5);
A19: 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:
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 A18;
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 ; :: thesis:

end;

A20: for n being Element of NAT st S₂[n] holds
S₂[n + 1]

proof

let n be Element of NAT ; :: thesis:
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: 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 set ; :: thesis:
assume s in succ t0 ; :: thesis:
then consider k being Element of NAT such that
A31: s = t0 ^ <*k*> and
A32: k in card (NIC (pi (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:

end;

let s be set ; :: 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 A26, A29; :: thesis:

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, Th20;
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 A36: k in Seg (n + 1) by A25, FINSEQ_1:3;

now

per cases by A36, FINSEQ_2:8;

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

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:

end;

suppose k = n + 1 ; :: thesis:

hence t1 . k = 0 by A33, FINSEQ_2:20; :: thesis:

end;

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

end;

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

end;

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

proof

end;

A41: S₃[ 0 ] by TREES_1:47;
for n being Element of NAT holds S₃[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:
then a = (n + 1) |-> 0 by TARSKI:def 1;
hence a in (dom (ExecTree (Stop S))) -level (n + 1) by A21, A22, A42; :: thesis:

end;

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

end;

(dom (ExecTree (Stop S))) -level 0 = {{} } by QC_LANG4:17
.= TrivialInfiniteTree -level 0 by QC_LANG4:17 ;
then A43: S₂[ 0 ] ;
for x being Element of NAT holds S₂[x] from NAT_1:sch 1(A43, A20);
then dom (ExecTree (Stop S)) = TrivialInfiniteTree by Th18;
hence ExecTree (Stop S) = TrivialInfiniteTree --> (il. S,0 ) by A19, FUNCOP_1:17; :: thesis: