Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk013Compact001Part061.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCsucex (x : SemanticCore.Var) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCmpt x Compiler.CompactSourceSyntax.synCvv (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv x) Compiler.CompactSourceSyntax.synC1c)) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_csucex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBrcsuc (x : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_B_x : x ∉ B.fv) (hyp_brcsuc_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_brcsuc_2 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr A (Compiler.CompactSourceSyntax.synCmpt x Compiler.CompactSourceSyntax.synCvv (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv x) Compiler.CompactSourceSyntax.synC1c)) B) (SemanticCore.Wff.classEq B (Compiler.CompactSourceSyntax.synCplc A Compiler.CompactSourceSyntax.synC1c)))

Checked nominal proof certificate identified upstream as g_brcsuc.

Equations

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

Certificates from NominalWPPReplayChunk013Compact001Part062.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNncdiv3lem1 (n b : SemanticCore.Var) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv n) (SemanticCore.Class.cv b)) (Compiler.CompactSourceSyntax.synCrn (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCins3 (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCtxp (Compiler.CompactSourceSyntax.synCrn (Compiler.CompactSourceSyntax.synCtxp (Compiler.CompactSourceSyntax.synCcnv Compiler.CompactSourceSyntax.synC1st) (Compiler.CompactSourceSyntax.synCin Compiler.CompactSourceSyntax.synC1st Compiler.CompactSourceSyntax.synC2nd))) Compiler.CompactSourceSyntax.synC2nd) Compiler.CompactSourceSyntax.synCaddcfn))) (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCtxp (Compiler.CompactSourceSyntax.synCcom Compiler.CompactSourceSyntax.synC1st Compiler.CompactSourceSyntax.synC1st) (Compiler.CompactSourceSyntax.synCtxp (Compiler.CompactSourceSyntax.synCcom Compiler.CompactSourceSyntax.synC2nd Compiler.CompactSourceSyntax.synC1st) Compiler.CompactSourceSyntax.synC2nd)) Compiler.CompactSourceSyntax.synCaddcfn)))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv b) (Compiler.CompactSourceSyntax.synCplc (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv n) (SemanticCore.Class.cv n)) (SemanticCore.Class.cv n))))

Checked nominal proof certificate identified upstream as g_nncdiv3lem1.

Equations

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

Certificates from NominalWPPReplayChunk013Compact001Part063.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNncdiv3lem2 (n a : SemanticCore.Var) (dv_a_n : a ≠ n) : Nominal.NPrf (SemanticCore.Wff.classMem (SemanticCore.Class.cab a (Compiler.CompactSourceSyntax.synWrex n Compiler.CompactSourceSyntax.synCnnc (Compiler.CompactSourceSyntax.synW3o (SemanticCore.Wff.classEq (SemanticCore.Class.cv a) (Compiler.CompactSourceSyntax.synCplc (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv n) (SemanticCore.Class.cv n)) (SemanticCore.Class.cv n))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv a) (Compiler.CompactSourceSyntax.synCplc (Compiler.CompactSourceSyntax.synCplc (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv n) (SemanticCore.Class.cv n)) (SemanticCore.Class.cv n)) Compiler.CompactSourceSyntax.synC1c)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv a) (Compiler.CompactSourceSyntax.synCplc (Compiler.CompactSourceSyntax.synCplc (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv n) (SemanticCore.Class.cv n)) (SemanticCore.Class.cv n)) Compiler.CompactSourceSyntax.synC2c))))) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_nncdiv3lem2.

Equations

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

Certificates from NominalWPPReplayChunk013Compact001Part064.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNncdiv3 (A : SemanticCore.Class) (n : SemanticCore.Var) (dv_A_n : n ∉ A.fv) : Nominal.NPrf ((SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCnnc).imp (Compiler.CompactSourceSyntax.synWrex n Compiler.CompactSourceSyntax.synCnnc (Compiler.CompactSourceSyntax.synW3o (SemanticCore.Wff.classEq A (Compiler.CompactSourceSyntax.synCplc (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv n) (SemanticCore.Class.cv n)) (SemanticCore.Class.cv n))) (SemanticCore.Wff.classEq A (Compiler.CompactSourceSyntax.synCplc (Compiler.CompactSourceSyntax.synCplc (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv n) (SemanticCore.Class.cv n)) (SemanticCore.Class.cv n)) Compiler.CompactSourceSyntax.synC1c)) (SemanticCore.Wff.classEq A (Compiler.CompactSourceSyntax.synCplc (Compiler.CompactSourceSyntax.synCplc (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv n) (SemanticCore.Class.cv n)) (SemanticCore.Class.cv n)) Compiler.CompactSourceSyntax.synC2c)))))

Checked nominal proof certificate identified upstream as g_nncdiv3.

Equations

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