:: AMISTD_3 semantic presentation
begin
definition
let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated standard AMI-Struct over N;
let M be Subset of NAT;
deffunc H1( set ) -> set = (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl M))),(RelIncl M))) . $1;
func LocSeq (M,S) -> T-Sequence of NAT means :Def1: :: AMISTD_3:def 1
( dom it = card M & ( for m being set st m in card M holds
it . m = (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl M))),(RelIncl M))) . m ) );
existence
ex b1 being T-Sequence of NAT st
( dom b1 = card M & ( for m being set st m in card M holds
b1 . m = (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl M))),(RelIncl M))) . m ) )
proof
consider f being T-Sequence such that
A1: dom f = card M and
A2: for A being Ordinal st A in card M holds
f . A = H1(A) from ORDINAL2:sch_2();
f is NAT -valued
proof
let y be set ; :: according to RELAT_1:def_19,TARSKI:def_3 ::_thesis: ( not y in rng f or y in NAT )
assume y in rng f ; ::_thesis: y in NAT
then consider x being set such that
A3: ( x in dom f & y = f . x ) by FUNCT_1:def_3;
H1(x) in NAT by ORDINAL1:def_12;
hence y in NAT by A1, A2, A3; ::_thesis: verum
end;
then reconsider f = f as T-Sequence of NAT ;
take f ; ::_thesis: ( dom f = card M & ( for m being set st m in card M holds
f . m = (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl M))),(RelIncl M))) . m ) )
thus dom f = card M by A1; ::_thesis: for m being set st m in card M holds
f . m = (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl M))),(RelIncl M))) . m
let m be set ; ::_thesis: ( m in card M implies f . m = (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl M))),(RelIncl M))) . m )
assume m in card M ; ::_thesis: f . m = (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl M))),(RelIncl M))) . m
hence f . m = (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl M))),(RelIncl M))) . m by A2; ::_thesis: verum
end;
uniqueness
for b1, b2 being T-Sequence of NAT st dom b1 = card M & ( for m being set st m in card M holds
b1 . m = (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl M))),(RelIncl M))) . m ) & dom b2 = card M & ( for m being set st m in card M holds
b2 . m = (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl M))),(RelIncl M))) . m ) holds
b1 = b2
proof
let f, g be T-Sequence of NAT ; ::_thesis: ( dom f = card M & ( for m being set st m in card M holds
f . m = (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl M))),(RelIncl M))) . m ) & dom g = card M & ( for m being set st m in card M holds
g . m = (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl M))),(RelIncl M))) . m ) implies f = g )
assume that
A4: dom f = card M and
A5: for m being set st m in card M holds
f . m = H1(m) and
A6: dom g = card M and
A7: for m being set st m in card M holds
g . m = H1(m) ; ::_thesis: f = g
for x being set st x in dom f holds
f . x = g . x
proof
let x be set ; ::_thesis: ( x in dom f implies f . x = g . x )
assume A8: x in dom f ; ::_thesis: f . x = g . x
thus f . x = H1(x) by A4, A5, A8
.= g . x by A4, A7, A8 ; ::_thesis: verum
end;
hence f = g by A4, A6, FUNCT_1:2; ::_thesis: verum
end;
end;
:: deftheorem Def1 defines LocSeq AMISTD_3:def_1_:_
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated standard AMI-Struct over N
for M being Subset of NAT
for b4 being T-Sequence of NAT holds
( b4 = LocSeq (M,S) iff ( dom b4 = card M & ( for m being set st m in card M holds
b4 . m = (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl M))),(RelIncl M))) . m ) ) );
theorem :: AMISTD_3:1
for n being Nat
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated standard AMI-Struct over N
for F being Subset of NAT st F = {n} holds
LocSeq (F,S) = 0 .--> n
proof
let n be Nat; ::_thesis: for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated standard AMI-Struct over N
for F being Subset of NAT st F = {n} holds
LocSeq (F,S) = 0 .--> n
let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated standard AMI-Struct over N
for F being Subset of NAT st F = {n} holds
LocSeq (F,S) = 0 .--> n
let S be non empty with_non-empty_values IC-Ins-separated standard AMI-Struct over N; ::_thesis: for F being Subset of NAT st F = {n} holds
LocSeq (F,S) = 0 .--> n
let F be Subset of NAT; ::_thesis: ( F = {n} implies LocSeq (F,S) = 0 .--> n )
assume A1: F = {n} ; ::_thesis: LocSeq (F,S) = 0 .--> n
then A2: card F = {0} by CARD_1:30, CARD_1:49;
{n} c= omega
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in {n} or a in omega )
assume a in {n} ; ::_thesis: a in omega
hence a in omega by ORDINAL1:def_12; ::_thesis: verum
end;
then A3: (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl {n}))),(RelIncl {n}))) . 0 = (0 .--> n) . 0 by CARD_5:38
.= n by FUNCOP_1:72 ;
A4: dom (LocSeq (F,S)) = card F by Def1;
A5: for a being set st a in dom (LocSeq (F,S)) holds
(LocSeq (F,S)) . a = (0 .--> n) . a
proof
let a be set ; ::_thesis: ( a in dom (LocSeq (F,S)) implies (LocSeq (F,S)) . a = (0 .--> n) . a )
assume A6: a in dom (LocSeq (F,S)) ; ::_thesis: (LocSeq (F,S)) . a = (0 .--> n) . a
then A7: a = 0 by A4, A2, TARSKI:def_1;
thus (LocSeq (F,S)) . a = (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl F))),(RelIncl F))) . a by A4, A6, Def1
.= (0 .--> n) . a by A1, A3, A7, FUNCOP_1:72 ; ::_thesis: verum
end;
dom (0 .--> n) = {0} by FUNCOP_1:13;
hence LocSeq (F,S) = 0 .--> n by A1, A4, A5, CARD_1:30, CARD_1:49, FUNCT_1:2; ::_thesis: verum
end;
registration
let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated standard AMI-Struct over N;
let M be Subset of NAT;
cluster LocSeq (M,S) -> one-to-one ;
coherence
LocSeq (M,S) is one-to-one
proof
set f = LocSeq (M,S);
set C = canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl M))),(RelIncl M));
let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in dom (LocSeq (M,S)) or not x2 in dom (LocSeq (M,S)) or not (LocSeq (M,S)) . x1 = (LocSeq (M,S)) . x2 or x1 = x2 )
assume that
A1: ( x1 in dom (LocSeq (M,S)) & x2 in dom (LocSeq (M,S)) ) and
A2: (LocSeq (M,S)) . x1 = (LocSeq (M,S)) . x2 ; ::_thesis: x1 = x2
A3: dom (LocSeq (M,S)) = card M by Def1;
then A4: ( (LocSeq (M,S)) . x1 = (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl M))),(RelIncl M))) . x1 & (LocSeq (M,S)) . x2 = (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl M))),(RelIncl M))) . x2 ) by A1, Def1;
A5: card M c= order_type_of (RelIncl M) by CARD_5:39;
consider phi being Ordinal-Sequence such that
A6: phi = canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl M))),(RelIncl M)) and
A7: phi is increasing and
A8: dom phi = order_type_of (RelIncl M) and
rng phi = M by CARD_5:5;
phi is one-to-one by A7, CARD_5:11;
hence x1 = x2 by A1, A2, A3, A4, A6, A8, A5, FUNCT_1:def_4; ::_thesis: verum
end;
end;
definition
let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated standard AMI-Struct over N;
let M be non empty preProgram of S;
func ExecTree M -> DecoratedTree of NAT means :Def2: :: AMISTD_3:def 2
( it . {} = FirstLoc M & ( for t being Element of dom it holds
( succ t = { (t ^ <*k*>) where k is Element of NAT : k in card (NIC ((M /. (it . t)),(it . t))) } & ( for m being Element of NAT st m in card (NIC ((M /. (it . t)),(it . t))) holds
it . (t ^ <*m*>) = (LocSeq ((NIC ((M /. (it . t)),(it . t))),S)) . m ) ) ) );
existence
ex b1 being DecoratedTree of NAT st
( b1 . {} = FirstLoc M & ( for t being Element of dom b1 holds
( succ t = { (t ^ <*k*>) where k is Element of NAT : k in card (NIC ((M /. (b1 . t)),(b1 . t))) } & ( for m being Element of NAT st m in card (NIC ((M /. (b1 . t)),(b1 . t))) holds
b1 . (t ^ <*m*>) = (LocSeq ((NIC ((M /. (b1 . t)),(b1 . t))),S)) . m ) ) ) )
proof
defpred S1[ Element of NAT , Nat] means $1 in card (NIC ((M /. $2),$2));
reconsider n = FirstLoc M as Element of NAT ;
defpred S2[ set , Element of NAT , set ] means ex l being Element of NAT st
( l = $1 & ( $2 in dom (LocSeq ((NIC ((M /. l),l)),S)) implies $3 = (LocSeq ((NIC ((M /. l),l)),S)) . $2 ) & ( not $2 in dom (LocSeq ((NIC ((M /. l),l)),S)) implies $3 = 0 ) );
set D = NAT ;
A1: for x, y being Element of NAT ex z being Element of NAT st S2[x,y,z]
proof
let x, y be Element of NAT ; ::_thesis: ex z being Element of NAT st S2[x,y,z]
reconsider z = (LocSeq ((NIC ((M /. x),x)),S)) . y as Element of NAT by ORDINAL1:def_12;
percases ( y in dom (LocSeq ((NIC ((M /. x),x)),S)) or not y in dom (LocSeq ((NIC ((M /. x),x)),S)) ) ;
supposeA2: y in dom (LocSeq ((NIC ((M /. x),x)),S)) ; ::_thesis: ex z being Element of NAT st S2[x,y,z]
take z ; ::_thesis: S2[x,y,z]
thus S2[x,y,z] by A2; ::_thesis: verum
end;
supposeA3: not y in dom (LocSeq ((NIC ((M /. x),x)),S)) ; ::_thesis: ex z being Element of NAT st S2[x,y,z]
reconsider il = 0 as Element of NAT ;
take il ; ::_thesis: S2[x,y,il]
thus S2[x,y,il] by A3; ::_thesis: verum
end;
end;
end;
consider f being Function of [:NAT,NAT:],NAT such that
A4: for l, n being Element of NAT holds S2[l,n,f . (l,n)] from BINOP_1:sch_3(A1);
A5: for d, k1, k2 being Element of NAT st k1 <= k2 & S1[k2,d] holds
S1[k1,d]
proof
let d be Element of NAT ; ::_thesis: for k1, k2 being Element of NAT st k1 <= k2 & S1[k2,d] holds
S1[k1,d]
let k1, k2 be Element of NAT ; ::_thesis: ( k1 <= k2 & S1[k2,d] implies S1[k1,d] )
assume that
A6: k1 <= k2 and
A7: S1[k2,d] ; ::_thesis: S1[k1,d]
k1 c= k2 by A6, NAT_1:39;
hence S1[k1,d] by A7, ORDINAL1:12; ::_thesis: verum
end;
consider T being DecoratedTree of NAT such that
A8: T . {} = n and
A9: for t being Element of dom T holds
( succ t = { (t ^ <*k*>) where k is Element of NAT : S1[k,T . t] } & ( for n being Element of NAT st S1[n,T . t] holds
T . (t ^ <*n*>) = f . ((T . t),n) ) ) from TREES_2:sch_10(A5);
take T ; ::_thesis: ( T . {} = FirstLoc M & ( for t being Element of dom T holds
( succ t = { (t ^ <*k*>) where k is Element of NAT : k in card (NIC ((M /. (T . t)),(T . t))) } & ( for m being Element of NAT st m in card (NIC ((M /. (T . t)),(T . t))) holds
T . (t ^ <*m*>) = (LocSeq ((NIC ((M /. (T . t)),(T . t))),S)) . m ) ) ) )
thus T . {} = FirstLoc M by A8; ::_thesis: for t being Element of dom T holds
( succ t = { (t ^ <*k*>) where k is Element of NAT : k in card (NIC ((M /. (T . t)),(T . t))) } & ( for m being Element of NAT st m in card (NIC ((M /. (T . t)),(T . t))) holds
T . (t ^ <*m*>) = (LocSeq ((NIC ((M /. (T . t)),(T . t))),S)) . m ) )
let t be Element of dom T; ::_thesis: ( succ t = { (t ^ <*k*>) where k is Element of NAT : k in card (NIC ((M /. (T . t)),(T . t))) } & ( for m being Element of NAT st m in card (NIC ((M /. (T . t)),(T . t))) holds
T . (t ^ <*m*>) = (LocSeq ((NIC ((M /. (T . t)),(T . t))),S)) . m ) )
thus succ t = { (t ^ <*k*>) where k is Element of NAT : S1[k,T . t] } by A9; ::_thesis: for m being Element of NAT st m in card (NIC ((M /. (T . t)),(T . t))) holds
T . (t ^ <*m*>) = (LocSeq ((NIC ((M /. (T . t)),(T . t))),S)) . m
reconsider n = T . t as Element of NAT ;
let m be Element of NAT ; ::_thesis: ( m in card (NIC ((M /. (T . t)),(T . t))) implies T . (t ^ <*m*>) = (LocSeq ((NIC ((M /. (T . t)),(T . t))),S)) . m )
consider l being Element of NAT such that
A10: l = n and
A11: ( m in dom (LocSeq ((NIC ((M /. l),l)),S)) implies f . (n,m) = (LocSeq ((NIC ((M /. l),l)),S)) . m ) and
( not m in dom (LocSeq ((NIC ((M /. l),l)),S)) implies f . (n,m) = 0 ) by A4;
assume m in card (NIC ((M /. (T . t)),(T . t))) ; ::_thesis: T . (t ^ <*m*>) = (LocSeq ((NIC ((M /. (T . t)),(T . t))),S)) . m
hence T . (t ^ <*m*>) = (LocSeq ((NIC ((M /. (T . t)),(T . t))),S)) . m by A9, A10, A11, Def1; ::_thesis: verum
end;
uniqueness
for b1, b2 being DecoratedTree of NAT st b1 . {} = FirstLoc M & ( for t being Element of dom b1 holds
( succ t = { (t ^ <*k*>) where k is Element of NAT : k in card (NIC ((M /. (b1 . t)),(b1 . t))) } & ( for m being Element of NAT st m in card (NIC ((M /. (b1 . t)),(b1 . t))) holds
b1 . (t ^ <*m*>) = (LocSeq ((NIC ((M /. (b1 . t)),(b1 . t))),S)) . m ) ) ) & b2 . {} = FirstLoc M & ( for t being Element of dom b2 holds
( succ t = { (t ^ <*k*>) where k is Element of NAT : k in card (NIC ((M /. (b2 . t)),(b2 . t))) } & ( for m being Element of NAT st m in card (NIC ((M /. (b2 . t)),(b2 . t))) holds
b2 . (t ^ <*m*>) = (LocSeq ((NIC ((M /. (b2 . t)),(b2 . t))),S)) . m ) ) ) holds
b1 = b2
proof
let T1, T2 be DecoratedTree of NAT ; ::_thesis: ( T1 . {} = FirstLoc M & ( for t being Element of dom T1 holds
( succ t = { (t ^ <*k*>) where k is Element of NAT : k in card (NIC ((M /. (T1 . t)),(T1 . t))) } & ( for m being Element of NAT st m in card (NIC ((M /. (T1 . t)),(T1 . t))) holds
T1 . (t ^ <*m*>) = (LocSeq ((NIC ((M /. (T1 . t)),(T1 . t))),S)) . m ) ) ) & T2 . {} = FirstLoc M & ( for t being Element of dom T2 holds
( succ t = { (t ^ <*k*>) where k is Element of NAT : k in card (NIC ((M /. (T2 . t)),(T2 . t))) } & ( for m being Element of NAT st m in card (NIC ((M /. (T2 . t)),(T2 . t))) holds
T2 . (t ^ <*m*>) = (LocSeq ((NIC ((M /. (T2 . t)),(T2 . t))),S)) . m ) ) ) implies T1 = T2 )
assume that
A12: T1 . {} = FirstLoc M and
A13: for t being Element of dom T1 holds
( succ t = { (t ^ <*k*>) where k is Element of NAT : k in card (NIC ((M /. (T1 . t)),(T1 . t))) } & ( for m being Element of NAT st m in card (NIC ((M /. (T1 . t)),(T1 . t))) holds
T1 . (t ^ <*m*>) = (LocSeq ((NIC ((M /. (T1 . t)),(T1 . t))),S)) . m ) ) and
A14: T2 . {} = FirstLoc M and
A15: for t being Element of dom T2 holds
( succ t = { (t ^ <*k*>) where k is Element of NAT : k in card (NIC ((M /. (T2 . t)),(T2 . t))) } & ( for m being Element of NAT st m in card (NIC ((M /. (T2 . t)),(T2 . t))) holds
T2 . (t ^ <*m*>) = (LocSeq ((NIC ((M /. (T2 . t)),(T2 . t))),S)) . m ) ) ; ::_thesis: T1 = T2
defpred S1[ Element of NAT ] means (dom T1) -level $1 = (dom T2) -level $1;
A16: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A17: S1[n] ; ::_thesis: S1[n + 1]
set U2 = { (succ w) where w is Element of dom T2 : len w = n } ;
set U1 = { (succ w) where w is Element of dom T1 : len w = n } ;
A18: (dom T2) -level n = { v where v is Element of dom T2 : len v = n } by TREES_2:def_6;
A19: (dom T1) -level n = { v where v is Element of dom T1 : len v = n } by TREES_2:def_6;
A20: union { (succ w) where w is Element of dom T1 : len w = n } = union { (succ w) where w is Element of dom T2 : len w = n }
proof
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: union { (succ w) where w is Element of dom T2 : len w = n } c= union { (succ w) where w is Element of dom T1 : len w = n }
let a be set ; ::_thesis: ( a in union { (succ w) where w is Element of dom T1 : len w = n } implies a in union { (succ w) where w is Element of dom T2 : len w = n } )
assume a in union { (succ w) where w is Element of dom T1 : len w = n } ; ::_thesis: a in union { (succ w) where w is Element of dom T2 : len w = n }
then consider A being set such that
A21: a in A and
A22: A in { (succ w) where w is Element of dom T1 : len w = n } by TARSKI:def_4;
consider w being Element of dom T1 such that
A23: A = succ w and
A24: len w = n by A22;
w in (dom T1) -level n by A19, A24;
then consider v being Element of dom T2 such that
A25: w = v and
A26: len v = n by A17, A18;
A27: w = w | (Seg (len w)) by FINSEQ_3:49;
defpred S2[ Element of NAT ] means ( $1 <= len w & w | (Seg $1) in dom T1 & v | (Seg $1) in dom T2 implies T1 . (w | (Seg $1)) = T2 . (w | (Seg $1)) );
A28: 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] )
assume that
A29: S2[n] and
A30: n + 1 <= len w and
A31: w | (Seg (n + 1)) in dom T1 and
A32: v | (Seg (n + 1)) in dom T2 ; ::_thesis: T1 . (w | (Seg (n + 1))) = T2 . (w | (Seg (n + 1)))
set t1 = w | (Seg n);
A33: 1 <= n + 1 by NAT_1:11;
A34: len (w | (Seg (n + 1))) = n + 1 by A30, FINSEQ_1:17;
then len (w | (Seg (n + 1))) in Seg (n + 1) by A33, FINSEQ_1:1;
then A35: w . (n + 1) = (w | (Seg (n + 1))) . (len (w | (Seg (n + 1)))) by A34, FUNCT_1:49;
n + 1 in dom w by A30, A33, FINSEQ_3:25;
then A36: w | (Seg (n + 1)) = (w | (Seg n)) ^ <*((w | (Seg (n + 1))) . (len (w | (Seg (n + 1)))))*> by A35, FINSEQ_5:10;
A37: n <= n + 1 by NAT_1:11;
then A38: Seg n c= Seg (n + 1) by FINSEQ_1:5;
then v | (Seg n) = (v | (Seg (n + 1))) | (Seg n) by RELAT_1:74;
then A39: v | (Seg n) is_a_prefix_of v | (Seg (n + 1)) by TREES_1:def_1;
w | (Seg n) = (w | (Seg (n + 1))) | (Seg n) by A38, RELAT_1:74;
then w | (Seg n) is_a_prefix_of w | (Seg (n + 1)) by TREES_1:def_1;
then reconsider t1 = w | (Seg n) as Element of dom T1 by A31, TREES_1:20;
reconsider t2 = t1 as Element of dom T2 by A25, A32, A39, TREES_1:20;
A40: succ t1 = { (t1 ^ <*k*>) where k is Element of NAT : k in card (NIC ((M /. (T1 . t1)),(T1 . t1))) } by A13;
A41: (w | (Seg (n + 1))) . (len (w | (Seg (n + 1)))) is Element of NAT by ORDINAL1:def_12;
then t1 ^ <*((w | (Seg (n + 1))) . (len (w | (Seg (n + 1)))))*> in succ t1 by A31, A36, TREES_2:12;
then consider k being Element of NAT such that
A42: t1 ^ <*((w | (Seg (n + 1))) . (len (w | (Seg (n + 1)))))*> = t1 ^ <*k*> and
A43: k in card (NIC ((M /. (T1 . t1)),(T1 . t1))) by A40;
A44: (w | (Seg (n + 1))) . (len (w | (Seg (n + 1)))) in card (NIC ((M /. (T2 . t2)),(T2 . t2))) by A29, A30, A32, A37, A39, A42, A43, FINSEQ_2:17, TREES_1:20, XXREAL_0:2;
k = (w | (Seg (n + 1))) . (len (w | (Seg (n + 1)))) by A42, FINSEQ_2:17;
hence T1 . (w | (Seg (n + 1))) = (LocSeq ((NIC ((M /. (T1 . t1)),(T1 . t1))),S)) . ((w | (Seg (n + 1))) . (len (w | (Seg (n + 1))))) by A13, A36, A43
.= T2 . (w | (Seg (n + 1))) by A15, A29, A30, A32, A37, A39, A41, A36, A44, TREES_1:20, XXREAL_0:2 ;
::_thesis: verum
end;
A45: S2[ 0 ] by A12, A14;
for n being Element of NAT holds S2[n] from NAT_1:sch_1(A45, A28);
then A46: T1 . w = T2 . w by A25, A27;
A47: succ v in { (succ w) where w is Element of dom T2 : len w = n } by A26;
( succ v = { (v ^ <*k*>) where k is Element of NAT : k in card (NIC ((M /. (T2 . v)),(T2 . v))) } & succ w = { (w ^ <*k*>) where k is Element of NAT : k in card (NIC ((M /. (T1 . w)),(T1 . w))) } ) by A13, A15;
hence a in union { (succ w) where w is Element of dom T2 : len w = n } by A21, A23, A25, A46, A47, TARSKI:def_4; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in union { (succ w) where w is Element of dom T2 : len w = n } or a in union { (succ w) where w is Element of dom T1 : len w = n } )
assume a in union { (succ w) where w is Element of dom T2 : len w = n } ; ::_thesis: a in union { (succ w) where w is Element of dom T1 : len w = n }
then consider A being set such that
A48: a in A and
A49: A in { (succ w) where w is Element of dom T2 : len w = n } by TARSKI:def_4;
consider w being Element of dom T2 such that
A50: A = succ w and
A51: len w = n by A49;
w in (dom T2) -level n by A18, A51;
then consider v being Element of dom T1 such that
A52: w = v and
A53: len v = n by A17, A19;
A54: w = w | (Seg (len w)) by FINSEQ_3:49;
defpred S2[ Element of NAT ] means ( $1 <= len w & w | (Seg $1) in dom T1 & v | (Seg $1) in dom T2 implies T1 . (w | (Seg $1)) = T2 . (w | (Seg $1)) );
A55: 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] )
assume that
A56: S2[n] and
A57: n + 1 <= len w and
A58: w | (Seg (n + 1)) in dom T1 and
A59: v | (Seg (n + 1)) in dom T2 ; ::_thesis: T1 . (w | (Seg (n + 1))) = T2 . (w | (Seg (n + 1)))
set t1 = w | (Seg n);
A60: 1 <= n + 1 by NAT_1:11;
A61: len (w | (Seg (n + 1))) = n + 1 by A57, FINSEQ_1:17;
then len (w | (Seg (n + 1))) in Seg (n + 1) by A60, FINSEQ_1:1;
then A62: w . (n + 1) = (w | (Seg (n + 1))) . (len (w | (Seg (n + 1)))) by A61, FUNCT_1:49;
n + 1 in dom w by A57, A60, FINSEQ_3:25;
then A63: w | (Seg (n + 1)) = (w | (Seg n)) ^ <*((w | (Seg (n + 1))) . (len (w | (Seg (n + 1)))))*> by A62, FINSEQ_5:10;
A64: n <= n + 1 by NAT_1:11;
then A65: Seg n c= Seg (n + 1) by FINSEQ_1:5;
then v | (Seg n) = (v | (Seg (n + 1))) | (Seg n) by RELAT_1:74;
then A66: v | (Seg n) is_a_prefix_of v | (Seg (n + 1)) by TREES_1:def_1;
w | (Seg n) = (w | (Seg (n + 1))) | (Seg n) by A65, RELAT_1:74;
then w | (Seg n) is_a_prefix_of w | (Seg (n + 1)) by TREES_1:def_1;
then reconsider t1 = w | (Seg n) as Element of dom T1 by A58, TREES_1:20;
reconsider t2 = t1 as Element of dom T2 by A52, A59, A66, TREES_1:20;
A67: succ t1 = { (t1 ^ <*k*>) where k is Element of NAT : k in card (NIC ((M /. (T1 . t1)),(T1 . t1))) } by A13;
A68: (w | (Seg (n + 1))) . (len (w | (Seg (n + 1)))) is Element of NAT by ORDINAL1:def_12;
then t1 ^ <*((w | (Seg (n + 1))) . (len (w | (Seg (n + 1)))))*> in succ t1 by A58, A63, TREES_2:12;
then consider k being Element of NAT such that
A69: t1 ^ <*((w | (Seg (n + 1))) . (len (w | (Seg (n + 1)))))*> = t1 ^ <*k*> and
A70: k in card (NIC ((M /. (T1 . t1)),(T1 . t1))) by A67;
A71: (w | (Seg (n + 1))) . (len (w | (Seg (n + 1)))) in card (NIC ((M /. (T2 . t2)),(T2 . t2))) by A56, A57, A59, A64, A66, A69, A70, FINSEQ_2:17, TREES_1:20, XXREAL_0:2;
k = (w | (Seg (n + 1))) . (len (w | (Seg (n + 1)))) by A69, FINSEQ_2:17;
hence T1 . (w | (Seg (n + 1))) = (LocSeq ((NIC ((M /. (T1 . t1)),(T1 . t1))),S)) . ((w | (Seg (n + 1))) . (len (w | (Seg (n + 1))))) by A13, A63, A70
.= T2 . (w | (Seg (n + 1))) by A15, A56, A57, A59, A64, A66, A68, A63, A71, TREES_1:20, XXREAL_0:2 ;
::_thesis: verum
end;
A72: S2[ 0 ] by A12, A14;
for n being Element of NAT holds S2[n] from NAT_1:sch_1(A72, A55);
then A73: T1 . w = T2 . w by A52, A54;
A74: succ v in { (succ w) where w is Element of dom T1 : len w = n } by A53;
( succ v = { (v ^ <*k*>) where k is Element of NAT : k in card (NIC ((M /. (T1 . v)),(T1 . v))) } & succ w = { (w ^ <*k*>) where k is Element of NAT : k in card (NIC ((M /. (T2 . w)),(T2 . w))) } ) by A13, A15;
hence a in union { (succ w) where w is Element of dom T1 : len w = n } by A48, A50, A52, A73, A74, TARSKI:def_4; ::_thesis: verum
end;
(dom T1) -level (n + 1) = union { (succ w) where w is Element of dom T1 : len w = n } by TREES_9:45;
hence S1[n + 1] by A20, TREES_9:45; ::_thesis: verum
end;
(dom T1) -level 0 = {{}} by TREES_9:44
.= (dom T2) -level 0 by TREES_9:44 ;
then A75: S1[ 0 ] ;
A76: for n being Element of NAT holds S1[n] from NAT_1:sch_1(A75, A16);
for p being FinSequence of NAT st p in dom T1 holds
T1 . p = T2 . p
proof
let p be FinSequence of NAT ; ::_thesis: ( p in dom T1 implies T1 . p = T2 . p )
defpred S2[ Element of NAT ] means ( $1 <= len p & p | (Seg $1) in dom T1 implies T1 . (p | (Seg $1)) = T2 . (p | (Seg $1)) );
A77: p | (Seg (len p)) = p by FINSEQ_3:49;
A78: 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] )
assume that
A79: S2[n] and
A80: n + 1 <= len p and
A81: p | (Seg (n + 1)) in dom T1 ; ::_thesis: T1 . (p | (Seg (n + 1))) = T2 . (p | (Seg (n + 1)))
set t1 = p | (Seg n);
A82: 1 <= n + 1 by NAT_1:11;
A83: len (p | (Seg (n + 1))) = n + 1 by A80, FINSEQ_1:17;
then len (p | (Seg (n + 1))) in Seg (n + 1) by A82, FINSEQ_1:1;
then A84: p . (n + 1) = (p | (Seg (n + 1))) . (len (p | (Seg (n + 1)))) by A83, FUNCT_1:49;
n + 1 in dom p by A80, A82, FINSEQ_3:25;
then A85: p | (Seg (n + 1)) = (p | (Seg n)) ^ <*((p | (Seg (n + 1))) . (len (p | (Seg (n + 1)))))*> by A84, FINSEQ_5:10;
A86: n <= n + 1 by NAT_1:11;
then Seg n c= Seg (n + 1) by FINSEQ_1:5;
then p | (Seg n) = (p | (Seg (n + 1))) | (Seg n) by RELAT_1:74;
then p | (Seg n) is_a_prefix_of p | (Seg (n + 1)) by TREES_1:def_1;
then reconsider t1 = p | (Seg n) as Element of dom T1 by A81, TREES_1:20;
reconsider t2 = t1 as Element of dom T2 by A76, TREES_2:38;
A87: succ t1 = { (t1 ^ <*k*>) where k is Element of NAT : k in card (NIC ((M /. (T1 . t1)),(T1 . t1))) } by A13;
A88: (p | (Seg (n + 1))) . (len (p | (Seg (n + 1)))) is Element of NAT by ORDINAL1:def_12;
then t1 ^ <*((p | (Seg (n + 1))) . (len (p | (Seg (n + 1)))))*> in succ t1 by A81, A85, TREES_2:12;
then consider k being Element of NAT such that
A89: t1 ^ <*((p | (Seg (n + 1))) . (len (p | (Seg (n + 1)))))*> = t1 ^ <*k*> and
A90: k in card (NIC ((M /. (T1 . t1)),(T1 . t1))) by A87;
A91: (p | (Seg (n + 1))) . (len (p | (Seg (n + 1)))) in card (NIC ((M /. (T2 . t2)),(T2 . t2))) by A79, A80, A86, A89, A90, FINSEQ_2:17, XXREAL_0:2;
k = (p | (Seg (n + 1))) . (len (p | (Seg (n + 1)))) by A89, FINSEQ_2:17;
hence T1 . (p | (Seg (n + 1))) = (LocSeq ((NIC ((M /. (T1 . t1)),(T1 . t1))),S)) . ((p | (Seg (n + 1))) . (len (p | (Seg (n + 1))))) by A13, A85, A90
.= T2 . (p | (Seg (n + 1))) by A15, A79, A80, A86, A88, A85, A91, XXREAL_0:2 ;
::_thesis: verum
end;
A92: S2[ 0 ] by A12, A14;
for n being Element of NAT holds S2[n] from NAT_1:sch_1(A92, A78);
hence ( p in dom T1 implies T1 . p = T2 . p ) by A77; ::_thesis: verum
end;
hence T1 = T2 by A76, TREES_2:31, TREES_2:38; ::_thesis: verum
end;
end;
:: deftheorem Def2 defines ExecTree AMISTD_3:def_2_:_
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated standard AMI-Struct over N
for M being non empty preProgram of S
for b4 being DecoratedTree of NAT holds
( b4 = ExecTree M iff ( b4 . {} = FirstLoc M & ( for t being Element of dom b4 holds
( succ t = { (t ^ <*k*>) where k is Element of NAT : k in card (NIC ((M /. (b4 . t)),(b4 . t))) } & ( for m being Element of NAT st m in card (NIC ((M /. (b4 . t)),(b4 . t))) holds
b4 . (t ^ <*m*>) = (LocSeq ((NIC ((M /. (b4 . t)),(b4 . t))),S)) . m ) ) ) ) );
theorem :: AMISTD_3:2
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated halting standard AMI-Struct over N holds ExecTree (Stop S) = TrivialInfiniteTree --> 0
proof
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 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: dom (Stop S) = {0} by FUNCOP_1:13;
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: 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;
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 A5, PARTFUN1:def_6;
reconsider Ef = (ExecTree (Stop S)) . f as Element of NAT ;
A7: (ExecTree (Stop S)) . f = 0 by A1, 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 A1, 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 Element of NAT : k in card (NIC (((Stop S) /. ((ExecTree (Stop S)) . f)),((ExecTree (Stop S)) . f))) } by Def2;
A12: 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
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;
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 A11, A10; ::_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 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 S1[f ^ <*a*>] by A1, 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 HILBERT2:sch_1(A15, A4);
A17: 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 A16;
hence (ExecTree (Stop S)) . x = 0 by A1, TARSKI:def_1; ::_thesis: verum
end;
A18: 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;
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 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
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 Element of 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 A1, 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
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
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;
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 A24, A27; ::_thesis: verum
end;
( t1 . (n + 1) is Element of NAT & t1 = t0 ^ <*(t1 . (n + 1))*> ) by A23, FINSEQ_3:55, ORDINAL1:def_12;
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;
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;
then A32: t0 in (dom (ExecTree (Stop S))) -level n ;
A33: (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: ( 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 A34: k in Seg (n + 1) by A23, FINSEQ_1:1;
now__::_thesis:_t1_._k_=_0
percases ( k in Seg n or k = n + 1 ) by A34, FINSEQ_2:7;
supposeA35: k in Seg n ; ::_thesis: t1 . k = 0
hence t1 . k = t0 . k by FUNCT_1:49
.= (n |-> 0) . k by A33, A32, TARSKI:def_1
.= 0 by A35, FUNCOP_1:7 ;
::_thesis: verum
end;
suppose k = n + 1 ; ::_thesis: t1 . k = 0
hence t1 . k = 0 by A31, FINSEQ_2:17; ::_thesis: verum
end;
end;
end;
hence t1 . k = ((n + 1) |-> 0) . k by A34, FUNCOP_1:7; ::_thesis: verum
end;
then t1 = (n + 1) |-> 0 by A20, A23, FINSEQ_1:14;
hence a in {((n + 1) |-> 0)} by A22, 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) )
A36: 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)) ;
A37: 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 Def2;
(ExecTree (Stop S)) . t in dom (Stop S) by A16;
then A38: (ExecTree (Stop S)) . t = 0 by A1, 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, A38, TARSKI:def_1;
then t ^ <*0*> in succ t by A37;
then t ^ <*0*> in dom (ExecTree (Stop S)) ;
hence S3[n + 1] by FINSEQ_2:60; ::_thesis: verum
end;
A39: S3[ 0 ] by TREES_1:22;
for n being Element of NAT holds S3[n] from NAT_1:sch_1(A39, A36);
then A40: (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, A40; ::_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 A41: S2[ 0 ] ;
for x being Element of NAT holds S2[x] from NAT_1:sch_1(A41, A18);
then dom (ExecTree (Stop S)) = TrivialInfiniteTree by TREES_2:38;
hence ExecTree (Stop S) = TrivialInfiniteTree --> 0 by A17, FUNCOP_1:11; ::_thesis: verum
end;