(PVSTypes (myabs_TCC1 0 (myabs_TCC1-1 nil 3309778887 3309864341 ("" (subtype-tcc) nil nil) proved ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil)) 146 90 nil nil)) (myabs_TCC2 0 (myabs_TCC2-1 nil 3309778887 3309864341 ("" (subtype-tcc) nil nil) proved ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil)) 76 70 nil nil)) (h_TCC1 0 (h_TCC1-1 nil 3309778887 3309864342 ("" (subtype-tcc) nil nil) proved ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (myabs const-decl "nonneg_real" PVSTypes nil)) 379 250 nil nil)) (h2_TCC1 0 (h2_TCC1-1 nil 3309778887 3309864342 ("" (subtype-tcc) nil nil) proved ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil)) 290 240 nil nil)) (signs_TCC1 0 (signs_TCC1-1 nil 3309864197 3309864541 ("" (cond-disjoint-tcc) (("" (postpone) nil nil)) nil) unfinished ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil)) 122402 670 t shostak)) (signs_TCC2 0 (signs_TCC2-1 nil 3309864197 3309864342 ("" (cond-coverage-tcc) nil nil) proved ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil)) 92 80 nil shostak)) (f_TCC1 0 (f_TCC1-1 nil 3309778888 3309864342 ("" (subtype-tcc) (("" (postpone) nil nil)) nil) unfinished nil 260 200 nil shostak)) (g_TCC1 0 (g_TCC1-1 nil 3309778887 3309864343 ("" (skolem!) (("" (typepred "y!1") (("" (assert) nil nil)) nil)) nil) proved ((>= const-decl "bool" reals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) 154 140 nil nil)) (PwrCond_TCC1 0 (PwrCond_TCC1-1 nil 3309778887 3309866209 ("" (cond-disjoint-tcc) (("" (delete -3 -5 -1) (("" (postpone) nil nil)) nil)) nil) unfinished nil 831392 1360 t nil)) (PwrCond_TCC2 0 (PwrCond_TCC2-1 nil 3309778887 3309864343 ("" (cond-coverage-tcc) nil nil) proved ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil)) 206 180 nil nil)) (DisjointnessCounterExample 0 (DisjointnessCounterExample-1 nil 3309778887 nil ("" (inst 1 "2" "1" "3") (("" (grind) nil nil)) nil) unchecked ((posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) nil nil nil nil)) (PwrCond_TCC1CounterExample 0 (PwrCond_TCC1CounterExample-1 nil 3309778887 nil ("" (inst -1 "1" "3" "2") (("" (grind) nil nil)) nil) unfinished nil nil nil nil nil)) (FixedPwrCond_TCC1 0 (FixedPwrCond_TCC1-1 nil 3309778887 3309864344 ("" (cond-disjoint-tcc) nil nil) proved ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (< const-decl "bool" reals nil)) 438 360 nil nil)) (FixedPwrCond_TCC2 0 (FixedPwrCond_TCC2-1 nil 3309778887 3309864344 ("" (cond-coverage-tcc) nil nil) proved ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (< const-decl "bool" reals nil)) 227 190 nil nil)) (Validation_TCC1 0 (Validation_TCC1-1 nil 3309778887 3309864344 ("" (subtype-tcc) (("" (postpone) nil nil)) nil) unfinished nil 157 130 nil nil)))