# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1574224474 -32400
# Node ID 37c919cec9acdba3a3dd764346f97a216c767b2c
# Parent  f00c990a24dae107424a41be893396e9837a93aa
fin-∨' almost finished

diff -r f00c990a24da -r 37c919cec9ac agda/finiteSet.agda
--- a/agda/finiteSet.agda	Wed Nov 20 00:01:38 2019 +0900
+++ b/agda/finiteSet.agda	Wed Nov 20 13:34:34 2019 +0900
@@ -165,6 +165,10 @@
         lemma6 : {a b : ℕ } → {f : Fin a} → toℕ (inject+ b f) ≡ toℕ f
         lemma6 {suc a} {b} {zero} = refl
         lemma6 {suc a} {b} {suc f} = cong (λ k → suc k ) (lemma6 {a} {b} {f})
+        lemmaa : {a b c : ℕ } → {b<a : b <  a } → {c<a : c <  a} → b ≡ c → fromℕ≤ b<a ≡  fromℕ≤ c<a
+        lemmaa {suc a} {zero} {zero} {s≤s z≤n} {s≤s z≤n} refl = refl
+        lemmaa {suc a} {suc b} {suc b} {s≤s b<a} {s≤s c<a} refl = subst₂ ( λ j k → j ≡ k ) (sym (lemma3 _ )) (sym (lemma3 _ )) 
+           (cong (λ k → suc k ) ( lemmaa {a} {b} {b} {b<a} {c<a} refl ))
         Q←F : Fin n → Q
         Q←F f with Data.Nat.Properties.<-cmp (toℕ f) a
         Q←F f | tri< lt ¬b ¬c = case1 (FiniteSet.Q←F fa (fromℕ≤ lt )) 
@@ -177,13 +181,11 @@
         finiso→ (case1 qa) = lemma7 where
             lemma5 : toℕ (inject+ b (FiniteSet.F←Q fa qa)) < a 
             lemma5 = subst (λ k → k < a ) (sym lemma6) (toℕ<n (FiniteSet.F←Q fa qa))
-            lemma8 : ((toℕ (inject+ b (FiniteSet.F←Q fa qa))) < a) ≡ ( toℕ (FiniteSet.F←Q fa qa) < a )
-            lemma8 = {!!}
             lemma7 : Q←F (F←Q (case1 qa)) ≡ case1 qa
             lemma7 with Data.Nat.Properties.<-cmp (toℕ (inject+ b (FiniteSet.F←Q fa qa))) a
             lemma7 | tri< lt ¬b ¬c = begin
                    case1 (FiniteSet.Q←F fa (fromℕ≤ lt ))
-                ≡⟨ {!!} ⟩
+                ≡⟨ cong (λ k → case1 (FiniteSet.Q←F fa k )) (lemmaa lemma6 ) ⟩
                    case1 (FiniteSet.Q←F fa (fromℕ≤ (toℕ<n (FiniteSet.F←Q fa qa)) ))
                 ≡⟨ cong (λ k → case1 (FiniteSet.Q←F fa k )) lemma4 ⟩
                    case1 (FiniteSet.Q←F fa (FiniteSet.F←Q fa qa) )
@@ -192,9 +194,32 @@
                 ∎  where open ≡-Reasoning
             lemma7 | tri≈ ¬a b ¬c = ⊥-elim ( ¬a lemma5 )
             lemma7 | tri> ¬a ¬b c = ⊥-elim ( ¬a lemma5 )
-        finiso→ (case2 qb) = {!!} where
+        finiso→ (case2 qb) = lemma9 where
+            lemmab : toℕ (raise a (FiniteSet.F←Q fb qb)) > a
+            lemmab = {!!}
+            lemmac : (f : Fin b) (f>a : toℕ (raise a f) > a ) → f-a (raise a f) a f>a (toℕ<n (raise a f)) ≡ f 
+            lemmac = {!!}
+            lemmad : {qb : B } → 0 ≡ toℕ (FiniteSet.F←Q fb qb)
+            lemmad = {!!}
             lemma9 :  Q←F (F←Q (case2 qb)) ≡ case2 qb
-            lemma9 = {!!} 
+            lemma9 with Data.Nat.Properties.<-cmp (toℕ (raise a (FiniteSet.F←Q fb qb))) a
+            lemma9 | tri< a ¬b ¬c = ⊥-elim ( ¬c lemmab )
+            lemma9 | tri≈ ¬a eq ¬c = begin
+                    case2 (FiniteSet.Q←F fb (fromℕ≤ (0<b a (a<a+b eq ) )))
+                 ≡⟨ cong (λ k → case2 (FiniteSet.Q←F fb k )) (lemmaa lemmad ) ⟩
+                    case2 (FiniteSet.Q←F fb (fromℕ≤ (toℕ<n (FiniteSet.F←Q fb qb))))
+                 ≡⟨  cong (λ k → case2 (FiniteSet.Q←F fb k )) lemma4  ⟩
+                    case2 (FiniteSet.Q←F fb (FiniteSet.F←Q fb qb)) 
+                 ≡⟨ cong (λ k → case2 k ) (FiniteSet.finiso→ fb _ ) ⟩
+                    case2 qb
+                 ∎  where open ≡-Reasoning
+            lemma9 | tri> ¬a ¬b c = begin
+                    case2 (FiniteSet.Q←F fb (f-a (raise a (FiniteSet.F←Q fb qb)) a c (toℕ<n (raise a (FiniteSet.F←Q fb qb)) ) ))
+                 ≡⟨ cong (λ k → case2 (FiniteSet.Q←F fb k) ) (lemmac (FiniteSet.F←Q fb qb) c ) ⟩
+                    case2 (FiniteSet.Q←F fb (FiniteSet.F←Q fb qb)) 
+                 ≡⟨ cong (λ k → case2 k ) (FiniteSet.finiso→ fb _ ) ⟩
+                    case2 qb
+                 ∎  where open ≡-Reasoning
         finiso← : (f : Fin n ) → F←Q ( Q←F f ) ≡ f
         finiso← f with Data.Nat.Properties.<-cmp (toℕ f) a
         finiso← f | tri< lt ¬b ¬c = lemma11 where