Documentation

LeanPool.NFWeakPartition.Certificates.NAR4C077C001Block015

Nominal proof certificates grouped in dependency order.

Certificates from NAR4C077C001Part042.

source
noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077SplitAlpha0028 (x : SemanticCore.Var) (F I : SemanticCore.Class) :
Nominal.TAlphaWff [(nb077AlphaDummy225 F I, nb077AlphaDummy226 x), (nb077AlphaDummy223 F I, nb077AlphaDummy224 x), (nb077AlphaDummy141 F I, nb077AlphaDummy144 x), (nb077AlphaDummy140 F I, nb077AlphaDummy143 x), (nb077AlphaDummy139 F I, nb077AlphaDummy142 x), (nb077AlphaDummy145 F I, nb077AlphaDummy146 x), (nb077AlphaDummy061 F I, nb077AlphaDummy064 x), (nb077AlphaDummy060 F I, nb077AlphaDummy063 x), (nb077AlphaDummy059 F I, nb077AlphaDummy062 x), (nb077AlphaDummy065 F I, nb077AlphaDummy066 x), (nb077AlphaDummy057 F I, nb077AlphaDummy058 x F), (nb077AlphaDummy055 F I, nb077AlphaDummy056 x F), (nb077AlphaDummy016 F I, nb077AlphaDummy018 x F I), (nb077AlphaDummy015 F I, nb077AlphaDummy017 x F I), (nb077AlphaDummy001 F I, nb077AlphaDummy002 x F I), (nb077AlphaDummy004 F I, nb077AlphaDummy006 x F I), (nb077AlphaDummy003 F I, nb077AlphaDummy005 x F I)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb077AlphaDummy225 F I)) (SemanticCore.Class.cab (nb077AlphaDummy219 F I) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy220 F I) (SemanticCore.Class.cv (nb077AlphaDummy141 F I)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy219 F I)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy220 F I))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb077AlphaDummy225 F I)) (SemanticCore.Class.cab (nb077AlphaDummy219 F I) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy220 F I) (SemanticCore.Class.cv (nb077AlphaDummy141 F I)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy219 F I)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy220 F I))))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb077AlphaDummy226 x)) (SemanticCore.Class.cab (nb077AlphaDummy221 x) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy222 x) (SemanticCore.Class.cv (nb077AlphaDummy144 x)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy221 x)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy222 x))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb077AlphaDummy226 x)) (SemanticCore.Class.cab (nb077AlphaDummy221 x) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy222 x) (SemanticCore.Class.cv (nb077AlphaDummy144 x)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy221 x)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy222 x))))))).neg)

Checked nominal proof certificate identified upstream as nb077_split_alpha_0028.

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

    Certificates from NAR4C077C001Part043.

    source
    noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077SplitAlpha0029 (x : SemanticCore.Var) (F I : SemanticCore.Class) :
    Nominal.TAlphaWff [(nb077AlphaDummy253 F I, nb077AlphaDummy254 x), (nb077AlphaDummy251 F I, nb077AlphaDummy252 x), (nb077AlphaDummy220 F I, nb077AlphaDummy222 x), (nb077AlphaDummy219 F I, nb077AlphaDummy221 x), (nb077AlphaDummy249 F I, nb077AlphaDummy250 x), (nb077AlphaDummy223 F I, nb077AlphaDummy224 x), (nb077AlphaDummy141 F I, nb077AlphaDummy144 x), (nb077AlphaDummy140 F I, nb077AlphaDummy143 x), (nb077AlphaDummy139 F I, nb077AlphaDummy142 x), (nb077AlphaDummy145 F I, nb077AlphaDummy146 x), (nb077AlphaDummy061 F I, nb077AlphaDummy064 x), (nb077AlphaDummy060 F I, nb077AlphaDummy063 x), (nb077AlphaDummy059 F I, nb077AlphaDummy062 x), (nb077AlphaDummy065 F I, nb077AlphaDummy066 x), (nb077AlphaDummy057 F I, nb077AlphaDummy058 x F), (nb077AlphaDummy055 F I, nb077AlphaDummy056 x F), (nb077AlphaDummy016 F I, nb077AlphaDummy018 x F I), (nb077AlphaDummy015 F I, nb077AlphaDummy017 x F I), (nb077AlphaDummy001 F I, nb077AlphaDummy002 x F I), (nb077AlphaDummy004 F I, nb077AlphaDummy006 x F I), (nb077AlphaDummy003 F I, nb077AlphaDummy005 x F I)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb077AlphaDummy253 F I)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy220 F I)))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb077AlphaDummy253 F I)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy220 F I)))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb077AlphaDummy254 x)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy222 x)))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb077AlphaDummy254 x)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy222 x)))).neg)

    Checked nominal proof certificate identified upstream as nb077_split_alpha_0029.

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

      Certificates from NAR4C077C001Part044.

      source
      noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077SplitAlpha0030 (x : SemanticCore.Var) (F I : SemanticCore.Class) :
      Nominal.TAlphaWff [(nb077AlphaDummy265 F I, nb077AlphaDummy266 x), (nb077AlphaDummy263 F I, nb077AlphaDummy264 x), (nb077AlphaDummy255 F I, nb077AlphaDummy256 x), (nb077AlphaDummy000 F I, x), (nb077AlphaDummy257 F I, nb077AlphaDummy258 x), (nb077AlphaDummy141 F I, nb077AlphaDummy144 x), (nb077AlphaDummy140 F I, nb077AlphaDummy143 x), (nb077AlphaDummy139 F I, nb077AlphaDummy142 x), (nb077AlphaDummy145 F I, nb077AlphaDummy146 x), (nb077AlphaDummy061 F I, nb077AlphaDummy064 x), (nb077AlphaDummy060 F I, nb077AlphaDummy063 x), (nb077AlphaDummy059 F I, nb077AlphaDummy062 x), (nb077AlphaDummy065 F I, nb077AlphaDummy066 x), (nb077AlphaDummy057 F I, nb077AlphaDummy058 x F), (nb077AlphaDummy055 F I, nb077AlphaDummy056 x F), (nb077AlphaDummy016 F I, nb077AlphaDummy018 x F I), (nb077AlphaDummy015 F I, nb077AlphaDummy017 x F I), (nb077AlphaDummy001 F I, nb077AlphaDummy002 x F I), (nb077AlphaDummy004 F I, nb077AlphaDummy006 x F I), (nb077AlphaDummy003 F I, nb077AlphaDummy005 x F I)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb077AlphaDummy265 F I)) (SemanticCore.Class.cab (nb077AlphaDummy259 F I) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy260 F I) (SemanticCore.Class.cv (nb077AlphaDummy000 F I)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy259 F I)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy260 F I))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb077AlphaDummy265 F I)) (SemanticCore.Class.cab (nb077AlphaDummy259 F I) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy260 F I) (SemanticCore.Class.cv (nb077AlphaDummy000 F I)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy259 F I)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy260 F I))))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb077AlphaDummy266 x)) (SemanticCore.Class.cab (nb077AlphaDummy261 x) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy262 x) (SemanticCore.Class.cv x) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy261 x)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy262 x))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb077AlphaDummy266 x)) (SemanticCore.Class.cab (nb077AlphaDummy261 x) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy262 x) (SemanticCore.Class.cv x) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy261 x)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy262 x))))))).neg)

      Checked nominal proof certificate identified upstream as nb077_split_alpha_0030.

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