:: TREES_9 semantic presentation

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

proof end;

end;

registration

cluster finite -> finite-order set ;
coherence

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

let p, q be FinSequence; :: thesis:
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:
A3: dom p = dom q by A1, FINSEQ_3:31;

now

let i be Nat; :: thesis:
assume i in dom p ; :: thesis:
then consider k being Nat such that
A4: ( i = k + 1 & k < len p ) by Lm1;
thus p . i = q . i by A2, A4; :: thesis:

end;

hence p = q by A3, FINSEQ_1:17; :: thesis:

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

let p be FinSequence; :: thesis:
let x be set ; :: thesis:
assume x in rng p ; :: thesis:
then consider y being set such that
A1: ( y in dom p & x = p . y ) by FUNCT_1:def 5;
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 A1; :: thesis:

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;

definition

let IT be DecoratedTree;
attr IT is root means :Def1: :: TREES_9:def 1
dom IT = elementary_tree 0;

end;

:: deftheorem Def1 defines root TREES_9:def 1 :

registration

cluster root -> finite set ;
coherence

proof end;

end;

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 finite root set ;
existence

proof end;

cluster finite non root set ;
existence

proof end;

end;

registration

let x be set ;
cluster root-tree x -> finite root ;
coherence

proof end;

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 :

registration

cluster finite-order -> finite-branching set ;
coherence

proof end;

end;

registration

cluster finite finite-order finite-branching set ;
existence

proof end;

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 :

:: deftheorem Def4 defines finite-branching TREES_9:def 4 :

registration

cluster finite -> finite-order set ;
coherence

proof end;

cluster finite-order -> finite-branching set ;
coherence

proof end;

end;

registration

cluster finite finite-order finite-branching set ;
existence

proof end;

end;

registration

let t be finite-order DecoratedTree;
cluster dom t -> finite-order finite-branching ;
coherence by Def3;

end;

registration

let t be finite-branching DecoratedTree;
cluster dom t -> finite-branching ;
coherence by Def4;

end;

registration

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

end;

scheme :: TREES_9:sch 1
FinOrdSet{ F₁( set ) -> 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;

registration

let X be set ;
cluster one-to-one empty FinSequence of X;
existence

proof end;

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines succ TREES_9:def 5 :

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

proof end;

uniqueness ;

end;

:: deftheorem Def6 defines succ TREES_9:def 6 :

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;

Lm5: for t being finite DecoratedTree
for p being Node of t holds t | p is finite
;

registration

let t be finite DecoratedTree;
let p be Node of t;
cluster t | p -> finite finite-order finite-branching ;
coherence ;

end;

theorem :: TREES_9:9

canceled;

theorem Th10: :: TREES_9:10

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 Element of S;
coherence

proof end;

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 ;

end;

:: deftheorem defines Subtrees TREES_9:def 7 :

registration

let t be DecoratedTree;
cluster Subtrees t -> non empty constituted-DTrees ;
coherence

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

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

proof end;

end;

registration

let t be finite DecoratedTree;
cluster -> finite Element of Subtrees t;
coherence

proof end;

end;

theorem Th11: :: TREES_9:11

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 Th12: :: TREES_9:12

for t being DecoratedTree holds t in Subtrees t

proof end;

theorem :: TREES_9:13

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

proof end;

theorem :: TREES_9:14

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

proof end;

end;

:: deftheorem defines FixedSubtrees TREES_9:def 8 :

registration

let t be DecoratedTree;
cluster FixedSubtrees t -> non empty ;
coherence

proof end;

end;

theorem :: TREES_9:15

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 Th16: :: TREES_9:16

for t being DecoratedTree holds [{} ,t] in FixedSubtrees t

proof end;

theorem :: TREES_9:17

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

proof end;

end;

:: deftheorem defines -Subtrees TREES_9:def 9 :

theorem Th18: :: TREES_9:18

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

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

proof end;

uniqueness

proof end;

end;

:: deftheorem defines -ImmediateSubtrees TREES_9:def 10 :

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 ;

end;

:: deftheorem defines Subtrees TREES_9:def 11 :

registration

let X be non empty constituted-DTrees set ;
cluster Subtrees X -> non empty constituted-DTrees ;
coherence

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

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

proof end;

end;

theorem Th20: :: TREES_9:20

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

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

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} -> non empty constituted-DTrees ;
coherence by TREES_3:15;

end;

theorem :: TREES_9:23

for t being DecoratedTree holds Subtrees {t} = Subtrees t

proof end;

theorem :: TREES_9:24

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

proof end;

end;

:: deftheorem defines -Subtrees TREES_9:def 12 :

theorem Th25: :: TREES_9:25

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

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

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

proof end;

theorem :: TREES_9:28

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

proof end;

uniqueness

proof end;

end;

:: deftheorem defines -ImmediateSubtrees TREES_9:def 13 :

registration

let t be Tree;
cluster empty Element of t;
existence

proof end;

end;

theorem :: TREES_9:29

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 Th30: :: TREES_9:30

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

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;

theorem :: TREES_9:32

for t being finite 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;