let P be the Instructions of SCMPDS -valued ManySortedSet of NAT ; :: thesis: ( GCD-Algorithm c= P implies for s being State of SCMPDS st Start-At (0,SCMPDS) c= s 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 State of SCMPDS st Start-At (0,SCMPDS) c= s 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 State of SCMPDS; :: thesis: ( Start-At (0,SCMPDS) c= s implies ( 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 ;
assume Start-At (0,SCMPDS) c= s ; :: 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) )
then A4: IC s = 0 by COMPOS_1:222;
A5: P /. (IC s) = P . (IC s) by PBOOLE:158;
A6: P /. (IC (Comput (P,s,1))) = P . (IC (Comput (P,s,1))) by PBOOLE:158;
A7: Comput (P,s,(0 + 1)) = Following (P,(Comput (P,s,0))) by EXTPRO_1:4
.= Following (P,s) by EXTPRO_1:3
.= Exec ((GBP := 0),s) by A4, Lm1, A5, A1 ;
then A8: IC (Comput (P,s,1)) = succ (IC s) by SCMPDS_2:57
.= 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:4
.= Exec ((SBP := 7),(Comput (P,s,1))) by A9 ;
A12: (Comput (P,s,1)) . GBP = 0 by A7, SCMPDS_2:57;
A13: (Comput (P,s,1)) . (intpos 9) = s . (intpos 9) by A7, AMI_3:52, SCMPDS_2:57;
A14: (Comput (P,s,1)) . (intpos 10) = s . (intpos 10) by A7, AMI_3:52, SCMPDS_2:57;
A15: P /. (IC (Comput (P,s,2))) = P . (IC (Comput (P,s,2))) by PBOOLE:158;
A16: IC (Comput (P,s,2)) = succ (IC (Comput (P,s,1))) by A11, SCMPDS_2:57
.= 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:4
.= Exec ((saveIC (SBP,RetIC)),(Comput (P,s,2))) by A17 ;
A20: (Comput (P,s,2)) . GBP = 0 by A11, A12, AMI_3:52, SCMPDS_2:57;
A21: (Comput (P,s,2)) . SBP = 7 by A11, SCMPDS_2:57;
A22: (Comput (P,s,2)) . (intpos 9) = s . (intpos 9) by A11, A13, AMI_3:52, SCMPDS_2:57;
A23: (Comput (P,s,2)) . (intpos 10) = s . (intpos 10) by A11, A14, AMI_3:52, SCMPDS_2:57;
A24: P /. (IC (Comput (P,s,3))) = P . (IC (Comput (P,s,3))) by PBOOLE:158;
A25: IC (Comput (P,s,3)) = succ (IC (Comput (P,s,2))) by A19, SCMPDS_2:71
.= 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:4
.= 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 23;
then A30: (Comput (P,s,3)) . GBP = 0 by A19, A20, AMI_3:52, SCMPDS_2:71;
A31: (Comput (P,s,3)) . SBP = 7 by A19, A21, A29, AMI_3:52, SCMPDS_2:71;
A32: (Comput (P,s,3)) . (intpos 8) = 2 by A16, A19, A29, SCMPDS_2:71;
A33: (Comput (P,s,3)) . (intpos 9) = s . (intpos 9) by A19, A22, A29, AMI_3:52, SCMPDS_2:71;
A34: (Comput (P,s,3)) . (intpos 10) = s . (intpos 10) by A19, A23, A29, AMI_3:52, SCMPDS_2:71;
thus IC (Comput (P,s,4)) = ICplusConst ((Comput (P,s,3)),2) by A28, SCMPDS_2:66
.= 3 + 2 by A25, SCMPDS_6:23
.= 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:66; :: 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:66; :: 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 23, SCMPDS_2:66; :: 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:66; :: 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:66; :: thesis: verum