Documentation

LeanPool.NFWeakPartition.NAR4C082C001Part004

NF weak partition development: NAR4C082C001Part004.

source
noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb082SplitAlpha0000 (A B R : SemanticCore.Class) (p : SemanticCore.Var) :
Nominal.TAlphaWff [(nb082AlphaDummy035 A B R, nb082AlphaDummy036 A B R p), (nb082AlphaDummy009 A B R, nb082AlphaDummy010 A B R p), (nb082AlphaDummy001 A B R, nb082AlphaDummy002 A B R p), (nb082AlphaDummy000 A B R, p), (nb082AlphaDummy003 A B R, nb082AlphaDummy004 A B R p)] (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb082AlphaDummy035 A B R)) (SemanticCore.Class.cab (nb082AlphaDummy005 A B R) (Compiler.CompactSourceSyntax.synWrex (nb082AlphaDummy006 A B R) (SemanticCore.Class.cv (nb082AlphaDummy001 A B R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb082AlphaDummy005 A B R)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb082AlphaDummy006 A B R))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb082AlphaDummy036 A B R p)) (SemanticCore.Class.cab (nb082AlphaDummy007 A B R p) (Compiler.CompactSourceSyntax.synWrex (nb082AlphaDummy008 A B R p) (SemanticCore.Class.cv (nb082AlphaDummy002 A B R p)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb082AlphaDummy007 A B R p)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb082AlphaDummy008 A B R p))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg

Checked nominal proof certificate identified upstream as nb082_split_alpha_0000.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb082SplitAlpha0001 (A B R : SemanticCore.Class) (p : SemanticCore.Var) :
    Nominal.TAlphaWff [(nb082AlphaDummy035 A B R, nb082AlphaDummy036 A B R p), (nb082AlphaDummy009 A B R, nb082AlphaDummy010 A B R p), (nb082AlphaDummy001 A B R, nb082AlphaDummy002 A B R p), (nb082AlphaDummy000 A B R, p), (nb082AlphaDummy003 A B R, nb082AlphaDummy004 A B R p)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb082AlphaDummy035 A B R)) (SemanticCore.Class.cab (nb082AlphaDummy005 A B R) (Compiler.CompactSourceSyntax.synWrex (nb082AlphaDummy006 A B R) (SemanticCore.Class.cv (nb082AlphaDummy001 A B R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb082AlphaDummy005 A B R)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb082AlphaDummy006 A B R))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb082AlphaDummy035 A B R)) (SemanticCore.Class.cab (nb082AlphaDummy005 A B R) (Compiler.CompactSourceSyntax.synWrex (nb082AlphaDummy006 A B R) (SemanticCore.Class.cv (nb082AlphaDummy001 A B R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb082AlphaDummy005 A B R)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb082AlphaDummy006 A B R))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb082AlphaDummy036 A B R p)) (SemanticCore.Class.cab (nb082AlphaDummy007 A B R p) (Compiler.CompactSourceSyntax.synWrex (nb082AlphaDummy008 A B R p) (SemanticCore.Class.cv (nb082AlphaDummy002 A B R p)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb082AlphaDummy007 A B R p)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb082AlphaDummy008 A B R p))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb082AlphaDummy036 A B R p)) (SemanticCore.Class.cab (nb082AlphaDummy007 A B R p) (Compiler.CompactSourceSyntax.synWrex (nb082AlphaDummy008 A B R p) (SemanticCore.Class.cv (nb082AlphaDummy002 A B R p)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb082AlphaDummy007 A B R p)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb082AlphaDummy008 A B R p))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg)

    Checked nominal proof certificate identified upstream as nb082_split_alpha_0001.

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