let P be Instruction-Sequence of SCMPDS; :: thesis: ( GCD-Algorithm c= P implies for s being 0 -started State of SCMPDS holds
( IC (Comput (P,s,4)) = 5 & (Comput (P,s,4)) . GBP = 0 & (Comput (P,s,4)) . SBP = 7 & (Comput (P,s,4)) . (intpos (7 + RetIC)) = 2 & (Comput (P,s,4)) . (intpos 9) = s . (intpos 9) & (Comput (P,s,4)) . (intpos 10) = s . (intpos 10) ) )
assume A1: GCD-Algorithm c= P ; :: thesis: for s being 0 -started State of SCMPDS holds
( IC (Comput (P,s,4)) = 5 & (Comput (P,s,4)) . GBP = 0 & (Comput (P,s,4)) . SBP = 7 & (Comput (P,s,4)) . (intpos (7 + RetIC)) = 2 & (Comput (P,s,4)) . (intpos 9) = s . (intpos 9) & (Comput (P,s,4)) . (intpos 10) = s . (intpos 10) )
let s be 0 -started State of SCMPDS; :: thesis: ( IC (Comput (P,s,4)) = 5 & (Comput (P,s,4)) . GBP = 0 & (Comput (P,s,4)) . SBP = 7 & (Comput (P,s,4)) . (intpos (7 + RetIC)) = 2 & (Comput (P,s,4)) . (intpos 9) = s . (intpos 9) & (Comput (P,s,4)) . (intpos 10) = s . (intpos 10) )
set GA = GCD-Algorithm ;
A2: IC s = 0 by MEMSTR_0:def 12;
A3: P /. (IC s) = P . (IC s) by PBOOLE:143;
A4: P /. (IC (Comput (P,s,1))) = P . (IC (Comput (P,s,1))) by PBOOLE:143;
A5: Comput (P,s,(0 + 1)) = Following (P,(Comput (P,s,0))) by EXTPRO_1:3
.= Following (P,s) by EXTPRO_1:2
.= Exec ((GBP := 0),s) by A2, Lm1, A3, A1 ;
then A6: IC (Comput (P,s,1)) = (IC s) + 1 by SCMPDS_2:45
.= 0 + 1 by A2 ;
then A7: CurInstr (P,(Comput (P,s,1))) = P . 1 by A4
.= SBP := 7 by Lm1, A1 ;
A8: Comput (P,s,(1 + 1)) = Following (P,(Comput (P,s,1))) by EXTPRO_1:3
.= Exec ((SBP := 7),(Comput (P,s,1))) by A7 ;
A9: (Comput (P,s,1)) . GBP = 0 by A5, SCMPDS_2:45;
A10: (Comput (P,s,1)) . (intpos 9) = s . (intpos 9) by A5, AMI_3:10, SCMPDS_2:45;
A11: (Comput (P,s,1)) . (intpos 10) = s . (intpos 10) by A5, AMI_3:10, SCMPDS_2:45;
A12: P /. (IC (Comput (P,s,2))) = P . (IC (Comput (P,s,2))) by PBOOLE:143;
A13: IC (Comput (P,s,2)) = (IC (Comput (P,s,1))) + 1 by A8, SCMPDS_2:45
.= 1 + 1 by A6 ;
then A14: CurInstr (P,(Comput (P,s,2))) = P . 2 by A12
.= saveIC (SBP,RetIC) by Lm1, A1 ;
A15: Comput (P,s,(2 + 1)) = Following (P,(Comput (P,s,2))) by EXTPRO_1:3
.= Exec ((saveIC (SBP,RetIC)),(Comput (P,s,2))) by A14 ;
A16: (Comput (P,s,2)) . GBP = 0 by A8, A9, AMI_3:10, SCMPDS_2:45;
A17: (Comput (P,s,2)) . SBP = 7 by A8, SCMPDS_2:45;
A18: (Comput (P,s,2)) . (intpos 9) = s . (intpos 9) by A8, A10, AMI_3:10, SCMPDS_2:45;
A19: (Comput (P,s,2)) . (intpos 10) = s . (intpos 10) by A8, A11, AMI_3:10, SCMPDS_2:45;
A20: P /. (IC (Comput (P,s,3))) = P . (IC (Comput (P,s,3))) by PBOOLE:143;
A21: IC (Comput (P,s,3)) = (IC (Comput (P,s,2))) + 1 by A15, SCMPDS_2:59
.= 2 + 1 by A13 ;
then A22: CurInstr (P,(Comput (P,s,3))) = P . 3 by A20
.= goto 2 by Lm1, A1 ;
A23: Comput (P,s,(3 + 1)) = Following (P,(Comput (P,s,3))) by EXTPRO_1:3
.= Exec ((goto 2),(Comput (P,s,3))) by A22 ;
A24: DataLoc (((Comput (P,s,2)) . SBP),RetIC) = intpos (7 + 1) by A17, Th1, SCMPDS_I:def 14;
then A25: (Comput (P,s,3)) . GBP = 0 by A15, A16, AMI_3:10, SCMPDS_2:59;
A26: (Comput (P,s,3)) . SBP = 7 by A15, A17, A24, AMI_3:10, SCMPDS_2:59;
A27: (Comput (P,s,3)) . (intpos 8) = 2 by A13, A15, A24, SCMPDS_2:59;
A28: (Comput (P,s,3)) . (intpos 9) = s . (intpos 9) by A15, A18, A24, AMI_3:10, SCMPDS_2:59;
A29: (Comput (P,s,3)) . (intpos 10) = s . (intpos 10) by A15, A19, A24, AMI_3:10, SCMPDS_2:59;
thus IC (Comput (P,s,4)) = ICplusConst ((Comput (P,s,3)),2) by A23, SCMPDS_2:54
.= 3 + 2 by A21, SCMPDS_6:12
.= 5 ; :: thesis: ( (Comput (P,s,4)) . GBP = 0 & (Comput (P,s,4)) . SBP = 7 & (Comput (P,s,4)) . (intpos (7 + RetIC)) = 2 & (Comput (P,s,4)) . (intpos 9) = s . (intpos 9) & (Comput (P,s,4)) . (intpos 10) = s . (intpos 10) )
thus (Comput (P,s,4)) . GBP = 0 by A23, A25, SCMPDS_2:54; :: thesis: ( (Comput (P,s,4)) . SBP = 7 & (Comput (P,s,4)) . (intpos (7 + RetIC)) = 2 & (Comput (P,s,4)) . (intpos 9) = s . (intpos 9) & (Comput (P,s,4)) . (intpos 10) = s . (intpos 10) )
thus (Comput (P,s,4)) . SBP = 7 by A23, A26, SCMPDS_2:54; :: thesis: ( (Comput (P,s,4)) . (intpos (7 + RetIC)) = 2 & (Comput (P,s,4)) . (intpos 9) = s . (intpos 9) & (Comput (P,s,4)) . (intpos 10) = s . (intpos 10) )
thus (Comput (P,s,4)) . (intpos (7 + RetIC)) = 2 by A23, A27, SCMPDS_2:54, SCMPDS_I:def 14; :: thesis: ( (Comput (P,s,4)) . (intpos 9) = s . (intpos 9) & (Comput (P,s,4)) . (intpos 10) = s . (intpos 10) )
thus (Comput (P,s,4)) . (intpos 9) = s . (intpos 9) by A23, A28, SCMPDS_2:54; :: thesis: (Comput (P,s,4)) . (intpos 10) = s . (intpos 10)
thus (Comput (P,s,4)) . (intpos 10) = s . (intpos 10) by A23, A29, SCMPDS_2:54; :: thesis: verum