Documentation

LeanPool.NFWeakPartition.Certificates.NAR4C068C001Block008

Nominal proof certificates grouped in dependency order.

Certificates from NAR4C068C001Part028.

source
noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0052 (x y f : SemanticCore.Var) :
Nominal.TAlphaWff [(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), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy176) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy175) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb068AlphaDummy175) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv nb068AlphaDummy175))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy178 f)) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy177 f)) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb068AlphaDummy177 f)) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv (nb068AlphaDummy177 f))))

Checked nominal proof certificate identified upstream as nb068_split_alpha_0052.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0053 (x y f : SemanticCore.Var) :
    Nominal.TAlphaWff [(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), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy197) (SemanticCore.Class.cab nb068AlphaDummy167 (Compiler.CompactSourceSyntax.synWrex 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)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy197) (SemanticCore.Class.cab nb068AlphaDummy167 (Compiler.CompactSourceSyntax.synWrex 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) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy198 f)) (SemanticCore.Class.cab (nb068AlphaDummy169 f) (Compiler.CompactSourceSyntax.synWrex (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)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy198 f)) (SemanticCore.Class.cab (nb068AlphaDummy169 f) (Compiler.CompactSourceSyntax.synWrex (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)

    Checked nominal proof certificate identified upstream as nb068_split_alpha_0053.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0054 (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), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] ((SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy129) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv nb068AlphaDummy125) (SemanticCore.Class.cv nb068AlphaDummy126))).imp (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb068AlphaDummy126) (SemanticCore.Class.cv nb068AlphaDummy000) (SemanticCore.Class.cv nb068AlphaDummy125)).neg) ((SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy130 f)) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv (nb068AlphaDummy127 f)) (SemanticCore.Class.cv (nb068AlphaDummy128 f)))).imp (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_0054.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0055 (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), (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_0055.

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

          Certificates from NAR4C068C001Part029.

          source
          noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0056 (x y f : SemanticCore.Var) :
          Nominal.TAlphaWff [(nb068AlphaDummy204, nb068AlphaDummy206 f), (nb068AlphaDummy203, nb068AlphaDummy205 f), (nb068AlphaDummy209, nb068AlphaDummy210 f), (nb068AlphaDummy207, nb068AlphaDummy208 f), (nb068AlphaDummy047, nb068AlphaDummy050 f), (nb068AlphaDummy046, nb068AlphaDummy049 f), (nb068AlphaDummy045, nb068AlphaDummy048 f), (nb068AlphaDummy051, nb068AlphaDummy052 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy203) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy204))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy205 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy206 f))))

          Checked nominal proof certificate identified upstream as nb068_split_alpha_0056.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0057 (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), (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_0057.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0058 (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), (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_0058.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0059 (x y f : SemanticCore.Var) :
                Nominal.TAlphaWff [(nb068AlphaDummy233, nb068AlphaDummy234 f), (nb068AlphaDummy207, nb068AlphaDummy208 f), (nb068AlphaDummy047, nb068AlphaDummy050 f), (nb068AlphaDummy046, nb068AlphaDummy049 f), (nb068AlphaDummy045, nb068AlphaDummy048 f), (nb068AlphaDummy051, nb068AlphaDummy052 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy233) (SemanticCore.Class.cab nb068AlphaDummy203 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy204 (SemanticCore.Class.cv nb068AlphaDummy046) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy203) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy204)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy233) (SemanticCore.Class.cab nb068AlphaDummy203 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy204 (SemanticCore.Class.cv nb068AlphaDummy046) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy203) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy204)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy234 f)) (SemanticCore.Class.cab (nb068AlphaDummy205 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy206 f) (SemanticCore.Class.cv (nb068AlphaDummy049 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy205 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy206 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy234 f)) (SemanticCore.Class.cab (nb068AlphaDummy205 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy206 f) (SemanticCore.Class.cv (nb068AlphaDummy049 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy205 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy206 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg)

                Checked nominal proof certificate identified upstream as nb068_split_alpha_0059.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0060 (x y f : SemanticCore.Var) :
                  Nominal.TAlphaWff [(nb068AlphaDummy047, nb068AlphaDummy050 f), (nb068AlphaDummy046, nb068AlphaDummy049 f), (nb068AlphaDummy045, nb068AlphaDummy048 f), (nb068AlphaDummy051, nb068AlphaDummy052 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] ((Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb068AlphaDummy045) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb068AlphaDummy000)) (SemanticCore.Class.cv nb068AlphaDummy047)).imp (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb068AlphaDummy047) (SemanticCore.Class.cv nb068AlphaDummy000) (SemanticCore.Class.cv nb068AlphaDummy046)).neg) ((Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb068AlphaDummy048 f)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)) (SemanticCore.Class.cv (nb068AlphaDummy050 f))).imp (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb068AlphaDummy050 f)) (SemanticCore.Class.cv f) (SemanticCore.Class.cv (nb068AlphaDummy049 f))).neg)

                  Checked nominal proof certificate identified upstream as nb068_split_alpha_0060.

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

                    Certificates from NAR4C068C001Part030.

                    source
                    noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0061 (x y f : SemanticCore.Var) :
                    Nominal.TAlphaWff [(nb068AlphaDummy259, nb068AlphaDummy262 f), (nb068AlphaDummy258, nb068AlphaDummy261 f), (nb068AlphaDummy257, nb068AlphaDummy260 f), (nb068AlphaDummy255, nb068AlphaDummy256 f), (nb068AlphaDummy251, nb068AlphaDummy253 f), (nb068AlphaDummy252, nb068AlphaDummy254 f), (nb068AlphaDummy244, nb068AlphaDummy246 f), (nb068AlphaDummy243, nb068AlphaDummy245 f), (nb068AlphaDummy249, nb068AlphaDummy250 f), (nb068AlphaDummy247, nb068AlphaDummy248 f), (nb068AlphaDummy240, nb068AlphaDummy242 f), (nb068AlphaDummy239, nb068AlphaDummy241 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb068AlphaDummy258) (SemanticCore.Class.cv nb068AlphaDummy259)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy257) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb068AlphaDummy258) (SemanticCore.Class.cv nb068AlphaDummy259))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb068AlphaDummy261 f)) (SemanticCore.Class.cv (nb068AlphaDummy262 f))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy260 f)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb068AlphaDummy261 f)) (SemanticCore.Class.cv (nb068AlphaDummy262 f)))).neg)

                    Checked nominal proof certificate identified upstream as nb068_split_alpha_0061.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      source
                      noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0062 (x y f : SemanticCore.Var) :
                      Nominal.TAlphaWff [(nb068AlphaDummy244, nb068AlphaDummy246 f), (nb068AlphaDummy243, nb068AlphaDummy245 f), (nb068AlphaDummy249, nb068AlphaDummy250 f), (nb068AlphaDummy247, nb068AlphaDummy248 f), (nb068AlphaDummy240, nb068AlphaDummy242 f), (nb068AlphaDummy239, nb068AlphaDummy241 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy243) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy244))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy245 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy246 f))))

                      Checked nominal proof certificate identified upstream as nb068_split_alpha_0062.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        source
                        noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0063 (x y f : SemanticCore.Var) :
                        Nominal.TAlphaWff [(nb068AlphaDummy259, nb068AlphaDummy262 f), (nb068AlphaDummy258, nb068AlphaDummy261 f), (nb068AlphaDummy257, nb068AlphaDummy260 f), (nb068AlphaDummy255, nb068AlphaDummy256 f), (nb068AlphaDummy251, nb068AlphaDummy253 f), (nb068AlphaDummy252, nb068AlphaDummy254 f), (nb068AlphaDummy277, nb068AlphaDummy278 f), (nb068AlphaDummy275, nb068AlphaDummy276 f), (nb068AlphaDummy244, nb068AlphaDummy246 f), (nb068AlphaDummy243, nb068AlphaDummy245 f), (nb068AlphaDummy273, nb068AlphaDummy274 f), (nb068AlphaDummy247, nb068AlphaDummy248 f), (nb068AlphaDummy240, nb068AlphaDummy242 f), (nb068AlphaDummy239, nb068AlphaDummy241 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb068AlphaDummy258) (SemanticCore.Class.cv nb068AlphaDummy259)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy257) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb068AlphaDummy258) (SemanticCore.Class.cv nb068AlphaDummy259))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb068AlphaDummy261 f)) (SemanticCore.Class.cv (nb068AlphaDummy262 f))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy260 f)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb068AlphaDummy261 f)) (SemanticCore.Class.cv (nb068AlphaDummy262 f)))).neg)

                        Checked nominal proof certificate identified upstream as nb068_split_alpha_0063.

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

                          Certificates from NAR4C068C001Part031.

                          source
                          noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0064 (x y f : SemanticCore.Var) :
                          Nominal.TAlphaWff [(nb068AlphaDummy251, nb068AlphaDummy253 f), (nb068AlphaDummy252, nb068AlphaDummy254 f), (nb068AlphaDummy277, nb068AlphaDummy278 f), (nb068AlphaDummy275, nb068AlphaDummy276 f), (nb068AlphaDummy244, nb068AlphaDummy246 f), (nb068AlphaDummy243, nb068AlphaDummy245 f), (nb068AlphaDummy273, nb068AlphaDummy274 f), (nb068AlphaDummy247, nb068AlphaDummy248 f), (nb068AlphaDummy240, nb068AlphaDummy242 f), (nb068AlphaDummy239, nb068AlphaDummy241 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy251) (SemanticCore.Class.cv nb068AlphaDummy244)).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy252) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy251) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb068AlphaDummy251) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv nb068AlphaDummy251))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy253 f)) (SemanticCore.Class.cv (nb068AlphaDummy246 f))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy254 f)) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy253 f)) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb068AlphaDummy253 f)) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv (nb068AlphaDummy253 f)))).neg)

                          Checked nominal proof certificate identified upstream as nb068_split_alpha_0064.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            source
                            noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0065 (x y f : SemanticCore.Var) :
                            Nominal.TAlphaWff [(nb068AlphaDummy273, nb068AlphaDummy274 f), (nb068AlphaDummy247, nb068AlphaDummy248 f), (nb068AlphaDummy240, nb068AlphaDummy242 f), (nb068AlphaDummy239, nb068AlphaDummy241 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy273) (SemanticCore.Class.cab nb068AlphaDummy243 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy244 (SemanticCore.Class.cv nb068AlphaDummy239) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy243) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy244)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy273) (SemanticCore.Class.cab nb068AlphaDummy243 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy244 (SemanticCore.Class.cv nb068AlphaDummy239) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy243) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy244)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy274 f)) (SemanticCore.Class.cab (nb068AlphaDummy245 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy246 f) (SemanticCore.Class.cv (nb068AlphaDummy241 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy245 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy246 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy274 f)) (SemanticCore.Class.cab (nb068AlphaDummy245 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy246 f) (SemanticCore.Class.cv (nb068AlphaDummy241 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy245 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy246 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg)

                            Checked nominal proof certificate identified upstream as nb068_split_alpha_0065.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              source
                              noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0066 (x y f : SemanticCore.Var) :
                              Nominal.TAlphaWff [(nb068AlphaDummy147, nb068AlphaDummy150 f), (nb068AlphaDummy146, nb068AlphaDummy149 f), (nb068AlphaDummy145, nb068AlphaDummy148 f), (nb068AlphaDummy143, nb068AlphaDummy144 f), (nb068AlphaDummy139, nb068AlphaDummy141 f), (nb068AlphaDummy140, nb068AlphaDummy142 f), (nb068AlphaDummy132, nb068AlphaDummy134 f), (nb068AlphaDummy131, nb068AlphaDummy133 f), (nb068AlphaDummy137, nb068AlphaDummy138 f), (nb068AlphaDummy135, nb068AlphaDummy136 f), (nb068AlphaDummy126, nb068AlphaDummy128 f), (nb068AlphaDummy125, nb068AlphaDummy127 f), (nb068AlphaDummy129, nb068AlphaDummy130 f), (nb068AlphaDummy240, nb068AlphaDummy242 f), (nb068AlphaDummy239, nb068AlphaDummy241 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb068AlphaDummy146) (SemanticCore.Class.cv nb068AlphaDummy147)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy145) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb068AlphaDummy146) (SemanticCore.Class.cv nb068AlphaDummy147))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb068AlphaDummy149 f)) (SemanticCore.Class.cv (nb068AlphaDummy150 f))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy148 f)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb068AlphaDummy149 f)) (SemanticCore.Class.cv (nb068AlphaDummy150 f)))).neg)

                              Checked nominal proof certificate identified upstream as nb068_split_alpha_0066.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                source
                                noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0067 (x y f : SemanticCore.Var) :
                                Nominal.TAlphaWff [(nb068AlphaDummy139, nb068AlphaDummy141 f), (nb068AlphaDummy140, nb068AlphaDummy142 f), (nb068AlphaDummy132, nb068AlphaDummy134 f), (nb068AlphaDummy131, nb068AlphaDummy133 f), (nb068AlphaDummy137, nb068AlphaDummy138 f), (nb068AlphaDummy135, nb068AlphaDummy136 f), (nb068AlphaDummy126, nb068AlphaDummy128 f), (nb068AlphaDummy125, nb068AlphaDummy127 f), (nb068AlphaDummy129, nb068AlphaDummy130 f), (nb068AlphaDummy240, nb068AlphaDummy242 f), (nb068AlphaDummy239, nb068AlphaDummy241 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy139) (SemanticCore.Class.cv nb068AlphaDummy132)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy140) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy139) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb068AlphaDummy139) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv nb068AlphaDummy139)))).neg (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy141 f)) (SemanticCore.Class.cv (nb068AlphaDummy134 f))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy142 f)) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy141 f)) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb068AlphaDummy141 f)) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv (nb068AlphaDummy141 f))))).neg

                                Checked nominal proof certificate identified upstream as nb068_split_alpha_0067.

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