Documentation

LeanPool.NFWeakPartition.Certificates.NominalWPPReplayChunk010Compact001Block001

Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk010Compact001Part001.

source
noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOddnn (A : SemanticCore.Class) :
Nominal.NPrf ((SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCoddfin).imp (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCnnc))

Checked nominal proof certificate identified upstream as g_oddnn.

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

    Checked nominal proof certificate identified upstream as g_evennnul.

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

      Checked nominal proof certificate identified upstream as g_oddnnul.

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

        Checked nominal proof certificate identified upstream as g_sucevenodd.

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

          Checked nominal proof certificate identified upstream as g_sucoddeven.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDfevenfin2 (x n : SemanticCore.Var) (dv_n_x : n ≠ x) :
            Nominal.NPrf (SemanticCore.Wff.classEq Compiler.CompactSourceSyntax.synCevenfin (SemanticCore.Class.cab x (Compiler.CompactSourceSyntax.synWrex n Compiler.CompactSourceSyntax.synCnnc (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv n) (SemanticCore.Class.cv n))) (Compiler.CompactSourceSyntax.synWne (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv n) (SemanticCore.Class.cv n)) Compiler.CompactSourceSyntax.synC0)))))

            Checked nominal proof certificate identified upstream as g_dfevenfin2.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDfoddfin2 (x n : SemanticCore.Var) (dv_n_x : n ≠ x) :
              Nominal.NPrf (SemanticCore.Wff.classEq Compiler.CompactSourceSyntax.synCoddfin (SemanticCore.Class.cab x (Compiler.CompactSourceSyntax.synWrex n Compiler.CompactSourceSyntax.synCnnc (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) (Compiler.CompactSourceSyntax.synCplc (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv n) (SemanticCore.Class.cv n)) Compiler.CompactSourceSyntax.synC1c)) (Compiler.CompactSourceSyntax.synWne (Compiler.CompactSourceSyntax.synCplc (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv n) (SemanticCore.Class.cv n)) Compiler.CompactSourceSyntax.synC1c) Compiler.CompactSourceSyntax.synC0)))))

              Checked nominal proof certificate identified upstream as g_dfoddfin2.

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

                Certificates from NominalWPPReplayChunk010Compact001Part002.

                source
                noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEvenoddnnnul :
                Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCun Compiler.CompactSourceSyntax.synCevenfin Compiler.CompactSourceSyntax.synCoddfin) (Compiler.CompactSourceSyntax.synCdif Compiler.CompactSourceSyntax.synCnnc (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0)))

                Checked nominal proof certificate identified upstream as g_evenoddnnnul.

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