Library scc_SCCTarjan72_WP_parameter_dfs1_2

Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Require int.MinMax.
Require list.List.
Require list.Length.
Require list.Mem.
Require map.Map.
Require map.Const.
Require list.Append.
Require list.Reverse.
Require list.NumOcc.

Definition unit := unit.

Axiom set : forall (a:Type), Type.
Parameter set_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (set a).
Existing Instance set_WhyType.

Parameter mem: forall {a:Type} {a_WT:WhyType a}, a -> (set a) -> Prop.

Definition infix_eqeq {a:Type} {a_WT:WhyType a} (s1:(set a)) (s2:(set
a)): Prop := forall (x:a), (mem x s1) <-> (mem x s2).

Axiom extensionality : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
(s2:(set a)), (infix_eqeq s1 s2) -> (s1 = s2).

Definition subset {a:Type} {a_WT:WhyType a} (s1:(set a)) (s2:(set
a)): Prop := forall (x:a), (mem x s1) -> (mem x s2).

Axiom subset_refl : forall {a:Type} {a_WT:WhyType a}, forall (s:(set a)),
(subset s s).

Axiom subset_trans : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
(s2:(set a)) (s3:(set a)), (subset s1 s2) -> ((subset s2 s3) -> (subset s1
s3)).

Parameter empty: forall {a:Type} {a_WT:WhyType a}, (set a).

Definition is_empty {a:Type} {a_WT:WhyType a} (s:(set a)): Prop :=
forall (x:a), ~ (mem x s).

Axiom empty_def1 : forall {a:Type} {a_WT:WhyType a}, (is_empty (empty : (set
a))).

Axiom mem_empty : forall {a:Type} {a_WT:WhyType a}, forall (x:a), ~ (mem x
(empty : (set a))).

Parameter add: forall {a:Type} {a_WT:WhyType a}, a -> (set a) -> (set a).

Axiom add_def1 : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (y:a),
forall (s:(set a)), (mem x (add y s)) <-> ((x = y) \/ (mem x s)).

Parameter remove: forall {a:Type} {a_WT:WhyType a}, a -> (set a) -> (set a).

Axiom remove_def1 : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (y:a)
(s:(set a)), (mem x (remove y s)) <-> ((~ (x = y)) /\ (mem x s)).

Axiom add_remove : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (s:(set
a)), (mem x s) -> ((add x (remove x s)) = s).

Axiom remove_add : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (s:(set
a)), ((remove x (add x s)) = (remove x s)).

Axiom subset_remove : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (s:(set
a)), (subset (remove x s) s).

Parameter union: forall {a:Type} {a_WT:WhyType a}, (set a) -> (set a) -> (set
a).

Axiom union_def1 : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
(s2:(set a)) (x:a), (mem x (union s1 s2)) <-> ((mem x s1) \/ (mem x s2)).

Parameter inter: forall {a:Type} {a_WT:WhyType a}, (set a) -> (set a) -> (set
a).

Axiom inter_def1 : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
(s2:(set a)) (x:a), (mem x (inter s1 s2)) <-> ((mem x s1) /\ (mem x s2)).

Parameter diff: forall {a:Type} {a_WT:WhyType a}, (set a) -> (set a) -> (set
a).

Axiom diff_def1 : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
(s2:(set a)) (x:a), (mem x (diff s1 s2)) <-> ((mem x s1) /\ ~ (mem x s2)).

Axiom subset_diff : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
(s2:(set a)), (subset (diff s1 s2) s1).

Parameter choose: forall {a:Type} {a_WT:WhyType a}, (set a) -> a.

Axiom choose_def : forall {a:Type} {a_WT:WhyType a}, forall (s:(set a)),
(~ (is_empty s)) -> (mem (choose s) s).

Parameter cardinal: forall {a:Type} {a_WT:WhyType a}, (set a) -> Z.

Axiom cardinal_nonneg : forall {a:Type} {a_WT:WhyType a}, forall (s:(set a)),
(0%Z <= (cardinal s))%Z.

Axiom cardinal_empty : forall {a:Type} {a_WT:WhyType a}, forall (s:(set a)),
((cardinal s) = 0%Z) <-> (is_empty s).

Axiom cardinal_add : forall {a:Type} {a_WT:WhyType a}, forall (x:a),
forall (s:(set a)), (~ (mem x s)) -> ((cardinal (add x
s)) = (1%Z + (cardinal s))%Z).

Axiom cardinal_remove : forall {a:Type} {a_WT:WhyType a}, forall (x:a),
forall (s:(set a)), (mem x s) -> ((cardinal s) = (1%Z + (cardinal (remove x
s)))%Z).

Axiom cardinal_subset : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
(s2:(set a)), (subset s1 s2) -> ((cardinal s1) <= (cardinal s2))%Z.

Axiom subset_eq : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
(s2:(set a)), (subset s1 s2) -> (((cardinal s1) = (cardinal s2)) ->
(infix_eqeq s1 s2)).

Axiom cardinal1 : forall {a:Type} {a_WT:WhyType a}, forall (s:(set a)),
((cardinal s) = 1%Z) -> forall (x:a), (mem x s) -> (x = (choose s)).

Parameter elements: forall {a:Type} {a_WT:WhyType a}, (list a) -> (set a).

Axiom elements_mem : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a))
(x:a), (list.Mem.mem x l) <-> (mem x (elements l)).

Axiom elements_Nil : forall {a:Type} {a_WT:WhyType a},
((elements Init.Datatypes.nil) = (empty : (set a))).

Definition vertex := Z.

Parameter vertices: (set Z).

Parameter successors: Z -> (set Z).

Axiom successors_vertices : forall (x:Z), (mem x vertices) -> (subset
(successors x) vertices).

Definition edge (x:Z) (y:Z): Prop := (mem x vertices) /\ (mem y
(successors x)).

Inductive path: Z -> (list Z) -> Z -> Prop :=
| Path_empty : forall (x:Z), (path x Init.Datatypes.nil x)
| Path_cons : forall (x:Z) (y:Z) (z:Z) (l:(list Z)), (edge x y) -> ((path y
l z) -> (path x (Init.Datatypes.cons x l) z)).

Axiom path_right_extension : forall (x:Z) (y:Z) (z:Z) (l:(list Z)), (path x l
y) -> ((edge y z) -> (path x
(Init.Datatypes.app l (Init.Datatypes.cons y Init.Datatypes.nil)) z)).

Axiom path_right_inversion : forall (x:Z) (z:Z) (l:(list Z)), (path x l z) ->
(((x = z) /\ (l = Init.Datatypes.nil)) \/ exists y:Z, exists l':(list Z),
(path x l' y) /\ ((edge y z) /\
(l = (Init.Datatypes.app l' (Init.Datatypes.cons y Init.Datatypes.nil))))).

Axiom path_trans : forall (x:Z) (y:Z) (z:Z) (l1:(list Z)) (l2:(list Z)),
(path x l1 y) -> ((path y l2 z) -> (path x (Init.Datatypes.app l1 l2) z)).

Axiom empty_path : forall (x:Z) (y:Z), (path x Init.Datatypes.nil y) ->
(x = y).

Axiom path_decomposition : forall (x:Z) (y:Z) (z:Z) (l1:(list Z))
(l2:(list Z)), (path x (Init.Datatypes.app l1 (Init.Datatypes.cons y l2))
z) -> ((path x l1 y) /\ (path y (Init.Datatypes.cons y l2) z)).

Inductive array (a:Type) :=
| mk_array : Z -> (map.Map.map Z a) -> array a.
Axiom array_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (array a).
Existing Instance array_WhyType.
Implicit Arguments mk_array [[a]].

Definition elts {a:Type} {a_WT:WhyType a} (v:(array a)): (map.Map.map Z a) :=
match v with
| (mk_array x x1) => x1
end.

Definition length {a:Type} {a_WT:WhyType a} (v:(array a)): Z :=
match v with
| (mk_array x x1) => x
end.

Definition get {a:Type} {a_WT:WhyType a} (a1:(array a)) (i:Z): a :=
(map.Map.get (elts a1) i).

Definition set1 {a:Type} {a_WT:WhyType a} (a1:(array a)) (i:Z) (v:a): (array
a) := (mk_array (length a1) (map.Map.set (elts a1) i v)).

Axiom vertices_def : forall (x:Z), (mem x vertices) <-> ((0%Z <= x)%Z /\
(x < (cardinal vertices))%Z).

Axiom lmem_dec : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (l:(list a)),
(list.Mem.mem x l) \/ ~ (list.Mem.mem x l).

Axiom list_simpl_r : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
(l2:(list a)) (l:(list a)),
((Init.Datatypes.app l1 l) = (Init.Datatypes.app l2 l)) -> (l1 = l2).

Axiom list_assoc_cons : forall {a:Type} {a_WT:WhyType a},
forall (l1:(list a)) (l2:(list a)) (x:a),
((Init.Datatypes.app l1 (Init.Datatypes.cons x l2)) = (Init.Datatypes.app (Init.Datatypes.app l1 (Init.Datatypes.cons x Init.Datatypes.nil)) l2)).

Definition is_last {a:Type} {a_WT:WhyType a} (x:a) (s:(list a)): Prop :=
exists s':(list a),
(s = (Init.Datatypes.app s' (Init.Datatypes.cons x Init.Datatypes.nil))).

Parameter rank: forall {a:Type} {a_WT:WhyType a}, a -> (list a) -> Z.

Axiom rank_def : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (s:(list a)),
match s with
| Init.Datatypes.nil => ((rank x s) = (cardinal vertices))
| (Init.Datatypes.cons y s') => (((x = y) /\ ~ (list.Mem.mem x s')) ->
((rank x s) = (list.Length.length s'))) /\ ((~ ((x = y) /\
~ (list.Mem.mem x s'))) -> ((rank x s) = (rank x s')))
end.

Axiom rank_not_mem : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
(s:(list a)), (~ (list.Mem.mem x s)) -> ((rank x s) = (cardinal vertices)).

Axiom rank_range : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
(s:(list a)), (list.Mem.mem x s) -> ((0%Z <= (rank x s))%Z /\ ((rank x
s) < (list.Length.length s))%Z).

Axiom rank_min : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (y:a)
(s:(list a)), (is_last x s) -> ((list.Mem.mem y s) -> ((rank x
s) <= (rank y s))%Z).

Axiom rank_app_l : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
(s:(list a)) (s':(list a)), (list.Mem.mem x s') -> ((~ (list.Mem.mem x
s)) -> ((rank x (Init.Datatypes.app s' s)) = ((rank x
s') + (list.Length.length s))%Z)).

Axiom rank_app_r : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
(s:(list a)) (s':(list a)), (list.Mem.mem x s) -> ((rank x s) = (rank x
(Init.Datatypes.app s' s))).

Definition simplelist {a:Type} {a_WT:WhyType a} (l:(list a)): Prop :=
forall (x:a), ((list.NumOcc.num_occ x l) <= 1%Z)%Z.

Axiom simplelist_tl : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
(l:(list a)), (simplelist (Init.Datatypes.cons x l)) -> ((simplelist l) /\
~ (list.Mem.mem x l)).

Axiom simplelist_split : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
(l1:(list a)) (l2:(list a)) (l3:(list a)) (l4:(list a)),
((Init.Datatypes.app l1 (Init.Datatypes.cons x l2)) = (Init.Datatypes.app l3 (Init.Datatypes.cons x l4))) ->
((simplelist (Init.Datatypes.app l1 (Init.Datatypes.cons x l2))) ->
((l1 = l3) /\ (l2 = l4))).

Axiom simplelist_hd_max_rank : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
(y:a) (s1:(list a)) (s2:(list a)), (s1 = (Init.Datatypes.cons x s2)) ->
((simplelist s1) -> ((list.Mem.mem y s2) -> ((rank y s1) < (rank x
s1))%Z)).

Axiom rank_before_suffix : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
(y:a) (s1:(list a)) (s2:(list a)), (simplelist
(Init.Datatypes.app s1 s2)) -> ((is_last x s1) -> ((list.Mem.mem y s2) ->
((rank y (Init.Datatypes.app s1 s2)) < (rank x
(Init.Datatypes.app s1 s2)))%Z)).

Axiom inter_com : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
(s2:(set a)), (infix_eqeq (inter s1 s2) (inter s2 s1)).

Axiom inter_add : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
(s2:(set a)) (x:a), (~ (mem x s2)) -> (infix_eqeq (inter (add x s1) s2)
(inter s1 s2)).

Axiom set_elt : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (s1:(set a))
(s2:(set a)) (s3:(set a)), (~ (mem x s3)) -> (infix_eqeq (union (add x s1)
(diff s2 s3)) (union s1 (diff (add x s2) s3))).

Axiom set_mem : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (s1:(set a))
(s2:(set a)) (s3:(set a)) (s4:(set a)), (infix_eqeq s1 (union s2 (diff s3
s4))) -> ((infix_eqeq (inter s2 s4) (empty : (set a))) -> ((mem x s1) ->
~ (mem x s4))).

Axiom inter_subset_inter : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set
a)) (s2:(set a)) (s2':(set a)), ((inter s1 s2) = (empty : (set a))) ->
((subset s2' s2) -> ((inter s1 s2') = (empty : (set a)))).

Axiom subset_add : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (s:(set a))
(s':(set a)), (subset s' (add x s)) -> ((mem x s') \/ (subset s' s)).

Axiom union_add_l : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (s:(set
a)) (s':(set a)), (infix_eqeq (union (add x s) s') (add x (union s s'))).

Axiom union_add_r : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (s:(set
a)) (s':(set a)), (infix_eqeq (union s (add x s')) (add x (union s s'))).

Axiom elts_cons : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
(l:(list a)), (infix_eqeq (elements (Init.Datatypes.cons x l)) (add x
(elements l))).

Axiom elts_app : forall {a:Type} {a_WT:WhyType a}, forall (s:(list a))
(s':(list a)), (infix_eqeq (elements (Init.Datatypes.app s s'))
(union (elements s) (elements s'))).

Axiom simplelist_app_inter : forall {a:Type} {a_WT:WhyType a},
forall (l1:(list a)) (l2:(list a)), (simplelist
(Init.Datatypes.app l1 l2)) -> ((inter (elements l1)
(elements l2)) = (empty : (set a))).

Axiom simplelist_length : forall {a:Type} {a_WT:WhyType a},
forall (s:(list a)), (simplelist s) ->
((list.Length.length s) = (cardinal (elements s))).

Parameter set_of: forall {a:Type} {a_WT:WhyType a}, (set (set a)) -> (set a).

Axiom set_of_empty : forall {a:Type} {a_WT:WhyType a}, ((set_of (empty : (set
(set a)))) = (empty : (set a))).

Axiom set_of_add : forall {a:Type} {a_WT:WhyType a}, forall (s:(set a))
(sx:(set (set a))), (infix_eqeq (set_of (add s sx)) (union s (set_of sx))).

Definition one_in_set_of {a:Type} {a_WT:WhyType a} (sccs:(set (set
a))): Prop := forall (x:a), (mem x (set_of sccs)) -> exists cc:(set a),
(mem cc sccs) /\ (mem x cc).

Axiom Induction : (forall (s:(set (set Z))), (is_empty s) -> (one_in_set_of
s)) -> ((forall (s:(set (set Z))), (one_in_set_of s) -> forall (t:(set Z)),
(~ (mem t s)) -> (one_in_set_of (add t s))) -> forall (s:(set (set Z))),
(one_in_set_of s)).

Axiom set_of_elt : forall (sccs:(set (set Z))), (one_in_set_of sccs).

Axiom elt_set_of : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (cc:(set
a)) (sccs:(set (set a))), (mem x cc) -> ((mem cc sccs) -> (mem x
(set_of sccs))).

Axiom subset_set_of : forall (s:(set (set Z))) (s':(set (set Z))), (subset s
s') -> (subset (set_of s) (set_of s')).

Definition reachable (x:Z) (y:Z): Prop := exists l:(list Z), (path x l y).

Axiom reachable_trans : forall (x:Z) (y:Z) (z:Z), (reachable x y) ->
((reachable y z) -> (reachable x z)).

Axiom xset_path_xedge : forall (x:Z) (y:Z) (l:(list Z)) (s:(set Z)), (mem x
s) -> ((~ (mem y s)) -> ((path x l y) -> exists x':Z, exists y':Z, (mem x'
s) /\ ((~ (mem y' s)) /\ ((edge x' y') /\ ((reachable x x') /\ (reachable
y' y)))))).

Definition in_same_scc (x:Z) (y:Z): Prop := (reachable x y) /\ (reachable y
x).

Definition is_subscc (s:(set Z)): Prop := forall (x:Z) (y:Z), (mem x s) ->
((mem y s) -> (in_same_scc x y)).

Definition is_scc (s:(set Z)): Prop := (~ (is_empty s)) /\ ((is_subscc s) /\
forall (s':(set Z)), (subset s s') -> ((is_subscc s') -> (infix_eqeq s
s'))).

Axiom same_scc_refl : forall (x:Z), (in_same_scc x x).

Axiom same_scc_sym : forall (x:Z) (z:Z), (in_same_scc x z) -> (in_same_scc z
x).

Axiom same_scc_trans : forall (x:Z) (y:Z) (z:Z), (in_same_scc x y) ->
((in_same_scc y z) -> (in_same_scc x z)).

Axiom subscc_add : forall (x:Z) (y:Z) (cc:(set Z)), (is_subscc cc) -> ((mem x
cc) -> ((in_same_scc x y) -> (is_subscc (add y cc)))).

Axiom scc_max : forall (x:Z) (y:Z) (cc:(set Z)), (is_scc cc) -> ((mem x
cc) -> ((in_same_scc x y) -> (mem y cc))).

Inductive env :=
| mk_env : (set Z) -> (list Z) -> (set (set Z)) -> Z -> (array Z) -> env.
Axiom env_WhyType : WhyType env.
Existing Instance env_WhyType.

Definition num (v:env): (array Z) :=
match v with
| (mk_env x x1 x2 x3 x4) => x4
end.

Definition sn (v:env): Z := match v with
| (mk_env x x1 x2 x3 x4) => x3
end.

Definition sccs (v:env): (set (set Z)) :=
match v with
| (mk_env x x1 x2 x3 x4) => x2
end.

Definition stack (v:env): (list Z) :=
match v with
| (mk_env x x1 x2 x3 x4) => x1
end.

Definition blacks (v:env): (set Z) :=
match v with
| (mk_env x x1 x2 x3 x4) => x
end.

Definition wf_color (e:env) (grays:(set Z)): Prop :=
match e with
| (mk_env b s ccs _ _) => (subset (union grays b) vertices) /\ ((infix_eqeq
(inter b grays) (empty : (set Z))) /\ ((infix_eqeq (elements s)
(union grays (diff b (set_of ccs)))) /\ (subset (set_of ccs) b)))
end.

Definition wf_num (e:env) (grays:(set Z)): Prop :=
match e with
| (mk_env b s ccs n f) => (forall (x:Z), ((0%Z <= x)%Z /\
(x < (length f))%Z) -> ((((-1%Z)%Z <= (get f x))%Z /\ (((get f
x) < n)%Z /\ (n <= (cardinal vertices))%Z)) \/ ((get f
x) = (cardinal vertices)))) /\ ((n = (cardinal (union grays b))) /\
((forall (x:Z), ((0%Z <= x)%Z /\ (x < (length f))%Z) -> (((get f
x) = (cardinal vertices)) <-> (mem x (set_of ccs)))) /\ ((forall (x:Z),
((0%Z <= x)%Z /\ (x < (length f))%Z) -> (((get f x) = (-1%Z)%Z) <->
~ (mem x (union grays b)))) /\ ((forall (x:Z) (y:Z), (list.Mem.mem x
s) -> ((list.Mem.mem y s) -> (((get f x) < (get f y))%Z <-> ((rank x
s) < (rank y s))%Z))) /\ ((length f) = (cardinal vertices))))))
end.

Definition no_black_to_white (blacks1:(set Z)) (grays:(set Z)): Prop :=
forall (x:Z) (x':Z), (edge x x') -> ((mem x blacks1) -> (mem x'
(union blacks1 grays))).

Definition wf_env (e:env) (grays:(set Z)): Prop := let s := (stack e) in
((wf_color e grays) /\ ((wf_num e grays) /\ ((no_black_to_white (blacks e)
grays) /\ ((simplelist s) /\ ((forall (x:Z) (y:Z), (mem x grays) ->
((list.Mem.mem y s) -> (((rank x s) <= (rank y s))%Z -> (reachable x
y)))) /\ forall (y:Z), (list.Mem.mem y s) -> exists x:Z, (mem x grays) /\
(((rank x s) <= (rank y s))%Z /\ (reachable y x))))))).

Definition access_from (x:Z) (s:(set Z)): Prop := forall (y:Z), (mem y s) ->
(reachable x y).

Definition access_to (s:(set Z)) (y:Z): Prop := forall (x:Z), (mem x s) ->
(reachable x y).

Definition num_of_reachable (n:Z) (x:Z) (e:env): Prop := exists y:Z,
(list.Mem.mem y (stack e)) /\ ((n = (get (num e) y)) /\ (reachable x y)).

Definition xedge_to (s1:(list Z)) (s3:(list Z)) (y:Z): Prop :=
(exists s2:(list Z), (s1 = (Init.Datatypes.app s2 s3)) /\ exists x:Z,
(list.Mem.mem x s2) /\ (edge x y)) /\ (list.Mem.mem y s3).

Definition subenv (e:env) (e':env): Prop := (exists s:(list Z),
((stack e') = (Init.Datatypes.app s (stack e))) /\ (subset (elements s)
(blacks e'))) /\ ((subset (blacks e) (blacks e')) /\ ((subset (sccs e)
(sccs e')) /\ forall (x:Z), (list.Mem.mem x (stack e)) -> ((get (num e)
x) = (get (num e') x)))).

Axiom subscc_after_last_gray : forall (x:Z) (e:env) (g:(set Z)) (s2:(list Z))
(s3:(list Z)), (wf_env e (add x g)) ->
match e with
| (mk_env b s _ _ _) => (s = (Init.Datatypes.app s2 s3)) -> ((is_last x
s2) -> ((subset (elements s2) (add x b)) -> (is_subscc (elements s2))))
end.

Axiom wf_color_postcond_split : forall (s2:(set Z)) (s3:(set Z)) (g:(set Z))
(b:(set Z)) (sccs1:(set Z)), (infix_eqeq (union s2 s3) (union g (diff b
sccs1))) -> ((infix_eqeq (inter s2 s3) (empty : (set Z))) -> ((infix_eqeq
(inter g s2) (empty : (set Z))) -> (infix_eqeq s3 (union g (diff b
(union s2 sccs1)))))).

Axiom wf_color_sccs : forall (e:env) (g:(set Z)), (wf_color e g) ->
(infix_eqeq (set_of (sccs e)) (diff (union (blacks e) g)
(elements (stack e)))).

Axiom wf_color_3_cases : forall (x:Z) (e:env) (g:(set Z)), (wf_color e g) ->
((mem x (set_of (sccs e))) \/ ((mem x (elements (stack e))) \/ ~ (mem x
(union (blacks e) g)))).

Require Import mathcomp.ssreflect.ssreflect.
Ltac compress :=
repeat (match goal with [H1: ?A, H2: ?A |- _] => clear H2 end).

Theorem WP_parameter_dfs1 : forall (x:Z) (e:(set Z)) (e1:(list Z)) (e2:(set
(set Z))) (e3:Z) (e4:Z) (e5:(map.Map.map Z Z)) (grays:(set Z)), let e6 :=
(mk_env e e1 e2 e3 (mk_array e4 e5)) in ((((0%Z < e4)%Z \/ (0%Z = e4)) /\
((mem x vertices) /\ ((forall (x1:Z), (mem x1 grays) -> (reachable x1
x)) /\ ((~ (mem x (union e grays))) /\ ((let s := (stack e6) in ((wf_color
e6 grays) /\ ((wf_num e6 grays) /\ ((no_black_to_white (blacks e6)
grays) /\ ((simplelist s) /\ ((forall (x1:Z) (y:Z), (mem x1 grays) ->
((list.Mem.mem y s) -> (((rank x1 s) <= (rank y s))%Z -> (reachable x1
y)))) /\ forall (y:Z), (list.Mem.mem y s) -> exists x1:Z, (mem x1 grays) /\
(((rank x1 s) <= (rank y s))%Z /\ (reachable y x1)))))))) /\
forall (cc:(set Z)), (mem cc e2) <-> ((forall (x1:Z), (mem x1 cc) -> (mem
x1 e)) /\ ((~ (is_empty cc)) /\ ((is_subscc cc) /\ forall (s':(set Z)),
(subset cc s') -> ((is_subscc s') -> (infix_eqeq cc s')))))))))) ->
((forall (z:Z), (list.Mem.mem z e1) -> (((-1%Z)%Z < (map.Map.get e5
z))%Z /\ ((map.Map.get e5 z) < e3)%Z)) -> forall (rho:(list Z)),
(rho = (Init.Datatypes.cons x e1)) -> forall (rho1:Z),
(rho1 = (e3 + 1%Z)%Z) -> ((((0%Z < x)%Z \/ (0%Z = x)) /\ (x < e4)%Z) ->
forall (o:(map.Map.map Z Z)), (((0%Z < e4)%Z \/ (0%Z = e4)) /\
(o = (map.Map.set e5 x e3))) -> (((0%Z < e4)%Z \/ (0%Z = e4)) -> let s :=
(stack (mk_env e rho e2 rho1 (mk_array e4 o))) in forall (y:Z),
(list.Mem.mem y s) -> exists x1:Z, (mem x1 (add x grays)) /\ (((rank x1
s) <= (rank y s))%Z /\ (reachable y x1)))))).
move=> x blacks stack sccs sn n num grays e6 [h1 [h2 [h3 [h4 [[hwf_color [hwf_num [hnbtw [hsimpl [hreach1 hreach2]]]]] h6]]]]] h7 s1 s1_is_xstack sn1 sn_incr hrangex num1 [_ num1_def] h14 s y hmemy.
compress.
unfold s in hmemy; simpl in hmemy.
rewrite s1_is_xstack in hmemy.
move: {+} hmemy => [hc1 | hc2].
- rewrite hc1.
exists x.
repeat split.
+ reflexivity.
+ exists nil.
by apply Path_empty.
- move: {+} hc2 => y_in_stack.
apply hreach2 in hc2 as [z [hzg [hrankz hreachable]]].
exists z.
repeat split.