while 0=0do output_byte stdout(input_byte stdin*7+7)done