let s be State of SCMPDS ; :: thesis: ( 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 ; :: thesis: ( 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 SCMPDS_4:57;
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 AMI_1:14
.= Following (ProgramPart s),s by AMI_1:13
.= 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 AMI_1:14
.= 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 AMI_1:14
.= 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 AMI_1:14
.= 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 ; :: thesis: ( (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; :: thesis: ( (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; :: thesis: ( (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; :: thesis: ( (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; :: thesis: (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; :: thesis: verum