[STATEMENT]
lemma [code]:
    "not_disjoint_intervals A B =
      (case A of (s,e) \<Rightarrow> case B of (s',e') \<Rightarrow> s \<le> e' \<and> s' \<le> e \<and> s \<le> e \<and> s' \<le> e')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. not_disjoint_intervals A B = (case A of (s, e) \<Rightarrow> case B of (s', e') \<Rightarrow> s \<le> e' \<and> s' \<le> e \<and> s \<le> e \<and> s' \<le> e')
[PROOF STEP]
apply(cases A, cases B)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>A = (a, b); B = (aa, ba)\<rbrakk> \<Longrightarrow> not_disjoint_intervals A B = (case A of (s, e) \<Rightarrow> case B of (s', e') \<Rightarrow> s \<le> e' \<and> s' \<le> e \<and> s \<le> e \<and> s' \<le> e')
[PROOF STEP]
apply(simp add: not_disjoint_intervals_def interval_of.simps disjoint_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done