Volume 6, 1994

University of Bialystok

Copyright (c) 1994 Association of Mizar Users

### The abstract of the Mizar article:

### Subtrees

**by****Grzegorz Bancerek**- Received November 25, 1994
- MML identifier: TREES_9

- [ Mizar article, MML identifier index ]

environ vocabulary FINSET_1, TREES_2, TREES_1, CARD_1, FINSEQ_1, FUNCT_1, ARYTM_1, RELAT_1, ORDINAL1, BOOLE, TREES_4, TARSKI, TREES_3, FUNCT_6, DTCONSTR, TREES_9; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, XCMPLX_0, XREAL_0, NAT_1, RELAT_1, FUNCT_1, FUNCT_2, FINSEQ_1, FINSET_1, FINSEQ_2, FUNCT_6, CARD_1, TREES_1, TREES_2, TREES_3, TREES_4, DTCONSTR; constructors WELLORD2, REAL_1, NAT_1, DTCONSTR, FINSOP_1, XREAL_0, MEMBERED, XBOOLE_0; clusters FUNCT_1, FINSET_1, PRELAMB, TREES_1, TREES_2, TREES_3, PRE_CIRC, FINSEQ_1, RELSET_1, XREAL_0, ARYTM_3, MEMBERED, ZFMISC_1, XBOOLE_0, NUMBERS, ORDINAL2; requirements NUMERALS, BOOLE, SUBSET, ARITHM; begin :: Root tree and successors of node in decorated tree definition cluster finite -> finite-order Tree; end; theorem :: TREES_9:1 for t being DecoratedTree holds t|<*>NAT = t; theorem :: TREES_9:2 for t being Tree, p,q being FinSequence of NAT st p^q in t holds t|(p^q) = (t|p)|q; theorem :: TREES_9:3 for t being DecoratedTree, p,q being FinSequence of NAT st p^q in dom t holds t|(p^q) = (t|p)|q; definition let IT be DecoratedTree; attr IT is root means :: TREES_9:def 1 dom IT = elementary_tree 0; end; definition cluster root -> finite DecoratedTree; end; theorem :: TREES_9:4 for t being DecoratedTree holds t is root iff {} in Leaves dom t; theorem :: TREES_9:5 for t being Tree, p being Element of t holds t|p = elementary_tree 0 iff p in Leaves t; theorem :: TREES_9:6 for t being DecoratedTree, p being Node of t holds t|p is root iff p in Leaves dom t; definition cluster root DecoratedTree; cluster finite non root DecoratedTree; end; definition let x be set; cluster root-tree x -> finite root; end; definition let IT be Tree; attr IT is finite-branching means :: TREES_9:def 2 for x being Element of IT holds succ x is finite; end; definition cluster finite-order -> finite-branching Tree; end; definition cluster finite Tree; end; definition let IT be DecoratedTree; attr IT is finite-order means :: TREES_9:def 3 dom IT is finite-order; attr IT is finite-branching means :: TREES_9:def 4 dom IT is finite-branching; end; definition cluster finite -> finite-order DecoratedTree; cluster finite-order -> finite-branching DecoratedTree; end; definition cluster finite DecoratedTree; end; definition let t be finite-order DecoratedTree; cluster dom t -> finite-order; end; definition let t be finite-branching DecoratedTree; cluster dom t -> finite-branching; end; definition let t be finite-branching Tree; let p be Element of t; cluster succ p -> finite; end; scheme FinOrdSet{f(set) -> set, X() -> finite set}: for n being Nat holds f(n) in X() iff n < card X() provided for x being set st x in X() ex n being Nat st x = f(n) and for i,j being Nat st i < j & f(j) in X() holds f(i) in X() and for i,j being Nat st f(i) = f(j) holds i = j; definition let X be set; cluster one-to-one empty FinSequence of X; end; theorem :: TREES_9:7 for t being finite-branching Tree, p being Element of t for n being Nat holds p^<*n*> in succ p iff n < card succ p; definition let t be finite-branching Tree; let p be Element of t; func p succ -> one-to-one FinSequence of t means :: TREES_9:def 5 len it = card succ p & rng it = succ p & for i being Nat st i < len it holds it.(i+1) = p^<*i*>; end; definition let t be finite-branching DecoratedTree; let p be FinSequence such that p in dom t; func succ(t,p) -> FinSequence means :: TREES_9:def 6 ex q being Element of dom t st q = p & it = t*(q succ); end; theorem :: TREES_9:8 for t being finite-branching DecoratedTree ex x being set, p being DTree-yielding FinSequence st t = x-tree p; definition let t be finite DecoratedTree; let p be Node of t; cluster t|p -> finite; end; canceled; theorem :: TREES_9:10 for t being finite Tree, p being Element of t st t = t|p holds p = {}; definition let D be non empty set; let S be non empty Subset of FinTrees D; cluster -> finite Element of S; end; begin :: Set of subtrees of decorated tree definition let t be DecoratedTree; func Subtrees t -> set equals :: TREES_9:def 7 {t|p where p is Node of t: not contradiction}; end; definition let t be DecoratedTree; cluster Subtrees t -> constituted-DTrees non empty; end; definition let D be non empty set; let t be DecoratedTree of D; redefine func Subtrees t -> non empty Subset of Trees D; end; definition let D be non empty set; let t be finite DecoratedTree of D; redefine func Subtrees t -> non empty Subset of FinTrees D; end; definition let t be finite DecoratedTree; cluster -> finite Element of Subtrees t; end; reserve x for set, t,t1,t2 for DecoratedTree; theorem :: TREES_9:11 x in Subtrees t iff ex n being Node of t st x = t|n; theorem :: TREES_9:12 t in Subtrees t; theorem :: TREES_9:13 t1 is finite & Subtrees t1 = Subtrees t2 implies t1 = t2; theorem :: TREES_9:14 for n being Node of t holds Subtrees (t|n) c= Subtrees t; definition let t be DecoratedTree; func FixedSubtrees t -> Subset of [:dom t, Subtrees t:] equals :: TREES_9:def 8 {[p,t|p] where p is Node of t: not contradiction}; end; definition let t be DecoratedTree; cluster FixedSubtrees t -> non empty; end; theorem :: TREES_9:15 x in FixedSubtrees t iff ex n being Node of t st x = [n,t|n]; theorem :: TREES_9:16 [{},t] in FixedSubtrees t; theorem :: TREES_9:17 FixedSubtrees t1 = FixedSubtrees t2 implies t1 = t2; definition let t be DecoratedTree; let C be set; func C-Subtrees t -> Subset of Subtrees t equals :: TREES_9:def 9 {t|p where p is Node of t: not p in Leaves dom t or t.p in C}; end; reserve C for set; theorem :: TREES_9:18 x in C-Subtrees t iff ex n being Node of t st x = t|n & (not n in Leaves dom t or t.n in C); theorem :: TREES_9:19 C-Subtrees t is empty iff t is root & not t.{} in C; definition let t be finite DecoratedTree; let C be set; func C-ImmediateSubtrees t -> Function of C-Subtrees t, (Subtrees t)* means :: TREES_9:def 10 for d being DecoratedTree st d in C-Subtrees t for p being FinSequence of Subtrees t st p = it.d holds d = (d.{})-tree p; end; begin :: Set of subtrees of set of decorated tree definition let X be constituted-DTrees non empty set; func Subtrees X -> set equals :: TREES_9:def 11 {t|p where t is Element of X, p is Node of t: not contradiction}; end; definition let X be constituted-DTrees non empty set; cluster Subtrees X -> constituted-DTrees non empty; end; definition let D be non empty set; let X be non empty Subset of Trees D; redefine func Subtrees X -> non empty Subset of Trees D; end; definition let D be non empty set; let X be non empty Subset of FinTrees D; redefine func Subtrees X -> non empty Subset of FinTrees D; end; reserve X,Y for non empty constituted-DTrees set; theorem :: TREES_9:20 x in Subtrees X iff ex t being Element of X, n being Node of t st x = t|n; theorem :: TREES_9:21 t in X implies t in Subtrees X; theorem :: TREES_9:22 X c= Y implies Subtrees X c= Subtrees Y; definition let t be DecoratedTree; cluster {t} -> non empty constituted-DTrees; end; theorem :: TREES_9:23 Subtrees {t} = Subtrees t; theorem :: TREES_9:24 Subtrees X = union {Subtrees t where t is Element of X: not contradiction}; definition let X be constituted-DTrees non empty set; let C be set; func C-Subtrees X -> Subset of Subtrees X equals :: TREES_9:def 12 {t|p where t is Element of X, p is Node of t: not p in Leaves dom t or t.p in C}; end; theorem :: TREES_9:25 x in C-Subtrees X iff ex t being Element of X, n being Node of t st x = t|n & (not n in Leaves dom t or t.n in C); theorem :: TREES_9:26 C-Subtrees X is empty iff for t being Element of X holds t is root & not t.{} in C; theorem :: TREES_9:27 C-Subtrees {t} = C-Subtrees t; theorem :: TREES_9:28 C-Subtrees X = union {C-Subtrees t where t is Element of X: not contradiction}; definition let X be non empty constituted-DTrees set such that for t being Element of X holds t is finite; let C be set; func C-ImmediateSubtrees X -> Function of C-Subtrees X, (Subtrees X)* means :: TREES_9:def 13 for d being DecoratedTree st d in C-Subtrees X for p being FinSequence of Subtrees X st p = it.d holds d = (d.{})-tree p; end; definition let t be Tree; cluster empty Element of t; end; theorem :: TREES_9:29 for t being finite DecoratedTree, p being Element of dom t holds len succ(t,p) = len (p succ) & dom succ(t,p) = dom (p succ); theorem :: TREES_9:30 for p being FinTree-yielding FinSequence, n being empty Element of tree p holds card succ n = len p; theorem :: TREES_9:31 for t being finite DecoratedTree, x being set, p being DTree-yielding FinSequence st t = x-tree p for n being empty Element of dom t holds succ(t,n) = roots p; theorem :: TREES_9:32 for t being finite DecoratedTree, p being Node of t, q being Node of t|p holds succ(t,p^q) = succ(t|p,q);

Back to top