:: Subtrees
:: by Grzegorz Bancerek
::
:: Received November 25, 1994
:: Copyright (c) 1994-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 XBOOLE_0, TREES_3, SUBSET_1, FINSET_1, TREES_2, TREES_1, CARD_1,
ARYTM_3, NAT_1, ORDINAL4, FINSEQ_1, ARYTM_1, RELAT_1, FUNCT_1, TARSKI,
ORDINAL1, NUMBERS, XXREAL_0, ZFMISC_1, TREES_4, FUNCT_6, TREES_A,
TREES_9, MCART_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, CARD_1, ORDINAL1,
NUMBERS, XCMPLX_0, RELAT_1, FUNCT_1, RELSET_1, FUNCT_2, FUNCT_6, NAT_1,
BINOP_1, FINSET_1, FINSEQ_1, FINSEQ_2, TREES_1, TREES_2, TREES_3,
TREES_4, MCART_1, XXREAL_0;
constructors WELLORD2, XXREAL_0, XREAL_0, NAT_1, FINSEQ_2, TREES_4, RELSET_1,
BINOP_1, FINSEQ_4, XTUPLE_0, NUMBERS;
registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, FINSET_1, XREAL_0,
FINSEQ_1, TREES_1, TREES_2, TREES_3, PRE_CIRC, CARD_1, RELSET_1, NAT_1;
requirements NUMERALS, BOOLE, SUBSET, ARITHM, REAL;
begin :: Root tree and successors of node in decorated tree
definition
let D be non empty set;
let F be non empty DTree-set of D;
let Tset be non empty Subset of F;
redefine mode Element of Tset -> Element of F;
end;
registration
cluster finite -> finite-order for 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;
notation
let IT be DecoratedTree;
synonym IT is root for IT is trivial;
end;
definition
let IT be DecoratedTree;
redefine attr IT is root means
:: TREES_9:def 1
dom IT = elementary_tree 0;
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;
registration
cluster root for DecoratedTree;
cluster finite non root for DecoratedTree;
end;
registration
let x be object;
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;
registration
cluster finite-order -> finite-branching for 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;
registration
cluster finite -> finite-order for DecoratedTree;
cluster finite-order -> finite-branching for DecoratedTree;
end;
registration
let t be finite-order DecoratedTree;
cluster dom t -> finite-order;
end;
registration
let t be finite-branching DecoratedTree;
cluster dom t -> finite-branching;
end;
registration
let t be finite-branching Tree;
let p be Element of t;
cluster succ p -> finite;
end;
scheme :: TREES_9:sch 1
FinOrdSet{f(object) -> 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;
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;
registration
let t be finite DecoratedTree;
let p be Node of t;
cluster t|p -> finite;
end;
theorem :: TREES_9:9
for t being finite Tree, p being Element of t st t = t|p holds p = {};
registration
let D be non empty set;
let S be non empty Subset of FinTrees D;
cluster -> finite for 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
the set of all t|p where p is Node of t;
end;
registration
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;
registration
let t be finite DecoratedTree;
cluster -> finite for Element of Subtrees t;
end;
reserve x for set,
t,t1,t2 for DecoratedTree;
theorem :: TREES_9:10
x in Subtrees t iff ex n being Node of t st x = t|n;
theorem :: TREES_9:11
t in Subtrees t;
theorem :: TREES_9:12
t1 is finite & Subtrees t1 = Subtrees t2 implies t1 = t2;
theorem :: TREES_9:13
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
the set of all [p,t|p]
where p is Node of t;
end;
registration
let t be DecoratedTree;
cluster FixedSubtrees t -> non empty;
end;
theorem :: TREES_9:14
x in FixedSubtrees t iff ex n being Node of t st x = [n,t|n];
theorem :: TREES_9:15
[{},t] in FixedSubtrees t;
theorem :: TREES_9:16
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:17
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:18
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
the set of all t|p where t is Element of X, p is Node of t;
end;
registration
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:19
x in Subtrees X iff ex t being Element of X, n being Node of t st x = t|n;
theorem :: TREES_9:20
t in X implies t in Subtrees X;
theorem :: TREES_9:21
X c= Y implies Subtrees X c= Subtrees Y;
registration
let t be DecoratedTree;
cluster {t} -> constituted-DTrees;
end;
theorem :: TREES_9:22
Subtrees {t} = Subtrees t;
theorem :: TREES_9:23
Subtrees X = union the set of all Subtrees t where t is Element of X;
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:24
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:25
C-Subtrees X is empty iff for t being Element of X holds t is root &
not t.{} in C;
theorem :: TREES_9:26
C-Subtrees {t} = C-Subtrees t;
theorem :: TREES_9:27
C-Subtrees X = union the set of all C-Subtrees t where t is Element of X;
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;
registration
let t be Tree;
cluster empty for Element of t;
end;
theorem :: TREES_9:28
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:29
for p being FinTree-yielding FinSequence, n being empty Element
of tree p holds card succ n = len p;
theorem :: TREES_9:30
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;
registration
let T be finite-branching DecoratedTree, t being Node of T;
cluster T|t -> finite-branching;
end;
theorem :: TREES_9:31
for t being finite-branching DecoratedTree, p being Node of t,
q being Node of t|p holds succ(t,p^q) = succ(t|p,q);
begin :: Moved from QC_LANG4, 2010.03.17, A.T
theorem :: TREES_9:32
for n being Nat, r being FinSequence ex q being
FinSequence st q = r|Seg n & q is_a_prefix_of r;
theorem :: TREES_9:33
for D being non empty set, r being FinSequence of D, r1,r2 being
FinSequence, k being Nat st k+1 <= len r & r1 = r|Seg (k+1) & r2 = r
|Seg k holds ex x being Element of D st r1 = r2^<*x*>;
theorem :: TREES_9:34
for D being non empty set, r being FinSequence of D, r1 being
FinSequence st 1 <= len r & r1 = r|Seg 1 holds ex x being Element of D st r1 =
<*x*>;
reserve T for DecoratedTree,
p for FinSequence of NAT;
theorem :: TREES_9:35
T.p = (T|p).{};
reserve T for finite-branching DecoratedTree,
t for Element of dom T,
x for FinSequence,
n, m for Nat;
theorem :: TREES_9:36
succ(T,t) = T*(t succ);
theorem :: TREES_9:37
dom (T*(t succ)) = dom (t succ);
theorem :: TREES_9:38
dom succ(T,t) = dom (t succ);
theorem :: TREES_9:39
t^<*n*> in dom T iff n+1 in dom (t succ);
theorem :: TREES_9:40
for T, x, n st x^<*n*> in dom T holds T.(x^<*n*>) = succ(T,x).(n +1);
reserve x, x9 for Element of dom T,
y9 for set;
theorem :: TREES_9:41
x9 in succ x implies T.x9 in rng succ(T,x);
theorem :: TREES_9:42
y9 in rng succ(T,x) implies ex x9 st y9 = T.x9 & x9 in succ x;
reserve n,k1,k2,l,k,m for Nat,
x,y for set;
scheme :: TREES_9:sch 2
ExDecTrees { D() -> non empty set, d() -> Element of D(), G(object) ->
FinSequence of D() }:
ex T being finite-branching DecoratedTree of D() st T.{}
= d() & for t being Element of dom T, w being Element of D() st w = T.t holds
succ(T,t) = G(w);
theorem :: TREES_9:43
for T being Tree, t being Element of T holds ProperPrefixes t is
finite Chain of T;
theorem :: TREES_9:44
for T being Tree holds T-level 0 = {{}};
theorem :: TREES_9:45
for T being Tree holds T-level (n+1) = union { succ w where w is
Element of T : len w = n };
theorem :: TREES_9:46
for T being finite-branching Tree, n being Nat holds
T-level n is finite;
theorem :: TREES_9:47
for T being finite-branching Tree holds T is finite iff ex n
being Nat st T-level n = {};
theorem :: TREES_9:48
for T being finite-branching Tree st not T is finite ex C being
Chain of T st not C is finite;
theorem :: TREES_9:49
for T being finite-branching Tree st not T is finite ex B being
Branch of T st not B is finite;
theorem :: TREES_9:50
for T being Tree, C being Chain of T, t being Element of T st t
in C & not C is finite ex t9 being Element of T st t9 in C & t
is_a_proper_prefix_of t9;
theorem :: TREES_9:51
for T being Tree, B being Branch of T, t being Element of T st t
in B & not B is finite ex t9 being Element of T st t9 in B & t9 in succ t;
theorem :: TREES_9:52
for f being sequence of NAT st (for n holds f.(n+1) qua
Nat <= f.n qua Nat) ex m st for n st m <= n holds f.n = f
.m;
scheme :: TREES_9:sch 3
FinDecTree { D() -> non empty set,
T() -> finite-branching (DecoratedTree of D()),
F(Element of D()) -> Nat }:
T() is finite
provided
for t,t9 being Element of dom T(), d being Element of D() st t9 in
succ t & d = T().t9 holds F(d) < F(T().t);