# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1664973412 -32400
# Node ID 290c61498d628d489e96f7c27454a858b1b71ab0
# Parent  f331c8be2425fa6662eb41b0a9ec50f2663cf921
...

diff -r f331c8be2425 -r 290c61498d62 src/zorn.agda
--- a/src/zorn.agda	Wed Oct 05 20:40:37 2022 +0900
+++ b/src/zorn.agda	Wed Oct 05 21:36:52 2022 +0900
@@ -395,7 +395,6 @@
       asupf :  {x : Ordinal } → odef A (supf x)
       supf-mono : {x y : Ordinal } → x o≤  y → supf x o≤ supf y
       supf-< : {x y : Ordinal } → supf x o< supf  y → supf x << supf y
-      x≤supfx : {x : Ordinal } → x o≤ z → x o≤ supf x
       supfmax : {x : Ordinal } → z o< x → supf x ≡ supf z
 
       minsup : {x : Ordinal } → x o≤ z  → MinSUP A (UnionCF A f mf ay supf x) 
@@ -666,10 +665,7 @@
               b<A : b o< & A
               b<A = z09 ab
               b<sfx : b o< ZChain.supf zc x
-              b<sfx with trio< x (& A)
-              ... | tri< a ¬b ¬c = ordtrans<-≤ b<x (ZChain.x≤supfx zc (o<→≤ a))
-              ... | tri≈ ¬a b ¬c = ordtrans<-≤ b<x (ZChain.x≤supfx zc (o≤-refl0 b))
-              ... | tri> ¬a ¬b c = subst (λ k → b o< k ) (sym (ZChain.supfmax zc c)) (ordtrans<-≤ b<A ( ZChain.x≤supfx zc (o≤-refl)))
+              b<sfx = ?
               m04 : ¬ HasPrev A (UnionCF A f mf ay supf b) b f
               m04 nhp = proj1 is-sup ( record { ax = HasPrev.ax nhp ; y = HasPrev.y nhp ; ay = chain-mono1 (ZChain.supf-mono zc (o<→≤ b<x)) (HasPrev.ay  nhp) 
                  ; x=fy = HasPrev.x=fy nhp } )
@@ -696,10 +692,7 @@
               m09 : b o< & A
               m09 = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) ab))
               b<sfx : b o< ZChain.supf zc x
-              b<sfx with trio< x (& A)
-              ... | tri< a ¬b ¬c = ordtrans<-≤ b<x (ZChain.x≤supfx zc (o<→≤ a))
-              ... | tri≈ ¬a b ¬c = ordtrans<-≤ b<x (ZChain.x≤supfx zc (o≤-refl0 b))
-              ... | tri> ¬a ¬b c = subst (λ k → b o< k ) (sym (ZChain.supfmax zc c)) (ordtrans<-≤ m09 ( ZChain.x≤supfx zc (o≤-refl)))
+              b<sfx = ? 
               m07 : {z : Ordinal} → FClosure A f y z → z <= ZChain.supf zc b
               m07 {z} fc = ZChain.fcy<sup zc (o<→≤ m09) fc
               m08 : {s z1 : Ordinal} → ZChain.supf zc s o< ZChain.supf zc b 
@@ -844,9 +837,9 @@
           ... | case2 b<x = ⊥-elim ( ¬p<x<op ⟪ px<b , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x  ⟫ ) 
 
           zc4 : ZChain A f mf ay x
-          zc4 with osuc-≡< (ZChain.x≤supfx zc o≤-refl )
+          zc4 with osuc-≡< ?
           ... | case1 sfpx=px = record { supf = supf1 ; sup=u = ? ; asupf = asupf1 ; supf-mono = supf-mono1 ; supf-< = supf-<1  
-              ; x≤supfx = ? ; minsup = ? ; supf-is-sup = ? ; csupf = ?    }  where
+              ; supfmax = ? ; minsup = ? ; supf-is-minsup = ? ; csupf = ?    }  where
 
                  --  we are going to determine (supf x), which is not specified in previous zc
                  --  case1 : supf px ≡ px 
@@ -1089,38 +1082,7 @@
                                   -- (sf1=sf0 ?) (trans ? sfpx=px ) ss<spx
                                   csupf17 : {z1 : Ordinal } → FClosure A f (supf0 s) z1 → odef (UnionCF A f mf ay supf0 px) z1
                                   csupf17 (init as refl ) = ZChain.csupf zc sf<px 
-                                  csupf17 (fsuc x fc) = ZChain.f-next zc ? -- (csupf17 fc)
-
-                 x≤supfx1 : {z : Ordinal} → z o≤ x → z o≤ supf1 z
-                 x≤supfx1 {z} z≤x with trio< z (supf1 z) --  supf1 x o< x → supf1 x o≤ supf1 px → x o< px ∨ supf1 x ≡ supf1 px
-                 ... | tri< a ¬b ¬c = o<→≤ a
-                 ... | tri≈ ¬a b ¬c = o≤-refl0 b
-                 ... | tri> ¬a ¬b c with trio< z px
-                 ... | tri< a ¬b ¬c = ZChain.x≤supfx zc (o<→≤ a)
-                 ... | tri≈ ¬a b ¬c = subst (λ k → k o< osuc px) (sym b) <-osuc
-                 ... | tri> ¬a ¬b lt = ⊥-elim ( o≤> sf04 c ) where --   c : sp1 o< z, lt : px o< z --  supf1 z ≡ sp1 -- supf1 z o< z
-                       z=x : z ≡ x 
-                       z=x with trio< z x
-                       ... | tri< a ¬b ¬c = ⊥-elim ( ¬p<x<op ⟪ lt , subst (λ k → z o< k ) (sym (Oprev.oprev=x op)) a ⟫ )
-                       ... | tri≈ ¬a b ¬c = b
-                       ... | tri> ¬a ¬b c = ⊥-elim ( o≤> z≤x c )
-                       sf01 : supf1 x ≡ sp1
-                       sf01 with trio< x px
-                       ... | tri< a ¬b ¬c = ⊥-elim ( ¬c (pxo<x op ))
-                       ... | tri≈ ¬a b ¬c = ⊥-elim ( ¬c (pxo<x op ))
-                       ... | tri> ¬a ¬b c = refl
-                       sf02 : supf1 px o≤ supf1 x
-                       sf02 = supf-mono1 (o<→≤ (pxo<x op ))
-                       sf00 : px o≤ sp1  --   supf1 px o≤ spuf1 x -- c : sp1 o< x
-                       sf00 = subst₂ (λ j k → j o≤ k ) (trans (sf1=sf0 o≤-refl) (sym sfpx=px)) sf01 sf02
-                       sf04 : z o≤ sp1
-                       sf04 with osuc-≡< sf00
-                       ... | case1 eq = ? where
-                             sf05 : px ≡ sp1 -- z o< osuc x -- z ≡ x
-                             sf05 = eq
-                             sf06 : z ≡ osuc sp1 -- z o< osuc x -- z ≡ x
-                             sf06 = trans z=x (trans (sym (Oprev.oprev=x op)) (cong osuc sf05 ))
-                       ... | case2 lt = subst (λ k → k o≤ sp1 ) (trans (Oprev.oprev=x op) (sym z=x)) (osucc lt )
+                                  csupf17 (fsuc x fc) = ZChain.f-next zc (csupf17 fc)
 
                  record STMP {z : Ordinal} (z≤x : z o≤ x ) : Set (Level.suc n) where
                      field
@@ -1145,7 +1107,7 @@
                         z1≤px = o<→≤ ( ZChain.supf-inject zc (subst (λ k → supf0 z1 o< k ) sfpx=px a ))
                  ... | tri≈ ¬a b ¬c = subst₂ (λ j k → odef j k ) (sym ch1x=pchainpx) zc20 (case2 (init apx sfpx=px )) where
                       z1≤px : z1 o≤ px -- z1 o≤ supf1 z1 ≡ px 
-                      z1≤px = subst (λ k → z1 o< k) (sym (Oprev.oprev=x op)) (supf-inject0 supf-mono1 (ordtrans<-≤ sz1<x (x≤supfx1 o≤-refl ) ))
+                      z1≤px = subst (λ k → z1 o< k) (sym (Oprev.oprev=x op)) (supf-inject0 supf-mono1 (ordtrans<-≤ sz1<x ? ))
                       zc20 : supf0 px ≡ supf1 z1 
                       zc20 = begin
                         supf0 px  ≡⟨ sym sfpx=px ⟩
@@ -1156,7 +1118,7 @@
                       zc21 : px o< z1
                       zc21 =  ZChain.supf-inject zc (subst (λ k → k o< supf0 z1) sfpx=px c  )
                       zc22 : z1 o< x -- c : px o< supf0 z1
-                      zc22 = supf-inject0 supf-mono1 (ordtrans<-≤ sz1<x (x≤supfx1 o≤-refl ) )
+                      zc22 = supf-inject0 supf-mono1 (ordtrans<-≤ sz1<x ? )
                      -- c : px ≡ spuf0 px o< supf0 z1 , px o< z1 o≤ supf1 z1 o< x
 
           ... | case2 px<spfx = ? where