# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1576283145 -32400
# Node ID 2eb30c8e5a206e981155392475550136be1cd702
# Parent  7049fbaf5e18f5827569c6606dc111eb29c8ba91
whileLoopStep

diff -r 7049fbaf5e18 -r 2eb30c8e5a20 whileTestGears.agda
--- a/whileTestGears.agda	Fri Dec 13 20:33:52 2019 +0900
+++ b/whileTestGears.agda	Sat Dec 14 09:25:45 2019 +0900
@@ -126,18 +126,11 @@
 
 
 {-# TERMINATING #-}
-whileLoopStep : {l : Level} {t : Set l} → Env → (Code : (e : Env ) → 1 ≤ varn e → t) (Code : (e : Env) → 0 ≡ varn e  → t) → t
+whileLoopStep : {l : Level} {t : Set l} → Env → (next : (e : Env ) → 1 ≤ varn e → t) (exit : (e : Env) → 0 ≡ varn e  → t) → t
 whileLoopStep env next exit with <-cmp 0 (varn env)
 whileLoopStep env next exit | tri≈ _ eq _ = exit env eq
-whileLoopStep env next exit | tri< gt ¬eq _  = {!!}
-      where
-        lem : (env : Env) → (1 ≤ varn env) → 1 ≤ (varn env - 1)
-        lem env (s≤s 1<varn) with 1 ≤? varn env
-        lem env (s≤s 1<varn) | no ¬p = {!!}
-        lem env (s≤s 1<varn) | yes p = ⊥-elim (¬eq ({!!}))
-        -- n が 0 の時 は正しい、　n が1の時正しくない
-
-whileLoopStep env next exit | tri> _ _ c  = ⊥-elim (m<n⇒n≢0 {varn env} {0} c refl) -- can't happen
+whileLoopStep env next exit | tri< gt ¬eq _  = next env gt
+whileLoopStep env next exit | tri> _ _ c  = ⊥-elim (m<n⇒n≢0 {varn env} {0} c refl) 
 
 whileTestProof : {l : Level} {t : Set l} → Context → (Code : Context → t) → t
 whileTestProof cxt next = next record cxt { whileDG = out ; whileCond = init } where