This is a listing of all goals defined over the current specification. Axioms are marked yellow, proved theorems green and unproved theorems blue. Click on individual names to get more information on the proof.
| Name: | Sequent: | Type: |
|---|---|---|
| psortcols | psortcols#(; MX){forall∥nf C with C < #c MX do psortcol#(C; MX)} | An Axiom |
| colsorted-permtoArr | #r mx = #r mx0, #c mx = #c mx0, c ≤ #c mx0 ⊦ colsorted(mx0, c, mx) → perm(mx0.toArr, mx.toArr) | A User Theorem |
| countevn-rec | m ≤ n, n ≤ # a ⊦ countevn(a, m, n + 1, p) = countevn(a, m, n, p) + (even(n) ∧ p(a[n]) ⊃ 1;0) | An Axiom |
| colsorted-colordered | #c mx = #c mx0, c < #c mx ⊦ colsorted(mx0, #c mx0, mx) → ordered≤(mx[c]c) | A User Theorem |
| divup-def | ⊦ m /↑ n = (∃ n0. m = n0 * n ⊃ m / n;m / n + 1) | An Axiom |
| countevn-zero-ind | ∀ r. m ≤ r ∧ r < n ∧ even(r) → ¬ p(a[r]), m ≤ n, n ≤ # a ⊦ countevn(a, m, n, p) = 0 | A User Theorem |
| clean0-plus-clean1-bounded | #c mx ≠ 0 ⊦ ¬ #r mx < #clean0rows(mx, i) + #clean1rows(mx, i) | A User Theorem |
| colno-updcol | #r mx = # a, c < #c mx ⊦ #c mx[c, a]c = #c mx | An Axiom |
| countodd-rec | m ≤ n, n ≤ # a ⊦ countodd(a, m, n + 1, p) = countodd(a, m, n, p) + (odd(n) ∧ p(a[n]) ⊃ 1;0) | An Axiom |
| dirytrows-leone | #c mx ≠ 0, #dirtyrows(mx, i) ≤ 1 ⊦ (∀ r. r < #r mx → count(mx[r]r, λ j. j < i) = 0 ∨ count(mx[r]r, λ j. ¬ j < i) = 0) ∨ (∃ r0. count(mx[r0]r, λ j. j < i) ≠ 0 ∧ count(mx[r0]r, λ j. ¬ j < i) ≠ 0 ∧ (∀ r. r ≠ r0 ∧ r < #r mx → count(mx[r]r, λ j. j < i) = 0 ∨ count(mx[r]r, λ j. ¬ j < i) = 0)) | A User Theorem |
| max0column-countcol | #r mx = #r mx0, #c mx = #c mx0, c < #c mx, c0 < #c mx, colsorted(mx0, #c mx, mx), ∀ c. c < #c mx → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i) ⊦ count(mx[c]c, λ j. j < i) = #clean0rows(mx0, i) + count(mx0[c]c, #clean0rows(mx0, i), #r mx, λ j. j < i) | A User Theorem |
| allperm-permtoArr | #r mx = #r mx0, #c mx = #c mx0, ∀ r. r < #r mx0 → perm(mx0[r]r, mx[r]r) ⊦ perm(mx0.toArr, mx.toArr) | A User Theorem |
| psortrows-correct | #c mx ≠ 0, #r mx ≠ 0, mx = mx0, rowsincreasing(mx, #r mx) ⊦ ⟪psortrows#(; mx)⟫ (#r mx0 = #r mx ∧ #c mx = #c mx0 ∧ perm(mx0.toArr, mx.toArr) ∧ ordered≤(mx.toArr)) | A User Theorem |
| allperm-permtoArr-ind | #r mx = #r mx0, #c mx = #c mx0, r ≤ #r mx0, ∀ r0. r0 < r → perm(mx0[r0]r, mx[r0]r) ⊦ perm(toArr(mx0, r), toArr(mx, r)) | A User Theorem |
| psortrowsnake-correct | MX[r]r = mx[r]r, r < #r MX, #r MX = #r mx, #c MX = #c mx, #c mx ≠ 0, #r mx ≠ 0 ⊦ ⟨: MX | (MX''[r]r = MX'[r]r) , (MX' = MX[r, MX'[r]r]r) , (#r MX = #r mx ∧ #c MX = #c mx) , psortrowsnake#(r, even(r); MX) ⟩ (perm(mx[r]r, MX[r]r) ∧ (even(r) ⊃ ordered≤(MX[r]r);ordered≥(MX[r]r))) | A User Theorem |
| countodd-append-ind | m ≤ n, n ≤ n0, n0 ≤ # a ⊦ countodd(a, m, n, p) + countodd(a, n, n0, p) = countodd(a, m, n0, p) | A User Theorem |
| rowsincreasing-allrowsorted-sorted | rowsincreasing(mx, #r mx), ∀ r. r < #r mx → ordered≤(mx[r]r) ⊦ ordered≤(mx.toArr) | A User Theorem |
| clean1rows-allge | ⊦ #r mx ≤ #clean1rows(mx, i) + r ∧ r < #r mx → count(mx[r]r, λ j. j < i) = 0 | An Axiom |
| srowsorted-dirtyboundunchanged | #c mx ≠ 0, #r mx = #r mx0, #c mx = #c mx0 ⊦ mx0.dirtyrows≤(bound) ∧ srowsorted(mx0, #r mx0, mx) → mx.dirtyrows≤(bound) | A User Theorem |
| dirtyrowsbound-def | ⊦ mx.dirtyrows≤(bound) ↔ (∀ i. #dirtyrows(mx, i) ≤ bound) | An Axiom |
| clean0rows-notallls | ⊦ #clean0rows(mx, i) < #r mx → count(mx[#clean0rows(mx, i)]r, λ j. ¬ j < i) ≠ 0 | An Axiom |
| log2up-def | ⊦ log2↑(n) = (∃ m. n = 2^ m ⊃ log2 n;log2(2 * n + 1)) | An Axiom |
| colsorted-def | ⊦ m ≤ #c mx → ( colsorted(mx0, m, mx) ↔ #r mx = #r mx0 ∧ #c mx = #c mx0 ∧ (∀ c. c < #c mx → (c < m ⊃ perm(mx0[c]c, mx[c]c) ∧ ordered≤(mx[c]c);mx0[c]c = mx[c]c))) | An Axiom |
| countodd-maxcol0-bounded | c0 < #c mx0 ⊦ countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) ≤ #dirtyrows(mx0, i) /↑ 2 | A User Theorem |
| rowsorted-smallercol-evnbounded | srowsorted(mx, #r mx, mx), c0 < #c mx, c < #c mx, c < c0, m ≤ n, n ≤ #r mx ⊦ count(mx[c]c, m, n, λ j. j < i) ≥ countevn(mx[c0]c, m, n, λ j. j < i) | A User Theorem |
| srowsorted-oddrowordered | #r mx = #r mx0, r < #r mx ⊦ srowsorted(mx0, #r mx0, mx) ∧ odd(r) → ordered≤(rev(mx[r]r)) | A User Theorem |
| log2ub-zero | ⊦ log2↑(n) = 0 ↔ n ≤ 1 | A User Theorem |
| colno-updrow | #c mx = # a, r < #r mx ⊦ #c mx[r, a]r = #c mx | An Axiom |
| exists-max1column | #c mx ≠ 0 ⊦ ∃ c. c < #c mx ∧ (∀ c0. c0 < #c mx → count(mx[c0]c, λ j. ¬ j < i) ≤ count(mx[c]c, λ j. ¬ j < i)) | A User Theorem |
| log2ub-lem | ⊦ n ≠ 0 → n /↑ 2^ log2↑(n) = 1 | A User Theorem |
| rowperms-clean1unchanged | #r mx = #r mx0, #c mx = #c mx0, #c mx ≠ 0, ∀ r. r < #r mx → perm(mx0[r]r, mx[r]r) ⊦ #clean1rows(mx0, i) = #clean1rows(mx, i) ↔ true | A User Theorem |
| colsorted-clean0notls | #c mx ≠ 0, #r mx = #r mx0, #c mx = #c mx0 ⊦ colsorted(mx0, #c mx0, mx) → ¬ #clean0rows(mx, i) < #clean0rows(mx0, i) | A User Theorem |
| sort-possible | ⊦ ∃ a0. perm(a, a0) ∧ ordered≤((asc ⊃ a0;rev(a0))) ∧ # a = # a0 | A User Theorem |
| count-add-even-odd | ⊦ countevn(a, p) + countodd(a, p) = count(a, p) | A User Theorem |
| exists-max0column-ind | n < #c mx ⊦ ∃ c. c ≤ n ∧ (∀ c0. c0 ≤ n → count(mx[c0]c, λ j. j < i) ≤ count(mx[c]c, λ j. j < i)) | A User Theorem |
| psortrows | psortrows#(; MX){forall∥nf R with R < #r MX do psortrow#(R; MX)} | An Axiom |
| log2ub-log2 | ⊦ log2↑(n) = (n = 0 ⊃ 0;(∃ m. n = 2^ m ⊃ log2 n;log2 n + 1)) | A User Theorem |
| countodd-zero-ind | ∀ r. m ≤ r ∧ r < n ∧ odd(r) → ¬ p(a[r]), m ≤ n, n ≤ # a ⊦ countodd(a, m, n, p) = 0 | A User Theorem |
| colsorted-permtoArc-ind | #r mx = #r mx0, #c mx = #c mx0, c ≤ #c mx0, m ≤ #c mx0 ⊦ colsorted(mx0, c, mx) → perm(toArc(mx0, m), toArc(mx, m)) | A User Theorem |
| fullcountodd-range | m ≤ n, n ≤ # a, ∀ n0. m ≤ n0 ∧ n0 < n ∧ odd(n0) → p(a[n0]) ⊦ countodd(a, m, n, p) = (odd(m) ⊃ (n + 1 - m) / 2;(n - m) / 2) | A User Theorem |
| sortedperm-count-splits | perm(a0, a), ordered≤(a), # a0 = # a, n < # a ⊦ a[n] < i ↔ n < count(a0, λ j. j < i) | A User Theorem |
| clean0rows-allls | ⊦ r < #clean0rows(mx, i) → count(mx[r]r, λ j. ¬ j < i) = 0 | An Axiom |
| srowsorted-permrow | #r mx = #r mx0, r < #r mx ⊦ srowsorted(mx0, #r mx0, mx) → perm(mx0[r]r, mx[r]r) | A User Theorem |
| clean1rows-notallge | ⊦ #clean1rows(mx, i) + r + 1 = #r mx → count(mx[r]r, λ j. j < i) ≠ 0 | An Axiom |
| ordered-rev | ⊦ ordered≤(rev(a)) ↔ ordered≥(a) | A User Theorem |
| max0column-countcol-big-odd | #r mx = #r mx0, #c mx = #c mx0, c < #c mx, c0 < #c mx, c ≥ c0, srowsorted(mx0, #r mx0, mx0), colsorted(mx0, #c mx, mx), ∀ c. c < #c mx → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i) ⊦ count(mx[c]c, λ j. j < i) ≥ #clean0rows(mx0, i) + countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx, λ j. j < i) | A User Theorem |
| dirtyrowsone-rowsincreasing | #r mx = #r mx0, #c mx = #c mx0 ⊦ mx.dirtyrows≤(1) ∧ colsorted(mx0, #c mx, mx) → rowsincreasing(mx, #r mx) | A User Theorem |
| divup-one | ⊦ m /↑ 1 = m | A User Theorem |
| psortrowssnake-correct | #c mx ≠ 0, mx = mx0 ⊦ ⟪psortrowssnake#(; mx)⟫ (#r mx0 = #r mx ∧ #c mx = #c mx0 ∧ perm(mx0.toArr, mx.toArr) ∧ srowsorted(mx0, #r mx, mx)) | A User Theorem |
| rowperms-clean0unchanged | #r mx = #r mx0, #c mx = #c mx0, #c mx ≠ 0, ∀ r. r < #r mx → perm(mx0[r]r, mx[r]r) ⊦ #clean0rows(mx0, i) = #clean0rows(mx, i) ↔ true | A User Theorem |
| colsorted-clean1notls | #c mx ≠ 0, #r mx = #r mx0, #c mx = #c mx0 ⊦ colsorted(mx0, #c mx0, mx) → ¬ #clean1rows(mx, i) < #clean1rows(mx0, i) | A User Theorem |
| colsorted-samecount-above-clean0 | #r mx = #r mx0, #c mx = #c mx0, c < #c mx, colsorted(mx0, #c mx, mx) ⊦ count(mx0[c]c, #clean0rows(mx0, i), #r mx, λ j. j < i) = count(mx[c]c, #clean0rows(mx0, i), #r mx, λ j. j < i) | A User Theorem |
| exists-max0column | #c mx ≠ 0 ⊦ ∃ c. c < #c mx ∧ (∀ c0. c0 < #c mx → count(mx[c0]c, λ j. j < i) ≤ count(mx[c]c, λ j. j < i)) | A User Theorem |
| clean1rows-bounded | ⊦ ¬ #r mx < #clean1rows(mx, i) | An Axiom |
| clean0rows-bounded | ⊦ ¬ #r mx < #clean0rows(mx, i) | An Axiom |
| max0column-determines-clean1rows | c0 < #c mx, ∀ c. c < #c mx → ordered≤(mx[c]c), ∀ c. c < #c mx → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i) ⊦ #clean1rows(mx, i) + count(mx[c0]c, λ j. j < i) = #r mx | A User Theorem |
| divup2-def | ⊦ n /↑ 2 = (even(n) ⊃ n / 2;(n + 1) / 2) | A User Theorem |
| rowperms-dirtyrowsunchanged | #r mx = #r mx0, #c mx = #c mx0, #c mx ≠ 0, ∀ r. r < #r mx → perm(mx0[r]r, mx[r]r) ⊦ #dirtyrows(mx0, i) = #dirtyrows(mx, i) ↔ true | A User Theorem |
| psortrowssnake | psortrowssnake#(; MX){forall∥nf M with M < #r MX do psortrowsnake#(M, even(M); MX)} | An Axiom |
| colsorted-permcol | #c mx = #c mx0, c < #c mx ⊦ colsorted(mx0, #c mx0, mx) → perm(mx0[c]c, mx[c]c) | A User Theorem |
| dirytrows-zero | #c mx ≠ 0 ⊦ #dirtyrows(mx, i) = 0 → (∀ r. r < #r mx → count(mx[r]r, λ j. j < i) = 0 ∨ count(mx[r]r, λ j. ¬ j < i) = 0) | A User Theorem |
| rowno-updcol | #r mx = # a, c < #c mx ⊦ #r mx[c, a]c = #r mx | An Axiom |
| exists-max1column-ind | n < #c mx ⊦ ∃ c. c ≤ n ∧ (∀ c0. c0 ≤ n → count(mx[c0]c, λ j. ¬ j < i) ≤ count(mx[c]c, λ j. ¬ j < i)) | A User Theorem |
| count0-leq-clean0 | c < #c mx ⊦ #clean0rows(mx, i) ≤ count(mx[c]c, λ j. j < i) | A User Theorem |
| countodd-bounded-ind | m ≤ n, n ≤ # a ⊦ countodd(a, m, n, p) ≤ (odd(m) ⊃ (n + 1 - m) / 2;(n - m) / 2) | A User Theorem |
| colsorted-count-below-clean0rows | #r mx = #r mx0, #c mx = #c mx0, c < #c mx, colsorted(mx0, #c mx, mx) ⊦ count(mx[c]c, 0, #clean0rows(mx0, i), λ j. j < i) = #clean0rows(mx0, i) | A User Theorem |
| srowsorted-def | ⊦ m ≤ #r mx → ( srowsorted(mx0, m, mx) ↔ #r mx = #r mx0 ∧ #c mx = #c mx0 ∧ (∀ r. r < #r mx → (r < m ⊃ perm(mx0[r]r, mx[r]r) ∧ ordered≤((even(r) ⊃ mx[r]r;rev(mx[r]r)));mx0[r]r = mx[r]r))) | An Axiom |
| dirtyrows-def | ⊦ #dirtyrows(mx, i) + #clean0rows(mx, i) + #clean1rows(mx, i) = #r mx | An Axiom |
| pshearsort | pshearsort#(; MX) {let N = log2↑(#r MX) in {/* invariant perm(MX`.toArr, MX.toArr) ∧ #c MX = #c MX` ∧ #r MX = #r MX` ∧ #c MX ≠ 0 ∧ MX.dirtyrows≤(#r MX /↑ 2^(N` - N)) ∧ N ≤ N` ∧ (N = 0 → colsorted(MX, #c MX, MX)) wfbound N */; while N > 0 do {/* use contract psortrowssnake-correct and skip call */; psortrowssnake#(; MX); /* use contract psortcols-correct and skip call */; psortcols#(; MX); N := N - 1}}; /* use contract psortrows-correct and skip call */; psortrows#(; MX) } | An Axiom |
| rowsincreasing-def | ⊦ rowsincreasing(mx, r) ↔ (∀ r1, r2, c1, c2. r1 < r2 ∧ r2 < r ∧ c1 < #c mx ∧ c2 < #c mx → ¬ mx[r2, c2] < mx[r1, c1]) | An Axiom |
| psortrowsnake | psortrowsnake#(M, ASC; MX){if ASC then psortrow#(M; MX) else psortrowrev#(M; MX)} | An Axiom |
| max0column-clean0rowsbounded | #r mx = #r mx0, #c mx = #c mx0, c0 < #c mx, srowsorted(mx0, #r mx0, mx0), colsorted(mx0, #c mx, mx), ∀ c. c < #c mx → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i) ⊦ #clean0rows(mx, i) ≥ #clean0rows(mx0, i) + min (countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx, λ j. j < i)) | A User Theorem |
| countevn-def | ⊦ countevn(a, p) = countevn(a, 0, # a, p) | An Axiom |
| srowsorted-evenrowordered | #r mx = #r mx0, r < #r mx ⊦ srowsorted(mx0, #r mx0, mx) ∧ even(r) → ordered≤(mx[r]r) | A User Theorem |
| fullcountevn-range | m ≤ n, n ≤ # a, ∀ n0. m ≤ n0 ∧ n0 < n ∧ even(n0) → p(a[n0]) ⊦ countevn(a, m, n, p) = (even(m) ⊃ (n + 1 - m) / 2;(n - m) / 2) | A User Theorem |
| countevn-base | m ≤ # a ⊦ countevn(a, m, m, p) = 0 | An Axiom |
| rowno-updrow | #c mx = # a, r < #r mx ⊦ #r mx[r, a]r = #r mx | An Axiom |
| dirtyrows-trivialbound | #c mx ≠ 0 ⊦ mx.dirtyrows≤(#r mx) | A User Theorem |
| countevn-maxcol0-bounded | c0 < #c mx0 ⊦ countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) ≤ #dirtyrows(mx0, i) /↑ 2 | A User Theorem |
| srowsorted-permtoArr-ind | #r mx = #r mx0, #c mx = #c mx0, r ≤ #r mx0, m ≤ #r mx0 ⊦ srowsorted(mx0, r, mx) → perm(toArr(mx0, m), toArr(mx, m)) | A User Theorem |
| count1-leq-clean1 | c < #c mx ⊦ #clean1rows(mx, i) ≤ count(mx[c]c, λ j. ¬ j < i) | A User Theorem |
| countodd-def | ⊦ countodd(a, p) = countodd(a, 0, # a, p) | An Axiom |
| psortcols-correct | #c mx ≠ 0, #r mx ≠ 0, mx = mx0, srowsorted(mx, #r mx0, mx) ⊦ ⟪psortcols#(; mx)⟫ (#r mx0 = #r mx ∧ #c mx = #c mx0 ∧ perm(mx0.toArr, mx.toArr) ∧ colsorted(mx0, #c mx, mx)) | A User Theorem |
| divup-half | ⊦ (m /↑ 2^ n) /↑ 2 = m /↑ 2^(n + 1) | A User Theorem |
| pshearsort-correct | mx = mx0, #r mx ≠ 0, #c mx ≠ 0 ⊦ ⟪pshearsort#(; mx)⟫ (perm(mx0.toArr, mx.toArr) ∧ ordered≤(mx.toArr)) | A User Theorem |
| countevn-bounded-ind | m ≤ n, n ≤ # a ⊦ countevn(a, m, n, p) ≤ (even(m) ⊃ (n + 1 - m) / 2;(n - m) / 2) | A User Theorem |
| srowsorted-permtoArr | #r mx = #r mx0, #c mx = #c mx0, r ≤ #r mx0 ⊦ srowsorted(mx0, r, mx) → perm(mx0.toArr, mx.toArr) | A User Theorem |
| rowsorted-biggercol-oddbounded | srowsorted(mx, #r mx, mx), c0 < #c mx, c < #c mx, c0 < c, m ≤ n, n ≤ #r mx ⊦ count(mx[c]c, m, n, λ j. j < i) ≥ countodd(mx[c0]c, m, n, λ j. j < i) | A User Theorem |
| countodd-base | m ≤ # a ⊦ countodd(a, m, m, p) = 0 | An Axiom |
| rowsincreasing-allrowsorted-sorted-ind | rowsincreasing(mx, #r mx), r ≤ #r mx, ∀ r0. r0 < r → ordered≤(mx[r0]r) ⊦ ordered≤(toArr(mx, r)) | A User Theorem |
| count-add-even-odd-ind | m ≤ n, n ≤ # a ⊦ countevn(a, m, n, p) + countodd(a, m, n, p) = count(a, m, n, p) | A User Theorem |
| count1-leq-clean1-ind | c < #c mx ⊦ m ≤ #clean1rows(mx, i) → count(mx[c]c, #r mx - #clean1rows(mx, i), (#r mx - #clean1rows(mx, i)) + m, λ j. ¬ j < i) = m | A User Theorem |
| count0-leq-clean0-ind | c < #c mx ⊦ m ≤ #clean0rows(mx, i) → count(mx[c]c, 0, m, λ j. j < i) = m | A User Theorem |
| countevn-append-ind | m ≤ n, n ≤ n0, n0 ≤ # a ⊦ countevn(a, m, n, p) + countevn(a, n, n0, p) = countevn(a, m, n0, p) | A User Theorem |
| max0column-countcol-small-even | #r mx = #r mx0, #c mx = #c mx0, c < #c mx, c0 < #c mx, c < c0, srowsorted(mx0, #r mx0, mx0), colsorted(mx0, #c mx, mx), ∀ c. c < #c mx → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i) ⊦ count(mx[c]c, λ j. j < i) ≥ #clean0rows(mx0, i) + countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx, λ j. j < i) | A User Theorem |
| colsort-dirtyboundhalf | #r mx0 = #r mx, #c mx0 = #c mx, #c mx ≠ 0 ⊦ colsorted(mx0, #c mx, mx) ∧ mx0.dirtyrows≤(bound) ∧ srowsorted(mx0, #r mx0, mx0) → mx.dirtyrows≤(bound /↑ 2) | A User Theorem |