definition semiconfluentp :: "('a \ 'a \ bool) \ bool" where "semiconfluentp r \ r\\ OO r\<^sup>*\<^sup>* \ r\<^sup>*\<^sup>* OO r\\\<^sup>*\<^sup>*"
definition confluentp :: "('a \ 'a \ bool) \ bool" where "confluentp r \ r\\\<^sup>*\<^sup>* OO r\<^sup>*\<^sup>* \ r\<^sup>*\<^sup>* OO r\\\<^sup>*\<^sup>*"
definition strong_confluentp :: "('a \ 'a \ bool) \ bool" where "strong_confluentp r \ r\\ OO r \ r\<^sup>*\<^sup>* OO (r\\)\<^sup>=\<^sup>="
lemma semiconfluentpI [intro?]: "semiconfluentp r"if"\x y z. \ r x y; r\<^sup>*\<^sup>* x z \ \ \u. r\<^sup>*\<^sup>* y u \ r\<^sup>*\<^sup>* z u" using that unfolding semiconfluentp_def rtranclp_conversep by blast
lemma semiconfluentpD: "\u. r\<^sup>*\<^sup>* y u \ r\<^sup>*\<^sup>* z u" if "semiconfluentp r" "r x y" "r\<^sup>*\<^sup>* x z" using that unfolding semiconfluentp_def rtranclp_conversep by blast
lemma confluentpI: "confluentp r"if"\x y z. \ r\<^sup>*\<^sup>* x y; r\<^sup>*\<^sup>* x z \ \ \u. r\<^sup>*\<^sup>* y u \ r\<^sup>*\<^sup>* z u" using that unfolding confluentp_def rtranclp_conversep by blast
lemma confluentpD: "\u. r\<^sup>*\<^sup>* y u \ r\<^sup>*\<^sup>* z u" if "confluentp r" "r\<^sup>*\<^sup>* x y" "r\<^sup>*\<^sup>* x z" using that unfolding confluentp_def rtranclp_conversep by blast
lemma strong_confluentpI [intro?]: "strong_confluentp r"if"\x y z. \ r x y; r x z \ \ \u. r\<^sup>*\<^sup>* y u \ r\<^sup>=\<^sup>= z u" using that unfolding strong_confluentp_def by blast
lemma strong_confluentpD: "\u. r\<^sup>*\<^sup>* y u \ r\<^sup>=\<^sup>= z u" if "strong_confluentp r" "r x y" "r x z" using that unfolding strong_confluentp_def by blast
lemma semiconfluentp_imp_confluentp: "confluentp r"if r: "semiconfluentp r" proof(rule confluentpI) show"\u. r\<^sup>*\<^sup>* y u \ r\<^sup>*\<^sup>* z u" if "r\<^sup>*\<^sup>* x y" "r\<^sup>*\<^sup>* x z" for x y z using that(2,1) by(induction arbitrary: y rule: converse_rtranclp_induct)
(blast intro: rtranclp_trans dest: r[THEN semiconfluentpD])+ qed
lemma confluentp_imp_semiconfluentp: "semiconfluentp r"if"confluentp r" using that by(auto intro!: semiconfluentpI dest: confluentpD[OF that])
lemma strong_confluentp_into_semiconfluentp: "semiconfluentp r"if r: "strong_confluentp r" proof show"\u. r\<^sup>*\<^sup>* y u \ r\<^sup>*\<^sup>* z u" if "r x y" "r\<^sup>*\<^sup>* x z" for x y z using that(2,1) apply(induction arbitrary: y rule: converse_rtranclp_induct)
subgoal by blast
subgoal for a b c by (drule (1) strong_confluentpD[OF r, of a c])(auto 10 0 intro: rtranclp_trans) done qed
lemma strong_confluentp_imp_confluentp: "confluentp r"if"strong_confluentp r" unfolding confluentp_eq_semiconfluentp using that by(rule strong_confluentp_into_semiconfluentp)
lemma semiconfluentp_equivclp: "equivclp r = r\<^sup>*\<^sup>* OO r\\\<^sup>*\<^sup>*" if r: "semiconfluentp r" proof(rule antisym[rotated] r_OO_conversep_into_equivclp predicate2I)+ show"(r\<^sup>*\<^sup>* OO r\\\<^sup>*\<^sup>*) x y" if "equivclp r x y" for x y using that unfolding equivclp_def rtranclp_conversep by(induction rule: converse_rtranclp_induct)
(blast elim!: symclpE intro: converse_rtranclp_into_rtranclp rtranclp_trans dest: semiconfluentpD[OF r])+ qed
end
¤ Dauer der Verarbeitung: 0.16 Sekunden
(vorverarbeitet)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
