[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 real-floor-ceil
Status:
Proved!
Axioms: 4, User Theorems: 35 (Proved: 35, Partially proved: 0, Unproved: 0, Invalid: 0, Siginvalid: 0)
Proof steps: 209, Interactions: 153
ceil-addint(12,11)
ceil-ls-add-one(0,0)
floor-gr-subone(0,0)
floor-ls-negint(6,5)
int-ls-ceil(2,0)
ls-ceille(2,1)
negint-le-floor(3,2)
ceil-ge(0,0)
ceil-ls-int(9,5)
floor-int(6,5)
floor-notls(3,2)
int-ls-floor(12,9)
ls-floorle(2,1)
negint-ls-ceil(2,1)
ceil-int(5,3)
ceil-ls-negint(3,2)
floor-le(0,0)
floor-triang(9,7)
le-ceille(8,6)
ls-floorsuc(3,1)
negint-ls-floor(3,2)
ceil-is-neg-floor-neg(24,22)
ceil-notls(2,1)
floor-le-int(11,8)
gr-ceilpred(3,1)
le-floorle(11,9)
ls-notceilgr(2,1)
ceil-le-int(9,5)
ceil-triang(9,8)
floor-le-negint(3,2)
int-le-ceil(2,0)
le-notceilgr(2,1)
ls-notfloorgr(2,1)
ceil-le-negint(2,1)
floor-addint(17,16)
floor-ls-int(5,4)
int-le-floor(10,7)
le-notfloorgr(2,1)
negint-le-ceil(3,2)