law rewind_run

bend-lawful-stdlib@0.1.0.0 · src/sim.bend:79

import Base
import bend-lawful-stdlib@0.1.0.0/src/class.bend as C

79# rewinding n steps undoes running n steps
80law rewind_run:
81  for ~P: Data
82  for ~g: C.Group<P>
83  for ~F: P -> P
84  for +n: Nat
85  for +s: State<P>
86  {s == rewind(~P, ~g, ~F, n, run(~P, ~g, ~F, n, s)) : State<P>}