theorem Th32: :: AMI_8:32

for n being Nat
for P being IterativeAlgorithm (MultBy ((dl. 2),(dl. 1))) -extending Instruction-Sequence of SCM
for s being 0 -started State-consisting of <%1,n,1%> holds
( ( for k being Nat st k < n holds
( (Comput (P,s,((4 * k) + 1))) . (dl. 2) = (n !) / (((Comput (P,s,((4 * k) + 1))) . (dl. 1)) !) & (Comput (P,s,((4 * k) + 2))) . (dl. 2) = (n !) / ((((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) = n ! ) & (Result (P,s)) . (dl. 2) = n ! )