fact: Definition step (M: Cm1) (x: Config) : Config := match (value x), (nth_error M (state x)) with | 0, _ => x | _, None => x | _, Some (p, n) => match modulo (value x) (n+1) with | 0 => {| state := p; value := ((value x) * (n+2)) / (n+1) |} | _ => {| state := 1 + state x; value := value x |} end end.
imports: List Nat