# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1577086566 -32400
# Node ID 5b17a360103772bdb0b8b92aff5cbe49e0cd8e80
# Parent  def072b6c016b0a642ffbbf9ceeb18ea25fd09be
try loop

diff -r def072b6c016 -r 5b17a3601037 whileTestGears.agda
--- a/whileTestGears.agda	Mon Dec 23 15:57:23 2019 +0900
+++ b/whileTestGears.agda	Mon Dec 23 16:36:06 2019 +0900
@@ -190,12 +190,25 @@
 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
+GearsUnitSound e0 e1 f fsem = fsem e0
+
+whileTestPSemSound : (c : ℕ ) (output : Envc ) → output ≡ whileTestP c (λ e → e) → ⊤ implies ((vari output ≡ 0) /\ (varn output ≡ c))
+whileTestPSemSound c output refl = whileTestPSem c 
 
-whileTestPSemSound : (c : ℕ ) (input output : Envc ) → output ≡ whileTestP c (λ e → e) → ⊤ implies ((vari output ≡ 0) /\ (varn output ≡ c))
-whileTestPSemSound c input output refl = whileTestPSem c 
+whileLoopPSem : {l : Level} {t : Set l}   → (input : Envc ) → whileTestStateP s2 input
+    → (next : (output : Envc ) → (whileTestStateP s2 input ) implies (whileTestStateP s2 output)  → t)
+    → (exit : (output : Envc ) → (whileTestStateP s2 input ) implies (whileTestStateP sf output)  → t) → t
+whileLoopPSem env s next exit with <-cmp 0 (varn env)
+whileLoopPSem env s next exit | tri≈ ¬a b ¬c = {!!}
+whileLoopPSem env s next exit | tri< a ¬b ¬c  = {!!}
+
+whileLoopPSemSound : (input output : Envc )
+   → whileTestStateP s2 input
+   →  output ≡ whileLoopP input (λ e → whileLoopP e ? (λ e → e ) ) (λ e → e)
+   → (whileTestStateP s2 input ) implies ( whileTestStateP sf output )
+whileLoopPSemSound = {!!}
+
 
 
 -- induction にする