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

# 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), n1 < NODE_HEADER_SIZE + node-size-headerless(nd) + n2, n1 < 2 * NODE_HEADER_SIZE + n2 + node-size-headerless(nd), n1 < 2 * NODE_HEADER_SIZE + node-size-headerless(nd) + n2, 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 ⊦ (n1 < NODE_HEADER_SIZE + node-size-headerless(nd) ⊃ subarray(buf2, 0, n + NODE_HEADER_SIZE + node-size-headerless(nd))[n + n1] ;fill(mkbuf(n2), empty)[n1 - NODE_HEADER_SIZE + node-size-headerless(nd)] ) = (n1 < NODE_HEADER_SIZE ⊃ buf0[n + n1] ;((subarray(buf2, n + NODE_HEADER_SIZE, node-size-headerless(nd)) + mkempbuf(n2)) + validtrailer)[n1 - NODE_HEADER_SIZE] )

User applied rule case distinction

And obtained the following new goals

Proof step 102:
# 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), n1 < 2 * NODE_HEADER_SIZE + node-size-headerless(nd) + n2, n1 < 2 * NODE_HEADER_SIZE + n2 + node-size-headerless(nd), n1 < NODE_HEADER_SIZE + node-size-headerless(nd) + n2, n1 < NODE_HEADER_SIZE + node-size-headerless(nd), 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(buf2, 0, n + NODE_HEADER_SIZE + node-size-headerless(nd))[n + n1] = (n1 < NODE_HEADER_SIZE ⊃ buf0[n + n1] ;((subarray(buf2, n + NODE_HEADER_SIZE, node-size-headerless(nd)) + mkempbuf(n2)) + validtrailer)[n1 - NODE_HEADER_SIZE] )
Proof step 118:
# 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), n1 < 2 * NODE_HEADER_SIZE + node-size-headerless(nd) + n2, n1 < 2 * NODE_HEADER_SIZE + n2 + node-size-headerless(nd), n1 < NODE_HEADER_SIZE + node-size-headerless(nd) + 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 ⊦ fill(mkbuf(n2), empty)[n1 - NODE_HEADER_SIZE + node-size-headerless(nd)] = (n1 < NODE_HEADER_SIZE ⊃ buf0[n + n1] ;((subarray(buf2, n + NODE_HEADER_SIZE, node-size-headerless(nd)) + mkempbuf(n2)) + validtrailer)[n1 - NODE_HEADER_SIZE] ), n1 < NODE_HEADER_SIZE + node-size-headerless(nd)

Rule argument

pos: right 1

Proof step 101 from proof encode-node (previous step)

User applied rule case distinction

And obtained the following new goals

Rule argument

Additional information