Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk010Compact001Part060.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElima (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 C)) (Compiler.CompactSourceSyntax.synWrex x C (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv x) B A)))

Checked nominal proof certificate identified upstream as g_elima.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElima2 (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 C)) (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) C) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv x) B A))))

Checked nominal proof certificate identified upstream as g_elima2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElima3 (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 C)) (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) C) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) A) B))))

Checked nominal proof certificate identified upstream as g_elima3.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBrssetg (A B V W : SemanticCore.Class) : 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.synCsset B) (Compiler.CompactSourceSyntax.synWss A B)))

Checked nominal proof certificate identified upstream as g_brssetg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBrsset (A B : SemanticCore.Class) (hyp_brsset_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_brsset_2 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr A Compiler.CompactSourceSyntax.synCsset B) (Compiler.CompactSourceSyntax.synWss A B))

Checked nominal proof certificate identified upstream as g_brsset.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBrssetsn (A B : SemanticCore.Class) (hyp_brssetsn_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_brssetsn_2 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCsn A) Compiler.CompactSourceSyntax.synCsset B) (SemanticCore.Wff.classMem A B))

Checked nominal proof certificate identified upstream as g_brssetsn.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOpelssetsn (A B : SemanticCore.Class) (hyp_brssetsn_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_brssetsn_2 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCsn A) B) Compiler.CompactSourceSyntax.synCsset) (SemanticCore.Wff.classMem A B))

Checked nominal proof certificate identified upstream as g_opelssetsn.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBrsi (x y : SemanticCore.Var) (A B R : 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_R_x : x ∉ R.fv) (dv_R_y : y ∉ R.fv) (dv_x_y : x ≠ y) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr A (Compiler.CompactSourceSyntax.synCsi R) B) (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWex y (Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classEq A (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x))) (SemanticCore.Wff.classEq B (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv y))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv x) R (SemanticCore.Class.cv y))))))

Checked nominal proof certificate identified upstream as g_brsi.

Equations

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

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

Checked nominal proof certificate identified upstream as g_xpeq1.

Equations

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

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

Checked nominal proof certificate identified upstream as g_xpeq2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElxp (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) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synCxp 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))) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) B) (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) C))))))

Checked nominal proof certificate identified upstream as g_elxp.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElxp2 (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) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synCxp B C)) (Compiler.CompactSourceSyntax.synWrex x B (Compiler.CompactSourceSyntax.synWrex y C (SemanticCore.Wff.classEq A (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y))))))

Checked nominal proof certificate identified upstream as g_elxp2.

Equations

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

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

Checked nominal proof certificate identified upstream as g_xpeq12.

Equations

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

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

Checked nominal proof certificate identified upstream as g_xpeq1i.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gXpeq1i A B C hyp_xpeq1i_1 = NFChoice.DirectNominalPrf.Nominal.mp hyp_xpeq1i_1 (NFChoice.DirectNominalPrf.WPPReplay.gXpeq1 A B C)

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

Checked nominal proof certificate identified upstream as g_xpeq2i.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gXpeq2i A B C hyp_xpeq1i_1 = NFChoice.DirectNominalPrf.Nominal.mp hyp_xpeq1i_1 (NFChoice.DirectNominalPrf.WPPReplay.gXpeq2 A B C)

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

Checked nominal proof certificate identified upstream as g_xpeq12i.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gXpeq1d (ph : SemanticCore.Wff) (A B C : SemanticCore.Class) (hyp_xpeq1d_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCxp A C) (Compiler.CompactSourceSyntax.synCxp B C)))

Checked nominal proof certificate identified upstream as g_xpeq1d.

Equations

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

Certificates from NominalWPPReplayChunk010Compact001Part061.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gXpeq2d (ph : SemanticCore.Wff) (A B C : SemanticCore.Class) (hyp_xpeq1d_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCxp C A) (Compiler.CompactSourceSyntax.synCxp C B)))

Checked nominal proof certificate identified upstream as g_xpeq2d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gXpeq12d (ph : SemanticCore.Wff) (A B C D : SemanticCore.Class) (hyp_xpeq1d_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) (hyp_xpeq12d_2 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq C D))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCxp A C) (Compiler.CompactSourceSyntax.synCxp B D)))

Checked nominal proof certificate identified upstream as g_xpeq12d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfxp (x : SemanticCore.Var) (A B : SemanticCore.Class) (hyp_nfxp_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc x A)) (hyp_nfxp_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc x B)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc x (Compiler.CompactSourceSyntax.synCxp A B))

Checked nominal proof certificate identified upstream as g_nfxp.

Equations

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

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

Checked nominal proof certificate identified upstream as g_opelxp.

Equations

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

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

Checked nominal proof certificate identified upstream as g_brxp.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFconstopab (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.synCxp A (Compiler.CompactSourceSyntax.synCsn B)) (Compiler.CompactSourceSyntax.synCopab x y (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A) (SemanticCore.Wff.classEq (SemanticCore.Class.cv y) B))))

Checked nominal proof certificate identified upstream as g_fconstopab.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gXpiundir (x : SemanticCore.Var) (A B C : SemanticCore.Class) (dv_C_x : x ∉ C.fv) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCiun x A B) C) (Compiler.CompactSourceSyntax.synCiun x A (Compiler.CompactSourceSyntax.synCxp B C)))

Checked nominal proof certificate identified upstream as g_xpiundir.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIunxpconst (x : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_B_x : x ∉ B.fv) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCiun x A (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)) B)) (Compiler.CompactSourceSyntax.synCxp A B))

Checked nominal proof certificate identified upstream as g_iunxpconst.

Equations

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

Certificates from NominalWPPReplayChunk010Compact001Part062.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOpeliunxp (x : SemanticCore.Var) (A B C : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) C) (Compiler.CompactSourceSyntax.synCiun x A (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)) B))) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A) (SemanticCore.Wff.classMem C B)))

Checked nominal proof certificate identified upstream as g_opeliunxp.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEliunxp (x y : SemanticCore.Var) (A B C : SemanticCore.Class) (dv_A_y : y ∉ A.fv) (dv_B_y : y ∉ B.fv) (dv_C_x : x ∉ C.fv) (dv_C_y : y ∉ C.fv) (dv_x_y : x ≠ y) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem C (Compiler.CompactSourceSyntax.synCiun x A (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)) B))) (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWex y (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classEq C (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y))) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A) (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) B))))))

Checked nominal proof certificate identified upstream as g_eliunxp.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRaliunxp (ph ps : SemanticCore.Wff) (x y z : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (_dv_A_y : y ∉ A.fv) (dv_A_z : z ∉ A.fv) (dv_B_x : x ∉ B.fv) (dv_B_z : z ∉ B.fv) (dv_ph_y : y ∉ ph.fv) (dv_ph_z : z ∉ ph.fv) (dv_ps_x : x ∉ ps.fv) (dv_x_y : x ≠ y) (dv_x_z : x ≠ z) (dv_y_z : y ≠ z) (hyp_raliunxp_1 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv x) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv y) (SemanticCore.Class.cv z))).imp (Compiler.CompactSourceSyntax.synWb ph ps))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWral x (Compiler.CompactSourceSyntax.synCiun y A (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv y)) B)) ph) (Compiler.CompactSourceSyntax.synWral y A (Compiler.CompactSourceSyntax.synWral z B ps)))

Checked nominal proof certificate identified upstream as g_raliunxp.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRexiunxp (ph ps : SemanticCore.Wff) (x y z : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_A_z : z ∉ A.fv) (dv_B_x : x ∉ B.fv) (dv_B_z : z ∉ B.fv) (dv_ph_y : y ∉ ph.fv) (dv_ph_z : z ∉ ph.fv) (dv_ps_x : x ∉ ps.fv) (dv_x_y : x ≠ y) (dv_x_z : x ≠ z) (dv_y_z : y ≠ z) (hyp_raliunxp_1 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv x) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv y) (SemanticCore.Class.cv z))).imp (Compiler.CompactSourceSyntax.synWb ph ps))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWrex x (Compiler.CompactSourceSyntax.synCiun y A (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv y)) B)) ph) (Compiler.CompactSourceSyntax.synWrex y A (Compiler.CompactSourceSyntax.synWrex z B ps)))

Checked nominal proof certificate identified upstream as g_rexiunxp.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRexxp (ph ps : SemanticCore.Wff) (x y z : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_A_z : z ∉ A.fv) (dv_B_x : x ∉ B.fv) (dv_B_y : y ∉ B.fv) (dv_B_z : z ∉ B.fv) (dv_ph_y : y ∉ ph.fv) (dv_ph_z : z ∉ ph.fv) (dv_ps_x : x ∉ ps.fv) (dv_x_y : x ≠ y) (dv_x_z : x ≠ z) (dv_y_z : y ≠ z) (hyp_raliunxp_1 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv x) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv y) (SemanticCore.Class.cv z))).imp (Compiler.CompactSourceSyntax.synWb ph ps))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWrex x (Compiler.CompactSourceSyntax.synCxp A B) ph) (Compiler.CompactSourceSyntax.synWrex y A (Compiler.CompactSourceSyntax.synWrex z B ps)))

Checked nominal proof certificate identified upstream as g_rexxp.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBrel (A B C D R : SemanticCore.Class) (hyp_brelg_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss R (Compiler.CompactSourceSyntax.synCxp C D))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWbr A R B).imp (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A C) (SemanticCore.Wff.classMem B D)))

Checked nominal proof certificate identified upstream as g_brel.

Equations

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

Certificates from NominalWPPReplayChunk010Compact001Part063.

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

Checked nominal proof certificate identified upstream as g_xpundi.

Equations

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

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

Checked nominal proof certificate identified upstream as g_xpundir.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBrinxp2 (A B C D R : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr A (Compiler.CompactSourceSyntax.synCin R (Compiler.CompactSourceSyntax.synCxp C D)) B) (Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classMem A C) (SemanticCore.Wff.classMem B D) (Compiler.CompactSourceSyntax.synWbr A R B)))

Checked nominal proof certificate identified upstream as g_brinxp2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBrinxp (A B C D R : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A C) (SemanticCore.Wff.classMem B D)).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr A R B) (Compiler.CompactSourceSyntax.synWbr A (Compiler.CompactSourceSyntax.synCin R (Compiler.CompactSourceSyntax.synCxp C D)) B)))

Checked nominal proof certificate identified upstream as g_brinxp.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gXp0r (A : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCxp Compiler.CompactSourceSyntax.synC0 A) Compiler.CompactSourceSyntax.synC0)

Checked nominal proof certificate identified upstream as g_xp0r.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gXpvv : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCxp Compiler.CompactSourceSyntax.synCvv Compiler.CompactSourceSyntax.synCvv) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_xpvv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSsrel (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 (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWss A B) (SemanticCore.Wff.all x (SemanticCore.Wff.all y ((SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) A).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) B)))))

Checked nominal proof certificate identified upstream as g_ssrel.

Equations

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

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

Checked nominal proof certificate identified upstream as g_eqrel.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSsopr (x y z : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_A_z : z ∉ A.fv) (dv_B_x : x ∉ B.fv) (dv_B_y : y ∉ B.fv) (dv_B_z : z ∉ B.fv) (dv_x_y : x ≠ y) (dv_x_z : x ≠ z) (dv_y_z : y ≠ z) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWss A B) (SemanticCore.Wff.all x (SemanticCore.Wff.all y (SemanticCore.Wff.all z ((SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (SemanticCore.Class.cv z)) A).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (SemanticCore.Class.cv z)) B))))))

Checked nominal proof certificate identified upstream as g_ssopr.

Equations

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

Certificates from NominalWPPReplayChunk010Compact001Part064.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEqopr (x y z : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_A_z : z ∉ A.fv) (dv_B_x : x ∉ B.fv) (dv_B_y : y ∉ B.fv) (dv_B_z : z ∉ B.fv) (dv_x_y : x ≠ y) (dv_x_z : x ≠ z) (dv_y_z : y ≠ z) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classEq A B) (SemanticCore.Wff.all x (SemanticCore.Wff.all y (SemanticCore.Wff.all z (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (SemanticCore.Class.cv z)) A) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (SemanticCore.Class.cv z)) B))))))

Checked nominal proof certificate identified upstream as g_eqopr.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRelssi (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) (hyp_relssi_1 : Nominal.NPrf ((SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) A).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) B))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss A B)

Checked nominal proof certificate identified upstream as g_relssi.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRelssdv (ph : SemanticCore.Wff) (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_ph_x : x ∉ ph.fv) (dv_ph_y : y ∉ ph.fv) (dv_x_y : x ≠ y) (hyp_relssdv_1 : Nominal.NPrf (ph.imp ((SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) A).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) B)))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWss A B))

Checked nominal proof certificate identified upstream as g_relssdv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEqrelriv (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) (hyp_eqrelriv_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) A) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) B))) : Nominal.NPrf (SemanticCore.Wff.classEq A B)

Checked nominal proof certificate identified upstream as g_eqrelriv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEqbrriv (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) (hyp_eqbrriv_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv x) A (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv x) B (SemanticCore.Class.cv y)))) : Nominal.NPrf (SemanticCore.Wff.classEq A B)

Checked nominal proof certificate identified upstream as g_eqbrriv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEqrelrdv (ph : SemanticCore.Wff) (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_ph_x : x ∉ ph.fv) (dv_ph_y : y ∉ ph.fv) (dv_x_y : x ≠ y) (hyp_eqrelrdv_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) A) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) B)))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))

Checked nominal proof certificate identified upstream as g_eqrelrdv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEqoprriv (x y z : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_A_z : z ∉ A.fv) (dv_B_x : x ∉ B.fv) (dv_B_y : y ∉ B.fv) (dv_B_z : z ∉ B.fv) (dv_x_y : x ≠ y) (dv_x_z : x ≠ z) (dv_y_z : y ≠ z) (hyp_eqoprriv_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (SemanticCore.Class.cv z)) A) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (SemanticCore.Class.cv z)) B))) : Nominal.NPrf (SemanticCore.Wff.classEq A B)

Checked nominal proof certificate identified upstream as g_eqoprriv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gXpss12 (A B C D : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWss A B) (Compiler.CompactSourceSyntax.synWss C D)).imp (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCxp A C) (Compiler.CompactSourceSyntax.synCxp B D)))

Checked nominal proof certificate identified upstream as g_xpss12.

Equations

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

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

Checked nominal proof certificate identified upstream as g_xpss1.

Equations

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

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

Checked nominal proof certificate identified upstream as g_xpss2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBr1st (x : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_B_x : x ∉ B.fv) (hyp_br1st_1 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr A Compiler.CompactSourceSyntax.synC1st B) (Compiler.CompactSourceSyntax.synWex x (SemanticCore.Wff.classEq A (Compiler.CompactSourceSyntax.synCop B (SemanticCore.Class.cv x)))))

Checked nominal proof certificate identified upstream as g_br1st.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBr2nd (x : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_B_x : x ∉ B.fv) (hyp_br1st_1 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr A Compiler.CompactSourceSyntax.synC2nd B) (Compiler.CompactSourceSyntax.synWex x (SemanticCore.Wff.classEq A (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) B))))

Checked nominal proof certificate identified upstream as g_br2nd.

Equations

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