This is a listing of all goals defined over the current specification. Axioms are yellow, proof obligations purple and theorems green. Click on individual names to get more information on the proof.
| Name: | Sequent: | Type: |
|---|---|---|
| checksum-prefix | ⊦ n ≤ # buf0 ∧ n ≤ # buf1 ∧ subarray(buf0, 0, n) = subarray(buf1, 0, n) → checksum(buf0, n) = checksum(buf1, n) | An Axiom |
| checksum-append-left | ⊦ n ≤ # buf0 → checksum(buf0 + buf1, n) = checksum(buf0, n) | A User Theorem |
| checksum-subarray-exact | ⊦ n ≤ # buf → checksum(subarray(buf, 0, n), n) = checksum(buf, n) | A User Theorem |