:: TREES_4 semantic presentation

definition

let c₁ be DecoratedTree;
mode Node of a₁ is Element of dom a₁;

end;

E1: now

let c₁, c₂ be set ;
let c₃ be FinSequence of c₁;
assume ( c₂ in dom c₃ or c₂ in dom c₃ ) ;
then ( c₃ . c₂ in rng c₃ & rng c₃ c= c₁ ) by FINSEQ_1:def 4, FUNCT_1:def 5;
hence c₃ . c₂ in c₁ ;

end;

definition

let c₁, c₂ be DecoratedTree;
redefine pred c₁ = c₂ means :: TREES_4:def 1
( dom a₁ = dom a₂ & ( for b₁ being Node of a₁ holds a₁ . b₁ = a₂ . b₁ ) );
compatibility

proof end;

end;

:: deftheorem Def1 defines = TREES_4:def 1 :

theorem Th1: :: TREES_4:1

for b₁, b₂ being Nat st elementary_tree b₁ c= elementary_tree b₂ holds
b₁ <= b₂

proof end;

theorem Th2: :: TREES_4:2

for b₁, b₂ being Nat st elementary_tree b₁ = elementary_tree b₂ holds
b₁ = b₂

proof end;

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

E5: now

let c₁ be Nat;
let c₂ be set ;
let c₃ be FinSequence of c₂;
assume c₁ < len c₃ ;
then ( c₃ . (c₁ + 1) in rng c₃ & rng c₃ c= c₂ ) by Lemma4, FINSEQ_1:def 4;
hence c₃ . (c₁ + 1) in c₂ ;

end;

definition

let c₁ be set ;
func root-tree c₁ -> DecoratedTree equals :: TREES_4:def 2
(elementary_tree 0) --> a₁;
correctness ;

end;

:: deftheorem Def2 defines root-tree TREES_4:def 2 :

definition

let c₁ be non empty set ;
let c₂ be Element of c₁;
redefine func root-tree as root-tree c₂ -> Element of FinTrees a₁;
coherence

proof end;

end;

theorem Th3: :: TREES_4:3

for b₁ being set holds
( dom (root-tree b₁) = elementary_tree 0 & (root-tree b₁) . {} = b₁ )

proof end;

theorem Th4: :: TREES_4:4

for b₁, b₂ being set st root-tree b₁ = root-tree b₂ holds
b₁ = b₂

proof end;

theorem Th5: :: TREES_4:5

for b₁ being DecoratedTree st dom b₁ = elementary_tree 0 holds
b₁ = root-tree (b₁ . {} )

proof end;

theorem Th6: :: TREES_4:6

for b₁ being set holds root-tree b₁ = {[{} ,b₁]}

proof end;

definition

let c₁ be set ;
let c₂ be FinSequence;
func c₁ -flat_tree c₂ -> DecoratedTree means :Def3: :: TREES_4:def 3
( dom a₃ = elementary_tree (len a₂) & a₃ . {} = a₁ & ( for b₁ being Nat st b₁ < len a₂ holds
a₃ . <*b₁*> = a₂ . (b₁ + 1) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines -flat_tree TREES_4:def 3 :

theorem Th7: :: TREES_4:7

for b₁, b₂ being set
for b₃, b₄ being FinSequence st b₁ -flat_tree b₃ = b₂ -flat_tree b₄ holds
( b₁ = b₂ & b₃ = b₄ )

proof end;

theorem Th8: :: TREES_4:8

for b₁, b₂ being Nat st b₁ < b₂ holds
(elementary_tree b₂) | <*b₁*> = elementary_tree 0

proof end;

theorem Th9: :: TREES_4:9

for b₁ being set
for b₂ being Nat
for b₃ being FinSequence st b₂ < len b₃ holds
(b₁ -flat_tree b₃) | <*b₂*> = root-tree (b₃ . (b₂ + 1))

proof end;

definition

let c₁ be set ;
let c₂ be FinSequence;
assume E11: c₂ is DTree-yielding ;
func c₁ -tree c₂ -> DecoratedTree means :Def4: :: TREES_4:def 4
( ex b₁ being DTree-yielding FinSequence st
( a₂ = b₁ & dom a₃ = tree (doms b₁) ) & a₃ . {} = a₁ & ( for b₁ being Nat st b₁ < len a₂ holds
a₃ | <*b₁*> = a₂ . (b₁ + 1) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines -tree TREES_4:def 4 :

definition

let c₁ be set ;
let c₂ be DecoratedTree;
func c₁ -tree c₂ -> DecoratedTree equals :: TREES_4:def 5
a₁ -tree <*a₂*>;
correctness ;

end;

:: deftheorem Def5 defines -tree TREES_4:def 5 :

definition

let c₁ be set ;
let c₂, c₃ be DecoratedTree;
func c₁ -tree c₂,c₃ -> DecoratedTree equals :: TREES_4:def 6
a₁ -tree <*a₂,a₃*>;
correctness ;

end;

:: deftheorem Def6 defines -tree TREES_4:def 6 :

theorem Th10: :: TREES_4:10

for b₁ being set
for b₂ being DTree-yielding FinSequence holds dom (b₁ -tree b₂) = tree (doms b₂)

proof end;

theorem Th11: :: TREES_4:11

for b₁, b₂ being set
for b₃ being DTree-yielding FinSequence holds
( b₁ in dom (b₂ -tree b₃) iff ( b₁ = {} or ex b₄ being Natex b₅ being DecoratedTreeex b₆ being Node of b₅ st
( b₄ < len b₃ & b₅ = b₃ . (b₄ + 1) & b₁ = <*b₄*> ^ b₆ ) ) )

proof end;

theorem Th12: :: TREES_4:12

for b₁ being set
for b₂ being DTree-yielding FinSequence
for b₃ being Nat
for b₄ being DecoratedTree
for b₅ being Node of b₄ st b₃ < len b₂ & b₄ = b₂ . (b₃ + 1) holds
(b₁ -tree b₂) . (<*b₃*> ^ b₅) = b₄ . b₅

proof end;

theorem Th13: :: TREES_4:13

for b₁ being set
for b₂ being DecoratedTree holds dom (b₁ -tree b₂) = ^ (dom b₂)

proof end;

theorem Th14: :: TREES_4:14

for b₁ being set
for b₂, b₃ being DecoratedTree holds dom (b₁ -tree b₂,b₃) = tree (dom b₂),(dom b₃)

proof end;

theorem Th15: :: TREES_4:15

for b₁, b₂ being set
for b₃, b₄ being DTree-yielding FinSequence st b₁ -tree b₃ = b₂ -tree b₄ holds
( b₁ = b₂ & b₃ = b₄ )

proof end;

theorem Th16: :: TREES_4:16

for b₁, b₂ being set
for b₃ being FinSequence st root-tree b₁ = b₂ -flat_tree b₃ holds
( b₁ = b₂ & b₃ = {} )

proof end;

theorem Th17: :: TREES_4:17

for b₁, b₂ being set
for b₃ being FinSequence st root-tree b₁ = b₂ -tree b₃ & b₃ is DTree-yielding holds
( b₁ = b₂ & b₃ = {} )

proof end;

theorem Th18: :: TREES_4:18

for b₁, b₂ being set
for b₃, b₄ being FinSequence st b₁ -flat_tree b₃ = b₂ -tree b₄ & b₄ is DTree-yielding holds
( b₁ = b₂ & len b₃ = len b₄ & ( for b₅ being Nat st b₅ in dom b₃ holds
b₄ . b₅ = root-tree (b₃ . b₅) ) )

proof end;

theorem Th19: :: TREES_4:19

for b₁ being set
for b₂ being DTree-yielding FinSequence
for b₃ being Nat
for b₄ being FinSequence st <*b₃*> ^ b₄ in dom (b₁ -tree b₂) holds
(b₁ -tree b₂) . (<*b₃*> ^ b₄) = b₂ .. (b₃ + 1),b₄

proof end;

theorem Th20: :: TREES_4:20

for b₁ being set holds
( b₁ -flat_tree {} = root-tree b₁ & b₁ -tree {} = root-tree b₁ )

proof end;

theorem Th21: :: TREES_4:21

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

proof end;

theorem Th22: :: TREES_4:22

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

proof end;

definition

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

proof end;

end;

definition

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

proof end;

end;

definition

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

proof end;

end;

definition

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

proof end;

end;

definition

let c₁ be non empty set ;
let c₂ be FinSequence of FinTrees c₁;
redefine func doms as doms c₂ -> FinSequence of FinTrees ;
coherence

proof end;

end;

definition

let c₁ be non empty set ;
let c₂ be Element of c₁;
let c₃ be FinSequence of FinTrees c₁;
redefine func -tree as c₂ -tree c₃ -> Element of FinTrees a₁;
coherence

proof end;

end;

definition

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

proof end;

end;

registration

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

proof end;

end;

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

ex b₁ being Tree st
for b₂ being FinSequence holds
( b₂ in b₁ iff ( b₂ in F₁() or ex b₃ being Element of F₁()ex b₄ being Element of F₂() st
( P₁[b₃] & b₂ = b₃ ^ b₄ ) ) )

proof end;

definition

let c₁, c₂ be DecoratedTree;
let c₃ be set ;
func c₁,c₃ <- c₂ -> DecoratedTree means :Def7: :: TREES_4:def 7
( ( for b₁ being FinSequence holds
( b₁ in dom a₄ iff ( b₁ in dom a₁ or ex b₂ being Node of a₁ex b₃ being Node of a₂ st
( b₂ in Leaves (dom a₁) & a₁ . b₂ = a₃ & b₁ = b₂ ^ b₃ ) ) ) ) & ( for b₁ being Node of a₁ st ( not b₁ in Leaves (dom a₁) or a₁ . b₁ <> a₃ ) holds
a₄ . b₁ = a₁ . b₁ ) & ( for b₁ being Node of a₁
for b₂ being Node of a₂ st b₁ in Leaves (dom a₁) & a₁ . b₁ = a₃ holds
a₄ . (b₁ ^ b₂) = a₂ . b₂ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines <- TREES_4:def 7 :

definition

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

proof end;

end;

theorem Th23: :: TREES_4:23

for b₁, b₂ being DecoratedTree
for b₃ being set st ( not b₃ in rng b₁ or not b₃ in Leaves b₁ ) holds
b₁,b₃ <- b₂ = b₁

proof end;

theorem Th24: :: TREES_4:24

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

proof end;

theorem Th25: :: TREES_4:25

for b₁, b₂ being non empty set
for b₃ being Element of b₁
for b₄ being Element of b₂ holds
( (root-tree [b₃,b₄]) `1 = root-tree b₃ & (root-tree [b₃,b₄]) `2 = root-tree b₄ )

proof end;

theorem Th26: :: TREES_4:26

for b₁, b₂ being set holds <:(root-tree b₁),(root-tree b₂):> = root-tree [b₁,b₂]

proof end;

theorem Th27: :: TREES_4:27

for b₁, b₂ being non empty set
for b₃ being Element of b₁
for b₄ being Element of b₂
for b₅ being non empty DTree-set of b₁,b₂
for b₆ being non empty DTree-set of b₁
for b₇ being FinSequence of b₅
for b₈ being FinSequence of b₆ st dom b₈ = dom b₇ & ( for b₉ being Nat st b₉ in dom b₇ holds
for b₁₀ being DecoratedTree of b₁,b₂ st b₁₀ = b₇ . b₉ holds
b₈ . b₉ = b₁₀ `1 ) holds
([b₃,b₄] -tree b₇) `1 = b₃ -tree b₈

proof end;

theorem Th28: :: TREES_4:28

for b₁, b₂ being non empty set
for b₃ being Element of b₁
for b₄ being Element of b₂
for b₅ being non empty DTree-set of b₁,b₂
for b₆ being non empty DTree-set of b₂
for b₇ being FinSequence of b₅
for b₈ being FinSequence of b₆ st dom b₈ = dom b₇ & ( for b₉ being Nat st b₉ in dom b₇ holds
for b₁₀ being DecoratedTree of b₁,b₂ st b₁₀ = b₇ . b₉ holds
b₈ . b₉ = b₁₀ `2 ) holds
([b₃,b₄] -tree b₇) `2 = b₄ -tree b₈

proof end;

theorem Th29: :: TREES_4:29

for b₁, b₂ being non empty set
for b₃ being Element of b₁
for b₄ being Element of b₂
for b₅ being non empty DTree-set of b₁,b₂
for b₆ being FinSequence of b₅ ex b₇ being FinSequence of Trees b₁ st
( dom b₇ = dom b₆ & ( for b₈ being Nat st b₈ in dom b₆ holds
ex b₉ being Element of b₅ st
( b₉ = b₆ . b₈ & b₇ . b₈ = b₉ `1 ) ) & ([b₃,b₄] -tree b₆) `1 = b₃ -tree b₇ )

proof end;

theorem Th30: :: TREES_4:30

for b₁, b₂ being non empty set
for b₃ being Element of b₁
for b₄ being Element of b₂
for b₅ being non empty DTree-set of b₁,b₂
for b₆ being FinSequence of b₅ ex b₇ being FinSequence of Trees b₂ st
( dom b₇ = dom b₆ & ( for b₈ being Nat st b₈ in dom b₆ holds
ex b₉ being Element of b₅ st
( b₉ = b₆ . b₈ & b₇ . b₈ = b₉ `2 ) ) & ([b₃,b₄] -tree b₆) `2 = b₄ -tree b₇ )

proof end;

theorem Th31: :: TREES_4:31

for b₁, b₂ being non empty set
for b₃ being Element of b₁
for b₄ being Element of b₂
for b₅ being FinSequence of FinTrees [:b₁,b₂:] ex b₆ being FinSequence of FinTrees b₁ st
( dom b₆ = dom b₅ & ( for b₇ being Nat st b₇ in dom b₅ holds
ex b₈ being Element of FinTrees [:b₁,b₂:] st
( b₈ = b₅ . b₇ & b₆ . b₇ = b₈ `1 ) ) & ([b₃,b₄] -tree b₅) `1 = b₃ -tree b₆ )

proof end;

theorem Th32: :: TREES_4:32

for b₁, b₂ being non empty set
for b₃ being Element of b₁
for b₄ being Element of b₂
for b₅ being FinSequence of FinTrees [:b₁,b₂:] ex b₆ being FinSequence of FinTrees b₂ st
( dom b₆ = dom b₅ & ( for b₇ being Nat st b₇ in dom b₅ holds
ex b₈ being Element of FinTrees [:b₁,b₂:] st
( b₈ = b₅ . b₇ & b₆ . b₇ = b₈ `2 ) ) & ([b₃,b₄] -tree b₅) `2 = b₄ -tree b₆ )

proof end;