NF weak partition development: NominalAlphaRepairedBase001039SwapReflected001.

Shared variable, support, and alpha-certificate components for swap.

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.alphaDummy000 : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_000.

Equations

• NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.alphaDummy000 = NFChoice.ReplaySupport.freshVar ∅

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.alphaDummy001 : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_001.

Equations

• NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.alphaDummy001 = NFChoice.ReplaySupport.freshVar ∅ 1

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.alphaDummy002 : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_002.

Equations

• NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.alphaDummy002 = NFChoice.ReplaySupport.freshVar ∅ 2

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.alphaDummy003 : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_003.

Equations

• NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.alphaDummy003 = NFChoice.ReplaySupport.freshVar ∅ 3

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.alphaDummy004 : 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.SwapAlpha.alphaDummy005 (x y z w : SemanticCore.Var) : 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.SwapAlpha.alphaDummy006 : 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.SwapAlpha.alphaDummy007 : 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.SwapAlpha.alphaDummy008 (x y : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_008.

Equations

• NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.alphaDummy008 x y = NFChoice.ReplaySupport.freshVar ((NFChoice.SemanticCore.Class.cv x).fv ∪ (NFChoice.SemanticCore.Class.cv y).fv)

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.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.SwapAlpha.alphaDummy010 : 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.SwapAlpha.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.SwapAlpha.alphaDummy012 : 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.SwapAlpha.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.SwapAlpha.alphaDummy014 : 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.SwapAlpha.alphaDummy015 : 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.SwapAlpha.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.SwapAlpha.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.SwapAlpha.alphaDummy018 : 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.SwapAlpha.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.SwapAlpha.alphaDummy020 : 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.SwapAlpha.alphaDummy021 : 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.SwapAlpha.alphaDummy022 : 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.SwapAlpha.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.SwapAlpha.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.SwapAlpha.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.SwapAlpha.alphaDummy036 : 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.SwapAlpha.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.SwapAlpha.alphaDummy038 : 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.SwapAlpha.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.SwapAlpha.alphaDummy040 : 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.SwapAlpha.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.SwapAlpha.alphaDummy042 : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_042.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.alphaDummy043 : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_043.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.alphaDummy044 (z w : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_044.

Equations

• NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.alphaDummy044 z w = NFChoice.ReplaySupport.freshVar ((NFChoice.SemanticCore.Class.cv z).fv ∪ (NFChoice.SemanticCore.Class.cv w).fv)

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.alphaDummy045 (z w : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_045.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.alphaDummy046 : 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.SwapAlpha.alphaDummy047 (z w : SemanticCore.Var) : 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.SwapAlpha.alphaDummy048 : 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.SwapAlpha.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.SwapAlpha.alphaDummy050 : 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.SwapAlpha.alphaDummy051 : 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.SwapAlpha.alphaDummy052 (z w : SemanticCore.Var) : 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.SwapAlpha.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.SwapAlpha.alphaDummy054 : 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.SwapAlpha.alphaDummy055 (z w : SemanticCore.Var) : 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.SwapAlpha.alphaDummy056 : 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.SwapAlpha.alphaDummy057 : 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.SwapAlpha.alphaDummy058 : 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.SwapAlpha.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.SwapAlpha.alphaDummy060 (z w : SemanticCore.Var) : 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.SwapAlpha.alphaDummy061 (z w : SemanticCore.Var) : 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.SwapAlpha.alphaDummy072 : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_072.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.alphaDummy073 (z w : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_073.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.alphaDummy074 : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_074.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.alphaDummy075 (z w : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_075.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.alphaDummy076 : 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.SwapAlpha.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.SwapAlpha.alphaDummy078 : 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.SwapAlpha.alphaDummy079 : 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.SwapAlpha.alphaDummy080 (z w : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_080.

Equations

• NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.alphaDummy080 z w = NFChoice.ReplaySupport.freshVar ((NFChoice.SemanticCore.Class.cv w).fv ∪ (NFChoice.SemanticCore.Class.cv z).fv)

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.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.

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.alphaDummy082 : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_082.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.alphaDummy083 (z w : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_083.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.alphaDummy084 : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_084.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.alphaDummy085 (z w : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_085.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.alphaDummy086 : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_086.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.alphaDummy087 : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_087.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.alphaDummy088 (z w : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_088.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.alphaDummy089 (z w : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_089.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.alphaDummy090 : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_090.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.alphaDummy091 (z w : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_091.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.alphaDummy092 : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_092.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.alphaDummy093 : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_093.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.alphaDummy094 : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_094.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.alphaDummy095 (z w : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_095.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.alphaDummy096 (z w : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_096.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.alphaDummy097 (z w : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_097.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.alphaDummy108 : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_108.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.alphaDummy109 (z w : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_109.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.alphaDummy110 : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_110.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.alphaDummy111 (z w : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_111.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.alphaDummy112 : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_112.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.alphaDummy113 (z w : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_113.

Equations

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

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.support_mem_0000 : alphaDummy001 ∈ {alphaDummy001} ∪ {alphaDummy002} ∪ (Compiler.CompactSourceSyntax.synWex alphaDummy003 (Compiler.CompactSourceSyntax.synWex alphaDummy000 (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classEq (SemanticCore.Class.cv alphaDummy001) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv alphaDummy003) (SemanticCore.Class.cv alphaDummy000))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv alphaDummy002) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv alphaDummy000) (SemanticCore.Class.cv alphaDummy003)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.support_mem_0001 (x y z w : SemanticCore.Var) : x ∈ {x} ∪ {y} ∪ (Compiler.CompactSourceSyntax.synWex z (Compiler.CompactSourceSyntax.synWex w (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv z) (SemanticCore.Class.cv w))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv y) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv w) (SemanticCore.Class.cv z)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.support_mem_0002 : alphaDummy002 ∈ {alphaDummy001} ∪ {alphaDummy002} ∪ (Compiler.CompactSourceSyntax.synWex alphaDummy003 (Compiler.CompactSourceSyntax.synWex alphaDummy000 (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classEq (SemanticCore.Class.cv alphaDummy001) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv alphaDummy003) (SemanticCore.Class.cv alphaDummy000))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv alphaDummy002) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv alphaDummy000) (SemanticCore.Class.cv alphaDummy003)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.support_mem_0003 (x y z w : SemanticCore.Var) : y ∈ {x} ∪ {y} ∪ (Compiler.CompactSourceSyntax.synWex z (Compiler.CompactSourceSyntax.synWex w (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv z) (SemanticCore.Class.cv w))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv y) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv w) (SemanticCore.Class.cv z)))))).fv

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

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.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.SwapAlpha.support_mem_0008 : alphaDummy001 ∈ (SemanticCore.Class.cab alphaDummy006 (Compiler.CompactSourceSyntax.synWrex alphaDummy007 (SemanticCore.Class.cv alphaDummy001) (SemanticCore.Wff.classEq (SemanticCore.Class.cv alphaDummy006) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv alphaDummy007))))).fv ∪ (SemanticCore.Class.cab alphaDummy006 (Compiler.CompactSourceSyntax.synWrex alphaDummy007 (SemanticCore.Class.cv alphaDummy001) (SemanticCore.Wff.classEq (SemanticCore.Class.cv alphaDummy006) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv alphaDummy007))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.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.SwapAlpha.support_mem_0010 : alphaDummy007 ∈ (SemanticCore.Class.cv alphaDummy007).fv

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.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.SwapAlpha.support_mem_0014 : alphaDummy014 ∈ (SemanticCore.Class.cv alphaDummy014).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.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.SwapAlpha.support_mem_0016 : alphaDummy021 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv alphaDummy021) (SemanticCore.Class.cv alphaDummy022)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv alphaDummy021) (SemanticCore.Class.cv alphaDummy022)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.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.SwapAlpha.support_mem_0018 : alphaDummy021 ∈ (SemanticCore.Class.cv alphaDummy021).fv ∪ (SemanticCore.Class.cv alphaDummy022).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.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.SwapAlpha.support_mem_0020 : alphaDummy022 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv alphaDummy021) (SemanticCore.Class.cv alphaDummy022)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv alphaDummy021) (SemanticCore.Class.cv alphaDummy022)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.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.SwapAlpha.support_mem_0022 : alphaDummy022 ∈ (SemanticCore.Class.cv alphaDummy021).fv ∪ (SemanticCore.Class.cv alphaDummy022).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.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.SwapAlpha.support_mem_0024 : alphaDummy021 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv alphaDummy021)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv alphaDummy022)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.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.SwapAlpha.support_mem_0026 : alphaDummy021 ∈ (SemanticCore.Class.cv alphaDummy021).fv ∪ (SemanticCore.Class.cv alphaDummy021).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.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.SwapAlpha.support_mem_0028 : alphaDummy022 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv alphaDummy021)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv alphaDummy022)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.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.SwapAlpha.support_mem_0030 : alphaDummy022 ∈ (SemanticCore.Class.cv alphaDummy022).fv ∪ (SemanticCore.Class.cv alphaDummy022).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.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.SwapAlpha.support_mem_0032 : alphaDummy002 ∈ (SemanticCore.Class.cv alphaDummy001).fv ∪ (SemanticCore.Class.cv alphaDummy002).fv

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.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.SwapAlpha.support_mem_0036 : alphaDummy002 ∈ (SemanticCore.Class.cab alphaDummy006 (Compiler.CompactSourceSyntax.synWrex alphaDummy007 (SemanticCore.Class.cv alphaDummy002) (SemanticCore.Wff.classEq (SemanticCore.Class.cv alphaDummy006) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv alphaDummy007)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab alphaDummy006 (Compiler.CompactSourceSyntax.synWrex alphaDummy007 (SemanticCore.Class.cv alphaDummy002) (SemanticCore.Wff.classEq (SemanticCore.Class.cv alphaDummy006) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv alphaDummy007)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.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.SwapAlpha.support_mem_0038 : alphaDummy007 ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv alphaDummy007))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.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.SwapAlpha.support_mem_0040 : alphaDummy007 ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv alphaDummy007)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv alphaDummy007)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.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.SwapAlpha.support_mem_0042 : alphaDummy003 ∈ (SemanticCore.Class.cv alphaDummy003).fv ∪ (SemanticCore.Class.cv alphaDummy000).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.support_mem_0043 : alphaDummy003 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab alphaDummy042 (Compiler.CompactSourceSyntax.synWrex alphaDummy043 (SemanticCore.Class.cv alphaDummy003) (SemanticCore.Wff.classEq (SemanticCore.Class.cv alphaDummy042) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv alphaDummy043)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab alphaDummy042 (Compiler.CompactSourceSyntax.synWrex alphaDummy043 (SemanticCore.Class.cv alphaDummy000) (SemanticCore.Wff.classEq (SemanticCore.Class.cv alphaDummy042) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv alphaDummy043)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.support_mem_0045 (z w : SemanticCore.Var) : z ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (alphaDummy044 z w) (Compiler.CompactSourceSyntax.synWrex (alphaDummy045 z w) (SemanticCore.Class.cv z) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy044 z w)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy045 z w))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (alphaDummy044 z w) (Compiler.CompactSourceSyntax.synWrex (alphaDummy045 z w) (SemanticCore.Class.cv w) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy044 z w)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy045 z w))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.support_mem_0046 : alphaDummy003 ∈ (SemanticCore.Class.cab alphaDummy042 (Compiler.CompactSourceSyntax.synWrex alphaDummy043 (SemanticCore.Class.cv alphaDummy003) (SemanticCore.Wff.classEq (SemanticCore.Class.cv alphaDummy042) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv alphaDummy043))))).fv ∪ (SemanticCore.Class.cab alphaDummy042 (Compiler.CompactSourceSyntax.synWrex alphaDummy043 (SemanticCore.Class.cv alphaDummy003) (SemanticCore.Wff.classEq (SemanticCore.Class.cv alphaDummy042) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv alphaDummy043))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.support_mem_0047 (z w : SemanticCore.Var) : z ∈ (SemanticCore.Class.cab (alphaDummy044 z w) (Compiler.CompactSourceSyntax.synWrex (alphaDummy045 z w) (SemanticCore.Class.cv z) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy044 z w)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy045 z w)))))).fv ∪ (SemanticCore.Class.cab (alphaDummy044 z w) (Compiler.CompactSourceSyntax.synWrex (alphaDummy045 z w) (SemanticCore.Class.cv z) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy044 z w)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy045 z w)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.support_mem_0048 : alphaDummy043 ∈ (SemanticCore.Class.cv alphaDummy043).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.support_mem_0049 (z w : SemanticCore.Var) : alphaDummy045 z w ∈ (SemanticCore.Class.cv (alphaDummy045 z w)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.support_mem_0050 : alphaDummy050 ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv alphaDummy050) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv alphaDummy050) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv alphaDummy050).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.support_mem_0052 : alphaDummy050 ∈ (SemanticCore.Class.cv alphaDummy050).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.support_mem_0053 (z w : SemanticCore.Var) : alphaDummy052 z w ∈ (SemanticCore.Class.cv (alphaDummy052 z w)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.support_mem_0054 : alphaDummy057 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv alphaDummy057) (SemanticCore.Class.cv alphaDummy058)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv alphaDummy057) (SemanticCore.Class.cv alphaDummy058)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.support_mem_0055 (z w : SemanticCore.Var) : alphaDummy060 z w ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (alphaDummy060 z w)) (SemanticCore.Class.cv (alphaDummy061 z w))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (alphaDummy060 z w)) (SemanticCore.Class.cv (alphaDummy061 z w))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.support_mem_0056 : alphaDummy057 ∈ (SemanticCore.Class.cv alphaDummy057).fv ∪ (SemanticCore.Class.cv alphaDummy058).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.support_mem_0057 (z w : SemanticCore.Var) : alphaDummy060 z w ∈ (SemanticCore.Class.cv (alphaDummy060 z w)).fv ∪ (SemanticCore.Class.cv (alphaDummy061 z w)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.support_mem_0058 : alphaDummy058 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv alphaDummy057) (SemanticCore.Class.cv alphaDummy058)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv alphaDummy057) (SemanticCore.Class.cv alphaDummy058)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.support_mem_0059 (z w : SemanticCore.Var) : alphaDummy061 z w ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (alphaDummy060 z w)) (SemanticCore.Class.cv (alphaDummy061 z w))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (alphaDummy060 z w)) (SemanticCore.Class.cv (alphaDummy061 z w))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.support_mem_0060 : alphaDummy058 ∈ (SemanticCore.Class.cv alphaDummy057).fv ∪ (SemanticCore.Class.cv alphaDummy058).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.support_mem_0061 (z w : SemanticCore.Var) : alphaDummy061 z w ∈ (SemanticCore.Class.cv (alphaDummy060 z w)).fv ∪ (SemanticCore.Class.cv (alphaDummy061 z w)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.support_mem_0062 : alphaDummy057 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv alphaDummy057)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv alphaDummy058)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.support_mem_0063 (z w : SemanticCore.Var) : alphaDummy060 z w ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (alphaDummy060 z w))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (alphaDummy061 z w))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.support_mem_0064 : alphaDummy057 ∈ (SemanticCore.Class.cv alphaDummy057).fv ∪ (SemanticCore.Class.cv alphaDummy057).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.support_mem_0065 (z w : SemanticCore.Var) : alphaDummy060 z w ∈ (SemanticCore.Class.cv (alphaDummy060 z w)).fv ∪ (SemanticCore.Class.cv (alphaDummy060 z w)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.support_mem_0066 : alphaDummy058 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv alphaDummy057)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv alphaDummy058)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.support_mem_0067 (z w : SemanticCore.Var) : alphaDummy061 z w ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (alphaDummy060 z w))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (alphaDummy061 z w))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.support_mem_0068 : alphaDummy058 ∈ (SemanticCore.Class.cv alphaDummy058).fv ∪ (SemanticCore.Class.cv alphaDummy058).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.support_mem_0070 : alphaDummy000 ∈ (SemanticCore.Class.cv alphaDummy003).fv ∪ (SemanticCore.Class.cv alphaDummy000).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.support_mem_0071 : alphaDummy000 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab alphaDummy042 (Compiler.CompactSourceSyntax.synWrex alphaDummy043 (SemanticCore.Class.cv alphaDummy003) (SemanticCore.Wff.classEq (SemanticCore.Class.cv alphaDummy042) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv alphaDummy043)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab alphaDummy042 (Compiler.CompactSourceSyntax.synWrex alphaDummy043 (SemanticCore.Class.cv alphaDummy000) (SemanticCore.Wff.classEq (SemanticCore.Class.cv alphaDummy042) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv alphaDummy043)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.support_mem_0073 (z w : SemanticCore.Var) : w ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (alphaDummy044 z w) (Compiler.CompactSourceSyntax.synWrex (alphaDummy045 z w) (SemanticCore.Class.cv z) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy044 z w)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy045 z w))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (alphaDummy044 z w) (Compiler.CompactSourceSyntax.synWrex (alphaDummy045 z w) (SemanticCore.Class.cv w) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy044 z w)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy045 z w))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.support_mem_0074 : alphaDummy000 ∈ (SemanticCore.Class.cab alphaDummy042 (Compiler.CompactSourceSyntax.synWrex alphaDummy043 (SemanticCore.Class.cv alphaDummy000) (SemanticCore.Wff.classEq (SemanticCore.Class.cv alphaDummy042) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv alphaDummy043)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab alphaDummy042 (Compiler.CompactSourceSyntax.synWrex alphaDummy043 (SemanticCore.Class.cv alphaDummy000) (SemanticCore.Wff.classEq (SemanticCore.Class.cv alphaDummy042) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv alphaDummy043)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.support_mem_0075 (z w : SemanticCore.Var) : w ∈ (SemanticCore.Class.cab (alphaDummy044 z w) (Compiler.CompactSourceSyntax.synWrex (alphaDummy045 z w) (SemanticCore.Class.cv w) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy044 z w)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy045 z w))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (alphaDummy044 z w) (Compiler.CompactSourceSyntax.synWrex (alphaDummy045 z w) (SemanticCore.Class.cv w) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy044 z w)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy045 z w))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.support_mem_0076 : alphaDummy043 ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv alphaDummy043))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.support_mem_0077 (z w : SemanticCore.Var) : alphaDummy045 z w ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy045 z w)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.support_mem_0078 : alphaDummy043 ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv alphaDummy043)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv alphaDummy043)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.support_mem_0079 (z w : SemanticCore.Var) : alphaDummy045 z w ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy045 z w))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy045 z w))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.support_mem_0080 : alphaDummy000 ∈ (SemanticCore.Class.cv alphaDummy000).fv ∪ (SemanticCore.Class.cv alphaDummy003).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.support_mem_0081 : alphaDummy000 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab alphaDummy078 (Compiler.CompactSourceSyntax.synWrex alphaDummy079 (SemanticCore.Class.cv alphaDummy000) (SemanticCore.Wff.classEq (SemanticCore.Class.cv alphaDummy078) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv alphaDummy079)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab alphaDummy078 (Compiler.CompactSourceSyntax.synWrex alphaDummy079 (SemanticCore.Class.cv alphaDummy003) (SemanticCore.Wff.classEq (SemanticCore.Class.cv alphaDummy078) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv alphaDummy079)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.support_mem_0083 (z w : SemanticCore.Var) : w ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (alphaDummy080 z w) (Compiler.CompactSourceSyntax.synWrex (alphaDummy081 z w) (SemanticCore.Class.cv w) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy080 z w)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy081 z w))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (alphaDummy080 z w) (Compiler.CompactSourceSyntax.synWrex (alphaDummy081 z w) (SemanticCore.Class.cv z) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy080 z w)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy081 z w))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.support_mem_0084 : alphaDummy000 ∈ (SemanticCore.Class.cab alphaDummy078 (Compiler.CompactSourceSyntax.synWrex alphaDummy079 (SemanticCore.Class.cv alphaDummy000) (SemanticCore.Wff.classEq (SemanticCore.Class.cv alphaDummy078) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv alphaDummy079))))).fv ∪ (SemanticCore.Class.cab alphaDummy078 (Compiler.CompactSourceSyntax.synWrex alphaDummy079 (SemanticCore.Class.cv alphaDummy000) (SemanticCore.Wff.classEq (SemanticCore.Class.cv alphaDummy078) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv alphaDummy079))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.support_mem_0085 (z w : SemanticCore.Var) : w ∈ (SemanticCore.Class.cab (alphaDummy080 z w) (Compiler.CompactSourceSyntax.synWrex (alphaDummy081 z w) (SemanticCore.Class.cv w) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy080 z w)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy081 z w)))))).fv ∪ (SemanticCore.Class.cab (alphaDummy080 z w) (Compiler.CompactSourceSyntax.synWrex (alphaDummy081 z w) (SemanticCore.Class.cv w) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy080 z w)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy081 z w)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.support_mem_0086 : alphaDummy079 ∈ (SemanticCore.Class.cv alphaDummy079).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.support_mem_0087 (z w : SemanticCore.Var) : alphaDummy081 z w ∈ (SemanticCore.Class.cv (alphaDummy081 z w)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.support_mem_0088 : alphaDummy086 ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv alphaDummy086) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv alphaDummy086) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv alphaDummy086).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.support_mem_0090 : alphaDummy086 ∈ (SemanticCore.Class.cv alphaDummy086).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.support_mem_0091 (z w : SemanticCore.Var) : alphaDummy088 z w ∈ (SemanticCore.Class.cv (alphaDummy088 z w)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.support_mem_0092 : alphaDummy093 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv alphaDummy093) (SemanticCore.Class.cv alphaDummy094)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv alphaDummy093) (SemanticCore.Class.cv alphaDummy094)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.support_mem_0093 (z w : SemanticCore.Var) : alphaDummy096 z w ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (alphaDummy096 z w)) (SemanticCore.Class.cv (alphaDummy097 z w))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (alphaDummy096 z w)) (SemanticCore.Class.cv (alphaDummy097 z w))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.support_mem_0094 : alphaDummy093 ∈ (SemanticCore.Class.cv alphaDummy093).fv ∪ (SemanticCore.Class.cv alphaDummy094).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.support_mem_0095 (z w : SemanticCore.Var) : alphaDummy096 z w ∈ (SemanticCore.Class.cv (alphaDummy096 z w)).fv ∪ (SemanticCore.Class.cv (alphaDummy097 z w)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.support_mem_0096 : alphaDummy094 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv alphaDummy093) (SemanticCore.Class.cv alphaDummy094)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv alphaDummy093) (SemanticCore.Class.cv alphaDummy094)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.support_mem_0097 (z w : SemanticCore.Var) : alphaDummy097 z w ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (alphaDummy096 z w)) (SemanticCore.Class.cv (alphaDummy097 z w))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (alphaDummy096 z w)) (SemanticCore.Class.cv (alphaDummy097 z w))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.support_mem_0098 : alphaDummy094 ∈ (SemanticCore.Class.cv alphaDummy093).fv ∪ (SemanticCore.Class.cv alphaDummy094).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.support_mem_0099 (z w : SemanticCore.Var) : alphaDummy097 z w ∈ (SemanticCore.Class.cv (alphaDummy096 z w)).fv ∪ (SemanticCore.Class.cv (alphaDummy097 z w)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.support_mem_0100 : alphaDummy093 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv alphaDummy093)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv alphaDummy094)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.support_mem_0101 (z w : SemanticCore.Var) : alphaDummy096 z w ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (alphaDummy096 z w))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (alphaDummy097 z w))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.support_mem_0102 : alphaDummy093 ∈ (SemanticCore.Class.cv alphaDummy093).fv ∪ (SemanticCore.Class.cv alphaDummy093).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.support_mem_0103 (z w : SemanticCore.Var) : alphaDummy096 z w ∈ (SemanticCore.Class.cv (alphaDummy096 z w)).fv ∪ (SemanticCore.Class.cv (alphaDummy096 z w)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.support_mem_0104 : alphaDummy094 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv alphaDummy093)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv alphaDummy094)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.support_mem_0105 (z w : SemanticCore.Var) : alphaDummy097 z w ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (alphaDummy096 z w))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (alphaDummy097 z w))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.support_mem_0106 : alphaDummy094 ∈ (SemanticCore.Class.cv alphaDummy094).fv ∪ (SemanticCore.Class.cv alphaDummy094).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.support_mem_0107 (z w : SemanticCore.Var) : alphaDummy097 z w ∈ (SemanticCore.Class.cv (alphaDummy097 z w)).fv ∪ (SemanticCore.Class.cv (alphaDummy097 z w)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.support_mem_0108 : alphaDummy003 ∈ (SemanticCore.Class.cv alphaDummy000).fv ∪ (SemanticCore.Class.cv alphaDummy003).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.support_mem_0109 : alphaDummy003 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab alphaDummy078 (Compiler.CompactSourceSyntax.synWrex alphaDummy079 (SemanticCore.Class.cv alphaDummy000) (SemanticCore.Wff.classEq (SemanticCore.Class.cv alphaDummy078) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv alphaDummy079)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab alphaDummy078 (Compiler.CompactSourceSyntax.synWrex alphaDummy079 (SemanticCore.Class.cv alphaDummy003) (SemanticCore.Wff.classEq (SemanticCore.Class.cv alphaDummy078) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv alphaDummy079)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.support_mem_0111 (z w : SemanticCore.Var) : z ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (alphaDummy080 z w) (Compiler.CompactSourceSyntax.synWrex (alphaDummy081 z w) (SemanticCore.Class.cv w) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy080 z w)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy081 z w))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (alphaDummy080 z w) (Compiler.CompactSourceSyntax.synWrex (alphaDummy081 z w) (SemanticCore.Class.cv z) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy080 z w)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy081 z w))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.support_mem_0112 : alphaDummy003 ∈ (SemanticCore.Class.cab alphaDummy078 (Compiler.CompactSourceSyntax.synWrex alphaDummy079 (SemanticCore.Class.cv alphaDummy003) (SemanticCore.Wff.classEq (SemanticCore.Class.cv alphaDummy078) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv alphaDummy079)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab alphaDummy078 (Compiler.CompactSourceSyntax.synWrex alphaDummy079 (SemanticCore.Class.cv alphaDummy003) (SemanticCore.Wff.classEq (SemanticCore.Class.cv alphaDummy078) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv alphaDummy079)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.support_mem_0113 (z w : SemanticCore.Var) : z ∈ (SemanticCore.Class.cab (alphaDummy080 z w) (Compiler.CompactSourceSyntax.synWrex (alphaDummy081 z w) (SemanticCore.Class.cv z) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy080 z w)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy081 z w))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (alphaDummy080 z w) (Compiler.CompactSourceSyntax.synWrex (alphaDummy081 z w) (SemanticCore.Class.cv z) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy080 z w)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy081 z w))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.support_mem_0114 : alphaDummy079 ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv alphaDummy079))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.support_mem_0115 (z w : SemanticCore.Var) : alphaDummy081 z w ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy081 z w)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.support_mem_0116 : alphaDummy079 ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv alphaDummy079)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv alphaDummy079)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SwapAlpha.support_mem_0117 (z w : SemanticCore.Var) : alphaDummy081 z w ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy081 z w))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy081 z w))).fv