# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1576738091 -32400
# Node ID 0bde332e121598dfb00f3bea44c93232b0276842
# Parent  3f4f93ac841dcc9e10c137b3671c878a9a4c3873
use state as t

diff -r 3f4f93ac841d -r 0bde332e1215 whileTestGears.agda
--- a/whileTestGears.agda	Wed Dec 18 20:34:00 2019 +0900
+++ b/whileTestGears.agda	Thu Dec 19 15:48:11 2019 +0900
@@ -123,7 +123,7 @@
 
 data whileTestStateP (c10 i n : ℕ ) : Set where
   pstate1 : (i ≡ 0) /\ (n ≡ c10) → whileTestStateP c10 i n    -- n ≡ c10
-  pstate2 : (0 < n) → (n < c10) → (n + i ≡ c10)        → whileTestStateP c10 i n    -- 0 < n < c10
+  pstate2 : (0 ≤ n) → (n ≤ c10) → (n + i ≡ c10)        → whileTestStateP c10 i n    -- 0 < n < c10
   pfinstate : (n ≡ 0 ) → (i ≡ c10 )         → whileTestStateP c10 i n    -- n ≡ 0
 
 record EnvP : Set (succ Zero) where
@@ -139,7 +139,10 @@
 
 s2 : (e : EnvP) → varn (env e) > 0 → varn (env e) < c10 e → EnvP
 s2 e n>0 n<c10 with <-cmp 0 (varn (env e))
-s2 e n>0 n<c10 | tri< a ¬b ¬c = record { env = record { varn = varn (env e) - 1 ; vari = vari (env e) + 1 } ; c10 = c10 e ; cx = pstate2 {!!} {!!} {!!} }
+s2 e n>0 n<c10 | tri< a ¬b ¬c =
+     record e { env = record { varn = varn (env e) - 1 ; vari = vari (env e) + 1 } ; cx = pstate2 {!!} {!!} {!!} } where
+        s2-1 : 0 ≤ (varn (env e) - 1)
+        s2-1 = {!!}
 s2 e n>0 n<c10 | tri≈ ¬a b ¬c = record { env = record { varn = varn (env e) - 1 ; vari = vari (env e) + 1 } ; c10 = c10 e ; cx = pfinstate {!!} {!!} }
 
 s3 : (e : EnvP) → varn (env e) ≡ 0 → vari (env e) ≡ c10 e
@@ -165,9 +168,9 @@
 
 {-# TERMINATING #-}
 loopPwithProof : {l : Level} {t : Set l} → (e : EnvP ) → (exit : (e : EnvP ) → t ) → t
-loopPwithProof e exit = whileLoopP (env e) (λ e1 → loopPwithProof record e { env = e1 ; cx = {!!} } exit ) (λ env → exit {!!} ) where
-    lemma :  {!!}
-    lemma = {!!}
+loopPwithProof e exit with  <-cmp 0 (varn (env e)) | whileLoopP (env e) (λ e1 → pstate2 {!!} {!!} {!!} ) ( λ env → pfinstate {!!} {!!} )
+loopPwithProof e exit | tri≈ ¬a b ¬c | tt = loopPwithProof {!!} {!!}
+loopPwithProof e exit | tri< a ¬b ¬c | tt = exit {!!}
 
 ConvP : (e : EnvP) → EnvP
 ConvP = {!!}