Proof step 142 from proof abs-nodes-crash-h (previous step)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 143:

  # buf = align↑(node-size-headerless(nd), 2 * NODE_HEADER_SIZE), # buf2 = NODE_HEADER_SIZE, # buf < n0, n0 < NODE_HEADER_SIZE + # buf, abs-nodes(buf0, 2 * NODE_HEADER_SIZE + m + # buf, x1, lax1, true), is-aligned(n0, NODE_HEADER_SIZE), is-encoded(nodeheader(node-size-headerless(nd), false), buf2), is-encoded(nd, subarray(buf, 0, node-size-headerless(nd))), n0 ≤ NODE_HEADER_SIZE + # buf + # buf0, ∀ buf3, m, x, lax, n. # buf3 < #(buf2 + (buf + validtrailer) + buf0) → abs-nodes(buf3, m, x, lax, true) ∧ is-aligned(n, NODE_HEADER_SIZE) ∧ n ≤ # buf3 → (∃ x0, lax0. x0 ⊑ x ∧ lax0 ⊑ lax ∧ abs-nodes(subarray(buf3, 0, n), m, x0, lax0, true)) ⊦ NODE_HEADER_SIZE = 1

Rule argument

Additional information

Used simplifier rules: ⊦ m +1 = m + 1; (s)%f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic%trans: ⊦ n < n0 ∧ n0 < n1 → n < n1; (forward) from specification nat-basic%fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat%lf-02: ⊦ m < n ∧ m = n0 → n0 < n; (forward) from specification nat-basic%lf: ⊦ m < n ∧ n < n0 → m +1 < n0; (forward) from specification nat-basic% ⊦ NODE_HEADER_SIZE + n ≠ 0; (s)% ⊦ m < m + n ↔ n ≠ 0; (s)%c: ⊦ m + n = n + m; from specification nat-basic%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic% ⊦ NODE_HEADER_SIZE ≠ 0; (s)% ⊦ 1 < m ↔ ¬(m = 0 ∨ m = 1); (s)% ⊦ m + n < m + n0 ↔ n < n0; (s)