[STATEMENT]
lemma sub_env_trans:
  assumes "sub_env e e'" and "sub_env e' e''"
  shows "sub_env e e''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sub_env e e''
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
sub_env e e'
sub_env e' e''

goal (1 subgoal):
 1. sub_env e e''
[PROOF STEP]
unfolding sub_env_def
[PROOF STATE]
proof (prove)
using this:
root e' = root e \<and> visited e \<subseteq> visited e' \<and> explored e \<subseteq> explored e' \<and> (\<forall>v. vsuccs e v \<subseteq> vsuccs e' v) \<and> (\<forall>v. \<S> e v \<subseteq> \<S> e' v) \<and> \<Union> {\<S> e v |v. v \<in> set (stack e)} \<subseteq> \<Union> {\<S> e' v |v. v \<in> set (stack e')}
root e'' = root e' \<and> visited e' \<subseteq> visited e'' \<and> explored e' \<subseteq> explored e'' \<and> (\<forall>v. vsuccs e' v \<subseteq> vsuccs e'' v) \<and> (\<forall>v. \<S> e' v \<subseteq> \<S> e'' v) \<and> \<Union> {\<S> e' v |v. v \<in> set (stack e')} \<subseteq> \<Union> {\<S> e'' v |v. v \<in> set (stack e'')}

goal (1 subgoal):
 1. root e'' = root e \<and> visited e \<subseteq> visited e'' \<and> explored e \<subseteq> explored e'' \<and> (\<forall>v. vsuccs e v \<subseteq> vsuccs e'' v) \<and> (\<forall>v. \<S> e v \<subseteq> \<S> e'' v) \<and> \<Union> {\<S> e v |v. v \<in> set (stack e)} \<subseteq> \<Union> {\<S> e'' v |v. v \<in> set (stack e'')}
[PROOF STEP]
by (metis (no_types, lifting) subset_trans)