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: |
|---|---|---|
| perm-def | ⊦ perm(ar, ar0) ↔ # ar = # ar0 ∧ (∀ a. #oc(a, ar, # ar) = #oc(a, ar0, # ar0)) | An Axiom |
| numoc-base | ⊦ #oc(a, ar, 0) = 0 | An Axiom |
| numoc-rec | ⊦ #oc(a, ar, n + 1) = #oc(a, ar, n) + (ar[n] = a ⊃ 1;0) | An Axiom |
| nonzero-numoc | ⊦ n < m ∧ m ≤ # ar → (#oc(ar[n], ar, m) = 0 ↔ false) | A User Theorem |
| numoc-swap | ⊦ m < # ar ∧ n < # ar → #oc(a, ar[n, ar[m]][m, ar[n]], # ar) = #oc(a, ar, # ar) | A User Theorem |
| numoc-swap-gen | ⊦ m < # ar ∧ n < # ar ∧ n0 ≤ # ar → #oc(a, ar[n, ar[m]][m, ar[n]], n0) = (ar[m] = ar[n] ⊃ #oc(a, ar, n0) ;(m < n0 ⊃ (n < n0 ⊃ #oc(a, ar, n0);(a = ar[m] ⊃ #oc(a, ar, n0) - 1;(a = ar[n] ⊃ #oc(a, ar, n0) + 1;#oc(a, ar, n0)))) ;(n < n0 ⊃ (a = ar[n] ⊃ #oc(a, ar, n0) - 1;(a = ar[m] ⊃ #oc(a, ar, n0) + 1;#oc(a, ar, n0)));#oc(a, ar, n0)) ) ) | A User Theorem |
| perm-refl | ⊦ perm(ar, ar) | A User Theorem |
| perm-swap | ⊦ perm(ar, ar0) ∧ m < # ar ∧ n < # ar ∧ m ≠ n → (¬ perm(ar, ar0[n, ar0[m]][m, ar0[n]]) ↔ false) | A User Theorem |
| perm-trans | ⊦ perm(ar, ar0) ∧ perm(ar1, ar) → perm(ar1, ar0) | A User Theorem |