Mercurial > hg > Members > kono > Proof > automaton

comparison automaton-in-agda/src/root2.agda @ 330:407684f806e4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 16 Nov 2022 17:43:10 +0900
parents 39f0e1d7a7e5
children af8f630b7e60
comparison
equal deleted inserted replaced
329:ba0ae5de62d1 330:407684f806e4
44 divdable^2 (suc n) (suc k) 1<k 1<n pk dn2 with decD {suc k} {suc n} 1<k 44 divdable^2 (suc n) (suc k) 1<k 1<n pk dn2 with decD {suc k} {suc n} 1<k
45 ... | yes y = y 45 ... | yes y = y
46 ... | no non with gcd-euclid (suc k) (suc n) (suc n) 1<k (<-trans a<sa 1<n) (<-trans a<sa 1<n) (Prime.isPrime pk) dn2 46 ... | no non with gcd-euclid (suc k) (suc n) (suc n) 1<k (<-trans a<sa 1<n) (<-trans a<sa 1<n) (Prime.isPrime pk) dn2
47 ... | case1 dn = dn 47 ... | case1 dn = dn
48 ... | case2 dm = dm 48 ... | case2 dm = dm
49
50 -- divdable-n*m : { n m k : ℕ } → 1 < k → 1 < n → Prime k → Dividable k ( n * m ) → Dividable k n ∨ Dividable k n
51 -- divdable-n*m = ?
52
53 -- 2^2 : { n k : ℕ } → 1 < n → Dividable 2 ( n * n ) → Dividable 2 n
54 -- 2^2 = ?
49 55
50 -- p * n * n ≡ m * m means (m/n)^2 = p 56 -- p * n * n ≡ m * m means (m/n)^2 = p
51 -- rational m/n requires m and n is comprime each other which contradicts the condition 57 -- rational m/n requires m and n is comprime each other which contradicts the condition
52 58
53 root-prime-irrational : ( n m p : ℕ ) → n > 1 → Prime p → m > 1 → p * n * n ≡ m * m → ¬ (gcd n m ≡ 1) 59 root-prime-irrational : ( n m p : ℕ ) → n > 1 → Prime p → m > 1 → p * n * n ≡ m * m → ¬ (gcd n m ≡ 1)