:: deftheorem defines with-replacement TREES_2:def 11 :
for T being DecoratedTree
for p being FinSequence of NAT
for T1 being DecoratedTree st p in dom T holds
for b₄ being DecoratedTree holds
( b₄ = T with-replacement (p,T1) iff ( dom b₄ = (dom T) with-replacement (p,(dom T1)) & ( for q being FinSequence of NAT holds
( not q in (dom T) with-replacement (p,(dom T1)) or ( not p is_a_prefix_of q & b₄ . q = T . q ) or ex r being FinSequence of NAT st
( r in dom T1 & q = p ^ r & b₄ . q = T1 . r ) ) ) ) );