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:
set M = Stop S;
set E = ExecTree (Stop S);
defpred S1[ set ] means (ExecTree (Stop S)) . \$1 in dom (Stop S);
defpred S2[ 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))) =
proof
let t be Element of dom (ExecTree (Stop S)); :: thesis: card (NIC ((halt S),((ExecTree (Stop S)) . t))) =
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))) = by ; :: thesis: verum
end;
A4: 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 A5: S1[f] ; :: thesis: for a being Element of NAT st f ^ <*a*> in dom (ExecTree (Stop S)) holds
S1[f ^ <*a*>]

A6: (Stop S) /. ((ExecTree (Stop S)) . f) = (Stop S) . ((ExecTree (Stop S)) . f) by ;
reconsider Ef = (ExecTree (Stop S)) . f as Nat ;
A7: (ExecTree (Stop S)) . f = 0 by ;
then NIC ((halt S),((ExecTree (Stop S)) . f)) = 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 ;
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 ;
A9: card (NIC ((halt S),((ExecTree (Stop S)) . f))) = by A3;
then A10: 0 in card (NIC (((Stop S) /. ((ExecTree (Stop S)) . f)),((ExecTree (Stop S)) . f))) by ;
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 = {()}
proof
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: {()} c= succ f
let s be object ; :: thesis: ( s in succ f implies s in {()} )
assume s in succ f ; :: thesis: s in {()}
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 ;
hence s in {()} by ; :: thesis: verum
end;
let s be object ; :: according to TARSKI:def 3 :: thesis: ( not s in {()} or s in succ f )
assume s in {()} ; :: thesis: s in succ f
then s = f ^ by TARSKI:def 1;
hence s in succ f by ; :: 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 ^ by ;
then (ExecTree (Stop S)) . (f ^ <*a*>) = (LocSeq ((NIC (((Stop S) /. ((ExecTree (Stop S)) . f)),((ExecTree (Stop S)) . f))),S)) . 0 by
.= 0 by ;
hence S1[f ^ <*a*>] by TARSKI:def 1; :: thesis: verum
end;
(ExecTree (Stop S)) . {} = FirstLoc (Stop S) by Def2;
then A15: S1[ <*> NAT] by VALUED_1:33;
A16: for f being Element of dom (ExecTree (Stop S)) holds S1[f] from A17: for x being object st x in dom (ExecTree (Stop S)) holds
(ExecTree (Stop S)) . x = 0
proof
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;
A18: for n being Nat st S2[n] holds
S2[n + 1]
proof
let n be Nat; :: thesis: ( S2[n] implies S2[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: 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 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 ;
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))) = & (Stop S) /. ((ExecTree (Stop S)) . t0) = (Stop S) . ((ExecTree (Stop S)) . t0) ) by ;
then A27: 0 in card (NIC (((Stop S) /. ((ExecTree (Stop S)) . t0)),((ExecTree (Stop S)) . t0))) by ;
A28: succ t0 = {(t0 ^ )}
proof
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: {(t0 ^ )} c= succ t0
let s be object ; :: thesis: ( s in succ t0 implies s in {(t0 ^ )} )
assume s in succ t0 ; :: thesis: s in {(t0 ^ )}
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 ;
hence s in {(t0 ^ )} by ; :: thesis: verum
end;
let s be object ; :: according to TARSKI:def 3 :: thesis: ( not s in {(t0 ^ )} or s in succ t0 )
assume s in {(t0 ^ )} ; :: thesis: s in succ t0
then s = t0 ^ by TARSKI:def 1;
hence s in succ t0 by ; :: thesis: verum
end;
( t1 . (n + 1) is Nat & t1 = t0 ^ <*(t1 . (n + 1))*> ) by ;
then t0 ^ <*(t1 . (n + 1))*> in succ t0 by TREES_2:12;
then A31: t0 ^ <*(t1 . (n + 1))*> = t0 ^ by ;
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 ;
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 ;
then A33: t0 in (dom (ExecTree (Stop S))) -level n ;
A34: (dom (ExecTree (Stop S))) -level n = {(n |-> 0)} by ;
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 ;
now :: thesis: t1 . k = 0
per cases ( k in Seg n or k = n + 1 ) by ;
suppose A36: k in Seg n ; :: thesis: t1 . k = 0
hence t1 . k = t0 . k by FUNCT_1:49
.= (n |-> 0) . k by
.= 0 by ;
:: thesis: verum
end;
suppose k = n + 1 ; :: thesis: t1 . k = 0
hence t1 . k = 0 by ; :: thesis: verum
end;
end;
end;
hence t1 . k = ((n + 1) |-> 0) . k by ; :: thesis: verum
end;
then t1 = (n + 1) |-> 0 by ;
hence a in {((n + 1) |-> 0)} by ; :: thesis: verum
end;
defpred S3[ 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 S3[n] holds
S3[n + 1]
proof
let n be 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 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))) = & (Stop S) /. ((ExecTree (Stop S)) . t) = (Stop S) . ((ExecTree (Stop S)) . t) ) by ;
then 0 in card (NIC (((Stop S) /. ((ExecTree (Stop S)) . t)),((ExecTree (Stop S)) . t))) by ;
then t ^ in succ t by A38;
then t ^ 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 Nat holds S3[n] from 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 ; :: 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 Nat holds S2[x] from then dom (ExecTree (Stop S)) = TrivialInfiniteTree by TREES_2:38;
hence ExecTree (Stop S) = TrivialInfiniteTree --> 0 by ; :: thesis: verum