:: by Grzegorz Bancerek

::

:: Received November 25, 1994

:: Copyright (c) 1994-2018 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_{1} being Element of Tset holds b_{1} is Element of F

end;
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

proof end;

registration
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

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

hence p = q by A3; :: thesis: verum

end;
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

dom p = dom q
by A1, FINSEQ_3:29;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;
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

hence p = q by A3; :: thesis: verum

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

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

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

for p, q being FinSequence of NAT st p ^ q in dom t holds

t | (p ^ q) = (t | p) | q

proof end;

definition
end;

:: deftheorem defines root TREES_9:def 1 :

for IT being DecoratedTree holds

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

for IT being DecoratedTree holds

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

registration

existence

ex b_{1} being DecoratedTree st b_{1} is root

ex b_{1} being DecoratedTree st

( b_{1} is finite & not b_{1} is root )

end;
ex b

proof end;

existence ex b

( b

proof end;

registration
end;

definition

let IT be Tree;

end;
attr IT is finite-branching means :Def2: :: TREES_9:def 2

for x being Element of IT holds succ x is finite ;

for x being Element of IT holds succ x is finite ;

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

for IT being Tree holds

( IT is finite-branching iff for x being Element of IT holds succ x is finite );

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

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

for IT being DecoratedTree holds

( IT is finite-branching iff dom IT is finite-branching );

registration

coherence

for b_{1} being DecoratedTree st b_{1} is finite holds

b_{1} is finite-order
;

for b_{1} being DecoratedTree st b_{1} is finite-order holds

b_{1} is finite-branching
;

end;
for b

b

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

coherence for b

b

registration
end;

registration
end;

scheme :: TREES_9:sch 1

FinOrdSet{ F_{1}( object ) -> set , F_{2}() -> finite set } :

provided

FinOrdSet{ F

provided

A1:
for x being set st x in F_{2}() holds

ex n being Nat st x = F_{1}(n)
and

A2: for i, j being Nat st i < j & F_{1}(j) in F_{2}() holds

F_{1}(i) in F_{2}()
and

A3: for i, j being Nat st F_{1}(i) = F_{1}(j) holds

i = j

ex n being Nat st x = F

A2: for i, j being Nat st i < j & F

F

A3: for i, j being Nat st F

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

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;

ex b_{1} being one-to-one FinSequence of t st

( len b_{1} = card (succ p) & rng b_{1} = succ p & ( for i being Nat st i < len b_{1} holds

b_{1} . (i + 1) = p ^ <*i*> ) )

for b_{1}, b_{2} being one-to-one FinSequence of t st len b_{1} = card (succ p) & rng b_{1} = succ p & ( for i being Nat st i < len b_{1} holds

b_{1} . (i + 1) = p ^ <*i*> ) & len b_{2} = card (succ p) & rng b_{2} = succ p & ( for i being Nat st i < len b_{2} holds

b_{2} . (i + 1) = p ^ <*i*> ) holds

b_{1} = b_{2}

end;
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 ( len it = card (succ p) & rng it = succ p & ( for i being Nat st i < len it holds

it . (i + 1) = p ^ <*i*> ) );

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def5 defines succ TREES_9:def 5 :

for t being finite-branching Tree

for p being Element of t

for b_{3} being one-to-one FinSequence of t holds

( b_{3} = p succ iff ( len b_{3} = card (succ p) & rng b_{3} = succ p & ( for i being Nat st i < len b_{3} holds

b_{3} . (i + 1) = p ^ <*i*> ) ) );

for t being finite-branching Tree

for p being Element of t

for b

( b

b

definition

let t be finite-branching DecoratedTree;

let p be FinSequence;

assume A1: p in dom t ;

ex b_{1} being FinSequence ex q being Element of dom t st

( q = p & b_{1} = t * (q succ) )

for b_{1}, b_{2} being FinSequence st ex q being Element of dom t st

( q = p & b_{1} = t * (q succ) ) & ex q being Element of dom t st

( q = p & b_{2} = t * (q succ) ) holds

b_{1} = b_{2}
;

end;
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 q being Element of dom t st

( q = p & it = t * (q succ) );

ex b

( q = p & b

proof end;

uniqueness for b

( q = p & b

( q = p & b

b

:: 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_{3} being FinSequence holds

( b_{3} = succ (t,p) iff ex q being Element of dom t st

( q = p & b_{3} = t * (q succ) ) );

for t being finite-branching DecoratedTree

for p being FinSequence st p in dom t holds

for b

( b

( q = p & b

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 D be non empty set ;

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

coherence

for b_{1} being Element of S holds b_{1} is finite
;

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

coherence

for b

:: deftheorem defines Subtrees TREES_9:def 7 :

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

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

registration

let t be DecoratedTree;

coherence

( Subtrees t is constituted-DTrees & not Subtrees t is empty )

end;
coherence

( Subtrees t is constituted-DTrees & not Subtrees t is empty )

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

end;
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;

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)

end;
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;

registration

let t be finite DecoratedTree;

coherence

for b_{1} being Element of Subtrees t holds b_{1} is finite

end;
coherence

for b

proof end;

definition

let t be DecoratedTree;

{ [p,(t | p)] where p is Node of t : verum } is Subset of [:(dom t),(Subtrees t):]

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

{ [p,(t | p)] where p is Node of t : verum } is Subset of [:(dom t),(Subtrees t):]

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

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

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

for t being DecoratedTree holds

( x in FixedSubtrees t iff ex n being Node of t st x = [n,(t | n)] ) ;

definition

let t be DecoratedTree;

let C be set ;

{ (t | p) where p is Node of t : ( not p in Leaves (dom t) or t . p in C ) } is Subset of (Subtrees t)

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

{ (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;

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

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

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 ;

ex b_{1} 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_{1} . d holds

d = (d . {}) -tree p

for b_{1}, b_{2} 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_{1} . 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_{2} . d holds

d = (d . {}) -tree p ) holds

b_{1} = b_{2}

end;
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 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;

ex b

for d being DecoratedTree st d in C -Subtrees t holds

for p being FinSequence of Subtrees t st p = b

d = (d . {}) -tree p

proof end;

uniqueness for b

for p being FinSequence of Subtrees t st p = b

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

b

proof end;

:: deftheorem defines -ImmediateSubtrees TREES_9:def 10 :

for t being finite DecoratedTree

for C being set

for b_{3} being Function of (C -Subtrees t),((Subtrees t) *) holds

( b_{3} = 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_{3} . d holds

d = (d . {}) -tree p );

for t being finite DecoratedTree

for C being set

for b

( b

for p being FinSequence of Subtrees t st p = b

d = (d . {}) -tree p );

definition

let X be non empty constituted-DTrees set ;

{ (t | p) where t is Element of X, p is Node of t : verum } is set ;

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

{ (t | p) where t is Element of X, p is Node of t : verum } is set ;

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

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 ;

coherence

( Subtrees X is constituted-DTrees & not Subtrees X is empty )

end;
coherence

( Subtrees X is constituted-DTrees & not Subtrees X is empty )

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

end;
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;

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)

end;
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;

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

for X being non empty constituted-DTrees set st t in X holds

t in Subtrees X

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 ;

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

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

{ (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;

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

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

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: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 }

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 ;

ex b_{1} 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_{1} . d holds

d = (d . {}) -tree p

for b_{1}, b_{2} 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_{1} . 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_{2} . d holds

d = (d . {}) -tree p ) holds

b_{1} = b_{2}

end;
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 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;

ex b

for d being DecoratedTree st d in C -Subtrees X holds

for p being FinSequence of Subtrees X st p = b

d = (d . {}) -tree p

proof end;

uniqueness for b

for p being FinSequence of Subtrees X st p = b

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

b

proof 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_{3} being Function of (C -Subtrees X),((Subtrees X) *) holds

( b_{3} = 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_{3} . d holds

d = (d . {}) -tree p );

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

( b

for p being FinSequence of Subtrees X st p = b

d = (d . {}) -tree p );

registration

let t be Tree;

ex b_{1} being Element of t st b_{1} is empty

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

existence ex b

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

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

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

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;

coherence

T | t is finite-branching

end;
let t be Node of T;

coherence

T | t is finite-branching

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

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 )

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

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

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 Th36: :: TREES_9:36

for T being finite-branching DecoratedTree

for t being Element of dom T holds succ (T,t) = T * (t succ)

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)

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)

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

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)

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

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 )

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_{1}() -> non empty set , F_{2}() -> Element of F_{1}(), F_{3}( object ) -> FinSequence of F_{1}() } :

ExDecTrees{ F

ex T being finite-branching DecoratedTree of F_{1}() st

( T . {} = F_{2}() & ( for t being Element of dom T

for w being Element of F_{1}() st w = T . t holds

succ (T,t) = F_{3}(w) ) )

( T . {} = F

for w being Element of F

succ (T,t) = F

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 }

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

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

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 )

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 )

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

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_{1}() -> non empty set , F_{2}() -> finite-branching DecoratedTree of F_{1}(), F_{3}( Element of F_{1}()) -> Nat } :

provided

FinDecTree{ F

provided

A1:
for t, t9 being Element of dom F_{2}()

for d being Element of F_{1}() st t9 in succ t & d = F_{2}() . t9 holds

F_{3}(d) < F_{3}((F_{2}() . t))

for d being Element of F

F

proof end;