# HG changeset patch
# User ryokka
# Date 1575884851 -32400
# Node ID a39a828207421701ff805b5b994287aca1800548
# Parent  e668962ac31a59661b5e0ddc491df9448a7d4b0e
add whileTestCondition

diff -r e668962ac31a -r a39a82820742 utilities.agda
--- a/utilities.agda	Tue Dec 25 08:45:06 2018 +0900
+++ b/utilities.agda	Mon Dec 09 18:47:31 2019 +0900
@@ -1,9 +1,10 @@
+{-# OPTIONS --allow-unsolved-metas #-}
 module utilities where
 
 open import Function
 open import Data.Nat
 open import Data.Product
-open import Data.Bool hiding ( _≟_ )
+open import Data.Bool hiding ( _≟_  ; _≤?_)
 open import Level renaming ( suc to succ ; zero to Zero )
 open import Relation.Nullary using (¬_; Dec; yes; no)
 open import Relation.Binary.PropositionalEquality
@@ -158,8 +159,8 @@
 
 Equal+1 : { x y : ℕ } →  Equal x y ≡ Equal (suc x) (suc y)
 Equal+1 {x} {y} with  x ≟ y
-Equal+1 {x} {.x} | yes refl = refl
-Equal+1 {x} {y} | no ¬p = refl
+Equal+1 {x} {.x} | yes refl = {!!}
+Equal+1 {x} {y} | no ¬p = {!!}
 
 open import Data.Empty 
 
diff -r e668962ac31a -r a39a82820742 whileTestGears.agda
--- a/whileTestGears.agda	Tue Dec 25 08:45:06 2018 +0900
+++ b/whileTestGears.agda	Mon Dec 09 18:47:31 2019 +0900
@@ -2,7 +2,7 @@
 
 open import Function
 open import Data.Nat
-open import Data.Bool hiding ( _≟_ )
+open import Data.Bool hiding ( _≟_ ; _≤?_ ; _≤_)
 open import Level renaming ( suc to succ ; zero to Zero )
 open import Relation.Nullary using (¬_; Dec; yes; no)
 open import Relation.Binary.PropositionalEquality
@@ -96,3 +96,30 @@
 
 proofGearsMeta : {c10 :  ℕ } → whileTest' {_} {_} {c10} (λ n p1 →  conversion1 n p1 (λ n1 p2 → whileLoop' n1 p2 (λ n2 →  ( vari n2 ≡ c10 )))) 
 proofGearsMeta {c10} = {!!}
+
+data whileTestState : Set where
+  
+  state1 : whileTestState
+  state2 : whileTestState
+
+
+record whileTestCondition  (c10 : ℕ)  (t : whileTestState)  : Set where
+  inductive
+  field
+    case1 : (env : Env)  → (t ≡ state1) → ((vari env) ≡ 0) /\ ((varn env) ≡ c10) → whileTestCondition c10 state2
+    case2 : (env : Env) → (t ≡ state2)  → (varn env + vari env ≡ c10) → whileTestCondition c10 state2
+
+open whileTestCondition
+
+test2 : (c10 : ℕ) → whileTestCondition c10 state1 → whileTestCondition c10 state2 
+test2 c10 cond1 = whileTest 10 (λ env  → whileLoop env (λ env1 → proof3 env1 cond1 ))
+  where    
+    whileLoopCond : (e env1 : Env) → varn env1 + vari env1 ≡ c10 → varn e + vari e ≡ c10 → whileTestCondition c10 state2
+    whileLoopCond = {!!}
+    proof2 : (env : Env) → ((vari env) ≡ 0) /\ ((varn env) ≡ c10) -- PostCondition
+    proof2 env = record {pi1 = {!!} ; pi2 = {!!}}
+    proof3 : (env : Env) → whileTestCondition c10 state1 → whileTestCondition c10 state2
+    proof3 env cond1 = record {
+                          case1 = λ e ()
+                          ; case2 = λ e refl → conversion1 e {c10} (record { pi1 = {!!} ; pi2 = {!!} }) {!!}
+                          }