Documentation

LeanPool.NFWeakPartition.AlphaSupport.NAR4C084C001Part004Stage1

NF weak partition development: NAR4C084C001Part004.

source
noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084SplitAlpha0001 (x y : SemanticCore.Var) (A B R : SemanticCore.Class) (d : SemanticCore.Var) :
Nominal.TAlphaWff [(nb084AlphaDummy010 A B R, nb084AlphaDummy012 x y A R), (nb084AlphaDummy009 A B R, nb084AlphaDummy011 x y A R), (nb084AlphaDummy039 A B R, nb084AlphaDummy040 x y A R), (nb084AlphaDummy013 A B R, nb084AlphaDummy014 x y A R), (nb084AlphaDummy004 A B R, nb084AlphaDummy006 x y A R), (nb084AlphaDummy003 A B R, nb084AlphaDummy005 x y A R), (nb084AlphaDummy002 A B R, y), (nb084AlphaDummy001 A B R, x), (nb084AlphaDummy000 A B R, d)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb084AlphaDummy010 A B R)) (SemanticCore.Class.cv (nb084AlphaDummy004 A B R))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb084AlphaDummy009 A B R)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb084AlphaDummy010 A B R))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb084AlphaDummy012 x y A R)) (SemanticCore.Class.cv (nb084AlphaDummy006 x y A R))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb084AlphaDummy011 x y A R)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb084AlphaDummy012 x y A R))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))).neg)

Checked nominal proof certificate identified upstream as nb084_split_alpha_0001.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_focused_notmem_0010 (A B R : SemanticCore.Class) :
    nb084AlphaDummy004 A B R ∉ R.fv
    source
    theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_focused_notmem_0011 (x y : SemanticCore.Var) (A R : SemanticCore.Class) :
    nb084AlphaDummy006 x y A R ∉ R.fv
    source
    theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_focused_notmem_0012 (A B R : SemanticCore.Class) :
    nb084AlphaDummy003 A B R ∉ R.fv
    source
    theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_focused_notmem_0013 (x y : SemanticCore.Var) (A R : SemanticCore.Class) :
    nb084AlphaDummy005 x y A R ∉ R.fv
    source
    theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_focused_notmem_0014 (A B R : SemanticCore.Class) :
    nb084AlphaDummy002 A B R ∉ R.fv
    source
    theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_focused_notmem_0015 (A B R : SemanticCore.Class) :
    nb084AlphaDummy001 A B R ∉ R.fv
    source
    theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_focused_notmem_0016 (A B R : SemanticCore.Class) :
    nb084AlphaDummy000 A B R ∉ R.fv
    source
    theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_compact_envfresh_0012 (x y : SemanticCore.Var) (A B R : SemanticCore.Class) (d : SemanticCore.Var) (dv_R_d : d ∉ R.fv) (dv_R_x : x ∉ R.fv) (dv_R_y : y ∉ R.fv) :
    Nominal.TEnvFresh [(nb084AlphaDummy004 A B R, nb084AlphaDummy006 x y A R), (nb084AlphaDummy003 A B R, nb084AlphaDummy005 x y A R), (nb084AlphaDummy002 A B R, y), (nb084AlphaDummy001 A B R, x), (nb084AlphaDummy000 A B R, d)] R.fv