let s be State of ; :: thesis: ( Insert-Sort-Algorithm c= s & s starts_at 0 implies ( ( for k being Element of NAT st k > 0 & k < 12 holds
( (Computation s,k) . (IC SCM+FSA ) = insloc k & (Computation s,k) . (intloc 0 ) = s . (intloc 0 ) & (Computation s,k) . (fsloc 0 ) = s . (fsloc 0 ) ) ) & (Computation s,11) . (intloc 1) = len (s . (fsloc 0 )) & (Computation s,11) . (intloc 2) = s . (intloc 0 ) & (Computation s,11) . (intloc 3) = s . (intloc 0 ) & (Computation s,11) . (intloc 4) = s . (intloc 0 ) & (Computation s,11) . (intloc 5) = s . (intloc 0 ) & (Computation s,11) . (intloc 6) = s . (intloc 0 ) ) )
assume that
A1: Insert-Sort-Algorithm c= s and
A2: s starts_at 0 ; :: thesis: ( ( for k being Element of NAT st k > 0 & k < 12 holds
( (Computation s,k) . (IC SCM+FSA ) = insloc k & (Computation s,k) . (intloc 0 ) = s . (intloc 0 ) & (Computation s,k) . (fsloc 0 ) = s . (fsloc 0 ) ) ) & (Computation s,11) . (intloc 1) = len (s . (fsloc 0 )) & (Computation s,11) . (intloc 2) = s . (intloc 0 ) & (Computation s,11) . (intloc 3) = s . (intloc 0 ) & (Computation s,11) . (intloc 4) = s . (intloc 0 ) & (Computation s,11) . (intloc 5) = s . (intloc 0 ) & (Computation s,11) . (intloc 6) = s . (intloc 0 ) )
A3: Computation s,0 = s by AMI_1:13;
then A4: IC (Computation s,0 ) = insloc 0 by A2, AMI_1:def 41;
then A5: Computation s,(0 + 1) = Exec (s . (insloc 0 )),(Computation s,0 ) by AMI_1:55
.= Exec ((intloc 2) := (intloc 0 )),(Computation s,0 ) by A1, Lm1 ;
then A6: (Computation s,1) . (IC SCM+FSA ) = Next (IC (Computation s,0 )) by SCMFSA_2:89
.= insloc 1 by A4 ;
then IC (Computation s,1) = insloc 1 ;
then A7: Computation s,(1 + 1) = Exec (s . (insloc 1)),(Computation s,1) by AMI_1:55
.= Exec (goto (insloc 2)),(Computation s,1) by A1, Lm1 ;
then A8: (Computation s,2) . (IC SCM+FSA ) = insloc 2 by SCMFSA_2:95;
IC (Computation s,2) = insloc 2 by A7, SCMFSA_2:95;
then A9: Computation s,(2 + 1) = Exec (s . (insloc 2)),(Computation s,2) by AMI_1:55
.= Exec ((intloc 3) := (intloc 0 )),(Computation s,2) by A1, Lm1 ;
then A10: (Computation s,3) . (IC SCM+FSA ) = Next (IC (Computation s,2)) by SCMFSA_2:89
.= insloc 3 by A8 ;
then IC (Computation s,3) = insloc 3 ;
then A11: Computation s,(3 + 1) = Exec (s . (insloc 3)),(Computation s,3) by AMI_1:55
.= Exec (goto (insloc 4)),(Computation s,3) by A1, Lm1 ;
then A12: (Computation s,4) . (IC SCM+FSA ) = insloc 4 by SCMFSA_2:95;
A13: intloc 2 <> intloc 0 by AMI_3:52;
then A14: (Computation s,1) . (intloc 0 ) = s . (intloc 0 ) by A3, A5, SCMFSA_2:89;
then A15: (Computation s,2) . (intloc 0 ) = s . (intloc 0 ) by A7, SCMFSA_2:95;
then (Computation s,3) . (intloc 3) = s . (intloc 0 ) by A9, SCMFSA_2:89;
then A16: (Computation s,4) . (intloc 3) = s . (intloc 0 ) by A11, SCMFSA_2:95;
IC (Computation s,4) = insloc 4 by A11, SCMFSA_2:95;
then A17: Computation s,(4 + 1) = Exec (s . (insloc 4)),(Computation s,4) by AMI_1:55
.= Exec ((intloc 4) := (intloc 0 )),(Computation s,4) by A1, Lm1 ;
then A18: (Computation s,5) . (IC SCM+FSA ) = Next (IC (Computation s,4)) by SCMFSA_2:89
.= insloc 5 by A12 ;
then IC (Computation s,5) = insloc 5 ;
then A19: Computation s,(5 + 1) = Exec (s . (insloc 5)),(Computation s,5) by AMI_1:55
.= Exec (goto (insloc 6)),(Computation s,5) by A1, Lm1 ;
then A20: (Computation s,6) . (IC SCM+FSA ) = insloc 6 by SCMFSA_2:95;
IC (Computation s,6) = insloc 6 by A19, SCMFSA_2:95;
then A21: Computation s,(6 + 1) = Exec (s . (insloc 6)),(Computation s,6) by AMI_1:55
.= Exec ((intloc 5) := (intloc 0 )),(Computation s,6) by A1, Lm1 ;
then A22: (Computation s,7) . (IC SCM+FSA ) = Next (IC (Computation s,6)) by SCMFSA_2:89
.= insloc 7 by A20 ;
then IC (Computation s,7) = insloc 7 ;
then A23: Computation s,(7 + 1) = Exec (s . (insloc 7)),(Computation s,7) by AMI_1:55
.= Exec (goto (insloc 8)),(Computation s,7) by A1, Lm1 ;
then A24: (Computation s,8) . (IC SCM+FSA ) = insloc 8 by SCMFSA_2:95;
IC (Computation s,8) = insloc 8 by A23, SCMFSA_2:95;
then A25: Computation s,(8 + 1) = Exec (s . (insloc 8)),(Computation s,8) by AMI_1:55
.= Exec ((intloc 6) := (intloc 0 )),(Computation s,8) by A1, Lm1 ;
then A26: (Computation s,9) . (IC SCM+FSA ) = Next (IC (Computation s,8)) by SCMFSA_2:89
.= insloc 9 by A24 ;
then IC (Computation s,9) = insloc 9 ;
then A27: Computation s,(9 + 1) = Exec (s . (insloc 9)),(Computation s,9) by AMI_1:55
.= Exec (goto (insloc 10)),(Computation s,9) by A1, Lm1 ;
then A28: (Computation s,10) . (IC SCM+FSA ) = insloc 10 by SCMFSA_2:95;
A29: (Computation s,1) . (fsloc 0 ) = s . (fsloc 0 ) by A3, A5, SCMFSA_2:89;
then A30: (Computation s,2) . (fsloc 0 ) = s . (fsloc 0 ) by A7, SCMFSA_2:95;
then A31: (Computation s,3) . (fsloc 0 ) = s . (fsloc 0 ) by A9, SCMFSA_2:89;
then A32: (Computation s,4) . (fsloc 0 ) = s . (fsloc 0 ) by A11, SCMFSA_2:95;
then A33: (Computation s,5) . (fsloc 0 ) = s . (fsloc 0 ) by A17, SCMFSA_2:89;
then A34: (Computation s,6) . (fsloc 0 ) = s . (fsloc 0 ) by A19, SCMFSA_2:95;
then A35: (Computation s,7) . (fsloc 0 ) = s . (fsloc 0 ) by A21, SCMFSA_2:89;
then A36: (Computation s,8) . (fsloc 0 ) = s . (fsloc 0 ) by A23, SCMFSA_2:95;
then A37: (Computation s,9) . (fsloc 0 ) = s . (fsloc 0 ) by A25, SCMFSA_2:89;
then A38: (Computation s,10) . (fsloc 0 ) = s . (fsloc 0 ) by A27, SCMFSA_2:95;
A39: (Computation s,3) . (intloc 0 ) = s . (intloc 0 ) by A15, A9, SCMFSA_2:89;
then A40: (Computation s,4) . (intloc 0 ) = s . (intloc 0 ) by A11, SCMFSA_2:95;
then (Computation s,5) . (intloc 4) = s . (intloc 0 ) by A17, SCMFSA_2:89;
then A41: (Computation s,6) . (intloc 4) = s . (intloc 0 ) by A19, SCMFSA_2:95;
A42: intloc 4 <> intloc 0 by AMI_3:52;
then A43: (Computation s,5) . (intloc 0 ) = s . (intloc 0 ) by A40, A17, SCMFSA_2:89;
then A44: (Computation s,6) . (intloc 0 ) = s . (intloc 0 ) by A19, SCMFSA_2:95;
then (Computation s,7) . (intloc 5) = s . (intloc 0 ) by A21, SCMFSA_2:89;
then A45: (Computation s,8) . (intloc 5) = s . (intloc 0 ) by A23, SCMFSA_2:95;
intloc 4 <> intloc 5 by AMI_3:52;
then (Computation s,7) . (intloc 4) = s . (intloc 0 ) by A41, A21, SCMFSA_2:89;
then A46: (Computation s,8) . (intloc 4) = s . (intloc 0 ) by A23, SCMFSA_2:95;
intloc 4 <> intloc 6 by AMI_3:52;
then (Computation s,9) . (intloc 4) = s . (intloc 0 ) by A46, A25, SCMFSA_2:89;
then A47: (Computation s,10) . (intloc 4) = s . (intloc 0 ) by A27, SCMFSA_2:95;
intloc 5 <> intloc 6 by AMI_3:52;
then (Computation s,9) . (intloc 5) = s . (intloc 0 ) by A45, A25, SCMFSA_2:89;
then A48: (Computation s,10) . (intloc 5) = s . (intloc 0 ) by A27, SCMFSA_2:95;
A49: intloc 5 <> intloc 0 by AMI_3:52;
then A50: (Computation s,7) . (intloc 0 ) = s . (intloc 0 ) by A44, A21, SCMFSA_2:89;
then A51: (Computation s,8) . (intloc 0 ) = s . (intloc 0 ) by A23, SCMFSA_2:95;
then (Computation s,9) . (intloc 6) = s . (intloc 0 ) by A25, SCMFSA_2:89;
then A52: (Computation s,10) . (intloc 6) = s . (intloc 0 ) by A27, SCMFSA_2:95;
IC (Computation s,10) = insloc 10 by A27, SCMFSA_2:95;
then A53: Computation s,(10 + 1) = Exec (s . (insloc 10)),(Computation s,10) by AMI_1:55
.= Exec ((intloc 1) :=len (fsloc 0 )),(Computation s,10) by A1, Lm1 ;
then A54: (Computation s,11) . (IC SCM+FSA ) = Next (IC (Computation s,10)) by SCMFSA_2:100
.= insloc 11 by A28 ;
A55: intloc 6 <> intloc 0 by AMI_3:52;
then A56: (Computation s,9) . (intloc 0 ) = s . (intloc 0 ) by A51, A25, SCMFSA_2:89;
then A57: (Computation s,10) . (intloc 0 ) = s . (intloc 0 ) by A27, SCMFSA_2:95;

hereby :: thesis: ( (Computation s,11) . (intloc 1) = len (s . (fsloc 0 )) & (Computation s,11) . (intloc 2) = s . (intloc 0 ) & (Computation s,11) . (intloc 3) = s . (intloc 0 ) & (Computation s,11) . (intloc 4) = s . (intloc 0 ) & (Computation s,11) . (intloc 5) = s . (intloc 0 ) & (Computation s,11) . (intloc 6) = s . (intloc 0 ) )

let k be Element of NAT ; :: thesis: ( k > 0 & k < 12 implies ( (Computation s,b₁) . (IC SCM+FSA ) = insloc b₁ & (Computation s,b₁) . (intloc 0 ) = s . (intloc 0 ) & (Computation s,b₁) . (fsloc 0 ) = s . (fsloc 0 ) ) )
assume that
A58: k > 0 and
A59: k < 12 ; :: thesis: ( (Computation s,b₁) . (IC SCM+FSA ) = insloc b₁ & (Computation s,b₁) . (intloc 0 ) = s . (intloc 0 ) & (Computation s,b₁) . (fsloc 0 ) = s . (fsloc 0 ) )
set c1 = (Computation s,k) . (IC SCM+FSA );
set d1 = insloc k;
set c2 = (Computation s,k) . (intloc 0 );
set d2 = s . (intloc 0 );
set c3 = (Computation s,k) . (fsloc 0 );
set d3 = s . (fsloc 0 );
k < 11 + 1 by A59;
then A60: k <= 11 by NAT_1:13;

per cases ( 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 A58, A60, NAT_1:36;

suppose k = 1 ; :: thesis: ( (Computation s,b₁) . (IC SCM+FSA ) = insloc b₁ & (Computation s,b₁) . (intloc 0 ) = s . (intloc 0 ) & (Computation s,b₁) . (fsloc 0 ) = s . (fsloc 0 ) )

hence ( (Computation s,k) . (IC SCM+FSA ) = insloc k & (Computation s,k) . (intloc 0 ) = s . (intloc 0 ) & (Computation s,k) . (fsloc 0 ) = s . (fsloc 0 ) ) by A3, A5, A6, A13, SCMFSA_2:89; :: thesis: verum

end;

suppose k = 2 ; :: thesis: ( (Computation s,b₁) . (IC SCM+FSA ) = insloc b₁ & (Computation s,b₁) . (intloc 0 ) = s . (intloc 0 ) & (Computation s,b₁) . (fsloc 0 ) = s . (fsloc 0 ) )

hence ( (Computation s,k) . (IC SCM+FSA ) = insloc k & (Computation s,k) . (intloc 0 ) = s . (intloc 0 ) & (Computation s,k) . (fsloc 0 ) = s . (fsloc 0 ) ) by A14, A29, A7, SCMFSA_2:95; :: thesis: verum

end;

suppose k = 3 ; :: thesis: ( (Computation s,b₁) . (IC SCM+FSA ) = insloc b₁ & (Computation s,b₁) . (intloc 0 ) = s . (intloc 0 ) & (Computation s,b₁) . (fsloc 0 ) = s . (fsloc 0 ) )

hence ( (Computation s,k) . (IC SCM+FSA ) = insloc k & (Computation s,k) . (intloc 0 ) = s . (intloc 0 ) & (Computation s,k) . (fsloc 0 ) = s . (fsloc 0 ) ) by A15, A30, A9, A10, SCMFSA_2:89; :: thesis: verum

end;

suppose k = 4 ; :: thesis: ( (Computation s,b₁) . (IC SCM+FSA ) = insloc b₁ & (Computation s,b₁) . (intloc 0 ) = s . (intloc 0 ) & (Computation s,b₁) . (fsloc 0 ) = s . (fsloc 0 ) )

hence ( (Computation s,k) . (IC SCM+FSA ) = insloc k & (Computation s,k) . (intloc 0 ) = s . (intloc 0 ) & (Computation s,k) . (fsloc 0 ) = s . (fsloc 0 ) ) by A39, A31, A11, SCMFSA_2:95; :: thesis: verum

end;

suppose k = 5 ; :: thesis: ( (Computation s,b₁) . (IC SCM+FSA ) = insloc b₁ & (Computation s,b₁) . (intloc 0 ) = s . (intloc 0 ) & (Computation s,b₁) . (fsloc 0 ) = s . (fsloc 0 ) )

hence ( (Computation s,k) . (IC SCM+FSA ) = insloc k & (Computation s,k) . (intloc 0 ) = s . (intloc 0 ) & (Computation s,k) . (fsloc 0 ) = s . (fsloc 0 ) ) by A40, A32, A17, A18, A42, SCMFSA_2:89; :: thesis: verum

end;

suppose k = 6 ; :: thesis: ( (Computation s,b₁) . (IC SCM+FSA ) = insloc b₁ & (Computation s,b₁) . (intloc 0 ) = s . (intloc 0 ) & (Computation s,b₁) . (fsloc 0 ) = s . (fsloc 0 ) )

hence ( (Computation s,k) . (IC SCM+FSA ) = insloc k & (Computation s,k) . (intloc 0 ) = s . (intloc 0 ) & (Computation s,k) . (fsloc 0 ) = s . (fsloc 0 ) ) by A43, A33, A19, SCMFSA_2:95; :: thesis: verum

end;

suppose k = 7 ; :: thesis: ( (Computation s,b₁) . (IC SCM+FSA ) = insloc b₁ & (Computation s,b₁) . (intloc 0 ) = s . (intloc 0 ) & (Computation s,b₁) . (fsloc 0 ) = s . (fsloc 0 ) )

hence ( (Computation s,k) . (IC SCM+FSA ) = insloc k & (Computation s,k) . (intloc 0 ) = s . (intloc 0 ) & (Computation s,k) . (fsloc 0 ) = s . (fsloc 0 ) ) by A44, A34, A21, A22, A49, SCMFSA_2:89; :: thesis: verum

end;

suppose k = 8 ; :: thesis: ( (Computation s,b₁) . (IC SCM+FSA ) = insloc b₁ & (Computation s,b₁) . (intloc 0 ) = s . (intloc 0 ) & (Computation s,b₁) . (fsloc 0 ) = s . (fsloc 0 ) )

hence ( (Computation s,k) . (IC SCM+FSA ) = insloc k & (Computation s,k) . (intloc 0 ) = s . (intloc 0 ) & (Computation s,k) . (fsloc 0 ) = s . (fsloc 0 ) ) by A50, A35, A23, SCMFSA_2:95; :: thesis: verum

end;

suppose k = 9 ; :: thesis: ( (Computation s,b₁) . (IC SCM+FSA ) = insloc b₁ & (Computation s,b₁) . (intloc 0 ) = s . (intloc 0 ) & (Computation s,b₁) . (fsloc 0 ) = s . (fsloc 0 ) )

hence ( (Computation s,k) . (IC SCM+FSA ) = insloc k & (Computation s,k) . (intloc 0 ) = s . (intloc 0 ) & (Computation s,k) . (fsloc 0 ) = s . (fsloc 0 ) ) by A51, A36, A25, A26, A55, SCMFSA_2:89; :: thesis: verum

end;

suppose k = 10 ; :: thesis: ( (Computation s,b₁) . (IC SCM+FSA ) = insloc b₁ & (Computation s,b₁) . (intloc 0 ) = s . (intloc 0 ) & (Computation s,b₁) . (fsloc 0 ) = s . (fsloc 0 ) )

hence ( (Computation s,k) . (IC SCM+FSA ) = insloc k & (Computation s,k) . (intloc 0 ) = s . (intloc 0 ) & (Computation s,k) . (fsloc 0 ) = s . (fsloc 0 ) ) by A56, A37, A27, SCMFSA_2:95; :: thesis: verum

end;

suppose k = 11 ; :: thesis: ( (Computation s,b₁) . (IC SCM+FSA ) = insloc b₁ & (Computation s,b₁) . (intloc 0 ) = s . (intloc 0 ) & (Computation s,b₁) . (fsloc 0 ) = s . (fsloc 0 ) )

hence ( (Computation s,k) . (IC SCM+FSA ) = insloc k & (Computation s,k) . (intloc 0 ) = s . (intloc 0 ) & (Computation s,k) . (fsloc 0 ) = s . (fsloc 0 ) ) by A57, A38, A53, A54, SCMFSA_2:100; :: thesis: verum

end;

end;

end;

thus (Computation s,11) . (intloc 1) = len (s . (fsloc 0 )) by A38, A53, SCMFSA_2:100; :: thesis: ( (Computation s,11) . (intloc 2) = s . (intloc 0 ) & (Computation s,11) . (intloc 3) = s . (intloc 0 ) & (Computation s,11) . (intloc 4) = s . (intloc 0 ) & (Computation s,11) . (intloc 5) = s . (intloc 0 ) & (Computation s,11) . (intloc 6) = s . (intloc 0 ) )
(Computation s,1) . (intloc 2) = s . (intloc 0 ) by A3, A5, SCMFSA_2:89;
then A61: (Computation s,2) . (intloc 2) = s . (intloc 0 ) by A7, SCMFSA_2:95;
intloc 2 <> intloc 3 by AMI_3:52;
then (Computation s,3) . (intloc 2) = s . (intloc 0 ) by A61, A9, SCMFSA_2:89;
then A62: (Computation s,4) . (intloc 2) = s . (intloc 0 ) by A11, SCMFSA_2:95;
intloc 2 <> intloc 4 by AMI_3:52;
then (Computation s,5) . (intloc 2) = s . (intloc 0 ) by A62, A17, SCMFSA_2:89;
then A63: (Computation s,6) . (intloc 2) = s . (intloc 0 ) by A19, SCMFSA_2:95;
intloc 2 <> intloc 5 by AMI_3:52;
then (Computation s,7) . (intloc 2) = s . (intloc 0 ) by A63, A21, SCMFSA_2:89;
then A64: (Computation s,8) . (intloc 2) = s . (intloc 0 ) by A23, SCMFSA_2:95;
intloc 2 <> intloc 6 by AMI_3:52;
then (Computation s,9) . (intloc 2) = s . (intloc 0 ) by A64, A25, SCMFSA_2:89;
then A65: (Computation s,10) . (intloc 2) = s . (intloc 0 ) by A27, SCMFSA_2:95;
intloc 3 <> intloc 4 by AMI_3:52;
then (Computation s,5) . (intloc 3) = s . (intloc 0 ) by A16, A17, SCMFSA_2:89;
then A66: (Computation s,6) . (intloc 3) = s . (intloc 0 ) by A19, SCMFSA_2:95;
intloc 3 <> intloc 5 by AMI_3:52;
then (Computation s,7) . (intloc 3) = s . (intloc 0 ) by A66, A21, SCMFSA_2:89;
then A67: (Computation s,8) . (intloc 3) = s . (intloc 0 ) by A23, SCMFSA_2:95;
intloc 3 <> intloc 6 by AMI_3:52;
then (Computation s,9) . (intloc 3) = s . (intloc 0 ) by A67, A25, SCMFSA_2:89;
then A68: (Computation s,10) . (intloc 3) = s . (intloc 0 ) by A27, SCMFSA_2:95;
intloc 2 <> intloc 1 by AMI_3:52;
hence (Computation s,11) . (intloc 2) = s . (intloc 0 ) by A65, A53, SCMFSA_2:100; :: thesis: ( (Computation s,11) . (intloc 3) = s . (intloc 0 ) & (Computation s,11) . (intloc 4) = s . (intloc 0 ) & (Computation s,11) . (intloc 5) = s . (intloc 0 ) & (Computation s,11) . (intloc 6) = s . (intloc 0 ) )
intloc 3 <> intloc 1 by AMI_3:52;
hence (Computation s,11) . (intloc 3) = s . (intloc 0 ) by A68, A53, SCMFSA_2:100; :: thesis: ( (Computation s,11) . (intloc 4) = s . (intloc 0 ) & (Computation s,11) . (intloc 5) = s . (intloc 0 ) & (Computation s,11) . (intloc 6) = s . (intloc 0 ) )
intloc 4 <> intloc 1 by AMI_3:52;
hence (Computation s,11) . (intloc 4) = s . (intloc 0 ) by A47, A53, SCMFSA_2:100; :: thesis: ( (Computation s,11) . (intloc 5) = s . (intloc 0 ) & (Computation s,11) . (intloc 6) = s . (intloc 0 ) )
intloc 5 <> intloc 1 by AMI_3:52;
hence (Computation s,11) . (intloc 5) = s . (intloc 0 ) by A48, A53, SCMFSA_2:100; :: thesis: (Computation s,11) . (intloc 6) = s . (intloc 0 )
intloc 6 <> intloc 1 by AMI_3:52;
hence (Computation s,11) . (intloc 6) = s . (intloc 0 ) by A52, A53, SCMFSA_2:100; :: thesis: verum