Mercurial > hg > Members > kono > Proof > galois

changeset 32:5b299203acf0

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, 19 Aug 2020 16:37:59 +0900
parents 039e8511da2a
children a986f22cde84
files Symmetric.agda
diffstat 1 files changed, 5 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- a/Symmetric.agda	Wed Aug 19 16:18:32 2020 +0900
+++ b/Symmetric.agda	Wed Aug 19 16:37:59 2020 +0900
@@ -108,9 +108,14 @@
    piso← x | tri< a ¬b ¬c = begin
           p← ( fin+1 (perm ⟨$⟩ʳ (fromℕ≤ x<sn)) ) 
        ≡⟨ {!!} ⟩
+          fin+1 (perm ⟨$⟩ˡ (perm ⟨$⟩ʳ fromℕ≤ (<-trans a (s≤s m<n))))
+       ≡⟨ cong (λ k → fin+1 k ) (inverseˡ perm) ⟩
+          fin+1 (fromℕ≤ x<sn)
+       ≡⟨ {!!} ⟩
           x
        ∎  where
             open ≡-Reasoning
+            k = inverseˡ perm 
             x<sn : toℕ x < suc n
             x<sn = <-trans a (s≤s m<n)
    piso← x | tri> ¬a ¬b c = begin