Formal target: Corpus.OtherEquationalTheories677255.Finite.Equation677_not_implies_Equation255

The negation of Finite.Equation677_implies_Equation255.

Exact formal statement

Exists.{2} fun G =>
  Exists.{1} fun x =>
    And (Finite.{1} G)
      (And (Corpus.OtherEquationalTheories677255.Equation677 G)
        (Not (Corpus.OtherEquationalTheories677255.Equation255 G)))

This target is a formal statement, not a proof of the problem.

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record