Documentation

LeanPool.NFWeakPartition.Certificates.NAR4C068C001Block015

Nominal proof certificates grouped in dependency order.

Certificates from NAR4C068C001Part059.

source
noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0175 (x y f : SemanticCore.Var) :
Nominal.TAlphaWff [(nb068AlphaDummy501, nb068AlphaDummy504 f), (nb068AlphaDummy500, nb068AlphaDummy503 f), (nb068AlphaDummy499, nb068AlphaDummy502 f), (nb068AlphaDummy497, nb068AlphaDummy498 f), (nb068AlphaDummy493, nb068AlphaDummy495 f), (nb068AlphaDummy494, nb068AlphaDummy496 f), (nb068AlphaDummy486, nb068AlphaDummy488 f), (nb068AlphaDummy485, nb068AlphaDummy487 f), (nb068AlphaDummy491, nb068AlphaDummy492 f), (nb068AlphaDummy489, nb068AlphaDummy490 f), (nb068AlphaDummy329, nb068AlphaDummy332 f), (nb068AlphaDummy328, nb068AlphaDummy331 f), (nb068AlphaDummy327, nb068AlphaDummy330 f), (nb068AlphaDummy333, nb068AlphaDummy334 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb068AlphaDummy500) (SemanticCore.Class.cv nb068AlphaDummy501)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy499) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb068AlphaDummy500) (SemanticCore.Class.cv nb068AlphaDummy501))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb068AlphaDummy503 f)) (SemanticCore.Class.cv (nb068AlphaDummy504 f))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy502 f)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb068AlphaDummy503 f)) (SemanticCore.Class.cv (nb068AlphaDummy504 f)))).neg)

Checked nominal proof certificate identified upstream as nb068_split_alpha_0175.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0176 (x y f : SemanticCore.Var) :
    Nominal.TAlphaWff [(nb068AlphaDummy486, nb068AlphaDummy488 f), (nb068AlphaDummy485, nb068AlphaDummy487 f), (nb068AlphaDummy491, nb068AlphaDummy492 f), (nb068AlphaDummy489, nb068AlphaDummy490 f), (nb068AlphaDummy329, nb068AlphaDummy332 f), (nb068AlphaDummy328, nb068AlphaDummy331 f), (nb068AlphaDummy327, nb068AlphaDummy330 f), (nb068AlphaDummy333, nb068AlphaDummy334 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy485) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy486))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy487 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy488 f))))

    Checked nominal proof certificate identified upstream as nb068_split_alpha_0176.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0177 (x y f : SemanticCore.Var) :
      Nominal.TAlphaWff [(nb068AlphaDummy501, nb068AlphaDummy504 f), (nb068AlphaDummy500, nb068AlphaDummy503 f), (nb068AlphaDummy499, nb068AlphaDummy502 f), (nb068AlphaDummy497, nb068AlphaDummy498 f), (nb068AlphaDummy493, nb068AlphaDummy495 f), (nb068AlphaDummy494, nb068AlphaDummy496 f), (nb068AlphaDummy519, nb068AlphaDummy520 f), (nb068AlphaDummy517, nb068AlphaDummy518 f), (nb068AlphaDummy486, nb068AlphaDummy488 f), (nb068AlphaDummy485, nb068AlphaDummy487 f), (nb068AlphaDummy515, nb068AlphaDummy516 f), (nb068AlphaDummy489, nb068AlphaDummy490 f), (nb068AlphaDummy329, nb068AlphaDummy332 f), (nb068AlphaDummy328, nb068AlphaDummy331 f), (nb068AlphaDummy327, nb068AlphaDummy330 f), (nb068AlphaDummy333, nb068AlphaDummy334 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb068AlphaDummy500) (SemanticCore.Class.cv nb068AlphaDummy501)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy499) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb068AlphaDummy500) (SemanticCore.Class.cv nb068AlphaDummy501))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb068AlphaDummy503 f)) (SemanticCore.Class.cv (nb068AlphaDummy504 f))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy502 f)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb068AlphaDummy503 f)) (SemanticCore.Class.cv (nb068AlphaDummy504 f)))).neg)

      Checked nominal proof certificate identified upstream as nb068_split_alpha_0177.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0178 (x y f : SemanticCore.Var) :
        Nominal.TAlphaWff [(nb068AlphaDummy493, nb068AlphaDummy495 f), (nb068AlphaDummy494, nb068AlphaDummy496 f), (nb068AlphaDummy519, nb068AlphaDummy520 f), (nb068AlphaDummy517, nb068AlphaDummy518 f), (nb068AlphaDummy486, nb068AlphaDummy488 f), (nb068AlphaDummy485, nb068AlphaDummy487 f), (nb068AlphaDummy515, nb068AlphaDummy516 f), (nb068AlphaDummy489, nb068AlphaDummy490 f), (nb068AlphaDummy329, nb068AlphaDummy332 f), (nb068AlphaDummy328, nb068AlphaDummy331 f), (nb068AlphaDummy327, nb068AlphaDummy330 f), (nb068AlphaDummy333, nb068AlphaDummy334 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy493) (SemanticCore.Class.cv nb068AlphaDummy486)).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy494) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy493) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb068AlphaDummy493) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv nb068AlphaDummy493))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy495 f)) (SemanticCore.Class.cv (nb068AlphaDummy488 f))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy496 f)) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy495 f)) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb068AlphaDummy495 f)) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv (nb068AlphaDummy495 f)))).neg)

        Checked nominal proof certificate identified upstream as nb068_split_alpha_0178.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0179 (x y f : SemanticCore.Var) :
          Nominal.TAlphaWff [(nb068AlphaDummy515, nb068AlphaDummy516 f), (nb068AlphaDummy489, nb068AlphaDummy490 f), (nb068AlphaDummy329, nb068AlphaDummy332 f), (nb068AlphaDummy328, nb068AlphaDummy331 f), (nb068AlphaDummy327, nb068AlphaDummy330 f), (nb068AlphaDummy333, nb068AlphaDummy334 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy515) (SemanticCore.Class.cab nb068AlphaDummy485 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy486 (SemanticCore.Class.cv nb068AlphaDummy328) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy485) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy486)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy515) (SemanticCore.Class.cab nb068AlphaDummy485 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy486 (SemanticCore.Class.cv nb068AlphaDummy328) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy485) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy486)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy516 f)) (SemanticCore.Class.cab (nb068AlphaDummy487 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy488 f) (SemanticCore.Class.cv (nb068AlphaDummy331 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy487 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy488 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy516 f)) (SemanticCore.Class.cab (nb068AlphaDummy487 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy488 f) (SemanticCore.Class.cv (nb068AlphaDummy331 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy487 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy488 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg)

          Checked nominal proof certificate identified upstream as nb068_split_alpha_0179.

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

            Certificates from NAR4C068C001Part060.

            source
            noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0180 (x y f : SemanticCore.Var) :
            Nominal.TAlphaWff [(nb068AlphaDummy147, nb068AlphaDummy150 f), (nb068AlphaDummy146, nb068AlphaDummy149 f), (nb068AlphaDummy145, nb068AlphaDummy148 f), (nb068AlphaDummy143, nb068AlphaDummy144 f), (nb068AlphaDummy139, nb068AlphaDummy141 f), (nb068AlphaDummy140, nb068AlphaDummy142 f), (nb068AlphaDummy132, nb068AlphaDummy134 f), (nb068AlphaDummy131, nb068AlphaDummy133 f), (nb068AlphaDummy137, nb068AlphaDummy138 f), (nb068AlphaDummy135, nb068AlphaDummy136 f), (nb068AlphaDummy126, nb068AlphaDummy128 f), (nb068AlphaDummy125, nb068AlphaDummy127 f), (nb068AlphaDummy129, nb068AlphaDummy130 f), (nb068AlphaDummy329, nb068AlphaDummy332 f), (nb068AlphaDummy328, nb068AlphaDummy331 f), (nb068AlphaDummy327, nb068AlphaDummy330 f), (nb068AlphaDummy333, nb068AlphaDummy334 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb068AlphaDummy146) (SemanticCore.Class.cv nb068AlphaDummy147)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy145) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb068AlphaDummy146) (SemanticCore.Class.cv nb068AlphaDummy147))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb068AlphaDummy149 f)) (SemanticCore.Class.cv (nb068AlphaDummy150 f))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy148 f)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb068AlphaDummy149 f)) (SemanticCore.Class.cv (nb068AlphaDummy150 f)))).neg)

            Checked nominal proof certificate identified upstream as nb068_split_alpha_0180.

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

              Checked nominal proof certificate identified upstream as nb068_split_alpha_0181.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0182 (x y f : SemanticCore.Var) :
                Nominal.TAlphaWff [(nb068AlphaDummy147, nb068AlphaDummy150 f), (nb068AlphaDummy146, nb068AlphaDummy149 f), (nb068AlphaDummy145, nb068AlphaDummy148 f), (nb068AlphaDummy143, nb068AlphaDummy144 f), (nb068AlphaDummy139, nb068AlphaDummy141 f), (nb068AlphaDummy140, nb068AlphaDummy142 f), (nb068AlphaDummy165, nb068AlphaDummy166 f), (nb068AlphaDummy163, nb068AlphaDummy164 f), (nb068AlphaDummy132, nb068AlphaDummy134 f), (nb068AlphaDummy131, nb068AlphaDummy133 f), (nb068AlphaDummy161, nb068AlphaDummy162 f), (nb068AlphaDummy135, nb068AlphaDummy136 f), (nb068AlphaDummy126, nb068AlphaDummy128 f), (nb068AlphaDummy125, nb068AlphaDummy127 f), (nb068AlphaDummy129, nb068AlphaDummy130 f), (nb068AlphaDummy329, nb068AlphaDummy332 f), (nb068AlphaDummy328, nb068AlphaDummy331 f), (nb068AlphaDummy327, nb068AlphaDummy330 f), (nb068AlphaDummy333, nb068AlphaDummy334 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb068AlphaDummy146) (SemanticCore.Class.cv nb068AlphaDummy147)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy145) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb068AlphaDummy146) (SemanticCore.Class.cv nb068AlphaDummy147))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb068AlphaDummy149 f)) (SemanticCore.Class.cv (nb068AlphaDummy150 f))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy148 f)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb068AlphaDummy149 f)) (SemanticCore.Class.cv (nb068AlphaDummy150 f)))).neg)

                Checked nominal proof certificate identified upstream as nb068_split_alpha_0182.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0183 (x y f : SemanticCore.Var) :
                  Nominal.TAlphaWff [(nb068AlphaDummy139, nb068AlphaDummy141 f), (nb068AlphaDummy140, nb068AlphaDummy142 f), (nb068AlphaDummy165, nb068AlphaDummy166 f), (nb068AlphaDummy163, nb068AlphaDummy164 f), (nb068AlphaDummy132, nb068AlphaDummy134 f), (nb068AlphaDummy131, nb068AlphaDummy133 f), (nb068AlphaDummy161, nb068AlphaDummy162 f), (nb068AlphaDummy135, nb068AlphaDummy136 f), (nb068AlphaDummy126, nb068AlphaDummy128 f), (nb068AlphaDummy125, nb068AlphaDummy127 f), (nb068AlphaDummy129, nb068AlphaDummy130 f), (nb068AlphaDummy329, nb068AlphaDummy332 f), (nb068AlphaDummy328, nb068AlphaDummy331 f), (nb068AlphaDummy327, nb068AlphaDummy330 f), (nb068AlphaDummy333, nb068AlphaDummy334 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy140) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy139) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb068AlphaDummy139) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv nb068AlphaDummy139))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy142 f)) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy141 f)) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb068AlphaDummy141 f)) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv (nb068AlphaDummy141 f))))

                  Checked nominal proof certificate identified upstream as nb068_split_alpha_0183.

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

                    Certificates from NAR4C068C001Part061.

                    source
                    noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0184 (x y f : SemanticCore.Var) :
                    Nominal.TAlphaWff [(nb068AlphaDummy161, nb068AlphaDummy162 f), (nb068AlphaDummy135, nb068AlphaDummy136 f), (nb068AlphaDummy126, nb068AlphaDummy128 f), (nb068AlphaDummy125, nb068AlphaDummy127 f), (nb068AlphaDummy129, nb068AlphaDummy130 f), (nb068AlphaDummy329, nb068AlphaDummy332 f), (nb068AlphaDummy328, nb068AlphaDummy331 f), (nb068AlphaDummy327, nb068AlphaDummy330 f), (nb068AlphaDummy333, nb068AlphaDummy334 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy161) (SemanticCore.Class.cab nb068AlphaDummy131 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy132 (SemanticCore.Class.cv nb068AlphaDummy126) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy131) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy132)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy161) (SemanticCore.Class.cab nb068AlphaDummy131 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy132 (SemanticCore.Class.cv nb068AlphaDummy126) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy131) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy132)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy162 f)) (SemanticCore.Class.cab (nb068AlphaDummy133 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy134 f) (SemanticCore.Class.cv (nb068AlphaDummy128 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy133 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy134 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy162 f)) (SemanticCore.Class.cab (nb068AlphaDummy133 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy134 f) (SemanticCore.Class.cv (nb068AlphaDummy128 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy133 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy134 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg)

                    Checked nominal proof certificate identified upstream as nb068_split_alpha_0184.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      source
                      noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0185 (x y f : SemanticCore.Var) :
                      Nominal.TAlphaWff [(nb068AlphaDummy183, nb068AlphaDummy186 f), (nb068AlphaDummy182, nb068AlphaDummy185 f), (nb068AlphaDummy181, nb068AlphaDummy184 f), (nb068AlphaDummy179, nb068AlphaDummy180 f), (nb068AlphaDummy175, nb068AlphaDummy177 f), (nb068AlphaDummy176, nb068AlphaDummy178 f), (nb068AlphaDummy168, nb068AlphaDummy170 f), (nb068AlphaDummy167, nb068AlphaDummy169 f), (nb068AlphaDummy173, nb068AlphaDummy174 f), (nb068AlphaDummy171, nb068AlphaDummy172 f), (nb068AlphaDummy126, nb068AlphaDummy128 f), (nb068AlphaDummy125, nb068AlphaDummy127 f), (nb068AlphaDummy129, nb068AlphaDummy130 f), (nb068AlphaDummy329, nb068AlphaDummy332 f), (nb068AlphaDummy328, nb068AlphaDummy331 f), (nb068AlphaDummy327, nb068AlphaDummy330 f), (nb068AlphaDummy333, nb068AlphaDummy334 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb068AlphaDummy182) (SemanticCore.Class.cv nb068AlphaDummy183)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy181) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb068AlphaDummy182) (SemanticCore.Class.cv nb068AlphaDummy183))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb068AlphaDummy185 f)) (SemanticCore.Class.cv (nb068AlphaDummy186 f))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy184 f)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb068AlphaDummy185 f)) (SemanticCore.Class.cv (nb068AlphaDummy186 f)))).neg)

                      Checked nominal proof certificate identified upstream as nb068_split_alpha_0185.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        source
                        noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0186 (x y f : SemanticCore.Var) :
                        Nominal.TAlphaWff [(nb068AlphaDummy175, nb068AlphaDummy177 f), (nb068AlphaDummy176, nb068AlphaDummy178 f), (nb068AlphaDummy168, nb068AlphaDummy170 f), (nb068AlphaDummy167, nb068AlphaDummy169 f), (nb068AlphaDummy173, nb068AlphaDummy174 f), (nb068AlphaDummy171, nb068AlphaDummy172 f), (nb068AlphaDummy126, nb068AlphaDummy128 f), (nb068AlphaDummy125, nb068AlphaDummy127 f), (nb068AlphaDummy129, nb068AlphaDummy130 f), (nb068AlphaDummy329, nb068AlphaDummy332 f), (nb068AlphaDummy328, nb068AlphaDummy331 f), (nb068AlphaDummy327, nb068AlphaDummy330 f), (nb068AlphaDummy333, nb068AlphaDummy334 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy175) (SemanticCore.Class.cv nb068AlphaDummy168)).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy176) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy175) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb068AlphaDummy175) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv nb068AlphaDummy175))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy177 f)) (SemanticCore.Class.cv (nb068AlphaDummy170 f))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy178 f)) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy177 f)) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb068AlphaDummy177 f)) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv (nb068AlphaDummy177 f)))).neg)

                        Checked nominal proof certificate identified upstream as nb068_split_alpha_0186.

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

                          Certificates from NAR4C068C001Part062.

                          source
                          noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0187 (x y f : SemanticCore.Var) :
                          Nominal.TAlphaWff [(nb068AlphaDummy183, nb068AlphaDummy186 f), (nb068AlphaDummy182, nb068AlphaDummy185 f), (nb068AlphaDummy181, nb068AlphaDummy184 f), (nb068AlphaDummy179, nb068AlphaDummy180 f), (nb068AlphaDummy175, nb068AlphaDummy177 f), (nb068AlphaDummy176, nb068AlphaDummy178 f), (nb068AlphaDummy201, nb068AlphaDummy202 f), (nb068AlphaDummy199, nb068AlphaDummy200 f), (nb068AlphaDummy168, nb068AlphaDummy170 f), (nb068AlphaDummy167, nb068AlphaDummy169 f), (nb068AlphaDummy197, nb068AlphaDummy198 f), (nb068AlphaDummy171, nb068AlphaDummy172 f), (nb068AlphaDummy126, nb068AlphaDummy128 f), (nb068AlphaDummy125, nb068AlphaDummy127 f), (nb068AlphaDummy129, nb068AlphaDummy130 f), (nb068AlphaDummy329, nb068AlphaDummy332 f), (nb068AlphaDummy328, nb068AlphaDummy331 f), (nb068AlphaDummy327, nb068AlphaDummy330 f), (nb068AlphaDummy333, nb068AlphaDummy334 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb068AlphaDummy182) (SemanticCore.Class.cv nb068AlphaDummy183)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy181) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb068AlphaDummy182) (SemanticCore.Class.cv nb068AlphaDummy183))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb068AlphaDummy185 f)) (SemanticCore.Class.cv (nb068AlphaDummy186 f))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy184 f)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb068AlphaDummy185 f)) (SemanticCore.Class.cv (nb068AlphaDummy186 f)))).neg)

                          Checked nominal proof certificate identified upstream as nb068_split_alpha_0187.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            source
                            noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0188 (x y f : SemanticCore.Var) :
                            Nominal.TAlphaWff [(nb068AlphaDummy175, nb068AlphaDummy177 f), (nb068AlphaDummy176, nb068AlphaDummy178 f), (nb068AlphaDummy201, nb068AlphaDummy202 f), (nb068AlphaDummy199, nb068AlphaDummy200 f), (nb068AlphaDummy168, nb068AlphaDummy170 f), (nb068AlphaDummy167, nb068AlphaDummy169 f), (nb068AlphaDummy197, nb068AlphaDummy198 f), (nb068AlphaDummy171, nb068AlphaDummy172 f), (nb068AlphaDummy126, nb068AlphaDummy128 f), (nb068AlphaDummy125, nb068AlphaDummy127 f), (nb068AlphaDummy129, nb068AlphaDummy130 f), (nb068AlphaDummy329, nb068AlphaDummy332 f), (nb068AlphaDummy328, nb068AlphaDummy331 f), (nb068AlphaDummy327, nb068AlphaDummy330 f), (nb068AlphaDummy333, nb068AlphaDummy334 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy176) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy175) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb068AlphaDummy175) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv nb068AlphaDummy175))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy178 f)) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy177 f)) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb068AlphaDummy177 f)) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv (nb068AlphaDummy177 f))))

                            Checked nominal proof certificate identified upstream as nb068_split_alpha_0188.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              source
                              noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0189 (x y f : SemanticCore.Var) :
                              Nominal.TAlphaWff [(nb068AlphaDummy197, nb068AlphaDummy198 f), (nb068AlphaDummy171, nb068AlphaDummy172 f), (nb068AlphaDummy126, nb068AlphaDummy128 f), (nb068AlphaDummy125, nb068AlphaDummy127 f), (nb068AlphaDummy129, nb068AlphaDummy130 f), (nb068AlphaDummy329, nb068AlphaDummy332 f), (nb068AlphaDummy328, nb068AlphaDummy331 f), (nb068AlphaDummy327, nb068AlphaDummy330 f), (nb068AlphaDummy333, nb068AlphaDummy334 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy197) (SemanticCore.Class.cab nb068AlphaDummy167 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy168 (SemanticCore.Class.cv nb068AlphaDummy125) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy167) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy168)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy197) (SemanticCore.Class.cab nb068AlphaDummy167 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy168 (SemanticCore.Class.cv nb068AlphaDummy125) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy167) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy168)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy198 f)) (SemanticCore.Class.cab (nb068AlphaDummy169 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy170 f) (SemanticCore.Class.cv (nb068AlphaDummy127 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy169 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy170 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy198 f)) (SemanticCore.Class.cab (nb068AlphaDummy169 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy170 f) (SemanticCore.Class.cv (nb068AlphaDummy127 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy169 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy170 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg)

                              Checked nominal proof certificate identified upstream as nb068_split_alpha_0189.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                source
                                noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0190 (x y f : SemanticCore.Var) :
                                Nominal.TAlphaWff [(nb068AlphaDummy126, nb068AlphaDummy128 f), (nb068AlphaDummy125, nb068AlphaDummy127 f), (nb068AlphaDummy129, nb068AlphaDummy130 f), (nb068AlphaDummy329, nb068AlphaDummy332 f), (nb068AlphaDummy328, nb068AlphaDummy331 f), (nb068AlphaDummy327, nb068AlphaDummy330 f), (nb068AlphaDummy333, nb068AlphaDummy334 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] ((SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy129) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv nb068AlphaDummy125) (SemanticCore.Class.cv nb068AlphaDummy126))).imp (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb068AlphaDummy126) (SemanticCore.Class.cv nb068AlphaDummy000) (SemanticCore.Class.cv nb068AlphaDummy125)).neg) ((SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy130 f)) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv (nb068AlphaDummy127 f)) (SemanticCore.Class.cv (nb068AlphaDummy128 f)))).imp (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb068AlphaDummy128 f)) (SemanticCore.Class.cv f) (SemanticCore.Class.cv (nb068AlphaDummy127 f))).neg)

                                Checked nominal proof certificate identified upstream as nb068_split_alpha_0190.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  source
                                  noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0191 (x y f : SemanticCore.Var) :
                                  Nominal.TAlphaWff [(nb068AlphaDummy329, nb068AlphaDummy332 f), (nb068AlphaDummy328, nb068AlphaDummy331 f), (nb068AlphaDummy327, nb068AlphaDummy330 f), (nb068AlphaDummy333, nb068AlphaDummy334 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] ((Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb068AlphaDummy327) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb068AlphaDummy000))) (SemanticCore.Class.cv nb068AlphaDummy329)).imp (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb068AlphaDummy329) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb068AlphaDummy000)) (SemanticCore.Class.cv nb068AlphaDummy328)).neg) ((Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb068AlphaDummy330 f)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))) (SemanticCore.Class.cv (nb068AlphaDummy332 f))).imp (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb068AlphaDummy332 f)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)) (SemanticCore.Class.cv (nb068AlphaDummy331 f))).neg)

                                  Checked nominal proof certificate identified upstream as nb068_split_alpha_0191.

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    source
                                    noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0192 (x y f : SemanticCore.Var) (dv_f_x : f ≠ x) (dv_f_y : f ≠ y) (dv_x_y : x ≠ y) :
                                    Nominal.TAlphaWff [(nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] ((Compiler.CompactSourceSyntax.synWf (SemanticCore.Class.cv nb068AlphaDummy000) (SemanticCore.Class.cv nb068AlphaDummy001) (SemanticCore.Class.cv nb068AlphaDummy002)).imp (Compiler.CompactSourceSyntax.synWfun (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb068AlphaDummy000))).neg) ((Compiler.CompactSourceSyntax.synWf (SemanticCore.Class.cv f) (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)).imp (Compiler.CompactSourceSyntax.synWfun (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))).neg)

                                    Checked nominal proof certificate identified upstream as nb068_split_alpha_0192.

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