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: |
|---|---|---|
| gen-03 | array generated by mkarray, [ ]; | An Axiom |
| Put-other | ⊦ m ≠ n → ar[n, a][m] = ar[m] | An Axiom |
| Put-same | ⊦ m < # ar → ar[m, a][m] = a | An Axiom |
| Size-put | ⊦ # ar[n, a] = # ar | An Axiom |
| Size-mkarray | ⊦ # mkarray(n) = n | An Axiom |
| Extension | ⊦ ar1 = ar2 ↔ # ar1 = # ar2 ∧ (∀ n. n < # ar1 → ar1[n] = ar2[n]) | An Axiom |
| cgetput | m < # ar ⊦ ar[m, a][m] = a | A User Theorem |
| cngetput | m ≠ n ⊦ ar[m, a][n] = ar[n] | A User Theorem |
| cngetput-num | m ≠ n ⊦ ar[(* m), a][(* n)] = ar[n] | A User Theorem |
| cputput | m < # ar ⊦ ar[m, a][m, b] = ar[m, b] | A User Theorem |
| cputput-reverse | m ≠ n ⊦ ar[m, a][n, b] = ar[n, b][m, a] | A User Theorem |
| ext-rec | ⊦ ar1 = ar0[n, a] ↔ # ar0 = # ar1 ∧ (∀ m. m < # ar0 → ar1[m] = (n = m ⊃ a;ar0[m])) | A User Theorem |
| ngp-06 | ⊦ m < n → ar[m, a][n] = ar[n] | A User Theorem |
| ngp-07 | ⊦ n < m → ar[m, a][n] = ar[n] | A User Theorem |
| ngp-08 | ⊦ m + m0 < n → ar[m, a][n] = ar[n] | A User Theorem |
| ngp-09 | ⊦ n + n0 < m → ar[m, a][n] = ar[n] | A User Theorem |
| ngp-10 | ⊦ ar[m + 1, a][m] = ar[m] | A User Theorem |
| put-both-eq | ⊦ ar[n, a] = ar[n, b] ↔ ¬ ¬(n < # ar → a = b) | A User Theorem |
| put-same-content | ⊦ ar[n] = a → ar[n, a] = ar | A User Theorem |
| putgetinv | m < # ar ⊦ ar[m, ar[m]] = ar | A User Theorem |