Documentation

LeanPool.NFWeakPartition.Certificates.NAR4C057C001Block004

Nominal proof certificates grouped in dependency order.

Certificates from NAR4C057C001Part009.

source
noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057SplitAlpha0005 (f a : SemanticCore.Var) :
Nominal.TAlphaWff [(nb057AlphaDummy068, nb057AlphaDummy071 f), (nb057AlphaDummy067, nb057AlphaDummy070 f), (nb057AlphaDummy066, nb057AlphaDummy069 f), (nb057AlphaDummy064, nb057AlphaDummy065 f), (nb057AlphaDummy060, nb057AlphaDummy062 f), (nb057AlphaDummy061, nb057AlphaDummy063 f), (nb057AlphaDummy053, nb057AlphaDummy055 f), (nb057AlphaDummy052, nb057AlphaDummy054 f), (nb057AlphaDummy058, nb057AlphaDummy059 f), (nb057AlphaDummy056, nb057AlphaDummy057 f), (nb057AlphaDummy045, nb057AlphaDummy048 f), (nb057AlphaDummy044, nb057AlphaDummy047 f), (nb057AlphaDummy050, nb057AlphaDummy051 f), (nb057AlphaDummy042, nb057AlphaDummy043 f), (nb057AlphaDummy040, nb057AlphaDummy041 f), (nb057AlphaDummy000, a), (nb057AlphaDummy001, f), (nb057AlphaDummy002, nb057AlphaDummy003 f a)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb057AlphaDummy067) (SemanticCore.Class.cv nb057AlphaDummy068)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy066) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb057AlphaDummy067) (SemanticCore.Class.cv nb057AlphaDummy068))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb057AlphaDummy070 f)) (SemanticCore.Class.cv (nb057AlphaDummy071 f))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy069 f)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb057AlphaDummy070 f)) (SemanticCore.Class.cv (nb057AlphaDummy071 f)))).neg)

Checked nominal proof certificate identified upstream as nb057_split_alpha_0005.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057SplitAlpha0006 (f a : SemanticCore.Var) :
    Nominal.TAlphaWff [(nb057AlphaDummy053, nb057AlphaDummy055 f), (nb057AlphaDummy052, nb057AlphaDummy054 f), (nb057AlphaDummy058, nb057AlphaDummy059 f), (nb057AlphaDummy056, nb057AlphaDummy057 f), (nb057AlphaDummy045, nb057AlphaDummy048 f), (nb057AlphaDummy044, nb057AlphaDummy047 f), (nb057AlphaDummy050, nb057AlphaDummy051 f), (nb057AlphaDummy042, nb057AlphaDummy043 f), (nb057AlphaDummy040, nb057AlphaDummy041 f), (nb057AlphaDummy000, a), (nb057AlphaDummy001, f), (nb057AlphaDummy002, nb057AlphaDummy003 f a)] (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy052) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy053))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy054 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy055 f))))

    Checked nominal proof certificate identified upstream as nb057_split_alpha_0006.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057SplitAlpha0007 (f a : SemanticCore.Var) :
      Nominal.TAlphaWff [(nb057AlphaDummy068, nb057AlphaDummy071 f), (nb057AlphaDummy067, nb057AlphaDummy070 f), (nb057AlphaDummy066, nb057AlphaDummy069 f), (nb057AlphaDummy064, nb057AlphaDummy065 f), (nb057AlphaDummy060, nb057AlphaDummy062 f), (nb057AlphaDummy061, nb057AlphaDummy063 f), (nb057AlphaDummy086, nb057AlphaDummy087 f), (nb057AlphaDummy084, nb057AlphaDummy085 f), (nb057AlphaDummy053, nb057AlphaDummy055 f), (nb057AlphaDummy052, nb057AlphaDummy054 f), (nb057AlphaDummy082, nb057AlphaDummy083 f), (nb057AlphaDummy056, nb057AlphaDummy057 f), (nb057AlphaDummy045, nb057AlphaDummy048 f), (nb057AlphaDummy044, nb057AlphaDummy047 f), (nb057AlphaDummy050, nb057AlphaDummy051 f), (nb057AlphaDummy042, nb057AlphaDummy043 f), (nb057AlphaDummy040, nb057AlphaDummy041 f), (nb057AlphaDummy000, a), (nb057AlphaDummy001, f), (nb057AlphaDummy002, nb057AlphaDummy003 f a)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb057AlphaDummy067) (SemanticCore.Class.cv nb057AlphaDummy068)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy066) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb057AlphaDummy067) (SemanticCore.Class.cv nb057AlphaDummy068))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb057AlphaDummy070 f)) (SemanticCore.Class.cv (nb057AlphaDummy071 f))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy069 f)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb057AlphaDummy070 f)) (SemanticCore.Class.cv (nb057AlphaDummy071 f)))).neg)

      Checked nominal proof certificate identified upstream as nb057_split_alpha_0007.

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

        Certificates from NAR4C057C001Part010.

        source
        noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057SplitAlpha0008 (f a : SemanticCore.Var) :
        Nominal.TAlphaWff [(nb057AlphaDummy060, nb057AlphaDummy062 f), (nb057AlphaDummy061, nb057AlphaDummy063 f), (nb057AlphaDummy086, nb057AlphaDummy087 f), (nb057AlphaDummy084, nb057AlphaDummy085 f), (nb057AlphaDummy053, nb057AlphaDummy055 f), (nb057AlphaDummy052, nb057AlphaDummy054 f), (nb057AlphaDummy082, nb057AlphaDummy083 f), (nb057AlphaDummy056, nb057AlphaDummy057 f), (nb057AlphaDummy045, nb057AlphaDummy048 f), (nb057AlphaDummy044, nb057AlphaDummy047 f), (nb057AlphaDummy050, nb057AlphaDummy051 f), (nb057AlphaDummy042, nb057AlphaDummy043 f), (nb057AlphaDummy040, nb057AlphaDummy041 f), (nb057AlphaDummy000, a), (nb057AlphaDummy001, f), (nb057AlphaDummy002, nb057AlphaDummy003 f a)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb057AlphaDummy060) (SemanticCore.Class.cv nb057AlphaDummy053)).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy061) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb057AlphaDummy060) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb057AlphaDummy060) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv nb057AlphaDummy060))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb057AlphaDummy062 f)) (SemanticCore.Class.cv (nb057AlphaDummy055 f))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy063 f)) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb057AlphaDummy062 f)) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb057AlphaDummy062 f)) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv (nb057AlphaDummy062 f)))).neg)

        Checked nominal proof certificate identified upstream as nb057_split_alpha_0008.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057SplitAlpha0009 (f a : SemanticCore.Var) :
          Nominal.TAlphaWff [(nb057AlphaDummy082, nb057AlphaDummy083 f), (nb057AlphaDummy056, nb057AlphaDummy057 f), (nb057AlphaDummy045, nb057AlphaDummy048 f), (nb057AlphaDummy044, nb057AlphaDummy047 f), (nb057AlphaDummy050, nb057AlphaDummy051 f), (nb057AlphaDummy042, nb057AlphaDummy043 f), (nb057AlphaDummy040, nb057AlphaDummy041 f), (nb057AlphaDummy000, a), (nb057AlphaDummy001, f), (nb057AlphaDummy002, nb057AlphaDummy003 f a)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb057AlphaDummy082) (SemanticCore.Class.cab nb057AlphaDummy052 (Compiler.CompactSourceSyntax.synWrex nb057AlphaDummy053 (SemanticCore.Class.cv nb057AlphaDummy045) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy052) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy053)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb057AlphaDummy082) (SemanticCore.Class.cab nb057AlphaDummy052 (Compiler.CompactSourceSyntax.synWrex nb057AlphaDummy053 (SemanticCore.Class.cv nb057AlphaDummy045) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy052) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy053)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb057AlphaDummy083 f)) (SemanticCore.Class.cab (nb057AlphaDummy054 f) (Compiler.CompactSourceSyntax.synWrex (nb057AlphaDummy055 f) (SemanticCore.Class.cv (nb057AlphaDummy048 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy054 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy055 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb057AlphaDummy083 f)) (SemanticCore.Class.cab (nb057AlphaDummy054 f) (Compiler.CompactSourceSyntax.synWrex (nb057AlphaDummy055 f) (SemanticCore.Class.cv (nb057AlphaDummy048 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy054 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy055 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg)

          Checked nominal proof certificate identified upstream as nb057_split_alpha_0009.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057SplitAlpha0010 (f a : SemanticCore.Var) :
            Nominal.TAlphaWff [(nb057AlphaDummy104, nb057AlphaDummy107 f), (nb057AlphaDummy103, nb057AlphaDummy106 f), (nb057AlphaDummy102, nb057AlphaDummy105 f), (nb057AlphaDummy100, nb057AlphaDummy101 f), (nb057AlphaDummy096, nb057AlphaDummy098 f), (nb057AlphaDummy097, nb057AlphaDummy099 f), (nb057AlphaDummy089, nb057AlphaDummy091 f), (nb057AlphaDummy088, nb057AlphaDummy090 f), (nb057AlphaDummy094, nb057AlphaDummy095 f), (nb057AlphaDummy092, nb057AlphaDummy093 f), (nb057AlphaDummy046, nb057AlphaDummy049 f), (nb057AlphaDummy045, nb057AlphaDummy048 f), (nb057AlphaDummy044, nb057AlphaDummy047 f), (nb057AlphaDummy050, nb057AlphaDummy051 f), (nb057AlphaDummy042, nb057AlphaDummy043 f), (nb057AlphaDummy040, nb057AlphaDummy041 f), (nb057AlphaDummy000, a), (nb057AlphaDummy001, f), (nb057AlphaDummy002, nb057AlphaDummy003 f a)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb057AlphaDummy103) (SemanticCore.Class.cv nb057AlphaDummy104)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy102) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb057AlphaDummy103) (SemanticCore.Class.cv nb057AlphaDummy104))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb057AlphaDummy106 f)) (SemanticCore.Class.cv (nb057AlphaDummy107 f))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy105 f)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb057AlphaDummy106 f)) (SemanticCore.Class.cv (nb057AlphaDummy107 f)))).neg)

            Checked nominal proof certificate identified upstream as nb057_split_alpha_0010.

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

              Certificates from NAR4C057C001Part011.

              source
              noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057SplitAlpha0011 (f a : SemanticCore.Var) :
              Nominal.TAlphaWff [(nb057AlphaDummy096, nb057AlphaDummy098 f), (nb057AlphaDummy097, nb057AlphaDummy099 f), (nb057AlphaDummy089, nb057AlphaDummy091 f), (nb057AlphaDummy088, nb057AlphaDummy090 f), (nb057AlphaDummy094, nb057AlphaDummy095 f), (nb057AlphaDummy092, nb057AlphaDummy093 f), (nb057AlphaDummy046, nb057AlphaDummy049 f), (nb057AlphaDummy045, nb057AlphaDummy048 f), (nb057AlphaDummy044, nb057AlphaDummy047 f), (nb057AlphaDummy050, nb057AlphaDummy051 f), (nb057AlphaDummy042, nb057AlphaDummy043 f), (nb057AlphaDummy040, nb057AlphaDummy041 f), (nb057AlphaDummy000, a), (nb057AlphaDummy001, f), (nb057AlphaDummy002, nb057AlphaDummy003 f a)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb057AlphaDummy096) (SemanticCore.Class.cv nb057AlphaDummy089)).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy097) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb057AlphaDummy096) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb057AlphaDummy096) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv nb057AlphaDummy096))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb057AlphaDummy098 f)) (SemanticCore.Class.cv (nb057AlphaDummy091 f))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy099 f)) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb057AlphaDummy098 f)) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb057AlphaDummy098 f)) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv (nb057AlphaDummy098 f)))).neg)

              Checked nominal proof certificate identified upstream as nb057_split_alpha_0011.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057SplitAlpha0012 (f a : SemanticCore.Var) :
                Nominal.TAlphaWff [(nb057AlphaDummy104, nb057AlphaDummy107 f), (nb057AlphaDummy103, nb057AlphaDummy106 f), (nb057AlphaDummy102, nb057AlphaDummy105 f), (nb057AlphaDummy100, nb057AlphaDummy101 f), (nb057AlphaDummy096, nb057AlphaDummy098 f), (nb057AlphaDummy097, nb057AlphaDummy099 f), (nb057AlphaDummy122, nb057AlphaDummy123 f), (nb057AlphaDummy120, nb057AlphaDummy121 f), (nb057AlphaDummy089, nb057AlphaDummy091 f), (nb057AlphaDummy088, nb057AlphaDummy090 f), (nb057AlphaDummy118, nb057AlphaDummy119 f), (nb057AlphaDummy092, nb057AlphaDummy093 f), (nb057AlphaDummy046, nb057AlphaDummy049 f), (nb057AlphaDummy045, nb057AlphaDummy048 f), (nb057AlphaDummy044, nb057AlphaDummy047 f), (nb057AlphaDummy050, nb057AlphaDummy051 f), (nb057AlphaDummy042, nb057AlphaDummy043 f), (nb057AlphaDummy040, nb057AlphaDummy041 f), (nb057AlphaDummy000, a), (nb057AlphaDummy001, f), (nb057AlphaDummy002, nb057AlphaDummy003 f a)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb057AlphaDummy103) (SemanticCore.Class.cv nb057AlphaDummy104)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy102) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb057AlphaDummy103) (SemanticCore.Class.cv nb057AlphaDummy104))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb057AlphaDummy106 f)) (SemanticCore.Class.cv (nb057AlphaDummy107 f))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy105 f)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb057AlphaDummy106 f)) (SemanticCore.Class.cv (nb057AlphaDummy107 f)))).neg)

                Checked nominal proof certificate identified upstream as nb057_split_alpha_0012.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057SplitAlpha0013 (f a : SemanticCore.Var) :
                  Nominal.TAlphaWff [(nb057AlphaDummy096, nb057AlphaDummy098 f), (nb057AlphaDummy097, nb057AlphaDummy099 f), (nb057AlphaDummy122, nb057AlphaDummy123 f), (nb057AlphaDummy120, nb057AlphaDummy121 f), (nb057AlphaDummy089, nb057AlphaDummy091 f), (nb057AlphaDummy088, nb057AlphaDummy090 f), (nb057AlphaDummy118, nb057AlphaDummy119 f), (nb057AlphaDummy092, nb057AlphaDummy093 f), (nb057AlphaDummy046, nb057AlphaDummy049 f), (nb057AlphaDummy045, nb057AlphaDummy048 f), (nb057AlphaDummy044, nb057AlphaDummy047 f), (nb057AlphaDummy050, nb057AlphaDummy051 f), (nb057AlphaDummy042, nb057AlphaDummy043 f), (nb057AlphaDummy040, nb057AlphaDummy041 f), (nb057AlphaDummy000, a), (nb057AlphaDummy001, f), (nb057AlphaDummy002, nb057AlphaDummy003 f a)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb057AlphaDummy096) (SemanticCore.Class.cv nb057AlphaDummy089)).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy097) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb057AlphaDummy096) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb057AlphaDummy096) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv nb057AlphaDummy096))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb057AlphaDummy098 f)) (SemanticCore.Class.cv (nb057AlphaDummy091 f))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy099 f)) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb057AlphaDummy098 f)) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb057AlphaDummy098 f)) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv (nb057AlphaDummy098 f)))).neg)

                  Checked nominal proof certificate identified upstream as nb057_split_alpha_0013.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057SplitAlpha0014 (f a : SemanticCore.Var) :
                    Nominal.TAlphaWff [(nb057AlphaDummy118, nb057AlphaDummy119 f), (nb057AlphaDummy092, nb057AlphaDummy093 f), (nb057AlphaDummy046, nb057AlphaDummy049 f), (nb057AlphaDummy045, nb057AlphaDummy048 f), (nb057AlphaDummy044, nb057AlphaDummy047 f), (nb057AlphaDummy050, nb057AlphaDummy051 f), (nb057AlphaDummy042, nb057AlphaDummy043 f), (nb057AlphaDummy040, nb057AlphaDummy041 f), (nb057AlphaDummy000, a), (nb057AlphaDummy001, f), (nb057AlphaDummy002, nb057AlphaDummy003 f a)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb057AlphaDummy118) (SemanticCore.Class.cab nb057AlphaDummy088 (Compiler.CompactSourceSyntax.synWrex nb057AlphaDummy089 (SemanticCore.Class.cv nb057AlphaDummy046) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy088) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy089)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb057AlphaDummy118) (SemanticCore.Class.cab nb057AlphaDummy088 (Compiler.CompactSourceSyntax.synWrex nb057AlphaDummy089 (SemanticCore.Class.cv nb057AlphaDummy046) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy088) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy089)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb057AlphaDummy119 f)) (SemanticCore.Class.cab (nb057AlphaDummy090 f) (Compiler.CompactSourceSyntax.synWrex (nb057AlphaDummy091 f) (SemanticCore.Class.cv (nb057AlphaDummy049 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy090 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy091 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb057AlphaDummy119 f)) (SemanticCore.Class.cab (nb057AlphaDummy090 f) (Compiler.CompactSourceSyntax.synWrex (nb057AlphaDummy091 f) (SemanticCore.Class.cv (nb057AlphaDummy049 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy090 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy091 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg)

                    Checked nominal proof certificate identified upstream as nb057_split_alpha_0014.

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

                      Certificates from NAR4C057C001Part012.

                      source
                      noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057SplitAlpha0015 (f a : SemanticCore.Var) :
                      Nominal.TAlphaWff [(nb057AlphaDummy146, nb057AlphaDummy149 f), (nb057AlphaDummy145, nb057AlphaDummy148 f), (nb057AlphaDummy144, nb057AlphaDummy147 f), (nb057AlphaDummy142, nb057AlphaDummy143 f), (nb057AlphaDummy138, nb057AlphaDummy140 f), (nb057AlphaDummy139, nb057AlphaDummy141 f), (nb057AlphaDummy131, nb057AlphaDummy133 f), (nb057AlphaDummy130, nb057AlphaDummy132 f), (nb057AlphaDummy136, nb057AlphaDummy137 f), (nb057AlphaDummy134, nb057AlphaDummy135 f), (nb057AlphaDummy125, nb057AlphaDummy127 f), (nb057AlphaDummy124, nb057AlphaDummy126 f), (nb057AlphaDummy128, nb057AlphaDummy129 f), (nb057AlphaDummy046, nb057AlphaDummy049 f), (nb057AlphaDummy045, nb057AlphaDummy048 f), (nb057AlphaDummy044, nb057AlphaDummy047 f), (nb057AlphaDummy050, nb057AlphaDummy051 f), (nb057AlphaDummy042, nb057AlphaDummy043 f), (nb057AlphaDummy040, nb057AlphaDummy041 f), (nb057AlphaDummy000, a), (nb057AlphaDummy001, f), (nb057AlphaDummy002, nb057AlphaDummy003 f a)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb057AlphaDummy145) (SemanticCore.Class.cv nb057AlphaDummy146)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy144) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb057AlphaDummy145) (SemanticCore.Class.cv nb057AlphaDummy146))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb057AlphaDummy148 f)) (SemanticCore.Class.cv (nb057AlphaDummy149 f))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy147 f)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb057AlphaDummy148 f)) (SemanticCore.Class.cv (nb057AlphaDummy149 f)))).neg)

                      Checked nominal proof certificate identified upstream as nb057_split_alpha_0015.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        source
                        noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057SplitAlpha0016 (f a : SemanticCore.Var) :
                        Nominal.TAlphaWff [(nb057AlphaDummy138, nb057AlphaDummy140 f), (nb057AlphaDummy139, nb057AlphaDummy141 f), (nb057AlphaDummy131, nb057AlphaDummy133 f), (nb057AlphaDummy130, nb057AlphaDummy132 f), (nb057AlphaDummy136, nb057AlphaDummy137 f), (nb057AlphaDummy134, nb057AlphaDummy135 f), (nb057AlphaDummy125, nb057AlphaDummy127 f), (nb057AlphaDummy124, nb057AlphaDummy126 f), (nb057AlphaDummy128, nb057AlphaDummy129 f), (nb057AlphaDummy046, nb057AlphaDummy049 f), (nb057AlphaDummy045, nb057AlphaDummy048 f), (nb057AlphaDummy044, nb057AlphaDummy047 f), (nb057AlphaDummy050, nb057AlphaDummy051 f), (nb057AlphaDummy042, nb057AlphaDummy043 f), (nb057AlphaDummy040, nb057AlphaDummy041 f), (nb057AlphaDummy000, a), (nb057AlphaDummy001, f), (nb057AlphaDummy002, nb057AlphaDummy003 f a)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb057AlphaDummy138) (SemanticCore.Class.cv nb057AlphaDummy131)).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy139) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb057AlphaDummy138) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb057AlphaDummy138) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv nb057AlphaDummy138))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb057AlphaDummy140 f)) (SemanticCore.Class.cv (nb057AlphaDummy133 f))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy141 f)) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb057AlphaDummy140 f)) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb057AlphaDummy140 f)) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv (nb057AlphaDummy140 f)))).neg)

                        Checked nominal proof certificate identified upstream as nb057_split_alpha_0016.

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

                          Certificates from NAR4C057C001Part013.

                          source
                          noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057SplitAlpha0017 (f a : SemanticCore.Var) :
                          Nominal.TAlphaWff [(nb057AlphaDummy146, nb057AlphaDummy149 f), (nb057AlphaDummy145, nb057AlphaDummy148 f), (nb057AlphaDummy144, nb057AlphaDummy147 f), (nb057AlphaDummy142, nb057AlphaDummy143 f), (nb057AlphaDummy138, nb057AlphaDummy140 f), (nb057AlphaDummy139, nb057AlphaDummy141 f), (nb057AlphaDummy164, nb057AlphaDummy165 f), (nb057AlphaDummy162, nb057AlphaDummy163 f), (nb057AlphaDummy131, nb057AlphaDummy133 f), (nb057AlphaDummy130, nb057AlphaDummy132 f), (nb057AlphaDummy160, nb057AlphaDummy161 f), (nb057AlphaDummy134, nb057AlphaDummy135 f), (nb057AlphaDummy125, nb057AlphaDummy127 f), (nb057AlphaDummy124, nb057AlphaDummy126 f), (nb057AlphaDummy128, nb057AlphaDummy129 f), (nb057AlphaDummy046, nb057AlphaDummy049 f), (nb057AlphaDummy045, nb057AlphaDummy048 f), (nb057AlphaDummy044, nb057AlphaDummy047 f), (nb057AlphaDummy050, nb057AlphaDummy051 f), (nb057AlphaDummy042, nb057AlphaDummy043 f), (nb057AlphaDummy040, nb057AlphaDummy041 f), (nb057AlphaDummy000, a), (nb057AlphaDummy001, f), (nb057AlphaDummy002, nb057AlphaDummy003 f a)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb057AlphaDummy145) (SemanticCore.Class.cv nb057AlphaDummy146)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy144) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb057AlphaDummy145) (SemanticCore.Class.cv nb057AlphaDummy146))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb057AlphaDummy148 f)) (SemanticCore.Class.cv (nb057AlphaDummy149 f))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy147 f)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb057AlphaDummy148 f)) (SemanticCore.Class.cv (nb057AlphaDummy149 f)))).neg)

                          Checked nominal proof certificate identified upstream as nb057_split_alpha_0017.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            source
                            noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057SplitAlpha0018 (f a : SemanticCore.Var) :
                            Nominal.TAlphaWff [(nb057AlphaDummy138, nb057AlphaDummy140 f), (nb057AlphaDummy139, nb057AlphaDummy141 f), (nb057AlphaDummy164, nb057AlphaDummy165 f), (nb057AlphaDummy162, nb057AlphaDummy163 f), (nb057AlphaDummy131, nb057AlphaDummy133 f), (nb057AlphaDummy130, nb057AlphaDummy132 f), (nb057AlphaDummy160, nb057AlphaDummy161 f), (nb057AlphaDummy134, nb057AlphaDummy135 f), (nb057AlphaDummy125, nb057AlphaDummy127 f), (nb057AlphaDummy124, nb057AlphaDummy126 f), (nb057AlphaDummy128, nb057AlphaDummy129 f), (nb057AlphaDummy046, nb057AlphaDummy049 f), (nb057AlphaDummy045, nb057AlphaDummy048 f), (nb057AlphaDummy044, nb057AlphaDummy047 f), (nb057AlphaDummy050, nb057AlphaDummy051 f), (nb057AlphaDummy042, nb057AlphaDummy043 f), (nb057AlphaDummy040, nb057AlphaDummy041 f), (nb057AlphaDummy000, a), (nb057AlphaDummy001, f), (nb057AlphaDummy002, nb057AlphaDummy003 f a)] (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy139) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb057AlphaDummy138) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb057AlphaDummy138) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv nb057AlphaDummy138))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy141 f)) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb057AlphaDummy140 f)) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb057AlphaDummy140 f)) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv (nb057AlphaDummy140 f))))

                            Checked nominal proof certificate identified upstream as nb057_split_alpha_0018.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              source
                              noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057SplitAlpha0019 (f a : SemanticCore.Var) :
                              Nominal.TAlphaWff [(nb057AlphaDummy160, nb057AlphaDummy161 f), (nb057AlphaDummy134, nb057AlphaDummy135 f), (nb057AlphaDummy125, nb057AlphaDummy127 f), (nb057AlphaDummy124, nb057AlphaDummy126 f), (nb057AlphaDummy128, nb057AlphaDummy129 f), (nb057AlphaDummy046, nb057AlphaDummy049 f), (nb057AlphaDummy045, nb057AlphaDummy048 f), (nb057AlphaDummy044, nb057AlphaDummy047 f), (nb057AlphaDummy050, nb057AlphaDummy051 f), (nb057AlphaDummy042, nb057AlphaDummy043 f), (nb057AlphaDummy040, nb057AlphaDummy041 f), (nb057AlphaDummy000, a), (nb057AlphaDummy001, f), (nb057AlphaDummy002, nb057AlphaDummy003 f a)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb057AlphaDummy160) (SemanticCore.Class.cab nb057AlphaDummy130 (Compiler.CompactSourceSyntax.synWrex nb057AlphaDummy131 (SemanticCore.Class.cv nb057AlphaDummy125) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy130) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy131)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb057AlphaDummy160) (SemanticCore.Class.cab nb057AlphaDummy130 (Compiler.CompactSourceSyntax.synWrex nb057AlphaDummy131 (SemanticCore.Class.cv nb057AlphaDummy125) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy130) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy131)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb057AlphaDummy161 f)) (SemanticCore.Class.cab (nb057AlphaDummy132 f) (Compiler.CompactSourceSyntax.synWrex (nb057AlphaDummy133 f) (SemanticCore.Class.cv (nb057AlphaDummy127 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy132 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy133 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb057AlphaDummy161 f)) (SemanticCore.Class.cab (nb057AlphaDummy132 f) (Compiler.CompactSourceSyntax.synWrex (nb057AlphaDummy133 f) (SemanticCore.Class.cv (nb057AlphaDummy127 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy132 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy133 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg)

                              Checked nominal proof certificate identified upstream as nb057_split_alpha_0019.

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

                                Certificates from NAR4C057C001Part014.

                                source
                                noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057SplitAlpha0020 (f a : SemanticCore.Var) :
                                Nominal.TAlphaWff [(nb057AlphaDummy182, nb057AlphaDummy185 f), (nb057AlphaDummy181, nb057AlphaDummy184 f), (nb057AlphaDummy180, nb057AlphaDummy183 f), (nb057AlphaDummy178, nb057AlphaDummy179 f), (nb057AlphaDummy174, nb057AlphaDummy176 f), (nb057AlphaDummy175, nb057AlphaDummy177 f), (nb057AlphaDummy167, nb057AlphaDummy169 f), (nb057AlphaDummy166, nb057AlphaDummy168 f), (nb057AlphaDummy172, nb057AlphaDummy173 f), (nb057AlphaDummy170, nb057AlphaDummy171 f), (nb057AlphaDummy125, nb057AlphaDummy127 f), (nb057AlphaDummy124, nb057AlphaDummy126 f), (nb057AlphaDummy128, nb057AlphaDummy129 f), (nb057AlphaDummy046, nb057AlphaDummy049 f), (nb057AlphaDummy045, nb057AlphaDummy048 f), (nb057AlphaDummy044, nb057AlphaDummy047 f), (nb057AlphaDummy050, nb057AlphaDummy051 f), (nb057AlphaDummy042, nb057AlphaDummy043 f), (nb057AlphaDummy040, nb057AlphaDummy041 f), (nb057AlphaDummy000, a), (nb057AlphaDummy001, f), (nb057AlphaDummy002, nb057AlphaDummy003 f a)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb057AlphaDummy181) (SemanticCore.Class.cv nb057AlphaDummy182)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy180) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb057AlphaDummy181) (SemanticCore.Class.cv nb057AlphaDummy182))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb057AlphaDummy184 f)) (SemanticCore.Class.cv (nb057AlphaDummy185 f))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy183 f)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb057AlphaDummy184 f)) (SemanticCore.Class.cv (nb057AlphaDummy185 f)))).neg)

                                Checked nominal proof certificate identified upstream as nb057_split_alpha_0020.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  source
                                  noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057SplitAlpha0021 (f a : SemanticCore.Var) :
                                  Nominal.TAlphaWff [(nb057AlphaDummy174, nb057AlphaDummy176 f), (nb057AlphaDummy175, nb057AlphaDummy177 f), (nb057AlphaDummy167, nb057AlphaDummy169 f), (nb057AlphaDummy166, nb057AlphaDummy168 f), (nb057AlphaDummy172, nb057AlphaDummy173 f), (nb057AlphaDummy170, nb057AlphaDummy171 f), (nb057AlphaDummy125, nb057AlphaDummy127 f), (nb057AlphaDummy124, nb057AlphaDummy126 f), (nb057AlphaDummy128, nb057AlphaDummy129 f), (nb057AlphaDummy046, nb057AlphaDummy049 f), (nb057AlphaDummy045, nb057AlphaDummy048 f), (nb057AlphaDummy044, nb057AlphaDummy047 f), (nb057AlphaDummy050, nb057AlphaDummy051 f), (nb057AlphaDummy042, nb057AlphaDummy043 f), (nb057AlphaDummy040, nb057AlphaDummy041 f), (nb057AlphaDummy000, a), (nb057AlphaDummy001, f), (nb057AlphaDummy002, nb057AlphaDummy003 f a)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb057AlphaDummy174) (SemanticCore.Class.cv nb057AlphaDummy167)).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy175) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb057AlphaDummy174) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb057AlphaDummy174) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv nb057AlphaDummy174))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb057AlphaDummy176 f)) (SemanticCore.Class.cv (nb057AlphaDummy169 f))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy177 f)) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb057AlphaDummy176 f)) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb057AlphaDummy176 f)) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv (nb057AlphaDummy176 f)))).neg)

                                  Checked nominal proof certificate identified upstream as nb057_split_alpha_0021.

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    source
                                    noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057SplitAlpha0022 (f a : SemanticCore.Var) :
                                    Nominal.TAlphaWff [(nb057AlphaDummy182, nb057AlphaDummy185 f), (nb057AlphaDummy181, nb057AlphaDummy184 f), (nb057AlphaDummy180, nb057AlphaDummy183 f), (nb057AlphaDummy178, nb057AlphaDummy179 f), (nb057AlphaDummy174, nb057AlphaDummy176 f), (nb057AlphaDummy175, nb057AlphaDummy177 f), (nb057AlphaDummy200, nb057AlphaDummy201 f), (nb057AlphaDummy198, nb057AlphaDummy199 f), (nb057AlphaDummy167, nb057AlphaDummy169 f), (nb057AlphaDummy166, nb057AlphaDummy168 f), (nb057AlphaDummy196, nb057AlphaDummy197 f), (nb057AlphaDummy170, nb057AlphaDummy171 f), (nb057AlphaDummy125, nb057AlphaDummy127 f), (nb057AlphaDummy124, nb057AlphaDummy126 f), (nb057AlphaDummy128, nb057AlphaDummy129 f), (nb057AlphaDummy046, nb057AlphaDummy049 f), (nb057AlphaDummy045, nb057AlphaDummy048 f), (nb057AlphaDummy044, nb057AlphaDummy047 f), (nb057AlphaDummy050, nb057AlphaDummy051 f), (nb057AlphaDummy042, nb057AlphaDummy043 f), (nb057AlphaDummy040, nb057AlphaDummy041 f), (nb057AlphaDummy000, a), (nb057AlphaDummy001, f), (nb057AlphaDummy002, nb057AlphaDummy003 f a)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb057AlphaDummy181) (SemanticCore.Class.cv nb057AlphaDummy182)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy180) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb057AlphaDummy181) (SemanticCore.Class.cv nb057AlphaDummy182))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb057AlphaDummy184 f)) (SemanticCore.Class.cv (nb057AlphaDummy185 f))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy183 f)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb057AlphaDummy184 f)) (SemanticCore.Class.cv (nb057AlphaDummy185 f)))).neg)

                                    Checked nominal proof certificate identified upstream as nb057_split_alpha_0022.

                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      source
                                      noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057SplitAlpha0023 (f a : SemanticCore.Var) :
                                      Nominal.TAlphaWff [(nb057AlphaDummy174, nb057AlphaDummy176 f), (nb057AlphaDummy175, nb057AlphaDummy177 f), (nb057AlphaDummy200, nb057AlphaDummy201 f), (nb057AlphaDummy198, nb057AlphaDummy199 f), (nb057AlphaDummy167, nb057AlphaDummy169 f), (nb057AlphaDummy166, nb057AlphaDummy168 f), (nb057AlphaDummy196, nb057AlphaDummy197 f), (nb057AlphaDummy170, nb057AlphaDummy171 f), (nb057AlphaDummy125, nb057AlphaDummy127 f), (nb057AlphaDummy124, nb057AlphaDummy126 f), (nb057AlphaDummy128, nb057AlphaDummy129 f), (nb057AlphaDummy046, nb057AlphaDummy049 f), (nb057AlphaDummy045, nb057AlphaDummy048 f), (nb057AlphaDummy044, nb057AlphaDummy047 f), (nb057AlphaDummy050, nb057AlphaDummy051 f), (nb057AlphaDummy042, nb057AlphaDummy043 f), (nb057AlphaDummy040, nb057AlphaDummy041 f), (nb057AlphaDummy000, a), (nb057AlphaDummy001, f), (nb057AlphaDummy002, nb057AlphaDummy003 f a)] (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy175) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb057AlphaDummy174) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb057AlphaDummy174) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv nb057AlphaDummy174))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy177 f)) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb057AlphaDummy176 f)) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb057AlphaDummy176 f)) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv (nb057AlphaDummy176 f))))

                                      Checked nominal proof certificate identified upstream as nb057_split_alpha_0023.

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

                                        Certificates from NAR4C057C001Part015.

                                        source
                                        noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057SplitAlpha0024 (f a : SemanticCore.Var) :
                                        Nominal.TAlphaWff [(nb057AlphaDummy196, nb057AlphaDummy197 f), (nb057AlphaDummy170, nb057AlphaDummy171 f), (nb057AlphaDummy125, nb057AlphaDummy127 f), (nb057AlphaDummy124, nb057AlphaDummy126 f), (nb057AlphaDummy128, nb057AlphaDummy129 f), (nb057AlphaDummy046, nb057AlphaDummy049 f), (nb057AlphaDummy045, nb057AlphaDummy048 f), (nb057AlphaDummy044, nb057AlphaDummy047 f), (nb057AlphaDummy050, nb057AlphaDummy051 f), (nb057AlphaDummy042, nb057AlphaDummy043 f), (nb057AlphaDummy040, nb057AlphaDummy041 f), (nb057AlphaDummy000, a), (nb057AlphaDummy001, f), (nb057AlphaDummy002, nb057AlphaDummy003 f a)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb057AlphaDummy196) (SemanticCore.Class.cab nb057AlphaDummy166 (Compiler.CompactSourceSyntax.synWrex nb057AlphaDummy167 (SemanticCore.Class.cv nb057AlphaDummy124) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy166) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy167)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb057AlphaDummy196) (SemanticCore.Class.cab nb057AlphaDummy166 (Compiler.CompactSourceSyntax.synWrex nb057AlphaDummy167 (SemanticCore.Class.cv nb057AlphaDummy124) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy166) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy167)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb057AlphaDummy197 f)) (SemanticCore.Class.cab (nb057AlphaDummy168 f) (Compiler.CompactSourceSyntax.synWrex (nb057AlphaDummy169 f) (SemanticCore.Class.cv (nb057AlphaDummy126 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy168 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy169 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb057AlphaDummy197 f)) (SemanticCore.Class.cab (nb057AlphaDummy168 f) (Compiler.CompactSourceSyntax.synWrex (nb057AlphaDummy169 f) (SemanticCore.Class.cv (nb057AlphaDummy126 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy168 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy169 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg)

                                        Checked nominal proof certificate identified upstream as nb057_split_alpha_0024.

                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        Instances For
                                          source
                                          noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057FunctionVariableOccurrence (f a : SemanticCore.Var) (dv_a_f : a ≠ f) :
                                          Nominal.TAlphaClass [(nb057AlphaDummy125, nb057AlphaDummy127 f), (nb057AlphaDummy124, nb057AlphaDummy126 f), (nb057AlphaDummy128, nb057AlphaDummy129 f), (nb057AlphaDummy046, nb057AlphaDummy049 f), (nb057AlphaDummy045, nb057AlphaDummy048 f), (nb057AlphaDummy044, nb057AlphaDummy047 f), (nb057AlphaDummy050, nb057AlphaDummy051 f), (nb057AlphaDummy042, nb057AlphaDummy043 f), (nb057AlphaDummy040, nb057AlphaDummy041 f), (nb057AlphaDummy000, a), (nb057AlphaDummy001, f), (nb057AlphaDummy002, nb057AlphaDummy003 f a)] (SemanticCore.Class.cv nb057AlphaDummy001) (SemanticCore.Class.cv f)

                                          Checked nominal proof certificate identified upstream as nb057_function_variable_occurrence.

                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For
                                            source
                                            noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057SplitAlpha0025 (f a : SemanticCore.Var) (dv_a_f : a ≠ f) :
                                            Nominal.TAlphaWff [(nb057AlphaDummy125, nb057AlphaDummy127 f), (nb057AlphaDummy124, nb057AlphaDummy126 f), (nb057AlphaDummy128, nb057AlphaDummy129 f), (nb057AlphaDummy046, nb057AlphaDummy049 f), (nb057AlphaDummy045, nb057AlphaDummy048 f), (nb057AlphaDummy044, nb057AlphaDummy047 f), (nb057AlphaDummy050, nb057AlphaDummy051 f), (nb057AlphaDummy042, nb057AlphaDummy043 f), (nb057AlphaDummy040, nb057AlphaDummy041 f), (nb057AlphaDummy000, a), (nb057AlphaDummy001, f), (nb057AlphaDummy002, nb057AlphaDummy003 f a)] ((SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy128) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv nb057AlphaDummy124) (SemanticCore.Class.cv nb057AlphaDummy125))).imp (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb057AlphaDummy125) (SemanticCore.Class.cv nb057AlphaDummy001) (SemanticCore.Class.cv nb057AlphaDummy124)).neg) ((SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy129 f)) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv (nb057AlphaDummy126 f)) (SemanticCore.Class.cv (nb057AlphaDummy127 f)))).imp (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb057AlphaDummy127 f)) (SemanticCore.Class.cv f) (SemanticCore.Class.cv (nb057AlphaDummy126 f))).neg)

                                            Checked nominal proof certificate identified upstream as nb057_split_alpha_0025.

                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            Instances For
                                              source
                                              noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057SplitAlpha0026 (f a : SemanticCore.Var) :
                                              Nominal.TAlphaWff [(nb057AlphaDummy218, nb057AlphaDummy221 f), (nb057AlphaDummy217, nb057AlphaDummy220 f), (nb057AlphaDummy216, nb057AlphaDummy219 f), (nb057AlphaDummy214, nb057AlphaDummy215 f), (nb057AlphaDummy210, nb057AlphaDummy212 f), (nb057AlphaDummy211, nb057AlphaDummy213 f), (nb057AlphaDummy203, nb057AlphaDummy205 f), (nb057AlphaDummy202, nb057AlphaDummy204 f), (nb057AlphaDummy208, nb057AlphaDummy209 f), (nb057AlphaDummy206, nb057AlphaDummy207 f), (nb057AlphaDummy046, nb057AlphaDummy049 f), (nb057AlphaDummy045, nb057AlphaDummy048 f), (nb057AlphaDummy044, nb057AlphaDummy047 f), (nb057AlphaDummy050, nb057AlphaDummy051 f), (nb057AlphaDummy042, nb057AlphaDummy043 f), (nb057AlphaDummy040, nb057AlphaDummy041 f), (nb057AlphaDummy000, a), (nb057AlphaDummy001, f), (nb057AlphaDummy002, nb057AlphaDummy003 f a)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb057AlphaDummy217) (SemanticCore.Class.cv nb057AlphaDummy218)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy216) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb057AlphaDummy217) (SemanticCore.Class.cv nb057AlphaDummy218))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb057AlphaDummy220 f)) (SemanticCore.Class.cv (nb057AlphaDummy221 f))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy219 f)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb057AlphaDummy220 f)) (SemanticCore.Class.cv (nb057AlphaDummy221 f)))).neg)

                                              Checked nominal proof certificate identified upstream as nb057_split_alpha_0026.

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

                                                Certificates from NAR4C057C001Part016.

                                                source
                                                noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057SplitAlpha0027 (f a : SemanticCore.Var) :
                                                Nominal.TAlphaWff [(nb057AlphaDummy210, nb057AlphaDummy212 f), (nb057AlphaDummy211, nb057AlphaDummy213 f), (nb057AlphaDummy203, nb057AlphaDummy205 f), (nb057AlphaDummy202, nb057AlphaDummy204 f), (nb057AlphaDummy208, nb057AlphaDummy209 f), (nb057AlphaDummy206, nb057AlphaDummy207 f), (nb057AlphaDummy046, nb057AlphaDummy049 f), (nb057AlphaDummy045, nb057AlphaDummy048 f), (nb057AlphaDummy044, nb057AlphaDummy047 f), (nb057AlphaDummy050, nb057AlphaDummy051 f), (nb057AlphaDummy042, nb057AlphaDummy043 f), (nb057AlphaDummy040, nb057AlphaDummy041 f), (nb057AlphaDummy000, a), (nb057AlphaDummy001, f), (nb057AlphaDummy002, nb057AlphaDummy003 f a)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb057AlphaDummy210) (SemanticCore.Class.cv nb057AlphaDummy203)).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy211) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb057AlphaDummy210) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb057AlphaDummy210) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv nb057AlphaDummy210))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb057AlphaDummy212 f)) (SemanticCore.Class.cv (nb057AlphaDummy205 f))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy213 f)) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb057AlphaDummy212 f)) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb057AlphaDummy212 f)) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv (nb057AlphaDummy212 f)))).neg)

                                                Checked nominal proof certificate identified upstream as nb057_split_alpha_0027.

                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                Instances For
                                                  source
                                                  noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057SplitAlpha0028 (f a : SemanticCore.Var) :
                                                  Nominal.TAlphaWff [(nb057AlphaDummy218, nb057AlphaDummy221 f), (nb057AlphaDummy217, nb057AlphaDummy220 f), (nb057AlphaDummy216, nb057AlphaDummy219 f), (nb057AlphaDummy214, nb057AlphaDummy215 f), (nb057AlphaDummy210, nb057AlphaDummy212 f), (nb057AlphaDummy211, nb057AlphaDummy213 f), (nb057AlphaDummy236, nb057AlphaDummy237 f), (nb057AlphaDummy234, nb057AlphaDummy235 f), (nb057AlphaDummy203, nb057AlphaDummy205 f), (nb057AlphaDummy202, nb057AlphaDummy204 f), (nb057AlphaDummy232, nb057AlphaDummy233 f), (nb057AlphaDummy206, nb057AlphaDummy207 f), (nb057AlphaDummy046, nb057AlphaDummy049 f), (nb057AlphaDummy045, nb057AlphaDummy048 f), (nb057AlphaDummy044, nb057AlphaDummy047 f), (nb057AlphaDummy050, nb057AlphaDummy051 f), (nb057AlphaDummy042, nb057AlphaDummy043 f), (nb057AlphaDummy040, nb057AlphaDummy041 f), (nb057AlphaDummy000, a), (nb057AlphaDummy001, f), (nb057AlphaDummy002, nb057AlphaDummy003 f a)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb057AlphaDummy217) (SemanticCore.Class.cv nb057AlphaDummy218)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy216) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb057AlphaDummy217) (SemanticCore.Class.cv nb057AlphaDummy218))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb057AlphaDummy220 f)) (SemanticCore.Class.cv (nb057AlphaDummy221 f))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy219 f)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb057AlphaDummy220 f)) (SemanticCore.Class.cv (nb057AlphaDummy221 f)))).neg)

                                                  Checked nominal proof certificate identified upstream as nb057_split_alpha_0028.

                                                  Equations
                                                  • One or more equations did not get rendered due to their size.
                                                  Instances For
                                                    source
                                                    noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057SplitAlpha0029 (f a : SemanticCore.Var) :
                                                    Nominal.TAlphaWff [(nb057AlphaDummy210, nb057AlphaDummy212 f), (nb057AlphaDummy211, nb057AlphaDummy213 f), (nb057AlphaDummy236, nb057AlphaDummy237 f), (nb057AlphaDummy234, nb057AlphaDummy235 f), (nb057AlphaDummy203, nb057AlphaDummy205 f), (nb057AlphaDummy202, nb057AlphaDummy204 f), (nb057AlphaDummy232, nb057AlphaDummy233 f), (nb057AlphaDummy206, nb057AlphaDummy207 f), (nb057AlphaDummy046, nb057AlphaDummy049 f), (nb057AlphaDummy045, nb057AlphaDummy048 f), (nb057AlphaDummy044, nb057AlphaDummy047 f), (nb057AlphaDummy050, nb057AlphaDummy051 f), (nb057AlphaDummy042, nb057AlphaDummy043 f), (nb057AlphaDummy040, nb057AlphaDummy041 f), (nb057AlphaDummy000, a), (nb057AlphaDummy001, f), (nb057AlphaDummy002, nb057AlphaDummy003 f a)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb057AlphaDummy210) (SemanticCore.Class.cv nb057AlphaDummy203)).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy211) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb057AlphaDummy210) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb057AlphaDummy210) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv nb057AlphaDummy210))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb057AlphaDummy212 f)) (SemanticCore.Class.cv (nb057AlphaDummy205 f))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy213 f)) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb057AlphaDummy212 f)) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb057AlphaDummy212 f)) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv (nb057AlphaDummy212 f)))).neg)

                                                    Checked nominal proof certificate identified upstream as nb057_split_alpha_0029.

                                                    Equations
                                                    • One or more equations did not get rendered due to their size.
                                                    Instances For
                                                      source
                                                      noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057SplitAlpha0030 (f a : SemanticCore.Var) :
                                                      Nominal.TAlphaWff [(nb057AlphaDummy232, nb057AlphaDummy233 f), (nb057AlphaDummy206, nb057AlphaDummy207 f), (nb057AlphaDummy046, nb057AlphaDummy049 f), (nb057AlphaDummy045, nb057AlphaDummy048 f), (nb057AlphaDummy044, nb057AlphaDummy047 f), (nb057AlphaDummy050, nb057AlphaDummy051 f), (nb057AlphaDummy042, nb057AlphaDummy043 f), (nb057AlphaDummy040, nb057AlphaDummy041 f), (nb057AlphaDummy000, a), (nb057AlphaDummy001, f), (nb057AlphaDummy002, nb057AlphaDummy003 f a)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb057AlphaDummy232) (SemanticCore.Class.cab nb057AlphaDummy202 (Compiler.CompactSourceSyntax.synWrex nb057AlphaDummy203 (SemanticCore.Class.cv nb057AlphaDummy045) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy202) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy203)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb057AlphaDummy232) (SemanticCore.Class.cab nb057AlphaDummy202 (Compiler.CompactSourceSyntax.synWrex nb057AlphaDummy203 (SemanticCore.Class.cv nb057AlphaDummy045) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy202) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy203)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb057AlphaDummy233 f)) (SemanticCore.Class.cab (nb057AlphaDummy204 f) (Compiler.CompactSourceSyntax.synWrex (nb057AlphaDummy205 f) (SemanticCore.Class.cv (nb057AlphaDummy048 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy204 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy205 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb057AlphaDummy233 f)) (SemanticCore.Class.cab (nb057AlphaDummy204 f) (Compiler.CompactSourceSyntax.synWrex (nb057AlphaDummy205 f) (SemanticCore.Class.cv (nb057AlphaDummy048 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy204 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy205 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg)

                                                      Checked nominal proof certificate identified upstream as nb057_split_alpha_0030.

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