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: |
|---|---|---|
| At-other-strong | ⊦ D[n0, n1][n] = (n ≠ n0 ⊃ D[n];n1) | A User Theorem |
| MAIN-example | A = mkarray(6)[0, 22][1, 33][2, 100][3, 55][4, 44][5, 11], D = (∅)[100, 2][11, 5][22, 0][33, 1][44, 4][55, 3], P = pe(0, 2, 0) + pe(3, 5, 0) + [], X = 11 + 22 + 44 + [], F = (∅)[0, 0][1, 0][2, 0][3, 1][4, 1][5, 1] ⊦ ⟨MAIN(X; A, D, P, F)⟩ ( A = mkarray(6)[0, 22][1, 33][2, 100][3, 11][4, 44][5, 55] ∧ D = (∅)[100, 2][11, 3][22, 0][33, 1][44, 4][55, 5] ∧ P = pe(0, 0, 0) + pe(3, 4, 0) + pe(1, 2, 0) + pe(5, 5, 0) + [] ∧ F = (∅)[0, 0][1, 2][2, 2][3, 1][4, 1][5, 3]) | A User Theorem |
| NEWPARTS-example | A = mkarray(6)[0, 22][1, 33][2, 100][3, 44][4, 11][5, 55], D = (∅)[100, 2][11, 4][22, 0][33, 1][44, 3][55, 5], P = pe(0, 2, 1) + pe(3, 5, 2) + [], F = (∅)[0, 0][1, 0][2, 0][3, 1][4, 1][5, 1] ⊦ ⟨NEWPARTS(; P, F)⟩ (P = pe(0, 0, 0) + pe(3, 4, 0) + pe(1, 2, 0) + pe(5, 5, 0) + [] ∧ F = (∅)[0, 0][1, 2][2, 2][3, 1][4, 1][5, 3]) | A User Theorem |
| REFINE-example | A = mkarray(6)[0, 22][1, 33][2, 100][3, 55][4, 44][5, 11], D = (∅)[100, 2][11, 5][22, 0][33, 1][44, 4][55, 3], P = pe(0, 2, 0) + pe(3, 5, 0) + [], X = 11 + 22 + 44 + [], F = (∅)[0, 0][1, 0][2, 0][3, 1][4, 1][5, 1] ⊦ ⟨REFINE(X, F; A, D, P)⟩ ( A = mkarray(6)[0, 22][1, 33][2, 100][3, 11][4, 44][5, 55] ∧ D = (∅)[100, 2][11, 3][22, 0][33, 1][44, 4][55, 5] ∧ P = pe(0, 2, 1) + pe(3, 5, 2) + []) | A User Theorem |
| in-insert-strong | ⊦ m0 ∈ D[m, n] ↔ ¬ ¬(m0 = m ∨ m0 ∈ D) | A User Theorem |
| updF-get-strong | m0 ∈ F ⊦ F[m, n, i][m0] = (m ≤ m0 ∧ m0 ≤ n ⊃ i;F[m0]) | A User Theorem |