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 ;
A4: IC s = 0 by MEMSTR_0:def 9;
A5: P /. (IC s) = P . (IC s) by PBOOLE:143;
A6: P /. (IC (Comput (P,s,1))) = P . (IC (Comput (P,s,1))) by PBOOLE:143;
A7: 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 A4, Lm1, A5, A1 ;
then A8: IC (Comput (P,s,1)) = succ (IC s) by SCMPDS_2:45
.= 0 + 1 by A4 ;
then A9: CurInstr (P,(Comput (P,s,1))) = P . 1 by A6
.= SBP := 7 by Lm1, A1 ;
A11: Comput (P,s,(1 + 1)) = Following (P,(Comput (P,s,1))) by EXTPRO_1:3
.= Exec ((SBP := 7),(Comput (P,s,1))) by A9 ;
A12: (Comput (P,s,1)) . GBP = 0 by A7, SCMPDS_2:45;
A13: (Comput (P,s,1)) . (intpos 9) = s . (intpos 9) by A7, AMI_3:10, SCMPDS_2:45;
A14: (Comput (P,s,1)) . (intpos 10) = s . (intpos 10) by A7, AMI_3:10, SCMPDS_2:45;
A15: P /. (IC (Comput (P,s,2))) = P . (IC (Comput (P,s,2))) by PBOOLE:143;
A16: IC (Comput (P,s,2)) = succ (IC (Comput (P,s,1))) by A11, SCMPDS_2:45
.= 1 + 1 by A8 ;
then A17: CurInstr (P,(Comput (P,s,2))) = P . 2 by A15
.= saveIC (SBP,RetIC) by Lm1, A1 ;
A19: Comput (P,s,(2 + 1)) = Following (P,(Comput (P,s,2))) by EXTPRO_1:3
.= Exec ((saveIC (SBP,RetIC)),(Comput (P,s,2))) by A17 ;
A20: (Comput (P,s,2)) . GBP = 0 by A11, A12, AMI_3:10, SCMPDS_2:45;
A21: (Comput (P,s,2)) . SBP = 7 by A11, SCMPDS_2:45;
A22: (Comput (P,s,2)) . (intpos 9) = s . (intpos 9) by A11, A13, AMI_3:10, SCMPDS_2:45;
A23: (Comput (P,s,2)) . (intpos 10) = s . (intpos 10) by A11, A14, AMI_3:10, SCMPDS_2:45;
A24: P /. (IC (Comput (P,s,3))) = P . (IC (Comput (P,s,3))) by PBOOLE:143;
A25: IC (Comput (P,s,3)) = succ (IC (Comput (P,s,2))) by A19, SCMPDS_2:59
.= 2 + 1 by A16 ;
then A26: CurInstr (P,(Comput (P,s,3))) = P . 3 by A24
.= goto 2 by Lm1, A1 ;
A28: Comput (P,s,(3 + 1)) = Following (P,(Comput (P,s,3))) by EXTPRO_1:3
.= Exec ((goto 2),(Comput (P,s,3))) by A26 ;
A29: DataLoc (((Comput (P,s,2)) . SBP),RetIC) = intpos (7 + 1) by A21, Th5, SCMPDS_1:def 21;
then A30: (Comput (P,s,3)) . GBP = 0 by A19, A20, AMI_3:10, SCMPDS_2:59;
A31: (Comput (P,s,3)) . SBP = 7 by A19, A21, A29, AMI_3:10, SCMPDS_2:59;
A32: (Comput (P,s,3)) . (intpos 8) = 2 by A16, A19, A29, SCMPDS_2:59;
A33: (Comput (P,s,3)) . (intpos 9) = s . (intpos 9) by A19, A22, A29, AMI_3:10, SCMPDS_2:59;
A34: (Comput (P,s,3)) . (intpos 10) = s . (intpos 10) by A19, A23, A29, AMI_3:10, SCMPDS_2:59;
thus IC (Comput (P,s,4)) = ICplusConst ((Comput (P,s,3)),2) by A28, SCMPDS_2:54
.= 3 + 2 by A25, 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 A28, A30, 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 A28, A31, 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 A28, A32, SCMPDS_1:def 21, SCMPDS_2:54; :: 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 A28, A33, SCMPDS_2:54; :: thesis: (Comput (P,s,4)) . (intpos 10) = s . (intpos 10)
thus (Comput (P,s,4)) . (intpos 10) = s . (intpos 10) by A28, A34, SCMPDS_2:54; :: thesis: verum