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: |
|---|---|---|
| invert-base | ⊦ bitsinvert([]) = [] | An Axiom |
| invert-zero | ⊦ bitsinvert(false ' + bits) = true + bitsinvert(bits) | An Axiom |
| invert-one | ⊦ bitsinvert(true ' + bits) = false + bitsinvert(bits) | An Axiom |
| succ-zero | ⊦ (bits + false ')+1 = bits + true | An Axiom |
| succ-rec | ⊦ (bits + true ')+1 = bits +1 + false | An Axiom |
| sgn-empty | ⊦ sgn([]) = [] | An Axiom |
| sgn-one | ⊦ sgn(boolvar ') = boolvar ' | An Axiom |
| sgn-base | ⊦ sgn(boolvar ' + (¬ boolvar)' + bits) = boolvar ' + (¬ boolvar)' + bits | An Axiom |
| sgn-rec | ⊦ sgn(boolvar ' + boolvar ' + bits) = sgn(boolvar ' + bits) | An Axiom |
| fillsgn-longer | ⊦ n ≤ # bits → fillsgn(n, bits) = bits | An Axiom |
| fillsgn-empty | ⊦ fillsgn(n, []) = mklist(false, n) | An Axiom |
| fillsgn-fill | ⊦ # bits < n → fillsgn(n, boolvar ' + bits) = mklist(boolvar, n - # bits) + bits | An Axiom |
| succ-empty | ⊦ [] +1 = true ' | An Axiom |
| fix-shorter | ⊦ ¬ n < # bits → fix(n, bits) = fillsgn(n, bits) | An Axiom |
| fix-longer | ⊦ n < # bits → fix(n, bits) = lastn(n, bits) | An Axiom |
| bitsinvert-size | ⊦ bits ≠ [] → # sgn(bitsinvert(bits)) = # sgn(bits) | A User Theorem |
| fill-empty | ⊦ fillsgn(n, bits) = [] ↔ bits = [] ∧ n = 0 | A User Theorem |
| fill-fill | ⊦ # bits ≤ n ∧ bits ≠ [] → fillsgn(n, bits) = mklist(bits.first, n - # bits) + bits | A User Theorem |
| fill-fill-01 | ⊦ bits ≠ [] → fillsgn(n, fillsgn(n, bits)) = fillsgn(n, bits) | A User Theorem |
| fill-first | ⊦ bits ≠ [] → (fillsgn(n, bits).first ↔ bits.first) | A User Theorem |
| fill-in | ⊦ bits ≠ [] → (boolvar ∈ fillsgn(n, bits) ↔ boolvar ∈ bits) | A User Theorem |
| fill-last | ⊦ n ≠ 0 ∧ bits ≠ [] → fillsgn(n, bits + boolvar ') = fillsgn(n -1, bits) + boolvar | A User Theorem |
| fill-lastn | ⊦ n < # bits → lastn(n, fillsgn(n, bits)) = lastn(n, bits) | A User Theorem |
| fill-lastn-01 | ⊦ n ≤ # bits → lastn(n, fillsgn(n, bits)) = lastn(n, bits) | A User Theorem |
| fill-lastn-02 | ⊦ bits ≠ [] → lastn(m, fillsgn(m + n, bits)) = lastn(m, fillsgn(m, bits)) | A User Theorem |
| fill-lastn-03 | ⊦ bits ≠ [] ∧ m ≤ n → lastn(m, fillsgn(n, bits)) = lastn(m, fillsgn(m, bits)) | A User Theorem |
| fill-lastn-04 | ⊦ m + 1 = n ∧ # bits0 < n → lastn(m, bits + fillsgn(n, bits0).rest) = fillsgn(n -1, bits0) | A User Theorem |
| fill-lastn-05 | ⊦ m + 1 = n ∧ # bits0 < n → lastn(m, fillsgn(n, bits0).rest) = fillsgn(n -1, bits0) | A User Theorem |
| fill-length | ⊦ # bits ≤ n → # fillsgn(n, bits) = n | A User Theorem |
| fill-mklist | ⊦ fillsgn(n, mklist(boolvar, n)) = mklist(boolvar, n) | A User Theorem |
| fill-nls | ⊦ ¬ # fillsgn(n, bits) < # bits | A User Theorem |
| fill-one | ⊦ fillsgn(1, boolvar ') = boolvar ' | A User Theorem |
| fill-one-01 | ⊦ fillsgn(n + 1, boolvar ') = mklist(boolvar, n + 1) | A User Theorem |
| fill-one-02 | ⊦ 0 < i → fillsgn(i→n(i), boolvar ') = mklist(boolvar, i→n(i)) | A User Theorem |
| fill-rec | ⊦ bits ≠ [] ∧ # bits < n → fillsgn(n, bits) = bits.first ' + fillsgn(n -1, bits) | A User Theorem |
| fill-rec-false | ⊦ bits ≠ [] ∧ ¬ bits.first ∧ # bits ≤ n → fillsgn(n + 1, bits) = false ' + fillsgn(n, bits) | A User Theorem |
| fill-rec-one | ⊦ 0 < n → fillsgn(n, boolvar ') = mklist(boolvar, n) | A User Theorem |
| fill-refill | ⊦ # bits ≤ n → fillsgn(n + 1, false ' + fillsgn(n, bits)).rest = fillsgn(n, bits) | A User Theorem |
| fill-sgn | ⊦ n = # bits → fillsgn(n, sgn(bits)) = bits | A User Theorem |
| fill-sgn-01 | ⊦ # bits ≤ n → fillsgn(n, sgn(bits)) = fillsgn(n, bits) | A User Theorem |
| fill-sgn-02 | ⊦ bits ≠ [] → fillsgn(# bits, sgn(bits)) = bits | A User Theorem |
| fill-sgn-03 | ⊦ bits ≠ [] ∧ # bits ≤ n + 1 → fillsgn(n + 1, sgn(bits.rest)).rest = fillsgn(n, bits.rest) | A User Theorem |
| fill-sgn-04 | ⊦ n = # bits ∧ bits ≠ [] → fillsgn(n, sgn(bits)) = bits | A User Theorem |
| fill-size | ⊦ fillsgn(# bits, bits) = bits | A User Theorem |
| fill-zero | ⊦ fillsgn(0, bits) = bits | A User Theorem |
| fix-empty | ⊦ fix(n, bits) = [] ↔ n = 0 | A User Theorem |
| fix-size | ⊦ # fix(n, bits) = n | A User Theorem |
| fix-zero | ⊦ fix(0, bits) = [] | A User Theorem |
| inv-append | ⊦ bitsinvert(bits + bits0) = bitsinvert(bits) + bitsinvert(bits0) | A User Theorem |
| inv-empty | ⊦ bitsinvert(bits) = [] ↔ bits = [] | A User Theorem |
| inv-false | ⊦ bitsinvert(false ') = true ' | A User Theorem |
| inv-false-01 | ⊦ bitsinvert(bits) = false ' ↔ bits = true ' | A User Theorem |
| inv-fill | ⊦ bits ≠ [] → bitsinvert(fillsgn(n, bits)) = fillsgn(n, bitsinvert(bits)) | A User Theorem |
| inv-first | ⊦ bitsinvert(bits) = false ' + bits0 ↔ bits = true ' + bitsinvert(bits0) | A User Theorem |
| inv-first-01 | ⊦ bitsinvert(bits) = true ' + bits0 ↔ bits = false ' + bitsinvert(bits0) | A User Theorem |
| inv-in | ⊦ boolvar ∈ bitsinvert(bits) ↔ (¬ boolvar) ∈ bits | A User Theorem |
| inv-in-01 | ⊦ false ∈ bitsinvert(bits) ↔ true ∈ bits | A User Theorem |
| inv-in-02 | ⊦ true ∈ bitsinvert(bits) ↔ false ∈ bits | A User Theorem |
| inv-intro | ⊦ bits = bits0 ↔ bitsinvert(bits) = bitsinvert(bits0) | A User Theorem |
| inv-inv | ⊦ bitsinvert(bitsinvert(bits)) = bits | A User Theorem |
| inv-last | ⊦ bitsinvert(bits + boolvar ') = bitsinvert(bits) + (¬ boolvar)' | A User Theorem |
| inv-last-01 | bits ≠ [] ⊦ ¬ false ∈ bits → ¬ bitsinvert(bits).last | A User Theorem |
| inv-last-02 | bits ≠ [] ⊦ ¬ true ∈ bits → bitsinvert(bits).last | A User Theorem |
| inv-last-03 | ⊦ bits ≠ [] → bitsinvert(bits) = bitsinvert(bits.butlast) + (¬ bits.last)' | A User Theorem |
| inv-len | ⊦ # bitsinvert(bits) = # bits | A User Theorem |
| inv-mklist | ⊦ bitsinvert(mklist(boolvar, n)) = mklist(¬ boolvar, n) | A User Theorem |
| inv-one | ⊦ bitsinvert(boolvar ') = (¬ boolvar)' | A User Theorem |
| inv-one-01 | ⊦ bitsinvert(true ') = false ' | A User Theorem |
| inv-rec | ⊦ bitsinvert(boolvar ' + bits) = (¬ boolvar)' + bitsinvert(bits) | A User Theorem |
| inv-rec-01 | ⊦ bits ≠ [] → bitsinvert(bits) = (¬ bits.first)' + bitsinvert(bits.rest) | A User Theorem |
| inv-rest | bits ≠ [] ⊦ bitsinvert(bits).rest = bitsinvert(bits.rest) | A User Theorem |
| inv-rew | ⊦ false ' + bitsinvert(bits) = bitsinvert(true ' + bits) | A User Theorem |
| inv-rew-01 | ⊦ true ' + bitsinvert(bits) = bitsinvert(false ' + bits) | A User Theorem |
| inv-sgn | ⊦ bitsinvert(sgn(bits)) = sgn(bitsinvert(bits)) | A User Theorem |
| inv-true-01 | ⊦ bitsinvert(bits) = true ' ↔ bits = false ' | A User Theorem |
| invert-rest | ⊦ bits ≠ [] → bitsinvert(bits.rest) = bitsinvert(bits).rest | A User Theorem |
| lastn-fill-sgn | ⊦ bits ≠ [] → lastn(n, fillsgn(n, sgn(bits))) = lastn(n, fillsgn(n, bits)) | A User Theorem |
| sgn-2pot | ⊦ sgn(true ' + mklist(false, n)) = true ' + mklist(false, n) | A User Theorem |
| sgn-append | ⊦ ¬ (¬ boolvar) ∈ bits → sgn(boolvar ' + bits + bits0) = sgn(boolvar ' + bits0) | A User Theorem |
| sgn-append-01 | ⊦ true ∈ bits ∧ false ∈ bits → sgn(bits + bits0) = sgn(bits) + bits0 | A User Theorem |
| sgn-append-02 | ⊦ true ∈ bits → sgn(bits + false ' + bits0) = sgn(bits) + false ' + bits0 | A User Theorem |
| sgn-append-03 | ⊦ ¬ boolvar ∈ bits ∧ bits ≠ [] → sgn(bits + bits0) = sgn((¬ boolvar)' + bits0) | A User Theorem |
| sgn-append-04 | ⊦ ¬ true ∈ bits ∧ bits ≠ [] → sgn(bits + bits0) = sgn(false ' + bits0) | A User Theorem |
| sgn-append-05 | ⊦ ¬ false ∈ bits ∧ bits ≠ [] → sgn(bits + bits0) = sgn(true ' + bits0) | A User Theorem |
| sgn-append-06 | ⊦ bits0 ≠ [] ∧ (¬ bits0.first) ∈ bits → sgn(bits + bits0) = sgn(bits) + bits0 | A User Theorem |
| sgn-base-01 | ⊦ sgn(true ' + false ' + bits) = true ' + false ' + bits | A User Theorem |
| sgn-base-02 | ⊦ sgn(false ' + true ' + bits) = false ' + true ' + bits | A User Theorem |
| sgn-base-03 | ⊦ bits ≠ [] ∧ (bits.first ↔ ¬ boolvar) → sgn(boolvar ' + bits) = boolvar ' + bits | A User Theorem |
| sgn-base-04 | ⊦ ¬ boolvar ∈ bits → sgn(boolvar ' + bits) = boolvar ' + bits | A User Theorem |
| sgn-base-05 | ⊦ (bits.first ↔ ¬ bits.rest.first) ∧ 1 < # bits → sgn(bits) = bits | A User Theorem |
| sgn-empty-01 | ⊦ sgn(bits) = [] ↔ bits = [] | A User Theorem |
| sgn-ex | ⊦ bits ≠ [] ↔ (∃ n. bits = mklist(bits.first, n) + sgn(bits) ∧ bits ≠ []) | A User Theorem |
| sgn-ex-01 | ⊦ true ∈ bits ∧ false ∈ bits → (∃ boolvar, n, boolvar0, bits0. bits = mklist(boolvar, n) + (boolvar0 + bits0) ∧ sgn(bits) = boolvar + boolvar0 + bits0 ∧ ¬(boolvar ↔ boolvar0) ∧ n ≠ 0) | A User Theorem |
| sgn-fill | ⊦ bits ≠ [] → sgn(fillsgn(n, bits)) = sgn(bits) | A User Theorem |
| sgn-first | ⊦ sgn(boolvar ' + bits).first ↔ boolvar | A User Theorem |
| sgn-first-01 | ⊦ bits ≠ [] → (sgn(bits).first ↔ bits.first) | A User Theorem |
| sgn-first-02 | ⊦ sgn(true ' + bits) ≠ false ' + bits0 | A User Theorem |
| sgn-first-03 | ⊦ sgn(false ' + bits) ≠ true ' + bits0 | A User Theorem |
| sgn-first-04 | ⊦ bits.first ∧ bits ≠ [] → sgn(bits) ≠ false ' + bits0 | A User Theorem |
| sgn-in | ¬ (¬ boolvar) ∈ bits ⊦ sgn(boolvar ' + bits) = boolvar ' | A User Theorem |
| sgn-in-01 | ⊦ bits ≠ [] → (boolvar ∈ sgn(bits) ↔ boolvar ∈ bits) | A User Theorem |
| sgn-in-02 | ⊦ boolvar ∈ sgn(boolvar0 ' + bits) ↔ boolvar ∈ boolvar0 ' + bits | A User Theorem |
| sgn-last | (¬ boolvar) ∈ bits ⊦ sgn(boolvar ' + bits + boolvar0 ') = sgn(boolvar ' + bits) + boolvar0 ' | A User Theorem |
| sgn-last-01 | boolvar ↔ ¬ boolvar0 ⊦ sgn(boolvar ' + bits + boolvar0 ') = sgn(boolvar ' + bits) + boolvar0 ' | A User Theorem |
| sgn-last-02 | bits.first ↔ ¬ boolvar0, bits ≠ [] ⊦ sgn(bits + boolvar0 ') = sgn(bits) + boolvar0 ' | A User Theorem |
| sgn-last-03 | (¬ bits.first) ∈ bits.rest, bits ≠ [] ⊦ sgn(bits + boolvar0 ') = sgn(bits) + boolvar0 ' | A User Theorem |
| sgn-last-04 | ⊦ (¬ boolvar) ∈ bits → sgn(bits + boolvar ') = sgn(bits) + boolvar ' | A User Theorem |
| sgn-last-both | ⊦ true ∈ bits ∧ false ∈ bits → sgn(bits + boolvar ') = sgn(bits) + boolvar ' | A User Theorem |
| sgn-last-diff | (¬ boolvar) ∈ bits ⊦ sgn(bits + boolvar ') = sgn(bits) + boolvar ' | A User Theorem |
| sgn-last-same | ¬ (¬ boolvar) ∈ bits ⊦ sgn(bits + boolvar ') = boolvar ' | A User Theorem |
| sgn-lastn | ⊦ n = # bits0 + 1 → lastn(n, sgn(bits + boolvar ') + bits0) = boolvar ' + bits0 | A User Theorem |
| sgn-lastn-01 | ⊦ n ≤ # sgn(bits) ∧ bits ≠ [] → lastn(n, sgn(bits)) = lastn(n, bits) | A User Theorem |
| sgn-length | ⊦ ¬ # bits < # sgn(bits) | A User Theorem |
| sgn-length-01 | ⊦ ¬ # sgn(bits) ≤ # bits ↔ false | A User Theorem |
| sgn-length-02 | ⊦ ¬ 2 + # bits ≤ # sgn(boolvar ' + bits) | A User Theorem |
| sgn-length-03 | ⊦ # bits ≤ n + 1 → ¬ 2 + n ≤ # sgn(bits) | A User Theorem |
| sgn-mklist | ⊦ sgn(mklist(boolvar, n) + sgn(boolvar ' + bits)) = sgn(boolvar ' + bits) | A User Theorem |
| sgn-mklist-01 | ⊦ sgn(false ' + mklist(false, n)) = false ' | A User Theorem |
| sgn-mklist-02 | ⊦ sgn(false ' + mklist(false, n) + bits) = sgn(false ' + bits) | A User Theorem |
| sgn-mklist-03 | ⊦ n ≠ 0 → sgn(mklist(boolvar, n)) = boolvar ' | A User Theorem |
| sgn-mklist-04 | ⊦ sgn(boolvar ' + mklist(boolvar, n) + bits0) = sgn(boolvar ' + bits0) | A User Theorem |
| sgn-mklist-05 | ⊦ 0 < i → sgn(mklist(boolvar, i→n(i))) = boolvar ' | A User Theorem |
| sgn-negint | ⊦ true ∈ bits → sgn(bitsinvert(false ' + true ' + bits) +1) = true ' + false ' + bitsinvert(bits) +1 | A User Theorem |
| sgn-nls | ⊦ # bits ≤ n → ¬ n < # sgn(bits) | A User Theorem |
| sgn-not-empty | ⊦ bits ≠ [] → sgn(bits) ≠ [] | A User Theorem |
| sgn-not-empty-01 | ⊦ sgn(boolvar ' + bits) ≠ [] | A User Theorem |
| sgn-notsame | ⊦ sgn(bits) ≠ boolvar ' + boolvar ' | A User Theorem |
| sgn-notsame-01 | ⊦ sgn(bits) ≠ boolvar ' + boolvar ' + bits0 | A User Theorem |
| sgn-one-01 | ⊦ bits ≠ [] → (sgn(bits) = boolvar ' ↔ ¬ (¬ boolvar) ∈ bits) | A User Theorem |
| sgn-rec-01 | bits ≠ [], bits.first ↔ boolvar ⊦ sgn(boolvar ' + bits) = sgn(bits) | A User Theorem |
| sgn-rec-01-01 | boolvar ↔ boolvar0 ⊦ sgn(boolvar ' + boolvar0 ' + bits) = sgn(boolvar0 ' + bits) | A User Theorem |
| sgn-sgn | ⊦ sgn(sgn(bits)) = sgn(bits) | A User Theorem |
| sgn-sgn-01 | ⊦ sgn(sgn(bits) + bits0) = sgn(bits + bits0) | A User Theorem |
| sgn-true | ⊦ ¬ false ∈ bits ∧ bits ≠ [] → sgn(bits) = true ' | A User Theorem |
| sgn-true-mklist | ⊦ 0 < i → sgn(true ' + mklist(false, i→n(i)) + bits) = true ' + mklist(false, i→n(i)) + bits | A User Theorem |
| sgn-two | ⊦ sgn(false ' + false ') = false ' | A User Theorem |
| sgn-two-01 | ⊦ sgn(true ' + true ') = true ' | A User Theorem |
| sgn-two-02 | ⊦ sgn(false ' + true ') = false ' + true ' | A User Theorem |
| sgn-two-03 | ⊦ sgn(true ' + false ') = true ' + false ' | A User Theorem |
| sgn-zero | ⊦ ¬ true ∈ bits ∧ bits ≠ [] → sgn(bits) = false ' | A User Theorem |
| sgn-zeros | ⊦ ¬ true ∈ bits → sgn(bits + false ' + bits0) = sgn(false ' + bits0) | A User Theorem |
| succ-01 | ⊦ (false ' + true ')+1 = true ' + false ' | A User Theorem |
| succ-empty-01 | ⊦ ¬ bits +1 ≠ [] ↔ false | A User Theorem |
| succ-ex | ⊦ false ∈ bits ↔ (∃ bits0, bits1. bits +1 = bits0 + true ' + bitsinvert(bits1) ∧ bits = bits0 + false ' + bits1 ∧ ¬ false ∈ bits1) | A User Theorem |
| succ-exinv | ⊦ true ∈ bits ↔ (∃ bits0, bits1. bitsinvert(bits) +1 = bitsinvert(bits0) + true ' + bits1 ∧ ¬ true ∈ bits1 ∧ bits = bits0 + true ' + bits1) | A User Theorem |
| succ-false | ⊦ bits +1 ≠ false ' | A User Theorem |
| succ-falsein | ⊦ bits ≠ [] → false ∈ (false ' + bits)+1 | A User Theorem |
| succ-falsein-01 | ⊦ bits ≠ [] → false ∈ (false ' + bitsinvert(bits))+1 | A User Theorem |
| succ-falsein-02 | ⊦ bits ≠ [] → (false ∈ bits +1 ↔ ¬(¬ bits.last ∧ ¬ false ∈ bits.butlast)) | A User Theorem |
| succ-fill | ⊦ false ∈ bits.rest ∧ bits ≠ [] → fillsgn(n, bits) +1 = fillsgn(n, bits +1) | A User Theorem |
| succ-first | ⊦ false ∈ bits.rest ∧ bits ≠ [] → (bits +1.first ↔ bits.first) | A User Theorem |
| succ-first-01 | ⊦ true ∈ bits +1.rest ∧ bits ≠ [] → (bits +1.first ↔ bits.first) | A User Theorem |
| succ-inv2x | ⊦ true ∈ bits → bitsinvert(bitsinvert(bits) +1) +1 = bits | A User Theorem |
| succ-len | ⊦ false ∈ bits → # bits +1 = # bits | A User Theorem |
| succ-length | ⊦ ¬ # bits + 1 < # bitsinvert(bits) +1 | A User Theorem |
| succ-length-01 | ⊦ ¬ # bits + 1 < # bits +1 | A User Theorem |
| succ-mklist | ⊦ (false ' + mklist(true, n))+1 = true ' + mklist(false, n) | A User Theorem |
| succ-mklist-01 | ⊦ mklist(true, n) +1 = true ' + mklist(false, n) | A User Theorem |
| succ-one | ⊦ false ' +1 = true ' | A User Theorem |
| succ-one-01 | ⊦ bits = true ' → bits +1 = true + false | A User Theorem |
| succ-ones | ⊦ ¬ false ∈ bits → bits +1 = true + bitsinvert(bits) | A User Theorem |
| succ-prefix | ⊦ (bits + false ' + bits0)+1 = bits + (false ' + bits0)+1 | A User Theorem |
| succ-rec-01 | ⊦ boolvar → (bits + boolvar ')+1 = bits +1 + false | A User Theorem |
| succ-rec-02 | ⊦ 0 ≠ # bits ∧ bits.last → bits +1 = bits.butlast +1 + false ' | A User Theorem |
| succ-rest | ⊦ false ∈ bits.rest ∧ bits ≠ [] → bits.rest +1 = bits +1.rest | A User Theorem |
| succ-succ | ⊦ (false ' + bitsinvert((false ' + bitsinvert(bits))+1))+1 = false ' + true ' + bits | A User Theorem |
| succ-true | ⊦ bits +1 = true ' ↔ bits = false ' ∨ bits = [] | A User Theorem |
| succ-truein | ⊦ true ∈ (false ' + true ' + bits)+1 | A User Theorem |
| succ-truein-01 | ⊦ ¬ true ∈ bits +1 ↔ false | A User Theorem |
| succ-zero-01 | ⊦ false ∈ bits0 → (bits + bits0)+1 = bits + bits0 +1 | A User Theorem |
| succ-zero-02 | ⊦ true ∈ bits0 → (bits + bitsinvert(bits0))+1 = bits + bitsinvert(bits0) +1 | A User Theorem |
| succ-zero-03 | ⊦ bits ≠ [] ∧ ¬ bits.last → bits +1 = bits.butlast + true | A User Theorem |
| succ-zeros | ⊦ ¬ true ∈ bits0 → (bits + bitsinvert(bits0))+1 = bits +1 + bits0 | A User Theorem |
| succ-zeros-01 | ⊦ ¬ false ∈ bits0 → (bits + bits0)+1 = bits +1 + bitsinvert(bits0) | A User Theorem |
| succ-zeros-02 | ⊦ n ≠ 0 → mklist(false, n) +1 = mklist(false, n -1) + true ' | A User Theorem |
| succ-zeros-03 | ⊦ (false ' + mklist(false, n))+1 = mklist(false, n) + true ' | A User Theorem |