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: |
|---|---|---|
| chartostring | ⊦ char ' = char + "" | An Axiom |
| append-base | ⊦ "" + str = str | An Axiom |
| append-rec | ⊦ (char + str) + str0 = char + (str + str0) | An Axiom |
| app | ⊦ str + str0 = str + str1 ↔ str0 = str1 | A User Theorem |
| assoc | ⊦ (str1 + str2) + str3 = str1 + str2 + str3 | A User Theorem |
| chartostring-01 | ⊦ char + str = char ' + str | A User Theorem |
| empty | ⊦ str1 + str2 = "" ↔ str1 = "" ∧ str2 = "" | A User Theorem |
| empty-01 | ⊦ str1 + "" = str1 | A User Theorem |
| first | str ≠ "" ⊦ ((* str) + str0).char1 = str.char1 | A User Theorem |
| first-01 | ⊦ str ≠ "" → (str + str0).char1 = str.char1 | A User Theorem |
| first-one | ⊦ char '.char1 = char | A User Theorem |
| injectivity | ⊦ char ' + str = char0 ' + str0 ↔ char = char0 ∧ str = str0 | A User Theorem |
| one | ⊦ char1 ' + str1 = char2 ' + str2 ↔ char1 = char2 ∧ str1 = str2 | A User Theorem |
| one-01 | ⊦ char ' ≠ "" | A User Theorem |
| rec | ⊦ str1 ≠ "" → (char ' + str = str1 ↔ char = str1.char1 ∧ str = str1.rstring) | A User Theorem |
| rest | str ≠ "" ⊦ ((* str) + str0).rstring = str.rstring + str0 | A User Theorem |
| rest-01 | ⊦ str ≠ "" → (str + str0).rstring = str.rstring + str0 | A User Theorem |
| rest-one | ⊦ char '.rstring = "" | A User Theorem |