diff options
Diffstat (limited to 'consecutive-fibonacci-numbers-are-coprime.lisp')
| -rw-r--r-- | consecutive-fibonacci-numbers-are-coprime.lisp | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/consecutive-fibonacci-numbers-are-coprime.lisp b/consecutive-fibonacci-numbers-are-coprime.lisp index e9bc9e2..1700e8e 100644 --- a/consecutive-fibonacci-numbers-are-coprime.lisp +++ b/consecutive-fibonacci-numbers-are-coprime.lisp @@ -17,13 +17,13 @@ (declare (xargs :measure (+ (nfix m) (nfix n)) :guard (and (posp n) (posp m)))) - (cond - ((or (not (posp n)) - (not (posp m)) - (= (nfix n) (nfix m))) - n) - ((< n m) (gcd$ (- m n) n)) - (t (gcd$ (- n m) m)))) + (if (and (posp n) (posp m)) + (cond + ((= (nfix n) (nfix m)) + n) + ((< n m) (gcd$ (- m n) n)) + (t (gcd$ (- n m) m))) + 0)) ;; gcd$ の結果は正の整数である (defthm posp-gcd$ |