Created
August 23, 2018 21:44
-
-
Save kbuzzard/84dbdf0fab4b96148099f49ac4f1770e to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| failed to synthesize type class instance for | |
| ⊢ decidable | |
| (∃ (x : square), | |
| … ∧ | |
| ∀ (y : square), | |
| (∃ (x : square), | |
| (∃ (x_1 : square), | |
| … ∧ | |
| ∀ (y_1 : square), | |
| (∃ (x_1 : square), | |
| (∃ (x_2 : square), | |
| (∃ (x_3 : square), | |
| … ∧ | |
| ∀ (y_2 : square), | |
| (∃ (x_3 : square), | |
| … ∧ | |
| ∀ (y_3 : square), | |
| (∃ (x_3 : square), | |
| … ∧ | |
| ∀ (y_4 : square), | |
| (∃ (x_3 : square), | |
| is_solved y x y_1 x_1 x_2 y_2 y_3 y_4 x_3 ∧ | |
| ∀ (y_5 : square), | |
| is_solved y x y_1 x_1 x_2 y_2 y_3 y_4 y_5 → | |
| y_5 = x_3) → | |
| y_4 = x_3) → | |
| …) → | |
| …) ∧ | |
| ∀ (y_2 : square), | |
| (∃ (x_2 : square), | |
| (∃ (x_3 : square), | |
| (∃ (x_4 : square), | |
| (∃ (x_5 : square), | |
| is_solved y x y_1 x_1 y_2 x_2 x_3 x_4 x_5 ∧ | |
| ∀ (y_3 : square), | |
| is_solved y x y_1 x_1 y_2 x_2 x_3 x_4 y_3 → y_3 = x_5) ∧ | |
| ∀ (y_3 : square), | |
| (∃ (x_4 : square), | |
| is_solved y x y_1 x_1 y_2 x_2 x_3 y_3 x_4 ∧ | |
| ∀ (y_4 : square), | |
| is_solved y x y_1 x_1 y_2 x_2 x_3 y_3 y_4 → y_4 = x_4) → | |
| y_3 = x_4) ∧ | |
| ∀ (y_3 : square), | |
| (∃ (x_3 : square), | |
| (∃ (x_4 : square), | |
| is_solved y x y_1 x_1 y_2 x_2 y_3 x_3 x_4 ∧ | |
| ∀ (y_4 : square), | |
| is_solved y x y_1 x_1 y_2 x_2 y_3 x_3 y_4 → y_4 = x_4) ∧ | |
| ∀ (y_4 : square), | |
| (∃ (x_3 : square), | |
| is_solved y x y_1 x_1 y_2 x_2 y_3 y_4 x_3 ∧ | |
| ∀ (y_5 : square), | |
| is_solved y x y_1 x_1 y_2 x_2 y_3 y_4 y_5 → | |
| y_5 = x_3) → | |
| y_4 = x_3) → | |
| y_3 = x_3) ∧ | |
| ∀ (y_3 : square), | |
| (∃ (x_2 : square), | |
| (∃ (x_3 : square), | |
| (∃ (x_4 : square), | |
| is_solved y x y_1 x_1 y_2 y_3 x_2 x_3 x_4 ∧ | |
| ∀ (y_4 : square), | |
| is_solved y x y_1 x_1 y_2 y_3 x_2 x_3 y_4 → y_4 = x_4) ∧ | |
| ∀ (y_4 : square), | |
| (∃ (x_3 : square), | |
| is_solved y x y_1 x_1 y_2 y_3 x_2 y_4 x_3 ∧ | |
| ∀ (y_5 : square), | |
| is_solved y x y_1 x_1 y_2 y_3 x_2 y_4 y_5 → | |
| y_5 = x_3) → | |
| y_4 = x_3) ∧ | |
| ∀ (y_4 : square), | |
| (∃ (x_2 : square), | |
| (∃ (x_3 : square), | |
| is_solved y x y_1 x_1 y_2 y_3 y_4 x_2 x_3 ∧ | |
| ∀ (y_5 : square), | |
| is_solved y x y_1 x_1 y_2 y_3 y_4 x_2 y_5 → | |
| y_5 = x_3) ∧ | |
| ∀ (y_5 : square), | |
| (∃ (x_2 : square), | |
| is_solved y x y_1 x_1 y_2 y_3 y_4 y_5 x_2 ∧ | |
| ∀ (y_6 : square), | |
| is_solved y x y_1 x_1 y_2 y_3 y_4 y_5 y_6 → | |
| y_6 = x_2) → | |
| y_5 = x_2) → | |
| y_4 = x_2) → | |
| y_3 = x_2) → | |
| y_2 = x_2) ∧ | |
| ∀ (y_2 : square), | |
| (∃ (x_1 : square), | |
| (∃ (x_2 : square), | |
| (∃ (x_3 : square), | |
| (∃ (x_4 : square), | |
| (∃ (x_5 : square), | |
| is_solved y x y_1 y_2 x_1 x_2 x_3 x_4 x_5 ∧ | |
| ∀ (y_3 : square), | |
| is_solved y x y_1 y_2 x_1 x_2 x_3 x_4 y_3 → y_3 = x_5) ∧ | |
| ∀ (y_3 : square), | |
| (∃ (x_4 : square), | |
| is_solved y x y_1 y_2 x_1 x_2 x_3 y_3 x_4 ∧ | |
| ∀ (y_4 : square), | |
| is_solved y x y_1 y_2 x_1 x_2 x_3 y_3 y_4 → y_4 = x_4) → | |
| y_3 = x_4) ∧ | |
| ∀ (y_3 : square), | |
| (∃ (x_3 : square), | |
| (∃ (x_4 : square), | |
| is_solved y x y_1 y_2 x_1 x_2 y_3 x_3 x_4 ∧ | |
| ∀ (y_4 : square), | |
| is_solved y x y_1 y_2 x_1 x_2 y_3 x_3 y_4 → y_4 = x_4) ∧ | |
| ∀ (y_4 : square), | |
| (∃ (x_3 : square), | |
| is_solved y x y_1 y_2 x_1 x_2 y_3 y_4 x_3 ∧ | |
| ∀ (y_5 : square), | |
| is_solved y x y_1 y_2 x_1 x_2 y_3 y_4 y_5 → | |
| y_5 = x_3) → | |
| y_4 = x_3) → | |
| y_3 = x_3) ∧ | |
| ∀ (y_3 : square), | |
| (∃ (x_2 : square), | |
| (∃ (x_3 : square), | |
| (∃ (x_4 : square), | |
| is_solved y x y_1 y_2 x_1 y_3 x_2 x_3 x_4 ∧ | |
| ∀ (y_4 : square), | |
| is_solved y x y_1 y_2 x_1 y_3 x_2 x_3 y_4 → y_4 = x_4) ∧ | |
| ∀ (y_4 : square), | |
| (∃ (x_3 : square), | |
| is_solved y x y_1 y_2 x_1 y_3 x_2 y_4 x_3 ∧ | |
| ∀ (y_5 : square), | |
| is_solved y x y_1 y_2 x_1 y_3 x_2 y_4 y_5 → | |
| y_5 = x_3) → | |
| y_4 = x_3) ∧ | |
| ∀ (y_4 : square), | |
| (∃ (x_2 : square), | |
| (∃ (x_3 : square), | |
| is_solved y x y_1 y_2 x_1 y_3 y_4 x_2 x_3 ∧ | |
| ∀ (y_5 : square), | |
| is_solved y x y_1 y_2 x_1 y_3 y_4 x_2 y_5 → | |
| y_5 = x_3) ∧ | |
| ∀ (y_5 : square), | |
| (∃ (x_2 : square), | |
| is_solved y x y_1 y_2 x_1 y_3 y_4 y_5 x_2 ∧ | |
| ∀ (y_6 : square), | |
| is_solved y x y_1 y_2 x_1 y_3 y_4 y_5 y_6 → | |
| y_6 = x_2) → | |
| y_5 = x_2) → | |
| y_4 = x_2) → | |
| y_3 = x_2) ∧ | |
| ∀ (y_3 : square), | |
| (∃ (x_1 : square), | |
| (∃ (x_2 : square), | |
| (∃ (x_3 : square), | |
| (∃ (x_4 : square), | |
| is_solved y x y_1 y_2 y_3 x_1 x_2 x_3 x_4 ∧ | |
| ∀ (y_4 : square), | |
| is_solved y x y_1 y_2 y_3 x_1 x_2 x_3 y_4 → y_4 = x_4) ∧ | |
| ∀ (y_4 : square), | |
| (∃ (x_3 : square), | |
| is_solved y x y_1 y_2 y_3 x_1 x_2 y_4 x_3 ∧ | |
| ∀ (y_5 : square), | |
| is_solved y x y_1 y_2 y_3 x_1 x_2 y_4 y_5 → | |
| y_5 = x_3) → | |
| y_4 = x_3) ∧ | |
| ∀ (y_4 : square), | |
| (∃ (x_2 : square), | |
| (∃ (x_3 : square), | |
| is_solved y x y_1 y_2 y_3 x_1 y_4 x_2 x_3 ∧ | |
| ∀ (y_5 : square), | |
| is_solved y x y_1 y_2 y_3 x_1 y_4 x_2 y_5 → | |
| y_5 = x_3) ∧ | |
| ∀ (y_5 : square), | |
| (∃ (x_2 : square), | |
| is_solved y x y_1 y_2 y_3 x_1 y_4 y_5 x_2 ∧ | |
| ∀ (y_6 : square), | |
| is_solved y x y_1 y_2 y_3 x_1 y_4 y_5 y_6 → | |
| y_6 = x_2) → | |
| y_5 = x_2) → | |
| y_4 = x_2) ∧ | |
| ∀ (y_4 : square), | |
| (∃ (x_1 : square), | |
| (∃ (x_2 : square), | |
| (∃ (x_3 : square), | |
| is_solved y x y_1 y_2 y_3 y_4 x_1 x_2 x_3 ∧ | |
| ∀ (y_5 : square), | |
| is_solved y x y_1 y_2 y_3 y_4 x_1 x_2 y_5 → | |
| y_5 = x_3) ∧ | |
| ∀ (y_5 : square), | |
| (∃ (x_2 : square), | |
| is_solved y x y_1 y_2 y_3 y_4 x_1 y_5 x_2 ∧ | |
| ∀ (y_6 : square), | |
| is_solved y x y_1 y_2 y_3 y_4 x_1 y_5 y_6 → | |
| y_6 = x_2) → | |
| y_5 = x_2) ∧ | |
| ∀ (y_5 : square), | |
| (∃ (x_1 : square), | |
| (∃ (x_2 : square), | |
| is_solved y x y_1 y_2 y_3 y_4 y_5 x_1 x_2 ∧ | |
| ∀ (y_6 : square), | |
| is_solved y x y_1 y_2 y_3 y_4 y_5 x_1 y_6 → | |
| y_6 = x_2) ∧ | |
| ∀ (y_6 : square), | |
| (∃ (x_1 : square), | |
| is_solved y x y_1 y_2 y_3 y_4 y_5 y_6 x_1 ∧ | |
| ∀ (y_7 : square), | |
| is_solved y x y_1 y_2 y_3 y_4 y_5 y_6 y_7 → | |
| y_7 = x_1) → | |
| y_6 = x_1) → | |
| y_5 = x_1) → | |
| y_4 = x_1) → | |
| y_3 = x_1) → | |
| y_2 = x_1) → | |
| …) ∧ | |
| ∀ (y_1 : square), | |
| (∃ (x : square), | |
| (∃ (x_1 : square), | |
| (∃ (x_2 : square), | |
| (∃ (x_3 : square), | |
| (∃ (x_4 : square), | |
| (∃ (x_5 : square), | |
| (∃ (x_6 : square), | |
| is_solved y y_1 x x_1 x_2 x_3 x_4 x_5 x_6 ∧ | |
| ∀ (y_2 : square), | |
| is_solved y y_1 x x_1 x_2 x_3 x_4 x_5 y_2 → y_2 = x_6) ∧ | |
| ∀ (y_2 : square), | |
| (∃ (x_5 : square), | |
| is_solved y y_1 x x_1 x_2 x_3 x_4 y_2 x_5 ∧ | |
| ∀ (y_3 : square), | |
| is_solved y y_1 x x_1 x_2 x_3 x_4 y_2 y_3 → y_3 = x_5) → | |
| y_2 = x_5) ∧ | |
| ∀ (y_2 : square), | |
| (∃ (x_4 : square), | |
| (∃ (x_5 : square), | |
| is_solved y y_1 x x_1 x_2 x_3 y_2 x_4 x_5 ∧ | |
| ∀ (y_3 : square), | |
| is_solved y y_1 x x_1 x_2 x_3 y_2 x_4 y_3 → y_3 = x_5) ∧ | |
| ∀ (y_3 : square), | |
| (∃ (x_4 : square), | |
| is_solved y y_1 x x_1 x_2 x_3 y_2 y_3 x_4 ∧ | |
| ∀ (y_4 : square), | |
| is_solved y y_1 x x_1 x_2 x_3 y_2 y_3 y_4 → y_4 = x_4) → | |
| y_3 = x_4) → | |
| y_2 = x_4) ∧ | |
| ∀ (y_2 : square), | |
| (∃ (x_3 : square), | |
| (∃ (x_4 : square), | |
| (∃ (x_5 : square), | |
| is_solved y y_1 x x_1 x_2 y_2 x_3 x_4 x_5 ∧ | |
| ∀ (y_3 : square), | |
| is_solved y y_1 x x_1 x_2 y_2 x_3 x_4 y_3 → y_3 = x_5) ∧ | |
| ∀ (y_3 : square), | |
| (∃ (x_4 : square), | |
| is_solved y y_1 x x_1 x_2 y_2 x_3 y_3 x_4 ∧ | |
| ∀ (y_4 : square), | |
| is_solved y y_1 x x_1 x_2 y_2 x_3 y_3 y_4 → y_4 = x_4) → | |
| y_3 = x_4) ∧ | |
| ∀ (y_3 : square), | |
| (∃ (x_3 : square), | |
| (∃ (x_4 : square), | |
| is_solved y y_1 x x_1 x_2 y_2 y_3 x_3 x_4 ∧ | |
| ∀ (y_4 : square), | |
| is_solved y y_1 x x_1 x_2 y_2 y_3 x_3 y_4 → y_4 = x_4) ∧ | |
| ∀ (y_4 : square), | |
| (∃ (x_3 : square), | |
| is_solved y y_1 x x_1 x_2 y_2 y_3 y_4 x_3 ∧ | |
| ∀ (y_5 : square), | |
| is_solved y y_1 x x_1 x_2 y_2 y_3 y_4 y_5 → | |
| y_5 = x_3) → | |
| y_4 = x_3) → | |
| y_3 = x_3) → | |
| y_2 = x_3) ∧ | |
| ∀ (y_2 : square), | |
| (∃ (x_2 : square), | |
| (∃ (x_3 : square), | |
| (∃ (x_4 : square), | |
| (∃ (x_5 : square), | |
| is_solved y y_1 x x_1 y_2 x_2 x_3 x_4 x_5 ∧ | |
| ∀ (y_3 : square), | |
| is_solved y y_1 x x_1 y_2 x_2 x_3 x_4 y_3 → y_3 = x_5) ∧ | |
| ∀ (y_3 : square), | |
| (∃ (x_4 : square), | |
| is_solved y y_1 x x_1 y_2 x_2 x_3 y_3 x_4 ∧ | |
| ∀ (y_4 : square), | |
| is_solved y y_1 x x_1 y_2 x_2 x_3 y_3 y_4 → y_4 = x_4) → | |
| y_3 = x_4) ∧ | |
| ∀ (y_3 : square), | |
| (∃ (x_3 : square), | |
| (∃ (x_4 : square), | |
| is_solved y y_1 x x_1 y_2 x_2 y_3 x_3 x_4 ∧ | |
| ∀ (y_4 : square), | |
| is_solved y y_1 x x_1 y_2 x_2 y_3 x_3 y_4 → y_4 = x_4) ∧ | |
| ∀ (y_4 : square), | |
| (∃ (x_3 : square), | |
| is_solved y y_1 x x_1 y_2 x_2 y_3 y_4 x_3 ∧ | |
| ∀ (y_5 : square), | |
| is_solved y y_1 x x_1 y_2 x_2 y_3 y_4 y_5 → | |
| y_5 = x_3) → | |
| y_4 = x_3) → | |
| y_3 = x_3) ∧ | |
| ∀ (y_3 : square), | |
| (∃ (x_2 : square), | |
| (∃ (x_3 : square), | |
| (∃ (x_4 : square), | |
| is_solved y y_1 x x_1 y_2 y_3 x_2 x_3 x_4 ∧ | |
| ∀ (y_4 : square), | |
| is_solved y y_1 x x_1 y_2 y_3 x_2 x_3 y_4 → y_4 = x_4) ∧ | |
| ∀ (y_4 : square), | |
| (∃ (x_3 : square), | |
| is_solved y y_1 x x_1 y_2 y_3 x_2 y_4 x_3 ∧ | |
| ∀ (y_5 : square), | |
| is_solved y y_1 x x_1 y_2 y_3 x_2 y_4 y_5 → | |
| y_5 = x_3) → | |
| y_4 = x_3) ∧ | |
| ∀ (y_4 : square), | |
| (∃ (x_2 : square), | |
| (∃ (x_3 : square), | |
| is_solved y y_1 x x_1 y_2 y_3 y_4 x_2 x_3 ∧ | |
| ∀ (y_5 : square), | |
| is_solved y y_1 x x_1 y_2 y_3 y_4 x_2 y_5 → | |
| y_5 = x_3) ∧ | |
| ∀ (y_5 : square), | |
| (∃ (x_2 : square), | |
| is_solved y y_1 x x_1 y_2 y_3 y_4 y_5 x_2 ∧ | |
| ∀ (y_6 : square), | |
| is_solved y y_1 x x_1 y_2 y_3 y_4 y_5 y_6 → | |
| y_6 = x_2) → | |
| y_5 = x_2) → | |
| y_4 = x_2) → | |
| y_3 = x_2) → | |
| y_2 = x_2) ∧ | |
| ∀ (y_2 : square), | |
| (∃ (x_1 : square), | |
| (∃ (x_2 : square), | |
| (∃ (x_3 : square), | |
| (∃ (x_4 : square), | |
| (∃ (x_5 : square), | |
| is_solved y y_1 x y_2 x_1 x_2 x_3 x_4 x_5 ∧ | |
| ∀ (y_3 : square), | |
| is_solved y y_1 x y_2 x_1 x_2 x_3 x_4 y_3 → y_3 = x_5) ∧ | |
| ∀ (y_3 : square), | |
| (∃ (x_4 : square), | |
| is_solved y y_1 x y_2 x_1 x_2 x_3 y_3 x_4 ∧ | |
| ∀ (y_4 : square), | |
| is_solved y y_1 x y_2 x_1 x_2 x_3 y_3 y_4 → y_4 = x_4) → | |
| y_3 = x_4) ∧ | |
| ∀ (y_3 : square), | |
| (∃ (x_3 : square), | |
| (∃ (x_4 : square), | |
| is_solved y y_1 x y_2 x_1 x_2 y_3 x_3 x_4 ∧ | |
| ∀ (y_4 : square), | |
| is_solved y y_1 x y_2 x_1 x_2 y_3 x_3 y_4 → y_4 = x_4) ∧ | |
| ∀ (y_4 : square), | |
| (∃ (x_3 : square), | |
| is_solved y y_1 x y_2 x_1 x_2 y_3 y_4 x_3 ∧ | |
| ∀ (y_5 : square), | |
| is_solved y y_1 x y_2 x_1 x_2 y_3 y_4 y_5 → | |
| y_5 = x_3) → | |
| y_4 = x_3) → | |
| y_3 = x_3) ∧ | |
| ∀ (y_3 : square), | |
| (∃ (x_2 : square), | |
| (∃ (x_3 : square), | |
| (∃ (x_4 : square), | |
| is_solved y y_1 x y_2 x_1 y_3 x_2 x_3 x_4 ∧ | |
| ∀ (y_4 : square), | |
| is_solved y y_1 x y_2 x_1 y_3 x_2 x_3 y_4 → y_4 = x_4) ∧ | |
| ∀ (y_4 : square), | |
| (∃ (x_3 : square), | |
| is_solved y y_1 x y_2 x_1 y_3 x_2 y_4 x_3 ∧ | |
| ∀ (y_5 : square), | |
| is_solved y y_1 x y_2 x_1 y_3 x_2 y_4 y_5 → | |
| y_5 = x_3) → | |
| y_4 = x_3) ∧ | |
| ∀ (y_4 : square), | |
| (∃ (x_2 : square), | |
| (∃ (x_3 : square), | |
| is_solved y y_1 x y_2 x_1 y_3 y_4 x_2 x_3 ∧ | |
| ∀ (y_5 : square), | |
| is_solved y y_1 x y_2 x_1 y_3 y_4 x_2 y_5 → | |
| y_5 = x_3) ∧ | |
| ∀ (y_5 : square), | |
| (∃ (x_2 : square), | |
| is_solved y y_1 x y_2 x_1 y_3 y_4 y_5 x_2 ∧ | |
| ∀ (y_6 : square), | |
| is_solved y y_1 x y_2 x_1 y_3 y_4 y_5 y_6 → | |
| y_6 = x_2) → | |
| y_5 = x_2) → | |
| y_4 = x_2) → | |
| y_3 = x_2) ∧ | |
| ∀ (y_3 : square), | |
| (∃ (x_1 : square), | |
| (∃ (x_2 : square), | |
| (∃ (x_3 : square), | |
| (∃ (x_4 : square), | |
| is_solved y y_1 x y_2 y_3 x_1 x_2 x_3 x_4 ∧ | |
| ∀ (y_4 : square), | |
| is_solved y y_1 x y_2 y_3 x_1 x_2 x_3 y_4 → y_4 = x_4) ∧ | |
| ∀ (y_4 : square), | |
| (∃ (x_3 : square), | |
| is_solved y y_1 x y_2 y_3 x_1 x_2 y_4 x_3 ∧ | |
| ∀ (y_5 : square), | |
| is_solved y y_1 x y_2 y_3 x_1 x_2 y_4 y_5 → | |
| y_5 = x_3) → | |
| y_4 = x_3) ∧ | |
| ∀ (y_4 : square), | |
| (∃ (x_2 : square), | |
| (∃ (x_3 : square), | |
| is_solved y y_1 x y_2 y_3 x_1 y_4 x_2 x_3 ∧ | |
| ∀ (y_5 : square), | |
| is_solved y y_1 x y_2 y_3 x_1 y_4 x_2 y_5 → | |
| y_5 = x_3) ∧ | |
| ∀ (y_5 : square), | |
| (∃ (x_2 : square), | |
| is_solved y y_1 x y_2 y_3 x_1 y_4 y_5 x_2 ∧ | |
| ∀ (y_6 : square), | |
| is_solved y y_1 x y_2 y_3 x_1 y_4 y_5 y_6 → | |
| y_6 = x_2) → | |
| y_5 = x_2) → | |
| y_4 = x_2) ∧ | |
| ∀ (y_4 : square), | |
| (∃ (x_1 : square), | |
| (∃ (x_2 : square), | |
| (∃ (x_3 : square), | |
| is_solved y y_1 x y_2 y_3 y_4 x_1 x_2 x_3 ∧ | |
| ∀ (y_5 : square), | |
| is_solved y y_1 x y_2 y_3 y_4 x_1 x_2 y_5 → | |
| y_5 = x_3) ∧ | |
| ∀ (y_5 : square), | |
| (∃ (x_2 : square), | |
| is_solved y y_1 x y_2 y_3 y_4 x_1 y_5 x_2 ∧ | |
| ∀ (y_6 : square), | |
| is_solved y y_1 x y_2 y_3 y_4 x_1 y_5 y_6 → | |
| y_6 = x_2) → | |
| y_5 = x_2) ∧ | |
| ∀ (y_5 : square), | |
| (∃ (x_1 : square), | |
| (∃ (x_2 : square), | |
| is_solved y y_1 x y_2 y_3 y_4 y_5 x_1 x_2 ∧ | |
| ∀ (y_6 : square), | |
| is_solved y y_1 x y_2 y_3 y_4 y_5 x_1 y_6 → | |
| y_6 = x_2) ∧ | |
| ∀ (y_6 : square), | |
| (∃ (x_1 : square), | |
| is_solved y y_1 x y_2 y_3 y_4 y_5 y_6 x_1 ∧ | |
| ∀ (y_7 : square), | |
| is_solved y y_1 x y_2 y_3 y_4 y_5 y_6 y_7 → | |
| y_7 = x_1) → | |
| y_6 = x_1) → | |
| y_5 = x_1) → | |
| y_4 = x_1) → | |
| y_3 = x_1) → | |
| y_2 = x_1) ∧ | |
| ∀ (y_2 : square), | |
| (∃ (x : square), | |
| (∃ (x_1 : square), | |
| (∃ (x_2 : square), | |
| (∃ (x_3 : square), | |
| (∃ (x_4 : square), | |
| (∃ (x_5 : square), | |
| is_solved y y_1 y_2 x x_1 x_2 x_3 x_4 x_5 ∧ | |
| ∀ (y_3 : square), | |
| is_solved y y_1 y_2 x x_1 x_2 x_3 x_4 y_3 → y_3 = x_5) ∧ | |
| ∀ (y_3 : square), | |
| (∃ (x_4 : square), | |
| is_solved y y_1 y_2 x x_1 x_2 x_3 y_3 x_4 ∧ | |
| ∀ (y_4 : square), | |
| is_solved y y_1 y_2 x x_1 x_2 x_3 y_3 y_4 → y_4 = x_4) → | |
| y_3 = x_4) ∧ | |
| ∀ (y_3 : square), | |
| (∃ (x_3 : square), | |
| (∃ (x_4 : square), | |
| is_solved y y_1 y_2 x x_1 x_2 y_3 x_3 x_4 ∧ | |
| ∀ (y_4 : square), | |
| is_solved y y_1 y_2 x x_1 x_2 y_3 x_3 y_4 → y_4 = x_4) ∧ | |
| ∀ (y_4 : square), | |
| (∃ (x_3 : square), | |
| is_solved y y_1 y_2 x x_1 x_2 y_3 y_4 x_3 ∧ | |
| ∀ (y_5 : square), | |
| is_solved y y_1 y_2 x x_1 x_2 y_3 y_4 y_5 → | |
| y_5 = x_3) → | |
| y_4 = x_3) → | |
| y_3 = x_3) ∧ | |
| ∀ (y_3 : square), | |
| (∃ (x_2 : square), | |
| (∃ (x_3 : square), | |
| (∃ (x_4 : square), | |
| is_solved y y_1 y_2 x x_1 y_3 x_2 x_3 x_4 ∧ | |
| ∀ (y_4 : square), | |
| is_solved y y_1 y_2 x x_1 y_3 x_2 x_3 y_4 → y_4 = x_4) ∧ | |
| ∀ (y_4 : square), | |
| (∃ (x_3 : square), | |
| is_solved y y_1 y_2 x x_1 y_3 x_2 y_4 x_3 ∧ | |
| ∀ (y_5 : square), | |
| is_solved y y_1 y_2 x x_1 y_3 x_2 y_4 y_5 → | |
| y_5 = x_3) → | |
| y_4 = x_3) ∧ | |
| ∀ (y_4 : square), | |
| (∃ (x_2 : square), | |
| (∃ (x_3 : square), | |
| is_solved y y_1 y_2 x x_1 y_3 y_4 x_2 x_3 ∧ | |
| ∀ (y_5 : square), | |
| is_solved y y_1 y_2 x x_1 y_3 y_4 x_2 y_5 → | |
| y_5 = x_3) ∧ | |
| ∀ (y_5 : square), | |
| (∃ (x_2 : square), | |
| is_solved y y_1 y_2 x x_1 y_3 y_4 y_5 x_2 ∧ | |
| ∀ (y_6 : square), | |
| is_solved y y_1 y_2 x x_1 y_3 y_4 y_5 y_6 → | |
| y_6 = x_2) → | |
| y_5 = x_2) → | |
| y_4 = x_2) → | |
| y_3 = x_2) ∧ | |
| ∀ (y_3 : square), | |
| (∃ (x_1 : square), | |
| (∃ (x_2 : square), | |
| (∃ (x_3 : square), | |
| (∃ (x_4 : square), | |
| is_solved y y_1 y_2 x y_3 x_1 x_2 x_3 x_4 ∧ | |
| ∀ (y_4 : square), | |
| is_solved y y_1 y_2 x y_3 x_1 x_2 x_3 y_4 → y_4 = x_4) ∧ | |
| ∀ (y_4 : square), | |
| (∃ (x_3 : square), | |
| is_solved y y_1 y_2 x y_3 x_1 x_2 y_4 x_3 ∧ | |
| ∀ (y_5 : square), | |
| is_solved y y_1 y_2 x y_3 x_1 x_2 y_4 y_5 → | |
| y_5 = x_3) → | |
| y_4 = x_3) ∧ | |
| ∀ (y_4 : square), | |
| (∃ (x_2 : square), | |
| (∃ (x_3 : square), | |
| is_solved y y_1 y_2 x y_3 x_1 y_4 x_2 x_3 ∧ | |
| ∀ (y_5 : square), | |
| is_solved y y_1 y_2 x y_3 x_1 y_4 x_2 y_5 → | |
| y_5 = x_3) ∧ | |
| ∀ (y_5 : square), | |
| (∃ (x_2 : square), | |
| is_solved y y_1 y_2 x y_3 x_1 y_4 y_5 x_2 ∧ | |
| ∀ (y_6 : square), | |
| is_solved y y_1 y_2 x y_3 x_1 y_4 y_5 y_6 → | |
| y_6 = x_2) → | |
| y_5 = x_2) → | |
| y_4 = x_2) ∧ | |
| ∀ (y_4 : square), | |
| (∃ (x_1 : square), | |
| (∃ (x_2 : square), | |
| (∃ (x_3 : square), | |
| is_solved y y_1 y_2 x y_3 y_4 x_1 x_2 x_3 ∧ | |
| ∀ (y_5 : square), | |
| is_solved y y_1 y_2 x y_3 y_4 x_1 x_2 y_5 → | |
| y_5 = x_3) ∧ | |
| ∀ (y_5 : square), | |
| (∃ (x_2 : square), | |
| is_solved y y_1 y_2 x y_3 y_4 x_1 y_5 x_2 ∧ | |
| ∀ (y_6 : square), | |
| is_solved y y_1 y_2 x y_3 y_4 x_1 y_5 y_6 → | |
| y_6 = x_2) → | |
| y_5 = x_2) ∧ | |
| ∀ (y_5 : square), | |
| (∃ (x_1 : square), | |
| (∃ (x_2 : square), | |
| is_solved y y_1 y_2 x y_3 y_4 y_5 x_1 x_2 ∧ | |
| ∀ (y_6 : square), | |
| is_solved y y_1 y_2 x y_3 y_4 y_5 x_1 y_6 → | |
| y_6 = x_2) ∧ | |
| ∀ (y_6 : square), | |
| (∃ (x_1 : square), | |
| is_solved y y_1 y_2 x y_3 y_4 y_5 y_6 x_1 ∧ | |
| ∀ (y_7 : square), | |
| is_solved y y_1 y_2 x y_3 y_4 y_5 y_6 y_7 → | |
| y_7 = x_1) → | |
| y_6 = x_1) → | |
| y_5 = x_1) → | |
| y_4 = x_1) → | |
| y_3 = x_1) ∧ | |
| ∀ (y_3 : square), | |
| (∃ (x : square), | |
| (∃ (x_1 : square), | |
| (∃ (x_2 : square), | |
| (∃ (x_3 : square), | |
| (∃ (x_4 : square), | |
| is_solved y y_1 y_2 y_3 x x_1 x_2 x_3 x_4 ∧ | |
| ∀ (y_4 : square), | |
| is_solved y y_1 y_2 y_3 x x_1 x_2 x_3 y_4 → y_4 = x_4) ∧ | |
| ∀ (y_4 : square), | |
| (∃ (x_3 : square), | |
| is_solved y y_1 y_2 y_3 x x_1 x_2 y_4 x_3 ∧ | |
| ∀ (y_5 : square), | |
| is_solved y y_1 y_2 y_3 x x_1 x_2 y_4 y_5 → | |
| y_5 = x_3) → | |
| y_4 = x_3) ∧ | |
| ∀ (y_4 : square), | |
| (∃ (x_2 : square), | |
| (∃ (x_3 : square), | |
| is_solved y y_1 y_2 y_3 x x_1 y_4 x_2 x_3 ∧ | |
| ∀ (y_5 : square), | |
| is_solved y y_1 y_2 y_3 x x_1 y_4 x_2 y_5 → | |
| y_5 = x_3) ∧ | |
| ∀ (y_5 : square), | |
| (∃ (x_2 : square), | |
| is_solved y y_1 y_2 y_3 x x_1 y_4 y_5 x_2 ∧ | |
| ∀ (y_6 : square), | |
| is_solved y y_1 y_2 y_3 x x_1 y_4 y_5 y_6 → | |
| y_6 = x_2) → | |
| y_5 = x_2) → | |
| y_4 = x_2) ∧ | |
| ∀ (y_4 : square), | |
| (∃ (x_1 : square), | |
| (∃ (x_2 : square), | |
| (∃ (x_3 : square), | |
| is_solved y y_1 y_2 y_3 x y_4 x_1 x_2 x_3 ∧ | |
| ∀ (y_5 : square), | |
| is_solved y y_1 y_2 y_3 x y_4 x_1 x_2 y_5 → | |
| y_5 = x_3) ∧ | |
| ∀ (y_5 : square), | |
| (∃ (x_2 : square), | |
| is_solved y y_1 y_2 y_3 x y_4 x_1 y_5 x_2 ∧ | |
| ∀ (y_6 : square), | |
| is_solved y y_1 y_2 y_3 x y_4 x_1 y_5 y_6 → | |
| y_6 = x_2) → | |
| y_5 = x_2) ∧ | |
| ∀ (y_5 : square), | |
| (∃ (x_1 : square), | |
| (∃ (x_2 : square), | |
| is_solved y y_1 y_2 y_3 x y_4 y_5 x_1 x_2 ∧ | |
| ∀ (y_6 : square), | |
| is_solved y y_1 y_2 y_3 x y_4 y_5 x_1 y_6 → | |
| y_6 = x_2) ∧ | |
| ∀ (y_6 : square), | |
| (∃ (x_1 : square), | |
| is_solved y y_1 y_2 y_3 x y_4 y_5 y_6 x_1 ∧ | |
| ∀ (y_7 : square), | |
| is_solved y y_1 y_2 y_3 x y_4 y_5 y_6 y_7 → | |
| y_7 = x_1) → | |
| y_6 = x_1) → | |
| y_5 = x_1) → | |
| y_4 = x_1) ∧ | |
| ∀ (y_4 : square), | |
| (∃ (x : square), | |
| (∃ (x_1 : square), | |
| (∃ (x_2 : square), | |
| (∃ (x_3 : square), | |
| is_solved y y_1 y_2 y_3 y_4 x x_1 x_2 x_3 ∧ | |
| ∀ (y_5 : square), | |
| is_solved y y_1 y_2 y_3 y_4 x x_1 x_2 y_5 → | |
| y_5 = x_3) ∧ | |
| ∀ (y_5 : square), | |
| (∃ (x_2 : square), | |
| is_solved y y_1 y_2 y_3 y_4 x x_1 y_5 x_2 ∧ | |
| ∀ (y_6 : square), | |
| is_solved y y_1 y_2 y_3 y_4 x x_1 y_5 y_6 → | |
| y_6 = x_2) → | |
| y_5 = x_2) ∧ | |
| ∀ (y_5 : square), | |
| (∃ (x_1 : square), | |
| (∃ (x_2 : square), | |
| is_solved y y_1 y_2 y_3 y_4 x y_5 x_1 x_2 ∧ | |
| ∀ (y_6 : square), | |
| is_solved y y_1 y_2 y_3 y_4 x y_5 x_1 y_6 → | |
| y_6 = x_2) ∧ | |
| ∀ (y_6 : square), | |
| (∃ (x_1 : square), | |
| is_solved y y_1 y_2 y_3 y_4 x y_5 y_6 x_1 ∧ | |
| ∀ (y_7 : square), | |
| is_solved y y_1 y_2 y_3 y_4 x y_5 y_6 y_7 → | |
| y_7 = x_1) → | |
| y_6 = x_1) → | |
| y_5 = x_1) ∧ | |
| ∀ (y_5 : square), | |
| (∃ (x : square), | |
| (∃ (x_1 : square), | |
| (∃ (x_2 : square), | |
| is_solved y y_1 y_2 y_3 y_4 y_5 x x_1 x_2 ∧ | |
| ∀ (y_6 : square), | |
| is_solved y y_1 y_2 y_3 y_4 y_5 x x_1 y_6 → | |
| y_6 = x_2) ∧ | |
| ∀ (y_6 : square), | |
| (∃ (x_1 : square), | |
| is_solved y y_1 y_2 y_3 y_4 y_5 x y_6 x_1 ∧ | |
| ∀ (y_7 : square), | |
| is_solved y y_1 y_2 y_3 y_4 y_5 x y_6 y_7 → | |
| y_7 = x_1) → | |
| y_6 = x_1) ∧ | |
| ∀ (y_6 : square), | |
| (∃ (x : square), | |
| (∃ (x_1 : square), | |
| is_solved y y_1 y_2 y_3 y_4 y_5 y_6 x x_1 ∧ | |
| ∀ (y_7 : square), | |
| is_solved y y_1 y_2 y_3 y_4 y_5 y_6 x y_7 → | |
| y_7 = x_1) ∧ | |
| ∀ (y_7 : square), | |
| (∃ (x : square), | |
| is_solved y y_1 y_2 y_3 y_4 y_5 y_6 y_7 x ∧ | |
| ∀ (y_8 : square), | |
| is_solved y y_1 y_2 y_3 y_4 y_5 y_6 y_7 y_8 → | |
| y_8 = x) → | |
| y_7 = x) → | |
| y_6 = x) → | |
| y_5 = x) → | |
| y_4 = x) → | |
| y_3 = x) → | |
| y_2 = x) → | |
| y_1 = x) → | |
| …) | |
| state: | |
| ⊢ ∃ (x : square), | |
| … ∧ | |
| ∀ (y : square), | |
| (∃ (x : square), | |
| (∃ (x_1 : square), | |
| … ∧ | |
| ∀ (y_1 : square), | |
| (∃ (x_1 : square), | |
| (∃ (x_2 : square), | |
| (∃ (x_3 : square), | |
| … ∧ | |
| ∀ (y_2 : square), | |
| (∃ (x_3 : square), | |
| … ∧ | |
| ∀ (y_3 : square), | |
| (∃ (x_3 : square), | |
| (∃ (x_4 : square), …) ∧ | |
| ∀ (y_4 : square), | |
| (∃ (x_3 : square), | |
| is_solved y x y_1 x_1 x_2 y_2 y_3 y_4 x_3 ∧ | |
| ∀ (y_5 : square), | |
| is_solved y x y_1 x_1 x_2 y_2 y_3 y_4 y_5 → y_5 = x_3) → | |
| y_4 = x_3) → | |
| …) → | |
| …) ∧ | |
| ∀ (y_2 : square), | |
| (∃ (x_2 : square), | |
| (∃ (x_3 : square), | |
| (∃ (x_4 : square), | |
| (∃ (x_5 : square), | |
| is_solved y x y_1 x_1 y_2 x_2 x_3 x_4 x_5 ∧ | |
| ∀ (y_3 : square), | |
| is_solved y x y_1 x_1 y_2 x_2 x_3 x_4 y_3 → y_3 = x_5) ∧ | |
| ∀ (y_3 : square), | |
| (∃ (x_4 : square), | |
| is_solved y x y_1 x_1 y_2 x_2 x_3 y_3 x_4 ∧ | |
| ∀ (y_4 : square), | |
| is_solved y x y_1 x_1 y_2 x_2 x_3 y_3 y_4 → y_4 = x_4) → | |
| y_3 = x_4) ∧ | |
| ∀ (y_3 : square), | |
| (∃ (x_3 : square), | |
| (∃ (x_4 : square), | |
| is_solved y x y_1 x_1 y_2 x_2 y_3 x_3 x_4 ∧ | |
| ∀ (y_4 : square), | |
| is_solved y x y_1 x_1 y_2 x_2 y_3 x_3 y_4 → y_4 = x_4) ∧ | |
| ∀ (y_4 : square), | |
| (∃ (x_3 : square), | |
| is_solved y x y_1 x_1 y_2 x_2 y_3 y_4 x_3 ∧ | |
| ∀ (y_5 : square), | |
| is_solved y x y_1 x_1 y_2 x_2 y_3 y_4 y_5 → y_5 = x_3) → | |
| y_4 = x_3) → | |
| y_3 = x_3) ∧ | |
| ∀ (y_3 : square), | |
| (∃ (x_2 : square), | |
| (∃ (x_3 : square), | |
| (∃ (x_4 : square), | |
| is_solved y x y_1 x_1 y_2 y_3 x_2 x_3 x_4 ∧ | |
| ∀ (y_4 : square), | |
| is_solved y x y_1 x_1 y_2 y_3 x_2 x_3 y_4 → y_4 = x_4) ∧ | |
| ∀ (y_4 : square), | |
| (∃ (x_3 : square), | |
| is_solved y x y_1 x_1 y_2 y_3 x_2 y_4 x_3 ∧ | |
| ∀ (y_5 : square), | |
| is_solved y x y_1 x_1 y_2 y_3 x_2 y_4 y_5 → y_5 = x_3) → | |
| y_4 = x_3) ∧ | |
| ∀ (y_4 : square), | |
| (∃ (x_2 : square), | |
| (∃ (x_3 : square), | |
| is_solved y x y_1 x_1 y_2 y_3 y_4 x_2 x_3 ∧ | |
| ∀ (y_5 : square), | |
| is_solved y x y_1 x_1 y_2 y_3 y_4 x_2 y_5 → y_5 = x_3) ∧ | |
| ∀ (y_5 : square), | |
| (∃ (x_2 : square), | |
| is_solved y x y_1 x_1 y_2 y_3 y_4 y_5 x_2 ∧ | |
| ∀ (y_6 : square), | |
| is_solved y x y_1 x_1 y_2 y_3 y_4 y_5 y_6 → y_6 = x_2) → | |
| y_5 = x_2) → | |
| y_4 = x_2) → | |
| y_3 = x_2) → | |
| y_2 = x_2) ∧ | |
| ∀ (y_2 : square), | |
| (∃ (x_1 : square), | |
| (∃ (x_2 : square), | |
| (∃ (x_3 : square), | |
| (∃ (x_4 : square), | |
| (∃ (x_5 : square), | |
| is_solved y x y_1 y_2 x_1 x_2 x_3 x_4 x_5 ∧ | |
| ∀ (y_3 : square), | |
| is_solved y x y_1 y_2 x_1 x_2 x_3 x_4 y_3 → y_3 = x_5) ∧ | |
| ∀ (y_3 : square), | |
| (∃ (x_4 : square), | |
| is_solved y x y_1 y_2 x_1 x_2 x_3 y_3 x_4 ∧ | |
| ∀ (y_4 : square), | |
| is_solved y x y_1 y_2 x_1 x_2 x_3 y_3 y_4 → y_4 = x_4) → | |
| y_3 = x_4) ∧ | |
| ∀ (y_3 : square), | |
| (∃ (x_3 : square), | |
| (∃ (x_4 : square), | |
| is_solved y x y_1 y_2 x_1 x_2 y_3 x_3 x_4 ∧ | |
| ∀ (y_4 : square), | |
| is_solved y x y_1 y_2 x_1 x_2 y_3 x_3 y_4 → y_4 = x_4) ∧ | |
| ∀ (y_4 : square), | |
| (∃ (x_3 : square), | |
| is_solved y x y_1 y_2 x_1 x_2 y_3 y_4 x_3 ∧ | |
| ∀ (y_5 : square), | |
| is_solved y x y_1 y_2 x_1 x_2 y_3 y_4 y_5 → y_5 = x_3) → | |
| y_4 = x_3) → | |
| y_3 = x_3) ∧ | |
| ∀ (y_3 : square), | |
| (∃ (x_2 : square), | |
| (∃ (x_3 : square), | |
| (∃ (x_4 : square), | |
| is_solved y x y_1 y_2 x_1 y_3 x_2 x_3 x_4 ∧ | |
| ∀ (y_4 : square), | |
| is_solved y x y_1 y_2 x_1 y_3 x_2 x_3 y_4 → y_4 = x_4) ∧ | |
| ∀ (y_4 : square), | |
| (∃ (x_3 : square), | |
| is_solved y x y_1 y_2 x_1 y_3 x_2 y_4 x_3 ∧ | |
| ∀ (y_5 : square), | |
| is_solved y x y_1 y_2 x_1 y_3 x_2 y_4 y_5 → y_5 = x_3) → | |
| y_4 = x_3) ∧ | |
| ∀ (y_4 : square), | |
| (∃ (x_2 : square), | |
| (∃ (x_3 : square), | |
| is_solved y x y_1 y_2 x_1 y_3 y_4 x_2 x_3 ∧ | |
| ∀ (y_5 : square), | |
| is_solved y x y_1 y_2 x_1 y_3 y_4 x_2 y_5 → y_5 = x_3) ∧ | |
| ∀ (y_5 : square), | |
| (∃ (x_2 : square), | |
| is_solved y x y_1 y_2 x_1 y_3 y_4 y_5 x_2 ∧ | |
| ∀ (y_6 : square), | |
| is_solved y x y_1 y_2 x_1 y_3 y_4 y_5 y_6 → y_6 = x_2) → | |
| y_5 = x_2) → | |
| y_4 = x_2) → | |
| y_3 = x_2) ∧ | |
| ∀ (y_3 : square), | |
| (∃ (x_1 : square), | |
| (∃ (x_2 : square), | |
| (∃ (x_3 : square), | |
| (∃ (x_4 : square), | |
| is_solved y x y_1 y_2 y_3 x_1 x_2 x_3 x_4 ∧ | |
| ∀ (y_4 : square), | |
| is_solved y x y_1 y_2 y_3 x_1 x_2 x_3 y_4 → y_4 = x_4) ∧ | |
| ∀ (y_4 : square), | |
| (∃ (x_3 : square), | |
| is_solved y x y_1 y_2 y_3 x_1 x_2 y_4 x_3 ∧ | |
| ∀ (y_5 : square), | |
| is_solved y x y_1 y_2 y_3 x_1 x_2 y_4 y_5 → y_5 = x_3) → | |
| y_4 = x_3) ∧ | |
| ∀ (y_4 : square), | |
| (∃ (x_2 : square), | |
| (∃ (x_3 : square), | |
| is_solved y x y_1 y_2 y_3 x_1 y_4 x_2 x_3 ∧ | |
| ∀ (y_5 : square), | |
| is_solved y x y_1 y_2 y_3 x_1 y_4 x_2 y_5 → y_5 = x_3) ∧ | |
| ∀ (y_5 : square), | |
| (∃ (x_2 : square), | |
| is_solved y x y_1 y_2 y_3 x_1 y_4 y_5 x_2 ∧ | |
| ∀ (y_6 : square), | |
| is_solved y x y_1 y_2 y_3 x_1 y_4 y_5 y_6 → y_6 = x_2) → | |
| y_5 = x_2) → | |
| y_4 = x_2) ∧ | |
| ∀ (y_4 : square), | |
| (∃ (x_1 : square), | |
| (∃ (x_2 : square), | |
| (∃ (x_3 : square), | |
| is_solved y x y_1 y_2 y_3 y_4 x_1 x_2 x_3 ∧ | |
| ∀ (y_5 : square), | |
| is_solved y x y_1 y_2 y_3 y_4 x_1 x_2 y_5 → y_5 = x_3) ∧ | |
| ∀ (y_5 : square), | |
| (∃ (x_2 : square), | |
| is_solved y x y_1 y_2 y_3 y_4 x_1 y_5 x_2 ∧ | |
| ∀ (y_6 : square), | |
| is_solved y x y_1 y_2 y_3 y_4 x_1 y_5 y_6 → y_6 = x_2) → | |
| y_5 = x_2) ∧ | |
| ∀ (y_5 : square), | |
| (∃ (x_1 : square), | |
| (∃ (x_2 : square), | |
| is_solved y x y_1 y_2 y_3 y_4 y_5 x_1 x_2 ∧ | |
| ∀ (y_6 : square), | |
| is_solved y x y_1 y_2 y_3 y_4 y_5 x_1 y_6 → y_6 = x_2) ∧ | |
| ∀ (y_6 : square), | |
| (∃ (x_1 : square), | |
| is_solved y x y_1 y_2 y_3 y_4 y_5 y_6 x_1 ∧ | |
| ∀ (y_7 : square), | |
| is_solved y x y_1 y_2 y_3 y_4 y_5 y_6 y_7 → | |
| y_7 = x_1) → | |
| y_6 = x_1) → | |
| y_5 = x_1) → | |
| y_4 = x_1) → | |
| y_3 = x_1) → | |
| y_2 = x_1) → | |
| …) ∧ | |
| ∀ (y_1 : square), | |
| (∃ (x : square), | |
| (∃ (x_1 : square), | |
| (∃ (x_2 : square), | |
| (∃ (x_3 : square), | |
| (∃ (x_4 : square), | |
| (∃ (x_5 : square), | |
| (∃ (x_6 : square), | |
| is_solved y y_1 x x_1 x_2 x_3 x_4 x_5 x_6 ∧ | |
| ∀ (y_2 : square), | |
| is_solved y y_1 x x_1 x_2 x_3 x_4 x_5 y_2 → y_2 = x_6) ∧ | |
| ∀ (y_2 : square), | |
| (∃ (x_5 : square), | |
| is_solved y y_1 x x_1 x_2 x_3 x_4 y_2 x_5 ∧ | |
| ∀ (y_3 : square), | |
| is_solved y y_1 x x_1 x_2 x_3 x_4 y_2 y_3 → y_3 = x_5) → | |
| y_2 = x_5) ∧ | |
| ∀ (y_2 : square), | |
| (∃ (x_4 : square), | |
| (∃ (x_5 : square), | |
| is_solved y y_1 x x_1 x_2 x_3 y_2 x_4 x_5 ∧ | |
| ∀ (y_3 : square), | |
| is_solved y y_1 x x_1 x_2 x_3 y_2 x_4 y_3 → y_3 = x_5) ∧ | |
| ∀ (y_3 : square), | |
| (∃ (x_4 : square), | |
| is_solved y y_1 x x_1 x_2 x_3 y_2 y_3 x_4 ∧ | |
| ∀ (y_4 : square), | |
| is_solved y y_1 x x_1 x_2 x_3 y_2 y_3 y_4 → y_4 = x_4) → | |
| y_3 = x_4) → | |
| y_2 = x_4) ∧ | |
| ∀ (y_2 : square), | |
| (∃ (x_3 : square), | |
| (∃ (x_4 : square), | |
| (∃ (x_5 : square), | |
| is_solved y y_1 x x_1 x_2 y_2 x_3 x_4 x_5 ∧ | |
| ∀ (y_3 : square), | |
| is_solved y y_1 x x_1 x_2 y_2 x_3 x_4 y_3 → y_3 = x_5) ∧ | |
| ∀ (y_3 : square), | |
| (∃ (x_4 : square), | |
| is_solved y y_1 x x_1 x_2 y_2 x_3 y_3 x_4 ∧ | |
| ∀ (y_4 : square), | |
| is_solved y y_1 x x_1 x_2 y_2 x_3 y_3 y_4 → y_4 = x_4) → | |
| y_3 = x_4) ∧ | |
| ∀ (y_3 : square), | |
| (∃ (x_3 : square), | |
| (∃ (x_4 : square), | |
| is_solved y y_1 x x_1 x_2 y_2 y_3 x_3 x_4 ∧ | |
| ∀ (y_4 : square), | |
| is_solved y y_1 x x_1 x_2 y_2 y_3 x_3 y_4 → y_4 = x_4) ∧ | |
| ∀ (y_4 : square), | |
| (∃ (x_3 : square), | |
| is_solved y y_1 x x_1 x_2 y_2 y_3 y_4 x_3 ∧ | |
| ∀ (y_5 : square), | |
| is_solved y y_1 x x_1 x_2 y_2 y_3 y_4 y_5 → y_5 = x_3) → | |
| y_4 = x_3) → | |
| y_3 = x_3) → | |
| y_2 = x_3) ∧ | |
| ∀ (y_2 : square), | |
| (∃ (x_2 : square), | |
| (∃ (x_3 : square), | |
| (∃ (x_4 : square), | |
| (∃ (x_5 : square), | |
| is_solved y y_1 x x_1 y_2 x_2 x_3 x_4 x_5 ∧ | |
| ∀ (y_3 : square), | |
| is_solved y y_1 x x_1 y_2 x_2 x_3 x_4 y_3 → y_3 = x_5) ∧ | |
| ∀ (y_3 : square), | |
| (∃ (x_4 : square), | |
| is_solved y y_1 x x_1 y_2 x_2 x_3 y_3 x_4 ∧ | |
| ∀ (y_4 : square), | |
| is_solved y y_1 x x_1 y_2 x_2 x_3 y_3 y_4 → y_4 = x_4) → | |
| y_3 = x_4) ∧ | |
| ∀ (y_3 : square), | |
| (∃ (x_3 : square), | |
| (∃ (x_4 : square), | |
| is_solved y y_1 x x_1 y_2 x_2 y_3 x_3 x_4 ∧ | |
| ∀ (y_4 : square), | |
| is_solved y y_1 x x_1 y_2 x_2 y_3 x_3 y_4 → y_4 = x_4) ∧ | |
| ∀ (y_4 : square), | |
| (∃ (x_3 : square), | |
| is_solved y y_1 x x_1 y_2 x_2 y_3 y_4 x_3 ∧ | |
| ∀ (y_5 : square), | |
| is_solved y y_1 x x_1 y_2 x_2 y_3 y_4 y_5 → y_5 = x_3) → | |
| y_4 = x_3) → | |
| y_3 = x_3) ∧ | |
| ∀ (y_3 : square), | |
| (∃ (x_2 : square), | |
| (∃ (x_3 : square), | |
| (∃ (x_4 : square), | |
| is_solved y y_1 x x_1 y_2 y_3 x_2 x_3 x_4 ∧ | |
| ∀ (y_4 : square), | |
| is_solved y y_1 x x_1 y_2 y_3 x_2 x_3 y_4 → y_4 = x_4) ∧ | |
| ∀ (y_4 : square), | |
| (∃ (x_3 : square), | |
| is_solved y y_1 x x_1 y_2 y_3 x_2 y_4 x_3 ∧ | |
| ∀ (y_5 : square), | |
| is_solved y y_1 x x_1 y_2 y_3 x_2 y_4 y_5 → y_5 = x_3) → | |
| y_4 = x_3) ∧ | |
| ∀ (y_4 : square), | |
| (∃ (x_2 : square), | |
| (∃ (x_3 : square), | |
| is_solved y y_1 x x_1 y_2 y_3 y_4 x_2 x_3 ∧ | |
| ∀ (y_5 : square), | |
| is_solved y y_1 x x_1 y_2 y_3 y_4 x_2 y_5 → y_5 = x_3) ∧ | |
| ∀ (y_5 : square), | |
| (∃ (x_2 : square), | |
| is_solved y y_1 x x_1 y_2 y_3 y_4 y_5 x_2 ∧ | |
| ∀ (y_6 : square), | |
| is_solved y y_1 x x_1 y_2 y_3 y_4 y_5 y_6 → y_6 = x_2) → | |
| y_5 = x_2) → | |
| y_4 = x_2) → | |
| y_3 = x_2) → | |
| y_2 = x_2) ∧ | |
| ∀ (y_2 : square), | |
| (∃ (x_1 : square), | |
| (∃ (x_2 : square), | |
| (∃ (x_3 : square), | |
| (∃ (x_4 : square), | |
| (∃ (x_5 : square), | |
| is_solved y y_1 x y_2 x_1 x_2 x_3 x_4 x_5 ∧ | |
| ∀ (y_3 : square), | |
| is_solved y y_1 x y_2 x_1 x_2 x_3 x_4 y_3 → y_3 = x_5) ∧ | |
| ∀ (y_3 : square), | |
| (∃ (x_4 : square), | |
| is_solved y y_1 x y_2 x_1 x_2 x_3 y_3 x_4 ∧ | |
| ∀ (y_4 : square), | |
| is_solved y y_1 x y_2 x_1 x_2 x_3 y_3 y_4 → y_4 = x_4) → | |
| y_3 = x_4) ∧ | |
| ∀ (y_3 : square), | |
| (∃ (x_3 : square), | |
| (∃ (x_4 : square), | |
| is_solved y y_1 x y_2 x_1 x_2 y_3 x_3 x_4 ∧ | |
| ∀ (y_4 : square), | |
| is_solved y y_1 x y_2 x_1 x_2 y_3 x_3 y_4 → y_4 = x_4) ∧ | |
| ∀ (y_4 : square), | |
| (∃ (x_3 : square), | |
| is_solved y y_1 x y_2 x_1 x_2 y_3 y_4 x_3 ∧ | |
| ∀ (y_5 : square), | |
| is_solved y y_1 x y_2 x_1 x_2 y_3 y_4 y_5 → y_5 = x_3) → | |
| y_4 = x_3) → | |
| y_3 = x_3) ∧ | |
| ∀ (y_3 : square), | |
| (∃ (x_2 : square), | |
| (∃ (x_3 : square), | |
| (∃ (x_4 : square), | |
| is_solved y y_1 x y_2 x_1 y_3 x_2 x_3 x_4 ∧ | |
| ∀ (y_4 : square), | |
| is_solved y y_1 x y_2 x_1 y_3 x_2 x_3 y_4 → y_4 = x_4) ∧ | |
| ∀ (y_4 : square), | |
| (∃ (x_3 : square), | |
| is_solved y y_1 x y_2 x_1 y_3 x_2 y_4 x_3 ∧ | |
| ∀ (y_5 : square), | |
| is_solved y y_1 x y_2 x_1 y_3 x_2 y_4 y_5 → y_5 = x_3) → | |
| y_4 = x_3) ∧ | |
| ∀ (y_4 : square), | |
| (∃ (x_2 : square), | |
| (∃ (x_3 : square), | |
| is_solved y y_1 x y_2 x_1 y_3 y_4 x_2 x_3 ∧ | |
| ∀ (y_5 : square), | |
| is_solved y y_1 x y_2 x_1 y_3 y_4 x_2 y_5 → y_5 = x_3) ∧ | |
| ∀ (y_5 : square), | |
| (∃ (x_2 : square), | |
| is_solved y y_1 x y_2 x_1 y_3 y_4 y_5 x_2 ∧ | |
| ∀ (y_6 : square), | |
| is_solved y y_1 x y_2 x_1 y_3 y_4 y_5 y_6 → y_6 = x_2) → | |
| y_5 = x_2) → | |
| y_4 = x_2) → | |
| y_3 = x_2) ∧ | |
| ∀ (y_3 : square), | |
| (∃ (x_1 : square), | |
| (∃ (x_2 : square), | |
| (∃ (x_3 : square), | |
| (∃ (x_4 : square), | |
| is_solved y y_1 x y_2 y_3 x_1 x_2 x_3 x_4 ∧ | |
| ∀ (y_4 : square), | |
| is_solved y y_1 x y_2 y_3 x_1 x_2 x_3 y_4 → y_4 = x_4) ∧ | |
| ∀ (y_4 : square), | |
| (∃ (x_3 : square), | |
| is_solved y y_1 x y_2 y_3 x_1 x_2 y_4 x_3 ∧ | |
| ∀ (y_5 : square), | |
| is_solved y y_1 x y_2 y_3 x_1 x_2 y_4 y_5 → y_5 = x_3) → | |
| y_4 = x_3) ∧ | |
| ∀ (y_4 : square), | |
| (∃ (x_2 : square), | |
| (∃ (x_3 : square), | |
| is_solved y y_1 x y_2 y_3 x_1 y_4 x_2 x_3 ∧ | |
| ∀ (y_5 : square), | |
| is_solved y y_1 x y_2 y_3 x_1 y_4 x_2 y_5 → y_5 = x_3) ∧ | |
| ∀ (y_5 : square), | |
| (∃ (x_2 : square), | |
| is_solved y y_1 x y_2 y_3 x_1 y_4 y_5 x_2 ∧ | |
| ∀ (y_6 : square), | |
| is_solved y y_1 x y_2 y_3 x_1 y_4 y_5 y_6 → y_6 = x_2) → | |
| y_5 = x_2) → | |
| y_4 = x_2) ∧ | |
| ∀ (y_4 : square), | |
| (∃ (x_1 : square), | |
| (∃ (x_2 : square), | |
| (∃ (x_3 : square), | |
| is_solved y y_1 x y_2 y_3 y_4 x_1 x_2 x_3 ∧ | |
| ∀ (y_5 : square), | |
| is_solved y y_1 x y_2 y_3 y_4 x_1 x_2 y_5 → y_5 = x_3) ∧ | |
| ∀ (y_5 : square), | |
| (∃ (x_2 : square), | |
| is_solved y y_1 x y_2 y_3 y_4 x_1 y_5 x_2 ∧ | |
| ∀ (y_6 : square), | |
| is_solved y y_1 x y_2 y_3 y_4 x_1 y_5 y_6 → y_6 = x_2) → | |
| y_5 = x_2) ∧ | |
| ∀ (y_5 : square), | |
| (∃ (x_1 : square), | |
| (∃ (x_2 : square), | |
| is_solved y y_1 x y_2 y_3 y_4 y_5 x_1 x_2 ∧ | |
| ∀ (y_6 : square), | |
| is_solved y y_1 x y_2 y_3 y_4 y_5 x_1 y_6 → y_6 = x_2) ∧ | |
| ∀ (y_6 : square), | |
| (∃ (x_1 : square), | |
| is_solved y y_1 x y_2 y_3 y_4 y_5 y_6 x_1 ∧ | |
| ∀ (y_7 : square), | |
| is_solved y y_1 x y_2 y_3 y_4 y_5 y_6 y_7 → | |
| y_7 = x_1) → | |
| y_6 = x_1) → | |
| y_5 = x_1) → | |
| y_4 = x_1) → | |
| y_3 = x_1) → | |
| y_2 = x_1) ∧ | |
| ∀ (y_2 : square), | |
| (∃ (x : square), | |
| (∃ (x_1 : square), | |
| (∃ (x_2 : square), | |
| (∃ (x_3 : square), | |
| (∃ (x_4 : square), | |
| (∃ (x_5 : square), | |
| is_solved y y_1 y_2 x x_1 x_2 x_3 x_4 x_5 ∧ | |
| ∀ (y_3 : square), | |
| is_solved y y_1 y_2 x x_1 x_2 x_3 x_4 y_3 → y_3 = x_5) ∧ | |
| ∀ (y_3 : square), | |
| (∃ (x_4 : square), | |
| is_solved y y_1 y_2 x x_1 x_2 x_3 y_3 x_4 ∧ | |
| ∀ (y_4 : square), | |
| is_solved y y_1 y_2 x x_1 x_2 x_3 y_3 y_4 → y_4 = x_4) → | |
| y_3 = x_4) ∧ | |
| ∀ (y_3 : square), | |
| (∃ (x_3 : square), | |
| (∃ (x_4 : square), | |
| is_solved y y_1 y_2 x x_1 x_2 y_3 x_3 x_4 ∧ | |
| ∀ (y_4 : square), | |
| is_solved y y_1 y_2 x x_1 x_2 y_3 x_3 y_4 → y_4 = x_4) ∧ | |
| ∀ (y_4 : square), | |
| (∃ (x_3 : square), | |
| is_solved y y_1 y_2 x x_1 x_2 y_3 y_4 x_3 ∧ | |
| ∀ (y_5 : square), | |
| is_solved y y_1 y_2 x x_1 x_2 y_3 y_4 y_5 → y_5 = x_3) → | |
| y_4 = x_3) → | |
| y_3 = x_3) ∧ | |
| ∀ (y_3 : square), | |
| (∃ (x_2 : square), | |
| (∃ (x_3 : square), | |
| (∃ (x_4 : square), | |
| is_solved y y_1 y_2 x x_1 y_3 x_2 x_3 x_4 ∧ | |
| ∀ (y_4 : square), | |
| is_solved y y_1 y_2 x x_1 y_3 x_2 x_3 y_4 → y_4 = x_4) ∧ | |
| ∀ (y_4 : square), | |
| (∃ (x_3 : square), | |
| is_solved y y_1 y_2 x x_1 y_3 x_2 y_4 x_3 ∧ | |
| ∀ (y_5 : square), | |
| is_solved y y_1 y_2 x x_1 y_3 x_2 y_4 y_5 → y_5 = x_3) → | |
| y_4 = x_3) ∧ | |
| ∀ (y_4 : square), | |
| (∃ (x_2 : square), | |
| (∃ (x_3 : square), | |
| is_solved y y_1 y_2 x x_1 y_3 y_4 x_2 x_3 ∧ | |
| ∀ (y_5 : square), | |
| is_solved y y_1 y_2 x x_1 y_3 y_4 x_2 y_5 → y_5 = x_3) ∧ | |
| ∀ (y_5 : square), | |
| (∃ (x_2 : square), | |
| is_solved y y_1 y_2 x x_1 y_3 y_4 y_5 x_2 ∧ | |
| ∀ (y_6 : square), | |
| is_solved y y_1 y_2 x x_1 y_3 y_4 y_5 y_6 → y_6 = x_2) → | |
| y_5 = x_2) → | |
| y_4 = x_2) → | |
| y_3 = x_2) ∧ | |
| ∀ (y_3 : square), | |
| (∃ (x_1 : square), | |
| (∃ (x_2 : square), | |
| (∃ (x_3 : square), | |
| (∃ (x_4 : square), | |
| is_solved y y_1 y_2 x y_3 x_1 x_2 x_3 x_4 ∧ | |
| ∀ (y_4 : square), | |
| is_solved y y_1 y_2 x y_3 x_1 x_2 x_3 y_4 → y_4 = x_4) ∧ | |
| ∀ (y_4 : square), | |
| (∃ (x_3 : square), | |
| is_solved y y_1 y_2 x y_3 x_1 x_2 y_4 x_3 ∧ | |
| ∀ (y_5 : square), | |
| is_solved y y_1 y_2 x y_3 x_1 x_2 y_4 y_5 → y_5 = x_3) → | |
| y_4 = x_3) ∧ | |
| ∀ (y_4 : square), | |
| (∃ (x_2 : square), | |
| (∃ (x_3 : square), | |
| is_solved y y_1 y_2 x y_3 x_1 y_4 x_2 x_3 ∧ | |
| ∀ (y_5 : square), | |
| is_solved y y_1 y_2 x y_3 x_1 y_4 x_2 y_5 → y_5 = x_3) ∧ | |
| ∀ (y_5 : square), | |
| (∃ (x_2 : square), | |
| is_solved y y_1 y_2 x y_3 x_1 y_4 y_5 x_2 ∧ | |
| ∀ (y_6 : square), | |
| is_solved y y_1 y_2 x y_3 x_1 y_4 y_5 y_6 → y_6 = x_2) → | |
| y_5 = x_2) → | |
| y_4 = x_2) ∧ | |
| ∀ (y_4 : square), | |
| (∃ (x_1 : square), | |
| (∃ (x_2 : square), | |
| (∃ (x_3 : square), | |
| is_solved y y_1 y_2 x y_3 y_4 x_1 x_2 x_3 ∧ | |
| ∀ (y_5 : square), | |
| is_solved y y_1 y_2 x y_3 y_4 x_1 x_2 y_5 → y_5 = x_3) ∧ | |
| ∀ (y_5 : square), | |
| (∃ (x_2 : square), | |
| is_solved y y_1 y_2 x y_3 y_4 x_1 y_5 x_2 ∧ | |
| ∀ (y_6 : square), | |
| is_solved y y_1 y_2 x y_3 y_4 x_1 y_5 y_6 → y_6 = x_2) → | |
| y_5 = x_2) ∧ | |
| ∀ (y_5 : square), | |
| (∃ (x_1 : square), | |
| (∃ (x_2 : square), | |
| is_solved y y_1 y_2 x y_3 y_4 y_5 x_1 x_2 ∧ | |
| ∀ (y_6 : square), | |
| is_solved y y_1 y_2 x y_3 y_4 y_5 x_1 y_6 → y_6 = x_2) ∧ | |
| ∀ (y_6 : square), | |
| (∃ (x_1 : square), | |
| is_solved y y_1 y_2 x y_3 y_4 y_5 y_6 x_1 ∧ | |
| ∀ (y_7 : square), | |
| is_solved y y_1 y_2 x y_3 y_4 y_5 y_6 y_7 → | |
| y_7 = x_1) → | |
| y_6 = x_1) → | |
| y_5 = x_1) → | |
| y_4 = x_1) → | |
| y_3 = x_1) ∧ | |
| ∀ (y_3 : square), | |
| (∃ (x : square), | |
| (∃ (x_1 : square), | |
| (∃ (x_2 : square), | |
| (∃ (x_3 : square), | |
| (∃ (x_4 : square), | |
| is_solved y y_1 y_2 y_3 x x_1 x_2 x_3 x_4 ∧ | |
| ∀ (y_4 : square), | |
| is_solved y y_1 y_2 y_3 x x_1 x_2 x_3 y_4 → y_4 = x_4) ∧ | |
| ∀ (y_4 : square), | |
| (∃ (x_3 : square), | |
| is_solved y y_1 y_2 y_3 x x_1 x_2 y_4 x_3 ∧ | |
| ∀ (y_5 : square), | |
| is_solved y y_1 y_2 y_3 x x_1 x_2 y_4 y_5 → y_5 = x_3) → | |
| y_4 = x_3) ∧ | |
| ∀ (y_4 : square), | |
| (∃ (x_2 : square), | |
| (∃ (x_3 : square), | |
| is_solved y y_1 y_2 y_3 x x_1 y_4 x_2 x_3 ∧ | |
| ∀ (y_5 : square), | |
| is_solved y y_1 y_2 y_3 x x_1 y_4 x_2 y_5 → y_5 = x_3) ∧ | |
| ∀ (y_5 : square), | |
| (∃ (x_2 : square), | |
| is_solved y y_1 y_2 y_3 x x_1 y_4 y_5 x_2 ∧ | |
| ∀ (y_6 : square), | |
| is_solved y y_1 y_2 y_3 x x_1 y_4 y_5 y_6 → y_6 = x_2) → | |
| y_5 = x_2) → | |
| y_4 = x_2) ∧ | |
| ∀ (y_4 : square), | |
| (∃ (x_1 : square), | |
| (∃ (x_2 : square), | |
| (∃ (x_3 : square), | |
| is_solved y y_1 y_2 y_3 x y_4 x_1 x_2 x_3 ∧ | |
| ∀ (y_5 : square), | |
| is_solved y y_1 y_2 y_3 x y_4 x_1 x_2 y_5 → y_5 = x_3) ∧ | |
| ∀ (y_5 : square), | |
| (∃ (x_2 : square), | |
| is_solved y y_1 y_2 y_3 x y_4 x_1 y_5 x_2 ∧ | |
| ∀ (y_6 : square), | |
| is_solved y y_1 y_2 y_3 x y_4 x_1 y_5 y_6 → y_6 = x_2) → | |
| y_5 = x_2) ∧ | |
| ∀ (y_5 : square), | |
| (∃ (x_1 : square), | |
| (∃ (x_2 : square), | |
| is_solved y y_1 y_2 y_3 x y_4 y_5 x_1 x_2 ∧ | |
| ∀ (y_6 : square), | |
| is_solved y y_1 y_2 y_3 x y_4 y_5 x_1 y_6 → y_6 = x_2) ∧ | |
| ∀ (y_6 : square), | |
| (∃ (x_1 : square), | |
| is_solved y y_1 y_2 y_3 x y_4 y_5 y_6 x_1 ∧ | |
| ∀ (y_7 : square), | |
| is_solved y y_1 y_2 y_3 x y_4 y_5 y_6 y_7 → | |
| y_7 = x_1) → | |
| y_6 = x_1) → | |
| y_5 = x_1) → | |
| y_4 = x_1) ∧ | |
| ∀ (y_4 : square), | |
| (∃ (x : square), | |
| (∃ (x_1 : square), | |
| (∃ (x_2 : square), | |
| (∃ (x_3 : square), | |
| is_solved y y_1 y_2 y_3 y_4 x x_1 x_2 x_3 ∧ | |
| ∀ (y_5 : square), | |
| is_solved y y_1 y_2 y_3 y_4 x x_1 x_2 y_5 → y_5 = x_3) ∧ | |
| ∀ (y_5 : square), | |
| (∃ (x_2 : square), | |
| is_solved y y_1 y_2 y_3 y_4 x x_1 y_5 x_2 ∧ | |
| ∀ (y_6 : square), | |
| is_solved y y_1 y_2 y_3 y_4 x x_1 y_5 y_6 → y_6 = x_2) → | |
| y_5 = x_2) ∧ | |
| ∀ (y_5 : square), | |
| (∃ (x_1 : square), | |
| (∃ (x_2 : square), | |
| is_solved y y_1 y_2 y_3 y_4 x y_5 x_1 x_2 ∧ | |
| ∀ (y_6 : square), | |
| is_solved y y_1 y_2 y_3 y_4 x y_5 x_1 y_6 → y_6 = x_2) ∧ | |
| ∀ (y_6 : square), | |
| (∃ (x_1 : square), | |
| is_solved y y_1 y_2 y_3 y_4 x y_5 y_6 x_1 ∧ | |
| ∀ (y_7 : square), | |
| is_solved y y_1 y_2 y_3 y_4 x y_5 y_6 y_7 → | |
| y_7 = x_1) → | |
| y_6 = x_1) → | |
| y_5 = x_1) ∧ | |
| ∀ (y_5 : square), | |
| (∃ (x : square), | |
| (∃ (x_1 : square), | |
| (∃ (x_2 : square), | |
| is_solved y y_1 y_2 y_3 y_4 y_5 x x_1 x_2 ∧ | |
| ∀ (y_6 : square), | |
| is_solved y y_1 y_2 y_3 y_4 y_5 x x_1 y_6 → y_6 = x_2) ∧ | |
| ∀ (y_6 : square), | |
| (∃ (x_1 : square), | |
| is_solved y y_1 y_2 y_3 y_4 y_5 x y_6 x_1 ∧ | |
| ∀ (y_7 : square), | |
| is_solved y y_1 y_2 y_3 y_4 y_5 x y_6 y_7 → | |
| y_7 = x_1) → | |
| y_6 = x_1) ∧ | |
| ∀ (y_6 : square), | |
| (∃ (x : square), | |
| (∃ (x_1 : square), | |
| is_solved y y_1 y_2 y_3 y_4 y_5 y_6 x x_1 ∧ | |
| ∀ (y_7 : square), | |
| is_solved y y_1 y_2 y_3 y_4 y_5 y_6 x y_7 → | |
| y_7 = x_1) ∧ | |
| ∀ (y_7 : square), | |
| (∃ (x : square), | |
| is_solved y y_1 y_2 y_3 y_4 y_5 y_6 y_7 x ∧ | |
| ∀ (y_8 : square), | |
| is_solved y y_1 y_2 y_3 y_4 y_5 y_6 y_7 y_8 → | |
| y_8 = x) → | |
| y_7 = x) → | |
| y_6 = x) → | |
| y_5 = x) → | |
| y_4 = x) → | |
| y_3 = x) → | |
| y_2 = x) → | |
| y_1 = x) → | |
| … |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment