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: (intloc 2) := (intloc 0 ) <> halt SCM+FSA by SCMBSORT:49;
A2: dom (Macro ((intloc 2) := (intloc 0 ))) = {0 ,1} by SCMFSA7B:4;
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 ))) = (card (Macro ((intloc 2) := (intloc 0 )))) + (card (Macro ((intloc 3) := (intloc 0 )))) by SCMFSA6A:61
.= 2 + (card (Macro ((intloc 3) := (intloc 0 )))) by SCMFSA7B:6
.= 2 + 2 by SCMFSA7B:6
.= 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 ) = ((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:69;
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;
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 = (insert-sort (fsloc 0 )) . 0
.= (Directed (Macro ((intloc 2) := (intloc 0 )))) . 0 by A11, A3, SCMFSA8A:28
.= (intloc 2) := (intloc 0 ) by A1, 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 SCMFSA7B:6;
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 + (card (Macro ((intloc 5) := (intloc 0 )))) by SCMFSA6A:61
.= 6 + 2 by SCMFSA7B:6
.= 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 + (card (Macro ((intloc 6) := (intloc 0 )))) by SCMFSA6A:61
.= 8 + 2 by SCMFSA7B:6
.= 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