proof_solver.bend

minebender-game@1.0.0.0 · 2,855 lines · 199 definitions

1import Base
2import minebender-game@1.0.0.0/types.bend as T
3import minebender-game@1.0.0.0/board.bend as B
4import minebender-game@1.0.0.0/solver.bend as S
5import minebender-game@1.0.0.0/LAWS.bend as L
6import minebender-game@1.0.0.0/proof_base.bend as P
7import minebender-game@1.0.0.0/proof_grid.bend as PG
8import minebender-game@1.0.0.0/proof_copy.bend as PC
9import minebender-game@1.0.0.0/proof_lists.bend as PL
10import minebender-game@1.0.0.0/proof_cells.bend as PS
11import minebender-game@1.0.0.0/proof_sums.bend as PU
12import minebender-game@1.0.0.0/proof_walk.bend as PW
13import minebender-game@1.0.0.0/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
21def one(b: Bool) -> Nat:
22  Bool.pick(Nat, b, 1n, 0n)
23
24def tf(m: Maybe<&2, Bool>) -> Nat:
25  S.one_if(S.is_true(m))
26
27def nf(m: Maybe<&2, Bool>) -> Nat:
28  S.one_if(S.is_none(m))
29
30law row_mines_sum:
31  for +r: List<&2, Bool>
32  {B.row_mines(r) == PU.rsum(~Bool, ~one, r) : Nat}
33
34def 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
42law total_sum:
43  for +g: T.Grid(Bool)
44  {B.total_mines(g) == PU.gsum(~Bool, ~one, g) : Nat}
45
46def 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
55law 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
60def 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
70law 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
74def 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
82law 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
86def 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
94law 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
98def 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
107law 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
111def 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
120law 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
125def 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
135law 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
140def 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
153def 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
164law beq_sound:
165  for +a: Bool
166  for +b: Bool
167  for e: {beq(a, b) == True{} : Bool}
168  {a == b : Bool}
169
170def 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
181law beq_refl:
182  for +a: Bool
183  {beq(a, a) == True{} : Bool}
184
185def beq_refl(a):
186  match a:
187    case True{}:
188      {==}
189    case False{}:
190      {==}
191
192def 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
199type CE is Data:
200  CE{part: T.Grid(Maybe<&2, Bool>), layout: T.Grid(Bool)}
201
202def 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
207def 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.
211def 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
214law 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
224def 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
227law 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
233def 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
241law 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
247def 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
259law 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
269def 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
280law 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
291def 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
310def 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.
316def 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
323def 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
329def 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
356law 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
367def 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.
384law 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
399def 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
422law 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
429def 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
438law 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
444def 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).
454law 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
459def 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
469law 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
473def 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
482law 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
486def 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
495law 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
500def 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
513law 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
519def 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
531type AG is Data:
532  AG{l1: T.Grid(Bool), l2: T.Grid(Bool)}
533
534def 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
539def ag_f(e: AG, q: T.Pos) -> Bool:
540  ag_f.go(e, q)
541
542def 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
545law 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
555def 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
559law 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
569def 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
581law 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
588def 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
594law 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
604def 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
610def 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
626law 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
636def 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
653law 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
667def 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
686def 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
693type CV is Data:
694  CV{todo: List<&2, S.Todo>, part: T.Grid(Maybe<&2, Bool>)}
695
696def 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
701def 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.
705def 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
708def 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
715def 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
722def 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
736law 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
746def 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
757def 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
764def 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
783law 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
797def 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
811def 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
832law 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
846def 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
863def 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
877law 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
885def 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
899def disc_some(-A: Data, m: Maybe<&2, A>) -> Type:
900  match m:
901    case None{}:
902      Empty
903    case Some{v}:
904      Unit
905
906def some_ne_none(-A: Data, -a: A, e: {Some{a} == None{} : Maybe<&2, A>}) -> Empty:
907  %e : disc_some(A, _)
908  Unit{}
909
910def 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
918def 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
926def 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
934def 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
975def 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
1002law 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
1012def 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).
1020law 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
1040def 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
1069def 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
1077def 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
1086def 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
1089def 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
1098def 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
1104def 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
1113def 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.
1121law 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
1129def 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
1138def 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
1161def 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
1171def 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
1186def 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
1198def 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
1207def 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.
1234law 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
1245def 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.
1259law 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
1269def 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
1292def 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.
1303law 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
1316def 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
1342def 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
1355def 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
1384law 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
1392def 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.
1403law 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
1412def 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
1444law 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
1450def 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
1459law 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
1465def 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.
1475law 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
1480def 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
1491law 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
1495def 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
1504law 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
1508def 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
1517law 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
1522def 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
1535law 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
1541def 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
1550def 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
1568law 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
1577def 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.
1594law 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
1603def 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
1616law 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
1624def 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
1634def 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
1654law 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
1662def 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
1671def 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
1684law 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
1691def 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
1703def 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
1713law 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
1720def 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
1730law 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
1737def 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
1746law 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
1753def 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
1762def 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
1774def 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
1786law 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
1794def 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
1803law 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
1811def 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
1820def 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
1828def 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
1834def 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
1842def 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
1848law 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
1854def 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
1862law 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
1868def 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
1876law 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
1882def 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
1889law 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
1895def 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
1902law 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
1908def 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
1916def 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
1927def 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
1937def 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
1941def 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
1945def 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
1952def 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
1966def 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
1978def 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.
1991law 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
1997def order_split(ts, q, m):
1998  match ts:
1999    case Nil{}:
2000      Empty.absurd({False{} == True{} : Bool}, P.false_ne_true(m))
2001    case S.Todo{c, rel} <> rest:
2002      order_split.cell(c, rel, rest, q, or_cases(B.same(c, q), tcontains(rest, q), m), mr => order_split(rest, q, mr))
2003
2004law tcontains_append:
2005  for +xs: List<&2, S.Todo>
2006  for +ys: List<&2, S.Todo>
2007  for +q: T.Pos
2008  {tcontains(List.append(&2, S.Todo, xs, ys), q) == Bool.or(tcontains(xs, q), tcontains(ys, q)) : Bool}
2009
2010def tcontains_append(xs, ys, q):
2011  match xs:
2012    case Nil{}:
2013      {==}
2014    case S.Todo{c, rel} <> t:
2015      %Equal.sym(Bool, tcontains(List.append(&2, S.Todo, t, ys), q), Bool.or(tcontains(t, q), tcontains(ys, q)),
2016        tcontains_append(t, ys, q)) :
2017        {Bool.or(B.same(c, q), _) == Bool.or(Bool.or(B.same(c, q), tcontains(t, q)), tcontains(ys, q)) : Bool}
2018      PS.contains_append.or(B.same(c, q), tcontains(t, q), tcontains(ys, q))
2019
2020law order_member:
2021  for +ts: List<&2, S.Todo>
2022  for +q: T.Pos
2023  for m: {tcontains(ts, q) == True{} : Bool}
2024  {tcontains(S.order(ts), q) == True{} : Bool}
2025
2026def order_member(ts, q, m):
2027  %Equal.sym(Bool, tcontains(List.append(&2, S.Todo, S.nears(ts), S.fars(ts)), q),
2028    Bool.or(tcontains(S.nears(ts), q), tcontains(S.fars(ts), q)), tcontains_append(S.nears(ts), S.fars(ts), q)) :
2029    {_ == True{} : Bool}
2030  order_split(ts, q, m)
2031
2032def hc_member.go(+rows: T.Grid(T.Seen), +p: T.Pos, +t: List<&2, T.Pos>, +q: T.Pos,
2033  hq: {S.is_hidden(B.at(T.Seen, T.Hidden{}, rows, q)) == True{} : Bool},
2034  r: Or({B.same(p, q) == True{} : Bool}, {B.contains(t, q) == True{} : Bool}),
2035  ih: {B.contains(t, q) == True{} : Bool} -> {B.contains(S.hidden_cells(rows, t), q) == True{} : Bool}) ->
2036  {B.contains(S.hidden_cells(rows, p <> t), q) == True{} : Bool}:
2037  match r:
2038    case Inl{pq}:
2039      %Equal.sym(T.Pos, p, q, PG.same_sound(p, q, pq)) :
2040        {B.contains(List.filter.put(T.Pos, _, S.hidden_cells(rows, t), S.is_hidden(B.at(T.Seen, T.Hidden{}, rows, _))), q) == True{} : Bool}
2041      %Equal.sym(Bool, S.is_hidden(B.at(T.Seen, T.Hidden{}, rows, q)), True{}, hq) :
2042        {B.contains(List.filter.put(T.Pos, q, S.hidden_cells(rows, t), _), q) == True{} : Bool}
2043      PG.contains_cons_self(q, S.hidden_cells(rows, t))
2044    case Inr{m}:
2045      PS.put_keeps(p, S.hidden_cells(rows, t), S.is_hidden(B.at(T.Seen, T.Hidden{}, rows, p)), q, ih(m))
2046
2047# A hidden cell of ps is one of the hidden cells.
2048law hc_member:
2049  for +rows: T.Grid(T.Seen)
2050  for +ps: List<&2, T.Pos>
2051  for +q: T.Pos
2052  for m: {B.contains(ps, q) == True{} : Bool}
2053  for +hq: {S.is_hidden(B.at(T.Seen, T.Hidden{}, rows, q)) == True{} : Bool}
2054  {B.contains(S.hidden_cells(rows, ps), q) == True{} : Bool}
2055
2056def hc_member(rows, ps, q, m, hq):
2057  match ps:
2058    case Nil{}:
2059      Empty.absurd({False{} == True{} : Bool}, P.false_ne_true(m))
2060    case p <> t:
2061      hc_member.go(rows, p, t, q, hq, or_cases(B.same(p, q), B.contains(t, q), m), mt => hc_member(rows, t, q, mt, hq))
2062
2063def hc_sound.f(+rows: T.Grid(T.Seen), +p: T.Pos, +t: List<&2, T.Pos>, +q: T.Pos,
2064  r: {S.is_hidden(B.at(T.Seen, T.Hidden{}, rows, q)) == True{} : Bool} & {B.contains(t, q) == True{} : Bool}) ->
2065  {S.is_hidden(B.at(T.Seen, T.Hidden{}, rows, q)) == True{} : Bool} & {B.contains(p <> t, q) == True{} : Bool}:
2066  match r:
2067    case (a, b):
2068      (a, or_r(B.same(p, q), B.contains(t, q), b))
2069
2070def hc_sound.t(+rows: T.Grid(T.Seen), +p: T.Pos, +t: List<&2, T.Pos>, +q: T.Pos,
2071  be: {S.is_hidden(B.at(T.Seen, T.Hidden{}, rows, p)) == True{} : Bool},
2072  r: Or({B.same(p, q) == True{} : Bool}, {B.contains(S.hidden_cells(rows, t), q) == True{} : Bool}),
2073  ih: {B.contains(S.hidden_cells(rows, t), q) == True{} : Bool} ->
2074    {S.is_hidden(B.at(T.Seen, T.Hidden{}, rows, q)) == True{} : Bool} & {B.contains(t, q) == True{} : Bool}) ->
2075  {S.is_hidden(B.at(T.Seen, T.Hidden{}, rows, q)) == True{} : Bool} & {B.contains(p <> t, q) == True{} : Bool}:
2076  match r:
2077    case Inl{+pq}:
2078      (%PG.same_sound(p, q, pq) : {S.is_hidden(B.at(T.Seen, T.Hidden{}, rows, _)) == True{} : Bool}; be,
2079        or_l(B.same(p, q), B.contains(t, q), pq))
2080    case Inr{m}:
2081      hc_sound.f(rows, p, t, q, ih(m))
2082
2083def hc_sound.go(+rows: T.Grid(T.Seen), +p: T.Pos, +t: List<&2, T.Pos>, +q: T.Pos, +b: Bool,
2084  be: {S.is_hidden(B.at(T.Seen, T.Hidden{}, rows, p)) == b : Bool},
2085  m: {B.contains(List.filter.put(T.Pos, p, S.hidden_cells(rows, t), b), q) == True{} : Bool},
2086  ih: {B.contains(S.hidden_cells(rows, t), q) == True{} : Bool} ->
2087    {S.is_hidden(B.at(T.Seen, T.Hidden{}, rows, q)) == True{} : Bool} & {B.contains(t, q) == True{} : Bool}) ->
2088  {S.is_hidden(B.at(T.Seen, T.Hidden{}, rows, q)) == True{} : Bool} & {B.contains(p <> t, q) == True{} : Bool}:
2089  match b:
2090    case True{}:
2091      hc_sound.t(rows, p, t, q, be, or_cases(B.same(p, q), B.contains(S.hidden_cells(rows, t), q), m), ih)
2092    case False{}:
2093      hc_sound.f(rows, p, t, q, ih(m))
2094
2095# A hidden cell is hidden and one of the cells it was taken from.
2096law hc_sound:
2097  for +rows: T.Grid(T.Seen)
2098  for +ps: List<&2, T.Pos>
2099  for +q: T.Pos
2100  for m: {B.contains(S.hidden_cells(rows, ps), q) == True{} : Bool}
2101  {S.is_hidden(B.at(T.Seen, T.Hidden{}, rows, q)) == True{} : Bool} & {B.contains(ps, q) == True{} : Bool}
2102
2103def hc_sound(rows, ps, q, m):
2104  match ps:
2105    case Nil{}:
2106      Empty.absurd({S.is_hidden(B.at(T.Seen, T.Hidden{}, rows, q)) == True{} : Bool} & {B.contains(Nil{}, q) == True{} : Bool},
2107        P.false_ne_true(m))
2108    case p <> t:
2109      hc_sound.go(rows, p, t, q, S.is_hidden(B.at(T.Seen, T.Hidden{}, rows, p)), {==}, m, mt => hc_sound(rows, t, q, mt))
2110
2111# The search's start
2112# ==================
2113
2114def start_cover.seen(+w: Nat, +h: Nat, +rows: T.Grid(T.Seen), +its: List<&2, S.Item>, +q: T.Pos,
2115  on: {B.on_board(w, h, q) == True{} : Bool}, +s: T.Seen, se: {B.at(T.Seen, T.Hidden{}, rows, q) == s : T.Seen}) ->
2116  {Bool.or(Bool.not(S.is_none(S.start.cell(s))), tcontains(S.order(S.todos(its, S.hidden_cells(rows, B.cells(w, h)))), q))
2117    == True{} : Bool}:
2118  match s:
2119    case T.Hidden{}:
2120      +hs = S.hidden_cells(rows, B.cells(w, h))
2121      order_member(S.todos(its, hs), q,
2122        %Equal.sym(Bool, tcontains(S.todos(its, hs), q), B.contains(hs, q), tcontains_todos(its, hs, q)) : {_ == True{} : Bool};
2123        hc_member(rows, B.cells(w, h), q, PS.cells_member(w, h, q, on),
2124          %Equal.sym(T.Seen, B.at(T.Seen, T.Hidden{}, rows, q), T.Hidden{}, se) : {S.is_hidden(_) == True{} : Bool}; {==}))
2125    case T.Shown{k}:
2126      {==}
2127    case T.Boom{}:
2128      {==}
2129
2130def start_cover.cell(+w: Nat, +h: Nat, +rows: T.Grid(T.Seen), +its: List<&2, S.Item>, +c: T.Pos, +q: T.Pos,
2131  +shP: {B.shaped(Maybe<&2, Bool>, w, h, S.start(rows)) == True{} : Bool},
2132  on: {B.on_board(w, h, q) == True{} : Bool}, +b: Bool, be: {B.same(c, q) == b : Bool}) ->
2133  {cv_f(CV{S.order(S.todos(its, S.hidden_cells(rows, B.cells(w, h)))), B.set_at(Maybe<&2, Bool>, S.start(rows), c, Some{True{}})}, q)
2134    == True{} : Bool}:
2135  match b:
2136    case True{}:
2137      +todo = S.order(S.todos(its, S.hidden_cells(rows, B.cells(w, h))))
2138      %Equal.sym(T.Pos, c, q, PG.same_sound(c, q, be)) :
2139        {Bool.or(Bool.not(S.is_none(S.look(B.set_at(Maybe<&2, Bool>, S.start(rows), _, Some{True{}}), q))), tcontains(todo, q)) == True{} : Bool}
2140      %Equal.sym(Maybe<&2, Bool>, S.look(B.set_at(Maybe<&2, Bool>, S.start(rows), q, Some{True{}}), q), Some{True{}},
2141        set_look(w, h, S.start(rows), q, Some{True{}}, shP, on)) :
2142        {Bool.or(Bool.not(S.is_none(_)), tcontains(todo, q)) == True{} : Bool}
2143      {==}
2144    case False{}:
2145      +todo = S.order(S.todos(its, S.hidden_cells(rows, B.cells(w, h))))
2146      %Equal.sym(Maybe<&2, Bool>, S.look(B.set_at(Maybe<&2, Bool>, S.start(rows), c, Some{True{}}), q), S.look(S.start(rows), q),
2147        PL.at_set_ne(Maybe<&2, Bool>, S.start(rows), c, q, Some{True{}}, None{}, be)) :
2148        {Bool.or(Bool.not(S.is_none(_)), tcontains(todo, q)) == True{} : Bool}
2149      %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)) :
2150        {Bool.or(Bool.not(S.is_none(_)), tcontains(todo, q)) == True{} : Bool}
2151      start_cover.seen(w, h, rows, its, q, on, B.at(T.Seen, T.Hidden{}, rows, q), {==})
2152
2153law start_cover.go:
2154  for +w: Nat
2155  for +h: Nat
2156  for +rows: T.Grid(T.Seen)
2157  for +its: List<&2, S.Item>
2158  for +c: T.Pos
2159  for +shP: {B.shaped(Maybe<&2, Bool>, w, h, S.start(rows)) == True{} : Bool}
2160  for +ps: List<&2, T.Pos>
2161  for +ons: {PS.allp(~PS.WH, ~PS.onb, PS.WH{w, h}, ps) == True{} : Bool}
2162  {PS.allp(~CV, ~cv_f, CV{S.order(S.todos(its, S.hidden_cells(rows, B.cells(w, h)))),
2163    B.set_at(Maybe<&2, Bool>, S.start(rows), c, Some{True{}})}, ps) == True{} : Bool}
2164
2165def start_cover.go(w, h, rows, its, c, shP, ps, ons):
2166  match ps:
2167    case Nil{}:
2168      {==}
2169    case +q <> +t:
2170      +e0 = {CV{S.order(S.todos(its, S.hidden_cells(rows, B.cells(w, h)))), B.set_at(Maybe<&2, Bool>, S.start(rows), c, Some{True{}})} : CV}
2171      %Equal.sym(Bool, cv_f(e0, q), True{},
2172        start_cover.cell(w, h, rows, its, c, q, shP, PS.allp_head(~PS.WH, ~PS.onb, PS.WH{w, h}, q, t, ons), B.same(c, q), {==})) :
2173        {Bool.and(_, PS.allp(~CV, ~cv_f, e0, t)) == True{} : Bool}
2174      start_cover.go(w, h, rows, its, c, shP, t, PS.allp_tail(~PS.WH, ~PS.onb, PS.WH{w, h}, q, t, ons))
2175
2176# The outer loop
2177# ==============
2178
2179def all_valid(+ctx: S.Ctx, ls: List<&2, T.Grid(Bool)>) -> Bool:
2180  match ls:
2181    case Nil{}:
2182      True{}
2183    case l <> t:
2184      S.check(ctx, l) && all_valid(ctx, t)
2185
2186# A layout that passes the check and mines c.
2187def Witness(+ctx: S.Ctx, +c: T.Pos) -> Type:
2188  Exists(T.Grid(Bool), l => {S.check(ctx, l) == True{} : Bool} & {B.mine(l, c) == True{} : Bool})
2189
2190def covered_extract.go(+ctx: S.Ctx, +l: T.Grid(Bool), +t: List<&2, T.Grid(Bool)>, +c: T.Pos,
2191  +vl: {S.check(ctx, l) == True{} : Bool},
2192  r: Or({B.mine(l, c) == True{} : Bool}, {S.covered(t, c) == True{} : Bool}),
2193  ih: {S.covered(t, c) == True{} : Bool} -> Witness(ctx, c)) -> Witness(ctx, c):
2194  match r:
2195    case Inl{m}:
2196      (l, (vl, m))
2197    case Inr{cv}:
2198      ih(cv)
2199
2200law covered_extract:
2201  for +ctx: S.Ctx
2202  for +ls: List<&2, T.Grid(Bool)>
2203  for +c: T.Pos
2204  for cov: {S.covered(ls, c) == True{} : Bool}
2205  for +val: {all_valid(ctx, ls) == True{} : Bool}
2206  Witness(ctx, c)
2207
2208def covered_extract(ctx, ls, c, cov, val):
2209  match ls:
2210    case Nil{}:
2211      Empty.absurd(Witness(ctx, c), P.false_ne_true(cov))
2212    case l <> t:
2213      covered_extract.go(ctx, l, t, c, P.and_true_l(S.check(ctx, l), all_valid(ctx, t), val),
2214        or_cases(B.mine(l, c), S.covered(t, c), cov),
2215        ct => covered_extract(ctx, t, c, ct, P.and_true_r(S.check(ctx, l), all_valid(ctx, t), val)))
2216
2217def loop_found_some(r: Maybe<&2, T.Grid(Bool)>, +c0: T.Pos, k: T.Grid(Bool) -> Maybe<&2, T.Pos>, +c: T.Pos,
2218  e: {S.loop.found(r, c0, k) == Some{c} : Maybe<&2, T.Pos>}) ->
2219  Or({c0 == c : T.Pos} & {r == None{} : Maybe<&2, T.Grid(Bool)>},
2220    Exists(T.Grid(Bool), l => {r == Some{l} : Maybe<&2, T.Grid(Bool)>} & {k(l) == Some{c} : Maybe<&2, T.Pos>})):
2221  match r:
2222    case None{}:
2223      Inl{(PL.some_inj(T.Pos, c0, c, e), {==})}
2224    case Some{l}:
2225      Inr{(l, ({==}, e))}
2226
2227def LoopSome(+hs: List<&2, T.Pos>, +todo: S.Plan, +part: T.Grid(Maybe<&2, Bool>), +ctx: S.Ctx, +c: T.Pos) -> Type:
2228  {B.contains(hs, c) == True{} : Bool} & {S.search(c, todo, part, ctx) == None{} : Maybe<&2, T.Grid(Bool)>}
2229
2230def loop_some.lift(+c0: T.Pos, +t: List<&2, T.Pos>, +todo: S.Plan, +part: T.Grid(Maybe<&2, Bool>),
2231  +ctx: S.Ctx, +c: T.Pos, r: LoopSome(t, todo, part, ctx, c)) -> LoopSome(c0 <> t, todo, part, ctx, c):
2232  match r:
2233    case (m, s):
2234      (or_r(B.same(c0, c), B.contains(t, c), m), s)
2235
2236def loop_some.found(+c0: T.Pos, +t: List<&2, T.Pos>, +found: List<&2, T.Grid(Bool)>, +todo: S.Plan,
2237  +part: T.Grid(Maybe<&2, Bool>), +ctx: S.Ctx, +c: T.Pos,
2238  r: Or({c0 == c : T.Pos} & {S.search(c0, todo, part, ctx) == None{} : Maybe<&2, T.Grid(Bool)>},
2239    Exists(T.Grid(Bool), l => {S.search(c0, todo, part, ctx) == Some{l} : Maybe<&2, T.Grid(Bool)>} &
2240      {S.loop(t, l <> found, todo, part, ctx) == Some{c} : Maybe<&2, T.Pos>})),
2241  ih: @l: T.Grid(Bool) -> {S.loop(t, l <> found, todo, part, ctx) == Some{c} : Maybe<&2, T.Pos>} -> LoopSome(t, todo, part, ctx, c)) ->
2242  LoopSome(c0 <> t, todo, part, ctx, c):
2243  match r:
2244    case Inl{pr}:
2245      match pr:
2246        case (cc, sn):
2247          %cc : {Bool.or(B.same(c0, _), B.contains(t, _)) == True{} : Bool} &
2248            {S.search(_, todo, part, ctx) == None{} : Maybe<&2, T.Grid(Bool)>}
2249          (or_l(B.same(c0, c0), B.contains(t, c0), PG.same_refl(c0)), sn)
2250    case Inr{ex}:
2251      match ex:
2252        case (l, pr):
2253          match pr:
2254            case (sl, lp):
2255              loop_some.lift(c0, t, todo, part, ctx, c, ih(l, lp))
2256
2257def loop_some.cov(+c0: T.Pos, +t: List<&2, T.Pos>, +found: List<&2, T.Grid(Bool)>, +todo: S.Plan,
2258  +part: T.Grid(Maybe<&2, Bool>), +ctx: S.Ctx, +c: T.Pos, +b: Bool,
2259  e: {S.loop.if(b, u => S.loop(t, found, todo, part, ctx),
2260      v => S.loop.found(S.search(c0, todo, part, ctx), c0, l => S.loop(t, l <> found, todo, part, ctx))) == Some{c} : Maybe<&2, T.Pos>},
2261  ihf: {S.loop(t, found, todo, part, ctx) == Some{c} : Maybe<&2, T.Pos>} -> LoopSome(t, todo, part, ctx, c),
2262  ihn: @l: T.Grid(Bool) -> {S.loop(t, l <> found, todo, part, ctx) == Some{c} : Maybe<&2, T.Pos>} -> LoopSome(t, todo, part, ctx, c)) ->
2263  LoopSome(c0 <> t, todo, part, ctx, c):
2264  match b:
2265    case True{}:
2266      loop_some.lift(c0, t, todo, part, ctx, c, ihf(e))
2267    case False{}:
2268      loop_some.found(c0, t, found, todo, part, ctx, c,
2269        loop_found_some(S.search(c0, todo, part, ctx), c0, l => S.loop(t, l <> found, todo, part, ctx), c, e), ihn)
2270
2271# When the loop names c, c is one of its cells and its search found nothing.
2272law loop_some:
2273  for +hs: List<&2, T.Pos>
2274  for +found: List<&2, T.Grid(Bool)>
2275  for +todo: S.Plan
2276  for +part: T.Grid(Maybe<&2, Bool>)
2277  for +ctx: S.Ctx
2278  for +c: T.Pos
2279  for e: {S.loop(hs, found, todo, part, ctx) == Some{c} : Maybe<&2, T.Pos>}
2280  LoopSome(hs, todo, part, ctx, c)
2281
2282def loop_some(hs, found, todo, part, ctx, c, e):
2283  match hs:
2284    case Nil{}:
2285      Empty.absurd(LoopSome(Nil{}, todo, part, ctx, c), PL.none_ne_some(T.Pos, c, e))
2286    case c0 <> t:
2287      loop_some.cov(c0, t, found, todo, part, ctx, c, S.covered(found, c0), e,
2288        ef => loop_some(t, found, todo, part, ctx, c, ef),
2289        l => el => loop_some(t, l <> found, todo, part, ctx, c, el))
2290
2291def loop_found_none(r: Maybe<&2, T.Grid(Bool)>, +c0: T.Pos, k: T.Grid(Bool) -> Maybe<&2, T.Pos>,
2292  e: {S.loop.found(r, c0, k) == None{} : Maybe<&2, T.Pos>}) ->
2293  Exists(T.Grid(Bool), l => {r == Some{l} : Maybe<&2, T.Grid(Bool)>} & {k(l) == None{} : Maybe<&2, T.Pos>}):
2294  match r:
2295    case None{}:
2296      Empty.absurd(Exists(T.Grid(Bool), l => {None{} == Some{l} : Maybe<&2, T.Grid(Bool)>} & {k(l) == None{} : Maybe<&2, T.Pos>}),
2297        some_ne_none(T.Pos, c0, e))
2298    case Some{l}:
2299      (l, ({==}, e))
2300
2301def witness_move(+ctx: S.Ctx, +c0: T.Pos, +c: T.Pos, cq: {B.same(c0, c) == True{} : Bool}, wt: Witness(ctx, c0)) ->
2302  Witness(ctx, c):
2303  %PG.same_sound(c0, c, cq) : Witness(ctx, _)
2304  wt
2305
2306def loop_none.pick(+ctx: S.Ctx, +c0: T.Pos, +t: List<&2, T.Pos>, +c: T.Pos, +l: T.Grid(Bool),
2307  vl: {S.check(ctx, l) == True{} : Bool}, ml: {B.mine(l, c0) == True{} : Bool},
2308  mr: Or({B.same(c0, c) == True{} : Bool}, {B.contains(t, c) == True{} : Bool}),
2309  k: {B.contains(t, c) == True{} : Bool} -> Witness(ctx, c)) -> Witness(ctx, c):
2310  match mr:
2311    case Inl{cq}:
2312      witness_move(ctx, c0, c, cq, (l, (vl, ml)))
2313    case Inr{mt}:
2314      k(mt)
2315
2316def loop_none.found(+c0: T.Pos, +t: List<&2, T.Pos>, +found: List<&2, T.Grid(Bool)>, +todo: S.Plan,
2317  +part: T.Grid(Maybe<&2, Bool>), +w: Nat, +h: Nat, +n: Nat, +rows: T.Grid(T.Seen), +its: List<&2, S.Item>,
2318  +val: {all_valid(S.Ctx{w, h, n, rows, its}, found) == True{} : Bool},
2319  +shP: {B.shaped(Maybe<&2, Bool>, w, h, part) == True{} : Bool}, on0: {B.on_board(w, h, c0) == True{} : Bool},
2320  +c: T.Pos, mr: Or({B.same(c0, c) == True{} : Bool}, {B.contains(t, c) == True{} : Bool}),
2321  ex: Exists(T.Grid(Bool), l => {S.search(c0, todo, part, S.Ctx{w, h, n, rows, its}) == Some{l} : Maybe<&2, T.Grid(Bool)>} &
2322    {S.loop(t, l <> found, todo, part, S.Ctx{w, h, n, rows, its}) == None{} : Maybe<&2, T.Pos>}),
2323  ih: @l: T.Grid(Bool) -> {S.loop(t, l <> found, todo, part, S.Ctx{w, h, n, rows, its}) == None{} : Maybe<&2, T.Pos>} ->
2324    {all_valid(S.Ctx{w, h, n, rows, its}, l <> found) == True{} : Bool} -> {B.contains(t, c) == True{} : Bool} ->
2325    Witness(S.Ctx{w, h, n, rows, its}, c)) ->
2326  Witness(S.Ctx{w, h, n, rows, its}, c):
2327  match ex:
2328    case (+l, pr):
2329      match pr:
2330        case (+sl, ln):
2331          +ctx = {S.Ctx{w, h, n, rows, its} : S.Ctx}
2332          +p1 = B.set_at(Maybe<&2, Bool>, part, c0, Some{True{}})
2333          +vl = dfs2_some_check(S.plan_todo(c0, todo, ctx), p1, S.part_true(p1), S.part_none(p1), ctx, l, sl)
2334          +ml = dfs2_some_keep(S.plan_todo(c0, todo, ctx), p1, S.part_true(p1), S.part_none(p1), ctx, l, sl, c0, True{},
2335            set_look(w, h, part, c0, Some{True{}}, shP, on0))
2336          loop_none.pick(ctx, c0, t, c, l, vl, ml, mr,
2337            mt => ih(l, ln, %Equal.sym(Bool, S.check(ctx, l), True{}, vl) : {Bool.and(_, all_valid(ctx, found)) == True{} : Bool}; val, mt))
2338
2339def loop_none.pick2(+ctx: S.Ctx, +c0: T.Pos, +t: List<&2, T.Pos>, +c: T.Pos, +found: List<&2, T.Grid(Bool)>,
2340  mr: Or({B.same(c0, c) == True{} : Bool}, {B.contains(t, c) == True{} : Bool}),
2341  cov: {S.covered(found, c0) == True{} : Bool}, val: {all_valid(ctx, found) == True{} : Bool},
2342  k: {B.contains(t, c) == True{} : Bool} -> Witness(ctx, c)) -> Witness(ctx, c):
2343  match mr:
2344    case Inl{cq}:
2345      witness_move(ctx, c0, c, cq, covered_extract(ctx, found, c0, cov, val))
2346    case Inr{mt}:
2347      k(mt)
2348
2349def loop_none.cov(+c0: T.Pos, +t: List<&2, T.Pos>, +found: List<&2, T.Grid(Bool)>, +todo: S.Plan,
2350  +part: T.Grid(Maybe<&2, Bool>), +w: Nat, +h: Nat, +n: Nat, +rows: T.Grid(T.Seen), +its: List<&2, S.Item>,
2351  +val: {all_valid(S.Ctx{w, h, n, rows, its}, found) == True{} : Bool},
2352  +shP: {B.shaped(Maybe<&2, Bool>, w, h, part) == True{} : Bool}, on0: {B.on_board(w, h, c0) == True{} : Bool},
2353  +c: T.Pos, mr: Or({B.same(c0, c) == True{} : Bool}, {B.contains(t, c) == True{} : Bool}),
2354  +b: Bool, be: {S.covered(found, c0) == b : Bool},
2355  e: {S.loop.if(b, u => S.loop(t, found, todo, part, S.Ctx{w, h, n, rows, its}),
2356      v => S.loop.found(S.search(c0, todo, part, S.Ctx{w, h, n, rows, its}), c0,
2357        l => S.loop(t, l <> found, todo, part, S.Ctx{w, h, n, rows, its}))) == None{} : Maybe<&2, T.Pos>},
2358  ihf: {S.loop(t, found, todo, part, S.Ctx{w, h, n, rows, its}) == None{} : Maybe<&2, T.Pos>} ->
2359    {B.contains(t, c) == True{} : Bool} -> Witness(S.Ctx{w, h, n, rows, its}, c),
2360  ihn: @l: T.Grid(Bool) -> {S.loop(t, l <> found, todo, part, S.Ctx{w, h, n, rows, its}) == None{} : Maybe<&2, T.Pos>} ->
2361    {all_valid(S.Ctx{w, h, n, rows, its}, l <> found) == True{} : Bool} -> {B.contains(t, c) == True{} : Bool} ->
2362    Witness(S.Ctx{w, h, n, rows, its}, c)) ->
2363  Witness(S.Ctx{w, h, n, rows, its}, c):
2364  match b:
2365    case True{}:
2366      +ctx = {S.Ctx{w, h, n, rows, its} : S.Ctx}
2367      loop_none.pick2(ctx, c0, t, c, found, mr, be, val, mt => ihf(e, mt))
2368    case False{}:
2369      +ctx = {S.Ctx{w, h, n, rows, its} : S.Ctx}
2370      loop_none.found(c0, t, found, todo, part, w, h, n, rows, its, val, shP, on0, c, mr,
2371        loop_found_none(S.search(c0, todo, part, ctx), c0, l => S.loop(t, l <> found, todo, part, ctx), e), ihn)
2372
2373# When the loop names no cell, every one of its cells has a checked layout
2374# that mines it.
2375law loop_none:
2376  for +hs: List<&2, T.Pos>
2377  for +found: List<&2, T.Grid(Bool)>
2378  for +todo: S.Plan
2379  for +part: T.Grid(Maybe<&2, Bool>)
2380  for +w: Nat
2381  for +h: Nat
2382  for +n: Nat
2383  for +rows: T.Grid(T.Seen)
2384  for +its: List<&2, S.Item>
2385  for e: {S.loop(hs, found, todo, part, S.Ctx{w, h, n, rows, its}) == None{} : Maybe<&2, T.Pos>}
2386  for +val: {all_valid(S.Ctx{w, h, n, rows, its}, found) == True{} : Bool}
2387  for +shP: {B.shaped(Maybe<&2, Bool>, w, h, part) == True{} : Bool}
2388  for +hon: {PS.allp(~PS.WH, ~PS.onb, PS.WH{w, h}, hs) == True{} : Bool}
2389  for +c: T.Pos
2390  for m: {B.contains(hs, c) == True{} : Bool}
2391  Witness(S.Ctx{w, h, n, rows, its}, c)
2392
2393def loop_none(hs, found, todo, part, w, h, n, rows, its, e, val, shP, hon, c, m):
2394  match hs:
2395    case Nil{}:
2396      Empty.absurd(Witness(S.Ctx{w, h, n, rows, its}, c), P.false_ne_true(m))
2397    case +c0 <> +t:
2398      +ht = PS.allp_tail(~PS.WH, ~PS.onb, PS.WH{w, h}, c0, t, hon)
2399      loop_none.cov(c0, t, found, todo, part, w, h, n, rows, its, val, shP,
2400        PS.allp_head(~PS.WH, ~PS.onb, PS.WH{w, h}, c0, t, hon), c, or_cases(B.same(c0, c), B.contains(t, c), m),
2401        S.covered(found, c0), {==}, e,
2402        ef => mt => loop_none(t, found, todo, part, w, h, n, rows, its, ef, val, shP, ht, c, mt),
2403        l => el => vl => mt => loop_none(t, l <> found, todo, part, w, h, n, rows, its, el, vl, shP, ht, c, mt))
2404
2405# The solver theorems
2406# ===================
2407
2408law s_hidden_eq:
2409  for +s: T.Seen
2410  {S.is_hidden(s) == L.is_hidden(s) : Bool}
2411
2412def s_hidden_eq(s):
2413  match s:
2414    case T.Hidden{}:
2415      {==}
2416    case T.Shown{k}:
2417      {==}
2418    case T.Boom{}:
2419      {==}
2420
2421# Hidden in LAWS.bend's sense: on the board, and hidden in the rows.
2422law hid_to:
2423  for +w: Nat
2424  for +h: Nat
2425  for +n: Nat
2426  for +rows: T.Grid(T.Seen)
2427  for +p: T.Pos
2428  for +on: {B.on_board(w, h, p) == True{} : Bool}
2429  for +hp: {S.is_hidden(B.at(T.Seen, T.Hidden{}, rows, p)) == True{} : Bool}
2430  {L.hidden(T.Knowledge{w, h, n, rows}, p) == True{} : Bool}
2431
2432def hid_to(w, h, n, rows, p, on, hp):
2433  %Equal.sym(Bool, L.on_board(w, h, p), True{}, %PC.on_board_eq(w, h, p) : {_ == True{} : Bool}; on) :
2434    {Bool.and(_, L.is_hidden(L.at(T.Seen, T.Hidden{}, rows, p))) == True{} : Bool}
2435  %PC.at_eq(T.Seen, T.Hidden{}, rows, p) : {Bool.and(True{}, L.is_hidden(_)) == True{} : Bool}
2436  %s_hidden_eq(B.at(T.Seen, T.Hidden{}, rows, p)) : {Bool.and(True{}, _) == True{} : Bool}
2437  hp
2438
2439law hid_on:
2440  for +w: Nat
2441  for +h: Nat
2442  for +n: Nat
2443  for +rows: T.Grid(T.Seen)
2444  for +p: T.Pos
2445  for hid: {L.hidden(T.Knowledge{w, h, n, rows}, p) == True{} : Bool}
2446  {B.on_board(w, h, p) == True{} : Bool}
2447
2448def hid_on(w, h, n, rows, p, hid):
2449  %Equal.sym(Bool, B.on_board(w, h, p), L.on_board(w, h, p), PC.on_board_eq(w, h, p)) : {_ == True{} : Bool}
2450  P.and_true_l(L.on_board(w, h, p), L.is_hidden(L.at(T.Seen, T.Hidden{}, rows, p)), hid)
2451
2452law hid_hp:
2453  for +w: Nat
2454  for +h: Nat
2455  for +n: Nat
2456  for +rows: T.Grid(T.Seen)
2457  for +p: T.Pos
2458  for hid: {L.hidden(T.Knowledge{w, h, n, rows}, p) == True{} : Bool}
2459  {S.is_hidden(B.at(T.Seen, T.Hidden{}, rows, p)) == True{} : Bool}
2460
2461def hid_hp(w, h, n, rows, p, hid):
2462  %Equal.sym(Bool, S.is_hidden(B.at(T.Seen, T.Hidden{}, rows, p)), L.is_hidden(B.at(T.Seen, T.Hidden{}, rows, p)),
2463    s_hidden_eq(B.at(T.Seen, T.Hidden{}, rows, p))) : {_ == True{} : Bool}
2464  %Equal.sym(T.Seen, B.at(T.Seen, T.Hidden{}, rows, p), L.at(T.Seen, T.Hidden{}, rows, p), PC.at_eq(T.Seen, T.Hidden{}, rows, p)) :
2465    {L.is_hidden(_) == True{} : Bool}
2466  P.and_true_r(L.on_board(w, h, p), L.is_hidden(L.at(T.Seen, T.Hidden{}, rows, p)), hid)
2467
2468def hc_on.cell(+rows: T.Grid(T.Seen), +w: Nat, +h: Nat, +p: T.Pos, +t: List<&2, T.Pos>, +b: Bool,
2469  on: {B.on_board(w, h, p) == True{} : Bool},
2470  ih: {PS.allp(~PS.WH, ~PS.onb, PS.WH{w, h}, S.hidden_cells(rows, t)) == True{} : Bool}) ->
2471  {PS.allp(~PS.WH, ~PS.onb, PS.WH{w, h}, List.filter.put(T.Pos, p, S.hidden_cells(rows, t), b)) == True{} : Bool}:
2472  match b:
2473    case False{}:
2474      ih
2475    case True{}:
2476      %Equal.sym(Bool, B.on_board(w, h, p), True{}, on) :
2477        {Bool.and(_, PS.allp(~PS.WH, ~PS.onb, PS.WH{w, h}, S.hidden_cells(rows, t))) == True{} : Bool}
2478      ih
2479
2480law hc_on:
2481  for +rows: T.Grid(T.Seen)
2482  for +w: Nat
2483  for +h: Nat
2484  for +ps: List<&2, T.Pos>
2485  for +ons: {PS.allp(~PS.WH, ~PS.onb, PS.WH{w, h}, ps) == True{} : Bool}
2486  {PS.allp(~PS.WH, ~PS.onb, PS.WH{w, h}, S.hidden_cells(rows, ps)) == True{} : Bool}
2487
2488def hc_on(rows, w, h, ps, ons):
2489  match ps:
2490    case Nil{}:
2491      {==}
2492    case +p <> +t:
2493      hc_on.cell(rows, w, h, p, t, S.is_hidden(B.at(T.Seen, T.Hidden{}, rows, p)),
2494        PS.allp_head(~PS.WH, ~PS.onb, PS.WH{w, h}, p, t, ons),
2495        hc_on(rows, w, h, t, PS.allp_tail(~PS.WH, ~PS.onb, PS.WH{w, h}, p, t, ons)))
2496
2497law head_some:
2498  for +hs: List<&2, T.Pos>
2499  for +c: T.Pos
2500  for e: {List.head(&2, T.Pos, hs) == Some{c} : Maybe<&2, T.Pos>}
2501  {B.contains(hs, c) == True{} : Bool}
2502
2503def head_some(hs, c, e):
2504  match hs:
2505    case Nil{}:
2506      Empty.absurd({False{} == True{} : Bool}, PL.none_ne_some(T.Pos, c, e))
2507    case x <> t:
2508      %PL.some_inj(T.Pos, x, c, e) : {Bool.or(B.same(x, _), B.contains(t, _)) == True{} : Bool}
2509      or_l(B.same(x, x), B.contains(t, x), PG.same_refl(x))
2510
2511law head_none:
2512  for +hs: List<&2, T.Pos>
2513  for +p: T.Pos
2514  for e: {List.head(&2, T.Pos, hs) == None{} : Maybe<&2, T.Pos>}
2515  for m: {B.contains(hs, p) == True{} : Bool}
2516  Empty
2517
2518def head_none(hs, p, e, m):
2519  match hs:
2520    case Nil{}:
2521      P.false_ne_true(m)
2522    case x <> t:
2523      some_ne_none(T.Pos, x, e)
2524
2525def solver_tok(+w: Nat, +h: Nat, +n: Nat, +rows: T.Grid(T.Seen), +layout: T.Grid(Bool),
2526  chk: {S.check(S.Ctx{w, h, n, rows, S.items(w, h, rows, B.cells(w, h))}, layout) == True{} : Bool}) ->
2527  {todos_ok(S.order(S.todos(S.items(w, h, rows, B.cells(w, h)), S.hidden_cells(rows, B.cells(w, h)))), layout) == True{} : Bool}:
2528  +its = S.items(w, h, rows, B.cells(w, h))
2529  +t0 = S.todos(its, S.hidden_cells(rows, B.cells(w, h)))
2530  +a = 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))
2531  +iok = P.and_true_r(a, S.items_ok(its, layout), chk)
2532  +ta = todos_ok_all(its, S.hidden_cells(rows, B.cells(w, h)), layout, iok)
2533  tok_append(S.nears(t0), S.fars(t0), layout, tok_order(t0, layout, ta), tok_order_f(t0, layout, ta))
2534
2535def solver_ton(+w: Nat, +h: Nat, +rows: T.Grid(T.Seen)) ->
2536  {todos_onb(PS.WH{w, h}, S.order(S.todos(S.items(w, h, rows, B.cells(w, h)), S.hidden_cells(rows, B.cells(w, h))))) == True{} : Bool}:
2537  +its = S.items(w, h, rows, B.cells(w, h))
2538  +t0 = S.todos(its, S.hidden_cells(rows, B.cells(w, h)))
2539  +ta = todos_onb_all(PS.WH{w, h}, its, S.hidden_cells(rows, B.cells(w, h)), items_onb_all(w, h, rows, B.cells(w, h), PS.cells_on(w, h)))
2540  ton_append(PS.WH{w, h}, S.nears(t0), S.fars(t0), ton_order(PS.WH{w, h}, t0, ta), ton_order_f(PS.WH{w, h}, t0, ta))
2541
2542# The order of a search
2543# ======================
2544# Each search walks the cells in a heuristic order, then in the plain one;
2545# whatever the heuristic, every cell is still in the walk, and every todo in
2546# it is one of the solve's own.
2547
2548def tok_f(l: T.Grid(Bool), t: S.Todo) -> Bool:
2549  match t:
2550    case S.Todo{c, rel}:
2551      S.items_ok(rel, l)
2552
2553def ton_f(e: PS.WH, t: S.Todo) -> Bool:
2554  match t:
2555    case S.Todo{c, rel}:
2556      items_onb(e, rel)
2557
2558law tok_tall:
2559  for +ts: List<&2, S.Todo>
2560  for +layout: T.Grid(Bool)
2561  {todos_ok(ts, layout) == PF.tall(~T.Grid(Bool), ~tok_f, layout, ts) : Bool}
2562
2563def tok_tall(ts, layout):
2564  match ts:
2565    case Nil{}:
2566      {==}
2567    case S.Todo{c, rel} <> t:
2568      %tok_tall(t, layout) : {Bool.and(S.items_ok(rel, layout), todos_ok(t, layout))
2569        == Bool.and(S.items_ok(rel, layout), _) : Bool}
2570      {==}
2571
2572law ton_tall:
2573  for +e: PS.WH
2574  for +ts: List<&2, S.Todo>
2575  {todos_onb(e, ts) == PF.tall(~PS.WH, ~ton_f, e, ts) : Bool}
2576
2577def ton_tall(e, ts):
2578  match ts:
2579    case Nil{}:
2580      {==}
2581    case S.Todo{c, rel} <> t:
2582      %ton_tall(e, t) : {Bool.and(items_onb(e, rel), todos_onb(e, t)) == Bool.and(items_onb(e, rel), _) : Bool}
2583      {==}
2584
2585law tcontains_pre:
2586  for +pre: List<&2, S.Todo>
2587  for +base: List<&2, S.Todo>
2588  for +q: T.Pos
2589  for e: {tcontains(base, q) == True{} : Bool}
2590  {tcontains(List.append(&2, S.Todo, pre, base), q) == True{} : Bool}
2591
2592def tcontains_pre(pre, base, q, e):
2593  match pre:
2594    case Nil{}:
2595      e
2596    case S.Todo{c, rel} <> t:
2597      %Equal.sym(Bool, tcontains(List.append(&2, S.Todo, t, base), q), True{}, tcontains_pre(t, base, q, e)) :
2598        {Bool.or(B.same(c, q), _) == True{} : Bool}
2599      PS.or_true_r(B.same(c, q))
2600
2601def or_mono(+a: Bool, +b: Bool, +b2: Bool, k: {b == True{} : Bool} -> {b2 == True{} : Bool},
2602  e: {Bool.or(a, b) == True{} : Bool}) -> {Bool.or(a, b2) == True{} : Bool}:
2603  match a:
2604    case True{}:
2605      {==}
2606    case False{}:
2607      k(e)
2608
2609# Cells still to do stay to do with more todos in front.
2610law covers_pre:
2611  for +pre: List<&2, S.Todo>
2612  for +base: List<&2, S.Todo>
2613  for +part: T.Grid(Maybe<&2, Bool>)
2614  for +ps: List<&2, T.Pos>
2615  for +cv: {PS.allp(~CV, ~cv_f, CV{base, part}, ps) == True{} : Bool}
2616  {PS.allp(~CV, ~cv_f, CV{List.append(&2, S.Todo, pre, base), part}, ps) == True{} : Bool}
2617
2618def covers_pre(pre, base, part, ps, cv):
2619  match ps:
2620    case Nil{}:
2621      {==}
2622    case +q <> +t:
2623      +a = Bool.not(S.is_none(S.look(part, q)))
2624      +app = List.append(&2, S.Todo, pre, base)
2625      +hd = or_mono(a, tcontains(base, q), tcontains(app, q), m => tcontains_pre(pre, base, q, m),
2626        PS.allp_head(~CV, ~cv_f, CV{base, part}, q, t, cv))
2627      %Equal.sym(Bool, PS.allp(~CV, ~cv_f, CV{app, part}, t), True{},
2628        covers_pre(pre, base, part, t, PS.allp_tail(~CV, ~cv_f, CV{base, part}, q, t, cv))) :
2629        {Bool.and(cv_f(CV{app, part}, q), _) == True{} : Bool}
2630      %Equal.sym(Bool, cv_f(CV{app, part}, q), True{}, hd) : {Bool.and(_, True{}) == True{} : Bool}
2631      {==}
2632
2633# The heuristic order of the search for c, as the plan builds it.
2634def plan_qs(+c: T.Pos, +w: Nat, +h: Nat, +ts: List<&2, S.Todo>) -> List<&2, T.Pos>:
2635  +near = S.nears(ts)
2636  +fuel = Nat.add(List.length(&2, S.Todo, near), 1n)
2637  +relg = S.rel_grid(w, h, near)
2638  List.append(&2, T.Pos, S.linked(c, w, h, fuel, relg), S.groups(w, h, near, fuel, relg))
2639
2640def plan_k(+c: T.Pos, +w: Nat, +n: Nat, +ts: List<&2, S.Todo>) -> Nat:
2641  S.spin(c, w, n, List.length(&2, S.Todo, S.fars(ts)))
2642
2643def plan_list(+c: T.Pos, +w: Nat, +h: Nat, +n: Nat, +ts: List<&2, S.Todo>) -> List<&2, S.Todo>:
2644  List.append(&2, S.Todo, S.gather(plan_qs(c, w, h, ts), S.nears(ts)),
2645    List.append(&2, S.Todo, S.rot(S.fars(ts), plan_k(c, w, n, ts)), S.order(ts)))
2646
2647law plan_shape:
2648  for +c: T.Pos
2649  for +w: Nat
2650  for +h: Nat
2651  for +n: Nat
2652  for +rows: T.Grid(T.Seen)
2653  for +its: List<&2, S.Item>
2654  for +ts: List<&2, S.Todo>
2655  {S.plan_todo(c, S.plan(w, h, ts), S.Ctx{w, h, n, rows, its}) == plan_list(c, w, h, n, ts) : List<&2, S.Todo>}
2656
2657def plan_shape(c, w, h, n, rows, its, ts):
2658  {==}
2659
2660# A failed search for c rules out every consistent layout mining c.
2661law search_none:
2662  for +w: Nat
2663  for +h: Nat
2664  for +n: Nat
2665  for +rows: T.Grid(T.Seen)
2666  for +okt: {B.shaped(T.Seen, w, h, rows) == True{} : Bool}
2667  for +c: T.Pos
2668  for +onc: {B.on_board(w, h, c) == True{} : Bool}
2669  for +layout: T.Grid(Bool)
2670  for +cons: {L.consistent(T.Knowledge{w, h, n, rows}, layout) == True{} : Bool}
2671  for +mc: {B.mine(layout, c) == True{} : Bool}
2672  for sn: {S.search(c, S.plan(w, h, S.todos(S.items(w, h, rows, B.cells(w, h)), S.hidden_cells(rows, B.cells(w, h)))),
2673    S.start(rows), S.Ctx{w, h, n, rows, S.items(w, h, rows, B.cells(w, h))}) == None{} : Maybe<&2, T.Grid(Bool)>}
2674  Empty
2675
2676def search_none(w, h, n, rows, okt, c, onc, layout, cons, mc, sn):
2677  +its = S.items(w, h, rows, B.cells(w, h))
2678  +hs = S.hidden_cells(rows, B.cells(w, h))
2679  +t0 = S.todos(its, hs)
2680  +ctx = {S.Ctx{w, h, n, rows, its} : S.Ctx}
2681  +shS = Equal.trans(Bool, B.shaped(Maybe<&2, Bool>, w, h, S.start(rows)), B.shaped(T.Seen, w, h, rows), True{},
2682    start_shaped(w, h, rows), okt)
2683  +chk = Equal.trans(Bool, S.check(S.Ctx{w, h, n, rows, its}, layout), L.consistent(T.Knowledge{w, h, n, rows}, layout), True{},
2684    check_cons(w, h, n, rows, layout), cons)
2685  +shL = {%Equal.sym(Bool, B.shaped(Bool, w, h, layout), L.shaped(Bool, w, h, layout), PC.shaped_eq(Bool, w, h, layout)) :
2686      {_ == True{} : Bool};
2687    PW.and4_a(L.shaped(Bool, w, h, layout), L.shaped(T.Seen, w, h, rows), Nat.is_eq(L.total_mines(layout), n),
2688      L.agrees_all(w, h, rows, layout, L.cells(w, h)), cons) : {B.shaped(Bool, w, h, layout) == True{} : Bool}}
2689  +p = B.set_at(Maybe<&2, Bool>, S.start(rows), c, Some{True{}})
2690  +shp = PL.shaped_set(Maybe<&2, Bool>, w, h, S.start(rows), c, Some{True{}}, shS)
2691  +qs = plan_qs(c, w, h, t0)
2692  +k = plan_k(c, w, n, t0)
2693  +todo = plan_list(c, w, h, n, t0)
2694  +con = PF.tall_plan(~PS.WH, ~PF.con_f, PS.WH{w, h}, t0, qs, k,
2695    PF.con_todos(w, h, its, hs, hc_on(rows, w, h, B.cells(w, h), PS.cells_on(w, h))))
2696  +eq = PF.dfs2_eq(todo, p, w, h, n, rows, its, S.part_true(p), S.part_none(p), shp, con, {==}, {==})
2697  +sn1 = {%Equal.sym(List<&2, S.Todo>, S.plan_todo(c, S.plan(w, h, t0), ctx), todo, plan_shape(c, w, h, n, rows, its, t0)) :
2698      {S.dfs2(_, p, S.part_true(p), S.part_none(p), ctx) == None{} : Maybe<&2, T.Grid(Bool)>};
2699    sn : {S.dfs2(todo, p, S.part_true(p), S.part_none(p), ctx) == None{} : Maybe<&2, T.Grid(Bool)>}}
2700  +sn2 = Equal.trans(Maybe<&2, T.Grid(Bool)>, S.dfs(todo, p, ctx), S.dfs2(todo, p, S.part_true(p), S.part_none(p), ctx), None{},
2701    Equal.sym(Maybe<&2, T.Grid(Bool)>, S.dfs2(todo, p, S.part_true(p), S.part_none(p), ctx), S.dfs(todo, p, ctx), eq), sn1)
2702  +rest = List.append(&2, S.Todo, S.rot(S.fars(t0), k), S.order(t0))
2703  +cov = covers_pre(S.gather(qs, S.nears(t0)), rest, p, B.cells(w, h),
2704    covers_pre(S.rot(S.fars(t0), k), S.order(t0), p, B.cells(w, h),
2705      start_cover.go(w, h, rows, its, c, shS, B.cells(w, h), PS.cells_on(w, h))))
2706  +a = 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))
2707  +ta = todos_ok_all(its, hs, layout, P.and_true_r(a, S.items_ok(its, layout), chk))
2708  +tok = {%Equal.sym(Bool, todos_ok(todo, layout), PF.tall(~T.Grid(Bool), ~tok_f, layout, todo), tok_tall(todo, layout)) :
2709      {_ == True{} : Bool};
2710    PF.tall_plan(~T.Grid(Bool), ~tok_f, layout, t0, qs, k,
2711      Equal.trans(Bool, PF.tall(~T.Grid(Bool), ~tok_f, layout, t0), todos_ok(t0, layout), True{},
2712        Equal.sym(Bool, todos_ok(t0, layout), PF.tall(~T.Grid(Bool), ~tok_f, layout, t0), tok_tall(t0, layout)), ta)) :
2713      {todos_ok(todo, layout) == True{} : Bool}}
2714  +e = {PS.WH{w, h} : PS.WH}
2715  +tn = todos_onb_all(e, its, hs, items_onb_all(w, h, rows, B.cells(w, h), PS.cells_on(w, h)))
2716  +ton = {%Equal.sym(Bool, todos_onb(e, todo), PF.tall(~PS.WH, ~ton_f, e, todo), ton_tall(e, todo)) :
2717      {_ == True{} : Bool};
2718    PF.tall_plan(~PS.WH, ~ton_f, e, t0, qs, k,
2719      Equal.trans(Bool, PF.tall(~PS.WH, ~ton_f, e, t0), todos_onb(e, t0), True{},
2720        Equal.sym(Bool, todos_onb(e, t0), PF.tall(~PS.WH, ~ton_f, e, t0), ton_tall(e, t0)), tn)) :
2721      {todos_onb(e, todo) == True{} : Bool}}
2722  dfs_none(todo, p, w, h, n, rows, its, layout, sn2, shp, shL, cov,
2723    comp_set(w, h, c, S.start(rows), layout, True{}, shS, mc, B.cells(w, h), PS.cells_on(w, h),
2724      start_comp(w, h, n, rows, layout, cons)),
2725    chk, tok, ton, items_onb_all(w, h, rows, B.cells(w, h), PS.cells_on(w, h)))
2726
2727def safe_fn(+w: Nat, +h: Nat, +n: Nat, +rows: T.Grid(T.Seen), +okt: {B.shaped(T.Seen, w, h, rows) == True{} : Bool},
2728  +c: T.Pos, +onc: {B.on_board(w, h, c) == True{} : Bool},
2729  +sn: {S.search(c, S.plan(w, h, S.todos(S.items(w, h, rows, B.cells(w, h)), S.hidden_cells(rows, B.cells(w, h)))),
2730    S.start(rows), S.Ctx{w, h, n, rows, S.items(w, h, rows, B.cells(w, h))}) == None{} : Maybe<&2, T.Grid(Bool)>},
2731  +layout: T.Grid(Bool), +cons: {L.consistent(T.Knowledge{w, h, n, rows}, layout) == True{} : Bool},
2732  +b: Bool, be: {B.mine(layout, c) == b : Bool}) -> {L.mine(layout, c) == False{} : Bool}:
2733  match b:
2734    case False{}:
2735      %PC.mine_eq(layout, c) : {_ == False{} : Bool}
2736      be
2737    case True{}:
2738      Empty.absurd({L.mine(layout, c) == False{} : Bool}, search_none(w, h, n, rows, okt, c, onc, layout, cons, be, sn))
2739
2740def PF_both(+a: Bool, e1: {a == False{} : Bool}, e2: {a == True{} : Bool}, -A: Type) -> A:
2741  Empty.absurd(A, P.false_ne_true(Equal.trans(Bool, False{}, a, True{}, Equal.sym(Bool, a, False{}, e1), e2)))
2742
2743def safe_none(+w: Nat, +h: Nat, +n: Nat, +rows: T.Grid(T.Seen), okf: {B.shaped(T.Seen, w, h, rows) == False{} : Bool},
2744  +c: T.Pos, +layout: T.Grid(Bool), cons: {L.consistent(T.Knowledge{w, h, n, rows}, layout) == True{} : Bool}) ->
2745  {L.mine(layout, c) == False{} : Bool}:
2746  PF_both(B.shaped(T.Seen, w, h, rows), okf,
2747    %Equal.sym(Bool, B.shaped(T.Seen, w, h, rows), L.shaped(T.Seen, w, h, rows), PC.shaped_eq(T.Seen, w, h, rows)) :
2748      {_ == True{} : Bool};
2749    PW.and4_b(L.shaped(Bool, w, h, layout), L.shaped(T.Seen, w, h, rows), Nat.is_eq(L.total_mines(layout), n),
2750      L.agrees_all(w, h, rows, layout, L.cells(w, h)), cons), {L.mine(layout, c) == False{} : Bool})
2751
2752def safe_hidden(+w: Nat, +h: Nat, +n: Nat, +rows: T.Grid(T.Seen), +c: T.Pos,
2753  hc: {S.is_hidden(B.at(T.Seen, T.Hidden{}, rows, c)) == True{} : Bool} & {B.contains(B.cells(w, h), c) == True{} : Bool},
2754  fn: @layout: T.Grid(Bool) -> {L.consistent(T.Knowledge{w, h, n, rows}, layout) == True{} : Bool} -> {L.mine(layout, c) == False{} : Bool}) ->
2755  L.ProvablySafe(T.Knowledge{w, h, n, rows}, c):
2756  match hc:
2757    case (hp, mc):
2758      (hid_to(w, h, n, rows, c, PS.allp_member(~PS.WH, ~PS.onb, PS.WH{w, h}, B.cells(w, h), c, PS.cells_on(w, h), mc), hp), fn)
2759
2760def safe_hidden.k(+w: Nat, +h: Nat, +n: Nat, +rows: T.Grid(T.Seen), +c: T.Pos,
2761  hc: {S.is_hidden(B.at(T.Seen, T.Hidden{}, rows, c)) == True{} : Bool} & {B.contains(B.cells(w, h), c) == True{} : Bool},
2762  fn: {B.on_board(w, h, c) == True{} : Bool} ->
2763    @layout: T.Grid(Bool) -> {L.consistent(T.Knowledge{w, h, n, rows}, layout) == True{} : Bool} -> {L.mine(layout, c) == False{} : Bool}) ->
2764  L.ProvablySafe(T.Knowledge{w, h, n, rows}, c):
2765  match hc:
2766    case (hp, mc):
2767      +onc = PS.allp_member(~PS.WH, ~PS.onb, PS.WH{w, h}, B.cells(w, h), c, PS.cells_on(w, h), mc)
2768      (hid_to(w, h, n, rows, c, onc, hp), fn(onc))
2769
2770def solve_safe.k(+w: Nat, +h: Nat, +n: Nat, +rows: T.Grid(T.Seen), +c: T.Pos,
2771  +okt: {B.shaped(T.Seen, w, h, rows) == True{} : Bool},
2772  ls: LoopSome(S.hidden_cells(rows, B.cells(w, h)), S.plan(w, h, S.todos(S.items(w, h, rows, B.cells(w, h)), S.hidden_cells(rows, B.cells(w, h)))),
2773    S.start(rows), S.Ctx{w, h, n, rows, S.items(w, h, rows, B.cells(w, h))}, c)) ->
2774  L.ProvablySafe(T.Knowledge{w, h, n, rows}, c):
2775  match ls:
2776    case (m, sn):
2777      hc = hc_sound(rows, B.cells(w, h), c, m)
2778      safe_hidden.k(w, h, n, rows, c, hc, onc => +layout => cons => safe_fn(w, h, n, rows, okt, c, onc, sn, layout, cons, B.mine(layout, c), {==}))
2779
2780def solve_safe.go(+w: Nat, +h: Nat, +n: Nat, +rows: T.Grid(T.Seen), +c: T.Pos, +ok: Bool,
2781  oke: {B.shaped(T.Seen, w, h, rows) == ok : Bool},
2782  e: {S.solve.go(ok, S.hidden_cells(rows, B.cells(w, h)), w, h, n, rows) == Some{c} : Maybe<&2, T.Pos>}) ->
2783  L.ProvablySafe(T.Knowledge{w, h, n, rows}, c):
2784  match ok:
2785    case False{}:
2786      +hs = S.hidden_cells(rows, B.cells(w, h))
2787      safe_hidden(w, h, n, rows, c, hc_sound(rows, B.cells(w, h), c, head_some(hs, c, e)),
2788        layout => cons => safe_none(w, h, n, rows, oke, c, layout, cons))
2789    case True{}:
2790      +hs = S.hidden_cells(rows, B.cells(w, h))
2791      +its = S.items(w, h, rows, B.cells(w, h))
2792      ls = loop_some(hs, Nil{}, S.plan(w, h, S.todos(its, hs)), S.start(rows), S.Ctx{w, h, n, rows, its}, c, e)
2793      solve_safe.k(w, h, n, rows, c, oke, ls)
2794
2795# Witness soundness: a cell the solver names is provably safe.
2796law solve_safe:
2797  for +k: T.Knowledge
2798  for +c: T.Pos
2799  for e: {S.solve(k) == Some{c} : Maybe<&2, T.Pos>}
2800  L.ProvablySafe(k, c)
2801
2802def solve_safe(k, c, e):
2803  match k:
2804    case T.Knowledge{w, h, n, rows}:
2805      solve_safe.go(w, h, n, rows, c, B.shaped(T.Seen, w, h, rows), {==}, e)
2806
2807def stuck_wit(+w: Nat, +h: Nat, +n: Nat, +rows: T.Grid(T.Seen), +p: T.Pos,
2808  H: @layout: T.Grid(Bool) -> {L.consistent(T.Knowledge{w, h, n, rows}, layout) == True{} : Bool} -> {L.mine(layout, p) == False{} : Bool},
2809  wt: Witness(S.Ctx{w, h, n, rows, S.items(w, h, rows, B.cells(w, h))}, p)) -> Empty:
2810  match wt:
2811    case (+l, pr):
2812      match pr:
2813        case (chk, ml):
2814          PF_both(L.mine(l, p),
2815            H(l, Equal.trans(Bool, L.consistent(T.Knowledge{w, h, n, rows}, l),
2816              S.check(S.Ctx{w, h, n, rows, S.items(w, h, rows, B.cells(w, h))}, l), True{},
2817              Equal.sym(Bool, S.check(S.Ctx{w, h, n, rows, S.items(w, h, rows, B.cells(w, h))}, l),
2818                L.consistent(T.Knowledge{w, h, n, rows}, l), check_cons(w, h, n, rows, l)), chk)),
2819            %PC.mine_eq(l, p) : {_ == True{} : Bool}; ml, Empty)
2820
2821def solve_stuck.go(+w: Nat, +h: Nat, +n: Nat, +rows: T.Grid(T.Seen), +ok: Bool,
2822  oke: {B.shaped(T.Seen, w, h, rows) == ok : Bool},
2823  e: {S.solve.go(ok, S.hidden_cells(rows, B.cells(w, h)), w, h, n, rows) == None{} : Maybe<&2, T.Pos>},
2824  +p: T.Pos, ps: L.ProvablySafe(T.Knowledge{w, h, n, rows}, p)) -> Empty:
2825  match ok:
2826    case False{}:
2827      match ps:
2828        case (+hid, H):
2829          head_none(S.hidden_cells(rows, B.cells(w, h)), p, e,
2830            hc_member(rows, B.cells(w, h), p, PS.cells_member(w, h, p, hid_on(w, h, n, rows, p, hid)), hid_hp(w, h, n, rows, p, hid)))
2831    case True{}:
2832      match ps:
2833        case (+hid, H):
2834          +hs = S.hidden_cells(rows, B.cells(w, h))
2835          +its = S.items(w, h, rows, B.cells(w, h))
2836          +shS = Equal.trans(Bool, B.shaped(Maybe<&2, Bool>, w, h, S.start(rows)), B.shaped(T.Seen, w, h, rows), True{},
2837            start_shaped(w, h, rows), oke)
2838          +mp = hc_member(rows, B.cells(w, h), p, PS.cells_member(w, h, p, hid_on(w, h, n, rows, p, hid)), hid_hp(w, h, n, rows, p, hid))
2839          stuck_wit(w, h, n, rows, p, H,
2840            loop_none(hs, Nil{}, S.plan(w, h, S.todos(its, hs)), S.start(rows), w, h, n, rows, its, e, {==}, shS,
2841              hc_on(rows, w, h, B.cells(w, h), PS.cells_on(w, h)), p, mp))
2842
2843def solve_stuck.k(+k: T.Knowledge, e: {S.solve(k) == None{} : Maybe<&2, T.Pos>}, +p: T.Pos, ps: L.ProvablySafe(k, p)) -> Empty:
2844  match k:
2845    case T.Knowledge{w, h, n, rows}:
2846      solve_stuck.go(w, h, n, rows, B.shaped(T.Seen, w, h, rows), {==}, e, p, ps)
2847
2848# Stuck soundness: when the solver names no cell, no cell is provably safe.
2849law solve_stuck:
2850  for +k: T.Knowledge
2851  for e: {S.solve(k) == None{} : Maybe<&2, T.Pos>}
2852  L.Stuck(k)
2853
2854def solve_stuck(k, e):
2855  p => ps => solve_stuck.k(k, e, p, ps)