Documentation

LeanPool.NFWeakPartition.NAR5H088P001Part004

NF weak partition development: NAR5H088P001Part004.

source
noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb088SplitAlpha0000 (u : SemanticCore.Var) (A B C R : SemanticCore.Class) :
Nominal.TAlphaWff [(nb088AlphaDummy035 A B C R, nb088AlphaDummy036 u A B C R), (nb088AlphaDummy009 A B C R, nb088AlphaDummy010 u A B C R), (nb088AlphaDummy001 A B C R, nb088AlphaDummy002 u A B C R), (nb088AlphaDummy000 A B C R, u), (nb088AlphaDummy003 A B C R, nb088AlphaDummy004 u A B C R)] (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb088AlphaDummy035 A B C R)) (SemanticCore.Class.cab (nb088AlphaDummy005 A B C R) (Compiler.CompactSourceSyntax.synWrex (nb088AlphaDummy006 A B C R) (SemanticCore.Class.cv (nb088AlphaDummy001 A B C R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb088AlphaDummy005 A B C R)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb088AlphaDummy006 A B C R))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb088AlphaDummy036 u A B C R)) (SemanticCore.Class.cab (nb088AlphaDummy007 u A B C R) (Compiler.CompactSourceSyntax.synWrex (nb088AlphaDummy008 u A B C R) (SemanticCore.Class.cv (nb088AlphaDummy002 u A B C R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb088AlphaDummy007 u A B C R)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb088AlphaDummy008 u A B C R))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg

Checked nominal proof certificate identified upstream as nb088_split_alpha_0000.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb088SplitAlpha0001 (u : SemanticCore.Var) (A B C R : SemanticCore.Class) :
    Nominal.TAlphaWff [(nb088AlphaDummy035 A B C R, nb088AlphaDummy036 u A B C R), (nb088AlphaDummy009 A B C R, nb088AlphaDummy010 u A B C R), (nb088AlphaDummy001 A B C R, nb088AlphaDummy002 u A B C R), (nb088AlphaDummy000 A B C R, u), (nb088AlphaDummy003 A B C R, nb088AlphaDummy004 u A B C R)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb088AlphaDummy035 A B C R)) (SemanticCore.Class.cab (nb088AlphaDummy005 A B C R) (Compiler.CompactSourceSyntax.synWrex (nb088AlphaDummy006 A B C R) (SemanticCore.Class.cv (nb088AlphaDummy001 A B C R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb088AlphaDummy005 A B C R)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb088AlphaDummy006 A B C R))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb088AlphaDummy035 A B C R)) (SemanticCore.Class.cab (nb088AlphaDummy005 A B C R) (Compiler.CompactSourceSyntax.synWrex (nb088AlphaDummy006 A B C R) (SemanticCore.Class.cv (nb088AlphaDummy001 A B C R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb088AlphaDummy005 A B C R)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb088AlphaDummy006 A B C R))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb088AlphaDummy036 u A B C R)) (SemanticCore.Class.cab (nb088AlphaDummy007 u A B C R) (Compiler.CompactSourceSyntax.synWrex (nb088AlphaDummy008 u A B C R) (SemanticCore.Class.cv (nb088AlphaDummy002 u A B C R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb088AlphaDummy007 u A B C R)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb088AlphaDummy008 u A B C R))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb088AlphaDummy036 u A B C R)) (SemanticCore.Class.cab (nb088AlphaDummy007 u A B C R) (Compiler.CompactSourceSyntax.synWrex (nb088AlphaDummy008 u A B C R) (SemanticCore.Class.cv (nb088AlphaDummy002 u A B C R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb088AlphaDummy007 u A B C R)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb088AlphaDummy008 u A B C R))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg)

    Checked nominal proof certificate identified upstream as nb088_split_alpha_0001.

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