Nominal proof certificates grouped in dependency order.

Certificates from NAR4C076C001Part008.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb076SplitAlpha0002 (g m n a b : SemanticCore.Var) (dv_m_n : m ≠ n) : Nominal.TAlphaWff [(nb076AlphaDummy015, nb076AlphaDummy016 g m n a b), (nb076AlphaDummy013, nb076AlphaDummy014 g m n a b), (nb076AlphaDummy005, nb076AlphaDummy006 g m n a b), (nb076AlphaDummy004, n), (nb076AlphaDummy003, m), (nb076AlphaDummy007, nb076AlphaDummy008 g m n a b)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb076AlphaDummy015) (SemanticCore.Class.cab nb076AlphaDummy009 (Compiler.CompactSourceSyntax.synWrex nb076AlphaDummy010 (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv nb076AlphaDummy003) (SemanticCore.Class.cv nb076AlphaDummy004)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb076AlphaDummy009) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb076AlphaDummy010)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb076AlphaDummy015) (SemanticCore.Class.cab nb076AlphaDummy009 (Compiler.CompactSourceSyntax.synWrex nb076AlphaDummy010 (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv nb076AlphaDummy003) (SemanticCore.Class.cv nb076AlphaDummy004)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb076AlphaDummy009) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb076AlphaDummy010)))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb076AlphaDummy016 g m n a b)) (SemanticCore.Class.cab (nb076AlphaDummy011 g m n a b) (Compiler.CompactSourceSyntax.synWrex (nb076AlphaDummy012 g m n a b) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv m) (SemanticCore.Class.cv n)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb076AlphaDummy011 g m n a b)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb076AlphaDummy012 g m n a b))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb076AlphaDummy016 g m n a b)) (SemanticCore.Class.cab (nb076AlphaDummy011 g m n a b) (Compiler.CompactSourceSyntax.synWrex (nb076AlphaDummy012 g m n a b) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv m) (SemanticCore.Class.cv n)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb076AlphaDummy011 g m n a b)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb076AlphaDummy012 g m n a b))))))).neg)

Checked nominal proof certificate identified upstream as nb076_split_alpha_0002.

Equations

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

Certificates from NAR4C076C001Part009.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb076SplitAlpha0003 (g m n a b : SemanticCore.Var) : Nominal.TAlphaWff [(nb076AlphaDummy010, nb076AlphaDummy012 g m n a b), (nb076AlphaDummy009, nb076AlphaDummy011 g m n a b), (nb076AlphaDummy075, nb076AlphaDummy076 g m n a b), (nb076AlphaDummy013, nb076AlphaDummy014 g m n a b), (nb076AlphaDummy005, nb076AlphaDummy006 g m n a b), (nb076AlphaDummy004, n), (nb076AlphaDummy003, m), (nb076AlphaDummy007, nb076AlphaDummy008 g m n a b)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb076AlphaDummy010) (SemanticCore.Class.cv nb076AlphaDummy005)).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb076AlphaDummy009) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb076AlphaDummy010)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb076AlphaDummy012 g m n a b)) (SemanticCore.Class.cv (nb076AlphaDummy006 g m n a b))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb076AlphaDummy011 g m n a b)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb076AlphaDummy012 g m n a b))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))).neg)

Checked nominal proof certificate identified upstream as nb076_split_alpha_0003.

Equations

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb076_wpp_notmem_0198 : nb076AlphaDummy005 ∉ Compiler.CompactSourceSyntax.synCncs.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb076_wpp_notmem_0199 (g m n a b : SemanticCore.Var) : nb076AlphaDummy006 g m n a b ∉ Compiler.CompactSourceSyntax.synCncs.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb076_wpp_notmem_0200 : nb076AlphaDummy004 ∉ Compiler.CompactSourceSyntax.synCncs.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb076_wpp_notmem_0201 (n : SemanticCore.Var) : n ∉ Compiler.CompactSourceSyntax.synCncs.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb076_wpp_notmem_0202 : nb076AlphaDummy003 ∉ Compiler.CompactSourceSyntax.synCncs.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb076_wpp_notmem_0203 (m : SemanticCore.Var) : m ∉ Compiler.CompactSourceSyntax.synCncs.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb076_wpp_notmem_0204 : nb076AlphaDummy007 ∉ Compiler.CompactSourceSyntax.synCncs.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb076_wpp_notmem_0205 (g m n a b : SemanticCore.Var) : nb076AlphaDummy008 g m n a b ∉ Compiler.CompactSourceSyntax.synCncs.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb076_compact_envfresh_0014 (g m n a b : SemanticCore.Var) : Nominal.TEnvFresh [(nb076AlphaDummy005, nb076AlphaDummy006 g m n a b), (nb076AlphaDummy004, n), (nb076AlphaDummy003, m), (nb076AlphaDummy007, nb076AlphaDummy008 g m n a b)] Compiler.CompactSourceSyntax.synCncs.fv

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb076WppRefl0014 (g m n a b : SemanticCore.Var) : Nominal.TReflOn [(nb076AlphaDummy005, nb076AlphaDummy006 g m n a b), (nb076AlphaDummy004, n), (nb076AlphaDummy003, m), (nb076AlphaDummy007, nb076AlphaDummy008 g m n a b)] Compiler.CompactSourceSyntax.synCncs.fv

Checked nominal proof certificate identified upstream as nb076_wpp_refl_0014.

Equations

• NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb076WppRefl0014 g m n a b = ⋯.reflOn

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb076_compact_fv_empty_0080 : nb076AlphaDummy002 ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb076_compact_fv_empty_0081 (g : SemanticCore.Var) : g ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb076_compact_fv_empty_0082 : nb076AlphaDummy001 ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb076_compact_fv_empty_0083 (b : SemanticCore.Var) : b ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb076_compact_fv_empty_0084 : nb076AlphaDummy000 ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb076_compact_fv_empty_0085 (a : SemanticCore.Var) : a ∉ ∅