NF weak partition development: NominalWPPReplayChunk001.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gA1ii (ph ps : SemanticCore.Wff) (hyp_a1ii_1 : Nominal.NPrf ph) (_hyp_a1ii_2 : Nominal.NPrf ps) : Nominal.NPrf ph

Checked nominal proof certificate identified upstream as g_a1ii.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gA1ii ph ps hyp_a1ii_1 _hyp_a1ii_2 = hyp_a1ii_1

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMp2b (ph ps ch : SemanticCore.Wff) (hyp_mp2b_1 : Nominal.NPrf ph) (hyp_mp2b_2 : Nominal.NPrf (ph.imp ps)) (hyp_mp2b_3 : Nominal.NPrf (ps.imp ch)) : Nominal.NPrf ch

Checked nominal proof certificate identified upstream as g_mp2b.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gMp2b ph ps ch hyp_mp2b_1 hyp_mp2b_2 hyp_mp2b_3 = NFChoice.DirectNominalPrf.Nominal.mp (NFChoice.DirectNominalPrf.Nominal.mp hyp_mp2b_1 hyp_mp2b_2) hyp_mp2b_3

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gA1i (ph ps : SemanticCore.Wff) (hyp_a1i_1 : Nominal.NPrf ph) : Nominal.NPrf (ps.imp ph)

Checked nominal proof certificate identified upstream as g_a1i.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gA1i ph ps hyp_a1i_1 = NFChoice.DirectNominalPrf.Nominal.mp hyp_a1i_1 (NFChoice.DirectNominalPrf.Nominal.ax1 ph ps)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gA2i (ph ps ch : SemanticCore.Wff) (hyp_a2i_1 : Nominal.NPrf (ph.imp (ps.imp ch))) : Nominal.NPrf ((ph.imp ps).imp (ph.imp ch))

Checked nominal proof certificate identified upstream as g_a2i.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gA2i ph ps ch hyp_a2i_1 = NFChoice.DirectNominalPrf.Nominal.mp hyp_a2i_1 (NFChoice.DirectNominalPrf.Nominal.ax2 ph ps ch)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gImim2i (ph ps ch : SemanticCore.Wff) (hyp_imim2i_1 : Nominal.NPrf (ph.imp ps)) : Nominal.NPrf ((ch.imp ph).imp (ch.imp ps))

Checked nominal proof certificate identified upstream as g_imim2i.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gImim2i ph ps ch hyp_imim2i_1 = NFChoice.DirectNominalPrf.WPPReplay.gA2i ch ph ps (NFChoice.DirectNominalPrf.WPPReplay.gA1i (ph.imp ps) ch hyp_imim2i_1)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMpd (ph ps ch : SemanticCore.Wff) (hyp_mpd_1 : Nominal.NPrf (ph.imp ps)) (hyp_mpd_2 : Nominal.NPrf (ph.imp (ps.imp ch))) : Nominal.NPrf (ph.imp ch)

Checked nominal proof certificate identified upstream as g_mpd.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gMpd ph ps ch hyp_mpd_1 hyp_mpd_2 = NFChoice.DirectNominalPrf.Nominal.mp hyp_mpd_1 (NFChoice.DirectNominalPrf.WPPReplay.gA2i ph ps ch hyp_mpd_2)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSyl (ph ps ch : SemanticCore.Wff) (hyp_syl_1 : Nominal.NPrf (ph.imp ps)) (hyp_syl_2 : Nominal.NPrf (ps.imp ch)) : Nominal.NPrf (ph.imp ch)

Checked nominal proof certificate identified upstream as g_syl.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMpi (ph ps ch : SemanticCore.Wff) (hyp_mpi_1 : Nominal.NPrf ps) (hyp_mpi_2 : Nominal.NPrf (ph.imp (ps.imp ch))) : Nominal.NPrf (ph.imp ch)

Checked nominal proof certificate identified upstream as g_mpi.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gMpi ph ps ch hyp_mpi_1 hyp_mpi_2 = NFChoice.DirectNominalPrf.WPPReplay.gMpd ph ps ch (NFChoice.DirectNominalPrf.WPPReplay.gA1i ps ph hyp_mpi_1) hyp_mpi_2

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMp2 (ph ps ch : SemanticCore.Wff) (hyp_mp2_1 : Nominal.NPrf ph) (hyp_mp2_2 : Nominal.NPrf ps) (hyp_mp2_3 : Nominal.NPrf (ph.imp (ps.imp ch))) : Nominal.NPrf ch

Checked nominal proof certificate identified upstream as g_mp2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN3syl (ph ps ch th : SemanticCore.Wff) (hyp_n_3syl_1 : Nominal.NPrf (ph.imp ps)) (hyp_n_3syl_2 : Nominal.NPrf (ps.imp ch)) (hyp_n_3syl_3 : Nominal.NPrf (ch.imp th)) : Nominal.NPrf (ph.imp th)

Checked nominal proof certificate identified upstream as g_n_3syl.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gId (ph : SemanticCore.Wff) : Nominal.NPrf (ph.imp ph)

Checked nominal proof certificate identified upstream as g_id.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIdd (ph ps : SemanticCore.Wff) : Nominal.NPrf (ph.imp (ps.imp ps))

Checked nominal proof certificate identified upstream as g_idd.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gIdd ph ps = NFChoice.DirectNominalPrf.WPPReplay.gA1i (ps.imp ps) ph (NFChoice.DirectNominalPrf.WPPReplay.gId ps)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gA1d (ph ps ch : SemanticCore.Wff) (hyp_a1d_1 : Nominal.NPrf (ph.imp ps)) : Nominal.NPrf (ph.imp (ch.imp ps))

Checked nominal proof certificate identified upstream as g_a1d.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gA1d ph ps ch hyp_a1d_1 = NFChoice.DirectNominalPrf.WPPReplay.gSyl ph ps (ch.imp ps) hyp_a1d_1 (NFChoice.DirectNominalPrf.Nominal.ax1 ps ch)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gA2d (ph ps ch th : SemanticCore.Wff) (hyp_a2d_1 : Nominal.NPrf (ph.imp (ps.imp (ch.imp th)))) : Nominal.NPrf (ph.imp ((ps.imp ch).imp (ps.imp th)))

Checked nominal proof certificate identified upstream as g_a2d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN2a1i (ph ps ch : SemanticCore.Wff) (hyp_n_2a1i_1 : Nominal.NPrf ch) : Nominal.NPrf (ph.imp (ps.imp ch))

Checked nominal proof certificate identified upstream as g_n_2a1i.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gN2a1i ph ps ch hyp_n_2a1i_1 = NFChoice.DirectNominalPrf.WPPReplay.gA1d ph ch ps (NFChoice.DirectNominalPrf.WPPReplay.gA1i ch ph hyp_n_2a1i_1)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSylcom (ph ps ch th : SemanticCore.Wff) (hyp_sylcom_1 : Nominal.NPrf (ph.imp (ps.imp ch))) (hyp_sylcom_2 : Nominal.NPrf (ps.imp (ch.imp th))) : Nominal.NPrf (ph.imp (ps.imp th))

Checked nominal proof certificate identified upstream as g_sylcom.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSyl5com (ph ps ch th : SemanticCore.Wff) (hyp_syl5com_1 : Nominal.NPrf (ph.imp ps)) (hyp_syl5com_2 : Nominal.NPrf (ch.imp (ps.imp th))) : Nominal.NPrf (ph.imp (ch.imp th))

Checked nominal proof certificate identified upstream as g_syl5com.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCom12 (ph ps ch : SemanticCore.Wff) (hyp_com12_1 : Nominal.NPrf (ph.imp (ps.imp ch))) : Nominal.NPrf (ps.imp (ph.imp ch))

Checked nominal proof certificate identified upstream as g_com12.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gCom12 ph ps ch hyp_com12_1 = NFChoice.DirectNominalPrf.WPPReplay.gSyl5com ps ps ph ch (NFChoice.DirectNominalPrf.WPPReplay.gId ps) hyp_com12_1

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSyl5 (ph ps ch th : SemanticCore.Wff) (hyp_syl5_1 : Nominal.NPrf (ph.imp ps)) (hyp_syl5_2 : Nominal.NPrf (ch.imp (ps.imp th))) : Nominal.NPrf (ch.imp (ph.imp th))

Checked nominal proof certificate identified upstream as g_syl5.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSyl6 (ph ps ch th : SemanticCore.Wff) (hyp_syl6_1 : Nominal.NPrf (ph.imp (ps.imp ch))) (hyp_syl6_2 : Nominal.NPrf (ch.imp th)) : Nominal.NPrf (ph.imp (ps.imp th))

Checked nominal proof certificate identified upstream as g_syl6.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSyl56 (ph ps ch th ta : SemanticCore.Wff) (hyp_syl56_1 : Nominal.NPrf (ph.imp ps)) (hyp_syl56_2 : Nominal.NPrf (ch.imp (ps.imp th))) (hyp_syl56_3 : Nominal.NPrf (th.imp ta)) : Nominal.NPrf (ch.imp (ph.imp ta))

Checked nominal proof certificate identified upstream as g_syl56.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSyl6com (ph ps ch th : SemanticCore.Wff) (hyp_syl6com_1 : Nominal.NPrf (ph.imp (ps.imp ch))) (hyp_syl6com_2 : Nominal.NPrf (ch.imp th)) : Nominal.NPrf (ps.imp (ph.imp th))

Checked nominal proof certificate identified upstream as g_syl6com.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMpcom (ph ps ch : SemanticCore.Wff) (hyp_mpcom_1 : Nominal.NPrf (ps.imp ph)) (hyp_mpcom_2 : Nominal.NPrf (ph.imp (ps.imp ch))) : Nominal.NPrf (ps.imp ch)

Checked nominal proof certificate identified upstream as g_mpcom.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSyli (ph ps ch th : SemanticCore.Wff) (hyp_syli_1 : Nominal.NPrf (ps.imp (ph.imp ch))) (hyp_syli_2 : Nominal.NPrf (ch.imp (ph.imp th))) : Nominal.NPrf (ps.imp (ph.imp th))

Checked nominal proof certificate identified upstream as g_syli.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSyl2im (ph ps ch th ta : SemanticCore.Wff) (hyp_syl2im_1 : Nominal.NPrf (ph.imp ps)) (hyp_syl2im_2 : Nominal.NPrf (ch.imp th)) (hyp_syl2im_3 : Nominal.NPrf (ps.imp (th.imp ta))) : Nominal.NPrf (ph.imp (ch.imp ta))

Checked nominal proof certificate identified upstream as g_syl2im.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPm227 (ph ps : SemanticCore.Wff) : Nominal.NPrf (ph.imp ((ph.imp ps).imp ps))

Checked nominal proof certificate identified upstream as g_pm2_27.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gPm227 ph ps = NFChoice.DirectNominalPrf.WPPReplay.gCom12 (ph.imp ps) ph ps (NFChoice.DirectNominalPrf.WPPReplay.gId (ph.imp ps))

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMpdd (ph ps ch th : SemanticCore.Wff) (hyp_mpdd_1 : Nominal.NPrf (ph.imp (ps.imp ch))) (hyp_mpdd_2 : Nominal.NPrf (ph.imp (ps.imp (ch.imp th)))) : Nominal.NPrf (ph.imp (ps.imp th))

Checked nominal proof certificate identified upstream as g_mpdd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMpid (ph ps ch th : SemanticCore.Wff) (hyp_mpid_1 : Nominal.NPrf (ph.imp ch)) (hyp_mpid_2 : Nominal.NPrf (ph.imp (ps.imp (ch.imp th)))) : Nominal.NPrf (ph.imp (ps.imp th))

Checked nominal proof certificate identified upstream as g_mpid.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMpdi (ph ps ch th : SemanticCore.Wff) (hyp_mpdi_1 : Nominal.NPrf (ps.imp ch)) (hyp_mpdi_2 : Nominal.NPrf (ph.imp (ps.imp (ch.imp th)))) : Nominal.NPrf (ph.imp (ps.imp th))

Checked nominal proof certificate identified upstream as g_mpdi.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMpii (ph ps ch th : SemanticCore.Wff) (hyp_mpii_1 : Nominal.NPrf ch) (hyp_mpii_2 : Nominal.NPrf (ph.imp (ps.imp (ch.imp th)))) : Nominal.NPrf (ph.imp (ps.imp th))

Checked nominal proof certificate identified upstream as g_mpii.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSyld (ph ps ch th : SemanticCore.Wff) (hyp_syld_1 : Nominal.NPrf (ph.imp (ps.imp ch))) (hyp_syld_2 : Nominal.NPrf (ph.imp (ch.imp th))) : Nominal.NPrf (ph.imp (ps.imp th))

Checked nominal proof certificate identified upstream as g_syld.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gA1dd (ph ps ch th : SemanticCore.Wff) (hyp_a1dd_1 : Nominal.NPrf (ph.imp (ps.imp ch))) : Nominal.NPrf (ph.imp (ps.imp (th.imp ch)))

Checked nominal proof certificate identified upstream as g_a1dd.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gA1dd ph ps ch th hyp_a1dd_1 = NFChoice.DirectNominalPrf.WPPReplay.gSyl6 ph ps ch (th.imp ch) hyp_a1dd_1 (NFChoice.DirectNominalPrf.Nominal.ax1 ch th)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPm243i (ph ps : SemanticCore.Wff) (hyp_pm2_43i_1 : Nominal.NPrf (ph.imp (ph.imp ps))) : Nominal.NPrf (ph.imp ps)

Checked nominal proof certificate identified upstream as g_pm2_43i.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gPm243i ph ps hyp_pm2_43i_1 = NFChoice.DirectNominalPrf.WPPReplay.gMpd ph ph ps (NFChoice.DirectNominalPrf.WPPReplay.gId ph) hyp_pm2_43i_1

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPm243d (ph ps ch : SemanticCore.Wff) (hyp_pm2_43d_1 : Nominal.NPrf (ph.imp (ps.imp (ps.imp ch)))) : Nominal.NPrf (ph.imp (ps.imp ch))

Checked nominal proof certificate identified upstream as g_pm2_43d.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gPm243d ph ps ch hyp_pm2_43d_1 = NFChoice.DirectNominalPrf.WPPReplay.gMpdi ph ps ps ch (NFChoice.DirectNominalPrf.WPPReplay.gId ps) hyp_pm2_43d_1

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPm243a (ph ps ch : SemanticCore.Wff) (hyp_pm2_43a_1 : Nominal.NPrf (ps.imp (ph.imp (ps.imp ch)))) : Nominal.NPrf (ps.imp (ph.imp ch))

Checked nominal proof certificate identified upstream as g_pm2_43a.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gPm243a ph ps ch hyp_pm2_43a_1 = NFChoice.DirectNominalPrf.WPPReplay.gMpid ps ph ps ch (NFChoice.DirectNominalPrf.WPPReplay.gId ps) hyp_pm2_43a_1

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPm243b (ph ps ch : SemanticCore.Wff) (hyp_pm2_43b_1 : Nominal.NPrf (ps.imp (ph.imp (ps.imp ch)))) : Nominal.NPrf (ph.imp (ps.imp ch))

Checked nominal proof certificate identified upstream as g_pm2_43b.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gPm243b ph ps ch hyp_pm2_43b_1 = NFChoice.DirectNominalPrf.WPPReplay.gCom12 ps ph ch (NFChoice.DirectNominalPrf.WPPReplay.gPm243a ph ps ch hyp_pm2_43b_1)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gImim2d (ph ps ch th : SemanticCore.Wff) (hyp_imim2d_1 : Nominal.NPrf (ph.imp (ps.imp ch))) : Nominal.NPrf (ph.imp ((th.imp ps).imp (th.imp ch)))

Checked nominal proof certificate identified upstream as g_imim2d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gImim2 (ph ps ch : SemanticCore.Wff) : Nominal.NPrf ((ph.imp ps).imp ((ch.imp ph).imp (ch.imp ps)))

Checked nominal proof certificate identified upstream as g_imim2.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gImim2 ph ps ch = NFChoice.DirectNominalPrf.WPPReplay.gImim2d (ph.imp ps) ph ps ch (NFChoice.DirectNominalPrf.WPPReplay.gId (ph.imp ps))

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEmbantd (ph ps ch th : SemanticCore.Wff) (hyp_embantd_1 : Nominal.NPrf (ph.imp ps)) (hyp_embantd_2 : Nominal.NPrf (ph.imp (ch.imp th))) : Nominal.NPrf (ph.imp ((ps.imp ch).imp th))

Checked nominal proof certificate identified upstream as g_embantd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSylsyld (ph ps ch th ta : SemanticCore.Wff) (hyp_sylsyld_1 : Nominal.NPrf (ph.imp ps)) (hyp_sylsyld_2 : Nominal.NPrf (ph.imp (ch.imp th))) (hyp_sylsyld_3 : Nominal.NPrf (ps.imp (th.imp ta))) : Nominal.NPrf (ph.imp (ch.imp ta))

Checked nominal proof certificate identified upstream as g_sylsyld.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gImim12i (ph ps ch th : SemanticCore.Wff) (hyp_imim12i_1 : Nominal.NPrf (ph.imp ps)) (hyp_imim12i_2 : Nominal.NPrf (ch.imp th)) : Nominal.NPrf ((ps.imp ch).imp (ph.imp th))

Checked nominal proof certificate identified upstream as g_imim12i.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gImim1i (ph ps ch : SemanticCore.Wff) (hyp_imim1i_1 : Nominal.NPrf (ph.imp ps)) : Nominal.NPrf ((ps.imp ch).imp (ph.imp ch))

Checked nominal proof certificate identified upstream as g_imim1i.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gImim1i ph ps ch hyp_imim1i_1 = NFChoice.DirectNominalPrf.WPPReplay.gImim12i ph ps ch ch hyp_imim1i_1 (NFChoice.DirectNominalPrf.WPPReplay.gId ch)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gImim3i (ph ps ch th : SemanticCore.Wff) (hyp_imim3i_1 : Nominal.NPrf (ph.imp (ps.imp ch))) : Nominal.NPrf ((th.imp ph).imp ((th.imp ps).imp (th.imp ch)))

Checked nominal proof certificate identified upstream as g_imim3i.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSylc (ph ps ch th : SemanticCore.Wff) (hyp_sylc_1 : Nominal.NPrf (ph.imp ps)) (hyp_sylc_2 : Nominal.NPrf (ph.imp ch)) (hyp_sylc_3 : Nominal.NPrf (ps.imp (ch.imp th))) : Nominal.NPrf (ph.imp th)

Checked nominal proof certificate identified upstream as g_sylc.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSyl3c (ph ps ch th ta : SemanticCore.Wff) (hyp_syl3c_1 : Nominal.NPrf (ph.imp ps)) (hyp_syl3c_2 : Nominal.NPrf (ph.imp ch)) (hyp_syl3c_3 : Nominal.NPrf (ph.imp th)) (hyp_syl3c_4 : Nominal.NPrf (ps.imp (ch.imp (th.imp ta)))) : Nominal.NPrf (ph.imp ta)

Checked nominal proof certificate identified upstream as g_syl3c.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMpsyl (ph ps ch th : SemanticCore.Wff) (hyp_mpsyl_1 : Nominal.NPrf ph) (hyp_mpsyl_2 : Nominal.NPrf (ps.imp ch)) (hyp_mpsyl_3 : Nominal.NPrf (ph.imp (ch.imp th))) : Nominal.NPrf (ps.imp th)

Checked nominal proof certificate identified upstream as g_mpsyl.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSyl6c (ph ps ch th ta : SemanticCore.Wff) (hyp_syl6c_1 : Nominal.NPrf (ph.imp (ps.imp ch))) (hyp_syl6c_2 : Nominal.NPrf (ph.imp (ps.imp th))) (hyp_syl6c_3 : Nominal.NPrf (ch.imp (th.imp ta))) : Nominal.NPrf (ph.imp (ps.imp ta))

Checked nominal proof certificate identified upstream as g_syl6c.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSyldd (ph ps ch th ta : SemanticCore.Wff) (hyp_syldd_1 : Nominal.NPrf (ph.imp (ps.imp (ch.imp th)))) (hyp_syldd_2 : Nominal.NPrf (ph.imp (ps.imp (th.imp ta)))) : Nominal.NPrf (ph.imp (ps.imp (ch.imp ta)))

Checked nominal proof certificate identified upstream as g_syldd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSyl5d (ph ps ch th ta : SemanticCore.Wff) (hyp_syl5d_1 : Nominal.NPrf (ph.imp (ps.imp ch))) (hyp_syl5d_2 : Nominal.NPrf (ph.imp (th.imp (ch.imp ta)))) : Nominal.NPrf (ph.imp (th.imp (ps.imp ta)))

Checked nominal proof certificate identified upstream as g_syl5d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSyl7 (ph ps ch th ta : SemanticCore.Wff) (hyp_syl7_1 : Nominal.NPrf (ph.imp ps)) (hyp_syl7_2 : Nominal.NPrf (ch.imp (th.imp (ps.imp ta)))) : Nominal.NPrf (ch.imp (th.imp (ph.imp ta)))

Checked nominal proof certificate identified upstream as g_syl7.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSyl6d (ph ps ch th ta : SemanticCore.Wff) (hyp_syl6d_1 : Nominal.NPrf (ph.imp (ps.imp (ch.imp th)))) (hyp_syl6d_2 : Nominal.NPrf (ph.imp (th.imp ta))) : Nominal.NPrf (ph.imp (ps.imp (ch.imp ta)))

Checked nominal proof certificate identified upstream as g_syl6d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSyl8 (ph ps ch th ta : SemanticCore.Wff) (hyp_syl8_1 : Nominal.NPrf (ph.imp (ps.imp (ch.imp th)))) (hyp_syl8_2 : Nominal.NPrf (th.imp ta)) : Nominal.NPrf (ph.imp (ps.imp (ch.imp ta)))

Checked nominal proof certificate identified upstream as g_syl8.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSyl9 (ph ps ch th ta : SemanticCore.Wff) (hyp_syl9_1 : Nominal.NPrf (ph.imp (ps.imp ch))) (hyp_syl9_2 : Nominal.NPrf (th.imp (ch.imp ta))) : Nominal.NPrf (ph.imp (th.imp (ps.imp ta)))

Checked nominal proof certificate identified upstream as g_syl9.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSyl9r (ph ps ch th ta : SemanticCore.Wff) (hyp_syl9r_1 : Nominal.NPrf (ph.imp (ps.imp ch))) (hyp_syl9r_2 : Nominal.NPrf (th.imp (ch.imp ta))) : Nominal.NPrf (th.imp (ph.imp (ps.imp ta)))

Checked nominal proof certificate identified upstream as g_syl9r.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gImim12d (ph ps ch th ta : SemanticCore.Wff) (hyp_imim12d_1 : Nominal.NPrf (ph.imp (ps.imp ch))) (hyp_imim12d_2 : Nominal.NPrf (ph.imp (th.imp ta))) : Nominal.NPrf (ph.imp ((ch.imp th).imp (ps.imp ta)))

Checked nominal proof certificate identified upstream as g_imim12d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gImim1d (ph ps ch th : SemanticCore.Wff) (hyp_imim1d_1 : Nominal.NPrf (ph.imp (ps.imp ch))) : Nominal.NPrf (ph.imp ((ch.imp th).imp (ps.imp th)))

Checked nominal proof certificate identified upstream as g_imim1d.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gImim1d ph ps ch th hyp_imim1d_1 = NFChoice.DirectNominalPrf.WPPReplay.gImim12d ph ps ch th th hyp_imim1d_1 (NFChoice.DirectNominalPrf.WPPReplay.gIdd ph th)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gImim1 (ph ps ch : SemanticCore.Wff) : Nominal.NPrf ((ph.imp ps).imp ((ps.imp ch).imp (ph.imp ch)))

Checked nominal proof certificate identified upstream as g_imim1.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gImim1 ph ps ch = NFChoice.DirectNominalPrf.WPPReplay.gImim1d (ph.imp ps) ph ps ch (NFChoice.DirectNominalPrf.WPPReplay.gId (ph.imp ps))

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCom23 (ph ps ch th : SemanticCore.Wff) (hyp_com3_1 : Nominal.NPrf (ph.imp (ps.imp (ch.imp th)))) : Nominal.NPrf (ph.imp (ch.imp (ps.imp th)))

Checked nominal proof certificate identified upstream as g_com23.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCom3r (ph ps ch th : SemanticCore.Wff) (hyp_com3_1 : Nominal.NPrf (ph.imp (ps.imp (ch.imp th)))) : Nominal.NPrf (ch.imp (ph.imp (ps.imp th)))

Checked nominal proof certificate identified upstream as g_com3r.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCom3l (ph ps ch th : SemanticCore.Wff) (hyp_com3_1 : Nominal.NPrf (ph.imp (ps.imp (ch.imp th)))) : Nominal.NPrf (ps.imp (ch.imp (ph.imp th)))

Checked nominal proof certificate identified upstream as g_com3l.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gCom3l ph ps ch th hyp_com3_1 = NFChoice.DirectNominalPrf.WPPReplay.gCom3r ch ph ps th (NFChoice.DirectNominalPrf.WPPReplay.gCom3r ph ps ch th hyp_com3_1)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPm204 (ph ps ch : SemanticCore.Wff) : Nominal.NPrf ((ph.imp (ps.imp ch)).imp (ps.imp (ph.imp ch)))

Checked nominal proof certificate identified upstream as g_pm2_04.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gPm204 ph ps ch = NFChoice.DirectNominalPrf.WPPReplay.gCom23 (ph.imp (ps.imp ch)) ph ps ch (NFChoice.DirectNominalPrf.WPPReplay.gId (ph.imp (ps.imp ch)))

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCom34 (ph ps ch th ta : SemanticCore.Wff) (hyp_com4_1 : Nominal.NPrf (ph.imp (ps.imp (ch.imp (th.imp ta))))) : Nominal.NPrf (ph.imp (ps.imp (th.imp (ch.imp ta))))

Checked nominal proof certificate identified upstream as g_com34.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCom4l (ph ps ch th ta : SemanticCore.Wff) (hyp_com4_1 : Nominal.NPrf (ph.imp (ps.imp (ch.imp (th.imp ta))))) : Nominal.NPrf (ps.imp (ch.imp (th.imp (ph.imp ta))))

Checked nominal proof certificate identified upstream as g_com4l.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCom4t (ph ps ch th ta : SemanticCore.Wff) (hyp_com4_1 : Nominal.NPrf (ph.imp (ps.imp (ch.imp (th.imp ta))))) : Nominal.NPrf (ch.imp (th.imp (ph.imp (ps.imp ta))))

Checked nominal proof certificate identified upstream as g_com4t.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCom4r (ph ps ch th ta : SemanticCore.Wff) (hyp_com4_1 : Nominal.NPrf (ph.imp (ps.imp (ch.imp (th.imp ta))))) : Nominal.NPrf (th.imp (ph.imp (ps.imp (ch.imp ta))))

Checked nominal proof certificate identified upstream as g_com4r.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPm286d (ph ps ch th : SemanticCore.Wff) (hyp_pm2_86d_1 : Nominal.NPrf (ph.imp ((ps.imp ch).imp (ps.imp th)))) : Nominal.NPrf (ph.imp (ps.imp (ch.imp th)))

Checked nominal proof certificate identified upstream as g_pm2_86d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCon4d (ph ps ch : SemanticCore.Wff) (hyp_con4d_1 : Nominal.NPrf (ph.imp (ps.neg.imp ch.neg))) : Nominal.NPrf (ph.imp (ch.imp ps))

Checked nominal proof certificate identified upstream as g_con4d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPm221d (ph ps ch : SemanticCore.Wff) (hyp_pm2_21d_1 : Nominal.NPrf (ph.imp ps.neg)) : Nominal.NPrf (ph.imp (ps.imp ch))

Checked nominal proof certificate identified upstream as g_pm2_21d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPm221dd (ph ps ch : SemanticCore.Wff) (hyp_pm2_21dd_1 : Nominal.NPrf (ph.imp ps)) (hyp_pm2_21dd_2 : Nominal.NPrf (ph.imp ps.neg)) : Nominal.NPrf (ph.imp ch)

Checked nominal proof certificate identified upstream as g_pm2_21dd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPm221 (ph ps : SemanticCore.Wff) : Nominal.NPrf (ph.neg.imp (ph.imp ps))

Checked nominal proof certificate identified upstream as g_pm2_21.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gPm221 ph ps = NFChoice.DirectNominalPrf.WPPReplay.gPm221d ph.neg ph ps (NFChoice.DirectNominalPrf.WPPReplay.gId ph.neg)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPm224 (ph ps : SemanticCore.Wff) : Nominal.NPrf (ph.imp (ph.neg.imp ps))

Checked nominal proof certificate identified upstream as g_pm2_24.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gPm224 ph ps = NFChoice.DirectNominalPrf.WPPReplay.gCom12 ph.neg ph ps (NFChoice.DirectNominalPrf.WPPReplay.gPm221 ph ps)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPm218 (ph : SemanticCore.Wff) : Nominal.NPrf ((ph.neg.imp ph).imp ph)

Checked nominal proof certificate identified upstream as g_pm2_18.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPm218d (ph ps : SemanticCore.Wff) (hyp_pm2_18d_1 : Nominal.NPrf (ph.imp (ps.neg.imp ps))) : Nominal.NPrf (ph.imp ps)

Checked nominal proof certificate identified upstream as g_pm2_18d.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gPm218d ph ps hyp_pm2_18d_1 = NFChoice.DirectNominalPrf.WPPReplay.gSyl ph (ps.neg.imp ps) ps hyp_pm2_18d_1 (NFChoice.DirectNominalPrf.WPPReplay.gPm218 ps)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNotnot2 (ph : SemanticCore.Wff) : Nominal.NPrf (ph.neg.neg.imp ph)

Checked nominal proof certificate identified upstream as g_notnot2.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gNotnot2 ph = NFChoice.DirectNominalPrf.WPPReplay.gPm218d ph.neg.neg ph (NFChoice.DirectNominalPrf.WPPReplay.gPm221 ph.neg ph)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNotnotrd (ph ps : SemanticCore.Wff) (hyp_notnotrd_1 : Nominal.NPrf (ph.imp ps.neg.neg)) : Nominal.NPrf (ph.imp ps)

Checked nominal proof certificate identified upstream as g_notnotrd.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gNotnotrd ph ps hyp_notnotrd_1 = NFChoice.DirectNominalPrf.WPPReplay.gSyl ph ps.neg.neg ps hyp_notnotrd_1 (NFChoice.DirectNominalPrf.WPPReplay.gNotnot2 ps)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNotnotri (ph : SemanticCore.Wff) (hyp_notnotri_1 : Nominal.NPrf ph.neg.neg) : Nominal.NPrf ph

Checked nominal proof certificate identified upstream as g_notnotri.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gNotnotri ph hyp_notnotri_1 = NFChoice.DirectNominalPrf.Nominal.mp hyp_notnotri_1 (NFChoice.DirectNominalPrf.WPPReplay.gNotnot2 ph)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCon2d (ph ps ch : SemanticCore.Wff) (hyp_con2d_1 : Nominal.NPrf (ph.imp (ps.imp ch.neg))) : Nominal.NPrf (ph.imp (ch.imp ps.neg))

Checked nominal proof certificate identified upstream as g_con2d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCon2 (ph ps : SemanticCore.Wff) : Nominal.NPrf ((ph.imp ps.neg).imp (ps.imp ph.neg))

Checked nominal proof certificate identified upstream as g_con2.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gCon2 ph ps = NFChoice.DirectNominalPrf.WPPReplay.gCon2d (ph.imp ps.neg) ph ps (NFChoice.DirectNominalPrf.WPPReplay.gId (ph.imp ps.neg))

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMt2d (ph ps ch : SemanticCore.Wff) (hyp_mt2d_1 : Nominal.NPrf (ph.imp ch)) (hyp_mt2d_2 : Nominal.NPrf (ph.imp (ps.imp ch.neg))) : Nominal.NPrf (ph.imp ps.neg)

Checked nominal proof certificate identified upstream as g_mt2d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNsyl3 (ph ps ch : SemanticCore.Wff) (hyp_nsyl3_1 : Nominal.NPrf (ph.imp ps.neg)) (hyp_nsyl3_2 : Nominal.NPrf (ch.imp ps)) : Nominal.NPrf (ch.imp ph.neg)

Checked nominal proof certificate identified upstream as g_nsyl3.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCon2i (ph ps : SemanticCore.Wff) (hyp_con2i_a : Nominal.NPrf (ph.imp ps.neg)) : Nominal.NPrf (ps.imp ph.neg)

Checked nominal proof certificate identified upstream as g_con2i.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gCon2i ph ps hyp_con2i_a = NFChoice.DirectNominalPrf.WPPReplay.gNsyl3 ph ps ps hyp_con2i_a (NFChoice.DirectNominalPrf.WPPReplay.gId ps)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNsyl (ph ps ch : SemanticCore.Wff) (hyp_nsyl_1 : Nominal.NPrf (ph.imp ps.neg)) (hyp_nsyl_2 : Nominal.NPrf (ch.imp ps)) : Nominal.NPrf (ph.imp ch.neg)

Checked nominal proof certificate identified upstream as g_nsyl.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNotnot1 (ph : SemanticCore.Wff) : Nominal.NPrf (ph.imp ph.neg.neg)

Checked nominal proof certificate identified upstream as g_notnot1.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gNotnot1 ph = NFChoice.DirectNominalPrf.WPPReplay.gCon2i ph.neg ph (NFChoice.DirectNominalPrf.WPPReplay.gId ph.neg)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNotnoti (ph : SemanticCore.Wff) (hyp_negbi_1 : Nominal.NPrf ph) : Nominal.NPrf ph.neg.neg

Checked nominal proof certificate identified upstream as g_notnoti.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gNotnoti ph hyp_negbi_1 = NFChoice.DirectNominalPrf.Nominal.mp hyp_negbi_1 (NFChoice.DirectNominalPrf.WPPReplay.gNotnot1 ph)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCon1d (ph ps ch : SemanticCore.Wff) (hyp_con1d_1 : Nominal.NPrf (ph.imp (ps.neg.imp ch))) : Nominal.NPrf (ph.imp (ch.neg.imp ps))

Checked nominal proof certificate identified upstream as g_con1d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMt3d (ph ps ch : SemanticCore.Wff) (hyp_mt3d_1 : Nominal.NPrf (ph.imp ch.neg)) (hyp_mt3d_2 : Nominal.NPrf (ph.imp (ps.neg.imp ch))) : Nominal.NPrf (ph.imp ps)

Checked nominal proof certificate identified upstream as g_mt3d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNsyl2 (ph ps ch : SemanticCore.Wff) (hyp_nsyl2_1 : Nominal.NPrf (ph.imp ps.neg)) (hyp_nsyl2_2 : Nominal.NPrf (ch.neg.imp ps)) : Nominal.NPrf (ph.imp ch)

Checked nominal proof certificate identified upstream as g_nsyl2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCon1 (ph ps : SemanticCore.Wff) : Nominal.NPrf ((ph.neg.imp ps).imp (ps.neg.imp ph))

Checked nominal proof certificate identified upstream as g_con1.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gCon1 ph ps = NFChoice.DirectNominalPrf.WPPReplay.gCon1d (ph.neg.imp ps) ph ps (NFChoice.DirectNominalPrf.WPPReplay.gId (ph.neg.imp ps))

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCon1i (ph ps : SemanticCore.Wff) (hyp_con1i_a : Nominal.NPrf (ph.neg.imp ps)) : Nominal.NPrf (ps.neg.imp ph)

Checked nominal proof certificate identified upstream as g_con1i.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gCon1i ph ps hyp_con1i_a = NFChoice.DirectNominalPrf.WPPReplay.gNsyl2 ps.neg ps ph (NFChoice.DirectNominalPrf.WPPReplay.gId ps.neg) hyp_con1i_a

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCon4i (ph ps : SemanticCore.Wff) (hyp_con4i_1 : Nominal.NPrf (ph.neg.imp ps.neg)) : Nominal.NPrf (ps.imp ph)

Checked nominal proof certificate identified upstream as g_con4i.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gCon4i ph ps hyp_con4i_1 = NFChoice.DirectNominalPrf.WPPReplay.gNsyl2 ps ps.neg ph (NFChoice.DirectNominalPrf.WPPReplay.gNotnot1 ps) hyp_con4i_1

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPm221i (ph ps : SemanticCore.Wff) (hyp_pm2_21i_1 : Nominal.NPrf ph.neg) : Nominal.NPrf (ph.imp ps)

Checked nominal proof certificate identified upstream as g_pm2_21i.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gPm221i ph ps hyp_pm2_21i_1 = NFChoice.DirectNominalPrf.WPPReplay.gCon4i ps ph (NFChoice.DirectNominalPrf.WPPReplay.gA1i ph.neg ps.neg hyp_pm2_21i_1)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCon3d (ph ps ch : SemanticCore.Wff) (hyp_con3d_1 : Nominal.NPrf (ph.imp (ps.imp ch))) : Nominal.NPrf (ph.imp (ch.neg.imp ps.neg))

Checked nominal proof certificate identified upstream as g_con3d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCon3 (ph ps : SemanticCore.Wff) : Nominal.NPrf ((ph.imp ps).imp (ps.neg.imp ph.neg))

Checked nominal proof certificate identified upstream as g_con3.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gCon3 ph ps = NFChoice.DirectNominalPrf.WPPReplay.gCon3d (ph.imp ps) ph ps (NFChoice.DirectNominalPrf.WPPReplay.gId (ph.imp ps))

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCon3i (ph ps : SemanticCore.Wff) (hyp_con3i_a : Nominal.NPrf (ph.imp ps)) : Nominal.NPrf (ps.neg.imp ph.neg)

Checked nominal proof certificate identified upstream as g_con3i.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gCon3i ph ps hyp_con3i_a = NFChoice.DirectNominalPrf.WPPReplay.gNsyl ps.neg ps ph (NFChoice.DirectNominalPrf.WPPReplay.gId ps.neg) hyp_con3i_a

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCon3rr3 (ph ps ch : SemanticCore.Wff) (hyp_con3rr3_1 : Nominal.NPrf (ph.imp (ps.imp ch))) : Nominal.NPrf (ch.neg.imp (ph.imp ps.neg))

Checked nominal proof certificate identified upstream as g_con3rr3.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNsyld (ph ps ch ta : SemanticCore.Wff) (hyp_nsyld_1 : Nominal.NPrf (ph.imp (ps.imp ch.neg))) (hyp_nsyld_2 : Nominal.NPrf (ph.imp (ta.imp ch))) : Nominal.NPrf (ph.imp (ps.imp ta.neg))

Checked nominal proof certificate identified upstream as g_nsyld.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNsyl4 (ph ps ch : SemanticCore.Wff) (hyp_nsyl4_1 : Nominal.NPrf (ph.imp ps)) (hyp_nsyl4_2 : Nominal.NPrf (ph.neg.imp ch)) : Nominal.NPrf (ch.neg.imp ps)

Checked nominal proof certificate identified upstream as g_nsyl4.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPm224i (ph ps : SemanticCore.Wff) (hyp_pm2_24i_1 : Nominal.NPrf ph) : Nominal.NPrf (ph.neg.imp ps)

Checked nominal proof certificate identified upstream as g_pm2_24i.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gPm224i ph ps hyp_pm2_24i_1 = NFChoice.DirectNominalPrf.WPPReplay.gCon1i ps ph (NFChoice.DirectNominalPrf.WPPReplay.gA1i ph ps.neg hyp_pm2_24i_1)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPm32im (ph ps : SemanticCore.Wff) : Nominal.NPrf (ph.imp (ps.imp (ph.imp ps.neg).neg))

Checked nominal proof certificate identified upstream as g_pm3_2im.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gPm32im ph ps = NFChoice.DirectNominalPrf.WPPReplay.gCon2d ph (ph.imp ps.neg) ps (NFChoice.DirectNominalPrf.WPPReplay.gPm227 ph ps.neg)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gImpi (ph ps ch : SemanticCore.Wff) (hyp_impi_1 : Nominal.NPrf (ph.imp (ps.imp ch))) : Nominal.NPrf ((ph.imp ps.neg).neg.imp ch)

Checked nominal proof certificate identified upstream as g_impi.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gImpi ph ps ch hyp_impi_1 = NFChoice.DirectNominalPrf.WPPReplay.gCon1i ch (ph.imp ps.neg) (NFChoice.DirectNominalPrf.WPPReplay.gCon3rr3 ph ps ch hyp_impi_1)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gExpi (ph ps ch : SemanticCore.Wff) (hyp_expi_1 : Nominal.NPrf ((ph.imp ps.neg).neg.imp ch)) : Nominal.NPrf (ph.imp (ps.imp ch))

Checked nominal proof certificate identified upstream as g_expi.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSimprim (ph ps : SemanticCore.Wff) : Nominal.NPrf ((ph.imp ps.neg).neg.imp ps)

Checked nominal proof certificate identified upstream as g_simprim.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gSimprim ph ps = NFChoice.DirectNominalPrf.WPPReplay.gImpi ph ps ps (NFChoice.DirectNominalPrf.WPPReplay.gIdd ph ps)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSimplim (ph ps : SemanticCore.Wff) : Nominal.NPrf ((ph.imp ps).neg.imp ph)

Checked nominal proof certificate identified upstream as g_simplim.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gSimplim ph ps = NFChoice.DirectNominalPrf.WPPReplay.gCon1i ph (ph.imp ps) (NFChoice.DirectNominalPrf.WPPReplay.gPm221 ph ps)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPm261d (ph ps ch : SemanticCore.Wff) (hyp_pm2_61d_1 : Nominal.NPrf (ph.imp (ps.imp ch))) (hyp_pm2_61d_2 : Nominal.NPrf (ph.imp (ps.neg.imp ch))) : Nominal.NPrf (ph.imp ch)

Checked nominal proof certificate identified upstream as g_pm2_61d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPm261d1 (ph ps ch : SemanticCore.Wff) (hyp_pm2_61d1_1 : Nominal.NPrf (ph.imp (ps.imp ch))) (hyp_pm2_61d1_2 : Nominal.NPrf (ps.neg.imp ch)) : Nominal.NPrf (ph.imp ch)

Checked nominal proof certificate identified upstream as g_pm2_61d1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPm261d2 (ph ps ch : SemanticCore.Wff) (hyp_pm2_61d2_1 : Nominal.NPrf (ph.imp (ps.neg.imp ch))) (hyp_pm2_61d2_2 : Nominal.NPrf (ps.imp ch)) : Nominal.NPrf (ph.imp ch)

Checked nominal proof certificate identified upstream as g_pm2_61d2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gJa (ph ps ch : SemanticCore.Wff) (hyp_ja_1 : Nominal.NPrf (ph.neg.imp ch)) (hyp_ja_2 : Nominal.NPrf (ps.imp ch)) : Nominal.NPrf ((ph.imp ps).imp ch)

Checked nominal proof certificate identified upstream as g_ja.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPm261i (ph ps : SemanticCore.Wff) (hyp_pm2_61i_1 : Nominal.NPrf (ph.imp ps)) (hyp_pm2_61i_2 : Nominal.NPrf (ph.neg.imp ps)) : Nominal.NPrf ps

Checked nominal proof certificate identified upstream as g_pm2_61i.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPm261ii (ph ps ch : SemanticCore.Wff) (hyp_pm2_61ii_1 : Nominal.NPrf (ph.neg.imp (ps.neg.imp ch))) (hyp_pm2_61ii_2 : Nominal.NPrf (ph.imp ch)) (hyp_pm2_61ii_3 : Nominal.NPrf (ps.imp ch)) : Nominal.NPrf ch

Checked nominal proof certificate identified upstream as g_pm2_61ii.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPm201d (ph ps : SemanticCore.Wff) (hyp_pm2_01d_1 : Nominal.NPrf (ph.imp (ps.imp ps.neg))) : Nominal.NPrf (ph.imp ps.neg)

Checked nominal proof certificate identified upstream as g_pm2_01d.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gPm201d ph ps hyp_pm2_01d_1 = NFChoice.DirectNominalPrf.WPPReplay.gPm261d1 ph ps ps.neg hyp_pm2_01d_1 (NFChoice.DirectNominalPrf.WPPReplay.gId ps.neg)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPm265i (ph ps : SemanticCore.Wff) (hyp_pm2_65i_1 : Nominal.NPrf (ph.imp ps)) (hyp_pm2_65i_2 : Nominal.NPrf (ph.imp ps.neg)) : Nominal.NPrf ph.neg

Checked nominal proof certificate identified upstream as g_pm2_65i.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPm265d (ph ps ch : SemanticCore.Wff) (hyp_pm2_65d_1 : Nominal.NPrf (ph.imp (ps.imp ch))) (hyp_pm2_65d_2 : Nominal.NPrf (ph.imp (ps.imp ch.neg))) : Nominal.NPrf (ph.imp ps.neg)

Checked nominal proof certificate identified upstream as g_pm2_65d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMto (ph ps : SemanticCore.Wff) (hyp_mto_1 : Nominal.NPrf ps.neg) (hyp_mto_2 : Nominal.NPrf (ph.imp ps)) : Nominal.NPrf ph.neg

Checked nominal proof certificate identified upstream as g_mto.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gMto ph ps hyp_mto_1 hyp_mto_2 = NFChoice.DirectNominalPrf.WPPReplay.gPm265i ph ps hyp_mto_2 (NFChoice.DirectNominalPrf.WPPReplay.gA1i ps.neg ph hyp_mto_1)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMtod (ph ps ch : SemanticCore.Wff) (hyp_mtod_1 : Nominal.NPrf (ph.imp ch.neg)) (hyp_mtod_2 : Nominal.NPrf (ph.imp (ps.imp ch))) : Nominal.NPrf (ph.imp ps.neg)

Checked nominal proof certificate identified upstream as g_mtod.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMtoi (ph ps ch : SemanticCore.Wff) (hyp_mtoi_1 : Nominal.NPrf ch.neg) (hyp_mtoi_2 : Nominal.NPrf (ph.imp (ps.imp ch))) : Nominal.NPrf (ph.imp ps.neg)

Checked nominal proof certificate identified upstream as g_mtoi.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMt2 (ph ps : SemanticCore.Wff) (hyp_mt2_1 : Nominal.NPrf ps) (hyp_mt2_2 : Nominal.NPrf (ph.imp ps.neg)) : Nominal.NPrf ph.neg

Checked nominal proof certificate identified upstream as g_mt2.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gMt2 ph ps hyp_mt2_1 hyp_mt2_2 = NFChoice.DirectNominalPrf.WPPReplay.gPm265i ph ps (NFChoice.DirectNominalPrf.WPPReplay.gA1i ps ph hyp_mt2_1) hyp_mt2_2

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMt3 (ph ps : SemanticCore.Wff) (hyp_mt3_1 : Nominal.NPrf ps.neg) (hyp_mt3_2 : Nominal.NPrf (ph.neg.imp ps)) : Nominal.NPrf ph

Checked nominal proof certificate identified upstream as g_mt3.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gMt3 ph ps hyp_mt3_1 hyp_mt3_2 = NFChoice.DirectNominalPrf.WPPReplay.gNotnotri ph (NFChoice.DirectNominalPrf.WPPReplay.gMto ph.neg ps hyp_mt3_1 hyp_mt3_2)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBi1 (ph ps : SemanticCore.Wff) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWb ph ps).imp (ph.imp ps))

Checked nominal proof certificate identified upstream as g_bi1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBi3 (ph ps : SemanticCore.Wff) : Nominal.NPrf ((ph.imp ps).imp ((ps.imp ph).imp (Compiler.CompactSourceSyntax.synWb ph ps)))

Checked nominal proof certificate identified upstream as g_bi3.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gImpbii (ph ps : SemanticCore.Wff) (hyp_impbii_1 : Nominal.NPrf (ph.imp ps)) (hyp_impbii_2 : Nominal.NPrf (ps.imp ph)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph ps)

Checked nominal proof certificate identified upstream as g_impbii.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gImpbidd (ph ps ch th : SemanticCore.Wff) (hyp_impbidd_1 : Nominal.NPrf (ph.imp (ps.imp (ch.imp th)))) (hyp_impbidd_2 : Nominal.NPrf (ph.imp (ps.imp (th.imp ch)))) : Nominal.NPrf (ph.imp (ps.imp (Compiler.CompactSourceSyntax.synWb ch th)))

Checked nominal proof certificate identified upstream as g_impbidd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gImpbid21d (ph ps ch th : SemanticCore.Wff) (hyp_impbid21d_1 : Nominal.NPrf (ps.imp (ch.imp th))) (hyp_impbid21d_2 : Nominal.NPrf (ph.imp (th.imp ch))) : Nominal.NPrf (ph.imp (ps.imp (Compiler.CompactSourceSyntax.synWb ch th)))

Checked nominal proof certificate identified upstream as g_impbid21d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gImpbid (ph ps ch : SemanticCore.Wff) (hyp_impbid_1 : Nominal.NPrf (ph.imp (ps.imp ch))) (hyp_impbid_2 : Nominal.NPrf (ph.imp (ch.imp ps))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))

Checked nominal proof certificate identified upstream as g_impbid.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDfbi1 (ph ps : SemanticCore.Wff) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWb ph ps) ((ph.imp ps).imp (ps.imp ph).neg).neg)

Checked nominal proof certificate identified upstream as g_dfbi1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBiimpi (ph ps : SemanticCore.Wff) (hyp_biimpi_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph ps)) : Nominal.NPrf (ph.imp ps)

Checked nominal proof certificate identified upstream as g_biimpi.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gBiimpi ph ps hyp_biimpi_1 = NFChoice.DirectNominalPrf.Nominal.mp hyp_biimpi_1 (NFChoice.DirectNominalPrf.WPPReplay.gBi1 ph ps)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSylbi (ph ps ch : SemanticCore.Wff) (hyp_sylbi_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph ps)) (hyp_sylbi_2 : Nominal.NPrf (ps.imp ch)) : Nominal.NPrf (ph.imp ch)

Checked nominal proof certificate identified upstream as g_sylbi.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSylib (ph ps ch : SemanticCore.Wff) (hyp_sylib_1 : Nominal.NPrf (ph.imp ps)) (hyp_sylib_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ps ch)) : Nominal.NPrf (ph.imp ch)

Checked nominal proof certificate identified upstream as g_sylib.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBi2 (ph ps : SemanticCore.Wff) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWb ph ps).imp (ps.imp ph))

Checked nominal proof certificate identified upstream as g_bi2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBicom1 (ph ps : SemanticCore.Wff) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWb ph ps).imp (Compiler.CompactSourceSyntax.synWb ps ph))

Checked nominal proof certificate identified upstream as g_bicom1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBicom (ph ps : SemanticCore.Wff) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWb ph ps) (Compiler.CompactSourceSyntax.synWb ps ph))

Checked nominal proof certificate identified upstream as g_bicom.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBicomd (ph ps ch : SemanticCore.Wff) (hyp_bicomd_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ch ps))

Checked nominal proof certificate identified upstream as g_bicomd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBicomi (ph ps : SemanticCore.Wff) (hyp_bicomi_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph ps)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ps ph)

Checked nominal proof certificate identified upstream as g_bicomi.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gBicomi ph ps hyp_bicomi_1 = NFChoice.DirectNominalPrf.Nominal.mp hyp_bicomi_1 (NFChoice.DirectNominalPrf.WPPReplay.gBicom1 ph ps)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gImpbid1 (ph ps ch : SemanticCore.Wff) (hyp_impbid1_1 : Nominal.NPrf (ph.imp (ps.imp ch))) (hyp_impbid1_2 : Nominal.NPrf (ch.imp ps)) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))

Checked nominal proof certificate identified upstream as g_impbid1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gImpbid2 (ph ps ch : SemanticCore.Wff) (hyp_impbid2_1 : Nominal.NPrf (ps.imp ch)) (hyp_impbid2_2 : Nominal.NPrf (ph.imp (ch.imp ps))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))

Checked nominal proof certificate identified upstream as g_impbid2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gImpcon4bid (ph ps ch : SemanticCore.Wff) (hyp_impcon4bid_1 : Nominal.NPrf (ph.imp (ps.imp ch))) (hyp_impcon4bid_2 : Nominal.NPrf (ph.imp (ps.neg.imp ch.neg))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))

Checked nominal proof certificate identified upstream as g_impcon4bid.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBiimpri (ph ps : SemanticCore.Wff) (hyp_biimpri_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph ps)) : Nominal.NPrf (ps.imp ph)

Checked nominal proof certificate identified upstream as g_biimpri.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gBiimpri ph ps hyp_biimpri_1 = NFChoice.DirectNominalPrf.WPPReplay.gBiimpi ps ph (NFChoice.DirectNominalPrf.WPPReplay.gBicomi ph ps hyp_biimpri_1)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBiimpd (ph ps ch : SemanticCore.Wff) (hyp_biimpd_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) : Nominal.NPrf (ph.imp (ps.imp ch))

Checked nominal proof certificate identified upstream as g_biimpd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMpbi (ph ps : SemanticCore.Wff) (hyp_mpbi_min : Nominal.NPrf ph) (hyp_mpbi_maj : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph ps)) : Nominal.NPrf ps

Checked nominal proof certificate identified upstream as g_mpbi.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gMpbi ph ps hyp_mpbi_min hyp_mpbi_maj = NFChoice.DirectNominalPrf.Nominal.mp hyp_mpbi_min (NFChoice.DirectNominalPrf.WPPReplay.gBiimpi ph ps hyp_mpbi_maj)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMpbir (ph ps : SemanticCore.Wff) (hyp_mpbir_min : Nominal.NPrf ps) (hyp_mpbir_maj : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph ps)) : Nominal.NPrf ph

Checked nominal proof certificate identified upstream as g_mpbir.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gMpbir ph ps hyp_mpbir_min hyp_mpbir_maj = NFChoice.DirectNominalPrf.Nominal.mp hyp_mpbir_min (NFChoice.DirectNominalPrf.WPPReplay.gBiimpri ph ps hyp_mpbir_maj)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMpbid (ph ps ch : SemanticCore.Wff) (hyp_mpbid_min : Nominal.NPrf (ph.imp ps)) (hyp_mpbid_maj : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) : Nominal.NPrf (ph.imp ch)

Checked nominal proof certificate identified upstream as g_mpbid.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMpbii (ph ps ch : SemanticCore.Wff) (hyp_mpbii_min : Nominal.NPrf ps) (hyp_mpbii_maj : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) : Nominal.NPrf (ph.imp ch)

Checked nominal proof certificate identified upstream as g_mpbii.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSylibr (ph ps ch : SemanticCore.Wff) (hyp_sylibr_1 : Nominal.NPrf (ph.imp ps)) (hyp_sylibr_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ch ps)) : Nominal.NPrf (ph.imp ch)

Checked nominal proof certificate identified upstream as g_sylibr.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSylbir (ph ps ch : SemanticCore.Wff) (hyp_sylbir_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ps ph)) (hyp_sylbir_2 : Nominal.NPrf (ps.imp ch)) : Nominal.NPrf (ph.imp ch)

Checked nominal proof certificate identified upstream as g_sylbir.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSylibd (ph ps ch th : SemanticCore.Wff) (hyp_sylibd_1 : Nominal.NPrf (ph.imp (ps.imp ch))) (hyp_sylibd_2 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ch th))) : Nominal.NPrf (ph.imp (ps.imp th))

Checked nominal proof certificate identified upstream as g_sylibd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSylbid (ph ps ch th : SemanticCore.Wff) (hyp_sylbid_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) (hyp_sylbid_2 : Nominal.NPrf (ph.imp (ch.imp th))) : Nominal.NPrf (ph.imp (ps.imp th))

Checked nominal proof certificate identified upstream as g_sylbid.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMpbidi (ph ps ch th : SemanticCore.Wff) (hyp_mpbidi_min : Nominal.NPrf (th.imp (ph.imp ps))) (hyp_mpbidi_maj : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) : Nominal.NPrf (th.imp (ph.imp ch))

Checked nominal proof certificate identified upstream as g_mpbidi.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSyl5bi (ph ps ch th : SemanticCore.Wff) (hyp_syl5bi_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph ps)) (hyp_syl5bi_2 : Nominal.NPrf (ch.imp (ps.imp th))) : Nominal.NPrf (ch.imp (ph.imp th))

Checked nominal proof certificate identified upstream as g_syl5bi.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSyl5bir (ph ps ch th : SemanticCore.Wff) (hyp_syl5bir_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ps ph)) (hyp_syl5bir_2 : Nominal.NPrf (ch.imp (ps.imp th))) : Nominal.NPrf (ch.imp (ph.imp th))

Checked nominal proof certificate identified upstream as g_syl5bir.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSyl5ib (ph ps ch th : SemanticCore.Wff) (hyp_syl5ib_1 : Nominal.NPrf (ph.imp ps)) (hyp_syl5ib_2 : Nominal.NPrf (ch.imp (Compiler.CompactSourceSyntax.synWb ps th))) : Nominal.NPrf (ch.imp (ph.imp th))

Checked nominal proof certificate identified upstream as g_syl5ib.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSyl5ibcom (ph ps ch th : SemanticCore.Wff) (hyp_syl5ib_1 : Nominal.NPrf (ph.imp ps)) (hyp_syl5ib_2 : Nominal.NPrf (ch.imp (Compiler.CompactSourceSyntax.synWb ps th))) : Nominal.NPrf (ph.imp (ch.imp th))

Checked nominal proof certificate identified upstream as g_syl5ibcom.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSyl5ibr (ph ps ch th : SemanticCore.Wff) (hyp_syl5ibr_1 : Nominal.NPrf (ph.imp th)) (hyp_syl5ibr_2 : Nominal.NPrf (ch.imp (Compiler.CompactSourceSyntax.synWb ps th))) : Nominal.NPrf (ch.imp (ph.imp ps))

Checked nominal proof certificate identified upstream as g_syl5ibr.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSyl5ibrcom (ph ps ch th : SemanticCore.Wff) (hyp_syl5ibr_1 : Nominal.NPrf (ph.imp th)) (hyp_syl5ibr_2 : Nominal.NPrf (ch.imp (Compiler.CompactSourceSyntax.synWb ps th))) : Nominal.NPrf (ph.imp (ch.imp ps))

Checked nominal proof certificate identified upstream as g_syl5ibrcom.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBiimprd (ph ps ch : SemanticCore.Wff) (hyp_biimprd_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) : Nominal.NPrf (ph.imp (ch.imp ps))

Checked nominal proof certificate identified upstream as g_biimprd.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gBiimprd ph ps ch hyp_biimprd_1 = NFChoice.DirectNominalPrf.WPPReplay.gSyl5ibr ch ps ph ch (NFChoice.DirectNominalPrf.WPPReplay.gId ch) hyp_biimprd_1

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBiimpcd (ph ps ch : SemanticCore.Wff) (hyp_biimpcd_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) : Nominal.NPrf (ps.imp (ph.imp ch))

Checked nominal proof certificate identified upstream as g_biimpcd.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gBiimpcd ph ps ch hyp_biimpcd_1 = NFChoice.DirectNominalPrf.WPPReplay.gSyl5ibcom ps ps ph ch (NFChoice.DirectNominalPrf.WPPReplay.gId ps) hyp_biimpcd_1

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBiimprcd (ph ps ch : SemanticCore.Wff) (hyp_biimpcd_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) : Nominal.NPrf (ch.imp (ph.imp ps))

Checked nominal proof certificate identified upstream as g_biimprcd.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gBiimprcd ph ps ch hyp_biimpcd_1 = NFChoice.DirectNominalPrf.WPPReplay.gSyl5ibrcom ch ps ph ch (NFChoice.DirectNominalPrf.WPPReplay.gId ch) hyp_biimpcd_1

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSyl6ib (ph ps ch th : SemanticCore.Wff) (hyp_syl6ib_1 : Nominal.NPrf (ph.imp (ps.imp ch))) (hyp_syl6ib_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ch th)) : Nominal.NPrf (ph.imp (ps.imp th))

Checked nominal proof certificate identified upstream as g_syl6ib.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSyl6ibr (ph ps ch th : SemanticCore.Wff) (hyp_syl6ibr_1 : Nominal.NPrf (ph.imp (ps.imp ch))) (hyp_syl6ibr_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb th ch)) : Nominal.NPrf (ph.imp (ps.imp th))

Checked nominal proof certificate identified upstream as g_syl6ibr.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSyl6bi (ph ps ch th : SemanticCore.Wff) (hyp_syl6bi_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) (hyp_syl6bi_2 : Nominal.NPrf (ch.imp th)) : Nominal.NPrf (ph.imp (ps.imp th))

Checked nominal proof certificate identified upstream as g_syl6bi.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSyl6bir (ph ps ch th : SemanticCore.Wff) (hyp_syl6bir_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ch ps))) (hyp_syl6bir_2 : Nominal.NPrf (ch.imp th)) : Nominal.NPrf (ph.imp (ps.imp th))

Checked nominal proof certificate identified upstream as g_syl6bir.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSyl7bi (ph ps ch th ta : SemanticCore.Wff) (hyp_syl7bi_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph ps)) (hyp_syl7bi_2 : Nominal.NPrf (ch.imp (th.imp (ps.imp ta)))) : Nominal.NPrf (ch.imp (th.imp (ph.imp ta)))

Checked nominal proof certificate identified upstream as g_syl7bi.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSyl8ib (ph ps ch th ta : SemanticCore.Wff) (hyp_syl8ib_1 : Nominal.NPrf (ph.imp (ps.imp (ch.imp th)))) (hyp_syl8ib_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb th ta)) : Nominal.NPrf (ph.imp (ps.imp (ch.imp ta)))

Checked nominal proof certificate identified upstream as g_syl8ib.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMpbird (ph ps ch : SemanticCore.Wff) (hyp_mpbird_min : Nominal.NPrf (ph.imp ch)) (hyp_mpbird_maj : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) : Nominal.NPrf (ph.imp ps)

Checked nominal proof certificate identified upstream as g_mpbird.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMpbiri (ph ps ch : SemanticCore.Wff) (hyp_mpbiri_min : Nominal.NPrf ch) (hyp_mpbiri_maj : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) : Nominal.NPrf (ph.imp ps)

Checked nominal proof certificate identified upstream as g_mpbiri.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSylibrd (ph ps ch th : SemanticCore.Wff) (hyp_sylibrd_1 : Nominal.NPrf (ph.imp (ps.imp ch))) (hyp_sylibrd_2 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb th ch))) : Nominal.NPrf (ph.imp (ps.imp th))

Checked nominal proof certificate identified upstream as g_sylibrd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSylbird (ph ps ch th : SemanticCore.Wff) (hyp_sylbird_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ch ps))) (hyp_sylbird_2 : Nominal.NPrf (ph.imp (ch.imp th))) : Nominal.NPrf (ph.imp (ps.imp th))

Checked nominal proof certificate identified upstream as g_sylbird.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBiid (ph : SemanticCore.Wff) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph ph)

Checked nominal proof certificate identified upstream as g_biid.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gBiid ph = NFChoice.DirectNominalPrf.WPPReplay.gImpbii ph ph (NFChoice.DirectNominalPrf.WPPReplay.gId ph) (NFChoice.DirectNominalPrf.WPPReplay.gId ph)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBiidd (ph ps : SemanticCore.Wff) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ps))

Checked nominal proof certificate identified upstream as g_biidd.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gBiidd ph ps = NFChoice.DirectNominalPrf.WPPReplay.gA1i (NFChoice.Compiler.CompactSourceSyntax.synWb ps ps) ph (NFChoice.DirectNominalPrf.WPPReplay.gBiid ps)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPm51im (ph ps : SemanticCore.Wff) : Nominal.NPrf (ph.imp (ps.imp (Compiler.CompactSourceSyntax.synWb ph ps)))

Checked nominal proof certificate identified upstream as g_pm5_1im.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN2th (ph ps : SemanticCore.Wff) (hyp_n_2th_1 : Nominal.NPrf ph) (hyp_n_2th_2 : Nominal.NPrf ps) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph ps)

Checked nominal proof certificate identified upstream as g_n_2th.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN2thd (ph ps ch : SemanticCore.Wff) (hyp_n_2thd_1 : Nominal.NPrf (ph.imp ps)) (hyp_n_2thd_2 : Nominal.NPrf (ph.imp ch)) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))

Checked nominal proof certificate identified upstream as g_n_2thd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIbi (ph ps : SemanticCore.Wff) (hyp_ibi_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ph ps))) : Nominal.NPrf (ph.imp ps)

Checked nominal proof certificate identified upstream as g_ibi.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gIbi ph ps hyp_ibi_1 = NFChoice.DirectNominalPrf.WPPReplay.gPm243i ph ps (NFChoice.DirectNominalPrf.WPPReplay.gBiimpd ph ph ps hyp_ibi_1)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIbir (ph ps : SemanticCore.Wff) (hyp_ibir_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ph))) : Nominal.NPrf (ph.imp ps)

Checked nominal proof certificate identified upstream as g_ibir.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gIbir ph ps hyp_ibir_1 = NFChoice.DirectNominalPrf.WPPReplay.gIbi ph ps (NFChoice.DirectNominalPrf.WPPReplay.gBicomd ph ps ph hyp_ibir_1)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIbd (ph ps ch : SemanticCore.Wff) (hyp_ibd_1 : Nominal.NPrf (ph.imp (ps.imp (Compiler.CompactSourceSyntax.synWb ps ch)))) : Nominal.NPrf (ph.imp (ps.imp ch))

Checked nominal proof certificate identified upstream as g_ibd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPm574 (ph ps ch : SemanticCore.Wff) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch)) (Compiler.CompactSourceSyntax.synWb (ph.imp ps) (ph.imp ch)))

Checked nominal proof certificate identified upstream as g_pm5_74.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPm574i (ph ps ch : SemanticCore.Wff) (hyp_pm5_74i_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (ph.imp ps) (ph.imp ch))

Checked nominal proof certificate identified upstream as g_pm5_74i.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPm574ri (ph ps ch : SemanticCore.Wff) (hyp_pm5_74ri_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (ph.imp ps) (ph.imp ch))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))

Checked nominal proof certificate identified upstream as g_pm5_74ri.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPm574d (ph ps ch th : SemanticCore.Wff) (hyp_pm5_74d_1 : Nominal.NPrf (ph.imp (ps.imp (Compiler.CompactSourceSyntax.synWb ch th)))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb (ps.imp ch) (ps.imp th)))

Checked nominal proof certificate identified upstream as g_pm5_74d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBitri (ph ps ch : SemanticCore.Wff) (hyp_bitri_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph ps)) (hyp_bitri_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ps ch)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph ch)

Checked nominal proof certificate identified upstream as g_bitri.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBitr2i (ph ps ch : SemanticCore.Wff) (hyp_bitr2i_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph ps)) (hyp_bitr2i_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ps ch)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ch ph)

Checked nominal proof certificate identified upstream as g_bitr2i.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBitr3i (ph ps ch : SemanticCore.Wff) (hyp_bitr3i_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ps ph)) (hyp_bitr3i_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ps ch)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph ch)

Checked nominal proof certificate identified upstream as g_bitr3i.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBitr4i (ph ps ch : SemanticCore.Wff) (hyp_bitr4i_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph ps)) (hyp_bitr4i_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ch ps)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph ch)

Checked nominal proof certificate identified upstream as g_bitr4i.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBitrd (ph ps ch th : SemanticCore.Wff) (hyp_bitrd_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) (hyp_bitrd_2 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ch th))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps th))

Checked nominal proof certificate identified upstream as g_bitrd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBitr2d (ph ps ch th : SemanticCore.Wff) (hyp_bitr2d_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) (hyp_bitr2d_2 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ch th))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb th ps))

Checked nominal proof certificate identified upstream as g_bitr2d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBitr3d (ph ps ch th : SemanticCore.Wff) (hyp_bitr3d_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) (hyp_bitr3d_2 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps th))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ch th))

Checked nominal proof certificate identified upstream as g_bitr3d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBitr4d (ph ps ch th : SemanticCore.Wff) (hyp_bitr4d_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) (hyp_bitr4d_2 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb th ch))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps th))

Checked nominal proof certificate identified upstream as g_bitr4d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSyl5bb (ph ps ch th : SemanticCore.Wff) (hyp_syl5bb_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph ps)) (hyp_syl5bb_2 : Nominal.NPrf (ch.imp (Compiler.CompactSourceSyntax.synWb ps th))) : Nominal.NPrf (ch.imp (Compiler.CompactSourceSyntax.synWb ph th))

Checked nominal proof certificate identified upstream as g_syl5bb.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSyl5rbb (ph ps ch th : SemanticCore.Wff) (hyp_syl5rbb_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph ps)) (hyp_syl5rbb_2 : Nominal.NPrf (ch.imp (Compiler.CompactSourceSyntax.synWb ps th))) : Nominal.NPrf (ch.imp (Compiler.CompactSourceSyntax.synWb th ph))

Checked nominal proof certificate identified upstream as g_syl5rbb.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSyl5bbr (ph ps ch th : SemanticCore.Wff) (hyp_syl5bbr_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ps ph)) (hyp_syl5bbr_2 : Nominal.NPrf (ch.imp (Compiler.CompactSourceSyntax.synWb ps th))) : Nominal.NPrf (ch.imp (Compiler.CompactSourceSyntax.synWb ph th))

Checked nominal proof certificate identified upstream as g_syl5bbr.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSyl5rbbr (ph ps ch th : SemanticCore.Wff) (hyp_syl5rbbr_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ps ph)) (hyp_syl5rbbr_2 : Nominal.NPrf (ch.imp (Compiler.CompactSourceSyntax.synWb ps th))) : Nominal.NPrf (ch.imp (Compiler.CompactSourceSyntax.synWb th ph))

Checked nominal proof certificate identified upstream as g_syl5rbbr.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSyl6bb (ph ps ch th : SemanticCore.Wff) (hyp_syl6bb_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) (hyp_syl6bb_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ch th)) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps th))

Checked nominal proof certificate identified upstream as g_syl6bb.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSyl6rbb (ph ps ch th : SemanticCore.Wff) (hyp_syl6rbb_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) (hyp_syl6rbb_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ch th)) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb th ps))

Checked nominal proof certificate identified upstream as g_syl6rbb.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSyl6bbr (ph ps ch th : SemanticCore.Wff) (hyp_syl6bbr_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) (hyp_syl6bbr_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb th ch)) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps th))

Checked nominal proof certificate identified upstream as g_syl6bbr.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSyl6rbbr (ph ps ch th : SemanticCore.Wff) (hyp_syl6rbbr_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) (hyp_syl6rbbr_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb th ch)) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb th ps))

Checked nominal proof certificate identified upstream as g_syl6rbbr.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN3imtr3i (ph ps ch th : SemanticCore.Wff) (hyp_n_3imtr3_1 : Nominal.NPrf (ph.imp ps)) (hyp_n_3imtr3_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph ch)) (hyp_n_3imtr3_3 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ps th)) : Nominal.NPrf (ch.imp th)

Checked nominal proof certificate identified upstream as g_n_3imtr3i.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN3imtr4i (ph ps ch th : SemanticCore.Wff) (hyp_n_3imtr4_1 : Nominal.NPrf (ph.imp ps)) (hyp_n_3imtr4_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ch ph)) (hyp_n_3imtr4_3 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb th ps)) : Nominal.NPrf (ch.imp th)

Checked nominal proof certificate identified upstream as g_n_3imtr4i.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN3imtr3d (ph ps ch th ta : SemanticCore.Wff) (hyp_n_3imtr3d_1 : Nominal.NPrf (ph.imp (ps.imp ch))) (hyp_n_3imtr3d_2 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps th))) (hyp_n_3imtr3d_3 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ch ta))) : Nominal.NPrf (ph.imp (th.imp ta))

Checked nominal proof certificate identified upstream as g_n_3imtr3d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN3imtr4d (ph ps ch th ta : SemanticCore.Wff) (hyp_n_3imtr4d_1 : Nominal.NPrf (ph.imp (ps.imp ch))) (hyp_n_3imtr4d_2 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb th ps))) (hyp_n_3imtr4d_3 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ta ch))) : Nominal.NPrf (ph.imp (th.imp ta))

Checked nominal proof certificate identified upstream as g_n_3imtr4d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN3imtr3g (ph ps ch th ta : SemanticCore.Wff) (hyp_n_3imtr3g_1 : Nominal.NPrf (ph.imp (ps.imp ch))) (hyp_n_3imtr3g_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ps th)) (hyp_n_3imtr3g_3 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ch ta)) : Nominal.NPrf (ph.imp (th.imp ta))

Checked nominal proof certificate identified upstream as g_n_3imtr3g.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN3imtr4g (ph ps ch th ta : SemanticCore.Wff) (hyp_n_3imtr4g_1 : Nominal.NPrf (ph.imp (ps.imp ch))) (hyp_n_3imtr4g_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb th ps)) (hyp_n_3imtr4g_3 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ta ch)) : Nominal.NPrf (ph.imp (th.imp ta))

Checked nominal proof certificate identified upstream as g_n_3imtr4g.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN3bitri (ph ps ch th : SemanticCore.Wff) (hyp_n_3bitri_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph ps)) (hyp_n_3bitri_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ps ch)) (hyp_n_3bitri_3 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ch th)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph th)

Checked nominal proof certificate identified upstream as g_n_3bitri.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN3bitrri (ph ps ch th : SemanticCore.Wff) (hyp_n_3bitri_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph ps)) (hyp_n_3bitri_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ps ch)) (hyp_n_3bitri_3 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ch th)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb th ph)

Checked nominal proof certificate identified upstream as g_n_3bitrri.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN3bitr2i (ph ps ch th : SemanticCore.Wff) (hyp_n_3bitr2i_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph ps)) (hyp_n_3bitr2i_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ch ps)) (hyp_n_3bitr2i_3 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ch th)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph th)

Checked nominal proof certificate identified upstream as g_n_3bitr2i.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN3bitr2ri (ph ps ch th : SemanticCore.Wff) (hyp_n_3bitr2i_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph ps)) (hyp_n_3bitr2i_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ch ps)) (hyp_n_3bitr2i_3 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ch th)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb th ph)

Checked nominal proof certificate identified upstream as g_n_3bitr2ri.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN3bitr3i (ph ps ch th : SemanticCore.Wff) (hyp_n_3bitr3i_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph ps)) (hyp_n_3bitr3i_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph ch)) (hyp_n_3bitr3i_3 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ps th)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ch th)

Checked nominal proof certificate identified upstream as g_n_3bitr3i.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN3bitr3ri (ph ps ch th : SemanticCore.Wff) (hyp_n_3bitr3i_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph ps)) (hyp_n_3bitr3i_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph ch)) (hyp_n_3bitr3i_3 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ps th)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb th ch)

Checked nominal proof certificate identified upstream as g_n_3bitr3ri.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN3bitr4i (ph ps ch th : SemanticCore.Wff) (hyp_n_3bitr4i_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph ps)) (hyp_n_3bitr4i_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ch ph)) (hyp_n_3bitr4i_3 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb th ps)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ch th)

Checked nominal proof certificate identified upstream as g_n_3bitr4i.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN3bitr4ri (ph ps ch th : SemanticCore.Wff) (hyp_n_3bitr4i_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph ps)) (hyp_n_3bitr4i_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ch ph)) (hyp_n_3bitr4i_3 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb th ps)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb th ch)

Checked nominal proof certificate identified upstream as g_n_3bitr4ri.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN3bitrd (ph ps ch th ta : SemanticCore.Wff) (hyp_n_3bitrd_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) (hyp_n_3bitrd_2 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ch th))) (hyp_n_3bitrd_3 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb th ta))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ta))

Checked nominal proof certificate identified upstream as g_n_3bitrd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN3bitr2rd (ph ps ch th ta : SemanticCore.Wff) (hyp_n_3bitr2d_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) (hyp_n_3bitr2d_2 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb th ch))) (hyp_n_3bitr2d_3 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb th ta))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ta ps))

Checked nominal proof certificate identified upstream as g_n_3bitr2rd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN3bitr3d (ph ps ch th ta : SemanticCore.Wff) (hyp_n_3bitr3d_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) (hyp_n_3bitr3d_2 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps th))) (hyp_n_3bitr3d_3 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ch ta))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb th ta))

Checked nominal proof certificate identified upstream as g_n_3bitr3d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN3bitr4d (ph ps ch th ta : SemanticCore.Wff) (hyp_n_3bitr4d_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) (hyp_n_3bitr4d_2 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb th ps))) (hyp_n_3bitr4d_3 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ta ch))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb th ta))

Checked nominal proof certificate identified upstream as g_n_3bitr4d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN3bitr3g (ph ps ch th ta : SemanticCore.Wff) (hyp_n_3bitr3g_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) (hyp_n_3bitr3g_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ps th)) (hyp_n_3bitr3g_3 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ch ta)) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb th ta))

Checked nominal proof certificate identified upstream as g_n_3bitr3g.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN3bitr4g (ph ps ch th ta : SemanticCore.Wff) (hyp_n_3bitr4g_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) (hyp_n_3bitr4g_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb th ps)) (hyp_n_3bitr4g_3 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ta ch)) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb th ta))

Checked nominal proof certificate identified upstream as g_n_3bitr4g.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNotnot (ph : SemanticCore.Wff) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph ph.neg.neg)

Checked nominal proof certificate identified upstream as g_notnot.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCon34b (ph ps : SemanticCore.Wff) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (ph.imp ps) (ps.neg.imp ph.neg))

Checked nominal proof certificate identified upstream as g_con34b.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCon4bid (ph ps ch : SemanticCore.Wff) (hyp_con4bid_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps.neg ch.neg))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))

Checked nominal proof certificate identified upstream as g_con4bid.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNotbid (ph ps ch : SemanticCore.Wff) (hyp_notbid_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps.neg ch.neg))

Checked nominal proof certificate identified upstream as g_notbid.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNotbi (ph ps : SemanticCore.Wff) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWb ph ps) (Compiler.CompactSourceSyntax.synWb ph.neg ps.neg))

Checked nominal proof certificate identified upstream as g_notbi.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNotbii (ph ps : SemanticCore.Wff) (hyp_notbii_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph ps)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph.neg ps.neg)

Checked nominal proof certificate identified upstream as g_notbii.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCon4bii (ph ps : SemanticCore.Wff) (hyp_con4bii_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph.neg ps.neg)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph ps)

Checked nominal proof certificate identified upstream as g_con4bii.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMtbi (ph ps : SemanticCore.Wff) (hyp_mtbi_1 : Nominal.NPrf ph.neg) (hyp_mtbi_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph ps)) : Nominal.NPrf ps.neg

Checked nominal proof certificate identified upstream as g_mtbi.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gMtbi ph ps hyp_mtbi_1 hyp_mtbi_2 = NFChoice.DirectNominalPrf.WPPReplay.gMto ps ph hyp_mtbi_1 (NFChoice.DirectNominalPrf.WPPReplay.gBiimpri ph ps hyp_mtbi_2)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMtbir (ph ps : SemanticCore.Wff) (hyp_mtbir_1 : Nominal.NPrf ps.neg) (hyp_mtbir_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph ps)) : Nominal.NPrf ph.neg

Checked nominal proof certificate identified upstream as g_mtbir.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMtbid (ph ps ch : SemanticCore.Wff) (hyp_mtbid_min : Nominal.NPrf (ph.imp ps.neg)) (hyp_mtbid_maj : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) : Nominal.NPrf (ph.imp ch.neg)

Checked nominal proof certificate identified upstream as g_mtbid.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMtbird (ph ps ch : SemanticCore.Wff) (hyp_mtbird_min : Nominal.NPrf (ph.imp ch.neg)) (hyp_mtbird_maj : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) : Nominal.NPrf (ph.imp ps.neg)

Checked nominal proof certificate identified upstream as g_mtbird.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMtbii (ph ps ch : SemanticCore.Wff) (hyp_mtbii_min : Nominal.NPrf ps.neg) (hyp_mtbii_maj : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) : Nominal.NPrf (ph.imp ch.neg)

Checked nominal proof certificate identified upstream as g_mtbii.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMtbiri (ph ps ch : SemanticCore.Wff) (hyp_mtbiri_min : Nominal.NPrf ch.neg) (hyp_mtbiri_maj : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) : Nominal.NPrf (ph.imp ps.neg)

Checked nominal proof certificate identified upstream as g_mtbiri.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSylnib (ph ps ch : SemanticCore.Wff) (hyp_sylnib_1 : Nominal.NPrf (ph.imp ps.neg)) (hyp_sylnib_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ps ch)) : Nominal.NPrf (ph.imp ch.neg)

Checked nominal proof certificate identified upstream as g_sylnib.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSylnibr (ph ps ch : SemanticCore.Wff) (hyp_sylnibr_1 : Nominal.NPrf (ph.imp ps.neg)) (hyp_sylnibr_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ch ps)) : Nominal.NPrf (ph.imp ch.neg)

Checked nominal proof certificate identified upstream as g_sylnibr.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSylnbi (ph ps ch : SemanticCore.Wff) (hyp_sylnbi_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph ps)) (hyp_sylnbi_2 : Nominal.NPrf (ps.neg.imp ch)) : Nominal.NPrf (ph.neg.imp ch)

Checked nominal proof certificate identified upstream as g_sylnbi.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSylnbir (ph ps ch : SemanticCore.Wff) (hyp_sylnbir_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ps ph)) (hyp_sylnbir_2 : Nominal.NPrf (ps.neg.imp ch)) : Nominal.NPrf (ph.neg.imp ch)

Checked nominal proof certificate identified upstream as g_sylnbir.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gXchnxbi (ph ps ch : SemanticCore.Wff) (hyp_xchnxbi_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph.neg ps)) (hyp_xchnxbi_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph ch)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ch.neg ps)

Checked nominal proof certificate identified upstream as g_xchnxbi.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gXchbinx (ph ps ch : SemanticCore.Wff) (hyp_xchbinx_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph ps.neg)) (hyp_xchbinx_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ps ch)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph ch.neg)

Checked nominal proof certificate identified upstream as g_xchbinx.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gXchbinxr (ph ps ch : SemanticCore.Wff) (hyp_xchbinxr_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph ps.neg)) (hyp_xchbinxr_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ch ps)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph ch.neg)

Checked nominal proof certificate identified upstream as g_xchbinxr.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gImbi2i (ph ps ch : SemanticCore.Wff) (hyp_bi_a : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph ps)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (ch.imp ph) (ch.imp ps))

Checked nominal proof certificate identified upstream as g_imbi2i.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBibi2i (ph ps ch : SemanticCore.Wff) (hyp_bibi_a : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph ps)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWb ch ph) (Compiler.CompactSourceSyntax.synWb ch ps))

Checked nominal proof certificate identified upstream as g_bibi2i.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBibi1i (ph ps ch : SemanticCore.Wff) (hyp_bibi_a : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph ps)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWb ph ch) (Compiler.CompactSourceSyntax.synWb ps ch))

Checked nominal proof certificate identified upstream as g_bibi1i.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBibi12i (ph ps ch th : SemanticCore.Wff) (hyp_bibi_a : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph ps)) (hyp_bibi12_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ch th)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWb ph ch) (Compiler.CompactSourceSyntax.synWb ps th))

Checked nominal proof certificate identified upstream as g_bibi12i.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gImbi2d (ph ps ch th : SemanticCore.Wff) (hyp_imbid_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb (th.imp ps) (th.imp ch)))

Checked nominal proof certificate identified upstream as g_imbi2d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gImbi1d (ph ps ch th : SemanticCore.Wff) (hyp_imbid_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb (ps.imp th) (ch.imp th)))

Checked nominal proof certificate identified upstream as g_imbi1d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBibi2d (ph ps ch th : SemanticCore.Wff) (hyp_imbid_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWb th ps) (Compiler.CompactSourceSyntax.synWb th ch)))

Checked nominal proof certificate identified upstream as g_bibi2d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBibi1d (ph ps ch th : SemanticCore.Wff) (hyp_imbid_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWb ps th) (Compiler.CompactSourceSyntax.synWb ch th)))

Checked nominal proof certificate identified upstream as g_bibi1d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gImbi12d (ph ps ch th ta : SemanticCore.Wff) (hyp_imbi12d_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) (hyp_imbi12d_2 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb th ta))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb (ps.imp th) (ch.imp ta)))

Checked nominal proof certificate identified upstream as g_imbi12d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBibi12d (ph ps ch th ta : SemanticCore.Wff) (hyp_imbi12d_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) (hyp_imbi12d_2 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb th ta))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWb ps th) (Compiler.CompactSourceSyntax.synWb ch ta)))

Checked nominal proof certificate identified upstream as g_bibi12d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gImbi1 (ph ps ch : SemanticCore.Wff) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWb ph ps).imp (Compiler.CompactSourceSyntax.synWb (ph.imp ch) (ps.imp ch)))

Checked nominal proof certificate identified upstream as g_imbi1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gImbi1i (ph ps ch : SemanticCore.Wff) (hyp_imbi1i_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph ps)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (ph.imp ch) (ps.imp ch))

Checked nominal proof certificate identified upstream as g_imbi1i.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gImbi1i ph ps ch hyp_imbi1i_1 = NFChoice.DirectNominalPrf.Nominal.mp hyp_imbi1i_1 (NFChoice.DirectNominalPrf.WPPReplay.gImbi1 ph ps ch)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gImbi12i (ph ps ch th : SemanticCore.Wff) (hyp_imbi12i_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph ps)) (hyp_imbi12i_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ch th)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (ph.imp ch) (ps.imp th))

Checked nominal proof certificate identified upstream as g_imbi12i.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBibi1 (ph ps ch : SemanticCore.Wff) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWb ph ps).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWb ph ch) (Compiler.CompactSourceSyntax.synWb ps ch)))

Checked nominal proof certificate identified upstream as g_bibi1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCon2bi (ph ps : SemanticCore.Wff) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWb ph ps.neg) (Compiler.CompactSourceSyntax.synWb ps ph.neg))

Checked nominal proof certificate identified upstream as g_con2bi.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCon2bid (ph ps ch : SemanticCore.Wff) (hyp_con2bid_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch.neg))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ch ps.neg))

Checked nominal proof certificate identified upstream as g_con2bid.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCon1bid (ph ps ch : SemanticCore.Wff) (hyp_con1bid_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps.neg ch))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ch.neg ps))

Checked nominal proof certificate identified upstream as g_con1bid.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCon1bii (ph ps : SemanticCore.Wff) (hyp_con1bii_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph.neg ps)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ps.neg ph)

Checked nominal proof certificate identified upstream as g_con1bii.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCon2bii (ph ps : SemanticCore.Wff) (hyp_con2bii_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph ps.neg)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ps ph.neg)

Checked nominal proof certificate identified upstream as g_con2bii.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCon2b (ph ps : SemanticCore.Wff) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (ph.imp ps.neg) (ps.imp ph.neg))

Checked nominal proof certificate identified upstream as g_con2b.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBiimt (ph ps : SemanticCore.Wff) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps (ph.imp ps)))

Checked nominal proof certificate identified upstream as g_biimt.

Equations

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