Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / optim / wpdir / typed / toto_step_assert_22.ergo @ 6a93d814

History | View | Annotate | Download (614 Bytes)

1
(* ---------------------------------------------------------- *)
2
(* --- Assertion (file clocks7/clocks7_7.c, line 187)     --- *)
3
(* ---------------------------------------------------------- *)
4

    
5
goal toto_step_assert_22:
6
  forall i : int.
7
  forall t_2,t_1,t : (addr,int) farray.
8
  forall a : addr.
9
  P_trans_totoA ->
10
  P_clock_y ->
11
  (i <= 0) ->
12
  is_sint32(i) ->
13
  is_sint32(t[a]) ->
14
  is_sint32(t_1[a]) ->
15
  is_sint32(t_2[a]) ->
16
  P_trans_totoB(i, 0) ->
17
  (P_clock_b3(0) -> P_trans_b3(3)) ->
18
  (region(a.base) <= 0) ->
19
  P_trans_totoH(i, 0, 3, 3) ->
20
  (P_clock_d -> P_trans_d(i, 0)) ->
21
  P_trans_y(0, 3, 3, 3)
22