[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/c
is used by
Sep-split,
- nat-basic/a
is used by
Sep-unfold,
Sep-split,
Sep-forall,
Sep-forall-prove-imp,
Sep-range,
- nat-basic/add-base
is used by
Sep-split,
Sep-forall,
Sep-forall-prove-imp,
Sep-range,
- nat-basic/c
is used by
Sep-unfold,
Sep-split,
Sep-forall,
Sep-forall-prove-imp,
Sep-range,
- nat-basic/f
is used by
Sep-unfold,
Sep-forall,
Sep-forall-reduce-imp,
Sep-forall-prove-imp,
Sep-weak-conjunction,
- nat-basic/l-01
is used by
Sep-unfold,
- nat-basic/l-02
is used by
Sep-unfold,
Sep-range,
- nat-basic/less-zero
is used by
Sep-forall,
Sep-forall-prove-imp,
- nat-basic/oz
is used by
Sep-unfold,
- nat-basic/s-04
is used by
Sep-forall,
Sep-forall-prove-imp,
Sep-range,
- nat-basic/succ
is used by
Sep-emp,
Sep-distribute-true,
Sep-split,
Sep-forall,
Sep-forall-prove-imp,
Sep-range,
Used from specification heap-sep
- heap-sep/sep-ass
is used by
Sep-distribute-true,
- heap-sep/sep-inj2-imp
is used by
Sep-forall-prove-imp,
- heap-sep/Imp-refl
is used by
Sep-forall-prove-imp,
- heap-sep/Imp2
is used by
Sep-forall-reduce-imp,
- heap-sep/emp-sep
is used by
Sep-emp,
Sep-distribute-true,
Sep-split,
- heap-sep/imp-proptrue
is used by
Sep-range,
- heap-sep/sep-ass
is used by
Sep-emp,
Sep-distribute-true,
Sep-unfold,
Sep-split,
Sep-forall-reduce-imp,
Sep-weak-conjunction,
- heap-sep/sep-com
is used by
Sep-emp,
Sep-distribute-true,
Sep-unfold,
Sep-split,
Sep-forall-reduce-imp,
Sep-weak-conjunction,
- heap-sep/true-elim
is used by
Sep-weak-conjunction,
- heap-sep/true-rev
is used by
Sep-range,
- heap-sep/true-true
is used by
Sep-distribute-true,
Used from specification nat