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)) . (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 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 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: 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 (((intloc 2) := (intloc 0)),(Comput (P,s,0))) by A1, Lm1 ;
then A4: (Comput (P,s,1)) . (IC ) = (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 A1, Lm1 ;
then A6: (Comput (P,s,2)) . (IC ) = 2 by SCMFSA_2:69;
IC (Comput (P,s,2)) = 2 by A5, SCMFSA_2:69;
then A7: 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 A8: (Comput (P,s,3)) . (IC ) = (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 A1, Lm1 ;
then A10: (Comput (P,s,4)) . (IC ) = 4 by SCMFSA_2:69;
A11: intloc 2 <> intloc 0 by SCMFSA_2:101;
then A12: (Comput (P,s,1)) . (intloc 0) = s . (intloc 0) by A3, SCMFSA_2:63;
then A13: (Comput (P,s,2)) . (intloc 0) = s . (intloc 0) by A5, SCMFSA_2:69;
then (Comput (P,s,3)) . (intloc 3) = s . (intloc 0) by A7, SCMFSA_2:63;
then A14: (Comput (P,s,4)) . (intloc 3) = s . (intloc 0) by A9, SCMFSA_2:69;
IC (Comput (P,s,4)) = 4 by A9, SCMFSA_2:69;
then A15: 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 A16: (Comput (P,s,5)) . (IC ) = (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 A1, Lm1 ;
then A18: (Comput (P,s,6)) . (IC ) = 6 by SCMFSA_2:69;
IC (Comput (P,s,6)) = 6 by A17, SCMFSA_2:69;
then A19: 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 A20: (Comput (P,s,7)) . (IC ) = (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 A1, Lm1 ;
then A22: (Comput (P,s,8)) . (IC ) = 8 by SCMFSA_2:69;
IC (Comput (P,s,8)) = 8 by A21, SCMFSA_2:69;
then A23: 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 A24: (Comput (P,s,9)) . (IC ) = (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 A1, Lm1 ;
then A26: (Comput (P,s,10)) . (IC ) = 10 by SCMFSA_2:69;
A27: (Comput (P,s,1)) . (fsloc 0) = s . (fsloc 0) by A3, SCMFSA_2:63;
then A28: (Comput (P,s,2)) . (fsloc 0) = s . (fsloc 0) by A5, SCMFSA_2:69;
then A29: (Comput (P,s,3)) . (fsloc 0) = s . (fsloc 0) by A7, SCMFSA_2:63;
then A30: (Comput (P,s,4)) . (fsloc 0) = s . (fsloc 0) by A9, SCMFSA_2:69;
then A31: (Comput (P,s,5)) . (fsloc 0) = s . (fsloc 0) by A15, SCMFSA_2:63;
then A32: (Comput (P,s,6)) . (fsloc 0) = s . (fsloc 0) by A17, SCMFSA_2:69;
then A33: (Comput (P,s,7)) . (fsloc 0) = s . (fsloc 0) by A19, SCMFSA_2:63;
then A34: (Comput (P,s,8)) . (fsloc 0) = s . (fsloc 0) by A21, SCMFSA_2:69;
then A35: (Comput (P,s,9)) . (fsloc 0) = s . (fsloc 0) by A23, SCMFSA_2:63;
then A36: (Comput (P,s,10)) . (fsloc 0) = s . (fsloc 0) by A25, SCMFSA_2:69;
A37: (Comput (P,s,3)) . (intloc 0) = s . (intloc 0) by A13, A7, SCMFSA_2:63;
then A38: (Comput (P,s,4)) . (intloc 0) = s . (intloc 0) by A9, SCMFSA_2:69;
then (Comput (P,s,5)) . (intloc 4) = s . (intloc 0) by A15, SCMFSA_2:63;
then A39: (Comput (P,s,6)) . (intloc 4) = s . (intloc 0) by A17, SCMFSA_2:69;
A40: intloc 4 <> intloc 0 by SCMFSA_2:101;
then A41: (Comput (P,s,5)) . (intloc 0) = s . (intloc 0) by A38, A15, SCMFSA_2:63;
then A42: (Comput (P,s,6)) . (intloc 0) = s . (intloc 0) by A17, SCMFSA_2:69;
then (Comput (P,s,7)) . (intloc 5) = s . (intloc 0) by A19, SCMFSA_2:63;
then A43: (Comput (P,s,8)) . (intloc 5) = s . (intloc 0) by A21, SCMFSA_2:69;
intloc 4 <> intloc 5 by SCMFSA_2:101;
then (Comput (P,s,7)) . (intloc 4) = s . (intloc 0) by A39, A19, SCMFSA_2:63;
then A44: (Comput (P,s,8)) . (intloc 4) = s . (intloc 0) by A21, SCMFSA_2:69;
intloc 4 <> intloc 6 by SCMFSA_2:101;
then (Comput (P,s,9)) . (intloc 4) = s . (intloc 0) by A44, A23, SCMFSA_2:63;
then A45: (Comput (P,s,10)) . (intloc 4) = s . (intloc 0) by A25, SCMFSA_2:69;
intloc 5 <> intloc 6 by SCMFSA_2:101;
then (Comput (P,s,9)) . (intloc 5) = s . (intloc 0) by A43, A23, SCMFSA_2:63;
then A46: (Comput (P,s,10)) . (intloc 5) = s . (intloc 0) by A25, SCMFSA_2:69;
A47: intloc 5 <> intloc 0 by SCMFSA_2:101;
then A48: (Comput (P,s,7)) . (intloc 0) = s . (intloc 0) by A42, A19, SCMFSA_2:63;
then A49: (Comput (P,s,8)) . (intloc 0) = s . (intloc 0) by A21, SCMFSA_2:69;
then (Comput (P,s,9)) . (intloc 6) = s . (intloc 0) by A23, SCMFSA_2:63;
then A50: (Comput (P,s,10)) . (intloc 6) = s . (intloc 0) by A25, SCMFSA_2:69;
IC (Comput (P,s,10)) = 10 by A25, SCMFSA_2:69;
then A51: 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 A52: (Comput (P,s,11)) . (IC ) = (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)) . (intloc 0) = s . (intloc 0) by A49, A23, SCMFSA_2:63;
then A55: (Comput (P,s,10)) . (intloc 0) = s . (intloc 0) by A25, 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 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
A56: k > 0 and
A57: 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 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)) . (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 A3, A4, A11, 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 A12, A27, A5, 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 A13, A28, A7, A8, 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 A37, A29, A9, 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 A38, A30, A15, A16, A40, 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 A41, A31, A17, 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 A42, A32, A19, A20, A47, 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 A48, A33, A21, 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 A49, A34, A23, A24, A53, 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 A54, A35, A25, SCMFSA_2:69; :: thesis: verum
end;
suppose A58: 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 A52; :: thesis: ( (Comput (P,s,k)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,k)) . (fsloc 0) = s . (fsloc 0) )
thus (Comput (P,s,k)) . (intloc 0) = s . (intloc 0) by A55, A51, A58, SCMFSA_2:74; :: thesis: (Comput (P,s,k)) . (fsloc 0) = s . (fsloc 0)
thus (Comput (P,s,k)) . (fsloc 0) = s . (fsloc 0) by A36, A51, A58, SCMFSA_2:74; :: thesis: verum
end;
end;
end;
thus (Comput (P,s,11)) . (intloc 1) = len (s . (fsloc 0)) by A36, A51, 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 A3, SCMFSA_2:63;
then A59: (Comput (P,s,2)) . (intloc 2) = s . (intloc 0) by A5, SCMFSA_2:69;
intloc 2 <> intloc 3 by SCMFSA_2:101;
then (Comput (P,s,3)) . (intloc 2) = s . (intloc 0) by A59, A7, SCMFSA_2:63;
then A60: (Comput (P,s,4)) . (intloc 2) = s . (intloc 0) by A9, SCMFSA_2:69;
intloc 2 <> intloc 4 by SCMFSA_2:101;
then (Comput (P,s,5)) . (intloc 2) = s . (intloc 0) by A60, A15, SCMFSA_2:63;
then A61: (Comput (P,s,6)) . (intloc 2) = s . (intloc 0) by A17, SCMFSA_2:69;
intloc 2 <> intloc 5 by SCMFSA_2:101;
then (Comput (P,s,7)) . (intloc 2) = s . (intloc 0) by A61, A19, SCMFSA_2:63;
then A62: (Comput (P,s,8)) . (intloc 2) = s . (intloc 0) by A21, SCMFSA_2:69;
intloc 2 <> intloc 6 by SCMFSA_2:101;
then (Comput (P,s,9)) . (intloc 2) = s . (intloc 0) by A62, A23, SCMFSA_2:63;
then A63: (Comput (P,s,10)) . (intloc 2) = s . (intloc 0) by A25, SCMFSA_2:69;
intloc 3 <> intloc 4 by SCMFSA_2:101;
then (Comput (P,s,5)) . (intloc 3) = s . (intloc 0) by A14, A15, SCMFSA_2:63;
then A64: (Comput (P,s,6)) . (intloc 3) = s . (intloc 0) by A17, SCMFSA_2:69;
intloc 3 <> intloc 5 by SCMFSA_2:101;
then (Comput (P,s,7)) . (intloc 3) = s . (intloc 0) by A64, A19, SCMFSA_2:63;
then A65: (Comput (P,s,8)) . (intloc 3) = s . (intloc 0) by A21, SCMFSA_2:69;
intloc 3 <> intloc 6 by SCMFSA_2:101;
then (Comput (P,s,9)) . (intloc 3) = s . (intloc 0) by A65, A23, SCMFSA_2:63;
then A66: (Comput (P,s,10)) . (intloc 3) = s . (intloc 0) by A25, SCMFSA_2:69;
intloc 2 <> intloc 1 by SCMFSA_2:101;
hence (Comput (P,s,11)) . (intloc 2) = s . (intloc 0) by A63, A51, 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 A66, A51, 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 A45, A51, 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 A46, A51, 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 A50, A51, SCMFSA_2:74; :: thesis: verum