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

changeset 1338:b969f1710434

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 Fri, 16 Jun 2023 11:38:05 +0900
parents 31c9f7fc6466
children 23bba94a980f
files src/bijection.agda
diffstat 1 files changed, 24 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
--- a/src/bijection.agda	Fri Jun 16 08:49:25 2023 +0900
+++ b/src/bijection.agda	Fri Jun 16 11:38:05 2023 +0900
@@ -671,9 +671,30 @@
 
     --
     c1-at-i : (n i : ℕ) → 
-           (suc (c1 n i) ≡ c1 n (suc i) → Is A C (λ i → g (f i)) (g (f (fun← an i))) )
-         ∧ (Is A C (λ i → g (f i)) (g (f (fun← an i)))  → suc (c1 n i) ≡ c1 n (suc i) )
-    c1-at-i = ?
+           (suc (c1 n i) ≡ c1 n (suc i) →  fun→ cn (g (f (fun← an n))) ≡ suc i)
+         ∧ ( (fun→ cn (g (f (fun← an n))) ≡ suc i)  → suc (c1 n i) ≡ c1 n (suc i) )
+    c1-at-i 0 i 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₁ = ⟪ ( λ () ) , (λ eq → ⊥-elim (nat-≡< eq (<-trans a a<sa)))  ⟫ 
+    ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = ⟪ ( λ () ) , (λ eq → ⊥-elim (nat-≡< eq (<-trans a a<sa)))  ⟫ 
+    ... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c₁ = ⟪ ( λ () ) , (λ eq → ⊥-elim (nat-≡< eq (<-trans a a<sa)))  ⟫ 
+    ... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ = ⟪ ( λ () ) , (λ eq → ⊥-elim ( ¬b eq ))  ⟫ 
+    ... | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ = ⟪ ( λ () ) , (λ eq → ⊥-elim (nat-≡< (sym b) (subst (λ k → i < k) (sym b₁) a<sa) ))  ⟫ 
+    ... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c₁ = ⟪ ( λ () ) , (λ eq → ⊥-elim ( ¬b eq ))  ⟫ 
+    ... | tri> ¬a ¬b c₁ | tri< (s≤s a) ¬b₁ ¬c = ⊥-elim (nat-≡< refl (≤-trans c₁ a))
+    ... | tri> ¬a ¬b c₁ | tri≈ ¬a₁ b ¬c = ⟪ ( λ _ → b ) , ( λ _ → refl ) ⟫
+    ... | tri> ¬a ¬b c₁ | tri> ¬a₁ ¬b₁ c₂ = ⟪ ( λ () ) , ( λ eq → ⊥-elim (¬b₁ eq )) ⟫
+    c1-at-i (suc n) zero with <-cmp (fun→ cn (g (f (fun← an (suc n))))) zero | <-cmp (fun→ cn (g (f (fun← an (suc n))))) (suc zero)
+    ... | s | t = ?
+    c1-at-i (suc n) (suc i) with  <-cmp (fun→ cn (g (f (fun← an (suc n))))) (suc i) | <-cmp (fun→ cn (g (f (fun← an (suc n))))) (suc (suc i)) 
+    ... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = ⟪ ?  , (λ eq → ⊥-elim ( ¬b₁ eq)) ⟫ where   
+        -- a (suc n) is less than (suc i) → c1 (suc n) (suc (suc i)) ≡ c1 (suc n) (suc i)
+        lemc00 : ¬ ( suc (suc (c1 n (suc i))) ≡ suc (c1 n (suc (suc i))) )
+        lemc00 = ?
+    ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = ?
+    ... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c₁ = ?
+    ... | tri≈ ¬a b ¬c | t = ?
+    ... | tri> ¬a ¬b c₁ | t = ?
+
     -- 
     -- c n < i means j < suc n → fun← an j < c n, we cannot have more else
     --    ∃ j → j < suc n → c n < fun← an j