# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1656254470 -32400
# Node ID 83f93d35b09a33450d2b035352411374fefdf4b2
# Parent  a7e538a7c87f3aff6aafc632373d493a9e334f5e
...

diff -r a7e538a7c87f -r 83f93d35b09a src/zorn.agda
--- a/src/zorn.agda	Sun Jun 26 22:27:17 2022 +0900
+++ b/src/zorn.agda	Sun Jun 26 23:41:10 2022 +0900
@@ -585,14 +585,6 @@
          ... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c = ⊥-elim ( osuc-< w≤x c ) -- o<> c ( ord≤< w≤x )) -- z≡w x o< w
          ... | tri> ¬a ¬b c | t = ⊥-elim ( osuc-< w≤x (ord≤< c  z≤w ) ) -- x o< z → x o< w 
          
-     SZ : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} (ya : odef A y) → ZChain A y f (& A)
-     SZ f mf {y} ay = TransFinite {λ z → ZChain A y f z  } (ind f mf ay ) (& A)
-
-     postulate
-       TFcomm :  { ψ : Ordinal  → Set (Level.suc n) }
-          → (ind :  (x : Ordinal)  → ( (y : Ordinal  ) → y o< x → ψ y ) → ψ x )
-          →  ∀ (x : Ordinal)  →   ind  x (λ y _ → TransFinite ind  y )  ≡ TransFinite ind  x
-
      record ZChain1 ( f : Ordinal → Ordinal )  ( y z : Ordinal ) : Set (Level.suc n) where
       inductive
       field
@@ -603,12 +595,17 @@
      SZ1 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} → (ay : odef A y)
          → (z : Ordinal) → ZChain1 f y z
      SZ1 f mf {y} ay z = TransFinite {λ w → ZChain1 f y w } indp z where
+         open ZChain
+         open ZChain1
          indp :  (x : Ordinal) → ((y₁ : Ordinal) → y₁ o< x → ZChain1 f y y₁) → ZChain1 f y x
          indp x prev with Oprev-p x
          ... | yes op  = sz02 where
-             sz02 : ZChain1 f y ?
+             px = Oprev.oprev op
+             zc1 : ZChain1 f y (Oprev.oprev op)
+             zc1 = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc )
+             sz02 : ZChain1 f y x
              sz02 with ODC.∋-p O A (* x)
-             ... | no noax = {!!}
+             ... | no noax = record { zc = ? ;  chain-mono = ? ; f-total = ? }
              ... | yes noax = {!!}
          ... | no  ¬ox  with trio< x y
          ... | tri< a ¬b ¬c = {!!}
@@ -631,12 +628,8 @@
          nmx mx =  ∅< {HasMaximal} zc5 ( ≡o∅→=od∅  ¬Maximal ) where
               zc5 : odef A (& (Maximal.maximal mx)) ∧ (( y : Ordinal ) →  odef A y → ¬ (* (& (Maximal.maximal mx)) < * y)) 
               zc5 = ⟪  Maximal.A∋maximal mx , (λ y ay mx<y → Maximal.¬maximal<x mx (subst (λ k → odef A k ) (sym &iso) ay) (subst (λ k → k < * y) *iso mx<y) ) ⟫
-         -- zorn04 : ZChain A (& s) (cf nmx) (& A)
-         -- zorn04 = SZ (cf nmx) (cf-is-≤-monotonic nmx) (subst (λ k → odef A k ) &iso as )
          zc0 : ZChain1  (cf nmx) (& s) (osuc (& A))
          zc0 = SZ1 (cf nmx) (cf-is-≤-monotonic nmx) (subst (λ k → odef A k ) &iso as) (osuc (& A))
-         -- zc1 :  IsTotalOrderSet ( ZChain.chain (ZChain1.zc zc0 <-osuc ) )
-         -- zc1 =  ZChain1.f-total zc0 <-osuc 
 
 -- usage (see filter.agda )
 --