reconsider II = I ";" (SubFrom (a,(intloc 0))) as MacroInstruction of SCM+FSA ;
set WH = while>0 (a,II);
thus ( Times (a,I) is halt-ending & Times (a,I) is unique-halt ) ; :: thesis: verum