[Imprint][Data Privacy Statement][E-Mail]

View long theorem info. View the proof. Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Proof step 59 from proof encode (previous step)

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

Heuristic elimination applied rule insert elim lemma

And obtained the following new goals

Proof step 60:
# buf6 = # buf4, # buf5 = # buf4, # buf2 = # vtbl * (ENCODED_VOLID_SIZE + ENCODED_NAT_SIZE), # buf0 = ENCODED_NAT_SIZE, # buf4 = (# buf2 + ENCODED_VOLID_SIZE + n2) + ENCODED_NAT_SIZE, # buf = # buf4, # buf3 = ENCODED_VOLID_SIZE + n2, # vtbl1 = m + 1, subarray(buf6, 0, (ENCODED_NAT_SIZE + # buf2) + ENCODED_VOLID_SIZE) = subarray(buf5, 0, (ENCODED_NAT_SIZE + # buf2) + ENCODED_VOLID_SIZE), subarray(buf6, 2 * ENCODED_NAT_SIZE + # buf2 + ENCODED_VOLID_SIZE, # buf4 - 2 * ENCODED_NAT_SIZE + # buf2 + ENCODED_VOLID_SIZE) = subarray(buf5, 2 * ENCODED_NAT_SIZE + # buf2 + ENCODED_VOLID_SIZE, # buf4 - 2 * ENCODED_NAT_SIZE + # buf2 + ENCODED_VOLID_SIZE), subarray(buf5, 0, ENCODED_NAT_SIZE + # buf2) = buf0 + buf2, subarray(buf5, ENCODED_NAT_SIZE + # buf2 + ENCODED_VOLID_SIZE, n2) = subarray(buf3, ENCODED_VOLID_SIZE, n2), subarray(buf4, ENCODED_NAT_SIZE, # buf2 + ENCODED_VOLID_SIZE + n2) = subarray(buf, ENCODED_NAT_SIZE, # buf2 + ENCODED_VOLID_SIZE + n2), is-encoded(v, subarray(buf5, ENCODED_NAT_SIZE + # buf2, ENCODED_VOLID_SIZE)), is-encoded(#(vtbl1 ∪ vtbl), buf0), is-encoded(vtbl1[v], subarray(buf6, (ENCODED_NAT_SIZE + # buf2) + ENCODED_VOLID_SIZE, ENCODED_NAT_SIZE)), is-encoded-rec(vtbl, buf2), v ∈ vtbl1, ENCODED_NAT_SIZE + # buf2 + ENCODED_VOLID_SIZE ≤ # buf4, # vtbl1 * (ENCODED_NAT_SIZE + ENCODED_VOLID_SIZE) ≤ ENCODED_VOLID_SIZE + n2, #(vtbl1 ∪ vtbl) * (ENCODED_NAT_SIZE + ENCODED_VOLID_SIZE) ≤ # buf2 + ENCODED_VOLID_SIZE + n2, 2 * ENCODED_NAT_SIZE + # buf2 + ENCODED_VOLID_SIZE ≤ # buf4, vtbl1 ⊥ vtbl, err0 = ESUCCESS → is-encoded(#(vtbl1 ∪ vtbl), subarray(buf4, 0, ENCODED_NAT_SIZE)) ∧ n1 = ENCODED_NAT_SIZE, err0 = ESUCCESS ∨ ⌊err0⌋ ⊦ # vtbl1 = 0, vtbl1 = ∅, v ∈ vtbl, ∃ buf1, buf7, buf8, vtbl0. buf6 = buf1 + buf7 + buf8 ∧ vtbl1 ∪ vtbl = (vtbl1 -- v) ∪ vtbl0 ∧ vtbl1 -- v ⊥ vtbl0 ∧ # buf1 + # buf7 = 2 * ENCODED_NAT_SIZE + # buf2 + ENCODED_VOLID_SIZE ∧ m * (ENCODED_NAT_SIZE + ENCODED_VOLID_SIZE) ≤ # buf8 ∧ is-encoded(#((vtbl1 -- v) ∪ vtbl0), buf1) ∧ is-encoded-rec(vtbl0, buf7)

Rule argument

spec: nat name: elim-pred-c seq: n ≠ 0 ⊦ m = n - 1 ↔ n = m + 1 subst: [n, m] → [# vtbl1, m]

Additional information

Used simplifier rules: ⊦ # vtbl = 0 ↔ vtbl = ∅; (s)%# buf = n ⊦ subarray(buf, 0, n) = buf; (s)%n ≠ 0 ⊦ m = n - 1 ↔ n = m + 1; (elim) Used terms: # vtbl1, m