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: |
|---|---|---|
| lookup | ⊦ ((i ' × val) ' + fis)[fs '] = fis[fs '] | A User Theorem |
| lookup-01 | class1 ≠ class2 ⊦ ((mkfs(class1, ty, fieldvar) ' × val) ' + fis)[mkfs(class2, ty0, fieldvar0) '] = fis[mkfs(class2, ty0, fieldvar0) '] | A User Theorem |
| lookup-02 | ty ≠ ty0 ⊦ ((mkfs(class1, ty, fieldvar) ' × val) ' + fis)[mkfs(class2, ty0, fieldvar0) '] = fis[mkfs(class2, ty0, fieldvar0) '] | A User Theorem |
| lookup-03 | fieldvar ≠ fieldvar0 ⊦ ((mkfs(class1, ty, fieldvar) ' × val) ' + fis)[mkfs(class2, ty0, fieldvar0) '] = fis[mkfs(class2, ty0, fieldvar0) '] | A User Theorem |
| shift | sk0 ≠ sk ⊦ ((sk0 × val0) ' + fis)[sk, val] = (sk0 × val0) ' + fis[sk, val] | A User Theorem |