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: |
|---|---|---|
| disj | ⊦ fs ' ≠ i ' | An Axiom |
| case | ⊦ sk = sk .fs ' ∨ sk = sk .index ' | An Axiom |
| gen | An Axiom | |
| elim-03 | ⊦ is_fskey(sk) → (fs = sk .fs ↔ sk = fs ') | An Axiom |
| elim-04 | ⊦ is_indexkey(sk) → (i = sk .index ↔ sk = i ') | An Axiom |
| ex-03 | ⊦ is_fskey(sk) ↔ (∃ fs. sk = fs ') | An Axiom |
| ex-04 | ⊦ is_indexkey(sk) ↔ (∃ i. sk = i ') | An Axiom |
| inj-03 | ⊦ fs ' = fs0 ' ↔ fs = fs0 | An Axiom |
| inj-04 | ⊦ i ' = i0 ' ↔ i = i0 | An Axiom |
| test-05 | ⊦ is_fskey(fs ') | An Axiom |
| test-06 | ⊦ ¬ is_fskey(i ') | An Axiom |
| test-07 | ⊦ ¬ is_indexkey(fs ') | An Axiom |
| test-08 | ⊦ is_indexkey(i ') | An Axiom |
| sel-05 | ⊦ fs ' .fs = fs | An Axiom |
| sel-06 | ⊦ i ' .index = i | An Axiom |
| test | ⊦ ¬ is_indexkey(sk) ↔ is_fskey(sk) | A User Theorem |
| test-01 | ⊦ ¬ is_fskey(sk) ↔ is_indexkey(sk) | A User Theorem |
| test-02 | ⊦ is_indexkey(sk) → ¬ is_fskey(sk) | A User Theorem |