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 );
let s be State of SCM+FSA ; :: thesis: ( Insert-Sort-Algorithm c= s implies ( s . (insloc 0 ) = (intloc 2) := (intloc 0 ) & s . (insloc 1) = goto (insloc 2) & s . (insloc 2) = (intloc 3) := (intloc 0 ) & s . (insloc 3) = goto (insloc 4) & s . (insloc 4) = (intloc 4) := (intloc 0 ) & s . (insloc 5) = goto (insloc 6) & s . (insloc 6) = (intloc 5) := (intloc 0 ) & s . (insloc 7) = goto (insloc 8) & s . (insloc 8) = (intloc 6) := (intloc 0 ) & s . (insloc 9) = goto (insloc 10) & s . (insloc 10) = (intloc 1) :=len (fsloc 0 ) & s . (insloc 11) = goto (insloc 12) ) )
assume A1: Insert-Sort-Algorithm c= s ; :: thesis: ( s . (insloc 0 ) = (intloc 2) := (intloc 0 ) & s . (insloc 1) = goto (insloc 2) & s . (insloc 2) = (intloc 3) := (intloc 0 ) & s . (insloc 3) = goto (insloc 4) & s . (insloc 4) = (intloc 4) := (intloc 0 ) & s . (insloc 5) = goto (insloc 6) & s . (insloc 6) = (intloc 5) := (intloc 0 ) & s . (insloc 7) = goto (insloc 8) & s . (insloc 8) = (intloc 6) := (intloc 0 ) & s . (insloc 9) = goto (insloc 10) & s . (insloc 10) = (intloc 1) :=len (fsloc 0 ) & s . (insloc 11) = goto (insloc 12) )

A2: now

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

end;

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 ));
A3: 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 A4: 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 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:69;
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:69;
then 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 B8: 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;
A9: 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 A6, SCMFSA6A:69;
dom (Macro ((intloc 2) := (intloc 0 ))) = {(insloc 0 ),(insloc 1)} by SCMFSA7B:4;
then A10: ( insloc 0 in dom (Macro ((intloc 2) := (intloc 0 ))) & insloc 1 in dom (Macro ((intloc 2) := (intloc 0 ))) ) by TARSKI:def 2;
A11: (intloc 2) := (intloc 0 ) <> halt SCM+FSA by SCMBSORT:49;
thus s . (insloc 0 ) = (insert-sort (fsloc 0 )) . (insloc 0 ) by A2
.= (Directed (Macro ((intloc 2) := (intloc 0 )))) . (insloc 0 ) by B8, A10, SCMFSA8A:28
.= (intloc 2) := (intloc 0 ) by A11, SCMFSA7B:7 ; :: thesis: ( s . (insloc 1) = goto (insloc 2) & s . (insloc 2) = (intloc 3) := (intloc 0 ) & s . (insloc 3) = goto (insloc 4) & s . (insloc 4) = (intloc 4) := (intloc 0 ) & s . (insloc 5) = goto (insloc 6) & s . (insloc 6) = (intloc 5) := (intloc 0 ) & s . (insloc 7) = goto (insloc 8) & s . (insloc 8) = (intloc 6) := (intloc 0 ) & s . (insloc 9) = goto (insloc 10) & s . (insloc 10) = (intloc 1) :=len (fsloc 0 ) & s . (insloc 11) = goto (insloc 12) )
thus s . (insloc 1) = (insert-sort (fsloc 0 )) . (insloc 1) by A2
.= (Directed (Macro ((intloc 2) := (intloc 0 )))) . (insloc 1) by B8, A10, SCMFSA8A:28
.= goto (insloc 2) by SCMFSA7B:8 ; :: thesis: ( s . (insloc 2) = (intloc 3) := (intloc 0 ) & s . (insloc 3) = goto (insloc 4) & s . (insloc 4) = (intloc 4) := (intloc 0 ) & s . (insloc 5) = goto (insloc 6) & s . (insloc 6) = (intloc 5) := (intloc 0 ) & s . (insloc 7) = goto (insloc 8) & s . (insloc 8) = (intloc 6) := (intloc 0 ) & s . (insloc 9) = goto (insloc 10) & s . (insloc 10) = (intloc 1) :=len (fsloc 0 ) & s . (insloc 11) = goto (insloc 12) )
A12: card (Macro ((intloc 2) := (intloc 0 ))) = 2 by SCMFSA7B:6;
thus s . (insloc 2) = (insert-sort (fsloc 0 )) . (insloc 2) by A2
.= (intloc 3) := (intloc 0 ) by A9, A12, SCMBSORT:51 ; :: thesis: ( s . (insloc 3) = goto (insloc 4) & s . (insloc 4) = (intloc 4) := (intloc 0 ) & s . (insloc 5) = goto (insloc 6) & s . (insloc 6) = (intloc 5) := (intloc 0 ) & s . (insloc 7) = goto (insloc 8) & s . (insloc 8) = (intloc 6) := (intloc 0 ) & s . (insloc 9) = goto (insloc 10) & s . (insloc 10) = (intloc 1) :=len (fsloc 0 ) & s . (insloc 11) = goto (insloc 12) )
thus s . (insloc 3) = (insert-sort (fsloc 0 )) . (insloc (2 + 1)) by A2
.= goto (insloc (2 + 2)) by A9, A12, SCMBSORT:51
.= goto (insloc 4) ; :: thesis: ( s . (insloc 4) = (intloc 4) := (intloc 0 ) & s . (insloc 5) = goto (insloc 6) & s . (insloc 6) = (intloc 5) := (intloc 0 ) & s . (insloc 7) = goto (insloc 8) & s . (insloc 8) = (intloc 6) := (intloc 0 ) & s . (insloc 9) = goto (insloc 10) & s . (insloc 10) = (intloc 1) :=len (fsloc 0 ) & s . (insloc 11) = goto (insloc 12) )
A13: 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 ;
thus s . (insloc 4) = (insert-sort (fsloc 0 )) . (insloc 4) by A2
.= (intloc 4) := (intloc 0 ) by A6, A13, SCMBSORT:51 ; :: thesis: ( s . (insloc 5) = goto (insloc 6) & s . (insloc 6) = (intloc 5) := (intloc 0 ) & s . (insloc 7) = goto (insloc 8) & s . (insloc 8) = (intloc 6) := (intloc 0 ) & s . (insloc 9) = goto (insloc 10) & s . (insloc 10) = (intloc 1) :=len (fsloc 0 ) & s . (insloc 11) = goto (insloc 12) )
thus s . (insloc 5) = (insert-sort (fsloc 0 )) . (insloc (4 + 1)) by A2
.= goto (insloc (4 + 2)) by A6, A13, SCMBSORT:51
.= goto (insloc 6) ; :: thesis: ( s . (insloc 6) = (intloc 5) := (intloc 0 ) & s . (insloc 7) = goto (insloc 8) & s . (insloc 8) = (intloc 6) := (intloc 0 ) & s . (insloc 9) = goto (insloc 10) & s . (insloc 10) = (intloc 1) :=len (fsloc 0 ) & s . (insloc 11) = goto (insloc 12) )
A14: card ((((intloc 2) := (intloc 0 )) ';' ((intloc 3) := (intloc 0 ))) ';' ((intloc 4) := (intloc 0 ))) = 6 by SCMBSORT:45;
thus s . (insloc 6) = (insert-sort (fsloc 0 )) . (insloc 6) by A2
.= (intloc 5) := (intloc 0 ) by A5, A14, SCMBSORT:51 ; :: thesis: ( s . (insloc 7) = goto (insloc 8) & s . (insloc 8) = (intloc 6) := (intloc 0 ) & s . (insloc 9) = goto (insloc 10) & s . (insloc 10) = (intloc 1) :=len (fsloc 0 ) & s . (insloc 11) = goto (insloc 12) )
thus s . (insloc 7) = (insert-sort (fsloc 0 )) . (insloc (6 + 1)) by A2
.= goto (insloc (6 + 2)) by A5, A14, SCMBSORT:51
.= goto (insloc 8) ; :: thesis: ( s . (insloc 8) = (intloc 6) := (intloc 0 ) & s . (insloc 9) = goto (insloc 10) & s . (insloc 10) = (intloc 1) :=len (fsloc 0 ) & s . (insloc 11) = goto (insloc 12) )
A15: 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 A14, SCMFSA6A:61
.= 6 + 2 by SCMFSA7B:6
.= 8 ;
thus s . (insloc 8) = (insert-sort (fsloc 0 )) . (insloc 8) by A2
.= (intloc 6) := (intloc 0 ) by A4, A15, SCMBSORT:51 ; :: thesis: ( s . (insloc 9) = goto (insloc 10) & s . (insloc 10) = (intloc 1) :=len (fsloc 0 ) & s . (insloc 11) = goto (insloc 12) )
thus s . (insloc 9) = (insert-sort (fsloc 0 )) . (insloc (8 + 1)) by A2
.= goto (insloc (8 + 2)) by A4, A15, SCMBSORT:51
.= goto (insloc 10) ; :: thesis: ( s . (insloc 10) = (intloc 1) :=len (fsloc 0 ) & s . (insloc 11) = goto (insloc 12) )
A16: 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 A15, SCMFSA6A:61
.= 8 + 2 by SCMFSA7B:6
.= 10 ;
thus s . (insloc 10) = (insert-sort (fsloc 0 )) . (insloc 10) by A2
.= (intloc 1) :=len (fsloc 0 ) by A3, A16, SCMBSORT:52 ; :: thesis: s . (insloc 11) = goto (insloc 12)
thus s . (insloc 11) = (insert-sort (fsloc 0 )) . (insloc (10 + 1)) by A2
.= goto (insloc (10 + 2)) by A3, A16, SCMBSORT:52
.= goto (insloc 12) ; :: thesis: verum