[STATEMENT]
lemma is_strict_orD: "is_strict (\<Otimes>\<^sub>\<or>\<^sub>D) d r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_strict (\<Otimes>\<^sub>\<or>\<^sub>D) d r
[PROOF STEP]
apply (simp add: is_strict_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d o\<^sub>f (\<emptyset> \<circ> r) = \<emptyset>
[PROOF STEP]
apply (simp add: policy_range_comp_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done