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 |