let s be 0 -started State of SCM+FSA; :: thesis: for P being Instruction-Sequence of SCM+FSA st Insert-Sort-Algorithm c= P holds
( ( for k being Nat st k > 0 & k < 12 holds
( (Comput (P,s,k)) . () = k & (Comput (P,s,k)) . () = s . () & (Comput (P,s,k)) . () = s . () ) ) & (Comput (P,s,11)) . () = len (s . ()) & (Comput (P,s,11)) . () = s . () & (Comput (P,s,11)) . () = s . () & (Comput (P,s,11)) . () = s . () & (Comput (P,s,11)) . () = s . () & (Comput (P,s,11)) . () = s . () )

let P be Instruction-Sequence of SCM+FSA; :: thesis: ( Insert-Sort-Algorithm c= P implies ( ( for k being Nat st k > 0 & k < 12 holds
( (Comput (P,s,k)) . () = k & (Comput (P,s,k)) . () = s . () & (Comput (P,s,k)) . () = s . () ) ) & (Comput (P,s,11)) . () = len (s . ()) & (Comput (P,s,11)) . () = s . () & (Comput (P,s,11)) . () = s . () & (Comput (P,s,11)) . () = s . () & (Comput (P,s,11)) . () = s . () & (Comput (P,s,11)) . () = s . () ) )

assume A1: Insert-Sort-Algorithm c= P ; :: thesis: ( ( for k being Nat st k > 0 & k < 12 holds
( (Comput (P,s,k)) . () = k & (Comput (P,s,k)) . () = s . () & (Comput (P,s,k)) . () = s . () ) ) & (Comput (P,s,11)) . () = len (s . ()) & (Comput (P,s,11)) . () = s . () & (Comput (P,s,11)) . () = s . () & (Comput (P,s,11)) . () = s . () & (Comput (P,s,11)) . () = s . () & (Comput (P,s,11)) . () = s . () )

A2: IC (Comput (P,s,0)) = 0 by MEMSTR_0:def 11;
then A3: Comput (P,s,(0 + 1)) = Exec ((P . 0),(Comput (P,s,0))) by EXTPRO_1:6
.= Exec ((() := ()),(Comput (P,s,0))) by ;
then A4: (Comput (P,s,1)) . () = (IC (Comput (P,s,0))) + 1 by SCMFSA_2:63
.= 1 by A2 ;
then IC (Comput (P,s,1)) = 1 ;
then A5: Comput (P,s,(1 + 1)) = Exec ((P . 1),(Comput (P,s,1))) by EXTPRO_1:6
.= Exec ((goto 2),(Comput (P,s,1))) by ;
then A6: (Comput (P,s,2)) . () = 2 by SCMFSA_2:69;
IC (Comput (P,s,2)) = 2 by ;
then A7: Comput (P,s,(2 + 1)) = Exec ((P . 2),(Comput (P,s,2))) by EXTPRO_1:6
.= Exec ((() := ()),(Comput (P,s,2))) by ;
then A8: (Comput (P,s,3)) . () = (IC (Comput (P,s,2))) + 1 by SCMFSA_2:63
.= 3 by A6 ;
then IC (Comput (P,s,3)) = 3 ;
then A9: Comput (P,s,(3 + 1)) = Exec ((P . 3),(Comput (P,s,3))) by EXTPRO_1:6
.= Exec ((goto 4),(Comput (P,s,3))) by ;
then A10: (Comput (P,s,4)) . () = 4 by SCMFSA_2:69;
A11: intloc 2 <> intloc 0 by SCMFSA_2:101;
then A12: (Comput (P,s,1)) . () = s . () by ;
then A13: (Comput (P,s,2)) . () = s . () by ;
then (Comput (P,s,3)) . () = s . () by ;
then A14: (Comput (P,s,4)) . () = s . () by ;
IC (Comput (P,s,4)) = 4 by ;
then A15: Comput (P,s,(4 + 1)) = Exec ((P . 4),(Comput (P,s,4))) by EXTPRO_1:6
.= Exec ((() := ()),(Comput (P,s,4))) by ;
then A16: (Comput (P,s,5)) . () = (IC (Comput (P,s,4))) + 1 by SCMFSA_2:63
.= 5 by A10 ;
then IC (Comput (P,s,5)) = 5 ;
then A17: Comput (P,s,(5 + 1)) = Exec ((P . 5),(Comput (P,s,5))) by EXTPRO_1:6
.= Exec ((goto 6),(Comput (P,s,5))) by ;
then A18: (Comput (P,s,6)) . () = 6 by SCMFSA_2:69;
IC (Comput (P,s,6)) = 6 by ;
then A19: Comput (P,s,(6 + 1)) = Exec ((P . 6),(Comput (P,s,6))) by EXTPRO_1:6
.= Exec ((() := ()),(Comput (P,s,6))) by ;
then A20: (Comput (P,s,7)) . () = (IC (Comput (P,s,6))) + 1 by SCMFSA_2:63
.= 7 by A18 ;
then IC (Comput (P,s,7)) = 7 ;
then A21: Comput (P,s,(7 + 1)) = Exec ((P . 7),(Comput (P,s,7))) by EXTPRO_1:6
.= Exec ((goto 8),(Comput (P,s,7))) by ;
then A22: (Comput (P,s,8)) . () = 8 by SCMFSA_2:69;
IC (Comput (P,s,8)) = 8 by ;
then A23: Comput (P,s,(8 + 1)) = Exec ((P . 8),(Comput (P,s,8))) by EXTPRO_1:6
.= Exec ((() := ()),(Comput (P,s,8))) by ;
then A24: (Comput (P,s,9)) . () = (IC (Comput (P,s,8))) + 1 by SCMFSA_2:63
.= 9 by A22 ;
then IC (Comput (P,s,9)) = 9 ;
then A25: Comput (P,s,(9 + 1)) = Exec ((P . 9),(Comput (P,s,9))) by EXTPRO_1:6
.= Exec ((goto 10),(Comput (P,s,9))) by ;
then A26: (Comput (P,s,10)) . () = 10 by SCMFSA_2:69;
A27: (Comput (P,s,1)) . () = s . () by ;
then A28: (Comput (P,s,2)) . () = s . () by ;
then A29: (Comput (P,s,3)) . () = s . () by ;
then A30: (Comput (P,s,4)) . () = s . () by ;
then A31: (Comput (P,s,5)) . () = s . () by ;
then A32: (Comput (P,s,6)) . () = s . () by ;
then A33: (Comput (P,s,7)) . () = s . () by ;
then A34: (Comput (P,s,8)) . () = s . () by ;
then A35: (Comput (P,s,9)) . () = s . () by ;
then A36: (Comput (P,s,10)) . () = s . () by ;
A37: (Comput (P,s,3)) . () = s . () by ;
then A38: (Comput (P,s,4)) . () = s . () by ;
then (Comput (P,s,5)) . () = s . () by ;
then A39: (Comput (P,s,6)) . () = s . () by ;
A40: intloc 4 <> intloc 0 by SCMFSA_2:101;
then A41: (Comput (P,s,5)) . () = s . () by ;
then A42: (Comput (P,s,6)) . () = s . () by ;
then (Comput (P,s,7)) . () = s . () by ;
then A43: (Comput (P,s,8)) . () = s . () by ;
intloc 4 <> intloc 5 by SCMFSA_2:101;
then (Comput (P,s,7)) . () = s . () by ;
then A44: (Comput (P,s,8)) . () = s . () by ;
intloc 4 <> intloc 6 by SCMFSA_2:101;
then (Comput (P,s,9)) . () = s . () by ;
then A45: (Comput (P,s,10)) . () = s . () by ;
intloc 5 <> intloc 6 by SCMFSA_2:101;
then (Comput (P,s,9)) . () = s . () by ;
then A46: (Comput (P,s,10)) . () = s . () by ;
A47: intloc 5 <> intloc 0 by SCMFSA_2:101;
then A48: (Comput (P,s,7)) . () = s . () by ;
then A49: (Comput (P,s,8)) . () = s . () by ;
then (Comput (P,s,9)) . () = s . () by ;
then A50: (Comput (P,s,10)) . () = s . () by ;
IC (Comput (P,s,10)) = 10 by ;
then A51: Comput (P,s,(10 + 1)) = Exec ((P . 10),(Comput (P,s,10))) by EXTPRO_1:6
.= Exec ((() :=len ()),(Comput (P,s,10))) by ;
then A52: (Comput (P,s,11)) . () = (IC (Comput (P,s,10))) + 1 by SCMFSA_2:74
.= 11 by A26 ;
A53: intloc 6 <> intloc 0 by SCMFSA_2:101;
then A54: (Comput (P,s,9)) . () = s . () by ;
then A55: (Comput (P,s,10)) . () = s . () by ;
hereby :: thesis: ( (Comput (P,s,11)) . () = len (s . ()) & (Comput (P,s,11)) . () = s . () & (Comput (P,s,11)) . () = s . () & (Comput (P,s,11)) . () = s . () & (Comput (P,s,11)) . () = s . () & (Comput (P,s,11)) . () = s . () )
let k be Nat; :: thesis: ( k > 0 & k < 12 implies ( (Comput (P,s,b1)) . () = b1 & (Comput (P,s,b1)) . () = s . () & (Comput (P,s,b1)) . () = s . () ) )
assume that
A56: k > 0 and
A57: k < 12 ; :: thesis: ( (Comput (P,s,b1)) . () = b1 & (Comput (P,s,b1)) . () = s . () & (Comput (P,s,b1)) . () = s . () )
set c1 = (Comput (P,s,k)) . ();
set d1 = k;
set c2 = (Comput (P,s,k)) . ();
set d2 = s . ();
set c3 = (Comput (P,s,k)) . ();
set d3 = s . ();
k < 11 + 1 by A57;
then k <= 11 by NAT_1:13;
then not not k = 0 & ... & not k = 11 ;
per cases then ( k = 1 or k = 2 or k = 3 or k = 4 or k = 5 or k = 6 or k = 7 or k = 8 or k = 9 or k = 10 or k = 11 ) by A56;
suppose k = 1 ; :: thesis: ( (Comput (P,s,b1)) . () = b1 & (Comput (P,s,b1)) . () = s . () & (Comput (P,s,b1)) . () = s . () )
hence ( (Comput (P,s,k)) . () = k & (Comput (P,s,k)) . () = s . () & (Comput (P,s,k)) . () = s . () ) by ; :: thesis: verum
end;
suppose k = 2 ; :: thesis: ( (Comput (P,s,b1)) . () = b1 & (Comput (P,s,b1)) . () = s . () & (Comput (P,s,b1)) . () = s . () )
hence ( (Comput (P,s,k)) . () = k & (Comput (P,s,k)) . () = s . () & (Comput (P,s,k)) . () = s . () ) by ; :: thesis: verum
end;
suppose k = 3 ; :: thesis: ( (Comput (P,s,b1)) . () = b1 & (Comput (P,s,b1)) . () = s . () & (Comput (P,s,b1)) . () = s . () )
hence ( (Comput (P,s,k)) . () = k & (Comput (P,s,k)) . () = s . () & (Comput (P,s,k)) . () = s . () ) by ; :: thesis: verum
end;
suppose k = 4 ; :: thesis: ( (Comput (P,s,b1)) . () = b1 & (Comput (P,s,b1)) . () = s . () & (Comput (P,s,b1)) . () = s . () )
hence ( (Comput (P,s,k)) . () = k & (Comput (P,s,k)) . () = s . () & (Comput (P,s,k)) . () = s . () ) by ; :: thesis: verum
end;
suppose k = 5 ; :: thesis: ( (Comput (P,s,b1)) . () = b1 & (Comput (P,s,b1)) . () = s . () & (Comput (P,s,b1)) . () = s . () )
hence ( (Comput (P,s,k)) . () = k & (Comput (P,s,k)) . () = s . () & (Comput (P,s,k)) . () = s . () ) by ; :: thesis: verum
end;
suppose k = 6 ; :: thesis: ( (Comput (P,s,b1)) . () = b1 & (Comput (P,s,b1)) . () = s . () & (Comput (P,s,b1)) . () = s . () )
hence ( (Comput (P,s,k)) . () = k & (Comput (P,s,k)) . () = s . () & (Comput (P,s,k)) . () = s . () ) by ; :: thesis: verum
end;
suppose k = 7 ; :: thesis: ( (Comput (P,s,b1)) . () = b1 & (Comput (P,s,b1)) . () = s . () & (Comput (P,s,b1)) . () = s . () )
hence ( (Comput (P,s,k)) . () = k & (Comput (P,s,k)) . () = s . () & (Comput (P,s,k)) . () = s . () ) by ; :: thesis: verum
end;
suppose k = 8 ; :: thesis: ( (Comput (P,s,b1)) . () = b1 & (Comput (P,s,b1)) . () = s . () & (Comput (P,s,b1)) . () = s . () )
hence ( (Comput (P,s,k)) . () = k & (Comput (P,s,k)) . () = s . () & (Comput (P,s,k)) . () = s . () ) by ; :: thesis: verum
end;
suppose k = 9 ; :: thesis: ( (Comput (P,s,b1)) . () = b1 & (Comput (P,s,b1)) . () = s . () & (Comput (P,s,b1)) . () = s . () )
hence ( (Comput (P,s,k)) . () = k & (Comput (P,s,k)) . () = s . () & (Comput (P,s,k)) . () = s . () ) by ; :: thesis: verum
end;
suppose k = 10 ; :: thesis: ( (Comput (P,s,b1)) . () = b1 & (Comput (P,s,b1)) . () = s . () & (Comput (P,s,b1)) . () = s . () )
hence ( (Comput (P,s,k)) . () = k & (Comput (P,s,k)) . () = s . () & (Comput (P,s,k)) . () = s . () ) by ; :: thesis: verum
end;
suppose A58: k = 11 ; :: thesis: ( (Comput (P,s,b1)) . () = b1 & (Comput (P,s,b1)) . () = s . () & (Comput (P,s,b1)) . () = s . () )
hence (Comput (P,s,k)) . () = k by A52; :: thesis: ( (Comput (P,s,k)) . () = s . () & (Comput (P,s,k)) . () = s . () )
thus (Comput (P,s,k)) . () = s . () by ; :: thesis: (Comput (P,s,k)) . () = s . ()
thus (Comput (P,s,k)) . () = s . () by ; :: thesis: verum
end;
end;
end;
thus (Comput (P,s,11)) . () = len (s . ()) by ; :: thesis: ( (Comput (P,s,11)) . () = s . () & (Comput (P,s,11)) . () = s . () & (Comput (P,s,11)) . () = s . () & (Comput (P,s,11)) . () = s . () & (Comput (P,s,11)) . () = s . () )
(Comput (P,s,1)) . () = s . () by ;
then A59: (Comput (P,s,2)) . () = s . () by ;
intloc 2 <> intloc 3 by SCMFSA_2:101;
then (Comput (P,s,3)) . () = s . () by ;
then A60: (Comput (P,s,4)) . () = s . () by ;
intloc 2 <> intloc 4 by SCMFSA_2:101;
then (Comput (P,s,5)) . () = s . () by ;
then A61: (Comput (P,s,6)) . () = s . () by ;
intloc 2 <> intloc 5 by SCMFSA_2:101;
then (Comput (P,s,7)) . () = s . () by ;
then A62: (Comput (P,s,8)) . () = s . () by ;
intloc 2 <> intloc 6 by SCMFSA_2:101;
then (Comput (P,s,9)) . () = s . () by ;
then A63: (Comput (P,s,10)) . () = s . () by ;
intloc 3 <> intloc 4 by SCMFSA_2:101;
then (Comput (P,s,5)) . () = s . () by ;
then A64: (Comput (P,s,6)) . () = s . () by ;
intloc 3 <> intloc 5 by SCMFSA_2:101;
then (Comput (P,s,7)) . () = s . () by ;
then A65: (Comput (P,s,8)) . () = s . () by ;
intloc 3 <> intloc 6 by SCMFSA_2:101;
then (Comput (P,s,9)) . () = s . () by ;
then A66: (Comput (P,s,10)) . () = s . () by ;
intloc 2 <> intloc 1 by SCMFSA_2:101;
hence (Comput (P,s,11)) . () = s . () by ; :: thesis: ( (Comput (P,s,11)) . () = s . () & (Comput (P,s,11)) . () = s . () & (Comput (P,s,11)) . () = s . () & (Comput (P,s,11)) . () = s . () )
intloc 3 <> intloc 1 by SCMFSA_2:101;
hence (Comput (P,s,11)) . () = s . () by ; :: thesis: ( (Comput (P,s,11)) . () = s . () & (Comput (P,s,11)) . () = s . () & (Comput (P,s,11)) . () = s . () )
intloc 4 <> intloc 1 by SCMFSA_2:101;
hence (Comput (P,s,11)) . () = s . () by ; :: thesis: ( (Comput (P,s,11)) . () = s . () & (Comput (P,s,11)) . () = s . () )
intloc 5 <> intloc 1 by SCMFSA_2:101;
hence (Comput (P,s,11)) . () = s . () by ; :: thesis: (Comput (P,s,11)) . () = s . ()
intloc 6 <> intloc 1 by SCMFSA_2:101;
hence (Comput (P,s,11)) . () = s . () by ; :: thesis: verum