Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
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_3y_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_4y_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_4y_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_4y_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_3y_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_4y_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_4y_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_4y_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_4y_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_2y_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_3y_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_3y_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_4y_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_3y_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_4y_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_4y_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_3y_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_4y_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_4y_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_4y_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_3y_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_4y_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_4y_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_4y_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_4y_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_3y_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_4y_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_4y_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_4y_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_4y_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_4y_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