|
1
|
1 TerminatingLoopS : {l : Level} {t : Set l} (Index : Set ) !$\rightarrow$! {Invraiant : Index !$\rightarrow$! Set } !$\rightarrow$! ( reduce : Index !$\rightarrow$! !$\mathbb{N}$!)
|
|
|
2 !$\rightarrow$! (loop : (r : Index) !$\rightarrow$! Invraiant r !$\rightarrow$! (next : (r1 : Index) !$\rightarrow$! Invraiant r1 !$\rightarrow$! reduce r1 < reduce r !$\rightarrow$! t ) !$\rightarrow$! t)
|
|
|
3 !$\rightarrow$! (r : Index) !$\rightarrow$! (p : Invraiant r) !$\rightarrow$! t
|
|
|
4 TerminatingLoopS {_} {t} Index {Invraiant} reduce loop r p with <-cmp 0 (reduce r)
|
|
|
5 ... | tri≈ !$\neg$!a b !$\neg$!c = loop r p (!$\lambda$! r1 p1 lt !$\rightarrow$! !$\bot$!-elim (lemma3 b lt) )
|
|
|
6 ... | 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
|
|
|
7 TerminatingLoop1 : (j : !$\mathbb{N}$!) !$\rightarrow$! (r r1 : Index) !$\rightarrow$! reduce r1 < suc j !$\rightarrow$! Invraiant r1 !$\rightarrow$! reduce r1 < reduce r !$\rightarrow$! t
|
|
|
8 TerminatingLoop1 zero r r1 n!$\leq$!j p1 lt = loop r1 p1 (!$\lambda$! r2 p1 lt1 !$\rightarrow$! !$\bot$!-elim (lemma5 n!$\leq$!j lt1))
|
|
|
9 TerminatingLoop1 (suc j) r r1 n!$\leq$!j p1 lt with <-cmp (reduce r1) (suc j)
|
|
|
10 ... | tri< a !$\neg$!b !$\neg$!c = TerminatingLoop1 j r r1 a p1 lt
|
|
|
11 ... | 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 )
|
|
|
12 ... | tri> !$\neg$!a !$\neg$!b c = !$\bot$!-elim ( nat-!$\leq$!> c n!$\leq$!j ) |
