section \<open>Prefixpoints\<close>
theory Ex4
imports "../LCF"
begin
lemma example:
assumes asms: "f(p) << p" "\q. f(q) << q \ p << q"
shows "FIX(f)=p"
apply (unfold eq_def)
apply (rule conjI)
apply (induct f)
apply (rule minimal)
apply (intro strip)
apply (rule less_trans)
prefer 2
apply (rule asms)
apply (erule less_ap_term)
apply (rule asms)
apply (rule FIX_eq [THEN eq_imp_less1])
done
end
¤ Dauer der Verarbeitung: 0.17 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
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.
|
