# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1671152885 -32400
# Node ID faa512b2425ca6d50468b40d4106f9fc9b392c9a
# Parent  7e047b46c3b22c2da7540f2fb9d2a9e76f04f86f
...

diff -r 7e047b46c3b2 -r faa512b2425c src/zorn.agda
--- a/src/zorn.agda	Fri Dec 16 09:03:29 2022 +0900
+++ b/src/zorn.agda	Fri Dec 16 10:08:05 2022 +0900
@@ -504,6 +504,16 @@
          z45 : f (supf x) ≤ supf x
          z45 = IsMinSUP.x≤sup (is-minsup x≤z ) z46 
 
+   order0 : {a b w : Ordinal } → b o≤ z → supf a o< supf b → supf a o≤ z → FClosure A f (supf a) w → w ≤ supf b 
+   order0 {a} {b} {w} b≤z sa<sb sa≤z fc = IsMinSUP.x≤sup (is-minsup b≤z) (cfcs (supf-inject sa<sb) b≤z sa<b fc) where
+         sa<b : supf a o< b
+         sa<b with x<y∨y≤x (supf a) b
+         ... | case1 lt = lt
+         ... | case2 b≤sa = ⊥-elim ( o≤> b≤sa ( supf-inject ( osucprev ( begin
+                 osuc (supf (supf a))  ≡⟨ cong osuc (supf-idem (ordtrans (supf-inject sa<sb) b≤z)  sa≤z)  ⟩
+                 osuc (supf a)  ≤⟨ osucc sa<sb ⟩
+                 supf b ∎ )))) where open o≤-Reasoning O
+
 record ZChain1 ( A : HOD )    ( f : Ordinal → Ordinal )  (mf< : <-monotonic-f A f)
         {y : Ordinal} (ay : odef A y)  (zc : ZChain A f mf< ay (& A)) ( z : Ordinal ) : Set (Level.suc n) where
    supf = ZChain.supf zc
@@ -1235,7 +1245,7 @@
               mf x ax = ⟪ case2 mf00 , proj2 (mf< x ax ) ⟫ where
                  mf00 : * x < * (f x)
                  mf00 = proj1 ( mf< x ax )
-     ... | tri> ¬a ¬b 0<x = record { supf = supf1 ; asupf = asupf ; supf-mono = supf-mono ; order = ? ; 0<supfz = 0<sufz
+     ... | tri> ¬a ¬b 0<x = record { supf = supf1 ; asupf = asupf ; supf-mono = supf-mono ; order = order ; 0<supfz = 0<sufz
               ; zo≤sz = ?   ; is-minsup = is-minsup ; cfcs = cfcs    }  where
 
           mf : ≤-monotonic-f A f
@@ -1578,6 +1588,10 @@
                    zc44 : FClosure A f (supf1 u) w
                    zc44 = subst (λ k → FClosure A f k w ) (sym zc45) fc
 
+          order : {a b w : Ordinal } → b o≤ x → supf1 a o< supf1 b → FClosure A f (supf1 a) w → w ≤ supf1 b
+          order = ?
+
+
      ---
      --- the maximum chain  has fix point of any ≤-monotonic function
      ---