|
section \<open>Addition with fixpoint of successor\<close>
theory Ex3
imports "../LCF"
begin
axiomatization
s :: "'a \ 'a" and
p :: "'a \ 'a \ 'a"
where
p_strict: "p(UU) = UU" and
p_s: "p(s(x),y) = s(p(x,y))"
declare p_strict [simp] p_s [simp]
lemma example: "p(FIX(s),y) = FIX(s)"
apply (induct s)
apply simp
apply simp
done
end
¤ Dauer der Verarbeitung: 0.15 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.
|
