[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-basic
- nat-basic/a
is used by
And-forall,
precise-Sep,
And-discard,
Sep-forall,
- nat-basic/c
is used by
And-forall,
precise-Sep,
And-discard,
Sep-forall,
- nat-basic/oz
is used by
And-forall,
precise-Sep,
And-discard,
Sep-forall,
- nat-basic/refl-nat
is used by
And-forall,
precise-Sep,
And-discard,
Sep-forall,
- nat-basic/s-04
is used by
And-forall,
precise-Sep,
And-discard,
Sep-forall,
Used from specification heap-sep
- heap-sep/and
is used by
And-discard,
- heap-sep/sep
is used by
Sep-forall,
- heap-sep/split-union
is used by
Sep-forall,
- heap-sep/and
is used by
And-forall,
- heap-sep/and-ass
is used by
And-forall,
And-discard,
- heap-sep/and-com
is used by
And-forall,
And-discard,
- heap-sep/emp
is used by
Sep-forall,
- heap-sep/precise-emp
is used by
precise-Sep,
- heap-sep/precise-sep
is used by
precise-Sep,
- heap-sep/sep-ass
is used by
precise-Sep,
- heap-sep/sep-com
is used by
precise-Sep,
- heap-sep/true-and
is used by
And-discard,
- heap-sep/trueH
is used by
And-forall,
Used from specification set-union
Used from specification set-basic
- set-basic/Extension
is used by
And-forall,
precise-Sep,
And-discard,
Sep-forall,
- set-basic/indef
is used by
Sep-unfold,
And-forall,
precise-Sep,
And-discard,
Sep-forall,
And-unfold,
- set-basic/In-empty
is used by
And-forall,
precise-Sep,
And-discard,
Sep-forall,
- set-basic/In-insert
is used by
And-forall,
precise-Sep,
Sep-forall,
- set-basic/Size-insert
is used by
And-forall,
precise-Sep,
And-discard,
Sep-forall,
- set-basic/ne-01
is used by
Sep-unfold,
And-forall,
precise-Sep,
Sep-forall,
And-unfold,
Sep-eq,
- set-basic/size-zero
is used by
And-forall,
precise-Sep,
And-discard,
Sep-forall,
- set-basic/size-zero-01
is used by
Sep-unfold,
And-forall,
precise-Sep,
And-discard,
Sep-forall,
And-unfold,
Sep-eq,
- set-basic/size-zero-02
is used by
And-discard,