Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 831:b91681b604d8
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Mon, 22 Aug 2022 11:03:00 +0900 (2022-08-22) |
parents | 507f6582c31d |
children | e61cbf28ec31 |
files | src/zorn.agda |
diffstat | 1 files changed, 33 insertions(+), 10 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Mon Aug 22 07:39:18 2022 +0900 +++ b/src/zorn.agda Mon Aug 22 11:03:00 2022 +0900 @@ -304,12 +304,35 @@ ... | case1 eq = case1 (subst (λ k → k ≡ supf u ) &iso (trans (cong (&) eq) (sym (supf-is-sup u<z ) ) )) ... | case2 lt = case2 (subst (λ k → * w < k ) (subst (λ k → k ≡ _ ) *iso (cong (*) (sym (supf-is-sup u<z ))) ) lt ) - csupf-fc : {b s z1 : Ordinal} → b o≤ z → supf s o< supf b → FClosure A f (supf s) z1 → UnionCF A f mf ay supf b ∋ * z1 - csupf-fc {b} {s} {z1} b≤<z ss<sb (init x refl ) = subst (λ k → odef (UnionCF A f mf ay supf b) k ) (sym &iso) zc05 where + csupf-fc : {b s z1 : Ordinal} → b o≤ z → supf s o≤ supf b → FClosure A f (supf s) z1 → UnionCF A f mf ay supf b ∋ * z1 + csupf-fc {b} {s} {z1} b≤z ss≤sb (init x refl ) with osuc-≡< ss≤sb + ... | case1 eq = subst (λ k → odef (UnionCF A f mf ay supf b) k ) (sym &iso) zc05 where + zc04 : odef (UnionCF A f mf ay supf (supf s)) (supf s) + zc04 = subst (λ k → odef (UnionCF A f mf ay supf k) k) (sym eq) ( csupf b≤z ) + zc05 : odef (UnionCF A f mf ay supf b) (supf s) + zc05 with zc04 + ... | ⟪ as , ch-init fc ⟫ = ⟪ as , ch-init fc ⟫ + ... | ⟪ as , ch-is-sup u u≤x is-sup fc ⟫ = zc09 u≤x where + zc06 : supf u ≡ u + zc06 = ChainP.supu=u is-sup + zc09 : u o≤ supf s → odef (UnionCF A f mf ay supf b) (supf s) + zc09 u≤ss with osuc-≡< (subst (λ k → k o≤ supf s) (sym zc06) u≤ss) + ... | case1 su=ss = zc08 where + zc07 : supf u o≤ supf b + zc07 = subst₂ (λ j k → j o≤ k) (sym zc06) eq u≤ss + zc08 : odef (UnionCF A f mf ay supf b) (supf s) + zc08 with osuc-≡< zc07 + ... | case2 lt = ⟪ as , ch-is-sup u (o<→≤ (supf-inject lt )) is-sup fc ⟫ + ... | case1 su=sb with trio< u b + ... | tri< u<b ¬b ¬c = ? + ... | tri≈ ¬a u=b ¬c = ? + ... | tri> ¬a ¬b b<u = ⟪ ? , ch-is-sup (supf b) ? ? ? ⟫ + ... | case2 lt = ⟪ as , ch-is-sup u (o<→≤ (supf-inject (subst (λ k → supf u o< k) eq lt ))) is-sup fc ⟫ + ... | case2 ss<sb = subst (λ k → odef (UnionCF A f mf ay supf b) k ) (sym &iso) zc05 where s<b : s o< b s<b = supf-inject ss<sb s≤<z : s o≤ z - s≤<z = ordtrans s<b b≤<z + s≤<z = ordtrans s<b b≤z zc04 : odef (UnionCF A f mf ay supf (supf s)) (supf s) zc04 = csupf s≤<z zc05 : odef (UnionCF A f mf ay supf b) (supf s) @@ -328,15 +351,15 @@ ... | case1 su=sb = ⊥-elim ( o<¬≡ (trans (sym su=ss) su=sb ) ss<sb ) ... | case2 lt = o<→≤ (supf-inject lt ) ... | case2 lt = o<→≤ (ordtrans (supf-inject lt) s<b) - csupf-fc {b} {s} {z1} b<z ss<sb (fsuc x fc) = subst (λ k → odef (UnionCF A f mf ay supf b) k ) (sym &iso) zc04 where + csupf-fc {b} {s} {z1} b<z ss≤sb (fsuc x fc) = subst (λ k → odef (UnionCF A f mf ay supf b) k ) (sym &iso) zc04 where zc04 : odef (UnionCF A f mf ay supf b) (f x) - zc04 with subst (λ k → odef (UnionCF A f mf ay supf b) k ) &iso (csupf-fc b<z ss<sb fc ) + zc04 with subst (λ k → odef (UnionCF A f mf ay supf b) k ) &iso (csupf-fc b<z ss≤sb fc ) ... | ⟪ as , ch-init fc ⟫ = ⟪ proj2 (mf _ as) , ch-init (fsuc _ fc) ⟫ ... | ⟪ as , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ proj2 (mf _ as) , ch-is-sup u u≤x is-sup (fsuc _ fc) ⟫ - order : {b s z1 : Ordinal} → b o< z → supf s o< supf b → FClosure A f (supf s) z1 → (z1 ≡ supf b) ∨ (z1 << supf b) - order {b} {s} {z1} b<z ss<sb fc = zc04 where + order : {b s z1 : Ordinal} → b o< z → supf s o≤ supf b → FClosure A f (supf s) z1 → (z1 ≡ supf b) ∨ (z1 << supf b) + order {b} {s} {z1} b<z ss≤sb fc = zc04 where zc00 : ( * z1 ≡ SUP.sup (sup b<z )) ∨ ( * z1 < SUP.sup ( sup b<z ) ) - zc00 = SUP.x<sup (sup b<z) (csupf-fc (o<→≤ b<z) ss<sb fc ) + zc00 = SUP.x<sup (sup b<z) (csupf-fc (o<→≤ b<z) ss≤sb fc ) zc04 : (z1 ≡ supf b) ∨ (z1 << supf b) zc04 with zc00 ... | case1 eq = case1 (subst₂ (λ j k → j ≡ k ) &iso (sym (supf-is-sup b<z) ) (cong (&) eq) ) @@ -541,7 +564,7 @@ m08 {z} fcz = ZChain.fcy<sup zc b<A fcz m09 : {s z1 : Ordinal} → ZChain.supf zc s o< ZChain.supf zc b → FClosure A f (ZChain.supf zc s) z1 → z1 <= ZChain.supf zc b - m09 {s} {z} s<b fcz = ZChain.order zc b<A s<b fcz + m09 {s} {z} s<b fcz = ZChain.order zc b<A (o<→≤ s<b) fcz m06 : ChainP A f mf ay (ZChain.supf zc) b m06 = record { fcy<sup = m08 ; order = m09 ; supu=u = ZChain.sup=u zc ab (o<→≤ b<A ) record { x<sup = λ {z} uz → IsSup.x<sup is-sup (chain-mono1 (o<→≤ b<x) uz ) } } @@ -561,7 +584,7 @@ m07 {z} fc = ZChain.fcy<sup zc m09 fc m08 : {s z1 : Ordinal} → ZChain.supf zc s o< ZChain.supf zc b → FClosure A f (ZChain.supf zc s) z1 → z1 <= ZChain.supf zc b - m08 {s} {z1} s<b fc = ZChain.order zc m09 s<b fc + m08 {s} {z1} s<b fc = ZChain.order zc m09 (o<→≤ s<b) fc m05 : b ≡ ZChain.supf zc b m05 = sym (ZChain.sup=u zc ab (o<→≤ m09) record { x<sup = λ lt → IsSup.x<sup is-sup (chain-mono1 (o<→≤ b<x) lt )} ) -- ZChain on x