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

changeset 956:a2b13a4b6727

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 Thu, 03 Nov 2022 12:11:38 +0900
parents bc27df170a1e
children ce42b1c5cf42
files src/zorn.agda
diffstat 1 files changed, 10 insertions(+), 9 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Thu Nov 03 10:16:02 2022 +0900
+++ b/src/zorn.agda	Thu Nov 03 12:11:38 2022 +0900
@@ -479,7 +479,7 @@
                 m01 : w <= s
                 m01 with trio< (supf u) (supf b)
                 ... | tri< a ¬b ¬c = b-is-sup ⟪ aa , ch-is-sup u {w} a is-sup-z fc ⟫ 
-                ... | tri≈ ¬a b ¬c = <=-trans  ?  ( b-is-sup ⟪ aa , ch-is-sup u {w} ? is-sup-z fc ⟫ )
+                ... | tri≈ ¬a b ¬c = ?
                 ... | tri> ¬a ¬b c = ?
                 -- <=-trans (IsSup.x≤sup is-sup ⟪ aa , ch-is-sup u u<x is-sup-z fc ⟫) b<=s
              m07 :  {s : Ordinal} → odef A s → ({z : Ordinal} →
@@ -682,14 +682,15 @@
                     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) )
-                      ⟪ ?  , m04 ⟫ where
-                             m10 : {s : Ordinal }  →  (odef A s ) 
-                                →  ( {z : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) b) z → (z ≡ s) ∨ (z << s) ) 
-                                →    {z : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) x) z → (z ≡ s) ∨ (z << s)
-                             m10 = ?
-                             m07 :  {sup1 : Ordinal} → odef A sup1 → ({z : Ordinal} →
-                                 odef (UnionCF A f mf ay (ZChain.supf zc) b) z → (z ≡ sup1) ∨ (z << sup1)) → b o≤ sup1
-                             m07 {s} as min = IsSup.minsup (proj2 is-sup) as (m10 as min)
+                      ⟪ record { x≤sup = λ {z} uz → IsSup.x≤sup (proj2 is-sup) (chain-mono1 (o<→≤ b<x) uz) 
+                          ; minsup = m07 }  , m04 ⟫ where
+                 m10 : {s : Ordinal }  →  (odef A s ) 
+                    →  ( {z : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) b) z → (z ≡ s) ∨ (z << s) ) 
+                    →    {z : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) x) z → (z ≡ s) ∨ (z << s)
+                 m10 = ?
+                 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 = IsSup.minsup (proj2 is-sup) as (m10 as s-is-sup)
               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