Documentation

LeanPool.NFWeakPartition.Certificates.NAR4C078C001Block028

Nominal proof certificates grouped in dependency order.

Certificates from NAR4C078C001Part089.

source
noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078SplitAlpha0062 (x y g : SemanticCore.Var) :
Nominal.TAlphaWff [(nb078AlphaDummy583, nb078AlphaDummy584 g), (nb078AlphaDummy581, nb078AlphaDummy582 g), (nb078AlphaDummy570, nb078AlphaDummy573 g), (nb078AlphaDummy569, nb078AlphaDummy572 g), (nb078AlphaDummy575, nb078AlphaDummy576 g), (nb078AlphaDummy567, nb078AlphaDummy568 g), (nb078AlphaDummy565, nb078AlphaDummy566 g), (nb078AlphaDummy001, g), (nb078AlphaDummy004, y), (nb078AlphaDummy003, x)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb078AlphaDummy583) (SemanticCore.Class.cab nb078AlphaDummy577 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy578 (SemanticCore.Class.cv nb078AlphaDummy569) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy577) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy578)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb078AlphaDummy583) (SemanticCore.Class.cab nb078AlphaDummy577 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy578 (SemanticCore.Class.cv nb078AlphaDummy569) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy577) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy578)))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb078AlphaDummy584 g)) (SemanticCore.Class.cab (nb078AlphaDummy579 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy580 g) (SemanticCore.Class.cv (nb078AlphaDummy572 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy579 g)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy580 g))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb078AlphaDummy584 g)) (SemanticCore.Class.cab (nb078AlphaDummy579 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy580 g) (SemanticCore.Class.cv (nb078AlphaDummy572 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy579 g)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy580 g))))))).neg)

Checked nominal proof certificate identified upstream as nb078_split_alpha_0062.

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

    Certificates from NAR4C078C001Part090.

    source
    noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078SplitAlpha0063 (x y g : SemanticCore.Var) :
    Nominal.TAlphaWff [(nb078AlphaDummy609, nb078AlphaDummy610 g), (nb078AlphaDummy578, nb078AlphaDummy580 g), (nb078AlphaDummy577, nb078AlphaDummy579 g), (nb078AlphaDummy607, nb078AlphaDummy608 g), (nb078AlphaDummy581, nb078AlphaDummy582 g), (nb078AlphaDummy570, nb078AlphaDummy573 g), (nb078AlphaDummy569, nb078AlphaDummy572 g), (nb078AlphaDummy575, nb078AlphaDummy576 g), (nb078AlphaDummy567, nb078AlphaDummy568 g), (nb078AlphaDummy565, nb078AlphaDummy566 g), (nb078AlphaDummy001, g), (nb078AlphaDummy004, y), (nb078AlphaDummy003, x)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb078AlphaDummy609) (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy578)))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb078AlphaDummy609) (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb078AlphaDummy610 g)) (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy580 g))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb078AlphaDummy610 g)) (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))).neg)

    Checked nominal proof certificate identified upstream as nb078_split_alpha_0063.

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

      Certificates from NAR4C078C001Part091.

      source
      noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078SplitAlpha0064 (x y g : SemanticCore.Var) :
      Nominal.TAlphaWff [(nb078AlphaDummy619, nb078AlphaDummy620 g), (nb078AlphaDummy617, nb078AlphaDummy618 g), (nb078AlphaDummy571, nb078AlphaDummy574 g), (nb078AlphaDummy570, nb078AlphaDummy573 g), (nb078AlphaDummy569, nb078AlphaDummy572 g), (nb078AlphaDummy575, nb078AlphaDummy576 g), (nb078AlphaDummy567, nb078AlphaDummy568 g), (nb078AlphaDummy565, nb078AlphaDummy566 g), (nb078AlphaDummy001, g), (nb078AlphaDummy004, y), (nb078AlphaDummy003, x)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb078AlphaDummy619) (SemanticCore.Class.cab nb078AlphaDummy613 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy614 (SemanticCore.Class.cv nb078AlphaDummy569) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy613) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy614)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb078AlphaDummy619) (SemanticCore.Class.cab nb078AlphaDummy613 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy614 (SemanticCore.Class.cv nb078AlphaDummy569) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy613) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy614)))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb078AlphaDummy620 g)) (SemanticCore.Class.cab (nb078AlphaDummy615 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy616 g) (SemanticCore.Class.cv (nb078AlphaDummy572 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy615 g)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy616 g))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb078AlphaDummy620 g)) (SemanticCore.Class.cab (nb078AlphaDummy615 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy616 g) (SemanticCore.Class.cv (nb078AlphaDummy572 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy615 g)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy616 g))))))).neg)

      Checked nominal proof certificate identified upstream as nb078_split_alpha_0064.

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