Nominal proof certificates grouped in dependency order.

Certificates from NAR4C077C001Part010.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077SplitAlpha0000 (x : SemanticCore.Var) (F I : SemanticCore.Class) : Nominal.TAlphaWff [(nb077AlphaDummy025 F I, nb077AlphaDummy026 x F I), (nb077AlphaDummy023 F I, nb077AlphaDummy024 x F I), (nb077AlphaDummy016 F I, nb077AlphaDummy018 x F I), (nb077AlphaDummy015 F I, nb077AlphaDummy017 x F I), (nb077AlphaDummy013 F I, nb077AlphaDummy014 x F I), (nb077AlphaDummy011 F I, nb077AlphaDummy012 x F I), (nb077AlphaDummy001 F I, nb077AlphaDummy002 x F I), (nb077AlphaDummy004 F I, nb077AlphaDummy006 x F I), (nb077AlphaDummy003 F I, nb077AlphaDummy005 x F I)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb077AlphaDummy025 F I)) (SemanticCore.Class.cab (nb077AlphaDummy019 F I) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy020 F I) (SemanticCore.Class.cv (nb077AlphaDummy016 F I)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy019 F I)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy020 F I))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb077AlphaDummy025 F I)) (SemanticCore.Class.cab (nb077AlphaDummy019 F I) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy020 F I) (SemanticCore.Class.cv (nb077AlphaDummy016 F I)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy019 F I)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy020 F I))))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb077AlphaDummy026 x F I)) (SemanticCore.Class.cab (nb077AlphaDummy021 x F I) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy022 x F I) (SemanticCore.Class.cv (nb077AlphaDummy018 x F I)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy021 x F I)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy022 x F I))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb077AlphaDummy026 x F I)) (SemanticCore.Class.cab (nb077AlphaDummy021 x F I) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy022 x F I) (SemanticCore.Class.cv (nb077AlphaDummy018 x F I)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy021 x F I)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy022 x F I))))))).neg)

Checked nominal proof certificate identified upstream as nb077_split_alpha_0000.

Equations

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

Certificates from NAR4C077C001Part011.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077SplitAlpha0001 (x : SemanticCore.Var) (F I : SemanticCore.Class) : Nominal.TAlphaWff [(nb077AlphaDummy051 F I, nb077AlphaDummy052 x F I), (nb077AlphaDummy020 F I, nb077AlphaDummy022 x F I), (nb077AlphaDummy019 F I, nb077AlphaDummy021 x F I), (nb077AlphaDummy049 F I, nb077AlphaDummy050 x F I), (nb077AlphaDummy023 F I, nb077AlphaDummy024 x F I), (nb077AlphaDummy016 F I, nb077AlphaDummy018 x F I), (nb077AlphaDummy015 F I, nb077AlphaDummy017 x F I), (nb077AlphaDummy013 F I, nb077AlphaDummy014 x F I), (nb077AlphaDummy011 F I, nb077AlphaDummy012 x F I), (nb077AlphaDummy001 F I, nb077AlphaDummy002 x F I), (nb077AlphaDummy004 F I, nb077AlphaDummy006 x F I), (nb077AlphaDummy003 F I, nb077AlphaDummy005 x F I)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb077AlphaDummy051 F I)) (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy020 F I))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb077AlphaDummy051 F I)) (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb077AlphaDummy052 x F I)) (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy022 x F I))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb077AlphaDummy052 x F I)) (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))).neg)

Checked nominal proof certificate identified upstream as nb077_split_alpha_0001.

Equations

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_compact_fv_empty_0064 (F I : SemanticCore.Class) : nb077AlphaDummy060 F I ∉ ∅

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_compact_fv_empty_0066 (F I : SemanticCore.Class) : nb077AlphaDummy059 F I ∉ ∅

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_compact_fv_empty_0068 (F I : SemanticCore.Class) : nb077AlphaDummy065 F I ∉ ∅

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_compact_fv_empty_0070 (F I : SemanticCore.Class) : nb077AlphaDummy057 F I ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_compact_fv_empty_0071 (x : SemanticCore.Var) (F : SemanticCore.Class) : nb077AlphaDummy058 x F ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_compact_fv_empty_0072 (F I : SemanticCore.Class) : nb077AlphaDummy055 F I ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_compact_fv_empty_0073 (x : SemanticCore.Var) (F : SemanticCore.Class) : nb077AlphaDummy056 x F ∉ ∅