[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 88 from proof encode-node (previous step)

# buf2 = # buf, # buf0 = # buf, # buf = n0 + n + 2 * NODE_HEADER_SIZE + n2 + node-size-headerless(nd), align↑(node-size-headerless(nd), 2 * NODE_HEADER_SIZE) = n2 + node-size-headerless(nd), subarray(buf2, 0, n + NODE_HEADER_SIZE) = subarray(buf0, 0, n + NODE_HEADER_SIZE), subarray(buf2, (n + NODE_HEADER_SIZE) + node-size-headerless(nd), NODE_HEADER_SIZE + n0 + n2) = subarray(buf0, (n + NODE_HEADER_SIZE) + node-size-headerless(nd), NODE_HEADER_SIZE + n0 + n2), subarray(buf0, 0, n) = subarray(buf, 0, n), subarray(buf0, n + NODE_HEADER_SIZE, node-size-headerless(nd) + NODE_HEADER_SIZE + n0 + n2) = subarray(buf, n + NODE_HEADER_SIZE, node-size-headerless(nd) + NODE_HEADER_SIZE + n0 + n2), is-encoded(nodeheader(node-size-headerless(nd), false), subarray(buf0, n, NODE_HEADER_SIZE)), is-encoded(nd, subarray(buf2, n + NODE_HEADER_SIZE, node-size-headerless(nd))), n + NODE_HEADER_SIZE + node-size-headerless(nd) ≤ # buf, (n + NODE_HEADER_SIZE + node-size-headerless(nd)) + n2 ≤ # buf, (n + NODE_HEADER_SIZE) + node-size-headerless(nd) ≤ # buf, n + NODE_HEADER_SIZE ≤ # buf, n + 2 * NODE_HEADER_SIZE + n2 + node-size-headerless(nd) ≤ # buf, (n2 + node-size-headerless(nd)) + n + NODE_HEADER_SIZE ≤ # buf, 2 * NODE_HEADER_SIZE + n + n2 + node-size-headerless(nd) ≤ # buf ⊦ subarray ((subarray(buf2, 0, n + NODE_HEADER_SIZE + node-size-headerless(nd)) + fill(mkbuf(n2), empty)) + validtrailer, n, 2 * NODE_HEADER_SIZE + n2 + node-size-headerless(nd)) = subarray(buf0, n, NODE_HEADER_SIZE) + (subarray(buf2, n + NODE_HEADER_SIZE, node-size-headerless(nd)) + mkempbuf(n2)) + validtrailer

User applied rule insert rewrite lemma

And obtained the following new goals

Proof step 89:
⊦ buf = buf0 ↔ # buf = # buf0 ∧ (∀ n. n < # buf → buf[n] = buf0[n])
Proof step 90:
# buf = n0 + n + 2 * NODE_HEADER_SIZE + n2 + node-size-headerless(nd), # buf0 = # buf, # buf2 = # buf, align↑(node-size-headerless(nd), 2 * NODE_HEADER_SIZE) = n2 + node-size-headerless(nd), subarray(buf0, n + NODE_HEADER_SIZE, node-size-headerless(nd) + NODE_HEADER_SIZE + n0 + n2) = subarray(buf, n + NODE_HEADER_SIZE, node-size-headerless(nd) + NODE_HEADER_SIZE + n0 + n2), subarray(buf0, 0, n) = subarray(buf, 0, n), subarray(buf2, (n + NODE_HEADER_SIZE) + node-size-headerless(nd), NODE_HEADER_SIZE + n0 + n2) = subarray(buf0, (n + NODE_HEADER_SIZE) + node-size-headerless(nd), NODE_HEADER_SIZE + n0 + n2), subarray(buf2, 0, n + NODE_HEADER_SIZE) = subarray(buf0, 0, n + NODE_HEADER_SIZE), is-encoded(nd, subarray(buf2, n + NODE_HEADER_SIZE, node-size-headerless(nd))), is-encoded(nodeheader(node-size-headerless(nd), false), subarray(buf0, n, NODE_HEADER_SIZE)), 2 * NODE_HEADER_SIZE + n + n2 + node-size-headerless(nd) ≤ # buf, (n2 + node-size-headerless(nd)) + n + NODE_HEADER_SIZE ≤ # buf, n + 2 * NODE_HEADER_SIZE + n2 + node-size-headerless(nd) ≤ # buf, n + NODE_HEADER_SIZE ≤ # buf, (n + NODE_HEADER_SIZE) + node-size-headerless(nd) ≤ # buf, (n + NODE_HEADER_SIZE + node-size-headerless(nd)) + n2 ≤ # buf, n + NODE_HEADER_SIZE + node-size-headerless(nd) ≤ # buf ⊦ # subarray ((subarray(buf2, 0, n + NODE_HEADER_SIZE + node-size-headerless(nd)) + fill(mkbuf(n2), empty)) + validtrailer, n, 2 * NODE_HEADER_SIZE + n2 + node-size-headerless(nd)) = #(subarray(buf0, n, NODE_HEADER_SIZE) + (subarray(buf2, n + NODE_HEADER_SIZE, node-size-headerless(nd)) + mkempbuf(n2)) + validtrailer) ∧ (∀ n0. n0 < # subarray ((subarray(buf2, 0, n + NODE_HEADER_SIZE + node-size-headerless(nd)) + fill(mkbuf(n2), empty)) + validtrailer, n, 2 * NODE_HEADER_SIZE + n2 + node-size-headerless(nd)) → subarray ((subarray(buf2, 0, n + NODE_HEADER_SIZE + node-size-headerless(nd)) + fill(mkbuf(n2), empty)) + validtrailer, n, 2 * NODE_HEADER_SIZE + n2 + node-size-headerless(nd)) [n0 ] = (subarray(buf0, n, NODE_HEADER_SIZE) + (subarray(buf2, n + NODE_HEADER_SIZE, node-size-headerless(nd)) + mkempbuf(n2)) + validtrailer)[n0])

Rule argument

spec: array, inst: buffer name: Extension seq: ⊦ buf = buf0 ↔ # buf = # buf0 ∧ (∀ n. n < # buf → buf[n] = buf0[n]) subst: [buf0, buf] → [ subarray(buf0, n, NODE_HEADER_SIZE) + ( subarray (buf2, n + NODE_HEADER_SIZE, node-size-headerless(nd)) + mkempbuf(n2)) + validtrailer, subarray ( ( subarray (buf2, 0, n + NODE_HEADER_SIZE + node-size-headerless(nd)) + fill(mkbuf(n2), empty)) + validtrailer, n, 2 * NODE_HEADER_SIZE + n2 + node-size-headerless(nd))] flags: <all paths>

Additional information

Used terms: subarray(buf0, n, NODE_HEADER_SIZE) + ( subarray(buf2, n + NODE_HEADER_SIZE, node-size-headerless(nd)) + mkempbuf(n2)) + validtrailer, subarray ( ( subarray (buf2, 0, n + NODE_HEADER_SIZE + node-size-headerless(nd)) + fill(mkbuf(n2), empty)) + validtrailer, n, 2 * NODE_HEADER_SIZE + n2 + node-size-headerless(nd))