# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1651306055 -32400
# Node ID d94f90607a7c13f943b35750e5ee34706f094841
# Parent  42ad203ff9134fae3beb11d4004e2fb77be60306
...

diff -r 42ad203ff913 -r d94f90607a7c src/zorn.agda
--- a/src/zorn.agda	Sat Apr 30 14:53:04 2022 +0900
+++ b/src/zorn.agda	Sat Apr 30 17:07:35 2022 +0900
@@ -164,21 +164,41 @@
 
 fcn-imm : {A : HOD} (s : Ordinal) { x y : Ordinal } (f : Ordinal → Ordinal) (mf : ≤-monotonic-f A f) 
     → (cx : FClosure A f s x) → (cy : FClosure A f s y ) → ¬ ( ( * x < * y ) ∧ ( * y < * (f x )) ) 
-fcn-imm {A} s {x} {y} f mf cx cy ⟪ x<y , y<fx ⟫ = {!!} where
-      fc17 : {x y : Ordinal } → (cx : FClosure A f s x) → (cy : FClosure A f s y ) → * y < * (f x ) → (y ≡ x ) ∨ ( * y < * x )
-      fc17 = {!!}
-      fc18 : {x : Ordinal } → (cx : FClosure A f s x) → {!!} -- (y ≡ x ) ∨ ( y ≡ f x )     * x < * y → ¬ ( * y < * ( f x ) )Ljjjj
-      fc18 = {!!}
-      ncx : { x : Ordinal } → (cx : FClosure A f s x) →  (cx1 : FClosure A f s (f x) ) → cx1 ≡ fsuc x cx
-      ncx {x} (init x₁) cx1 = {!!}
-      ncx {.(f x)} (fsuc x cx) cx1 = {!!}
-      fc16 : (x : Ordinal ) → (cx : FClosure A f s x) → (fcn s mf cx  ≡ fcn s mf (fsuc x cx)) ∨ ( suc (fcn s mf cx ) ≡ fcn s mf (fsuc x cx))
-      fc16 x (init sa) with proj1 (mf s sa )
-      ... | case1 _ = case1 refl
-      ... | case2 _ = case2 refl
-      fc16 .(f x) (fsuc x cx ) with proj1 (mf (f x) (A∋fc s f mf (fsuc x cx)) )
-      ... | case1 _ = case1 refl 
-      ... | case2 _ = case2 refl
+fcn-imm {A} s {x} {y} f mf cx cy ⟪ x<y , y<fx ⟫ = fc21 where
+      fc20 : fcn s mf cy Data.Nat.< suc (fcn s mf cx) → (fcn s mf cy ≡ fcn s mf cx) ∨ ( fcn s mf cy Data.Nat.< fcn s mf cx )
+      fc20 y<sx with <-cmp ( fcn s mf cy ) (fcn s mf cx )
+      ... | tri< a ¬b ¬c = case2 a
+      ... | tri≈ ¬a b ¬c = case1 b
+      ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> y<sx (s≤s c))
+      fc17 : {x y : Ordinal } → (cx : FClosure A f s x) → (cy : FClosure A f s y ) → suc (fcn s mf cx) ≡ fcn s mf cy → * (f x ) ≡ * y
+      fc17 {x} {y} cx cy sx=y = fc18 (fcn s mf cy) cx cy refl sx=y  where
+          fc18 : (i : ℕ ) → {y : Ordinal } → (cx : FClosure A f s x ) (cy : FClosure A f s y ) → (i ≡ fcn s mf cy ) → suc (fcn s mf cx) ≡  i → * (f x) ≡ * y
+          fc18 (suc i) {y} cx (fsuc y1 cy)  i=y sx=i with proj1 (mf y1 (A∋fc s f mf cy ) )
+          ... | case1 y=fy = subst (λ k → * (f x) ≡  k ) y=fy ( fc18 (suc i) {y1} cx cy i=y sx=i)  -- dereference
+          ... | case2 y<fy = subst₂ (λ j k → * (f j) ≡ * (f k) ) &iso &iso (cong (λ k → * (f (& k) ) ) fc19) where
+               fc19 : * x ≡ * y1
+               fc19 = fcn-inject s mf cx cy (cong pred ( trans sx=i i=y ))
+      fc21 :  ⊥
+      fc21 with <-cmp (suc ( fcn s mf cx )) (fcn s mf cy )
+      ... | tri< a ¬b ¬c = <-irr (case2 y<fx) (fc22 a) where -- suc ncx < ncy
+           cxx :  FClosure A f s (f x)
+           cxx = fsuc x cx 
+           fc16 : (x : Ordinal ) → (cx : FClosure A f s x) → (fcn s mf cx  ≡ fcn s mf (fsuc x cx)) ∨ ( suc (fcn s mf cx ) ≡ fcn s mf (fsuc x cx))
+           fc16 x (init sa) with proj1 (mf s sa )
+           ... | case1 _ = case1 refl
+           ... | case2 _ = case2 refl
+           fc16 .(f x) (fsuc x cx ) with proj1 (mf (f x) (A∋fc s f mf (fsuc x cx)) )
+           ... | case1 _ = case1 refl 
+           ... | case2 _ = case2 refl
+           fc22 : (suc ( fcn s mf cx ))  Data.Nat.< (fcn s mf cy ) → * (f x) < * y
+           fc22 a with fc16 x cx
+           ... | case1 eq = fcn-< s mf cxx cy (subst (λ k → k Data.Nat.< fcn s mf cy ) eq (<-trans a<sa a))
+           ... | case2 eq = fcn-< s mf cxx cy (subst (λ k → k Data.Nat.< fcn s mf cy ) eq a )
+      ... | tri≈ ¬a b ¬c = <-irr (case1 (fc17 cx cy b)) y<fx
+      ... | tri> ¬a ¬b c with fc20 c -- ncy < suc ncx
+      ... | case1 y=x = <-irr (case1 ( fcn-inject s mf cy cx  y=x ))  x<y
+      ... | case2 y<x = <-irr (case2 x<y) (fcn-< s mf cy cx y<x ) 
+
 
 -- open import Relation.Binary.Properties.Poset as Poset