Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk016Compact001Part061.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppcardt6fnvalsingndv (D : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem D Compiler.CompactSourceSyntax.synCncs).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synCwppcardt6fn (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCsn (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 (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc D))))))))

Checked nominal proof certificate identified upstream as g_wppcardt6fnvalsingndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppconcrete6fnfnndv : Nominal.NPrf (Compiler.CompactSourceSyntax.synWfn Compiler.CompactSourceSyntax.synCwppconcrete6fn (Compiler.CompactSourceSyntax.synCrn Compiler.CompactSourceSyntax.synCwppcardt6fn))

Checked nominal proof certificate identified upstream as g_wppconcrete6fnfnndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppconcrete6fndmndv : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCdm Compiler.CompactSourceSyntax.synCwppconcrete6fn) (Compiler.CompactSourceSyntax.synCrn Compiler.CompactSourceSyntax.synCwppcardt6fn))

Checked nominal proof certificate identified upstream as g_wppconcrete6fndmndv.

Equations

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

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

Checked nominal proof certificate identified upstream as g_wppconcrete6fnfunsndv.

Equations

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

Certificates from NominalWPPReplayChunk016Compact001Part062.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppconcrete6fnvalndv (X : SemanticCore.Class) (hyp_wppconcrete6fnvalndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem X Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synCwppconcrete6fn (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (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_wppconcrete6fnvalndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLetc2w6ndv (M N : SemanticCore.Class) (p : SemanticCore.Var) (dv_M_p : p ∉ M.fv) (dv_N_p : p ∉ N.fv) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classMem M Compiler.CompactSourceSyntax.synCncs) (SemanticCore.Wff.classMem N Compiler.CompactSourceSyntax.synCncs) (Compiler.CompactSourceSyntax.synWbr M Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc N)))).imp (Compiler.CompactSourceSyntax.synWrex p Compiler.CompactSourceSyntax.synCncs (SemanticCore.Wff.classEq M (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (SemanticCore.Class.cv p))))))

Checked nominal proof certificate identified upstream as g_letc2w6ndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLetc3w6ndv (M N : SemanticCore.Class) (p : SemanticCore.Var) (dv_M_p : p ∉ M.fv) (dv_N_p : p ∉ N.fv) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classMem M Compiler.CompactSourceSyntax.synCncs) (SemanticCore.Wff.classMem N Compiler.CompactSourceSyntax.synCncs) (Compiler.CompactSourceSyntax.synWbr M Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc N))))).imp (Compiler.CompactSourceSyntax.synWrex p Compiler.CompactSourceSyntax.synCncs (SemanticCore.Wff.classEq M (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (SemanticCore.Class.cv p)))))))

Checked nominal proof certificate identified upstream as g_letc3w6ndv.

Equations

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

Certificates from NominalWPPReplayChunk016Compact001Part063.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLetc4w6ndv (M N : SemanticCore.Class) (p : SemanticCore.Var) (dv_M_p : p ∉ M.fv) (dv_N_p : p ∉ N.fv) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classMem M Compiler.CompactSourceSyntax.synCncs) (SemanticCore.Wff.classMem N Compiler.CompactSourceSyntax.synCncs) (Compiler.CompactSourceSyntax.synWbr M Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc N)))))).imp (Compiler.CompactSourceSyntax.synWrex p Compiler.CompactSourceSyntax.synCncs (SemanticCore.Wff.classEq M (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (SemanticCore.Class.cv p))))))))

Checked nominal proof certificate identified upstream as g_letc4w6ndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLetc5w6ndv (M N : SemanticCore.Class) (p : SemanticCore.Var) (dv_M_p : p ∉ M.fv) (dv_N_p : p ∉ N.fv) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classMem M Compiler.CompactSourceSyntax.synCncs) (SemanticCore.Wff.classMem N Compiler.CompactSourceSyntax.synCncs) (Compiler.CompactSourceSyntax.synWbr M Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc N))))))).imp (Compiler.CompactSourceSyntax.synWrex p Compiler.CompactSourceSyntax.synCncs (SemanticCore.Wff.classEq M (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (SemanticCore.Class.cv p)))))))))

Checked nominal proof certificate identified upstream as g_letc5w6ndv.

Equations

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

Certificates from NominalWPPReplayChunk016Compact001Part064.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLetc6w6ndv (M N : SemanticCore.Class) (p : SemanticCore.Var) (dv_M_p : p ∉ M.fv) (dv_N_p : p ∉ N.fv) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classMem M Compiler.CompactSourceSyntax.synCncs) (SemanticCore.Wff.classMem N Compiler.CompactSourceSyntax.synCncs) (Compiler.CompactSourceSyntax.synWbr M Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc N)))))))).imp (Compiler.CompactSourceSyntax.synWrex p Compiler.CompactSourceSyntax.synCncs (SemanticCore.Wff.classEq M (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (SemanticCore.Class.cv p))))))))))

Checked nominal proof certificate identified upstream as g_letc6w6ndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppconcrete6dmcovndv (D : SemanticCore.Class) (p : SemanticCore.Var) (_dv_D_p : p ∉ D.fv) (hyp_wppconcrete6dmcovndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem D Compiler.CompactSourceSyntax.synCncs)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWral p (Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv) ((Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv p) Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc D))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv p) (Compiler.CompactSourceSyntax.synCdm Compiler.CompactSourceSyntax.synCwppconcrete6fn))))

Checked nominal proof certificate identified upstream as g_wppconcrete6dmcovndv.

Equations

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

Certificates from NominalWPPReplayChunk016Compact001Part065.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppconcrete6dmpaircovndv (D : SemanticCore.Class) (p : SemanticCore.Var) (_dv_D_p : p ∉ D.fv) (hyp_wppconcrete6dmpaircovndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem D Compiler.CompactSourceSyntax.synCncs)) (hyp_wppconcrete6dmpaircovndv_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc D))))))) Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc D)))))))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWral p (Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv) ((Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv p) Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc D))))))).imp (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv p) (Compiler.CompactSourceSyntax.synCdm Compiler.CompactSourceSyntax.synCwppconcrete6fn)) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCtc (SemanticCore.Class.cv p)) (Compiler.CompactSourceSyntax.synCdm Compiler.CompactSourceSyntax.synCwppconcrete6fn)))))

Checked nominal proof certificate identified upstream as g_wppconcrete6dmpaircovndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHncardnc1ndv : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synChncard Compiler.CompactSourceSyntax.synC1c) Compiler.CompactSourceSyntax.synCncs)

Checked nominal proof certificate identified upstream as g_hncardnc1ndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppconcrete6hncard1dmcovndv (p : SemanticCore.Var) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWral p (Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv) ((Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv p) Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synChncard Compiler.CompactSourceSyntax.synC1c)))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv p) (Compiler.CompactSourceSyntax.synCdm Compiler.CompactSourceSyntax.synCwppconcrete6fn))))

Checked nominal proof certificate identified upstream as g_wppconcrete6hncard1dmcovndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppconcrete6hncard1dmpaircovndv (p : SemanticCore.Var) (hyp_wppconcrete6hncard1dmpaircovndv_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synChncard Compiler.CompactSourceSyntax.synC1c)))))))) Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synChncard Compiler.CompactSourceSyntax.synC1c))))))))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWral p (Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv) ((Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv p) Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synChncard Compiler.CompactSourceSyntax.synC1c)))))))).imp (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv p) (Compiler.CompactSourceSyntax.synCdm Compiler.CompactSourceSyntax.synCwppconcrete6fn)) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCtc (SemanticCore.Class.cv p)) (Compiler.CompactSourceSyntax.synCdm Compiler.CompactSourceSyntax.synCwppconcrete6fn)))))

Checked nominal proof certificate identified upstream as g_wppconcrete6hncard1dmpaircovndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHncardtcshiftcondndv (A : SemanticCore.Class) (hyp_hncardtcshiftcondndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_hncardtcshiftcondndv_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChnord A)) Compiler.CompactSourceSyntax.synCen (Compiler.CompactSourceSyntax.synChnord (Compiler.CompactSourceSyntax.synCpw1 A)))) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synChncard A)) (Compiler.CompactSourceSyntax.synChncard (Compiler.CompactSourceSyntax.synCpw1 A)))

Checked nominal proof certificate identified upstream as g_hncardtcshiftcondndv.

Equations

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

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

Checked nominal proof certificate identified upstream as g_hnsicodeliftfnexndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnsicodeliftfnfnndv : Nominal.NPrf (Compiler.CompactSourceSyntax.synWfn Compiler.CompactSourceSyntax.synChnsicodeliftfn Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_hnsicodeliftfnfnndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSisuppdndv (ph : SemanticCore.Wff) (D R : SemanticCore.Class) (hyp_sisuppdndv_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWss R (Compiler.CompactSourceSyntax.synCxp D D)))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCsi R) (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCpw1 D) (Compiler.CompactSourceSyntax.synCpw1 D))))

Checked nominal proof certificate identified upstream as g_sisuppdndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnsicodeliftcodeclndv (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 (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCsi (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv u))) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))) (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCpw1 A))))

Checked nominal proof certificate identified upstream as g_hnsicodeliftcodeclndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnsicodeliftfnvalgndv (D R : SemanticCore.Class) (hyp_hnsicodeliftfnvalgndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) (hyp_hnsicodeliftfnvalgndv_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.synChnsicodeliftfn (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCop R D))) (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCsi R) (Compiler.CompactSourceSyntax.synCpw1 D))))

Checked nominal proof certificate identified upstream as g_hnsicodeliftfnvalgndv.

Equations

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