Documentation

LeanPool.NFWeakPartition.Certificates.NAR4C068C001Block005

Nominal proof certificates grouped in dependency order.

Certificates from NAR4C068C001Part015.

source
noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0005 (x y f : SemanticCore.Var) :
Nominal.TAlphaWff [(nb068AlphaDummy069, nb068AlphaDummy072 f), (nb068AlphaDummy068, nb068AlphaDummy071 f), (nb068AlphaDummy067, nb068AlphaDummy070 f), (nb068AlphaDummy065, nb068AlphaDummy066 f), (nb068AlphaDummy061, nb068AlphaDummy063 f), (nb068AlphaDummy062, nb068AlphaDummy064 f), (nb068AlphaDummy054, nb068AlphaDummy056 f), (nb068AlphaDummy053, nb068AlphaDummy055 f), (nb068AlphaDummy059, nb068AlphaDummy060 f), (nb068AlphaDummy057, nb068AlphaDummy058 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 nb068AlphaDummy068) (SemanticCore.Class.cv nb068AlphaDummy069)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy067) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb068AlphaDummy068) (SemanticCore.Class.cv nb068AlphaDummy069))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb068AlphaDummy071 f)) (SemanticCore.Class.cv (nb068AlphaDummy072 f))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy070 f)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb068AlphaDummy071 f)) (SemanticCore.Class.cv (nb068AlphaDummy072 f)))).neg)

Checked nominal proof certificate identified upstream as nb068_split_alpha_0005.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0006 (x y f : SemanticCore.Var) :
    Nominal.TAlphaWff [(nb068AlphaDummy061, nb068AlphaDummy063 f), (nb068AlphaDummy062, nb068AlphaDummy064 f), (nb068AlphaDummy054, nb068AlphaDummy056 f), (nb068AlphaDummy053, nb068AlphaDummy055 f), (nb068AlphaDummy059, nb068AlphaDummy060 f), (nb068AlphaDummy057, nb068AlphaDummy058 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 nb068AlphaDummy061) (SemanticCore.Class.cv nb068AlphaDummy054)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy062) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy061) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb068AlphaDummy061) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv nb068AlphaDummy061)))).neg (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy063 f)) (SemanticCore.Class.cv (nb068AlphaDummy056 f))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy064 f)) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy063 f)) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb068AlphaDummy063 f)) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv (nb068AlphaDummy063 f))))).neg

    Checked nominal proof certificate identified upstream as nb068_split_alpha_0006.

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

      Certificates from NAR4C068C001Part016.

      source
      noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0007 (x y f : SemanticCore.Var) :
      Nominal.TAlphaWff [(nb068AlphaDummy069, nb068AlphaDummy072 f), (nb068AlphaDummy068, nb068AlphaDummy071 f), (nb068AlphaDummy067, nb068AlphaDummy070 f), (nb068AlphaDummy065, nb068AlphaDummy066 f), (nb068AlphaDummy061, nb068AlphaDummy063 f), (nb068AlphaDummy062, nb068AlphaDummy064 f), (nb068AlphaDummy087, nb068AlphaDummy088 f), (nb068AlphaDummy085, nb068AlphaDummy086 f), (nb068AlphaDummy054, nb068AlphaDummy056 f), (nb068AlphaDummy053, nb068AlphaDummy055 f), (nb068AlphaDummy083, nb068AlphaDummy084 f), (nb068AlphaDummy057, nb068AlphaDummy058 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 nb068AlphaDummy068) (SemanticCore.Class.cv nb068AlphaDummy069)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy067) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb068AlphaDummy068) (SemanticCore.Class.cv nb068AlphaDummy069))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb068AlphaDummy071 f)) (SemanticCore.Class.cv (nb068AlphaDummy072 f))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy070 f)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb068AlphaDummy071 f)) (SemanticCore.Class.cv (nb068AlphaDummy072 f)))).neg)

      Checked nominal proof certificate identified upstream as nb068_split_alpha_0007.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0008 (x y f : SemanticCore.Var) :
        Nominal.TAlphaWff [(nb068AlphaDummy061, nb068AlphaDummy063 f), (nb068AlphaDummy062, nb068AlphaDummy064 f), (nb068AlphaDummy087, nb068AlphaDummy088 f), (nb068AlphaDummy085, nb068AlphaDummy086 f), (nb068AlphaDummy054, nb068AlphaDummy056 f), (nb068AlphaDummy053, nb068AlphaDummy055 f), (nb068AlphaDummy083, nb068AlphaDummy084 f), (nb068AlphaDummy057, nb068AlphaDummy058 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 nb068AlphaDummy061) (SemanticCore.Class.cv nb068AlphaDummy054)).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy062) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy061) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb068AlphaDummy061) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv nb068AlphaDummy061))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy063 f)) (SemanticCore.Class.cv (nb068AlphaDummy056 f))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy064 f)) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy063 f)) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb068AlphaDummy063 f)) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv (nb068AlphaDummy063 f)))).neg)

        Checked nominal proof certificate identified upstream as nb068_split_alpha_0008.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0009 (x y f : SemanticCore.Var) :
          Nominal.TAlphaWff [(nb068AlphaDummy083, nb068AlphaDummy084 f), (nb068AlphaDummy057, nb068AlphaDummy058 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 nb068AlphaDummy083) (SemanticCore.Class.cab nb068AlphaDummy053 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy054 (SemanticCore.Class.cv nb068AlphaDummy046) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy053) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy054)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy083) (SemanticCore.Class.cab nb068AlphaDummy053 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy054 (SemanticCore.Class.cv nb068AlphaDummy046) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy053) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy054)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy084 f)) (SemanticCore.Class.cab (nb068AlphaDummy055 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy056 f) (SemanticCore.Class.cv (nb068AlphaDummy049 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy055 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy056 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy084 f)) (SemanticCore.Class.cab (nb068AlphaDummy055 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy056 f) (SemanticCore.Class.cv (nb068AlphaDummy049 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy055 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy056 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg)

          Checked nominal proof certificate identified upstream as nb068_split_alpha_0009.

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

            Certificates from NAR4C068C001Part017.

            source
            noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0010 (x y f : SemanticCore.Var) :
            Nominal.TAlphaWff [(nb068AlphaDummy105, nb068AlphaDummy108 f), (nb068AlphaDummy104, nb068AlphaDummy107 f), (nb068AlphaDummy103, nb068AlphaDummy106 f), (nb068AlphaDummy101, nb068AlphaDummy102 f), (nb068AlphaDummy097, nb068AlphaDummy099 f), (nb068AlphaDummy098, nb068AlphaDummy100 f), (nb068AlphaDummy090, nb068AlphaDummy092 f), (nb068AlphaDummy089, nb068AlphaDummy091 f), (nb068AlphaDummy095, nb068AlphaDummy096 f), (nb068AlphaDummy093, nb068AlphaDummy094 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 nb068AlphaDummy104) (SemanticCore.Class.cv nb068AlphaDummy105)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy103) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb068AlphaDummy104) (SemanticCore.Class.cv nb068AlphaDummy105))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb068AlphaDummy107 f)) (SemanticCore.Class.cv (nb068AlphaDummy108 f))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy106 f)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb068AlphaDummy107 f)) (SemanticCore.Class.cv (nb068AlphaDummy108 f)))).neg)

            Checked nominal proof certificate identified upstream as nb068_split_alpha_0010.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0011 (x y f : SemanticCore.Var) :
              Nominal.TAlphaWff [(nb068AlphaDummy097, nb068AlphaDummy099 f), (nb068AlphaDummy098, nb068AlphaDummy100 f), (nb068AlphaDummy090, nb068AlphaDummy092 f), (nb068AlphaDummy089, nb068AlphaDummy091 f), (nb068AlphaDummy095, nb068AlphaDummy096 f), (nb068AlphaDummy093, nb068AlphaDummy094 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 nb068AlphaDummy097) (SemanticCore.Class.cv nb068AlphaDummy090)).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy098) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy097) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb068AlphaDummy097) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv nb068AlphaDummy097))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy099 f)) (SemanticCore.Class.cv (nb068AlphaDummy092 f))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy100 f)) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy099 f)) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb068AlphaDummy099 f)) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv (nb068AlphaDummy099 f)))).neg)

              Checked nominal proof certificate identified upstream as nb068_split_alpha_0011.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0012 (x y f : SemanticCore.Var) :
                Nominal.TAlphaWff [(nb068AlphaDummy105, nb068AlphaDummy108 f), (nb068AlphaDummy104, nb068AlphaDummy107 f), (nb068AlphaDummy103, nb068AlphaDummy106 f), (nb068AlphaDummy101, nb068AlphaDummy102 f), (nb068AlphaDummy097, nb068AlphaDummy099 f), (nb068AlphaDummy098, nb068AlphaDummy100 f), (nb068AlphaDummy123, nb068AlphaDummy124 f), (nb068AlphaDummy121, nb068AlphaDummy122 f), (nb068AlphaDummy090, nb068AlphaDummy092 f), (nb068AlphaDummy089, nb068AlphaDummy091 f), (nb068AlphaDummy119, nb068AlphaDummy120 f), (nb068AlphaDummy093, nb068AlphaDummy094 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 nb068AlphaDummy104) (SemanticCore.Class.cv nb068AlphaDummy105)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy103) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb068AlphaDummy104) (SemanticCore.Class.cv nb068AlphaDummy105))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb068AlphaDummy107 f)) (SemanticCore.Class.cv (nb068AlphaDummy108 f))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy106 f)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb068AlphaDummy107 f)) (SemanticCore.Class.cv (nb068AlphaDummy108 f)))).neg)

                Checked nominal proof certificate identified upstream as nb068_split_alpha_0012.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0013 (x y f : SemanticCore.Var) :
                  Nominal.TAlphaWff [(nb068AlphaDummy097, nb068AlphaDummy099 f), (nb068AlphaDummy098, nb068AlphaDummy100 f), (nb068AlphaDummy123, nb068AlphaDummy124 f), (nb068AlphaDummy121, nb068AlphaDummy122 f), (nb068AlphaDummy090, nb068AlphaDummy092 f), (nb068AlphaDummy089, nb068AlphaDummy091 f), (nb068AlphaDummy119, nb068AlphaDummy120 f), (nb068AlphaDummy093, nb068AlphaDummy094 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 nb068AlphaDummy097) (SemanticCore.Class.cv nb068AlphaDummy090)).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy098) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy097) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb068AlphaDummy097) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv nb068AlphaDummy097))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy099 f)) (SemanticCore.Class.cv (nb068AlphaDummy092 f))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy100 f)) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy099 f)) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb068AlphaDummy099 f)) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv (nb068AlphaDummy099 f)))).neg)

                  Checked nominal proof certificate identified upstream as nb068_split_alpha_0013.

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

                    Certificates from NAR4C068C001Part018.

                    source
                    noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0014 (x y f : SemanticCore.Var) :
                    Nominal.TAlphaWff [(nb068AlphaDummy119, nb068AlphaDummy120 f), (nb068AlphaDummy093, nb068AlphaDummy094 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 nb068AlphaDummy119) (SemanticCore.Class.cab nb068AlphaDummy089 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy090 (SemanticCore.Class.cv nb068AlphaDummy047) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy089) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy090)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy119) (SemanticCore.Class.cab nb068AlphaDummy089 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy090 (SemanticCore.Class.cv nb068AlphaDummy047) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy089) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy090)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy120 f)) (SemanticCore.Class.cab (nb068AlphaDummy091 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy092 f) (SemanticCore.Class.cv (nb068AlphaDummy050 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy091 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy092 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy120 f)) (SemanticCore.Class.cab (nb068AlphaDummy091 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy092 f) (SemanticCore.Class.cv (nb068AlphaDummy050 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy091 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy092 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg)

                    Checked nominal proof certificate identified upstream as nb068_split_alpha_0014.

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

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

                        Checked nominal proof certificate identified upstream as nb068_split_alpha_0016.

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

                          Certificates from NAR4C068C001Part019.

                          source
                          noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0017 (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), (nb068AlphaDummy165, nb068AlphaDummy166 f), (nb068AlphaDummy163, nb068AlphaDummy164 f), (nb068AlphaDummy132, nb068AlphaDummy134 f), (nb068AlphaDummy131, nb068AlphaDummy133 f), (nb068AlphaDummy161, nb068AlphaDummy162 f), (nb068AlphaDummy135, nb068AlphaDummy136 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.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_0017.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            source
                            noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0018 (x y f : SemanticCore.Var) :
                            Nominal.TAlphaWff [(nb068AlphaDummy143, nb068AlphaDummy144 f), (nb068AlphaDummy139, nb068AlphaDummy141 f), (nb068AlphaDummy140, nb068AlphaDummy142 f), (nb068AlphaDummy165, nb068AlphaDummy166 f), (nb068AlphaDummy163, nb068AlphaDummy164 f), (nb068AlphaDummy132, nb068AlphaDummy134 f), (nb068AlphaDummy131, nb068AlphaDummy133 f), (nb068AlphaDummy161, nb068AlphaDummy162 f), (nb068AlphaDummy135, nb068AlphaDummy136 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 nb068AlphaDummy143) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb068AlphaDummy139) Compiler.CompactSourceSyntax.synC1c)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy139) Compiler.CompactSourceSyntax.synCnnc)).neg.imp (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy143) (SemanticCore.Class.cv nb068AlphaDummy139)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy139) Compiler.CompactSourceSyntax.synCnnc).neg)) ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy144 f)) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb068AlphaDummy141 f)) Compiler.CompactSourceSyntax.synC1c)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy141 f)) Compiler.CompactSourceSyntax.synCnnc)).neg.imp (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy144 f)) (SemanticCore.Class.cv (nb068AlphaDummy141 f))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy141 f)) Compiler.CompactSourceSyntax.synCnnc).neg))

                            Checked nominal proof certificate identified upstream as nb068_split_alpha_0018.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              source
                              noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0019 (x y f : SemanticCore.Var) :
                              Nominal.TAlphaWff [(nb068AlphaDummy161, nb068AlphaDummy162 f), (nb068AlphaDummy135, nb068AlphaDummy136 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.classMem (SemanticCore.Class.cv nb068AlphaDummy161) (SemanticCore.Class.cab nb068AlphaDummy131 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy132 (SemanticCore.Class.cv nb068AlphaDummy126) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy131) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy132)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy161) (SemanticCore.Class.cab nb068AlphaDummy131 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy132 (SemanticCore.Class.cv nb068AlphaDummy126) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy131) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy132)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy162 f)) (SemanticCore.Class.cab (nb068AlphaDummy133 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy134 f) (SemanticCore.Class.cv (nb068AlphaDummy128 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy133 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy134 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy162 f)) (SemanticCore.Class.cab (nb068AlphaDummy133 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy134 f) (SemanticCore.Class.cv (nb068AlphaDummy128 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy133 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy134 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg)

                              Checked nominal proof certificate identified upstream as nb068_split_alpha_0019.

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

                                Certificates from NAR4C068C001Part020.

                                source
                                noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0020 (x y f : SemanticCore.Var) :
                                Nominal.TAlphaWff [(nb068AlphaDummy183, nb068AlphaDummy186 f), (nb068AlphaDummy182, nb068AlphaDummy185 f), (nb068AlphaDummy181, nb068AlphaDummy184 f), (nb068AlphaDummy179, nb068AlphaDummy180 f), (nb068AlphaDummy175, nb068AlphaDummy177 f), (nb068AlphaDummy176, nb068AlphaDummy178 f), (nb068AlphaDummy168, nb068AlphaDummy170 f), (nb068AlphaDummy167, nb068AlphaDummy169 f), (nb068AlphaDummy173, nb068AlphaDummy174 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.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb068AlphaDummy182) (SemanticCore.Class.cv nb068AlphaDummy183)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy181) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb068AlphaDummy182) (SemanticCore.Class.cv nb068AlphaDummy183))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb068AlphaDummy185 f)) (SemanticCore.Class.cv (nb068AlphaDummy186 f))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy184 f)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb068AlphaDummy185 f)) (SemanticCore.Class.cv (nb068AlphaDummy186 f)))).neg)

                                Checked nominal proof certificate identified upstream as nb068_split_alpha_0020.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  source
                                  noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0021 (x y f : SemanticCore.Var) :
                                  Nominal.TAlphaWff [(nb068AlphaDummy175, nb068AlphaDummy177 f), (nb068AlphaDummy176, nb068AlphaDummy178 f), (nb068AlphaDummy168, nb068AlphaDummy170 f), (nb068AlphaDummy167, nb068AlphaDummy169 f), (nb068AlphaDummy173, nb068AlphaDummy174 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.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_0021.

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    source
                                    noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0022 (x y f : SemanticCore.Var) :
                                    Nominal.TAlphaWff [(nb068AlphaDummy183, nb068AlphaDummy186 f), (nb068AlphaDummy182, nb068AlphaDummy185 f), (nb068AlphaDummy181, nb068AlphaDummy184 f), (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)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb068AlphaDummy182) (SemanticCore.Class.cv nb068AlphaDummy183)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy181) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb068AlphaDummy182) (SemanticCore.Class.cv nb068AlphaDummy183))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb068AlphaDummy185 f)) (SemanticCore.Class.cv (nb068AlphaDummy186 f))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy184 f)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb068AlphaDummy185 f)) (SemanticCore.Class.cv (nb068AlphaDummy186 f)))).neg)

                                    Checked nominal proof certificate identified upstream as nb068_split_alpha_0022.

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