[STATEMENT]
lemma rtrancl3p_induct1:
  "\<lbrakk> rtrancl3p r a bs c; P a; \<And>bs c b d. \<lbrakk> rtrancl3p r a bs c; r c b d; P c \<rbrakk> \<Longrightarrow> P d \<rbrakk> \<Longrightarrow> P c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>rtrancl3p r a bs c; P a; \<And>bs c b d. \<lbrakk>rtrancl3p r a bs c; r c b d; P c\<rbrakk> \<Longrightarrow> P d\<rbrakk> \<Longrightarrow> P c
[PROOF STEP]
apply(induct rule: rtrancl3p.induct)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>P a; \<And>bs c b d. \<lbrakk>rtrancl3p r a bs c; r c b d; P c\<rbrakk> \<Longrightarrow> P d\<rbrakk> \<Longrightarrow> P a
 2. \<And>a bs a' b a''. \<lbrakk>rtrancl3p r a bs a'; \<lbrakk>P a; \<And>bs c b d. \<lbrakk>rtrancl3p r a bs c; r c b d; P c\<rbrakk> \<Longrightarrow> P d\<rbrakk> \<Longrightarrow> P a'; r a' b a''; P a; \<And>bs c b d. \<lbrakk>rtrancl3p r a bs c; r c b d; P c\<rbrakk> \<Longrightarrow> P d\<rbrakk> \<Longrightarrow> P a''
[PROOF STEP]
apply(auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done