NF weak partition development: NAR4C070C001Part004.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070SplitAlpha0004 (x : SemanticCore.Var) (A : SemanticCore.Class) (b : SemanticCore.Var) : Nominal.TAlphaWff [(nb070AlphaDummy032 A, nb070AlphaDummy034 x), (nb070AlphaDummy033 A, nb070AlphaDummy035 x), (nb070AlphaDummy058 A, nb070AlphaDummy059 x), (nb070AlphaDummy056 A, nb070AlphaDummy057 x), (nb070AlphaDummy025 A, nb070AlphaDummy027 x), (nb070AlphaDummy024 A, nb070AlphaDummy026 x), (nb070AlphaDummy054 A, nb070AlphaDummy055 x), (nb070AlphaDummy028 A, nb070AlphaDummy029 x), (nb070AlphaDummy009 A, nb070AlphaDummy011 x), (nb070AlphaDummy008 A, nb070AlphaDummy010 x), (nb070AlphaDummy001 A, x), (nb070AlphaDummy000 A, b), (nb070AlphaDummy002 A, nb070AlphaDummy003 x A b), (nb070AlphaDummy005 A, nb070AlphaDummy007 x A b), (nb070AlphaDummy004 A, nb070AlphaDummy006 x A b)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb070AlphaDummy032 A)) (SemanticCore.Class.cv (nb070AlphaDummy025 A))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb070AlphaDummy033 A)) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb070AlphaDummy032 A)) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb070AlphaDummy032 A)) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv (nb070AlphaDummy032 A)))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb070AlphaDummy034 x)) (SemanticCore.Class.cv (nb070AlphaDummy027 x))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb070AlphaDummy035 x)) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb070AlphaDummy034 x)) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb070AlphaDummy034 x)) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv (nb070AlphaDummy034 x)))).neg)

Checked nominal proof certificate identified upstream as nb070_split_alpha_0004.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070SplitAlpha0005 (x : SemanticCore.Var) (A : SemanticCore.Class) (b : SemanticCore.Var) : Nominal.TAlphaWff [(nb070AlphaDummy054 A, nb070AlphaDummy055 x), (nb070AlphaDummy028 A, nb070AlphaDummy029 x), (nb070AlphaDummy009 A, nb070AlphaDummy011 x), (nb070AlphaDummy008 A, nb070AlphaDummy010 x), (nb070AlphaDummy001 A, x), (nb070AlphaDummy000 A, b), (nb070AlphaDummy002 A, nb070AlphaDummy003 x A b), (nb070AlphaDummy005 A, nb070AlphaDummy007 x A b), (nb070AlphaDummy004 A, nb070AlphaDummy006 x A b)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb070AlphaDummy054 A)) (SemanticCore.Class.cab (nb070AlphaDummy024 A) (Compiler.CompactSourceSyntax.synWrex (nb070AlphaDummy025 A) (SemanticCore.Class.cv (nb070AlphaDummy008 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb070AlphaDummy024 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb070AlphaDummy025 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb070AlphaDummy054 A)) (SemanticCore.Class.cab (nb070AlphaDummy024 A) (Compiler.CompactSourceSyntax.synWrex (nb070AlphaDummy025 A) (SemanticCore.Class.cv (nb070AlphaDummy008 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb070AlphaDummy024 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb070AlphaDummy025 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb070AlphaDummy055 x)) (SemanticCore.Class.cab (nb070AlphaDummy026 x) (Compiler.CompactSourceSyntax.synWrex (nb070AlphaDummy027 x) (SemanticCore.Class.cv (nb070AlphaDummy010 x)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb070AlphaDummy026 x)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb070AlphaDummy027 x))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb070AlphaDummy055 x)) (SemanticCore.Class.cab (nb070AlphaDummy026 x) (Compiler.CompactSourceSyntax.synWrex (nb070AlphaDummy027 x) (SemanticCore.Class.cv (nb070AlphaDummy010 x)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb070AlphaDummy026 x)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb070AlphaDummy027 x))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg)

Checked nominal proof certificate identified upstream as nb070_split_alpha_0005.

Equations

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_wpp_notmem_0162 (A : SemanticCore.Class) : nb070AlphaDummy009 A ∉ Compiler.CompactSourceSyntax.synCen.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_wpp_notmem_0163 (x : SemanticCore.Var) : nb070AlphaDummy011 x ∉ Compiler.CompactSourceSyntax.synCen.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_wpp_notmem_0164 (A : SemanticCore.Class) : nb070AlphaDummy008 A ∉ Compiler.CompactSourceSyntax.synCen.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_wpp_notmem_0165 (x : SemanticCore.Var) : nb070AlphaDummy010 x ∉ Compiler.CompactSourceSyntax.synCen.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_wpp_notmem_0166 (A : SemanticCore.Class) : nb070AlphaDummy001 A ∉ Compiler.CompactSourceSyntax.synCen.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_wpp_notmem_0167 (x : SemanticCore.Var) : x ∉ Compiler.CompactSourceSyntax.synCen.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_wpp_notmem_0168 (A : SemanticCore.Class) : nb070AlphaDummy000 A ∉ Compiler.CompactSourceSyntax.synCen.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_wpp_notmem_0169 (b : SemanticCore.Var) : b ∉ Compiler.CompactSourceSyntax.synCen.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_wpp_notmem_0170 (A : SemanticCore.Class) : nb070AlphaDummy002 A ∉ Compiler.CompactSourceSyntax.synCen.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_wpp_notmem_0171 (x : SemanticCore.Var) (A : SemanticCore.Class) (b : SemanticCore.Var) : nb070AlphaDummy003 x A b ∉ Compiler.CompactSourceSyntax.synCen.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_wpp_notmem_0172 (A : SemanticCore.Class) : nb070AlphaDummy005 A ∉ Compiler.CompactSourceSyntax.synCen.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_wpp_notmem_0173 (x : SemanticCore.Var) (A : SemanticCore.Class) (b : SemanticCore.Var) : nb070AlphaDummy007 x A b ∉ Compiler.CompactSourceSyntax.synCen.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_wpp_notmem_0174 (A : SemanticCore.Class) : nb070AlphaDummy004 A ∉ Compiler.CompactSourceSyntax.synCen.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_wpp_notmem_0175 (x : SemanticCore.Var) (A : SemanticCore.Class) (b : SemanticCore.Var) : nb070AlphaDummy006 x A b ∉ Compiler.CompactSourceSyntax.synCen.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070_compact_envfresh_0010 (x : SemanticCore.Var) (A : SemanticCore.Class) (b : SemanticCore.Var) : Nominal.TEnvFresh [(nb070AlphaDummy009 A, nb070AlphaDummy011 x), (nb070AlphaDummy008 A, nb070AlphaDummy010 x), (nb070AlphaDummy001 A, x), (nb070AlphaDummy000 A, b), (nb070AlphaDummy002 A, nb070AlphaDummy003 x A b), (nb070AlphaDummy005 A, nb070AlphaDummy007 x A b), (nb070AlphaDummy004 A, nb070AlphaDummy006 x A b)] Compiler.CompactSourceSyntax.synCen.fv