scheme :: TREES_9:sch 3
FinDecTree{ F₁() -> non empty set , F₂() -> finite-branching DecoratedTree of F₁(), F₃( Element of F₁()) -> Nat } :

provided

A1: for t, t9 being Element of dom F₂()
for d being Element of F₁() st t9 in succ t & d = F₂() . t9 holds
F₃(d) < F₃((F₂() . t))