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 | ⊦ "" ≠ char + str | An Axiom |
| sel-01 | ⊦ (char + str).char1 = char | An Axiom |
| sel-02 | ⊦ (char + str).rstring = str | An Axiom |
| inj | ⊦ char + str = char0 + str0 ↔ char = char0 ∧ str = str0 | An Axiom |
| case | ⊦ str = "" ∨ str = str.char1 + str.rstring | An Axiom |
| elim | ⊦ str ≠ "" → (char = str.char1 ∧ str0 = str.rstring ↔ str = char + str0) | An Axiom |
| gen | string freely generated by "", +; | An Axiom |
| empty | ⊦ char + str ≠ "" | A User Theorem |
| inj-01 | ⊦ char + str1 = char + str2 ↔ str1 = str2 | A User Theorem |
| inj-02 | ⊦ char1 + str = char2 + str ↔ char1 = char2 | A User Theorem |
| inj-03 | ⊦ str ≠ "" ∧ str0 ≠ "" → (str = str0 ↔ str.char1 = str0.char1 ∧ str.rstring = str0.rstring) | A User Theorem |