--- a/src/zorn.agda	Fri Apr 29 17:53:31 2022 +0900
+++ b/src/zorn.agda	Fri Apr 29 18:23:49 2022 +0900
@@ -99,6 +99,24 @@
 ... | case1 s≡x = case2 ( subst₂ (λ j k → j < k ) (sym s≡x) refl x<fx )
 ... | case2 s<x = case2 ( IsStrictPartialOrder.trans PO s<x x<fx )
 
+fcn : {A : HOD} (s : Ordinal) { x : Ordinal} {f : Ordinal → Ordinal} → (mf : ≤-monotonic-f A f) → FClosure A f s x → ℕ
+fcn s mf (init as) = zero
+fcn {A} s {x} {f} mf (fsuc y p) with mf y (A∋fc f mf p)
+... | ⟪ case1 eq , _ ⟫ = fcn s mf p
+... | ⟪ case2 y<fy , _ ⟫ = suc (fcn s mf p )
+
+fcn-suc : {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 ) → suc (fcn s mf cx ) ≡ fcn s mf cy  → * x < * y
+fcn-suc = ?
+
+fcn-< : {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 ) → fcn s mf cx Data.Nat.< fcn s mf cy  → * x < * y
+fcn-< = ?
+
+fcn-fsuc : {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 (f x) ) → * x < * (f x)  → suc (fcn s mf cx ) ≡ fcn s mf cy  
+fcn-fsuc = ?
+
 fcn-cmp : {A : HOD} (s : Ordinal) { x y : Ordinal } (f : Ordinal → Ordinal) (mf : ≤-monotonic-f A f) (imm : immieate-f A f )
     → (cx : FClosure A f s x) → (cy : FClosure A f s y ) → Tri (* x < * y) (* x ≡ * y) (* y < * x )
 fcn-cmp {A} s {.s} {.s} f mf imm (init x) (init x₁) = tri≈ (λ lt → <-irr (case1 refl) lt ) refl (λ lt → <-irr (case1 refl) lt )