# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1577084243 -32400
# Node ID def072b6c016b0a642ffbbf9ceeb18ea25fd09be
# Parent  946d6b82aad5f0d3571a0e5f09a42d1f536f08b4
GearsUnitSound

diff -r 946d6b82aad5 -r def072b6c016 whileTestGears.agda
--- a/whileTestGears.agda	Mon Dec 23 12:54:36 2019 +0900
+++ b/whileTestGears.agda	Mon Dec 23 15:57:23 2019 +0900
@@ -181,19 +181,22 @@
 implies2p : {A B : Set } → A implies B  → A → B
 implies2p (proof x) = x
 
-whileTestPwPSound :  (c : ℕ) → whileTestP c ( λ env → ⊤ implies (whileTestStateP s1 env) )
-whileTestPwPSound c = proof ( λ _ → record { pi1 = refl ; pi2 = refl } )
+whileTestPSem :  (c : ℕ) → whileTestP c ( λ env → ⊤ implies (whileTestStateP s1 env) )
+whileTestPSem c = proof ( λ _ → record { pi1 = refl ; pi2 = refl } )
 
 SemGears : (f : {l : Level } {t : Set l } → (e0 : Envc ) → ((e : Envc) → t)  → t ) → Set (succ Zero)
 SemGears f = Envc → Envc → Set
 
-GearsIdSound : (e0 e1 : Envc) {pre : Envc → Set} {post : Envc → Set}
-   (f : {l : Level } {t : Set l } → (e0 : Envc ) → pre e0 → ((e : Envc) → post e → t)  → t )
-   → pre e0 → post e1
-GearsIdSound e0 e1 f p0 = {!!}
+GearsUnitSound : (e0 e1 : Envc) {pre : Envc → Set} {post : Envc → Set}
+   → (f : {l : Level } {t : Set l } → (e0 : Envc ) → (Envc → t)  → t )
+   → (fsem : (e0 : Envc ) → f e0 ( λ e1 → (pre e0) implies (post e1)))
+   → e1 ≡ f e0 (λ e → e )
+   → f e0 (λ e1 → pre e0 implies post e1)
+GearsUnitSound e0 e1 f fsem refl = fsem e0
 
-hoge : (c : ℕ ) (input output : Envc ) → ? → (vari output ≡ 0) /\ (varn output ≡ c)
-hoge c input output sem = GearsIdSound input output {λ e → ⊤} ? tt
+whileTestPSemSound : (c : ℕ ) (input output : Envc ) → output ≡ whileTestP c (λ e → e) → ⊤ implies ((vari output ≡ 0) /\ (varn output ≡ c))
+whileTestPSemSound c input output refl = whileTestPSem c 
+
 
 -- induction にする
 {-# TERMINATING #-}