NF weak partition development: NAR4C072C001Part016.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb072SplitAlpha0006 (x y : SemanticCore.Var) (A B R S_cls H : SemanticCore.Class) (dv_H_x : x ∉ H.fv) (dv_H_y : y ∉ H.fv) : Nominal.TAlphaWff [(nb072AlphaDummy039 A B R S_cls H, nb072AlphaDummy041 x y H), (nb072AlphaDummy038 A B R S_cls H, nb072AlphaDummy040 x y H), (nb072AlphaDummy114 A B R S_cls H, nb072AlphaDummy115 x y H), (nb072AlphaDummy042 A B R S_cls H, nb072AlphaDummy043 x y H), (nb072AlphaDummy001 A B R S_cls H, y), (nb072AlphaDummy000 A B R S_cls H, x)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb072AlphaDummy039 A B R S_cls H)) (Compiler.CompactSourceSyntax.synCfv H (SemanticCore.Class.cv (nb072AlphaDummy001 A B R S_cls H)))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb072AlphaDummy038 A B R S_cls H)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb072AlphaDummy039 A B R S_cls H))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb072AlphaDummy041 x y H)) (Compiler.CompactSourceSyntax.synCfv H (SemanticCore.Class.cv y))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb072AlphaDummy040 x y H)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb072AlphaDummy041 x y H))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))).neg)

Checked nominal proof certificate identified upstream as nb072_split_alpha_0006.

Equations

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb072_focused_notmem_0032 (A B R S_cls H : SemanticCore.Class) : nb072AlphaDummy001 A B R S_cls H ∉ S_cls.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb072_focused_notmem_0033 (A B R S_cls H : SemanticCore.Class) : nb072AlphaDummy000 A B R S_cls H ∉ S_cls.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb072_compact_envfresh_0034 (x y : SemanticCore.Var) (A B R S_cls H : SemanticCore.Class) (dv_S_x : x ∉ S_cls.fv) (dv_S_y : y ∉ S_cls.fv) : Nominal.TEnvFresh [(nb072AlphaDummy001 A B R S_cls H, y), (nb072AlphaDummy000 A B R S_cls H, x)] S_cls.fv

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb072FocusedRefl0005 (x y : SemanticCore.Var) (A B R S_cls H : SemanticCore.Class) (dv_S_x : x ∉ S_cls.fv) (dv_S_y : y ∉ S_cls.fv) : Nominal.TReflOn [(nb072AlphaDummy001 A B R S_cls H, y), (nb072AlphaDummy000 A B R S_cls H, x)] S_cls.fv

Checked nominal proof certificate identified upstream as nb072_focused_refl_0005.

Equations

• NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb072FocusedRefl0005 x y A B R S_cls H dv_S_x dv_S_y = ⋯.reflOn