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: |
|---|---|---|
| bool-less | ⊦ bv < bv0 ↔ ¬ ¬ (¬ bv ∧ bv0) | An Axiom |
| issorted-le-all-def | ⊦ issorted(bits) ↔ (∀ m, n. m ≤ n ∧ n < # bits → ¬ bits[n] < bits[m]) | An Axiom |
| getbooleanarray | ⊦ getbooleanarray(r, i, j, st) = booleanvalues(getarray(r, i, j, st)) | An Axiom |
| getbooleanarray-def | ⊦ getbooleanarray(r, st) = getbooleanarray(r, 0, st[r -- _length] .intval, st) | An Axiom |
| booleanvalues-rec | ⊦ booleanvalues(val ' + vals) = val .boolval + booleanvalues(vals) | An Axiom |
| booleanvalues-empty | ⊦ booleanvalues([]) = [] | An Axiom |
| booleanarray-get | ⊦ okarray(r, boolean_type, st) ∧ 0 ≤ i ∧ i < st[r -- _length] .intval → (getbooleanarray(r, st)[i→n(i)] ↔ st[r -- i '] .boolval) | A User Theorem |
| booleanarray-len | ⊦ okarray(r, boolean_type, st) → # getbooleanarray(r, st[r -- i ', val]) = # getbooleanarray(r, st) | A User Theorem |
| booleanarray-put | ⊦ is_boolvalue(val) ∧ 0 ≤ i ∧ i < st[r -- _length] .intval → (getbooleanarray(r, st)[i→n(i), val .boolval]) = getbooleanarray(r, st[r -- i ', val]) | A User Theorem |
| boolvals-get | ⊦ n < # vals → (booleanvalues(vals)[n] ↔ vals[n] .boolval) | A User Theorem |
| boolvals-length | ⊦ # booleanvalues(vals) = # vals | A User Theorem |
| boolvals-put | ⊦ n < # vals → (booleanvalues(vals)[n, bv]) = booleanvalues(vals[n, boolval(bv)]) | A User Theorem |
| getbooleanarray-length | ⊦ okarray(r, boolean_type, st) → st[r -- _length] .intval = n→i(# getbooleanarray(r, st)) | A User Theorem |
| issorted-empty | ⊦ ¬ issorted([]) ↔ false | A User Theorem |
| okarray-mod | ⊦ okarray(r, boolean_type, st) ∧ is_boolvalue(val) → (¬ okarray(r, boolean_type, st[r -- i ', val]) ↔ false) | A User Theorem |