:: deftheorem Def9 defines with-replacement TREES_1:def 9 :
for T being Tree
for p being FinSequence of NAT
for T1 being Tree st p in T holds
for b₄ being Tree holds
( b₄ = T with-replacement (p,T1) iff for q being FinSequence of NAT holds
( q in b₄ iff ( ( q in T & not p is_a_proper_prefix_of q ) or ex r being FinSequence of NAT st
( r in T1 & q = p ^ r ) ) ) );