|
interval_expr_lnexp : THEORY
BEGIN
IMPORTING interval_expr,
interval_lnexp
expr : VAR RealExpr
n : VAR nat
ln_safe(x:real): real = IF x <= 0 THEN 0 ELSE ln(x) ENDIF
Ln_Inclusion : JUDGEMENT
Ln(n) HAS_TYPE (Inclusion?(Pos?,ln_safe))
Ln_Fundamental : JUDGEMENT
Ln(n) HAS_TYPE (Fundamental?(Pos?))
LN_n(n:nat)(expr): MACRO RealExpr = FUN(Pos?,ln_safe,Ln(n),expr)
exp_safe(x:real) : posreal = exp(x)
Exp_Inclusion : JUDGEMENT
Exp(n) HAS_TYPE (Inclusion?(PreTrue,exp_safe))
Exp_Fundamental : JUDGEMENT
Exp(n) HAS_TYPE (Fundamental?(PreTrue))
EXP_n(n:nat)(expr): MACRO RealExpr = FUN(PreTrue,exp_safe,Exp(n),expr)
e_safe : [Unit->real] = LAMBDA(u:Unit) : e
E_Inclusion : JUDGEMENT
En(n) HAS_TYPE (Includes?(e_safe(unit)))
E_n(n): MACRO RealExpr = CONST(e_safe,En(n))
END interval_expr_lnexp
¤ 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.
|
