Why3 Proof Results for Project "dfs7"

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

Obligations			Alt-Ergo (2.2.0)	Coq (8.7.2)	Eprover (1.9)
nbtw_path			---	---	---
induction_pr
	nbtw_path.1		0.01	---	---
	nbtw_path.2		---	---	0.13
2. VC for dfs			---	---	---
split_goal_wp
	1. postcondition		0.01	---	---
	2. postcondition		0.01	---	---
	3. postcondition		0.01	---	---
	4. postcondition		0.02	---	---
	5. variant decrease		0.01	---	---
	6. precondition		0.01	---	---
	7. precondition		0.01	---	---
	8. postcondition		0.01	---	---
	9. postcondition		0.01	---	---
	10. postcondition		0.02	---	---
	11. postcondition		0.15	---	---
	12. variant decrease		0.01	---	---
	13. precondition		0.01	---	---
	14. precondition		0.01	---	---
	15. assertion		0.04	---	---
	16. variant decrease		0.01	---	---
	17. precondition		0.01	---	---
	18. precondition		0.01	---	---
	19. assertion		0.13	---	---
	20. postcondition		0.01	---	---
	21. postcondition		0.08	---	---
	22. postcondition		0.08	---	---
	23. postcondition		1.00	---	---
path_wpath			---	---	---
split_goal_wp
	path_wpath.1		---	---	---
	induction_pr
		path_wpath.1.1	0.01	---	---
		path_wpath.1.2	0.01	---	---
	path_wpath.2		---	---	---
	induction_pr
		path_wpath.2.1	0.01	---	---
		path_wpath.2.2	0.01	---	---
	path_wpath.3		---	0.70	---
path_wpath_empty			0.01	---	---
access_whitepath_empty			---	---	---
split_goal_wp
	access_whitepath_empty.1		0.01	---	---
	access_whitepath_empty.2		0.01	---	---
6. VC for dfs_main			---	---	---
split_goal_wp
	1. precondition		0.01	---	---
	2. precondition		0.01	---	---
	3. postcondition		0.01	---	---