[STATEMENT]
lemma [simp]: "pc\<^sub>1 + size(compE\<^sub>2 e\<^sub>1) \<le> pc\<^sub>2 \<Longrightarrow> pcs(compxE\<^sub>2 e\<^sub>1 pc\<^sub>1 d\<^sub>1) \<inter> pcs(compxE\<^sub>2 e\<^sub>2 pc\<^sub>2 d\<^sub>2) = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pc\<^sub>1 + length (compE\<^sub>2 e\<^sub>1) \<le> pc\<^sub>2 \<Longrightarrow> pcs (compxE\<^sub>2 e\<^sub>1 pc\<^sub>1 d\<^sub>1) \<inter> pcs (compxE\<^sub>2 e\<^sub>2 pc\<^sub>2 d\<^sub>2) = {}
[PROOF STEP]
using pcs_subset
[PROOF STATE]
proof (prove)
using this:
pcs (compxE\<^sub>2 ?e ?pc ?d) \<subseteq> {?pc..<?pc + length (compE\<^sub>2 ?e)}
pcs (compxEs\<^sub>2 ?es ?pc ?d) \<subseteq> {?pc..<?pc + length (compEs\<^sub>2 ?es)}

goal (1 subgoal):
 1. pc\<^sub>1 + length (compE\<^sub>2 e\<^sub>1) \<le> pc\<^sub>2 \<Longrightarrow> pcs (compxE\<^sub>2 e\<^sub>1 pc\<^sub>1 d\<^sub>1) \<inter> pcs (compxE\<^sub>2 e\<^sub>2 pc\<^sub>2 d\<^sub>2) = {}
[PROOF STEP]
by fastforce