Proof step 14 from proof prepost-encode-lpt (previous step)

User applied rule insert program lemma

And obtained the following new goals

• Proof step 15:

  n + encoding-size(lp) ≤ # buf, buf0 = buf ⊦ ⟪encode_lprops#(lp, n; buf, n0; err)⟫ ( (err = ESUCCESS ∨ ⌊err⌋ ) ∧ # buf = # buf0 ∧ subarray(buf, 0, n) = subarray(buf0, 0, n) ∧ subarray(buf, n + encoding-size(lp), # buf - n + encoding-size(lp)) = subarray(buf0, n + encoding-size(lp), # buf - n + encoding-size(lp)) ∧ (err = ESUCCESS → is-encoded(lp, subarray(buf, n, encoding-size(lp))) ∧ n0 = encoding-size(lp)))

• Proof step 16:

  # buf = lptsize(n1 + n0, LEB_SIZE), # lpt = n1 + n0, is-encoded(lpt, buf, n0) ⊦ n1 = 0, n0 * ENCODED_LPROPS_SIZE + encoding-size(lpt[n0]) ≤ # buf ∧ buf = buf

• Proof step 20:

  # buf = lptsize(n1 + n0, LEB_SIZE), # lpt = n1 + n0, buf = buf, buf1 = buf, lp0 = lpt[n0], n2 = n0 * ENCODED_LPROPS_SIZE, is-encoded(lpt, buf, n0), n0 * ENCODED_LPROPS_SIZE + encoding-size(lpt[n0]) ≤ # buf ⊦ [encode_lprops#(lpt[n0], n0 * ENCODED_LPROPS_SIZE; buf, m; err)] ( (err = ESUCCESS ∨ ⌊err⌋ ) ∧ # buf = # buf1 ∧ subarray(buf, 0, n2) = subarray(buf1, 0, n2) ∧ subarray(buf, n2 + encoding-size(lp0), # buf - n2 + encoding-size(lp0)) = subarray(buf1, n2 + encoding-size(lp0), # buf - n2 + encoding-size(lp0)) ∧ (err = ESUCCESS → is-encoded(lp0, subarray(buf, n2, encoding-size(lp0))) ∧ m = encoding-size(lp0)) → ⟪n := n0 + 1⟫ ( n ≤ # lpt ∧ # buf = lptsize(# lpt, LEB_SIZE) ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ (err = ESUCCESS → is-encoded(lpt, buf, n)) ∧ # lpt < n1 + n)), n1 = 0

Rule argument

Additional information