Documentation

LeanPool.NFWeakPartition.Certificates.NAR4C072C001Block004

Nominal proof certificates grouped in dependency order.

Certificates from NAR4C072C001Part014.

source
noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb072SplitAlpha0005 (x y : SemanticCore.Var) (A B R S_cls H : SemanticCore.Class) :
Nominal.TAlphaWff [(nb072AlphaDummy158 A B R S_cls H, nb072AlphaDummy159 y H), (nb072AlphaDummy156 A B R S_cls H, nb072AlphaDummy157 y H), (nb072AlphaDummy125 A B R S_cls H, nb072AlphaDummy127 y H), (nb072AlphaDummy124 A B R S_cls H, nb072AlphaDummy126 y H), (nb072AlphaDummy154 A B R S_cls H, nb072AlphaDummy155 y H), (nb072AlphaDummy128 A B R S_cls H, nb072AlphaDummy129 y H), (nb072AlphaDummy116 A B R S_cls H, nb072AlphaDummy117 y H), (nb072AlphaDummy118 A B R S_cls H, nb072AlphaDummy119 y H), (nb072AlphaDummy121 A B R S_cls H, nb072AlphaDummy123 y H), (nb072AlphaDummy120 A B R S_cls H, nb072AlphaDummy122 y H), (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 (nb072AlphaDummy158 A B R S_cls H)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb072AlphaDummy125 A B R S_cls H)))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb072AlphaDummy158 A B R S_cls H)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb072AlphaDummy125 A B R S_cls H)))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb072AlphaDummy159 y H)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb072AlphaDummy127 y H)))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb072AlphaDummy159 y H)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb072AlphaDummy127 y H)))).neg)

Checked nominal proof certificate identified upstream as nb072_split_alpha_0005.

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

    Certificates from NAR4C072C001Part015.

    source
    theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb072_focused_notmem_0022 (A B R S_cls H : SemanticCore.Class) :
    nb072AlphaDummy116 A B R S_cls H ∉ H.fv
    source
    theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb072_focused_notmem_0023 (y : SemanticCore.Var) (H : SemanticCore.Class) :
    nb072AlphaDummy117 y H ∉ H.fv
    source
    theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb072_focused_notmem_0024 (A B R S_cls H : SemanticCore.Class) :
    nb072AlphaDummy118 A B R S_cls H ∉ H.fv
    source
    theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb072_focused_notmem_0025 (y : SemanticCore.Var) (H : SemanticCore.Class) :
    nb072AlphaDummy119 y H ∉ H.fv
    source
    theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb072_focused_notmem_0026 (A B R S_cls H : SemanticCore.Class) :
    nb072AlphaDummy121 A B R S_cls H ∉ H.fv
    source
    theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb072_focused_notmem_0027 (y : SemanticCore.Var) (H : SemanticCore.Class) :
    nb072AlphaDummy123 y H ∉ H.fv
    source
    theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb072_focused_notmem_0028 (A B R S_cls H : SemanticCore.Class) :
    nb072AlphaDummy120 A B R S_cls H ∉ H.fv
    source
    theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb072_focused_notmem_0029 (y : SemanticCore.Var) (H : SemanticCore.Class) :
    nb072AlphaDummy122 y H ∉ H.fv
    source
    theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb072_focused_notmem_0030 (A B R S_cls H : SemanticCore.Class) :
    nb072AlphaDummy114 A B R S_cls H ∉ H.fv
    source
    theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb072_focused_notmem_0031 (x y : SemanticCore.Var) (H : SemanticCore.Class) :
    nb072AlphaDummy115 x y H ∉ H.fv
    source
    theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb072_compact_envfresh_0029 (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 [(nb072AlphaDummy116 A B R S_cls H, nb072AlphaDummy117 y H), (nb072AlphaDummy118 A B R S_cls H, nb072AlphaDummy119 y H), (nb072AlphaDummy121 A B R S_cls H, nb072AlphaDummy123 y H), (nb072AlphaDummy120 A B R S_cls H, nb072AlphaDummy122 y H), (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)] H.fv
    source
    noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb072FocusedRefl0004 (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 [(nb072AlphaDummy116 A B R S_cls H, nb072AlphaDummy117 y H), (nb072AlphaDummy118 A B R S_cls H, nb072AlphaDummy119 y H), (nb072AlphaDummy121 A B R S_cls H, nb072AlphaDummy123 y H), (nb072AlphaDummy120 A B R S_cls H, nb072AlphaDummy122 y H), (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)] H.fv

    Checked nominal proof certificate identified upstream as nb072_focused_refl_0004.

    Equations
    Instances For