### Profile

Statistics
| Branch: | Tag: | Revision:

## lustrec / optim / wpdir / typed / Axiomatic.ergo @ 6a93d814

 1 ```(* ---------------------------------------------------------- *) ``` ```(* --- Global Definitions --- *) ``` ```(* ---------------------------------------------------------- *) ``` ```predicate P_trans_totoA() = true ``` ```predicate P_clock_d() = true ``` ```predicate P_trans_d ``` ``` (x:int, ``` ``` d:int) = ``` ``` ((0 = d) and (x <= 0)) or ((1 = d) and (0 < x)) ``` ```predicate P_trans_totoB ``` ``` (x:int, ``` ``` d:int) = ``` ``` P_trans_totoA and (P_clock_d -> P_trans_d(x, d)) ``` ```predicate P_clock_toto_2(d:int) = 1 = d ``` ```predicate P_trans_toto_2(x:int, toto_2_0:int) = (0 = x) <-> (0 <> toto_2_0) ``` ```predicate P_trans_totoC ``` ``` (x:int, ``` ``` d:int, ``` ``` toto_2_0:int) = ``` ``` P_trans_totoB(x, d) and ``` ``` (P_clock_toto_2(d) -> P_trans_toto_2(x, toto_2_0)) ``` ```predicate P_clock_c(d:int) = 1 = d ``` ```predicate P_trans_c ``` ``` (toto_2_0:int, ``` ``` c:int) = ``` ``` ((0 = c) and (0 <> toto_2_0)) or ((0 = toto_2_0) and (1 = c)) ``` ```predicate P_trans_totoD ``` ``` (x:int, ``` ``` d:int, ``` ``` c:int) = ``` ``` exists i : int. is_uint32(i) and P_trans_totoC(x, d, i) and ``` ``` (P_clock_c(d) -> P_trans_c(i, c)) ``` ```predicate P_clock_b2(d:int, c:int) = (0 = c) and P_clock_c(d) ``` ```predicate P_trans_b2(b2_0:int) = 2 = b2_0 ``` ```predicate P_trans_totoE ``` ``` (x:int, ``` ``` d:int, ``` ``` c:int, ``` ``` b2_0:int) = ``` ``` P_trans_totoD(x, d, c) and (P_clock_b2(d, c) -> P_trans_b2(b2_0)) ``` ```predicate P_clock_b1(d:int, c:int) = (1 = c) and P_clock_c(d) ``` ```predicate P_trans_b1(b1_0:int) = 1 = b1_0 ``` ```predicate P_trans_totoF ``` ``` (x:int, ``` ``` d:int, ``` ``` c:int, ``` ``` b2_0:int, ``` ``` b1_0:int) = ``` ``` P_trans_totoE(x, d, c, b2_0) and (P_clock_b1(d, c) -> P_trans_b1(b1_0)) ``` ```predicate P_clock_z(d:int) = P_clock_c(d) ``` ```predicate P_trans_z ``` ``` (c:int, ``` ``` b1_0:int, ``` ``` b2_0:int, ``` ``` z:int) = ``` ``` ((1 = c) -> (b1_0 = z)) and ((0 = c) -> (b2_0 = z)) ``` ```predicate P_trans_totoG ``` ``` (x:int, ``` ``` d:int, ``` ``` z:int) = ``` ``` exists i_2,i_1,i : int. is_sint32(i) and is_sint32(i_1) and ``` ``` is_uint32(i_2) and P_trans_totoF(x, d, i_2, i_1, i) and ``` ``` (P_clock_z(d) -> P_trans_z(i_2, i, i_1, z)) ``` ```predicate P_clock_b3(d:int) = 0 = d ``` ```predicate P_trans_b3(b3_0:int) = 3 = b3_0 ``` ```predicate P_trans_totoH ``` ``` (x:int, ``` ``` d:int, ``` ``` z:int, ``` ``` b3_0:int) = ``` ``` P_trans_totoG(x, d, z) and (P_clock_b3(d) -> P_trans_b3(b3_0)) ``` ```predicate P_clock_y() = P_clock_d ``` ```predicate P_trans_y ``` ``` (d:int, ``` ``` b3_0:int, ``` ``` z:int, ``` ``` y:int) = ``` ``` ((0 = d) -> (b3_0 = y)) and ((1 = d) -> (y = z)) ``` ```predicate P_trans_totoI ``` ``` (x:int, ``` ``` y:int) = ``` ``` exists i_2,i_1,i : int. is_sint32(i_1) and is_sint32(i_2) and ``` ``` is_uint32(i) and P_trans_totoH(x, i, i_2, i_1) and ``` ``` (P_clock_y -> P_trans_y(i, i_1, i_2, y)) ```