1	import Base
2	import ./types.bend as T
3	import ./board.bend as B
4	import ./game.bend as G
5	import ./solver.bend as S
6	import ./LAWS.bend as L
7	import ./proof_base.bend as P
8	import ./proof_grid.bend as PG
9	import ./proof_copy.bend as PC
10	import ./proof_cells.bend as PS
11	import ./proof_inv.bend as PI
12	import ./proof_laws.bend as PW
13	import ./proof_solver.bend as PV
14	
15	# Proofs of the two assist laws.
16	
17	# A safe hidden cell, while one exists
18	# ====================================
19	
20	def not_and_false(+a: Bool, +b: Bool, e: {Bool.and(Bool.not(a), Bool.not(b)) == False{} : Bool}) ->
21	  {Bool.or(a, b) == True{} : Bool}:
22	  match a b:
23	    case True{} _:
24	      {==}
25	    case False{} True{}:
26	      {==}
27	    case False{} False{}:
28	      Empty.absurd({False{} == True{} : Bool}, P.true_ne_false(e))
29	
30	def SafeAt(+layout: T.Grid(Bool), +shown: T.Grid(Bool), +ps: List<&2, T.Pos>) -> Type:
31	  Exists(T.Pos, p => {G.first_safe(layout, shown, ps) == Some{p} : Maybe<&2, T.Pos>} &
32	    ({Bool.and(Bool.not(B.mine(layout, p)), Bool.not(B.at(Bool, False{}, shown, p))) == True{} : Bool} &
33	     {B.contains(ps, p) == True{} : Bool}))
34	
35	def first_safe.lift(+layout: T.Grid(Bool), +shown: T.Grid(Bool), +q: T.Pos, +t: List<&2, T.Pos>,
36	  r: SafeAt(layout, shown, t), -hit: Bool, he: {hit == False{} : Bool}) ->
37	  Exists(T.Pos, p => {G.first_safe.go(q <> t, hit, layout, shown) == Some{p} : Maybe<&2, T.Pos>} &
38	    ({Bool.and(Bool.not(B.mine(layout, p)), Bool.not(B.at(Bool, False{}, shown, p))) == True{} : Bool} &
39	     {B.contains(q <> t, p) == True{} : Bool})):
40	  match r:
41	    case (+p, pr):
42	      match pr:
43	        case (fe, rest):
44	          match rest:
45	            case (sf, m):
46	              %Equal.sym(Bool, hit, False{}, he) :
47	                Exists(T.Pos, p2 => {G.first_safe.go(q <> t, _, layout, shown) == Some{p2} : Maybe<&2, T.Pos>} &
48	                  ({Bool.and(Bool.not(B.mine(layout, p2)), Bool.not(B.at(Bool, False{}, shown, p2))) == True{} : Bool} &
49	                   {B.contains(q <> t, p2) == True{} : Bool}))
50	              (p, (fe, (sf, PV.or_r(B.same(q, p), B.contains(t, p), m))))
51	
52	def first_safe.go2(+layout: T.Grid(Bool), +shown: T.Grid(Bool), +q: T.Pos, +t: List<&2, T.Pos>, +hit: Bool,
53	  he: {Bool.and(Bool.not(B.mine(layout, q)), Bool.not(B.at(Bool, False{}, shown, q))) == hit : Bool},
54	  e: {Bool.and(Bool.or(B.mine(layout, q), B.at(Bool, False{}, shown, q)), G.all_safe.go(layout, shown, t)) == False{} : Bool},
55	  ih: {G.all_safe.go(layout, shown, t) == False{} : Bool} -> SafeAt(layout, shown, t)) ->
56	  Exists(T.Pos, p => {G.first_safe.go(q <> t, hit, layout, shown) == Some{p} : Maybe<&2, T.Pos>} &
57	    ({Bool.and(Bool.not(B.mine(layout, p)), Bool.not(B.at(Bool, False{}, shown, p))) == True{} : Bool} &
58	     {B.contains(q <> t, p) == True{} : Bool})):
59	  match hit:
60	    case True{}:
61	      (q, ({==}, (he, PV.or_l(B.same(q, q), B.contains(t, q), PG.same_refl(q)))))
62	    case False{}:
63	      first_safe.lift(layout, shown, q, t,
64	        ih(%not_and_false(B.mine(layout, q), B.at(Bool, False{}, shown, q), he) :
65	            {Bool.and(_, G.all_safe.go(layout, shown, t)) == False{} : Bool}; e),
66	        False{}, {==})
67	
68	# While some safe cell is unrevealed, first_safe finds one.
69	law first_safe_some:
70	  for +layout: T.Grid(Bool)
71	  for +shown: T.Grid(Bool)
72	  for +ps: List<&2, T.Pos>
73	  for e: {G.all_safe.go(layout, shown, ps) == False{} : Bool}
74	  SafeAt(layout, shown, ps)
75	
76	def first_safe_some(layout, shown, ps, e):
77	  match ps:
78	    case Nil{}:
79	      Empty.absurd(SafeAt(layout, shown, Nil{}), P.true_ne_false(e))
80	    case q <> t:
81	      first_safe.go2(layout, shown, q, t,
82	        Bool.and(Bool.not(B.mine(layout, q)), Bool.not(B.at(Bool, False{}, shown, q))), {==}, e,
83	        et => first_safe_some(layout, shown, t, et))
84	
85	# Where the assist looks
86	# ======================
87	
88	law all_safe_append:
89	  for +layout: T.Grid(Bool)
90	  for +shown: T.Grid(Bool)
91	  for +xs: List<&2, T.Pos>
92	  for +ys: List<&2, T.Pos>
93	  for e: {G.all_safe.go(layout, shown, ys) == False{} : Bool}
94	  {G.all_safe.go(layout, shown, List.append(&2, T.Pos, xs, ys)) == False{} : Bool}
95	
96	def all_safe_append(layout, shown, xs, ys, e):
97	  match xs:
98	    case Nil{}:
99	      e
100	    case +p <> t:
101	      %Equal.sym(Bool, G.all_safe.go(layout, shown, List.append(&2, T.Pos, t, ys)), False{},
102	        all_safe_append(layout, shown, t, ys, e)) :
103	        {Bool.and(Bool.or(B.mine(layout, p), B.at(Bool, False{}, shown, p)), _) == False{} : Bool}
104	      P.and_false_r(Bool.or(B.mine(layout, p), B.at(Bool, False{}, shown, p)))
105	
106	law on_drop:
107	  for +w: Nat
108	  for +h: Nat
109	  for +ps: List<&2, T.Pos>
110	  for +i: Nat
111	  for +on: {PS.allp(~PS.WH, ~PS.onb, PS.WH{w, h}, ps) == True{} : Bool}
112	  {PS.allp(~PS.WH, ~PS.onb, PS.WH{w, h}, List.drop(&2, T.Pos, ps, i)) == True{} : Bool}
113	
114	def on_drop(w, h, ps, i, on):
115	  match ps i:
116	    case Nil{} _:
117	      {==}
118	    case q <> t 0n:
119	      on
120	    case q <> t 1n+j:
121	      on_drop(w, h, t, j, PS.allp_tail(~PS.WH, ~PS.onb, PS.WH{w, h}, q, t, on))
122	
123	law on_take:
124	  for +w: Nat
125	  for +h: Nat
126	  for +ps: List<&2, T.Pos>
127	  for +i: Nat
128	  for +on: {PS.allp(~PS.WH, ~PS.onb, PS.WH{w, h}, ps) == True{} : Bool}
129	  {PS.allp(~PS.WH, ~PS.onb, PS.WH{w, h}, List.take(&2, T.Pos, ps, i)) == True{} : Bool}
130	
131	def on_take(w, h, ps, i, on):
132	  match ps i:
133	    case Nil{} _:
134	      {==}
135	    case q <> t 0n:
136	      {==}
137	    case q <> t 1n+j:
138	      %Equal.sym(Bool, PS.allp(~PS.WH, ~PS.onb, PS.WH{w, h}, List.take(&2, T.Pos, t, j)), True{},
139	        on_take(w, h, t, j, PS.allp_tail(~PS.WH, ~PS.onb, PS.WH{w, h}, q, t, on))) :
140	        {Bool.and(PS.onb(PS.WH{w, h}, q), _) == True{} : Bool}
141	      %Equal.sym(Bool, PS.onb(PS.WH{w, h}, q), True{}, PS.allp_head(~PS.WH, ~PS.onb, PS.WH{w, h}, q, t, on)) :
142	        {Bool.and(_, True{}) == True{} : Bool}
143	      {==}
144	
145	def on_turn(+w: Nat, +h: Nat, +ps: List<&2, T.Pos>, +k: Nat,
146	  +on: {PS.allp(~PS.WH, ~PS.onb, PS.WH{w, h}, ps) == True{} : Bool}) ->
147	  {PS.allp(~PS.WH, ~PS.onb, PS.WH{w, h}, G.turn(ps, k)) == True{} : Bool}:
148	  +i = Nat.mod(k, Nat.add(List.length(&2, T.Pos, ps), 1n))
149	  PS.allp_append(~PS.WH, ~PS.onb, PS.WH{w, h}, List.drop(&2, T.Pos, ps, i), List.take(&2, T.Pos, ps, i),
150	    on_drop(w, h, ps, i, on), on_take(w, h, ps, i, on))
151	
152	def on_put(+w: Nat, +h: Nat, +p: T.Pos, +t: List<&2, T.Pos>, +b: Bool,
153	  hd: {PS.onb(PS.WH{w, h}, p) == True{} : Bool}, tl: {PS.allp(~PS.WH, ~PS.onb, PS.WH{w, h}, t) == True{} : Bool}) ->
154	  {PS.allp(~PS.WH, ~PS.onb, PS.WH{w, h}, List.filter.put(T.Pos, p, t, b)) == True{} : Bool}:
155	  match b:
156	    case False{}:
157	      tl
158	    case True{}:
159	      %Equal.sym(Bool, PS.allp(~PS.WH, ~PS.onb, PS.WH{w, h}, t), True{}, tl) :
160	        {Bool.and(PS.onb(PS.WH{w, h}, p), _) == True{} : Bool}
161	      %Equal.sym(Bool, PS.onb(PS.WH{w, h}, p), True{}, hd) : {Bool.and(_, True{}) == True{} : Bool}
162	      {==}
163	
164	law on_edges:
165	  for +w: Nat
166	  for +h: Nat
167	  for +shown: T.Grid(Bool)
168	  for +ps: List<&2, T.Pos>
169	  for +on: {PS.allp(~PS.WH, ~PS.onb, PS.WH{w, h}, ps) == True{} : Bool}
170	  {PS.allp(~PS.WH, ~PS.onb, PS.WH{w, h}, G.edges(w, h, shown, ps)) == True{} : Bool}
171	
172	def on_edges(w, h, shown, ps, on):
173	  match ps:
174	    case Nil{}:
175	      {==}
176	    case +p <> +t:
177	      on_put(w, h, p, G.edges(w, h, shown, t),
178	        Bool.and(Bool.not(B.at(Bool, False{}, shown, p)), G.any_shown(shown, B.neighbours(w, h, p))),
179	        PS.allp_head(~PS.WH, ~PS.onb, PS.WH{w, h}, p, t, on),
180	        on_edges(w, h, shown, t, PS.allp_tail(~PS.WH, ~PS.onb, PS.WH{w, h}, p, t, on)))
181	
182	# Every cell the assist may look at is on the board.
183	def on_list(+w: Nat, +h: Nat, +shown: T.Grid(Bool), +k: Nat) ->
184	  {PS.allp(~PS.WH, ~PS.onb, PS.WH{w, h}, G.safe_list(w, h, shown, k)) == True{} : Bool}:
185	  +cs = B.cells(w, h)
186	  +es = G.edges(w, h, shown, cs)
187	  PS.allp_append(~PS.WH, ~PS.onb, PS.WH{w, h}, G.turn(es, k), List.append(&2, T.Pos, G.turn(cs, k), cs),
188	    on_turn(w, h, es, k, on_edges(w, h, shown, cs, PS.cells_on(w, h))),
189	    PS.allp_append(~PS.WH, ~PS.onb, PS.WH{w, h}, G.turn(cs, k), cs, on_turn(w, h, cs, k, PS.cells_on(w, h)), PS.cells_on(w, h)))
190	
191	# While a safe cell is hidden, the assist's list holds one.
192	def nos_list(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +shown: T.Grid(Bool), +k: Nat,
193	  nos: {G.all_safe(w, h, layout, shown) == False{} : Bool}) ->
194	  {G.all_safe.go(layout, shown, G.safe_list(w, h, shown, k)) == False{} : Bool}:
195	  +cs = B.cells(w, h)
196	  all_safe_append(layout, shown, G.turn(G.edges(w, h, shown, cs), k), List.append(&2, T.Pos, G.turn(cs, k), cs),
197	    all_safe_append(layout, shown, G.turn(cs, k), cs, nos))
198	
199	# Pressing the assist when stuck
200	# ==============================
201	
202	def stuck_pick.none(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +s: T.Grid(Bool), +f: List<&2, T.Pos>, +k: Nat,
203	  sa: SafeAt(layout, s, G.safe_list(w, h, s, k))) ->
204	  Exists(T.Pos, p => {L.mine(layout, p) == False{} : Bool} &
205	    ({L.hidden(G.knowledge(G.Game{w, h, layout, s, f, T.Playing{}}), p) == True{} : Bool} &
206	     {G.assist.safe(G.first_safe(layout, s, G.safe_list(w, h, s, k)), G.Game{w, h, layout, s, f, T.Playing{}})
207	       == G.open(G.Game{w, h, layout, s, f, T.Playing{}}, p) : G.Game})):
208	  match sa:
209	    case (+p, pr):
210	      match pr:
211	        case (+fe, rest):
212	          match rest:
213	            case (+sf, m):
214	              +g0 = {G.Game{w, h, layout, s, f, T.Playing{}} : G.Game}
215	              +nm = P.not_true(B.mine(layout, p), P.and_true_l(Bool.not(B.mine(layout, p)), Bool.not(B.at(Bool, False{}, s, p)), sf))
216	              +onp = PS.allp_member(~PS.WH, ~PS.onb, PS.WH{w, h}, G.safe_list(w, h, s, k), p, on_list(w, h, s, k), m)
217	              (p,
218	                (%PC.mine_eq(layout, p) : {_ == False{} : Bool}; nm,
219	                 (%Equal.sym(Bool, L.hidden(G.knowledge(g0), p), G.unrevealed(w, h, s, p),
220	                    PG.know_hidden(w, h, layout, s, f, T.Playing{}, p)) : {_ == True{} : Bool};
221	                    %Equal.sym(Bool, B.on_board(w, h, p), True{}, onp) :
222	                      {Bool.and(_, Bool.not(B.at(Bool, False{}, s, p))) == True{} : Bool};
223	                    P.and_true_r(Bool.not(B.mine(layout, p)), Bool.not(B.at(Bool, False{}, s, p)), sf),
224	                  %Equal.sym(Maybe<&2, T.Pos>, G.first_safe(layout, s, G.safe_list(w, h, s, k)), Some{p}, fe) :
225	                    {G.assist.safe(_, g0) == G.open(g0, p) : G.Game};
226	                  {==})))
227	
228	def stuck_pick(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +s: T.Grid(Bool), +f: List<&2, T.Pos>,
229	  +nos: {G.all_safe(w, h, layout, s) == False{} : Bool},
230	  stuck: L.Stuck(G.knowledge(G.Game{w, h, layout, s, f, T.Playing{}})),
231	  +r: Maybe<&2, T.Pos>, re: {S.solve(G.knowledge(G.Game{w, h, layout, s, f, T.Playing{}})) == r : Maybe<&2, T.Pos>}, +k: Nat) ->
232	  Exists(T.Pos, p => {L.mine(layout, p) == False{} : Bool} &
233	    ({L.hidden(G.knowledge(G.Game{w, h, layout, s, f, T.Playing{}}), p) == True{} : Bool} &
234	     {G.assist.pick(r, G.Game{w, h, layout, s, f, T.Playing{}}, k) == G.open(G.Game{w, h, layout, s, f, T.Playing{}}, p) : G.Game})):
235	  match r:
236	    case Some{q}:
237	      +k0 = G.knowledge(G.Game{w, h, layout, s, f, T.Playing{}})
238	      Empty.absurd(Exists(T.Pos, p => {L.mine(layout, p) == False{} : Bool} &
239	        ({L.hidden(k0, p) == True{} : Bool} &
240	         {G.assist.pick(Some{q}, G.Game{w, h, layout, s, f, T.Playing{}}, k) == G.open(G.Game{w, h, layout, s, f, T.Playing{}}, p) : G.Game})),
241	        stuck(q, PV.solve_safe(k0, q, re)))
242	    case None{}:
243	      stuck_pick.none(w, h, layout, s, f, k, first_safe_some(layout, s, G.safe_list(w, h, s, k), nos_list(w, h, layout, s, k, nos)))
244	
245	def assist_stuck.k(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +g: G.Game,
246	  +playing: {G.status(g) == T.Playing{} : T.Status}, stuck: L.Stuck(G.knowledge(g)), +k: Nat, c: PW.Canon(w, h, layout, g)) ->
247	  Exists(T.Pos, p => {L.mine(layout, p) == False{} : Bool} &
248	    ({L.hidden(G.knowledge(g), p) == True{} : Bool} & {G.step(g, T.Assist{k}) == G.open(g, p) : G.Game})):
249	  match c:
250	    case (+eg, facts):
251	      match facts:
252	        case (sh, f2):
253	          match f2:
254	            case (won, f3):
255	              +s = PW.shown_of(g)
256	              +f = PW.flags_of(g)
257	              +gp = {G.Game{w, h, layout, s, f, T.Playing{}} : G.Game}
258	              %Equal.sym(G.Game, g, G.Game{w, h, layout, s, f, G.status(g)}, eg) :
259	                Exists(T.Pos, p => {L.mine(layout, p) == False{} : Bool} &
260	                  ({L.hidden(G.knowledge(_), p) == True{} : Bool} & {G.step(_, T.Assist{k}) == G.open(_, p) : G.Game}))
261	              %Equal.sym(T.Status, G.status(g), T.Playing{}, playing) :
262	                Exists(T.Pos, p => {L.mine(layout, p) == False{} : Bool} &
263	                  ({L.hidden(G.knowledge(G.Game{w, h, layout, s, f, _}), p) == True{} : Bool} &
264	                   {G.step(G.Game{w, h, layout, s, f, _}, T.Assist{k}) == G.open(G.Game{w, h, layout, s, f, _}, p) : G.Game}))
265	              stuck_pick(w, h, layout, s, f,
266	                Equal.sym(Bool, False{}, G.all_safe(w, h, layout, s),
267	                  %playing : {L.is_won(_) == G.all_safe(w, h, layout, s) : Bool}; won),
268	                {%playing : L.Stuck(G.knowledge(G.Game{w, h, layout, s, f, _}));
269	                  %eg : L.Stuck(G.knowledge(_)); stuck : L.Stuck(G.knowledge(gp))},
270	                S.solve(G.knowledge(gp)), {==}, k)
271	
272	law assist_stuck_:
273	  for +w: Nat
274	  for +h: Nat
275	  for +layout: T.Grid(Bool)
276	  for shape: {L.shaped(Bool, w, h, layout) == True{} : Bool}
277	  for +g: G.Game
278	  for r: L.Reachable(w, h, layout, g)
279	  for +playing: {G.status(g) == T.Playing{} : T.Status}
280	  for stuck: L.Stuck(G.knowledge(g))
281	  for +k: Nat
282	  Exists(T.Pos, p => {L.mine(layout, p) == False{} : Bool} &
283	    ({L.hidden(G.knowledge(g), p) == True{} : Bool} & {G.step(g, T.Assist{k}) == G.open(g, p) : G.Game}))
284	
285	def assist_stuck_(w, h, layout, shape, g, r, playing, stuck, k):
286	  assist_stuck.k(w, h, layout, g, playing, stuck, k, PW.canon(w, h, layout, g, PI.inv_reach(w, h, layout, g, r)))
287	
288	# Pressing the assist too early
289	# =============================
290	
291	def early_pick(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +s: T.Grid(Bool), +f: List<&2, T.Pos>, +q: T.Pos,
292	  option: L.ProvablySafe(G.knowledge(G.Game{w, h, layout, s, f, T.Playing{}}), q),
293	  +r: Maybe<&2, T.Pos>, re: {S.solve(G.knowledge(G.Game{w, h, layout, s, f, T.Playing{}})) == r : Maybe<&2, T.Pos>}, +k: Nat) ->
294	  Exists(T.Pos, p => L.ProvablySafe(G.knowledge(G.Game{w, h, layout, s, f, T.Playing{}}), p) &
295	    ({G.status(G.assist.pick(r, G.Game{w, h, layout, s, f, T.Playing{}}, k)) == T.Lost{T.AssistTooEarly{p}} : T.Status} &
296	     {G.knowledge(G.assist.pick(r, G.Game{w, h, layout, s, f, T.Playing{}}, k)) == G.knowledge(G.Game{w, h, layout, s, f, T.Playing{}}) : T.Knowledge})):
297	  match r:
298	    case Some{p}:
299	      +k0 = G.knowledge(G.Game{w, h, layout, s, f, T.Playing{}})
300	      (p, (PV.solve_safe(k0, p, re), ({==}, {==})))
301	    case None{}:
302	      +k0 = G.knowledge(G.Game{w, h, layout, s, f, T.Playing{}})
303	      Empty.absurd(Exists(T.Pos, p => L.ProvablySafe(k0, p) &
304	        ({G.status(G.assist.pick(None{}, G.Game{w, h, layout, s, f, T.Playing{}}, k)) == T.Lost{T.AssistTooEarly{p}} : T.Status} &
305	         {G.knowledge(G.assist.pick(None{}, G.Game{w, h, layout, s, f, T.Playing{}}, k)) == k0 : T.Knowledge})),
306	        PV.solve_stuck(k0, re)(q, option))
307	
308	def assist_early.k(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +g: G.Game,
309	  +playing: {G.status(g) == T.Playing{} : T.Status}, +q: T.Pos, option: L.ProvablySafe(G.knowledge(g), q), +k: Nat,
310	  c: PW.Canon(w, h, layout, g)) ->
311	  Exists(T.Pos, p => L.ProvablySafe(G.knowledge(g), p) &
312	    ({G.status(G.step(g, T.Assist{k})) == T.Lost{T.AssistTooEarly{p}} : T.Status} &
313	     {G.knowledge(G.step(g, T.Assist{k})) == G.knowledge(g) : T.Knowledge})):
314	  match c:
315	    case (+eg, facts):
316	      +s = PW.shown_of(g)
317	      +f = PW.flags_of(g)
318	      +gp = {G.Game{w, h, layout, s, f, T.Playing{}} : G.Game}
319	      %Equal.sym(G.Game, g, G.Game{w, h, layout, s, f, G.status(g)}, eg) :
320	        Exists(T.Pos, p => L.ProvablySafe(G.knowledge(_), p) &
321	          ({G.status(G.step(_, T.Assist{k})) == T.Lost{T.AssistTooEarly{p}} : T.Status} &
322	           {G.knowledge(G.step(_, T.Assist{k})) == G.knowledge(_) : T.Knowledge}))
323	      %Equal.sym(T.Status, G.status(g), T.Playing{}, playing) :
324	        Exists(T.Pos, p => L.ProvablySafe(G.knowledge(G.Game{w, h, layout, s, f, _}), p) &
325	          ({G.status(G.step(G.Game{w, h, layout, s, f, _}, T.Assist{k})) == T.Lost{T.AssistTooEarly{p}} : T.Status} &
326	           {G.knowledge(G.step(G.Game{w, h, layout, s, f, _}, T.Assist{k})) == G.knowledge(G.Game{w, h, layout, s, f, _}) : T.Knowledge}))
327	      early_pick(w, h, layout, s, f, q,
328	        {%playing : L.ProvablySafe(G.knowledge(G.Game{w, h, layout, s, f, _}), q);
329	          %eg : L.ProvablySafe(G.knowledge(_), q); option : L.ProvablySafe(G.knowledge(gp), q)},
330	        S.solve(G.knowledge(gp)), {==}, k)
331	
332	law assist_too_early_:
333	  for +w: Nat
334	  for +h: Nat
335	  for +layout: T.Grid(Bool)
336	  for shape: {L.shaped(Bool, w, h, layout) == True{} : Bool}
337	  for +g: G.Game
338	  for r: L.Reachable(w, h, layout, g)
339	  for +playing: {G.status(g) == T.Playing{} : T.Status}
340	  for +q: T.Pos
341	  for option: L.ProvablySafe(G.knowledge(g), q)
342	  for +k: Nat
343	  Exists(T.Pos, p => L.ProvablySafe(G.knowledge(g), p) &
344	    ({G.status(G.step(g, T.Assist{k})) == T.Lost{T.AssistTooEarly{p}} : T.Status} &
345	     {G.knowledge(G.step(g, T.Assist{k})) == G.knowledge(g) : T.Knowledge}))
346	
347	def assist_too_early_(w, h, layout, shape, g, r, playing, q, option, k):
348	  assist_early.k(w, h, layout, g, playing, q, option, k, PW.canon(w, h, layout, g, PI.inv_reach(w, h, layout, g, r)))