Documentation

LeanPool.NFWeakPartition.Certificates.NominalWPPReplayChunk009StructuralBlock008

Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk009StructuralPart041.

source
noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLefinlteq (A B V W : SemanticCore.Class) :
Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classMem A V) (SemanticCore.Wff.classMem B W) (Compiler.CompactSourceSyntax.synWne A Compiler.CompactSourceSyntax.synC0)).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk A B) Compiler.CompactSourceSyntax.synClefin) (Compiler.CompactSourceSyntax.synWo (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk A B) Compiler.CompactSourceSyntax.synCltfin) (SemanticCore.Wff.classEq A B))))

Checked nominal proof certificate identified upstream as g_lefinlteq.

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

    Certificates from NominalWPPReplayChunk009StructuralPart042.

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

    Checked nominal proof certificate identified upstream as g_ltfinex.

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

      Certificates from NominalWPPReplayChunk009StructuralPart043.

      source
      noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLtfintrilem1 (m n : SemanticCore.Var) (dv_m_n : m ≠ n) :
      Nominal.NPrf (SemanticCore.Wff.classMem (SemanticCore.Class.cab m ((SemanticCore.Wff.classMem (SemanticCore.Class.cv n) Compiler.CompactSourceSyntax.synCnnc).imp ((Compiler.CompactSourceSyntax.synWne (SemanticCore.Class.cv m) Compiler.CompactSourceSyntax.synC0).imp (Compiler.CompactSourceSyntax.synW3o (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk (SemanticCore.Class.cv m) (SemanticCore.Class.cv n)) Compiler.CompactSourceSyntax.synCltfin) (SemanticCore.Wff.objEq m n) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk (SemanticCore.Class.cv n) (SemanticCore.Class.cv m)) Compiler.CompactSourceSyntax.synCltfin))))) Compiler.CompactSourceSyntax.synCvv)

      Checked nominal proof certificate identified upstream as g_ltfintrilem1.

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