Conservative definition
Parameters: b, c, a, l
forall ff_i_defined_repeat. (exists ff_lt_defined_repeat_bound. ff_lt_defined_repeat_bound + S ff_i_defined_repeat = l) -> (((exists ff_h_defined_repeat_decoded. ff_h_defined_repeat_decoded + S (a) = S ((S (ff_i_defined_repeat)) * c)) /\ exists ff_q_defined_repeat_decoded. b = ff_q_defined_repeat_decoded * S ((S (ff_i_defined_repeat)) * c) + (a)))