Freshness and support lemmas for finite-type alpha renaming.

Shared freshness facts and the four alpha-certificate subtrees for finite types.

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FiniteTypeAlpha.alphaDummy000 (M : SemanticCore.Class) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_000.

Equations

• NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FiniteTypeAlpha.alphaDummy000 M = NFChoice.ReplaySupport.freshVar M.fv

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FiniteTypeAlpha.alphaDummy001 (M : SemanticCore.Class) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_001.

Equations

• NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FiniteTypeAlpha.alphaDummy001 M = NFChoice.ReplaySupport.freshVar M.fv 1

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FiniteTypeAlpha.alphaDummy002 (M : SemanticCore.Class) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_002.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FiniteTypeAlpha.alphaDummy003 (n : SemanticCore.Var) (M : SemanticCore.Class) (a : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_003.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FiniteTypeAlpha.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.FiniteTypeAlpha.alphaDummy005 : 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.FiniteTypeAlpha.alphaDummy006 : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_006.

Equations

• NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FiniteTypeAlpha.alphaDummy006 = NFChoice.ReplaySupport.freshVar ∅

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FiniteTypeAlpha.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.FiniteTypeAlpha.alphaDummy008 (M : SemanticCore.Class) : 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.FiniteTypeAlpha.alphaDummy009 (n : SemanticCore.Var) (M : SemanticCore.Class) (a : 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.FiniteTypeAlpha.alphaDummy010 (M : 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.FiniteTypeAlpha.alphaDummy011 (M : SemanticCore.Class) : 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.FiniteTypeAlpha.alphaDummy012 (n : SemanticCore.Var) (M : SemanticCore.Class) (a : SemanticCore.Var) : 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.FiniteTypeAlpha.alphaDummy013 (n : SemanticCore.Var) (M : SemanticCore.Class) (a : 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.FiniteTypeAlpha.alphaDummy014 : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_014.

Equations

• NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FiniteTypeAlpha.alphaDummy014 = NFChoice.ReplaySupport.freshVar ∅ 1

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FiniteTypeAlpha.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.FiniteTypeAlpha.alphaDummy016 : 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.FiniteTypeAlpha.alphaDummy017 : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_017.

Equations

• NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FiniteTypeAlpha.alphaDummy017 = NFChoice.ReplaySupport.freshVar NFChoice.Compiler.CompactSourceSyntax.synC0.fv

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FiniteTypeAlpha.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.FiniteTypeAlpha.alphaDummy019 : 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.FiniteTypeAlpha.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.FiniteTypeAlpha.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.FiniteTypeAlpha.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.FiniteTypeAlpha.alphaDummy023 : 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.FiniteTypeAlpha.alphaDummy024 : 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.FiniteTypeAlpha.alphaDummy025 : 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.FiniteTypeAlpha.alphaDummy026 : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_026.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FiniteTypeAlpha.alphaDummy027 (M : SemanticCore.Class) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_027.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FiniteTypeAlpha.alphaDummy028 (a : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_028.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FiniteTypeAlpha.alphaDummy029 (M : SemanticCore.Class) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_029.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FiniteTypeAlpha.alphaDummy030 (a : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_030.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FiniteTypeAlpha.alphaDummy031 (M : SemanticCore.Class) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_031.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FiniteTypeAlpha.alphaDummy032 (a : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_032.

Equations

• NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FiniteTypeAlpha.alphaDummy032 a = NFChoice.ReplaySupport.freshVar (NFChoice.SemanticCore.Class.cv a).fv

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FiniteTypeAlpha.alphaDummy033 (M : SemanticCore.Class) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_033.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FiniteTypeAlpha.alphaDummy034 (a : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_034.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FiniteTypeAlpha.alphaDummy035 (M : SemanticCore.Class) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_035.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FiniteTypeAlpha.alphaDummy036 (a : SemanticCore.Var) : 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.FiniteTypeAlpha.alphaDummy037 (M : SemanticCore.Class) : 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.FiniteTypeAlpha.alphaDummy038 (n : SemanticCore.Var) (M : SemanticCore.Class) (a : SemanticCore.Var) : 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.

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FiniteTypeAlpha.fresh_003 (M : SemanticCore.Class) : alphaDummy010 M ∉ (SemanticCore.Class.cab (alphaDummy008 M) (SemanticCore.Wff.classEq (SemanticCore.Class.cab (alphaDummy001 M) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (alphaDummy001 M)) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synWrex (alphaDummy000 M) M (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCpw1 (SemanticCore.Class.cv (alphaDummy000 M))) (SemanticCore.Class.cv (alphaDummy001 M)))))) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (alphaDummy008 M))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FiniteTypeAlpha.fresh_004 (M : SemanticCore.Class) : alphaDummy011 M ∉ (SemanticCore.Class.cab (alphaDummy008 M) (SemanticCore.Wff.classEq (SemanticCore.Class.cab (alphaDummy001 M) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (alphaDummy001 M)) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synWrex (alphaDummy000 M) M (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCpw1 (SemanticCore.Class.cv (alphaDummy000 M))) (SemanticCore.Class.cv (alphaDummy001 M)))))) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (alphaDummy008 M))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FiniteTypeAlpha.fresh_006 (n : SemanticCore.Var) (M : SemanticCore.Class) (a : SemanticCore.Var) : alphaDummy012 n M a ∉ (SemanticCore.Class.cab (alphaDummy009 n M a) (SemanticCore.Wff.classEq (SemanticCore.Class.cab n (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv n) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synWrex a M (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCpw1 (SemanticCore.Class.cv a)) (SemanticCore.Class.cv n))))) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (alphaDummy009 n M a))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FiniteTypeAlpha.fresh_007 (n : SemanticCore.Var) (M : SemanticCore.Class) (a : SemanticCore.Var) : alphaDummy013 n M a ∉ (SemanticCore.Class.cab (alphaDummy009 n M a) (SemanticCore.Wff.classEq (SemanticCore.Class.cab n (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv n) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synWrex a M (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCpw1 (SemanticCore.Class.cv a)) (SemanticCore.Class.cv n))))) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (alphaDummy009 n M a))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FiniteTypeAlpha.fresh_025 (M : SemanticCore.Class) : alphaDummy002 M ∉ (SemanticCore.Wff.classEq M Compiler.CompactSourceSyntax.synC0).fv ∪ Compiler.CompactSourceSyntax.synC0.fv ∪ (Compiler.CompactSourceSyntax.synCio (alphaDummy001 M) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (alphaDummy001 M)) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synWrex (alphaDummy000 M) M (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCpw1 (SemanticCore.Class.cv (alphaDummy000 M))) (SemanticCore.Class.cv (alphaDummy001 M)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FiniteTypeAlpha.fresh_026 (n : SemanticCore.Var) (M : SemanticCore.Class) (a : SemanticCore.Var) : alphaDummy003 n M a ∉ (SemanticCore.Wff.classEq M Compiler.CompactSourceSyntax.synC0).fv ∪ Compiler.CompactSourceSyntax.synC0.fv ∪ (Compiler.CompactSourceSyntax.synCio n (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv n) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synWrex a M (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCpw1 (SemanticCore.Class.cv a)) (SemanticCore.Class.cv n))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FiniteTypeAlpha.fresh_039 (M : SemanticCore.Class) : alphaDummy000 M ∉ M.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FiniteTypeAlpha.fresh_040 (M : SemanticCore.Class) : alphaDummy001 M ∉ M.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FiniteTypeAlpha.fresh_042 (M : SemanticCore.Class) : alphaDummy008 M ∉ {alphaDummy001 M} ∪ (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (alphaDummy001 M)) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synWrex (alphaDummy000 M) M (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCpw1 (SemanticCore.Class.cv (alphaDummy000 M))) (SemanticCore.Class.cv (alphaDummy001 M))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FiniteTypeAlpha.fresh_043 (n : SemanticCore.Var) (M : SemanticCore.Class) (a : SemanticCore.Var) : alphaDummy009 n M a ∉ {n} ∪ (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv n) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synWrex a M (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCpw1 (SemanticCore.Class.cv a)) (SemanticCore.Class.cv n)))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FiniteTypeAlpha.support_part_0000 : alphaDummy014 ∈ (SemanticCore.Class.cv alphaDummy014).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FiniteTypeAlpha.support_mem_0000 : alphaDummy014 ∈ (SemanticCore.Class.cv alphaDummy014).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FiniteTypeAlpha.support_part_0001 : alphaDummy014 ∈ (SemanticCore.Class.cv alphaDummy014).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FiniteTypeAlpha.support_mem_0001 : alphaDummy014 ∈ (SemanticCore.Class.cv alphaDummy014).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FiniteTypeAlpha.support_part_0002 : alphaDummy019 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv alphaDummy019) (SemanticCore.Class.cv alphaDummy020)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FiniteTypeAlpha.support_mem_0002 : alphaDummy019 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv alphaDummy019) (SemanticCore.Class.cv alphaDummy020)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv alphaDummy019) (SemanticCore.Class.cv alphaDummy020)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FiniteTypeAlpha.support_part_0003 : alphaDummy019 ∈ (SemanticCore.Class.cv alphaDummy019).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FiniteTypeAlpha.support_mem_0003 : alphaDummy019 ∈ (SemanticCore.Class.cv alphaDummy019).fv ∪ (SemanticCore.Class.cv alphaDummy020).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FiniteTypeAlpha.support_part_0004 : alphaDummy020 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv alphaDummy019) (SemanticCore.Class.cv alphaDummy020)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FiniteTypeAlpha.support_mem_0004 : alphaDummy020 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv alphaDummy019) (SemanticCore.Class.cv alphaDummy020)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv alphaDummy019) (SemanticCore.Class.cv alphaDummy020)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FiniteTypeAlpha.support_part_0005 : alphaDummy020 ∈ (SemanticCore.Class.cv alphaDummy020).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FiniteTypeAlpha.support_mem_0005 : alphaDummy020 ∈ (SemanticCore.Class.cv alphaDummy019).fv ∪ (SemanticCore.Class.cv alphaDummy020).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FiniteTypeAlpha.support_part_0006 : alphaDummy019 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv alphaDummy019)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FiniteTypeAlpha.support_mem_0006 : alphaDummy019 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv alphaDummy019)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv alphaDummy020)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FiniteTypeAlpha.support_part_0007 : alphaDummy019 ∈ (SemanticCore.Class.cv alphaDummy019).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FiniteTypeAlpha.support_mem_0007 : alphaDummy019 ∈ (SemanticCore.Class.cv alphaDummy019).fv ∪ (SemanticCore.Class.cv alphaDummy019).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FiniteTypeAlpha.support_part_0008 : alphaDummy020 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv alphaDummy020)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FiniteTypeAlpha.support_mem_0008 : alphaDummy020 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv alphaDummy019)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv alphaDummy020)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FiniteTypeAlpha.support_part_0009 : alphaDummy020 ∈ (SemanticCore.Class.cv alphaDummy020).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FiniteTypeAlpha.support_mem_0009 : alphaDummy020 ∈ (SemanticCore.Class.cv alphaDummy020).fv ∪ (SemanticCore.Class.cv alphaDummy020).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FiniteTypeAlpha.support_part_0010 (M : SemanticCore.Class) : alphaDummy031 M ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (alphaDummy031 M)) (SemanticCore.Class.cv (alphaDummy000 M))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FiniteTypeAlpha.support_mem_0010 (M : SemanticCore.Class) : alphaDummy031 M ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (alphaDummy031 M)) (SemanticCore.Class.cv (alphaDummy000 M))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (alphaDummy031 M)) (SemanticCore.Class.cv (alphaDummy000 M))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FiniteTypeAlpha.support_part_0011 (a : SemanticCore.Var) : alphaDummy032 a ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (alphaDummy032 a)) (SemanticCore.Class.cv a)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FiniteTypeAlpha.support_mem_0011 (a : SemanticCore.Var) : alphaDummy032 a ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (alphaDummy032 a)) (SemanticCore.Class.cv a)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (alphaDummy032 a)) (SemanticCore.Class.cv a)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FiniteTypeAlpha.support_part_0012 (M : SemanticCore.Class) : alphaDummy031 M ∈ (SemanticCore.Class.cv (alphaDummy031 M)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FiniteTypeAlpha.support_mem_0012 (M : SemanticCore.Class) : alphaDummy031 M ∈ (SemanticCore.Class.cv (alphaDummy031 M)).fv ∪ (SemanticCore.Class.cv (alphaDummy000 M)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FiniteTypeAlpha.support_part_0013 (a : SemanticCore.Var) : alphaDummy032 a ∈ (SemanticCore.Class.cv (alphaDummy032 a)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FiniteTypeAlpha.support_mem_0013 (a : SemanticCore.Var) : alphaDummy032 a ∈ (SemanticCore.Class.cv (alphaDummy032 a)).fv ∪ (SemanticCore.Class.cv a).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FiniteTypeAlpha.support_part_0014 (M : SemanticCore.Class) : alphaDummy000 M ∈ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCpw (SemanticCore.Class.cv (alphaDummy000 M))) Compiler.CompactSourceSyntax.synC1c).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FiniteTypeAlpha.support_mem_0014 (M : SemanticCore.Class) : alphaDummy000 M ∈ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCpw (SemanticCore.Class.cv (alphaDummy000 M))) Compiler.CompactSourceSyntax.synC1c).fv ∪ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCpw (SemanticCore.Class.cv (alphaDummy000 M))) Compiler.CompactSourceSyntax.synC1c).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FiniteTypeAlpha.support_part_0015 (a : SemanticCore.Var) : a ∈ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCpw (SemanticCore.Class.cv a)) Compiler.CompactSourceSyntax.synC1c).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FiniteTypeAlpha.support_mem_0015 (a : SemanticCore.Var) : a ∈ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCpw (SemanticCore.Class.cv a)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCpw (SemanticCore.Class.cv a)) Compiler.CompactSourceSyntax.synC1c).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FiniteTypeAlpha.support_part_0016 (M : SemanticCore.Class) : alphaDummy000 M ∈ (Compiler.CompactSourceSyntax.synCpw (SemanticCore.Class.cv (alphaDummy000 M))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FiniteTypeAlpha.support_mem_0016 (M : SemanticCore.Class) : alphaDummy000 M ∈ (Compiler.CompactSourceSyntax.synCpw (SemanticCore.Class.cv (alphaDummy000 M))).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FiniteTypeAlpha.support_part_0017 (a : SemanticCore.Var) : a ∈ (Compiler.CompactSourceSyntax.synCpw (SemanticCore.Class.cv a)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FiniteTypeAlpha.support_mem_0017 (a : SemanticCore.Var) : a ∈ (Compiler.CompactSourceSyntax.synCpw (SemanticCore.Class.cv a)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FiniteTypeAlpha.support_part_0018 (M : SemanticCore.Class) : alphaDummy000 M ∈ (SemanticCore.Class.cv (alphaDummy000 M)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FiniteTypeAlpha.support_mem_0018 (M : SemanticCore.Class) : alphaDummy000 M ∈ (SemanticCore.Class.cv (alphaDummy000 M)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FiniteTypeAlpha.support_part_0019 (a : SemanticCore.Var) : a ∈ (SemanticCore.Class.cv a).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FiniteTypeAlpha.support_mem_0019 (a : SemanticCore.Var) : a ∈ (SemanticCore.Class.cv a).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FiniteTypeAlpha.support_part_0020 (M : SemanticCore.Class) : alphaDummy000 M ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (alphaDummy031 M)) (SemanticCore.Class.cv (alphaDummy000 M))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FiniteTypeAlpha.support_mem_0020 (M : SemanticCore.Class) : alphaDummy000 M ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (alphaDummy031 M)) (SemanticCore.Class.cv (alphaDummy000 M))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (alphaDummy031 M)) (SemanticCore.Class.cv (alphaDummy000 M))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FiniteTypeAlpha.support_part_0021 (a : SemanticCore.Var) : a ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (alphaDummy032 a)) (SemanticCore.Class.cv a)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FiniteTypeAlpha.support_mem_0021 (a : SemanticCore.Var) : a ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (alphaDummy032 a)) (SemanticCore.Class.cv a)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (alphaDummy032 a)) (SemanticCore.Class.cv a)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FiniteTypeAlpha.support_part_0022 (M : SemanticCore.Class) : alphaDummy000 M ∈ (SemanticCore.Class.cv (alphaDummy000 M)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FiniteTypeAlpha.support_mem_0022 (M : SemanticCore.Class) : alphaDummy000 M ∈ (SemanticCore.Class.cv (alphaDummy031 M)).fv ∪ (SemanticCore.Class.cv (alphaDummy000 M)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FiniteTypeAlpha.support_part_0023 (a : SemanticCore.Var) : a ∈ (SemanticCore.Class.cv a).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FiniteTypeAlpha.support_mem_0023 (a : SemanticCore.Var) : a ∈ (SemanticCore.Class.cv (alphaDummy032 a)).fv ∪ (SemanticCore.Class.cv a).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FiniteTypeAlpha.support_part_0024 (M : SemanticCore.Class) : alphaDummy008 M ∈ (SemanticCore.Class.cv (alphaDummy008 M)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FiniteTypeAlpha.support_mem_0024 (M : SemanticCore.Class) : alphaDummy008 M ∈ (SemanticCore.Class.cv (alphaDummy008 M)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FiniteTypeAlpha.support_part_0025 (n : SemanticCore.Var) (M : SemanticCore.Class) (a : SemanticCore.Var) : alphaDummy009 n M a ∈ (SemanticCore.Class.cv (alphaDummy009 n M a)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FiniteTypeAlpha.support_mem_0025 (n : SemanticCore.Var) (M : SemanticCore.Class) (a : SemanticCore.Var) : alphaDummy009 n M a ∈ (SemanticCore.Class.cv (alphaDummy009 n M a)).fv

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FiniteTypeAlpha.finitePredicate (n : SemanticCore.Var) (M : SemanticCore.Class) (a : SemanticCore.Var) : SemanticCore.Wff

Predicate whose restricted existential retains every free parameter variable.

Equations

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

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FiniteTypeAlpha.codingClass (outer n : SemanticCore.Var) (M : SemanticCore.Class) (a : SemanticCore.Var) : SemanticCore.Class

The singleton-encoding class used in the finite-type alpha certificate.

Equations

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FiniteTypeAlpha.parameter_subset_predicate (n : SemanticCore.Var) (M : SemanticCore.Class) (a : SemanticCore.Var) (ha : a ∉ M.fv) : M.fv ⊆ (finitePredicate n M a).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FiniteTypeAlpha.parameter_subset_codingClass (outer n : SemanticCore.Var) (M : SemanticCore.Class) (a : SemanticCore.Var) (ha : a ∉ M.fv) (hn : n ∉ M.fv) (houter : outer ∉ {n} ∪ (finitePredicate n M a).fv) : M.fv ⊆ (codingClass outer n M a).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FiniteTypeAlpha.outerVariablesFresh (n : SemanticCore.Var) (M : SemanticCore.Class) (a : SemanticCore.Var) : Nominal.TEnvFresh [(alphaDummy002 M, alphaDummy003 n M a)] M.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.FiniteTypeAlpha.allVariablesFresh (n : SemanticCore.Var) (M : SemanticCore.Class) (a : SemanticCore.Var) (ha : a ∉ M.fv) (hn : n ∉ M.fv) : Nominal.TEnvFresh [(alphaDummy000 M, a), (alphaDummy001 M, n), (alphaDummy008 M, alphaDummy009 n M a), (alphaDummy011 M, alphaDummy013 n M a), (alphaDummy010 M, alphaDummy012 n M a), (alphaDummy002 M, alphaDummy003 n M a)] M.fv