Created
June 26, 2015 04:19
-
-
Save wenjianhn/4a0551bafe954c6a7f46 to your computer and use it in GitHub Desktop.
The Greatest Common Divisor
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| -------------------------------- MODULE GCD -------------------------------- | |
| EXTENDS Integers | |
| Divides(p, n) == | |
| \E q \in -n..n : n = q * p | |
| DivisorsOf(n) == {p \in -n..n : Divides(p, n)} | |
| SetMax(S) == | |
| CHOOSE i \in S : \A j \in S : i >= j | |
| GCD(m, n) == | |
| SetMax(DivisorsOf(m) \cap DivisorsOf(n)) | |
| ============================================================================= | |
| \* Modification History | |
| \* Last modified Fri Jun 26 11:17:37 CST 2015 by jian | |
| \* Created Fri Jun 26 11:14:28 CST 2015 by jian |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment