Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk010Compact001Part065.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBrswap2 (A B C : SemanticCore.Class) (hyp_br1st_1 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) (hyp_brswap_2 : Nominal.NPrf (SemanticCore.Wff.classMem C Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr A Compiler.CompactSourceSyntax.synCswap (Compiler.CompactSourceSyntax.synCop B C)) (SemanticCore.Wff.classEq A (Compiler.CompactSourceSyntax.synCop C B)))

Checked nominal proof certificate identified upstream as g_brswap2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOpabid2 (x y : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_x_y : x ≠ y) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCopab x y (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) A)) A)

Checked nominal proof certificate identified upstream as g_opabid2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gInopab (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) (dv_x_y : x ≠ y) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCopab x y ph) (Compiler.CompactSourceSyntax.synCopab x y ps)) (Compiler.CompactSourceSyntax.synCopab x y (Compiler.CompactSourceSyntax.synWa ph ps)))

Checked nominal proof certificate identified upstream as g_inopab.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gInxp (A B C D : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCxp A B) (Compiler.CompactSourceSyntax.synCxp C D)) (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCin A C) (Compiler.CompactSourceSyntax.synCin B D)))

Checked nominal proof certificate identified upstream as g_inxp.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOpabbi2i (ph : SemanticCore.Wff) (x y : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_x_y : x ≠ y) (hyp_opabbi2i_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) A) ph)) : Nominal.NPrf (SemanticCore.Wff.classEq A (Compiler.CompactSourceSyntax.synCopab x y ph))

Checked nominal proof certificate identified upstream as g_opabbi2i.

Equations

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

Certificates from NominalWPPReplayChunk010Compact001Part066.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIdeqg (A B V : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem B V).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr A Compiler.CompactSourceSyntax.synCid B) (SemanticCore.Wff.classEq A B)))

Checked nominal proof certificate identified upstream as g_ideqg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIdeq (A B : SemanticCore.Class) (hyp_ideq_1 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr A Compiler.CompactSourceSyntax.synCid B) (SemanticCore.Wff.classEq A B))

Checked nominal proof certificate identified upstream as g_ideq.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIdidg (A V : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem A V).imp (Compiler.CompactSourceSyntax.synWbr A Compiler.CompactSourceSyntax.synCid A))

Checked nominal proof certificate identified upstream as g_ididg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCoss1 (A B C : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWss A B).imp (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCcom A C) (Compiler.CompactSourceSyntax.synCcom B C)))

Checked nominal proof certificate identified upstream as g_coss1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCoss2 (A B C : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWss A B).imp (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCcom C A) (Compiler.CompactSourceSyntax.synCcom C B)))

Checked nominal proof certificate identified upstream as g_coss2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCoeq1 (A B C : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classEq A B).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCcom A C) (Compiler.CompactSourceSyntax.synCcom B C)))

Checked nominal proof certificate identified upstream as g_coeq1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCoeq2 (A B C : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classEq A B).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCcom C A) (Compiler.CompactSourceSyntax.synCcom C B)))

Checked nominal proof certificate identified upstream as g_coeq2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCoeq1i (A B C : SemanticCore.Class) (hyp_coeq1i_1 : Nominal.NPrf (SemanticCore.Wff.classEq A B)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCcom A C) (Compiler.CompactSourceSyntax.synCcom B C))

Checked nominal proof certificate identified upstream as g_coeq1i.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gCoeq1i A B C hyp_coeq1i_1 = NFChoice.DirectNominalPrf.Nominal.mp hyp_coeq1i_1 (NFChoice.DirectNominalPrf.WPPReplay.gCoeq1 A B C)