[STATEMENT]
lemma sparsegrid'I[intro]:
  assumes b: "b \<in> sparsegrid' dm" and p: "p \<in> grid b ds"
  shows "p \<in> sparsegrid' dm"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<in> sparsegrid' dm
[PROOF STEP]
using sparsegrid'_length[OF b] b
       grid_transitive[OF grid_subset_alldim[OF p], where c="start dm" and ds''="{0..<dm}"]
[PROOF STATE]
proof (prove)
using this:
length b = dm
b \<in> sparsegrid' dm
\<lbrakk>b \<in> grid (start dm) ?ds'; ?ds' \<subseteq> {0..<dm}; {0..<length b} \<subseteq> {0..<dm}\<rbrakk> \<Longrightarrow> p \<in> grid (start dm) {0..<dm}

goal (1 subgoal):
 1. p \<in> sparsegrid' dm
[PROOF STEP]
unfolding sparsegrid'_def
[PROOF STATE]
proof (prove)
using this:
length b = dm
b \<in> grid (start dm) {0..<dm}
\<lbrakk>b \<in> grid (start dm) ?ds'; ?ds' \<subseteq> {0..<dm}; {0..<length b} \<subseteq> {0..<dm}\<rbrakk> \<Longrightarrow> p \<in> grid (start dm) {0..<dm}

goal (1 subgoal):
 1. p \<in> grid (start dm) {0..<dm}
[PROOF STEP]
by auto