# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1544842638 -32400
# Node ID 46b301ad447892b2669d8172e2121a4837f96907
# Parent  e4f087b823d47ae0a0afae6a7a41e41c319b41d1
add some proof

diff -r e4f087b823d4 -r 46b301ad4478 whileTestGears.agda
--- a/whileTestGears.agda	Sat Dec 15 11:38:55 2018 +0900
+++ b/whileTestGears.agda	Sat Dec 15 11:57:18 2018 +0900
@@ -90,11 +90,6 @@
 proof1 : whileTest (λ env → whileLoop env (λ e → (vari e) ≡ 10 ))
 proof1 = refl
 
-
-
--- stmt2Cond : {l : Level} → EnvWithCond {l} → 
--- stmt2Cond env = (Equal (varn' env) 10) ∧ (Equal (vari' env) 0)
-
 whileTest' : {l : Level} {t : Set l}  -> (Code : (env : Env)  -> ((vari env) ≡ 0) ∧ ((varn env) ≡ 10) -> t) -> t
 whileTest' next = next env proof2
   where
@@ -105,13 +100,15 @@
     
 {-# TERMINATING #-}
 whileLoop' : {l : Level} {t : Set l} -> (env : Env) -> ((varn env) + (vari env) ≡ 10) -> (Code : Env -> t) -> t
-whileLoop' env proof next with lt 0 (varn  env)
-whileLoop' env proof next | false = next env 
-whileLoop' env proof next | true = whileLoop' env1 proof3 next
+whileLoop' env proof next with  ( suc zero  ≤? (varn  env) )
+whileLoop' env proof next | no p = next env 
+whileLoop' env proof next | yes p = whileLoop' env1 (proof3 p ) next
     where
       env1 = record {varn = (varn  env) - 1 ; vari = (vari env) + 1}
-      proof3 : varn env1 + vari env1 ≡ 10
-      proof3 = {!!}
+      proof3 : (suc zero  ≤ (varn  env))  → varn env1 + vari env1 ≡ 10
+      proof3 (s≤s lt) with varn  env
+      proof3 (s≤s z≤n) | zero = {!!}
+      proof3 (s≤s lt) | suc n = {!!}
 
 
 conversion1 : {l : Level} {t : Set l } → (env : Env) -> ((vari env) ≡ 0) ∧ ((varn env) ≡ 10)
@@ -133,3 +130,6 @@
 
 proofGears : Set
 proofGears = whileTest' (λ n p1 →  conversion1 n p1 (λ n1 p2 → whileLoop' n1 p2 (λ n2 →  ( vari n2 ≡ 10 )))) 
+
+proofGearsMeta : whileTest' (λ n p1 →  conversion1 n p1 (λ n1 p2 → whileLoop' n1 p2 (λ n2 →  ( vari n2 ≡ 10 )))) 
+proofGearsMeta = refl