deep handlers examples are done

hipsleek · May 7, 2024 · f79a512 · f79a512
1 parent 380d817
commit f79a512
Showing 1 changed file with 4 additions and 1 deletion.
diff --git a/src/demo/4_Deep_Left_Toss.ml b/src/demo/4_Deep_Left_Toss.ml
@@ -17,7 +17,10 @@ let rec tossNtimeLeft n
   \/ ex w2 r2; req counter->w2; Norm (counter->w2+((2^(n+m)) -2) /\  res=r2/\r2=0/\acc=false, res)  *) 
 
 let tossHandlerTail counter n 
-(*@ ex w; req counter->w /\ n>=1; Norm (counter->w+((2^(n+1)) -2) ,1) @*)
+(*@ 
+ex w; req counter->w /\ n=1; Norm (counter->w+2 ,1)
+\/    
+ex w; req counter->w /\ n>=1; Norm (counter->w+((2^(n+1)) -2) ,1) @*)
 = match tossNtimeLeft n with 
 
   (* try-catch lemma defined here *)