Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1314:8cd195679686
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 10 Jun 2023 12:37:13 +0900 |
| parents | b8489dcae236 |
| children | 08cd04cc33fe |
| files | src/bijection.agda |
| diffstat | 1 files changed, 12 insertions(+), 8 deletions(-) [+] |
line wrap: on
line diff
--- a/src/bijection.agda Sat Jun 10 11:47:43 2023 +0900 +++ b/src/bijection.agda Sat Jun 10 12:37:13 2023 +0900 @@ -627,14 +627,18 @@ -- lem31 : suc j < count-A (fun→ cn (g (f (fun← an (suc j))))) lem31 with <∨≤ (suc j) (fun→ cn (g (f (fun← an (suc j))))) - ... | case1 lt = lem12 _ refl where - lem12 : (i : ℕ) → i ≡ fun→ cn (g (f (fun← an (suc j)))) → suc j < count-A (fun→ cn (g (f (fun← an (suc j))))) - lem12 zero i=z with is-A (fun← cn zero) | inspect ( count-A ) zero - ... | yes isa | record { eq = eq1 } = ? - ... | no nisa | record { eq = eq1 } = ⊥-elim ( nisa record { a = fun← an 0 ; fa=c = trans (sym (fiso← cn _)) (sym (cong (fun← cn) ? )) } ) - lem12 (suc i) i=z with is-A (fun← cn (suc i)) | inspect ( count-A ) (suc i) - ... | yes isa | record { eq = eq1 } = ? - ... | no nisa | record { eq = eq1 } = ⊥-elim ( nisa record { a = fun← an zero ; fa=c = trans (sym (fiso← cn _)) (sym (cong (fun← cn) ?)) } ) + ... | case1 lt = lem12 _ lt ≤-refl where + lem13 : suc j < fun→ cn (g (f (fun← an (suc j)))) + lem13 = lt + -- suc j is current count of A + -- it increase at fun→ cn (g (f (fun← an (suc j)))) + -- otherwise ≤ + lem12 : (i : ℕ) → suc j < i → i ≤ fun→ cn (g (f (fun← an (suc j)))) → suc j < count-A i + lem12 (suc i) (s≤s sj<i) i≤fj with ≤-∨ sj<i + ... | case1 eq = ? + ... | case2 lt = ? where + lem14 : suc j < count-A i + lem14 = lem12 i lt (≤-trans refl-≤s i≤fj) ... | case2 le = ? where -- count-A<i : (i : ℕ) → count-A i ≤ suc i lem33 : (i : ℕ) → i ≡ fun→ cn (g (f (fun← an (suc j)))) → ¬ (i ≤ maxAC.ac (lem10 j))