:: Subtrees
:: by Grzegorz Bancerek
::
:: Received November 25, 1994
:: Copyright (c) 1994-2012 Association of Mizar Users


begin

definition
let D be non empty set ;
let F be non empty DTree-set of D;
let Tset be non empty Subset of F;
:: original:Element
redefine mode Element of Tset ->  Element of F;
coherence
 for b1 being Element of Tset holds b1 is Element of F
proofend;
end;

registration
cluster non empty finite Tree-like  ->  finite-order for set ;
coherence
 for b1 being Tree st b1 is finite holds
b1 is finite-order
proofend;
end;

Lm1:  for n being set
for p being FinSequence st n in dom p holds
ex k being Element of NAT st
( n = k + 1 &amp; k < len p )
proofend;

Lm2: now__::_thesis:_for_p,_q_being_FinSequence_st_len_p_=_len_q_&amp;_(_for_i_being_Element_of_NAT_st_i_<_len_p_holds_
p_._(i_+_1)_=_q_._(i_+_1)_)_holds_
p_=_q
let p, q be FinSequence; ::_thesis: ( len p = len q &amp; ( for i being Element of NAT st i < len p holds
p . (i + 1) = q . (i + 1) ) implies p = q )
assume that
A1: len p = len q and
A2: for i being Element of NAT st i < len p holds
p . (i + 1) = q . (i + 1) ; ::_thesis: p = q
A3: now__::_thesis:_for_i_being_Nat_st_i_in_dom_p_holds_
p_._i_=_q_._i
let i be Nat; ::_thesis: ( i in dom p implies p . i = q . i )
assume  i in dom p ; ::_thesis: p . i = q . i
then  ex k being Element of NAT st
( i = k + 1 &amp; k < len p ) by Lm1;
hence  p . i = q . i by A2; ::_thesis: verum
end;
 dom p = dom q by A1, FINSEQ_3:29;
hence  p = q by A3, FINSEQ_1:13; ::_thesis: verum
end;

Lm3:  for n being Element of NAT
for p being FinSequence st n < len p holds
( n + 1 in dom p &amp; p . (n + 1) in rng p )
proofend;

Lm4: now__::_thesis:_for_p_being_FinSequence
for_x_being_set_st_x_in_rng_p_holds_
ex_k_being_Element_of_NAT_st_
(_k_<_len_p_&amp;_x_=_p_._(k_+_1)_)
let p be FinSequence; ::_thesis: for x being set st x in rng p holds
ex k being Element of NAT st
( k < len p &amp; x = p . (k + 1) )
let x be set ; ::_thesis: ( x in rng p implies ex k being Element of NAT st
( k < len p &amp; x = p . (k + 1) ) )
assume  x in rng p ; ::_thesis: ex k being Element of NAT st
( k < len p &amp; x = p . (k + 1) )
then consider y being set  such that
A1: y in dom p and
A2: x = p . y by FUNCT_1:def_3;
 ex k being Element of NAT st
( y = k + 1 &amp; k < len p ) by A1, Lm1;
hence  ex k being Element of NAT st
( k < len p &amp; x = p . (k + 1) ) by A2; ::_thesis: verum
end;

theorem Th1: :: TREES_9:1
for t being DecoratedTree holds t | (<*> NAT) = t
proofend;

theorem Th2: :: TREES_9:2
for t being Tree
for p, q being FinSequence of NAT st p ^ q in t holds
t | (p ^ q) = (t | p) | q
proofend;

theorem Th3: :: TREES_9:3
for t being DecoratedTree
for p, q being FinSequence of NAT st p ^ q in dom t holds
t | (p ^ q) = (t | p) | q
proofend;

notation
let IT be DecoratedTree;
synonym  root IT for  trivial ;
end;

definition
let IT be DecoratedTree;
redefine attr IT is trivial  means :Def1: :: TREES_9:def 1
 dom IT = elementary_tree 0;
compatibility
 ( IT is root iff dom IT = elementary_tree 0 )
proofend;
end;

:: deftheorem Def1 defines root TREES_9:def_1_:_
 for IT being DecoratedTree holds
( IT is root iff dom IT = elementary_tree 0 );

theorem Th4: :: TREES_9:4
for t being DecoratedTree holds
( t is root iff {} in Leaves (dom t) )
proofend;

theorem Th5: :: TREES_9:5
for t being Tree
for p being Element of t holds
( t | p = elementary_tree 0 iff p in Leaves t )
proofend;

theorem :: TREES_9:6
for t being DecoratedTree
for p being Node of t holds
( t | p is root iff p in Leaves (dom t) )
proofend;

registration
cluster Relation-like root Function-like DecoratedTree-like for set ;
existence
 ex b1 being DecoratedTree st b1 is root
proofend;
cluster Relation-like non root Function-like finite DecoratedTree-like for set ;
existence
 ex b1 being DecoratedTree st
( b1 is finite &amp; not b1 is root )
proofend;
end;

registration
let x be set ;
cluster root-tree x ->  root finite ;
coherence
 ( root-tree x is finite &amp; root-tree x is root )
proofend;
end;

definition
let IT be Tree;
attrIT is finite-branching  means :Def2: :: TREES_9:def 2
 for x being Element of IT holds succ x is finite ;
end;

:: deftheorem Def2 defines finite-branching TREES_9:def_2_:_
 for IT being Tree holds
( IT is finite-branching iff for x being Element of IT holds succ x is finite );

registration
cluster non empty Tree-like finite-order  ->  finite-branching for set ;
coherence
 for b1 being Tree st b1 is finite-order holds
b1 is finite-branching
proofend;
end;

definition
let IT be DecoratedTree;
attrIT is finite-order  means :Def3: :: TREES_9:def 3
 dom IT is finite-order ;
attrIT is finite-branching  means :Def4: :: TREES_9:def 4
 dom IT is finite-branching ;
end;

:: deftheorem Def3 defines finite-order TREES_9:def_3_:_
 for IT being DecoratedTree holds
( IT is finite-order iff dom IT is finite-order );

:: deftheorem Def4 defines finite-branching TREES_9:def_4_:_
 for IT being DecoratedTree holds
( IT is finite-branching iff dom IT is finite-branching );

registration
cluster Relation-like Function-like finite DecoratedTree-like  ->  finite-order for set ;
coherence
 for b1 being DecoratedTree st b1 is finite holds
b1 is finite-order
proofend;
cluster Relation-like Function-like DecoratedTree-like finite-order  ->  finite-branching for set ;
coherence
 for b1 being DecoratedTree st b1 is finite-order holds
b1 is finite-branching
proofend;
end;

registration
let t be finite-order DecoratedTree;
cluster proj1 t ->  finite-order ;
coherence
 dom t is finite-order by Def3;
end;

registration
let t be finite-branching DecoratedTree;
cluster proj1 t ->  finite-branching ;
coherence
 dom t is finite-branching by Def4;
end;

registration
let t be finite-branching Tree;
let p be Element of t;
cluster succ p ->  finite ;
coherence
 succ p is finite by Def2;
end;

scheme :: TREES_9:sch 1
FinOrdSet{ F1( set ) ->  set , F2() ->  finite set } :
 for n being Element of NAT holds
( F1(n) in F2() iff n < card F2() )
provided
A1: for x being set st x in F2() holds
ex n being Element of NAT st x = F1(n) and
A2: for i, j being Element of NAT st i < j &amp; F1(j) in F2() holds
F1(i) in F2() and
A3: for i, j being Element of NAT st F1(i) = F1(j) holds
i = j
proofend;

theorem Th7: :: TREES_9:7
for t being finite-branching Tree
for p being Element of t
for n being Element of NAT holds
( p ^ <*n*> in succ p iff n < card (succ p) )
proofend;

definition
let t be finite-branching Tree;
let p be Element of t;
funcp succ  ->  one-to-one FinSequence of t means :Def5: :: TREES_9:def 5
( len it = card (succ p) &amp; rng it = succ p &amp; ( for i being Element of NAT st i < len it holds
it . (i + 1) = p ^ <*i*> ) );
existence
 ex b1 being one-to-one FinSequence of t st
( len b1 = card (succ p) &amp; rng b1 = succ p &amp; ( for i being Element of NAT st i < len b1 holds
b1 . (i + 1) = p ^ <*i*> ) )
proofend;
uniqueness
 for b1, b2 being one-to-one FinSequence of t st len b1 = card (succ p) &amp; rng b1 = succ p &amp; ( for i being Element of NAT st i < len b1 holds
b1 . (i + 1) = p ^ <*i*> ) &amp; len b2 = card (succ p) &amp; rng b2 = succ p &amp; ( for i being Element of NAT st i < len b2 holds
b2 . (i + 1) = p ^ <*i*> ) holds
b1 = b2
proofend;
end;

:: deftheorem Def5 defines succ TREES_9:def_5_:_
 for t being finite-branching Tree
for p being Element of t
for b3 being one-to-one FinSequence of t holds
( b3 = p succ iff ( len b3 = card (succ p) &amp; rng b3 = succ p &amp; ( for i being Element of NAT st i < len b3 holds
b3 . (i + 1) = p ^ <*i*> ) ) );

definition
let t be finite-branching DecoratedTree;
let p be FinSequence;
assume A1: p in dom t ;
func succ (t,p) ->  FinSequence means :Def6: :: TREES_9:def 6
 ex q being Element of dom t st
( q = p &amp; it = t * (q succ) );
existence
 ex b1 being FinSequence ex q being Element of dom t st
( q = p &amp; b1 = t * (q succ) )
proofend;
uniqueness
 for b1, b2 being FinSequence st ex q being Element of dom t st
( q = p &amp; b1 = t * (q succ) ) &amp; ex q being Element of dom t st
( q = p &amp; b2 = t * (q succ) ) holds
b1 = b2 ;
end;

:: deftheorem Def6 defines succ TREES_9:def_6_:_
 for t being finite-branching DecoratedTree
for p being FinSequence st p in dom t holds
for b3 being FinSequence holds
( b3 = succ (t,p) iff ex q being Element of dom t st
( q = p &amp; b3 = t * (q succ) ) );

theorem Th8: :: TREES_9:8
for t being finite-branching DecoratedTree ex x being set ex p being DTree-yielding FinSequence st t = x -tree p
proofend;

registration
let t be finite DecoratedTree;
let p be Node of t;
clustert | p ->  finite ;
coherence
 t | p is finite ;
end;

theorem Th9: :: TREES_9:9
for t being finite Tree
for p being Element of t st t = t | p holds
p = {}
proofend;

registration
let D be non empty set ;
let S be non empty Subset of (FinTrees D);
cluster  ->  finite for Element of S;
coherence
 for b1 being Element of S holds b1 is finite ;
end;

begin

definition
let t be DecoratedTree;
func Subtrees t ->  set  equals :: TREES_9:def 7
 {  (t | p) where p is Node of t : verum  }  ;
coherence
  {  (t | p) where p is Node of t : verum  }  is set ;
end;

:: deftheorem  defines Subtrees TREES_9:def_7_:_
 for t being DecoratedTree holds Subtrees t =  {  (t | p) where p is Node of t : verum  }  ;

registration
let t be DecoratedTree;
cluster Subtrees t ->  non empty constituted-DTrees ;
coherence
 ( Subtrees t is constituted-DTrees &amp; not Subtrees t is empty )
proofend;
end;

definition
let D be non empty set ;
let t be DecoratedTree of D;
:: original:Subtrees
redefine func Subtrees t ->  non empty Subset of (Trees D);
coherence
 Subtrees t is non empty Subset of (Trees D)
proofend;
end;

definition
let D be non empty set ;
let t be finite DecoratedTree of D;
:: original:Subtrees
redefine func Subtrees t ->  non empty Subset of (FinTrees D);
coherence
 Subtrees t is non empty Subset of (FinTrees D)
proofend;
end;

registration
let t be finite DecoratedTree;
cluster  ->  finite for Element of Subtrees t;
coherence
 for b1 being Element of Subtrees t holds b1 is finite
proofend;
end;

theorem Th10: :: TREES_9:10
for x being set
for t being DecoratedTree holds
( x in Subtrees t iff ex n being Node of t st x = t | n ) ;

theorem Th11: :: TREES_9:11
for t being DecoratedTree holds t in Subtrees t
proofend;

theorem :: TREES_9:12
for t1, t2 being DecoratedTree st t1 is finite &amp; Subtrees t1 = Subtrees t2 holds
t1 = t2
proofend;

theorem :: TREES_9:13
for t being DecoratedTree
for n being Node of t holds Subtrees (t | n) c= Subtrees t
proofend;

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 : verum  }  ;
coherence
  {  [p,(t | p)] where p is Node of t : verum  }  is Subset of [:(dom t),(Subtrees t):]
proofend;
end;

:: deftheorem  defines FixedSubtrees TREES_9:def_8_:_
 for t being DecoratedTree holds FixedSubtrees t =  {  [p,(t | p)] where p is Node of t : verum  }  ;

registration
let t be DecoratedTree;
cluster FixedSubtrees t ->  non empty ;
coherence
 not FixedSubtrees t is empty
proofend;
end;

theorem :: TREES_9:14
for x being set
for t being DecoratedTree holds
( x in FixedSubtrees t iff ex n being Node of t st x = [n,(t | n)] ) ;

theorem Th15: :: TREES_9:15
for t being DecoratedTree holds [{},t] in FixedSubtrees t
proofend;

theorem :: TREES_9:16
for t1, t2 being DecoratedTree st FixedSubtrees t1 = FixedSubtrees t2 holds
t1 = t2
proofend;

definition
let t be DecoratedTree;
let C be set ;
funcC -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 )  }  ;
coherence
  {  (t | p) where p is Node of t : ( not p in Leaves (dom t) or t . p in C )  }  is Subset of (Subtrees t)
proofend;
end;

:: deftheorem  defines -Subtrees TREES_9:def_9_:_
 for t being DecoratedTree
for C being set holds C -Subtrees t =  {  (t | p) where p is Node of t : ( not p in Leaves (dom t) or t . p in C )  }  ;

theorem Th17: :: TREES_9:17
for x being set
for t being DecoratedTree
for C being set holds
( x in C -Subtrees t iff ex n being Node of t st
( x = t | n &amp; ( not n in Leaves (dom t) or t . n in C ) ) ) ;

theorem :: TREES_9:18
for t being DecoratedTree
for C being set holds
( C -Subtrees t is empty iff ( t is root &amp; not t . {} in C ) )
proofend;

definition
let t be finite DecoratedTree;
let C be set ;
funcC -ImmediateSubtrees t ->  Function of (C -Subtrees t),((Subtrees t) *) means :: TREES_9:def 10
 for d being DecoratedTree st d in C -Subtrees t holds
for p being FinSequence of Subtrees t st p = it . d holds
d = (d . {}) -tree p;
existence
 ex b1 being Function of (C -Subtrees t),((Subtrees t) *) st
for d being DecoratedTree st d in C -Subtrees t holds
for p being FinSequence of Subtrees t st p = b1 . d holds
d = (d . {}) -tree p
proofend;
uniqueness
 for b1, b2 being Function of (C -Subtrees t),((Subtrees t) *) st ( for d being DecoratedTree st d in C -Subtrees t holds
for p being FinSequence of Subtrees t st p = b1 . d holds
d = (d . {}) -tree p ) &amp; ( for d being DecoratedTree st d in C -Subtrees t holds
for p being FinSequence of Subtrees t st p = b2 . d holds
d = (d . {}) -tree p ) holds
b1 = b2
proofend;
end;

:: deftheorem  defines -ImmediateSubtrees TREES_9:def_10_:_
 for t being finite DecoratedTree
for C being set
for b3 being Function of (C -Subtrees t),((Subtrees t) *) holds
( b3 = C -ImmediateSubtrees t iff for d being DecoratedTree st d in C -Subtrees t holds
for p being FinSequence of Subtrees t st p = b3 . d holds
d = (d . {}) -tree p );

begin

definition
let X be non empty constituted-DTrees set ;
func Subtrees X ->  set  equals :: TREES_9:def 11
 {  (t | p) where t is Element of X, p is Node of t : verum  }  ;
coherence
  {  (t | p) where t is Element of X, p is Node of t : verum  }  is set ;
end;

:: deftheorem  defines Subtrees TREES_9:def_11_:_
 for X being non empty constituted-DTrees set holds Subtrees X =  {  (t | p) where t is Element of X, p is Node of t : verum  }  ;

registration
let X be non empty constituted-DTrees set ;
cluster Subtrees X ->  non empty constituted-DTrees ;
coherence
 ( Subtrees X is constituted-DTrees &amp; not Subtrees X is empty )
proofend;
end;

definition
let D be non empty set ;
let X be non empty Subset of (Trees D);
:: original:Subtrees
redefine func Subtrees X ->  non empty Subset of (Trees D);
coherence
 Subtrees X is non empty Subset of (Trees D)
proofend;
end;

definition
let D be non empty set ;
let X be non empty Subset of (FinTrees D);
:: original:Subtrees
redefine func Subtrees X ->  non empty Subset of (FinTrees D);
coherence
 Subtrees X is non empty Subset of (FinTrees D)
proofend;
end;

theorem Th19: :: TREES_9:19
for x being set
for X being non empty constituted-DTrees set holds
( x in Subtrees X iff ex t being Element of X ex n being Node of t st x = t | n ) ;

theorem :: TREES_9:20
for t being DecoratedTree
for X being non empty constituted-DTrees set st t in X holds
t in Subtrees X
proofend;

theorem :: TREES_9:21
for X, Y being non empty constituted-DTrees set st X c= Y holds
Subtrees X c= Subtrees Y
proofend;

registration
let t be DecoratedTree;
cluster{t} ->  constituted-DTrees ;
coherence
 {t} is constituted-DTrees by TREES_3:14;
end;

theorem :: TREES_9:22
for t being DecoratedTree holds Subtrees {t} = Subtrees t
proofend;

theorem :: TREES_9:23
for X being non empty constituted-DTrees set holds Subtrees X = union  {  (Subtrees t) where t is Element of X : verum  }
proofend;

definition
let X be non empty constituted-DTrees set ;
let C be set ;
funcC -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 )  }  ;
coherence
  {  (t | p) where t is Element of X, p is Node of t : ( not p in Leaves (dom t) or t . p in C )  }  is Subset of (Subtrees X)
proofend;
end;

:: deftheorem  defines -Subtrees TREES_9:def_12_:_
 for X being non empty constituted-DTrees set
for C being set holds C -Subtrees X =  {  (t | p) where t is Element of X, p is Node of t : ( not p in Leaves (dom t) or t . p in C )  }  ;

theorem Th24: :: TREES_9:24
for x, C being set
for X being non empty constituted-DTrees set holds
( x in C -Subtrees X iff ex t being Element of X ex n being Node of t st
( x = t | n &amp; ( not n in Leaves (dom t) or t . n in C ) ) ) ;

theorem :: TREES_9:25
for C being set
for X being non empty constituted-DTrees set holds
( C -Subtrees X is empty iff for t being Element of X holds
( t is root &amp; not t . {} in C ) )
proofend;

theorem :: TREES_9:26
for t being DecoratedTree
for C being set holds C -Subtrees {t} = C -Subtrees t
proofend;

theorem :: TREES_9:27
for C being set
for X being non empty constituted-DTrees set holds C -Subtrees X = union  {  (C -Subtrees t) where t is Element of X : verum  }
proofend;

definition
let X be non empty constituted-DTrees set ;
assume B1: for t being Element of X holds t is finite ;
let C be set ;
funcC -ImmediateSubtrees X ->  Function of (C -Subtrees X),((Subtrees X) *) means :: TREES_9:def 13
 for d being DecoratedTree st d in C -Subtrees X holds
for p being FinSequence of Subtrees X st p = it . d holds
d = (d . {}) -tree p;
existence
 ex b1 being Function of (C -Subtrees X),((Subtrees X) *) st
for d being DecoratedTree st d in C -Subtrees X holds
for p being FinSequence of Subtrees X st p = b1 . d holds
d = (d . {}) -tree p
proofend;
uniqueness
 for b1, b2 being Function of (C -Subtrees X),((Subtrees X) *) st ( for d being DecoratedTree st d in C -Subtrees X holds
for p being FinSequence of Subtrees X st p = b1 . d holds
d = (d . {}) -tree p ) &amp; ( for d being DecoratedTree st d in C -Subtrees X holds
for p being FinSequence of Subtrees X st p = b2 . d holds
d = (d . {}) -tree p ) holds
b1 = b2
proofend;
end;

:: deftheorem  defines -ImmediateSubtrees TREES_9:def_13_:_
 for X being non empty constituted-DTrees set st ( for t being Element of X holds t is finite ) holds
for C being set
for b3 being Function of (C -Subtrees X),((Subtrees X) *) holds
( b3 = C -ImmediateSubtrees X iff for d being DecoratedTree st d in C -Subtrees X holds
for p being FinSequence of Subtrees X st p = b3 . d holds
d = (d . {}) -tree p );

registration
let t be Tree;
cluster Relation-like NAT -defined NAT -valued empty Function-like finite FinSequence-like FinSubsequence-like for Element of t;
existence
 ex b1 being Element of t st b1 is empty
proofend;
end;

theorem :: TREES_9:28
for t being finite DecoratedTree
for p being Element of dom t holds
( len (succ (t,p)) = len (p succ) &amp; dom (succ (t,p)) = dom (p succ) )
proofend;

theorem Th29: :: TREES_9:29
for p being FinTree-yielding FinSequence
for n being empty Element of tree p holds card (succ n) = len p
proofend;

theorem :: TREES_9:30
for t being finite DecoratedTree
for x being set
for p being DTree-yielding FinSequence st t = x -tree p holds
for n being empty Element of dom t holds succ (t,n) = roots p
proofend;

registration
let T be finite-branching DecoratedTree;
let t be Node of T;
clusterT | t ->  finite-branching ;
coherence
 T | t is finite-branching
proofend;
end;

theorem :: TREES_9:31
for t being finite-branching DecoratedTree
for p being Node of t
for q being Node of (t | p) holds succ (t,(p ^ q)) = succ ((t | p),q)
proofend;

begin

theorem Th32: :: TREES_9:32
for n being Element of NAT
for r being FinSequence ex q being FinSequence st
( q = r | (Seg n) &amp; q is_a_prefix_of r )
proofend;

theorem Th33: :: TREES_9:33
for D being non empty set
for r being FinSequence of D
for r1, r2 being FinSequence
for k being Element of NAT st k + 1 <= len r &amp; r1 = r | (Seg (k + 1)) &amp; r2 = r | (Seg k) holds
ex x being Element of D st r1 = r2 ^ <*x*>
proofend;

theorem Th34: :: TREES_9:34
for D being non empty set
for r being FinSequence of D
for r1 being FinSequence st 1 <= len r &amp; r1 = r | (Seg 1) holds
ex x being Element of D st r1 = <*x*>
proofend;

theorem :: TREES_9:35
for T being DecoratedTree
for p being FinSequence of NAT holds T . p = (T | p) . {}
proofend;

theorem Th36: :: TREES_9:36
for T being finite-branching DecoratedTree
for t being Element of dom T holds succ (T,t) = T * (t succ)
proofend;

theorem Th37: :: TREES_9:37
for T being finite-branching DecoratedTree
for t being Element of dom T holds dom (T * (t succ)) = dom (t succ)
proofend;

theorem Th38: :: TREES_9:38
for T being finite-branching DecoratedTree
for t being Element of dom T holds dom (succ (T,t)) = dom (t succ)
proofend;

theorem Th39: :: TREES_9:39
for T being finite-branching DecoratedTree
for t being Element of dom T
for n being Element of NAT holds
( t ^ <*n*> in dom T iff n + 1 in dom (t succ) )
proofend;

theorem Th40: :: TREES_9:40
for T being finite-branching DecoratedTree
for x being FinSequence
for n being Element of NAT st x ^ <*n*> in dom T holds
T . (x ^ <*n*>) = (succ (T,x)) . (n + 1)
proofend;

theorem :: TREES_9:41
for T being finite-branching DecoratedTree
for x9, x being Element of dom T st x9 in succ x holds
T . x9 in rng (succ (T,x))
proofend;

theorem :: TREES_9:42
for T being finite-branching DecoratedTree
for x being Element of dom T
for y9 being set st y9 in rng (succ (T,x)) holds
ex x9 being Element of dom T st
( y9 = T . x9 &amp; x9 in succ x )
proofend;

scheme :: TREES_9:sch 2
ExDecTrees{ F1() ->  non empty set , F2() ->  Element of F1(), F3( set ) ->  FinSequence of F1() } :
 ex T being finite-branching DecoratedTree of F1() st
( T . {} = F2() &amp; ( for t being Element of dom T
for w being Element of F1() st w = T . t holds
succ (T,t) = F3(w) ) )
proofend;

theorem Th43: :: TREES_9:43
for T being Tree
for t being Element of T holds ProperPrefixes t is finite Chain of T
proofend;

theorem Th44: :: TREES_9:44
for T being Tree holds T -level 0 = {{}}
proofend;

theorem Th45: :: TREES_9:45
for n being Element of NAT
for T being Tree holds T -level (n + 1) = union  {  (succ w) where w is Element of T : len w = n  }
proofend;

theorem Th46: :: TREES_9:46
for T being finite-branching Tree
for n being Element of NAT holds T -level n is finite
proofend;

theorem Th47: :: TREES_9:47
for T being finite-branching Tree holds
( T is finite iff ex n being Element of NAT st T -level n = {} )
proofend;

theorem Th48: :: TREES_9:48
for T being finite-branching Tree st not T is finite holds
ex C being Chain of T st not C is finite
proofend;

theorem Th49: :: TREES_9:49
for T being finite-branching Tree st not T is finite holds
ex B being Branch of T st not B is finite
proofend;

theorem Th50: :: TREES_9:50
for T being Tree
for C being Chain of T
for t being Element of T st t in C &amp; not C is finite holds
ex t9 being Element of T st
( t9 in C &amp; t is_a_proper_prefix_of t9 )
proofend;

theorem Th51: :: TREES_9:51
for T being Tree
for B being Branch of T
for t being Element of T st t in B &amp; not B is finite holds
ex t9 being Element of T st
( t9 in B &amp; t9 in succ t )
proofend;

theorem Th52: :: TREES_9:52
for f being Function of NAT,NAT st ( for n being Element of NAT holds f . (n + 1) <= f . n ) holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
f . n = f . m
proofend;

scheme :: TREES_9:sch 3
FinDecTree{ F1() ->  non empty set , F2() ->  finite-branching DecoratedTree of F1(), F3( Element of F1()) ->  Element of NAT } :
 F2() is finite
provided
A1: for t, t9 being Element of dom F2()
for d being Element of F1() st t9 in succ t &amp; d = F2() . t9 holds
F3(d) < F3((F2() . t))
proofend;