Proof step 107 from proof decode-node (previous step)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 108:

  # buf1 = align↑(node-size-headerless(nd), 2 * NODE_HEADER_SIZE), # buf = NODE_HEADER_SIZE, is-encoded(nodeheader(node-size-headerless(nd), false), buf), is-encoded(nd, subarray(buf1 + buf2, 0, node-size-headerless(nd))), range=(buf + buf1 + buf2, NODE_HEADER_SIZE + # buf1, validtrailer, 0, NODE_HEADER_SIZE), NODE_HEADER_SIZE ≤ # buf2, node-size-headerless(nd) ≤ # buf1 + # buf2 ⊦ ∃ buf0, buf3. buf + buf1 + subarray(buf2, 0, NODE_HEADER_SIZE) = buf0 + buf3 + validtrailer ∧ is-encoded(nodeheader(node-size-headerless(nd), false), buf0) ∧ is-encoded(nd, subarray(buf3, 0, node-size-headerless(nd))) ∧ # buf3 = # buf1

Rule argument

Additional information

Used simplifier rules: m ≤ # buf ⊦ subarray(buf0 + buf, 0, # buf0 + m) = buf0 + subarray(buf, 0, m); (s)% ⊦ m ≤ n → (n < m ↔ false); (s)% ⊦ m + n ≤ m + n0 ↔ n ≤ n0; (s)% ⊦ m ≤ m + n; (s)%append-a: ⊦ (buf + buf0) + buf1 = buf + buf0 + buf1; from specification array-splice[buffer]% ⊦ #(buf + buf0) = # buf + # buf0; (s)%c: ⊦ m + n = n + m; from specification nat-basic%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic% ⊦ ¬ m + n < m; (s)% ⊦ m < n → n ≠ 0; (s)%fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat%f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic% ⊦ m ≤ n ↔ ¬ n < m; (ss)