Nominal proof certificates grouped in dependency order.

Certificates from AlphaSupport.NAR4C070C001Part002Stage1.

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_support_mem_0011 (x : SemanticCore.Var) : x ∈ (Compiler.CompactSourceSyntax.synCpw (SemanticCore.Class.cv x)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_support_mem_0012 (A : SemanticCore.Class) : nb070AlphaDummy001 A ∈ (SemanticCore.Class.cv (nb070AlphaDummy001 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_support_mem_0013 (x : SemanticCore.Var) : x ∈ (SemanticCore.Class.cv x).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_support_mem_0014 (A : SemanticCore.Class) : nb070AlphaDummy001 A ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb070AlphaDummy018 A)) (SemanticCore.Class.cv (nb070AlphaDummy001 A))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb070AlphaDummy018 A)) (SemanticCore.Class.cv (nb070AlphaDummy001 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_support_mem_0015 (x : SemanticCore.Var) : x ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb070AlphaDummy019 x)) (SemanticCore.Class.cv x)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb070AlphaDummy019 x)) (SemanticCore.Class.cv x)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_support_mem_0016 (A : SemanticCore.Class) : nb070AlphaDummy001 A ∈ (SemanticCore.Class.cv (nb070AlphaDummy018 A)).fv ∪ (SemanticCore.Class.cv (nb070AlphaDummy001 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_support_mem_0017 (x : SemanticCore.Var) : x ∈ (SemanticCore.Class.cv (nb070AlphaDummy019 x)).fv ∪ (SemanticCore.Class.cv x).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_support_mem_0018 (A : SemanticCore.Class) : nb070AlphaDummy009 A ∈ (SemanticCore.Class.cv (nb070AlphaDummy009 A)).fv ∪ (SemanticCore.Class.cv (nb070AlphaDummy008 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_support_mem_0019 (A : SemanticCore.Class) : nb070AlphaDummy009 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb070AlphaDummy024 A) (Compiler.CompactSourceSyntax.synWrex (nb070AlphaDummy025 A) (SemanticCore.Class.cv (nb070AlphaDummy009 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb070AlphaDummy024 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb070AlphaDummy025 A))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb070AlphaDummy024 A) (Compiler.CompactSourceSyntax.synWrex (nb070AlphaDummy025 A) (SemanticCore.Class.cv (nb070AlphaDummy008 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb070AlphaDummy024 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb070AlphaDummy025 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_support_mem_0020 (x : SemanticCore.Var) : nb070AlphaDummy011 x ∈ (SemanticCore.Class.cv (nb070AlphaDummy011 x)).fv ∪ (SemanticCore.Class.cv (nb070AlphaDummy010 x)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_support_mem_0021 (x : SemanticCore.Var) : nb070AlphaDummy011 x ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb070AlphaDummy026 x) (Compiler.CompactSourceSyntax.synWrex (nb070AlphaDummy027 x) (SemanticCore.Class.cv (nb070AlphaDummy011 x)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb070AlphaDummy026 x)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb070AlphaDummy027 x))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb070AlphaDummy026 x) (Compiler.CompactSourceSyntax.synWrex (nb070AlphaDummy027 x) (SemanticCore.Class.cv (nb070AlphaDummy010 x)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb070AlphaDummy026 x)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb070AlphaDummy027 x))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_support_mem_0022 (A : SemanticCore.Class) : nb070AlphaDummy009 A ∈ (SemanticCore.Class.cab (nb070AlphaDummy024 A) (Compiler.CompactSourceSyntax.synWrex (nb070AlphaDummy025 A) (SemanticCore.Class.cv (nb070AlphaDummy009 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb070AlphaDummy024 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb070AlphaDummy025 A)))))).fv ∪ (SemanticCore.Class.cab (nb070AlphaDummy024 A) (Compiler.CompactSourceSyntax.synWrex (nb070AlphaDummy025 A) (SemanticCore.Class.cv (nb070AlphaDummy009 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb070AlphaDummy024 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb070AlphaDummy025 A)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_support_mem_0023 (x : SemanticCore.Var) : nb070AlphaDummy011 x ∈ (SemanticCore.Class.cab (nb070AlphaDummy026 x) (Compiler.CompactSourceSyntax.synWrex (nb070AlphaDummy027 x) (SemanticCore.Class.cv (nb070AlphaDummy011 x)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb070AlphaDummy026 x)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb070AlphaDummy027 x)))))).fv ∪ (SemanticCore.Class.cab (nb070AlphaDummy026 x) (Compiler.CompactSourceSyntax.synWrex (nb070AlphaDummy027 x) (SemanticCore.Class.cv (nb070AlphaDummy011 x)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb070AlphaDummy026 x)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb070AlphaDummy027 x)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_support_mem_0024 (A : SemanticCore.Class) : nb070AlphaDummy025 A ∈ (SemanticCore.Class.cv (nb070AlphaDummy025 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_support_mem_0025 (x : SemanticCore.Var) : nb070AlphaDummy027 x ∈ (SemanticCore.Class.cv (nb070AlphaDummy027 x)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_support_mem_0026 (A : SemanticCore.Class) : nb070AlphaDummy032 A ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb070AlphaDummy032 A)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb070AlphaDummy032 A)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb070AlphaDummy032 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_support_mem_0027 (x : SemanticCore.Var) : nb070AlphaDummy034 x ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb070AlphaDummy034 x)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb070AlphaDummy034 x)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb070AlphaDummy034 x)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_support_mem_0028 (A : SemanticCore.Class) : nb070AlphaDummy032 A ∈ (SemanticCore.Class.cv (nb070AlphaDummy032 A)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_support_mem_0029 (x : SemanticCore.Var) : nb070AlphaDummy034 x ∈ (SemanticCore.Class.cv (nb070AlphaDummy034 x)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_support_mem_0030 (A : SemanticCore.Class) : nb070AlphaDummy039 A ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb070AlphaDummy039 A)) (SemanticCore.Class.cv (nb070AlphaDummy040 A))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb070AlphaDummy039 A)) (SemanticCore.Class.cv (nb070AlphaDummy040 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_support_mem_0031 (x : SemanticCore.Var) : nb070AlphaDummy042 x ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb070AlphaDummy042 x)) (SemanticCore.Class.cv (nb070AlphaDummy043 x))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb070AlphaDummy042 x)) (SemanticCore.Class.cv (nb070AlphaDummy043 x))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_support_mem_0032 (A : SemanticCore.Class) : nb070AlphaDummy039 A ∈ (SemanticCore.Class.cv (nb070AlphaDummy039 A)).fv ∪ (SemanticCore.Class.cv (nb070AlphaDummy040 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_support_mem_0033 (x : SemanticCore.Var) : nb070AlphaDummy042 x ∈ (SemanticCore.Class.cv (nb070AlphaDummy042 x)).fv ∪ (SemanticCore.Class.cv (nb070AlphaDummy043 x)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_support_mem_0034 (A : SemanticCore.Class) : nb070AlphaDummy040 A ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb070AlphaDummy039 A)) (SemanticCore.Class.cv (nb070AlphaDummy040 A))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb070AlphaDummy039 A)) (SemanticCore.Class.cv (nb070AlphaDummy040 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_support_mem_0035 (x : SemanticCore.Var) : nb070AlphaDummy043 x ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb070AlphaDummy042 x)) (SemanticCore.Class.cv (nb070AlphaDummy043 x))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb070AlphaDummy042 x)) (SemanticCore.Class.cv (nb070AlphaDummy043 x))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_support_mem_0036 (A : SemanticCore.Class) : nb070AlphaDummy040 A ∈ (SemanticCore.Class.cv (nb070AlphaDummy039 A)).fv ∪ (SemanticCore.Class.cv (nb070AlphaDummy040 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_support_mem_0037 (x : SemanticCore.Var) : nb070AlphaDummy043 x ∈ (SemanticCore.Class.cv (nb070AlphaDummy042 x)).fv ∪ (SemanticCore.Class.cv (nb070AlphaDummy043 x)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_support_mem_0038 (A : SemanticCore.Class) : nb070AlphaDummy039 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb070AlphaDummy039 A))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb070AlphaDummy040 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_support_mem_0039 (x : SemanticCore.Var) : nb070AlphaDummy042 x ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb070AlphaDummy042 x))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb070AlphaDummy043 x))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_support_mem_0040 (A : SemanticCore.Class) : nb070AlphaDummy039 A ∈ (SemanticCore.Class.cv (nb070AlphaDummy039 A)).fv ∪ (SemanticCore.Class.cv (nb070AlphaDummy039 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_support_mem_0041 (x : SemanticCore.Var) : nb070AlphaDummy042 x ∈ (SemanticCore.Class.cv (nb070AlphaDummy042 x)).fv ∪ (SemanticCore.Class.cv (nb070AlphaDummy042 x)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_support_mem_0042 (A : SemanticCore.Class) : nb070AlphaDummy040 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb070AlphaDummy039 A))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb070AlphaDummy040 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_support_mem_0043 (x : SemanticCore.Var) : nb070AlphaDummy043 x ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb070AlphaDummy042 x))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb070AlphaDummy043 x))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_support_mem_0044 (A : SemanticCore.Class) : nb070AlphaDummy040 A ∈ (SemanticCore.Class.cv (nb070AlphaDummy040 A)).fv ∪ (SemanticCore.Class.cv (nb070AlphaDummy040 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_support_mem_0045 (x : SemanticCore.Var) : nb070AlphaDummy043 x ∈ (SemanticCore.Class.cv (nb070AlphaDummy043 x)).fv ∪ (SemanticCore.Class.cv (nb070AlphaDummy043 x)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_support_mem_0046 (A : SemanticCore.Class) : nb070AlphaDummy008 A ∈ (SemanticCore.Class.cv (nb070AlphaDummy009 A)).fv ∪ (SemanticCore.Class.cv (nb070AlphaDummy008 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_support_mem_0047 (A : SemanticCore.Class) : nb070AlphaDummy008 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb070AlphaDummy024 A) (Compiler.CompactSourceSyntax.synWrex (nb070AlphaDummy025 A) (SemanticCore.Class.cv (nb070AlphaDummy009 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb070AlphaDummy024 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb070AlphaDummy025 A))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb070AlphaDummy024 A) (Compiler.CompactSourceSyntax.synWrex (nb070AlphaDummy025 A) (SemanticCore.Class.cv (nb070AlphaDummy008 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb070AlphaDummy024 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb070AlphaDummy025 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_support_mem_0048 (x : SemanticCore.Var) : nb070AlphaDummy010 x ∈ (SemanticCore.Class.cv (nb070AlphaDummy011 x)).fv ∪ (SemanticCore.Class.cv (nb070AlphaDummy010 x)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_support_mem_0049 (x : SemanticCore.Var) : nb070AlphaDummy010 x ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb070AlphaDummy026 x) (Compiler.CompactSourceSyntax.synWrex (nb070AlphaDummy027 x) (SemanticCore.Class.cv (nb070AlphaDummy011 x)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb070AlphaDummy026 x)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb070AlphaDummy027 x))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb070AlphaDummy026 x) (Compiler.CompactSourceSyntax.synWrex (nb070AlphaDummy027 x) (SemanticCore.Class.cv (nb070AlphaDummy010 x)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb070AlphaDummy026 x)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb070AlphaDummy027 x))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_support_mem_0050 (A : SemanticCore.Class) : nb070AlphaDummy008 A ∈ (SemanticCore.Class.cab (nb070AlphaDummy024 A) (Compiler.CompactSourceSyntax.synWrex (nb070AlphaDummy025 A) (SemanticCore.Class.cv (nb070AlphaDummy008 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb070AlphaDummy024 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb070AlphaDummy025 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb070AlphaDummy024 A) (Compiler.CompactSourceSyntax.synWrex (nb070AlphaDummy025 A) (SemanticCore.Class.cv (nb070AlphaDummy008 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb070AlphaDummy024 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb070AlphaDummy025 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_support_mem_0051 (x : SemanticCore.Var) : nb070AlphaDummy010 x ∈ (SemanticCore.Class.cab (nb070AlphaDummy026 x) (Compiler.CompactSourceSyntax.synWrex (nb070AlphaDummy027 x) (SemanticCore.Class.cv (nb070AlphaDummy010 x)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb070AlphaDummy026 x)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb070AlphaDummy027 x))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb070AlphaDummy026 x) (Compiler.CompactSourceSyntax.synWrex (nb070AlphaDummy027 x) (SemanticCore.Class.cv (nb070AlphaDummy010 x)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb070AlphaDummy026 x)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb070AlphaDummy027 x))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_support_mem_0052 (A : SemanticCore.Class) : nb070AlphaDummy025 A ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb070AlphaDummy025 A)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_support_mem_0053 (x : SemanticCore.Var) : nb070AlphaDummy027 x ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb070AlphaDummy027 x)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_support_mem_0054 (A : SemanticCore.Class) : nb070AlphaDummy025 A ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb070AlphaDummy025 A))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb070AlphaDummy025 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_support_mem_0055 (x : SemanticCore.Var) : nb070AlphaDummy027 x ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb070AlphaDummy027 x))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb070AlphaDummy027 x))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_support_mem_0056 (A : SemanticCore.Class) : nb070AlphaDummy002 A ∈ (SemanticCore.Class.cv (nb070AlphaDummy002 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_support_mem_0057 (x : SemanticCore.Var) (A : SemanticCore.Class) (b : SemanticCore.Var) : nb070AlphaDummy003 x A b ∈ (SemanticCore.Class.cv (nb070AlphaDummy003 x A b)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_compact_fv_empty_0000 (A : SemanticCore.Class) : nb070AlphaDummy000 A ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_wpp_notmem_0000 (A : SemanticCore.Class) : nb070AlphaDummy000 A ∉ Compiler.CompactSourceSyntax.synCncs.fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_wpp_notmem_0001 (b : SemanticCore.Var) : b ∉ Compiler.CompactSourceSyntax.synCncs.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_compact_fv_empty_0002 (A : SemanticCore.Class) : nb070AlphaDummy002 A ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_wpp_notmem_0002 (A : SemanticCore.Class) : nb070AlphaDummy002 A ∉ Compiler.CompactSourceSyntax.synCncs.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_compact_fv_empty_0003 (x : SemanticCore.Var) (A : SemanticCore.Class) (b : SemanticCore.Var) : nb070AlphaDummy003 x A b ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_wpp_notmem_0003 (x : SemanticCore.Var) (A : SemanticCore.Class) (b : SemanticCore.Var) : nb070AlphaDummy003 x A b ∉ Compiler.CompactSourceSyntax.synCncs.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_compact_fv_empty_0004 (A : SemanticCore.Class) : nb070AlphaDummy005 A ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_wpp_notmem_0004 (A : SemanticCore.Class) : nb070AlphaDummy005 A ∉ Compiler.CompactSourceSyntax.synCncs.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_compact_fv_empty_0005 (x : SemanticCore.Var) (A : SemanticCore.Class) (b : SemanticCore.Var) : nb070AlphaDummy007 x A b ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_wpp_notmem_0005 (x : SemanticCore.Var) (A : SemanticCore.Class) (b : SemanticCore.Var) : nb070AlphaDummy007 x A b ∉ Compiler.CompactSourceSyntax.synCncs.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_compact_fv_empty_0006 (A : SemanticCore.Class) : nb070AlphaDummy004 A ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_wpp_notmem_0006 (A : SemanticCore.Class) : nb070AlphaDummy004 A ∉ Compiler.CompactSourceSyntax.synCncs.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_compact_fv_empty_0007 (x : SemanticCore.Var) (A : SemanticCore.Class) (b : SemanticCore.Var) : nb070AlphaDummy006 x A b ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_wpp_notmem_0007 (x : SemanticCore.Var) (A : SemanticCore.Class) (b : SemanticCore.Var) : nb070AlphaDummy006 x A b ∉ Compiler.CompactSourceSyntax.synCncs.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_compact_envfresh_0000 (x : SemanticCore.Var) (A : SemanticCore.Class) (b : SemanticCore.Var) : Nominal.TEnvFresh [(nb070AlphaDummy000 A, b), (nb070AlphaDummy002 A, nb070AlphaDummy003 x A b), (nb070AlphaDummy005 A, nb070AlphaDummy007 x A b), (nb070AlphaDummy004 A, nb070AlphaDummy006 x A b)] Compiler.CompactSourceSyntax.synCncs.fv

Certificates from AlphaSupport.NAR4C070C001Part002Stage2.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070WppRefl0000 (x : SemanticCore.Var) (A : SemanticCore.Class) (b : SemanticCore.Var) : Nominal.TReflOn [(nb070AlphaDummy000 A, b), (nb070AlphaDummy002 A, nb070AlphaDummy003 x A b), (nb070AlphaDummy005 A, nb070AlphaDummy007 x A b), (nb070AlphaDummy004 A, nb070AlphaDummy006 x A b)] Compiler.CompactSourceSyntax.synCncs.fv

Checked nominal proof certificate identified upstream as nb070_wpp_refl_0000.

Equations

• NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070WppRefl0000 x A b = ⋯.reflOn

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_focused_notmem_0000 (A : SemanticCore.Class) : nb070AlphaDummy001 A ∉ A.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_wpp_notmem_0008 (A : SemanticCore.Class) : nb070AlphaDummy001 A ∉ A.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_wpp_notmem_0009 (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) : x ∉ A.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_focused_notmem_0001 (A : SemanticCore.Class) : nb070AlphaDummy000 A ∉ A.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_wpp_notmem_0010 (A : SemanticCore.Class) : nb070AlphaDummy000 A ∉ A.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_wpp_notmem_0011 (A : SemanticCore.Class) (b : SemanticCore.Var) (dv_A_b : b ∉ A.fv) : b ∉ A.fv

Certificates from AlphaSupport.NAR4C070C001Part002Stage3.

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070Predicate (x : SemanticCore.Var) (A : SemanticCore.Class) (b : SemanticCore.Var) : SemanticCore.Wff

Checked nominal proof certificate identified upstream as nb070_predicate.

Equations

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_predicate_support (x : SemanticCore.Var) (A : SemanticCore.Class) (b : SemanticCore.Var) (hx : x ∉ A.fv) (u : SemanticCore.Var) : u ∈ A.fv → u ∈ (nb070Predicate x A b).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_support_cab (support : Finset SemanticCore.Var) (b : SemanticCore.Var) (predicate : SemanticCore.Wff) (hb : b ∉ support) (hsub : ∀ u ∈ support, u ∈ predicate.fv) (u : SemanticCore.Var) : u ∈ support → u ∈ (SemanticCore.Class.cab b predicate).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_inner_support (x : SemanticCore.Var) (A : SemanticCore.Class) (b : SemanticCore.Var) (hx : x ∉ A.fv) (hb : b ∉ A.fv) (u : SemanticCore.Var) : u ∈ A.fv → u ∈ (SemanticCore.Class.cab b (nb070Predicate x A b)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_outer_support (x : SemanticCore.Var) (A : SemanticCore.Class) (b v : SemanticCore.Var) (hx : x ∉ A.fv) (hb : b ∉ A.fv) (hv : v ∉ A.fv) (u : SemanticCore.Var) : u ∈ A.fv → u ∈ (SemanticCore.Class.cab v (SemanticCore.Wff.classEq (SemanticCore.Class.cab b (nb070Predicate x A b)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv v)))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_predicate_fresh (x : SemanticCore.Var) (A : SemanticCore.Class) (b : SemanticCore.Var) (hx : x ∉ A.fv) : ReplaySupport.freshVar ({b} ∪ (nb070Predicate x A b).fv) ∉ A.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_outer_fresh (x : SemanticCore.Var) (A : SemanticCore.Class) (b v : SemanticCore.Var) (offset : ℕ) (hx : x ∉ A.fv) (hb : b ∉ A.fv) (hv : v ∉ A.fv) : ReplaySupport.freshVar (SemanticCore.Class.cab v (SemanticCore.Wff.classEq (SemanticCore.Class.cab b (nb070Predicate x A b)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv v)))).fv offset ∉ A.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_focused_notmem_0002 (A : SemanticCore.Class) : nb070AlphaDummy002 A ∉ A.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_wpp_notmem_0012 (A : SemanticCore.Class) : nb070AlphaDummy002 A ∉ A.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_focused_notmem_0003 (x : SemanticCore.Var) (A : SemanticCore.Class) (b : SemanticCore.Var) (dv_A_x : x ∉ A.fv) : nb070AlphaDummy003 x A b ∉ A.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_wpp_notmem_0013 (x : SemanticCore.Var) (A : SemanticCore.Class) (b : SemanticCore.Var) (dv_A_x : x ∉ A.fv) : nb070AlphaDummy003 x A b ∉ A.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_focused_notmem_0004 (A : SemanticCore.Class) : nb070AlphaDummy005 A ∉ A.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_wpp_notmem_0014 (A : SemanticCore.Class) : nb070AlphaDummy005 A ∉ A.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_focused_notmem_0005 (x : SemanticCore.Var) (A : SemanticCore.Class) (b : SemanticCore.Var) (dv_A_b : b ∉ A.fv) (dv_A_x : x ∉ A.fv) : nb070AlphaDummy007 x A b ∉ A.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_wpp_notmem_0015 (x : SemanticCore.Var) (A : SemanticCore.Class) (b : SemanticCore.Var) (dv_A_b : b ∉ A.fv) (dv_A_x : x ∉ A.fv) : nb070AlphaDummy007 x A b ∉ A.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_focused_notmem_0006 (A : SemanticCore.Class) : nb070AlphaDummy004 A ∉ A.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_wpp_notmem_0016 (A : SemanticCore.Class) : nb070AlphaDummy004 A ∉ A.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_focused_notmem_0007 (x : SemanticCore.Var) (A : SemanticCore.Class) (b : SemanticCore.Var) (dv_A_b : b ∉ A.fv) (dv_A_x : x ∉ A.fv) : nb070AlphaDummy006 x A b ∉ A.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_wpp_notmem_0017 (x : SemanticCore.Var) (A : SemanticCore.Class) (b : SemanticCore.Var) (dv_A_b : b ∉ A.fv) (dv_A_x : x ∉ A.fv) : nb070AlphaDummy006 x A b ∉ A.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_compact_envfresh_0001 (x : SemanticCore.Var) (A : SemanticCore.Class) (b : SemanticCore.Var) (dv_A_b : b ∉ A.fv) (dv_A_x : x ∉ A.fv) : Nominal.TEnvFresh [(nb070AlphaDummy001 A, x), (nb070AlphaDummy000 A, b), (nb070AlphaDummy002 A, nb070AlphaDummy003 x A b), (nb070AlphaDummy005 A, nb070AlphaDummy007 x A b), (nb070AlphaDummy004 A, nb070AlphaDummy006 x A b)] A.fv

Certificates from AlphaSupport.NAR4C070C001Part002Stage4.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070WppRefl0001 (x : SemanticCore.Var) (A : SemanticCore.Class) (b : SemanticCore.Var) (dv_A_b : b ∉ A.fv) (dv_A_x : x ∉ A.fv) : Nominal.TReflOn [(nb070AlphaDummy001 A, x), (nb070AlphaDummy000 A, b), (nb070AlphaDummy002 A, nb070AlphaDummy003 x A b), (nb070AlphaDummy005 A, nb070AlphaDummy007 x A b), (nb070AlphaDummy004 A, nb070AlphaDummy006 x A b)] A.fv

Checked nominal proof certificate identified upstream as nb070_wpp_refl_0001.

Equations

• NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070WppRefl0001 x A b dv_A_b dv_A_x = ⋯.reflOn

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_compact_fv_empty_0014 (A : SemanticCore.Class) : nb070AlphaDummy009 A ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_compact_fv_empty_0015 (x : SemanticCore.Var) : nb070AlphaDummy011 x ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_compact_fv_empty_0016 (A : SemanticCore.Class) : nb070AlphaDummy008 A ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_compact_fv_empty_0017 (x : SemanticCore.Var) : nb070AlphaDummy010 x ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_compact_fv_empty_0018 (A : SemanticCore.Class) : nb070AlphaDummy001 A ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_compact_fv_empty_0019 (x : SemanticCore.Var) : x ∉ ∅