Nominal proof certificates grouped in dependency order.

Certificates from AlphaSupport.NAR4C059C001Part002Stage1.

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb059_support_mem_0030 (R S_cls : SemanticCore.Class) : nb059AlphaDummy032 R S_cls ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb059AlphaDummy032 R S_cls))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb059AlphaDummy033 R S_cls))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb059_support_mem_0031 (R : SemanticCore.Class) (a : SemanticCore.Var) : nb059AlphaDummy035 R a ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb059AlphaDummy035 R a))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb059AlphaDummy036 R a))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb059_support_mem_0032 (R S_cls : SemanticCore.Class) : nb059AlphaDummy032 R S_cls ∈ (SemanticCore.Class.cv (nb059AlphaDummy032 R S_cls)).fv ∪ (SemanticCore.Class.cv (nb059AlphaDummy032 R S_cls)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb059_support_mem_0033 (R : SemanticCore.Class) (a : SemanticCore.Var) : nb059AlphaDummy035 R a ∈ (SemanticCore.Class.cv (nb059AlphaDummy035 R a)).fv ∪ (SemanticCore.Class.cv (nb059AlphaDummy035 R a)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb059_support_mem_0034 (R S_cls : SemanticCore.Class) : nb059AlphaDummy033 R S_cls ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb059AlphaDummy032 R S_cls))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb059AlphaDummy033 R S_cls))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb059_support_mem_0035 (R : SemanticCore.Class) (a : SemanticCore.Var) : nb059AlphaDummy036 R a ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb059AlphaDummy035 R a))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb059AlphaDummy036 R a))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb059_support_mem_0036 (R S_cls : SemanticCore.Class) : nb059AlphaDummy033 R S_cls ∈ (SemanticCore.Class.cv (nb059AlphaDummy033 R S_cls)).fv ∪ (SemanticCore.Class.cv (nb059AlphaDummy033 R S_cls)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb059_support_mem_0037 (R : SemanticCore.Class) (a : SemanticCore.Var) : nb059AlphaDummy036 R a ∈ (SemanticCore.Class.cv (nb059AlphaDummy036 R a)).fv ∪ (SemanticCore.Class.cv (nb059AlphaDummy036 R a)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb059_support_mem_0038 (R S_cls : SemanticCore.Class) : nb059AlphaDummy013 R S_cls ∈ (SemanticCore.Class.cv (nb059AlphaDummy014 R S_cls)).fv ∪ (SemanticCore.Class.cv (nb059AlphaDummy013 R S_cls)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb059_support_mem_0039 (R S_cls : SemanticCore.Class) : nb059AlphaDummy013 R S_cls ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb059AlphaDummy017 R S_cls) (Compiler.CompactSourceSyntax.synWrex (nb059AlphaDummy018 R S_cls) (SemanticCore.Class.cv (nb059AlphaDummy014 R S_cls)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb059AlphaDummy017 R S_cls)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb059AlphaDummy018 R S_cls))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb059AlphaDummy017 R S_cls) (Compiler.CompactSourceSyntax.synWrex (nb059AlphaDummy018 R S_cls) (SemanticCore.Class.cv (nb059AlphaDummy013 R S_cls)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb059AlphaDummy017 R S_cls)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb059AlphaDummy018 R S_cls))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb059_support_mem_0040 (R : SemanticCore.Class) (a : SemanticCore.Var) : nb059AlphaDummy015 R a ∈ (SemanticCore.Class.cv (nb059AlphaDummy016 R a)).fv ∪ (SemanticCore.Class.cv (nb059AlphaDummy015 R a)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb059_support_mem_0041 (R : SemanticCore.Class) (a : SemanticCore.Var) : nb059AlphaDummy015 R a ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb059AlphaDummy019 R a) (Compiler.CompactSourceSyntax.synWrex (nb059AlphaDummy020 R a) (SemanticCore.Class.cv (nb059AlphaDummy016 R a)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb059AlphaDummy019 R a)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb059AlphaDummy020 R a))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb059AlphaDummy019 R a) (Compiler.CompactSourceSyntax.synWrex (nb059AlphaDummy020 R a) (SemanticCore.Class.cv (nb059AlphaDummy015 R a)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb059AlphaDummy019 R a)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb059AlphaDummy020 R a))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb059_support_mem_0042 (R S_cls : SemanticCore.Class) : nb059AlphaDummy013 R S_cls ∈ (SemanticCore.Class.cab (nb059AlphaDummy017 R S_cls) (Compiler.CompactSourceSyntax.synWrex (nb059AlphaDummy018 R S_cls) (SemanticCore.Class.cv (nb059AlphaDummy013 R S_cls)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb059AlphaDummy017 R S_cls)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb059AlphaDummy018 R S_cls))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb059AlphaDummy017 R S_cls) (Compiler.CompactSourceSyntax.synWrex (nb059AlphaDummy018 R S_cls) (SemanticCore.Class.cv (nb059AlphaDummy013 R S_cls)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb059AlphaDummy017 R S_cls)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb059AlphaDummy018 R S_cls))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb059_support_mem_0043 (R : SemanticCore.Class) (a : SemanticCore.Var) : nb059AlphaDummy015 R a ∈ (SemanticCore.Class.cab (nb059AlphaDummy019 R a) (Compiler.CompactSourceSyntax.synWrex (nb059AlphaDummy020 R a) (SemanticCore.Class.cv (nb059AlphaDummy015 R a)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb059AlphaDummy019 R a)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb059AlphaDummy020 R a))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb059AlphaDummy019 R a) (Compiler.CompactSourceSyntax.synWrex (nb059AlphaDummy020 R a) (SemanticCore.Class.cv (nb059AlphaDummy015 R a)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb059AlphaDummy019 R a)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb059AlphaDummy020 R a))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb059_support_mem_0044 (R S_cls : SemanticCore.Class) : nb059AlphaDummy018 R S_cls ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb059AlphaDummy018 R S_cls)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb059_support_mem_0045 (R : SemanticCore.Class) (a : SemanticCore.Var) : nb059AlphaDummy020 R a ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb059AlphaDummy020 R a)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb059_support_mem_0046 (R S_cls : SemanticCore.Class) : nb059AlphaDummy018 R S_cls ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb059AlphaDummy018 R S_cls))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb059AlphaDummy018 R S_cls))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb059_support_mem_0047 (R : SemanticCore.Class) (a : SemanticCore.Var) : nb059AlphaDummy020 R a ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb059AlphaDummy020 R a))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb059AlphaDummy020 R a))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb059_focused_notmem_0000 (R S_cls : SemanticCore.Class) : nb059AlphaDummy007 R S_cls ∉ S_cls.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb059_wpp_notmem_0000 (R S_cls : SemanticCore.Class) : nb059AlphaDummy007 R S_cls ∉ S_cls.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb059_focused_notmem_0001 (S_cls : SemanticCore.Class) (a : SemanticCore.Var) : nb059AlphaDummy008 S_cls a ∉ S_cls.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb059_wpp_notmem_0001 (S_cls : SemanticCore.Class) (a : SemanticCore.Var) : nb059AlphaDummy008 S_cls a ∉ S_cls.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb059_focused_notmem_0002 (R S_cls : SemanticCore.Class) : nb059AlphaDummy005 R S_cls ∉ S_cls.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb059_wpp_notmem_0002 (R S_cls : SemanticCore.Class) : nb059AlphaDummy005 R S_cls ∉ S_cls.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb059_focused_notmem_0003 (S_cls : SemanticCore.Class) (a : SemanticCore.Var) : nb059AlphaDummy006 S_cls a ∉ S_cls.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb059_wpp_notmem_0003 (S_cls : SemanticCore.Class) (a : SemanticCore.Var) : nb059AlphaDummy006 S_cls a ∉ S_cls.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb059_focused_notmem_0004 (R S_cls : SemanticCore.Class) : nb059AlphaDummy000 R S_cls ∉ S_cls.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb059_wpp_notmem_0004 (R S_cls : SemanticCore.Class) : nb059AlphaDummy000 R S_cls ∉ S_cls.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb059_wpp_notmem_0005 (S_cls : SemanticCore.Class) (a : SemanticCore.Var) (dv_S_a : a ∉ S_cls.fv) : a ∉ S_cls.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb059_focused_notmem_0005 (R S_cls : SemanticCore.Class) : nb059AlphaDummy002 R S_cls ∉ S_cls.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb059_wpp_notmem_0006 (R S_cls : SemanticCore.Class) : nb059AlphaDummy002 R S_cls ∉ S_cls.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb059_focused_notmem_0006 (R S_cls : SemanticCore.Class) (a : SemanticCore.Var) (dv_S_a : a ∉ S_cls.fv) : nb059AlphaDummy004 R S_cls a ∉ S_cls.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb059_wpp_notmem_0007 (R S_cls : SemanticCore.Class) (a : SemanticCore.Var) (dv_S_a : a ∉ S_cls.fv) : nb059AlphaDummy004 R S_cls a ∉ S_cls.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb059_focused_notmem_0007 (R S_cls : SemanticCore.Class) : nb059AlphaDummy001 R S_cls ∉ S_cls.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb059_wpp_notmem_0008 (R S_cls : SemanticCore.Class) : nb059AlphaDummy001 R S_cls ∉ S_cls.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb059_focused_notmem_0008 (R S_cls : SemanticCore.Class) (a : SemanticCore.Var) (dv_S_a : a ∉ S_cls.fv) : nb059AlphaDummy003 R S_cls a ∉ S_cls.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb059_wpp_notmem_0009 (R S_cls : SemanticCore.Class) (a : SemanticCore.Var) (dv_S_a : a ∉ S_cls.fv) : nb059AlphaDummy003 R S_cls a ∉ S_cls.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb059_compact_envfresh_0000 (R S_cls : SemanticCore.Class) (a : SemanticCore.Var) (dv_S_a : a ∉ S_cls.fv) : Nominal.TEnvFresh [(nb059AlphaDummy007 R S_cls, nb059AlphaDummy008 S_cls a), (nb059AlphaDummy005 R S_cls, nb059AlphaDummy006 S_cls a), (nb059AlphaDummy000 R S_cls, a), (nb059AlphaDummy002 R S_cls, nb059AlphaDummy004 R S_cls a), (nb059AlphaDummy001 R S_cls, nb059AlphaDummy003 R S_cls a)] S_cls.fv

Certificates from AlphaSupport.NAR4C059C001Part002Stage2.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb059WppRefl0000 (R S_cls : SemanticCore.Class) (a : SemanticCore.Var) (dv_S_a : a ∉ S_cls.fv) : Nominal.TReflOn [(nb059AlphaDummy007 R S_cls, nb059AlphaDummy008 S_cls a), (nb059AlphaDummy005 R S_cls, nb059AlphaDummy006 S_cls a), (nb059AlphaDummy000 R S_cls, a), (nb059AlphaDummy002 R S_cls, nb059AlphaDummy004 R S_cls a), (nb059AlphaDummy001 R S_cls, nb059AlphaDummy003 R S_cls a)] S_cls.fv

Checked nominal proof certificate identified upstream as nb059_wpp_refl_0000.

Equations

• NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb059WppRefl0000 R S_cls a dv_S_a = ⋯.reflOn

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb059_compact_envfresh_0001 (R S_cls : SemanticCore.Class) (a : SemanticCore.Var) (dv_S_a : a ∉ S_cls.fv) : Nominal.TEnvFresh [(nb059AlphaDummy000 R S_cls, a), (nb059AlphaDummy002 R S_cls, nb059AlphaDummy004 R S_cls a), (nb059AlphaDummy001 R S_cls, nb059AlphaDummy003 R S_cls a)] S_cls.fv