# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1574563020 -32400
# Node ID 370b3fc69c1ae6d05761daf2ccb56369799825a2
# Parent  06a42928de38693b0896827a69561119d14bace8
...

diff -r 06a42928de38 -r 370b3fc69c1a agda/finiteSet.agda
--- a/agda/finiteSet.agda	Sun Nov 24 11:05:32 2019 +0900
+++ b/agda/finiteSet.agda	Sun Nov 24 11:37:00 2019 +0900
@@ -394,15 +394,17 @@
    fin- : FiniteSet (Fin-< (Data.Nat.Properties.<-trans n<m a<sa) fa)
    fin- = fin-< {A} {n} {m} (Data.Nat.Properties.<-trans n<m a<sa) fa
    iso : ISO (One ∨ Fin-< (Data.Nat.Properties.<-trans n<m a<sa) fa) (Fin-< (s≤s n<m) fa)
-   c1 : toℕ (FiniteSet.F←Q fa (FiniteSet.Q←F fa (fromℕ≤ (Data.Nat.Properties.<-trans n<m a<sa) ))) ≡ n 
+   lastf = FiniteSet.F←Q fa (FiniteSet.Q←F fa (fromℕ≤ (Data.Nat.Properties.<-trans n<m a<sa) ))
+   last1 = FiniteSet.Q←F fa (fromℕ≤ (Data.Nat.Properties.<-trans n<m a<sa))
+   c1 : toℕ lastf ≡ n 
    c1 = subst (λ k → toℕ k ≡ n ) (sym (FiniteSet.finiso← fa _ )) (subst (λ k → k ≡ n) (sym (toℕ-fromℕ≤ _ )) refl )
-   f<n : toℕ (FiniteSet.F←Q fa (FiniteSet.Q←F fa (fromℕ≤ (Data.Nat.Properties.<-trans n<m a<sa)))) < suc n
+   f<n : toℕ lastf < suc n
    f<n = subst ( λ k → k < suc n ) (sym c1) a<sa
    ISO.A←B iso x with Data.Nat.Properties.<-cmp (toℕ (FiniteSet.F←Q fa (elm x )) ) n
    ISO.A←B iso x | tri< a ¬b ¬c = case2 record { elm = elm x ; elm<n = a }
    ISO.A←B iso x | tri≈ ¬a b ¬c = case1 one
    ISO.A←B iso x | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c (elm<n x) )
-   ISO.B←A iso (case1 one)  = record { elm = FiniteSet.Q←F fa (fromℕ≤ (Data.Nat.Properties.<-trans n<m a<sa) ); elm<n = f<n }
+   ISO.B←A iso (case1 one)  = record { elm = last1 ; elm<n = f<n }
    ISO.B←A iso (case2 x)  = record { elm = elm x ; elm<n = Data.Nat.Properties.<-trans (elm<n x) a<sa }
    ISO.iso← iso (case1 one) with Data.Nat.Properties.<-cmp (toℕ (FiniteSet.F←Q fa (elm (ISO.B←A iso (case1 one))))) n
    ISO.iso← iso (case1 one) | tri< a ¬b ¬c = ⊥-elim ( ¬b c1 )
@@ -415,16 +417,12 @@
      lemma1 {suc m} {suc n} (s≤s i) (s≤s j) = cong ( λ k → s≤s k ) ( lemma1 {m} {n} i j )
    ISO.iso← iso (case2 x) | tri≈ ¬a b ¬c = ⊥-elim ( nat-≡< b (elm<n x) )
    ISO.iso← iso (case2 x) | tri> ¬a ¬b c = ⊥-elim ( nat-<> c (elm<n x) )
-   ISO.iso→ iso x with ISO.A←B iso x 
-   ISO.iso→ iso x | case1 one with Data.Nat.Properties.<-cmp (toℕ (FiniteSet.F←Q fa (elm x )) ) n
-   ISO.iso→ iso x | case1 one | tri< a ¬b ¬c = ⊥-elim ( ¬c lemma3 ) where
-      lemma2 : n < toℕ (FiniteSet.F←Q fa (FiniteSet.Q←F fa (fromℕ≤ (Data.Nat.Properties.<-trans n<m a<sa))))  
-      lemma2 =  subst (λ k → n < toℕ k ) (sym (FiniteSet.finiso← fa _ )) {!!}
-      lemma3 : n < toℕ (FiniteSet.F←Q fa (elm x))
-      lemma3 = subst (λ k → n < toℕ k ) {!!} lemma2 
-   ISO.iso→ iso x | case1 one | tri≈ ¬a b ¬c = {!!}
-   ISO.iso→ iso x | case1 one | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c (elm<n x) )
-   ISO.iso→ iso x | case2 x1 = {!!} -- with Data.Nat.Properties.<-cmp (toℕ (FiniteSet.F←Q fa (elm x )) ) n
+   ISO.iso→ iso x with ISO.A←B iso x  
+   ISO.iso→ iso x | case1 one with Data.Nat.Properties.<-cmp (toℕ (FiniteSet.F←Q fa (elm x )) ) n | inspect (λ x → ISO.B←A iso ( ISO.A←B iso x )) x
+   ... | tri< a ¬b ¬c | record { eq = e } = {!!}
+   ... | tri≈ ¬a b ¬c | record { eq = e } = {!!} 
+   ... | tri> ¬a ¬b c | record { eq = e } = ⊥-elim ( nat-≤> c (elm<n x) )
+   ISO.iso→ iso x | case2 x1 = {!!}
    -- ISO.iso→ iso x | case2 x1 | tri< a ¬b ¬c = ?
    -- ISO.iso→ iso x | case2 x1 | tri≈ ¬a b ¬c = {!!}
    -- ISO.iso→ iso x | case2 x1 | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c (elm<n x) )