Function terminal_byte_nat 

pub open spec fn terminal_byte_nat() -> TerminalByteNat

{
    Mapped {
        inner: terminal_byte(),
        mapper: TermByteFromToNat,
    }
}

Check that high bit is not set, and map to the corresponding nat value.