[STATEMENT]
lemma Image_SN_on:
  assumes "SN_on r (r `` A)"
  shows "SN_on r A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SN_on r A
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f. \<lbrakk>f 0 \<in> A; \<forall>i. (f i, f (Suc i)) \<in> r\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
fix f
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f. \<lbrakk>f 0 \<in> A; \<forall>i. (f i, f (Suc i)) \<in> r\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume "f 0 \<in> A" and chain: "chain r f"
[PROOF STATE]
proof (state)
this:
f 0 \<in> A
\<forall>i. (f i, f (Suc i)) \<in> r

goal (1 subgoal):
 1. \<And>f. \<lbrakk>f 0 \<in> A; \<forall>i. (f i, f (Suc i)) \<in> r\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f 0 \<in> A
\<forall>i. (f i, f (Suc i)) \<in> r
[PROOF STEP]
have "f (Suc 0) \<in> r `` A"
[PROOF STATE]
proof (prove)
using this:
f 0 \<in> A
\<forall>i. (f i, f (Suc i)) \<in> r

goal (1 subgoal):
 1. f (Suc 0) \<in> r `` A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f (Suc 0) \<in> r `` A

goal (1 subgoal):
 1. \<And>f. \<lbrakk>f 0 \<in> A; \<forall>i. (f i, f (Suc i)) \<in> r\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
SN_on r (r `` A)
f (Suc 0) \<in> r `` A
[PROOF STEP]
have "SN_on r {f (Suc 0)}"
[PROOF STATE]
proof (prove)
using this:
SN_on r (r `` A)
f (Suc 0) \<in> r `` A

goal (1 subgoal):
 1. SN_on r {f (Suc 0)}
[PROOF STEP]
by (auto simp add: \<open>f 0 \<in> A\<close> SN_defs)
[PROOF STATE]
proof (state)
this:
SN_on r {f (Suc 0)}

goal (1 subgoal):
 1. \<And>f. \<lbrakk>f 0 \<in> A; \<forall>i. (f i, f (Suc i)) \<in> r\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
SN_on r {f (Suc 0)}

goal (1 subgoal):
 1. \<And>f. \<lbrakk>f 0 \<in> A; \<forall>i. (f i, f (Suc i)) \<in> r\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have "\<not> SN_on r {f (Suc 0)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> SN_on r {f (Suc 0)}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> SN_on r {f (Suc 0)}
[PROOF STEP]
have "f (Suc 0) \<in> {f (Suc 0)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (Suc 0) \<in> {f (Suc 0)}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f (Suc 0) \<in> {f (Suc 0)}

goal (1 subgoal):
 1. \<not> SN_on r {f (Suc 0)}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
f (Suc 0) \<in> {f (Suc 0)}

goal (1 subgoal):
 1. \<not> SN_on r {f (Suc 0)}
[PROOF STEP]
from chain
[PROOF STATE]
proof (chain)
picking this:
\<forall>i. (f i, f (Suc i)) \<in> r
[PROOF STEP]
have "chain r (f \<circ> Suc)"
[PROOF STATE]
proof (prove)
using this:
\<forall>i. (f i, f (Suc i)) \<in> r

goal (1 subgoal):
 1. \<forall>i. ((f \<circ> Suc) i, (f \<circ> Suc) (Suc i)) \<in> r
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>i. ((f \<circ> Suc) i, (f \<circ> Suc) (Suc i)) \<in> r

goal (1 subgoal):
 1. \<not> SN_on r {f (Suc 0)}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
f (Suc 0) \<in> {f (Suc 0)}
\<forall>i. ((f \<circ> Suc) i, (f \<circ> Suc) (Suc i)) \<in> r
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
f (Suc 0) \<in> {f (Suc 0)}
\<forall>i. ((f \<circ> Suc) i, (f \<circ> Suc) (Suc i)) \<in> r

goal (1 subgoal):
 1. \<not> SN_on r {f (Suc 0)}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> SN_on r {f (Suc 0)}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<not> SN_on r {f (Suc 0)}

goal (1 subgoal):
 1. \<And>f. \<lbrakk>f 0 \<in> A; \<forall>i. (f i, f (Suc i)) \<in> r\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
SN_on r {f (Suc 0)}
\<not> SN_on r {f (Suc 0)}
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
SN_on r {f (Suc 0)}
\<not> SN_on r {f (Suc 0)}

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

goal:
No subgoals!
[PROOF STEP]
qed