Mercurial > hg > Members > kono > Proof > automaton

comparison automaton-in-agda/src/bijection.agda @ 403:c298981108c1

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix for std-lib 2.0
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 24 Sep 2023 11:32:01 +0900
parents 78e094559ceb
children
comparison
equal deleted inserted replaced
402:093e386c10a2 403:c298981108c1
1 {-# OPTIONS --allow-unsolved-metas #-} 1 {-# OPTIONS --cubical-compatible --safe #-}
2 2
3 module bijection where 3 module bijection where
4 4
5 5
6 open import Level renaming ( zero to Zero ; suc to Suc ) 6 open import Level renaming ( zero to Zero ; suc to Suc )
215 -- 215 --
216 -- create the invariant NN for all n 216 -- create the invariant NN for all n
217 -- 217 --
218 nn zero = record { j = 0 ; k = 0 ; k1 = refl 218 nn zero = record { j = 0 ; k = 0 ; k1 = refl
219 ; nn-unique = λ {j0} {k0} eq → cong₂ (λ x y → ⟪ x , y ⟫) (sym (proj1 (nxn→n0 eq))) (sym (proj2 (nxn→n0 {j0} {k0} eq))) } 219 ; nn-unique = λ {j0} {k0} eq → cong₂ (λ x y → ⟪ x , y ⟫) (sym (proj1 (nxn→n0 eq))) (sym (proj2 (nxn→n0 {j0} {k0} eq))) }
220 nn (suc i) with NN.k (nn i) | inspect NN.k (nn i) 220 nn (suc i) with NN.k (nn i) in eq
221 ... | zero | record { eq = eq } = record { k = suc (sum ) ; j = 0 221 ... | zero = record { k = suc (sum ) ; j = 0
222 ; k1 = nn02 ; nn-unique = nn04 } where 222 ; k1 = nn02 ; nn-unique = nn04 } where
223 --- 223 ---
224 --- increment the stage 224 --- increment the stage
225 --- 225 ---
226 sum = NN.j (nn i) + NN.k (nn i) 226 sum = NN.j (nn i) + NN.k (nn i)
260 nxn→n (suc j0) k0 ≡⟨ eq1 ⟩ 260 nxn→n (suc j0) k0 ≡⟨ eq1 ⟩
261 suc i ∎ ) ⟩ 261 suc i ∎ ) ⟩
262 i ∎ where open ≡-Reasoning 262 i ∎ where open ≡-Reasoning
263 nn06 : nxn→n j0 (suc k0) ≡ i → ⟪ NN.j (nn i) , NN.k (nn i) ⟫ ≡ ⟪ j0 , suc k0 ⟫ 263 nn06 : nxn→n j0 (suc k0) ≡ i → ⟪ NN.j (nn i) , NN.k (nn i) ⟫ ≡ ⟪ j0 , suc k0 ⟫
264 nn06 = NN.nn-unique (nn i) 264 nn06 = NN.nn-unique (nn i)
265 ... | suc k | record {eq = eq} = record { k = k ; j = suc (NN.j (nn i)) ; k1 = nn11 ; nn-unique = nn13 } where 265 ... | suc k = record { k = k ; j = suc (NN.j (nn i)) ; k1 = nn11 ; nn-unique = nn13 } where
266 --- 266 ---
267 --- increment in a stage 267 --- increment in a stage
268 --- 268 ---
269 sum = NN.j (nn i) + NN.k (nn i) 269 sum = NN.j (nn i) + NN.k (nn i)
270 stage = minus i (NN.j (nn i)) 270 stage = minus i (NN.j (nn i))
436 436
437 lb : (n : ℕ) → LB n lton 437 lb : (n : ℕ) → LB n lton
438 lb zero = record { nlist = [] ; isBin = refl ; isUnique = lb05 } where 438 lb zero = record { nlist = [] ; isBin = refl ; isUnique = lb05 } where
439 lb05 : (x : List Bool) → lton x ≡ zero → [] ≡ x 439 lb05 : (x : List Bool) → lton x ≡ zero → [] ≡ x
440 lb05 x eq = lb=b [] x (sym eq) 440 lb05 x eq = lb=b [] x (sym eq)
441 lb (suc n) with LB.nlist (lb n) | inspect LB.nlist (lb n) 441 lb (suc n) with LB.nlist (lb n) in eq
442 ... | [] | record { eq = eq } = record { nlist = false ∷ [] ; isUnique = lb06 ; isBin = lb10 } where 442 ... | [] = record { nlist = false ∷ [] ; isUnique = lb06 ; isBin = lb10 } where
443 open ≡-Reasoning 443 open ≡-Reasoning
444 lb10 : lton1 (false ∷ []) ∸ 1 ≡ suc n 444 lb10 : lton1 (false ∷ []) ∸ 1 ≡ suc n
445 lb10 = begin 445 lb10 = begin
446 lton (false ∷ []) ≡⟨ refl ⟩ 446 lton (false ∷ []) ≡⟨ refl ⟩
447 suc 0 ≡⟨ refl ⟩ 447 suc 0 ≡⟨ refl ⟩
448 suc (lton []) ≡⟨ cong (λ k → suc (lton k)) (sym eq) ⟩ 448 suc (lton []) ≡⟨ cong (λ k → suc (lton k)) (sym eq) ⟩
449 suc (lton (LB.nlist (lb n))) ≡⟨ cong suc (LB.isBin (lb n) ) ⟩ 449 suc (lton (LB.nlist (lb n))) ≡⟨ cong suc (LB.isBin (lb n) ) ⟩
450 suc n ∎ 450 suc n ∎
451 lb06 : (x : List Bool) → pred (lton1 x ) ≡ suc n → false ∷ [] ≡ x 451 lb06 : (x : List Bool) → pred (lton1 x ) ≡ suc n → false ∷ [] ≡ x
452 lb06 x eq1 = lb=b (false ∷ []) x (trans lb10 (sym eq1)) -- lton (false ∷ []) ≡ lton x 452 lb06 x eq1 = lb=b (false ∷ []) x (trans lb10 (sym eq1)) -- lton (false ∷ []) ≡ lton x
453 ... | false ∷ t | record { eq = eq } = record { nlist = true ∷ t ; isBin = lb01 ; isUnique = lb09 } where 453 ... | false ∷ t = record { nlist = true ∷ t ; isBin = lb01 ; isUnique = lb09 } where
454 lb01 : lton (true ∷ t) ≡ suc n 454 lb01 : lton (true ∷ t) ≡ suc n
455 lb01 = begin 455 lb01 = begin
456 lton (true ∷ t) ≡⟨ refl ⟩ 456 lton (true ∷ t) ≡⟨ refl ⟩
457 lton1 t + lton1 t ≡⟨ sym ( sucprd (2lton1>0 t) ) ⟩ 457 lton1 t + lton1 t ≡⟨ sym ( sucprd (2lton1>0 t) ) ⟩
458 suc (pred (lton1 t + lton1 t )) ≡⟨ refl ⟩ 458 suc (pred (lton1 t + lton1 t )) ≡⟨ refl ⟩
459 suc (lton (false ∷ t)) ≡⟨ cong (λ k → suc (lton k )) (sym eq) ⟩ 459 suc (lton (false ∷ t)) ≡⟨ cong (λ k → suc (lton k )) (sym eq) ⟩
460 suc (lton (LB.nlist (lb n))) ≡⟨ cong suc (LB.isBin (lb n)) ⟩ 460 suc (lton (LB.nlist (lb n))) ≡⟨ cong suc (LB.isBin (lb n)) ⟩
461 suc n ∎ where open ≡-Reasoning 461 suc n ∎ where open ≡-Reasoning
462 lb09 : (x : List Bool) → lton1 x ∸ 1 ≡ suc n → true ∷ t ≡ x 462 lb09 : (x : List Bool) → lton1 x ∸ 1 ≡ suc n → true ∷ t ≡ x
463 lb09 x eq1 = lb=b (true ∷ t) x (trans lb01 (sym eq1) ) -- lton (true ∷ t) ≡ lton x 463 lb09 x eq1 = lb=b (true ∷ t) x (trans lb01 (sym eq1) ) -- lton (true ∷ t) ≡ lton x
464 ... | true ∷ t | record { eq = eq } = record { nlist = lb+1 (true ∷ t) ; isBin = lb02 (true ∷ t) lb03 ; isUnique = lb07 } where 464 ... | true ∷ t = record { nlist = lb+1 (true ∷ t) ; isBin = lb02 (true ∷ t) lb03 ; isUnique = lb07 } where
465 lb03 : lton (true ∷ t) ≡ n 465 lb03 : lton (true ∷ t) ≡ n
466 lb03 = begin 466 lb03 = begin
467 lton (true ∷ t) ≡⟨ cong (λ k → lton k ) (sym eq ) ⟩ 467 lton (true ∷ t) ≡⟨ cong (λ k → lton k ) (sym eq ) ⟩
468 lton (LB.nlist (lb n)) ≡⟨ LB.isBin (lb n) ⟩ 468 lton (LB.nlist (lb n)) ≡⟨ LB.isBin (lb n) ⟩
469 n ∎ where open ≡-Reasoning 469 n ∎ where open ≡-Reasoning
755 -- injection of count-B 755 -- injection of count-B
756 --- 756 ---
757 lem06 : (i j : ℕ ) → Is B C g (fun← cn i) → Is B C g (fun← cn j) → count-B i ≡ count-B j → i ≡ j 757 lem06 : (i j : ℕ ) → Is B C g (fun← cn i) → Is B C g (fun← cn j) → count-B i ≡ count-B j → i ≡ j
758 lem06 i j bi bj eq = lem08 where 758 lem06 i j bi bj eq = lem08 where
759 lem20 : (i j : ℕ) → i < j → Is B C g (fun← cn i) → Is B C g (fun← cn j) → count-B j ≡ count-B i → ⊥ 759 lem20 : (i j : ℕ) → i < j → Is B C g (fun← cn i) → Is B C g (fun← cn j) → count-B j ≡ count-B i → ⊥
760 lem20 zero (suc j) i<j bi bj le with is-B (fun← cn 0) | inspect count-B 0 | is-B (fun← cn (suc j)) | inspect count-B (suc j) 760 lem20 zero (suc j) i<j bi bj le with is-B (fun← cn 0) in eq1 | is-B (fun← cn (suc j)) in eq2
761 ... | no nisc | _ | _ | _ = ⊥-elim (nisc bi) 761 ... | no nisc | _ = ⊥-elim (nisc bi)
762 ... | yes _ | _ | no nisc | _ = ⊥-elim (nisc bj) 762 ... | yes _ | no nisc = ⊥-elim (nisc bj)
763 ... | yes _ | record { eq = eq1 } | yes _ | record { eq = eq2 } = ⊥-elim ( nat-≤> lem25 a<sa) where 763 ... | yes _ | yes _ = ⊥-elim ( nat-≤> lem25 a<sa) where
764 lem22 : 1 ≡ count-B 0 764 lem22 : 1 ≡ count-B 0
765 lem22 with is-B (fun← cn 0) | inspect count-B 0 765 lem22 with is-B (fun← cn 0) in eq1
766 ... | yes _ | record { eq = eq1 } = refl 766 ... | yes _ = refl
767 ... | no nisa | _ = ⊥-elim ( nisa bi ) 767 ... | no nisa = ⊥-elim ( nisa bi )
768 lem24 : count-B j ≡ 0 768 lem24 : count-B j ≡ 0
769 lem24 = cong pred le 769 lem24 = cong pred le
770 lem25 : 1 ≤ 0 770 lem25 : 1 ≤ 0
771 lem25 = begin 771 lem25 = begin
772 1 ≡⟨ lem22 ⟩ 772 1 ≡⟨ lem22 ⟩
778 -- 778 --
779 -- i < suc i ≤ j 779 -- i < suc i ≤ j
780 -- cb i < suc (cb i) < cb (suc i) ≤ cb j 780 -- cb i < suc (cb i) < cb (suc i) ≤ cb j
781 -- suc (cb i) ≡ suc (cb j) → cb i ≡ cb j 781 -- suc (cb i) ≡ suc (cb j) → cb i ≡ cb j
782 lem22 : suc (count-B i) ≡ count-B (suc i) 782 lem22 : suc (count-B i) ≡ count-B (suc i)
783 lem22 with is-B (fun← cn (suc i)) | inspect count-B (suc i) 783 lem22 with is-B (fun← cn (suc i)) in eq1
784 ... | yes _ | record { eq = eq1 } = refl 784 ... | yes _ = refl
785 ... | no nisa | _ = ⊥-elim ( nisa bi ) 785 ... | no nisa = ⊥-elim ( nisa bi )
786 lem23 : suc (count-B j) ≡ count-B (suc j) 786 lem23 : suc (count-B j) ≡ count-B (suc j)
787 lem23 with is-B (fun← cn (suc j)) | inspect count-B (suc j) 787 lem23 with is-B (fun← cn (suc j)) in eq1
788 ... | yes _ | record { eq = eq1 } = refl 788 ... | yes _ = refl
789 ... | no nisa | _ = ⊥-elim ( nisa bj ) 789 ... | no nisa = ⊥-elim ( nisa bj )
790 lem24 : count-B i ≡ count-B j 790 lem24 : count-B i ≡ count-B j
791 lem24 with is-B (fun← cn (suc i)) | inspect count-B (suc i) | is-B (fun← cn (suc j)) | inspect count-B (suc j) 791 lem24 with is-B (fun← cn (suc i)) in eq1 | is-B (fun← cn (suc j)) in eq2
792 ... | no nisc | _ | _ | _ = ⊥-elim (nisc bi) 792 ... | no nisc | _ = ⊥-elim (nisc bi)
793 ... | yes _ | _ | no nisc | _ = ⊥-elim (nisc bj) 793 ... | yes _ | no nisc = ⊥-elim (nisc bj)
794 ... | yes _ | record { eq = eq1 } | yes _ | record { eq = eq2 } = sym (cong pred le) 794 ... | yes _ | yes _ = sym (cong pred le)
795 lem21 : suc (count-B i) ≤ count-B j 795 lem21 : suc (count-B i) ≤ count-B j
796 lem21 = begin 796 lem21 = begin
797 suc (count-B i) ≡⟨ lem22 ⟩ 797 suc (count-B i) ≡⟨ lem22 ⟩
798 count-B (suc i) ≤⟨ count-B-mono i<j ⟩ 798 count-B (suc i) ≤⟨ count-B-mono i<j ⟩
799 count-B j ∎ where 799 count-B j ∎ where
803 ... | tri< a ¬b ¬c = ⊥-elim ( lem20 i j a bi bj (sym eq) ) 803 ... | tri< a ¬b ¬c = ⊥-elim ( lem20 i j a bi bj (sym eq) )
804 ... | tri≈ ¬a b ¬c = b 804 ... | tri≈ ¬a b ¬c = b
805 ... | tri> ¬a ¬b c₁ = ⊥-elim ( lem20 j i c₁ bj bi eq ) 805 ... | tri> ¬a ¬b c₁ = ⊥-elim ( lem20 j i c₁ bj bi eq )
806 806
807 lem07 : (n i : ℕ) → count-B i ≡ suc n → CountB n 807 lem07 : (n i : ℕ) → count-B i ≡ suc n → CountB n
808 lem07 n 0 eq with is-B (fun← cn 0) | inspect count-B 0 808 lem07 n 0 eq with is-B (fun← cn 0)
809 ... | yes isb | record { eq = eq1 } = record { b = Is.a isb ; cb = 0 ; b=cn = sym (Is.fa=c isb) ; cb=n = trans eq1 eq 809 ... | yes isb = lem13 where
810 ; cb-inject = λ cb1 iscb1 cb1eq → lem12 cb1 iscb1 (subst (λ k → k ≡ count-B cb1) eq1 cb1eq) } where 810 cb1 = count-B 0
811 lem14 : count-B 0 ≡ 1
812 lem14 with is-B (fun← cn 0)
813 ... | yes _ = refl
814 ... | no ne = ⊥-elim (ne isb)
811 lem12 : (cb1 : ℕ) → Is B C g (fun← cn cb1) → 1 ≡ count-B cb1 → 0 ≡ cb1 815 lem12 : (cb1 : ℕ) → Is B C g (fun← cn cb1) → 1 ≡ count-B cb1 → 0 ≡ cb1
812 lem12 cb1 iscb1 cbeq = lem06 0 cb1 isb iscb1 (trans eq1 cbeq) 816 lem12 cb1 iscb1 cbeq = lem06 0 cb1 isb iscb1 (trans lem14 cbeq)
813 ... | no nisb | record { eq = eq1 } = ⊥-elim ( nat-≡< eq (s≤s z≤n ) ) 817 lem13 : CountB n
814 lem07 n (suc i) eq with is-B (fun← cn (suc i)) | inspect count-B (suc i) 818 lem13 = record { b = Is.a isb ; cb = 0 ; b=cn = sym (Is.fa=c isb) ; cb=n = trans lem14 eq
815 ... | yes isb | record { eq = eq1 } = record { b = Is.a isb ; cb = suc i ; b=cn = sym (Is.fa=c isb) ; cb=n = trans eq1 eq 819 ; cb-inject = λ cb1 iscb1 cb1eq → lem12 cb1 iscb1 (subst (λ k → k ≡ count-B cb1) lem14 cb1eq) }
816 ; cb-inject = λ cb1 iscb1 cb1eq → lem12 cb1 iscb1 (subst (λ k → k ≡ count-B cb1) eq1 cb1eq) } where 820 ... | no nisb = ⊥-elim ( nat-≡< eq (s≤s z≤n ) )
821 lem07 n (suc i) eq with is-B (fun← cn (suc i))
822 ... | yes isb = record { b = Is.a isb ; cb = suc i ; b=cn = sym (Is.fa=c isb) ; cb=n = trans lem14 eq
823 ; cb-inject = λ cb1 iscb1 cb1eq → lem12 cb1 iscb1 (subst (λ k → k ≡ count-B cb1) lem14 cb1eq) } where
824 cbs = count-B (suc i)
825 lem14 : count-B (suc i) ≡ suc (count-B i)
826 lem14 with is-B (fun← cn (suc i))
827 ... | yes _ = refl
828 ... | no ne = ⊥-elim (ne isb)
817 lem12 : (cb1 : ℕ) → Is B C g (fun← cn cb1) → suc (count-B i) ≡ count-B cb1 → suc i ≡ cb1 829 lem12 : (cb1 : ℕ) → Is B C g (fun← cn cb1) → suc (count-B i) ≡ count-B cb1 → suc i ≡ cb1
818 lem12 cb1 iscb1 cbeq = lem06 (suc i) cb1 isb iscb1 (trans eq1 cbeq) 830 lem12 cb1 iscb1 cbeq = lem06 (suc i) cb1 isb iscb1 (trans lem14 cbeq)
819 ... | no nisb | record { eq = eq1 } = lem07 n i eq 831 ... | no nisb = lem07 n i eq
820 832
821 -- starting from 0, if count B i ≡ suc n, this is it 833 -- starting from 0, if count B i ≡ suc n, this is it
822 834
823 lem09 : (i j : ℕ) → suc n ≤ j → j ≡ count-B i → CountB n 835 lem09 : (i j : ℕ) → suc n ≤ j → j ≡ count-B i → CountB n
824 lem09 0 (suc j) (s≤s le) eq with ≤-∨ (s≤s le) 836 lem09 0 (suc j) (s≤s le) eq with ≤-∨ (s≤s le)
825 ... | case1 eq1 = lem07 n 0 (sym (trans eq1 eq )) 837 ... | case1 eq1 = lem07 n 0 (sym (trans eq1 eq ))
826 ... | case2 (s≤s lt) with is-B (fun← cn 0) | inspect count-B 0 838 ... | case2 (s≤s lt) with is-B (fun← cn 0) in eq1
827 ... | yes isb | record { eq = eq1 } = ⊥-elim ( nat-≤> (≤-trans (s≤s lt) (refl-≤≡ eq) ) (s≤s (s≤s z≤n)) ) 839 ... | yes isb = ⊥-elim ( nat-≤> (≤-trans (s≤s lt) (refl-≤≡ eq) ) (s≤s (s≤s z≤n)) )
828 ... | no nisb | record { eq = eq1 } = ⊥-elim (nat-≡< (sym eq) (s≤s z≤n)) 840 ... | no nisb = ⊥-elim (nat-≡< (sym eq) (s≤s z≤n))
829 lem09 (suc i) (suc j) (s≤s le) eq with ≤-∨ (s≤s le) 841 lem09 (suc i) (suc j) (s≤s le) eq with ≤-∨ (s≤s le)
830 ... | case1 eq1 = lem07 n (suc i) (sym (trans eq1 eq )) 842 ... | case1 eq1 = lem07 n (suc i) (sym (trans eq1 eq ))
831 ... | case2 (s≤s lt) with is-B (fun← cn (suc i)) | inspect count-B (suc i) 843 ... | case2 (s≤s lt) with is-B (fun← cn (suc i)) in eq1
832 ... | yes isb | record { eq = eq1 } = lem09 i j lt (cong pred eq) 844 ... | yes isb = lem09 i j lt (cong pred eq)
833 ... | no nisb | record { eq = eq1 } = lem09 i (suc j) (≤-trans lt a≤sa) eq 845 ... | no nisb = lem09 i (suc j) (≤-trans lt a≤sa) eq
834 846
835 bton : B → ℕ 847 bton : B → ℕ
836 bton b = pred (count-B (fun→ cn (g b))) 848 bton b = pred (count-B (fun→ cn (g b)))
837 849
838 ntob : (n : ℕ) → B 850 ntob : (n : ℕ) → B
851 863
852 -- 864 --
853 -- uniqueness of ntob is proved by injection 865 -- uniqueness of ntob is proved by injection
854 -- 866 --
855 biso1 : (b : B) → ntob (bton b) ≡ b 867 biso1 : (b : B) → ntob (bton b) ≡ b
856 biso1 b with count-B (fun→ cn (g b)) | inspect count-B (fun→ cn (g b)) 868 biso1 b with count-B (fun→ cn (g b)) in eq1
857 ... | zero | record { eq = eq1 } = ⊥-elim ( nat-≡< (sym lem20) (lem21 _ refl) ) where 869 ... | zero = ⊥-elim ( nat-≡< (sym lem20) (lem21 _ refl) ) where
858 lem20 : count-B (fun→ cn (InjectiveF.f gi b)) ≡ zero 870 lem20 : count-B (fun→ cn (InjectiveF.f gi b)) ≡ zero
859 lem20 = eq1 871 lem20 = eq1
860 lem21 : (i : ℕ) → i ≡ fun→ cn (InjectiveF.f gi b) → 0 < count-B i 872 lem21 : (i : ℕ) → i ≡ fun→ cn (InjectiveF.f gi b) → 0 < count-B i
861 lem21 0 eq with is-B (fun← cn 0) | inspect count-B 0 873 lem21 0 eq with is-B (fun← cn 0) in eq1
862 ... | yes isb | record { eq = eq1 } = ≤-refl 874 ... | yes isb = ≤-refl
863 ... | no nisb | record{ eq = eq1 } = ⊥-elim ( nisb record { a = b ; fa=c = trans (sym (fiso← cn _)) (cong (fun← cn) (sym eq)) } ) 875 ... | no nisb = ⊥-elim ( nisb record { a = b ; fa=c = trans (sym (fiso← cn _)) (cong (fun← cn) (sym eq)) } )
864 lem21 (suc i) eq with is-B (fun← cn (suc i)) | inspect count-B (suc i) 876 lem21 (suc i) eq with is-B (fun← cn (suc i)) in eq2
865 ... | yes isb | record{ eq = eq2 } = s≤s z≤n 877 ... | yes isb = s≤s z≤n
866 ... | no nisb | record{ eq = eq2 } = ⊥-elim ( nisb record { a = b ; fa=c = trans (sym (fiso← cn _)) (cong (fun← cn) (sym eq)) } ) 878 ... | no nisb = ⊥-elim ( nisb record { a = b ; fa=c = trans (sym (fiso← cn _)) (cong (fun← cn) (sym eq)) } )
867 ... | suc n | record { eq = eq1 } = begin 879 ... | suc n = begin
868 CountB.b CB ≡⟨ InjectiveF.inject gi (bi-inject→ cn (begin 880 CountB.b CB ≡⟨ InjectiveF.inject gi (bi-inject→ cn (begin
869 fun→ cn (g (CountB.b CB)) ≡⟨ cong (fun→ cn) (sym (CountB.b=cn CB)) ⟩ 881 fun→ cn (g (CountB.b CB)) ≡⟨ cong (fun→ cn) (sym (CountB.b=cn CB)) ⟩
870 fun→ cn (fun← cn (CountB.cb CB)) ≡⟨ fiso→ cn _ ⟩ 882 fun→ cn (fun← cn (CountB.cb CB)) ≡⟨ fiso→ cn _ ⟩
871 CountB.cb CB ≡⟨ CountB.cb-inject CB _ record { a = b ; fa=c = sym (fiso← cn _) } (trans (CountB.cb=n CB) (sym eq1)) ⟩ 883 CountB.cb CB ≡⟨ CountB.cb-inject CB _ record { a = b ; fa=c = sym (fiso← cn _) } (trans (CountB.cb=n CB) (sym eq1)) ⟩
872 fun→ cn (InjectiveF.f gi b) ∎ )) ⟩ 884 fun→ cn (InjectiveF.f gi b) ∎ )) ⟩
989 -- true ∷ true ∷ false ∷ true ∷ true ∷ false ∷ true ∷ [] 1001 -- true ∷ true ∷ false ∷ true ∷ true ∷ false ∷ true ∷ []
990 1002
991 -- LMℕ A Ln = Countable-Bernstein (List A) (List (Maybe A)) (List A ∧ List Bool) Ln (LM1 A Ln) fi gi dec0 dec1 where 1003 -- LMℕ A Ln = Countable-Bernstein (List A) (List (Maybe A)) (List A ∧ List Bool) Ln (LM1 A Ln) fi gi dec0 dec1 where
992 -- someday ... 1004 -- someday ...
993 1005
994 LBBℕ : Bijection (List (List Bool)) ℕ 1006 -- LBBℕ : Bijection (List (List Bool)) ℕ
995 LBBℕ = Countable-Bernstein (List Bool ∧ List Bool) (List (List Bool)) (List Bool ∧ List Bool ) (LM1 Bool (bi-sym _ _ LBℕ)) (LM1 Bool (bi-sym _ _ LBℕ)) 1007 -- LBBℕ = Countable-Bernstein (List Bool ∧ List Bool) (List (List Bool)) (List Bool ∧ List Bool ) (LM1 Bool (bi-sym _ _ LBℕ)) (LM1 Bool (bi-sym _ _ LBℕ))
996 ? ? ? ? where 1008 -- ? ? ? ? where
997 1009 --
998 atob : List (List Bool) → List Bool ∧ List Bool 1010 -- atob : List (List Bool) → List Bool ∧ List Bool
999 atob [] = ⟪ [] , [] ⟫ 1011 -- atob [] = ⟪ [] , [] ⟫
1000 atob ( [] ∷ t ) = ⟪ false ∷ proj1 ( atob t ) , false ∷ proj2 ( atob t ) ⟫ 1012 -- atob ( [] ∷ t ) = ⟪ false ∷ proj1 ( atob t ) , false ∷ proj2 ( atob t ) ⟫
1001 atob ( (h ∷ t1) ∷ t ) = ⟪ h ∷ proj1 ( atob t ) , true ∷ proj2 ( atob t ) ⟫ 1013 -- atob ( (h ∷ t1) ∷ t ) = ⟪ h ∷ proj1 ( atob t ) , true ∷ proj2 ( atob t ) ⟫
1002 1014 --
1003 btoa : List Bool ∧ List Bool → List (List Bool) 1015 -- btoa : List Bool ∧ List Bool → List (List Bool)
1004 btoa ⟪ [] , _ ⟫ = [] 1016 -- btoa ⟪ [] , _ ⟫ = []
1005 btoa ⟪ _ ∷ _ , [] ⟫ = [] 1017 -- btoa ⟪ _ ∷ _ , [] ⟫ = []
1006 btoa ⟪ _ ∷ t0 , false ∷ t1 ⟫ = [] ∷ btoa ⟪ t0 , t1 ⟫ 1018 -- btoa ⟪ _ ∷ t0 , false ∷ t1 ⟫ = [] ∷ btoa ⟪ t0 , t1 ⟫
1007 btoa ⟪ h ∷ t0 , true ∷ t1 ⟫ with btoa ⟪ t0 , t1 ⟫ 1019 -- btoa ⟪ h ∷ t0 , true ∷ t1 ⟫ with btoa ⟪ t0 , t1 ⟫
1008 ... | [] = ( h ∷ [] ) ∷ [] 1020 -- ... | [] = ( h ∷ [] ) ∷ []
1009 ... | x ∷ y = (h ∷ x ) ∷ y 1021 -- ... | x ∷ y = (h ∷ x ) ∷ y
1010 1022 --
1011 Lℕ=ℕ : Bijection (List ℕ) ℕ 1023 -- Lℕ=ℕ : Bijection (List ℕ) ℕ
1012 Lℕ=ℕ = record { 1024 -- Lℕ=ℕ = record {
1013 fun→ = λ x → ? 1025 -- fun→ = λ x → ?
1014 ; fun← = λ n → ? 1026 -- ; fun← = λ n → ?
1015 ; fiso→ = ? 1027 -- ; fiso→ = ?
1016 ; fiso← = ? 1028 -- ; fiso← = ?
1017 } 1029 -- }