Proof step 27 from proof encode (previous step)

User applied rule insert program lemma

And obtained the following new goals

• Proof step 28:

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

• Proof step 29:

  # buf2 = # vtbl * (ENCODED_VOLID_SIZE + ENCODED_NAT_SIZE), # buf0 = ENCODED_NAT_SIZE, # buf4 = (# buf2 + # buf3) + ENCODED_NAT_SIZE, # buf = # buf4, buf1 = buf0 + buf2 + buf3, subarray(buf4, ENCODED_NAT_SIZE, # buf2 + # buf3) = subarray(buf, ENCODED_NAT_SIZE, # buf2 + # buf3), is-encoded(#(vtbl1 ∪ vtbl), buf0), is-encoded-rec(vtbl, buf2), v ∈ vtbl1, # vtbl1 * (ENCODED_NAT_SIZE + ENCODED_VOLID_SIZE) ≤ # buf3, #(vtbl1 ∪ vtbl) * (ENCODED_NAT_SIZE + ENCODED_VOLID_SIZE) ≤ # buf2 + # buf3, vtbl1 ⊥ vtbl, err0 = ESUCCESS → is-encoded(#(vtbl1 ∪ vtbl), subarray(buf4, 0, ENCODED_NAT_SIZE)) ∧ n1 = ENCODED_NAT_SIZE, err0 = ESUCCESS ∨ ⌊err0⌋ ⊦ vtbl1 = ∅, v ∈ vtbl, (ENCODED_NAT_SIZE + # buf2) + encoding-size(v) ≤ # buf1 ∧ buf1 = buf1

• Proof step 35:

  # buf2 = # vtbl * (ENCODED_VOLID_SIZE + ENCODED_NAT_SIZE), # buf0 = ENCODED_NAT_SIZE, # buf4 = (# buf2 + # buf3) + ENCODED_NAT_SIZE, # buf = # buf4, buf1 = buf0 + buf2 + buf3, buf1 = buf1, buf5 = buf1, n2 = ENCODED_NAT_SIZE + # buf2, subarray(buf4, ENCODED_NAT_SIZE, # buf2 + # buf3) = subarray(buf, ENCODED_NAT_SIZE, # buf2 + # buf3), v0 = v, is-encoded(#(vtbl1 ∪ vtbl), buf0), is-encoded-rec(vtbl, buf2), v ∈ vtbl1, # vtbl1 * (ENCODED_NAT_SIZE + ENCODED_VOLID_SIZE) ≤ # buf3, #(vtbl1 ∪ vtbl) * (ENCODED_NAT_SIZE + ENCODED_VOLID_SIZE) ≤ # buf2 + # buf3, (ENCODED_NAT_SIZE + # buf2) + encoding-size(v) ≤ # buf1, vtbl1 ⊥ vtbl, err0 = ESUCCESS → is-encoded(#(vtbl1 ∪ vtbl), subarray(buf4, 0, ENCODED_NAT_SIZE)) ∧ n1 = ENCODED_NAT_SIZE, err0 = ESUCCESS ∨ ⌊err0⌋ ⊦ [encode_volid#(v, ENCODED_NAT_SIZE + # buf2; buf1, n; err)] ( (err = ESUCCESS ∨ ⌊err⌋ ) ∧ # buf1 = # buf5 ∧ subarray(buf1, 0, n2) = subarray(buf5, 0, n2) ∧ subarray(buf1, n2 + encoding-size(v0), # buf1 - n2 + encoding-size(v0)) = subarray(buf5, n2 + encoding-size(v0), # buf1 - n2 + encoding-size(v0)) ∧ (err = ESUCCESS → is-encoded(v0, subarray(buf1, n2, encoding-size(v0))) ∧ n = encoding-size(v0)) → ⟪vtbl0 := vtbl1; n0 := ENCODED_NAT_SIZE + # buf2; if err = ESUCCESS then {n0 := n0 + n; encode_nat#(vtbl0[v], n0; buf1, n; err); n0 := n0 + n}; vtbl0 := vtbl0 -- v⟫ ( (err = ESUCCESS ∨ ⌊err⌋ ) ∧ # buf1 = # buf4 ∧ ( err = ESUCCESS → (∃ buf0, buf2, buf5, vtbl3. buf1 = buf0 + buf2 + buf5 ∧ vtbl1 ∪ vtbl = vtbl0 ∪ vtbl3 ∧ vtbl0 ⊥ vtbl3 ∧ # buf0 + # buf2 = n0 ∧ # vtbl0 * (ENCODED_NAT_SIZE + ENCODED_VOLID_SIZE) ≤ # buf5 ∧ is-encoded(#(vtbl0 ∪ vtbl3), buf0) ∧ is-encoded-rec(vtbl3, buf2))) ∧ # vtbl0 < # vtbl1)), vtbl1 = ∅, v ∈ vtbl

Rule argument

Additional information