Nominal proof certificates grouped in dependency order.

Certificates from NAR4C072C001Part009.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb072SplitAlpha0001 (x y : SemanticCore.Var) (A B R S_cls H : SemanticCore.Class) (dv_x_y : x ≠ y) : Nominal.TAlphaWff [(nb072AlphaDummy060 A B R S_cls H, nb072AlphaDummy061 x H), (nb072AlphaDummy058 A B R S_cls H, nb072AlphaDummy059 x H), (nb072AlphaDummy046 A B R S_cls H, nb072AlphaDummy047 x H), (nb072AlphaDummy048 A B R S_cls H, nb072AlphaDummy049 x H), (nb072AlphaDummy051 A B R S_cls H, nb072AlphaDummy053 x H), (nb072AlphaDummy050 A B R S_cls H, nb072AlphaDummy052 x H), (nb072AlphaDummy039 A B R S_cls H, nb072AlphaDummy041 x y H), (nb072AlphaDummy038 A B R S_cls H, nb072AlphaDummy040 x y H), (nb072AlphaDummy044 A B R S_cls H, nb072AlphaDummy045 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 (nb072AlphaDummy060 A B R S_cls H)) (SemanticCore.Class.cab (nb072AlphaDummy054 A B R S_cls H) (Compiler.CompactSourceSyntax.synWrex (nb072AlphaDummy055 A B R S_cls H) (SemanticCore.Class.cv (nb072AlphaDummy000 A B R S_cls H)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb072AlphaDummy054 A B R S_cls H)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb072AlphaDummy055 A B R S_cls H))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb072AlphaDummy060 A B R S_cls H)) (SemanticCore.Class.cab (nb072AlphaDummy054 A B R S_cls H) (Compiler.CompactSourceSyntax.synWrex (nb072AlphaDummy055 A B R S_cls H) (SemanticCore.Class.cv (nb072AlphaDummy000 A B R S_cls H)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb072AlphaDummy054 A B R S_cls H)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb072AlphaDummy055 A B R S_cls H))))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb072AlphaDummy061 x H)) (SemanticCore.Class.cab (nb072AlphaDummy056 x H) (Compiler.CompactSourceSyntax.synWrex (nb072AlphaDummy057 x H) (SemanticCore.Class.cv x) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb072AlphaDummy056 x H)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb072AlphaDummy057 x H))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb072AlphaDummy061 x H)) (SemanticCore.Class.cab (nb072AlphaDummy056 x H) (Compiler.CompactSourceSyntax.synWrex (nb072AlphaDummy057 x H) (SemanticCore.Class.cv x) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb072AlphaDummy056 x H)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb072AlphaDummy057 x H))))))).neg)

Checked nominal proof certificate identified upstream as nb072_split_alpha_0001.

Equations

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

Certificates from NAR4C072C001Part010.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb072SplitAlpha0002 (x y : SemanticCore.Var) (A B R S_cls H : SemanticCore.Class) : Nominal.TAlphaWff [(nb072AlphaDummy088 A B R S_cls H, nb072AlphaDummy089 x H), (nb072AlphaDummy086 A B R S_cls H, nb072AlphaDummy087 x H), (nb072AlphaDummy055 A B R S_cls H, nb072AlphaDummy057 x H), (nb072AlphaDummy054 A B R S_cls H, nb072AlphaDummy056 x H), (nb072AlphaDummy084 A B R S_cls H, nb072AlphaDummy085 x H), (nb072AlphaDummy058 A B R S_cls H, nb072AlphaDummy059 x H), (nb072AlphaDummy046 A B R S_cls H, nb072AlphaDummy047 x H), (nb072AlphaDummy048 A B R S_cls H, nb072AlphaDummy049 x H), (nb072AlphaDummy051 A B R S_cls H, nb072AlphaDummy053 x H), (nb072AlphaDummy050 A B R S_cls H, nb072AlphaDummy052 x H), (nb072AlphaDummy039 A B R S_cls H, nb072AlphaDummy041 x y H), (nb072AlphaDummy038 A B R S_cls H, nb072AlphaDummy040 x y H), (nb072AlphaDummy044 A B R S_cls H, nb072AlphaDummy045 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 (nb072AlphaDummy088 A B R S_cls H)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb072AlphaDummy055 A B R S_cls H)))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb072AlphaDummy088 A B R S_cls H)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb072AlphaDummy055 A B R S_cls H)))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb072AlphaDummy089 x H)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb072AlphaDummy057 x H)))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb072AlphaDummy089 x H)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb072AlphaDummy057 x H)))).neg)

Checked nominal proof certificate identified upstream as nb072_split_alpha_0002.

Equations

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb072_focused_notmem_0005 (x : SemanticCore.Var) (H : SemanticCore.Class) : nb072AlphaDummy047 x H ∉ H.fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb072_focused_notmem_0007 (x : SemanticCore.Var) (H : SemanticCore.Class) : nb072AlphaDummy049 x H ∉ H.fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb072_focused_notmem_0009 (x : SemanticCore.Var) (H : SemanticCore.Class) : nb072AlphaDummy053 x H ∉ H.fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb072_focused_notmem_0011 (x : SemanticCore.Var) (H : SemanticCore.Class) : nb072AlphaDummy052 x H ∉ H.fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb072_focused_notmem_0013 (x y : SemanticCore.Var) (H : SemanticCore.Class) : nb072AlphaDummy041 x y H ∉ H.fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb072_focused_notmem_0015 (x y : SemanticCore.Var) (H : SemanticCore.Class) : nb072AlphaDummy040 x y H ∉ H.fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb072_focused_notmem_0017 (x y : SemanticCore.Var) (H : SemanticCore.Class) : nb072AlphaDummy045 x y H ∉ H.fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb072_focused_notmem_0019 (x y : SemanticCore.Var) (H : SemanticCore.Class) : nb072AlphaDummy043 x y H ∉ H.fv

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

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

Certificates from NAR4C072C001Part011.

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb072_compact_envfresh_0018 (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.TEnvFresh [(nb072AlphaDummy046 A B R S_cls H, nb072AlphaDummy047 x H), (nb072AlphaDummy048 A B R S_cls H, nb072AlphaDummy049 x H), (nb072AlphaDummy051 A B R S_cls H, nb072AlphaDummy053 x H), (nb072AlphaDummy050 A B R S_cls H, nb072AlphaDummy052 x H), (nb072AlphaDummy039 A B R S_cls H, nb072AlphaDummy041 x y H), (nb072AlphaDummy038 A B R S_cls H, nb072AlphaDummy040 x y H), (nb072AlphaDummy044 A B R S_cls H, nb072AlphaDummy045 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)] H.fv

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb072FocusedRefl0003 (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.TReflOn [(nb072AlphaDummy046 A B R S_cls H, nb072AlphaDummy047 x H), (nb072AlphaDummy048 A B R S_cls H, nb072AlphaDummy049 x H), (nb072AlphaDummy051 A B R S_cls H, nb072AlphaDummy053 x H), (nb072AlphaDummy050 A B R S_cls H, nb072AlphaDummy052 x H), (nb072AlphaDummy039 A B R S_cls H, nb072AlphaDummy041 x y H), (nb072AlphaDummy038 A B R S_cls H, nb072AlphaDummy040 x y H), (nb072AlphaDummy044 A B R S_cls H, nb072AlphaDummy045 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)] H.fv

Checked nominal proof certificate identified upstream as nb072_focused_refl_0003.

Equations

• NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb072FocusedRefl0003 x y A B R S_cls H dv_H_x dv_H_y = ⋯.reflOn