scheme :: DTCONSTR:sch 6
DTCUniq{ F₁() -> Function, F₂() -> non empty DTConstrStr , F₃() -> non empty set , F₄( set ) -> Element of F₃(), F₅( set , set , set ) -> Element of F₃() } :

for dt1, dt2 being DecoratedTree of [: the carrier of F₂(),F₃():] st dt1 in Union F₁() & dt2 in Union F₁() & dt1 `1 = dt2 `1 holds
dt1 = dt2

provided

A1: dom F₁() = NAT and
A2: F₁() . 0 = { (root-tree [t,d]) where t is Symbol of F₂(), d is Element of F₃() : ( ( t in Terminals F₂() & d = F₄(t) ) or ( t ==> {} & d = F₅(t,{},{}) ) ) } and
A3: for n being Nat holds F₁() . (n + 1) = (F₁() . n) \/ { ([o,F₅(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p) where o is Symbol of F₂(), p is Element of (F₁() . n) * : ex q being FinSequence of FinTrees [: the carrier of F₂(),F₃():] st
( p = q & o ==> pr1 (roots q) ) }