| 〈build_rec#(i + 1; x2, to2)〉 (x2 = x1 ∧ 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)), x2 = d ' + y, to2 = fail, d ' + y = depths(t, i + 1) + x1, 0 ≠ i1, d ∈ depths(t, i + 1), max(d ' + y) ≤ i1 + i, i < d, 0 < i1, i1 + i < max(x1), max(d ' + y) < max(x1) ⊦ 〈x := x1, d0 := i + 1〉 〈if is_empty(x) then to := fail else let h = head(x) in if h < d0 then to := fail else if h = d0 then { x := pop(x) ; to := some(Leaf) } else let to0 = fail, to1 = fail in { build_rec#(d0 + 1; x, to0) ; if to0 = fail then to := fail else { build_rec#(d0 + 1; x, 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) + x) |
〈build_rec#(i + 1; x2, to2)〉 (x2 = x1 ∧ 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)), x2 = d ' + y, to2 = fail, d ' + y = depths(t, i + 1) + x1, 0 ≠ i1, d ∈ depths(t, i + 1), max(d ' + y) ≤ i1 + i, i < d, 0 < i1, i1 + i < max(x1), max(d ' + y) < max(x1), x0 = x1 ∧ d1 = i + 1 ⊦ 〈if is_empty(x0) then to := fail else let h = head(x0) in if h < d1 then to := fail else if h = d1 then { x0 := pop(x0) ; to := some(Leaf) } else let to0 = fail, to1 = fail in { build_rec#(d1 + 1; x0, to0) ; if to0 = fail then to := fail else { build_rec#(d1 + 1; x0, 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) + x0)
[[CONCRETESIMPRULES : ()]]