Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1050:323e6e6622a2
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 08 Dec 2022 07:55:31 +0900 |
| parents | e6b9de04d0ca |
| children | 8d25e368e26f |
| files | src/zorn.agda |
| diffstat | 1 files changed, 33 insertions(+), 7 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Wed Dec 07 21:02:52 2022 +0900 +++ b/src/zorn.agda Thu Dec 08 07:55:31 2022 +0900 @@ -1133,8 +1133,8 @@ sup=u : {b : Ordinal} (ab : odef A b) → b o≤ x → IsSUP A (UnionCF A f ay supf1 b) b ∧ (¬ HasPrev A (UnionCF A f ay supf1 b) f b ) → supf1 b ≡ b sup=u {b} ab b≤x is-sup with trio< b px - ... | tri< a ¬b ¬c = ? -- ZChain.sup=u zc ab (o<→≤ a) is-sup - ... | tri≈ ¬a b ¬c = ? -- ZChain.sup=u zc ab (o≤-refl0 b) is-sup + ... | tri< a ¬b ¬c = ZChain.sup=u zc ab (o<→≤ a) ⟪ record { ax = ? ; x≤sup = ? } , ? ⟫ + ... | tri≈ ¬a b=px ¬c = ZChain.sup=u zc ab (o≤-refl0 b=px) ⟪ record { ax = ? ; x≤sup = ? }, ? ⟫ ... | tri> ¬a ¬b px<b = trans zc36 x=b where x=b : x ≡ b x=b with osuc-≡< b≤x @@ -1143,7 +1143,14 @@ zc31 : sp1 o≤ b zc31 = MinSUP.minsup sup1 ab zc32 where zc32 : {w : Ordinal } → odef pchainpx w → (w ≡ b) ∨ (w << b) - zc32 {w} (case1 uw) = IsSUP.x≤sup (proj1 is-sup) ? + zc32 {w} (case1 ⟪ ua , ch-init fc ⟫ ) = IsSUP.x≤sup (proj1 is-sup) ⟪ ua , ch-init fc ⟫ + zc32 {w} (case1 ⟪ ua , ch-is-sup u u<x su=u fc ⟫ ) = IsSUP.x≤sup (proj1 is-sup) ⟪ ua , ch-is-sup u z01 z02 z03 ⟫ where + z01 : u o< b + z01 = ordtrans u<x (subst (λ k → px o< k ) x=b px<x ) + z02 : supf1 u ≡ u + z02 = trans (sf1=sf0 (o<→≤ u<x)) su=u + z03 : FClosure A f (supf1 u) w + z03 = fcpu fc (o<→≤ u<x) zc32 {w} (case2 fc) = IsSUP.x≤sup (proj1 is-sup) ⟪ A∋fc _ f mf (proj1 fc) , ch-is-sup (supf0 px) sa<x su=u fc1 ⟫ where su=u : supf1 (supf0 px) ≡ supf0 px su=u = trans (sf1=sf0 (zc-b<x _ (proj2 fc))) ( ZChain.supf-idem zc o≤-refl (zc-b<x _ (proj2 fc)) ) @@ -1151,10 +1158,10 @@ fc1 = subst (λ k → FClosure A f k w ) (sym su=u) (proj1 fc) sa<x : supf0 px o< b sa<x = subst (λ k → supf0 px o< k ) x=b ( proj2 fc) - zc36 : sp1 ≡ x -- this cannot heppen because + zc36 : sp1 ≡ x zc36 with osuc-≡< zc31 ... | case1 eq = trans eq (sym x=b) - ... | case2 sp1<b = ⊥-elim (¬p<x<op ⟪ ? , ? ⟫ ) where + ... | case2 sp1<b = ⊥-elim ( <<-irr zc40 (proj1 ( mf< (supf0 px) (ZChain.asupf zc))) ) where -- sp1 o< x → ⊥ -- supf0 px o≤ sp1 o< x → supf0 px o≤ px -- px o≤ supf0 px → px ≡ spuf0 px o≤ spuf1 x o< x @@ -1164,8 +1171,8 @@ zc38 : supf0 px o≤ px zc38 = begin supf0 px ≡⟨ sym (sf1=sf0 o≤-refl) ⟩ - supf1 px ≤⟨ supf1-mono ? ⟩ - supf1 x ≡⟨ sf1=sp1 ? ⟩ + supf1 px ≤⟨ supf1-mono (o<→≤ px<x) ⟩ + supf1 x ≡⟨ sf1=sp1 px<x ⟩ sp1 ≤⟨ zc-b<x _ sp1<x ⟩ px ∎ where open o≤-Reasoning O zc37 : supf0 px ≡ px @@ -1173,6 +1180,25 @@ ... | tri< a ¬b ¬c = ⊥-elim ( o≤> (ZChain.x≤supfx zc o≤-refl zc38) a ) ... | tri≈ ¬a b ¬c = b ... | tri> ¬a ¬b c = ⊥-elim ( o≤> zc38 c ) + zc44 : sp1 o≤ supf0 px + zc44 = begin + sp1 ≤⟨ zc-b<x _ sp1<x ⟩ + px ≡⟨ sym zc37 ⟩ + supf0 px ∎ where open o≤-Reasoning O + zc45 : supf0 px o≤ sp1 + zc45 = begin + supf0 px ≡⟨ sym (sf1=sf0 o≤-refl) ⟩ + supf1 px ≤⟨ supf1-mono (o<→≤ px<x) ⟩ + supf1 x ≡⟨ sf1=sp1 px<x ⟩ + sp1 ∎ where open o≤-Reasoning O + zc39 : supf0 px ≡ sp1 + zc39 with trio< (supf0 px) sp1 + ... | tri< a ¬b ¬c = ⊥-elim ( o≤> zc44 a ) --- sp1 o< x ≡ osuc px ≡ osuc (supf0 px) + ... | tri≈ ¬a b ¬c = b + ... | tri> ¬a ¬b c = ⊥-elim ( o≤> zc45 c ) --- supf0 px o≤ supf1 x ≡ sp1 + zc40 : f (supf0 px) ≤ supf0 px + zc40 = subst (λ k → f (supf0 px) ≤ k ) (sym zc39) + ( MinSUP.x≤sup sup1 (case2 ⟪ fsuc _ (init (ZChain.asupf zc) refl) , subst (λ k → k o< x) (sym zc37) px<x ⟫ )) ... | no lim with trio< x o∅ ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a )