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 object st y in dom T1 holds
T1 . y = T2 . y
let y be object ; :: 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 ;
per cases ( 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
per cases ( ( p in Leaves (dom T) & T . p = x ) or not p in Leaves (dom T) or T . p <> x ) ;
suppose A29: ( 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;
suppose A31: ( 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; :: thesis: verum