[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 align
Status:
Proved!
Axioms: 3, User Theorems: 77 (Proved: 77, Partially proved: 0, Unproved: 0, Invalid: 0, Siginvalid: 0)
Proof steps: 377, Interactions: 89
add-n-aligndown(5,1)
aligndown-add-same(7,3)
aligndown-is-smaller(3,0)
aligndown-same-equiv(3,1)
alignup-is-aligned(3,0)
alignup-same0(2,0)
is-aligned-align-down(3,1)
is-aligned-ls-eq-zero(2,0)
is-aligned-pad(3,1)
align-down-add-eq(5,2)
aligndown-add-same0(7,2)
aligndown-is-smaller-01(3,0)
aligndown-same0(2,0)
alignup-is-bigger(5,1)
alignup-upper-bound(5,1)
is-aligned-align-up-multiple(4,1)
is-aligned-minus(3,0)
is-aligned-same(2,0)
align-down-add-eq-add-ls(4,2)
aligndown-aligndown-add(11,1)
aligndown-is-zero(7,2)
aligndown-sub-add-sub(9,1)
alignup-is-even-bigger(2,1)
alignup-upper-bound-01(3,1)
is-aligned-aligndown-zero(2,0)
is-aligned-mod(2,0)
is-aligned-simp(2,0)
align-down-add-ls(19,9)
aligndown-def(0,0)
aligndown-le(3,1)
alignup-add-bounded1(8,1)
alignup-isnot-smaller(2,1)
between-is-aligned(3,1)
is-aligned-aligndown-zero-ls(2,0)
is-aligned-mod-alignment(5,2)
is-aligned-still-space(14,7)
align-down-add-to-align-up(2,0)
aligndown-eq-add(3,1)
aligndown-multiplier(2,0)
alignup-add-le(5,2)
alignup-le(15,3)
div-mult-to-diff-mod(5,1)
is-aligned-def(0,0)
is-aligned-multiple(7,1)
is-aligned-zero(2,0)
align-down-ls-zero(2,0)
aligndown-is-aligned(3,0)
aligndown-not-smaller(3,0)
alignup-add-mult(3,0)
alignup-le-is-aligned(17,3)
eq1(15,6)
is-aligned-elim(3,1)
is-aligned-multiple-1(3,1)
not-mod0-not-aligned(2,0)
aligndown-add-n(5,1)
aligndown-is-aligned-add(5,1)
aligndown-plus-remainder(5,1)
alignup-calc(3,1)
alignup-lower-bound(5,1)
is-aligned-add(2,0)
is-aligned-intro(2,0)
is-aligned-multiplier(2,0)
rounded-help(11,3)
aligndown-add-n-alignup(2,0)
aligndown-is-aligned0(2,0)
aligndown-remainder(12,2)
alignup-def(0,0)
alignup-multiplier(2,0)
is-aligned-add-diff-le(3,0)
is-aligned-is-aligned-mod(9,4)
is-aligned-not-multiples(3,1)
rounded-help2(7,3)
aligndown-add-not-smaller(10,2)
aligndown-is-n(13,3)
aligndown-same(2,0)
alignup-div-mult(3,0)
alignup-same(2,0)
is-aligned-add-diff-ls(2,0)
is-aligned-le-eq-zero(2,0)
is-aligned-of-mod(6,3)