Documentation

LeanPool.NFWeakPartition.Certificates.NominalWPPReplayChunk010Compact001Block002

Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk010Compact001Part004.

source
noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEvenodddisj :
Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin Compiler.CompactSourceSyntax.synCevenfin Compiler.CompactSourceSyntax.synCoddfin) Compiler.CompactSourceSyntax.synC0)

Checked nominal proof certificate identified upstream as g_evenodddisj.

Equations
  • One or more equations did not get rendered due to their size.
Instances For

    Certificates from NominalWPPReplayChunk010Compact001Part005.

    source
    noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEventfin (M : SemanticCore.Class) :
    Nominal.NPrf ((SemanticCore.Wff.classMem M Compiler.CompactSourceSyntax.synCevenfin).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCtfin M) Compiler.CompactSourceSyntax.synCevenfin))

    Checked nominal proof certificate identified upstream as g_eventfin.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOddtfin (M : SemanticCore.Class) :
      Nominal.NPrf ((SemanticCore.Wff.classMem M Compiler.CompactSourceSyntax.synCoddfin).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCtfin M) Compiler.CompactSourceSyntax.synCoddfin))

      Checked nominal proof certificate identified upstream as g_oddtfin.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For