Documentation

LeanPool.NFWeakPartition.NAR4C072C001Part007

NF weak partition development: NAR4C072C001Part007.

source
noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb072SplitAlpha0000 (x y : SemanticCore.Var) (A B R S_cls H : SemanticCore.Class) :
Nominal.TAlphaWff [(nb072AlphaDummy032 A B R S_cls H, nb072AlphaDummy033 x y), (nb072AlphaDummy006 A B R S_cls H, nb072AlphaDummy007 x y), (nb072AlphaDummy001 A B R S_cls H, y), (nb072AlphaDummy000 A B R S_cls H, x)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb072AlphaDummy032 A B R S_cls H)) (SemanticCore.Class.cab (nb072AlphaDummy002 A B R S_cls H) (Compiler.CompactSourceSyntax.synWrex (nb072AlphaDummy003 A B R S_cls H) (SemanticCore.Class.cv (nb072AlphaDummy001 A B R S_cls H)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb072AlphaDummy002 A B R S_cls H)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb072AlphaDummy003 A B R S_cls H))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb072AlphaDummy032 A B R S_cls H)) (SemanticCore.Class.cab (nb072AlphaDummy002 A B R S_cls H) (Compiler.CompactSourceSyntax.synWrex (nb072AlphaDummy003 A B R S_cls H) (SemanticCore.Class.cv (nb072AlphaDummy001 A B R S_cls H)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb072AlphaDummy002 A B R S_cls H)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb072AlphaDummy003 A B R S_cls H))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb072AlphaDummy033 x y)) (SemanticCore.Class.cab (nb072AlphaDummy004 x y) (Compiler.CompactSourceSyntax.synWrex (nb072AlphaDummy005 x y) (SemanticCore.Class.cv y) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb072AlphaDummy004 x y)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb072AlphaDummy005 x y))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb072AlphaDummy033 x y)) (SemanticCore.Class.cab (nb072AlphaDummy004 x y) (Compiler.CompactSourceSyntax.synWrex (nb072AlphaDummy005 x y) (SemanticCore.Class.cv y) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb072AlphaDummy004 x y)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb072AlphaDummy005 x y))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg)

Checked nominal proof certificate identified upstream as nb072_split_alpha_0000.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb072_focused_notmem_0002 (A B R S_cls H : SemanticCore.Class) :
    nb072AlphaDummy001 A B R S_cls H ∉ R.fv
    source
    theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb072_focused_notmem_0003 (A B R S_cls H : SemanticCore.Class) :
    nb072AlphaDummy000 A B R S_cls H ∉ R.fv
    source
    theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb072_compact_envfresh_0010 (x y : SemanticCore.Var) (A B R S_cls H : SemanticCore.Class) (dv_R_x : x ∉ R.fv) (dv_R_y : y ∉ R.fv) :
    Nominal.TEnvFresh [(nb072AlphaDummy001 A B R S_cls H, y), (nb072AlphaDummy000 A B R S_cls H, x)] R.fv
    source
    noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb072FocusedRefl0002 (x y : SemanticCore.Var) (A B R S_cls H : SemanticCore.Class) (dv_R_x : x ∉ R.fv) (dv_R_y : y ∉ R.fv) :
    Nominal.TReflOn [(nb072AlphaDummy001 A B R S_cls H, y), (nb072AlphaDummy000 A B R S_cls H, x)] R.fv

    Checked nominal proof certificate identified upstream as nb072_focused_refl_0002.

    Equations
    Instances For