--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/while_loop_verif/verif_loop.agda.replaced	Sun Apr 24 23:13:44 2022 +0900
@@ -0,0 +1,12 @@
+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!$\approx$! !$\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!$\approx$! !$\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 )   
\ No newline at end of file