:: Sets and Functions of Trees and Joining Operations of Trees :: by Grzegorz Bancerek :: :: Received November 27, 1992 :: Copyright (c) 1992-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, SUBSET_1, FINSEQ_1, FUNCT_1, XXREAL_0, ORDINAL4, RELAT_1, TREES_1, XBOOLE_0, FINSET_1, TARSKI, TREES_2, FUNCT_2, CARD_1, FINSEQ_2, FUNCOP_1, FUNCT_6, ZFMISC_1, PARTFUN1, MCART_1, NAT_1, ARYTM_3, TREES_A, ARYTM_1, TREES_3; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, NAT_1, RELAT_1, FUNCT_1, FINSEQ_1, FINSET_1, DOMAIN_1, FUNCOP_1, RELSET_1, PARTFUN1, BINOP_1, FUNCT_2, FUNCT_3, FINSEQ_2, TREES_1, TREES_2, FUNCT_6, XXREAL_0; constructors PARTFUN1, BINOP_1, DOMAIN_1, FUNCT_3, SQUARE_1, NAT_1, FINSEQ_2, FUNCT_6, TREES_2, RELSET_1; registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FUNCT_2, FINSET_1, XXREAL_0, XREAL_0, NAT_1, FINSEQ_1, TREES_1, TREES_2, CARD_1, RELSET_1, FINSEQ_2; requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM; begin :: Finite sets reserve x,y,z for object, X,Y for set, i,k,n for Nat, p,q,r,s for FinSequence, w for FinSequence of NAT, f for Function; begin :: Sets of trees definition func Trees -> set means :: TREES_3:def 1 x in it iff x is Tree; end; registration cluster Trees -> non empty; end; definition func FinTrees -> Subset of Trees means :: TREES_3:def 2 x in it iff x is finite Tree; end; registration cluster FinTrees -> non empty; end; definition let IT be set; attr IT is constituted-Trees means :: TREES_3:def 3 for x st x in IT holds x is Tree; attr IT is constituted-FinTrees means :: TREES_3:def 4 for x st x in IT holds x is finite Tree; attr IT is constituted-DTrees means :: TREES_3:def 5 for x st x in IT holds x is DecoratedTree; end; theorem :: TREES_3:1 X is constituted-Trees iff X c= Trees; theorem :: TREES_3:2 X is constituted-FinTrees iff X c= FinTrees; theorem :: TREES_3:3 X is constituted-Trees & Y is constituted-Trees iff X \/ Y is constituted-Trees; theorem :: TREES_3:4 X is constituted-Trees & Y is constituted-Trees implies X \+\ Y is constituted-Trees; theorem :: TREES_3:5 X is constituted-Trees implies X /\ Y is constituted-Trees & Y /\ X is constituted-Trees & X \ Y is constituted-Trees; theorem :: TREES_3:6 X is constituted-FinTrees & Y is constituted-FinTrees iff X \/ Y is constituted-FinTrees; theorem :: TREES_3:7 X is constituted-FinTrees & Y is constituted-FinTrees implies X \+\ Y is constituted-FinTrees; theorem :: TREES_3:8 X is constituted-FinTrees implies X /\ Y is constituted-FinTrees & Y /\ X is constituted-FinTrees & X \ Y is constituted-FinTrees; theorem :: TREES_3:9 X is constituted-DTrees & Y is constituted-DTrees iff X \/ Y is constituted-DTrees; theorem :: TREES_3:10 X is constituted-DTrees & Y is constituted-DTrees implies X \+\ Y is constituted-DTrees; theorem :: TREES_3:11 X is constituted-DTrees implies X /\ Y is constituted-DTrees & Y /\ X is constituted-DTrees & X \ Y is constituted-DTrees; registration cluster empty -> constituted-Trees constituted-FinTrees constituted-DTrees for set; end; theorem :: TREES_3:12 {x} is constituted-Trees iff x is Tree; theorem :: TREES_3:13 for x being object holds {x} is constituted-FinTrees iff x is finite Tree; theorem :: TREES_3:14 {x} is constituted-DTrees iff x is DecoratedTree; theorem :: TREES_3:15 {x,y} is constituted-Trees iff x is Tree & y is Tree; theorem :: TREES_3:16 {x,y} is constituted-FinTrees iff x is finite Tree & y is finite Tree; theorem :: TREES_3:17 {x,y} is constituted-DTrees iff x is DecoratedTree & y is DecoratedTree; theorem :: TREES_3:18 X is constituted-Trees & Y c= X implies Y is constituted-Trees; theorem :: TREES_3:19 X is constituted-FinTrees & Y c= X implies Y is constituted-FinTrees; theorem :: TREES_3:20 X is constituted-DTrees & Y c= X implies Y is constituted-DTrees; registration cluster finite constituted-Trees constituted-FinTrees non empty for set; cluster finite constituted-DTrees non empty for set; end; registration cluster constituted-FinTrees -> constituted-Trees for set; end; registration let X be constituted-Trees set; cluster -> constituted-Trees for Subset of X; end; registration let X be constituted-FinTrees set; cluster -> constituted-FinTrees for Subset of X; end; registration let X be constituted-DTrees set; cluster -> constituted-DTrees for Subset of X; end; registration let D be constituted-Trees non empty set; cluster -> non empty Tree-like for Element of D; end; registration let D be constituted-FinTrees non empty set; cluster -> finite for Element of D; end; registration cluster constituted-DTrees -> functional for set; end; registration let D be constituted-DTrees non empty set; cluster -> DecoratedTree-like for Element of D; end; registration cluster Trees -> constituted-Trees; end; registration cluster FinTrees -> constituted-FinTrees; end; registration cluster constituted-FinTrees non empty for Subset of Trees; end; definition let D be non empty set; mode DTree-set of D -> non empty set means :: TREES_3:def 6 for x st x in it holds x is DecoratedTree of D; end; registration let D be non empty set; cluster -> constituted-DTrees for DTree-set of D; end; registration let D be non empty set; cluster finite non empty for DTree-set of D; end; registration let D be non empty set, E be non empty DTree-set of D; cluster -> D-valued for Element of E; end; definition let T be Tree, D be non empty set; redefine func Funcs(T,D) -> non empty DTree-set of D; end; registration let T be Tree, D be non empty set; cluster -> DecoratedTree-like for Function of T,D; end; definition let D be non empty set; func Trees(D) -> DTree-set of D means :: TREES_3:def 7 for T being DecoratedTree of D holds T in it; end; registration let D be non empty set; cluster Trees(D) -> non empty; end; definition let D be non empty set; func FinTrees(D) -> DTree-set of D means :: TREES_3:def 8 for T being DecoratedTree of D holds dom T is finite iff T in it; end; theorem :: TREES_3:21 for D being non empty set holds FinTrees D c= Trees D; begin :: Functions yielding trees definition let IT be Function; attr IT is Tree-yielding means :: TREES_3:def 9 rng IT is constituted-Trees; attr IT is FinTree-yielding means :: TREES_3:def 10 rng IT is constituted-FinTrees; attr IT is DTree-yielding means :: TREES_3:def 11 rng IT is constituted-DTrees; end; registration cluster empty -> Tree-yielding FinTree-yielding DTree-yielding for Function; end; theorem :: TREES_3:22 f is Tree-yielding iff for x st x in dom f holds f.x is Tree; theorem :: TREES_3:23 f is FinTree-yielding iff for x st x in dom f holds f.x is finite Tree; theorem :: TREES_3:24 f is DTree-yielding iff for x st x in dom f holds f.x is DecoratedTree; theorem :: TREES_3:25 p is Tree-yielding & q is Tree-yielding iff p^q is Tree-yielding; theorem :: TREES_3:26 p is FinTree-yielding & q is FinTree-yielding iff p^q is FinTree-yielding; theorem :: TREES_3:27 p is DTree-yielding & q is DTree-yielding iff p^q is DTree-yielding; theorem :: TREES_3:28 <*x*> is Tree-yielding iff x is Tree; theorem :: TREES_3:29 for x being object holds <*x*> is FinTree-yielding iff x is finite Tree; theorem :: TREES_3:30 <*x*> is DTree-yielding iff x is DecoratedTree; theorem :: TREES_3:31 <*x,y*> is Tree-yielding iff x is Tree & y is Tree; theorem :: TREES_3:32 <*x,y*> is FinTree-yielding iff x is finite Tree & y is finite Tree; theorem :: TREES_3:33 <*x,y*> is DTree-yielding iff x is DecoratedTree & y is DecoratedTree; theorem :: TREES_3:34 i <> 0 implies (i |-> x is Tree-yielding iff x is Tree); theorem :: TREES_3:35 i <> 0 implies (i |-> x is FinTree-yielding iff x is finite Tree); theorem :: TREES_3:36 i <> 0 implies (i |-> x is DTree-yielding iff x is DecoratedTree); registration cluster Tree-yielding FinTree-yielding non empty for FinSequence; cluster DTree-yielding non empty for FinSequence; end; registration cluster Tree-yielding FinTree-yielding non empty for Function; cluster DTree-yielding non empty for Function; end; registration cluster FinTree-yielding -> Tree-yielding for Function; end; registration let D be constituted-Trees non empty set; cluster -> Tree-yielding for FinSequence of D; end; registration let p,q be Tree-yielding FinSequence; cluster p^q -> Tree-yielding; end; registration let D be constituted-FinTrees non empty set; cluster -> FinTree-yielding for FinSequence of D; end; registration let p,q be FinTree-yielding FinSequence; cluster p^q -> FinTree-yielding; end; registration let D be constituted-DTrees non empty set; cluster -> DTree-yielding for FinSequence of D; end; registration let p,q be DTree-yielding FinSequence; cluster p^q -> DTree-yielding; end; registration let T be Tree; cluster <*T*> -> Tree-yielding non empty; let S be Tree; cluster <*T,S*> -> Tree-yielding non empty; end; registration let n be Nat, T be Tree; cluster n |-> T -> Tree-yielding; end; registration let T be finite Tree; cluster <*T*> -> FinTree-yielding; let S be finite Tree; cluster <*T,S*> -> FinTree-yielding; end; registration let n be Nat, T be finite Tree; cluster n |-> T -> FinTree-yielding; end; registration let T be DecoratedTree; cluster <*T*> -> DTree-yielding non empty; let S be DecoratedTree; cluster <*T,S*> -> DTree-yielding non empty; end; registration let n be Nat, T be DecoratedTree; cluster n |-> T -> DTree-yielding; end; registration cluster DTree-yielding -> Function-yielding for Function; end; theorem :: TREES_3:37 for f being DTree-yielding Function holds dom doms f = dom f & doms f is Tree-yielding; registration let p be DTree-yielding FinSequence; cluster doms p -> Tree-yielding FinSequence-like; end; theorem :: TREES_3:38 for p being DTree-yielding FinSequence holds len doms p = len p; begin :: Trees decorated by Cartesian product and structure of substitution 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; 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; end; registration let D,E be non empty set; let T be DecoratedTree of D; let f be Function of D,E; cluster f*T -> DecoratedTree-like; end; definition let D1,D2 be non empty set; redefine func pr1(D1,D2) -> Function of [:D1,D2:], D1; redefine func pr2(D1,D2) -> Function of [:D1,D2:], D2; end; definition let D1,D2 be non empty set, T be DecoratedTree of D1,D2; func T`1 -> DecoratedTree of D1 equals :: TREES_3:def 12 pr1(D1,D2)*T; func T`2 -> DecoratedTree of D2 equals :: TREES_3:def 13 pr2(D1,D2)*T; end; theorem :: TREES_3:39 for D1,D2 being non empty set, T being DecoratedTree of D1,D2, t being Element of dom T holds (T.t)`1 = T`1.t & T`2.t = (T.t)`2; theorem :: TREES_3:40 for D1,D2 being non empty set, T being DecoratedTree of D1,D2 holds <:T`1,T`2:> = T; registration let T be finite Tree; cluster Leaves T -> finite non empty; end; definition let T be Tree, S be non empty Subset of T; redefine mode Element of S -> Element of T; end; definition let T be finite Tree; redefine mode Leaf of T -> Element of Leaves T; end; definition let T be finite Tree; mode T-Substitution of T -> Tree means :: 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; end; definition let T be finite Tree, t be Leaf of T, S be Tree; redefine func T with-replacement (t,S) -> T-Substitution of T; end; registration let T be finite Tree; cluster finite for T-Substitution of T; end; definition let n; 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; 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; begin :: Joining of trees theorem :: TREES_3:43 for T,T9 being Tree, p being FinSequence of NAT st p in Leaves T holds T c= T with-replacement (p,T9); theorem :: TREES_3:44 for T,T9 being DecoratedTree, p being Element of dom T holds (T with-replacement (p,T9)).p = T9.{}; theorem :: TREES_3:45 for T,T9 being DecoratedTree, p,q being Element of dom T st not p is_a_prefix_of q holds (T with-replacement (p,T9)).q = T.q; theorem :: TREES_3:46 for T,T9 being DecoratedTree, p being Element of dom T, q being Element of dom T9 holds (T with-replacement (p,T9)).(p^q) = T9.q; registration let T1,T2 be Tree; cluster T1 \/ T2 -> non empty Tree-like; end; theorem :: TREES_3:47 for T1,T2 being Tree, 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); definition let p such that p is Tree-yielding; func tree p -> Tree means :: TREES_3:def 15 x in it iff x = {} or ex n,q st n < len p & q in p.(n+1) & x = <*n*>^q; end; definition let T be Tree; func ^T -> Tree equals :: TREES_3:def 16 tree<*T*>; end; definition let T1,T2 be Tree; func tree(T1,T2) -> Tree equals :: TREES_3:def 17 tree(<*T1,T2*>); end; theorem :: TREES_3:48 p is Tree-yielding implies (<*n*>^q in tree(p) iff n < len p & q in p.(n+ 1 ) ); theorem :: TREES_3:49 p is Tree-yielding implies tree(p)-level 1 = {<*n*>: n < len p} & for n being Element of NAT st n < len p holds (tree(p))|<*n*> = p.(n+1); theorem :: TREES_3:50 for p,q being Tree-yielding FinSequence st tree(p) = tree(q) holds p = q; theorem :: TREES_3:51 for p1,p2 being Tree-yielding FinSequence, T being Tree holds p in T iff <*len p1*>^p in tree(p1^<*T*>^p2); theorem :: TREES_3:52 tree({}) = elementary_tree 0; theorem :: TREES_3:53 p is Tree-yielding implies elementary_tree len p c= tree(p); theorem :: TREES_3:54 elementary_tree i = tree(i|->elementary_tree 0); theorem :: TREES_3:55 for T being Tree, p being Tree-yielding FinSequence holds tree(p^<*T*>) = (tree(p) \/ elementary_tree (len p + 1)) with-replacement (<*len p*>, T); theorem :: TREES_3:56 for p being Tree-yielding FinSequence holds tree(p^<*elementary_tree 0*>) = tree(p) \/ elementary_tree (len p + 1); theorem :: TREES_3:57 for p, q being Tree-yielding FinSequence for T1,T2 be Tree holds tree(p^<*T1*>^q) = tree(p^<*T2*>^q) with-replacement(<*len p*>,T1); definition let n be Nat; redefine func <*n*> -> FinSequence of NAT; end; theorem :: TREES_3:58 for T being Tree holds ^T = elementary_tree 1 with-replacement(<*0*>, T); theorem :: TREES_3:59 for T1,T2 being Tree holds tree(T1,T2) = (elementary_tree 2 with-replacement(<*0*>,T1)) with-replacement (<*1*>, T2); registration let p be FinTree-yielding FinSequence; cluster tree(p) -> finite; end; registration let T be finite Tree; cluster ^T -> finite; end; registration let T1,T2 be finite Tree; cluster tree(T1,T2) -> finite; end; theorem :: TREES_3:60 for T being Tree, x being object holds x in ^T iff x = {} or ex p st p in T & x = <*0*>^p; theorem :: TREES_3:61 for T being Tree, p being FinSequence holds p in T iff <*0*>^p in ^T; theorem :: TREES_3:62 for T being Tree holds elementary_tree 1 c= ^T; theorem :: TREES_3:63 for T1,T2 being Tree st T1 c= T2 holds ^T1 c= ^T2; theorem :: TREES_3:64 for T1,T2 being Tree st ^T1 = ^T2 holds T1 = T2; theorem :: TREES_3:65 for T being Tree holds (^T)|<*0*> = T; theorem :: TREES_3:66 for T1,T2 being Tree holds ^T1 with-replacement (<*0*>,T2) = ^T2; theorem :: TREES_3:67 ^elementary_tree 0 = elementary_tree 1; theorem :: TREES_3:68 for T1,T2 being Tree, x being object holds x in tree(T1,T2) iff x = {} or ex p st p in T1 & x = <*0*>^p or p in T2 & x = <*1*>^p; theorem :: TREES_3:69 for T1,T2 being Tree, p being FinSequence holds p in T1 iff <*0*>^p in tree(T1,T2); theorem :: TREES_3:70 for T1,T2 being Tree, p being FinSequence holds p in T2 iff <*1*>^p in tree(T1,T2); theorem :: TREES_3:71 for T1,T2 being Tree holds elementary_tree 2 c= tree(T1,T2); 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); theorem :: TREES_3:73 for T1,T2, W1,W2 being Tree st tree(T1,T2) = tree(W1,W2) holds T1 = W1 & T2 = W2; theorem :: TREES_3:74 for T1,T2 being Tree holds tree(T1,T2)|<*0*> = T1 & tree(T1,T2)|<*1*> = T2; 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); theorem :: TREES_3:76 tree(elementary_tree 0, elementary_tree 0) = elementary_tree 2; reserve w for FinTree-yielding FinSequence; theorem :: TREES_3:77 for w st for t being finite Tree st t in rng w holds height t <= n holds height tree(w) <= n+1; theorem :: TREES_3:78 for t being finite Tree st t in rng w holds height tree(w) > height t; theorem :: TREES_3:79 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; theorem :: TREES_3:80 for T being finite Tree holds height ^T = (height T) + 1; theorem :: TREES_3:81 for T1,T2 being finite Tree holds height tree(T1,T2) = max(height T1, height T2)+1; begin :: Addenda :: from DTCONSTR registration let D be non empty set, t be Element of FinTrees D; cluster dom t -> finite; end; definition let p be FinSequence such that p is DTree-yielding; func roots p -> FinSequence means :: TREES_3:def 18 dom it = dom p & for i being Element of NAT st i in dom p ex T being DecoratedTree st T = p.i & it.i = T.{}; end;