# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1576996886 -32400
# Node ID 87e125b119997e0157e910b0173bd5fa49e968f5
# Parent  222dd3869ab06f9abf17b2663840fd702ad5a858
...

diff -r 222dd3869ab0 -r 87e125b11999 whileTestGears.agda
--- a/whileTestGears.agda	Sun Dec 22 09:15:44 2019 +0900
+++ b/whileTestGears.agda	Sun Dec 22 15:41:26 2019 +0900
@@ -176,6 +176,14 @@
          c10 env
       ∎
 
+whileTestPwPSound :  (c : ℕ) → whileTestPwP c ( λ env s → whileTestStateP s1 env )
+whileTestPwPSound c = record { pi1 = refl ; pi2 = refl }
+
+GearsIdSound : (env : Envc) {post : Envc → Set} (f : {l : Level } {t : Set l } → Envc → ((e : Envc) → post e → t ) → t )  → f env ( λ env s → post env )
+GearsIdSound env {post} f = {!!}
+
+-- hoge : (c : ℕ ) (env : Envc ) → whileTestPwP c ( λ e s → (vari e ≡ 0) /\ (varn e ≡ c))
+-- hoge c env = GearsIdSound env (λ e → whileTestPwP c )
 
 -- induction にする
 {-# TERMINATING #-}