let s be State of SCMPDS; :: thesis: ( Initialize 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 ((ProgramPart s),s)) . (intpos 9) = x gcd y )
set GA = GCD-Algorithm ;
assume A1: Initialize 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 ((ProgramPart s),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 ((ProgramPart s),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 ((ProgramPart s),s)) . (intpos 9) = x gcd y
set s4 = Comput ((ProgramPart s),s,4);
A6: GCD-Algorithm c= s by A1, COMPOS_1:132;
A7: GCD-Algorithm c= Comput ((ProgramPart s),s,4) by A1, AMI_1:81, COMPOS_1:132;
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:123;
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 EXTPRO_1:4
.= 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:123;
Th3x: for m being Element of NAT st m = (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)) holds
m = 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))) by ABSVALUE:46;
X: IC (Comput ((ProgramPart s),s,(4 + (n + 1)))) = (Comput ((ProgramPart s),(Comput ((ProgramPart s),s,4)),(n + 1))) . (IC SCMPDS) by EXTPRO_1:5
.= (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, T, SCMPDS_2:70
.= 2 + 2 by A10, A11, A19, A20, Th3x, SCMPDS_1:def 23 ;
(ProgramPart s) . (IC (Comput ((ProgramPart s),s,(4 + (n + 1))))) = s . (IC (Comput ((ProgramPart s),s,(4 + (n + 1))))) by COMPOS_1:2
.= halt SCMPDS by A6, Lm1, X ;
then Result ((ProgramPart s),s) = Comput ((ProgramPart s),s,(4 + (n + 1))) by EXTPRO_1:8
.= Comput ((ProgramPart (Comput ((ProgramPart s),s,4))),(Comput ((ProgramPart s),s,4)),(n + 1)) by T, EXTPRO_1:5 ;
hence (Result ((ProgramPart s),s)) . (intpos 9) = x gcd y by A13, A14, A15, A18, A21, AMI_3:52, SCMPDS_2:70; :: thesis: verum