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

diff -r 7fff07748fde -r e1c6c32efe01 src/zorn.agda
--- a/src/zorn.agda	Mon Jul 25 18:13:43 2022 +0900
+++ b/src/zorn.agda	Mon Jul 25 21:21:29 2022 +0900
@@ -323,8 +323,14 @@
      ct-ind : (xa xb : Ordinal) → {a b : Ordinal} → UChain A f mf ay supf xa a → UChain A f mf ay supf xb b → Tri (* a < * b) (* a ≡ * b) (* b < * a)
      ct-ind xa xb {a} {b} (ch-init fca) (ch-init fcb) = fcn-cmp y f mf fca fcb
      ct-ind xa xb {a} {b} (ch-init fca) (ch-is-sup ub supb fcb) with ChainP.fcy<sup supb fca
-     ... | case1 eq = ?
+     ... | 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
+          ct00 : * a ≡ * b
+          ct00 = trans (cong (*) eq) eq1
      ... | case2 lt = tri< ct01  (λ eq → <-irr (case1 (sym eq)) ct01) (λ lt → <-irr (case2 ct01) lt)  where
+          ct01 : * a < * b 
+          ct01 = subst (λ k → * k < * b ) (sym eq) lt
+     ct-ind xa xb {a} {b} (ch-init fca) (ch-is-sup ub supb fcb) | case2 lt = tri< ct01  (λ eq → <-irr (case1 (sym eq)) ct01) (λ lt → <-irr (case2 ct01) lt)  where
           ct00 : * a < * (supf ub)
           ct00 = lt
           ct01 : * a < * b 
@@ -332,8 +338,14 @@
           ... | case1 eq =  subst (λ k → * a < k ) eq ct00
           ... | case2 lt =  IsStrictPartialOrder.trans POO ct00 lt
      ct-ind xa xb {a} {b} (ch-is-sup ua supa fca) (ch-init fcb) with ChainP.fcy<sup supa fcb
-     ... | case1 eq = ?
+     ... | 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
+          ct00 : * a ≡ * b
+          ct00 = sym (trans (cong (*) eq) eq1 )
      ... | case2 lt = tri> (λ lt → <-irr (case2 ct01) lt) (λ eq → <-irr (case1 eq) ct01) ct01    where
+          ct01 : * b < * a 
+          ct01 = subst (λ k → * k < * a ) (sym eq) lt
+     ct-ind xa xb {a} {b} (ch-is-sup ua supa fca) (ch-init fcb) | case2 lt = tri> (λ lt → <-irr (case2 ct01) lt) (λ eq → <-irr (case1 eq) ct01) ct01    where
           ct00 : * b < * (supf ua)
           ct00 = lt
           ct01 : * b < * a 
@@ -342,8 +354,14 @@
           ... | 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
      ... | tri< a₁ ¬b ¬c with ChainP.order supb  a₁ (ChainP.csupz supa)
-     ... | case1 eq = ?
-     ... | case2 lt = tri< ct02  (λ eq → <-irr (case1 (sym eq)) ct02) (λ lt → <-irr (case2 ct02) lt)  where
+     ... | 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
+          ct00 : * a ≡ * b
+          ct00 = trans (cong (*) eq) eq1
+     ... | case2 lt =  tri< ct02  (λ eq → <-irr (case1 (sym eq)) ct02) (λ lt → <-irr (case2 ct02) lt)  where
+          ct02 : * a < * b 
+          ct02 = subst (λ k → * k < * b ) (sym eq) lt
+     ct-ind xa xb {a} {b} (ch-is-sup ua supa fca) (ch-is-sup ub supb fcb) | tri< a₁ ¬b ¬c | case2 lt = tri< ct02  (λ eq → <-irr (case1 (sym eq)) ct02) (λ lt → <-irr (case2 ct02) lt)  where
           ct03 : * a < * (supf ub)
           ct03 = lt
           ct02 : * a < * b 
@@ -352,8 +370,14 @@
           ... | 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 ¬b c with ChainP.order supa c (ChainP.csupz supb)
-     ... | case1 eq = ?
-     ... | case2 lt = tri> (λ lt → <-irr (case2 ct04) lt) (λ eq → <-irr (case1 (eq)) ct04) ct04    where
+     ... | 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
+          ct00 : * a ≡ * b
+          ct00 = sym (trans (cong (*) eq) eq1)
+     ... | case2 lt =  tri> (λ lt → <-irr (case2 ct02) lt) (λ eq → <-irr (case1 eq) ct02) ct02    where
+          ct02 : * b < * a 
+          ct02 = subst (λ k → * k < * a ) (sym eq) lt
+     ct-ind xa xb {a} {b} (ch-is-sup ua supa fca) (ch-is-sup ub supb fcb) | tri> ¬a ¬b c | case2 lt = tri> (λ lt → <-irr (case2 ct04) lt) (λ eq → <-irr (case1 (eq)) ct04) ct04    where
           ct05 : * b < * (supf ua)
           ct05 = lt
           ct04 : * b < * a 
@@ -480,7 +504,7 @@
                     ... | ch-is-sup u is-sup-a fc with trio< u px
                     ... | tri< a ¬b ¬c    = ⟪ proj1 ua , ch-is-sup u  is-sup-a fc ⟫ -- u o< osuc x
                     ... | tri≈ ¬a u=px ¬c = ⟪ proj1 ua , ch-is-sup u  is-sup-a fc ⟫
-                    ... | tri> ¬a ¬b c = ⊥-elim (<-irr u≤a (ptrans a<b ? ) ) where
+                    ... | tri> ¬a ¬b c = m08 where
                          --  a and b is a sup of chain, order forces minimulity of sup
                          su=u : ZChain.supf zc u ≡ u
                          su=u = ChainP.supfu=u is-sup-a 
@@ -493,8 +517,10 @@
                          fcb : FClosure A f (ZChain.supf zc b) b
                          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 )
-                         b<u : b <= u
-                         b<u = subst (λ k → b <= k ) su=u ( ZChain.order zc u<A (ordtrans b<px c)  fcb )
+                         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 )
+                         ... | 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
                     m04 = ZChain1.is-max (prev px px<x) m03 b<px ab 
                          (case2 record {x<sup = λ {z} lt → IsSup.x<sup is-sup (chain-mono2 x ( o<→≤  (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ))  o≤-refl lt)  } ) a<b
@@ -614,7 +640,7 @@
      ysup f mf {y} ay = supP (uchain f mf ay) (λ lt → A∋fc y f mf lt)  (utotal f mf ay) 
 
      inititalChain : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → ZChain A f mf ay o∅
-     inititalChain f mf {y} ay = record { supf = isupf ; chain⊆A = λ lt → proj1 lt ; chain∋init = cy ; csupf = ? ; fcy<sup = ? 
+     inititalChain f mf {y} ay = record { supf = isupf ; chain⊆A = λ lt → proj1 lt ; chain∋init = cy ; csupf = csupf ; fcy<sup = ? 
       ; initial = isy ; f-next = inext ; f-total = itotal ; sup=u = λ _ b<0 → ⊥-elim (¬x<0 b<0) ; order = λ b<0 → ⊥-elim (¬x<0 b<0) } where
           spi =  & (SUP.sup (ysup f mf ay))
           isupf : Ordinal → Ordinal
@@ -627,7 +653,7 @@
           isy : {z : Ordinal } → odef (UnionCF A f mf ay isupf o∅) z → * y ≤ * z
           isy {z} ⟪ az , uz ⟫ with uz 
           ... | ch-init fc = s≤fc y f mf fc 
-          ... | ch-is-sup u is-sup fc = ≤-ftrans (subst (λ k → * y ≤ k) (sym *iso) y<sup)  (s≤fc (& (SUP.sup (ysup f mf ay))) f mf ? )
+          ... | ch-is-sup u is-sup fc = ≤-ftrans (subst (λ k → * y ≤ k) (sym *iso) y<sup)  (s≤fc (& (SUP.sup (ysup f mf ay))) f mf fc )
           inext : {a : Ordinal} → odef (UnionCF A f mf ay isupf o∅) a → odef (UnionCF A f mf ay isupf o∅) (f a)
           inext {a} ua with (proj2 ua)
           ... | ch-init fc = ⟪ proj2 (mf _ (proj1 ua))  , ch-init (fsuc _ fc )  ⟫