Математическая логика и теория алгоритмов

Основной алгоритм:

дано: Робот в корне, листья не обработаны

надо: Робот в корне, листья обработаны

{ОЛ}

вверх_до_упора_и_обработать

{инвариант: ОЛН}

while есть_снизу do begin

if есть_справа then begin {ОЛН, есть справа}

вправо;