Proof step 1 from proof inv-add (conclusion)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  # xs = xs_len, # xs < h, # ys = 0 ∨ # ys = h ⊦ ⟪caterpillar_add#(a, h; xs, xs_len, ys)⟫ (# xs < h ∧ # xs = xs_len ∧ (# ys = 0 ∨ # ys = h))

Rule argument

Additional information