[Imprint][Data Privacy Statement][E-Mail]
Back to main index.
View the specification.
View theorem base summary,
View theorem base listing,
the used properties by spec,
the dependency list,
the symbol table,
Theorem base summary for Specification bitopsaux
- Status: Proved!
- Axioms: 15,
User Theorems: 161
(Proved: 161,
Partially proved: 0,
Unproved: 0,
Invalid: 0,
Siginvalid: 0)
- Proof steps: 932,
Interactions: 346
| bitsinvert-size(24,6) | fill-one-02(4,1) | fix-size(1,1) | inv-len(1,0) | sgn-append-01(15,7) | sgn-first-01(2,0) | sgn-length-01(1,0) | sgn-rec-01(2,0) | succ-falsein(6,3) | succ-rec-02(2,1) |
| fill-empty(4,2) | fill-rec(8,1) | fix-zero(3,2) | inv-mklist(7,0) | sgn-append-02(14,6) | sgn-first-02(3,2) | sgn-length-02(14,5) | sgn-rec-01-01(1,0) | succ-falsein-01(2,1) | succ-rest(2,0) |
| fill-fill(6,1) | fill-rec-false(6,1) | inv-append(3,0) | inv-one(5,3) | sgn-append-03(20,7) | sgn-first-03(3,2) | sgn-length-03(2,1) | sgn-sgn(7,3) | succ-falsein-02(2,1) | succ-succ(7,3) |
| fill-fill-01(4,2) | fill-rec-one(4,1) | inv-empty(2,0) | inv-one-01(1,0) | sgn-append-04(2,1) | sgn-first-04(2,0) | sgn-mklist(7,5) | sgn-sgn-01(11,3) | succ-fill(12,4) | succ-true(6,3) |
| fill-first(8,2) | fill-refill(2,1) | inv-false(1,0) | inv-rec(1,0) | sgn-append-05(2,1) | sgn-in(8,2) | sgn-mklist-01(1,0) | sgn-true(6,3) | succ-first(2,0) | succ-truein(1,0) |
| fill-in(4,2) | fill-sgn(13,6) | inv-false-01(2,0) | inv-rec-01(2,0) | sgn-append-06(9,4) | sgn-in-01(12,4) | sgn-mklist-02(3,0) | sgn-true-mklist(6,3) | succ-first-01(9,3) | succ-truein-01(8,3) |
| fill-last(20,7) | fill-sgn-01(31,17) | inv-fill(11,4) | inv-rest(2,0) | sgn-base(0,0) | sgn-in-02(1,1) | sgn-mklist-03(10,2) | sgn-two(1,1) | succ-inv2x(2,1) | succ-zero(0,0) |
| fill-lastn(2,1) | fill-sgn-02(16,6) | inv-first(2,1) | inv-rew(1,0) | sgn-base-01(1,1) | sgn-last(7,2) | sgn-mklist-04(1,1) | sgn-two-01(1,1) | succ-len(2,1) | succ-zero-01(7,3) |
| fill-lastn-01(1,0) | fill-sgn-03(6,1) | inv-first-01(2,1) | inv-rew-01(1,0) | sgn-base-02(1,1) | sgn-last-01(8,4) | sgn-mklist-05(1,1) | sgn-two-02(1,1) | succ-length(2,1) | succ-zero-02(2,1) |
| fill-lastn-02(2,1) | fill-sgn-04(1,0) | inv-in(7,2) | inv-sgn(9,3) | sgn-base-03(2,0) | sgn-last-02(4,1) | sgn-negint(1,0) | sgn-two-03(1,1) | succ-length-01(2,1) | succ-zero-03(2,1) |
| fill-lastn-03(25,11) | fill-size(1,1) | inv-in-01(1,0) | inv-true-01(2,0) | sgn-base-04(6,2) | sgn-last-03(4,1) | sgn-nls(2,1) | sgn-zero(6,2) | succ-mklist(1,1) | succ-zeros(2,1) |
| fill-lastn-04(9,5) | fill-zero(1,1) | inv-in-02(1,0) | invert-base(0,0) | sgn-base-05(6,1) | sgn-last-04(38,12) | sgn-not-empty(8,3) | sgn-zeros(10,2) | succ-mklist-01(1,1) | succ-zeros-01(6,3) |
| fill-lastn-05(4,2) | fillsgn-empty(0,0) | inv-intro(3,2) | invert-one(0,0) | sgn-empty(0,0) | sgn-last-both(2,1) | sgn-not-empty-01(6,2) | succ-01(1,0) | succ-one(1,1) | succ-zeros-02(2,2) |
| fill-length(2,0) | fillsgn-fill(0,0) | inv-inv(1,0) | invert-rest(1,0) | sgn-empty-01(1,0) | sgn-last-diff(15,7) | sgn-notsame(10,3) | succ-empty(0,0) | succ-one-01(2,1) | succ-zeros-03(2,2) |
| fill-mklist(1,1) | fillsgn-longer(0,0) | inv-last(1,0) | invert-zero(0,0) | sgn-ex(12,5) | sgn-last-same(14,7) | sgn-notsame-01(10,3) | succ-empty-01(6,3) | succ-ones(6,3) |
| fill-nls(4,2) | fix-empty(2,1) | inv-last-01(8,0) | lastn-fill-sgn(31,13) | sgn-ex-01(32,12) | sgn-lastn(8,5) | sgn-one(0,0) | succ-ex(4,1) | succ-prefix(6,3) |
| fill-one(1,1) | fix-longer(0,0) | inv-last-02(8,0) | sgn-2pot(3,1) | sgn-fill(8,2) | sgn-lastn-01(16,5) | sgn-one-01(28,9) | succ-exinv(4,1) | succ-rec(0,0) |
| fill-one-01(2,1) | fix-shorter(0,0) | inv-last-03(2,0) | sgn-append(8,2) | sgn-first(7,4) | sgn-length(8,3) | sgn-rec(0,0) | succ-false(6,3) | succ-rec-01(1,0) |