let T, T1 be DecoratedTree; :: thesis: for P being AntiChain_of_Prefixes of dom T st P <> {} holds

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

not p is_a_prefix_of t1 } holds

(tree (T,P,T1)) . q = T . q

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

not p is_a_prefix_of t1 } holds

(tree (T,P,T1)) . q = T . q )

assume A1: P <> {} ; :: thesis: for q being FinSequence of NAT st q in dom (tree (T,P,T1)) & q in { t1 where t1 is Element of dom T : for p being FinSequence of NAT st p in P holds

not p is_a_prefix_of t1 } holds

(tree (T,P,T1)) . q = T . q

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

not p is_a_prefix_of t1 } implies (tree (T,P,T1)) . q = T . q )

assume that

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

A3: q in { t1 where t1 is Element of dom T : for p being FinSequence of NAT st p in P holds

not p is_a_prefix_of t1 } ; :: thesis: (tree (T,P,T1)) . q = T . q

A4: ex t9 being Element of dom T st

( t9 = q & ( for p being FinSequence of NAT st p in P holds

not p is_a_prefix_of t9 ) ) by A3;

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

not p is_a_prefix_of t1 } holds

(tree (T,P,T1)) . q = T . q

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

not p is_a_prefix_of t1 } holds

(tree (T,P,T1)) . q = T . q )

assume A1: P <> {} ; :: thesis: for q being FinSequence of NAT st q in dom (tree (T,P,T1)) & q in { t1 where t1 is Element of dom T : for p being FinSequence of NAT st p in P holds

not p is_a_prefix_of t1 } holds

(tree (T,P,T1)) . q = T . q

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

not p is_a_prefix_of t1 } implies (tree (T,P,T1)) . q = T . q )

assume that

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

A3: q in { t1 where t1 is Element of dom T : for p being FinSequence of NAT st p in P holds

not p is_a_prefix_of t1 } ; :: thesis: (tree (T,P,T1)) . q = T . q

A4: ex t9 being Element of dom T st

( t9 = q & ( for p being FinSequence of NAT st p in P holds

not p is_a_prefix_of t9 ) ) by A3;

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 A2, 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 A2, Th10;

suppose A5:
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: (tree (T,P,T1)) . q = T . q

( not p is_a_prefix_of q & (tree (T,P,T1)) . q = T . q ) ; :: thesis: (tree (T,P,T1)) . q = T . q

consider x being object such that

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

ex p9 being FinSequence of NAT st p9 = x ;

hence (tree (T,P,T1)) . q = T . q by A5, A6; :: thesis: verum

end;A6: 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 A6;

ex p9 being FinSequence of NAT st p9 = x ;

hence (tree (T,P,T1)) . q = T . q by A5, A6; :: 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: (tree (T,P,T1)) . q = T . q

( p in P & r in dom T1 & q = p ^ r & (tree (T,P,T1)) . q = T1 . r ) ; :: thesis: (tree (T,P,T1)) . q = T . q

then consider p, r being FinSequence of NAT such that

A7: p in P and

r in dom T1 and

A8: q = p ^ r and

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

not p is_a_prefix_of q by A4, A7;

hence (tree (T,P,T1)) . q = T . q by A8, TREES_1:1; :: thesis: verum

end;A7: p in P and

r in dom T1 and

A8: q = p ^ r and

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

not p is_a_prefix_of q by A4, A7;

hence (tree (T,P,T1)) . q = T . q by A8, TREES_1:1; :: thesis: verum