set f0 = fsloc 0;
set TT = Times ((intloc 1),(((((((((intloc 2) :=len (fsloc 0)) ";" (SubFrom ((intloc 2),(intloc 1)))) ";" ((intloc 3) := (intloc 2))) ";" (AddTo ((intloc 3),(intloc 0)))) ";" ((intloc 6) := ((fsloc 0),(intloc 3)))) ";" (SubFrom ((intloc 4),(intloc 4)))) ";" (while>0 ((intloc 2),((((intloc 5) := ((fsloc 0),(intloc 2))) ";" (SubFrom ((intloc 5),(intloc 6)))) ";" (if>0 ((intloc 5),(Macro (SubFrom ((intloc 2),(intloc 2)))),((AddTo ((intloc 4),(intloc 0))) ";" (SubFrom ((intloc 2),(intloc 0)))))))))) ";" (Times ((intloc 4),(((((((intloc 2) := (intloc 3)) ";" (SubFrom ((intloc 3),(intloc 0)))) ";" ((intloc 5) := ((fsloc 0),(intloc 2)))) ";" ((intloc 6) := ((fsloc 0),(intloc 3)))) ";" (((fsloc 0),(intloc 2)) := (intloc 6))) ";" (((fsloc 0),(intloc 3)) := (intloc 5)))))));
set q = Insert-Sort-Algorithm ;
set q0 = insert-sort (fsloc 0);
set W2 = (intloc 2) := (intloc 0);
set W3 = (intloc 3) := (intloc 0);
set W4 = (intloc 4) := (intloc 0);
set W5 = (intloc 5) := (intloc 0);
set W6 = (intloc 6) := (intloc 0);
set W7 = (intloc 1) :=len (fsloc 0);
set W8 = SubFrom ((intloc 1),(intloc 0));
set T8 = (SubFrom ((intloc 1),(intloc 0))) ";" (Times ((intloc 1),(((((((((intloc 2) :=len (fsloc 0)) ";" (SubFrom ((intloc 2),(intloc 1)))) ";" ((intloc 3) := (intloc 2))) ";" (AddTo ((intloc 3),(intloc 0)))) ";" ((intloc 6) := ((fsloc 0),(intloc 3)))) ";" (SubFrom ((intloc 4),(intloc 4)))) ";" (while>0 ((intloc 2),((((intloc 5) := ((fsloc 0),(intloc 2))) ";" (SubFrom ((intloc 5),(intloc 6)))) ";" (if>0 ((intloc 5),(Macro (SubFrom ((intloc 2),(intloc 2)))),((AddTo ((intloc 4),(intloc 0))) ";" (SubFrom ((intloc 2),(intloc 0)))))))))) ";" (Times ((intloc 4),(((((((intloc 2) := (intloc 3)) ";" (SubFrom ((intloc 3),(intloc 0)))) ";" ((intloc 5) := ((fsloc 0),(intloc 2)))) ";" ((intloc 6) := ((fsloc 0),(intloc 3)))) ";" (((fsloc 0),(intloc 2)) := (intloc 6))) ";" (((fsloc 0),(intloc 3)) := (intloc 5))))))));
set T7 = ((intloc 1) :=len (fsloc 0)) ";" ((SubFrom ((intloc 1),(intloc 0))) ";" (Times ((intloc 1),(((((((((intloc 2) :=len (fsloc 0)) ";" (SubFrom ((intloc 2),(intloc 1)))) ";" ((intloc 3) := (intloc 2))) ";" (AddTo ((intloc 3),(intloc 0)))) ";" ((intloc 6) := ((fsloc 0),(intloc 3)))) ";" (SubFrom ((intloc 4),(intloc 4)))) ";" (while>0 ((intloc 2),((((intloc 5) := ((fsloc 0),(intloc 2))) ";" (SubFrom ((intloc 5),(intloc 6)))) ";" (if>0 ((intloc 5),(Macro (SubFrom ((intloc 2),(intloc 2)))),((AddTo ((intloc 4),(intloc 0))) ";" (SubFrom ((intloc 2),(intloc 0)))))))))) ";" (Times ((intloc 4),(((((((intloc 2) := (intloc 3)) ";" (SubFrom ((intloc 3),(intloc 0)))) ";" ((intloc 5) := ((fsloc 0),(intloc 2)))) ";" ((intloc 6) := ((fsloc 0),(intloc 3)))) ";" (((fsloc 0),(intloc 2)) := (intloc 6))) ";" (((fsloc 0),(intloc 3)) := (intloc 5)))))))));
set T6 = ((intloc 6) := (intloc 0)) ";" (((intloc 1) :=len (fsloc 0)) ";" ((SubFrom ((intloc 1),(intloc 0))) ";" (Times ((intloc 1),(((((((((intloc 2) :=len (fsloc 0)) ";" (SubFrom ((intloc 2),(intloc 1)))) ";" ((intloc 3) := (intloc 2))) ";" (AddTo ((intloc 3),(intloc 0)))) ";" ((intloc 6) := ((fsloc 0),(intloc 3)))) ";" (SubFrom ((intloc 4),(intloc 4)))) ";" (while>0 ((intloc 2),((((intloc 5) := ((fsloc 0),(intloc 2))) ";" (SubFrom ((intloc 5),(intloc 6)))) ";" (if>0 ((intloc 5),(Macro (SubFrom ((intloc 2),(intloc 2)))),((AddTo ((intloc 4),(intloc 0))) ";" (SubFrom ((intloc 2),(intloc 0)))))))))) ";" (Times ((intloc 4),(((((((intloc 2) := (intloc 3)) ";" (SubFrom ((intloc 3),(intloc 0)))) ";" ((intloc 5) := ((fsloc 0),(intloc 2)))) ";" ((intloc 6) := ((fsloc 0),(intloc 3)))) ";" (((fsloc 0),(intloc 2)) := (intloc 6))) ";" (((fsloc 0),(intloc 3)) := (intloc 5))))))))));
set T5 = ((intloc 5) := (intloc 0)) ";" (((intloc 6) := (intloc 0)) ";" (((intloc 1) :=len (fsloc 0)) ";" ((SubFrom ((intloc 1),(intloc 0))) ";" (Times ((intloc 1),(((((((((intloc 2) :=len (fsloc 0)) ";" (SubFrom ((intloc 2),(intloc 1)))) ";" ((intloc 3) := (intloc 2))) ";" (AddTo ((intloc 3),(intloc 0)))) ";" ((intloc 6) := ((fsloc 0),(intloc 3)))) ";" (SubFrom ((intloc 4),(intloc 4)))) ";" (while>0 ((intloc 2),((((intloc 5) := ((fsloc 0),(intloc 2))) ";" (SubFrom ((intloc 5),(intloc 6)))) ";" (if>0 ((intloc 5),(Macro (SubFrom ((intloc 2),(intloc 2)))),((AddTo ((intloc 4),(intloc 0))) ";" (SubFrom ((intloc 2),(intloc 0)))))))))) ";" (Times ((intloc 4),(((((((intloc 2) := (intloc 3)) ";" (SubFrom ((intloc 3),(intloc 0)))) ";" ((intloc 5) := ((fsloc 0),(intloc 2)))) ";" ((intloc 6) := ((fsloc 0),(intloc 3)))) ";" (((fsloc 0),(intloc 2)) := (intloc 6))) ";" (((fsloc 0),(intloc 3)) := (intloc 5)))))))))));
set T4 = ((intloc 4) := (intloc 0)) ";" (((intloc 5) := (intloc 0)) ";" (((intloc 6) := (intloc 0)) ";" (((intloc 1) :=len (fsloc 0)) ";" ((SubFrom ((intloc 1),(intloc 0))) ";" (Times ((intloc 1),(((((((((intloc 2) :=len (fsloc 0)) ";" (SubFrom ((intloc 2),(intloc 1)))) ";" ((intloc 3) := (intloc 2))) ";" (AddTo ((intloc 3),(intloc 0)))) ";" ((intloc 6) := ((fsloc 0),(intloc 3)))) ";" (SubFrom ((intloc 4),(intloc 4)))) ";" (while>0 ((intloc 2),((((intloc 5) := ((fsloc 0),(intloc 2))) ";" (SubFrom ((intloc 5),(intloc 6)))) ";" (if>0 ((intloc 5),(Macro (SubFrom ((intloc 2),(intloc 2)))),((AddTo ((intloc 4),(intloc 0))) ";" (SubFrom ((intloc 2),(intloc 0)))))))))) ";" (Times ((intloc 4),(((((((intloc 2) := (intloc 3)) ";" (SubFrom ((intloc 3),(intloc 0)))) ";" ((intloc 5) := ((fsloc 0),(intloc 2)))) ";" ((intloc 6) := ((fsloc 0),(intloc 3)))) ";" (((fsloc 0),(intloc 2)) := (intloc 6))) ";" (((fsloc 0),(intloc 3)) := (intloc 5))))))))))));
set T3 = ((intloc 3) := (intloc 0)) ";" (((intloc 4) := (intloc 0)) ";" (((intloc 5) := (intloc 0)) ";" (((intloc 6) := (intloc 0)) ";" (((intloc 1) :=len (fsloc 0)) ";" ((SubFrom ((intloc 1),(intloc 0))) ";" (Times ((intloc 1),(((((((((intloc 2) :=len (fsloc 0)) ";" (SubFrom ((intloc 2),(intloc 1)))) ";" ((intloc 3) := (intloc 2))) ";" (AddTo ((intloc 3),(intloc 0)))) ";" ((intloc 6) := ((fsloc 0),(intloc 3)))) ";" (SubFrom ((intloc 4),(intloc 4)))) ";" (while>0 ((intloc 2),((((intloc 5) := ((fsloc 0),(intloc 2))) ";" (SubFrom ((intloc 5),(intloc 6)))) ";" (if>0 ((intloc 5),(Macro (SubFrom ((intloc 2),(intloc 2)))),((AddTo ((intloc 4),(intloc 0))) ";" (SubFrom ((intloc 2),(intloc 0)))))))))) ";" (Times ((intloc 4),(((((((intloc 2) := (intloc 3)) ";" (SubFrom ((intloc 3),(intloc 0)))) ";" ((intloc 5) := ((fsloc 0),(intloc 2)))) ";" ((intloc 6) := ((fsloc 0),(intloc 3)))) ";" (((fsloc 0),(intloc 2)) := (intloc 6))) ";" (((fsloc 0),(intloc 3)) := (intloc 5)))))))))))));
set X3 = ((intloc 2) := (intloc 0)) ";" ((intloc 3) := (intloc 0));
set X4 = (((intloc 2) := (intloc 0)) ";" ((intloc 3) := (intloc 0))) ";" ((intloc 4) := (intloc 0));
set X5 = ((((intloc 2) := (intloc 0)) ";" ((intloc 3) := (intloc 0))) ";" ((intloc 4) := (intloc 0))) ";" ((intloc 5) := (intloc 0));
set X6 = (((((intloc 2) := (intloc 0)) ";" ((intloc 3) := (intloc 0))) ";" ((intloc 4) := (intloc 0))) ";" ((intloc 5) := (intloc 0))) ";" ((intloc 6) := (intloc 0));
A1: dom (Macro ((intloc 2) := (intloc 0))) = {0,1} by COMPOS_1:61;
then A2: 0 in dom (Macro ((intloc 2) := (intloc 0))) by TARSKI:def 2;
A3: 1 in dom (Macro ((intloc 2) := (intloc 0))) by A1, TARSKI:def 2;
A4: card (((intloc 2) := (intloc 0)) ";" ((intloc 3) := (intloc 0))) = 4 by SCMFSA6A:35;
A5: insert-sort (fsloc 0) = (((((((intloc 2) := (intloc 0)) ";" ((intloc 3) := (intloc 0))) ";" ((intloc 4) := (intloc 0))) ";" ((intloc 5) := (intloc 0))) ";" ((intloc 6) := (intloc 0))) ";" ((intloc 1) :=len (fsloc 0))) ";" ((SubFrom ((intloc 1),(intloc 0))) ";" (Times ((intloc 1),(((((((((intloc 2) :=len (fsloc 0)) ";" (SubFrom ((intloc 2),(intloc 1)))) ";" ((intloc 3) := (intloc 2))) ";" (AddTo ((intloc 3),(intloc 0)))) ";" ((intloc 6) := ((fsloc 0),(intloc 3)))) ";" (SubFrom ((intloc 4),(intloc 4)))) ";" (while>0 ((intloc 2),((((intloc 5) := ((fsloc 0),(intloc 2))) ";" (SubFrom ((intloc 5),(intloc 6)))) ";" (if>0 ((intloc 5),(Macro (SubFrom ((intloc 2),(intloc 2)))),((AddTo ((intloc 4),(intloc 0))) ";" (SubFrom ((intloc 2),(intloc 0)))))))))) ";" (Times ((intloc 4),(((((((intloc 2) := (intloc 3)) ";" (SubFrom ((intloc 3),(intloc 0)))) ";" ((intloc 5) := ((fsloc 0),(intloc 2)))) ";" ((intloc 6) := ((fsloc 0),(intloc 3)))) ";" (((fsloc 0),(intloc 2)) := (intloc 6))) ";" (((fsloc 0),(intloc 3)) := (intloc 5))))))))) by SCMFSA6A:27;
then A6: insert-sort (fsloc 0) = ((((((intloc 2) := (intloc 0)) ";" ((intloc 3) := (intloc 0))) ";" ((intloc 4) := (intloc 0))) ";" ((intloc 5) := (intloc 0))) ";" ((intloc 6) := (intloc 0))) ";" (((intloc 1) :=len (fsloc 0)) ";" ((SubFrom ((intloc 1),(intloc 0))) ";" (Times ((intloc 1),(((((((((intloc 2) :=len (fsloc 0)) ";" (SubFrom ((intloc 2),(intloc 1)))) ";" ((intloc 3) := (intloc 2))) ";" (AddTo ((intloc 3),(intloc 0)))) ";" ((intloc 6) := ((fsloc 0),(intloc 3)))) ";" (SubFrom ((intloc 4),(intloc 4)))) ";" (while>0 ((intloc 2),((((intloc 5) := ((fsloc 0),(intloc 2))) ";" (SubFrom ((intloc 5),(intloc 6)))) ";" (if>0 ((intloc 5),(Macro (SubFrom ((intloc 2),(intloc 2)))),((AddTo ((intloc 4),(intloc 0))) ";" (SubFrom ((intloc 2),(intloc 0)))))))))) ";" (Times ((intloc 4),(((((((intloc 2) := (intloc 3)) ";" (SubFrom ((intloc 3),(intloc 0)))) ";" ((intloc 5) := ((fsloc 0),(intloc 2)))) ";" ((intloc 6) := ((fsloc 0),(intloc 3)))) ";" (((fsloc 0),(intloc 2)) := (intloc 6))) ";" (((fsloc 0),(intloc 3)) := (intloc 5)))))))))) by SCMFSA6A:27;
then A7: insert-sort (fsloc 0) = (((((intloc 2) := (intloc 0)) ";" ((intloc 3) := (intloc 0))) ";" ((intloc 4) := (intloc 0))) ";" ((intloc 5) := (intloc 0))) ";" (((intloc 6) := (intloc 0)) ";" (((intloc 1) :=len (fsloc 0)) ";" ((SubFrom ((intloc 1),(intloc 0))) ";" (Times ((intloc 1),(((((((((intloc 2) :=len (fsloc 0)) ";" (SubFrom ((intloc 2),(intloc 1)))) ";" ((intloc 3) := (intloc 2))) ";" (AddTo ((intloc 3),(intloc 0)))) ";" ((intloc 6) := ((fsloc 0),(intloc 3)))) ";" (SubFrom ((intloc 4),(intloc 4)))) ";" (while>0 ((intloc 2),((((intloc 5) := ((fsloc 0),(intloc 2))) ";" (SubFrom ((intloc 5),(intloc 6)))) ";" (if>0 ((intloc 5),(Macro (SubFrom ((intloc 2),(intloc 2)))),((AddTo ((intloc 4),(intloc 0))) ";" (SubFrom ((intloc 2),(intloc 0)))))))))) ";" (Times ((intloc 4),(((((((intloc 2) := (intloc 3)) ";" (SubFrom ((intloc 3),(intloc 0)))) ";" ((intloc 5) := ((fsloc 0),(intloc 2)))) ";" ((intloc 6) := ((fsloc 0),(intloc 3)))) ";" (((fsloc 0),(intloc 2)) := (intloc 6))) ";" (((fsloc 0),(intloc 3)) := (intloc 5))))))))))) by SCMFSA6A:27;
then A8: insert-sort (fsloc 0) = ((((intloc 2) := (intloc 0)) ";" ((intloc 3) := (intloc 0))) ";" ((intloc 4) := (intloc 0))) ";" (((intloc 5) := (intloc 0)) ";" (((intloc 6) := (intloc 0)) ";" (((intloc 1) :=len (fsloc 0)) ";" ((SubFrom ((intloc 1),(intloc 0))) ";" (Times ((intloc 1),(((((((((intloc 2) :=len (fsloc 0)) ";" (SubFrom ((intloc 2),(intloc 1)))) ";" ((intloc 3) := (intloc 2))) ";" (AddTo ((intloc 3),(intloc 0)))) ";" ((intloc 6) := ((fsloc 0),(intloc 3)))) ";" (SubFrom ((intloc 4),(intloc 4)))) ";" (while>0 ((intloc 2),((((intloc 5) := ((fsloc 0),(intloc 2))) ";" (SubFrom ((intloc 5),(intloc 6)))) ";" (if>0 ((intloc 5),(Macro (SubFrom ((intloc 2),(intloc 2)))),((AddTo ((intloc 4),(intloc 0))) ";" (SubFrom ((intloc 2),(intloc 0)))))))))) ";" (Times ((intloc 4),(((((((intloc 2) := (intloc 3)) ";" (SubFrom ((intloc 3),(intloc 0)))) ";" ((intloc 5) := ((fsloc 0),(intloc 2)))) ";" ((intloc 6) := ((fsloc 0),(intloc 3)))) ";" (((fsloc 0),(intloc 2)) := (intloc 6))) ";" (((fsloc 0),(intloc 3)) := (intloc 5)))))))))))) by SCMFSA6A:27;
then A9: insert-sort (fsloc 0) = (((intloc 2) := (intloc 0)) ";" ((intloc 3) := (intloc 0))) ";" (((intloc 4) := (intloc 0)) ";" (((intloc 5) := (intloc 0)) ";" (((intloc 6) := (intloc 0)) ";" (((intloc 1) :=len (fsloc 0)) ";" ((SubFrom ((intloc 1),(intloc 0))) ";" (Times ((intloc 1),(((((((((intloc 2) :=len (fsloc 0)) ";" (SubFrom ((intloc 2),(intloc 1)))) ";" ((intloc 3) := (intloc 2))) ";" (AddTo ((intloc 3),(intloc 0)))) ";" ((intloc 6) := ((fsloc 0),(intloc 3)))) ";" (SubFrom ((intloc 4),(intloc 4)))) ";" (while>0 ((intloc 2),((((intloc 5) := ((fsloc 0),(intloc 2))) ";" (SubFrom ((intloc 5),(intloc 6)))) ";" (if>0 ((intloc 5),(Macro (SubFrom ((intloc 2),(intloc 2)))),((AddTo ((intloc 4),(intloc 0))) ";" (SubFrom ((intloc 2),(intloc 0)))))))))) ";" (Times ((intloc 4),(((((((intloc 2) := (intloc 3)) ";" (SubFrom ((intloc 3),(intloc 0)))) ";" ((intloc 5) := ((fsloc 0),(intloc 2)))) ";" ((intloc 6) := ((fsloc 0),(intloc 3)))) ";" (((fsloc 0),(intloc 2)) := (intloc 6))) ";" (((fsloc 0),(intloc 3)) := (intloc 5))))))))))))) by SCMFSA6A:27
.= ((Macro ((intloc 2) := (intloc 0))) ";" ((intloc 3) := (intloc 0))) ";" (((intloc 4) := (intloc 0)) ";" (((intloc 5) := (intloc 0)) ";" (((intloc 6) := (intloc 0)) ";" (((intloc 1) :=len (fsloc 0)) ";" ((SubFrom ((intloc 1),(intloc 0))) ";" (Times ((intloc 1),(((((((((intloc 2) :=len (fsloc 0)) ";" (SubFrom ((intloc 2),(intloc 1)))) ";" ((intloc 3) := (intloc 2))) ";" (AddTo ((intloc 3),(intloc 0)))) ";" ((intloc 6) := ((fsloc 0),(intloc 3)))) ";" (SubFrom ((intloc 4),(intloc 4)))) ";" (while>0 ((intloc 2),((((intloc 5) := ((fsloc 0),(intloc 2))) ";" (SubFrom ((intloc 5),(intloc 6)))) ";" (if>0 ((intloc 5),(Macro (SubFrom ((intloc 2),(intloc 2)))),((AddTo ((intloc 4),(intloc 0))) ";" (SubFrom ((intloc 2),(intloc 0)))))))))) ";" (Times ((intloc 4),(((((((intloc 2) := (intloc 3)) ";" (SubFrom ((intloc 3),(intloc 0)))) ";" ((intloc 5) := ((fsloc 0),(intloc 2)))) ";" ((intloc 6) := ((fsloc 0),(intloc 3)))) ";" (((fsloc 0),(intloc 2)) := (intloc 6))) ";" (((fsloc 0),(intloc 3)) := (intloc 5))))))))))))) by SCMFSA6A:19 ;
insert-sort (fsloc 0) = (((intloc 2) := (intloc 0)) ";" ((intloc 3) := (intloc 0))) ";" (((intloc 4) := (intloc 0)) ";" (((intloc 5) := (intloc 0)) ";" (((intloc 6) := (intloc 0)) ";" (((intloc 1) :=len (fsloc 0)) ";" ((SubFrom ((intloc 1),(intloc 0))) ";" (Times ((intloc 1),(((((((((intloc 2) :=len (fsloc 0)) ";" (SubFrom ((intloc 2),(intloc 1)))) ";" ((intloc 3) := (intloc 2))) ";" (AddTo ((intloc 3),(intloc 0)))) ";" ((intloc 6) := ((fsloc 0),(intloc 3)))) ";" (SubFrom ((intloc 4),(intloc 4)))) ";" (while>0 ((intloc 2),((((intloc 5) := ((fsloc 0),(intloc 2))) ";" (SubFrom ((intloc 5),(intloc 6)))) ";" (if>0 ((intloc 5),(Macro (SubFrom ((intloc 2),(intloc 2)))),((AddTo ((intloc 4),(intloc 0))) ";" (SubFrom ((intloc 2),(intloc 0)))))))))) ";" (Times ((intloc 4),(((((((intloc 2) := (intloc 3)) ";" (SubFrom ((intloc 3),(intloc 0)))) ";" ((intloc 5) := ((fsloc 0),(intloc 2)))) ";" ((intloc 6) := ((fsloc 0),(intloc 3)))) ";" (((fsloc 0),(intloc 2)) := (intloc 6))) ";" (((fsloc 0),(intloc 3)) := (intloc 5))))))))))))) by A8, SCMFSA6A:27;
then A10: insert-sort (fsloc 0) = ((intloc 2) := (intloc 0)) ";" (((intloc 3) := (intloc 0)) ";" (((intloc 4) := (intloc 0)) ";" (((intloc 5) := (intloc 0)) ";" (((intloc 6) := (intloc 0)) ";" (((intloc 1) :=len (fsloc 0)) ";" ((SubFrom ((intloc 1),(intloc 0))) ";" (Times ((intloc 1),(((((((((intloc 2) :=len (fsloc 0)) ";" (SubFrom ((intloc 2),(intloc 1)))) ";" ((intloc 3) := (intloc 2))) ";" (AddTo ((intloc 3),(intloc 0)))) ";" ((intloc 6) := ((fsloc 0),(intloc 3)))) ";" (SubFrom ((intloc 4),(intloc 4)))) ";" (while>0 ((intloc 2),((((intloc 5) := ((fsloc 0),(intloc 2))) ";" (SubFrom ((intloc 5),(intloc 6)))) ";" (if>0 ((intloc 5),(Macro (SubFrom ((intloc 2),(intloc 2)))),((AddTo ((intloc 4),(intloc 0))) ";" (SubFrom ((intloc 2),(intloc 0)))))))))) ";" (Times ((intloc 4),(((((((intloc 2) := (intloc 3)) ";" (SubFrom ((intloc 3),(intloc 0)))) ";" ((intloc 5) := ((fsloc 0),(intloc 2)))) ";" ((intloc 6) := ((fsloc 0),(intloc 3)))) ";" (((fsloc 0),(intloc 2)) := (intloc 6))) ";" (((fsloc 0),(intloc 3)) := (intloc 5)))))))))))))) by SCMFSA6A:31
.= (Macro ((intloc 2) := (intloc 0))) ";" (((intloc 3) := (intloc 0)) ";" (((intloc 4) := (intloc 0)) ";" (((intloc 5) := (intloc 0)) ";" (((intloc 6) := (intloc 0)) ";" (((intloc 1) :=len (fsloc 0)) ";" ((SubFrom ((intloc 1),(intloc 0))) ";" (Times ((intloc 1),(((((((((intloc 2) :=len (fsloc 0)) ";" (SubFrom ((intloc 2),(intloc 1)))) ";" ((intloc 3) := (intloc 2))) ";" (AddTo ((intloc 3),(intloc 0)))) ";" ((intloc 6) := ((fsloc 0),(intloc 3)))) ";" (SubFrom ((intloc 4),(intloc 4)))) ";" (while>0 ((intloc 2),((((intloc 5) := ((fsloc 0),(intloc 2))) ";" (SubFrom ((intloc 5),(intloc 6)))) ";" (if>0 ((intloc 5),(Macro (SubFrom ((intloc 2),(intloc 2)))),((AddTo ((intloc 4),(intloc 0))) ";" (SubFrom ((intloc 2),(intloc 0)))))))))) ";" (Times ((intloc 4),(((((((intloc 2) := (intloc 3)) ";" (SubFrom ((intloc 3),(intloc 0)))) ";" ((intloc 5) := ((fsloc 0),(intloc 2)))) ";" ((intloc 6) := ((fsloc 0),(intloc 3)))) ";" (((fsloc 0),(intloc 2)) := (intloc 6))) ";" (((fsloc 0),(intloc 3)) := (intloc 5)))))))))))))) by SCMFSA6A:def 5 ;
let P be Instruction-Sequence of SCM+FSA; :: thesis: ( Insert-Sort-Algorithm c= P implies ( P . 0 = (intloc 2) := (intloc 0) & P . 1 = goto 2 & P . 2 = (intloc 3) := (intloc 0) & P . 3 = goto 4 & P . 4 = (intloc 4) := (intloc 0) & P . 5 = goto 6 & P . 6 = (intloc 5) := (intloc 0) & P . 7 = goto 8 & P . 8 = (intloc 6) := (intloc 0) & P . 9 = goto 10 & P . 10 = (intloc 1) :=len (fsloc 0) & P . 11 = goto 12 ) )
assume A11: Insert-Sort-Algorithm c= P ; :: thesis: ( P . 0 = (intloc 2) := (intloc 0) & P . 1 = goto 2 & P . 2 = (intloc 3) := (intloc 0) & P . 3 = goto 4 & P . 4 = (intloc 4) := (intloc 0) & P . 5 = goto 6 & P . 6 = (intloc 5) := (intloc 0) & P . 7 = goto 8 & P . 8 = (intloc 6) := (intloc 0) & P . 9 = goto 10 & P . 10 = (intloc 1) :=len (fsloc 0) & P . 11 = goto 12 )

A12: now :: thesis: for i being Nat st i < 71 holds
(insert-sort (fsloc 0)) . i = P . i

let i be Nat; :: thesis: ( i < 71 implies (insert-sort (fsloc 0)) . i = P . i )
assume i < 71 ; :: thesis: (insert-sort (fsloc 0)) . i = P . i
then i in dom (insert-sort (fsloc 0)) by Th23;
hence (insert-sort (fsloc 0)) . i = P . i by A11, GRFUNC_1:2; :: thesis: verum

end;

hence P . 0 = ((Macro ((intloc 2) := (intloc 0))) ";" (((intloc 3) := (intloc 0)) ";" (((intloc 4) := (intloc 0)) ";" (((intloc 5) := (intloc 0)) ";" (((intloc 6) := (intloc 0)) ";" (((intloc 1) :=len (fsloc 0)) ";" ((SubFrom ((intloc 1),(intloc 0))) ";" (Times ((intloc 1),(((((((((intloc 2) :=len (fsloc 0)) ";" (SubFrom ((intloc 2),(intloc 1)))) ";" ((intloc 3) := (intloc 2))) ";" (AddTo ((intloc 3),(intloc 0)))) ";" ((intloc 6) := ((fsloc 0),(intloc 3)))) ";" (SubFrom ((intloc 4),(intloc 4)))) ";" (while>0 ((intloc 2),((((intloc 5) := ((fsloc 0),(intloc 2))) ";" (SubFrom ((intloc 5),(intloc 6)))) ";" (if>0 ((intloc 5),(Macro (SubFrom ((intloc 2),(intloc 2)))),((AddTo ((intloc 4),(intloc 0))) ";" (SubFrom ((intloc 2),(intloc 0)))))))))) ";" (Times ((intloc 4),(((((((intloc 2) := (intloc 3)) ";" (SubFrom ((intloc 3),(intloc 0)))) ";" ((intloc 5) := ((fsloc 0),(intloc 2)))) ";" ((intloc 6) := ((fsloc 0),(intloc 3)))) ";" (((fsloc 0),(intloc 2)) := (intloc 6))) ";" (((fsloc 0),(intloc 3)) := (intloc 5))))))))))))))) . 0 by A10
.= (Directed (Macro ((intloc 2) := (intloc 0)))) . 0 by A2, SCMFSA8A:14
.= (intloc 2) := (intloc 0) by SCMFSA7B:1 ;
:: thesis: ( P . 1 = goto 2 & P . 2 = (intloc 3) := (intloc 0) & P . 3 = goto 4 & P . 4 = (intloc 4) := (intloc 0) & P . 5 = goto 6 & P . 6 = (intloc 5) := (intloc 0) & P . 7 = goto 8 & P . 8 = (intloc 6) := (intloc 0) & P . 9 = goto 10 & P . 10 = (intloc 1) :=len (fsloc 0) & P . 11 = goto 12 )
A13: card (Macro ((intloc 2) := (intloc 0))) = 2 by COMPOS_1:56;
A14: card ((((intloc 2) := (intloc 0)) ";" ((intloc 3) := (intloc 0))) ";" ((intloc 4) := (intloc 0))) = 6 by SCMBSORT:23;
then A15: card (((((intloc 2) := (intloc 0)) ";" ((intloc 3) := (intloc 0))) ";" ((intloc 4) := (intloc 0))) ";" ((intloc 5) := (intloc 0))) = 6 + 2 by SCMFSA6A:34
.= 8 ;
then A16: card ((((((intloc 2) := (intloc 0)) ";" ((intloc 3) := (intloc 0))) ";" ((intloc 4) := (intloc 0))) ";" ((intloc 5) := (intloc 0))) ";" ((intloc 6) := (intloc 0))) = 8 + 2 by SCMFSA6A:34
.= 10 ;
thus P . 1 = (insert-sort (fsloc 0)) . 1 by A12
.= (Directed (Macro ((intloc 2) := (intloc 0)))) . 1 by A10, A3, SCMFSA8A:14
.= goto 2 by SCMFSA7B:2 ; :: thesis: ( P . 2 = (intloc 3) := (intloc 0) & P . 3 = goto 4 & P . 4 = (intloc 4) := (intloc 0) & P . 5 = goto 6 & P . 6 = (intloc 5) := (intloc 0) & P . 7 = goto 8 & P . 8 = (intloc 6) := (intloc 0) & P . 9 = goto 10 & P . 10 = (intloc 1) :=len (fsloc 0) & P . 11 = goto 12 )
thus P . 2 = (insert-sort (fsloc 0)) . 2 by A12
.= (intloc 3) := (intloc 0) by A9, A13, SCMBSORT:27 ; :: thesis: ( P . 3 = goto 4 & P . 4 = (intloc 4) := (intloc 0) & P . 5 = goto 6 & P . 6 = (intloc 5) := (intloc 0) & P . 7 = goto 8 & P . 8 = (intloc 6) := (intloc 0) & P . 9 = goto 10 & P . 10 = (intloc 1) :=len (fsloc 0) & P . 11 = goto 12 )
thus P . 3 = (insert-sort (fsloc 0)) . (2 + 1) by A12
.= goto (2 + 2) by A9, A13, SCMBSORT:28
.= goto 4 ; :: thesis: ( P . 4 = (intloc 4) := (intloc 0) & P . 5 = goto 6 & P . 6 = (intloc 5) := (intloc 0) & P . 7 = goto 8 & P . 8 = (intloc 6) := (intloc 0) & P . 9 = goto 10 & P . 10 = (intloc 1) :=len (fsloc 0) & P . 11 = goto 12 )
thus P . 4 = (insert-sort (fsloc 0)) . 4 by A12
.= (intloc 4) := (intloc 0) by A8, A4, SCMBSORT:27 ; :: thesis: ( P . 5 = goto 6 & P . 6 = (intloc 5) := (intloc 0) & P . 7 = goto 8 & P . 8 = (intloc 6) := (intloc 0) & P . 9 = goto 10 & P . 10 = (intloc 1) :=len (fsloc 0) & P . 11 = goto 12 )
thus P . 5 = (insert-sort (fsloc 0)) . (4 + 1) by A12
.= goto (4 + 2) by A8, A4, SCMBSORT:28
.= goto 6 ; :: thesis: ( P . 6 = (intloc 5) := (intloc 0) & P . 7 = goto 8 & P . 8 = (intloc 6) := (intloc 0) & P . 9 = goto 10 & P . 10 = (intloc 1) :=len (fsloc 0) & P . 11 = goto 12 )
thus P . 6 = (insert-sort (fsloc 0)) . 6 by A12
.= (intloc 5) := (intloc 0) by A7, A14, SCMBSORT:27 ; :: thesis: ( P . 7 = goto 8 & P . 8 = (intloc 6) := (intloc 0) & P . 9 = goto 10 & P . 10 = (intloc 1) :=len (fsloc 0) & P . 11 = goto 12 )
thus P . 7 = (insert-sort (fsloc 0)) . (6 + 1) by A12
.= goto (6 + 2) by A7, A14, SCMBSORT:28
.= goto 8 ; :: thesis: ( P . 8 = (intloc 6) := (intloc 0) & P . 9 = goto 10 & P . 10 = (intloc 1) :=len (fsloc 0) & P . 11 = goto 12 )
thus P . 8 = (insert-sort (fsloc 0)) . 8 by A12
.= (intloc 6) := (intloc 0) by A6, A15, SCMBSORT:27 ; :: thesis: ( P . 9 = goto 10 & P . 10 = (intloc 1) :=len (fsloc 0) & P . 11 = goto 12 )
thus P . 9 = (insert-sort (fsloc 0)) . (8 + 1) by A12
.= goto (8 + 2) by A6, A15, SCMBSORT:28
.= goto 10 ; :: thesis: ( P . 10 = (intloc 1) :=len (fsloc 0) & P . 11 = goto 12 )
thus P . 10 = (insert-sort (fsloc 0)) . 10 by A12
.= (intloc 1) :=len (fsloc 0) by A5, A16, SCMBSORT:27 ; :: thesis: P . 11 = goto 12
thus P . 11 = (insert-sort (fsloc 0)) . (10 + 1) by A12
.= goto (10 + 2) by A5, A16, SCMBSORT:28
.= goto 12 ; :: thesis: verum