theorem Th31: :: AMI_8:31

for n being Nat
for P being IterativeAlgorithm (AddTo ((dl. 2),(dl. 1))) -extending Instruction-Sequence of SCM
for s being 0 -started State-consisting of <%1,n,0%> holds
( ( for k being Nat st k < n holds
( (Comput (P,s,((4 * k) + 1))) . (dl. 2) = (Triangle n) - (Triangle ((Comput (P,s,((4 * k) + 1))) . (dl. 1))) & (Comput (P,s,((4 * k) + 2))) . (dl. 2) = (Triangle n) - (Triangle (((Comput (P,s,((4 * k) + 2))) . (dl. 1)) -' 1)) & (Comput (P,s,((4 * k) + 3))) . (dl. 2) = (Comput (P,s,((4 * k) + 2))) . (dl. 2) & (Comput (P,s,((4 * k) + 4))) . (dl. 2) = (Comput (P,s,((4 * k) + 3))) . (dl. 2) ) ) & ( for k, j being Nat st k >= n holds
(Comput (P,s,(((4 * k) + 1) + j))) . (dl. 2) = Triangle n ) & (Result (P,s)) . (dl. 2) = Triangle n )