def chord_targets_eq.go

minebender-game@1.0.0.0 · proof_copy.bend:344

import Base
import minebender-game@1.0.0.0/types.bend as T
import minebender-game@1.0.0.0/board.bend as B
import minebender-game@1.0.0.0/game.bend as G
import minebender-game@1.0.0.0/LAWS.bend as L

344def chord_targets_eq.go(+g: G.Game, +v: T.Knowledge, +p: T.Pos) ->
345  {G.chord_targets.go(g, v, p) == L.chord_targets.go(g, v, p) : List<&2, T.Pos>}:
346  match v:
347    case T.Knowledge{w, h, n, rows}:
348      +k = {T.Knowledge{w, h, n, rows} : T.Knowledge}
349      %neighbours_eq(w, h, p) :
350        {G.chord_targets.pick(g, k, B.neighbours(w, h, p), G.seen(k, p))
351          == L.chord_targets.pick(g, k, _, L.seen(k, p)) : List<&2, T.Pos>}
352      %seen_eq(k, p) :
353        {G.chord_targets.pick(g, k, B.neighbours(w, h, p), G.seen(k, p))
354          == L.chord_targets.pick(g, k, B.neighbours(w, h, p), _) : List<&2, T.Pos>}
355      chord_pick_eq(g, k, B.neighbours(w, h, p), G.seen(k, p))