| products/sources/formale sprachen/PVS/interval_arith/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: interval_expr.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(interval_expr
(r2E_TCC1 0 (r2E_TCC1-1 nil 3576786010 ("" (subtype-tcc) nil nil) (([\|\|] const-decl "Interval" interval nil) (|##| const-decl "bool" interval nil) (Includes? const-decl "bool" interval nil)) nil)) (I2E_TCC1 0 (I2E_TCC1-1 nil 3576786010 ("" (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) (real nonempty-type-from-decl nil reals nil) (Interval type-eq-decl nil interval nil) (Proper? const-decl "bool" interval nil) (ProperInterval type-eq-decl nil interval nil) (le_realorder name-judgement "RealOrder" real_orders "reals/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (slice const-decl "real" interval nil) (midpoint const-decl "real" interval nil) (|##| const-decl "bool" interval nil) (Includes? const-decl "bool" interval nil) (real_plus_real_is_real application-judgement "real" reals nil)) nil)) (PreTrue_TCC1 0 (PreTrue_TCC1-1 nil 3577184980 ("" (subtype-tcc) nil nil) ((Precondition? const-decl "bool" interval nil)) nil)) (real_bool_expr 0 (real_bool_expr-1 nil 3577460822 ("" (grind) nil nil) ((realexpr? const-decl "bool" interval_expr nil) (boolexpr? const-decl "bool" interval_expr nil)) shostak)) (eval_TCC1 0 (eval_TCC1-1 nil 3546625295 ("" (lemma "well_founded_restrict[IntervalExpr,RealExpr]") (("" (inst?) (("" (expand "well_founded?") (("" (propax) nil nil)) nil)) nil)) nil) ((<< adt-def-decl "(strict_well_founded?[IntervalExpr])" IntervalExpr_adt nil) (strict_well_founded? const-decl "bool" orders nil) (well_founded? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil) (well_founded_restrict judgement-tcc nil restrict_order_props nil) (IntervalExpr type-decl nil IntervalExpr_adt nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (const? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (varidx? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (add? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (abs? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (neg? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sub? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (mult? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sq? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (pow? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (div? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (fun? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (letin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (RealExpr type-eq-decl nil IntervalExpr_adt nil)) nil)) (eval_TCC2 0 (eval_TCC2-1 nil 3546625295 ("" (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) (OR const-decl "[bool, bool -> bool]" booleans nil) (IntervalExpr type-decl nil IntervalExpr_adt nil) (const? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (varidx? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (add? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (abs? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (neg? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sub? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (mult? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sq? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (pow? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (div? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (fun? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (letin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (RealExpr type-eq-decl nil IntervalExpr_adt nil)) nil)) (eval_TCC3 0 (eval_TCC3-1 nil 3546625295 ("" (termination-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) (OR const-decl "[bool, bool -> bool]" booleans nil) (IntervalExpr type-decl nil IntervalExpr_adt nil) (const? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (varidx? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (add? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (abs? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (neg? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sub? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (mult? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sq? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (pow? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (div? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (fun? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (letin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (RealExpr type-eq-decl nil IntervalExpr_adt nil) (<< adt-def-decl "(strict_well_founded?[IntervalExpr])" IntervalExpr_adt nil) (restrict const-decl "R" restrict nil)) nil)) (eval_TCC4 0 (eval_TCC4-1 nil 3546625295 ("" (termination-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) (OR const-decl "[bool, bool -> bool]" booleans nil) (IntervalExpr type-decl nil IntervalExpr_adt nil) (const? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (varidx? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (add? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (abs? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (neg? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sub? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (mult? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sq? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (pow? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (div? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (fun? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (letin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (RealExpr type-eq-decl nil IntervalExpr_adt nil) (<< adt-def-decl "(strict_well_founded?[IntervalExpr])" IntervalExpr_adt nil) (restrict const-decl "R" restrict nil)) nil)) (eval_TCC5 0 (eval_TCC5-1 nil 3546625295 ("" (termination-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) (OR const-decl "[bool, bool -> bool]" booleans nil) (IntervalExpr type-decl nil IntervalExpr_adt nil) (const? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (varidx? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (add? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (abs? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (neg? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sub? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (mult? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sq? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (pow? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (div? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (fun? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (letin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (RealExpr type-eq-decl nil IntervalExpr_adt nil)) nil)) (eval_TCC6 0 (eval_TCC6-1 nil 3546625295 ("" (termination-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) (OR const-decl "[bool, bool -> bool]" booleans nil) (IntervalExpr type-decl nil IntervalExpr_adt nil) (const? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (varidx? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (add? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (abs? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (neg? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sub? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (mult? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sq? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (pow? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (div? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (fun? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (letin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (RealExpr type-eq-decl nil IntervalExpr_adt nil) (<< adt-def-decl "(strict_well_founded?[IntervalExpr])" IntervalExpr_adt nil) (restrict const-decl "R" restrict nil)) nil)) (eval_TCC7 0 (eval_TCC7-1 nil 3546625295 ("" (termination-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) (OR const-decl "[bool, bool -> bool]" booleans nil) (IntervalExpr type-decl nil IntervalExpr_adt nil) (const? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (varidx? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (add? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (abs? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (neg? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sub? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (mult? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sq? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (pow? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (div? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (fun? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (letin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (RealExpr type-eq-decl nil IntervalExpr_adt nil)) nil)) (eval_TCC8 0 (eval_TCC8-1 nil 3546625295 ("" (termination-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) (OR const-decl "[bool, bool -> bool]" booleans nil) (IntervalExpr type-decl nil IntervalExpr_adt nil) (const? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (varidx? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (add? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (abs? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (neg? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sub? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (mult? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sq? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (pow? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (div? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (fun? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (letin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (RealExpr type-eq-decl nil IntervalExpr_adt nil) (<< adt-def-decl "(strict_well_founded?[IntervalExpr])" IntervalExpr_adt nil) (restrict const-decl "R" restrict nil)) nil)) (eval_TCC9 0 (eval_TCC9-1 nil 3546625295 ("" (termination-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) (OR const-decl "[bool, bool -> bool]" booleans nil) (IntervalExpr type-decl nil IntervalExpr_adt nil) (const? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (varidx? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (add? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (abs? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (neg? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sub? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (mult? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sq? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (pow? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (div? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (fun? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (letin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (RealExpr type-eq-decl nil IntervalExpr_adt nil)) nil)) (eval_TCC10 0 (eval_TCC10-1 nil 3546625295 ("" (termination-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) (OR const-decl "[bool, bool -> bool]" booleans nil) (IntervalExpr type-decl nil IntervalExpr_adt nil) (const? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (varidx? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (add? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (abs? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (neg? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sub? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (mult? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sq? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (pow? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (div? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (fun? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (letin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (RealExpr type-eq-decl nil IntervalExpr_adt nil) (<< adt-def-decl "(strict_well_founded?[IntervalExpr])" IntervalExpr_adt nil) (restrict const-decl "R" restrict nil)) nil)) (eval_TCC11 0 (eval_TCC11-1 nil 3546625295 ("" (termination-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) (OR const-decl "[bool, bool -> bool]" booleans nil) (IntervalExpr type-decl nil IntervalExpr_adt nil) (const? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (varidx? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (add? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (abs? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (neg? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sub? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (mult? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sq? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (pow? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (div? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (fun? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (letin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (RealExpr type-eq-decl nil IntervalExpr_adt nil) (<< adt-def-decl "(strict_well_founded?[IntervalExpr])" IntervalExpr_adt nil) (restrict const-decl "R" restrict nil)) nil)) (eval_TCC12 0 (eval_TCC12-1 nil 3546625295 ("" (termination-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) (OR const-decl "[bool, bool -> bool]" booleans nil) (IntervalExpr type-decl nil IntervalExpr_adt nil) (const? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (varidx? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (add? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (abs? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (neg? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sub? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (mult? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sq? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (pow? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (div? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (fun? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (letin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (RealExpr type-eq-decl nil IntervalExpr_adt nil)) nil)) (eval_TCC13 0 (eval_TCC13-1 nil 3546625295 ("" (termination-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) (OR const-decl "[bool, bool -> bool]" booleans nil) (IntervalExpr type-decl nil IntervalExpr_adt nil) (const? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (varidx? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (add? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (abs? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (neg? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sub? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (mult? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sq? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (pow? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (div? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (fun? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (letin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (RealExpr type-eq-decl nil IntervalExpr_adt nil) (<< adt-def-decl "(strict_well_founded?[IntervalExpr])" IntervalExpr_adt nil) (restrict const-decl "R" restrict nil)) nil)) (eval_TCC14 0 (eval_TCC14-1 nil 3546625295 ("" (termination-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) (OR const-decl "[bool, bool -> bool]" booleans nil) (IntervalExpr type-decl nil IntervalExpr_adt nil) (const? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (varidx? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (add? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (abs? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (neg? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sub? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (mult? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sq? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (pow? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (div? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (fun? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (letin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (RealExpr type-eq-decl nil IntervalExpr_adt nil) (<< adt-def-decl "(strict_well_founded?[IntervalExpr])" IntervalExpr_adt nil) (restrict const-decl "R" restrict nil)) nil)) (eval_TCC15 0 (eval_TCC15-1 nil 3546625295 ("" (termination-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) (OR const-decl "[bool, bool -> bool]" booleans nil) (IntervalExpr type-decl nil IntervalExpr_adt nil) (const? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (varidx? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (add? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (abs? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (neg? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sub? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (mult? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sq? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (pow? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (div? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (fun? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (letin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (RealExpr type-eq-decl nil IntervalExpr_adt nil)) nil)) (eval_TCC16 0 (eval_TCC16-1 nil 3546625295 ("" (termination-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) (OR const-decl "[bool, bool -> bool]" booleans nil) (IntervalExpr type-decl nil IntervalExpr_adt nil) (const? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (varidx? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (add? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (abs? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (neg? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sub? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (mult? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sq? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (pow? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (div? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (fun? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (letin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (RealExpr type-eq-decl nil IntervalExpr_adt nil) (<< adt-def-decl "(strict_well_founded?[IntervalExpr])" IntervalExpr_adt nil) (restrict const-decl "R" restrict nil)) nil)) (eval_TCC17 0 (eval_TCC17-1 nil 3546625295 ("" (termination-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) (OR const-decl "[bool, bool -> bool]" booleans nil) (IntervalExpr type-decl nil IntervalExpr_adt nil) (const? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (varidx? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (add? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (abs? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (neg? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sub? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (mult? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sq? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (pow? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (div? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (fun? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (letin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (RealExpr type-eq-decl nil IntervalExpr_adt nil)) nil)) (eval_TCC18 0 (eval_TCC18-1 nil 3546625295 ("" (termination-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) (OR const-decl "[bool, bool -> bool]" booleans nil) (IntervalExpr type-decl nil IntervalExpr_adt nil) (const? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (varidx? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (add? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (abs? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (neg? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sub? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (mult? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sq? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (pow? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (div? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (fun? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (letin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (RealExpr type-eq-decl nil IntervalExpr_adt nil) (<< adt-def-decl "(strict_well_founded?[IntervalExpr])" IntervalExpr_adt nil) (restrict const-decl "R" restrict nil)) nil)) (eval_TCC19 0 (eval_TCC19-1 nil 3546625295 ("" (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) (OR const-decl "[bool, bool -> bool]" booleans nil) (IntervalExpr type-decl nil IntervalExpr_adt nil) (const? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (varidx? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (add? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (abs? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (neg? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sub? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (mult? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sq? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (pow? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (div? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (fun? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (letin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (RealExpr type-eq-decl nil IntervalExpr_adt 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) (>= const-decl "bool" 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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (ge_realorder name-judgement "RealOrder" real_orders "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (/= const-decl "boolean" notequal nil)) nil)) (eval_TCC20 0 (eval_TCC20-1 nil 3546625295 ("" (termination-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) (OR const-decl "[bool, bool -> bool]" booleans nil) (IntervalExpr type-decl nil IntervalExpr_adt nil) (const? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (varidx? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (add? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (abs? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (neg? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sub? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (mult? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sq? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (pow? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (div? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (fun? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (letin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (RealExpr type-eq-decl nil IntervalExpr_adt 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) (>= const-decl "bool" 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) (nat nonempty-type-eq-decl nil naturalnumbers nil)) nil)) (eval_TCC21 0 (eval_TCC21-1 nil 3546625295 ("" (termination-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) (OR const-decl "[bool, bool -> bool]" booleans nil) (IntervalExpr type-decl nil IntervalExpr_adt nil) (const? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (varidx? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (add? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (abs? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (neg? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sub? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (mult? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sq? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (pow? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (div? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (fun? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (letin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (RealExpr type-eq-decl nil IntervalExpr_adt 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) (>= const-decl "bool" 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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (<< adt-def-decl "(strict_well_founded?[IntervalExpr])" IntervalExpr_adt nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (ge_realorder name-judgement "RealOrder" real_orders "reals/") (restrict const-decl "R" restrict nil)) nil)) (eval_TCC22 0 (eval_TCC22-1 nil 3546625295 ("" (termination-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) (OR const-decl "[bool, bool -> bool]" booleans nil) (IntervalExpr type-decl nil IntervalExpr_adt nil) (const? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (varidx? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (add? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (abs? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (neg? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sub? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (mult? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sq? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (pow? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (div? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (fun? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (letin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (RealExpr type-eq-decl nil IntervalExpr_adt 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) (>= const-decl "bool" 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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (<< adt-def-decl "(strict_well_founded?[IntervalExpr])" IntervalExpr_adt nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (ge_realorder name-judgement "RealOrder" real_orders "reals/") (restrict const-decl "R" restrict nil)) nil)) (eval_TCC23 0 (eval_TCC23-1 nil 3546625295 ("" (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) (OR const-decl "[bool, bool -> bool]" booleans nil) (IntervalExpr type-decl nil IntervalExpr_adt nil) (const? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (varidx? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (add? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (abs? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (neg? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sub? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (mult? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sq? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (pow? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (div? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (fun? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (letin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (RealExpr type-eq-decl nil IntervalExpr_adt 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) (>= const-decl "bool" 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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (/= const-decl "boolean" notequal nil)) nil)) (eval_TCC24 0 (eval_TCC24-1 nil 3546625295 ("" (termination-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) (OR const-decl "[bool, bool -> bool]" booleans nil) (IntervalExpr type-decl nil IntervalExpr_adt nil) (const? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (varidx? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (add? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (abs? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (neg? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sub? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (mult? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sq? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (pow? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (div? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (fun? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (letin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (RealExpr type-eq-decl nil IntervalExpr_adt nil)) nil)) (eval_TCC25 0 (eval_TCC25-1 nil 3546710894 ("" (termination-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) (OR const-decl "[bool, bool -> bool]" booleans nil) (IntervalExpr type-decl nil IntervalExpr_adt nil) (const? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (varidx? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (add? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (abs? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (neg? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sub? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (mult? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sq? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (pow? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (div? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (fun? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (letin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (RealExpr type-eq-decl nil IntervalExpr_adt nil) (<< adt-def-decl "(strict_well_founded?[IntervalExpr])" IntervalExpr_adt nil) (restrict const-decl "R" restrict nil)) nil)) (eval_TCC26 0 (eval_TCC26-1 nil 3546710894 ("" (termination-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) (OR const-decl "[bool, bool -> bool]" booleans nil) (IntervalExpr type-decl nil IntervalExpr_adt nil) (const? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (varidx? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (add? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (abs? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (neg? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sub? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (mult? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sq? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (pow? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (div? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (fun? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (letin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (RealExpr type-eq-decl nil IntervalExpr_adt nil)) nil)) (eval_TCC27 0 (eval_TCC27-1 nil 3568989877 ("" (termination-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) (OR const-decl "[bool, bool -> bool]" booleans nil) (IntervalExpr type-decl nil IntervalExpr_adt nil) (const? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (varidx? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (add? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (abs? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (neg? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sub? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (mult? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sq? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (pow? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (div? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (fun? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (letin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (RealExpr type-eq-decl nil IntervalExpr_adt nil) (<< adt-def-decl "(strict_well_founded?[IntervalExpr])" IntervalExpr_adt nil) (restrict const-decl "R" restrict nil)) nil)) (eval_TCC28 0 (eval_TCC28-1 nil 3580034334 ("" (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) (OR const-decl "[bool, bool -> bool]" booleans nil) (IntervalExpr type-decl nil IntervalExpr_adt nil) (const? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (varidx? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (add? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (abs? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (neg? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sub? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (mult? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sq? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (pow? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (div? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (fun? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (letin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (RealExpr type-eq-decl nil IntervalExpr_adt 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) (>= const-decl "bool" 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) (nat nonempty-type-eq-decl nil naturalnumbers nil)) nil)) (eval_TCC29 0 (eval_TCC29-1 nil 3580034334 ("" (termination-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) (OR const-decl "[bool, bool -> bool]" booleans nil) (IntervalExpr type-decl nil IntervalExpr_adt nil) (const? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (varidx? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (add? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (abs? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (neg? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sub? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (mult? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sq? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (pow? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (div? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (fun? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (letin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (RealExpr type-eq-decl nil IntervalExpr_adt 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) (>= const-decl "bool" 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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (<< adt-def-decl "(strict_well_founded?[IntervalExpr])" IntervalExpr_adt nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (ge_realorder name-judgement "RealOrder" real_orders "reals/") (restrict const-decl "R" restrict nil)) nil)) (eval_TCC30 0 (eval_TCC30-1 nil 3580034334 ("" (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) (OR const-decl "[bool, bool -> bool]" booleans nil) (IntervalExpr type-decl nil IntervalExpr_adt nil) (const? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (varidx? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (add? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (abs? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (neg? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sub? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (mult? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sq? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (pow? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (div? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (fun? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (letin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (RealExpr type-eq-decl nil IntervalExpr_adt nil)) nil)) (eval_TCC31 0 (eval_TCC31-1 nil 3580034334 ("" (termination-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) (OR const-decl "[bool, bool -> bool]" booleans nil) (IntervalExpr type-decl nil IntervalExpr_adt nil) (const? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (varidx? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (add? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (abs? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (neg? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sub? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (mult? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sq? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (pow? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (div? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (fun? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (letin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (RealExpr type-eq-decl nil IntervalExpr_adt nil) (<< adt-def-decl "(strict_well_founded?[IntervalExpr])" IntervalExpr_adt nil) (restrict const-decl "R" restrict nil)) nil)) (Eval_TCC1 0 (Eval_TCC1-1 nil 3546624714 ("" (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) (OR const-decl "[bool, bool -> bool]" booleans nil) (IntervalExpr type-decl nil IntervalExpr_adt nil) (const? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (varidx? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (add? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (abs? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (neg? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sub? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (mult? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sq? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (pow? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (div? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (fun? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (letin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (RealExpr type-eq-decl nil IntervalExpr_adt nil) (ge_realorder name-judgement "RealOrder" real_orders "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (lt_realorder name-judgement "RealOrder" real_orders "reals/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (Eval_TCC2 0 (Eval_TCC2-1 nil 3546624714 ("" (grind) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (IntervalExpr type-decl nil IntervalExpr_adt nil) (const? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (varidx? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (add? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (abs? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (neg? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sub? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (mult? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sq? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (pow? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (div? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (fun? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (letin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (RealExpr type-eq-decl nil IntervalExpr_adt nil) (<< adt-def-decl "(strict_well_founded?[IntervalExpr])" IntervalExpr_adt nil) (restrict const-decl "R" restrict nil)) nil)) (Eval_TCC3 0 (Eval_TCC3-1 nil 3580034334 ("" (termination-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) (OR const-decl "[bool, bool -> bool]" booleans nil) (IntervalExpr type-decl nil IntervalExpr_adt nil) (const? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (varidx? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (add? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (abs? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (neg? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sub? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (mult? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sq? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (pow? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (div? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (fun? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (letin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (RealExpr type-eq-decl nil IntervalExpr_adt nil) (<< adt-def-decl "(strict_well_founded?[IntervalExpr])" IntervalExpr_adt nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (le_realorder name-judgement "RealOrder" real_orders "reals/") (Proper? const-decl "bool" interval nil) (restrict const-decl "R" restrict nil)) nil)) (well_typed?_TCC1 0 (well_typed?_TCC1-1 nil 3576776063 ("" (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) (OR const-decl "[bool, bool -> bool]" booleans nil) (IntervalExpr type-decl nil IntervalExpr_adt nil) (const? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (varidx? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (add? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (abs? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (neg? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sub? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (mult? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sq? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (pow? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (div? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (fun? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (letin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (RealExpr type-eq-decl nil IntervalExpr_adt nil)) nil)) (well_typed?_TCC2 0 (well_typed?_TCC2-1 nil 3576776063 ("" (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) (OR const-decl "[bool, bool -> bool]" booleans nil) (IntervalExpr type-decl nil IntervalExpr_adt nil) (const? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (varidx? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (add? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (abs? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (neg? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sub? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (mult? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sq? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (pow? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (div? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (fun? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (letin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (RealExpr type-eq-decl nil IntervalExpr_adt nil)) nil)) (well_typed?_TCC3 0 (well_typed?_TCC3-1 nil 3576776063 ("" (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) (OR const-decl "[bool, bool -> bool]" booleans nil) (IntervalExpr type-decl nil IntervalExpr_adt nil) (const? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (varidx? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (add? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (abs? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (neg? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sub? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (mult? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sq? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (pow? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (div? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (fun? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (letin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (RealExpr type-eq-decl nil IntervalExpr_adt nil)) nil)) (well_typed?_TCC4 0 (well_typed?_TCC4-1 nil 3576776063 ("" (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) (OR const-decl "[bool, bool -> bool]" booleans nil) (IntervalExpr type-decl nil IntervalExpr_adt nil) (const? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (varidx? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (add? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (abs? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (neg? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sub? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (mult? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sq? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (pow? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (div? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (fun? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (letin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (RealExpr type-eq-decl nil IntervalExpr_adt nil)) nil)) (well_typed?_TCC5 0 (well_typed?_TCC5-1 nil 3576776063 ("" (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) (OR const-decl "[bool, bool -> bool]" booleans nil) (IntervalExpr type-decl nil IntervalExpr_adt nil) (const? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (varidx? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (add? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (abs? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (neg? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sub? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (mult? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sq? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (pow? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (div? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (fun? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (letin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (RealExpr type-eq-decl nil IntervalExpr_adt nil)) nil)) --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.29 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.Bot Zugriff |
