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: |
|---|---|---|
| build-rec | An Axiom | |
| build | An Axiom | |
| completeness | ⊦ 〈build#(x; to)〉 (to = fail → ¬ (∃ t. x = depths(t, 0))) | A User Theorem |
| completeness-rec | x ≠ [], x = x0, i ≤ j, max(x) ≤ j ⊦ 〈build_rec#(i; x, to)〉 (to = fail → ¬ (∃ t, x1. x0 = depths(t, i) + x1)) | A User Theorem |
| harness-1 | ⊦ 〈build#(1 + 3 + 3 + 2 '; to)〉 to = some(Node(Leaf, Node(Node(Leaf, Leaf), Leaf))) | A User Theorem |
| harness-2 | ⊦ 〈build#(1 + 3 + 2 + 2 '; to)〉 to = fail | A User Theorem |
| soundness | ⊦ 〈build#(x; to)〉 (to ≠ fail → x = depths(to .t, 0)) | A User Theorem |
| soundness-rec | x ≠ [], x = x0, i ≤ j, max(x) ≤ j ⊦ 〈build_rec#(i; x, to)〉 (to ≠ fail → x0 = depths(to .t, i) + x) | A User Theorem |
| termination | ⊦ 〈build#(x; to)〉 true | A User Theorem |