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 | ⊦ Node(a, succ).edges = succ | An Axiom |
| sel-02 | ⊦ Node(a, succ).value = a | An Axiom |
| upd-01 | ⊦ Node(a, succ).value:= a0 = Node(a0, succ) | An Axiom |
| upd-02 | ⊦ Node(a, succ).edges:= succ0 = Node(a, succ0) | An Axiom |
| updsel-01 | ⊦ (nd.edges:= succ).value = nd.value | An Axiom |
| updsel-02 | ⊦ (nd.value:= a).edges = nd.edges | An Axiom |
| updsel-03 | ⊦ (nd.edges:= succ).edges = succ | An Axiom |
| updsel-04 | ⊦ (nd.value:= a).value = a | An Axiom |
| inj | ⊦ Node(a, succ) = Node(a0, succ0) ↔ a = a0 ∧ succ = succ0 | An Axiom |
| case | ⊦ Node(nd.value, nd.edges) = nd | An Axiom |
| elim | ⊦ a = nd.value ∧ succ = nd.edges ↔ nd = Node(a, succ) | An Axiom |
| gen | An Axiom |