Documentation

LeanPool.NFWeakPartition.NAR4C083C001Part003

NF weak partition development: NAR4C083C001Part003.

source
noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083SplitAlpha0000 (A B C R : SemanticCore.Class) (b c : SemanticCore.Var) :
Nominal.TAlphaWff [(nb083AlphaDummy032 A B C R, nb083AlphaDummy033 b c), (nb083AlphaDummy006 A B C R, nb083AlphaDummy007 b c), (nb083AlphaDummy001 A B C R, c), (nb083AlphaDummy000 A B C R, b)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb083AlphaDummy032 A B C R)) (SemanticCore.Class.cab (nb083AlphaDummy002 A B C R) (Compiler.CompactSourceSyntax.synWrex (nb083AlphaDummy003 A B C R) (SemanticCore.Class.cv (nb083AlphaDummy001 A B C R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb083AlphaDummy002 A B C R)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb083AlphaDummy003 A B C R))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb083AlphaDummy032 A B C R)) (SemanticCore.Class.cab (nb083AlphaDummy002 A B C R) (Compiler.CompactSourceSyntax.synWrex (nb083AlphaDummy003 A B C R) (SemanticCore.Class.cv (nb083AlphaDummy001 A B C R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb083AlphaDummy002 A B C R)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb083AlphaDummy003 A B C R))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb083AlphaDummy033 b c)) (SemanticCore.Class.cab (nb083AlphaDummy004 b c) (Compiler.CompactSourceSyntax.synWrex (nb083AlphaDummy005 b c) (SemanticCore.Class.cv c) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb083AlphaDummy004 b c)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb083AlphaDummy005 b c))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb083AlphaDummy033 b c)) (SemanticCore.Class.cab (nb083AlphaDummy004 b c) (Compiler.CompactSourceSyntax.synWrex (nb083AlphaDummy005 b c) (SemanticCore.Class.cv c) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb083AlphaDummy004 b c)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb083AlphaDummy005 b c))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg)

Checked nominal proof certificate identified upstream as nb083_split_alpha_0000.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_focused_notmem_0006 (A B C R : SemanticCore.Class) :
    nb083AlphaDummy001 A B C R ∉ R.fv
    source
    theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_focused_notmem_0007 (A B C R : SemanticCore.Class) :
    nb083AlphaDummy000 A B C R ∉ R.fv
    source
    theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_compact_envfresh_0011 (A B C R : SemanticCore.Class) (b c : SemanticCore.Var) (dv_R_b : b ∉ R.fv) (dv_R_c : c ∉ R.fv) :
    Nominal.TEnvFresh [(nb083AlphaDummy001 A B C R, c), (nb083AlphaDummy000 A B C R, b)] R.fv
    source
    noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083FocusedRefl0002 (A B C R : SemanticCore.Class) (b c : SemanticCore.Var) (dv_R_b : b ∉ R.fv) (dv_R_c : c ∉ R.fv) :
    Nominal.TReflOn [(nb083AlphaDummy001 A B C R, c), (nb083AlphaDummy000 A B C R, b)] R.fv

    Checked nominal proof certificate identified upstream as nb083_focused_refl_0002.

    Equations
    Instances For