Proof step 9 from proof completeness (previous step)

Heuristic weak unfold applied rule call right

And obtained the following new goals

• Proof step 2:

  ⊦

• Proof step 8:

  x = [] ⊦ 〈x0 := x, d := 0〉 〈if is_empty(x0) then to0 := fail else let h = head(x0) in if h < d then to0 := fail else if h = d then { x0 := pop(x0) ; to0 := some(Leaf) } else let to2 = fail, to1 = fail in { build_rec#(d + 1; x0, to2) ; if to2 = fail then to0 := fail else { build_rec#(d + 1; x0, to1) ; if to1 = fail then to0 := fail else to0 := some(Node(to2 .t, to1 .t)) } }〉 〈to1 := to0, x1 := x0 ; if x1 ≠ [] then to1 := fail〉 true

Rule argument

Additional information

[[CONCRETESIMPRULES : ()]]