Documentation

LeanPool.NFWeakPartition.Certificates.NominalWPPReplayChunk010Compact001Block009

Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk010Compact001Part023.

source
noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gVfinspsslem1 (x z n : SemanticCore.Var) (_dv_n_x : n ≠ x) (_dv_n_z : n ≠ z) (dv_x_z : x ≠ z) :
Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem Compiler.CompactSourceSyntax.synCvv Compiler.CompactSourceSyntax.synCfin) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCtfin (SemanticCore.Class.cv n)) Compiler.CompactSourceSyntax.synCspfin)) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv n) Compiler.CompactSourceSyntax.synCspfin) (Compiler.CompactSourceSyntax.synWsfin (SemanticCore.Class.cv z) (Compiler.CompactSourceSyntax.synCtfin (SemanticCore.Class.cv n))))).imp (Compiler.CompactSourceSyntax.synWrex x Compiler.CompactSourceSyntax.synCspfin (SemanticCore.Wff.classEq (SemanticCore.Class.cv z) (Compiler.CompactSourceSyntax.synCtfin (SemanticCore.Class.cv x)))))

Checked nominal proof certificate identified upstream as g_vfinspsslem1.

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

    Certificates from NominalWPPReplayChunk010Compact001Part024.

    source
    noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gVfinspss (x a : SemanticCore.Var) (dv_a_x : a ≠ x) :
    Nominal.NPrf ((SemanticCore.Wff.classMem Compiler.CompactSourceSyntax.synCvv Compiler.CompactSourceSyntax.synCfin).imp (Compiler.CompactSourceSyntax.synWss Compiler.CompactSourceSyntax.synCspfin (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cab a (Compiler.CompactSourceSyntax.synWrex x Compiler.CompactSourceSyntax.synCspfin (SemanticCore.Wff.classEq (SemanticCore.Class.cv a) (Compiler.CompactSourceSyntax.synCtfin (SemanticCore.Class.cv x))))) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCncfin Compiler.CompactSourceSyntax.synCvv)))))

    Checked nominal proof certificate identified upstream as g_vfinspss.

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

      Certificates from NominalWPPReplayChunk010Compact001Part025.

      source
      noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gVfinspclt (X : SemanticCore.Class) :
      Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem Compiler.CompactSourceSyntax.synCvv Compiler.CompactSourceSyntax.synCfin) (SemanticCore.Wff.classMem X Compiler.CompactSourceSyntax.synCspfin)).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCtfin X) Compiler.CompactSourceSyntax.synCspfin))

      Checked nominal proof certificate identified upstream as g_vfinspclt.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gVfinspeqtncv (x a : SemanticCore.Var) (dv_a_x : a ≠ x) :
        Nominal.NPrf ((SemanticCore.Wff.classMem Compiler.CompactSourceSyntax.synCvv Compiler.CompactSourceSyntax.synCfin).imp (SemanticCore.Wff.classEq Compiler.CompactSourceSyntax.synCspfin (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cab a (Compiler.CompactSourceSyntax.synWrex x Compiler.CompactSourceSyntax.synCspfin (SemanticCore.Wff.classEq (SemanticCore.Class.cv a) (Compiler.CompactSourceSyntax.synCtfin (SemanticCore.Class.cv x))))) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCncfin Compiler.CompactSourceSyntax.synCvv)))))

        Checked nominal proof certificate identified upstream as g_vfinspeqtncv.

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