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: |
|---|---|---|
| assoc-yes | ⊦ ((a × d)' + ax)[a] = d | An Axiom |
| assoc-no | ⊦ a ≠ b → ((b × d)' + ax)[a] = ax[a] | An Axiom |
| rassoc-yes | ⊦ ((a × d)' + ax)[d] = a | An Axiom |
| rassoc-no | ⊦ d ≠ d0 → ((a × d0)' + ax)[d] = ax[d] | An Axiom |
| inassoc | ⊦ a ∈ ax ↔ (∃ d. a × d ∈ ax) | An Axiom |
| put-empty | ⊦ ([])[a, d] = (a × d)' | An Axiom |
| put-yes | ⊦ ((a × d0)' + ax)[a, d] = (a × d)' + ax | An Axiom |
| put-no | ⊦ a ≠ b → ((b × d0)' + ax)[a, d] = (b × d0)' + ax[a, d] | An Axiom |
| unique-e | ⊦ unique_al([]) | An Axiom |
| unique-r | ⊦ unique_al((a × d) + ax) ↔ ¬ a ∈ ax ∧ unique_al(ax) | An Axiom |
| app | ⊦ unique_al(ax + p ' + ay) → unique_al(ax + ay) | A User Theorem |
| cons | ⊦ unique_al((a × d)' + ax) ↔ ¬ a ∈ ax ∧ unique_al(ax) | A User Theorem |
| empty | ⊦ ¬ a ∈ [] | A User Theorem |
| ex | ⊦ a ∈ ax ↔ (∃ d, ay, az. ax = ay + (a × d)' + az) | A User Theorem |
| firstoc | ⊦ a ∈ ax → (∃ ax0, d, ax1. ax = ax0 + (a × d)' + ax1 ∧ ¬ a ∈ ax0) | A User Theorem |
| in | ⊦ a × d ∈ ax → ¬ unique_al((a × d0)' + ax) | A User Theorem |
| in-01 | ⊦ a × d ∈ ax → a ∈ ax | A User Theorem |
| in-02 | ⊦ a ∈ ax + (a × d)' + ay | A User Theorem |
| in-03 | ⊦ a ∈ ax + ay → a ∈ ax + p ' + ay | A User Theorem |
| in-put | ⊦ a ∈ ax[b, d] ↔ a = b ∨ a ∈ ax | A User Theorem |
| inapp | ⊦ a ∈ ax + ay ↔ ¬ ¬(a ∈ ax ∨ a ∈ ay) | A User Theorem |
| incons | ⊦ a ∈ ax → a ∈ p ' + ax | A User Theorem |
| infirst | ⊦ a ∈ (a × d)' + ax | A User Theorem |
| inkeys-n | ⊦ a ≠ b → (a ∈ (b × d0)' + ax ↔ a ∈ ax) | A User Theorem |
| inkeys-nc | a ≠ b ⊦ a ∈ (b × d0)' + ax ↔ a ∈ ax | A User Theorem |
| inone | ⊦ a ∈ (b × d0)' ↔ a = b | A User Theorem |
| inrec | ⊦ a ∈ (b × d0)' + ax ↔ a = b ∨ a ∈ ax | A User Theorem |
| insfirst | ⊦ ¬ a ∈ ax → (ax + (a × d)' + ax0)[a, d0] = ax + (a × d0)' + ax0 | A User Theorem |
| insnotin | ⊦ ¬ a ∈ ax → ax[a, d] = ax + (a × d)' | A User Theorem |
| k-unique-r | ⊦ unique_al(ay) ↔ ay = [] ∨ ¬ ay.first.1 ∈ ay.rest ∧ unique_al(ay.rest) | A User Theorem |
| lenequal | unique_al(ax), unique_al(ay), # ax = # ay, ∀ a. a ∈ ax → a ∈ ay, b ∈ ay ⊦ b ∈ ax | A User Theorem |
| lenle | unique_al(ax), ∀ a. a ∈ ax → a ∈ ay ⊦ # ax ≤ # ay | A User Theorem |
| not | ⊦ ¬ unique_al(ax) → ¬ unique_al(p ' + ax) | A User Theorem |
| nuni | ⊦ unique_al(ay + (a × d)' + az) → ¬ a ∈ ay | A User Theorem |
| nuni-01 | ⊦ unique_al(ay + (a × d)' + az) → ¬ a ∈ az | A User Theorem |
| one | ⊦ unique_al(p ') | A User Theorem |
| one-01 | ⊦ (a × d)'[a] = d | A User Theorem |
| put-one | ⊦ (a × d)'[a, d0] = (a × d0)' | A User Theorem |
| unique | ⊦ unique_al(ax + p ') → unique_al(ax) | A User Theorem |
| unique-01 | ⊦ unique_al(ax + (a × d)') → ¬ a ∈ ax | A User Theorem |
| unique-02 | ⊦ unique_al(ax) ∧ a × d ∈ ax ∧ a × d0 ∈ ax → d = d0 | A User Theorem |
| unique-03 | ⊦ a ∈ ax → ¬ unique_al(ax + (a × d)' + ay) | A User Theorem |
| unique-04 | ⊦ a ∈ ay → ¬ unique_al(ax + (a × d)' + ay) | A User Theorem |
| uniquelen | ∀ a. a ∈ ax ↔ a ∈ ay, unique_al(ax), unique_al(ay) ⊦ # ax = # ay | A User Theorem |