Function decimal_2 

pub exec fn decimal_2(bytes: &[u8], pos: usize) -> u8

requires

pos < usize::MAX,

pos + 1 < bytes.len(),

ascii_digit(bytes@[pos as int]),

ascii_digit(bytes@[pos as int + 1]),

returns

decimal2(bytes@, pos),