Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk013Compact001Part039.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEnprmaplem3 (x y : SemanticCore.Var) (A B W : SemanticCore.Class) (r : SemanticCore.Var) (dv_A_r : r ∉ A.fv) (dv_B_r : r ∉ B.fv) (dv_r_x : r ≠ x) (hyp_enprmaplem3_1 : Nominal.NPrf (SemanticCore.Wff.classEq W (Compiler.CompactSourceSyntax.synCmpt r (Compiler.CompactSourceSyntax.synCo A Compiler.CompactSourceSyntax.synCmap B) (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv r)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)))))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWne (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (SemanticCore.Wff.classEq A (Compiler.CompactSourceSyntax.synCpr (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)))).imp (Compiler.CompactSourceSyntax.synWfun (Compiler.CompactSourceSyntax.synCcnv W)))

Checked nominal proof certificate identified upstream as g_enprmaplem3.

Equations

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

Certificates from NominalWPPReplayChunk013Compact001Part040.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEnprmaplem4 (x y u : SemanticCore.Var) (B R : SemanticCore.Class) (p : SemanticCore.Var) (dv_B_u : u ∉ B.fv) (dv_p_u : p ≠ u) (dv_u_x : u ≠ x) (dv_u_y : u ≠ y) (hyp_enprmaplem4_1 : Nominal.NPrf (SemanticCore.Wff.classEq R (Compiler.CompactSourceSyntax.synCmpt u B (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.objMem u p) (SemanticCore.Class.cv x) (SemanticCore.Class.cv y))))) (hyp_enprmaplem4_2 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_enprmaplem4.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEnprmaplem5 (x y u : SemanticCore.Var) (A B R W : SemanticCore.Class) (r p : SemanticCore.Var) (dv_A_p : p ∉ A.fv) (dv_A_r : r ∉ A.fv) (dv_A_u : u ∉ A.fv) (dv_B_p : p ∉ B.fv) (dv_B_r : r ∉ B.fv) (dv_B_u : u ∉ B.fv) (dv_R_r : r ∉ R.fv) (dv_W_p : p ∉ W.fv) (dv_p_u : p ≠ u) (dv_p_x : p ≠ x) (dv_p_y : p ≠ y) (dv_r_x : r ≠ x) (dv_u_x : u ≠ x) (dv_u_y : u ≠ y) (hyp_enprmaplem5_1 : Nominal.NPrf (SemanticCore.Wff.classEq W (Compiler.CompactSourceSyntax.synCmpt r (Compiler.CompactSourceSyntax.synCo A Compiler.CompactSourceSyntax.synCmap B) (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv r)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)))))) (hyp_enprmaplem5_2 : Nominal.NPrf (SemanticCore.Wff.classEq R (Compiler.CompactSourceSyntax.synCmpt u B (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.objMem u p) (SemanticCore.Class.cv x) (SemanticCore.Class.cv y))))) (hyp_enprmaplem5_3 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWne (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (SemanticCore.Wff.classEq A (Compiler.CompactSourceSyntax.synCpr (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)))).imp (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCpw B) (Compiler.CompactSourceSyntax.synCrn W)))

Checked nominal proof certificate identified upstream as g_enprmaplem5.

Equations

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

Certificates from NominalWPPReplayChunk013Compact001Part041.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEnprmaplem6 (x y : SemanticCore.Var) (A B W : SemanticCore.Class) (r : SemanticCore.Var) (dv_A_r : r ∉ A.fv) (dv_B_r : r ∉ B.fv) (dv_r_x : r ≠ x) (dv_r_y : r ≠ y) (hyp_enprmaplem6_1 : Nominal.NPrf (SemanticCore.Wff.classEq W (Compiler.CompactSourceSyntax.synCmpt r (Compiler.CompactSourceSyntax.synCo A Compiler.CompactSourceSyntax.synCmap B) (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv r)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)))))) (hyp_enprmaplem6_2 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWne (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (SemanticCore.Wff.classEq A (Compiler.CompactSourceSyntax.synCpr (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)))).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCrn W) (Compiler.CompactSourceSyntax.synCpw B)))

Checked nominal proof certificate identified upstream as g_enprmaplem6.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEnprmap (x y : SemanticCore.Var) (A B : SemanticCore.Class) (hyp_enprmap_1 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWne (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (SemanticCore.Wff.classEq A (Compiler.CompactSourceSyntax.synCpr (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)))).imp (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCo A Compiler.CompactSourceSyntax.synCmap B) Compiler.CompactSourceSyntax.synCen (Compiler.CompactSourceSyntax.synCpw B)))

Checked nominal proof certificate identified upstream as g_enprmap.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEnprmapc (A B C P : SemanticCore.Class) (hyp_enprmapc_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_enprmapc_2 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) (hyp_enprmapc_3 : Nominal.NPrf (SemanticCore.Wff.classMem C Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWne A B) (SemanticCore.Wff.classEq P (Compiler.CompactSourceSyntax.synCpr A B))).imp (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCo P Compiler.CompactSourceSyntax.synCmap C) Compiler.CompactSourceSyntax.synCen (Compiler.CompactSourceSyntax.synCpw C)))

Checked nominal proof certificate identified upstream as g_enprmapc.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEnpw (A B : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWbr A Compiler.CompactSourceSyntax.synCen B).imp (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCpw A) Compiler.CompactSourceSyntax.synCen (Compiler.CompactSourceSyntax.synCpw B)))

Checked nominal proof certificate identified upstream as g_enpw.

Equations

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

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

Checked nominal proof certificate identified upstream as g_nceq.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNceqi (A B : SemanticCore.Class) (hyp_nceqi_1 : Nominal.NPrf (SemanticCore.Wff.classEq A B)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCnc A) (Compiler.CompactSourceSyntax.synCnc B))

Checked nominal proof certificate identified upstream as g_nceqi.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gNceqi A B hyp_nceqi_1 = NFChoice.DirectNominalPrf.Nominal.mp hyp_nceqi_1 (NFChoice.DirectNominalPrf.WPPReplay.gNceq A B)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNceqd (ph : SemanticCore.Wff) (A B : SemanticCore.Class) (hyp_nceqd_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCnc A) (Compiler.CompactSourceSyntax.synCnc B)))

Checked nominal proof certificate identified upstream as g_nceqd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNcsex : Nominal.NPrf (SemanticCore.Wff.classMem Compiler.CompactSourceSyntax.synCncs Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_ncsex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBrlecg (x y : SemanticCore.Var) (A B V W : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_B_x : x ∉ B.fv) (dv_B_y : y ∉ B.fv) (dv_x_y : x ≠ y) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A V) (SemanticCore.Wff.classMem B W)).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr A Compiler.CompactSourceSyntax.synClec B) (Compiler.CompactSourceSyntax.synWrex x A (Compiler.CompactSourceSyntax.synWrex y B (Compiler.CompactSourceSyntax.synWss (SemanticCore.Class.cv x) (SemanticCore.Class.cv y))))))

Checked nominal proof certificate identified upstream as g_brlecg.

Equations

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

Certificates from NominalWPPReplayChunk013Compact001Part042.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBrlec (x y : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_B_x : x ∉ B.fv) (dv_B_y : y ∉ B.fv) (dv_x_y : x ≠ y) (hyp_brlec_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_brlec_2 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr A Compiler.CompactSourceSyntax.synClec B) (Compiler.CompactSourceSyntax.synWrex x A (Compiler.CompactSourceSyntax.synWrex y B (Compiler.CompactSourceSyntax.synWss (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)))))

Checked nominal proof certificate identified upstream as g_brlec.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBrltc (A B : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr A Compiler.CompactSourceSyntax.synCltc B) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr A Compiler.CompactSourceSyntax.synClec B) (Compiler.CompactSourceSyntax.synWne A B)))

Checked nominal proof certificate identified upstream as g_brltc.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLecex : Nominal.NPrf (SemanticCore.Wff.classMem Compiler.CompactSourceSyntax.synClec Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_lecex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLtcex : Nominal.NPrf (SemanticCore.Wff.classMem Compiler.CompactSourceSyntax.synCltc Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_ltcex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNcex (A : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCnc A) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_ncex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNulnnc : Nominal.NPrf (SemanticCore.Wff.classMem Compiler.CompactSourceSyntax.synC0 Compiler.CompactSourceSyntax.synCncs).neg

Checked nominal proof certificate identified upstream as g_nulnnc.

Equations

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

Certificates from NominalWPPReplayChunk013Compact001Part043.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElncs (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCncs) (Compiler.CompactSourceSyntax.synWex x (SemanticCore.Wff.classEq A (Compiler.CompactSourceSyntax.synCnc (SemanticCore.Class.cv x)))))

Checked nominal proof certificate identified upstream as g_elncs.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNcelncs (A V : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem A V).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCnc A) Compiler.CompactSourceSyntax.synCncs))

Checked nominal proof certificate identified upstream as g_ncelncs.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNcelncsi (A : SemanticCore.Class) (hyp_ncelncsi_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCnc A) Compiler.CompactSourceSyntax.synCncs)

Checked nominal proof certificate identified upstream as g_ncelncsi.

Equations

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

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

Checked nominal proof certificate identified upstream as g_ncidg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNcid (A : SemanticCore.Class) (hyp_ncid_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synCnc A))

Checked nominal proof certificate identified upstream as g_ncid.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElnc (A B : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synCnc B)) (Compiler.CompactSourceSyntax.synWbr A Compiler.CompactSourceSyntax.synCen B))

Checked nominal proof certificate identified upstream as g_elnc.

Equations

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

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

Checked nominal proof certificate identified upstream as g_eqncg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEqnc (A B : SemanticCore.Class) (hyp_eqnc_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCnc A) (Compiler.CompactSourceSyntax.synCnc B)) (Compiler.CompactSourceSyntax.synWbr A Compiler.CompactSourceSyntax.synCen B))

Checked nominal proof certificate identified upstream as g_eqnc.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNcseqnc (A X : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCncs).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classEq A (Compiler.CompactSourceSyntax.synCnc X)) (SemanticCore.Wff.classMem X A)))

Checked nominal proof certificate identified upstream as g_ncseqnc.

Equations

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