Why3 Proof Results for Project "dfs2"
Theory "dfs2.DfsWhitePathCompleteness": 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. precondition | 0.01 |
| 2. precondition | 0.01 |
| 3. postcondition | 0.01 |
| 4. postcondition | 0.01 |
| 5. postcondition | 0.02 |
| 6. postcondition | 0.12 |
| 7. precondition | 0.01 |
| 8. precondition | 0.01 |
| 9. assertion | 0.09 |
| 10. precondition | 0.01 |
| 11. precondition | 0.01 |
| 12. assertion | 0.16 |
| 13. postcondition | 0.01 |
| 14. postcondition | 0.09 |
| 15. postcondition | 0.09 |
| 16. postcondition | --- |
| split_goal_wp | |
| | 1. VC for dfs | 0.12 |
| 2. VC for dfs | 0.20 |
| 17. postcondition | 0.01 |
| 18. postcondition | 0.01 |
| 19. postcondition | 0.01 |
| 20. postcondition | 0.02 |