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: |
|---|---|---|
| inj | ⊦ pe(m, m0, m1) = pe(m2, m3, m4) ↔ m = m2 ∧ m0 = m3 ∧ m1 = m4 | An Axiom |
| case | ⊦ pe(p.first, p.last, p.count) = p | An Axiom |
| elim | ⊦ (m = p.first ∧ m0 = p.last) ∧ m1 = p.count ↔ p = pe(m, m0, m1) | An Axiom |
| gen | An Axiom | |
| sel-03 | ⊦ pe(m, m0, m1).first = m | An Axiom |
| sel-04 | ⊦ pe(m, m0, m1).last = m0 | An Axiom |
| sel-05 | ⊦ pe(m, m0, m1).count = m1 | An Axiom |
| updsel-01 | ⊦ (p.first:= m).first = m | An Axiom |
| updsel-02 | ⊦ (p.last:= m0).first = p.first | An Axiom |
| updsel-03 | ⊦ (p.count:= m1).first = p.first | An Axiom |
| updsel-04 | ⊦ (p.first:= m).last = p.last | An Axiom |
| updsel-05 | ⊦ (p.last:= m0).last = m0 | An Axiom |
| updsel-06 | ⊦ (p.count:= m1).last = p.last | An Axiom |
| updsel-07 | ⊦ (p.first:= m).count = p.count | An Axiom |
| updsel-08 | ⊦ (p.last:= m0).count = p.count | An Axiom |
| updsel-09 | ⊦ (p.count:= m1).count = m1 | An Axiom |
| upd-01 | ⊦ pe(m, m0, m1).first:= m2 = pe(m2, m0, m1) | An Axiom |
| upd-02 | ⊦ pe(m, m0, m1).last:= m3 = pe(m, m3, m1) | An Axiom |
| upd-03 | ⊦ pe(m, m0, m1).count:= m4 = pe(m, m0, m4) | An Axiom |