1	import Base
2	import ./types.bend as T
3	import ./board.bend as B
4	import ./solver.bend as S
5	import ./LAWS.bend as L
6	import ./proof_base.bend as P
7	import ./proof_grid.bend as PG
8	import ./proof_copy.bend as PC
9	import ./proof_lists.bend as PL
10	import ./proof_cells.bend as PS
11	import ./proof_sums.bend as PU
12	import ./proof_walk.bend as PW
13	import ./proof_speed.bend as PF
14	
15	# The solver is right: when it names a cell, the cell is provably safe;
16	# when it names none, every hidden cell might hold a mine.
17	
18	# Counting as sums
19	# ================
20	
21	def one(b: Bool) -> Nat:
22	  Bool.pick(Nat, b, 1n, 0n)
23	
24	def tf(m: Maybe<&2, Bool>) -> Nat:
25	  S.one_if(S.is_true(m))
26	
27	def nf(m: Maybe<&2, Bool>) -> Nat:
28	  S.one_if(S.is_none(m))
29	
30	law row_mines_sum:
31	  for +r: List<&2, Bool>
32	  {B.row_mines(r) == PU.rsum(~Bool, ~one, r) : Nat}
33	
34	def row_mines_sum(r):
35	  match r:
36	    case Nil{}:
37	      {==}
38	    case b <> t:
39	      %row_mines_sum(t) : {Nat.add(Bool.pick(Nat, b, 1n, 0n), B.row_mines(t)) == Nat.add(one(b), _) : Nat}
40	      {==}
41	
42	law total_sum:
43	  for +g: T.Grid(Bool)
44	  {B.total_mines(g) == PU.gsum(~Bool, ~one, g) : Nat}
45	
46	def total_sum(g):
47	  match g:
48	    case Nil{}:
49	      {==}
50	    case r <> t:
51	      %row_mines_sum(r) : {Nat.add(B.row_mines(r), B.total_mines(t)) == Nat.add(_, PU.gsum(~Bool, ~one, t)) : Nat}
52	      %total_sum(t) : {Nat.add(B.row_mines(r), B.total_mines(t)) == Nat.add(B.row_mines(r), _) : Nat}
53	      {==}
54	
55	law count_sum:
56	  for +layout: T.Grid(Bool)
57	  for +ps: List<&2, T.Pos>
58	  {B.count_mines(layout, ps) == PU.csum(~Bool, ~one, False{}, layout, ps) : Nat}
59	
60	def count_sum(layout, ps):
61	  match ps:
62	    case Nil{}:
63	      {==}
64	    case q <> t:
65	      %count_sum(layout, t) :
66	        {Nat.add(Bool.pick(Nat, B.mine(layout, q), 1n, 0n), B.count_mines(layout, t))
67	          == Nat.add(one(B.at(Bool, False{}, layout, q)), _) : Nat}
68	      {==}
69	
70	law row_true_sum:
71	  for +r: List<&2, Maybe<&2, Bool>>
72	  {S.row_true(r) == PU.rsum(~Maybe<&2, Bool>, ~tf, r) : Nat}
73	
74	def row_true_sum(r):
75	  match r:
76	    case Nil{}:
77	      {==}
78	    case m <> t:
79	      %row_true_sum(t) : {Nat.add(S.one_if(S.is_true(m)), S.row_true(t)) == Nat.add(tf(m), _) : Nat}
80	      {==}
81	
82	law row_none_sum:
83	  for +r: List<&2, Maybe<&2, Bool>>
84	  {S.row_none(r) == PU.rsum(~Maybe<&2, Bool>, ~nf, r) : Nat}
85	
86	def row_none_sum(r):
87	  match r:
88	    case Nil{}:
89	      {==}
90	    case m <> t:
91	      %row_none_sum(t) : {Nat.add(S.one_if(S.is_none(m)), S.row_none(t)) == Nat.add(nf(m), _) : Nat}
92	      {==}
93	
94	law part_true_sum:
95	  for +g: T.Grid(Maybe<&2, Bool>)
96	  {S.part_true(g) == PU.gsum(~Maybe<&2, Bool>, ~tf, g) : Nat}
97	
98	def part_true_sum(g):
99	  match g:
100	    case Nil{}:
101	      {==}
102	    case r <> t:
103	      %row_true_sum(r) : {Nat.add(S.row_true(r), S.part_true(t)) == Nat.add(_, PU.gsum(~Maybe<&2, Bool>, ~tf, t)) : Nat}
104	      %part_true_sum(t) : {Nat.add(S.row_true(r), S.part_true(t)) == Nat.add(S.row_true(r), _) : Nat}
105	      {==}
106	
107	law part_none_sum:
108	  for +g: T.Grid(Maybe<&2, Bool>)
109	  {S.part_none(g) == PU.gsum(~Maybe<&2, Bool>, ~nf, g) : Nat}
110	
111	def part_none_sum(g):
112	  match g:
113	    case Nil{}:
114	      {==}
115	    case r <> t:
116	      %row_none_sum(r) : {Nat.add(S.row_none(r), S.part_none(t)) == Nat.add(_, PU.gsum(~Maybe<&2, Bool>, ~nf, t)) : Nat}
117	      %part_none_sum(t) : {Nat.add(S.row_none(r), S.part_none(t)) == Nat.add(S.row_none(r), _) : Nat}
118	      {==}
119	
120	law true_among_sum:
121	  for +part: T.Grid(Maybe<&2, Bool>)
122	  for +ps: List<&2, T.Pos>
123	  {S.true_among(part, ps) == PU.csum(~Maybe<&2, Bool>, ~tf, None{}, part, ps) : Nat}
124	
125	def true_among_sum(part, ps):
126	  match ps:
127	    case Nil{}:
128	      {==}
129	    case q <> t:
130	      %true_among_sum(part, t) :
131	        {Nat.add(S.one_if(S.is_true(S.look(part, q))), S.true_among(part, t))
132	          == Nat.add(tf(B.at(Maybe<&2, Bool>, None{}, part, q)), _) : Nat}
133	      {==}
134	
135	law none_among_sum:
136	  for +part: T.Grid(Maybe<&2, Bool>)
137	  for +ps: List<&2, T.Pos>
138	  {S.none_among(part, ps) == PU.csum(~Maybe<&2, Bool>, ~nf, None{}, part, ps) : Nat}
139	
140	def none_among_sum(part, ps):
141	  match ps:
142	    case Nil{}:
143	      {==}
144	    case q <> t:
145	      %none_among_sum(part, t) :
146	        {Nat.add(S.one_if(S.is_none(S.look(part, q))), S.none_among(part, t))
147	          == Nat.add(nf(B.at(Maybe<&2, Bool>, None{}, part, q)), _) : Nat}
148	      {==}
149	
150	# A full layout completing a partial one
151	# ======================================
152	
153	def beq(a: Bool, b: Bool) -> Bool:
154	  match a b:
155	    case True{} True{}:
156	      True{}
157	    case False{} False{}:
158	      True{}
159	    case True{} False{}:
160	      False{}
161	    case False{} True{}:
162	      False{}
163	
164	law beq_sound:
165	  for +a: Bool
166	  for +b: Bool
167	  for e: {beq(a, b) == True{} : Bool}
168	  {a == b : Bool}
169	
170	def beq_sound(a, b, e):
171	  match a b:
172	    case True{} True{}:
173	      {==}
174	    case False{} False{}:
175	      {==}
176	    case True{} False{}:
177	      Empty.absurd({True{} == False{} : Bool}, P.false_ne_true(e))
178	    case False{} True{}:
179	      Empty.absurd({False{} == True{} : Bool}, P.false_ne_true(e))
180	
181	law beq_refl:
182	  for +a: Bool
183	  {beq(a, a) == True{} : Bool}
184	
185	def beq_refl(a):
186	  match a:
187	    case True{}:
188	      {==}
189	    case False{}:
190	      {==}
191	
192	def cmp_cell(m: Maybe<&2, Bool>, b: Bool) -> Bool:
193	  match m:
194	    case None{}:
195	      True{}
196	    case Some{c}:
197	      beq(b, c)
198	
199	type CE is Data:
200	  CE{part: T.Grid(Maybe<&2, Bool>), layout: T.Grid(Bool)}
201	
202	def cmp_f.go(e: CE, +q: T.Pos) -> Bool:
203	  match e:
204	    case CE{part, layout}:
205	      cmp_cell(S.look(part, q), B.mine(layout, q))
206	
207	def cmp_f(e: CE, q: T.Pos) -> Bool:
208	  cmp_f.go(e, q)
209	
210	# The layout has every cell the partial layout fixes.
211	def completes(+w: Nat, +h: Nat, part: T.Grid(Maybe<&2, Bool>), layout: T.Grid(Bool)) -> Bool:
212	  PS.allp(~CE, ~cmp_f, CE{part, layout}, B.cells(w, h))
213	
214	law comp_cell:
215	  for +w: Nat
216	  for +h: Nat
217	  for +part: T.Grid(Maybe<&2, Bool>)
218	  for +layout: T.Grid(Bool)
219	  for comp: {completes(w, h, part, layout) == True{} : Bool}
220	  for +q: T.Pos
221	  for on: {B.on_board(w, h, q) == True{} : Bool}
222	  {cmp_cell(S.look(part, q), B.mine(layout, q)) == True{} : Bool}
223	
224	def comp_cell(w, h, part, layout, comp, q, on):
225	  PS.allp_member(~CE, ~cmp_f, CE{part, layout}, B.cells(w, h), q, comp, PS.cells_member(w, h, q, on))
226	
227	law cell_lo:
228	  for +m: Maybe<&2, Bool>
229	  for +b: Bool
230	  for c: {cmp_cell(m, b) == True{} : Bool}
231	  {Nat.is_le(tf(m), one(b)) == True{} : Bool}
232	
233	def cell_lo(m, b, c):
234	  match m:
235	    case None{}:
236	      P.le_zero_l(one(b))
237	    case Some{c0}:
238	      %Equal.sym(Bool, b, c0, beq_sound(b, c0, c)) : {Nat.is_le(S.one_if(c0), one(_)) == True{} : Bool}
239	      P.le_refl(one(c0))
240	
241	law cell_hi:
242	  for +m: Maybe<&2, Bool>
243	  for +b: Bool
244	  for c: {cmp_cell(m, b) == True{} : Bool}
245	  {Nat.is_le(one(b), Nat.add(tf(m), nf(m))) == True{} : Bool}
246	
247	def cell_hi(m, b, c):
248	  match m:
249	    case None{}:
250	      match b:
251	        case True{}:
252	          {==}
253	        case False{}:
254	          {==}
255	    case Some{c0}:
256	      %Equal.sym(Bool, b, c0, beq_sound(b, c0, c)) : {Nat.is_le(one(_), Nat.add(S.one_if(c0), 0n)) == True{} : Bool}
257	      P.le_of_add(one(c0), 0n)
258	
259	law among_lo:
260	  for +w: Nat
261	  for +h: Nat
262	  for +part: T.Grid(Maybe<&2, Bool>)
263	  for +layout: T.Grid(Bool)
264	  for +comp: {completes(w, h, part, layout) == True{} : Bool}
265	  for +ps: List<&2, T.Pos>
266	  for +ons: {PS.allp(~PS.WH, ~PS.onb, PS.WH{w, h}, ps) == True{} : Bool}
267	  {Nat.is_le(PU.csum(~Maybe<&2, Bool>, ~tf, None{}, part, ps), PU.csum(~Bool, ~one, False{}, layout, ps)) == True{} : Bool}
268	
269	def among_lo(w, h, part, layout, comp, ps, ons):
270	  match ps:
271	    case Nil{}:
272	      {==}
273	    case +q <> +t:
274	      +m = S.look(part, q)
275	      +b = B.mine(layout, q)
276	      P.le_add(tf(m), one(b), PU.csum(~Maybe<&2, Bool>, ~tf, None{}, part, t), PU.csum(~Bool, ~one, False{}, layout, t),
277	        cell_lo(m, b, comp_cell(w, h, part, layout, comp, q, PS.allp_head(~PS.WH, ~PS.onb, PS.WH{w, h}, q, t, ons))),
278	        among_lo(w, h, part, layout, comp, t, PS.allp_tail(~PS.WH, ~PS.onb, PS.WH{w, h}, q, t, ons)))
279	
280	law among_hi:
281	  for +w: Nat
282	  for +h: Nat
283	  for +part: T.Grid(Maybe<&2, Bool>)
284	  for +layout: T.Grid(Bool)
285	  for +comp: {completes(w, h, part, layout) == True{} : Bool}
286	  for +ps: List<&2, T.Pos>
287	  for +ons: {PS.allp(~PS.WH, ~PS.onb, PS.WH{w, h}, ps) == True{} : Bool}
288	  {Nat.is_le(PU.csum(~Bool, ~one, False{}, layout, ps),
289	    Nat.add(PU.csum(~Maybe<&2, Bool>, ~tf, None{}, part, ps), PU.csum(~Maybe<&2, Bool>, ~nf, None{}, part, ps))) == True{} : Bool}
290	
291	def among_hi(w, h, part, layout, comp, ps, ons):
292	  match ps:
293	    case Nil{}:
294	      {==}
295	    case +q <> +t:
296	      +m = S.look(part, q)
297	      +b = B.mine(layout, q)
298	      +tt = PU.csum(~Maybe<&2, Bool>, ~tf, None{}, part, t)
299	      +nt = PU.csum(~Maybe<&2, Bool>, ~nf, None{}, part, t)
300	      %Equal.sym(Nat, Nat.add(Nat.add(tf(m), tt), Nat.add(nf(m), nt)), Nat.add(Nat.add(tf(m), nf(m)), Nat.add(tt, nt)),
301	        P.add_swap(tf(m), tt, nf(m), nt)) :
302	        {Nat.is_le(Nat.add(one(b), PU.csum(~Bool, ~one, False{}, layout, t)), _) == True{} : Bool}
303	      P.le_add(one(b), Nat.add(tf(m), nf(m)), PU.csum(~Bool, ~one, False{}, layout, t), Nat.add(tt, nt),
304	        cell_hi(m, b, comp_cell(w, h, part, layout, comp, q, PS.allp_head(~PS.WH, ~PS.onb, PS.WH{w, h}, q, t, ons))),
305	        among_hi(w, h, part, layout, comp, t, PS.allp_tail(~PS.WH, ~PS.onb, PS.WH{w, h}, q, t, ons)))
306	
307	# Pruning only drops partial layouts that no consistent layout completes
308	# ======================================================================
309	
310	def item_onb(e: PS.WH, i: S.Item) -> Bool:
311	  match e i:
312	    case PS.WH{+w, +h} S.Item{p, s, ns}:
313	      B.on_board(w, h, p) && PS.allp(~PS.WH, ~PS.onb, PS.WH{w, h}, ns)
314	
315	# Every revealed cell of the items, and every cell its number counts, is on the board.
316	def items_onb(+e: PS.WH, its: List<&2, S.Item>) -> Bool:
317	  match its:
318	    case Nil{}:
319	      True{}
320	    case i <> t:
321	      item_onb(e, i) && items_onb(e, t)
322	
323	def sum_eq_cells(~A: Data, ~f: A -> Nat, +d: A, +w: Nat, +h: Nat, +g: T.Grid(A), +x: Nat,
324	  sh: {B.shaped(A, w, h, g) == True{} : Bool}, e: {x == PU.gsum(~A, ~f, g) : Nat}) ->
325	  {x == PU.csum(~A, ~f, d, g, B.cells(w, h)) : Nat}:
326	  Equal.trans(Nat, x, PU.gsum(~A, ~f, g), PU.csum(~A, ~f, d, g, B.cells(w, h)), e,
327	    Equal.sym(Nat, PU.csum(~A, ~f, d, g, B.cells(w, h)), PU.gsum(~A, ~f, g), PU.grid_sum(~A, ~f, d, w, h, g, sh)))
328	
329	def item_open_sound(+w: Nat, +h: Nat, +part: T.Grid(Maybe<&2, Bool>), +layout: T.Grid(Bool),
330	  +comp: {completes(w, h, part, layout) == True{} : Bool}, +p: T.Pos, +s: T.Seen, +ns: List<&2, T.Pos>,
331	  ok: {S.item_ok(s, p, ns, layout) == True{} : Bool},
332	  +on: {PS.allp(~PS.WH, ~PS.onb, PS.WH{w, h}, ns) == True{} : Bool}) ->
333	  {S.item_open(s, part, ns) == True{} : Bool}:
334	  match s:
335	    case T.Shown{k}:
336	      +c = B.count_mines(layout, ns)
337	      +ck = P.eq_sound(c, k, P.and_true_r(Bool.not(B.mine(layout, p)), Nat.is_eq(c, k), ok))
338	      %ck : {S.between(S.true_among(part, ns), S.none_among(part, ns), _) == True{} : Bool}
339	      %Equal.sym(Nat, S.true_among(part, ns), PU.csum(~Maybe<&2, Bool>, ~tf, None{}, part, ns), true_among_sum(part, ns)) :
340	        {S.between(_, S.none_among(part, ns), c) == True{} : Bool}
341	      %Equal.sym(Nat, S.none_among(part, ns), PU.csum(~Maybe<&2, Bool>, ~nf, None{}, part, ns), none_among_sum(part, ns)) :
342	        {S.between(PU.csum(~Maybe<&2, Bool>, ~tf, None{}, part, ns), _, c) == True{} : Bool}
343	      %Equal.sym(Nat, c, PU.csum(~Bool, ~one, False{}, layout, ns), count_sum(layout, ns)) :
344	        {S.between(PU.csum(~Maybe<&2, Bool>, ~tf, None{}, part, ns), PU.csum(~Maybe<&2, Bool>, ~nf, None{}, part, ns), _)
345	          == True{} : Bool}
346	      %Equal.sym(Bool, Nat.is_le(PU.csum(~Maybe<&2, Bool>, ~tf, None{}, part, ns), PU.csum(~Bool, ~one, False{}, layout, ns)),
347	        True{}, among_lo(w, h, part, layout, comp, ns, on)) :
348	        {Bool.and(_, Nat.is_le(PU.csum(~Bool, ~one, False{}, layout, ns),
349	          Nat.add(PU.csum(~Maybe<&2, Bool>, ~tf, None{}, part, ns), PU.csum(~Maybe<&2, Bool>, ~nf, None{}, part, ns)))) == True{} : Bool}
350	      among_hi(w, h, part, layout, comp, ns, on)
351	    case T.Hidden{}:
352	      {==}
353	    case T.Boom{}:
354	      {==}
355	
356	law items_open_sound:
357	  for +w: Nat
358	  for +h: Nat
359	  for +part: T.Grid(Maybe<&2, Bool>)
360	  for +layout: T.Grid(Bool)
361	  for +comp: {completes(w, h, part, layout) == True{} : Bool}
362	  for +rel: List<&2, S.Item>
363	  for +rok: {S.items_ok(rel, layout) == True{} : Bool}
364	  for +ron: {items_onb(PS.WH{w, h}, rel) == True{} : Bool}
365	  {S.items_open(part, rel) == True{} : Bool}
366	
367	def items_open_sound(w, h, part, layout, comp, rel, rok, ron):
368	  match rel:
369	    case Nil{}:
370	      {==}
371	    case S.Item{p, s, ns} <> t:
372	      +i = {S.Item{p, s, ns} : S.Item}
373	      +io = item_onb(PS.WH{w, h}, i)
374	      +ok1 = S.item_ok(s, p, ns, layout)
375	      %Equal.sym(Bool, S.item_open(s, part, ns), True{},
376	        item_open_sound(w, h, part, layout, comp, p, s, ns, P.and_true_l(ok1, S.items_ok(t, layout), rok),
377	          P.and_true_r(B.on_board(w, h, p), PS.allp(~PS.WH, ~PS.onb, PS.WH{w, h}, ns),
378	            P.and_true_l(io, items_onb(PS.WH{w, h}, t), ron)))) :
379	        {Bool.and(_, S.items_open(part, t)) == True{} : Bool}
380	      items_open_sound(w, h, part, layout, comp, t, P.and_true_r(ok1, S.items_ok(t, layout), rok),
381	        P.and_true_r(io, items_onb(PS.WH{w, h}, t), ron))
382	
383	# A partial layout that a consistent layout completes is never pruned.
384	law open_ok_sound:
385	  for +w: Nat
386	  for +h: Nat
387	  for +n: Nat
388	  for +part: T.Grid(Maybe<&2, Bool>)
389	  for +rel: List<&2, S.Item>
390	  for +layout: T.Grid(Bool)
391	  for +shP: {B.shaped(Maybe<&2, Bool>, w, h, part) == True{} : Bool}
392	  for +shL: {B.shaped(Bool, w, h, layout) == True{} : Bool}
393	  for +comp: {completes(w, h, part, layout) == True{} : Bool}
394	  for tot: {B.total_mines(layout) == n : Nat}
395	  for rok: {S.items_ok(rel, layout) == True{} : Bool}
396	  for ron: {items_onb(PS.WH{w, h}, rel) == True{} : Bool}
397	  {S.open_ok(part, rel, n) == True{} : Bool}
398	
399	def open_ok_sound(w, h, n, part, rel, layout, shP, shL, comp, tot, rok, ron):
400	  +pt = sum_eq_cells(~Maybe<&2, Bool>, ~tf, None{}, w, h, part, S.part_true(part), shP, part_true_sum(part))
401	  +pn = sum_eq_cells(~Maybe<&2, Bool>, ~nf, None{}, w, h, part, S.part_none(part), shP, part_none_sum(part))
402	  +nc = sum_eq_cells(~Bool, ~one, False{}, w, h, layout, n, shL,
403	    Equal.trans(Nat, n, B.total_mines(layout), PU.gsum(~Bool, ~one, layout), Equal.sym(Nat, B.total_mines(layout), n, tot),
404	      total_sum(layout)))
405	  +T0 = PU.csum(~Maybe<&2, Bool>, ~tf, None{}, part, B.cells(w, h))
406	  +N0 = PU.csum(~Maybe<&2, Bool>, ~nf, None{}, part, B.cells(w, h))
407	  +C0 = PU.csum(~Bool, ~one, False{}, layout, B.cells(w, h))
408	  %Equal.sym(Bool, S.items_open(part, rel), True{}, items_open_sound(w, h, part, layout, comp, rel, rok, ron)) :
409	    {Bool.and(S.between(S.part_true(part), S.part_none(part), n), _) == True{} : Bool}
410	  %Equal.sym(Nat, S.part_true(part), T0, pt) : {Bool.and(S.between(_, S.part_none(part), n), True{}) == True{} : Bool}
411	  %Equal.sym(Nat, S.part_none(part), N0, pn) : {Bool.and(S.between(T0, _, n), True{}) == True{} : Bool}
412	  %Equal.sym(Nat, n, C0, nc) : {Bool.and(S.between(T0, N0, _), True{}) == True{} : Bool}
413	  %Equal.sym(Bool, Nat.is_le(T0, C0), True{}, among_lo(w, h, part, layout, comp, B.cells(w, h), PS.cells_on(w, h))) :
414	    {Bool.and(Bool.and(_, Nat.is_le(C0, Nat.add(T0, N0))), True{}) == True{} : Bool}
415	  %Equal.sym(Bool, Nat.is_le(C0, Nat.add(T0, N0)), True{}, among_hi(w, h, part, layout, comp, B.cells(w, h), PS.cells_on(w, h))) :
416	    {Bool.and(Bool.and(True{}, _), True{}) == True{} : Bool}
417	  {==}
418	
419	# Filling in a partial layout
420	# ===========================
421	
422	law fill_rows_get:
423	  for +g: T.Grid(Maybe<&2, Bool>)
424	  for +y: Nat
425	  {Maybe.default(&2, List<&2, Bool>, List.get(&2, List<&2, Bool>, S.fill(g), y), Nil{})
426	    == S.fill.row(Maybe.default(&2, List<&2, Maybe<&2, Bool>>, List.get(&2, List<&2, Maybe<&2, Bool>>, g, y), Nil{}))
427	    : List<&2, Bool>}
428	
429	def fill_rows_get(g, y):
430	  match g y:
431	    case Nil{} _:
432	      {==}
433	    case r <> t 0n:
434	      {==}
435	    case r <> t 1n+k:
436	      fill_rows_get(t, k)
437	
438	law fill_row_get:
439	  for +r: List<&2, Maybe<&2, Bool>>
440	  for +x: Nat
441	  {Maybe.default(&2, Bool, List.get(&2, Bool, S.fill.row(r), x), False{})
442	    == Maybe.default(&2, Bool, Maybe.default(&2, Maybe<&2, Bool>, List.get(&2, Maybe<&2, Bool>, r, x), None{}), False{}) : Bool}
443	
444	def fill_row_get(r, x):
445	  match r x:
446	    case Nil{} _:
447	      {==}
448	    case m <> t 0n:
449	      {==}
450	    case m <> t 1n+k:
451	      fill_row_get(t, k)
452	
453	# A filled-in cell holds what the partial layout fixed (False if nothing).
454	law fill_at:
455	  for +part: T.Grid(Maybe<&2, Bool>)
456	  for +q: T.Pos
457	  {B.mine(S.fill(part), q) == Maybe.default(&2, Bool, S.look(part, q), False{}) : Bool}
458	
459	def fill_at(part, q):
460	  match q:
461	    case T.Pos{x, y}:
462	      %Equal.sym(List<&2, Bool>, Maybe.default(&2, List<&2, Bool>, List.get(&2, List<&2, Bool>, S.fill(part), y), Nil{}),
463	        S.fill.row(Maybe.default(&2, List<&2, Maybe<&2, Bool>>, List.get(&2, List<&2, Maybe<&2, Bool>>, part, y), Nil{})),
464	        fill_rows_get(part, y)) :
465	        {Maybe.default(&2, Bool, List.get(&2, Bool, _, x), False{})
466	          == Maybe.default(&2, Bool, S.look(part, T.Pos{x, y}), False{}) : Bool}
467	      fill_row_get(Maybe.default(&2, List<&2, Maybe<&2, Bool>>, List.get(&2, List<&2, Maybe<&2, Bool>>, part, y), Nil{}), x)
468	
469	law fill_row_len:
470	  for +r: List<&2, Maybe<&2, Bool>>
471	  {List.length(&2, Bool, S.fill.row(r)) == List.length(&2, Maybe<&2, Bool>, r) : Nat}
472	
473	def fill_row_len(r):
474	  match r:
475	    case Nil{}:
476	      {==}
477	    case m <> t:
478	      %Equal.sym(Nat, List.length(&2, Bool, S.fill.row(t)), List.length(&2, Maybe<&2, Bool>, t), fill_row_len(t)) :
479	        {1n+_ == 1n+List.length(&2, Maybe<&2, Bool>, t) : Nat}
480	      {==}
481	
482	law fill_len:
483	  for +g: T.Grid(Maybe<&2, Bool>)
484	  {List.length(&2, List<&2, Bool>, S.fill(g)) == List.length(&2, List<&2, Maybe<&2, Bool>>, g) : Nat}
485	
486	def fill_len(g):
487	  match g:
488	    case Nil{}:
489	      {==}
490	    case r <> t:
491	      %Equal.sym(Nat, List.length(&2, List<&2, Bool>, S.fill(t)), List.length(&2, List<&2, Maybe<&2, Bool>>, t), fill_len(t)) :
492	        {1n+_ == 1n+List.length(&2, List<&2, Maybe<&2, Bool>>, t) : Nat}
493	      {==}
494	
495	law fill_wide:
496	  for +w: Nat
497	  for +g: T.Grid(Maybe<&2, Bool>)
498	  {B.rows_wide(Bool, w, S.fill(g)) == B.rows_wide(Maybe<&2, Bool>, w, g) : Bool}
499	
500	def fill_wide(w, g):
501	  match g:
502	    case Nil{}:
503	      {==}
504	    case r <> t:
505	      %Equal.sym(Nat, List.length(&2, Bool, S.fill.row(r)), List.length(&2, Maybe<&2, Bool>, r), fill_row_len(r)) :
506	        {Bool.and(Nat.is_eq(_, w), B.rows_wide(Bool, w, S.fill(t)))
507	          == Bool.and(Nat.is_eq(List.length(&2, Maybe<&2, Bool>, r), w), B.rows_wide(Maybe<&2, Bool>, w, t)) : Bool}
508	      %Equal.sym(Bool, B.rows_wide(Bool, w, S.fill(t)), B.rows_wide(Maybe<&2, Bool>, w, t), fill_wide(w, t)) :
509	        {Bool.and(Nat.is_eq(List.length(&2, Maybe<&2, Bool>, r), w), _)
510	          == Bool.and(Nat.is_eq(List.length(&2, Maybe<&2, Bool>, r), w), B.rows_wide(Maybe<&2, Bool>, w, t)) : Bool}
511	      {==}
512	
513	law fill_shaped:
514	  for +w: Nat
515	  for +h: Nat
516	  for +g: T.Grid(Maybe<&2, Bool>)
517	  {B.shaped(Bool, w, h, S.fill(g)) == B.shaped(Maybe<&2, Bool>, w, h, g) : Bool}
518	
519	def fill_shaped(w, h, g):
520	  %Equal.sym(Nat, List.length(&2, List<&2, Bool>, S.fill(g)), List.length(&2, List<&2, Maybe<&2, Bool>>, g), fill_len(g)) :
521	    {Bool.and(Nat.is_eq(_, h), B.rows_wide(Bool, w, S.fill(g)))
522	      == Bool.and(Nat.is_eq(List.length(&2, List<&2, Maybe<&2, Bool>>, g), h), B.rows_wide(Maybe<&2, Bool>, w, g)) : Bool}
523	  %Equal.sym(Bool, B.rows_wide(Bool, w, S.fill(g)), B.rows_wide(Maybe<&2, Bool>, w, g), fill_wide(w, g)) :
524	    {Bool.and(Nat.is_eq(List.length(&2, List<&2, Maybe<&2, Bool>>, g), h), _)
525	      == Bool.and(Nat.is_eq(List.length(&2, List<&2, Maybe<&2, Bool>>, g), h), B.rows_wide(Maybe<&2, Bool>, w, g)) : Bool}
526	  {==}
527	
528	# Two layouts that agree cell by cell
529	# ===================================
530	
531	type AG is Data:
532	  AG{l1: T.Grid(Bool), l2: T.Grid(Bool)}
533	
534	def ag_f.go(e: AG, +q: T.Pos) -> Bool:
535	  match e:
536	    case AG{l1, l2}:
537	      beq(B.mine(l1, q), B.mine(l2, q))
538	
539	def ag_f(e: AG, q: T.Pos) -> Bool:
540	  ag_f.go(e, q)
541	
542	def agree(+w: Nat, +h: Nat, l1: T.Grid(Bool), l2: T.Grid(Bool)) -> Bool:
543	  PS.allp(~AG, ~ag_f, AG{l1, l2}, B.cells(w, h))
544	
545	law agree_cell:
546	  for +w: Nat
547	  for +h: Nat
548	  for +l1: T.Grid(Bool)
549	  for +l2: T.Grid(Bool)
550	  for ag: {agree(w, h, l1, l2) == True{} : Bool}
551	  for +q: T.Pos
552	  for on: {B.on_board(w, h, q) == True{} : Bool}
553	  {B.mine(l1, q) == B.mine(l2, q) : Bool}
554	
555	def agree_cell(w, h, l1, l2, ag, q, on):
556	  beq_sound(B.mine(l1, q), B.mine(l2, q),
557	    PS.allp_member(~AG, ~ag_f, AG{l1, l2}, B.cells(w, h), q, ag, PS.cells_member(w, h, q, on)))
558	
559	law count_agree:
560	  for +w: Nat
561	  for +h: Nat
562	  for +l1: T.Grid(Bool)
563	  for +l2: T.Grid(Bool)
564	  for +ag: {agree(w, h, l1, l2) == True{} : Bool}
565	  for +ps: List<&2, T.Pos>
566	  for +ons: {PS.allp(~PS.WH, ~PS.onb, PS.WH{w, h}, ps) == True{} : Bool}
567	  {B.count_mines(l1, ps) == B.count_mines(l2, ps) : Nat}
568	
569	def count_agree(w, h, l1, l2, ag, ps, ons):
570	  match ps:
571	    case Nil{}:
572	      {==}
573	    case +q <> +t:
574	      %Equal.sym(Bool, B.mine(l1, q), B.mine(l2, q), agree_cell(w, h, l1, l2, ag, q, PS.allp_head(~PS.WH, ~PS.onb, PS.WH{w, h}, q, t, ons))) :
575	        {Nat.add(Bool.pick(Nat, _, 1n, 0n), B.count_mines(l1, t)) == Nat.add(Bool.pick(Nat, B.mine(l2, q), 1n, 0n), B.count_mines(l2, t)) : Nat}
576	      %Equal.sym(Nat, B.count_mines(l1, t), B.count_mines(l2, t),
577	        count_agree(w, h, l1, l2, ag, t, PS.allp_tail(~PS.WH, ~PS.onb, PS.WH{w, h}, q, t, ons))) :
578	        {Nat.add(Bool.pick(Nat, B.mine(l2, q), 1n, 0n), _) == Nat.add(Bool.pick(Nat, B.mine(l2, q), 1n, 0n), B.count_mines(l2, t)) : Nat}
579	      {==}
580	
581	law total_cells:
582	  for +w: Nat
583	  for +h: Nat
584	  for +l: T.Grid(Bool)
585	  for sh: {B.shaped(Bool, w, h, l) == True{} : Bool}
586	  {B.total_mines(l) == B.count_mines(l, B.cells(w, h)) : Nat}
587	
588	def total_cells(w, h, l, sh):
589	  Equal.trans(Nat, B.total_mines(l), PU.gsum(~Bool, ~one, l), B.count_mines(l, B.cells(w, h)), total_sum(l),
590	    Equal.trans(Nat, PU.gsum(~Bool, ~one, l), PU.csum(~Bool, ~one, False{}, l, B.cells(w, h)), B.count_mines(l, B.cells(w, h)),
591	      Equal.sym(Nat, PU.csum(~Bool, ~one, False{}, l, B.cells(w, h)), PU.gsum(~Bool, ~one, l), PU.grid_sum(~Bool, ~one, False{}, w, h, l, sh)),
592	      Equal.sym(Nat, B.count_mines(l, B.cells(w, h)), PU.csum(~Bool, ~one, False{}, l, B.cells(w, h)), count_sum(l, B.cells(w, h)))))
593	
594	law total_agree:
595	  for +w: Nat
596	  for +h: Nat
597	  for +l1: T.Grid(Bool)
598	  for +l2: T.Grid(Bool)
599	  for sh1: {B.shaped(Bool, w, h, l1) == True{} : Bool}
600	  for sh2: {B.shaped(Bool, w, h, l2) == True{} : Bool}
601	  for +ag: {agree(w, h, l1, l2) == True{} : Bool}
602	  {B.total_mines(l1) == B.total_mines(l2) : Nat}
603	
604	def total_agree(w, h, l1, l2, sh1, sh2, ag):
605	  Equal.trans(Nat, B.total_mines(l1), B.count_mines(l1, B.cells(w, h)), B.total_mines(l2), total_cells(w, h, l1, sh1),
606	    Equal.trans(Nat, B.count_mines(l1, B.cells(w, h)), B.count_mines(l2, B.cells(w, h)), B.total_mines(l2),
607	      count_agree(w, h, l1, l2, ag, B.cells(w, h), PS.cells_on(w, h)),
608	      Equal.sym(Nat, B.total_mines(l2), B.count_mines(l2, B.cells(w, h)), total_cells(w, h, l2, sh2))))
609	
610	def item_ok_agree(+w: Nat, +h: Nat, +l1: T.Grid(Bool), +l2: T.Grid(Bool), +ag: {agree(w, h, l1, l2) == True{} : Bool},
611	  +p: T.Pos, +s: T.Seen, +ns: List<&2, T.Pos>, on: {B.on_board(w, h, p) == True{} : Bool},
612	  ons: {PS.allp(~PS.WH, ~PS.onb, PS.WH{w, h}, ns) == True{} : Bool}) ->
613	  {S.item_ok(s, p, ns, l1) == S.item_ok(s, p, ns, l2) : Bool}:
614	  match s:
615	    case T.Hidden{}:
616	      {==}
617	    case T.Shown{k}:
618	      %Equal.sym(Bool, B.mine(l1, p), B.mine(l2, p), agree_cell(w, h, l1, l2, ag, p, on)) :
619	        {Bool.and(Bool.not(_), Nat.is_eq(B.count_mines(l1, ns), k)) == Bool.and(Bool.not(B.mine(l2, p)), Nat.is_eq(B.count_mines(l2, ns), k)) : Bool}
620	      %Equal.sym(Nat, B.count_mines(l1, ns), B.count_mines(l2, ns), count_agree(w, h, l1, l2, ag, ns, ons)) :
621	        {Bool.and(Bool.not(B.mine(l2, p)), Nat.is_eq(_, k)) == Bool.and(Bool.not(B.mine(l2, p)), Nat.is_eq(B.count_mines(l2, ns), k)) : Bool}
622	      {==}
623	    case T.Boom{}:
624	      agree_cell(w, h, l1, l2, ag, p, on)
625	
626	law items_ok_agree:
627	  for +w: Nat
628	  for +h: Nat
629	  for +l1: T.Grid(Bool)
630	  for +l2: T.Grid(Bool)
631	  for +ag: {agree(w, h, l1, l2) == True{} : Bool}
632	  for +its: List<&2, S.Item>
633	  for +ion: {items_onb(PS.WH{w, h}, its) == True{} : Bool}
634	  {S.items_ok(its, l1) == S.items_ok(its, l2) : Bool}
635	
636	def items_ok_agree(w, h, l1, l2, ag, its, ion):
637	  match its:
638	    case Nil{}:
639	      {==}
640	    case S.Item{p, s, ns} <> t:
641	      +io = item_onb(PS.WH{w, h}, S.Item{p, s, ns})
642	      +io1 = P.and_true_l(io, items_onb(PS.WH{w, h}, t), ion)
643	      %Equal.sym(Bool, S.item_ok(s, p, ns, l1), S.item_ok(s, p, ns, l2),
644	        item_ok_agree(w, h, l1, l2, ag, p, s, ns,
645	          P.and_true_l(B.on_board(w, h, p), PS.allp(~PS.WH, ~PS.onb, PS.WH{w, h}, ns), io1),
646	          P.and_true_r(B.on_board(w, h, p), PS.allp(~PS.WH, ~PS.onb, PS.WH{w, h}, ns), io1))) :
647	        {Bool.and(_, S.items_ok(t, l1)) == Bool.and(S.item_ok(s, p, ns, l2), S.items_ok(t, l2)) : Bool}
648	      %Equal.sym(Bool, S.items_ok(t, l1), S.items_ok(t, l2),
649	        items_ok_agree(w, h, l1, l2, ag, t, P.and_true_r(io, items_onb(PS.WH{w, h}, t), ion))) :
650	        {Bool.and(S.item_ok(s, p, ns, l2), _) == Bool.and(S.item_ok(s, p, ns, l2), S.items_ok(t, l2)) : Bool}
651	      {==}
652	
653	law check_agree:
654	  for +w: Nat
655	  for +h: Nat
656	  for +n: Nat
657	  for +rows: T.Grid(T.Seen)
658	  for +its: List<&2, S.Item>
659	  for +l1: T.Grid(Bool)
660	  for +l2: T.Grid(Bool)
661	  for +sh1: {B.shaped(Bool, w, h, l1) == True{} : Bool}
662	  for +sh2: {B.shaped(Bool, w, h, l2) == True{} : Bool}
663	  for +ag: {agree(w, h, l1, l2) == True{} : Bool}
664	  for +ion: {items_onb(PS.WH{w, h}, its) == True{} : Bool}
665	  {S.check(S.Ctx{w, h, n, rows, its}, l1) == S.check(S.Ctx{w, h, n, rows, its}, l2) : Bool}
666	
667	def check_agree(w, h, n, rows, its, l1, l2, sh1, sh2, ag, ion):
668	  +sr = B.shaped(T.Seen, w, h, rows)
669	  %Equal.sym(Bool, B.shaped(Bool, w, h, l1), True{}, sh1) :
670	    {Bool.and(Bool.and(Bool.and(_, sr), Nat.is_eq(B.total_mines(l1), n)), S.items_ok(its, l1))
671	      == Bool.and(Bool.and(Bool.and(B.shaped(Bool, w, h, l2), sr), Nat.is_eq(B.total_mines(l2), n)), S.items_ok(its, l2)) : Bool}
672	  %Equal.sym(Bool, B.shaped(Bool, w, h, l2), True{}, sh2) :
673	    {Bool.and(Bool.and(Bool.and(True{}, sr), Nat.is_eq(B.total_mines(l1), n)), S.items_ok(its, l1))
674	      == Bool.and(Bool.and(Bool.and(_, sr), Nat.is_eq(B.total_mines(l2), n)), S.items_ok(its, l2)) : Bool}
675	  %Equal.sym(Nat, B.total_mines(l1), B.total_mines(l2), total_agree(w, h, l1, l2, sh1, sh2, ag)) :
676	    {Bool.and(Bool.and(Bool.and(True{}, sr), Nat.is_eq(_, n)), S.items_ok(its, l1))
677	      == Bool.and(Bool.and(Bool.and(True{}, sr), Nat.is_eq(B.total_mines(l2), n)), S.items_ok(its, l2)) : Bool}
678	  %Equal.sym(Bool, S.items_ok(its, l1), S.items_ok(its, l2), items_ok_agree(w, h, l1, l2, ag, its, ion)) :
679	    {Bool.and(Bool.and(Bool.and(True{}, sr), Nat.is_eq(B.total_mines(l2), n)), _)
680	      == Bool.and(Bool.and(Bool.and(True{}, sr), Nat.is_eq(B.total_mines(l2), n)), S.items_ok(its, l2)) : Bool}
681	  {==}
682	
683	# Coverage by the to-do list
684	# ==========================
685	
686	def tcontains(ts: List<&2, S.Todo>, +q: T.Pos) -> Bool:
687	  match ts:
688	    case Nil{}:
689	      False{}
690	    case S.Todo{c, rel} <> t:
691	      B.same(c, q) || tcontains(t, q)
692	
693	type CV is Data:
694	  CV{todo: List<&2, S.Todo>, part: T.Grid(Maybe<&2, Bool>)}
695	
696	def cv_f.go(e: CV, +q: T.Pos) -> Bool:
697	  match e:
698	    case CV{todo, part}:
699	      Bool.not(S.is_none(S.look(part, q))) || tcontains(todo, q)
700	
701	def cv_f(e: CV, q: T.Pos) -> Bool:
702	  cv_f.go(e, q)
703	
704	# Every unassigned cell of the board is still to do.
705	def covers(+w: Nat, +h: Nat, todo: List<&2, S.Todo>, part: T.Grid(Maybe<&2, Bool>)) -> Bool:
706	  PS.allp(~CV, ~cv_f, CV{todo, part}, B.cells(w, h))
707	
708	def todos_ok(ts: List<&2, S.Todo>, +layout: T.Grid(Bool)) -> Bool:
709	  match ts:
710	    case Nil{}:
711	      True{}
712	    case S.Todo{c, rel} <> t:
713	      S.items_ok(rel, layout) && todos_ok(t, layout)
714	
715	def todos_onb(+e: PS.WH, ts: List<&2, S.Todo>) -> Bool:
716	  match ts:
717	    case Nil{}:
718	      True{}
719	    case S.Todo{c, rel} <> t:
720	      items_onb(e, rel) && todos_onb(e, t)
721	
722	def covers_skip.cell(+c: T.Pos, +rel: List<&2, S.Item>, +rest: List<&2, S.Todo>, +part: T.Grid(Maybe<&2, Bool>),
723	  +q: T.Pos, fr: {S.is_none(S.look(part, c)) == False{} : Bool},
724	  h: {cv_f(CV{S.Todo{c, rel} <> rest, part}, q) == True{} : Bool}, +b: Bool, be: {B.same(c, q) == b : Bool}) ->
725	  {cv_f(CV{rest, part}, q) == True{} : Bool}:
726	  match b:
727	    case True{}:
728	      %PG.same_sound(c, q, be) :
729	        {Bool.or(Bool.not(S.is_none(S.look(part, _))), tcontains(rest, _)) == True{} : Bool}
730	      %Equal.sym(Bool, S.is_none(S.look(part, c)), False{}, fr) :
731	        {Bool.or(Bool.not(_), tcontains(rest, c)) == True{} : Bool}
732	      {==}
733	    case False{}:
734	      %be : {Bool.or(Bool.not(S.is_none(S.look(part, q))), Bool.or(_, tcontains(rest, q))) == True{} : Bool}; h
735	
736	law covers_skip:
737	  for +c: T.Pos
738	  for +rel: List<&2, S.Item>
739	  for +rest: List<&2, S.Todo>
740	  for +part: T.Grid(Maybe<&2, Bool>)
741	  for +fr: {S.is_none(S.look(part, c)) == False{} : Bool}
742	  for +ps: List<&2, T.Pos>
743	  for +cv: {PS.allp(~CV, ~cv_f, CV{S.Todo{c, rel} <> rest, part}, ps) == True{} : Bool}
744	  {PS.allp(~CV, ~cv_f, CV{rest, part}, ps) == True{} : Bool}
745	
746	def covers_skip(c, rel, rest, part, fr, ps, cv):
747	  match ps:
748	    case Nil{}:
749	      {==}
750	    case +q <> +t:
751	      +e0 = {CV{S.Todo{c, rel} <> rest, part} : CV}
752	      %Equal.sym(Bool, cv_f(CV{rest, part}, q), True{},
753	        covers_skip.cell(c, rel, rest, part, q, fr, PS.allp_head(~CV, ~cv_f, e0, q, t, cv), B.same(c, q), {==})) :
754	        {Bool.and(_, PS.allp(~CV, ~cv_f, CV{rest, part}, t)) == True{} : Bool}
755	      covers_skip(c, rel, rest, part, fr, t, PS.allp_tail(~CV, ~cv_f, e0, q, t, cv))
756	
757	def set_look(+w: Nat, +h: Nat, +part: T.Grid(Maybe<&2, Bool>), +q: T.Pos, +v: Maybe<&2, Bool>,
758	  sh: {B.shaped(Maybe<&2, Bool>, w, h, part) == True{} : Bool}, on: {B.on_board(w, h, q) == True{} : Bool}) ->
759	  {S.look(B.set_at(Maybe<&2, Bool>, part, q, v), q) == v : Maybe<&2, Bool>}:
760	  match q:
761	    case T.Pos{x, y}:
762	      PL.at_set_eq(Maybe<&2, Bool>, w, h, part, x, y, v, None{}, sh, on)
763	
764	def covers_set.cell(+w: Nat, +h: Nat, +c: T.Pos, +rel: List<&2, S.Item>, +rest: List<&2, S.Todo>,
765	  +part: T.Grid(Maybe<&2, Bool>), +bv: Bool, +shP: {B.shaped(Maybe<&2, Bool>, w, h, part) == True{} : Bool},
766	  +q: T.Pos, on: {B.on_board(w, h, q) == True{} : Bool},
767	  h0: {cv_f(CV{S.Todo{c, rel} <> rest, part}, q) == True{} : Bool}, +b: Bool, +be: {B.same(c, q) == b : Bool}) ->
768	  {cv_f(CV{rest, B.set_at(Maybe<&2, Bool>, part, c, Some{bv})}, q) == True{} : Bool}:
769	  match b:
770	    case True{}:
771	      %Equal.sym(T.Pos, c, q, PG.same_sound(c, q, be)) :
772	        {Bool.or(Bool.not(S.is_none(S.look(B.set_at(Maybe<&2, Bool>, part, _, Some{bv}), q))), tcontains(rest, q)) == True{} : Bool}
773	      %Equal.sym(Maybe<&2, Bool>, S.look(B.set_at(Maybe<&2, Bool>, part, q, Some{bv}), q), Some{bv},
774	        set_look(w, h, part, q, Some{bv}, shP, on)) :
775	        {Bool.or(Bool.not(S.is_none(_)), tcontains(rest, q)) == True{} : Bool}
776	      {==}
777	    case False{}:
778	      %Equal.sym(Maybe<&2, Bool>, S.look(B.set_at(Maybe<&2, Bool>, part, c, Some{bv}), q), S.look(part, q),
779	        PL.at_set_ne(Maybe<&2, Bool>, part, c, q, Some{bv}, None{}, be)) :
780	        {Bool.or(Bool.not(S.is_none(_)), tcontains(rest, q)) == True{} : Bool}
781	      %be : {Bool.or(Bool.not(S.is_none(S.look(part, q))), Bool.or(_, tcontains(rest, q))) == True{} : Bool}; h0
782	
783	law covers_set:
784	  for +w: Nat
785	  for +h: Nat
786	  for +c: T.Pos
787	  for +rel: List<&2, S.Item>
788	  for +rest: List<&2, S.Todo>
789	  for +part: T.Grid(Maybe<&2, Bool>)
790	  for +bv: Bool
791	  for +shP: {B.shaped(Maybe<&2, Bool>, w, h, part) == True{} : Bool}
792	  for +ps: List<&2, T.Pos>
793	  for +ons: {PS.allp(~PS.WH, ~PS.onb, PS.WH{w, h}, ps) == True{} : Bool}
794	  for +cv: {PS.allp(~CV, ~cv_f, CV{S.Todo{c, rel} <> rest, part}, ps) == True{} : Bool}
795	  {PS.allp(~CV, ~cv_f, CV{rest, B.set_at(Maybe<&2, Bool>, part, c, Some{bv})}, ps) == True{} : Bool}
796	
797	def covers_set(w, h, c, rel, rest, part, bv, shP, ps, ons, cv):
798	  match ps:
799	    case Nil{}:
800	      {==}
801	    case +q <> +t:
802	      +e0 = {CV{S.Todo{c, rel} <> rest, part} : CV}
803	      +e1 = {CV{rest, B.set_at(Maybe<&2, Bool>, part, c, Some{bv})} : CV}
804	      %Equal.sym(Bool, cv_f(e1, q), True{},
805	        covers_set.cell(w, h, c, rel, rest, part, bv, shP, q, PS.allp_head(~PS.WH, ~PS.onb, PS.WH{w, h}, q, t, ons),
806	          PS.allp_head(~CV, ~cv_f, e0, q, t, cv), B.same(c, q), {==})) :
807	        {Bool.and(_, PS.allp(~CV, ~cv_f, e1, t)) == True{} : Bool}
808	      covers_set(w, h, c, rel, rest, part, bv, shP, t, PS.allp_tail(~PS.WH, ~PS.onb, PS.WH{w, h}, q, t, ons),
809	        PS.allp_tail(~CV, ~cv_f, e0, q, t, cv))
810	
811	def comp_set.cell(+w: Nat, +h: Nat, +c: T.Pos, +part: T.Grid(Maybe<&2, Bool>), +layout: T.Grid(Bool), +bv: Bool,
812	  +shP: {B.shaped(Maybe<&2, Bool>, w, h, part) == True{} : Bool}, mc: {B.mine(layout, c) == bv : Bool},
813	  +q: T.Pos, on: {B.on_board(w, h, q) == True{} : Bool},
814	  h0: {cmp_f(CE{part, layout}, q) == True{} : Bool}, +b: Bool, +be: {B.same(c, q) == b : Bool}) ->
815	  {cmp_f(CE{B.set_at(Maybe<&2, Bool>, part, c, Some{bv}), layout}, q) == True{} : Bool}:
816	  match b:
817	    case True{}:
818	      %Equal.sym(T.Pos, c, q, PG.same_sound(c, q, be)) :
819	        {cmp_cell(S.look(B.set_at(Maybe<&2, Bool>, part, _, Some{bv}), q), B.mine(layout, q)) == True{} : Bool}
820	      %Equal.sym(Maybe<&2, Bool>, S.look(B.set_at(Maybe<&2, Bool>, part, q, Some{bv}), q), Some{bv},
821	        set_look(w, h, part, q, Some{bv}, shP, on)) :
822	        {cmp_cell(_, B.mine(layout, q)) == True{} : Bool}
823	      %PG.same_sound(c, q, be) : {beq(B.mine(layout, _), bv) == True{} : Bool}
824	      %Equal.sym(Bool, B.mine(layout, c), bv, mc) : {beq(_, bv) == True{} : Bool}
825	      beq_refl(bv)
826	    case False{}:
827	      %Equal.sym(Maybe<&2, Bool>, S.look(B.set_at(Maybe<&2, Bool>, part, c, Some{bv}), q), S.look(part, q),
828	        PL.at_set_ne(Maybe<&2, Bool>, part, c, q, Some{bv}, None{}, be)) :
829	        {cmp_cell(_, B.mine(layout, q)) == True{} : Bool}
830	      h0
831	
832	law comp_set:
833	  for +w: Nat
834	  for +h: Nat
835	  for +c: T.Pos
836	  for +part: T.Grid(Maybe<&2, Bool>)
837	  for +layout: T.Grid(Bool)
838	  for +bv: Bool
839	  for +shP: {B.shaped(Maybe<&2, Bool>, w, h, part) == True{} : Bool}
840	  for +mc: {B.mine(layout, c) == bv : Bool}
841	  for +ps: List<&2, T.Pos>
842	  for +ons: {PS.allp(~PS.WH, ~PS.onb, PS.WH{w, h}, ps) == True{} : Bool}
843	  for +cm: {PS.allp(~CE, ~cmp_f, CE{part, layout}, ps) == True{} : Bool}
844	  {PS.allp(~CE, ~cmp_f, CE{B.set_at(Maybe<&2, Bool>, part, c, Some{bv}), layout}, ps) == True{} : Bool}
845	
846	def comp_set(w, h, c, part, layout, bv, shP, mc, ps, ons, cm):
847	  match ps:
848	    case Nil{}:
849	      {==}
850	    case +q <> +t:
851	      +e0 = {CE{part, layout} : CE}
852	      +e1 = {CE{B.set_at(Maybe<&2, Bool>, part, c, Some{bv}), layout} : CE}
853	      %Equal.sym(Bool, cmp_f(e1, q), True{},
854	        comp_set.cell(w, h, c, part, layout, bv, shP, mc, q, PS.allp_head(~PS.WH, ~PS.onb, PS.WH{w, h}, q, t, ons),
855	          PS.allp_head(~CE, ~cmp_f, e0, q, t, cm), B.same(c, q), {==})) :
856	        {Bool.and(_, PS.allp(~CE, ~cmp_f, e1, t)) == True{} : Bool}
857	      comp_set(w, h, c, part, layout, bv, shP, mc, t, PS.allp_tail(~PS.WH, ~PS.onb, PS.WH{w, h}, q, t, ons),
858	        PS.allp_tail(~CE, ~cmp_f, e0, q, t, cm))
859	
860	# The search is complete
861	# ======================
862	
863	def leaf_cell.go(+part: T.Grid(Maybe<&2, Bool>), +layout: T.Grid(Bool), +q: T.Pos, +m: Maybe<&2, Bool>,
864	  me: {S.look(part, q) == m : Maybe<&2, Bool>},
865	  cv: {Bool.not(S.is_none(m)) == True{} : Bool}, cm: {cmp_cell(m, B.mine(layout, q)) == True{} : Bool}) ->
866	  {beq(B.mine(S.fill(part), q), B.mine(layout, q)) == True{} : Bool}:
867	  match m:
868	    case None{}:
869	      Empty.absurd({beq(B.mine(S.fill(part), q), B.mine(layout, q)) == True{} : Bool}, P.false_ne_true(cv))
870	    case Some{c}:
871	      %Equal.sym(Bool, B.mine(S.fill(part), q), Maybe.default(&2, Bool, S.look(part, q), False{}), fill_at(part, q)) :
872	        {beq(_, B.mine(layout, q)) == True{} : Bool}
873	      %Equal.sym(Maybe<&2, Bool>, S.look(part, q), Some{c}, me) : {beq(Maybe.default(&2, Bool, _, False{}), B.mine(layout, q)) == True{} : Bool}
874	      %Equal.sym(Bool, B.mine(layout, q), c, beq_sound(B.mine(layout, q), c, cm)) : {beq(c, _) == True{} : Bool}
875	      beq_refl(c)
876	
877	law leaf_agree:
878	  for +part: T.Grid(Maybe<&2, Bool>)
879	  for +layout: T.Grid(Bool)
880	  for +ps: List<&2, T.Pos>
881	  for +cv: {PS.allp(~CV, ~cv_f, CV{Nil{}, part}, ps) == True{} : Bool}
882	  for +cm: {PS.allp(~CE, ~cmp_f, CE{part, layout}, ps) == True{} : Bool}
883	  {PS.allp(~AG, ~ag_f, AG{S.fill(part), layout}, ps) == True{} : Bool}
884	
885	def leaf_agree(part, layout, ps, cv, cm):
886	  match ps:
887	    case Nil{}:
888	      {==}
889	    case +q <> +t:
890	      +e0 = {CV{Nil{}, part} : CV}
891	      +e1 = {CE{part, layout} : CE}
892	      +cvq = {%P.or_false_r(Bool.not(S.is_none(S.look(part, q)))) : {_ == True{} : Bool};
893	        PS.allp_head(~CV, ~cv_f, e0, q, t, cv) : {Bool.not(S.is_none(S.look(part, q))) == True{} : Bool}}
894	      %Equal.sym(Bool, ag_f(AG{S.fill(part), layout}, q), True{},
895	        leaf_cell.go(part, layout, q, S.look(part, q), {==}, cvq, PS.allp_head(~CE, ~cmp_f, e1, q, t, cm))) :
896	        {Bool.and(_, PS.allp(~AG, ~ag_f, AG{S.fill(part), layout}, t)) == True{} : Bool}
897	      leaf_agree(part, layout, t, PS.allp_tail(~CV, ~cv_f, e0, q, t, cv), PS.allp_tail(~CE, ~cmp_f, e1, q, t, cm))
898	
899	def disc_some(-A: Data, m: Maybe<&2, A>) -> Type:
900	  match m:
901	    case None{}:
902	      Empty
903	    case Some{v}:
904	      Unit
905	
906	def some_ne_none(-A: Data, -a: A, e: {Some{a} == None{} : Maybe<&2, A>}) -> Empty:
907	  %e : disc_some(A, _)
908	  Unit{}
909	
910	def dfs_when_none(ok: Bool, k: Unit -> Maybe<&2, T.Grid(Bool)>, e: {S.dfs.when(ok, k) == None{} : Maybe<&2, T.Grid(Bool)>},
911	  okt: {ok == True{} : Bool}) -> {k(Unit{}) == None{} : Maybe<&2, T.Grid(Bool)>}:
912	  match ok:
913	    case True{}:
914	      e
915	    case False{}:
916	      Empty.absurd({k(Unit{}) == None{} : Maybe<&2, T.Grid(Bool)>}, P.false_ne_true(okt))
917	
918	def dfs_or_none_l(r: Maybe<&2, T.Grid(Bool)>, k: Unit -> Maybe<&2, T.Grid(Bool)>,
919	  e: {S.dfs.or(r, k) == None{} : Maybe<&2, T.Grid(Bool)>}) -> {r == None{} : Maybe<&2, T.Grid(Bool)>}:
920	  match r:
921	    case None{}:
922	      {==}
923	    case Some{l}:
924	      Empty.absurd({Some{l} == None{} : Maybe<&2, T.Grid(Bool)>}, some_ne_none(T.Grid(Bool), l, e))
925	
926	def dfs_or_none_r(r: Maybe<&2, T.Grid(Bool)>, k: Unit -> Maybe<&2, T.Grid(Bool)>,
927	  e: {S.dfs.or(r, k) == None{} : Maybe<&2, T.Grid(Bool)>}) -> {k(Unit{}) == None{} : Maybe<&2, T.Grid(Bool)>}:
928	  match r:
929	    case None{}:
930	      e
931	    case Some{l}:
932	      Empty.absurd({k(Unit{}) == None{} : Maybe<&2, T.Grid(Bool)>}, some_ne_none(T.Grid(Bool), l, e))
933	
934	def dfs_none.pick(+c: T.Pos, +rel: List<&2, S.Item>, +rest: List<&2, S.Todo>, +part: T.Grid(Maybe<&2, Bool>),
935	  +w: Nat, +h: Nat, +n: Nat, +rows: T.Grid(T.Seen), +its: List<&2, S.Item>, +layout: T.Grid(Bool),
936	  +shP: {B.shaped(Maybe<&2, Bool>, w, h, part) == True{} : Bool}, +shL: {B.shaped(Bool, w, h, layout) == True{} : Bool},
937	  +cov: {covers(w, h, S.Todo{c, rel} <> rest, part) == True{} : Bool},
938	  +comp: {completes(w, h, part, layout) == True{} : Bool}, +tot: {B.total_mines(layout) == n : Nat},
939	  +rok: {S.items_ok(rel, layout) == True{} : Bool}, +ron: {items_onb(PS.WH{w, h}, rel) == True{} : Bool},
940	  +bl: Bool, ble: {B.mine(layout, c) == bl : Bool},
941	  e: {S.dfs.or(S.dfs.when(S.open_ok(B.set_at(Maybe<&2, Bool>, part, c, Some{False{}}), rel, n),
942	       x => S.dfs(rest, B.set_at(Maybe<&2, Bool>, part, c, Some{False{}}), S.Ctx{w, h, n, rows, its})),
943	     y => S.dfs.when(S.open_ok(B.set_at(Maybe<&2, Bool>, part, c, Some{True{}}), rel, n),
944	       z => S.dfs(rest, B.set_at(Maybe<&2, Bool>, part, c, Some{True{}}), S.Ctx{w, h, n, rows, its}))) == None{} : Maybe<&2, T.Grid(Bool)>},
945	  k0: {S.dfs(rest, B.set_at(Maybe<&2, Bool>, part, c, Some{False{}}), S.Ctx{w, h, n, rows, its}) == None{} : Maybe<&2, T.Grid(Bool)>} ->
946	    {covers(w, h, rest, B.set_at(Maybe<&2, Bool>, part, c, Some{False{}})) == True{} : Bool} ->
947	    {completes(w, h, B.set_at(Maybe<&2, Bool>, part, c, Some{False{}}), layout) == True{} : Bool} -> Empty,
948	  k1: {S.dfs(rest, B.set_at(Maybe<&2, Bool>, part, c, Some{True{}}), S.Ctx{w, h, n, rows, its}) == None{} : Maybe<&2, T.Grid(Bool)>} ->
949	    {covers(w, h, rest, B.set_at(Maybe<&2, Bool>, part, c, Some{True{}})) == True{} : Bool} ->
950	    {completes(w, h, B.set_at(Maybe<&2, Bool>, part, c, Some{True{}}), layout) == True{} : Bool} -> Empty) -> Empty:
951	  match bl:
952	    case False{}:
953	      +p0 = B.set_at(Maybe<&2, Bool>, part, c, Some{False{}})
954	      +comp0 = comp_set(w, h, c, part, layout, False{}, shP, ble, B.cells(w, h), PS.cells_on(w, h), comp)
955	      +ok0 = open_ok_sound(w, h, n, p0, rel, layout, PL.shaped_set(Maybe<&2, Bool>, w, h, part, c, Some{False{}}, shP),
956	        shL, comp0, tot, rok, ron)
957	      +ctx = {S.Ctx{w, h, n, rows, its} : S.Ctx}
958	      k0(dfs_when_none(S.open_ok(p0, rel, n), x => S.dfs(rest, p0, ctx),
959	          dfs_or_none_l(S.dfs.when(S.open_ok(p0, rel, n), x => S.dfs(rest, p0, ctx)),
960	            y => S.dfs.when(S.open_ok(B.set_at(Maybe<&2, Bool>, part, c, Some{True{}}), rel, n),
961	              z => S.dfs(rest, B.set_at(Maybe<&2, Bool>, part, c, Some{True{}}), ctx)), e), ok0),
962	        covers_set(w, h, c, rel, rest, part, False{}, shP, B.cells(w, h), PS.cells_on(w, h), cov), comp0)
963	    case True{}:
964	      +p1 = B.set_at(Maybe<&2, Bool>, part, c, Some{True{}})
965	      +comp1 = comp_set(w, h, c, part, layout, True{}, shP, ble, B.cells(w, h), PS.cells_on(w, h), comp)
966	      +ok1 = open_ok_sound(w, h, n, p1, rel, layout, PL.shaped_set(Maybe<&2, Bool>, w, h, part, c, Some{True{}}, shP),
967	        shL, comp1, tot, rok, ron)
968	      +ctx = {S.Ctx{w, h, n, rows, its} : S.Ctx}
969	      k1(dfs_when_none(S.open_ok(p1, rel, n), z => S.dfs(rest, p1, ctx),
970	          dfs_or_none_r(S.dfs.when(S.open_ok(B.set_at(Maybe<&2, Bool>, part, c, Some{False{}}), rel, n),
971	              x => S.dfs(rest, B.set_at(Maybe<&2, Bool>, part, c, Some{False{}}), ctx)),
972	            y => S.dfs.when(S.open_ok(p1, rel, n), z => S.dfs(rest, p1, ctx)), e), ok1),
973	        covers_set(w, h, c, rel, rest, part, True{}, shP, B.cells(w, h), PS.cells_on(w, h), cov), comp1)
974	
975	def dfs_none.node(+c: T.Pos, +rel: List<&2, S.Item>, +rest: List<&2, S.Todo>, +part: T.Grid(Maybe<&2, Bool>),
976	  +w: Nat, +h: Nat, +n: Nat, +rows: T.Grid(T.Seen), +its: List<&2, S.Item>, +layout: T.Grid(Bool),
977	  +shP: {B.shaped(Maybe<&2, Bool>, w, h, part) == True{} : Bool}, +shL: {B.shaped(Bool, w, h, layout) == True{} : Bool},
978	  +cov: {covers(w, h, S.Todo{c, rel} <> rest, part) == True{} : Bool},
979	  +comp: {completes(w, h, part, layout) == True{} : Bool}, +tot: {B.total_mines(layout) == n : Nat},
980	  +rok: {S.items_ok(rel, layout) == True{} : Bool}, +ron: {items_onb(PS.WH{w, h}, rel) == True{} : Bool},
981	  +fr: Bool, fre: {S.is_none(S.look(part, c)) == fr : Bool},
982	  e: {S.dfs.free(fr, u => S.dfs(rest, part, S.Ctx{w, h, n, rows, its}),
983	      v => S.dfs.or(S.dfs.when(S.open_ok(B.set_at(Maybe<&2, Bool>, part, c, Some{False{}}), rel, n),
984	        x => S.dfs(rest, B.set_at(Maybe<&2, Bool>, part, c, Some{False{}}), S.Ctx{w, h, n, rows, its})),
985	      y => S.dfs.when(S.open_ok(B.set_at(Maybe<&2, Bool>, part, c, Some{True{}}), rel, n),
986	        z => S.dfs(rest, B.set_at(Maybe<&2, Bool>, part, c, Some{True{}}), S.Ctx{w, h, n, rows, its})))) == None{} : Maybe<&2, T.Grid(Bool)>},
987	  kp: {S.dfs(rest, part, S.Ctx{w, h, n, rows, its}) == None{} : Maybe<&2, T.Grid(Bool)>} ->
988	    {covers(w, h, rest, part) == True{} : Bool} -> Empty,
989	  k0: {S.dfs(rest, B.set_at(Maybe<&2, Bool>, part, c, Some{False{}}), S.Ctx{w, h, n, rows, its}) == None{} : Maybe<&2, T.Grid(Bool)>} ->
990	    {covers(w, h, rest, B.set_at(Maybe<&2, Bool>, part, c, Some{False{}})) == True{} : Bool} ->
991	    {completes(w, h, B.set_at(Maybe<&2, Bool>, part, c, Some{False{}}), layout) == True{} : Bool} -> Empty,
992	  k1: {S.dfs(rest, B.set_at(Maybe<&2, Bool>, part, c, Some{True{}}), S.Ctx{w, h, n, rows, its}) == None{} : Maybe<&2, T.Grid(Bool)>} ->
993	    {covers(w, h, rest, B.set_at(Maybe<&2, Bool>, part, c, Some{True{}})) == True{} : Bool} ->
994	    {completes(w, h, B.set_at(Maybe<&2, Bool>, part, c, Some{True{}}), layout) == True{} : Bool} -> Empty) -> Empty:
995	  match fr:
996	    case False{}:
997	      kp(e, covers_skip(c, rel, rest, part, fre, B.cells(w, h), cov))
998	    case True{}:
999	      dfs_none.pick(c, rel, rest, part, w, h, n, rows, its, layout, shP, shL, cov, comp, tot, rok, ron,
1000	        B.mine(layout, c), {==}, e, k0, k1)
1001	
1002	law chk_total:
1003	  for +w: Nat
1004	  for +h: Nat
1005	  for +n: Nat
1006	  for +rows: T.Grid(T.Seen)
1007	  for +its: List<&2, S.Item>
1008	  for +layout: T.Grid(Bool)
1009	  for chk: {S.check(S.Ctx{w, h, n, rows, its}, layout) == True{} : Bool}
1010	  {B.total_mines(layout) == n : Nat}
1011	
1012	def chk_total(w, h, n, rows, its, layout, chk):
1013	  +a = Bool.and(B.shaped(Bool, w, h, layout), B.shaped(T.Seen, w, h, rows))
1014	  +b = Nat.is_eq(B.total_mines(layout), n)
1015	  P.eq_sound(B.total_mines(layout), n,
1016	    P.and_true_r(a, b, P.and_true_l(Bool.and(a, b), S.items_ok(its, layout), chk)))
1017	
1018	# If the search finds nothing, no consistent layout completes the partial
1019	# layout (given that every unassigned cell is still to do).
1020	law dfs_none:
1021	  for +todo: List<&2, S.Todo>
1022	  for +part: T.Grid(Maybe<&2, Bool>)
1023	  for +w: Nat
1024	  for +h: Nat
1025	  for +n: Nat
1026	  for +rows: T.Grid(T.Seen)
1027	  for +its: List<&2, S.Item>
1028	  for +layout: T.Grid(Bool)
1029	  for e: {S.dfs(todo, part, S.Ctx{w, h, n, rows, its}) == None{} : Maybe<&2, T.Grid(Bool)>}
1030	  for +shP: {B.shaped(Maybe<&2, Bool>, w, h, part) == True{} : Bool}
1031	  for +shL: {B.shaped(Bool, w, h, layout) == True{} : Bool}
1032	  for +cov: {covers(w, h, todo, part) == True{} : Bool}
1033	  for +comp: {completes(w, h, part, layout) == True{} : Bool}
1034	  for +chk: {S.check(S.Ctx{w, h, n, rows, its}, layout) == True{} : Bool}
1035	  for +tok: {todos_ok(todo, layout) == True{} : Bool}
1036	  for +ton: {todos_onb(PS.WH{w, h}, todo) == True{} : Bool}
1037	  for +ion: {items_onb(PS.WH{w, h}, its) == True{} : Bool}
1038	  Empty
1039	
1040	def dfs_none(todo, part, w, h, n, rows, its, layout, e, shP, shL, cov, comp, chk, tok, ton, ion):
1041	  match todo:
1042	    case Nil{}:
1043	      +fp = S.fill(part)
1044	      +shF = Equal.trans(Bool, B.shaped(Bool, w, h, fp), B.shaped(Maybe<&2, Bool>, w, h, part), True{},
1045	        fill_shaped(w, h, part), shP)
1046	      +agF = leaf_agree(part, layout, B.cells(w, h), cov, comp)
1047	      +cf = Equal.trans(Bool, S.check(S.Ctx{w, h, n, rows, its}, fp), S.check(S.Ctx{w, h, n, rows, its}, layout), True{},
1048	        check_agree(w, h, n, rows, its, fp, layout, shF, shL, agF, ion), chk)
1049	      some_ne_none(T.Grid(Bool), fp,
1050	        {%cf : {Bool.pick(Maybe<&2, T.Grid(Bool)>, _, Some{fp}, None{}) == None{} : Maybe<&2, T.Grid(Bool)>};
1051	          e : {Some{fp} == None{} : Maybe<&2, T.Grid(Bool)>}})
1052	    case S.Todo{c, rel} <> rest:
1053	      +rok = P.and_true_l(S.items_ok(rel, layout), todos_ok(rest, layout), tok)
1054	      +tokr = P.and_true_r(S.items_ok(rel, layout), todos_ok(rest, layout), tok)
1055	      +ron = P.and_true_l(items_onb(PS.WH{w, h}, rel), todos_onb(PS.WH{w, h}, rest), ton)
1056	      +tonr = P.and_true_r(items_onb(PS.WH{w, h}, rel), todos_onb(PS.WH{w, h}, rest), ton)
1057	      +tot = chk_total(w, h, n, rows, its, layout, chk)
1058	      dfs_none.node(c, rel, rest, part, w, h, n, rows, its, layout, shP, shL, cov, comp, tot, rok, ron,
1059	        S.is_none(S.look(part, c)), {==}, e,
1060	        e2 => cv2 => dfs_none(rest, part, w, h, n, rows, its, layout, e2, shP, shL, cv2, comp, chk, tokr, tonr, ion),
1061	        e2 => cv2 => cm2 => dfs_none(rest, B.set_at(Maybe<&2, Bool>, part, c, Some{False{}}), w, h, n, rows, its, layout, e2,
1062	          PL.shaped_set(Maybe<&2, Bool>, w, h, part, c, Some{False{}}, shP), shL, cv2, cm2, chk, tokr, tonr, ion),
1063	        e2 => cv2 => cm2 => dfs_none(rest, B.set_at(Maybe<&2, Bool>, part, c, Some{True{}}), w, h, n, rows, its, layout, e2,
1064	          PL.shaped_set(Maybe<&2, Bool>, w, h, part, c, Some{True{}}, shP), shL, cv2, cm2, chk, tokr, tonr, ion))
1065	
1066	# What the search finds is a real candidate
1067	# =========================================
1068	
1069	def dfs_when_some(ok: Bool, k: Unit -> Maybe<&2, T.Grid(Bool)>, -l: T.Grid(Bool),
1070	  e: {S.dfs.when(ok, k) == Some{l} : Maybe<&2, T.Grid(Bool)>}) -> {k(Unit{}) == Some{l} : Maybe<&2, T.Grid(Bool)>}:
1071	  match ok:
1072	    case True{}:
1073	      e
1074	    case False{}:
1075	      Empty.absurd({k(Unit{}) == Some{l} : Maybe<&2, T.Grid(Bool)>}, PL.none_ne_some(T.Grid(Bool), l, e))
1076	
1077	def dfs_or_some(r: Maybe<&2, T.Grid(Bool)>, k: Unit -> Maybe<&2, T.Grid(Bool)>, -l: T.Grid(Bool),
1078	  e: {S.dfs.or(r, k) == Some{l} : Maybe<&2, T.Grid(Bool)>}) ->
1079	  Or({r == Some{l} : Maybe<&2, T.Grid(Bool)>}, {k(Unit{}) == Some{l} : Maybe<&2, T.Grid(Bool)>}):
1080	  match r:
1081	    case None{}:
1082	      Inr{e}
1083	    case Some{x}:
1084	      Inl{e}
1085	
1086	def BranchSome(+d0: Maybe<&2, T.Grid(Bool)>, +d1: Maybe<&2, T.Grid(Bool)>, +l: T.Grid(Bool)) -> Type:
1087	  Or({d0 == Some{l} : Maybe<&2, T.Grid(Bool)>}, {d1 == Some{l} : Maybe<&2, T.Grid(Bool)>})
1088	
1089	def dfs_branch_some.k(+ok0: Bool, +ok1: Bool, +d0: Maybe<&2, T.Grid(Bool)>, +d1: Maybe<&2, T.Grid(Bool)>, +l: T.Grid(Bool),
1090	  r: Or({S.dfs.when(ok0, x => d0) == Some{l} : Maybe<&2, T.Grid(Bool)>},
1091	    {S.dfs.when(ok1, z => d1) == Some{l} : Maybe<&2, T.Grid(Bool)>})) -> BranchSome(d0, d1, l):
1092	  match r:
1093	    case Inl{e0}:
1094	      Inl{dfs_when_some(ok0, x => d0, l, e0)}
1095	    case Inr{e1}:
1096	      Inr{dfs_when_some(ok1, z => d1, l, e1)}
1097	
1098	def dfs_branch_some(+ok0: Bool, +ok1: Bool, +d0: Maybe<&2, T.Grid(Bool)>, +d1: Maybe<&2, T.Grid(Bool)>, +l: T.Grid(Bool),
1099	  e: {S.dfs.or(S.dfs.when(ok0, x => d0), y => S.dfs.when(ok1, z => d1)) == Some{l} : Maybe<&2, T.Grid(Bool)>}) ->
1100	  BranchSome(d0, d1, l):
1101	  dfs_branch_some.k(ok0, ok1, d0, d1, l,
1102	    dfs_or_some(S.dfs.when(ok0, x => d0), y => S.dfs.when(ok1, z => d1), l, e))
1103	
1104	def leaf_some(+ctx: S.Ctx, +f: T.Grid(Bool), +l: T.Grid(Bool), +b: Bool, be: {S.check(ctx, f) == b : Bool},
1105	  e: {Bool.pick(Maybe<&2, T.Grid(Bool)>, b, Some{f}, None{}) == Some{l} : Maybe<&2, T.Grid(Bool)>}) ->
1106	  {f == l : T.Grid(Bool)} & {S.check(ctx, f) == True{} : Bool}:
1107	  match b:
1108	    case True{}:
1109	      (PL.some_inj(T.Grid(Bool), f, l, e), be)
1110	    case False{}:
1111	      Empty.absurd({f == l : T.Grid(Bool)} & {S.check(ctx, f) == True{} : Bool}, PL.none_ne_some(T.Grid(Bool), l, e))
1112	
1113	def leaf_check.k(+ctx: S.Ctx, +f: T.Grid(Bool), +l: T.Grid(Bool),
1114	  r: {f == l : T.Grid(Bool)} & {S.check(ctx, f) == True{} : Bool}) -> {S.check(ctx, l) == True{} : Bool}:
1115	  match r:
1116	    case (fl, ck):
1117	      %fl : {S.check(ctx, _) == True{} : Bool}
1118	      ck
1119	
1120	# A layout the search returns passes the consistency check.
1121	law dfs_some_check:
1122	  for +todo: List<&2, S.Todo>
1123	  for +part: T.Grid(Maybe<&2, Bool>)
1124	  for +ctx: S.Ctx
1125	  for +l: T.Grid(Bool)
1126	  for e: {S.dfs(todo, part, ctx) == Some{l} : Maybe<&2, T.Grid(Bool)>}
1127	  {S.check(ctx, l) == True{} : Bool}
1128	
1129	def dfs_some_check.br(+l: T.Grid(Bool), +ctx: S.Ctx, +d0: Maybe<&2, T.Grid(Bool)>, +d1: Maybe<&2, T.Grid(Bool)>,
1130	  r: BranchSome(d0, d1, l), k0: {d0 == Some{l} : Maybe<&2, T.Grid(Bool)>} -> {S.check(ctx, l) == True{} : Bool},
1131	  k1: {d1 == Some{l} : Maybe<&2, T.Grid(Bool)>} -> {S.check(ctx, l) == True{} : Bool}) -> {S.check(ctx, l) == True{} : Bool}:
1132	  match r:
1133	    case Inl{e0}:
1134	      k0(e0)
1135	    case Inr{e1}:
1136	      k1(e1)
1137	
1138	def dfs_some_check.node(+c: T.Pos, +rel: List<&2, S.Item>, +rest: List<&2, S.Todo>, +part: T.Grid(Maybe<&2, Bool>),
1139	  +ctx: S.Ctx, +l: T.Grid(Bool), +fr: Bool,
1140	  e: {S.dfs.free(fr, u => S.dfs(rest, part, ctx),
1141	      v => S.dfs.or(S.dfs.when(S.open_ok(B.set_at(Maybe<&2, Bool>, part, c, Some{False{}}), rel, S.ctx_n(ctx)),
1142	        x => S.dfs(rest, B.set_at(Maybe<&2, Bool>, part, c, Some{False{}}), ctx)),
1143	      y => S.dfs.when(S.open_ok(B.set_at(Maybe<&2, Bool>, part, c, Some{True{}}), rel, S.ctx_n(ctx)),
1144	        z => S.dfs(rest, B.set_at(Maybe<&2, Bool>, part, c, Some{True{}}), ctx)))) == Some{l} : Maybe<&2, T.Grid(Bool)>},
1145	  kp: {S.dfs(rest, part, ctx) == Some{l} : Maybe<&2, T.Grid(Bool)>} -> {S.check(ctx, l) == True{} : Bool},
1146	  k0: {S.dfs(rest, B.set_at(Maybe<&2, Bool>, part, c, Some{False{}}), ctx) == Some{l} : Maybe<&2, T.Grid(Bool)>} ->
1147	    {S.check(ctx, l) == True{} : Bool},
1148	  k1: {S.dfs(rest, B.set_at(Maybe<&2, Bool>, part, c, Some{True{}}), ctx) == Some{l} : Maybe<&2, T.Grid(Bool)>} ->
1149	    {S.check(ctx, l) == True{} : Bool}) -> {S.check(ctx, l) == True{} : Bool}:
1150	  match fr:
1151	    case False{}:
1152	      kp(e)
1153	    case True{}:
1154	      dfs_some_check.br(l, ctx, S.dfs(rest, B.set_at(Maybe<&2, Bool>, part, c, Some{False{}}), ctx),
1155	        S.dfs(rest, B.set_at(Maybe<&2, Bool>, part, c, Some{True{}}), ctx),
1156	        dfs_branch_some(S.open_ok(B.set_at(Maybe<&2, Bool>, part, c, Some{False{}}), rel, S.ctx_n(ctx)),
1157	          S.open_ok(B.set_at(Maybe<&2, Bool>, part, c, Some{True{}}), rel, S.ctx_n(ctx)),
1158	          S.dfs(rest, B.set_at(Maybe<&2, Bool>, part, c, Some{False{}}), ctx),
1159	          S.dfs(rest, B.set_at(Maybe<&2, Bool>, part, c, Some{True{}}), ctx), l, e), k0, k1)
1160	
1161	def dfs_some_check(todo, part, ctx, l, e):
1162	  match todo:
1163	    case Nil{}:
1164	      leaf_check.k(ctx, S.fill(part), l, leaf_some(ctx, S.fill(part), l, S.check(ctx, S.fill(part)), {==}, e))
1165	    case S.Todo{c, rel} <> rest:
1166	      dfs_some_check.node(c, rel, rest, part, ctx, l, S.is_none(S.look(part, c)), e,
1167	        e2 => dfs_some_check(rest, part, ctx, l, e2),
1168	        e2 => dfs_some_check(rest, B.set_at(Maybe<&2, Bool>, part, c, Some{False{}}), ctx, l, e2),
1169	        e2 => dfs_some_check(rest, B.set_at(Maybe<&2, Bool>, part, c, Some{True{}}), ctx, l, e2))
1170	
1171	def set_keep(+part: T.Grid(Maybe<&2, Bool>), +c: T.Pos, +q: T.Pos, +v: Maybe<&2, Bool>, +bq: Bool,
1172	  fre: {S.is_none(S.look(part, c)) == True{} : Bool}, lq: {S.look(part, q) == Some{bq} : Maybe<&2, Bool>},
1173	  +b: Bool, be: {B.same(c, q) == b : Bool}) ->
1174	  {S.look(B.set_at(Maybe<&2, Bool>, part, c, v), q) == Some{bq} : Maybe<&2, Bool>}:
1175	  match b:
1176	    case True{}:
1177	      +lc = {%Equal.sym(T.Pos, c, q, PG.same_sound(c, q, be)) : {S.look(part, _) == Some{bq} : Maybe<&2, Bool>};
1178	        lq : {S.look(part, c) == Some{bq} : Maybe<&2, Bool>}}
1179	      Empty.absurd({S.look(B.set_at(Maybe<&2, Bool>, part, c, v), q) == Some{bq} : Maybe<&2, Bool>},
1180	        P.false_ne_true(%lc : {S.is_none(_) == True{} : Bool}; fre))
1181	    case False{}:
1182	      %Equal.sym(Maybe<&2, Bool>, S.look(B.set_at(Maybe<&2, Bool>, part, c, v), q), S.look(part, q),
1183	        PL.at_set_ne(Maybe<&2, Bool>, part, c, q, v, None{}, be)) : {_ == Some{bq} : Maybe<&2, Bool>}
1184	      lq
1185	
1186	def leaf_keep(+ctx: S.Ctx, +part: T.Grid(Maybe<&2, Bool>), +l: T.Grid(Bool), +q: T.Pos, +bq: Bool,
1187	  lq: {S.look(part, q) == Some{bq} : Maybe<&2, Bool>},
1188	  r: {S.fill(part) == l : T.Grid(Bool)} & {S.check(ctx, S.fill(part)) == True{} : Bool}) ->
1189	  {B.mine(l, q) == bq : Bool}:
1190	  match r:
1191	    case (fl, ck):
1192	      %fl : {B.mine(_, q) == bq : Bool}
1193	      %Equal.sym(Bool, B.mine(S.fill(part), q), Maybe.default(&2, Bool, S.look(part, q), False{}), fill_at(part, q)) :
1194	        {_ == bq : Bool}
1195	      %Equal.sym(Maybe<&2, Bool>, S.look(part, q), Some{bq}, lq) : {Maybe.default(&2, Bool, _, False{}) == bq : Bool}
1196	      {==}
1197	
1198	def dfs_some_keep.br(+l: T.Grid(Bool), +q: T.Pos, +bq: Bool, +d0: Maybe<&2, T.Grid(Bool)>, +d1: Maybe<&2, T.Grid(Bool)>,
1199	  r: BranchSome(d0, d1, l), k0: {d0 == Some{l} : Maybe<&2, T.Grid(Bool)>} -> {B.mine(l, q) == bq : Bool},
1200	  k1: {d1 == Some{l} : Maybe<&2, T.Grid(Bool)>} -> {B.mine(l, q) == bq : Bool}) -> {B.mine(l, q) == bq : Bool}:
1201	  match r:
1202	    case Inl{e0}:
1203	      k0(e0)
1204	    case Inr{e1}:
1205	      k1(e1)
1206	
1207	def dfs_some_keep.node(+c: T.Pos, +rel: List<&2, S.Item>, +rest: List<&2, S.Todo>, +part: T.Grid(Maybe<&2, Bool>),
1208	  +ctx: S.Ctx, +l: T.Grid(Bool), +q: T.Pos, +bq: Bool, +fr: Bool, +fre: {S.is_none(S.look(part, c)) == fr : Bool},
1209	  e: {S.dfs.free(fr, u => S.dfs(rest, part, ctx),
1210	      v => S.dfs.or(S.dfs.when(S.open_ok(B.set_at(Maybe<&2, Bool>, part, c, Some{False{}}), rel, S.ctx_n(ctx)),
1211	        x => S.dfs(rest, B.set_at(Maybe<&2, Bool>, part, c, Some{False{}}), ctx)),
1212	      y => S.dfs.when(S.open_ok(B.set_at(Maybe<&2, Bool>, part, c, Some{True{}}), rel, S.ctx_n(ctx)),
1213	        z => S.dfs(rest, B.set_at(Maybe<&2, Bool>, part, c, Some{True{}}), ctx)))) == Some{l} : Maybe<&2, T.Grid(Bool)>},
1214	  +lq: {S.look(part, q) == Some{bq} : Maybe<&2, Bool>},
1215	  kp: {S.dfs(rest, part, ctx) == Some{l} : Maybe<&2, T.Grid(Bool)>} -> {B.mine(l, q) == bq : Bool},
1216	  k0: {S.dfs(rest, B.set_at(Maybe<&2, Bool>, part, c, Some{False{}}), ctx) == Some{l} : Maybe<&2, T.Grid(Bool)>} ->
1217	    {S.look(B.set_at(Maybe<&2, Bool>, part, c, Some{False{}}), q) == Some{bq} : Maybe<&2, Bool>} -> {B.mine(l, q) == bq : Bool},
1218	  k1: {S.dfs(rest, B.set_at(Maybe<&2, Bool>, part, c, Some{True{}}), ctx) == Some{l} : Maybe<&2, T.Grid(Bool)>} ->
1219	    {S.look(B.set_at(Maybe<&2, Bool>, part, c, Some{True{}}), q) == Some{bq} : Maybe<&2, Bool>} -> {B.mine(l, q) == bq : Bool}) ->
1220	  {B.mine(l, q) == bq : Bool}:
1221	  match fr:
1222	    case False{}:
1223	      kp(e)
1224	    case True{}:
1225	      +d0 = S.dfs(rest, B.set_at(Maybe<&2, Bool>, part, c, Some{False{}}), ctx)
1226	      +d1 = S.dfs(rest, B.set_at(Maybe<&2, Bool>, part, c, Some{True{}}), ctx)
1227	      dfs_some_keep.br(l, q, bq, d0, d1,
1228	        dfs_branch_some(S.open_ok(B.set_at(Maybe<&2, Bool>, part, c, Some{False{}}), rel, S.ctx_n(ctx)),
1229	          S.open_ok(B.set_at(Maybe<&2, Bool>, part, c, Some{True{}}), rel, S.ctx_n(ctx)), d0, d1, l, e),
1230	        e0 => k0(e0, set_keep(part, c, q, Some{False{}}, bq, fre, lq, B.same(c, q), {==})),
1231	        e1 => k1(e1, set_keep(part, c, q, Some{True{}}, bq, fre, lq, B.same(c, q), {==})))
1232	
1233	# A layout the search returns keeps every cell the partial layout fixed.
1234	law dfs_some_keep:
1235	  for +todo: List<&2, S.Todo>
1236	  for +part: T.Grid(Maybe<&2, Bool>)
1237	  for +ctx: S.Ctx
1238	  for +l: T.Grid(Bool)
1239	  for e: {S.dfs(todo, part, ctx) == Some{l} : Maybe<&2, T.Grid(Bool)>}
1240	  for +q: T.Pos
1241	  for +bq: Bool
1242	  for +lq: {S.look(part, q) == Some{bq} : Maybe<&2, Bool>}
1243	  {B.mine(l, q) == bq : Bool}
1244	
1245	def dfs_some_keep(todo, part, ctx, l, e, q, bq, lq):
1246	  match todo:
1247	    case Nil{}:
1248	      leaf_keep(ctx, part, l, q, bq, lq, leaf_some(ctx, S.fill(part), l, S.check(ctx, S.fill(part)), {==}, e))
1249	    case S.Todo{c, rel} <> rest:
1250	      dfs_some_keep.node(c, rel, rest, part, ctx, l, q, bq, S.is_none(S.look(part, c)), {==}, e, lq,
1251	        e2 => dfs_some_keep(rest, part, ctx, l, e2, q, bq, lq),
1252	        e2 => l2 => dfs_some_keep(rest, B.set_at(Maybe<&2, Bool>, part, c, Some{False{}}), ctx, l, e2, q, bq, l2),
1253	        e2 => l2 => dfs_some_keep(rest, B.set_at(Maybe<&2, Bool>, part, c, Some{True{}}), ctx, l, e2, q, bq, l2))
1254	
1255	# The same for the counting search
1256	# =================================
1257	
1258	# A layout the counting search returns passes the consistency check.
1259	law dfs2_some_check:
1260	  for +todo: List<&2, S.Todo>
1261	  for +part: T.Grid(Maybe<&2, Bool>)
1262	  for +t: Nat
1263	  for +f: Nat
1264	  for +ctx: S.Ctx
1265	  for +l: T.Grid(Bool)
1266	  for e: {S.dfs2(todo, part, t, f, ctx) == Some{l} : Maybe<&2, T.Grid(Bool)>}
1267	  {S.check(ctx, l) == True{} : Bool}
1268	
1269	def dfs2_some_check.node(+c: T.Pos, +rel: List<&2, S.Item>, +rest: List<&2, S.Todo>, +part: T.Grid(Maybe<&2, Bool>),
1270	  +t: Nat, +f: Nat, +ctx: S.Ctx, +l: T.Grid(Bool), +fr: Bool,
1271	  e: {S.dfs.free(fr, u => S.dfs2(rest, part, t, f, ctx),
1272	      v => S.dfs.or(S.dfs.when(Bool.and(S.between(t, Nat.sub(f, 1n), S.ctx_n(ctx)), S.items_open(B.set_at(Maybe<&2, Bool>, part, c, Some{False{}}), rel)),
1273	        x => S.dfs2(rest, B.set_at(Maybe<&2, Bool>, part, c, Some{False{}}), t, Nat.sub(f, 1n), ctx)),
1274	      y => S.dfs.when(Bool.and(S.between(1n+t, Nat.sub(f, 1n), S.ctx_n(ctx)), S.items_open(B.set_at(Maybe<&2, Bool>, part, c, Some{True{}}), rel)),
1275	        z => S.dfs2(rest, B.set_at(Maybe<&2, Bool>, part, c, Some{True{}}), 1n+t, Nat.sub(f, 1n), ctx)))) == Some{l} : Maybe<&2, T.Grid(Bool)>},
1276	  kp: {S.dfs2(rest, part, t, f, ctx) == Some{l} : Maybe<&2, T.Grid(Bool)>} -> {S.check(ctx, l) == True{} : Bool},
1277	  k0: {S.dfs2(rest, B.set_at(Maybe<&2, Bool>, part, c, Some{False{}}), t, Nat.sub(f, 1n), ctx) == Some{l} : Maybe<&2, T.Grid(Bool)>} ->
1278	    {S.check(ctx, l) == True{} : Bool},
1279	  k1: {S.dfs2(rest, B.set_at(Maybe<&2, Bool>, part, c, Some{True{}}), 1n+t, Nat.sub(f, 1n), ctx) == Some{l} : Maybe<&2, T.Grid(Bool)>} ->
1280	    {S.check(ctx, l) == True{} : Bool}) -> {S.check(ctx, l) == True{} : Bool}:
1281	  match fr:
1282	    case False{}:
1283	      kp(e)
1284	    case True{}:
1285	      dfs_some_check.br(l, ctx, S.dfs2(rest, B.set_at(Maybe<&2, Bool>, part, c, Some{False{}}), t, Nat.sub(f, 1n), ctx),
1286	        S.dfs2(rest, B.set_at(Maybe<&2, Bool>, part, c, Some{True{}}), 1n+t, Nat.sub(f, 1n), ctx),
1287	        dfs_branch_some(Bool.and(S.between(t, Nat.sub(f, 1n), S.ctx_n(ctx)), S.items_open(B.set_at(Maybe<&2, Bool>, part, c, Some{False{}}), rel)),
1288	          Bool.and(S.between(1n+t, Nat.sub(f, 1n), S.ctx_n(ctx)), S.items_open(B.set_at(Maybe<&2, Bool>, part, c, Some{True{}}), rel)),
1289	          S.dfs2(rest, B.set_at(Maybe<&2, Bool>, part, c, Some{False{}}), t, Nat.sub(f, 1n), ctx),
1290	          S.dfs2(rest, B.set_at(Maybe<&2, Bool>, part, c, Some{True{}}), 1n+t, Nat.sub(f, 1n), ctx), l, e), k0, k1)
1291	
1292	def dfs2_some_check(todo, part, t, f, ctx, l, e):
1293	  match todo:
1294	    case Nil{}:
1295	      leaf_check.k(ctx, S.fill(part), l, leaf_some(ctx, S.fill(part), l, S.check(ctx, S.fill(part)), {==}, e))
1296	    case S.Todo{c, rel} <> rest:
1297	      dfs2_some_check.node(c, rel, rest, part, t, f, ctx, l, S.is_none(S.look(part, c)), e,
1298	        e2 => dfs2_some_check(rest, part, t, f, ctx, l, e2),
1299	        e2 => dfs2_some_check(rest, B.set_at(Maybe<&2, Bool>, part, c, Some{False{}}), t, Nat.sub(f, 1n), ctx, l, e2),
1300	        e2 => dfs2_some_check(rest, B.set_at(Maybe<&2, Bool>, part, c, Some{True{}}), 1n+t, Nat.sub(f, 1n), ctx, l, e2))
1301	
1302	# A layout the counting search returns keeps every cell the partial layout fixed.
1303	law dfs2_some_keep:
1304	  for +todo: List<&2, S.Todo>
1305	  for +part: T.Grid(Maybe<&2, Bool>)
1306	  for +t: Nat
1307	  for +f: Nat
1308	  for +ctx: S.Ctx
1309	  for +l: T.Grid(Bool)
1310	  for e: {S.dfs2(todo, part, t, f, ctx) == Some{l} : Maybe<&2, T.Grid(Bool)>}
1311	  for +q: T.Pos
1312	  for +bq: Bool
1313	  for +lq: {S.look(part, q) == Some{bq} : Maybe<&2, Bool>}
1314	  {B.mine(l, q) == bq : Bool}
1315	
1316	def dfs2_some_keep.node(+c: T.Pos, +rel: List<&2, S.Item>, +rest: List<&2, S.Todo>, +part: T.Grid(Maybe<&2, Bool>),
1317	  +t: Nat, +f: Nat, +ctx: S.Ctx, +l: T.Grid(Bool), +q: T.Pos, +bq: Bool, +fr: Bool, +fre: {S.is_none(S.look(part, c)) == fr : Bool},
1318	  e: {S.dfs.free(fr, u => S.dfs2(rest, part, t, f, ctx),
1319	      v => S.dfs.or(S.dfs.when(Bool.and(S.between(t, Nat.sub(f, 1n), S.ctx_n(ctx)), S.items_open(B.set_at(Maybe<&2, Bool>, part, c, Some{False{}}), rel)),
1320	        x => S.dfs2(rest, B.set_at(Maybe<&2, Bool>, part, c, Some{False{}}), t, Nat.sub(f, 1n), ctx)),
1321	      y => S.dfs.when(Bool.and(S.between(1n+t, Nat.sub(f, 1n), S.ctx_n(ctx)), S.items_open(B.set_at(Maybe<&2, Bool>, part, c, Some{True{}}), rel)),
1322	        z => S.dfs2(rest, B.set_at(Maybe<&2, Bool>, part, c, Some{True{}}), 1n+t, Nat.sub(f, 1n), ctx)))) == Some{l} : Maybe<&2, T.Grid(Bool)>},
1323	  +lq: {S.look(part, q) == Some{bq} : Maybe<&2, Bool>},
1324	  kp: {S.dfs2(rest, part, t, f, ctx) == Some{l} : Maybe<&2, T.Grid(Bool)>} -> {B.mine(l, q) == bq : Bool},
1325	  k0: {S.dfs2(rest, B.set_at(Maybe<&2, Bool>, part, c, Some{False{}}), t, Nat.sub(f, 1n), ctx) == Some{l} : Maybe<&2, T.Grid(Bool)>} ->
1326	    {S.look(B.set_at(Maybe<&2, Bool>, part, c, Some{False{}}), q) == Some{bq} : Maybe<&2, Bool>} -> {B.mine(l, q) == bq : Bool},
1327	  k1: {S.dfs2(rest, B.set_at(Maybe<&2, Bool>, part, c, Some{True{}}), 1n+t, Nat.sub(f, 1n), ctx) == Some{l} : Maybe<&2, T.Grid(Bool)>} ->
1328	    {S.look(B.set_at(Maybe<&2, Bool>, part, c, Some{True{}}), q) == Some{bq} : Maybe<&2, Bool>} -> {B.mine(l, q) == bq : Bool}) ->
1329	  {B.mine(l, q) == bq : Bool}:
1330	  match fr:
1331	    case False{}:
1332	      kp(e)
1333	    case True{}:
1334	      +d0 = S.dfs2(rest, B.set_at(Maybe<&2, Bool>, part, c, Some{False{}}), t, Nat.sub(f, 1n), ctx)
1335	      +d1 = S.dfs2(rest, B.set_at(Maybe<&2, Bool>, part, c, Some{True{}}), 1n+t, Nat.sub(f, 1n), ctx)
1336	      dfs_some_keep.br(l, q, bq, d0, d1,
1337	        dfs_branch_some(Bool.and(S.between(t, Nat.sub(f, 1n), S.ctx_n(ctx)), S.items_open(B.set_at(Maybe<&2, Bool>, part, c, Some{False{}}), rel)),
1338	          Bool.and(S.between(1n+t, Nat.sub(f, 1n), S.ctx_n(ctx)), S.items_open(B.set_at(Maybe<&2, Bool>, part, c, Some{True{}}), rel)), d0, d1, l, e),
1339	        e0 => k0(e0, set_keep(part, c, q, Some{False{}}, bq, fre, lq, B.same(c, q), {==})),
1340	        e1 => k1(e1, set_keep(part, c, q, Some{True{}}, bq, fre, lq, B.same(c, q), {==})))
1341	
1342	def dfs2_some_keep(todo, part, t, f, ctx, l, e, q, bq, lq):
1343	  match todo:
1344	    case Nil{}:
1345	      leaf_keep(ctx, part, l, q, bq, lq, leaf_some(ctx, S.fill(part), l, S.check(ctx, S.fill(part)), {==}, e))
1346	    case S.Todo{c, rel} <> rest:
1347	      dfs2_some_keep.node(c, rel, rest, part, t, f, ctx, l, q, bq, S.is_none(S.look(part, c)), {==}, e, lq,
1348	        e2 => dfs2_some_keep(rest, part, t, f, ctx, l, e2, q, bq, lq),
1349	        e2 => l2 => dfs2_some_keep(rest, B.set_at(Maybe<&2, Bool>, part, c, Some{False{}}), t, Nat.sub(f, 1n), ctx, l, e2, q, bq, l2),
1350	        e2 => l2 => dfs2_some_keep(rest, B.set_at(Maybe<&2, Bool>, part, c, Some{True{}}), 1n+t, Nat.sub(f, 1n), ctx, l, e2, q, bq, l2))
1351	
1352	# The check is consistency
1353	# ========================
1354	
1355	def items_agrees.cell(+w: Nat, +h: Nat, +rows: T.Grid(T.Seen), +layout: T.Grid(Bool), +p: T.Pos,
1356	  +t: List<&2, T.Pos>, +s: T.Seen,
1357	  ih: {S.items_ok(S.items(w, h, rows, t), layout) == L.agrees_all(w, h, rows, layout, t) : Bool}) ->
1358	  {S.items_ok(S.items.put(s, p, w, h, S.items(w, h, rows, t)), layout)
1359	    == Bool.and(L.agrees(w, h, layout, p, s), L.agrees_all(w, h, rows, layout, t)) : Bool}:
1360	  match s:
1361	    case T.Hidden{}:
1362	      ih
1363	    case T.Shown{k}:
1364	      %PC.mine_eq(layout, p) :
1365	        {Bool.and(Bool.and(Bool.not(B.mine(layout, p)), Nat.is_eq(B.count_mines(layout, B.neighbours(w, h, p)), k)),
1366	          S.items_ok(S.items(w, h, rows, t), layout))
1367	          == Bool.and(Bool.and(Bool.not(_), Nat.is_eq(L.adj_mines(w, h, layout, p), k)), L.agrees_all(w, h, rows, layout, t)) : Bool}
1368	      %PC.adj_mines_eq(w, h, layout, p) :
1369	        {Bool.and(Bool.and(Bool.not(B.mine(layout, p)), Nat.is_eq(B.adj_mines(w, h, layout, p), k)),
1370	          S.items_ok(S.items(w, h, rows, t), layout))
1371	          == Bool.and(Bool.and(Bool.not(B.mine(layout, p)), Nat.is_eq(_, k)), L.agrees_all(w, h, rows, layout, t)) : Bool}
1372	      %Equal.sym(Bool, S.items_ok(S.items(w, h, rows, t), layout), L.agrees_all(w, h, rows, layout, t), ih) :
1373	        {Bool.and(Bool.and(Bool.not(B.mine(layout, p)), Nat.is_eq(B.adj_mines(w, h, layout, p), k)), _)
1374	          == Bool.and(Bool.and(Bool.not(B.mine(layout, p)), Nat.is_eq(B.adj_mines(w, h, layout, p), k)), L.agrees_all(w, h, rows, layout, t)) : Bool}
1375	      {==}
1376	    case T.Boom{}:
1377	      %PC.mine_eq(layout, p) :
1378	        {Bool.and(B.mine(layout, p), S.items_ok(S.items(w, h, rows, t), layout))
1379	          == Bool.and(_, L.agrees_all(w, h, rows, layout, t)) : Bool}
1380	      %Equal.sym(Bool, S.items_ok(S.items(w, h, rows, t), layout), L.agrees_all(w, h, rows, layout, t), ih) :
1381	        {Bool.and(B.mine(layout, p), _) == Bool.and(B.mine(layout, p), L.agrees_all(w, h, rows, layout, t)) : Bool}
1382	      {==}
1383	
1384	law items_agrees:
1385	  for +w: Nat
1386	  for +h: Nat
1387	  for +rows: T.Grid(T.Seen)
1388	  for +layout: T.Grid(Bool)
1389	  for +ps: List<&2, T.Pos>
1390	  {S.items_ok(S.items(w, h, rows, ps), layout) == L.agrees_all(w, h, rows, layout, ps) : Bool}
1391	
1392	def items_agrees(w, h, rows, layout, ps):
1393	  match ps:
1394	    case Nil{}:
1395	      {==}
1396	    case p <> t:
1397	      %PC.at_eq(T.Seen, T.Hidden{}, rows, p) :
1398	        {S.items_ok(S.items.put(B.at(T.Seen, T.Hidden{}, rows, p), p, w, h, S.items(w, h, rows, t)), layout)
1399	          == Bool.and(L.agrees(w, h, layout, p, _), L.agrees_all(w, h, rows, layout, t)) : Bool}
1400	      items_agrees.cell(w, h, rows, layout, p, t, B.at(T.Seen, T.Hidden{}, rows, p), items_agrees(w, h, rows, layout, t))
1401	
1402	# The solver's check is LAWS.bend's consistent.
1403	law check_cons:
1404	  for +w: Nat
1405	  for +h: Nat
1406	  for +n: Nat
1407	  for +rows: T.Grid(T.Seen)
1408	  for +layout: T.Grid(Bool)
1409	  {S.check(S.Ctx{w, h, n, rows, S.items(w, h, rows, B.cells(w, h))}, layout)
1410	    == L.consistent(T.Knowledge{w, h, n, rows}, layout) : Bool}
1411	
1412	def check_cons(w, h, n, rows, layout):
1413	  +its = S.items(w, h, rows, B.cells(w, h))
1414	  %PC.shaped_eq(Bool, w, h, layout) :
1415	    {Bool.and(Bool.and(Bool.and(B.shaped(Bool, w, h, layout), B.shaped(T.Seen, w, h, rows)), Nat.is_eq(B.total_mines(layout), n)),
1416	      S.items_ok(its, layout))
1417	      == Bool.and(Bool.and(Bool.and(_, L.shaped(T.Seen, w, h, rows)), Nat.is_eq(L.total_mines(layout), n)),
1418	        L.agrees_all(w, h, rows, layout, L.cells(w, h))) : Bool}
1419	  %PC.shaped_eq(T.Seen, w, h, rows) :
1420	    {Bool.and(Bool.and(Bool.and(B.shaped(Bool, w, h, layout), B.shaped(T.Seen, w, h, rows)), Nat.is_eq(B.total_mines(layout), n)),
1421	      S.items_ok(its, layout))
1422	      == Bool.and(Bool.and(Bool.and(B.shaped(Bool, w, h, layout), _), Nat.is_eq(L.total_mines(layout), n)),
1423	        L.agrees_all(w, h, rows, layout, L.cells(w, h))) : Bool}
1424	  %PC.total_mines_eq(layout) :
1425	    {Bool.and(Bool.and(Bool.and(B.shaped(Bool, w, h, layout), B.shaped(T.Seen, w, h, rows)), Nat.is_eq(B.total_mines(layout), n)),
1426	      S.items_ok(its, layout))
1427	      == Bool.and(Bool.and(Bool.and(B.shaped(Bool, w, h, layout), B.shaped(T.Seen, w, h, rows)), Nat.is_eq(_, n)),
1428	        L.agrees_all(w, h, rows, layout, L.cells(w, h))) : Bool}
1429	  %PC.cells_eq(w, h) :
1430	    {Bool.and(Bool.and(Bool.and(B.shaped(Bool, w, h, layout), B.shaped(T.Seen, w, h, rows)), Nat.is_eq(B.total_mines(layout), n)),
1431	      S.items_ok(its, layout))
1432	      == Bool.and(Bool.and(Bool.and(B.shaped(Bool, w, h, layout), B.shaped(T.Seen, w, h, rows)), Nat.is_eq(B.total_mines(layout), n)),
1433	        L.agrees_all(w, h, rows, layout, _)) : Bool}
1434	  %items_agrees(w, h, rows, layout, B.cells(w, h)) :
1435	    {Bool.and(Bool.and(Bool.and(B.shaped(Bool, w, h, layout), B.shaped(T.Seen, w, h, rows)), Nat.is_eq(B.total_mines(layout), n)),
1436	      S.items_ok(its, layout))
1437	      == Bool.and(Bool.and(Bool.and(B.shaped(Bool, w, h, layout), B.shaped(T.Seen, w, h, rows)), Nat.is_eq(B.total_mines(layout), n)),
1438	        _) : Bool}
1439	  {==}
1440	
1441	# The starting partial layout
1442	# ===========================
1443	
1444	law start_rows_get:
1445	  for +g: T.Grid(T.Seen)
1446	  for +y: Nat
1447	  {Maybe.default(&2, List<&2, Maybe<&2, Bool>>, List.get(&2, List<&2, Maybe<&2, Bool>>, S.start(g), y), Nil{})
1448	    == S.start.row(Maybe.default(&2, List<&2, T.Seen>, List.get(&2, List<&2, T.Seen>, g, y), Nil{})) : List<&2, Maybe<&2, Bool>>}
1449	
1450	def start_rows_get(g, y):
1451	  match g y:
1452	    case Nil{} _:
1453	      {==}
1454	    case r <> t 0n:
1455	      {==}
1456	    case r <> t 1n+k:
1457	      start_rows_get(t, k)
1458	
1459	law start_row_get:
1460	  for +r: List<&2, T.Seen>
1461	  for +x: Nat
1462	  {Maybe.default(&2, Maybe<&2, Bool>, List.get(&2, Maybe<&2, Bool>, S.start.row(r), x), None{})
1463	    == S.start.cell(Maybe.default(&2, T.Seen, List.get(&2, T.Seen, r, x), T.Hidden{})) : Maybe<&2, Bool>}
1464	
1465	def start_row_get(r, x):
1466	  match r x:
1467	    case Nil{} _:
1468	      {==}
1469	    case s <> t 0n:
1470	      {==}
1471	    case s <> t 1n+k:
1472	      start_row_get(t, k)
1473	
1474	# Each cell starts as the revealed cells fix it.
1475	law start_at:
1476	  for +rows: T.Grid(T.Seen)
1477	  for +q: T.Pos
1478	  {S.look(S.start(rows), q) == S.start.cell(B.at(T.Seen, T.Hidden{}, rows, q)) : Maybe<&2, Bool>}
1479	
1480	def start_at(rows, q):
1481	  match q:
1482	    case T.Pos{x, y}:
1483	      %Equal.sym(List<&2, Maybe<&2, Bool>>,
1484	        Maybe.default(&2, List<&2, Maybe<&2, Bool>>, List.get(&2, List<&2, Maybe<&2, Bool>>, S.start(rows), y), Nil{}),
1485	        S.start.row(Maybe.default(&2, List<&2, T.Seen>, List.get(&2, List<&2, T.Seen>, rows, y), Nil{})),
1486	        start_rows_get(rows, y)) :
1487	        {Maybe.default(&2, Maybe<&2, Bool>, List.get(&2, Maybe<&2, Bool>, _, x), None{})
1488	          == S.start.cell(B.at(T.Seen, T.Hidden{}, rows, T.Pos{x, y})) : Maybe<&2, Bool>}
1489	      start_row_get(Maybe.default(&2, List<&2, T.Seen>, List.get(&2, List<&2, T.Seen>, rows, y), Nil{}), x)
1490	
1491	law start_row_len:
1492	  for +r: List<&2, T.Seen>
1493	  {List.length(&2, Maybe<&2, Bool>, S.start.row(r)) == List.length(&2, T.Seen, r) : Nat}
1494	
1495	def start_row_len(r):
1496	  match r:
1497	    case Nil{}:
1498	      {==}
1499	    case s <> t:
1500	      %Equal.sym(Nat, List.length(&2, Maybe<&2, Bool>, S.start.row(t)), List.length(&2, T.Seen, t), start_row_len(t)) :
1501	        {1n+_ == 1n+List.length(&2, T.Seen, t) : Nat}
1502	      {==}
1503	
1504	law start_len:
1505	  for +g: T.Grid(T.Seen)
1506	  {List.length(&2, List<&2, Maybe<&2, Bool>>, S.start(g)) == List.length(&2, List<&2, T.Seen>, g) : Nat}
1507	
1508	def start_len(g):
1509	  match g:
1510	    case Nil{}:
1511	      {==}
1512	    case r <> t:
1513	      %Equal.sym(Nat, List.length(&2, List<&2, Maybe<&2, Bool>>, S.start(t)), List.length(&2, List<&2, T.Seen>, t), start_len(t)) :
1514	        {1n+_ == 1n+List.length(&2, List<&2, T.Seen>, t) : Nat}
1515	      {==}
1516	
1517	law start_wide:
1518	  for +w: Nat
1519	  for +g: T.Grid(T.Seen)
1520	  {B.rows_wide(Maybe<&2, Bool>, w, S.start(g)) == B.rows_wide(T.Seen, w, g) : Bool}
1521	
1522	def start_wide(w, g):
1523	  match g:
1524	    case Nil{}:
1525	      {==}
1526	    case r <> t:
1527	      %Equal.sym(Nat, List.length(&2, Maybe<&2, Bool>, S.start.row(r)), List.length(&2, T.Seen, r), start_row_len(r)) :
1528	        {Bool.and(Nat.is_eq(_, w), B.rows_wide(Maybe<&2, Bool>, w, S.start(t)))
1529	          == Bool.and(Nat.is_eq(List.length(&2, T.Seen, r), w), B.rows_wide(T.Seen, w, t)) : Bool}
1530	      %Equal.sym(Bool, B.rows_wide(Maybe<&2, Bool>, w, S.start(t)), B.rows_wide(T.Seen, w, t), start_wide(w, t)) :
1531	        {Bool.and(Nat.is_eq(List.length(&2, T.Seen, r), w), _)
1532	          == Bool.and(Nat.is_eq(List.length(&2, T.Seen, r), w), B.rows_wide(T.Seen, w, t)) : Bool}
1533	      {==}
1534	
1535	law start_shaped:
1536	  for +w: Nat
1537	  for +h: Nat
1538	  for +g: T.Grid(T.Seen)
1539	  {B.shaped(Maybe<&2, Bool>, w, h, S.start(g)) == B.shaped(T.Seen, w, h, g) : Bool}
1540	
1541	def start_shaped(w, h, g):
1542	  %Equal.sym(Nat, List.length(&2, List<&2, Maybe<&2, Bool>>, S.start(g)), List.length(&2, List<&2, T.Seen>, g), start_len(g)) :
1543	    {Bool.and(Nat.is_eq(_, h), B.rows_wide(Maybe<&2, Bool>, w, S.start(g)))
1544	      == Bool.and(Nat.is_eq(List.length(&2, List<&2, T.Seen>, g), h), B.rows_wide(T.Seen, w, g)) : Bool}
1545	  %Equal.sym(Bool, B.rows_wide(Maybe<&2, Bool>, w, S.start(g)), B.rows_wide(T.Seen, w, g), start_wide(w, g)) :
1546	    {Bool.and(Nat.is_eq(List.length(&2, List<&2, T.Seen>, g), h), _)
1547	      == Bool.and(Nat.is_eq(List.length(&2, List<&2, T.Seen>, g), h), B.rows_wide(T.Seen, w, g)) : Bool}
1548	  {==}
1549	
1550	def start_comp.cell(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +q: T.Pos, +s: T.Seen,
1551	  ag: {L.agrees(w, h, layout, q, s) == True{} : Bool}) ->
1552	  {cmp_cell(S.start.cell(s), B.mine(layout, q)) == True{} : Bool}:
1553	  match s:
1554	    case T.Hidden{}:
1555	      {==}
1556	    case T.Shown{k}:
1557	      %Equal.sym(Bool, B.mine(layout, q), False{}, P.not_true(B.mine(layout, q),
1558	        %Equal.sym(Bool, B.mine(layout, q), L.mine(layout, q), PC.mine_eq(layout, q)) : {Bool.not(_) == True{} : Bool};
1559	        P.and_true_l(Bool.not(L.mine(layout, q)), Nat.is_eq(L.adj_mines(w, h, layout, q), k), ag))) :
1560	        {beq(_, False{}) == True{} : Bool}
1561	      {==}
1562	    case T.Boom{}:
1563	      %Equal.sym(Bool, B.mine(layout, q), True{},
1564	        %Equal.sym(Bool, B.mine(layout, q), L.mine(layout, q), PC.mine_eq(layout, q)) : {_ == True{} : Bool}; ag) :
1565	        {beq(_, True{}) == True{} : Bool}
1566	      {==}
1567	
1568	law start_comp.go:
1569	  for +w: Nat
1570	  for +h: Nat
1571	  for +rows: T.Grid(T.Seen)
1572	  for +layout: T.Grid(Bool)
1573	  for +ps: List<&2, T.Pos>
1574	  for +ag: {L.agrees_all(w, h, rows, layout, ps) == True{} : Bool}
1575	  {PS.allp(~CE, ~cmp_f, CE{S.start(rows), layout}, ps) == True{} : Bool}
1576	
1577	def start_comp.go(w, h, rows, layout, ps, ag):
1578	  match ps:
1579	    case Nil{}:
1580	      {==}
1581	    case +q <> +t:
1582	      +s = L.at(T.Seen, T.Hidden{}, rows, q)
1583	      +a1 = L.agrees(w, h, layout, q, s)
1584	      %Equal.sym(Bool, cmp_f(CE{S.start(rows), layout}, q), True{},
1585	        %Equal.sym(Maybe<&2, Bool>, S.look(S.start(rows), q), S.start.cell(B.at(T.Seen, T.Hidden{}, rows, q)), start_at(rows, q)) :
1586	          {cmp_cell(_, B.mine(layout, q)) == True{} : Bool};
1587	        %Equal.sym(T.Seen, B.at(T.Seen, T.Hidden{}, rows, q), L.at(T.Seen, T.Hidden{}, rows, q), PC.at_eq(T.Seen, T.Hidden{}, rows, q)) :
1588	          {cmp_cell(S.start.cell(_), B.mine(layout, q)) == True{} : Bool};
1589	        start_comp.cell(w, h, layout, q, s, P.and_true_l(a1, L.agrees_all(w, h, rows, layout, t), ag))) :
1590	        {Bool.and(_, PS.allp(~CE, ~cmp_f, CE{S.start(rows), layout}, t)) == True{} : Bool}
1591	      start_comp.go(w, h, rows, layout, t, P.and_true_r(a1, L.agrees_all(w, h, rows, layout, t), ag))
1592	
1593	# A consistent layout completes the starting partial layout.
1594	law start_comp:
1595	  for +w: Nat
1596	  for +h: Nat
1597	  for +n: Nat
1598	  for +rows: T.Grid(T.Seen)
1599	  for +layout: T.Grid(Bool)
1600	  for cons: {L.consistent(T.Knowledge{w, h, n, rows}, layout) == True{} : Bool}
1601	  {completes(w, h, S.start(rows), layout) == True{} : Bool}
1602	
1603	def start_comp(w, h, n, rows, layout, cons):
1604	  +a = L.shaped(Bool, w, h, layout)
1605	  +b = L.shaped(T.Seen, w, h, rows)
1606	  +c = Nat.is_eq(L.total_mines(layout), n)
1607	  +d = L.agrees_all(w, h, rows, layout, L.cells(w, h))
1608	  start_comp.go(w, h, rows, layout, B.cells(w, h),
1609	    %Equal.sym(List<&2, T.Pos>, B.cells(w, h), L.cells(w, h), PC.cells_eq(w, h)) :
1610	      {L.agrees_all(w, h, rows, layout, _) == True{} : Bool};
1611	    PW.and4_d(a, b, c, d, cons))
1612	
1613	# The items, the to-do list and the hidden cells
1614	# ==============================================
1615	
1616	law adj_onb:
1617	  for +w: Nat
1618	  for +h: Nat
1619	  for +s: T.Pos
1620	  for +ns: List<&2, T.Pos>
1621	  for +a: {PS.allp(~PS.WHS, ~PS.adj_on, PS.WHS{w, h, s}, ns) == True{} : Bool}
1622	  {PS.allp(~PS.WH, ~PS.onb, PS.WH{w, h}, ns) == True{} : Bool}
1623	
1624	def adj_onb(w, h, s, ns, a):
1625	  match ns:
1626	    case Nil{}:
1627	      {==}
1628	    case +q <> +t:
1629	      +hq = PS.allp_head(~PS.WHS, ~PS.adj_on, PS.WHS{w, h, s}, q, t, a)
1630	      %Equal.sym(Bool, B.on_board(w, h, q), True{}, P.and_true_r(B.adjacent(s, q), B.on_board(w, h, q), hq)) :
1631	        {Bool.and(_, PS.allp(~PS.WH, ~PS.onb, PS.WH{w, h}, t)) == True{} : Bool}
1632	      adj_onb(w, h, s, t, PS.allp_tail(~PS.WHS, ~PS.adj_on, PS.WHS{w, h, s}, q, t, a))
1633	
1634	def items_onb.cell(+w: Nat, +h: Nat, +rows: T.Grid(T.Seen), +p: T.Pos, +t: List<&2, T.Pos>, +s: T.Seen,
1635	  on: {B.on_board(w, h, p) == True{} : Bool},
1636	  ih: {items_onb(PS.WH{w, h}, S.items(w, h, rows, t)) == True{} : Bool}) ->
1637	  {items_onb(PS.WH{w, h}, S.items.put(s, p, w, h, S.items(w, h, rows, t))) == True{} : Bool}:
1638	  match s:
1639	    case T.Hidden{}:
1640	      ih
1641	    case T.Shown{k}:
1642	      %Equal.sym(Bool, B.on_board(w, h, p), True{}, on) :
1643	        {Bool.and(Bool.and(_, PS.allp(~PS.WH, ~PS.onb, PS.WH{w, h}, B.neighbours(w, h, p))),
1644	          items_onb(PS.WH{w, h}, S.items(w, h, rows, t))) == True{} : Bool}
1645	      %Equal.sym(Bool, PS.allp(~PS.WH, ~PS.onb, PS.WH{w, h}, B.neighbours(w, h, p)), True{},
1646	        adj_onb(w, h, p, B.neighbours(w, h, p), PS.neighbours_all(w, h, p))) :
1647	        {Bool.and(Bool.and(True{}, _), items_onb(PS.WH{w, h}, S.items(w, h, rows, t))) == True{} : Bool}
1648	      ih
1649	    case T.Boom{}:
1650	      %Equal.sym(Bool, B.on_board(w, h, p), True{}, on) :
1651	        {Bool.and(Bool.and(_, True{}), items_onb(PS.WH{w, h}, S.items(w, h, rows, t))) == True{} : Bool}
1652	      ih
1653	
1654	law items_onb_all:
1655	  for +w: Nat
1656	  for +h: Nat
1657	  for +rows: T.Grid(T.Seen)
1658	  for +ps: List<&2, T.Pos>
1659	  for +ons: {PS.allp(~PS.WH, ~PS.onb, PS.WH{w, h}, ps) == True{} : Bool}
1660	  {items_onb(PS.WH{w, h}, S.items(w, h, rows, ps)) == True{} : Bool}
1661	
1662	def items_onb_all(w, h, rows, ps, ons):
1663	  match ps:
1664	    case Nil{}:
1665	      {==}
1666	    case +p <> +t:
1667	      items_onb.cell(w, h, rows, p, t, B.at(T.Seen, T.Hidden{}, rows, p),
1668	        PS.allp_head(~PS.WH, ~PS.onb, PS.WH{w, h}, p, t, ons),
1669	        items_onb_all(w, h, rows, t, PS.allp_tail(~PS.WH, ~PS.onb, PS.WH{w, h}, p, t, ons)))
1670	
1671	def around_ok.cell(+b: Bool, +i: S.Item, +rest: List<&2, S.Item>, +layout: T.Grid(Bool),
1672	  hi: {S.items_ok([i], layout) == True{} : Bool}, hr: {S.items_ok(rest, layout) == True{} : Bool}) ->
1673	  {S.items_ok(List.filter.put(S.Item, i, rest, b), layout) == True{} : Bool}:
1674	  match b:
1675	    case False{}:
1676	      hr
1677	    case True{}:
1678	      match i:
1679	        case S.Item{p, s, ns}:
1680	          %Equal.sym(Bool, S.items_ok(rest, layout), True{}, hr) :
1681	            {Bool.and(S.item_ok(s, p, ns, layout), _) == True{} : Bool}
1682	          hi
1683	
1684	law around_ok:
1685	  for +its: List<&2, S.Item>
1686	  for +c: T.Pos
1687	  for +layout: T.Grid(Bool)
1688	  for +ok: {S.items_ok(its, layout) == True{} : Bool}
1689	  {S.items_ok(S.around(its, c), layout) == True{} : Bool}
1690	
1691	def around_ok(its, c, layout, ok):
1692	  match its:
1693	    case Nil{}:
1694	      {==}
1695	    case S.Item{p, s, ns} <> t:
1696	      +i = {S.Item{p, s, ns} : S.Item}
1697	      +o1 = S.item_ok(s, p, ns, layout)
1698	      around_ok.cell(S.is_number(s) && B.contains(ns, c), i, S.around(t, c), layout,
1699	        %Equal.sym(Bool, Bool.and(o1, True{}), o1, P.and_true_r_id(o1)) : {_ == True{} : Bool};
1700	          P.and_true_l(o1, S.items_ok(t, layout), ok),
1701	        around_ok(t, c, layout, P.and_true_r(o1, S.items_ok(t, layout), ok)))
1702	
1703	def around_onb.cell(+e: PS.WH, +i: S.Item, +rest: List<&2, S.Item>, +b: Bool,
1704	  hi: {item_onb(e, i) == True{} : Bool}, hr: {items_onb(e, rest) == True{} : Bool}) ->
1705	  {items_onb(e, List.filter.put(S.Item, i, rest, b)) == True{} : Bool}:
1706	  match b:
1707	    case False{}:
1708	      hr
1709	    case True{}:
1710	      %Equal.sym(Bool, item_onb(e, i), True{}, hi) : {Bool.and(_, items_onb(e, rest)) == True{} : Bool}
1711	      hr
1712	
1713	law around_onb:
1714	  for +e: PS.WH
1715	  for +its: List<&2, S.Item>
1716	  for +c: T.Pos
1717	  for +ok: {items_onb(e, its) == True{} : Bool}
1718	  {items_onb(e, S.around(its, c)) == True{} : Bool}
1719	
1720	def around_onb(e, its, c, ok):
1721	  match its:
1722	    case Nil{}:
1723	      {==}
1724	    case S.Item{p, s, ns} <> t:
1725	      +i = {S.Item{p, s, ns} : S.Item}
1726	      around_onb.cell(e, i, S.around(t, c), S.is_number(s) && B.contains(ns, c),
1727	        P.and_true_l(item_onb(e, i), items_onb(e, t), ok),
1728	        around_onb(e, t, c, P.and_true_r(item_onb(e, i), items_onb(e, t), ok)))
1729	
1730	law todos_ok_all:
1731	  for +its: List<&2, S.Item>
1732	  for +cs: List<&2, T.Pos>
1733	  for +layout: T.Grid(Bool)
1734	  for +ok: {S.items_ok(its, layout) == True{} : Bool}
1735	  {todos_ok(S.todos(its, cs), layout) == True{} : Bool}
1736	
1737	def todos_ok_all(its, cs, layout, ok):
1738	  match cs:
1739	    case Nil{}:
1740	      {==}
1741	    case c <> t:
1742	      %Equal.sym(Bool, S.items_ok(S.around(its, c), layout), True{}, around_ok(its, c, layout, ok)) :
1743	        {Bool.and(_, todos_ok(S.todos(its, t), layout)) == True{} : Bool}
1744	      todos_ok_all(its, t, layout, ok)
1745	
1746	law todos_onb_all:
1747	  for +e: PS.WH
1748	  for +its: List<&2, S.Item>
1749	  for +cs: List<&2, T.Pos>
1750	  for +ok: {items_onb(e, its) == True{} : Bool}
1751	  {todos_onb(e, S.todos(its, cs)) == True{} : Bool}
1752	
1753	def todos_onb_all(e, its, cs, ok):
1754	  match cs:
1755	    case Nil{}:
1756	      {==}
1757	    case c <> t:
1758	      %Equal.sym(Bool, items_onb(e, S.around(its, c)), True{}, around_onb(e, its, c, ok)) :
1759	        {Bool.and(_, todos_onb(e, S.todos(its, t))) == True{} : Bool}
1760	      todos_onb_all(e, its, t, ok)
1761	
1762	def tok_put(+b: Bool, +t: S.Todo, +rest: List<&2, S.Todo>, +layout: T.Grid(Bool),
1763	  ht: {todos_ok([t], layout) == True{} : Bool}, hr: {todos_ok(rest, layout) == True{} : Bool}) ->
1764	  {todos_ok(List.filter.put(S.Todo, t, rest, b), layout) == True{} : Bool}:
1765	  match b:
1766	    case False{}:
1767	      hr
1768	    case True{}:
1769	      match t:
1770	        case S.Todo{c, rel}:
1771	          %Equal.sym(Bool, todos_ok(rest, layout), True{}, hr) : {Bool.and(S.items_ok(rel, layout), _) == True{} : Bool}
1772	          ht
1773	
1774	def ton_put(+b: Bool, +e: PS.WH, +t: S.Todo, +rest: List<&2, S.Todo>,
1775	  ht: {todos_onb(e, [t]) == True{} : Bool}, hr: {todos_onb(e, rest) == True{} : Bool}) ->
1776	  {todos_onb(e, List.filter.put(S.Todo, t, rest, b)) == True{} : Bool}:
1777	  match b:
1778	    case False{}:
1779	      hr
1780	    case True{}:
1781	      match t:
1782	        case S.Todo{c, rel}:
1783	          %Equal.sym(Bool, todos_onb(e, rest), True{}, hr) : {Bool.and(items_onb(e, rel), _) == True{} : Bool}
1784	          ht
1785	
1786	law tok_append:
1787	  for +xs: List<&2, S.Todo>
1788	  for +ys: List<&2, S.Todo>
1789	  for +layout: T.Grid(Bool)
1790	  for +a: {todos_ok(xs, layout) == True{} : Bool}
1791	  for b: {todos_ok(ys, layout) == True{} : Bool}
1792	  {todos_ok(List.append(&2, S.Todo, xs, ys), layout) == True{} : Bool}
1793	
1794	def tok_append(xs, ys, layout, a, b):
1795	  match xs:
1796	    case Nil{}:
1797	      b
1798	    case S.Todo{c, rel} <> t:
1799	      %Equal.sym(Bool, S.items_ok(rel, layout), True{}, P.and_true_l(S.items_ok(rel, layout), todos_ok(t, layout), a)) :
1800	        {Bool.and(_, todos_ok(List.append(&2, S.Todo, t, ys), layout)) == True{} : Bool}
1801	      tok_append(t, ys, layout, P.and_true_r(S.items_ok(rel, layout), todos_ok(t, layout), a), b)
1802	
1803	law ton_append:
1804	  for +e: PS.WH
1805	  for +xs: List<&2, S.Todo>
1806	  for +ys: List<&2, S.Todo>
1807	  for +a: {todos_onb(e, xs) == True{} : Bool}
1808	  for b: {todos_onb(e, ys) == True{} : Bool}
1809	  {todos_onb(e, List.append(&2, S.Todo, xs, ys)) == True{} : Bool}
1810	
1811	def ton_append(e, xs, ys, a, b):
1812	  match xs:
1813	    case Nil{}:
1814	      b
1815	    case S.Todo{c, rel} <> t:
1816	      %Equal.sym(Bool, items_onb(e, rel), True{}, P.and_true_l(items_onb(e, rel), todos_onb(e, t), a)) :
1817	        {Bool.and(_, todos_onb(e, List.append(&2, S.Todo, t, ys))) == True{} : Bool}
1818	      ton_append(e, t, ys, P.and_true_r(items_onb(e, rel), todos_onb(e, t), a), b)
1819	
1820	def tok_head(+t: S.Todo, +rest: List<&2, S.Todo>, +layout: T.Grid(Bool),
1821	  h: {todos_ok(t <> rest, layout) == True{} : Bool}) -> {todos_ok([t], layout) == True{} : Bool}:
1822	  match t:
1823	    case S.Todo{c, rel}:
1824	      %Equal.sym(Bool, Bool.and(S.items_ok(rel, layout), True{}), S.items_ok(rel, layout), P.and_true_r_id(S.items_ok(rel, layout))) :
1825	        {_ == True{} : Bool}
1826	      P.and_true_l(S.items_ok(rel, layout), todos_ok(rest, layout), h)
1827	
1828	def tok_tail(+t: S.Todo, +rest: List<&2, S.Todo>, +layout: T.Grid(Bool),
1829	  h: {todos_ok(t <> rest, layout) == True{} : Bool}) -> {todos_ok(rest, layout) == True{} : Bool}:
1830	  match t:
1831	    case S.Todo{c, rel}:
1832	      P.and_true_r(S.items_ok(rel, layout), todos_ok(rest, layout), h)
1833	
1834	def ton_head(+e: PS.WH, +t: S.Todo, +rest: List<&2, S.Todo>,
1835	  h: {todos_onb(e, t <> rest) == True{} : Bool}) -> {todos_onb(e, [t]) == True{} : Bool}:
1836	  match t:
1837	    case S.Todo{c, rel}:
1838	      %Equal.sym(Bool, Bool.and(items_onb(e, rel), True{}), items_onb(e, rel), P.and_true_r_id(items_onb(e, rel))) :
1839	        {_ == True{} : Bool}
1840	      P.and_true_l(items_onb(e, rel), todos_onb(e, rest), h)
1841	
1842	def ton_tail(+e: PS.WH, +t: S.Todo, +rest: List<&2, S.Todo>,
1843	  h: {todos_onb(e, t <> rest) == True{} : Bool}) -> {todos_onb(e, rest) == True{} : Bool}:
1844	  match t:
1845	    case S.Todo{c, rel}:
1846	      P.and_true_r(items_onb(e, rel), todos_onb(e, rest), h)
1847	
1848	law tok_order:
1849	  for +ts: List<&2, S.Todo>
1850	  for +layout: T.Grid(Bool)
1851	  for +h: {todos_ok(ts, layout) == True{} : Bool}
1852	  {todos_ok(S.nears(ts), layout) == True{} : Bool}
1853	
1854	def tok_order(ts, layout, h):
1855	  match ts:
1856	    case Nil{}:
1857	      {==}
1858	    case +t <> +rest:
1859	      tok_put(S.has_rel(t), t, S.nears(rest), layout, tok_head(t, rest, layout, h),
1860	        tok_order(rest, layout, tok_tail(t, rest, layout, h)))
1861	
1862	law tok_order_f:
1863	  for +ts: List<&2, S.Todo>
1864	  for +layout: T.Grid(Bool)
1865	  for +h: {todos_ok(ts, layout) == True{} : Bool}
1866	  {todos_ok(S.fars(ts), layout) == True{} : Bool}
1867	
1868	def tok_order_f(ts, layout, h):
1869	  match ts:
1870	    case Nil{}:
1871	      {==}
1872	    case +t <> +rest:
1873	      tok_put(Bool.not(S.has_rel(t)), t, S.fars(rest), layout, tok_head(t, rest, layout, h),
1874	        tok_order_f(rest, layout, tok_tail(t, rest, layout, h)))
1875	
1876	law ton_order:
1877	  for +e: PS.WH
1878	  for +ts: List<&2, S.Todo>
1879	  for +h: {todos_onb(e, ts) == True{} : Bool}
1880	  {todos_onb(e, S.nears(ts)) == True{} : Bool}
1881	
1882	def ton_order(e, ts, h):
1883	  match ts:
1884	    case Nil{}:
1885	      {==}
1886	    case +t <> +rest:
1887	      ton_put(S.has_rel(t), e, t, S.nears(rest), ton_head(e, t, rest, h), ton_order(e, rest, ton_tail(e, t, rest, h)))
1888	
1889	law ton_order_f:
1890	  for +e: PS.WH
1891	  for +ts: List<&2, S.Todo>
1892	  for +h: {todos_onb(e, ts) == True{} : Bool}
1893	  {todos_onb(e, S.fars(ts)) == True{} : Bool}
1894	
1895	def ton_order_f(e, ts, h):
1896	  match ts:
1897	    case Nil{}:
1898	      {==}
1899	    case +t <> +rest:
1900	      ton_put(Bool.not(S.has_rel(t)), e, t, S.fars(rest), ton_head(e, t, rest, h), ton_order_f(e, rest, ton_tail(e, t, rest, h)))
1901	
1902	law tcontains_todos:
1903	  for +its: List<&2, S.Item>
1904	  for +cs: List<&2, T.Pos>
1905	  for +q: T.Pos
1906	  {tcontains(S.todos(its, cs), q) == B.contains(cs, q) : Bool}
1907	
1908	def tcontains_todos(its, cs, q):
1909	  match cs:
1910	    case Nil{}:
1911	      {==}
1912	    case c <> t:
1913	      %tcontains_todos(its, t, q) : {Bool.or(B.same(c, q), tcontains(S.todos(its, t), q)) == Bool.or(B.same(c, q), _) : Bool}
1914	      {==}
1915	
1916	def tput_keeps(+b: Bool, +t: S.Todo, +rest: List<&2, S.Todo>, +q: T.Pos, m: {tcontains(rest, q) == True{} : Bool}) ->
1917	  {tcontains(List.filter.put(S.Todo, t, rest, b), q) == True{} : Bool}:
1918	  match b:
1919	    case False{}:
1920	      m
1921	    case True{}:
1922	      match t:
1923	        case S.Todo{c, rel}:
1924	          %Equal.sym(Bool, tcontains(rest, q), True{}, m) : {Bool.or(B.same(c, q), _) == True{} : Bool}
1925	          PS.or_true_r(B.same(c, q))
1926	
1927	def tput_self(+b: Bool, +c: T.Pos, +rel: List<&2, S.Item>, +rest: List<&2, S.Todo>, +q: T.Pos,
1928	  bt: {b == True{} : Bool}, cq: {B.same(c, q) == True{} : Bool}) ->
1929	  {tcontains(List.filter.put(S.Todo, S.Todo{c, rel}, rest, b), q) == True{} : Bool}:
1930	  match b:
1931	    case True{}:
1932	      %Equal.sym(Bool, B.same(c, q), True{}, cq) : {Bool.or(_, tcontains(rest, q)) == True{} : Bool}
1933	      {==}
1934	    case False{}:
1935	      Empty.absurd({tcontains(rest, q) == True{} : Bool}, P.false_ne_true(bt))
1936	
1937	def or_l(+a: Bool, +b: Bool, e: {a == True{} : Bool}) -> {Bool.or(a, b) == True{} : Bool}:
1938	  %Equal.sym(Bool, a, True{}, e) : {Bool.or(_, b) == True{} : Bool}
1939	  {==}
1940	
1941	def or_r(+a: Bool, +b: Bool, e: {b == True{} : Bool}) -> {Bool.or(a, b) == True{} : Bool}:
1942	  %Equal.sym(Bool, b, True{}, e) : {Bool.or(a, _) == True{} : Bool}
1943	  PS.or_true_r(a)
1944	
1945	def or_cases(+a: Bool, +b: Bool, e: {Bool.or(a, b) == True{} : Bool}) -> Or({a == True{} : Bool}, {b == True{} : Bool}):
1946	  match a:
1947	    case True{}:
1948	      Inl{{==}}
1949	    case False{}:
1950	      Inr{e}
1951	
1952	def order_split.self(+c: T.Pos, +rel: List<&2, S.Item>, +rest: List<&2, S.Todo>, +q: T.Pos,
1953	  cq: {B.same(c, q) == True{} : Bool}, +hr: Bool, hre: {S.has_rel(S.Todo{c, rel}) == hr : Bool}) ->
1954	  {Bool.or(tcontains(List.filter.put(S.Todo, S.Todo{c, rel}, S.nears(rest), hr), q),
1955	    tcontains(List.filter.put(S.Todo, S.Todo{c, rel}, S.fars(rest), Bool.not(hr)), q)) == True{} : Bool}:
1956	  match hr:
1957	    case True{}:
1958	      or_l(tcontains(List.filter.put(S.Todo, S.Todo{c, rel}, S.nears(rest), True{}), q),
1959	        tcontains(List.filter.put(S.Todo, S.Todo{c, rel}, S.fars(rest), False{}), q),
1960	        tput_self(True{}, c, rel, S.nears(rest), q, {==}, cq))
1961	    case False{}:
1962	      or_r(tcontains(List.filter.put(S.Todo, S.Todo{c, rel}, S.nears(rest), False{}), q),
1963	        tcontains(List.filter.put(S.Todo, S.Todo{c, rel}, S.fars(rest), True{}), q),
1964	        tput_self(True{}, c, rel, S.fars(rest), q, {==}, cq))
1965	
1966	def order_split.rest(+t: S.Todo, +rest: List<&2, S.Todo>, +q: T.Pos, +hr: Bool,
1967	  r: Or({tcontains(S.nears(rest), q) == True{} : Bool}, {tcontains(S.fars(rest), q) == True{} : Bool})) ->
1968	  {Bool.or(tcontains(List.filter.put(S.Todo, t, S.nears(rest), hr), q),
1969	    tcontains(List.filter.put(S.Todo, t, S.fars(rest), Bool.not(hr)), q)) == True{} : Bool}:
1970	  match r:
1971	    case Inl{a}:
1972	      or_l(tcontains(List.filter.put(S.Todo, t, S.nears(rest), hr), q),
1973	        tcontains(List.filter.put(S.Todo, t, S.fars(rest), Bool.not(hr)), q), tput_keeps(hr, t, S.nears(rest), q, a))
1974	    case Inr{b}:
1975	      or_r(tcontains(List.filter.put(S.Todo, t, S.nears(rest), hr), q),
1976	        tcontains(List.filter.put(S.Todo, t, S.fars(rest), Bool.not(hr)), q), tput_keeps(Bool.not(hr), t, S.fars(rest), q, b))
1977	
1978	def order_split.cell(+c: T.Pos, +rel: List<&2, S.Item>, +rest: List<&2, S.Todo>, +q: T.Pos,
1979	  r: Or({B.same(c, q) == True{} : Bool}, {tcontains(rest, q) == True{} : Bool}),
1980	  ih: {tcontains(rest, q) == True{} : Bool} ->
1981	    {Bool.or(tcontains(S.nears(rest), q), tcontains(S.fars(rest), q)) == True{} : Bool}) ->
1982	  {Bool.or(tcontains(S.nears(S.Todo{c, rel} <> rest), q), tcontains(S.fars(S.Todo{c, rel} <> rest), q)) == True{} : Bool}:
1983	  match r:
1984	    case Inl{cq}:
1985	      order_split.self(c, rel, rest, q, cq, S.has_rel(S.Todo{c, rel}), {==})
1986	    case Inr{m}:
1987	      order_split.rest(S.Todo{c, rel}, rest, q, S.has_rel(S.Todo{c, rel}),
1988	        or_cases(tcontains(S.nears(rest), q), tcontains(S.fars(rest), q), ih(m)))
1989	
1990	# A to-do cell is in the near part or the far part.
1991	law order_split:
1992	  for +ts: List<&2, S.Todo>
1993	  for +q: T.Pos
1994	  for m: {tcontains(ts, q) == True{} : Bool}
1995	  {Bool.or(tcontains(S.nears(ts), q), tcontains(S.fars(ts), q)) == True{} : Bool}
1996	
1997	def order_split(ts, q, m):
1998	  match ts:
1999	    case Nil{}:
2000	      Empty.absurd({False{} == True{} : Bool}, P.false_ne_true(m))
Lines 1-2000 of 2855. More: https://jend.leeeet.dev/read.txt?path=minebender-game@1.0.0.0/proof_solver.bend&start_line=2001