let p be FinSequence of NAT ; :: thesis: for T, T1 being DecoratedTree st p in dom T holds

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

ex r being Element of dom T1 st

( q = p ^ r & (T with-replacement (p,T1)) . q = T1 . r )

let T, T1 be DecoratedTree; :: thesis: ( p in dom T implies for q being FinSequence of NAT st q in dom (T with-replacement (p,T1)) & q in { (p ^ s) where s is Element of dom T1 : verum } holds

ex r being Element of dom T1 st

( q = p ^ r & (T with-replacement (p,T1)) . q = T1 . r ) )

assume A1: p in dom T ; :: thesis: for q being FinSequence of NAT st q in dom (T with-replacement (p,T1)) & q in { (p ^ s) where s is Element of dom T1 : verum } holds

ex r being Element of dom T1 st

( q = p ^ r & (T with-replacement (p,T1)) . q = T1 . r )

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

( q = p ^ r & (T with-replacement (p,T1)) . q = T1 . r ) )

assume that

A2: q in dom (T with-replacement (p,T1)) and

A3: q in { (p ^ s) where s is Element of dom T1 : verum } ; :: thesis: ex r being Element of dom T1 st

( q = p ^ r & (T with-replacement (p,T1)) . q = T1 . r )

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

ex r being Element of dom T1 st

( q = p ^ r & (T with-replacement (p,T1)) . q = T1 . r )

let T, T1 be DecoratedTree; :: thesis: ( p in dom T implies for q being FinSequence of NAT st q in dom (T with-replacement (p,T1)) & q in { (p ^ s) where s is Element of dom T1 : verum } holds

ex r being Element of dom T1 st

( q = p ^ r & (T with-replacement (p,T1)) . q = T1 . r ) )

assume A1: p in dom T ; :: thesis: for q being FinSequence of NAT st q in dom (T with-replacement (p,T1)) & q in { (p ^ s) where s is Element of dom T1 : verum } holds

ex r being Element of dom T1 st

( q = p ^ r & (T with-replacement (p,T1)) . q = T1 . r )

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

( q = p ^ r & (T with-replacement (p,T1)) . q = T1 . r ) )

assume that

A2: q in dom (T with-replacement (p,T1)) and

A3: q in { (p ^ s) where s is Element of dom T1 : verum } ; :: thesis: ex r being Element of dom T1 st

( q = p ^ r & (T with-replacement (p,T1)) . q = T1 . r )

per cases
( ( not p is_a_prefix_of q & (T with-replacement (p,T1)) . q = T . q ) or ex r being FinSequence of NAT st

( r in dom T1 & q = p ^ r & (T with-replacement (p,T1)) . q = T1 . r ) ) by A1, A2, Th11;

end;

( r in dom T1 & q = p ^ r & (T with-replacement (p,T1)) . q = T1 . r ) ) by A1, A2, Th11;

suppose A4:
( not p is_a_prefix_of q & (T with-replacement (p,T1)) . q = T . q )
; :: thesis: ex r being Element of dom T1 st

( q = p ^ r & (T with-replacement (p,T1)) . q = T1 . r )

( q = p ^ r & (T with-replacement (p,T1)) . q = T1 . r )

ex r being Element of dom T1 st q = p ^ r
by A3;

hence ex r being Element of dom T1 st

( q = p ^ r & (T with-replacement (p,T1)) . q = T1 . r ) by A4, TREES_1:1; :: thesis: verum

end;hence ex r being Element of dom T1 st

( q = p ^ r & (T with-replacement (p,T1)) . q = T1 . r ) by A4, TREES_1:1; :: thesis: verum

suppose
ex r being FinSequence of NAT st

( r in dom T1 & q = p ^ r & (T with-replacement (p,T1)) . q = T1 . r ) ; :: thesis: ex r being Element of dom T1 st

( q = p ^ r & (T with-replacement (p,T1)) . q = T1 . r )

( r in dom T1 & q = p ^ r & (T with-replacement (p,T1)) . q = T1 . r ) ; :: thesis: ex r being Element of dom T1 st

( q = p ^ r & (T with-replacement (p,T1)) . q = T1 . r )

hence
ex r being Element of dom T1 st

( q = p ^ r & (T with-replacement (p,T1)) . q = T1 . r ) ; :: thesis: verum

end;( q = p ^ r & (T with-replacement (p,T1)) . q = T1 . r ) ; :: thesis: verum