let N be with_zero set ; :: thesis: for S being non empty with_non-empty_values IC-Ins-separated halting standard AMI-Struct over N holds ExecTree (Stop S) = TrivialInfiniteTree --> 0

set D = TrivialInfiniteTree ;

let S be non empty with_non-empty_values IC-Ins-separated halting standard AMI-Struct over N; :: thesis: ExecTree (Stop S) = TrivialInfiniteTree --> 0

set M = Stop S;

set E = ExecTree (Stop S);

defpred S_{1}[ set ] means (ExecTree (Stop S)) . $1 in dom (Stop S);

defpred S_{2}[ 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}_{1}[f] holds

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

S_{1}[f ^ <*a*>]

then A15: S_{1}[ <*> NAT]
by VALUED_1:33;

A16: for f being Element of dom (ExecTree (Stop S)) holds S_{1}[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_{2}[n] holds

S_{2}[n + 1]

.= TrivialInfiniteTree -level 0 by TREES_9:44 ;

then A42: S_{2}[ 0 ]
;

for x being Nat holds S_{2}[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: verum

set D = TrivialInfiniteTree ;

let S be non empty with_non-empty_values IC-Ins-separated halting standard AMI-Struct over N; :: thesis: ExecTree (Stop S) = TrivialInfiniteTree --> 0

set M = Stop S;

set E = ExecTree (Stop S);

defpred S

defpred S

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

A4:
for f being Element of dom (ExecTree (Stop S)) st S
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 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;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: verum

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

S

proof

(ExecTree (Stop S)) . {} = FirstLoc (Stop S)
by Def2;
let f be Element of dom (ExecTree (Stop S)); :: thesis: ( S_{1}[f] implies for a being Element of NAT st f ^ <*a*> in dom (ExecTree (Stop S)) holds

S_{1}[f ^ <*a*>] )

assume A5: S_{1}[f]
; :: thesis: for a being Element of NAT st f ^ <*a*> in dom (ExecTree (Stop S)) holds

S_{1}[f ^ <*a*>]

A6: (Stop S) /. ((ExecTree (Stop S)) . f) = (Stop S) . ((ExecTree (Stop S)) . f) by A5, PARTFUN1:def 6;

reconsider Ef = (ExecTree (Stop S)) . f as Nat ;

A7: (ExecTree (Stop S)) . f = 0 by A5, 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 A2, A7, A6, CARD_5:38;

then A8: (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 A5, TARSKI:def 1 ;

A9: card (NIC ((halt S),((ExecTree (Stop S)) . f))) = {0} by A3;

then A10: 0 in card (NIC (((Stop S) /. ((ExecTree (Stop S)) . f)),((ExecTree (Stop S)) . f))) by A2, A7, A6, TARSKI:def 1;

A11: succ f = { (f ^ <*k*>) where k is Nat : k in card (NIC (((Stop S) /. ((ExecTree (Stop S)) . f)),((ExecTree (Stop S)) . f))) } by Def2;

A12: succ f = {(f ^ <*0*>)}_{1}[f ^ <*a*>] )

assume f ^ <*a*> in dom (ExecTree (Stop S)) ; :: thesis: S_{1}[f ^ <*a*>]

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_{1}[f ^ <*a*>]
by TARSKI:def 1; :: thesis: verum

end;S

assume A5: S

S

A6: (Stop S) /. ((ExecTree (Stop S)) . f) = (Stop S) . ((ExecTree (Stop S)) . f) by A5, PARTFUN1:def 6;

reconsider Ef = (ExecTree (Stop S)) . f as Nat ;

A7: (ExecTree (Stop S)) . f = 0 by A5, 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 A2, A7, A6, CARD_5:38;

then A8: (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 A5, TARSKI:def 1 ;

A9: card (NIC ((halt S),((ExecTree (Stop S)) . f))) = {0} by A3;

then A10: 0 in card (NIC (((Stop S) /. ((ExecTree (Stop S)) . f)),((ExecTree (Stop S)) . f))) by A2, A7, A6, TARSKI:def 1;

A11: succ f = { (f ^ <*k*>) where k is Nat : k in card (NIC (((Stop S) /. ((ExecTree (Stop S)) . f)),((ExecTree (Stop S)) . f))) } by Def2;

A12: succ f = {(f ^ <*0*>)}

proof

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, A10; :: thesis: verum

end;

let a be Element of NAT ; :: thesis: ( f ^ <*a*> in dom (ExecTree (Stop S)) implies Shereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: {(f ^ <*0*>)} c= succ f

let s be object ; :: according to TARSKI:def 3 :: thesis: ( not s in {(f ^ <*0*>)} or s in succ f )let s be object ; :: thesis: ( s in succ f implies s in {(f ^ <*0*>)} )

assume s in succ f ; :: thesis: s in {(f ^ <*0*>)}

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: verum

end;assume s in succ f ; :: thesis: s in {(f ^ <*0*>)}

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: verum

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, A10; :: thesis: verum

assume f ^ <*a*> in dom (ExecTree (Stop S)) ; :: thesis: S

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

then A15: S

A16: for f being Element of dom (ExecTree (Stop S)) holds S

A17: for x being object st x in dom (ExecTree (Stop S)) holds

(ExecTree (Stop S)) . x = 0

proof

A18:
for n being Nat st S
let x be object ; :: 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 A16;

hence (ExecTree (Stop S)) . x = 0 by TARSKI:def 1; :: thesis: verum

end;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 A16;

hence (ExecTree (Stop S)) . x = 0 by TARSKI:def 1; :: thesis: verum

S

proof

(dom (ExecTree (Stop S))) -level 0 =
{{}}
by TREES_9:44
let n be Nat; :: thesis: ( S_{2}[n] implies S_{2}[n + 1] )

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_{2}[n]
; :: thesis: S_{2}[n + 1]

(dom (ExecTree (Stop S))) -level (n + 1) = {((n + 1) |-> 0)}_{2}[n + 1]
by TREES_2:39; :: thesis: verum

end;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

(dom (ExecTree (Stop S))) -level (n + 1) = {((n + 1) |-> 0)}

proof
_{3}[ Nat] means $1 |-> 0 in dom (ExecTree (Stop S));

let a be object ; :: 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 Nat st S_{3}[n] holds

S_{3}[n + 1]
_{3}[ 0 ]
by TREES_1:22;

for n being Nat holds S_{3}[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: 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 A19, A20, A41; :: thesis: verum

end;

hence
Shereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: {((n + 1) |-> 0)} c= (dom (ExecTree (Stop S))) -level (n + 1)

defpred Slet a be object ; :: 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

A22: a = t1 and

A23: len t1 = n + 1 by A19;

reconsider t0 = t1 | (Seg n) as Element of dom (ExecTree (Stop S)) by RELAT_1:59, TREES_1:20;

A24: succ t0 = { (t0 ^ <*k*>) where k is Nat : k in card (NIC (((Stop S) /. ((ExecTree (Stop S)) . t0)),((ExecTree (Stop S)) . t0))) } by Def2;

(ExecTree (Stop S)) . t0 in dom (Stop S) by A16;

then A25: (ExecTree (Stop S)) . t0 = 0 by TARSKI:def 1;

A26: ( card (NIC ((halt S),((ExecTree (Stop S)) . t0))) = {0} & (Stop S) /. ((ExecTree (Stop S)) . t0) = (Stop S) . ((ExecTree (Stop S)) . t0) ) by A3, A16, PARTFUN1:def 6;

then A27: 0 in card (NIC (((Stop S) /. ((ExecTree (Stop S)) . t0)),((ExecTree (Stop S)) . t0))) by A2, A25, TARSKI:def 1;

A28: succ t0 = {(t0 ^ <*0*>)}

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

hence a in {((n + 1) |-> 0)} by A22, TARSKI:def 1; :: thesis: verum

end;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

A22: a = t1 and

A23: len t1 = n + 1 by A19;

reconsider t0 = t1 | (Seg n) as Element of dom (ExecTree (Stop S)) by RELAT_1:59, TREES_1:20;

A24: succ t0 = { (t0 ^ <*k*>) where k is Nat : k in card (NIC (((Stop S) /. ((ExecTree (Stop S)) . t0)),((ExecTree (Stop S)) . t0))) } by Def2;

(ExecTree (Stop S)) . t0 in dom (Stop S) by A16;

then A25: (ExecTree (Stop S)) . t0 = 0 by TARSKI:def 1;

A26: ( card (NIC ((halt S),((ExecTree (Stop S)) . t0))) = {0} & (Stop S) /. ((ExecTree (Stop S)) . t0) = (Stop S) . ((ExecTree (Stop S)) . t0) ) by A3, A16, PARTFUN1:def 6;

then A27: 0 in card (NIC (((Stop S) /. ((ExecTree (Stop S)) . t0)),((ExecTree (Stop S)) . t0))) by A2, A25, TARSKI:def 1;

A28: succ t0 = {(t0 ^ <*0*>)}

proof

assume s in {(t0 ^ <*0*>)} ; :: thesis: s in succ t0

then s = t0 ^ <*0*> by TARSKI:def 1;

hence s in succ t0 by A24, A27; :: thesis: verum

end;

( t1 . (n + 1) is Nat & t1 = t0 ^ <*(t1 . (n + 1))*> )
by A23, FINSEQ_3:55;hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: {(t0 ^ <*0*>)} c= succ t0

let s be object ; :: according to TARSKI:def 3 :: thesis: ( not s in {(t0 ^ <*0*>)} or s in succ t0 )let s be object ; :: thesis: ( s in succ t0 implies s in {(t0 ^ <*0*>)} )

assume s in succ t0 ; :: thesis: s in {(t0 ^ <*0*>)}

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: verum

end;assume s in succ t0 ; :: thesis: s in {(t0 ^ <*0*>)}

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: verum

assume s in {(t0 ^ <*0*>)} ; :: thesis: s in succ t0

then s = t0 ^ <*0*> by TARSKI:def 1;

hence s in succ t0 by A24, A27; :: thesis: verum

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

then
t1 = (n + 1) |-> 0
by A20, A23, FINSEQ_1:14;
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 A23, FINSEQ_1:1;

end;assume ( 1 <= k & k <= len t1 ) ; :: thesis: t1 . k = ((n + 1) |-> 0) . k

then A35: k in Seg (n + 1) by A23, FINSEQ_1:1;

now :: thesis: t1 . k = 0

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

hence a in {((n + 1) |-> 0)} by A22, TARSKI:def 1; :: thesis: verum

let a be object ; :: 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 Nat st S

S

proof

A40:
S
let n be Nat; :: thesis: ( S_{3}[n] implies S_{3}[n + 1] )

assume S_{3}[n]
; :: thesis: S_{3}[n + 1]

then reconsider t = n |-> 0 as Element of dom (ExecTree (Stop S)) ;

A38: succ t = { (t ^ <*k*>) where k is Nat : k in card (NIC (((Stop S) /. ((ExecTree (Stop S)) . t)),((ExecTree (Stop S)) . t))) } by Def2;

(ExecTree (Stop S)) . t in dom (Stop S) by A16;

then A39: (ExecTree (Stop S)) . t = 0 by 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 A3, A16, PARTFUN1:def 6;

then 0 in card (NIC (((Stop S) /. ((ExecTree (Stop S)) . t)),((ExecTree (Stop S)) . t))) by A2, A39, TARSKI:def 1;

then t ^ <*0*> in succ t by A38;

then t ^ <*0*> in dom (ExecTree (Stop S)) ;

hence S_{3}[n + 1]
by FINSEQ_2:60; :: thesis: verum

end;assume S

then reconsider t = n |-> 0 as Element of dom (ExecTree (Stop S)) ;

A38: succ t = { (t ^ <*k*>) where k is Nat : k in card (NIC (((Stop S) /. ((ExecTree (Stop S)) . t)),((ExecTree (Stop S)) . t))) } by Def2;

(ExecTree (Stop S)) . t in dom (Stop S) by A16;

then A39: (ExecTree (Stop S)) . t = 0 by 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 A3, A16, PARTFUN1:def 6;

then 0 in card (NIC (((Stop S) /. ((ExecTree (Stop S)) . t)),((ExecTree (Stop S)) . t))) by A2, A39, TARSKI:def 1;

then t ^ <*0*> in succ t by A38;

then t ^ <*0*> in dom (ExecTree (Stop S)) ;

hence S

for n being Nat holds S

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 A19, A20, A41; :: thesis: verum

.= TrivialInfiniteTree -level 0 by TREES_9:44 ;

then A42: S

for x being Nat holds S

then dom (ExecTree (Stop S)) = TrivialInfiniteTree by TREES_2:38;

hence ExecTree (Stop S) = TrivialInfiniteTree --> 0 by A17, FUNCOP_1:11; :: thesis: verum