|
(interval_expr_lnexp
(ln_safe_TCC1 0
(ln_safe_TCC1-1 nil 3567425561 ("" (subtype-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(ge_realorder name-judgement "RealOrder" real_orders "reals/")
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(le_realorder name-judgement "RealOrder" real_orders "reals/"))
nil))
(Ln_Inclusion 0
(Ln_Inclusion-2 nil 3567440894
("" (skeep)
(("" (expand "Inclusion?")
(("" (skeep :preds? t)
(("" (expand "ln_safe")
(("" (case-replace "x <= 0")
(("1" (hide 1) (("1" (grind) nil nil)) nil)
("2" (assert) (("2" (rewrite "Ln_inclusion") nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
((Inclusion? const-decl "bool" interval nil)
(ln_safe const-decl "real" interval_expr_lnexp nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(Interval type-eq-decl nil interval nil)
(Ln_inclusion formula-decl nil interval_lnexp nil)
(|##| const-decl "bool" interval nil)
(Pos? const-decl "bool" interval nil)
(Gt const-decl "bool" interval nil)
(le_realorder name-judgement "RealOrder" real_orders "reals/")
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(Pos_Precondition name-judgement "(Precondition?)" interval nil)
(gt_realorder name-judgement "RealOrder" real_orders "reals/")
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(<= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil))
nil)
(Ln_Inclusion-1 nil 3567440888 ("" (judgement-tcc) nil nil) nil nil))
(Ln_Fundamental 0
(Ln_Fundamental-1 nil 3567440888
("" (skeep)
(("" (expand "Fundamental?")
(("" (skeep) (("" (rewrite "Ln_fundamental") nil nil)) nil))
nil))
nil)
((Fundamental? const-decl "bool" interval nil)
(Ln_fundamental formula-decl nil interval_lnexp nil)
(real nonempty-type-from-decl nil reals nil)
(Interval type-eq-decl nil interval nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(Proper? const-decl "bool" interval nil)
(ProperInterval type-eq-decl nil interval nil)
(Pos? const-decl "bool" interval nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil))
nil))
(LN_n_TCC1 0
(LN_n_TCC1-2 nil 3567425678 ("" (assert) nil nil)
((Ln_Fundamental application-judgement "(Fundamental?(Pos?))"
interval_expr_lnexp nil)
(Ln_Inclusion application-judgement "(Inclusion?(Pos?, ln_safe))"
interval_expr_lnexp nil))
nil)
(LN_n_TCC1-1 nil 3567425561 ("" (subtype-tcc) nil nil) nil nil))
(Exp_Inclusion 0
(Exp_Inclusion-2 nil 3568635461
("" (skeep)
(("" (expand "Inclusion?")
(("" (skeep)
(("" (expand "exp_safe")
(("" (rewrite "Exp_inclusion") nil nil)) nil))
nil))
nil))
nil)
((Inclusion? const-decl "bool" interval nil)
(exp_safe const-decl "posreal" interval_expr_lnexp nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(PreTrue const-decl "(Precondition?)" interval_expr nil)
(Precondition? const-decl "bool" interval nil)
(PRED type-eq-decl nil defined_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(Interval type-eq-decl nil interval nil)
(real nonempty-type-from-decl nil reals nil)
(Exp_inclusion formula-decl nil interval_lnexp nil))
nil)
(Exp_Inclusion-1 nil 3568635426 ("" (judgement-tcc) nil nil) nil
nil))
(Exp_Fundamental 0
(Exp_Fundamental-2 nil 3568635497
("" (skeep)
(("" (expand "Fundamental?")
(("" (skeep) (("" (rewrite "Exp_fundamental") nil nil)) nil))
nil))
nil)
((Fundamental? const-decl "bool" interval nil)
(Exp_fundamental formula-decl nil interval_lnexp nil)
(real nonempty-type-from-decl nil reals nil)
(Interval type-eq-decl nil interval nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(Proper? const-decl "bool" interval nil)
(ProperInterval type-eq-decl nil interval nil)
(PRED type-eq-decl nil defined_types nil)
(Precondition? const-decl "bool" interval nil)
(PreTrue const-decl "(Precondition?)" interval_expr nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil))
nil)
(Exp_Fundamental-1 nil 3568635426 ("" (judgement-tcc) nil nil) nil
nil))
(EXP_n_TCC1 0
(EXP_n_TCC1-1 nil 3568635426 ("" (subtype-tcc) nil nil)
((Exp_Fundamental application-judgement "(Fundamental?(PreTrue))"
interval_expr_lnexp nil)
(Exp_Inclusion application-judgement
"(Inclusion?(PreTrue, exp_safe))" interval_expr_lnexp nil))
nil))
(E_Inclusion 0
(E_Inclusion-2 nil 3568635873
("" (skeep)
(("" (expand "Includes?")
(("" (expand "e_safe")
(("" (expand "En")
(("" (expand "e")
(("" (rewrite "Exp_inclusion")
(("" (hide 2) (("" (grind) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil)
((Includes? const-decl "bool" interval nil)
(En const-decl "(Pos?)" interval_lnexp nil)
(Exp_inclusion formula-decl nil interval_lnexp nil)
(real nonempty-type-from-decl nil reals nil)
(Interval type-eq-decl nil interval nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
([\|\|] const-decl "Interval" interval nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(Exp_Inclusion application-judgement
"(Inclusion?(PreTrue, exp_safe))" interval_expr_lnexp nil)
(Exp_Fundamental application-judgement "(Fundamental?(PreTrue))"
interval_expr_lnexp nil)
(Proper_Exp application-judgement "ProperInterval" interval_lnexp
nil)
(e_bound name-judgement "{x: posreal | e_lb < e AND e < e_ub}"
exp_approx "lnexp_fnd/")
(r2i_Proper application-judgement "ProperInterval" interval nil)
(r2i_Pos application-judgement "(Pos?)" interval nil)
(r2i_Nneg application-judgement "(NonNeg?)" interval nil)
(exp_1 formula-decl nil ln_exp "lnexp_fnd/")
(|##| const-decl "bool" interval nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(le_realorder name-judgement "RealOrder" real_orders "reals/")
(e const-decl "posreal" ln_exp "lnexp_fnd/")
(e_safe const-decl "[Unit -> real]" interval_expr_lnexp nil))
nil)
(E_Inclusion-1 nil 3568635847 ("" (judgement-tcc) nil nil) nil nil)))
¤ Dauer der Verarbeitung: 0.21 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.
|
