| 〈build_rec#(i + 1; x2, to2)〉 (x2 = d0 ' + y0 ∧ to2 = some(t)), ∀ j0, i0, x, x0, to. i→n(j0 - i0) < i→n(i1) → (x = x0 ∧ x0 ≠ [] ∧ i0 ≤ j0 ∧ max(x0) ≤ j0 → 〈build_rec#(i0; x, to)〉 (to ≠ fail → x0 = depths(to .t, i0) + x)), x1 = d0 ' + y0, d ' + y = depths(t, i + 1) + d0 ' + y0, to2 = fail, x2 = d ' + y, 0 ≠ i1, max(d ' + y) < max(d0 ' + y0), i1 + i < max(d0 ' + y0), 0 < i1, i < d, max(d ' + y) ≤ i1 + i, d ∈ depths(t, i + 1) ⊦ 〈if d0 ≤ i then to := fail else if d0 = i + 1 then { x1 := pop(x1) ; to := some(Leaf) } else let to0 = fail, to1 = fail in { build_rec#(2 + i; x1, to0) ; if to0 = fail then to := fail else { build_rec#(2 + i; x1, to1) ; if to1 = fail then to := fail else to := some(Node(to0 .t, to1 .t)) } }〉 〈to2 := to ; if to2 = fail then to0 := fail else to0 := some(Node(t, to2 .t))〉 (to0 ≠ fail → d ' + y = depths(to0 .t, i) + x1) |
〈build_rec#(i + 1; x2, to2)〉 (x2 = d0 ' + y0 ∧ to2 = some(t)), ∀ j0, i0, x, x0, to. i→n(j0 - i0) < i→n(i1) → (x = x0 ∧ x0 ≠ [] ∧ i0 ≤ j0 ∧ max(x0) ≤ j0 → 〈build_rec#(i0; x, to)〉 (to ≠ fail → x0 = depths(to .t, i0) + x)), x1 = d0 ' + y0, to2 = fail, x2 = depths(t, i + 1) + d0 ' + y0, 0 ≠ i1, max(depths(t, i + 1) + d0 ' + y0) < max(d0 ' + y0), i1 + i < max(d0 ' + y0), 0 < i1, i < d, max(depths(t, i + 1) + d0 ' + y0) ≤ i1 + i, d ∈ depths(t, i + 1) ⊦ 〈if d0 ≤ i then to := fail else if d0 = i + 1 then { x1 := pop(x1) ; to := some(Leaf) } else let to0 = fail, to1 = fail in { build_rec#(2 + i; x1, to0) ; if to0 = fail then to := fail else { build_rec#(2 + i; x1, to1) ; if to1 = fail then to := fail else to := some(Node(to0 .t, to1 .t)) } }〉 〈to2 := to ; if to2 = fail then to0 := fail else to0 := some(Node(t, to2 .t))〉 (to0 ≠ fail → d ' + y = depths(to0 .t, i) + x1)
[[CONCRETESIMPRULES : ()]]