--- a/whileTestGears.agda	Sat Dec 21 16:49:07 2019 +0900
+++ b/whileTestGears.agda	Sat Dec 21 17:49:15 2019 +0900
@@ -183,6 +183,55 @@
     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
+conv1 e record { pi1 = refl ; pi2 = refl } = +zero
+
+-- = whileTestPwP (suc c) (λ env s → loopPwP env (conv1 env s) (λ env₁ s₁ → {!!}))
+
 {-# TERMINATING #-}
 Proof : (c :  ℕ ) → whileTestPCallwP c
-Proof c = Proof c
+Proof zero = whileTestPwP {_} {_} zero ( λ env s → loopPwP env (conv env s) ( λ env s → refl)  )
+  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
+Proof (suc c) = whileTestPwP {_} {_} c ( λ env s → loopPwP env (conv env s) ( λ env s → lem ))
+  where
+    lem : whileLoopPwP (record { c10 = suc c ; varn = c ; vari = 0 + 1 }) ({!!})
+      (λ env s → loopPwP env s (λ env₁ s₁ → vari env₁ ≡ suc c)) (λ env s3 → {!!})
+    lem = {!!}
+    conv : (env : Envc ) → (vari env ≡ 0) /\ (varn env ≡ c10 env) → varn env + vari env ≡ c10 env
+    conv e record { pi1 = refl ; pi2 = refl } = +zero
+
+
+{--
+-- whileLoopPwP : {l : Level} {t : Set l}   → (env : Envc ) → whileTestStateP s2 env
+--     → (next : (env : Envc ) → whileTestStateP s2 env  → t)
+--     → (exit : (env : Envc ) → whileTestStateP sf env  → t) → t
+
+next : (whileTestGears.proof5
+     (record { c10 = suc c ; varn = suc c ; vari = 0 })
+     (<ᵇ⇒< 0 (suc c) Agda.Builtin.Unit.⊤.tt)
+     (λ x →
+        Relation.Nullary.Reflects.invert (ofⁿ (λ ())) (≡⇒≡ᵇ 0 (suc c) x))
+     (<⇒≯ (<ᵇ⇒< 0 (suc c) Agda.Builtin.Unit.⊤.tt))
+     (whileTestGears.conv (suc c) (whileTestP (suc c) (λ env₁ → env₁))
+      (record { pi1 = refl ; pi2 = refl }))
+     (λ env₁ s₁ → loopPwP env₁ s₁ (λ env₂ s₂ → vari env₂ ≡ suc c))
+     (λ env₁ s₁ → vari env₁ ≡ suc c)
+     (<ᵇ⇒< 0 (suc c) Agda.Builtin.Unit.⊤.tt))
+
+exit : (whileTestGears.conv (suc c) (whileTestP (suc c) (λ env₁ → env₁))
+      (record { pi1 = refl ; pi2 = refl }))
+     (λ env₁ s₁ → loopPwP env₁ s₁ (λ env₂ s₂ → vari env₂ ≡ suc c))
+     (λ env₁ s₁ → vari env₁ ≡ suc c)
+     (<ᵇ⇒< 0 (suc c) Agda.Builtin.Unit.⊤.tt))
+    (λ env₁ s₁ → loopPwP env₁ s₁ (λ env₂ s₂ → vari env₂ ≡ suc c))
+    (λ env₁ s₁ → vari env₁ ≡ suc c)
+
+    | (<-cmp 0 c
+       | Relation.Nullary.Decidable.Core.map′ (≡ᵇ⇒≡ 0 c) (≡⇒≡ᵇ 0 c)
+         (Data.Bool.Properties.T? (0 ≡ᵇ c))
+       | Data.Bool.Properties.T? (0 <ᵇ c))
+
+--}