--- a/whileTest.agda	Thu Dec 13 15:37:57 2018 +0900
+++ b/whileTest.agda	Thu Dec 13 17:45:50 2018 +0900
@@ -1,7 +1,11 @@
 module whileTest where
 
 open import Data.Nat
-open import Data.Bool
+open import Data.Bool hiding (_≟_)
+open import Data.Product
+open import Relation.Nullary
+open import Relation.Binary
+open import SET
 
 
 record Env : Set where
@@ -10,36 +14,91 @@
     vari : ℕ
 open Env
 
-data PrimComm  : Set where
-  command : (Env → Env) → PrimComm
---  seti : (v : ℕ) → PrimComm (record  {varn = {!!} ; vari = {!!}} )
+neg : (Env → Bool) → (Env → Bool)
+neg x e = not (x e)
+
+and : (Env → Bool) → (Env → Bool)  → (Env → Bool)
+and x y e = (x e) ∧ (y e)
+
+enveq : (Env → Bool) → (Env → Bool) → Set
+enveq x y = {!!}
+
+sem : (Env → Bool) → Pred Env
+sem x y = {!!}
+
+tautValid : (b1 b2 : Env → Bool) -> enveq b1 b2 ->
+                 (s : Env) -> sem b1 s -> sem b2 s
+tautValid = {!!}
+
+respNeg : (b : Env → Bool) -> (s : Env) ->
+               Iff (sem (neg b) s) (¬ sem b s)
+respNeg = {!!}               
+
+respAnd : (b1 b2 : Env → Bool) -> (s : Env) ->
+               Iff (sem (and b1 b2) s)
+                   ((sem b1 s) ×  (sem b2 s))
+respAnd = {!!}
 
-data Cond : Set where
-  cond : (Env → Bool) → Cond 
+PrimSemComm : ∀ {l} -> (Env → Env) -> Rel Env l
+PrimSemComm = {!!}
+
+Axiom :( Env → Bool) -> (Env → Env) -> (Env → Bool) -> Set
+Axiom = {!!}
+
+axiomValid : ∀ {l} -> (bPre : Env → Bool ) -> (pcm : (Env → Env)) -> (bPost : Env → Bool) ->
+                  (ax : Axiom bPre pcm bPost) -> (s1 s2 : Env) ->
+                  sem bPre s1 -> PrimSemComm {l} pcm s1 s2 -> sem bPost s2
+axiomValid = {!!}
+
+open import Hoare (Env → Bool) (Env → Env) neg and enveq Env sem  tautValid
+                  respNeg respAnd PrimSemComm Axiom axiomValid
 
-open import Hoare Cond PrimComm {!!} {!!} {!!} Env {!!} {!!} {!!} {!!} {!!} {!!} {!!}
+lt : ℕ → ℕ → Bool
+lt x y with x <? y
+lt x y | yes p = true
+lt x y | no ¬p = false
+
+_-_ : ℕ → ℕ → ℕ
+x - zero = x
+zero - (suc _) = zero
+(suc x) - (suc y) = x - y
+
+_==_ : ℕ → ℕ → Bool
+x == y with x ≟ y
+(x == y) | yes p = true
+(x == y) | no ¬p = false
+
 
 program : Comm
 program = 
-    Seq ( PComm (command (λ env → record env {varn = 10})))
-    (Seq ( PComm (command (λ env → record env {vari = 0})))
-    (While (cond (λ env → {!!} ))
-      (Seq (PComm (command (λ env → record env {vari = ((vari env) + 1)} )))
-        (PComm (command (λ env → record env {varn = ((varn env) + 1)} ))))))
+    Seq ( PComm (λ env → record env {varn = 10}))
+    (Seq ( PComm (λ env → record env {vari = 0}))
+    (While (λ env → lt 0 (varn env) )
+      (Seq (PComm (λ env → record env {vari = ((vari env) + 1)} ))
+        (PComm (λ env → record env {varn = ((varn env) - 1)} )))))
 
--- {#- TERMINATION -#}
-interpreter : Env → Comm → Env
-interpreter env Skip = env
-interpreter env Abort = env
-interpreter env (PComm (command x)) = x env
-interpreter env (Seq comm comm1) = interpreter (interpreter env comm) comm1
-interpreter env (If (cond x) then else) with x env
-... | true = interpreter env then
-... | false = interpreter env else
-interpreter env (While (cond x) comm) with x env
-... | true = interpreter (interpreter env comm) (While (cond x) comm)
+{-# TERMINATING #-}
+interpret : Env → Comm → Env
+interpret env Skip = env
+interpret env Abort = env
+interpret env (PComm  x) = x env
+interpret env (Seq comm comm1) = interpret (interpret env comm) comm1
+interpret env (If x then else) with x env
+... | true = interpret env then
+... | false = interpret env else
+interpret env (While x comm) with x env
+... | true = interpret (interpret env comm) (While x comm)
 ... | false = env
 
+test1 = interpret (record {vari = 0 ; varn = 0}) program
 
-proof1 : HTProof {!!} program {!!}
+initCond : Env → Bool
+initCond _ = true
+
+termCond : Env → Bool
+termCond env = (vari env) == 10
+
+
+proof1 : HTProof initCond program termCond
 proof1 = {!!}
+