# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1655511966 -32400
# Node ID b726eedf9041e34ccab2879a3cbe70831f5120c7
# Parent  50999e72f19f629da8789747c83a3e8b366ae570
nested transfinie on monotonicity

diff -r 50999e72f19f -r b726eedf9041 src/zorn.agda
--- a/src/zorn.agda	Sat Jun 18 00:41:37 2022 +0900
+++ b/src/zorn.agda	Sat Jun 18 09:26:06 2022 +0900
@@ -548,8 +548,8 @@
                      ... | case1 y=b  = subst (λ k → odef chain0 k )  y=b ( ZChain.chain∋x zc0 )
                      ... | case2 y<b  = ZChain.is-max zc0 (ZChain.chain∋x zc0 ) (zc0-b<x b b<x) ab (case2 (z24 p)) y<b
           ... | case2 ¬x=sup =  -- x is not f y' nor sup of former ZChain from y
-                   record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 ; f-next = ZChain.f-next zc0 ; chain∋sup = {!!}
-                     ; initial = ZChain.initial zc0 ; f-immediate = ZChain.f-immediate zc0 ; chain∋x  =  ZChain.chain∋x zc0 ; is-max = z18 ; fc∨sup = {!!} }  where
+                   record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 ; f-next = ZChain.f-next zc0  
+                     ; initial = ZChain.initial zc0 ; f-immediate = ZChain.f-immediate zc0 ; chain∋x  =  ZChain.chain∋x zc0 ; is-max = z18 }  where
                       -- no extention
                 z18 :  {a b : Ordinal} → odef (ZChain.chain zc0) a → b o< osuc x → (ab : odef A b) →
                             HasPrev A (ZChain.chain zc0) ab f ∨ IsSup A (ZChain.chain zc0)   ab →
@@ -586,34 +586,41 @@
          u-chain∋x :  odef Uz y
          u-chain∋x = record { u = y ; u<x = y<x ; chain∋z = ZChain.chain∋x (prev y y<x ay ) }
 
-         ind-mono :  {y : Ordinal } (ay : odef A y ) {a b : Ordinal } ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → (zb : ZChain A y f b) →
-             (x : Ordinal)
-                → ((c : Ordinal) → c o< x → a o≤ b → b o≤ c → (za : ZChain A y f a) {i : Ordinal} → odef (ZChain.chain za) i → odef (ZChain.chain zb) i)
-                → a o≤ b → b o≤ x → (za : ZChain A y f a) {i : Ordinal} → odef (ZChain.chain za) i → odef (ZChain.chain zb) i
-         ind-mono {y} ay {a} {b} f mf zb x prev-mono a≤b b≤x za {i} zai with Oprev-p x
-         ... | yes op = mc00 where
+         ind-mono :  {a b : Ordinal } → (zb : ZChain A y f b) →
+             (z : Ordinal)
+                → ((c : Ordinal) → c o< z → a o≤ b → b o≤ c → (za : ZChain A y f a) {i : Ordinal} → odef (ZChain.chain za) i → odef (ZChain.chain zb) i)
+                → a o≤ b → b o≤ z → (za : ZChain A y f a) {i : Ordinal} → odef (ZChain.chain za) i → odef (ZChain.chain zb) i
+         ind-mono {a} {b} zb z prev-mono a≤b b≤z za {i} zai = mc01 where
+           open ZChain
+           mc01 : odef (chain zb) i
+           mc01 with trio< b z | osuc-≡< b≤z
+           ... | tri< b<z ¬b ¬c | _ = prev-mono b b<z a≤b <-osuc za zai
+           ... | tri> ¬a ¬b b>z | case1 b=z = ⊥-elim ( ¬b b=z )
+           ... | tri> ¬a ¬b b>z | case2 b<z = ⊥-elim ( ¬a b<z )
+           ... | tri≈ ¬a b=z ¬c | _  with Oprev-p z
+           ... | yes op = mc00 where
               open ZChain
-              px = Oprev.oprev op
+              pz = Oprev.oprev op
               zc0 : ZChain A y f (Oprev.oprev op)
-              zc0 = {!!} -- zfx (Oprev.oprev op) ay f mf
+              zc0 = prev pz (subst (λ k → pz o< k) {!!} <-osuc ) ay
               mc00 : odef (chain zb) i
-              mc00 with ODC.∋-p O A (* x)
-              ... | no noax = {!!}
-              ... | yes ax with ODC.p∨¬p O ( HasPrev A (ZChain.chain zc0) ax f )
+              mc00 with ODC.∋-p O A (* z)
+              ... | no noaz = {!!}
+              ... | yes az with ODC.p∨¬p O ( HasPrev A (ZChain.chain zc0) az f )
               ... | case1 pr = {!!}
-              ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain.chain zc0) ax )
-              ... | case1 is-sup = {!!} -- x is a sup of zc0 
-              ... | case2 ¬x=sup  = {!!}
-         ... | no ¬ox with trio< x y
-         ... | tri< a ¬b ¬c = {!!}
-         ... | tri≈ ¬a b ¬c = {!!}
-         ... | tri> ¬a ¬b y<x = {!!}
+              ... | case2 ¬fy<z with ODC.p∨¬p O (IsSup A (ZChain.chain zc0) az )
+              ... | case1 is-sup = {!!} -- z is a sup of zc0 
+              ... | case2 ¬z=sup  = {!!}
+           ... | no ¬oz with trio< z y
+           ... | tri< a ¬b ¬c = {!!}
+           ... | tri≈ ¬a b ¬c = {!!}
+           ... | tri> ¬a ¬b y<z = {!!}
     
-         chain-mono :  {x y : Ordinal} (ay : odef A y)  ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f ) { a b : Ordinal }
+         chain-mono : { a b : Ordinal }
               → (zx : ZChain A y f a ) → (zy : ZChain A y f b)  → a o≤ b → b o< osuc x →  ZChain.chain zx ⊆' ZChain.chain zy
-         chain-mono {x} {y} ay f mf {a} {b} za zb a≤b b≤x = TransFinite {λ x →  
+         chain-mono {a} {b} za zb a≤b b≤x = TransFinite {λ x →  
              a o≤ b → b o≤ x  → (za : ZChain A y f a) → {i : Ordinal } → odef (ZChain.chain za) i → odef (ZChain.chain zb) i }
-             (ind-mono ay f mf zb) x a≤b b≤x za  
+             (ind-mono zb) x a≤b b≤x za  
 
          u-mono :  ( a b : Ordinal ) → b o< osuc x → a o< osuc b → (za : ZChain A y f a) (zb : ZChain A y f b) → ZChain.chain za  ⊆' ZChain.chain zb
          u-mono a b b≤x a≤b za zb {i} zai = {!!} -- chain-mono ay f mf za zb a≤b  b≤x zai