Documentation

LeanPool.NFWeakPartition.Certificates.NominalWPPReplayChunk009StructuralBlock013

Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk009StructuralPart059.

source
noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOddfinex :
Nominal.NPrf (SemanticCore.Wff.classMem Compiler.CompactSourceSyntax.synCoddfin Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_oddfinex.

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

    Certificates from NominalWPPReplayChunk009StructuralPart060.

    source
    noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN0ceven :
    Nominal.NPrf (SemanticCore.Wff.classMem Compiler.CompactSourceSyntax.synC0c Compiler.CompactSourceSyntax.synCevenfin)

    Checked nominal proof certificate identified upstream as g_n_0ceven.

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

      Checked nominal proof certificate identified upstream as g_evennn.

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