[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 44 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), 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)), (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, 2 * NODE_HEADER_SIZE + n + n2 + node-size-headerless(nd) ≤ # buf, NODE_HEADER_SIZE ≤ # validtrailer, (n + NODE_HEADER_SIZE + n2 + node-size-headerless(nd)) + NODE_HEADER_SIZE ≤ # fill(buf2, empty, n + NODE_HEADER_SIZE + node-size-headerless(nd), n2) ⊦ subarray(fill(buf2, empty, n + NODE_HEADER_SIZE + node-size-headerless(nd), n2), 0, n) = subarray(buf, 0, n) ∧ subarray(fill(buf2, empty, n + NODE_HEADER_SIZE + node-size-headerless(nd), n2), n + 2 * NODE_HEADER_SIZE + n2 + node-size-headerless(nd), n0) = subarray(buf, n + 2 * NODE_HEADER_SIZE + n2 + node-size-headerless(nd), n0) ∧ (∃ buf, buf1. subarray ( subarray (fill(buf2, empty, n + NODE_HEADER_SIZE + node-size-headerless(nd), n2), 0, n + NODE_HEADER_SIZE + n2 + node-size-headerless(nd)) + subarray(validtrailer, 0, NODE_HEADER_SIZE) + subarray (fill(buf2, empty, n + NODE_HEADER_SIZE + node-size-headerless(nd), n2), (n + NODE_HEADER_SIZE + n2 + node-size-headerless(nd)) + NODE_HEADER_SIZE, # fill(buf2, empty, n + NODE_HEADER_SIZE + node-size-headerless(nd), n2) - n + NODE_HEADER_SIZE + n2 + node-size-headerless(nd) - NODE_HEADER_SIZE), n, 2 * NODE_HEADER_SIZE + n2 + node-size-headerless(nd)) = buf + buf1 + validtrailer ∧ is-encoded(nodeheader(node-size-headerless(nd), false), buf) ∧ is-encoded(nd, subarray(buf1, 0, node-size-headerless(nd))) ∧ # buf1 = n2 + node-size-headerless(nd))

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 45:
# 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 ≤ # 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(fill(buf2, empty, n + NODE_HEADER_SIZE + node-size-headerless(nd), n2), 0, n) = subarray(buf, 0, n) ∧ subarray(fill(buf2, empty, n + NODE_HEADER_SIZE + node-size-headerless(nd), n2), n + 2 * NODE_HEADER_SIZE + n2 + node-size-headerless(nd), n0) = subarray(buf, n + 2 * NODE_HEADER_SIZE + n2 + node-size-headerless(nd), n0) ∧ (∃ buf1, buf3. subarray ( subarray (fill(buf2, empty, n + NODE_HEADER_SIZE + node-size-headerless(nd), n2), 0, n + NODE_HEADER_SIZE + n2 + node-size-headerless(nd)) + validtrailer, n, 2 * NODE_HEADER_SIZE + n2 + node-size-headerless(nd)) = buf1 + buf3 + validtrailer ∧ is-encoded(nodeheader(node-size-headerless(nd), false), buf1) ∧ is-encoded(nd, subarray(buf3, 0, node-size-headerless(nd))) ∧ # buf3 = n2 + node-size-headerless(nd))

Rule argument

Additional information

Used simplifier rules: n + m ≤ # buf ⊦ subarray(buf + buf0, n, m) = subarray(buf, n, m); (s)% ⊦ ¬ n < n; (s)% ⊦ m ≤ n ↔ ¬ n < m; (ss)% ⊦ m + n ≤ m + n0 ↔ n ≤ n0; (s)% ⊦ # subarray(buf, m, n) = n; (s)% ⊦ #(buf + buf0) = # buf + # buf0; (s)%append-a: ⊦ (buf + buf0) + buf1 = buf + buf0 + buf1; from specification array-splice[buffer]%# buf = n ⊦ subarray(buf, 0, n) = buf; (s)% ⊦ m ≤ m; (s)% ⊦ # validtrailer = NODE_HEADER_SIZE; (s)% ⊦ # fill(buf, d, m, n) = # buf; (s)%c: ⊦ m + n = n + m; from specification nat-basic%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic% ⊦ m + m = 2 * m; (s)