1	import Base
2	import ./types.bend as T
3	import ./board.bend as B
4	import ./game.bend as G
5	import ./LAWS.bend as L
6	import ./proof_base.bend as P
7	import ./proof_grid.bend as PG
8	
9	# Lemmas about board generation.
10	
11	# Shape
12	# =====
13	
14	law gen_row_len:
15	  for +z: G.Zone
16	  for +y: Nat
17	  for +xs: List<&2, Nat>
18	  for +st: G.GenState
19	  {List.length(&2, Bool, G.gen.row(z, y, xs, st)) == List.length(&2, Nat, xs) : Nat}
20	
21	def gen_row_len(z, y, xs, st):
22	  match xs:
23	    case Nil{}:
24	      {==}
25	    case x <> t:
26	      %gen_row_len(z, y, t, G.gen.next(z, T.Pos{x, y}, st)) :
27	        {1n+List.length(&2, Bool, G.gen.row(z, y, t, G.gen.next(z, T.Pos{x, y}, st)))
28	          == 1n+_ : Nat}
29	      {==}
30	
31	law gen_rows_len:
32	  for +z: G.Zone
33	  for +w: Nat
34	  for +ys: List<&2, Nat>
35	  for +st: G.GenState
36	  {List.length(&2, List<&2, Bool>, G.gen.rows(z, w, ys, st)) == List.length(&2, Nat, ys) : Nat}
37	
38	def gen_rows_len(z, w, ys, st):
39	  match ys:
40	    case Nil{}:
41	      {==}
42	    case y <> t:
43	      +st2 = G.gen.row_state(z, y, List.range(w), st)
44	      %gen_rows_len(z, w, t, st2) :
45	        {1n+List.length(&2, List<&2, Bool>, G.gen.rows(z, w, t, st2)) == 1n+_ : Nat}
46	      {==}
47	
48	law gen_rows_wide:
49	  for +z: G.Zone
50	  for +w: Nat
51	  for +ys: List<&2, Nat>
52	  for +st: G.GenState
53	  {L.rows_wide(Bool, w, G.gen.rows(z, w, ys, st)) == True{} : Bool}
54	
55	def gen_rows_wide(z, w, ys, st):
56	  match ys:
57	    case Nil{}:
58	      {==}
59	    case y <> t:
60	      +row = G.gen.row(z, y, List.range(w), st)
61	      +st2 = G.gen.row_state(z, y, List.range(w), st)
62	      +len = Equal.trans(Nat, List.length(&2, Bool, row), List.length(&2, Nat, List.range(w)), w,
63	        gen_row_len(z, y, List.range(w), st), P.range_length(w))
64	      %Equal.sym(Nat, List.length(&2, Bool, row), w, len) :
65	        {Bool.and(Nat.is_eq(_, w), L.rows_wide(Bool, w, G.gen.rows(z, w, t, st2))) == True{} : Bool}
66	      %Equal.sym(Bool, Nat.is_eq(w, w), True{}, P.eq_refl(w)) :
67	        {Bool.and(_, L.rows_wide(Bool, w, G.gen.rows(z, w, t, st2))) == True{} : Bool}
68	      gen_rows_wide(z, w, t, st2)
69	
70	# The zone a board of n mines keeps free around the first click.
71	def zone(+w: Nat, +h: Nat, +n: Nat, +first: T.Pos) -> G.Zone:
72	  G.Zone{first, Nat.is_le(Nat.add(n, 9n), Nat.mul(w, h))}
73	
74	law gen_shape_:
75	  for +w: Nat
76	  for +h: Nat
77	  for +n: Nat
78	  for +first: T.Pos
79	  for +rs: List<&2, U32>
80	  {L.shaped(Bool, w, h, G.place_mines(w, h, n, first, rs)) == True{} : Bool}
81	
82	def gen_shape_(w, h, n, first, rs):
83	  +z = zone(w, h, n, first)
84	  +st = {G.GenState{n, G.gen.left(z, B.cells(w, h)), rs} : G.GenState}
85	  +g = G.gen.rows(z, w, List.range(h), st)
86	  +len = Equal.trans(Nat, List.length(&2, List<&2, Bool>, g), List.length(&2, Nat, List.range(h)), h,
87	    gen_rows_len(z, w, List.range(h), st), P.range_length(h))
88	  %Equal.sym(Nat, List.length(&2, List<&2, Bool>, g), h, len) :
89	    {Bool.and(Nat.is_eq(_, h), L.rows_wide(Bool, w, g)) == True{} : Bool}
90	  %Equal.sym(Bool, Nat.is_eq(h, h), True{}, P.eq_refl(h)) :
91	    {Bool.and(_, L.rows_wide(Bool, w, g)) == True{} : Bool}
92	  gen_rows_wide(z, w, List.range(h), st)
93	
94	# The first click
95	# ===============
96	
97	def gen_bit_first(+z: G.Zone, +p: T.Pos, +st: G.GenState,
98	  s: {G.gen.out(z, p) == True{} : Bool}) -> {G.gen.bit(z, p, st) == False{} : Bool}:
99	  match st:
100	    case G.GenState{need, left, rs}:
101	      %Equal.sym(Bool, G.gen.out(z, p), True{}, s) :
102	        {Bool.and(Bool.and(Bool.not(_), Nat.is_lt(0n, need)), G.gen.pick(need, left, rs))
103	          == False{} : Bool}
104	      {==}
105	
106	# A cell of a generated row that is in the zone has no mine.
107	law gen_row_first:
108	  for +z: G.Zone
109	  for +y: Nat
110	  for +xs: List<&2, Nat>
111	  for +j: Nat
112	  for +x: Nat
113	  for +st: G.GenState
114	  for e: {List.get(&2, Nat, xs, j) == Some{x} : Maybe<&2, Nat>}
115	  for +s: {G.gen.out(z, T.Pos{x, y}) == True{} : Bool}
116	  {List.get(&2, Bool, G.gen.row(z, y, xs, st), j) == Some{False{}} : Maybe<&2, Bool>}
117	
118	def gen_row_first(z, y, xs, j, x, st, e, s):
119	  match xs j:
120	    case Nil{} _:
121	      Empty.absurd({List.get(&2, Bool, G.gen.row(z, y, Nil{}, st), j) == Some{False{}}
122	        : Maybe<&2, Bool>}, PG.know_row_get.none(Nat, x, e))
123	    case a <> t 0n:
124	      %Equal.sym(Nat, a, x, PG.know_row_get.some(Nat, a, x, e)) :
125	        {Some{G.gen.bit(z, T.Pos{_, y}, st)} == Some{False{}} : Maybe<&2, Bool>}
126	      %Equal.sym(Bool, G.gen.bit(z, T.Pos{x, y}, st), False{},
127	        gen_bit_first(z, T.Pos{x, y}, st, s)) :
128	        {Some{_} == Some{False{}} : Maybe<&2, Bool>}
129	      {==}
130	    case a <> t 1n+k:
131	      gen_row_first(z, y, t, k, x, G.gen.next(z, T.Pos{a, y}, st), e, s)
132	
133	def Maybe.disc_some(-A: Data, m: Maybe<&2, A>) -> Type:
134	  match m:
135	    case None{}:
136	      Empty
137	    case Some{v}:
138	      Unit
139	
140	def gen_some_ne_none(-A: Data, -a: A, e: {Some{a} == None{} : Maybe<&2, A>}) -> Empty:
141	  %e : Maybe.disc_some(A, _)
142	  Unit{}
143	
144	law gen_row_out:
145	  for +z: G.Zone
146	  for +y: Nat
147	  for +xs: List<&2, Nat>
148	  for +j: Nat
149	  for +st: G.GenState
150	  for e: {List.get(&2, Nat, xs, j) == None{} : Maybe<&2, Nat>}
151	  {List.get(&2, Bool, G.gen.row(z, y, xs, st), j) == None{} : Maybe<&2, Bool>}
152	
153	def gen_row_out(z, y, xs, j, st, e):
154	  match xs j:
155	    case Nil{} _:
156	      {==}
157	    case a <> t 0n:
158	      Empty.absurd({List.get(&2, Bool, G.gen.row(z, y, a <> t, st), 0n) == None{}
159	        : Maybe<&2, Bool>}, gen_some_ne_none(Nat, a, e))
160	    case a <> t 1n+k:
161	      gen_row_out(z, y, t, k, G.gen.next(z, T.Pos{a, y}, st), e)
162	
163	law gen_rows_get:
164	  for +z: G.Zone
165	  for +w: Nat
166	  for +ys: List<&2, Nat>
167	  for +i: Nat
168	  for +y: Nat
169	  for +st: G.GenState
170	  for e: {List.get(&2, Nat, ys, i) == Some{y} : Maybe<&2, Nat>}
171	  exs st2: G.GenState
172	  {List.get(&2, List<&2, Bool>, G.gen.rows(z, w, ys, st), i)
173	    == Some{G.gen.row(z, y, List.range(w), st2)} : Maybe<&2, List<&2, Bool>>}
174	
175	def gen_rows_get(z, w, ys, i, y, st, e):
176	  match ys i:
177	    case Nil{} _:
178	      Empty.absurd(Exists(G.GenState, st2 => {List.get(&2, List<&2, Bool>,
179	        G.gen.rows(z, w, Nil{}, st), i) == Some{G.gen.row(z, y, List.range(w), st2)}
180	        : Maybe<&2, List<&2, Bool>>}), PG.know_row_get.none(Nat, y, e))
181	    case a <> t 0n:
182	      %PG.know_row_get.some(Nat, a, y, e) :
183	        Exists(G.GenState, st2 => {Some{G.gen.row(z, a, List.range(w), st)}
184	          == Some{G.gen.row(z, _, List.range(w), st2)} : Maybe<&2, List<&2, Bool>>})
185	      (st, {==})
186	    case a <> t 1n+k:
187	      gen_rows_get(z, w, t, k, y, G.gen.row_state(z, a, List.range(w), st), e)
188	
189	law gen_rows_out:
190	  for +z: G.Zone
191	  for +w: Nat
192	  for +ys: List<&2, Nat>
193	  for +i: Nat
194	  for +st: G.GenState
195	  for e: {List.get(&2, Nat, ys, i) == None{} : Maybe<&2, Nat>}
196	  {List.get(&2, List<&2, Bool>, G.gen.rows(z, w, ys, st), i) == None{}
197	    : Maybe<&2, List<&2, Bool>>}
198	
199	def gen_rows_out(z, w, ys, i, st, e):
200	  match ys i:
201	    case Nil{} _:
202	      {==}
203	    case a <> t 0n:
204	      Empty.absurd({List.get(&2, List<&2, Bool>, G.gen.rows(z, w, a <> t, st), 0n) == None{}
205	        : Maybe<&2, List<&2, Bool>>}, gen_some_ne_none(Nat, a, e))
206	    case a <> t 1n+k:
207	      gen_rows_out(z, w, t, k, G.gen.row_state(z, a, List.range(w), st), e)
208	
209	def gen_first.col(+z: G.Zone, +fx: Nat, +fy: Nat, +w: Nat, +st2: G.GenState,
210	  s: {G.gen.out(z, T.Pos{fx, fy}) == True{} : Bool}, +b: Bool,
211	  e: {Nat.is_lt(fx, w) == b : Bool}) ->
212	  {Maybe.default(&2, Bool, List.get(&2, Bool, G.gen.row(z, fy, List.range(w), st2), fx), False{})
213	    == False{} : Bool}:
214	  match b:
215	    case True{}:
216	      %Equal.sym(Maybe<&2, Bool>, List.get(&2, Bool, G.gen.row(z, fy, List.range(w), st2), fx),
217	        Some{False{}},
218	        gen_row_first(z, fy, List.range(w), fx, fx, st2, P.range_get(w, fx, e), s)) :
219	        {Maybe.default(&2, Bool, _, False{}) == False{} : Bool}
220	      {==}
221	    case False{}:
222	      %Equal.sym(Maybe<&2, Bool>, List.get(&2, Bool, G.gen.row(z, fy, List.range(w), st2), fx),
223	        None{}, gen_row_out(z, fy, List.range(w), fx, st2, P.range_get_out(w, fx, e))) :
224	        {Maybe.default(&2, Bool, _, False{}) == False{} : Bool}
225	      {==}
226	
227	def gen_first.found(+z: G.Zone, +fx: Nat, +fy: Nat, +w: Nat, +g: T.Grid(Bool),
228	  s: {G.gen.out(z, T.Pos{fx, fy}) == True{} : Bool},
229	  r: Exists(G.GenState, st2 => {List.get(&2, List<&2, Bool>, g, fy)
230	    == Some{G.gen.row(z, fy, List.range(w), st2)} : Maybe<&2, List<&2, Bool>>})) ->
231	  {L.mine(g, T.Pos{fx, fy}) == False{} : Bool}:
232	  match r:
233	    case (st2, eq):
234	      %Equal.sym(Maybe<&2, List<&2, Bool>>, List.get(&2, List<&2, Bool>, g, fy),
235	        Some{G.gen.row(z, fy, List.range(w), st2)}, eq) :
236	        {Maybe.default(&2, Bool, List.get(&2, Bool,
237	          Maybe.default(&2, List<&2, Bool>, _, Nil{}), fx), False{}) == False{} : Bool}
238	      gen_first.col(z, fx, fy, w, st2, s, Nat.is_lt(fx, w), {==})
239	
240	def gen_first.row(+z: G.Zone, +fx: Nat, +fy: Nat, +w: Nat, +h: Nat, +st: G.GenState,
241	  s: {G.gen.out(z, T.Pos{fx, fy}) == True{} : Bool}, +b: Bool,
242	  e: {Nat.is_lt(fy, h) == b : Bool}) ->
243	  {L.mine(G.gen.rows(z, w, List.range(h), st), T.Pos{fx, fy}) == False{} : Bool}:
244	  match b:
245	    case True{}:
246	      gen_first.found(z, fx, fy, w, G.gen.rows(z, w, List.range(h), st), s,
247	        gen_rows_get(z, w, List.range(h), fy, fy, st, P.range_get(h, fy, e)))
248	    case False{}:
249	      %Equal.sym(Maybe<&2, List<&2, Bool>>,
250	        List.get(&2, List<&2, Bool>, G.gen.rows(z, w, List.range(h), st), fy), None{},
251	        gen_rows_out(z, w, List.range(h), fy, st, P.range_get_out(h, fy, e))) :
252	        {Maybe.default(&2, Bool, List.get(&2, Bool,
253	          Maybe.default(&2, List<&2, Bool>, _, Nil{}), fx), False{}) == False{} : Bool}
254	      {==}
255	
256	law sub_self:
257	  for +a: Nat
258	  {Nat.sub(a, a) == 0n : Nat}
259	
260	def sub_self(a):
261	  match a:
262	    case 0n:
263	      {==}
264	    case 1n+k:
265	      sub_self(k)
266	
267	# A cell is within one step of itself.
268	law within_self:
269	  for +p: T.Pos
270	  {B.within_one(p, p) == True{} : Bool}
271	
272	def within_self(p):
273	  match p:
274	    case T.Pos{x, y}:
275	      %Equal.sym(Nat, Nat.sub(x, x), 0n, sub_self(x)) :
276	        {Bool.and(Nat.is_le(Nat.add(_, _), 1n), Nat.is_le(Nat.add(Nat.sub(y, y), Nat.sub(y, y)), 1n)) == True{} : Bool}
277	      %Equal.sym(Nat, Nat.sub(y, y), 0n, sub_self(y)) :
278	        {Bool.and(Nat.is_le(Nat.add(0n, 0n), 1n), Nat.is_le(Nat.add(_, _), 1n)) == True{} : Bool}
279	      {==}
280	
281	# The first click is always in its own zone.
282	law out_first:
283	  for +first: T.Pos
284	  for +wide: Bool
285	  {G.gen.out(G.Zone{first, wide}, first) == True{} : Bool}
286	
287	def out_first(first, wide):
288	  match wide:
289	    case True{}:
290	      within_self(first)
291	    case False{}:
292	      PG.same_refl(first)
293	
294	law gen_first_safe_:
295	  for +w: Nat
296	  for +h: Nat
297	  for +n: Nat
298	  for +first: T.Pos
299	  for +rs: List<&2, U32>
300	  {L.mine(G.place_mines(w, h, n, first, rs), first) == False{} : Bool}
301	
302	def gen_first_safe_(w, h, n, first, rs):
303	  match first:
304	    case T.Pos{fx, fy}:
305	      +p = {T.Pos{fx, fy} : T.Pos}
306	      +z = zone(w, h, n, p)
307	      gen_first.row(z, fx, fy, w, h,
308	        {G.GenState{n, G.gen.left(z, B.cells(w, h)), rs} : G.GenState},
309	        out_first(p, Nat.is_le(Nat.add(n, 9n), Nat.mul(w, h))), Nat.is_lt(fy, h), {==})
310	
311	law within_eq:
312	  for +p: T.Pos
313	  for +q: T.Pos
314	  {B.within_one(p, q) == L.within_one(p, q) : Bool}
315	
316	def within_eq(p, q):
317	  match p q:
318	    case T.Pos{px, py} T.Pos{qx, qy}:
319	      {==}
320	
321	# A wide zone holds every cell next to the first click.
322	def opening_in(+first: T.Pos, +p: T.Pos, +wide: Bool, ew: {wide == True{} : Bool},
323	  near: {L.within_one(first, p) == True{} : Bool}) -> {G.gen.out(G.Zone{first, wide}, p) == True{} : Bool}:
324	  %Equal.sym(Bool, wide, True{}, ew) : {G.gen.out(G.Zone{first, _}, p) == True{} : Bool}
325	  Equal.trans(Bool, B.within_one(first, p), L.within_one(first, p), True{}, within_eq(first, p), near)
326	
327	# With room, no cell next to the first click gets a mine.
328	law gen_opening_:
329	  for +w: Nat
330	  for +h: Nat
331	  for +n: Nat
332	  for +first: T.Pos
333	  for +rs: List<&2, U32>
334	  for +room: {Nat.is_le(Nat.add(n, 9n), Nat.mul(w, h)) == True{} : Bool}
335	  for +q: T.Pos
336	  for +near: {L.within_one(first, q) == True{} : Bool}
337	  {L.mine(G.place_mines(w, h, n, first, rs), q) == False{} : Bool}
338	
339	def gen_opening_(w, h, n, first, rs, room, q, near):
340	  match q:
341	    case T.Pos{qx, qy}:
342	      +p = {T.Pos{qx, qy} : T.Pos}
343	      +z = zone(w, h, n, first)
344	      gen_first.row(z, qx, qy, w, h,
345	        {G.GenState{n, G.gen.left(z, B.cells(w, h)), rs} : G.GenState},
346	        opening_in(first, p, Nat.is_le(Nat.add(n, 9n), Nat.mul(w, h)), room, near), Nat.is_lt(qy, h), {==})
347	
348	# Exactly n mines
349	# ===============
350	
351	def st_need(st: G.GenState) -> Nat:
352	  match st:
353	    case G.GenState{need, left, rs}:
354	      need
355	
356	def st_left(st: G.GenState) -> Nat:
357	  match st:
358	    case G.GenState{need, left, rs}:
359	      left
360	
361	def one(b: Bool) -> Nat:
362	  Bool.pick(Nat, b, 1n, 0n)
363	
364	# What one cell does to the state: the mines placed plus the mines still
365	# needed stay the same, need <= left stays true, and left counts down for
366	# every cell outside the zone.
367	def GenStep(+z: G.Zone, +p: T.Pos, +st: G.GenState, +lp: Nat) -> Type:
368	  {Nat.add(one(G.gen.bit(z, p, st)), st_need(G.gen.next(z, p, st))) == st_need(st) : Nat} &
369	  {Nat.is_le(st_need(G.gen.next(z, p, st)), st_left(G.gen.next(z, p, st))) == True{} : Bool} &
370	  {st_left(G.gen.next(z, p, st)) == lp : Nat}
371	
372	def gen_pick_false(+need: Nat, +left: Nat, +rs: List<&2, U32>,
373	  e: {G.gen.pick(need, left, rs) == False{} : Bool}) -> {Nat.is_eq(need, left) == False{} : Bool}:
374	  match rs:
375	    case Nil{}:
376	      e
377	    case r <> t:
378	      P.or_false_inv(Nat.is_eq(need, left), G.gen.coin(r, left, need), e)
379	
380	def gen_take(+z: G.Zone, +p: T.Pos, +m: Nat, +lp: Nat, +rs: List<&2, U32>,
381	  inv: {Nat.is_le(1n+m, 1n+lp) == True{} : Bool}, +c: Bool,
382	  ce: {G.gen.pick(1n+m, 1n+lp, rs) == c : Bool}) ->
383	  {Nat.add(one(c), Nat.sub(1n+m, one(c))) == 1n+m : Nat} &
384	  {Nat.is_le(Nat.sub(1n+m, one(c)), Nat.sub(1n+lp, 1n)) == True{} : Bool} &
385	  {Nat.sub(1n+lp, 1n) == lp : Nat}:
386	  match c:
387	    case True{}:
388	      %Equal.sym(Nat, Nat.sub(m, 0n), m, P.sub_zero(m)) :
389	        {1n+_ == 1n+m : Nat} & {Nat.is_le(_, Nat.sub(lp, 0n)) == True{} : Bool} &
390	        {Nat.sub(lp, 0n) == lp : Nat}
391	      %Equal.sym(Nat, Nat.sub(lp, 0n), lp, P.sub_zero(lp)) :
392	        {1n+m == 1n+m : Nat} & {Nat.is_le(m, _) == True{} : Bool} & {_ == lp : Nat}
393	      ({==}, (inv, {==}))
394	    case False{}:
395	      %Equal.sym(Nat, Nat.sub(lp, 0n), lp, P.sub_zero(lp)) :
396	        {1n+m == 1n+m : Nat} & {Nat.is_le(1n+m, _) == True{} : Bool} & {_ == lp : Nat}
397	      ({==}, (P.le_ne(m, lp, inv, gen_pick_false(1n+m, 1n+lp, rs, ce)), {==}))
398	
399	def gen_cell.need(+z: G.Zone, +p: T.Pos, +need: Nat, +lp: Nat, +rs: List<&2, U32>,
400	  inv: {Nat.is_le(need, 1n+lp) == True{} : Bool}) ->
401	  {Nat.add(one(Bool.and(Nat.is_lt(0n, need), G.gen.pick(need, 1n+lp, rs))),
402	     Nat.sub(need, one(Bool.and(Nat.is_lt(0n, need), G.gen.pick(need, 1n+lp, rs))))) == need : Nat} &
403	  {Nat.is_le(Nat.sub(need, one(Bool.and(Nat.is_lt(0n, need), G.gen.pick(need, 1n+lp, rs)))),
404	     Nat.sub(1n+lp, 1n)) == True{} : Bool} &
405	  {Nat.sub(1n+lp, 1n) == lp : Nat}:
406	  match need:
407	    case 0n:
408	      %Equal.sym(Nat, Nat.sub(lp, 0n), lp, P.sub_zero(lp)) :
409	        {0n == 0n : Nat} & {Nat.is_le(0n, _) == True{} : Bool} & {_ == lp : Nat}
410	      ({==}, (P.le_zero_l(lp), {==}))
411	    case 1n+m:
412	      gen_take(z, p, m, lp, rs, inv, G.gen.pick(1n+m, 1n+lp, rs), {==})
413	
414	def gen_cell.go(+z: G.Zone, +p: T.Pos, +need: Nat, +left: Nat, +rs: List<&2, U32>, +lp: Nat,
415	  inv: {Nat.is_le(need, left) == True{} : Bool}, +s: Bool, e: {G.gen.out(z, p) == s : Bool},
416	  +lft: {left == Nat.add(Bool.pick(Nat, s, 0n, 1n), lp) : Nat}) ->
417	  GenStep(z, p, G.GenState{need, left, rs}, lp):
418	  match s:
419	    case True{}:
420	      %Equal.sym(Bool, G.gen.out(z, p), True{}, e) :
421	        {Nat.add(one(Bool.and(Bool.and(Bool.not(_), Nat.is_lt(0n, need)), G.gen.pick(need, left, rs))),
422	          st_need(G.gen.next.go(_, Bool.and(Bool.and(Bool.not(_), Nat.is_lt(0n, need)),
423	            G.gen.pick(need, left, rs)), need, left, rs))) == need : Nat} &
424	        {Nat.is_le(st_need(G.gen.next.go(_, Bool.and(Bool.and(Bool.not(_), Nat.is_lt(0n, need)),
425	            G.gen.pick(need, left, rs)), need, left, rs)),
426	          st_left(G.gen.next.go(_, Bool.and(Bool.and(Bool.not(_), Nat.is_lt(0n, need)),
427	            G.gen.pick(need, left, rs)), need, left, rs))) == True{} : Bool} &
428	        {st_left(G.gen.next.go(_, Bool.and(Bool.and(Bool.not(_), Nat.is_lt(0n, need)),
429	            G.gen.pick(need, left, rs)), need, left, rs)) == lp : Nat}
430	      ({==}, (inv, lft))
431	    case False{}:
432	      %Equal.sym(Bool, G.gen.out(z, p), False{}, e) :
433	        {Nat.add(one(Bool.and(Bool.and(Bool.not(_), Nat.is_lt(0n, need)), G.gen.pick(need, left, rs))),
434	          st_need(G.gen.next.go(_, Bool.and(Bool.and(Bool.not(_), Nat.is_lt(0n, need)),
435	            G.gen.pick(need, left, rs)), need, left, rs))) == need : Nat} &
436	        {Nat.is_le(st_need(G.gen.next.go(_, Bool.and(Bool.and(Bool.not(_), Nat.is_lt(0n, need)),
437	            G.gen.pick(need, left, rs)), need, left, rs)),
438	          st_left(G.gen.next.go(_, Bool.and(Bool.and(Bool.not(_), Nat.is_lt(0n, need)),
439	            G.gen.pick(need, left, rs)), need, left, rs))) == True{} : Bool} &
440	        {st_left(G.gen.next.go(_, Bool.and(Bool.and(Bool.not(_), Nat.is_lt(0n, need)),
441	            G.gen.pick(need, left, rs)), need, left, rs)) == lp : Nat}
442	      %Equal.sym(Nat, left, 1n+lp, lft) :
443	        {Nat.add(one(Bool.and(Nat.is_lt(0n, need), G.gen.pick(need, _, rs))),
444	          Nat.sub(need, one(Bool.and(Nat.is_lt(0n, need), G.gen.pick(need, _, rs))))) == need : Nat} &
445	        {Nat.is_le(Nat.sub(need, one(Bool.and(Nat.is_lt(0n, need), G.gen.pick(need, _, rs)))),
446	          Nat.sub(_, 1n)) == True{} : Bool} &
447	        {Nat.sub(_, 1n) == lp : Nat}
448	      gen_cell.need(z, p, need, lp, rs,
449	        {%lft : {Nat.is_le(need, _) == True{} : Bool}; inv : {Nat.is_le(need, 1n+lp) == True{} : Bool}})
450	
451	
452	law gen_cell:
453	  for +z: G.Zone
454	  for +p: T.Pos
455	  for +st: G.GenState
456	  for +lp: Nat
457	  for inv: {Nat.is_le(st_need(st), st_left(st)) == True{} : Bool}
458	  for lft: {st_left(st) == Nat.add(Bool.pick(Nat, G.gen.out(z, p), 0n, 1n), lp) : Nat}
459	  GenStep(z, p, st, lp)
460	
461	def gen_cell(z, p, st, lp, inv, lft):
462	  match st:
463	    case G.GenState{need, left, rs}:
464	      gen_cell.go(z, p, need, left, rs, lp, inv, G.gen.out(z, p), {==}, lft)
465	
466	def gen_row_count.step(+z: G.Zone, +p: T.Pos, +st: G.GenState, +rm: Nat, +nf: Nat,
467	  s1: {Nat.add(one(G.gen.bit(z, p, st)), st_need(G.gen.next(z, p, st))) == st_need(st) : Nat},
468	  r1: {Nat.add(rm, nf) == st_need(G.gen.next(z, p, st)) : Nat}) ->
469	  {Nat.add(Nat.add(one(G.gen.bit(z, p, st)), rm), nf) == st_need(st) : Nat}:
470	  %Equal.sym(Nat, Nat.add(Nat.add(one(G.gen.bit(z, p, st)), rm), nf),
471	    Nat.add(one(G.gen.bit(z, p, st)), Nat.add(rm, nf)),
472	    P.add_assoc(one(G.gen.bit(z, p, st)), rm, nf)) : {_ == st_need(st) : Nat}
473	  %Equal.sym(Nat, Nat.add(rm, nf), st_need(G.gen.next(z, p, st)), r1) :
474	    {Nat.add(one(G.gen.bit(z, p, st)), _) == st_need(st) : Nat}
475	  s1
476	
477	def gen_row_count.k2(+z: G.Zone, +y: Nat, +t: List<&2, Nat>, +p: T.Pos, +st: G.GenState,
478	  +cs: List<&2, T.Pos>,
479	  s1: {Nat.add(one(G.gen.bit(z, p, st)), st_need(G.gen.next(z, p, st))) == st_need(st) : Nat},
480	  r: {Nat.add(L.row_mines(G.gen.row(z, y, t, G.gen.next(z, p, st))),
481	       st_need(G.gen.row_state(z, y, t, G.gen.next(z, p, st)))) == st_need(G.gen.next(z, p, st)) : Nat} &
482	    {Nat.is_le(st_need(G.gen.row_state(z, y, t, G.gen.next(z, p, st))),
483	       st_left(G.gen.row_state(z, y, t, G.gen.next(z, p, st)))) == True{} : Bool} &
484	    {st_left(G.gen.row_state(z, y, t, G.gen.next(z, p, st))) == G.gen.left(z, cs) : Nat}) ->
485	  {Nat.add(Nat.add(one(G.gen.bit(z, p, st)), L.row_mines(G.gen.row(z, y, t, G.gen.next(z, p, st)))),
486	     st_need(G.gen.row_state(z, y, t, G.gen.next(z, p, st)))) == st_need(st) : Nat} &
487	  {Nat.is_le(st_need(G.gen.row_state(z, y, t, G.gen.next(z, p, st))),
488	     st_left(G.gen.row_state(z, y, t, G.gen.next(z, p, st)))) == True{} : Bool} &
489	  {st_left(G.gen.row_state(z, y, t, G.gen.next(z, p, st))) == G.gen.left(z, cs) : Nat}:
490	  match r:
491	    case (r1, rest):
492	      (gen_row_count.step(z, p, st,
493	        L.row_mines(G.gen.row(z, y, t, G.gen.next(z, p, st))),
494	        st_need(G.gen.row_state(z, y, t, G.gen.next(z, p, st))), s1, r1), rest)
495	
496	def gen_row_count.k(+z: G.Zone, +y: Nat, +t: List<&2, Nat>, +p: T.Pos, +st: G.GenState,
497	  +cs: List<&2, T.Pos>,
498	  step: GenStep(z, p, st, G.gen.left(z, List.append(&2, T.Pos, B.row_cells(y, t), cs))),
499	  ih: ({Nat.is_le(st_need(G.gen.next(z, p, st)), st_left(G.gen.next(z, p, st))) == True{} : Bool} ->
500	    {st_left(G.gen.next(z, p, st)) == G.gen.left(z, List.append(&2, T.Pos, B.row_cells(y, t), cs)) : Nat} ->
501	    {Nat.add(L.row_mines(G.gen.row(z, y, t, G.gen.next(z, p, st))),
502	       st_need(G.gen.row_state(z, y, t, G.gen.next(z, p, st)))) == st_need(G.gen.next(z, p, st)) : Nat} &
503	    {Nat.is_le(st_need(G.gen.row_state(z, y, t, G.gen.next(z, p, st))),
504	       st_left(G.gen.row_state(z, y, t, G.gen.next(z, p, st)))) == True{} : Bool} &
505	    {st_left(G.gen.row_state(z, y, t, G.gen.next(z, p, st))) == G.gen.left(z, cs) : Nat})) ->
506	  {Nat.add(Nat.add(one(G.gen.bit(z, p, st)), L.row_mines(G.gen.row(z, y, t, G.gen.next(z, p, st)))),
507	     st_need(G.gen.row_state(z, y, t, G.gen.next(z, p, st)))) == st_need(st) : Nat} &
508	  {Nat.is_le(st_need(G.gen.row_state(z, y, t, G.gen.next(z, p, st))),
509	     st_left(G.gen.row_state(z, y, t, G.gen.next(z, p, st)))) == True{} : Bool} &
510	  {st_left(G.gen.row_state(z, y, t, G.gen.next(z, p, st))) == G.gen.left(z, cs) : Nat}:
511	  match step:
512	    case (s1, rest):
513	      match rest:
514	        case (s2, s3):
515	          gen_row_count.k2(z, y, t, p, st, cs, s1, ih(s2, s3))
516	
517	
518	law gen_row_count:
519	  for +z: G.Zone
520	  for +y: Nat
521	  for +xs: List<&2, Nat>
522	  for +st: G.GenState
523	  for +cs: List<&2, T.Pos>
524	  for inv: {Nat.is_le(st_need(st), st_left(st)) == True{} : Bool}
525	  for lft: {st_left(st) == G.gen.left(z, List.append(&2, T.Pos, B.row_cells(y, xs), cs)) : Nat}
526	  {Nat.add(L.row_mines(G.gen.row(z, y, xs, st)), st_need(G.gen.row_state(z, y, xs, st)))
527	    == st_need(st) : Nat} &
528	  {Nat.is_le(st_need(G.gen.row_state(z, y, xs, st)), st_left(G.gen.row_state(z, y, xs, st)))
529	    == True{} : Bool} &
530	  {st_left(G.gen.row_state(z, y, xs, st)) == G.gen.left(z, cs) : Nat}
531	
532	def gen_row_count(z, y, xs, st, cs, inv, lft):
533	  match xs:
534	    case Nil{}:
535	      ({==}, (inv, lft))
536	    case x <> t:
537	      +p = {T.Pos{x, y} : T.Pos}
538	      +lp = G.gen.left(z, List.append(&2, T.Pos, B.row_cells(y, t), cs))
539	      +nx = G.gen.next(z, p, st)
540	      gen_row_count.k(z, y, t, p, st, cs, gen_cell(z, p, st, lp, inv, lft),
541	        s => gen_row_count(z, y, t, nx, cs, s))
542	
543	
544	def gen_rows_count.k(+z: G.Zone, +w: Nat, +y: Nat, +t: List<&2, Nat>, +st: G.GenState,
545	  r: {Nat.add(L.row_mines(G.gen.row(z, y, List.range(w), st)),
546	       st_need(G.gen.row_state(z, y, List.range(w), st))) == st_need(st) : Nat} &
547	    {Nat.is_le(st_need(G.gen.row_state(z, y, List.range(w), st)),
548	       st_left(G.gen.row_state(z, y, List.range(w), st))) == True{} : Bool} &
549	    {st_left(G.gen.row_state(z, y, List.range(w), st)) == G.gen.left(z, B.cells.go(w, t)) : Nat},
550	  ih: {Nat.is_le(st_need(G.gen.row_state(z, y, List.range(w), st)),
551	       st_left(G.gen.row_state(z, y, List.range(w), st))) == True{} : Bool} ->
552	    {st_left(G.gen.row_state(z, y, List.range(w), st)) == G.gen.left(z, B.cells.go(w, t)) : Nat} ->
553	    {L.total_mines(G.gen.rows(z, w, t, G.gen.row_state(z, y, List.range(w), st)))
554	      == st_need(G.gen.row_state(z, y, List.range(w), st)) : Nat}) ->
555	  {Nat.add(L.row_mines(G.gen.row(z, y, List.range(w), st)),
556	     L.total_mines(G.gen.rows(z, w, t, G.gen.row_state(z, y, List.range(w), st))))
557	    == st_need(st) : Nat}:
558	  match r:
559	    case (r1, rest):
560	      match rest:
561	        case (r2, r3):
562	          %Equal.sym(Nat, L.total_mines(G.gen.rows(z, w, t, G.gen.row_state(z, y, List.range(w), st))),
563	            st_need(G.gen.row_state(z, y, List.range(w), st)), ih(r2, r3)) :
564	            {Nat.add(L.row_mines(G.gen.row(z, y, List.range(w), st)), _) == st_need(st) : Nat}
565	          r1
566	
567	law gen_rows_count:
568	  for +z: G.Zone
569	  for +w: Nat
570	  for +ys: List<&2, Nat>
571	  for +st: G.GenState
572	  for inv: {Nat.is_le(st_need(st), st_left(st)) == True{} : Bool}
573	  for lft: {st_left(st) == G.gen.left(z, B.cells.go(w, ys)) : Nat}
574	  {L.total_mines(G.gen.rows(z, w, ys, st)) == st_need(st) : Nat}
575	
576	def gen_rows_count(z, w, ys, st, inv, lft):
577	  match ys:
578	    case Nil{}:
579	      Equal.sym(Nat, st_need(st), 0n, P.le_zero(st_need(st),
580	        {%lft : {Nat.is_le(st_need(st), _) == True{} : Bool};
581	          inv : {Nat.is_le(st_need(st), 0n) == True{} : Bool}}))
582	    case y <> t:
583	      +rs2 = G.gen.row_state(z, y, List.range(w), st)
584	      gen_rows_count.k(z, w, y, t, st,
585	        gen_row_count(z, y, List.range(w), st, B.cells.go(w, t), inv, lft),
586	        a => b => gen_rows_count(z, w, t, rs2, a, b))
587	
588	# Counting the candidates
589	# =======================
590	
591	# How many cells of ps are in the zone.
592	def outs(+z: G.Zone, ps: List<&2, T.Pos>) -> Nat:
593	  match ps:
594	    case Nil{}:
595	      0n
596	    case p <> t:
597	      Nat.add(Bool.pick(Nat, G.gen.out(z, p), 1n, 0n), outs(z, t))
598	
599	def gen_left_firsts.go(+z: G.Zone, +p: T.Pos, +t: List<&2, T.Pos>, +s: Bool,
600	  ih: {Nat.add(G.gen.left(z, t), outs(z, t)) == List.length(&2, T.Pos, t) : Nat}) ->
601	  {Nat.add(Nat.add(Bool.pick(Nat, s, 0n, 1n), G.gen.left(z, t)),
602	     Nat.add(Bool.pick(Nat, s, 1n, 0n), outs(z, t))) == 1n+List.length(&2, T.Pos, t) : Nat}:
603	  match s:
604	    case True{}:
605	      %Equal.sym(Nat, Nat.add(G.gen.left(z, t), 1n+outs(z, t)),
606	        1n+Nat.add(G.gen.left(z, t), outs(z, t)),
607	        P.add_succ(G.gen.left(z, t), outs(z, t))) :
608	        {_ == 1n+List.length(&2, T.Pos, t) : Nat}
609	      %Equal.sym(Nat, Nat.add(G.gen.left(z, t), outs(z, t)), List.length(&2, T.Pos, t), ih) :
610	        {1n+_ == 1n+List.length(&2, T.Pos, t) : Nat}
611	      {==}
612	    case False{}:
613	      %Equal.sym(Nat, Nat.add(G.gen.left(z, t), outs(z, t)), List.length(&2, T.Pos, t), ih) :
614	        {1n+_ == 1n+List.length(&2, T.Pos, t) : Nat}
615	      {==}
616	
617	# Every cell is either a candidate or in the zone.
618	law gen_left_firsts:
619	  for +z: G.Zone
620	  for +ps: List<&2, T.Pos>
621	  {Nat.add(G.gen.left(z, ps), outs(z, ps)) == List.length(&2, T.Pos, ps) : Nat}
622	
623	def gen_left_firsts(z, ps):
624	  match ps:
625	    case Nil{}:
626	      {==}
627	    case p <> t:
628	      gen_left_firsts.go(z, p, t, G.gen.out(z, p), gen_left_firsts(z, t))
629	
630	law firsts_append:
631	  for +z: G.Zone
632	  for +xs: List<&2, T.Pos>
633	  for +ys: List<&2, T.Pos>
634	  {outs(z, List.append(&2, T.Pos, xs, ys)) == Nat.add(outs(z, xs), outs(z, ys)) : Nat}
635	
636	def firsts_append(z, xs, ys):
637	  match xs:
638	    case Nil{}:
639	      {==}
640	    case p <> t:
641	      %Equal.sym(Nat, outs(z, List.append(&2, T.Pos, t, ys)),
642	        Nat.add(outs(z, t), outs(z, ys)), firsts_append(z, t, ys)) :
643	        {Nat.add(Bool.pick(Nat, G.gen.out(z, p), 1n, 0n), _)
644	          == Nat.add(Nat.add(Bool.pick(Nat, G.gen.out(z, p), 1n, 0n), outs(z, t)), outs(z, ys)) : Nat}
645	      Equal.sym(Nat, Nat.add(Nat.add(Bool.pick(Nat, G.gen.out(z, p), 1n, 0n), outs(z, t)), outs(z, ys)),
646	        Nat.add(Bool.pick(Nat, G.gen.out(z, p), 1n, 0n), Nat.add(outs(z, t), outs(z, ys))),
647	        P.add_assoc(Bool.pick(Nat, G.gen.out(z, p), 1n, 0n), outs(z, t), outs(z, ys)))
648	
649	# How many elements of xs are i.
650	def cnt(+i: Nat, xs: List<&2, Nat>) -> Nat:
651	  match xs:
652	    case Nil{}:
653	      0n
654	    case x <> t:
655	      Nat.add(Bool.pick(Nat, Nat.is_eq(x, i), 1n, 0n), cnt(i, t))
656	
657	law cnt_append:
658	  for +i: Nat
659	  for +xs: List<&2, Nat>
660	  for +ys: List<&2, Nat>
661	  {cnt(i, List.append(&2, Nat, xs, ys)) == Nat.add(cnt(i, xs), cnt(i, ys)) : Nat}
662	
663	def cnt_append(i, xs, ys):
664	  match xs:
665	    case Nil{}:
666	      {==}
667	    case x <> t:
668	      %Equal.sym(Nat, cnt(i, List.append(&2, Nat, t, ys)), Nat.add(cnt(i, t), cnt(i, ys)), cnt_append(i, t, ys)) :
669	        {Nat.add(Bool.pick(Nat, Nat.is_eq(x, i), 1n, 0n), _)
670	          == Nat.add(Nat.add(Bool.pick(Nat, Nat.is_eq(x, i), 1n, 0n), cnt(i, t)), cnt(i, ys)) : Nat}
671	      Equal.sym(Nat, Nat.add(Nat.add(Bool.pick(Nat, Nat.is_eq(x, i), 1n, 0n), cnt(i, t)), cnt(i, ys)),
672	        Nat.add(Bool.pick(Nat, Nat.is_eq(x, i), 1n, 0n), Nat.add(cnt(i, t), cnt(i, ys))),
673	        P.add_assoc(Bool.pick(Nat, Nat.is_eq(x, i), 1n, 0n), cnt(i, t), cnt(i, ys)))
674	
675	law cnt_step:
676	  for +i: Nat
677	  for +p: Nat
678	  {Nat.add(Bool.pick(Nat, Nat.is_lt(i, p), 1n, 0n), Nat.add(Bool.pick(Nat, Nat.is_eq(p, i), 1n, 0n), 0n))
679	    == Bool.pick(Nat, Nat.is_lt(i, 1n+p), 1n, 0n) : Nat}
680	
681	def cnt_step(i, p):
682	  match i p:
683	    case 0n 0n:
684	      {==}
685	    case 0n 1n+q:
686	      {==}
687	    case 1n+j 0n:
688	      %Equal.sym(Bool, Nat.is_lt(j, 0n), False{}, P.lt_zero(j)) :
689	        {0n == Bool.pick(Nat, _, 1n, 0n) : Nat}
690	      {==}
691	    case 1n+j 1n+q:
692	      cnt_step(j, q)
693	
694	# Each number below n appears in range(n) once.
695	law cnt_range:
696	  for +i: Nat
697	  for +n: Nat
698	  {cnt(i, List.range(n)) == Bool.pick(Nat, Nat.is_lt(i, n), 1n, 0n) : Nat}
699	
700	def cnt_range(i, n):
701	  match n:
702	    case 0n:
703	      %Equal.sym(Bool, Nat.is_lt(i, 0n), False{}, P.lt_zero(i)) :
704	        {0n == Bool.pick(Nat, _, 1n, 0n) : Nat}
705	      {==}
706	    case 1n+p:
707	      %Equal.sym(List<&2, Nat>, List.range(1n+p), List.append(&2, Nat, List.range(p), [p]), P.range_snoc(p)) :
708	        {cnt(i, _) == Bool.pick(Nat, Nat.is_lt(i, 1n+p), 1n, 0n) : Nat}
709	      %Equal.sym(Nat, cnt(i, List.append(&2, Nat, List.range(p), [p])),
710	        Nat.add(cnt(i, List.range(p)), cnt(i, [p])), cnt_append(i, List.range(p), [p])) :
711	        {_ == Bool.pick(Nat, Nat.is_lt(i, 1n+p), 1n, 0n) : Nat}
712	      %Equal.sym(Nat, cnt(i, List.range(p)), Bool.pick(Nat, Nat.is_lt(i, p), 1n, 0n), cnt_range(i, p)) :
713	        {Nat.add(_, cnt(i, [p])) == Bool.pick(Nat, Nat.is_lt(i, 1n+p), 1n, 0n) : Nat}
714	      cnt_step(i, p)
715	
716	def firsts_row.end(+a: Bool, +b: Bool, +c: Nat) ->
717	  {Nat.add(Bool.pick(Nat, Bool.and(a, b), 1n, 0n), Bool.pick(Nat, b, c, 0n))
718	    == Bool.pick(Nat, b, Nat.add(Bool.pick(Nat, a, 1n, 0n), c), 0n) : Nat}:
719	  match a b:
720	    case True{} True{}:
721	      {==}
722	    case True{} False{}:
723	      {==}
724	    case False{} True{}:
725	      {==}
726	    case False{} False{}:
727	      {==}
728	
729	def firsts_row.go(+fx: Nat, +fy: Nat, +y: Nat, +xs: List<&2, Nat>, +b: Bool,
730	  +e: {Nat.is_eq(y, fy) == b : Bool}) ->
731	  {outs(G.Zone{T.Pos{fx, fy}, False{}}, B.row_cells(y, xs)) == Bool.pick(Nat, b, cnt(fx, xs), 0n) : Nat}:
732	  match xs:
733	    case Nil{}:
734	      match b:
735	        case True{}:
736	          {==}
737	        case False{}:
738	          {==}
739	    case x <> t:
740	      %Equal.sym(Bool, Nat.is_eq(y, fy), b, e) :
741	        {Nat.add(Bool.pick(Nat, Bool.and(Nat.is_eq(x, fx), _), 1n, 0n), outs(G.Zone{T.Pos{fx, fy}, False{}}, B.row_cells(y, t)))
742	          == Bool.pick(Nat, b, cnt(fx, x <> t), 0n) : Nat}
743	      %Equal.sym(Nat, outs(G.Zone{T.Pos{fx, fy}, False{}}, B.row_cells(y, t)), Bool.pick(Nat, b, cnt(fx, t), 0n),
744	        firsts_row.go(fx, fy, y, t, b, e)) :
745	        {Nat.add(Bool.pick(Nat, Bool.and(Nat.is_eq(x, fx), b), 1n, 0n), _)
746	          == Bool.pick(Nat, b, cnt(fx, x <> t), 0n) : Nat}
747	      firsts_row.end(Nat.is_eq(x, fx), b, cnt(fx, t))
748	
749	def firsts_rows.go(+fx: Nat, +fy: Nat, +w: Nat, +y: Nat, +t: List<&2, Nat>,
750	  c1: {cnt(fx, List.range(w)) == 1n : Nat},
751	  ih: {outs(G.Zone{T.Pos{fx, fy}, False{}}, B.cells.go(w, t)) == cnt(fy, t) : Nat}) ->
752	  {outs(G.Zone{T.Pos{fx, fy}, False{}}, List.append(&2, T.Pos, B.row_cells(y, List.range(w)), B.cells.go(w, t)))
753	    == cnt(fy, y <> t) : Nat}:
754	  +row = B.row_cells(y, List.range(w))
755	  %Equal.sym(Nat, outs(G.Zone{T.Pos{fx, fy}, False{}}, List.append(&2, T.Pos, row, B.cells.go(w, t))),
756	    Nat.add(outs(G.Zone{T.Pos{fx, fy}, False{}}, row), outs(G.Zone{T.Pos{fx, fy}, False{}}, B.cells.go(w, t))),
757	    firsts_append(G.Zone{T.Pos{fx, fy}, False{}}, row, B.cells.go(w, t))) : {_ == cnt(fy, y <> t) : Nat}
758	  %Equal.sym(Nat, outs(G.Zone{T.Pos{fx, fy}, False{}}, row), Bool.pick(Nat, Nat.is_eq(y, fy), cnt(fx, List.range(w)), 0n),
759	    firsts_row.go(fx, fy, y, List.range(w), Nat.is_eq(y, fy), {==})) :
760	    {Nat.add(_, outs(G.Zone{T.Pos{fx, fy}, False{}}, B.cells.go(w, t))) == cnt(fy, y <> t) : Nat}
761	  %Equal.sym(Nat, cnt(fx, List.range(w)), 1n, c1) :
762	    {Nat.add(Bool.pick(Nat, Nat.is_eq(y, fy), _, 0n), outs(G.Zone{T.Pos{fx, fy}, False{}}, B.cells.go(w, t)))
763	      == cnt(fy, y <> t) : Nat}
764	  %Equal.sym(Nat, outs(G.Zone{T.Pos{fx, fy}, False{}}, B.cells.go(w, t)), cnt(fy, t), ih) :
765	    {Nat.add(Bool.pick(Nat, Nat.is_eq(y, fy), 1n, 0n), _) == cnt(fy, y <> t) : Nat}
766	  {==}
767	
768	law firsts_rows:
769	  for +fx: Nat
770	  for +fy: Nat
771	  for +w: Nat
772	  for +ys: List<&2, Nat>
773	  for +c1: {cnt(fx, List.range(w)) == 1n : Nat}
774	  {outs(G.Zone{T.Pos{fx, fy}, False{}}, B.cells.go(w, ys)) == cnt(fy, ys) : Nat}
775	
776	def firsts_rows(fx, fy, w, ys, c1):
777	  match ys:
778	    case Nil{}:
779	      {==}
780	    case y <> t:
781	      firsts_rows.go(fx, fy, w, y, t, c1, firsts_rows(fx, fy, w, t, c1))
782	
783	law row_cells_len:
784	  for +y: Nat
785	  for +xs: List<&2, Nat>
786	  {List.length(&2, T.Pos, B.row_cells(y, xs)) == List.length(&2, Nat, xs) : Nat}
787	
788	def row_cells_len(y, xs):
789	  match xs:
790	    case Nil{}:
791	      {==}
792	    case x <> t:
793	      %Equal.sym(Nat, List.length(&2, T.Pos, B.row_cells(y, t)), List.length(&2, Nat, t), row_cells_len(y, t)) :
794	        {1n+_ == 1n+List.length(&2, Nat, t) : Nat}
795	      {==}
796	
797	law cells_go_len:
798	  for +w: Nat
799	  for +ys: List<&2, Nat>
800	  {List.length(&2, T.Pos, B.cells.go(w, ys)) == Nat.mul(List.length(&2, Nat, ys), w) : Nat}
801	
802	def cells_go_len(w, ys):
803	  match ys:
804	    case Nil{}:
805	      {==}
806	    case y <> t:
807	      +row = B.row_cells(y, List.range(w))
808	      %Equal.sym(Nat, List.length(&2, T.Pos, List.append(&2, T.Pos, row, B.cells.go(w, t))),
809	        Nat.add(List.length(&2, T.Pos, row), List.length(&2, T.Pos, B.cells.go(w, t))),
810	        P.length_append(T.Pos, row, B.cells.go(w, t))) :
811	        {_ == Nat.add(w, Nat.mul(List.length(&2, Nat, t), w)) : Nat}
812	      %Equal.sym(Nat, List.length(&2, T.Pos, row), w,
813	        Equal.trans(Nat, List.length(&2, T.Pos, row), List.length(&2, Nat, List.range(w)), w,
814	          row_cells_len(y, List.range(w)), P.range_length(w))) :
815	        {Nat.add(_, List.length(&2, T.Pos, B.cells.go(w, t))) == Nat.add(w, Nat.mul(List.length(&2, Nat, t), w)) : Nat}
816	      %Equal.sym(Nat, List.length(&2, T.Pos, B.cells.go(w, t)), Nat.mul(List.length(&2, Nat, t), w), cells_go_len(w, t)) :
817	        {Nat.add(w, _) == Nat.add(w, Nat.mul(List.length(&2, Nat, t), w)) : Nat}
818	      {==}
819	
820	def one_when(+i: Nat, +n: Nat, lt: {Nat.is_lt(i, n) == True{} : Bool}) -> {cnt(i, List.range(n)) == 1n : Nat}:
821	  Equal.trans(Nat, cnt(i, List.range(n)), Bool.pick(Nat, Nat.is_lt(i, n), 1n, 0n), 1n,
822	    cnt_range(i, n),
823	    Equal.cong(Bool, Nat, b => Bool.pick(Nat, b, 1n, 0n), Nat.is_lt(i, n), True{}, lt))
824	
825	# Arithmetic
826	# ==========
827	
828	law le_trans:
829	  for +a: Nat
830	  for +b: Nat
831	  for +c: Nat
832	  for e1: {Nat.is_le(a, b) == True{} : Bool}
833	  for e2: {Nat.is_le(b, c) == True{} : Bool}
834	  {Nat.is_le(a, c) == True{} : Bool}
835	
836	def le_trans.k(+a: Nat, +b: Nat, +c: Nat, r1: P.LeW(a, b), r2: P.LeW(b, c)) -> {Nat.is_le(a, c) == True{} : Bool}:
837	  match r1:
838	    case (+k1, e1):
839	      match r2:
840	        case (+k2, e2):
841	          %Equal.sym(Nat, c, Nat.add(b, k2), e2) : {Nat.is_le(a, _) == True{} : Bool}
842	          %Equal.sym(Nat, b, Nat.add(a, k1), e1) : {Nat.is_le(a, Nat.add(_, k2)) == True{} : Bool}
843	          %Equal.sym(Nat, Nat.add(Nat.add(a, k1), k2), Nat.add(a, Nat.add(k1, k2)), P.add_assoc(a, k1, k2)) :
844	            {Nat.is_le(a, _) == True{} : Bool}
845	          P.le_of_add(a, Nat.add(k1, k2))
846	
847	def le_trans(a, b, c, e1, e2):
848	  le_trans.k(a, b, c, P.le_witness(a, b, e1), P.le_witness(b, c, e2))
849	
850	law add_cancel_l:
851	  for +c: Nat
852	  for +a: Nat
853	  for +b: Nat
854	  for e: {Nat.add(c, a) == Nat.add(c, b) : Nat}
855	  {a == b : Nat}
856	
857	def add_cancel_l(c, a, b, e):
858	  match c:
859	    case 0n:
860	      e
861	    case 1n+k:
862	      add_cancel_l(k, a, b, P.succ_inj(Nat.add(k, a), Nat.add(k, b), e))
863	
864	# ((a+b)+c) + ((a'+b')+c') regrouped as ((a+a')+(b+b')) + (c+c').
865	def swap3(+a: Nat, +b: Nat, +c: Nat, +a2: Nat, +b2: Nat, +c2: Nat) ->
866	  {Nat.add(Nat.add(Nat.add(a, b), c), Nat.add(Nat.add(a2, b2), c2))
867	    == Nat.add(Nat.add(Nat.add(a, a2), Nat.add(b, b2)), Nat.add(c, c2)) : Nat}:
868	  %P.add_swap(a, b, a2, b2) : {Nat.add(Nat.add(Nat.add(a, b), c), Nat.add(Nat.add(a2, b2), c2))
869	    == Nat.add(_, Nat.add(c, c2)) : Nat}
870	  P.add_swap(Nat.add(a, b), c, Nat.add(a2, b2), c2)
871	
872	# Room for n mines and 9 more among the L + O cells, with O <= 9: n <= L.
873	def room_left.k(+l: Nat, +o: Nat, +m: Nat, +n: Nat, e: {Nat.add(l, o) == m : Nat},
874	  wb: P.LeW(o, 9n), wr: P.LeW(Nat.add(n, 9n), m)) -> {Nat.is_le(n, l) == True{} : Bool}:
875	  match wb:
876	    case (+d, eb):
877	      match wr:
878	        case (+k, er):
879	          +dk = Nat.add(d, k)
880	          +t1 = Equal.trans(Nat, Nat.add(o, l), m, Nat.add(Nat.add(n, 9n), k),
881	            Equal.trans(Nat, Nat.add(o, l), Nat.add(l, o), m, P.add_comm(o, l), e), er)
882	          +t2 = Equal.cong(Nat, Nat, x => Nat.add(Nat.add(n, x), k), 9n, Nat.add(o, d), eb)
883	          +t4 = Equal.cong(Nat, Nat, x => Nat.add(n, x), Nat.add(Nat.add(o, d), k), Nat.add(o, dk), P.add_assoc(o, d, k))
884	          +t345 = Equal.trans(Nat, Nat.add(Nat.add(n, Nat.add(o, d)), k), Nat.add(n, Nat.add(Nat.add(o, d), k)),
885	            Nat.add(o, Nat.add(n, dk)), P.add_assoc(n, Nat.add(o, d), k),
886	            Equal.trans(Nat, Nat.add(n, Nat.add(Nat.add(o, d), k)), Nat.add(n, Nat.add(o, dk)), Nat.add(o, Nat.add(n, dk)),
887	              t4, P.add_left_comm(n, o, dk)))
888	          +e3 = Equal.trans(Nat, Nat.add(o, l), Nat.add(Nat.add(n, 9n), k), Nat.add(o, Nat.add(n, dk)), t1,
889	            Equal.trans(Nat, Nat.add(Nat.add(n, 9n), k), Nat.add(Nat.add(n, Nat.add(o, d)), k), Nat.add(o, Nat.add(n, dk)),
890	              t2, t345))
891	          %Equal.sym(Nat, l, Nat.add(n, dk), add_cancel_l(o, l, Nat.add(n, dk), e3)) : {Nat.is_le(n, _) == True{} : Bool}
892	          P.le_of_add(n, dk)
893	
894	def room_left(+l: Nat, +o: Nat, +m: Nat, +n: Nat, e: {Nat.add(l, o) == m : Nat},
895	  r: {Nat.is_le(Nat.add(n, 9n), m) == True{} : Bool}, b: {Nat.is_le(o, 9n) == True{} : Bool}) ->
896	  {Nat.is_le(n, l) == True{} : Bool}:
897	  room_left.k(l, o, m, n, e, P.le_witness(o, 9n, b), P.le_witness(Nat.add(n, 9n), m, r))
898	
899	# At most nine cells near the first click
900	# =======================================
901	
902	# x is within one step of a.
903	def nr(+a: Nat, +x: Nat) -> Bool:
904	  Nat.is_le(B.dist(a, x), 1n)
905	
906	# How many elements of xs are within one step of a.
907	def ncnt(+a: Nat, xs: List<&2, Nat>) -> Nat:
908	  match xs:
909	    case Nil{}:
910	      0n
911	    case x <> t:
912	      Nat.add(one(nr(a, x)), ncnt(a, t))
913	
914	# How many elements of xs are one below a.
915	def cnt1(+a: Nat, xs: List<&2, Nat>) -> Nat:
916	  match xs:
917	    case Nil{}:
918	      0n
919	    case x <> t:
920	      Nat.add(one(Nat.is_eq(1n+x, a)), cnt1(a, t))
921	
922	# Within one step of a means a, a + 1 or a - 1.
923	law near_pt:
924	  for +a: Nat
925	  for +x: Nat
926	  {Nat.is_le(one(nr(a, x)), Nat.add(Nat.add(one(Nat.is_eq(x, a)), one(Nat.is_eq(x, 1n+a))), one(Nat.is_eq(1n+x, a))))
927	    == True{} : Bool}
928	
929	def near_pt.zx(+j: Nat) ->
930	  {Nat.is_le(one(nr(0n, 1n+j)), Nat.add(Nat.add(one(Nat.is_eq(1n+j, 0n)), one(Nat.is_eq(1n+j, 1n))), one(Nat.is_eq(2n+j, 0n))))
931	    == True{} : Bool}:
932	  match j:
933	    case 0n:
934	      {==}
935	    case 1n+i:
936	      P.le_zero_l(Nat.add(Nat.add(one(Nat.is_eq(2n+i, 0n)), one(Nat.is_eq(2n+i, 1n))), one(Nat.is_eq(3n+i, 0n))))
937	
938	def near_pt.xz(+k: Nat) ->
939	  {Nat.is_le(one(nr(1n+k, 0n)), Nat.add(Nat.add(one(Nat.is_eq(0n, 1n+k)), one(Nat.is_eq(0n, 2n+k))), one(Nat.is_eq(1n, 1n+k))))
940	    == True{} : Bool}:
941	  match k:
942	    case 0n:
943	      {==}
944	    case 1n+i:
945	      P.le_zero_l(Nat.add(Nat.add(one(Nat.is_eq(0n, 2n+i)), one(Nat.is_eq(0n, 3n+i))), one(Nat.is_eq(1n, 2n+i))))
946	
947	def near_pt(a, x):
948	  match a x:
949	    case 0n 0n:
950	      {==}
951	    case 0n 1n+j:
952	      near_pt.zx(j)
953	    case 1n+k 0n:
954	      near_pt.xz(k)
955	    case 1n+k 1n+j:
956	      near_pt(k, j)
957	
958	law near_cnt:
959	  for +a: Nat
960	  for +xs: List<&2, Nat>
961	  {Nat.is_le(ncnt(a, xs), Nat.add(Nat.add(cnt(a, xs), cnt(1n+a, xs)), cnt1(a, xs))) == True{} : Bool}
962	
963	def near_cnt(a, xs):
964	  match xs:
965	    case Nil{}:
966	      {==}
967	    case x <> t:
968	      +o1 = one(Nat.is_eq(x, a))
969	      +o2 = one(Nat.is_eq(x, 1n+a))
970	      +o3 = one(Nat.is_eq(1n+x, a))
971	      %swap3(o1, o2, o3, cnt(a, t), cnt(1n+a, t), cnt1(a, t)) :
972	        {Nat.is_le(Nat.add(one(nr(a, x)), ncnt(a, t)), _) == True{} : Bool}
973	      P.le_add(one(nr(a, x)), Nat.add(Nat.add(o1, o2), o3), ncnt(a, t), Nat.add(Nat.add(cnt(a, t), cnt(1n+a, t)), cnt1(a, t)),
974	        near_pt(a, x), near_cnt(a, t))
975	
976	law cnt1_succ:
977	  for +a: Nat
978	  for +xs: List<&2, Nat>
979	  {cnt1(1n+a, xs) == cnt(a, xs) : Nat}
980	
981	def cnt1_succ(a, xs):
982	  match xs:
983	    case Nil{}:
984	      {==}
985	    case x <> t:
986	      %cnt1_succ(a, t) : {Nat.add(one(Nat.is_eq(1n+x, 1n+a)), cnt1(1n+a, t))
987	        == Nat.add(one(Nat.is_eq(x, a)), _) : Nat}
988	      {==}
989	
990	law cnt1_zero:
991	  for +xs: List<&2, Nat>
992	  {cnt1(0n, xs) == 0n : Nat}
993	
994	def cnt1_zero(xs):
995	  match xs:
996	    case Nil{}:
997	      {==}
998	    case x <> t:
999	      cnt1_zero(t)
1000	
1001	def pick_le1(+b: Bool) -> {Nat.is_le(Bool.pick(Nat, b, 1n, 0n), 1n) == True{} : Bool}:
1002	  match b:
1003	    case True{}:
1004	      {==}
1005	    case False{}:
1006	      {==}
1007	
1008	def cnt_le1(+i: Nat, +n: Nat) -> {Nat.is_le(cnt(i, List.range(n)), 1n) == True{} : Bool}:
1009	  %Equal.sym(Nat, cnt(i, List.range(n)), Bool.pick(Nat, Nat.is_lt(i, n), 1n, 0n), cnt_range(i, n)) :
1010	    {Nat.is_le(_, 1n) == True{} : Bool}
1011	  pick_le1(Nat.is_lt(i, n))
1012	
1013	def cnt1_le1(+a: Nat, +n: Nat) -> {Nat.is_le(cnt1(a, List.range(n)), 1n) == True{} : Bool}:
1014	  match a:
1015	    case 0n:
1016	      %Equal.sym(Nat, cnt1(0n, List.range(n)), 0n, cnt1_zero(List.range(n))) : {Nat.is_le(_, 1n) == True{} : Bool}
1017	      {==}
1018	    case 1n+k:
1019	      %Equal.sym(Nat, cnt1(1n+k, List.range(n)), cnt(k, List.range(n)), cnt1_succ(k, List.range(n))) :
1020	        {Nat.is_le(_, 1n) == True{} : Bool}
1021	      cnt_le1(k, n)
1022	
1023	# At most three numbers below n are within one step of a.
1024	law ncnt_le3:
1025	  for +a: Nat
1026	  for +n: Nat
1027	  {Nat.is_le(ncnt(a, List.range(n)), 3n) == True{} : Bool}
1028	
1029	def ncnt_le3(a, n):
1030	  +xs = List.range(n)
1031	  le_trans(ncnt(a, xs), Nat.add(Nat.add(cnt(a, xs), cnt(1n+a, xs)), cnt1(a, xs)), 3n,
1032	    near_cnt(a, xs),
1033	    P.le_add(Nat.add(cnt(a, xs), cnt(1n+a, xs)), 2n, cnt1(a, xs), 1n,
1034	      P.le_add(cnt(a, xs), 1n, cnt(1n+a, xs), 1n, cnt_le1(a, n), cnt_le1(1n+a, n)),
1035	      cnt1_le1(a, n)))
1036	
1037	def wide_row.go(+fx: Nat, +fy: Nat, +y: Nat, +xs: List<&2, Nat>, +b: Bool,
1038	  +e: {nr(fy, y) == b : Bool}) ->
1039	  {outs(G.Zone{T.Pos{fx, fy}, True{}}, B.row_cells(y, xs)) == Bool.pick(Nat, b, ncnt(fx, xs), 0n) : Nat}:
1040	  match xs:
1041	    case Nil{}:
1042	      match b:
1043	        case True{}:
1044	          {==}
1045	        case False{}:
1046	          {==}
1047	    case x <> t:
1048	      %Equal.sym(Bool, nr(fy, y), b, e) :
1049	        {Nat.add(Bool.pick(Nat, Bool.and(nr(fx, x), _), 1n, 0n), outs(G.Zone{T.Pos{fx, fy}, True{}}, B.row_cells(y, t)))
1050	          == Bool.pick(Nat, b, ncnt(fx, x <> t), 0n) : Nat}
1051	      %Equal.sym(Nat, outs(G.Zone{T.Pos{fx, fy}, True{}}, B.row_cells(y, t)), Bool.pick(Nat, b, ncnt(fx, t), 0n),
1052	        wide_row.go(fx, fy, y, t, b, e)) :
1053	        {Nat.add(Bool.pick(Nat, Bool.and(nr(fx, x), b), 1n, 0n), _)
1054	          == Bool.pick(Nat, b, ncnt(fx, x <> t), 0n) : Nat}
1055	      firsts_row.end(nr(fx, x), b, ncnt(fx, t))
1056	
1057	# Each row near the first click's row, counted c times.
1058	def rsum(+fy: Nat, +c: Nat, ys: List<&2, Nat>) -> Nat:
1059	  match ys:
1060	    case Nil{}:
1061	      0n
1062	    case y <> t:
1063	      Nat.add(Bool.pick(Nat, nr(fy, y), c, 0n), rsum(fy, c, t))
1064	
1065	law wide_rows:
1066	  for +fx: Nat
1067	  for +fy: Nat
1068	  for +w: Nat
1069	  for +ys: List<&2, Nat>
1070	  {outs(G.Zone{T.Pos{fx, fy}, True{}}, B.cells.go(w, ys)) == rsum(fy, ncnt(fx, List.range(w)), ys) : Nat}
1071	
1072	def wide_rows(fx, fy, w, ys):
1073	  match ys:
1074	    case Nil{}:
1075	      {==}
1076	    case y <> t:
1077	      +z = {G.Zone{T.Pos{fx, fy}, True{}} : G.Zone}
1078	      +row = B.row_cells(y, List.range(w))
1079	      +c = ncnt(fx, List.range(w))
1080	      %Equal.sym(Nat, outs(z, List.append(&2, T.Pos, row, B.cells.go(w, t))),
1081	        Nat.add(outs(z, row), outs(z, B.cells.go(w, t))), firsts_append(z, row, B.cells.go(w, t))) :
1082	        {_ == rsum(fy, c, y <> t) : Nat}
1083	      %Equal.sym(Nat, outs(z, row), Bool.pick(Nat, nr(fy, y), c, 0n), wide_row.go(fx, fy, y, List.range(w), nr(fy, y), {==})) :
1084	        {Nat.add(_, outs(z, B.cells.go(w, t))) == rsum(fy, c, y <> t) : Nat}
1085	      %Equal.sym(Nat, outs(z, B.cells.go(w, t)), rsum(fy, c, t), wide_rows(fx, fy, w, t)) :
1086	        {Nat.add(Bool.pick(Nat, nr(fy, y), c, 0n), _) == rsum(fy, c, y <> t) : Nat}
1087	      {==}
1088	
1089	def pick_le3(+b: Bool, +c: Nat, lc: {Nat.is_le(c, 3n) == True{} : Bool}) ->
1090	  {Nat.is_le(Bool.pick(Nat, b, c, 0n), Nat.add(Nat.add(one(b), one(b)), one(b))) == True{} : Bool}:
1091	  match b:
1092	    case True{}:
1093	      lc
1094	    case False{}:
1095	      {==}
1096	
1097	law rsum_le:
1098	  for +fy: Nat
1099	  for +c: Nat
1100	  for +ys: List<&2, Nat>
1101	  for +lc: {Nat.is_le(c, 3n) == True{} : Bool}
1102	  {Nat.is_le(rsum(fy, c, ys), Nat.add(Nat.add(ncnt(fy, ys), ncnt(fy, ys)), ncnt(fy, ys))) == True{} : Bool}
1103	
1104	def rsum_le(fy, c, ys, lc):
1105	  match ys:
1106	    case Nil{}:
1107	      {==}
1108	    case y <> t:
1109	      +o = one(nr(fy, y))
1110	      +nt = ncnt(fy, t)
1111	      %swap3(o, o, o, nt, nt, nt) :
1112	        {Nat.is_le(rsum(fy, c, y <> t), _) == True{} : Bool}
1113	      P.le_add(Bool.pick(Nat, nr(fy, y), c, 0n), Nat.add(Nat.add(o, o), o), rsum(fy, c, t), Nat.add(Nat.add(nt, nt), nt),
1114	        pick_le3(nr(fy, y), c, lc), rsum_le(fy, c, t, lc))
1115	
1116	# The zone around a first click holds at most 9 cells of the board.
1117	law wide_le9:
1118	  for +fx: Nat
1119	  for +fy: Nat
1120	  for +w: Nat
1121	  for +h: Nat
1122	  {Nat.is_le(outs(G.Zone{T.Pos{fx, fy}, True{}}, B.cells(w, h)), 9n) == True{} : Bool}
1123	
1124	def wide_le9(fx, fy, w, h):
1125	  +c = ncnt(fx, List.range(w))
1126	  +ny = ncnt(fy, List.range(h))
1127	  %Equal.sym(Nat, outs(G.Zone{T.Pos{fx, fy}, True{}}, B.cells(w, h)), rsum(fy, c, List.range(h)),
1128	    wide_rows(fx, fy, w, List.range(h))) : {Nat.is_le(_, 9n) == True{} : Bool}
1129	  le_trans(rsum(fy, c, List.range(h)), Nat.add(Nat.add(ny, ny), ny), 9n,
1130	    rsum_le(fy, c, List.range(h), ncnt_le3(fx, w)),
1131	    P.le_add(Nat.add(ny, ny), 6n, ny, 3n,
1132	      P.le_add(ny, 3n, ny, 3n, ncnt_le3(fy, h), ncnt_le3(fy, h)), ncnt_le3(fy, h)))
1133	
1134	# Exactly n mines, again
1135	# =====================
1136	
1137	def cells_len(+w: Nat, +h: Nat) -> {List.length(&2, T.Pos, B.cells(w, h)) == Nat.mul(w, h) : Nat}:
1138	  Equal.trans(Nat, List.length(&2, T.Pos, B.cells(w, h)),
1139	    Nat.mul(List.length(&2, Nat, List.range(h)), w), Nat.mul(w, h),
1140	    cells_go_len(w, List.range(h)),
1141	    %Equal.sym(Nat, List.length(&2, Nat, List.range(h)), h, P.range_length(h)) :
1142	      {Nat.mul(_, w) == Nat.mul(w, h) : Nat};
1143	      P.mul_comm(h, w))
1144	
1145	# With just the first click kept free, there are w*h - 1 candidates, so
1146	# n < w*h mines fit among them.
1147	law gen_inv_one:
1148	  for +w: Nat
1149	  for +h: Nat
1150	  for +n: Nat
1151	  for +fx: Nat
1152	  for +fy: Nat
1153	  for +on: {L.on_board(w, h, T.Pos{fx, fy}) == True{} : Bool}
1154	  for fits: {Nat.is_lt(n, Nat.mul(w, h)) == True{} : Bool}
1155	  {Nat.is_le(n, G.gen.left(G.Zone{T.Pos{fx, fy}, False{}}, B.cells(w, h))) == True{} : Bool}
1156	
1157	def gen_inv_one(w, h, n, fx, fy, on, fits):
1158	  +z = {G.Zone{T.Pos{fx, fy}, False{}} : G.Zone}
1159	  +gl = G.gen.left(z, B.cells(w, h))
1160	  +xw = P.and_true_l(Nat.is_lt(fx, w), Nat.is_lt(fy, h), on)
1161	  +yh = P.and_true_r(Nat.is_lt(fx, w), Nat.is_lt(fy, h), on)
1162	  +f1 = Equal.trans(Nat, outs(z, B.cells(w, h)), cnt(fy, List.range(h)), 1n,
1163	    firsts_rows(fx, fy, w, List.range(h), one_when(fx, w, xw)), one_when(fy, h, yh))
1164	  +e1 = {%f1 : {Nat.add(gl, _) == List.length(&2, T.Pos, B.cells(w, h)) : Nat};
1165	    gen_left_firsts(z, B.cells(w, h)) : {Nat.add(gl, 1n) == List.length(&2, T.Pos, B.cells(w, h)) : Nat}}
1166	  +e2 = Equal.trans(Nat, 1n+gl, Nat.add(gl, 1n), Nat.mul(w, h),
1167	    Equal.sym(Nat, Nat.add(gl, 1n), 1n+gl, P.add_one(gl)),
1168	    Equal.trans(Nat, Nat.add(gl, 1n), List.length(&2, T.Pos, B.cells(w, h)), Nat.mul(w, h), e1, cells_len(w, h)))
1169	  P.lt_succ_le(n, gl,
1170	    {%Equal.sym(Nat, 1n+gl, Nat.mul(w, h), e2) : {Nat.is_lt(n, _) == True{} : Bool};
1171	      fits : {Nat.is_lt(n, 1n+gl) == True{} : Bool}})
1172	
1173	# With room for 9 more, n mines fit outside the wider zone.
1174	law gen_inv_wide:
1175	  for +w: Nat
1176	  for +h: Nat
1177	  for +n: Nat
1178	  for +fx: Nat
1179	  for +fy: Nat
1180	  for room: {Nat.is_le(Nat.add(n, 9n), Nat.mul(w, h)) == True{} : Bool}
1181	  {Nat.is_le(n, G.gen.left(G.Zone{T.Pos{fx, fy}, True{}}, B.cells(w, h))) == True{} : Bool}
1182	
1183	def gen_inv_wide(w, h, n, fx, fy, room):
1184	  +z = {G.Zone{T.Pos{fx, fy}, True{}} : G.Zone}
1185	  +gl = G.gen.left(z, B.cells(w, h))
1186	  +o = outs(z, B.cells(w, h))
1187	  room_left(gl, o, Nat.mul(w, h), n,
1188	    Equal.trans(Nat, Nat.add(gl, o), List.length(&2, T.Pos, B.cells(w, h)), Nat.mul(w, h),
1189	      gen_left_firsts(z, B.cells(w, h)), cells_len(w, h)),
1190	    room, wide_le9(fx, fy, w, h))
1191	
1192	def gen_inv.k(+w: Nat, +h: Nat, +n: Nat, +fx: Nat, +fy: Nat,
1193	  +on: {L.on_board(w, h, T.Pos{fx, fy}) == True{} : Bool}, fits: {Nat.is_lt(n, Nat.mul(w, h)) == True{} : Bool},
1194	  +wide: Bool, ew: {Nat.is_le(Nat.add(n, 9n), Nat.mul(w, h)) == wide : Bool}) ->
1195	  {Nat.is_le(n, G.gen.left(G.Zone{T.Pos{fx, fy}, wide}, B.cells(w, h))) == True{} : Bool}:
1196	  match wide:
1197	    case False{}:
1198	      gen_inv_one(w, h, n, fx, fy, on, fits)
1199	    case True{}:
1200	      gen_inv_wide(w, h, n, fx, fy, ew)
1201	
1202	# Whichever zone the board keeps free, the n mines fit outside it.
1203	law gen_inv:
1204	  for +w: Nat
1205	  for +h: Nat
1206	  for +n: Nat
1207	  for +first: T.Pos
1208	  for +on: {L.on_board(w, h, first) == True{} : Bool}
1209	  for fits: {Nat.is_lt(n, Nat.mul(w, h)) == True{} : Bool}
1210	  {Nat.is_le(n, G.gen.left(zone(w, h, n, first), B.cells(w, h))) == True{} : Bool}
1211	
1212	def gen_inv(w, h, n, first, on, fits):
1213	  match first:
1214	    case T.Pos{fx, fy}:
1215	      gen_inv.k(w, h, n, fx, fy, on, fits, Nat.is_le(Nat.add(n, 9n), Nat.mul(w, h)), {==})
1216	
1217	law gen_count_:
1218	  for +w: Nat
1219	  for +h: Nat
1220	  for +n: Nat
1221	  for +first: T.Pos
1222	  for +rs: List<&2, U32>
1223	  for on: {L.on_board(w, h, first) == True{} : Bool}
1224	  for fits: {Nat.is_lt(n, Nat.mul(w, h)) == True{} : Bool}
1225	  {L.total_mines(G.place_mines(w, h, n, first, rs)) == n : Nat}
1226	
1227	def gen_count_(w, h, n, first, rs, on, fits):
1228	  +z = zone(w, h, n, first)
1229	  gen_rows_count(z, w, List.range(h),
1230	    {G.GenState{n, G.gen.left(z, B.cells(w, h)), rs} : G.GenState},
1231	    gen_inv(w, h, n, first, on, fits), {==})