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	import ./proof_flood.bend as PF
13	import ./proof_inv.bend as PI
14	import ./solver.bend as S
15	
16	# Proofs of the laws about real games, from the invariant.
17	
18	def shown_of(g: G.Game) -> T.Grid(Bool):
19	  match g:
20	    case G.Game{w, h, layout, shown, flags, status}:
21	      shown
22	
23	def flags_of(g: G.Game) -> List<&2, T.Pos>:
24	  match g:
25	    case G.Game{w, h, layout, shown, flags, status}:
26	      flags
27	
28	def Canon(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +g: G.Game) -> Type:
29	  {g == G.Game{w, h, layout, shown_of(g), flags_of(g), G.status(g)} : G.Game} &
30	  PI.Facts(w, h, layout, shown_of(g), G.status(g))
31	
32	# A real game in its canonical form, with the facts of the invariant.
33	law canon:
34	  for +w: Nat
35	  for +h: Nat
36	  for +layout: T.Grid(Bool)
37	  for +g: G.Game
38	  for inv: PI.Inv(w, h, layout, g)
39	  Canon(w, h, layout, g)
40	
41	def canon(w, h, layout, g, inv):
42	  match g:
43	    case G.Game{gw, gh, gl, shown, flags, status}:
44	      match inv:
45	        case (ew, rest):
46	          match rest:
47	            case (eh, rest2):
48	              match rest2:
49	                case (el, facts):
50	                  %Equal.sym(Nat, gw, w, ew) :
51	                    {G.Game{_, gh, gl, shown, flags, status} == G.Game{w, h, layout, shown, flags, status} : G.Game} &
52	                    PI.Facts(w, h, layout, shown, status)
53	                  %Equal.sym(Nat, gh, h, eh) :
54	                    {G.Game{w, _, gl, shown, flags, status} == G.Game{w, h, layout, shown, flags, status} : G.Game} &
55	                    PI.Facts(w, h, layout, shown, status)
56	                  %Equal.sym(T.Grid(Bool), gl, layout, el) :
57	                    {G.Game{w, h, _, shown, flags, status} == G.Game{w, h, layout, shown, flags, status} : G.Game} &
58	                    PI.Facts(w, h, layout, shown, status)
59	                  ({==}, facts)
60	
61	# Reading the knowledge of a game
62	# ===============================
63	
64	law know_seen:
65	  for +w: Nat
66	  for +h: Nat
67	  for +layout: T.Grid(Bool)
68	  for +shown: T.Grid(Bool)
69	  for +flags: List<&2, T.Pos>
70	  for +status: T.Status
71	  for +q: T.Pos
72	  for on: {B.on_board(w, h, q) == True{} : Bool}
73	  {L.seen(G.knowledge(G.Game{w, h, layout, shown, flags, status}), q) == G.seen_at(w, h, layout, shown, q) : T.Seen}
74	
75	def know_seen(w, h, layout, shown, flags, status, q, on):
76	  match q:
77	    case T.Pos{x, y}:
78	      PG.know_at(w, h, layout, shown, x, y, on)
79	
80	law revealed_pick:
81	  for +c: Bool
82	  for +m: Bool
83	  for +w: Nat
84	  for +h: Nat
85	  for +layout: T.Grid(Bool)
86	  for +p: T.Pos
87	  {Bool.not(L.is_hidden(G.seen_pick(c, m, w, h, layout, p))) == c : Bool}
88	
89	def revealed_pick(c, m, w, h, layout, p):
90	  match c m:
91	    case False{} _:
92	      {==}
93	    case True{} True{}:
94	      {==}
95	    case True{} False{}:
96	      {==}
97	
98	# On the board, revealed in the knowledge means revealed in the game.
99	law know_revealed:
100	  for +w: Nat
101	  for +h: Nat
102	  for +layout: T.Grid(Bool)
103	  for +shown: T.Grid(Bool)
104	  for +flags: List<&2, T.Pos>
105	  for +status: T.Status
106	  for +q: T.Pos
107	  for +on: {B.on_board(w, h, q) == True{} : Bool}
108	  {L.revealed(G.knowledge(G.Game{w, h, layout, shown, flags, status}), q) == B.at(Bool, False{}, shown, q) : Bool}
109	
110	def know_revealed(w, h, layout, shown, flags, status, q, on):
111	  match q:
112	    case T.Pos{x, y}:
113	      +rows = G.know_rows(w, h, layout, shown, List.range(h))
114	      +p = {T.Pos{x, y} : T.Pos}
115	      %Equal.sym(Bool, B.on_board(w, h, p), True{}, on) :
116	        {Bool.and(_, Bool.not(L.is_hidden(L.at(T.Seen, T.Hidden{}, rows, p)))) == B.at(Bool, False{}, shown, p) : Bool}
117	      %Equal.sym(T.Seen, L.at(T.Seen, T.Hidden{}, rows, p), G.seen_at(w, h, layout, shown, p),
118	        PG.know_at(w, h, layout, shown, x, y, on)) :
119	        {Bool.not(L.is_hidden(_)) == B.at(Bool, False{}, shown, p) : Bool}
120	      revealed_pick(B.at(Bool, False{}, shown, p), B.mine(layout, p), w, h, layout, p)
121	
122	# The real board
123	# ==============
124	
125	law know_row_len:
126	  for +w: Nat
127	  for +h: Nat
128	  for +layout: T.Grid(Bool)
129	  for +shown: T.Grid(Bool)
130	  for +y: Nat
131	  for +xs: List<&2, Nat>
132	  {List.length(&2, T.Seen, G.know_row(w, h, layout, shown, y, xs)) == List.length(&2, Nat, xs) : Nat}
133	
134	def know_row_len(w, h, layout, shown, y, xs):
135	  match xs:
136	    case Nil{}:
137	      {==}
138	    case x <> t:
139	      %Equal.sym(Nat, List.length(&2, T.Seen, G.know_row(w, h, layout, shown, y, t)), List.length(&2, Nat, t),
140	        know_row_len(w, h, layout, shown, y, t)) : {1n+_ == 1n+List.length(&2, Nat, t) : Nat}
141	      {==}
142	
143	law know_rows_len:
144	  for +w: Nat
145	  for +h: Nat
146	  for +layout: T.Grid(Bool)
147	  for +shown: T.Grid(Bool)
148	  for +ys: List<&2, Nat>
149	  {List.length(&2, List<&2, T.Seen>, G.know_rows(w, h, layout, shown, ys)) == List.length(&2, Nat, ys) : Nat}
150	
151	def know_rows_len(w, h, layout, shown, ys):
152	  match ys:
153	    case Nil{}:
154	      {==}
155	    case y <> t:
156	      %Equal.sym(Nat, List.length(&2, List<&2, T.Seen>, G.know_rows(w, h, layout, shown, t)), List.length(&2, Nat, t),
157	        know_rows_len(w, h, layout, shown, t)) : {1n+_ == 1n+List.length(&2, Nat, t) : Nat}
158	      {==}
159	
160	law know_rows_wide:
161	  for +w: Nat
162	  for +h: Nat
163	  for +layout: T.Grid(Bool)
164	  for +shown: T.Grid(Bool)
165	  for +ys: List<&2, Nat>
166	  {L.rows_wide(T.Seen, w, G.know_rows(w, h, layout, shown, ys)) == True{} : Bool}
167	
168	def know_rows_wide(w, h, layout, shown, ys):
169	  match ys:
170	    case Nil{}:
171	      {==}
172	    case y <> t:
173	      +row = G.know_row(w, h, layout, shown, y, List.range(w))
174	      %Equal.sym(Nat, List.length(&2, T.Seen, row), w,
175	        Equal.trans(Nat, List.length(&2, T.Seen, row), List.length(&2, Nat, List.range(w)), w,
176	          know_row_len(w, h, layout, shown, y, List.range(w)), P.range_length(w))) :
177	        {Bool.and(Nat.is_eq(_, w), L.rows_wide(T.Seen, w, G.know_rows(w, h, layout, shown, t))) == True{} : Bool}
178	      %Equal.sym(Bool, Nat.is_eq(w, w), True{}, P.eq_refl(w)) :
179	        {Bool.and(_, L.rows_wide(T.Seen, w, G.know_rows(w, h, layout, shown, t))) == True{} : Bool}
180	      know_rows_wide(w, h, layout, shown, t)
181	
182	law know_shaped:
183	  for +w: Nat
184	  for +h: Nat
185	  for +layout: T.Grid(Bool)
186	  for +shown: T.Grid(Bool)
187	  {L.shaped(T.Seen, w, h, G.know_rows(w, h, layout, shown, List.range(h))) == True{} : Bool}
188	
189	def know_shaped(w, h, layout, shown):
190	  +rows = G.know_rows(w, h, layout, shown, List.range(h))
191	  %Equal.sym(Nat, List.length(&2, List<&2, T.Seen>, rows), h,
192	    Equal.trans(Nat, List.length(&2, List<&2, T.Seen>, rows), List.length(&2, Nat, List.range(h)), h,
193	      know_rows_len(w, h, layout, shown, List.range(h)), P.range_length(h))) :
194	    {Bool.and(Nat.is_eq(_, h), L.rows_wide(T.Seen, w, rows)) == True{} : Bool}
195	  %Equal.sym(Bool, Nat.is_eq(h, h), True{}, P.eq_refl(h)) : {Bool.and(_, L.rows_wide(T.Seen, w, rows)) == True{} : Bool}
196	  know_rows_wide(w, h, layout, shown, List.range(h))
197	
198	def agrees_pick(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +p: T.Pos, +c: Bool, +m: Bool,
199	  me: {B.mine(layout, p) == m : Bool}) ->
200	  {L.agrees(w, h, layout, p, G.seen_pick(c, m, w, h, layout, p)) == True{} : Bool}:
201	  match c m:
202	    case False{} _:
203	      {==}
204	    case True{} True{}:
205	      %PC.mine_eq(layout, p) : {_ == True{} : Bool}
206	      me
207	    case True{} False{}:
208	      %PC.mine_eq(layout, p) :
209	        {Bool.and(Bool.not(_), Nat.is_eq(L.adj_mines(w, h, layout, p), B.adj_mines(w, h, layout, p))) == True{} : Bool}
210	      %Equal.sym(Bool, B.mine(layout, p), False{}, me) :
211	        {Bool.and(Bool.not(_), Nat.is_eq(L.adj_mines(w, h, layout, p), B.adj_mines(w, h, layout, p))) == True{} : Bool}
212	      %PC.adj_mines_eq(w, h, layout, p) :
213	        {Bool.and(True{}, Nat.is_eq(_, B.adj_mines(w, h, layout, p))) == True{} : Bool}
214	      P.eq_refl(B.adj_mines(w, h, layout, p))
215	
216	def agrees_cell(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +shown: T.Grid(Bool), +p: T.Pos,
217	  on: {B.on_board(w, h, p) == True{} : Bool}) ->
218	  {L.agrees(w, h, layout, p, L.at(T.Seen, T.Hidden{}, G.know_rows(w, h, layout, shown, List.range(h)), p)) == True{} : Bool}:
219	  match p:
220	    case T.Pos{x, y}:
221	      +q = {T.Pos{x, y} : T.Pos}
222	      %Equal.sym(T.Seen, L.at(T.Seen, T.Hidden{}, G.know_rows(w, h, layout, shown, List.range(h)), q),
223	        G.seen_at(w, h, layout, shown, q), PG.know_at(w, h, layout, shown, x, y, on)) :
224	        {L.agrees(w, h, layout, q, _) == True{} : Bool}
225	      agrees_pick(w, h, layout, q, B.at(Bool, False{}, shown, q), B.mine(layout, q), {==})
226	
227	def agrees_all_cells(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +shown: T.Grid(Bool), ps: List<&2, T.Pos>,
228	  +ons: {PS.allp(~PS.WH, ~PS.onb, PS.WH{w, h}, ps) == True{} : Bool}) ->
229	  {L.agrees_all(w, h, G.know_rows(w, h, layout, shown, List.range(h)), layout, ps) == True{} : Bool}:
230	  match ps:
231	    case Nil{}:
232	      {==}
233	    case +q <> +t:
234	      +rows = G.know_rows(w, h, layout, shown, List.range(h))
235	      %Equal.sym(Bool, L.agrees(w, h, layout, q, L.at(T.Seen, T.Hidden{}, rows, q)), True{},
236	        agrees_cell(w, h, layout, shown, q, PS.allp_head(~PS.WH, ~PS.onb, PS.WH{w, h}, q, t, ons))) :
237	        {Bool.and(_, L.agrees_all(w, h, rows, layout, t)) == True{} : Bool}
238	      agrees_all_cells(w, h, layout, shown, t, PS.allp_tail(~PS.WH, ~PS.onb, PS.WH{w, h}, q, t, ons))
239	
240	law bridge_canon:
241	  for +w: Nat
242	  for +h: Nat
243	  for +layout: T.Grid(Bool)
244	  for +shown: T.Grid(Bool)
245	  for +flags: List<&2, T.Pos>
246	  for +status: T.Status
247	  for shape: {L.shaped(Bool, w, h, layout) == True{} : Bool}
248	  {L.consistent(G.knowledge(G.Game{w, h, layout, shown, flags, status}), layout) == True{} : Bool}
249	
250	def bridge_canon(w, h, layout, shown, flags, status, shape):
251	  +rows = G.know_rows(w, h, layout, shown, List.range(h))
252	  PW.and4_intro(L.shaped(Bool, w, h, layout), L.shaped(T.Seen, w, h, rows),
253	    Nat.is_eq(L.total_mines(layout), B.total_mines(layout)), L.agrees_all(w, h, rows, layout, L.cells(w, h)),
254	    shape, know_shaped(w, h, layout, shown),
255	    %PC.total_mines_eq(layout) : {Nat.is_eq(_, B.total_mines(layout)) == True{} : Bool};
256	      P.eq_refl(B.total_mines(layout)),
257	    %PC.cells_eq(w, h) : {L.agrees_all(w, h, rows, layout, _) == True{} : Bool};
258	      agrees_all_cells(w, h, layout, shown, B.cells(w, h), PS.cells_on(w, h)))
259	
260	def bridge.k(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +g: G.Game,
261	  shape: {L.shaped(Bool, w, h, layout) == True{} : Bool}, c: Canon(w, h, layout, g)) ->
262	  {L.consistent(G.knowledge(g), layout) == True{} : Bool}:
263	  match c:
264	    case (eg, facts):
265	      %Equal.sym(G.Game, g, G.Game{w, h, layout, shown_of(g), flags_of(g), G.status(g)}, eg) :
266	        {L.consistent(G.knowledge(_), layout) == True{} : Bool}
267	      bridge_canon(w, h, layout, shown_of(g), flags_of(g), G.status(g), shape)
268	
269	law bridge_:
270	  for +w: Nat
271	  for +h: Nat
272	  for +layout: T.Grid(Bool)
273	  for shape: {L.shaped(Bool, w, h, layout) == True{} : Bool}
274	  for +g: G.Game
275	  for r: L.Reachable(w, h, layout, g)
276	  {L.consistent(G.knowledge(g), layout) == True{} : Bool}
277	
278	def bridge_(w, h, layout, shape, g, r):
279	  bridge.k(w, h, layout, g, shape, canon(w, h, layout, g, PI.inv_reach(w, h, layout, g, r)))
280	
281	# Winning
282	# =======
283	
284	def safe_rev_cell(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +shown: T.Grid(Bool), +flags: List<&2, T.Pos>,
285	  +status: T.Status, +q: T.Pos, +on: {B.on_board(w, h, q) == True{} : Bool}) ->
286	  {Bool.or(L.mine(layout, q), L.revealed(G.knowledge(G.Game{w, h, layout, shown, flags, status}), q))
287	    == Bool.or(B.mine(layout, q), B.at(Bool, False{}, shown, q)) : Bool}:
288	  %PC.mine_eq(layout, q) :
289	    {Bool.or(_, L.revealed(G.knowledge(G.Game{w, h, layout, shown, flags, status}), q))
290	      == Bool.or(B.mine(layout, q), B.at(Bool, False{}, shown, q)) : Bool}
291	  %Equal.sym(Bool, L.revealed(G.knowledge(G.Game{w, h, layout, shown, flags, status}), q), B.at(Bool, False{}, shown, q),
292	    know_revealed(w, h, layout, shown, flags, status, q, on)) :
293	    {Bool.or(B.mine(layout, q), _) == Bool.or(B.mine(layout, q), B.at(Bool, False{}, shown, q)) : Bool}
294	  {==}
295	
296	def safe_rev_all(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +shown: T.Grid(Bool), +flags: List<&2, T.Pos>,
297	  +status: T.Status, ps: List<&2, T.Pos>, +ons: {PS.allp(~PS.WH, ~PS.onb, PS.WH{w, h}, ps) == True{} : Bool}) ->
298	  {L.all_safe_revealed.go(G.knowledge(G.Game{w, h, layout, shown, flags, status}), layout, ps)
299	    == G.all_safe.go(layout, shown, ps) : Bool}:
300	  match ps:
301	    case Nil{}:
302	      {==}
303	    case +q <> +t:
304	      +v = G.knowledge(G.Game{w, h, layout, shown, flags, status})
305	      %Equal.sym(Bool, Bool.or(L.mine(layout, q), L.revealed(v, q)), Bool.or(B.mine(layout, q), B.at(Bool, False{}, shown, q)),
306	        safe_rev_cell(w, h, layout, shown, flags, status, q, PS.allp_head(~PS.WH, ~PS.onb, PS.WH{w, h}, q, t, ons))) :
307	        {Bool.and(_, L.all_safe_revealed.go(v, layout, t))
308	          == Bool.and(Bool.or(B.mine(layout, q), B.at(Bool, False{}, shown, q)), G.all_safe.go(layout, shown, t)) : Bool}
309	      %Equal.sym(Bool, L.all_safe_revealed.go(v, layout, t), G.all_safe.go(layout, shown, t),
310	        safe_rev_all(w, h, layout, shown, flags, status, t, PS.allp_tail(~PS.WH, ~PS.onb, PS.WH{w, h}, q, t, ons))) :
311	        {Bool.and(Bool.or(B.mine(layout, q), B.at(Bool, False{}, shown, q)), _)
312	          == Bool.and(Bool.or(B.mine(layout, q), B.at(Bool, False{}, shown, q)), G.all_safe.go(layout, shown, t)) : Bool}
313	      {==}
314	
315	def won_iff.k(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +g: G.Game, c: Canon(w, h, layout, g)) ->
316	  {L.is_won(G.status(g)) == L.all_safe_revealed(G.knowledge(g), layout) : Bool}:
317	  match c:
318	    case (eg, facts):
319	      match facts:
320	        case (sh, f2):
321	          match f2:
322	            case (won, f3):
323	              %Equal.sym(G.Game, g, G.Game{w, h, layout, shown_of(g), flags_of(g), G.status(g)}, eg) :
324	                {L.is_won(G.status(_)) == L.all_safe_revealed(G.knowledge(_), layout) : Bool}
325	              +s = shown_of(g)
326	              +f = flags_of(g)
327	              +st = G.status(g)
328	              %PC.cells_eq(w, h) :
329	                {L.is_won(st) == L.all_safe_revealed.go(G.knowledge(G.Game{w, h, layout, s, f, st}), layout, _) : Bool}
330	              %Equal.sym(Bool, L.all_safe_revealed.go(G.knowledge(G.Game{w, h, layout, s, f, st}), layout, B.cells(w, h)),
331	                G.all_safe.go(layout, s, B.cells(w, h)), safe_rev_all(w, h, layout, s, f, st, B.cells(w, h), PS.cells_on(w, h))) :
332	                {L.is_won(st) == _ : Bool}
333	              won
334	
335	law won_iff_:
336	  for +w: Nat
337	  for +h: Nat
338	  for +layout: T.Grid(Bool)
339	  for shape: {L.shaped(Bool, w, h, layout) == True{} : Bool}
340	  for +g: G.Game
341	  for r: L.Reachable(w, h, layout, g)
342	  {L.is_won(G.status(g)) == L.all_safe_revealed(G.knowledge(g), layout) : Bool}
343	
344	def won_iff_(w, h, layout, shape, g, r):
345	  won_iff.k(w, h, layout, g, canon(w, h, layout, g, PI.inv_reach(w, h, layout, g, r)))
346	
347	# Flags
348	# =====
349	
350	law flags_hidden_:
351	  for +g: G.Game
352	  for +q: T.Pos
353	  for flag: {G.flagged(g, q) == True{} : Bool}
354	  {L.hidden(G.knowledge(g), q) == True{} : Bool}
355	
356	def flags_hidden_(g, q, flag):
357	  match g:
358	    case G.Game{w, h, layout, shown, flags, status}:
359	      %Equal.sym(Bool, L.hidden(G.knowledge(G.Game{w, h, layout, shown, flags, status}), q), G.unrevealed(w, h, shown, q),
360	        PG.know_hidden(w, h, layout, shown, flags, status, q)) : {_ == True{} : Bool}
361	      P.and_true_l(G.unrevealed(w, h, shown, q), B.contains(flags, q), flag)
362	
363	# Revealed cells stay revealed
364	# ============================
365	
366	def open_mono.go(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +shown: T.Grid(Bool), +flags: List<&2, T.Pos>,
367	  +status: T.Status, +p: T.Pos, +q: T.Pos, s: {B.at(Bool, False{}, shown, q) == True{} : Bool}, +c: Bool, +m: Bool) ->
368	  {B.at(Bool, False{}, shown_of(G.open.go(c, m, G.Game{w, h, layout, shown, flags, status}, p)), q) == True{} : Bool}:
369	  match c m:
370	    case False{} _:
371	      s
372	    case True{} True{}:
373	      PF.at_set_mono(shown, p, q, s)
374	    case True{} False{}:
375	      +start = {[G.Work{p, Nil{}}] : List<&2, G.Work>}
376	      PF.flood_mono(B.count_false(shown), start, G.head_hidden(w, h, shown, start), w, h, layout, shown, q, s)
377	
378	law open_mono:
379	  for +g: G.Game
380	  for +p: T.Pos
381	  for +q: T.Pos
382	  for s: {B.at(Bool, False{}, shown_of(g), q) == True{} : Bool}
383	  {B.at(Bool, False{}, shown_of(G.open(g, p)), q) == True{} : Bool}
384	
385	def open_mono(g, p, q, s):
386	  match g:
387	    case G.Game{w, h, layout, shown, flags, status}:
388	      open_mono.go(w, h, layout, shown, flags, status, p, q, s,
389	        Bool.and(G.is_playing(status), G.unrevealed(w, h, shown, p)), B.mine(layout, p))
390	
391	def reveal_mono.go(+g: G.Game, +p: T.Pos, +q: T.Pos, s: {B.at(Bool, False{}, shown_of(g), q) == True{} : Bool}, +f: Bool) ->
392	  {B.at(Bool, False{}, shown_of(G.reveal.go(f, g, p)), q) == True{} : Bool}:
393	  match f:
394	    case True{}:
395	      s
396	    case False{}:
397	      open_mono(g, p, q, s)
398	
399	law reveal_mono:
400	  for +g: G.Game
401	  for +p: T.Pos
402	  for +q: T.Pos
403	  for s: {B.at(Bool, False{}, shown_of(g), q) == True{} : Bool}
404	  {B.at(Bool, False{}, shown_of(G.reveal(g, p)), q) == True{} : Bool}
405	
406	def reveal_mono(g, p, q, s):
407	  reveal_mono.go(g, p, q, s, G.flagged(g, p))
408	
409	law chord_mono:
410	  for +ts: List<&2, T.Pos>
411	  for +g: G.Game
412	  for +q: T.Pos
413	  for s: {B.at(Bool, False{}, shown_of(g), q) == True{} : Bool}
414	  {B.at(Bool, False{}, shown_of(G.chord_play(ts, g)), q) == True{} : Bool}
415	
416	def chord_mono(ts, g, q, s):
417	  match ts:
418	    case Nil{}:
419	      s
420	    case p <> t:
421	      chord_mono(t, G.reveal(g, p), q, reveal_mono(g, p, q, s))
422	
423	def flag_mono.go(+c: Bool, +g: G.Game, +p: T.Pos, +q: T.Pos, s: {B.at(Bool, False{}, shown_of(g), q) == True{} : Bool}) ->
424	  {B.at(Bool, False{}, shown_of(G.flag.go(c, g, p)), q) == True{} : Bool}:
425	  match c:
426	    case False{}:
427	      s
428	    case True{}:
429	      match g:
430	        case G.Game{w, h, layout, shown, flags, status}:
431	          s
432	
433	def assist_mono.safe(+g: G.Game, +q: T.Pos, s: {B.at(Bool, False{}, shown_of(g), q) == True{} : Bool},
434	  +m: Maybe<&2, T.Pos>) -> {B.at(Bool, False{}, shown_of(G.assist.safe(m, g)), q) == True{} : Bool}:
435	  match m:
436	    case None{}:
437	      s
438	    case Some{p}:
439	      open_mono(g, p, q, s)
440	
441	def assist_mono.pick(+r: Maybe<&2, T.Pos>, +g: G.Game, +q: T.Pos, s: {B.at(Bool, False{}, shown_of(g), q) == True{} : Bool}, +k: Nat) ->
442	  {B.at(Bool, False{}, shown_of(G.assist.pick(r, g, k)), q) == True{} : Bool}:
443	  match r:
444	    case Some{x}:
445	      match g:
446	        case G.Game{w, h, layout, shown, flags, status}:
447	          s
448	    case None{}:
449	      assist_mono.safe(g, q, s, G.safe_cell(g, k))
450	
451	def assist_mono.go(+g: G.Game, +q: T.Pos, s: {B.at(Bool, False{}, shown_of(g), q) == True{} : Bool}, +c: Bool, +k: Nat) ->
452	  {B.at(Bool, False{}, shown_of(G.assist.go(c, g, k)), q) == True{} : Bool}:
453	  match c:
454	    case False{}:
455	      s
456	    case True{}:
457	      assist_mono.pick(S.solve(G.knowledge(g)), g, q, s, k)
458	
459	law step_mono:
460	  for +g: G.Game
461	  for +a: T.Action
462	  for +q: T.Pos
463	  for s: {B.at(Bool, False{}, shown_of(g), q) == True{} : Bool}
464	  {B.at(Bool, False{}, shown_of(G.step(g, a)), q) == True{} : Bool}
465	
466	def step_mono(g, a, q, s):
467	  match a:
468	    case T.Reveal{p}:
469	      reveal_mono(g, p, q, s)
470	    case T.Chord{p}:
471	      chord_mono(G.chord_targets(g, p), g, q, s)
472	    case T.Flag{p}:
473	      flag_mono.go(G.can_flag(g, p), g, p, q, s)
474	    case T.Assist{k}:
475	      assist_mono.go(g, q, s, G.is_playing(G.status(g)), k)
476	
477	law inv_of:
478	  for +w: Nat
479	  for +h: Nat
480	  for +layout: T.Grid(Bool)
481	  for +g: G.Game
482	  for +acts: List<&2, T.Action>
483	  for +e: {L.play(acts, G.fresh(w, h, layout)) == g : G.Game}
484	  PI.Inv(w, h, layout, g)
485	
486	def inv_of(w, h, layout, g, acts, e):
487	  %e : PI.Inv(w, h, layout, _)
488	  PI.inv_play(w, h, layout, acts, G.fresh(w, h, layout), PI.inv_fresh(w, h, layout))
489	
490	# A revealed cell of the knowledge is on the board and revealed in the game.
491	def vis_parts(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +s: T.Grid(Bool), +f: List<&2, T.Pos>, +st: T.Status,
492	  +q: T.Pos, vis: {L.revealed(G.knowledge(G.Game{w, h, layout, s, f, st}), q) == True{} : Bool}) ->
493	  {B.on_board(w, h, q) == True{} : Bool}:
494	  match q:
495	    case T.Pos{x, y}:
496	      P.and_true_l(L.on_board(w, h, T.Pos{x, y}),
497	        Bool.not(L.is_hidden(L.at(T.Seen, T.Hidden{}, G.know_rows(w, h, layout, s, List.range(h)), T.Pos{x, y}))), vis)
498	
499	def monotone.k2(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +g: G.Game, +a: T.Action, +q: T.Pos,
500	  vis: {L.revealed(G.knowledge(g), q) == True{} : Bool},
501	  +eg: {g == G.Game{w, h, layout, shown_of(g), flags_of(g), G.status(g)} : G.Game},
502	  eg2: {G.step(g, a) == G.Game{w, h, layout, shown_of(G.step(g, a)), flags_of(G.step(g, a)), G.status(G.step(g, a))} : G.Game}) ->
503	  {L.seen(G.knowledge(G.step(g, a)), q) == L.seen(G.knowledge(g), q) : T.Seen}:
504	  +s1 = shown_of(g)
505	  +f1 = flags_of(g)
506	  +t1 = G.status(g)
507	  +g2 = G.step(g, a)
508	  +s2 = shown_of(g2)
509	  +f2 = flags_of(g2)
510	  +t2 = G.status(g2)
511	  +vis1 = {%eg : {L.revealed(G.knowledge(_), q) == True{} : Bool};
512	    vis : {L.revealed(G.knowledge(G.Game{w, h, layout, s1, f1, t1}), q) == True{} : Bool}}
513	  +on = vis_parts(w, h, layout, s1, f1, t1, q, vis1)
514	  +at1 = {%know_revealed(w, h, layout, s1, f1, t1, q, on) : {_ == True{} : Bool};
515	    vis1 : {B.at(Bool, False{}, s1, q) == True{} : Bool}}
516	  +at2 = step_mono(g, a, q, at1)
517	  %Equal.sym(G.Game, g2, G.Game{w, h, layout, s2, f2, t2}, eg2) :
518	    {L.seen(G.knowledge(_), q) == L.seen(G.knowledge(g), q) : T.Seen}
519	  %Equal.sym(G.Game, g, G.Game{w, h, layout, s1, f1, t1}, eg) :
520	    {L.seen(G.knowledge(G.Game{w, h, layout, s2, f2, t2}), q) == L.seen(G.knowledge(_), q) : T.Seen}
521	  %Equal.sym(T.Seen, L.seen(G.knowledge(G.Game{w, h, layout, s2, f2, t2}), q), G.seen_at(w, h, layout, s2, q),
522	    know_seen(w, h, layout, s2, f2, t2, q, on)) :
523	    {_ == L.seen(G.knowledge(G.Game{w, h, layout, s1, f1, t1}), q) : T.Seen}
524	  %Equal.sym(T.Seen, L.seen(G.knowledge(G.Game{w, h, layout, s1, f1, t1}), q), G.seen_at(w, h, layout, s1, q),
525	    know_seen(w, h, layout, s1, f1, t1, q, on)) :
526	    {G.seen_at(w, h, layout, s2, q) == _ : T.Seen}
527	  %Equal.sym(Bool, B.at(Bool, False{}, s2, q), True{}, at2) :
528	    {G.seen_pick(_, B.mine(layout, q), w, h, layout, q) == G.seen_pick(B.at(Bool, False{}, s1, q), B.mine(layout, q), w, h, layout, q) : T.Seen}
529	  %Equal.sym(Bool, B.at(Bool, False{}, s1, q), True{}, at1) :
530	    {G.seen_pick(True{}, B.mine(layout, q), w, h, layout, q) == G.seen_pick(_, B.mine(layout, q), w, h, layout, q) : T.Seen}
531	  {==}
532	
533	def monotone.k(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +g: G.Game, +a: T.Action, +q: T.Pos,
534	  vis: {L.revealed(G.knowledge(g), q) == True{} : Bool}, c1: Canon(w, h, layout, g),
535	  c2: Canon(w, h, layout, G.step(g, a))) ->
536	  {L.seen(G.knowledge(G.step(g, a)), q) == L.seen(G.knowledge(g), q) : T.Seen}:
537	  match c1:
538	    case (eg, f1):
539	      match c2:
540	        case (eg2, f2):
541	          monotone.k2(w, h, layout, g, a, q, vis, eg, eg2)
542	
543	def monotone.r(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +g: G.Game, +a: T.Action, +q: T.Pos,
544	  vis: {L.revealed(G.knowledge(g), q) == True{} : Bool}, +acts: List<&2, T.Action>,
545	  +e: {L.play(acts, G.fresh(w, h, layout)) == g : G.Game}) ->
546	  {L.seen(G.knowledge(G.step(g, a)), q) == L.seen(G.knowledge(g), q) : T.Seen}:
547	  monotone.k(w, h, layout, g, a, q, vis, canon(w, h, layout, g, inv_of(w, h, layout, g, acts, e)),
548	    canon(w, h, layout, G.step(g, a), PI.inv_step(w, h, layout, g, inv_of(w, h, layout, g, acts, e), a)))
549	
550	law monotone_:
551	  for +w: Nat
552	  for +h: Nat
553	  for +layout: T.Grid(Bool)
554	  for shape: {L.shaped(Bool, w, h, layout) == True{} : Bool}
555	  for +g: G.Game
556	  for r: L.Reachable(w, h, layout, g)
557	  for +a: T.Action
558	  for +q: T.Pos
559	  for vis: {L.revealed(G.knowledge(g), q) == True{} : Bool}
560	  {L.seen(G.knowledge(G.step(g, a)), q) == L.seen(G.knowledge(g), q) : T.Seen}
561	
562	def monotone_(w, h, layout, shape, g, r, a, q, vis):
563	  match r:
564	    case (acts, e):
565	      monotone.r(w, h, layout, g, a, q, vis, acts, e)
566	
567	# Opening cells
568	# =============
569	
570	def mine_on.col(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +x: Nat, +y: Nat,
571	  +sh: {B.shaped(Bool, w, h, layout) == True{} : Bool}, yh: {Nat.is_lt(y, h) == True{} : Bool},
572	  m: {Maybe.default(&2, Bool, List.get(&2, Bool, PL.row_of(Bool, layout, y), x), False{}) == True{} : Bool},
573	  +b: Bool, be: {Nat.is_lt(x, w) == b : Bool}) -> {B.on_board(w, h, T.Pos{x, y}) == True{} : Bool}:
574	  match b:
575	    case True{}:
576	      %Equal.sym(Bool, Nat.is_lt(x, w), True{}, be) : {Bool.and(_, Nat.is_lt(y, h)) == True{} : Bool}
577	      yh
578	    case False{}:
579	      +row = PL.row_of(Bool, layout, y)
580	      Empty.absurd({B.on_board(w, h, T.Pos{x, y}) == True{} : Bool},
581	        P.false_ne_true(%P.get_out(Bool, row, x,
582	          %Equal.sym(Nat, List.length(&2, Bool, row), w, PL.row_in_len(Bool, w, h, layout, y, sh, yh)) :
583	            {Nat.is_lt(x, _) == False{} : Bool}; be) :
584	          {Maybe.default(&2, Bool, _, False{}) == True{} : Bool}; m))
585	
586	def mine_on.row(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +x: Nat, +y: Nat,
587	  +sh: {B.shaped(Bool, w, h, layout) == True{} : Bool},
588	  m: {B.mine(layout, T.Pos{x, y}) == True{} : Bool}, +b: Bool, +be: {Nat.is_lt(y, h) == b : Bool}) ->
589	  {B.on_board(w, h, T.Pos{x, y}) == True{} : Bool}:
590	  match b:
591	    case True{}:
592	      mine_on.col(w, h, layout, x, y, sh, be,
593	        %Equal.sym(Maybe<&2, List<&2, Bool>>, List.get(&2, List<&2, Bool>, layout, y), Some{PL.row_of(Bool, layout, y)},
594	          PL.row_in_get(Bool, w, h, layout, y, sh, be)) :
595	          {Maybe.default(&2, Bool, List.get(&2, Bool, Maybe.default(&2, List<&2, Bool>, _, Nil{}), x), False{}) == True{} : Bool};
596	        m, Nat.is_lt(x, w), {==})
597	    case False{}:
598	      Empty.absurd({B.on_board(w, h, T.Pos{x, y}) == True{} : Bool},
599	        P.false_ne_true(%P.get_out(List<&2, Bool>, layout, y,
600	          %Equal.sym(Nat, List.length(&2, List<&2, Bool>, layout), h, PL.shaped_len(Bool, w, h, layout, sh)) :
601	            {Nat.is_lt(y, _) == False{} : Bool}; be) :
602	          {Maybe.default(&2, Bool, List.get(&2, Bool, Maybe.default(&2, List<&2, Bool>, _, Nil{}), x), False{})
603	            == True{} : Bool}; m))
604	
605	# A mine of a w-by-h layout is on the board.
606	law mine_on:
607	  for +w: Nat
608	  for +h: Nat
609	  for +layout: T.Grid(Bool)
610	  for +sh: {B.shaped(Bool, w, h, layout) == True{} : Bool}
611	  for +p: T.Pos
612	  for m: {B.mine(layout, p) == True{} : Bool}
613	  {B.on_board(w, h, p) == True{} : Bool}
614	
615	def mine_on(w, h, layout, sh, p, m):
616	  match p:
617	    case T.Pos{x, y}:
618	      mine_on.row(w, h, layout, x, y, sh, m, Nat.is_lt(y, h), {==})
619	
620	# In a closed grid, a zero walk from a revealed cell ends at a revealed cell.
621	law path_closed:
622	  for +path: List<&2, T.Pos>
623	  for +w: Nat
624	  for +h: Nat
625	  for +layout: T.Grid(Bool)
626	  for +g: T.Grid(Bool)
627	  for +cl: {PI.closed(w, h, layout, g) == True{} : Bool}
628	  for +s: T.Pos
629	  for +q: T.Pos
630	  for gs: {B.at(Bool, False{}, g, s) == True{} : Bool}
631	  for +wk: {L.zero_walk(path, w, h, layout, s, q) == True{} : Bool}
632	  {B.at(Bool, False{}, g, q) == True{} : Bool}
633	
634	def path_closed(path, w, h, layout, g, cl, s, q, gs, wk):
635	  match path:
636	    case Nil{}:
637	      %PW.lsame_sound(s, q, wk) : {B.at(Bool, False{}, g, _) == True{} : Bool}
638	      gs
639	    case r <> t:
640	      +zs = L.zero(w, h, layout, s)
641	      +sr = L.adjacent(s, r)
642	      +orr = L.on_board(w, h, r)
643	      +rest = L.zero_walk(t, w, h, layout, r, q)
644	      +zsB = {%Equal.sym(Bool, B.zero(w, h, layout, s), L.zero(w, h, layout, s), PC.zero_eq(w, h, layout, s)) :
645	        {_ == True{} : Bool}; PW.and4_a(zs, sr, orr, rest, wk) :
646	        {B.zero(w, h, layout, s) == True{} : Bool}}
647	      +onsB = P.and_true_l(B.on_board(w, h, s), Bool.not(B.mine(layout, s)),
648	        P.and_true_l(Bool.and(B.on_board(w, h, s), Bool.not(B.mine(layout, s))),
649	          Nat.is_eq(B.adj_mines(w, h, layout, s), 0n), zsB))
650	      +rm = PS.neighbours_member(w, h, s, r,
651	        %Equal.sym(Bool, B.on_board(w, h, r), L.on_board(w, h, r), PC.on_board_eq(w, h, r)) :
652	          {_ == True{} : Bool}; PW.and4_c(zs, sr, orr, rest, wk),
653	        %Equal.sym(Bool, B.adjacent(s, r), L.adjacent(s, r), PC.adjacent_eq(s, r)) :
654	          {_ == True{} : Bool}; PW.and4_b(zs, sr, orr, rest, wk))
655	      path_closed(t, w, h, layout, g, cl, r, q,
656	        PI.closed_use(w, h, layout, g, cl, s, onsB, gs, zsB, r, rm), PW.and4_d(zs, sr, orr, rest, wk))
657	
658	def unrev_true(+w: Nat, +h: Nat, +shown: T.Grid(Bool), +p: T.Pos, on: {B.on_board(w, h, p) == True{} : Bool},
659	  hid: {B.at(Bool, False{}, shown, p) == False{} : Bool}) -> {G.unrevealed(w, h, shown, p) == True{} : Bool}:
660	  %Equal.sym(Bool, B.on_board(w, h, p), True{}, on) :
661	    {Bool.and(_, Bool.not(B.at(Bool, False{}, shown, p))) == True{} : Bool}
662	  %Equal.sym(Bool, B.at(Bool, False{}, shown, p), False{}, hid) : {Bool.and(True{}, Bool.not(_)) == True{} : Bool}
663	  {==}
664	
665	def is_lost_wop(+b: Bool) -> {L.is_lost(G.won_or_playing(b)) == False{} : Bool}:
666	  match b:
667	    case True{}:
668	      {==}
669	    case False{}:
670	      {==}
671	
672	def start_ok(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +p: T.Pos) ->
673	  {PF.works_ok({[G.Work{p, Nil{}}] : List<&2, G.Work>}, w, h, layout, p) == True{} : Bool}:
674	  %Equal.sym(Bool, L.same(p, p), True{}, PW.lsame_refl(p)) : {Bool.and(_, True{}) == True{} : Bool}
675	  {==}
676	
677	def start_has(+p: T.Pos) -> {PF.wcontains({[G.Work{p, Nil{}}] : List<&2, G.Work>}, p) == True{} : Bool}:
678	  %Equal.sym(Bool, B.same(p, p), True{}, PG.same_refl(p)) : {Bool.or(_, False{}) == True{} : Bool}
679	  {==}
680	
681	# Opening a mine
682	# --------------
683	
684	law open_mine_c:
685	  for +w: Nat
686	  for +h: Nat
687	  for +layout: T.Grid(Bool)
688	  for +s: T.Grid(Bool)
689	  for +f: List<&2, T.Pos>
690	  for +shL: {B.shaped(Bool, w, h, layout) == True{} : Bool}
691	  for +shS: {B.shaped(Bool, w, h, s) == True{} : Bool}
692	  for +ns: {PI.nsm(w, h, layout, s) == True{} : Bool}
693	  for +p: T.Pos
694	  for +bm: {B.mine(layout, p) == True{} : Bool}
695	  {G.status(G.open(G.Game{w, h, layout, s, f, T.Playing{}}, p)) == T.Lost{T.Exploded{p}} : T.Status} &
696	  {L.seen(G.knowledge(G.open(G.Game{w, h, layout, s, f, T.Playing{}}, p)), p) == T.Boom{} : T.Seen}
697	
698	def open_mine_c(w, h, layout, s, f, shL, shS, ns, p, bm):
699	  +g0 = {G.Game{w, h, layout, s, f, T.Playing{}} : G.Game}
700	  +on = mine_on(w, h, layout, shL, p, bm)
701	  +u = unrev_true(w, h, s, p, on, PI.nsm_use(w, h, layout, s, ns, p, on, bm))
702	  +s2 = B.set_at(Bool, s, p, True{})
703	  %Equal.sym(Bool, G.unrevealed(w, h, s, p), True{}, u) :
704	    {G.status(G.open.go(_, B.mine(layout, p), g0, p)) == T.Lost{T.Exploded{p}} : T.Status} &
705	    {L.seen(G.knowledge(G.open.go(_, B.mine(layout, p), g0, p)), p) == T.Boom{} : T.Seen}
706	  %Equal.sym(Bool, B.mine(layout, p), True{}, bm) :
707	    {G.status(G.open.go(True{}, _, g0, p)) == T.Lost{T.Exploded{p}} : T.Status} &
708	    {L.seen(G.knowledge(G.open.go(True{}, _, g0, p)), p) == T.Boom{} : T.Seen}
709	  ({==},
710	    %Equal.sym(T.Seen, L.seen(G.knowledge(G.Game{w, h, layout, s2, f, T.Lost{T.Exploded{p}}}), p),
711	      G.seen_at(w, h, layout, s2, p), know_seen(w, h, layout, s2, f, T.Lost{T.Exploded{p}}, p, on)) :
712	      {_ == T.Boom{} : T.Seen};
713	    %Equal.sym(Bool, B.at(Bool, False{}, s2, p), True{}, PF.at_set_on(w, h, s, p, shS, on)) :
714	      {G.seen_pick(_, B.mine(layout, p), w, h, layout, p) == T.Boom{} : T.Seen};
715	    %Equal.sym(Bool, B.mine(layout, p), True{}, bm) :
716	      {G.seen_pick(True{}, _, w, h, layout, p) == T.Boom{} : T.Seen};
717	    {==})
718	
719	# Opening a safe cell
720	# -------------------
721	
722	def open_safe_c.go(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +s: T.Grid(Bool), +f: List<&2, T.Pos>, +p: T.Pos,
723	  bm: {B.mine(layout, p) == False{} : Bool}, +c: Bool) ->
724	  {L.is_lost(G.status(G.open.go(c, B.mine(layout, p), G.Game{w, h, layout, s, f, T.Playing{}}, p))) == False{} : Bool}:
725	  match c:
726	    case False{}:
727	      {==}
728	    case True{}:
729	      +g0 = {G.Game{w, h, layout, s, f, T.Playing{}} : G.Game}
730	      %Equal.sym(Bool, B.mine(layout, p), False{}, bm) :
731	        {L.is_lost(G.status(G.open.go(True{}, _, g0, p))) == False{} : Bool}
732	      +start = {[G.Work{p, Nil{}}] : List<&2, G.Work>}
733	      is_lost_wop(G.all_safe(w, h, layout,
734	        G.flood(B.count_false(s), start, G.head_hidden(w, h, s, start), w, h, layout, s)))
735	
736	law open_safe_c:
737	  for +w: Nat
738	  for +h: Nat
739	  for +layout: T.Grid(Bool)
740	  for +s: T.Grid(Bool)
741	  for +f: List<&2, T.Pos>
742	  for +p: T.Pos
743	  for bm: {B.mine(layout, p) == False{} : Bool}
744	  {L.is_lost(G.status(G.open(G.Game{w, h, layout, s, f, T.Playing{}}, p))) == False{} : Bool}
745	
746	def open_safe_c(w, h, layout, s, f, p, bm):
747	  open_safe_c.go(w, h, layout, s, f, p, bm, G.unrevealed(w, h, s, p))
748	
749	# The flood, completely and exactly
750	# ---------------------------------
751	
752	def flood_complete_c.go(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +s: T.Grid(Bool), +f: List<&2, T.Pos>,
753	  +shS: {B.shaped(Bool, w, h, s) == True{} : Bool}, +cl: {PI.closed(w, h, layout, s) == True{} : Bool},
754	  +p: T.Pos, +on: {B.on_board(w, h, p) == True{} : Bool}, +q: T.Pos, +onq: {B.on_board(w, h, q) == True{} : Bool},
755	  +path: List<&2, T.Pos>, +wk: {L.zero_walk(path, w, h, layout, p, q) == True{} : Bool},
756	  +c: Bool, ce: {G.unrevealed(w, h, s, p) == c : Bool}, +m: Bool, me: {B.mine(layout, p) == m : Bool}) ->
757	  {L.revealed(G.knowledge(G.open.go(c, m, G.Game{w, h, layout, s, f, T.Playing{}}, p)), q) == True{} : Bool}:
758	  match c m:
759	    case False{} _:
760	      %Equal.sym(Bool, L.revealed(G.knowledge(G.Game{w, h, layout, s, f, T.Playing{}}), q), B.at(Bool, False{}, s, q),
761	        know_revealed(w, h, layout, s, f, T.Playing{}, q, onq)) : {_ == True{} : Bool}
762	      path_closed(path, w, h, layout, s, cl, p, q, PF.unrev_shown(w, h, s, p, ce, on), wk)
763	    case True{} True{}:
764	      +s2 = B.set_at(Bool, s, p, True{})
765	      %Equal.sym(Bool, L.revealed(G.knowledge(G.Game{w, h, layout, s2, f, T.Lost{T.Exploded{p}}}), q), B.at(Bool, False{}, s2, q),
766	        know_revealed(w, h, layout, s2, f, T.Lost{T.Exploded{p}}, q, onq)) : {_ == True{} : Bool}
767	      path_closed(path, w, h, layout, s2, PI.closed_explode(w, h, layout, s, p, me, cl), p, q,
768	        PF.at_set_on(w, h, s, p, shS, on), wk)
769	    case True{} False{}:
770	      +start = {[G.Work{p, Nil{}}] : List<&2, G.Work>}
771	      +cf = B.count_false(s)
772	      +hh = G.head_hidden(w, h, s, start)
773	      +fl = G.flood(cf, start, hh, w, h, layout, s)
774	      +st = G.won_or_playing(G.all_safe(w, h, layout, fl))
775	      %Equal.sym(Bool, L.revealed(G.knowledge(G.Game{w, h, layout, fl, f, st}), q), B.at(Bool, False{}, fl, q),
776	        know_revealed(w, h, layout, fl, f, st, q, onq)) : {_ == True{} : Bool}
777	      path_closed(path, w, h, layout, fl, PI.closed_flood(cf, start, hh, w, h, layout, s, shS, cl, {==}, {==}), p, q,
778	        PF.flood_work(cf, start, hh, w, h, layout, s, shS, {==}, {==}, p, on, start_has(p)), wk)
779	
780	law flood_complete_c:
781	  for +w: Nat
782	  for +h: Nat
783	  for +layout: T.Grid(Bool)
784	  for +s: T.Grid(Bool)
785	  for +f: List<&2, T.Pos>
786	  for +shS: {B.shaped(Bool, w, h, s) == True{} : Bool}
787	  for +cl: {PI.closed(w, h, layout, s) == True{} : Bool}
788	  for +p: T.Pos
789	  for +on: {L.on_board(w, h, p) == True{} : Bool}
790	  for +q: T.Pos
791	  for +path: List<&2, T.Pos>
792	  for +wk: {L.zero_walk(path, w, h, layout, p, q) == True{} : Bool}
793	  {L.revealed(G.knowledge(G.open(G.Game{w, h, layout, s, f, T.Playing{}}, p)), q) == True{} : Bool}
794	
795	def flood_complete_c(w, h, layout, s, f, shS, cl, p, on, q, path, wk):
796	  +onB = {%Equal.sym(Bool, B.on_board(w, h, p), L.on_board(w, h, p), PC.on_board_eq(w, h, p)) : {_ == True{} : Bool};
797	    on : {B.on_board(w, h, p) == True{} : Bool}}
798	  +onq = {%Equal.sym(Bool, B.on_board(w, h, q), L.on_board(w, h, q), PC.on_board_eq(w, h, q)) : {_ == True{} : Bool};
799	    PW.walk_on(path, w, h, layout, p, q, wk, on) : {B.on_board(w, h, q) == True{} : Bool}}
800	  flood_complete_c.go(w, h, layout, s, f, shS, cl, p, onB, q, onq, path, wk,
801	    G.unrevealed(w, h, s, p), {==}, B.mine(layout, p), {==})
802	
803	def exact_explode(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +s: T.Grid(Bool), +p: T.Pos, +q: T.Pos,
804	  hidq: {B.at(Bool, False{}, s, q) == False{} : Bool},
805	  after: {B.at(Bool, False{}, B.set_at(Bool, s, p, True{}), q) == True{} : Bool},
806	  +b: Bool, be: {B.same(p, q) == b : Bool}) -> PF.Walk(w, h, layout, p, q):
807	  match b:
808	    case True{}:
809	      (Nil{}, %PC.same_eq(p, q) : {_ == True{} : Bool}; be)
810	    case False{}:
811	      PF.both_absurd(PF.Walk(w, h, layout, p, q), B.at(Bool, False{}, s, q), hidq,
812	        %PL.at_set_ne(Bool, s, p, q, True{}, False{}, be) : {_ == True{} : Bool}; after)
813	
814	def flood_exact_c.go(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +s: T.Grid(Bool), +f: List<&2, T.Pos>,
815	  +p: T.Pos, +q: T.Pos, +onq: {B.on_board(w, h, q) == True{} : Bool},
816	  +hidq: {B.at(Bool, False{}, s, q) == False{} : Bool},
817	  +c: Bool, +m: Bool,
818	  after: {L.revealed(G.knowledge(G.open.go(c, m, G.Game{w, h, layout, s, f, T.Playing{}}, p)), q) == True{} : Bool}) ->
819	  PF.Walk(w, h, layout, p, q):
820	  match c m:
821	    case False{} _:
822	      PF.both_absurd(PF.Walk(w, h, layout, p, q), B.at(Bool, False{}, s, q), hidq,
823	        %know_revealed(w, h, layout, s, f, T.Playing{}, q, onq) : {_ == True{} : Bool}; after)
824	    case True{} True{}:
825	      +s2 = B.set_at(Bool, s, p, True{})
826	      exact_explode(w, h, layout, s, p, q, hidq,
827	        %know_revealed(w, h, layout, s2, f, T.Lost{T.Exploded{p}}, q, onq) : {_ == True{} : Bool}; after,
828	        B.same(p, q), {==})
829	    case True{} False{}:
830	      +start = {[G.Work{p, Nil{}}] : List<&2, G.Work>}
831	      +cf = B.count_false(s)
832	      +hh = G.head_hidden(w, h, s, start)
833	      +fl = G.flood(cf, start, hh, w, h, layout, s)
834	      +st = G.won_or_playing(G.all_safe(w, h, layout, fl))
835	      PF.flood_path(cf, start, hh, w, h, layout, s, p, start_ok(w, h, layout, p), q, hidq,
836	        %know_revealed(w, h, layout, fl, f, st, q, onq) : {_ == True{} : Bool}; after)
837	
838	law flood_exact_c:
839	  for +w: Nat
840	  for +h: Nat
841	  for +layout: T.Grid(Bool)
842	  for +s: T.Grid(Bool)
843	  for +f: List<&2, T.Pos>
844	  for +p: T.Pos
845	  for +q: T.Pos
846	  for before: {L.hidden(G.knowledge(G.Game{w, h, layout, s, f, T.Playing{}}), q) == True{} : Bool}
847	  for after: {L.revealed(G.knowledge(G.open(G.Game{w, h, layout, s, f, T.Playing{}}, p)), q) == True{} : Bool}
848	  PF.Walk(w, h, layout, p, q)
849	
850	def flood_exact_c(w, h, layout, s, f, p, q, before, after):
851	  +u = {%PG.know_hidden(w, h, layout, s, f, T.Playing{}, q) : {_ == True{} : Bool};
852	    before : {G.unrevealed(w, h, s, q) == True{} : Bool}}
853	  flood_exact_c.go(w, h, layout, s, f, p, q, PF.unrev_on(w, h, s, q, u), PF.unrev_hidden(w, h, s, q, u),
854	    G.unrevealed(w, h, s, p), B.mine(layout, p), after)
855	
856	# The opening laws for real games
857	# ===============================
858	
859	def open_mine.k(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +g: G.Game,
860	  shape: {L.shaped(Bool, w, h, layout) == True{} : Bool},
861	  +playing: {G.status(g) == T.Playing{} : T.Status}, +p: T.Pos, boom: {L.mine(layout, p) == True{} : Bool},
862	  c: Canon(w, h, layout, g)) ->
863	  {G.status(G.open(g, p)) == T.Lost{T.Exploded{p}} : T.Status} &
864	  {L.seen(G.knowledge(G.open(g, p)), p) == T.Boom{} : T.Seen}:
865	  match c:
866	    case (eg, facts):
867	      match facts:
868	        case (sh, f2):
869	          match f2:
870	            case (won, f3):
871	              match f3:
872	                case (cm, cl):
873	                  +s = shown_of(g)
874	                  +f = flags_of(g)
875	                  %Equal.sym(G.Game, g, G.Game{w, h, layout, s, f, G.status(g)}, eg) :
876	                    {G.status(G.open(_, p)) == T.Lost{T.Exploded{p}} : T.Status} &
877	                    {L.seen(G.knowledge(G.open(_, p)), p) == T.Boom{} : T.Seen}
878	                  %Equal.sym(T.Status, G.status(g), T.Playing{}, playing) :
879	                    {G.status(G.open(G.Game{w, h, layout, s, f, _}, p)) == T.Lost{T.Exploded{p}} : T.Status} &
880	                    {L.seen(G.knowledge(G.open(G.Game{w, h, layout, s, f, _}, p)), p) == T.Boom{} : T.Seen}
881	                  open_mine_c(w, h, layout, s, f,
882	                    %Equal.sym(Bool, B.shaped(Bool, w, h, layout), L.shaped(Bool, w, h, layout), PC.shaped_eq(Bool, w, h, layout)) :
883	                      {_ == True{} : Bool}; shape,
884	                    sh,
885	                    %playing : {PI.calm(_, w, h, layout, s) == True{} : Bool}; cm,
886	                    p,
887	                    %Equal.sym(Bool, B.mine(layout, p), L.mine(layout, p), PC.mine_eq(layout, p)) :
888	                      {_ == True{} : Bool}; boom)
889	
890	law open_mine_:
891	  for +w: Nat
892	  for +h: Nat
893	  for +layout: T.Grid(Bool)
894	  for shape: {L.shaped(Bool, w, h, layout) == True{} : Bool}
895	  for +g: G.Game
896	  for r: L.Reachable(w, h, layout, g)
897	  for +playing: {G.status(g) == T.Playing{} : T.Status}
898	  for +p: T.Pos
899	  for boom: {L.mine(layout, p) == True{} : Bool}
900	  {G.status(G.open(g, p)) == T.Lost{T.Exploded{p}} : T.Status} &
901	  {L.seen(G.knowledge(G.open(g, p)), p) == T.Boom{} : T.Seen}
902	
903	def open_mine_(w, h, layout, shape, g, r, playing, p, boom):
904	  open_mine.k(w, h, layout, g, shape, playing, p, boom, canon(w, h, layout, g, PI.inv_reach(w, h, layout, g, r)))
905	
906	def open_safe.k(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +g: G.Game,
907	  +playing: {G.status(g) == T.Playing{} : T.Status}, +p: T.Pos, safe: {L.mine(layout, p) == False{} : Bool},
908	  c: Canon(w, h, layout, g)) ->
909	  {L.is_lost(G.status(G.open(g, p))) == False{} : Bool}:
910	  match c:
911	    case (eg, facts):
912	      +s = shown_of(g)
913	      +f = flags_of(g)
914	      %Equal.sym(G.Game, g, G.Game{w, h, layout, s, f, G.status(g)}, eg) :
915	        {L.is_lost(G.status(G.open(_, p))) == False{} : Bool}
916	      %Equal.sym(T.Status, G.status(g), T.Playing{}, playing) :
917	        {L.is_lost(G.status(G.open(G.Game{w, h, layout, s, f, _}, p))) == False{} : Bool}
918	      open_safe_c(w, h, layout, s, f, p,
919	        %Equal.sym(Bool, B.mine(layout, p), L.mine(layout, p), PC.mine_eq(layout, p)) :
920	          {_ == False{} : Bool}; safe)
921	
922	law open_safe_:
923	  for +w: Nat
924	  for +h: Nat
925	  for +layout: T.Grid(Bool)
926	  for shape: {L.shaped(Bool, w, h, layout) == True{} : Bool}
927	  for +g: G.Game
928	  for r: L.Reachable(w, h, layout, g)
929	  for +playing: {G.status(g) == T.Playing{} : T.Status}
930	  for +p: T.Pos
931	  for safe: {L.mine(layout, p) == False{} : Bool}
932	  {L.is_lost(G.status(G.open(g, p))) == False{} : Bool}
933	
934	def open_safe_(w, h, layout, shape, g, r, playing, p, safe):
935	  open_safe.k(w, h, layout, g, playing, p, safe, canon(w, h, layout, g, PI.inv_reach(w, h, layout, g, r)))
936	
937	def flood_complete.k(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +g: G.Game,
938	  +playing: {G.status(g) == T.Playing{} : T.Status}, +p: T.Pos, +on: {L.on_board(w, h, p) == True{} : Bool},
939	  +q: T.Pos, +path: List<&2, T.Pos>, +wk: {L.zero_walk(path, w, h, layout, p, q) == True{} : Bool},
940	  c: Canon(w, h, layout, g)) ->
941	  {L.revealed(G.knowledge(G.open(g, p)), q) == True{} : Bool}:
942	  match c:
943	    case (eg, facts):
944	      match facts:
945	        case (sh, f2):
946	          match f2:
947	            case (won, f3):
948	              match f3:
949	                case (cm, cl):
950	                  +s = shown_of(g)
951	                  +f = flags_of(g)
952	                  %Equal.sym(G.Game, g, G.Game{w, h, layout, s, f, G.status(g)}, eg) :
953	                    {L.revealed(G.knowledge(G.open(_, p)), q) == True{} : Bool}
954	                  %Equal.sym(T.Status, G.status(g), T.Playing{}, playing) :
955	                    {L.revealed(G.knowledge(G.open(G.Game{w, h, layout, s, f, _}, p)), q) == True{} : Bool}
956	                  flood_complete_c(w, h, layout, s, f, sh, cl, p, on, q, path, wk)
957	
958	law flood_complete_:
959	  for +w: Nat
960	  for +h: Nat
961	  for +layout: T.Grid(Bool)
962	  for shape: {L.shaped(Bool, w, h, layout) == True{} : Bool}
963	  for +g: G.Game
964	  for r: L.Reachable(w, h, layout, g)
965	  for +playing: {G.status(g) == T.Playing{} : T.Status}
966	  for +p: T.Pos
967	  for +on: {L.on_board(w, h, p) == True{} : Bool}
968	  for +q: T.Pos
969	  for +path: List<&2, T.Pos>
970	  for +wk: {L.zero_walk(path, w, h, layout, p, q) == True{} : Bool}
971	  {L.revealed(G.knowledge(G.open(g, p)), q) == True{} : Bool}
972	
973	def flood_complete_(w, h, layout, shape, g, r, playing, p, on, q, path, wk):
974	  flood_complete.k(w, h, layout, g, playing, p, on, q, path, wk, canon(w, h, layout, g, PI.inv_reach(w, h, layout, g, r)))
975	
976	def flood_exact.k(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +g: G.Game,
977	  +playing: {G.status(g) == T.Playing{} : T.Status}, +p: T.Pos, +q: T.Pos,
978	  before: {L.hidden(G.knowledge(g), q) == True{} : Bool},
979	  after: {L.revealed(G.knowledge(G.open(g, p)), q) == True{} : Bool},
980	  c: Canon(w, h, layout, g)) -> PF.Walk(w, h, layout, p, q):
981	  match c:
982	    case (+eg, facts):
983	      +s = shown_of(g)
984	      +f = flags_of(g)
985	      +gp = {G.Game{w, h, layout, s, f, T.Playing{}} : G.Game}
986	      flood_exact_c(w, h, layout, s, f, p, q,
987	        {%playing : {L.hidden(G.knowledge(G.Game{w, h, layout, s, f, _}), q) == True{} : Bool};
988	          %eg : {L.hidden(G.knowledge(_), q) == True{} : Bool};
989	          before : {L.hidden(G.knowledge(gp), q) == True{} : Bool}},
990	        {%playing : {L.revealed(G.knowledge(G.open(G.Game{w, h, layout, s, f, _}, p)), q) == True{} : Bool};
991	          %eg : {L.revealed(G.knowledge(G.open(_, p)), q) == True{} : Bool};
992	          after : {L.revealed(G.knowledge(G.open(gp, p)), q) == True{} : Bool}})
993	
994	law flood_exact_:
995	  for +w: Nat
996	  for +h: Nat
997	  for +layout: T.Grid(Bool)
998	  for shape: {L.shaped(Bool, w, h, layout) == True{} : Bool}
999	  for +g: G.Game
1000	  for r: L.Reachable(w, h, layout, g)
1001	  for +playing: {G.status(g) == T.Playing{} : T.Status}
1002	  for +p: T.Pos
1003	  for +q: T.Pos
1004	  for before: {L.hidden(G.knowledge(g), q) == True{} : Bool}
1005	  for after: {L.revealed(G.knowledge(G.open(g, p)), q) == True{} : Bool}
1006	  PF.Walk(w, h, layout, p, q)
1007	
1008	def flood_exact_(w, h, layout, shape, g, r, playing, p, q, before, after):
1009	  flood_exact.k(w, h, layout, g, playing, p, q, before, after, canon(w, h, layout, g, PI.inv_reach(w, h, layout, g, r)))