48 proof - |
48 proof - |
49 assume A1: "f c = Intg x" |
49 assume A1: "f c = Intg x" |
50 assume A2: "\<forall>y. f b = Intg y \<longrightarrow> y \<noteq> x" |
50 assume A2: "\<forall>y. f b = Intg y \<longrightarrow> y \<noteq> x" |
51 assume A3: "(a, b) \<in> R\<^sup>*" |
51 assume A3: "(a, b) \<in> R\<^sup>*" |
52 assume A4: "(b, c) \<in> R\<^sup>*" |
52 assume A4: "(b, c) \<in> R\<^sup>*" |
53 have "(R\<^sup>*) (a, b)" using A3 by (metis mem_def) |
|
54 hence F1: "(a, b) \<in> R\<^sup>*" by (metis mem_def) |
|
55 have "b \<noteq> c" using A1 A2 by metis |
53 have "b \<noteq> c" using A1 A2 by metis |
56 hence "\<exists>x\<^isub>1. (b, x\<^isub>1) \<in> R" using A4 by (metis converse_rtranclE) |
54 hence "\<exists>x\<^isub>1. (b, x\<^isub>1) \<in> R" using A4 by (metis converse_rtranclE) |
57 thus "\<exists>c. (b, c) \<in> R \<and> (a, c) \<in> R\<^sup>*" using F1 by (metis transitive_closure_trans(6)) |
55 thus "\<exists>c. (b, c) \<in> R \<and> (a, c) \<in> R\<^sup>*" using A3 by (metis transitive_closure_trans(6)) |
58 qed |
56 qed |
59 |
57 |
60 lemma "\<lbrakk>f c = Intg x; \<forall>y. f b = Intg y \<longrightarrow> y \<noteq> x; (a, b) \<in> R\<^sup>*; (b, c) \<in> R\<^sup>*\<rbrakk> |
58 lemma "\<lbrakk>f c = Intg x; \<forall>y. f b = Intg y \<longrightarrow> y \<noteq> x; (a, b) \<in> R\<^sup>*; (b, c) \<in> R\<^sup>*\<rbrakk> |
61 \<Longrightarrow> \<exists>c. (b, c) \<in> R \<and> (a, c) \<in> R\<^sup>*" |
59 \<Longrightarrow> \<exists>c. (b, c) \<in> R \<and> (a, c) \<in> R\<^sup>*" |
62 apply (erule_tac x = b in converse_rtranclE) |
60 apply (erule_tac x = b in converse_rtranclE) |