let D1, D2 be DecoratedTree; :: thesis: ( dom D1 = tree ((dom T),P,(dom T1)) & ( for q being FinSequence of NAT holds

( not q in tree ((dom T),P,(dom T1)) or for p being FinSequence of NAT st p in P holds

( not p is_a_prefix_of q & D1 . q = T . q ) or ex p, r being FinSequence of NAT st

( p in P & r in dom T1 & q = p ^ r & D1 . q = T1 . r ) ) ) & dom D2 = tree ((dom T),P,(dom T1)) & ( for q being FinSequence of NAT holds

( not q in tree ((dom T),P,(dom T1)) or for p being FinSequence of NAT st p in P holds

( not p is_a_prefix_of q & D2 . q = T . q ) or ex p, r being FinSequence of NAT st

( p in P & r in dom T1 & q = p ^ r & D2 . q = T1 . r ) ) ) implies D1 = D2 )

assume that

A7: dom D1 = tree ((dom T),P,(dom T1)) and

A8: for q being FinSequence of NAT holds

( not q in tree ((dom T),P,(dom T1)) or for p being FinSequence of NAT st p in P holds

( not p is_a_prefix_of q & D1 . q = T . q ) or ex p, r being FinSequence of NAT st

( p in P & r in dom T1 & q = p ^ r & D1 . q = T1 . r ) ) and

A9: dom D2 = tree ((dom T),P,(dom T1)) and

A10: for q being FinSequence of NAT holds

( not q in tree ((dom T),P,(dom T1)) or for p being FinSequence of NAT st p in P holds

( not p is_a_prefix_of q & D2 . q = T . q ) or ex p, r being FinSequence of NAT st

( p in P & r in dom T1 & q = p ^ r & D2 . q = T1 . r ) ) ; :: thesis: D1 = D2

( not q in tree ((dom T),P,(dom T1)) or for p being FinSequence of NAT st p in P holds

( not p is_a_prefix_of q & D1 . q = T . q ) or ex p, r being FinSequence of NAT st

( p in P & r in dom T1 & q = p ^ r & D1 . q = T1 . r ) ) ) & dom D2 = tree ((dom T),P,(dom T1)) & ( for q being FinSequence of NAT holds

( not q in tree ((dom T),P,(dom T1)) or for p being FinSequence of NAT st p in P holds

( not p is_a_prefix_of q & D2 . q = T . q ) or ex p, r being FinSequence of NAT st

( p in P & r in dom T1 & q = p ^ r & D2 . q = T1 . r ) ) ) implies D1 = D2 )

assume that

A7: dom D1 = tree ((dom T),P,(dom T1)) and

A8: for q being FinSequence of NAT holds

( not q in tree ((dom T),P,(dom T1)) or for p being FinSequence of NAT st p in P holds

( not p is_a_prefix_of q & D1 . q = T . q ) or ex p, r being FinSequence of NAT st

( p in P & r in dom T1 & q = p ^ r & D1 . q = T1 . r ) ) and

A9: dom D2 = tree ((dom T),P,(dom T1)) and

A10: for q being FinSequence of NAT holds

( not q in tree ((dom T),P,(dom T1)) or for p being FinSequence of NAT st p in P holds

( not p is_a_prefix_of q & D2 . q = T . q ) or ex p, r being FinSequence of NAT st

( p in P & r in dom T1 & q = p ^ r & D2 . q = T1 . r ) ) ; :: thesis: D1 = D2

now :: thesis: for q being FinSequence of NAT st q in dom D1 holds

not D1 . q <> D2 . q

hence
D1 = D2
by A7, A9, TREES_2:31; :: thesis: verumnot D1 . q <> D2 . q

let q be FinSequence of NAT ; :: thesis: ( q in dom D1 implies not D1 . q <> D2 . q )

assume that

A11: q in dom D1 and

A12: D1 . q <> D2 . q ; :: thesis: contradiction

thus contradiction :: thesis: verum

end;assume that

A11: q in dom D1 and

A12: D1 . q <> D2 . q ; :: thesis: contradiction

thus contradiction :: thesis: verum

proof
end;

per cases
( for p being FinSequence of NAT st p in P holds

( not p is_a_prefix_of q & D1 . q = T . q ) or ex p, r being FinSequence of NAT st

( p in P & r in dom T1 & q = p ^ r & D1 . q = T1 . r ) ) by A7, A8, A11;

end;

( not p is_a_prefix_of q & D1 . q = T . q ) or ex p, r being FinSequence of NAT st

( p in P & r in dom T1 & q = p ^ r & D1 . q = T1 . r ) ) by A7, A8, A11;

suppose A13:
for p being FinSequence of NAT st p in P holds

( not p is_a_prefix_of q & D1 . q = T . q ) ; :: thesis: contradiction

end;

( not p is_a_prefix_of q & D1 . q = T . q ) ; :: thesis: contradiction

now :: thesis: contradictionend;

hence
contradiction
; :: thesis: verumper cases
( for p being FinSequence of NAT st p in P holds

( not p is_a_prefix_of q & D2 . q = T . q ) or ex p, r being FinSequence of NAT st

( p in P & r in dom T1 & q = p ^ r & D2 . q = T1 . r ) ) by A7, A10, A11;

end;

( not p is_a_prefix_of q & D2 . q = T . q ) or ex p, r being FinSequence of NAT st

( p in P & r in dom T1 & q = p ^ r & D2 . q = T1 . r ) ) by A7, A10, A11;

suppose A14:
for p being FinSequence of NAT st p in P holds

( not p is_a_prefix_of q & D2 . q = T . q ) ; :: thesis: contradiction

( not p is_a_prefix_of q & D2 . q = T . q ) ; :: thesis: contradiction

consider x being object such that

A15: x in P by A1, XBOOLE_0:def 1;

P c= dom T by TREES_1:def 11;

then reconsider x = x as Element of dom T by A15;

A16: ex p9 being FinSequence of NAT st p9 = x ;

then D1 . q = T . q by A13, A15;

hence contradiction by A12, A14, A15, A16; :: thesis: verum

end;A15: x in P by A1, XBOOLE_0:def 1;

P c= dom T by TREES_1:def 11;

then reconsider x = x as Element of dom T by A15;

A16: ex p9 being FinSequence of NAT st p9 = x ;

then D1 . q = T . q by A13, A15;

hence contradiction by A12, A14, A15, A16; :: thesis: verum

suppose
ex p, r being FinSequence of NAT st

( p in P & r in dom T1 & q = p ^ r & D2 . q = T1 . r ) ; :: thesis: contradiction

( p in P & r in dom T1 & q = p ^ r & D2 . q = T1 . r ) ; :: thesis: contradiction

then consider p2, r2 being FinSequence of NAT such that

A17: p2 in P and

r2 in dom T1 and

A18: q = p2 ^ r2 and

D2 . q = T1 . r2 ;

not p2 is_a_prefix_of q by A13, A17;

hence contradiction by A18, TREES_1:1; :: thesis: verum

end;A17: p2 in P and

r2 in dom T1 and

A18: q = p2 ^ r2 and

D2 . q = T1 . r2 ;

not p2 is_a_prefix_of q by A13, A17;

hence contradiction by A18, TREES_1:1; :: thesis: verum

suppose
ex p, r being FinSequence of NAT st

( p in P & r in dom T1 & q = p ^ r & D1 . q = T1 . r ) ; :: thesis: contradiction

( p in P & r in dom T1 & q = p ^ r & D1 . q = T1 . r ) ; :: thesis: contradiction

then consider p1, r1 being FinSequence of NAT such that

A19: p1 in P and

r1 in dom T1 and

A20: q = p1 ^ r1 and

A21: D1 . q = T1 . r1 ;

end;A19: p1 in P and

r1 in dom T1 and

A20: q = p1 ^ r1 and

A21: D1 . q = T1 . r1 ;

now :: thesis: contradictionend;

hence
contradiction
; :: thesis: verumper cases
( for p being FinSequence of NAT st p in P holds

( not p is_a_prefix_of q & D2 . q = T . q ) or ex p, r being FinSequence of NAT st

( p in P & r in dom T1 & q = p ^ r & D2 . q = T1 . r ) ) by A7, A10, A11;

end;

( not p is_a_prefix_of q & D2 . q = T . q ) or ex p, r being FinSequence of NAT st

( p in P & r in dom T1 & q = p ^ r & D2 . q = T1 . r ) ) by A7, A10, A11;

suppose
for p being FinSequence of NAT st p in P holds

( not p is_a_prefix_of q & D2 . q = T . q ) ; :: thesis: contradiction

end;

( not p is_a_prefix_of q & D2 . q = T . q ) ; :: thesis: contradiction

end;

suppose
ex p, r being FinSequence of NAT st

( p in P & r in dom T1 & q = p ^ r & D2 . q = T1 . r ) ; :: thesis: contradiction

( p in P & r in dom T1 & q = p ^ r & D2 . q = T1 . r ) ; :: thesis: contradiction

then consider p2, r2 being FinSequence of NAT such that

A22: p2 in P and

r2 in dom T1 and

A23: q = p2 ^ r2 and

A24: D2 . q = T1 . r2 ;

end;A22: p2 in P and

r2 in dom T1 and

A23: q = p2 ^ r2 and

A24: D2 . q = T1 . r2 ;

now :: thesis: not p1 <> p2

hence
contradiction
by A12, A20, A21, A23, A24, FINSEQ_1:33; :: thesis: verumassume A25:
p1 <> p2
; :: thesis: contradiction

p1,p2 are_c=-comparable by A20, A23, Th1;

hence contradiction by A19, A22, A25, TREES_1:def 10; :: thesis: verum

end;p1,p2 are_c=-comparable by A20, A23, Th1;

hence contradiction by A19, A22, A25, TREES_1:def 10; :: thesis: verum