:: Sets and Functions of Trees and Joining Operations of Trees :: by Grzegorz Bancerek :: :: Received November 27, 1992 :: Copyright (c) 1992-2012 Association of Mizar Users begin Lm1: for n being Element of NAT for p, q being FinSequence st 1 <= n & n <= len p holds (p ^ q) . n = p . n proofend; begin definition func Trees -> set means :Def1: :: TREES_3:def 1 for x being set holds ( x in it iff x is Tree ); existence ex b1 being set st for x being set holds ( x in b1 iff x is Tree ) proofend; uniqueness for b1, b2 being set st ( for x being set holds ( x in b1 iff x is Tree ) ) & ( for x being set holds ( x in b2 iff x is Tree ) ) holds b1 = b2 proofend; end; :: deftheorem Def1 defines Trees TREES_3:def_1_:_ for b1 being set holds ( b1 = Trees iff for x being set holds ( x in b1 iff x is Tree ) ); registration cluster Trees -> non empty ; coherence not Trees is empty proofend; end; definition func FinTrees -> Subset of Trees means :Def2: :: TREES_3:def 2 for x being set holds ( x in it iff x is finite Tree ); existence ex b1 being Subset of Trees st for x being set holds ( x in b1 iff x is finite Tree ) proofend; uniqueness for b1, b2 being Subset of Trees st ( for x being set holds ( x in b1 iff x is finite Tree ) ) & ( for x being set holds ( x in b2 iff x is finite Tree ) ) holds b1 = b2 proofend; end; :: deftheorem Def2 defines FinTrees TREES_3:def_2_:_ for b1 being Subset of Trees holds ( b1 = FinTrees iff for x being set holds ( x in b1 iff x is finite Tree ) ); registration cluster FinTrees -> non empty ; coherence not FinTrees is empty proofend; end; definition let IT be set ; attrIT is constituted-Trees means :Def3: :: TREES_3:def 3 for x being set st x in IT holds x is Tree; attrIT is constituted-FinTrees means :Def4: :: TREES_3:def 4 for x being set st x in IT holds x is finite Tree; attrIT is constituted-DTrees means :Def5: :: TREES_3:def 5 for x being set st x in IT holds x is DecoratedTree; end; :: deftheorem Def3 defines constituted-Trees TREES_3:def_3_:_ for IT being set holds ( IT is constituted-Trees iff for x being set st x in IT holds x is Tree ); :: deftheorem Def4 defines constituted-FinTrees TREES_3:def_4_:_ for IT being set holds ( IT is constituted-FinTrees iff for x being set st x in IT holds x is finite Tree ); :: deftheorem Def5 defines constituted-DTrees TREES_3:def_5_:_ for IT being set holds ( IT is constituted-DTrees iff for x being set st x in IT holds x is DecoratedTree ); theorem :: TREES_3:1 for X being set holds ( X is constituted-Trees iff X c= Trees ) proofend; theorem :: TREES_3:2 for X being set holds ( X is constituted-FinTrees iff X c= FinTrees ) proofend; theorem Th3: :: TREES_3:3 for X, Y being set holds ( ( X is constituted-Trees & Y is constituted-Trees ) iff X \/ Y is constituted-Trees ) proofend; theorem :: TREES_3:4 for X, Y being set st X is constituted-Trees & Y is constituted-Trees holds X \+\ Y is constituted-Trees proofend; theorem :: TREES_3:5 for X, Y being set st X is constituted-Trees holds ( X /\ Y is constituted-Trees & Y /\ X is constituted-Trees & X \ Y is constituted-Trees ) proofend; theorem Th6: :: TREES_3:6 for X, Y being set holds ( ( X is constituted-FinTrees & Y is constituted-FinTrees ) iff X \/ Y is constituted-FinTrees ) proofend; theorem :: TREES_3:7 for X, Y being set st X is constituted-FinTrees & Y is constituted-FinTrees holds X \+\ Y is constituted-FinTrees proofend; theorem :: TREES_3:8 for X, Y being set st X is constituted-FinTrees holds ( X /\ Y is constituted-FinTrees & Y /\ X is constituted-FinTrees & X \ Y is constituted-FinTrees ) proofend; theorem Th9: :: TREES_3:9 for X, Y being set holds ( ( X is constituted-DTrees & Y is constituted-DTrees ) iff X \/ Y is constituted-DTrees ) proofend; theorem :: TREES_3:10 for X, Y being set st X is constituted-DTrees & Y is constituted-DTrees holds X \+\ Y is constituted-DTrees proofend; theorem :: TREES_3:11 for X, Y being set st X is constituted-DTrees holds ( X /\ Y is constituted-DTrees & Y /\ X is constituted-DTrees & X \ Y is constituted-DTrees ) proofend; registration cluster empty -> constituted-Trees constituted-FinTrees constituted-DTrees for set ; coherence for b1 being set st b1 is empty holds ( b1 is constituted-Trees & b1 is constituted-FinTrees & b1 is constituted-DTrees ) proofend; end; theorem Th12: :: TREES_3:12 for x being set holds ( {x} is constituted-Trees iff x is Tree ) proofend; theorem Th13: :: TREES_3:13 for x being set holds ( {x} is constituted-FinTrees iff x is finite Tree ) proofend; theorem Th14: :: TREES_3:14 for x being set holds ( {x} is constituted-DTrees iff x is DecoratedTree ) proofend; theorem Th15: :: TREES_3:15 for x, y being set holds ( {x,y} is constituted-Trees iff ( x is Tree & y is Tree ) ) proofend; theorem Th16: :: TREES_3:16 for x, y being set holds ( {x,y} is constituted-FinTrees iff ( x is finite Tree & y is finite Tree ) ) proofend; theorem Th17: :: TREES_3:17 for x, y being set holds ( {x,y} is constituted-DTrees iff ( x is DecoratedTree & y is DecoratedTree ) ) proofend; theorem :: TREES_3:18 for X, Y being set st X is constituted-Trees & Y c= X holds Y is constituted-Trees proofend; theorem :: TREES_3:19 for X, Y being set st X is constituted-FinTrees & Y c= X holds Y is constituted-FinTrees proofend; theorem :: TREES_3:20 for X, Y being set st X is constituted-DTrees & Y c= X holds Y is constituted-DTrees proofend; registration cluster non empty finite constituted-Trees constituted-FinTrees for set ; existence ex b1 being set st ( b1 is finite & b1 is constituted-Trees & b1 is constituted-FinTrees & not b1 is empty ) proofend; cluster non empty finite constituted-DTrees for set ; existence ex b1 being set st ( b1 is finite & b1 is constituted-DTrees & not b1 is empty ) proofend; end; registration cluster constituted-FinTrees -> constituted-Trees for set ; coherence for b1 being set st b1 is constituted-FinTrees holds b1 is constituted-Trees proofend; end; registration let X be constituted-Trees set ; cluster -> constituted-Trees for Element of bool X; coherence for b1 being Subset of X holds b1 is constituted-Trees proofend; end; registration let X be constituted-FinTrees set ; cluster -> constituted-FinTrees for Element of bool X; coherence for b1 being Subset of X holds b1 is constituted-FinTrees proofend; end; registration let X be constituted-DTrees set ; cluster -> constituted-DTrees for Element of bool X; coherence for b1 being Subset of X holds b1 is constituted-DTrees proofend; end; registration let D be non empty constituted-Trees set ; cluster -> non empty Tree-like for Element of D; coherence for b1 being Element of D holds ( not b1 is empty & b1 is Tree-like ) by Def3; end; registration let D be non empty constituted-FinTrees set ; cluster -> finite for Element of D; coherence for b1 being Element of D holds b1 is finite by Def4; end; registration cluster constituted-DTrees -> functional for set ; coherence for b1 being set st b1 is constituted-DTrees holds b1 is functional proofend; end; registration let D be non empty constituted-DTrees set ; cluster -> DecoratedTree-like for Element of D; coherence for b1 being Element of D holds b1 is DecoratedTree-like by Def5; end; registration cluster Trees -> constituted-Trees ; coherence Trees is constituted-Trees proofend; end; registration cluster FinTrees -> constituted-FinTrees ; coherence FinTrees is constituted-FinTrees proofend; end; registration cluster non empty constituted-Trees constituted-FinTrees for Element of bool Trees; existence ex b1 being Subset of Trees st ( b1 is constituted-FinTrees & not b1 is empty ) proofend; end; definition let D be non empty set ; mode DTree-set of D -> non empty set means :Def6: :: TREES_3:def 6 for x being set st x in it holds x is DecoratedTree of D; existence ex b1 being non empty set st for x being set st x in b1 holds x is DecoratedTree of D proofend; end; :: deftheorem Def6 defines DTree-set TREES_3:def_6_:_ for D, b2 being non empty set holds ( b2 is DTree-set of D iff for x being set st x in b2 holds x is DecoratedTree of D ); registration let D be non empty set ; cluster -> constituted-DTrees for DTree-set of D; coherence for b1 being DTree-set of D holds b1 is constituted-DTrees proofend; end; registration let D be non empty set ; cluster functional non empty finite constituted-DTrees for DTree-set of D; existence ex b1 being DTree-set of D st ( b1 is finite & not b1 is empty ) proofend; end; registration let D be non empty set ; let E be non empty DTree-set of D; cluster -> D -valued for Element of E; coherence for b1 being Element of E holds b1 is D -valued by Def6; end; definition let T be Tree; let D be non empty set ; :: original:Funcs redefine func Funcs (T,D) -> non empty DTree-set of D; coherence Funcs (T,D) is non empty DTree-set of D proofend; end; registration let T be Tree; let D be non empty set ; cluster Function-like quasi_total -> DecoratedTree-like for Element of bool [:T,D:]; coherence for b1 being Function of T,D holds b1 is DecoratedTree-like proofend; end; definition let D be non empty set ; func Trees D -> DTree-set of D means :Def7: :: TREES_3:def 7 for T being DecoratedTree of D holds T in it; existence ex b1 being DTree-set of D st for T being DecoratedTree of D holds T in b1 proofend; uniqueness for b1, b2 being DTree-set of D st ( for T being DecoratedTree of D holds T in b1 ) & ( for T being DecoratedTree of D holds T in b2 ) holds b1 = b2 proofend; end; :: deftheorem Def7 defines Trees TREES_3:def_7_:_ for D being non empty set for b2 being DTree-set of D holds ( b2 = Trees D iff for T being DecoratedTree of D holds T in b2 ); registration let D be non empty set ; cluster Trees D -> non empty ; coherence not Trees D is empty ; end; definition let D be non empty set ; func FinTrees D -> DTree-set of D means :Def8: :: TREES_3:def 8 for T being DecoratedTree of D holds ( dom T is finite iff T in it ); existence ex b1 being DTree-set of D st for T being DecoratedTree of D holds ( dom T is finite iff T in b1 ) proofend; uniqueness for b1, b2 being DTree-set of D st ( for T being DecoratedTree of D holds ( dom T is finite iff T in b1 ) ) & ( for T being DecoratedTree of D holds ( dom T is finite iff T in b2 ) ) holds b1 = b2 proofend; end; :: deftheorem Def8 defines FinTrees TREES_3:def_8_:_ for D being non empty set for b2 being DTree-set of D holds ( b2 = FinTrees D iff for T being DecoratedTree of D holds ( dom T is finite iff T in b2 ) ); theorem :: TREES_3:21 for D being non empty set holds FinTrees D c= Trees D proofend; begin definition let IT be Function; attrIT is Tree-yielding means :Def9: :: TREES_3:def 9 rng IT is constituted-Trees ; attrIT is FinTree-yielding means :Def10: :: TREES_3:def 10 rng IT is constituted-FinTrees ; attrIT is DTree-yielding means :Def11: :: TREES_3:def 11 rng IT is constituted-DTrees ; end; :: deftheorem Def9 defines Tree-yielding TREES_3:def_9_:_ for IT being Function holds ( IT is Tree-yielding iff rng IT is constituted-Trees ); :: deftheorem Def10 defines FinTree-yielding TREES_3:def_10_:_ for IT being Function holds ( IT is FinTree-yielding iff rng IT is constituted-FinTrees ); :: deftheorem Def11 defines DTree-yielding TREES_3:def_11_:_ for IT being Function holds ( IT is DTree-yielding iff rng IT is constituted-DTrees ); registration cluster Relation-like Function-like empty -> Tree-yielding FinTree-yielding DTree-yielding for set ; coherence for b1 being Function st b1 is empty holds ( b1 is Tree-yielding & b1 is FinTree-yielding & b1 is DTree-yielding ) proofend; end; theorem Th22: :: TREES_3:22 for f being Function holds ( f is Tree-yielding iff for x being set st x in dom f holds f . x is Tree ) proofend; theorem :: TREES_3:23 for f being Function holds ( f is FinTree-yielding iff for x being set st x in dom f holds f . x is finite Tree ) proofend; theorem Th24: :: TREES_3:24 for f being Function holds ( f is DTree-yielding iff for x being set st x in dom f holds f . x is DecoratedTree ) proofend; theorem Th25: :: TREES_3:25 for p, q being FinSequence holds ( ( p is Tree-yielding & q is Tree-yielding ) iff p ^ q is Tree-yielding ) proofend; theorem Th26: :: TREES_3:26 for p, q being FinSequence holds ( ( p is FinTree-yielding & q is FinTree-yielding ) iff p ^ q is FinTree-yielding ) proofend; theorem Th27: :: TREES_3:27 for p, q being FinSequence holds ( ( p is DTree-yielding & q is DTree-yielding ) iff p ^ q is DTree-yielding ) proofend; theorem Th28: :: TREES_3:28 for x being set holds ( <*x*> is Tree-yielding iff x is Tree ) proofend; theorem Th29: :: TREES_3:29 for x being set holds ( <*x*> is FinTree-yielding iff x is finite Tree ) proofend; theorem Th30: :: TREES_3:30 for x being set holds ( <*x*> is DTree-yielding iff x is DecoratedTree ) proofend; theorem Th31: :: TREES_3:31 for x, y being set holds ( <*x,y*> is Tree-yielding iff ( x is Tree & y is Tree ) ) proofend; theorem Th32: :: TREES_3:32 for x, y being set holds ( <*x,y*> is FinTree-yielding iff ( x is finite Tree & y is finite Tree ) ) proofend; theorem Th33: :: TREES_3:33 for x, y being set holds ( <*x,y*> is DTree-yielding iff ( x is DecoratedTree & y is DecoratedTree ) ) proofend; theorem Th34: :: TREES_3:34 for x being set for i being Element of NAT st i <> 0 holds ( i |-> x is Tree-yielding iff x is Tree ) proofend; theorem Th35: :: TREES_3:35 for x being set for i being Element of NAT st i <> 0 holds ( i |-> x is FinTree-yielding iff x is finite Tree ) proofend; theorem Th36: :: TREES_3:36 for x being set for i being Element of NAT st i <> 0 holds ( i |-> x is DTree-yielding iff x is DecoratedTree ) proofend; registration cluster Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like Tree-yielding FinTree-yielding for set ; existence ex b1 being FinSequence st ( b1 is Tree-yielding & b1 is FinTree-yielding & not b1 is empty ) proofend; cluster Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like DTree-yielding for set ; existence ex b1 being FinSequence st ( b1 is DTree-yielding & not b1 is empty ) proofend; end; registration cluster Relation-like Function-like non empty Tree-yielding FinTree-yielding for set ; existence ex b1 being Function st ( b1 is Tree-yielding & b1 is FinTree-yielding & not b1 is empty ) proofend; cluster Relation-like Function-like non empty DTree-yielding for set ; existence ex b1 being Function st ( b1 is DTree-yielding & not b1 is empty ) proofend; end; registration cluster Relation-like Function-like FinTree-yielding -> Tree-yielding for set ; coherence for b1 being Function st b1 is FinTree-yielding holds b1 is Tree-yielding proofend; end; registration let D be non empty constituted-Trees set ; cluster -> Tree-yielding for FinSequence of D; coherence for b1 being FinSequence of D holds b1 is Tree-yielding proofend; end; registration let p, q be Tree-yielding FinSequence; clusterp ^ q -> Tree-yielding ; coherence p ^ q is Tree-yielding by Th25; end; registration let D be non empty constituted-FinTrees set ; cluster -> FinTree-yielding for FinSequence of D; coherence for b1 being FinSequence of D holds b1 is FinTree-yielding proofend; end; registration let p, q be FinTree-yielding FinSequence; clusterp ^ q -> FinTree-yielding ; coherence p ^ q is FinTree-yielding by Th26; end; registration let D be non empty constituted-DTrees set ; cluster -> DTree-yielding for FinSequence of D; coherence for b1 being FinSequence of D holds b1 is DTree-yielding proofend; end; registration let p, q be DTree-yielding FinSequence; clusterp ^ q -> DTree-yielding ; coherence p ^ q is DTree-yielding by Th27; end; registration let T be Tree; cluster<*T*> -> non empty Tree-yielding ; coherence ( <*T*> is Tree-yielding & not <*T*> is empty ) by Th28; let S be Tree; cluster<*T,S*> -> non empty Tree-yielding ; coherence ( <*T,S*> is Tree-yielding & not <*T,S*> is empty ) by Th31; end; registration let n be Element of NAT ; let T be Tree; clustern |-> T -> Tree-yielding ; coherence n |-> T is Tree-yielding proofend; end; registration let T be finite Tree; cluster<*T*> -> FinTree-yielding ; coherence <*T*> is FinTree-yielding by Th29; let S be finite Tree; cluster<*T,S*> -> FinTree-yielding ; coherence <*T,S*> is FinTree-yielding by Th32; end; registration let n be Element of NAT ; let T be finite Tree; clustern |-> T -> FinTree-yielding ; coherence n |-> T is FinTree-yielding proofend; end; registration let T be DecoratedTree; cluster<*T*> -> non empty DTree-yielding ; coherence ( <*T*> is DTree-yielding & not <*T*> is empty ) by Th30; let S be DecoratedTree; cluster<*T,S*> -> non empty DTree-yielding ; coherence ( <*T,S*> is DTree-yielding & not <*T,S*> is empty ) by Th33; end; registration let n be Element of NAT ; let T be DecoratedTree; clustern |-> T -> DTree-yielding ; coherence n |-> T is DTree-yielding proofend; end; theorem Th37: :: TREES_3:37 for f being DTree-yielding Function holds ( dom (doms f) = dom f & doms f is Tree-yielding ) proofend; registration let p be DTree-yielding FinSequence; cluster doms p -> FinSequence-like Tree-yielding ; coherence ( doms p is Tree-yielding & doms p is FinSequence-like ) proofend; end; theorem :: TREES_3:38 for p being DTree-yielding FinSequence holds len (doms p) = len p proofend; Lm2: for D being non empty set for T being DecoratedTree of D holds T is Function of (dom T),D proofend; begin definition let D, E be non empty set ; mode DecoratedTree of D,E is DecoratedTree of [:D,E:]; mode DTree-set of D,E is DTree-set of [:D,E:]; end; registration let T1, T2 be DecoratedTree; cluster<:T1,T2:> -> DecoratedTree-like ; coherence <:T1,T2:> is DecoratedTree-like proofend; end; registration let D1, D2 be non empty set ; let T1 be DecoratedTree of D1; let T2 be DecoratedTree of D2; cluster<:T1,T2:> -> [:D1,D2:] -valued ; coherence <:T1,T2:> is [:D1,D2:] -valued proofend; end; registration let D, E be non empty set ; let T be DecoratedTree of D; let f be Function of D,E; clusterT * f -> DecoratedTree-like ; coherence f * T is DecoratedTree-like proofend; end; definition let D1, D2 be non empty set ; :: original:pr1 redefine func pr1 (D1,D2) -> Function of [:D1,D2:],D1; coherence pr1 (D1,D2) is Function of [:D1,D2:],D1 proofend; :: original:pr2 redefine func pr2 (D1,D2) -> Function of [:D1,D2:],D2; coherence pr2 (D1,D2) is Function of [:D1,D2:],D2 proofend; end; definition let D1, D2 be non empty set ; let T be DecoratedTree of D1,D2; funcT `1 -> DecoratedTree of D1 equals :: TREES_3:def 12 (pr1 (D1,D2)) * T; correctness coherence (pr1 (D1,D2)) * T is DecoratedTree of D1; ; funcT `2 -> DecoratedTree of D2 equals :: TREES_3:def 13 (pr2 (D1,D2)) * T; correctness coherence (pr2 (D1,D2)) * T is DecoratedTree of D2; ; end; :: deftheorem defines `1 TREES_3:def_12_:_ for D1, D2 being non empty set for T being DecoratedTree of D1,D2 holds T `1 = (pr1 (D1,D2)) * T; :: deftheorem defines `2 TREES_3:def_13_:_ for D1, D2 being non empty set for T being DecoratedTree of D1,D2 holds T `2 = (pr2 (D1,D2)) * T; theorem Th39: :: TREES_3:39 for D1, D2 being non empty set for T being DecoratedTree of D1,D2 for t being Element of dom T holds ( (T . t) `1 = (T `1) . t & (T `2) . t = (T . t) `2 ) proofend; theorem :: TREES_3:40 for D1, D2 being non empty set for T being DecoratedTree of D1,D2 holds <:(T `1),(T `2):> = T proofend; registration let T be finite Tree; cluster Leaves T -> non empty finite ; coherence ( Leaves T is finite & not Leaves T is empty ) proofend; end; definition let T be Tree; let S be non empty Subset of T; :: original:Element redefine mode Element of S -> Element of T; coherence for b1 being Element of S holds b1 is Element of T proofend; end; definition let T be finite Tree; :: original:Leaf redefine mode Leaf of T -> Element of Leaves T; coherence for b1 being Leaf of T holds b1 is Element of Leaves T by TREES_1:def_7; end; definition let T be finite Tree; mode T-Substitution of T -> Tree means :Def14: :: TREES_3:def 14 for t being Element of it holds ( t in T or ex l being Leaf of T st l is_a_proper_prefix_of t ); existence ex b1 being Tree st for t being Element of b1 holds ( t in T or ex l being Leaf of T st l is_a_proper_prefix_of t ) proofend; end; :: deftheorem Def14 defines T-Substitution TREES_3:def_14_:_ for T being finite Tree for b2 being Tree holds ( b2 is T-Substitution of T iff for t being Element of b2 holds ( t in T or ex l being Leaf of T st l is_a_proper_prefix_of t ) ); definition let T be finite Tree; let t be Leaf of T; let S be Tree; :: original:with-replacement redefine funcT with-replacement (t,S) -> T-Substitution of T; coherence T with-replacement (t,S) is T-Substitution of T proofend; end; registration let T be finite Tree; cluster non empty finite Tree-like for T-Substitution of T; existence ex b1 being T-Substitution of T st b1 is finite proofend; end; definition let n be Element of NAT ; mode T-Substitution of n is T-Substitution of elementary_tree n; end; theorem :: TREES_3:41 for T being Tree holds T is T-Substitution of 0 proofend; theorem :: TREES_3:42 for T1, T2 being Tree st T1 -level 1 c= T2 -level 1 & ( for n being Element of NAT st <*n*> in T1 holds T1 | <*n*> = T2 | <*n*> ) holds T1 c= T2 proofend; Lm3: for n being Element of NAT for p being FinSequence st n < len p holds ( n + 1 in dom p & p . (n + 1) in rng p ) proofend; begin theorem :: TREES_3:43 for T, T9 being Tree for p being FinSequence of NAT st p in Leaves T holds T c= T with-replacement (p,T9) proofend; theorem :: TREES_3:44 for T, T9 being DecoratedTree for p being Element of dom T holds (T with-replacement (p,T9)) . p = T9 . {} proofend; theorem :: TREES_3:45 for T, T9 being DecoratedTree for p, q being Element of dom T st not p is_a_prefix_of q holds (T with-replacement (p,T9)) . q = T . q proofend; theorem :: TREES_3:46 for T, T9 being DecoratedTree for p being Element of dom T for q being Element of dom T9 holds (T with-replacement (p,T9)) . (p ^ q) = T9 . q proofend; registration let T1, T2 be Tree; clusterT1 \/ T2 -> non empty Tree-like ; coherence ( not T1 \/ T2 is empty & T1 \/ T2 is Tree-like ) ; end; theorem Th47: :: TREES_3:47 for T1, T2 being Tree for p being Element of T1 \/ T2 holds ( ( p in T1 & p in T2 implies (T1 \/ T2) | p = (T1 | p) \/ (T2 | p) ) & ( not p in T1 implies (T1 \/ T2) | p = T2 | p ) & ( not p in T2 implies (T1 \/ T2) | p = T1 | p ) ) proofend; definition let p be FinSequence; assume B1: p is Tree-yielding ; func tree p -> Tree means :Def15: :: TREES_3:def 15 for x being set holds ( x in it iff ( x = {} or ex n being Element of NAT ex q being FinSequence st ( n < len p & q in p . (n + 1) & x = <*n*> ^ q ) ) ); existence ex b1 being Tree st for x being set holds ( x in b1 iff ( x = {} or ex n being Element of NAT ex q being FinSequence st ( n < len p & q in p . (n + 1) & x = <*n*> ^ q ) ) ) proofend; uniqueness for b1, b2 being Tree st ( for x being set holds ( x in b1 iff ( x = {} or ex n being Element of NAT ex q being FinSequence st ( n < len p & q in p . (n + 1) & x = <*n*> ^ q ) ) ) ) & ( for x being set holds ( x in b2 iff ( x = {} or ex n being Element of NAT ex q being FinSequence st ( n < len p & q in p . (n + 1) & x = <*n*> ^ q ) ) ) ) holds b1 = b2 proofend; end; :: deftheorem Def15 defines tree TREES_3:def_15_:_ for p being FinSequence st p is Tree-yielding holds for b2 being Tree holds ( b2 = tree p iff for x being set holds ( x in b2 iff ( x = {} or ex n being Element of NAT ex q being FinSequence st ( n < len p & q in p . (n + 1) & x = <*n*> ^ q ) ) ) ); definition let T be Tree; func ^ T -> Tree equals :: TREES_3:def 16 tree <*T*>; correctness coherence tree <*T*> is Tree; ; end; :: deftheorem defines ^ TREES_3:def_16_:_ for T being Tree holds ^ T = tree <*T*>; definition let T1, T2 be Tree; func tree (T1,T2) -> Tree equals :: TREES_3:def 17 tree <*T1,T2*>; correctness coherence tree <*T1,T2*> is Tree; ; end; :: deftheorem defines tree TREES_3:def_17_:_ for T1, T2 being Tree holds tree (T1,T2) = tree <*T1,T2*>; theorem :: TREES_3:48 for n being Element of NAT for p, q being FinSequence st p is Tree-yielding holds ( <*n*> ^ q in tree p iff ( n < len p & q in p . (n + 1) ) ) proofend; theorem Th49: :: TREES_3:49 for p being FinSequence st p is Tree-yielding holds ( (tree p) -level 1 = { <*n*> where n is Element of NAT : n < len p } & ( for n being Element of NAT st n < len p holds (tree p) | <*n*> = p . (n + 1) ) ) proofend; theorem :: TREES_3:50 for p, q being Tree-yielding FinSequence st tree p = tree q holds p = q proofend; theorem Th51: :: TREES_3:51 for p being FinSequence for p1, p2 being Tree-yielding FinSequence for T being Tree holds ( p in T iff <*(len p1)*> ^ p in tree ((p1 ^ <*T*>) ^ p2) ) proofend; theorem Th52: :: TREES_3:52 tree {} = elementary_tree 0 proofend; theorem Th53: :: TREES_3:53 for p being FinSequence st p is Tree-yielding holds elementary_tree (len p) c= tree p proofend; theorem Th54: :: TREES_3:54 for i being Element of NAT holds elementary_tree i = tree (i |-> (elementary_tree 0)) proofend; theorem Th55: :: TREES_3:55 for T being Tree for p being Tree-yielding FinSequence holds tree (p ^ <*T*>) = ((tree p) \/ (elementary_tree ((len p) + 1))) with-replacement (<*(len p)*>,T) proofend; theorem :: TREES_3:56 for p being Tree-yielding FinSequence holds tree (p ^ <*(elementary_tree 0)*>) = (tree p) \/ (elementary_tree ((len p) + 1)) proofend; theorem Th57: :: TREES_3:57 for p, q being Tree-yielding FinSequence for T1, T2 being Tree holds tree ((p ^ <*T1*>) ^ q) = (tree ((p ^ <*T2*>) ^ q)) with-replacement (<*(len p)*>,T1) proofend; theorem :: TREES_3:58 for T being Tree holds ^ T = (elementary_tree 1) with-replacement (<*0*>,T) proofend; theorem :: TREES_3:59 for T1, T2 being Tree holds tree (T1,T2) = ((elementary_tree 2) with-replacement (<*0*>,T1)) with-replacement (<*1*>,T2) proofend; registration let p be FinTree-yielding FinSequence; cluster tree p -> finite ; coherence tree p is finite proofend; end; registration let T be finite Tree; cluster ^ T -> finite ; coherence ^ T is finite ; end; registration let T1, T2 be finite Tree; cluster tree (T1,T2) -> finite ; coherence tree (T1,T2) is finite ; end; theorem Th60: :: TREES_3:60 for T being Tree for x being set holds ( x in ^ T iff ( x = {} or ex p being FinSequence st ( p in T & x = <*0*> ^ p ) ) ) proofend; theorem Th61: :: TREES_3:61 for T being Tree for p being FinSequence holds ( p in T iff <*0*> ^ p in ^ T ) proofend; theorem :: TREES_3:62 for T being Tree holds elementary_tree 1 c= ^ T proofend; theorem :: TREES_3:63 for T1, T2 being Tree st T1 c= T2 holds ^ T1 c= ^ T2 proofend; theorem :: TREES_3:64 for T1, T2 being Tree st ^ T1 = ^ T2 holds T1 = T2 proofend; theorem :: TREES_3:65 for T being Tree holds (^ T) | <*0*> = T proofend; theorem :: TREES_3:66 for T1, T2 being Tree holds (^ T1) with-replacement (<*0*>,T2) = ^ T2 proofend; theorem :: TREES_3:67 ^ (elementary_tree 0) = elementary_tree 1 proofend; theorem Th68: :: TREES_3:68 for T1, T2 being Tree for x being set holds ( x in tree (T1,T2) iff ( x = {} or ex p being FinSequence st ( ( p in T1 & x = <*0*> ^ p ) or ( p in T2 & x = <*1*> ^ p ) ) ) ) proofend; theorem Th69: :: TREES_3:69 for T1, T2 being Tree for p being FinSequence holds ( p in T1 iff <*0*> ^ p in tree (T1,T2) ) proofend; theorem Th70: :: TREES_3:70 for T1, T2 being Tree for p being FinSequence holds ( p in T2 iff <*1*> ^ p in tree (T1,T2) ) proofend; theorem :: TREES_3:71 for T1, T2 being Tree holds elementary_tree 2 c= tree (T1,T2) proofend; theorem :: TREES_3:72 for T1, T2, W1, W2 being Tree st T1 c= W1 & T2 c= W2 holds tree (T1,T2) c= tree (W1,W2) proofend; theorem :: TREES_3:73 for T1, T2, W1, W2 being Tree st tree (T1,T2) = tree (W1,W2) holds ( T1 = W1 & T2 = W2 ) proofend; theorem :: TREES_3:74 for T1, T2 being Tree holds ( (tree (T1,T2)) | <*0*> = T1 & (tree (T1,T2)) | <*1*> = T2 ) proofend; theorem :: TREES_3:75 for T, T1, T2 being Tree holds ( (tree (T1,T2)) with-replacement (<*0*>,T) = tree (T,T2) & (tree (T1,T2)) with-replacement (<*1*>,T) = tree (T1,T) ) proofend; theorem :: TREES_3:76 tree ((elementary_tree 0),(elementary_tree 0)) = elementary_tree 2 proofend; theorem Th77: :: TREES_3:77 for n being Element of NAT for w being FinTree-yielding FinSequence st ( for t being finite Tree st t in rng w holds height t <= n ) holds height (tree w) <= n + 1 proofend; theorem Th78: :: TREES_3:78 for w being FinTree-yielding FinSequence for t being finite Tree st t in rng w holds height (tree w) > height t proofend; theorem Th79: :: TREES_3:79 for w being FinTree-yielding FinSequence for t being finite Tree st t in rng w & ( for t9 being finite Tree st t9 in rng w holds height t9 <= height t ) holds height (tree w) = (height t) + 1 proofend; theorem :: TREES_3:80 for T being finite Tree holds height (^ T) = (height T) + 1 proofend; theorem :: TREES_3:81 for T1, T2 being finite Tree holds height (tree (T1,T2)) = (max ((height T1),(height T2))) + 1 proofend; begin :: from DTCONSTR registration let D be non empty set ; let t be Element of FinTrees D; cluster dom t -> finite ; coherence dom t is finite by Def8; end; definition let p be FinSequence; assume B1: p is DTree-yielding ; defpred S1[ Nat, set ] means ex T being DecoratedTree st ( T = p . $1 & $2 = T . {} ); func roots p -> FinSequence means :: TREES_3:def 18 ( dom it = dom p & ( for i being Element of NAT st i in dom p holds ex T being DecoratedTree st ( T = p . i & it . i = T . {} ) ) ); existence ex b1 being FinSequence st ( dom b1 = dom p & ( for i being Element of NAT st i in dom p holds ex T being DecoratedTree st ( T = p . i & b1 . i = T . {} ) ) ) proofend; uniqueness for b1, b2 being FinSequence st dom b1 = dom p & ( for i being Element of NAT st i in dom p holds ex T being DecoratedTree st ( T = p . i & b1 . i = T . {} ) ) & dom b2 = dom p & ( for i being Element of NAT st i in dom p holds ex T being DecoratedTree st ( T = p . i & b2 . i = T . {} ) ) holds b1 = b2 proofend; end; :: deftheorem defines roots TREES_3:def_18_:_ for p being FinSequence st p is DTree-yielding holds for b2 being FinSequence holds ( b2 = roots p iff ( dom b2 = dom p & ( for i being Element of NAT st i in dom p holds ex T being DecoratedTree st ( T = p . i & b2 . i = T . {} ) ) ) );