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 Element of NAT st k > 0 & k < 12 holds
( (Comput (P,s,k)) . (IC ) = k & (Comput (P,s,k)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,k)) . (fsloc 0) = s . (fsloc 0) ) ) & (Comput (P,s,11)) . (intloc 1) = len (s . (fsloc 0)) & (Comput (P,s,11)) . (intloc 2) = s . (intloc 0) & (Comput (P,s,11)) . (intloc 3) = s . (intloc 0) & (Comput (P,s,11)) . (intloc 4) = s . (intloc 0) & (Comput (P,s,11)) . (intloc 5) = s . (intloc 0) & (Comput (P,s,11)) . (intloc 6) = s . (intloc 0) )
let P be Instruction-Sequence of SCM+FSA; :: thesis: ( Insert-Sort-Algorithm c= P implies ( ( for k being Element of NAT st k > 0 & k < 12 holds
( (Comput (P,s,k)) . (IC ) = k & (Comput (P,s,k)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,k)) . (fsloc 0) = s . (fsloc 0) ) ) & (Comput (P,s,11)) . (intloc 1) = len (s . (fsloc 0)) & (Comput (P,s,11)) . (intloc 2) = s . (intloc 0) & (Comput (P,s,11)) . (intloc 3) = s . (intloc 0) & (Comput (P,s,11)) . (intloc 4) = s . (intloc 0) & (Comput (P,s,11)) . (intloc 5) = s . (intloc 0) & (Comput (P,s,11)) . (intloc 6) = s . (intloc 0) ) )
assume A1: Insert-Sort-Algorithm c= P ; :: thesis: ( ( for k being Element of NAT st k > 0 & k < 12 holds
( (Comput (P,s,k)) . (IC ) = k & (Comput (P,s,k)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,k)) . (fsloc 0) = s . (fsloc 0) ) ) & (Comput (P,s,11)) . (intloc 1) = len (s . (fsloc 0)) & (Comput (P,s,11)) . (intloc 2) = s . (intloc 0) & (Comput (P,s,11)) . (intloc 3) = s . (intloc 0) & (Comput (P,s,11)) . (intloc 4) = s . (intloc 0) & (Comput (P,s,11)) . (intloc 5) = s . (intloc 0) & (Comput (P,s,11)) . (intloc 6) = s . (intloc 0) )
A2: Comput (P,s,0) = s by EXTPRO_1:2;
then A3: IC (Comput (P,s,0)) = 0 by MEMSTR_0:def 8;
then A4: Comput (P,s,(0 + 1)) = Exec ((P . 0),(Comput (P,s,0))) by EXTPRO_1:6
.= Exec (((intloc 2) := (intloc 0)),(Comput (P,s,0))) by A1, Lm1 ;
then A5: (Comput (P,s,1)) . (IC ) = succ (IC (Comput (P,s,0))) by SCMFSA_2:63
.= 1 by A3 ;
then IC (Comput (P,s,1)) = 1 ;
then A6: Comput (P,s,(1 + 1)) = Exec ((P . 1),(Comput (P,s,1))) by EXTPRO_1:6
.= Exec ((goto 2),(Comput (P,s,1))) by A1, Lm1 ;
then A7: (Comput (P,s,2)) . (IC ) = 2 by SCMFSA_2:69;
IC (Comput (P,s,2)) = 2 by A6, SCMFSA_2:69;
then A8: Comput (P,s,(2 + 1)) = Exec ((P . 2),(Comput (P,s,2))) by EXTPRO_1:6
.= Exec (((intloc 3) := (intloc 0)),(Comput (P,s,2))) by A1, Lm1 ;
then A9: (Comput (P,s,3)) . (IC ) = succ (IC (Comput (P,s,2))) by SCMFSA_2:63
.= 3 by A7 ;
then IC (Comput (P,s,3)) = 3 ;
then A10: Comput (P,s,(3 + 1)) = Exec ((P . 3),(Comput (P,s,3))) by EXTPRO_1:6
.= Exec ((goto 4),(Comput (P,s,3))) by A1, Lm1 ;
then A11: (Comput (P,s,4)) . (IC ) = 4 by SCMFSA_2:69;
A12: intloc 2 <> intloc 0 by SCMFSA_2:101;
then A13: (Comput (P,s,1)) . (intloc 0) = s . (intloc 0) by A2, A4, SCMFSA_2:63;
then A14: (Comput (P,s,2)) . (intloc 0) = s . (intloc 0) by A6, SCMFSA_2:69;
then (Comput (P,s,3)) . (intloc 3) = s . (intloc 0) by A8, SCMFSA_2:63;
then A15: (Comput (P,s,4)) . (intloc 3) = s . (intloc 0) by A10, SCMFSA_2:69;
IC (Comput (P,s,4)) = 4 by A10, SCMFSA_2:69;
then A16: Comput (P,s,(4 + 1)) = Exec ((P . 4),(Comput (P,s,4))) by EXTPRO_1:6
.= Exec (((intloc 4) := (intloc 0)),(Comput (P,s,4))) by A1, Lm1 ;
then A17: (Comput (P,s,5)) . (IC ) = succ (IC (Comput (P,s,4))) by SCMFSA_2:63
.= 5 by A11 ;
then IC (Comput (P,s,5)) = 5 ;
then A18: Comput (P,s,(5 + 1)) = Exec ((P . 5),(Comput (P,s,5))) by EXTPRO_1:6
.= Exec ((goto 6),(Comput (P,s,5))) by A1, Lm1 ;
then A19: (Comput (P,s,6)) . (IC ) = 6 by SCMFSA_2:69;
IC (Comput (P,s,6)) = 6 by A18, SCMFSA_2:69;
then A20: Comput (P,s,(6 + 1)) = Exec ((P . 6),(Comput (P,s,6))) by EXTPRO_1:6
.= Exec (((intloc 5) := (intloc 0)),(Comput (P,s,6))) by A1, Lm1 ;
then A21: (Comput (P,s,7)) . (IC ) = succ (IC (Comput (P,s,6))) by SCMFSA_2:63
.= 7 by A19 ;
then IC (Comput (P,s,7)) = 7 ;
then A22: Comput (P,s,(7 + 1)) = Exec ((P . 7),(Comput (P,s,7))) by EXTPRO_1:6
.= Exec ((goto 8),(Comput (P,s,7))) by A1, Lm1 ;
then A23: (Comput (P,s,8)) . (IC ) = 8 by SCMFSA_2:69;
IC (Comput (P,s,8)) = 8 by A22, SCMFSA_2:69;
then A24: Comput (P,s,(8 + 1)) = Exec ((P . 8),(Comput (P,s,8))) by EXTPRO_1:6
.= Exec (((intloc 6) := (intloc 0)),(Comput (P,s,8))) by A1, Lm1 ;
then A25: (Comput (P,s,9)) . (IC ) = succ (IC (Comput (P,s,8))) by SCMFSA_2:63
.= 9 by A23 ;
then IC (Comput (P,s,9)) = 9 ;
then A26: Comput (P,s,(9 + 1)) = Exec ((P . 9),(Comput (P,s,9))) by EXTPRO_1:6
.= Exec ((goto 10),(Comput (P,s,9))) by A1, Lm1 ;
then A27: (Comput (P,s,10)) . (IC ) = 10 by SCMFSA_2:69;
A28: (Comput (P,s,1)) . (fsloc 0) = s . (fsloc 0) by A2, A4, SCMFSA_2:63;
then A29: (Comput (P,s,2)) . (fsloc 0) = s . (fsloc 0) by A6, SCMFSA_2:69;
then A30: (Comput (P,s,3)) . (fsloc 0) = s . (fsloc 0) by A8, SCMFSA_2:63;
then A31: (Comput (P,s,4)) . (fsloc 0) = s . (fsloc 0) by A10, SCMFSA_2:69;
then A32: (Comput (P,s,5)) . (fsloc 0) = s . (fsloc 0) by A16, SCMFSA_2:63;
then A33: (Comput (P,s,6)) . (fsloc 0) = s . (fsloc 0) by A18, SCMFSA_2:69;
then A34: (Comput (P,s,7)) . (fsloc 0) = s . (fsloc 0) by A20, SCMFSA_2:63;
then A35: (Comput (P,s,8)) . (fsloc 0) = s . (fsloc 0) by A22, SCMFSA_2:69;
then A36: (Comput (P,s,9)) . (fsloc 0) = s . (fsloc 0) by A24, SCMFSA_2:63;
then A37: (Comput (P,s,10)) . (fsloc 0) = s . (fsloc 0) by A26, SCMFSA_2:69;
A38: (Comput (P,s,3)) . (intloc 0) = s . (intloc 0) by A14, A8, SCMFSA_2:63;
then A39: (Comput (P,s,4)) . (intloc 0) = s . (intloc 0) by A10, SCMFSA_2:69;
then (Comput (P,s,5)) . (intloc 4) = s . (intloc 0) by A16, SCMFSA_2:63;
then A40: (Comput (P,s,6)) . (intloc 4) = s . (intloc 0) by A18, SCMFSA_2:69;
A41: intloc 4 <> intloc 0 by SCMFSA_2:101;
then A42: (Comput (P,s,5)) . (intloc 0) = s . (intloc 0) by A39, A16, SCMFSA_2:63;
then A43: (Comput (P,s,6)) . (intloc 0) = s . (intloc 0) by A18, SCMFSA_2:69;
then (Comput (P,s,7)) . (intloc 5) = s . (intloc 0) by A20, SCMFSA_2:63;
then A44: (Comput (P,s,8)) . (intloc 5) = s . (intloc 0) by A22, SCMFSA_2:69;
intloc 4 <> intloc 5 by SCMFSA_2:101;
then (Comput (P,s,7)) . (intloc 4) = s . (intloc 0) by A40, A20, SCMFSA_2:63;
then A45: (Comput (P,s,8)) . (intloc 4) = s . (intloc 0) by A22, SCMFSA_2:69;
intloc 4 <> intloc 6 by SCMFSA_2:101;
then (Comput (P,s,9)) . (intloc 4) = s . (intloc 0) by A45, A24, SCMFSA_2:63;
then A46: (Comput (P,s,10)) . (intloc 4) = s . (intloc 0) by A26, SCMFSA_2:69;
intloc 5 <> intloc 6 by SCMFSA_2:101;
then (Comput (P,s,9)) . (intloc 5) = s . (intloc 0) by A44, A24, SCMFSA_2:63;
then A47: (Comput (P,s,10)) . (intloc 5) = s . (intloc 0) by A26, SCMFSA_2:69;
A48: intloc 5 <> intloc 0 by SCMFSA_2:101;
then A49: (Comput (P,s,7)) . (intloc 0) = s . (intloc 0) by A43, A20, SCMFSA_2:63;
then A50: (Comput (P,s,8)) . (intloc 0) = s . (intloc 0) by A22, SCMFSA_2:69;
then (Comput (P,s,9)) . (intloc 6) = s . (intloc 0) by A24, SCMFSA_2:63;
then A51: (Comput (P,s,10)) . (intloc 6) = s . (intloc 0) by A26, SCMFSA_2:69;
IC (Comput (P,s,10)) = 10 by A26, SCMFSA_2:69;
then A52: Comput (P,s,(10 + 1)) = Exec ((P . 10),(Comput (P,s,10))) by EXTPRO_1:6
.= Exec (((intloc 1) :=len (fsloc 0)),(Comput (P,s,10))) by A1, Lm1 ;
then A53: (Comput (P,s,11)) . (IC ) = succ (IC (Comput (P,s,10))) by SCMFSA_2:74
.= 11 by A27 ;
A54: intloc 6 <> intloc 0 by SCMFSA_2:101;
then A55: (Comput (P,s,9)) . (intloc 0) = s . (intloc 0) by A50, A24, SCMFSA_2:63;
then A56: (Comput (P,s,10)) . (intloc 0) = s . (intloc 0) by A26, SCMFSA_2:69;
hereby :: thesis: ( (Comput (P,s,11)) . (intloc 1) = len (s . (fsloc 0)) & (Comput (P,s,11)) . (intloc 2) = s . (intloc 0) & (Comput (P,s,11)) . (intloc 3) = s . (intloc 0) & (Comput (P,s,11)) . (intloc 4) = s . (intloc 0) & (Comput (P,s,11)) . (intloc 5) = s . (intloc 0) & (Comput (P,s,11)) . (intloc 6) = s . (intloc 0) )
let k be Element of NAT ; :: thesis: ( k > 0 & k < 12 implies ( (Comput (P,s,b1)) . (IC ) = b1 & (Comput (P,s,b1)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,b1)) . (fsloc 0) = s . (fsloc 0) ) )
assume that
A57: k > 0 and
A58: k < 12 ; :: thesis: ( (Comput (P,s,b1)) . (IC ) = b1 & (Comput (P,s,b1)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,b1)) . (fsloc 0) = s . (fsloc 0) )
set c1 = (Comput (P,s,k)) . (IC );
set d1 = k;
set c2 = (Comput (P,s,k)) . (intloc 0);
set d2 = s . (intloc 0);
set c3 = (Comput (P,s,k)) . (fsloc 0);
set d3 = s . (fsloc 0);
k < 11 + 1 by A58;
then A59: 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 A57, A59, NAT_1:35;
suppose k = 1 ; :: thesis: ( (Comput (P,s,b1)) . (IC ) = b1 & (Comput (P,s,b1)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,b1)) . (fsloc 0) = s . (fsloc 0) )
hence ( (Comput (P,s,k)) . (IC ) = k & (Comput (P,s,k)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,k)) . (fsloc 0) = s . (fsloc 0) ) by A2, A4, A5, A12, SCMFSA_2:63; :: thesis: verum
end;
suppose k = 2 ; :: thesis: ( (Comput (P,s,b1)) . (IC ) = b1 & (Comput (P,s,b1)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,b1)) . (fsloc 0) = s . (fsloc 0) )
hence ( (Comput (P,s,k)) . (IC ) = k & (Comput (P,s,k)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,k)) . (fsloc 0) = s . (fsloc 0) ) by A13, A28, A6, SCMFSA_2:69; :: thesis: verum
end;
suppose k = 3 ; :: thesis: ( (Comput (P,s,b1)) . (IC ) = b1 & (Comput (P,s,b1)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,b1)) . (fsloc 0) = s . (fsloc 0) )
hence ( (Comput (P,s,k)) . (IC ) = k & (Comput (P,s,k)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,k)) . (fsloc 0) = s . (fsloc 0) ) by A14, A29, A8, A9, SCMFSA_2:63; :: thesis: verum
end;
suppose k = 4 ; :: thesis: ( (Comput (P,s,b1)) . (IC ) = b1 & (Comput (P,s,b1)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,b1)) . (fsloc 0) = s . (fsloc 0) )
hence ( (Comput (P,s,k)) . (IC ) = k & (Comput (P,s,k)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,k)) . (fsloc 0) = s . (fsloc 0) ) by A38, A30, A10, SCMFSA_2:69; :: thesis: verum
end;
suppose k = 5 ; :: thesis: ( (Comput (P,s,b1)) . (IC ) = b1 & (Comput (P,s,b1)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,b1)) . (fsloc 0) = s . (fsloc 0) )
hence ( (Comput (P,s,k)) . (IC ) = k & (Comput (P,s,k)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,k)) . (fsloc 0) = s . (fsloc 0) ) by A39, A31, A16, A17, A41, SCMFSA_2:63; :: thesis: verum
end;
suppose k = 6 ; :: thesis: ( (Comput (P,s,b1)) . (IC ) = b1 & (Comput (P,s,b1)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,b1)) . (fsloc 0) = s . (fsloc 0) )
hence ( (Comput (P,s,k)) . (IC ) = k & (Comput (P,s,k)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,k)) . (fsloc 0) = s . (fsloc 0) ) by A42, A32, A18, SCMFSA_2:69; :: thesis: verum
end;
suppose k = 7 ; :: thesis: ( (Comput (P,s,b1)) . (IC ) = b1 & (Comput (P,s,b1)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,b1)) . (fsloc 0) = s . (fsloc 0) )
hence ( (Comput (P,s,k)) . (IC ) = k & (Comput (P,s,k)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,k)) . (fsloc 0) = s . (fsloc 0) ) by A43, A33, A20, A21, A48, SCMFSA_2:63; :: thesis: verum
end;
suppose k = 8 ; :: thesis: ( (Comput (P,s,b1)) . (IC ) = b1 & (Comput (P,s,b1)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,b1)) . (fsloc 0) = s . (fsloc 0) )
hence ( (Comput (P,s,k)) . (IC ) = k & (Comput (P,s,k)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,k)) . (fsloc 0) = s . (fsloc 0) ) by A49, A34, A22, SCMFSA_2:69; :: thesis: verum
end;
suppose k = 9 ; :: thesis: ( (Comput (P,s,b1)) . (IC ) = b1 & (Comput (P,s,b1)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,b1)) . (fsloc 0) = s . (fsloc 0) )
hence ( (Comput (P,s,k)) . (IC ) = k & (Comput (P,s,k)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,k)) . (fsloc 0) = s . (fsloc 0) ) by A50, A35, A24, A25, A54, SCMFSA_2:63; :: thesis: verum
end;
suppose k = 10 ; :: thesis: ( (Comput (P,s,b1)) . (IC ) = b1 & (Comput (P,s,b1)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,b1)) . (fsloc 0) = s . (fsloc 0) )
hence ( (Comput (P,s,k)) . (IC ) = k & (Comput (P,s,k)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,k)) . (fsloc 0) = s . (fsloc 0) ) by A55, A36, A26, SCMFSA_2:69; :: thesis: verum
end;
suppose A60: k = 11 ; :: thesis: ( (Comput (P,s,b1)) . (IC ) = b1 & (Comput (P,s,b1)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,b1)) . (fsloc 0) = s . (fsloc 0) )
hence (Comput (P,s,k)) . (IC ) = k by A53; :: thesis: ( (Comput (P,s,k)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,k)) . (fsloc 0) = s . (fsloc 0) )
intloc 0 <> intloc 1 by SCMFSA_2:101;
hence (Comput (P,s,k)) . (intloc 0) = s . (intloc 0) by A56, A52, A60, SCMFSA_2:74; :: thesis: (Comput (P,s,k)) . (fsloc 0) = s . (fsloc 0)
thus (Comput (P,s,k)) . (fsloc 0) = s . (fsloc 0) by A37, A52, A60, SCMFSA_2:74; :: thesis: verum
end;
end;
end;
thus (Comput (P,s,11)) . (intloc 1) = len (s . (fsloc 0)) by A37, A52, SCMFSA_2:74; :: thesis: ( (Comput (P,s,11)) . (intloc 2) = s . (intloc 0) & (Comput (P,s,11)) . (intloc 3) = s . (intloc 0) & (Comput (P,s,11)) . (intloc 4) = s . (intloc 0) & (Comput (P,s,11)) . (intloc 5) = s . (intloc 0) & (Comput (P,s,11)) . (intloc 6) = s . (intloc 0) )
(Comput (P,s,1)) . (intloc 2) = s . (intloc 0) by A2, A4, SCMFSA_2:63;
then A61: (Comput (P,s,2)) . (intloc 2) = s . (intloc 0) by A6, SCMFSA_2:69;
intloc 2 <> intloc 3 by SCMFSA_2:101;
then (Comput (P,s,3)) . (intloc 2) = s . (intloc 0) by A61, A8, SCMFSA_2:63;
then A62: (Comput (P,s,4)) . (intloc 2) = s . (intloc 0) by A10, SCMFSA_2:69;
intloc 2 <> intloc 4 by SCMFSA_2:101;
then (Comput (P,s,5)) . (intloc 2) = s . (intloc 0) by A62, A16, SCMFSA_2:63;
then A63: (Comput (P,s,6)) . (intloc 2) = s . (intloc 0) by A18, SCMFSA_2:69;
intloc 2 <> intloc 5 by SCMFSA_2:101;
then (Comput (P,s,7)) . (intloc 2) = s . (intloc 0) by A63, A20, SCMFSA_2:63;
then A64: (Comput (P,s,8)) . (intloc 2) = s . (intloc 0) by A22, SCMFSA_2:69;
intloc 2 <> intloc 6 by SCMFSA_2:101;
then (Comput (P,s,9)) . (intloc 2) = s . (intloc 0) by A64, A24, SCMFSA_2:63;
then A65: (Comput (P,s,10)) . (intloc 2) = s . (intloc 0) by A26, SCMFSA_2:69;
intloc 3 <> intloc 4 by SCMFSA_2:101;
then (Comput (P,s,5)) . (intloc 3) = s . (intloc 0) by A15, A16, SCMFSA_2:63;
then A66: (Comput (P,s,6)) . (intloc 3) = s . (intloc 0) by A18, SCMFSA_2:69;
intloc 3 <> intloc 5 by SCMFSA_2:101;
then (Comput (P,s,7)) . (intloc 3) = s . (intloc 0) by A66, A20, SCMFSA_2:63;
then A67: (Comput (P,s,8)) . (intloc 3) = s . (intloc 0) by A22, SCMFSA_2:69;
intloc 3 <> intloc 6 by SCMFSA_2:101;
then (Comput (P,s,9)) . (intloc 3) = s . (intloc 0) by A67, A24, SCMFSA_2:63;
then A68: (Comput (P,s,10)) . (intloc 3) = s . (intloc 0) by A26, SCMFSA_2:69;
intloc 2 <> intloc 1 by SCMFSA_2:101;
hence (Comput (P,s,11)) . (intloc 2) = s . (intloc 0) by A65, A52, SCMFSA_2:74; :: thesis: ( (Comput (P,s,11)) . (intloc 3) = s . (intloc 0) & (Comput (P,s,11)) . (intloc 4) = s . (intloc 0) & (Comput (P,s,11)) . (intloc 5) = s . (intloc 0) & (Comput (P,s,11)) . (intloc 6) = s . (intloc 0) )
intloc 3 <> intloc 1 by SCMFSA_2:101;
hence (Comput (P,s,11)) . (intloc 3) = s . (intloc 0) by A68, A52, SCMFSA_2:74; :: thesis: ( (Comput (P,s,11)) . (intloc 4) = s . (intloc 0) & (Comput (P,s,11)) . (intloc 5) = s . (intloc 0) & (Comput (P,s,11)) . (intloc 6) = s . (intloc 0) )
intloc 4 <> intloc 1 by SCMFSA_2:101;
hence (Comput (P,s,11)) . (intloc 4) = s . (intloc 0) by A46, A52, SCMFSA_2:74; :: thesis: ( (Comput (P,s,11)) . (intloc 5) = s . (intloc 0) & (Comput (P,s,11)) . (intloc 6) = s . (intloc 0) )
intloc 5 <> intloc 1 by SCMFSA_2:101;
hence (Comput (P,s,11)) . (intloc 5) = s . (intloc 0) by A47, A52, SCMFSA_2:74; :: thesis: (Comput (P,s,11)) . (intloc 6) = s . (intloc 0)
intloc 6 <> intloc 1 by SCMFSA_2:101;
hence (Comput (P,s,11)) . (intloc 6) = s . (intloc 0) by A51, A52, SCMFSA_2:74; :: thesis: verum