ProofCopy.chord_targets_eq.go: def of minebender-game@1.0.0.0
Import: import minebender-game@1.0.0.0/proof_copy.bend as ProofCopy
Lines 344-355 of minebender-game@1.0.0.0/proof_copy.bend: https://jend.leeeet.dev/read.txt?path=minebender-game@1.0.0.0/proof_copy.bend&start_line=344&end_line=355

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

def chord_targets_eq.go(+g: G.Game, +v: T.Knowledge, +p: T.Pos) ->
  {G.chord_targets.go(g, v, p) == L.chord_targets.go(g, v, p) : List<&2, T.Pos>}:
  match v:
    case T.Knowledge{w, h, n, rows}:
      +k = {T.Knowledge{w, h, n, rows} : T.Knowledge}
      %neighbours_eq(w, h, p) :
        {G.chord_targets.pick(g, k, B.neighbours(w, h, p), G.seen(k, p))
          == L.chord_targets.pick(g, k, _, L.seen(k, p)) : List<&2, T.Pos>}
      %seen_eq(k, p) :
        {G.chord_targets.pick(g, k, B.neighbours(w, h, p), G.seen(k, p))
          == L.chord_targets.pick(g, k, B.neighbours(w, h, p), _) : List<&2, T.Pos>}
      chord_pick_eq(g, k, B.neighbours(w, h, p), G.seen(k, p))

Uses (14):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=chord_targets.go
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=chord_targets.pick
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=seen
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/board.bend&name=neighbours
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/game.bend&name=Game
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/game.bend&name=chord_targets.go
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/game.bend&name=chord_targets.pick
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/game.bend&name=seen
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_copy.bend&name=chord_pick_eq
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_copy.bend&name=neighbours_eq
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_copy.bend&name=seen_eq
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/types.bend&name=Knowledge
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/types.bend&name=Pos