[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 int-div

Div-def(0,0)div-elim-pospos(2,0)div-mult-nls-est-01(4,2)div-zero-05(2,1)ls(6,2)mod-ls-same(4,2)mod-pred-neg(12,4)modby6-help(24,13)modmod-mult-08(1,0)one-02(1,0)
Div-left(0,0)div-elim1(2,1)div-mult-nls-zero(2,1)div-zero-06(1,0)ls-01(7,2)mod-ls-same-01(21,10)mod-pred-neg-01(8,2)modeq-neg(6,2)modmod-mult-09(5,4)one-03(1,0)
Div-right(0,0)div-elim2(4,2)div-mult-num(3,1)div-zero-ngr(2,0)ls-02(10,4)mod-ls-same-02(20,7)mod-rec(8,2)modeq-neg-02(14,8)modmod-pos(16,7)one-04(1,0)
Mod-def(0,0)div-elim3(2,1)div-mult-num-01(2,0)div-zero-ngr-01(2,1)ls-03(1,1)mod-ls-zero(3,1)mod-rec-01(7,3)modeq-pos(4,2)modnum-neg(2,0)one-05(1,0)
abs(8,3)div-eq-same(10,5)div-mult-pos(1,0)div-zero-nls(2,1)ls-even(1,0)mod-lsz(4,1)mod-rew(1,0)modeq-pos-01(1,1)modnum-neg-01(2,0)one-06(1,0)
abs-01(1,0)div-eq-same-01(20,8)div-mult-pos-01(2,1)div-zero-nls-01(2,1)ls-even-01(27,16)mod-lsz-01(2,1)mod-same(2,1)modeq-pos-02(4,2)mult(1,0)one-lez(1,0)
abs-02(1,0)div-eq-zero(6,2)div-mult-pos-02(1,0)div2-add-neg(12,5)ls-same-pos(2,1)mod-mod-less(2,1)mod-shift(6,3)modeq-pos-03(5,2)mult-01(1,1)one-neg(11,5)
abs-03(1,0)div-eq-zero-01(29,14)div-mult-pos-03(1,0)div2-neg(1,0)ls-same-pos-01(2,1)mod-mult(1,1)mod-sub(3,3)modeq-pos-04(2,1)mult-02(8,4)one-pos(2,1)
abs-div10-le(2,1)div-est-denom-pos(6,2)div-mult-pos-rew(1,0)div2-neg-01(2,1)ls-same-pos-02(2,1)mod-mult-01(1,0)mod-sub-01(3,3)modeven-neg(7,4)mult-03(5,4)pdiv-ls(2,1)
abs-intro(2,1)div-est-nle-pos(4,1)div-mult-rew(1,0)div2-neg-odd(3,2)ls-succ(2,1)mod-mult-02(2,1)mod-sub-02(3,2)modeven-neg-01(2,1)mult-04(1,0)pos(1,0)
abs-shift(14,7)div-est-nls(6,1)div-mult-rew-01(1,0)div2-nle(1,0)lsf(2,1)mod-mult-03(1,0)mod-succ(1,0)modeven-pos(2,1)mult-05(2,1)prod-div-less(10,6)
abs-shift-01(6,3)div-est-num(12,4)div-mult-shift-holds(7,4)div2-nle-01(1,0)lsf-01(2,1)mod-mult-04(2,1)mod-succ-01(6,2)modex(10,6)mult-div-switch(1,0)prod-div-less-01(1,0)
add-div-mult(13,9)div-le-modnotzero(9,4)div-mult-three(1,0)div2-nle-02(8,4)lsf-02(2,1)mod-mult-neg(4,4)mod-succ-02(2,0)modex-odd(4,2)mult-ls(10,3)quad-div-less(1,0)
div-abs(2,1)div-le-modnotzero-01(3,2)div-mult-three-nls(17,14)div2-nls(17,9)lsfc(1,1)mod-mult-neg-01(3,3)mod-three(1,0)modex-odd-neg(9,5)mult-ls-01(10,3)square-even(2,1)
div-add-both(6,3)div-le-modzero(5,3)div-mult-two-nls(1,0)div2-nls-01(2,1)lsfc-01(2,1)mod-mult-neg-02(6,2)mod-two(1,0)modex-odd-neg-01(9,4)mult-split-mod(6,3)square-even-01(1,1)
div-add-neg(7,2)div-le-modzero-01(3,2)div-mult-two-nls-01(13,9)div2-nls-02(17,9)lsfc-02(2,1)mod-mult-neg-03(1,0)mod-two-01(1,0)modmod(1,1)mult-split-mod-02(1,0)square-even-02(3,3)
div-add-nosucc(9,3)div-le-pos(16,6)div-nearer-zero(20,13)div2-nls-03(2,1)lstwozero(1,0)mod-mult-pos(5,3)mod-two-02(1,0)modmod-add(10,3)neg(1,0)square-inject(17,10)
div-add-nosucc-neg(5,4)div-le-same(2,1)div-ngr-zero(4,1)div2-notzero(4,1)minus-add(3,2)mod-mult-pos-01(4,1)mod-two-03(2,1)modmod-add-01(4,2)neg-01(1,0)square-interval(12,10)
div-add-pos(7,2)div-le-same-neg(7,2)div-nle(1,0)div2-odd(1,0)mod-abs(2,1)mod-mult-pos-02(1,0)mod-two-04(1,0)modmod-add-02(2,1)neqf(1,0)square-ls(2,1)
div-add-rew(1,0)div-lezero(8,2)div-nls(1,0)div2-odd-01(4,3)mod-abs-intro(2,1)mod-neg(2,1)mod-two-05(1,0)modmod-add-03(4,2)nls-mult-div(8,5)square-ls-01(4,3)
div-add-succ(12,8)div-ls(8,4)div-nls-01(3,2)div2-one(1,0)mod-add(2,1)mod-neg-01(2,1)mod-two-06(2,1)modmod-add-04(11,4)num-ls(5,1)square-ls-02(5,5)
div-add-succ-neg(5,4)div-ls-01(1,1)div-rec(8,2)div2-zero(4,3)mod-add-01(8,3)mod-neq(10,5)mod-two-pred(1,0)modmod-add-case(18,9)num-neg(2,0)square-nle(16,10)
div-add1-negneg(1,0)div-ls-02(2,1)div-rec-01(5,3)div2one(2,1)mod-add-both-zero(4,2)mod-neq-01(4,3)mod-two-pred-01(4,2)modmod-add-if(18,2)num-neg-01(2,0)square-nle-01(2,1)
div-add1-negpos-neg(1,0)div-ls-modnotzero(3,2)div-same(4,2)div2one-01(4,2)mod-add-neg(7,2)mod-neq-02(1,0)mod-two-pred-02(4,3)modmod-add-if3(19,1)nummult-eq(2,0)square-nle-02(3,2)
div-add1-negpos-neg-01(15,6)div-ls-modzero(2,1)div-shift-two(13,7)div2zero(1,0)mod-add-pos(7,2)mod-next-square(13,8)mod-twoeven(2,1)modmod-add-law(3,3)nummult-eq-01(3,1)square-nls(12,8)
div-add1-negpos-neg-02(2,2)div-ls-mone(22,12)div-sub(3,2)div53(1,0)mod-add-zero(14,9)mod-ngez(1,0)mod-twoodd(3,2)modmod-add-law-pos(19,16)nummult-le(9,3)square-nls-01(3,2)
div-add1-negpos-pos(4,0)div-ls-pos-better(1,1)div-sub-01(4,2)diveq-neg(4,2)mod-add1-negneg(1,0)mod-ngez-01(1,0)mod-twoodd-01(3,2)modmod-add-zero(18,11)nummult-le-01(14,7)square-nls-02(2,1)
div-add1-posneg-neg(10,3)div-ls-pos-mon(2,1)div-sum-ls(11,9)diveq-pos(6,3)mod-add1-negpos-neg(15,6)mod-ngr(1,0)mod-twoodd-02(2,1)modmod-add2-negpos-neg(6,4)nummult-le-01-01(2,1)sub-ls(1,0)
div-add1-posneg-pos(1,0)div-ls-same(17,7)div-sum-ls-01(1,1)divmod-rew(2,1)mod-add1-negpos-pos(4,0)mod-nle(2,0)mod-twoodd-03(5,4)modmod-add2-negpos-pos(2,1)nummult-le-02(12,4)sub-ls-01(2,0)
div-add1-posneg-pos-01(15,6)div-ls-zero(9,4)div-two(1,0)divmult(2,1)mod-add1-posneg-neg(8,2)mod-nle-01(1,0)mod-zero(1,0)modmod-add2-negpos-pos-01(6,4)nummult-le-02-01(2,1)three(1,0)
div-add1-posneg-pos-02(5,3)div-minus-onediff(10,5)div-two-01(1,0)estimate-01(8,5)mod-add1-posneg-pos(13,5)mod-nle-02(3,1)mod-zero-01(4,2)modmod-add2-negpos-pos-02(1,0)nummult-le-03(9,3)two-add-square(1,1)
div-add1-pospos(1,0)div-minus-onediff-01(17,8)div-two-intro(25,14)even-add(34,17)mod-add1-pospos(1,0)mod-nls(1,0)mod-zero-02(1,0)modmod-add2-posneg-neg(6,4)nummult-le-03-01(2,1)two-add-square-01(1,1)
div-addthree-rew(13,5)div-minus255-256(2,1)div-two-zero(1,0)even-mult(13,9)mod-by6(16,8)mod-nls-01(2,1)mod-zero-03(1,0)modmod-add2-posneg-neg-01(6,4)nummult-le-04(2,1)two-even(1,0)
div-am-rew(6,3)div-minus255-256-01(2,1)div-two-zero-01(2,1)even-not(4,2)mod-div-ls(13,10)mod-nls-02(3,2)mod-zero-04(2,1)modmod-add2-posneg-neg-02(1,0)nummult-ls(19,6)two-mult(1,1)
div-div(17,9)div-mone(1,0)div-twoodd(1,0)even-not-ex(6,4)mod-div-zero(11,5)mod-nls-03(1,0)mod-zero-05(4,1)modmod-add2-posneg-pos(6,3)nummult-ls-01(5,1)two-mult-01(1,0)
div-div-intro(1,0)div-mone-01(1,0)div-twoodd-01(3,3)even-or-succ-even(2,1)mod-four(1,1)mod-nls-04(13,8)mod-zero-06(6,2)modmod-law-mult(2,1)nummult-ls-01-01(2,1)two-odd(2,1)
div-div-num(2,0)div-mult(1,0)div-twoodd-02(5,5)exeven(3,2)mod-gez(2,1)mod-nls-05(2,1)mod-zero-07(3,0)modmod-ma(8,4)nummult-ls-02(5,2)zero(3,2)
div-div-pos(2,0)div-mult-01(25,15)div-twoodd-03(4,4)exodd(2,1)mod-grz(2,0)mod-nls-06(6,4)mod-zero-08(2,0)modmod-ma-01(3,2)nummult-ls-02-01(2,1)zero-01(1,0)
div-div-pred(23,11)div-mult-02(5,3)div-twoodd-04(4,4)is-div(2,1)mod-grz-01(4,1)mod-not-less(2,0)mod-zero-09(2,1)modmod-ma-negpos-neg(7,5)nummult-ls-03(17,8)zero-02(2,1)
div-div-pred-01(30,16)div-mult-03(2,1)div-twoodd-05(5,4)le-abs-numerator(27,15)mod-grz-02(2,0)mod-one(1,1)mod-zero-ls(2,1)modmod-mult(5,3)nummult-ls-03-01(2,1)zero-03(2,1)
div-div-switch(2,1)div-mult-le(1,0)div-twoodd-06(2,1)le-norest(4,2)mod-le(1,0)mod-one-01(1,0)mod-zero-num(3,1)modmod-mult-01(4,2)nummult-ls-04(2,1)zero-04(10,2)
div-elim(2,1)div-mult-le-01(2,0)div-twoodd-07(9,8)leone-two(10,5)mod-le-01(1,0)mod-pos-not-neg(1,0)mod-zero-one(17,11)modmod-mult-02(11,6)nummult-modle(3,0)zero-05(4,2)
div-elim-divides(1,0)div-mult-ls(6,3)div-zero(1,0)less-mult-div(1,0)mod-le-num(3,1)mod-pred(2,0)mod2-add-neg(10,5)modmod-mult-03(10,5)nummult-modle-01(3,1)zero-06(2,0)
div-elim-negneg(6,2)div-mult-ls-pos(1,0)div-zero-01(2,0)less-mult-div-01(15,8)mod-les(4,1)mod-pred-01(2,0)mod2-neg-odd(2,1)modmod-mult-04(6,3)nummult-modls(3,0)zero-07(2,1)
div-elim-negpos(2,0)div-mult-neg(5,4)div-zero-02(7,4)less-mult-div-02(1,0)mod-less(1,0)mod-pred-02(12,4)mod256(1,0)modmod-mult-05(3,2)nummult-modls-01(3,1)
div-elim-pos(4,2)div-mult-nle-est(4,2)div-zero-03(2,0)letwo(1,0)mod-less-01(1,0)mod-pred-03(4,1)mod53(1,0)modmod-mult-06(1,0)one(3,2)
div-elim-posneg(4,1)div-mult-nls-est(4,2)div-zero-04(2,0)letwozero(2,2)mod-lezero(4,1)mod-pred-04(2,0)mod62(1,0)modmod-mult-07(18,14)one-01(2,1)