# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1658473711 -32400
# Node ID c3388f0e9899e1286d801cc26c97177b7a6b10cc
# Parent  6c8ba542d11bda16c4ef730e17622f1c997b76d3
...

diff -r 6c8ba542d11b -r c3388f0e9899 src/zorn.agda
--- a/src/zorn.agda	Fri Jul 22 10:15:05 2022 +0900
+++ b/src/zorn.agda	Fri Jul 22 16:08:31 2022 +0900
@@ -322,8 +322,6 @@
      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 ub<x supb fcb) = tri< ct01  (λ eq → <-irr (case1 (sym eq)) ct01) (λ lt → <-irr (case2 ct01) lt)  where
-          ct02 : * a < * (supf xb)
-          ct02 = ? -- ChainP.fcy<sup supb fca
           ct00 : * a < * (supf ub)
           ct00 = ChainP.fcy<sup supb fca
           ct01 : * a < * b 
@@ -331,10 +329,10 @@
           ... | 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 ua<x supa fca) (ch-init fcb)= tri> (λ lt → <-irr (case2 ct01) lt) (λ eq → <-irr (case1 eq) ct01) ct01    where
-          ct00 : * b < * (supf xa)
-          ct00 = ? -- ChainP.fcy<sup supa fcb
+          ct00 : * b < * (supf ua)
+          ct00 = ChainP.fcy<sup supa fcb
           ct01 : * b < * a 
-          ct01 with s≤fc (supf xa) f mf ? --  fca
+          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 ua<x supa fca) (ch-is-sup ub ub<x supb fcb) with trio< ua ub
@@ -345,12 +343,12 @@
           ct02 with s≤fc (supf ub) f mf fcb
           ... | case1 eq =  subst (λ k → * a < k ) eq ct03
           ... | case2 lt =  IsStrictPartialOrder.trans POO ct03 lt
-     ... | tri≈ ¬a  refl ¬c = fcn-cmp (supf xa) f mf ? ?
+     ... | tri≈ ¬a  refl ¬c = fcn-cmp (supf ua) f mf fca fcb
      ... | tri> ¬a ¬b c = tri> (λ lt → <-irr (case2 ct04) lt) (λ eq → <-irr (case1 (eq)) ct04) ct04    where
-          ct05 : * b < * (supf xa)
-          ct05 = ? --  ChainP.order supa ? (ChainP.csupz supb)
+          ct05 : * b < * (supf ua)
+          ct05 = ChainP.order supa c (ChainP.csupz supb)
           ct04 : * b < * a 
-          ct04 with s≤fc (supf xa) f mf ? -- fca
+          ct04 with s≤fc (supf ua) f mf fca
           ... | case1 eq =  subst (λ k → * b < k ) eq ct05
           ... | case2 lt =  IsStrictPartialOrder.trans POO ct05 lt
 
@@ -431,31 +429,24 @@
         chain-mono2 x {a} {b} {c} a≤b b≤x ⟪ ua , ch-init fc  ⟫ = 
             ⟪ ua , ch-init fc  ⟫ 
         chain-mono2 x {a} {b} {c} a≤b b≤x ⟪ uaa ,  ch-is-sup ua u<x is-sup fc  ⟫ = 
-            ⟪ uaa , ch-is-sup ua ? is-sup fc  ⟫ 
+            ⟪ uaa , ch-is-sup ua (ordtrans<-≤ u<x a≤b ) is-sup fc  ⟫ 
         chain<ZA : {x : Ordinal } → UnionCF A f mf ay (ZChain.supf zc) x ⊆' UnionCF A f mf ay (ZChain.supf zc) (& A)
         chain<ZA {x} ux with proj2 ux
         ... | ch-init fc = ⟪ proj1 ux , ch-init fc ⟫
-        ... | ch-is-sup u pu<x is-sup fc = ⟪ proj1 ux , ? ⟫ where
-            u<A : (& ( * ( ZChain.supf zc x)))  o< & A
-            u<A = ? -- c<→o< (subst (λ k → odef A k ) (sym &iso) (A∋fcs _ f mf fc) )
-            u<x :  ZChain.supf zc x o< & A
-            u<x = ? -- subst (λ k → k o< & A ) (trans &iso (ChainP.supfu=u is-sup)) ? -- u<A
+        ... | ch-is-sup u pu<x is-sup fc = ⟪ proj1 ux , ch-is-sup u u<x is-sup fc ⟫ where
+            u<A : (& ( * ( ZChain.supf zc u)))  o< & A
+            u<A = c<→o< (subst (λ k → odef A k ) (sym &iso) (A∋fcs _ f mf fc) )
+            u<x :  u o< & A
+            u<x = subst (λ k → k o< & A ) (trans &iso (ChainP.supfu=u is-sup)) u<A
         is-max-hp : (x : Ordinal) {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) x) a →
             b o< x → (ab : odef A b) →
             HasPrev A (UnionCF A f mf ay (ZChain.supf zc) x) ab f → 
             * a < * b → odef (UnionCF A f mf ay (ZChain.supf zc) x) b
-        is-max-hp x {a} {b} ua b<x ab has-prev a<b = m04 where
-            m04 : odef (UnionCF A f mf ay (ZChain.supf zc) x) b
-            m04 = ⟪ m07   , subst (λ k → UChain A f mf ay (ZChain.supf zc) ? k) (sym (HasPrev.x=fy has-prev)) m08  ⟫ where
-                m06 : odef (UnionCF A f mf ay (ZChain.supf zc) x) (HasPrev.y has-prev )
-                m06 = HasPrev.ay has-prev
-                m07 : odef A b 
-                m07 = subst (λ k → odef A k ) (sym (HasPrev.x=fy has-prev)) (proj2 (mf _ (proj1 m06) ))
-                m08 :  UChain A f mf ay (ZChain.supf zc) ? (f ( HasPrev.y has-prev ))
-                m08 with proj2 m06
-                ... | ch-init fc  = 
-                          ch-init (fsuc _ fc) 
-                ... | ch-is-sup u u<x is-sup fc  = ? -- ch-is-sup u u<x (ChainP-next A f mf ay _ is-sup) (fsuc _ fc) 
+        is-max-hp x {a} {b} ua b<x ab has-prev a<b with HasPrev.ay has-prev
+        ... | ⟪ ab0 , ch-init fc ⟫ = ⟪ ab , ch-init ( subst (λ k → FClosure A f y k) (sym (HasPrev.x=fy has-prev)) (fsuc _ fc )) ⟫ 
+        ... | ⟪ ab0 , ch-is-sup u u<x is-sup fc ⟫ = ⟪ ab , 
+                 subst (λ k → UChain A f mf ay (ZChain.supf zc) x k )
+                      (sym (HasPrev.x=fy has-prev)) ( ch-is-sup u u<x (ChainP-next A f mf ay _ is-sup) (fsuc _ fc))  ⟫ 
         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
         ... | yes op = record { is-max = is-max ; chain-mono2 = chain-mono2 x ; fcy<sup = ? ; sup=u = ? ; order = ? } where
@@ -477,7 +468,13 @@
                  ... | tri> ¬a ¬b c = ⊥-elim (¬p<x<op ⟪ c , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x  ⟫)
                  ... | tri< b<px ¬b ¬c = chain-mono2 x ( o<→≤  (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ))  o≤-refl m04 where
                     m03 :  odef (UnionCF A f mf ay (ZChain.supf zc) px) a
-                    m03 = ⟪ proj1 ua , ? ⟫
+                    m03 with proj2 ua
+                    ... | ch-init fc = ⟪ proj1 ua ,  ch-init fc ⟫
+                    ... | ch-is-sup u u<x is-sup fc with trio< u px
+                    ... | tri< a ¬b ¬c = ⟪ proj1 ua , ch-is-sup u a is-sup fc ⟫
+                    ... | tri≈ ¬a b ¬c = ?
+                    ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) u<x ⟫ )
+                    -- = ⟪ proj1 ua , ? ⟫
                     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
@@ -633,18 +630,13 @@
           pchain⊆A : {y : Ordinal} → odef pchain y →  odef A y
           pchain⊆A {y} ny = proj1 ny
           pnext : {a : Ordinal} → odef pchain a → odef pchain (f a)
-          pnext {a} ⟪ aa , ua ⟫ = ⟪ afa , fua  ⟫ where
-               afa : odef A ( f a )
-               afa = proj2 ( mf a aa )
-               fua : UChain A f mf ay (ZChain.supf zc)  ? (f a)
-               fua = ? -- with ? 
-               -- ... | ch-init fc = ch-init  ( fsuc _ fc )
-               --- ... | ch-is-sup u is-sup fc = ch-is-sup ? (ChainP-next A f mf ay _ is-sup ) (fsuc _ fc )
+          pnext {a} ⟪ aa , ch-init fc ⟫ = ⟪ proj2 (mf a aa) , ch-init (fsuc _ fc)  ⟫
+          pnext {a} ⟪ aa , ch-is-sup u u<x is-sup fc ⟫ = ⟪ proj2 (mf a aa) , ch-is-sup u u<x (ChainP-next A f mf ay _ is-sup ) (fsuc _ fc ) ⟫
           pinit :  {y₁ : Ordinal} → odef pchain y₁ → * y ≤ * y₁
           pinit {a} ⟪ aa , ua ⟫  with  ua
           ... | ch-init fc = s≤fc y f mf fc
           ... | ch-is-sup u u<x is-sup fc = ≤-ftrans (case2 zc7) (s≤fc _ f mf fc)  where
-               zc7 : y << (ZChain.supf zc) ? -- (UChain.u ua)
+               zc7 : y << (ZChain.supf zc) u 
                zc7 = ChainP.fcy<sup is-sup (init ay)
           pcy : odef pchain y
           pcy = ⟪ ay , ch-init (init ay)    ⟫
@@ -665,11 +657,8 @@
                      pc20 : {z : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) (Oprev.oprev op)) z → (z ≡ b) ∨ (z << b)
                      pc20 {z} ⟪ az , ch-init fc  ⟫ = 
                          IsSup.x<sup is-sup ⟪ az ,  ch-init fc  ⟫ 
-                     pc20 {z} ⟪ az , ch-is-sup u u<x is-sup-c fc  ⟫ = ? -- with u<x 
-                     -- ... | case2 u=0 = ?
-                     -- ... | case1 u<px = IsSup.x<sup is-sup ⟪ az , ch-is-sup
-                     --   (case1 (subst (λ k → ? o< k) (Oprev.oprev=x op) (ordtrans u<px <-osuc)))
-                     --   is-sup-c fc  ⟫ 
+                     pc20 {z} ⟪ az , ch-is-sup u u<x is-sup-c fc  ⟫ = IsSup.x<sup is-sup 
+                         ⟪ az , ch-is-sup u (subst (λ k → u o< k) (Oprev.oprev=x op) (ordtrans u<x <-osuc)) is-sup-c fc  ⟫ 
               ... | tri≈ ¬a refl ¬c = ?
               ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → b o< k ) (sym (Oprev.oprev=x op))  b<x  ⟫ )
               order : {b sup1 z1 : Ordinal} → b o< x → sup1 o< b → FClosure A f (supf0 sup1) z1 → z1 << supf0 b
@@ -678,18 +667,6 @@
               ... | tri≈ ¬a refl ¬c = ?
               ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → b o< k ) (sym (Oprev.oprev=x op))  b<x  ⟫ )
 
-          -- chain-x : ( {z : Ordinal} → (az : odef pchain z) → ¬ ( (proj2 az) ≡ px  )) → pchain ⊆' UnionCF A f mf ay (ZChain.supf zc) px
-          -- chain-x ne {z} ⟪ az , record { u = u ; u<x = case2 u=y ; uchain = uc } ⟫ = 
-          --     ⟪ az , record { u = u ; u<x = case2 u=y ; uchain = uc } ⟫ 
-          -- chain-x ne {z} ⟪ az , record { u = u ; u<x = case1 u<x ; uchain = ch-init fc } ⟫ with trio<  o∅ px
-          -- ... | tri< a ¬b ¬c = ⟪ az , record { u = u ; u<x = case1 a ; uchain = ch-init fc } ⟫  
-          -- ... | tri≈ ¬a b ¬c = ⟪ az , record { u = u ; u<x = case2 refl ; uchain = ch-init fc } ⟫  
-          -- ... | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c )
-          --- chain-x ne {z} uz@record { proj1 = az ; proj2 =  record { u = u ; u<x = case1 u<x ; uchain = ch-is-sup u is-sup fc } } with trio< u px
-          --- ... | tri< a ¬b ¬c = ⟪ az , record { u = u ; u<x = case1 a ; uchain = ch-is-sup u is-sup fc } ⟫ 
-          --- ... | tri≈ ¬a b ¬c = ⊥-elim ( ne uz  b )
-          --- ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → u o< k ) (sym (Oprev.oprev=x op))  u<x  ⟫ )
-
           zc4 : ZChain A f mf ay x 
           zc4 with ODC.∋-p O A (* px)
           ... | no noapx = no-extension -- ¬ A ∋ p, just skip