let n be Nat; :: thesis: 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 )
let P be IterativeAlgorithm (AddTo ((dl. 2),(dl. 1))) -extending Instruction-Sequence of SCM; :: thesis: 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 )
let s be 0 -started State-consisting of <%1,n,0%>; :: thesis: ( ( 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 )
A1: H₁( 0 ) = 0 ;
A2: for n being Nat holds H₁(n + 1) = (n + 1) + H₁(n) by NUMPOLY1:10;
A3: 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) = 0 + (H₁(n) - H₁((Comput (P,s,((4 * k) + 1))) . (dl. 1))) & (Comput (P,s,((4 * k) + 2))) . (dl. 2) = 0 + (H₁(n) - H₁(((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) = H₁(n) ) & (Result (P,s)) . (dl. 2) = H₁(n) ) from AMI_8:sch 1(A1, A2);

hereby :: thesis: ( ( 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 )

let k be Nat; :: thesis: ( k < n implies ( (Comput (P,s,((4 * k) + 1))) . (dl. 2) = H₁(n) - H₁((Comput (P,s,((4 * k) + 1))) . (dl. 1)) & (Comput (P,s,((4 * k) + 2))) . (dl. 2) = H₁(n) - H₁(((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) ) )
assume A4: k < n ; :: thesis: ( (Comput (P,s,((4 * k) + 1))) . (dl. 2) = H₁(n) - H₁((Comput (P,s,((4 * k) + 1))) . (dl. 1)) & (Comput (P,s,((4 * k) + 2))) . (dl. 2) = H₁(n) - H₁(((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) )
thus (Comput (P,s,((4 * k) + 1))) . (dl. 2) = 0 + (H₁(n) - H₁((Comput (P,s,((4 * k) + 1))) . (dl. 1))) by A3, A4
.= H₁(n) - H₁((Comput (P,s,((4 * k) + 1))) . (dl. 1)) ; :: thesis: ( (Comput (P,s,((4 * k) + 2))) . (dl. 2) = H₁(n) - H₁(((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) )
thus (Comput (P,s,((4 * k) + 2))) . (dl. 2) = 0 + (H₁(n) - H₁(((Comput (P,s,((4 * k) + 2))) . (dl. 1)) -' 1)) by A3, A4
.= H₁(n) - H₁(((Comput (P,s,((4 * k) + 2))) . (dl. 1)) -' 1) ; :: thesis: ( (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) )
thus (Comput (P,s,((4 * k) + 3))) . (dl. 2) = (Comput (P,s,((4 * k) + 2))) . (dl. 2) by A3, A4; :: thesis: (Comput (P,s,((4 * k) + 4))) . (dl. 2) = (Comput (P,s,((4 * k) + 3))) . (dl. 2)
thus (Comput (P,s,((4 * k) + 4))) . (dl. 2) = (Comput (P,s,((4 * k) + 3))) . (dl. 2) by A3, A4; :: thesis: verum

end;

thus ( ( 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 ) by A3; :: thesis: verum