let s be 0 -started State of SCM+FSA; for P being Instruction-Sequence of SCM+FSA st Bubble-Sort-Algorithm c= P holds
( (Comput (P,s,1)) . (IC ) = 1 & (Comput (P,s,1)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,1)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,2)) . (IC ) = 2 & (Comput (P,s,2)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,2)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,3)) . (IC ) = 3 & (Comput (P,s,3)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,3)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,4)) . (IC ) = 4 & (Comput (P,s,4)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,4)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,5)) . (IC ) = 5 & (Comput (P,s,5)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,5)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,6)) . (IC ) = 6 & (Comput (P,s,6)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,6)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,7)) . (IC ) = 7 & (Comput (P,s,7)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,7)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,8)) . (IC ) = 8 & (Comput (P,s,8)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,8)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,9)) . (IC ) = 9 & (Comput (P,s,9)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,9)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,10)) . (IC ) = 10 & (Comput (P,s,10)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,10)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,11)) . (IC ) = 11 & (Comput (P,s,11)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,11)) . (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; ( Bubble-Sort-Algorithm c= P implies ( (Comput (P,s,1)) . (IC ) = 1 & (Comput (P,s,1)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,1)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,2)) . (IC ) = 2 & (Comput (P,s,2)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,2)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,3)) . (IC ) = 3 & (Comput (P,s,3)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,3)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,4)) . (IC ) = 4 & (Comput (P,s,4)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,4)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,5)) . (IC ) = 5 & (Comput (P,s,5)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,5)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,6)) . (IC ) = 6 & (Comput (P,s,6)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,6)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,7)) . (IC ) = 7 & (Comput (P,s,7)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,7)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,8)) . (IC ) = 8 & (Comput (P,s,8)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,8)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,9)) . (IC ) = 9 & (Comput (P,s,9)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,9)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,10)) . (IC ) = 10 & (Comput (P,s,10)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,10)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,11)) . (IC ) = 11 & (Comput (P,s,11)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,11)) . (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:
Bubble-Sort-Algorithm c= P
; ( (Comput (P,s,1)) . (IC ) = 1 & (Comput (P,s,1)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,1)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,2)) . (IC ) = 2 & (Comput (P,s,2)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,2)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,3)) . (IC ) = 3 & (Comput (P,s,3)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,3)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,4)) . (IC ) = 4 & (Comput (P,s,4)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,4)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,5)) . (IC ) = 5 & (Comput (P,s,5)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,5)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,6)) . (IC ) = 6 & (Comput (P,s,6)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,6)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,7)) . (IC ) = 7 & (Comput (P,s,7)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,7)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,8)) . (IC ) = 8 & (Comput (P,s,8)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,8)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,9)) . (IC ) = 9 & (Comput (P,s,9)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,9)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,10)) . (IC ) = 10 & (Comput (P,s,10)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,10)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,11)) . (IC ) = 11 & (Comput (P,s,11)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,11)) . (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, Lm20
;
hence (Comput (P,s,1)) . (IC ) =
(IC (Comput (P,s,0))) + 1
by SCMFSA_2:63
.=
1
by A2
;
( (Comput (P,s,1)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,1)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,2)) . (IC ) = 2 & (Comput (P,s,2)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,2)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,3)) . (IC ) = 3 & (Comput (P,s,3)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,3)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,4)) . (IC ) = 4 & (Comput (P,s,4)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,4)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,5)) . (IC ) = 5 & (Comput (P,s,5)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,5)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,6)) . (IC ) = 6 & (Comput (P,s,6)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,6)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,7)) . (IC ) = 7 & (Comput (P,s,7)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,7)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,8)) . (IC ) = 8 & (Comput (P,s,8)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,8)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,9)) . (IC ) = 9 & (Comput (P,s,9)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,9)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,10)) . (IC ) = 10 & (Comput (P,s,10)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,10)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,11)) . (IC ) = 11 & (Comput (P,s,11)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,11)) . (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) )
then A4:
IC (Comput (P,s,1)) = 1
;
A5:
(Comput (P,s,1)) . (intloc 2) = s . (intloc 0)
by A3, SCMFSA_2:63;
thus A6:
(Comput (P,s,1)) . (intloc 0) = s . (intloc 0)
by A3, Lm1, SCMFSA_2:63; ( (Comput (P,s,1)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,2)) . (IC ) = 2 & (Comput (P,s,2)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,2)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,3)) . (IC ) = 3 & (Comput (P,s,3)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,3)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,4)) . (IC ) = 4 & (Comput (P,s,4)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,4)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,5)) . (IC ) = 5 & (Comput (P,s,5)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,5)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,6)) . (IC ) = 6 & (Comput (P,s,6)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,6)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,7)) . (IC ) = 7 & (Comput (P,s,7)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,7)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,8)) . (IC ) = 8 & (Comput (P,s,8)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,8)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,9)) . (IC ) = 9 & (Comput (P,s,9)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,9)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,10)) . (IC ) = 10 & (Comput (P,s,10)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,10)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,11)) . (IC ) = 11 & (Comput (P,s,11)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,11)) . (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) )
thus A7:
(Comput (P,s,1)) . (fsloc 0) = s . (fsloc 0)
by A3, SCMFSA_2:63; ( (Comput (P,s,2)) . (IC ) = 2 & (Comput (P,s,2)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,2)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,3)) . (IC ) = 3 & (Comput (P,s,3)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,3)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,4)) . (IC ) = 4 & (Comput (P,s,4)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,4)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,5)) . (IC ) = 5 & (Comput (P,s,5)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,5)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,6)) . (IC ) = 6 & (Comput (P,s,6)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,6)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,7)) . (IC ) = 7 & (Comput (P,s,7)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,7)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,8)) . (IC ) = 8 & (Comput (P,s,8)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,8)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,9)) . (IC ) = 9 & (Comput (P,s,9)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,9)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,10)) . (IC ) = 10 & (Comput (P,s,10)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,10)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,11)) . (IC ) = 11 & (Comput (P,s,11)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,11)) . (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) )
A8: Comput (P,s,(1 + 1)) =
Exec ((P . 1),(Comput (P,s,1)))
by A4, EXTPRO_1:6
.=
Exec ((goto 2),(Comput (P,s,1)))
by A1, Lm20
;
hence A9:
(Comput (P,s,2)) . (IC ) = 2
by SCMFSA_2:69; ( (Comput (P,s,2)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,2)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,3)) . (IC ) = 3 & (Comput (P,s,3)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,3)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,4)) . (IC ) = 4 & (Comput (P,s,4)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,4)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,5)) . (IC ) = 5 & (Comput (P,s,5)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,5)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,6)) . (IC ) = 6 & (Comput (P,s,6)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,6)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,7)) . (IC ) = 7 & (Comput (P,s,7)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,7)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,8)) . (IC ) = 8 & (Comput (P,s,8)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,8)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,9)) . (IC ) = 9 & (Comput (P,s,9)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,9)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,10)) . (IC ) = 10 & (Comput (P,s,10)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,10)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,11)) . (IC ) = 11 & (Comput (P,s,11)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,11)) . (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) )
A10:
IC (Comput (P,s,2)) = 2
by A8, SCMFSA_2:69;
thus A11:
(Comput (P,s,2)) . (intloc 0) = s . (intloc 0)
by A6, A8, SCMFSA_2:69; ( (Comput (P,s,2)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,3)) . (IC ) = 3 & (Comput (P,s,3)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,3)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,4)) . (IC ) = 4 & (Comput (P,s,4)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,4)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,5)) . (IC ) = 5 & (Comput (P,s,5)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,5)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,6)) . (IC ) = 6 & (Comput (P,s,6)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,6)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,7)) . (IC ) = 7 & (Comput (P,s,7)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,7)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,8)) . (IC ) = 8 & (Comput (P,s,8)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,8)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,9)) . (IC ) = 9 & (Comput (P,s,9)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,9)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,10)) . (IC ) = 10 & (Comput (P,s,10)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,10)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,11)) . (IC ) = 11 & (Comput (P,s,11)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,11)) . (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) )
thus A12:
(Comput (P,s,2)) . (fsloc 0) = s . (fsloc 0)
by A7, A8, SCMFSA_2:69; ( (Comput (P,s,3)) . (IC ) = 3 & (Comput (P,s,3)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,3)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,4)) . (IC ) = 4 & (Comput (P,s,4)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,4)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,5)) . (IC ) = 5 & (Comput (P,s,5)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,5)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,6)) . (IC ) = 6 & (Comput (P,s,6)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,6)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,7)) . (IC ) = 7 & (Comput (P,s,7)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,7)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,8)) . (IC ) = 8 & (Comput (P,s,8)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,8)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,9)) . (IC ) = 9 & (Comput (P,s,9)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,9)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,10)) . (IC ) = 10 & (Comput (P,s,10)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,10)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,11)) . (IC ) = 11 & (Comput (P,s,11)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,11)) . (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) )
A13:
(Comput (P,s,2)) . (intloc 2) = s . (intloc 0)
by A5, A8, SCMFSA_2:69;
A14: Comput (P,s,(2 + 1)) =
Exec ((P . 2),(Comput (P,s,2)))
by A10, EXTPRO_1:6
.=
Exec (((intloc 3) := (intloc 0)),(Comput (P,s,2)))
by A1, Lm20
;
hence (Comput (P,s,3)) . (IC ) =
(IC (Comput (P,s,2))) + 1
by SCMFSA_2:63
.=
3
by A9
;
( (Comput (P,s,3)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,3)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,4)) . (IC ) = 4 & (Comput (P,s,4)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,4)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,5)) . (IC ) = 5 & (Comput (P,s,5)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,5)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,6)) . (IC ) = 6 & (Comput (P,s,6)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,6)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,7)) . (IC ) = 7 & (Comput (P,s,7)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,7)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,8)) . (IC ) = 8 & (Comput (P,s,8)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,8)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,9)) . (IC ) = 9 & (Comput (P,s,9)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,9)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,10)) . (IC ) = 10 & (Comput (P,s,10)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,10)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,11)) . (IC ) = 11 & (Comput (P,s,11)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,11)) . (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) )
then A15:
IC (Comput (P,s,3)) = 3
;
A16:
(Comput (P,s,3)) . (intloc 3) = s . (intloc 0)
by A11, A14, SCMFSA_2:63;
thus A17:
(Comput (P,s,3)) . (intloc 0) = s . (intloc 0)
by A11, A14, SCMFSA_2:63; ( (Comput (P,s,3)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,4)) . (IC ) = 4 & (Comput (P,s,4)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,4)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,5)) . (IC ) = 5 & (Comput (P,s,5)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,5)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,6)) . (IC ) = 6 & (Comput (P,s,6)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,6)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,7)) . (IC ) = 7 & (Comput (P,s,7)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,7)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,8)) . (IC ) = 8 & (Comput (P,s,8)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,8)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,9)) . (IC ) = 9 & (Comput (P,s,9)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,9)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,10)) . (IC ) = 10 & (Comput (P,s,10)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,10)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,11)) . (IC ) = 11 & (Comput (P,s,11)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,11)) . (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) )
thus A18:
(Comput (P,s,3)) . (fsloc 0) = s . (fsloc 0)
by A12, A14, SCMFSA_2:63; ( (Comput (P,s,4)) . (IC ) = 4 & (Comput (P,s,4)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,4)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,5)) . (IC ) = 5 & (Comput (P,s,5)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,5)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,6)) . (IC ) = 6 & (Comput (P,s,6)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,6)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,7)) . (IC ) = 7 & (Comput (P,s,7)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,7)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,8)) . (IC ) = 8 & (Comput (P,s,8)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,8)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,9)) . (IC ) = 9 & (Comput (P,s,9)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,9)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,10)) . (IC ) = 10 & (Comput (P,s,10)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,10)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,11)) . (IC ) = 11 & (Comput (P,s,11)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,11)) . (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) )
A19:
(Comput (P,s,3)) . (intloc 2) = s . (intloc 0)
by A13, A14, Lm10, SCMFSA_2:63;
A20: Comput (P,s,(3 + 1)) =
Exec ((P . 3),(Comput (P,s,3)))
by A15, EXTPRO_1:6
.=
Exec ((goto 4),(Comput (P,s,3)))
by A1, Lm20
;
hence A21:
(Comput (P,s,4)) . (IC ) = 4
by SCMFSA_2:69; ( (Comput (P,s,4)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,4)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,5)) . (IC ) = 5 & (Comput (P,s,5)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,5)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,6)) . (IC ) = 6 & (Comput (P,s,6)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,6)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,7)) . (IC ) = 7 & (Comput (P,s,7)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,7)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,8)) . (IC ) = 8 & (Comput (P,s,8)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,8)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,9)) . (IC ) = 9 & (Comput (P,s,9)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,9)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,10)) . (IC ) = 10 & (Comput (P,s,10)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,10)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,11)) . (IC ) = 11 & (Comput (P,s,11)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,11)) . (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) )
A22:
IC (Comput (P,s,4)) = 4
by A20, SCMFSA_2:69;
thus A23:
(Comput (P,s,4)) . (intloc 0) = s . (intloc 0)
by A17, A20, SCMFSA_2:69; ( (Comput (P,s,4)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,5)) . (IC ) = 5 & (Comput (P,s,5)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,5)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,6)) . (IC ) = 6 & (Comput (P,s,6)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,6)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,7)) . (IC ) = 7 & (Comput (P,s,7)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,7)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,8)) . (IC ) = 8 & (Comput (P,s,8)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,8)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,9)) . (IC ) = 9 & (Comput (P,s,9)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,9)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,10)) . (IC ) = 10 & (Comput (P,s,10)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,10)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,11)) . (IC ) = 11 & (Comput (P,s,11)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,11)) . (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) )
thus A24:
(Comput (P,s,4)) . (fsloc 0) = s . (fsloc 0)
by A18, A20, SCMFSA_2:69; ( (Comput (P,s,5)) . (IC ) = 5 & (Comput (P,s,5)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,5)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,6)) . (IC ) = 6 & (Comput (P,s,6)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,6)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,7)) . (IC ) = 7 & (Comput (P,s,7)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,7)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,8)) . (IC ) = 8 & (Comput (P,s,8)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,8)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,9)) . (IC ) = 9 & (Comput (P,s,9)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,9)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,10)) . (IC ) = 10 & (Comput (P,s,10)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,10)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,11)) . (IC ) = 11 & (Comput (P,s,11)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,11)) . (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) )
A25:
(Comput (P,s,4)) . (intloc 2) = s . (intloc 0)
by A19, A20, SCMFSA_2:69;
A26:
(Comput (P,s,4)) . (intloc 3) = s . (intloc 0)
by A16, A20, SCMFSA_2:69;
A27: Comput (P,s,(4 + 1)) =
Exec ((P . 4),(Comput (P,s,4)))
by A22, EXTPRO_1:6
.=
Exec (((intloc 4) := (intloc 0)),(Comput (P,s,4)))
by A1, Lm20
;
hence (Comput (P,s,5)) . (IC ) =
(IC (Comput (P,s,4))) + 1
by SCMFSA_2:63
.=
5
by A21
;
( (Comput (P,s,5)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,5)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,6)) . (IC ) = 6 & (Comput (P,s,6)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,6)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,7)) . (IC ) = 7 & (Comput (P,s,7)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,7)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,8)) . (IC ) = 8 & (Comput (P,s,8)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,8)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,9)) . (IC ) = 9 & (Comput (P,s,9)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,9)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,10)) . (IC ) = 10 & (Comput (P,s,10)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,10)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,11)) . (IC ) = 11 & (Comput (P,s,11)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,11)) . (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) )
then A28:
IC (Comput (P,s,5)) = 5
;
A29:
(Comput (P,s,5)) . (intloc 4) = s . (intloc 0)
by A23, A27, SCMFSA_2:63;
thus A30:
(Comput (P,s,5)) . (intloc 0) = s . (intloc 0)
by A23, A27, Lm2, SCMFSA_2:63; ( (Comput (P,s,5)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,6)) . (IC ) = 6 & (Comput (P,s,6)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,6)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,7)) . (IC ) = 7 & (Comput (P,s,7)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,7)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,8)) . (IC ) = 8 & (Comput (P,s,8)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,8)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,9)) . (IC ) = 9 & (Comput (P,s,9)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,9)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,10)) . (IC ) = 10 & (Comput (P,s,10)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,10)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,11)) . (IC ) = 11 & (Comput (P,s,11)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,11)) . (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) )
thus A31:
(Comput (P,s,5)) . (fsloc 0) = s . (fsloc 0)
by A24, A27, SCMFSA_2:63; ( (Comput (P,s,6)) . (IC ) = 6 & (Comput (P,s,6)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,6)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,7)) . (IC ) = 7 & (Comput (P,s,7)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,7)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,8)) . (IC ) = 8 & (Comput (P,s,8)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,8)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,9)) . (IC ) = 9 & (Comput (P,s,9)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,9)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,10)) . (IC ) = 10 & (Comput (P,s,10)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,10)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,11)) . (IC ) = 11 & (Comput (P,s,11)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,11)) . (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) )
A32:
(Comput (P,s,5)) . (intloc 2) = s . (intloc 0)
by A25, A27, Lm11, SCMFSA_2:63;
A33:
(Comput (P,s,5)) . (intloc 3) = s . (intloc 0)
by A26, A27, Lm14, SCMFSA_2:63;
A34: Comput (P,s,(5 + 1)) =
Exec ((P . 5),(Comput (P,s,5)))
by A28, EXTPRO_1:6
.=
Exec ((goto 6),(Comput (P,s,5)))
by A1, Lm20
;
hence A35:
(Comput (P,s,6)) . (IC ) = 6
by SCMFSA_2:69; ( (Comput (P,s,6)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,6)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,7)) . (IC ) = 7 & (Comput (P,s,7)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,7)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,8)) . (IC ) = 8 & (Comput (P,s,8)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,8)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,9)) . (IC ) = 9 & (Comput (P,s,9)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,9)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,10)) . (IC ) = 10 & (Comput (P,s,10)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,10)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,11)) . (IC ) = 11 & (Comput (P,s,11)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,11)) . (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) )
A36:
IC (Comput (P,s,6)) = 6
by A34, SCMFSA_2:69;
thus A37:
(Comput (P,s,6)) . (intloc 0) = s . (intloc 0)
by A30, A34, SCMFSA_2:69; ( (Comput (P,s,6)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,7)) . (IC ) = 7 & (Comput (P,s,7)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,7)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,8)) . (IC ) = 8 & (Comput (P,s,8)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,8)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,9)) . (IC ) = 9 & (Comput (P,s,9)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,9)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,10)) . (IC ) = 10 & (Comput (P,s,10)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,10)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,11)) . (IC ) = 11 & (Comput (P,s,11)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,11)) . (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) )
thus A38:
(Comput (P,s,6)) . (fsloc 0) = s . (fsloc 0)
by A31, A34, SCMFSA_2:69; ( (Comput (P,s,7)) . (IC ) = 7 & (Comput (P,s,7)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,7)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,8)) . (IC ) = 8 & (Comput (P,s,8)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,8)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,9)) . (IC ) = 9 & (Comput (P,s,9)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,9)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,10)) . (IC ) = 10 & (Comput (P,s,10)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,10)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,11)) . (IC ) = 11 & (Comput (P,s,11)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,11)) . (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) )
A39:
(Comput (P,s,6)) . (intloc 2) = s . (intloc 0)
by A32, A34, SCMFSA_2:69;
A40:
(Comput (P,s,6)) . (intloc 3) = s . (intloc 0)
by A33, A34, SCMFSA_2:69;
A41:
(Comput (P,s,6)) . (intloc 4) = s . (intloc 0)
by A29, A34, SCMFSA_2:69;
A42: Comput (P,s,(6 + 1)) =
Exec ((P . 6),(Comput (P,s,6)))
by A36, EXTPRO_1:6
.=
Exec (((intloc 5) := (intloc 0)),(Comput (P,s,6)))
by A1, Lm20
;
hence (Comput (P,s,7)) . (IC ) =
(IC (Comput (P,s,6))) + 1
by SCMFSA_2:63
.=
7
by A35
;
( (Comput (P,s,7)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,7)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,8)) . (IC ) = 8 & (Comput (P,s,8)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,8)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,9)) . (IC ) = 9 & (Comput (P,s,9)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,9)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,10)) . (IC ) = 10 & (Comput (P,s,10)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,10)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,11)) . (IC ) = 11 & (Comput (P,s,11)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,11)) . (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) )
then A43:
IC (Comput (P,s,7)) = 7
;
A44:
(Comput (P,s,7)) . (intloc 5) = s . (intloc 0)
by A37, A42, SCMFSA_2:63;
thus A45:
(Comput (P,s,7)) . (intloc 0) = s . (intloc 0)
by A37, A42, Lm3, SCMFSA_2:63; ( (Comput (P,s,7)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,8)) . (IC ) = 8 & (Comput (P,s,8)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,8)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,9)) . (IC ) = 9 & (Comput (P,s,9)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,9)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,10)) . (IC ) = 10 & (Comput (P,s,10)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,10)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,11)) . (IC ) = 11 & (Comput (P,s,11)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,11)) . (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) )
thus A46:
(Comput (P,s,7)) . (fsloc 0) = s . (fsloc 0)
by A38, A42, SCMFSA_2:63; ( (Comput (P,s,8)) . (IC ) = 8 & (Comput (P,s,8)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,8)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,9)) . (IC ) = 9 & (Comput (P,s,9)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,9)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,10)) . (IC ) = 10 & (Comput (P,s,10)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,10)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,11)) . (IC ) = 11 & (Comput (P,s,11)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,11)) . (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) )
A47:
(Comput (P,s,7)) . (intloc 2) = s . (intloc 0)
by A39, A42, Lm12, SCMFSA_2:63;
A48:
(Comput (P,s,7)) . (intloc 3) = s . (intloc 0)
by A40, A42, Lm15, SCMFSA_2:63;
A49:
(Comput (P,s,7)) . (intloc 4) = s . (intloc 0)
by A41, A42, Lm17, SCMFSA_2:63;
A50: Comput (P,s,(7 + 1)) =
Exec ((P . 7),(Comput (P,s,7)))
by A43, EXTPRO_1:6
.=
Exec ((goto 8),(Comput (P,s,7)))
by A1, Lm20
;
hence A51:
(Comput (P,s,8)) . (IC ) = 8
by SCMFSA_2:69; ( (Comput (P,s,8)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,8)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,9)) . (IC ) = 9 & (Comput (P,s,9)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,9)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,10)) . (IC ) = 10 & (Comput (P,s,10)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,10)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,11)) . (IC ) = 11 & (Comput (P,s,11)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,11)) . (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) )
A52:
IC (Comput (P,s,8)) = 8
by A50, SCMFSA_2:69;
thus A53:
(Comput (P,s,8)) . (intloc 0) = s . (intloc 0)
by A45, A50, SCMFSA_2:69; ( (Comput (P,s,8)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,9)) . (IC ) = 9 & (Comput (P,s,9)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,9)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,10)) . (IC ) = 10 & (Comput (P,s,10)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,10)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,11)) . (IC ) = 11 & (Comput (P,s,11)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,11)) . (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) )
thus A54:
(Comput (P,s,8)) . (fsloc 0) = s . (fsloc 0)
by A46, A50, SCMFSA_2:69; ( (Comput (P,s,9)) . (IC ) = 9 & (Comput (P,s,9)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,9)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,10)) . (IC ) = 10 & (Comput (P,s,10)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,10)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,11)) . (IC ) = 11 & (Comput (P,s,11)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,11)) . (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) )
A55:
(Comput (P,s,8)) . (intloc 2) = s . (intloc 0)
by A47, A50, SCMFSA_2:69;
A56:
(Comput (P,s,8)) . (intloc 3) = s . (intloc 0)
by A48, A50, SCMFSA_2:69;
A57:
(Comput (P,s,8)) . (intloc 4) = s . (intloc 0)
by A49, A50, SCMFSA_2:69;
A58:
(Comput (P,s,8)) . (intloc 5) = s . (intloc 0)
by A44, A50, SCMFSA_2:69;
A59: Comput (P,s,(8 + 1)) =
Exec ((P . 8),(Comput (P,s,8)))
by A52, EXTPRO_1:6
.=
Exec (((intloc 6) := (intloc 0)),(Comput (P,s,8)))
by A1, Lm20
;
hence (Comput (P,s,9)) . (IC ) =
(IC (Comput (P,s,8))) + 1
by SCMFSA_2:63
.=
9
by A51
;
( (Comput (P,s,9)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,9)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,10)) . (IC ) = 10 & (Comput (P,s,10)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,10)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,11)) . (IC ) = 11 & (Comput (P,s,11)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,11)) . (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) )
then A60:
IC (Comput (P,s,9)) = 9
;
A61:
(Comput (P,s,9)) . (intloc 6) = s . (intloc 0)
by A53, A59, SCMFSA_2:63;
thus A62:
(Comput (P,s,9)) . (intloc 0) = s . (intloc 0)
by A53, A59, Lm4, SCMFSA_2:63; ( (Comput (P,s,9)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,10)) . (IC ) = 10 & (Comput (P,s,10)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,10)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,11)) . (IC ) = 11 & (Comput (P,s,11)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,11)) . (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) )
thus A63:
(Comput (P,s,9)) . (fsloc 0) = s . (fsloc 0)
by A54, A59, SCMFSA_2:63; ( (Comput (P,s,10)) . (IC ) = 10 & (Comput (P,s,10)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,10)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,11)) . (IC ) = 11 & (Comput (P,s,11)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,11)) . (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) )
A64:
(Comput (P,s,9)) . (intloc 2) = s . (intloc 0)
by A55, A59, Lm13, SCMFSA_2:63;
A65:
(Comput (P,s,9)) . (intloc 3) = s . (intloc 0)
by A56, A59, Lm16, SCMFSA_2:63;
A66:
(Comput (P,s,9)) . (intloc 4) = s . (intloc 0)
by A57, A59, Lm18, SCMFSA_2:63;
A67:
(Comput (P,s,9)) . (intloc 5) = s . (intloc 0)
by A58, A59, Lm19, SCMFSA_2:63;
A68: Comput (P,s,(9 + 1)) =
Exec ((P . 9),(Comput (P,s,9)))
by A60, EXTPRO_1:6
.=
Exec ((goto 10),(Comput (P,s,9)))
by A1, Lm20
;
hence A69:
(Comput (P,s,10)) . (IC ) = 10
by SCMFSA_2:69; ( (Comput (P,s,10)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,10)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,11)) . (IC ) = 11 & (Comput (P,s,11)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,11)) . (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) )
A70:
IC (Comput (P,s,10)) = 10
by A68, SCMFSA_2:69;
thus A71:
(Comput (P,s,10)) . (intloc 0) = s . (intloc 0)
by A62, A68, SCMFSA_2:69; ( (Comput (P,s,10)) . (fsloc 0) = s . (fsloc 0) & (Comput (P,s,11)) . (IC ) = 11 & (Comput (P,s,11)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,11)) . (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) )
thus A72:
(Comput (P,s,10)) . (fsloc 0) = s . (fsloc 0)
by A63, A68, SCMFSA_2:69; ( (Comput (P,s,11)) . (IC ) = 11 & (Comput (P,s,11)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,11)) . (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) )
A73:
(Comput (P,s,10)) . (intloc 2) = s . (intloc 0)
by A64, A68, SCMFSA_2:69;
A74:
(Comput (P,s,10)) . (intloc 3) = s . (intloc 0)
by A65, A68, SCMFSA_2:69;
A75:
(Comput (P,s,10)) . (intloc 4) = s . (intloc 0)
by A66, A68, SCMFSA_2:69;
A76:
(Comput (P,s,10)) . (intloc 5) = s . (intloc 0)
by A67, A68, SCMFSA_2:69;
A77:
(Comput (P,s,10)) . (intloc 6) = s . (intloc 0)
by A61, A68, SCMFSA_2:69;
A78: Comput (P,s,(10 + 1)) =
Exec ((P . 10),(Comput (P,s,10)))
by A70, EXTPRO_1:6
.=
Exec (((intloc 1) :=len (fsloc 0)),(Comput (P,s,10)))
by A1, Lm20
;
hence (Comput (P,s,11)) . (IC ) =
(IC (Comput (P,s,10))) + 1
by SCMFSA_2:74
.=
11
by A69
;
( (Comput (P,s,11)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,11)) . (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) )
thus
(Comput (P,s,11)) . (intloc 0) = s . (intloc 0)
by A71, A78, SCMFSA_2:74; ( (Comput (P,s,11)) . (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) )
thus
(Comput (P,s,11)) . (fsloc 0) = s . (fsloc 0)
by A72, A78, SCMFSA_2:74; ( (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) )
thus
(Comput (P,s,11)) . (intloc 1) = len (s . (fsloc 0))
by A72, A78, SCMFSA_2:74; ( (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) )
thus
(Comput (P,s,11)) . (intloc 2) = s . (intloc 0)
by A73, A78, Lm5, SCMFSA_2:74; ( (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) )
thus
(Comput (P,s,11)) . (intloc 3) = s . (intloc 0)
by A74, A78, Lm6, SCMFSA_2:74; ( (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) )
thus
(Comput (P,s,11)) . (intloc 4) = s . (intloc 0)
by A75, A78, Lm7, SCMFSA_2:74; ( (Comput (P,s,11)) . (intloc 5) = s . (intloc 0) & (Comput (P,s,11)) . (intloc 6) = s . (intloc 0) )
thus
(Comput (P,s,11)) . (intloc 5) = s . (intloc 0)
by A76, A78, Lm8, SCMFSA_2:74; (Comput (P,s,11)) . (intloc 6) = s . (intloc 0)
thus
(Comput (P,s,11)) . (intloc 6) = s . (intloc 0)
by A77, A78, Lm9, SCMFSA_2:74; verum