at_end_of_stream(Stream) succeeds right after the last character from the stream Stream has been read, or when Stream is not a valid input stream.