Why3 Proof Results for Project "ABF20"

Theory "ABF20.MapRelation": fully verified

Obligations	Alt-Ergo 2.4.0	CVC4 1.6	Z3 4.7.1	Z3 4.8.10
Deter	0.00	0.01	---	---
Total	0.01	0.03	0.08	0.03

Theory "ABF20.NumOfExt": fully verified

Obligations	Alt-Ergo 2.4.0	CVC4 1.6	Z3 4.7.1	Z3 4.8.10
Numof_no_add	0.14	Timeout (1s)	0.02	0.02

Theory "ABF20.Interval": fully verified

Obligations	Alt-Ergo 2.4.0	CVC4 1.6	Z3 4.7.1
VC for bint	0.00	---	---
VC for low_bint	0.00	---	---
TotalStrictOrder.Trans	0.00	---	---
TotalStrictOrder.Asymm	0.00	---	---
TotalStrictOrder.Trichotomy	0.00	---	---
VC for of_int	0.00	---	---
of_int_quasi_inj	---	0.02	0.02
of_intK	0.00	---	---
VC for numof_bint	0.00	---	---

Theory "ABF20.ModelTOOB": fully verified

Obligations	Alt-Ergo 2.4.0	CVC4 1.6	Z3 4.7.1
TOOB.Deter	0.01	---	---
TOOB.Total	---	0.02	0.04
TOOB.Injec	0.01	---	---
TOOB.Surjec	0.11	---	---

Theory "ABF20.Proposition2": fully verified

Obligations									Alt-Ergo 2.4.0	CVC4 1.6	Coq 8.12.2	Z3 4.7.1	Z3 4.8.10
ex_rel_permut									Timeout (5s)	0.07	0.52	Timeout (5s)	Timeout (5s)
inline_goal
	ex_rel_permut.0								---	---	---	---	---
	split_all_full
		ex_rel_permut.0.0							Timeout (30s)	0.09	---	---	Timeout (30s)
Proposition2									Timeout (5s)	0.08	---	Timeout (5s)	Timeout (5s)
inline_goal
	Proposition2.0								---	---	---	---	---
	split_all_full
		Proposition2.0.0							---	0.18	---	Timeout (1s)	---
		inline_goal
			Proposition2.0.0.0						---	0.05	---	Timeout (1s)	---
			inline_goal
				Proposition2.0.0.0.0					Timeout (5s)	0.06	---	Timeout (1s)	Timeout (5s)
				inline_goal
					Proposition2.0.0.0.0.0				Timeout (30s)	0.07	---	---	Timeout (30s)
destruct ex_rel_permut
	Proposition2.0								---	---	---	---	---
	exists rel_permut
		Proposition2.0.0							---	---	---	---	---
		split_goal_full
			Proposition2.0.0.0						---	---	---	---	---
			unfold bijective
				Proposition2.0.0.0.0					---	---	---	---	---
				split_goal_full
					Proposition2.0.0.0.0.0				0.00	---	---	---	---
					Proposition2.0.0.0.0.1				Timeout (1s)	0.08	---	Timeout (1s)	Timeout (1s)
					inline_goal
						Proposition2.0.0.0.0.1.0			Timeout (1s)	0.06	---	---	Timeout (1s)
						intros j
							Proposition2.0.0.0.0.1.0.0		Timeout (1s)	0.07	---	Timeout (1s)	Timeout (1s)
							cut (exists x:a. rel x (bint2a j))
								Proposition2.0.0.0.0.1.0.0.0	1.43	0.09	---	0.03	0.04
								asserted formula	Timeout (1s)	0.07	---	Timeout (1s)	Timeout (1s)
								apply Surjec2
			Proposition2.0.0.1						Timeout (5s)	0.09	---	Timeout (1s)	---
			inline_goal
				Proposition2.0.0.1.0					Timeout (5s)	---	---	---	---
				exists a2bint
					Proposition2.0.0.1.0.0				0.02	0.11	---	Timeout (1s)	---

Theory "ABF20.MapGraph": fully verified

Obligations	Alt-Ergo 2.4.0	CVC4 1.6
VC for arrow	0.00	---
Trans	0.01	---
Asymm	0.01	---
Trichotomy	---	0.03
Source_inj	---	0.02

Theory "ABF20.ModelTOTO": fully verified

Obligations	Alt-Ergo 2.4.0
TOTO.Trans	0.01
TOTO.Asymm	0.01
TOTO.Trichotomy	0.01
TOTO.V.Trans	0.01
TOTO.V.Asymm	0.01
TOTO.V.Trichotomy	0.01

Theory "ABF20.STOI": fully verified

Obligations	Alt-Ergo 2.4.0
Strict	0.00

Theory "ABF20.Gio20proposition5": fully verified

Obligations	Alt-Ergo 2.4.0
Trans	0.01
Asymm	0.01
Trichotomy	0.01

Theory "ABF20.ModelSTOI": fully verified

Obligations	Alt-Ergo 2.4.0
Trans	0.01
Asymm	0.01
Trichotomy	0.01

Theory "ABF20.Rank": not fully verified

Obligations									Alt-Ergo 2.4.0	CVC4 1.6	Coq 8.12.2	Z3 4.7.1	Z3 4.8.10
irrefl									0.01	---	---	---	---
VC for lt_int									0.01	---	---	---	---
numof_max									Timeout (1s)	Timeout (1s)	---	Timeout (1s)	Timeout (1s)
split_vc
	numof_max.0								Timeout (1s)	Timeout (1s)	---	Timeout (1s)	Timeout (1s)
intros lt,A,a
	numof_max.0								Timeout (1s)	Timeout (1s)	---	Timeout (1s)	Timeout (1s)
	rewrite Numof_no_add with (to_int a)
		numof_max.0.0							0.02	---	---	---	---
		rewrite premises							0.01	---	---	---	---
		rewrite premises							0.01	---	---	---	---
lt_map_bij_sto									0.02	---	---	---	---
VC for rank									0.06	0.04	---	0.03	---
rank_lt_inj									Timeout (1s)	Timeout (1s)	0.43	Timeout (1s)	Timeout (1s)
split_vc
	rank_lt_inj.0								Timeout (5s)	Timeout (5s)	---	---	Timeout (5s)
	inline_goal
		rank_lt_inj.0.0							---	---	---	---	---
		split_all_full
			rank_lt_inj.0.0.0						Timeout (1s)	Timeout (1s)	---	---	Timeout (1s)
			split_vc
				rank_lt_inj.0.0.0.0					Timeout (30s)	Timeout (30s)	---	---	Timeout (30s)
VC for max									0.03	0.07	---	---	---
max_is_max									0.14	Timeout (1s)	---	0.06	---
VC for succ									0.43	---	---	---	---
VC for min									0.04	0.07	---	---	---
VC for unrank									0.01	0.05	---	0.03	---
rank_ltK									Timeout (1s)	Timeout (1s)	---	Timeout (1s)	Timeout (1s)
split_vc
	rank_ltK.0								Timeout (5s)	Timeout (1s)	---	Timeout (1s)	---
unrank_ltK									0.01	Timeout (1s)	---	0.09	---
intros lt, H, i
	unrank_ltK.0								---	---	---	---	---
	assert (injective ((fun (y0:bint -> bint -> bool) (y1:bint) -> rank y0 y1) @ lt))
		asserted formula							---	---	---	---	---
		apply rank_lt_inj
			apply premises						---	---	---	---	---
			apply H
		unrank_ltK.0.1							---	---	---	---	---
		unfold injective in h
			unrank_ltK.0.1.0						---	---	---	---	---
			apply h
				apply premises					0.01	---	---	---	---
lt_mapK									Timeout (5s)	Timeout (1s)	---	0.09	0.21
Proposition1									Timeout (5s)	Timeout (1s)	---	Timeout (1s)	Timeout (5s)
split_vc
	Proposition1.0								---	Timeout (5s)	---	Timeout (5s)	---
	inline_goal
		Proposition1.0.0							---	---	---	---	---
		split_all_full
			Proposition1.0.0.0						---	Timeout (5s)	---	Timeout (5s)	---
			inline_goal
				Proposition1.0.0.0.0					Timeout (5s)	Timeout (5s)	---	Timeout (30s)	Timeout (5s)
				inline_goal
					Proposition1.0.0.0.0.0				Timeout (30s)	Timeout (30s)	---	---	Timeout (30s)
intros lt, T
	Proposition1.0								---	---	---	---	---
	exists (rank lt)
		Proposition1.0.0							Timeout (5s)	Timeout (1s)	---	Timeout (1s)	---
		split_goal_full
			Proposition1.0.0.0						---	---	---	---	---
			unfold bijective
				Proposition1.0.0.0.0					---	---	---	---	---
				split_goal_full
					Proposition1.0.0.0.0.0				0.01	---	---	---	---
					Proposition1.0.0.0.0.1				---	---	---	---	---
					unfold surjective
						Proposition1.0.0.0.0.1.0			---	---	---	---	---
						intros j
							Proposition1.0.0.0.0.1.0.0		---	---	---	---	---
							exists (unrank lt j)
								Proposition1.0.0.0.0.1.0.0.0	0.00	---	---	---	---
			Proposition1.0.0.1						0.01	---	---	---	---

Theory "ABF20.Tests": not fully verified

Obligations						Alt-Ergo 2.4.0	CVC4 1.6	Z3 4.7.1
VC for array_sto						0.04	---	---
VC for rank_cancel						0.02	0.10	0.04
VC for rank_cancel_array						0.01	---	---
VC for rank_cancel_test						Timeout (1s)	Timeout (1s)	Timeout (1s)
split_vc
	precondition					Timeout (1s)	Timeout (1s)	Timeout (1s)
	split_vc
		precondition				Timeout (5s)	Timeout (5s)	Timeout (5s)
		inline_goal
			precondition			---	---	---
			split_all_full
				precondition		Timeout (5s)	Timeout (30s)	Timeout (30s)
		precondition				Timeout (5s)	Timeout (5s)	Timeout (5s)
		inline_goal
			precondition			---	---	---
			split_all_full
				VC for rank_cancel_test		Timeout (5s)	Timeout (5s)	Timeout (5s)
				inline_goal
					VC for rank_cancel_test	Timeout (5s)	Timeout (30s)	Timeout (30s)
				VC for rank_cancel_test		Timeout (5s)	Timeout (5s)	Timeout (5s)
				inline_goal
					VC for rank_cancel_test	Timeout (5s)	Timeout (30s)	Timeout (30s)