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: |
|---|---|---|
| FINDDUP | An Axiom | |
| FINDDUPSND | An Axiom | |
| challenge3 | ∃ m, n, m0, n0. ar[m] = ar[n] ∧ m ≠ n ∧ m < # ar ∧ n < # ar ∧ ar[m0] = ar[n0] ∧ m0 ≠ n0 ∧ m0 < # ar ∧ n0 < # ar ∧ ar[m] ≠ ar[m0] ⊦ ⦉FINDDUP#(ar; m0, n0)⦊ ⦉FINDDUPSND#(ar, ar[m0]; m1, n1)⦊ (ar[m0] = ar[n0] ∧ m0 ≠ n0 ∧ m0 < # ar ∧ n0 < # ar ∧ ar[m1] = ar[n1] ∧ m1 ≠ n1 ∧ m1 < # ar ∧ n1 < # ar ∧ ar[m0] ≠ ar[m1]) | A User Theorem |
| challenge3a | ∃ m, n. ar[m] = ar[n] ∧ m ≠ n ∧ m < # ar ∧ n < # ar ⊦ ⦉FINDDUP#(ar; m0, n0)⦊ (ar[m0] = ar[n0] ∧ m0 ≠ n0 ∧ m0 < # ar ∧ n0 < # ar) | A User Theorem |
| challenge3b | ∃ m, n. ar[m] = ar[n] ∧ m ≠ n ∧ m < # ar ∧ n < # ar ∧ ar[m] ≠ a ⊦ ⦉FINDDUPSND#(ar, a; m0, n0)⦊ (ar[m0] = ar[n0] ∧ ar[m0] ≠ a ∧ m0 ≠ n0 ∧ m0 < # ar ∧ n0 < # ar) | A User Theorem |