let s be 0 -started State of SCM+FSA; ( Insert-Sort-Algorithm c= s implies ( ( for k being Element of NAT st k > 0 & k < 12 holds
( (Comput ((ProgramPart s),s,k)) . (IC SCM+FSA) = k & (Comput ((ProgramPart s),s,k)) . (intloc 0) = s . (intloc 0) & (Comput ((ProgramPart s),s,k)) . (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 A1:
Insert-Sort-Algorithm c= s
; ( ( for k being Element of NAT st k > 0 & k < 12 holds
( (Comput ((ProgramPart s),s,k)) . (IC SCM+FSA) = k & (Comput ((ProgramPart s),s,k)) . (intloc 0) = s . (intloc 0) & (Comput ((ProgramPart s),s,k)) . (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) )
X0:
(ProgramPart s) . 0 = s . 0
by COMPOS_1:2;
X1:
(ProgramPart s) . 1 = s . 1
by COMPOS_1:2;
X2:
(ProgramPart s) . 2 = s . 2
by COMPOS_1:2;
X3:
(ProgramPart s) . 3 = s . 3
by COMPOS_1:2;
X4:
(ProgramPart s) . 4 = s . 4
by COMPOS_1:2;
X5:
(ProgramPart s) . 5 = s . 5
by COMPOS_1:2;
X6:
(ProgramPart s) . 6 = s . 6
by COMPOS_1:2;
X7:
(ProgramPart s) . 7 = s . 7
by COMPOS_1:2;
X8:
(ProgramPart s) . 8 = s . 8
by COMPOS_1:2;
X9:
(ProgramPart s) . 9 = s . 9
by COMPOS_1:2;
X10:
(ProgramPart s) . 10 = s . 10
by COMPOS_1:2;
A3:
Comput ((ProgramPart s),s,0) = s
by EXTPRO_1:3;
then A4:
IC (Comput ((ProgramPart s),s,0)) = 0
by COMPOS_1:def 16;
then A5: Comput ((ProgramPart s),s,(0 + 1)) =
Exec ((s . 0),(Comput ((ProgramPart s),s,0)))
by X0, EXTPRO_1:7
.=
Exec (((intloc 2) := (intloc 0)),(Comput ((ProgramPart s),s,0)))
by A1, Lm1
;
then A6: (Comput ((ProgramPart s),s,1)) . (IC SCM+FSA) =
succ (IC (Comput ((ProgramPart s),s,0)))
by SCMFSA_2:89
.=
1
by A4
;
then
IC (Comput ((ProgramPart s),s,1)) = 1
;
then A7: Comput ((ProgramPart s),s,(1 + 1)) =
Exec ((s . 1),(Comput ((ProgramPart s),s,1)))
by X1, EXTPRO_1:7
.=
Exec ((goto 2),(Comput ((ProgramPart s),s,1)))
by A1, Lm1
;
then A8:
(Comput ((ProgramPart s),s,2)) . (IC SCM+FSA) = 2
by SCMFSA_2:95;
IC (Comput ((ProgramPart s),s,2)) = 2
by A7, SCMFSA_2:95;
then A9: Comput ((ProgramPart s),s,(2 + 1)) =
Exec ((s . 2),(Comput ((ProgramPart s),s,2)))
by X2, EXTPRO_1:7
.=
Exec (((intloc 3) := (intloc 0)),(Comput ((ProgramPart s),s,2)))
by A1, Lm1
;
then A10: (Comput ((ProgramPart s),s,3)) . (IC SCM+FSA) =
succ (IC (Comput ((ProgramPart s),s,2)))
by SCMFSA_2:89
.=
3
by A8
;
then
IC (Comput ((ProgramPart s),s,3)) = 3
;
then A11: Comput ((ProgramPart s),s,(3 + 1)) =
Exec ((s . 3),(Comput ((ProgramPart s),s,3)))
by X3, EXTPRO_1:7
.=
Exec ((goto 4),(Comput ((ProgramPart s),s,3)))
by A1, Lm1
;
then A12:
(Comput ((ProgramPart s),s,4)) . (IC SCM+FSA) = 4
by SCMFSA_2:95;
A13:
intloc 2 <> intloc 0
by SCMFSA_2:128;
then A14:
(Comput ((ProgramPart s),s,1)) . (intloc 0) = s . (intloc 0)
by A3, A5, SCMFSA_2:89;
then A15:
(Comput ((ProgramPart s),s,2)) . (intloc 0) = s . (intloc 0)
by A7, SCMFSA_2:95;
then
(Comput ((ProgramPart s),s,3)) . (intloc 3) = s . (intloc 0)
by A9, SCMFSA_2:89;
then A16:
(Comput ((ProgramPart s),s,4)) . (intloc 3) = s . (intloc 0)
by A11, SCMFSA_2:95;
IC (Comput ((ProgramPart s),s,4)) = 4
by A11, SCMFSA_2:95;
then A17: Comput ((ProgramPart s),s,(4 + 1)) =
Exec ((s . 4),(Comput ((ProgramPart s),s,4)))
by X4, EXTPRO_1:7
.=
Exec (((intloc 4) := (intloc 0)),(Comput ((ProgramPart s),s,4)))
by A1, Lm1
;
then A18: (Comput ((ProgramPart s),s,5)) . (IC SCM+FSA) =
succ (IC (Comput ((ProgramPart s),s,4)))
by SCMFSA_2:89
.=
5
by A12
;
then
IC (Comput ((ProgramPart s),s,5)) = 5
;
then A19: Comput ((ProgramPart s),s,(5 + 1)) =
Exec ((s . 5),(Comput ((ProgramPart s),s,5)))
by X5, EXTPRO_1:7
.=
Exec ((goto 6),(Comput ((ProgramPart s),s,5)))
by A1, Lm1
;
then A20:
(Comput ((ProgramPart s),s,6)) . (IC SCM+FSA) = 6
by SCMFSA_2:95;
IC (Comput ((ProgramPart s),s,6)) = 6
by A19, SCMFSA_2:95;
then A21: Comput ((ProgramPart s),s,(6 + 1)) =
Exec ((s . 6),(Comput ((ProgramPart s),s,6)))
by X6, EXTPRO_1:7
.=
Exec (((intloc 5) := (intloc 0)),(Comput ((ProgramPart s),s,6)))
by A1, Lm1
;
then A22: (Comput ((ProgramPart s),s,7)) . (IC SCM+FSA) =
succ (IC (Comput ((ProgramPart s),s,6)))
by SCMFSA_2:89
.=
7
by A20
;
then
IC (Comput ((ProgramPart s),s,7)) = 7
;
then A23: Comput ((ProgramPart s),s,(7 + 1)) =
Exec ((s . 7),(Comput ((ProgramPart s),s,7)))
by X7, EXTPRO_1:7
.=
Exec ((goto 8),(Comput ((ProgramPart s),s,7)))
by A1, Lm1
;
then A24:
(Comput ((ProgramPart s),s,8)) . (IC SCM+FSA) = 8
by SCMFSA_2:95;
IC (Comput ((ProgramPart s),s,8)) = 8
by A23, SCMFSA_2:95;
then A25: Comput ((ProgramPart s),s,(8 + 1)) =
Exec ((s . 8),(Comput ((ProgramPart s),s,8)))
by X8, EXTPRO_1:7
.=
Exec (((intloc 6) := (intloc 0)),(Comput ((ProgramPart s),s,8)))
by A1, Lm1
;
then A26: (Comput ((ProgramPart s),s,9)) . (IC SCM+FSA) =
succ (IC (Comput ((ProgramPart s),s,8)))
by SCMFSA_2:89
.=
9
by A24
;
then
IC (Comput ((ProgramPart s),s,9)) = 9
;
then A27: Comput ((ProgramPart s),s,(9 + 1)) =
Exec ((s . 9),(Comput ((ProgramPart s),s,9)))
by X9, EXTPRO_1:7
.=
Exec ((goto 10),(Comput ((ProgramPart s),s,9)))
by A1, Lm1
;
then A28:
(Comput ((ProgramPart s),s,10)) . (IC SCM+FSA) = 10
by SCMFSA_2:95;
A29:
(Comput ((ProgramPart s),s,1)) . (fsloc 0) = s . (fsloc 0)
by A3, A5, SCMFSA_2:89;
then A30:
(Comput ((ProgramPart s),s,2)) . (fsloc 0) = s . (fsloc 0)
by A7, SCMFSA_2:95;
then A31:
(Comput ((ProgramPart s),s,3)) . (fsloc 0) = s . (fsloc 0)
by A9, SCMFSA_2:89;
then A32:
(Comput ((ProgramPart s),s,4)) . (fsloc 0) = s . (fsloc 0)
by A11, SCMFSA_2:95;
then A33:
(Comput ((ProgramPart s),s,5)) . (fsloc 0) = s . (fsloc 0)
by A17, SCMFSA_2:89;
then A34:
(Comput ((ProgramPart s),s,6)) . (fsloc 0) = s . (fsloc 0)
by A19, SCMFSA_2:95;
then A35:
(Comput ((ProgramPart s),s,7)) . (fsloc 0) = s . (fsloc 0)
by A21, SCMFSA_2:89;
then A36:
(Comput ((ProgramPart s),s,8)) . (fsloc 0) = s . (fsloc 0)
by A23, SCMFSA_2:95;
then A37:
(Comput ((ProgramPart s),s,9)) . (fsloc 0) = s . (fsloc 0)
by A25, SCMFSA_2:89;
then A38:
(Comput ((ProgramPart s),s,10)) . (fsloc 0) = s . (fsloc 0)
by A27, SCMFSA_2:95;
A39:
(Comput ((ProgramPart s),s,3)) . (intloc 0) = s . (intloc 0)
by A15, A9, SCMFSA_2:89;
then A40:
(Comput ((ProgramPart s),s,4)) . (intloc 0) = s . (intloc 0)
by A11, SCMFSA_2:95;
then
(Comput ((ProgramPart s),s,5)) . (intloc 4) = s . (intloc 0)
by A17, SCMFSA_2:89;
then A41:
(Comput ((ProgramPart s),s,6)) . (intloc 4) = s . (intloc 0)
by A19, SCMFSA_2:95;
A42:
intloc 4 <> intloc 0
by SCMFSA_2:128;
then A43:
(Comput ((ProgramPart s),s,5)) . (intloc 0) = s . (intloc 0)
by A40, A17, SCMFSA_2:89;
then A44:
(Comput ((ProgramPart s),s,6)) . (intloc 0) = s . (intloc 0)
by A19, SCMFSA_2:95;
then
(Comput ((ProgramPart s),s,7)) . (intloc 5) = s . (intloc 0)
by A21, SCMFSA_2:89;
then A45:
(Comput ((ProgramPart s),s,8)) . (intloc 5) = s . (intloc 0)
by A23, SCMFSA_2:95;
intloc 4 <> intloc 5
by SCMFSA_2:128;
then
(Comput ((ProgramPart s),s,7)) . (intloc 4) = s . (intloc 0)
by A41, A21, SCMFSA_2:89;
then A46:
(Comput ((ProgramPart s),s,8)) . (intloc 4) = s . (intloc 0)
by A23, SCMFSA_2:95;
intloc 4 <> intloc 6
by SCMFSA_2:128;
then
(Comput ((ProgramPart s),s,9)) . (intloc 4) = s . (intloc 0)
by A46, A25, SCMFSA_2:89;
then A47:
(Comput ((ProgramPart s),s,10)) . (intloc 4) = s . (intloc 0)
by A27, SCMFSA_2:95;
intloc 5 <> intloc 6
by SCMFSA_2:128;
then
(Comput ((ProgramPart s),s,9)) . (intloc 5) = s . (intloc 0)
by A45, A25, SCMFSA_2:89;
then A48:
(Comput ((ProgramPart s),s,10)) . (intloc 5) = s . (intloc 0)
by A27, SCMFSA_2:95;
A49:
intloc 5 <> intloc 0
by SCMFSA_2:128;
then A50:
(Comput ((ProgramPart s),s,7)) . (intloc 0) = s . (intloc 0)
by A44, A21, SCMFSA_2:89;
then A51:
(Comput ((ProgramPart s),s,8)) . (intloc 0) = s . (intloc 0)
by A23, SCMFSA_2:95;
then
(Comput ((ProgramPart s),s,9)) . (intloc 6) = s . (intloc 0)
by A25, SCMFSA_2:89;
then A52:
(Comput ((ProgramPart s),s,10)) . (intloc 6) = s . (intloc 0)
by A27, SCMFSA_2:95;
IC (Comput ((ProgramPart s),s,10)) = 10
by A27, SCMFSA_2:95;
then A53: Comput ((ProgramPart s),s,(10 + 1)) =
Exec ((s . 10),(Comput ((ProgramPart s),s,10)))
by X10, EXTPRO_1:7
.=
Exec (((intloc 1) :=len (fsloc 0)),(Comput ((ProgramPart s),s,10)))
by A1, Lm1
;
then A54: (Comput ((ProgramPart s),s,11)) . (IC SCM+FSA) =
succ (IC (Comput ((ProgramPart s),s,10)))
by SCMFSA_2:100
.=
11
by A28
;
A55:
intloc 6 <> intloc 0
by SCMFSA_2:128;
then A56:
(Comput ((ProgramPart s),s,9)) . (intloc 0) = s . (intloc 0)
by A51, A25, SCMFSA_2:89;
then A57:
(Comput ((ProgramPart s),s,10)) . (intloc 0) = s . (intloc 0)
by A27, SCMFSA_2:95;
hereby ( (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) )
let k be
Element of
NAT ;
( k > 0 & k < 12 implies ( (Comput ((ProgramPart s),s,b1)) . (IC SCM+FSA) = b1 & (Comput ((ProgramPart s),s,b1)) . (intloc 0) = s . (intloc 0) & (Comput ((ProgramPart s),s,b1)) . (fsloc 0) = s . (fsloc 0) ) )assume that A58:
k > 0
and A59:
k < 12
;
( (Comput ((ProgramPart s),s,b1)) . (IC SCM+FSA) = b1 & (Comput ((ProgramPart s),s,b1)) . (intloc 0) = s . (intloc 0) & (Comput ((ProgramPart s),s,b1)) . (fsloc 0) = s . (fsloc 0) )set c1 =
(Comput ((ProgramPart s),s,k)) . (IC SCM+FSA);
set d1 =
k;
set c2 =
(Comput ((ProgramPart s),s,k)) . (intloc 0);
set d2 =
s . (intloc 0);
set c3 =
(Comput ((ProgramPart s),s,k)) . (fsloc 0);
set d3 =
s . (fsloc 0);
k < 11
+ 1
by A59;
then A60:
k <= 11
by NAT_1:13;
per cases
( k = 1 or k = 2 or k = 3 or k = 4 or k = 5 or k = 6 or k = 7 or k = 8 or k = 9 or k = 10 or k = 11 )
by A58, A60, NAT_1:36;
suppose
k = 1
;
( (Comput ((ProgramPart s),s,b1)) . (IC SCM+FSA) = b1 & (Comput ((ProgramPart s),s,b1)) . (intloc 0) = s . (intloc 0) & (Comput ((ProgramPart s),s,b1)) . (fsloc 0) = s . (fsloc 0) )hence
(
(Comput ((ProgramPart s),s,k)) . (IC SCM+FSA) = k &
(Comput ((ProgramPart s),s,k)) . (intloc 0) = s . (intloc 0) &
(Comput ((ProgramPart s),s,k)) . (fsloc 0) = s . (fsloc 0) )
by A3, A5, A6, A13, SCMFSA_2:89;
verum end; suppose
k = 3
;
( (Comput ((ProgramPart s),s,b1)) . (IC SCM+FSA) = b1 & (Comput ((ProgramPart s),s,b1)) . (intloc 0) = s . (intloc 0) & (Comput ((ProgramPart s),s,b1)) . (fsloc 0) = s . (fsloc 0) )hence
(
(Comput ((ProgramPart s),s,k)) . (IC SCM+FSA) = k &
(Comput ((ProgramPart s),s,k)) . (intloc 0) = s . (intloc 0) &
(Comput ((ProgramPart s),s,k)) . (fsloc 0) = s . (fsloc 0) )
by A15, A30, A9, A10, SCMFSA_2:89;
verum end; suppose
k = 5
;
( (Comput ((ProgramPart s),s,b1)) . (IC SCM+FSA) = b1 & (Comput ((ProgramPart s),s,b1)) . (intloc 0) = s . (intloc 0) & (Comput ((ProgramPart s),s,b1)) . (fsloc 0) = s . (fsloc 0) )hence
(
(Comput ((ProgramPart s),s,k)) . (IC SCM+FSA) = k &
(Comput ((ProgramPart s),s,k)) . (intloc 0) = s . (intloc 0) &
(Comput ((ProgramPart s),s,k)) . (fsloc 0) = s . (fsloc 0) )
by A40, A32, A17, A18, A42, SCMFSA_2:89;
verum end; suppose
k = 7
;
( (Comput ((ProgramPart s),s,b1)) . (IC SCM+FSA) = b1 & (Comput ((ProgramPart s),s,b1)) . (intloc 0) = s . (intloc 0) & (Comput ((ProgramPart s),s,b1)) . (fsloc 0) = s . (fsloc 0) )hence
(
(Comput ((ProgramPart s),s,k)) . (IC SCM+FSA) = k &
(Comput ((ProgramPart s),s,k)) . (intloc 0) = s . (intloc 0) &
(Comput ((ProgramPart s),s,k)) . (fsloc 0) = s . (fsloc 0) )
by A44, A34, A21, A22, A49, SCMFSA_2:89;
verum end; suppose
k = 9
;
( (Comput ((ProgramPart s),s,b1)) . (IC SCM+FSA) = b1 & (Comput ((ProgramPart s),s,b1)) . (intloc 0) = s . (intloc 0) & (Comput ((ProgramPart s),s,b1)) . (fsloc 0) = s . (fsloc 0) )hence
(
(Comput ((ProgramPart s),s,k)) . (IC SCM+FSA) = k &
(Comput ((ProgramPart s),s,k)) . (intloc 0) = s . (intloc 0) &
(Comput ((ProgramPart s),s,k)) . (fsloc 0) = s . (fsloc 0) )
by A51, A36, A25, A26, A55, SCMFSA_2:89;
verum end; suppose S:
k = 11
;
( (Comput ((ProgramPart s),s,b1)) . (IC SCM+FSA) = b1 & (Comput ((ProgramPart s),s,b1)) . (intloc 0) = s . (intloc 0) & (Comput ((ProgramPart s),s,b1)) . (fsloc 0) = s . (fsloc 0) )hence
(Comput ((ProgramPart s),s,k)) . (IC SCM+FSA) = k
by A54;
( (Comput ((ProgramPart s),s,k)) . (intloc 0) = s . (intloc 0) & (Comput ((ProgramPart s),s,k)) . (fsloc 0) = s . (fsloc 0) )
intloc 0 <> intloc 1
by SCMFSA_2:128;
hence
(Comput ((ProgramPart s),s,k)) . (intloc 0) = s . (intloc 0)
by A57, A53, S, SCMFSA_2:100;
(Comput ((ProgramPart s),s,k)) . (fsloc 0) = s . (fsloc 0)thus
(Comput ((ProgramPart s),s,k)) . (fsloc 0) = s . (fsloc 0)
by A38, A53, S, SCMFSA_2:100;
verum end;
end;
thus
(Comput ((ProgramPart s),s,11)) . (intloc 1) = len (s . (fsloc 0))
by A38, A53, 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) )
(Comput ((ProgramPart s),s,1)) . (intloc 2) = s . (intloc 0)
by A3, A5, SCMFSA_2:89;
then A61:
(Comput ((ProgramPart s),s,2)) . (intloc 2) = s . (intloc 0)
by A7, SCMFSA_2:95;
intloc 2 <> intloc 3
by SCMFSA_2:128;
then
(Comput ((ProgramPart s),s,3)) . (intloc 2) = s . (intloc 0)
by A61, A9, SCMFSA_2:89;
then A62:
(Comput ((ProgramPart s),s,4)) . (intloc 2) = s . (intloc 0)
by A11, SCMFSA_2:95;
intloc 2 <> intloc 4
by SCMFSA_2:128;
then
(Comput ((ProgramPart s),s,5)) . (intloc 2) = s . (intloc 0)
by A62, A17, SCMFSA_2:89;
then A63:
(Comput ((ProgramPart s),s,6)) . (intloc 2) = s . (intloc 0)
by A19, SCMFSA_2:95;
intloc 2 <> intloc 5
by SCMFSA_2:128;
then
(Comput ((ProgramPart s),s,7)) . (intloc 2) = s . (intloc 0)
by A63, A21, SCMFSA_2:89;
then A64:
(Comput ((ProgramPart s),s,8)) . (intloc 2) = s . (intloc 0)
by A23, SCMFSA_2:95;
intloc 2 <> intloc 6
by SCMFSA_2:128;
then
(Comput ((ProgramPart s),s,9)) . (intloc 2) = s . (intloc 0)
by A64, A25, SCMFSA_2:89;
then A65:
(Comput ((ProgramPart s),s,10)) . (intloc 2) = s . (intloc 0)
by A27, SCMFSA_2:95;
intloc 3 <> intloc 4
by SCMFSA_2:128;
then
(Comput ((ProgramPart s),s,5)) . (intloc 3) = s . (intloc 0)
by A16, A17, SCMFSA_2:89;
then A66:
(Comput ((ProgramPart s),s,6)) . (intloc 3) = s . (intloc 0)
by A19, SCMFSA_2:95;
intloc 3 <> intloc 5
by SCMFSA_2:128;
then
(Comput ((ProgramPart s),s,7)) . (intloc 3) = s . (intloc 0)
by A66, A21, SCMFSA_2:89;
then A67:
(Comput ((ProgramPart s),s,8)) . (intloc 3) = s . (intloc 0)
by A23, SCMFSA_2:95;
intloc 3 <> intloc 6
by SCMFSA_2:128;
then
(Comput ((ProgramPart s),s,9)) . (intloc 3) = s . (intloc 0)
by A67, A25, SCMFSA_2:89;
then A68:
(Comput ((ProgramPart s),s,10)) . (intloc 3) = s . (intloc 0)
by A27, SCMFSA_2:95;
intloc 2 <> intloc 1
by SCMFSA_2:128;
hence
(Comput ((ProgramPart s),s,11)) . (intloc 2) = s . (intloc 0)
by A65, A53, 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) )
intloc 3 <> intloc 1
by SCMFSA_2:128;
hence
(Comput ((ProgramPart s),s,11)) . (intloc 3) = s . (intloc 0)
by A68, A53, 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) )
intloc 4 <> intloc 1
by SCMFSA_2:128;
hence
(Comput ((ProgramPart s),s,11)) . (intloc 4) = s . (intloc 0)
by A47, A53, SCMFSA_2:100; ( (Comput ((ProgramPart s),s,11)) . (intloc 5) = s . (intloc 0) & (Comput ((ProgramPart s),s,11)) . (intloc 6) = s . (intloc 0) )
intloc 5 <> intloc 1
by SCMFSA_2:128;
hence
(Comput ((ProgramPart s),s,11)) . (intloc 5) = s . (intloc 0)
by A48, A53, SCMFSA_2:100; (Comput ((ProgramPart s),s,11)) . (intloc 6) = s . (intloc 0)
intloc 6 <> intloc 1
by SCMFSA_2:128;
hence
(Comput ((ProgramPart s),s,11)) . (intloc 6) = s . (intloc 0)
by A52, A53, SCMFSA_2:100; verum