Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1378:5349fe40b6d4
no-good
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 23 Jun 2023 09:47:29 +0900 |
| parents | ddb581d5599b |
| children | |
| files | src/bijection.agda |
| diffstat | 1 files changed, 10 insertions(+), 3 deletions(-) [+] |
line wrap: on
line diff
--- a/src/bijection.agda Fri Jun 23 08:52:08 2023 +0900 +++ b/src/bijection.agda Fri Jun 23 09:47:29 2023 +0900 @@ -728,8 +728,15 @@ cb=n : count-B cb ≡ n lem01 : (n i : ℕ) → n ≤ count-B i → CountB n - lem01 0 i le = ? - lem01 (suc n) i le = ? where -- lem09 (suc n) i (count-B i) ? ? where + lem01 0 i le = lem10 (c 1) (≤-trans ( subst (λ k → 1 ≤ k) (ca-list=count-A (c 1)) (n≤ca-list 1)) (ca≤cb0 (c 1))) where + lem10 : (i : ℕ) → 1 ≤ count-B i → CountB 0 + lem10 0 le with is-B (fun← cn 0) | inspect count-B 0 + ... | yes isb | record { eq = eq1 } = record { b = Is.a isb ; cb = 0 ; b=cn = sym (Is.fa=c isb) ; cb=n = ? } + ... | no nisb | record { eq = eq1 } = ⊥-elim ( nat-≤> le (s≤s z≤n)) + lem10 (suc i) le with is-B (fun← cn (suc i)) | inspect count-B (suc i) + ... | yes isb | record { eq = eq1 } = record { b = Is.a isb ; cb = suc i ; b=cn = sym (Is.fa=c isb) ; cb=n = ? } + ... | no nisb | record { eq = eq1 } = lem10 i le + lem01 (suc n) i le = lem09 n i (count-B i) le refl where -- starting from 0, if count B i ≡ suc n, this is it lem07 : (n i : ℕ) → count-B i ≡ suc n → CountB (suc n) lem07 n 0 eq with is-B (fun← cn 0) | inspect count-B 0 @@ -759,7 +766,7 @@ biso : (n : ℕ) → bton (ntob n) ≡ n biso n = begin - bton (ntob (suc n)) ≡⟨ refl ⟩ + bton (ntob n) ≡⟨ refl ⟩ count-B (fun→ cn (g (CountB.b CB))) ≡⟨ sym ( cong (λ k → count-B (fun→ cn k)) ( CountB.b=cn CB)) ⟩ count-B (fun→ cn (fun← cn (CountB.cb CB))) ≡⟨ ? ⟩ count-B (CountB.cb CB) ≡⟨ CountB.cb=n CB ⟩