Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk015Compact001Part027.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLnimageopval (B R : SemanticCore.Class) (hyp_lnimageopval_1 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) (hyp_lnimageopval_2 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synClnimageop (Compiler.CompactSourceSyntax.synCop R B)) (Compiler.CompactSourceSyntax.synCima R B))

Checked nominal proof certificate identified upstream as g_lnimageopval.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLnpwcnvkerfnval (D R : SemanticCore.Class) (hyp_lnpwcnvkerfnval_1 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) (hyp_lnpwcnvkerfnval_2 : Nominal.NPrf (SemanticCore.Wff.classMem D Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synClnpwcnvkerfn (Compiler.CompactSourceSyntax.synCop R D)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synClnker R)))

Checked nominal proof certificate identified upstream as g_lnpwcnvkerfnval.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLnpwclasspairfnval (D R S : SemanticCore.Class) (hyp_lnpwclasspairfnval_1 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) (hyp_lnpwclasspairfnval_2 : Nominal.NPrf (SemanticCore.Wff.classMem D Compiler.CompactSourceSyntax.synCvv)) (hyp_lnpwclasspairfnval_3 : Nominal.NPrf (SemanticCore.Wff.classMem S Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synClnpwclasspairfn (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCop R D) S)) (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synClnker R)) S))

Checked nominal proof certificate identified upstream as g_lnpwclasspairfnval.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLnpwclassfnfn : Nominal.NPrf (Compiler.CompactSourceSyntax.synWfn Compiler.CompactSourceSyntax.synClnpwclassfn Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_lnpwclassfnfn.

Equations

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

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

Checked nominal proof certificate identified upstream as g_lnpwclassfnex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLnpwclassfnval (D R S : SemanticCore.Class) (hyp_lnpwclassfnval_1 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) (hyp_lnpwclassfnval_2 : Nominal.NPrf (SemanticCore.Wff.classMem D Compiler.CompactSourceSyntax.synCvv)) (hyp_lnpwclassfnval_3 : Nominal.NPrf (SemanticCore.Wff.classMem S Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synClnpwclassfn (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCop R D) S)) (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synClnker R)) S))

Checked nominal proof certificate identified upstream as g_lnpwclassfnval.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLnpwpw1secondfnfn : Nominal.NPrf (Compiler.CompactSourceSyntax.synWfn Compiler.CompactSourceSyntax.synClnpwpw1secondfn Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_lnpwpw1secondfnfn.

Equations

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

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

Checked nominal proof certificate identified upstream as g_lnpwpw1secondfnex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLnpwpw1secondfnval (D R : SemanticCore.Class) (hyp_lnpwpw1secondfnval_1 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) (hyp_lnpwpw1secondfnval_2 : Nominal.NPrf (SemanticCore.Wff.classMem D Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synClnpwpw1secondfn (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCop R D))) (Compiler.CompactSourceSyntax.synCpw1 D))

Checked nominal proof certificate identified upstream as g_lnpwpw1secondfnval.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLnpwquoinputfnfn : Nominal.NPrf (Compiler.CompactSourceSyntax.synWfn Compiler.CompactSourceSyntax.synClnpwquoinputfn Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_lnpwquoinputfnfn.

Equations

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

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

Checked nominal proof certificate identified upstream as g_lnpwquoinputfnex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLnpwquoinputfnval (D R : SemanticCore.Class) (hyp_lnpwquoinputfnval_1 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) (hyp_lnpwquoinputfnval_2 : Nominal.NPrf (SemanticCore.Wff.classMem D Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synClnpwquoinputfn (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCop R D))) (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCop R D)) (Compiler.CompactSourceSyntax.synCpw1 D)))

Checked nominal proof certificate identified upstream as g_lnpwquoinputfnval.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLnpwquofnfn : Nominal.NPrf (Compiler.CompactSourceSyntax.synWfn Compiler.CompactSourceSyntax.synClnpwquofn Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_lnpwquofnfn.

Equations

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

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

Checked nominal proof certificate identified upstream as g_lnpwquofnex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLnpwquofnrawval (D R : SemanticCore.Class) (hyp_lnpwquofnrawval_1 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) (hyp_lnpwquofnrawval_2 : Nominal.NPrf (SemanticCore.Wff.classMem D Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synClnpwquofn (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCop R D))) (Compiler.CompactSourceSyntax.synCima Compiler.CompactSourceSyntax.synClnpwclassfn (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCop R D)) (Compiler.CompactSourceSyntax.synCpw1 D))))

Checked nominal proof certificate identified upstream as g_lnpwquofnrawval.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLnpwclassfnsnval (D R X : SemanticCore.Class) (hyp_lnpwclassfnsnval_1 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) (hyp_lnpwclassfnsnval_2 : Nominal.NPrf (SemanticCore.Wff.classMem D Compiler.CompactSourceSyntax.synCvv)) (_hyp_lnpwclassfnsnval_3 : Nominal.NPrf (SemanticCore.Wff.classMem X Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synClnpwclassfn (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCop R D) (Compiler.CompactSourceSyntax.synCsn X))) (Compiler.CompactSourceSyntax.synCec X (Compiler.CompactSourceSyntax.synClnker R)))

Checked nominal proof certificate identified upstream as g_lnpwclassfnsnval.

Equations

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

Certificates from NominalWPPReplayChunk015Compact001Part028.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLnpwquofnrawexact (D R : SemanticCore.Class) (hyp_lnpwquofnrawexact_1 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) (hyp_lnpwquofnrawexact_2 : Nominal.NPrf (SemanticCore.Wff.classMem D Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCima Compiler.CompactSourceSyntax.synClnpwclassfn (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCop R D)) (Compiler.CompactSourceSyntax.synCpw1 D))) (Compiler.CompactSourceSyntax.synCqs D (Compiler.CompactSourceSyntax.synClnker R)))

Checked nominal proof certificate identified upstream as g_lnpwquofnrawexact.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLnpwquofnval (D R : SemanticCore.Class) (hyp_lnpwquofnval_1 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) (hyp_lnpwquofnval_2 : Nominal.NPrf (SemanticCore.Wff.classMem D Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synClnpwquofn (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCop R D))) (Compiler.CompactSourceSyntax.synCqs D (Compiler.CompactSourceSyntax.synClnker R)))

Checked nominal proof certificate identified upstream as g_lnpwquofnval.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLnpairraisefnfn : Nominal.NPrf (Compiler.CompactSourceSyntax.synWfn Compiler.CompactSourceSyntax.synClnpairraisefn Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_lnpairraisefnfn.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLnpairraisefnval (X Y : SemanticCore.Class) (hyp_lnpairraisefnval_1 : Nominal.NPrf (SemanticCore.Wff.classMem X Compiler.CompactSourceSyntax.synCvv)) (hyp_lnpairraisefnval_2 : Nominal.NPrf (SemanticCore.Wff.classMem Y Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synClnpairraisefn (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCop X Y))) (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCsn X) (Compiler.CompactSourceSyntax.synCsn Y)))

Checked nominal proof certificate identified upstream as g_lnpairraisefnval.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLnsifnfn : Nominal.NPrf (Compiler.CompactSourceSyntax.synWfn Compiler.CompactSourceSyntax.synClnsifn Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_lnsifnfn.

Equations

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

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

Checked nominal proof certificate identified upstream as g_lnsifnex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLnsifnrawval (R : SemanticCore.Class) (hyp_lnsifnrawval_1 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synClnsifn (Compiler.CompactSourceSyntax.synCsn R)) (Compiler.CompactSourceSyntax.synCima Compiler.CompactSourceSyntax.synClnpairraisefn (Compiler.CompactSourceSyntax.synCpw1 R)))

Checked nominal proof certificate identified upstream as g_lnsifnrawval.

Equations

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

Certificates from NominalWPPReplayChunk015Compact001Part029.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLnsifnimageexactg (R : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWss R (Compiler.CompactSourceSyntax.synCxp Compiler.CompactSourceSyntax.synCvv Compiler.CompactSourceSyntax.synCvv)).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCima Compiler.CompactSourceSyntax.synClnpairraisefn (Compiler.CompactSourceSyntax.synCpw1 R)) (Compiler.CompactSourceSyntax.synCsi R)))

Checked nominal proof certificate identified upstream as g_lnsifnimageexactg.

Equations

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

Certificates from NominalWPPReplayChunk015Compact001Part030.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLnsifnvalg (R : SemanticCore.Class) (hyp_lnsifnvalg_1 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWss R (Compiler.CompactSourceSyntax.synCxp Compiler.CompactSourceSyntax.synCvv Compiler.CompactSourceSyntax.synCvv)).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synClnsifn (Compiler.CompactSourceSyntax.synCsn R)) (Compiler.CompactSourceSyntax.synCsi R)))

Checked nominal proof certificate identified upstream as g_lnsifnvalg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLnpwsirelfnfn : Nominal.NPrf (Compiler.CompactSourceSyntax.synWfn Compiler.CompactSourceSyntax.synClnpwsirelfn Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_lnpwsirelfnfn.

Equations

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

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

Checked nominal proof certificate identified upstream as g_lnpwsirelfnex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLnpwsirelfnrawval (D R : SemanticCore.Class) (_hyp_lnpwsirelfnrawval_1 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) (hyp_lnpwsirelfnrawval_2 : Nominal.NPrf (SemanticCore.Wff.classMem D Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synClnpwsirelfn (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCop R D))) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synClnsifn (Compiler.CompactSourceSyntax.synCsn R)))

Checked nominal proof certificate identified upstream as g_lnpwsirelfnrawval.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLnpwsirelfnvalg (D R : SemanticCore.Class) (hyp_lnpwsirelfnvalg_1 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) (hyp_lnpwsirelfnvalg_2 : Nominal.NPrf (SemanticCore.Wff.classMem D Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWss R (Compiler.CompactSourceSyntax.synCxp Compiler.CompactSourceSyntax.synCvv Compiler.CompactSourceSyntax.synCvv)).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synClnpwsirelfn (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCop R D))) (Compiler.CompactSourceSyntax.synCsi R)))

Checked nominal proof certificate identified upstream as g_lnpwsirelfnvalg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPw1subuniss (x : SemanticCore.Var) (A : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWss (SemanticCore.Class.cv x) (Compiler.CompactSourceSyntax.synCpw1 A)).imp (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv x)) A))

Checked nominal proof certificate identified upstream as g_pw1subuniss.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPw1subunine (x : SemanticCore.Var) (A : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWss (SemanticCore.Class.cv x) (Compiler.CompactSourceSyntax.synCpw1 A)) (Compiler.CompactSourceSyntax.synWne (SemanticCore.Class.cv x) Compiler.CompactSourceSyntax.synC0)).imp (Compiler.CompactSourceSyntax.synWne (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv x)) Compiler.CompactSourceSyntax.synC0))

Checked nominal proof certificate identified upstream as g_pw1subunine.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppreachopfn (F : SemanticCore.Class) (hyp_wppreachopfn_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWfn (Compiler.CompactSourceSyntax.synCimage (Compiler.CompactSourceSyntax.synCcnv F)) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_wppreachopfn.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppreachupperex (C : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCima Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCsn C)) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_wppreachupperex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppreach0 (C F : SemanticCore.Class) (dv_C_F : Disjoint C.fv F.fv) (hyp_wppreachorbitfn_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec (Compiler.CompactSourceSyntax.synCimage (Compiler.CompactSourceSyntax.synCcnv F)) (Compiler.CompactSourceSyntax.synCima Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCsn C))) Compiler.CompactSourceSyntax.synC0c) (Compiler.CompactSourceSyntax.synCima Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCsn C)))

Checked nominal proof certificate identified upstream as g_wppreach0.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElwppcand (C D F : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem D (Compiler.CompactSourceSyntax.synCwppcand F C)) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem D (Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv)) (Compiler.CompactSourceSyntax.synWbr D Compiler.CompactSourceSyntax.synClec C)) (SemanticCore.Wff.classMem D (Compiler.CompactSourceSyntax.synCwppreach F C))))

Checked nominal proof certificate identified upstream as g_elwppcand.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHwcnwendv (u : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_u : u ∉ A.fv) : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn A)).imp (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv u)) Compiler.CompactSourceSyntax.synCwe (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))

Checked nominal proof certificate identified upstream as g_hwcnwendv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHwbaseswev (r d : SemanticCore.Var) (dv_d_r : d ≠ r) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (SemanticCore.Class.cv d) (Compiler.CompactSourceSyntax.synChwbases Compiler.CompactSourceSyntax.synCvv)) (Compiler.CompactSourceSyntax.synWex r (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCwe (SemanticCore.Class.cv d))))

Checked nominal proof certificate identified upstream as g_hwbaseswev.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElhwcardswev (k s d : SemanticCore.Var) (dv_d_k : d ≠ k) (dv_d_s : d ≠ s) (dv_k_s : k ≠ s) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (SemanticCore.Class.cv k) (Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv)) (Compiler.CompactSourceSyntax.synWex d (Compiler.CompactSourceSyntax.synWex s (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv s) Compiler.CompactSourceSyntax.synCwe (SemanticCore.Class.cv d)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv k) (Compiler.CompactSourceSyntax.synCnc (SemanticCore.Class.cv d)))))))

Checked nominal proof certificate identified upstream as g_elhwcardswev.

Equations

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

Certificates from NominalWPPReplayChunk015Compact001Part031.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHwcardslecanti (k m : SemanticCore.Var) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv k) (Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv m) (Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv))).imp ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv k) Compiler.CompactSourceSyntax.synClec (SemanticCore.Class.cv m)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv m) Compiler.CompactSourceSyntax.synClec (SemanticCore.Class.cv k))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv k) (SemanticCore.Class.cv m))))

Checked nominal proof certificate identified upstream as g_hwcardslecanti.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWpporbitfnndv (F I : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCfuns) (SemanticCore.Wff.classMem I (Compiler.CompactSourceSyntax.synCdm F)) (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn F) (Compiler.CompactSourceSyntax.synCdm F))).imp (Compiler.CompactSourceSyntax.synWfn (Compiler.CompactSourceSyntax.synCfrec F I) Compiler.CompactSourceSyntax.synCnnc))

Checked nominal proof certificate identified upstream as g_wpporbitfnndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWpporbit0ndv (F I : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCfuns) (SemanticCore.Wff.classMem I (Compiler.CompactSourceSyntax.synCdm F)) (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn F) (Compiler.CompactSourceSyntax.synCdm F))).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec F I) Compiler.CompactSourceSyntax.synC0c) I))

Checked nominal proof certificate identified upstream as g_wpporbit0ndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWpporbitsucndv (F I N : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCfuns) (SemanticCore.Wff.classMem I (Compiler.CompactSourceSyntax.synCdm F)) (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn F) (Compiler.CompactSourceSyntax.synCdm F))) (SemanticCore.Wff.classMem N Compiler.CompactSourceSyntax.synCnnc)).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec F I) (Compiler.CompactSourceSyntax.synCplc N Compiler.CompactSourceSyntax.synC1c)) (Compiler.CompactSourceSyntax.synCfv F (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec F I) N))))

Checked nominal proof certificate identified upstream as g_wpporbitsucndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLnwpwccore (A R : SemanticCore.Class) (dv_A_R : Disjoint A.fv R.fv) (hyp_lnwpwccore_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_lnwpwccore_2 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) (hyp_lnwpwccore_3 : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop R A) (Compiler.CompactSourceSyntax.synClnpwc A))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCref A) (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCtrans A)) (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCconnex A)) (Compiler.CompactSourceSyntax.synWss R (Compiler.CompactSourceSyntax.synCxp A A)))

Checked nominal proof certificate identified upstream as g_lnwpwccore.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLnworigqordwe (A R : SemanticCore.Class) (dv_A_R : Disjoint A.fv R.fv) (hyp_lnworigqordwe_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_lnworigqordwe_2 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) (hyp_lnworigqordwe_3 : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop R A) (Compiler.CompactSourceSyntax.synClnpwc A))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synClnqord R A) Compiler.CompactSourceSyntax.synCwe (Compiler.CompactSourceSyntax.synClnquo R A))

Checked nominal proof certificate identified upstream as g_lnworigqordwe.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppreachsucndv (C F N : SemanticCore.Class) (dv_C_F : Disjoint C.fv F.fv) (dv_C_N : Disjoint C.fv N.fv) (dv_F_N : Disjoint F.fv N.fv) (hyp_wppreachsucndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((SemanticCore.Wff.classMem N Compiler.CompactSourceSyntax.synCnnc).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec (Compiler.CompactSourceSyntax.synCimage (Compiler.CompactSourceSyntax.synCcnv F)) (Compiler.CompactSourceSyntax.synCima Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCsn C))) (Compiler.CompactSourceSyntax.synCplc N Compiler.CompactSourceSyntax.synC1c)) (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv F) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec (Compiler.CompactSourceSyntax.synCimage (Compiler.CompactSourceSyntax.synCcnv F)) (Compiler.CompactSourceSyntax.synCima Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCsn C))) N))))

Checked nominal proof certificate identified upstream as g_wppreachsucndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWpppredfamex (C F : SemanticCore.Class) (hyp_wpppredfamex_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCwpppredfam F C) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_wpppredfamex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppimagefun (R : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWfun (Compiler.CompactSourceSyntax.synCimage R))

Checked nominal proof certificate identified upstream as g_wppimagefun.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppimagefv (B G : SemanticCore.Class) (hyp_wppimagefv_1 : Nominal.NPrf (SemanticCore.Wff.classMem G Compiler.CompactSourceSyntax.synCvv)) (hyp_wppimagefv_2 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCimage G) B) (Compiler.CompactSourceSyntax.synCima G B))

Checked nominal proof certificate identified upstream as g_wppimagefv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppreachorbitfnndv (C F : SemanticCore.Class) (hyp_wppreachorbitfnndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWfn (Compiler.CompactSourceSyntax.synCfrec (Compiler.CompactSourceSyntax.synCimage (Compiler.CompactSourceSyntax.synCcnv F)) (Compiler.CompactSourceSyntax.synCima Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCsn C))) Compiler.CompactSourceSyntax.synCnnc)

Checked nominal proof certificate identified upstream as g_wppreachorbitfnndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWpppredfamfv (C D F : SemanticCore.Class) (hyp_wpppredfamfv_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCwpppredfam F C) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCsn D))) (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCfrec (Compiler.CompactSourceSyntax.synCimage (Compiler.CompactSourceSyntax.synCcnv F)) (Compiler.CompactSourceSyntax.synCima Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCsn C))) Compiler.CompactSourceSyntax.synCtcfn)) (Compiler.CompactSourceSyntax.synCima Compiler.CompactSourceSyntax.synCsset (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCsn D)))))

Checked nominal proof certificate identified upstream as g_wpppredfamfv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElwpppredfam (C D F : SemanticCore.Class) (q : SemanticCore.Var) (hyp_elwpppredfam_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCvv)) (hyp_elwpppredfam_2 : Nominal.NPrf (SemanticCore.Wff.classMem D Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv q)) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCwpppredfam F C) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCsn D)))) (SemanticCore.Wff.classMem D (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec (Compiler.CompactSourceSyntax.synCimage (Compiler.CompactSourceSyntax.synCcnv F)) (Compiler.CompactSourceSyntax.synCima Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCsn C))) (Compiler.CompactSourceSyntax.synCtc (SemanticCore.Class.cv q)))))

Checked nominal proof certificate identified upstream as g_elwpppredfam.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWpppostcompex (F : SemanticCore.Class) (_hyp_wpppostcompex_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCwpppostcomp F) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_wpppostcompex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppupperpreopex (C : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCwppupperpreop C) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_wppupperpreopex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWpppowlayerseqex (C F : SemanticCore.Class) (hyp_wpppowlayerseqex_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCwpppowlayerseq F C) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_wpppowlayerseqex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWpphitfamex (C F : SemanticCore.Class) (hyp_wpphitfamex_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCwpphitfam F C) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_wpphitfamex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWpppostcompfn (F : SemanticCore.Class) (hyp_wpppostcompfn_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWfn (Compiler.CompactSourceSyntax.synCwpppostcomp F) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_wpppostcompfn.

Equations

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