Goal let x:=O+O in x=x.
intro.
set (y1:=O) in (type of x).
Show.
set (y2:=O) in (value of x) at 1.
Show.
set (y3:=O) in (value of x).
Show.
trivial.
Qed.
¤ Dauer der Verarbeitung: 0.13 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.
|