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: |
|---|---|---|
| extensionality | ⊦ s = s0 ↔ (∀ nam, ag. s(nam, ag) = s0(nam, ag)) | An Axiom |
| Term-stepjsiz | ⊦ 〈STEP#(s, a; s1)〉 true | An Axiom |
| RMA-3 | ⊦ ¬ 〈STEP#(s, a; s2)〉 s2(nam, ag) = s(nam, ag) → alter(dom(a), nam, ag) | An Axiom |
| RMA-2 | ⊦ eqd(s, dom(a), s0) ∧ s(nam, ag) = s0(nam, ag) ∧ alter(dom(a), nam, ag) → 〈STEP#(s, a; s2)〉 〈STEP#(s0, a; s3)〉 s2(nam, ag) = s3(nam, ag) | An Axiom |
| STEP-decl | An Axiom |