| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/interval_arith/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 136 kB |
|
SSL interval_bexpr.prfSprache: Lisp |
|||||||||||||||
|
(interval_bexpr (beval_TCC1 0 (beval_TCC1-1 nil 3568996631 ("" (lemma "well_founded_restrict[IntervalExpr,BoolExpr]") (("" (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) (bconst? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bnot? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (band? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bor? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bimplies? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (brel? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bincludes? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bite? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bletin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (BoolExpr type-eq-decl nil IntervalExpr_adt nil)) nil)) (beval_TCC2 0 (beval_TCC2-1 nil 3568996631 ("" (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) (bconst? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bnot? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (band? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bor? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bimplies? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (brel? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bincludes? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bite? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bletin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (BoolExpr type-eq-decl nil IntervalExpr_adt nil) (<< adt-def-decl "(strict_well_founded?[IntervalExpr])" IntervalExpr_adt nil) (restrict const-decl "R" restrict nil)) nil)) (beval_TCC3 0 (beval_TCC3-1 nil 3568996631 ("" (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) (bconst? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bnot? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (band? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bor? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bimplies? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (brel? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bincludes? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bite? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bletin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (BoolExpr type-eq-decl nil IntervalExpr_adt nil)) nil)) (beval_TCC4 0 (beval_TCC4-1 nil 3568996631 ("" (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) (bconst? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bnot? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (band? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bor? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bimplies? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (brel? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bincludes? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bite? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bletin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (BoolExpr type-eq-decl nil IntervalExpr_adt nil) (<< adt-def-decl "(strict_well_founded?[IntervalExpr])" IntervalExpr_adt nil) (restrict const-decl "R" restrict nil)) nil)) (beval_TCC5 0 (beval_TCC5-1 nil 3568996631 ("" (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) (bconst? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bnot? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (band? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bor? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bimplies? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (brel? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bincludes? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bite? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bletin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (BoolExpr 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) (<< adt-def-decl "(strict_well_founded?[IntervalExpr])" IntervalExpr_adt nil) (restrict const-decl "R" restrict nil)) nil)) (beval_TCC6 0 (beval_TCC6-1 nil 3568996631 ("" (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) (bconst? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bnot? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (band? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bor? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bimplies? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (brel? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bincludes? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bite? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bletin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (BoolExpr type-eq-decl nil IntervalExpr_adt nil)) nil)) (beval_TCC7 0 (beval_TCC7-1 nil 3568996631 ("" (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) (bconst? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bnot? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (band? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bor? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bimplies? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (brel? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bincludes? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bite? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bletin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (BoolExpr type-eq-decl nil IntervalExpr_adt nil) (<< adt-def-decl "(strict_well_founded?[IntervalExpr])" IntervalExpr_adt nil) (restrict const-decl "R" restrict nil)) nil)) (beval_TCC8 0 (beval_TCC8-1 nil 3568996631 ("" (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) (bconst? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bnot? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (band? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bor? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bimplies? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (brel? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bincludes? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bite? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bletin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (BoolExpr 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) (<< adt-def-decl "(strict_well_founded?[IntervalExpr])" IntervalExpr_adt nil) (restrict const-decl "R" restrict nil)) nil)) (beval_TCC9 0 (beval_TCC9-1 nil 3568996631 ("" (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) (bconst? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bnot? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (band? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bor? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bimplies? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (brel? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bincludes? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bite? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bletin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (BoolExpr type-eq-decl nil IntervalExpr_adt nil)) nil)) (beval_TCC10 0 (beval_TCC10-1 nil 3568996631 ("" (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) (bconst? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bnot? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (band? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bor? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bimplies? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (brel? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bincludes? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bite? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bletin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (BoolExpr type-eq-decl nil IntervalExpr_adt nil) (<< adt-def-decl "(strict_well_founded?[IntervalExpr])" IntervalExpr_adt nil) (restrict const-decl "R" restrict nil)) nil)) (beval_TCC11 0 (beval_TCC11-1 nil 3568996631 ("" (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) (bconst? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bnot? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (band? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bor? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bimplies? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (brel? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bincludes? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bite? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bletin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (BoolExpr 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) (<< adt-def-decl "(strict_well_founded?[IntervalExpr])" IntervalExpr_adt nil) (restrict const-decl "R" restrict nil)) nil)) (beval_TCC12 0 (beval_TCC12-1 nil 3568996631 ("" (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) (bconst? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bnot? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (band? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bor? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bimplies? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (brel? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bincludes? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bite? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bletin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (BoolExpr type-eq-decl nil IntervalExpr_adt nil)) nil)) (beval_TCC13 0 (beval_TCC13-1 nil 3569606887 ("" (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) (bconst? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bnot? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (band? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bor? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bimplies? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (brel? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bincludes? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bite? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bletin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (BoolExpr type-eq-decl nil IntervalExpr_adt nil)) nil)) (beval_TCC14 0 (beval_TCC14-1 nil 3569606887 ("" (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) (bconst? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bnot? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (band? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bor? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bimplies? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (brel? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bincludes? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bite? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bletin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (BoolExpr 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/") (realexpr? const-decl "bool" interval_expr nil) (restrict const-decl "R" restrict nil)) nil)) (beval_TCC15 0 (beval_TCC15-1 nil 3576871852 ("" (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) (bconst? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bnot? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (band? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bor? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bimplies? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (brel? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bincludes? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bite? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bletin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (BoolExpr type-eq-decl nil IntervalExpr_adt nil) (realexpr? const-decl "bool" interval_expr nil)) nil)) (beval_TCC16 0 (beval_TCC16-1 nil 3576871852 ("" (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) (bconst? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bnot? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (band? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bor? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bimplies? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (brel? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bincludes? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bite? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bletin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (BoolExpr 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/") (realexpr? const-decl "bool" interval_expr nil) (restrict const-decl "R" restrict nil)) nil)) (beval_TCC17 0 (beval_TCC17-1 nil 3576871852 ("" (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) (bconst? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bnot? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (band? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bor? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bimplies? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (brel? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bincludes? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bite? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bletin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (BoolExpr type-eq-decl nil IntervalExpr_adt nil) (realexpr? const-decl "bool" interval_expr nil)) nil)) (beval_TCC18 0 (beval_TCC18-1 nil 3577463524 ("" (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) (bconst? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bnot? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (band? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bor? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bimplies? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (brel? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bincludes? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bite? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bletin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (BoolExpr type-eq-decl nil IntervalExpr_adt nil) (<< adt-def-decl "(strict_well_founded?[IntervalExpr])" IntervalExpr_adt nil) (realexpr? const-decl "bool" interval_expr nil) (restrict const-decl "R" restrict nil)) nil)) (beval_TCC19 0 (beval_TCC19-1 nil 3577463524 ("" (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) (bconst? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bnot? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (band? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bor? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bimplies? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (brel? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bincludes? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bite? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bletin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (BoolExpr type-eq-decl nil IntervalExpr_adt nil)) nil)) (beval_TCC20 0 (beval_TCC20-1 nil 3577463524 ("" (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) (bconst? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bnot? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (band? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bor? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bimplies? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (brel? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bincludes? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bite? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bletin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (BoolExpr type-eq-decl nil IntervalExpr_adt nil) (<< adt-def-decl "(strict_well_founded?[IntervalExpr])" IntervalExpr_adt nil) (restrict const-decl "R" restrict nil)) nil)) (beval_TCC21 0 (beval_TCC21-1 nil 3577463524 ("" (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) (bconst? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bnot? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (band? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bor? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bimplies? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (brel? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bincludes? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bite? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bletin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (BoolExpr 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) (<< adt-def-decl "(strict_well_founded?[IntervalExpr])" IntervalExpr_adt nil) (restrict const-decl "R" restrict nil)) nil)) (beval_TCC22 0 (beval_TCC22-1 nil 3577463524 ("" (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) (bconst? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bnot? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (band? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bor? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bimplies? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (brel? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bincludes? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bite? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bletin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (BoolExpr 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) (<< adt-def-decl "(strict_well_founded?[IntervalExpr])" IntervalExpr_adt nil) (restrict const-decl "R" restrict nil)) nil)) (BEval_TCC1 0 (BEval_TCC1-2 nil 3569607328 ("" (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) (bconst? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bnot? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (band? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bor? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bimplies? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (brel? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bincludes? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bite? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bletin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (BoolExpr type-eq-decl nil IntervalExpr_adt nil)) nil) (BEval_TCC1-1 nil 3568996631 ("" (termination-tcc) nil nil) ((IntervalExpr type-decl nil IntervalExpr_adt nil) (bconst? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (band? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bor? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bimplies? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (brel? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (BoolExpr type-eq-decl nil IntervalExpr_adt nil) (<< adt-def-decl "(strict_well_founded?[IntervalExpr])" IntervalExpr_adt nil)) nil)) (BEval_TCC2 0 (BEval_TCC2-1 nil 3568996631 ("" (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) (bconst? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bnot? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (band? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bor? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bimplies? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (brel? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bincludes? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bite? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bletin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (BoolExpr type-eq-decl nil IntervalExpr_adt nil)) nil)) (BEval_TCC3 0 (BEval_TCC3-1 nil 3568996631 ("" (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) (bconst? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bnot? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (band? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bor? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bimplies? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (brel? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bincludes? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bite? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bletin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (BoolExpr type-eq-decl nil IntervalExpr_adt nil) (<< adt-def-decl "(strict_well_founded?[IntervalExpr])" IntervalExpr_adt nil) (restrict const-decl "R" restrict nil)) nil)) (BEval_TCC4 0 (BEval_TCC4-1 nil 3569002381 ("" (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) (bconst? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bnot? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (band? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bor? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bimplies? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (brel? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bincludes? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bite? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bletin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (BoolExpr type-eq-decl nil IntervalExpr_adt nil)) nil)) (BEval_TCC5 0 (BEval_TCC5-1 nil 3569002381 ("" (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) (bconst? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bnot? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (band? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bor? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bimplies? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (brel? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bincludes? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bite? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bletin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (BoolExpr type-eq-decl nil IntervalExpr_adt nil) (<< adt-def-decl "(strict_well_founded?[IntervalExpr])" IntervalExpr_adt nil) (restrict const-decl "R" restrict nil)) nil)) (BEval_TCC6 0 (BEval_TCC6-1 nil 3569002381 ("" (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) (bconst? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bnot? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (band? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bor? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bimplies? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (brel? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bincludes? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bite? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bletin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (BoolExpr type-eq-decl nil IntervalExpr_adt nil)) nil)) (BEval_TCC7 0 (BEval_TCC7-1 nil 3576797914 ("" (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) (bconst? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bnot? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (band? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bor? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bimplies? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (brel? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bincludes? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bite? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bletin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (BoolExpr type-eq-decl nil IntervalExpr_adt nil) (<< adt-def-decl "(strict_well_founded?[IntervalExpr])" IntervalExpr_adt nil) (restrict const-decl "R" restrict nil)) nil)) (BEval_TCC8 0 (BEval_TCC8-1 nil 3576871852 ("" (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) (bconst? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bnot? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (band? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bor? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bimplies? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (brel? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bincludes? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bite? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bletin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (BoolExpr 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/") (realexpr? const-decl "bool" interval_expr nil) (Proper? const-decl "bool" interval nil) (restrict const-decl "R" restrict nil)) nil)) (BEval_TCC9 0 (BEval_TCC9-1 nil 3576871852 ("" (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) (bconst? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bnot? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (band? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bor? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bimplies? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (brel? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bincludes? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bite? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bletin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (BoolExpr type-eq-decl nil IntervalExpr_adt nil) (realexpr? const-decl "bool" interval_expr nil)) nil)) (BEval_TCC10 0 (BEval_TCC10-1 nil 3576871852 ("" (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) (bconst? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bnot? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (band? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bor? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bimplies? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (brel? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bincludes? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bite? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bletin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (BoolExpr type-eq-decl nil IntervalExpr_adt nil) (<< adt-def-decl "(strict_well_founded?[IntervalExpr])" IntervalExpr_adt nil) (realexpr? const-decl "bool" interval_expr nil) (restrict const-decl "R" restrict nil)) nil)) (BEval_TCC11 0 (BEval_TCC11-1 nil 3577234317 ("" (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) (bconst? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bnot? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (band? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bor? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bimplies? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (brel? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bincludes? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bite? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bletin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (BoolExpr type-eq-decl nil IntervalExpr_adt nil) (<< adt-def-decl "(strict_well_founded?[IntervalExpr])" IntervalExpr_adt nil) (restrict const-decl "R" restrict nil)) nil)) (BEval_TCC12 0 (BEval_TCC12-1 nil 3577463524 ("" (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) (bconst? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bnot? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (band? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bor? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bimplies? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (brel? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bincludes? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bite? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bletin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (BoolExpr type-eq-decl nil IntervalExpr_adt nil) (<< adt-def-decl "(strict_well_founded?[IntervalExpr])" IntervalExpr_adt nil) (restrict const-decl "R" restrict nil)) nil)) (BEval_TCC13 0 (BEval_TCC13-1 nil 3577463524 ("" (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) (bconst? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bnot? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (band? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bor? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bimplies? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (brel? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bincludes? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bite? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bletin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (BoolExpr type-eq-decl nil IntervalExpr_adt nil) (<< adt-def-decl "(strict_well_founded?[IntervalExpr])" IntervalExpr_adt nil) (restrict const-decl "R" restrict nil)) nil)) (BEval_TCC14 0 (BEval_TCC14-1 nil 3577487424 ("" (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) (bconst? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bnot? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (band? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bor? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bimplies? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (brel? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bincludes? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bite? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bletin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (BoolExpr type-eq-decl nil IntervalExpr_adt nil) (<< adt-def-decl "(strict_well_founded?[IntervalExpr])" IntervalExpr_adt nil) (restrict const-decl "R" restrict nil)) nil)) (BEval_inclusion 0 (BEval_inclusion-1 nil 3568996643 ("" (induct "bexpr") (("1" (assert) nil nil) ("2" (typepred "bexpr!1") (("2" (assert) nil nil)) nil) ("3" (assert) nil nil) ("4" (assert) nil nil) ("5" (assert) nil nil) ("6" (assert) nil nil) ("7" (assert) nil nil) ("8" (assert) nil nil) ("9" (assert) nil nil) ("10" (assert) nil nil) ("11" (assert) nil nil) ("12" (assert) nil nil) ("13" (assert) nil nil) ("14" (assert) nil nil) ("15" (skeep) (("15" (hide -1) (("15" (expand* "BEval" "beval") nil nil)) nil)) nil) ("16" (skolem 1 "be" :skolem-typepreds? t) (("16" (replaces -) (("16" (flatten) (("16" (skeep) (("16" (insteep -) (("16" (expand "beval" 1) (("16" (expand "BEval" (-2 1)) (("16" (lift-if) (("16" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("17" (skolem 1 ("be1" "be2") :skolem-typepreds? t) (("17" (replaces -) (("17" (flatten) (("17" (skeep) (("17" (insteep -) (("17" (insteep -) (("17" (expand "beval" 1) (("17" (expand "BEval" (-3 1)) (("17" (lift-if) (("17" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("18" (skolem 1 ("be1" "be2") :skolem-typepreds? t) (("18" (replaces -) (("18" (flatten) (("18" (skeep) (("18" (insteep -) (("18" (insteep -) (("18" (expand "beval" 1) (("18" (expand "BEval" (-3 1)) (("18" (lift-if) (("18" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("19" (skolem 1 ("be1" "be2") :skolem-typepreds? t) (("19" (replaces -) (("19" (flatten) (("19" (skeep) (("19" (insteep -) (("19" (insteep -) (("19" (expand "beval" 1) (("19" (expand "BEval" (-3 1)) (("19" (lift-if) (("19" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("20" (skolem 1 ("rel" "r1" "r2")) (("20" (flatten) (("20" (hide (-1 -2 -3)) (("20" (skeep) (("20" (expand "beval") (("20" (expand "BEval") (("20" (case "Proper?(Eval(r1,box)) AND Proper?(Eval(r2,box))") (("1" (flatten) (("1" (assert) (("1" (lemma "Eval_inclusion_Proper") (("1" (copy -1) (("1" (inst? -1 :where -3) (("1" (inst? -1) (("1" (inst? -2 :where -4) (("1" (inst? -2) (("1" (assert) (("1" (typepred "rel") (("1" (case "rel(0,1)") (("1" (assert) (("1" (lift-if 1) (("1" (split) (("1" (flatten) (("1" (assert) (("1" (grind :exclude ("Eval" "eval")) nil nil)) nil)) nil) ("2" (flatten) (("2" (assert) (("2" (split 2) (("1" (flatten) (("1" (assert) (("1" (grind :exclude ("Eval" "eval")) nil nil)) nil)) nil) ("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (lift-if 2) (("2" (split) (("1" (flatten) (("1" (assert) (("1" (grind :exclude ("Eval" "eval")) nil nil)) nil)) nil) ("2" (flatten) (("2" (assert) (("2" (split) (("1" (flatten) (("1" (assert) (("1" (grind :exclude ("Eval" "eval")) nil nil)) nil)) nil) ("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("21" (skolem 1 ("r" "R")) (("21" (flatten) (("21" (hide -1 -2) (("21" (skeep) (("21" (expand "beval") (("21" (expand "BEval") (("21" (case "Proper?(Eval(r,box)) AND Proper?(R)") (("1" (flatten) (("1" (assert) (("1" (lemma "Eval_inclusion_Proper") (("1" (inst? -1) (("1" (assert) (("1" (case "Eval(r, box) << R") (("1" (assert) (("1" (grind :exclude ("Eval" "eval")) nil nil)) nil) ("2" (assert) (("2" (lift-if 2) (("2" (split 2) (("1" (flatten) (("1" (assert) (("1" (replace -1) (("1" (grind :exclude ("Eval" "eval")) nil nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("22" (skolem 1 ("be1" "be2" "b3") :skolem-typepreds? t) (("22" (replaces -) (("22" (flatten) (("22" (skeep) (("22" (insteep -) (("22" (insteep -) (("22" (insteep -) (("22" (expand "beval" 1) (("22" (expand "BEval" (-4 1)) (("22" (case-replace "some?(BEval(be1, box))") (("1" (lift-if) (("1" (ground) nil nil)) nil) ("2" (replace 1) (("2" (lift-if) (("2" (ground) (("2" (assert) (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("23" (skolem 1 ("blet" "bin") :skolem-typepreds? t) (("23" (replaces -) (("23" (flatten) (("23" (skeep) (("23" (case "realexpr?(blet)") (("1" (hide -2) (("1" (expand "beval" 1) (("1" (expand "BEval" (-3 1)) (("1" (replace -1) (("1" (lift-if) (("1" (case-replace "Proper?(Eval(blet, box))") (("1" (inst? -) (("1" (case "length(append(box, (: Eval(blet, box) :))) = length(box) + 1") (("1" (inst -4 "vs WITH [(length(box)) := eval(blet, vs,length(box))]") (("1" (assert) nil nil) ("2" (hide -4 2) (("2" (typepred "vs") (("2" (expand "vars_in_box?") (("2" (skeep :preds? t) (("2" (replace -3) (("2" (case-replace "i=length(box)") (("1" (assert) (("1" (rewrite "nth_append") (("1" (expand "nth" 1) (("1" (lemma "Eval_inclusion_Proper") (("1" (inst? -1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (inst? -2) (("2" (rewrite "nth_append") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (rewrite "length_append") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil) ("3" (expand "realexpr?") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "real_bool_expr") (("2" (inst?) (("2" (assert) (("2" (expand "boolexpr?") (("2" (replace -1) (("2" (expand "beval" 2) (("2" (expand "BEval" (-4 2)) (("2" (name-replace "nbox" "append(box, (: IF none?(BEval(blet, box)) THEN [|-1, 1|] ELSIF val(BEval(blet, box)) THEN [|1/2, 1|] ELSE [|-1, -1 / 2|] ENDIF :))" :hide? nil) (("1" (case "length(nbox) = 1+length(box)") (("1" (inst? -5) (("1" (inst -5 "vs WITH [(length(box)) := IF beval(blet, vs, length(box)) THEN 1 ELSE -1 ENDIF]") (("1" (assert) (("1" (replace -1) (("1" (propax) nil nil)) nil)) nil) ("2" (hide 3) (("2" (typepred "vs") (("2" (expand "vars_in_box?") (("2" (skeep :preds? t) (("2" (replace -3) (("2" (case-replace "i=length(box)") (("1" (assert) (("1" (replaces -5 :dir rl) (("1" (rewrite "nth_append") (("1" (expand "nth" 1) (("1" (insteep -6) (("1" (case-replace "some?(BEval(blet, box))") (("1" (assert) (("1" (replaces -7) (("1" (hide-all-but 1) (("1" (grind :exclude "beval") nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (hide-all-but 2) (("2" (grind :exclude "beval") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) nil nil)) nil) ("3" (flatten) (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (inst? -2) (("2" (replaces -4 :dir rl) (("2" (rewrite "nth_append") (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replaces -1 :dir rl) (("2" (rewrite "length_append") (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) nil nil)) nil) ("3" (flatten) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((realexpr? const-decl "bool" interval_expr nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (nth def-decl "T" list_props nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (length_singleton formula-decl nil more_list_props "structures/") (int_minus_int_is_int application-judgement "int" integers nil) (nth_append formula-decl nil more_list_props "structures/") (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (eval def-decl "real" interval_expr nil) (vs skolem-const-decl "(vars_in_box?(box))" interval_bexpr nil) (blet skolem-const-decl "IntervalExpr" interval_bexpr nil) (box skolem-const-decl "Box" interval_bexpr nil) (length_append formula-decl nil list_props nil) (append def-decl "list[T]" list_props nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (null adt-constructor-decl "(null?)" list_adt nil) (boolexpr? const-decl "bool" interval_expr nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (- const-decl "[numfield -> numfield]" number_fields nil) ([\|\|] const-decl "Interval" interval nil) (none? adt-recognizer-decl "[Maybe -> boolean]" Maybe "structures/") (IF const-decl "[boolean, T, T -> T]" if_def nil) (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (nbox skolem-const-decl "list[Interval]" interval_bexpr nil) (real_bool_expr formula-decl nil interval_expr nil) (<< const-decl "bool" interval nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (Proper? const-decl "bool" interval 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) (Eval def-decl "Interval" interval_expr nil) (realorder? const-decl "bool" real_orders "reals/") (RealOrder type-eq-decl nil real_orders "reals/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (gt_realorder name-judgement "RealOrder" real_orders "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (ge_realorder name-judgement "RealOrder" real_orders "reals/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (lt_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/") (|##| const-decl "bool" interval nil) (neg_rel_order application-judgement "RealOrder" real_orders "reals/") (neg_rel const-decl "bool" real_orders "reals/") (Eval_inclusion_Proper formula-decl nil interval_expr nil) (NOT const-decl "[bool -> bool]" booleans nil) (IntervalExpr_induction formula-decl nil IntervalExpr_adt nil) (BEval def-decl "Maybe[bool]" interval_bexpr nil) (length def-decl "nat" list_props nil) (beval def-decl "bool" interval_bexpr nil) (BoolExpr type-eq-decl nil IntervalExpr_adt nil) (val adt-accessor-decl "[(some?) -> T]" Maybe "structures/") (= const-decl "[T, T -> boolean]" equalities nil) (some? adt-recognizer-decl "[Maybe -> boolean]" Maybe "structures/") (Maybe type-decl nil Maybe "structures/") (vars_in_box? const-decl "bool" box nil) (Env type-eq-decl nil box 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) (Box type-eq-decl nil box nil) (list type-decl nil list_adt nil) (Interval type-eq-decl nil interval nil) (real nonempty-type-from-decl nil reals nil) (bletin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bite? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bincludes? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (brel? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bimplies? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bor? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (band? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bnot? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bconst? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (IntervalExpr type-decl nil IntervalExpr_adt nil)) shostak)) (BEval_inclusion_Proper 0 (BEval_inclusion_Proper-1 nil 3576919950 ("" (skeep) (("" (beta) (("" (flatten) (("" (iff) (("" (lemma "BEval_inclusion") (("" (inst -1 "pox" _ "bexpr") (("" (split) (("1" (flatten) (("1" (skeep) (("1" (inst? -) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) (("2" (inst -1 "midvars(pox)") (("2" (inst -2 "midvars(pox)") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real nonempty-type-from-decl nil reals nil) (Interval type-eq-decl nil interval nil) (list type-decl nil list_adt nil) (Box type-eq-decl nil box nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (ProperBox? const-decl "bool" box nil) (ProperBox type-eq-decl nil box nil) (IntervalExpr type-decl nil IntervalExpr_adt nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (bconst? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bnot? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (band? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bor? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bimplies? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (brel? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bincludes? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bite? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bletin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (BoolExpr type-eq-decl nil IntervalExpr_adt nil) (midvars const-decl "(vars_in_box?(pox))" box nil) (vars_in_box? const-decl "bool" box nil) (Env type-eq-decl nil box 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) (BEval_inclusion formula-decl nil interval_bexpr nil)) nil)) (BEval_fundamental 0 (BEval_fundamental-2 nil 3576854177 ("" (induct "bexpr") (("1" (assert) nil nil) ("2" (typepred "bexpr!1") (("2" (assert) nil nil)) nil) ("3" (assert) nil nil) ("4" (assert) nil nil) ("5" (assert) nil nil) ("6" (assert) nil nil) ("7" (assert) nil nil) ("8" (assert) nil nil) ("9" (assert) nil nil) ("10" (assert) nil nil) ("11" (assert) nil nil) ("12" (assert) nil nil) ("13" (assert) nil nil) ("14" (assert) nil nil) ("15" (skeep) (("15" (hide -1) (("15" (skeep) (("15" (expand "BEval") (("15" (propax) nil nil)) nil)) nil)) nil)) nil) ("16" (skolem 1 "be" :skolem-typepreds? t) (("16" (replaces -1) (("16" (flatten) (("16" (skeep) (("16" (insteep -) (("16" (assert) (("16" (expand "BEval" (-3 1)) (("16" (lift-if) (("16" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("17" (skolem 1 ("be1" "be2") :skolem-typepreds? t) (("17" (replaces (-1 -2)) (("17" (flatten) (("17" (skeep) (("17" (insteep -) (("17" (insteep -) (("17" (assert) (("17" (expand "BEval" (-4 1)) (("17" (lift-if) (("17" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("18" (skolem 1 ("be1" "be2") :skolem-typepreds? t) (("18" (replaces (-1 -2)) (("18" (flatten) (("18" (skeep) (("18" (insteep -) (("18" (insteep -) (("18" (expand "BEval" (-4 1)) (("18" (lift-if) (("18" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("19" (skolem 1 ("be1" "be2") :skolem-typepreds? t) (("19" (replaces (-1 -2)) (("19" (flatten) (("19" (skeep) (("19" (insteep -) (("19" (insteep -) (("19" (assert) (("19" (expand "BEval" (-4 1)) (("19" (lift-if) (("19" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("20" (skolem 1 ("rel" "r1" "r2")) (("20" (flatten) (("20" (hide -) (("20" (skeep) (("20" (name-replace "beb" "BEval(BREL(rel, r1, r2), box)" :hide? nil) (("20" (name-replace "bep" "BEval(BREL(rel, r1, r2), pox)" :hide? nil) (("20" (lemma "Proper_Inclusion") (("20" (inst?) (("20" (assert) (("20" (expand "BEval") (("20" (case "Proper?(Eval(r1,box))") (("1" (assert) (("1" (copy -2) (("1" (inst? -) (("1" (assert) (("1" (case "Proper?(Eval(r2,box))") (("1" (assert) (("1" (inst? - :where -1) (("1" (assert) (("1" (typepred "rel") (("1" (lemma "Eval_fundamental_proper") (("1" (inst?) (("1" (assert) (("1" (copy -1) (("1" (inst? -1 :where -6) (("1" (inst? -2 :where -4) (("1" (assert) (("1" (hide -11) (("1" (grind :exclude "Eval") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("21" (skolem 1 ("r" "R")) (("21" (flatten) (("21" (hide -) (("21" (skeep) (("21" (name-replace "bep" "BEval(BINCLUDES(r, R), pox)" :hide? nil) (("21" (name-replace "beb" "BEval(BINCLUDES(r, R), box)" :hide? nil) (("21" (lemma "Proper_Inclusion") (("21" (inst?) (("21" (assert) (("21" (inst?) (("21" (expand "BEval") (("21" (case "Proper?(Eval(r, box))") (("1" (assert) (("1" (case "Proper?(R)") (("1" (assert) (("1" (lemma "Eval_fundamental_proper") (("1" (inst?) (("1" (assert) (("1" (inst?) (("1" (assert) (("1" (hide -8) (("1" (grind :exclude "Eval") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("22" (skolem 1 ("be1" "be2" "be3") :skolem-typepreds? t) (("22" (replaces (-1 -2 -3)) (("22" (flatten) (("22" (skeep) (("22" (insteep -) (("22" (insteep -) (("22" (insteep -) (("22" (assert) (("22" (case "some?(BEval(be1, box))") (("1" (assert) (("1" (flatten) (("1" (expand "BEval" (-7 1)) (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "BEval" (-5 2)) (("2" (assert) (("2" (case "NOT some?(BEval(be1,pox))") (("1" (assert) (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil) ("2" (assert) (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("23" (skolem 1 ("blet" "bin") :skolem-typepreds? t) (("23" (replaces -1) (("23" (flatten) (("23" (skeep) (("23" (lemma "real_bool_expr") (("23" (inst?) (("23" (case "realexpr?(blet)") (("1" (hide -2 -3) (("1" (expand "BEval" (-4 1)) (("1" (assert) (("1" (case-replace "Proper?(Eval(blet, box))") (("1" (lemma "Proper_Inclusion") (("1" (inst? -) (("1" (assert) (("1" (inst?) (("1" (assert) (("1" (inst -4 "append(box, (: Eval(blet, box) :))" "append(pox, (: Eval(blet, pox) :))") (("1" (replace -6) (("1" (replace 1) (("1" (hide 2) (("1" (expand "Inclusion?") (("1" (flatten) (("1" (case "length(append(pox, (: Eval(blet, pox) :))) = length(pox) + 1") (("1" (case "length(append(box, (: Eval(blet, box) :))) = length(box) + 1") (("1" (assert) (("1" (skeep :preds? t) (("1" (replace -3) (("1" (case-replace "i=length(pox)") (("1" (rewrite "nth_append") (("1" (expand "nth" 1 1) (("1" (replace -8) (("1" (rewrite "nth_append") (("1" (expand "nth" 1) (("1" (lemma "Eval_fundamental_proper") (("1" (insteep -) (("1" (assert) (("1" (inst? -) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "nth_append") (("2" (assert) (("2" (rewrite "nth_append") (("2" (insteep -8) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (rewrite "length_append") (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (rewrite "length_append") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -5 2) (("2" (rewrite "proper_append") (("2" (hide 2) (("2" (expand "ProperBox?") (("2" (expand "every") (("2" (expand "every") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil) ("3" (hide 2) (("3" (expand "realexpr?") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "boolexpr?") (("2" (replace -1) (("2" (expand "BEval" (-5 2)) (("2" (name-replace "nbox" "append(box, cons(IF none?(BEval(blet, box)) THEN [|-1, 1|] ELSIF val(BEval(blet, box)) THEN [|1/2, 1|] ELSE [|-1, -1 / 2|] ENDIF, null))" :hide? nil) (("1" (name-replace "npox" "append(pox, cons(IF none?(BEval(blet, pox)) THEN [|-1, 1|] ELSIF val(BEval(blet, pox)) THEN [|1/2, 1|] ELSE [|-1, -1 / 2|] ENDIF, null))" :hide? nil) (("1" (case "length(npox) = 1+length(pox)") (("1" (case "length(nbox) = 1+length(box)") (("1" (insteep -6) (("1" (assert) (("1" (inst -7 "nbox" "npox") (("1" (replace -9) (("1" (replace 2) (("1" (hide 3) (("1" (expand "Inclusion?") (("1" (flatten) (("1" (assert) (("1" (skeep :preds? t) (("1" (case-replace "i=length(pox)") (("1" (replaces (-5 -6) 2 :dir rl :hide? nil) (("1" (rewrite "nth_append") (("1" (expand "nth" 2 1) (("1" (rewrite "nth_append") (("1" (expand "nth" 2 1) (("1" (hide -5 -6) (("1" (case "some?(BEval(blet, box))") (("1" (assert) (("1" (flatten) (("1" (assert) (("1" (replaces -8) (("1" (hide-all-but 2) (("1" (grind :exclude "BEval") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (hide-all-but 3) (("2" (grind :exclude "BEval") nil nil)) nil)) nil) ("3" (propax) nil nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) nil nil)) nil) ("3" (flatten) (("3" (assert) nil nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) nil nil)) nil) ("3" (flatten) (("3" (assert) nil nil)) nil)) nil)) nil) ("2" (replaces (-4 -5) 3 :dir rl :hide? nil) (("2" (rewrite "nth_append") (("1" (assert) (("1" (rewrite "nth_append") (("1" (inst? -9) nil nil) ("2" (flatten) (("2" (assert) nil nil)) nil) ("3" (flatten) (("3" (assert) nil nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) nil nil)) nil) ("3" (flatten) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replaces -3 1 :dir rl) (("2" (rewrite "proper_append") (("1" (hide 2) (("1" (expand "ProperBox?") (("1" (expand "every") (("1" (hide-all-but 1) (("1" (expand "every") (("1" (grind :exclude "BEval") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) nil nil)) nil) ("3" (flatten) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-3 -4 1)) (("2" (replaces -1 :dir rl) (("2" (rewrite "length_append") (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 -3 1)) (("2" (replaces -1 :dir rl) (("2" (rewrite "length_append") (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) nil nil)) nil) ("3" (flatten) (("3" (assert) nil nil)) nil)) nil) ("2" (flatten) (("2" (assert) nil nil)) nil) ("3" (flatten) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real_bool_expr formula-decl nil interval_expr nil) (realexpr? const-decl "bool" interval_expr nil) (append def-decl "list[T]" list_props nil) (pox skolem-const-decl "ProperBox" interval_bexpr nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil) (blet skolem-const-decl "IntervalExpr" interval_bexpr nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (null adt-constructor-decl "(null?)" list_adt nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (length_append formula-decl nil list_props nil) (nth_append formula-decl nil more_list_props "structures/") (int_minus_int_is_int application-judgement "int" integers nil) (length_singleton formula-decl nil more_list_props "structures/") (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nth def-decl "T" list_props nil) (proper_append formula-decl nil box nil) (every adt-def-decl "boolean" list_adt nil) (boolexpr? const-decl "bool" interval_expr nil) (npox skolem-const-decl "list[Interval]" interval_bexpr nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (- const-decl "[numfield -> numfield]" number_fields nil) ([\|\|] const-decl "Interval" interval nil) (none? adt-recognizer-decl "[Maybe -> boolean]" Maybe "structures/") (IF const-decl "[boolean, T, T -> T]" if_def nil) (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (BINCLUDES adt-constructor-decl "[[RealExpr, Interval] -> (bincludes?)]" IntervalExpr_adt nil) (pox skolem-const-decl "ProperBox" interval_bexpr nil) (box skolem-const-decl "Box" interval_bexpr nil) (r skolem-const-decl "RealExpr" interval_bexpr 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) (realorder? const-decl "bool" real_orders "reals/") (RealOrder type-eq-decl nil real_orders "reals/") (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) (BREL adt-constructor-decl "[[RealOrder, RealExpr, RealExpr] -> (brel?)]" IntervalExpr_adt nil) (Proper_Inclusion formula-decl nil interval_expr nil) (Proper? const-decl "bool" interval nil) (Eval def-decl "Interval" interval_expr nil) (Eval_fundamental_proper formula-decl nil interval_expr nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (gt_realorder name-judgement "RealOrder" real_orders "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (ge_realorder name-judgement "RealOrder" real_orders "reals/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (lt_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/") (<< const-decl "bool" interval nil) (neg_rel const-decl "bool" real_orders "reals/") (rational_pred const-decl "[real -> boolean]" rationals nil) (r1 skolem-const-decl "RealExpr" interval_bexpr nil) (box skolem-const-decl "Box" interval_bexpr nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (>= const-decl "bool" reals nil) (< const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (length def-decl "nat" list_props nil) (pox skolem-const-decl "ProperBox" interval_bexpr nil) (below type-eq-decl nil naturalnumbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (IntervalExpr_induction formula-decl nil IntervalExpr_adt nil) (BEval def-decl "Maybe[bool]" interval_bexpr nil) (BoolExpr type-eq-decl nil IntervalExpr_adt nil) (val adt-accessor-decl "[(some?) -> T]" Maybe "structures/") (= const-decl "[T, T -> boolean]" equalities nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (some? adt-recognizer-decl "[Maybe -> boolean]" Maybe "structures/") (Maybe type-decl nil Maybe "structures/") (Inclusion? const-decl "bool" box nil) (ProperBox type-eq-decl nil box nil) (ProperBox? const-decl "bool" box nil) (Box type-eq-decl nil box nil) (list type-decl nil list_adt nil) (Interval type-eq-decl nil interval nil) (real nonempty-type-from-decl nil reals nil) (bletin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bite? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bincludes? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (brel? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bimplies? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bor? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (band? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bnot? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bconst? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (IntervalExpr type-decl nil IntervalExpr_adt nil)) nil)))
¤ 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.0.157Bemerkung: (vorverarbeitet am 2026-05-02) ¤*Bot Zugriff |
|
||||||||||||||
2026-05-26