let n, m 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 & 1 < m & m <= n + 1 holds
(Comput ((ProgramPart s),s,7)) . (intpos m) = s . (intpos m)
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 & 1 < m & m <= n + 1 implies (Comput ((ProgramPart s),s,7)) . (intpos m) = s . (intpos m) )
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 not 1 < m or not m <= n + 1 or (Comput ((ProgramPart s),s,7)) . (intpos m) = s . (intpos m) )
assume A2:
IC s = 5
; ( not n = s . SBP or not s . GBP = 0 or not s . (DataLoc ((s . SBP),3)) > 0 or not 1 < m or not m <= n + 1 or (Comput ((ProgramPart s),s,7)) . (intpos m) = s . (intpos m) )
assume A3:
n = s . SBP
; ( not s . GBP = 0 or not s . (DataLoc ((s . SBP),3)) > 0 or not 1 < m or not m <= n + 1 or (Comput ((ProgramPart s),s,7)) . (intpos m) = s . (intpos m) )
assume A4:
s . GBP = 0
; ( not s . (DataLoc ((s . SBP),3)) > 0 or not 1 < m or not m <= n + 1 or (Comput ((ProgramPart s),s,7)) . (intpos m) = s . (intpos m) )
assume A5:
s . (DataLoc ((s . SBP),3)) > 0
; ( not 1 < m or not m <= n + 1 or (Comput ((ProgramPart s),s,7)) . (intpos m) = s . (intpos m) )
assume A6:
1 < m
; ( not m <= n + 1 or (Comput ((ProgramPart s),s,7)) . (intpos m) = s . (intpos m) )
assume A7:
m <= n + 1
; (Comput ((ProgramPart s),s,7)) . (intpos m) = s . (intpos m)
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;
A8: 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 A9: IC (Comput ((ProgramPart s),s,1)) =
succ (IC s)
by A5, SCMPDS_2:68
.=
5 + 1
by A2
;
then A10: 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;
A11: 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 A10, T
;
A12:
(Comput ((ProgramPart s),s,1)) . SBP = n
by A3, A8, SCMPDS_2:68;
A13:
(Comput ((ProgramPart s),s,1)) . GBP = 0
by A4, A8, SCMPDS_2:68;
A14:
(Comput ((ProgramPart s),s,1)) . (intpos m) = s . (intpos m)
by A8, 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;
A15: IC (Comput ((ProgramPart s),s,2)) =
succ (IC (Comput ((ProgramPart s),s,1)))
by A11, SCMPDS_2:59
.=
6 + 1
by A9
;
then A16: 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;
A17: 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 A16, T
;
A18:
DataLoc (((Comput ((ProgramPart s),s,1)) . SBP),6) = intpos (n + 6)
by A12, Th5;
then A19:
(Comput ((ProgramPart s),s,2)) . SBP = n
by A11, A12, Lm3, SCMPDS_2:59;
A20:
(Comput ((ProgramPart s),s,2)) . GBP = 0
by A11, A13, A18, Lm2, SCMPDS_2:59;
n + 1 < n + 6
by XREAL_1:8;
then A21:
(Comput ((ProgramPart s),s,2)) . (intpos m) = s . (intpos m)
by A7, A11, A14, A18, 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;
A22: IC (Comput ((ProgramPart s),s,3)) =
succ (IC (Comput ((ProgramPart s),s,2)))
by A17, SCMPDS_2:64
.=
7 + 1
by A15
;
then A23: 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;
A24: 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 A23, T
;
A25:
DataLoc (((Comput ((ProgramPart s),s,2)) . SBP),2) = intpos (n + 2)
by A19, Th5;
then A26:
SBP <> DataLoc (((Comput ((ProgramPart s),s,2)) . SBP),2)
by Lm3;
A27:
DataLoc (((Comput ((ProgramPart s),s,2)) . SBP),3) = intpos (n + 3)
by A19, Th5;
then
SBP <> DataLoc (((Comput ((ProgramPart s),s,2)) . SBP),3)
by Lm3;
then A28:
(Comput ((ProgramPart s),s,3)) . SBP = n
by A17, A19, A26, SCMPDS_2:64;
A29:
GBP <> DataLoc (((Comput ((ProgramPart s),s,2)) . SBP),2)
by A25, Lm2;
GBP <> DataLoc (((Comput ((ProgramPart s),s,2)) . SBP),3)
by A27, Lm2;
then A30:
(Comput ((ProgramPart s),s,3)) . GBP = 0
by A17, A20, A29, SCMPDS_2:64;
n + 1 < n + 2
by XREAL_1:8;
then A31:
intpos m <> DataLoc (((Comput ((ProgramPart s),s,2)) . SBP),2)
by A7, A25, AMI_3:52;
n + 1 < n + 3
by XREAL_1:8;
then
intpos m <> DataLoc (((Comput ((ProgramPart s),s,2)) . SBP),3)
by A7, A27, AMI_3:52;
then A32:
(Comput ((ProgramPart s),s,3)) . (intpos m) = s . (intpos m)
by A17, A21, A31, 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;
A33: IC (Comput ((ProgramPart s),s,4)) =
succ (IC (Comput ((ProgramPart s),s,3)))
by A24, SCMPDS_2:59
.=
8 + 1
by A22
;
then A34: 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;
A35: 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 A34, T
;
A36:
DataLoc (((Comput ((ProgramPart s),s,3)) . SBP),7) = intpos (n + 7)
by A28, Th5;
then A37:
(Comput ((ProgramPart s),s,4)) . SBP = n
by A24, A28, Lm3, SCMPDS_2:59;
A38:
(Comput ((ProgramPart s),s,4)) . GBP = 0
by A24, A30, A36, Lm2, SCMPDS_2:59;
n + 1 < n + 7
by XREAL_1:8;
then A39:
(Comput ((ProgramPart s),s,4)) . (intpos m) = s . (intpos m)
by A7, A24, A32, A36, 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;
A40: IC (Comput ((ProgramPart s),s,5)) =
succ (IC (Comput ((ProgramPart s),s,4)))
by A35, SCMPDS_2:59
.=
9 + 1
by A33
;
then A41: 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;
A42: 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 A41, T
;
A43:
DataLoc (((Comput ((ProgramPart s),s,4)) . SBP),(4 + RetSP)) = intpos (n + (4 + 0))
by A37, Th5, SCMPDS_1:def 22;
then A44:
(Comput ((ProgramPart s),s,5)) . SBP = n
by A35, A37, Lm3, SCMPDS_2:59;
A45:
(Comput ((ProgramPart s),s,5)) . GBP = 0
by A35, A38, A43, Lm2, SCMPDS_2:59;
n + 1 < n + 4
by XREAL_1:8;
then A46:
(Comput ((ProgramPart s),s,5)) . (intpos m) = s . (intpos m)
by A7, A35, A39, A43, AMI_3:52, 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;
IC (Comput ((ProgramPart s),s,6)) =
succ (IC (Comput ((ProgramPart s),s,5)))
by A42, SCMPDS_2:60
.=
10 + 1
by A40
;
then A47: 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;
A48: 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 A47, T
;
A49:
DataLoc (((Comput ((ProgramPart s),s,5)) . GBP),1) = intpos (0 + 1)
by A45, Th5;
then A50:
(Comput ((ProgramPart s),s,6)) . SBP = n + 4
by A42, A44, SCMPDS_2:60;
A51:
(Comput ((ProgramPart s),s,6)) . (intpos m) = s . (intpos m)
by A6, A42, A46, A49, AMI_3:52, SCMPDS_2:60;
A52: DataLoc (((Comput ((ProgramPart s),s,6)) . SBP),RetIC) =
intpos ((n + 4) + 1)
by A50, Th5, SCMPDS_1:def 23
.=
intpos (n + (4 + 1))
;
n + 1 < n + 5
by XREAL_1:8;
hence
(Comput ((ProgramPart s),s,7)) . (intpos m) = s . (intpos m)
by A7, A48, A51, A52, AMI_3:52, SCMPDS_2:71; verum