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: |
|---|---|---|
| sel-01 | ⊦ mkfs(class, ty, fieldvar) .class = class | An Axiom |
| sel-02 | ⊦ mkfs(class, ty, fieldvar) .field = fieldvar | An Axiom |
| sel-03 | ⊦ mkfs(class, ty, fieldvar) .type = ty | An Axiom |
| inj | ⊦ mkfs(class, ty, fieldvar) = mkfs(class0, ty0, fieldvar0) ↔ class = class0 ∧ ty = ty0 ∧ fieldvar = fieldvar0 | An Axiom |
| case | ⊦ mkfs(fs .class, fs .type, fs .field) = fs | An Axiom |
| elim | ⊦ class = fs .class ∧ ty = fs .type ∧ fieldvar = fs .field ↔ fs = mkfs(class, ty, fieldvar) | An Axiom |
| gen | An Axiom | |
| inj-01 | ⊦ mkfs(class1, ty, fieldvar) = mkfs(class2, ty0, fieldvar0) ↔ ¬ ¬ (class1 = class2 ∧ ty = ty0 ∧ fieldvar = fieldvar0) | A User Theorem |