Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk013Compact001Part001.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBrdisj (A B : SemanticCore.Class) (hyp_brdisj_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_brdisj_2 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr A Compiler.CompactSourceSyntax.synCdisj B) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin A B) Compiler.CompactSourceSyntax.synC0))

Checked nominal proof certificate identified upstream as g_brdisj.

Equations

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

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

Checked nominal proof certificate identified upstream as g_disjex.

Equations

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

Certificates from NominalWPPReplayChunk013Compact001Part002.

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

Checked nominal proof certificate identified upstream as g_addcfnex.

Equations

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

Certificates from NominalWPPReplayChunk013Compact001Part003.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAddcfn : Nominal.NPrf (Compiler.CompactSourceSyntax.synWfn Compiler.CompactSourceSyntax.synCaddcfn Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_addcfn.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBraddcfn (A B C : SemanticCore.Class) (hyp_braddcfn_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_braddcfn_2 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCop A B) Compiler.CompactSourceSyntax.synCaddcfn C) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCplc A B) C))

Checked nominal proof certificate identified upstream as g_braddcfn.

Equations

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

Certificates from NominalWPPReplayChunk013Compact001Part004.

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

Checked nominal proof certificate identified upstream as g_funsex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElfuns (F : SemanticCore.Class) (hyp_elfuns_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCfuns) (Compiler.CompactSourceSyntax.synWfun F))

Checked nominal proof certificate identified upstream as g_elfuns.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElfunsg (F V : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem F V).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCfuns) (Compiler.CompactSourceSyntax.synWfun F)))

Checked nominal proof certificate identified upstream as g_elfunsg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElfunsi (F : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCfuns).imp (Compiler.CompactSourceSyntax.synWfun F))

Checked nominal proof certificate identified upstream as g_elfunsi.

Equations

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

Certificates from NominalWPPReplayChunk013Compact001Part005.

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

Checked nominal proof certificate identified upstream as g_fnsex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBrfns (A F : SemanticCore.Class) (hyp_brfns_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr F Compiler.CompactSourceSyntax.synCfns A) (Compiler.CompactSourceSyntax.synWfn F A))

Checked nominal proof certificate identified upstream as g_brfns.

Equations

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

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

Checked nominal proof certificate identified upstream as g_pprodeq2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gQrpprod (A B C D R S : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCop A B) (Compiler.CompactSourceSyntax.synCpprod R S) (Compiler.CompactSourceSyntax.synCop C D)) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr A R C) (Compiler.CompactSourceSyntax.synWbr B S D)))

Checked nominal proof certificate identified upstream as g_qrpprod.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPprodexg (A B V W : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A V) (SemanticCore.Wff.classMem B W)).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCpprod A B) Compiler.CompactSourceSyntax.synCvv))

Checked nominal proof certificate identified upstream as g_pprodexg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPprodex (A B : SemanticCore.Class) (hyp_pprodex_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_pprodex_2 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCpprod A B) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_pprodex.

Equations

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