# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1664620444 -32400
# Node ID b7fb839cdcd04479cbee4c8eafe06aac3700e4e2
# Parent  1a84433ebc1be2795740ce3b23ef12216c80413b
...

diff -r 1a84433ebc1b -r b7fb839cdcd0 src/zorn.agda
--- a/src/zorn.agda	Fri Sep 30 17:48:11 2022 +0900
+++ b/src/zorn.agda	Sat Oct 01 19:34:04 2022 +0900
@@ -829,16 +829,15 @@
           ... | case1 eq = case2 eq
           ... | case2 b<x = ⊥-elim ( ¬p<x<op ⟪ px<b , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x  ⟫ ) 
 
-          -- if previous chain satisfies maximality, we caan reuse it
-          --
-          --    UninCF supf0 px  previous chain u o< px, supf0 px is not included
-          --    UninCF supf0 x   supf0 px is included
-          --           supf0 px ≡ px 
-          --           supf0 px ≡ supf0 x 
-
           zc4 : ZChain A f mf ay x
           zc4 with osuc-≡< (ZChain.x≤supfx zc )
-          ... | case1 sfpx=px = ? where
+          ... | 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
+
+                 --  we are going to determine (supf x), which is not specified in previous zc
+                 --  case1 : supf px ≡ px 
+                 --     supf px is MinSUP of previous chain , supf x ≡ MinSUP of Union of UChain and  FClosure px 
+
                  pchainpx : HOD
                  pchainpx = record { od = record { def = λ z →  (odef A z ∧ UChain A f mf ay supf0 px z ) ∨ FClosure A f px z  } ; odmax = & A ; <odmax = zc00 } where
                       zc00 : {z : Ordinal } → (odef A z ∧ UChain A f mf ay supf0 px z ) ∨ FClosure A f px z → z o< & A
@@ -890,20 +889,44 @@
                  supf1 z with trio< z px 
                  ... | tri< a ¬b ¬c = supf0 z
                  ... | tri≈ ¬a b ¬c = px   --- supf px ≡ px
-                 ... | tri> ¬a ¬b c = sp1 
+                 ... | tri> ¬a ¬b c = sp1  --- this may equal or larger then x, and sp1 ≡ supf x, is not included in UniofCF
 
-                 pchainp : HOD
-                 pchainp = UnionCF A f mf ay supf1  x
+                 asupf1 : {z : Ordinal } → odef A (supf1 z )
+                 asupf1 {z} with trio< z px
+                 ... | tri< a ¬b ¬c = ZChain.asupf zc
+                 ... | tri≈ ¬a b ¬c = subst (λ k → odef A k ) (trans (cong supf0 b) (sym sfpx=px)) ( ZChain.asupf zc )
+                 ... | tri> ¬a ¬b c = MinSUP.asm sup1
 
-                 zc16 : {z : Ordinal } → z o< px → supf1 z ≡ supf0 z
+                 -- ch1x=pchainpx : UnionCF A f mf ay supf1  x ≡ pchainpx
+                 -- ch1x=pchainpx = ?
+
+                 --  UnionCF A f mf ay supf0  x ⊆  UnionCF A f mf ay supf1  x 
+
+                 zc16 : {z : Ordinal } → z o≤ px → supf1 z ≡ supf0 z
                  zc16 {z} z<px with trio< z px
                  ... | tri< a ¬b ¬c = refl
-                 ... | tri≈ ¬a b ¬c = ⊥-elim ( ¬a z<px )
-                 ... | tri> ¬a ¬b c = ⊥-elim ( ¬a z<px )
+                 ... | tri≈ ¬a b ¬c = trans sfpx=px (cong supf0 (sym b))
+                 ... | tri> ¬a ¬b c = ⊥-elim ( o≤> z<px c )
+
+                 record STMP {z : Ordinal} (z≤x : z o≤ x ) : Set (Level.suc n) where
+                     field
+                         tsup : MinSUP A (UnionCF A f mf ay supf1 z)
+                         tsup=sup : supf1 z ≡ MinSUP.sup tsup 
+
+                 sup : {z : Ordinal} → (z≤x : z o≤ x ) → STMP z≤x
+                 sup {z} z≤x with trio< z px 
+                 ... | tri< a ¬b ¬c = record { tsup = record { sup = MinSUP.sup m  ; asm = MinSUP.asm m  
+                         ; x<sup = ? ; minsup = ? } ; tsup=sup = trans (zc16 (o<→≤ a)) (ZChain.supf-is-minsup zc (o<→≤ a))  } where
+                    m = ZChain.minsup zc (o<→≤ a)
+                 ... | tri≈ ¬a b ¬c = record { tsup = record { sup = MinSUP.sup m  ; asm = MinSUP.asm m  
+                         ; x<sup = ? ; minsup = ? } ; tsup=sup = trans (zc16 (o≤-refl0 b)) (ZChain.supf-is-minsup zc (o≤-refl0 b))  } where
+                    m = ZChain.minsup zc (o≤-refl0 b)
+                 ... | tri> ¬a ¬b px<z = record { tsup = record { sup = sp1 ; asm = MinSUP.asm sup1  
+                         ; x<sup = ? ; minsup = ? } ; tsup=sup = ? } where
 
                  supf-mono1 : {z w : Ordinal } → z o≤ w → supf1 z o≤ supf1 w
                  supf-mono1 {z} {w} z≤w with trio< w px 
-                 ... | tri< a ¬b ¬c = subst₂ (λ j k → j o≤ k ) (sym (zc16 (ordtrans≤-< z≤w a))) refl ( supf-mono z≤w )
+                 ... | tri< a ¬b ¬c = subst₂ (λ j k → j o≤ k ) (sym (zc16 (o<→≤ (ordtrans≤-< z≤w a)))) refl ( supf-mono z≤w )
                  ... | tri≈ ¬a refl ¬c with osuc-≡< z≤w 
                  ... | case1 refl = o≤-refl0 zc17 where
                        zc17 : supf1 px ≡ px
@@ -911,60 +934,68 @@
                        ... | tri< a ¬b ¬c = ⊥-elim ( ¬b refl )
                        ... | tri≈ ¬a b ¬c = refl
                        ... | tri> ¬a ¬b c = ⊥-elim ( ¬b refl )
-                 ... | case2 lt = subst₂ (λ j k → j o≤ k ) (sym (zc16 lt)) (sym sfpx=px) ( supf-mono z≤w )
+                 ... | case2 lt = subst₂ (λ j k → j o≤ k ) (sym (zc16 (o<→≤ lt))) (sym sfpx=px) ( supf-mono z≤w )
                  supf-mono1 {z} {w} z≤w | tri> ¬a ¬b c with trio< z px
                  ... | tri< a ¬b ¬c = zc19 where
                        zc21 : MinSUP A (UnionCF A f mf ay supf0 z)
                        zc21 = ZChain.minsup zc (o<→≤ a)
-                       zc23 : odef A sp1
-                       zc23 = MinSUP.asm sup1
                        zc24 : {x₁ : Ordinal} → odef (UnionCF A f mf ay supf0 z) x₁ → (x₁ ≡ sp1) ∨ (x₁ << sp1)
-                       zc24 {x₁} ux = MinSUP.x<sup sup1 ?
+                       zc24 {x₁} ux = MinSUP.x<sup sup1 (case1 (chain-mono f mf ay supf0 (o<→≤ a) ux))
                        zc19 : supf0 z o≤ sp1 
-                       zc19 = subst (λ k → k o≤ sp1) (sym (ZChain.supf-is-minsup zc  (o<→≤ a))) ( MinSUP.minsup zc21 zc23 zc24 )
+                       zc19 = subst (λ k → k o≤ sp1) (sym (ZChain.supf-is-minsup zc  (o<→≤ a))) ( MinSUP.minsup zc21 (MinSUP.asm sup1) zc24 )
                  ... | tri≈ ¬a b ¬c = zc18 where
                        zc21 : MinSUP A (UnionCF A f mf ay supf0 z)
                        zc21 = ZChain.minsup zc (o≤-refl0 b)
+                       zc20 : MinSUP.sup zc21 ≡ px
+                       zc20 = begin
+                         MinSUP.sup zc21 ≡⟨ sym (ZChain.supf-is-minsup zc (o≤-refl0 b)) ⟩
+                         supf0 z ≡⟨ cong supf0 b ⟩
+                         supf0 px ≡⟨ sym sfpx=px ⟩
+                         px ∎ where open ≡-Reasoning
+                       zc24 : {x₁ : Ordinal} → odef (UnionCF A f mf ay supf0 z) x₁ → (x₁ ≡ sp1) ∨ (x₁ << sp1)
+                       zc24 {x₁} ux = MinSUP.x<sup sup1 (case1 (chain-mono f mf ay supf0 (o≤-refl0 b) ux))
                        zc18 : px o≤ sp1 -- supf0 z ≡ px 
-                       zc18 = ?
+                       zc18 = subst (λ k → k o≤ sp1) zc20 ( MinSUP.minsup zc21 (MinSUP.asm sup1) zc24 )
                  ... | tri> ¬a ¬b c = o≤-refl
 
-                 zc10 :  {z : Ordinal} → OD.def (od pchain) z → OD.def (od pchainp) z
-                 zc10 {z} ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ 
-                 zc10 {z} ⟪ az , ch-is-sup u1 u1<x u1-is-sup fc ⟫ = ⟪ az , ch-is-sup u1 (ordtrans u1<x (pxo<x op)) zc15  zc14  ⟫ where
-                    zc14 : FClosure A f (supf1 u1) z
-                    zc14 = subst (λ k → FClosure A f k z) (sym (zc16 u1<x)) fc
-                    zc15 : ChainP A f mf ay supf1 u1
-                    zc15 = record { fcy<sup = λ {z} fcy → subst (λ k →  (z ≡ k) ∨ ( z << k ) ) (sym (zc16 u1<x)) (ChainP.fcy<sup u1-is-sup fcy)
-                       ; order = λ {s} {z1} lt fc1 → subst (λ k → (z1 ≡ k) ∨ ( z1 << k ) ) (sym (zc16 u1<x)) (
-                           ChainP.order u1-is-sup (subst₂ (λ j k → j o< k) (zc17 u1<x lt) (zc16 u1<x) lt) (subst (λ k → FClosure A f k z1) (zc17 u1<x lt) fc1) )
-                       ; supu=u = trans (zc16 u1<x) (ChainP.supu=u u1-is-sup) } where
-                               zc17 : {s u : Ordinal } → u o< px → supf1 s o< supf1 u → supf1 s ≡ supf0 s
-                               zc17 u1<x lt = zc16 (ordtrans ( supf-inject0 supf-mono1 lt) u1<x) 
-
-                 zc11 :  {z : Ordinal} → z o< px  → OD.def (od pchainp) z → OD.def (od pchain) z
-                 zc11 {z} z<px ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ 
-                 zc11 {z} z<px ⟪ az , ch-is-sup u1 u1<x u1-is-sup fc ⟫ = ⟪ az , ch-is-sup u1 (ordtrans u1<x ?) ?  ?  ⟫
+                 supf-<1 : {z0 z1 : Ordinal} → supf1 z0 o< supf1 z1 → supf1 z0 << supf1 z1
+                 supf-<1 {z0} {z1} sz0<sz1 = zc21 where
+                        z0<z1 :  z0 o< z1
+                        z0<z1 = supf-inject0 supf-mono1 sz0<sz1
+                        zc26 : supf0 px <= sp1
+                        zc26 with MinSUP.x<sup sup1 (case2 (init (subst (λ k → odef A k) (sym sfpx=px) (ZChain.asupf zc) ) refl ))
+                        ... | case1 eq = case1 (trans (sym sfpx=px) eq  )
+                        ... | case2 lt = case2 (subst (λ k → k << sp1 ) sfpx=px lt)
+                        zc22 : ¬ px ≡ sp1 → supf0 px << sp1
+                        zc22 not with MinSUP.x<sup sup1 (case2 (init (subst (λ k → odef A k) (sym sfpx=px) (ZChain.asupf zc) ) refl ))
+                        ... | case1 eq = ⊥-elim ( not eq )  -- px ≡ sp1
+                        ... | case2 lt = subst (λ k → k << sp1 ) sfpx=px lt
+                        zc21 : supf1 z0 << supf1 z1
+                        zc21 with trio< z1 px
+                        ... | tri< a ¬b ¬c = subst (λ k → k << supf0 z1) (sym (zc16 (o<→≤ (ordtrans z0<z1 a))))
+                           ( ZChain.supf-< zc (subst (λ k → k o< supf0 z1) (zc16 (o<→≤ (ordtrans z0<z1 a))) sz0<sz1 ))
+                        ... | tri≈ ¬a b ¬c = subst₂ (λ j k → j << k ) (sym (zc16 (o<→≤ (subst (λ k → z0 o< k) b z0<z1 )))) (sym sfpx=px)
+                           ( ZChain.supf-< zc (subst₂ (λ j k → j o< k ) (zc16 (o<→≤ (subst (λ k → z0 o< k) b z0<z1 ))) sfpx=px sz0<sz1 ))
+                        ... | tri> ¬a ¬b px<z1 with trio< z0 px   --- supf1 z1 ≡ sp1
+                        ... | tri< a ¬b ¬c = zc23 where  
+                              zc23 : supf0 z0 << sp1
+                              zc23 with osuc-≡< ( ZChain.supf-mono zc (o<→≤ a) )
+                              ... | case1 eq = subst (λ k → k << sp1 ) (sym eq) (zc22 zc24) where
+                                  zc25 : px ≡ sp1 → supf0 z0 ≡ sp1
+                                  zc25 px=sp1 = begin supf0 z0 ≡⟨ eq ⟩
+                                     supf0 px ≡⟨ sym ( sfpx=px ) ⟩
+                                     px ≡⟨ px=sp1 ⟩
+                                     sp1 ∎ where open ≡-Reasoning
+                                  zc24 : ¬ px ≡ sp1
+                                  zc24 eq1 = ⊥-elim (o<¬≡ (zc25 eq1) sz0<sz1 )
+                              ... | case2 lt with zc26
+                              ... | case1 eq = subst (λ k → supf0 z0 << k ) eq (ZChain.supf-< zc lt) 
+                              ... | case2 lt1 = ptrans (ZChain.supf-< zc lt) lt1
+                        ... | tri≈ ¬a b ¬c = subst (λ k → k << sp1 ) (sym sfpx=px) (zc22 zc23 ) where
+                              zc23 : ¬ px ≡ sp1
+                              zc23 eq = ⊥-elim (o<¬≡  eq sz0<sz1 )
+                        ... | tri> ¬a ¬b c = ⊥-elim ( o<¬≡ refl sz0<sz1 )
 
-                 zc12 :  {z : Ordinal} → OD.def (od pchainp) z → OD.def (od pchainpx) z
-                 zc12 {z} ⟪ az , ch-init fc ⟫ = case1 ⟪ az , ch-init fc ⟫ 
-                 zc12 {z} ⟪ az , ch-is-sup u1 u1<x u1-is-sup fc ⟫ = ?
-
-                 zc13 :  {z : Ordinal} → OD.def (od pchainpx) z → OD.def (od pchainp) z
-                 zc13 {z} (case1 ⟪ az , ch-init fc ⟫ ) = ⟪ az , ch-init fc ⟫ 
-                 zc13 {z} (case1 ⟪ az , ch-is-sup u1 u1<x u1-is-sup fc ⟫ ) = ⟪ az , ch-is-sup u1 (ordtrans u1<x (pxo<x op)) ?  ?  ⟫
-                 zc13 {z} (case2 fc) = ⟪ ? , ch-is-sup ? ? ?  ?  ⟫
-
-                 record STMP {z : Ordinal} (z≤x : z o≤ x ) : Set (Level.suc n) where
-                     field
-                         tsup : SUP A (UnionCF A f mf ay supf1 z)
-                         tsup=sup : supf1 z ≡ & (SUP.sup tsup ) 
-
-                 sup : {z : Ordinal} → (z≤x : z o≤ x ) → STMP z≤x
-                 sup {z} z≤x with trio< z px 
-                 ... | tri< a ¬b ¬c = record { tsup = ? ; tsup=sup = ? }
-                 ... | tri≈ ¬a b ¬c = record { tsup = ?  ; tsup=sup = ? }
-                 ... | tri> ¬a ¬b px<z = record { tsup = ? ; tsup=sup = ? }
 
                  csupf1 : {b : Ordinal } → supf1 b o< x → odef (UnionCF A f mf ay supf1 x) (supf1 b) 
                  csupf1 {b} sb<z = ⟪ asb , ch-is-sup (supf1 b) sb<z 
@@ -985,6 +1016,10 @@
                     ... | case2 lt = ?
 
           ... | case2 px<spfx = ? where
+
+                 --  case2 : px o< supf px 
+                 --     supf px is not MinSUP of previous chain , supf x ≡ supf px
+
             -- record { supf = supf0 ;  asupf = ZChain.asupf zc ; sup = λ lt → STMP.tsup (sup lt ) ; supf-mono = supf-mono 
             --              ; supf-< = ? ; sup=u = sup=u ; supf-is-sup = λ lt → STMP.tsup=sup (sup lt) }  where
                  supf1 : Ordinal → Ordinal