Documentation

LeanPool.NFWeakPartition.NAR4H5C091M3BPart004

NF weak partition development: NAR4H5C091M3BPart004.

source
noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091SplitAlpha0003 (D R : SemanticCore.Class) (p : SemanticCore.Var) :
Nominal.TAlphaWff [(nb091AlphaDummy071 D R, nb091AlphaDummy072 D R p), (nb091AlphaDummy069 D R, nb091AlphaDummy070 D R p), (nb091AlphaDummy060 D R, nb091AlphaDummy062 D R p), (nb091AlphaDummy059 D R, nb091AlphaDummy061 D R p), (nb091AlphaDummy063 D R, nb091AlphaDummy064 D R p), (nb091AlphaDummy057 D R, nb091AlphaDummy058 D R p), (nb091AlphaDummy055 D R, nb091AlphaDummy056 D R p), (nb091AlphaDummy048 D R, nb091AlphaDummy050 D R p), (nb091AlphaDummy047 D R, nb091AlphaDummy049 D R p), (nb091AlphaDummy053 D R, nb091AlphaDummy054 D R p), (nb091AlphaDummy051 D R, nb091AlphaDummy052 D R p), (nb091AlphaDummy045 D R, nb091AlphaDummy046 D R p), (nb091AlphaDummy042 D R, nb091AlphaDummy044 D R p), (nb091AlphaDummy041 D R, nb091AlphaDummy043 D R p), (nb091AlphaDummy001 D R, nb091AlphaDummy002 D R p), (nb091AlphaDummy000 D R, p), (nb091AlphaDummy003 D R, nb091AlphaDummy004 D R p)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb091AlphaDummy071 D R)) (SemanticCore.Class.cab (nb091AlphaDummy065 D R) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy066 D R) (SemanticCore.Class.cv (nb091AlphaDummy059 D R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy065 D R)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy066 D R))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb091AlphaDummy071 D R)) (SemanticCore.Class.cab (nb091AlphaDummy065 D R) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy066 D R) (SemanticCore.Class.cv (nb091AlphaDummy059 D R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy065 D R)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy066 D R))))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb091AlphaDummy072 D R p)) (SemanticCore.Class.cab (nb091AlphaDummy067 D R p) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy068 D R p) (SemanticCore.Class.cv (nb091AlphaDummy061 D R p)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy067 D R p)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy068 D R p))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb091AlphaDummy072 D R p)) (SemanticCore.Class.cab (nb091AlphaDummy067 D R p) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy068 D R p) (SemanticCore.Class.cv (nb091AlphaDummy061 D R p)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy067 D R p)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy068 D R p))))))).neg)

Checked nominal proof certificate identified upstream as nb091_split_alpha_0003.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091SplitAlpha0004 (D R : SemanticCore.Class) (p : SemanticCore.Var) :
    Nominal.TAlphaWff [(nb091AlphaDummy099 D R, nb091AlphaDummy100 D R p), (nb091AlphaDummy097 D R, nb091AlphaDummy098 D R p), (nb091AlphaDummy066 D R, nb091AlphaDummy068 D R p), (nb091AlphaDummy065 D R, nb091AlphaDummy067 D R p), (nb091AlphaDummy095 D R, nb091AlphaDummy096 D R p), (nb091AlphaDummy069 D R, nb091AlphaDummy070 D R p), (nb091AlphaDummy060 D R, nb091AlphaDummy062 D R p), (nb091AlphaDummy059 D R, nb091AlphaDummy061 D R p), (nb091AlphaDummy063 D R, nb091AlphaDummy064 D R p), (nb091AlphaDummy057 D R, nb091AlphaDummy058 D R p), (nb091AlphaDummy055 D R, nb091AlphaDummy056 D R p), (nb091AlphaDummy048 D R, nb091AlphaDummy050 D R p), (nb091AlphaDummy047 D R, nb091AlphaDummy049 D R p), (nb091AlphaDummy053 D R, nb091AlphaDummy054 D R p), (nb091AlphaDummy051 D R, nb091AlphaDummy052 D R p), (nb091AlphaDummy045 D R, nb091AlphaDummy046 D R p), (nb091AlphaDummy042 D R, nb091AlphaDummy044 D R p), (nb091AlphaDummy041 D R, nb091AlphaDummy043 D R p), (nb091AlphaDummy001 D R, nb091AlphaDummy002 D R p), (nb091AlphaDummy000 D R, p), (nb091AlphaDummy003 D R, nb091AlphaDummy004 D R p)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb091AlphaDummy099 D R)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy066 D R)))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb091AlphaDummy099 D R)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy066 D R)))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb091AlphaDummy100 D R p)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy068 D R p)))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb091AlphaDummy100 D R p)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy068 D R p)))).neg)

    Checked nominal proof certificate identified upstream as nb091_split_alpha_0004.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_focused_notmem_0028 (D R : SemanticCore.Class) :
      nb091AlphaDummy103 D R ∉ D.fv
      source
      theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_focused_notmem_0029 (D R : SemanticCore.Class) (p : SemanticCore.Var) :
      nb091AlphaDummy104 D R p ∉ D.fv
      source
      theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_focused_notmem_0030 (D R : SemanticCore.Class) :
      nb091AlphaDummy101 D R ∉ D.fv
      source
      theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_focused_notmem_0031 (D R : SemanticCore.Class) (p : SemanticCore.Var) :
      nb091AlphaDummy102 D R p ∉ D.fv
      source
      theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_focused_notmem_0032 (D R : SemanticCore.Class) :
      nb091AlphaDummy060 D R ∉ D.fv
      source
      theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_focused_notmem_0033 (D R : SemanticCore.Class) (p : SemanticCore.Var) :
      nb091AlphaDummy062 D R p ∉ D.fv
      source
      theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_focused_notmem_0034 (D R : SemanticCore.Class) :
      nb091AlphaDummy059 D R ∉ D.fv
      source
      theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_focused_notmem_0035 (D R : SemanticCore.Class) (p : SemanticCore.Var) :
      nb091AlphaDummy061 D R p ∉ D.fv
      source
      theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_focused_notmem_0036 (D R : SemanticCore.Class) :
      nb091AlphaDummy063 D R ∉ D.fv
      source
      theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_focused_notmem_0037 (D R : SemanticCore.Class) (p : SemanticCore.Var) :
      nb091AlphaDummy064 D R p ∉ D.fv
      source
      theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_focused_notmem_0038 (D R : SemanticCore.Class) :
      nb091AlphaDummy057 D R ∉ D.fv
      source
      theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_focused_notmem_0039 (D R : SemanticCore.Class) (p : SemanticCore.Var) :
      nb091AlphaDummy058 D R p ∉ D.fv
      source
      theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_focused_notmem_0040 (D R : SemanticCore.Class) :
      nb091AlphaDummy055 D R ∉ D.fv
      source
      theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_focused_notmem_0041 (D R : SemanticCore.Class) (p : SemanticCore.Var) :
      nb091AlphaDummy056 D R p ∉ D.fv
      source
      theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_focused_notmem_0042 (D R : SemanticCore.Class) :
      nb091AlphaDummy048 D R ∉ D.fv
      source
      theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_focused_notmem_0043 (D R : SemanticCore.Class) (p : SemanticCore.Var) :
      nb091AlphaDummy050 D R p ∉ D.fv
      source
      theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_focused_notmem_0044 (D R : SemanticCore.Class) :
      nb091AlphaDummy047 D R ∉ D.fv
      source
      theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_focused_notmem_0045 (D R : SemanticCore.Class) (p : SemanticCore.Var) :
      nb091AlphaDummy049 D R p ∉ D.fv
      source
      theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_focused_notmem_0046 (D R : SemanticCore.Class) :
      nb091AlphaDummy053 D R ∉ D.fv
      source
      theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_focused_notmem_0047 (D R : SemanticCore.Class) (p : SemanticCore.Var) :
      nb091AlphaDummy054 D R p ∉ D.fv
      source
      theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_focused_notmem_0048 (D R : SemanticCore.Class) :
      nb091AlphaDummy051 D R ∉ D.fv
      source
      theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_focused_notmem_0049 (D R : SemanticCore.Class) (p : SemanticCore.Var) :
      nb091AlphaDummy052 D R p ∉ D.fv
      source
      theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_focused_notmem_0050 (D R : SemanticCore.Class) :
      nb091AlphaDummy045 D R ∉ D.fv
      source
      theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_focused_notmem_0051 (D R : SemanticCore.Class) (p : SemanticCore.Var) :
      nb091AlphaDummy046 D R p ∉ D.fv
      source
      theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_focused_notmem_0052 (D R : SemanticCore.Class) :
      nb091AlphaDummy042 D R ∉ D.fv
      source
      theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_focused_notmem_0053 (D R : SemanticCore.Class) (p : SemanticCore.Var) :
      nb091AlphaDummy044 D R p ∉ D.fv
      source
      theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_focused_notmem_0054 (D R : SemanticCore.Class) :
      nb091AlphaDummy041 D R ∉ D.fv
      source
      theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_focused_notmem_0055 (D R : SemanticCore.Class) (p : SemanticCore.Var) :
      nb091AlphaDummy043 D R p ∉ D.fv
      source
      theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_compact_envfresh_0016 (D R : SemanticCore.Class) (p : SemanticCore.Var) (dv_D_p : p ∉ D.fv) :
      Nominal.TEnvFresh [(nb091AlphaDummy103 D R, nb091AlphaDummy104 D R p), (nb091AlphaDummy101 D R, nb091AlphaDummy102 D R p), (nb091AlphaDummy060 D R, nb091AlphaDummy062 D R p), (nb091AlphaDummy059 D R, nb091AlphaDummy061 D R p), (nb091AlphaDummy063 D R, nb091AlphaDummy064 D R p), (nb091AlphaDummy057 D R, nb091AlphaDummy058 D R p), (nb091AlphaDummy055 D R, nb091AlphaDummy056 D R p), (nb091AlphaDummy048 D R, nb091AlphaDummy050 D R p), (nb091AlphaDummy047 D R, nb091AlphaDummy049 D R p), (nb091AlphaDummy053 D R, nb091AlphaDummy054 D R p), (nb091AlphaDummy051 D R, nb091AlphaDummy052 D R p), (nb091AlphaDummy045 D R, nb091AlphaDummy046 D R p), (nb091AlphaDummy042 D R, nb091AlphaDummy044 D R p), (nb091AlphaDummy041 D R, nb091AlphaDummy043 D R p), (nb091AlphaDummy001 D R, nb091AlphaDummy002 D R p), (nb091AlphaDummy000 D R, p), (nb091AlphaDummy003 D R, nb091AlphaDummy004 D R p)] D.fv
      source
      noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091FocusedRefl0001 (D R : SemanticCore.Class) (p : SemanticCore.Var) (dv_D_p : p ∉ D.fv) :
      Nominal.TReflOn [(nb091AlphaDummy103 D R, nb091AlphaDummy104 D R p), (nb091AlphaDummy101 D R, nb091AlphaDummy102 D R p), (nb091AlphaDummy060 D R, nb091AlphaDummy062 D R p), (nb091AlphaDummy059 D R, nb091AlphaDummy061 D R p), (nb091AlphaDummy063 D R, nb091AlphaDummy064 D R p), (nb091AlphaDummy057 D R, nb091AlphaDummy058 D R p), (nb091AlphaDummy055 D R, nb091AlphaDummy056 D R p), (nb091AlphaDummy048 D R, nb091AlphaDummy050 D R p), (nb091AlphaDummy047 D R, nb091AlphaDummy049 D R p), (nb091AlphaDummy053 D R, nb091AlphaDummy054 D R p), (nb091AlphaDummy051 D R, nb091AlphaDummy052 D R p), (nb091AlphaDummy045 D R, nb091AlphaDummy046 D R p), (nb091AlphaDummy042 D R, nb091AlphaDummy044 D R p), (nb091AlphaDummy041 D R, nb091AlphaDummy043 D R p), (nb091AlphaDummy001 D R, nb091AlphaDummy002 D R p), (nb091AlphaDummy000 D R, p), (nb091AlphaDummy003 D R, nb091AlphaDummy004 D R p)] D.fv

      Checked nominal proof certificate identified upstream as nb091_focused_refl_0001.

      Equations
      Instances For
        source
        theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_compact_fv_empty_0102 (D R : SemanticCore.Class) :
        nb091AlphaDummy106 D R ∉ ∅
        source
        theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_compact_fv_empty_0103 (R : SemanticCore.Class) (p : SemanticCore.Var) :
        nb091AlphaDummy108 R p ∉ ∅
        source
        theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_compact_fv_empty_0104 (D R : SemanticCore.Class) :
        nb091AlphaDummy105 D R ∉ ∅
        source
        theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_compact_fv_empty_0105 (R : SemanticCore.Class) (p : SemanticCore.Var) :
        nb091AlphaDummy107 R p ∉ ∅
        source
        theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_compact_fv_empty_0106 (D R : SemanticCore.Class) :
        nb091AlphaDummy103 D R ∉ ∅
        source
        theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_compact_fv_empty_0107 (D R : SemanticCore.Class) (p : SemanticCore.Var) :
        nb091AlphaDummy104 D R p ∉ ∅
        source
        theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_compact_fv_empty_0108 (D R : SemanticCore.Class) :
        nb091AlphaDummy101 D R ∉ ∅
        source
        theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_compact_fv_empty_0109 (D R : SemanticCore.Class) (p : SemanticCore.Var) :
        nb091AlphaDummy102 D R p ∉ ∅