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 )