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: |
|---|---|---|
| inmklist | ⊦ ¬ true ∈ mklist(false, n) | A User Theorem |
| inmklist-01 | ⊦ ¬ false ∈ mklist(true, n) | A User Theorem |
| last-first | ¬ false ∈ bits ⊦ bits + true ' = true ' + bits | A User Theorem |
| last-first-01 | ¬ true ∈ bits ⊦ bits + false ' = false ' + bits | A User Theorem |
| leone | ⊦ # bits ≤ 1 ∧ bits ≠ true ' ∧ bits ≠ false ' → bits = [] | A User Theorem |
| leone-false | ⊦ bits ≠ true ' → (# bits ≤ 1 ↔ bits = [] ∨ bits = false ') | A User Theorem |
| leone-true | ⊦ bits ≠ false ' → (# bits ≤ 1 ↔ bits = [] ∨ bits = true ') | A User Theorem |
| mklist | ⊦ ¬ true ∈ bits → mklist(false, # bits) = bits | A User Theorem |
| mklist-01 | ⊦ ¬ false ∈ bits → mklist(true, # bits) = bits | A User Theorem |
| mklist-02 | ⊦ n ≠ 0 → mklist(false, n) + bits ≠ true ' + bits0 | A User Theorem |
| mklist-03 | ⊦ n ≠ 0 → mklist(false, n) + bits ≠ true ' | A User Theorem |
| mklist-intro | ⊦ ¬ boolvar ∈ bits ↔ mklist(¬ boolvar, # bits) = bits | A User Theorem |
| mklist-num | n ≠ 0 ⊦ mklist(false, (* n)) = false ' + mklist(false, n -1) | A User Theorem |
| mklist-num-01 | n ≠ 0 ⊦ mklist(true, (* n)) = true ' + mklist(true, n -1) | A User Theorem |
| notfalse | ⊦ ¬ false ∈ bits → (bits + true ' = true ' + bits ↔ true) | A User Theorem |
| notfalse-01 | ⊦ ¬ false ∈ bits → (bits + true ' + true ' = true ' + true ' + bits ↔ true) | A User Theorem |
| nottrue | ⊦ ¬ true ∈ bits → (bits + false ' = false ' + bits ↔ true) | A User Theorem |
| nottrue-01 | ⊦ ¬ true ∈ bits → (bits + false ' + false ' = false ' + false ' + bits ↔ true) | A User Theorem |
| nottrue-02 | ⊦ ¬ true ∈ bits ∧ ¬ true ∈ bits0 → (bits + false ' + false ' + bits0 + false ' = false ' + false ' + false ' + bits + bits0 ↔ true) | A User Theorem |
| one-01 | ⊦ # bits = 1 ∧ bits ≠ true ' → bits = false ' | A User Theorem |
| one-02 | ⊦ # bits = 1 ∧ bits ≠ false ' → bits = true ' | A User Theorem |
| somein | ⊦ ¬ true ∈ bits ∧ bits ≠ [] → (¬ false ∈ bits ↔ false) | A User Theorem |