[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,

Used simplifier rules/spec theorems by specification

Used from specification int-mult

int-mult/dist-lsplit is used by i2np,
int-mult/succ-lsplit is used by i2np,
int-mult/associativity is used by zero-13, zero-02, zero-01, qzero-02, qzero-01, qzero, natpos, n2i-mult, mult-ls-05, mult-ls-04, i2np, i2n-mod, i2n-divtwo, i2n,
int-mult/commutativity is used by zero-13, zero-02, zero-01, qzero-02, qzero-01, qzero, natpos, n2i-mult, mult-ls-05, mult-ls-04, i2np, i2n-mod, i2n-divtwo, i2n,
int-mult/dist-rmerge is used by i2n-divtwo,
int-mult/eq-dist is used by n2i-mult,
int-mult/eq-one-neg is used by i2n-divtwo,
int-mult/eq-pos is used by i2n-divtwo,
int-mult/ls-forward is used by zero-13,
int-mult/ls-pos is used by zero-13,
int-mult/minus-left is used by i2n,
int-mult/odd-even is used by i2n-divtwo,
int-mult/one is used by n2i-mult, i2np,
int-mult/succ-rmerge is used by mult-ls-05, mult-ls-04,
int-mult/two-zero is used by i2n-divtwo,
int-mult/zero-ge is used by natpos, i2n-mod, i2n-divtwo,
int-mult/zero-ge-02 is used by i2np,
int-mult/zero-ge-add is used by natpos, i2n-mod,
int-mult/zero-gr-01 is used by zero-01, qzero-02, qzero-01, qzero,
int-mult/zero-left is used by zero-02, n2i-mult, i2np,
int-mult/zero-ls is used by i2n-divtwo,
int-mult/zero-ls-01 is used by zero-02,
int-mult/zero-ls-02 is used by zero-02,

Used from specification int-basic1

int-basic1/tot is used by abs-eq,
int-basic1/elim-pred is used by two,
int-basic1/forward-pos is used by rax-01, natpos, ls-fin-add,
int-basic1/irref is used by ls-fin-add, le-fin-add, abs-eq, abs,
int-basic1/lf-01 is used by zero-09, zero-08, qzero-02, num-n2i-ls-07, num-n2i-ls-01, natpos, mod-zero-02,
int-basic1/lf-02 is used by rax-03, num-i2n-eq-01, natpos, ls-fin-add, abs-pred-01,
int-basic1/ls-01 is used by num-n2i-ls-07, num-n2i-ls-01, nat, mod-zero-02, le-fin-add, labsp, labs, i2n-mod, abs-zero, abs-pred-02, abs-pred,
int-basic1/lst-01 is used by nat, labsp, abs-zero, abs-pred,
int-basic1/numlsf is used by nat2int-06,
int-basic1/numlslsdel is used by nat2int-06,
int-basic1/trans is used by zero-09, zero-08, qzero-02, num-n2i-ls-07, num-n2i-ls-01,

Used from specification nat

nat/lels is used by nat2int-04,
nat/prop-01 is used by sub-same,
nat/add-01 is used by i2np, abs-pred-01,
nat/add-num-01 is used by ls-fin-add,
nat/add-num-04 is used by n2i2,
nat/anti is used by le-fin-add,
nat/elim-pred-c is used by ls-fin-add, inj, abs-pred-01,
nat/elim-sub is used by n2i-sub,
nat/eq-01 is used by sub-01, sub,
nat/eq-02 is used by ls-fin-add, abs-pred-02,
nat/eqle-one is used by ls-fin-add,
nat/fle is used by natpos,
nat/l-num-06 is used by labsp,
nat/le-ls-simp is used by zero-13, num-n2i-ls, ls-int-ls-nat,
nat/lels is used by num-n2i-ls-06, num-n2i-ls, num-i2n-ls, natpos, ls-int-ls-nat, ls-fin-add, le-fin-add, labs, i2n-mod, abs-succ-01,
nat/lels-01 is used by sub-same, num-n2i-ls-02, num-i2n-le, ls-fin-add, le-fin-add, labsp, labs-01,
nat/lep-02 is used by nat2int-04,
nat/les is used by ls-fin-add,
nat/lez is used by nat2int-04, le,
nat/lez-01 is used by nat2int-04, ls-fin-add, le-fin-add,
nat/ls is used by labsp, abs-succ,
nat/ls-01 is used by labsp, abs-pred,
nat/ls-le-simp is used by ls-int-ls-nat, ls-fin-add, labs-01,
nat/pred-03 is used by rax-02, rax-01, ls-fin-add, inj, abs-succ-02, abs-succ, abs-pred-01,
nat/succ-01 is used by le,
nat/zero is used by sub-01,

Used from specification int-abs

int-abs/le-def is used by labs-01,
int-abs/Abs-pos is used by ini2-abs,
int-abs/abs-01 is used by abs,
int-abs/abs-05 is used by labsp, abs-succ-01,
int-abs/abs-08 is used by labsp, ini2-abs, abs-succ-01,
int-abs/abs-09 is used by labsp,
int-abs/abs-16 is used by natpos, labsp, labs, inni-le, i2n-mod, i2i-pos,
int-abs/abs-18 is used by abs-02,
int-abs/abs-neg is used by labs,
int-abs/abseq is used by i2i-neg-01,
int-abs/absle is used by labsp, i2n-mod,
int-abs/absls-01 is used by inni-ls,
int-abs/anti is used by zero-12, zero-10, sub-01, ls-fin-add, labsp, labs, i2i-pos-01, abs-negp,
int-abs/elim-sub is used by sub-01, sub, rax-03, qzero-01, i2np, add,
int-abs/forward-le is used by ls-fin-add,
int-abs/forward-le-01 is used by zero-13, zero-12, zero-10, sub-same, sub, rax, num-n2i-ls-06, num-n2i-ls-04, num-n2i-ls-02, num-n2i-ls, num-i2n-ls-02, num-i2n-ls, num-i2n-le-02, num-i2n-le, natpos, nat-to-int-ge-0, mod-zero-02, ls-int-ls-nat, ls-fin-add, ls-03, le-int-le-nat, le-fin-add, labsp, i2np, i2n-mult, i2n-mod, i2n-divtwo, i2n, i2i-pos-01, add-nonneg-int-to-nat, add, abs-negp,
int-abs/forward-le-02 is used by zero-13, zero-12, zero-10, zero-09, zero-08, zero-02, sub-01, qzero-02, num-n2i-ls-07, num-n2i-ls-05, num-n2i-ls-03, num-n2i-ls-01, num-i2n-ls-03, num-i2n-ls-01, num-i2n-le-03, num-i2n-le-01, num-i2n-eq-01, nat2int-08, nat-to-int-ge-0, mod-zero-02, minus-one, ls-int-ls-nat, le-int-le-nat, labsp, i2np, i2n-divtwo, i2n, i2i-neg, add, abs-succ-01, abs-succ, abs-pred-01, abs-pred, abs-neg,
int-abs/forward-le-04 is used by sub-01, rax-01, pos-int, pos-add, nat2int-10, nat-to-int-ge-0, ls-fin-add, abs-pred,
int-abs/forward-le-05 is used by zero-09, zero-08, sub-same, rax-01, qzero-02, qzero-01, num-n2i-ls, num-i2n-le, natpos, mod-zero-02, ls-fin-add, ls-03, labsp, labs, i2np, i2n-mod, i2i-pos, add, abs-succ-03,
int-abs/forward-lele is used by sub, num-i2n-le,
int-abs/forward-lels is used by num-n2i-ls-05, num-n2i-ls-03, num-i2n-ls, ls-int-ls-nat,
int-abs/forward-lsle is used by zero-13, zero-12, zero-10, zero-01, sub-same, rax-03, rax-01, qzero, pos-int, pos-add, num-n2i-ls, num-i2n-le, mod-zero-02, ls-int-ls-nat, ls-fin-add, le-int-le-nat, labsp, inni-ls, i2np, i2n, add,
int-abs/ge-def is used by nat-to-int-ge-0, ls-int-ls-nat, le-int-le-nat,
int-abs/lels is used by zero-13, zero-12, zero-10, zero-02, zero-01, sub-same, rax-03, rax-02, rax-01, qzero, pos-int, pos-add, num-n2i-ls-03, num-n2i-ls-02, num-n2i-ls, num-i2n-ls, nat2int-04, nat-to-int-ge-0, nat, mult-ls-05, mult-ls-04, mult-ls-03, mult-ls-02, minus-one, ls-int-ls-nat, ls-fin-add, le-int-le-nat, labsp, labs, ini2-abs, i2np, i2n-divtwo, i2n, i2i-pos-01, abs-zero, abs-succ-01, abs-pred-02, abs-pred-01, abs-pred, abs-negp,
int-abs/lels-01 is used by zero-11, zero-10, zero-09, zero-08, qzero-02, qzero-01, num-n2i-ls-07, num-n2i-ls-06, num-i2n-le, nat2int-13, nat2int-12, nat2int-01, nat2int, nat, mod-zero-02, ls-int-ls-nat, ls-03, le-int-le-nat, le-fin-add, labsp, labs, i2np, i2n-mod, i2n-divtwo, add, abs-succ, abs-pred-02, abs-pred, abs-neg,
int-abs/lels-02 is used by zero-13, sub-same, sub-01, num-n2i-ls, num-i2n-le, natpos, ls-fin-add, labs, abs-pred,
int-abs/lels-03 is used by zero-12, zero-10, zero-09, zero-08, sub-same, rax-03, num-n2i-ls-06, num-n2i-ls, num-i2n-ls, natpos, ls-fin-add, labsp, labs, inni-le, i2np, i2n-mod, i2n-divtwo, abs-zero, abs-pred-02, abs-pred,
int-abs/lels-04 is used by mult-ls-05, mult-ls-04,
int-abs/lenls is used by num-n2i-ls-02, num-i2n-le, mult-ls-03, mult-ls-02, labsp, i2n-mod,
int-abs/leone is used by rax-01, ls-fin-add, labsp, i2np, add, abs-succ-02, abs-succ, abs-pred-02, abs-pred,
int-abs/lep is used by sub, rax-03,
int-abs/lep-01 is used by sub-01,
int-abs/lep-02 is used by le-fin-add,
int-abs/ler is used by rax-03, le-fin-add,
int-abs/lsone is used by abs-pred,
int-abs/minus-02 is used by abs-pred,
int-abs/minus-add is used by labsp,
int-abs/mone-06 is used by zero-10, zero-08, zero-01, rax-04, rax, qzero, mult-ls-05, mult-ls-04, ls-fin-add, labsp, i2np, add,
int-abs/mone-08 is used by minus-one, labsp, i2np, add, abs-pred-01, abs-pred,
int-abs/neg is used by rax-03, rax-02, nat, i2i-neg, abs-zero, abs-succ,
int-abs/neg-02 is used by nat, i2n, abs-negp, abs-neg,
int-abs/neg-03 is used by rax-03, num-i2n-eq-01, i2n-divtwo,
int-abs/neg-05 is used by abs-negp,
int-abs/neg-06 is used by abs-pred,
int-abs/neg-07 is used by num-i2n-ls-03,
int-abs/neg-10 is used by nat,
int-abs/neg-11 is used by sub-01,
int-abs/neg-12 is used by num-i2n-eq-01, ini2-abs,
int-abs/neg-13 is used by num-i2n-ls-01, labsp,
int-abs/neg-15 is used by abs-succ-01, abs-pred,
int-abs/negeq is used by two, rax-03, num-i2n-eq-01, mone-01, i2n-divtwo, i2i-neg-01, i2i-neg, abs-one,
int-abs/negle-07 is used by sub-01, num-i2n-le-03, nat, labs, i2n, abs-neg,
int-abs/negle-13 is used by num-i2n-le-01, abs-succ-01, abs-pred,
int-abs/num-subadd is used by abs-pred,
int-abs/numadd is used by succ-01, nat2int-05, n2i-add, inj,
int-abs/numadd-01 is used by two, rax-03, nat2int-07, n2i2, mone-01, ls-fin-add, i2n-divtwo, abs-succ, abs-one,
int-abs/numle-02 is used by labsp, i2np, add-nonneg-int-to-nat, add, abs-pred,
int-abs/numle-03 is used by nat2int-10,
int-abs/numlef-01 is used by zero-01, qzero,
int-abs/numleledel-01 is used by labsp, i2np, add-nonneg-int-to-nat, add,
int-abs/numls-01 is used by ls-fin-add,
int-abs/numls-02 is used by zero-10, zero-08, rax-04, rax, mult-ls-05, mult-ls-04, ls-fin-add, labsp, i2np, add,
int-abs/numls-03 is used by rax-02, nat2int-12, nat2int-06, minus-one, ls-fin-add, abs-pred-01,
int-abs/numsub is used by rax, labsp, i2np, add,
int-abs/sub-add-01 is used by ls-fin-add, add,
int-abs/sub-add-09 is used by abs-succ-01,
int-abs/sub-eq is used by n2i-sub, ls-fin-add,
int-abs/sub-le-01 is used by labsp, i2np, add,
int-abs/sub-ls is used by labsp, abs-pred,
int-abs/sub-ls-01 is used by ls-fin-add, labsp, abs-pred,
int-abs/sub-pred is used by ls-fin-add, labsp, i2np, add,
int-abs/sub-sub is used by abs-pred,
int-abs/subsub is used by rax-02, labsp, abs-succ-01,
int-abs/succ-01 is used by le-fin-add, le,
int-abs/succ-02 is used by rax-03, ls-fin-add, labsp,
int-abs/zero-gels is used by rax-02,
int-abs/zero-gels-01 is used by zero-13, zero-12, zero-10, zero-09, zero-08, rax-02, num-i2n-ls-03, nat2int-06, nat, mod-zero-02, labsp, i2n-divtwo, i2n, i2i-neg, abs-succ, abs-pred, abs-one,
int-abs/zero-gels-03 is used by sub-01, nat, i2n, abs-pred, abs-neg,
int-abs/zero-gels-04 is used by sub-01, sub, rax-04, rax, num-i2n-le-03, num-i2n-le-01, natpos, nat, mod-zero-02, ls-fin-add, ls-03, le-fin-add, labsp, labs, i2np, i2n-mult, i2n-mod, i2i-neg-01, add-01, add,
int-abs/zero-gs is used by labsp, add,

Used from specification nat-basic2

nat-basic2/a is used by two-01, three, ten, succ-01, succ, sub-same, sub-01, sub, six, seven, rax-03, rax-02, rax, nine, nat2int-10, nat2int-09, nat2int-08, nat2int-06, nat2int-05, nat2int-04, nat2int-02, nat-to-int-ge-0, n2n, n2i2, n2i-sub, n2i-mult, n2i-add, ls-fin-add, le-fin-add, le, labsp, inj, i2np, i2n-mod, i2n-divtwo, four, five, eight, add-nonneg-int-to-nat, add-n2i-num, add, abs-zero, abs-succ-01, abs-succ, abs-pred-02, abs-pred-01, abs-pred, abs-01,
nat-basic2/add-base is used by n2i-add, ls-fin-add, i2np, add-nonneg-int-to-nat, add, abs-pred-01,
nat-basic2/c is used by two-01, three, ten, succ-01, succ, sub-same, sub-01, sub, six, seven, rax-03, rax-02, rax, nine, nat2int-11, nat2int-10, nat2int-09, nat2int-08, nat2int-06, nat2int-05, nat2int-04, nat2int-02, nat-to-int-ge-0, n2n, n2i2, n2i-sub, n2i-mult, n2i-add, ls-fin-add, le-fin-add, le, labsp, inj, i2np, i2n-mod, i2n-divtwo, four, five, eight, add-nonneg-int-to-nat, add-n2i-num, add, abs-zero, abs-succ-01, abs-succ, abs-pred-02, abs-pred-01, abs-pred, abs-01,
nat-basic2/eq-01 is used by succ, rax-03, rax, nat2int-09, nat2int-05, n2n, ls-fin-add, inj, i2np, add,
nat-basic2/l-02 is used by ls-fin-add, abs-succ-01, abs-succ, abs-pred,
nat-basic2/oz is used by nat2int-10, nat2int-04, ls-fin-add, le-fin-add, inj, abs-zero,
nat-basic2/pred is used by rax-02,
nat-basic2/s is used by ls-fin-add, le-fin-add, labsp, abs-succ, abs-pred,
nat-basic2/succ is used by nat2int-10, nat2int-08, nat2int-06, nat2int-05, nat2int-04, nat2int-03, nat2int-02, n2n, n2i2, n2i-mult, n2i-add, ls-fin-add, le-fin-add, le, inj, add-nonneg-int-to-nat, abs-pred-02,
nat-basic2/z-01 is used by ls-fin-add, le-fin-add,

Used from specification nat-mult

nat-mult/modeq is used by natpos,
nat-mult/ls2-03 is used by abs-pred,
nat-mult/mult-a is used by n2i-mult, i2np, i2n-mod, i2n-divtwo, abs-pred,
nat-mult/mult-c is used by n2i-mult, i2np, i2n-mod, i2n-divtwo, abs-pred,
nat-mult/rsucc-02 is used by n2i-mult, i2np,
nat-mult/two-02 is used by abs-pred,
nat-mult/zero is used by n2i-mult, i2np,

Used from specification int-basic2

int-basic2/add-a is used by zero-13, zero-10, zero-08, zero-01, two-01, two, three, ten, succ-01, succ, sub-same, sub-01, sub, six, seven, rax-04, rax-03, rax-02, rax, qzero-02, qzero-01, qzero, num-i2n-eq-01, nine, natpos, nat2int-13, nat2int-12, nat2int-11, nat2int-10, nat2int-09, nat2int-08, nat2int-07, nat2int-06, nat2int-05, nat2int-04, nat2int-02, nat2int-01, nat-to-int-ge-0, nat, n2n, n2i2, n2i-sub, n2i-mult, n2i-add, n2i, mult-ls-05, mult-ls-04, mone-01, minus-one, ls-int-ls-nat, ls-fin-add, le-int-le-nat, le-fin-add, le, labsp, labs, inni-ls-01, inj, i2np, i2n-mod, i2n-divtwo, i2n, i2i-neg-01, four, five, eight, add-nonneg-int-to-nat, add-n2i-num, add, abs-succ-03, abs-succ-01, abs-succ, abs-pred-01, abs-pred, abs-one, abs-neg,
int-basic2/add-c is used by zero-13, zero-10, zero-08, zero-01, two-01, two, three, ten, succ-01, succ, sub-same, sub-01, sub, six, seven, rax-04, rax-03, rax-02, rax, qzero-02, qzero-01, qzero, num-i2n-eq-01, nine, natpos, nat2int-13, nat2int-12, nat2int-11, nat2int-10, nat2int-09, nat2int-08, nat2int-07, nat2int-06, nat2int-05, nat2int-04, nat2int-02, nat2int-01, nat-to-int-ge-0, nat, n2n, n2i2, n2i-sub, n2i-mult, n2i-add, n2i, mult-ls-05, mult-ls-04, mone-01, minus-one, ls-int-ls-nat, ls-fin-add, le-int-le-nat, le-fin-add, le, labsp, labs, inni-ls-01, inj, i2np, i2n-mod, i2n-divtwo, i2n, i2i-neg-01, four, five, eight, add-nonneg-int-to-nat, add-n2i-num, add, abs-succ-03, abs-succ-01, abs-succ, abs-pred-01, abs-pred, abs-one, abs-neg,
int-basic2/add-in is used by n2i-sub, add-n2i-num,
int-basic2/add-zero is used by i2n-divtwo,
int-basic2/add-zero-rev is used by succ-01, sub-01, rax, nat2int-05, nat, n2i-add, ls-fin-add, labsp, labs, inj, i2np, i2n, add-nonneg-int-to-nat, add, abs-pred, abs-neg,
int-basic2/ls is used by sub-same, rax-03, qzero-01, nat2int-13, nat2int-12, nat2int-01, ls-int-ls-nat, ls-fin-add, le-int-le-nat,
int-basic2/ls-01 is used by zero-13, rax-03, qzero-02, nat2int-04, ls-fin-add, le-fin-add,
int-basic2/ls-02 is used by zero-01, qzero-02, qzero, num-i2n-eq-01,
int-basic2/lst-03 is used by ls-fin-add,
int-basic2/lst-04 is used by ls-fin-add,
int-basic2/mone-02 is used by two,
int-basic2/mone-03 is used by rax-03,
int-basic2/succ-01 is used by zero-09, zero-08, two, qzero-02, nat2int-03, mod-zero-02, ls-fin-add, labsp, i2np, add,
int-basic2/zero-02 is used by abs-succ-03,

Used from specification int-div

int-div/lsf-01 is used by ls-03,
int-div/mod-zero-01 is used by mod-zero-02,
int-div/mult-ls is used by mult-ls-04, mult-ls-02,
int-div/mult-ls-01 is used by mult-ls-05, mult-ls-03,
int-div/zero-01 is used by zero-09, zero-08,
int-div/zero-03 is used by zero-12, zero-10,
int-div/div-elim-pos is used by natpos,
int-div/div-elim-pospos is used by i2n-mod,
int-div/mod-ls-same-01 is used by mod-zero-02,
int-div/mod-one is used by mod-zero-02,
int-div/mod-zero-09 is used by mod-zero-02,
int-div/neg is used by nat,
int-div/neg-01 is used by nat,
int-div/one is used by ls-03,
int-div/zero is used by zero-12, zero-10,

Used from specification nat-basic1

nat-basic1/tot is used by abs-eq, abs,
nat-basic1/twols-01 is used by i2n-divtwo,
nat-basic1/elim-pred-c is used by nat2int-04,
nat-basic1/f is used by sub-same, num-n2i-ls, num-i2n-le, natpos, ls-int-ls-nat, ls-fin-add, le-fin-add, inni-ls, inni-le-01, i2n-divtwo, abs-succ, abs-pred,
nat-basic1/lf-01 is used by ls-fin-add,
nat-basic1/lf-02 is used by ls-fin-add,
nat-basic1/one-01 is used by nat2int-14, labsp,
nat-basic1/ref-1 is used by ls-fin-add, abs-succ, abs-pred, abs-eq,
nat-basic1/zero is used by zero-12, zero-09, zero-02, num-n2i-ls, num-i2n-ls, num-i2n-le, num-i2n-eq-01, mult-ls-03, mult-ls-02, mod-zero-02, ls-fin-add, ls-03, labsp,
nat-basic1/zero-01 is used by labs,

Used from specification nat-div

nat-div/mod-eq is used by i2n-mod,
nat-div/div-elim is used by natpos, i2n-divtwo,
nat-div/mod-mult is used by i2n-mod,