[STATEMENT]
lemma my_trancl_step_induct [consumes 1, case_names base step]:
  "\<lbrakk>(a, b) \<in> r\<^sup>+; 
   \<And>x y. (x, y) \<in> r \<Longrightarrow> P x y;
   \<And>x y z. P x y \<Longrightarrow> (y, z) \<in> r \<Longrightarrow> P x z\<rbrakk> \<Longrightarrow> P a b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(a, b) \<in> r\<^sup>+; \<And>x y. (x, y) \<in> r \<Longrightarrow> P x y; \<And>x y z. \<lbrakk>P x y; (y, z) \<in> r\<rbrakk> \<Longrightarrow> P x z\<rbrakk> \<Longrightarrow> P a b
[PROOF STEP]
by (induct rule: trancl_induct, blast+)