Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 854:14bd0c9ad267
csupf b is no good, because supf1 x is not in UnionCF x ( but UnionCD (supf x) )
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 06 Sep 2022 05:15:40 +0900 |
| parents | 2569ace27176 |
| children | 822df9180e63 |
| files | src/zorn.agda |
| diffstat | 1 files changed, 9 insertions(+), 25 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Tue Sep 06 04:38:39 2022 +0900 +++ b/src/zorn.agda Tue Sep 06 05:15:40 2022 +0900 @@ -297,7 +297,7 @@ sup=u : {b : Ordinal} → (ab : odef A b) → b o≤ z → IsSup A (UnionCF A f mf ay supf b) ab → supf b ≡ b supf-is-sup : {x : Ordinal } → (x≤z : x o≤ z) → supf x ≡ & (SUP.sup (sup x≤z) ) supf-mono : {x y : Ordinal } → x o≤ y → supf x o≤ supf y - csupf : {b : Ordinal } → b o≤ z → odef (UnionCF A f mf ay supf (supf b)) (supf b) + csupf : {b : Ordinal } → b o≤ z → odef (UnionCF A f mf ay supf b) (supf b) supf-inject : {x y : Ordinal } → supf x o< supf y → x o< y supf-inject {x} {y} sx<sy with trio< x y ... | tri< a ¬b ¬c = a @@ -323,24 +323,8 @@ s<b = supf-inject ss<sb s≤<z : s o≤ 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) - zc05 with zc04 - ... | ⟪ as , ch-init fc ⟫ = ⟪ as , ch-init fc ⟫ - ... | ⟪ as , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ as , ch-is-sup u (zc09 u≤x ) is-sup fc ⟫ where - zc06 : supf u ≡ u - zc06 = ChainP.supu=u is-sup - zc09 : u o≤ supf s → u o≤ b - zc09 u<s with osuc-≡< (subst (λ k → k o≤ supf s) (sym zc06) u<s) - ... | case1 su=ss = zc08 where - zc07 : supf u o≤ supf b - zc07 = subst (λ k → k o≤ supf b) (sym su=ss) (supf-mono (o<→≤ s<b) ) - zc08 : u o≤ b - zc08 with osuc-≡< zc07 - ... | 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) + zc05 = ? -- csupf s≤<z 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 ) @@ -899,7 +883,7 @@ zcsup with zc30 ... | refl = record { ax = ab ; is-sup = record { x<sup = λ {w} lt → IsSup.x<sup is-sup (subst (λ k → odef k w) pchain0=1 lt) } } - csupf : {b : Ordinal} → b o≤ x → odef (UnionCF A f mf ay (supf1 px) (supf1 px b)) (supf1 px b) + csupf : {b : Ordinal} → b o≤ x → odef (UnionCF A f mf ay (supf1 px) b) (supf1 px b) csupf {b} b≤x = zc05 where zc04 : (b o≤ px ) ∨ (b ≡ x ) zc04 with trio< b px @@ -908,15 +892,15 @@ ... | tri> ¬a ¬b px<b with osuc-≡< b≤x ... | case1 eq = case2 eq ... | case2 b<x = ⊥-elim ( ¬p<x<op ⟪ px<b , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x ⟫ ) - zc05 : odef (UnionCF A f mf ay (supf1 px) (supf1 px b)) (supf1 px b) + zc05 : odef (UnionCF A f mf ay (supf1 px) b) (supf1 px b) zc05 with zc04 ... | case2 b=x with ZChain.csupf zc o≤-refl ... | ⟪ au , ch-init fc ⟫ = ⟪ subst (λ k → odef A k) (supfx b=x) au , ch-init (subst₂ (λ j k → FClosure A f j k ) refl (supfx b=x) fc) ⟫ ... | ⟪ au , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ subst (λ k → odef A k) (supfx b=x) au - , ch-is-sup u (subst (λ k → u o≤ k) (supfx b=x) u≤x) ? zc06 ⟫ where + , ch-is-sup u ? ? zc06 ⟫ where zc08 : supf0 u o≤ supf0 px - zc08 = subst₂ (λ j k → j o≤ k) (sym (ChainP.supu=u is-sup)) refl u≤x + zc08 = ? -- subst₂ (λ j k → j o≤ k) (sym (ChainP.supu=u is-sup)) refl u≤x zc06 : FClosure A f (supf1 px u) (supf1 px b) zc06 with osuc-≡< zc08 ... | case1 eq = subst₂ (λ j k → FClosure A f j k ) zc10 (supfx b=x) fc where @@ -931,9 +915,9 @@ ... | ⟪ au , ch-init fc ⟫ = ⟪ subst (λ k → odef A k) (supf0=1 b≤px) au , ch-init (subst₂ (λ j k → FClosure A f j k ) refl (supf0=1 b≤px) fc) ⟫ ... | ⟪ au , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ subst (λ k → odef A k) (supf0=1 b≤px) au - , ch-is-sup u (subst (λ k → u o≤ k) (supf0=1 b≤px) u≤x) ? zc06 ⟫ where + , ch-is-sup u (subst (λ k → u o≤ k) ? ? ) ? zc06 ⟫ where zc08 : supf0 u o≤ supf0 b - zc08 = subst₂ (λ j k → j o≤ k) (sym (ChainP.supu=u is-sup)) refl u≤x + zc08 = ? -- subst₂ (λ j k → j o≤ k) (sym (ChainP.supu=u is-sup)) refl u≤x zc06 : FClosure A f (supf1 px u) (supf1 px b) zc06 with osuc-≡< zc08 ... | case1 eq = subst₂ (λ j k → FClosure A f j k ) zc10 (supf0=1 b≤px) fc where @@ -1097,7 +1081,7 @@ ... | tri< a ¬b ¬c = ? -- ZChain.sup=u (pzc (osuc b) (ob<x lim a)) ab {!!} record { x<sup = {!!} } ... | tri≈ ¬a b ¬c = {!!} -- ZChain.sup=u (pzc (osuc ?) ?) ab {!!} record { x<sup = {!!} } ... | tri> ¬a ¬b x<z = ⊥-elim (o<¬≡ refl (ordtrans<-≤ x<z z≤x )) - csupf : {z : Ordinal} → z o≤ x → odef (UnionCF A f mf ay supf1 (supf1 z)) (supf1 z) + csupf : {z : Ordinal} → z o≤ x → odef (UnionCF A f mf ay supf1 z) (supf1 z) csupf {z} z≤x with trio< z x ... | tri< a ¬b ¬c = ? where zc9 : odef (UnionCF A f mf ay supf1 z) (ZChain.supf (pzc (osuc z) (ob<x lim a)) z)