NF weak partition development: NominalWPPReplayChunk004.

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

Checked nominal proof certificate identified upstream as g_merlem11.

Equations

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

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

Checked nominal proof certificate identified upstream as g_merlem12.

Equations

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

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

Checked nominal proof certificate identified upstream as g_merlem13.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.g_luk_1 (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_luk_1.

Equations

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

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

Checked nominal proof certificate identified upstream as g_luk_2.

Equations

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

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

Checked nominal proof certificate identified upstream as g_luk_3.

Equations

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

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

Checked nominal proof certificate identified upstream as g_luklem1.

Equations

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

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

Checked nominal proof certificate identified upstream as g_luklem2.

Equations

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

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

Checked nominal proof certificate identified upstream as g_luklem3.

Equations

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

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

Checked nominal proof certificate identified upstream as g_luklem4.

Equations

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

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

Checked nominal proof certificate identified upstream as g_luklem5.

Equations

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

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

Checked nominal proof certificate identified upstream as g_ax1.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gAx1 ph ps = NFChoice.DirectNominalPrf.WPPReplay.gLuklem5 ph ps

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAlnex (ph : SemanticCore.Wff) (x : SemanticCore.Var) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.all x ph.neg) (Compiler.CompactSourceSyntax.synWex x ph).neg)

Checked nominal proof certificate identified upstream as g_alnex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gGen2 (ph : SemanticCore.Wff) (x y : SemanticCore.Var) (hyp_gen2_1 : Nominal.NPrf ph) : Nominal.NPrf (SemanticCore.Wff.all x (SemanticCore.Wff.all y ph))

Checked nominal proof certificate identified upstream as g_gen2.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gGen2 ph x y hyp_gen2_1 = NFChoice.DirectNominalPrf.Nominal.gen (NFChoice.DirectNominalPrf.Nominal.gen hyp_gen2_1 y) x

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMpg (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (hyp_mpg_1 : Nominal.NPrf ((SemanticCore.Wff.all x ph).imp ps)) (hyp_mpg_2 : Nominal.NPrf ph) : Nominal.NPrf ps

Checked nominal proof certificate identified upstream as g_mpg.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gMpg ph ps x hyp_mpg_1 hyp_mpg_2 = NFChoice.DirectNominalPrf.Nominal.mp (NFChoice.DirectNominalPrf.Nominal.gen hyp_mpg_2 x) hyp_mpg_1

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMpgbi (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (hyp_mpgbi_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.all x ph) ps)) (hyp_mpgbi_2 : Nominal.NPrf ph) : Nominal.NPrf ps

Checked nominal proof certificate identified upstream as g_mpgbi.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMpgbir (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (hyp_mpgbir_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph (SemanticCore.Wff.all x ps))) (hyp_mpgbir_2 : Nominal.NPrf ps) : Nominal.NPrf ph

Checked nominal proof certificate identified upstream as g_mpgbir.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfi (ph : SemanticCore.Wff) (x : SemanticCore.Var) (hyp_nfi_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.all x ph))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ph)

Checked nominal proof certificate identified upstream as g_nfi.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHbth (ph : SemanticCore.Wff) (x : SemanticCore.Var) (hyp_hbth_1 : Nominal.NPrf ph) : Nominal.NPrf (ph.imp (SemanticCore.Wff.all x ph))

Checked nominal proof certificate identified upstream as g_hbth.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gHbth ph x hyp_hbth_1 = NFChoice.DirectNominalPrf.WPPReplay.gA1i (NFChoice.SemanticCore.Wff.all x ph) ph (NFChoice.DirectNominalPrf.Nominal.gen hyp_hbth_1 x)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfth (ph : SemanticCore.Wff) (x : SemanticCore.Var) (hyp_hbth_1 : Nominal.NPrf ph) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ph)

Checked nominal proof certificate identified upstream as g_nfth.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gNfth ph x hyp_hbth_1 = NFChoice.DirectNominalPrf.WPPReplay.gNfi ph x (NFChoice.DirectNominalPrf.WPPReplay.gHbth ph x hyp_hbth_1)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNftru (x : SemanticCore.Var) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x Compiler.CompactSourceSyntax.synWtru)

Checked nominal proof certificate identified upstream as g_nftru.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gNftru x = NFChoice.DirectNominalPrf.WPPReplay.gNfth NFChoice.Compiler.CompactSourceSyntax.synWtru x NFChoice.DirectNominalPrf.WPPReplay.gTru

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNex (ph : SemanticCore.Wff) (x : SemanticCore.Var) (hyp_nex_1 : Nominal.NPrf ph.neg) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWex x ph).neg

Checked nominal proof certificate identified upstream as g_nex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAlim (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) : Nominal.NPrf ((SemanticCore.Wff.all x (ph.imp ps)).imp ((SemanticCore.Wff.all x ph).imp (SemanticCore.Wff.all x ps)))

Checked nominal proof certificate identified upstream as g_alim.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gAlim ph ps x = NFChoice.DirectNominalPrf.Nominal.ax5 x ph ps

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAlimi (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (hyp_alimi_1 : Nominal.NPrf (ph.imp ps)) : Nominal.NPrf ((SemanticCore.Wff.all x ph).imp (SemanticCore.Wff.all x ps))

Checked nominal proof certificate identified upstream as g_alimi.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN2alimi (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) (hyp_alimi_1 : Nominal.NPrf (ph.imp ps)) : Nominal.NPrf ((SemanticCore.Wff.all x (SemanticCore.Wff.all y ph)).imp (SemanticCore.Wff.all x (SemanticCore.Wff.all y ps)))

Checked nominal proof certificate identified upstream as g_n_2alimi.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAl2imi (ph ps ch : SemanticCore.Wff) (x : SemanticCore.Var) (hyp_al2imi_1 : Nominal.NPrf (ph.imp (ps.imp ch))) : Nominal.NPrf ((SemanticCore.Wff.all x ph).imp ((SemanticCore.Wff.all x ps).imp (SemanticCore.Wff.all x ch)))

Checked nominal proof certificate identified upstream as g_al2imi.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAlanimi (ph ps ch : SemanticCore.Wff) (x : SemanticCore.Var) (hyp_alanimi_1 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph ps).imp ch)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.all x ph) (SemanticCore.Wff.all x ps)).imp (SemanticCore.Wff.all x ch))

Checked nominal proof certificate identified upstream as g_alanimi.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAlimdh (ph ps ch : SemanticCore.Wff) (x : SemanticCore.Var) (hyp_alimdh_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.all x ph))) (hyp_alimdh_2 : Nominal.NPrf (ph.imp (ps.imp ch))) : Nominal.NPrf (ph.imp ((SemanticCore.Wff.all x ps).imp (SemanticCore.Wff.all x ch)))

Checked nominal proof certificate identified upstream as g_alimdh.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAlbi (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) : Nominal.NPrf ((SemanticCore.Wff.all x (Compiler.CompactSourceSyntax.synWb ph ps)).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.all x ph) (SemanticCore.Wff.all x ps)))

Checked nominal proof certificate identified upstream as g_albi.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAlrimih (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (hyp_alrimih_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.all x ph))) (hyp_alrimih_2 : Nominal.NPrf (ph.imp ps)) : Nominal.NPrf (ph.imp (SemanticCore.Wff.all x ps))

Checked nominal proof certificate identified upstream as g_alrimih.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAlbii (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (hyp_albii_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph ps)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.all x ph) (SemanticCore.Wff.all x ps))

Checked nominal proof certificate identified upstream as g_albii.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN2albii (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) (hyp_albii_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph ps)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.all x (SemanticCore.Wff.all y ph)) (SemanticCore.Wff.all x (SemanticCore.Wff.all y ps)))

Checked nominal proof certificate identified upstream as g_n_2albii.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHbxfrbi (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (hyp_hbxfrbi_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph ps)) (hyp_hbxfrbi_2 : Nominal.NPrf (ps.imp (SemanticCore.Wff.all x ps))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.all x ph))

Checked nominal proof certificate identified upstream as g_hbxfrbi.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfbii (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (hyp_nfbii_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph ps)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWnf x ph) (Compiler.CompactSourceSyntax.synWnf x ps))

Checked nominal proof certificate identified upstream as g_nfbii.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfxfr (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (hyp_nfbii_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph ps)) (hyp_nfxfr_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ps)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ph)

Checked nominal proof certificate identified upstream as g_nfxfr.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfxfrd (ph ps ch : SemanticCore.Wff) (x : SemanticCore.Var) (hyp_nfbii_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph ps)) (hyp_nfxfrd_2 : Nominal.NPrf (ch.imp (Compiler.CompactSourceSyntax.synWnf x ps))) : Nominal.NPrf (ch.imp (Compiler.CompactSourceSyntax.synWnf x ph))

Checked nominal proof certificate identified upstream as g_nfxfrd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAlex (ph : SemanticCore.Wff) (x : SemanticCore.Var) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.all x ph) (Compiler.CompactSourceSyntax.synWex x ph.neg).neg)

Checked nominal proof certificate identified upstream as g_alex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN2nalexn (ph : SemanticCore.Wff) (x y : SemanticCore.Var) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.all x (SemanticCore.Wff.all y ph)).neg (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWex y ph.neg)))

Checked nominal proof certificate identified upstream as g_n_2nalexn.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gExnal (ph : SemanticCore.Wff) (x : SemanticCore.Var) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWex x ph.neg) (SemanticCore.Wff.all x ph).neg)

Checked nominal proof certificate identified upstream as g_exnal.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gExim (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) : Nominal.NPrf ((SemanticCore.Wff.all x (ph.imp ps)).imp ((Compiler.CompactSourceSyntax.synWex x ph).imp (Compiler.CompactSourceSyntax.synWex x ps)))

Checked nominal proof certificate identified upstream as g_exim.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEximi (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (hyp_eximi_1 : Nominal.NPrf (ph.imp ps)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWex x ph).imp (Compiler.CompactSourceSyntax.synWex x ps))

Checked nominal proof certificate identified upstream as g_eximi.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN2eximi (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) (hyp_eximi_1 : Nominal.NPrf (ph.imp ps)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWex y ph)).imp (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWex y ps)))

Checked nominal proof certificate identified upstream as g_n_2eximi.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAlinexa (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.all x (ph.imp ps.neg)) (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWa ph ps)).neg)

Checked nominal proof certificate identified upstream as g_alinexa.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gExbi (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) : Nominal.NPrf ((SemanticCore.Wff.all x (Compiler.CompactSourceSyntax.synWb ph ps)).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWex x ph) (Compiler.CompactSourceSyntax.synWex x ps)))

Checked nominal proof certificate identified upstream as g_exbi.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gExbii (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (hyp_exbii_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph ps)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWex x ph) (Compiler.CompactSourceSyntax.synWex x ps))

Checked nominal proof certificate identified upstream as g_exbii.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN2exbii (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) (hyp_n_2exbii_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph ps)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWex y ph)) (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWex y ps)))

Checked nominal proof certificate identified upstream as g_n_2exbii.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN3exbii (ph ps : SemanticCore.Wff) (x y z : SemanticCore.Var) (hyp_n_3exbii_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph ps)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWex y (Compiler.CompactSourceSyntax.synWex z ph))) (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWex y (Compiler.CompactSourceSyntax.synWex z ps))))

Checked nominal proof certificate identified upstream as g_n_3exbii.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gExanali (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWa ph ps.neg)) (SemanticCore.Wff.all x (ph.imp ps)).neg)

Checked nominal proof certificate identified upstream as g_exanali.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gExancom (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWa ph ps)) (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWa ps ph)))

Checked nominal proof certificate identified upstream as g_exancom.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAlrimdh (ph ps ch : SemanticCore.Wff) (x : SemanticCore.Var) (hyp_alrimdh_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.all x ph))) (hyp_alrimdh_2 : Nominal.NPrf (ps.imp (SemanticCore.Wff.all x ps))) (hyp_alrimdh_3 : Nominal.NPrf (ph.imp (ps.imp ch))) : Nominal.NPrf (ph.imp (ps.imp (SemanticCore.Wff.all x ch)))

Checked nominal proof certificate identified upstream as g_alrimdh.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEximdh (ph ps ch : SemanticCore.Wff) (x : SemanticCore.Var) (hyp_eximdh_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.all x ph))) (hyp_eximdh_2 : Nominal.NPrf (ph.imp (ps.imp ch))) : Nominal.NPrf (ph.imp ((Compiler.CompactSourceSyntax.synWex x ps).imp (Compiler.CompactSourceSyntax.synWex x ch)))

Checked nominal proof certificate identified upstream as g_eximdh.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNexdh (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (hyp_nexdh_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.all x ph))) (hyp_nexdh_2 : Nominal.NPrf (ph.imp ps.neg)) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWex x ps).neg)

Checked nominal proof certificate identified upstream as g_nexdh.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAlbidh (ph ps ch : SemanticCore.Wff) (x : SemanticCore.Var) (hyp_albidh_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.all x ph))) (hyp_albidh_2 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.all x ps) (SemanticCore.Wff.all x ch)))

Checked nominal proof certificate identified upstream as g_albidh.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gExbidh (ph ps ch : SemanticCore.Wff) (x : SemanticCore.Var) (hyp_exbidh_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.all x ph))) (hyp_exbidh_2 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWex x ps) (Compiler.CompactSourceSyntax.synWex x ch)))

Checked nominal proof certificate identified upstream as g_exbidh.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gExsimpl (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWa ph ps)).imp (Compiler.CompactSourceSyntax.synWex x ph))

Checked nominal proof certificate identified upstream as g_exsimpl.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN1926 (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.all x (Compiler.CompactSourceSyntax.synWa ph ps)) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.all x ph) (SemanticCore.Wff.all x ps)))

Checked nominal proof certificate identified upstream as g_n_19_26.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN1929 (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.all x ph) (Compiler.CompactSourceSyntax.synWex x ps)).imp (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWa ph ps)))

Checked nominal proof certificate identified upstream as g_n_19_29.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN1929r (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWex x ph) (SemanticCore.Wff.all x ps)).imp (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWa ph ps)))

Checked nominal proof certificate identified upstream as g_n_19_29r.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN1935 (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWex x (ph.imp ps)) ((SemanticCore.Wff.all x ph).imp (Compiler.CompactSourceSyntax.synWex x ps)))

Checked nominal proof certificate identified upstream as g_n_19_35.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN1935i (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (hyp_n_19_35i_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWex x (ph.imp ps))) : Nominal.NPrf ((SemanticCore.Wff.all x ph).imp (Compiler.CompactSourceSyntax.synWex x ps))

Checked nominal proof certificate identified upstream as g_n_19_35i.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN1943 (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWo ph ps)) (Compiler.CompactSourceSyntax.synWo (Compiler.CompactSourceSyntax.synWex x ph) (Compiler.CompactSourceSyntax.synWex x ps)))

Checked nominal proof certificate identified upstream as g_n_19_43.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN1940 (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWa ph ps)).imp (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWex x ph) (Compiler.CompactSourceSyntax.synWex x ps)))

Checked nominal proof certificate identified upstream as g_n_19_40.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAlbiim (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.all x (Compiler.CompactSourceSyntax.synWb ph ps)) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.all x (ph.imp ps)) (SemanticCore.Wff.all x (ps.imp ph))))

Checked nominal proof certificate identified upstream as g_albiim.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN2albiim (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.all x (SemanticCore.Wff.all y (Compiler.CompactSourceSyntax.synWb ph ps))) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.all x (SemanticCore.Wff.all y (ph.imp ps))) (SemanticCore.Wff.all x (SemanticCore.Wff.all y (ps.imp ph)))))

Checked nominal proof certificate identified upstream as g_n_2albiim.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gExintrbi (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) : Nominal.NPrf ((SemanticCore.Wff.all x (ph.imp ps)).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWex x ph) (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWa ph ps))))

Checked nominal proof certificate identified upstream as g_exintrbi.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gExintr (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) : Nominal.NPrf ((SemanticCore.Wff.all x (ph.imp ps)).imp ((Compiler.CompactSourceSyntax.synWex x ph).imp (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWa ph ps))))

Checked nominal proof certificate identified upstream as g_exintr.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gA17d (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (dv_ps_x : x ∉ ps.fv) : Nominal.NPrf (ph.imp (ps.imp (SemanticCore.Wff.all x ps)))

Checked nominal proof certificate identified upstream as g_a17d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAx17e (ph : SemanticCore.Wff) (x : SemanticCore.Var) (dv_ph_x : x ∉ ph.fv) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWex x ph).imp ph)

Checked nominal proof certificate identified upstream as g_ax17e.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfv (ph : SemanticCore.Wff) (x : SemanticCore.Var) (dv_ph_x : x ∉ ph.fv) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ph)

Checked nominal proof certificate identified upstream as g_nfv.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gNfv ph x dv_ph_x = NFChoice.DirectNominalPrf.WPPReplay.gNfi ph x (NFChoice.DirectNominalPrf.Nominal.ax17 ph x ⋯)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfvd (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (dv_ps_x : x ∉ ps.fv) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWnf x ps))

Checked nominal proof certificate identified upstream as g_nfvd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAlimdv (ph ps ch : SemanticCore.Wff) (x : SemanticCore.Var) (dv_ph_x : x ∉ ph.fv) (hyp_alimdv_1 : Nominal.NPrf (ph.imp (ps.imp ch))) : Nominal.NPrf (ph.imp ((SemanticCore.Wff.all x ps).imp (SemanticCore.Wff.all x ch)))

Checked nominal proof certificate identified upstream as g_alimdv.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gAlimdv ph ps ch x dv_ph_x hyp_alimdv_1 = NFChoice.DirectNominalPrf.WPPReplay.gAlimdh ph ps ch x (NFChoice.DirectNominalPrf.Nominal.ax17 ph x ⋯) hyp_alimdv_1

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEximdv (ph ps ch : SemanticCore.Wff) (x : SemanticCore.Var) (dv_ph_x : x ∉ ph.fv) (hyp_alimdv_1 : Nominal.NPrf (ph.imp (ps.imp ch))) : Nominal.NPrf (ph.imp ((Compiler.CompactSourceSyntax.synWex x ps).imp (Compiler.CompactSourceSyntax.synWex x ch)))

Checked nominal proof certificate identified upstream as g_eximdv.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gEximdv ph ps ch x dv_ph_x hyp_alimdv_1 = NFChoice.DirectNominalPrf.WPPReplay.gEximdh ph ps ch x (NFChoice.DirectNominalPrf.Nominal.ax17 ph x ⋯) hyp_alimdv_1

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN2eximdv (ph ps ch : SemanticCore.Wff) (x y : SemanticCore.Var) (dv_ph_x : x ∉ ph.fv) (dv_ph_y : y ∉ ph.fv) (hyp_n_2alimdv_1 : Nominal.NPrf (ph.imp (ps.imp ch))) : Nominal.NPrf (ph.imp ((Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWex y ps)).imp (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWex y ch))))

Checked nominal proof certificate identified upstream as g_n_2eximdv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAlbidv (ph ps ch : SemanticCore.Wff) (x : SemanticCore.Var) (dv_ph_x : x ∉ ph.fv) (hyp_albidv_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.all x ps) (SemanticCore.Wff.all x ch)))

Checked nominal proof certificate identified upstream as g_albidv.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gAlbidv ph ps ch x dv_ph_x hyp_albidv_1 = NFChoice.DirectNominalPrf.WPPReplay.gAlbidh ph ps ch x (NFChoice.DirectNominalPrf.Nominal.ax17 ph x ⋯) hyp_albidv_1

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gExbidv (ph ps ch : SemanticCore.Wff) (x : SemanticCore.Var) (dv_ph_x : x ∉ ph.fv) (hyp_albidv_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWex x ps) (Compiler.CompactSourceSyntax.synWex x ch)))

Checked nominal proof certificate identified upstream as g_exbidv.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gExbidv ph ps ch x dv_ph_x hyp_albidv_1 = NFChoice.DirectNominalPrf.WPPReplay.gExbidh ph ps ch x (NFChoice.DirectNominalPrf.Nominal.ax17 ph x ⋯) hyp_albidv_1

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN2albidv (ph ps ch : SemanticCore.Wff) (x y : SemanticCore.Var) (dv_ph_x : x ∉ ph.fv) (dv_ph_y : y ∉ ph.fv) (hyp_n_2albidv_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.all x (SemanticCore.Wff.all y ps)) (SemanticCore.Wff.all x (SemanticCore.Wff.all y ch))))

Checked nominal proof certificate identified upstream as g_n_2albidv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN2exbidv (ph ps ch : SemanticCore.Wff) (x y : SemanticCore.Var) (dv_ph_x : x ∉ ph.fv) (dv_ph_y : y ∉ ph.fv) (hyp_n_2albidv_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWex y ps)) (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWex y ch))))

Checked nominal proof certificate identified upstream as g_n_2exbidv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN3exbidv (ph ps ch : SemanticCore.Wff) (x y z : SemanticCore.Var) (dv_ph_x : x ∉ ph.fv) (dv_ph_y : y ∉ ph.fv) (dv_ph_z : z ∉ ph.fv) (hyp_n_3exbidv_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWex y (Compiler.CompactSourceSyntax.synWex z ps))) (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWex y (Compiler.CompactSourceSyntax.synWex z ch)))))

Checked nominal proof certificate identified upstream as g_n_3exbidv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAlrimiv (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (dv_ph_x : x ∉ ph.fv) (hyp_alrimiv_1 : Nominal.NPrf (ph.imp ps)) : Nominal.NPrf (ph.imp (SemanticCore.Wff.all x ps))

Checked nominal proof certificate identified upstream as g_alrimiv.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gAlrimiv ph ps x dv_ph_x hyp_alrimiv_1 = NFChoice.DirectNominalPrf.WPPReplay.gAlrimih ph ps x (NFChoice.DirectNominalPrf.Nominal.ax17 ph x ⋯) hyp_alrimiv_1

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAlrimivv (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) (dv_ph_x : x ∉ ph.fv) (dv_ph_y : y ∉ ph.fv) (hyp_alrimivv_1 : Nominal.NPrf (ph.imp ps)) : Nominal.NPrf (ph.imp (SemanticCore.Wff.all x (SemanticCore.Wff.all y ps)))

Checked nominal proof certificate identified upstream as g_alrimivv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAlrimdv (ph ps ch : SemanticCore.Wff) (x : SemanticCore.Var) (dv_ph_x : x ∉ ph.fv) (dv_ps_x : x ∉ ps.fv) (hyp_alrimdv_1 : Nominal.NPrf (ph.imp (ps.imp ch))) : Nominal.NPrf (ph.imp (ps.imp (SemanticCore.Wff.all x ch)))

Checked nominal proof certificate identified upstream as g_alrimdv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gExlimiv (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (dv_ps_x : x ∉ ps.fv) (hyp_exlimiv_1 : Nominal.NPrf (ph.imp ps)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWex x ph).imp ps)

Checked nominal proof certificate identified upstream as g_exlimiv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gExlimivv (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) (dv_ps_x : x ∉ ps.fv) (dv_ps_y : y ∉ ps.fv) (hyp_exlimivv_1 : Nominal.NPrf (ph.imp ps)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWex y ph)).imp ps)

Checked nominal proof certificate identified upstream as g_exlimivv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gExlimdv (ph ps ch : SemanticCore.Wff) (x : SemanticCore.Var) (dv_ch_x : x ∉ ch.fv) (dv_ph_x : x ∉ ph.fv) (hyp_exlimdv_1 : Nominal.NPrf (ph.imp (ps.imp ch))) : Nominal.NPrf (ph.imp ((Compiler.CompactSourceSyntax.synWex x ps).imp ch))

Checked nominal proof certificate identified upstream as g_exlimdv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gExlimdvv (ph ps ch : SemanticCore.Wff) (x y : SemanticCore.Var) (dv_ch_x : x ∉ ch.fv) (dv_ch_y : y ∉ ch.fv) (dv_ph_x : x ∉ ph.fv) (dv_ph_y : y ∉ ph.fv) (hyp_exlimdvv_1 : Nominal.NPrf (ph.imp (ps.imp ch))) : Nominal.NPrf (ph.imp ((Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWex y ps)).imp ch))

Checked nominal proof certificate identified upstream as g_exlimdvv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gExlimddv (ph ps ch : SemanticCore.Wff) (x : SemanticCore.Var) (dv_ch_x : x ∉ ch.fv) (dv_ph_x : x ∉ ph.fv) (hyp_exlimddv_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWex x ps))) (hyp_exlimddv_2 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph ps).imp ch)) : Nominal.NPrf (ph.imp ch)

Checked nominal proof certificate identified upstream as g_exlimddv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEqus3 (ph : SemanticCore.Wff) (x y : SemanticCore.Var) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.objEq x y) ph)) (SemanticCore.Wff.all x ((SemanticCore.Wff.objEq x y).imp ph.neg)).neg)

Checked nominal proof certificate identified upstream as g_equs3.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSpeimfw (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) (hyp_speimfw_2 : Nominal.NPrf ((SemanticCore.Wff.objEq x y).imp (ph.imp ps))) : Nominal.NPrf ((SemanticCore.Wff.all x (SemanticCore.Wff.objEq x y).neg).neg.imp ((SemanticCore.Wff.all x ph).imp (Compiler.CompactSourceSyntax.synWex x ps)))

Checked nominal proof certificate identified upstream as g_speimfw.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSpimfw (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) (hyp_spimfw_1 : Nominal.NPrf (ps.neg.imp (SemanticCore.Wff.all x ps.neg))) (hyp_spimfw_2 : Nominal.NPrf ((SemanticCore.Wff.objEq x y).imp (ph.imp ps))) : Nominal.NPrf ((SemanticCore.Wff.all x (SemanticCore.Wff.objEq x y).neg).neg.imp ((SemanticCore.Wff.all x ph).imp ps))

Checked nominal proof certificate identified upstream as g_spimfw.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSbequ2 (ph : SemanticCore.Wff) (x y : SemanticCore.Var) : Nominal.NPrf ((SemanticCore.Wff.objEq x y).imp ((Compiler.CompactSourceSyntax.synWsb y x ph).imp ph))

Checked nominal proof certificate identified upstream as g_sbequ2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSb1 (ph : SemanticCore.Wff) (x y : SemanticCore.Var) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWsb y x ph).imp (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.objEq x y) ph)))

Checked nominal proof certificate identified upstream as g_sb1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSbimi (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) (hyp_sbimi_1 : Nominal.NPrf (ph.imp ps)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWsb y x ph).imp (Compiler.CompactSourceSyntax.synWsb y x ps))

Checked nominal proof certificate identified upstream as g_sbimi.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSbbii (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) (hyp_sbbii_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph ps)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWsb y x ph) (Compiler.CompactSourceSyntax.synWsb y x ps))

Checked nominal proof certificate identified upstream as g_sbbii.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAx9v (x y : SemanticCore.Var) (_dv_x_y : x ≠ y) : Nominal.NPrf (SemanticCore.Wff.all x (SemanticCore.Wff.objEq x y).neg).neg

Checked nominal proof certificate identified upstream as g_ax9v.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gAx9v x y _dv_x_y = NFChoice.DirectNominalPrf.Nominal.ax9 x y

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gA9ev (x y : SemanticCore.Var) (dv_x_y : x ≠ y) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWex x (SemanticCore.Wff.objEq x y))

Checked nominal proof certificate identified upstream as g_a9ev.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSpimeh (ph ps : SemanticCore.Wff) (x z : SemanticCore.Var) (dv_x_z : x ≠ z) (hyp_spimeh_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.all x ph))) (hyp_spimeh_2 : Nominal.NPrf ((SemanticCore.Wff.objEq x z).imp (ph.imp ps))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWex x ps))

Checked nominal proof certificate identified upstream as g_spimeh.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSpimw (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) (dv_x_y : x ≠ y) (hyp_spimw_1 : Nominal.NPrf (ps.neg.imp (SemanticCore.Wff.all x ps.neg))) (hyp_spimw_2 : Nominal.NPrf ((SemanticCore.Wff.objEq x y).imp (ph.imp ps))) : Nominal.NPrf ((SemanticCore.Wff.all x ph).imp ps)

Checked nominal proof certificate identified upstream as g_spimw.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSpimvw (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) (dv_ps_x : x ∉ ps.fv) (dv_x_y : x ≠ y) (hyp_spimvw_1 : Nominal.NPrf ((SemanticCore.Wff.objEq x y).imp (ph.imp ps))) : Nominal.NPrf ((SemanticCore.Wff.all x ph).imp ps)

Checked nominal proof certificate identified upstream as g_spimvw.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCbvalivw (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) (dv_ph_y : y ∉ ph.fv) (dv_ps_x : x ∉ ps.fv) (dv_x_y : x ≠ y) (hyp_cbvalivw_1 : Nominal.NPrf ((SemanticCore.Wff.objEq x y).imp (ph.imp ps))) : Nominal.NPrf ((SemanticCore.Wff.all x ph).imp (SemanticCore.Wff.all y ps))

Checked nominal proof certificate identified upstream as g_cbvalivw.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEquid (x : SemanticCore.Var) : Nominal.NPrf (SemanticCore.Wff.objEq x x)

Checked nominal proof certificate identified upstream as g_equid.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEqucomi (x y : SemanticCore.Var) : Nominal.NPrf ((SemanticCore.Wff.objEq x y).imp (SemanticCore.Wff.objEq y x))

Checked nominal proof certificate identified upstream as g_equcomi.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEqucom (x y : SemanticCore.Var) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.objEq x y) (SemanticCore.Wff.objEq y x))

Checked nominal proof certificate identified upstream as g_equcom.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEqucoms (ph : SemanticCore.Wff) (x y : SemanticCore.Var) (hyp_equcoms_1 : Nominal.NPrf ((SemanticCore.Wff.objEq x y).imp ph)) : Nominal.NPrf ((SemanticCore.Wff.objEq y x).imp ph)

Checked nominal proof certificate identified upstream as g_equcoms.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEqutr (x y z : SemanticCore.Var) : Nominal.NPrf ((SemanticCore.Wff.objEq x y).imp ((SemanticCore.Wff.objEq y z).imp (SemanticCore.Wff.objEq x z)))

Checked nominal proof certificate identified upstream as g_equtr.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEqutrr (x y z : SemanticCore.Var) : Nominal.NPrf ((SemanticCore.Wff.objEq x y).imp ((SemanticCore.Wff.objEq z x).imp (SemanticCore.Wff.objEq z y)))

Checked nominal proof certificate identified upstream as g_equtrr.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEquequ1 (x y z : SemanticCore.Var) : Nominal.NPrf ((SemanticCore.Wff.objEq x y).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.objEq x z) (SemanticCore.Wff.objEq y z)))

Checked nominal proof certificate identified upstream as g_equequ1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEquequ2 (x y z : SemanticCore.Var) : Nominal.NPrf ((SemanticCore.Wff.objEq x y).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.objEq z x) (SemanticCore.Wff.objEq z y)))

Checked nominal proof certificate identified upstream as g_equequ2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gStdpc6 (x : SemanticCore.Var) : Nominal.NPrf (SemanticCore.Wff.all x (SemanticCore.Wff.objEq x x))

Checked nominal proof certificate identified upstream as g_stdpc6.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gStdpc6 x = NFChoice.DirectNominalPrf.Nominal.gen (NFChoice.DirectNominalPrf.WPPReplay.gEquid x) x

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEqutr2 (x y z : SemanticCore.Var) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.objEq x z) (SemanticCore.Wff.objEq y z)).imp (SemanticCore.Wff.objEq x y))

Checked nominal proof certificate identified upstream as g_equtr2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElequ1 (x y z : SemanticCore.Var) : Nominal.NPrf ((SemanticCore.Wff.objEq x y).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.objMem x z) (SemanticCore.Wff.objMem y z)))

Checked nominal proof certificate identified upstream as g_elequ1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElequ2 (x y z : SemanticCore.Var) : Nominal.NPrf ((SemanticCore.Wff.objEq x y).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.objMem z x) (SemanticCore.Wff.objMem z y)))

Checked nominal proof certificate identified upstream as g_elequ2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHbn1 (ph : SemanticCore.Wff) (x : SemanticCore.Var) : Nominal.NPrf ((SemanticCore.Wff.all x ph).neg.imp (SemanticCore.Wff.all x (SemanticCore.Wff.all x ph).neg))

Checked nominal proof certificate identified upstream as g_hbn1.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gHbn1 ph x = NFChoice.DirectNominalPrf.Nominal.ax6 x ph

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHbe1 (ph : SemanticCore.Wff) (x : SemanticCore.Var) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWex x ph).imp (SemanticCore.Wff.all x (Compiler.CompactSourceSyntax.synWex x ph)))

Checked nominal proof certificate identified upstream as g_hbe1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfe1 (ph : SemanticCore.Wff) (x : SemanticCore.Var) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x (Compiler.CompactSourceSyntax.synWex x ph))

Checked nominal proof certificate identified upstream as g_nfe1.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gNfe1 ph x = NFChoice.DirectNominalPrf.WPPReplay.gNfi (NFChoice.Compiler.CompactSourceSyntax.synWex x ph) x (NFChoice.DirectNominalPrf.WPPReplay.gHbe1 ph x)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gA7s (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) (hyp_a7s_1 : Nominal.NPrf ((SemanticCore.Wff.all x (SemanticCore.Wff.all y ph)).imp ps)) : Nominal.NPrf ((SemanticCore.Wff.all y (SemanticCore.Wff.all x ph)).imp ps)

Checked nominal proof certificate identified upstream as g_a7s.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHbal (ph : SemanticCore.Wff) (x y : SemanticCore.Var) (hyp_hbal_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.all x ph))) : Nominal.NPrf ((SemanticCore.Wff.all y ph).imp (SemanticCore.Wff.all x (SemanticCore.Wff.all y ph)))

Checked nominal proof certificate identified upstream as g_hbal.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAlcom (ph : SemanticCore.Wff) (x y : SemanticCore.Var) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.all x (SemanticCore.Wff.all y ph)) (SemanticCore.Wff.all y (SemanticCore.Wff.all x ph)))

Checked nominal proof certificate identified upstream as g_alcom.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAlrot3 (ph : SemanticCore.Wff) (x y z : SemanticCore.Var) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.all x (SemanticCore.Wff.all y (SemanticCore.Wff.all z ph))) (SemanticCore.Wff.all y (SemanticCore.Wff.all z (SemanticCore.Wff.all x ph))))

Checked nominal proof certificate identified upstream as g_alrot3.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHbald (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) (hyp_hbald_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.all y ph))) (hyp_hbald_2 : Nominal.NPrf (ph.imp (ps.imp (SemanticCore.Wff.all x ps)))) : Nominal.NPrf (ph.imp ((SemanticCore.Wff.all y ps).imp (SemanticCore.Wff.all x (SemanticCore.Wff.all y ps))))

Checked nominal proof certificate identified upstream as g_hbald.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gExcom (ph : SemanticCore.Wff) (x y : SemanticCore.Var) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWex y ph)) (Compiler.CompactSourceSyntax.synWex y (Compiler.CompactSourceSyntax.synWex x ph)))

Checked nominal proof certificate identified upstream as g_excom.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gExcom13 (ph : SemanticCore.Wff) (x y z : SemanticCore.Var) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWex y (Compiler.CompactSourceSyntax.synWex z ph))) (Compiler.CompactSourceSyntax.synWex z (Compiler.CompactSourceSyntax.synWex y (Compiler.CompactSourceSyntax.synWex x ph))))

Checked nominal proof certificate identified upstream as g_excom13.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gExrot3 (ph : SemanticCore.Wff) (x y z : SemanticCore.Var) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWex y (Compiler.CompactSourceSyntax.synWex z ph))) (Compiler.CompactSourceSyntax.synWex y (Compiler.CompactSourceSyntax.synWex z (Compiler.CompactSourceSyntax.synWex x ph))))

Checked nominal proof certificate identified upstream as g_exrot3.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gExrot4 (ph : SemanticCore.Wff) (x y z w : SemanticCore.Var) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWex y (Compiler.CompactSourceSyntax.synWex z (Compiler.CompactSourceSyntax.synWex w ph)))) (Compiler.CompactSourceSyntax.synWex z (Compiler.CompactSourceSyntax.synWex w (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWex y ph)))))

Checked nominal proof certificate identified upstream as g_exrot4.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSp (ph : SemanticCore.Wff) (x : SemanticCore.Var) : Nominal.NPrf ((SemanticCore.Wff.all x ph).imp ph)

Checked nominal proof certificate identified upstream as g_sp.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAx6o (ph : SemanticCore.Wff) (x : SemanticCore.Var) : Nominal.NPrf ((SemanticCore.Wff.all x (SemanticCore.Wff.all x ph).neg).neg.imp ph)

Checked nominal proof certificate identified upstream as g_ax6o.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSps (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (hyp_sps_1 : Nominal.NPrf (ph.imp ps)) : Nominal.NPrf ((SemanticCore.Wff.all x ph).imp ps)

Checked nominal proof certificate identified upstream as g_sps.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSpsd (ph ps ch : SemanticCore.Wff) (x : SemanticCore.Var) (hyp_spsd_1 : Nominal.NPrf (ph.imp (ps.imp ch))) : Nominal.NPrf (ph.imp ((SemanticCore.Wff.all x ps).imp ch))

Checked nominal proof certificate identified upstream as g_spsd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN198a (ph : SemanticCore.Wff) (x : SemanticCore.Var) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWex x ph))

Checked nominal proof certificate identified upstream as g_n_19_8a.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN1921bi (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (hyp_n_19_21bi_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.all x ps))) : Nominal.NPrf (ph.imp ps)

Checked nominal proof certificate identified upstream as g_n_19_21bi.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfr (ph : SemanticCore.Wff) (x : SemanticCore.Var) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWnf x ph).imp (ph.imp (SemanticCore.Wff.all x ph)))

Checked nominal proof certificate identified upstream as g_nfr.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfri (ph : SemanticCore.Wff) (x : SemanticCore.Var) (hyp_nfri_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ph)) : Nominal.NPrf (ph.imp (SemanticCore.Wff.all x ph))

Checked nominal proof certificate identified upstream as g_nfri.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gNfri ph x hyp_nfri_1 = NFChoice.DirectNominalPrf.Nominal.mp hyp_nfri_1 (NFChoice.DirectNominalPrf.WPPReplay.gNfr ph x)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfrd (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (hyp_nfrd_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWnf x ps))) : Nominal.NPrf (ph.imp (ps.imp (SemanticCore.Wff.all x ps)))

Checked nominal proof certificate identified upstream as g_nfrd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAlimd (ph ps ch : SemanticCore.Wff) (x : SemanticCore.Var) (hyp_alimd_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ph)) (hyp_alimd_2 : Nominal.NPrf (ph.imp (ps.imp ch))) : Nominal.NPrf (ph.imp ((SemanticCore.Wff.all x ps).imp (SemanticCore.Wff.all x ch)))

Checked nominal proof certificate identified upstream as g_alimd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAlrimi (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (hyp_alrimi_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ph)) (hyp_alrimi_2 : Nominal.NPrf (ph.imp ps)) : Nominal.NPrf (ph.imp (SemanticCore.Wff.all x ps))

Checked nominal proof certificate identified upstream as g_alrimi.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfd (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (hyp_nfd_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ph)) (hyp_nfd_2 : Nominal.NPrf (ph.imp (ps.imp (SemanticCore.Wff.all x ps)))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWnf x ps))

Checked nominal proof certificate identified upstream as g_nfd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfdh (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (hyp_nfdh_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.all x ph))) (hyp_nfdh_2 : Nominal.NPrf (ph.imp (ps.imp (SemanticCore.Wff.all x ps)))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWnf x ps))

Checked nominal proof certificate identified upstream as g_nfdh.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gNfdh ph ps x hyp_nfdh_1 hyp_nfdh_2 = NFChoice.DirectNominalPrf.WPPReplay.gNfd ph ps x (NFChoice.DirectNominalPrf.WPPReplay.gNfi ph x hyp_nfdh_1) hyp_nfdh_2

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAlrimdd (ph ps ch : SemanticCore.Wff) (x : SemanticCore.Var) (hyp_alrimdd_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ph)) (hyp_alrimdd_2 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWnf x ps))) (hyp_alrimdd_3 : Nominal.NPrf (ph.imp (ps.imp ch))) : Nominal.NPrf (ph.imp (ps.imp (SemanticCore.Wff.all x ch)))

Checked nominal proof certificate identified upstream as g_alrimdd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAlrimd (ph ps ch : SemanticCore.Wff) (x : SemanticCore.Var) (hyp_alrimd_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ph)) (hyp_alrimd_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ps)) (hyp_alrimd_3 : Nominal.NPrf (ph.imp (ps.imp ch))) : Nominal.NPrf (ph.imp (ps.imp (SemanticCore.Wff.all x ch)))

Checked nominal proof certificate identified upstream as g_alrimd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEximd (ph ps ch : SemanticCore.Wff) (x : SemanticCore.Var) (hyp_eximd_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ph)) (hyp_eximd_2 : Nominal.NPrf (ph.imp (ps.imp ch))) : Nominal.NPrf (ph.imp ((Compiler.CompactSourceSyntax.synWex x ps).imp (Compiler.CompactSourceSyntax.synWex x ch)))

Checked nominal proof certificate identified upstream as g_eximd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNexd (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (hyp_nexd_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ph)) (hyp_nexd_2 : Nominal.NPrf (ph.imp ps.neg)) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWex x ps).neg)

Checked nominal proof certificate identified upstream as g_nexd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAlbid (ph ps ch : SemanticCore.Wff) (x : SemanticCore.Var) (hyp_albid_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ph)) (hyp_albid_2 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.all x ps) (SemanticCore.Wff.all x ch)))

Checked nominal proof certificate identified upstream as g_albid.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gExbid (ph ps ch : SemanticCore.Wff) (x : SemanticCore.Var) (hyp_exbid_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ph)) (hyp_exbid_2 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWex x ps) (Compiler.CompactSourceSyntax.synWex x ch)))

Checked nominal proof certificate identified upstream as g_exbid.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfbidf (ph ps ch : SemanticCore.Wff) (x : SemanticCore.Var) (hyp_nfbidf_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ph)) (hyp_nfbidf_2 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWnf x ps) (Compiler.CompactSourceSyntax.synWnf x ch)))

Checked nominal proof certificate identified upstream as g_nfbidf.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHbnt (ph : SemanticCore.Wff) (x : SemanticCore.Var) : Nominal.NPrf ((SemanticCore.Wff.all x (ph.imp (SemanticCore.Wff.all x ph))).imp (ph.neg.imp (SemanticCore.Wff.all x ph.neg)))

Checked nominal proof certificate identified upstream as g_hbnt.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHbn (ph : SemanticCore.Wff) (x : SemanticCore.Var) (hyp_hbn_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.all x ph))) : Nominal.NPrf (ph.neg.imp (SemanticCore.Wff.all x ph.neg))

Checked nominal proof certificate identified upstream as g_hbn.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN199ht (ph : SemanticCore.Wff) (x : SemanticCore.Var) : Nominal.NPrf ((SemanticCore.Wff.all x (ph.imp (SemanticCore.Wff.all x ph))).imp ((Compiler.CompactSourceSyntax.synWex x ph).imp ph))

Checked nominal proof certificate identified upstream as g_n_19_9ht.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN199t (ph : SemanticCore.Wff) (x : SemanticCore.Var) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWnf x ph).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWex x ph) ph))

Checked nominal proof certificate identified upstream as g_n_19_9t.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN199h (ph : SemanticCore.Wff) (x : SemanticCore.Var) (hyp_n_19_9h_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.all x ph))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWex x ph) ph)

Checked nominal proof certificate identified upstream as g_n_19_9h.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN199d (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (hyp_n_19_9d_1 : Nominal.NPrf (ps.imp (Compiler.CompactSourceSyntax.synWnf x ph))) : Nominal.NPrf (ps.imp ((Compiler.CompactSourceSyntax.synWex x ph).imp ph))

Checked nominal proof certificate identified upstream as g_n_19_9d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN199 (ph : SemanticCore.Wff) (x : SemanticCore.Var) (hyp_n_19_9_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ph)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWex x ph) ph)

Checked nominal proof certificate identified upstream as g_n_19_9.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gN199 ph x hyp_n_19_9_1 = NFChoice.DirectNominalPrf.WPPReplay.gN199h ph x (NFChoice.DirectNominalPrf.WPPReplay.gNfri ph x hyp_n_19_9_1)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN193 (ph : SemanticCore.Wff) (x : SemanticCore.Var) (hyp_n_19_3_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ph)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.all x ph) ph)

Checked nominal proof certificate identified upstream as g_n_19_3.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHba1 (ph : SemanticCore.Wff) (x : SemanticCore.Var) : Nominal.NPrf ((SemanticCore.Wff.all x ph).imp (SemanticCore.Wff.all x (SemanticCore.Wff.all x ph)))

Checked nominal proof certificate identified upstream as g_hba1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfa1 (ph : SemanticCore.Wff) (x : SemanticCore.Var) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x (SemanticCore.Wff.all x ph))

Checked nominal proof certificate identified upstream as g_nfa1.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gNfa1 ph x = NFChoice.DirectNominalPrf.WPPReplay.gNfi (NFChoice.SemanticCore.Wff.all x ph) x (NFChoice.DirectNominalPrf.WPPReplay.gHba1 ph x)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gA5i (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (hyp_a5i_1 : Nominal.NPrf ((SemanticCore.Wff.all x ph).imp ps)) : Nominal.NPrf ((SemanticCore.Wff.all x ph).imp (SemanticCore.Wff.all x ps))

Checked nominal proof certificate identified upstream as g_a5i.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfnf1 (ph : SemanticCore.Wff) (x : SemanticCore.Var) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x (Compiler.CompactSourceSyntax.synWnf x ph))

Checked nominal proof certificate identified upstream as g_nfnf1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfnd (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (hyp_nfnd_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWnf x ps))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWnf x ps.neg))

Checked nominal proof certificate identified upstream as g_nfnd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfn (ph : SemanticCore.Wff) (x : SemanticCore.Var) (hyp_nfn_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ph)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ph.neg)

Checked nominal proof certificate identified upstream as g_nfn.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN1938 (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) : Nominal.NPrf (((Compiler.CompactSourceSyntax.synWex x ph).imp (SemanticCore.Wff.all x ps)).imp (SemanticCore.Wff.all x (ph.imp ps)))

Checked nominal proof certificate identified upstream as g_n_19_38.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN1921t (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWnf x ph).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.all x (ph.imp ps)) (ph.imp (SemanticCore.Wff.all x ps))))

Checked nominal proof certificate identified upstream as g_n_19_21t.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN1921 (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (hyp_n_19_21_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ph)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.all x (ph.imp ps)) (ph.imp (SemanticCore.Wff.all x ps)))

Checked nominal proof certificate identified upstream as g_n_19_21.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gN1921 ph ps x hyp_n_19_21_1 = NFChoice.DirectNominalPrf.Nominal.mp hyp_n_19_21_1 (NFChoice.DirectNominalPrf.WPPReplay.gN1921t ph ps x)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN1921h (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (hyp_n_19_21h_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.all x ph))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.all x (ph.imp ps)) (ph.imp (SemanticCore.Wff.all x ps)))

Checked nominal proof certificate identified upstream as g_n_19_21h.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gN1921h ph ps x hyp_n_19_21h_1 = NFChoice.DirectNominalPrf.WPPReplay.gN1921 ph ps x (NFChoice.DirectNominalPrf.WPPReplay.gNfi ph x hyp_n_19_21h_1)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN1923t (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWnf x ps).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.all x (ph.imp ps)) ((Compiler.CompactSourceSyntax.synWex x ph).imp ps)))

Checked nominal proof certificate identified upstream as g_n_19_23t.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN1923 (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (hyp_n_19_23_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ps)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.all x (ph.imp ps)) ((Compiler.CompactSourceSyntax.synWex x ph).imp ps))

Checked nominal proof certificate identified upstream as g_n_19_23.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gN1923 ph ps x hyp_n_19_23_1 = NFChoice.DirectNominalPrf.Nominal.mp hyp_n_19_23_1 (NFChoice.DirectNominalPrf.WPPReplay.gN1923t ph ps x)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN1923h (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (hyp_n_19_23h_1 : Nominal.NPrf (ps.imp (SemanticCore.Wff.all x ps))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.all x (ph.imp ps)) ((Compiler.CompactSourceSyntax.synWex x ph).imp ps))

Checked nominal proof certificate identified upstream as g_n_19_23h.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gN1923h ph ps x hyp_n_19_23h_1 = NFChoice.DirectNominalPrf.WPPReplay.gN1923 ph ps x (NFChoice.DirectNominalPrf.WPPReplay.gNfi ps x hyp_n_19_23h_1)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gExlimi (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (hyp_exlimi_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ps)) (hyp_exlimi_2 : Nominal.NPrf (ph.imp ps)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWex x ph).imp ps)

Checked nominal proof certificate identified upstream as g_exlimi.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gExlimih (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (hyp_exlimih_1 : Nominal.NPrf (ps.imp (SemanticCore.Wff.all x ps))) (hyp_exlimih_2 : Nominal.NPrf (ph.imp ps)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWex x ph).imp ps)

Checked nominal proof certificate identified upstream as g_exlimih.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gExlimd (ph ps ch : SemanticCore.Wff) (x : SemanticCore.Var) (hyp_exlimd_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ph)) (hyp_exlimd_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ch)) (hyp_exlimd_3 : Nominal.NPrf (ph.imp (ps.imp ch))) : Nominal.NPrf (ph.imp ((Compiler.CompactSourceSyntax.synWex x ps).imp ch))

Checked nominal proof certificate identified upstream as g_exlimd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfimd (ph ps ch : SemanticCore.Wff) (x : SemanticCore.Var) (hyp_nfimd_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWnf x ps))) (hyp_nfimd_2 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWnf x ch))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWnf x (ps.imp ch)))

Checked nominal proof certificate identified upstream as g_nfimd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHbim1 (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (hyp_hbim1_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.all x ph))) (hyp_hbim1_2 : Nominal.NPrf (ph.imp (ps.imp (SemanticCore.Wff.all x ps)))) : Nominal.NPrf ((ph.imp ps).imp (SemanticCore.Wff.all x (ph.imp ps)))

Checked nominal proof certificate identified upstream as g_hbim1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfim1 (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (hyp_nfim1_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ph)) (hyp_nfim1_2 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWnf x ps))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x (ph.imp ps))

Checked nominal proof certificate identified upstream as g_nfim1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfim (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (hyp_nfim_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ph)) (hyp_nfim_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ps)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x (ph.imp ps))

Checked nominal proof certificate identified upstream as g_nfim.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHbimd (ph ps ch : SemanticCore.Wff) (x : SemanticCore.Var) (hyp_hbimd_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.all x ph))) (hyp_hbimd_2 : Nominal.NPrf (ph.imp (ps.imp (SemanticCore.Wff.all x ps)))) (hyp_hbimd_3 : Nominal.NPrf (ph.imp (ch.imp (SemanticCore.Wff.all x ch)))) : Nominal.NPrf (ph.imp ((ps.imp ch).imp (SemanticCore.Wff.all x (ps.imp ch))))

Checked nominal proof certificate identified upstream as g_hbimd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHbim (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (hyp_hbim_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.all x ph))) (hyp_hbim_2 : Nominal.NPrf (ps.imp (SemanticCore.Wff.all x ps))) : Nominal.NPrf ((ph.imp ps).imp (SemanticCore.Wff.all x (ph.imp ps)))

Checked nominal proof certificate identified upstream as g_hbim.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfand (ph ps ch : SemanticCore.Wff) (x : SemanticCore.Var) (hyp_nfand_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWnf x ps))) (hyp_nfand_2 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWnf x ch))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWnf x (Compiler.CompactSourceSyntax.synWa ps ch)))

Checked nominal proof certificate identified upstream as g_nfand.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfan (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (hyp_nfan_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ph)) (hyp_nfan_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ps)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x (Compiler.CompactSourceSyntax.synWa ph ps))

Checked nominal proof certificate identified upstream as g_nfan.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfnan (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (hyp_nfan_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ph)) (hyp_nfan_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ps)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x (Compiler.CompactSourceSyntax.synWnan ph ps))

Checked nominal proof certificate identified upstream as g_nfnan.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHban (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (hyp_hb_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.all x ph))) (hyp_hb_2 : Nominal.NPrf (ps.imp (SemanticCore.Wff.all x ps))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph ps).imp (SemanticCore.Wff.all x (Compiler.CompactSourceSyntax.synWa ph ps)))

Checked nominal proof certificate identified upstream as g_hban.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfbid (ph ps ch : SemanticCore.Wff) (x : SemanticCore.Var) (hyp_nfbid_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWnf x ps))) (hyp_nfbid_2 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWnf x ch))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWnf x (Compiler.CompactSourceSyntax.synWb ps ch)))

Checked nominal proof certificate identified upstream as g_nfbid.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfbi (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (hyp_nf_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ph)) (hyp_nf_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ps)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x (Compiler.CompactSourceSyntax.synWb ph ps))

Checked nominal proof certificate identified upstream as g_nfbi.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEqusalhw (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) (dv_x_y : x ≠ y) (hyp_equsalhw_1 : Nominal.NPrf (ps.imp (SemanticCore.Wff.all x ps))) (hyp_equsalhw_2 : Nominal.NPrf ((SemanticCore.Wff.objEq x y).imp (Compiler.CompactSourceSyntax.synWb ph ps))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.all x ((SemanticCore.Wff.objEq x y).imp ph)) ps)

Checked nominal proof certificate identified upstream as g_equsalhw.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHbex (ph : SemanticCore.Wff) (x y : SemanticCore.Var) (hyp_hbex_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.all x ph))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWex y ph).imp (SemanticCore.Wff.all x (Compiler.CompactSourceSyntax.synWex y ph)))

Checked nominal proof certificate identified upstream as g_hbex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfal (ph : SemanticCore.Wff) (x y : SemanticCore.Var) (hyp_nfal_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ph)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x (SemanticCore.Wff.all y ph))

Checked nominal proof certificate identified upstream as g_nfal.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfex (ph : SemanticCore.Wff) (x y : SemanticCore.Var) (hyp_nfal_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ph)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x (Compiler.CompactSourceSyntax.synWex y ph))

Checked nominal proof certificate identified upstream as g_nfex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN1912 (ph : SemanticCore.Wff) (x y : SemanticCore.Var) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWex x (SemanticCore.Wff.all y ph)).imp (SemanticCore.Wff.all y (Compiler.CompactSourceSyntax.synWex x ph)))

Checked nominal proof certificate identified upstream as g_n_19_12.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDvelimhw (ph ps : SemanticCore.Wff) (x y z : SemanticCore.Var) (_dv_x_z : x ≠ z) (dv_y_z : y ≠ z) (hyp_dvelimhw_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.all x ph))) (hyp_dvelimhw_2 : Nominal.NPrf (ps.imp (SemanticCore.Wff.all z ps))) (hyp_dvelimhw_3 : Nominal.NPrf ((SemanticCore.Wff.objEq z y).imp (Compiler.CompactSourceSyntax.synWb ph ps))) (hyp_dvelimhw_4 : Nominal.NPrf ((SemanticCore.Wff.all x (SemanticCore.Wff.objEq x y)).neg.imp ((SemanticCore.Wff.objEq y z).imp (SemanticCore.Wff.all x (SemanticCore.Wff.objEq y z))))) : Nominal.NPrf ((SemanticCore.Wff.all x (SemanticCore.Wff.objEq x y)).neg.imp (ps.imp (SemanticCore.Wff.all x ps)))

Checked nominal proof certificate identified upstream as g_dvelimhw.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfald (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) (hyp_nfald_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf y ph)) (hyp_nfald_2 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWnf x ps))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWnf x (SemanticCore.Wff.all y ps)))

Checked nominal proof certificate identified upstream as g_nfald.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfexd (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) (hyp_nfald_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf y ph)) (hyp_nfald_2 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWnf x ps))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWnf x (Compiler.CompactSourceSyntax.synWex y ps)))

Checked nominal proof certificate identified upstream as g_nfexd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfa2 (ph : SemanticCore.Wff) (x y : SemanticCore.Var) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x (SemanticCore.Wff.all y (SemanticCore.Wff.all x ph)))

Checked nominal proof certificate identified upstream as g_nfa2.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gNfa2 ph x y = NFChoice.DirectNominalPrf.WPPReplay.gNfal (NFChoice.SemanticCore.Wff.all x ph) x y (NFChoice.DirectNominalPrf.WPPReplay.gNfa1 ph x)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN1921bbi (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) (hyp_n_19_21bbi_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.all x (SemanticCore.Wff.all y ps)))) : Nominal.NPrf (ph.imp ps)

Checked nominal proof certificate identified upstream as g_n_19_21bbi.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN1927 (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (hyp_n_19_27_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ps)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.all x (Compiler.CompactSourceSyntax.synWa ph ps)) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.all x ph) ps))

Checked nominal proof certificate identified upstream as g_n_19_27.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN1928 (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (hyp_n_19_28_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ph)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.all x (Compiler.CompactSourceSyntax.synWa ph ps)) (Compiler.CompactSourceSyntax.synWa ph (SemanticCore.Wff.all x ps)))

Checked nominal proof certificate identified upstream as g_n_19_28.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN1936 (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (hyp_n_19_36_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ps)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWex x (ph.imp ps)) ((SemanticCore.Wff.all x ph).imp ps))

Checked nominal proof certificate identified upstream as g_n_19_36.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN1936i (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (hyp_n_19_36_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ps)) (hyp_n_19_36i_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWex x (ph.imp ps))) : Nominal.NPrf ((SemanticCore.Wff.all x ph).imp ps)

Checked nominal proof certificate identified upstream as g_n_19_36i.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN1937 (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (hyp_n_19_37_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ph)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWex x (ph.imp ps)) (ph.imp (Compiler.CompactSourceSyntax.synWex x ps)))

Checked nominal proof certificate identified upstream as g_n_19_37.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN1941 (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (hyp_n_19_41_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ps)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWa ph ps)) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWex x ph) ps))

Checked nominal proof certificate identified upstream as g_n_19_41.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN1942 (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (hyp_n_19_42_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ph)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWa ph ps)) (Compiler.CompactSourceSyntax.synWa ph (Compiler.CompactSourceSyntax.synWex x ps)))

Checked nominal proof certificate identified upstream as g_n_19_42.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfan1 (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (hyp_nfan1_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ph)) (hyp_nfan1_2 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWnf x ps))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x (Compiler.CompactSourceSyntax.synWa ph ps))

Checked nominal proof certificate identified upstream as g_nfan1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAaan (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) (hyp_aaan_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf y ph)) (hyp_aaan_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ps)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.all x (SemanticCore.Wff.all y (Compiler.CompactSourceSyntax.synWa ph ps))) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.all x ph) (SemanticCore.Wff.all y ps)))

Checked nominal proof certificate identified upstream as g_aaan.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEqus5a (ph : SemanticCore.Wff) (x y : SemanticCore.Var) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.objEq x y) (SemanticCore.Wff.all y ph))).imp (SemanticCore.Wff.all x ((SemanticCore.Wff.objEq x y).imp ph)))

Checked nominal proof certificate identified upstream as g_equs5a.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN1921v (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (dv_ph_x : x ∉ ph.fv) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.all x (ph.imp ps)) (ph.imp (SemanticCore.Wff.all x ps)))

Checked nominal proof certificate identified upstream as g_n_19_21v.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gN1921v ph ps x dv_ph_x = NFChoice.DirectNominalPrf.WPPReplay.gN1921 ph ps x (NFChoice.DirectNominalPrf.WPPReplay.gNfv ph x ⋯)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN1923v (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (dv_ps_x : x ∉ ps.fv) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.all x (ph.imp ps)) ((Compiler.CompactSourceSyntax.synWex x ph).imp ps))

Checked nominal proof certificate identified upstream as g_n_19_23v.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gN1923v ph ps x dv_ps_x = NFChoice.DirectNominalPrf.WPPReplay.gN1923 ph ps x (NFChoice.DirectNominalPrf.WPPReplay.gNfv ps x ⋯)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN1923vv (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) (dv_ps_x : x ∉ ps.fv) (dv_ps_y : y ∉ ps.fv) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.all x (SemanticCore.Wff.all y (ph.imp ps))) ((Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWex y ph)).imp ps))

Checked nominal proof certificate identified upstream as g_n_19_23vv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN1927v (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (dv_ps_x : x ∉ ps.fv) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.all x (Compiler.CompactSourceSyntax.synWa ph ps)) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.all x ph) ps))

Checked nominal proof certificate identified upstream as g_n_19_27v.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gN1927v ph ps x dv_ps_x = NFChoice.DirectNominalPrf.WPPReplay.gN1927 ph ps x (NFChoice.DirectNominalPrf.WPPReplay.gNfv ps x ⋯)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN1928v (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (dv_ph_x : x ∉ ph.fv) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.all x (Compiler.CompactSourceSyntax.synWa ph ps)) (Compiler.CompactSourceSyntax.synWa ph (SemanticCore.Wff.all x ps)))

Checked nominal proof certificate identified upstream as g_n_19_28v.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gN1928v ph ps x dv_ph_x = NFChoice.DirectNominalPrf.WPPReplay.gN1928 ph ps x (NFChoice.DirectNominalPrf.WPPReplay.gNfv ph x ⋯)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN1936v (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (dv_ps_x : x ∉ ps.fv) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWex x (ph.imp ps)) ((SemanticCore.Wff.all x ph).imp ps))

Checked nominal proof certificate identified upstream as g_n_19_36v.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gN1936v ph ps x dv_ps_x = NFChoice.DirectNominalPrf.WPPReplay.gN1936 ph ps x (NFChoice.DirectNominalPrf.WPPReplay.gNfv ps x ⋯)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN1936aiv (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (dv_ps_x : x ∉ ps.fv) (hyp_n_19_36aiv_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWex x (ph.imp ps))) : Nominal.NPrf ((SemanticCore.Wff.all x ph).imp ps)

Checked nominal proof certificate identified upstream as g_n_19_36aiv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN1937v (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (dv_ph_x : x ∉ ph.fv) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWex x (ph.imp ps)) (ph.imp (Compiler.CompactSourceSyntax.synWex x ps)))

Checked nominal proof certificate identified upstream as g_n_19_37v.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gN1937v ph ps x dv_ph_x = NFChoice.DirectNominalPrf.WPPReplay.gN1937 ph ps x (NFChoice.DirectNominalPrf.WPPReplay.gNfv ph x ⋯)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN1937aiv (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (dv_ph_x : x ∉ ph.fv) (hyp_n_19_37aiv_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWex x (ph.imp ps))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWex x ps))

Checked nominal proof certificate identified upstream as g_n_19_37aiv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN1941v (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (dv_ps_x : x ∉ ps.fv) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWa ph ps)) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWex x ph) ps))

Checked nominal proof certificate identified upstream as g_n_19_41v.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gN1941v ph ps x dv_ps_x = NFChoice.DirectNominalPrf.WPPReplay.gN1941 ph ps x (NFChoice.DirectNominalPrf.WPPReplay.gNfv ps x ⋯)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN1941vv (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) (dv_ps_x : x ∉ ps.fv) (dv_ps_y : y ∉ ps.fv) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWex y (Compiler.CompactSourceSyntax.synWa ph ps))) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWex y ph)) ps))

Checked nominal proof certificate identified upstream as g_n_19_41vv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN1941vvv (ph ps : SemanticCore.Wff) (x y z : SemanticCore.Var) (dv_ps_x : x ∉ ps.fv) (dv_ps_y : y ∉ ps.fv) (dv_ps_z : z ∉ ps.fv) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWex y (Compiler.CompactSourceSyntax.synWex z (Compiler.CompactSourceSyntax.synWa ph ps)))) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWex y (Compiler.CompactSourceSyntax.synWex z ph))) ps))

Checked nominal proof certificate identified upstream as g_n_19_41vvv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN1942v (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (dv_ph_x : x ∉ ph.fv) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWa ph ps)) (Compiler.CompactSourceSyntax.synWa ph (Compiler.CompactSourceSyntax.synWex x ps)))

Checked nominal proof certificate identified upstream as g_n_19_42v.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gN1942v ph ps x dv_ph_x = NFChoice.DirectNominalPrf.WPPReplay.gN1942 ph ps x (NFChoice.DirectNominalPrf.WPPReplay.gNfv ph x ⋯)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gExdistr (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) (dv_ph_y : y ∉ ph.fv) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWex y (Compiler.CompactSourceSyntax.synWa ph ps))) (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWa ph (Compiler.CompactSourceSyntax.synWex y ps))))

Checked nominal proof certificate identified upstream as g_exdistr.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN1942vv (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) (dv_ph_x : x ∉ ph.fv) (dv_ph_y : y ∉ ph.fv) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWex y (Compiler.CompactSourceSyntax.synWa ph ps))) (Compiler.CompactSourceSyntax.synWa ph (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWex y ps))))

Checked nominal proof certificate identified upstream as g_n_19_42vv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEean (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) (hyp_eean_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf y ph)) (hyp_eean_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ps)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWex y (Compiler.CompactSourceSyntax.synWa ph ps))) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWex x ph) (Compiler.CompactSourceSyntax.synWex y ps)))

Checked nominal proof certificate identified upstream as g_eean.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEeanv (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) (dv_ph_y : y ∉ ph.fv) (dv_ps_x : x ∉ ps.fv) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWex y (Compiler.CompactSourceSyntax.synWa ph ps))) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWex x ph) (Compiler.CompactSourceSyntax.synWex y ps)))

Checked nominal proof certificate identified upstream as g_eeanv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEeeanv (ph ps ch : SemanticCore.Wff) (x y z : SemanticCore.Var) (dv_ch_x : x ∉ ch.fv) (dv_ch_y : y ∉ ch.fv) (dv_ph_y : y ∉ ph.fv) (dv_ph_z : z ∉ ph.fv) (dv_ps_x : x ∉ ps.fv) (dv_ps_z : z ∉ ps.fv) (_dv_x_y : x ≠ y) (dv_x_z : x ≠ z) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWex y (Compiler.CompactSourceSyntax.synWex z (Compiler.CompactSourceSyntax.synW3a ph ps ch)))) (Compiler.CompactSourceSyntax.synW3a (Compiler.CompactSourceSyntax.synWex x ph) (Compiler.CompactSourceSyntax.synWex y ps) (Compiler.CompactSourceSyntax.synWex z ch)))

Checked nominal proof certificate identified upstream as g_eeeanv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEe4anv (ph ps : SemanticCore.Wff) (x y z w : SemanticCore.Var) (dv_ph_w : w ∉ ph.fv) (dv_ph_z : z ∉ ph.fv) (dv_ps_x : x ∉ ps.fv) (dv_ps_y : y ∉ ps.fv) (_dv_w_x : w ≠ x) (_dv_y_z : y ≠ z) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWex y (Compiler.CompactSourceSyntax.synWex z (Compiler.CompactSourceSyntax.synWex w (Compiler.CompactSourceSyntax.synWa ph ps))))) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWex y ph)) (Compiler.CompactSourceSyntax.synWex z (Compiler.CompactSourceSyntax.synWex w ps))))

Checked nominal proof certificate identified upstream as g_ee4anv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNexdv (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (dv_ph_x : x ∉ ph.fv) (hyp_nexdv_1 : Nominal.NPrf (ph.imp ps.neg)) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWex x ps).neg)

Checked nominal proof certificate identified upstream as g_nexdv.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gNexdv ph ps x dv_ph_x hyp_nexdv_1 = NFChoice.DirectNominalPrf.WPPReplay.gNexd ph ps x (NFChoice.DirectNominalPrf.WPPReplay.gNfv ph x ⋯) hyp_nexdv_1

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gStdpc7 (ph : SemanticCore.Wff) (x y : SemanticCore.Var) : Nominal.NPrf ((SemanticCore.Wff.objEq x y).imp ((Compiler.CompactSourceSyntax.synWsb x y ph).imp ph))

Checked nominal proof certificate identified upstream as g_stdpc7.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSbequ1 (ph : SemanticCore.Wff) (x y : SemanticCore.Var) : Nominal.NPrf ((SemanticCore.Wff.objEq x y).imp (ph.imp (Compiler.CompactSourceSyntax.synWsb y x ph)))

Checked nominal proof certificate identified upstream as g_sbequ1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSbequ12 (ph : SemanticCore.Wff) (x y : SemanticCore.Var) : Nominal.NPrf ((SemanticCore.Wff.objEq x y).imp (Compiler.CompactSourceSyntax.synWb ph (Compiler.CompactSourceSyntax.synWsb y x ph)))

Checked nominal proof certificate identified upstream as g_sbequ12.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSbequ12r (ph : SemanticCore.Wff) (x y : SemanticCore.Var) : Nominal.NPrf ((SemanticCore.Wff.objEq x y).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWsb x y ph) ph))

Checked nominal proof certificate identified upstream as g_sbequ12r.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSbid (ph : SemanticCore.Wff) (x : SemanticCore.Var) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWsb x x ph) ph)

Checked nominal proof certificate identified upstream as g_sbid.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSb4a (ph : SemanticCore.Wff) (x y : SemanticCore.Var) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWsb y x (SemanticCore.Wff.all y ph)).imp (SemanticCore.Wff.all x ((SemanticCore.Wff.objEq x y).imp ph)))

Checked nominal proof certificate identified upstream as g_sb4a.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAx12v (x y z : SemanticCore.Var) (_dv_x_z : x ≠ z) (_dv_y_z : y ≠ z) : Nominal.NPrf ((SemanticCore.Wff.objEq x y).neg.imp ((SemanticCore.Wff.objEq y z).imp (SemanticCore.Wff.all x (SemanticCore.Wff.objEq y z))))

Checked nominal proof certificate identified upstream as g_ax12v.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gAx12v x y z _dv_x_z _dv_y_z = NFChoice.DirectNominalPrf.Nominal.ax12 x y z

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAx12olem1 (y z w : SemanticCore.Var) (dv_w_y : w ≠ y) (dv_w_z : w ≠ z) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWex w (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.objEq y w) (SemanticCore.Wff.objEq z w).neg)) (SemanticCore.Wff.objEq y z).neg)

Checked nominal proof certificate identified upstream as g_ax12olem1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAx12olem2 (x y z w : SemanticCore.Var) (dv_w_x : w ≠ x) (dv_w_y : w ≠ y) (dv_w_z : w ≠ z) (dv_x_z : x ≠ z) (hyp_ax12olem2_1 : Nominal.NPrf ((SemanticCore.Wff.objEq x y).neg.imp ((SemanticCore.Wff.objEq y w).imp (SemanticCore.Wff.all x (SemanticCore.Wff.objEq y w))))) : Nominal.NPrf ((SemanticCore.Wff.objEq x y).neg.imp ((SemanticCore.Wff.objEq y z).neg.imp (SemanticCore.Wff.all x (SemanticCore.Wff.objEq y z).neg)))

Checked nominal proof certificate identified upstream as g_ax12olem2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAx12olem3 (x y z : SemanticCore.Var) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ((SemanticCore.Wff.objEq x y).neg.imp ((SemanticCore.Wff.all x (SemanticCore.Wff.objEq y z).neg).neg.imp (SemanticCore.Wff.all x (SemanticCore.Wff.objEq y z)))) (Compiler.CompactSourceSyntax.synWa ((SemanticCore.Wff.objEq x y).neg.imp ((SemanticCore.Wff.objEq y z).imp (SemanticCore.Wff.all x (SemanticCore.Wff.objEq y z)))) ((SemanticCore.Wff.objEq x y).neg.imp ((SemanticCore.Wff.objEq y z).neg.imp (SemanticCore.Wff.all x (SemanticCore.Wff.objEq y z).neg)))))

Checked nominal proof certificate identified upstream as g_ax12olem3.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAx12olem4 (x y z w : SemanticCore.Var) (dv_w_x : w ≠ x) (dv_w_y : w ≠ y) (dv_w_z : w ≠ z) (dv_x_z : x ≠ z) (_dv_y_z : y ≠ z) (hyp_ax12olem4_1 : Nominal.NPrf ((SemanticCore.Wff.objEq x y).neg.imp ((SemanticCore.Wff.objEq y z).imp (SemanticCore.Wff.all x (SemanticCore.Wff.objEq y z))))) (hyp_ax12olem4_2 : Nominal.NPrf ((SemanticCore.Wff.objEq x y).neg.imp ((SemanticCore.Wff.objEq y w).imp (SemanticCore.Wff.all x (SemanticCore.Wff.objEq y w))))) : Nominal.NPrf ((SemanticCore.Wff.objEq x y).neg.imp ((SemanticCore.Wff.all x (SemanticCore.Wff.objEq y z).neg).neg.imp (SemanticCore.Wff.all x (SemanticCore.Wff.objEq y z))))

Checked nominal proof certificate identified upstream as g_ax12olem4.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAx12olem5 (x y z : SemanticCore.Var) (hyp_ax12olem5_1 : Nominal.NPrf ((SemanticCore.Wff.objEq x y).neg.imp ((SemanticCore.Wff.all x (SemanticCore.Wff.objEq y z).neg).neg.imp (SemanticCore.Wff.all x (SemanticCore.Wff.objEq y z))))) : Nominal.NPrf ((SemanticCore.Wff.all x (SemanticCore.Wff.objEq x y)).neg.imp ((SemanticCore.Wff.objEq y z).imp (SemanticCore.Wff.all x (SemanticCore.Wff.objEq y z))))

Checked nominal proof certificate identified upstream as g_ax12olem5.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAx12olem6 (x y z w : SemanticCore.Var) (dv_w_x : w ≠ x) (dv_w_y : w ≠ y) (dv_w_z : w ≠ z) (hyp_ax12olem6_1 : Nominal.NPrf ((SemanticCore.Wff.all x (SemanticCore.Wff.objEq x z)).neg.imp ((SemanticCore.Wff.objEq z w).imp (SemanticCore.Wff.all x (SemanticCore.Wff.objEq z w))))) (hyp_ax12olem6_2 : Nominal.NPrf ((SemanticCore.Wff.all x (SemanticCore.Wff.objEq x y)).neg.imp ((SemanticCore.Wff.objEq y w).imp (SemanticCore.Wff.all x (SemanticCore.Wff.objEq y w))))) : Nominal.NPrf ((SemanticCore.Wff.all x (SemanticCore.Wff.objEq x y)).neg.imp ((SemanticCore.Wff.all x (SemanticCore.Wff.objEq x z)).neg.imp ((SemanticCore.Wff.objEq y z).imp (SemanticCore.Wff.all x (SemanticCore.Wff.objEq y z)))))

Checked nominal proof certificate identified upstream as g_ax12olem6.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAx12olem7 (x y z w : SemanticCore.Var) (dv_w_x : w ≠ x) (dv_w_y : w ≠ y) (dv_w_z : w ≠ z) (hyp_ax12olem7_1 : Nominal.NPrf ((SemanticCore.Wff.objEq x z).neg.imp ((SemanticCore.Wff.all x (SemanticCore.Wff.objEq z w).neg).neg.imp (SemanticCore.Wff.all x (SemanticCore.Wff.objEq z w))))) (hyp_ax12olem7_2 : Nominal.NPrf ((SemanticCore.Wff.objEq x y).neg.imp ((SemanticCore.Wff.all x (SemanticCore.Wff.objEq y w).neg).neg.imp (SemanticCore.Wff.all x (SemanticCore.Wff.objEq y w))))) : Nominal.NPrf ((SemanticCore.Wff.all x (SemanticCore.Wff.objEq x y)).neg.imp ((SemanticCore.Wff.all x (SemanticCore.Wff.objEq x z)).neg.imp ((SemanticCore.Wff.objEq y z).imp (SemanticCore.Wff.all x (SemanticCore.Wff.objEq y z)))))

Checked nominal proof certificate identified upstream as g_ax12olem7.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAx12o (x y z : SemanticCore.Var) : Nominal.NPrf ((SemanticCore.Wff.all z (SemanticCore.Wff.objEq z x)).neg.imp ((SemanticCore.Wff.all z (SemanticCore.Wff.objEq z y)).neg.imp ((SemanticCore.Wff.objEq x y).imp (SemanticCore.Wff.all z (SemanticCore.Wff.objEq x y)))))

Checked nominal proof certificate identified upstream as g_ax12o.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAx10lem1 (x y w : SemanticCore.Var) (dv_w_x : w ≠ x) (dv_w_y : w ≠ y) : Nominal.NPrf ((SemanticCore.Wff.all x (SemanticCore.Wff.objEq x w)).imp (SemanticCore.Wff.all y (SemanticCore.Wff.objEq y w)))

Checked nominal proof certificate identified upstream as g_ax10lem1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAx10lem2 (x y z : SemanticCore.Var) (dv_x_y : x ≠ y) (dv_x_z : x ≠ z) : Nominal.NPrf ((SemanticCore.Wff.all x (SemanticCore.Wff.objEq x y)).imp (SemanticCore.Wff.all x (SemanticCore.Wff.objEq x z)))

Checked nominal proof certificate identified upstream as g_ax10lem2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAx10lem3 (x y : SemanticCore.Var) (dv_x_y : x ≠ y) : Nominal.NPrf ((SemanticCore.Wff.all x (SemanticCore.Wff.objEq x y)).imp (SemanticCore.Wff.all y (SemanticCore.Wff.objEq y x)))

Checked nominal proof certificate identified upstream as g_ax10lem3.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDvelimv (ph ps : SemanticCore.Wff) (x y z : SemanticCore.Var) (dv_ph_x : x ∉ ph.fv) (dv_ps_z : z ∉ ps.fv) (dv_x_z : x ≠ z) (dv_y_z : y ≠ z) (hyp_dvelimv_1 : Nominal.NPrf ((SemanticCore.Wff.objEq z y).imp (Compiler.CompactSourceSyntax.synWb ph ps))) : Nominal.NPrf ((SemanticCore.Wff.all x (SemanticCore.Wff.objEq x y)).neg.imp (ps.imp (SemanticCore.Wff.all x ps)))

Checked nominal proof certificate identified upstream as g_dvelimv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDveeq2 (x y z : SemanticCore.Var) (dv_x_z : x ≠ z) : Nominal.NPrf ((SemanticCore.Wff.all x (SemanticCore.Wff.objEq x y)).neg.imp ((SemanticCore.Wff.objEq z y).imp (SemanticCore.Wff.all x (SemanticCore.Wff.objEq z y))))

Checked nominal proof certificate identified upstream as g_dveeq2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAx10lem4 (x y w : SemanticCore.Var) (dv_w_x : w ≠ x) (dv_w_y : w ≠ y) : Nominal.NPrf ((SemanticCore.Wff.all x (SemanticCore.Wff.objEq x w)).imp (SemanticCore.Wff.all y (SemanticCore.Wff.objEq y x)))

Checked nominal proof certificate identified upstream as g_ax10lem4.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAx10lem5 (x y z w : SemanticCore.Var) (dv_w_z : w ≠ z) : Nominal.NPrf ((SemanticCore.Wff.all z (SemanticCore.Wff.objEq z w)).imp (SemanticCore.Wff.all y (SemanticCore.Wff.objEq y x)))

Checked nominal proof certificate identified upstream as g_ax10lem5.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAx10lem6 (ph : SemanticCore.Wff) (x y : SemanticCore.Var) : Nominal.NPrf ((SemanticCore.Wff.all y (SemanticCore.Wff.objEq y x)).imp ((SemanticCore.Wff.all x ph).imp (SemanticCore.Wff.all y ph)))

Checked nominal proof certificate identified upstream as g_ax10lem6.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAx10 (x y : SemanticCore.Var) : Nominal.NPrf ((SemanticCore.Wff.all x (SemanticCore.Wff.objEq x y)).imp (SemanticCore.Wff.all y (SemanticCore.Wff.objEq y x)))

Checked nominal proof certificate identified upstream as g_ax10.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gA16g (ph : SemanticCore.Wff) (x y z : SemanticCore.Var) (dv_x_y : x ≠ y) : Nominal.NPrf ((SemanticCore.Wff.all x (SemanticCore.Wff.objEq x y)).imp (ph.imp (SemanticCore.Wff.all z ph)))

Checked nominal proof certificate identified upstream as g_a16g.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAecom (x y : SemanticCore.Var) : Nominal.NPrf ((SemanticCore.Wff.all x (SemanticCore.Wff.objEq x y)).imp (SemanticCore.Wff.all y (SemanticCore.Wff.objEq y x)))

Checked nominal proof certificate identified upstream as g_aecom.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gAecom x y = NFChoice.DirectNominalPrf.WPPReplay.gAx10 x y

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAecoms (ph : SemanticCore.Wff) (x y : SemanticCore.Var) (hyp_alequcoms_1 : Nominal.NPrf ((SemanticCore.Wff.all x (SemanticCore.Wff.objEq x y)).imp ph)) : Nominal.NPrf ((SemanticCore.Wff.all y (SemanticCore.Wff.objEq y x)).imp ph)

Checked nominal proof certificate identified upstream as g_aecoms.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAx9 (x y : SemanticCore.Var) : Nominal.NPrf (SemanticCore.Wff.all x (SemanticCore.Wff.objEq x y).neg).neg

Checked nominal proof certificate identified upstream as g_ax9.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAx9o (ph : SemanticCore.Wff) (x y : SemanticCore.Var) : Nominal.NPrf ((SemanticCore.Wff.all x ((SemanticCore.Wff.objEq x y).imp (SemanticCore.Wff.all x ph))).imp ph)

Checked nominal proof certificate identified upstream as g_ax9o.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gA9e (x y : SemanticCore.Var) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWex x (SemanticCore.Wff.objEq x y))

Checked nominal proof certificate identified upstream as g_a9e.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAx10o (ph : SemanticCore.Wff) (x y : SemanticCore.Var) : Nominal.NPrf ((SemanticCore.Wff.all x (SemanticCore.Wff.objEq x y)).imp ((SemanticCore.Wff.all x ph).imp (SemanticCore.Wff.all y ph)))

Checked nominal proof certificate identified upstream as g_ax10o.

Equations

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