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

changeset 1076:7e047b46c3b2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
is-minsup done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 16 Dec 2022 09:03:29 +0900
parents 4e986bf9be8c
children faa512b2425c
files src/zorn.agda
diffstat 1 files changed, 20 insertions(+), 9 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Thu Dec 15 18:10:51 2022 +0900
+++ b/src/zorn.agda	Fri Dec 16 09:03:29 2022 +0900
@@ -1470,18 +1470,29 @@
           is-minsup {z} z≤x with osuc-≡< 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 ? ? ?  ⟫  )
+               zm00 {w} ⟪ az , ch-init fc ⟫ = subst (λ k → w ≤ k ) (sym (sf1=spu (sym z=x))) ( 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 (sf1=spu (sym z=x)))  
+                   ( MinSUP.x≤sup usup  ⟪ az , ic-isup u u<x (o≤-refl0 zm05) (subst (λ k → FClosure A f k w) (sym zm06) fc)  ⟫  ) where
+                       u<x : u o< x
+                       u<x = subst (λ k → u o< k) z=x u<b
+                       zm06 : supfz (subst (λ k → u o< k) z=x u<b) ≡ supf1 u
+                       zm06 = trans (zeq _ _  o≤-refl (o<→≤ <-osuc) ) (sym (sf1=sf u<x ))
+                       zm05 : supfz (subst (λ k → u o< k) z=x u<b) ≡ u 
+                       zm05 = trans zm06 su=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 ?)) ? ) ⟫  
+                   zm02 {w} uw with pchainU⊆chain uw
+                   ... | ⟪ 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 zm05) (trans zm03 su=u) zm04 ⟫  where
+                       zm05 : osuc (IChain-i (proj2 uw)) o< z 
+                       zm05 = subst (λ k → osuc  (IChain-i (proj2 uw)) o< k) (sym z=x) ( pic<x (proj2 uw) )
+                       u<x : u1 o< x
+                       u<x = subst (λ k → u1 o< k) z=x ( ordtrans u<b zm05 )
+                       zm03 : supf1 u1 ≡ ZChain.supf (prev (osuc (IChain-i (proj2 uw))) (pic<x (proj2 uw))) u1
+                       zm03 = trans (sf1=sf u<x) (zeq _ _ (osucc u<b) (o<→≤ <-osuc) )
+                       zm04 : FClosure A f (supf1 u1) w
+                       zm04 = subst (λ k → FClosure A f k w) (sym zm03) fc
           ... | 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)