Documentation

LeanPool.NFWeakPartition.AlphaSupport.NAR4H5C096M3Part002Stage3

NF weak partition development: NAR4H5C096M3Part002.

source
noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb096WppRefl0007 (D R : SemanticCore.Class) (q : SemanticCore.Var) (dv_D_q : q ∉ D.fv) :
Nominal.TReflOn [(nb096AlphaDummy001 D R, nb096AlphaDummy002 D R q), (nb096AlphaDummy000 D R, q), (nb096AlphaDummy003 D R, nb096AlphaDummy004 D R q)] (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 D)).fv

Checked nominal proof certificate identified upstream as nb096_wpp_refl_0007.

Equations
Instances For
    source
    theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb096_focused_notmem_0005 (D R : SemanticCore.Class) :
    nb096AlphaDummy049 D R ∉ D.fv
    source
    theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb096_focused_notmem_0006 (D R : SemanticCore.Class) (q : SemanticCore.Var) :
    nb096AlphaDummy050 D R q ∉ D.fv
    source
    theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb096_focused_notmem_0007 (D R : SemanticCore.Class) :
    nb096AlphaDummy047 D R ∉ D.fv
    source
    theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb096_focused_notmem_0008 (D R : SemanticCore.Class) (q : SemanticCore.Var) :
    nb096AlphaDummy048 D R q ∉ D.fv
    source
    theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb096_focused_notmem_0009 (D R : SemanticCore.Class) :
    nb096AlphaDummy045 D R ∉ D.fv
    source
    theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb096_focused_notmem_0010 (D R : SemanticCore.Class) (q : SemanticCore.Var) :
    nb096AlphaDummy046 D R q ∉ D.fv
    source
    theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb096_focused_notmem_0011 (D R : SemanticCore.Class) :
    nb096AlphaDummy042 D R ∉ D.fv
    source
    theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb096_focused_notmem_0012 (D R : SemanticCore.Class) (q : SemanticCore.Var) :
    nb096AlphaDummy044 D R q ∉ D.fv
    source
    theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb096_focused_notmem_0013 (D R : SemanticCore.Class) :
    nb096AlphaDummy041 D R ∉ D.fv
    source
    theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb096_focused_notmem_0014 (D R : SemanticCore.Class) (q : SemanticCore.Var) :
    nb096AlphaDummy043 D R q ∉ D.fv
    source
    theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb096_compact_envfresh_0008 (D R : SemanticCore.Class) (q : SemanticCore.Var) (dv_D_q : q ∉ D.fv) :
    Nominal.TEnvFresh [(nb096AlphaDummy049 D R, nb096AlphaDummy050 D R q), (nb096AlphaDummy047 D R, nb096AlphaDummy048 D R q), (nb096AlphaDummy045 D R, nb096AlphaDummy046 D R q), (nb096AlphaDummy042 D R, nb096AlphaDummy044 D R q), (nb096AlphaDummy041 D R, nb096AlphaDummy043 D R q), (nb096AlphaDummy001 D R, nb096AlphaDummy002 D R q), (nb096AlphaDummy000 D R, q), (nb096AlphaDummy003 D R, nb096AlphaDummy004 D R q)] D.fv