let s be 0 -started State of SCM+FSA ; :: thesis: ( Insert-Sort-Algorithm c= s implies ( ( for k being Element of NAT st k > 0 & k < 12 holds
( (Comput (ProgramPart s),s,k) . (IC SCM+FSA ) = k & (Comput (ProgramPart s),s,k) . (intloc 0 ) = s . (intloc 0 ) & (Comput (ProgramPart s),s,k) . (fsloc 0 ) = s . (fsloc 0 ) ) ) & (Comput (ProgramPart s),s,11) . (intloc 1) = len (s . (fsloc 0 )) & (Comput (ProgramPart s),s,11) . (intloc 2) = s . (intloc 0 ) & (Comput (ProgramPart s),s,11) . (intloc 3) = s . (intloc 0 ) & (Comput (ProgramPart s),s,11) . (intloc 4) = s . (intloc 0 ) & (Comput (ProgramPart s),s,11) . (intloc 5) = s . (intloc 0 ) & (Comput (ProgramPart s),s,11) . (intloc 6) = s . (intloc 0 ) ) )
assume A1: Insert-Sort-Algorithm c= s ; :: thesis: ( ( for k being Element of NAT st k > 0 & k < 12 holds
( (Comput (ProgramPart s),s,k) . (IC SCM+FSA ) = k & (Comput (ProgramPart s),s,k) . (intloc 0 ) = s . (intloc 0 ) & (Comput (ProgramPart s),s,k) . (fsloc 0 ) = s . (fsloc 0 ) ) ) & (Comput (ProgramPart s),s,11) . (intloc 1) = len (s . (fsloc 0 )) & (Comput (ProgramPart s),s,11) . (intloc 2) = s . (intloc 0 ) & (Comput (ProgramPart s),s,11) . (intloc 3) = s . (intloc 0 ) & (Comput (ProgramPart s),s,11) . (intloc 4) = s . (intloc 0 ) & (Comput (ProgramPart s),s,11) . (intloc 5) = s . (intloc 0 ) & (Comput (ProgramPart s),s,11) . (intloc 6) = s . (intloc 0 ) )
X0: (ProgramPart s) . 0 = s . 0 by COMPOS_1:2;
X1: (ProgramPart s) . 1 = s . 1 by COMPOS_1:2;
X2: (ProgramPart s) . 2 = s . 2 by COMPOS_1:2;
X3: (ProgramPart s) . 3 = s . 3 by COMPOS_1:2;
X4: (ProgramPart s) . 4 = s . 4 by COMPOS_1:2;
X5: (ProgramPart s) . 5 = s . 5 by COMPOS_1:2;
X6: (ProgramPart s) . 6 = s . 6 by COMPOS_1:2;
X7: (ProgramPart s) . 7 = s . 7 by COMPOS_1:2;
X8: (ProgramPart s) . 8 = s . 8 by COMPOS_1:2;
X9: (ProgramPart s) . 9 = s . 9 by COMPOS_1:2;
X10: (ProgramPart s) . 10 = s . 10 by COMPOS_1:2;
A3: Comput (ProgramPart s),s,0 = s by AMI_1:13;
then A4: IC (Comput (ProgramPart s),s,0 ) = 0 by COMPOS_1:def 16;
then A5: Comput (ProgramPart s),s,(0 + 1) = Exec (s . 0 ),(Comput (ProgramPart s),s,0 ) by X0, AMI_1:55
.= Exec ((intloc 2) := (intloc 0 )),(Comput (ProgramPart s),s,0 ) by A1, Lm1 ;
then A6: (Comput (ProgramPart s),s,1) . (IC SCM+FSA ) = succ (IC (Comput (ProgramPart s),s,0 )) by SCMFSA_2:89
.= 1 by A4 ;
then IC (Comput (ProgramPart s),s,1) = 1 ;
then A7: Comput (ProgramPart s),s,(1 + 1) = Exec (s . 1),(Comput (ProgramPart s),s,1) by X1, AMI_1:55
.= Exec (goto 2),(Comput (ProgramPart s),s,1) by A1, Lm1 ;
then A8: (Comput (ProgramPart s),s,2) . (IC SCM+FSA ) = 2 by SCMFSA_2:95;
IC (Comput (ProgramPart s),s,2) = 2 by A7, SCMFSA_2:95;
then A9: Comput (ProgramPart s),s,(2 + 1) = Exec (s . 2),(Comput (ProgramPart s),s,2) by X2, AMI_1:55
.= Exec ((intloc 3) := (intloc 0 )),(Comput (ProgramPart s),s,2) by A1, Lm1 ;
then A10: (Comput (ProgramPart s),s,3) . (IC SCM+FSA ) = succ (IC (Comput (ProgramPart s),s,2)) by SCMFSA_2:89
.= 3 by A8 ;
then IC (Comput (ProgramPart s),s,3) = 3 ;
then A11: Comput (ProgramPart s),s,(3 + 1) = Exec (s . 3),(Comput (ProgramPart s),s,3) by X3, AMI_1:55
.= Exec (goto 4),(Comput (ProgramPart s),s,3) by A1, Lm1 ;
then A12: (Comput (ProgramPart s),s,4) . (IC SCM+FSA ) = 4 by SCMFSA_2:95;
A13: intloc 2 <> intloc 0 by AMI_3:52;
then A14: (Comput (ProgramPart s),s,1) . (intloc 0 ) = s . (intloc 0 ) by A3, A5, SCMFSA_2:89;
then A15: (Comput (ProgramPart s),s,2) . (intloc 0 ) = s . (intloc 0 ) by A7, SCMFSA_2:95;
then (Comput (ProgramPart s),s,3) . (intloc 3) = s . (intloc 0 ) by A9, SCMFSA_2:89;
then A16: (Comput (ProgramPart s),s,4) . (intloc 3) = s . (intloc 0 ) by A11, SCMFSA_2:95;
IC (Comput (ProgramPart s),s,4) = 4 by A11, SCMFSA_2:95;
then A17: Comput (ProgramPart s),s,(4 + 1) = Exec (s . 4),(Comput (ProgramPart s),s,4) by X4, AMI_1:55
.= Exec ((intloc 4) := (intloc 0 )),(Comput (ProgramPart s),s,4) by A1, Lm1 ;
then A18: (Comput (ProgramPart s),s,5) . (IC SCM+FSA ) = succ (IC (Comput (ProgramPart s),s,4)) by SCMFSA_2:89
.= 5 by A12 ;
then IC (Comput (ProgramPart s),s,5) = 5 ;
then A19: Comput (ProgramPart s),s,(5 + 1) = Exec (s . 5),(Comput (ProgramPart s),s,5) by X5, AMI_1:55
.= Exec (goto 6),(Comput (ProgramPart s),s,5) by A1, Lm1 ;
then A20: (Comput (ProgramPart s),s,6) . (IC SCM+FSA ) = 6 by SCMFSA_2:95;
IC (Comput (ProgramPart s),s,6) = 6 by A19, SCMFSA_2:95;
then A21: Comput (ProgramPart s),s,(6 + 1) = Exec (s . 6),(Comput (ProgramPart s),s,6) by X6, AMI_1:55
.= Exec ((intloc 5) := (intloc 0 )),(Comput (ProgramPart s),s,6) by A1, Lm1 ;
then A22: (Comput (ProgramPart s),s,7) . (IC SCM+FSA ) = succ (IC (Comput (ProgramPart s),s,6)) by SCMFSA_2:89
.= 7 by A20 ;
then IC (Comput (ProgramPart s),s,7) = 7 ;
then A23: Comput (ProgramPart s),s,(7 + 1) = Exec (s . 7),(Comput (ProgramPart s),s,7) by X7, AMI_1:55
.= Exec (goto 8),(Comput (ProgramPart s),s,7) by A1, Lm1 ;
then A24: (Comput (ProgramPart s),s,8) . (IC SCM+FSA ) = 8 by SCMFSA_2:95;
IC (Comput (ProgramPart s),s,8) = 8 by A23, SCMFSA_2:95;
then A25: Comput (ProgramPart s),s,(8 + 1) = Exec (s . 8),(Comput (ProgramPart s),s,8) by X8, AMI_1:55
.= Exec ((intloc 6) := (intloc 0 )),(Comput (ProgramPart s),s,8) by A1, Lm1 ;
then A26: (Comput (ProgramPart s),s,9) . (IC SCM+FSA ) = succ (IC (Comput (ProgramPart s),s,8)) by SCMFSA_2:89
.= 9 by A24 ;
then IC (Comput (ProgramPart s),s,9) = 9 ;
then A27: Comput (ProgramPart s),s,(9 + 1) = Exec (s . 9),(Comput (ProgramPart s),s,9) by X9, AMI_1:55
.= Exec (goto 10),(Comput (ProgramPart s),s,9) by A1, Lm1 ;
then A28: (Comput (ProgramPart s),s,10) . (IC SCM+FSA ) = 10 by SCMFSA_2:95;
A29: (Comput (ProgramPart s),s,1) . (fsloc 0 ) = s . (fsloc 0 ) by A3, A5, SCMFSA_2:89;
then A30: (Comput (ProgramPart s),s,2) . (fsloc 0 ) = s . (fsloc 0 ) by A7, SCMFSA_2:95;
then A31: (Comput (ProgramPart s),s,3) . (fsloc 0 ) = s . (fsloc 0 ) by A9, SCMFSA_2:89;
then A32: (Comput (ProgramPart s),s,4) . (fsloc 0 ) = s . (fsloc 0 ) by A11, SCMFSA_2:95;
then A33: (Comput (ProgramPart s),s,5) . (fsloc 0 ) = s . (fsloc 0 ) by A17, SCMFSA_2:89;
then A34: (Comput (ProgramPart s),s,6) . (fsloc 0 ) = s . (fsloc 0 ) by A19, SCMFSA_2:95;
then A35: (Comput (ProgramPart s),s,7) . (fsloc 0 ) = s . (fsloc 0 ) by A21, SCMFSA_2:89;
then A36: (Comput (ProgramPart s),s,8) . (fsloc 0 ) = s . (fsloc 0 ) by A23, SCMFSA_2:95;
then A37: (Comput (ProgramPart s),s,9) . (fsloc 0 ) = s . (fsloc 0 ) by A25, SCMFSA_2:89;
then A38: (Comput (ProgramPart s),s,10) . (fsloc 0 ) = s . (fsloc 0 ) by A27, SCMFSA_2:95;
A39: (Comput (ProgramPart s),s,3) . (intloc 0 ) = s . (intloc 0 ) by A15, A9, SCMFSA_2:89;
then A40: (Comput (ProgramPart s),s,4) . (intloc 0 ) = s . (intloc 0 ) by A11, SCMFSA_2:95;
then (Comput (ProgramPart s),s,5) . (intloc 4) = s . (intloc 0 ) by A17, SCMFSA_2:89;
then A41: (Comput (ProgramPart s),s,6) . (intloc 4) = s . (intloc 0 ) by A19, SCMFSA_2:95;
A42: intloc 4 <> intloc 0 by AMI_3:52;
then A43: (Comput (ProgramPart s),s,5) . (intloc 0 ) = s . (intloc 0 ) by A40, A17, SCMFSA_2:89;
then A44: (Comput (ProgramPart s),s,6) . (intloc 0 ) = s . (intloc 0 ) by A19, SCMFSA_2:95;
then (Comput (ProgramPart s),s,7) . (intloc 5) = s . (intloc 0 ) by A21, SCMFSA_2:89;
then A45: (Comput (ProgramPart s),s,8) . (intloc 5) = s . (intloc 0 ) by A23, SCMFSA_2:95;
intloc 4 <> intloc 5 by AMI_3:52;
then (Comput (ProgramPart s),s,7) . (intloc 4) = s . (intloc 0 ) by A41, A21, SCMFSA_2:89;
then A46: (Comput (ProgramPart s),s,8) . (intloc 4) = s . (intloc 0 ) by A23, SCMFSA_2:95;
intloc 4 <> intloc 6 by AMI_3:52;
then (Comput (ProgramPart s),s,9) . (intloc 4) = s . (intloc 0 ) by A46, A25, SCMFSA_2:89;
then A47: (Comput (ProgramPart s),s,10) . (intloc 4) = s . (intloc 0 ) by A27, SCMFSA_2:95;
intloc 5 <> intloc 6 by AMI_3:52;
then (Comput (ProgramPart s),s,9) . (intloc 5) = s . (intloc 0 ) by A45, A25, SCMFSA_2:89;
then A48: (Comput (ProgramPart s),s,10) . (intloc 5) = s . (intloc 0 ) by A27, SCMFSA_2:95;
A49: intloc 5 <> intloc 0 by AMI_3:52;
then A50: (Comput (ProgramPart s),s,7) . (intloc 0 ) = s . (intloc 0 ) by A44, A21, SCMFSA_2:89;
then A51: (Comput (ProgramPart s),s,8) . (intloc 0 ) = s . (intloc 0 ) by A23, SCMFSA_2:95;
then (Comput (ProgramPart s),s,9) . (intloc 6) = s . (intloc 0 ) by A25, SCMFSA_2:89;
then A52: (Comput (ProgramPart s),s,10) . (intloc 6) = s . (intloc 0 ) by A27, SCMFSA_2:95;
IC (Comput (ProgramPart s),s,10) = 10 by A27, SCMFSA_2:95;
then A53: Comput (ProgramPart s),s,(10 + 1) = Exec (s . 10),(Comput (ProgramPart s),s,10) by X10, AMI_1:55
.= Exec ((intloc 1) :=len (fsloc 0 )),(Comput (ProgramPart s),s,10) by A1, Lm1 ;
then A54: (Comput (ProgramPart s),s,11) . (IC SCM+FSA ) = succ (IC (Comput (ProgramPart s),s,10)) by SCMFSA_2:100
.= 11 by A28 ;
A55: intloc 6 <> intloc 0 by AMI_3:52;
then A56: (Comput (ProgramPart s),s,9) . (intloc 0 ) = s . (intloc 0 ) by A51, A25, SCMFSA_2:89;
then A57: (Comput (ProgramPart s),s,10) . (intloc 0 ) = s . (intloc 0 ) by A27, SCMFSA_2:95;
hereby :: thesis: ( (Comput (ProgramPart s),s,11) . (intloc 1) = len (s . (fsloc 0 )) & (Comput (ProgramPart s),s,11) . (intloc 2) = s . (intloc 0 ) & (Comput (ProgramPart s),s,11) . (intloc 3) = s . (intloc 0 ) & (Comput (ProgramPart s),s,11) . (intloc 4) = s . (intloc 0 ) & (Comput (ProgramPart s),s,11) . (intloc 5) = s . (intloc 0 ) & (Comput (ProgramPart s),s,11) . (intloc 6) = s . (intloc 0 ) )
let k be Element of NAT ; :: thesis: ( k > 0 & k < 12 implies ( (Comput (ProgramPart s),s,b1) . (IC SCM+FSA ) = b1 & (Comput (ProgramPart s),s,b1) . (intloc 0 ) = s . (intloc 0 ) & (Comput (ProgramPart s),s,b1) . (fsloc 0 ) = s . (fsloc 0 ) ) )
assume that
A58: k > 0 and
A59: k < 12 ; :: thesis: ( (Comput (ProgramPart s),s,b1) . (IC SCM+FSA ) = b1 & (Comput (ProgramPart s),s,b1) . (intloc 0 ) = s . (intloc 0 ) & (Comput (ProgramPart s),s,b1) . (fsloc 0 ) = s . (fsloc 0 ) )
set c1 = (Comput (ProgramPart s),s,k) . (IC SCM+FSA );
set d1 = k;
set c2 = (Comput (ProgramPart s),s,k) . (intloc 0 );
set d2 = s . (intloc 0 );
set c3 = (Comput (ProgramPart s),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: ( (Comput (ProgramPart s),s,b1) . (IC SCM+FSA ) = b1 & (Comput (ProgramPart s),s,b1) . (intloc 0 ) = s . (intloc 0 ) & (Comput (ProgramPart s),s,b1) . (fsloc 0 ) = s . (fsloc 0 ) )
hence ( (Comput (ProgramPart s),s,k) . (IC SCM+FSA ) = k & (Comput (ProgramPart s),s,k) . (intloc 0 ) = s . (intloc 0 ) & (Comput (ProgramPart s),s,k) . (fsloc 0 ) = s . (fsloc 0 ) ) by A3, A5, A6, A13, SCMFSA_2:89; :: thesis: verum
end;
suppose k = 2 ; :: thesis: ( (Comput (ProgramPart s),s,b1) . (IC SCM+FSA ) = b1 & (Comput (ProgramPart s),s,b1) . (intloc 0 ) = s . (intloc 0 ) & (Comput (ProgramPart s),s,b1) . (fsloc 0 ) = s . (fsloc 0 ) )
hence ( (Comput (ProgramPart s),s,k) . (IC SCM+FSA ) = k & (Comput (ProgramPart s),s,k) . (intloc 0 ) = s . (intloc 0 ) & (Comput (ProgramPart s),s,k) . (fsloc 0 ) = s . (fsloc 0 ) ) by A14, A29, A7, SCMFSA_2:95; :: thesis: verum
end;
suppose k = 3 ; :: thesis: ( (Comput (ProgramPart s),s,b1) . (IC SCM+FSA ) = b1 & (Comput (ProgramPart s),s,b1) . (intloc 0 ) = s . (intloc 0 ) & (Comput (ProgramPart s),s,b1) . (fsloc 0 ) = s . (fsloc 0 ) )
hence ( (Comput (ProgramPart s),s,k) . (IC SCM+FSA ) = k & (Comput (ProgramPart s),s,k) . (intloc 0 ) = s . (intloc 0 ) & (Comput (ProgramPart s),s,k) . (fsloc 0 ) = s . (fsloc 0 ) ) by A15, A30, A9, A10, SCMFSA_2:89; :: thesis: verum
end;
suppose k = 4 ; :: thesis: ( (Comput (ProgramPart s),s,b1) . (IC SCM+FSA ) = b1 & (Comput (ProgramPart s),s,b1) . (intloc 0 ) = s . (intloc 0 ) & (Comput (ProgramPart s),s,b1) . (fsloc 0 ) = s . (fsloc 0 ) )
hence ( (Comput (ProgramPart s),s,k) . (IC SCM+FSA ) = k & (Comput (ProgramPart s),s,k) . (intloc 0 ) = s . (intloc 0 ) & (Comput (ProgramPart s),s,k) . (fsloc 0 ) = s . (fsloc 0 ) ) by A39, A31, A11, SCMFSA_2:95; :: thesis: verum
end;
suppose k = 5 ; :: thesis: ( (Comput (ProgramPart s),s,b1) . (IC SCM+FSA ) = b1 & (Comput (ProgramPart s),s,b1) . (intloc 0 ) = s . (intloc 0 ) & (Comput (ProgramPart s),s,b1) . (fsloc 0 ) = s . (fsloc 0 ) )
hence ( (Comput (ProgramPart s),s,k) . (IC SCM+FSA ) = k & (Comput (ProgramPart s),s,k) . (intloc 0 ) = s . (intloc 0 ) & (Comput (ProgramPart s),s,k) . (fsloc 0 ) = s . (fsloc 0 ) ) by A40, A32, A17, A18, A42, SCMFSA_2:89; :: thesis: verum
end;
suppose k = 6 ; :: thesis: ( (Comput (ProgramPart s),s,b1) . (IC SCM+FSA ) = b1 & (Comput (ProgramPart s),s,b1) . (intloc 0 ) = s . (intloc 0 ) & (Comput (ProgramPart s),s,b1) . (fsloc 0 ) = s . (fsloc 0 ) )
hence ( (Comput (ProgramPart s),s,k) . (IC SCM+FSA ) = k & (Comput (ProgramPart s),s,k) . (intloc 0 ) = s . (intloc 0 ) & (Comput (ProgramPart s),s,k) . (fsloc 0 ) = s . (fsloc 0 ) ) by A43, A33, A19, SCMFSA_2:95; :: thesis: verum
end;
suppose k = 7 ; :: thesis: ( (Comput (ProgramPart s),s,b1) . (IC SCM+FSA ) = b1 & (Comput (ProgramPart s),s,b1) . (intloc 0 ) = s . (intloc 0 ) & (Comput (ProgramPart s),s,b1) . (fsloc 0 ) = s . (fsloc 0 ) )
hence ( (Comput (ProgramPart s),s,k) . (IC SCM+FSA ) = k & (Comput (ProgramPart s),s,k) . (intloc 0 ) = s . (intloc 0 ) & (Comput (ProgramPart s),s,k) . (fsloc 0 ) = s . (fsloc 0 ) ) by A44, A34, A21, A22, A49, SCMFSA_2:89; :: thesis: verum
end;
suppose k = 8 ; :: thesis: ( (Comput (ProgramPart s),s,b1) . (IC SCM+FSA ) = b1 & (Comput (ProgramPart s),s,b1) . (intloc 0 ) = s . (intloc 0 ) & (Comput (ProgramPart s),s,b1) . (fsloc 0 ) = s . (fsloc 0 ) )
hence ( (Comput (ProgramPart s),s,k) . (IC SCM+FSA ) = k & (Comput (ProgramPart s),s,k) . (intloc 0 ) = s . (intloc 0 ) & (Comput (ProgramPart s),s,k) . (fsloc 0 ) = s . (fsloc 0 ) ) by A50, A35, A23, SCMFSA_2:95; :: thesis: verum
end;
suppose k = 9 ; :: thesis: ( (Comput (ProgramPart s),s,b1) . (IC SCM+FSA ) = b1 & (Comput (ProgramPart s),s,b1) . (intloc 0 ) = s . (intloc 0 ) & (Comput (ProgramPart s),s,b1) . (fsloc 0 ) = s . (fsloc 0 ) )
hence ( (Comput (ProgramPart s),s,k) . (IC SCM+FSA ) = k & (Comput (ProgramPart s),s,k) . (intloc 0 ) = s . (intloc 0 ) & (Comput (ProgramPart s),s,k) . (fsloc 0 ) = s . (fsloc 0 ) ) by A51, A36, A25, A26, A55, SCMFSA_2:89; :: thesis: verum
end;
suppose k = 10 ; :: thesis: ( (Comput (ProgramPart s),s,b1) . (IC SCM+FSA ) = b1 & (Comput (ProgramPart s),s,b1) . (intloc 0 ) = s . (intloc 0 ) & (Comput (ProgramPart s),s,b1) . (fsloc 0 ) = s . (fsloc 0 ) )
hence ( (Comput (ProgramPart s),s,k) . (IC SCM+FSA ) = k & (Comput (ProgramPart s),s,k) . (intloc 0 ) = s . (intloc 0 ) & (Comput (ProgramPart s),s,k) . (fsloc 0 ) = s . (fsloc 0 ) ) by A56, A37, A27, SCMFSA_2:95; :: thesis: verum
end;
suppose k = 11 ; :: thesis: ( (Comput (ProgramPart s),s,b1) . (IC SCM+FSA ) = b1 & (Comput (ProgramPart s),s,b1) . (intloc 0 ) = s . (intloc 0 ) & (Comput (ProgramPart s),s,b1) . (fsloc 0 ) = s . (fsloc 0 ) )
hence ( (Comput (ProgramPart s),s,k) . (IC SCM+FSA ) = k & (Comput (ProgramPart s),s,k) . (intloc 0 ) = s . (intloc 0 ) & (Comput (ProgramPart s),s,k) . (fsloc 0 ) = s . (fsloc 0 ) ) by A57, A38, A53, A54, SCMFSA_2:100; :: thesis: verum
end;
end;
end;
thus (Comput (ProgramPart s),s,11) . (intloc 1) = len (s . (fsloc 0 )) by A38, A53, SCMFSA_2:100; :: thesis: ( (Comput (ProgramPart s),s,11) . (intloc 2) = s . (intloc 0 ) & (Comput (ProgramPart s),s,11) . (intloc 3) = s . (intloc 0 ) & (Comput (ProgramPart s),s,11) . (intloc 4) = s . (intloc 0 ) & (Comput (ProgramPart s),s,11) . (intloc 5) = s . (intloc 0 ) & (Comput (ProgramPart s),s,11) . (intloc 6) = s . (intloc 0 ) )
(Comput (ProgramPart s),s,1) . (intloc 2) = s . (intloc 0 ) by A3, A5, SCMFSA_2:89;
then A61: (Comput (ProgramPart s),s,2) . (intloc 2) = s . (intloc 0 ) by A7, SCMFSA_2:95;
intloc 2 <> intloc 3 by AMI_3:52;
then (Comput (ProgramPart s),s,3) . (intloc 2) = s . (intloc 0 ) by A61, A9, SCMFSA_2:89;
then A62: (Comput (ProgramPart s),s,4) . (intloc 2) = s . (intloc 0 ) by A11, SCMFSA_2:95;
intloc 2 <> intloc 4 by AMI_3:52;
then (Comput (ProgramPart s),s,5) . (intloc 2) = s . (intloc 0 ) by A62, A17, SCMFSA_2:89;
then A63: (Comput (ProgramPart s),s,6) . (intloc 2) = s . (intloc 0 ) by A19, SCMFSA_2:95;
intloc 2 <> intloc 5 by AMI_3:52;
then (Comput (ProgramPart s),s,7) . (intloc 2) = s . (intloc 0 ) by A63, A21, SCMFSA_2:89;
then A64: (Comput (ProgramPart s),s,8) . (intloc 2) = s . (intloc 0 ) by A23, SCMFSA_2:95;
intloc 2 <> intloc 6 by AMI_3:52;
then (Comput (ProgramPart s),s,9) . (intloc 2) = s . (intloc 0 ) by A64, A25, SCMFSA_2:89;
then A65: (Comput (ProgramPart s),s,10) . (intloc 2) = s . (intloc 0 ) by A27, SCMFSA_2:95;
intloc 3 <> intloc 4 by AMI_3:52;
then (Comput (ProgramPart s),s,5) . (intloc 3) = s . (intloc 0 ) by A16, A17, SCMFSA_2:89;
then A66: (Comput (ProgramPart s),s,6) . (intloc 3) = s . (intloc 0 ) by A19, SCMFSA_2:95;
intloc 3 <> intloc 5 by AMI_3:52;
then (Comput (ProgramPart s),s,7) . (intloc 3) = s . (intloc 0 ) by A66, A21, SCMFSA_2:89;
then A67: (Comput (ProgramPart s),s,8) . (intloc 3) = s . (intloc 0 ) by A23, SCMFSA_2:95;
intloc 3 <> intloc 6 by AMI_3:52;
then (Comput (ProgramPart s),s,9) . (intloc 3) = s . (intloc 0 ) by A67, A25, SCMFSA_2:89;
then A68: (Comput (ProgramPart s),s,10) . (intloc 3) = s . (intloc 0 ) by A27, SCMFSA_2:95;
intloc 2 <> intloc 1 by AMI_3:52;
hence (Comput (ProgramPart s),s,11) . (intloc 2) = s . (intloc 0 ) by A65, A53, SCMFSA_2:100; :: thesis: ( (Comput (ProgramPart s),s,11) . (intloc 3) = s . (intloc 0 ) & (Comput (ProgramPart s),s,11) . (intloc 4) = s . (intloc 0 ) & (Comput (ProgramPart s),s,11) . (intloc 5) = s . (intloc 0 ) & (Comput (ProgramPart s),s,11) . (intloc 6) = s . (intloc 0 ) )
intloc 3 <> intloc 1 by AMI_3:52;
hence (Comput (ProgramPart s),s,11) . (intloc 3) = s . (intloc 0 ) by A68, A53, SCMFSA_2:100; :: thesis: ( (Comput (ProgramPart s),s,11) . (intloc 4) = s . (intloc 0 ) & (Comput (ProgramPart s),s,11) . (intloc 5) = s . (intloc 0 ) & (Comput (ProgramPart s),s,11) . (intloc 6) = s . (intloc 0 ) )
intloc 4 <> intloc 1 by AMI_3:52;
hence (Comput (ProgramPart s),s,11) . (intloc 4) = s . (intloc 0 ) by A47, A53, SCMFSA_2:100; :: thesis: ( (Comput (ProgramPart s),s,11) . (intloc 5) = s . (intloc 0 ) & (Comput (ProgramPart s),s,11) . (intloc 6) = s . (intloc 0 ) )
intloc 5 <> intloc 1 by AMI_3:52;
hence (Comput (ProgramPart s),s,11) . (intloc 5) = s . (intloc 0 ) by A48, A53, SCMFSA_2:100; :: thesis: (Comput (ProgramPart s),s,11) . (intloc 6) = s . (intloc 0 )
intloc 6 <> intloc 1 by AMI_3:52;
hence (Comput (ProgramPart s),s,11) . (intloc 6) = s . (intloc 0 ) by A52, A53, SCMFSA_2:100; :: thesis: verum