Documentation

LeanPool.NFWeakPartition.NAR4C074C001Part012

NF weak partition development: NAR4C074C001Part012.

source
noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb074SplitAlpha0008 (x : SemanticCore.Var) :
Nominal.TAlphaWff [(nb074AlphaDummy155, nb074AlphaDummy156 x), (nb074AlphaDummy124, nb074AlphaDummy126 x), (nb074AlphaDummy123, nb074AlphaDummy125 x), (nb074AlphaDummy153, nb074AlphaDummy154 x), (nb074AlphaDummy127, nb074AlphaDummy128 x), (nb074AlphaDummy082, nb074AlphaDummy084 x), (nb074AlphaDummy081, nb074AlphaDummy083 x), (nb074AlphaDummy085, nb074AlphaDummy086 x), (nb074AlphaDummy042, nb074AlphaDummy044 x), (nb074AlphaDummy041, nb074AlphaDummy043 x), (nb074AlphaDummy001, nb074AlphaDummy002 x), (nb074AlphaDummy000, x), (nb074AlphaDummy003, nb074AlphaDummy004 x)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb074AlphaDummy155) (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb074AlphaDummy124)))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb074AlphaDummy155) (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb074AlphaDummy156 x)) (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb074AlphaDummy126 x))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb074AlphaDummy156 x)) (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))).neg)

Checked nominal proof certificate identified upstream as nb074_split_alpha_0008.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nominalDfDomfn (x : SemanticCore.Var) :
    Nominal.NPrf (SemanticCore.Wff.classEq Compiler.CompactSourceSyntax.synCdomfn (Compiler.CompactSourceSyntax.synCmpt x Compiler.CompactSourceSyntax.synCvv (Compiler.CompactSourceSyntax.synCdm (SemanticCore.Class.cv x))))

    Checked nominal proof certificate identified upstream as nominal_df_domfn.

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