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

changeset 1341:49e5a4d8c958

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
... simple c1
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 16 Jun 2023 21:39:50 +0900
parents 4c32cd3b84c2
children 884f5fcd41dc
files src/bijection.agda
diffstat 1 files changed, 47 insertions(+), 86 deletions(-) [+]
line wrap: on
line diff
--- a/src/bijection.agda	Fri Jun 16 20:45:28 2023 +0900
+++ b/src/bijection.agda	Fri Jun 16 21:39:50 2023 +0900
@@ -41,10 +41,10 @@
 bi-sym : {n m : Level} (R : Set n) (S : Set m) → Bijection R S →  Bijection S R
 bi-sym R S eq = record {  fun← =  fun→ eq ; fun→  = fun← eq  ; fiso← =  fiso→ eq ;  fiso→ =  fiso← eq }
 
-bi-inject← : {n m : Level} {R : Set n} {S : Set m} → (rs : Bijection R S) → {x y : S} → fun← rs x ≡ fun← rs y → x ≡ y 
+bi-inject← : {n m : Level} {R : Set n} {S : Set m} → (rs : Bijection R S) → {x y : S} → fun← rs x ≡ fun← rs y → x ≡ y
 bi-inject← rs {x} {y} eq = subst₂ (λ j k → j ≡ k ) (fiso→  rs _) (fiso→ rs _) (cong (fun→ rs) eq)
 
-bi-inject→ : {n m : Level} {R : Set n} {S : Set m} → (rs : Bijection R S) → {x y : R} → fun→ rs x ≡ fun→ rs y → x ≡ y 
+bi-inject→ : {n m : Level} {R : Set n} {S : Set m} → (rs : Bijection R S) → {x y : R} → fun→ rs x ≡ fun→ rs y → x ≡ y
 bi-inject→ rs {x} {y} eq = subst₂ (λ j k → j ≡ k ) (fiso←  rs _) (fiso← rs _) (cong (fun← rs) eq)
 
 open import Relation.Binary.Structures
@@ -489,8 +489,8 @@
 open import Relation.Nullary.Decidable hiding (⌊_⌋)
 open import Data.Unit.Base using (⊤ ; tt)
 open import Data.List.Fresh hiding ([_])
-open import Data.List.Fresh.Relation.Unary.Any 
-open import Data.List.Fresh.Relation.Unary.All 
+open import Data.List.Fresh.Relation.Unary.Any
+open import Data.List.Fresh.Relation.Unary.All
 
 record InjectiveF (A B : Set) : Set where
    field
@@ -526,7 +526,7 @@
     --     if we have a , number a of A is larger than the numner of B C, so we have the inverse
     --
 
-    count-B : ℕ → ℕ 
+    count-B : ℕ → ℕ
     count-B zero with is-B (fun← cn zero)
     ... | yes isb = 1
     ... | no nisb = 0
@@ -537,7 +537,7 @@
     bton : B → ℕ
     bton b = count-B (fun→ cn (g b))
 
-    count-A : ℕ → ℕ 
+    count-A : ℕ → ℕ
     count-A zero with is-A (fun← cn zero)
     ... | yes isb = 1
     ... | no nisb = 0
@@ -551,7 +551,7 @@
     ... | case2 i<j = lem00 _ _ i<j where
          lem00 : (i j : ℕ) → i < j → count-A i ≤ count-A j
          lem00 i (suc j) (s≤s i<j) = ≤-trans (count-A-mono i<j) (lem01 j) where
-             lem01 : (j : ℕ) → count-A j ≤ count-A (suc j) 
+             lem01 : (j : ℕ) → count-A j ≤ count-A (suc j)
              lem01 zero with is-A (fun← cn (suc zero))
              ... | yes isb = refl-≤s
              ... | no nisb = ≤-refl
@@ -567,7 +567,7 @@
     ... | yes isa | record { eq = eq1 } = s≤s ( count-A<i i )
     ... | no nisa | record { eq = eq1 } = ≤-trans (count-A<i i ) refl-≤s
 
-    full-a : (i : ℕ) → i < count-A i → Is A C (λ x → g (f x)) (fun← cn i) 
+    full-a : (i : ℕ) → i < count-A i → Is A C (λ x → g (f x)) (fun← cn i)
     full-a zero i<ci with is-A (fun← cn  zero) | inspect ( count-A ) zero
     ... | yes isa | record { eq = eq1 } = isa
     ... | no nisa | record { eq = eq1 } = ⊥-elim ( nat-≡< refl i<ci )
@@ -589,25 +589,25 @@
 
     ca≤cb0 : (n : ℕ) → count-A n ≤ count-B n
     ca≤cb0 zero with is-A (fun← cn zero) | is-B (fun← cn zero)
-    ... | yes isA | yes isB = ≤-refl 
+    ... | yes isA | yes isB = ≤-refl
     ... | yes isA | no nisB = ⊥-elim ( ¬isA∧isB _ isA nisB )
-    ... | no nisA | yes isB = px≤x  
-    ... | no nisA | no nisB = ≤-refl 
+    ... | no nisA | yes isB = px≤x
+    ... | no nisA | no nisB = ≤-refl
     ca≤cb0 (suc n) with is-A (fun← cn (suc n)) | is-B (fun← cn (suc n))
     ... | yes isA | yes isB = s≤s (ca≤cb0 n)
     ... | yes isA | no nisB = ⊥-elim ( ¬isA∧isB _ isA nisB )
     ... | no nisA | yes isB = ≤-trans (ca≤cb0 n) px≤x
     ... | no nisA | no nisB = ca≤cb0 n
 
-    --  (c n)  is 
+    --  (c n)  is
     --     fun→ c, where c contains all "a" less than n
     --     (i n : ℕ) → i < suc n → fun→ cn (g (f (fun← an i))) < suc (c n)
-    c : (n : ℕ) → ℕ 
+    c : (n : ℕ) → ℕ
     c zero = fun→ cn (g (f (fun← an zero)))
     c (suc n) = max (fun→ cn (g (f (fun← an (suc n))))) (c n)
 
     c< : (i n : ℕ) → i < suc n → fun→ cn (g (f (fun← an i))) < suc (c n)
-    c< zero zero (s≤s z≤n) = a<sa 
+    c< zero zero (s≤s z≤n) = a<sa
     c< (suc i) zero  (s≤s ())
     c< zero (suc n) (s≤s z≤n) = ≤-trans (c< zero n (<-transʳ  z≤n a<sa) ) (s≤s (y≤max (fun→ cn (g (f (fun← an (suc n))))) (c n)))
     c< (i @ (suc _)) (suc n) i≤n with ≤-∨ i≤n
@@ -617,17 +617,17 @@
     --  (c1 n i) is number of a which fun← an a ≤ n ∧ fun→ cn (g (f a)) < i ∧ g (f a) is A
 
     c1 : (n i : ℕ) → ℕ
-    c1 zero i with <-cmp (fun→ cn (g (f (fun← an zero)))) i 
+    c1 zero i with <-cmp (fun→ cn (g (f (fun← an zero)))) i
     ... | tri< a ¬b ¬c = 1
     ... | tri≈ ¬a b ¬c = 1
     ... | tri> ¬a ¬b c₁ = 0
-    c1 (suc n) i with <-cmp (fun→ cn (g (f (fun← an (suc n))))) i 
+    c1 (suc n) i with <-cmp (fun→ cn (g (f (fun← an (suc n))))) i
     ... | tri< a ¬b ¬c = suc (c1 n i)
     ... | tri≈ ¬a b ¬c = suc (c1 n i)
     ... | tri> ¬a ¬b c₁ = c1 n i
 
     c1-mono : {n i j : ℕ} → i ≤ j  → (c1 n i ≡ c1 n j) ∨ (c1 n i < c1 n j)
-    c1-mono {zero} {i} {j} le with <-cmp (fun→ cn (g (f (fun← an zero)))) i  | <-cmp (fun→ cn (g (f (fun← an zero)))) j  
+    c1-mono {zero} {i} {j} le with <-cmp (fun→ cn (g (f (fun← an zero)))) i  | <-cmp (fun→ cn (g (f (fun← an zero)))) j
     ... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = case1 refl
     ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = case1 refl
     ... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c₁ = ⊥-elim ( nat-≤> le (<-trans c₁ a) )
@@ -638,7 +638,7 @@
     ... | tri> ¬a ¬b c₁ | tri≈ ¬a₁ b ¬c = case2 ≤-refl
     ... | tri> ¬a ¬b c₁ | tri> ¬a₁ ¬b₁ c₂ = case1 refl
     c1-mono {suc n} {zero} {zero} z≤n = case1 refl
-    c1-mono {suc n} {zero} {suc j} z≤n with <-cmp (fun→ cn (g (f (fun← an (suc n))))) zero  | <-cmp (fun→ cn (g (f (fun← an (suc n))))) (suc j)  
+    c1-mono {suc n} {zero} {suc j} z≤n with <-cmp (fun→ cn (g (f (fun← an (suc n))))) zero  | <-cmp (fun→ cn (g (f (fun← an (suc n))))) (suc j)
         | c1-mono {n} {zero} {suc j} z≤n
     ... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ | case1 eq = case1 (cong suc eq)
     ... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ | case2 le = case2 ( s≤s le )
@@ -646,12 +646,12 @@
     ... | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ | case2 le = case2 ( s≤s le )
     ... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c₁ | _ = ⊥-elim ( nat-≡< (sym b) (≤-trans (s≤s z≤n) c₁)  )
     ... | tri> ¬a ¬b c₁ | tri< a ¬b₁ ¬c | case1 eq = case2 ( subst (λ k → suc (c1 n zero) ≤ k ) (cong suc eq) ≤-refl )
-    ... | tri> ¬a ¬b c₁ | tri< a ¬b₁ ¬c | case2 le = case2 (≤-trans le refl-≤s ) 
+    ... | tri> ¬a ¬b c₁ | tri< a ¬b₁ ¬c | case2 le = case2 (≤-trans le refl-≤s )
     ... | tri> ¬a ¬b c₁ | tri≈ ¬a₁ b ¬c | case1 eq = case2 ( subst (λ k → suc (c1 n zero) ≤ k ) (cong suc eq) ≤-refl )
-    ... | tri> ¬a ¬b c₁ | tri≈ ¬a₁ b ¬c | case2 le = case2 (≤-trans le refl-≤s ) 
+    ... | tri> ¬a ¬b c₁ | tri≈ ¬a₁ b ¬c | case2 le = case2 (≤-trans le refl-≤s )
     ... | tri> ¬a ¬b c₁ | tri> ¬a₁ ¬b₁ c₂ | case1 eq = case1 eq
     ... | tri> ¬a ¬b c₁ | tri> ¬a₁ ¬b₁ c₂ | case2 le = case2 le
-    c1-mono {suc n} {suc i} {suc j} (s≤s le) with <-cmp (fun→ cn (g (f (fun← an (suc n))))) (suc i) | <-cmp (fun→ cn (g (f (fun← an (suc n))))) (suc j)   
+    c1-mono {suc n} {suc i} {suc j} (s≤s le) with <-cmp (fun→ cn (g (f (fun← an (suc n))))) (suc i) | <-cmp (fun→ cn (g (f (fun← an (suc n))))) (suc j)
          | c1-mono {n} {suc i} {suc j} (s≤s le)
     ... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ | case1 eq = case1 (cong suc eq)
     ... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ | case2 le = case2 (s≤s le)
@@ -659,70 +659,31 @@
     ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ | case2 le = case2 (s≤s le)
     ... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c₁ | u = ⊥-elim ( nat-≤> (s≤s le) (<-transˡ c₁ (≤-trans refl-≤s a ) ))
     ... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ | case1 eq = case1 (cong suc eq)
-    ... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ | case2 le = case2 (s≤s le) 
+    ... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ | case2 le = case2 (s≤s le)
     ... | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ | case1 eq = case1 (cong suc eq)
-    ... | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ | case2 le = case2 (s≤s le) 
+    ... | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ | case2 le = case2 (s≤s le)
     ... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c₁ | u = ⊥-elim ( nat-≤> (subst (λ k → k ≤ _) (sym b) (s≤s le)) c₁  )
     ... | tri> ¬a ¬b c₁ | tri< a ¬b₁ ¬c | case1 eq = case2 ( subst (λ k → suc (c1 n (suc i)) ≤ k ) (cong suc eq) ≤-refl )
-    ... | tri> ¬a ¬b c₁ | tri< a ¬b₁ ¬c | case2 le = case2 (≤-trans le refl-≤s ) 
+    ... | tri> ¬a ¬b c₁ | tri< a ¬b₁ ¬c | case2 le = case2 (≤-trans le refl-≤s )
     ... | tri> ¬a ¬b c₁ | tri≈ ¬a₁ b ¬c | case1 eq = case2 ( subst (λ k → suc (c1 n (suc i)) ≤ k ) (cong suc eq) ≤-refl )
-    ... | tri> ¬a ¬b c₁ | tri≈ ¬a₁ b ¬c | case2 le = case2 (≤-trans le refl-≤s ) 
+    ... | tri> ¬a ¬b c₁ | tri≈ ¬a₁ b ¬c | case2 le = case2 (≤-trans le refl-≤s )
     ... | tri> ¬a ¬b c₁ | tri> ¬a₁ ¬b₁ c₂ | u = u
 
-    record An (n i : ℕ) : Set where
-        field
-          ai : ℕ
-          ai<n : ai ≤ n
-          cn=n : fun→ cn (g (f (fun← an ai))) ≡ suc i
-        cn=a0 : n ≡ 0 → fun→ cn (g (f (fun← an 0))) ≡ suc i
-        cn=a0 n=0 with <-cmp ai n
-        ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> a (subst (λ k → k < suc ai) (sym n=0) (s≤s z≤n)  ))
-        ... | tri≈ ¬a b ¬c = subst (λ k → fun→ cn (g (f (fun← an k))) ≡ suc i) (trans b n=0) cn=n
-        ... | tri> ¬a ¬b c₁ = ⊥-elim ( nat-≤> c₁ (<-transʳ ai<n a<sa) )
-
-    c1-at-i : (n i : ℕ) → 
-           (suc (c1 n i) ≡ c1 n (suc i) →  An n i)                             
-         ∧ ( An n 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-≡< (An.cn=a0 eq refl) (<-trans a a<sa)))  ⟫ 
-    ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = ⟪ ( λ () ) , (λ eq → ⊥-elim (nat-≡< (An.cn=a0 eq refl) (<-trans a a<sa)))  ⟫ 
-    ... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c₁ = ⟪ ( λ () ) , (λ eq → ⊥-elim (nat-≡< (An.cn=a0 eq refl) (<-trans a a<sa)))  ⟫ 
-    ... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ = ⟪ ( λ () ) , (λ eq → ⊥-elim ( ¬b (An.cn=a0 eq refl) ))  ⟫ 
-    ... | 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 (An.cn=a0 eq refl) ))  ⟫ 
-    ... | tri> ¬a ¬b c₁ | tri< (s≤s a) ¬b₁ ¬c = ⊥-elim (nat-≡< refl (≤-trans c₁ a))
-    ... | tri> ¬a ¬b c₁ | tri≈ ¬a₁ b ¬c = ⟪ ( λ eq → record { ai = 0 ; ai<n = z≤n ; cn=n = b } ) , ( λ _ → refl ) ⟫
-    ... | tri> ¬a ¬b c₁ | tri> ¬a₁ ¬b₁ c₂ = ⟪ ( λ () ) , ( λ eq → ⊥-elim (¬b₁ (An.cn=a0 eq refl) )) ⟫
-    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₁ ? )) ⟫ 
-
-    -- 
+    --
     -- 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
-    -- 
-    c1-max : (n i : ℕ) → c n < i → c1 n i ≡ c1 n (suc i)
-    c1-max zero zero ()
-    c1-max zero (suc i) (s≤s c0<i) with <-cmp (fun→ cn (g (f (fun← an zero)))) (suc i)
-    ---     we only have one (fun← an zero), it is in c1 zero (suc i) ≡ c1 zero i ≡ 1
-    ... | tri≈ ¬a b ¬c = ? where
-          lem00 : c1 zero i ≡ c1 zero (suc i)
-          lem00 = c1-max zero i ?
-    ... | tri> ¬a ¬b c = ?
-    ... | tri< a ¬b ¬c with is-A (g (f (fun← an zero)))
-    ... | yes _ = ?
-    ... | no _  = ?
-    c1-max (suc n) zero ()
-    c1-max (suc n) (suc i) cn<i with <-cmp (fun→ cn (g (f (fun← an (suc n))))) (suc i)
-    ---     we already have all j < suc n → (fun← an j), it is in c1 (suc n) (suc i) ≡ c1 (suc n) i ≡ suc n
-    ... | tri≈ ¬a b ¬c = ? -- c1-max n i ?
-    ... | tri> ¬a ¬b c = ? -- c1-max n i ?
-    ... | tri< a ¬b ¬c with is-A (g (f (fun← an (suc n))))
-    ... | yes _ = ? -- cong suc (c1-max n i ?)
-    ... | no _  = ? --      c1-max n i ?
+    --
+    c1-max : (n i : ℕ) → c n < i → c1 n i ≡ suc n
+    c1-max zero i cn<i with <-cmp (fun→ cn (g (f (fun← an zero)))) i
+    ... | tri< a ¬b ¬c = refl
+    ... | tri≈ ¬a b ¬c = refl
+    ... | tri> ¬a ¬b c₁ = ?
+    c1-max (suc n) i cn<i with <-cmp (fun→ cn (g (f (fun← an (suc n))))) i
+    ... | tri< a ¬b ¬c = cong suc (c1-max n i ? )
+    ... | tri≈ ¬a b ¬c = cong suc (c1-max n i ? )
+    ... | tri> ¬a ¬b c₁ = ?
 
-    --- c1 n i 
+    --- c1 n i
     c1+1 : (n i : ℕ) → i < c n → Is A C (λ i → g (f i)) (g (f (fun← an i))) → suc (c1 n i) ≡ c1 n (suc i)
     c1+1 zero i i<c0 isa = c1+10 where
         c1+10 : suc (c1 zero i) ≡ c1 zero (suc i)
@@ -764,7 +725,7 @@
     --    0 < suc (count-A (c 0)) ≡  count-A (suc (c 0)) ≤ count-A (c 1) < ... < suc (count-A (c n)) ≤ count-A (c n)
     --    0 < cm  →          1 < cm                                                → n < cm
     -- it means
-    --    n < count-A (c n) 
+    --    n < count-A (c n)
     --
 
     cl07 : { i j : ℕ } → suc i < suc j → i < j
@@ -772,8 +733,8 @@
 
     lem02 : (n : ℕ) → maxAC n
     lem02 n = record { ac = c n ; n<ca = n<ca n } where
-         ca+1 : (i : ℕ) → i < fun→ cn (g (f (fun← an i))) → count-A i < count-A (fun→ cn (g (f (fun← an i)))) 
-         ca+1 i i<ca with fun→ cn (g (f (fun← an i))) | inspect (fun→ cn) (g (f (fun← an i))) 
+         ca+1 : (i : ℕ) → i < fun→ cn (g (f (fun← an i))) → count-A i < count-A (fun→ cn (g (f (fun← an i))))
+         ca+1 i i<ca with fun→ cn (g (f (fun← an i))) | inspect (fun→ cn) (g (f (fun← an i)))
          ... | suc ca | record { eq = eq1 } with is-A (fun← cn (suc ca))
          ... | yes isa = <-transʳ ( count-A-mono (px≤py i<ca)) cl22 where
              cl22 :  count-A (pred (suc ca)) < suc (count-A ca)
@@ -784,19 +745,19 @@
                 g (f ( fun← an i)) ≡⟨ sym (fiso← cn _)  ⟩
                 fun← cn (fun→ cn (g (f ( fun← an i)))) ≡⟨ cong (fun← cn) eq1 ⟩
                 fun← cn (suc ca) ∎ where open ≡-Reasoning
-         n<ca : (n : ℕ ) → n < count-A (c n) 
-         n<ca zero with fun→ cn (g (f (fun← an zero))) | inspect (fun→ cn) (g (f (fun← an zero))) 
+         n<ca : (n : ℕ ) → n < count-A (c n)
+         n<ca zero with fun→ cn (g (f (fun← an zero))) | inspect (fun→ cn) (g (f (fun← an zero)))
          ... | zero | record { eq = eq1 } = cl23 where
              cl23 : 1 ≤ count-A zero
              cl23 = ?
          ... | suc ca | record { eq = eq1 } = cl24 where
              cl24 : 1 ≤ count-A (suc ca)
              cl24 = ?
-         n<ca (suc n) with <-cmp (c n) (fun→ cn (g (f (fun← an (suc n))))) 
+         n<ca (suc n) with <-cmp (c n) (fun→ cn (g (f (fun← an (suc n)))))
          ... | tri< ca<an ¬b ¬c = ? where
              cl26 : n < count-A (c n)
-             cl26 = n<ca n 
-             cl25 : suc (suc n) ≤ count-A (fun→ cn (g (f (fun← an (suc n))))) 
+             cl26 = n<ca n
+             cl25 : suc (suc n) ≤ count-A (fun→ cn (g (f (fun← an (suc n)))))
              cl25 = begin
                  suc (suc n) ≤⟨ s≤s (n<ca n) ⟩
                  suc (count-A (c n)) ≤⟨ s≤s (count-A-mono ( sx≤py→x≤y  ( begin
@@ -812,7 +773,7 @@
              cl25 = ?
              cl27 : fun→ cn (g (f (fun← an (suc n) )) )  < c (suc n)
              cl27 = ?
-             cl26 : fun→ cn (g (f (fun← an ? ))  )  < fun→ cn (g (f (fun← an (suc n)))) 
+             cl26 : fun→ cn (g (f (fun← an ? ))  )  < fun→ cn (g (f (fun← an (suc n))))
              cl26 = ?
              --
              --  count-A (c m)                                                           < count (c (suc m))           ≤ count (c n)
@@ -845,7 +806,7 @@
     ntob n = CountB.b (lem01 n (maxAC.ac (lem02 n)) (≤-trans (maxAC.n<ca (lem02 n)) (ca≤cb0 (maxAC.ac (lem02 n))) ))
 
     biso : (n : ℕ) → bton (ntob n) ≡ n
-    biso n = ? -- lem03 _ (≤-trans (maxAC.n<ca (lem02 n )) ?) refl 
+    biso n = ? -- lem03 _ (≤-trans (maxAC.n<ca (lem02 n )) ?) refl
 
     biso1 : (b : B) → ntob (bton b) ≡ b
     biso1 b = ?