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: |
|---|---|---|
| scolsorted-colordered | #c mx = #c mx0, c < #c mx ⊦ scolsorted(mx, #c mx0, mx0) → ordered≤(mx[c]c) | A User Theorem |
| sortcols-correct | #c mx ≠ 0, mx = mx0, srowsorted(mx, #r mx0, mx), mx.dirtyrows≤(bound) ⊦ ⟪sortcols#(; mx)⟫ (#r mx0 = #r mx ∧ #c mx = #c mx0 ∧ perm(mx0.toArr, mx.toArr) ∧ scolsorted(mx, #c mx, mx0) ∧ mx.dirtyrows≤(bound /↑ 2)) | 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 |
| 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 |
| shearsort | shearsort#(; mx) {let n = log2↑(#r mx) in while n > 0 do {/* 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 → scolsorted(mx, #c mx, mx)) wfbound n */; /* use contract sortrowssnake-correct and skip call */; sortrowssnake#(; mx); /* use contract sortcols-correct and skip call */; sortcols#(; mx); n := n - 1}; /* use contract sortrows-correct and skip call */; sortrows#(; mx) } | An Axiom |
| 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, scolsorted(mx, #c mx, mx0), ∀ 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 |
| 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 |
| clean1rows-allge | ⊦ #r mx ≤ #clean1rows(mx, i) + r ∧ r < #r mx → count(mx[r]r, λ j. j < i) = 0 | An Axiom |
| sortcol-correct | m < #c mx, scolsorted(mx, m, mx0), #r mx0 = #r mx, #c mx = #c mx0 ⊦ ⟪sortcol#(m; mx)⟫ (#r mx0 = #r mx ∧ #c mx = #c mx0 ∧ perm(mx0.toArr, mx.toArr) ∧ scolsorted(mx, m + 1, mx0)) | A User Theorem |
| srowsorted-dirtyboundunchanged | #c mx ≠ 0, #r mx = #r mx0, #c mx = #c mx0 ⊦ mx0.dirtyrows≤(bound) ∧ srowsorted(mx, #r mx0, mx0) → 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 |
| scolsorted-permtoArc-ind | #r mx = #r mx0, #c mx = #c mx0, c ≤ #c mx0, m ≤ #c mx0 ⊦ scolsorted(mx, c, mx0) → perm(toArc(mx0, m), toArc(mx, m)) | A User Theorem |
| 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 |
| sortrowssnake-correct | #c mx ≠ 0, mx = mx0, mx.dirtyrows≤(bound) ⊦ ⟪sortrowssnake#(; mx)⟫ ( #r mx0 = #r mx ∧ #c mx = #c mx0 ∧ perm(mx0.toArr, mx.toArr) ∧ srowsorted(mx, #r mx, mx0) ∧ mx.dirtyrows≤(bound) ∧ #c mx ≠ 0) | A User Theorem |
| sortcols | sortcols#(; mx) {let m = 0 in while m < #c mx do {/* invariant scolsorted(mx, m, mx`) ∧ perm(mx`.toArr, mx.toArr) ∧ #c mx = #c mx` ∧ #r mx = #r mx` ∧ m ≤ #c mx ∧ #c mx ≠ 0 wfbound #c mx - m */; /* use contract sortcol-correct and skip call */; sortcol#(m; mx); m := m + 1} } | An Axiom |
| srowsorted-oddrowordered | #r mx = #r mx0, r < #r mx ⊦ srowsorted(mx, #r mx0, mx0) ∧ 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 |
| sort-possible | ⊦ ∃ a0. perm(a, a0) ∧ ordered≤((asc ⊃ a0;rev(a0))) ∧ # a = # a0 | A User Theorem |
| sortrow | sortrow#(m, asc; mx){choose a with # a = #c mx ∧ perm(mx[m]r, a) ∧ ordered≤((asc ⊃ a;rev(a))) in mx[m]r := a} | An Axiom |
| 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 |
| 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 |
| 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(mx, #r mx0, mx0) → 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 |
| 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), scolsorted(mx, #c mx, mx0), ∀ 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 |
| scolsorted-clean0notls | #c mx ≠ 0, #r mx = #r mx0, #c mx = #c mx0 ⊦ scolsorted(mx, #c mx0, mx0) → ¬ #clean0rows(mx, i) < #clean0rows(mx0, i) | A User Theorem |
| dirtyrowsone-rowsincreasing | #r mx = #r mx0, #c mx = #c mx0 ⊦ mx.dirtyrows≤(1) ∧ scolsorted(mx, #c mx, mx0) → rowsincreasing(mx, #r mx) | A User Theorem |
| divup-one | ⊦ m /↑ 1 = m | 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 |
| sortrowssnake | sortrowssnake#(; mx) {let m = 0 in while m < #r mx do {/* invariant srowsorted(mx, m, mx`) ∧ perm(mx`.toArr, mx.toArr) ∧ #c mx = #c mx` ∧ #r mx = #r mx` ∧ m ≤ #r mx ∧ #c mx ≠ 0 wfbound #r mx - m */; /* use contract sortrowsnake-correct and skip call */; sortrow#(m, even(m); mx); m := m + 1} } | An Axiom |
| shearsort-correct | mx = mx0, #r mx ≠ 0, #c mx ≠ 0 ⊦ ⟪shearsort#(; mx)⟫ (perm(mx0.toArr, mx.toArr) ∧ ordered≤(mx.toArr)) | 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 |
| sortrows-correct | mx = mx0, rowsincreasing(mx, #r mx) ⊦ ⟪sortrows#(; mx)⟫ (#r mx0 = #r mx ∧ #c mx = #c mx0 ∧ perm(mx0.toArr, mx.toArr) ∧ ordered≤(mx.toArr)) | A User Theorem |
| 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 |
| sortrows | sortrows#(; mx) {let m = 0 in while m < #r mx do {/* invariant ordered≤(toArr(mx, m)) ∧ rowsincreasing(mx, #r mx) ∧ perm(mx`.toArr, mx.toArr) ∧ #c mx = #c mx` ∧ #r mx = #r mx` ∧ m ≤ #r mx wfbound #r mx - m */; /* use contract sortrow-correct and skip call */; sortrow#(m, true; mx); m := m + 1} } | An Axiom |
| 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 |
| 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 |
| scolsorted-permcol | #c mx = #c mx0, c < #c mx ⊦ scolsorted(mx, #c mx0, mx0) → perm(mx0[c]c, mx[c]c) | A User Theorem |
| 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 |
| scolsorted-clean1notls | #c mx ≠ 0, #r mx = #r mx0, #c mx = #c mx0 ⊦ scolsorted(mx, #c mx0, mx0) → ¬ #clean1rows(mx, i) < #clean1rows(mx0, 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 |
| srowsorted-def | ⊦ m ≤ #r mx → ( srowsorted(mx, m, mx0) ↔ #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 |
| 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 |
| sortrowsnake-correct | #c mx ≠ 0, m < #r mx, #r mx0 = #r mx, #c mx = #c mx0, srowsorted(mx, m, mx0), asc ↔ even(m), perm(mx0.toArr, mx.toArr) ⊦ ⟪sortrow#(m, asc; mx)⟫ (#r mx0 = #r mx ∧ #c mx = #c mx0 ∧ perm(mx0.toArr, mx.toArr) ∧ #c mx ≠ 0 ∧ srowsorted(mx, m + 1, mx0)) | A User Theorem |
| max0column-clean0rowsbounded | #r mx = #r mx0, #c mx = #c mx0, c0 < #c mx, srowsorted(mx0, #r mx0, mx0), scolsorted(mx, #c mx, mx0), ∀ 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 |
| scolsorted-permtoArr | #r mx = #r mx0, #c mx = #c mx0, c ≤ #c mx0 ⊦ scolsorted(mx, c, mx0) → perm(mx0.toArr, mx.toArr) | 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(mx, #r mx0, mx0) ∧ 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 |
| scolsorted-def | ⊦ m ≤ #c mx → ( scolsorted(mx, m, mx0) ↔ #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 |
| rowno-updrow | #c mx = # a, r < #r mx ⊦ #r mx[r, a]r = #r mx | An Axiom |
| scolsorted-samecount-above-clean0 | #r mx = #r mx0, #c mx = #c mx0, c < #c mx, scolsorted(mx, #c mx, mx0) ⊦ 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 |
| 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(mx, r, mx0) → 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 |
| divup-half | ⊦ (m /↑ 2^ n) /↑ 2 = m /↑ 2^(n + 1) | 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(mx, r, mx0) → perm(mx0.toArr, mx.toArr) | A User Theorem |
| sortcol | sortcol#(m; mx){choose a with # a = #r mx ∧ perm(mx[m]c, a) ∧ ordered≤(a) in mx[m]c := a} | An Axiom |
| 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 |
| scolsort-dirtyboundhalf | #r mx0 = #r mx, #c mx0 = #c mx, #c mx ≠ 0 ⊦ scolsorted(mx, #c mx, mx0) ∧ mx0.dirtyrows≤(bound) ∧ srowsorted(mx0, #r mx0, mx0) → mx.dirtyrows≤(bound /↑ 2) | 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 |
| sortrow-correct | mx = mx0, m < #r mx, rowsincreasing(mx, #r mx), ordered≤(toArr(mx, m)) ⊦ ⟪sortrow#(m, true; mx)⟫ (#r mx0 = #r mx ∧ #c mx = #c mx0 ∧ perm(mx0.toArr, mx.toArr) ∧ rowsincreasing(mx, #r mx) ∧ ordered≤(toArr(mx, m + 1))) | A User Theorem |
| scolsorted-count-below-clean0rows | #r mx = #r mx0, #c mx = #c mx0, c < #c mx, scolsorted(mx, #c mx, mx0) ⊦ count(mx[c]c, 0, #clean0rows(mx0, i), λ j. j < i) = #clean0rows(mx0, i) | 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), scolsorted(mx, #c mx, mx0), ∀ 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 |