[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
value-context,
substap-is-not-K,
subst-SK-equal,
subst-KK-equal,
not-value-02,
not-value,
K-is-only-OK,
- term/disj-02
is used by
value-context,
substap-is-not-S,
subst-SS-equal,
subst-SK-equal,
not-value-02,
not-value,
S-is-only-OS,
- term/disj-03
is used by
value-context,
subst-SK-equal,
not-value,
- term/elim
is used by
value-context,
not-value-02,
not-value,
- term/inj
is used by
subst-SS-equal,
subst-SK-equal,
subst-KK-equal,
- term/sel-01
is used by
not-value-02,
not-value,
- term/sel-02
is used by
not-value-02,
not-value,
- term/test-03
is used by
value-context,
not-value-02,
not-value,
ap-in-context-is-ap,
Used from specification context
- context/ax-01
is used by
value-context,
subst-SS-equal,
subst-SK-equal,
subst-KK-equal,
- context/ax-02
is used by
value-context,
subst-SS-equal,
subst-SK-equal,
subst-KK-equal,
- context/context-O
is used by
value-context,
subst-SS-equal,
subst-SK-equal,
subst-KK-equal,
Used from specification value
- value/val-other-ap
is used by
value-context,
not-value-02,
not-value-01,
not-value,
- value/val-K
is used by
value-context,
subst-SK-equal,
subst-KK-equal,
- value/val-K-ap
is used by
value-context,
subst-SK-equal,
subst-KK-equal,
not-value-02,
not-value-01,
not-value,
- value/val-S
is used by
value-context,
subst-SS-equal,
subst-SK-equal,
- value/val-S-ap
is used by
value-context,
subst-SS-equal,
subst-SK-equal,
not-value-02,
not-value-01,
not-value,