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 A1: 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
A2: s . (intpos 9) = x and
A3: s . (intpos 10) = y and
A4: x >= 0 and
A5: y >= 0 ; :: thesis: (Result (P,s)) . (intpos 9) = x gcd y
set s4 = Comput (P,s,4);
A6: IC (Comput (P,s,4)) = 5 by Th11, A1;
A7: (Comput (P,s,4)) . GBP = 0 by Th11, A1;
A8: (Comput (P,s,4)) . SBP = 7 by Th11, A1;
A9: (Comput (P,s,4)) . (intpos (7 + RetIC)) = 2 by Th11, A1;
A10: (Comput (P,s,4)) . (intpos 9) = s . (intpos 9) by Th11, A1;
A11: (Comput (P,s,4)) . (DataLoc (((Comput (P,s,4)) . SBP),3)) = (Comput (P,s,4)) . (intpos (7 + 3)) by A8, Th1
.= y by A3, Th11, A1 ;
A12: DataLoc (((Comput (P,s,4)) . SBP),2) = intpos (7 + 2) by A8, Th1;
then A13: (Comput (P,s,4)) . (DataLoc (((Comput (P,s,4)) . SBP),2)) = x by A2, Th11, A1;
consider n being Nat such that
A14: CurInstr (P,(Comput (P,(Comput (P,s,4)),n))) = return SBP and
A15: (Comput (P,s,4)) . SBP = (Comput (P,(Comput (P,s,4)),n)) . SBP and
A16: (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
A17: for j being 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 A2, A4, A5, A6, A7, A8, A10, A11, A12, Th13, A1;
A18: DataLoc (((Comput (P,(Comput (P,s,4)),n)) . SBP),RetIC) = intpos (7 + 1) by A8, A15, Th1, SCMPDS_I:def 14;
A19: 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 A14 ;
A20: for m being Nat st m = (Comput (P,(Comput (P,s,4)),n)) . (DataLoc (((Comput (P,(Comput (P,s,4)),n)) . SBP),RetIC)) holds
m = |.((Comput (P,(Comput (P,s,4)),n)) . (DataLoc (((Comput (P,(Comput (P,s,4)),n)) . SBP),RetIC))).| by ABSVALUE:29;
A21: IC (Comput (P,s,(4 + (n + 1)))) = (Comput (P,(Comput (P,s,4)),(n + 1))) . (IC ) by EXTPRO_1:4
.= |.((Comput (P,(Comput (P,s,4)),n)) . (DataLoc (((Comput (P,(Comput (P,s,4)),n)) . SBP),RetIC))).| + 2 by A19, SCMPDS_2:58
.= 2 + 2 by A8, A9, A17, A18, A20, SCMPDS_I:def 14 ;
P . (IC (Comput (P,s,(4 + (n + 1))))) = P . (IC (Comput (P,s,(4 + (n + 1)))))
.= halt SCMPDS by Lm1, A21, A1 ;
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 A11, A12, A13, A16, A19, AMI_3:10, SCMPDS_2:58; :: thesis: verum