:: TREES_2 semantic presentation

theorem Th1: :: TREES_2:1

for b₁, b₂, b₃ being FinSequence st b₁ is_a_prefix_of b₃ & b₂ is_a_prefix_of b₃ holds
b₁,b₂ are_c=-comparable

proof end;

theorem Th2: :: TREES_2:2

for b₁, b₂, b₃ being FinSequence st b₁ is_a_proper_prefix_of b₃ & b₂ is_a_prefix_of b₃ holds
b₁,b₂ are_c=-comparable

proof end;

Lemma3: for b₁ being set
for b₂ being FinSequence holds len (b₂ ^ <*b₁*>) = (len b₂) + 1

proof end;

theorem Th3: :: TREES_2:3

canceled;

theorem Th4: :: TREES_2:4

for b₁ being Nat
for b₂ being FinSequence st len b₂ = b₁ + 1 holds
ex b₃ being FinSequenceex b₄ being set st
( b₂ = b₃ ^ <*b₄*> & len b₃ = b₁ )

proof end;

theorem Th5: :: TREES_2:5

canceled;

theorem Th6: :: TREES_2:6

for b₁ being set
for b₂ being FinSequence holds ProperPrefixes (b₂ ^ <*b₁*>) = (ProperPrefixes b₂) \/ {b₂}

proof end;

scheme :: TREES_2:sch 1
s1{ F₁() -> Tree, P₁[ set ] } :

for b₁ being Element of F₁() holds P₁[b₁]

provided

E6: P₁[ {} ] and
E7: for b₁ being Element of F₁()
for b₂ being Nat st P₁[b₁] & b₁ ^ <*b₂*> in F₁() holds
P₁[b₁ ^ <*b₂*>]

proof end;

theorem Th7: :: TREES_2:7

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

proof end;

definition

let c₁, c₂ be Tree;
redefine pred c₁ = c₂ means :: TREES_2:def 1
for b₁ being FinSequence of NAT holds
( b₁ in a₁ iff b₁ in a₂ );
compatibility by Th7;

end;

:: deftheorem Def1 defines = TREES_2:def 1 :

theorem Th8: :: TREES_2:8

for b₁ being Tree
for b₂ being FinSequence of NAT st b₂ in b₁ holds
b₁ = b₁ with-replacement b₂,(b₁ | b₂)

proof end;

theorem Th9: :: TREES_2:9

for b₁, b₂ being Tree
for b₃, b₄ being FinSequence of NAT st b₃ in b₁ & b₄ in b₁ & not b₃ is_a_prefix_of b₄ holds
b₄ in b₁ with-replacement b₃,b₂

proof end;

theorem Th10: :: TREES_2:10

for b₁, b₂, b₃ being Tree
for b₄, b₅ being FinSequence of NAT st b₄ in b₁ & b₅ in b₁ & not b₄,b₅ are_c=-comparable holds
(b₁ with-replacement b₄,b₂) with-replacement b₅,b₃ = (b₁ with-replacement b₅,b₃) with-replacement b₄,b₂

proof end;

definition

let c₁ be Tree;
attr a₁ is finite-order means :: TREES_2:def 2
ex b₁ being Nat st
for b₂ being Element of a₁ holds not b₂ ^ <*b₁*> in a₁;

end;

:: deftheorem Def2 defines finite-order TREES_2:def 2 :

registration

cluster finite-order set ;
existence

proof end;

end;

definition

let c₁ be Tree;
mode Chain of c₁ -> Subset of a₁ means :Def3: :: TREES_2:def 3
for b₁, b₂ being FinSequence of NAT st b₁ in a₂ & b₂ in a₂ holds
b₁,b₂ are_c=-comparable ;
existence

proof end;

mode Level of c₁ -> Subset of a₁ means :Def4: :: TREES_2:def 4
ex b₁ being Nat st a₂ = { b₂ where B is Element of a₁ : len b₂ = b₁ } ;
existence

proof end;

let c₂ be Element of c₁;
func succ c₂ -> Subset of a₁ equals :: TREES_2:def 5
{ (a₂ ^ <*b₁*>) where B is Nat : a₂ ^ <*b₁*> in a₁ } ;
coherence

proof end;

end;

:: deftheorem Def3 defines Chain TREES_2:def 3 :

:: deftheorem Def4 defines Level TREES_2:def 4 :

:: deftheorem Def5 defines succ TREES_2:def 5 :

theorem Th11: :: TREES_2:11

for b₁ being Tree
for b₂ being Level of b₁ holds b₂ is AntiChain_of_Prefixes of b₁

proof end;

theorem Th12: :: TREES_2:12

for b₁ being Tree
for b₂ being Element of b₁ holds succ b₂ is AntiChain_of_Prefixes of b₁

proof end;

theorem Th13: :: TREES_2:13

for b₁ being Tree
for b₂ being AntiChain_of_Prefixes of b₁
for b₃ being Chain of b₁ ex b₄ being Element of b₁ st b₂ /\ b₃ c= {b₄}

proof end;

definition

let c₁ be Tree;
let c₂ be Nat;
func c₁ -level c₂ -> Level of a₁ equals :: TREES_2:def 6
{ b₁ where B is Element of a₁ : len b₁ = a₂ } ;
coherence

proof end;

end;

:: deftheorem Def6 defines -level TREES_2:def 6 :

theorem Th14: :: TREES_2:14

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

theorem Th15: :: TREES_2:15

for b₁ being Tree
for b₂ being Element of b₁ st b₂ = {} holds
b₁ -level 1 = succ b₂

proof end;

theorem Th16: :: TREES_2:16

for b₁ being Tree holds b₁ = union { (b₁ -level b₂) where B is Nat : verum }

proof end;

theorem Th17: :: TREES_2:17

for b₁ being finite Tree holds b₁ = union { (b₁ -level b₂) where B is Nat : b₂ <= height b₁ }

proof end;

theorem Th18: :: TREES_2:18

for b₁ being Tree
for b₂ being Level of b₁ ex b₃ being Nat st b₂ = b₁ -level b₃

proof end;

scheme :: TREES_2:sch 2
s2{ F₁() -> non empty set , F₂() -> set , F₃( set ) -> set } :

Card { F₃(b₁) where B is Element of F₁() : b₁ in F₂() } <=` Card F₂()

proof end;

scheme :: TREES_2:sch 3
s3{ F₁() -> non empty set , F₂() -> finite set , F₃() -> finite set , F₄( set ) -> set } :

card F₃() <= card F₂()

provided

E10: F₃() = { F₄(b₁) where B is Element of F₁() : b₁ in F₂() }

proof end;

theorem Th19: :: TREES_2:19

for b₁ being Tree st b₁ is finite-order holds
ex b₂ being Nat st
for b₃ being Element of b₁ ex b₄ being finite set st
( b₄ = succ b₃ & card b₄ <= b₂ )

proof end;

theorem Th20: :: TREES_2:20

for b₁ being Tree
for b₂ being Element of b₁ st b₁ is finite-order holds
succ b₂ is finite

proof end;

registration

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

end;

theorem Th21: :: TREES_2:21

for b₁ being Tree holds {} is Chain of b₁

proof end;

theorem Th22: :: TREES_2:22

for b₁ being Tree holds {{} } is Chain of b₁

proof end;

registration

let c₁ be Tree;
cluster non empty Chain of a₁;
existence

proof end;

end;

definition

let c₁ be Tree;
let c₂ be Chain of c₁;
attr a₂ is Branch-like means :Def7: :: TREES_2:def 7
( ( for b₁ being FinSequence of NAT st b₁ in a₂ holds
ProperPrefixes b₁ c= a₂ ) & ( for b₁ being FinSequence of NAT holds
( not b₁ in a₁ or ex b₂ being FinSequence of NAT st
( b₂ in a₂ & not b₂ is_a_proper_prefix_of b₁ ) ) ) );

end;

:: deftheorem Def7 defines Branch-like TREES_2:def 7 :

registration

let c₁ be Tree;
cluster Branch-like Chain of a₁;
existence

proof end;

end;

definition

let c₁ be Tree;
mode Branch of a₁ is Branch-like Chain of a₁;

end;

registration

let c₁ be Tree;
cluster Branch-like -> non empty Chain of a₁;
coherence

proof end;

end;

theorem Th23: :: TREES_2:23

for b₁ being Tree
for b₂, b₃ being FinSequence
for b₄ being Chain of b₁ st b₂ in b₄ & b₃ in b₄ & not b₂ in ProperPrefixes b₃ holds
b₃ is_a_prefix_of b₂

proof end;

theorem Th24: :: TREES_2:24

for b₁ being Tree
for b₂, b₃, b₄ being FinSequence
for b₅ being Chain of b₁ st b₂ in b₅ & b₃ in b₅ & b₄ is_a_prefix_of b₃ & not b₂ in ProperPrefixes b₄ holds
b₄ is_a_prefix_of b₂

proof end;

registration

let c₁ be Tree;
cluster finite Chain of a₁;
existence

proof end;

end;

theorem Th25: :: TREES_2:25

for b₁ being Tree
for b₂ being Nat
for b₃ being finite Chain of b₁ st card b₃ > b₂ holds
ex b₄ being FinSequence of NAT st
( b₄ in b₃ & len b₄ >= b₂ )

proof end;

theorem Th26: :: TREES_2:26

for b₁ being Tree
for b₂ being Chain of b₁ holds { b₃ where B is Element of b₁ : ex b₁ being FinSequence of NAT st
( b₄ in b₂ & b₃ is_a_prefix_of b₄ ) } is Chain of b₁

proof end;

theorem Th27: :: TREES_2:27

for b₁ being Tree
for b₂, b₃ being FinSequence of NAT
for b₄ being Branch of b₁ st b₂ is_a_prefix_of b₃ & b₃ in b₄ holds
b₂ in b₄

proof end;

theorem Th28: :: TREES_2:28

for b₁ being Tree
for b₂ being Branch of b₁ holds {} in b₂

proof end;

theorem Th29: :: TREES_2:29

for b₁ being Tree
for b₂, b₃ being FinSequence of NAT
for b₄ being Chain of b₁ st b₂ in b₄ & b₃ in b₄ & len b₂ <= len b₃ holds
b₂ is_a_prefix_of b₃

proof end;

theorem Th30: :: TREES_2:30

for b₁ being Tree
for b₂ being Chain of b₁ ex b₃ being Branch of b₁ st b₂ c= b₃

proof end;

scheme :: TREES_2:sch 4
s4{ P₁[ set , Nat], F₁() -> set } :

ex b₁ being Function st
( dom b₁ = F₁() & ( for b₂ being set st b₂ in F₁() holds
ex b₃ being Nat st
( b₁ . b₂ = b₃ & P₁[b₂,b₃] & ( for b₄ being Nat st P₁[b₂,b₄] holds
b₃ <= b₄ ) ) ) )

provided

E23: for b₁ being set st b₁ in F₁() holds
ex b₂ being Nat st P₁[b₁,b₂]

proof end;

Lemma23: for b₁ being set st b₁ is finite holds
ex b₂ being Nat st
for b₃ being Nat st b₃ in b₁ holds
b₃ <= b₂

proof end;

scheme :: TREES_2:sch 5
s5{ F₁() -> set , F₂() -> set , P₁[ set ], P₂[ set , set ] } :

ex b₁ being Function st
( dom b₁ = NAT & rng b₁ c= F₁() & b₁ . 0 = F₂() & ( for b₂ being Nat holds
( P₂[b₁ . b₂,b₁ . (b₂ + 1)] & P₁[b₁ . b₂] ) ) )

provided

E24: ( F₂() in F₁() & P₁[F₂()] ) and
E25: for b₁ being set st b₁ in F₁() & P₁[b₁] holds
ex b₂ being set st
( b₂ in F₁() & P₂[b₁,b₂] & P₁[b₂] )

proof end;

theorem Th31: :: TREES_2:31

for b₁ being Tree st ( for b₂ being Nat ex b₃ being finite Chain of b₁ st card b₃ = b₂ ) & ( for b₂ being Element of b₁ holds succ b₂ is finite ) holds
ex b₂ being Chain of b₁ st not b₂ is finite

proof end;

theorem Th32: :: TREES_2:32

for b₁ being finite-order Tree st ( for b₂ being Nat ex b₃ being finite Chain of b₁ st card b₃ = b₂ ) holds
ex b₂ being Chain of b₁ st not b₂ is finite

proof end;

definition

let c₁ be Relation;
attr a₁ is DecoratedTree-like means :Def8: :: TREES_2:def 8
dom a₁ is Tree;

end;

:: deftheorem Def8 defines DecoratedTree-like TREES_2:def 8 :

registration

cluster DecoratedTree-like set ;
existence

proof end;

end;

definition

mode DecoratedTree is DecoratedTree-like Function;

end;

registration

let c₁ be DecoratedTree;
cluster dom a₁ -> non empty Tree-like ;
coherence by Def8;

end;

definition

let c₁ be set ;
mode ParametrizedSubset of c₁ -> Relation means :Def9: :: TREES_2:def 9
rng a₂ c= a₁;
existence

proof end;

end;

:: deftheorem Def9 defines ParametrizedSubset TREES_2:def 9 :

registration

let c₁ be non empty set ;
cluster Function-like DecoratedTree-like ParametrizedSubset of a₁;
existence

proof end;

end;

definition

let c₁ be non empty set ;
mode DecoratedTree of a₁ is Function-like DecoratedTree-like ParametrizedSubset of a₁;

end;

definition

let c₁ be non empty set ;
let c₂ be DecoratedTree of c₁;
let c₃ be Element of dom c₂;
redefine func . as c₂ . c₃ -> Element of a₁;
coherence

proof end;

end;

theorem Th33: :: TREES_2:33

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

proof end;

scheme :: TREES_2:sch 6
s6{ F₁() -> Tree, P₁[ set , set ] } :

ex b₁ being DecoratedTree st
( dom b₁ = F₁() & ( for b₂ being FinSequence of NAT st b₂ in F₁() holds
P₁[b₂,b₁ . b₂] ) )

provided

E28: for b₁ being FinSequence of NAT st b₁ in F₁() holds
ex b₂ being set st P₁[b₁,b₂]

proof end;

scheme :: TREES_2:sch 7
s7{ F₁() -> Tree, F₂( set ) -> set } :

ex b₁ being DecoratedTree st
( dom b₁ = F₁() & ( for b₂ being FinSequence of NAT st b₂ in F₁() holds
b₁ . b₂ = F₂(b₂) ) )

proof end;

definition

let c₁ be DecoratedTree;
func Leaves c₁ -> set equals :: TREES_2:def 10
a₁ .: (Leaves (dom a₁));
correctness ;
let c₂ be FinSequence of NAT ;
func c₁ | c₂ -> DecoratedTree means :Def11: :: TREES_2:def 11
( dom a₃ = (dom a₁) | a₂ & ( for b₁ being FinSequence of NAT st b₁ in (dom a₁) | a₂ holds
a₃ . b₁ = a₁ . (a₂ ^ b₁) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def10 defines Leaves TREES_2:def 10 :

:: deftheorem Def11 defines | TREES_2:def 11 :

theorem Th34: :: TREES_2:34

for b₁ being FinSequence of NAT
for b₂ being DecoratedTree st b₁ in dom b₂ holds
rng (b₂ | b₁) c= rng b₂

proof end;

definition

let c₁ be non empty set ;
let c₂ be DecoratedTree of c₁;
redefine func Leaves as Leaves c₂ -> Subset of a₁;
coherence

proof end;

let c₃ be Element of dom c₂;
redefine func | as c₂ | c₃ -> DecoratedTree of a₁;
coherence

proof end;

end;

definition

let c₁ be DecoratedTree;
let c₂ be FinSequence of NAT ;
let c₃ be DecoratedTree;
assume E30: c₂ in dom c₁ ;
func c₁ with-replacement c₂,c₃ -> DecoratedTree means :: TREES_2:def 12
( dom a₄ = (dom a₁) with-replacement a₂,(dom a₃) & ( for b₁ being FinSequence of NAT holds
( not b₁ in (dom a₁) with-replacement a₂,(dom a₃) or ( not a₂ is_a_prefix_of b₁ & a₄ . b₁ = a₁ . b₁ ) or ex b₂ being FinSequence of NAT st
( b₂ in dom a₃ & b₁ = a₂ ^ b₂ & a₄ . b₁ = a₃ . b₂ ) ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def12 defines with-replacement TREES_2:def 12 :

registration

let c₁ be Tree;
let c₂ be set ;
cluster a₁ --> a₂ -> DecoratedTree-like ;
coherence

proof end;

end;

definition

let c₁ be non empty set ;
let c₂ be Tree;
let c₃ be Element of c₁;
redefine func --> as c₂ --> c₃ -> DecoratedTree of a₁;
coherence

proof end;

end;

theorem Th35: :: TREES_2:35

for b₁ being non empty set st ( for b₂ being set st b₂ in b₁ holds
b₂ is Tree ) holds
union b₁ is Tree

proof end;

theorem Th36: :: TREES_2:36

for b₁ being set st ( for b₂ being set st b₂ in b₁ holds
b₂ is Function ) & b₁ is c=-linear holds
( union b₁ is Relation-like & union b₁ is Function-like )

proof end;

theorem Th37: :: TREES_2:37

for b₁ being non empty set st ( for b₂ being set st b₂ in b₁ holds
b₂ is DecoratedTree ) & b₁ is c=-linear holds
union b₁ is DecoratedTree

proof end;

theorem Th38: :: TREES_2:38

for b₁, b₂ being non empty set st ( for b₃ being set st b₃ in b₁ holds
b₃ is DecoratedTree of b₂ ) & b₁ is c=-linear holds
union b₁ is DecoratedTree of b₂

proof end;

scheme :: TREES_2:sch 8
s8{ F₁() -> non empty set , F₂() -> Element of F₁(), F₃( set ) -> set , F₄() -> Function of [:F₁(),NAT :],F₁() } :

ex b₁ being DecoratedTree of F₁() st
( b₁ . {} = F₂() & ( for b₂ being Element of dom b₁ holds
( succ b₂ = { (b₂ ^ <*b₃*>) where B is Nat : b₃ in F₃((b₁ . b₂)) } & ( for b₃ being Nat st b₃ in F₃((b₁ . b₂)) holds
b₁ . (b₂ ^ <*b₃*>) = F₄() . [(b₁ . b₂),b₃] ) ) ) )

provided

E34: for b₁ being Element of F₁()
for b₂, b₃ being Nat st b₂ <= b₃ & b₃ in F₃(b₁) holds
b₂ in F₃(b₁)

proof end;

scheme :: TREES_2:sch 9
s9{ F₁() -> non empty set , F₂() -> Element of F₁(), F₃( set ) -> Nat, F₄() -> Function of [:F₁(),NAT :],F₁() } :

ex b₁ being DecoratedTree of F₁() st
( b₁ . {} = F₂() & ( for b₂ being Element of dom b₁ holds
( succ b₂ = { (b₂ ^ <*b₃*>) where B is Nat : b₃ < F₃((b₁ . b₂)) } & ( for b₃ being Nat st b₃ < F₃((b₁ . b₂)) holds
b₁ . (b₂ ^ <*b₃*>) = F₄() . [(b₁ . b₂),b₃] ) ) ) )

proof end;

registration

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

end;

definition

let c₁ be finite Tree;
let c₂ be Element of c₁;
func branchdeg c₂ -> set equals :: TREES_2:def 13
card (succ a₂);
correctness ;

end;

:: deftheorem Def13 defines branchdeg TREES_2:def 13 :

Lemma34: for b₁ being Function holds (pr1 (dom b₁),(rng b₁)) .: b₁ = dom b₁

proof end;

Lemma35: for b₁ being Function holds
( dom b₁ is finite iff b₁ is finite )

proof end;

registration

cluster finite set ;
existence

proof end;

end;

registration

let c₁ be non empty set ;
cluster finite ParametrizedSubset of a₁;
existence

proof end;

end;

registration

let c₁ be finite Relation;
cluster dom a₁ -> finite ;
coherence

proof end;

end;

registration

let c₁, c₂ be non empty set ;
cluster non empty Relation of a₁,a₂;
existence

proof end;

end;