[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 nat-even
Used from specification reduce
- reduce/irred-def
is used by
RED1-lem,
RED-correct,
- reduce/it-rec-01
is used by
RED-complete,
- reduce/reduce-def
is used by
RED-correct,
RED-complete,
- reduce/reduce-unique
is used by
RED-complete,
- reduce/topred-def
is used by
TOPRED-lem,
- reduce/K-top-reduce
is used by
TOPRED-lem,
- reduce/S-top-reduce
is used by
TOPRED-lem,
- reduce/fun-reduces-imp-app-reduces
is used by
RED1-lem,
- reduce/fun-value-and-arg-reduces-imp-app-reduces
is used by
RED1-lem,
- reduce/irred-no-step
is used by
RED-correct,
RED-complete,
- reduce/irred-top
is used by
RED1-lem,
- reduce/irred-top-01
is used by
RED1-lem,
- reduce/it-base
is used by
RED-complete,
- reduce/it-rec
is used by
RED-correct,
- reduce/no-ap-irred
is used by
RED1-lem,
- reduce/reduce-topreduce
is used by
RED1-lem,
- reduce/reduction-is-reflexive
is used by
RED-correct,
Used from specification termfuns
- termfuns/ks-rec-01
is used by
ks-TOPRED,
ks-RED1,
ks-RED,
- termfuns/hasS-A
is used by
termination-TOPRED,
termination-RED1,
- termfuns/hasS-K
is used by
termination-TOPRED,
termination-RED1,
- termfuns/hasS-S
is used by
termination-TOPRED,
termination-RED1,
- termfuns/hasS-some
is used by
termination-TOPRED,
termination-RED1,
termination-RED,
- termfuns/ks-K
is used by
ks-TOPRED,
ks-RED,
- termfuns/ks-K-01
is used by
ks-RED1,
- termfuns/ks-K-02
is used by
ks-RED,
- termfuns/ks-not-S
is used by
ks-TOPRED,
ks-RED,
- termfuns/ks-not-S-01
is used by
ks-RED1,
- termfuns/ks-rec
is used by
ks-RED1,
- termfuns/ks-zero
is used by
ks-TOPRED,
ks-RED1,
ks-RED,
- termfuns/size-some
is used by
termination-TOPRED,
termination-RED1,
termination-RED,
Used from specification nat-mult
- nat-mult/mult-a
is used by
termination-TOPRED,
termination-RED1,
- nat-mult/mult-c
is used by
termination-TOPRED,
termination-RED1,
- nat-mult/numeral-21
is used by
termination-TOPRED,
termination-RED1,
- nat-mult/one
is used by
termination-TOPRED,
termination-RED1,
- nat-mult/two-02
is used by
termination-TOPRED,
termination-RED1,
Used from specification term
- term/disj-01
is used by
termination-TOPRED,
termination-RED1,
ks-TOPRED,
ks-RED1,
ks-RED,
kappa-TOPRED,
kappa-RED1,
TOPRED-lem,
SII-loops,
- term/disj-02
is used by
termination-RED1,
SII-loops,
- term/disj-03
is used by
termination-RED1,
SII-loops,
- term/elim
is used by
termination-TOPRED,
termination-RED1,
ks-TOPRED,
ks-RED1,
ks-RED,
kappa-TOPRED,
kappa-RED1,
TOPRED-lem,
RED1-lem,
- term/inj
is used by
ks-TOPRED,
ks-RED,
TOPRED-lem,
- term/sel-01
is used by
termination-RED1,
ks-TOPRED,
ks-RED1,
kappa-TOPRED,
kappa-RED1,
TOPRED-lem,
SII-loops,
- term/sel-02
is used by
termination-RED1,
ks-RED1,
kappa-TOPRED,
kappa-RED1,
TOPRED-lem,
SII-loops,
- term/size-02
is used by
termination-TOPRED,
termination-RED1,
- term/size-03
is used by
termination-TOPRED,
termination-RED1,
RED1-lem,
- term/test-01
is used by
SII-loops,
- term/test-02
is used by
termination-RED1,
ks-RED1,
ks-RED,
kappa-TOPRED,
TOPRED-lem,
SII-loops,
- term/test-03
is used by
termination-TOPRED,
termination-RED1,
ks-TOPRED,
ks-RED1,
ks-RED,
kappa-TOPRED,
kappa-RED1,
TOPRED-lem,
SII-loops,
RED1-lem,
Used from specification nat-basic1
Used from specification nat
- nat/add-01
is used by
ks-RED1,
SII-loops,
- nat/add-num-03
is used by
termination-RED1,
ks-RED1,
ks-RED,
SII-loops,
- nat/elim-pred-c
is used by
kappa-RED1,
SII-loops,
RED-complete,
- nat/elim-sub
is used by
ks-RED1,
ks-RED,
- nat/l-num-01
is used by
termination-RED1,
- nat/l-num-02
is used by
termination-TOPRED,
termination-RED1,
- nat/le-add
is used by
termination-RED1,
ks-RED1,
ks-RED,
- nat/le-num-01
is used by
termination-TOPRED,
termination-RED1,
- nat/lels
is used by
termination-TOPRED,
termination-RED1,
ks-RED,
- nat/lels-01
is used by
ks-RED1,
ks-RED,
- nat/lep
is used by
ks-RED,
- nat/lep-02
is used by
termination-TOPRED,
termination-RED1,
- nat/one-02
is used by
ks-RED1,
ks-RED,
- nat/pred-03
is used by
kappa-RED1,
SII-loops,
RED-complete,
Used from specification nat-basic2
- nat-basic2/a
is used by
termination-TOPRED,
termination-RED1,
ks-RED1,
ks-RED,
kappa-RED1,
SII-loops,
RED1-lem,
RED-correct,
RED-complete,
- nat-basic2/c
is used by
termination-TOPRED,
termination-RED1,
ks-RED1,
ks-RED,
kappa-RED1,
SII-loops,
RED1-lem,
RED-correct,
RED-complete,
- nat-basic2/l
is used by
termination-RED1,
SII-loops,
- nat-basic2/l-02
is used by
termination-TOPRED,
termination-RED1,
RED1-lem,
- nat-basic2/one
is used by
ks-RED1,
ks-RED,
- nat-basic2/oz
is used by
kappa-RED1,
SII-loops,
RED-complete,
- nat-basic2/pred
is used by
SII-loops,
- nat-basic2/s
is used by
termination-TOPRED,
termination-RED1,
kappa-RED1,
RED1-lem,
RED-complete,
- nat-basic2/succ
is used by
termination-TOPRED,
termination-RED1,
ks-RED1,
RED1-lem,
RED-correct,
- nat-basic2/z
is used by
termination-TOPRED,
termination-RED1,
- term_or_none/disj
is used by
termination-TOPRED,
termination-RED1,
termination-RED,
ks-TOPRED,
ks-RED1,
ks-RED,
kappa-TOPRED,
kappa-RED1,
TOPRED-lem,
SII-loops,
RED1-lem,
RED-correct,
RED-complete,
- term_or_none/elim
is used by
termination-RED1,
termination-RED,
kappa-RED1,
RED-correct,
RED-complete,
- term_or_none/inj
is used by
ks-TOPRED,
ks-RED1,
kappa-TOPRED,
kappa-RED1,
- term_or_none/sel
is used by
ks-RED1,
ks-RED,
TOPRED-lem,
SII-loops,
RED1-lem,
Used from specification value
- value/val-K
is used by
termination-RED1,
ks-TOPRED,
ks-RED1,
ks-RED,
SII-loops,
- value/val-K-ap
is used by
termination-RED1,
ks-RED1,
kappa-RED1,
SII-loops,
- value/val-S
is used by
SII-loops,
- value/val-S-ap
is used by
SII-loops,
- value/val-other-ap
is used by
termination-RED1,
- value/value
is used by
SII-loops,
- value/value-01
is used by
SII-loops,
- value/value-02
is used by
SII-loops,
- value/value-03
is used by
SII-loops,