Documentation

LeanPool.NFWeakPartition.NAR4C087C001Part003

NF weak partition development: NAR4C087C001Part003.

source
noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb087SplitAlpha0000 (A B C R : SemanticCore.Class) (d : SemanticCore.Var) (dv_C_d : d ∉ C.fv) :
Nominal.TAlphaWff [(nb087AlphaDummy033 A B C R, nb087AlphaDummy034 C d), (nb087AlphaDummy005 A B C R, nb087AlphaDummy006 C d), (nb087AlphaDummy000 A B C R, d)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb087AlphaDummy033 A B C R)) (SemanticCore.Class.cab (nb087AlphaDummy001 A B C R) (Compiler.CompactSourceSyntax.synWrex (nb087AlphaDummy002 A B C R) C (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb087AlphaDummy001 A B C R)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb087AlphaDummy002 A B C R))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb087AlphaDummy033 A B C R)) (SemanticCore.Class.cab (nb087AlphaDummy001 A B C R) (Compiler.CompactSourceSyntax.synWrex (nb087AlphaDummy002 A B C R) C (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb087AlphaDummy001 A B C R)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb087AlphaDummy002 A B C R))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb087AlphaDummy034 C d)) (SemanticCore.Class.cab (nb087AlphaDummy003 C d) (Compiler.CompactSourceSyntax.synWrex (nb087AlphaDummy004 C d) C (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb087AlphaDummy003 C d)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb087AlphaDummy004 C d))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb087AlphaDummy034 C d)) (SemanticCore.Class.cab (nb087AlphaDummy003 C d) (Compiler.CompactSourceSyntax.synWrex (nb087AlphaDummy004 C d) C (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb087AlphaDummy003 C d)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb087AlphaDummy004 C d))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg)

Checked nominal proof certificate identified upstream as nb087_split_alpha_0000.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb087_focused_notmem_0009 (A B C R : SemanticCore.Class) :
    nb087AlphaDummy000 A B C R ∉ A.fv
    source
    theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb087_focused_notmem_0010 (A B C R : SemanticCore.Class) :
    nb087AlphaDummy000 A B C R ∉ B.fv
    source
    theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb087_focused_notmem_0011 (A B C R : SemanticCore.Class) :
    nb087AlphaDummy000 A B C R ∉ R.fv
    source
    theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb087_wpp_notmem_0090 (A B C R : SemanticCore.Class) :
    nb087AlphaDummy000 A B C R ∉ (Compiler.CompactSourceSyntax.synCfdrowrel R A B).fv
    source
    theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb087_wpp_notmem_0091 (A B R : SemanticCore.Class) (d : SemanticCore.Var) (dv_A_d : d ∉ A.fv) (dv_B_d : d ∉ B.fv) (dv_R_d : d ∉ R.fv) :
    d ∉ (Compiler.CompactSourceSyntax.synCfdrowrel R A B).fv
    source
    theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb087_compact_envfresh_0008 (A B C R : SemanticCore.Class) (d : SemanticCore.Var) (dv_A_d : d ∉ A.fv) (dv_B_d : d ∉ B.fv) (dv_R_d : d ∉ R.fv) :
    Nominal.TEnvFresh [(nb087AlphaDummy000 A B C R, d)] (Compiler.CompactSourceSyntax.synCfdrowrel R A B).fv
    source
    noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb087WppRefl0007 (A B C R : SemanticCore.Class) (d : SemanticCore.Var) (dv_A_d : d ∉ A.fv) (dv_B_d : d ∉ B.fv) (dv_R_d : d ∉ R.fv) :
    Nominal.TReflOn [(nb087AlphaDummy000 A B C R, d)] (Compiler.CompactSourceSyntax.synCfdrowrel R A B).fv

    Checked nominal proof certificate identified upstream as nb087_wpp_refl_0007.

    Equations
    Instances For