let n be Element of NAT ; for s being State of SCMPDS st GCD-Algorithm c= s & IC s = 5 & n = s . SBP & s . GBP = 0 & s . (DataLoc ((s . SBP),3)) > 0 holds
( IC (Comput ((ProgramPart s),s,7)) = 5 + 7 & Comput ((ProgramPart s),s,8) = Exec ((goto (- 7)),(Comput ((ProgramPart s),s,7))) & (Comput ((ProgramPart s),s,7)) . SBP = n + 4 & (Comput ((ProgramPart s),s,7)) . GBP = 0 & (Comput ((ProgramPart s),s,7)) . (intpos (n + 7)) = (s . (DataLoc ((s . SBP),2))) mod (s . (DataLoc ((s . SBP),3))) & (Comput ((ProgramPart s),s,7)) . (intpos (n + 6)) = s . (DataLoc ((s . SBP),3)) & (Comput ((ProgramPart s),s,7)) . (intpos (n + 4)) = n & (Comput ((ProgramPart s),s,7)) . (intpos (n + 5)) = 11 )
let s be State of SCMPDS; ( GCD-Algorithm c= s & IC s = 5 & n = s . SBP & s . GBP = 0 & s . (DataLoc ((s . SBP),3)) > 0 implies ( IC (Comput ((ProgramPart s),s,7)) = 5 + 7 & Comput ((ProgramPart s),s,8) = Exec ((goto (- 7)),(Comput ((ProgramPart s),s,7))) & (Comput ((ProgramPart s),s,7)) . SBP = n + 4 & (Comput ((ProgramPart s),s,7)) . GBP = 0 & (Comput ((ProgramPart s),s,7)) . (intpos (n + 7)) = (s . (DataLoc ((s . SBP),2))) mod (s . (DataLoc ((s . SBP),3))) & (Comput ((ProgramPart s),s,7)) . (intpos (n + 6)) = s . (DataLoc ((s . SBP),3)) & (Comput ((ProgramPart s),s,7)) . (intpos (n + 4)) = n & (Comput ((ProgramPart s),s,7)) . (intpos (n + 5)) = 11 ) )
set x = s . (DataLoc ((s . SBP),2));
set y = s . (DataLoc ((s . SBP),3));
assume A1:
GCD-Algorithm c= s
; ( not IC s = 5 or not n = s . SBP or not s . GBP = 0 or not s . (DataLoc ((s . SBP),3)) > 0 or ( IC (Comput ((ProgramPart s),s,7)) = 5 + 7 & Comput ((ProgramPart s),s,8) = Exec ((goto (- 7)),(Comput ((ProgramPart s),s,7))) & (Comput ((ProgramPart s),s,7)) . SBP = n + 4 & (Comput ((ProgramPart s),s,7)) . GBP = 0 & (Comput ((ProgramPart s),s,7)) . (intpos (n + 7)) = (s . (DataLoc ((s . SBP),2))) mod (s . (DataLoc ((s . SBP),3))) & (Comput ((ProgramPart s),s,7)) . (intpos (n + 6)) = s . (DataLoc ((s . SBP),3)) & (Comput ((ProgramPart s),s,7)) . (intpos (n + 4)) = n & (Comput ((ProgramPart s),s,7)) . (intpos (n + 5)) = 11 ) )
assume A2:
IC s = 5
; ( not n = s . SBP or not s . GBP = 0 or not s . (DataLoc ((s . SBP),3)) > 0 or ( IC (Comput ((ProgramPart s),s,7)) = 5 + 7 & Comput ((ProgramPart s),s,8) = Exec ((goto (- 7)),(Comput ((ProgramPart s),s,7))) & (Comput ((ProgramPart s),s,7)) . SBP = n + 4 & (Comput ((ProgramPart s),s,7)) . GBP = 0 & (Comput ((ProgramPart s),s,7)) . (intpos (n + 7)) = (s . (DataLoc ((s . SBP),2))) mod (s . (DataLoc ((s . SBP),3))) & (Comput ((ProgramPart s),s,7)) . (intpos (n + 6)) = s . (DataLoc ((s . SBP),3)) & (Comput ((ProgramPart s),s,7)) . (intpos (n + 4)) = n & (Comput ((ProgramPart s),s,7)) . (intpos (n + 5)) = 11 ) )
assume A3:
n = s . SBP
; ( not s . GBP = 0 or not s . (DataLoc ((s . SBP),3)) > 0 or ( IC (Comput ((ProgramPart s),s,7)) = 5 + 7 & Comput ((ProgramPart s),s,8) = Exec ((goto (- 7)),(Comput ((ProgramPart s),s,7))) & (Comput ((ProgramPart s),s,7)) . SBP = n + 4 & (Comput ((ProgramPart s),s,7)) . GBP = 0 & (Comput ((ProgramPart s),s,7)) . (intpos (n + 7)) = (s . (DataLoc ((s . SBP),2))) mod (s . (DataLoc ((s . SBP),3))) & (Comput ((ProgramPart s),s,7)) . (intpos (n + 6)) = s . (DataLoc ((s . SBP),3)) & (Comput ((ProgramPart s),s,7)) . (intpos (n + 4)) = n & (Comput ((ProgramPart s),s,7)) . (intpos (n + 5)) = 11 ) )
assume A4:
s . GBP = 0
; ( not s . (DataLoc ((s . SBP),3)) > 0 or ( IC (Comput ((ProgramPart s),s,7)) = 5 + 7 & Comput ((ProgramPart s),s,8) = Exec ((goto (- 7)),(Comput ((ProgramPart s),s,7))) & (Comput ((ProgramPart s),s,7)) . SBP = n + 4 & (Comput ((ProgramPart s),s,7)) . GBP = 0 & (Comput ((ProgramPart s),s,7)) . (intpos (n + 7)) = (s . (DataLoc ((s . SBP),2))) mod (s . (DataLoc ((s . SBP),3))) & (Comput ((ProgramPart s),s,7)) . (intpos (n + 6)) = s . (DataLoc ((s . SBP),3)) & (Comput ((ProgramPart s),s,7)) . (intpos (n + 4)) = n & (Comput ((ProgramPart s),s,7)) . (intpos (n + 5)) = 11 ) )
assume A5:
s . (DataLoc ((s . SBP),3)) > 0
; ( IC (Comput ((ProgramPart s),s,7)) = 5 + 7 & Comput ((ProgramPart s),s,8) = Exec ((goto (- 7)),(Comput ((ProgramPart s),s,7))) & (Comput ((ProgramPart s),s,7)) . SBP = n + 4 & (Comput ((ProgramPart s),s,7)) . GBP = 0 & (Comput ((ProgramPart s),s,7)) . (intpos (n + 7)) = (s . (DataLoc ((s . SBP),2))) mod (s . (DataLoc ((s . SBP),3))) & (Comput ((ProgramPart s),s,7)) . (intpos (n + 6)) = s . (DataLoc ((s . SBP),3)) & (Comput ((ProgramPart s),s,7)) . (intpos (n + 4)) = n & (Comput ((ProgramPart s),s,7)) . (intpos (n + 5)) = 11 )
Y:
(ProgramPart s) /. (IC s) = s . (IC s)
by COMPOS_1:38;
Z:
(ProgramPart (Comput ((ProgramPart s),s,1))) /. (IC (Comput ((ProgramPart s),s,1))) = (Comput ((ProgramPart s),s,1)) . (IC (Comput ((ProgramPart s),s,1)))
by COMPOS_1:38;
A6: Comput ((ProgramPart s),s,(1 + 0)) =
Following ((ProgramPart s),(Comput ((ProgramPart s),s,0)))
by EXTPRO_1:4
.=
Following ((ProgramPart s),s)
by EXTPRO_1:3
.=
Exec (((SBP,3) <=0_goto 9),s)
by A1, A2, Y, Lm1
;
then A7: IC (Comput ((ProgramPart s),s,1)) =
succ (IC s)
by A5, SCMPDS_2:68
.=
5 + 1
by A2
;
then A8: CurInstr ((ProgramPart (Comput ((ProgramPart s),s,1))),(Comput ((ProgramPart s),s,1))) =
s . 6
by Z, AMI_1:54
.=
(SBP,6) := (SBP,3)
by A1, Lm1
;
T:
ProgramPart s = ProgramPart (Comput ((ProgramPart s),s,1))
by AMI_1:123;
A9: Comput ((ProgramPart s),s,(1 + 1)) =
Following ((ProgramPart s),(Comput ((ProgramPart s),s,1)))
by EXTPRO_1:4
.=
Exec (((SBP,6) := (SBP,3)),(Comput ((ProgramPart s),s,1)))
by A8, T
;
A10:
(Comput ((ProgramPart s),s,1)) . SBP = n
by A3, A6, SCMPDS_2:68;
A11:
(Comput ((ProgramPart s),s,1)) . GBP = 0
by A4, A6, SCMPDS_2:68;
A12: (Comput ((ProgramPart s),s,1)) . (intpos (n + 3)) =
(Comput ((ProgramPart s),s,1)) . (DataLoc (n,3))
by Th5
.=
s . (DataLoc ((s . SBP),3))
by A3, A6, SCMPDS_2:68
;
A13: (Comput ((ProgramPart s),s,1)) . (intpos (n + 2)) =
(Comput ((ProgramPart s),s,1)) . (DataLoc (n,2))
by Th5
.=
s . (DataLoc ((s . SBP),2))
by A3, A6, SCMPDS_2:68
;
Y:
(ProgramPart (Comput ((ProgramPart s),s,2))) /. (IC (Comput ((ProgramPart s),s,2))) = (Comput ((ProgramPart s),s,2)) . (IC (Comput ((ProgramPart s),s,2)))
by COMPOS_1:38;
A14: IC (Comput ((ProgramPart s),s,2)) =
succ (IC (Comput ((ProgramPart s),s,1)))
by A9, SCMPDS_2:59
.=
6 + 1
by A7
;
then A15: CurInstr ((ProgramPart (Comput ((ProgramPart s),s,2))),(Comput ((ProgramPart s),s,2))) =
s . 7
by Y, AMI_1:54
.=
Divide (SBP,2,SBP,3)
by A1, Lm1
;
T:
ProgramPart s = ProgramPart (Comput ((ProgramPart s),s,2))
by AMI_1:123;
A16: Comput ((ProgramPart s),s,(2 + 1)) =
Following ((ProgramPart s),(Comput ((ProgramPart s),s,2)))
by EXTPRO_1:4
.=
Exec ((Divide (SBP,2,SBP,3)),(Comput ((ProgramPart s),s,2)))
by A15, T
;
A17:
DataLoc (((Comput ((ProgramPart s),s,1)) . SBP),6) = intpos (n + 6)
by A10, Th5;
then A18:
(Comput ((ProgramPart s),s,2)) . SBP = n
by A9, A10, Lm3, SCMPDS_2:59;
A19:
(Comput ((ProgramPart s),s,2)) . GBP = 0
by A9, A11, A17, Lm2, SCMPDS_2:59;
A20: (Comput ((ProgramPart s),s,2)) . (intpos (n + 6)) =
(Comput ((ProgramPart s),s,1)) . (DataLoc (n,3))
by A9, A10, A17, SCMPDS_2:59
.=
s . (DataLoc ((s . SBP),3))
by A12, Th5
;
n + 3 <> n + 6
;
then A21:
(Comput ((ProgramPart s),s,2)) . (intpos (n + 3)) = s . (DataLoc ((s . SBP),3))
by A9, A12, A17, AMI_3:52, SCMPDS_2:59;
n + 2 <> n + 6
;
then A22:
(Comput ((ProgramPart s),s,2)) . (intpos (n + 2)) = s . (DataLoc ((s . SBP),2))
by A9, A13, A17, AMI_3:52, SCMPDS_2:59;
Y:
(ProgramPart (Comput ((ProgramPart s),s,3))) /. (IC (Comput ((ProgramPart s),s,3))) = (Comput ((ProgramPart s),s,3)) . (IC (Comput ((ProgramPart s),s,3)))
by COMPOS_1:38;
A23: IC (Comput ((ProgramPart s),s,3)) =
succ (IC (Comput ((ProgramPart s),s,2)))
by A16, SCMPDS_2:64
.=
7 + 1
by A14
;
then A24: CurInstr ((ProgramPart (Comput ((ProgramPart s),s,3))),(Comput ((ProgramPart s),s,3))) =
s . 8
by Y, AMI_1:54
.=
(SBP,7) := (SBP,3)
by A1, Lm1
;
T:
ProgramPart s = ProgramPart (Comput ((ProgramPart s),s,3))
by AMI_1:123;
A25: Comput ((ProgramPart s),s,(3 + 1)) =
Following ((ProgramPart s),(Comput ((ProgramPart s),s,3)))
by EXTPRO_1:4
.=
Exec (((SBP,7) := (SBP,3)),(Comput ((ProgramPart s),s,3)))
by A24, T
;
A26:
DataLoc (((Comput ((ProgramPart s),s,2)) . SBP),2) = intpos (n + 2)
by A18, Th5;
then A27:
SBP <> DataLoc (((Comput ((ProgramPart s),s,2)) . SBP),2)
by Lm3;
A28:
DataLoc (((Comput ((ProgramPart s),s,2)) . SBP),3) = intpos (n + 3)
by A18, Th5;
then
SBP <> DataLoc (((Comput ((ProgramPart s),s,2)) . SBP),3)
by Lm3;
then A29:
(Comput ((ProgramPart s),s,3)) . SBP = n
by A16, A18, A27, SCMPDS_2:64;
A30:
GBP <> DataLoc (((Comput ((ProgramPart s),s,2)) . SBP),2)
by A26, Lm2;
GBP <> DataLoc (((Comput ((ProgramPart s),s,2)) . SBP),3)
by A28, Lm2;
then A31:
(Comput ((ProgramPart s),s,3)) . GBP = 0
by A16, A19, A30, SCMPDS_2:64;
A32:
(Comput ((ProgramPart s),s,3)) . (intpos (n + 3)) = (s . (DataLoc ((s . SBP),2))) mod (s . (DataLoc ((s . SBP),3)))
by A16, A21, A22, A26, A28, SCMPDS_2:64;
n + 6 <> n + 2
;
then A33:
intpos (n + 6) <> DataLoc (((Comput ((ProgramPart s),s,2)) . SBP),2)
by A26, AMI_3:52;
n + 6 <> n + 3
;
then
intpos (n + 6) <> DataLoc (((Comput ((ProgramPart s),s,2)) . SBP),3)
by A28, AMI_3:52;
then A34:
(Comput ((ProgramPart s),s,3)) . (intpos (n + 6)) = s . (DataLoc ((s . SBP),3))
by A16, A20, A33, SCMPDS_2:64;
Y:
(ProgramPart (Comput ((ProgramPart s),s,4))) /. (IC (Comput ((ProgramPart s),s,4))) = (Comput ((ProgramPart s),s,4)) . (IC (Comput ((ProgramPart s),s,4)))
by COMPOS_1:38;
A35: IC (Comput ((ProgramPart s),s,4)) =
succ (IC (Comput ((ProgramPart s),s,3)))
by A25, SCMPDS_2:59
.=
8 + 1
by A23
;
then A36: CurInstr ((ProgramPart (Comput ((ProgramPart s),s,4))),(Comput ((ProgramPart s),s,4))) =
s . 9
by Y, AMI_1:54
.=
(SBP,(4 + RetSP)) := (GBP,1)
by A1, Lm1
;
T:
ProgramPart s = ProgramPart (Comput ((ProgramPart s),s,4))
by AMI_1:123;
A37: Comput ((ProgramPart s),s,(4 + 1)) =
Following ((ProgramPart s),(Comput ((ProgramPart s),s,4)))
by EXTPRO_1:4
.=
Exec (((SBP,(4 + RetSP)) := (GBP,1)),(Comput ((ProgramPart s),s,4)))
by A36, T
;
A38:
DataLoc (((Comput ((ProgramPart s),s,3)) . SBP),7) = intpos (n + 7)
by A29, Th5;
then A39:
(Comput ((ProgramPart s),s,4)) . SBP = n
by A25, A29, Lm3, SCMPDS_2:59;
A40:
(Comput ((ProgramPart s),s,4)) . GBP = 0
by A25, A31, A38, Lm2, SCMPDS_2:59;
A41: (Comput ((ProgramPart s),s,4)) . (intpos (n + 7)) =
(Comput ((ProgramPart s),s,3)) . (DataLoc (n,3))
by A25, A29, A38, SCMPDS_2:59
.=
(s . (DataLoc ((s . SBP),2))) mod (s . (DataLoc ((s . SBP),3)))
by A32, Th5
;
n + 6 <> n + 7
;
then A42:
(Comput ((ProgramPart s),s,4)) . (intpos (n + 6)) = s . (DataLoc ((s . SBP),3))
by A25, A34, A38, AMI_3:52, SCMPDS_2:59;
Y:
(ProgramPart (Comput ((ProgramPart s),s,5))) /. (IC (Comput ((ProgramPart s),s,5))) = (Comput ((ProgramPart s),s,5)) . (IC (Comput ((ProgramPart s),s,5)))
by COMPOS_1:38;
A43: IC (Comput ((ProgramPart s),s,5)) =
succ (IC (Comput ((ProgramPart s),s,4)))
by A37, SCMPDS_2:59
.=
9 + 1
by A35
;
then A44: CurInstr ((ProgramPart (Comput ((ProgramPart s),s,5))),(Comput ((ProgramPart s),s,5))) =
s . 10
by Y, AMI_1:54
.=
AddTo (GBP,1,4)
by A1, Lm1
;
T:
ProgramPart s = ProgramPart (Comput ((ProgramPart s),s,5))
by AMI_1:123;
A45: Comput ((ProgramPart s),s,(5 + 1)) =
Following ((ProgramPart s),(Comput ((ProgramPart s),s,5)))
by EXTPRO_1:4
.=
Exec ((AddTo (GBP,1,4)),(Comput ((ProgramPart s),s,5)))
by A44, T
;
A46:
DataLoc (((Comput ((ProgramPart s),s,4)) . SBP),(4 + RetSP)) = intpos (n + (4 + 0))
by A39, Th5, SCMPDS_1:def 22;
then A47:
(Comput ((ProgramPart s),s,5)) . SBP = n
by A37, A39, Lm3, SCMPDS_2:59;
A48:
(Comput ((ProgramPart s),s,5)) . GBP = 0
by A37, A40, A46, Lm2, SCMPDS_2:59;
n + 7 <> n + 4
;
then A49:
(Comput ((ProgramPart s),s,5)) . (intpos (n + 7)) = (s . (DataLoc ((s . SBP),2))) mod (s . (DataLoc ((s . SBP),3)))
by A37, A41, A46, AMI_3:52, SCMPDS_2:59;
n + 6 <> n + 4
;
then A50:
(Comput ((ProgramPart s),s,5)) . (intpos (n + 6)) = s . (DataLoc ((s . SBP),3))
by A37, A42, A46, AMI_3:52, SCMPDS_2:59;
A51: (Comput ((ProgramPart s),s,5)) . (intpos (n + 4)) =
(Comput ((ProgramPart s),s,4)) . (DataLoc (0,1))
by A37, A40, A46, SCMPDS_2:59
.=
(Comput ((ProgramPart s),s,4)) . (intpos (0 + 1))
by Th5
.=
n
by A25, A29, A38, Lm3, SCMPDS_2:59
;
Y:
(ProgramPart (Comput ((ProgramPart s),s,6))) /. (IC (Comput ((ProgramPart s),s,6))) = (Comput ((ProgramPart s),s,6)) . (IC (Comput ((ProgramPart s),s,6)))
by COMPOS_1:38;
A52: IC (Comput ((ProgramPart s),s,6)) =
succ (IC (Comput ((ProgramPart s),s,5)))
by A45, SCMPDS_2:60
.=
10 + 1
by A43
;
then A53: CurInstr ((ProgramPart (Comput ((ProgramPart s),s,6))),(Comput ((ProgramPart s),s,6))) =
s . 11
by Y, AMI_1:54
.=
saveIC (SBP,RetIC)
by A1, Lm1
;
T:
ProgramPart s = ProgramPart (Comput ((ProgramPart s),s,6))
by AMI_1:123;
A54: Comput ((ProgramPart s),s,(6 + 1)) =
Following ((ProgramPart s),(Comput ((ProgramPart s),s,6)))
by EXTPRO_1:4
.=
Exec ((saveIC (SBP,RetIC)),(Comput ((ProgramPart s),s,6)))
by A53, T
;
A55:
DataLoc (((Comput ((ProgramPart s),s,5)) . GBP),1) = intpos (0 + 1)
by A48, Th5;
then A56:
(Comput ((ProgramPart s),s,6)) . SBP = n + 4
by A45, A47, SCMPDS_2:60;
A57:
(Comput ((ProgramPart s),s,6)) . GBP = 0
by A45, A48, A55, AMI_3:52, SCMPDS_2:60;
n + 7 <> 1
by NAT_1:11;
then A58:
(Comput ((ProgramPart s),s,6)) . (intpos (n + 7)) = (s . (DataLoc ((s . SBP),2))) mod (s . (DataLoc ((s . SBP),3)))
by A45, A49, A55, AMI_3:52, SCMPDS_2:60;
n + 6 <> 1
by NAT_1:11;
then A59:
(Comput ((ProgramPart s),s,6)) . (intpos (n + 6)) = s . (DataLoc ((s . SBP),3))
by A45, A50, A55, AMI_3:52, SCMPDS_2:60;
n + 4 <> 1
by NAT_1:11;
then A60:
(Comput ((ProgramPart s),s,6)) . (intpos (n + 4)) = n
by A45, A51, A55, AMI_3:52, SCMPDS_2:60;
Y:
(ProgramPart (Comput ((ProgramPart s),s,7))) /. (IC (Comput ((ProgramPart s),s,7))) = (Comput ((ProgramPart s),s,7)) . (IC (Comput ((ProgramPart s),s,7)))
by COMPOS_1:38;
thus IC (Comput ((ProgramPart s),s,7)) =
succ (IC (Comput ((ProgramPart s),s,6)))
by A54, SCMPDS_2:71
.=
11 + 1
by A52
.=
5 + 7
; ( Comput ((ProgramPart s),s,8) = Exec ((goto (- 7)),(Comput ((ProgramPart s),s,7))) & (Comput ((ProgramPart s),s,7)) . SBP = n + 4 & (Comput ((ProgramPart s),s,7)) . GBP = 0 & (Comput ((ProgramPart s),s,7)) . (intpos (n + 7)) = (s . (DataLoc ((s . SBP),2))) mod (s . (DataLoc ((s . SBP),3))) & (Comput ((ProgramPart s),s,7)) . (intpos (n + 6)) = s . (DataLoc ((s . SBP),3)) & (Comput ((ProgramPart s),s,7)) . (intpos (n + 4)) = n & (Comput ((ProgramPart s),s,7)) . (intpos (n + 5)) = 11 )
then A61: CurInstr ((ProgramPart (Comput ((ProgramPart s),s,7))),(Comput ((ProgramPart s),s,7))) =
s . 12
by Y, AMI_1:54
.=
goto (- 7)
by A1, Lm1
;
T:
ProgramPart s = ProgramPart (Comput ((ProgramPart s),s,7))
by AMI_1:123;
thus Comput ((ProgramPart s),s,8) =
Comput ((ProgramPart s),s,(7 + 1))
.=
Following ((ProgramPart s),(Comput ((ProgramPart s),s,7)))
by EXTPRO_1:4
.=
Exec ((goto (- 7)),(Comput ((ProgramPart s),s,7)))
by A61, T
; ( (Comput ((ProgramPart s),s,7)) . SBP = n + 4 & (Comput ((ProgramPart s),s,7)) . GBP = 0 & (Comput ((ProgramPart s),s,7)) . (intpos (n + 7)) = (s . (DataLoc ((s . SBP),2))) mod (s . (DataLoc ((s . SBP),3))) & (Comput ((ProgramPart s),s,7)) . (intpos (n + 6)) = s . (DataLoc ((s . SBP),3)) & (Comput ((ProgramPart s),s,7)) . (intpos (n + 4)) = n & (Comput ((ProgramPart s),s,7)) . (intpos (n + 5)) = 11 )
A62: DataLoc (((Comput ((ProgramPart s),s,6)) . SBP),RetIC) =
intpos ((n + 4) + 1)
by A56, Th5, SCMPDS_1:def 23
.=
intpos (n + (4 + 1))
;
then
SBP <> DataLoc (((Comput ((ProgramPart s),s,6)) . SBP),RetIC)
by Lm3;
hence
(Comput ((ProgramPart s),s,7)) . SBP = n + 4
by A54, A56, SCMPDS_2:71; ( (Comput ((ProgramPart s),s,7)) . GBP = 0 & (Comput ((ProgramPart s),s,7)) . (intpos (n + 7)) = (s . (DataLoc ((s . SBP),2))) mod (s . (DataLoc ((s . SBP),3))) & (Comput ((ProgramPart s),s,7)) . (intpos (n + 6)) = s . (DataLoc ((s . SBP),3)) & (Comput ((ProgramPart s),s,7)) . (intpos (n + 4)) = n & (Comput ((ProgramPart s),s,7)) . (intpos (n + 5)) = 11 )
GBP <> DataLoc (((Comput ((ProgramPart s),s,6)) . SBP),RetIC)
by A62, Lm2;
hence
(Comput ((ProgramPart s),s,7)) . GBP = 0
by A54, A57, SCMPDS_2:71; ( (Comput ((ProgramPart s),s,7)) . (intpos (n + 7)) = (s . (DataLoc ((s . SBP),2))) mod (s . (DataLoc ((s . SBP),3))) & (Comput ((ProgramPart s),s,7)) . (intpos (n + 6)) = s . (DataLoc ((s . SBP),3)) & (Comput ((ProgramPart s),s,7)) . (intpos (n + 4)) = n & (Comput ((ProgramPart s),s,7)) . (intpos (n + 5)) = 11 )
n + 7 <> n + 5
;
hence
(Comput ((ProgramPart s),s,7)) . (intpos (n + 7)) = (s . (DataLoc ((s . SBP),2))) mod (s . (DataLoc ((s . SBP),3)))
by A54, A58, A62, AMI_3:52, SCMPDS_2:71; ( (Comput ((ProgramPart s),s,7)) . (intpos (n + 6)) = s . (DataLoc ((s . SBP),3)) & (Comput ((ProgramPart s),s,7)) . (intpos (n + 4)) = n & (Comput ((ProgramPart s),s,7)) . (intpos (n + 5)) = 11 )
n + 6 <> n + 5
;
hence
(Comput ((ProgramPart s),s,7)) . (intpos (n + 6)) = s . (DataLoc ((s . SBP),3))
by A54, A59, A62, AMI_3:52, SCMPDS_2:71; ( (Comput ((ProgramPart s),s,7)) . (intpos (n + 4)) = n & (Comput ((ProgramPart s),s,7)) . (intpos (n + 5)) = 11 )
n + 4 <> n + 5
;
hence
(Comput ((ProgramPart s),s,7)) . (intpos (n + 4)) = n
by A54, A60, A62, AMI_3:52, SCMPDS_2:71; (Comput ((ProgramPart s),s,7)) . (intpos (n + 5)) = 11
thus
(Comput ((ProgramPart s),s,7)) . (intpos (n + 5)) = 11
by A52, A54, A62, SCMPDS_2:71; verum