Volume 4, 1992

University of Bialystok

Copyright (c) 1992 Association of Mizar Users

### The abstract of the Mizar article:

### Sets and Functions of Trees and Joining Operations of Trees

**by****Grzegorz Bancerek**- Received November 27, 1992
- MML identifier: TREES_3

- [ Mizar article, MML identifier index ]

environ vocabulary FINSEQ_1, FUNCT_1, RELAT_1, FINSET_1, MCART_1, TREES_1, TREES_2, BOOLE, FUNCT_2, TARSKI, FINSEQ_2, FUNCOP_1, FUNCT_6, PARTFUN1, FUNCT_3, ARYTM_1, SQUARE_1, TREES_3; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, XCMPLX_0, XREAL_0, NAT_1, RELAT_1, FUNCT_1, FINSEQ_1, FINSET_1, DOMAIN_1, SQUARE_1, FUNCOP_1, RELSET_1, FUNCT_2, FUNCT_3, FINSEQ_2, TREES_1, TREES_2, FUNCT_6; constructors FUNCT_5, NAT_1, DOMAIN_1, SQUARE_1, FUNCT_3, FINSEQ_2, TREES_2, FUNCT_6, MEMBERED, XBOOLE_0; clusters SUBSET_1, FINSEQ_1, TREES_1, TREES_2, FINSET_1, RELSET_1, CARD_1, XREAL_0, MEMBERED, ZFMISC_1, XBOOLE_0, ORDINAL2, NUMBERS; requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM; begin :: Finite sets reserve x,y,z for set, i,k,n for Nat, p,q,r,s for FinSequence, w for FinSequence of NAT, X,Y for set, f for Function; begin :: Sets of trees definition func Trees -> set means :: TREES_3:def 1 x in it iff x is Tree; end; definition 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; definition 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; theorem :: TREES_3:12 {} is constituted-Trees constituted-FinTrees constituted-DTrees; theorem :: TREES_3:13 {x} is constituted-Trees iff x is Tree; theorem :: TREES_3:14 {x} is constituted-FinTrees iff x is finite Tree; theorem :: TREES_3:15 {x} is constituted-DTrees iff x is DecoratedTree; theorem :: TREES_3:16 {x,y} is constituted-Trees iff x is Tree & y is Tree; theorem :: TREES_3:17 {x,y} is constituted-FinTrees iff x is finite Tree & y is finite Tree; theorem :: TREES_3:18 {x,y} is constituted-DTrees iff x is DecoratedTree & y is DecoratedTree; theorem :: TREES_3:19 X is constituted-Trees & Y c= X implies Y is constituted-Trees; theorem :: TREES_3:20 X is constituted-FinTrees & Y c= X implies Y is constituted-FinTrees; theorem :: TREES_3:21 X is constituted-DTrees & Y c= X implies Y is constituted-DTrees; definition cluster finite constituted-Trees constituted-FinTrees non empty set; cluster finite constituted-DTrees non empty set; end; definition cluster constituted-FinTrees -> constituted-Trees set; end; definition let X be constituted-Trees set; cluster -> constituted-Trees Subset of X; end; definition let X be constituted-FinTrees set; cluster -> constituted-FinTrees Subset of X; end; definition let X be constituted-DTrees set; cluster -> constituted-DTrees Subset of X; end; definition let D be constituted-Trees non empty set; redefine mode Element of D -> Tree; end; definition let D be constituted-FinTrees non empty set; redefine mode Element of D -> finite Tree; end; definition let D be constituted-DTrees non empty set; redefine mode Element of D -> DecoratedTree; end; definition cluster Trees -> constituted-Trees; end; definition cluster constituted-FinTrees non empty Subset of Trees; end; definition cluster FinTrees -> constituted-FinTrees; end; definition let D be non empty set; mode DTree-set of D -> set means :: TREES_3:def 6 for x st x in it holds x is DecoratedTree of D; end; definition let D be non empty set; cluster -> constituted-DTrees DTree-set of D; end; definition let D be non empty set; cluster finite non empty DTree-set of D; end; definition let D be non empty set, E be non empty DTree-set of D; redefine mode Element of E -> DecoratedTree of D; end; definition let T be Tree, D be non empty set; redefine func Funcs(T,D) -> non empty DTree-set of D; mode Relation of T,D -> ParametrizedSubset of D; end; definition let T be Tree, D be non empty set; cluster -> DecoratedTree-like 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; definition 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; definition let D be non empty set; cluster FinTrees D -> non empty; end; theorem :: TREES_3:22 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; theorem :: TREES_3:23 {} is Tree-yielding FinTree-yielding DTree-yielding; theorem :: TREES_3:24 f is Tree-yielding iff for x st x in dom f holds f.x is Tree; theorem :: TREES_3:25 f is FinTree-yielding iff for x st x in dom f holds f.x is finite Tree; theorem :: TREES_3:26 f is DTree-yielding iff for x st x in dom f holds f.x is DecoratedTree; theorem :: TREES_3:27 p is Tree-yielding & q is Tree-yielding iff p^q is Tree-yielding; theorem :: TREES_3:28 p is FinTree-yielding & q is FinTree-yielding iff p^q is FinTree-yielding; theorem :: TREES_3:29 p is DTree-yielding & q is DTree-yielding iff p^q is DTree-yielding; theorem :: TREES_3:30 <*x*> is Tree-yielding iff x is Tree; theorem :: TREES_3:31 <*x*> is FinTree-yielding iff x is finite Tree; theorem :: TREES_3:32 <*x*> is DTree-yielding iff x is DecoratedTree; theorem :: TREES_3:33 <*x,y*> is Tree-yielding iff x is Tree & y is Tree; theorem :: TREES_3:34 <*x,y*> is FinTree-yielding iff x is finite Tree & y is finite Tree; theorem :: TREES_3:35 <*x,y*> is DTree-yielding iff x is DecoratedTree & y is DecoratedTree; theorem :: TREES_3:36 i <> 0 implies (i |-> x is Tree-yielding iff x is Tree); theorem :: TREES_3:37 i <> 0 implies (i |-> x is FinTree-yielding iff x is finite Tree); theorem :: TREES_3:38 i <> 0 implies (i |-> x is DTree-yielding iff x is DecoratedTree); definition cluster Tree-yielding FinTree-yielding non empty FinSequence; cluster DTree-yielding non empty FinSequence; end; definition cluster Tree-yielding FinTree-yielding non empty Function; cluster DTree-yielding non empty Function; end; definition cluster FinTree-yielding -> Tree-yielding Function; end; definition let D be constituted-Trees non empty set; cluster -> Tree-yielding FinSequence of D; end; definition let p,q be Tree-yielding FinSequence; cluster p^q -> Tree-yielding; end; definition let D be constituted-FinTrees non empty set; cluster -> FinTree-yielding FinSequence of D; end; definition let p,q be FinTree-yielding FinSequence; cluster p^q -> FinTree-yielding; end; definition let D be constituted-DTrees non empty set; cluster -> DTree-yielding FinSequence of D; end; definition let p,q be DTree-yielding FinSequence; cluster p^q -> DTree-yielding; end; definition let T be Tree; cluster <*T*> -> Tree-yielding non empty; let S be Tree; cluster <*T,S*> -> Tree-yielding non empty; end; definition let n be Nat, T be Tree; cluster n |-> T -> Tree-yielding; end; definition let T be finite Tree; cluster <*T*> -> FinTree-yielding; let S be finite Tree; cluster <*T,S*> -> FinTree-yielding; end; definition let n be Nat, T be finite Tree; cluster n |-> T -> FinTree-yielding; end; definition let T be DecoratedTree; cluster <*T*> -> DTree-yielding non empty; let S be DecoratedTree; cluster <*T,S*> -> DTree-yielding non empty; end; definition let n be Nat, T be DecoratedTree; cluster n |-> T -> DTree-yielding; end; theorem :: TREES_3:39 for f being DTree-yielding Function holds dom doms f = dom f & doms f is Tree-yielding; definition let p be DTree-yielding FinSequence; cluster doms p -> Tree-yielding FinSequence-like; end; theorem :: TREES_3:40 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; definition let T1,T2 be DecoratedTree; cluster <:T1,T2:> -> DecoratedTree-like; end; definition let D1,D2 be non empty set; let T1 be DecoratedTree of D1; let T2 be DecoratedTree of D2; redefine func <:T1,T2:> -> DecoratedTree of D1,D2; end; definition let D,E be non empty set; let T be DecoratedTree of D; let f be Function of D,E; redefine func f*T -> DecoratedTree of E; end; definition let D1,D2 be non empty set; redefine func pr1(D1,D2) -> Function of [:D1,D2:], D1; 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:41 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:42 for D1,D2 being non empty set, T being DecoratedTree of D1,D2 holds <:T`1,T`2:> = T; definition 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; definition let T be finite Tree; cluster finite T-Substitution of T; end; definition let n; mode T-Substitution of n is T-Substitution of elementary_tree n; end; theorem :: TREES_3:43 for T being Tree holds T is T-Substitution of 0; theorem :: TREES_3:44 for T1, T2 being Tree st T1-level 1 c= T2-level 1 & for n st <*n*> in T1 holds T1|<*n*> = T2|<*n*> holds T1 c= T2; begin :: Joining of trees canceled; theorem :: TREES_3:46 for T,T' being Tree, p being FinSequence of NAT st p in Leaves T holds T c= T with-replacement (p,T'); theorem :: TREES_3:47 for T,T' being DecoratedTree, p being Element of dom T holds (T with-replacement (p,T')).p = T'.{}; theorem :: TREES_3:48 for T,T' being DecoratedTree, p,q being Element of dom T st not p is_a_prefix_of q holds (T with-replacement (p,T')).q = T.q; theorem :: TREES_3:49 for T,T' being DecoratedTree, p being Element of dom T, q being Element of dom T' holds (T with-replacement (p,T')).(p^q) = T'.q; definition let T1,T2 be Tree; cluster T1 \/ T2 -> non empty Tree-like; end; theorem :: TREES_3:50 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:51 p is Tree-yielding implies (<*n*>^q in tree(p) iff n < len p & q in p.(n+1)) ; theorem :: TREES_3:52 p is Tree-yielding implies tree(p)-level 1 = {<*n*>: n < len p} & for n st n < len p holds (tree(p))|<*n*> = p.(n+1); theorem :: TREES_3:53 for p,q being Tree-yielding FinSequence st tree(p) = tree(q) holds p = q; theorem :: TREES_3:54 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:55 tree({}) = elementary_tree 0; theorem :: TREES_3:56 p is Tree-yielding implies elementary_tree len p c= tree(p); theorem :: TREES_3:57 elementary_tree i = tree(i|->elementary_tree 0); theorem :: TREES_3:58 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:59 for p being Tree-yielding FinSequence holds tree(p^<*elementary_tree 0*>) = tree(p) \/ elementary_tree (len p + 1); theorem :: TREES_3:60 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); theorem :: TREES_3:61 for T being Tree holds ^T = elementary_tree 1 with-replacement(<*0*>, T); theorem :: TREES_3:62 for T1,T2 being Tree holds tree(T1,T2) = (elementary_tree 2 with-replacement(<*0*>,T1)) with-replacement (<*1*>, T2); definition let p be FinTree-yielding FinSequence; cluster tree(p) -> finite; end; definition let T be finite Tree; cluster ^T -> finite; end; definition let T1,T2 be finite Tree; cluster tree(T1,T2) -> finite; end; theorem :: TREES_3:63 for T being Tree, x being set holds x in ^T iff x = {} or ex p st p in T & x = <*0*>^p; theorem :: TREES_3:64 for T being Tree, p being FinSequence holds p in T iff <*0*>^p in ^T; theorem :: TREES_3:65 for T being Tree holds elementary_tree 1 c= ^T; theorem :: TREES_3:66 for T1,T2 being Tree st T1 c= T2 holds ^T1 c= ^T2; theorem :: TREES_3:67 for T1,T2 being Tree st ^T1 = ^T2 holds T1 = T2; theorem :: TREES_3:68 for T being Tree holds (^T)|<*0*> = T; theorem :: TREES_3:69 for T1,T2 being Tree holds ^T1 with-replacement (<*0*>,T2) = ^T2; theorem :: TREES_3:70 ^elementary_tree 0 = elementary_tree 1; theorem :: TREES_3:71 for T1,T2 being Tree, x being set 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:72 for T1,T2 being Tree, p being FinSequence holds p in T1 iff <*0*>^p in tree(T1,T2); theorem :: TREES_3:73 for T1,T2 being Tree, p being FinSequence holds p in T2 iff <*1*>^p in tree(T1,T2); theorem :: TREES_3:74 for T1,T2 being Tree holds elementary_tree 2 c= tree(T1,T2); theorem :: TREES_3:75 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:76 for T1,T2, W1,W2 being Tree st tree(T1,T2) = tree(W1,W2) holds T1 = W1 & T2 = W2; theorem :: TREES_3:77 for T1,T2 being Tree holds tree(T1,T2)|<*0*> = T1 & tree(T1,T2)|<*1*> = T2; theorem :: TREES_3:78 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:79 tree(elementary_tree 0, elementary_tree 0) = elementary_tree 2; reserve w for FinTree-yielding FinSequence; theorem :: TREES_3:80 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:81 for t being finite Tree st t in rng w holds height tree(w) > height t; theorem :: TREES_3:82 for t being finite Tree st t in rng w & for t' being finite Tree st t' in rng w holds height t' <= height t holds height tree(w) = (height t) + 1; theorem :: TREES_3:83 for T being finite Tree holds height ^T = (height T) + 1; theorem :: TREES_3:84 for T1,T2 being finite Tree holds height tree(T1,T2) = max(height T1, height T2)+1;

Back to top