# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1657402494 -32400
# Node ID 6814fc4e79987bf368358385db1b1d03056eb82f
# Parent  663b34227faf586d55da590cf86c6182b8b3c2ea
...

diff -r 663b34227faf -r 6814fc4e7998 src/OrdUtil.agda
--- a/src/OrdUtil.agda	Sat Jul 09 21:51:39 2022 +0900
+++ b/src/OrdUtil.agda	Sun Jul 10 06:34:54 2022 +0900
@@ -173,6 +173,12 @@
 ... | tri≈ ¬a b ¬c = yes (o≤-refl0 b)
 ... | tri> ¬a ¬b c = no (λ n → osuc-< n c )
 
+o¬≤→< : {x z : Ordinal} →  ¬ (x o< osuc z) → z o< x
+o¬≤→< {x} {z} not with trio< z x
+... | tri< a ¬b ¬c = a
+... | tri≈ ¬a b ¬c = ⊥-elim (not (o≤-refl0 (sym b)))
+... | tri> ¬a ¬b c = ⊥-elim (not (o<→≤ c ))
+
 OrdTrans :  Transitive  _o≤_
 OrdTrans a≤b b≤c with osuc-≡< a≤b | osuc-≡< b≤c
 OrdTrans a≤b b≤c | case1 refl | case1 refl = <-osuc
diff -r 663b34227faf -r 6814fc4e7998 src/zorn.agda
--- a/src/zorn.agda	Sat Jul 09 21:51:39 2022 +0900
+++ b/src/zorn.agda	Sun Jul 10 06:34:54 2022 +0900
@@ -430,37 +430,62 @@
           pchain : HOD
           pchain  = chainf sc px
 
-          no-ext : ZChain1 A f mf ay x
-          no-ext = record { psup = ZChain1.psup sc ; p≤z = ZChain1.p≤z sc ; chainf = ZChain1.chainf sc 
-              ; is-chain = ZChain1.is-chain sc ; psup-mono = sc0 } where
-            sc0 : (z : Ordinal) → z o≤ x → chainf sc z ⊆' chainf sc x
-            sc0 = ?
+          no-ext :  ZChain1 A f mf ay x
+          no-ext = record { psup = psup1 ; p≤z = p≤z1 ; chainf = chainf1 ; is-chain = is-chain1 ; psup-mono = sc0 }  where
+            psup1 : Ordinal → Ordinal
+            psup1 z with o≤? z x
+            ... | yes _ = ZChain1.psup sc z
+            ... | no _ = ZChain1.psup sc x
+            p≤z1 : (z : Ordinal ) → odef A (psup1 z)
+            p≤z1 z with o≤? z x
+            ... | yes _  = ZChain1.p≤z sc z
+            ... | no _  = ZChain1.p≤z sc x
+            chainf1 : (z : Ordinal ) → HOD
+            chainf1 z with o≤? z x
+            ... | yes _  = ZChain1.chainf sc z
+            ... | no _ = ZChain1.chainf sc x
+            sc0 : (z : Ordinal) → z o≤ x → chainf1 z ⊆' chainf1 x
+            sc0 z = ?
+            is-chain1 : ?
+            is-chain1 = ?
           sc4 : ZChain1 A f mf ay x
           sc4 with ODC.∋-p O A (* x)
-          ... | no noax = record { psup = ZChain1.psup sc ; p≤z = ? ; chainf = ? ; is-chain = ? ; psup-mono = ? }
+          ... | no noax = no-ext
           ... | yes ax with ODC.p∨¬p O ( HasPrev A pchain ax f )   
-          ... | case1 pr = record { psup = ZChain1.psup sc ; p≤z = ? ; chainf = ? ; is-chain = ? ; psup-mono = ? }
+          ... | case1 pr = no-ext
           ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A pchain ax )
           ... | case1 is-sup = record { psup = ? ; p≤z = ? ; chainf = ? ; is-chain = ? ; psup-mono = ? } where
                 schain : HOD
                 schain = ? -- record { od = record { def = λ z → odef A z ∧ ( odef (ZChain1.chain sc ) z ∨ (FClosure A f x z)) } 
                     -- ; odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy }
-          ... | case2 ¬x=sup = record { psup = ZChain1.psup sc ; p≤z = ? ; chainf = ? ; is-chain = ? ; psup-mono = ? }
+          ... | case2 ¬x=sup = no-ext
      ... | no ¬ox = sc4 where
           pchainf : (z : Ordinal) → z o< x → HOD
           pchainf z z<x = ZChain1.chainf (prev z z<x) z
+          pzc : (z : Ordinal) → z o< x → ZChain1 A f mf ay z
+          pzc z z<x = prev z z<x
           UZ : HOD
           UZ = UnionCF A x pchainf
-          sc4 : ZChain1 A f mf ay x
-          sc4 with o≤? x o∅
-          ... | yes x=0 = record { psup = ? ; p≤z = ? ; chainf = ? ; is-chain = ? ; psup-mono = ? }
-          ... | no 0<x with ODC.∋-p O A (* x)
-          ... | no noax = record { psup = ? ; p≤z = ? ; chainf = ? ; is-chain = ? ; psup-mono = ? }
-          ... | yes ax with ODC.p∨¬p O ( HasPrev A (UnionCF A x pchainf) ax f )   
-          ... | case1 pr = record { psup = ? ; p≤z = ? ; chainf = ? ; is-chain = ? ; psup-mono = ? }
-          ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (UnionCF A x pchainf) ax )
-          ... | case1 is-sup = ?
-          ... | case2 ¬x=sup = ?
+          usup : SUP A UZ
+          usup = supP UZ ? ? 
+          sc4 :  ZChain1 A f mf ay x
+          sc4 = record { psup = psup1 ; p≤z = p≤z1 ; chainf = chainf1 ; is-chain = is-chain1 ; psup-mono = sc0 }  where
+            psup1 : Ordinal → Ordinal
+            psup1 z with o≤? x z
+            ... | yes _ = ?
+            ... | no z<x = ZChain1.psup (pzc z (o¬≤→< z<x)) z
+            p≤z1 : (z : Ordinal ) → odef A (psup1 z)
+            p≤z1 z with o≤? x z
+            ... | yes _  = ?
+            ... | no z<x  = ZChain1.p≤z (pzc z (o¬≤→< z<x)) z
+            chainf1 : (z : Ordinal ) → HOD
+            chainf1 z with o≤? x z
+            ... | yes _  = UZ
+            ... | no z<x = ZChain1.chainf (pzc z (o¬≤→< z<x)) z
+            sc0 : (z : Ordinal) → z o≤ x → chainf1 z ⊆' chainf1 x
+            sc0 z = ?
+            is-chain1 : ?
+            is-chain1 = ?
 
      ind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → (x : Ordinal) 
          → (zc0 : (x : Ordinal) →  ZChain1 A f mf ay x) 
@@ -623,6 +648,8 @@
           uzc {z} u =  prev (UChain.u u) (UChain.u<x u) 
           Uz : HOD
           Uz = record { od = record { def = λ z → odef A z ∧ ( UChain x supf z ∨ FClosure A f y z ) } ; odmax = & A ; <odmax = {!!}  }
+          Uzchain : ¬ (odef (ZChain1.chainf (zc0 (& A) ) x) x) → ZChain A f mf ay zc0 x
+          Uzchain nz = record { chain-mono = ?  ; chain⊆A = ? ; chain∋init = ? ; initial = ? ; f-next = ? ; f-total = ? ; is-max = ? }
           zc5 : ZChain A f mf ay zc0 x 
           zc5 with o≤? x o∅
           ... | yes x=0 = ?