Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk016Compact001Part056.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppcardt4fnvalsingndv (D : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem D Compiler.CompactSourceSyntax.synCncs).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synCwppcardt4fn (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCsn D))))) (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc D))))))

Checked nominal proof certificate identified upstream as g_wppcardt4fnvalsingndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCnv2resndv (A B R : SemanticCore.Class) (_dv_A_R : Disjoint A.fv R.fv) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCres (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCres R A)) B)) (Compiler.CompactSourceSyntax.synCin R (Compiler.CompactSourceSyntax.synCxp A B)))

Checked nominal proof certificate identified upstream as g_cnv2resndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCnvrngresndv (B R : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCres (Compiler.CompactSourceSyntax.synCcnv R) B)) (Compiler.CompactSourceSyntax.synCin R (Compiler.CompactSourceSyntax.synCxp Compiler.CompactSourceSyntax.synCvv B)))

Checked nominal proof certificate identified upstream as g_cnvrngresndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHwcodesunivndv : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synChwcodes Compiler.CompactSourceSyntax.synCvv) Compiler.CompactSourceSyntax.synCwe)

Checked nominal proof certificate identified upstream as g_hwcodesunivndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHwcnunivrrndv (A : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCres (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChwcn Compiler.CompactSourceSyntax.synCvv)) (Compiler.CompactSourceSyntax.synCpw A))) (Compiler.CompactSourceSyntax.synChwcn A))

Checked nominal proof certificate identified upstream as g_hwcnunivrrndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHwnisogendrrndv (A : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCres (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCres (Compiler.CompactSourceSyntax.synCima Compiler.CompactSourceSyntax.synChwgen (Compiler.CompactSourceSyntax.synCxp Compiler.CompactSourceSyntax.synChwbij Compiler.CompactSourceSyntax.synCvv)) (Compiler.CompactSourceSyntax.synChwcn A))) (Compiler.CompactSourceSyntax.synChwcn A))) (Compiler.CompactSourceSyntax.synChwniso A))

Checked nominal proof certificate identified upstream as g_hwnisogendrrndv.

Equations

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

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

Checked nominal proof certificate identified upstream as g_wpppowsetfnexndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWpppowsetfnfnndv : Nominal.NPrf (Compiler.CompactSourceSyntax.synWfn Compiler.CompactSourceSyntax.synCwpppowsetfn Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_wpppowsetfnfnndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWpppowsetfnvalndv (A : SemanticCore.Class) (hyp_wpppowsetfnvalndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synCwpppowsetfn (Compiler.CompactSourceSyntax.synCsn A)) (Compiler.CompactSourceSyntax.synCpw A))

Checked nominal proof certificate identified upstream as g_wpppowsetfnvalndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWpphwcnsetfnvalndv (A : SemanticCore.Class) (hyp_wpphwcnsetfnvalndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synCwpphwcnsetfn (Compiler.CompactSourceSyntax.synCsn A)) (Compiler.CompactSourceSyntax.synChwcn A))

Checked nominal proof certificate identified upstream as g_wpphwcnsetfnvalndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWpphwgendomfnvalndv (A : SemanticCore.Class) (hyp_wpphwgendomfnvalndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synCwpphwgendomfn (Compiler.CompactSourceSyntax.synCsn A)) (Compiler.CompactSourceSyntax.synCres (Compiler.CompactSourceSyntax.synCima Compiler.CompactSourceSyntax.synChwgen (Compiler.CompactSourceSyntax.synCxp Compiler.CompactSourceSyntax.synChwbij Compiler.CompactSourceSyntax.synCvv)) (Compiler.CompactSourceSyntax.synChwcn A)))

Checked nominal proof certificate identified upstream as g_wpphwgendomfnvalndv.

Equations

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

Certificates from NominalWPPReplayChunk016Compact001Part057.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWpphwgencnvfnvalndv (A : SemanticCore.Class) (hyp_wpphwgencnvfnvalndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synCwpphwgencnvfn (Compiler.CompactSourceSyntax.synCsn A)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCres (Compiler.CompactSourceSyntax.synCima Compiler.CompactSourceSyntax.synChwgen (Compiler.CompactSourceSyntax.synCxp Compiler.CompactSourceSyntax.synChwbij Compiler.CompactSourceSyntax.synCvv)) (Compiler.CompactSourceSyntax.synChwcn A))))

Checked nominal proof certificate identified upstream as g_wpphwgencnvfnvalndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWpphwnisosetfnvalndv (A : SemanticCore.Class) (hyp_wpphwnisosetfnvalndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synCwpphwnisosetfn (Compiler.CompactSourceSyntax.synCsn A)) (Compiler.CompactSourceSyntax.synChwniso A))

Checked nominal proof certificate identified upstream as g_wpphwnisosetfnvalndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWpphnpairfnvalndv (A : SemanticCore.Class) (hyp_wpphnpairfnvalndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synCwpphnpairfn (Compiler.CompactSourceSyntax.synCsn A)) (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synChwniso A) (Compiler.CompactSourceSyntax.synChwcn A)))

Checked nominal proof certificate identified upstream as g_wpphnpairfnvalndv.

Equations

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

Certificates from NominalWPPReplayChunk016Compact001Part058.

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

Checked nominal proof certificate identified upstream as g_wpphninputfnexndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWpphninputfnmapndv : Nominal.NPrf (Compiler.CompactSourceSyntax.synWf Compiler.CompactSourceSyntax.synCwpphninputfn (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synCvv) (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synCvv))

Checked nominal proof certificate identified upstream as g_wpphninputfnmapndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWpphninputfnvalndv (A : SemanticCore.Class) (hyp_wpphninputfnvalndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synCwpphninputfn (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCsn A))) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synChwniso A) (Compiler.CompactSourceSyntax.synChwcn A))))

Checked nominal proof certificate identified upstream as g_wpphninputfnvalndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFdpointimagevvdndv (A : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCfdpointrel Compiler.CompactSourceSyntax.synCvv) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCsn A))) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 A))))

Checked nominal proof certificate identified upstream as g_fdpointimagevvdndv.

Equations

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

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

Checked nominal proof certificate identified upstream as g_wppqkrelkernelexndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppqkrelkernelvalndv (A : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCimak Compiler.CompactSourceSyntax.synCwppqkrelkernel (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 A))) (Compiler.CompactSourceSyntax.synCqkrel A))

Checked nominal proof certificate identified upstream as g_wppqkrelkernelvalndv.

Equations

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

Certificates from NominalWPPReplayChunk016Compact001Part059.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHwnisolnkereqndv (A : SemanticCore.Class) (hyp_hwnisolnkereqndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synClnker (Compiler.CompactSourceSyntax.synChwniso A)) (Compiler.CompactSourceSyntax.synChwniso A))

Checked nominal proof certificate identified upstream as g_hwnisolnkereqndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLnpwhnordvalndv (A : SemanticCore.Class) (hyp_lnpwhnordvalndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synClnpwquofn (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synChwniso A) (Compiler.CompactSourceSyntax.synChwcn A)))) (Compiler.CompactSourceSyntax.synChnord A))

Checked nominal proof certificate identified upstream as g_lnpwhnordvalndv.

Equations

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

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

Checked nominal proof certificate identified upstream as g_wpplitphnordpointfnexndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWpplitphnordpointfnfnndv : Nominal.NPrf (Compiler.CompactSourceSyntax.synWfn Compiler.CompactSourceSyntax.synCwpplitphnordpointfn (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synCvv))

Checked nominal proof certificate identified upstream as g_wpplitphnordpointfnfnndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWpplitphnordpointfnvalndv (A : SemanticCore.Class) (hyp_wpplitphnordpointfnvalndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synCwpplitphnordpointfn (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCsn A))) (Compiler.CompactSourceSyntax.synChnord A))

Checked nominal proof certificate identified upstream as g_wpplitphnordpointfnvalndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHncardnceqsetimpndv (D E : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem D Compiler.CompactSourceSyntax.synCvv).imp ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCnc D) (Compiler.CompactSourceSyntax.synCnc E)).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synChncard D) (Compiler.CompactSourceSyntax.synChncard E))))

Checked nominal proof certificate identified upstream as g_hncardnceqsetimpndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnordncmemimpndv (A B : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem B (Compiler.CompactSourceSyntax.synCnc A)).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synChnord B) (Compiler.CompactSourceSyntax.synCnc (Compiler.CompactSourceSyntax.synChnord A))))

Checked nominal proof certificate identified upstream as g_hnordncmemimpndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEnimasatndv (A Q : SemanticCore.Class) (hyp_enimasatndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Q)) (hyp_enimasatndv_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss Q (Compiler.CompactSourceSyntax.synCnc A))) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCima Compiler.CompactSourceSyntax.synCen Q) (Compiler.CompactSourceSyntax.synCnc A))

Checked nominal proof certificate identified upstream as g_enimasatndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWpplitphnordpointfnvalimpndv (q : SemanticCore.Var) : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv q) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synCvv))).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synCwpplitphnordpointfn (SemanticCore.Class.cv q)) (Compiler.CompactSourceSyntax.synChnord (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv q))))))

Checked nominal proof certificate identified upstream as g_wpplitphnordpointfnvalimpndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWpplitphnordimexndv (Q : SemanticCore.Class) (hyp_wpplitphnordimexndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem Q Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCima Compiler.CompactSourceSyntax.synCwpplitphnordpointfn (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 Q))) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_wpplitphnordimexndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWpplitphnordimcanndv (C Q : SemanticCore.Class) (_hyp_wpplitphnordimcanndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem Q Compiler.CompactSourceSyntax.synCvv)) (hyp_wpplitphnordimcanndv_2 : Nominal.NPrf (SemanticCore.Wff.classMem C Q)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synChnord C) (Compiler.CompactSourceSyntax.synCima Compiler.CompactSourceSyntax.synCwpplitphnordpointfn (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 Q))))

Checked nominal proof certificate identified upstream as g_wpplitphnordimcanndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWpplitphnordimssndv (C Q : SemanticCore.Class) (_hyp_wpplitphnordimssndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem Q Compiler.CompactSourceSyntax.synCvv)) (hyp_wpplitphnordimssndv_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss Q (Compiler.CompactSourceSyntax.synCnc C))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCima Compiler.CompactSourceSyntax.synCwpplitphnordpointfn (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 Q))) (Compiler.CompactSourceSyntax.synCnc (Compiler.CompactSourceSyntax.synChnord C)))

Checked nominal proof certificate identified upstream as g_wpplitphnordimssndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWpplitphnordcardvalndv (C Q : SemanticCore.Class) (hyp_wpplitphnordcardvalndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem Q Compiler.CompactSourceSyntax.synCvv)) (hyp_wpplitphnordcardvalndv_2 : Nominal.NPrf (SemanticCore.Wff.classMem C Q)) (hyp_wpplitphnordcardvalndv_3 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss Q (Compiler.CompactSourceSyntax.synCnc C))) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCimage Compiler.CompactSourceSyntax.synCen) (Compiler.CompactSourceSyntax.synCima Compiler.CompactSourceSyntax.synCwpplitphnordpointfn (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 Q)))) (Compiler.CompactSourceSyntax.synChncard C))

Checked nominal proof certificate identified upstream as g_wpplitphnordcardvalndv.

Equations

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

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

Checked nominal proof certificate identified upstream as g_wpppowset2fnexndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWpppowset2fnfnndv : Nominal.NPrf (Compiler.CompactSourceSyntax.synWfn Compiler.CompactSourceSyntax.synCwpppowset2fn (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synCvv))

Checked nominal proof certificate identified upstream as g_wpppowset2fnfnndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWpppowset2fnvalndv (A : SemanticCore.Class) (hyp_wpppowset2fnvalndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synCwpppowset2fn (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCsn A))) (Compiler.CompactSourceSyntax.synCpw (Compiler.CompactSourceSyntax.synCpw A)))

Checked nominal proof certificate identified upstream as g_wpppowset2fnvalndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWpppowset2fnvalimpndv (q : SemanticCore.Var) : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv q) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synCvv))).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synCwpppowset2fn (SemanticCore.Class.cv q)) (Compiler.CompactSourceSyntax.synCpw (Compiler.CompactSourceSyntax.synCpw (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv q)))))))

Checked nominal proof certificate identified upstream as g_wpppowset2fnvalimpndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWpppowset2imexndv (Q : SemanticCore.Class) (hyp_wpppowset2imexndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem Q Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCima Compiler.CompactSourceSyntax.synCwpppowset2fn (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 Q))) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_wpppowset2imexndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWpppowset2imcanndv (C Q : SemanticCore.Class) (_hyp_wpppowset2imcanndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem Q Compiler.CompactSourceSyntax.synCvv)) (hyp_wpppowset2imcanndv_2 : Nominal.NPrf (SemanticCore.Wff.classMem C Q)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCpw (Compiler.CompactSourceSyntax.synCpw C)) (Compiler.CompactSourceSyntax.synCima Compiler.CompactSourceSyntax.synCwpppowset2fn (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 Q))))

Checked nominal proof certificate identified upstream as g_wpppowset2imcanndv.

Equations

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

Certificates from NominalWPPReplayChunk016Compact001Part060.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWpppowset2imssndv (C Q : SemanticCore.Class) (_hyp_wpppowset2imssndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem Q Compiler.CompactSourceSyntax.synCvv)) (hyp_wpppowset2imssndv_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss Q (Compiler.CompactSourceSyntax.synCnc C))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCima Compiler.CompactSourceSyntax.synCwpppowset2fn (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 Q))) (Compiler.CompactSourceSyntax.synCnc (Compiler.CompactSourceSyntax.synCpw (Compiler.CompactSourceSyntax.synCpw C))))

Checked nominal proof certificate identified upstream as g_wpppowset2imssndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSif1mapndv (A B F : SemanticCore.Class) (hyp_sif1mapndv_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWf1 F A B)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWf1 (Compiler.CompactSourceSyntax.synCsi F) (Compiler.CompactSourceSyntax.synCpw1 A) (Compiler.CompactSourceSyntax.synCpw1 B))

Checked nominal proof certificate identified upstream as g_sif1mapndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppcardt2fnf1ndv : Nominal.NPrf (Compiler.CompactSourceSyntax.synWf1 Compiler.CompactSourceSyntax.synCwppcardt2fn (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synCncs)) Compiler.CompactSourceSyntax.synCncs)

Checked nominal proof certificate identified upstream as g_wppcardt2fnf1ndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppcardt4fnf1ndv : Nominal.NPrf (Compiler.CompactSourceSyntax.synWf1 Compiler.CompactSourceSyntax.synCwppcardt4fn (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synCncs)))) Compiler.CompactSourceSyntax.synCncs)

Checked nominal proof certificate identified upstream as g_wppcardt4fnf1ndv.

Equations

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

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

Checked nominal proof certificate identified upstream as g_wppfamilyrep2fnexndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppfamilyrep2fnfnndv : Nominal.NPrf (Compiler.CompactSourceSyntax.synWfn Compiler.CompactSourceSyntax.synCwppfamilyrep2fn Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_wppfamilyrep2fnfnndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppfamilyrep2fnvalndv (Q : SemanticCore.Class) (hyp_wppfamilyrep2fnvalndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem Q Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synCwppfamilyrep2fn (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCsn Q))) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 Q)))

Checked nominal proof certificate identified upstream as g_wppfamilyrep2fnvalndv.

Equations

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

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

Checked nominal proof certificate identified upstream as g_wppdirecte2famfnexndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppdirecte2famfnfnndv : Nominal.NPrf (Compiler.CompactSourceSyntax.synWfn Compiler.CompactSourceSyntax.synCwppdirecte2famfn Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_wppdirecte2famfnfnndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppdirecte2famfnvalndv (Q : SemanticCore.Class) (hyp_wppdirecte2famfnvalndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem Q Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synCwppdirecte2famfn (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCsn Q))) (Compiler.CompactSourceSyntax.synCima Compiler.CompactSourceSyntax.synCwpppowset2fn (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 Q))))

Checked nominal proof certificate identified upstream as g_wppdirecte2famfnvalndv.

Equations

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

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

Checked nominal proof certificate identified upstream as g_wppdirecth1famfnexndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppdirecth1famfnfnndv : Nominal.NPrf (Compiler.CompactSourceSyntax.synWfn Compiler.CompactSourceSyntax.synCwppdirecth1famfn (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synCvv)))

Checked nominal proof certificate identified upstream as g_wppdirecth1famfnfnndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppdirecth1famfnvalndv (Q : SemanticCore.Class) (hyp_wppdirecth1famfnvalndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem Q Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synCwppdirecth1famfn (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCsn Q))) (Compiler.CompactSourceSyntax.synCima Compiler.CompactSourceSyntax.synCwpplitphnordpointfn (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synCwppdirecte2famfn Q)))))

Checked nominal proof certificate identified upstream as g_wppdirecth1famfnvalndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppdirecth2famfnvalndv (Q : SemanticCore.Class) (hyp_wppdirecth2famfnvalndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem Q (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synCvv)))) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synCwppdirecth2famfn (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCsn Q))) (Compiler.CompactSourceSyntax.synCima Compiler.CompactSourceSyntax.synCwpplitphnordpointfn (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synCwppdirecth1famfn Q)))))

Checked nominal proof certificate identified upstream as g_wppdirecth2famfnvalndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppconcrete6codefnvalndv (X : SemanticCore.Class) (hyp_wppconcrete6codefnvalndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem X Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synCwppconcrete6codefn (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCnc X)))))))) (Compiler.CompactSourceSyntax.synChncard (Compiler.CompactSourceSyntax.synChnord (Compiler.CompactSourceSyntax.synCpw (Compiler.CompactSourceSyntax.synCpw X)))))

Checked nominal proof certificate identified upstream as g_wppconcrete6codefnvalndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppcardt6fnmapndv : Nominal.NPrf (Compiler.CompactSourceSyntax.synWf Compiler.CompactSourceSyntax.synCwppcardt6fn (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synCncs)))))) Compiler.CompactSourceSyntax.synCncs)

Checked nominal proof certificate identified upstream as g_wppcardt6fnmapndv.

Equations

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