# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1686215895 -32400
# Node ID 4ad33efd8486e57e4aa16bfb7a7fddfb4f7ae8f8
# Parent  81f66cec617ea2f492dd83f35fd0e17b9c985223
...

diff -r 81f66cec617e -r 4ad33efd8486 src/bijection.agda
--- a/src/bijection.agda	Thu Jun 08 11:21:20 2023 +0900
+++ b/src/bijection.agda	Thu Jun 08 18:18:15 2023 +0900
@@ -557,29 +557,20 @@
     cbn : ℕ → ℕ
     cbn n = fun→ cn (g (f (fun← an n)))
 
-    cbn-mono1 : {i : ℕ} → cbn i < cbn (suc i)
-    cbn-mono1 {i} with cbn i | inspect cbn i | lb (cbn i) 
-    ... | zero | record {eq = eq1 } | s with is-A (fun← cn (cbn i)) | is-B (fun← cn (cbn i))
-    ... | yes isA | yes isB = ?
-    ... | yes isA | no nisB = ⊥-elim ( ¬isA∧isB _ isA nisB )
-    ... | no nisA | yes isB = ⊥-elim ( nisA record { a = fun← an i ; fa=c = trans (sym (fiso← cn _)) ( cong (fun← cn)  refl  )   } )
-    ... | no nisA | no nisB = ⊥-elim ( nisA record { a = fun← an i ; fa=c = trans (sym (fiso← cn _)) ( cong (fun← cn)  refl  )   } )
-    cbn-mono1 {i} | suc t | record {eq = eq1 } | s with is-A (fun← cn (suc t)) | is-B (fun← cn (suc t))
-    ... | yes isA | yes isB = ? -- <-transʳ z≤n ≤-refl 
-    ... | yes isA | no nisB = ⊥-elim ( ¬isA∧isB _ isA nisB )
-    ... | no nisA | yes isB = ⊥-elim ( nisA record { a = fun← an i ; fa=c = trans (sym (fiso← cn _)) ( cong (fun← cn)  eq1 )   } )
-    ... | no nisA | no nisB = ⊥-elim ( nisA record { a = fun← an i ; fa=c = trans (sym (fiso← cn _)) ( cong (fun← cn)  eq1 )   } )
-
-    cbn-mono : {i j : ℕ} → i < j → cbn i < cbn j
-    cbn-mono {i} {suc j} (s≤s i≤j) with <-∨ {i} {j} (<-transʳ i≤j a<sa )
-    ... | case1 refl = cbn-mono1
-    ... | case2 lt = <-trans (cbn-mono {i} {j} lt) cbn-mono1
-
     cb< : (n : ℕ) → CB.cb (lb (cbn n)) < CB.cb (lb (cbn (suc n)))
-    cb< n = cb00 _ _ _ refl refl   where
-        cb00 : (n i j : ℕ) → i ≡ cbn n → j ≡ cbn (suc n)  → CB.cb (lb i) < CB.cb (lb j)
-        cb00 zero i j eq eq1 = ?
-        cb00 (suc n) i j eq eq1 = <-trans (cb00 n i j ? ?  ) ?
+    cb< n = ? where
+        cb00 : (i : ℕ) → i ≤ CB.cb (lb (cbn (suc n))) → CB.cb (lb (cbn n)) < CB.cb (lb (cbn (suc n)))
+        cb00 i i≤csn with inspect cbn (suc n) | lb (cbn (suc n)) 
+        cb00 zero lt | record {eq = eq1 } | s with is-A (fun← cn (cbn 0)) | is-B (fun← cn (cbn 0))
+        ... | yes isA | yes isB = ?
+        ... | yes isA | no nisB = ⊥-elim ( ¬isA∧isB _ isA nisB )
+        ... | no nisA | yes isB = ⊥-elim ( nisA record { a = fun← an 0 ; fa=c = trans (sym (fiso← cn _)) ( cong (fun← cn)  refl )   } )
+        ... | no nisA | no nisB = ⊥-elim ( nisA record { a = fun← an 0 ; fa=c = trans (sym (fiso← cn _)) ( cong (fun← cn)  refl )   } )
+        cb00 (suc c) lt | record {eq = eq1 } | s with is-A (fun← cn (suc c)) | is-B (fun← cn (suc c))
+        ... | yes isA | yes isB = ? -- <-transʳ z≤n ≤-refl 
+        ... | yes isA | no nisB = ⊥-elim ( ¬isA∧isB _ isA nisB )
+        ... | no nisA | yes isB = ⊥-elim ( nisA record { a = fun← an (suc n) ; fa=c = trans (sym (fiso← cn _)) ( cong (fun← cn)  ? )   } )
+        ... | no nisA | no nisB = ⊥-elim ( nisA record { a = fun← an (suc n) ; fa=c = trans (sym (fiso← cn _)) ( cong (fun← cn)  ? )   } )
 
     cb<0 : 0 < CB.cb (lb (cbn 0))
     cb<0 with cbn 0 | inspect cbn 0