[STATEMENT]
lemma foreachc_reflexive_transitive:
    assumes "reflp r" "transp r"
    assumes "foreach\<^sub>C c f S a\<^sub>1 a\<^sub>2"
    assumes "\<And> x a\<^sub>1 a\<^sub>2. x \<in> S \<Longrightarrow> f x a\<^sub>1 a\<^sub>2 \<Longrightarrow> r a\<^sub>1 a\<^sub>2"
    shows "r a\<^sub>1 a\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r a\<^sub>1 a\<^sub>2
[PROOF STEP]
using assms(3, 4)
[PROOF STATE]
proof (prove)
using this:
foreach\<^sub>C c f S a\<^sub>1 a\<^sub>2
\<lbrakk>?x \<in> S; f ?x ?a\<^sub>1 ?a\<^sub>2\<rbrakk> \<Longrightarrow> r ?a\<^sub>1 ?a\<^sub>2

goal (1 subgoal):
 1. r a\<^sub>1 a\<^sub>2
[PROOF STEP]
proof induct
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>a. (\<And>x a\<^sub>1 a\<^sub>2. \<lbrakk>x \<in> {}; f x a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>1 a\<^sub>2) \<Longrightarrow> r a a
 2. \<And>S a\<^sub>0 a\<^sub>1 x a\<^sub>2. \<lbrakk>foreach\<^sub>C c f S a\<^sub>0 a\<^sub>1; (\<And>x a\<^sub>1 a\<^sub>2. \<lbrakk>x \<in> S; f x a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>1 a\<^sub>2) \<Longrightarrow> r a\<^sub>0 a\<^sub>1; c a\<^sub>1; x \<notin> S; f x a\<^sub>1 a\<^sub>2; \<And>xa a\<^sub>1 a\<^sub>2. \<lbrakk>xa \<in> insert x S; f xa a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>0 a\<^sub>2
 3. \<And>S a\<^sub>0 a\<^sub>1 S'. \<lbrakk>foreach\<^sub>C c f S a\<^sub>0 a\<^sub>1; (\<And>x a\<^sub>1 a\<^sub>2. \<lbrakk>x \<in> S; f x a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>1 a\<^sub>2) \<Longrightarrow> r a\<^sub>0 a\<^sub>1; \<not> c a\<^sub>1; S \<subseteq> S'; \<And>x a\<^sub>1 a\<^sub>2. \<lbrakk>x \<in> S'; f x a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>0 a\<^sub>1
[PROOF STEP]
case (empty a)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x \<in> {}; f ?x ?a\<^sub>1 ?a\<^sub>2\<rbrakk> \<Longrightarrow> r ?a\<^sub>1 ?a\<^sub>2

goal (3 subgoals):
 1. \<And>a. (\<And>x a\<^sub>1 a\<^sub>2. \<lbrakk>x \<in> {}; f x a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>1 a\<^sub>2) \<Longrightarrow> r a a
 2. \<And>S a\<^sub>0 a\<^sub>1 x a\<^sub>2. \<lbrakk>foreach\<^sub>C c f S a\<^sub>0 a\<^sub>1; (\<And>x a\<^sub>1 a\<^sub>2. \<lbrakk>x \<in> S; f x a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>1 a\<^sub>2) \<Longrightarrow> r a\<^sub>0 a\<^sub>1; c a\<^sub>1; x \<notin> S; f x a\<^sub>1 a\<^sub>2; \<And>xa a\<^sub>1 a\<^sub>2. \<lbrakk>xa \<in> insert x S; f xa a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>0 a\<^sub>2
 3. \<And>S a\<^sub>0 a\<^sub>1 S'. \<lbrakk>foreach\<^sub>C c f S a\<^sub>0 a\<^sub>1; (\<And>x a\<^sub>1 a\<^sub>2. \<lbrakk>x \<in> S; f x a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>1 a\<^sub>2) \<Longrightarrow> r a\<^sub>0 a\<^sub>1; \<not> c a\<^sub>1; S \<subseteq> S'; \<And>x a\<^sub>1 a\<^sub>2. \<lbrakk>x \<in> S'; f x a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>0 a\<^sub>1
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r a a
[PROOF STEP]
using reflpD assms(1)
[PROOF STATE]
proof (prove)
using this:
reflp ?R \<Longrightarrow> ?R ?x ?x
reflp r

goal (1 subgoal):
 1. r a a
[PROOF STEP]
by this
[PROOF STATE]
proof (state)
this:
r a a

goal (2 subgoals):
 1. \<And>S a\<^sub>0 a\<^sub>1 x a\<^sub>2. \<lbrakk>foreach\<^sub>C c f S a\<^sub>0 a\<^sub>1; (\<And>x a\<^sub>1 a\<^sub>2. \<lbrakk>x \<in> S; f x a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>1 a\<^sub>2) \<Longrightarrow> r a\<^sub>0 a\<^sub>1; c a\<^sub>1; x \<notin> S; f x a\<^sub>1 a\<^sub>2; \<And>xa a\<^sub>1 a\<^sub>2. \<lbrakk>xa \<in> insert x S; f xa a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>0 a\<^sub>2
 2. \<And>S a\<^sub>0 a\<^sub>1 S'. \<lbrakk>foreach\<^sub>C c f S a\<^sub>0 a\<^sub>1; (\<And>x a\<^sub>1 a\<^sub>2. \<lbrakk>x \<in> S; f x a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>1 a\<^sub>2) \<Longrightarrow> r a\<^sub>0 a\<^sub>1; \<not> c a\<^sub>1; S \<subseteq> S'; \<And>x a\<^sub>1 a\<^sub>2. \<lbrakk>x \<in> S'; f x a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>0 a\<^sub>1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>S a\<^sub>0 a\<^sub>1 x a\<^sub>2. \<lbrakk>foreach\<^sub>C c f S a\<^sub>0 a\<^sub>1; (\<And>x a\<^sub>1 a\<^sub>2. \<lbrakk>x \<in> S; f x a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>1 a\<^sub>2) \<Longrightarrow> r a\<^sub>0 a\<^sub>1; c a\<^sub>1; x \<notin> S; f x a\<^sub>1 a\<^sub>2; \<And>xa a\<^sub>1 a\<^sub>2. \<lbrakk>xa \<in> insert x S; f xa a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>0 a\<^sub>2
 2. \<And>S a\<^sub>0 a\<^sub>1 S'. \<lbrakk>foreach\<^sub>C c f S a\<^sub>0 a\<^sub>1; (\<And>x a\<^sub>1 a\<^sub>2. \<lbrakk>x \<in> S; f x a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>1 a\<^sub>2) \<Longrightarrow> r a\<^sub>0 a\<^sub>1; \<not> c a\<^sub>1; S \<subseteq> S'; \<And>x a\<^sub>1 a\<^sub>2. \<lbrakk>x \<in> S'; f x a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>0 a\<^sub>1
[PROOF STEP]
case (insert S a\<^sub>0 a\<^sub>1 x a\<^sub>2)
[PROOF STATE]
proof (state)
this:
foreach\<^sub>C c f S a\<^sub>0 a\<^sub>1
(\<And>x a\<^sub>1 a\<^sub>2. \<lbrakk>x \<in> S; f x a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>1 a\<^sub>2) \<Longrightarrow> r a\<^sub>0 a\<^sub>1
c a\<^sub>1
x \<notin> S
f x a\<^sub>1 a\<^sub>2
\<lbrakk>?x \<in> insert x S; f ?x ?a\<^sub>1 ?a\<^sub>2\<rbrakk> \<Longrightarrow> r ?a\<^sub>1 ?a\<^sub>2

goal (2 subgoals):
 1. \<And>S a\<^sub>0 a\<^sub>1 x a\<^sub>2. \<lbrakk>foreach\<^sub>C c f S a\<^sub>0 a\<^sub>1; (\<And>x a\<^sub>1 a\<^sub>2. \<lbrakk>x \<in> S; f x a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>1 a\<^sub>2) \<Longrightarrow> r a\<^sub>0 a\<^sub>1; c a\<^sub>1; x \<notin> S; f x a\<^sub>1 a\<^sub>2; \<And>xa a\<^sub>1 a\<^sub>2. \<lbrakk>xa \<in> insert x S; f xa a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>0 a\<^sub>2
 2. \<And>S a\<^sub>0 a\<^sub>1 S'. \<lbrakk>foreach\<^sub>C c f S a\<^sub>0 a\<^sub>1; (\<And>x a\<^sub>1 a\<^sub>2. \<lbrakk>x \<in> S; f x a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>1 a\<^sub>2) \<Longrightarrow> r a\<^sub>0 a\<^sub>1; \<not> c a\<^sub>1; S \<subseteq> S'; \<And>x a\<^sub>1 a\<^sub>2. \<lbrakk>x \<in> S'; f x a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>0 a\<^sub>1
[PROOF STEP]
have 0: "r a\<^sub>0 a\<^sub>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r a\<^sub>0 a\<^sub>1
[PROOF STEP]
using insert(2) insert(6)
[PROOF STATE]
proof (prove)
using this:
(\<And>x a\<^sub>1 a\<^sub>2. \<lbrakk>x \<in> S; f x a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>1 a\<^sub>2) \<Longrightarrow> r a\<^sub>0 a\<^sub>1
\<lbrakk>?x \<in> insert x S; f ?x ?a\<^sub>1 ?a\<^sub>2\<rbrakk> \<Longrightarrow> r ?a\<^sub>1 ?a\<^sub>2

goal (1 subgoal):
 1. r a\<^sub>0 a\<^sub>1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
r a\<^sub>0 a\<^sub>1

goal (2 subgoals):
 1. \<And>S a\<^sub>0 a\<^sub>1 x a\<^sub>2. \<lbrakk>foreach\<^sub>C c f S a\<^sub>0 a\<^sub>1; (\<And>x a\<^sub>1 a\<^sub>2. \<lbrakk>x \<in> S; f x a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>1 a\<^sub>2) \<Longrightarrow> r a\<^sub>0 a\<^sub>1; c a\<^sub>1; x \<notin> S; f x a\<^sub>1 a\<^sub>2; \<And>xa a\<^sub>1 a\<^sub>2. \<lbrakk>xa \<in> insert x S; f xa a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>0 a\<^sub>2
 2. \<And>S a\<^sub>0 a\<^sub>1 S'. \<lbrakk>foreach\<^sub>C c f S a\<^sub>0 a\<^sub>1; (\<And>x a\<^sub>1 a\<^sub>2. \<lbrakk>x \<in> S; f x a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>1 a\<^sub>2) \<Longrightarrow> r a\<^sub>0 a\<^sub>1; \<not> c a\<^sub>1; S \<subseteq> S'; \<And>x a\<^sub>1 a\<^sub>2. \<lbrakk>x \<in> S'; f x a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>0 a\<^sub>1
[PROOF STEP]
have 1: "r a\<^sub>1 a\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r a\<^sub>1 a\<^sub>2
[PROOF STEP]
using insert(6) insert(5)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<in> insert x S; f ?x ?a\<^sub>1 ?a\<^sub>2\<rbrakk> \<Longrightarrow> r ?a\<^sub>1 ?a\<^sub>2
f x a\<^sub>1 a\<^sub>2

goal (1 subgoal):
 1. r a\<^sub>1 a\<^sub>2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
r a\<^sub>1 a\<^sub>2

goal (2 subgoals):
 1. \<And>S a\<^sub>0 a\<^sub>1 x a\<^sub>2. \<lbrakk>foreach\<^sub>C c f S a\<^sub>0 a\<^sub>1; (\<And>x a\<^sub>1 a\<^sub>2. \<lbrakk>x \<in> S; f x a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>1 a\<^sub>2) \<Longrightarrow> r a\<^sub>0 a\<^sub>1; c a\<^sub>1; x \<notin> S; f x a\<^sub>1 a\<^sub>2; \<And>xa a\<^sub>1 a\<^sub>2. \<lbrakk>xa \<in> insert x S; f xa a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>0 a\<^sub>2
 2. \<And>S a\<^sub>0 a\<^sub>1 S'. \<lbrakk>foreach\<^sub>C c f S a\<^sub>0 a\<^sub>1; (\<And>x a\<^sub>1 a\<^sub>2. \<lbrakk>x \<in> S; f x a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>1 a\<^sub>2) \<Longrightarrow> r a\<^sub>0 a\<^sub>1; \<not> c a\<^sub>1; S \<subseteq> S'; \<And>x a\<^sub>1 a\<^sub>2. \<lbrakk>x \<in> S'; f x a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>0 a\<^sub>1
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r a\<^sub>0 a\<^sub>2
[PROOF STEP]
using transpD assms(2) 0 1
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>transp ?r; ?r ?x ?y; ?r ?y ?z\<rbrakk> \<Longrightarrow> ?r ?x ?z
transp r
r a\<^sub>0 a\<^sub>1
r a\<^sub>1 a\<^sub>2

goal (1 subgoal):
 1. r a\<^sub>0 a\<^sub>2
[PROOF STEP]
by this
[PROOF STATE]
proof (state)
this:
r a\<^sub>0 a\<^sub>2

goal (1 subgoal):
 1. \<And>S a\<^sub>0 a\<^sub>1 S'. \<lbrakk>foreach\<^sub>C c f S a\<^sub>0 a\<^sub>1; (\<And>x a\<^sub>1 a\<^sub>2. \<lbrakk>x \<in> S; f x a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>1 a\<^sub>2) \<Longrightarrow> r a\<^sub>0 a\<^sub>1; \<not> c a\<^sub>1; S \<subseteq> S'; \<And>x a\<^sub>1 a\<^sub>2. \<lbrakk>x \<in> S'; f x a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>0 a\<^sub>1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>S a\<^sub>0 a\<^sub>1 S'. \<lbrakk>foreach\<^sub>C c f S a\<^sub>0 a\<^sub>1; (\<And>x a\<^sub>1 a\<^sub>2. \<lbrakk>x \<in> S; f x a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>1 a\<^sub>2) \<Longrightarrow> r a\<^sub>0 a\<^sub>1; \<not> c a\<^sub>1; S \<subseteq> S'; \<And>x a\<^sub>1 a\<^sub>2. \<lbrakk>x \<in> S'; f x a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>0 a\<^sub>1
[PROOF STEP]
case (abort S a\<^sub>0 a\<^sub>1 S')
[PROOF STATE]
proof (state)
this:
foreach\<^sub>C c f S a\<^sub>0 a\<^sub>1
(\<And>x a\<^sub>1 a\<^sub>2. \<lbrakk>x \<in> S; f x a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>1 a\<^sub>2) \<Longrightarrow> r a\<^sub>0 a\<^sub>1
\<not> c a\<^sub>1
S \<subseteq> S'
\<lbrakk>?x \<in> S'; f ?x ?a\<^sub>1 ?a\<^sub>2\<rbrakk> \<Longrightarrow> r ?a\<^sub>1 ?a\<^sub>2

goal (1 subgoal):
 1. \<And>S a\<^sub>0 a\<^sub>1 S'. \<lbrakk>foreach\<^sub>C c f S a\<^sub>0 a\<^sub>1; (\<And>x a\<^sub>1 a\<^sub>2. \<lbrakk>x \<in> S; f x a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>1 a\<^sub>2) \<Longrightarrow> r a\<^sub>0 a\<^sub>1; \<not> c a\<^sub>1; S \<subseteq> S'; \<And>x a\<^sub>1 a\<^sub>2. \<lbrakk>x \<in> S'; f x a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>0 a\<^sub>1
[PROOF STEP]
have 0: "r a\<^sub>0 a\<^sub>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r a\<^sub>0 a\<^sub>1
[PROOF STEP]
using abort(2) abort(4) abort(5)
[PROOF STATE]
proof (prove)
using this:
(\<And>x a\<^sub>1 a\<^sub>2. \<lbrakk>x \<in> S; f x a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>1 a\<^sub>2) \<Longrightarrow> r a\<^sub>0 a\<^sub>1
S \<subseteq> S'
\<lbrakk>?x \<in> S'; f ?x ?a\<^sub>1 ?a\<^sub>2\<rbrakk> \<Longrightarrow> r ?a\<^sub>1 ?a\<^sub>2

goal (1 subgoal):
 1. r a\<^sub>0 a\<^sub>1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
r a\<^sub>0 a\<^sub>1

goal (1 subgoal):
 1. \<And>S a\<^sub>0 a\<^sub>1 S'. \<lbrakk>foreach\<^sub>C c f S a\<^sub>0 a\<^sub>1; (\<And>x a\<^sub>1 a\<^sub>2. \<lbrakk>x \<in> S; f x a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>1 a\<^sub>2) \<Longrightarrow> r a\<^sub>0 a\<^sub>1; \<not> c a\<^sub>1; S \<subseteq> S'; \<And>x a\<^sub>1 a\<^sub>2. \<lbrakk>x \<in> S'; f x a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>0 a\<^sub>1
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r a\<^sub>0 a\<^sub>1
[PROOF STEP]
using 0
[PROOF STATE]
proof (prove)
using this:
r a\<^sub>0 a\<^sub>1

goal (1 subgoal):
 1. r a\<^sub>0 a\<^sub>1
[PROOF STEP]
by this
[PROOF STATE]
proof (state)
this:
r a\<^sub>0 a\<^sub>1

goal:
No subgoals!
[PROOF STEP]
qed