Documentation

LeanPool.NFWeakPartition.Certificates.NominalWPPReplayChunk013Compact001Block014

Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk013Compact001Part065.

source
noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNnc3n3p1 (A B : SemanticCore.Class) :
Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCnnc) (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCnnc)).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCplc (Compiler.CompactSourceSyntax.synCplc A A) A) (Compiler.CompactSourceSyntax.synCplc (Compiler.CompactSourceSyntax.synCplc (Compiler.CompactSourceSyntax.synCplc B B) B) Compiler.CompactSourceSyntax.synC1c)).neg)

Checked nominal proof certificate identified upstream as g_nnc3n3p1.

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

    Certificates from NominalWPPReplayChunk013Compact001Part066.

    source
    noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNnc3n3p2 (A B : SemanticCore.Class) :
    Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCnnc) (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCnnc)).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCplc (Compiler.CompactSourceSyntax.synCplc A A) A) (Compiler.CompactSourceSyntax.synCplc (Compiler.CompactSourceSyntax.synCplc (Compiler.CompactSourceSyntax.synCplc B B) B) Compiler.CompactSourceSyntax.synC2c)).neg)

    Checked nominal proof certificate identified upstream as g_nnc3n3p2.

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

      Checked nominal proof certificate identified upstream as g_nchoicelem1.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFreceq12 (F G I J : SemanticCore.Class) :
        Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classEq F G) (SemanticCore.Wff.classEq I J)).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfrec F I) (Compiler.CompactSourceSyntax.synCfrec G J)))

        Checked nominal proof certificate identified upstream as g_freceq12.

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