Nominal proof certificates grouped in dependency order.

Certificates from AlphaSupport.NAR4H5C095M3Part018Stage1.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095SplitAlpha0026 (x u : SemanticCore.Var) (D R S_cls : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) : Nominal.TAlphaWff [(nb095AlphaDummy165 D R S_cls E, nb095AlphaDummy166 f), (nb095AlphaDummy134 D R S_cls E, nb095AlphaDummy136 f), (nb095AlphaDummy133 D R S_cls E, nb095AlphaDummy135 f), (nb095AlphaDummy163 D R S_cls E, nb095AlphaDummy164 f), (nb095AlphaDummy137 D R S_cls E, nb095AlphaDummy138 f), (nb095AlphaDummy092 D R S_cls E, nb095AlphaDummy094 f), (nb095AlphaDummy091 D R S_cls E, nb095AlphaDummy093 f), (nb095AlphaDummy095 D R S_cls E, nb095AlphaDummy096 f), (nb095AlphaDummy206 D R S_cls E, nb095AlphaDummy208 f), (nb095AlphaDummy205 D R S_cls E, nb095AlphaDummy207 f), (nb095AlphaDummy001 D R S_cls E, u), (nb095AlphaDummy002 D R S_cls E, x), (nb095AlphaDummy000 D R S_cls E, f)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy165 D R S_cls E)) (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy134 D R S_cls E))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy165 D R S_cls E)) (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy166 f)) (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy136 f))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy166 f)) (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))).neg)

Checked nominal proof certificate identified upstream as nb095_split_alpha_0026.

Equations

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_focused_notmem_0005 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy247 D R S_cls E ∉ D.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_focused_notmem_0006 (x : SemanticCore.Var) (D R : SemanticCore.Class) : nb095AlphaDummy248 x D R ∉ D.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_focused_notmem_0007 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy245 D R S_cls E ∉ D.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_focused_notmem_0008 (x : SemanticCore.Var) (D R : SemanticCore.Class) : nb095AlphaDummy246 x D R ∉ D.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_focused_notmem_0009 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy001 D R S_cls E ∉ D.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_compact_envfresh_0095 (x u : SemanticCore.Var) (D R S_cls : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) (dv_D_f : f ∉ D.fv) (dv_D_u : u ∉ D.fv) (dv_D_x : x ∉ D.fv) : Nominal.TEnvFresh [(nb095AlphaDummy247 D R S_cls E, nb095AlphaDummy248 x D R), (nb095AlphaDummy245 D R S_cls E, nb095AlphaDummy246 x D R), (nb095AlphaDummy001 D R S_cls E, u), (nb095AlphaDummy002 D R S_cls E, x), (nb095AlphaDummy000 D R S_cls E, f)] D.fv

Certificates from AlphaSupport.NAR4H5C095M3Part018Stage2.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095FocusedRefl0002 (x u : SemanticCore.Var) (D R S_cls : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) (dv_D_f : f ∉ D.fv) (dv_D_u : u ∉ D.fv) (dv_D_x : x ∉ D.fv) : Nominal.TReflOn [(nb095AlphaDummy247 D R S_cls E, nb095AlphaDummy248 x D R), (nb095AlphaDummy245 D R S_cls E, nb095AlphaDummy246 x D R), (nb095AlphaDummy001 D R S_cls E, u), (nb095AlphaDummy002 D R S_cls E, x), (nb095AlphaDummy000 D R S_cls E, f)] D.fv

Checked nominal proof certificate identified upstream as nb095_focused_refl_0002.

Equations

• NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095FocusedRefl0002 x u D R S_cls f E dv_D_f dv_D_u dv_D_x = ⋯.reflOn

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_compact_fv_empty_0204 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy250 D R S_cls E ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_compact_fv_empty_0205 (x : SemanticCore.Var) (R : SemanticCore.Class) : nb095AlphaDummy252 x R ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_compact_fv_empty_0206 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy249 D R S_cls E ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_compact_fv_empty_0207 (x : SemanticCore.Var) (R : SemanticCore.Class) : nb095AlphaDummy251 x R ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_compact_fv_empty_0208 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy247 D R S_cls E ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_compact_fv_empty_0209 (x : SemanticCore.Var) (D R : SemanticCore.Class) : nb095AlphaDummy248 x D R ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_compact_fv_empty_0210 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy245 D R S_cls E ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_compact_fv_empty_0211 (x : SemanticCore.Var) (D R : SemanticCore.Class) : nb095AlphaDummy246 x D R ∉ ∅