Documentation

LeanPool.NFWeakPartition.AlphaSupport.NAR4H5C095M3Part018Stage3

NF weak partition development: NAR4H5C095M3Part018.

source
noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095SplitAlpha0027 (x u : SemanticCore.Var) (D R S_cls : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) :
Nominal.TAlphaWff [(nb095AlphaDummy261 D R S_cls E, nb095AlphaDummy262 x R), (nb095AlphaDummy259 D R S_cls E, nb095AlphaDummy260 x R), (nb095AlphaDummy250 D R S_cls E, nb095AlphaDummy252 x R), (nb095AlphaDummy249 D R S_cls E, nb095AlphaDummy251 x R), (nb095AlphaDummy247 D R S_cls E, nb095AlphaDummy248 x D R), (nb095AlphaDummy245 D R S_cls E, nb095AlphaDummy246 x D R), (nb095AlphaDummy001 D R S_cls E, u), (nb095AlphaDummy002 D R S_cls E, x), (nb095AlphaDummy000 D R S_cls E, f)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy261 D R S_cls E)) (SemanticCore.Class.cab (nb095AlphaDummy255 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy256 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy250 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy255 D R S_cls E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy256 D R S_cls E))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy261 D R S_cls E)) (SemanticCore.Class.cab (nb095AlphaDummy255 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy256 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy250 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy255 D R S_cls E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy256 D R S_cls E))))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy262 x R)) (SemanticCore.Class.cab (nb095AlphaDummy257 x R) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy258 x R) (SemanticCore.Class.cv (nb095AlphaDummy252 x R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy257 x R)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy258 x R))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy262 x R)) (SemanticCore.Class.cab (nb095AlphaDummy257 x R) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy258 x R) (SemanticCore.Class.cv (nb095AlphaDummy252 x R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy257 x R)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy258 x R))))))).neg)

Checked nominal proof certificate identified upstream as nb095_split_alpha_0027.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095SplitAlpha0028 (x u : SemanticCore.Var) (D R S_cls : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) :
    Nominal.TAlphaWff [(nb095AlphaDummy287 D R S_cls E, nb095AlphaDummy288 x R), (nb095AlphaDummy256 D R S_cls E, nb095AlphaDummy258 x R), (nb095AlphaDummy255 D R S_cls E, nb095AlphaDummy257 x R), (nb095AlphaDummy285 D R S_cls E, nb095AlphaDummy286 x R), (nb095AlphaDummy259 D R S_cls E, nb095AlphaDummy260 x R), (nb095AlphaDummy250 D R S_cls E, nb095AlphaDummy252 x R), (nb095AlphaDummy249 D R S_cls E, nb095AlphaDummy251 x R), (nb095AlphaDummy247 D R S_cls E, nb095AlphaDummy248 x D R), (nb095AlphaDummy245 D R S_cls E, nb095AlphaDummy246 x D R), (nb095AlphaDummy001 D R S_cls E, u), (nb095AlphaDummy002 D R S_cls E, x), (nb095AlphaDummy000 D R S_cls E, f)] (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy287 D R S_cls E)) (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy256 D R S_cls E))))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy287 D R S_cls E)) (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))).neg (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy288 x R)) (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy258 x R))))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy288 x R)) (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))).neg

    Checked nominal proof certificate identified upstream as nb095_split_alpha_0028.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_focused_notmem_0010 (D R S_cls E : SemanticCore.Class) :
      nb095AlphaDummy250 D R S_cls E ∉ R.fv
      source
      theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_wpp_notmem_0738 (D R S_cls E : SemanticCore.Class) :
      nb095AlphaDummy250 D R S_cls E ∉ (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)).fv
      source
      theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_focused_notmem_0011 (x : SemanticCore.Var) (R : SemanticCore.Class) :
      nb095AlphaDummy252 x R ∉ R.fv
      source
      theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_wpp_notmem_0739 (x : SemanticCore.Var) (R : SemanticCore.Class) :
      nb095AlphaDummy252 x R ∉ (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)).fv
      source
      theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_focused_notmem_0012 (D R S_cls E : SemanticCore.Class) :
      nb095AlphaDummy249 D R S_cls E ∉ R.fv
      source
      theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_wpp_notmem_0740 (D R S_cls E : SemanticCore.Class) :
      nb095AlphaDummy249 D R S_cls E ∉ (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)).fv
      source
      theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_focused_notmem_0013 (x : SemanticCore.Var) (R : SemanticCore.Class) :
      nb095AlphaDummy251 x R ∉ R.fv
      source
      theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_wpp_notmem_0741 (x : SemanticCore.Var) (R : SemanticCore.Class) :
      nb095AlphaDummy251 x R ∉ (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)).fv
      source
      theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_focused_notmem_0014 (D R S_cls E : SemanticCore.Class) :
      nb095AlphaDummy247 D R S_cls E ∉ R.fv
      source
      theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_wpp_notmem_0742 (D R S_cls E : SemanticCore.Class) :
      nb095AlphaDummy247 D R S_cls E ∉ (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)).fv
      source
      theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_focused_notmem_0015 (x : SemanticCore.Var) (D R : SemanticCore.Class) :
      nb095AlphaDummy248 x D R ∉ R.fv
      source
      theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_wpp_notmem_0743 (x : SemanticCore.Var) (D R : SemanticCore.Class) :
      nb095AlphaDummy248 x D R ∉ (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)).fv
      source
      theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_focused_notmem_0016 (D R S_cls E : SemanticCore.Class) :
      nb095AlphaDummy245 D R S_cls E ∉ R.fv
      source
      theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_wpp_notmem_0744 (D R S_cls E : SemanticCore.Class) :
      nb095AlphaDummy245 D R S_cls E ∉ (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)).fv
      source
      theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_focused_notmem_0017 (x : SemanticCore.Var) (D R : SemanticCore.Class) :
      nb095AlphaDummy246 x D R ∉ R.fv
      source
      theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_wpp_notmem_0745 (x : SemanticCore.Var) (D R : SemanticCore.Class) :
      nb095AlphaDummy246 x D R ∉ (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)).fv
      source
      theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_focused_notmem_0018 (D R S_cls E : SemanticCore.Class) :
      nb095AlphaDummy001 D R S_cls E ∉ R.fv
      source
      theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_wpp_notmem_0746 (D R S_cls E : SemanticCore.Class) :
      nb095AlphaDummy001 D R S_cls E ∉ (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)).fv
      source
      theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_wpp_notmem_0747 (u : SemanticCore.Var) (R : SemanticCore.Class) (dv_R_u : u ∉ R.fv) :
      u ∉ (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)).fv
      source
      theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_focused_notmem_0019 (D R S_cls E : SemanticCore.Class) :
      nb095AlphaDummy002 D R S_cls E ∉ R.fv
      source
      theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_wpp_notmem_0748 (D R S_cls E : SemanticCore.Class) :
      nb095AlphaDummy002 D R S_cls E ∉ (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)).fv
      source
      theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_wpp_notmem_0749 (x : SemanticCore.Var) (R : SemanticCore.Class) (dv_R_x : x ∉ R.fv) :
      x ∉ (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)).fv
      source
      theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_focused_notmem_0020 (D R S_cls E : SemanticCore.Class) :
      nb095AlphaDummy000 D R S_cls E ∉ R.fv
      source
      theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_wpp_notmem_0750 (D R S_cls E : SemanticCore.Class) :
      nb095AlphaDummy000 D R S_cls E ∉ (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)).fv
      source
      theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_wpp_notmem_0751 (R : SemanticCore.Class) (f : SemanticCore.Var) (dv_R_f : f ∉ R.fv) :
      f ∉ (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)).fv
      source
      theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_compact_envfresh_0103 (x u : SemanticCore.Var) (D R S_cls : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) (dv_R_f : f ∉ R.fv) (dv_R_u : u ∉ R.fv) (dv_R_x : x ∉ R.fv) :
      Nominal.TEnvFresh [(nb095AlphaDummy250 D R S_cls E, nb095AlphaDummy252 x R), (nb095AlphaDummy249 D R S_cls E, nb095AlphaDummy251 x R), (nb095AlphaDummy247 D R S_cls E, nb095AlphaDummy248 x D R), (nb095AlphaDummy245 D R S_cls E, nb095AlphaDummy246 x D R), (nb095AlphaDummy001 D R S_cls E, u), (nb095AlphaDummy002 D R S_cls E, x), (nb095AlphaDummy000 D R S_cls E, f)] (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)).fv