:: 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: for p being FinSequence of x st ( y in dom p or y in dom p ) holds
p . y in x

let p be FinSequence of x; :: thesis: ( ( y in dom p or y in dom p ) implies p . y in x )
assume ( y in dom p or y in dom p ) ; :: thesis: p . y in x
then A2: 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 A2; :: thesis: verum
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
( T1 = T2 iff ( dom T1 = dom T2 & ( for p being Node of T1 holds T1 . p = T2 . p ) ) )
proof end;
end;

:: deftheorem defines = TREES_4:def 1 :
for T1, T2 being DecoratedTree holds
( T1 = T2 iff ( dom T1 = dom T2 & ( for p being Node of T1 holds T1 . p = T2 . p ) ) );

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: for x being set
for p being FinSequence of x st n < len p holds
p . (n + 1) in x

let x be set ; :: thesis: for p being FinSequence of x st n < len p holds
p . (n + 1) in x

let p be FinSequence of x; :: thesis: ( n < len p implies p . (n + 1) in x )
assume n < len p ; :: thesis: p . (n + 1) in x
then A2: p . (n + 1) in rng p by Lm2;
rng p c= x by FINSEQ_1:def 4;
hence p . (n + 1) in x by A2; :: thesis: verum
end;

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

:: deftheorem defines root-tree TREES_4:def 2 :
for x being set holds root-tree x = (elementary_tree 0) --> x;

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
root-tree d is Element of FinTrees D
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
ex b1 being DecoratedTree st
( dom b1 = elementary_tree (len p) & b1 . {} = x & ( for n being Element of NAT st n < len p holds
b1 . <*n*> = p . (n + 1) ) )
proof end;
uniqueness
for b1, b2 being DecoratedTree st dom b1 = elementary_tree (len p) & b1 . {} = x & ( for n being Element of NAT st n < len p holds
b1 . <*n*> = p . (n + 1) ) & dom b2 = elementary_tree (len p) & b2 . {} = x & ( for n being Element of NAT st n < len p holds
b2 . <*n*> = p . (n + 1) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines -flat_tree TREES_4:def 3 :
for x being set
for p being FinSequence
for b3 being DecoratedTree holds
( b3 = x -flat_tree p iff ( dom b3 = elementary_tree (len p) & b3 . {} = x & ( for n being Element of NAT st n < len p holds
b3 . <*n*> = p . (n + 1) ) ) );

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
ex b1 being DecoratedTree st
( ex q being DTree-yielding FinSequence st
( p = q & dom b1 = tree (doms q) ) & b1 . {} = x & ( for n being Element of NAT st n < len p holds
b1 | <*n*> = p . (n + 1) ) )
proof end;
uniqueness
for b1, b2 being DecoratedTree st ex q being DTree-yielding FinSequence st
( p = q & dom b1 = tree (doms q) ) & b1 . {} = x & ( for n being Element of NAT st n < len p holds
b1 | <*n*> = p . (n + 1) ) & ex q being DTree-yielding FinSequence st
( p = q & dom b2 = tree (doms q) ) & b2 . {} = x & ( for n being Element of NAT st n < len p holds
b2 | <*n*> = p . (n + 1) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines -tree TREES_4:def 4 :
for x being set
for p being FinSequence st p is DTree-yielding holds
for b3 being DecoratedTree holds
( b3 = x -tree p iff ( ex q being DTree-yielding FinSequence st
( p = q & dom b3 = tree (doms q) ) & b3 . {} = x & ( for n being Element of NAT st n < len p holds
b3 | <*n*> = p . (n + 1) ) ) );

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

:: deftheorem defines -tree TREES_4:def 5 :
for x being set
for T being DecoratedTree holds x -tree T = x -tree <*T*>;

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
coherence
x -tree <*T1,T2*> is DecoratedTree
;
;
end;

:: deftheorem defines -tree TREES_4:def 6 :
for x being set
for T1, T2 being DecoratedTree holds x -tree (T1,T2) = x -tree <*T1,T2*>;

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
d -flat_tree p is D -valued
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
d -tree p is D -valued
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
d -tree T is D -valued
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
d -tree (T1,T2) is D -valued
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
doms p is FinSequence of FinTrees
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
d -tree p is Element of FinTrees D
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
for b1 being FinSequence of x holds b1 is FinSequence of D
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
for b1 being FinSequence of X holds b1 is DTree-yielding
;
end;

begin

scheme :: TREES_4:sch 1
ExpandTree{ F1() -> Tree, F2() -> Tree, P1[ set ] } :
ex T being Tree st
for p being FinSequence holds
( p in T iff ( p in F1() or ex q being Element of F1() ex r being Element of F2() st
( P1[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
ex b1 being DecoratedTree st
( ( for p being FinSequence holds
( p in dom b1 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
b1 . 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
b1 . (p ^ q) = T9 . q ) )
proof end;
uniqueness
for b1, b2 being DecoratedTree st ( for p being FinSequence holds
( p in dom b1 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
b1 . 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
b1 . (p ^ q) = T9 . q ) & ( for p being FinSequence holds
( p in dom b2 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
b2 . 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
b2 . (p ^ q) = T9 . q ) holds
b1 = b2
proof end;
end;

:: deftheorem Def7 defines <- TREES_4:def 7 :
for T, T9 being DecoratedTree
for x being set
for b4 being DecoratedTree holds
( b4 = (T,x) <- T9 iff ( ( for p being FinSequence holds
( p in dom b4 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
b4 . 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
b4 . (p ^ q) = T9 . q ) ) );

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
(T,x) <- T9 is D -valued
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;