:: Recursive Euclide Algorithm :: by JingChao Chen :: :: Received June 15, 1999 :: Copyright (c) 1999-2012 Association of Mizar Users begin definition let k be Nat; func intpos k -> Int_position equals :: SCMP_GCD:def 1 dl. k; coherence dl. k is Int_position by SCMPDS_2:def_1; end; :: deftheorem defines intpos SCMP_GCD:def_1_:_ for k being Nat holds intpos k = dl. k; theorem Th1: :: SCMP_GCD:1 for n1, n2 being Element of NAT holds DataLoc (n1,n2) = intpos (n1 + n2) proofend; theorem Th2: :: SCMP_GCD:2 for s being State of SCMPDS for m1, m2 being Element of NAT st IC s = m1 + m2 holds ICplusConst (s,(- m2)) = m1 proofend; :: GBP:Global Base Pointer definition func GBP -> Int_position equals :: SCMP_GCD:def 2 intpos 0; coherence intpos 0 is Int_position ; func SBP -> Int_position equals :: SCMP_GCD:def 3 intpos 1; coherence intpos 1 is Int_position ; end; :: deftheorem defines GBP SCMP_GCD:def_2_:_ GBP = intpos 0; :: deftheorem defines SBP SCMP_GCD:def_3_:_ SBP = intpos 1; theorem :: SCMP_GCD:3 GBP <> SBP by AMI_3:10; theorem Th4: :: SCMP_GCD:4 for i being Instruction of SCMPDS for I being Program of SCMPDS holds card (I ';' i) = (card I) + 1 proofend; theorem Th5: :: SCMP_GCD:5 for i, j being Instruction of SCMPDS holds card (i ';' j) = 2 proofend; theorem Th6: :: SCMP_GCD:6 for i being Instruction of SCMPDS for I being Program of SCMPDS holds ( (I ';' i) . (card I) = i & card I in dom (I ';' i) ) proofend; theorem Th7: :: SCMP_GCD:7 for i being Instruction of SCMPDS for I, J being Program of SCMPDS holds ((I ';' i) ';' J) . (card I) = i proofend; begin :: Greatest Common Divisor :: gcd(x,y) < x=(SBP,2) y=(SBP,3) > :: BEGIN :: if y=0 then gcd:=x else :: gcd:=gcd(y, x mod y) :: END definition ::Def04 func GCD-Algorithm -> Program of SCMPDS equals :: SCMP_GCD:def 4 ((((((((((((((GBP := 0) ';' (SBP := 7)) ';' (saveIC (SBP,RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' ((SBP,3) <=0_goto 9)) ';' ((SBP,6) := (SBP,3))) ';' (Divide (SBP,2,SBP,3))) ';' ((SBP,7) := (SBP,3))) ';' ((SBP,(4 + RetSP)) := (GBP,1))) ';' (AddTo (GBP,1,4))) ';' (saveIC (SBP,RetIC))) ';' (goto (- 7))) ';' ((SBP,2) := (SBP,6))) ';' (return SBP); coherence ((((((((((((((GBP := 0) ';' (SBP := 7)) ';' (saveIC (SBP,RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' ((SBP,3) <=0_goto 9)) ';' ((SBP,6) := (SBP,3))) ';' (Divide (SBP,2,SBP,3))) ';' ((SBP,7) := (SBP,3))) ';' ((SBP,(4 + RetSP)) := (GBP,1))) ';' (AddTo (GBP,1,4))) ';' (saveIC (SBP,RetIC))) ';' (goto (- 7))) ';' ((SBP,2) := (SBP,6))) ';' (return SBP) is Program of SCMPDS ; end; :: deftheorem defines GCD-Algorithm SCMP_GCD:def_4_:_ GCD-Algorithm = ((((((((((((((GBP := 0) ';' (SBP := 7)) ';' (saveIC (SBP,RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' ((SBP,3) <=0_goto 9)) ';' ((SBP,6) := (SBP,3))) ';' (Divide (SBP,2,SBP,3))) ';' ((SBP,7) := (SBP,3))) ';' ((SBP,(4 + RetSP)) := (GBP,1))) ';' (AddTo (GBP,1,4))) ';' (saveIC (SBP,RetIC))) ';' (goto (- 7))) ';' ((SBP,2) := (SBP,6))) ';' (return SBP); set i00 = GBP := 0; set i01 = SBP := 7; set i02 = saveIC (SBP,RetIC); set i03 = goto 2; set i04 = halt SCMPDS; set i05 = (SBP,3) <=0_goto 9; set i06 = (SBP,6) := (SBP,3); set i07 = Divide (SBP,2,SBP,3); set i08 = (SBP,7) := (SBP,3); set i09 = (SBP,(4 + RetSP)) := (GBP,1); set i10 = AddTo (GBP,1,4); set i11 = saveIC (SBP,RetIC); set i12 = goto (- 7); set i13 = (SBP,2) := (SBP,6); set i14 = return SBP; begin theorem Th8: :: SCMP_GCD:8 card GCD-Algorithm = 15 proofend; theorem :: SCMP_GCD:9 for n being Element of NAT holds ( n < 15 iff n in dom GCD-Algorithm ) by Th8, AFINSQ_1:66; theorem Th10: :: SCMP_GCD:10 ( GCD-Algorithm . 0 = GBP := 0 & GCD-Algorithm . 1 = SBP := 7 & GCD-Algorithm . 2 = saveIC (SBP,RetIC) & GCD-Algorithm . 3 = goto 2 & GCD-Algorithm . 4 = halt SCMPDS & GCD-Algorithm . 5 = (SBP,3) <=0_goto 9 & GCD-Algorithm . 6 = (SBP,6) := (SBP,3) & GCD-Algorithm . 7 = Divide (SBP,2,SBP,3) & GCD-Algorithm . 8 = (SBP,7) := (SBP,3) & GCD-Algorithm . 9 = (SBP,(4 + RetSP)) := (GBP,1) & GCD-Algorithm . 10 = AddTo (GBP,1,4) & GCD-Algorithm . 11 = saveIC (SBP,RetIC) & GCD-Algorithm . 12 = goto (- 7) & GCD-Algorithm . 13 = (SBP,2) := (SBP,6) & GCD-Algorithm . 14 = return SBP ) proofend; Lm1: for P being Instruction-Sequence of SCMPDS st GCD-Algorithm c= P holds ( P . 0 = GBP := 0 & P . 1 = SBP := 7 & P . 2 = saveIC (SBP,RetIC) & P . 3 = goto 2 & P . 4 = halt SCMPDS & P . 5 = (SBP,3) <=0_goto 9 & P . 6 = (SBP,6) := (SBP,3) & P . 7 = Divide (SBP,2,SBP,3) & P . 8 = (SBP,7) := (SBP,3) & P . 9 = (SBP,(4 + RetSP)) := (GBP,1) & P . 10 = AddTo (GBP,1,4) & P . 11 = saveIC (SBP,RetIC) & P . 12 = goto (- 7) & P . 13 = (SBP,2) := (SBP,6) & P . 14 = return SBP ) proofend; theorem Th11: :: SCMP_GCD:11 for P being Instruction-Sequence of SCMPDS st GCD-Algorithm c= P holds 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) ) proofend; Lm2: for n, m being Element of NAT st n > 0 holds GBP <> intpos (m + n) proofend; Lm3: for n, m being Element of NAT st n > 1 holds SBP <> intpos (m + n) proofend; Lm4: for n being Element of NAT for s being State of SCMPDS for P being Instruction-Sequence of SCMPDS st GCD-Algorithm c= P & IC s = 5 & n = s . SBP & s . GBP = 0 & s . (DataLoc ((s . SBP),3)) > 0 holds ( IC (Comput (P,s,7)) = 5 + 7 & Comput (P,s,8) = Exec ((goto (- 7)),(Comput (P,s,7))) & (Comput (P,s,7)) . SBP = n + 4 & (Comput (P,s,7)) . GBP = 0 & (Comput (P,s,7)) . (intpos (n + 7)) = (s . (DataLoc ((s . SBP),2))) mod (s . (DataLoc ((s . SBP),3))) & (Comput (P,s,7)) . (intpos (n + 6)) = s . (DataLoc ((s . SBP),3)) & (Comput (P,s,7)) . (intpos (n + 4)) = n & (Comput (P,s,7)) . (intpos (n + 5)) = 11 ) proofend; Lm5: for n, m being Element of NAT for s being State of SCMPDS for P being Instruction-Sequence of SCMPDS st GCD-Algorithm c= P & IC s = 5 & n = s . SBP & s . GBP = 0 & s . (DataLoc ((s . SBP),3)) > 0 & 1 < m & m <= n + 1 holds (Comput (P,s,7)) . (intpos m) = s . (intpos m) proofend; theorem Th12: :: SCMP_GCD:12 for P being Instruction-Sequence of SCMPDS for s being State of SCMPDS st GCD-Algorithm c= P & IC s = 5 & s . SBP > 0 & s . GBP = 0 & s . (DataLoc ((s . SBP),3)) >= 0 & s . (DataLoc ((s . SBP),2)) >= s . (DataLoc ((s . SBP),3)) holds ex n being Element of NAT st ( CurInstr (P,(Comput (P,s,n))) = return SBP & s . SBP = (Comput (P,s,n)) . SBP & (Comput (P,s,n)) . (DataLoc ((s . SBP),2)) = (s . (DataLoc ((s . SBP),2))) gcd (s . (DataLoc ((s . SBP),3))) & ( for j being Element of NAT st 1 < j & j <= (s . SBP) + 1 holds s . (intpos j) = (Comput (P,s,n)) . (intpos j) ) ) proofend; theorem Th13: :: SCMP_GCD:13 for P being Instruction-Sequence of SCMPDS for s being State of SCMPDS st GCD-Algorithm c= P & IC s = 5 & s . SBP > 0 & s . GBP = 0 & s . (DataLoc ((s . SBP),3)) >= 0 & s . (DataLoc ((s . SBP),2)) >= 0 holds ex n being Element of NAT st ( CurInstr (P,(Comput (P,s,n))) = return SBP & s . SBP = (Comput (P,s,n)) . SBP & (Comput (P,s,n)) . (DataLoc ((s . SBP),2)) = (s . (DataLoc ((s . SBP),2))) gcd (s . (DataLoc ((s . SBP),3))) & ( for j being Element of NAT st 1 < j & j <= (s . SBP) + 1 holds s . (intpos j) = (Comput (P,s,n)) . (intpos j) ) ) proofend; begin theorem :: SCMP_GCD:14 for P being Instruction-Sequence of SCMPDS 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 proofend; Lm6: for n being Element of NAT for s1, s2 being State of SCMPDS for P1, P2 being Instruction-Sequence of SCMPDS st GCD-Algorithm c= P1 & GCD-Algorithm c= P2 & IC s1 = 5 & n = s1 . SBP & s1 . GBP = 0 & s1 . (DataLoc ((s1 . SBP),3)) > 0 & IC s2 = IC s1 & s2 . SBP = s1 . SBP & s2 . GBP = 0 & s2 . (DataLoc ((s1 . SBP),2)) = s1 . (DataLoc ((s1 . SBP),2)) & s2 . (DataLoc ((s1 . SBP),3)) = s1 . (DataLoc ((s1 . SBP),3)) holds ( IC (Comput (P1,s1,7)) = 5 + 7 & Comput (P1,s1,8) = Exec ((goto (- 7)),(Comput (P1,s1,7))) & (Comput (P1,s1,7)) . SBP = n + 4 & (Comput (P1,s1,7)) . GBP = 0 & (Comput (P1,s1,7)) . (intpos (n + 7)) = (s1 . (intpos (n + 2))) mod (s1 . (intpos (n + 3))) & (Comput (P1,s1,7)) . (intpos (n + 6)) = s1 . (intpos (n + 3)) & IC (Comput (P2,s2,7)) = 5 + 7 & Comput (P2,s2,8) = Exec ((goto (- 7)),(Comput (P2,s2,7))) & (Comput (P2,s2,7)) . SBP = n + 4 & (Comput (P2,s2,7)) . GBP = 0 & (Comput (P2,s2,7)) . (intpos (n + 7)) = (s1 . (intpos (n + 2))) mod (s1 . (intpos (n + 3))) & (Comput (P2,s2,7)) . (intpos (n + 6)) = s1 . (intpos (n + 3)) & (Comput (P1,s1,7)) . (intpos (n + 4)) = n & (Comput (P1,s1,7)) . (intpos (n + 5)) = 11 & (Comput (P2,s2,7)) . (intpos (n + 4)) = n & (Comput (P2,s2,7)) . (intpos (n + 5)) = 11 ) proofend; Lm7: for n being Element of NAT for s1, s2 being State of SCMPDS for P1, P2 being Instruction-Sequence of SCMPDS st GCD-Algorithm c= P1 & GCD-Algorithm c= P2 & IC s1 = 5 & n = s1 . SBP & s1 . GBP = 0 & s1 . (DataLoc ((s1 . SBP),3)) > 0 & IC s2 = IC s1 & s2 . SBP = s1 . SBP & s2 . GBP = 0 & s2 . (DataLoc ((s1 . SBP),2)) = s1 . (DataLoc ((s1 . SBP),2)) & s2 . (DataLoc ((s1 . SBP),3)) = s1 . (DataLoc ((s1 . SBP),3)) holds for k being Element of NAT for a being Int_position st k <= 7 & s1 . a = s2 . a holds ( IC (Comput (P1,s1,k)) = IC (Comput (P2,s2,k)) & (Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . a ) proofend; Lm8: for P1, P2 being Instruction-Sequence of SCMPDS for s1, s2 being State of SCMPDS st GCD-Algorithm c= P1 & GCD-Algorithm c= P2 & IC s1 = 5 & s1 . SBP > 0 & s1 . GBP = 0 & s1 . (DataLoc ((s1 . SBP),3)) >= 0 & s1 . (DataLoc ((s1 . SBP),2)) >= s1 . (DataLoc ((s1 . SBP),3)) & IC s2 = IC s1 & s2 . SBP = s1 . SBP & s2 . GBP = 0 & s2 . (DataLoc ((s1 . SBP),2)) = s1 . (DataLoc ((s1 . SBP),2)) & s2 . (DataLoc ((s1 . SBP),3)) = s1 . (DataLoc ((s1 . SBP),3)) holds ex n being Element of NAT st ( CurInstr (P1,(Comput (P1,s1,n))) = return SBP & s1 . SBP = (Comput (P1,s1,n)) . SBP & CurInstr (P2,(Comput (P2,s2,n))) = return SBP & s2 . SBP = (Comput (P2,s2,n)) . SBP & ( for j being Element of NAT st 1 < j & j <= (s1 . SBP) + 1 holds ( s1 . (intpos j) = (Comput (P1,s1,n)) . (intpos j) & s2 . (intpos j) = (Comput (P2,s2,n)) . (intpos j) ) ) & ( for k being Element of NAT for a being Int_position st k <= n & s1 . a = s2 . a holds ( IC (Comput (P1,s1,k)) = IC (Comput (P2,s2,k)) & (Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . a ) ) ) proofend; Lm9: for P1, P2 being Instruction-Sequence of SCMPDS for s1, s2 being State of SCMPDS for a being Int_position for k being Element of NAT st Start-At (0,SCMPDS) c= s1 & Start-At (0,SCMPDS) c= s2 & GCD-Algorithm c= P1 & GCD-Algorithm c= P2 & s1 . a = s2 . a & k <= 4 holds ( IC (Comput (P1,s1,k)) = IC (Comput (P2,s2,k)) & (Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . a ) proofend; begin theorem :: SCMP_GCD:15 for p being FinPartState of SCMPDS for x, y being Integer st y >= 0 & x >= y & p = ((intpos 9),(intpos 10)) --> (x,y) holds Initialize p is GCD-Algorithm -autonomic proofend;