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));
A2: dom (Macro ((intloc 2) := (intloc 0))) = {0,1} by COMPOS_1:149;
then A3: 0 in dom (Macro ((intloc 2) := (intloc 0))) by TARSKI:def 2;
A4: 1 in dom (Macro ((intloc 2) := (intloc 0))) by A2, TARSKI:def 2;
A5: card (((intloc 2) := (intloc 0)) ';' ((intloc 3) := (intloc 0))) = 2 + 2 by SCMFSA6A:77
.= 4 ;
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:69;
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:69;
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:69;
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:69;
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:69
.= ((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:59 ;
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 A9, SCMFSA6A:69;
then A11: 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:73
.= (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 6 ;
let s be State of SCM+FSA; :: thesis: ( Insert-Sort-Algorithm c= s implies ( s . 0 = (intloc 2) := (intloc 0) & s . 1 = goto 2 & s . 2 = (intloc 3) := (intloc 0) & s . 3 = goto 4 & s . 4 = (intloc 4) := (intloc 0) & s . 5 = goto 6 & s . 6 = (intloc 5) := (intloc 0) & s . 7 = goto 8 & s . 8 = (intloc 6) := (intloc 0) & s . 9 = goto 10 & s . 10 = (intloc 1) :=len (fsloc 0) & s . 11 = goto 12 ) )
assume A12: Insert-Sort-Algorithm c= s ; :: thesis: ( s . 0 = (intloc 2) := (intloc 0) & s . 1 = goto 2 & s . 2 = (intloc 3) := (intloc 0) & s . 3 = goto 4 & s . 4 = (intloc 4) := (intloc 0) & s . 5 = goto 6 & s . 6 = (intloc 5) := (intloc 0) & s . 7 = goto 8 & s . 8 = (intloc 6) := (intloc 0) & s . 9 = goto 10 & s . 10 = (intloc 1) :=len (fsloc 0) & s . 11 = goto 12 )

A13: now

let i be Element of NAT ; :: thesis: ( i < 82 implies (insert-sort (fsloc 0)) . i = s . i )
assume i < 82 ; :: thesis: (insert-sort (fsloc 0)) . i = s . i
then i in dom (insert-sort (fsloc 0)) by Th43;
hence (insert-sort (fsloc 0)) . i = s . i by A12, GRFUNC_1:8; :: thesis: verum

end;

hence s . 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 A11
.= (Directed (Macro ((intloc 2) := (intloc 0)))) . 0 by A3, SCMFSA8A:28
.= (intloc 2) := (intloc 0) by SCMFSA7B:7 ;
:: thesis: ( s . 1 = goto 2 & s . 2 = (intloc 3) := (intloc 0) & s . 3 = goto 4 & s . 4 = (intloc 4) := (intloc 0) & s . 5 = goto 6 & s . 6 = (intloc 5) := (intloc 0) & s . 7 = goto 8 & s . 8 = (intloc 6) := (intloc 0) & s . 9 = goto 10 & s . 10 = (intloc 1) :=len (fsloc 0) & s . 11 = goto 12 )
A14: card (Macro ((intloc 2) := (intloc 0))) = 2 by COMPOS_1:150;
A15: card ((((intloc 2) := (intloc 0)) ';' ((intloc 3) := (intloc 0))) ';' ((intloc 4) := (intloc 0))) = 6 by SCMBSORT:45;
then A16: card (((((intloc 2) := (intloc 0)) ';' ((intloc 3) := (intloc 0))) ';' ((intloc 4) := (intloc 0))) ';' ((intloc 5) := (intloc 0))) = 6 + 2 by SCMFSA6A:76
.= 8 ;
then A17: 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:76
.= 10 ;
thus s . 1 = (insert-sort (fsloc 0)) . 1 by A13
.= (Directed (Macro ((intloc 2) := (intloc 0)))) . 1 by A11, A4, SCMFSA8A:28
.= goto 2 by SCMFSA7B:8 ; :: thesis: ( s . 2 = (intloc 3) := (intloc 0) & s . 3 = goto 4 & s . 4 = (intloc 4) := (intloc 0) & s . 5 = goto 6 & s . 6 = (intloc 5) := (intloc 0) & s . 7 = goto 8 & s . 8 = (intloc 6) := (intloc 0) & s . 9 = goto 10 & s . 10 = (intloc 1) :=len (fsloc 0) & s . 11 = goto 12 )
thus s . 2 = (insert-sort (fsloc 0)) . 2 by A13
.= (intloc 3) := (intloc 0) by A10, A14, SCMBSORT:51 ; :: thesis: ( s . 3 = goto 4 & s . 4 = (intloc 4) := (intloc 0) & s . 5 = goto 6 & s . 6 = (intloc 5) := (intloc 0) & s . 7 = goto 8 & s . 8 = (intloc 6) := (intloc 0) & s . 9 = goto 10 & s . 10 = (intloc 1) :=len (fsloc 0) & s . 11 = goto 12 )
thus s . 3 = (insert-sort (fsloc 0)) . (2 + 1) by A13
.= goto (2 + 2) by A10, A14, SCMBSORT:51
.= goto 4 ; :: thesis: ( s . 4 = (intloc 4) := (intloc 0) & s . 5 = goto 6 & s . 6 = (intloc 5) := (intloc 0) & s . 7 = goto 8 & s . 8 = (intloc 6) := (intloc 0) & s . 9 = goto 10 & s . 10 = (intloc 1) :=len (fsloc 0) & s . 11 = goto 12 )
thus s . 4 = (insert-sort (fsloc 0)) . 4 by A13
.= (intloc 4) := (intloc 0) by A9, A5, SCMBSORT:51 ; :: thesis: ( s . 5 = goto 6 & s . 6 = (intloc 5) := (intloc 0) & s . 7 = goto 8 & s . 8 = (intloc 6) := (intloc 0) & s . 9 = goto 10 & s . 10 = (intloc 1) :=len (fsloc 0) & s . 11 = goto 12 )
thus s . 5 = (insert-sort (fsloc 0)) . (4 + 1) by A13
.= goto (4 + 2) by A9, A5, SCMBSORT:51
.= goto 6 ; :: thesis: ( s . 6 = (intloc 5) := (intloc 0) & s . 7 = goto 8 & s . 8 = (intloc 6) := (intloc 0) & s . 9 = goto 10 & s . 10 = (intloc 1) :=len (fsloc 0) & s . 11 = goto 12 )
thus s . 6 = (insert-sort (fsloc 0)) . 6 by A13
.= (intloc 5) := (intloc 0) by A8, A15, SCMBSORT:51 ; :: thesis: ( s . 7 = goto 8 & s . 8 = (intloc 6) := (intloc 0) & s . 9 = goto 10 & s . 10 = (intloc 1) :=len (fsloc 0) & s . 11 = goto 12 )
thus s . 7 = (insert-sort (fsloc 0)) . (6 + 1) by A13
.= goto (6 + 2) by A8, A15, SCMBSORT:51
.= goto 8 ; :: thesis: ( s . 8 = (intloc 6) := (intloc 0) & s . 9 = goto 10 & s . 10 = (intloc 1) :=len (fsloc 0) & s . 11 = goto 12 )
thus s . 8 = (insert-sort (fsloc 0)) . 8 by A13
.= (intloc 6) := (intloc 0) by A7, A16, SCMBSORT:51 ; :: thesis: ( s . 9 = goto 10 & s . 10 = (intloc 1) :=len (fsloc 0) & s . 11 = goto 12 )
thus s . 9 = (insert-sort (fsloc 0)) . (8 + 1) by A13
.= goto (8 + 2) by A7, A16, SCMBSORT:51
.= goto 10 ; :: thesis: ( s . 10 = (intloc 1) :=len (fsloc 0) & s . 11 = goto 12 )
thus s . 10 = (insert-sort (fsloc 0)) . 10 by A13
.= (intloc 1) :=len (fsloc 0) by A6, A17, SCMBSORT:52 ; :: thesis: s . 11 = goto 12
thus s . 11 = (insert-sort (fsloc 0)) . (10 + 1) by A13
.= goto (10 + 2) by A6, A17, SCMBSORT:52
.= goto 12 ; :: thesis: verum