Mercurial > hg > Members > kono > Proof > automaton

changeset 131:06a42928de38

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 Sun, 24 Nov 2019 11:05:32 +0900
parents 08990387c919
children 370b3fc69c1a
files agda/finiteSet.agda
diffstat 1 files changed, 12 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/agda/finiteSet.agda	Sun Nov 24 10:08:14 2019 +0900
+++ b/agda/finiteSet.agda	Sun Nov 24 11:05:32 2019 +0900
@@ -416,8 +416,18 @@
    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 = ?
-   ISO.iso→ iso x | case2 x1 = {!!}
+   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 | 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) )
 
 fin-× : {A B : Set} → { a b : ℕ } → FiniteSet A {a} → FiniteSet B {b} → FiniteSet (A × B) {a * b}
 fin-× {A} {B} {a} {b} fa fb with FiniteSet→Fin fa