|
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
|
|