Quelle interval_bexpr.prf
Sprache: Lisp
(interval_bexprnil 3568996631"" (lemma "well_founded_restrict[IntervalExpr,BoolExpr]" )"" (inst?)"" (expand "well_founded?" ) (("" (propax) nil nil )) nil )) nil ))nil )"(strict_well_founded?[IntervalExpr])" nil )"bool" orders nil )"bool" orders nil )nil defined_types nil )nil restrict_order_props nil )nil IntervalExpr_adt nil )nil booleans nil )nil booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )nil IntervalExpr_adt nil ))nil ))nil 3568996631 ("" (termination-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil IntervalExpr_adt nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )nil IntervalExpr_adt nil )"(strict_well_founded?[IntervalExpr])" nil )"R" restrict nil ))nil ))nil 3568996631 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil IntervalExpr_adt nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )nil IntervalExpr_adt nil ))nil ))nil 3568996631 ("" (termination-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil IntervalExpr_adt nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )nil IntervalExpr_adt nil )"(strict_well_founded?[IntervalExpr])" nil )"R" restrict nil ))nil ))nil 3568996631 ("" (termination-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil IntervalExpr_adt nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )nil IntervalExpr_adt nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"RealOrder" real_orders "reals/" )"(total_order?[real])" nil )"(strict_well_founded?[IntervalExpr])" nil )"R" restrict nil ))nil ))nil 3568996631 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil IntervalExpr_adt nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )nil IntervalExpr_adt nil ))nil ))nil 3568996631 ("" (termination-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil IntervalExpr_adt nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )nil IntervalExpr_adt nil )"(strict_well_founded?[IntervalExpr])" nil )"R" restrict nil ))nil ))nil 3568996631 ("" (termination-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil IntervalExpr_adt nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )nil IntervalExpr_adt nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"RealOrder" real_orders "reals/" )"(total_order?[real])" nil )"(strict_well_founded?[IntervalExpr])" nil )"R" restrict nil ))nil ))nil 3568996631 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil IntervalExpr_adt nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )nil IntervalExpr_adt nil ))nil ))nil 3568996631 ("" (termination-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil IntervalExpr_adt nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )nil IntervalExpr_adt nil )"(strict_well_founded?[IntervalExpr])" nil )"R" restrict nil ))nil ))nil 3568996631 ("" (termination-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil IntervalExpr_adt nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )nil IntervalExpr_adt nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"RealOrder" real_orders "reals/" )"(total_order?[real])" nil )"(strict_well_founded?[IntervalExpr])" nil )"R" restrict nil ))nil ))nil 3568996631 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil IntervalExpr_adt nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )nil IntervalExpr_adt nil ))nil ))nil 3569606887 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil IntervalExpr_adt nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )nil IntervalExpr_adt nil ))nil ))nil 3569606887 ("" (termination-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil IntervalExpr_adt nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )nil IntervalExpr_adt nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"(strict_well_founded?[IntervalExpr])" nil )"(total_order?[real])" nil )"RealOrder" real_orders "reals/" )"bool" interval_expr nil )"R" restrict nil ))nil ))nil 3576871852 ("" (termination-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil IntervalExpr_adt nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )nil IntervalExpr_adt nil )"bool" interval_expr nil ))nil ))nil 3576871852 ("" (termination-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil IntervalExpr_adt nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )nil IntervalExpr_adt nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"(strict_well_founded?[IntervalExpr])" nil )"(total_order?[real])" nil )"RealOrder" real_orders "reals/" )"bool" interval_expr nil )"R" restrict nil ))nil ))nil 3576871852 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil IntervalExpr_adt nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )nil IntervalExpr_adt nil )"bool" interval_expr nil ))nil ))nil 3577463524 ("" (termination-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil IntervalExpr_adt nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )nil IntervalExpr_adt nil )"(strict_well_founded?[IntervalExpr])" nil )"bool" interval_expr nil )"R" restrict nil ))nil ))nil 3577463524 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil IntervalExpr_adt nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )nil IntervalExpr_adt nil ))nil ))nil 3577463524 ("" (termination-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil IntervalExpr_adt nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )nil IntervalExpr_adt nil )"(strict_well_founded?[IntervalExpr])" nil )"R" restrict nil ))nil ))nil 3577463524 ("" (termination-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil IntervalExpr_adt nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )nil IntervalExpr_adt nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"RealOrder" real_orders "reals/" )"(total_order?[real])" nil )"(strict_well_founded?[IntervalExpr])" nil )"R" restrict nil ))nil ))nil 3577463524 ("" (termination-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil IntervalExpr_adt nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )nil IntervalExpr_adt nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"RealOrder" real_orders "reals/" )"(total_order?[real])" nil )"(strict_well_founded?[IntervalExpr])" nil )"R" restrict nil ))nil ))nil 3569607328 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil IntervalExpr_adt nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )nil IntervalExpr_adt nil ))nil )nil 3568996631 ("" (termination-tcc) nil nil )nil IntervalExpr_adt nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )nil IntervalExpr_adt nil )"(strict_well_founded?[IntervalExpr])" nil ))nil ))nil 3568996631 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil IntervalExpr_adt nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )nil IntervalExpr_adt nil ))nil ))nil 3568996631 ("" (termination-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil IntervalExpr_adt nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )nil IntervalExpr_adt nil )"(strict_well_founded?[IntervalExpr])" nil )"R" restrict nil ))nil ))nil 3569002381 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil IntervalExpr_adt nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )nil IntervalExpr_adt nil ))nil ))nil 3569002381 ("" (termination-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil IntervalExpr_adt nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )nil IntervalExpr_adt nil )"(strict_well_founded?[IntervalExpr])" nil )"R" restrict nil ))nil ))nil 3569002381 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil IntervalExpr_adt nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )nil IntervalExpr_adt nil ))nil ))nil 3576797914 ("" (termination-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil IntervalExpr_adt nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )nil IntervalExpr_adt nil )"(strict_well_founded?[IntervalExpr])" nil )"R" restrict nil ))nil ))nil 3576871852 ("" (termination-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil IntervalExpr_adt nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )nil IntervalExpr_adt nil )"(strict_well_founded?[IntervalExpr])" nil )"(total_order?[real])" nil )"RealOrder" real_orders "reals/" )"bool" interval_expr nil )"bool" interval nil )"R" restrict nil ))nil ))nil 3576871852 ("" (termination-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil IntervalExpr_adt nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )nil IntervalExpr_adt nil )"bool" interval_expr nil ))nil ))nil 3576871852 ("" (termination-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil IntervalExpr_adt nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )nil IntervalExpr_adt nil )"(strict_well_founded?[IntervalExpr])" nil )"bool" interval_expr nil )"R" restrict nil ))nil ))nil 3577234317 ("" (termination-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil IntervalExpr_adt nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )nil IntervalExpr_adt nil )"(strict_well_founded?[IntervalExpr])" nil )"R" restrict nil ))nil ))nil 3577463524 ("" (termination-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil IntervalExpr_adt nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )nil IntervalExpr_adt nil )"(strict_well_founded?[IntervalExpr])" nil )"R" restrict nil ))nil ))nil 3577463524 ("" (termination-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil IntervalExpr_adt nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )nil IntervalExpr_adt nil )"(strict_well_founded?[IntervalExpr])" nil )"R" restrict nil ))nil ))nil 3577487424 ("" (termination-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil IntervalExpr_adt nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )nil IntervalExpr_adt nil )"(strict_well_founded?[IntervalExpr])" nil )"R" restrict nil ))nil ))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" "1" "1" assert )"1" "rel" )"1" case "rel(0,1)" )"1" assert )"1" "1" "1" "1" assert )"1" "Eval" "eval" ))nil nil ))nil ))nil )"2" "2" assert )"2" "1" "1" assert )"1" "Eval" "eval" ))nil nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" "1" "1" assert )"1" "Eval" "eval" ))nil nil ))nil ))nil )"2" "2" assert )"2" "1" "1" assert )"1" "Eval" "eval" ))nil nil ))nil ))nil )"2" "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" "Eval" "eval" ))nil nil ))nil )"2" assert )"2" "2" "1" "1" assert )"1" replace -1)"1" "Eval" "eval" ))nil nil ))nil ))nil ))nil )"2" "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" "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" "vs WITH [(length(box)) := eval(blet, vs,length(box))]" )"1" (assert ) nil nil )"2" "2" "vs" )"2" expand "vars_in_box?" )"2" "2" replace -3)"2" "i=length(box)" )"1" assert )"1" rewrite "nth_append" )"1" expand "nth" 1)"1" "Eval_inclusion_Proper" )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" rewrite "nth_append" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "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" "nbox" "append(box, IF none?(BEval(blet, box)) THEN [|-1, 1|]" :hide? nil) "1" case "length(nbox) = 1+length(box)" )"1" "1" "vs WITH [(length(box)) IF beval(blet, vs, length(box)) THEN 1") "1" assert )"1" replace -1)"1" (propax) nil nil ))nil ))nil )"2" "2" "vs" )"2" expand "vars_in_box?" )"2" "2" replace -3)"2" "i=length(box)" )"1" assert )"1" "1" rewrite "nth_append" )"1" expand "nth" "1" "1" "some?(BEval(blet, box))" )"1" assert )"1" "1" "1" "beval" )nil nil ))nil ))nil ))nil )"2" assert )"2" "2" "beval" )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" "2" rewrite "nth_append" )"1" "1" assert )nil nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "length_append" )"1" "1" (assert ) nil nil ))nil )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" "2" (assert ) nil nil ))nil )"3" "3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" interval_expr nil )"posint" nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"T" list_props nil )"nonneg_int" nil )nil more_list_props "structures/" )"int" integers nil )nil more_list_props "structures/" )"bool" reals nil )nil naturalnumbers nil )"posint" nil )eval def-decl "real" interval_expr nil )"(vars_in_box?(box))" interval_bexpr nil )"IntervalExpr" interval_bexpr nil )"Box" interval_bexpr nil )nil list_props nil )"list[T]" list_props nil )"[list -> boolean]" list_adt nil )"[[T, list] -> (cons?)]" list_adt nil )"[list -> boolean]" list_adt nil )"(null?)" list_adt nil )"bool" interval_expr nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )"[numfield -> numfield]" number_fields nil )"Interval" interval nil )"[Maybe -> boolean]" Maybe"structures/" )IF const-decl "[boolean, T, T -> T]" if_def nil )"nzrat" rationalsnil )"posrat" nil )"odd_int" integers nil )"list[Interval]" interval_bexpr nil )nil interval_expr nil )"bool" interval nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" interval nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )nil IntervalExpr_adt nil )Eval def-decl "Interval" interval_expr nil )"bool" real_orders "reals/" )nil real_orders "reals/" )"(strict_total_order?[real])" real_props nil )"RealOrder" real_orders "reals/" )"(total_order?[real])" nil )"RealOrder" real_orders "reals/" )"(strict_total_order?[real])" real_props nil )"RealOrder" real_orders "reals/" )"(total_order?[real])" nil )"RealOrder" real_orders "reals/" )"bool" interval nil )"RealOrder" real_orders"reals/" )"bool" real_orders "reals/" )nil interval_expr nil )NOT const-decl "[bool -> bool]" booleans nil )nil IntervalExpr_adt nil )"Maybe[bool]" interval_bexpr nil )"nat" list_props nil )"bool" interval_bexpr nil )nil IntervalExpr_adt nil )"[(some?) -> T]" Maybe "structures/" )"[T, T -> boolean]" equalities nil )"[Maybe -> boolean]" Maybe"structures/" )nil Maybe "structures/" )"bool" box nil )nil box nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil box nil ) (list type-decl nil list_adt nil )nil interval nil )nil reals nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil IntervalExpr_adt nil ))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 )nil reals nil )nil interval nil )nil list_adt nil ) (Box type-eq-decl nil box nil )nil booleans nil )nil booleans nil )"bool" box nil )nil box nil )nil IntervalExpr_adt nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )nil IntervalExpr_adt nil )"(vars_in_box?(pox))" box nil )"bool" box nil )nil box nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil interval_bexpr nil ))nil ))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" "beb" "BEval(BREL(rel, r1, r2), box)" nil )"20" "bep" "BEval(BREL(rel, r1, r2), pox)" nil )"20" (lemma "Proper_Inclusion" )"20" (inst?)"20" (assert )"20" (expand "BEval" )"20" (case "Proper?(Eval(r1,box))" )"1" (assert )"1" (copy -2)"1" "1" assert )"1" case "Proper?(Eval(r2,box))" )"1" assert )"1" "1" assert )"1" "rel" )"1" "Eval_fundamental_proper" )"1" "1" assert )"1" "1" "1" "1" assert )"1" "1" "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" "bep" "BEval(BINCLUDES(r, R), pox)" :hide?nil )"21" "beb" "BEval(BINCLUDES(r, R), box)" 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" "Eval_fundamental_proper" )"1" "1" assert )"1" "1" assert )"1" "1" "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" "1" (ground) nil nil ))nil ))nil )"2" (assert )"2" "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" "1" assert )"1" "append(box, (: Eval(blet, box) :))" "append(pox, (: Eval(blet, pox) :))" )"1" replace -6)"1" replace 1)"1" "1" expand "Inclusion?" )"1" "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" "1" replace -3)"1" "i=length(pox)" )"1" rewrite "nth_append" )"1" expand "nth" "1" replace "1" rewrite "nth_append" )"1" expand "nth" "1" "Eval_fundamental_proper" )"1" "1" assert )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" rewrite "nth_append" )"2" assert )"2" rewrite "nth_append" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "length_append" )"2" assert )nil nil ))nil ))nil ))nil )"2" "2" rewrite "length_append" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "proper_append" )"2" "2" expand "ProperBox?" )"2" expand "every" )"2" expand "every" )"2" 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" "nbox" "append(box, IF none?(BEval(blet, box)) THEN [|-1, 1|]" :hide? nil) "1" "npox" "append(pox, IF none?(BEval(blet, pox)) THEN [|-1, 1|]" :hide? nil) "1" case "length(npox) = 1+length(pox)" )"1" case "length(nbox) = 1+length(box)" )"1" "1" assert )"1" "nbox" "npox" )"1" replace -9)"1" replace 2)"1" "1" expand "Inclusion?" )"1" "1" assert )"1" "1" "i=length(pox)" )"1" nil )"1" rewrite "nth_append" )"1" expand "nth" "1" rewrite "nth_append" )"1" expand "nth" "1" "1" case "some?(BEval(blet, box))" )"1" assert )"1" "1" assert )"1" "1" "1" "BEval" )nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" "BEval" )nil nil ))nil ))nil )"3" nil nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil )"3" "3" assert )nil nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil )"3" "3" assert )nil nil ))nil ))nil ))nil )"2" nil )"2" rewrite "nth_append" )"1" assert )"1" rewrite "nth_append" )"1" nil nil )"2" "2" assert )nil nil ))nil )"3" "3" assert )nil nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "proper_append" )"1" "1" expand "ProperBox?" )"1" expand "every" )"1" "1" expand "every" )"1" "BEval" )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (assert ) nil nil ))nil )"3" "3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" rewrite "length_append" )"1" "1" (assert ) nil nil ))nil )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" rewrite "length_append" )"1" "1" (assert ) nil nil ))nil )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (assert ) nil nil ))nil )"3" "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 )nil interval_expr nil )"bool" interval_expr nil )"list[T]" list_props nil )"ProperBox" interval_bexpr nil )"[list -> boolean]" list_adt nil )"[[T, list] -> (cons?)]" list_adt nil )"IntervalExpr" interval_bexpr nil )"[list -> boolean]" list_adt nil )"(null?)" list_adt nil )"posint" nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil list_props nil )nil more_list_props "structures/" )"int" integers nil )nil more_list_props "structures/" )"nonneg_int" nil )"posint" nil )"T" list_props nil )nil box nil )"boolean" list_adt nil )"bool" interval_expr nil )"list[Interval]" interval_bexpr nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )"[numfield -> numfield]" number_fields nil )"Interval" interval nil )"[Maybe -> boolean]" Maybe"structures/" )IF const-decl "[boolean, T, T -> T]" if_def nil )"nzrat" rationalsnil )"posrat" nil )"odd_int" integers nil )"[[RealExpr, Interval] -> (bincludes?)]" IntervalExpr_adt nil )"ProperBox" interval_bexpr nil )"Box" interval_bexpr nil )"RealExpr" interval_bexpr nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )"bool" real_orders "reals/" )nil real_orders "reals/" )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )nil IntervalExpr_adt nil )"[[RealOrder, RealExpr, RealExpr] -> (brel?)]" IntervalExpr_adtnil )nil interval_expr nil )"bool" interval nil )Eval def-decl "Interval" interval_expr nil )nil interval_expr nil )"(strict_total_order?[real])" real_props nil )"RealOrder" real_orders "reals/" )"(total_order?[real])" nil )"RealOrder" real_orders "reals/" )"(strict_total_order?[real])" real_props nil )"RealOrder" real_orders "reals/" )"(total_order?[real])" nil )"RealOrder" real_orders "reals/" )"bool" interval nil )"bool" real_orders "reals/" )"[real -> boolean]" rationals nil )"RealExpr" interval_bexpr nil )"Box" interval_bexpr nil )nil rationals nil )"[rational -> boolean]" integers nil )"bool" reals nil ) (< const-decl "bool" reals nil )nil integers nil )nil naturalnumbers nil )"nat" list_props nil )"ProperBox" interval_bexpr nil )nil naturalnumbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil IntervalExpr_adt nil )"Maybe[bool]" interval_bexpr nil )nil IntervalExpr_adt nil )"[(some?) -> T]" Maybe "structures/" )"[T, T -> boolean]" equalities nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[Maybe -> boolean]" Maybe"structures/" )nil Maybe "structures/" )"bool" box nil )nil box nil )"bool" box nil )nil box nil ) (list type-decl nil list_adt nil )nil interval nil )nil reals nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil IntervalExpr_adt nil ))nil )))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Dauer der Verarbeitung: 0.75 Sekunden
(vorverarbeitet am 2026-05-02)
¤ *© Formatika GbR, Deutschland
2026-05-26
