Documentation

LeanPool.NFWeakPartition.Certificates.NAR4C057C001Block005

Nominal proof certificates grouped in dependency order.

Certificates from NAR4C057C001Part017.

source
noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057WppRefl0042 (f a : SemanticCore.Var) :
Nominal.TReflOn [(nb057AlphaDummy042, nb057AlphaDummy043 f), (nb057AlphaDummy040, nb057AlphaDummy041 f), (nb057AlphaDummy000, a), (nb057AlphaDummy001, f), (nb057AlphaDummy002, nb057AlphaDummy003 f a)] Compiler.CompactSourceSyntax.synCid.fv

Checked nominal proof certificate identified upstream as nb057_wpp_refl_0042.

Equations
Instances For
    source
    noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057FunctionBinderOccurrence (f a : SemanticCore.Var) :
    Nominal.TAlphaClass [(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 nb057AlphaDummy050) (SemanticCore.Class.cv (nb057AlphaDummy051 f))

    Checked nominal proof certificate identified upstream as nb057_function_binder_occurrence.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057SplitAlpha0032 (f a : SemanticCore.Var) (dv_a_f : a ≠ f) :
      Nominal.TAlphaWff [(nb057AlphaDummy040, nb057AlphaDummy041 f), (nb057AlphaDummy000, a), (nb057AlphaDummy001, f), (nb057AlphaDummy002, nb057AlphaDummy003 f a)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb057AlphaDummy040) (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCcom (SemanticCore.Class.cv nb057AlphaDummy001) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb057AlphaDummy001))) Compiler.CompactSourceSyntax.synCid)).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb057AlphaDummy040) (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCcom (SemanticCore.Class.cv nb057AlphaDummy001) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb057AlphaDummy001))) Compiler.CompactSourceSyntax.synCid)).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb057AlphaDummy041 f)) (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCcom (SemanticCore.Class.cv f) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))) Compiler.CompactSourceSyntax.synCid)).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb057AlphaDummy041 f)) (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCcom (SemanticCore.Class.cv f) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))) Compiler.CompactSourceSyntax.synCid)).neg)

      Checked nominal proof certificate identified upstream as nb057_split_alpha_0032.

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

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

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

            Certificates from NAR4C057C001Part018.

            source
            noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057SplitAlpha0035 (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), (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_0035.

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

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057SplitAlpha0037 (f a : SemanticCore.Var) :
                Nominal.TAlphaWff [(nb057AlphaDummy082, nb057AlphaDummy083 f), (nb057AlphaDummy056, nb057AlphaDummy057 f), (nb057AlphaDummy045, nb057AlphaDummy048 f), (nb057AlphaDummy044, nb057AlphaDummy047 f), (nb057AlphaDummy050, nb057AlphaDummy051 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_0037.

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

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057SplitAlpha0039 (f a : SemanticCore.Var) :
                    Nominal.TAlphaWff [(nb057AlphaDummy089, nb057AlphaDummy091 f), (nb057AlphaDummy088, nb057AlphaDummy090 f), (nb057AlphaDummy094, nb057AlphaDummy095 f), (nb057AlphaDummy092, nb057AlphaDummy093 f), (nb057AlphaDummy046, nb057AlphaDummy049 f), (nb057AlphaDummy045, nb057AlphaDummy048 f), (nb057AlphaDummy044, nb057AlphaDummy047 f), (nb057AlphaDummy050, nb057AlphaDummy051 f), (nb057AlphaDummy000, a), (nb057AlphaDummy001, f), (nb057AlphaDummy002, nb057AlphaDummy003 f a)] (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy088) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy089))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy090 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy091 f))))

                    Checked nominal proof certificate identified upstream as nb057_split_alpha_0039.

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

                      Certificates from NAR4C057C001Part019.

                      source
                      noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057SplitAlpha0040 (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), (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_0040.

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

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          source
                          noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057SplitAlpha0042 (f a : SemanticCore.Var) :
                          Nominal.TAlphaWff [(nb057AlphaDummy118, nb057AlphaDummy119 f), (nb057AlphaDummy092, nb057AlphaDummy093 f), (nb057AlphaDummy046, nb057AlphaDummy049 f), (nb057AlphaDummy045, nb057AlphaDummy048 f), (nb057AlphaDummy044, nb057AlphaDummy047 f), (nb057AlphaDummy050, nb057AlphaDummy051 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_0042.

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

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

                              Certificates from NAR4C057C001Part020.

                              source
                              noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057SplitAlpha0044 (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), (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_0044.

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

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

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

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

                                      Certificates from NAR4C057C001Part021.

                                      source
                                      noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057SplitAlpha0048 (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), (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_0048.

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

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

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

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

                                              Certificates from NAR4C057C001Part022.

                                              source
                                              noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057SplitAlpha0052 (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), (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_0052.

                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              Instances For
                                                source
                                                noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057DirectFunctionVariableOccurrence (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), (nb057AlphaDummy000, a), (nb057AlphaDummy001, f), (nb057AlphaDummy002, nb057AlphaDummy003 f a)] (SemanticCore.Class.cv nb057AlphaDummy001) (SemanticCore.Class.cv f)

                                                Checked nominal proof certificate identified upstream as nb057_direct_function_variable_occurrence.

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

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

                                                    Equations
                                                    • One or more equations did not get rendered due to their size.
                                                    Instances For
                                                      source
                                                      noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057SplitAlpha0055 (f a : SemanticCore.Var) :
                                                      Nominal.TAlphaWff [(nb057AlphaDummy203, nb057AlphaDummy205 f), (nb057AlphaDummy202, nb057AlphaDummy204 f), (nb057AlphaDummy208, nb057AlphaDummy209 f), (nb057AlphaDummy206, nb057AlphaDummy207 f), (nb057AlphaDummy046, nb057AlphaDummy049 f), (nb057AlphaDummy045, nb057AlphaDummy048 f), (nb057AlphaDummy044, nb057AlphaDummy047 f), (nb057AlphaDummy050, nb057AlphaDummy051 f), (nb057AlphaDummy000, a), (nb057AlphaDummy001, f), (nb057AlphaDummy002, nb057AlphaDummy003 f a)] (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy202) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy203))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy204 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy205 f))))

                                                      Checked nominal proof certificate identified upstream as nb057_split_alpha_0055.

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

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

                                                          Certificates from NAR4C057C001Part023.

                                                          source
                                                          noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057SplitAlpha0057 (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), (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_0057.

                                                          Equations
                                                          • One or more equations did not get rendered due to their size.
                                                          Instances For
                                                            source
                                                            noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057SplitAlpha0058 (f a : SemanticCore.Var) :
                                                            Nominal.TAlphaWff [(nb057AlphaDummy232, nb057AlphaDummy233 f), (nb057AlphaDummy206, nb057AlphaDummy207 f), (nb057AlphaDummy046, nb057AlphaDummy049 f), (nb057AlphaDummy045, nb057AlphaDummy048 f), (nb057AlphaDummy044, nb057AlphaDummy047 f), (nb057AlphaDummy050, nb057AlphaDummy051 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_0058.

                                                            Equations
                                                            • One or more equations did not get rendered due to their size.
                                                            Instances For
                                                              source
                                                              noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057DirectCompositionVariableOccurrence (f a : SemanticCore.Var) (dv_a_f : a ≠ f) :
                                                              Nominal.TAlphaClass [(nb057AlphaDummy046, nb057AlphaDummy049 f), (nb057AlphaDummy045, nb057AlphaDummy048 f), (nb057AlphaDummy044, nb057AlphaDummy047 f), (nb057AlphaDummy050, nb057AlphaDummy051 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_direct_composition_variable_occurrence.

                                                              Equations
                                                              • One or more equations did not get rendered due to their size.
                                                              Instances For
                                                                source
                                                                noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057SplitAlpha0059 (f a : SemanticCore.Var) (dv_a_f : a ≠ f) :
                                                                Nominal.TAlphaWff [(nb057AlphaDummy046, nb057AlphaDummy049 f), (nb057AlphaDummy045, nb057AlphaDummy048 f), (nb057AlphaDummy044, nb057AlphaDummy047 f), (nb057AlphaDummy050, nb057AlphaDummy051 f), (nb057AlphaDummy000, a), (nb057AlphaDummy001, f), (nb057AlphaDummy002, nb057AlphaDummy003 f a)] ((Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb057AlphaDummy044) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb057AlphaDummy001)) (SemanticCore.Class.cv nb057AlphaDummy046)).imp (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb057AlphaDummy046) (SemanticCore.Class.cv nb057AlphaDummy001) (SemanticCore.Class.cv nb057AlphaDummy045)).neg) ((Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb057AlphaDummy047 f)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)) (SemanticCore.Class.cv (nb057AlphaDummy049 f))).imp (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb057AlphaDummy049 f)) (SemanticCore.Class.cv f) (SemanticCore.Class.cv (nb057AlphaDummy048 f))).neg)

                                                                Checked nominal proof certificate identified upstream as nb057_split_alpha_0059.

                                                                Equations
                                                                • One or more equations did not get rendered due to their size.
                                                                Instances For
                                                                  source
                                                                  noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057SplitAlpha0060 (f a : SemanticCore.Var) :
                                                                  Nominal.TAlphaWff [(nb057AlphaDummy258, nb057AlphaDummy261 f), (nb057AlphaDummy257, nb057AlphaDummy260 f), (nb057AlphaDummy256, nb057AlphaDummy259 f), (nb057AlphaDummy254, nb057AlphaDummy255 f), (nb057AlphaDummy250, nb057AlphaDummy252 f), (nb057AlphaDummy251, nb057AlphaDummy253 f), (nb057AlphaDummy243, nb057AlphaDummy245 f), (nb057AlphaDummy242, nb057AlphaDummy244 f), (nb057AlphaDummy248, nb057AlphaDummy249 f), (nb057AlphaDummy246, nb057AlphaDummy247 f), (nb057AlphaDummy239, nb057AlphaDummy241 f), (nb057AlphaDummy238, nb057AlphaDummy240 f), (nb057AlphaDummy000, a), (nb057AlphaDummy001, f), (nb057AlphaDummy002, nb057AlphaDummy003 f a)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb057AlphaDummy257) (SemanticCore.Class.cv nb057AlphaDummy258)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy256) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb057AlphaDummy257) (SemanticCore.Class.cv nb057AlphaDummy258))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb057AlphaDummy260 f)) (SemanticCore.Class.cv (nb057AlphaDummy261 f))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy259 f)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb057AlphaDummy260 f)) (SemanticCore.Class.cv (nb057AlphaDummy261 f)))).neg)

                                                                  Checked nominal proof certificate identified upstream as nb057_split_alpha_0060.

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

                                                                    Certificates from NAR4C057C001Part024.

                                                                    source
                                                                    noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057SplitAlpha0061 (f a : SemanticCore.Var) :
                                                                    Nominal.TAlphaWff [(nb057AlphaDummy243, nb057AlphaDummy245 f), (nb057AlphaDummy242, nb057AlphaDummy244 f), (nb057AlphaDummy248, nb057AlphaDummy249 f), (nb057AlphaDummy246, nb057AlphaDummy247 f), (nb057AlphaDummy239, nb057AlphaDummy241 f), (nb057AlphaDummy238, nb057AlphaDummy240 f), (nb057AlphaDummy000, a), (nb057AlphaDummy001, f), (nb057AlphaDummy002, nb057AlphaDummy003 f a)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb057AlphaDummy243) (SemanticCore.Class.cv nb057AlphaDummy239)).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy242) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy243))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb057AlphaDummy245 f)) (SemanticCore.Class.cv (nb057AlphaDummy241 f))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy244 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy245 f)))).neg)

                                                                    Checked nominal proof certificate identified upstream as nb057_split_alpha_0061.

                                                                    Equations
                                                                    • One or more equations did not get rendered due to their size.
                                                                    Instances For
                                                                      source
                                                                      noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057SplitAlpha0062 (f a : SemanticCore.Var) :
                                                                      Nominal.TAlphaWff [(nb057AlphaDummy258, nb057AlphaDummy261 f), (nb057AlphaDummy257, nb057AlphaDummy260 f), (nb057AlphaDummy256, nb057AlphaDummy259 f), (nb057AlphaDummy254, nb057AlphaDummy255 f), (nb057AlphaDummy250, nb057AlphaDummy252 f), (nb057AlphaDummy251, nb057AlphaDummy253 f), (nb057AlphaDummy276, nb057AlphaDummy277 f), (nb057AlphaDummy274, nb057AlphaDummy275 f), (nb057AlphaDummy243, nb057AlphaDummy245 f), (nb057AlphaDummy242, nb057AlphaDummy244 f), (nb057AlphaDummy272, nb057AlphaDummy273 f), (nb057AlphaDummy246, nb057AlphaDummy247 f), (nb057AlphaDummy239, nb057AlphaDummy241 f), (nb057AlphaDummy238, nb057AlphaDummy240 f), (nb057AlphaDummy000, a), (nb057AlphaDummy001, f), (nb057AlphaDummy002, nb057AlphaDummy003 f a)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb057AlphaDummy257) (SemanticCore.Class.cv nb057AlphaDummy258)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy256) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb057AlphaDummy257) (SemanticCore.Class.cv nb057AlphaDummy258))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb057AlphaDummy260 f)) (SemanticCore.Class.cv (nb057AlphaDummy261 f))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy259 f)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb057AlphaDummy260 f)) (SemanticCore.Class.cv (nb057AlphaDummy261 f)))).neg)

                                                                      Checked nominal proof certificate identified upstream as nb057_split_alpha_0062.

                                                                      Equations
                                                                      • One or more equations did not get rendered due to their size.
                                                                      Instances For
                                                                        source
                                                                        noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057SplitAlpha0063 (f a : SemanticCore.Var) :
                                                                        Nominal.TAlphaWff [(nb057AlphaDummy250, nb057AlphaDummy252 f), (nb057AlphaDummy251, nb057AlphaDummy253 f), (nb057AlphaDummy276, nb057AlphaDummy277 f), (nb057AlphaDummy274, nb057AlphaDummy275 f), (nb057AlphaDummy243, nb057AlphaDummy245 f), (nb057AlphaDummy242, nb057AlphaDummy244 f), (nb057AlphaDummy272, nb057AlphaDummy273 f), (nb057AlphaDummy246, nb057AlphaDummy247 f), (nb057AlphaDummy239, nb057AlphaDummy241 f), (nb057AlphaDummy238, nb057AlphaDummy240 f), (nb057AlphaDummy000, a), (nb057AlphaDummy001, f), (nb057AlphaDummy002, nb057AlphaDummy003 f a)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb057AlphaDummy250) (SemanticCore.Class.cv nb057AlphaDummy243)).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy251) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb057AlphaDummy250) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb057AlphaDummy250) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv nb057AlphaDummy250))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb057AlphaDummy252 f)) (SemanticCore.Class.cv (nb057AlphaDummy245 f))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy253 f)) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb057AlphaDummy252 f)) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb057AlphaDummy252 f)) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv (nb057AlphaDummy252 f)))).neg)

                                                                        Checked nominal proof certificate identified upstream as nb057_split_alpha_0063.

                                                                        Equations
                                                                        • One or more equations did not get rendered due to their size.
                                                                        Instances For
                                                                          source
                                                                          noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057SplitAlpha0064 (f a : SemanticCore.Var) :
                                                                          Nominal.TAlphaWff [(nb057AlphaDummy272, nb057AlphaDummy273 f), (nb057AlphaDummy246, nb057AlphaDummy247 f), (nb057AlphaDummy239, nb057AlphaDummy241 f), (nb057AlphaDummy238, nb057AlphaDummy240 f), (nb057AlphaDummy000, a), (nb057AlphaDummy001, f), (nb057AlphaDummy002, nb057AlphaDummy003 f a)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb057AlphaDummy272) (SemanticCore.Class.cab nb057AlphaDummy242 (Compiler.CompactSourceSyntax.synWrex nb057AlphaDummy243 (SemanticCore.Class.cv nb057AlphaDummy238) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy242) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy243)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb057AlphaDummy272) (SemanticCore.Class.cab nb057AlphaDummy242 (Compiler.CompactSourceSyntax.synWrex nb057AlphaDummy243 (SemanticCore.Class.cv nb057AlphaDummy238) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy242) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy243)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb057AlphaDummy273 f)) (SemanticCore.Class.cab (nb057AlphaDummy244 f) (Compiler.CompactSourceSyntax.synWrex (nb057AlphaDummy245 f) (SemanticCore.Class.cv (nb057AlphaDummy240 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy244 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy245 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb057AlphaDummy273 f)) (SemanticCore.Class.cab (nb057AlphaDummy244 f) (Compiler.CompactSourceSyntax.synWrex (nb057AlphaDummy245 f) (SemanticCore.Class.cv (nb057AlphaDummy240 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy244 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy245 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg)

                                                                          Checked nominal proof certificate identified upstream as nb057_split_alpha_0064.

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