Documentation

LeanPool.NFWeakPartition.NAR4H5C091M3BPart005

NF weak partition development: NAR4H5C091M3BPart005.

source
noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091SplitAlpha0005 (D R : SemanticCore.Class) (p : SemanticCore.Var) :
Nominal.TAlphaWff [(nb091AlphaDummy125 D R, nb091AlphaDummy126 R p), (nb091AlphaDummy123 D R, nb091AlphaDummy124 R p), (nb091AlphaDummy106 D R, nb091AlphaDummy108 R p), (nb091AlphaDummy105 D R, nb091AlphaDummy107 R p), (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)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb091AlphaDummy125 D R)) (SemanticCore.Class.cab (nb091AlphaDummy119 D R) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy120 D R) (SemanticCore.Class.cv (nb091AlphaDummy106 D R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy119 D R)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy120 D R))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb091AlphaDummy125 D R)) (SemanticCore.Class.cab (nb091AlphaDummy119 D R) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy120 D R) (SemanticCore.Class.cv (nb091AlphaDummy106 D R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy119 D R)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy120 D R))))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb091AlphaDummy126 R p)) (SemanticCore.Class.cab (nb091AlphaDummy121 R p) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy122 R p) (SemanticCore.Class.cv (nb091AlphaDummy108 R p)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy121 R p)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy122 R p))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb091AlphaDummy126 R p)) (SemanticCore.Class.cab (nb091AlphaDummy121 R p) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy122 R p) (SemanticCore.Class.cv (nb091AlphaDummy108 R p)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy121 R p)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy122 R p))))))).neg)

Checked nominal proof certificate identified upstream as nb091_split_alpha_0005.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091SplitAlpha0006 (D R : SemanticCore.Class) (p : SemanticCore.Var) :
    Nominal.TAlphaWff [(nb091AlphaDummy153 D R, nb091AlphaDummy154 R p), (nb091AlphaDummy151 D R, nb091AlphaDummy152 R p), (nb091AlphaDummy120 D R, nb091AlphaDummy122 R p), (nb091AlphaDummy119 D R, nb091AlphaDummy121 R p), (nb091AlphaDummy149 D R, nb091AlphaDummy150 R p), (nb091AlphaDummy123 D R, nb091AlphaDummy124 R p), (nb091AlphaDummy106 D R, nb091AlphaDummy108 R p), (nb091AlphaDummy105 D R, nb091AlphaDummy107 R p), (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)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb091AlphaDummy153 D R)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy120 D R)))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb091AlphaDummy153 D R)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy120 D R)))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb091AlphaDummy154 R p)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy122 R p)))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb091AlphaDummy154 R p)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy122 R p)))).neg)

    Checked nominal proof certificate identified upstream as nb091_split_alpha_0006.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_focused_notmem_0056 (D R : SemanticCore.Class) :
      nb091AlphaDummy106 D R ∉ R.fv
      source
      theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_wpp_notmem_0404 (D R : SemanticCore.Class) :
      nb091AlphaDummy106 D R ∉ (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)).fv
      source
      theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_focused_notmem_0057 (R : SemanticCore.Class) (p : SemanticCore.Var) :
      nb091AlphaDummy108 R p ∉ R.fv
      source
      theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_wpp_notmem_0405 (R : SemanticCore.Class) (p : SemanticCore.Var) :
      nb091AlphaDummy108 R p ∉ (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)).fv
      source
      theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_focused_notmem_0058 (D R : SemanticCore.Class) :
      nb091AlphaDummy105 D R ∉ R.fv
      source
      theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_wpp_notmem_0406 (D R : SemanticCore.Class) :
      nb091AlphaDummy105 D R ∉ (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)).fv
      source
      theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_focused_notmem_0059 (R : SemanticCore.Class) (p : SemanticCore.Var) :
      nb091AlphaDummy107 R p ∉ R.fv
      source
      theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_wpp_notmem_0407 (R : SemanticCore.Class) (p : SemanticCore.Var) :
      nb091AlphaDummy107 R p ∉ (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)).fv
      source
      theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_focused_notmem_0060 (D R : SemanticCore.Class) :
      nb091AlphaDummy103 D R ∉ R.fv
      source
      theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_wpp_notmem_0408 (D R : SemanticCore.Class) :
      nb091AlphaDummy103 D R ∉ (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)).fv
      source
      theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_focused_notmem_0061 (D R : SemanticCore.Class) (p : SemanticCore.Var) :
      nb091AlphaDummy104 D R p ∉ R.fv
      source
      theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_wpp_notmem_0409 (D R : SemanticCore.Class) (p : SemanticCore.Var) :
      nb091AlphaDummy104 D R p ∉ (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)).fv
      source
      theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_focused_notmem_0062 (D R : SemanticCore.Class) :
      nb091AlphaDummy101 D R ∉ R.fv
      source
      theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_wpp_notmem_0410 (D R : SemanticCore.Class) :
      nb091AlphaDummy101 D R ∉ (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)).fv
      source
      theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_focused_notmem_0063 (D R : SemanticCore.Class) (p : SemanticCore.Var) :
      nb091AlphaDummy102 D R p ∉ R.fv
      source
      theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_wpp_notmem_0411 (D R : SemanticCore.Class) (p : SemanticCore.Var) :
      nb091AlphaDummy102 D R p ∉ (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)).fv