>>515
<>の定義は>>501です
>>511
x_2は自然数なので0ではないとします