Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk009StructuralPart035.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNndisjeq (M N : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem M Compiler.CompactSourceSyntax.synCnnc) (SemanticCore.Wff.classMem N Compiler.CompactSourceSyntax.synCnnc)).imp (Compiler.CompactSourceSyntax.synWo (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin M N) Compiler.CompactSourceSyntax.synC0) (SemanticCore.Wff.classEq M N)))

Checked nominal proof certificate identified upstream as g_nndisjeq.

Equations

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

Certificates from NominalWPPReplayChunk009StructuralPart036.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNnceleq (A M N : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem M Compiler.CompactSourceSyntax.synCnnc) (SemanticCore.Wff.classMem N Compiler.CompactSourceSyntax.synCnnc)) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A M) (SemanticCore.Wff.classMem A N))).imp (SemanticCore.Wff.classEq M N))

Checked nominal proof certificate identified upstream as g_nnceleq.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOpklefing (x : SemanticCore.Var) (A B V W : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_B_x : x ∉ B.fv) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A V) (SemanticCore.Wff.classMem B W)).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk A B) Compiler.CompactSourceSyntax.synClefin) (Compiler.CompactSourceSyntax.synWrex x Compiler.CompactSourceSyntax.synCnnc (SemanticCore.Wff.classEq B (Compiler.CompactSourceSyntax.synCplc A (SemanticCore.Class.cv x))))))

Checked nominal proof certificate identified upstream as g_opklefing.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOpkltfing (x : SemanticCore.Var) (A B V W : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_B_x : x ∉ B.fv) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A V) (SemanticCore.Wff.classMem B W)).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk A B) Compiler.CompactSourceSyntax.synCltfin) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWne A Compiler.CompactSourceSyntax.synC0) (Compiler.CompactSourceSyntax.synWrex x Compiler.CompactSourceSyntax.synCnnc (SemanticCore.Wff.classEq B (Compiler.CompactSourceSyntax.synCplc (Compiler.CompactSourceSyntax.synCplc A (SemanticCore.Class.cv x)) Compiler.CompactSourceSyntax.synC1c))))))

Checked nominal proof certificate identified upstream as g_opkltfing.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLefinaddc (A N V : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A V) (SemanticCore.Wff.classMem N Compiler.CompactSourceSyntax.synCnnc)).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk A (Compiler.CompactSourceSyntax.synCplc A N)) Compiler.CompactSourceSyntax.synClefin))

Checked nominal proof certificate identified upstream as g_lefinaddc.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPrepeano4 (M N : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem M Compiler.CompactSourceSyntax.synCnnc) (SemanticCore.Wff.classMem N Compiler.CompactSourceSyntax.synCnnc)) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCplc M Compiler.CompactSourceSyntax.synC1c) (Compiler.CompactSourceSyntax.synCplc N Compiler.CompactSourceSyntax.synC1c)) (Compiler.CompactSourceSyntax.synWne (Compiler.CompactSourceSyntax.synCplc M Compiler.CompactSourceSyntax.synC1c) Compiler.CompactSourceSyntax.synC0))).imp (SemanticCore.Wff.classEq M N))

Checked nominal proof certificate identified upstream as g_prepeano4.

Equations

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

Certificates from NominalWPPReplayChunk009StructuralPart037.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAddcnul1 (A : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCplc A Compiler.CompactSourceSyntax.synC0) Compiler.CompactSourceSyntax.synC0)

Checked nominal proof certificate identified upstream as g_addcnul1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAddcnnul (A B : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWne (Compiler.CompactSourceSyntax.synCplc A B) Compiler.CompactSourceSyntax.synC0).imp (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWne A Compiler.CompactSourceSyntax.synC0) (Compiler.CompactSourceSyntax.synWne B Compiler.CompactSourceSyntax.synC0)))

Checked nominal proof certificate identified upstream as g_addcnnul.

Equations

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

Certificates from NominalWPPReplayChunk009StructuralPart038.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPreaddccan2lem1 (P : SemanticCore.Class) (m : SemanticCore.Var) (N : SemanticCore.Class) (dv_N_m : m ∉ N.fv) (dv_P_m : m ∉ P.fv) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem N Compiler.CompactSourceSyntax.synCnnc) (SemanticCore.Wff.classMem P Compiler.CompactSourceSyntax.synCnnc)).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cab m ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWne (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv m) N) Compiler.CompactSourceSyntax.synC0) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv m) N) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv m) P))).imp (SemanticCore.Wff.classEq N P))) Compiler.CompactSourceSyntax.synCvv))

Checked nominal proof certificate identified upstream as g_preaddccan2lem1.

Equations

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

Certificates from NominalWPPReplayChunk009StructuralPart039.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPreaddccan2 (P M N : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classMem M Compiler.CompactSourceSyntax.synCnnc) (SemanticCore.Wff.classMem N Compiler.CompactSourceSyntax.synCnnc) (SemanticCore.Wff.classMem P Compiler.CompactSourceSyntax.synCnnc)) (Compiler.CompactSourceSyntax.synWne (Compiler.CompactSourceSyntax.synCplc M N) Compiler.CompactSourceSyntax.synC0)).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCplc M N) (Compiler.CompactSourceSyntax.synCplc M P)) (SemanticCore.Wff.classEq N P)))

Checked nominal proof certificate identified upstream as g_preaddccan2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNulge (A V : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem Compiler.CompactSourceSyntax.synC0 Compiler.CompactSourceSyntax.synCnnc) (SemanticCore.Wff.classMem A V)).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk A Compiler.CompactSourceSyntax.synC0) Compiler.CompactSourceSyntax.synClefin))

Checked nominal proof certificate identified upstream as g_nulge.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLtfinirr (A : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCnnc).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk A A) Compiler.CompactSourceSyntax.synCltfin).neg)

Checked nominal proof certificate identified upstream as g_ltfinirr.

Equations

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

Certificates from NominalWPPReplayChunk009StructuralPart040.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLeltfintr (A B C : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCnnc) (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCnnc) (SemanticCore.Wff.classMem C Compiler.CompactSourceSyntax.synCnnc)).imp ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk A B) Compiler.CompactSourceSyntax.synClefin) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk B C) Compiler.CompactSourceSyntax.synCltfin)).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk A C) Compiler.CompactSourceSyntax.synCltfin)))

Checked nominal proof certificate identified upstream as g_leltfintr.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLtfintr (A B C : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCnnc) (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCnnc) (SemanticCore.Wff.classMem C Compiler.CompactSourceSyntax.synCnnc)).imp ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk A B) Compiler.CompactSourceSyntax.synCltfin) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk B C) Compiler.CompactSourceSyntax.synCltfin)).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk A C) Compiler.CompactSourceSyntax.synCltfin)))

Checked nominal proof certificate identified upstream as g_ltfintr.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLtfinasym (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.classMem (Compiler.CompactSourceSyntax.synCopk A B) Compiler.CompactSourceSyntax.synCltfin).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk B A) Compiler.CompactSourceSyntax.synCltfin).neg))

Checked nominal proof certificate identified upstream as g_ltfinasym.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN0cminle (A : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCnnc).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk Compiler.CompactSourceSyntax.synC0c A) Compiler.CompactSourceSyntax.synClefin))

Checked nominal proof certificate identified upstream as g_n_0cminle.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLtfinp1 (A V : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A V) (Compiler.CompactSourceSyntax.synWne A Compiler.CompactSourceSyntax.synC0)).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk A (Compiler.CompactSourceSyntax.synCplc A Compiler.CompactSourceSyntax.synC1c)) Compiler.CompactSourceSyntax.synCltfin))

Checked nominal proof certificate identified upstream as g_ltfinp1.

Equations

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