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: |
|---|---|---|
| next | next#(; ar; hasNext) {let ghostar = ar in if # ar = 0 then hasNext := false else let i = (# ar)-1 in {while i > 0 ∧ ar[i -1] ≥ ar[i] do {/* next-perm: invariant i < # ar wfbound i; next-proper-permutation: invariant i < # ar ∧ ordered≤(rev(subarray(ar, i, # ar - i))) wfbound i */; i := i -1}; if i ≤ 0 then hasNext := false else {let j = (# ar)-1 in {while ar[j] ≤ ar[i -1] do {/* next-perm: invariant j < # ar ∧ i ≤ j ∧ i ≠ 0 wfbound j; next-proper-permutation: invariant j < # ar ∧ i ≤ j ∧ i ≠ 0 ∧ ordered≤(rev(subarray(ar, i, # ar - i))) ∧ (∀ n. n > j ∧ n < # ar → ar[n] ≤ ar[i - 1]) wfbound j */; j := j -1}; let temp = ar[i -1] in {ar[i -1] := ar[j]; ar[j] := temp; /* next-proper-permutation: ordered≤(rev(subarray(ar, i, # ar - i))) ∧ (∀ n. n ≥ j ∧ n < # ar → ar[n] < ar[i - 1]) ∧ ghostar ≠ ar ∧ ghostar ≤ ar ∧ ghostar[j] = ar[i - 1] */; let ghost_j = j in {j := (# ar)-1; while i < j do {/* next-perm: invariant perm(ar`, ar) ∧ i ≠ 0 ∧ i < # ar ∧ j < # ar wfbound j; next-proper-permutation: invariant j < # ar ∧ i < # ar ∧ i ≠ 0 ∧ i` ≤ i ∧ perm(ghostar, ar) ∧ subarray(ghostar, 0, i` - 1) = subarray(ar, 0, i` - 1) ∧ ghostar[ghost_j] = ar[i` - 1] ∧ ( i < j → rev(subarray(ar`, i`, # ar - i`)) = subarray(ar, i`, i - i`) + rev(subarray(ar, i, j + 1 - i)) + subarray(ar, j + 1, # ar - j + 1)) ∧ (i ≥ j → rev(subarray(ar`, i`, # ar - i`)) = subarray(ar, i`, # ar - i`)) wfbound j */; temp := ar[i]; ar[i] := ar[j]; ar[j] := temp; i := i +1; j := j -1}}}}; hasNext := true}} } | An Axiom |
| smaller-perms | ⊦ ar0 ∈ smallerPerms(ar) ↔ ar ≠ ar0 ∧ perm(ar, ar0) ∧ ar0 ≤ ar | An Axiom |
| toSet | ⊦ ar ∈ arx.toSet ↔ ar ∈ arx | An Axiom |
| EndIncreasingPart-rec | ⊦ m1 ≤ m2 → EndIncreasingPart(m1 ' + m2 ' + ar) = 1 + EndIncreasingPart(m2 ' + ar) | An Axiom |
| lexicographic-base1 | ⊦ [] ≤ [] | An Axiom |
| sort-def | ar0 = ar ⊦ ⟨sort#(; ar)⟩ (ordered≤(ar) ∧ perm(ar0, ar)) | An Axiom |
| ordered-arraylist-rec | ⊦ ordered≤(ar0 ' + ar1 ' + arx) ↔ ar0 ≤ ar1 ∧ ordered≤(ar1 ' + arx) | An Axiom |
| hasGreaterElem-rec2 | ⊦ n > m → (hasGreaterElem(n + ar, m) ↔ true) | An Axiom |
| minimum-permutation | ⊦ min(ar1) ↔ (∀ ar2. perm(ar1, ar2) → ar1 ≤ ar2) | An Axiom |
| next-permutation | ⊦ nextperm(ar1, ar2) ↔ perm(ar1, ar2) ∧ ar1 ≠ ar2 ∧ ar1 ≤ ar2 ∧ (∀ ar3. perm(ar1, ar3) ∧ ar3 ≠ ar1 ∧ ar3 ≠ ar2 → ¬(ar1 ≤ ar3 ∧ ar3 ≤ ar2)) | An Axiom |
| greater-perms | ⊦ ar0 ∈ greaterPerms(ar) ↔ ar ≠ ar0 ∧ perm(ar, ar0) ∧ ar ≤ ar0 | An Axiom |
| lexicographic-rec1 | ⊦ n ' + ar1 ≤ m ' + ar2 ↔ (n = m ⊃ ar1 ≤ ar2;n ≤ m) | An Axiom |
| EndIncreasingPart-base | ⊦ m1 > m2 → EndIncreasingPart(m1 ' + m2 ') = 0 | An Axiom |
| lexicographic-base3 | ⊦ ¬ ar1 ≤ [] | An Axiom |
| maximum-permutation | ⊦ max(ar1) ↔ (∀ ar2. perm(ar1, ar2) → ar2 ≤ ar1) | An Axiom |
| permut | permut#(; ar, listofar) {listofar := []; sort#(; ar); let hasNext = true in while hasNext do {/* invariant ¬ dups(listofar) ∧ perm(ar, ar`) ∧ ordered≤(listofar) ∧ (hasNext ⊃ listofar.toSet = smallerPerms(ar);listofar.toSet = smallerPerms(ar) ++ ar) ∧ (¬ hasNext → max(ar)) wfbound # greaterPerms(ar) + (hasNext ⊃ 1;0) */; listofar := listofar + ar; next#(; ar; hasNext)} } | An Axiom |
| hasGreaterElem-rec1 | ⊦ n ≤ m → hasGreaterElem(n + ar, m) ↔ hasGreaterElem(ar, m) | An Axiom |
| ordered-arraylist-base1 | ⊦ ordered≤(ar ') | An Axiom |
| hasGreaterElem-base | ⊦ ¬ hasGreaterElem([], m) | An Axiom |
| all-perms | ⊦ ar0 ∈ allPerms(ar) ↔ perm(ar, ar0) | An Axiom |
| lexicographic-base2 | ⊦ [] ≤ ar2 | An Axiom |
| ordered-arraylist-base0 | ⊦ ordered≤([]) | An Axiom |
| array-le-kill-prefix | ⊦ # ar3 = n0 + m + 1 ∧ subarray(ar1, 0, m) = subarray(ar3, 0, m) ∧ m + 1 < # ar3 ∧ n0 ≠ 0 ∧ ar1 ≠ ar3 ∧ perm(ar1, ar2) ∧ perm(ar2, ar3) ∧ ar1 ≤ ar2 ∧ ar2 ≤ ar3 ∧ ar2 ≠ ar1 ∧ ar2 ≠ ar3 → subarray(ar1, m, n0 + 1) ≤ subarray(ar2, m, n0 + 1) ∧ subarray(ar2, m, n0 + 1) ≤ subarray(ar3, m, n0 + 1) ∧ perm(subarray(ar1, m, n0 + 1), subarray(ar2, m, n0 + 1)) ∧ perm(subarray(ar2, m, n0 + 1), subarray(ar3, m, n0 + 1)) ∧ subarray(ar1, m, n0 + 1) ≠ subarray(ar2, m, n0 + 1) ∧ subarray(ar2, m, n0 + 1) ≠ subarray(ar3, m, n0 + 1) | A User Theorem |
| array-le-one-diffrent-position | ⊦ ar1[m] < ar2[m] ∧ m < # ar2 ∧ m < # ar1 ∧ subarray(ar1, 0, m) = subarray(ar2, 0, m) → ar1 ≤ ar2 | A User Theorem |
| array-le-refl | ⊦ ar ≤ ar | A User Theorem |
| array-le-same-prefix | ⊦ x + y1 ≤ ar2 ∧ ar2 ≤ x + y3 → (∃ y2. ar2 = x + y2) | A User Theorem |
| array-le-same-prefix2 | ⊦ ar + ar1 ≤ ar + ar2 ↔ ar1 ≤ ar2 | A User Theorem |
| array-le-same-prefix3 | ⊦ ar1 = ar + ar11 ∧ ar2 = ar + ar22 → (ar1 ≤ ar2 ↔ ar11 ≤ ar22) | A User Theorem |
| array-le-same-prepart | ⊦ ar1 ≤ ar2 ∧ ar2 ≤ ar3 ∧ subarray(ar1, 0, m) = subarray(ar3, 0, m) ∧ m < # ar1 ∧ m < # ar2 ∧ m < # ar3 → subarray(ar1, 0, m) = subarray(ar2, 0, m) | A User Theorem |
| array-le-same-prepart2 | ⊦ ar1 ≤ ar2 ∧ ar2 ≤ ar3 ∧ subarray(ar1, 0, m) = subarray(ar3, 0, m) ∧ perm(ar1, ar2) ∧ perm(ar2, ar3) ∧ m < # ar1 → subarray(ar1, 0, m) = subarray(ar2, 0, m) | A User Theorem |
| array-le-split | ⊦ ar1 = ar11 + ar12 → (ar1 ≤ ar2 ↔ ar11 + ar12 ≤ ar2) | A User Theorem |
| array-le-swap | ⊦ i < # ar ∧ j < # ar ∧ i < j → (ar ≤ ar[i, ar[j]][j, ar[i]] ↔ ar[i] ≤ ar[j]) | A User Theorem |
| array-le-trans | ⊦ ar0 ≤ ar1 ∧ ar1 ≤ ar2 → ar0 ≤ ar2 | A User Theorem |
| array-neg-le-eq | ⊦ ar0 ≠ ar1 ∧ ¬ ar1 ≤ ar0 → ar0 ≤ ar1 | A User Theorem |
| array-neg-le-eq-2 | ⊦ ar0 ≠ ar1 ∧ ar0 ≤ ar1 → ¬ ar1 ≤ ar0 | A User Theorem |
| array-split-into-subarrays | m < # ar ⊦ ar = subarray(ar, 0, m) + subarray(ar, m, # ar - m) | A User Theorem |
| ascending-order-is-min-permuted | ⊦ ordered≤(ar) → min(ar) | A User Theorem |
| descending-order-is-max-permuted | ⊦ ordered≤(rev(ar)) → max(ar) | A User Theorem |
| get-rev | ⊦ n < # ar → rev(ar)[n] = ar[# ar - n + 1] | A User Theorem |
| max-smaller-perms-all-perms | ⊦ max(ar) → smallerPerms(ar) ++ ar = allPerms(ar) | A User Theorem |
| next-perm | ar = ar0 ⊦ ⟨next#(; ar; hasNext)⟩ perm(ar, ar0) | A User Theorem |
| next-perm-greaterPerms | ⊦ nextperm(ar1, ar2) → greaterPerms(ar1) = greaterPerms(ar2) ++ ar2 | A User Theorem |
| next-perm-smallerPerms | ⊦ nextperm(ar1, ar2) → smallerPerms(ar2) = smallerPerms(ar1) ++ ar1 | A User Theorem |
| next-proper-permutation | ar = ar0 ⊦ ⟨next#(; ar; hasNext)⟩ (hasNext ⊃ nextperm(ar0, ar);ar = ar0 ∧ max(ar)) | A User Theorem |
| nil-toSet | ⊦ [].toSet = ∅ | A User Theorem |
| not-ordered | ⊦ i > j ∧ i ∈ ar1 ∧ j ∈ ar2 → ¬ ordered≤(ar1 + ar2) | A User Theorem |
| ordered-all-rev | ⊦ ordered≤(rev(ar)) ↔ (∀ m, n. m ≤ n ∧ n < # ar → ¬ ar[m] < ar[n]) | A User Theorem |
| ordered-append | ⊦ ordered≤(arx) ∧ arx.toSet = smallerPerms(ar) → ordered≤(arx + ar ') | A User Theorem |
| ordered-arraylist-append-last | ⊦ ordered≤(arx + ar0 ') → (ordered≤(arx + ar0 ' + ar ') ↔ ar0 ≤ ar) | A User Theorem |
| ordered-arraylist-two | ⊦ ordered≤(ar0 ' + ar1 ') ↔ ar0 ≤ ar1 | A User Theorem |
| ordered-notsmaller | ⊦ ordered≤(ar) ∧ perm(ar, ar0) ∧ ar ≠ ar0 → ¬ ar0 ≤ ar | A User Theorem |
| ordered-size-smaller-one | ⊦ # ar ≤ 1 → ordered≤(ar) | A User Theorem |
| ordered-smallerPerms | ⊦ ordered≤(ar) → smallerPerms(ar) = ∅ | A User Theorem |
| ordered-step-down | ⊦ # ar0 = (n0 + 1) + m ∧ ordered≤(rev(subarray(ar0, m + 1, n0))) ∧ ar0[m + 1] ≤ ar0[m] → ordered≤(rev(subarray(ar0, m, n0 + 1))) | A User Theorem |
| perm-all-perms-eq | ⊦ perm(ar0, ar1) → allPerms(ar0) = allPerms(ar1) | A User Theorem |
| permut-correct | ar0 = ar ⊦ ⟨permut#(; ar, listofar)⟩ (¬ dups(listofar) ∧ ordered≤(listofar) ∧ listofar.toSet = allPerms(ar0)) | A User Theorem |
| remains-ordered-by-swap | ⊦ # ar1 = n0 + m + 1 ∧ n0 ≠ 0 ∧ ar1[m] < ar1[j] ∧ j < # ar1 ∧ m < j ∧ ordered≤(rev(subarray(ar1, m + 1, n0))) ∧ (∀ n. j < n ∧ n < # ar1 → ar1[n] ≤ ar1[m]) → ordered≤(rev(subarray(ar1[m, ar1[j]][j, ar1[m]], m + 1, n0))) | A User Theorem |
| rev-mkarray-empty | ⊦ rev(mkarray(0)) = [] | A User Theorem |
| rev-subarray-last | m + n < # ar, n ≠ 0 ⊦ rev(subarray(ar, m, n)).last = ar[m] | A User Theorem |
| rev-subarray-split-last-swap | 3 + n0 + k + n + m ≤ # ar ⊦ k ≤ 1 → subarray(ar, m + 1, n) + rev(subarray(ar, m + n + 1, k + 2)) + subarray(ar, m + n + 3 + k, n0) = subarray(ar[m + n + 1, ar[m + n + k + 2]][m + n + k + 2, ar[m + n + 1]], m + 1, n + k + 2 + n0) | A User Theorem |
| rev-subarray-split-step | 3 + n0 + k + n + m ≤ # ar ⊦ subarray(ar[m + n + 1, ar[m + n + 2 + k]], m + 1, n + 1) + rev(subarray(ar, m + n + 2, k)) + subarray(ar[m + n + 2 + k, ar[m + n + 1]], n + m + 2 + k, n0 + 1) = subarray(ar, m + 1, n) + rev(subarray(ar, m + n + 1, k + 2)) + subarray(ar, n + m + 3 + k, n0) | A User Theorem |
| subarray-inc | m + n < # ar ⊦ subarray(ar, m, n + 1) = subarray(ar, m, n) + ar[m + n] | A User Theorem |
| subarray-inc-offset | m + n < # ar ⊦ subarray(ar, m + 1, n) = (subarray(ar, m, n) + ar[m + n]).rest | A User Theorem |
| subarray-inc-offset0 | m + n ≤ # ar, n ≠ 0 ⊦ subarray(ar, m, n) = ar[m] + subarray(ar, m + 1, n - 1) | A User Theorem |
| subarray-prefix-fistn | m < # ar ⊦ subarray(ar, 0, m) = firstn(m, ar) | A User Theorem |
| subarray-write-above | n ≥ n0 + n1 ⊦ subarray(ar[n, a], n0, n1) = subarray(ar, n0, n1) | A User Theorem |