Mercurial > hg > Members > kono > Proof > galois

comparison Putil.agda @ 161:047efc82be47

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
sized fresh list
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 22 Nov 2020 20:43:01 +0900
parents d880595eae30
children
comparison
equal deleted inserted replaced
160:254f3acb2091 161:047efc82be47
195 p15 with <-cmp (toℕ y) (suc m) -- eq : suc y ≡ suc (suc (fromℕ< (≤-pred (≤-trans a (s≤s m≤n))))) , a : suc x < suc m 195 p15 with <-cmp (toℕ y) (suc m) -- eq : suc y ≡ suc (suc (fromℕ< (≤-pred (≤-trans a (s≤s m≤n))))) , a : suc x < suc m
196 ... | tri< a₁ ¬b ¬c = p11 where 196 ... | tri< a₁ ¬b ¬c = p11 where
197 p11 : fromℕ< (≤-trans (fin<n {_} {y}) a≤sa ) ≡ suc x 197 p11 : fromℕ< (≤-trans (fin<n {_} {y}) a≤sa ) ≡ suc x
198 p11 = begin 198 p11 = begin
199 fromℕ< (≤-trans (fin<n {_} {y}) a≤sa ) 199 fromℕ< (≤-trans (fin<n {_} {y}) a≤sa )
200 ≡⟨ fromℕ<-irrelevant _ _ p12 _ (s≤s (fin<n {suc n})) ⟩ 200 -- ≡⟨ fromℕ<-irrelevant _ _ p12 _ (s≤s (fin<n {suc n})) ⟩
201 ≡⟨ {!!} ⟩
201 suc (fromℕ< (fin<n {suc n} {x} )) 202 suc (fromℕ< (fin<n {suc n} {x} ))
202 ≡⟨ cong suc (fromℕ<-toℕ x _ ) ⟩ 203 ≡⟨ cong suc (fromℕ<-toℕ x _ ) ⟩
203 suc x 204 suc x
204 ∎ 205 ∎
205 ... | tri≈ ¬a b ¬c = ⊥-elim ( nat-≡< b (subst (λ k → k < suc m) (sym p12) a )) -- suc x < suc m -> y = suc x → toℕ y < suc m 206 ... | tri≈ ¬a b ¬c = ⊥-elim ( nat-≡< b (subst (λ k → k < suc m) (sym p12) a )) -- suc x < suc m -> y = suc x → toℕ y < suc m
276 p005 zero m eq (s≤s m≤n) meq = p004 where 277 p005 zero m eq (s≤s m≤n) meq = p004 where
277 p004 : perm ⟨$⟩ˡ (fromℕ< (s≤s (s≤s m≤n))) ≡ zero 278 p004 : perm ⟨$⟩ˡ (fromℕ< (s≤s (s≤s m≤n))) ≡ zero
278 p004 = p003 (fromℕ< (s≤s (s≤s m≤n))) ( 279 p004 = p003 (fromℕ< (s≤s (s≤s m≤n))) (
279 begin 280 begin
280 fromℕ< (s≤s (s≤s m≤n)) 281 fromℕ< (s≤s (s≤s m≤n))
281 ≡⟨ fromℕ<-irrelevant _ _ (cong suc meq) (s≤s (s≤s m≤n)) (subst (λ k → suc k < suc (suc n)) meq (s≤s (s≤s m≤n)) ) ⟩ 282 -- ≡⟨ fromℕ<-irrelevant _ _ (cong suc meq) (s≤s (s≤s m≤n)) (subst (λ k → suc k < suc (suc n)) meq (s≤s (s≤s m≤n)) ) ⟩
283 ≡⟨ {!!} ⟩
282 fromℕ< (subst (λ k → suc k < suc (suc n)) meq (s≤s (s≤s m≤n)) ) 284 fromℕ< (subst (λ k → suc k < suc (suc n)) meq (s≤s (s≤s m≤n)) )
283 ≡⟨ fromℕ<-toℕ {suc (suc n)} (suc t) (subst (λ k → suc k < suc (suc n)) meq (s≤s (s≤s m≤n)) ) ⟩ 285 ≡⟨ fromℕ<-toℕ {suc (suc n)} (suc t) (subst (λ k → suc k < suc (suc n)) meq (s≤s (s≤s m≤n)) ) ⟩
284 suc t 286 suc t
285 ≡⟨ sym e ⟩ 287 ≡⟨ sym e ⟩
286 (perm ⟨$⟩ʳ (# 0)) 288 (perm ⟨$⟩ʳ (# 0))