# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1657848835 -32400
# Node ID 55e82405ec0d8d783235dab32b33774ebdb5daa8
# Parent  92275389e6234d288917c65ae49784807140727e
px?

diff -r 92275389e623 -r 55e82405ec0d src/zorn.agda
--- a/src/zorn.agda	Fri Jul 15 07:44:50 2022 +0900
+++ b/src/zorn.agda	Fri Jul 15 10:33:55 2022 +0900
@@ -569,32 +569,34 @@
           chain-≡ lt = ==→o≡ record { eq→ = lt ; eq← = chain-mono }
 
           zc4 : ZChain A f mf ay x 
-          zc4 with ODC.∋-p O A (* x)
-          ... | no noax = no-extenion zc1 where -- ¬ A ∋ p, just skip
+          zc4 with ODC.∋-p O A (* px)
+          ... | no nopax = no-extenion zc1 where -- ¬ A ∋ p, just skip
                 zc1 : {a b : Ordinal} → odef pchain a → b o< x → (ab : odef A b) →
                     HasPrev A pchain ab f ∨  IsSup A pchain ab →
                             * a < * b → odef pchain b
-                zc1 {a} {b} za b<ox ab P a<b with osuc-≡< ?
-                ... | case1 eq = ⊥-elim ( noax (subst (λ k → odef A k) (trans eq (sym &iso)) ab ) )
-                ... | case2 lt = zcp za (chain-≡ zc10) ? ab P a<b where
-                     zc10 : pchain ⊆' UnionCF A f mf ay (ZChain.supf zc) (Oprev.oprev op)
-                     zc10 {z} ⟪ az , record { u = u ; u<x = case2 u=y ; uchain = uc } ⟫ = 
-                                   ⟪ az , record { u = u ; u<x = case2 u=y ; uchain = uc } ⟫ 
-                     zc10 {z} ⟪ az , record { u = u ; u<x = case1 u<x ; uchain = ch-init z fc } ⟫ = 
-                                   ⟪ az , record { u = u ; u<x = case1 ? ; uchain = ch-init z fc } ⟫ 
-                     zc10 {z} ⟪ az , record { u = u ; u<x = case1 u<x ; uchain = ch-is-sup is-sup fc } ⟫ = 
-                                   ⟪ az , record { u = u ; u<x = case1 ? ; uchain = ch-is-sup is-sup fc } ⟫ 
-          ... | yes ax with ODC.p∨¬p O ( HasPrev A (ZChain.chain zc ) ax f )   
+                zc1 {a} {b} za b<x ab P a<b with trio< b px
+                ... | tri< lt ¬b ¬c = zcp za (chain-≡ zc10) lt ab P a<b where
+                      zc10 : pchain ⊆' UnionCF A f mf ay (ZChain.supf zc) (Oprev.oprev op)
+                      zc10 {z} ⟪ az , record { u = u ; u<x = case2 u=y ; uchain = uc } ⟫ = 
+                                    ⟪ az , record { u = u ; u<x = case2 u=y ; uchain = uc } ⟫ 
+                      zc10 {z} ⟪ az , record { u = u ; u<x = case1 u<x ; uchain = ch-init z fc } ⟫ = 
+                                    ⟪ az , record { u = u ; u<x = case1 ? ; uchain = ch-init z fc } ⟫ 
+                      zc10 {z} ⟪ az , record { u = u ; u<x = case1 u<x ; uchain = ch-is-sup is-sup fc } ⟫ = 
+                                    ⟪ az , record { u = u ; u<x = case1 ? ; uchain = ch-is-sup is-sup fc } ⟫ 
+                -- ... | case1 eq = ⊥-elim ( noax (subst (λ k → odef A k) (trans eq (sym &iso)) ab ) )
+                ... | tri≈ ¬a b=px ¬c = ?
+                ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → b o< k ) (sym (Oprev.oprev=x op))  b<x  ⟫ )
+          ... | yes apx with ODC.p∨¬p O ( HasPrev A (ZChain.chain zc ) apx f )   
                -- we have to check adding x preserve is-max ZChain A y f mf x
           ... | case1 pr = no-extenion ? where -- we have previous A ∋ z < x , f z ≡ x, so chain ∋ f z ≡ x because of f-next
                 zc7 : {a b : Ordinal} → odef pchain a → b o< x → (ab : odef A b) →
                     HasPrev A pchain ab f ∨  IsSup A pchain ab →
                             * a < * b → odef pchain b
-                zc7 {a} {b} za b<ox ab P a<b with osuc-≡< ?
+                zc7 {a} {b} za b<x ab P a<b with osuc-≡< ?
                 ... | case2 lt = zcp za ? ? ab P a<b
                 ... | case1 b=x = ? 
                 -- subst (λ k → odef chain0 k ) (trans (sym (HasPrev.x=fy pr )) (trans &iso (sym b=x)) ) ( ZChain.f-next zc (HasPrev.ay pr))
-          ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain.chain zc ) ax )
+          ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain.chain zc ) apx )
           ... | case1 is-sup = -- x is a sup of zc 
                 record {  chain⊆A = pchain⊆A ; f-next = pnext ; f-total = ptotal
                      ; initial = pinit ; chain∋init  = pcy ; is-max = p-ismax } where
@@ -602,8 +604,8 @@
                     b o< x → (ab : odef A b) →
                     ( HasPrev A pchain ab f ∨ IsSup A pchain ab ) →
                         * a < * b → odef pchain b
-                p-ismax {a} {b} ua b<ox ab (case1 hasp) a<b = ?
-                p-ismax {a} {b} ua b<ox ab (case2 sup)  a<b = ?
+                p-ismax {a} {b} ua b<x ab (case1 hasp) a<b = ?
+                p-ismax {a} {b} ua b<x ab (case2 sup)  a<b = ?
 
           ... | case2 ¬x=sup =  no-extenion z18 where -- x is not f y' nor sup of former ZChain from y -- no extention
                 z18 :  {a b : Ordinal} → odef pchain a → b o< x → (ab : odef A b) →
@@ -668,24 +670,28 @@
           uzc : {a : Ordinal } → (za : odef pchain a) → ZChain A f mf ay (UChain.u (proj2 za))
           uzc {a} za with UChain.u<x (proj2 za)
           ... | case1 u<x = pzc _ u<x
-          ... | case2 u=0 = ?
+          ... | case2 u=0 =  subst (λ k → ZChain A f mf ay k ) (sym u=0) (inititalChain f mf {y} ay )
 
           zcp : {a b : Ordinal} → (za : odef pchain a )
-              → pchain ≡ ?
+              → pchain ≡ UnionCF A f mf ay psupf x
               → b o< x → (ab : odef A b) 
               → HasPrev A pchain ab f ∨  IsSup A pchain ab 
               → * a < * b → odef pchain b
-          zcp {a} {b} za cheq b<x ab P a<b = ? where
-              zc12 : odef ? b
-              zc12 = ZChain.is-max (pzc _ ?) ? ? ab 
-                       (subst (λ k → HasPrev A k ab f ∨  IsSup A k ab ) ? P)  a<b 
+          zcp {a} {b} za cheq b<x ab P a<b = subst (λ k → odef k b) (sym cheq) zc12  where
+              zc13 : odef (UnionCF A f mf ay (ZChain.supf (uzc za)) (UChain.u (proj2 za))) a
+              zc13 = ⟪ proj1 za , record { u = UChain.u (proj2 za) ; u<x = ? ; uchain = ? } ⟫
+              zc14 : b o< UChain.u (proj2 za)
+              zc14 = ?
+              zc12 : odef (UnionCF A f mf ay psupf x) b
+              zc12 = ⟪ ab , record { u = UChain.u (proj2 za) ;  u<x = ? ; uchain = ? } ⟫
+              -- ZChain.is-max (uzc za) ? ? ab (subst (λ k → HasPrev A k ab f ∨  IsSup A k ab ) cheq P)  a<b 
 
           chain-mono : pchain ⊆'  UnionCF A f mf ay psupf x  
           chain-mono {a} za = ⟪ proj1 za , record { u = UChain.u (proj2 za)  ; u<x = UChain.u<x (proj2 za) ; uchain = zc11 }  ⟫ where
               zc11 : Chain A f mf ay psupf (UChain.u (proj2 za)) a
               zc11 with UChain.uchain (proj2 za)
               ... | ch-init .a x = ch-init a x
-              ... | ch-is-sup is-sup fc = ch-is-sup ? ?
+              ... | ch-is-sup is-sup fc = ch-is-sup ? (subst (λ k → FClosure A f k a ) ? fc )
 
           chain-≡ : UnionCF A f mf ay psupf x ⊆' pchain 
              → UnionCF A f mf ay psupf x ≡ pchain