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

diff -r 9071e5a77a13 -r 946d6b82aad5 whileTestGears.agda
--- a/whileTestGears.agda	Mon Dec 23 09:48:54 2019 +0900
+++ b/whileTestGears.agda	Mon Dec 23 12:54:36 2019 +0900
@@ -96,7 +96,6 @@
 proofGears : {c10 :  ℕ } → Set
 proofGears {c10} = whileTest' {_} {_} {c10} (λ n p1 →  conversion1 n p1 (λ n1 p2 → whileLoop' n1 p2 (λ n2 →  ( vari n2 ≡ c10 )))) 
 
-
 -- proofGearsMeta : {c10 :  ℕ } →  proofGears {c10}
 -- proofGearsMeta {c10} = {!!} -- net yet done
 
@@ -185,17 +184,16 @@
 whileTestPwPSound :  (c : ℕ) → whileTestP c ( λ env → ⊤ implies (whileTestStateP s1 env) )
 whileTestPwPSound 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 )
-   → (p : pre e0)
-   → e1 ≡ ( f e0 p ( λ e1 s → e1 ))
-   → (pre e0) implies (post e1)
-GearsIdSound e0 _ {pre} {post} f p refl = proof (λ p → (f e0 p (λ e1 s → {!!} ))) where
-    lemma : post (f e0 p (λ e1 s → e1))
-    lemma = subst (λ k → post k ) {!!} {!!}
+   → pre e0 → post e1
+GearsIdSound e0 e1 f p0 = {!!}
 
-hoge : (c : ℕ ) (env : Envc ) → whileTestPwP c ( λ e s → ⊤ implies ((vari e ≡ 0) /\ (varn e ≡ c)))
-hoge c env = {!!} -- GearsIdSound env (λ e → whileTestPwP c )
+hoge : (c : ℕ ) (input output : Envc ) → ? → (vari output ≡ 0) /\ (varn output ≡ c)
+hoge c input output sem = GearsIdSound input output {λ e → ⊤} ? tt
 
 -- induction にする
 {-# TERMINATING #-}