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: |
|---|---|---|
| NEWPARTS | An Axiom | |
| REFINEONE | An Axiom | |
| updF-get | ⊦ m0 ∈ F → F[m, n, i][m0] = (m ≤ m0 ∧ m0 ≤ n ⊃ i;F[m0]) | An Axiom |
| updF-member | ⊦ m0 ∈ F[m, n, i] ↔ m0 ∈ F | An Axiom |
| REFINE | An Axiom | |
| MAIN | An Axiom | |
| inpartelem-def | ⊦ n ∈ p ↔ p.first ≤ n ∧ n ≤ p.last | An Axiom |
| partititions-def | ⊦ partitions(P, n0) ↔ (∀ n. n < n0 → (∃ m. m < # P ∧ n ∈ P[m] ∧ (∀ m0. m0 < # P ∧ m0 ≠ m → ¬ n ∈ P[m0]))) | An Axiom |
| okp-def | ⊦ okp(p, n) ↔ p.first ≤ p.last ∧ p.first + p.count ≤ p.last + 1 ∧ p.last < n | An Axiom |
| splitone-def | ⊦ splitone(p, A, X) ↔ (∀ n. n ∈ p → (n < p.first + p.count ↔ A[n] ∈ X)) | An Axiom |
| split-def | ⊦ split(P, A, X) ↔ (∀ p. p ∈ P → okp(p, # A) ∧ splitone(p, A, X)) | An Axiom |
| ADid-def | ⊦ ADid(A, D) ↔ (∀ m. m ∈ D → D[m] < # A ∧ A[D[m]] = m) | An Axiom |
| DAid-def | ⊦ DAid(A, D) ↔ (∀ n. n < # A → A[n] ∈ D ∧ D[A[n]] = n) | An Axiom |
| XornoX-def | ⊦ XornoX(p, X, A) ↔ (∀ n. n ∈ p → A[n] ∈ X) ∨ (∀ n. n ∈ p → ¬ A[n] ∈ X) | An Axiom |
| startorfin-def | ⊦ startorfin(p, P0) ↔ (∃ p0. p0 ∈ P0 ∧ (p0.first = p.first ∧ p.last ≤ p0.last ∨ p0.first ≤ p.first ∧ p0.last = p.last)) | An Axiom |
| divides-def | ⊦ divides(P, P0, X, A) ↔ (∀ p. p ∈ P → XornoX(p, X, A) ∧ startorfin(p, P0)) | An Axiom |
| resetcnt-rec | ⊦ resetcnt(p ' + P) = p.count:= 0 + resetcnt(P) | An Axiom |
| resetcnt-empty | ⊦ resetcnt([]) = [] | An Axiom |
| Fok-def | ⊦ Fok(F, P, n0) ↔ (∀ n. n < n0 → n ∈ F ∧ F[n] < # P ∧ n ∈ P[F[n]]) | An Axiom |
| nodups-def | ⊦ nodups(A) ↔ (∀ m, m0. m ≠ m0 ∧ m < # A ∧ m0 < # A → A[m] ≠ A[m0]) | An Axiom |
| partelem-sem-def | ⊦ n ∈ ⟦p⟧ (A) ↔ (∃ m. m ∈ p ∧ A[m] = n) | An Axiom |
| samepartitions-def | ⊦ samepartitions(P, A, P0, A0) ↔ # P = # P0 ∧ (∀ n. n < # P → ⟦P[n]⟧ (A) = ⟦P0[n]⟧ (A0)) | An Axiom |
| partitionRefinement-def | ⊦ partitionRefinement(P, A, P0, A0, X) ↔ (∀ p. p ∈ P → (∃ p0. p0 ∈ P0 ∧ (⟦p⟧ (A) = ⟦p0⟧ (A0) ∩ list2set(X) ∨ ⟦p⟧ (A) = ⟦p0⟧ (A0) \ list2set(X)))) | An Axiom |
| list2set-def | ⊦ n ∈ list2set(X) ↔ n ∈ X | An Axiom |
| Fok-lem | ⊦ Fok(F, resetcnt(P), n) ↔ Fok(F, P, n) | A User Theorem |
| Fok-mod-cnt | ⊦ Fok(F, P, n0) ∧ n < # P ∧ P[n] = pe(m, m0, m1) → (¬ Fok(F, P[n, pe(m, m0, m2)], n0) ↔ false) | A User Theorem |
| MAIN-theorem | A = A0, P = P0, ∀ p. p ∈ P → p.count = 0 ∧ okp(p, # A), DAid(A, D), ADid(A, D), nodups(A), partitions(P, # A), Fok(F, P, # A) ⊦ ⟨MAIN(X; A, D, P, F)⟩ ( perm(A0, A) ∧ partitions(P, # A) ∧ divides(P, P0, X, A) ∧ DAid(A, D) ∧ ADid(A, D) ∧ Fok(F, P, # A) ∧ partitionRefinement(P, A, P0, A0, X)) | A User Theorem |
| NEWPARTS-theorem | DAid(A, D), ADid(A, D), nodups(A), split(P, A, X), partitions(P, # A), P = P0, Fok(F, P, # A), samepartitions(P, A, P4, A4) ⊦ ⟨NEWPARTS(; P, F)⟩ (partitions(P, # A) ∧ divides(P, P0, X, A) ∧ Fok(F, P, # A) ∧ partitionRefinement(P, A, P4, A4, X)) | A User Theorem |
| REFINE-theorem | ∀ p. p ∈ P → p.count = 0 ∧ okp(p, # A), DAid(A, D), ADid(A, D), nodups(A), A0 = A, partitions(P, # A), P = P0, Fok(F, P, # A) ⊦ ⟨REFINE(X, F; A, D, P)⟩ ( perm(A0, A) ∧ DAid(A, D) ∧ ADid(A, D) ∧ split(P, A, X) ∧ partitions(P, # A) ∧ resetcnt(P) = P0 ∧ nodups(A) ∧ Fok(F, P, # A) ∧ samepartitions(P, A, P0, A0)) | A User Theorem |
| REFINEONE-theorem | DAid(A, D), ADid(A, D), nodups(A), A0 = A, split(P, A, X), partitions(P, # A), P = P0, Fok(F, P, # A), samepartitions(P, A, P4, A4) ⊦ ⟨REFINEONE(x, F; A, D, P)⟩ ( perm(A0, A) ∧ DAid(A, D) ∧ ADid(A, D) ∧ split(P, A, X + x) ∧ partitions(P, # A) ∧ resetcnt(P) = resetcnt(P0) ∧ nodups(A) ∧ Fok(F, P, # A) ∧ samepartitions(P, A, P4, A4)) | A User Theorem |
| divides-XornoX-head | ⊦ divides(p ' + P, P1, X, A1) → (¬ XornoX(p, X, A1) ↔ false) | A User Theorem |
| divides-reset | ⊦ divides(P2, P1, X, A1) → (¬ divides(P2, resetcnt(P1), X, A1) ↔ false) | A User Theorem |
| elem-below-occurs | ⊦ m < n ∧ n ≤ # A → #oc(A[m], A, n) ≠ 0 | A User Theorem |
| elem-does-occur | ⊦ m < # A → #oc(A[m], A, # A) ≠ 0 | A User Theorem |
| empty-divides | ⊦ divides([], P1, X, A1) | A User Theorem |
| in-mod-count | ⊦ n ∈ pe(m, m0, m1) → (¬ n ∈ pe(m, m0, m2) ↔ false) | A User Theorem |
| member-reset | ⊦ pe(m, m0, m1) ∈ P → (¬ pe(m, m0, 0) ∈ resetcnt(P) ↔ false) | A User Theorem |
| no-oc | ⊦ #oc(n, A, m0) = 0 ↔ (∀ m. m < m0 → A[m] ≠ n) | A User Theorem |
| nodups-numoc | ⊦ nodups(A) ↔ (∀ n. #oc(n, A, # A) ≤ 1) | A User Theorem |
| nodups-oc | ⊦ m < # A ∧ nodups(A) → (∀ n. (n < m → #oc(A[n], A, m) = 1) ∧ (m ≤ n ∧ n < # A → #oc(A[n], A, m) = 0)) | A User Theorem |
| nodups-oc-2 | ⊦ m < # A ∧ nodups(A) → (∀ n. n < m → #oc(A[n], A, m) = 1) | A User Theorem |
| nodups-perm | ⊦ nodups(A0) ∧ perm(A0, A1) → (¬ nodups(A1) ↔ false) | A User Theorem |
| one-oc | ⊦ #oc(n, A, m0) = 1 ↔ (∃ m. m < m0 ∧ A[m] = n ∧ (∀ m1. m1 ≠ m ∧ m1 < m0 → A[m1] ≠ n)) | A User Theorem |
| partitions-mod-count | ⊦ partitions(P, n0) ∧ n < # P ∧ P[n] = pe(m, m0, m1) → (¬ partitions(P[n, pe(m, m0, m2)], n0) ↔ false) | A User Theorem |
| resetcnt-idem | ⊦ resetcnt(resetcnt(P1)) = resetcnt(P1) | A User Theorem |
| resetcnt-length | ⊦ # resetcnt(P0) = # P0 | A User Theorem |
| resetcnt-mod-cnt | ⊦ n < # P ∧ P[n] = pe(m, m0, m1) → resetcnt(P[n, pe(m, m0, m2)]) = resetcnt(P) | A User Theorem |
| resetcount-elem | ⊦ resetcnt(P)[n] = pe(m, m0, m1) → (∃ m2. P[n] = pe(m, m0, m2)) | A User Theorem |
| samepartitions-same | ⊦ samepartitions(P1, A1, P1, A1) | A User Theorem |
| split-init-2 | ⊦ partitions(P, # A) ∧ split(P, A, X) ∧ (∀ p. p ∈ P → p.count = 0) → split(P, A, []) | A User Theorem |
| startorfin-reset | ⊦ startorfin(p1, P1) → (¬ startorfin(p1, resetcnt(P1)) ↔ false) | A User Theorem |