Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk016Compact001Part051.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPwpullwesetimpndv (x y f r : SemanticCore.Var) (_dv_f_r : f ≠ r) (_dv_f_x : f ≠ x) (_dv_f_y : f ≠ y) (_dv_r_x : r ≠ x) (_dv_r_y : r ≠ y) (_dv_x_y : x ≠ y) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWf1o (SemanticCore.Class.cv f) (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCwe (SemanticCore.Class.cv y))).imp (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCpwpull (SemanticCore.Class.cv f) (SemanticCore.Class.cv r)) Compiler.CompactSourceSyntax.synCwe (SemanticCore.Class.cv x)))

Checked nominal proof certificate identified upstream as g_pwpullwesetimpndv.

Equations

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

Certificates from NominalWPPReplayChunk016Compact001Part052.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPwpullssxpsetimpndv (x y f r : SemanticCore.Var) (_dv_f_r : f ≠ r) (_dv_f_x : f ≠ x) (_dv_f_y : f ≠ y) (_dv_r_x : r ≠ x) (_dv_r_y : r ≠ y) (_dv_x_y : x ≠ y) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWfo (SemanticCore.Class.cv f) (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)).imp (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCpwpull (SemanticCore.Class.cv f) (SemanticCore.Class.cv r)) (Compiler.CompactSourceSyntax.synCxp (SemanticCore.Class.cv x) (SemanticCore.Class.cv x))))

Checked nominal proof certificate identified upstream as g_pwpullssxpsetimpndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElhwcodesclndv (B C D : SemanticCore.Class) (hyp_elhwcodesclndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) (hyp_elhwcodesclndv_2 : Nominal.NPrf (SemanticCore.Wff.classMem C Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop B C) (Compiler.CompactSourceSyntax.synChwcodes D)) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr B Compiler.CompactSourceSyntax.synCwe C) (Compiler.CompactSourceSyntax.synWss C D)))

Checked nominal proof certificate identified upstream as g_elhwcodesclndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHwbijf1oclndv (B : SemanticCore.Class) (hyp_hwbijf1oclndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synChwbij) (Compiler.CompactSourceSyntax.synWf1o B (Compiler.CompactSourceSyntax.synCdm B) (Compiler.CompactSourceSyntax.synCrn B)))

Checked nominal proof certificate identified upstream as g_hwbijf1oclndv.

Equations

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

Certificates from NominalWPPReplayChunk016Compact001Part053.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHncodetrncndndv (u : SemanticCore.Var) (D E F : SemanticCore.Class) (hyp_hncodetrncndndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCvv)) (hyp_hncodetrncndndv_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWf1o F D E)) : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn D)).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChncodetrnfn F) (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synChwcn E)))

Checked nominal proof certificate identified upstream as g_hncodetrncndndv.

Equations

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

Certificates from NominalWPPReplayChunk016Compact001Part054.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnqinctrnvaldndv (u : SemanticCore.Var) (A D E F : SemanticCore.Class) (hyp_hnqinctrnvaldndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCvv)) (hyp_hnqinctrnvaldndv_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWf1o F D E)) (hyp_hnqinctrnvaldndv_3 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss D A)) (hyp_hnqinctrnvaldndv_4 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss E A)) (hyp_hnqinctrnvaldndv_5 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn D)).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqinc D A) (Compiler.CompactSourceSyntax.synCec (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwniso D))) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqinc E A) (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChncodetrnfn F) (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synChwniso E)))))

Checked nominal proof certificate identified upstream as g_hnqinctrnvaldndv.

Equations

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

Certificates from NominalWPPReplayChunk016Compact001Part055.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnqinctrnrnssndv (A D E F : SemanticCore.Class) (hyp_hnqinctrnrnssndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCvv)) (hyp_hnqinctrnrnssndv_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWf1o F D E)) (hyp_hnqinctrnrnssndv_3 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss D A)) (hyp_hnqinctrnrnssndv_4 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss E A)) (hyp_hnqinctrnrnssndv_5 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn (Compiler.CompactSourceSyntax.synChnqinc D A)) (Compiler.CompactSourceSyntax.synCrn (Compiler.CompactSourceSyntax.synChnqinc E A)))

Checked nominal proof certificate identified upstream as g_hnqinctrnrnssndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnqinctrnrneqndv (A D E F : SemanticCore.Class) (hyp_hnqinctrnrneqndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCvv)) (hyp_hnqinctrnrneqndv_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWf1o F D E)) (hyp_hnqinctrnrneqndv_3 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss D A)) (hyp_hnqinctrnrneqndv_4 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss E A)) (hyp_hnqinctrnrneqndv_5 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCrn (Compiler.CompactSourceSyntax.synChnqinc D A)) (Compiler.CompactSourceSyntax.synCrn (Compiler.CompactSourceSyntax.synChnqinc E A)))

Checked nominal proof certificate identified upstream as g_hnqinctrnrneqndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnordf1oenambndv (A D E F : SemanticCore.Class) (hyp_hnordf1oenambndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCvv)) (hyp_hnordf1oenambndv_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWf1o F D E)) (hyp_hnordf1oenambndv_3 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss D A)) (hyp_hnordf1oenambndv_4 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss E A)) (hyp_hnordf1oenambndv_5 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synChnord D) Compiler.CompactSourceSyntax.synCen (Compiler.CompactSourceSyntax.synChnord E))

Checked nominal proof certificate identified upstream as g_hnordf1oenambndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHncardf1oeqambndv (A D E F : SemanticCore.Class) (hyp_hncardf1oeqambndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCvv)) (hyp_hncardf1oeqambndv_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWf1o F D E)) (hyp_hncardf1oeqambndv_3 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss D A)) (hyp_hncardf1oeqambndv_4 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss E A)) (hyp_hncardf1oeqambndv_5 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synChncard D) (Compiler.CompactSourceSyntax.synChncard E))

Checked nominal proof certificate identified upstream as g_hncardf1oeqambndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHncardf1oeqndv (D E F : SemanticCore.Class) (hyp_hncardf1oeqndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCvv)) (hyp_hncardf1oeqndv_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWf1o F D E)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synChncard D) (Compiler.CompactSourceSyntax.synChncard E))

Checked nominal proof certificate identified upstream as g_hncardf1oeqndv.

Equations

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

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

Checked nominal proof certificate identified upstream as g_hnordeqdndv.

Equations

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

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

Checked nominal proof certificate identified upstream as g_hncardeqdndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHncardf1oimpndv (D E F : SemanticCore.Class) (hyp_hncardf1oimpndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWf1o F D E).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synChncard D) (Compiler.CompactSourceSyntax.synChncard E)))

Checked nominal proof certificate identified upstream as g_hncardf1oimpndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHncardnceqdndv (D E : SemanticCore.Class) (hyp_hncardnceqdndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem D Compiler.CompactSourceSyntax.synCvv)) (_hyp_hncardnceqdndv_2 : Nominal.NPrf (SemanticCore.Wff.classMem E Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((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_hncardnceqdndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHncardnceqndv (D E : SemanticCore.Class) (hyp_hncardnceqndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem D Compiler.CompactSourceSyntax.synCvv)) (hyp_hncardnceqndv_2 : Nominal.NPrf (SemanticCore.Wff.classMem E Compiler.CompactSourceSyntax.synCvv)) (hyp_hncardnceqndv_3 : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCnc D) (Compiler.CompactSourceSyntax.synCnc E))) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synChncard D) (Compiler.CompactSourceSyntax.synChncard E))

Checked nominal proof certificate identified upstream as g_hncardnceqndv.

Equations

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

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

Checked nominal proof certificate identified upstream as g_wppcardt4fnexndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppcardt4fnmapndv : Nominal.NPrf (Compiler.CompactSourceSyntax.synWf 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_wppcardt4fnmapndv.

Equations

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