--- a/whileTestGears.agda	Sun Dec 15 12:29:13 2019 +0900
+++ b/whileTestGears.agda	Sun Dec 15 19:22:21 2019 +0900
@@ -97,11 +97,17 @@
 proofGears {c10} c = whileTest' {_} {_} {c} {c10} (λ n p1 →  conversion1 n p1 (λ n1 p2 → whileLoop' n1 p2 (λ n2 →  ( vari n2 ≡ c10 )))) 
 
 data whileTestState (c10 : ℕ ) (env : Env ) : Set where
-  error : whileTestState c10 env
+--   error : whileTestState c10 env
   state1 : ((vari env) ≡ 0) /\ ((varn env) ≡ c10) → whileTestState c10 env
   state2 : (varn env + vari env ≡ c10) → whileTestState c10 env
   finstate : ((vari env) ≡ c10 ) → whileTestState c10 env
 
+transition : (c10 : ℕ ) (env0 : Env) → (Env → Env) → Set
+transition c10 env0 prog  = whileTestState c10 env0 → whileTestState c10 (prog env0)
+
+whileTrans : (c10 : ℕ ) (env0 : Env) → transition c10 env0 {!!}
+whileTrans c10 env0 st = {!!}
+
 --
 --      openended Env c  <=>  Context
 --
@@ -109,11 +115,14 @@
 record Context : Set (succ Zero) where
    field 
      c10 : ℕ
-     whileDG : Env 
+     whileDG : Env
      whileCond : whileTestState c10 whileDG
 
 open Context
 
+
+
+
 open import Relation.Nullary
 open import Relation.Binary
 
@@ -122,23 +131,23 @@
 --
 
 whileCondP : Env → Set
-whileCondP env = varn env > 0
+whileCondP env = (varn env > 0) /\  (vari env > 0)
 
 whileDec : (cxt : Context) → Dec (whileCondP (whileDG cxt))
 whileDec cxt = {!!}
 
 whileTestContext : {l : Level} {t : Set l} → Context → (Code : Context → t) → t
-whileTestContext cxt next = next (record cxt { whileDG = record (whileDG cxt) {varn = c10 cxt ; vari = 0} ; whileCond = {!!} } )
+whileTestContext cxt next = next (record cxt { whileDG = record (whileDG cxt) {varn = c10 cxt ; vari = 0} ;  whileCond = {!!} } )
 
 {-# TERMINATING #-}
 whileLoopContext : {l : Level} {t : Set l} → Context → (Code : Context → t) → t
 whileLoopContext cxt next with lt 0 (varn (whileDG cxt) )
 whileLoopContext cxt next | false = next cxt
 whileLoopContext cxt next | true =
-    whileLoopContext (record cxt { whileDG = record (whileDG cxt) {varn = (varn (whileDG cxt)) - 1 ; vari = (vari (whileDG cxt)) + 1} ; whileCond = state2 (proof cxt) } )  next
+    whileLoopContext (record cxt { whileDG = record (whileDG cxt) {varn = (varn (whileDG cxt)) - 1 ; vari = (vari (whileDG cxt)) + 1} ; whileCond = state2 (proof3 cxt) } )  next
       where
-        proof : (cxt : Context) → (varn (whileDG cxt) - 1) + (vari (whileDG cxt) + 1) ≡ c10 cxt
-        proof cxt = {!!} 
+        proof3 : (cxt : Context) → (varn (whileDG cxt) - 1) + (vari (whileDG cxt) + 1) ≡ c10 cxt
+        proof3 cxt = {!!} 
 
 {-# TERMINATING #-}
 whileLoopStep : {l : Level} {t : Set l} → Env → (next : (e : Env ) → t) (exit : (e : Env) → t) → t
@@ -160,14 +169,26 @@
 whileLoopProof : {l : Level} {t : Set l} → (cxt : Context ) → whileCondP (whileDG cxt) 
     → (continue : (cxt : Context ) → whileCondP (whileDG cxt)  → t) (exit : Context → ¬ whileCondP (whileDG cxt)  → t) → t
 whileLoopProof cxt i!=n next exit = whileLoopStep (whileDG cxt)
-    ( λ env → next record cxt { whileDG = env ; whileCond = {!!} } {!!} ) 
+    ( λ env → next record cxt { whileDG = env ; whileCond = (state2 (proof4 env {!!})) } {!!} ) 
     ( λ env → exit record cxt { whileDG = env ; whileCond = exitCond env {!!} } {!!} )   where
         proof5 : (e : Env ) → varn e + vari e ≡ c10 cxt →  0 ≡ varn e → vari e ≡ c10 cxt
         proof5 record { varn = .0 ; vari = vari } refl refl = refl
+        proof4 : (e : Env ) → (vari e ≡ 0) /\ (varn e ≡ c10 cxt)  → varn e + vari e ≡ c10 cxt
+        proof4 e p1 = let open ≡-Reasoning  in
+          begin
+            varn e + vari e
+          ≡⟨ cong ( λ n → n + vari e ) (pi2 p1 ) ⟩
+            (c10 cxt) + vari e
+          ≡⟨ cong ( λ n → (c10 cxt) + n ) (pi1 p1 ) ⟩
+            (c10 cxt) + 0
+          ≡⟨ +-sym {c10 cxt} {0} ⟩
+            c10 cxt
+          ∎
+        
         exitCond : (e : Env ) → 0 ≡ varn e → whileTestState (c10 cxt) e
         exitCond nenv eq1 with whileCond cxt | inspect whileDG cxt
         ... | state2 cond | record { eq = eq2 } = finstate ( proof5 nenv {!!} eq1 )
-        ... | _ | _ = error
+        ... | _ | _ = {!!} -- error
 
 whileConvProof : {l : Level} {t : Set l} → (cxt : Context ) → ¬ (vari (whileDG cxt) ≡ varn (whileDG cxt))
     → ((cxt : Context ) → ¬ (vari (whileDG cxt) ≡ varn (whileDG cxt)) → t) → t
@@ -186,7 +207,7 @@
     postCond : whileTestState (c10 cxt) (whileDG cxt)
     postCond with whileCond cxt
     ... | state1 cond = state2 (proof4 (whileDG cxt) cond )
-    ... | _ = error
+    ... | _ = {!!} -- error
 
 {-# TERMINATING #-}
 loop : {l : Level} {t : Set l} → (cxt : Context ) → whileCondP (whileDG cxt) 
@@ -194,6 +215,7 @@
 loop cxt i!=n exit = whileLoopProof cxt i!=n (λ cxt → loop cxt {!!} {!!} exit ) {!!}
 
 
+
 {-# TERMINATING #-}
 loopProof : {l : Level} {t : Set l} {P Inv : Context → Set } → (c : Context) → (if : (c : Context) → Dec (P c))
           → ( (cont : (c2 : Context) → (P c2) → t) → (exit : (c2 : Context) → ¬ (P c2) → t) → t )
@@ -209,7 +231,7 @@
     → (cxt : Context ) → ( continue : (cxt : Context ) → whileCondP (whileDG cxt)  → t) (exit : Context → ¬ whileCondP (whileDG cxt)  → t) → t
 whileLoopProof' = {!!}
 
-proofWhileGear : (c : ℕ) (cxt : Context) → whileTestProof (record cxt { c10 = c ; whileCond = error }) 
+proofWhileGear : (c : ℕ) (cxt : Context) → whileTestProof (record cxt { c10 = c ; whileCond = {!!} }) -- error
     $ λ cxt i!=n → whileConvProof cxt i!=n
     $ λ cxt i+n=c10 → loopProof cxt whileDec {!!} -- whileLoopProof'
     $ λ cxt _ → {!!}