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