[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 decimal
Status:
Proved!
Axioms: 15, User Theorems: 45 (Proved: 45, Partially proved: 0, Unproved: 0, Invalid: 0, Siginvalid: 0)
Proof steps: 451, Interactions: 252
Equality(0,0)
ex-mkDecimal(3,1)
inc-def(0,0)
maxScale-not-negt(5,3)
maxScale-zero-01(8,6)
mkDecimal-maxScale-nle-scale(9,5)
scale-base(0,0)
test-inc-01(8,5)
dec2int-def(0,0)
gen(0,0)
intvalue-base(0,0)
maxScale-pot10(9,5)
mkDecimal-constructor(1,1)
mkDecimal-negated(9,5)
scale-le(8,4)
test-truncate-01(7,4)
dec2int-def-any(15,8)
getint-neg(11,6)
intvalue-mod-10(12,7)
maxScale-pot10-01(12,6)
mkDecimal-enlarge(13,7)
mkDecimal-rec(5,3)
scale-negate(10,6)
truncate-nothing-def(0,0)
dec2int-zero(4,3)
getint-neg-01(2,1)
intvalue-rec(0,0)
maxScale-pot10-02(7,4)
mkDecimal-maxScale-le(8,5)
mkDecimal-reduce-int(19,10)
scale-neq(2,1)
truncate-really-def(0,0)
dec2int-zero-01(1,1)
getint-neg-02(9,5)
intvalue-zero(1,1)
maxScale-pot10-add(21,13)
mkDecimal-maxScale-le-int(18,10)
mkDecimal-reduce-scale(9,5)
scale-neq-01(2,1)
eq-same(36,17)
getint-pos(7,4)
maxScale-base(0,0)
maxScale-pot10-nls(8,4)
mkDecimal-maxScale-le-scale(9,5)
mkDecimal-scale-not-neg(16,9)
scale-not-neg(9,5)
eq-zero(1,1)
getint-pos-01(1,1)
maxScale-le-zero(1,0)
maxScale-rec(0,0)
mkDecimal-maxScale-nle(9,5)
mkDecimal-selectors(19,11)
scale-rec(0,0)
equality-any(63,34)
getint-zero(9,5)
maxScale-min(1,1)
maxScale-zero(0,0)
mkDecimal-maxScale-nle-int(13,7)
mkDecimal-zero(1,1)
scale-zero(0,0)