def ticks_length

bend-kit-scheduler@0.4.1.0 · recurrence_proof.bend:18

import Base
import bend-kit-scheduler@0.4.1.0/recurrence.bend as R

18def ticks_length(count: Nat, +previous: Nat, +period: Nat)
19  -> {List.length(&2, Nat, R.ticks(count, previous, period)) == count : Nat}:
20  match count:
21    case 0n:
22      {==}
23    case 1n+n:
24      %ticks_length(n, Nat.add(previous, period), period) : {1n+List.length(&2, Nat,
25        R.ticks(n, Nat.add(previous, period), period)) == 1n+_ : Nat}
26      {==}