equal
deleted
inserted
replaced
688 from this[folded tRAG_s] show ?thesis . |
688 from this[folded tRAG_s] show ?thesis . |
689 qed |
689 qed |
690 show ?thesis by (unfold cp_alt_def1 h preced_kept, simp) |
690 show ?thesis by (unfold cp_alt_def1 h preced_kept, simp) |
691 qed |
691 qed |
692 |
692 |
693 lemma cp_kept_tG: |
693 lemma cp_kept_tG: (* aaa *) |
694 assumes "th'' \<notin> ancestors (tG (e#s)) th" |
694 assumes "th'' \<notin> ancestors (tG (e#s)) th" |
695 shows "cp (e#s) th'' = cp s th''" |
695 shows "cp (e#s) th'' = cp s th''" |
696 using cp_kept tG_ancestors_tRAG_refute assms |
696 using cp_kept tG_ancestors_tRAG_refute assms |
697 by blast |
697 by blast |
698 |
698 |
857 qed |
857 qed |
858 with cp_gen_def_cond[OF refl[of "Th th''"]] |
858 with cp_gen_def_cond[OF refl[of "Th th''"]] |
859 show ?thesis by metis |
859 show ?thesis by metis |
860 qed |
860 qed |
861 |
861 |
862 lemma cp_up_tG: |
862 lemma cp_up_tG: (* aaa *) |
863 assumes "th' \<in> ancestors (tG (e#s)) th" |
863 assumes "th' \<in> ancestors (tG (e#s)) th" |
864 and "cp (e#s) th' = cp s th'" |
864 and "cp (e#s) th' = cp s th'" |
865 and "th'' \<in> ancestors (tG (e#s)) th'" |
865 and "th'' \<in> ancestors (tG (e#s)) th'" |
866 shows "cp (e#s) th'' = cp s th''" |
866 shows "cp (e#s) th'' = cp s th''" |
867 using assms cp_up ancestors_tG_tRAG by blast |
867 using assms cp_up ancestors_tG_tRAG by blast |