defpred S_{1}[ FinSequence, set ] means ( for p being FinSequence of NAT st p in P holds

( not p is_a_prefix_of $1 & $2 = T . $1 ) or ex p, r being FinSequence of NAT st

( p in P & r in dom T1 & $1 = p ^ r & $2 = T1 . r ) );

A2: for q being FinSequence of NAT st q in tree ((dom T),P,(dom T1)) holds

ex x being set st S_{1}[q,x]

( dom T0 = tree ((dom T),P,(dom T1)) & ( for p being FinSequence of NAT st p in tree ((dom T),P,(dom T1)) holds

S_{1}[p,T0 . p] ) )
from TREES_2:sch 6(A2); :: thesis: verum

( not p is_a_prefix_of $1 & $2 = T . $1 ) or ex p, r being FinSequence of NAT st

( p in P & r in dom T1 & $1 = p ^ r & $2 = T1 . r ) );

A2: for q being FinSequence of NAT st q in tree ((dom T),P,(dom T1)) holds

ex x being set st S

proof

thus
ex T0 being DecoratedTree st
let q be FinSequence of NAT ; :: thesis: ( q in tree ((dom T),P,(dom T1)) implies ex x being set st S_{1}[q,x] )

assume q in tree ((dom T),P,(dom T1)) ; :: thesis: ex x being set st S_{1}[q,x]

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

not p is_a_prefix_of t } \/ { (p ^ s) where p is Element of dom T, s is Element of dom T1 : p in P } by A1, Th7;

_{1}[q,x]
by A3, A4, XBOOLE_0:def 3; :: thesis: verum

end;assume q in tree ((dom T),P,(dom T1)) ; :: thesis: ex x being set st S

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

not p is_a_prefix_of t } \/ { (p ^ s) where p is Element of dom T, s is Element of dom T1 : p in P } by A1, Th7;

A4: now :: thesis: ( q in { t where t is Element of dom T : for p being FinSequence of NAT st p in P holds

not p is_a_prefix_of t } implies ex x being set ex x being set st S_{1}[q,x] )

not p is_a_prefix_of t } implies ex x being set ex x being set st S

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

not p is_a_prefix_of t } ; :: thesis: ex x being set ex x being set st S_{1}[q,x]

then consider t being Element of dom T such that

A5: ( q = t & ( for p being FinSequence of NAT st p in P holds

not p is_a_prefix_of t ) ) ;

take x = T . t; :: thesis: ex x being set st S_{1}[q,x]

for p being FinSequence of NAT st p in P holds

( not p is_a_prefix_of q & x = T . q ) by A5;

hence ex x being set st S_{1}[q,x]
; :: thesis: verum

end;not p is_a_prefix_of t } ; :: thesis: ex x being set ex x being set st S

then consider t being Element of dom T such that

A5: ( q = t & ( for p being FinSequence of NAT st p in P holds

not p is_a_prefix_of t ) ) ;

take x = T . t; :: thesis: ex x being set st S

for p being FinSequence of NAT st p in P holds

( not p is_a_prefix_of q & x = T . q ) by A5;

hence ex x being set st S

now :: thesis: ( q in { (p ^ s) where p is Element of dom T, s is Element of dom T1 : p in P } implies ex x being set ex x being set st S_{1}[q,x] )

hence
ex x being set st Sassume
q in { (p ^ s) where p is Element of dom T, s is Element of dom T1 : p in P }
; :: thesis: ex x being set ex x being set st S_{1}[q,x]

then consider p being Element of dom T, s being Element of dom T1 such that

A6: ( q = p ^ s & p in P ) ;

take x = T1 . s; :: thesis: ex x being set st S_{1}[q,x]

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

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

( p in P & r in dom T1 & q = p ^ r & x = T1 . r ) ) by A6;

hence ex x being set st S_{1}[q,x]
; :: thesis: verum

end;then consider p being Element of dom T, s being Element of dom T1 such that

A6: ( q = p ^ s & p in P ) ;

take x = T1 . s; :: thesis: ex x being set st S

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

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

( p in P & r in dom T1 & q = p ^ r & x = T1 . r ) ) by A6;

hence ex x being set st S

( dom T0 = tree ((dom T),P,(dom T1)) & ( for p being FinSequence of NAT st p in tree ((dom T),P,(dom T1)) holds

S