Proof step 88 from proof encode (previous step)

User applied rule case distinction

And obtained the following new goals

• Proof step 89:

  # buf4 = 2 * ENCODED_NAT_SIZE + n0 + # buf2 + ENCODED_VOLID_SIZE, # buf11 = 0, # buf7 = ENCODED_NAT_SIZE, # vtbl1 = m + 1, # buf1 = 0, # buf = 0, # buf8 = ENCODED_VOLID_SIZE, # buf0 = ENCODED_NAT_SIZE, # buf2 = # vtbl * (ENCODED_VOLID_SIZE + ENCODED_NAT_SIZE), # buf3 = 0, # buf10 = 0, ENCODED_NAT_SIZE + ENCODED_VOLID_SIZE + n0 = # buf9, ENCODED_NAT_SIZE + # buf2 + # buf9 = # buf4, ENCODED_NAT_SIZE = # buf5, is-encoded(#(vtbl1 ∪ vtbl), buf0), is-encoded(v, subarray(buf9, 0, ENCODED_VOLID_SIZE)), is-encoded(vtbl1[v], subarray(buf9, ENCODED_VOLID_SIZE, ENCODED_NAT_SIZE)), is-encoded-rec(vtbl, buf2), v ∈ vtbl1, ENCODED_NAT_SIZE + ENCODED_VOLID_SIZE ≤ # buf9, #(vtbl1 ∪ vtbl) * (ENCODED_NAT_SIZE + ENCODED_VOLID_SIZE) ≤ # buf2 + # buf9, (ENCODED_NAT_SIZE + ENCODED_VOLID_SIZE) * m ≤ n0, 2 * ENCODED_NAT_SIZE + # buf2 + ENCODED_VOLID_SIZE ≤ # buf4, ENCODED_NAT_SIZE + # buf2 + ENCODED_VOLID_SIZE ≤ # buf4, ENCODED_VOLID_SIZE ≤ # buf9, m * (ENCODED_NAT_SIZE + ENCODED_VOLID_SIZE) + ENCODED_NAT_SIZE + ENCODED_VOLID_SIZE ≤ # buf9, vtbl1 ⊥ vtbl, err0 = ESUCCESS → is-encoded(#(vtbl1 ∪ vtbl), subarray(buf4, 0, ENCODED_NAT_SIZE)) ∧ n1 = ENCODED_NAT_SIZE, err0 = ESUCCESS ∨ ⌊err0⌋ ⊦ vtbl1 = ∅, is-encoded-rec(vtbl[v, vtbl1[v]], buf2 + subarray(buf9, 0, ENCODED_NAT_SIZE + ENCODED_VOLID_SIZE)), v ∈ vtbl

• Proof step 97:

  # buf4 = 2 * ENCODED_NAT_SIZE + n0 + # buf2 + ENCODED_VOLID_SIZE, # buf11 = 0, # buf7 = ENCODED_NAT_SIZE, # vtbl1 = m + 1, # buf1 = 0, # buf = 0, # buf8 = ENCODED_VOLID_SIZE, # buf0 = ENCODED_NAT_SIZE, # buf2 = # vtbl * (ENCODED_VOLID_SIZE + ENCODED_NAT_SIZE), # buf3 = 0, # buf10 = 0, ENCODED_NAT_SIZE + ENCODED_VOLID_SIZE + n0 = # buf9, ENCODED_NAT_SIZE + # buf2 + # buf9 = # buf4, ENCODED_NAT_SIZE = # buf5, is-encoded(#(vtbl1 ∪ vtbl), buf0), is-encoded(v, subarray(buf9, 0, ENCODED_VOLID_SIZE)), is-encoded(vtbl1[v], subarray(buf9, ENCODED_VOLID_SIZE, ENCODED_NAT_SIZE)), is-encoded-rec(vtbl, buf2), v ∈ vtbl1, ENCODED_NAT_SIZE + ENCODED_VOLID_SIZE ≤ # buf9, #(vtbl1 ∪ vtbl) * (ENCODED_NAT_SIZE + ENCODED_VOLID_SIZE) ≤ # buf2 + # buf9, (ENCODED_NAT_SIZE + ENCODED_VOLID_SIZE) * m ≤ n0, 2 * ENCODED_NAT_SIZE + # buf2 + ENCODED_VOLID_SIZE ≤ # buf4, ENCODED_NAT_SIZE + # buf2 + ENCODED_VOLID_SIZE ≤ # buf4, ENCODED_VOLID_SIZE ≤ # buf9, m * (ENCODED_NAT_SIZE + ENCODED_VOLID_SIZE) + ENCODED_NAT_SIZE + ENCODED_VOLID_SIZE ≤ # buf9, vtbl1 ⊥ vtbl, err0 = ESUCCESS → is-encoded(#(vtbl1 ∪ vtbl), subarray(buf4, 0, ENCODED_NAT_SIZE)) ∧ n1 = ENCODED_NAT_SIZE, err0 = ESUCCESS ∨ ⌊err0⌋ ⊦ #(vtbl1 ∪ vtbl) = #((vtbl1 -- v) ∪ vtbl[v, vtbl1[v]]), vtbl1 = ∅, v ∈ vtbl

• Proof step 116:

  # buf4 = 2 * ENCODED_NAT_SIZE + n0 + # buf2 + ENCODED_VOLID_SIZE, # buf11 = 0, # buf7 = ENCODED_NAT_SIZE, # vtbl1 = m + 1, # buf1 = 0, # buf = 0, # buf8 = ENCODED_VOLID_SIZE, # buf0 = ENCODED_NAT_SIZE, # buf2 = # vtbl * (ENCODED_VOLID_SIZE + ENCODED_NAT_SIZE), # buf3 = 0, # buf10 = 0, ENCODED_NAT_SIZE + ENCODED_VOLID_SIZE + n0 = # buf9, ENCODED_NAT_SIZE + # buf2 + # buf9 = # buf4, ENCODED_NAT_SIZE = # buf5, is-encoded(#(vtbl1 ∪ vtbl), buf0), is-encoded(v, subarray(buf9, 0, ENCODED_VOLID_SIZE)), is-encoded(vtbl1[v], subarray(buf9, ENCODED_VOLID_SIZE, ENCODED_NAT_SIZE)), is-encoded-rec(vtbl, buf2), v ∈ vtbl1, ENCODED_NAT_SIZE + ENCODED_VOLID_SIZE ≤ # buf9, #(vtbl1 ∪ vtbl) * (ENCODED_NAT_SIZE + ENCODED_VOLID_SIZE) ≤ # buf2 + # buf9, (ENCODED_NAT_SIZE + ENCODED_VOLID_SIZE) * m ≤ n0, 2 * ENCODED_NAT_SIZE + # buf2 + ENCODED_VOLID_SIZE ≤ # buf4, ENCODED_NAT_SIZE + # buf2 + ENCODED_VOLID_SIZE ≤ # buf4, ENCODED_VOLID_SIZE ≤ # buf9, m * (ENCODED_NAT_SIZE + ENCODED_VOLID_SIZE) + ENCODED_NAT_SIZE + ENCODED_VOLID_SIZE ≤ # buf9, vtbl1 ⊥ vtbl, err0 = ESUCCESS → is-encoded(#(vtbl1 ∪ vtbl), subarray(buf4, 0, ENCODED_NAT_SIZE)) ∧ n1 = ENCODED_NAT_SIZE, err0 = ESUCCESS ∨ ⌊err0⌋ ⊦ vtbl1 = ∅, v ∈ vtbl, vtbl1 -- v ⊥ vtbl[v, vtbl1[v]]

• Proof step 118:

  # buf4 = 2 * ENCODED_NAT_SIZE + n0 + # buf2 + ENCODED_VOLID_SIZE, # buf11 = 0, # buf7 = ENCODED_NAT_SIZE, # vtbl1 = m + 1, # buf1 = 0, # buf = 0, # buf8 = ENCODED_VOLID_SIZE, # buf0 = ENCODED_NAT_SIZE, # buf2 = # vtbl * (ENCODED_VOLID_SIZE + ENCODED_NAT_SIZE), # buf3 = 0, # buf10 = 0, ENCODED_NAT_SIZE + ENCODED_VOLID_SIZE + n0 = # buf9, ENCODED_NAT_SIZE + # buf2 + # buf9 = # buf4, ENCODED_NAT_SIZE = # buf5, is-encoded(#(vtbl1 ∪ vtbl), buf0), is-encoded(v, subarray(buf9, 0, ENCODED_VOLID_SIZE)), is-encoded(vtbl1[v], subarray(buf9, ENCODED_VOLID_SIZE, ENCODED_NAT_SIZE)), is-encoded-rec(vtbl, buf2), v ∈ vtbl1, ENCODED_NAT_SIZE + ENCODED_VOLID_SIZE ≤ # buf9, #(vtbl1 ∪ vtbl) * (ENCODED_NAT_SIZE + ENCODED_VOLID_SIZE) ≤ # buf2 + # buf9, (ENCODED_NAT_SIZE + ENCODED_VOLID_SIZE) * m ≤ n0, 2 * ENCODED_NAT_SIZE + # buf2 + ENCODED_VOLID_SIZE ≤ # buf4, ENCODED_NAT_SIZE + # buf2 + ENCODED_VOLID_SIZE ≤ # buf4, ENCODED_VOLID_SIZE ≤ # buf9, m * (ENCODED_NAT_SIZE + ENCODED_VOLID_SIZE) + ENCODED_NAT_SIZE + ENCODED_VOLID_SIZE ≤ # buf9, vtbl1 ⊥ vtbl, err0 = ESUCCESS → is-encoded(#(vtbl1 ∪ vtbl), subarray(buf4, 0, ENCODED_NAT_SIZE)) ∧ n1 = ENCODED_NAT_SIZE, err0 = ESUCCESS ∨ ⌊err0⌋ ⊦ vtbl1 = ∅, vtbl1 ∪ vtbl = (vtbl1 -- v) ∪ vtbl[v, vtbl1[v]], v ∈ vtbl

• Proof step 136:

  # buf4 = 2 * ENCODED_NAT_SIZE + n0 + # buf2 + ENCODED_VOLID_SIZE, # buf11 = 0, # buf7 = ENCODED_NAT_SIZE, # vtbl1 = m + 1, # buf1 = 0, # buf = 0, # buf8 = ENCODED_VOLID_SIZE, # buf0 = ENCODED_NAT_SIZE, # buf2 = # vtbl * (ENCODED_VOLID_SIZE + ENCODED_NAT_SIZE), # buf3 = 0, # buf10 = 0, ENCODED_NAT_SIZE + ENCODED_VOLID_SIZE + n0 = # buf9, ENCODED_NAT_SIZE + # buf2 + # buf9 = # buf4, ENCODED_NAT_SIZE = # buf5, is-encoded(#(vtbl1 ∪ vtbl), buf0), is-encoded(v, subarray(buf9, 0, ENCODED_VOLID_SIZE)), is-encoded(vtbl1[v], subarray(buf9, ENCODED_VOLID_SIZE, ENCODED_NAT_SIZE)), is-encoded-rec(vtbl, buf2), v ∈ vtbl1, ENCODED_NAT_SIZE + ENCODED_VOLID_SIZE ≤ # buf9, #(vtbl1 ∪ vtbl) * (ENCODED_NAT_SIZE + ENCODED_VOLID_SIZE) ≤ # buf2 + # buf9, (ENCODED_NAT_SIZE + ENCODED_VOLID_SIZE) * m ≤ n0, 2 * ENCODED_NAT_SIZE + # buf2 + ENCODED_VOLID_SIZE ≤ # buf4, ENCODED_NAT_SIZE + # buf2 + ENCODED_VOLID_SIZE ≤ # buf4, ENCODED_VOLID_SIZE ≤ # buf9, m * (ENCODED_NAT_SIZE + ENCODED_VOLID_SIZE) + ENCODED_NAT_SIZE + ENCODED_VOLID_SIZE ≤ # buf9, vtbl1 ⊥ vtbl, err0 = ESUCCESS → is-encoded(#(vtbl1 ∪ vtbl), subarray(buf4, 0, ENCODED_NAT_SIZE)) ∧ n1 = ENCODED_NAT_SIZE, err0 = ESUCCESS ∨ ⌊err0⌋ ⊦ buf9 = subarray(buf9, 0, ENCODED_NAT_SIZE + ENCODED_VOLID_SIZE) + subarray(buf9, ENCODED_NAT_SIZE + ENCODED_VOLID_SIZE, n0), vtbl1 = ∅, v ∈ vtbl

Rule argument

Additional information