diff --git a/wp.v b/wp.v
index adabce5..ec3360c 100644
--- a/wp.v
+++ b/wp.v
@@ -164,37 +164,60 @@ Definition assertImplLogical : Assert -> Assert -> Prop :=
 (***** Hoare provability *****************************************************)
 
 Parameter  hoare_provability : Assert -> Instr -> Assert -> Prop.
-Notation "[| pre  |] instr  [| post |]" := (hoare_provability pre instr post)
-        (at level 30): assert.
+Notation "|- [| pre  |] instr  [| post |]" :=
+        (hoare_provability pre instr post) (at level 30): assert.
 
-Axiom h_skip: forall (asser: Assert), ( [|asser|] skip [|asser|]) % assert.
+Axiom h_skip: forall (asser: Assert), ( |- [|asser|] skip [|asser|]) % assert.
 Axiom h_abort: forall (a1:Assert), forall (a2: Assert),
-    ([|a1|] abort [|a2|]) % assert.
+    (|- [|a1|] abort [|a2|]) % assert.
 Axiom h_assign: forall (asser: Assert), forall (x: Var), forall (e: Expr),
-    ([| asser [[ x <- expr e ]] |] (assign x e) [|asser|]) % assert.
+    (|- [| asser [[ x <- expr e ]] |] (assign x e) [|asser|]) % assert.
 Axiom h_conseq:
     forall (a1: Assert), forall (a1': Assert),
     forall (a2: Assert), forall (a2': Assert),
     forall (s: Instr),
-    ([| a1' |] s [| a2' |]) % assert ->
+    (|- [| a1' |] s [| a2' |]) % assert ->
             (assertImplLogical a1 a1') ->
             (assertImplLogical a2' a2) ->
-            ([| a1 |] s [| a2 |]) % assert.
+            (|- [| a1 |] s [| a2 |]) % assert.
 Axiom h_seq:
     forall (a1: Assert), forall (a2: Assert), forall (a3: Assert),
     forall (s1: Instr), forall (s2: Instr),
-    ([|a1|] s1 [|a2|]) % assert -> ([|a2|] s2 [|a3|]) % assert ->
-            ([|a1|] (seq s1 s2) [|a3|]) % assert.
+    (|- [|a1|] s1 [|a2|]) % assert -> (|- [|a2|] s2 [|a3|]) % assert ->
+            (|- [|a1|] (seq s1 s2) [|a3|]) % assert.
 Axiom h_if:
     forall (a1: Assert), forall (a2: Assert),
     forall (e: Expr),
     forall (s1: Instr), forall (s2: Instr),
-    ([| a1 /\ (assertOfExpr e) |] s1 [| a2 |]) % assert ->
-        ([| a1 /\ ~ (assertOfExpr e) |] s2 [| a2 |]) % assert ->
-        ([| a1 |] (ifelse e s1 s2) [| a2 |]) % assert.
+    (|- [| a1 /\ (assertOfExpr e) |] s1 [| a2 |]) % assert ->
+        (|- [| a1 /\ ~ (assertOfExpr e) |] s2 [| a2 |]) % assert ->
+        (|- [| a1 |] (ifelse e s1 s2) [| a2 |]) % assert.
 Axiom h_while:
     forall (inv: Assert),
     forall (e: Expr),
     forall (s: Instr),
-    ([| inv /\ (assertOfExpr e) |] s [| inv |]) % assert ->
-        ([| inv |] (while e s) [| inv /\ ~ (assertOfExpr e) |]) % assert.
+    (|- [| inv /\ (assertOfExpr e) |] s [| inv |]) % assert ->
+        (|- [| inv |] (while e s) [| inv /\ ~ (assertOfExpr e) |]) % assert.
+
+(***** Hoare: provability implies consequence ********************************)
+
+Definition conseq_or_bottom (y: Assert) (m: MemCpo) :=
+    match m with
+    | CpoError _ => True
+    | CpoElem _ m0 => y m0
+    end.
+
+Definition hoare_consequence (pre: Assert) (instr: Instr) (post: Assert) :=
+    forall mem: Mem,
+    (pre mem) -> (conseq_or_bottom post (interp instr (MemElem mem))).
+
+Notation "|= [| pre  |] instr  [| post |]" :=
+        (hoare_consequence pre instr post) (at level 30): assert.
+
+Theorem hoare_provability_implies_consequence :
+    forall (pre: Assert), forall (s: Instr), forall (post: Assert),
+    ( |- [| pre |] s [| post |] ) % assert
+            -> ( |= [| pre |] s [| post |] ) % assert.
+Proof.
+    (* TODO *)
+Admitted.