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