Documentation

LeanPool.NFWeakPartition.Certificates.NAR4C068C001Block006

Nominal proof certificates grouped in dependency order.

Certificates from NAR4C068C001Part021.

source
noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0023 (x y f : SemanticCore.Var) :
Nominal.TAlphaWff [(nb068AlphaDummy179, nb068AlphaDummy180 f), (nb068AlphaDummy175, nb068AlphaDummy177 f), (nb068AlphaDummy176, nb068AlphaDummy178 f), (nb068AlphaDummy201, nb068AlphaDummy202 f), (nb068AlphaDummy199, nb068AlphaDummy200 f), (nb068AlphaDummy168, nb068AlphaDummy170 f), (nb068AlphaDummy167, nb068AlphaDummy169 f), (nb068AlphaDummy197, nb068AlphaDummy198 f), (nb068AlphaDummy171, nb068AlphaDummy172 f), (nb068AlphaDummy126, nb068AlphaDummy128 f), (nb068AlphaDummy125, nb068AlphaDummy127 f), (nb068AlphaDummy129, nb068AlphaDummy130 f), (nb068AlphaDummy047, nb068AlphaDummy050 f), (nb068AlphaDummy046, nb068AlphaDummy049 f), (nb068AlphaDummy045, nb068AlphaDummy048 f), (nb068AlphaDummy051, nb068AlphaDummy052 f), (nb068AlphaDummy043, nb068AlphaDummy044 f), (nb068AlphaDummy041, nb068AlphaDummy042 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy179) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb068AlphaDummy175) Compiler.CompactSourceSyntax.synC1c)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy175) Compiler.CompactSourceSyntax.synCnnc)).neg.imp (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy179) (SemanticCore.Class.cv nb068AlphaDummy175)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy175) Compiler.CompactSourceSyntax.synCnnc).neg)) ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy180 f)) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb068AlphaDummy177 f)) Compiler.CompactSourceSyntax.synC1c)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy177 f)) Compiler.CompactSourceSyntax.synCnnc)).neg.imp (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy180 f)) (SemanticCore.Class.cv (nb068AlphaDummy177 f))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy177 f)) Compiler.CompactSourceSyntax.synCnnc).neg))

Checked nominal proof certificate identified upstream as nb068_split_alpha_0023.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0024 (x y f : SemanticCore.Var) :
    Nominal.TAlphaWff [(nb068AlphaDummy167, nb068AlphaDummy169 f), (nb068AlphaDummy197, nb068AlphaDummy198 f), (nb068AlphaDummy171, nb068AlphaDummy172 f), (nb068AlphaDummy126, nb068AlphaDummy128 f), (nb068AlphaDummy125, nb068AlphaDummy127 f), (nb068AlphaDummy129, nb068AlphaDummy130 f), (nb068AlphaDummy047, nb068AlphaDummy050 f), (nb068AlphaDummy046, nb068AlphaDummy049 f), (nb068AlphaDummy045, nb068AlphaDummy048 f), (nb068AlphaDummy051, nb068AlphaDummy052 f), (nb068AlphaDummy043, nb068AlphaDummy044 f), (nb068AlphaDummy041, nb068AlphaDummy042 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] (SemanticCore.Wff.all nb068AlphaDummy168 (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy168) (SemanticCore.Class.cv nb068AlphaDummy125)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy167) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy168)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))).neg).neg (SemanticCore.Wff.all (nb068AlphaDummy170 f) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy170 f)) (SemanticCore.Class.cv (nb068AlphaDummy127 f))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy169 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy170 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))).neg).neg

    Checked nominal proof certificate identified upstream as nb068_split_alpha_0024.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0025 (x y f : SemanticCore.Var) :
      Nominal.TAlphaWff [(nb068AlphaDummy126, nb068AlphaDummy128 f), (nb068AlphaDummy125, nb068AlphaDummy127 f), (nb068AlphaDummy129, nb068AlphaDummy130 f), (nb068AlphaDummy047, nb068AlphaDummy050 f), (nb068AlphaDummy046, nb068AlphaDummy049 f), (nb068AlphaDummy045, nb068AlphaDummy048 f), (nb068AlphaDummy051, nb068AlphaDummy052 f), (nb068AlphaDummy043, nb068AlphaDummy044 f), (nb068AlphaDummy041, nb068AlphaDummy042 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv nb068AlphaDummy126) (SemanticCore.Class.cv nb068AlphaDummy125)) (SemanticCore.Class.cv nb068AlphaDummy000)) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv (nb068AlphaDummy128 f)) (SemanticCore.Class.cv (nb068AlphaDummy127 f))) (SemanticCore.Class.cv f))

      Checked nominal proof certificate identified upstream as nb068_split_alpha_0025.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0026 (x y f : SemanticCore.Var) :
        Nominal.TAlphaWff [(nb068AlphaDummy125, nb068AlphaDummy127 f), (nb068AlphaDummy129, nb068AlphaDummy130 f), (nb068AlphaDummy047, nb068AlphaDummy050 f), (nb068AlphaDummy046, nb068AlphaDummy049 f), (nb068AlphaDummy045, nb068AlphaDummy048 f), (nb068AlphaDummy051, nb068AlphaDummy052 f), (nb068AlphaDummy043, nb068AlphaDummy044 f), (nb068AlphaDummy041, nb068AlphaDummy042 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] (SemanticCore.Wff.all nb068AlphaDummy126 (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy129) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv nb068AlphaDummy125) (SemanticCore.Class.cv nb068AlphaDummy126))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb068AlphaDummy126) (SemanticCore.Class.cv nb068AlphaDummy000) (SemanticCore.Class.cv nb068AlphaDummy125))).neg) (SemanticCore.Wff.all (nb068AlphaDummy128 f) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy130 f)) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv (nb068AlphaDummy127 f)) (SemanticCore.Class.cv (nb068AlphaDummy128 f)))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb068AlphaDummy128 f)) (SemanticCore.Class.cv f) (SemanticCore.Class.cv (nb068AlphaDummy127 f)))).neg)

        Checked nominal proof certificate identified upstream as nb068_split_alpha_0026.

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

          Certificates from NAR4C068C001Part022.

          source
          noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0027 (x y f : SemanticCore.Var) :
          Nominal.TAlphaWff [(nb068AlphaDummy219, nb068AlphaDummy222 f), (nb068AlphaDummy218, nb068AlphaDummy221 f), (nb068AlphaDummy217, nb068AlphaDummy220 f), (nb068AlphaDummy215, nb068AlphaDummy216 f), (nb068AlphaDummy211, nb068AlphaDummy213 f), (nb068AlphaDummy212, nb068AlphaDummy214 f), (nb068AlphaDummy204, nb068AlphaDummy206 f), (nb068AlphaDummy203, nb068AlphaDummy205 f), (nb068AlphaDummy209, nb068AlphaDummy210 f), (nb068AlphaDummy207, nb068AlphaDummy208 f), (nb068AlphaDummy047, nb068AlphaDummy050 f), (nb068AlphaDummy046, nb068AlphaDummy049 f), (nb068AlphaDummy045, nb068AlphaDummy048 f), (nb068AlphaDummy051, nb068AlphaDummy052 f), (nb068AlphaDummy043, nb068AlphaDummy044 f), (nb068AlphaDummy041, nb068AlphaDummy042 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb068AlphaDummy218) (SemanticCore.Class.cv nb068AlphaDummy219)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy217) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb068AlphaDummy218) (SemanticCore.Class.cv nb068AlphaDummy219))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb068AlphaDummy221 f)) (SemanticCore.Class.cv (nb068AlphaDummy222 f))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy220 f)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb068AlphaDummy221 f)) (SemanticCore.Class.cv (nb068AlphaDummy222 f)))).neg)

          Checked nominal proof certificate identified upstream as nb068_split_alpha_0027.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0028 (x y f : SemanticCore.Var) :
            Nominal.TAlphaWff [(nb068AlphaDummy211, nb068AlphaDummy213 f), (nb068AlphaDummy212, nb068AlphaDummy214 f), (nb068AlphaDummy204, nb068AlphaDummy206 f), (nb068AlphaDummy203, nb068AlphaDummy205 f), (nb068AlphaDummy209, nb068AlphaDummy210 f), (nb068AlphaDummy207, nb068AlphaDummy208 f), (nb068AlphaDummy047, nb068AlphaDummy050 f), (nb068AlphaDummy046, nb068AlphaDummy049 f), (nb068AlphaDummy045, nb068AlphaDummy048 f), (nb068AlphaDummy051, nb068AlphaDummy052 f), (nb068AlphaDummy043, nb068AlphaDummy044 f), (nb068AlphaDummy041, nb068AlphaDummy042 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy211) (SemanticCore.Class.cv nb068AlphaDummy204)).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy212) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy211) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb068AlphaDummy211) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv nb068AlphaDummy211))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy213 f)) (SemanticCore.Class.cv (nb068AlphaDummy206 f))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy214 f)) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy213 f)) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb068AlphaDummy213 f)) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv (nb068AlphaDummy213 f)))).neg)

            Checked nominal proof certificate identified upstream as nb068_split_alpha_0028.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0029 (x y f : SemanticCore.Var) :
              Nominal.TAlphaWff [(nb068AlphaDummy219, nb068AlphaDummy222 f), (nb068AlphaDummy218, nb068AlphaDummy221 f), (nb068AlphaDummy217, nb068AlphaDummy220 f), (nb068AlphaDummy215, nb068AlphaDummy216 f), (nb068AlphaDummy211, nb068AlphaDummy213 f), (nb068AlphaDummy212, nb068AlphaDummy214 f), (nb068AlphaDummy237, nb068AlphaDummy238 f), (nb068AlphaDummy235, nb068AlphaDummy236 f), (nb068AlphaDummy204, nb068AlphaDummy206 f), (nb068AlphaDummy203, nb068AlphaDummy205 f), (nb068AlphaDummy233, nb068AlphaDummy234 f), (nb068AlphaDummy207, nb068AlphaDummy208 f), (nb068AlphaDummy047, nb068AlphaDummy050 f), (nb068AlphaDummy046, nb068AlphaDummy049 f), (nb068AlphaDummy045, nb068AlphaDummy048 f), (nb068AlphaDummy051, nb068AlphaDummy052 f), (nb068AlphaDummy043, nb068AlphaDummy044 f), (nb068AlphaDummy041, nb068AlphaDummy042 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb068AlphaDummy218) (SemanticCore.Class.cv nb068AlphaDummy219)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy217) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb068AlphaDummy218) (SemanticCore.Class.cv nb068AlphaDummy219))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb068AlphaDummy221 f)) (SemanticCore.Class.cv (nb068AlphaDummy222 f))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy220 f)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb068AlphaDummy221 f)) (SemanticCore.Class.cv (nb068AlphaDummy222 f)))).neg)

              Checked nominal proof certificate identified upstream as nb068_split_alpha_0029.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0030 (x y f : SemanticCore.Var) :
                Nominal.TAlphaWff [(nb068AlphaDummy211, nb068AlphaDummy213 f), (nb068AlphaDummy212, nb068AlphaDummy214 f), (nb068AlphaDummy237, nb068AlphaDummy238 f), (nb068AlphaDummy235, nb068AlphaDummy236 f), (nb068AlphaDummy204, nb068AlphaDummy206 f), (nb068AlphaDummy203, nb068AlphaDummy205 f), (nb068AlphaDummy233, nb068AlphaDummy234 f), (nb068AlphaDummy207, nb068AlphaDummy208 f), (nb068AlphaDummy047, nb068AlphaDummy050 f), (nb068AlphaDummy046, nb068AlphaDummy049 f), (nb068AlphaDummy045, nb068AlphaDummy048 f), (nb068AlphaDummy051, nb068AlphaDummy052 f), (nb068AlphaDummy043, nb068AlphaDummy044 f), (nb068AlphaDummy041, nb068AlphaDummy042 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy211) (SemanticCore.Class.cv nb068AlphaDummy204)).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy212) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy211) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb068AlphaDummy211) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv nb068AlphaDummy211))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy213 f)) (SemanticCore.Class.cv (nb068AlphaDummy206 f))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy214 f)) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy213 f)) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb068AlphaDummy213 f)) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv (nb068AlphaDummy213 f)))).neg)

                Checked nominal proof certificate identified upstream as nb068_split_alpha_0030.

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