Documentation

LeanPool.NFWeakPartition.AlphaSupport.NAR4H5C095M3Part019Stage1

NF weak partition development: NAR4H5C095M3Part019.

source
noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095SplitAlpha0029 (x u : SemanticCore.Var) (D R S_cls : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) (dv_D_f : f ∉ D.fv) (dv_D_u : u ∉ D.fv) (dv_D_x : x ∉ D.fv) (dv_R_f : f ∉ R.fv) (dv_R_u : u ∉ R.fv) (dv_R_x : x ∉ R.fv) (dv_f_u : f ≠ u) (dv_f_x : f ≠ x) (dv_u_x : u ≠ x) :
Nominal.TAlphaWff [(nb095AlphaDummy001 D R S_cls E, u), (nb095AlphaDummy002 D R S_cls E, x), (nb095AlphaDummy000 D R S_cls E, f)] ((Compiler.CompactSourceSyntax.synWfun (SemanticCore.Class.cv (nb095AlphaDummy000 D R S_cls E))).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCdm (SemanticCore.Class.cv (nb095AlphaDummy000 D R S_cls E))) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (nb095AlphaDummy002 D R S_cls E)))))).neg) ((Compiler.CompactSourceSyntax.synWfun (SemanticCore.Class.cv f)).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCdm (SemanticCore.Class.cv f)) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x))))).neg)

Checked nominal proof certificate identified upstream as nb095_split_alpha_0029.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_compact_fv_empty_0222 (D R S_cls E : SemanticCore.Class) :
    nb095AlphaDummy293 D R S_cls E ∉ ∅
    source
    theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_compact_fv_empty_0223 (u : SemanticCore.Var) (S_cls : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) :
    nb095AlphaDummy294 u S_cls f E ∉ ∅
    source
    theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_compact_fv_empty_0224 (D R S_cls E : SemanticCore.Class) :
    nb095AlphaDummy291 D R S_cls E ∉ ∅
    source
    theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_compact_fv_empty_0225 (u : SemanticCore.Var) (S_cls : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) :
    nb095AlphaDummy292 u S_cls f E ∉ ∅