Mercurial > hg > Members > kono > Proof > automaton
diff agda/finiteSet.agda @ 134:14cf0e1c8d91
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 24 Nov 2019 14:52:20 +0900 |
| parents | 65bea0aad363 |
| children | 2d70f90565c6 |
line wrap: on
line diff
--- a/agda/finiteSet.agda Sun Nov 24 14:30:11 2019 +0900 +++ b/agda/finiteSet.agda Sun Nov 24 14:52:20 2019 +0900 @@ -425,10 +425,10 @@ 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 | inspect (λ x → ISO.B←A iso ( ISO.A←B iso x )) x - ... | tri> ¬a ¬b c | record { eq = e } = ⊥-elim ( nat-≤> c (elm<n x) ) - ... | tri< a ¬b ¬c | record { eq = e } = {!!} - ... | tri≈ ¬a b ¬c | record { eq = e } = begin + ISO.iso→ iso x | case1 one with Data.Nat.Properties.<-cmp (toℕ (FiniteSet.F←Q fa (elm x )) ) n + ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c (elm<n x) ) + ... | tri< a ¬b ¬c = {!!} + ... | tri≈ ¬a b ¬c = begin record { elm = FiniteSet.Q←F fa (fromℕ≤ (Data.Nat.Properties.<-trans n<m a<sa)) ; elm<n = lemma5 } ≡⟨ Fin-<-cong (s≤s n<m) fa _ _ (sym (lemma2 b)) lemma7 ⟩ record { elm = elm x ; elm<n = elm<n x }