Mercurial > hg > Members > kono > Proof > automaton

comparison automaton-in-agda/src/root2.agda @ 324:329adb1b71c7

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 Fri, 14 Jan 2022 22:58:25 +0900
parents 7f806a28a866
children 39f0e1d7a7e5
comparison
equal deleted inserted replaced
323:7f806a28a866 324:329adb1b71c7
217 r04 = begin 217 r04 = begin
218 1 ≡⟨ sym (Prime.isPrime pr _ {!!} {!!} ) ⟩ 218 1 ≡⟨ sym (Prime.isPrime pr _ {!!} {!!} ) ⟩
219 gcd p i ≡⟨ r02 r01 ⟩ 219 gcd p i ≡⟨ r02 r01 ⟩
220 i ∎ where open ≡-Reasoning 220 i ∎ where open ≡-Reasoning
221 ... | tri> ¬a ¬b c with <-cmp (Rational.i r) 1 221 ... | tri> ¬a ¬b c with <-cmp (Rational.i r) 1
222 ... | tri< a ¬b₁ ¬c = {!!} where 222 ... | tri< a ¬b₁ ¬c = ⊥-elim ( nat-≡< (sym r05) r08) where
223 i = Rational.i r 223 i = Rational.i r
224 j = Rational.j r 224 j = Rational.j r
225 r00 : p * j * j ≡ i * i 225 r00 : p * j * j ≡ i * i
226 r00 = r3 p (<-trans a<sa (Prime.p>1 pr )) r div 226 r00 = r3 p (<-trans a<sa (Prime.p>1 pr )) r div
227 r06 : i ≡ 0 227 r06 : i ≡ 0
228 r06 = {!!} 228 r06 with <-cmp i 0
229 r05 : p * j * j ≡ i * i -- j > 0 → p * j * j > 0 229 ... | tri≈ ¬a b ¬c = b
230 ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c a )
231 r05 : p * j * j ≡ 0
230 r05 = {!!} 232 r05 = {!!}
231 ... | tri≈ ¬a₁ b ¬c = {!!} where 233 r08 : p * j * j > 0
234 r08 = {!!}
235 ... | tri≈ ¬a₁ b ¬c = ⊥-elim ( nat-≡< (sym r07) r09) where
232 i = Rational.i r 236 i = Rational.i r
233 j = Rational.j r 237 j = Rational.j r
234 r00 : p * j * j ≡ i * i 238 r00 : p * j * j ≡ i * i
235 r00 = r3 p (<-trans a<sa (Prime.p>1 pr )) r div 239 r00 = r3 p (<-trans a<sa (Prime.p>1 pr )) r div
236 r07 : p * j * j ≡ i * i -- j > 0 → p * j * j > 0 240 r07 : p * j * j ≡ 1
237 r07 = {!!} 241 r07 = {!!}
242 r09 : 1 < p * j * j
243 r09 = {!!}
238 ... | tri> ¬a₁ ¬b₁ c₁ = root-prime-irrational (Rational.j r) (Rational.i r) p c pr c₁ (r3 p (<-trans a<sa (Prime.p>1 pr ) ) r div) 244 ... | tri> ¬a₁ ¬b₁ c₁ = root-prime-irrational (Rational.j r) (Rational.i r) p c pr c₁ (r3 p (<-trans a<sa (Prime.p>1 pr ) ) r div)
239 (trans (GCD.gcdsym {Rational.j r} {_} ) (Rational.coprime r) ) 245 (trans (GCD.gcdsym {Rational.j r} {_} ) (Rational.coprime r) )