Изменения
→Доказательство
== Доказательство ==
Покажем, что инвариант не нарушится.
Инвариант можно нарушить в 2 случаях, когда к единице прибавляют 1, и в следующем разряде стоит не 0, и когда к нулю прибавляется 1, а в предыдущем разряде стоит 2.
В первом случае, если в следующем разряде 1, алгоритм будет устанавливать в текущий разряд 0 и запускаться от следующего разряда. Если в следующем разряде 2, то, согласно инварианту, следующий за 2 разряд 0, и установив в следующий за двойкой и разряд с двойкой едины единцы инвариант не нарушится.
Во втором случае, если в следующем разряде 0, то предыдущий установится в 0, текущий в 2 и так как в следующем 0 инвариант не нарушится. Если в следующем разряде не 0, то предыдущий установится в 0 и алгоритм запустится от следующего.
