TREES_4: Joining of Decorated Trees

:: Joining of Decorated Trees
:: by Grzegorz Bancerek
::
:: Received October 8, 1993
:: Copyright (c) 1993 Association of Mizar Users

begin

definition

let T be DecoratedTree;
mode Node of T is Element of dom T;

end;

Lm1: now

let x, y be set ; :: thesis:
let p be FinSequence of x; :: thesis:
assume ( y in dom p or y in dom p ) ; :: thesis:
then A1: p . y in rng p by FUNCT_1:def 5;
rng p c= x by FINSEQ_1:def 4;
hence p . y in x by A1; :: thesis:

end;

definition

let T1, T2 be DecoratedTree;
redefine pred T1 = T2 means :: TREES_4:def 1
( dom T1 = dom T2 & ( for p being Node of T1 holds T1 . p = T2 . p ) );
compatibility

proof end;

end;

:: deftheorem defines = TREES_4:def 1 :

theorem Th1: :: TREES_4:1

for i, j being Element of NAT st elementary_tree i c= elementary_tree j holds
i <= j

proof end;

theorem Th2: :: TREES_4:2

for i, j being Element of NAT st elementary_tree i = elementary_tree j holds
i = j

proof end;

Lm2: for n being Element of NAT
for p being FinSequence st n < len p holds
( n + 1 in dom p & p . (n + 1) in rng p )

proof end;

Lm3: now

let n be Element of NAT ; :: thesis:
let x be set ; :: thesis:
let p be FinSequence of x; :: thesis:
assume n < len p ; :: thesis:
then A1: p . (n + 1) in rng p by Lm2;
rng p c= x by FINSEQ_1:def 4;
hence p . (n + 1) in x by A1; :: thesis:

end;

definition

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

end;

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

definition

let D be non empty set ;
let d be Element of D;
:: original: root-tree
redefine func root-tree d -> Element of FinTrees D;
coherence

proof end;

end;

theorem Th3: :: TREES_4:3

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

proof end;

theorem :: TREES_4:4

for x, y being set st root-tree x = root-tree y holds
x = y

proof end;

theorem Th5: :: TREES_4:5

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

proof end;

theorem :: TREES_4:6

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

proof end;

definition

let x be set ;
let p be FinSequence;
func x -flat_tree p -> DecoratedTree means :Def3: :: TREES_4:def 3
( dom it = elementary_tree (len p) & it . {} = x & ( for n being Element of NAT st n < len p holds
it . <*n*> = p . (n + 1) ) );
existence

proof end;

uniqueness

proof end;

end;

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

theorem :: TREES_4:7

for x, y being set
for p, q being FinSequence st x -flat_tree p = y -flat_tree q holds
( x = y & p = q )

proof end;

theorem Th8: :: TREES_4:8

for j, i being Element of NAT st j < i holds
(elementary_tree i) | <*j*> = elementary_tree 0

proof end;

theorem Th9: :: TREES_4:9

for x being set
for i being Element of NAT
for p being FinSequence st i < len p holds
(x -flat_tree p) | <*i*> = root-tree (p . (i + 1))

proof end;

definition

let x be set ;
let p be FinSequence;
assume A1: p is DTree-yielding ;
func x -tree p -> DecoratedTree means :Def4: :: TREES_4:def 4
( ex q being DTree-yielding FinSequence st
( p = q & dom it = tree (doms q) ) & it . {} = x & ( for n being Element of NAT st n < len p holds
it | <*n*> = p . (n + 1) ) );
existence

proof end;

uniqueness

proof end;

end;

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

definition

let x be set ;
let T be DecoratedTree;
func x -tree T -> DecoratedTree equals :: TREES_4:def 5
x -tree <*T*>;
correctness ;

end;

:: deftheorem defines -tree TREES_4:def 5 :

definition

let x be set ;
let T1, T2 be DecoratedTree;
func x -tree (T1,T2) -> DecoratedTree equals :: TREES_4:def 6
x -tree <*T1,T2*>;
correctness ;

end;

:: deftheorem defines -tree TREES_4:def 6 :

theorem Th10: :: TREES_4:10

for x being set
for p being DTree-yielding FinSequence holds dom (x -tree p) = tree (doms p)

proof end;

theorem Th11: :: TREES_4:11

for y, x being set
for p being DTree-yielding FinSequence holds
( y in dom (x -tree p) iff ( y = {} or ex i being Element of NAT ex T being DecoratedTree ex q being Node of T st
( i < len p & T = p . (i + 1) & y = <*i*> ^ q ) ) )

proof end;

theorem Th12: :: TREES_4:12

for x being set
for p being DTree-yielding FinSequence
for i being Element of NAT
for T being DecoratedTree
for q being Node of T st i < len p & T = p . (i + 1) holds
(x -tree p) . (<*i*> ^ q) = T . q

proof end;

theorem :: TREES_4:13

for x being set
for T being DecoratedTree holds dom (x -tree T) = ^ (dom T)

proof end;

theorem :: TREES_4:14

for x being set
for T1, T2 being DecoratedTree holds dom (x -tree (T1,T2)) = tree ((dom T1),(dom T2))

proof end;

theorem :: TREES_4:15

for x, y being set
for p, q being DTree-yielding FinSequence st x -tree p = y -tree q holds
( x = y & p = q )

proof end;

theorem :: TREES_4:16

for x, y being set
for p being FinSequence st root-tree x = y -flat_tree p holds
( x = y & p = {} )

proof end;

theorem :: TREES_4:17

for x, y being set
for p being FinSequence st root-tree x = y -tree p & p is DTree-yielding holds
( x = y & p = {} )

proof end;

theorem :: TREES_4:18

for x, y being set
for p, q being FinSequence st x -flat_tree p = y -tree q & q is DTree-yielding holds
( x = y & len p = len q & ( for i being Element of NAT st i in dom p holds
q . i = root-tree (p . i) ) )

proof end;

theorem :: TREES_4:19

for x being set
for p being DTree-yielding FinSequence
for n being Element of NAT
for q being FinSequence st <*n*> ^ q in dom (x -tree p) holds
(x -tree p) . (<*n*> ^ q) = p .. ((n + 1),q)

proof end;

theorem :: TREES_4:20

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

proof end;

theorem :: TREES_4:21

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

proof end;

theorem :: TREES_4:22

for x being set
for T being DecoratedTree holds x -tree <*T*> = ((elementary_tree 1) --> x) with-replacement (<*0*>,T)

proof end;

registration

let D be non empty set ;
let d be Element of D;
let p be FinSequence of D;
cluster d -flat_tree p -> D -valued ;
coherence

proof end;

end;

registration

let D be non empty set ;
let F be non empty DTree-set of D;
let d be Element of D;
let p be FinSequence of F;
cluster d -tree p -> D -valued ;
coherence

proof end;

end;

registration

let D be non empty set ;
let d be Element of D;
let T be DecoratedTree of D;
cluster d -tree T -> D -valued ;
coherence

proof end;

end;

registration

let D be non empty set ;
let d be Element of D;
let T1, T2 be DecoratedTree of D;
cluster d -tree (T1,T2) -> D -valued ;
coherence

proof end;

end;

definition

let D be non empty set ;
let p be FinSequence of FinTrees D;
:: original: doms
redefine func doms p -> FinSequence of FinTrees ;
coherence

proof end;

end;

definition

let D be non empty set ;
let d be Element of D;
let p be FinSequence of FinTrees D;
:: original: -tree
redefine func d -tree p -> Element of FinTrees D;
coherence

proof end;

end;

definition

let D be non empty set ;
let x be Subset of D;
:: original: FinSequence
redefine mode FinSequence of x -> FinSequence of D;
coherence

proof end;

end;

registration

let D be non empty constituted-DTrees set ;
let X be Subset of D;
cluster -> DTree-yielding FinSequence of X;
coherence ;

end;

begin

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

ex T being Tree st
for p being FinSequence holds
( p in T iff ( p in F₁() or ex q being Element of F₁() ex r being Element of F₂() st
( P₁[q] & p = q ^ r ) ) )

proof end;

definition

let T, T9 be DecoratedTree;
let x be set ;
func (T,x) <- T9 -> DecoratedTree means :Def7: :: TREES_4:def 7
( ( for p being FinSequence holds
( p in dom it iff ( p in dom T or ex q being Node of T ex r being Node of T9 st
( q in Leaves (dom T) & T . q = x & p = q ^ r ) ) ) ) & ( for p being Node of T st ( not p in Leaves (dom T) or T . p <> x ) holds
it . p = T . p ) & ( for p being Node of T
for q being Node of T9 st p in Leaves (dom T) & T . p = x holds
it . (p ^ q) = T9 . q ) );
existence

proof end;

uniqueness

proof end;

end;

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

registration

let D be non empty set ;
let T, T9 be DecoratedTree of D;
let x be set ;
cluster (T,x) <- T9 -> D -valued ;
coherence

proof end;

end;

theorem :: TREES_4:23

for T, T9 being DecoratedTree
for x being set st ( not x in rng T or not x in Leaves T ) holds
(T,x) <- T9 = T

proof end;

begin

theorem Th24: :: TREES_4:24

for D1, D2 being non empty set
for T being DecoratedTree of D1,D2 holds
( dom (T `1) = dom T & dom (T `2) = dom T )

proof end;

theorem Th25: :: TREES_4:25

for D1, D2 being non empty set
for d1 being Element of D1
for d2 being Element of D2 holds
( (root-tree [d1,d2]) `1 = root-tree d1 & (root-tree [d1,d2]) `2 = root-tree d2 )

proof end;

theorem :: TREES_4:26

for x, y being set holds <:(root-tree x),(root-tree y):> = root-tree [x,y]

proof end;

theorem Th27: :: TREES_4:27

for D1, D2 being non empty set
for d1 being Element of D1
for d2 being Element of D2
for F being non empty DTree-set of D1,D2
for F1 being non empty DTree-set of D1
for p being FinSequence of F
for p1 being FinSequence of F1 st dom p1 = dom p & ( for i being Element of NAT st i in dom p holds
for T being DecoratedTree of D1,D2 st T = p . i holds
p1 . i = T `1 ) holds
([d1,d2] -tree p) `1 = d1 -tree p1

proof end;

theorem Th28: :: TREES_4:28

for D1, D2 being non empty set
for d1 being Element of D1
for d2 being Element of D2
for F being non empty DTree-set of D1,D2
for F2 being non empty DTree-set of D2
for p being FinSequence of F
for p2 being FinSequence of F2 st dom p2 = dom p & ( for i being Element of NAT st i in dom p holds
for T being DecoratedTree of D1,D2 st T = p . i holds
p2 . i = T `2 ) holds
([d1,d2] -tree p) `2 = d2 -tree p2

proof end;

theorem Th29: :: TREES_4:29

for D1, D2 being non empty set
for d1 being Element of D1
for d2 being Element of D2
for F being non empty DTree-set of D1,D2
for p being FinSequence of F ex p1 being FinSequence of Trees D1 st
( dom p1 = dom p & ( for i being Element of NAT st i in dom p holds
ex T being Element of F st
( T = p . i & p1 . i = T `1 ) ) & ([d1,d2] -tree p) `1 = d1 -tree p1 )

proof end;

theorem Th30: :: TREES_4:30

for D1, D2 being non empty set
for d1 being Element of D1
for d2 being Element of D2
for F being non empty DTree-set of D1,D2
for p being FinSequence of F ex p2 being FinSequence of Trees D2 st
( dom p2 = dom p & ( for i being Element of NAT st i in dom p holds
ex T being Element of F st
( T = p . i & p2 . i = T `2 ) ) & ([d1,d2] -tree p) `2 = d2 -tree p2 )

proof end;

theorem :: TREES_4:31

for D1, D2 being non empty set
for d1 being Element of D1
for d2 being Element of D2
for p being FinSequence of FinTrees [:D1,D2:] ex p1 being FinSequence of FinTrees D1 st
( dom p1 = dom p & ( for i being Element of NAT st i in dom p holds
ex T being Element of FinTrees [:D1,D2:] st
( T = p . i & p1 . i = T `1 ) ) & ([d1,d2] -tree p) `1 = d1 -tree p1 )

proof end;

theorem :: TREES_4:32

for D1, D2 being non empty set
for d1 being Element of D1
for d2 being Element of D2
for p being FinSequence of FinTrees [:D1,D2:] ex p2 being FinSequence of FinTrees D2 st
( dom p2 = dom p & ( for i being Element of NAT st i in dom p holds
ex T being Element of FinTrees [:D1,D2:] st
( T = p . i & p2 . i = T `2 ) ) & ([d1,d2] -tree p) `2 = d2 -tree p2 )

proof end;