Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk010Compact001Part034.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPhi011lem1 (A B : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi A) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi B) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))).imp (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCphi A) (Compiler.CompactSourceSyntax.synCphi B)))

Checked nominal proof certificate identified upstream as g_phi011lem1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPhi011 (A B : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classEq A B) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi A) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi B) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))

Checked nominal proof certificate identified upstream as g_phi011.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gProj1op (A B : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCproj1 (Compiler.CompactSourceSyntax.synCop A B)) A)

Checked nominal proof certificate identified upstream as g_proj1op.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gProj2op (A B : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCproj2 (Compiler.CompactSourceSyntax.synCop A B)) B)

Checked nominal proof certificate identified upstream as g_proj2op.

Equations

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

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

Checked nominal proof certificate identified upstream as g_opth.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOpexb (A B : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop A B) Compiler.CompactSourceSyntax.synCvv) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv) (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)))

Checked nominal proof certificate identified upstream as g_opexb.

Equations

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

Certificates from NominalWPPReplayChunk010Compact001Part035.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfop (x : SemanticCore.Var) (A B : SemanticCore.Class) (hyp_nfop_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc x A)) (hyp_nfop_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc x B)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc x (Compiler.CompactSourceSyntax.synCop A B))

Checked nominal proof certificate identified upstream as g_nfop.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfopd (ph : SemanticCore.Wff) (x : SemanticCore.Var) (A B : SemanticCore.Class) (hyp_nfopd_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWnfc x A))) (hyp_nfopd_2 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWnfc x B))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWnfc x (Compiler.CompactSourceSyntax.synCop A B)))

Checked nominal proof certificate identified upstream as g_nfopd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEqvinop (x y : SemanticCore.Var) (A B C : 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_C_x : x ∉ C.fv) (dv_C_y : y ∉ C.fv) (dv_x_y : x ≠ y) (hyp_eqvinop_1 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) (hyp_eqvinop_2 : Nominal.NPrf (SemanticCore.Wff.classMem C Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classEq A (Compiler.CompactSourceSyntax.synCop B C)) (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.classEq (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synCop B C))))))

Checked nominal proof certificate identified upstream as g_eqvinop.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCopsexg (ph : SemanticCore.Wff) (x y : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) : Nominal.NPrf ((SemanticCore.Wff.classEq A (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y))).imp (Compiler.CompactSourceSyntax.synWb ph (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))) ph)))))

Checked nominal proof certificate identified upstream as g_copsexg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCopsex2g (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) (A B V W : 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_ps_x : x ∉ ps.fv) (dv_ps_y : y ∉ ps.fv) (dv_x_y : x ≠ y) (hyp_copsex2g_1 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A) (SemanticCore.Wff.classEq (SemanticCore.Class.cv y) B)).imp (Compiler.CompactSourceSyntax.synWb ph ps))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A V) (SemanticCore.Wff.classMem B W)).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWex y (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCop A B) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y))) ph))) ps))

Checked nominal proof certificate identified upstream as g_copsex2g.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEqop (z t : SemanticCore.Var) (A B C : SemanticCore.Class) (_dv_A_t : t ∉ A.fv) (dv_A_z : z ∉ A.fv) (dv_B_t : t ∉ B.fv) (dv_B_z : z ∉ B.fv) (dv_C_t : t ∉ C.fv) (dv_C_z : z ∉ C.fv) (dv_t_z : t ≠ z) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classEq A (Compiler.CompactSourceSyntax.synCop B C)) (SemanticCore.Wff.all z (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (SemanticCore.Class.cv z) A) (Compiler.CompactSourceSyntax.synWo (Compiler.CompactSourceSyntax.synWrex t B (SemanticCore.Wff.classEq (SemanticCore.Class.cv z) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv t)))) (Compiler.CompactSourceSyntax.synWrex t C (SemanticCore.Wff.classEq (SemanticCore.Class.cv z) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv t)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))))))

Checked nominal proof certificate identified upstream as g_eqop.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMosubopt (ph : SemanticCore.Wff) (x y z : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_A_z : z ∉ A.fv) (dv_x_y : x ≠ y) (dv_x_z : x ≠ z) (_dv_y_z : y ≠ z) : Nominal.NPrf ((SemanticCore.Wff.all y (SemanticCore.Wff.all z (Compiler.CompactSourceSyntax.synWmo x ph))).imp (Compiler.CompactSourceSyntax.synWmo x (Compiler.CompactSourceSyntax.synWex y (Compiler.CompactSourceSyntax.synWex z (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classEq A (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv y) (SemanticCore.Class.cv z))) ph)))))

Checked nominal proof certificate identified upstream as g_mosubopt.

Equations

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

Certificates from NominalWPPReplayChunk010Compact001Part036.

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

Checked nominal proof certificate identified upstream as g_phiun.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPhidisjnn (A : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin A Compiler.CompactSourceSyntax.synCnnc) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCphi A) A))

Checked nominal proof certificate identified upstream as g_phidisjnn.

Equations

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

Certificates from NominalWPPReplayChunk010Compact001Part037.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPhialllem1 (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (hyp_phiall_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWss A Compiler.CompactSourceSyntax.synCnnc) (SemanticCore.Wff.classMem Compiler.CompactSourceSyntax.synC0c A).neg).imp (Compiler.CompactSourceSyntax.synWex x (SemanticCore.Wff.classEq A (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv x)))))

Checked nominal proof certificate identified upstream as g_phialllem1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPhialllem2 (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (hyp_phiall_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((SemanticCore.Wff.classMem Compiler.CompactSourceSyntax.synC0c A).neg.imp (Compiler.CompactSourceSyntax.synWex x (SemanticCore.Wff.classEq A (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv x)))))

Checked nominal proof certificate identified upstream as g_phialllem2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPhiall (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (hyp_phiall_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWo (SemanticCore.Wff.classEq A (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv x))) (SemanticCore.Wff.classEq A (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv x)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))

Checked nominal proof certificate identified upstream as g_phiall.

Equations

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

Certificates from NominalWPPReplayChunk010Compact001Part038.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOpeq (A : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq A (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCproj1 A) (Compiler.CompactSourceSyntax.synCproj2 A)))

Checked nominal proof certificate identified upstream as g_opeq.

Equations

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

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

Checked nominal proof certificate identified upstream as g_opeqexb.

Equations

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

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

Checked nominal proof certificate identified upstream as g_opeqex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOpabbid (ph ps ch : SemanticCore.Wff) (x y : SemanticCore.Var) (hyp_opabbid_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ph)) (hyp_opabbid_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf y ph)) (hyp_opabbid_3 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCopab x y ps) (Compiler.CompactSourceSyntax.synCopab x y ch)))

Checked nominal proof certificate identified upstream as g_opabbid.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOpabbidv (ph ps ch : SemanticCore.Wff) (x y : SemanticCore.Var) (dv_ph_x : x ∉ ph.fv) (dv_ph_y : y ∉ ph.fv) (hyp_opabbidv_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCopab x y ps) (Compiler.CompactSourceSyntax.synCopab x y ch)))

Checked nominal proof certificate identified upstream as g_opabbidv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOpabbii (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) (hyp_opabbii_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph ps)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCopab x y ph) (Compiler.CompactSourceSyntax.synCopab x y ps))

Checked nominal proof certificate identified upstream as g_opabbii.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfopab (ph : SemanticCore.Wff) (x y z : SemanticCore.Var) (dv_x_z : x ≠ z) (dv_y_z : y ≠ z) (hyp_nfopab_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf z ph)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc z (Compiler.CompactSourceSyntax.synCopab x y ph))

Checked nominal proof certificate identified upstream as g_nfopab.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfopab1 (ph : SemanticCore.Wff) (x y : SemanticCore.Var) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc x (Compiler.CompactSourceSyntax.synCopab x y ph))

Checked nominal proof certificate identified upstream as g_nfopab1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfopab2 (ph : SemanticCore.Wff) (x y : SemanticCore.Var) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc y (Compiler.CompactSourceSyntax.synCopab x y ph))

Checked nominal proof certificate identified upstream as g_nfopab2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCbvopab1 (ph ps : SemanticCore.Wff) (x y z : SemanticCore.Var) (dv_x_y : x ≠ y) (dv_y_z : y ≠ z) (hyp_cbvopab1_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf z ph)) (hyp_cbvopab1_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ps)) (hyp_cbvopab1_3 : Nominal.NPrf ((SemanticCore.Wff.objEq x z).imp (Compiler.CompactSourceSyntax.synWb ph ps))) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCopab x y ph) (Compiler.CompactSourceSyntax.synCopab z y ps))

Checked nominal proof certificate identified upstream as g_cbvopab1.

Equations

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