Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk011Compact001Part001.

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

Checked nominal proof certificate identified upstream as g_coeq2i.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gCoeq2i A B C hyp_coeq1i_1 = NFChoice.DirectNominalPrf.Nominal.mp hyp_coeq1i_1 (NFChoice.DirectNominalPrf.WPPReplay.gCoeq2 A B C)

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

Checked nominal proof certificate identified upstream as g_coeq1d.

Equations

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

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

Checked nominal proof certificate identified upstream as g_coeq2d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCoeq12i (A B C D : SemanticCore.Class) (hyp_coeq12i_1 : Nominal.NPrf (SemanticCore.Wff.classEq A B)) (hyp_coeq12i_2 : Nominal.NPrf (SemanticCore.Wff.classEq C D)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCcom A C) (Compiler.CompactSourceSyntax.synCcom B D))

Checked nominal proof certificate identified upstream as g_coeq12i.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCoeq12d (ph : SemanticCore.Wff) (A B C D : SemanticCore.Class) (hyp_coeq12d_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) (hyp_coeq12d_2 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq C D))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCcom A C) (Compiler.CompactSourceSyntax.synCcom B D)))

Checked nominal proof certificate identified upstream as g_coeq12d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBrco (x : SemanticCore.Var) (A B C D : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_B_x : x ∉ B.fv) (dv_C_x : x ∉ C.fv) (dv_D_x : x ∉ D.fv) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr A (Compiler.CompactSourceSyntax.synCcom C D) B) (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr A D (SemanticCore.Class.cv x)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv x) C B))))

Checked nominal proof certificate identified upstream as g_brco.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOpelco (x : SemanticCore.Var) (A B C D : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_B_x : x ∉ B.fv) (dv_C_x : x ∉ C.fv) (dv_D_x : x ∉ D.fv) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop A B) (Compiler.CompactSourceSyntax.synCcom C D)) (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr A D (SemanticCore.Class.cv x)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv x) C B))))

Checked nominal proof certificate identified upstream as g_opelco.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCnvss (A B : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWss A B).imp (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCcnv A) (Compiler.CompactSourceSyntax.synCcnv B)))

Checked nominal proof certificate identified upstream as g_cnvss.

Equations

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

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

Checked nominal proof certificate identified upstream as g_cnveq.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCnveqi (A B : SemanticCore.Class) (hyp_cnveqi_1 : Nominal.NPrf (SemanticCore.Wff.classEq A B)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCcnv A) (Compiler.CompactSourceSyntax.synCcnv B))

Checked nominal proof certificate identified upstream as g_cnveqi.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gCnveqi A B hyp_cnveqi_1 = NFChoice.DirectNominalPrf.Nominal.mp hyp_cnveqi_1 (NFChoice.DirectNominalPrf.WPPReplay.gCnveq A B)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCnveqd (ph : SemanticCore.Wff) (A B : SemanticCore.Class) (hyp_cnveqd_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCcnv A) (Compiler.CompactSourceSyntax.synCcnv B)))

Checked nominal proof certificate identified upstream as g_cnveqd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElcnv (x y : SemanticCore.Var) (A R : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_R_x : x ∉ R.fv) (dv_R_y : y ∉ R.fv) (dv_x_y : x ≠ y) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synCcnv R)) (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWex y (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classEq A (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv y) R (SemanticCore.Class.cv x))))))

Checked nominal proof certificate identified upstream as g_elcnv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElcnv2 (x y : SemanticCore.Var) (A R : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_R_x : x ∉ R.fv) (dv_R_y : y ∉ R.fv) (dv_x_y : x ≠ y) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synCcnv R)) (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWex y (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classEq A (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y))) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv y) (SemanticCore.Class.cv x)) R)))))

Checked nominal proof certificate identified upstream as g_elcnv2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBrcnv (A B R : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr A (Compiler.CompactSourceSyntax.synCcnv R) B) (Compiler.CompactSourceSyntax.synWbr B R A))

Checked nominal proof certificate identified upstream as g_brcnv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOpelcnv (A B R : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop A B) (Compiler.CompactSourceSyntax.synCcnv R)) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop B A) R))

Checked nominal proof certificate identified upstream as g_opelcnv.

Equations

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

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

Checked nominal proof certificate identified upstream as g_cnvco.

Equations

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

Certificates from NominalWPPReplayChunk011Compact001Part002.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCnvuni (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCuni A)) (Compiler.CompactSourceSyntax.synCiun x A (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv x))))

Checked nominal proof certificate identified upstream as g_cnvuni.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElrn (x : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_B_x : x ∉ B.fv) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synCrn B)) (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv x) B A)))

Checked nominal proof certificate identified upstream as g_elrn.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElrn2 (x : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_B_x : x ∉ B.fv) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synCrn B)) (Compiler.CompactSourceSyntax.synWex x (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) A) B)))

Checked nominal proof certificate identified upstream as g_elrn2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEldm (y : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_y : y ∉ A.fv) (dv_B_y : y ∉ B.fv) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synCdm B)) (Compiler.CompactSourceSyntax.synWex y (Compiler.CompactSourceSyntax.synWbr A B (SemanticCore.Class.cv y))))

Checked nominal proof certificate identified upstream as g_eldm.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEldm2 (y : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_y : y ∉ A.fv) (dv_B_y : y ∉ B.fv) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synCdm B)) (Compiler.CompactSourceSyntax.synWex y (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop A (SemanticCore.Class.cv y)) B)))

Checked nominal proof certificate identified upstream as g_eldm2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDfdm2 (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.synCdm A) (SemanticCore.Class.cab x (Compiler.CompactSourceSyntax.synWex y (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv x) A (SemanticCore.Class.cv y)))))

Checked nominal proof certificate identified upstream as g_dfdm2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDfdm3 (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.synCdm A) (SemanticCore.Class.cab x (Compiler.CompactSourceSyntax.synWex y (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) A))))

Checked nominal proof certificate identified upstream as g_dfdm3.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDfrn2 (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.synCrn A) (SemanticCore.Class.cab y (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv x) A (SemanticCore.Class.cv y)))))

Checked nominal proof certificate identified upstream as g_dfrn2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDfrn3 (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.synCrn A) (SemanticCore.Class.cab y (Compiler.CompactSourceSyntax.synWex x (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) A))))

Checked nominal proof certificate identified upstream as g_dfrn3.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDfrn4 (A : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCrn A) (Compiler.CompactSourceSyntax.synCdm (Compiler.CompactSourceSyntax.synCcnv A)))

Checked nominal proof certificate identified upstream as g_dfrn4.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDfdmf (x y : SemanticCore.Var) (A : SemanticCore.Class) (dv_x_y : x ≠ y) (hyp_dfdmf_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc x A)) (hyp_dfdmf_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc y A)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCdm A) (SemanticCore.Class.cab x (Compiler.CompactSourceSyntax.synWex y (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv x) A (SemanticCore.Class.cv y)))))

Checked nominal proof certificate identified upstream as g_dfdmf.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDmss (A B : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWss A B).imp (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCdm A) (Compiler.CompactSourceSyntax.synCdm B)))

Checked nominal proof certificate identified upstream as g_dmss.

Equations

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

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

Checked nominal proof certificate identified upstream as g_dmeq.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDmeqi (A B : SemanticCore.Class) (hyp_dmeqi_1 : Nominal.NPrf (SemanticCore.Wff.classEq A B)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCdm A) (Compiler.CompactSourceSyntax.synCdm B))

Checked nominal proof certificate identified upstream as g_dmeqi.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gDmeqi A B hyp_dmeqi_1 = NFChoice.DirectNominalPrf.Nominal.mp hyp_dmeqi_1 (NFChoice.DirectNominalPrf.WPPReplay.gDmeq A B)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDmeqd (ph : SemanticCore.Wff) (A B : SemanticCore.Class) (hyp_dmeqd_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCdm A) (Compiler.CompactSourceSyntax.synCdm B)))

Checked nominal proof certificate identified upstream as g_dmeqd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOpeldm (A B C : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop A B) C).imp (SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synCdm C)))

Checked nominal proof certificate identified upstream as g_opeldm.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBreldm (A B R : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWbr A R B).imp (SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synCdm R)))

Checked nominal proof certificate identified upstream as g_breldm.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDmun (A B : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCdm (Compiler.CompactSourceSyntax.synCun A B)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCdm A) (Compiler.CompactSourceSyntax.synCdm B)))

Checked nominal proof certificate identified upstream as g_dmun.

Equations

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

Certificates from NominalWPPReplayChunk011Compact001Part003.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDmuni (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCdm (Compiler.CompactSourceSyntax.synCuni A)) (Compiler.CompactSourceSyntax.synCiun x A (Compiler.CompactSourceSyntax.synCdm (SemanticCore.Class.cv x))))

Checked nominal proof certificate identified upstream as g_dmuni.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDmopab (ph : SemanticCore.Wff) (x y : SemanticCore.Var) (dv_x_y : x ≠ y) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCdm (Compiler.CompactSourceSyntax.synCopab x y ph)) (SemanticCore.Class.cab x (Compiler.CompactSourceSyntax.synWex y ph)))

Checked nominal proof certificate identified upstream as g_dmopab.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDmopab3 (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) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWral x A (Compiler.CompactSourceSyntax.synWex y ph)) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCdm (Compiler.CompactSourceSyntax.synCopab x y (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A) ph))) A))

Checked nominal proof certificate identified upstream as g_dmopab3.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDm0 : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCdm Compiler.CompactSourceSyntax.synC0) Compiler.CompactSourceSyntax.synC0)

Checked nominal proof certificate identified upstream as g_dm0.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDmi : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCdm Compiler.CompactSourceSyntax.synCid) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_dmi.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDm0rn0 (A : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCdm A) Compiler.CompactSourceSyntax.synC0) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCrn A) Compiler.CompactSourceSyntax.synC0))

Checked nominal proof certificate identified upstream as g_dm0rn0.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDmeq0 (A : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classEq A Compiler.CompactSourceSyntax.synC0) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCdm A) Compiler.CompactSourceSyntax.synC0))

Checked nominal proof certificate identified upstream as g_dmeq0.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDmxp (A B : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWne B Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCdm (Compiler.CompactSourceSyntax.synCxp A B)) A))

Checked nominal proof certificate identified upstream as g_dmxp.

Equations

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

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

Checked nominal proof certificate identified upstream as g_reseq1.

Equations

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

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

Checked nominal proof certificate identified upstream as g_reseq2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gReseq1i (A B C : SemanticCore.Class) (hyp_reseqi_1 : Nominal.NPrf (SemanticCore.Wff.classEq A B)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCres A C) (Compiler.CompactSourceSyntax.synCres B C))

Checked nominal proof certificate identified upstream as g_reseq1i.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gReseq1i A B C hyp_reseqi_1 = NFChoice.DirectNominalPrf.Nominal.mp hyp_reseqi_1 (NFChoice.DirectNominalPrf.WPPReplay.gReseq1 A B C)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gReseq2i (A B C : SemanticCore.Class) (hyp_reseqi_1 : Nominal.NPrf (SemanticCore.Wff.classEq A B)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCres C A) (Compiler.CompactSourceSyntax.synCres C B))

Checked nominal proof certificate identified upstream as g_reseq2i.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gReseq2i A B C hyp_reseqi_1 = NFChoice.DirectNominalPrf.Nominal.mp hyp_reseqi_1 (NFChoice.DirectNominalPrf.WPPReplay.gReseq2 A B C)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gReseq12i (A B C D : SemanticCore.Class) (hyp_reseqi_1 : Nominal.NPrf (SemanticCore.Wff.classEq A B)) (hyp_reseqi_2 : Nominal.NPrf (SemanticCore.Wff.classEq C D)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCres A C) (Compiler.CompactSourceSyntax.synCres B D))

Checked nominal proof certificate identified upstream as g_reseq12i.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gReseq2d (ph : SemanticCore.Wff) (A B C : SemanticCore.Class) (hyp_reseqd_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCres C A) (Compiler.CompactSourceSyntax.synCres C B)))

Checked nominal proof certificate identified upstream as g_reseq2d.

Equations

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

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

Checked nominal proof certificate identified upstream as g_imaeq1.

Equations

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

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

Checked nominal proof certificate identified upstream as g_imaeq2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gImaeq1i (A B C : SemanticCore.Class) (hyp_imaeq1i_1 : Nominal.NPrf (SemanticCore.Wff.classEq A B)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCima A C) (Compiler.CompactSourceSyntax.synCima B C))

Checked nominal proof certificate identified upstream as g_imaeq1i.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gImaeq1i A B C hyp_imaeq1i_1 = NFChoice.DirectNominalPrf.Nominal.mp hyp_imaeq1i_1 (NFChoice.DirectNominalPrf.WPPReplay.gImaeq1 A B C)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gImaeq2i (A B C : SemanticCore.Class) (hyp_imaeq1i_1 : Nominal.NPrf (SemanticCore.Wff.classEq A B)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCima C A) (Compiler.CompactSourceSyntax.synCima C B))

Checked nominal proof certificate identified upstream as g_imaeq2i.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gImaeq2i A B C hyp_imaeq1i_1 = NFChoice.DirectNominalPrf.Nominal.mp hyp_imaeq1i_1 (NFChoice.DirectNominalPrf.WPPReplay.gImaeq2 A B C)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gImaeq1d (ph : SemanticCore.Wff) (A B C : SemanticCore.Class) (hyp_imaeq1d_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCima A C) (Compiler.CompactSourceSyntax.synCima B C)))

Checked nominal proof certificate identified upstream as g_imaeq1d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gImaeq2d (ph : SemanticCore.Wff) (A B C : SemanticCore.Class) (hyp_imaeq1d_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCima C A) (Compiler.CompactSourceSyntax.synCima C B)))

Checked nominal proof certificate identified upstream as g_imaeq2d.

Equations

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

Certificates from NominalWPPReplayChunk011Compact001Part004.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElimapw1 (x : SemanticCore.Var) (A B C : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_B_x : x ∉ B.fv) (dv_C_x : x ∉ C.fv) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synCima B (Compiler.CompactSourceSyntax.synCpw1 C))) (Compiler.CompactSourceSyntax.synWrex x C (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)) A) B)))

Checked nominal proof certificate identified upstream as g_elimapw1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElimapw12 (x : SemanticCore.Var) (A B C : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_B_x : x ∉ B.fv) (dv_C_x : x ∉ C.fv) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synCima B (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 C)))) (Compiler.CompactSourceSyntax.synWrex x C (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x))) A) B)))

Checked nominal proof certificate identified upstream as g_elimapw12.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElima1c (x : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_B_x : x ∉ B.fv) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synCima B Compiler.CompactSourceSyntax.synC1c)) (Compiler.CompactSourceSyntax.synWex x (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)) A) B)))

Checked nominal proof certificate identified upstream as g_elima1c.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElimapw11c (x : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_B_x : x ∉ B.fv) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synCima B (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synC1c))) (Compiler.CompactSourceSyntax.synWex x (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x))) A) B)))

Checked nominal proof certificate identified upstream as g_elimapw11c.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBrres (A B C D : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr A (Compiler.CompactSourceSyntax.synCres C D) B) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr A C B) (SemanticCore.Wff.classMem A D)))

Checked nominal proof certificate identified upstream as g_brres.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOpelres (A B C D : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop A B) (Compiler.CompactSourceSyntax.synCres C D)) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop A B) C) (SemanticCore.Wff.classMem A D)))

Checked nominal proof certificate identified upstream as g_opelres.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDfima3 (A B : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCima A B) (Compiler.CompactSourceSyntax.synCrn (Compiler.CompactSourceSyntax.synCres A B)))

Checked nominal proof certificate identified upstream as g_dfima3.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDfima4 (x y : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_B_x : x ∉ B.fv) (dv_B_y : y ∉ B.fv) (dv_x_y : x ≠ y) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCima A B) (SemanticCore.Class.cab y (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) B) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) A)))))

Checked nominal proof certificate identified upstream as g_dfima4.

Equations

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

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

Checked nominal proof certificate identified upstream as g_rneq.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRneqi (A B : SemanticCore.Class) (hyp_rneqi_1 : Nominal.NPrf (SemanticCore.Wff.classEq A B)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCrn A) (Compiler.CompactSourceSyntax.synCrn B))

Checked nominal proof certificate identified upstream as g_rneqi.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gRneqi A B hyp_rneqi_1 = NFChoice.DirectNominalPrf.Nominal.mp hyp_rneqi_1 (NFChoice.DirectNominalPrf.WPPReplay.gRneq A B)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRneqd (ph : SemanticCore.Wff) (A B : SemanticCore.Class) (hyp_rneqd_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCrn A) (Compiler.CompactSourceSyntax.synCrn B)))

Checked nominal proof certificate identified upstream as g_rneqd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRnss (A B : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWss A B).imp (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn A) (Compiler.CompactSourceSyntax.synCrn B)))

Checked nominal proof certificate identified upstream as g_rnss.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBrelrn (A B C : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWbr A C B).imp (SemanticCore.Wff.classMem B (Compiler.CompactSourceSyntax.synCrn C)))

Checked nominal proof certificate identified upstream as g_brelrn.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOpelrn (A B C : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop A B) C).imp (SemanticCore.Wff.classMem B (Compiler.CompactSourceSyntax.synCrn C)))

Checked nominal proof certificate identified upstream as g_opelrn.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDfrnf (x y : SemanticCore.Var) (A : SemanticCore.Class) (dv_x_y : x ≠ y) (hyp_dfrnf_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc x A)) (hyp_dfrnf_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc y A)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCrn A) (SemanticCore.Class.cab y (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv x) A (SemanticCore.Class.cv y)))))

Checked nominal proof certificate identified upstream as g_dfrnf.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRnopab (ph : SemanticCore.Wff) (x y : SemanticCore.Var) (dv_x_y : x ≠ y) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCrn (Compiler.CompactSourceSyntax.synCopab x y ph)) (SemanticCore.Class.cab y (Compiler.CompactSourceSyntax.synWex x ph)))

Checked nominal proof certificate identified upstream as g_rnopab.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRnopab2 (x y : SemanticCore.Var) (A B : SemanticCore.Class) (dv_x_y : x ≠ y) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCrn (Compiler.CompactSourceSyntax.synCopab x y (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A) (SemanticCore.Wff.classEq (SemanticCore.Class.cv y) B)))) (SemanticCore.Class.cab y (Compiler.CompactSourceSyntax.synWrex x A (SemanticCore.Wff.classEq (SemanticCore.Class.cv y) B))))

Checked nominal proof certificate identified upstream as g_rnopab2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRn0 : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCrn Compiler.CompactSourceSyntax.synC0) Compiler.CompactSourceSyntax.synC0)

Checked nominal proof certificate identified upstream as g_rn0.

Equations

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