law walk_snoc

minebender-game@1.0.0.0 · proof_walk.bend:94

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

94# Extending a walk to c by one step from c (a zero) to r.
95law walk_snoc:
96  for +path: List<&2, T.Pos>
97  for +w: Nat
98  for +h: Nat
99  for +layout: T.Grid(Bool)
100  for +p: T.Pos
101  for +c: T.Pos
102  for +r: T.Pos
103  for +wk: {L.zero_walk(path, w, h, layout, p, c) == True{} : Bool}
104  for +z: {L.zero(w, h, layout, c) == True{} : Bool}
105  for +a: {L.adjacent(c, r) == True{} : Bool}
106  for +on: {L.on_board(w, h, r) == True{} : Bool}
107  {L.zero_walk(List.append(&2, T.Pos, path, [r]), w, h, layout, p, r) == True{} : Bool}