Proof step 49 from proof copy-stream-append (previous step)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 50:

  # buf1 = n2 + n1 + m, #(⌜buf0⌝ from n0) < ⌜m⌝ , n0 + m ≤ # buf0 ⊦ ⌜n2⌝ + ⌜m⌝ = #((⌜buf0⌝ from n0) to m) + #(⌜buf1⌝ from n1 + m)

Rule argument

Additional information