Mercurial > hg > Members > kono > Proof > ZF-in-agda

changeset 1354:3e14418230bc

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, 18 Jun 2023 20:17:50 +0900
parents ddbc0726f9bb
children db8229569750
files src/bijection.agda
diffstat 1 files changed, 4 insertions(+), 27 deletions(-) [+]
line wrap: on
line diff
--- a/src/bijection.agda	Sun Jun 18 18:16:03 2023 +0900
+++ b/src/bijection.agda	Sun Jun 18 20:17:50 2023 +0900
@@ -934,38 +934,15 @@
     c1<count-A zero (suc i) = ?
     c1<count-A (suc n) (suc i) with is-A (fun← cn (suc i)) |  <-cmp (fun→ cn (g (f (fun← an (suc n))))) (suc i)
     ... | no nisa | tri< a ¬b ¬c = ? where -- subst (λ k → k ≤ count-A i) (sym (lem11 n ≤-refl)) lem10 where
-          lem12 : suc (c1 n (suc i)) ≤ count-A i
-          lem12 = ?
           lem13 : c1 n i ≡ c1 n (suc i) 
           lem13 = c1+0 {n} {i} nisa
           lem10 : c1 n i ≤ count-A i
           lem10 = c1<count-A n i
-          lem14 : suc (c1 n i) ≤ count-A i   -- becase count-A i contains (ani (suc n))
-          lem14 = ?
-          lem11 : (j : ℕ ) → j ≤ n → suc (c1 j (suc i)) ≡ c1 j i 
-          lem11 zero j≤n with <-cmp (fun→ cn (g (f (fun← an zero)))) i | <-cmp (fun→ cn (g (f (fun← an zero)))) (suc i) 
-          ... | tri< a₂ ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = ?
-          ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = ⊥-elim ( nisa record { a = fun← an 0  ; fa=c = trans (sym (fiso← cn _)) (cong (fun← cn) b) })
-          ... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c₁ = refl
-          ... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ = ?
-          ... | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ = ?
-          ... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c₁ = ?
-          ... | tri> ¬a ¬b c₁ | tri< a ¬b₁ ¬c = ?
-          ... | tri> ¬a ¬b c₁ | tri≈ ¬a₁ b ¬c = ?
-          ... | tri> ¬a ¬b c₁ | tri> ¬a₁ ¬b₁ c₂ = ?
-          lem11 (suc j) j≤n with <-cmp (fun→ cn (g (f (fun← an (suc j))))) i | <-cmp (fun→ cn (g (f (fun← an (suc j)))))  (suc i)
-          ... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = cong suc (lem11 j (≤-trans a≤sa j≤n ) )
-          ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = cong suc (lem11 j  (≤-trans a≤sa j≤n ))
-          ... | tri< a₁ ¬b ¬c | tri> ¬a ¬b₁ c₁ = ⊥-elim ( nat-≡< refl ( <-trans a₁ (<-trans a<sa c₁ )))
-          ... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ = cong suc (lem11 j  (≤-trans a≤sa j≤n ))
-          ... | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ = cong suc (lem11 j  (≤-trans a≤sa j≤n ))
-          ... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c₁ = ⊥-elim ( nat-≡< (sym b) (<-trans a<sa c₁) )
-          ... | tri> ¬a ¬b c₁ | tri< (s≤s a₁) ¬b₁ ¬c = ⊥-elim (nat-≤> a₁ c₁ )
-          ... | tri> ¬a ¬b c₁ | tri≈ ¬a₁ b ¬c = ⊥-elim ( nisa record { a = fun← an (suc j) ; fa=c = trans (sym (fiso← cn _)) (cong (fun← cn) b) })  
-          ... | tri> ¬a ¬b c₁ | tri> ¬a₁ ¬b₁ c₂ = lem11 j  (≤-trans a≤sa j≤n )
-    ... | no nisa | tri≈ ¬a b ¬c = ?
+          lem12 : suc (c1 n (suc i)) ≤ count-A i  -- becase count-A i contains (ani (suc n))
+          lem12 = ?
+    ... | no nisa | tri≈ ¬a b ¬c = ⊥-elim (nisa ? )
     ... | no nisa | tri> ¬a ¬b c₁ = ?
-    ... | yes isa | tri< a ¬b ¬c = ?
+    ... | yes isa | tri< a ¬b ¬c = ?   -- count-A contains (suc i), so keep ≤-relation
     ... | yes isa | tri≈ ¬a b ¬c = ?
     ... | yes isa | tri> ¬a ¬b c₁ = ?