LeanPool.NFWeakPartition.Certificates.NAPD051C001Block001

Nominal proof certificates grouped in dependency order.

Certificates from NAPD051C001Part001.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051AlphaDummy000 (x y : SemanticCore.Var) (A B C : SemanticCore.Class) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb051_alpha_dummy_000.

Equations

NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051AlphaDummy000 x y A B C = NFChoice.ReplaySupport.freshVar ({x} ∪ A.fv ∪ {y} ∪ B.fv ∪ C.fv)

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051AlphaDummy001 (x y : SemanticCore.Var) (A B C : SemanticCore.Class) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb051_alpha_dummy_001.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051AlphaDummy002 (x y z : SemanticCore.Var) (A B C : SemanticCore.Class) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb051_alpha_dummy_002.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051AlphaDummy003 (x y : SemanticCore.Var) (A B C : SemanticCore.Class) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb051_alpha_dummy_003.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051AlphaDummy004 (x y : SemanticCore.Var) (A B C : SemanticCore.Class) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb051_alpha_dummy_004.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051AlphaDummy005 (x y z : SemanticCore.Var) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb051_alpha_dummy_005.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051AlphaDummy006 (x y z : SemanticCore.Var) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb051_alpha_dummy_006.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051AlphaDummy007 (x y : SemanticCore.Var) (A B C : SemanticCore.Class) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb051_alpha_dummy_007.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051AlphaDummy008 (x y z : SemanticCore.Var) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb051_alpha_dummy_008.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051AlphaDummy009 (x y : SemanticCore.Var) (A B C : SemanticCore.Class) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb051_alpha_dummy_009.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051AlphaDummy010 (x y z : SemanticCore.Var) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb051_alpha_dummy_010.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051AlphaDummy011 (x y : SemanticCore.Var) (A B C : SemanticCore.Class) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb051_alpha_dummy_011.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051AlphaDummy012 (x y : SemanticCore.Var) (A B C : SemanticCore.Class) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb051_alpha_dummy_012.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051AlphaDummy013 (x y z : SemanticCore.Var) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb051_alpha_dummy_013.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051AlphaDummy014 (x y z : SemanticCore.Var) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb051_alpha_dummy_014.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051AlphaDummy015 (x y : SemanticCore.Var) (A B C : SemanticCore.Class) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb051_alpha_dummy_015.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051AlphaDummy016 (x y z : SemanticCore.Var) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb051_alpha_dummy_016.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051AlphaDummy017 (x y : SemanticCore.Var) (A B C : SemanticCore.Class) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb051_alpha_dummy_017.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051AlphaDummy018 (x y : SemanticCore.Var) (A B C : SemanticCore.Class) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb051_alpha_dummy_018.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051AlphaDummy019 (x y : SemanticCore.Var) (A B C : SemanticCore.Class) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb051_alpha_dummy_019.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051AlphaDummy020 (x y z : SemanticCore.Var) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb051_alpha_dummy_020.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051AlphaDummy021 (x y z : SemanticCore.Var) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb051_alpha_dummy_021.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051AlphaDummy022 (x y z : SemanticCore.Var) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb051_alpha_dummy_022.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051AlphaDummy023 (x y : SemanticCore.Var) (A B C : SemanticCore.Class) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb051_alpha_dummy_023.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051AlphaDummy024 (x y z : SemanticCore.Var) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb051_alpha_dummy_024.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051AlphaDummy025 (x y : SemanticCore.Var) (A B C : SemanticCore.Class) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb051_alpha_dummy_025.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051AlphaDummy026 (x y z : SemanticCore.Var) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb051_alpha_dummy_026.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051AlphaDummy027 (x y : SemanticCore.Var) (A B C : SemanticCore.Class) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb051_alpha_dummy_027.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051AlphaDummy028 (x y z : SemanticCore.Var) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb051_alpha_dummy_028.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051AlphaDummy029 (x y : SemanticCore.Var) (A B C : SemanticCore.Class) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb051_alpha_dummy_029.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051AlphaDummy030 (x y z : SemanticCore.Var) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb051_alpha_dummy_030.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051AlphaDummy031 (x y : SemanticCore.Var) (A B C : SemanticCore.Class) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb051_alpha_dummy_031.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051AlphaDummy032 (x y z : SemanticCore.Var) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb051_alpha_dummy_032.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051AlphaDummy033 (x y : SemanticCore.Var) (A B C : SemanticCore.Class) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb051_alpha_dummy_033.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051AlphaDummy034 (x y z : SemanticCore.Var) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb051_alpha_dummy_034.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051AlphaDummy035 (x y : SemanticCore.Var) (A B C : SemanticCore.Class) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb051_alpha_dummy_035.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051AlphaDummy036 (x y z : SemanticCore.Var) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb051_alpha_dummy_036.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051AlphaDummy037 (x y : SemanticCore.Var) (A B C : SemanticCore.Class) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb051_alpha_dummy_037.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051AlphaDummy038 (x y z : SemanticCore.Var) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb051_alpha_dummy_038.

Equations

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

Instances For

Certificates from NAPD051C001Part002.

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_fresh_000 (x y : SemanticCore.Var) (A B C : SemanticCore.Class) :

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_fresh_001 (x y : SemanticCore.Var) (A B C : SemanticCore.Class) :

nb051AlphaDummy009 x y A B C ∉ (SemanticCore.Class.cab (nb051AlphaDummy003 x y A B C) (Compiler.CompactSourceSyntax.synWrex (nb051AlphaDummy004 x y A B C) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb051AlphaDummy003 x y A B C)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb051AlphaDummy004 x y A B C)))))).fv ∪ (SemanticCore.Class.cab (nb051AlphaDummy003 x y A B C) (Compiler.CompactSourceSyntax.synWrex (nb051AlphaDummy004 x y A B C) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb051AlphaDummy003 x y A B C)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb051AlphaDummy004 x y A B C)))))).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_fresh_002 (x y z : SemanticCore.Var) :

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_fresh_003 (x y z : SemanticCore.Var) :

nb051AlphaDummy010 x y z ∉ (SemanticCore.Class.cab (nb051AlphaDummy005 x y z) (Compiler.CompactSourceSyntax.synWrex (nb051AlphaDummy006 x y z) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb051AlphaDummy005 x y z)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb051AlphaDummy006 x y z)))))).fv ∪ (SemanticCore.Class.cab (nb051AlphaDummy005 x y z) (Compiler.CompactSourceSyntax.synWrex (nb051AlphaDummy006 x y z) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb051AlphaDummy005 x y z)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb051AlphaDummy006 x y z)))))).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_fresh_004 (x y : SemanticCore.Var) (A B C : SemanticCore.Class) :

nb051AlphaDummy011 x y A B C ∉ (SemanticCore.Class.cv (nb051AlphaDummy004 x y A B C)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_fresh_005 (x y : SemanticCore.Var) (A B C : SemanticCore.Class) :

nb051AlphaDummy012 x y A B C ∉ (SemanticCore.Class.cv (nb051AlphaDummy004 x y A B C)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_distinct_006 (x y : SemanticCore.Var) (A B C : SemanticCore.Class) :

nb051AlphaDummy011 x y A B C ≠ nb051AlphaDummy012 x y A B C

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_fresh_007 (x y z : SemanticCore.Var) :

nb051AlphaDummy013 x y z ∉ (SemanticCore.Class.cv (nb051AlphaDummy006 x y z)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_fresh_008 (x y z : SemanticCore.Var) :

nb051AlphaDummy014 x y z ∉ (SemanticCore.Class.cv (nb051AlphaDummy006 x y z)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_distinct_009 (x y z : SemanticCore.Var) :

nb051AlphaDummy013 x y z ≠ nb051AlphaDummy014 x y z

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_fresh_010 (x y : SemanticCore.Var) (A B C : SemanticCore.Class) :

nb051AlphaDummy017 x y A B C ∉ (SemanticCore.Class.cv (nb051AlphaDummy011 x y A B C)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_fresh_011 (x y : SemanticCore.Var) (A B C : SemanticCore.Class) :

nb051AlphaDummy018 x y A B C ∉ (SemanticCore.Class.cv (nb051AlphaDummy011 x y A B C)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_fresh_012 (x y : SemanticCore.Var) (A B C : SemanticCore.Class) :

nb051AlphaDummy019 x y A B C ∉ (SemanticCore.Class.cv (nb051AlphaDummy011 x y A B C)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_distinct_013 (x y : SemanticCore.Var) (A B C : SemanticCore.Class) :

nb051AlphaDummy017 x y A B C ≠ nb051AlphaDummy018 x y A B C

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_distinct_014 (x y : SemanticCore.Var) (A B C : SemanticCore.Class) :

nb051AlphaDummy017 x y A B C ≠ nb051AlphaDummy019 x y A B C

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_distinct_015 (x y : SemanticCore.Var) (A B C : SemanticCore.Class) :

nb051AlphaDummy018 x y A B C ≠ nb051AlphaDummy019 x y A B C

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_fresh_016 (x y z : SemanticCore.Var) :

nb051AlphaDummy020 x y z ∉ (SemanticCore.Class.cv (nb051AlphaDummy013 x y z)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_fresh_017 (x y z : SemanticCore.Var) :

nb051AlphaDummy021 x y z ∉ (SemanticCore.Class.cv (nb051AlphaDummy013 x y z)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_fresh_018 (x y z : SemanticCore.Var) :

nb051AlphaDummy022 x y z ∉ (SemanticCore.Class.cv (nb051AlphaDummy013 x y z)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_distinct_019 (x y z : SemanticCore.Var) :

nb051AlphaDummy020 x y z ≠ nb051AlphaDummy021 x y z

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_distinct_020 (x y z : SemanticCore.Var) :

nb051AlphaDummy020 x y z ≠ nb051AlphaDummy022 x y z

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_distinct_021 (x y z : SemanticCore.Var) :

nb051AlphaDummy021 x y z ≠ nb051AlphaDummy022 x y z

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_fresh_022 (x y : SemanticCore.Var) (A B C : SemanticCore.Class) :

nb051AlphaDummy029 x y A B C ∉ (SemanticCore.Class.cv (nb051AlphaDummy018 x y A B C)).fv ∪ (SemanticCore.Class.cv (nb051AlphaDummy018 x y A B C)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_fresh_023 (x y : SemanticCore.Var) (A B C : SemanticCore.Class) :

nb051AlphaDummy025 x y A B C ∉ (SemanticCore.Class.cv (nb051AlphaDummy018 x y A B C)).fv ∪ (SemanticCore.Class.cv (nb051AlphaDummy019 x y A B C)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_fresh_024 (x y : SemanticCore.Var) (A B C : SemanticCore.Class) :

nb051AlphaDummy031 x y A B C ∉ (SemanticCore.Class.cv (nb051AlphaDummy019 x y A B C)).fv ∪ (SemanticCore.Class.cv (nb051AlphaDummy019 x y A B C)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_fresh_025 (x y z : SemanticCore.Var) :

nb051AlphaDummy030 x y z ∉ (SemanticCore.Class.cv (nb051AlphaDummy021 x y z)).fv ∪ (SemanticCore.Class.cv (nb051AlphaDummy021 x y z)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_fresh_026 (x y z : SemanticCore.Var) :

nb051AlphaDummy026 x y z ∉ (SemanticCore.Class.cv (nb051AlphaDummy021 x y z)).fv ∪ (SemanticCore.Class.cv (nb051AlphaDummy022 x y z)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_fresh_027 (x y z : SemanticCore.Var) :

nb051AlphaDummy032 x y z ∉ (SemanticCore.Class.cv (nb051AlphaDummy022 x y z)).fv ∪ (SemanticCore.Class.cv (nb051AlphaDummy022 x y z)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_fresh_028 (x y : SemanticCore.Var) (A B C : SemanticCore.Class) :

nb051AlphaDummy015 x y A B C ∉ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb051AlphaDummy011 x y A B C)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb051AlphaDummy011 x y A B C)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb051AlphaDummy011 x y A B C)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_fresh_029 (x y z : SemanticCore.Var) :

nb051AlphaDummy016 x y z ∉ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb051AlphaDummy013 x y z)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb051AlphaDummy013 x y z)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb051AlphaDummy013 x y z)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_fresh_030 (x y : SemanticCore.Var) (A B C : SemanticCore.Class) :

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_fresh_031 (x y z : SemanticCore.Var) :

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_fresh_032 (x y : SemanticCore.Var) (A B C : SemanticCore.Class) :

nb051AlphaDummy027 x y A B C ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb051AlphaDummy018 x y A B C))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb051AlphaDummy019 x y A B C))).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_fresh_033 (x y z : SemanticCore.Var) :

nb051AlphaDummy028 x y z ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb051AlphaDummy021 x y z))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb051AlphaDummy022 x y z))).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_fresh_034 (x y : SemanticCore.Var) (A B C : SemanticCore.Class) :

nb051AlphaDummy035 x y A B C ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb051AlphaDummy004 x y A B C)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_fresh_035 (x y z : SemanticCore.Var) :

nb051AlphaDummy036 x y z ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb051AlphaDummy006 x y z)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_fresh_036 (x y : SemanticCore.Var) (A B C : SemanticCore.Class) :

nb051AlphaDummy023 x y A B C ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb051AlphaDummy018 x y A B C)) (SemanticCore.Class.cv (nb051AlphaDummy019 x y A B C))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb051AlphaDummy018 x y A B C)) (SemanticCore.Class.cv (nb051AlphaDummy019 x y A B C))).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_fresh_037 (x y z : SemanticCore.Var) :

nb051AlphaDummy024 x y z ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb051AlphaDummy021 x y z)) (SemanticCore.Class.cv (nb051AlphaDummy022 x y z))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb051AlphaDummy021 x y z)) (SemanticCore.Class.cv (nb051AlphaDummy022 x y z))).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_fresh_038 (x y : SemanticCore.Var) (A B C : SemanticCore.Class) :

nb051AlphaDummy003 x y A B C ∉ (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)).fv ∪ (SemanticCore.Class.cv (nb051AlphaDummy000 x y A B C)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_fresh_039 (x y : SemanticCore.Var) (A B C : SemanticCore.Class) :

nb051AlphaDummy004 x y A B C ∉ (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)).fv ∪ (SemanticCore.Class.cv (nb051AlphaDummy000 x y A B C)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_distinct_040 (x y : SemanticCore.Var) (A B C : SemanticCore.Class) :

nb051AlphaDummy003 x y A B C ≠ nb051AlphaDummy004 x y A B C

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_fresh_041 (x y z : SemanticCore.Var) :

nb051AlphaDummy005 x y z ∉ (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)).fv ∪ (SemanticCore.Class.cv z).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_fresh_042 (x y z : SemanticCore.Var) :

nb051AlphaDummy006 x y z ∉ (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)).fv ∪ (SemanticCore.Class.cv z).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_distinct_043 (x y z : SemanticCore.Var) :

nb051AlphaDummy005 x y z ≠ nb051AlphaDummy006 x y z

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_fresh_044 (x y : SemanticCore.Var) (A B C : SemanticCore.Class) :

nb051AlphaDummy037 x y A B C ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb051AlphaDummy004 x y A B C))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb051AlphaDummy004 x y A B C))).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_fresh_045 (x y z : SemanticCore.Var) :

nb051AlphaDummy038 x y z ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb051AlphaDummy006 x y z))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb051AlphaDummy006 x y z))).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_fresh_046 (x y : SemanticCore.Var) (A B C : SemanticCore.Class) :

nb051AlphaDummy000 x y A B C ∉ {x} ∪ A.fv ∪ {y} ∪ B.fv ∪ C.fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_fresh_047 (x y : SemanticCore.Var) (A B C : SemanticCore.Class) :

nb051AlphaDummy001 x y A B C ∉ {x} ∪ {y} ∪ {nb051AlphaDummy000 x y A B C} ∪ (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A) (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) B)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb051AlphaDummy000 x y A B C)) C)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_fresh_048 (x y z : SemanticCore.Var) (A B C : SemanticCore.Class) :

nb051AlphaDummy002 x y z A B C ∉ {x} ∪ {y} ∪ {z} ∪ (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A) (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) B)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv z) C)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_support_mem_0000 (x y : SemanticCore.Var) (A B C : SemanticCore.Class) :

x ∈ {x} ∪ {y} ∪ {nb051AlphaDummy000 x y A B C} ∪ (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A) (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) B)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb051AlphaDummy000 x y A B C)) C)).fv

Certificates from NAPD051C001Part003.

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_support_mem_0002 (x y : SemanticCore.Var) (A B C : SemanticCore.Class) :

y ∈ {x} ∪ {y} ∪ {nb051AlphaDummy000 x y A B C} ∪ (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A) (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) B)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb051AlphaDummy000 x y A B C)) C)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_support_mem_0004 (x y : SemanticCore.Var) (A B C : SemanticCore.Class) :

nb051AlphaDummy000 x y A B C ∈ {x} ∪ {y} ∪ {nb051AlphaDummy000 x y A B C} ∪ (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A) (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) B)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb051AlphaDummy000 x y A B C)) C)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_support_mem_0006 (x y : SemanticCore.Var) (A B C : SemanticCore.Class) :

x ∈ (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)).fv ∪ (SemanticCore.Class.cv (nb051AlphaDummy000 x y A B C)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_support_mem_0007 (x y : SemanticCore.Var) (A B C : SemanticCore.Class) :

y ∈ (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)).fv ∪ (SemanticCore.Class.cv (nb051AlphaDummy000 x y A B C)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_support_mem_0008 (x y z : SemanticCore.Var) :

x ∈ (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)).fv ∪ (SemanticCore.Class.cv z).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_support_mem_0009 (x y z : SemanticCore.Var) :

y ∈ (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)).fv ∪ (SemanticCore.Class.cv z).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_support_mem_0010 (x y : SemanticCore.Var) (A B C : SemanticCore.Class) :

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_support_mem_0011 (x y : SemanticCore.Var) (A B C : SemanticCore.Class) :

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_support_mem_0012 (x y z : SemanticCore.Var) :

x ∈ (SemanticCore.Class.cab (nb051AlphaDummy005 x y z) (Compiler.CompactSourceSyntax.synWrex (nb051AlphaDummy006 x y z) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb051AlphaDummy005 x y z)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb051AlphaDummy006 x y z)))))).fv ∪ (SemanticCore.Class.cab (nb051AlphaDummy005 x y z) (Compiler.CompactSourceSyntax.synWrex (nb051AlphaDummy006 x y z) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb051AlphaDummy005 x y z)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb051AlphaDummy006 x y z)))))).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_support_mem_0013 (x y z : SemanticCore.Var) :

y ∈ (SemanticCore.Class.cab (nb051AlphaDummy005 x y z) (Compiler.CompactSourceSyntax.synWrex (nb051AlphaDummy006 x y z) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb051AlphaDummy005 x y z)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb051AlphaDummy006 x y z)))))).fv ∪ (SemanticCore.Class.cab (nb051AlphaDummy005 x y z) (Compiler.CompactSourceSyntax.synWrex (nb051AlphaDummy006 x y z) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb051AlphaDummy005 x y z)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb051AlphaDummy006 x y z)))))).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_support_mem_0014 (x y : SemanticCore.Var) (A B C : SemanticCore.Class) :

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_support_mem_0015 (x y : SemanticCore.Var) (A B C : SemanticCore.Class) :

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_support_mem_0016 (x y z : SemanticCore.Var) :

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_support_mem_0017 (x y z : SemanticCore.Var) :

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_support_mem_0018 (x y : SemanticCore.Var) (A B C : SemanticCore.Class) :

x ∈ {x} ∪ A.fv ∪ {y} ∪ B.fv ∪ C.fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_support_mem_0019 (x y : SemanticCore.Var) (A B C : SemanticCore.Class) :

y ∈ {x} ∪ A.fv ∪ {y} ∪ B.fv ∪ C.fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_support_mem_0020 (x y : SemanticCore.Var) (A B C : SemanticCore.Class) :

nb051AlphaDummy004 x y A B C ∈ (SemanticCore.Class.cv (nb051AlphaDummy004 x y A B C)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_support_mem_0021 (x y z : SemanticCore.Var) :

nb051AlphaDummy006 x y z ∈ (SemanticCore.Class.cv (nb051AlphaDummy006 x y z)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_support_mem_0022 (x y : SemanticCore.Var) (A B C : SemanticCore.Class) :

nb051AlphaDummy011 x y A B C ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb051AlphaDummy011 x y A B C)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb051AlphaDummy011 x y A B C)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb051AlphaDummy011 x y A B C)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_support_mem_0024 (x y : SemanticCore.Var) (A B C : SemanticCore.Class) :

nb051AlphaDummy011 x y A B C ∈ (SemanticCore.Class.cv (nb051AlphaDummy011 x y A B C)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_support_mem_0025 (x y z : SemanticCore.Var) :

nb051AlphaDummy013 x y z ∈ (SemanticCore.Class.cv (nb051AlphaDummy013 x y z)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_support_mem_0026 (x y : SemanticCore.Var) (A B C : SemanticCore.Class) :

nb051AlphaDummy018 x y A B C ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb051AlphaDummy018 x y A B C)) (SemanticCore.Class.cv (nb051AlphaDummy019 x y A B C))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb051AlphaDummy018 x y A B C)) (SemanticCore.Class.cv (nb051AlphaDummy019 x y A B C))).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_support_mem_0027 (x y z : SemanticCore.Var) :

nb051AlphaDummy021 x y z ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb051AlphaDummy021 x y z)) (SemanticCore.Class.cv (nb051AlphaDummy022 x y z))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb051AlphaDummy021 x y z)) (SemanticCore.Class.cv (nb051AlphaDummy022 x y z))).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_support_mem_0028 (x y : SemanticCore.Var) (A B C : SemanticCore.Class) :

nb051AlphaDummy018 x y A B C ∈ (SemanticCore.Class.cv (nb051AlphaDummy018 x y A B C)).fv ∪ (SemanticCore.Class.cv (nb051AlphaDummy019 x y A B C)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_support_mem_0029 (x y z : SemanticCore.Var) :

nb051AlphaDummy021 x y z ∈ (SemanticCore.Class.cv (nb051AlphaDummy021 x y z)).fv ∪ (SemanticCore.Class.cv (nb051AlphaDummy022 x y z)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_support_mem_0030 (x y : SemanticCore.Var) (A B C : SemanticCore.Class) :

nb051AlphaDummy019 x y A B C ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb051AlphaDummy018 x y A B C)) (SemanticCore.Class.cv (nb051AlphaDummy019 x y A B C))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb051AlphaDummy018 x y A B C)) (SemanticCore.Class.cv (nb051AlphaDummy019 x y A B C))).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_support_mem_0031 (x y z : SemanticCore.Var) :

nb051AlphaDummy022 x y z ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb051AlphaDummy021 x y z)) (SemanticCore.Class.cv (nb051AlphaDummy022 x y z))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb051AlphaDummy021 x y z)) (SemanticCore.Class.cv (nb051AlphaDummy022 x y z))).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_support_mem_0032 (x y : SemanticCore.Var) (A B C : SemanticCore.Class) :

nb051AlphaDummy019 x y A B C ∈ (SemanticCore.Class.cv (nb051AlphaDummy018 x y A B C)).fv ∪ (SemanticCore.Class.cv (nb051AlphaDummy019 x y A B C)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_support_mem_0033 (x y z : SemanticCore.Var) :

nb051AlphaDummy022 x y z ∈ (SemanticCore.Class.cv (nb051AlphaDummy021 x y z)).fv ∪ (SemanticCore.Class.cv (nb051AlphaDummy022 x y z)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_support_mem_0034 (x y : SemanticCore.Var) (A B C : SemanticCore.Class) :

nb051AlphaDummy018 x y A B C ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb051AlphaDummy018 x y A B C))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb051AlphaDummy019 x y A B C))).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_support_mem_0035 (x y z : SemanticCore.Var) :

nb051AlphaDummy021 x y z ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb051AlphaDummy021 x y z))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb051AlphaDummy022 x y z))).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_support_mem_0036 (x y : SemanticCore.Var) (A B C : SemanticCore.Class) :

nb051AlphaDummy018 x y A B C ∈ (SemanticCore.Class.cv (nb051AlphaDummy018 x y A B C)).fv ∪ (SemanticCore.Class.cv (nb051AlphaDummy018 x y A B C)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_support_mem_0037 (x y z : SemanticCore.Var) :

nb051AlphaDummy021 x y z ∈ (SemanticCore.Class.cv (nb051AlphaDummy021 x y z)).fv ∪ (SemanticCore.Class.cv (nb051AlphaDummy021 x y z)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_support_mem_0038 (x y : SemanticCore.Var) (A B C : SemanticCore.Class) :

nb051AlphaDummy019 x y A B C ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb051AlphaDummy018 x y A B C))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb051AlphaDummy019 x y A B C))).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_support_mem_0039 (x y z : SemanticCore.Var) :

nb051AlphaDummy022 x y z ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb051AlphaDummy021 x y z))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb051AlphaDummy022 x y z))).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_support_mem_0040 (x y : SemanticCore.Var) (A B C : SemanticCore.Class) :

nb051AlphaDummy019 x y A B C ∈ (SemanticCore.Class.cv (nb051AlphaDummy019 x y A B C)).fv ∪ (SemanticCore.Class.cv (nb051AlphaDummy019 x y A B C)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_support_mem_0041 (x y z : SemanticCore.Var) :

nb051AlphaDummy022 x y z ∈ (SemanticCore.Class.cv (nb051AlphaDummy022 x y z)).fv ∪ (SemanticCore.Class.cv (nb051AlphaDummy022 x y z)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_support_mem_0042 (x y : SemanticCore.Var) (A B C : SemanticCore.Class) :

nb051AlphaDummy000 x y A B C ∈ (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)).fv ∪ (SemanticCore.Class.cv (nb051AlphaDummy000 x y A B C)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_support_mem_0043 (x y : SemanticCore.Var) (A B C : SemanticCore.Class) :

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_support_mem_0044 (x y z : SemanticCore.Var) :

z ∈ (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)).fv ∪ (SemanticCore.Class.cv z).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_support_mem_0045 (x y z : SemanticCore.Var) :

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_support_mem_0046 (x y : SemanticCore.Var) (A B C : SemanticCore.Class) :

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_support_mem_0047 (x y z : SemanticCore.Var) :

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_support_mem_0048 (x y : SemanticCore.Var) (A B C : SemanticCore.Class) :

nb051AlphaDummy004 x y A B C ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb051AlphaDummy004 x y A B C)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_support_mem_0049 (x y z : SemanticCore.Var) :

nb051AlphaDummy006 x y z ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb051AlphaDummy006 x y z)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_support_mem_0050 (x y : SemanticCore.Var) (A B C : SemanticCore.Class) :

nb051AlphaDummy004 x y A B C ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb051AlphaDummy004 x y A B C))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb051AlphaDummy004 x y A B C))).fv

Certificates from NAPD051C001Part004.

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_support_mem_0051 (x y z : SemanticCore.Var) :

nb051AlphaDummy006 x y z ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb051AlphaDummy006 x y z))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb051AlphaDummy006 x y z))).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_wpp_notmem_0000 (x y : SemanticCore.Var) (A B C : SemanticCore.Class) :

nb051AlphaDummy004 x y A B C ∉ (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_wpp_notmem_0001 (x y z : SemanticCore.Var) :

nb051AlphaDummy006 x y z ∉ (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_wpp_notmem_0002 (x y : SemanticCore.Var) (A B C : SemanticCore.Class) :

nb051AlphaDummy003 x y A B C ∉ (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_wpp_notmem_0003 (x y z : SemanticCore.Var) :

nb051AlphaDummy005 x y z ∉ (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_wpp_notmem_0004 (x y : SemanticCore.Var) (A B C : SemanticCore.Class) :

nb051AlphaDummy009 x y A B C ∉ (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_wpp_notmem_0005 (x y z : SemanticCore.Var) :

nb051AlphaDummy010 x y z ∉ (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_wpp_notmem_0006 (x y : SemanticCore.Var) (A B C : SemanticCore.Class) :

nb051AlphaDummy007 x y A B C ∉ (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_wpp_notmem_0007 (x y z : SemanticCore.Var) :

nb051AlphaDummy008 x y z ∉ (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_compact_fv_empty_0008 (x y : SemanticCore.Var) (A B C : SemanticCore.Class) :

nb051AlphaDummy000 x y A B C ∉ ∅

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_wpp_notmem_0008 (x y : SemanticCore.Var) (A B C : SemanticCore.Class) :

nb051AlphaDummy000 x y A B C ∉ (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_compact_fv_empty_0009 (z : SemanticCore.Var) :

z ∉ ∅

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_wpp_notmem_0009 (x y z : SemanticCore.Var) (dv_x_z : x ≠ z) (dv_y_z : y ≠ z) :

z ∉ (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_compact_fv_empty_0010 (x y : SemanticCore.Var) (A B C : SemanticCore.Class) :

nb051AlphaDummy001 x y A B C ∉ ∅

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_wpp_notmem_0010 (x y : SemanticCore.Var) (A B C : SemanticCore.Class) :

nb051AlphaDummy001 x y A B C ∉ (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_compact_fv_empty_0011 (x y z : SemanticCore.Var) (A B C : SemanticCore.Class) :

nb051AlphaDummy002 x y z A B C ∉ ∅

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_wpp_notmem_0011 (x y z : SemanticCore.Var) (A B C : SemanticCore.Class) :

nb051AlphaDummy002 x y z A B C ∉ (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)).fv

Certificates from NAPD051C001Part005.

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051_compact_envfresh_0000 (x y z : SemanticCore.Var) (A B C : SemanticCore.Class) (dv_x_z : x ≠ z) (dv_y_z : y ≠ z) :

Nominal.TEnvFresh [(nb051AlphaDummy004 x y A B C, nb051AlphaDummy006 x y z), (nb051AlphaDummy003 x y A B C, nb051AlphaDummy005 x y z), (nb051AlphaDummy009 x y A B C, nb051AlphaDummy010 x y z), (nb051AlphaDummy007 x y A B C, nb051AlphaDummy008 x y z), (nb051AlphaDummy000 x y A B C, z), (y, y), (x, x), (nb051AlphaDummy001 x y A B C, nb051AlphaDummy002 x y z A B C)] (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)).fv

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051WppRefl0000 (x y z : SemanticCore.Var) (A B C : SemanticCore.Class) (dv_x_z : x ≠ z) (dv_y_z : y ≠ z) :

Nominal.TReflOn [(nb051AlphaDummy004 x y A B C, nb051AlphaDummy006 x y z), (nb051AlphaDummy003 x y A B C, nb051AlphaDummy005 x y z), (nb051AlphaDummy009 x y A B C, nb051AlphaDummy010 x y z), (nb051AlphaDummy007 x y A B C, nb051AlphaDummy008 x y z), (nb051AlphaDummy000 x y A B C, z), (y, y), (x, x), (nb051AlphaDummy001 x y A B C, nb051AlphaDummy002 x y z A B C)] (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)).fv

Checked nominal proof certificate identified upstream as nb051_wpp_refl_0000.

Equations

NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb051WppRefl0000 x y z A B C dv_x_z dv_y_z = ⋯.reflOn

Instances For