Function digits 

pub open spec fn digits(bytes: Seq<u8>, start: int, end: int) -> bool

{
    &&& 0 <= start <= end <= bytes.len()
    &&& forall |i: int| start <= i < end ==> ascii_digit(#[trigger] bytes[i])

}