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	import ./proof_copy.bend as PC
9	import ./proof_lists.bend as PL
10	import ./proof_cells.bend as PS
11	import ./proof_walk.bend as PW
12	
13	# Lemmas about the flood (G.flood), for a fixed board w, h, layout.
14	
15	# Reading a revealed cell after setting a cell to True
16	# ===================================================
17	
18	def at_true_self.col(+r: List<&2, Bool>, +x: Nat, +b: Bool,
19	  be: {Nat.is_lt(x, List.length(&2, Bool, r)) == b : Bool},
20	  e: {Maybe.default(&2, Bool, List.get(&2, Bool, r, x), False{}) == True{} : Bool}) ->
21	  {Maybe.default(&2, Bool, List.get(&2, Bool, List.set(&2, Bool, r, x, True{}), x), False{}) == True{} : Bool}:
22	  match b:
23	    case True{}:
24	      %Equal.sym(Maybe<&2, Bool>, List.get(&2, Bool, List.set(&2, Bool, r, x, True{}), x), Some{True{}},
25	        PL.get_set_eq(Bool, r, x, True{}, be)) : {Maybe.default(&2, Bool, _, False{}) == True{} : Bool}
26	      {==}
27	    case False{}:
28	      Empty.absurd({Maybe.default(&2, Bool, List.get(&2, Bool, List.set(&2, Bool, r, x, True{}), x), False{}) == True{} : Bool},
29	        P.false_ne_true(%P.get_out(Bool, r, x, be) :
30	          {Maybe.default(&2, Bool, _, False{}) == True{} : Bool}; e))
31	
32	def at_true_self.row(+g: T.Grid(Bool), +x: Nat, +y: Nat, +b: Bool,
33	  be: {Nat.is_lt(y, List.length(&2, List<&2, Bool>, g)) == b : Bool},
34	  e: {B.at(Bool, False{}, g, T.Pos{x, y}) == True{} : Bool}) ->
35	  {B.at(Bool, False{}, B.set_at(Bool, g, T.Pos{x, y}, True{}), T.Pos{x, y}) == True{} : Bool}:
36	  match b:
37	    case True{}:
38	      +r = PL.row_of(Bool, g, y)
39	      +r2 = List.set(&2, Bool, r, x, True{})
40	      %Equal.sym(Maybe<&2, List<&2, Bool>>, List.get(&2, List<&2, Bool>, List.set(&2, List<&2, Bool>, g, y, r2), y),
41	        Some{r2}, PL.get_set_eq(List<&2, Bool>, g, y, r2, be)) :
42	        {Maybe.default(&2, Bool, List.get(&2, Bool, Maybe.default(&2, List<&2, Bool>, _, Nil{}), x), False{})
43	          == True{} : Bool}
44	      at_true_self.col(r, x, Nat.is_lt(x, List.length(&2, Bool, r)), {==}, e)
45	    case False{}:
46	      Empty.absurd({B.at(Bool, False{}, B.set_at(Bool, g, T.Pos{x, y}, True{}), T.Pos{x, y}) == True{} : Bool},
47	        P.false_ne_true(%P.get_out(List<&2, Bool>, g, y, be) :
48	          {Maybe.default(&2, Bool, List.get(&2, Bool, Maybe.default(&2, List<&2, Bool>, _, Nil{}), x), False{})
49	            == True{} : Bool}; e))
50	
51	law at_true_self:
52	  for +g: T.Grid(Bool)
53	  for +q: T.Pos
54	  for e: {B.at(Bool, False{}, g, q) == True{} : Bool}
55	  {B.at(Bool, False{}, B.set_at(Bool, g, q, True{}), q) == True{} : Bool}
56	
57	def at_true_self(g, q, e):
58	  match q:
59	    case T.Pos{x, y}:
60	      at_true_self.row(g, x, y, Nat.is_lt(y, List.length(&2, List<&2, Bool>, g)), {==}, e)
61	
62	def at_set_mono.go(+g: T.Grid(Bool), +p: T.Pos, +q: T.Pos, e: {B.at(Bool, False{}, g, q) == True{} : Bool},
63	  +b: Bool, be: {B.same(p, q) == b : Bool}) ->
64	  {B.at(Bool, False{}, B.set_at(Bool, g, p, True{}), q) == True{} : Bool}:
65	  match b:
66	    case True{}:
67	      %Equal.sym(T.Pos, p, q, PG.same_sound(p, q, be)) :
68	        {B.at(Bool, False{}, B.set_at(Bool, g, _, True{}), q) == True{} : Bool}
69	      at_true_self(g, q, e)
70	    case False{}:
71	      %Equal.sym(Bool, B.at(Bool, False{}, B.set_at(Bool, g, p, True{}), q), B.at(Bool, False{}, g, q),
72	        PL.at_set_ne(Bool, g, p, q, True{}, False{}, be)) : {_ == True{} : Bool}
73	      e
74	
75	# Revealing a cell keeps every revealed cell revealed.
76	law at_set_mono:
77	  for +g: T.Grid(Bool)
78	  for +p: T.Pos
79	  for +q: T.Pos
80	  for e: {B.at(Bool, False{}, g, q) == True{} : Bool}
81	  {B.at(Bool, False{}, B.set_at(Bool, g, p, True{}), q) == True{} : Bool}
82	
83	def at_set_mono(g, p, q, e):
84	  at_set_mono.go(g, p, q, e, B.same(p, q), {==})
85	
86	# Shape and monotonicity of the flood
87	# ===================================
88	
89	law flood_shaped:
90	  for +n: Nat
91	  for +work: List<&2, G.Work>
92	  for +hd: Bool
93	  for +w: Nat
94	  for +h: Nat
95	  for +layout: T.Grid(Bool)
96	  for +shown: T.Grid(Bool)
97	  for +sh: {B.shaped(Bool, w, h, shown) == True{} : Bool}
98	  {B.shaped(Bool, w, h, G.flood(n, work, hd, w, h, layout, shown)) == True{} : Bool}
99	
100	def flood_shaped(n, work, hd, w, h, layout, shown, sh):
101	  match n:
102	    case 0n:
103	      sh
104	    case 1n+m:
105	      match work:
106	        case Nil{}:
107	          sh
108	        case G.Work{c, back} <> rest:
109	          match hd:
110	            case False{}:
111	              flood_shaped(n, rest, G.head_hidden(w, h, shown, rest), w, h, layout, shown, sh)
112	            case True{}:
113	              +s2 = B.set_at(Bool, shown, c, True{})
114	              +wk = G.push(B.zero(w, h, layout, c), B.neighbours(w, h, c), back, rest)
115	              flood_shaped(m, wk, G.head_hidden(w, h, s2, wk), w, h, layout, s2,
116	                PL.shaped_set(Bool, w, h, shown, c, True{}, sh))
117	
118	law flood_mono:
119	  for +n: Nat
120	  for +work: List<&2, G.Work>
121	  for +hd: Bool
122	  for +w: Nat
123	  for +h: Nat
124	  for +layout: T.Grid(Bool)
125	  for +shown: T.Grid(Bool)
126	  for +q: T.Pos
127	  for +s: {B.at(Bool, False{}, shown, q) == True{} : Bool}
128	  {B.at(Bool, False{}, G.flood(n, work, hd, w, h, layout, shown), q) == True{} : Bool}
129	
130	def flood_mono(n, work, hd, w, h, layout, shown, q, s):
131	  match n:
132	    case 0n:
133	      s
134	    case 1n+m:
135	      match work:
136	        case Nil{}:
137	          s
138	        case G.Work{c, back} <> rest:
139	          match hd:
140	            case False{}:
141	              flood_mono(n, rest, G.head_hidden(w, h, shown, rest), w, h, layout, shown, q, s)
142	            case True{}:
143	              +s2 = B.set_at(Bool, shown, c, True{})
144	              +wk = G.push(B.zero(w, h, layout, c), B.neighbours(w, h, c), back, rest)
145	              flood_mono(m, wk, G.head_hidden(w, h, s2, wk), w, h, layout, s2, q,
146	                at_set_mono(shown, c, q, s))
147	
148	# The work list
149	# =============
150	
151	# Some queued cell is q.
152	def wcontains(ws: List<&2, G.Work>, +q: T.Pos) -> Bool:
153	  match ws:
154	    case Nil{}:
155	      False{}
156	    case G.Work{c, back} <> t:
157	      B.same(c, q) || wcontains(t, q)
158	
159	def wcontains_append_r.go(+c: T.Pos, +xs: List<&2, G.Work>, +ys: List<&2, G.Work>, +q: T.Pos,
160	  ih: {wcontains(List.append(&2, G.Work, xs, ys), q) == True{} : Bool}) ->
161	  {Bool.or(B.same(c, q), wcontains(List.append(&2, G.Work, xs, ys), q)) == True{} : Bool}:
162	  %Equal.sym(Bool, wcontains(List.append(&2, G.Work, xs, ys), q), True{}, ih) :
163	    {Bool.or(B.same(c, q), _) == True{} : Bool}
164	  PS.or_true_r(B.same(c, q))
165	
166	law wcontains_append_r:
167	  for +xs: List<&2, G.Work>
168	  for +ys: List<&2, G.Work>
169	  for +q: T.Pos
170	  for e: {wcontains(ys, q) == True{} : Bool}
171	  {wcontains(List.append(&2, G.Work, xs, ys), q) == True{} : Bool}
172	
173	def wcontains_append_r(xs, ys, q, e):
174	  match xs:
175	    case Nil{}:
176	      e
177	    case G.Work{c, back} <> t:
178	      wcontains_append_r.go(c, t, ys, q, wcontains_append_r(t, ys, q, e))
179	
180	def wcontains_append_l.go(+c: T.Pos, +t: List<&2, G.Work>, +ys: List<&2, G.Work>, +q: T.Pos, +b: Bool,
181	  e: {Bool.or(b, wcontains(t, q)) == True{} : Bool},
182	  ih: {wcontains(t, q) == True{} : Bool} -> {wcontains(List.append(&2, G.Work, t, ys), q) == True{} : Bool}) ->
183	  {Bool.or(b, wcontains(List.append(&2, G.Work, t, ys), q)) == True{} : Bool}:
184	  match b:
185	    case True{}:
186	      {==}
187	    case False{}:
188	      ih(e)
189	
190	law wcontains_append_l:
191	  for +xs: List<&2, G.Work>
192	  for +ys: List<&2, G.Work>
193	  for +q: T.Pos
194	  for e: {wcontains(xs, q) == True{} : Bool}
195	  {wcontains(List.append(&2, G.Work, xs, ys), q) == True{} : Bool}
196	
197	def wcontains_append_l(xs, ys, q, e):
198	  match xs:
199	    case Nil{}:
200	      Empty.absurd({wcontains(ys, q) == True{} : Bool}, P.false_ne_true(e))
201	    case G.Work{c, back} <> t:
202	      wcontains_append_l.go(c, t, ys, q, B.same(c, q), e, et => wcontains_append_l(t, ys, q, et))
203	
204	def wcontains_works.go(+r0: T.Pos, +t: List<&2, T.Pos>, +back: List<&2, T.Pos>, +q: T.Pos, +b: Bool,
205	  e: {Bool.or(b, B.contains(t, q)) == True{} : Bool},
206	  ih: {B.contains(t, q) == True{} : Bool} -> {wcontains(G.works(t, back), q) == True{} : Bool}) ->
207	  {Bool.or(b, wcontains(G.works(t, back), q)) == True{} : Bool}:
208	  match b:
209	    case True{}:
210	      {==}
211	    case False{}:
212	      ih(e)
213	
214	law wcontains_works:
215	  for +ns: List<&2, T.Pos>
216	  for +back: List<&2, T.Pos>
217	  for +q: T.Pos
218	  for e: {B.contains(ns, q) == True{} : Bool}
219	  {wcontains(G.works(ns, back), q) == True{} : Bool}
220	
221	def wcontains_works(ns, back, q, e):
222	  match ns:
223	    case Nil{}:
224	      Empty.absurd({wcontains(Nil{}, q) == True{} : Bool}, P.false_ne_true(e))
225	    case r <> t:
226	      wcontains_works.go(r, t, back, q, B.same(r, q), e, et => wcontains_works(t, back, q, et))
227	
228	law push_keeps:
229	  for +z: Bool
230	  for +ns: List<&2, T.Pos>
231	  for +back: List<&2, T.Pos>
232	  for +rest: List<&2, G.Work>
233	  for +q: T.Pos
234	  for e: {wcontains(rest, q) == True{} : Bool}
235	  {wcontains(G.push(z, ns, back, rest), q) == True{} : Bool}
236	
237	def push_keeps(z, ns, back, rest, q, e):
238	  match z:
239	    case True{}:
240	      wcontains_append_r(G.works(ns, back), rest, q, e)
241	    case False{}:
242	      e
243	
244	# Unrevealed cells
245	# ================
246	
247	law unrev_on:
248	  for +w: Nat
249	  for +h: Nat
250	  for +shown: T.Grid(Bool)
251	  for +c: T.Pos
252	  for e: {G.unrevealed(w, h, shown, c) == True{} : Bool}
253	  {B.on_board(w, h, c) == True{} : Bool}
254	
255	def unrev_on(w, h, shown, c, e):
256	  P.and_true_l(B.on_board(w, h, c), Bool.not(B.at(Bool, False{}, shown, c)), e)
257	
258	law unrev_hidden:
259	  for +w: Nat
260	  for +h: Nat
261	  for +shown: T.Grid(Bool)
262	  for +c: T.Pos
263	  for e: {G.unrevealed(w, h, shown, c) == True{} : Bool}
264	  {B.at(Bool, False{}, shown, c) == False{} : Bool}
265	
266	def unrev_hidden(w, h, shown, c, e):
267	  P.not_true(B.at(Bool, False{}, shown, c),
268	    P.and_true_r(B.on_board(w, h, c), Bool.not(B.at(Bool, False{}, shown, c)), e))
269	
270	law unrev_shown:
271	  for +w: Nat
272	  for +h: Nat
273	  for +shown: T.Grid(Bool)
274	  for +c: T.Pos
275	  for e: {G.unrevealed(w, h, shown, c) == False{} : Bool}
276	  for on: {B.on_board(w, h, c) == True{} : Bool}
277	  {B.at(Bool, False{}, shown, c) == True{} : Bool}
278	
279	def unrev_shown(w, h, shown, c, e, on):
280	  P.not_false(B.at(Bool, False{}, shown, c),
281	    %on : {Bool.and(_, Bool.not(B.at(Bool, False{}, shown, c))) == False{} : Bool}; e)
282	
283	law count_after:
284	  for +w: Nat
285	  for +h: Nat
286	  for +shown: T.Grid(Bool)
287	  for +c: T.Pos
288	  for +m: Nat
289	  for +sh: {B.shaped(Bool, w, h, shown) == True{} : Bool}
290	  for +u: {G.unrevealed(w, h, shown, c) == True{} : Bool}
291	  for cnt: {1n+m == B.count_false(shown) : Nat}
292	  {m == B.count_false(B.set_at(Bool, shown, c, True{})) : Nat}
293	
294	def count_after(w, h, shown, c, m, sh, u, cnt):
295	  match c:
296	    case T.Pos{x, y}:
297	      P.succ_inj(m, B.count_false(B.set_at(Bool, shown, T.Pos{x, y}, True{})),
298	        Equal.trans(Nat, 1n+m, B.count_false(shown), 1n+B.count_false(B.set_at(Bool, shown, T.Pos{x, y}, True{})),
299	          cnt, PL.count_false_set(w, h, shown, x, y, sh, unrev_on(w, h, shown, T.Pos{x, y}, u),
300	            unrev_hidden(w, h, shown, T.Pos{x, y}, u))))
301	
302	law at_set_on:
303	  for +w: Nat
304	  for +h: Nat
305	  for +shown: T.Grid(Bool)
306	  for +c: T.Pos
307	  for +sh: {B.shaped(Bool, w, h, shown) == True{} : Bool}
308	  for on: {B.on_board(w, h, c) == True{} : Bool}
309	  {B.at(Bool, False{}, B.set_at(Bool, shown, c, True{}), c) == True{} : Bool}
310	
311	def at_set_on(w, h, shown, c, sh, on):
312	  match c:
313	    case T.Pos{x, y}:
314	      PL.at_set_eq(Bool, w, h, shown, x, y, True{}, False{}, sh, on)
315	
316	law cf_zero:
317	  for +w: Nat
318	  for +h: Nat
319	  for +shown: T.Grid(Bool)
320	  for +q: T.Pos
321	  for +sh: {B.shaped(Bool, w, h, shown) == True{} : Bool}
322	  for on: {B.on_board(w, h, q) == True{} : Bool}
323	  for z: {0n == B.count_false(shown) : Nat}
324	  {B.at(Bool, False{}, shown, q) == True{} : Bool}
325	
326	def cf_zero(w, h, shown, q, sh, on, z):
327	  match q:
328	    case T.Pos{x, y}:
329	      PL.count_false_zero(w, h, shown, x, y, sh, on, Equal.sym(Nat, 0n, B.count_false(shown), z))
330	
331	# Every queued cell of the board
332	# ==============================
333	
334	def flood_work.skip(+n: Nat, +c: T.Pos, +rest: List<&2, G.Work>, +w: Nat, +h: Nat, +layout: T.Grid(Bool),
335	  +shown: T.Grid(Bool), +q: T.Pos, on: {B.on_board(w, h, q) == True{} : Bool},
336	  he: {G.unrevealed(w, h, shown, c) == False{} : Bool}, +b: Bool, be: {B.same(c, q) == b : Bool},
337	  m: {Bool.or(b, wcontains(rest, q)) == True{} : Bool},
338	  ih: {wcontains(rest, q) == True{} : Bool} ->
339	    {B.at(Bool, False{}, G.flood(n, rest, G.head_hidden(w, h, shown, rest), w, h, layout, shown), q) == True{} : Bool}) ->
340	  {B.at(Bool, False{}, G.flood(n, rest, G.head_hidden(w, h, shown, rest), w, h, layout, shown), q) == True{} : Bool}:
341	  match b:
342	    case True{}:
343	      +cq = PG.same_sound(c, q, be)
344	      flood_mono(n, rest, G.head_hidden(w, h, shown, rest), w, h, layout, shown, q,
345	        unrev_shown(w, h, shown, q, %cq : {G.unrevealed(w, h, shown, _) == False{} : Bool}; he, on))
346	    case False{}:
347	      ih(m)
348	
349	def flood_work.take(+m: Nat, +c: T.Pos, +wk: List<&2, G.Work>, +rest: List<&2, G.Work>, +w: Nat, +h: Nat,
350	  +layout: T.Grid(Bool), +shown: T.Grid(Bool), +q: T.Pos,
351	  +sh: {B.shaped(Bool, w, h, shown) == True{} : Bool},
352	  he: {G.unrevealed(w, h, shown, c) == True{} : Bool},
353	  keep: {wcontains(rest, q) == True{} : Bool} -> {wcontains(wk, q) == True{} : Bool},
354	  +b: Bool, be: {B.same(c, q) == b : Bool}, m2: {Bool.or(b, wcontains(rest, q)) == True{} : Bool},
355	  ih: {wcontains(wk, q) == True{} : Bool} ->
356	    {B.at(Bool, False{}, G.flood(m, wk, G.head_hidden(w, h, B.set_at(Bool, shown, c, True{}), wk), w, h, layout,
357	      B.set_at(Bool, shown, c, True{})), q) == True{} : Bool}) ->
358	  {B.at(Bool, False{}, G.flood(m, wk, G.head_hidden(w, h, B.set_at(Bool, shown, c, True{}), wk), w, h, layout,
359	    B.set_at(Bool, shown, c, True{})), q) == True{} : Bool}:
360	  match b:
361	    case True{}:
362	      +cq = PG.same_sound(c, q, be)
363	      +s2 = B.set_at(Bool, shown, c, True{})
364	      flood_mono(m, wk, G.head_hidden(w, h, s2, wk), w, h, layout, s2, q,
365	        %cq : {B.at(Bool, False{}, s2, _) == True{} : Bool};
366	        at_set_on(w, h, shown, c, sh, unrev_on(w, h, shown, c, he)))
367	    case False{}:
368	      ih(keep(m2))
369	
370	# A queued cell of the board ends up revealed (given n counts the
371	# unrevealed cells).
372	law flood_work:
373	  for +n: Nat
374	  for +work: List<&2, G.Work>
375	  for +hd: Bool
376	  for +w: Nat
377	  for +h: Nat
378	  for +layout: T.Grid(Bool)
379	  for +shown: T.Grid(Bool)
380	  for +sh: {B.shaped(Bool, w, h, shown) == True{} : Bool}
381	  for +cnt: {n == B.count_false(shown) : Nat}
382	  for +he: {G.head_hidden(w, h, shown, work) == hd : Bool}
383	  for +q: T.Pos
384	  for +on: {B.on_board(w, h, q) == True{} : Bool}
385	  for m: {wcontains(work, q) == True{} : Bool}
386	  {B.at(Bool, False{}, G.flood(n, work, hd, w, h, layout, shown), q) == True{} : Bool}
387	
388	def flood_work(n, work, hd, w, h, layout, shown, sh, cnt, he, q, on, m):
389	  match n:
390	    case 0n:
391	      cf_zero(w, h, shown, q, sh, on, cnt)
392	    case 1n+k:
393	      match work:
394	        case Nil{}:
395	          Empty.absurd({B.at(Bool, False{}, shown, q) == True{} : Bool}, P.false_ne_true(m))
396	        case G.Work{c, back} <> rest:
397	          match hd:
398	            case False{}:
399	              flood_work.skip(n, c, rest, w, h, layout, shown, q, on, he, B.same(c, q), {==}, m,
400	                mr => flood_work(n, rest, G.head_hidden(w, h, shown, rest), w, h, layout, shown, sh, cnt, {==},
401	                  q, on, mr))
402	            case True{}:
403	              +s2 = B.set_at(Bool, shown, c, True{})
404	              +z = B.zero(w, h, layout, c)
405	              +ns = B.neighbours(w, h, c)
406	              +wk = G.push(z, ns, back, rest)
407	              flood_work.take(k, c, wk, rest, w, h, layout, shown, q, sh, he,
408	                mr => push_keeps(z, ns, back, rest, q, mr), B.same(c, q), {==}, m,
409	                mw => flood_work(k, wk, G.head_hidden(w, h, s2, wk), w, h, layout, s2,
410	                  PL.shaped_set(Bool, w, h, shown, c, True{}, sh), count_after(w, h, shown, c, k, sh, he, cnt),
411	                  {==}, q, on, mw))
412	
413	# A newly revealed zero has its neighbours revealed
414	# =================================================
415	
416	def both_absurd(-A: Type, +a: Bool, e1: {a == False{} : Bool}, e2: {a == True{} : Bool}) -> A:
417	  Empty.absurd(A, P.false_ne_true(Equal.trans(Bool, False{}, a, True{}, Equal.sym(Bool, a, False{}, e1), e2)))
418	
419	def flood_zero.take(+k: Nat, +c: T.Pos, +back: List<&2, T.Pos>, +rest: List<&2, G.Work>, +w: Nat, +h: Nat,
420	  +layout: T.Grid(Bool), +shown: T.Grid(Bool), +q: T.Pos, +r: T.Pos,
421	  +sh: {B.shaped(Bool, w, h, shown) == True{} : Bool},
422	  +cnt: {1n+k == B.count_false(shown) : Nat},
423	  +he: {G.unrevealed(w, h, shown, c) == True{} : Bool},
424	  before: {B.at(Bool, False{}, shown, q) == False{} : Bool},
425	  z: {B.zero(w, h, layout, q) == True{} : Bool},
426	  +rm: {B.contains(B.neighbours(w, h, q), r) == True{} : Bool},
427	  +b: Bool, +be: {B.same(c, q) == b : Bool},
428	  ih: {B.at(Bool, False{}, B.set_at(Bool, shown, c, True{}), q) == False{} : Bool} ->
429	    {B.at(Bool, False{}, G.flood(k, G.push(B.zero(w, h, layout, c), B.neighbours(w, h, c), back, rest),
430	      G.head_hidden(w, h, B.set_at(Bool, shown, c, True{}), G.push(B.zero(w, h, layout, c), B.neighbours(w, h, c), back, rest)),
431	      w, h, layout, B.set_at(Bool, shown, c, True{})), r) == True{} : Bool}) ->
432	  {B.at(Bool, False{}, G.flood(k, G.push(B.zero(w, h, layout, c), B.neighbours(w, h, c), back, rest),
433	    G.head_hidden(w, h, B.set_at(Bool, shown, c, True{}), G.push(B.zero(w, h, layout, c), B.neighbours(w, h, c), back, rest)),
434	    w, h, layout, B.set_at(Bool, shown, c, True{})), r) == True{} : Bool}:
435	  match b:
436	    case True{}:
437	      %Equal.sym(T.Pos, c, q, PG.same_sound(c, q, be)) :
438	        {B.at(Bool, False{}, G.flood(k, G.push(B.zero(w, h, layout, _), B.neighbours(w, h, _), back, rest),
439	          G.head_hidden(w, h, B.set_at(Bool, shown, _, True{}), G.push(B.zero(w, h, layout, _), B.neighbours(w, h, _), back, rest)),
440	          w, h, layout, B.set_at(Bool, shown, _, True{})), r) == True{} : Bool}
441	      %Equal.sym(Bool, B.zero(w, h, layout, q), True{}, z) :
442	        {B.at(Bool, False{}, G.flood(k, G.push(_, B.neighbours(w, h, q), back, rest),
443	          G.head_hidden(w, h, B.set_at(Bool, shown, q, True{}), G.push(_, B.neighbours(w, h, q), back, rest)),
444	          w, h, layout, B.set_at(Bool, shown, q, True{})), r) == True{} : Bool}
445	      +s2 = B.set_at(Bool, shown, q, True{})
446	      +wk = List.append(&2, G.Work, G.works(B.neighbours(w, h, q), back), rest)
447	      +hq = {%PG.same_sound(c, q, be) : {G.unrevealed(w, h, shown, _) == True{} : Bool};
448	        he : {G.unrevealed(w, h, shown, q) == True{} : Bool}}
449	      +ron = P.and_true_r(B.adjacent(q, r), B.on_board(w, h, r),
450	        PS.allp_member(~PS.WHS, ~PS.adj_on, PS.WHS{w, h, q}, B.neighbours(w, h, q), r,
451	          PS.neighbours_all(w, h, q), rm))
452	      flood_work(k, wk, G.head_hidden(w, h, s2, wk), w, h, layout, s2,
453	        PL.shaped_set(Bool, w, h, shown, q, True{}, sh), count_after(w, h, shown, q, k, sh, hq, cnt), {==}, r, ron,
454	        wcontains_append_l(G.works(B.neighbours(w, h, q), back), rest, r,
455	          wcontains_works(B.neighbours(w, h, q), back, r, rm)))
456	    case False{}:
457	      ih(%Equal.sym(Bool, B.at(Bool, False{}, B.set_at(Bool, shown, c, True{}), q), B.at(Bool, False{}, shown, q),
458	        PL.at_set_ne(Bool, shown, c, q, True{}, False{}, be)) : {_ == False{} : Bool}; before)
459	
460	law flood_zero:
461	  for +n: Nat
462	  for +work: List<&2, G.Work>
463	  for +hd: Bool
464	  for +w: Nat
465	  for +h: Nat
466	  for +layout: T.Grid(Bool)
467	  for +shown: T.Grid(Bool)
468	  for +sh: {B.shaped(Bool, w, h, shown) == True{} : Bool}
469	  for +cnt: {n == B.count_false(shown) : Nat}
470	  for +he: {G.head_hidden(w, h, shown, work) == hd : Bool}
471	  for +q: T.Pos
472	  for +before: {B.at(Bool, False{}, shown, q) == False{} : Bool}
473	  for +after: {B.at(Bool, False{}, G.flood(n, work, hd, w, h, layout, shown), q) == True{} : Bool}
474	  for +z: {B.zero(w, h, layout, q) == True{} : Bool}
475	  for +r: T.Pos
476	  for +rm: {B.contains(B.neighbours(w, h, q), r) == True{} : Bool}
477	  {B.at(Bool, False{}, G.flood(n, work, hd, w, h, layout, shown), r) == True{} : Bool}
478	
479	def flood_zero(n, work, hd, w, h, layout, shown, sh, cnt, he, q, before, after, z, r, rm):
480	  match n:
481	    case 0n:
482	      both_absurd({B.at(Bool, False{}, shown, r) == True{} : Bool}, B.at(Bool, False{}, shown, q), before, after)
483	    case 1n+k:
484	      match work:
485	        case Nil{}:
486	          both_absurd({B.at(Bool, False{}, shown, r) == True{} : Bool}, B.at(Bool, False{}, shown, q), before, after)
487	        case G.Work{c, back} <> rest:
488	          match hd:
489	            case False{}:
490	              flood_zero(n, rest, G.head_hidden(w, h, shown, rest), w, h, layout, shown, sh, cnt, {==}, q,
491	                before, after, z, r, rm)
492	            case True{}:
493	              +s2 = B.set_at(Bool, shown, c, True{})
494	              +wk = G.push(B.zero(w, h, layout, c), B.neighbours(w, h, c), back, rest)
495	              flood_zero.take(k, c, back, rest, w, h, layout, shown, q, r, sh, cnt, he, before, z, rm,
496	                B.same(c, q), {==},
497	                b2 => flood_zero(k, wk, G.head_hidden(w, h, s2, wk), w, h, layout, s2,
498	                  PL.shaped_set(Bool, w, h, shown, c, True{}, sh), count_after(w, h, shown, c, k, sh, he, cnt),
499	                  {==}, q, b2, after, z, r, rm))
500	
501	# Every newly revealed cell has a zero walk from the first cell
502	# =============================================================
503	
504	# Each queued cell's ghost path is a zero walk from p0 to it.
505	def works_ok(ws: List<&2, G.Work>, +w: Nat, +h: Nat, +layout: T.Grid(Bool), +p0: T.Pos) -> Bool:
506	  match ws:
507	    case Nil{}:
508	      True{}
509	    case G.Work{c, back} <> t:
510	      L.zero_walk(List.reverse(&2, T.Pos, back), w, h, layout, p0, c) && works_ok(t, w, h, layout, p0)
511	
512	law works_ok_append:
513	  for +xs: List<&2, G.Work>
514	  for +ys: List<&2, G.Work>
515	  for +w: Nat
516	  for +h: Nat
517	  for +layout: T.Grid(Bool)
518	  for +p0: T.Pos
519	  for +a: {works_ok(xs, w, h, layout, p0) == True{} : Bool}
520	  for b: {works_ok(ys, w, h, layout, p0) == True{} : Bool}
521	  {works_ok(List.append(&2, G.Work, xs, ys), w, h, layout, p0) == True{} : Bool}
522	
523	def works_ok_append(xs, ys, w, h, layout, p0, a, b):
524	  match xs:
525	    case Nil{}:
526	      b
527	    case G.Work{c, back} <> t:
528	      +hd = L.zero_walk(List.reverse(&2, T.Pos, back), w, h, layout, p0, c)
529	      %Equal.sym(Bool, hd, True{}, P.and_true_l(hd, works_ok(t, w, h, layout, p0), a)) :
530	        {Bool.and(_, works_ok(List.append(&2, G.Work, t, ys), w, h, layout, p0)) == True{} : Bool}
531	      works_ok_append(t, ys, w, h, layout, p0, P.and_true_r(hd, works_ok(t, w, h, layout, p0), a), b)
532	
533	law works_ok_works:
534	  for +ns: List<&2, T.Pos>
535	  for +back: List<&2, T.Pos>
536	  for +c: T.Pos
537	  for +w: Nat
538	  for +h: Nat
539	  for +layout: T.Grid(Bool)
540	  for +p0: T.Pos
541	  for +okc: {L.zero_walk(List.reverse(&2, T.Pos, back), w, h, layout, p0, c) == True{} : Bool}
542	  for +zc: {L.zero(w, h, layout, c) == True{} : Bool}
543	  for +adj: {PS.allp(~PS.WHS, ~PS.adj_on, PS.WHS{w, h, c}, ns) == True{} : Bool}
544	  {works_ok(G.works(ns, back), w, h, layout, p0) == True{} : Bool}
545	
546	def works_ok_works(ns, back, c, w, h, layout, p0, okc, zc, adj):
547	  match ns:
548	    case Nil{}:
549	      {==}
550	    case r <> t:
551	      +ar = PS.allp_head(~PS.WHS, ~PS.adj_on, PS.WHS{w, h, c}, r, t, adj)
552	      +a1 = P.and_true_l(B.adjacent(c, r), B.on_board(w, h, r), ar)
553	      +a2 = P.and_true_r(B.adjacent(c, r), B.on_board(w, h, r), ar)
554	      +wr = PW.walk_snoc(List.reverse(&2, T.Pos, back), w, h, layout, p0, c, r, okc, zc,
555	        %PC.adjacent_eq(c, r) : {_ == True{} : Bool}; a1,
556	        %PC.on_board_eq(w, h, r) : {_ == True{} : Bool}; a2)
557	      %Equal.sym(Bool, L.zero_walk(List.reverse(&2, T.Pos, r <> back), w, h, layout, p0, r), True{},
558	        %Equal.sym(List<&2, T.Pos>, List.reverse(&2, T.Pos, r <> back),
559	          List.append(&2, T.Pos, List.reverse(&2, T.Pos, back), [r]), PW.rev_cons(T.Pos, r, back)) :
560	          {L.zero_walk(_, w, h, layout, p0, r) == True{} : Bool}; wr) :
561	        {Bool.and(_, works_ok(G.works(t, back), w, h, layout, p0)) == True{} : Bool}
562	      works_ok_works(t, back, c, w, h, layout, p0, okc, zc,
563	        PS.allp_tail(~PS.WHS, ~PS.adj_on, PS.WHS{w, h, c}, r, t, adj))
564	
565	def works_ok_push(+z: Bool, +c: T.Pos, +back: List<&2, T.Pos>, +rest: List<&2, G.Work>, +w: Nat, +h: Nat,
566	  +layout: T.Grid(Bool), +p0: T.Pos, ze: {B.zero(w, h, layout, c) == z : Bool},
567	  okc: {L.zero_walk(List.reverse(&2, T.Pos, back), w, h, layout, p0, c) == True{} : Bool},
568	  okr: {works_ok(rest, w, h, layout, p0) == True{} : Bool}) ->
569	  {works_ok(G.push(z, B.neighbours(w, h, c), back, rest), w, h, layout, p0) == True{} : Bool}:
570	  match z:
571	    case True{}:
572	      works_ok_append(G.works(B.neighbours(w, h, c), back), rest, w, h, layout, p0,
573	        works_ok_works(B.neighbours(w, h, c), back, c, w, h, layout, p0, okc,
574	          %PC.zero_eq(w, h, layout, c) : {_ == True{} : Bool}; ze,
575	          PS.neighbours_all(w, h, c)), okr)
576	    case False{}:
577	      okr
578	
579	def Walk(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +p0: T.Pos, +q: T.Pos) -> Type:
580	  Exists(List<&2, T.Pos>, path => {L.zero_walk(path, w, h, layout, p0, q) == True{} : Bool})
581	
582	def flood_path.take(+c: T.Pos, +back: List<&2, T.Pos>, +rest: List<&2, G.Work>, +w: Nat, +h: Nat,
583	  +layout: T.Grid(Bool), +shown: T.Grid(Bool), +p0: T.Pos, +q: T.Pos,
584	  +ok: {Bool.and(L.zero_walk(List.reverse(&2, T.Pos, back), w, h, layout, p0, c), works_ok(rest, w, h, layout, p0)) == True{} : Bool},
585	  before: {B.at(Bool, False{}, shown, q) == False{} : Bool}, +b: Bool, be: {B.same(c, q) == b : Bool},
586	  ih: {works_ok(G.push(B.zero(w, h, layout, c), B.neighbours(w, h, c), back, rest), w, h, layout, p0) == True{} : Bool} ->
587	    {B.at(Bool, False{}, B.set_at(Bool, shown, c, True{}), q) == False{} : Bool} -> Walk(w, h, layout, p0, q)) ->
588	  Walk(w, h, layout, p0, q):
589	  match b:
590	    case True{}:
591	      +hd = L.zero_walk(List.reverse(&2, T.Pos, back), w, h, layout, p0, c)
592	      +okc = P.and_true_l(hd, works_ok(rest, w, h, layout, p0), ok)
593	      (List.reverse(&2, T.Pos, back),
594	        %PG.same_sound(c, q, be) : {L.zero_walk(List.reverse(&2, T.Pos, back), w, h, layout, p0, _) == True{} : Bool};
595	        okc)
596	    case False{}:
597	      +hd = L.zero_walk(List.reverse(&2, T.Pos, back), w, h, layout, p0, c)
598	      +okc = P.and_true_l(hd, works_ok(rest, w, h, layout, p0), ok)
599	      ih(works_ok_push(B.zero(w, h, layout, c), c, back, rest, w, h, layout, p0, {==}, okc,
600	          P.and_true_r(hd, works_ok(rest, w, h, layout, p0), ok)),
601	        %Equal.sym(Bool, B.at(Bool, False{}, B.set_at(Bool, shown, c, True{}), q), B.at(Bool, False{}, shown, q),
602	          PL.at_set_ne(Bool, shown, c, q, True{}, False{}, be)) : {_ == False{} : Bool}; before)
603	
604	law flood_path:
605	  for +n: Nat
606	  for +work: List<&2, G.Work>
607	  for +hd: Bool
608	  for +w: Nat
609	  for +h: Nat
610	  for +layout: T.Grid(Bool)
611	  for +shown: T.Grid(Bool)
612	  for +p0: T.Pos
613	  for +ok: {works_ok(work, w, h, layout, p0) == True{} : Bool}
614	  for +q: T.Pos
615	  for +before: {B.at(Bool, False{}, shown, q) == False{} : Bool}
616	  for +after: {B.at(Bool, False{}, G.flood(n, work, hd, w, h, layout, shown), q) == True{} : Bool}
617	  Walk(w, h, layout, p0, q)
618	
619	def flood_path(n, work, hd, w, h, layout, shown, p0, ok, q, before, after):
620	  match n:
621	    case 0n:
622	      both_absurd(Walk(w, h, layout, p0, q), B.at(Bool, False{}, shown, q), before, after)
623	    case 1n+k:
624	      match work:
625	        case Nil{}:
626	          both_absurd(Walk(w, h, layout, p0, q), B.at(Bool, False{}, shown, q), before, after)
627	        case G.Work{c, back} <> rest:
628	          match hd:
629	            case False{}:
630	              flood_path(n, rest, G.head_hidden(w, h, shown, rest), w, h, layout, shown, p0,
631	                P.and_true_r(L.zero_walk(List.reverse(&2, T.Pos, back), w, h, layout, p0, c),
632	                  works_ok(rest, w, h, layout, p0), ok), q, before, after)
633	            case True{}:
634	              +s2 = B.set_at(Bool, shown, c, True{})
635	              +wk = G.push(B.zero(w, h, layout, c), B.neighbours(w, h, c), back, rest)
636	              flood_path.take(c, back, rest, w, h, layout, shown, p0, q, ok, before, B.same(c, q), {==},
637	                okw => b2 => flood_path(k, wk, G.head_hidden(w, h, s2, wk), w, h, layout, s2, p0, okw, q, b2, after))