Documentation

LeanPool.NFWeakPartition.NAR4C075C001Part004

NF weak partition development: NAR4C075C001Part004.

source
noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb075SplitAlpha0000 (x : SemanticCore.Var) :
Nominal.TAlphaWff [(nb075AlphaDummy035, nb075AlphaDummy036 x), (nb075AlphaDummy009, nb075AlphaDummy010 x), (nb075AlphaDummy001, nb075AlphaDummy002 x), (nb075AlphaDummy000, x), (nb075AlphaDummy003, nb075AlphaDummy004 x)] (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb075AlphaDummy035) (SemanticCore.Class.cab nb075AlphaDummy005 (Compiler.CompactSourceSyntax.synWrex nb075AlphaDummy006 (SemanticCore.Class.cv nb075AlphaDummy001) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb075AlphaDummy005) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb075AlphaDummy006)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb075AlphaDummy036 x)) (SemanticCore.Class.cab (nb075AlphaDummy007 x) (Compiler.CompactSourceSyntax.synWrex (nb075AlphaDummy008 x) (SemanticCore.Class.cv (nb075AlphaDummy002 x)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb075AlphaDummy007 x)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb075AlphaDummy008 x))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg

Checked nominal proof certificate identified upstream as nb075_split_alpha_0000.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb075SplitAlpha0001 (x : SemanticCore.Var) :
    Nominal.TAlphaWff [(nb075AlphaDummy035, nb075AlphaDummy036 x), (nb075AlphaDummy009, nb075AlphaDummy010 x), (nb075AlphaDummy001, nb075AlphaDummy002 x), (nb075AlphaDummy000, x), (nb075AlphaDummy003, nb075AlphaDummy004 x)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb075AlphaDummy035) (SemanticCore.Class.cab nb075AlphaDummy005 (Compiler.CompactSourceSyntax.synWrex nb075AlphaDummy006 (SemanticCore.Class.cv nb075AlphaDummy001) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb075AlphaDummy005) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb075AlphaDummy006)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb075AlphaDummy035) (SemanticCore.Class.cab nb075AlphaDummy005 (Compiler.CompactSourceSyntax.synWrex nb075AlphaDummy006 (SemanticCore.Class.cv nb075AlphaDummy001) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb075AlphaDummy005) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb075AlphaDummy006)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb075AlphaDummy036 x)) (SemanticCore.Class.cab (nb075AlphaDummy007 x) (Compiler.CompactSourceSyntax.synWrex (nb075AlphaDummy008 x) (SemanticCore.Class.cv (nb075AlphaDummy002 x)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb075AlphaDummy007 x)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb075AlphaDummy008 x))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb075AlphaDummy036 x)) (SemanticCore.Class.cab (nb075AlphaDummy007 x) (Compiler.CompactSourceSyntax.synWrex (nb075AlphaDummy008 x) (SemanticCore.Class.cv (nb075AlphaDummy002 x)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb075AlphaDummy007 x)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb075AlphaDummy008 x))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg)

    Checked nominal proof certificate identified upstream as nb075_split_alpha_0001.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For