# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1669363053 -32400
# Node ID 52272b5c9d588c176c763c8dc2e1e21788ec730b
# Parent  1b87669d9b11b912adb2d99b0b39acc2de0eb975
...

diff -r 1b87669d9b11 -r 52272b5c9d58 src/zorn.agda
--- a/src/zorn.agda	Fri Nov 25 12:22:22 2022 +0900
+++ b/src/zorn.agda	Fri Nov 25 16:57:33 2022 +0900
@@ -535,6 +535,9 @@
        z52 : supf (supf b) ≡ supf b
        z52 = sup=u asupf sfb≤x ⟪ record { x≤sup = z54  } , IsMinSUP→NotHasPrev asupf z54 ( λ ax → proj1 (mf< _ ax)) ⟫ 
 
+   -- cp : (mf< : <-monotonic-f A f) {b : Ordinal } → b o≤ z → supf b o≤ z  → ChainP A f mf ay supf (supf b)
+   --    the condition of cfcs is satisfied, this is obvious
+
 supf-unique :  ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f)
         {y xa xb : Ordinal} → (ay : odef A y) →  (xa o≤ xb ) → (za : ZChain A f mf ay xa ) (zb : ZChain A f mf ay xb ) 
       → {z : Ordinal } → z o≤ xa → ZChain.supf za z ≡ ZChain.supf zb z
@@ -1114,6 +1117,8 @@
                      → a o< b → b o≤ x → supf1 a o< b  → FClosure A f (supf1 a) w → odef (UnionCF A f mf ay supf1 b) w
                  cfcs mf< {a} {b} {w} a<b b≤x sa<b fc with zc43 (supf0 a) px
                  ... | case2 px≤sa = z50 where
+                      a<x : a o< x
+                      a<x = ordtrans<-≤ a<b b≤x
                       a≤px : a o≤ px
                       a≤px = subst (λ k → a o< k) (sym (Oprev.oprev=x op)) (ordtrans<-≤ a<b b≤x)
                       --  supf0 a ≡ px we cannot use previous cfcs, it is in the chain because
@@ -1121,10 +1126,20 @@
                       z50 : odef (UnionCF A f mf ay supf1 b) w
                       z50 with osuc-≡< px≤sa
                       ... | case1 px=sa = ⟪ A∋fc {A} _ f mf fc , ch-is-sup (supf0 px) z51 ? (subst (λ k → FClosure A f k w) z52 fc)  ⟫ where
+                          sa≤px : supf0 a o≤ px
+                          sa≤px = subst₂ (λ j k → j o< k) px=sa (sym (Oprev.oprev=x op)) px<x
                           z51 : supf0 px o< b
-                          z51 = ?
+                          z51 = subst (λ k → k o< b ) (sym ( begin supf0 px ≡⟨ cong supf0 px=sa ⟩ 
+                             supf0 (supf0 a ) ≡⟨ ZChain.supf-idem zc mf< a≤px sa≤px ⟩ 
+                             supf0 a ≡⟨ sym (sf1=sf0 a≤px) ⟩ 
+                             supf1 a ∎ )) sa<b where open ≡-Reasoning
                           z52 : supf1 a ≡ supf1 (supf0 px)
-                          z52 = ?
+                          z52 = begin supf1 a ≡⟨ sf1=sf0 a≤px ⟩ 
+                             supf0 a ≡⟨ sym (ZChain.supf-idem zc mf< a≤px sa≤px ) ⟩ 
+                             supf0 (supf0 a) ≡⟨ sym (sf1=sf0 sa≤px)  ⟩ 
+                             supf1 (supf0 a) ≡⟨ cong supf1 (sym (ZChain.supf-idem zc mf< a≤px sa≤px )) ⟩ 
+                             supf1 (supf0 (supf0 a)) ≡⟨ cong (λ k → supf1 (supf0 k)) (sym px=sa)  ⟩ 
+                             supf1 (supf0 px) ∎ where open ≡-Reasoning
                       ... | case2 px<sa = ⊥-elim ( ¬p<x<op ⟪ px<sa , subst₂ (λ j k → j o< k ) (sf1=sf0 a≤px) (sym (Oprev.oprev=x op)) z53 ⟫  ) where
                           z53  : supf1 a o< x
                           z53  = ordtrans<-≤ sa<b b≤x
@@ -1301,9 +1316,15 @@
                      --                        a ≡ px → supf px ≡ px → odef U w
 
                      cfcs0 : a ≡ px → odef (UnionCF A f mf ay supf0 b) w
-                     cfcs0 a=px = ⟪  A∋fc {A} _ f mf fc , ch-is-sup (supf0 px) spx<b ? ? ⟫ where
+                     cfcs0 a=px = ⟪  A∋fc {A} _ f mf fc , ch-is-sup (supf0 px) spx<b ? fc1 ⟫ where
                          spx<b : supf0 px o< b
-                         spx<b = ?
+                         spx<b = subst (λ k → supf0 k o< b) a=px sa<b
+                         cs01 : supf0 a ≡ supf0 (supf0 px)
+                         cs01 = trans (cong supf0 a=px) ( sym ( ZChain.supf-idem zc mf< o≤-refl 
+                              (subst (λ k → supf0 px o< k ) (sym (Oprev.oprev=x op)) (ordtrans<-≤ spx<b b≤x))))
+                         fc1 : FClosure A f (supf0 (supf0 px)) w
+                         fc1 = subst (λ k → FClosure A f k w) cs01 fc
+
 
                      cfcs1 : odef (UnionCF A f mf ay supf0 b) w
                      cfcs1 with trio< a px
@@ -1316,7 +1337,11 @@
                              ( ZChain.cfcs zc mf< a<px o≤-refl sa<x fc ) 
                          ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , (zc-b<x _ sa<x)  ⟫ )
                          ... | tri≈ ¬a sa=px ¬c with trio< a px
-                         ... | tri< a<px ¬b ¬c = ⟪  A∋fc {A} _ f mf fc , ch-is-sup (supf0 a) sa<b ? ? ⟫ 
+                         ... | tri< a<px ¬b ¬c = ⟪  A∋fc {A} _ f mf fc , ch-is-sup (supf0 a) sa<b ? fc1 ⟫ where
+                             cs01 : supf0 a ≡ supf0 (supf0 a)
+                             cs01 =  sym ( ZChain.supf-idem zc mf< (zc-b<x _ (ordtrans<-≤ a<b b≤x)) (zc-b<x _ (ordtrans<-≤ sa<b b≤x)))  
+                             fc1 : FClosure A f (supf0 (supf0 a)) w
+                             fc1 = subst (λ k → FClosure A f k w) cs01 fc
                          ... | tri≈ ¬a a=px ¬c = cfcs0 a=px
                          ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , (zc-b<x _ (ordtrans<-≤ a<b b≤x) )  ⟫ )
                      ... | tri≈ ¬a a=px ¬c = cfcs0 a=px