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

changeset 949:efc833407350

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 Mon, 31 Oct 2022 23:27:55 +0900
parents 51556591c879
children 6e126013f056
files src/zorn.agda
diffstat 1 files changed, 17 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Mon Oct 31 18:34:06 2022 +0900
+++ b/src/zorn.agda	Mon Oct 31 23:27:55 2022 +0900
@@ -466,6 +466,8 @@
       is-max :  {a b : Ordinal } → (ca : odef (UnionCF A f mf ay supf z) a ) → supf b o< supf z  → (ab : odef A b) 
           → HasPrev A (UnionCF A f mf ay supf z) b f ∨  IsSup A (UnionCF A f mf ay supf z) ab  
           → * a < * b  → odef ((UnionCF A f mf ay supf z)) b
+      order : {b s z1 : Ordinal} → b o< & A → supf s o< supf b → FClosure A f (supf s) z1 → (z1 ≡ supf b) ∨ (z1 << supf b)
+
 
 record Maximal ( A : HOD )  : Set (Level.suc n) where
    field
@@ -630,7 +632,7 @@
 
         zc1 :  (x : Ordinal) →  ((y₁ : Ordinal) → y₁ o< x → ZChain1 A f mf ay zc y₁) → ZChain1 A f mf ay zc x
         zc1 x prev with Oprev-p x  -- prev is not used now....
-        ... | yes op = record { is-max = is-max } where
+        ... | yes op = record { is-max = is-max ; order = order  } where
            px = Oprev.oprev op
            zc-b<x : {b : Ordinal } → ZChain.supf zc b o< ZChain.supf zc x → b o< osuc px
            zc-b<x {b} lt = subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) (ZChain.supf-inject zc lt  )
@@ -659,7 +661,7 @@
               m09 {s} {z} s<b fcz = order b<A s<b fcz    
               m06 : ChainP A f mf ay supf b 
               m06 = record {  fcy<sup = m08  ; order = m09 ; supu=u = m05 }
-        ... | no lim = record { is-max = is-max }  where
+        ... | no lim = record { is-max = is-max ; order = order }  where
            is-max :  {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay supf x) a →
               ZChain.supf zc b o< ZChain.supf zc x → (ab : odef A b) →
               HasPrev A (UnionCF A f mf ay supf x) b f ∨ IsSup A (UnionCF A f mf ay supf x) ab →
@@ -1529,6 +1531,19 @@
                 z45 p = subst (λ k → (* (cf nmx k) ≡ * d) ∨ (* (cf nmx k) < * d)) (sym x=fy) p
                 z48 : supf mc << d
                 z48 = sc<<d {mc} asc spd
+                z53 : supf u o< supf (& A)
+                z53 = ordtrans<-≤ u<x (ZChain.supf-mono zc (o<→≤ d<A) )
+                z52 : ( u ≡ mc ) ∨  ( u << mc )
+                z52 = MinSUP.x<sup msp1 ⟪ subst (λ k → odef A k ) (ChainP.supu=u is-sup1) (A∋fcs _ _ (cf-is-≤-monotonic nmx) fc) 
+                        , ch-is-sup u z53 is-sup1 (init (ZChain.asupf zc)  (ChainP.supu=u is-sup1)) ⟫
+                z51 : supf u o≤ supf mc
+                z51 = ? --with z52
+                -- ... | case1 eq = ?
+                -- ... | case2 lt = ? -- ZChain.supf-<= zc (case2 ? )
+                z49 : supf u o< supf mc → (cf nmx (cf nmx y) ≡ supf mc) ∨ (* (cf nmx (cf nmx y)) < * (supf mc) )
+                z49 su<smc = ZChain1.order (SZ1 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc (& A)) mc<A su<smc (fsuc _ ( fsuc  _ fc ))
+                z50 : (cf nmx (cf nmx y) ≡ supf d) ∨ (* (cf nmx (cf nmx y)) < * (supf d) )
+                z50 = ZChain1.order (SZ1 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc (& A)) d<A u<x (fsuc _ ( fsuc  _ fc ))
                 z47 : {mc d1 : Ordinal } {asc : odef A (supf mc)} (spd : MinSUP A (uchain (cf nmx)  (cf-is-≤-monotonic nmx) asc )) 
                     →  * (cf nmx (cf nmx y)) < * d1
                 z47 {mc} {d1} {asc} spd = ?