NF weak partition development: NAR4H5C095M3Part034.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095SplitAlpha0073 (x u : SemanticCore.Var) (D R S_cls : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) : Nominal.TAlphaWff [(nb095AlphaDummy131 D R S_cls E, nb095AlphaDummy132 f), (nb095AlphaDummy129 D R S_cls E, nb095AlphaDummy130 f), (nb095AlphaDummy098 D R S_cls E, nb095AlphaDummy100 f), (nb095AlphaDummy097 D R S_cls E, nb095AlphaDummy099 f), (nb095AlphaDummy127 D R S_cls E, nb095AlphaDummy128 f), (nb095AlphaDummy101 D R S_cls E, nb095AlphaDummy102 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), (nb095AlphaDummy387 D R S_cls E, nb095AlphaDummy390 f), (nb095AlphaDummy386 D R S_cls E, nb095AlphaDummy389 f), (nb095AlphaDummy385 D R S_cls E, nb095AlphaDummy388 f), (nb095AlphaDummy391 D R S_cls E, nb095AlphaDummy392 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 (nb095AlphaDummy131 D R S_cls E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy098 D R S_cls E)))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy131 D R S_cls E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy098 D R S_cls E)))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy132 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy100 f)))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy132 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy100 f)))).neg)

Checked nominal proof certificate identified upstream as nb095_split_alpha_0073.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095SplitAlpha0074 (x u : SemanticCore.Var) (D R S_cls : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) : Nominal.TAlphaWff [(nb095AlphaDummy139 D R S_cls E, nb095AlphaDummy140 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), (nb095AlphaDummy387 D R S_cls E, nb095AlphaDummy390 f), (nb095AlphaDummy386 D R S_cls E, nb095AlphaDummy389 f), (nb095AlphaDummy385 D R S_cls E, nb095AlphaDummy388 f), (nb095AlphaDummy391 D R S_cls E, nb095AlphaDummy392 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 (nb095AlphaDummy139 D R S_cls E)) (SemanticCore.Class.cab (nb095AlphaDummy133 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy134 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy092 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy133 D R S_cls E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy134 D R S_cls E))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy139 D R S_cls E)) (SemanticCore.Class.cab (nb095AlphaDummy133 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy134 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy092 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy133 D R S_cls E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy134 D R S_cls E))))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy140 f)) (SemanticCore.Class.cab (nb095AlphaDummy135 f) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy136 f) (SemanticCore.Class.cv (nb095AlphaDummy094 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy135 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy136 f))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy140 f)) (SemanticCore.Class.cab (nb095AlphaDummy135 f) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy136 f) (SemanticCore.Class.cv (nb095AlphaDummy094 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy135 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy136 f))))))).neg)

Checked nominal proof certificate identified upstream as nb095_split_alpha_0074.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095SplitAlpha0075 (x u : SemanticCore.Var) (D R S_cls : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) : Nominal.TAlphaWff [(nb095AlphaDummy167 D R S_cls E, nb095AlphaDummy168 f), (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), (nb095AlphaDummy387 D R S_cls E, nb095AlphaDummy390 f), (nb095AlphaDummy386 D R S_cls E, nb095AlphaDummy389 f), (nb095AlphaDummy385 D R S_cls E, nb095AlphaDummy388 f), (nb095AlphaDummy391 D R S_cls E, nb095AlphaDummy392 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 (nb095AlphaDummy167 D R S_cls E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy134 D R S_cls E)))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy167 D R S_cls E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy134 D R S_cls E)))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy168 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy136 f)))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy168 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy136 f)))).neg)

Checked nominal proof certificate identified upstream as nb095_split_alpha_0075.

Equations

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_compact_envfresh_0256 (x u : SemanticCore.Var) (D R S_cls : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) (dv_E_f : f ∉ E.fv) (dv_E_u : u ∉ E.fv) (dv_E_x : x ∉ E.fv) : Nominal.TEnvFresh [(nb095AlphaDummy337 D R S_cls E, nb095AlphaDummy338 u S_cls E), (nb095AlphaDummy335 D R S_cls E, nb095AlphaDummy336 u S_cls E), (nb095AlphaDummy001 D R S_cls E, u), (nb095AlphaDummy002 D R S_cls E, x), (nb095AlphaDummy000 D R S_cls E, f)] E.fv

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095FocusedRefl0004 (x u : SemanticCore.Var) (D R S_cls : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) (dv_E_f : f ∉ E.fv) (dv_E_u : u ∉ E.fv) (dv_E_x : x ∉ E.fv) : Nominal.TReflOn [(nb095AlphaDummy337 D R S_cls E, nb095AlphaDummy338 u S_cls E), (nb095AlphaDummy335 D R S_cls E, nb095AlphaDummy336 u S_cls E), (nb095AlphaDummy001 D R S_cls E, u), (nb095AlphaDummy002 D R S_cls E, x), (nb095AlphaDummy000 D R S_cls E, f)] E.fv

Checked nominal proof certificate identified upstream as nb095_focused_refl_0004.

Equations

• NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095FocusedRefl0004 x u D R S_cls f E dv_E_f dv_E_u dv_E_x = ⋯.reflOn