let s be State of SCMPDS; ( Initialize GCD-Algorithm c= s implies ( IC (Comput ((ProgramPart s),s,4)) = 5 & (Comput ((ProgramPart s),s,4)) . GBP = 0 & (Comput ((ProgramPart s),s,4)) . SBP = 7 & (Comput ((ProgramPart s),s,4)) . (intpos (7 + RetIC)) = 2 & (Comput ((ProgramPart s),s,4)) . (intpos 9) = s . (intpos 9) & (Comput ((ProgramPart s),s,4)) . (intpos 10) = s . (intpos 10) ) )
set GA = GCD-Algorithm ;
assume A1:
Initialize GCD-Algorithm c= s
; ( IC (Comput ((ProgramPart s),s,4)) = 5 & (Comput ((ProgramPart s),s,4)) . GBP = 0 & (Comput ((ProgramPart s),s,4)) . SBP = 7 & (Comput ((ProgramPart s),s,4)) . (intpos (7 + RetIC)) = 2 & (Comput ((ProgramPart s),s,4)) . (intpos 9) = s . (intpos 9) & (Comput ((ProgramPart s),s,4)) . (intpos 10) = s . (intpos 10) )
then A2:
GCD-Algorithm c= s
by COMPOS_1:132;
A3:
IC s = 0
by A1, SCMPDS_5:18;
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;
A4: Comput ((ProgramPart s),s,(0 + 1)) =
Following ((ProgramPart s),(Comput ((ProgramPart s),s,0)))
by EXTPRO_1:4
.=
Following ((ProgramPart s),s)
by EXTPRO_1:3
.=
Exec ((GBP := 0),s)
by A2, A3, Lm1, Y
;
then A5: IC (Comput ((ProgramPart s),s,1)) =
succ (IC s)
by SCMPDS_2:57
.=
0 + 1
by A3
;
then A6: CurInstr ((ProgramPart (Comput ((ProgramPart s),s,1))),(Comput ((ProgramPart s),s,1))) =
s . 1
by Z, AMI_1:54
.=
SBP := 7
by A2, Lm1
;
T:
ProgramPart s = ProgramPart (Comput ((ProgramPart s),s,1))
by AMI_1:123;
A7: Comput ((ProgramPart s),s,(1 + 1)) =
Following ((ProgramPart s),(Comput ((ProgramPart s),s,1)))
by EXTPRO_1:4
.=
Exec ((SBP := 7),(Comput ((ProgramPart s),s,1)))
by A6, T
;
A8:
(Comput ((ProgramPart s),s,1)) . GBP = 0
by A4, SCMPDS_2:57;
A9:
(Comput ((ProgramPart s),s,1)) . (intpos 9) = s . (intpos 9)
by A4, AMI_3:52, SCMPDS_2:57;
A10:
(Comput ((ProgramPart s),s,1)) . (intpos 10) = s . (intpos 10)
by A4, AMI_3:52, SCMPDS_2:57;
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;
A11: IC (Comput ((ProgramPart s),s,2)) =
succ (IC (Comput ((ProgramPart s),s,1)))
by A7, SCMPDS_2:57
.=
1 + 1
by A5
;
then A12: CurInstr ((ProgramPart (Comput ((ProgramPart s),s,2))),(Comput ((ProgramPart s),s,2))) =
s . 2
by Y, AMI_1:54
.=
saveIC (SBP,RetIC)
by A2, Lm1
;
T:
ProgramPart s = ProgramPart (Comput ((ProgramPart s),s,2))
by AMI_1:123;
A13: Comput ((ProgramPart s),s,(2 + 1)) =
Following ((ProgramPart s),(Comput ((ProgramPart s),s,2)))
by EXTPRO_1:4
.=
Exec ((saveIC (SBP,RetIC)),(Comput ((ProgramPart s),s,2)))
by A12, T
;
A14:
(Comput ((ProgramPart s),s,2)) . GBP = 0
by A7, A8, AMI_3:52, SCMPDS_2:57;
A15:
(Comput ((ProgramPart s),s,2)) . SBP = 7
by A7, SCMPDS_2:57;
A16:
(Comput ((ProgramPart s),s,2)) . (intpos 9) = s . (intpos 9)
by A7, A9, AMI_3:52, SCMPDS_2:57;
A17:
(Comput ((ProgramPart s),s,2)) . (intpos 10) = s . (intpos 10)
by A7, A10, AMI_3:52, SCMPDS_2:57;
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;
A18: IC (Comput ((ProgramPart s),s,3)) =
succ (IC (Comput ((ProgramPart s),s,2)))
by A13, SCMPDS_2:71
.=
2 + 1
by A11
;
then A19: CurInstr ((ProgramPart (Comput ((ProgramPart s),s,3))),(Comput ((ProgramPart s),s,3))) =
s . 3
by Y, AMI_1:54
.=
goto 2
by A2, Lm1
;
T:
ProgramPart s = ProgramPart (Comput ((ProgramPart s),s,3))
by AMI_1:123;
A20: Comput ((ProgramPart s),s,(3 + 1)) =
Following ((ProgramPart s),(Comput ((ProgramPart s),s,3)))
by EXTPRO_1:4
.=
Exec ((goto 2),(Comput ((ProgramPart s),s,3)))
by A19, T
;
A21:
DataLoc (((Comput ((ProgramPart s),s,2)) . SBP),RetIC) = intpos (7 + 1)
by A15, Th5, SCMPDS_1:def 23;
then A22:
(Comput ((ProgramPart s),s,3)) . GBP = 0
by A13, A14, AMI_3:52, SCMPDS_2:71;
A23:
(Comput ((ProgramPart s),s,3)) . SBP = 7
by A13, A15, A21, AMI_3:52, SCMPDS_2:71;
A24:
(Comput ((ProgramPart s),s,3)) . (intpos 8) = 2
by A11, A13, A21, SCMPDS_2:71;
A25:
(Comput ((ProgramPart s),s,3)) . (intpos 9) = s . (intpos 9)
by A13, A16, A21, AMI_3:52, SCMPDS_2:71;
A26:
(Comput ((ProgramPart s),s,3)) . (intpos 10) = s . (intpos 10)
by A13, A17, A21, AMI_3:52, SCMPDS_2:71;
thus IC (Comput ((ProgramPart s),s,4)) =
ICplusConst ((Comput ((ProgramPart s),s,3)),2)
by A20, SCMPDS_2:66
.=
3 + 2
by A18, SCMPDS_6:23
.=
5
; ( (Comput ((ProgramPart s),s,4)) . GBP = 0 & (Comput ((ProgramPart s),s,4)) . SBP = 7 & (Comput ((ProgramPart s),s,4)) . (intpos (7 + RetIC)) = 2 & (Comput ((ProgramPart s),s,4)) . (intpos 9) = s . (intpos 9) & (Comput ((ProgramPart s),s,4)) . (intpos 10) = s . (intpos 10) )
thus
(Comput ((ProgramPart s),s,4)) . GBP = 0
by A20, A22, SCMPDS_2:66; ( (Comput ((ProgramPart s),s,4)) . SBP = 7 & (Comput ((ProgramPart s),s,4)) . (intpos (7 + RetIC)) = 2 & (Comput ((ProgramPart s),s,4)) . (intpos 9) = s . (intpos 9) & (Comput ((ProgramPart s),s,4)) . (intpos 10) = s . (intpos 10) )
thus
(Comput ((ProgramPart s),s,4)) . SBP = 7
by A20, A23, SCMPDS_2:66; ( (Comput ((ProgramPart s),s,4)) . (intpos (7 + RetIC)) = 2 & (Comput ((ProgramPart s),s,4)) . (intpos 9) = s . (intpos 9) & (Comput ((ProgramPart s),s,4)) . (intpos 10) = s . (intpos 10) )
thus
(Comput ((ProgramPart s),s,4)) . (intpos (7 + RetIC)) = 2
by A20, A24, SCMPDS_1:def 23, SCMPDS_2:66; ( (Comput ((ProgramPart s),s,4)) . (intpos 9) = s . (intpos 9) & (Comput ((ProgramPart s),s,4)) . (intpos 10) = s . (intpos 10) )
thus
(Comput ((ProgramPart s),s,4)) . (intpos 9) = s . (intpos 9)
by A20, A25, SCMPDS_2:66; (Comput ((ProgramPart s),s,4)) . (intpos 10) = s . (intpos 10)
thus
(Comput ((ProgramPart s),s,4)) . (intpos 10) = s . (intpos 10)
by A20, A26, SCMPDS_2:66; verum