let s be State of SCMPDS ; :: thesis: ( Initialized GCD-Algorithm c= s implies for x, y being Integer st s . (intpos 9) = x & s . (intpos 10) = y & x >= 0 & y >= 0 holds
(Result s) . (intpos 9) = x gcd y )
set GA = GCD-Algorithm ;
assume A1: Initialized GCD-Algorithm c= s ; :: thesis: for x, y being Integer st s . (intpos 9) = x & s . (intpos 10) = y & x >= 0 & y >= 0 holds
(Result s) . (intpos 9) = x gcd y
let x, y be Integer; :: thesis: ( s . (intpos 9) = x & s . (intpos 10) = y & x >= 0 & y >= 0 implies (Result s) . (intpos 9) = x gcd y )
assume that
A2: s . (intpos 9) = x and
A3: s . (intpos 10) = y and
A4: x >= 0 and
A5: y >= 0 ; :: thesis: (Result s) . (intpos 9) = x gcd y
set s4 = Comput (ProgramPart s),s,4;
A6: GCD-Algorithm c= s by A1, SCMPDS_4:57;
A7: GCD-Algorithm c= Comput (ProgramPart s),s,4 by A1, AMI_1:81, SCMPDS_4:57;
A8: IC (Comput (ProgramPart s),s,4) = 5 by A1, Th15;
A9: (Comput (ProgramPart s),s,4) . GBP = 0 by A1, Th15;
A10: (Comput (ProgramPart s),s,4) . SBP = 7 by A1, Th15;
A11: (Comput (ProgramPart s),s,4) . (intpos (7 + RetIC )) = 2 by A1, Th15;
A12: (Comput (ProgramPart s),s,4) . (intpos 9) = s . (intpos 9) by A1, Th15;
A13: (Comput (ProgramPart s),s,4) . (DataLoc ((Comput (ProgramPart s),s,4) . SBP ),3) = (Comput (ProgramPart s),s,4) . (intpos (7 + 3)) by A10, Th5
.= y by A1, A3, Th15 ;
A14: DataLoc ((Comput (ProgramPart s),s,4) . SBP ),2 = intpos (7 + 2) by A10, Th5;
then A15: (Comput (ProgramPart s),s,4) . (DataLoc ((Comput (ProgramPart s),s,4) . SBP ),2) = x by A1, A2, Th15;
consider n being Element of NAT such that
A16: CurInstr (ProgramPart (Comput (ProgramPart (Comput (ProgramPart s),s,4)),(Comput (ProgramPart s),s,4),n)),(Comput (ProgramPart (Comput (ProgramPart s),s,4)),(Comput (ProgramPart s),s,4),n) = return SBP and
A17: (Comput (ProgramPart s),s,4) . SBP = (Comput (ProgramPart (Comput (ProgramPart s),s,4)),(Comput (ProgramPart s),s,4),n) . SBP and
A18: (Comput (ProgramPart (Comput (ProgramPart s),s,4)),(Comput (ProgramPart s),s,4),n) . (DataLoc ((Comput (ProgramPart s),s,4) . SBP ),2) = ((Comput (ProgramPart s),s,4) . (DataLoc ((Comput (ProgramPart s),s,4) . SBP ),2)) gcd ((Comput (ProgramPart s),s,4) . (DataLoc ((Comput (ProgramPart s),s,4) . SBP ),3)) and
A19: for j being Element of NAT st 1 < j & j <= ((Comput (ProgramPart s),s,4) . SBP ) + 1 holds
(Comput (ProgramPart s),s,4) . (intpos j) = (Comput (ProgramPart (Comput (ProgramPart s),s,4)),(Comput (ProgramPart s),s,4),n) . (intpos j) by A2, A4, A5, A7, A8, A9, A10, A12, A13, A14, Th17;
A20: DataLoc ((Comput (ProgramPart (Comput (ProgramPart s),s,4)),(Comput (ProgramPart s),s,4),n) . SBP ),RetIC = intpos (7 + 1) by A10, A17, Th5, SCMPDS_1:def 23;
T: ProgramPart (Comput (ProgramPart s),s,4) = ProgramPart (Comput (ProgramPart (Comput (ProgramPart s),s,4)),(Comput (ProgramPart s),s,4),n) by AMI_1:144;
A21: Comput (ProgramPart (Comput (ProgramPart s),s,4)),(Comput (ProgramPart s),s,4),(n + 1) = Following (ProgramPart (Comput (ProgramPart s),s,4)),(Comput (ProgramPart (Comput (ProgramPart s),s,4)),(Comput (ProgramPart s),s,4),n) by AMI_1:14
.= Exec (return SBP ),(Comput (ProgramPart (Comput (ProgramPart s),s,4)),(Comput (ProgramPart s),s,4),n) by A16, T ;
T: ProgramPart s = ProgramPart (Comput (ProgramPart s),s,4) by AMI_1:144;
IC (Comput (ProgramPart s),s,(4 + (n + 1))) = (Comput (ProgramPart s),(Comput (ProgramPart s),s,4),(n + 1)) . (IC SCMPDS ) by AMI_1:51
.= (abs ((Comput (ProgramPart (Comput (ProgramPart s),s,4)),(Comput (ProgramPart s),s,4),n) . (DataLoc ((Comput (ProgramPart (Comput (ProgramPart s),s,4)),(Comput (ProgramPart s),s,4),n) . SBP ),RetIC ))) + 2 by A21, SCMPDS_2:70, T
.= 2 + 2 by A10, A11, A19, A20, Th3, SCMPDS_1:def 23 ;
then s . (IC (Comput (ProgramPart s),s,(4 + (n + 1)))) = halt SCMPDS by A6, Lm1;
then Result s = Comput (ProgramPart s),s,(4 + (n + 1)) by AMI_1:56
.= Comput (ProgramPart (Comput (ProgramPart s),s,4)),(Comput (ProgramPart s),s,4),(n + 1) by AMI_1:51, T ;
hence (Result s) . (intpos 9) = x gcd y by A13, A14, A15, A18, A21, AMI_3:52, SCMPDS_2:70; :: thesis: verum