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

changeset 963:a8c3ccf8f9d9

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 04 Nov 2022 20:27:31 +0900
parents d594a8439174
children 0bee632db679
files src/zorn.agda
diffstat 1 files changed, 5 insertions(+), 12 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Fri Nov 04 19:19:51 2022 +0900
+++ b/src/zorn.agda	Fri Nov 04 20:27:31 2022 +0900
@@ -677,12 +677,7 @@
               m04 nhp = proj1 is-sup ( record { ax = HasPrev.ax nhp ; y = HasPrev.y nhp ; ay = 
                     chain-mono1 (o<→≤ b<x) (HasPrev.ay  nhp) ; x=fy = HasPrev.x=fy nhp } )
               m05 : ZChain.supf zc b ≡ b
-              m05 =  ZChain.sup=u zc ab (o<→≤ (z09 ab) )
-                      ⟪ record { x≤sup = λ {z} uz → IsMinSUP.x≤sup (proj2 is-sup) uz  
-                          ; minsup = m07 ; not-hp = m04 }  , m04 ⟫ where
-                 m07 :  {s : Ordinal} → odef A s → ({z : Ordinal} →
-                     odef (UnionCF A f mf ay (ZChain.supf zc) b) z → (z ≡ s) ∨ (z << s)) → b o≤ s
-                 m07 {s} as s-is-sup = IsMinSUP.minsup (proj2 is-sup) as s-is-sup
+              m05 =  ZChain.sup=u zc ab (o<→≤ (z09 ab) ) ⟪ record { x≤sup = λ {z} uz → IsMinSUP.x≤sup (proj2 is-sup) uz  }  , m04 ⟫ 
               m08 : {z : Ordinal} → (fcz : FClosure A f y z ) → z <= ZChain.supf zc b
               m08 {z} fcz = ZChain.fcy<sup zc (o<→≤ b<A) fcz
               m09 : {s z1 : Ordinal} → ZChain.supf zc s o< ZChain.supf zc b 
@@ -714,9 +709,7 @@
                       chain-mono1 (o<→≤ b<x) (HasPrev.ay  nhp) 
                  ; x=fy = HasPrev.x=fy nhp } )
               m05 : ZChain.supf zc b ≡ b
-              m05 = ZChain.sup=u zc ab (o<→≤  m09)
-                      ⟪ record { x≤sup = λ lt → IsMinSUP.x≤sup (proj2 is-sup) lt 
-                         ; minsup = IsMinSUP.minsup (proj2 is-sup) ; not-hp = m04 } , m04 ⟫    -- ZChain on x
+              m05 = ZChain.sup=u zc ab (o<→≤  m09) ⟪ record { x≤sup = λ lt → IsMinSUP.x≤sup (proj2 is-sup) lt } , m04 ⟫    -- ZChain on x
               m06 : ChainP A f mf ay supf b 
               m06 = record { fcy<sup = m07 ;  order = m08 ; supu=u = m05 }
 
@@ -1227,8 +1220,8 @@
                  sup=u : {b : Ordinal} (ab : odef A b) →
                     b o≤ x → IsMinSUP A (UnionCF A f mf ay supf0 b) supf0 ab ∧ (¬ HasPrev A (UnionCF A f mf ay supf0 b) f b ) → supf0 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 { x≤sup = λ lt → IsMinSUP.x≤sup (proj1 is-sup) lt ; minsup = ? } , proj2 is-sup ⟫ 
-                 ... | tri≈ ¬a b ¬c = ZChain.sup=u zc ab (o≤-refl0 b) ⟪ record { x≤sup = λ lt → IsMinSUP.x≤sup (proj1 is-sup) lt ; minsup = ? } , proj2 is-sup ⟫ 
+                 ... | tri< a ¬b ¬c = ZChain.sup=u zc ab (o<→≤ a) ⟪ record { x≤sup = λ lt → IsMinSUP.x≤sup (proj1 is-sup) lt } , proj2 is-sup ⟫ 
+                 ... | tri≈ ¬a b ¬c = ZChain.sup=u zc ab (o≤-refl0 b) ⟪ record { x≤sup = λ lt → IsMinSUP.x≤sup (proj1 is-sup) lt } , proj2 is-sup ⟫ 
                  ... | tri> ¬a ¬b px<b = zc31 ? where
                      zc30 : x ≡ b
                      zc30 with osuc-≡< b≤x
@@ -1391,7 +1384,7 @@
                        --  to prove sp is minsup , supf sp ≡ sp is necessary
                        --  to prove supf s ≡ sp , sp is minsup is necessary
                        z26 : supf sp ≡ sp
-                       z26 = ZChain.sup=u zc ? ? ⟪ record { x≤sup = ? } , ? ⟫
+                       z26 = ZChain.sup=u zc asp (o<→≤ z22) ⟪ record { x≤sup = ? } , ? ⟫
                        z25 : u <= sp
                        z25 = MinSUP.x≤sup sp1 ⟪ subst (λ k → odef A k) (ChainP.supu=u is-sup) (ZChain.asupf zc) 
                            , ch-is-sup u u<x is-sup (init (ZChain.asupf zc) (ChainP.supu=u is-sup))  ⟫