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/Mult-zero is used by i2np, n2i-mult,
• int-mult/associativity is used by i2np, i2n-mod, natpos, n2i-mult, mult-ls-04, qzero-01, qzero, mult-ls-05, zero-01, zero-13, qzero-02, zero-02, i2n-divtwo, i2n,
• int-mult/commutativity is used by i2np, i2n-mod, natpos, n2i-mult, mult-ls-04, qzero-01, qzero, mult-ls-05, zero-01, zero-13, qzero-02, zero-02, i2n-divtwo, i2n,
• int-mult/dist-rmerge is used by i2n-divtwo,
• 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 i2np,
• int-mult/succ-rmerge is used by i2np, n2i-mult, mult-ls-04, mult-ls-05, qzero-02,
• int-mult/two-zero is used by i2n-divtwo,
• int-mult/zero-ge is used by i2n-mod, natpos, i2n-divtwo,
• int-mult/zero-ge-02 is used by i2np,
• int-mult/zero-ge-add is used by i2n-mod, natpos,
• int-mult/zero-gr-01 is used by qzero-01, qzero, zero-01,
• int-mult/zero-le-01 is used by qzero-02,
• int-mult/zero-left is used by zero-02,
• 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/irref is used by abs, le-fin-add, abs-eq, ls-fin-add,
• int-basic1/lf-01 is used by natpos, zero-13, num-n2i-ls-01, num-n2i-ls-07,
• int-basic1/lf-02 is used by natpos, ls-fin-add,
• int-basic1/lf-03 is used by abs-pred-01, minus-one,
• int-basic1/ls-01 is used by i2n-mod, abs-neg, labs, abs-pred, abs-zero, abs-succ-03, num-n2i-ls-01, labsp, num-n2i-ls-07, nat, le-fin-add, abs-pred-02, i2n, sub-01,
• int-basic1/lst-01 is used by abs-pred, abs-zero, labsp, nat,
• int-basic1/lst-02 is used by nat,
• int-basic1/trans is used by num-n2i-ls-01, num-n2i-ls-07,

Used from specification nat-basic

• nat-basic/lstwo is used by i2n-divtwo,
• nat-basic/tot is used by abs, abs-eq,
• nat-basic/a is used by rax-02, add-n2i-num, i2np, i2n-mod, add, n2i-mult, nat2int-04, abs-pred, sub-same, n2i-sub, abs-zero, le, rax, nat2int-10, rax-03, succ, inj, n2n, nat2int-05, sub, labsp, i2n-divtwo, nat2int-02, n2i-add, abs-pred-01, abs-succ, le-fin-add, nat2int-08, abs-pred-02, nat-to-int-ge-0, add-nonneg-int-to-nat, ls-fin-add, nat2int-09, n2i2, nat2int-06, abs-succ-01, sub-01,
• nat-basic/add-base is used by ls-fin-add,
• nat-basic/c is used by rax-02, add-n2i-num, i2np, i2n-mod, add, n2i-mult, nat2int-04, abs-pred, sub-same, n2i-sub, abs-zero, le, rax, nat2int-10, rax-03, succ, inj, n2n, nat2int-05, sub, nat2int-11, labsp, i2n-divtwo, nat2int-02, n2i-add, abs-pred-01, abs-succ, le-fin-add, nat2int-08, abs-pred-02, nat-to-int-ge-0, add-nonneg-int-to-nat, ls-fin-add, nat2int-09, n2i2, nat2int-06, abs-succ-01, sub-01,
• nat-basic/elim-pred-c is used by nat2int-04,
• nat-basic/eq-01 is used by i2np, add, rax, rax-03, succ, inj, n2n, nat2int-05, ls-fin-add, nat2int-09,
• nat-basic/f is used by natpos, abs-pred, sub-same, num-i2n-le, zero-13, inni-ls, ls-int-ls-nat, num-n2i-ls, i2n-divtwo, abs-succ, le-fin-add, ls-fin-add,
• nat-basic/l-02 is used by abs-pred, abs-succ, ls-fin-add, abs-succ-01,
• nat-basic/less-zero is used by le-fin-add,
• nat-basic/lf-01 is used by ls-fin-add,
• nat-basic/lf-02 is used by ls-fin-add,
• nat-basic/one-01 is used by labsp, nat2int-14,
• nat-basic/oz is used by abs-zero, nat2int-10, inj, ls-fin-add,
• nat-basic/pred is used by rax-02,
• nat-basic/refl-nat is used by abs-pred, zero-13, abs-succ, abs-eq, ls-fin-add,
• nat-basic/s-04 is used by abs-pred, labsp, abs-succ, le-fin-add, ls-fin-add,
• nat-basic/succ is used by nat2int-03, n2i-mult, nat2int-04, le, nat2int-10, inj, n2n, nat2int-05, nat2int-02, n2i-add, le-fin-add, nat2int-08, abs-pred-02, add-nonneg-int-to-nat, ls-fin-add, n2i2, nat2int-06,
• nat-basic/z-01 is used by ls-fin-add,
• nat-basic/z-02 is used by i2np, add, n2i-add, add-nonneg-int-to-nat,
• nat-basic/zero is used by zero-09, num-i2n-ls, zero-12, num-i2n-le, mult-ls-02, zero-02, labsp, num-n2i-ls, mult-ls-03, mod-zero-02, ls-03, ls-fin-add,

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

Used from specification nat-mult

• nat-mult/modeq is used by natpos,
• nat-mult/mult-a is used by i2np, i2n-mod, n2i-mult, i2n-divtwo,
• nat-mult/mult-base is used by i2np, n2i-mult,
• nat-mult/mult-c is used by i2np, i2n-mod, n2i-mult, i2n-divtwo,
• nat-mult/rsucc-02 is used by i2np, n2i-mult,

Used from specification int-basic2

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

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