# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1668619359 -32400
# Node ID 4aaecae58da5bc42f69e3931f08e431feaa97fc8
# Parent  c190f708862ae43d1b6b66e5c4c0f521c84dc0f8
... x < & A ?

diff -r c190f708862a -r 4aaecae58da5 src/zorn.agda
--- a/src/zorn.agda	Thu Nov 17 00:22:58 2022 +0900
+++ b/src/zorn.agda	Thu Nov 17 02:22:39 2022 +0900
@@ -116,6 +116,9 @@
 ≤-monotonic-f : (A : HOD) → ( Ordinal → Ordinal ) → Set (Level.suc n)
 ≤-monotonic-f A f = (x : Ordinal ) → odef A x → ( * x ≤ * (f x) ) ∧  odef A (f x )
 
+<-monotonic-f : (A : HOD) → ( Ordinal → Ordinal ) → Set n
+<-monotonic-f A f = (x : Ordinal ) → odef A x → ( * x < * (f x) ) ∧  odef A (f x )
+
 data FClosure (A : HOD) (f : Ordinal → Ordinal ) (s : Ordinal) : Ordinal → Set n where
    init : {s1 : Ordinal } → odef A s → s ≡ s1  → FClosure A f s s1
    fsuc : (x : Ordinal) ( p :  FClosure A f s x ) → FClosure A f s (f x)
@@ -660,9 +663,9 @@
      --     supf is fixed for z ≡ & A , we can prove order and is-max
      --
 
-     SZ1 : ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f)
+     SZ1 : ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) (mf< : <-monotonic-f A f)
         {init : Ordinal} (ay : odef A init) (zc : ZChain A f mf ay (& A)) (x : Ordinal)   → ZChain1 A f mf ay zc x
-     SZ1 f mf {y} ay zc x = TransFinite { λ x →  ZChain1 A f mf ay zc x } zc1 x where
+     SZ1 f mf mf< {y} ay zc x = ? where
         chain-mono1 :  {a b c : Ordinal} → a o≤ b
             → odef (UnionCF A f mf ay (ZChain.supf zc) a) c → odef (UnionCF A f mf ay (ZChain.supf zc) b) c
         chain-mono1  {a} {b} {c} a≤b = chain-mono f mf ay (ZChain.supf zc) (ZChain.supf-mono zc) a≤b
@@ -709,8 +712,8 @@
           ... | case1 eq = case1 (subst₂ (λ j k → j ≡ k ) refl (sym (ZChain.supf-is-minsup zc (o<→≤ b<z))  ) eq )
           ... | case2 lt = case2 (subst₂ (λ j k → j < * k ) refl (sym (ZChain.supf-is-minsup zc (o<→≤ b<z) )) lt )
 
-        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  
+        zc1 :  (x : Ordinal ) → x o< & A →   ZChain1 A f mf ay zc x
+        zc1 x x<A with Oprev-p x  
         ... | yes op = record { is-max = is-max ; order = order  } where
                px = Oprev.oprev op
                is-max :  {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay supf x) a →
@@ -735,38 +738,19 @@
                   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 }
-               ... | case1 sb=sx = ? where
-                  b<A : b o< & A
-                  b<A = z09 ab
-                  m09 : IsSUP A (UnionCF A f mf ay (ZChain.supf zc) b) ab
-                  m09 = proj2 is-sup
-                  m04 : ¬ HasPrev A (UnionCF A f mf ay supf b) f b
-                  m04 nhp = proj1 is-sup ( record { ax = HasPrev.ax nhp ; y = HasPrev.y nhp ; ay =
-                        chain-mono1 (o<→≤ b<x) (HasPrev.ay  nhp) ; x=fy = HasPrev.x=fy nhp } )
-                  m05 : ZChain.supf zc b ≡ b
-                  m05 = ZChain.sup=u zc ab (o<→≤ (z09 ab) ) ⟪ record { x≤sup = λ {z} uz → IsSUP.x≤sup (proj2 is-sup) uz  }  , m04 ⟫
-                  m07 : MinSUP A (UnionCF A f mf ay supf (supf x)) -- supf z o< supf ( supf x )
-                  m07 = ZChain.minsup zc (o<→≤ (z09 (ZChain.asupf zc)))
-                  m29 : x o≤ & A
-                  m29 = ?
-                  m15 : supf (supf x) ≡ MinSUP.sup m07 
-                  m15 = ZChain.supf-is-minsup zc (o<→≤ (z09 (ZChain.asupf zc)))
+               ... | case1 sb=sx = ⊥-elim (<-irr (case1 (cong (*) m10)) (proj1 (mf< (supf b) (ZChain.asupf zc)))) where
+                  x≤A : x o≤ & A
+                  x≤A = o<→≤ x<A
                   m17 : MinSUP A (UnionCF A f mf ay supf x) -- supf z o< supf ( supf x )
-                  m17 = ZChain.minsup zc m29
+                  m17 = ZChain.minsup zc x≤A
                   m18 : supf x ≡ MinSUP.sup m17 
-                  m18 = ZChain.supf-is-minsup zc m29
+                  m18 = ZChain.supf-is-minsup zc x≤A
                   m10 : f (supf b) ≡ supf b
                   m10 = fc-stop A f mf (ZChain.asupf zc) m11 sb=sx where
                       m11 : {z : Ordinal} → FClosure A f (supf b) z → (z ≡ ZChain.supf zc x) ∨ (z << ZChain.supf zc x)
                       m11 {z} fc = subst (λ k → (z ≡ k) ∨ (z << k)) (sym m18) ( MinSUP.x≤sup m17 m13 ) where
                           m13 :  odef (UnionCF A f mf ay supf x) z
-                          m13 = ZChain.fcs<sup zc b<x m29  fc
-                          m12 :  odef (UnionCF A f mf ay supf (& A)) z
-                          m12 = ZChain.fcs<sup zc ? ?  fc
-                          -- m14 :  odef (UnionCF A f mf ay supf x) z
-                          -- m14 = ZChain.fcs<sup zc ? ?
-                  m08 : MinSUP A (UnionCF A f mf ay supf b)
-                  m08 = ZChain.minsup zc (o<→≤ (z09 ab))           -- supf z o< supf b
+                          m13 = ZChain.fcs<sup zc b<x x≤A  fc
 
         ... | 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 →
@@ -794,17 +778,19 @@
                   m05 = ZChain.sup=u zc ab (o<→≤  m09) ⟪ record { x≤sup = λ lt → IsSUP.x≤sup (proj2 is-sup) lt } , m04 ⟫    -- ZChain on x
                   m06 : ChainP A f mf ay supf b
                   m06 = record { fcy<sup = m07 ;  order = m08 ; supu=u = m05 }
-               ... | case1 sb=sx = ? where
+               ... | case1 sb=sx = ⊥-elim (<-irr (case1 (cong (*) m10)) (proj1 (mf< (supf b) (ZChain.asupf zc)))) where
+                  x≤A : x o≤ & A
+                  x≤A = o<→≤ x<A
                   m17 : MinSUP A (UnionCF A f mf ay supf x) -- supf z o< supf ( supf x )
-                  m17 = ZChain.minsup zc ?
+                  m17 = ZChain.minsup zc x≤A
                   m18 : supf x ≡ MinSUP.sup m17 
-                  m18 = ZChain.supf-is-minsup zc ?
+                  m18 = ZChain.supf-is-minsup zc x≤A
                   m10 : f (supf b) ≡ supf b
                   m10 = fc-stop A f mf (ZChain.asupf zc) m11 sb=sx where
                       m11 : {z : Ordinal} → FClosure A f (supf b) z → (z ≡ ZChain.supf zc x) ∨ (z << ZChain.supf zc x)
                       m11 {z} fc = subst (λ k → (z ≡ k) ∨ (z << k)) (sym m18) ( MinSUP.x≤sup m17 m13 ) where
                           m13 :  odef (UnionCF A f mf ay supf x) z
-                          m13 = ZChain.fcs<sup zc b<x ?  fc
+                          m13 = ZChain.fcs<sup zc b<x x≤A  fc
 
      uchain : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → HOD
      uchain f mf {y} ay = record { od = record { def = λ x → FClosure A f y x } ; odmax = & A ; <odmax =
@@ -836,7 +822,13 @@
             ... | tri< a ¬b ¬c = ?
             ... | tri≈ ¬a b ¬c = MinSUP.sup (ysup f mf ay)
             ... | tri> ¬a ¬b 0<x with Oprev-p x
-            ... | yes op = ?
+            ... | yes op = ? where
+                px = Oprev.oprev  op
+                sfc00 : Ordinal
+                sfc00 with trio< (prev px ? ) (MinSUP.sup (ysup f mf ? ))
+                ... | tri< a ¬b ¬c = ?
+                ... | tri≈ ¬a b ¬c = ?
+                ... | tri> ¬a ¬b c = ?
             ... | no lim = ?
 
      --
@@ -1395,10 +1387,10 @@
          → MinSUP A (UnionCF A f mf ay (ZChain.supf zc) x)
      msp0 f mf {x} ay zc = minsupP (UnionCF A f mf ay (ZChain.supf zc) x) (ZChain.chain⊆A zc) (ZChain.f-total zc)
 
-     fixpoint :  ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f )  (zc : ZChain A f mf as0 (& A) )
+     fixpoint :  ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (mf< : <-monotonic-f A f )  (zc : ZChain A f mf as0 (& A) )
             → (sp1 : MinSUP A (ZChain.chain zc))
             → f (MinSUP.sup sp1)  ≡ MinSUP.sup sp1
-     fixpoint f mf zc sp1 = z14 where
+     fixpoint f mf mf< zc sp1 = z14 where
            chain = ZChain.chain zc
            supf = ZChain.supf zc
            sp : Ordinal
@@ -1408,13 +1400,13 @@
            z10 :  {a b : Ordinal } → (ca : odef chain a ) → b o< (& A) → (ab : odef A b )
               →  HasPrev A chain f b  ∨  IsSUP A (UnionCF A f mf as0 (ZChain.supf zc) b) ab
               → * a < * b  → odef chain b
-           z10 = ZChain1.is-max (SZ1 f mf as0 zc (& A) )
+           z10 = ZChain1.is-max (SZ1 f mf mf< as0 zc (& A) )
            z22 : sp o< & A
            z22 = z09 asp
            z12 : odef chain sp
            z12 with o≡? (& s) sp
            ... | yes eq = subst (λ k → odef chain k) eq ( ZChain.chain∋init zc )
-           ... | no ne = ZChain1.is-max (SZ1 f mf as0 zc (& A)) {& s} {sp} ( ZChain.chain∋init zc ) (z09 asp) asp (case2 z19 ) z13 where
+           ... | no ne = ZChain1.is-max (SZ1 f mf mf< as0 zc (& A)) {& s} {sp} ( ZChain.chain∋init zc ) (z09 asp) asp (case2 z19 ) z13 where
                z13 :  * (& s) < * sp
                z13 with MinSUP.x≤sup sp1 ( ZChain.chain∋init zc )
                ... | case1 eq = ⊥-elim ( ne eq )
@@ -1463,7 +1455,7 @@
      z04 nmx zc = <-irr0  {* (cf nmx c)} {* c}
            (subst (λ k → odef A k ) (sym &iso) (proj1 (is-cf nmx (MinSUP.asm  msp1 ))))
            (subst (λ k → odef A k) (sym &iso) (MinSUP.asm msp1) )
-           (case1 ( cong (*)( fixpoint (cf nmx) (cf-is-≤-monotonic nmx ) zc msp1  ))) -- x ≡ f x ̄
+           (case1 ( cong (*)( fixpoint (cf nmx) (cf-is-≤-monotonic nmx ) (cf-is-<-monotonic nmx ) zc msp1  ))) -- x ≡ f x ̄
                 (proj1 (cf-is-<-monotonic nmx c (MinSUP.asm msp1 ))) where          -- x < f x
 
           supf = ZChain.supf zc