lex3: THEORY
BEGIN
i, j, m, n, k, p: VAR nat
lex3(m, n, p): ordinal =
add(1+m,add(2,zero,zero),lex2(n,p))
lex3_lt: LEMMA
lex3(i, j, k) < lex3(m, n, p) =
i<m OR
(i=m AND (j<n OR (j=n AND k<p)))
lex3_lt_2: LEMMA
lex3(i, j, k) < lex3(m, n, p) IFF (
i<m OR
(i=m AND (j<n OR (j=n AND k<p))))
END lex3
¤ Dauer der Verarbeitung: 0.0 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.
|