package mizar
Ordering
- Alphabetic
Visibility
- Public
- All
Value Members
-
object
IntroduceEquivalence extends RewriteRule with ComplificationRule
(X implies Y) and (Y implies X) ---> X equiv Y
-
object
IntroduceExistential extends TermTransformationRule with ComplificationRule
not forall x.
not forall x. not P(x) ---> exists x. P(x)
this cannot be a RewriteRule because HOAS matching cannot match for the name of the bound variable so we use basic Scala matching instead
-
object
IntroduceImplication extends TermTransformationRule with ComplificationRule
not and(X1,...,Xm, not Y1,...,not Yn) ---> and X implies or Y not and (not Y1,..., not Yn) ---> or Y
not and(X1,...,Xm, not Y1,...,not Yn) ---> and X implies or Y not and (not Y1,..., not Yn) ---> or Y
this cannot easily be a rewrite rule because m and n can be arbitrary
- object IntroductionRule
- object MizarPatterns extends RealizedTheory