So P(k+1)≡TP(k+1)≡TP( k+1 ) \equiv T.

Define predicate P(n)P(n)P( n ) as the equation that square_sum( n ) =n∑i=1(i2)\displaystyle=\sum_{i=1}^n (i^2), where n∈Z+n \in Z^+.

Using the direct proof technique, we assume that P(k)≡TP( k ) \equiv T so square_sum(k)=k∑i=1(i2)\displaystyle = \sum_{i=1}^k (i^2).

For P(1)P( 1 ), the left-hand side (LHS) = square_sum(1) =1=1∑i=1(i2)==1= \displaystyle \sum_{i=1}^1 (i^2) = the right-hand side (RHS), so P(1)≡TP( 1 ) \equiv T.

Basis step: to prove that P(1)≡TP( 1 ) \equiv T.

proof

For P(k+1)P( k+1 ), the LHS = square_sum(k+1) = (k+1)2+(k+1)^2+ square_sum(k) =(k+1)2+k∑i=1(i2)=k+1∑i=1(i2)== \displaystyle (k+1)^2+ \sum_{i=1}^k (i^2) = \sum_{i=1}^{k+1} (i^2) = the RHS.

Inductive step: to prove that ∀k(P(k)→P(k+1))≡T\forall k ( P( k ) \to P( k+1 ) ) \equiv T.

To use the UG rule, we consider an arbitrary positive integer kk.

QED

end of the second if

end of the first if

if (n==0)

return 1

return (a*a)

if (n is even)

a = power_bin(b, n div 2)

return (b*a*a)