# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1658759918 -32400
# Node ID 34678c0ad2788dee4a58c9788223a7d3368ffd03
# Parent  67c7d4b43844eb0f5819579376d8520555a9750d
...

diff -r 67c7d4b43844 -r 34678c0ad278 src/zorn.agda
--- a/src/zorn.agda	Mon Jul 25 22:53:11 2022 +0900
+++ b/src/zorn.agda	Mon Jul 25 23:38:38 2022 +0900
@@ -264,7 +264,7 @@
       csupz    : FClosure A f (supf u) z 
       supfu=u  : supf u ≡ u 
       fcy<sup  : {z : Ordinal } → FClosure A f y z → (z ≡ supf u) ∨ ( z << supf u ) 
-      order    : {sup1 z1 : Ordinal} → (lt : sup1 o< u ) → FClosure A f (supf sup1 ) z1 → (z1 ≡ supf u ) ∨ ( z1 << supf u )
+      order    : {sup1 z1 : Ordinal} → (lt : supf sup1 o< supf u ) → FClosure A f (supf sup1 ) z1 → (z1 ≡ supf u ) ∨ ( z1 << supf u )
 
 -- Union of supf z which o< x
 --
@@ -296,10 +296,11 @@
       f-next : {a : Ordinal } → odef chain a → odef chain (f a)
       f-total : IsTotalOrderSet chain
 
+      supf-mono : { a b : Ordinal } → a o< b → supf a o≤ supf b
       csupf : {z : Ordinal } → odef chain (supf z) 
       sup=u : {b : Ordinal} → (ab : odef A b) → b o< z  → IsSup A (UnionCF A f mf ay supf (osuc b)) ab → supf b ≡ b 
       fcy<sup  : {u w : Ordinal } → u o< z  → FClosure A f init w → (w ≡ supf u ) ∨ ( w << supf u ) -- different from order because y o< supf 
-      order : {b sup1 z1 : Ordinal} → b o< z → sup1 o< b → FClosure A f (supf sup1) z1 → (z1 ≡ supf b) ∨ (z1 << supf b)
+      order : {b sup1 z1 : Ordinal} → b o< z → supf sup1 o< supf b → FClosure A f (supf sup1) z1 → (z1 ≡ supf b) ∨ (z1 << supf b)
 
 
 record ZChain1 ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) 
@@ -352,7 +353,7 @@
           ct01 with s≤fc (supf ua) f mf fca
           ... | case1 eq =  subst (λ k → * b < k ) eq ct00
           ... | case2 lt =  IsStrictPartialOrder.trans POO ct00 lt
-     ct-ind xa xb {a} {b} (ch-is-sup ua supa fca) (ch-is-sup ub supb fcb) with trio< ua ub
+     ct-ind xa xb {a} {b} (ch-is-sup ua supa fca) (ch-is-sup ub supb fcb) with trio< (supf ua) (supf ub)
      ... | tri< a₁ ¬b ¬c with ChainP.order supb  a₁ (ChainP.csupz supa)
      ... | case1 eq with s≤fc (supf ub) f mf fcb 
      ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00  (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where
@@ -368,7 +369,8 @@
           ct02 with s≤fc (supf ub) f mf fcb
           ... | case1 eq =  subst (λ k → * a < k ) eq ct03
           ... | case2 lt =  IsStrictPartialOrder.trans POO ct03 lt
-     ct-ind xa xb {a} {b} (ch-is-sup ua supa fca) (ch-is-sup ub supb fcb) | tri≈ ¬a  refl ¬c = fcn-cmp (supf ua) f mf fca fcb
+     ct-ind xa xb {a} {b} (ch-is-sup ua supa fca) (ch-is-sup ub supb fcb) | tri≈ ¬a  eq ¬c 
+         = fcn-cmp (supf ua) f mf fca (subst (λ k → FClosure A f k b ) (sym eq) fcb )
      ct-ind xa xb {a} {b} (ch-is-sup ua supa fca) (ch-is-sup ub supb fcb) | tri> ¬a ¬b c with ChainP.order supa c (ChainP.csupz supb)
      ... | case1 eq with s≤fc (supf ua) f mf fca 
      ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00  (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where
@@ -518,7 +520,9 @@
                          fcb = subst (λ k → FClosure A f k b ) (sym (ZChain.sup=u zc ab (z09 ab) 
                             (record {x<sup = λ {z} lt → IsSup.x<sup is-sup (chain-mono2 x m07 o≤-refl lt)  } ) )) ( init ab )
                          m08 :  odef (UnionCF A f mf ay (ZChain.supf zc) px) a 
-                         m08 with subst (λ k → b <= k ) su=u ( ZChain.order zc u<A (ordtrans b<px c)  fcb )
+                         m08 with osuc-≡<  (ZChain.supf-mono zc (ordtrans b<px c))
+                         ... | case1 eq = ?
+                         ... | case2 lt  with subst (λ k → b <= k ) su=u ( ZChain.order zc u<A lt fcb )
                          ... | case2 b<u = ⊥-elim (<-irr u≤a (ptrans a<b b<u ) ) 
                          ... | case1 eq = ⊥-elim ( <-irr (s≤fc u f mf (subst (λ k → FClosure A f k a ) su=u fc )) (subst (λ k → * a < * k) eq a<b ))
                     m04 : odef (UnionCF A f mf ay (ZChain.supf zc) px) b
@@ -532,11 +536,12 @@
                       record { x<sup = λ {z} uz → IsSup.x<sup is-sup (chain-mono2 x (osucc b<x) o≤-refl uz )  }  )
                     m08 : {z : Ordinal} → (fcz : FClosure A f y z ) → z <= ZChain.supf zc b
                     m08 {z} fcz = ZChain.fcy<sup zc b<A fcz
-                    m09 : {sup1 z1 : Ordinal} → sup1 o< b → FClosure A f (ZChain.supf zc sup1) z1 → z1 <= ZChain.supf zc b
-                    m09 {sup1} {z} s<b fcz = ZChain.order zc b<A s<b fcz
+                    m09 : {sup1 z1 : Ordinal} → (ZChain.supf zc sup1) o< (ZChain.supf zc b) 
+                           → FClosure A f (ZChain.supf zc sup1) z1 → z1 <= ZChain.supf zc b
+                    m09 {sup1} {z} s<b fcz = ZChain.order zc b<A ? fcz
                     m06 : ChainP A f mf ay (ZChain.supf zc) b b
                     m06 = record { csupz = subst (λ k → FClosure A f k b) m05 (init ab) ; supfu=u = sym m05 
-                      ; fcy<sup = m08  ; order = m09 }
+                      ; fcy<sup = m08  ; order = m09 } 
         ... | no lim = record { is-max = is-max }  where
            is-max :  {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) x) a →
               b o< x → (ab : odef A b) →
@@ -551,13 +556,14 @@
                  m09 = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) ab))
                  m07 : {z : Ordinal} → FClosure A f y z → z <= ZChain.supf zc b
                  m07 {z} fc = ZChain.fcy<sup zc m09 fc
-                 m08 : {sup1 z1 : Ordinal} → sup1 o< b → FClosure A f (ZChain.supf zc sup1) z1 → z1 <= ZChain.supf zc b
+                 m08 : {sup1 z1 : Ordinal} → (ZChain.supf zc sup1) o< (ZChain.supf zc b) 
+                       → FClosure A f (ZChain.supf zc sup1) z1 → z1 <= ZChain.supf zc b
                  m08 {sup1} {z1} s<b fc = ZChain.order zc m09 s<b fc
                  m05 : b ≡ ZChain.supf zc b
                  m05 = sym (ZChain.sup=u zc ab m09
                       record { x<sup = λ lt → IsSup.x<sup is-sup (chain-mono2 x (o<→≤ (ob<x lim b<x)) o≤-refl lt )} )   -- ZChain on x
                  m06 : ChainP A f mf ay (ZChain.supf zc) b b
-                 m06 = record { fcy<sup = m07 ; csupz = subst (λ k →  FClosure A f k b ) m05 (init ab) ; order = m08 
+                 m06 = record { fcy<sup = m07 ; csupz = subst (λ k →  FClosure A f k b ) m05 (init ab) ; order = m08
                        ; supfu=u = sym m05 }
                  m04 : odef (UnionCF A f mf ay (ZChain.supf zc) (osuc b)) b
                  m04 = ⟪ ab , ch-is-sup b  m06 (subst (λ k → FClosure A f k b) m05 (init ab))  ⟫
@@ -674,10 +680,10 @@
                   & (* z) ≡⟨ cong (&) eq  ⟩
                   spi  ∎ ) where open ≡-Reasoning
                ... | case2 lt = case2 (subst (λ k → * z < k ) (sym *iso) lt )
-               uz04 : {sup1 z1 : Ordinal} → sup1 o< spi → FClosure A f (isupf sup1) z1 → (z1 ≡ isupf spi) ∨ (z1 << isupf spi)
-               uz04 {s} {z} s<spi fcz = ?
+               uz04 : {sup1 z1 : Ordinal} → isupf sup1 o< isupf spi → FClosure A f (isupf sup1) z1 → (z1 ≡ isupf spi) ∨ (z1 << isupf spi)
+               uz04 {s} {z} s<spi fcz = ⊥-elim ( o<¬≡ refl s<spi )
                uz02 :  ChainP A f mf ay isupf spi (isupf z)
-               uz02 = record { csupz = init asi ; supfu=u = refl ; fcy<sup = uz03 ; order = ? }
+               uz02 = record { csupz = init asi ; supfu=u = refl ; fcy<sup = uz03 ; order = λ {s} {z} → uz04 {s} {z} }
 
 
      --