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

int-basic1/lf-02 is used by dec-int-01, dec-int,

Used from specification int-mult

int-mult/add-mult-two is used by dec-int-01, dec-int,
int-mult/associativity is used by dec-int-01, dec-int,
int-mult/commutativity is used by dec-int-01, dec-int,
int-mult/zero-neq-01 is used by dec-int-01, dec-int,

Used from specification nat

nat/add-num-01 is used by dec-nat-01, dec-nat,
nat/elim-pred-c is used by enc-zero-01, dec-nat-01, dec-nat, dec-int-01, dec-int,

Used from specification int-abs

int-abs/forward-le-01 is used by dec-int-01, dec-int,
int-abs/forward-le-02 is used by enc-zero-01, dec-int-01, dec-int,
int-abs/lels is used by enc-zero-01, dec-int-01, dec-int,
int-abs/lels-02 is used by enc-zero-01,
int-abs/neg-05 is used by dec-nat-01, dec-nat,
int-abs/neg-10 is used by enc-zero-02,
int-abs/negeq is used by dec-int-01, dec-int,
int-abs/numadd-01 is used by dec-int-01, dec-int,

Used from specification nat-basic2

nat-basic2/a is used by enc-zero-02, enc-zero-01, dec-nat-01, dec-nat, dec-int-01, dec-int,
nat-basic2/c is used by enc-zero-02, enc-zero-01, dec-nat-01, dec-nat, dec-int-01, dec-int,
nat-basic2/one-03 is used by enc-zero-02, dec-nat-01, dec-nat,
nat-basic2/oz is used by enc-zero-02, dec-nat-01, dec-nat,

Used from specification nat-pair

nat-pair/enc-invert is used by exencode, enc-invert,
nat-pair/encode-zero is used by enc-zero,
nat-pair/encode-zero-01 is used by enc-zero,
nat-pair/fst-def is used by sel-fst,
nat-pair/snd-def is used by sel-snd,

Used from specification intnat

intnat/abs-neg is used by dec-nat-01, dec-nat,
intnat/abs-zero is used by enc-zero-01, dec-int-01, dec-int,
intnat/i2i-neg is used by dec-int-01, dec-int,
intnat/i2i-pos-01 is used by dec-int-01, dec-int,
intnat/n2i-add is used by dec-int-01, dec-int,
intnat/n2n is used by dec-nat-01, dec-nat,
intnat/nat2int is used by dec-nat-01, dec-nat,
intnat/nat2int-02 is used by enc-zero-02,
intnat/num-n2i-ls-02 is used by dec-nat-01, dec-nat,
intnat/succ-01 is used by dec-int-01, dec-int,

Used from specification int-basic2

int-basic2/add-a is used by dec-int-01, dec-int,
int-basic2/add-c is used by dec-int-01, dec-int,

Used from specification nat-mult

nat-mult/coef-17 is used by dec-int-01, dec-int,
nat-mult/modeq-01 is used by dec-int-01, dec-int,
nat-mult/mult-a is used by enc-zero-01, enc-zero, dec-nat-01, dec-nat, dec-int-01, dec-int,
nat-mult/mult-c is used by enc-zero-01, enc-zero, dec-nat-01, dec-nat, dec-int-01, dec-int,
nat-mult/one-01 is used by enc-zero-01,
nat-mult/rsucc-02 is used by dec-nat-01, dec-nat,
nat-mult/two-zero-01 is used by enc-zero-01, dec-nat-01, dec-nat, dec-int-01, dec-int,

Used from specification nat-basic1

nat-basic1/twols-02 is used by dec-nat-01, dec-nat, dec-int-01, dec-int,
nat-basic1/zero is used by dec-nat-01, dec-nat,

Used from specification nat-div

nat-div/modex is used by dec-int-01, dec-int,
nat-div/div-elim is used by dec-nat-01, dec-nat, dec-int-01, dec-int,
nat-div/mod-mult-01 is used by dec-int-01, dec-int,
nat-div/mult-02 is used by dec-nat-01, dec-nat,
nat-div/two-mdiv2-02 is used by dec-int-01, dec-int,
nat-div/two-mdiv2-03 is used by dec-int-01, dec-int,
nat-div/two-twosucc-02 is used by dec-nat-01, dec-nat, dec-int-01, dec-int,
nat-div/two-zero-01-01 is used by enc-zero-02, dec-nat-01, dec-nat,