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)).

Fixpoint elements {a:Type} {a_WT:WhyType a} (l:(list a)) {struct l}: (set
  a) :=
  match l with
  | Init.Datatypes.nil => (empty : (set a))
  | (Init.Datatypes.cons x r) => (add x (elements r))
  end.

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

Axiom vertex : Type.
Parameter vertex_WhyType : WhyType vertex.
Existing Instance vertex_WhyType.

Parameter vertices: (set vertex).

Parameter successors: vertex -> (set vertex).

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

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

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

Axiom path_right_extension : forall (x:vertex) (y:vertex) (z:vertex)
  (l:(list vertex)), (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:vertex) (z:vertex) (l:(list vertex)),
  (path x l z) -> (((x = z) /\ (l = Init.Datatypes.nil)) \/ exists y:vertex,
  exists l':(list vertex), (path x l' y) /\ ((edge y z) /\
  (l = (Init.Datatypes.app l' (Init.Datatypes.cons y Init.Datatypes.nil))))).

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

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

Axiom path_decomposition : forall (x:vertex) (y:vertex) (z:vertex)
  (l1:(list vertex)) (l2:(list vertex)), (path x
  (Init.Datatypes.app l1 (Init.Datatypes.cons y l2)) z) -> ((path x l1 y) /\
  (path y (Init.Datatypes.cons y l2) 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 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_l : 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) (add x
  (inter s1 s2))).

Axiom inter_not_add_l : 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 diff_add_l : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (s1:(set
  a)) (s2:(set a)), (~ (mem x s2)) -> (infix_eqeq (diff (add x s1) s2) (add x
  (diff s1 s2))).

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

Axiom subset_add_r : 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 union_com : forall {a:Type} {a_WT:WhyType a}, forall (s:(set a))
  (s':(set a)), (infix_eqeq (union s s') (union s' s)).

Axiom union_var_l : forall {a:Type} {a_WT:WhyType a}, forall (s:(set a))
  (s':(set a)) (t:(set a)), (subset s s') -> (subset (union s t) (union s'
  t)).

Axiom union_var_r : forall {a:Type} {a_WT:WhyType a}, forall (s:(set a))
  (t:(set a)) (t':(set a)), (subset t t') -> (subset (union s t) (union s
  t')).

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 x cc) /\ (mem cc sccs).

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

Axiom set_of_elt : forall (sccs:(set (set vertex))), (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 vertex))) (s':(set (set vertex))),
  (subset s s') -> (subset (set_of s) (set_of 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 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 snoc_app : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
  (l2:(list a)) (x:a),
  ((Init.Datatypes.app (Init.Datatypes.app l1 (Init.Datatypes.cons x Init.Datatypes.nil)) l2) = (Init.Datatypes.app l1 (Init.Datatypes.cons x 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))).

Definition precedes {a:Type} {a_WT:WhyType a} (x:a) (y:a)
  (s:(list a)): Prop := exists s1:(list a), exists s2:(list a),
  (s = (Init.Datatypes.app s1 (Init.Datatypes.cons x s2))) /\ (list.Mem.mem y
  (Init.Datatypes.cons x s2)).

Axiom precedes_mem : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (y:a)
  (s:(list a)), (precedes x y s) -> ((list.Mem.mem x s) /\ (list.Mem.mem y
  s)).

Axiom head_precedes : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (y:a)
  (s:(list a)), (list.Mem.mem y (Init.Datatypes.cons x s)) -> (precedes x y
  (Init.Datatypes.cons x s)).

Axiom precedes_tail : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (y:a)
  (z:a) (s:(list a)), (~ (x = z)) -> ((precedes x y
  (Init.Datatypes.cons z s)) <-> (precedes x y s)).

Axiom tail_not_precedes : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
  (y:a) (s:(list a)), (precedes y x (Init.Datatypes.cons x s)) ->
  ((~ (list.Mem.mem x s)) -> (y = x)).

Axiom split_list_precedes : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
  (y:a) (s1:(list a)) (s2:(list a)), (list.Mem.mem y
  (Init.Datatypes.app s1 (Init.Datatypes.cons x Init.Datatypes.nil))) ->
  (precedes y x (Init.Datatypes.app s1 (Init.Datatypes.cons x s2))).

Axiom precedes_refl : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
  (s:(list a)), (precedes x x s) <-> (list.Mem.mem x s).

Axiom precedes_append_left : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
  (y:a) (s1:(list a)) (s2:(list a)), (precedes x y s1) -> (precedes x y
  (Init.Datatypes.app s2 s1)).

Axiom precedes_append_left_iff : forall {a:Type} {a_WT:WhyType a},
  forall (x:a) (y:a) (s1:(list a)) (s2:(list a)), (~ (list.Mem.mem x s1)) ->
  ((precedes x y (Init.Datatypes.app s1 s2)) <-> (precedes x y s2)).

Axiom precedes_append_right : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
  (y:a) (s1:(list a)) (s2:(list a)), (precedes x y s1) -> (precedes x y
  (Init.Datatypes.app s1 s2)).

Axiom precedes_append_right_iff : forall {a:Type} {a_WT:WhyType a},
  forall (x:a) (y:a) (s1:(list a)) (s2:(list a)), (~ (list.Mem.mem y s2)) ->
  ((precedes x y (Init.Datatypes.app s1 s2)) <-> (precedes x y s1)).

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)), (simplelist
  (Init.Datatypes.app l1 (Init.Datatypes.cons x l2))) ->
  (((Init.Datatypes.app l1 (Init.Datatypes.cons x l2)) = (Init.Datatypes.app l3 (Init.Datatypes.cons x l4))) ->
  ((l1 = l3) /\ (l2 = l4))).

Axiom simplelist_app_disjoint : 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))).

Axiom precedes_antisym : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (y:a)
  (s:(list a)), (simplelist s) -> ((precedes x y s) -> ((precedes y x s) ->
  (x = y))).

Axiom precedes_trans : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (y:a)
  (z:a) (s:(list a)), (simplelist s) -> ((precedes x y s) -> ((precedes y z
  s) -> (precedes x z s))).

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

Axiom reachable_refl : forall (x:vertex), (reachable x x).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Definition no_black_to_white (black1:(set vertex)) (gray1:(set
  vertex)): Prop := forall (x:vertex) (x':vertex), (edge x x') -> ((mem x
  black1) -> (mem x' (union black1 gray1))).

Definition wf_env (e:env): Prop :=
  match e with
  | (mk_env b g s _ _ _) => (wf_color e) /\ ((wf_num e) /\
      ((no_black_to_white b g) /\ ((simplelist s) /\ ((forall (x:vertex)
      (y:vertex), (list.Mem.mem x s) -> ((list.Mem.mem y s) ->
      (((map.Map.get (num e) x) <= (map.Map.get (num e) y))%Z -> (reachable x
      y)))) /\ ((forall (y:vertex), (list.Mem.mem y s) -> exists x:vertex,
      (mem x g) /\ (((map.Map.get (num e) x) <= (map.Map.get (num e) y))%Z /\
      (reachable y x))) /\ forall (cc:(set vertex)), (mem cc (sccs e)) <->
      ((subset cc b) /\ (is_scc cc)))))))
  end.

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

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

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

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

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

Axiom subscc_after_last_gray : forall (e:env) (x:vertex) (s2:(list vertex))
  (s3:(list vertex)), (wf_env e) ->
  match e with
  | (mk_env b g s _ _ _) => (mem x g) -> ((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 vertex)) (s3:(set vertex))
  (g:(set vertex)) (b:(set vertex)) (sccs1:(set vertex)), (infix_eqeq
  (union s2 s3) (union g (diff b sccs1))) -> ((infix_eqeq (inter s2 s3)
  (empty : (set vertex))) -> ((infix_eqeq (inter g s2) (empty : (set
  vertex))) -> (infix_eqeq s3 (union g (diff b (union s2 sccs1)))))).

Axiom wf_color_sccs : forall (e:env), (wf_color e) -> (infix_eqeq
  (set_of (sccs e)) (diff (union (black e) (gray e)) (elements (stack e)))).

Axiom wf_color_3_cases : forall (x:vertex) (e:env), (wf_color e) -> ((mem x
  (set_of (sccs e))) \/ ((mem x (elements (stack e))) \/ ~ (mem x
  (union (black e) (gray e))))).

Axiom num_lmem : forall (e:env) (x:vertex), (wf_env e) ->
  (((0%Z <= (map.Map.get (num e) x))%Z /\ ((map.Map.get (num e)
  x) < (cardinal vertices))%Z) <-> (list.Mem.mem x (stack e))).

Axiom num_rank_strict : forall (e:env) (x:vertex) (y:vertex), (wf_env e) ->
  ((list.Mem.mem x (stack e)) -> ((list.Mem.mem y (stack e)) ->
  (((map.Map.get (num e) x) < (map.Map.get (num e) y))%Z <-> ((precedes y x
  (stack e)) /\ ~ (x = y))))).

Axiom simplelist_x_prec_strict_y' : forall
  {alpha:Type} {alpha_WT:WhyType alpha}, forall (s1:(list alpha))
  (s2:(list alpha)) (s3:(list alpha)) (x:alpha) (y':alpha),
  (s1 = (Init.Datatypes.app s2 s3)) -> ((simplelist s1) -> ((is_last x s2) ->
  ((list.Mem.mem y' s3) -> ((precedes x y' s1) /\ ~ (y' = x))))).

Parameter x: vertex.

Parameter e: (set vertex).

Parameter e1: (set vertex).

Parameter e2: (list vertex).

Parameter e3: (set (set vertex)).

Parameter e4: Z.

Parameter e5: (map.Map.map vertex Z).

Axiom H : (mem x vertices) /\ ~ (mem x (union e e1)).

Axiom H1 : (access_to e1 x).

Axiom H2 : (wf_env (mk_env e e1 e2 e3 e4 e5)).

Parameter o: (set vertex).

Parameter o1: (set vertex).

Parameter o2: (list vertex).

Parameter o3: (set (set vertex)).

Parameter o4: Z.

Parameter o5: (map.Map.map vertex Z).

Axiom H3 : (o = e) /\ ((o1 = (add x e1)) /\ ((o3 = e3) /\
  ((o2 = (Init.Datatypes.cons x e2)) /\ ((o4 = (e4 + 1%Z)%Z) /\
  (o5 = (map.Map.set e5 x e4)))))).

Axiom H4 : (subset (successors x) vertices).

Axiom H5 : forall (x1:vertex), (mem x1 (successors x)) -> (access_to o1 x1).

Axiom H6 : (wf_env (mk_env o o1 o2 o3 o4 o5)).

Parameter result: Z.

Parameter result1: (set vertex).

Parameter result2: (set vertex).

Parameter result3: (list vertex).

Parameter result4: (set (set vertex)).

Parameter result5: Z.

Parameter result6: (map.Map.map vertex Z).

Axiom H7 : let e' := (mk_env result1 result2 result3 result4 result5
  result6) in ((wf_env e') /\ (subenv (mk_env o o1 o2 o3 o4 o5) e')).

Axiom H8 : (subset (successors x) (union result1 result2)).

Axiom H9 : forall (x1:vertex), (mem x1 (successors x)) ->
  (result <= (map.Map.get result6 x1))%Z.

Axiom H10 : (result = (cardinal vertices)) \/ exists x1:vertex, (mem x1
  (successors x)) /\ (num_of_reachable result x1 (mk_env result1 result2
  result3 result4 result5 result6)).

Axiom H11 : forall (y:vertex), (xedge_to result3 o2 y) ->
  (result <= (map.Map.get result6 y))%Z.

Axiom H12 : (result < e4)%Z.

Axiom H13 : ~ (result = (cardinal vertices)).

Axiom H14 : exists y:vertex, (~ (y = x)) /\ ((mem y result2) /\
  (((map.Map.get result6 y) < (map.Map.get result6 x))%Z /\ (in_same_scc x
  y))).

Parameter o6: (set vertex).

Parameter o7: (set vertex).

Parameter o8: (list vertex).

Parameter o9: (set (set vertex)).

Parameter o10: Z.

Parameter o11: (map.Map.map vertex Z).

Axiom H15 : (o6 = (add x result1)) /\ ((o7 = (remove x result2)) /\
  ((o8 = result3) /\ ((o9 = result4) /\ ((o10 = result5) /\
  (o11 = result6))))).

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

Theorem WP_parameter_dfs1 : exists s:(list vertex), ((stack (mk_env o6 o7 o8
  o9 o10 o11)) = (Init.Datatypes.app s (stack (mk_env e e1 e2 e3 e4 e5)))) /\
  (subset (elements s) (black (mk_env o6 o7 o8 o9 o10 o11))).
Proof.

move: x e e1 e2 e3 e4 e5 H H1 H2 o o1 o2 o3 o4 o5 H3 H4 H5 H6
        result result1 result2 result3 result4 result5 result6
        H7 H8 H9 H10 H11 H12 H13 H14
        o6 o7 o8 o9 o10 o11 H15.
move => x b g s sccs sn num H H1 wfe
         b0 g0 s0 sccs0 sn0 num0
        [eq1 [eq2 [eq3 [s0def [eq5 eq6]]]]]
H4 H5 H6
      n1 b1 g1 s1 sccs1 sn1 num1
      I' H8 H9 H10 H11 H12 H13 H14
      b' g' s' sccs' sn' num' H15.
pose e := mk_env b g s sccs sn num.
pose e0 := mk_env b0 g0 s0 sccs0 sn0 num0.
pose e1 := mk_env b1 g1 s1 sccs1 sn1 num1.
pose e' := mk_env b' g' s' sccs' sn' num'.
simpl.
s' extends s with black vertices
move: I' => [wfe1 sube0e1].
move: sube0e1 => [[s2 G0] _]; simpl in G0.
move: G0 => [s1def s2black].
move: H15 => [b'def [_ [s'def _]]].

rewrite s'def b'def.
exists (s2 ++ (x :: nil) )%list; split.
- by rewrite -Append.Append_assoc /= -s0def.
- move => y ymem; rewrite add_def1.
  move /elts_app /union_def1 :ymem => [y_in_s2 | y_is_x].
  + by right; move /s2black :y_in_s2.
  + left.
    move /add_def1 :y_is_x => [ | y_in_nil ] //.
    by move /(mem_empty y) :y_in_nil.
Qed.