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

diff -r 5b17a3601037 -r fdd31b6808db whileTestGears.agda
--- a/whileTestGears.agda	Mon Dec 23 16:36:06 2019 +0900
+++ b/whileTestGears.agda	Mon Dec 23 18:20:42 2019 +0900
@@ -203,13 +203,18 @@
 whileLoopPSem env s next exit | tri≈ ¬a b ¬c = {!!}
 whileLoopPSem env s next exit | tri< a ¬b ¬c  = {!!}
 
+loopPP : (input : Envc ) → Envc
+loopPP input with <-cmp 0 (varn input )
+loopPP input | tri≈ ¬a b ¬c = input
+loopPP input | tri< a ¬b ¬c = {!!} -- loopPP (whileLoopP ?
+-- = whileLoopP input (λ next → loopPP next ) (λ output → output )
+
 whileLoopPSemSound : (input output : Envc )
    → whileTestStateP s2 input
-   →  output ≡ whileLoopP input (λ e → whileLoopP e ? (λ e → e ) ) (λ e → e)
+   →  output ≡ loopPP input
    → (whileTestStateP s2 input ) implies ( whileTestStateP sf output )
-whileLoopPSemSound = {!!}
-
-
+whileLoopPSemSound input output pre refl with <-cmp 0 (varn input )
+... | ttt = {!!}
 
 -- induction にする
 {-# TERMINATING #-}
@@ -219,8 +224,8 @@
 --  wP を Env のRel にする  Env → Env → Set にしちゃう
 whileTestPCallwP : (c :  ℕ ) → Set
 whileTestPCallwP c = whileTestPwP {_} {_} c ( λ env s → loopPwP env (conv env s) ( λ env s → vari env ≡ c )  ) where
-    conv : (env : Envc ) → (vari env ≡ 0) /\ (varn env ≡ c10 env) → varn env + vari env ≡ c10 env
-    conv e record { pi1 = refl ; pi2 = refl } = +zero
+   conv : (env : Envc ) → (vari env ≡ 0) /\ (varn env ≡ c10 env) → varn env + vari env ≡ c10 env
+   conv e record { pi1 = refl ; pi2 = refl } = +zero
 
 
 conv1 : (env : Envc ) → (vari env ≡ 0) /\ (varn env ≡ c10 env) → varn env + vari env ≡ c10 env