:: TREES_4 semantic presentation

begin

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


Lm1: now__::_thesis:_for_x,_y_being_set_
for_p_being_FinSequence_of_x_st_(_y_in_dom_p_or_y_in_dom_p_)_holds_
p_._y_in_x
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 A1: p . y in rng p by FUNCT_1:def_3;
 rng p c= x by FINSEQ_1:def_4;
hence  p . y in x by A1; ::_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
 ( ( for p being Node of T1 holds T1 . p = T2 . p ) & dom T1 = dom T2 implies for x being set st x in dom T1 holds
T1 . x = T2 . x ) ;
hence  ( T1 = T2 iff ( dom T1 = dom T2 & ( for p being Node of T1 holds T1 . p = T2 . p ) ) ) by FUNCT_1:2; ::_thesis: verum
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
let i, j be Element of NAT ; ::_thesis: ( elementary_tree i c= elementary_tree j implies i <= j )
assume that
A1: elementary_tree i c= elementary_tree j and
A2: i > j ; ::_thesis: contradiction
 <*j*> in elementary_tree i by A2, TREES_1:28;
then A3: ex n being Element of NAT st
( n < j & <*j*> = <*n*> ) by A1, TREES_1:30;
 <*j*> . 1 = j by FINSEQ_1:40;
hence  contradiction by A3, FINSEQ_1:40; ::_thesis: verum
end;

theorem Th2: :: TREES_4:2
for i, j being Element of NAT st elementary_tree i = elementary_tree j holds
i = j
proof
let i, j be Element of NAT ; ::_thesis: ( elementary_tree i = elementary_tree j implies i = j )
assume  elementary_tree i = elementary_tree j ; ::_thesis: i = j
then  ( i <= j & i >= j ) by Th1;
hence  i = j by XXREAL_0:1; ::_thesis: verum
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
let n be Element of NAT ; ::_thesis: for p being FinSequence st n < len p holds
( n + 1 in dom p & p . (n + 1) in rng p )
let p be FinSequence; ::_thesis: ( n < len p implies ( n + 1 in dom p & p . (n + 1) in rng p ) )
assume A1: n < len p ; ::_thesis: ( n + 1 in dom p & p . (n + 1) in rng p )
 n >= 0 by NAT_1:2;
then A2: n + 1 >= 0 + 1 by XREAL_1:7;
 n + 1 <= len p by A1, NAT_1:13;
then  n + 1 in dom p by A2, FINSEQ_3:25;
hence  ( n + 1 in dom p & p . (n + 1) in rng p ) by FUNCT_1:def_3; ::_thesis: verum
end;

Lm3: now__::_thesis:_for_n_being_Element_of_NAT_
for_x_being_set_
for_p_being_FinSequence_of_x_st_n_<_len_p_holds_
p_._(n_+_1)_in_x
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 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: 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
 dom ((elementary_tree 0) --> d) = elementary_tree 0 by FUNCOP_1:13;
hence  root-tree d is Element of FinTrees D by TREES_3:def_8; ::_thesis: verum
end;
end;

theorem Th3: :: TREES_4:3
for x being set holds
( dom (root-tree x) = elementary_tree 0 & (root-tree x) . {} = x )
proof
let x be set ; ::_thesis: ( dom (root-tree x) = elementary_tree 0 & (root-tree x) . {} = x )
 {} in elementary_tree 0 by TARSKI:def_1, TREES_1:29;
hence  ( dom (root-tree x) = elementary_tree 0 & (root-tree x) . {} = x ) by FUNCOP_1:7, FUNCOP_1:13; ::_thesis: verum
end;

theorem :: TREES_4:4
for x, y being set st root-tree x = root-tree y holds
x = y
proof
let x, y be set ; ::_thesis: ( root-tree x = root-tree y implies x = y )
 (root-tree x) . {} = x by Th3;
hence  ( root-tree x = root-tree y implies x = y ) by Th3; ::_thesis: verum
end;

theorem Th5: :: TREES_4:5
for T being DecoratedTree st dom T = elementary_tree 0 holds
T = root-tree (T . {})
proof
let T be DecoratedTree; ::_thesis: ( dom T = elementary_tree 0 implies T = root-tree (T . {}) )
assume A1: dom T = elementary_tree 0 ; ::_thesis: T = root-tree (T . {})
then  for x being set st x in dom T holds
T . x = T . {} by TARSKI:def_1, TREES_1:29;
hence  T = root-tree (T . {}) by A1, FUNCOP_1:11; ::_thesis: verum
end;

theorem :: TREES_4:6
for x being set holds root-tree x = {[{},x]}
proof
let x be set ; ::_thesis: root-tree x = {[{},x]}
thus  root-tree x = [:{{}},{x}:] by FUNCOP_1:def_2, TREES_1:29
.= {[{},x]} by ZFMISC_1:29 ; ::_thesis: verum
end;

definition
let x be set ;
let p be FinSequence;
funcx -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
defpred S1[ set , set ] means ( ( $1 = {} & $2 = x ) or ex n being Element of NAT st
( $1 = <*n*> & $2 = p . (n + 1) ) );
A1: for z being set st z in elementary_tree (len p) holds
ex y being set st S1[z,y]
proof
let z be set ; ::_thesis: ( z in elementary_tree (len p) implies ex y being set st S1[z,y] )
assume  z in elementary_tree (len p) ; ::_thesis: ex y being set st S1[z,y]
then reconsider z = z as Element of elementary_tree (len p) ;
reconsider z = z as FinSequence of NAT ;
A2: ( z = {} or ex n being Element of NAT st
( n < len p & z = <*n*> ) ) by TREES_1:30;
now__::_thesis:_(_ex_n_being_Element_of_NAT_st_
(_z_=_<*n*>_&_n_<_len_p_)_implies_ex_y_being_set_ex_n_being_Element_of_NAT_st_
(_z_=_<*n*>_&_y_=_p_._(n_+_1)_)_)
given n being Element of NAT  such that A3: z = <*n*> and
 n < len p ; ::_thesis: ex y being set ex n being Element of NAT st
( z = <*n*> & y = p . (n + 1) )
take y = p . (n + 1); ::_thesis: ex n being Element of NAT st
( z = <*n*> & y = p . (n + 1) )
take n = n; ::_thesis: ( z = <*n*> & y = p . (n + 1) )
thus  ( z = <*n*> & y = p . (n + 1) ) by A3; ::_thesis: verum
end;
hence  ex y being set st S1[z,y] by A2; ::_thesis: verum
end;
consider f being Function such that
A4: ( dom f = elementary_tree (len p) & ( for y being set st y in elementary_tree (len p) holds
S1[y,f . y] ) ) from CLASSES1:sch_1(A1);
reconsider f = f as DecoratedTree by A4, TREES_2:def_8;
take  f ; ::_thesis: ( dom f = elementary_tree (len p) & f . {} = x & ( for n being Element of NAT st n < len p holds
f . <*n*> = p . (n + 1) ) )
thus  dom f = elementary_tree (len p) by A4; ::_thesis: ( f . {} = x & ( for n being Element of NAT st n < len p holds
f . <*n*> = p . (n + 1) ) )
 ( {} in dom f & ( for n being Element of NAT st {} = <*n*> holds
f . {} <> p . (n + 1) ) ) by TREES_1:22;
hence  f . {} = x by A4; ::_thesis: for n being Element of NAT st n < len p holds
f . <*n*> = p . (n + 1)
let n be Element of NAT ; ::_thesis: ( n < len p implies f . <*n*> = p . (n + 1) )
assume  n < len p ; ::_thesis: f . <*n*> = p . (n + 1)
then  <*n*> in dom f by A4, TREES_1:28;
then consider k being Element of NAT  such that
A5: <*n*> = <*k*> and
A6: f . <*n*> = p . (k + 1) by A4;
k = <*n*> . 1 by A5, FINSEQ_1:40
.= n by FINSEQ_1:40 ;
hence  f . <*n*> = p . (n + 1) by A6; ::_thesis: verum
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
let T1, T2 be DecoratedTree; ::_thesis: ( dom T1 = elementary_tree (len p) & T1 . {} = x & ( for n being Element of NAT st n < len p holds
T1 . <*n*> = p . (n + 1) ) & dom T2 = elementary_tree (len p) & T2 . {} = x & ( for n being Element of NAT st n < len p holds
T2 . <*n*> = p . (n + 1) ) implies T1 = T2 )
assume that
A7: dom T1 = elementary_tree (len p) and
A8: T1 . {} = x and
A9: for n being Element of NAT st n < len p holds
T1 . <*n*> = p . (n + 1) and
A10: dom T2 = elementary_tree (len p) and
A11: T2 . {} = x and
A12: for n being Element of NAT st n < len p holds
T2 . <*n*> = p . (n + 1) ; ::_thesis: T1 = T2
now__::_thesis:_for_x_being_set_st_x_in_elementary_tree_(len_p)_holds_
T1_._x_=_T2_._x
let x be set ; ::_thesis: ( x in elementary_tree (len p) implies T1 . x = T2 . x )
assume  x in elementary_tree (len p) ; ::_thesis: T1 . x = T2 . x
then reconsider x9 = x as Element of elementary_tree (len p) ;
A13: ( x9 = {} or ex n being Element of NAT st
( n < len p & x9 = <*n*> ) ) by TREES_1:30;
now__::_thesis:_(_ex_n_being_Element_of_NAT_st_
(_n_<_len_p_&_x_=_<*n*>_)_implies_T1_._x_=_T2_._x_)
given n being Element of NAT  such that A14: ( n < len p & x = <*n*> ) ; ::_thesis: T1 . x = T2 . x
thus T1 . x = p . (n + 1) by A9, A14
.= T2 . x by A12, A14 ; ::_thesis: verum
end;
hence  T1 . x = T2 . x by A8, A11, A13; ::_thesis: verum
end;
hence  T1 = T2 by A7, A10, FUNCT_1:2; ::_thesis: verum
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
let x, y be set ; ::_thesis: for p, q being FinSequence st x -flat_tree p = y -flat_tree q holds
( x = y & p = q )
let p, q be FinSequence; ::_thesis: ( x -flat_tree p = y -flat_tree q implies ( x = y & p = q ) )
assume A1: x -flat_tree p = y -flat_tree q ; ::_thesis: ( x = y & p = q )
 (x -flat_tree p) . {} = x by Def3;
hence  x = y by A1, Def3; ::_thesis: p = q
A2: ( dom (x -flat_tree p) = elementary_tree (len p) & dom (y -flat_tree q) = elementary_tree (len q) ) by Def3;
then A3: len p = len q by A1, Th2;
now__::_thesis:_for_i_being_Nat_st_i_>=_1_&_i_<=_len_p_holds_
p_._i_=_q_._i
let i be Nat; ::_thesis: ( i >= 1 & i <= len p implies p . i = q . i )
assume that
A4: i >= 1 and
A5: i <= len p ; ::_thesis: p . i = q . i
consider n being Nat such that
A6: i = 1 + n by A4, NAT_1:10;
A7: ( n in NAT & n < len p ) by A5, A6, NAT_1:13, ORDINAL1:def_12;
then  p . i = (x -flat_tree p) . <*n*> by A6, Def3;
hence  p . i = q . i by A1, A3, A6, A7, Def3; ::_thesis: verum
end;
hence  p = q by A1, A2, Th2, FINSEQ_1:14; ::_thesis: verum
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
let j, i be Element of NAT ; ::_thesis: ( j < i implies (elementary_tree i) | <*j*> = elementary_tree 0 )
set p = i |-> (elementary_tree 0);
set T = tree (i |-> (elementary_tree 0));
assume A1: j < i ; ::_thesis: (elementary_tree i) | <*j*> = elementary_tree 0
then A2: ( 1 + j >= 1 & j + 1 <= i ) by NAT_1:11, NAT_1:13;
 len (i |-> (elementary_tree 0)) = i by CARD_1:def_7;
then A3: ( elementary_tree i = tree (i |-> (elementary_tree 0)) & (tree (i |-> (elementary_tree 0))) | <*j*> = (i |-> (elementary_tree 0)) . (j + 1) ) by A1, TREES_3:49, TREES_3:54;
 j + 1 in Seg i by A2;
hence  (elementary_tree i) | <*j*> = elementary_tree 0 by A3, FUNCOP_1:7; ::_thesis: verum
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
let x be set ; ::_thesis: 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))
let i be Element of NAT ; ::_thesis: for p being FinSequence st i < len p holds
(x -flat_tree p) | <*i*> = root-tree (p . (i + 1))
let p be FinSequence; ::_thesis: ( i < len p implies (x -flat_tree p) | <*i*> = root-tree (p . (i + 1)) )
reconsider t = {} as Element of (dom (x -flat_tree p)) | <*i*> by TREES_1:22;
assume A1: i < len p ; ::_thesis: (x -flat_tree p) | <*i*> = root-tree (p . (i + 1))
then A2: (x -flat_tree p) . <*i*> = p . (i + 1) by Def3;
A3: dom (x -flat_tree p) = elementary_tree (len p) by Def3;
 (elementary_tree (len p)) | <*i*> = elementary_tree 0 by A1, Th8;
then A4: dom ((x -flat_tree p) | <*i*>) = elementary_tree 0 by A3, TREES_2:def_10;
 ( <*i*> ^ t = <*i*> & ((x -flat_tree p) | <*i*>) . t = (x -flat_tree p) . (<*i*> ^ t) ) by FINSEQ_1:34, TREES_2:def_10;
hence  (x -flat_tree p) | <*i*> = root-tree (p . (i + 1)) by A2, A4, Th5; ::_thesis: verum
end;

definition
let x be set ;
let p be FinSequence;
assume B1: p is DTree-yielding ;
funcx -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
A1: dom (doms p) = dom p by B1, TREES_3:37;
reconsider q = doms p as Tree-yielding FinSequence by B1;
defpred S1[ set , set ] means ( ( $1 = {} & $2 = x ) or ( $1 <> {} & ex n being Element of NAT ex r being FinSequence st
( $1 = <*n*> ^ r & $2 = p .. ((n + 1),r) ) ) );
A2: for y being set st y in tree q holds
ex z being set st S1[y,z]
proof
let y be set ; ::_thesis: ( y in tree q implies ex z being set st S1[y,z] )
assume  y in tree q ; ::_thesis: ex z being set st S1[y,z]
then reconsider s = y as Element of tree q ;
now__::_thesis:_(_y_<>_{}_implies_ex_z_being_set_st_
(_(_y_=_{}_&_z_=_x_)_or_(_y_<>_{}_&_ex_n_being_Element_of_NAT_ex_r_being_FinSequence_st_
(_y_=_<*n*>_^_r_&_z_=_p_.._((n_+_1),r)_)_)_)_)
assume  y <> {} ; ::_thesis: ex z being set st
( ( y = {} & z = x ) or ( y <> {} & ex n being Element of NAT ex r being FinSequence st
( y = <*n*> ^ r & z = p .. ((n + 1),r) ) ) )
then consider w being FinSequence of NAT , n being Element of NAT  such that
A3: s = <*n*> ^ w by FINSEQ_2:130;
reconsider w = w as FinSequence ;
take z = p .. ((n + 1),w); ::_thesis: ( ( y = {} & z = x ) or ( y <> {} & ex n being Element of NAT ex r being FinSequence st
( y = <*n*> ^ r & z = p .. ((n + 1),r) ) ) )
thus  ( ( y = {} & z = x ) or ( y <> {} & ex n being Element of NAT ex r being FinSequence st
( y = <*n*> ^ r & z = p .. ((n + 1),r) ) ) ) by A3; ::_thesis: verum
end;
hence  ex z being set st S1[y,z] ; ::_thesis: verum
end;
consider T being Function such that
A4: ( dom T = tree q & ( for y being set st y in tree q holds
S1[y,T . y] ) ) from CLASSES1:sch_1(A2);
reconsider T = T as DecoratedTree by A4, TREES_2:def_8;
take  T ; ::_thesis: ( ex q being DTree-yielding FinSequence st
( p = q & dom T = tree (doms q) ) & T . {} = x & ( for n being Element of NAT st n < len p holds
T | <*n*> = p . (n + 1) ) )
thus  ex q being DTree-yielding FinSequence st
( p = q & dom T = tree (doms q) ) by B1, A4; ::_thesis: ( T . {} = x & ( for n being Element of NAT st n < len p holds
T | <*n*> = p . (n + 1) ) )
 {} in tree q by TREES_1:22;
hence  T . {} = x by A4; ::_thesis: for n being Element of NAT st n < len p holds
T | <*n*> = p . (n + 1)
A5: len p = len q by A1, FINSEQ_3:29;
let n be Element of NAT ; ::_thesis: ( n < len p implies T | <*n*> = p . (n + 1) )
assume A6: n < len p ; ::_thesis: T | <*n*> = p . (n + 1)
then A7: n + 1 in dom p by Lm2;
then reconsider t = p . (n + 1) as DecoratedTree by B1, TREES_3:24;
A8: dom t = q . (n + 1) by A7, FUNCT_6:22;
A9: dom t = q . (n + 1) by A7, FUNCT_6:22
.= (dom T) | <*n*> by A4, A5, A6, TREES_3:49 ;
A10: (dom T) | <*n*> = dom (T | <*n*>) by TREES_2:def_10;
now__::_thesis:_for_r_being_FinSequence_of_NAT_st_r_in_dom_t_holds_
(T_|_<*n*>)_._r_=_t_._r
let r be FinSequence of NAT ; ::_thesis: ( r in dom t implies (T | <*n*>) . r = t . r )
assume A11: r in dom t ; ::_thesis: (T | <*n*>) . r = t . r
then  <*n*> ^ r in dom T by A4, A5, A6, A8, TREES_3:def_15;
then consider m being Element of NAT , s being FinSequence such that
A12: <*n*> ^ r = <*m*> ^ s and
A13: T . (<*n*> ^ r) = p .. ((m + 1),s) by A4;
A14: ( (<*n*> ^ r) . 1 = n & (<*m*> ^ s) . 1 = m ) by FINSEQ_1:41;
then  ( m + 1 in dom p & r = s ) by A6, A12, Lm2, FINSEQ_1:33;
then  p .. ((m + 1),s) = t . r by A11, A12, A14, FUNCT_5:38;
hence  (T | <*n*>) . r = t . r by A9, A11, A13, TREES_2:def_10; ::_thesis: verum
end;
hence  T | <*n*> = p . (n + 1) by A9, A10, TREES_2:31; ::_thesis: verum
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
let T1, T2 be DecoratedTree; ::_thesis: ( ex q being DTree-yielding FinSequence st
( p = q & dom T1 = tree (doms q) ) & T1 . {} = x & ( for n being Element of NAT st n < len p holds
T1 | <*n*> = p . (n + 1) ) & ex q being DTree-yielding FinSequence st
( p = q & dom T2 = tree (doms q) ) & T2 . {} = x & ( for n being Element of NAT st n < len p holds
T2 | <*n*> = p . (n + 1) ) implies T1 = T2 )
given q1 being DTree-yielding FinSequence such that A15: p = q1 and
A16: dom T1 = tree (doms q1) ; ::_thesis: ( not T1 . {} = x or ex n being Element of NAT st
( n < len p & not T1 | <*n*> = p . (n + 1) ) or for q being DTree-yielding FinSequence holds
( not p = q or not dom T2 = tree (doms q) ) or not T2 . {} = x or ex n being Element of NAT st
( n < len p & not T2 | <*n*> = p . (n + 1) ) or T1 = T2 )
assume that
A17: T1 . {} = x and
A18: for n being Element of NAT st n < len p holds
T1 | <*n*> = p . (n + 1) ; ::_thesis: ( for q being DTree-yielding FinSequence holds
( not p = q or not dom T2 = tree (doms q) ) or not T2 . {} = x or ex n being Element of NAT st
( n < len p & not T2 | <*n*> = p . (n + 1) ) or T1 = T2 )
given q2 being DTree-yielding FinSequence such that A19: ( p = q2 & dom T2 = tree (doms q2) ) ; ::_thesis: ( not T2 . {} = x or ex n being Element of NAT st
( n < len p & not T2 | <*n*> = p . (n + 1) ) or T1 = T2 )
assume that
A20: T2 . {} = x and
A21: for n being Element of NAT st n < len p holds
T2 | <*n*> = p . (n + 1) ; ::_thesis: T1 = T2
now__::_thesis:_for_q_being_FinSequence_of_NAT_st_q_in_dom_T1_holds_
T1_._q_=_T2_._q
let q be FinSequence of NAT ; ::_thesis: ( q in dom T1 implies T1 . q = T2 . q )
assume A22: q in dom T1 ; ::_thesis: T1 . q = T2 . q
now__::_thesis:_(_q_<>_{}_implies_T1_._q_=_T2_._q_)
assume  q <> {} ; ::_thesis: T1 . q = T2 . q
then consider s being FinSequence of NAT , n being Element of NAT  such that
A23: q = <*n*> ^ s by FINSEQ_2:130;
A24: <*n*> in dom T1 by A22, A23, TREES_1:21;
A25: n < len (doms q1) by A16, A22, A23, TREES_3:48;
 len (doms q1) = len p by A15, TREES_3:38;
then A26: ( T1 | <*n*> = p . (n + 1) & T2 | <*n*> = p . (n + 1) ) by A18, A21, A25;
A27: s in (dom T1) | <*n*> by A22, A23, A24, TREES_1:def_6;
then  T1 . q = (T1 | <*n*>) . s by A23, TREES_2:def_10;
hence  T1 . q = T2 . q by A15, A16, A19, A23, A26, A27, TREES_2:def_10; ::_thesis: verum
end;
hence  T1 . q = T2 . q by A17, A20; ::_thesis: verum
end;
hence  T1 = T2 by A15, A16, A19, TREES_2:31; ::_thesis: verum
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;
funcx -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;
funcx -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
let x be set ; ::_thesis: for p being DTree-yielding FinSequence holds dom (x -tree p) = tree (doms p)
let p be DTree-yielding FinSequence; ::_thesis: dom (x -tree p) = tree (doms p)
 ex q being DTree-yielding FinSequence st
( p = q & dom (x -tree p) = tree (doms q) ) by Def4;
hence  dom (x -tree p) = tree (doms p) ; ::_thesis: verum
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
let y, x be set ; ::_thesis: 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 ) ) )
let p be DTree-yielding FinSequence; ::_thesis: ( 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 ) ) )
A1: dom (x -tree p) = tree (doms p) by Th10;
A2: now__::_thesis:_(_ex_i_being_Element_of_NAT_ex_q_being_FinSequence_st_
(_i_<_len_(doms_p)_&_q_in_(doms_p)_._(i_+_1)_&_y_=_<*i*>_^_q_)_implies_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_)_)
given i being Element of NAT , q being FinSequence such that A3: i < len (doms p) and
A4: q in (doms p) . (i + 1) and
A5: y = <*i*> ^ q ; ::_thesis: 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 )
 len (doms p) = len p by TREES_3:38;
then A6: i + 1 in dom p by A3, Lm2;
then reconsider T = p . (i + 1) as DecoratedTree by TREES_3:24;
take i = i; ::_thesis: ex T being DecoratedTree ex q being Node of T st
( i < len p & T = p . (i + 1) & y = <*i*> ^ q )
take T = T; ::_thesis: ex q being Node of T st
( i < len p & T = p . (i + 1) & y = <*i*> ^ q )
reconsider q = q as Node of T by A4, A6, FUNCT_6:22;
take q = q; ::_thesis: ( i < len p & T = p . (i + 1) & y = <*i*> ^ q )
thus  ( i < len p & T = p . (i + 1) & y = <*i*> ^ q ) by A3, A5, TREES_3:38; ::_thesis: verum
end;
now__::_thesis:_(_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_)_implies_ex_i_being_Element_of_NAT_ex_q_being_FinSequence_st_
(_i_<_len_(doms_p)_&_q_in_(doms_p)_._(i_+_1)_&_y_=_<*i*>_^_q_)_)
given i being Element of NAT , T being DecoratedTree, q being Node of T such that A7: i < len p and
A8: T = p . (i + 1) and
A9: y = <*i*> ^ q ; ::_thesis: ex i being Element of NAT ex q being FinSequence st
( i < len (doms p) & q in (doms p) . (i + 1) & y = <*i*> ^ q )
reconsider q = q as FinSequence ;
take i = i; ::_thesis: ex q being FinSequence st
( i < len (doms p) & q in (doms p) . (i + 1) & y = <*i*> ^ q )
take q = q; ::_thesis: ( i < len (doms p) & q in (doms p) . (i + 1) & y = <*i*> ^ q )
 i + 1 in dom p by A7, Lm2;
then  (doms p) . (i + 1) = dom T by A8, FUNCT_6:22;
hence  ( i < len (doms p) & q in (doms p) . (i + 1) & y = <*i*> ^ q ) by A7, A9, TREES_3:38; ::_thesis: verum
end;
hence  ( 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 ) ) ) by A1, A2, TREES_3:def_15; ::_thesis: verum
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
let x be set ; ::_thesis: 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
let p be DTree-yielding FinSequence; ::_thesis: 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
let n be Element of NAT ; ::_thesis: for T being DecoratedTree
for q being Node of T st n < len p & T = p . (n + 1) holds
(x -tree p) . (<*n*> ^ q) = T . q
let T be DecoratedTree; ::_thesis: for q being Node of T st n < len p & T = p . (n + 1) holds
(x -tree p) . (<*n*> ^ q) = T . q
let q be Node of T; ::_thesis: ( n < len p & T = p . (n + 1) implies (x -tree p) . (<*n*> ^ q) = T . q )
assume A1: ( n < len p & T = p . (n + 1) ) ; ::_thesis: (x -tree p) . (<*n*> ^ q) = T . q
then A2: <*n*> ^ q in dom (x -tree p) by Th11;
then  <*n*> in dom (x -tree p) by TREES_1:21;
then  q in (dom (x -tree p)) | <*n*> by A2, TREES_1:def_6;
then  ((x -tree p) | <*n*>) . q = (x -tree p) . (<*n*> ^ q) by TREES_2:def_10;
hence  (x -tree p) . (<*n*> ^ q) = T . q by A1, Def4; ::_thesis: verum
end;

theorem :: TREES_4:13
for x being set
for T being DecoratedTree holds dom (x -tree T) = ^ (dom T)
proof
let x be set ; ::_thesis: for T being DecoratedTree holds dom (x -tree T) = ^ (dom T)
let T be DecoratedTree; ::_thesis: dom (x -tree T) = ^ (dom T)
 ( dom (x -tree <*T*>) = tree (doms <*T*>) & doms <*T*> = <*(dom T)*> ) by Th10, FINSEQ_3:132;
hence  dom (x -tree T) = ^ (dom T) by TREES_3:def_16; ::_thesis: verum
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
let x be set ; ::_thesis: for T1, T2 being DecoratedTree holds dom (x -tree (T1,T2)) = tree ((dom T1),(dom T2))
let T1, T2 be DecoratedTree; ::_thesis: dom (x -tree (T1,T2)) = tree ((dom T1),(dom T2))
 ( dom (x -tree <*T1,T2*>) = tree (doms <*T1,T2*>) & doms <*T1,T2*> = <*(dom T1),(dom T2)*> ) by Th10, FINSEQ_3:133;
hence  dom (x -tree (T1,T2)) = tree ((dom T1),(dom T2)) by TREES_3:def_17; ::_thesis: verum
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
let x, y be set ; ::_thesis: for p, q being DTree-yielding FinSequence st x -tree p = y -tree q holds
( x = y & p = q )
let p, q be DTree-yielding FinSequence; ::_thesis: ( x -tree p = y -tree q implies ( x = y & p = q ) )
assume A1: x -tree p = y -tree q ; ::_thesis: ( x = y & p = q )
 (x -tree p) . {} = x by Def4;
hence  x = y by A1, Def4; ::_thesis: p = q
 ( dom (x -tree p) = tree (doms p) & dom (y -tree q) = tree (doms q) ) by Th10;
then A2: doms p = doms q by A1, TREES_3:50;
 ( dom p = dom (doms p) & dom (doms q) = dom q ) by TREES_3:37;
then A3: len p = len q by A2, FINSEQ_3:29;
now__::_thesis:_for_i_being_Nat_st_i_>=_1_&_i_<=_len_p_holds_
p_._i_=_q_._i
let i be Nat; ::_thesis: ( i >= 1 & i <= len p implies p . i = q . i )
assume that
A4: i >= 1 and
A5: i <= len p ; ::_thesis: p . i = q . i
consider n being Nat such that
A6: i = 1 + n by A4, NAT_1:10;
reconsider n = n as Element of NAT by ORDINAL1:def_12;
A7: n < len p by A5, A6, NAT_1:13;
then  p . i = (x -tree p) | <*n*> by A6, Def4;
hence  p . i = q . i by A1, A3, A6, A7, Def4; ::_thesis: verum
end;
hence  p = q by A3, FINSEQ_1:14; ::_thesis: verum
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
let x, y be set ; ::_thesis: for p being FinSequence st root-tree x = y -flat_tree p holds
( x = y & p = {} )
let p be FinSequence; ::_thesis: ( root-tree x = y -flat_tree p implies ( x = y & p = {} ) )
assume A1: root-tree x = y -flat_tree p ; ::_thesis: ( x = y & p = {} )
thus x = (root-tree x) . {} by Th3
.= y by A1, Def3 ; ::_thesis: p = {}
 dom (y -flat_tree p) = elementary_tree (len p) by Def3;
hence  p = {} by A1, Th2, Th3; ::_thesis: verum
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
let x, y be set ; ::_thesis: for p being FinSequence st root-tree x = y -tree p & p is DTree-yielding holds
( x = y & p = {} )
let p be FinSequence; ::_thesis: ( root-tree x = y -tree p & p is DTree-yielding implies ( x = y & p = {} ) )
assume that
A1: root-tree x = y -tree p and
A2: p is DTree-yielding ; ::_thesis: ( x = y & p = {} )
reconsider p9 = p as DTree-yielding FinSequence by A2;
thus x = (root-tree x) . {} by Th3
.= y by A1, A2, Def4 ; ::_thesis: p = {}
A3: dom (y -tree p) = tree (doms p9) by Th10;
then A4: doms p = {} by A1, Th3, TREES_3:50, TREES_3:52;
 dom (doms p) = dom p by A3, TREES_3:37;
hence  p = {} by A4; ::_thesis: verum
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
let x, y be set ; ::_thesis: 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) ) )
let p, q be FinSequence; ::_thesis: ( x -flat_tree p = y -tree q & q is DTree-yielding implies ( x = y & len p = len q & ( for i being Element of NAT st i in dom p holds
q . i = root-tree (p . i) ) ) )
assume that
A1: x -flat_tree p = y -tree q and
A2: q is DTree-yielding ; ::_thesis: ( x = y & len p = len q & ( for i being Element of NAT st i in dom p holds
q . i = root-tree (p . i) ) )
reconsider q9 = q as DTree-yielding FinSequence by A2;
thus x = (x -flat_tree p) . {} by Def3
.= y by A1, A2, Def4 ; ::_thesis: ( len p = len q & ( for i being Element of NAT st i in dom p holds
q . i = root-tree (p . i) ) )
tree ((len p) |-> (elementary_tree 0)) = elementary_tree (len p) by TREES_3:54
.= dom (x -flat_tree p) by Def3
.= tree (doms q9) by A1, Th10 ;
then A3: (len p) |-> (elementary_tree 0) = doms q9 by TREES_3:50;
 len (doms q9) = len q by TREES_3:38;
hence A4: len p = len q by A3, CARD_1:def_7; ::_thesis: for i being Element of NAT st i in dom p holds
q . i = root-tree (p . i)
let i be Element of NAT ; ::_thesis: ( i in dom p implies q . i = root-tree (p . i) )
assume A5: i in dom p ; ::_thesis: q . i = root-tree (p . i)
then A6: i >= 1 by FINSEQ_3:25;
A7: i <= len p by A5, FINSEQ_3:25;
consider n being Nat such that
A8: i = 1 + n by A6, NAT_1:10;
reconsider n = n as Element of NAT by ORDINAL1:def_12;
A9: n < len p by A7, A8, NAT_1:13;
then  (x -flat_tree p) | <*n*> = root-tree (p . i) by A8, Th9;
hence  q . i = root-tree (p . i) by A1, A2, A4, A8, A9, Def4; ::_thesis: verum
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
let x be set ; ::_thesis: 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)
let p be DTree-yielding FinSequence; ::_thesis: 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)
let n be Element of NAT ; ::_thesis: for q being FinSequence st <*n*> ^ q in dom (x -tree p) holds
(x -tree p) . (<*n*> ^ q) = p .. ((n + 1),q)
let q be FinSequence; ::_thesis: ( <*n*> ^ q in dom (x -tree p) implies (x -tree p) . (<*n*> ^ q) = p .. ((n + 1),q) )
assume A1: <*n*> ^ q in dom (x -tree p) ; ::_thesis: (x -tree p) . (<*n*> ^ q) = p .. ((n + 1),q)
then  <*n*> ^ q is Node of (x -tree p) ;
then reconsider q9 = q as FinSequence of NAT by FINSEQ_1:36;
A2: <*n*> in dom (x -tree p) by A1, TREES_1:21;
A3: <*n*> ^ q in tree (doms p) by A1, Th10;
A4: len (doms p) = len p by TREES_3:38;
A5: q9 in (dom (x -tree p)) | <*n*> by A1, A2, TREES_1:def_6;
A6: n < len p by A3, A4, TREES_3:48;
A7: ( dom ((x -tree p) | <*n*>) = (dom (x -tree p)) | <*n*> & ((x -tree p) | <*n*>) . q9 = (x -tree p) . (<*n*> ^ q) ) by A5, TREES_2:def_10;
 ( n + 1 in dom p & p . (n + 1) = (x -tree p) | <*n*> ) by A6, Def4, Lm2;
hence  (x -tree p) . (<*n*> ^ q) = p .. ((n + 1),q) by A5, A7, FUNCT_5:38; ::_thesis: verum
end;

theorem :: TREES_4:20
for x being set holds
( x -flat_tree {} = root-tree x & x -tree {} = root-tree x )
proof
let x be set ; ::_thesis: ( x -flat_tree {} = root-tree x & x -tree {} = root-tree x )
 len {} = 0 ;
then A1: dom (x -flat_tree {}) = elementary_tree 0 by Def3;
now__::_thesis:_for_y_being_set_st_y_in_elementary_tree_0_holds_
(x_-flat_tree_{})_._y_=_x
let y be set ; ::_thesis: ( y in elementary_tree 0 implies (x -flat_tree {}) . y = x )
assume  y in elementary_tree 0 ; ::_thesis: (x -flat_tree {}) . y = x
then  y = {} by TARSKI:def_1, TREES_1:29;
hence  (x -flat_tree {}) . y = x by Def3; ::_thesis: verum
end;
hence  x -flat_tree {} = root-tree x by A1, FUNCOP_1:11; ::_thesis: x -tree {} = root-tree x
reconsider e = {} as DTree-yielding FinSequence ;
A2: dom (x -tree {}) = tree (doms e) by Th10
.= elementary_tree 0 by FUNCT_6:23, TREES_3:52 ;
now__::_thesis:_for_y_being_set_st_y_in_elementary_tree_0_holds_
(x_-tree_e)_._y_=_x
let y be set ; ::_thesis: ( y in elementary_tree 0 implies (x -tree e) . y = x )
assume  y in elementary_tree 0 ; ::_thesis: (x -tree e) . y = x
then  y = {} by TARSKI:def_1, TREES_1:29;
hence  (x -tree e) . y = x by Def4; ::_thesis: verum
end;
hence  x -tree {} = root-tree x by A2, FUNCOP_1:11; ::_thesis: verum
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
let x, y be set ; ::_thesis: x -flat_tree <*y*> = ((elementary_tree 1) --> x) with-replacement (<*0*>,(root-tree y))
set T = ((elementary_tree 1) --> x) with-replacement (<*0*>,(root-tree y));
A1: dom (x -flat_tree <*y*>) = elementary_tree (len <*y*>) by Def3
.= elementary_tree 1 by FINSEQ_1:40 ;
A2: dom (root-tree y) = elementary_tree 0 by FUNCOP_1:13;
A3: ( dom ((elementary_tree 1) --> x) = elementary_tree 1 & <*0*> in elementary_tree 1 ) by FUNCOP_1:13, TARSKI:def_2, TREES_1:51;
then A4: dom (((elementary_tree 1) --> x) with-replacement (<*0*>,(root-tree y))) = (elementary_tree 1) with-replacement (<*0*>,(elementary_tree 0)) by A2, TREES_2:def_11
.= elementary_tree 1 by TREES_3:58, TREES_3:67 ;
now__::_thesis:_for_z_being_set_st_z_in_elementary_tree_1_holds_
(((elementary_tree_1)_-->_x)_with-replacement_(<*0*>,(root-tree_y)))_._z_=_(x_-flat_tree_<*y*>)_._z
let z be set ; ::_thesis: ( z in elementary_tree 1 implies (((elementary_tree 1) --> x) with-replacement (<*0*>,(root-tree y))) . z = (x -flat_tree <*y*>) . z )
assume  z in elementary_tree 1 ; ::_thesis: (((elementary_tree 1) --> x) with-replacement (<*0*>,(root-tree y))) . z = (x -flat_tree <*y*>) . z
then A5: ( z = {} or z = <*0*> ) by TARSKI:def_2, TREES_1:51;
A6: {} in elementary_tree 1 by TARSKI:def_2, TREES_1:51;
A7: not <*0*> is_a_prefix_of {} ;
A8: len <*y*> = 1 by FINSEQ_1:40;
A9: ( <*y*> . 1 = y & (x -flat_tree <*y*>) . {} = x ) by Def3, FINSEQ_1:40;
A10: (((elementary_tree 1) --> x) with-replacement (<*0*>,(root-tree y))) . {} = ((elementary_tree 1) --> x) . {} by A3, A6, A7, TREES_3:45;
A11: (x -flat_tree <*y*>) . <*0*> = <*y*> . (0 + 1) by A8, Def3;
 (((elementary_tree 1) --> x) with-replacement (<*0*>,(root-tree y))) . <*0*> = (root-tree y) . {} by A3, TREES_3:44;
hence  (((elementary_tree 1) --> x) with-replacement (<*0*>,(root-tree y))) . z = (x -flat_tree <*y*>) . z by A5, A6, A9, A10, A11, Th3, FUNCOP_1:7; ::_thesis: verum
end;
hence  x -flat_tree <*y*> = ((elementary_tree 1) --> x) with-replacement (<*0*>,(root-tree y)) by A1, A4, FUNCT_1:2; ::_thesis: verum
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
let x be set ; ::_thesis: for T being DecoratedTree holds x -tree <*T*> = ((elementary_tree 1) --> x) with-replacement (<*0*>,T)
let T be DecoratedTree; ::_thesis: x -tree <*T*> = ((elementary_tree 1) --> x) with-replacement (<*0*>,T)
set D = ((elementary_tree 1) --> x) with-replacement (<*0*>,T);
set W = (elementary_tree 1) with-replacement (<*0*>,(dom T));
A1: dom (x -tree <*T*>) = tree (doms <*T*>) by Th10
.= tree <*(dom T)*> by FINSEQ_3:132
.= ^ (dom T) by TREES_3:def_16
.= (elementary_tree 1) with-replacement (<*0*>,(dom T)) by TREES_3:58 ;
A2: dom ((elementary_tree 1) --> x) = elementary_tree 1 by FUNCOP_1:13;
reconsider t1 = {} , t2 = <*0*> as Element of elementary_tree 1 by TARSKI:def_2, TREES_1:51;
 t2 = t2 ;
then A3: dom (((elementary_tree 1) --> x) with-replacement (<*0*>,T)) = (elementary_tree 1) with-replacement (<*0*>,(dom T)) by A2, TREES_2:def_11;
A4: {} in dom T by TREES_1:22;
now__::_thesis:_for_y_being_set_st_y_in_(elementary_tree_1)_with-replacement_(<*0*>,(dom_T))_holds_
(((elementary_tree_1)_-->_x)_with-replacement_(<*0*>,T))_._y_=_(x_-tree_<*T*>)_._y
let y be set ; ::_thesis: ( y in (elementary_tree 1) with-replacement (<*0*>,(dom T)) implies (((elementary_tree 1) --> x) with-replacement (<*0*>,T)) . y = (x -tree <*T*>) . y )
assume  y in (elementary_tree 1) with-replacement (<*0*>,(dom T)) ; ::_thesis: (((elementary_tree 1) --> x) with-replacement (<*0*>,T)) . y = (x -tree <*T*>) . y
then reconsider q = y as Element of (elementary_tree 1) with-replacement (<*0*>,(dom T)) ;
 ( q in elementary_tree 1 or ex v being FinSequence of NAT st
( v in dom T & q = t2 ^ v ) ) by TREES_1:def_9;
then A5: ( q = {} or ( q = t2 & t2 = t2 ^ t1 ) or ex v being FinSequence of NAT st
( v in dom T & q = <*0*> ^ v ) ) by FINSEQ_1:34, TARSKI:def_2, TREES_1:51;
 not t2 is_a_prefix_of t1 ;
then A6: (((elementary_tree 1) --> x) with-replacement (<*0*>,T)) . {} = ((elementary_tree 1) --> x) . t1 by A2, TREES_3:45
.= x by FUNCOP_1:7
.= (x -tree <*T*>) . {} by Def4 ;
now__::_thesis:_(_ex_r_being_FinSequence_of_NAT_st_
(_r_in_dom_T_&_q_=_<*0*>_^_r_)_implies_(((elementary_tree_1)_-->_x)_with-replacement_(<*0*>,T))_._q_=_(x_-tree_<*T*>)_._q_)
given r being FinSequence of NAT  such that A7: r in dom T and
A8: q = <*0*> ^ r ; ::_thesis: (((elementary_tree 1) --> x) with-replacement (<*0*>,T)) . q = (x -tree <*T*>) . q
reconsider r = r as Node of T by A7;
 q = t2 ^ r by A8;
then A9: (((elementary_tree 1) --> x) with-replacement (<*0*>,T)) . q = T . r by A2, TREES_3:46;
 ( len <*T*> = 1 & <*T*> . (0 + 1) = T ) by FINSEQ_1:40;
then A10: (x -tree <*T*>) | t2 = T by Def4;
 ((elementary_tree 1) with-replacement (<*0*>,(dom T))) | t2 = dom T by TREES_1:33;
hence  (((elementary_tree 1) --> x) with-replacement (<*0*>,T)) . q = (x -tree <*T*>) . q by A1, A8, A9, A10, TREES_2:def_10; ::_thesis: verum
end;
hence  (((elementary_tree 1) --> x) with-replacement (<*0*>,T)) . y = (x -tree <*T*>) . y by A4, A5, A6; ::_thesis: verum
end;
hence  x -tree <*T*> = ((elementary_tree 1) --> x) with-replacement (<*0*>,T) by A1, A3, FUNCT_1:2; ::_thesis: verum
end;

registration
let D be non empty set ;
let d be Element of D;
let p be FinSequence of D;
clusterd -flat_tree p -> D -valued ;
coherence
 d -flat_tree p is D -valued
proof
set T = d -flat_tree p;
 rng (d -flat_tree p) c= D
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (d -flat_tree p) or x in D )
assume  x in rng (d -flat_tree p) ; ::_thesis: x in D
then consider y being set  such that
A1: y in dom (d -flat_tree p) and
A2: x = (d -flat_tree p) . y by FUNCT_1:def_3;
reconsider y = y as Node of (d -flat_tree p) by A1;
A3: dom (d -flat_tree p) = elementary_tree (len p) by Def3;
A4: (d -flat_tree p) . {} = d by Def3;
now__::_thesis:_(_y_<>_{}_implies_x_in_D_)
assume  y <> {} ; ::_thesis: x in D
then consider n being Element of NAT  such that
A5: ( n < len p & y = <*n*> ) by A3, TREES_1:30;
A6: ( (d -flat_tree p) . y = p . (n + 1) & p . (n + 1) in rng p ) by A5, Def3, Lm2;
 rng p c= D by FINSEQ_1:def_4;
hence  x in D by A2, A6; ::_thesis: verum
end;
hence  x in D by A2, A4; ::_thesis: verum
end;
hence  d -flat_tree p is D -valued by RELAT_1:def_19; ::_thesis: verum
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;
clusterd -tree p -> D -valued ;
coherence
 d -tree p is D -valued
proof
set T = d -tree p;
 rng (d -tree p) c= D
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (d -tree p) or x in D )
assume  x in rng (d -tree p) ; ::_thesis: x in D
then consider y being set  such that
A1: y in dom (d -tree p) and
A2: x = (d -tree p) . y by FUNCT_1:def_3;
reconsider y = y as Node of (d -tree p) by A1;
A3: (tree (doms p)) -level 1 =  {  <*n*> where n is Element of NAT : n < len (doms p)  }  by TREES_3:49;
A4: (d -tree p) . {} = d by Def4;
A5: ( tree (doms p) = dom (d -tree p) & len (doms p) = len p ) by Th10, TREES_3:38;
now__::_thesis:_(_y_<>_{}_implies_x_in_D_)
assume  y <> {} ; ::_thesis: x in D
then consider q being FinSequence of NAT , n being Element of NAT  such that
A6: y = <*n*> ^ q by FINSEQ_2:130;
A7: <*n*> in dom (d -tree p) by A6, TREES_1:21;
A8: len <*n*> = 1 by FINSEQ_1:40;
A9: q in (dom (d -tree p)) | <*n*> by A6, A7, TREES_1:def_6;
A10: <*n*> in (dom (d -tree p)) -level 1 by A7, A8;
A11: dom ((d -tree p) | <*n*>) = (dom (d -tree p)) | <*n*> by TREES_2:def_10;
consider i being Element of NAT  such that
A12: ( <*n*> = <*i*> & i < len p ) by A3, A5, A10;
A13: ( <*n*> . 1 = n & <*i*> . 1 = i ) by FINSEQ_1:40;
then A14: (d -tree p) | <*n*> = p . (n + 1) by A12, Def4;
A15: p . (n + 1) in rng p by A12, A13, Lm2;
 rng p c= F by FINSEQ_1:def_4;
then reconsider t = p . (n + 1) as Element of F by A15;
A16: t . q = x by A2, A6, A9, A14, TREES_2:def_10;
A17: t . q in rng t by A9, A11, A14, FUNCT_1:def_3;
 rng t c= D by RELAT_1:def_19;
hence  x in D by A16, A17; ::_thesis: verum
end;
hence  x in D by A2, A4; ::_thesis: verum
end;
hence  d -tree p is D -valued by RELAT_1:def_19; ::_thesis: verum
end;
end;

registration
let D be non empty set ;
let d be Element of D;
let T be DecoratedTree of D;
clusterd -tree T -> D -valued ;
coherence
 d -tree T is D -valued
proof
reconsider T = T as Element of Trees D by TREES_3:def_7;
reconsider t = <*T*> as Element of (Trees D) * by FINSEQ_1:def_11;
 d -tree T = d -tree t ;
hence  d -tree T is D -valued ; ::_thesis: verum
end;
end;

registration
let D be non empty set ;
let d be Element of D;
let T1, T2 be DecoratedTree of D;
clusterd -tree (T1,T2) -> D -valued ;
coherence
 d -tree (T1,T2) is D -valued
proof
reconsider T1 = T1, T2 = T2 as Element of Trees D by TREES_3:def_7;
 <*T1,T2*> = <*T1*> ^ <*T2*> ;
then reconsider t = <*T1,T2*> as Element of (Trees D) * by FINSEQ_1:def_11;
 d -tree (T1,T2) = d -tree t ;
hence  d -tree (T1,T2) is D -valued ; ::_thesis: verum
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
A1: dom (doms p) = dom p by TREES_3:37;
A2: rng p c= FinTrees D by FINSEQ_1:def_4;
thus  doms p is FinSequence of FinTrees ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3,FINSEQ_1:def_4 ::_thesis: ( not x in rng (doms p) or x in FinTrees )
assume  x in rng (doms p) ; ::_thesis: x in FinTrees
then consider y being set  such that
A3: y in dom p and
A4: x = (doms p) . y by A1, FUNCT_1:def_3;
reconsider T = p . y as DecoratedTree by A3, TREES_3:24;
 T in rng p by A3, FUNCT_1:def_3;
then  dom T in FinTrees by A2, TREES_3:def_2;
hence  x in FinTrees by A3, A4, FUNCT_6:22; ::_thesis: verum
end;
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 funcd -tree p ->  Element of FinTrees D;
coherence
 d -tree p is Element of FinTrees D
proof
 dom (d -tree p) = tree (doms p) by Th10;
hence  d -tree p is Element of FinTrees D by TREES_3:def_8; ::_thesis: verum
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
let p be FinSequence of x; ::_thesis: p is FinSequence of D
 rng p c= x by FINSEQ_1:def_4;
hence  rng p c= D by XBOOLE_1:1; :: according to FINSEQ_1:def_4 ::_thesis: verum
end;
end;

registration
let D be non empty constituted-DTrees set ;
let X be Subset of D;
cluster  ->  DTree-yielding for 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
defpred S1[ set ] means ( $1 in F1() or ex q being Element of F1() ex r being Element of F2() st
( P1[q] & $1 = q ^ r ) );
consider T being set  such that
A1: for x being set holds
( x in T iff ( x in NAT * & S1[x] ) ) from XBOOLE_0:sch_1();
set t = the Element of F1();
 the Element of F1() in NAT * by FINSEQ_1:def_11;
then reconsider T = T as non empty set by A1;
 T is Tree-like
proof
thus  T c= NAT * :: according to TREES_1:def_3 ::_thesis: ( ( for b1 being FinSequence of NAT holds
( not b1 in T or ProperPrefixes b1 c= T ) ) & ( for b1 being FinSequence of NAT
for b2, b3 being Element of NAT holds
( not b1 ^ <*b2*> in T or not b3 <= b2 or b1 ^ <*b3*> in T ) ) )
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in T or x in NAT * )
thus  ( not x in T or x in NAT * ) by A1; ::_thesis: verum
end;
thus  for p being FinSequence of NAT st p in T holds
ProperPrefixes p c= T ::_thesis: for b1 being FinSequence of NAT
for b2, b3 being Element of NAT holds
( not b1 ^ <*b2*> in T or not b3 <= b2 or b1 ^ <*b3*> in T )
proof
let p be FinSequence of NAT ; ::_thesis: ( p in T implies ProperPrefixes p c= T )
assume A2: p in T ; ::_thesis: ProperPrefixes p c= T
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ProperPrefixes p or x in T )
assume  x in ProperPrefixes p ; ::_thesis: x in T
then consider q being FinSequence such that
A3: x = q and
A4: q is_a_proper_prefix_of p by TREES_1:def_2;
assume A5: not x in T ; ::_thesis: contradiction
 q is_a_prefix_of p by A4, XBOOLE_0:def_8;
then consider r being FinSequence such that
A6: p = q ^ r by TREES_1:1;
reconsider q = q, r = r as FinSequence of NAT by A6, FINSEQ_1:36;
 ( ( q ^ r in F1() & q in NAT * & ( q ^ r in F1() implies q in F1() ) ) or ex q being Element of F1() ex r being Element of F2() st
( P1[q] & p = q ^ r ) ) by A1, A2, A6, FINSEQ_1:def_11, TREES_1:21;
then consider q9 being Element of F1(), r9 being Element of F2() such that
A7: P1[q9] and
A8: q ^ r = q9 ^ r9 by A1, A3, A5, A6;
now__::_thesis:_not_len_q_<=_len_q9
assume  len q <= len q9 ; ::_thesis: contradiction
then  ex s being FinSequence st q ^ s = q9 by A8, FINSEQ_1:47;
then A9: q in F1() by TREES_1:21;
 q in NAT * by FINSEQ_1:def_11;
hence  contradiction by A1, A3, A5, A9; ::_thesis: verum
end;
then consider s being FinSequence such that
A10: q9 ^ s = q by A8, FINSEQ_1:47;
reconsider s = s as FinSequence of NAT by A10, FINSEQ_1:36;
 q9 ^ r9 = q9 ^ (s ^ r) by A8, A10, FINSEQ_1:32;
then  s ^ r = r9 by FINSEQ_1:33;
then  ( q in NAT * & s is Element of F2() ) by FINSEQ_1:def_11, TREES_1:21;
hence  contradiction by A1, A3, A5, A7, A10; ::_thesis: verum
end;
let p be FinSequence of NAT ; ::_thesis: for b1, b2 being Element of NAT holds
( not p ^ <*b1*> in T or not b2 <= b1 or p ^ <*b2*> in T )
let k, n be Element of NAT ; ::_thesis: ( not p ^ <*k*> in T or not n <= k or p ^ <*n*> in T )
assume that
A11: p ^ <*k*> in T and
A12: n <= k ; ::_thesis: p ^ <*n*> in T
A13: now__::_thesis:_(_p_^_<*k*>_in_F1()_implies_p_^_<*n*>_in_T_)
assume  p ^ <*k*> in F1() ; ::_thesis: p ^ <*n*> in T
then A14: p ^ <*n*> in F1() by A12, TREES_1:def_3;
 p ^ <*n*> in NAT * by FINSEQ_1:def_11;
hence  p ^ <*n*> in T by A1, A14; ::_thesis: verum
end;
now__::_thesis:_(_not_p_^_<*k*>_in_F1()_implies_p_^_<*n*>_in_T_)
assume A15: not p ^ <*k*> in F1() ; ::_thesis: p ^ <*n*> in T
then consider q being Element of F1(), r being Element of F2() such that
A16: P1[q] and
A17: p ^ <*k*> = q ^ r by A1, A11;
 q ^ {} = q by FINSEQ_1:34;
then  r <> {} by A15, A17;
then consider w being FinSequence, z being set  such that
A18: r = w ^ <*z*> by FINSEQ_1:46;
reconsider w = w as FinSequence of NAT by A18, FINSEQ_1:36;
A19: p ^ <*k*> = (q ^ w) ^ <*z*> by A17, A18, FINSEQ_1:32;
A20: ( (p ^ <*k*>) . ((len p) + 1) = k & ((q ^ w) ^ <*z*>) . ((len (q ^ w)) + 1) = z ) by FINSEQ_1:42;
A21: ( len <*k*> = 1 & len <*z*> = 1 ) by FINSEQ_1:40;
A22: ( len (p ^ <*k*>) = (len p) + (len <*k*>) & len ((q ^ w) ^ <*z*>) = (len (q ^ w)) + (len <*z*>) ) by FINSEQ_1:22;
then A23: p = q ^ w by A19, A20, A21, FINSEQ_1:33;
A24: w ^ <*n*> in F2() by A12, A18, A19, A20, A21, A22, TREES_1:def_3;
A25: p ^ <*n*> = q ^ (w ^ <*n*>) by A23, FINSEQ_1:32;
 p ^ <*n*> in NAT * by FINSEQ_1:def_11;
hence  p ^ <*n*> in T by A1, A16, A24, A25; ::_thesis: verum
end;
hence  p ^ <*n*> in T by A13; ::_thesis: verum
end;
then reconsider T = T as Tree ;
take  T ; ::_thesis: 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 ) ) )
let p be FinSequence; ::_thesis: ( 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 ) ) )
 ( ( p is Element of F1() or ex q being Element of F1() ex r being Element of F2() st
( P1[q] & p = q ^ r ) ) implies p in NAT * ) by FINSEQ_1:def_11;
hence  ( 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 ) ) ) by A1; ::_thesis: verum
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
defpred S1[ set ] means ( $1 in Leaves (dom T) & T . $1 = x );
consider W being Tree such that
A1: for p being FinSequence holds
( p in W iff ( p in dom T or ex q being Node of T ex r being Node of T9 st
( S1[q] & p = q ^ r ) ) ) from TREES_4:sch_1();
defpred S2[ set , set ] means ( ( $1 is Node of T & ( not $1 in Leaves (dom T) or T . $1 <> x ) & $2 = T . $1 ) or ex p being Node of T ex q being Node of T9 st
( $1 = p ^ q & p in Leaves (dom T) & T . p = x & $2 = T9 . q ) );
A2: for z being set st z in W holds
ex y being set st S2[z,y]
proof
let z be set ; ::_thesis: ( z in W implies ex y being set st S2[z,y] )
assume  z in W ; ::_thesis: ex y being set st S2[z,y]
then reconsider w = z as Element of W ;
A3: now__::_thesis:_(_ex_q_being_Node_of_T_ex_r_being_Node_of_T9_st_
(_q_in_Leaves_(dom_T)_&_T_._q_=_x_&_w_=_q_^_r_)_implies_ex_y_being_set_ex_q_being_Node_of_T_ex_r_being_Node_of_T9_st_
(_z_=_q_^_r_&_q_in_Leaves_(dom_T)_&_T_._q_=_x_&_y_=_T9_._r_)_)
given q being Node of T, r being Node of T9 such that A4: ( q in Leaves (dom T) & T . q = x & w = q ^ r ) ; ::_thesis: ex y being set ex q being Node of T ex r being Node of T9 st
( z = q ^ r & q in Leaves (dom T) & T . q = x & y = T9 . r )
take y = T9 . r; ::_thesis: ex q being Node of T ex r being Node of T9 st
( z = q ^ r & q in Leaves (dom T) & T . q = x & y = T9 . r )
take q = q; ::_thesis: ex r being Node of T9 st
( z = q ^ r & q in Leaves (dom T) & T . q = x & y = T9 . r )
take r = r; ::_thesis: ( z = q ^ r & q in Leaves (dom T) & T . q = x & y = T9 . r )
thus  ( z = q ^ r & q in Leaves (dom T) & T . q = x & y = T9 . r ) by A4; ::_thesis: verum
end;
now__::_thesis:_(_(_for_q_being_Node_of_T
for_r_being_Node_of_T9_holds_
(_not_q_in_Leaves_(dom_T)_or_not_T_._q_=_x_or_not_w_=_q_^_r_)_)_implies_ex_y_being_set_st_
(_z_is_Node_of_T_&_(_not_z_in_Leaves_(dom_T)_or_T_._z_<>_x_)_&_y_=_T_._z_)_)
assume A5: for q being Node of T
for r being Node of T9 holds
( not q in Leaves (dom T) or not T . q = x or not w = q ^ r ) ; ::_thesis: ex y being set st
( z is Node of T & ( not z in Leaves (dom T) or T . z <> x ) & y = T . z )
take y = T . z; ::_thesis: ( z is Node of T & ( not z in Leaves (dom T) or T . z <> x ) & y = T . z )
thus  z is Node of T by A1, A5; ::_thesis: ( ( not z in Leaves (dom T) or T . z <> x ) & y = T . z )
reconsider w = w as Node of T by A1, A5;
reconsider e = {} as Node of T9 by TREES_1:22;
 w ^ e = w by FINSEQ_1:34;
hence  ( ( not z in Leaves (dom T) or T . z <> x ) & y = T . z ) by A5; ::_thesis: verum
end;
hence  ex y being set st S2[z,y] by A3; ::_thesis: verum
end;
consider f being Function such that
A6: ( dom f = W & ( for z being set st z in W holds
S2[z,f . z] ) ) from CLASSES1:sch_1(A2);
reconsider f = f as DecoratedTree by A6, TREES_2:def_8;
take  f ; ::_thesis: ( ( for p being FinSequence holds
( p in dom f 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
f . 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
f . (p ^ q) = T9 . q ) )
thus  for p being FinSequence holds
( p in dom f 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 ) ) ) by A1, A6; ::_thesis: ( ( for p being Node of T st ( not p in Leaves (dom T) or T . p <> x ) holds
f . 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
f . (p ^ q) = T9 . q ) )
thus  for p being Node of T st ( not p in Leaves (dom T) or T . p <> x ) holds
f . p = T . p ::_thesis: for p being Node of T
for q being Node of T9 st p in Leaves (dom T) & T . p = x holds
f . (p ^ q) = T9 . q
proof
let p be Node of T; ::_thesis: ( ( not p in Leaves (dom T) or T . p <> x ) implies f . p = T . p )
assume A7: ( not p in Leaves (dom T) or T . p <> x ) ; ::_thesis: f . p = T . p
A8: p in W by A1;
now__::_thesis:_for_p9_being_Node_of_T
for_q_being_Node_of_T9_holds_
(_not_p_=_p9_^_q_or_not_p9_in_Leaves_(dom_T)_or_not_T_._p9_=_x_or_not_f_._p_=_T9_._q_)
given p9 being Node of T, q being Node of T9 such that A9: p = p9 ^ q and
A10: p9 in Leaves (dom T) and
A11: T . p9 = x and
 f . p = T9 . q ; ::_thesis: contradiction
 ( p9 is_a_prefix_of p & not p9 is_a_proper_prefix_of p ) by A9, A10, TREES_1:1, TREES_1:def_5;
hence  contradiction by A7, A10, A11, XBOOLE_0:def_8; ::_thesis: verum
end;
hence  f . p = T . p by A6, A8; ::_thesis: verum
end;
let p be Node of T; ::_thesis: for q being Node of T9 st p in Leaves (dom T) & T . p = x holds
f . (p ^ q) = T9 . q
let q be Node of T9; ::_thesis: ( p in Leaves (dom T) & T . p = x implies f . (p ^ q) = T9 . q )
assume that
A12: p in Leaves (dom T) and
A13: T . p = x ; ::_thesis: f . (p ^ q) = T9 . q
A14: p ^ q in W by A1, A12, A13;
now__::_thesis:_(_p_^_q_is_Node_of_T_implies_p_=_p_^_q_)
assume  p ^ q is Node of T ; ::_thesis: p = p ^ q
then A15: not p is_a_proper_prefix_of p ^ q by A12, TREES_1:def_5;
 p is_a_prefix_of p ^ q by TREES_1:1;
hence  p = p ^ q by A15, XBOOLE_0:def_8; ::_thesis: verum
end;
then consider p9 being Node of T, q9 being Node of T9 such that
A16: p ^ q = p9 ^ q9 and
A17: p9 in Leaves (dom T) and
 T . p9 = x and
A18: f . (p ^ q) = T9 . q9 by A6, A12, A13, A14;
now__::_thesis:_for_p,_p9,_q,_q9_being_FinSequence_of_NAT_
for_T_being_Tree_st_p_^_q_=_p9_^_q9_&_p_in_Leaves_T_&_p9_in_Leaves_T_holds_
not_p_<>_p9
let p, p9, q, q9 be FinSequence of NAT ; ::_thesis: for T being Tree st p ^ q = p9 ^ q9 & p in Leaves T & p9 in Leaves T holds
not p <> p9
let T be Tree; ::_thesis: ( p ^ q = p9 ^ q9 & p in Leaves T & p9 in Leaves T implies not p <> p9 )
assume that
A19: p ^ q = p9 ^ q9 and
A20: ( p in Leaves T & p9 in Leaves T ) and
A21: p <> p9 ; ::_thesis: contradiction
now__::_thesis:_not_len_p_<=_len_p9
assume  len p <= len p9 ; ::_thesis: contradiction
then  ex r being FinSequence st p ^ r = p9 by A19, FINSEQ_1:47;
then  p is_a_prefix_of p9 by TREES_1:1;
then  p is_a_proper_prefix_of p9 by A21, XBOOLE_0:def_8;
hence  contradiction by A20, TREES_1:def_5; ::_thesis: verum
end;
then  ex r being FinSequence st p9 ^ r = p by A19, FINSEQ_1:47;
then  p9 is_a_prefix_of p by TREES_1:1;
then  p9 is_a_proper_prefix_of p by A21, XBOOLE_0:def_8;
hence  contradiction by A20, TREES_1:def_5; ::_thesis: verum
end;
then  p = p9 by A12, A16, A17;
hence  f . (p ^ q) = T9 . q by A16, A18, FINSEQ_1:33; ::_thesis: verum
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
let T1, T2 be DecoratedTree; ::_thesis: ( ( for p being FinSequence holds
( p in dom T1 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
T1 . 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
T1 . (p ^ q) = T9 . q ) & ( for p being FinSequence holds
( p in dom T2 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
T2 . 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
T2 . (p ^ q) = T9 . q ) implies T1 = T2 )
assume that
A22: for p being FinSequence holds
( p in dom T1 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 ) ) ) and
A23: for p being Node of T st ( not p in Leaves (dom T) or T . p <> x ) holds
T1 . p = T . p and
A24: for p being Node of T
for q being Node of T9 st p in Leaves (dom T) & T . p = x holds
T1 . (p ^ q) = T9 . q and
A25: for p being FinSequence holds
( p in dom T2 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 ) ) ) and
A26: for p being Node of T st ( not p in Leaves (dom T) or T . p <> x ) holds
T2 . p = T . p and
A27: for p being Node of T
for q being Node of T9 st p in Leaves (dom T) & T . p = x holds
T2 . (p ^ q) = T9 . q ; ::_thesis: T1 = T2
A28: dom T1 = dom T2
proof
let p be FinSequence of NAT ; :: according to TREES_2:def_1 ::_thesis: ( ( not p in dom T1 or p in dom T2 ) & ( not p in dom T2 or p in dom T1 ) )
 ( p in dom T1 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 ) ) ) by A22;
hence  ( ( not p in dom T1 or p in dom T2 ) & ( not p in dom T2 or p in dom T1 ) ) by A25; ::_thesis: verum
end;
reconsider p9 = {} as Node of T9 by TREES_1:22;
now__::_thesis:_for_y_being_set_st_y_in_dom_T1_holds_
T1_._y_=_T2_._y
let y be set ; ::_thesis: ( y in dom T1 implies T1 . b1 = T2 . b1 )
assume  y in dom T1 ; ::_thesis: T1 . b1 = T2 . b1
then reconsider p = y as Node of T1 ;
percases ( 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 ) ) by A22;
suppose p in dom T ; ::_thesis: T1 . b1 = T2 . b1
then reconsider p = p as Node of T ;
hereby  ::_thesis: verum
percases ( ( p in Leaves (dom T) & T . p = x ) or not p in Leaves (dom T) or T . p <> x ) ;
supposeA29: ( p in Leaves (dom T) & T . p = x ) ; ::_thesis: T1 . y = T2 . y
then A30: T1 . (p ^ p9) = T9 . p9 by A24;
 p ^ p9 = p by FINSEQ_1:34;
hence  T1 . y = T2 . y by A27, A29, A30; ::_thesis: verum
end;
supposeA31: ( not p in Leaves (dom T) or T . p <> x ) ; ::_thesis: T1 . y = T2 . y
then  T1 . p = T . p by A23;
hence  T1 . y = T2 . y by A26, A31; ::_thesis: verum
end;
end;
end;
end;
suppose ex q being Node of T ex r being Node of T9 st
( q in Leaves (dom T) & T . q = x & p = q ^ r ) ; ::_thesis: T1 . b1 = T2 . b1
then consider q being Node of T, r being Node of T9 such that
A32: ( q in Leaves (dom T) & T . q = x & p = q ^ r ) ;
thus T1 . y = T9 . r by A24, A32
.= T2 . y by A27, A32 ; ::_thesis: verum
end;
end;
end;
hence  T1 = T2 by A28, FUNCT_1:2; ::_thesis: verum
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
 rng ((T,x) <- T9) c= D
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng ((T,x) <- T9) or y in D )
assume  y in rng ((T,x) <- T9) ; ::_thesis: y in D
then consider z being set  such that
A1: z in dom ((T,x) <- T9) and
A2: y = ((T,x) <- T9) . z by FUNCT_1:def_3;
reconsider z = z as Node of ((T,x) <- T9) by A1;
reconsider p9 = {} as Node of T9 by TREES_1:22;
percases ( z 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 & z = q ^ r ) ) by Def7;
suppose z in dom T ; ::_thesis: y in D
then reconsider p = z as Node of T ;
hereby  ::_thesis: verum
percases ( ( p in Leaves (dom T) & T . p = x ) or not p in Leaves (dom T) or T . p <> x ) ;
suppose ( p in Leaves (dom T) & T . p = x ) ; ::_thesis: y in D
then A3: ((T,x) <- T9) . (p ^ p9) = T9 . p9 by Def7;
 p ^ p9 = p by FINSEQ_1:34;
hence  y in D by A2, A3; ::_thesis: verum
end;
suppose ( not p in Leaves (dom T) or T . p <> x ) ; ::_thesis: y in D
then  ((T,x) <- T9) . p = T . p by Def7;
hence  y in D by A2; ::_thesis: verum
end;
end;
end;
end;
suppose ex q being Node of T ex r being Node of T9 st
( q in Leaves (dom T) & T . q = x & z = q ^ r ) ; ::_thesis: y in D
then consider q being Node of T, r being Node of T9 such that
A4: ( q in Leaves (dom T) & T . q = x & z = q ^ r ) ;
 ((T,x) <- T9) . z = T9 . r by A4, Def7;
hence  y in D by A2; ::_thesis: verum
end;
end;
end;
hence  (T,x) <- T9 is D -valued by RELAT_1:def_19; ::_thesis: verum
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
let T, T9 be DecoratedTree; ::_thesis: for x being set st ( not x in rng T or not x in Leaves T ) holds
(T,x) <- T9 = T
let x be set ; ::_thesis: ( ( not x in rng T or not x in Leaves T ) implies (T,x) <- T9 = T )
A1: Leaves T c= rng T by RELAT_1:111;
assume  ( not x in rng T or not x in Leaves T ) ; ::_thesis: (T,x) <- T9 = T
then A2: not x in Leaves T by A1;
thus A3: dom ((T,x) <- T9) = dom T :: according to TREES_4:def_1 ::_thesis: for p being Node of ((T,x) <- T9) holds ((T,x) <- T9) . p = T . p
proof
let p be FinSequence of NAT ; :: according to TREES_2:def_1 ::_thesis: ( ( not p in dom ((T,x) <- T9) or p in dom T ) & ( not p in dom T or p in dom ((T,x) <- T9) ) )
 ( p in dom ((T,x) <- T9) 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 ) ) ) by Def7;
hence  ( ( not p in dom ((T,x) <- T9) or p in dom T ) & ( not p in dom T or p in dom ((T,x) <- T9) ) ) by A2, FUNCT_1:def_6; ::_thesis: verum
end;
let p be Node of ((T,x) <- T9); ::_thesis: ((T,x) <- T9) . p = T . p
reconsider p9 = p as Node of T by A3;
 ( p9 in Leaves (dom T) implies T . p9 in Leaves T ) by FUNCT_1:def_6;
hence  ((T,x) <- T9) . p = T . p by A2, Def7; ::_thesis: verum
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
let D1, D2 be non empty set ; ::_thesis: for T being DecoratedTree of D1,D2 holds
( dom (T `1) = dom T & dom (T `2) = dom T )
let T be DecoratedTree of D1,D2; ::_thesis: ( dom (T `1) = dom T & dom (T `2) = dom T )
A1: ( T `1 = (pr1 (D1,D2)) * T & T `2 = (pr2 (D1,D2)) * T ) by TREES_3:def_12, TREES_3:def_13;
A2: ( rng T c= [:D1,D2:] & dom (pr1 (D1,D2)) = [:D1,D2:] ) by FUNCT_2:def_1, RELAT_1:def_19;
 dom (pr2 (D1,D2)) = [:D1,D2:] by FUNCT_2:def_1;
hence  ( dom (T `1) = dom T & dom (T `2) = dom T ) by A1, A2, RELAT_1:27; ::_thesis: verum
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
let D1, D2 be non empty set ; ::_thesis: 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 )
let d1 be Element of D1; ::_thesis: for d2 being Element of D2 holds
( (root-tree [d1,d2]) `1 = root-tree d1 & (root-tree [d1,d2]) `2 = root-tree d2 )
let d2 be Element of D2; ::_thesis: ( (root-tree [d1,d2]) `1 = root-tree d1 & (root-tree [d1,d2]) `2 = root-tree d2 )
reconsider r = {} as Node of (root-tree [d1,d2]) by TREES_1:22;
A1: dom ((root-tree [d1,d2]) `1) = dom (root-tree [d1,d2]) by Th24;
A2: dom ((root-tree [d1,d2]) `2) = dom (root-tree [d1,d2]) by Th24;
A3: (root-tree [d1,d2]) . r = [d1,d2] by Th3;
A4: [d1,d2] `1 = d1 by MCART_1:7;
A5: [d1,d2] `2 = d2 by MCART_1:7;
thus (root-tree [d1,d2]) `1 = root-tree (((root-tree [d1,d2]) `1) . r) by A1, Th3, Th5
.= root-tree d1 by A3, A4, TREES_3:39 ; ::_thesis: (root-tree [d1,d2]) `2 = root-tree d2
thus (root-tree [d1,d2]) `2 = root-tree (((root-tree [d1,d2]) `2) . r) by A2, Th3, Th5
.= root-tree d2 by A3, A5, TREES_3:39 ; ::_thesis: verum
end;

theorem :: TREES_4:26
for x, y being set holds <:(root-tree x),(root-tree y):> = root-tree [x,y]
proof
let x, y be set ; ::_thesis: <:(root-tree x),(root-tree y):> = root-tree [x,y]
reconsider x9 = x as Element of {x} by TARSKI:def_1;
reconsider y9 = y as Element of {y} by TARSKI:def_1;
 ( (root-tree [x9,y9]) `1 = root-tree x & (root-tree [x9,y9]) `2 = root-tree y ) by Th25;
hence  <:(root-tree x),(root-tree y):> = root-tree [x,y] by TREES_3:40; ::_thesis: verum
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
let D1, D2 be non empty set ; ::_thesis: 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
let d1 be Element of D1; ::_thesis: 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
let d2 be Element of D2; ::_thesis: 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
let F be non empty DTree-set of D1,D2; ::_thesis: 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
let F1 be non empty DTree-set of D1; ::_thesis: 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
let p be FinSequence of F; ::_thesis: 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
let p1 be FinSequence of F1; ::_thesis: ( 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 ) implies ([d1,d2] -tree p) `1 = d1 -tree p1 )
assume that
A1: dom p1 = dom p and
A2: 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 ; ::_thesis: ([d1,d2] -tree p) `1 = d1 -tree p1
set W = [d1,d2] -tree p;
set W1 = d1 -tree p1;
A3: len (doms p) = len p by TREES_3:38;
A4: len (doms p1) = len p1 by TREES_3:38;
A5: len p = len p1 by A1, FINSEQ_3:29;
then A6: dom (doms p) = dom (doms p1) by A3, A4, FINSEQ_3:29;
A7: dom (doms p) = dom p by A3, FINSEQ_3:29;
now__::_thesis:_for_i_being_Nat_st_i_in_dom_p_holds_
(doms_p)_._i_=_(doms_p1)_._i
let i be Nat; ::_thesis: ( i in dom p implies (doms p) . i = (doms p1) . i )
assume A8: i in dom p ; ::_thesis: (doms p) . i = (doms p1) . i
then reconsider T = p . i as Element of F by Lm1;
A9: p1 . i = T `1 by A2, A8;
A10: (doms p) . i = dom T by A8, FUNCT_6:22;
 (doms p1) . i = dom (T `1) by A1, A8, A9, FUNCT_6:22;
hence  (doms p) . i = (doms p1) . i by A10, Th24; ::_thesis: verum
end;
then A11: doms p = doms p1 by A6, A7, FINSEQ_1:13;
dom (([d1,d2] -tree p) `1) = dom ([d1,d2] -tree p) by Th24
.= tree (doms p) by Th10 ;
hence  dom (([d1,d2] -tree p) `1) = dom (d1 -tree p1) by A11, Th10; :: according to TREES_4:def_1 ::_thesis: for p being Node of (([d1,d2] -tree p) `1) holds (([d1,d2] -tree p) `1) . p = (d1 -tree p1) . p
let x be Node of (([d1,d2] -tree p) `1); ::_thesis: (([d1,d2] -tree p) `1) . x = (d1 -tree p1) . x
reconsider a = x as Node of ([d1,d2] -tree p) by Th24;
A12: (([d1,d2] -tree p) `1) . x = (([d1,d2] -tree p) . a) `1 by TREES_3:39;
percases ( x = {} or x <> {} ) ;
suppose x = {} ; ::_thesis: (([d1,d2] -tree p) `1) . x = (d1 -tree p1) . x
then  ( ([d1,d2] -tree p) . x = [d1,d2] & (d1 -tree p1) . x = d1 ) by Def4;
hence  (([d1,d2] -tree p) `1) . x = (d1 -tree p1) . x by A12, MCART_1:7; ::_thesis: verum
end;
suppose x <> {} ; ::_thesis: (([d1,d2] -tree p) `1) . x = (d1 -tree p1) . x
then consider n being Element of NAT , T being DecoratedTree, q being Node of T such that
A13: n < len p and
A14: T = p . (n + 1) and
A15: a = <*n*> ^ q by Th11;
reconsider T = T as Element of F by A13, A14, Lm3;
reconsider q = q as Node of (T `1) by Th24;
A16: p1 . (n + 1) = T `1 by A2, A13, A14, Lm2;
A17: ([d1,d2] -tree p) . a = T . q by A13, A14, A15, Th12;
 (d1 -tree p1) . a = (T `1) . q by A5, A13, A15, A16, Th12;
hence  (([d1,d2] -tree p) `1) . x = (d1 -tree p1) . x by A12, A17, TREES_3:39; ::_thesis: verum
end;
end;
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
let D1, D2 be non empty set ; ::_thesis: 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
let d1 be Element of D1; ::_thesis: 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
let d2 be Element of D2; ::_thesis: 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
let F be non empty DTree-set of D1,D2; ::_thesis: 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
let F2 be non empty DTree-set of D2; ::_thesis: 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
let p be FinSequence of F; ::_thesis: 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
let p2 be FinSequence of F2; ::_thesis: ( 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 ) implies ([d1,d2] -tree p) `2 = d2 -tree p2 )
assume that
A1: dom p2 = dom p and
A2: 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 ; ::_thesis: ([d1,d2] -tree p) `2 = d2 -tree p2
set W = [d1,d2] -tree p;
set W2 = d2 -tree p2;
A3: len (doms p) = len p by TREES_3:38;
A4: len (doms p2) = len p2 by TREES_3:38;
A5: len p = len p2 by A1, FINSEQ_3:29;
then A6: dom (doms p) = dom (doms p2) by A3, A4, FINSEQ_3:29;
A7: dom (doms p) = dom p by A3, FINSEQ_3:29;
now__::_thesis:_for_i_being_Nat_st_i_in_dom_p_holds_
(doms_p)_._i_=_(doms_p2)_._i
let i be Nat; ::_thesis: ( i in dom p implies (doms p) . i = (doms p2) . i )
assume A8: i in dom p ; ::_thesis: (doms p) . i = (doms p2) . i
then reconsider T = p . i as Element of F by Lm1;
A9: p2 . i = T `2 by A2, A8;
A10: (doms p) . i = dom T by A8, FUNCT_6:22;
 (doms p2) . i = dom (T `2) by A1, A8, A9, FUNCT_6:22;
hence  (doms p) . i = (doms p2) . i by A10, Th24; ::_thesis: verum
end;
then A11: doms p = doms p2 by A6, A7, FINSEQ_1:13;
dom (([d1,d2] -tree p) `2) = dom ([d1,d2] -tree p) by Th24
.= tree (doms p) by Th10 ;
hence  dom (([d1,d2] -tree p) `2) = dom (d2 -tree p2) by A11, Th10; :: according to TREES_4:def_1 ::_thesis: for p being Node of (([d1,d2] -tree p) `2) holds (([d1,d2] -tree p) `2) . p = (d2 -tree p2) . p
let x be Node of (([d1,d2] -tree p) `2); ::_thesis: (([d1,d2] -tree p) `2) . x = (d2 -tree p2) . x
reconsider a = x as Node of ([d1,d2] -tree p) by Th24;
A12: (([d1,d2] -tree p) `2) . x = (([d1,d2] -tree p) . a) `2 by TREES_3:39;
percases ( x = {} or x <> {} ) ;
suppose x = {} ; ::_thesis: (([d1,d2] -tree p) `2) . x = (d2 -tree p2) . x
then  ( ([d1,d2] -tree p) . x = [d1,d2] & (d2 -tree p2) . x = d2 ) by Def4;
hence  (([d1,d2] -tree p) `2) . x = (d2 -tree p2) . x by A12, MCART_1:7; ::_thesis: verum
end;
suppose x <> {} ; ::_thesis: (([d1,d2] -tree p) `2) . x = (d2 -tree p2) . x
then consider n being Element of NAT , T being DecoratedTree, q being Node of T such that
A13: n < len p and
A14: T = p . (n + 1) and
A15: a = <*n*> ^ q by Th11;
reconsider T = T as Element of F by A13, A14, Lm3;
reconsider q = q as Node of (T `2) by Th24;
A16: p2 . (n + 1) = T `2 by A2, A13, A14, Lm2;
A17: ([d1,d2] -tree p) . a = T . q by A13, A14, A15, Th12;
 (d2 -tree p2) . a = (T `2) . q by A5, A13, A15, A16, Th12;
hence  (([d1,d2] -tree p) `2) . x = (d2 -tree p2) . x by A12, A17, TREES_3:39; ::_thesis: verum
end;
end;
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
let D1, D2 be non empty set ; ::_thesis: 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 )
let d1 be Element of D1; ::_thesis: 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 )
let d2 be Element of D2; ::_thesis: 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 )
let F be non empty DTree-set of D1,D2; ::_thesis: 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 )
let p be FinSequence of F; ::_thesis: 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 )
A1: Seg (len p) = dom p by FINSEQ_1:def_3;
defpred S1[ set , set ] means  ex T being Element of F st
( T = p . $1 & $2 = T `1 );
A2: for i being Nat st i in Seg (len p) holds
ex x being Element of Trees D1 st S1[i,x]
proof
let i be Nat; ::_thesis: ( i in Seg (len p) implies ex x being Element of Trees D1 st S1[i,x] )
assume  i in Seg (len p) ; ::_thesis: ex x being Element of Trees D1 st S1[i,x]
then reconsider T = p . i as Element of F by A1, Lm1;
reconsider y = T `1 as Element of Trees D1 by TREES_3:def_7;
take  y ; ::_thesis: S1[i,y]
take  T ; ::_thesis: ( T = p . i & y = T `1 )
thus  ( T = p . i & y = T `1 ) ; ::_thesis: verum
end;
consider p1 being FinSequence of Trees D1 such that
A3: ( dom p1 = Seg (len p) & ( for i being Nat st i in Seg (len p) holds
S1[i,p1 . i] ) ) from FINSEQ_1:sch_5(A2);
take  p1 ; ::_thesis: ( 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 )
thus A4: dom p1 = dom p by A3, FINSEQ_1:def_3; ::_thesis: ( ( 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 )
hence  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 ) by A3; ::_thesis: ([d1,d2] -tree p) `1 = d1 -tree p1
now__::_thesis:_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
let i be Element of NAT ; ::_thesis: ( i in dom p implies for T being DecoratedTree of D1,D2 st T = p . i holds
p1 . i = T `1 )
assume  i in dom p ; ::_thesis: for T being DecoratedTree of D1,D2 st T = p . i holds
p1 . i = T `1
then  ex T being Element of F st
( T = p . i & p1 . i = T `1 ) by A3, A4;
hence  for T being DecoratedTree of D1,D2 st T = p . i holds
p1 . i = T `1 ; ::_thesis: verum
end;
hence  ([d1,d2] -tree p) `1 = d1 -tree p1 by A4, Th27; ::_thesis: verum
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
let D1, D2 be non empty set ; ::_thesis: 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 )
let d1 be Element of D1; ::_thesis: 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 )
let d2 be Element of D2; ::_thesis: 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 )
let F be non empty DTree-set of D1,D2; ::_thesis: 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 )
let p be FinSequence of F; ::_thesis: 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 )
A1: Seg (len p) = dom p by FINSEQ_1:def_3;
defpred S1[ Nat, set ] means  ex T being Element of F st
( T = p . $1 & $2 = T `2 );
A2: for i being Nat st i in Seg (len p) holds
ex x being Element of Trees D2 st S1[i,x]
proof
let i be Nat; ::_thesis: ( i in Seg (len p) implies ex x being Element of Trees D2 st S1[i,x] )
assume  i in Seg (len p) ; ::_thesis: ex x being Element of Trees D2 st S1[i,x]
then reconsider T = p . i as Element of F by A1, Lm1;
reconsider y = T `2 as Element of Trees D2 by TREES_3:def_7;
take  y ; ::_thesis: S1[i,y]
take  T ; ::_thesis: ( T = p . i & y = T `2 )
thus  ( T = p . i & y = T `2 ) ; ::_thesis: verum
end;
consider p2 being FinSequence of Trees D2 such that
A3: ( dom p2 = Seg (len p) & ( for i being Nat st i in Seg (len p) holds
S1[i,p2 . i] ) ) from FINSEQ_1:sch_5(A2);
take  p2 ; ::_thesis: ( 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 )
thus A4: dom p2 = dom p by A3, FINSEQ_1:def_3; ::_thesis: ( ( 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 )
hence  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 ) by A3; ::_thesis: ([d1,d2] -tree p) `2 = d2 -tree p2
now__::_thesis:_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
let i be Element of NAT ; ::_thesis: ( i in dom p implies for T being DecoratedTree of D1,D2 st T = p . i holds
p2 . i = T `2 )
assume  i in dom p ; ::_thesis: for T being DecoratedTree of D1,D2 st T = p . i holds
p2 . i = T `2
then  ex T being Element of F st
( T = p . i & p2 . i = T `2 ) by A3, A4;
hence  for T being DecoratedTree of D1,D2 st T = p . i holds
p2 . i = T `2 ; ::_thesis: verum
end;
hence  ([d1,d2] -tree p) `2 = d2 -tree p2 by A4, Th28; ::_thesis: verum
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
let D1, D2 be non empty set ; ::_thesis: 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 )
let d1 be Element of D1; ::_thesis: 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 )
let d2 be Element of D2; ::_thesis: 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 )
let p be FinSequence of FinTrees [:D1,D2:]; ::_thesis: 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 )
consider p1 being FinSequence of Trees D1 such that
A1: ( 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 ) ) ) and
A2: ([d1,d2] -tree p) `1 = d1 -tree p1 by Th29;
 rng p1 c= FinTrees D1
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng p1 or x in FinTrees D1 )
assume  x in rng p1 ; ::_thesis: x in FinTrees D1
then consider y being set  such that
A3: y in dom p1 and
A4: x = p1 . y by FUNCT_1:def_3;
reconsider y = y as Element of NAT by A3;
consider T being Element of FinTrees [:D1,D2:] such that
 T = p . y and
A5: p1 . y = T `1 by A1, A3;
 dom (T `1) = dom T by Th24;
hence  x in FinTrees D1 by A4, A5, TREES_3:def_8; ::_thesis: verum
end;
then  p1 is FinSequence of FinTrees D1 by FINSEQ_1:def_4;
hence  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 ) by A1, A2; ::_thesis: verum
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
let D1, D2 be non empty set ; ::_thesis: 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 )
let d1 be Element of D1; ::_thesis: 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 )
let d2 be Element of D2; ::_thesis: 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 )
let p be FinSequence of FinTrees [:D1,D2:]; ::_thesis: 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 )
consider p2 being FinSequence of Trees D2 such that
A1: ( 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 ) ) ) and
A2: ([d1,d2] -tree p) `2 = d2 -tree p2 by Th30;
 rng p2 c= FinTrees D2
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng p2 or x in FinTrees D2 )
assume  x in rng p2 ; ::_thesis: x in FinTrees D2
then consider y being set  such that
A3: y in dom p2 and
A4: x = p2 . y by FUNCT_1:def_3;
reconsider y = y as Element of NAT by A3;
consider T being Element of FinTrees [:D1,D2:] such that
 T = p . y and
A5: p2 . y = T `2 by A1, A3;
 dom (T `2) = dom T by Th24;
hence  x in FinTrees D2 by A4, A5, TREES_3:def_8; ::_thesis: verum
end;
then  p2 is FinSequence of FinTrees D2 by FINSEQ_1:def_4;
hence  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 ) by A1, A2; ::_thesis: verum
end;