1	import Base
2	import ./types.bend as T
3	import ./board.bend as B
4	import ./solver.bend as S
5	import ./proof_base.bend as P
6	import ./proof_lists.bend as PL
7	import ./proof_cells.bend as PS
8	
9	# The counting search answers exactly as the plain one: dfs2, which carries
10	# the mines and unassigned cells of the partial layout, returns what dfs
11	# returns, as long as the counts start right and every cell it assigns is
12	# on the board.
13	
14	# Counting after an assignment
15	# ============================
16	
17	law row_none_set:
18	  for +r: List<&2, Maybe<&2, Bool>>
19	  for +x: Nat
20	  for +b: Bool
21	  for e: {List.get(&2, Maybe<&2, Bool>, r, x) == Some{None{}} : Maybe<&2, Maybe<&2, Bool>>}
22	  {S.row_none(r) == 1n+S.row_none(List.set(&2, Maybe<&2, Bool>, r, x, Some{b})) : Nat}
23	
24	def row_none_set(r, x, b, e):
25	  match r x:
26	    case Nil{} _:
27	      Empty.absurd({0n == 1n+0n : Nat}, PL.none_ne_some(Maybe<&2, Bool>, None{}, e))
28	    case m <> t 0n:
29	      %Equal.sym(Maybe<&2, Bool>, m, None{}, PL.some_inj(Maybe<&2, Bool>, m, None{}, e)) :
30	        {Nat.add(S.one_if(S.is_none(_)), S.row_none(t)) == 1n+Nat.add(S.one_if(S.is_none(Some{b})), S.row_none(t)) : Nat}
31	      {==}
32	    case m <> t 1n+k:
33	      %Equal.sym(Nat, S.row_none(t), 1n+S.row_none(List.set(&2, Maybe<&2, Bool>, t, k, Some{b})), row_none_set(t, k, b, e)) :
34	        {Nat.add(S.one_if(S.is_none(m)), _)
35	          == 1n+Nat.add(S.one_if(S.is_none(m)), S.row_none(List.set(&2, Maybe<&2, Bool>, t, k, Some{b}))) : Nat}
36	      P.add_succ(S.one_if(S.is_none(m)), S.row_none(List.set(&2, Maybe<&2, Bool>, t, k, Some{b})))
37	
38	law row_true_set_t:
39	  for +r: List<&2, Maybe<&2, Bool>>
40	  for +x: Nat
41	  for e: {List.get(&2, Maybe<&2, Bool>, r, x) == Some{None{}} : Maybe<&2, Maybe<&2, Bool>>}
42	  {S.row_true(List.set(&2, Maybe<&2, Bool>, r, x, Some{True{}})) == 1n+S.row_true(r) : Nat}
43	
44	def row_true_set_t(r, x, e):
45	  match r x:
46	    case Nil{} _:
47	      Empty.absurd({0n == 1n+0n : Nat}, PL.none_ne_some(Maybe<&2, Bool>, None{}, e))
48	    case m <> t 0n:
49	      %Equal.sym(Maybe<&2, Bool>, m, None{}, PL.some_inj(Maybe<&2, Bool>, m, None{}, e)) :
50	        {Nat.add(S.one_if(S.is_true(Some{True{}})), S.row_true(t)) == 1n+Nat.add(S.one_if(S.is_true(_)), S.row_true(t)) : Nat}
51	      {==}
52	    case m <> t 1n+k:
53	      %Equal.sym(Nat, S.row_true(List.set(&2, Maybe<&2, Bool>, t, k, Some{True{}})), 1n+S.row_true(t), row_true_set_t(t, k, e)) :
54	        {Nat.add(S.one_if(S.is_true(m)), _) == 1n+Nat.add(S.one_if(S.is_true(m)), S.row_true(t)) : Nat}
55	      P.add_succ(S.one_if(S.is_true(m)), S.row_true(t))
56	
57	law row_true_set_f:
58	  for +r: List<&2, Maybe<&2, Bool>>
59	  for +x: Nat
60	  for e: {List.get(&2, Maybe<&2, Bool>, r, x) == Some{None{}} : Maybe<&2, Maybe<&2, Bool>>}
61	  {S.row_true(List.set(&2, Maybe<&2, Bool>, r, x, Some{False{}})) == S.row_true(r) : Nat}
62	
63	def row_true_set_f(r, x, e):
64	  match r x:
65	    case Nil{} _:
66	      Empty.absurd({0n == 0n : Nat}, PL.none_ne_some(Maybe<&2, Bool>, None{}, e))
67	    case m <> t 0n:
68	      %Equal.sym(Maybe<&2, Bool>, m, None{}, PL.some_inj(Maybe<&2, Bool>, m, None{}, e)) :
69	        {Nat.add(S.one_if(S.is_true(Some{False{}})), S.row_true(t)) == Nat.add(S.one_if(S.is_true(_)), S.row_true(t)) : Nat}
70	      {==}
71	    case m <> t 1n+k:
72	      %Equal.sym(Nat, S.row_true(List.set(&2, Maybe<&2, Bool>, t, k, Some{False{}})), S.row_true(t), row_true_set_f(t, k, e)) :
73	        {Nat.add(S.one_if(S.is_true(m)), _) == Nat.add(S.one_if(S.is_true(m)), S.row_true(t)) : Nat}
74	      {==}
75	
76	law none_go:
77	  for +g: T.Grid(Maybe<&2, Bool>)
78	  for +y: Nat
79	  for +r: List<&2, Maybe<&2, Bool>>
80	  for +r2: List<&2, Maybe<&2, Bool>>
81	  for e: {List.get(&2, List<&2, Maybe<&2, Bool>>, g, y) == Some{r} : Maybe<&2, List<&2, Maybe<&2, Bool>>>}
82	  for rf: {S.row_none(r) == 1n+S.row_none(r2) : Nat}
83	  {S.part_none(g) == 1n+S.part_none(List.set(&2, List<&2, Maybe<&2, Bool>>, g, y, r2)) : Nat}
84	
85	def none_go(g, y, r, r2, e, rf):
86	  match g y:
87	    case Nil{} _:
88	      Empty.absurd({0n == 1n+0n : Nat}, PL.none_ne_some(List<&2, Maybe<&2, Bool>>, r, e))
89	    case row <> t 0n:
90	      %Equal.sym(List<&2, Maybe<&2, Bool>>, row, r, PL.some_inj(List<&2, Maybe<&2, Bool>>, row, r, e)) :
91	        {Nat.add(S.row_none(_), S.part_none(t)) == 1n+Nat.add(S.row_none(r2), S.part_none(t)) : Nat}
92	      %Equal.sym(Nat, S.row_none(r), 1n+S.row_none(r2), rf) :
93	        {Nat.add(_, S.part_none(t)) == 1n+Nat.add(S.row_none(r2), S.part_none(t)) : Nat}
94	      {==}
95	    case row <> t 1n+k:
96	      %Equal.sym(Nat, S.part_none(t), 1n+S.part_none(List.set(&2, List<&2, Maybe<&2, Bool>>, t, k, r2)), none_go(t, k, r, r2, e, rf)) :
97	        {Nat.add(S.row_none(row), _)
98	          == 1n+Nat.add(S.row_none(row), S.part_none(List.set(&2, List<&2, Maybe<&2, Bool>>, t, k, r2))) : Nat}
99	      P.add_succ(S.row_none(row), S.part_none(List.set(&2, List<&2, Maybe<&2, Bool>>, t, k, r2)))
100	
101	law true_go_t:
102	  for +g: T.Grid(Maybe<&2, Bool>)
103	  for +y: Nat
104	  for +r: List<&2, Maybe<&2, Bool>>
105	  for +r2: List<&2, Maybe<&2, Bool>>
106	  for e: {List.get(&2, List<&2, Maybe<&2, Bool>>, g, y) == Some{r} : Maybe<&2, List<&2, Maybe<&2, Bool>>>}
107	  for rf: {S.row_true(r2) == 1n+S.row_true(r) : Nat}
108	  {S.part_true(List.set(&2, List<&2, Maybe<&2, Bool>>, g, y, r2)) == 1n+S.part_true(g) : Nat}
109	
110	def true_go_t(g, y, r, r2, e, rf):
111	  match g y:
112	    case Nil{} _:
113	      Empty.absurd({0n == 1n+0n : Nat}, PL.none_ne_some(List<&2, Maybe<&2, Bool>>, r, e))
114	    case row <> t 0n:
115	      %Equal.sym(List<&2, Maybe<&2, Bool>>, row, r, PL.some_inj(List<&2, Maybe<&2, Bool>>, row, r, e)) :
116	        {Nat.add(S.row_true(r2), S.part_true(t)) == 1n+Nat.add(S.row_true(_), S.part_true(t)) : Nat}
117	      %Equal.sym(Nat, S.row_true(r2), 1n+S.row_true(r), rf) :
118	        {Nat.add(_, S.part_true(t)) == 1n+Nat.add(S.row_true(r), S.part_true(t)) : Nat}
119	      {==}
120	    case row <> t 1n+k:
121	      %Equal.sym(Nat, S.part_true(List.set(&2, List<&2, Maybe<&2, Bool>>, t, k, r2)), 1n+S.part_true(t), true_go_t(t, k, r, r2, e, rf)) :
122	        {Nat.add(S.row_true(row), _) == 1n+Nat.add(S.row_true(row), S.part_true(t)) : Nat}
123	      P.add_succ(S.row_true(row), S.part_true(t))
124	
125	law true_go_f:
126	  for +g: T.Grid(Maybe<&2, Bool>)
127	  for +y: Nat
128	  for +r: List<&2, Maybe<&2, Bool>>
129	  for +r2: List<&2, Maybe<&2, Bool>>
130	  for e: {List.get(&2, List<&2, Maybe<&2, Bool>>, g, y) == Some{r} : Maybe<&2, List<&2, Maybe<&2, Bool>>>}
131	  for rf: {S.row_true(r2) == S.row_true(r) : Nat}
132	  {S.part_true(List.set(&2, List<&2, Maybe<&2, Bool>>, g, y, r2)) == S.part_true(g) : Nat}
133	
134	def true_go_f(g, y, r, r2, e, rf):
135	  match g y:
136	    case Nil{} _:
137	      Empty.absurd({0n == 0n : Nat}, PL.none_ne_some(List<&2, Maybe<&2, Bool>>, r, e))
138	    case row <> t 0n:
139	      %Equal.sym(List<&2, Maybe<&2, Bool>>, row, r, PL.some_inj(List<&2, Maybe<&2, Bool>>, row, r, e)) :
140	        {Nat.add(S.row_true(r2), S.part_true(t)) == Nat.add(S.row_true(_), S.part_true(t)) : Nat}
141	      %Equal.sym(Nat, S.row_true(r2), S.row_true(r), rf) :
142	        {Nat.add(_, S.part_true(t)) == Nat.add(S.row_true(r), S.part_true(t)) : Nat}
143	      {==}
144	    case row <> t 1n+k:
145	      %Equal.sym(Nat, S.part_true(List.set(&2, List<&2, Maybe<&2, Bool>>, t, k, r2)), S.part_true(t), true_go_f(t, k, r, r2, e, rf)) :
146	        {Nat.add(S.row_true(row), _) == Nat.add(S.row_true(row), S.part_true(t)) : Nat}
147	      {==}
148	
149	# The row of an unassigned cell, and the cell in it.
150	def cell_none(+w: Nat, +h: Nat, +part: T.Grid(Maybe<&2, Bool>), +x: Nat, +y: Nat,
151	  +sh: {B.shaped(Maybe<&2, Bool>, w, h, part) == True{} : Bool}, +on: {B.on_board(w, h, T.Pos{x, y}) == True{} : Bool},
152	  fr: {S.look(part, T.Pos{x, y}) == None{} : Maybe<&2, Bool>}) ->
153	  {List.get(&2, Maybe<&2, Bool>, PL.row_of(Maybe<&2, Bool>, part, y), x) == Some{None{}} : Maybe<&2, Maybe<&2, Bool>>}:
154	  +xw = P.and_true_l(Nat.is_lt(x, w), Nat.is_lt(y, h), on)
155	  +yh = P.and_true_r(Nat.is_lt(x, w), Nat.is_lt(y, h), on)
156	  +row = PL.row_of(Maybe<&2, Bool>, part, y)
157	  +xl = {%Equal.sym(Nat, List.length(&2, Maybe<&2, Bool>, row), w, PL.row_in_len(Maybe<&2, Bool>, w, h, part, y, sh, yh)) :
158	    {Nat.is_lt(x, _) == True{} : Bool};
159	    xw : {Nat.is_lt(x, List.length(&2, Maybe<&2, Bool>, row)) == True{} : Bool}}
160	  %fr : {List.get(&2, Maybe<&2, Bool>, row, x) == Some{_} : Maybe<&2, Maybe<&2, Bool>>}
161	  PL.get_in(Maybe<&2, Bool>, row, x, None{}, xl)
162	
163	def row_get(+w: Nat, +h: Nat, +part: T.Grid(Maybe<&2, Bool>), +x: Nat, +y: Nat,
164	  +sh: {B.shaped(Maybe<&2, Bool>, w, h, part) == True{} : Bool}, +on: {B.on_board(w, h, T.Pos{x, y}) == True{} : Bool}) ->
165	  {List.get(&2, List<&2, Maybe<&2, Bool>>, part, y) == Some{PL.row_of(Maybe<&2, Bool>, part, y)} : Maybe<&2, List<&2, Maybe<&2, Bool>>>}:
166	  PL.row_in_get(Maybe<&2, Bool>, w, h, part, y, sh, P.and_true_r(Nat.is_lt(x, w), Nat.is_lt(y, h), on))
167	
168	# Assigning an unassigned cell of the board uses up one unassigned cell...
169	law none_set:
170	  for +w: Nat
171	  for +h: Nat
172	  for +part: T.Grid(Maybe<&2, Bool>)
173	  for +x: Nat
174	  for +y: Nat
175	  for +b: Bool
176	  for +sh: {B.shaped(Maybe<&2, Bool>, w, h, part) == True{} : Bool}
177	  for +on: {B.on_board(w, h, T.Pos{x, y}) == True{} : Bool}
178	  for +fr: {S.look(part, T.Pos{x, y}) == None{} : Maybe<&2, Bool>}
179	  {S.part_none(part) == 1n+S.part_none(B.set_at(Maybe<&2, Bool>, part, T.Pos{x, y}, Some{b})) : Nat}
180	
181	def none_set(w, h, part, x, y, b, sh, on, fr):
182	  +row = PL.row_of(Maybe<&2, Bool>, part, y)
183	  none_go(part, y, row, List.set(&2, Maybe<&2, Bool>, row, x, Some{b}), row_get(w, h, part, x, y, sh, on),
184	    row_none_set(row, x, b, cell_none(w, h, part, x, y, sh, on, fr)))
185	
186	# ... and adds a mine when it places one ...
187	law true_set_t:
188	  for +w: Nat
189	  for +h: Nat
190	  for +part: T.Grid(Maybe<&2, Bool>)
191	  for +x: Nat
192	  for +y: Nat
193	  for +sh: {B.shaped(Maybe<&2, Bool>, w, h, part) == True{} : Bool}
194	  for +on: {B.on_board(w, h, T.Pos{x, y}) == True{} : Bool}
195	  for +fr: {S.look(part, T.Pos{x, y}) == None{} : Maybe<&2, Bool>}
196	  {S.part_true(B.set_at(Maybe<&2, Bool>, part, T.Pos{x, y}, Some{True{}})) == 1n+S.part_true(part) : Nat}
197	
198	def true_set_t(w, h, part, x, y, sh, on, fr):
199	  +row = PL.row_of(Maybe<&2, Bool>, part, y)
200	  true_go_t(part, y, row, List.set(&2, Maybe<&2, Bool>, row, x, Some{True{}}), row_get(w, h, part, x, y, sh, on),
201	    row_true_set_t(row, x, cell_none(w, h, part, x, y, sh, on, fr)))
202	
203	# ... and none otherwise.
204	law true_set_f:
205	  for +w: Nat
206	  for +h: Nat
207	  for +part: T.Grid(Maybe<&2, Bool>)
208	  for +x: Nat
209	  for +y: Nat
210	  for +sh: {B.shaped(Maybe<&2, Bool>, w, h, part) == True{} : Bool}
211	  for +on: {B.on_board(w, h, T.Pos{x, y}) == True{} : Bool}
212	  for +fr: {S.look(part, T.Pos{x, y}) == None{} : Maybe<&2, Bool>}
213	  {S.part_true(B.set_at(Maybe<&2, Bool>, part, T.Pos{x, y}, Some{False{}})) == S.part_true(part) : Nat}
214	
215	def true_set_f(w, h, part, x, y, sh, on, fr):
216	  +row = PL.row_of(Maybe<&2, Bool>, part, y)
217	  true_go_f(part, y, row, List.set(&2, Maybe<&2, Bool>, row, x, Some{False{}}), row_get(w, h, part, x, y, sh, on),
218	    row_true_set_f(row, x, cell_none(w, h, part, x, y, sh, on, fr)))
219	
220	# Lists of todos
221	# ==============
222	
223	# Every todo of ts passes f (with e for f's context).
224	def tall(~E: Data, ~f: E -> S.Todo -> Bool, +e: E, ts: List<&2, S.Todo>) -> Bool:
225	  match ts:
226	    case Nil{}:
227	      True{}
228	    case t <> rest:
229	      f(e, t) && tall(~E, ~f, e, rest)
230	
231	def tall_head(~E: Data, ~f: E -> S.Todo -> Bool, +e: E, +t: S.Todo, +rest: List<&2, S.Todo>,
232	  h: {tall(~E, ~f, e, t <> rest) == True{} : Bool}) -> {f(e, t) == True{} : Bool}:
233	  P.and_true_l(f(e, t), tall(~E, ~f, e, rest), h)
234	
235	def tall_tail(~E: Data, ~f: E -> S.Todo -> Bool, +e: E, +t: S.Todo, +rest: List<&2, S.Todo>,
236	  h: {tall(~E, ~f, e, t <> rest) == True{} : Bool}) -> {tall(~E, ~f, e, rest) == True{} : Bool}:
237	  P.and_true_r(f(e, t), tall(~E, ~f, e, rest), h)
238	
239	def tall_cons(~E: Data, ~f: E -> S.Todo -> Bool, +e: E, +t: S.Todo, +rest: List<&2, S.Todo>,
240	  a: {f(e, t) == True{} : Bool}, b: {tall(~E, ~f, e, rest) == True{} : Bool}) ->
241	  {tall(~E, ~f, e, t <> rest) == True{} : Bool}:
242	  %Equal.sym(Bool, tall(~E, ~f, e, rest), True{}, b) : {Bool.and(f(e, t), _) == True{} : Bool}
243	  %Equal.sym(Bool, f(e, t), True{}, a) : {Bool.and(_, True{}) == True{} : Bool}
244	  {==}
245	
246	def tall_put(~E: Data, ~f: E -> S.Todo -> Bool, +e: E, +b: Bool, +t: S.Todo, +rest: List<&2, S.Todo>,
247	  a: {f(e, t) == True{} : Bool}, r: {tall(~E, ~f, e, rest) == True{} : Bool}) ->
248	  {tall(~E, ~f, e, List.filter.put(S.Todo, t, rest, b)) == True{} : Bool}:
249	  match b:
250	    case False{}:
251	      r
252	    case True{}:
253	      tall_cons(~E, ~f, e, t, rest, a, r)
254	
255	law tall_append:
256	  for ~E: Data
257	  for ~f: E -> S.Todo -> Bool
258	  for +e: E
259	  for +xs: List<&2, S.Todo>
260	  for +ys: List<&2, S.Todo>
261	  for +a: {tall(~E, ~f, e, xs) == True{} : Bool}
262	  for b: {tall(~E, ~f, e, ys) == True{} : Bool}
263	  {tall(~E, ~f, e, List.append(&2, S.Todo, xs, ys)) == True{} : Bool}
264	
265	def tall_append(E, f, e, xs, ys, a, b):
266	  match xs:
267	    case Nil{}:
268	      b
269	    case t <> rest:
270	      tall_cons(~E, ~f, e, t, List.append(&2, S.Todo, rest, ys), tall_head(~E, ~f, e, t, rest, a),
271	        tall_append(~E, ~f, e, rest, ys, tall_tail(~E, ~f, e, t, rest, a), b))
272	
273	law tall_nears:
274	  for ~E: Data
275	  for ~f: E -> S.Todo -> Bool
276	  for +e: E
277	  for +ts: List<&2, S.Todo>
278	  for +a: {tall(~E, ~f, e, ts) == True{} : Bool}
279	  {tall(~E, ~f, e, S.nears(ts)) == True{} : Bool}
280	
281	def tall_nears(E, f, e, ts, a):
282	  match ts:
283	    case Nil{}:
284	      {==}
285	    case +t <> +rest:
286	      tall_put(~E, ~f, e, S.has_rel(t), t, S.nears(rest), tall_head(~E, ~f, e, t, rest, a),
287	        tall_nears(~E, ~f, e, rest, tall_tail(~E, ~f, e, t, rest, a)))
288	
289	law tall_fars:
290	  for ~E: Data
291	  for ~f: E -> S.Todo -> Bool
292	  for +e: E
293	  for +ts: List<&2, S.Todo>
294	  for +a: {tall(~E, ~f, e, ts) == True{} : Bool}
295	  {tall(~E, ~f, e, S.fars(ts)) == True{} : Bool}
296	
297	def tall_fars(E, f, e, ts, a):
298	  match ts:
299	    case Nil{}:
300	      {==}
301	    case +t <> +rest:
302	      tall_put(~E, ~f, e, Bool.not(S.has_rel(t)), t, S.fars(rest), tall_head(~E, ~f, e, t, rest, a),
303	        tall_fars(~E, ~f, e, rest, tall_tail(~E, ~f, e, t, rest, a)))
304	
305	law tall_with_c:
306	  for ~E: Data
307	  for ~f: E -> S.Todo -> Bool
308	  for +e: E
309	  for +ts: List<&2, S.Todo>
310	  for +q: T.Pos
311	  for +a: {tall(~E, ~f, e, ts) == True{} : Bool}
312	  {tall(~E, ~f, e, S.with_c(ts, q)) == True{} : Bool}
313	
314	def tall_with_c(E, f, e, ts, q, a):
315	  match ts:
316	    case Nil{}:
317	      {==}
318	    case +t <> +rest:
319	      tall_put(~E, ~f, e, B.same(S.todo_c(t), q), t, S.with_c(rest, q), tall_head(~E, ~f, e, t, rest, a),
320	        tall_with_c(~E, ~f, e, rest, q, tall_tail(~E, ~f, e, t, rest, a)))
321	
322	law tall_gather:
323	  for ~E: Data
324	  for ~f: E -> S.Todo -> Bool
325	  for +e: E
326	  for +qs: List<&2, T.Pos>
327	  for +ts: List<&2, S.Todo>
328	  for +a: {tall(~E, ~f, e, ts) == True{} : Bool}
329	  {tall(~E, ~f, e, S.gather(qs, ts)) == True{} : Bool}
330	
331	def tall_gather(E, f, e, qs, ts, a):
332	  match qs:
333	    case Nil{}:
334	      {==}
335	    case q <> t:
336	      tall_append(~E, ~f, e, S.with_c(ts, q), S.gather(t, ts), tall_with_c(~E, ~f, e, ts, q, a),
337	        tall_gather(~E, ~f, e, t, ts, a))
338	
339	law tall_drop:
340	  for ~E: Data
341	  for ~f: E -> S.Todo -> Bool
342	  for +e: E
343	  for +ts: List<&2, S.Todo>
344	  for +k: Nat
345	  for +a: {tall(~E, ~f, e, ts) == True{} : Bool}
346	  {tall(~E, ~f, e, List.drop(&2, S.Todo, ts, k)) == True{} : Bool}
347	
348	def tall_drop(E, f, e, ts, k, a):
349	  match ts k:
350	    case Nil{} _:
351	      {==}
352	    case t <> rest 0n:
353	      a
354	    case t <> rest 1n+j:
355	      tall_drop(~E, ~f, e, rest, j, tall_tail(~E, ~f, e, t, rest, a))
356	
357	law tall_take:
358	  for ~E: Data
359	  for ~f: E -> S.Todo -> Bool
360	  for +e: E
361	  for +ts: List<&2, S.Todo>
362	  for +k: Nat
363	  for +a: {tall(~E, ~f, e, ts) == True{} : Bool}
364	  {tall(~E, ~f, e, List.take(&2, S.Todo, ts, k)) == True{} : Bool}
365	
366	def tall_take(E, f, e, ts, k, a):
367	  match ts k:
368	    case Nil{} _:
369	      {==}
370	    case t <> rest 0n:
371	      {==}
372	    case t <> rest 1n+j:
373	      tall_cons(~E, ~f, e, t, List.take(&2, S.Todo, rest, j), tall_head(~E, ~f, e, t, rest, a),
374	        tall_take(~E, ~f, e, rest, j, tall_tail(~E, ~f, e, t, rest, a)))
375	
376	# The order of every search passes whatever the cells of a solve pass.
377	law tall_plan:
378	  for ~E: Data
379	  for ~f: E -> S.Todo -> Bool
380	  for +e: E
381	  for +ts: List<&2, S.Todo>
382	  for +qs: List<&2, T.Pos>
383	  for +k: Nat
384	  for +a: {tall(~E, ~f, e, ts) == True{} : Bool}
385	  {tall(~E, ~f, e, List.append(&2, S.Todo, S.gather(qs, S.nears(ts)),
386	    List.append(&2, S.Todo, S.rot(S.fars(ts), k), S.order(ts)))) == True{} : Bool}
387	
388	def tall_plan(E, f, e, ts, qs, k, a):
389	  +an = tall_nears(~E, ~f, e, ts, a)
390	  +af = tall_fars(~E, ~f, e, ts, a)
391	  +far = S.fars(ts)
392	  tall_append(~E, ~f, e, S.gather(qs, S.nears(ts)), List.append(&2, S.Todo, S.rot(far, k), S.order(ts)),
393	    tall_gather(~E, ~f, e, qs, S.nears(ts), an),
394	    tall_append(~E, ~f, e, S.rot(far, k), S.order(ts),
395	      tall_append(~E, ~f, e, List.drop(&2, S.Todo, far, k), List.take(&2, S.Todo, far, k),
396	        tall_drop(~E, ~f, e, far, k, af), tall_take(~E, ~f, e, far, k, af)),
397	      tall_append(~E, ~f, e, S.nears(ts), far, an, af)))
398	
399	# Todos on the board
400	# ==================
401	
402	def con_f(e: PS.WH, t: S.Todo) -> Bool:
403	  match t:
404	    case S.Todo{c, rel}:
405	      PS.onb(e, c)
406	
407	# The todos of cells on the board are on the board.
408	law con_todos:
409	  for +w: Nat
410	  for +h: Nat
411	  for +its: List<&2, S.Item>
412	  for +cs: List<&2, T.Pos>
413	  for +on: {PS.allp(~PS.WH, ~PS.onb, PS.WH{w, h}, cs) == True{} : Bool}
414	  {tall(~PS.WH, ~con_f, PS.WH{w, h}, S.todos(its, cs)) == True{} : Bool}
415	
416	def con_todos(w, h, its, cs, on):
417	  match cs:
418	    case Nil{}:
419	      {==}
420	    case +c <> +t:
421	      tall_cons(~PS.WH, ~con_f, PS.WH{w, h}, S.Todo{c, S.around(its, c)}, S.todos(its, t),
422	        PS.allp_head(~PS.WH, ~PS.onb, PS.WH{w, h}, c, t, on),
423	        con_todos(w, h, its, t, PS.allp_tail(~PS.WH, ~PS.onb, PS.WH{w, h}, c, t, on)))
424	
425	# The counting search
426	# ===================
427	
428	def none_of(m: Maybe<&2, Bool>, e: {S.is_none(m) == True{} : Bool}) -> {m == None{} : Maybe<&2, Bool>}:
429	  match m:
430	    case Some{b}:
431	      Empty.absurd({Some{b} == None{} : Maybe<&2, Bool>}, P.false_ne_true(e))
432	    case None{}:
433	      {==}
434	
435	def one_less(+a: Nat, +b: Nat, +f: Nat, e1: {a == f : Nat}, e2: {a == 1n+b : Nat}) -> {b == Nat.sub(f, 1n) : Nat}:
436	  %e1 : {b == Nat.sub(_, 1n) : Nat}
437	  %Equal.sym(Nat, a, 1n+b, e2) : {b == Nat.sub(_, 1n) : Nat}
438	  Equal.sym(Nat, Nat.sub(b, 0n), b, P.sub_zero(b))
439	
440	def when_or_eq(+g0a: Bool, +g0b: Bool, eg0: {g0a == g0b : Bool},
441	  +d0a: Maybe<&2, T.Grid(Bool)>, +d0b: Maybe<&2, T.Grid(Bool)>, ed0: {d0a == d0b : Maybe<&2, T.Grid(Bool)>},
442	  +g1a: Bool, +g1b: Bool, eg1: {g1a == g1b : Bool},
443	  +d1a: Maybe<&2, T.Grid(Bool)>, +d1b: Maybe<&2, T.Grid(Bool)>, ed1: {d1a == d1b : Maybe<&2, T.Grid(Bool)>}) ->
444	  {S.dfs.or(S.dfs.when(g0a, x => d0a), y => S.dfs.when(g1a, z => d1a))
445	    == S.dfs.or(S.dfs.when(g0b, x => d0b), y => S.dfs.when(g1b, z => d1b)) : Maybe<&2, T.Grid(Bool)>}:
446	  %eg0 : {S.dfs.or(S.dfs.when(g0a, x => d0a), y => S.dfs.when(g1a, z => d1a))
447	    == S.dfs.or(S.dfs.when(_, x => d0b), y => S.dfs.when(g1b, z => d1b)) : Maybe<&2, T.Grid(Bool)>}
448	  %ed0 : {S.dfs.or(S.dfs.when(g0a, x => d0a), y => S.dfs.when(g1a, z => d1a))
449	    == S.dfs.or(S.dfs.when(g0a, x => _), y => S.dfs.when(g1b, z => d1b)) : Maybe<&2, T.Grid(Bool)>}
450	  %eg1 : {S.dfs.or(S.dfs.when(g0a, x => d0a), y => S.dfs.when(g1a, z => d1a))
451	    == S.dfs.or(S.dfs.when(g0a, x => d0a), y => S.dfs.when(_, z => d1b)) : Maybe<&2, T.Grid(Bool)>}
452	  %ed1 : {S.dfs.or(S.dfs.when(g0a, x => d0a), y => S.dfs.when(g1a, z => d1a))
453	    == S.dfs.or(S.dfs.when(g0a, x => d0a), y => S.dfs.when(g1a, z => _)) : Maybe<&2, T.Grid(Bool)>}
454	  {==}
455	
456	def dfs2_eq.node(+x: Nat, +y: Nat, +rel: List<&2, S.Item>, +rest: List<&2, S.Todo>, +part: T.Grid(Maybe<&2, Bool>),
457	  +w: Nat, +h: Nat, +n: Nat, +rows: T.Grid(T.Seen), +its: List<&2, S.Item>, +t: Nat, +f: Nat,
458	  +sh: {B.shaped(Maybe<&2, Bool>, w, h, part) == True{} : Bool}, +on: {B.on_board(w, h, T.Pos{x, y}) == True{} : Bool},
459	  +et: {S.part_true(part) == t : Nat}, +ef: {S.part_none(part) == f : Nat},
460	  +fr: Bool, fre: {S.is_none(S.look(part, T.Pos{x, y})) == fr : Bool},
461	  ks: {S.dfs2(rest, part, t, f, S.Ctx{w, h, n, rows, its}) == S.dfs(rest, part, S.Ctx{w, h, n, rows, its}) : Maybe<&2, T.Grid(Bool)>},
462	  k0: {S.part_true(B.set_at(Maybe<&2, Bool>, part, T.Pos{x, y}, Some{False{}})) == t : Nat} ->
463	    {S.part_none(B.set_at(Maybe<&2, Bool>, part, T.Pos{x, y}, Some{False{}})) == Nat.sub(f, 1n) : Nat} ->
464	    {S.dfs2(rest, B.set_at(Maybe<&2, Bool>, part, T.Pos{x, y}, Some{False{}}), t, Nat.sub(f, 1n), S.Ctx{w, h, n, rows, its})
465	      == S.dfs(rest, B.set_at(Maybe<&2, Bool>, part, T.Pos{x, y}, Some{False{}}), S.Ctx{w, h, n, rows, its}) : Maybe<&2, T.Grid(Bool)>},
466	  k1: {S.part_true(B.set_at(Maybe<&2, Bool>, part, T.Pos{x, y}, Some{True{}})) == 1n+t : Nat} ->
467	    {S.part_none(B.set_at(Maybe<&2, Bool>, part, T.Pos{x, y}, Some{True{}})) == Nat.sub(f, 1n) : Nat} ->
468	    {S.dfs2(rest, B.set_at(Maybe<&2, Bool>, part, T.Pos{x, y}, Some{True{}}), 1n+t, Nat.sub(f, 1n), S.Ctx{w, h, n, rows, its})
469	      == S.dfs(rest, B.set_at(Maybe<&2, Bool>, part, T.Pos{x, y}, Some{True{}}), S.Ctx{w, h, n, rows, its}) : Maybe<&2, T.Grid(Bool)>}) ->
470	  {S.dfs.free(fr, u => S.dfs2(rest, part, t, f, S.Ctx{w, h, n, rows, its}),
471	      v => S.dfs.or(S.dfs.when(Bool.and(S.between(t, Nat.sub(f, 1n), n),
472	          S.items_open(B.set_at(Maybe<&2, Bool>, part, T.Pos{x, y}, Some{False{}}), rel)),
473	        x0 => S.dfs2(rest, B.set_at(Maybe<&2, Bool>, part, T.Pos{x, y}, Some{False{}}), t, Nat.sub(f, 1n), S.Ctx{w, h, n, rows, its})),
474	      y0 => S.dfs.when(Bool.and(S.between(1n+t, Nat.sub(f, 1n), n),
475	          S.items_open(B.set_at(Maybe<&2, Bool>, part, T.Pos{x, y}, Some{True{}}), rel)),
476	        z0 => S.dfs2(rest, B.set_at(Maybe<&2, Bool>, part, T.Pos{x, y}, Some{True{}}), 1n+t, Nat.sub(f, 1n), S.Ctx{w, h, n, rows, its}))))
477	    == S.dfs.free(fr, u => S.dfs(rest, part, S.Ctx{w, h, n, rows, its}),
478	      v => S.dfs.or(S.dfs.when(S.open_ok(B.set_at(Maybe<&2, Bool>, part, T.Pos{x, y}, Some{False{}}), rel, n),
479	        x0 => S.dfs(rest, B.set_at(Maybe<&2, Bool>, part, T.Pos{x, y}, Some{False{}}), S.Ctx{w, h, n, rows, its})),
480	      y0 => S.dfs.when(S.open_ok(B.set_at(Maybe<&2, Bool>, part, T.Pos{x, y}, Some{True{}}), rel, n),
481	        z0 => S.dfs(rest, B.set_at(Maybe<&2, Bool>, part, T.Pos{x, y}, Some{True{}}), S.Ctx{w, h, n, rows, its})))) : Maybe<&2, T.Grid(Bool)>}:
482	  match fr:
483	    case False{}:
484	      ks
485	    case True{}:
486	      +q = {T.Pos{x, y} : T.Pos}
487	      +p0 = B.set_at(Maybe<&2, Bool>, part, q, Some{False{}})
488	      +p1 = B.set_at(Maybe<&2, Bool>, part, q, Some{True{}})
489	      +lk = none_of(S.look(part, q), fre)
490	      +e0f = one_less(S.part_none(part), S.part_none(p0), f, ef, none_set(w, h, part, x, y, False{}, sh, on, lk))
491	      +e1f = one_less(S.part_none(part), S.part_none(p1), f, ef, none_set(w, h, part, x, y, True{}, sh, on, lk))
492	      +e0t = Equal.trans(Nat, S.part_true(p0), S.part_true(part), t, true_set_f(w, h, part, x, y, sh, on, lk), et)
493	      +e1t = {%et : {S.part_true(p1) == 1n+_ : Nat}; true_set_t(w, h, part, x, y, sh, on, lk) : {S.part_true(p1) == 1n+t : Nat}}
494	      +eg0 = {%e0t : {Bool.and(S.between(_, Nat.sub(f, 1n), n), S.items_open(p0, rel)) == S.open_ok(p0, rel, n) : Bool};
495	        %e0f : {Bool.and(S.between(S.part_true(p0), _, n), S.items_open(p0, rel)) == S.open_ok(p0, rel, n) : Bool};
496	        {==} : {Bool.and(S.between(t, Nat.sub(f, 1n), n), S.items_open(p0, rel)) == S.open_ok(p0, rel, n) : Bool}}
497	      +eg1 = {%e1t : {Bool.and(S.between(_, Nat.sub(f, 1n), n), S.items_open(p1, rel)) == S.open_ok(p1, rel, n) : Bool};
498	        %e1f : {Bool.and(S.between(S.part_true(p1), _, n), S.items_open(p1, rel)) == S.open_ok(p1, rel, n) : Bool};
499	        {==} : {Bool.and(S.between(1n+t, Nat.sub(f, 1n), n), S.items_open(p1, rel)) == S.open_ok(p1, rel, n) : Bool}}
500	      +ctx = {S.Ctx{w, h, n, rows, its} : S.Ctx}
501	      when_or_eq(Bool.and(S.between(t, Nat.sub(f, 1n), n), S.items_open(p0, rel)), S.open_ok(p0, rel, n), eg0,
502	        S.dfs2(rest, p0, t, Nat.sub(f, 1n), ctx), S.dfs(rest, p0, ctx), k0(e0t, e0f),
503	        Bool.and(S.between(1n+t, Nat.sub(f, 1n), n), S.items_open(p1, rel)), S.open_ok(p1, rel, n), eg1,
504	        S.dfs2(rest, p1, 1n+t, Nat.sub(f, 1n), ctx), S.dfs(rest, p1, ctx), k1(e1t, e1f))
505	
506	# With the counts right and every cell on the board, the counting search
507	# answers exactly as the plain one.
508	law dfs2_eq:
509	  for +todo: List<&2, S.Todo>
510	  for +part: T.Grid(Maybe<&2, Bool>)
511	  for +w: Nat
512	  for +h: Nat
513	  for +n: Nat
514	  for +rows: T.Grid(T.Seen)
515	  for +its: List<&2, S.Item>
516	  for +t: Nat
517	  for +f: Nat
518	  for +sh: {B.shaped(Maybe<&2, Bool>, w, h, part) == True{} : Bool}
519	  for +con: {tall(~PS.WH, ~con_f, PS.WH{w, h}, todo) == True{} : Bool}
520	  for +et: {S.part_true(part) == t : Nat}
521	  for +ef: {S.part_none(part) == f : Nat}
522	  {S.dfs2(todo, part, t, f, S.Ctx{w, h, n, rows, its}) == S.dfs(todo, part, S.Ctx{w, h, n, rows, its}) : Maybe<&2, T.Grid(Bool)>}
523	
524	def dfs2_eq(todo, part, w, h, n, rows, its, t, f, sh, con, et, ef):
525	  match todo:
526	    case Nil{}:
527	      {==}
528	    case S.Todo{c, rel} <> rest:
529	      match c:
530	        case T.Pos{x, y}:
531	          +q = {T.Pos{x, y} : T.Pos}
532	          +onc = tall_head(~PS.WH, ~con_f, PS.WH{w, h}, S.Todo{q, rel}, rest, con)
533	          +conr = tall_tail(~PS.WH, ~con_f, PS.WH{w, h}, S.Todo{q, rel}, rest, con)
534	          +p0 = B.set_at(Maybe<&2, Bool>, part, q, Some{False{}})
535	          +p1 = B.set_at(Maybe<&2, Bool>, part, q, Some{True{}})
536	          dfs2_eq.node(x, y, rel, rest, part, w, h, n, rows, its, t, f, sh, onc, et, ef, S.is_none(S.look(part, q)), {==},
537	            dfs2_eq(rest, part, w, h, n, rows, its, t, f, sh, conr, et, ef),
538	            e0t => e0f => dfs2_eq(rest, p0, w, h, n, rows, its, t, Nat.sub(f, 1n),
539	              PL.shaped_set(Maybe<&2, Bool>, w, h, part, q, Some{False{}}, sh), conr, e0t, e0f),
540	            e1t => e1f => dfs2_eq(rest, p1, w, h, n, rows, its, 1n+t, Nat.sub(f, 1n),
541	              PL.shaped_set(Maybe<&2, Bool>, w, h, part, q, Some{True{}}, sh), conr, e1t, e1f))