[Imprint]
[Data Privacy Statement]
[E-Mail]
View
long theorem info
. View
the proof
. 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 alignup-def
0 ≠ m ⊦ align↑(n, m) = (n % m = 0 ⊃ n;(n / m)+1 * m)
Type: An axiom
Validity: The proof is valid.
Features: ls, smt,
Comment:
Used by:
align-down-add-to-align-up
,
aligndown-add-n-alignup
,
alignup-add-bounded1
,
alignup-add-le
,
alignup-add-mult
,
alignup-calc
,
alignup-div-mult
,
alignup-is-aligned
,
alignup-is-bigger
,
alignup-is-even-bigger
,
alignup-isnot-smaller
,
alignup-le
,
alignup-le-is-aligned
,
alignup-lower-bound
,
alignup-multiplier
,
alignup-same
,
alignup-same0
,
alignup-upper-bound
,
alignup-upper-bound-01
,
is-aligned-align-up-multiple
,
Used by units in proved state:
Proof exists?: No