Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 893:290c61498d62
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 05 Oct 2022 21:36:52 +0900 |
| parents | f331c8be2425 |
| children | b09e39629d86 |
| files | src/zorn.agda |
| diffstat | 1 files changed, 7 insertions(+), 45 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Wed Oct 05 20:40:37 2022 +0900 +++ b/src/zorn.agda Wed Oct 05 21:36:52 2022 +0900 @@ -395,7 +395,6 @@ asupf : {x : Ordinal } → odef A (supf x) supf-mono : {x y : Ordinal } → x o≤ y → supf x o≤ supf y supf-< : {x y : Ordinal } → supf x o< supf y → supf x << supf y - x≤supfx : {x : Ordinal } → x o≤ z → x o≤ supf x supfmax : {x : Ordinal } → z o< x → supf x ≡ supf z minsup : {x : Ordinal } → x o≤ z → MinSUP A (UnionCF A f mf ay supf x) @@ -666,10 +665,7 @@ b<A : b o< & A b<A = z09 ab b<sfx : b o< ZChain.supf zc x - b<sfx with trio< x (& A) - ... | tri< a ¬b ¬c = ordtrans<-≤ b<x (ZChain.x≤supfx zc (o<→≤ a)) - ... | tri≈ ¬a b ¬c = ordtrans<-≤ b<x (ZChain.x≤supfx zc (o≤-refl0 b)) - ... | tri> ¬a ¬b c = subst (λ k → b o< k ) (sym (ZChain.supfmax zc c)) (ordtrans<-≤ b<A ( ZChain.x≤supfx zc (o≤-refl))) + b<sfx = ? m04 : ¬ HasPrev A (UnionCF A f mf ay supf b) b f m04 nhp = proj1 is-sup ( record { ax = HasPrev.ax nhp ; y = HasPrev.y nhp ; ay = chain-mono1 (ZChain.supf-mono zc (o<→≤ b<x)) (HasPrev.ay nhp) ; x=fy = HasPrev.x=fy nhp } ) @@ -696,10 +692,7 @@ m09 : b o< & A m09 = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) ab)) b<sfx : b o< ZChain.supf zc x - b<sfx with trio< x (& A) - ... | tri< a ¬b ¬c = ordtrans<-≤ b<x (ZChain.x≤supfx zc (o<→≤ a)) - ... | tri≈ ¬a b ¬c = ordtrans<-≤ b<x (ZChain.x≤supfx zc (o≤-refl0 b)) - ... | tri> ¬a ¬b c = subst (λ k → b o< k ) (sym (ZChain.supfmax zc c)) (ordtrans<-≤ m09 ( ZChain.x≤supfx zc (o≤-refl))) + b<sfx = ? m07 : {z : Ordinal} → FClosure A f y z → z <= ZChain.supf zc b m07 {z} fc = ZChain.fcy<sup zc (o<→≤ m09) fc m08 : {s z1 : Ordinal} → ZChain.supf zc s o< ZChain.supf zc b @@ -844,9 +837,9 @@ ... | case2 b<x = ⊥-elim ( ¬p<x<op ⟪ px<b , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x ⟫ ) zc4 : ZChain A f mf ay x - zc4 with osuc-≡< (ZChain.x≤supfx zc o≤-refl ) + zc4 with osuc-≡< ? ... | case1 sfpx=px = record { supf = supf1 ; sup=u = ? ; asupf = asupf1 ; supf-mono = supf-mono1 ; supf-< = supf-<1 - ; x≤supfx = ? ; minsup = ? ; supf-is-sup = ? ; csupf = ? } where + ; supfmax = ? ; minsup = ? ; supf-is-minsup = ? ; csupf = ? } where -- we are going to determine (supf x), which is not specified in previous zc -- case1 : supf px ≡ px @@ -1089,38 +1082,7 @@ -- (sf1=sf0 ?) (trans ? sfpx=px ) ss<spx csupf17 : {z1 : Ordinal } → FClosure A f (supf0 s) z1 → odef (UnionCF A f mf ay supf0 px) z1 csupf17 (init as refl ) = ZChain.csupf zc sf<px - csupf17 (fsuc x fc) = ZChain.f-next zc ? -- (csupf17 fc) - - x≤supfx1 : {z : Ordinal} → z o≤ x → z o≤ supf1 z - x≤supfx1 {z} z≤x with trio< z (supf1 z) -- supf1 x o< x → supf1 x o≤ supf1 px → x o< px ∨ supf1 x ≡ supf1 px - ... | tri< a ¬b ¬c = o<→≤ a - ... | tri≈ ¬a b ¬c = o≤-refl0 b - ... | tri> ¬a ¬b c with trio< z px - ... | tri< a ¬b ¬c = ZChain.x≤supfx zc (o<→≤ a) - ... | tri≈ ¬a b ¬c = subst (λ k → k o< osuc px) (sym b) <-osuc - ... | tri> ¬a ¬b lt = ⊥-elim ( o≤> sf04 c ) where -- c : sp1 o< z, lt : px o< z -- supf1 z ≡ sp1 -- supf1 z o< z - z=x : z ≡ x - z=x with trio< z x - ... | tri< a ¬b ¬c = ⊥-elim ( ¬p<x<op ⟪ lt , subst (λ k → z o< k ) (sym (Oprev.oprev=x op)) a ⟫ ) - ... | tri≈ ¬a b ¬c = b - ... | tri> ¬a ¬b c = ⊥-elim ( o≤> z≤x c ) - sf01 : supf1 x ≡ sp1 - sf01 with trio< x px - ... | tri< a ¬b ¬c = ⊥-elim ( ¬c (pxo<x op )) - ... | tri≈ ¬a b ¬c = ⊥-elim ( ¬c (pxo<x op )) - ... | tri> ¬a ¬b c = refl - sf02 : supf1 px o≤ supf1 x - sf02 = supf-mono1 (o<→≤ (pxo<x op )) - sf00 : px o≤ sp1 -- supf1 px o≤ spuf1 x -- c : sp1 o< x - sf00 = subst₂ (λ j k → j o≤ k ) (trans (sf1=sf0 o≤-refl) (sym sfpx=px)) sf01 sf02 - sf04 : z o≤ sp1 - sf04 with osuc-≡< sf00 - ... | case1 eq = ? where - sf05 : px ≡ sp1 -- z o< osuc x -- z ≡ x - sf05 = eq - sf06 : z ≡ osuc sp1 -- z o< osuc x -- z ≡ x - sf06 = trans z=x (trans (sym (Oprev.oprev=x op)) (cong osuc sf05 )) - ... | case2 lt = subst (λ k → k o≤ sp1 ) (trans (Oprev.oprev=x op) (sym z=x)) (osucc lt ) + csupf17 (fsuc x fc) = ZChain.f-next zc (csupf17 fc) record STMP {z : Ordinal} (z≤x : z o≤ x ) : Set (Level.suc n) where field @@ -1145,7 +1107,7 @@ z1≤px = o<→≤ ( ZChain.supf-inject zc (subst (λ k → supf0 z1 o< k ) sfpx=px a )) ... | tri≈ ¬a b ¬c = subst₂ (λ j k → odef j k ) (sym ch1x=pchainpx) zc20 (case2 (init apx sfpx=px )) where z1≤px : z1 o≤ px -- z1 o≤ supf1 z1 ≡ px - z1≤px = subst (λ k → z1 o< k) (sym (Oprev.oprev=x op)) (supf-inject0 supf-mono1 (ordtrans<-≤ sz1<x (x≤supfx1 o≤-refl ) )) + z1≤px = subst (λ k → z1 o< k) (sym (Oprev.oprev=x op)) (supf-inject0 supf-mono1 (ordtrans<-≤ sz1<x ? )) zc20 : supf0 px ≡ supf1 z1 zc20 = begin supf0 px ≡⟨ sym sfpx=px ⟩ @@ -1156,7 +1118,7 @@ zc21 : px o< z1 zc21 = ZChain.supf-inject zc (subst (λ k → k o< supf0 z1) sfpx=px c ) zc22 : z1 o< x -- c : px o< supf0 z1 - zc22 = supf-inject0 supf-mono1 (ordtrans<-≤ sz1<x (x≤supfx1 o≤-refl ) ) + zc22 = supf-inject0 supf-mono1 (ordtrans<-≤ sz1<x ? ) -- c : px ≡ spuf0 px o< supf0 z1 , px o< z1 o≤ supf1 z1 o< x ... | case2 px<spfx = ? where