Why3 Proof Results for Project "dfs6"
Theory "dfs6.DfsWhitePathCopmleteness": fully verified in 0.00 s
Obligations | Alt-Ergo (2.1.0) |
nbtw_path | --- |
induction_pr | |
| nbtw_path.1 | 0.01 |
nbtw_path.2 | 0.01 |
2. VC for dfs | --- |
split_goal_wp | |
| 1. postcondition | 0.01 |
2. postcondition | 0.01 |
3. postcondition | 0.01 |
4. postcondition | 0.03 |
5. precondition | 0.01 |
6. precondition | 0.01 |
7. postcondition | 0.01 |
8. postcondition | 0.01 |
9. postcondition | 0.01 |
10. postcondition | 0.04 |
11. precondition | 0.01 |
12. precondition | 0.02 |
13. assertion | 0.09 |
14. precondition | 0.03 |
15. precondition | 0.01 |
16. assertion | 0.12 |
17. postcondition | 0.01 |
18. postcondition | 0.06 |
19. postcondition | 0.06 |
20. postcondition | 0.58 |