# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1659766018 -32400
# Node ID 3a8493e6cd675ee054ee131dde5cee8004cb3c21
# Parent  171123c92007b30dbdcdf9454c649606c8155dd3
supf contraint

diff -r 171123c92007 -r 3a8493e6cd67 src/zorn.agda
--- a/src/zorn.agda	Fri Aug 05 17:57:41 2022 +0900
+++ b/src/zorn.agda	Sat Aug 06 15:06:58 2022 +0900
@@ -226,8 +226,30 @@
       sup : {x : Ordinal } → x o≤ z  → SUP A (UnionCF A f mf ay supf x)
       sup=u : {b : Ordinal} → (ab : odef A b) → b o< z  → IsSup A (UnionCF A f mf ay supf (osuc b)) ab → supf b ≡ b 
       supf-is-sup : {x : Ordinal } → (x≤z : x o≤ z) → supf x ≡ & (SUP.sup (sup x≤z) )
-      csupf : {b : Ordinal } → b o< z → odef (UnionCF A f mf ay supf b) (supf b) 
-      supf-mono : {x y : Ordinal } → x o< y → supf x o≤ supf y
+      csupf : {b : Ordinal } → b o≤ z → odef (UnionCF A f mf ay supf b) (supf b) 
+      supf≤x :{x : Ordinal } → z o≤ x → supf z ≡  supf x
+   supf-mono : {x y : Ordinal } → x o< y → supf x o≤ supf y
+   supf-mono {x} {y} x<y = ? where
+      --   z o≤ x → supf x ≡ supf y ≡ supf z
+      --   x o< z → z o< y → supf x ≡ supf y ≡ supf z
+      sf<sy : supf x o≤ supf y
+      sf<sy with trio< x z
+      ... | tri> ¬a ¬b c = o≤-refl0 (( trans (sym (supf≤x (o<→≤ c))) (supf≤x (ordtrans (ordtrans c x<y ) <-osuc ) ) )) 
+      ... | tri≈ ¬a b ¬c = o≤-refl0 (trans (sym (supf≤x (o≤-refl0 (sym b)))) (supf≤x (subst (λ k → k o< osuc y) b (o<→≤ x<y)))) 
+      ... | tri< x<z ¬b ¬c with trio< y z
+      ... | tri> ¬a ¬b c = ?
+      ... | tri≈ ¬a b ¬c = ?
+      ... | tri< y<z ¬b ¬c with csupf (o<→≤ x<z) | csupf (o<→≤ y<z)
+      ... | ⟪ ax , ch-init fcx ⟫ | ⟪ ay , ch-init fcy ⟫  = ?
+      ... | ⟪ ax , ch-is-sup ux ux≤z is-sup-x fcx ⟫ | ⟪ ay , ch-init fcy ⟫  = ?
+      ... | ⟪ ax , ch-init fcx ⟫ | ⟪ ay , ch-is-sup uy uy≤z is-sup-y fcy ⟫ = ?
+      ... | ⟪ ax , ch-is-sup ux ux≤z is-sup-x fcx ⟫ | ⟪ ay , ch-is-sup uy uy≤z is-sup-y fcy ⟫ = ?
+      -- ... | tri< a ¬b ¬c = csupf (o<→≤ a)
+      -- ... | tri≈ ¬a b ¬c = csupf (o≤-refl0 b)
+      -- ... | tri> ¬a ¬b c = subst (λ k → odef (UnionCF A f mf ay supf x) k ) ? (csupf ? )
+      -- csy : odef (UnionCF A f mf ay supf y) (supf y) 
+      -- csy = csupf ?
+       
    fcy<sup  : {u w : Ordinal } → u o< z  → FClosure A f y w → (w ≡ supf u ) ∨ ( w << supf u ) -- different from order because y o< supf 
    fcy<sup  {u} {w} u<z fc with SUP.x<sup (sup (o<→≤ u<z)) ⟪ subst (λ k → odef A k ) (sym &iso) (A∋fc {A} y f mf fc)  
        , ch-init (subst (λ k → FClosure A f y k) (sym &iso) fc ) ⟫ 
@@ -235,8 +257,8 @@
    ... | case2 lt = case2 (subst (λ k → * w < k ) (subst (λ k → k ≡ _ ) *iso (cong (*) (sym (supf-is-sup (o<→≤ u<z) ))) ) lt )
    order : {b s z1 : Ordinal} → b o< z → supf s o< supf b → FClosure A f (supf s) z1 → (z1 ≡ supf b) ∨ (z1 << supf b)
    order {b} {s} {z1} b<z sf<sb fc = zc04 where
-        zc01 : {z1 : Ordinal } → FClosure A f (supf s) z1 → UnionCF A f mf ay supf b ∋ * z1
-        zc01  (init x refl ) = subst (λ k → odef (UnionCF A f mf ay supf b) k ) (sym &iso) zc03  where
+      zc01 : {z1 : Ordinal } → FClosure A f (supf s) z1 → UnionCF A f mf ay supf b ∋ * z1
+      zc01  (init x refl ) = subst (λ k → odef (UnionCF A f mf ay supf b) k ) (sym &iso) zc03  where
             s<b : s o< b
             s<b with trio< s b
             ... | tri< a ¬b ¬c = a
@@ -247,20 +269,20 @@
             s<z : s o< z
             s<z = ordtrans s<b b<z
             zc03 : odef (UnionCF A f mf ay supf b)  (supf s)
-            zc03 with csupf s<z 
+            zc03 with csupf (o<→≤ s<z )
             ... | ⟪ as , ch-init fc ⟫ = ⟪ as , ch-init fc  ⟫ 
             ... | ⟪ as , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ as , ch-is-sup u (ordtrans u≤x (osucc s<b)) is-sup fc ⟫ 
-        zc01  (fsuc x fc) = subst (λ k → odef (UnionCF A f mf ay supf b) k ) (sym &iso) zc04  where
+      zc01  (fsuc x fc) = subst (λ k → odef (UnionCF A f mf ay supf b) k ) (sym &iso) zc04  where
             zc04 : odef (UnionCF A f mf ay supf b) (f x)
             zc04 with subst (λ k → odef (UnionCF A f mf ay supf b) k ) &iso (zc01 fc  )
             ... | ⟪ as , ch-init fc ⟫ = ⟪ proj2 (mf _ as) , ch-init (fsuc _ fc) ⟫ 
             ... | ⟪ as , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ proj2 (mf _ as) , ch-is-sup u u≤x is-sup (fsuc _ fc) ⟫ 
-        zc00 : ( * z1  ≡  SUP.sup (sup (o<→≤ b<z) )) ∨ ( * z1  < SUP.sup ( sup (o<→≤ b<z) ) )
-        zc00 = SUP.x<sup (sup (o<→≤ b<z)) (zc01 fc )
-        zc04 : (z1 ≡ supf b) ∨ (z1 << supf b)
-        zc04 with zc00
-        ... | case1 eq = case1 (subst₂ (λ j k → j ≡ k ) &iso (sym (supf-is-sup  (o<→≤ b<z) ) ) (cong (&) eq) )
-        ... | case2 lt = case2 (subst₂ (λ j k → j < k ) refl (subst₂ (λ j k → j ≡ k ) *iso refl (cong (*) (sym (supf-is-sup (o<→≤ b<z) ) )))  lt )
+      zc00 : ( * z1  ≡  SUP.sup (sup (o<→≤ b<z) )) ∨ ( * z1  < SUP.sup ( sup (o<→≤ b<z) ) )
+      zc00 = SUP.x<sup (sup (o<→≤ b<z)) (zc01 fc )
+      zc04 : (z1 ≡ supf b) ∨ (z1 << supf b)
+      zc04 with zc00
+      ... | case1 eq = case1 (subst₂ (λ j k → j ≡ k ) &iso (sym (supf-is-sup  (o<→≤ b<z) ) ) (cong (&) eq) )
+      ... | case2 lt = case2 (subst₂ (λ j k → j < k ) refl (subst₂ (λ j k → j ≡ k ) *iso refl (cong (*) (sym (supf-is-sup (o<→≤ b<z) ) )))  lt )
 
 
 record ZChain1 ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) 
@@ -635,7 +657,7 @@
           pchain⊆A {y} ny = proj1 ny
           pnext : {a : Ordinal} → odef pchain a → odef pchain (f a)
           pnext {a} ⟪ aa , ch-init fc ⟫ = ⟪ proj2 (mf a aa) , ch-init (fsuc _ fc)  ⟫
-          pnext {a} ⟪ aa , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ proj2 (mf a aa) , ch-is-sup u {!!} is-sup (fsuc _ fc ) ⟫
+          pnext {a} ⟪ aa , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ proj2 (mf a aa) , ch-is-sup u u≤x is-sup (fsuc _ fc ) ⟫
           pinit :  {y₁ : Ordinal} → odef pchain y₁ → * y ≤ * y₁
           pinit {a} ⟪ aa , ua ⟫  with  ua
           ... | ch-init fc = s≤fc y f mf fc
@@ -796,12 +818,61 @@
 
           no-extension : ¬ spu ≡ x → ZChain A f mf ay x
           no-extension ¬sp=x  = record { initial = pinit ; chain∋init = pcy  ; supf = supf1  ; sup=u = {!!} 
-               ; sup = {!!} ; supf-is-sup = {!!}
-               ; csupf = {!!} ; chain⊆A = pchain⊆A ;  f-next = pnext ;  f-total = ptotal ; supf-mono = {!!} } where
+               ; sup = sup ; supf-is-sup = sis
+               ; csupf = csupf ; chain⊆A = pchain⊆A ;  f-next = pnext ;  f-total = ptotal ; supf-mono = {!!} } where
                  supfu : {u : Ordinal } → ( a : u o< x ) → (z : Ordinal) → Ordinal
                  supfu {u} a z = ZChain.supf (pzc (osuc u) (ob<x lim a)) z
                  UnionCF⊆ : {u : Ordinal} → (a : u o< x ) → UnionCF A f mf ay supf1 x ⊆' UnionCF A f mf ay (supfu a) x 
                  UnionCF⊆ = {!!}
+                 sup : {z : Ordinal} → z o≤ x → SUP A (UnionCF A f mf ay supf1 z)
+                 sup {z} z≤x with trio< z x
+                 ... | tri< a ¬b ¬c = SUP⊆ {!!} (ZChain.sup (pzc z a) o≤-refl )
+                 ... | tri≈ ¬a b ¬c = SUP⊆ {!!} usup
+                 ... | tri> ¬a ¬b c = SUP⊆ {!!} usup
+                 sis : {z : Ordinal} (x≤z : z o≤ x) → supf1 z ≡ & (SUP.sup (sup x≤z))
+                 sis {z} z≤x with trio< z x
+                 ... | tri< a ¬b ¬c = ? where
+                     zc8 = ZChain.supf-is-sup (pzc z a) o≤-refl 
+                 ... | tri≈ ¬a b ¬c = refl
+                 ... | tri> ¬a ¬b c with osuc-≡< z≤x
+                 ... | case1 eq = ⊥-elim ( ¬b eq )
+                 ... | case2 lt = ⊥-elim ( ¬a lt )
+                 sup=u : {b : Ordinal} (ab : odef A b) → b o< x → IsSup A (UnionCF A f mf ay supf1 (osuc b)) ab → supf1 b ≡ b
+                 sup=u {b} ab b<x is-sup with trio< b x
+                 ... | tri< a ¬b ¬c = ZChain.sup=u (pzc (osuc b)  (ob<x lim a))  ab <-osuc record { x<sup = ? }
+                 ... | tri≈ ¬a b ¬c = ?
+                 ... | tri> ¬a ¬b c = ?
+                 csupf : {z : Ordinal} → z o≤ x → odef (UnionCF A f mf ay supf1 z) (supf1 z)
+                 csupf {z} z<x with trio< z x
+                 ... | tri< a ¬b ¬c = zc9 where
+                     zc9 : odef (UnionCF A f mf ay supf1 z)  (ZChain.supf  (pzc (osuc z) (ob<x lim a)) z)
+                     zc9 = ?
+                     zc8 : odef (UnionCF A f mf ay (supfu a) z)  (ZChain.supf  (pzc (osuc z) (ob<x lim a)) z)
+                     zc8 = ZChain.csupf  (pzc (osuc z) (ob<x lim a)) (o<→≤ <-osuc )
+                 ... | tri≈ ¬a b ¬c = ? -- ⊥-elim (¬a z<x)
+                 ... | tri> ¬a ¬b c = ? -- ⊥-elim (¬a z<x)
+                 supf-mono :  {a b : Ordinal}  → a o< b → supf1 a o≤ supf1 b
+                 supf-mono {a0} {b0} a<b = zc10 where
+                     --  x o≤ a → supf1 a ≡ supf1 b ≡ spu
+                     --  x o≤ b → supf1 b ≡ spu
+                     --  a o< x → b o≤ x →   supf1 (supf1 a) ≡ supf1 a
+                     --                      supf1 (supf1 b) ≡ supf1 b
+                     usa : odef (UnionCF A f mf ay (supfu ?) (osuc a0)) (supf1 a0)
+                     usa = ?
+                     usb : odef (UnionCF A f mf ay (supfu ?) (osuc b0)) (supf1 b0)
+                     usb = ?
+                     zc10 : supf1 a0 o≤ supf1 b0
+                     zc10 with trio< a0 x | trio< b0 x
+                     ... | tri< a ¬b ¬c | tri< a' ¬b' ¬c' = ? where
+                         zc11 = ZChain.supf-mono (pzc (osuc a0)  (ob<x lim a)) a<b  
+                         zc12 = ZChain.supf-mono (pzc (osuc b0)  (ob<x lim a')) a<b  
+                     ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c' = ?
+                     ... | tri< a ¬b ¬c | tri> ¬a ¬b' c = ?
+                     ... | tri≈ ¬a b ¬c | tri< a ¬b ¬c' = ? 
+                     ... | tri≈ ¬a b ¬c | tri≈ ¬a' b' ¬c' = ?
+                     ... | tri≈ ¬a b ¬c | tri> ¬a' ¬b c = ?
+                     ... | tri> ¬a ¬b c | _ = ?
+
           zc5 : ZChain A f mf ay x 
           zc5 with ODC.∋-p O A (* x)
           ... | no noax = no-extension {!!} -- ¬ A ∋ p, just skip