NF weak partition development: NominalAlphaRepairedBase001043SiReflected001.

Shared variable, support, and alpha-certificate components.

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.alphaDummy000 (A : SemanticCore.Class) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_000.

Equations

• NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.alphaDummy000 A = NFChoice.ReplaySupport.freshVar A.fv

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.alphaDummy001 (A : SemanticCore.Class) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_001.

Equations

• NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.alphaDummy001 A = NFChoice.ReplaySupport.freshVar A.fv 1

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.alphaDummy002 (A : SemanticCore.Class) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_002.

Equations

• NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.alphaDummy002 A = NFChoice.ReplaySupport.freshVar A.fv 2

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.alphaDummy003 (A : SemanticCore.Class) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_003.

Equations

• NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.alphaDummy003 A = NFChoice.ReplaySupport.freshVar A.fv 3

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.alphaDummy004 (A : SemanticCore.Class) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_004.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.alphaDummy005 (x y z w : SemanticCore.Var) (A : SemanticCore.Class) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_005.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.alphaDummy006 (A : SemanticCore.Class) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_006.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.alphaDummy007 (A : SemanticCore.Class) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_007.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.alphaDummy008 (x y : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_008.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.alphaDummy009 (x y : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_009.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.alphaDummy010 (A : SemanticCore.Class) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_010.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.alphaDummy011 (x y : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_011.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.alphaDummy012 (A : SemanticCore.Class) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_012.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.alphaDummy013 (x y : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_013.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.alphaDummy014 (A : SemanticCore.Class) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_014.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.alphaDummy015 (A : SemanticCore.Class) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_015.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.alphaDummy016 (x y : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_016.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.alphaDummy017 (x y : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_017.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.alphaDummy018 (A : SemanticCore.Class) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_018.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.alphaDummy019 (x y : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_019.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.alphaDummy020 (A : SemanticCore.Class) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_020.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.alphaDummy021 (A : SemanticCore.Class) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_021.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.alphaDummy022 (A : SemanticCore.Class) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_022.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.alphaDummy023 (x y : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_023.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.alphaDummy024 (x y : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_024.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.alphaDummy025 (x y : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_025.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.alphaDummy036 (A : SemanticCore.Class) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_036.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.alphaDummy037 (x y : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_037.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.alphaDummy038 (A : SemanticCore.Class) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_038.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.alphaDummy039 (x y : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_039.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.alphaDummy040 (A : SemanticCore.Class) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_040.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.alphaDummy041 (x y : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_041.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.alphaDummy046 (A : SemanticCore.Class) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_046.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.alphaDummy047 (A : SemanticCore.Class) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_047.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.alphaDummy048 (z w : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_048.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.alphaDummy049 (z w : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_049.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.alphaDummy050 (A : SemanticCore.Class) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_050.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.alphaDummy051 (z w : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_051.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.alphaDummy052 (A : SemanticCore.Class) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_052.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.alphaDummy053 (z w : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_053.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.alphaDummy054 (A : SemanticCore.Class) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_054.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.alphaDummy055 (A : SemanticCore.Class) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_055.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.alphaDummy056 (z w : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_056.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.alphaDummy057 (z w : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_057.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.alphaDummy058 (A : SemanticCore.Class) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_058.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.alphaDummy059 (z w : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_059.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.alphaDummy060 (A : SemanticCore.Class) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_060.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.alphaDummy061 (A : SemanticCore.Class) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_061.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.alphaDummy062 (A : SemanticCore.Class) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_062.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.alphaDummy063 (z w : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_063.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.alphaDummy064 (z w : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_064.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.alphaDummy065 (z w : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_065.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.alphaDummy076 (A : SemanticCore.Class) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_076.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.alphaDummy077 (z w : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_077.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.alphaDummy078 (A : SemanticCore.Class) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_078.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.alphaDummy079 (z w : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_079.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.alphaDummy080 (A : SemanticCore.Class) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_080.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.alphaDummy081 (z w : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_081.

Equations

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.mem_pair_support_left (u v : SemanticCore.Var) (support : Finset SemanticCore.Var) : u ∈ {u} ∪ {v} ∪ support

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.mem_pair_support_right (u v : SemanticCore.Var) (support : Finset SemanticCore.Var) : v ∈ {u} ∪ {v} ∪ support

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.support_mem_0000 (A : SemanticCore.Class) : alphaDummy001 A ∈ {alphaDummy001 A} ∪ {alphaDummy002 A} ∪ (Compiler.CompactSourceSyntax.synWex (alphaDummy003 A) (Compiler.CompactSourceSyntax.synWex (alphaDummy000 A) (Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy001 A)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (alphaDummy003 A)))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy002 A)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (alphaDummy000 A)))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (alphaDummy003 A)) A (SemanticCore.Class.cv (alphaDummy000 A)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.support_mem_0001 (x y z w : SemanticCore.Var) (A : SemanticCore.Class) : x ∈ {x} ∪ {y} ∪ (Compiler.CompactSourceSyntax.synWex z (Compiler.CompactSourceSyntax.synWex w (Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv z))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv y) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv w))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv z) A (SemanticCore.Class.cv w))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.support_mem_0002 (A : SemanticCore.Class) : alphaDummy002 A ∈ {alphaDummy001 A} ∪ {alphaDummy002 A} ∪ (Compiler.CompactSourceSyntax.synWex (alphaDummy003 A) (Compiler.CompactSourceSyntax.synWex (alphaDummy000 A) (Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy001 A)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (alphaDummy003 A)))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy002 A)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (alphaDummy000 A)))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (alphaDummy003 A)) A (SemanticCore.Class.cv (alphaDummy000 A)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.support_mem_0003 (x y z w : SemanticCore.Var) (A : SemanticCore.Class) : y ∈ {x} ∪ {y} ∪ (Compiler.CompactSourceSyntax.synWex z (Compiler.CompactSourceSyntax.synWex w (Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv z))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv y) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv w))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv z) A (SemanticCore.Class.cv w))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.support_mem_0004 (A : SemanticCore.Class) : alphaDummy001 A ∈ (SemanticCore.Class.cv (alphaDummy001 A)).fv ∪ (SemanticCore.Class.cv (alphaDummy002 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.support_mem_0005 (A : SemanticCore.Class) : alphaDummy001 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (alphaDummy006 A) (Compiler.CompactSourceSyntax.synWrex (alphaDummy007 A) (SemanticCore.Class.cv (alphaDummy001 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy006 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy007 A))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (alphaDummy006 A) (Compiler.CompactSourceSyntax.synWrex (alphaDummy007 A) (SemanticCore.Class.cv (alphaDummy002 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy006 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy007 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.support_mem_0006 (x y : SemanticCore.Var) : x ∈ (SemanticCore.Class.cv x).fv ∪ (SemanticCore.Class.cv y).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.support_mem_0007 (x y : SemanticCore.Var) : x ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (alphaDummy008 x y) (Compiler.CompactSourceSyntax.synWrex (alphaDummy009 x y) (SemanticCore.Class.cv x) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy008 x y)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy009 x y))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (alphaDummy008 x y) (Compiler.CompactSourceSyntax.synWrex (alphaDummy009 x y) (SemanticCore.Class.cv y) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy008 x y)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy009 x y))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.support_mem_0008 (A : SemanticCore.Class) : alphaDummy001 A ∈ (SemanticCore.Class.cab (alphaDummy006 A) (Compiler.CompactSourceSyntax.synWrex (alphaDummy007 A) (SemanticCore.Class.cv (alphaDummy001 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy006 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy007 A)))))).fv ∪ (SemanticCore.Class.cab (alphaDummy006 A) (Compiler.CompactSourceSyntax.synWrex (alphaDummy007 A) (SemanticCore.Class.cv (alphaDummy001 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy006 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy007 A)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.support_mem_0009 (x y : SemanticCore.Var) : x ∈ (SemanticCore.Class.cab (alphaDummy008 x y) (Compiler.CompactSourceSyntax.synWrex (alphaDummy009 x y) (SemanticCore.Class.cv x) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy008 x y)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy009 x y)))))).fv ∪ (SemanticCore.Class.cab (alphaDummy008 x y) (Compiler.CompactSourceSyntax.synWrex (alphaDummy009 x y) (SemanticCore.Class.cv x) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy008 x y)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy009 x y)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.support_mem_0010 (A : SemanticCore.Class) : alphaDummy007 A ∈ (SemanticCore.Class.cv (alphaDummy007 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.support_mem_0011 (x y : SemanticCore.Var) : alphaDummy009 x y ∈ (SemanticCore.Class.cv (alphaDummy009 x y)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.support_mem_0013 (x y : SemanticCore.Var) : alphaDummy016 x y ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (alphaDummy016 x y)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (alphaDummy016 x y)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (alphaDummy016 x y)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.support_mem_0014 (A : SemanticCore.Class) : alphaDummy014 A ∈ (SemanticCore.Class.cv (alphaDummy014 A)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.support_mem_0015 (x y : SemanticCore.Var) : alphaDummy016 x y ∈ (SemanticCore.Class.cv (alphaDummy016 x y)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.support_mem_0016 (A : SemanticCore.Class) : alphaDummy021 A ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (alphaDummy021 A)) (SemanticCore.Class.cv (alphaDummy022 A))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (alphaDummy021 A)) (SemanticCore.Class.cv (alphaDummy022 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.support_mem_0017 (x y : SemanticCore.Var) : alphaDummy024 x y ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (alphaDummy024 x y)) (SemanticCore.Class.cv (alphaDummy025 x y))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (alphaDummy024 x y)) (SemanticCore.Class.cv (alphaDummy025 x y))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.support_mem_0018 (A : SemanticCore.Class) : alphaDummy021 A ∈ (SemanticCore.Class.cv (alphaDummy021 A)).fv ∪ (SemanticCore.Class.cv (alphaDummy022 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.support_mem_0019 (x y : SemanticCore.Var) : alphaDummy024 x y ∈ (SemanticCore.Class.cv (alphaDummy024 x y)).fv ∪ (SemanticCore.Class.cv (alphaDummy025 x y)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.support_mem_0020 (A : SemanticCore.Class) : alphaDummy022 A ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (alphaDummy021 A)) (SemanticCore.Class.cv (alphaDummy022 A))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (alphaDummy021 A)) (SemanticCore.Class.cv (alphaDummy022 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.support_mem_0021 (x y : SemanticCore.Var) : alphaDummy025 x y ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (alphaDummy024 x y)) (SemanticCore.Class.cv (alphaDummy025 x y))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (alphaDummy024 x y)) (SemanticCore.Class.cv (alphaDummy025 x y))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.support_mem_0022 (A : SemanticCore.Class) : alphaDummy022 A ∈ (SemanticCore.Class.cv (alphaDummy021 A)).fv ∪ (SemanticCore.Class.cv (alphaDummy022 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.support_mem_0023 (x y : SemanticCore.Var) : alphaDummy025 x y ∈ (SemanticCore.Class.cv (alphaDummy024 x y)).fv ∪ (SemanticCore.Class.cv (alphaDummy025 x y)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.support_mem_0024 (A : SemanticCore.Class) : alphaDummy021 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (alphaDummy021 A))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (alphaDummy022 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.support_mem_0025 (x y : SemanticCore.Var) : alphaDummy024 x y ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (alphaDummy024 x y))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (alphaDummy025 x y))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.support_mem_0026 (A : SemanticCore.Class) : alphaDummy021 A ∈ (SemanticCore.Class.cv (alphaDummy021 A)).fv ∪ (SemanticCore.Class.cv (alphaDummy021 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.support_mem_0027 (x y : SemanticCore.Var) : alphaDummy024 x y ∈ (SemanticCore.Class.cv (alphaDummy024 x y)).fv ∪ (SemanticCore.Class.cv (alphaDummy024 x y)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.support_mem_0028 (A : SemanticCore.Class) : alphaDummy022 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (alphaDummy021 A))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (alphaDummy022 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.support_mem_0029 (x y : SemanticCore.Var) : alphaDummy025 x y ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (alphaDummy024 x y))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (alphaDummy025 x y))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.support_mem_0030 (A : SemanticCore.Class) : alphaDummy022 A ∈ (SemanticCore.Class.cv (alphaDummy022 A)).fv ∪ (SemanticCore.Class.cv (alphaDummy022 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.support_mem_0031 (x y : SemanticCore.Var) : alphaDummy025 x y ∈ (SemanticCore.Class.cv (alphaDummy025 x y)).fv ∪ (SemanticCore.Class.cv (alphaDummy025 x y)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.support_mem_0032 (A : SemanticCore.Class) : alphaDummy002 A ∈ (SemanticCore.Class.cv (alphaDummy001 A)).fv ∪ (SemanticCore.Class.cv (alphaDummy002 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.support_mem_0033 (A : SemanticCore.Class) : alphaDummy002 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (alphaDummy006 A) (Compiler.CompactSourceSyntax.synWrex (alphaDummy007 A) (SemanticCore.Class.cv (alphaDummy001 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy006 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy007 A))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (alphaDummy006 A) (Compiler.CompactSourceSyntax.synWrex (alphaDummy007 A) (SemanticCore.Class.cv (alphaDummy002 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy006 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy007 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.support_mem_0034 (x y : SemanticCore.Var) : y ∈ (SemanticCore.Class.cv x).fv ∪ (SemanticCore.Class.cv y).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.support_mem_0035 (x y : SemanticCore.Var) : y ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (alphaDummy008 x y) (Compiler.CompactSourceSyntax.synWrex (alphaDummy009 x y) (SemanticCore.Class.cv x) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy008 x y)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy009 x y))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (alphaDummy008 x y) (Compiler.CompactSourceSyntax.synWrex (alphaDummy009 x y) (SemanticCore.Class.cv y) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy008 x y)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy009 x y))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.support_mem_0036 (A : SemanticCore.Class) : alphaDummy002 A ∈ (SemanticCore.Class.cab (alphaDummy006 A) (Compiler.CompactSourceSyntax.synWrex (alphaDummy007 A) (SemanticCore.Class.cv (alphaDummy002 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy006 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy007 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (alphaDummy006 A) (Compiler.CompactSourceSyntax.synWrex (alphaDummy007 A) (SemanticCore.Class.cv (alphaDummy002 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy006 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy007 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.support_mem_0037 (x y : SemanticCore.Var) : y ∈ (SemanticCore.Class.cab (alphaDummy008 x y) (Compiler.CompactSourceSyntax.synWrex (alphaDummy009 x y) (SemanticCore.Class.cv y) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy008 x y)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy009 x y))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (alphaDummy008 x y) (Compiler.CompactSourceSyntax.synWrex (alphaDummy009 x y) (SemanticCore.Class.cv y) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy008 x y)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy009 x y))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.support_mem_0039 (x y : SemanticCore.Var) : alphaDummy009 x y ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy009 x y)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.support_mem_0040 (A : SemanticCore.Class) : alphaDummy007 A ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy007 A))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy007 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.support_mem_0041 (x y : SemanticCore.Var) : alphaDummy009 x y ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy009 x y))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy009 x y))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.support_mem_0042 (A : SemanticCore.Class) : alphaDummy003 A ∈ (SemanticCore.Class.cv (alphaDummy003 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.support_mem_0043 (z : SemanticCore.Var) : z ∈ (SemanticCore.Class.cv z).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.support_mem_0044 (A : SemanticCore.Class) : alphaDummy000 A ∈ (SemanticCore.Class.cv (alphaDummy000 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.support_mem_0045 (w : SemanticCore.Var) : w ∈ (SemanticCore.Class.cv w).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.support_mem_0046 (A : SemanticCore.Class) : alphaDummy003 A ∈ (SemanticCore.Class.cv (alphaDummy003 A)).fv ∪ (SemanticCore.Class.cv (alphaDummy000 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.support_mem_0047 (A : SemanticCore.Class) : alphaDummy003 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (alphaDummy046 A) (Compiler.CompactSourceSyntax.synWrex (alphaDummy047 A) (SemanticCore.Class.cv (alphaDummy003 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy046 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy047 A))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (alphaDummy046 A) (Compiler.CompactSourceSyntax.synWrex (alphaDummy047 A) (SemanticCore.Class.cv (alphaDummy000 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy046 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy047 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.support_mem_0048 (z w : SemanticCore.Var) : z ∈ (SemanticCore.Class.cv z).fv ∪ (SemanticCore.Class.cv w).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.support_mem_0049 (z w : SemanticCore.Var) : z ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (alphaDummy048 z w) (Compiler.CompactSourceSyntax.synWrex (alphaDummy049 z w) (SemanticCore.Class.cv z) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy048 z w)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy049 z w))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (alphaDummy048 z w) (Compiler.CompactSourceSyntax.synWrex (alphaDummy049 z w) (SemanticCore.Class.cv w) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy048 z w)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy049 z w))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.support_mem_0050 (A : SemanticCore.Class) : alphaDummy003 A ∈ (SemanticCore.Class.cab (alphaDummy046 A) (Compiler.CompactSourceSyntax.synWrex (alphaDummy047 A) (SemanticCore.Class.cv (alphaDummy003 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy046 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy047 A)))))).fv ∪ (SemanticCore.Class.cab (alphaDummy046 A) (Compiler.CompactSourceSyntax.synWrex (alphaDummy047 A) (SemanticCore.Class.cv (alphaDummy003 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy046 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy047 A)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.support_mem_0051 (z w : SemanticCore.Var) : z ∈ (SemanticCore.Class.cab (alphaDummy048 z w) (Compiler.CompactSourceSyntax.synWrex (alphaDummy049 z w) (SemanticCore.Class.cv z) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy048 z w)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy049 z w)))))).fv ∪ (SemanticCore.Class.cab (alphaDummy048 z w) (Compiler.CompactSourceSyntax.synWrex (alphaDummy049 z w) (SemanticCore.Class.cv z) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy048 z w)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy049 z w)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.support_mem_0052 (A : SemanticCore.Class) : alphaDummy047 A ∈ (SemanticCore.Class.cv (alphaDummy047 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.support_mem_0053 (z w : SemanticCore.Var) : alphaDummy049 z w ∈ (SemanticCore.Class.cv (alphaDummy049 z w)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.support_mem_0055 (z w : SemanticCore.Var) : alphaDummy056 z w ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (alphaDummy056 z w)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (alphaDummy056 z w)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (alphaDummy056 z w)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.support_mem_0056 (A : SemanticCore.Class) : alphaDummy054 A ∈ (SemanticCore.Class.cv (alphaDummy054 A)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.support_mem_0057 (z w : SemanticCore.Var) : alphaDummy056 z w ∈ (SemanticCore.Class.cv (alphaDummy056 z w)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.support_mem_0058 (A : SemanticCore.Class) : alphaDummy061 A ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (alphaDummy061 A)) (SemanticCore.Class.cv (alphaDummy062 A))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (alphaDummy061 A)) (SemanticCore.Class.cv (alphaDummy062 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.support_mem_0059 (z w : SemanticCore.Var) : alphaDummy064 z w ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (alphaDummy064 z w)) (SemanticCore.Class.cv (alphaDummy065 z w))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (alphaDummy064 z w)) (SemanticCore.Class.cv (alphaDummy065 z w))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.support_mem_0060 (A : SemanticCore.Class) : alphaDummy061 A ∈ (SemanticCore.Class.cv (alphaDummy061 A)).fv ∪ (SemanticCore.Class.cv (alphaDummy062 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.support_mem_0061 (z w : SemanticCore.Var) : alphaDummy064 z w ∈ (SemanticCore.Class.cv (alphaDummy064 z w)).fv ∪ (SemanticCore.Class.cv (alphaDummy065 z w)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.support_mem_0062 (A : SemanticCore.Class) : alphaDummy062 A ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (alphaDummy061 A)) (SemanticCore.Class.cv (alphaDummy062 A))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (alphaDummy061 A)) (SemanticCore.Class.cv (alphaDummy062 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.support_mem_0063 (z w : SemanticCore.Var) : alphaDummy065 z w ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (alphaDummy064 z w)) (SemanticCore.Class.cv (alphaDummy065 z w))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (alphaDummy064 z w)) (SemanticCore.Class.cv (alphaDummy065 z w))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.support_mem_0064 (A : SemanticCore.Class) : alphaDummy062 A ∈ (SemanticCore.Class.cv (alphaDummy061 A)).fv ∪ (SemanticCore.Class.cv (alphaDummy062 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.support_mem_0065 (z w : SemanticCore.Var) : alphaDummy065 z w ∈ (SemanticCore.Class.cv (alphaDummy064 z w)).fv ∪ (SemanticCore.Class.cv (alphaDummy065 z w)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.support_mem_0066 (A : SemanticCore.Class) : alphaDummy061 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (alphaDummy061 A))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (alphaDummy062 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.support_mem_0067 (z w : SemanticCore.Var) : alphaDummy064 z w ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (alphaDummy064 z w))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (alphaDummy065 z w))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.support_mem_0068 (A : SemanticCore.Class) : alphaDummy061 A ∈ (SemanticCore.Class.cv (alphaDummy061 A)).fv ∪ (SemanticCore.Class.cv (alphaDummy061 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.support_mem_0069 (z w : SemanticCore.Var) : alphaDummy064 z w ∈ (SemanticCore.Class.cv (alphaDummy064 z w)).fv ∪ (SemanticCore.Class.cv (alphaDummy064 z w)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.support_mem_0070 (A : SemanticCore.Class) : alphaDummy062 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (alphaDummy061 A))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (alphaDummy062 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.support_mem_0071 (z w : SemanticCore.Var) : alphaDummy065 z w ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (alphaDummy064 z w))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (alphaDummy065 z w))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.support_mem_0072 (A : SemanticCore.Class) : alphaDummy062 A ∈ (SemanticCore.Class.cv (alphaDummy062 A)).fv ∪ (SemanticCore.Class.cv (alphaDummy062 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.support_mem_0073 (z w : SemanticCore.Var) : alphaDummy065 z w ∈ (SemanticCore.Class.cv (alphaDummy065 z w)).fv ∪ (SemanticCore.Class.cv (alphaDummy065 z w)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.support_mem_0074 (A : SemanticCore.Class) : alphaDummy000 A ∈ (SemanticCore.Class.cv (alphaDummy003 A)).fv ∪ (SemanticCore.Class.cv (alphaDummy000 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.support_mem_0075 (A : SemanticCore.Class) : alphaDummy000 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (alphaDummy046 A) (Compiler.CompactSourceSyntax.synWrex (alphaDummy047 A) (SemanticCore.Class.cv (alphaDummy003 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy046 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy047 A))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (alphaDummy046 A) (Compiler.CompactSourceSyntax.synWrex (alphaDummy047 A) (SemanticCore.Class.cv (alphaDummy000 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy046 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy047 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.support_mem_0076 (z w : SemanticCore.Var) : w ∈ (SemanticCore.Class.cv z).fv ∪ (SemanticCore.Class.cv w).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.support_mem_0077 (z w : SemanticCore.Var) : w ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (alphaDummy048 z w) (Compiler.CompactSourceSyntax.synWrex (alphaDummy049 z w) (SemanticCore.Class.cv z) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy048 z w)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy049 z w))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (alphaDummy048 z w) (Compiler.CompactSourceSyntax.synWrex (alphaDummy049 z w) (SemanticCore.Class.cv w) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy048 z w)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy049 z w))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.support_mem_0078 (A : SemanticCore.Class) : alphaDummy000 A ∈ (SemanticCore.Class.cab (alphaDummy046 A) (Compiler.CompactSourceSyntax.synWrex (alphaDummy047 A) (SemanticCore.Class.cv (alphaDummy000 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy046 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy047 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (alphaDummy046 A) (Compiler.CompactSourceSyntax.synWrex (alphaDummy047 A) (SemanticCore.Class.cv (alphaDummy000 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy046 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy047 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.support_mem_0079 (z w : SemanticCore.Var) : w ∈ (SemanticCore.Class.cab (alphaDummy048 z w) (Compiler.CompactSourceSyntax.synWrex (alphaDummy049 z w) (SemanticCore.Class.cv w) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy048 z w)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy049 z w))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (alphaDummy048 z w) (Compiler.CompactSourceSyntax.synWrex (alphaDummy049 z w) (SemanticCore.Class.cv w) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy048 z w)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy049 z w))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.support_mem_0081 (z w : SemanticCore.Var) : alphaDummy049 z w ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy049 z w)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.support_mem_0082 (A : SemanticCore.Class) : alphaDummy047 A ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy047 A))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy047 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.support_mem_0083 (z w : SemanticCore.Var) : alphaDummy049 z w ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy049 z w))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy049 z w))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.focused_notmem_0000 (A : SemanticCore.Class) : alphaDummy000 A ∉ A.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.focused_notmem_0001 (A : SemanticCore.Class) : alphaDummy003 A ∉ A.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.parameter_support (x y z w : SemanticCore.Var) (A : SemanticCore.Class) (hz : z ∉ A.fv) (hw : w ∉ A.fv) ⦃u : SemanticCore.Var⦄ : u ∈ A.fv → u ∈ (Compiler.CompactSourceSyntax.synWex z (Compiler.CompactSourceSyntax.synWex w (Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv z))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv y) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv w))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv z) A (SemanticCore.Class.cv w))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.focused_notmem_0002 (A : SemanticCore.Class) : alphaDummy004 A ∉ A.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.wpp_notmem_0204 (A : SemanticCore.Class) : alphaDummy004 A ∉ A.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.focused_notmem_0003 (x y z w : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_w : w ∉ A.fv) (dv_A_z : z ∉ A.fv) : alphaDummy005 x y z w A ∉ A.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.wpp_notmem_0205 (x y z w : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_w : w ∉ A.fv) (dv_A_z : z ∉ A.fv) : alphaDummy005 x y z w A ∉ A.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.focused_notmem_0004 (A : SemanticCore.Class) : alphaDummy001 A ∉ A.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.wpp_notmem_0206 (A : SemanticCore.Class) : alphaDummy001 A ∉ A.fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.focused_notmem_0005 (A : SemanticCore.Class) : alphaDummy002 A ∉ A.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.wpp_notmem_0208 (A : SemanticCore.Class) : alphaDummy002 A ∉ A.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.wpp_notmem_0209 (y : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_y : y ∉ A.fv) : y ∉ A.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.wpp_notmem_0210 (A : SemanticCore.Class) : alphaDummy003 A ∉ A.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.wpp_notmem_0211 (z : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_z : z ∉ A.fv) : z ∉ A.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.wpp_notmem_0212 (A : SemanticCore.Class) : alphaDummy000 A ∉ A.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SingletonImageAlpha.wpp_notmem_0213 (w : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_w : w ∉ A.fv) : w ∉ A.fv