Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1370:3bcff593255e
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 21 Jun 2023 17:05:15 +0900 |
| parents | 43471e03d6fe |
| children | 8b66575d4939 |
| files | src/bijection.agda |
| diffstat | 1 files changed, 5 insertions(+), 5 deletions(-) [+] |
line wrap: on
line diff
--- a/src/bijection.agda Wed Jun 21 14:46:51 2023 +0900 +++ b/src/bijection.agda Wed Jun 21 17:05:15 2023 +0900 @@ -697,14 +697,14 @@ lem30 : (i : ℕ) → (cl : List C) → (i≤n : i ≤ suc n) → (a : any-cl (suc i) cl) → suc i < ca-list cl lem30 0 cl i≤n a = begin 2 ≤⟨ s≤s (s≤s z≤n) ⟩ - suc (suc (ca-list (del 1 (del 0 cl a) ?) )) ≡⟨ ? ⟩ - suc (ca-list (del 1 cl ?) ) ≡⟨ ? ⟩ + suc (suc (ca-list (del 0 (del 1 cl a) (del-any 0 cl a)) )) ≡⟨ cong suc ( del-ca 0 (del 1 cl a) (del-any 0 cl a) ) ⟩ + suc (ca-list (del 1 cl a) ) ≡⟨ del-ca 1 cl a ⟩ ca-list cl ∎ where open ≤-Reasoning - -- <-transʳ ? (subst (λ k → ca-list (del ? cl ?) < k) (a-list-ca ? ? (a _ ≤-refl)) a<sa ) lem30 (suc i) cl i≤n a = begin - suc (suc (suc i)) ≤⟨ s≤s (lem30 i (del (suc i) cl a ) (≤-trans a≤sa i≤n) (del-any (suc i) cl a)) ⟩ - suc (ca-list (del (suc i) cl a)) ≡⟨ del-ca (suc i) cl a ⟩ + suc (suc (suc i)) ≤⟨ s≤s (lem30 i (del (suc i) (del (suc (suc i)) cl a ) + (del-any (suc i) cl a) ) (≤-trans a≤sa i≤n) (del-any (suc i) cl a)) ⟩ + suc (ca-list (del (suc i) cl (del-any (suc i) cl a))) ≡⟨ del-ca (suc i) cl (del-any (suc i) cl a) ⟩ ca-list cl ∎ where open ≤-Reasoning lem31 : suc n < ca-list (clist (c (suc n)))