Documentation

LeanPool.NFWeakPartition.Certificates.NAR4C078C001Block035

Nominal proof certificates grouped in dependency order.

Certificates from NAR4C078C001Part107.

source
noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078SplitAlpha0082 (x y g : SemanticCore.Var) :
Nominal.TAlphaWff [(nb078AlphaDummy583, nb078AlphaDummy584 g), (nb078AlphaDummy581, nb078AlphaDummy582 g), (nb078AlphaDummy570, nb078AlphaDummy573 g), (nb078AlphaDummy569, nb078AlphaDummy572 g), (nb078AlphaDummy575, nb078AlphaDummy576 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_0082.

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

    Certificates from NAR4C078C001Part108.

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

    Checked nominal proof certificate identified upstream as nb078_split_alpha_0083.

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

      Certificates from NAR4C078C001Part109.

      source
      noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078SplitAlpha0084 (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), (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_0084.

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