--- a/hoareBinaryTree.agda	Mon Dec 06 06:59:55 2021 +0900
+++ b/hoareBinaryTree.agda	Tue Dec 07 18:28:06 2021 +0900
@@ -533,6 +533,25 @@
     ... | tri≈ ¬a b ¬c = loop r1 p1 (λ r2 p2 lt1 → TerminatingLoop1 j r1 r2 (subst (λ k → reduce r2 < k ) b lt1 ) p2 lt1 )
     ... | tri> ¬a ¬b c =  ⊥-elim ( nat-≤> c n≤j )   
 
+record LoopTermination {n : Level} {Index : Set n } { reduce : Index → ℕ }
+       (r : Index ) (C : Set n) : Set (Level.suc n) where
+   field
+     rd :  (r1 : Index) → reduce r1 < reduce r
+     ci : C -- data continuation
+
+TerminatingLoopC : {l n : Level} {t : Set l} (Index : Set n ) → {C : Set n } → ( reduce : Index → ℕ)
+   → (r : Index) → (P : LoopTermination r C )  
+   → (loop : (r : Index)  → LoopTermination {_} {_} {reduce} r C → (next : (r1 : Index)  → LoopTermination r1 C  → t ) → t) → t
+TerminatingLoopC {_} {_} {t} Index {C} reduce r P loop with <-cmp 0 (reduce r)
+... | tri≈ ¬a b ¬c = loop r P (λ r1 p1 → ⊥-elim (lemma3 b (LoopTermination.rd P r1)))
+... | tri< a ¬b ¬c = loop r P (λ r1 p1 → TerminatingLoop1 (reduce r) r r1 (≤-step (LoopTermination.rd P r1)) p1 (LoopTermination.rd P r1)) where 
+    TerminatingLoop1 : (j : ℕ) → (r r1 : Index) → reduce r1 < suc j  → {!!} →  reduce r1 < reduce r → t
+    TerminatingLoop1 zero r r1 n≤j p1 lt = loop r1 {!!} (λ r2 P1 → ⊥-elim (lemma5 n≤j (LoopTermination.rd P1 r2))) 
+    TerminatingLoop1 (suc j) r r1  n≤j p1 lt with <-cmp (reduce r1) (suc j)
+    ... | tri< a ¬b ¬c = TerminatingLoop1 j r r1 a p1 lt 
+    ... | tri≈ ¬a b ¬c = loop r1 {!!} (λ r2 p2 → TerminatingLoop1 j r1 r2 (subst (λ k → reduce r2 < k ) b {!!} ) p2 {!!} )
+    ... | tri> ¬a ¬b c =  ⊥-elim ( nat-≤> c n≤j )   
+
 record ReplCond {n  : Level} {A : Set n} (C : ℕ → bt A → List (bt A) → Set n)   : Set (Level.suc n) where
    field
       c1 : (key : ℕ) → (repl : bt A) → (stack : List (bt A)) → C key repl stack