for T, T1 being DecoratedTree
for P being AntiChain_of_Prefixes of dom T st P <> {} holds
for q being FinSequence of NAT holds
( not q in dom (tree (T,P,T1)) or for p being FinSequence of NAT st p in P holds
( not p is_a_prefix_of q & (tree (T,P,T1)) . q = T . q ) or ex p, r being FinSequence of NAT st
( p in P & r in dom T1 & q = p ^ r & (tree (T,P,T1)) . q = T1 . r ) )