SSL interval_expr.prf
Interaktion und
(interval_exprnil 3576786010 ("" (subtype-tcc) nil nil )"Interval" interval nil )"bool" interval nil )"bool" interval nil ))nil ))nil 3576786010 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil reals nil )nil interval nil )"bool" interval nil )nil interval nil )"RealOrder" real_orders "reals/" )"(total_order?[real])" nil )"real" reals nil )"real" interval nil )"real" interval nil )"bool" interval nil )"bool" interval nil )"real" reals nil ))nil ))nil 3577184980 ("" (subtype-tcc) nil nil )"bool" interval nil )) nil ))nil 3577460822 ("" (grind) nil nil )"bool" interval_expr nil )"bool" interval_expr nil ))nil 3546625295"" (lemma "well_founded_restrict[IntervalExpr,RealExpr]" )"" (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 )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )nil IntervalExpr_adt nil ))nil ))nil 3546625295 ("" (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 )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )nil IntervalExpr_adt nil ))nil ))nil 3546625295 ("" (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 )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )nil IntervalExpr_adt nil )"(strict_well_founded?[IntervalExpr])" nil )"R" restrict nil ))nil ))nil 3546625295 ("" (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 )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )nil IntervalExpr_adt nil )"(strict_well_founded?[IntervalExpr])" nil )"R" restrict nil ))nil ))nil 3546625295 ("" (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 )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )nil IntervalExpr_adt nil ))nil ))nil 3546625295 ("" (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 )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )nil IntervalExpr_adt nil )"(strict_well_founded?[IntervalExpr])" nil )"R" restrict nil ))nil ))nil 3546625295 ("" (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 )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )nil IntervalExpr_adt nil ))nil ))nil 3546625295 ("" (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 )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )nil IntervalExpr_adt nil )"(strict_well_founded?[IntervalExpr])" nil )"R" restrict nil ))nil ))nil 3546625295 ("" (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 )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )nil IntervalExpr_adt nil ))nil ))nil 3546625295 ("" (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 )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )nil IntervalExpr_adt nil )"(strict_well_founded?[IntervalExpr])" nil )"R" restrict nil ))nil ))nil 3546625295 ("" (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 )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )nil IntervalExpr_adt nil )"(strict_well_founded?[IntervalExpr])" nil )"R" restrict nil ))nil ))nil 3546625295 ("" (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 )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )nil IntervalExpr_adt nil ))nil ))nil 3546625295 ("" (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 )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )nil IntervalExpr_adt nil )"(strict_well_founded?[IntervalExpr])" nil )"R" restrict nil ))nil ))nil 3546625295 ("" (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 )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )nil IntervalExpr_adt nil )"(strict_well_founded?[IntervalExpr])" nil )"R" restrict nil ))nil ))nil 3546625295 ("" (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 )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )nil IntervalExpr_adt nil ))nil ))nil 3546625295 ("" (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 )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )nil IntervalExpr_adt nil )"(strict_well_founded?[IntervalExpr])" nil )"R" restrict nil ))nil ))nil 3546625295 ("" (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 )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )nil IntervalExpr_adt nil ))nil ))nil 3546625295 ("" (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 )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )nil IntervalExpr_adt nil )"(strict_well_founded?[IntervalExpr])" nil )"R" restrict nil ))nil ))nil 3546625295 ("" (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 )"[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 )"boolean" notequal nil ))nil ))nil 3546625295 ("" (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 )"[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 ))nil ))nil 3546625295 ("" (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 )"[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/" )"R" restrict nil ))nil ))nil 3546625295 ("" (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 )"[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/" )"R" restrict nil ))nil ))nil 3546625295 ("" (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 )"[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 )"boolean" notequal nil ))nil ))nil 3546625295 ("" (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 )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )nil IntervalExpr_adt nil ))nil ))nil 3546710894 ("" (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 )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )nil IntervalExpr_adt nil )"(strict_well_founded?[IntervalExpr])" nil )"R" restrict nil ))nil ))nil 3546710894 ("" (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 )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )nil IntervalExpr_adt nil ))nil ))nil 3568989877 ("" (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 )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )nil IntervalExpr_adt nil )"(strict_well_founded?[IntervalExpr])" nil )"R" restrict nil ))nil ))nil 3580034334 ("" (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 )"[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 ))nil ))nil 3580034334 ("" (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 )"[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/" )"R" restrict nil ))nil ))nil 3580034334 ("" (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 )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )nil IntervalExpr_adt nil ))nil ))nil 3580034334 ("" (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 )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )nil IntervalExpr_adt nil )"(strict_well_founded?[IntervalExpr])" nil )"R" restrict nil ))nil ))nil 3546624714 ("" (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 )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )nil IntervalExpr_adt nil )"RealOrder" real_orders "reals/" )"(total_order?[real])" nil )"RealOrder" real_orders "reals/" )"(strict_total_order?[real])" real_props nil ))nil ))nil 3546624714 ("" (grind) 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 )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )nil IntervalExpr_adt nil )"(strict_well_founded?[IntervalExpr])" nil )"R" restrict nil ))nil ))nil 3580034334 ("" (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 )"[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 nil )"R" restrict nil ))nil ))nil 3576776063 ("" (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 )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )nil IntervalExpr_adt nil ))nil ))nil 3576776063 ("" (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 )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )nil IntervalExpr_adt nil ))nil ))nil 3576776063 ("" (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 )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )nil IntervalExpr_adt nil ))nil ))nil 3576776063 ("" (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 )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )nil IntervalExpr_adt nil ))nil ))nil 3576776063 ("" (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 )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )nil IntervalExpr_adt nil ))nil ))nil 3576776063 ("" (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 )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )nil IntervalExpr_adt nil ))nil ))nil 3576776063 ("" (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 )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )nil IntervalExpr_adt nil ))nil ))nil 3576776063 ("" (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 )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )nil IntervalExpr_adt nil )"bool" interval nil ))nil ))nil 3576776063 ("" (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 )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )nil IntervalExpr_adt nil )"bool" interval nil ))nil ))nil 3580040755"" "r1" "r2" ) :skolem-typepreds? t) (replaces -)expand "well_typed?" 1)expand "Eval" -3)case "Proper?(Eval(r1, box)) AND Proper?(Eval(r2, box))" )assert ))"Proper_NonEmpty" )"" "r1" :skolem-typepreds? t) (replaces -1)expand "well_typed?" 1) (expand "Eval" -2)case "Proper?(Eval(r1, box))" )assert ))"Proper_NonEmpty" )"" (induct "expr" )"1" (typepred "expr!1" ) (("1" (assert ) nil nil )) nil )"2" (skeep)"2" (hide -1)"2" (expand "well_typed?" ) (("2" (propax) nil nil )) nil ))nil ))nil )"3" (skeep)"3" (hide -1)"3" (skeep)"3" (expand "well_typed?" )"3" (expand "Proper?" )"3" (expand "Eval" -1)"3" (assert ) (("3" (grind) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil )"4" (binop) nil nil ) ("5" (unop) nil nil )"6" (unop) (("6" (grind) nil nil )) nil ) ("7" (binop) nil nil )"8" (binop) nil nil ) ("9" (unop) nil nil )"10" (skolem 1 (_ "n" )) (("10" (unop) nil nil )) nil )"11" (skolem 1 ("r1" "r2" ) :skolem-typepreds? t)"11" (replaces -)"11" (flatten)"11" (skeep)"11" (insteep)"11" (insteep)"11" (expand "well_typed?" 1)"11" (expand "Eval" -3)"11" case "Proper?(Eval(r1, box)) AND Proper?(Eval(r2, box)) AND Zeroless?(Eval(r2,box))" )"1" (flatten) (("1" (assert ) nil nil )) nil )"2" (hide-all-but (-3 1))"2" (lemma "Proper_NonEmpty" )"2" (ground) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"12" (skolem 1 ("Pre" "f" "F" _))"12" (skolem 1 "r1" :skolem-typepreds? t)"12" (replaces -1)"12" (flatten)"12" (skeep)"12" (insteep)"12" (expand "well_typed?" 1)"12" (expand "Eval" -2)"12" case "Proper?(Eval(r1, box)) AND Pre(Eval(r1, box))" )"1" (flatten) (("1" (assert ) nil nil )) nil )"2" (hide-all-but (-2 1))"2" (lemma "Proper_NonEmpty" )"2" (ground) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"13" (skolem 1 ("r1" "r2" ) :skolem-typepreds? t)"13" (replaces -)"13" (flatten)"13" (skeep)"13" (insteep)"13" (expand "well_typed?" 1)"13" (expand "Eval" -3)"13" (case-replace "Proper?(Eval(r1, box))" )"1" (assert )"1" (inst? -3) (("1" (assert ) nil nil ))nil ))nil )"2" (hide-all-but (-3 1))"2" (lemma "Proper_NonEmpty" )"2" (ground) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"14" (assert ) nil nil ) ("15" (assert ) nil nil )"16" (assert ) nil nil ) ("17" (assert ) nil nil )"18" (assert ) nil nil ) ("19" (assert ) nil nil )"20" (assert ) nil nil ) ("21" (assert ) nil nil )"22" (assert ) nil nil ))nil ))nil ))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 )nil defined_types nil )"bool" interval nil )"bool" interval nil )"(Precondition?)" intervalnil )"real" reals nil )"Interval" interval nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil interval nil )"(total_order?[real])" nil )"RealOrder" real_orders "reals/" )"(total_order?[real])" nil )"RealOrder" real_orders "reals/" )"(strict_total_order?[real])" real_props nil )"RealOrder" real_orders "reals/" )"Interval" interval nil )"Interval" interval nil )NOT const-decl "[bool -> bool]" booleans nil )nil IntervalExpr_adt nil )"bool" interval_expr nil )Eval def-decl "Interval" interval_expr nil )nil IntervalExpr_adt nil )"bool" interval 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 )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )nil IntervalExpr_adt nil )"bool" booleans nil )"[T, T -> boolean]" equalities nil )nil booleans nil )nil booleans nil ))nil )nil 3580040577"" "r1" "r2" ) :skolem-typepreds? t) (replaces -)expand "well_typed?" 1) (expand "Eval" -3)case "Proper?(Eval(r1, box)) AND Proper?(Eval(r2, box))" )assert ))"Proper_NonEmpty" )"" "r1" :skolem-typepreds? t) (replaces -1)expand "well_typed?" 1) (expand "Eval" -2)case "Proper?(Eval(r1, box))" )assert ))"Proper_NonEmpty" )"" (induct "expr" )"1" (typepred "expr!1" ) (("1" (assert ) nil nil )) nil )"2" (skeep)"2" (hide -1)"2" (expand "well_typed?" ) (("2" (propax) nil nil )) nil ))nil ))nil )"3" (skeep)"3" (hide -1)"3" (skeep)"3" (expand "well_typed?" )"3" (expand "Proper?" )"3" (expand "Eval" -1)"3" (assert ) (("3" (grind) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil )"4" (binop) nil nil ) ("5" (unop) nil nil )"6" (unop) (("6" (grind) nil nil )) nil ) ("7" (binop) nil nil )"8" (binop) nil nil ) ("9" (unop) nil nil )"10" (skolem 1 (_ "n" )) (("10" (unop) nil nil )) nil )"11" (skolem 1 ("r1" "r2" ) :skolem-typepreds? t)"11" (replaces -)"11" (flatten)"11" (skeep)"11" (insteep)"11" (insteep)"11" (expand "well_typed?" 1)"11" (expand "Eval" -3)"11" case "Proper?(Eval(r1, box)) AND Proper?(Eval(r2, box)) AND Zeroless?(Eval(r2,box))" )"1" (flatten) (("1" (assert ) nil nil )) nil )"2" (hide-all-but (-3 1))"2" (lemma "Proper_NonEmpty" )"2" (ground) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"12" (skolem 1 ("Pre" "f" "F" _))"12" (skolem 1 "r1" :skolem-typepreds? t)"12" (replaces -1)"12" (flatten)"12" (skeep)"12" (insteep)"12" (expand "well_typed?" 1)"12" (expand "Eval" -2)"12" case "Proper?(Eval(r1, box)) AND Pre(Eval(r1, box))" )"1" (flatten) (("1" (assert ) nil nil )) nil )"2" (hide-all-but (-2 1))"2" (lemma "Proper_NonEmpty" )"2" (ground) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"13" (skolem 1 ("r1" "r2" ) :skolem-typepreds? t)"13" (replaces -)"13" (flatten)"13" (skeep) (("13" (postpone) nil nil )) nil )) nil ))nil ))nil )"14" (assert ) nil nil ) ("15" (assert ) nil nil )"16" (assert ) nil nil ) ("17" (assert ) nil nil )"18" (assert ) nil nil ) ("19" (assert ) nil nil )"20" (assert ) nil nil ) ("21" (assert ) nil nil )"22" (assert ) nil nil ))nil ))nil ))nil )nil nil )nil 3576784677"" "r1" "r2" ) :skolem-typepreds? t) (replaces -)expand "well_typed?" 1) (expand "Eval" -3)case "Proper?(Eval(r1, box)) AND Proper?(Eval(r2, box))" )assert ))"Proper_NonEmpty" )"" "r1" :skolem-typepreds? t) (replaces -1)expand "well_typed?" 1) (expand "Eval" -2)case "Proper?(Eval(r1, box))" )assert ))"Proper_NonEmpty" )"" (skeep :but "expr" )"" (induct "expr" )"1" (typepred "expr!1" ) (("1" (assert ) nil nil )) nil )"2" (skeep)"2" (hide -1)"2" (expand "well_typed?" ) (("2" (propax) nil nil ))nil ))nil ))nil )"3" (skeep)"3" (hide -1)"3" (expand "well_typed?" )"3" (expand "Proper?" )"3" (expand "Eval" -1)"3" (assert ) (("3" (grind) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )"4" (binop) nil nil ) ("5" (unop) nil nil )"6" (unop) (("6" (grind) nil nil )) nil )"7" (binop) nil nil ) ("8" (binop) nil nil )"9" (unop) nil nil )"10" (skolem 1 (_ "n" )) (("10" (unop) nil nil )) nil )"11" (skolem 1 ("r1" "r2" ) :skolem-typepreds? t)"11" (replaces -)"11" (flatten)"11" (expand "well_typed?" 1)"11" (expand "Eval" -3)"11" case "Proper?(Eval(r1, box)) AND Proper?(Eval(r2, box)) AND Zeroless?(Eval(r2,box))" )"1" (flatten) (("1" (assert ) nil nil )) nil )"2" (hide-all-but (-3 1))"2" (lemma "Proper_NonEmpty" )"2" (ground) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"12" (skolem 1 ("Pre" "f" "F" _))"12" (skolem 1 "r1" :skolem-typepreds? t)"12" (replaces -1)"12" (flatten)"12" (expand "well_typed?" 1)"12" (expand "Eval" -2)"12" case "Proper?(Eval(r1, box)) AND Pre(Eval(r1, box))" )"1" (flatten) (("1" (assert ) nil nil )) nil )"2" (hide-all-but (-2 1))"2" (lemma "Proper_NonEmpty" )"2" (ground) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"13" (skolem 1 ("r1" "r2" ) :skolem-typepreds? t)"13" (replaces -)"13" (flatten) (("13" (postpone) nil nil )) nil )) nil ))nil )"14" (assert ) nil nil ) ("15" (assert ) nil nil )"16" (assert ) nil nil ) ("17" (assert ) nil nil )"18" (assert ) nil nil ) ("19" (assert ) nil nil )"20" (assert ) nil nil ) ("21" (assert ) nil nil )"22" (assert ) nil nil ))nil ))nil ))nil ))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 )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )nil interval nil )"bool" interval nil )nil IntervalExpr_adt nil )nil box nil )nil IntervalExpr_adt nil )"RealOrder" real_orders "reals/" )"RealOrder" real_orders "reals/" )"RealOrder" real_orders "reals/" )"Interval" interval nil )nil interval nil )"Interval" interval nil )"bool" interval nil )"(Precondition?)" intervalnil )"bool" interval nil ))nil ))nil 3580041393"" "r1" "r2" ) :skolem-typepreds? t) (flatten)expand "well_typed?" -3) (flatten) (assert ) (expand "eval" 1)expand "Eval" 1) (lemma "Member_Proper" ) (copy -1)assert )let ((lmnil "~a_inclusion" '(! 1 r)))))) rewrite lm))))"" "r" :skolem-typepreds? t) (flatten)expand "well_typed?" -2) (flatten) (assert ) (expand "eval" 1)expand "Eval" 1) (lemma "Member_Proper" ) (inst? -1 :where -2)assert )let ((lmnil "~a_inclusion" '(! 1 r)))))) rewrite lm))))"" (induct "expr" )"1" (typepred "expr!1" ) (("1" (assert ) nil nil )) nil )"2" (skeep :preds? t)"2" (hide -2)"2" (skeep)"2" (expand * "Eval" "eval" )"2" (expand "Includes?" ) (("2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )"3" (skeep)"3" (hide -1)"3" (skeep)"3" (expand * "Eval" "eval" "well_typed?" )"3" (assert )"3" (typepred "vs" )"3" (expand "vars_in_box?" )"3" (inst? -1) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" (binop) nil nil ) ("5" (unop) nil nil )"6" (unop) nil nil ) ("7" (binop) nil nil )"8" (binop) nil nil ) ("9" (unop) nil nil )"10" (skolem 1 (_ "n" )) (("10" (unop) nil nil )) nil )"11" (skolem 1 ("r1" "r2" ) :skolem-typepreds? t)"11" (flatten)"11" (replaces (-1 -2))"11" (skeep)"11" (insteep)"11" (insteep)"11" (expand "well_typed?" -3)"11" (flatten)"11" (assert )"11" (expand "eval" 1)"11" (expand "Eval" 1)"11" "Member_Proper" )"11" "11" "11" "11" assert )"11" "11" "1" "1" "1" "1" "Eval" )nil nil ))nil ))nil ))nil )"2" "2" rewrite "Div_inclusion" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"12" (skolem 1 ("Pre" "f" "F" _))"12" (skolem 1 "r" :skolem-typepreds? t)"12" (flatten)"12" (replaces -1)"12" (skeep)"12" (insteep)"12" (expand "well_typed?" -2)"12" (flatten)"12" (assert )"12" (lemma "Member_Proper" )"12" (inst? -1 :where -2)"12" assert )"12" expand "eval" 1)"12" expand "Eval" 1)"12" "F" )"12" expand "Inclusion?" )"12" "12" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"13" (skolem 1 ("r1" "r2" ) :skolem-typepreds? t)"13" (flatten)"13" (replaces -)"13" (skeep)"13" (insteep -)"13" (expand "well_typed?" -3)"13" (flatten)"13" (assert )"13" (expand "eval" 1)"13" (expand "Eval" 1)"13" (inst? - :where -4)"13" assert )"13" rewrite "length_append" )"13" "Proper?(Eval(r1,box))" )"1" "1" "1" expand "vars_in_box?" )"1" "1" "i=length(box)" )"1" assert )"1" rewrite "nth_append[Interval]" )"1" expand "nth" )"1" nil nil ))nil ))nil ))nil )"2" assert )"2" rewrite "nth_append[Interval]" )"1" "i" )"1" rewrite "length_append" )"1" assert )"1" "vs" )"1" expand "vars_in_box?" )"1" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "i" )"2" rewrite "length_append" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" "Eval" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"14" (assert ) nil nil ) ("15" (assert ) nil nil )"16" (assert ) nil nil ) ("17" (assert ) nil nil )"18" (assert ) nil nil ) ("19" (assert ) nil nil )"20" (assert ) nil nil ) ("21" (assert ) nil nil )"22" (assert ) nil nil ))nil ))nil ))nil )"(null?)" list_adt nil )"[list -> boolean]" list_adt nil )"[[T, list] -> (cons?)]" list_adt nil )"[list -> boolean]" list_adt nil )"list[T]" list_props nil )nil list_props nil )"nonneg_int" nil )nil more_list_props "structures/" )"Box" interval_expr nil )"RealExpr" interval_expr nil )"(vars_in_box?(box))" interval_expr nil )nil more_list_props "structures/" )"int" integers nil )"T" list_props nil )"posint" nil )nil defined_types nil )"bool" interval nil )"bool" interval nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" interval nil )"(Precondition?)" intervalnil )nil interval nil )"(strict_total_order?[real])" real_props nil )"RealOrder" real_orders "reals/" )"(total_order?[real])" nil )"RealOrder" real_orders "reals/" )"bool" interval nil )"bool" interval nil )nil interval nil )nil interval nil )nil interval nil )"real" reals nil )nil interval nil )"real" reals nil )nil interval nil )"real" reals nil )nil interval nil )nil interval nil )"real" reals nil )nil interval nil )"(total_order?[real])" nil )"RealOrder" real_orders "reals/" )"(strict_total_order?[real])" real_props nil )"RealOrder" real_orders "reals/" )nil naturalnumbers nil )"bool" reals nil )"bool" interval nil )NOT const-decl "[bool -> bool]" booleans nil )nil IntervalExpr_adt nil )Eval def-decl "Interval" interval_expr nil )"nat" list_props nil )eval def-decl "real" interval_expr nil )"bool" interval nil )"bool" interval_expr nil )nil IntervalExpr_adt 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 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 )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )nil IntervalExpr_adt nil )"bool" booleans nil )"[T, T -> boolean]" equalities nil )nil booleans nil )nil booleans nil ))nil )nil 3576777542"" (skeep)"" "r1" "r2" ) :skolem-typepreds? t) (flatten)expand "well_typed?" -3) (flatten) (assert )expand "eval" 1) (expand "Eval" 1) (lemma "Member_Proper" )assert )let ((lmnil "~a_inclusion" '(! 1 r)))))) rewrite lm))))"" "r" :skolem-typepreds? t) (flatten)expand "well_typed?" -2) (flatten) (assert )expand "eval" 1) (expand "Eval" 1) (lemma "Member_Proper" )assert )let ((lmnil "~a_inclusion" '(! 1 r)))))) rewrite lm))))"" (induct "expr" )"1" (typepred "expr!1" ) (("1" (assert ) nil nil )) nil )"2" (skeep :preds? t)"2" (hide -2)"2" (expand * "Eval" "eval" )"2" (expand "Includes?" ) (("2" (propax) nil nil ))nil ))nil ))nil ))nil )"3" (skeep)"3" (hide -1)"3" (expand * "Eval" "eval" "well_typed?" )"3" (assert )"3" (typepred "vs" )"3" (expand "vars_in_box?" )"3" (inst? -1) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"4" (binop) nil nil ) ("5" (unop) nil nil )"6" (unop) nil nil ) ("7" (binop) nil nil )"8" (binop) nil nil ) ("9" (unop) nil nil )"10" (skolem 1 (_ "n" )) (("10" (unop) nil nil )) nil )"11" (skolem 1 ("r1" "r2" ) :skolem-typepreds? t)"11" (flatten)"11" (replaces (-1 -2))"11" (expand "well_typed?" -3)"11" (flatten)"11" (assert )"11" (expand "eval" 1)"11" (expand "Eval" 1)"11" (lemma "Member_Proper" )"11" (copy -1)"11" "11" "11" assert )"11" "11" "1" "1" "1" "1" "Eval" )nil nil ))nil ))nil ))nil )"2" "2" rewrite "Div_inclusion" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"12" (skolem 1 ("Pre" "f" "F" _))"12" (skolem 1 "r" :skolem-typepreds? t)"12" (flatten)"12" (replaces -1)"12" (expand "well_typed?" -2)"12" (flatten)"12" (assert )"12" (lemma "Member_Proper" )"12" (inst? -1 :where -2)"12" (assert )"12" expand "eval" 1)"12" expand "Eval" 1)"12" "F" )"12" expand "Inclusion?" )"12" "12" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"13" (assert ) nil nil ) ("14" (assert ) nil nil )"15" (assert ) nil nil ) ("16" (assert ) nil nil )"17" (assert ) nil nil ) ("18" (assert ) nil nil )"19" (assert ) nil nil ) ("20" (assert ) nil nil )"21" (assert ) nil nil ))nil ))nil ))nil ))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 )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )nil interval nil )nil box nil )nil IntervalExpr_adt nil )"bool" interval nil )nil box nil )"bool" box nil )nil IntervalExpr_adt nil )"bool" interval nil )"RealOrder" real_orders "reals/" )"RealOrder" real_orders "reals/" )nil interval nil )nil interval nil )nil interval nil )nil interval nil )nil interval nil )nil interval nil )nil interval nil )nil interval nil )"(Precondition?)" intervalnil )nil interval nil )"RealOrder" real_orders "reals/" )"RealOrder" real_orders "reals/" )"bool" interval nil )"bool" interval nil )"bool" interval nil )"bool" interval nil )"bool" interval nil ))nil ))nil 3576776063"" (skeep*)"" (beta)"" (flatten)"" (lemma "Proper_well_typed" )"" (inst?)"" (assert )"" (lemma "Eval_inclusion" )"" (inst?) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )nil interval_expr nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )nil box nil )"bool" box nil )nil interval_expr 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 )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil IntervalExpr_adt nil )nil box nil ) (list type-decl nil list_adt nil )nil interval nil )nil reals nil ))nil ))nil 3576777667"" (skeep)"" (lemma "Eval_inclusion" )"" (inst? -1)"" (inst -1 "midvars(pox)" )"" (assert )"" (lemma "Member_Proper" )"" (inst? -1) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil )nil interval_expr 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 nil )"nat" list_props nil )eval def-decl "real" interval_expr nil )Eval def-decl "Interval" interval_expr 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 )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil IntervalExpr_adt nil )nil box nil )"bool" box nil )nil booleans nil )nil booleans nil )nil box nil ) (list type-decl nil list_adt nil )nil interval nil )nil reals nil ))"test" 3580046533"" "r1" "r2" ) :skolem-typepreds? t) (flatten)assert )expand "well_typed?" -4) (label "PP" -5) (flatten) (assert )expand "Eval" ("PP" 1))case "Proper?(Eval(r1, box)) AND Proper?(Eval(r2, box))" )assert ) (lemma "Incl_Proper" ) (copy -1)assert )let ((lmnil "~a_fundamental" '(! 1 r)))))) rewrite lm)))"PP" 1)) (lemma "Proper_NonEmpty" )"" "r" :skolem-typepreds? t) (flatten)assert )expand "well_typed?" -3) (label "PP" -4) (assert )expand "Eval" ("PP" 1))case "Proper?(Eval(r, box))" )assert ) (lemma "Incl_Proper" ) (inst? -1 :where -3)assert )let ((lmnil "~a_fundamental" '(! 1 r)))))) rewrite lm)))"PP" 1)) (assert )rewrite "Proper_NonEmpty" ))))))"" (induct "expr" )"1" (typepred "expr!1" ) (("1" (assert ) nil nil )) nil )"2" (skeep)"2" (hide -1)"2" (expand "Eval" ) (("2" (assert ) nil nil )) nil )) nil ))nil )"3" (skeep)"3" (hide -1)"3" (skeep)"3" (expand "well_typed?" )"3" (expand "Inclusion?" )"3" (flatten)"3" (expand "Eval" )"3" (assert ) (("3" (inst? -) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" (binop) nil nil ) ("5" (unop) nil nil )"6" (unop) (("6" (grind) nil nil )) nil ) ("7" (binop) nil nil )"8" (binop) nil nil ) ("9" (unop) nil nil )"10" (skolem 1 (_ "n" )) (("10" (unop) nil nil )) nil )"11" (skolem 1 ("r1" "r2" ) :skolem-typepreds? t)"11" (flatten)"11" (replaces (-1 -2))"11" (skeep)"11" (insteep)"11" (insteep)"11" (assert )"11" (expand "well_typed?" -4)"11" (label "PP" -5)"11" (flatten)"11" (assert )"11" expand "Eval" ("PP" 1))"11" case "Proper?(Eval(r1, box)) AND Proper?(Eval(r2, box))" )"1" "1" assert )"1" "Incl_Proper" )"1" "1" "1" "1" assert )"1" "1" "1" "1" assert )"1" rewrite "Div_fundamental" )nil nil ))nil ))nil )"2" "2" assert )"2" rewrite "Proper_NonEmpty" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "PP" 1))"2" "Proper_NonEmpty" )"2" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"12" (skolem 1 ("Pre" "f" "F" _))"12" (skolem 1 "r" :skolem-typepreds? t)"12" (flatten)"12" (replaces -1)"12" (skeep)"12" (insteep)"12" (assert )"12" (expand "well_typed?" -3)"12" (label "PP" -4)"12" (flatten)"12" (assert )"12" expand "Eval" ("PP" 1))"12" case "Proper?(Eval(r, box))" )"1" assert )"1" "Incl_Proper" )"1" "1" assert )"1" "1" "1" "1" assert )"1" "F" )"1" expand "Fundamental?" )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "Proper_NonEmpty" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "PP" 1))"2" assert )"2" rewrite "Proper_NonEmpty" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"13" (skolem 1 ("r1" "r2" ) :skolem-typepreds? t)"13" (flatten)"13" (replaces (-1 -2))"13" (skeep)"13" (insteep)"13" (assert )"13" (expand "well_typed?" -4)"13" (flatten)"13" (assert )"13" (label "PP" -6)"13" (expand "Eval" ("PP" 1))"13" case "Proper?(Eval(r1, box)) AND Proper?(Eval(r2, append(box, (: Eval(r1, box) :))))" )"1" "1" assert )"1" "Incl_Proper" )"1" "1" "1" "1" expand "Inclusion?" -1)"1" "1" "append(box, (: Eval(r1, box) :))" "append(pox, (: Eval(r1, pox) :))" )"1" case "length(append(box, (: Eval(r1, box) :))) = length(append(pox, (: Eval(r1, pox) :)))" )"1" "1" assert )"1" assert )"1" "1" expand "Inclusion?" "1" "1" "1" rewrite "nth_append" )"1" rewrite "nth_append" )"1" "i<length(box)" )"1" assert )"1" nil nil ))nil )"2" assert )"2" case "i=length(box)" )"1" replace "1" replace "1" assert )"1" expand "nth" "1" nil nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "length_append" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" rewrite "length_append" )"2" assert )nil nil ))nil ))nil )"2" rewrite "length_append" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "length_append" )"2" rewrite "length_append" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "PP" 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 ))nil ))nil ))nil )"2" "PP" 1))"2" "Proper_NonEmpty" )"2" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"14" (assert ) nil nil ) ("15" (assert ) nil nil )"16" (assert ) nil nil ) ("17" (assert ) nil nil )"18" (assert ) nil nil ) ("19" (assert ) nil nil )"20" (assert ) nil nil ) ("21" (assert ) nil nil )"22" (assert ) nil nil ))nil ))nil ))nil )"ProperBox" interval_expr nil )"RealExpr" interval_expr nil )"int" integers nil )"posint" nil )nil list_props nil )"odd_int" integers nil )"T" list_props nil )nil more_list_props "structures/" )"nonneg_int" nil )nil more_list_props "structures/" )nil box nil )"boolean" list_adt nil )"(null?)" list_adt nil )"[list -> boolean]" list_adt nil )"[[T, list] -> (cons?)]" list_adt nil )"[list -> boolean]" list_adt nil )"list[T]" list_props nil )nil interval nil )"bool" interval nil )"bool" interval nil )"bool" interval nil )nil defined_types nil )"(Precondition?)" intervalnil )nil interval nil )nil interval nil )nil interval nil )nil interval nil )nil interval nil )nil interval nil )"RealOrder" real_orders "reals/" )"(total_order?[real])" nil )"real" reals nil )"Interval" interval nil )"Interval" interval nil )nil interval nil )nil interval nil )nil interval nil )nil interval nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )"nat" list_props nil )nil naturalnumbers nil )"RealOrder" real_orders "reals/" )"(strict_total_order?[real])" real_props nil )"RealOrder" real_orders "reals/" )"(total_order?[real])" nil )nil interval nil )NOT const-decl "[bool -> bool]" booleans nil )nil IntervalExpr_adt nil )"bool" interval nil )Eval def-decl "Interval" interval_expr nil )"bool" interval nil )"bool" interval_expr nil )nil IntervalExpr_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"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 )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )nil IntervalExpr_adt nil )"bool" booleans nil )"[T, T -> boolean]" equalities nil )nil booleans nil )nil booleans nil ))nil ))nil 3580050685"" "r1" "r2" ) :skolem-typepreds? t) (flatten)expand "well_typed?" (-4 1)) (flatten) (assert )))"" "r" :skolem-typepreds? t) (flatten)expand "well_typed?" (-3 1))assert )))"" (lemma "Inclusion_Proper" )"" (induct "expr" )"1" (typepred "expr!1" ) (("1" (assert ) nil nil )) nil )"2" (skeep)"2" (hide -1)"2" (expand "well_typed?" 1) (("2" (propax) nil nil ))nil ))nil ))nil )"3" (skeep)"3" (hide -1)"3" (skeep)"3" (insteep)"3" (expand "well_typed?" )"3" (expand "Inclusion?" )"3" (flatten) (("3" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" (skeepreds2) nil nil ) ("5" (skeepreds1) nil nil )"6" (skeepreds1) nil nil ) ("7" (skeepreds2) nil nil )"8" (skeepreds2) nil nil ) ("9" (skeepreds1) nil nil )"10" (skolem 1 (_ "n" )) (("10" (skeepreds1) nil nil )) nil )"11" (skeepreds2)"11" (insteep)"11" (assert )"11" (lemma "Eval_fundamental_aux" )"11" (inst -1 "pox" "box" "r2" )"11" (assert )"11" (lemma "well_typed_Proper" )"11" (inst? - :where -4)"11" (assert )"11" (hide-all-but (-1 -2 -8 1))"11" (grind :exclude "Eval" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"12" (skolem 1 ("Pre" "f" "F" _))"12" (skeepreds1)"12" (insteep)"12" (assert )"12" (lemma "Eval_fundamental_aux" )"12" (inst -1 "pox" "box" "r" )"12" (assert )"12" (flatten)"12" (assert )"12" (lemma "well_typed_Proper" )"12" "12" assert )"12" "Pre" )"12" expand "Precondition?" )"12" "12" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"13" (skolem 1 ("r1" "r2" ) :skolem-typepreds? t)"13" (flatten)"13" (replaces (-1 -2))"13" (skeep)"13" (insteep)"13" (assert )"13" (expand "well_typed?" -4)"13" (flatten)"13" (assert )"13" (expand "well_typed?" 1)"13" "append(box, (: Eval(r1, box) :))" "append(pox, (: Eval(r1, pox) :))" )"1" assert )"1" "1" expand "Inclusion?" 1)"1" rewrite "length_append" )"1" rewrite "length_append" )"1" assert )"1" "1" assert )"1" expand "Inclusion?" )"1" "1" assert )"1" "1" rewrite "length_append" )"1" rewrite "nth_append" )"1" rewrite "nth_append" )"1" case "i< length(pox)" )"1" assert )"1" nil nil ))nil )"2" assert )"2" "i=length(box)" )"1" replace "1" assert )"1" "1" expand "nth" )"1" "Eval_fundamental_aux" )"1" "1" assert )"1" "well_typed_Proper" )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "proper_append" )"2" "2" expand "ProperBox?" 1)"2" expand "every" 1)"2" expand "every" 1)"2" "well_typed_Proper" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"14" (assert ) nil nil ) ("15" (assert ) nil nil )"16" (assert ) nil nil ) ("17" (assert ) nil nil )"18" (assert ) nil nil ) ("19" (assert ) nil nil )"20" (assert ) nil nil ) ("21" (assert ) nil nil )"22" (assert ) nil nil ))nil ))nil ))nil ))nil )nil IntervalExpr_adt nil )"[bool, bool -> bool]" 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 )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )nil reals nil )nil interval nil )nil list_adt nil ) (Box type-eq-decl nil box nil )"bool" box nil )nil box nil )"bool" box nil )nil IntervalExpr_adt nil )"bool" interval_expr nil )nil IntervalExpr_adt nil )NOT const-decl "[bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )"RealOrder" real_orders "reals/" )nil interval_expr nil )"(strict_total_order?[real])" real_props nil )"RealOrder" real_orders "reals/" )"(total_order?[real])" nil )"RealOrder" real_orders "reals/" )"bool" interval nil )"bool" interval nil )"bool" interval nil )nil interval_expr nil )"(Precondition?)" intervalnil )nil interval nil )Eval def-decl "Interval" interval_expr nil )"bool" interval nil )nil defined_types nil )"boolean" list_adt nil )nil box nil )"int" integers nil )"T" list_props nil )"odd_int" integers nil )nil naturalnumbers nil )"nat" list_props nil )"bool" reals 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 more_list_props "structures/" )"posint" nil )nil more_list_props "structures/" )"nonneg_int" nil )nil list_props nil )"list[T]" list_props nil )"ProperBox" interval_expr nil )"[list -> boolean]" list_adt nil )"[[T, list] -> (cons?)]" list_adt nil )"RealExpr" interval_expr nil )"[list -> boolean]" list_adt nil )"(null?)" list_adt nil )nil box nil )"bool" booleans nil )"[T, T -> boolean]" equalities nil )nil booleans nil )nil booleans nil ))nil ))nil 3580050420"" (skeep*)"" (lemma "well_typed_Inclusion_aux" )"" (insteep) (("" (assert ) nil nil )) nil )) nil ))nil )nil interval_expr 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 )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )nil IntervalExpr_adt nil ))nil ))nil 3576849784"" (skeep*)"" (lemma "Proper_well_typed" )"" (inst?)"" (assert )"" (lemma "well_typed_Inclusion" )"" (inst?)"" (assert )"" (inst?)"" (assert )"" (lemma "well_typed_Proper" )"" (inst? :where -2) (("" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil interval_expr nil )nil box nil )"bool" box nil )nil interval_expr nil )nil interval_expr 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 )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil IntervalExpr_adt nil )nil box nil ) (list type-decl nil list_adt nil )nil interval nil )nil reals nil ))nil 3549124802"" (skeep*)"" (lemma "well_typed_Inclusion" )"" (inst?)"" (assert )"" (inst? -1)"" (assert )"" (lemma "Eval_fundamental_aux" )"" (inst? -1)"1" (assert )"1" (lemma "well_typed_Proper" )"1" (inst? -1) (("1" (assert ) nil nil )) nil ))nil ))nil )"2" (lemma "Inclusion_Proper" )"2" (inst? -) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil interval_expr nil )"Box" interval_expr nil )nil interval_expr nil )nil box nil )nil interval_expr 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 )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil IntervalExpr_adt nil )nil box nil )"bool" box nil )nil booleans nil )nil booleans nil )nil box nil ) (list type-decl nil list_adt nil )nil interval nil )nil reals nil ))nil ))nil 3576785019"" (skeep*)"" (beta)"" (flatten)"" (lemma "Proper_well_typed" )"" (inst?)"" (assert )"" (lemma "Eval_fundamental" )"" (inst?)"" (assert )"" (inst? -) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil interval_expr nil )nil box nil )"bool" box nil )nil interval_expr 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 )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )"[IntervalExpr -> boolean]" nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil IntervalExpr_adt nil )nil box nil ) (list type-decl nil list_adt nil )nil interval nil )nil reals nil ))nil 3546789664 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans 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 )nil naturalnumbers nil )nil box nil )"nat" list_props nil )nil list_adt nil )nil interval nil )"bool" reals nil ))nil ))nil 3546789664 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans 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 )nil naturalnumbers nil )nil box nil )"nat" list_props nil )nil list_adt nil )nil interval nil )"bool" reals nil )"real" interval nil )"real" interval nil )"Interval" interval nil )"Interval" interval nil )"real" reals nil ))nil ))nil 3546789664 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans 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 )nil naturalnumbers nil )nil box nil )"nat" list_props nil )nil list_adt nil )nil interval nil )"bool" reals nil ))nil ))nil 3546789664 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans 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 )nil naturalnumbers nil )nil box nil )"nat" list_props nil )nil list_adt nil )nil interval nil )"bool" reals nil ))nil ))nil 3546789664 ("" (grind) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans 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 )"(total_order?[real])" nil )"RealOrder" real_orders "reals/" )"(strict_total_order?[real])" real_props nil )"RealOrder" real_orders "reals/" )"bool" reals nil )nil interval nil )nil list_adt nil ) (Box type-eq-decl nil box nil )nil naturalnumbers nil )"nat" list_props nil )"real" interval nil )"real" interval nil )"Interval" interval nil )"Interval" interval nil )"Interval" interval nil )"real" reals nil ))nil ))nil 3546789664 ("" (grind) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans 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 ))nil ))nil 3546789664 ("" (grind) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans 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 )"posint" nil )"posint" nil )"T" list_props nil )"real" interval nil )"real" interval nil )"Interval" interval nil )"Interval" interval nil )"nat" list_props nil )"Interval" interval nil )"real" reals nil ))nil ))nil 3546789664 ("" (grind) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans 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 )"int" integers nil ))nil ))nil 3546791205"" (skeep :preds? t)"" (skeep 3)"" (name-replace "V" "v1(v - 1, cdr(box))" :hide? t)"1" (typepred "V" )"1" (split)"1" (hide -3) (("1" (grind) nil nil )) nil )"2" (hide -3) (("2" (grind) nil nil )) nil )"3" (skeep)"3" (case-replace "i=0" )"1" (assert )"1" (expand "nth" +) (("1" (propax) nil nil )) nil ))nil )"2" (inst -3 "i-1" )"1" (assert )"1" (split 2)"1" (flatten)"1" (assert )"1" (flatten)"1" (expand "nth" 1)"1" (assert ) nil nil )) nil ))nil ))nil ))nil )"2" (flatten)"2" (assert )"2" (expand "nth" 2)"2" (flatten) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 3)"2" (typepred "i" )"2" (assert )"2" (expand "length" -1)"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 4) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil )NOT const-decl "[bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )"RealOrder" real_orders "reals/" )"Box" interval_expr nil )"below(length(box))" interval_expr nil )"posint" nil )"posint" nil )"[(cons?) -> list]" list_adt nil )"[list -> boolean]" list_adt nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"Interval" interval nil )"Interval" interval nil )"T" list_props nil )nil nat_types nil )IF const-decl "[boolean, T, T -> T]" if_def nil )nil naturalnumbers nil )"bool" reals nil )"nat" list_props nil )AND const-decl "[bool, bool -> bool]" booleans nil )"(strict_well_founded?[list])" list_adt nil )"bool" orders nil )nil defined_types nil )nil naturalnumbers nil )"bool" reals nil )nil booleans 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 )"[T, T -> boolean]" equalities nil )nil booleans nil )nil box nil ) (list type-decl nil list_adt nil )nil interval nil )nil reals nil )"int" integers nil )"RealOrder" real_orders "reals/" )"(total_order?[real])" nil ))nil )nil 3546789664 ("" (subtype-tcc) nil nil ) nil nil ))nil 3546789664 ("" (grind) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans 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 )"int" integers nil )"(total_order?[real])" nil )"RealOrder" real_orders "reals/" ))nil ))nil 3546789664 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans 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 )"(total_order?[real])" nil )"RealOrder" real_orders "reals/" ))nil ))nil 3546789664 ("" (grind) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans 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?[list])" list_adt nil )"(total_order?[real])" nil )"RealOrder" real_orders "reals/" ))nil ))nil 3546811001"" (recursive-judgement-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans 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 )"bool" reals nil )nil interval nil )nil list_adt nil )"nat" list_props nil )nil box nil )"(total_order?[real])" nil )"RealOrder" real_orders "reals/" )"(total_order?[real])" nil )"RealOrder" real_orders "reals/" ))nil ))nil 3546811001"" (recursive-judgement-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans 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 )"bool" reals nil )nil interval nil )nil list_adt nil )"nat" list_props nil )nil box nil )"posint" nil )"RealOrder" real_orders "reals/" )"(total_order?[real])" nil )"RealOrder" real_orders "reals/" )"(total_order?[real])" nil )"real" reals nil )"real" interval nil )"real" interval nil )"Interval" interval nil )"Interval" interval nil )"Interval" interval nil )"real" reals nil ))nil ))nil 3546811001"" (recursive-judgement-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans 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 )"bool" reals nil )nil interval nil )nil list_adt nil )"nat" list_props nil )nil box nil )"int" integers nil )"(total_order?[real])" nil )"RealOrder" real_orders "reals/" )"(total_order?[real])" nil )"RealOrder" real_orders "reals/" )"posint" nil ))nil ))nil 3546811387"" (skeep)"" (skeep 3)"" (typepred "v1(v - 1, cdr(box))" )"1" (replaces (-1 -2))"1" (replaces (-1 -2))"1" case "cons[Interval](car[Interval](box), cdr(box)) = box" )"1" (assert ) nil nil )"2" (hide 4)"2" (lemma "list_cons_eta[Interval]" )"2" (inst -1 "box" ) nil nil )) nil ))nil )"3" (assert ) nil nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil )"[[T, list] -> (cons?)]" list_adt nil )"[(cons?) -> T]" list_adt nil )nil list_adt nil )"(total_order?[real])" nil )"RealOrder" real_orders "reals/" )"int" integers nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil reals nil )nil interval nil )nil list_adt nil ) (Box type-eq-decl nil box nil )"[T, T -> boolean]" equalities nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )"nat" list_props nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[list -> boolean]" list_adt nil )"[(cons?) -> list]" list_adt nil ))nil )nil 3546811001"" (recursive-judgement-tcc) nil nil )nil interval nil )nil box nil ))nil ))nil 3546805651"" (skeep :preds? t)"" (case "v < length(box)" )"1" (beta)"1" (flatten)"1" (expand "vars_in_box?" )"1" (skolem 1 "i1" )"1" (skolem 2 "i2" )"1" (typepred "split(v, box)" )"1" (case-replace "i1=v" )"1" (case-replace "i2=v" )"1" (inst -5 "v" )"1" (flatten)"1" (replaces (-5 -6))"1" (inst -6 "v" )"1" "Halves_inclusion" )"1" "1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (inst -4 "i2" )"1" (assert )"1" (flatten)"1" (replaces -5)"1" (inst -6 "i2" ) nil nil )) nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" (inst -3 "i1" )"1" (assert )"1" (flatten)"1" (replaces -3)"1" (inst -5 "i1" ) nil nil )) nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "split_eq" )"2" (inst -1 "v" "box" )"1" (flatten) (("1" (assert ) nil nil )) nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )nil box nil )"nat" list_props nil )nil list_adt nil )nil interval nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"{lrb: [Box, Box] | LET (lb, rb) = lrb INAND AND IF i = vAND AND nth(rb, i) = nth(box, i)" interval_expr nil) "Interval" interval nil )"Interval" interval nil )"T" list_props nil )nil nat_types nil )IF const-decl "[boolean, T, T -> T]" if_def nil )nil naturalnumbers nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )NOT const-decl "[bool -> bool]" booleans nil )"below(length(split(v, box)`1))" nil )nil box nil )"RealOrder" real_orders "reals/" )"(total_order?[real])" nil )nil interval nil )"Box" interval_expr nil )"nat" interval_expr nil )"RealOrder" real_orders "reals/" )"(strict_total_order?[real])" real_props nil )"below(length(split(v, box)`2))" nil )"bool" box nil )"(total_order?[real])" nil )"RealOrder" real_orders "reals/" )"bool" reals nil )nil interval_expr nil ))nil 3576783085"" (skeep)"" (skoletin*)"" (expand "Inclusion?" )"" (typepred "split(v,pox)" )"" (assert )"" (replaces (-4 -5) :dir rl)"" (split)"1" (skeep)"1" (inst - "i" )"1" (split -)"1" (flatten)"1" (lemma "Halves_Incl" )"1" (inst?)"1" (assert )"1" "pox" )"1" expand "ProperBox?" )"1" rewrite "every_nth" )"1" (inst - "i" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (replaces -1) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (skeep)"2" (inst - "i" )"2" (split -)"1" (flatten)"1" (lemma "Halves_Incl" )"1" (inst?)"1" (assert )"1" "pox" )"1" expand "ProperBox?" )"1" rewrite "every_nth" )"1" (inst - "i" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (replaces -2) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"[bool, bool -> bool]" booleans nil )nil reals nil )nil interval nil )nil list_adt nil ) (Box type-eq-decl nil box nil )nil booleans nil )"[T, T -> boolean]" equalities nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )AND const-decl "[bool, bool -> bool]" booleans nil )"nat" list_props nil )"bool" reals nil )nil naturalnumbers nil )IF const-decl "[boolean, T, T -> T]" if_def nil )nil nat_types nil )"T" list_props nil )"Interval" interval nil )"Interval" interval nil )"{lrb: [Box, Box] | LET (lb, rb) = lrb INAND AND IF i = vAND AND nth(rb, i) = nth(box, i)" interval_expr nil) "bool" box nil )nil box nil )"bool" box nil )NOT const-decl "[bool -> bool]" booleans nil )nil interval nil )nil list_props nil )nil defined_types nil )"bool" interval nil )nil interval nil ))nil )nil 3549125269"" (skeep)"" (skoletin* 1)"" (expand "Inclusion?" )"" (typepred "split(v,box)" )"" (assert )"" (replaces (-4 -5) :dir rl)"" (split)"1" (skeep 1)"1" (inst -3 "i" )"1" (split -3)"1" (flatten)"1" (lemma "Halves_Incl" )"1" (inst?)"1" (assert )"1" "box" )"1" expand "ProperBox?" )"1" "1" rewrite "every_nth" )"1" (inst -2 "i" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (replaces -1) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (skeep 1)"2" (inst -3 "i" )"2" (split -3)"1" (flatten)"1" (lemma "Halves_Incl" )"1" (inst?)"1" (assert )"1" "box" )"1" expand "ProperBox?" )"1" "1" rewrite "every_nth" )"1" (inst -2 "i" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (replaces -2) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil interval nil )nil box nil )"Interval" interval nil )"Interval" interval nil )"bool" box nil )nil box nil )"bool" box nil )nil interval nil )"bool" interval nil )nil interval nil ))nil 3546795902"" (skeep)"" (typepred "pox" )"" (expand "ProperBox?" )"" (rewrite "every_nth" )"" (rewrite "every_nth" )"" (rewrite "every_nth" )"" (typepred "split(v,pox)" )"" (ground)"1" (skeep)"1" (inst - "i" )"1" (inst - "i" )"1" (split -)"1" (flatten)"1" (replaces (-1 -3))"1" rewrite "Proper_HalfRight" )nil nil ))nil ))nil )"2" (flatten) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (skeep)"2" (inst - "i" )"2" (inst - "i" )"2" (split -)"1" (flatten)"1" (replaces (-1 -2))"1" rewrite "Proper_HalfLeft" )nil nil ))nil ))nil )"2" (flatten) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil box nil )"bool" box nil )nil box nil ) (list type-decl nil list_adt nil )nil interval nil )nil reals nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil list_props nil )nil defined_types nil )"bool" interval nil )"(strict_total_order?[real])" real_props nil )"RealOrder" real_orders "reals/" )nil interval nil )nil interval nil )nil interval nil )"{lrb: [Box, Box] | LET (lb, rb) = lrb INAND AND IF i = vAND AND nth(rb, i) = nth(box, i)" interval_expr nil) "Interval" interval nil )"Interval" interval nil )"T" list_props nil )nil nat_types nil )IF const-decl "[boolean, T, T -> T]" if_def nil )nil naturalnumbers nil )"bool" reals nil )"nat" list_props nil )"[T, T -> boolean]" equalities nil )AND const-decl "[bool, bool -> bool]" booleans 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 ))nil 3577554456"" (skeep)"" (typepred "split(v, pox)" ) (("" (propax) nil nil )) nil )) nil )nil box nil )"bool" box nil )"{lrb: [Box, Box] | LET (lb, rb) = lrb INAND AND IF i = vAND AND nth(rb, i) = nth(box, i)" interval_expr nil) "Interval" interval nil )"Interval" interval nil )"T" list_props nil )nil nat_types nil )IF const-decl "[boolean, T, T -> T]" if_def nil )nil naturalnumbers nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil box nil )"nat" list_props 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 list_adt nil )nil interval nil )nil reals nil )"[T, T -> boolean]" equalities nil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"[ProperBox, ProperBox]" nil ))nil 3577554519"" (skeep)"" (typepred "split(v, pox)" ) (("" (propax) nil nil )) nil )) nil )nil box nil )"bool" box nil )"{lrb: [Box, Box] | LET (lb, rb) = lrb INAND AND IF i = vAND AND nth(rb, i) = nth(box, i)" interval_expr nil) "Interval" interval nil )"Interval" interval nil )"T" list_props nil )nil nat_types nil )IF const-decl "[boolean, T, T -> T]" if_def nil )nil naturalnumbers nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil box nil )"nat" list_props 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 list_adt nil )nil interval nil )nil reals nil )"[T, T -> boolean]" equalities nil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"[ProperBox, ProperBox]" nil ))nil )))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ 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.211Bemerkung:
(vorverarbeitet am 2026-04-28)
¤ *Bot Zugriff
2026-05-26
