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

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 b₁ being Element of Tset holds b₁ is Element of F

proof end;

end;

registration

cluster non empty finite Tree-like -> finite-order for set ;

coherence
for b₁ being Tree st b₁ is finite holds
b₁ is finite-order

proof end;

end;

Lm1: for n being set
for p being FinSequence st n in dom p holds
ex k being Nat st
( n = k + 1 & k < len p )

proof end;

Lm2: now :: thesis: for p, q being FinSequence st len p = len q & ( for i being 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 & ( for i being 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 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 Nat st
( i = k + 1 & 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; :: thesis: verum

end;

Lm3: for n being Nat
for p being FinSequence st n < len p holds
( n + 1 in dom p & p . (n + 1) in rng p )

proof end;

Lm4: now :: thesis: for p being FinSequence
for x being set st x in rng p holds
ex k being Nat st
( k < len p & x = p . (k + 1) )

let p be FinSequence; :: thesis: for x being set st x in rng p holds
ex k being Nat st
( k < len p & x = p . (k + 1) )
let x be set ; :: thesis: ( x in rng p implies ex k being Nat st
( k < len p & x = p . (k + 1) ) )
assume x in rng p ; :: thesis: ex k being Nat st
( k < len p & x = p . (k + 1) )
then consider y being object such that
A1: y in dom p and
A2: x = p . y by FUNCT_1:def 3;
ex k being Nat st
( y = k + 1 & k < len p ) by A1, Lm1;
hence ex k being Nat st
( k < len p & x = p . (k + 1) ) by A2; :: thesis: verum

end;

theorem Th1: :: TREES_9:1

for t being DecoratedTree holds t | (<*> NAT) = t

proof end;

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

proof end;

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

proof end;

notation

let IT be DecoratedTree;
synonym root IT for trivial ;

end;

definition

let IT be DecoratedTree;

redefine attr IT is trivial means :: TREES_9:def 1
dom IT = elementary_tree 0;

compatibility
( IT is root iff dom IT = elementary_tree 0 )

proof end;

end;

:: deftheorem 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) )

proof end;

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 )

proof end;

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) )

proof end;

registration

cluster Relation-like root Function-like DecoratedTree-like for set ;

existence
ex b₁ being DecoratedTree st b₁ is root

proof end;

cluster Relation-like non root Function-like finite DecoratedTree-like for set ;

existence
ex b₁ being DecoratedTree st
( b₁ is finite & not b₁ is root )

proof end;

end;

registration

let x be object ;

cluster root-tree x -> root finite ;

coherence
( root-tree x is finite & root-tree x is root ) by TREES_4:3;

end;

definition

let IT be Tree;

attr IT 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 b₁ being Tree st b₁ is finite-order holds
b₁ is finite-branching ;

end;

definition

let IT be DecoratedTree;

attr IT is finite-order means :Def3: :: TREES_9:def 3
dom IT is finite-order ;

attr IT 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 b₁ being DecoratedTree st b₁ is finite holds
b₁ is finite-order ;

cluster Relation-like Function-like DecoratedTree-like finite-order -> finite-branching for set ;

coherence
for b₁ being DecoratedTree st b₁ is finite-order holds
b₁ is finite-branching ;

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{ F₁( object ) -> set , F₂() -> finite set } :

for n being Nat holds
( F₁(n) in F₂() iff n < card F₂() )

provided

A1: for x being set st x in F₂() holds
ex n being Nat st x = F₁(n) and
A2: for i, j being Nat st i < j & F₁(j) in F₂() holds
F₁(i) in F₂() and
A3: for i, j being Nat st F₁(i) = F₁(j) holds
i = j

proof end;

theorem Th7: :: TREES_9:7

for t being finite-branching Tree
for p being Element of t
for n being Nat holds
( p ^ <*n*> in succ p iff n < card (succ p) )

proof end;

definition

let t be finite-branching Tree;
let p be Element of t;

func p succ -> one-to-one FinSequence of t means :Def5: :: 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*> ) );

existence
ex b₁ being one-to-one FinSequence of t st
( len b₁ = card (succ p) & rng b₁ = succ p & ( for i being Nat st i < len b₁ holds
b₁ . (i + 1) = p ^ <*i*> ) )

proof end;

uniqueness
for b₁, b₂ being one-to-one FinSequence of t st len b₁ = card (succ p) & rng b₁ = succ p & ( for i being Nat st i < len b₁ holds
b₁ . (i + 1) = p ^ <*i*> ) & len b₂ = card (succ p) & rng b₂ = succ p & ( for i being Nat st i < len b₂ holds
b₂ . (i + 1) = p ^ <*i*> ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def5 defines succ TREES_9:def 5 :
for t being finite-branching Tree
for p being Element of t
for b₃ being one-to-one FinSequence of t holds
( b₃ = p succ iff ( len b₃ = card (succ p) & rng b₃ = succ p & ( for i being Nat st i < len b₃ holds
b₃ . (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 & it = t * (q succ) );

existence
ex b₁ being FinSequence ex q being Element of dom t st
( q = p & b₁ = t * (q succ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence st ex q being Element of dom t st
( q = p & b₁ = t * (q succ) ) & ex q being Element of dom t st
( q = p & b₂ = t * (q succ) ) holds
b₁ = b₂ ;

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 b₃ being FinSequence holds
( b₃ = succ (t,p) iff ex q being Element of dom t st
( q = p & b₃ = 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

proof end;

registration

let t be finite DecoratedTree;
let p be Node of t;

cluster t | 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 = {}

proof end;

registration

let D be non empty set ;
let S be non empty Subset of (FinTrees D);

cluster -> finite for Element of S;

coherence
for b₁ being Element of S holds b₁ is finite ;

end;

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 & not Subtrees t is empty )

proof end;

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)

proof end;

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)

proof end;

end;

registration

let t be finite DecoratedTree;

cluster -> finite for Element of Subtrees t;

coherence
for b₁ being Element of Subtrees t holds b₁ is finite

proof end;

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

proof end;

theorem :: TREES_9:12

for t1, t2 being DecoratedTree st t1 is finite & Subtrees t1 = Subtrees t2 holds
t1 = t2

proof end;

theorem :: TREES_9:13

for t being DecoratedTree
for n being Node of t holds Subtrees (t | n) c= Subtrees t

proof end;

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):]

proof end;

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

proof end;

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

proof end;

theorem :: TREES_9:16

for t1, t2 being DecoratedTree st FixedSubtrees t1 = FixedSubtrees t2 holds
t1 = t2

proof end;

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 ) } ;

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)

proof end;

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 & ( 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 & not t . {} in C ) )

proof end;

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 holds
for p being FinSequence of Subtrees t st p = it . d holds
d = (d . {}) -tree p;

existence
ex b₁ 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 = b₁ . d holds
d = (d . {}) -tree p

proof end;

uniqueness
for b₁, b₂ 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 = b₁ . d holds
d = (d . {}) -tree p ) & ( for d being DecoratedTree st d in C -Subtrees t holds
for p being FinSequence of Subtrees t st p = b₂ . d holds
d = (d . {}) -tree p ) holds
b₁ = b₂

proof end;

end;

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

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 & not Subtrees X is empty )

proof end;

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)

proof end;

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)

proof end;

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

proof end;

theorem :: TREES_9:21

for X, Y being non empty constituted-DTrees set st X c= Y holds
Subtrees X c= Subtrees Y

proof end;

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

proof end;

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 }

proof end;

definition

let X be non empty constituted-DTrees 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 ) } ;

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)

proof end;

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 & ( 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 & not t . {} in C ) )

proof end;

theorem :: TREES_9:26

for t being DecoratedTree
for C being set holds C -Subtrees {t} = C -Subtrees t

proof end;

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 }

proof end;

definition

let X be non empty constituted-DTrees set ;
assume A1: 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 holds
for p being FinSequence of Subtrees X st p = it . d holds
d = (d . {}) -tree p;

existence
ex b₁ 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 = b₁ . d holds
d = (d . {}) -tree p

proof end;

uniqueness
for b₁, b₂ 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 = b₁ . d holds
d = (d . {}) -tree p ) & ( for d being DecoratedTree st d in C -Subtrees X holds
for p being FinSequence of Subtrees X st p = b₂ . d holds
d = (d . {}) -tree p ) holds
b₁ = b₂

proof end;

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 b₃ being Function of (C -Subtrees X),((Subtrees X) *) holds
( b₃ = C -ImmediateSubtrees X iff for d being DecoratedTree st d in C -Subtrees X holds
for p being FinSequence of Subtrees X st p = b₃ . d holds
d = (d . {}) -tree p );

registration

let t be Tree;

cluster Relation-like omega -defined omega -valued empty Function-like finite FinSequence-like FinSubsequence-like for Element of t;

existence
ex b₁ being Element of t st b₁ is empty

proof end;

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) & dom (succ (t,p)) = dom (p succ) )

proof end;

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

proof end;

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

proof end;

registration

let T be finite-branching DecoratedTree;
let t be Node of T;

cluster T | t -> finite-branching ;

coherence
T | t is finite-branching

proof end;

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)

proof end;

theorem Th32: :: TREES_9:32

for n being Nat
for r being FinSequence ex q being FinSequence st
( q = r | (Seg n) & q is_a_prefix_of r )

proof end;

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 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*>

proof end;

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 & r1 = r | (Seg 1) holds
ex x being Element of D st r1 = <*x*>

proof end;

theorem :: TREES_9:35

for T being DecoratedTree
for p being FinSequence of NAT holds T . p = (T | p) . {}

proof end;

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)

proof end;

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)

proof end;

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)

proof end;

theorem Th39: :: TREES_9:39

for T being finite-branching DecoratedTree
for t being Element of dom T
for n being Nat holds
( t ^ <*n*> in dom T iff n + 1 in dom (t succ) )

proof end;

theorem Th40: :: TREES_9:40

for T being finite-branching DecoratedTree
for x being FinSequence
for n being Nat st x ^ <*n*> in dom T holds
T . (x ^ <*n*>) = (succ (T,x)) . (n + 1)

proof end;

theorem :: TREES_9:41

for T being finite-branching DecoratedTree
for x, x9 being Element of dom T st x9 in succ x holds
T . x9 in rng (succ (T,x))

proof end;

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 & x9 in succ x )

proof end;

scheme :: TREES_9:sch 2
ExDecTrees{ F₁() -> non empty set , F₂() -> Element of F₁(), F₃( object ) -> FinSequence of F₁() } :

ex T being finite-branching DecoratedTree of F₁() st
( T . {} = F₂() & ( for t being Element of dom T
for w being Element of F₁() st w = T . t holds
succ (T,t) = F₃(w) ) )

proof end;

theorem Th43: :: TREES_9:43

for T being Tree
for t being Element of T holds ProperPrefixes t is finite Chain of T

proof end;

theorem Th44: :: TREES_9:44

for T being Tree holds T -level 0 = {{}}

proof end;

theorem Th45: :: TREES_9:45

for n being Nat
for T being Tree holds T -level (n + 1) = union { (succ w) where w is Element of T : len w = n }

proof end;

theorem Th46: :: TREES_9:46

for T being finite-branching Tree
for n being Nat holds T -level n is finite

proof end;

theorem Th47: :: TREES_9:47

for T being finite-branching Tree holds
( T is finite iff ex n being Nat st T -level n = {} )

proof end;

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

proof end;

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

proof end;

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 & not C is finite holds
ex t9 being Element of T st
( t9 in C & t is_a_proper_prefix_of t9 )

proof end;

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 & not B is finite holds
ex t9 being Element of T st
( t9 in B & t9 in succ t )

proof end;

theorem Th52: :: TREES_9:52

for f being sequence of NAT st ( for n being Nat holds f . (n + 1) <= f . n ) holds
ex m being Nat st
for n being Nat st m <= n holds
f . n = f . m

proof end;

scheme :: TREES_9:sch 3
FinDecTree{ F₁() -> non empty set , F₂() -> finite-branching DecoratedTree of F₁(), F₃( Element of F₁()) -> Nat } :

F₂() is finite

provided

A1: for t, t9 being Element of dom F₂()
for d being Element of F₁() st t9 in succ t & d = F₂() . t9 holds
F₃(d) < F₃((F₂() . t))

proof end;