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 |
| at-put | ⊦ a ≠ b → ax[b, d][a] = ax[a] | A User Theorem |
| at-put-01 | ⊦ ax[a, d][a] = d | 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 |
| firstoccurrence-key | ⊦ 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-04 | ⊦ a ∈ ax + (a × d)' | A User Theorem |
| in-append | ⊦ a ∈ ax + ay ↔ a ∈ ax ∨ a ∈ ay | A User Theorem |
| in-assoclist | ⊦ a ∈ ax ∧ ax[a] = d → (¬ a × d ∈ ax ↔ false) | A User Theorem |
| in-assoclist-01 | ⊦ a ∈ ax → (¬ a × ax[a] ∈ ax ↔ false) | 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 |
| lastoccurrence-key | ⊦ a ∈ ax ↔ (∃ ax0, d, ax1. ax = ax0 + ((a × d) + ax1) ∧ ¬ a ∈ ax1) | 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 |
| lookup | ⊦ ¬ a ∈ ax → (ax + (a × d)' + ax0)[a] = d | A User Theorem |
| lookup-01 | ⊦ ¬ a ∈ ax → (ax + (a × d)')[a] = d | A User Theorem |
| lookup-02 | ⊦ a × d ∈ ax ∧ unique_al(ax) → ax[a] = d | A User Theorem |
| lookup-append | ⊦ a ∈ ax → (ax + ay)[a] = ax[a] | A User Theorem |
| lookup-append-01 | ⊦ ¬ a ∈ ax → (ax + ay)[a] = ay[a] | A User Theorem |
| lookup-one | ⊦ a ≠ b → (b × d)'[a] = ([])[a] | A User Theorem |
| not | ⊦ ¬ unique_al(ax) → ¬ unique_al(p ' + ax) | A User Theorem |
| not-in | ⊦ ¬ a ∈ ax → ¬ a × d ∈ 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 |
| perm-eq | ⊦ perm(ax, ay) ∧ unique_al(ax) ∧ a ∈ ax → ax[a] = ay[a] | A User Theorem |
| perm-unique | ⊦ perm(ax, ay) ∧ unique_al(ax) → unique_al(ay) | A User Theorem |
| put-in | ⊦ ¬ p ∈ ax → (p ∈ ax[a, d] ↔ p = a × d) | A User Theorem |
| put-one | ⊦ (a × d)'[a, d0] = (a × d0)' | A User Theorem |
| put-one-01 | a ≠ a0 ⊦ (a × d)'[a0, d0] = (a × d)' + (a0 × 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 |
| unique-add | ⊦ unique_al(ax + p ') ↔ ¬ p.1 ∈ ax ∧ unique_al(ax) | A User Theorem |
| unique-del | ⊦ unique_al(ax -1l (a × d)) ∧ ¬ a ∈ ax -1l (a × d) → unique_al(ax) | A User Theorem |
| unique-put | ⊦ unique_al(ax[a, d]) ↔ unique_al(ax) | A User Theorem |
| uniquelen | ∀ a. a ∈ ax ↔ a ∈ ay, unique_al(ax), unique_al(ay) ⊦ # ax = # ay | A User Theorem |