Documentation

LeanPool.NFWeakPartition.Certificates.NAR4C053C001Block001

Nominal proof certificates grouped in dependency order.

Certificates from NAR4C053C001Part002.

source
noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb053SplitAlpha0000 (x y : SemanticCore.Var) :
Nominal.TAlphaWff [(nb053AlphaDummy020, nb053AlphaDummy023 x y), (nb053AlphaDummy019, nb053AlphaDummy022 x y), (nb053AlphaDummy018, nb053AlphaDummy021 x y), (nb053AlphaDummy016, nb053AlphaDummy017 x y), (nb053AlphaDummy012, nb053AlphaDummy014 x y), (nb053AlphaDummy013, nb053AlphaDummy015 x y), (nb053AlphaDummy005, nb053AlphaDummy007 x y), (nb053AlphaDummy004, nb053AlphaDummy006 x y), (nb053AlphaDummy010, nb053AlphaDummy011 x y), (nb053AlphaDummy008, nb053AlphaDummy009 x y), (nb053AlphaDummy001, y), (nb053AlphaDummy000, x), (nb053AlphaDummy002, nb053AlphaDummy003 x y)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb053AlphaDummy019) (SemanticCore.Class.cv nb053AlphaDummy020)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb053AlphaDummy018) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb053AlphaDummy019) (SemanticCore.Class.cv nb053AlphaDummy020))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb053AlphaDummy022 x y)) (SemanticCore.Class.cv (nb053AlphaDummy023 x y))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb053AlphaDummy021 x y)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb053AlphaDummy022 x y)) (SemanticCore.Class.cv (nb053AlphaDummy023 x y)))).neg)

Checked nominal proof certificate identified upstream as nb053_split_alpha_0000.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb053SplitAlpha0001 (x y : SemanticCore.Var) (dv_x_y : x ≠ y) :
    Nominal.TAlphaWff [(nb053AlphaDummy005, nb053AlphaDummy007 x y), (nb053AlphaDummy004, nb053AlphaDummy006 x y), (nb053AlphaDummy010, nb053AlphaDummy011 x y), (nb053AlphaDummy008, nb053AlphaDummy009 x y), (nb053AlphaDummy001, y), (nb053AlphaDummy000, x), (nb053AlphaDummy002, nb053AlphaDummy003 x y)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb053AlphaDummy005) (SemanticCore.Class.cv nb053AlphaDummy000)).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb053AlphaDummy004) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb053AlphaDummy005))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb053AlphaDummy007 x y)) (SemanticCore.Class.cv x)).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb053AlphaDummy006 x y)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb053AlphaDummy007 x y)))).neg)

    Checked nominal proof certificate identified upstream as nb053_split_alpha_0001.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb053SplitAlpha0002 (x y : SemanticCore.Var) :
      Nominal.TAlphaWff [(nb053AlphaDummy020, nb053AlphaDummy023 x y), (nb053AlphaDummy019, nb053AlphaDummy022 x y), (nb053AlphaDummy018, nb053AlphaDummy021 x y), (nb053AlphaDummy016, nb053AlphaDummy017 x y), (nb053AlphaDummy012, nb053AlphaDummy014 x y), (nb053AlphaDummy013, nb053AlphaDummy015 x y), (nb053AlphaDummy038, nb053AlphaDummy039 x y), (nb053AlphaDummy036, nb053AlphaDummy037 x y), (nb053AlphaDummy005, nb053AlphaDummy007 x y), (nb053AlphaDummy004, nb053AlphaDummy006 x y), (nb053AlphaDummy034, nb053AlphaDummy035 x y), (nb053AlphaDummy008, nb053AlphaDummy009 x y), (nb053AlphaDummy001, y), (nb053AlphaDummy000, x), (nb053AlphaDummy002, nb053AlphaDummy003 x y)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb053AlphaDummy019) (SemanticCore.Class.cv nb053AlphaDummy020)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb053AlphaDummy018) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb053AlphaDummy019) (SemanticCore.Class.cv nb053AlphaDummy020))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb053AlphaDummy022 x y)) (SemanticCore.Class.cv (nb053AlphaDummy023 x y))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb053AlphaDummy021 x y)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb053AlphaDummy022 x y)) (SemanticCore.Class.cv (nb053AlphaDummy023 x y)))).neg)

      Checked nominal proof certificate identified upstream as nb053_split_alpha_0002.

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

        Certificates from NAR4C053C001Part003.

        source
        noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb053SplitAlpha0003 (x y : SemanticCore.Var) :
        Nominal.TAlphaWff [(nb053AlphaDummy038, nb053AlphaDummy039 x y), (nb053AlphaDummy036, nb053AlphaDummy037 x y), (nb053AlphaDummy005, nb053AlphaDummy007 x y), (nb053AlphaDummy004, nb053AlphaDummy006 x y), (nb053AlphaDummy034, nb053AlphaDummy035 x y), (nb053AlphaDummy008, nb053AlphaDummy009 x y), (nb053AlphaDummy001, y), (nb053AlphaDummy000, x), (nb053AlphaDummy002, nb053AlphaDummy003 x y)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb053AlphaDummy038) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb053AlphaDummy005))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb053AlphaDummy038) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb053AlphaDummy005))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb053AlphaDummy039 x y)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb053AlphaDummy007 x y)))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb053AlphaDummy039 x y)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb053AlphaDummy007 x y)))).neg)

        Checked nominal proof certificate identified upstream as nb053_split_alpha_0003.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb053SplitAlpha0004 (x y : SemanticCore.Var) (dv_x_y : x ≠ y) :
          Nominal.TAlphaWff [(nb053AlphaDummy001, y), (nb053AlphaDummy000, x), (nb053AlphaDummy002, nb053AlphaDummy003 x y)] (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb053AlphaDummy002) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv nb053AlphaDummy000) (SemanticCore.Class.cv nb053AlphaDummy001))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb053AlphaDummy003 x y)) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)))

          Checked nominal proof certificate identified upstream as nb053_split_alpha_0004.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nominalDfDisj (x y : SemanticCore.Var) (dv_x_y : x ≠ y) :
            Nominal.NPrf (SemanticCore.Wff.classEq Compiler.CompactSourceSyntax.synCdisj (Compiler.CompactSourceSyntax.synCopab x y (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) Compiler.CompactSourceSyntax.synC0)))

            Checked nominal proof certificate identified upstream as nominal_df_disj.

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