[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
- monotone-set-fixpoint/fixpoint
is used by
iterate-subseq-mu,
- monotone-set-fixpoint/least-prefixpoint-def
is used by
iterate-is-fix,
- monotone-set-fixpoint/monotone-def
is used by
iterate-subseq-mu,
iterate-subseq-leq,
iterate-subseq,
cont-monotone,
- monotone-set-fixpoint/subseteq-def
is used by
iterate-subseq-mu,
iterate-subseq-leq,
iterate-subseq,
iterate-is-fix,
cont-monotone,
- monotone-set-fixpoint/subset-refl
is used by
cont-monotone,
Used from specification nat
Used from specification nat-basic2
Used from specification nat-basic1