# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1576326469 -32400
# Node ID a9cac7960e81e1d5d489e6c3178bdb86b88bab57
# Parent  2eb30c8e5a206e981155392475550136be1cd702
...

diff -r 2eb30c8e5a20 -r a9cac7960e81 whileTestGears.agda
--- a/whileTestGears.agda	Sat Dec 14 09:25:45 2019 +0900
+++ b/whileTestGears.agda	Sat Dec 14 21:27:49 2019 +0900
@@ -132,18 +132,21 @@
 whileLoopStep env next exit | tri< gt ¬eq _  = next env gt
 whileLoopStep env next exit | tri> _ _ c  = ⊥-elim (m<n⇒n≢0 {varn env} {0} c refl) 
 
-whileTestProof : {l : Level} {t : Set l} → Context → (Code : Context → t) → t
-whileTestProof cxt next = next record cxt { whileDG = out ; whileCond = init } where
+whileTestProof : {l : Level} {t : Set l} → Context → (Code : (cxt : Context ) → ¬ (vari (whileDG cxt) ≡ varn (whileDG cxt) ) → t) → t
+whileTestProof cxt next = next record cxt { whileDG = out ; whileCond = init } i!=n where
     out : Env 
     out =  whileTest (c10 cxt) ( λ e → e ) 
     init : whileTestState (c10 cxt) out
     init = state1 record { pi1 = refl ; pi2 = refl }
+    i!=n : ¬ vari out ≡ varn out
+    i!=n eq = {!!}
 
 {-# TERMINATING #-}
-whileLoopProof : {l : Level} {t : Set l} → Context → (Code : Context → t) (Code : Context → t) → t
-whileLoopProof cxt next exit = whileLoopStep (whileDG cxt)
-    ( λ env lt → next record cxt { whileDG = env ; whileCond = {!!} } ) 
-    ( λ env eq → exit record cxt { whileDG = env ; whileCond = exitCond env eq } )   where
+whileLoopProof : {l : Level} {t : Set l} → (cxt : Context ) → ¬ (vari (whileDG cxt) ≡ varn (whileDG cxt) )
+    → (continue : (cxt : Context ) → ¬ (vari (whileDG cxt) ≡ varn (whileDG cxt) )  → t) (exit : Context → (vari (whileDG cxt) ≡ varn (whileDG cxt) )  → t) → t
+whileLoopProof cxt i!=n next exit = whileLoopStep (whileDG cxt)
+    ( λ env lt → next record cxt { whileDG = env ; whileCond = {!!} } {!!} ) 
+    ( λ env eq → exit record cxt { whileDG = env ; whileCond = exitCond env eq } {!!} )   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
         exitCond : (e : Env ) → 0 ≡ varn e → whileTestState (c10 cxt) e
@@ -151,8 +154,9 @@
         ... | state2 cond | record { eq = eq2 } = finstate ( proof5 nenv {!!} eq1 )
         ... | _ | _ = error
 
-whileConvProof : {l : Level} {t : Set l} → Context → (Code : Context → t) → t
-whileConvProof cxt next = next record cxt { whileCond = postCond } where
+whileConvProof : {l : Level} {t : Set l} → (cxt : Context ) → ¬ (vari (whileDG cxt) ≡ varn (whileDG cxt))
+    → ((cxt : Context ) → ¬ (vari (whileDG cxt) ≡ varn (whileDG cxt)) → t) → t
+whileConvProof cxt i!=n next = next record cxt { whileCond = postCond } i!=n where
     proof4 : (e : Env ) → (vari e ≡ 0) /\ (varn e ≡ c10 cxt)  → varn e + vari e ≡ c10 cxt
     proof4 env p1 = let open ≡-Reasoning  in
           begin
@@ -169,9 +173,10 @@
     ... | state1 cond = state2 (proof4 (whileDG cxt) cond )
     ... | _ = error
 
-{-# TERMINATING #-}
-loop : {l : Level} {t : Set l} → Context → (exit : Context → t) → t
-loop cxt exit = whileLoopProof cxt (λ cxt → loop cxt exit ) exit
+-- {-# TERMINATING #-}
+-- loop : {l : Level} {t : Set l} → (cxt : Context ) → ¬ (vari (whileDG cxt) ≡ varn (whileDG cxt) )
+--    → (exit : (cxt : Context ) → (vari (whileDG cxt) ≡ varn (whileDG cxt) )  → t) → t
+-- loop cxt i!=n exit = whileLoopProof cxt i!=n (λ cxt → loop cxt {!!} {!!} exit ) {!!}
 
 
 {-# TERMINATING #-}
@@ -187,8 +192,8 @@
         
 
 
-proofWhileGear : (c : ℕ) (cxt : Context) → whileTestProof (record cxt { c10 = c ; whileCond = error })
-    $ λ cxt → whileConvProof cxt 
-    $ λ cxt → loop cxt 
-    $ λ cxt → vari (whileDG cxt) ≡ c10 cxt
+proofWhileGear : (c : ℕ) (cxt : Context) → whileTestProof (record cxt { c10 = c ; whileCond = error }) {!!}
+    $ λ cxt i!=n → whileConvProof cxt {!!}
+    $ λ cxt i+n=c10 → loopProof cxt {!!} {!!} ( whileLoopStep (whileDG cxt) {!!} {!!} )
+    $ λ cxt _ → vari (whileDG cxt) ≡ c10 cxt
 proofWhileGear c cxt = {!!}