Why3 Proof Results for Project "dfs7"

Theory "dfs7.DfsWhitePathCompleteness": fully verified in 0.01 s

ObligationsAlt-Ergo (2.2.0)Coq (8.7.2)Eprover (1.9)
nbtw_path---------
induction_pr
  nbtw_path.10.01------
nbtw_path.2------0.13
2. VC for dfs---------
split_goal_wp
  1. postcondition0.01------
2. postcondition0.01------
3. postcondition0.01------
4. postcondition0.02------
5. variant decrease0.01------
6. precondition0.01------
7. precondition0.01------
8. postcondition0.01------
9. postcondition0.01------
10. postcondition0.02------
11. postcondition0.15------
12. variant decrease0.01------
13. precondition0.01------
14. precondition0.01------
15. assertion0.04------
16. variant decrease0.01------
17. precondition0.01------
18. precondition0.01------
19. assertion0.13------
20. postcondition0.01------
21. postcondition0.08------
22. postcondition0.08------
23. postcondition1.00------
path_wpath---------
split_goal_wp
  path_wpath.1---------
induction_pr
  path_wpath.1.10.01------
path_wpath.1.20.01------
path_wpath.2---------
induction_pr
  path_wpath.2.10.01------
path_wpath.2.20.01------
path_wpath.3---0.70---
path_wpath_empty0.01------
access_whitepath_empty---------
split_goal_wp
  access_whitepath_empty.10.01------
access_whitepath_empty.20.01------
6. VC for dfs_main---------
split_goal_wp
  1. precondition0.01------
2. precondition0.01------
3. postcondition0.01------