Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk013Compact001Part034.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEnpw1lem1 (x y g : SemanticCore.Var) (dv_g_x : g ≠ x) (dv_g_y : g ≠ y) (dv_x_y : x ≠ y) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopab x y (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)) (SemanticCore.Class.cv g) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv y)))) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_enpw1lem1.

Equations

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

Certificates from NominalWPPReplayChunk013Compact001Part035.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEnpw1 (A B : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr A Compiler.CompactSourceSyntax.synCen B) (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCpw1 A) Compiler.CompactSourceSyntax.synCen (Compiler.CompactSourceSyntax.synCpw1 B)))

Checked nominal proof certificate identified upstream as g_enpw1.

Equations

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

Certificates from NominalWPPReplayChunk013Compact001Part036.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEnmap2lem1 (A G W : SemanticCore.Class) (s r : SemanticCore.Var) (dv_A_s : s ∉ A.fv) (dv_G_s : s ∉ G.fv) (dv_r_s : r ≠ s) (hyp_enmap2lem1_1 : Nominal.NPrf (SemanticCore.Wff.classEq W (Compiler.CompactSourceSyntax.synCmpt s (Compiler.CompactSourceSyntax.synCo G Compiler.CompactSourceSyntax.synCmap A) (Compiler.CompactSourceSyntax.synCcom (SemanticCore.Class.cv s) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv r)))))) : Nominal.NPrf (SemanticCore.Wff.classMem W Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_enmap2lem1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEnmap2lem2 (G W : SemanticCore.Class) (s r a : SemanticCore.Var) (dv_G_s : s ∉ G.fv) (dv_a_s : a ≠ s) (hyp_enmap2lem2_1 : Nominal.NPrf (SemanticCore.Wff.classEq W (Compiler.CompactSourceSyntax.synCmpt s (Compiler.CompactSourceSyntax.synCo G Compiler.CompactSourceSyntax.synCmap (SemanticCore.Class.cv a)) (Compiler.CompactSourceSyntax.synCcom (SemanticCore.Class.cv s) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv r)))))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWfn W (Compiler.CompactSourceSyntax.synCo G Compiler.CompactSourceSyntax.synCmap (SemanticCore.Class.cv a)))

Checked nominal proof certificate identified upstream as g_enmap2lem2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEnmap2lem3 (S T G W : SemanticCore.Class) (s r a b : SemanticCore.Var) (dv_G_s : s ∉ G.fv) (dv_S_s : s ∉ S.fv) (dv_a_s : a ≠ s) (dv_r_s : r ≠ s) (hyp_enmap2lem3_1 : Nominal.NPrf (SemanticCore.Wff.classEq W (Compiler.CompactSourceSyntax.synCmpt s (Compiler.CompactSourceSyntax.synCo G Compiler.CompactSourceSyntax.synCmap (SemanticCore.Class.cv a)) (Compiler.CompactSourceSyntax.synCcom (SemanticCore.Class.cv s) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv r)))))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWf1o (SemanticCore.Class.cv r) (SemanticCore.Class.cv a) (SemanticCore.Class.cv b)).imp ((Compiler.CompactSourceSyntax.synWbr S W T).imp (SemanticCore.Wff.classEq S (Compiler.CompactSourceSyntax.synCcom T (SemanticCore.Class.cv r)))))

Checked nominal proof certificate identified upstream as g_enmap2lem3.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEnmap2lem4 (G W : SemanticCore.Class) (s r a b : SemanticCore.Var) (dv_G_s : s ∉ G.fv) (dv_a_s : a ≠ s) (dv_r_s : r ≠ s) (hyp_enmap2lem4_1 : Nominal.NPrf (SemanticCore.Wff.classEq W (Compiler.CompactSourceSyntax.synCmpt s (Compiler.CompactSourceSyntax.synCo G Compiler.CompactSourceSyntax.synCmap (SemanticCore.Class.cv a)) (Compiler.CompactSourceSyntax.synCcom (SemanticCore.Class.cv s) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv r)))))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWf1o (SemanticCore.Class.cv r) (SemanticCore.Class.cv a) (SemanticCore.Class.cv b)).imp (Compiler.CompactSourceSyntax.synWfun (Compiler.CompactSourceSyntax.synCcnv W)))

Checked nominal proof certificate identified upstream as g_enmap2lem4.

Equations

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

Certificates from NominalWPPReplayChunk013Compact001Part037.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEnmap2lem5 (G W : SemanticCore.Class) (s r a b : SemanticCore.Var) (dv_G_s : s ∉ G.fv) (dv_a_s : a ≠ s) (dv_r_s : r ≠ s) (hyp_enmap2lem5_1 : Nominal.NPrf (SemanticCore.Wff.classEq W (Compiler.CompactSourceSyntax.synCmpt s (Compiler.CompactSourceSyntax.synCo G Compiler.CompactSourceSyntax.synCmap (SemanticCore.Class.cv a)) (Compiler.CompactSourceSyntax.synCcom (SemanticCore.Class.cv s) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv r)))))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWf1o (SemanticCore.Class.cv r) (SemanticCore.Class.cv a) (SemanticCore.Class.cv b)).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCrn W) (Compiler.CompactSourceSyntax.synCo G Compiler.CompactSourceSyntax.synCmap (SemanticCore.Class.cv b))))

Checked nominal proof certificate identified upstream as g_enmap2lem5.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEnmap2 (A B C : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWbr A Compiler.CompactSourceSyntax.synCen B).imp (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCo C Compiler.CompactSourceSyntax.synCmap A) Compiler.CompactSourceSyntax.synCen (Compiler.CompactSourceSyntax.synCo C Compiler.CompactSourceSyntax.synCmap B)))

Checked nominal proof certificate identified upstream as g_enmap2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEnpw1pw (A : SemanticCore.Class) (hyp_enpw1pw_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw A)) Compiler.CompactSourceSyntax.synCen (Compiler.CompactSourceSyntax.synCpw (Compiler.CompactSourceSyntax.synCpw1 A)))

Checked nominal proof certificate identified upstream as g_enpw1pw.

Equations

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

Certificates from NominalWPPReplayChunk013Compact001Part038.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEnprmaplem1 (x : SemanticCore.Var) (A B W : SemanticCore.Class) (r : SemanticCore.Var) (dv_A_r : r ∉ A.fv) (dv_B_r : r ∉ B.fv) (dv_r_x : r ≠ x) (hyp_enprmaplem1_1 : Nominal.NPrf (SemanticCore.Wff.classEq W (Compiler.CompactSourceSyntax.synCmpt r (Compiler.CompactSourceSyntax.synCo A Compiler.CompactSourceSyntax.synCmap B) (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv r)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)))))) : Nominal.NPrf (SemanticCore.Wff.classMem W Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_enprmaplem1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEnprmaplem2 (x : SemanticCore.Var) (A B W : SemanticCore.Class) (r : SemanticCore.Var) (dv_A_r : r ∉ A.fv) (dv_B_r : r ∉ B.fv) (hyp_enprmaplem2_1 : Nominal.NPrf (SemanticCore.Wff.classEq W (Compiler.CompactSourceSyntax.synCmpt r (Compiler.CompactSourceSyntax.synCo A Compiler.CompactSourceSyntax.synCmap B) (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv r)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)))))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWfn W (Compiler.CompactSourceSyntax.synCo A Compiler.CompactSourceSyntax.synCmap B))

Checked nominal proof certificate identified upstream as g_enprmaplem2.

Equations

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