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

term/disj-01 is used by topred-unique, K-does-not-top-reduce,
term/disj-02 is used by S-does-not-top-reduce,
term/inj is used by topred-unique, reduction-is-topred-in-ctxt, irred-top-01, irred-top,
term/test-03 is used by reduce-no-ap,

Used from specification nat

nat/elim-pred-c is used by it-rec-01,
nat/pred-03 is used by it-rec-01,

Used from specification context

context/ax-01 is used by reduction-is-topred-in-ctxt, irred-top-01, irred-top, fun-reduces-imp-app-reduces,
context/ax-02 is used by reduction-is-topred-in-ctxt, irred-top-01, irred-top, fun-value-and-arg-reduces-imp-app-reduces,
context/context-O is used by reduction-is-topred-in-ctxt, reduce-topreduce, irred-top-01, irred-top, S-reduce, K-reduce,

Used from specification subst

subst/subst-KK-equal is used by reduce-unique,
subst/subst-SK-equal is used by reduce-unique,
subst/subst-SS-equal is used by reduce-unique,
subst/K-is-only-OK is used by reduction-is-topred-in-ctxt,
subst/S-is-only-OS is used by reduction-is-topred-in-ctxt,
subst/not-value is used by irred-top-01, irred-top,
subst/not-value-02 is used by irred-top-01, irred-top,
subst/subst-Carg is used by reduction-is-topred-in-ctxt, irred-top-01, irred-top, fun-value-and-arg-reduces-imp-app-reduces,
subst/subst-Cfun is used by reduction-is-topred-in-ctxt, irred-top-01, irred-top, fun-reduces-imp-app-reduces,
subst/subst-O is used by reduction-is-topred-in-ctxt, reduce-topreduce, irred-top-01, irred-top, S-reduce, K-reduce,
subst/substap-is-not-K is used by K-does-not-reduce,
subst/substap-is-not-S is used by S-does-not-reduce,

Used from specification nat-basic2

nat-basic2/a is used by it-rec-01,
nat-basic2/c is used by it-rec-01,
nat-basic2/oz is used by it-rec-01,