Packages

package mizar

Ordering
  1. Alphabetic
Visibility
  1. Public
  2. All

Value Members

  1. object IntroduceEquivalence extends RewriteRule with ComplificationRule

    (X implies Y) and (Y implies X) ---> X equiv Y

  2. 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

  3. 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

  4. object IntroductionRule
  5. object MizarPatterns extends RealizedTheory

Ungrouped