Доказывая хвост рекурсивной функции (вычисления силы целого)

Question

Вот функция, corectness Я хочу доказать (написано в OCaml):

let rec pow ak a k = if k=0 then ak 
else if (k mod 2)=1 then pow (ak*a) (a*a) (k/2) 
else pow ak (a*a) (k/2);; 

Его спецификация:

For integers ak, a>0, k>=0 pow returns ak*(a^k). 

Я знаю, необходимо доказать 2 вещи - что функция завершается и возвращает правильный результат для предполагаемого ввода. Проблема в том, что я не видел много таких доказательств, и единственное, что я знаю, это то, что мне нужно использовать индукцию. Как мне подойти к такой проблеме?

Answer 1

Доказать базу чехол. Затем докажите, что для a+1 и k+1 утверждение верно в предположении, что оно работает для a и k.