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

changeset 1021:1407fed90475

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, 25 Nov 2022 10:45:05 +0900
parents eee019e64bea
children 1b87669d9b11
files src/zorn.agda
diffstat 1 files changed, 24 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Fri Nov 25 08:57:28 2022 +0900
+++ b/src/zorn.agda	Fri Nov 25 10:45:05 2022 +0900
@@ -1480,7 +1480,7 @@
                zc40 : odef (UnionCF A f mf ay supf1 b) w
                zc40 with ZChain.cfcs (pzc  (ob<x lim m<x)) mf< (o<→≤ (omax-x _ _)) o≤-refl (o<→≤ sam<m) fcm
                ... | ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ 
-               ... | ⟪ az , ch-is-sup u u<x is-sup fc1 ⟫ = ⟪ az , ch-is-sup u u<b ? fc2 ⟫  where -- u o< px → u o< b ?
+               ... | ⟪ az , ch-is-sup u u<x is-sup fc1 ⟫ = ⟪ az , ch-is-sup u u<b cp fc2 ⟫  where 
                    zc55 : u o< osuc m
                    zc55 = u<x
                    u<b : u o< b 
@@ -1493,6 +1493,19 @@
                    fc2 = subst (λ k → FClosure A f k w) (trans (sym (zeq _ _ zc57 (o<→≤ <-osuc))) (sym (sf1=sf (ordtrans≤-< u<x m<x))) )  fc1 where
                        zc57 : osuc u o≤ osuc m 
                        zc57 = osucc u<x
+                   sb=sa : {a : Ordinal } → a o≤ m → supf1 a ≡ ZChain.supf (pzc (ob<x lim m<x)) a 
+                   sb=sa {a} a≤m = trans (sf1=sf (ordtrans≤-< a≤m m<x)) (zeq _ _ (osucc a≤m) (o<→≤ <-osuc))
+                   cp : ChainP A f mf ay supf1 u
+                   cp = record { fcy<sup = λ {z} fc → subst (λ k → (z ≡ k) ∨ ( z << k ) ) (sym (sb=sa u<x)) (ChainP.fcy<sup is-sup fc )  
+                        ; order = order 
+                        ; supu=u = trans (sb=sa u<x ) (ChainP.supu=u is-sup)  } where
+                         order : {s : Ordinal} {z1 : Ordinal} → supf1 s o< supf1 u →
+                                FClosure A f (supf1 s) z1 → (z1 ≡ supf1 u) ∨ (z1 << supf1 u)
+                         order {s} {z} s<u fc  = subst (λ k → (z ≡ k) ∨ ( z << k ) ) (sym (sb=sa u<x)) 
+                           (ChainP.order is-sup (subst₂ (λ j k → j o< k ) (sb=sa s≤m) (sb=sa u<x) s<u)  
+                              (subst (λ k → FClosure A f k z) (sb=sa s≤m ) fc )) where
+                              s≤m : s o≤ m 
+                              s≤m = ordtrans (supf-inject0 supf-mono  s<u ) u<x
           ... | tri≈ ¬a b ¬c = ⊥-elim ( ¬a (ordtrans<-≤ a<b b≤x))
           ... | tri> ¬a ¬b c = ⊥-elim ( ¬a (ordtrans<-≤ a<b b≤x))
           cfcs mf< {a} {b} {w} a<b b≤x sa<b fc | case2 b<x = zc40 where
@@ -1509,8 +1522,16 @@
                ... | ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ 
                ... | ⟪ az , ch-is-sup u u<x is-sup fc1 ⟫ = ⟪ az , ch-is-sup u u<x cp (subst (λ k → FClosure A f k w) (sym (sb=sa u<x)) fc1 ) ⟫ where
                    cp : ChainP A f mf ay supf1 u
-                   cp = ?
-                 
+                   cp = record { fcy<sup = λ {z} fc → subst (λ k → (z ≡ k) ∨ ( z << k ) ) (sym (sb=sa u<x)) (ChainP.fcy<sup is-sup fc )  
+                        ; order = order
+                        ; supu=u = trans (sb=sa u<x) (ChainP.supu=u is-sup)  } where
+                         order : {s : Ordinal} {z1 : Ordinal} → supf1 s o< supf1 u →
+                                FClosure A f (supf1 s) z1 → (z1 ≡ supf1 u) ∨ (z1 << supf1 u)
+                         order {s} {z} s<u fc  = subst (λ k → (z ≡ k) ∨ ( z << k ) ) (sym (sb=sa u<x)) 
+                           (ChainP.order is-sup (subst₂ (λ j k → j o< k ) (sb=sa s<b) (sb=sa u<x) s<u)  
+                              (subst (λ k → FClosure A f k z) (sb=sa s<b ) fc )) where
+                              s<b : s o< b 
+                              s<b = ordtrans (supf-inject0 supf-mono  s<u ) u<x
      ---
      --- the maximum chain  has fix point of any ≤-monotonic function
      ---