:: TREES_3 semantic presentation

Lemma1: for b₁ being Nat
for b₂, b₃ being FinSequence st 1 <= b₁ & b₁ <= len b₂ holds
(b₂ ^ b₃) . b₁ = b₂ . b₁

proof end;

definition

func Trees -> set means :Def1: :: TREES_3:def 1
for b₁ being set holds
( b₁ in a₁ iff b₁ is Tree );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines Trees TREES_3:def 1 :

registration

cluster Trees -> non empty ;
coherence

proof end;

end;

definition

func FinTrees -> Subset of Trees means :Def2: :: TREES_3:def 2
for b₁ being set holds
( b₁ in a₁ iff b₁ is finite Tree );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines FinTrees TREES_3:def 2 :

registration

cluster FinTrees -> non empty ;
coherence

proof end;

end;

definition

let c₁ be set ;
attr a₁ is constituted-Trees means :Def3: :: TREES_3:def 3
for b₁ being set st b₁ in a₁ holds
b₁ is Tree;
attr a₁ is constituted-FinTrees means :Def4: :: TREES_3:def 4
for b₁ being set st b₁ in a₁ holds
b₁ is finite Tree;
attr a₁ is constituted-DTrees means :Def5: :: TREES_3:def 5
for b₁ being set st b₁ in a₁ holds
b₁ is DecoratedTree;

end;

:: deftheorem Def3 defines constituted-Trees TREES_3:def 3 :

:: deftheorem Def4 defines constituted-FinTrees TREES_3:def 4 :

:: deftheorem Def5 defines constituted-DTrees TREES_3:def 5 :

theorem Th1: :: TREES_3:1

for b₁ being set holds
( b₁ is constituted-Trees iff b₁ c= Trees )

proof end;

theorem Th2: :: TREES_3:2

for b₁ being set holds
( b₁ is constituted-FinTrees iff b₁ c= FinTrees )

proof end;

theorem Th3: :: TREES_3:3

for b₁, b₂ being set holds
( ( b₁ is constituted-Trees & b₂ is constituted-Trees ) iff b₁ \/ b₂ is constituted-Trees )

proof end;

theorem Th4: :: TREES_3:4

for b₁, b₂ being set st b₁ is constituted-Trees & b₂ is constituted-Trees holds
b₁ \+\ b₂ is constituted-Trees

proof end;

theorem Th5: :: TREES_3:5

for b₁, b₂ being set st b₁ is constituted-Trees holds
( b₁ /\ b₂ is constituted-Trees & b₂ /\ b₁ is constituted-Trees & b₁ \ b₂ is constituted-Trees )

proof end;

theorem Th6: :: TREES_3:6

for b₁, b₂ being set holds
( ( b₁ is constituted-FinTrees & b₂ is constituted-FinTrees ) iff b₁ \/ b₂ is constituted-FinTrees )

proof end;

theorem Th7: :: TREES_3:7

for b₁, b₂ being set st b₁ is constituted-FinTrees & b₂ is constituted-FinTrees holds
b₁ \+\ b₂ is constituted-FinTrees

proof end;

theorem Th8: :: TREES_3:8

for b₁, b₂ being set st b₁ is constituted-FinTrees holds
( b₁ /\ b₂ is constituted-FinTrees & b₂ /\ b₁ is constituted-FinTrees & b₁ \ b₂ is constituted-FinTrees )

proof end;

theorem Th9: :: TREES_3:9

for b₁, b₂ being set holds
( ( b₁ is constituted-DTrees & b₂ is constituted-DTrees ) iff b₁ \/ b₂ is constituted-DTrees )

proof end;

theorem Th10: :: TREES_3:10

for b₁, b₂ being set st b₁ is constituted-DTrees & b₂ is constituted-DTrees holds
b₁ \+\ b₂ is constituted-DTrees

proof end;

theorem Th11: :: TREES_3:11

for b₁, b₂ being set st b₁ is constituted-DTrees holds
( b₁ /\ b₂ is constituted-DTrees & b₂ /\ b₁ is constituted-DTrees & b₁ \ b₂ is constituted-DTrees )

proof end;

theorem Th12: :: TREES_3:12

( {} is constituted-Trees & {} is constituted-FinTrees & {} is constituted-DTrees )

proof end;

theorem Th13: :: TREES_3:13

for b₁ being set holds
( {b₁} is constituted-Trees iff b₁ is Tree )

proof end;

theorem Th14: :: TREES_3:14

for b₁ being set holds
( {b₁} is constituted-FinTrees iff b₁ is finite Tree )

proof end;

theorem Th15: :: TREES_3:15

for b₁ being set holds
( {b₁} is constituted-DTrees iff b₁ is DecoratedTree )

proof end;

theorem Th16: :: TREES_3:16

for b₁, b₂ being set holds
( {b₁,b₂} is constituted-Trees iff ( b₁ is Tree & b₂ is Tree ) )

proof end;

theorem Th17: :: TREES_3:17

for b₁, b₂ being set holds
( {b₁,b₂} is constituted-FinTrees iff ( b₁ is finite Tree & b₂ is finite Tree ) )

proof end;

theorem Th18: :: TREES_3:18

for b₁, b₂ being set holds
( {b₁,b₂} is constituted-DTrees iff ( b₁ is DecoratedTree & b₂ is DecoratedTree ) )

proof end;

theorem Th19: :: TREES_3:19

for b₁, b₂ being set st b₁ is constituted-Trees & b₂ c= b₁ holds
b₂ is constituted-Trees

proof end;

theorem Th20: :: TREES_3:20

for b₁, b₂ being set st b₁ is constituted-FinTrees & b₂ c= b₁ holds
b₂ is constituted-FinTrees

proof end;

theorem Th21: :: TREES_3:21

for b₁, b₂ being set st b₁ is constituted-DTrees & b₂ c= b₁ holds
b₂ is constituted-DTrees

proof end;

registration

cluster non empty finite constituted-Trees constituted-FinTrees set ;
existence

proof end;

cluster non empty finite constituted-DTrees set ;
existence

proof end;

end;

registration

cluster constituted-FinTrees -> constituted-Trees set ;
coherence

proof end;

end;

registration

let c₁ be constituted-Trees set ;
cluster -> constituted-Trees Element of bool a₁;
coherence

proof end;

end;

registration

let c₁ be constituted-FinTrees set ;
cluster -> constituted-Trees constituted-FinTrees Element of bool a₁;
coherence

proof end;

end;

registration

let c₁ be constituted-DTrees set ;
cluster -> constituted-DTrees Element of bool a₁;
coherence

proof end;

end;

definition

let c₁ be non empty constituted-Trees set ;
redefine mode Element as Element of c₁ -> Tree;
coherence by Def3;

end;

definition

let c₁ be non empty constituted-FinTrees set ;
redefine mode Element as Element of c₁ -> finite Tree;
coherence by Def4;

end;

definition

let c₁ be non empty constituted-DTrees set ;
redefine mode Element as Element of c₁ -> DecoratedTree;
coherence by Def5;

end;

registration

cluster Trees -> non empty constituted-Trees ;
coherence

proof end;

end;

registration

cluster non empty constituted-Trees constituted-FinTrees Element of bool Trees ;
existence

proof end;

end;

registration

cluster FinTrees -> non empty constituted-Trees constituted-FinTrees ;
coherence

proof end;

end;

definition

let c₁ be non empty set ;
mode DTree-set of c₁ -> set means :Def6: :: TREES_3:def 6
for b₁ being set st b₁ in a₂ holds
b₁ is DecoratedTree of a₁;
existence

proof end;

end;

:: deftheorem Def6 defines DTree-set TREES_3:def 6 :

registration

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

proof end;

end;

registration

let c₁ be non empty set ;
cluster non empty finite constituted-DTrees DTree-set of a₁;
existence

proof end;

end;

definition

let c₁ be non empty set ;
let c₂ be non empty DTree-set of c₁;
redefine mode Element as Element of c₂ -> DecoratedTree of a₁;
coherence by Def6;

end;

definition

let c₁ be Tree;
let c₂ be non empty set ;
redefine func Funcs as Funcs c₁,c₂ -> non empty DTree-set of a₂;
coherence

proof end;

redefine mode Relation as Relation of c₁,c₂ -> ParametrizedSubset of a₂;
coherence

proof end;

end;

registration

let c₁ be Tree;
let c₂ be non empty set ;
cluster -> DecoratedTree-like Relation of a₁,a₂;
coherence

proof end;

end;

definition

let c₁ be non empty set ;
func Trees c₁ -> DTree-set of a₁ means :Def7: :: TREES_3:def 7
for b₁ being DecoratedTree of a₁ holds b₁ in a₂;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines Trees TREES_3:def 7 :

registration

let c₁ be non empty set ;
cluster Trees a₁ -> non empty constituted-DTrees ;
coherence by Def7;

end;

definition

let c₁ be non empty set ;
func FinTrees c₁ -> DTree-set of a₁ means :Def8: :: TREES_3:def 8
for b₁ being DecoratedTree of a₁ holds
( dom b₁ is finite iff b₁ in a₂ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines FinTrees TREES_3:def 8 :

registration

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

proof end;

end;

theorem Th22: :: TREES_3:22

for b₁ being non empty set holds FinTrees b₁ c= Trees b₁

proof end;

definition

let c₁ be Function;
attr a₁ is Tree-yielding means :Def9: :: TREES_3:def 9
rng a₁ is constituted-Trees;
attr a₁ is FinTree-yielding means :Def10: :: TREES_3:def 10
rng a₁ is constituted-FinTrees;
attr a₁ is DTree-yielding means :Def11: :: TREES_3:def 11
rng a₁ is constituted-DTrees;

end;

:: deftheorem Def9 defines Tree-yielding TREES_3:def 9 :

:: deftheorem Def10 defines FinTree-yielding TREES_3:def 10 :

:: deftheorem Def11 defines DTree-yielding TREES_3:def 11 :

theorem Th23: :: TREES_3:23

( {} is Tree-yielding & {} is FinTree-yielding & {} is DTree-yielding )

proof end;

theorem Th24: :: TREES_3:24

for b₁ being Function holds
( b₁ is Tree-yielding iff for b₂ being set st b₂ in dom b₁ holds
b₁ . b₂ is Tree )

proof end;

theorem Th25: :: TREES_3:25

for b₁ being Function holds
( b₁ is FinTree-yielding iff for b₂ being set st b₂ in dom b₁ holds
b₁ . b₂ is finite Tree )

proof end;

theorem Th26: :: TREES_3:26

for b₁ being Function holds
( b₁ is DTree-yielding iff for b₂ being set st b₂ in dom b₁ holds
b₁ . b₂ is DecoratedTree )

proof end;

theorem Th27: :: TREES_3:27

for b₁, b₂ being FinSequence holds
( ( b₁ is Tree-yielding & b₂ is Tree-yielding ) iff b₁ ^ b₂ is Tree-yielding )

proof end;

theorem Th28: :: TREES_3:28

for b₁, b₂ being FinSequence holds
( ( b₁ is FinTree-yielding & b₂ is FinTree-yielding ) iff b₁ ^ b₂ is FinTree-yielding )

proof end;

theorem Th29: :: TREES_3:29

for b₁, b₂ being FinSequence holds
( ( b₁ is DTree-yielding & b₂ is DTree-yielding ) iff b₁ ^ b₂ is DTree-yielding )

proof end;

theorem Th30: :: TREES_3:30

for b₁ being set holds
( <*b₁*> is Tree-yielding iff b₁ is Tree )

proof end;

theorem Th31: :: TREES_3:31

for b₁ being set holds
( <*b₁*> is FinTree-yielding iff b₁ is finite Tree )

proof end;

theorem Th32: :: TREES_3:32

for b₁ being set holds
( <*b₁*> is DTree-yielding iff b₁ is DecoratedTree )

proof end;

theorem Th33: :: TREES_3:33

for b₁, b₂ being set holds
( <*b₁,b₂*> is Tree-yielding iff ( b₁ is Tree & b₂ is Tree ) )

proof end;

theorem Th34: :: TREES_3:34

for b₁, b₂ being set holds
( <*b₁,b₂*> is FinTree-yielding iff ( b₁ is finite Tree & b₂ is finite Tree ) )

proof end;

theorem Th35: :: TREES_3:35

for b₁, b₂ being set holds
( <*b₁,b₂*> is DTree-yielding iff ( b₁ is DecoratedTree & b₂ is DecoratedTree ) )

proof end;

theorem Th36: :: TREES_3:36

for b₁ being set
for b₂ being Nat st b₂ <> 0 holds
( b₂ |-> b₁ is Tree-yielding iff b₁ is Tree )

proof end;

theorem Th37: :: TREES_3:37

for b₁ being set
for b₂ being Nat st b₂ <> 0 holds
( b₂ |-> b₁ is FinTree-yielding iff b₁ is finite Tree )

proof end;

theorem Th38: :: TREES_3:38

for b₁ being set
for b₂ being Nat st b₂ <> 0 holds
( b₂ |-> b₁ is DTree-yielding iff b₁ is DecoratedTree )

proof end;

registration

cluster non empty Tree-yielding FinTree-yielding set ;
existence

proof end;

cluster non empty DTree-yielding set ;
existence

proof end;

end;

registration

cluster non empty Tree-yielding FinTree-yielding set ;
existence

proof end;

cluster non empty DTree-yielding set ;
existence

proof end;

end;

registration

cluster FinTree-yielding -> Tree-yielding set ;
coherence

proof end;

end;

registration

let c₁ be non empty constituted-Trees set ;
cluster -> Tree-yielding FinSequence of a₁;
coherence

proof end;

end;

registration

let c₁, c₂ be Tree-yielding FinSequence;
cluster a₁ ^ a₂ -> Tree-yielding ;
coherence by Th27;

end;

registration

let c₁ be non empty constituted-FinTrees set ;
cluster -> Tree-yielding FinTree-yielding FinSequence of a₁;
coherence

proof end;

end;

registration

let c₁, c₂ be FinTree-yielding FinSequence;
cluster a₁ ^ a₂ -> Tree-yielding FinTree-yielding ;
coherence by Th28;

end;

registration

let c₁ be non empty constituted-DTrees set ;
cluster -> DTree-yielding FinSequence of a₁;
coherence

proof end;

end;

registration

let c₁, c₂ be DTree-yielding FinSequence;
cluster a₁ ^ a₂ -> DTree-yielding ;
coherence by Th29;

end;

Lemma38: for b₁, b₂ being set holds
( not <*b₁*> is empty & not <*b₁,b₂*> is empty )

proof end;

registration

let c₁ be Tree;
cluster <*a₁*> -> non empty Tree-yielding ;
coherence by Th30;
let c₂ be Tree;
cluster <*a₁,a₂*> -> non empty Tree-yielding ;
coherence by Lemma38, Th33;

end;

registration

let c₁ be Nat;
let c₂ be Tree;
cluster a₁ |-> a₂ -> Tree-yielding ;
coherence

proof end;

end;

registration

let c₁ be finite Tree;
cluster <*a₁*> -> Tree-yielding FinTree-yielding ;
coherence by Th31;
let c₂ be finite Tree;
cluster <*a₁,a₂*> -> non empty Tree-yielding FinTree-yielding ;
coherence by Th34;

end;

registration

let c₁ be Nat;
let c₂ be finite Tree;
cluster a₁ |-> a₂ -> Tree-yielding FinTree-yielding ;
coherence

proof end;

end;

registration

let c₁ be DecoratedTree;
cluster <*a₁*> -> non empty DTree-yielding ;
coherence by Th32;
let c₂ be DecoratedTree;
cluster <*a₁,a₂*> -> non empty DTree-yielding ;
coherence by Lemma38, Th35;

end;

registration

let c₁ be Nat;
let c₂ be DecoratedTree;
cluster a₁ |-> a₂ -> DTree-yielding ;
coherence

proof end;

end;

theorem Th39: :: TREES_3:39

for b₁ being DTree-yielding Function holds
( dom (doms b₁) = dom b₁ & doms b₁ is Tree-yielding )

proof end;

registration

let c₁ be DTree-yielding FinSequence;
cluster doms a₁ -> FinSequence-like Tree-yielding ;
coherence

proof end;

end;

theorem Th40: :: TREES_3:40

for b₁ being DTree-yielding FinSequence holds len (doms b₁) = len b₁

proof end;

Lemma40: for b₁ being non empty set
for b₂ being DecoratedTree of b₁ holds b₂ is Function of dom b₂,b₁

proof end;

definition

let c₁, c₂ be non empty set ;
mode DecoratedTree of a₁,a₂ is DecoratedTree of [:a₁,a₂:];
mode DTree-set of a₁,a₂ is DTree-set of [:a₁,a₂:];

end;

registration

let c₁, c₂ be DecoratedTree;
cluster <:a₁,a₂:> -> DecoratedTree-like ;
coherence

proof end;

end;

definition

let c₁, c₂ be non empty set ;
let c₃ be DecoratedTree of c₁;
let c₄ be DecoratedTree of c₂;
redefine func <: as <:c₃,c₄:> -> DecoratedTree of a₁,a₂;
coherence

proof end;

end;

definition

let c₁, c₂ be non empty set ;
let c₃ be DecoratedTree of c₁;
let c₄ be Function of c₁,c₂;
redefine func * as c₄ * c₃ -> DecoratedTree of a₂;
coherence

proof end;

end;

definition

let c₁, c₂ be non empty set ;
redefine func pr1 as pr1 c₁,c₂ -> Function of [:a₁,a₂:],a₁;
coherence

proof end;

redefine func pr2 as pr2 c₁,c₂ -> Function of [:a₁,a₂:],a₂;
coherence

proof end;

end;

definition

let c₁, c₂ be non empty set ;
let c₃ be DecoratedTree of c₁,c₂;
func c₃ `1 -> DecoratedTree of a₁ equals :: TREES_3:def 12
(pr1 a₁,a₂) * a₃;
correctness ;
func c₃ `2 -> DecoratedTree of a₂ equals :: TREES_3:def 13
(pr2 a₁,a₂) * a₃;
correctness ;

end;

:: deftheorem Def12 defines `1 TREES_3:def 12 :

:: deftheorem Def13 defines `2 TREES_3:def 13 :

theorem Th41: :: TREES_3:41

for b₁, b₂ being non empty set
for b₃ being DecoratedTree of b₁,b₂
for b₄ being Element of dom b₃ holds
( (b₃ . b₄) `1 = (b₃ `1 ) . b₄ & (b₃ `2 ) . b₄ = (b₃ . b₄) `2 )

proof end;

theorem Th42: :: TREES_3:42

for b₁, b₂ being non empty set
for b₃ being DecoratedTree of b₁,b₂ holds <:(b₃ `1 ),(b₃ `2 ):> = b₃

proof end;

registration

let c₁ be finite Tree;
cluster Leaves a₁ -> non empty finite ;
coherence

proof end;

end;

definition

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

proof end;

end;

definition

let c₁ be finite Tree;
redefine mode Leaf as Leaf of c₁ -> Element of Leaves a₁;
coherence by TREES_1:def 10;

end;

definition

let c₁ be finite Tree;
mode T-Substitution of c₁ -> Tree means :Def14: :: TREES_3:def 14
for b₁ being Element of a₂ holds
( b₁ in a₁ or ex b₂ being Leaf of a₁ st b₂ is_a_proper_prefix_of b₁ );
existence

proof end;

end;

:: deftheorem Def14 defines T-Substitution TREES_3:def 14 :

definition

let c₁ be finite Tree;
let c₂ be Leaf of c₁;
let c₃ be Tree;
redefine func with-replacement as c₁ with-replacement c₂,c₃ -> T-Substitution of a₁;
coherence

proof end;

end;

registration

let c₁ be finite Tree;
cluster finite T-Substitution of a₁;
existence

proof end;

end;

definition

let c₁ be Nat;
mode T-Substitution of a₁ is T-Substitution of elementary_tree a₁;

end;

theorem Th43: :: TREES_3:43

for b₁ being Tree holds b₁ is T-Substitution of 0

proof end;

theorem Th44: :: TREES_3:44

for b₁, b₂ being Tree st b₁ -level 1 c= b₂ -level 1 & ( for b₃ being Nat st <*b₃*> in b₁ holds
b₁ | <*b₃*> = b₂ | <*b₃*> ) holds
b₁ c= b₂

proof end;

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

theorem Th45: :: TREES_3:45

canceled;

theorem Th46: :: TREES_3:46

for b₁, b₂ being Tree
for b₃ being FinSequence of NAT st b₃ in Leaves b₁ holds
b₁ c= b₁ with-replacement b₃,b₂

proof end;

theorem Th47: :: TREES_3:47

for b₁, b₂ being DecoratedTree
for b₃ being Element of dom b₁ holds (b₁ with-replacement b₃,b₂) . b₃ = b₂ . {}

proof end;

theorem Th48: :: TREES_3:48

for b₁, b₂ being DecoratedTree
for b₃, b₄ being Element of dom b₁ st not b₃ is_a_prefix_of b₄ holds
(b₁ with-replacement b₃,b₂) . b₄ = b₁ . b₄

proof end;

theorem Th49: :: TREES_3:49

for b₁, b₂ being DecoratedTree
for b₃ being Element of dom b₁
for b₄ being Element of dom b₂ holds (b₁ with-replacement b₃,b₂) . (b₃ ^ b₄) = b₂ . b₄

proof end;

registration

let c₁, c₂ be Tree;
cluster a₁ \/ a₂ -> non empty Tree-like ;
coherence by TREES_1:49;

end;

theorem Th50: :: TREES_3:50

for b₁, b₂ being Tree
for b₃ being Element of b₁ \/ b₂ holds
( ( b₃ in b₁ & b₃ in b₂ implies (b₁ \/ b₂) | b₃ = (b₁ | b₃) \/ (b₂ | b₃) ) & ( not b₃ in b₁ implies (b₁ \/ b₂) | b₃ = b₂ | b₃ ) & ( not b₃ in b₂ implies (b₁ \/ b₂) | b₃ = b₁ | b₃ ) )

proof end;

definition

let c₁ be FinSequence;
assume E45: c₁ is Tree-yielding ;
func tree c₁ -> Tree means :Def15: :: TREES_3:def 15
for b₁ being set holds
( b₁ in a₂ iff ( b₁ = {} or ex b₂ being Natex b₃ being FinSequence st
( b₂ < len a₁ & b₃ in a₁ . (b₂ + 1) & b₁ = <*b₂*> ^ b₃ ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def15 defines tree TREES_3:def 15 :

definition

let c₁ be Tree;
func ^ c₁ -> Tree equals :: TREES_3:def 16
tree <*a₁*>;
correctness ;

end;

:: deftheorem Def16 defines ^ TREES_3:def 16 :

definition

let c₁, c₂ be Tree;
func tree c₁,c₂ -> Tree equals :: TREES_3:def 17
tree <*a₁,a₂*>;
correctness ;

end;

:: deftheorem Def17 defines tree TREES_3:def 17 :

theorem Th51: :: TREES_3:51

for b₁ being Nat
for b₂, b₃ being FinSequence st b₂ is Tree-yielding holds
( <*b₁*> ^ b₃ in tree b₂ iff ( b₁ < len b₂ & b₃ in b₂ . (b₁ + 1) ) )

proof end;

theorem Th52: :: TREES_3:52

for b₁ being FinSequence st b₁ is Tree-yielding holds
( (tree b₁) -level 1 = { <*b₂*> where B is Nat : b₂ < len b₁ } & ( for b₂ being Nat st b₂ < len b₁ holds
(tree b₁) | <*b₂*> = b₁ . (b₂ + 1) ) )

proof end;

theorem Th53: :: TREES_3:53

for b₁, b₂ being Tree-yielding FinSequence st tree b₁ = tree b₂ holds
b₁ = b₂

proof end;

theorem Th54: :: TREES_3:54

for b₁ being FinSequence
for b₂, b₃ being Tree-yielding FinSequence
for b₄ being Tree holds
( b₁ in b₄ iff <*(len b₂)*> ^ b₁ in tree ((b₂ ^ <*b₄*>) ^ b₃) )

proof end;

theorem Th55: :: TREES_3:55

tree {} = elementary_tree 0

proof end;

theorem Th56: :: TREES_3:56

for b₁ being FinSequence st b₁ is Tree-yielding holds
elementary_tree (len b₁) c= tree b₁

proof end;

theorem Th57: :: TREES_3:57

for b₁ being Nat holds elementary_tree b₁ = tree (b₁ |-> (elementary_tree 0))

proof end;

theorem Th58: :: TREES_3:58

for b₁ being Tree
for b₂ being Tree-yielding FinSequence holds tree (b₂ ^ <*b₁*>) = ((tree b₂) \/ (elementary_tree ((len b₂) + 1))) with-replacement <*(len b₂)*>,b₁

proof end;

theorem Th59: :: TREES_3:59

for b₁ being Tree-yielding FinSequence holds tree (b₁ ^ <*(elementary_tree 0)*>) = (tree b₁) \/ (elementary_tree ((len b₁) + 1))

proof end;

theorem Th60: :: TREES_3:60

for b₁, b₂ being Tree-yielding FinSequence
for b₃, b₄ being Tree holds tree ((b₁ ^ <*b₃*>) ^ b₂) = (tree ((b₁ ^ <*b₄*>) ^ b₂)) with-replacement <*(len b₁)*>,b₃

proof end;

theorem Th61: :: TREES_3:61

for b₁ being Tree holds ^ b₁ = (elementary_tree 1) with-replacement <*0*>,b₁

proof end;

theorem Th62: :: TREES_3:62

for b₁, b₂ being Tree holds tree b₁,b₂ = ((elementary_tree 2) with-replacement <*0*>,b₁) with-replacement <*1*>,b₂

proof end;

registration

let c₁ be FinTree-yielding FinSequence;
cluster tree a₁ -> finite ;
coherence

proof end;

end;

registration

let c₁ be finite Tree;
cluster ^ a₁ -> finite ;
coherence ;

end;

registration

let c₁, c₂ be finite Tree;
cluster tree a₁,a₂ -> finite ;
coherence ;

end;

theorem Th63: :: TREES_3:63

for b₁ being Tree
for b₂ being set holds
( b₂ in ^ b₁ iff ( b₂ = {} or ex b₃ being FinSequence st
( b₃ in b₁ & b₂ = <*0*> ^ b₃ ) ) )

proof end;

theorem Th64: :: TREES_3:64

for b₁ being Tree
for b₂ being FinSequence holds
( b₂ in b₁ iff <*0*> ^ b₂ in ^ b₁ )

proof end;

theorem Th65: :: TREES_3:65

for b₁ being Tree holds elementary_tree 1 c= ^ b₁

proof end;

theorem Th66: :: TREES_3:66

for b₁, b₂ being Tree st b₁ c= b₂ holds
^ b₁ c= ^ b₂

proof end;

theorem Th67: :: TREES_3:67

for b₁, b₂ being Tree st ^ b₁ = ^ b₂ holds
b₁ = b₂

proof end;

theorem Th68: :: TREES_3:68

for b₁ being Tree holds (^ b₁) | <*0*> = b₁

proof end;

theorem Th69: :: TREES_3:69

for b₁, b₂ being Tree holds (^ b₁) with-replacement <*0*>,b₂ = ^ b₂

proof end;

theorem Th70: :: TREES_3:70

^ (elementary_tree 0) = elementary_tree 1

proof end;

theorem Th71: :: TREES_3:71

for b₁, b₂ being Tree
for b₃ being set holds
( b₃ in tree b₁,b₂ iff ( b₃ = {} or ex b₄ being FinSequence st
( ( b₄ in b₁ & b₃ = <*0*> ^ b₄ ) or ( b₄ in b₂ & b₃ = <*1*> ^ b₄ ) ) ) )

proof end;

theorem Th72: :: TREES_3:72

for b₁, b₂ being Tree
for b₃ being FinSequence holds
( b₃ in b₁ iff <*0*> ^ b₃ in tree b₁,b₂ )

proof end;

theorem Th73: :: TREES_3:73

for b₁, b₂ being Tree
for b₃ being FinSequence holds
( b₃ in b₂ iff <*1*> ^ b₃ in tree b₁,b₂ )

proof end;

theorem Th74: :: TREES_3:74

for b₁, b₂ being Tree holds elementary_tree 2 c= tree b₁,b₂

proof end;

theorem Th75: :: TREES_3:75

for b₁, b₂, b₃, b₄ being Tree st b₁ c= b₃ & b₂ c= b₄ holds
tree b₁,b₂ c= tree b₃,b₄

proof end;

theorem Th76: :: TREES_3:76

for b₁, b₂, b₃, b₄ being Tree st tree b₁,b₂ = tree b₃,b₄ holds
( b₁ = b₃ & b₂ = b₄ )

proof end;

theorem Th77: :: TREES_3:77

for b₁, b₂ being Tree holds
( (tree b₁,b₂) | <*0*> = b₁ & (tree b₁,b₂) | <*1*> = b₂ )

proof end;

theorem Th78: :: TREES_3:78

for b₁, b₂, b₃ being Tree holds
( (tree b₂,b₃) with-replacement <*0*>,b₁ = tree b₁,b₃ & (tree b₂,b₃) with-replacement <*1*>,b₁ = tree b₂,b₁ )

proof end;

theorem Th79: :: TREES_3:79

tree (elementary_tree 0),(elementary_tree 0) = elementary_tree 2

proof end;

theorem Th80: :: TREES_3:80

for b₁ being Nat
for b₂ being FinTree-yielding FinSequence st ( for b₃ being finite Tree st b₃ in rng b₂ holds
height b₃ <= b₁ ) holds
height (tree b₂) <= b₁ + 1

proof end;

theorem Th81: :: TREES_3:81

for b₁ being FinTree-yielding FinSequence
for b₂ being finite Tree st b₂ in rng b₁ holds
height (tree b₁) > height b₂

proof end;

theorem Th82: :: TREES_3:82

for b₁ being FinTree-yielding FinSequence
for b₂ being finite Tree st b₂ in rng b₁ & ( for b₃ being finite Tree st b₃ in rng b₁ holds
height b₃ <= height b₂ ) holds
height (tree b₁) = (height b₂) + 1

proof end;

theorem Th83: :: TREES_3:83

for b₁ being finite Tree holds height (^ b₁) = (height b₁) + 1

proof end;

theorem Th84: :: TREES_3:84

for b₁, b₂ being finite Tree holds height (tree b₁,b₂) = (max (height b₁),(height b₂)) + 1

proof end;

registration

let c₁ be non empty set ;
let c₂ be Element of FinTrees c₁;
cluster dom a₂ -> finite ;
coherence by Def8;

end;

definition

let c₁ be FinSequence;
assume E61: c₁ is DTree-yielding ;
defpred S₁[ Nat, set ] means ex b₁ being DecoratedTree st
( b₁ = c₁ . a₁ & a₂ = b₁ . {} );
func roots c₁ -> FinSequence means :: TREES_3:def 18
( dom a₂ = dom a₁ & ( for b₁ being Nat st b₁ in dom a₁ holds
ex b₂ being DecoratedTree st
( b₂ = a₁ . b₁ & a₂ . b₁ = b₂ . {} ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def18 defines roots TREES_3:def 18 :