Documentation

LeanPool.NFWeakPartition.Certificates.NominalWPPReplayChunk009StructuralBlock010

Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk009StructuralPart048.

source
noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNcfinraiselem2 (m n a b : SemanticCore.Var) (dv_a_b : a ≠ b) (dv_a_m : a ≠ m) (dv_a_n : a ≠ n) (dv_b_m : b ≠ m) (dv_b_n : b ≠ n) :
Nominal.NPrf (SemanticCore.Wff.classMem (SemanticCore.Class.cab m (Compiler.CompactSourceSyntax.synWral a (SemanticCore.Class.cv m) (Compiler.CompactSourceSyntax.synWral b (SemanticCore.Class.cv m) (Compiler.CompactSourceSyntax.synWrex n Compiler.CompactSourceSyntax.synCnnc (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCpw1 (SemanticCore.Class.cv a)) (SemanticCore.Class.cv n)) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCpw1 (SemanticCore.Class.cv b)) (SemanticCore.Class.cv n))))))) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_ncfinraiselem2.

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

    Certificates from NominalWPPReplayChunk009StructuralPart049.

    source
    noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNcfinraise (A B : SemanticCore.Class) (n : SemanticCore.Var) (M : SemanticCore.Class) (dv_A_n : n ∉ A.fv) (dv_B_n : n ∉ B.fv) :
    Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classMem M Compiler.CompactSourceSyntax.synCnnc) (SemanticCore.Wff.classMem A M) (SemanticCore.Wff.classMem B M)).imp (Compiler.CompactSourceSyntax.synWrex n Compiler.CompactSourceSyntax.synCnnc (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCpw1 A) (SemanticCore.Class.cv n)) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCpw1 B) (SemanticCore.Class.cv n)))))

    Checked nominal proof certificate identified upstream as g_ncfinraise.

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

      Certificates from NominalWPPReplayChunk009StructuralPart050.

      source
      noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNcfinlowerlem1 (m n a b : SemanticCore.Var) (dv_a_b : a ≠ b) (dv_a_m : a ≠ m) (dv_a_n : a ≠ n) (dv_b_m : b ≠ m) (dv_b_n : b ≠ n) (_dv_m_n : m ≠ n) :
      Nominal.NPrf (SemanticCore.Wff.classMem (SemanticCore.Class.cab m (SemanticCore.Wff.all a (SemanticCore.Wff.all b ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCpw1 (SemanticCore.Class.cv a)) (SemanticCore.Class.cv m)) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCpw1 (SemanticCore.Class.cv b)) (SemanticCore.Class.cv m))).imp (Compiler.CompactSourceSyntax.synWrex n Compiler.CompactSourceSyntax.synCnnc (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.objMem a n) (SemanticCore.Wff.objMem b n))))))) Compiler.CompactSourceSyntax.synCvv)

      Checked nominal proof certificate identified upstream as g_ncfinlowerlem1.

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