# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1573211890 -32400
# Node ID 184752a8f0edc634e5e6cf23e3da56dd57216e65
# Parent  803391cc8b3e9a0465f6fd22dec0350162bb512d
...

diff -r 803391cc8b3e -r 184752a8f0ed agda/finiteSet.agda
--- a/agda/finiteSet.agda	Fri Nov 08 19:52:26 2019 +0900
+++ b/agda/finiteSet.agda	Fri Nov 08 20:18:10 2019 +0900
@@ -56,44 +56,28 @@
      fin<n : {n : ℕ} {f : Fin n} → toℕ f < n
      fin<n {_} {zero} = s≤s z≤n
      fin<n {suc n} {suc f} = s≤s (fin<n {n} {f})
-     <s : {m : ℕ} → m Data.Nat.≤ suc m
-     <s {zero} = z≤n
-     <s {suc m} = s≤s <s
-     lemma0 : {n : ℕ } {i j : ℕ } → i ≡ j → ( i<n : (suc i) Data.Nat.≤ n ) → ( j<n : (suc j) Data.Nat.≤ n ) → i<n ≅ j<n
-     lemma0 {_} {0} {0} refl (s≤s z≤n) (s≤s z≤n) = HE.refl
-     lemma0 {suc n} {suc i} {suc i} refl (s≤s (s≤s x)) (s≤s (s≤s y))  = HE.cong ( λ k → s≤s k) (lemma0 {n} {i} {i} refl (s≤s x)  (s≤s y))
-     lemma : {n : ℕ } {i j : ℕ } → i ≡ j → { i<n : (suc i) Data.Nat.≤ n } → { j<n : (suc j) Data.Nat.≤ n } → fromℕ≤ i<n ≅ fromℕ≤ j<n
-     lemma refl {x} {y} = HE.cong ( λ k → fromℕ≤ k ) ( lemma0 refl x y )
-     lemma1 : {i m : ℕ } (i≤m : (suc i) Data.Nat.≤ m ) (m<n : m Data.Nat.≤ n ) → i < n
-     lemma1 {i} {m} i≤m m<n =  Data.Nat.Properties.≤-trans i≤m m<n 
      found : { p : Q → Bool } → {q : Q } → p q ≡ true → exists p ≡ true
-     found {p} {q} pt = found1 n (toℕ (F←Q q)) (fin<n {n} {F←Q q}) (lt0 n) {!!} where
-         lemma2 : F←Q q ≅ fromℕ≤ (lemma1 (fin<n {n} {F←Q q}) (lt0 n))
-         lemma2 = {!!}
-         lemma3 : {m i : ℕ} → ( m<n : m Data.Nat.≤ n ) → (i≤m : i Data.Nat.≤ suc m )
-             → (iq :  F←Q q ≅ fromℕ≤ {i} {n} {!!} ) → Q←F (fromℕ≤ {!!}) ≡ q
-         lemma3 = {!!}
-         found1 : (m : ℕ ) (i : ℕ) (i≤m : (suc i) Data.Nat.≤ m ) (m<n : m Data.Nat.≤ n ) ( iq : F←Q q ≡ fromℕ≤ {i} (lemma1 i≤m m<n) ) →  exists1 m m<n p ≡ true
-         found1 (suc m) i lt m<n iq with Data.Nat._≟_ m i
-         found1 (suc m) i lt m<n iq | yes refl = begin
+     found {p} {q} pt = found1 n  (fin<n {n} {F←Q q}) (lt0 n) where
+         iq : {m : ℕ} (lt : suc m Data.Nat.≤ n ) → toℕ (F←Q q) ≡ m → Q←F (fromℕ≤ lt) ≡ q
+         iq {m} lt refl = begin
+                 Q←F (fromℕ≤ lt) 
+              ≡⟨ {!!} ⟩
+                 Q←F (F←Q q)
+              ≡⟨ finiso→ q ⟩
+                 q 
+              ∎  where open ≡-Reasoning
+         found1 : (m : ℕ ) {i : ℕ} (i≤m : (suc i) Data.Nat.≤ m ) (m<n : m Data.Nat.≤ n ) →  exists1 m m<n p ≡ true
+         found1 (suc m)  lt m<n with Data.Nat._≟_ m (toℕ (F←Q q))
+         found1 (suc m)  lt m<n | yes refl = begin
                  p (Q←F (fromℕ≤ m<n )) \/ exists1 m (lt2 m<n ) p
-              ≡⟨ cong (λ k → (p k \/ exists1 m (lt2 m<n ) p )) (
-                 begin
-                    Q←F (fromℕ≤ m<n) 
-                 ≡⟨ lemma HE.refl ⟩
-                    Q←F (fromℕ≤ {i} (lemma1 lt m<n))
-                 ≡⟨ cong ( λ k → Q←F k ) (sym iq)  ⟩
-                    Q←F (F←Q q)
-                 ≡⟨ {!!} ⟩
-                    q
-                 ∎ ) ⟩
+              ≡⟨ cong (λ k → (p k \/ exists1 m (lt2 m<n ) p )) (iq m<n refl ) ⟩
                  p q \/ exists1 m (lt2 m<n ) p
               ≡⟨ cong (λ k → ( k \/ exists1 m (lt2 m<n ) p )) pt ⟩
                   true \/ exists1 m (lt2 m<n ) p
               ≡⟨⟩
                  true 
               ∎  where open ≡-Reasoning
-         found1 (suc m) i lt m<n iq | no ¬p = {!!}
+         found1 (suc m)  lt m<n | no ¬p = {!!}
              
 
 fless : {n : ℕ} → (f : Fin n ) → toℕ f < n