:: TREES_9 semantic presentation

definition

let c₁ be non empty set ;
let c₂ be non empty DTree-set of c₁;
let c₃ be non empty Subset of c₂;
redefine mode Element as Element of c₃ -> Element of a₂;
coherence

proof end;

end;

registration

cluster finite -> finite-order set ;
coherence

proof end;

end;

Lemma1: for b₁ being set
for b₂ being FinSequence st b₁ in dom b₂ holds
ex b₃ being Nat st
( b₁ = b₃ + 1 & b₃ < len b₂ )

proof end;

E2: now

let c₁, c₂ be FinSequence;
assume that
E3: len c₁ = len c₂ and
E4: for b₁ being Nat st b₁ < len c₁ holds
c₁ . (b₁ + 1) = c₂ . (b₁ + 1) ;
E5: dom c₁ = dom c₂ by E3, FINSEQ_3:31;

now

let c₃ be Nat;
assume c₃ in dom c₁ ;
then consider c₄ being Nat such that
E6: ( c₃ = c₄ + 1 & c₄ < len c₁ ) by Lemma1;
thus c₁ . c₃ = c₂ . c₃ by E4, E6;

end;

hence c₁ = c₂ by E5, FINSEQ_1:17;

end;

Lemma3: for b₁ being Nat
for b₂ being FinSequence st b₁ < len b₂ holds
( b₁ + 1 in dom b₂ & b₂ . (b₁ + 1) in rng b₂ )

proof end;

E4: now

let c₁ be FinSequence;
let c₂ be set ;
assume c₂ in rng c₁ ;
then consider c₃ being set such that
E5: ( c₃ in dom c₁ & c₂ = c₁ . c₃ ) by FUNCT_1:def 5;
ex b₁ being Nat st
( c₃ = b₁ + 1 & b₁ < len c₁ ) by E5, Lemma1;
hence ex b₁ being Nat st
( b₁ < len c₁ & c₂ = c₁ . (b₁ + 1) ) by E5;

end;

theorem Th1: :: TREES_9:1

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

proof end;

theorem Th2: :: TREES_9:2

for b₁ being Tree
for b₂, b₃ being FinSequence of NAT st b₂ ^ b₃ in b₁ holds
b₁ | (b₂ ^ b₃) = (b₁ | b₂) | b₃

proof end;

theorem Th3: :: TREES_9:3

for b₁ being DecoratedTree
for b₂, b₃ being FinSequence of NAT st b₂ ^ b₃ in dom b₁ holds
b₁ | (b₂ ^ b₃) = (b₁ | b₂) | b₃

proof end;

definition

let c₁ be DecoratedTree;
attr a₁ is root means :Def1: :: TREES_9:def 1
dom a₁ = 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 b₁ being DecoratedTree holds
( b₁ is root iff {} in Leaves (dom b₁) )

proof end;

theorem Th5: :: TREES_9:5

for b₁ being Tree
for b₂ being Element of b₁ holds
( b₁ | b₂ = elementary_tree 0 iff b₂ in Leaves b₁ )

proof end;

theorem Th6: :: TREES_9:6

for b₁ being DecoratedTree
for b₂ being Node of b₁ holds
( b₁ | b₂ is root iff b₂ in Leaves (dom b₁) )

proof end;

registration

cluster finite root set ;
existence

proof end;

cluster finite non root set ;
existence

proof end;

end;

registration

let c₁ be set ;
cluster root-tree a₁ -> finite root ;
coherence

proof end;

end;

definition

let c₁ be Tree;
attr a₁ is finite-branching means :Def2: :: TREES_9:def 2
for b₁ being Element of a₁ holds succ b₁ 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 c₁ be DecoratedTree;
attr a₁ is finite-order means :Def3: :: TREES_9:def 3
dom a₁ is finite-order;
attr a₁ is finite-branching means :Def4: :: TREES_9:def 4
dom a₁ 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 c₁ be finite-order DecoratedTree;
cluster dom a₁ -> finite-order finite-branching ;
coherence by Def3;

end;

registration

let c₁ be finite-branching DecoratedTree;
cluster dom a₁ -> finite-branching ;
coherence by Def4;

end;

registration

let c₁ be finite-branching Tree;
let c₂ be Element of c₁;
cluster succ a₂ -> finite ;
coherence by Def2;

end;

scheme :: TREES_9:sch 1
s1{ F₁( set ) -> set , F₂() -> finite set } :

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

provided

E14: for b₁ being set st b₁ in F₂() holds
ex b₂ being Nat st b₁ = F₁(b₂) and
E15: for b₁, b₂ being Nat st b₁ < b₂ & F₁(b₂) in F₂() holds
F₁(b₁) in F₂() and
E16: for b₁, b₂ being Nat st F₁(b₁) = F₁(b₂) holds
b₁ = b₂

proof end;

registration

let c₁ be set ;
cluster one-to-one empty FinSequence of a₁;
existence

proof end;

end;

theorem Th7: :: TREES_9:7

for b₁ being finite-branching Tree
for b₂ being Element of b₁
for b₃ being Nat holds
( b₂ ^ <*b₃*> in succ b₂ iff b₃ < card (succ b₂) )

proof end;

definition

let c₁ be finite-branching Tree;
let c₂ be Element of c₁;
func c₂ succ -> one-to-one FinSequence of a₁ means :Def5: :: TREES_9:def 5
( len a₃ = card (succ a₂) & rng a₃ = succ a₂ & ( for b₁ being Nat st b₁ < len a₃ holds
a₃ . (b₁ + 1) = a₂ ^ <*b₁*> ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines succ TREES_9:def 5 :

definition

let c₁ be finite-branching DecoratedTree;
let c₂ be FinSequence;
assume E16: c₂ in dom c₁ ;
func succ c₁,c₂ -> FinSequence means :Def6: :: TREES_9:def 6
ex b₁ being Element of dom a₁ st
( b₁ = a₂ & a₃ = a₁ * (b₁ succ ) );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def6 defines succ TREES_9:def 6 :

theorem Th8: :: TREES_9:8

for b₁ being finite-branching DecoratedTree ex b₂ being set ex b₃ being DTree-yielding FinSequence st b₁ = b₂ -tree b₃

proof end;

Lemma18: for b₁ being finite DecoratedTree
for b₂ being Node of b₁ holds b₁ | b₂ is finite
;

registration

let c₁ be finite DecoratedTree;
let c₂ be Node of c₁;
cluster a₁ | a₂ -> finite finite-order finite-branching ;
coherence ;

end;

theorem Th9: :: TREES_9:9

canceled;

theorem Th10: :: TREES_9:10

for b₁ being finite Tree
for b₂ being Element of b₁ st b₁ = b₁ | b₂ holds
b₂ = {}

proof end;

registration

let c₁ be non empty set ;
let c₂ be non empty Subset of (FinTrees c₁);
cluster -> finite Element of a₂;
coherence

proof end;

end;

definition

let c₁ be DecoratedTree;
func Subtrees c₁ -> set equals :: TREES_9:def 7
{ (a₁ | b₁) where B is Node of a₁ : verum } ;
coherence ;

end;

:: deftheorem Def7 defines Subtrees TREES_9:def 7 :

registration

let c₁ be DecoratedTree;
cluster Subtrees a₁ -> non empty constituted-DTrees ;
coherence

proof end;

end;

definition

let c₁ be non empty set ;
let c₂ be DecoratedTree of c₁;
redefine func Subtrees as Subtrees c₂ -> non empty Subset of (Trees a₁);
coherence

proof end;

end;

definition

let c₁ be non empty set ;
let c₂ be finite DecoratedTree of c₁;
redefine func Subtrees as Subtrees c₂ -> non empty Subset of (FinTrees a₁);
coherence

proof end;

end;

registration

let c₁ be finite DecoratedTree;
cluster -> finite Element of Subtrees a₁;
coherence

proof end;

end;

theorem Th11: :: TREES_9:11

for b₁ being set
for b₂ being DecoratedTree holds
( b₁ in Subtrees b₂ iff ex b₃ being Node of b₂ st b₁ = b₂ | b₃ ) ;

theorem Th12: :: TREES_9:12

for b₁ being DecoratedTree holds b₁ in Subtrees b₁

proof end;

theorem Th13: :: TREES_9:13

for b₁, b₂ being DecoratedTree st b₁ is finite & Subtrees b₁ = Subtrees b₂ holds
b₁ = b₂

proof end;

theorem Th14: :: TREES_9:14

for b₁ being DecoratedTree
for b₂ being Node of b₁ holds Subtrees (b₁ | b₂) c= Subtrees b₁

proof end;

definition

let c₁ be DecoratedTree;
func FixedSubtrees c₁ -> Subset of [:(dom a₁),(Subtrees a₁):] equals :: TREES_9:def 8
{ [b₁,(a₁ | b₁)] where B is Node of a₁ : verum } ;
coherence

proof end;

end;

:: deftheorem Def8 defines FixedSubtrees TREES_9:def 8 :

registration

let c₁ be DecoratedTree;
cluster FixedSubtrees a₁ -> non empty ;
coherence

proof end;

end;

theorem Th15: :: TREES_9:15

for b₁ being set
for b₂ being DecoratedTree holds
( b₁ in FixedSubtrees b₂ iff ex b₃ being Node of b₂ st b₁ = [b₃,(b₂ | b₃)] ) ;

theorem Th16: :: TREES_9:16

for b₁ being DecoratedTree holds [{} ,b₁] in FixedSubtrees b₁

proof end;

theorem Th17: :: TREES_9:17

for b₁, b₂ being DecoratedTree st FixedSubtrees b₁ = FixedSubtrees b₂ holds
b₁ = b₂

proof end;

definition

let c₁ be DecoratedTree;
let c₂ be set ;
func c₂ -Subtrees c₁ -> Subset of (Subtrees a₁) equals :: TREES_9:def 9
{ (a₁ | b₁) where B is Node of a₁ : ( not b₁ in Leaves (dom a₁) or a₁ . b₁ in a₂ ) } ;
coherence

proof end;

end;

:: deftheorem Def9 defines -Subtrees TREES_9:def 9 :

theorem Th18: :: TREES_9:18

for b₁ being set
for b₂ being DecoratedTree
for b₃ being set holds
( b₁ in b₃ -Subtrees b₂ iff ex b₄ being Node of b₂ st
( b₁ = b₂ | b₄ & ( not b₄ in Leaves (dom b₂) or b₂ . b₄ in b₃ ) ) ) ;

theorem Th19: :: TREES_9:19

for b₁ being DecoratedTree
for b₂ being set holds
( b₂ -Subtrees b₁ is empty iff ( b₁ is root & not b₁ . {} in b₂ ) )

proof end;

definition

let c₁ be finite DecoratedTree;
let c₂ be set ;
func c₂ -ImmediateSubtrees c₁ -> Function of a₂ -Subtrees a₁,(Subtrees a₁) * means :: TREES_9:def 10
for b₁ being DecoratedTree st b₁ in a₂ -Subtrees a₁ holds
for b₂ being FinSequence of Subtrees a₁ st b₂ = a₃ . b₁ holds
b₁ = (b₁ . {} ) -tree b₂;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def10 defines -ImmediateSubtrees TREES_9:def 10 :

definition

let c₁ be non empty constituted-DTrees set ;
func Subtrees c₁ -> set equals :: TREES_9:def 11
{ (b₁ | b₂) where B is Element of a₁, B is Node of b₁ : verum } ;
coherence ;

end;

:: deftheorem Def11 defines Subtrees TREES_9:def 11 :

registration

let c₁ be non empty constituted-DTrees set ;
cluster Subtrees a₁ -> non empty constituted-DTrees ;
coherence

proof end;

end;

definition

let c₁ be non empty set ;
let c₂ be non empty Subset of (Trees c₁);
redefine func Subtrees as Subtrees c₂ -> non empty Subset of (Trees a₁);
coherence

proof end;

end;

definition

let c₁ be non empty set ;
let c₂ be non empty Subset of (FinTrees c₁);
redefine func Subtrees as Subtrees c₂ -> non empty Subset of (FinTrees a₁);
coherence

proof end;

end;

theorem Th20: :: TREES_9:20

for b₁ being set
for b₂ being non empty constituted-DTrees set holds
( b₁ in Subtrees b₂ iff ex b₃ being Element of b₂ex b₄ being Node of b₃ st b₁ = b₃ | b₄ ) ;

theorem Th21: :: TREES_9:21

for b₁ being DecoratedTree
for b₂ being non empty constituted-DTrees set st b₁ in b₂ holds
b₁ in Subtrees b₂

proof end;

theorem Th22: :: TREES_9:22

for b₁, b₂ being non empty constituted-DTrees set st b₁ c= b₂ holds
Subtrees b₁ c= Subtrees b₂

proof end;

registration

let c₁ be DecoratedTree;
cluster {a₁} -> non empty constituted-DTrees ;
coherence by TREES_3:15;

end;

theorem Th23: :: TREES_9:23

for b₁ being DecoratedTree holds Subtrees {b₁} = Subtrees b₁

proof end;

theorem Th24: :: TREES_9:24

for b₁ being non empty constituted-DTrees set holds Subtrees b₁ = union { (Subtrees b₂) where B is Element of b₁ : verum }

proof end;

definition

let c₁ be non empty constituted-DTrees set ;
let c₂ be set ;
func c₂ -Subtrees c₁ -> Subset of (Subtrees a₁) equals :: TREES_9:def 12
{ (b₁ | b₂) where B is Element of a₁, B is Node of b₁ : ( not b₂ in Leaves (dom b₁) or b₁ . b₂ in a₂ ) } ;
coherence

proof end;

end;

:: deftheorem Def12 defines -Subtrees TREES_9:def 12 :

theorem Th25: :: TREES_9:25

for b₁, b₂ being set
for b₃ being non empty constituted-DTrees set holds
( b₁ in b₂ -Subtrees b₃ iff ex b₄ being Element of b₃ex b₅ being Node of b₄ st
( b₁ = b₄ | b₅ & ( not b₅ in Leaves (dom b₄) or b₄ . b₅ in b₂ ) ) ) ;

theorem Th26: :: TREES_9:26

for b₁ being set
for b₂ being non empty constituted-DTrees set holds
( b₁ -Subtrees b₂ is empty iff for b₃ being Element of b₂ holds
( b₃ is root & not b₃ . {} in b₁ ) )

proof end;

theorem Th27: :: TREES_9:27

for b₁ being DecoratedTree
for b₂ being set holds b₂ -Subtrees {b₁} = b₂ -Subtrees b₁

proof end;

theorem Th28: :: TREES_9:28

for b₁ being set
for b₂ being non empty constituted-DTrees set holds b₁ -Subtrees b₂ = union { (b₁ -Subtrees b₃) where B is Element of b₂ : verum }

proof end;

definition

let c₁ be non empty constituted-DTrees set ;
assume E26: for b₁ being Element of c₁ holds b₁ is finite ;
let c₂ be set ;
func c₂ -ImmediateSubtrees c₁ -> Function of a₂ -Subtrees a₁,(Subtrees a₁) * means :: TREES_9:def 13
for b₁ being DecoratedTree st b₁ in a₂ -Subtrees a₁ holds
for b₂ being FinSequence of Subtrees a₁ st b₂ = a₃ . b₁ holds
b₁ = (b₁ . {} ) -tree b₂;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def13 defines -ImmediateSubtrees TREES_9:def 13 :

registration

let c₁ be Tree;
cluster empty Element of a₁;
existence

proof end;

end;

theorem Th29: :: TREES_9:29

for b₁ being finite DecoratedTree
for b₂ being Element of dom b₁ holds
( len (succ b₁,b₂) = len (b₂ succ ) & dom (succ b₁,b₂) = dom (b₂ succ ) )

proof end;

theorem Th30: :: TREES_9:30

for b₁ being FinTree-yielding FinSequence
for b₂ being empty Element of tree b₁ holds card (succ b₂) = len b₁

proof end;

theorem Th31: :: TREES_9:31

for b₁ being finite DecoratedTree
for b₂ being set
for b₃ being DTree-yielding FinSequence st b₁ = b₂ -tree b₃ holds
for b₄ being empty Element of dom b₁ holds succ b₁,b₄ = roots b₃

proof end;

theorem Th32: :: TREES_9:32

for b₁ being finite DecoratedTree
for b₂ being Node of b₁
for b₃ being Node of (b₁ | b₂) holds succ b₁,(b₂ ^ b₃) = succ (b₁ | b₂),b₃

proof end;