TerminatingLoopS : {l : Level} {t : Set l} (Index : Set ) !$\rightarrow$! {Invraiant : Index !$\rightarrow$! Set } !$\rightarrow$! ( reduce : Index !$\rightarrow$! !$\mathbb{N}$!)
   !$\rightarrow$! (loop : (r : Index)  !$\rightarrow$! Invraiant r !$\rightarrow$! (next : (r1 : Index)  !$\rightarrow$! Invraiant r1 !$\rightarrow$! reduce r1 < reduce r  !$\rightarrow$! t ) !$\rightarrow$! t)
   !$\rightarrow$! (r : Index) !$\rightarrow$! (p : Invraiant r)  !$\rightarrow$! t 
TerminatingLoopS {_} {t} Index {Invraiant} reduce loop  r p with <-cmp 0 (reduce r)
... | tri≈ !$\neg$!a b !$\neg$!c = loop r p (!$\lambda$! r1 p1 lt !$\rightarrow$! !$\bot$!-elim (lemma3 b lt) ) 
... | tri< a !$\neg$!b !$\neg$!c = loop r p (!$\lambda$! r1 p1 lt1 !$\rightarrow$! TerminatingLoop1 (reduce r) r r1 (!$\leq$!-step lt1) p1 lt1 ) where 
    TerminatingLoop1 : (j : !$\mathbb{N}$!) !$\rightarrow$! (r r1 : Index) !$\rightarrow$! reduce r1 < suc j  !$\rightarrow$! Invraiant r1 !$\rightarrow$!  reduce r1 < reduce r !$\rightarrow$! t
    TerminatingLoop1 zero r r1 n!$\leq$!j p1 lt = loop r1 p1 (!$\lambda$! r2 p1 lt1 !$\rightarrow$! !$\bot$!-elim (lemma5 n!$\leq$!j lt1)) 
    TerminatingLoop1 (suc j) r r1  n!$\leq$!j p1 lt with <-cmp (reduce r1) (suc j)
    ... | tri< a !$\neg$!b !$\neg$!c = TerminatingLoop1 j r r1 a p1 lt 
    ... | tri≈ !$\neg$!a b !$\neg$!c = loop r1 p1 (!$\lambda$! r2 p2 lt1 !$\rightarrow$! TerminatingLoop1 j r1 r2 (subst (!$\lambda$! k !$\rightarrow$! reduce r2 < k ) b lt1 ) p2 lt1 )
    ... | tri> !$\neg$!a !$\neg$!b c =  !$\bot$!-elim ( nat-!$\leq$!> c n!$\leq$!j )