# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1660654443 -32400
# Node ID d70f3f0681eaf2896e6d54b4a910582ab7221d2a
# Parent  95db436cce670975da11eb752a9703f80aa25c88
...

diff -r 95db436cce67 -r d70f3f0681ea src/OrdUtil.agda
--- a/src/OrdUtil.agda	Tue Aug 16 16:29:57 2022 +0900
+++ b/src/OrdUtil.agda	Tue Aug 16 21:54:03 2022 +0900
@@ -4,20 +4,20 @@
 
 open import logic
 open import nat
-open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ ) 
+open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ )
 open import Data.Empty
 open import Relation.Binary.PropositionalEquality
 open import Relation.Nullary
 open import Relation.Binary hiding (_⇔_)
 
 open Ordinals.Ordinals  O
-open Ordinals.IsOrdinals isOrdinal 
-open Ordinals.IsNext isNext 
+open Ordinals.IsOrdinals isOrdinal
+open Ordinals.IsNext isNext
 
-o<-dom :   { x y : Ordinal } → x o< y → Ordinal 
+o<-dom :   { x y : Ordinal } → x o< y → Ordinal
 o<-dom  {x} _ = x
 
-o<-cod :   { x y : Ordinal } → x o< y → Ordinal 
+o<-cod :   { x y : Ordinal } → x o< y → Ordinal
 o<-cod  {_} {y} _ = y
 
 o<-subst : {Z X z x : Ordinal }  → Z o< X → Z ≡ z  →  X ≡ x  →  z o< x
@@ -40,13 +40,13 @@
 osuc-< {x} {y} y<ox x<y | case1 refl = o<¬≡ refl x<y
 osuc-< {x} {y} y<ox x<y | case2 y<x = o<> x<y y<x
 
-                                                      
+
 open _∧_
 
 ¬p<x<op : { p b : Ordinal } → ¬ ( (p o< b ) ∧ (b o< osuc p ) )
 ¬p<x<op {p} {b} P with osuc-≡< (proj2 P)
-... | case1 eq = o<¬≡ (sym eq) (proj1 P) 
-... | case2 lt = o<> lt (proj1 P) 
+... | case1 eq = o<¬≡ (sym eq) (proj1 P)
+... | case2 lt = o<> lt (proj1 P)
 
 b<x→0<x : { p b : Ordinal } → p o< b →  o∅  o< b
 b<x→0<x {p} {b} p<b with trio< o∅ b
@@ -54,13 +54,23 @@
 ... | tri≈ ¬a 0=b ¬c = ⊥-elim ( ¬x<0 ( subst (λ k → p o< k) (sym 0=b) p<b ) )
 ... | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c )
 
-ob<x : {b x : Ordinal} (lim : ¬ (Oprev Ordinal osuc x ) ) (b<x : b o< x ) → osuc b o< x                                        
-ob<x {b} {x} lim b<x with trio< (osuc b) x                                                                                     
-... | tri< a ¬b ¬c = a                                                                                                         
-... | tri≈ ¬a ob=x ¬c = ⊥-elim ( lim record { oprev = b ; oprev=x = ob=x }  )                                                     
-... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ b<x , c ⟫ )                           
+ob<x : {b x : Ordinal} (lim : ¬ (Oprev Ordinal osuc x ) ) (b<x : b o< x ) → osuc b o< x
+ob<x {b} {x} lim b<x with trio< (osuc b) x
+... | tri< a ¬b ¬c = a
+... | tri≈ ¬a ob=x ¬c = ⊥-elim ( lim record { oprev = b ; oprev=x = ob=x }  )
+... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ b<x , c ⟫ )
+
 
-osucc :  {ox oy : Ordinal } → oy o< ox  → osuc oy o< osuc ox  
+pxo<x : {x : Ordinal} (op : Oprev Ordinal osuc x)  → Oprev.oprev op o< x
+pxo<x {x} op with trio< (Oprev.oprev op) x
+... | tri< a ¬b ¬c = a
+... | tri≈ ¬a b ¬c = ⊥-elim ( o<¬≡ (trans b (sym (Oprev.oprev=x op))) <-osuc )
+... | tri> ¬a ¬b c = ⊥-elim ( o<> c (subst₂ (λ j k → j o< k ) refl (Oprev.oprev=x op) <-osuc ) )
+
+pxo≤x : {x : Ordinal} (op : Oprev Ordinal osuc x)  → Oprev.oprev op o< osuc x
+pxo≤x {x} op = ordtrans (pxo<x {x} op ) <-osuc
+
+osucc :  {ox oy : Ordinal } → oy o< ox  → osuc oy o< osuc ox
 osucc {ox} {oy} oy<ox with trio< (osuc oy) ox
 osucc {ox} {oy} oy<ox | tri< a ¬b ¬c = ordtrans a <-osuc
 osucc {ox} {oy} oy<ox | tri≈ ¬a refl ¬c = <-osuc
@@ -68,7 +78,7 @@
 osucc {ox} {oy} oy<ox | tri> ¬a ¬b c | case1 eq = ⊥-elim (o<¬≡ (sym eq) oy<ox)
 osucc {ox} {oy} oy<ox | tri> ¬a ¬b c | case2 lt = ⊥-elim (o<> lt oy<ox)
 
-osucprev :  {ox oy : Ordinal } → osuc oy o< osuc ox  → oy o< ox  
+osucprev :  {ox oy : Ordinal } → osuc oy o< osuc ox  → oy o< ox
 osucprev {ox} {oy} oy<ox with trio< oy ox
 osucprev {ox} {oy} oy<ox | tri< a ¬b ¬c = a
 osucprev {ox} {oy} oy<ox | tri≈ ¬a b ¬c = ⊥-elim (o<¬≡ (cong (λ k → osuc k) b) oy<ox )
@@ -91,7 +101,7 @@
 proj2 (osuc2 x y) lt = osucc lt
 proj1 (osuc2 x y) ox<ooy with osuc-≡< ox<ooy
 proj1 (osuc2 x y) ox<ooy | case1 ox=oy = o<-subst <-osuc refl ox=oy
-proj1 (osuc2 x y) ox<ooy | case2 ox<oy = ordtrans <-osuc ox<oy 
+proj1 (osuc2 x y) ox<ooy | case2 ox<oy = ordtrans <-osuc ox<oy
 
 o≡? : (x y : Ordinal) → Dec ( x ≡ y )
 o≡? x y with trio< x y
@@ -138,7 +148,7 @@
 --  max ( osuc x , osuc y )
 --
 
-omax :  ( x y : Ordinal  ) → Ordinal 
+omax :  ( x y : Ordinal  ) → Ordinal
 omax  x y with trio< x y
 omax  x y | tri< a ¬b ¬c = osuc y
 omax  x y | tri> ¬a ¬b c = osuc x
@@ -214,20 +224,20 @@
 
 OrdPreorder :   Preorder n n n
 OrdPreorder  = record { Carrier = Ordinal
-   ; _≈_  = _≡_ 
+   ; _≈_  = _≡_
    ; _∼_   = _o≤_
    ; isPreorder   = record {
         isEquivalence = record { refl = refl  ; sym = sym ; trans = trans }
         ; reflexive     = o≤-refl0
-        ; trans         = OrdTrans 
+        ; trans         = OrdTrans
      }
  }
 
-FExists : {m l : Level} → ( ψ : Ordinal  → Set m ) 
+FExists : {m l : Level} → ( ψ : Ordinal  → Set m )
   → {p : Set l} ( P : { y : Ordinal  } →  ψ y → ¬ p )
   → (exists : ¬ (∀ y → ¬ ( ψ y ) ))
   → ¬ p
-FExists  {m} {l} ψ {p} P = contra-position ( λ p y ψy → P {y} ψy p ) 
+FExists  {m} {l} ψ {p} P = contra-position ( λ p y ψy → P {y} ψy p )
 
 nexto∅ : {x : Ordinal} → o∅ o< next x
 nexto∅ {x} with trio< o∅ x
@@ -244,13 +254,13 @@
    (λ w nz=ow → o<¬≡ (sym nz=ow) (osuc<nx (subst (λ k → w o< k ) (sym nz=ow) <-osuc ))))
 
 osuc< : {x y : Ordinal} → osuc x ≡ y → x o< y
-osuc< {x} {y} refl = <-osuc 
+osuc< {x} {y} refl = <-osuc
 
-nexto=n : {x y : Ordinal} → x o< next (osuc y)  → x o< next y 
+nexto=n : {x y : Ordinal} → x o< next (osuc y)  → x o< next y
 nexto=n {x} {y} x<noy = next< (osuc<nx x<nx) x<noy
 
-nexto≡ : {x : Ordinal} → next x ≡ next (osuc x)  
-nexto≡ {x} with trio< (next x) (next (osuc x) ) 
+nexto≡ : {x : Ordinal} → next x ≡ next (osuc x)
+nexto≡ {x} with trio< (next x) (next (osuc x) )
 --    next x o< next (osuc x ) ->  osuc x o< next x o< next (osuc x) -> next x ≡ osuc z -> z o o< next x -> osuc z o< next x -> next x o< next x
 nexto≡ {x} | tri< a ¬b ¬c = ⊥-elim (¬nx<nx (osuc<nx  x<nx ) a
    (λ z eq → o<¬≡ (sym eq) (osuc<nx  (osuc< (sym eq)))))
@@ -268,12 +278,12 @@
 omax<next {x} {y} x<y = subst (λ k → k o< next y ) (omax< _ _ x<y ) (osuc<nx x<nx)
 
 x<ny→≡next : {x y : Ordinal} → x o< y → y o< next x → next x ≡ next y
-x<ny→≡next {x} {y} x<y y<nx with trio< (next x) (next y)    
+x<ny→≡next {x} {y} x<y y<nx with trio< (next x) (next y)
 x<ny→≡next {x} {y} x<y y<nx | tri< a ¬b ¬c =          -- x < y < next x <  next y ∧ next x = osuc z
-     ⊥-elim ( ¬nx<nx y<nx a (λ z eq →  o<¬≡ (sym eq) (osuc<nx (subst (λ k → z o< k ) (sym eq) <-osuc )))) 
+     ⊥-elim ( ¬nx<nx y<nx a (λ z eq →  o<¬≡ (sym eq) (osuc<nx (subst (λ k → z o< k ) (sym eq) <-osuc ))))
 x<ny→≡next {x} {y} x<y y<nx | tri≈ ¬a b ¬c = b
 x<ny→≡next {x} {y} x<y y<nx | tri> ¬a ¬b c =          -- x < y < next y < next x
-     ⊥-elim ( ¬nx<nx (ordtrans x<y x<nx) c (λ z eq →  o<¬≡ (sym eq) (osuc<nx (subst (λ k → z o< k ) (sym eq) <-osuc )))) 
+     ⊥-elim ( ¬nx<nx (ordtrans x<y x<nx) c (λ z eq →  o<¬≡ (sym eq) (osuc<nx (subst (λ k → z o< k ) (sym eq) <-osuc ))))
 
 ≤next : {x y : Ordinal} → x o≤ y → next x o≤ next y
 ≤next {x} {y} x≤y with trio< (next x) y
@@ -281,12 +291,12 @@
 ≤next {x} {y} x≤y | tri≈ ¬a refl ¬c = (ordtrans x<nx <-osuc )
 ≤next {x} {y} x≤y | tri> ¬a ¬b c with osuc-≡< x≤y
 ≤next {x} {y} x≤y | tri> ¬a ¬b c | case1 refl = o≤-refl -- x = y < next x
-≤next {x} {y} x≤y | tri> ¬a ¬b c | case2 x<y = o≤-refl0 (x<ny→≡next x<y c) -- x ≤ y < next x 
+≤next {x} {y} x≤y | tri> ¬a ¬b c | case2 x<y = o≤-refl0 (x<ny→≡next x<y c) -- x ≤ y < next x
 
 x<ny→≤next : {x y : Ordinal} → x o< next y → next x o≤ next y
 x<ny→≤next {x} {y} x<ny with trio< x y
 x<ny→≤next {x} {y} x<ny | tri< a ¬b ¬c =  ≤next (ordtrans a <-osuc )
-x<ny→≤next {x} {y} x<ny | tri≈ ¬a refl ¬c =  o≤-refl 
+x<ny→≤next {x} {y} x<ny | tri≈ ¬a refl ¬c =  o≤-refl
 x<ny→≤next {x} {y} x<ny | tri> ¬a ¬b c = o≤-refl0 (sym ( x<ny→≡next c x<ny ))
 
 omax<nomax : {x y : Ordinal} → omax x y o< next (omax x y )
@@ -332,8 +342,8 @@
     trans2 {i} {j} {k} i<oj j<k | case1 refl = j<k
     trans2 {i} {j} {k} i<oj j<k | case2 i<j = ordtrans i<j j<k
 
-    open import Relation.Binary.Reasoning.Base.Triple 
-      (Preorder.isPreorder OrdPreorder) 
+    open import Relation.Binary.Reasoning.Base.Triple
+      (Preorder.isPreorder OrdPreorder)
          ordtrans --<-trans
          (resp₂ _o<_) --(resp₂ _<_)
          (λ x → ordtrans x <-osuc ) --<⇒≤
diff -r 95db436cce67 -r d70f3f0681ea src/zorn.agda
--- a/src/zorn.agda	Tue Aug 16 16:29:57 2022 +0900
+++ b/src/zorn.agda	Tue Aug 16 21:54:03 2022 +0900
@@ -803,19 +803,32 @@
                       zc60 (fsuc w1 fc) with zc60 fc
                       ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ proj2 ( mf _ ua1)  , ch-init (fsuc _ fc₁)  ⟫ 
                       ... | ⟪ ua1 , ch-is-sup u u≤x is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1)  , ch-is-sup u u≤x is-sup (fsuc _ fc₁) ⟫ 
+                 chp10 : {u : Ordinal } → u o< x → ChainP A f mf ay supf1 u → ChainP A f mf ay supf0 u
+                 chp10 = ?
+                 fc10 : {w : Ordinal } → u o< x → FClosure A f supf1 w → FClosure A f supf0 w 
+                 fc10 = ?
                  sup : {z : Ordinal} → z o< x → SUP A (UnionCF A f mf ay supf1 z)
                  sup {z} z<x with trio< z px
-                 ... | tri< a ¬b ¬c = SUP⊆ (UnionCFR⊆ o≤-refl ? (o<→≤ a)) ( ZChain.sup zc  a )
-                 ... | tri≈ ¬a b ¬c = record { sup = SUP.sup sup1 ; as = SUP.as sup1 ; x<sup = zc61 } where
-                     zc61 : {w : HOD} → UnionCF A f mf ay supf1 z ∋ w → (w ≡ SUP.sup sup1) ∨ (w < SUP.sup sup1)
-                     zc61 {w} lt = ?
+                 ... | tri< a ¬b ¬c = SUP⊆ (UnionCFR⊆ o≤-refl (ordtrans z<x <-osuc) (o<→≤ a)) ( ZChain.sup zc  a ) 
+                 ... | tri≈ ¬a b ¬c = record { sup = SUP.sup sup1 ; as = SUP.as sup1 ; x<sup = λ {w} lt → zc61 (subst (λ k → UnionCF A f mf ay supf1 k ∋ w) b lt) } where
+                     zc61 : {w : HOD} → UnionCF A f mf ay supf1 px ∋ w → (w ≡ SUP.sup sup1) ∨ (w < SUP.sup sup1)
+                     zc61 {w} ⟪ au , ch-init fc ⟫  with SUP.x<sup sup1 ⟪ au , ch-init fc ⟫ 
+                     ... | case1 eq = case1 eq
+                     ... | case2 lt = case2 lt
+                     zc61 {w} ⟪ au , ch-is-sup u u≤px is-sup fc ⟫ with SUP.x<sup sup1 ⟪ au , ch-is-sup u (subst (λ k → u o≤ k) (Oprev.oprev=x op) (ordtrans u≤px <-osuc))  ? ? ⟫ 
+                     ... | case1 eq = case1 eq
+                     ... | case2 lt = case2 lt
                  ... | tri> ¬a ¬b px<z = ⊥-elim (¬p<x<op ⟪ px<z , subst (λ k → z o< k ) (sym (Oprev.oprev=x op)) z<x ⟫ )
                  sup=u : {b : Ordinal} (ab : odef A b) →
                     b o≤ x → IsSup A (UnionCF A f mf ay supf1 (osuc b)) ab → supf1 b ≡ b
                  sup=u {b} ab b≤x is-sup with trio< b px
                  ... | tri< a ¬b ¬c = ZChain.sup=u zc ab (o<→≤ a) record { x<sup = {!!} }
-                 ... | tri≈ ¬a b ¬c = ?
-                 ... | tri> ¬a ¬b px<b = ⊥-elim (¬p<x<op ⟪ px<b , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) ? ⟫ )
+                 ... | tri≈ ¬a b ¬c = ZChain.sup=u zc ab {!!} record { x<sup = {!!} }
+                 ... | tri> ¬a ¬b px<b = {!!} where
+                     zc30 : x ≡ b
+                     zc30 with osuc-≡< b≤x
+                     ... | case1 eq = sym (eq)
+                     ... | case2 b<x = ⊥-elim (¬p<x<op ⟪ px<b , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x ⟫ )
                  csupf : {b : Ordinal} → b o≤ x → odef (UnionCF A f mf ay supf1 b) (supf1 b)
                  csupf {b} b≤x with trio< b px | inspect supf1 b
                  ... | tri< a ¬b ¬c | _ = UnionCF⊆ o≤-refl (o<→≤ a) b≤x ( ZChain.csupf zc (o<→≤ a) )
@@ -960,18 +973,18 @@
                  sup : {z : Ordinal} → z o< x → SUP A (UnionCF A f mf ay supf1 z)
                  sup {z} z≤x with trio< z x
                  ... | tri< a ¬b ¬c = SUP⊆ (UnionCF⊆ a) (ZChain.sup (pzc (osuc z) {!!}) {!!} )
-                 ... | tri≈ ¬a b ¬c = ?
-                 ... | tri> ¬a ¬b c = ?
-                 sis : {z : Ordinal} (x≤z : z o< x) → supf1 z ≡ & (SUP.sup (sup ?))
+                 ... | tri≈ ¬a b ¬c = {!!}
+                 ... | tri> ¬a ¬b c = {!!}
+                 sis : {z : Ordinal} (x≤z : z o< x) → supf1 z ≡ & (SUP.sup (sup {!!}))
                  sis {z} z<x with trio< z x
                  ... | tri< a ¬b ¬c = {!!} where
-                     zc8 = ZChain.supf-is-sup (pzc z a) ?
-                 ... | tri≈ ¬a b ¬c = ?
-                 ... | tri> ¬a ¬b c = ?
+                     zc8 = ZChain.supf-is-sup (pzc z a) {!!}
+                 ... | tri≈ ¬a b ¬c = {!!}
+                 ... | tri> ¬a ¬b c = {!!}
                  sup=u : {b : Ordinal} (ab : odef A b) → b o≤ x → IsSup A (UnionCF A f mf ay supf1 (osuc b)) ab → supf1 b ≡ b
                  sup=u {b} ab b<x is-sup with trio< b x
                  ... | tri< a ¬b ¬c = ZChain.sup=u (pzc (osuc b)  (ob<x lim a))  ab {!!} record { x<sup = {!!} }
-                 ... | tri≈ ¬a b ¬c = {!!}
+                 ... | tri≈ ¬a b ¬c = {!!} -- ZChain.sup=u (pzc (osuc ?)  ?)  ab {!!} record { x<sup = {!!} }
                  ... | tri> ¬a ¬b c = {!!}
                  csupf : {z : Ordinal} → z o≤ x → odef (UnionCF A f mf ay supf1 z) (supf1 z)
                  csupf {z} z≤x with trio< z x