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