This is a listing of all goals defined over the current specification. Axioms are marked yellow, proved theorems green and unproved theorems blue. Click on individual names to get more information on the proof.
| Name: | Sequent: | Type: |
|---|---|---|
| gen | group-node freely generated by mkgnode; | An Axiom |
| elim | ⊦ ((nd = gnd.nd ∧ m = gnd.sqnum) ∧ (boolvar ↔ gnd.start)) ∧ (boolvar0 ↔ gnd.end) ↔ gnd = mkgnode(nd, m, boolvar, boolvar0) | An Axiom |
| case | ⊦ mkgnode(gnd.nd, gnd.sqnum, gnd.start, gnd.end) = gnd | An Axiom |
| inj | ⊦ mkgnode(nd, m, boolvar, boolvar0) = mkgnode(nd0, m0, boolvar1, boolvar2) ↔ nd = nd0 ∧ m = m0 ∧ (boolvar ↔ boolvar1) ∧ (boolvar0 ↔ boolvar2) | An Axiom |
| updsel | ⊦ (gnd.nd:= nd).nd = nd | An Axiom |
| upd | ⊦ mkgnode(nd, m, boolvar, boolvar0).nd:= nd0 = mkgnode(nd0, m, boolvar, boolvar0) | An Axiom |
| sel | ⊦ mkgnode(nd, m, boolvar, boolvar0).nd = nd | An Axiom |
| updsel-01 | ⊦ (gnd.sqnum:= m).nd = gnd.nd | An Axiom |
| updsel-03 | ⊦ (gnd.nd:= nd).sqnum = gnd.sqnum | An Axiom |
| updsel-04 | ⊦ (gnd.sqnum:= m).sqnum = m | An Axiom |
| updsel-09 | ⊦ (gnd.start:= boolvar).nd = gnd.nd | An Axiom |
| updsel-10 | ⊦ (gnd.end:= boolvar0).nd = gnd.nd | An Axiom |
| updsel-11 | ⊦ (gnd.start:= boolvar).sqnum = gnd.sqnum | An Axiom |
| updsel-12 | ⊦ (gnd.end:= boolvar0).sqnum = gnd.sqnum | An Axiom |
| updsel-13 | ⊦ (gnd.nd:= nd).start ↔ gnd.start | An Axiom |
| updsel-14 | ⊦ (gnd.sqnum:= m).start ↔ gnd.start | An Axiom |
| updsel-15 | ⊦ (gnd.start:= boolvar).start ↔ boolvar | An Axiom |
| updsel-16 | ⊦ (gnd.end:= boolvar0).start ↔ gnd.start | An Axiom |
| updsel-17 | ⊦ (gnd.nd:= nd).end ↔ gnd.end | An Axiom |
| updsel-18 | ⊦ (gnd.sqnum:= m).end ↔ gnd.end | An Axiom |
| updsel-19 | ⊦ (gnd.start:= boolvar).end ↔ gnd.end | An Axiom |
| updsel-20 | ⊦ (gnd.end:= boolvar0).end ↔ boolvar0 | An Axiom |
| upd-03 | ⊦ mkgnode(nd, m, boolvar, boolvar0).sqnum:= m0 = mkgnode(nd, m0, boolvar, boolvar0) | An Axiom |
| upd-04 | ⊦ mkgnode(nd, m, boolvar, boolvar0).start:= boolvar1 = mkgnode(nd, m, boolvar1, boolvar0) | An Axiom |
| upd-05 | ⊦ mkgnode(nd, m, boolvar, boolvar0).end:= boolvar2 = mkgnode(nd, m, boolvar, boolvar2) | An Axiom |
| sel-03 | ⊦ mkgnode(nd, m, boolvar, boolvar0).sqnum = m | An Axiom |
| sel-04 | ⊦ mkgnode(nd, m, boolvar, boolvar0).start ↔ boolvar | An Axiom |
| sel-05 | ⊦ mkgnode(nd, m, boolvar, boolvar0).end ↔ boolvar0 | An Axiom |