Documentation

LeanPool.NFWeakPartition.Certificates.NominalWPPReplayChunk017Compact001Block006

Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk017Compact001Part025.

source
noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHncodecmpsetconnexndv (A : SemanticCore.Class) :
Nominal.NPrf ((SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv).imp (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synChncodecmpset A) Compiler.CompactSourceSyntax.synCconnex (Compiler.CompactSourceSyntax.synChwcn A)))

Checked nominal proof certificate identified upstream as g_hncodecmpsetconnexndv.

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

    Certificates from NominalWPPReplayChunk017Compact001Part026.

    source
    noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnwcutcodenestndv (x y : SemanticCore.Var) (D R : SemanticCore.Class) :
    Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D) (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) D)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv y)))))).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synChnwcutcode (Compiler.CompactSourceSyntax.synCin R (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv y)))) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv y)))))) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv y)))) (SemanticCore.Class.cv x)) (Compiler.CompactSourceSyntax.synChnwcutcode R D (SemanticCore.Class.cv x))))

    Checked nominal proof certificate identified upstream as g_hnwcutcodenestndv.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnwcutcodeeq12ndv (x : SemanticCore.Var) (D R S E : SemanticCore.Class) :
      Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classEq R S) (SemanticCore.Wff.classEq D E)).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synChnwcutcode R D (SemanticCore.Class.cv x)) (Compiler.CompactSourceSyntax.synChnwcutcode S E (SemanticCore.Class.cv x))))

      Checked nominal proof certificate identified upstream as g_hnwcutcodeeq12ndv.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnwcutcodeambientndv (x u : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_u : u ∉ A.fv) :
        Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn A)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synChnwcutcode (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)) (SemanticCore.Class.cv x)) (Compiler.CompactSourceSyntax.synChwcn A)))

        Checked nominal proof certificate identified upstream as g_hnwcutcodeambientndv.

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