let s be State of ; ( Initialized GCD-Algorithm c= s implies ( IC (Computation s,4) = inspos 5 & (Computation s,4) . GBP = 0 & (Computation s,4) . SBP = 7 & (Computation s,4) . (intpos (7 + RetIC )) = inspos 2 & (Computation s,4) . (intpos 9) = s . (intpos 9) & (Computation s,4) . (intpos 10) = s . (intpos 10) ) )
set GA = GCD-Algorithm ;
assume A1:
Initialized GCD-Algorithm c= s
; ( IC (Computation s,4) = inspos 5 & (Computation s,4) . GBP = 0 & (Computation s,4) . SBP = 7 & (Computation s,4) . (intpos (7 + RetIC )) = inspos 2 & (Computation s,4) . (intpos 9) = s . (intpos 9) & (Computation s,4) . (intpos 10) = s . (intpos 10) )
then A2:
GCD-Algorithm c= s
by SCMPDS_4:57;
A3:
IC s = inspos 0
by A1, SCMPDS_5:18;
A4: Computation s,(0 + 1) =
Following (Computation s,0 )
by AMI_1:14
.=
Following s
by AMI_1:13
.=
Exec (GBP := 0 ),s
by A2, A3, Lm1
;
then A5: IC (Computation s,1) =
Next (IC s)
by SCMPDS_2:57
.=
inspos (0 + 1)
by A3
;
then A6: CurInstr (Computation s,1) =
s . (inspos 1)
by AMI_1:54
.=
SBP := 7
by A2, Lm1
;
A7: Computation s,(1 + 1) =
Following (Computation s,1)
by AMI_1:14
.=
Exec (SBP := 7),(Computation s,1)
by A6
;
A8:
(Computation s,1) . GBP = 0
by A4, SCMPDS_2:57;
A9:
(Computation s,1) . (intpos 9) = s . (intpos 9)
by A4, AMI_3:52, SCMPDS_2:57;
A10:
(Computation s,1) . (intpos 10) = s . (intpos 10)
by A4, AMI_3:52, SCMPDS_2:57;
A11: IC (Computation s,2) =
Next (IC (Computation s,1))
by A7, SCMPDS_2:57
.=
inspos (1 + 1)
by A5
;
then A12: CurInstr (Computation s,2) =
s . (inspos 2)
by AMI_1:54
.=
saveIC SBP ,RetIC
by A2, Lm1
;
A13: Computation s,(2 + 1) =
Following (Computation s,2)
by AMI_1:14
.=
Exec (saveIC SBP ,RetIC ),(Computation s,2)
by A12
;
A14:
(Computation s,2) . GBP = 0
by A7, A8, AMI_3:52, SCMPDS_2:57;
A15:
(Computation s,2) . SBP = 7
by A7, SCMPDS_2:57;
A16:
(Computation s,2) . (intpos 9) = s . (intpos 9)
by A7, A9, AMI_3:52, SCMPDS_2:57;
A17:
(Computation s,2) . (intpos 10) = s . (intpos 10)
by A7, A10, AMI_3:52, SCMPDS_2:57;
A18: IC (Computation s,3) =
Next (IC (Computation s,2))
by A13, SCMPDS_2:71
.=
inspos (2 + 1)
by A11
;
then A19: CurInstr (Computation s,3) =
s . (inspos 3)
by AMI_1:54
.=
goto 2
by A2, Lm1
;
A20: Computation s,(3 + 1) =
Following (Computation s,3)
by AMI_1:14
.=
Exec (goto 2),(Computation s,3)
by A19
;
A21:
DataLoc ((Computation s,2) . SBP ),RetIC = intpos (7 + 1)
by A15, Th5, SCMPDS_1:def 23;
then A22:
(Computation s,3) . GBP = 0
by A13, A14, AMI_3:52, SCMPDS_2:71;
A23:
(Computation s,3) . SBP = 7
by A13, A15, A21, AMI_3:52, SCMPDS_2:71;
A24:
(Computation s,3) . (intpos 8) = inspos 2
by A11, A13, A21, SCMPDS_2:71;
A25:
(Computation s,3) . (intpos 9) = s . (intpos 9)
by A13, A16, A21, AMI_3:52, SCMPDS_2:71;
A26:
(Computation s,3) . (intpos 10) = s . (intpos 10)
by A13, A17, A21, AMI_3:52, SCMPDS_2:71;
thus IC (Computation s,4) =
ICplusConst (Computation s,3),2
by A20, SCMPDS_2:66
.=
inspos (3 + 2)
by A18, SCMPDS_6:23
.=
inspos 5
; ( (Computation s,4) . GBP = 0 & (Computation s,4) . SBP = 7 & (Computation s,4) . (intpos (7 + RetIC )) = inspos 2 & (Computation s,4) . (intpos 9) = s . (intpos 9) & (Computation s,4) . (intpos 10) = s . (intpos 10) )
thus
(Computation s,4) . GBP = 0
by A20, A22, SCMPDS_2:66; ( (Computation s,4) . SBP = 7 & (Computation s,4) . (intpos (7 + RetIC )) = inspos 2 & (Computation s,4) . (intpos 9) = s . (intpos 9) & (Computation s,4) . (intpos 10) = s . (intpos 10) )
thus
(Computation s,4) . SBP = 7
by A20, A23, SCMPDS_2:66; ( (Computation s,4) . (intpos (7 + RetIC )) = inspos 2 & (Computation s,4) . (intpos 9) = s . (intpos 9) & (Computation s,4) . (intpos 10) = s . (intpos 10) )
thus
(Computation s,4) . (intpos (7 + RetIC )) = inspos 2
by A20, A24, SCMPDS_1:def 23, SCMPDS_2:66; ( (Computation s,4) . (intpos 9) = s . (intpos 9) & (Computation s,4) . (intpos 10) = s . (intpos 10) )
thus
(Computation s,4) . (intpos 9) = s . (intpos 9)
by A20, A25, SCMPDS_2:66; (Computation s,4) . (intpos 10) = s . (intpos 10)
thus
(Computation s,4) . (intpos 10) = s . (intpos 10)
by A20, A26, SCMPDS_2:66; verum