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

changeset 1075:4e986bf9be8c

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, 15 Dec 2022 18:10:51 +0900
parents 1e7d20b15341
children 7e047b46c3b2
files src/zorn.agda
diffstat 1 files changed, 14 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Wed Dec 14 12:18:48 2022 +0900
+++ b/src/zorn.agda	Thu Dec 15 18:10:51 2022 +0900
@@ -1468,7 +1468,20 @@
 
           is-minsup :  {z : Ordinal} → z o≤ x → IsMinSUP A (UnionCF A f ay supf1 z) (supf1 z)
           is-minsup {z} z≤x with osuc-≡< z≤x
-          ... | case1 z=x = ?
+          ... | case1 z=x = record { as = asupf ; x≤sup = zm00 ; minsup = zm01 } where
+               zm00 : {w : Ordinal } → odef (UnionCF A f ay supf1 z) w → w ≤ supf1 z 
+               zm00 {w} ⟪ az , ch-init fc ⟫ = subst (λ k → w ≤ k ) (sym ?) ( MinSUP.x≤sup usup ⟪ az , ic-init fc ⟫ ) 
+               zm00 {w} ⟪ az , ch-is-sup u u<b su=u fc ⟫ = subst (λ k → w ≤ k ) (sym ? ) 
+                  ( MinSUP.x≤sup usup  ⟪ az , ic-isup u ? ? ?  ⟫  )
+               zm01 : { s : Ordinal } → odef A s →  ( {x : Ordinal  } → odef (UnionCF A f ay supf1 z) x → x ≤ s )  → supf1 z o≤ s
+               zm01 {s} as sup = subst (λ k → k o≤ s ) (sym (sf1=spu (sym z=x))) ( MinSUP.minsup usup as zm02 ) where 
+                   zm02 : {w : Ordinal } →  odef pchainU w → w ≤ s
+                   zm02 {w} ⟪ az , ic-init fc ⟫ = sup ⟪ az , ch-init fc ⟫
+                   zm02 {w} ⟪ az , ic-isup u u<x sa<x fc  ⟫  = sup ⟪ az , ch-is-sup u 
+                      (subst (λ k → u o< k) (sym z=x) u<x) ? (subst (λ k → FClosure A f k w) (sym (sf1=sf u<x)) fc)  ⟫
+                   -- with ZChain.cfcs (pzc  (ob<x lim u<x)) <-osuc o≤-refl sa<x fc
+                   -- ... | ⟪ az , ch-init fc ⟫ = sup ⟪ az , ch-init fc ⟫ 
+                   -- ... | ⟪ az , ch-is-sup u1 u<b su=u fc ⟫ = sup  ⟪ az , ch-is-sup u1 (ordtrans u<b ?) ? (subst (λ k → FClosure A f k w) (sym (sf1=sf ?)) ? ) ⟫  
           ... | case2 z<x = record { as = asupf ; x≤sup = zm00 ; minsup = zm01 } where
                supf0 = ZChain.supf (pzc (ob<x lim z<x)) 
                msup : IsMinSUP A (UnionCF A f ay supf0 z) (supf0 z)