:: Joining of Decorated Trees :: by Grzegorz Bancerek :: :: Received October 8, 1993 :: Copyright (c) 1993-2012 Association of Mizar Users begin definition let T be DecoratedTree; mode Node of T is Element of dom T; end; Lm1: now__::_thesis:_for_x,_y_being_set_ for_p_being_FinSequence_of_x_st_(_y_in_dom_p_or_y_in_dom_p_)_holds_ p_._y_in_x let x, y be set ; ::_thesis: for p being FinSequence of x st ( y in dom p or y in dom p ) holds p . y in x let p be FinSequence of x; ::_thesis: ( ( y in dom p or y in dom p ) implies p . y in x ) assume ( y in dom p or y in dom p ) ; ::_thesis: p . y in x then A1: p . y in rng p by FUNCT_1:def_3; rng p c= x by FINSEQ_1:def_4; hence p . y in x by A1; ::_thesis: verum end; definition let T1, T2 be DecoratedTree; redefine pred T1 = T2 means :: TREES_4:def 1 ( dom T1 = dom T2 & ( for p being Node of T1 holds T1 . p = T2 . p ) ); compatibility ( T1 = T2 iff ( dom T1 = dom T2 & ( for p being Node of T1 holds T1 . p = T2 . p ) ) ) proofend; end; :: deftheorem defines = TREES_4:def_1_:_ for T1, T2 being DecoratedTree holds ( T1 = T2 iff ( dom T1 = dom T2 & ( for p being Node of T1 holds T1 . p = T2 . p ) ) ); theorem Th1: :: TREES_4:1 for i, j being Element of NAT st elementary_tree i c= elementary_tree j holds i <= j proofend; theorem Th2: :: TREES_4:2 for i, j being Element of NAT st elementary_tree i = elementary_tree j holds i = j proofend; Lm2: 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; Lm3: now__::_thesis:_for_n_being_Element_of_NAT_ for_x_being_set_ for_p_being_FinSequence_of_x_st_n_<_len_p_holds_ p_._(n_+_1)_in_x let n be Element of NAT ; ::_thesis: for x being set for p being FinSequence of x st n < len p holds p . (n + 1) in x let x be set ; ::_thesis: for p being FinSequence of x st n < len p holds p . (n + 1) in x let p be FinSequence of x; ::_thesis: ( n < len p implies p . (n + 1) in x ) assume n < len p ; ::_thesis: p . (n + 1) in x then A1: p . (n + 1) in rng p by Lm2; rng p c= x by FINSEQ_1:def_4; hence p . (n + 1) in x by A1; ::_thesis: verum end; definition let x be set ; func root-tree x -> DecoratedTree equals :: TREES_4:def 2 (elementary_tree 0) --> x; correctness coherence (elementary_tree 0) --> x is DecoratedTree; ; end; :: deftheorem defines root-tree TREES_4:def_2_:_ for x being set holds root-tree x = (elementary_tree 0) --> x; definition let D be non empty set ; let d be Element of D; :: original:root-tree redefine func root-tree d -> Element of FinTrees D; coherence root-tree d is Element of FinTrees D proofend; end; theorem Th3: :: TREES_4:3 for x being set holds ( dom (root-tree x) = elementary_tree 0 & (root-tree x) . {} = x ) proofend; theorem :: TREES_4:4 for x, y being set st root-tree x = root-tree y holds x = y proofend; theorem Th5: :: TREES_4:5 for T being DecoratedTree st dom T = elementary_tree 0 holds T = root-tree (T . {}) proofend; theorem :: TREES_4:6 for x being set holds root-tree x = {[{},x]} proofend; definition let x be set ; let p be FinSequence; funcx -flat_tree p -> DecoratedTree means :Def3: :: TREES_4:def 3 ( dom it = elementary_tree (len p) & it . {} = x & ( for n being Element of NAT st n < len p holds it . <*n*> = p . (n + 1) ) ); existence ex b1 being DecoratedTree st ( dom b1 = elementary_tree (len p) & b1 . {} = x & ( for n being Element of NAT st n < len p holds b1 . <*n*> = p . (n + 1) ) ) proofend; uniqueness for b1, b2 being DecoratedTree st dom b1 = elementary_tree (len p) & b1 . {} = x & ( for n being Element of NAT st n < len p holds b1 . <*n*> = p . (n + 1) ) & dom b2 = elementary_tree (len p) & b2 . {} = x & ( for n being Element of NAT st n < len p holds b2 . <*n*> = p . (n + 1) ) holds b1 = b2 proofend; end; :: deftheorem Def3 defines -flat_tree TREES_4:def_3_:_ for x being set for p being FinSequence for b3 being DecoratedTree holds ( b3 = x -flat_tree p iff ( dom b3 = elementary_tree (len p) & b3 . {} = x & ( for n being Element of NAT st n < len p holds b3 . <*n*> = p . (n + 1) ) ) ); theorem :: TREES_4:7 for x, y being set for p, q being FinSequence st x -flat_tree p = y -flat_tree q holds ( x = y & p = q ) proofend; theorem Th8: :: TREES_4:8 for j, i being Element of NAT st j < i holds (elementary_tree i) | <*j*> = elementary_tree 0 proofend; theorem Th9: :: TREES_4:9 for x being set for i being Element of NAT for p being FinSequence st i < len p holds (x -flat_tree p) | <*i*> = root-tree (p . (i + 1)) proofend; definition let x be set ; let p be FinSequence; assume B1: p is DTree-yielding ; funcx -tree p -> DecoratedTree means :Def4: :: TREES_4:def 4 ( ex q being DTree-yielding FinSequence st ( p = q & dom it = tree (doms q) ) & it . {} = x & ( for n being Element of NAT st n < len p holds it | <*n*> = p . (n + 1) ) ); existence ex b1 being DecoratedTree st ( ex q being DTree-yielding FinSequence st ( p = q & dom b1 = tree (doms q) ) & b1 . {} = x & ( for n being Element of NAT st n < len p holds b1 | <*n*> = p . (n + 1) ) ) proofend; uniqueness for b1, b2 being DecoratedTree st ex q being DTree-yielding FinSequence st ( p = q & dom b1 = tree (doms q) ) & b1 . {} = x & ( for n being Element of NAT st n < len p holds b1 | <*n*> = p . (n + 1) ) & ex q being DTree-yielding FinSequence st ( p = q & dom b2 = tree (doms q) ) & b2 . {} = x & ( for n being Element of NAT st n < len p holds b2 | <*n*> = p . (n + 1) ) holds b1 = b2 proofend; end; :: deftheorem Def4 defines -tree TREES_4:def_4_:_ for x being set for p being FinSequence st p is DTree-yielding holds for b3 being DecoratedTree holds ( b3 = x -tree p iff ( ex q being DTree-yielding FinSequence st ( p = q & dom b3 = tree (doms q) ) & b3 . {} = x & ( for n being Element of NAT st n < len p holds b3 | <*n*> = p . (n + 1) ) ) ); definition let x be set ; let T be DecoratedTree; funcx -tree T -> DecoratedTree equals :: TREES_4:def 5 x -tree <*T*>; correctness coherence x -tree <*T*> is DecoratedTree; ; end; :: deftheorem defines -tree TREES_4:def_5_:_ for x being set for T being DecoratedTree holds x -tree T = x -tree <*T*>; definition let x be set ; let T1, T2 be DecoratedTree; funcx -tree (T1,T2) -> DecoratedTree equals :: TREES_4:def 6 x -tree <*T1,T2*>; correctness coherence x -tree <*T1,T2*> is DecoratedTree; ; end; :: deftheorem defines -tree TREES_4:def_6_:_ for x being set for T1, T2 being DecoratedTree holds x -tree (T1,T2) = x -tree <*T1,T2*>; theorem Th10: :: TREES_4:10 for x being set for p being DTree-yielding FinSequence holds dom (x -tree p) = tree (doms p) proofend; theorem Th11: :: TREES_4:11 for y, x being set for p being DTree-yielding FinSequence holds ( y in dom (x -tree p) iff ( y = {} or ex i being Element of NAT ex T being DecoratedTree ex q being Node of T st ( i < len p & T = p . (i + 1) & y = <*i*> ^ q ) ) ) proofend; theorem Th12: :: TREES_4:12 for x being set for p being DTree-yielding FinSequence for i being Element of NAT for T being DecoratedTree for q being Node of T st i < len p & T = p . (i + 1) holds (x -tree p) . (<*i*> ^ q) = T . q proofend; theorem :: TREES_4:13 for x being set for T being DecoratedTree holds dom (x -tree T) = ^ (dom T) proofend; theorem :: TREES_4:14 for x being set for T1, T2 being DecoratedTree holds dom (x -tree (T1,T2)) = tree ((dom T1),(dom T2)) proofend; theorem :: TREES_4:15 for x, y being set for p, q being DTree-yielding FinSequence st x -tree p = y -tree q holds ( x = y & p = q ) proofend; theorem :: TREES_4:16 for x, y being set for p being FinSequence st root-tree x = y -flat_tree p holds ( x = y & p = {} ) proofend; theorem :: TREES_4:17 for x, y being set for p being FinSequence st root-tree x = y -tree p & p is DTree-yielding holds ( x = y & p = {} ) proofend; theorem :: TREES_4:18 for x, y being set for p, q being FinSequence st x -flat_tree p = y -tree q & q is DTree-yielding holds ( x = y & len p = len q & ( for i being Element of NAT st i in dom p holds q . i = root-tree (p . i) ) ) proofend; theorem :: TREES_4:19 for x being set for p being DTree-yielding FinSequence for n being Element of NAT for q being FinSequence st <*n*> ^ q in dom (x -tree p) holds (x -tree p) . (<*n*> ^ q) = p .. ((n + 1),q) proofend; theorem :: TREES_4:20 for x being set holds ( x -flat_tree {} = root-tree x & x -tree {} = root-tree x ) proofend; theorem :: TREES_4:21 for x, y being set holds x -flat_tree <*y*> = ((elementary_tree 1) --> x) with-replacement (<*0*>,(root-tree y)) proofend; theorem :: TREES_4:22 for x being set for T being DecoratedTree holds x -tree <*T*> = ((elementary_tree 1) --> x) with-replacement (<*0*>,T) proofend; registration let D be non empty set ; let d be Element of D; let p be FinSequence of D; clusterd -flat_tree p -> D -valued ; coherence d -flat_tree p is D -valued proofend; end; registration let D be non empty set ; let F be non empty DTree-set of D; let d be Element of D; let p be FinSequence of F; clusterd -tree p -> D -valued ; coherence d -tree p is D -valued proofend; end; registration let D be non empty set ; let d be Element of D; let T be DecoratedTree of D; clusterd -tree T -> D -valued ; coherence d -tree T is D -valued proofend; end; registration let D be non empty set ; let d be Element of D; let T1, T2 be DecoratedTree of D; clusterd -tree (T1,T2) -> D -valued ; coherence d -tree (T1,T2) is D -valued proofend; end; definition let D be non empty set ; let p be FinSequence of FinTrees D; :: original:doms redefine func doms p -> FinSequence of FinTrees ; coherence doms p is FinSequence of FinTrees proofend; end; definition let D be non empty set ; let d be Element of D; let p be FinSequence of FinTrees D; :: original:-tree redefine funcd -tree p -> Element of FinTrees D; coherence d -tree p is Element of FinTrees D proofend; end; definition let D be non empty set ; let x be Subset of D; :: original:FinSequence redefine mode FinSequence of x -> FinSequence of D; coherence for b1 being FinSequence of x holds b1 is FinSequence of D proofend; end; registration let D be non empty constituted-DTrees set ; let X be Subset of D; cluster -> DTree-yielding for FinSequence of X; coherence for b1 being FinSequence of X holds b1 is DTree-yielding ; end; begin scheme :: TREES_4:sch 1 ExpandTree{ F1() -> Tree, F2() -> Tree, P1[ set ] } : ex T being Tree st for p being FinSequence holds ( p in T iff ( p in F1() or ex q being Element of F1() ex r being Element of F2() st ( P1[q] & p = q ^ r ) ) ) proofend; definition let T, T9 be DecoratedTree; let x be set ; func(T,x) <- T9 -> DecoratedTree means :Def7: :: TREES_4:def 7 ( ( for p being FinSequence holds ( p in dom it iff ( p in dom T or ex q being Node of T ex r being Node of T9 st ( q in Leaves (dom T) & T . q = x & p = q ^ r ) ) ) ) & ( for p being Node of T st ( not p in Leaves (dom T) or T . p <> x ) holds it . p = T . p ) & ( for p being Node of T for q being Node of T9 st p in Leaves (dom T) & T . p = x holds it . (p ^ q) = T9 . q ) ); existence ex b1 being DecoratedTree st ( ( for p being FinSequence holds ( p in dom b1 iff ( p in dom T or ex q being Node of T ex r being Node of T9 st ( q in Leaves (dom T) & T . q = x & p = q ^ r ) ) ) ) & ( for p being Node of T st ( not p in Leaves (dom T) or T . p <> x ) holds b1 . p = T . p ) & ( for p being Node of T for q being Node of T9 st p in Leaves (dom T) & T . p = x holds b1 . (p ^ q) = T9 . q ) ) proofend; uniqueness for b1, b2 being DecoratedTree st ( for p being FinSequence holds ( p in dom b1 iff ( p in dom T or ex q being Node of T ex r being Node of T9 st ( q in Leaves (dom T) & T . q = x & p = q ^ r ) ) ) ) & ( for p being Node of T st ( not p in Leaves (dom T) or T . p <> x ) holds b1 . p = T . p ) & ( for p being Node of T for q being Node of T9 st p in Leaves (dom T) & T . p = x holds b1 . (p ^ q) = T9 . q ) & ( for p being FinSequence holds ( p in dom b2 iff ( p in dom T or ex q being Node of T ex r being Node of T9 st ( q in Leaves (dom T) & T . q = x & p = q ^ r ) ) ) ) & ( for p being Node of T st ( not p in Leaves (dom T) or T . p <> x ) holds b2 . p = T . p ) & ( for p being Node of T for q being Node of T9 st p in Leaves (dom T) & T . p = x holds b2 . (p ^ q) = T9 . q ) holds b1 = b2 proofend; end; :: deftheorem Def7 defines <- TREES_4:def_7_:_ for T, T9 being DecoratedTree for x being set for b4 being DecoratedTree holds ( b4 = (T,x) <- T9 iff ( ( for p being FinSequence holds ( p in dom b4 iff ( p in dom T or ex q being Node of T ex r being Node of T9 st ( q in Leaves (dom T) & T . q = x & p = q ^ r ) ) ) ) & ( for p being Node of T st ( not p in Leaves (dom T) or T . p <> x ) holds b4 . p = T . p ) & ( for p being Node of T for q being Node of T9 st p in Leaves (dom T) & T . p = x holds b4 . (p ^ q) = T9 . q ) ) ); registration let D be non empty set ; let T, T9 be DecoratedTree of D; let x be set ; cluster(T,x) <- T9 -> D -valued ; coherence (T,x) <- T9 is D -valued proofend; end; theorem :: TREES_4:23 for T, T9 being DecoratedTree for x being set st ( not x in rng T or not x in Leaves T ) holds (T,x) <- T9 = T proofend; begin theorem Th24: :: TREES_4:24 for D1, D2 being non empty set for T being DecoratedTree of D1,D2 holds ( dom (T `1) = dom T & dom (T `2) = dom T ) proofend; theorem Th25: :: TREES_4:25 for D1, D2 being non empty set for d1 being Element of D1 for d2 being Element of D2 holds ( (root-tree [d1,d2]) `1 = root-tree d1 & (root-tree [d1,d2]) `2 = root-tree d2 ) proofend; theorem :: TREES_4:26 for x, y being set holds <:(root-tree x),(root-tree y):> = root-tree [x,y] proofend; theorem Th27: :: TREES_4:27 for D1, D2 being non empty set for d1 being Element of D1 for d2 being Element of D2 for F being non empty DTree-set of D1,D2 for F1 being non empty DTree-set of D1 for p being FinSequence of F for p1 being FinSequence of F1 st dom p1 = dom p & ( for i being Element of NAT st i in dom p holds for T being DecoratedTree of D1,D2 st T = p . i holds p1 . i = T `1 ) holds ([d1,d2] -tree p) `1 = d1 -tree p1 proofend; theorem Th28: :: TREES_4:28 for D1, D2 being non empty set for d1 being Element of D1 for d2 being Element of D2 for F being non empty DTree-set of D1,D2 for F2 being non empty DTree-set of D2 for p being FinSequence of F for p2 being FinSequence of F2 st dom p2 = dom p & ( for i being Element of NAT st i in dom p holds for T being DecoratedTree of D1,D2 st T = p . i holds p2 . i = T `2 ) holds ([d1,d2] -tree p) `2 = d2 -tree p2 proofend; theorem Th29: :: TREES_4:29 for D1, D2 being non empty set for d1 being Element of D1 for d2 being Element of D2 for F being non empty DTree-set of D1,D2 for p being FinSequence of F ex p1 being FinSequence of Trees D1 st ( dom p1 = dom p & ( for i being Element of NAT st i in dom p holds ex T being Element of F st ( T = p . i & p1 . i = T `1 ) ) & ([d1,d2] -tree p) `1 = d1 -tree p1 ) proofend; theorem Th30: :: TREES_4:30 for D1, D2 being non empty set for d1 being Element of D1 for d2 being Element of D2 for F being non empty DTree-set of D1,D2 for p being FinSequence of F ex p2 being FinSequence of Trees D2 st ( dom p2 = dom p & ( for i being Element of NAT st i in dom p holds ex T being Element of F st ( T = p . i & p2 . i = T `2 ) ) & ([d1,d2] -tree p) `2 = d2 -tree p2 ) proofend; theorem :: TREES_4:31 for D1, D2 being non empty set for d1 being Element of D1 for d2 being Element of D2 for p being FinSequence of FinTrees [:D1,D2:] ex p1 being FinSequence of FinTrees D1 st ( dom p1 = dom p & ( for i being Element of NAT st i in dom p holds ex T being Element of FinTrees [:D1,D2:] st ( T = p . i & p1 . i = T `1 ) ) & ([d1,d2] -tree p) `1 = d1 -tree p1 ) proofend; theorem :: TREES_4:32 for D1, D2 being non empty set for d1 being Element of D1 for d2 being Element of D2 for p being FinSequence of FinTrees [:D1,D2:] ex p2 being FinSequence of FinTrees D2 st ( dom p2 = dom p & ( for i being Element of NAT st i in dom p holds ex T being Element of FinTrees [:D1,D2:] st ( T = p . i & p2 . i = T `2 ) ) & ([d1,d2] -tree p) `2 = d2 -tree p2 ) proofend;