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