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 )
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, Th13;
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 )
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;
A6: now
assume (tree T,P,T1) . q <> T1 . r ; :: thesis: contradiction
A7: not p9 is_a_prefix_of q by A3, A5;
thus contradiction by A4, A7, TREES_1:8; :: thesis: verum
end;
thus 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, A6; :: thesis: verum
end;
suppose A8: 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 )
consider p, r being FinSequence of NAT such that
A9: p in P and
A10: r in dom T1 and
A11: q = p ^ r and
A12: (tree T,P,T1) . q = T1 . r by A8;
consider p9 being Element of dom T, r9 being Element of dom T1 such that
A13: q = p9 ^ r9 and
A14: p9 in P by A2;
thus 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 A9, A10, A11, A12, A15; :: thesis: verum
end;
end;