[STATEMENT]
lemma blocksOf_nonInitBlks: 
  "(\<forall>p bk. bk \<in> blocksOf s p \<longrightarrow> P bk) 
       \<Longrightarrow> bk \<in> nonInitBlks s p \<longrightarrow> P bk"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>p bk. bk \<in> blocksOf s p \<longrightarrow> P bk \<Longrightarrow> bk \<in> nonInitBlks s p \<longrightarrow> P bk
[PROOF STEP]
by(auto simp add: allRdBlks_def blocksOf_def nonInitBlks_def 
                    blocksSeen_def allBlocksRead_def rdBy_def, 
    blast)