Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 812:96e6643c833d
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 16 Aug 2022 15:24:14 +0900 |
| parents | e09ba00c9b85 |
| children | 1627cc8f193e |
| files | src/zorn.agda |
| diffstat | 1 files changed, 13 insertions(+), 3 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Tue Aug 16 14:34:54 2022 +0900 +++ b/src/zorn.agda Tue Aug 16 15:24:14 2022 +0900 @@ -786,10 +786,20 @@ zc33 = ChainP.supu=u u1-is-sup zc32 : sp1 ≡ x zc32 = begin - ? ≡⟨ ? ⟩ - ? ∎ where open ≡-Reasoning + sp1 ≡⟨ sym eq2 ⟩ + supf1 u1 ≡⟨ zc33 ⟩ + u1 ≡⟨ sym zc31 ⟩ + x ∎ where open ≡-Reasoning + zc34 : {z : Ordinal} → odef (UnionCF A f mf ay supf0 x) z → (z ≡ x) ∨ (z << x) + zc34 {z} lt with SUP.x<sup sup1 (subst (λ k → odef (UnionCF A f mf ay supf0 x) k ) (sym &iso) lt ) + ... | case1 eq = case1 ( begin + z ≡⟨ sym &iso ⟩ + & (* z) ≡⟨ cong (&) eq ⟩ + sp1 ≡⟨ zc32 ⟩ + x ∎ ) where open ≡-Reasoning + ... | case2 lt = case2 ( subst (λ k → * z < k ) (trans (sym *iso) (cong (*) zc32 )) lt ) zcsup : xSUP - zcsup = record { ax = subst (λ k → odef A k) zc32 asp ; is-sup = record { x<sup = {!!} } } + zcsup = record { ax = subst (λ k → odef A k) zc32 asp ; is-sup = record { x<sup = zc34 } } zc60 (fsuc w1 fc) with zc60 fc ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-init (fsuc _ fc₁) ⟫ ... | ⟪ ua1 , ch-is-sup u u≤x is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-is-sup u u≤x is-sup (fsuc _ fc₁) ⟫