Documentation

LeanPool.NFWeakPartition.NAR4H5C094M3Part002

NF weak partition development: NAR4H5C094M3Part002.

source
noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094SplitAlpha0000 (x y : SemanticCore.Var) (dv_x_y : x ≠ y) :
Nominal.TAlphaWff [(nb094AlphaDummy020, nb094AlphaDummy021 x y), (nb094AlphaDummy018, nb094AlphaDummy019 x y), (nb094AlphaDummy007, nb094AlphaDummy009 x y), (nb094AlphaDummy006, nb094AlphaDummy008 x y), (nb094AlphaDummy012, nb094AlphaDummy013 x y), (nb094AlphaDummy010, nb094AlphaDummy011 x y), (nb094AlphaDummy002, nb094AlphaDummy003 x y), (nb094AlphaDummy001, y), (nb094AlphaDummy000, x), (nb094AlphaDummy004, nb094AlphaDummy005 x y)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb094AlphaDummy020) (SemanticCore.Class.cab nb094AlphaDummy014 (Compiler.CompactSourceSyntax.synWrex nb094AlphaDummy015 (SemanticCore.Class.cv nb094AlphaDummy000) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb094AlphaDummy014) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb094AlphaDummy015)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb094AlphaDummy020) (SemanticCore.Class.cab nb094AlphaDummy014 (Compiler.CompactSourceSyntax.synWrex nb094AlphaDummy015 (SemanticCore.Class.cv nb094AlphaDummy000) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb094AlphaDummy014) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb094AlphaDummy015)))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb094AlphaDummy021 x y)) (SemanticCore.Class.cab (nb094AlphaDummy016 x y) (Compiler.CompactSourceSyntax.synWrex (nb094AlphaDummy017 x y) (SemanticCore.Class.cv x) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb094AlphaDummy016 x y)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb094AlphaDummy017 x y))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb094AlphaDummy021 x y)) (SemanticCore.Class.cab (nb094AlphaDummy016 x y) (Compiler.CompactSourceSyntax.synWrex (nb094AlphaDummy017 x y) (SemanticCore.Class.cv x) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb094AlphaDummy016 x y)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb094AlphaDummy017 x y))))))).neg)

Checked nominal proof certificate identified upstream as nb094_split_alpha_0000.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094SplitAlpha0001 (x y : SemanticCore.Var) :
    Nominal.TAlphaWff [(nb094AlphaDummy046, nb094AlphaDummy047 x y), (nb094AlphaDummy015, nb094AlphaDummy017 x y), (nb094AlphaDummy014, nb094AlphaDummy016 x y), (nb094AlphaDummy044, nb094AlphaDummy045 x y), (nb094AlphaDummy018, nb094AlphaDummy019 x y), (nb094AlphaDummy007, nb094AlphaDummy009 x y), (nb094AlphaDummy006, nb094AlphaDummy008 x y), (nb094AlphaDummy012, nb094AlphaDummy013 x y), (nb094AlphaDummy010, nb094AlphaDummy011 x y), (nb094AlphaDummy002, nb094AlphaDummy003 x y), (nb094AlphaDummy001, y), (nb094AlphaDummy000, x), (nb094AlphaDummy004, nb094AlphaDummy005 x y)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb094AlphaDummy046) (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb094AlphaDummy015)))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb094AlphaDummy046) (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb094AlphaDummy047 x y)) (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb094AlphaDummy017 x y))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb094AlphaDummy047 x y)) (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))).neg)

    Checked nominal proof certificate identified upstream as nb094_split_alpha_0001.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094SplitAlpha0002 (x y : SemanticCore.Var) (dv_x_y : x ≠ y) :
      Nominal.TAlphaWff [(nb094AlphaDummy012, nb094AlphaDummy013 x y), (nb094AlphaDummy010, nb094AlphaDummy011 x y), (nb094AlphaDummy002, nb094AlphaDummy003 x y), (nb094AlphaDummy001, y), (nb094AlphaDummy000, x), (nb094AlphaDummy004, nb094AlphaDummy005 x y)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb094AlphaDummy012) (SemanticCore.Class.cab nb094AlphaDummy006 (Compiler.CompactSourceSyntax.synWrex nb094AlphaDummy007 (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv nb094AlphaDummy000) (SemanticCore.Class.cv nb094AlphaDummy001)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb094AlphaDummy006) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb094AlphaDummy007)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb094AlphaDummy012) (SemanticCore.Class.cab nb094AlphaDummy006 (Compiler.CompactSourceSyntax.synWrex nb094AlphaDummy007 (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv nb094AlphaDummy000) (SemanticCore.Class.cv nb094AlphaDummy001)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb094AlphaDummy006) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb094AlphaDummy007)))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb094AlphaDummy013 x y)) (SemanticCore.Class.cab (nb094AlphaDummy008 x y) (Compiler.CompactSourceSyntax.synWrex (nb094AlphaDummy009 x y) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb094AlphaDummy008 x y)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb094AlphaDummy009 x y))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb094AlphaDummy013 x y)) (SemanticCore.Class.cab (nb094AlphaDummy008 x y) (Compiler.CompactSourceSyntax.synWrex (nb094AlphaDummy009 x y) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb094AlphaDummy008 x y)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb094AlphaDummy009 x y))))))).neg)

      Checked nominal proof certificate identified upstream as nb094_split_alpha_0002.

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