let P be Instruction-Sequence of SCMPDS; :: thesis: for s being 0 -started State of SCMPDS st GCD-Algorithm c= P holds
for x, y being Integer st s . (intpos 9) = x & s . (intpos 10) = y & x >= 0 & y >= 0 holds
(Result (P,s)) . (intpos 9) = x gcd y
let s be 0 -started State of SCMPDS; :: thesis: ( GCD-Algorithm c= P implies for x, y being Integer st s . (intpos 9) = x & s . (intpos 10) = y & x >= 0 & y >= 0 holds
(Result (P,s)) . (intpos 9) = x gcd y )
set GA = GCD-Algorithm ;
assume A2: GCD-Algorithm c= P ; :: thesis: for x, y being Integer st s . (intpos 9) = x & s . (intpos 10) = y & x >= 0 & y >= 0 holds
(Result (P,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 (P,s)) . (intpos 9) = x gcd y )
assume that
A3: s . (intpos 9) = x and
A4: s . (intpos 10) = y and
A5: x >= 0 and
A6: y >= 0 ; :: thesis: (Result (P,s)) . (intpos 9) = x gcd y
set s4 = Comput (P,s,4);
A9: IC (Comput (P,s,4)) = 5 by Th15, A2;
A10: (Comput (P,s,4)) . GBP = 0 by Th15, A2;
A11: (Comput (P,s,4)) . SBP = 7 by Th15, A2;
A12: (Comput (P,s,4)) . (intpos (7 + RetIC)) = 2 by Th15, A2;
A13: (Comput (P,s,4)) . (intpos 9) = s . (intpos 9) by Th15, A2;
A14: (Comput (P,s,4)) . (DataLoc (((Comput (P,s,4)) . SBP),3)) = (Comput (P,s,4)) . (intpos (7 + 3)) by A11, Th5
.= y by A4, Th15, A2 ;
A15: DataLoc (((Comput (P,s,4)) . SBP),2) = intpos (7 + 2) by A11, Th5;
then A16: (Comput (P,s,4)) . (DataLoc (((Comput (P,s,4)) . SBP),2)) = x by A3, Th15, A2;
consider n being Element of NAT such that
A17: CurInstr (P,(Comput (P,(Comput (P,s,4)),n))) = return SBP and
A18: (Comput (P,s,4)) . SBP = (Comput (P,(Comput (P,s,4)),n)) . SBP and
A19: (Comput (P,(Comput (P,s,4)),n)) . (DataLoc (((Comput (P,s,4)) . SBP),2)) = ((Comput (P,s,4)) . (DataLoc (((Comput (P,s,4)) . SBP),2))) gcd ((Comput (P,s,4)) . (DataLoc (((Comput (P,s,4)) . SBP),3))) and
A20: for j being Element of NAT st 1 < j & j <= ((Comput (P,s,4)) . SBP) + 1 holds
(Comput (P,s,4)) . (intpos j) = (Comput (P,(Comput (P,s,4)),n)) . (intpos j) by A3, A5, A6, A9, A10, A11, A13, A14, A15, Th17, A2;
A21: DataLoc (((Comput (P,(Comput (P,s,4)),n)) . SBP),RetIC) = intpos (7 + 1) by A11, A18, Th5, SCMPDS_1:def 21;
A23: Comput (P,(Comput (P,s,4)),(n + 1)) = Following (P,(Comput (P,(Comput (P,s,4)),n))) by EXTPRO_1:3
.= Exec ((return SBP),(Comput (P,(Comput (P,s,4)),n))) by A17 ;
A25: for m being Element of NAT st m = (Comput (P,(Comput (P,s,4)),n)) . (DataLoc (((Comput (P,(Comput (P,s,4)),n)) . SBP),RetIC)) holds
m = abs ((Comput (P,(Comput (P,s,4)),n)) . (DataLoc (((Comput (P,(Comput (P,s,4)),n)) . SBP),RetIC))) by ABSVALUE:29;
A26: IC (Comput (P,s,(4 + (n + 1)))) = (Comput (P,(Comput (P,s,4)),(n + 1))) . (IC ) by EXTPRO_1:4
.= (abs ((Comput (P,(Comput (P,s,4)),n)) . (DataLoc (((Comput (P,(Comput (P,s,4)),n)) . SBP),RetIC)))) + 2 by A23, SCMPDS_2:58
.= 2 + 2 by A11, A12, A20, A21, A25, SCMPDS_1:def 21 ;
P . (IC (Comput (P,s,(4 + (n + 1))))) = P . (IC (Comput (P,s,(4 + (n + 1)))))
.= halt SCMPDS by Lm1, A26, A2 ;
then Result (P,s) = Comput (P,s,(4 + (n + 1))) by EXTPRO_1:7
.= Comput (P,(Comput (P,s,4)),(n + 1)) by EXTPRO_1:4 ;
hence (Result (P,s)) . (intpos 9) = x gcd y by A14, A15, A16, A19, A23, AMI_3:10, SCMPDS_2:58; :: thesis: verum