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

History | View | Annotate | Download (1.22 KB)

1 |
(* ---------------------------------------------------------- *) |
---|---|

2 |
(* --- Assertion (file clocks7/clocks7_7.c, line 189) --- *) |

3 |
(* ---------------------------------------------------------- *) |

4 | |

5 |
goal toto_step_assert_23: |

6 |
forall i : int. |

7 |
forall t_6,t_5,t_4,t_3,t_2,t_1,t : (addr,int) farray. |

8 |
forall a : addr. |

9 |
let x = t_6[a] : int in |

10 |
let m = t_2[a <- 1] in |

11 |
P_trans_totoA -> |

12 |
is_sint32(i) -> |

13 |
is_sint32(t_1[a]) -> |

14 |
is_sint32(t_3[a]) -> |

15 |
is_sint32(t_4[a]) -> |

16 |
is_sint32(t_5[a]) -> |

17 |
is_sint32(x) -> |

18 |
(region(a.base) <= 0) -> |

19 |
(((i <= 0) -> |

20 |
((t_6 = t[a <- 3]) and P_trans_totoB(i, 0) and |

21 |
(P_clock_b3(0) -> P_trans_b3(3)) and P_trans_totoH(i, 0, 3, 3) and |

22 |
(P_clock_d -> P_trans_d(i, 0)) and (P_clock_y -> P_trans_y(0, 3, 3, 3)))) and |

23 |
((0 < i) -> |

24 |
((t_5 = m) and (t_6 = m) and P_trans_totoB(i, 1) and |

25 |
P_trans_totoC(i, 1, 0) and P_trans_totoD(i, 1, 1) and |

26 |
P_trans_totoG(i, 1, 1) and (P_clock_b1(1, 1) -> P_trans_b1(1)) and |

27 |
(P_clock_c(1) -> P_trans_c(0, 1)) and (P_clock_d -> P_trans_d(i, 1)) and |

28 |
(P_clock_toto_2(1) -> P_trans_toto_2(i, 0)) and |

29 |
P_trans_totoF(i, 1, 1, 1, 1) and |

30 |
(P_clock_z(1) -> P_trans_z(1, 1, 1, 1)) and |

31 |
(P_clock_y -> P_trans_y(1, 1, 1, 1))))) -> |

32 |
P_trans_totoI(i, x) |

33 |