defpred S1[ 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 S1[q,x]
proof
let q be FinSequence of NAT ; :: thesis: ( q in tree ((dom T),P,(dom T1)) implies ex x being set st S1[q,x] )
assume q in tree ((dom T),P,(dom T1)) ; :: thesis: ex x being set st S1[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 ;
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 S1[q,x] )
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 S1[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 S1[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 S1[q,x] ; :: thesis: verum
end;
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 S1[q,x] )
assume 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 S1[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 S1[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 S1[q,x] ; :: thesis: verum
end;
hence ex x being set st S1[q,x] by ; :: thesis: verum
end;
thus ex T0 being DecoratedTree st
( dom T0 = tree ((dom T),P,(dom T1)) & ( for p being FinSequence of NAT st p in tree ((dom T),P,(dom T1)) holds
S1[p,T0 . p] ) ) from :: thesis: verum