|
1
|
(* ---------------------------------------------------------- *)
|
|
2
|
(* --- Assertion (file clocks7/clocks7_7.c, line 178) --- *)
|
|
3
|
(* ---------------------------------------------------------- *)
|
|
4
|
|
|
5
|
goal toto_step_assert_17:
|
|
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
|
(0 < i) ->
|
|
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, 1) ->
|
|
17
|
P_trans_totoC(i, 1, 0) ->
|
|
18
|
P_trans_totoD(i, 1, 1) ->
|
|
19
|
P_trans_totoG(i, 1, 1) ->
|
|
20
|
(P_clock_b1(1, 1) -> P_trans_b1(1)) ->
|
|
21
|
(P_clock_c(1) -> P_trans_c(0, 1)) ->
|
|
22
|
(region(a.base) <= 0) ->
|
|
23
|
(P_clock_d -> P_trans_d(i, 1)) ->
|
|
24
|
(P_clock_toto_2(1) -> P_trans_toto_2(i, 0)) ->
|
|
25
|
P_trans_totoF(i, 1, 1, 1, 1) ->
|
|
26
|
(P_clock_z(1) -> P_trans_z(1, 1, 1, 1)) ->
|
|
27
|
P_trans_y(1, 1, 1, 1)
|
|
28
|
|