Documentation

LeanPool.NFWeakPartition.Certificates.NAR4C068C001Block009

Nominal proof certificates grouped in dependency order.

Certificates from NAR4C068C001Part032.

source
noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0068 (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), (nb068AlphaDummy240, nb068AlphaDummy242 f), (nb068AlphaDummy239, nb068AlphaDummy241 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb068AlphaDummy146) (SemanticCore.Class.cv nb068AlphaDummy147)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy145) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb068AlphaDummy146) (SemanticCore.Class.cv nb068AlphaDummy147))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb068AlphaDummy149 f)) (SemanticCore.Class.cv (nb068AlphaDummy150 f))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy148 f)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb068AlphaDummy149 f)) (SemanticCore.Class.cv (nb068AlphaDummy150 f)))).neg)

Checked nominal proof certificate identified upstream as nb068_split_alpha_0068.

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

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0070 (x y f : SemanticCore.Var) :
      Nominal.TAlphaWff [(nb068AlphaDummy161, nb068AlphaDummy162 f), (nb068AlphaDummy135, nb068AlphaDummy136 f), (nb068AlphaDummy126, nb068AlphaDummy128 f), (nb068AlphaDummy125, nb068AlphaDummy127 f), (nb068AlphaDummy129, nb068AlphaDummy130 f), (nb068AlphaDummy240, nb068AlphaDummy242 f), (nb068AlphaDummy239, nb068AlphaDummy241 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] ((SemanticCore.Wff.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_0070.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0071 (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), (nb068AlphaDummy240, nb068AlphaDummy242 f), (nb068AlphaDummy239, nb068AlphaDummy241 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv 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_0071.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0072 (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), (nb068AlphaDummy240, nb068AlphaDummy242 f), (nb068AlphaDummy239, nb068AlphaDummy241 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy175) (SemanticCore.Class.cv nb068AlphaDummy168)) (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 (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy177 f)) (SemanticCore.Class.cv (nb068AlphaDummy170 f))) (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_0072.

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

            Certificates from NAR4C068C001Part033.

            source
            noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0073 (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), (nb068AlphaDummy240, nb068AlphaDummy242 f), (nb068AlphaDummy239, nb068AlphaDummy241 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv 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_0073.

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

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0075 (x y f : SemanticCore.Var) :
                Nominal.TAlphaWff [(nb068AlphaDummy197, nb068AlphaDummy198 f), (nb068AlphaDummy171, nb068AlphaDummy172 f), (nb068AlphaDummy126, nb068AlphaDummy128 f), (nb068AlphaDummy125, nb068AlphaDummy127 f), (nb068AlphaDummy129, nb068AlphaDummy130 f), (nb068AlphaDummy240, nb068AlphaDummy242 f), (nb068AlphaDummy239, nb068AlphaDummy241 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] ((SemanticCore.Wff.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_0075.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0076 (x y f : SemanticCore.Var) :
                  Nominal.TAlphaWff [(nb068AlphaDummy126, nb068AlphaDummy128 f), (nb068AlphaDummy125, nb068AlphaDummy127 f), (nb068AlphaDummy129, nb068AlphaDummy130 f), (nb068AlphaDummy240, nb068AlphaDummy242 f), (nb068AlphaDummy239, nb068AlphaDummy241 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] ((SemanticCore.Wff.classEq (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_0076.

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

                    Checked nominal proof certificate identified upstream as nb068_split_alpha_0077.

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

                      Certificates from NAR4C068C001Part034.

                      source
                      noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0078 (x y f : SemanticCore.Var) :
                      Nominal.TAlphaWff [(nb068AlphaDummy303, nb068AlphaDummy306 f), (nb068AlphaDummy302, nb068AlphaDummy305 f), (nb068AlphaDummy301, nb068AlphaDummy304 f), (nb068AlphaDummy299, nb068AlphaDummy300 f), (nb068AlphaDummy295, nb068AlphaDummy297 f), (nb068AlphaDummy296, nb068AlphaDummy298 f), (nb068AlphaDummy288, nb068AlphaDummy290 f), (nb068AlphaDummy287, nb068AlphaDummy289 f), (nb068AlphaDummy293, nb068AlphaDummy294 f), (nb068AlphaDummy291, nb068AlphaDummy292 f), (nb068AlphaDummy284, nb068AlphaDummy286 f), (nb068AlphaDummy283, nb068AlphaDummy285 f), (nb068AlphaDummy281, nb068AlphaDummy282 y f), (nb068AlphaDummy279, nb068AlphaDummy280 y f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb068AlphaDummy302) (SemanticCore.Class.cv nb068AlphaDummy303)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy301) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb068AlphaDummy302) (SemanticCore.Class.cv nb068AlphaDummy303))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb068AlphaDummy305 f)) (SemanticCore.Class.cv (nb068AlphaDummy306 f))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy304 f)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb068AlphaDummy305 f)) (SemanticCore.Class.cv (nb068AlphaDummy306 f)))).neg)

                      Checked nominal proof certificate identified upstream as nb068_split_alpha_0078.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        source
                        noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0079 (x y f : SemanticCore.Var) :
                        Nominal.TAlphaWff [(nb068AlphaDummy288, nb068AlphaDummy290 f), (nb068AlphaDummy287, nb068AlphaDummy289 f), (nb068AlphaDummy293, nb068AlphaDummy294 f), (nb068AlphaDummy291, nb068AlphaDummy292 f), (nb068AlphaDummy284, nb068AlphaDummy286 f), (nb068AlphaDummy283, nb068AlphaDummy285 f), (nb068AlphaDummy281, nb068AlphaDummy282 y f), (nb068AlphaDummy279, nb068AlphaDummy280 y f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy287) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy288))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy289 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy290 f))))

                        Checked nominal proof certificate identified upstream as nb068_split_alpha_0079.

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

                          Certificates from NAR4C068C001Part035.

                          source
                          noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0080 (x y f : SemanticCore.Var) :
                          Nominal.TAlphaWff [(nb068AlphaDummy303, nb068AlphaDummy306 f), (nb068AlphaDummy302, nb068AlphaDummy305 f), (nb068AlphaDummy301, nb068AlphaDummy304 f), (nb068AlphaDummy299, nb068AlphaDummy300 f), (nb068AlphaDummy295, nb068AlphaDummy297 f), (nb068AlphaDummy296, nb068AlphaDummy298 f), (nb068AlphaDummy321, nb068AlphaDummy322 f), (nb068AlphaDummy319, nb068AlphaDummy320 f), (nb068AlphaDummy288, nb068AlphaDummy290 f), (nb068AlphaDummy287, nb068AlphaDummy289 f), (nb068AlphaDummy317, nb068AlphaDummy318 f), (nb068AlphaDummy291, nb068AlphaDummy292 f), (nb068AlphaDummy284, nb068AlphaDummy286 f), (nb068AlphaDummy283, nb068AlphaDummy285 f), (nb068AlphaDummy281, nb068AlphaDummy282 y f), (nb068AlphaDummy279, nb068AlphaDummy280 y f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb068AlphaDummy302) (SemanticCore.Class.cv nb068AlphaDummy303)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy301) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb068AlphaDummy302) (SemanticCore.Class.cv nb068AlphaDummy303))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb068AlphaDummy305 f)) (SemanticCore.Class.cv (nb068AlphaDummy306 f))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy304 f)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb068AlphaDummy305 f)) (SemanticCore.Class.cv (nb068AlphaDummy306 f)))).neg)

                          Checked nominal proof certificate identified upstream as nb068_split_alpha_0080.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            source
                            noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0081 (x y f : SemanticCore.Var) :
                            Nominal.TAlphaWff [(nb068AlphaDummy295, nb068AlphaDummy297 f), (nb068AlphaDummy296, nb068AlphaDummy298 f), (nb068AlphaDummy321, nb068AlphaDummy322 f), (nb068AlphaDummy319, nb068AlphaDummy320 f), (nb068AlphaDummy288, nb068AlphaDummy290 f), (nb068AlphaDummy287, nb068AlphaDummy289 f), (nb068AlphaDummy317, nb068AlphaDummy318 f), (nb068AlphaDummy291, nb068AlphaDummy292 f), (nb068AlphaDummy284, nb068AlphaDummy286 f), (nb068AlphaDummy283, nb068AlphaDummy285 f), (nb068AlphaDummy281, nb068AlphaDummy282 y f), (nb068AlphaDummy279, nb068AlphaDummy280 y f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy295) (SemanticCore.Class.cv nb068AlphaDummy288)).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy296) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy295) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb068AlphaDummy295) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv nb068AlphaDummy295))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy297 f)) (SemanticCore.Class.cv (nb068AlphaDummy290 f))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy298 f)) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy297 f)) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb068AlphaDummy297 f)) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv (nb068AlphaDummy297 f)))).neg)

                            Checked nominal proof certificate identified upstream as nb068_split_alpha_0081.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              source
                              noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0082 (x y f : SemanticCore.Var) :
                              Nominal.TAlphaWff [(nb068AlphaDummy317, nb068AlphaDummy318 f), (nb068AlphaDummy291, nb068AlphaDummy292 f), (nb068AlphaDummy284, nb068AlphaDummy286 f), (nb068AlphaDummy283, nb068AlphaDummy285 f), (nb068AlphaDummy281, nb068AlphaDummy282 y f), (nb068AlphaDummy279, nb068AlphaDummy280 y f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy317) (SemanticCore.Class.cab nb068AlphaDummy287 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy288 (SemanticCore.Class.cv nb068AlphaDummy283) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy287) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy288)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy317) (SemanticCore.Class.cab nb068AlphaDummy287 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy288 (SemanticCore.Class.cv nb068AlphaDummy283) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy287) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy288)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy318 f)) (SemanticCore.Class.cab (nb068AlphaDummy289 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy290 f) (SemanticCore.Class.cv (nb068AlphaDummy285 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy289 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy290 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy318 f)) (SemanticCore.Class.cab (nb068AlphaDummy289 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy290 f) (SemanticCore.Class.cv (nb068AlphaDummy285 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy289 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy290 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg)

                              Checked nominal proof certificate identified upstream as nb068_split_alpha_0082.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                source
                                noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0083 (x y f : SemanticCore.Var) (dv_f_y : f ≠ y) :
                                Nominal.TAlphaWff [(nb068AlphaDummy279, nb068AlphaDummy280 y f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy279) (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv nb068AlphaDummy000)) (SemanticCore.Class.cv nb068AlphaDummy002))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy279) (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv nb068AlphaDummy000)) (SemanticCore.Class.cv nb068AlphaDummy002))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy280 y f)) (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv f)) (SemanticCore.Class.cv y))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy280 y f)) (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv f)) (SemanticCore.Class.cv y))).neg)

                                Checked nominal proof certificate identified upstream as nb068_split_alpha_0083.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  source
                                  noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0084 (x y f : SemanticCore.Var) :
                                  Nominal.TAlphaWff [(nb068AlphaDummy303, nb068AlphaDummy306 f), (nb068AlphaDummy302, nb068AlphaDummy305 f), (nb068AlphaDummy301, nb068AlphaDummy304 f), (nb068AlphaDummy299, nb068AlphaDummy300 f), (nb068AlphaDummy295, nb068AlphaDummy297 f), (nb068AlphaDummy296, nb068AlphaDummy298 f), (nb068AlphaDummy288, nb068AlphaDummy290 f), (nb068AlphaDummy287, nb068AlphaDummy289 f), (nb068AlphaDummy293, nb068AlphaDummy294 f), (nb068AlphaDummy291, nb068AlphaDummy292 f), (nb068AlphaDummy284, nb068AlphaDummy286 f), (nb068AlphaDummy283, nb068AlphaDummy285 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb068AlphaDummy302) (SemanticCore.Class.cv nb068AlphaDummy303)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy301) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb068AlphaDummy302) (SemanticCore.Class.cv nb068AlphaDummy303))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb068AlphaDummy305 f)) (SemanticCore.Class.cv (nb068AlphaDummy306 f))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy304 f)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb068AlphaDummy305 f)) (SemanticCore.Class.cv (nb068AlphaDummy306 f)))).neg)

                                  Checked nominal proof certificate identified upstream as nb068_split_alpha_0084.

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