defpred S_{1}[ 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

( S_{1}[q] & p = q ^ r ) ) )
from TREES_4:sch 1();

defpred S_{2}[ object , object ] 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 object st z in W holds

ex y being object st S_{2}[z,y]

A6: ( dom f = W & ( for z being object st z in W holds

S_{2}[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

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;

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;

hence f . (p ^ q) = T9 . q by A16, A18, FINSEQ_1:33; :: thesis: verum

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

( S

defpred S

( $1 = p ^ q & p in Leaves (dom T) & T . p = x & $2 = T9 . q ) );

A2: for z being object st z in W holds

ex y being object st S

proof

consider f being Function such that
let z be object ; :: thesis: ( z in W implies ex y being object st S_{2}[z,y] )

assume z in W ; :: thesis: ex y being object st S_{2}[z,y]

then reconsider w = z as Element of W ;

_{2}[z,y]
by A3; :: thesis: verum

end;assume z in W ; :: thesis: ex y being object st S

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 ) )

( 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;( 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

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 ) )

hence
ex y being object st Sfor 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;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

A6: ( dom f = W & ( for z being object st z in W holds

S

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: for q being Node of T9 st p in Leaves (dom T) & T . p = x holds
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;

end;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 )

hence
f . p = T . p
by A6, A8; :: thesis: verumfor 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;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

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 )

then consider p9 being Node of T, q9 being Node of T9 such that 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 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

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

then
p = p9
by A12, A16, A17;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

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

then
ex r being FinSequence st p9 ^ r = p
by A19, FINSEQ_1:47;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 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

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

hence f . (p ^ q) = T9 . q by A16, A18, FINSEQ_1:33; :: thesis: verum