Mercurial > hg > Members > kono > Proof > ZF-in-agda

changeset 1056:0dff7ab7a55f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
sup=u ONDE
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 10 Dec 2022 00:38:22 +0900
parents 60211e5b1fe5
children cd3237120dec
files src/zorn.agda
diffstat 1 files changed, 24 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Fri Dec 09 23:27:05 2022 +0900
+++ b/src/zorn.agda	Sat Dec 10 00:38:22 2022 +0900
@@ -899,7 +899,7 @@
 
           zc41 : ZChain A f mf< ay x
           zc41 =  record { supf = supf1 ; sup=u = sup=u ; asupf = asupf1 ; supf-mono = supf1-mono ; order = order
-              ; supfmax = ? ; is-minsup = ? ;  cfcs = cfcs  }  where
+              ; supfmax = supfmax ; is-minsup = is-minsup ;  cfcs = cfcs  }  where
 
                  supf1 : Ordinal → Ordinal
                  supf1 z with trio< z px
@@ -959,6 +959,12 @@
                      (supf1-mono (o<→≤ c ))
                       --  px o<z → supf x ≡ supf0 px ≡ supf1 px o≤ supf1 z
 
+                 supfmax : {z : Ordinal } → x o< z → supf1 z ≡ supf1 x
+                 supfmax {z} x<z with trio< z px
+                 ... | tri< a ¬b ¬c = ⊥-elim ( o<> x<z (subst (λ k → z o< k) (Oprev.oprev=x op) (ordtrans a <-osuc) ))
+                 ... | tri≈ ¬a b ¬c = ⊥-elim ( o<> x<z (subst (λ k → k o< x ) (sym b) px<x ))
+                 ... | tri> ¬a ¬b c = sym (sf1=sp1 px<x )
+
                  fcup : {u z : Ordinal } → FClosure A f (supf1 u) z → u o≤ px → FClosure A f (supf0 u) z
                  fcup {u} {z} fc u≤px = subst (λ k → FClosure A f k z ) (sf1=sf0 u≤px) fc
                  fcpu : {u z : Ordinal } → FClosure A f (supf0 u) z → u o≤ px →  FClosure A f (supf1 u) z
@@ -1133,8 +1139,23 @@
                  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) ⟪ 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 ¬c = ZChain.sup=u zc ab (o<→≤ a) ⟪ zc40 , ZChain.IsMinSUP→NotHasPrev zc ab zc42 (λ ax → proj1 (mf< _ ax))  ⟫ where
+                     zc42 : {w : Ordinal} → odef (UnionCF A f ay (ZChain.supf zc) b) w → w ≤ b
+                     zc42 {w} ⟪ ua , ch-init fc ⟫ = IsSUP.x≤sup (proj1 is-sup)  ⟪ ua , ch-init fc ⟫ 
+                     zc42 {w} ⟪ ua ,  ch-is-sup u u<x su=u fc  ⟫ = IsSUP.x≤sup (proj1 is-sup) ⟪ ua ,  
+                         ch-is-sup u u<x (trans (sf1=sf0 zc44) su=u) (fcpu fc zc44)  ⟫ where
+                           zc44 : u o≤ px
+                           zc44 = ordtrans u<x (o<→≤ a)
+                     zc40 : IsSUP A (UnionCF A f ay supf0 b) b
+                     zc40 = record { ax = ab ; x≤sup = zc42 } 
+                 ... | tri≈ ¬a b=px ¬c = ZChain.sup=u zc ab (o≤-refl0 b=px) ⟪ record { ax = ab ; x≤sup = zc42 } , 
+                                ZChain.IsMinSUP→NotHasPrev zc ab zc42 (λ ax → proj1 (mf< _ ax))  ⟫ where
+                     zc42 : {w : Ordinal} → odef (UnionCF A f ay (ZChain.supf zc) b) w → w ≤ b
+                     zc42 {w} ⟪ ua , ch-init fc ⟫ = IsSUP.x≤sup (proj1 is-sup)  ⟪ ua , ch-init fc ⟫ 
+                     zc42 {w} ⟪ ua ,  ch-is-sup u u<x su=u fc  ⟫ = IsSUP.x≤sup (proj1 is-sup) ⟪ ua ,  
+                         ch-is-sup u u<x (trans (sf1=sf0 zc44) su=u) (fcpu fc zc44)  ⟫ where
+                           zc44 : u o≤ px
+                           zc44 = o<→≤ ( subst (λ k → u o< k ) b=px u<x )
                  ... | tri> ¬a ¬b px<b = trans zc36 x=b where
                      x=b : x ≡ b
                      x=b with osuc-≡< b≤x