# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1657445402 -32400
# Node ID 34650e39e553c92b24ac4cb20270be325e0b71f4
# Parent  10195ebfbe2b31f021647acdf49f56ed62104e25
Chain is not strictly positive

diff -r 10195ebfbe2b -r 34650e39e553 src/zorn.agda
--- a/src/zorn.agda	Sun Jul 10 16:22:46 2022 +0900
+++ b/src/zorn.agda	Sun Jul 10 18:30:02 2022 +0900
@@ -254,9 +254,10 @@
 UnionCF A x chainf = record { od = record { def = λ z → odef A z ∧ UChain x chainf z } ; odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy }
 
 data Chain (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y) : Ordinal →  Ordinal → Set n where
-    ch-init    : (x z : Ordinal) → x ≡ o∅ → FClosure A f y z  → Chain A f mf  ay x z 
-    ch-is-sup : {x z : Ordinal } (0<x : o∅ o< x) ( ax : odef A x ) 
-         → ( is-sup : (x1 w : Ordinal) → x1 o< x → Chain A f mf ay x1 w → w << x )  → ( fc : FClosure A f x z ) → Chain A f mf ay x z
+    ch-init    : (z : Ordinal) → FClosure A f y z  → Chain A f mf  ay y z 
+    ch-is-sup : {x z : Ordinal } (init<x : y << x) (lty : y o< x ) ( ax : odef A x ) 
+         → ( is-sup : (x1 w : Ordinal) →  ( x1 ≡ y ) ∨ ( (y << x1) ∧ (x1 o< x) )  → Chain A f mf ay x1 w → w << x )  
+         → ( fc : FClosure A f x z ) → Chain A f mf ay x z
 
 record ZChain1 ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) {y : Ordinal } (ay : odef A y ) ( z : Ordinal ) : Set (Level.suc n) where
    field
@@ -294,33 +295,39 @@
 
 chain-total : (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y) 
    {s s1 a b : Ordinal } ( ca : Chain A f mf ay s a ) ( cb : Chain A f mf ay s1 b ) → Tri (* a < * b) (* a ≡ * b) (* b < * a )
-chain-total A f mf {y} ay {s} {s1} {a} {b} ca cb = ct-ind s ca cb where
-     ct-ind : (x : Ordinal) → {s1 a b : Ordinal} → Chain A f mf ay x a → Chain A f mf ay s1 b → Tri (* a < * b) (* a ≡ * b) (* b < * a)
-     ct-ind x {s1} {a} {b} (ch-init s a x=0 fca) (ch-init s1 b x=0' fcb) = fcn-cmp y f mf fca fcb
-     ct-ind x {s1} {a} {b} (ch-init s a x=0 fca) (ch-is-sup 0<x as supb fcb) = tri< ct01  (λ eq → <-irr (case1 (sym eq)) ct01) (λ lt → <-irr (case2 ct01) lt)  where
-         ct00 : * a < * s1
-         ct00 = supb _ _ 0<x (subst (λ k → Chain A f mf ay k a) x=0 (ch-init s a x=0 fca) )
-         ct01 : * a < * b 
-         ct01 with s≤fc s1 f mf fcb 
-         ... | case1 eq =  subst (λ k → * a < k ) eq ct00
-         ... | case2 lt =  IsStrictPartialOrder.trans POO ct00 lt
-     ct-ind x {s1} {a} {b} (ch-is-sup 0<x as supa fca) (ch-init s1 b x=0' fcb) = ?
-     ct-ind x {s1} {a} {b} (ch-is-sup 0<x as supa fca) (ch-is-sup 0<x' as' supb fcb) with trio< x s1
+chain-total A f mf {y} ay {xa} {xb} {a} {b} ca cb = ct-ind xa xb ca cb where
+     ct-ind : (xa xb : Ordinal) → {a b : Ordinal} → Chain A f mf ay xa a → Chain A f mf ay xb b → Tri (* a < * b) (* a ≡ * b) (* b < * a)
+     ct-ind xa xb {a} {b} (ch-init a fca) (ch-init b fcb) = fcn-cmp y f mf fca fcb
+     ct-ind xa xb {a} {b} (ch-init a fca) (ch-is-sup y<xb ltyb axb supb fcb) = tri< ct01  (λ eq → <-irr (case1 (sym eq)) ct01) (λ lt → <-irr (case2 ct01) lt)  where
+          ct00 : * a < * xb
+          ct00 = supb _ _ (case1 refl) (ch-init a fca)  
+          ct01 : * a < * b 
+          ct01 with s≤fc xb f mf fcb 
+          ... | case1 eq =  subst (λ k → * a < k ) eq ct00
+          ... | case2 lt =  IsStrictPartialOrder.trans POO ct00 lt
+     ct-ind xa xb {a} {b} (ch-is-sup y<x ltya ax supa fca) (ch-init b fcb)= tri> (λ lt → <-irr (case2 ct01) lt) (λ eq → <-irr (case1 eq) ct01) ct01    where
+          ct00 : * b < * xa
+          ct00 = supa _ _ (case1 refl) (ch-init b fcb)  
+          ct01 : * b < * a 
+          ct01 with s≤fc xa 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 y<xa ltya axa supa fca) (ch-is-sup y<xb ltyb axb supb fcb) with trio< xa xb
      ... | tri< a₁ ¬b ¬c = tri< ct02  (λ eq → <-irr (case1 (sym eq)) ct02) (λ lt → <-irr (case2 ct02) lt)  where
-         ct03 : * a < * s1
-         ct03 = supb _ _ a₁ (ch-is-sup 0<x as supa fca)
-         ct02 : * a < * b 
-         ct02 with s≤fc s1 f mf fcb 
-         ... | case1 eq =  subst (λ k → * a < k ) eq ct03
-         ... | case2 lt =  IsStrictPartialOrder.trans POO ct03 lt
-     ... | tri≈ ¬a  refl ¬c = fcn-cmp s1 f mf fca fcb
+          ct03 : * a < * xb
+          ct03 = supb _ _ (case2 ⟪ y<xa , a₁ ⟫) (ch-is-sup y<xa ltya axa supa fca)
+          ct02 : * a < * b 
+          ct02 with s≤fc xb f mf fcb 
+          ... | case1 eq =  subst (λ k → * a < k ) eq ct03
+          ... | case2 lt =  IsStrictPartialOrder.trans POO ct03 lt
+     ... | tri≈ ¬a  refl ¬c = fcn-cmp xa f mf fca fcb
      ... | tri> ¬a ¬b c = tri> (λ lt → <-irr (case2 ct04) lt) (λ eq → <-irr (case1 (eq)) ct04) ct04    where
-         ct05 : * b < * x
-         ct05 = supa _ _ c (ch-is-sup 0<x' as' supb fcb)
-         ct04 : * b < * a 
-         ct04 with s≤fc x f mf fca 
-         ... | case1 eq =  subst (λ k → * b < k ) eq ct05
-         ... | case2 lt =  IsStrictPartialOrder.trans POO ct05 lt
+          ct05 : * b < * xa
+          ct05 = supa _ _ (case2 ⟪ y<xb , c ⟫) (ch-is-sup y<xb ltyb axb supb fcb)
+          ct04 : * b < * a 
+          ct04 with s≤fc xa f mf fca 
+          ... | case1 eq =  subst (λ k → * b < k ) eq ct05
+          ... | case2 lt =  IsStrictPartialOrder.trans POO ct05 lt
 
 Zorn-lemma : { A : HOD } 
     → o∅ o< & A 
@@ -475,17 +482,17 @@
             chainf1 z with o≤? z x
             ... | yes _  = ZChain1.chainf sc z
             ... | no _ = ZChain1.chainf sc x
-            is-chain1 : ?
-            is-chain1 = ?
+            is-chain1 : {!!}
+            is-chain1 = {!!}
           sc4 : ZChain1 A f mf ay x
           sc4 with ODC.∋-p O A (* x)
           ... | no noax = no-ext
           ... | yes ax with ODC.p∨¬p O ( HasPrev A pchain ax f )   
           ... | 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 = ? } where
+          ... | case1 is-sup = record { psup = {!!} ; p≤z = {!!} ; chainf = {!!} ; is-chain = {!!} } where
                 schain : HOD
-                schain = ? -- record { od = record { def = λ z → odef A z ∧ ( odef (ZChain1.chain sc ) z ∨ (FClosure A f x z)) } 
+                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 = no-ext
      ... | no ¬ox = sc4 where
@@ -515,49 +522,46 @@
             ... | no z<x  = ZChain1.p≤z (pzc z (o¬≤→< z<x)) z
             chainf1 : (z : Ordinal ) → HOD
             chainf1 z with o≤? x z
-            ... | yes _  = record { od = record { def = λ w → odef A w ∧ FClosure A f spu w  } ; odmax = & A ; <odmax = ? }
+            ... | yes _  = record { od = record { def = λ w → odef A w ∧ FClosure A f spu w  } ; odmax = & A ; <odmax = {!!} }
             ... | no z<x = ZChain1.chainf (pzc z (o¬≤→< z<x)) z
             is-chain1 : (z w : Ordinal) → odef (chainf1 z) w → Chain A f mf ay (psup1 z ) w
             is-chain1 z w lt with o≤? x z
             ... | no z<x = ZChain1.is-chain (pzc z (o¬≤→< z<x)) z w lt
-            is-chain1 z w ⟪ ax , ux ⟫ | yes _ with trio< o∅ spu
-            ... | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c )
-            ... | tri≈ ¬a b ¬c = ch-init _ _ (sym b) ? where
-                sc0 : FClosure A f spu w
-                sc0 = ux
-            ... | tri< a ¬b ¬c = ch-is-sup 0<s aspu is-sup ux where
-                0<s : o∅ o< spu
-                0<s = a 
+            is-chain1 z w ⟪ ax , ux ⟫ | yes _ = ch-is-sup y<spu lty aspu {!!} ux where
+                y<spu : y << spu
+                y<spu = {!!}
+                lty : y o< spu
+                lty = {!!}
                 aspu : odef A spu
                 aspu = SUP.A∋maximal usup
                 is-sup : (x1 w₁ : Ordinal) → x1 o< & (SUP.sup usup) → Chain A f mf ay x1 w₁ → w₁ << & (SUP.sup usup)
-                is-sup = ?
+                is-sup = {!!}
 
      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) 
          → ((z : Ordinal) → z o< x → ZChain A f mf ay zc0 z) → ZChain A f mf ay zc0 x
      ind f mf {y} ay x zc0 prev with Oprev-p x
-     ... | yes op = ? where
+     ... | yes op = {!!} where
           --
           -- we have previous ordinal to use induction
           --
           px = Oprev.oprev op
           supf : Ordinal → HOD
-          supf x =  ? -- ChainF A f mf ay x zc0 
+          supf x =  {!!} -- ChainF A f mf ay x zc0 
           zc : ZChain A f mf ay zc0 (Oprev.oprev op)
           zc = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ) 
           px<x : px o< x
           px<x = subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc
           -- if previous chain satisfies maximality, we caan reuse it
           --
-          no-extenion : ( {a b z : Ordinal} → (z<x : z o< x)  → odef (ZChain.chain ?) a → b o< osuc x → (ab : odef A b) →
-                    HasPrev A (ZChain.chain zc ) ab f ∨  IsSup A (ZChain.chain ? ) ab →
+          no-extenion : ( {a b z : Ordinal} → (z<x : z o< x)  → odef (ZChain.chain {!!}) a → b o< osuc x → (ab : odef A b) →
+                    HasPrev A (ZChain.chain zc ) ab f ∨  IsSup A (ZChain.chain {!!} ) ab →
                             * a < * b → odef (ZChain.chain zc ) b ) → ZChain A f mf ay zc0 x
-          no-extenion is-max = ? 
+          no-extenion is-max = {!!} 
 
           zc4 : ZChain A f mf ay zc0 x 
           zc4 with o≤? x o∅
-          ... | yes x=0 = ?
+          ... | yes x=0 = {!!}
           ... | no 0<x with ODC.∋-p O A (* x)
           ... | no noax = no-extenion zc1  where -- ¬ A ∋ p, just skip
                 zc1 : {a b z : Ordinal} → (z<x : z o< x) → odef (ZChain.chain zc ) a → b o< osuc x → (ab : odef A b) →
@@ -565,7 +569,7 @@
                             * a < * b → odef (ZChain.chain zc ) b
                 zc1 {a} {b} z<x za b<ox ab P a<b with osuc-≡< b<ox
                 ... | case1 eq = ⊥-elim ( noax (subst (λ k → odef A k) (trans eq (sym &iso)) ab ) )
-                ... | case2 lt = ZChain.is-max zc za ?  ab P a<b
+                ... | case2 lt = ZChain.is-max zc za {!!}  ab P a<b
           ... | yes ax with ODC.p∨¬p O ( HasPrev A (ZChain.chain zc ) ax f )   
                -- we have to check adding x preserve is-max ZChain A y f mf zc0 x
           ... | case1 pr = no-extenion zc7  where -- we have previous A ∋ z < x , f z ≡ x, so chain ∋ f z ≡ x because of f-next
@@ -574,8 +578,8 @@
                             HasPrev A (ZChain.chain zc ) ab f ∨ IsSup A (ZChain.chain zc ) ab →
                             * a < * b → odef (ZChain.chain zc ) b
                 zc7 {a} {b} z<x za b<ox ab P a<b with osuc-≡< b<ox
-                ... | case2 lt = ZChain.is-max zc 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 lt = ZChain.is-max zc 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 )
           ... | case1 is-sup = -- x is a sup of zc 
                 record {  chain⊆A = {!!} ; f-next = {!!}  ; f-total = {!!}
@@ -598,7 +602,7 @@
                 schain = record { od = record { def = λ x → odef chain0 x ∨ (FClosure A f (& sp) x) } ; odmax = & A ; <odmax = λ {y} sy → sc<A {y} sy  }
                 supf0 : Ordinal → HOD
                 supf0 z with trio< z x
-                ... | tri< a ¬b ¬c = ? -- supf z
+                ... | tri< a ¬b ¬c = {!!} -- supf z
                 ... | tri≈ ¬a b ¬c = schain 
                 ... | tri> ¬a ¬b c = schain
                 A∋schain : {x : HOD } → schain ∋ x → A ∋ x
@@ -651,9 +655,9 @@
                 s-ismax {a} {b} (case1 za) b<ox ab (case1 p) a<b | case2 b<x = z21 p where   -- has previous
                      z21 : HasPrev A schain ab f → odef schain b
                      z21 record { y = y ; ay = (case1 zy) ; x=fy = x=fy } = 
-                           case1 (ZChain.is-max zc za ? ab (case1 record { y = y ; ay = zy ; x=fy = x=fy }) a<b )
+                           case1 (ZChain.is-max zc za {!!} ab (case1 record { y = y ; ay = zy ; x=fy = x=fy }) a<b )
                      z21 record { y = y ; ay = (case2 sy) ; x=fy = x=fy } = subst (λ k → odef schain k) (sym x=fy) (case2 (fsuc y sy) )
-                s-ismax {a} {b} (case1 za) b<ox ab (case2 p) a<b | case2 b<x = case1 (ZChain.is-max zc za ? ab (case2 z22) a<b ) where -- previous sup
+                s-ismax {a} {b} (case1 za) b<ox ab (case2 p) a<b | case2 b<x = case1 (ZChain.is-max zc za {!!} ab (case2 z22) a<b ) where -- previous sup
                      z22 : IsSup A (ZChain.chain zc )   ab 
                      z22 = record { x<sup = λ {y} zy → IsSup.x<sup p (case1 zy ) }
                 s-ismax {a} {b} (case2 sa) b<ox ab (case1 p)  a<b | case2 b<x with HasPrev.ay p
@@ -665,13 +669,13 @@
                      z23 : odef chain0 b
                      z23 with IsSup.x<sup (z24 p) ( ZChain.chain∋init zc )
                      ... | case1 y=b  = subst (λ k → odef chain0 k )  y=b ( ZChain.chain∋init zc )
-                     ... | case2 y<b  = ZChain.is-max zc (ZChain.chain∋init zc ) ? ab (case2 (z24 p)) y<b
+                     ... | case2 y<b  = ZChain.is-max zc (ZChain.chain∋init zc ) {!!} ab (case2 (z24 p)) y<b
                 seq : schain ≡ supf0 x 
                 seq with trio< x x
                 ... | tri< a ¬b ¬c = ⊥-elim ( ¬b refl )
                 ... | tri≈ ¬a b ¬c = refl
                 ... | tri> ¬a ¬b c = refl
-                seq<x : {b : Ordinal } → b o< x → ? --  supf b  ≡ supf0 b
+                seq<x : {b : Ordinal } → b o< x → {!!} --  supf b  ≡ supf0 b
                 seq<x {b} b<x with trio< b x
                 ... | tri< a ¬b ¬c = refl
                 ... | tri≈ ¬a b₁ ¬c = ⊥-elim (¬a  b<x )
@@ -682,11 +686,11 @@
                             HasPrev A (ZChain.chain zc ) ab f ∨ IsSup A (ZChain.chain zc )   ab →
                             * a < * b → odef (ZChain.chain zc ) b
                 z18 {a} {b} z<x za b<x ab p a<b with osuc-≡< b<x
-                ... | case2 lt = ZChain.is-max zc za ? ab p a<b 
+                ... | case2 lt = ZChain.is-max zc za {!!} ab p a<b 
                 ... | case1 b=x with p
-                ... | case1 pr = ⊥-elim ( ¬fy<x record {y = HasPrev.y pr ; ay = ? ; x=fy = trans (trans &iso (sym b=x) ) (HasPrev.x=fy pr ) } )
+                ... | case1 pr = ⊥-elim ( ¬fy<x record {y = HasPrev.y pr ; ay = {!!} ; x=fy = trans (trans &iso (sym b=x) ) (HasPrev.x=fy pr ) } )
                 ... | case2 b=sup = ⊥-elim ( ¬x=sup record { 
-                      x<sup = λ {y} zy → subst (λ k → (y ≡ k) ∨ (y << k)) (trans b=x (sym &iso)) (IsSup.x<sup b=sup ? )  } ) 
+                      x<sup = λ {y} zy → subst (λ k → (y ≡ k) ∨ (y << k)) (trans b=x (sym &iso)) (IsSup.x<sup b=sup {!!} )  } ) 
      ... | no op = zc5 where
           supf : (z : Ordinal ) → z o< x  → HOD
           supf x lt = ZChain1.chainf ( zc0  (& A) ) x 
@@ -695,18 +699,18 @@
           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 = ? }
+          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 = ?
+          ... | yes x=0 = {!!}
           ... | no 0<x with ODC.∋-p O A (* x)
-          ... | no noax = ? where -- ¬ A ∋ p, just skip
+          ... | no noax = {!!} where -- ¬ A ∋ p, just skip
           ... | yes ax with ODC.p∨¬p O ( HasPrev A Uz ax f )   
                -- we have to check adding x preserve is-max ZChain A y f mf zc0 x
-          ... | case1 pr = ? where -- we have previous A ∋ z < x , f z ≡ x, so chain ∋ f z ≡ x because of f-next
+          ... | case1 pr = {!!} where -- we have previous A ∋ z < x , f z ≡ x, so chain ∋ f z ≡ x because of f-next
           ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A Uz ax )
-          ... | case1 is-sup = ? -- x is a sup of (zc ?) 
-          ... | case2 ¬x=sup =  ? -- no-extenion z18 where -- x is not f y' nor sup of former ZChain from y -- no extention
+          ... | case1 is-sup = {!!} -- x is a sup of (zc ?) 
+          ... | case2 ¬x=sup =  {!!} -- no-extenion z18 where -- x is not f y' nor sup of former ZChain from y -- no extention
 
          
      SZ0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} (ay : odef A y) → (x : Ordinal) → ZChain1 A f mf ay x