let T, T1 be DecoratedTree; :: thesis: for P being AntiChain_of_Prefixes of dom T

for q being FinSequence of NAT st q in dom (tree (T,P,T1)) & q in { (p ^ s) where p is Element of dom T, s is Element of dom T1 : p in P } holds

ex p9 being Element of dom T ex r being Element of dom T1 st

( q = p9 ^ r & p9 in P & (tree (T,P,T1)) . q = T1 . r )

let P be AntiChain_of_Prefixes of dom T; :: thesis: for q being FinSequence of NAT st q in dom (tree (T,P,T1)) & q in { (p ^ s) where p is Element of dom T, s is Element of dom T1 : p in P } holds

ex p9 being Element of dom T ex r being Element of dom T1 st

( q = p9 ^ r & p9 in P & (tree (T,P,T1)) . q = T1 . r )

let q be FinSequence of NAT ; :: thesis: ( q in dom (tree (T,P,T1)) & q in { (p ^ s) where p is Element of dom T, s is Element of dom T1 : p in P } implies ex p9 being Element of dom T ex r being Element of dom T1 st

( q = p9 ^ r & p9 in P & (tree (T,P,T1)) . q = T1 . r ) )

assume that

A1: q in dom (tree (T,P,T1)) and

A2: q in { (p ^ s) where p is Element of dom T, s is Element of dom T1 : p in P } ; :: thesis: ex p9 being Element of dom T ex r being Element of dom T1 st

( q = p9 ^ r & p9 in P & (tree (T,P,T1)) . q = T1 . r )

for q being FinSequence of NAT st q in dom (tree (T,P,T1)) & q in { (p ^ s) where p is Element of dom T, s is Element of dom T1 : p in P } holds

ex p9 being Element of dom T ex r being Element of dom T1 st

( q = p9 ^ r & p9 in P & (tree (T,P,T1)) . q = T1 . r )

let P be AntiChain_of_Prefixes of dom T; :: thesis: for q being FinSequence of NAT st q in dom (tree (T,P,T1)) & q in { (p ^ s) where p is Element of dom T, s is Element of dom T1 : p in P } holds

ex p9 being Element of dom T ex r being Element of dom T1 st

( q = p9 ^ r & p9 in P & (tree (T,P,T1)) . q = T1 . r )

let q be FinSequence of NAT ; :: thesis: ( q in dom (tree (T,P,T1)) & q in { (p ^ s) where p is Element of dom T, s is Element of dom T1 : p in P } implies ex p9 being Element of dom T ex r being Element of dom T1 st

( q = p9 ^ r & p9 in P & (tree (T,P,T1)) . q = T1 . r ) )

assume that

A1: q in dom (tree (T,P,T1)) and

A2: q in { (p ^ s) where p is Element of dom T, s is Element of dom T1 : p in P } ; :: thesis: ex p9 being Element of dom T ex r being Element of dom T1 st

( q = p9 ^ r & p9 in P & (tree (T,P,T1)) . q = T1 . r )

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

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

( p in P & r in dom T1 & q = p ^ r & (tree (T,P,T1)) . q = T1 . r ) ) by A1, Th10;

end;

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

( p in P & r in dom T1 & q = p ^ r & (tree (T,P,T1)) . q = T1 . r ) ) by A1, Th10;

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

( not p is_a_prefix_of q & (tree (T,P,T1)) . q = T . q ) ; :: thesis: ex p9 being Element of dom T ex r being Element of dom T1 st

( q = p9 ^ r & p9 in P & (tree (T,P,T1)) . q = T1 . r )

( not p is_a_prefix_of q & (tree (T,P,T1)) . q = T . q ) ; :: thesis: ex p9 being Element of dom T ex r being Element of dom T1 st

( q = p9 ^ r & p9 in P & (tree (T,P,T1)) . q = T1 . r )

consider p9 being Element of dom T, r being Element of dom T1 such that

A4: q = p9 ^ r and

A5: p9 in P by A2;

(tree (T,P,T1)) . q = T1 . r by A4, TREES_1:1, A3, A5;

hence ex p9 being Element of dom T ex r being Element of dom T1 st

( q = p9 ^ r & p9 in P & (tree (T,P,T1)) . q = T1 . r ) by A4, A5; :: thesis: verum

end;A4: q = p9 ^ r and

A5: p9 in P by A2;

(tree (T,P,T1)) . q = T1 . r by A4, TREES_1:1, A3, A5;

hence ex p9 being Element of dom T ex r being Element of dom T1 st

( q = p9 ^ r & p9 in P & (tree (T,P,T1)) . q = T1 . r ) by A4, A5; :: thesis: verum

suppose
ex p, r being FinSequence of NAT st

( p in P & r in dom T1 & q = p ^ r & (tree (T,P,T1)) . q = T1 . r ) ; :: thesis: ex p9 being Element of dom T ex r being Element of dom T1 st

( q = p9 ^ r & p9 in P & (tree (T,P,T1)) . q = T1 . r )

( p in P & r in dom T1 & q = p ^ r & (tree (T,P,T1)) . q = T1 . r ) ; :: thesis: ex p9 being Element of dom T ex r being Element of dom T1 st

( q = p9 ^ r & p9 in P & (tree (T,P,T1)) . q = T1 . r )

then consider p, r being FinSequence of NAT such that

A6: p in P and

A7: r in dom T1 and

A8: q = p ^ r and

A9: (tree (T,P,T1)) . q = T1 . r ;

consider p9 being Element of dom T, r9 being Element of dom T1 such that

A10: q = p9 ^ r9 and

A11: p9 in P by A2;

( q = p9 ^ r & p9 in P & (tree (T,P,T1)) . q = T1 . r ) by A6, A7, A8, A9; :: thesis: verum

end;A6: p in P and

A7: r in dom T1 and

A8: q = p ^ r and

A9: (tree (T,P,T1)) . q = T1 . r ;

consider p9 being Element of dom T, r9 being Element of dom T1 such that

A10: q = p9 ^ r9 and

A11: p9 in P by A2;

now :: thesis: not p <> p9

hence
ex p9 being Element of dom T ex r being Element of dom T1 st assume A12:
p <> p9
; :: thesis: contradiction

p,p9 are_c=-comparable by A8, A10, Th1;

hence contradiction by A6, A11, A12, TREES_1:def 10; :: thesis: verum

end;p,p9 are_c=-comparable by A8, A10, Th1;

hence contradiction by A6, A11, A12, TREES_1:def 10; :: thesis: verum

( q = p9 ^ r & p9 in P & (tree (T,P,T1)) . q = T1 . r ) by A6, A7, A8, A9; :: thesis: verum