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-01 | ⊦ O ≠ C _ t | An Axiom |
| disj-02 | ⊦ O ≠ t _ C | An Axiom |
| disj-03 | ⊦ C _ t ≠ t0 _ C0 | An Axiom |
| sel-01 | ⊦ .c(t _ C) = C | An Axiom |
| sel-02 | ⊦ (t _ C) .t = t | An Axiom |
| sel-03 | ⊦ (C _ t) .t = t | An Axiom |
| sel-04 | ⊦ .c(C _ t) = C | An Axiom |
| inj-01 | ⊦ t _ C = t0 _ C0 ↔ t = t0 ∧ C = C0 | An Axiom |
| inj-02 | ⊦ C _ t = C0 _ t0 ↔ C = C0 ∧ t = t0 | An Axiom |
| case | ⊦ C = O ∨ C = .c(C) _ C .t ∨ C = C .t _ .c(C) | An Axiom |
| size-01 | ⊦ #(t _ C) = #(C) +1 | An Axiom |
| size-02 | ⊦ #(C _ t) = #(C) +1 | An Axiom |
| size-03 | ⊦ #(O) = 0 | An Axiom |
| gen | An Axiom | |
| elim-01 | ⊦ Cf(C) → (C0 = .c(C) ∧ t = C .t ↔ C = C0 _ t) | An Axiom |
| elim-02 | ⊦ Ca(C) → (t = C .t ∧ C0 = .c(C) ↔ C = t _ C0) | An Axiom |
| ex-01 | ⊦ Cf(C) ↔ (∃ C0, t. C = C0 _ t) | An Axiom |
| ex-02 | ⊦ Ca(C) ↔ (∃ t, C0. C = t _ C0) | An Axiom |
| test-01 | ⊦ ¬ Cf(O) | An Axiom |
| test-02 | ⊦ Cf(C _ t) | An Axiom |
| test-03 | ⊦ ¬ Cf(t _ C) | An Axiom |
| test-04 | ⊦ ¬ Ca(O) | An Axiom |
| test-05 | ⊦ ¬ Ca(C _ t) | An Axiom |
| test-06 | ⊦ Ca(t _ C) | An Axiom |