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 | ⊦ ⌜x⌝ ≠ ⌜nf⌝ | An Axiom |
| sel-01 | ⊦ ⌜nf⌝ .f = nf | An Axiom |
| sel-02 | ⊦ ⌜x⌝ .l = x | An Axiom |
| test-01 | ⊦ ¬ finp(⌜nf⌝ ) | An Axiom |
| test-02 | ⊦ finp(⌜x⌝ ) | An Axiom |
| inj-01 | ⊦ ⌜nf⌝ = ⌜nf0⌝ ↔ nf = nf0 | An Axiom |
| inj-02 | ⊦ ⌜x⌝ = ⌜x0⌝ ↔ x = x0 | An Axiom |
| case | ⊦ σ = ⌜σ.l⌝ ∨ σ = ⌜σ.f⌝ | An Axiom |
| ex | ⊦ finp(σ) ↔ (∃ x. σ = ⌜x⌝ ) | An Axiom |
| elim | ⊦ finp(σ) → (x = σ.l ↔ σ = ⌜x⌝ ) | An Axiom |
| gen | stream freely generated by ⌜ ⌝, ⌜ ⌝; | An Axiom |
| sel-embed-fin | ⊦ finp(σ) → ⌜σ.l⌝ = σ | A User Theorem |
| sel-embed-inf | ⊦ ¬ finp(σ) → ⌜σ.f⌝ = σ | A User Theorem |
| stream-fin-forward | ⊦ finp(σ) → (∃ x. ⌜x⌝ = σ) | A User Theorem |
| stream-inf-forward | ⊦ ¬ finp(σ) → (∃ nf. ⌜nf⌝ = σ) | A User Theorem |