equal
deleted
inserted
replaced
33 then obtain f where |
33 then obtain f where |
34 in_R: "\<And>x. \<not>accp R x \<Longrightarrow> R (f x) x" |
34 in_R: "\<And>x. \<not>accp R x \<Longrightarrow> R (f x) x" |
35 and nia: "\<And>x. \<not>accp R x \<Longrightarrow> \<not>accp R (f x)" |
35 and nia: "\<And>x. \<not>accp R x \<Longrightarrow> \<not>accp R (f x)" |
36 by blast |
36 by blast |
37 |
37 |
38 let ?s = "\<lambda>i. (f o^ i) x" |
38 let ?s = "\<lambda>i. (f ^^ i) x" |
39 |
39 |
40 { |
40 { |
41 fix i |
41 fix i |
42 have "\<not>accp R (?s i)" |
42 have "\<not>accp R (?s i)" |
43 by (induct i) (auto simp:nia `\<not>accp R x`) |
43 by (induct i) (auto simp:nia `\<not>accp R x`) |