|
(bands_3D
(trk_bands_3D_TCC1 0
(trk_bands_3D_TCC1-1 nil 3477656172 ("" (assuming-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(real nonempty-type-from-decl nil reals nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(/= const-decl "boolean" notequal nil)
(Vect3 type-eq-decl nil vectors_3D_def "vectors/")
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(vect2 const-decl "Vect2" vect_3D_2D "vectors/")
(zero const-decl "Vector" vectors_2D "vectors/")
(Nzv2_vect3 type-eq-decl nil definitions_3D nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nzv2 application-judgement "Nz_vect2" definitions_3D nil))
nil))
(trk_bands_3D_TCC2 0
(trk_bands_3D_TCC2-1 nil 3477656172 ("" (subtype-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(real nonempty-type-from-decl nil reals nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(Vect3 type-eq-decl nil vectors_3D_def "vectors/")
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(vect2 const-decl "Vect2" vect_3D_2D "vectors/")
(zero const-decl "Vector" vectors_2D "vectors/")
(Nzv2_vect3 type-eq-decl nil definitions_3D nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(nzv2 application-judgement "Nz_vect2" definitions_3D nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(/= const-decl "boolean" notequal nil))
nil))
(trk_bands_3D_TCC3 0
(trk_bands_3D_TCC3-1 nil 3477656172 ("" (subtype-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(real nonempty-type-from-decl nil reals nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(Vect3 type-eq-decl nil vectors_3D_def "vectors/")
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(vect2 const-decl "Vect2" vect_3D_2D "vectors/")
(zero const-decl "Vector" vectors_2D "vectors/")
(Nzv2_vect3 type-eq-decl nil definitions_3D nil)
(T formal-const-decl "{x: posreal | x > B}" bands_3D nil)
(<= const-decl "bool" reals nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nzint_times_nzint_is_nzint application-judgement "nzint" integers
nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(nzv2 application-judgement "Nz_vect2" definitions_3D nil)
(B formal-const-decl "nnreal" bands_3D nil)
(nnreal type-eq-decl nil real_types nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(H formal-const-decl "posreal" bands_3D nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(Sign type-eq-decl nil sign "reals/")
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(nzint nonempty-type-eq-decl nil integers nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(>= const-decl "bool" 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)
(Theta_H const-decl "real" vertical nil)
(/= const-decl "boolean" notequal nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(real_times_real_is_real application-judgement "real" reals nil))
nil))
(trk_bands_3D_TCC4 0
(trk_bands_3D_TCC4-1 nil 3477656172 ("" (subtype-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(real nonempty-type-from-decl nil reals nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(Vect3 type-eq-decl nil vectors_3D_def "vectors/")
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(vect2 const-decl "Vect2" vect_3D_2D "vectors/")
(zero const-decl "Vector" vectors_2D "vectors/")
(Nzv2_vect3 type-eq-decl nil definitions_3D nil)
(T formal-const-decl "{x: posreal | x > B}" bands_3D nil)
(<= const-decl "bool" reals nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nzint_times_nzint_is_nzint application-judgement "nzint" integers
nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(nzv2 application-judgement "Nz_vect2" definitions_3D nil)
(B formal-const-decl "nnreal" bands_3D nil)
(nnreal type-eq-decl nil real_types nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(H formal-const-decl "posreal" bands_3D nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(Sign type-eq-decl nil sign "reals/")
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(nzint nonempty-type-eq-decl nil integers nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(>= const-decl "bool" 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)
(Theta_H const-decl "real" vertical nil)
(/= const-decl "boolean" notequal nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(real_times_real_is_real application-judgement "real" reals nil))
nil))
(trk_bands_3D_TCC5 0
(trk_bands_3D_TCC5-1 nil 3477656172 ("" (assuming-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(real nonempty-type-from-decl nil reals nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(Vect3 type-eq-decl nil vectors_3D_def "vectors/")
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(vect2 const-decl "Vect2" vect_3D_2D "vectors/")
(zero const-decl "Vector" vectors_2D "vectors/")
(Nzv2_vect3 type-eq-decl nil definitions_3D nil)
(T formal-const-decl "{x: posreal | x > B}" bands_3D nil)
(<= const-decl "bool" reals nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nzint_times_nzint_is_nzint application-judgement "nzint" integers
nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(nzv2 application-judgement "Nz_vect2" definitions_3D nil)
(B formal-const-decl "nnreal" bands_3D nil)
(nnreal type-eq-decl nil real_types nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(H formal-const-decl "posreal" bands_3D nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(Sign type-eq-decl nil sign "reals/")
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(nzint nonempty-type-eq-decl nil integers nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(>= const-decl "bool" 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)
(Theta_H const-decl "real" vertical nil)
(/= const-decl "boolean" notequal nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(real_times_real_is_real application-judgement "real" reals nil))
nil))
(trk_bands_3D_TCC6 0
(trk_bands_3D_TCC6-1 nil 3477656172 ("" (subtype-tcc) nil nil)
((/= const-decl "boolean" notequal nil)
(Theta_H const-decl "real" vertical 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)
(default const-decl "T" fseqs "structures/")
(empty_seq const-decl "fsq" fseqs "structures/")
(real_times_real_is_real application-judgement "real" reals nil)
(nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(real_minus_real_is_real application-judgement "real" reals nil))
nil))
(trk_bands_3D_TCC7 0
(trk_bands_3D_TCC7-1 nil 3477736096
("" (skeep)
(("" (skosimp*)
(("" (expand "add")
(("" (expand "insert")
(("" (expand "empty_seq")
(("" (split 4)
(("1" (expand "trk_fseq?")
(("1" (skosimp*)
(("1" (lift-if)
(("1" (split +)
(("1" (flatten)
(("1" (assert) (("1" (assert) nil nil)) nil))
nil)
("2" (flatten) (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (expand "increasing?")
(("2" (skosimp*)
(("2" (case "i!1 = 0 AND j!1 = 1")
(("1" (flatten) (("1" (assert) nil nil)) nil)
("2" (typepred "i!1")
(("2" (typepred "j!1") (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((insert const-decl "fseq" fseqs_ops "structures/")
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(trk_fseq? const-decl "bool" fseqs_aux_2D nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(= const-decl "[T, T -> boolean]" equalities 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)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(increasing? const-decl "bool" sort_fseq "structures/")
(empty_seq const-decl "fsq" fseqs "structures/")
(add const-decl "fseq" fseqs_ops "structures/")
(pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx "trig_fnd/"))
nil))
(trk_bands_3D_TCC8 0
(trk_bands_3D_TCC8-1 nil 3477736096 ("" (subtype-tcc) nil nil)
((/= const-decl "boolean" notequal 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)
(default const-decl "T" fseqs "structures/")
(empty_seq const-decl "fsq" fseqs "structures/"))
nil))
(trk_bands_3D_TCC9 0
(trk_bands_3D_TCC9-2 "" 3504804745
("" (skeep)
(("" (expand "add")
(("" (expand "insert")
(("" (expand "empty_seq")
(("" (split 2)
(("1" (expand "trk_fseq?")
(("1" (skosimp*)
(("1" (lift-if)
(("1" (ground)
(("1" (lift-if) (("1" (ground) nil nil)) nil)
("2" (lift-if) (("2" (ground) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (expand "increasing?")
(("2" (skosimp*)
(("2" (case "i!1 = 0 AND j!1 = 1")
(("1" (flatten) (("1" (assert) nil nil)) nil)
("2" (typepred "i!1") (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx "trig_fnd/")
(add const-decl "fseq" fseqs_ops "structures/")
(empty_seq const-decl "fsq" fseqs "structures/")
(increasing? const-decl "bool" sort_fseq "structures/")
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real 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)
(= const-decl "[T, T -> boolean]" equalities nil)
(number nonempty-type-decl nil numbers nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(trk_fseq? const-decl "bool" fseqs_aux_2D nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(insert const-decl "fseq" fseqs_ops "structures/"))
shostak)
(trk_bands_3D_TCC9-1 nil 3477736096
("" (skeep)
(("" (expand "add")
(("" (expand "insert")
(("" (expand "empty_seq")
(("" (split 2)
(("1" (expand "trk_fseq?")
(("1" (skosimp*)
(("1" (lift-if) (("1" (ground) nil nil)) nil)) nil))
nil)
("2" (expand "increasing?")
(("2" (skosimp*)
(("2" (case "i!1 = 0 AND j!1 = 1")
(("1" (flatten) (("1" (assert) nil nil)) nil)
("2" (typepred "i!1") (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx "trig_fnd/")
(add const-decl "fseq" fseqs_ops "structures/")
(empty_seq const-decl "fsq" fseqs "structures/")
(increasing? const-decl "bool" sort_fseq "structures/")
(trk_fseq? const-decl "bool" fseqs_aux_2D nil)
(insert const-decl "fseq" fseqs_ops "structures/"))
nil))
(gs_bands_3D_TCC1 0
(gs_bands_3D_TCC1-1 nil 3477656172 ("" (subtype-tcc) nil nil)
((Nzv2_vect3 type-eq-decl nil definitions_3D nil)
(zero const-decl "Vector" vectors_2D "vectors/")
(vect2 const-decl "Vect2" vect_3D_2D "vectors/")
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(Vect3 type-eq-decl nil vectors_3D_def "vectors/")
(Vector type-eq-decl nil vectors_2D "vectors/")
(NOT const-decl "[bool -> bool]" booleans nil)
(T formal-const-decl "{x: posreal | x > B}" bands_3D nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(below type-eq-decl nil naturalnumbers nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nzint_times_nzint_is_nzint application-judgement "nzint" integers
nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(nzv2 application-judgement "Nz_vect2" definitions_3D nil)
(B formal-const-decl "nnreal" bands_3D nil)
(nnreal type-eq-decl nil real_types nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(H formal-const-decl "posreal" bands_3D nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(Sign type-eq-decl nil sign "reals/")
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(nzint nonempty-type-eq-decl nil integers nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(>= const-decl "bool" reals nil)
(/= const-decl "boolean" notequal nil)
(Theta_H const-decl "real" vertical 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)
(default const-decl "T" fseqs "structures/")
(empty_seq const-decl "fsq" fseqs "structures/")
(insert const-decl "fseq" fseqs_ops "structures/")
(add const-decl "fseq" fseqs_ops "structures/")
(gs_fseq? const-decl "bool" fseqs_aux_2D nil)
(<= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(increasing? const-decl "bool" sort_fseq "structures/")
(real_minus_real_is_real application-judgement "real" reals nil)
(nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(real_times_real_is_real application-judgement "real" reals nil))
nil))
(gs_bands_3D_TCC2 0
(gs_bands_3D_TCC2-1 nil 3477736096 ("" (subtype-tcc) nil nil)
((Nzv2_vect3 type-eq-decl nil definitions_3D nil)
(zero const-decl "Vector" vectors_2D "vectors/")
(vect2 const-decl "Vect2" vect_3D_2D "vectors/")
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(Vect3 type-eq-decl nil vectors_3D_def "vectors/")
(Vector type-eq-decl nil vectors_2D "vectors/")
(NOT const-decl "[bool -> bool]" booleans nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(>= const-decl "bool" reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(below type-eq-decl nil naturalnumbers nil)
(nzv2 application-judgement "Nz_vect2" definitions_3D nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(/= const-decl "boolean" notequal 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)
(default const-decl "T" fseqs "structures/")
(empty_seq const-decl "fsq" fseqs "structures/")
(insert const-decl "fseq" fseqs_ops "structures/")
(add const-decl "fseq" fseqs_ops "structures/")
(gs_fseq? const-decl "bool" fseqs_aux_2D nil)
(<= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(increasing? const-decl "bool" sort_fseq "structures/"))
nil))
(vs_bands_3D_TCC1 0
(vs_bands_3D_TCC1-1 nil 3477656172 ("" (assuming-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(real nonempty-type-from-decl nil reals nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(/= const-decl "boolean" notequal nil)
(Vect3 type-eq-decl nil vectors_3D_def "vectors/")
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(zero const-decl "Vector" vectors_2D "vectors/")
(Nzv2_vect3 type-eq-decl nil definitions_3D nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(nzv2 application-judgement "Nz_vect2" definitions_3D nil)
(- const-decl "Vector" vectors_3D "vectors/")
(vect2 const-decl "Vect2" vect_3D_2D "vectors/")
(* const-decl "real" vectors_2D "vectors/")
(sqv const-decl "nnreal" vectors_2D "vectors/")
(sq const-decl "nonneg_real" sq "reals/")
(real_times_real_is_real application-judgement "real" reals nil))
nil))
(vs_bands_3D_TCC2 0
(vs_bands_3D_TCC2-1 nil 3477656172
("" (skeep)
(("" (assert)
(("" (lemma "Delta_gt_0_nzv")
(("" (inst?) (("" (assert) nil nil)) nil)) nil))
nil))
nil)
((real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(Nzv2_vect3 type-eq-decl nil definitions_3D nil)
(zero const-decl "Vector" vectors_2D "vectors/")
(/= const-decl "boolean" notequal nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(- const-decl "Vector" vectors_3D "vectors/")
(Vector type-eq-decl nil vectors_3D "vectors/")
(vect2 const-decl "Vect2" vect_3D_2D "vectors/")
(Vect3 type-eq-decl nil vectors_3D_def "vectors/")
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(Delta_gt_0_nzv formula-decl nil horizontal nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans 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)
(bool nonempty-type-eq-decl nil booleans 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)
(D formal-const-decl "posreal" bands_3D nil))
nil))
(vs_bands_3D_TCC3 0
(vs_bands_3D_TCC3-1 nil 3477656172
("" (skeep)
(("" (skosimp*)
(("" (replace -2)
(("" (hide-all-but 2) (("" (grind :exclude "Theta_D") nil nil))
nil))
nil))
nil))
nil)
((real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(vect2 const-decl "Vect2" vect_3D_2D "vectors/")
(- const-decl "Vector" vectors_3D "vectors/")
(max const-decl "{p: real | p >= m AND p >= n}" real_defs nil))
nil))
(vs_bands_3D_TCC4 0
(vs_bands_3D_TCC4-1 nil 3477656172
("" (skeep)
(("" (hide-all-but (-2 2))
(("" (grind :exclude "Theta_D") nil nil)) nil))
nil)
((min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
(max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
(- const-decl "Vector" vectors_3D "vectors/")
(vect2 const-decl "Vect2" vect_3D_2D "vectors/")
(<= const-decl "bool" reals nil)
(T formal-const-decl "{x: posreal | x > B}" bands_3D nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(B formal-const-decl "nnreal" bands_3D nil)
(nnreal type-eq-decl nil real_types nil)
(Nzv2_vect3 type-eq-decl nil definitions_3D nil)
(Vector type-eq-decl nil vectors_3D "vectors/")
(Vect3 type-eq-decl nil vectors_3D_def "vectors/")
(Theta_D const-decl "real" horizontal nil)
(Sign type-eq-decl nil sign "reals/")
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(nzint nonempty-type-eq-decl nil integers nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(Delta const-decl "real" horizontal nil)
(D formal-const-decl "posreal" bands_3D nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
(zero const-decl "Vector" vectors_2D "vectors/")
(/= const-decl "boolean" notequal nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(AND const-decl "[bool, bool -> bool]" booleans nil)
(>= 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))
nil))
(vs_bands_3D_TCC5 0
(vs_bands_3D_TCC5-1 nil 3477656172
("" (skeep) (("" (skosimp*) (("" (assert) nil nil)) nil)) nil)
((real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
nil))
(vs_bands_3D_TCC6 0
(vs_bands_3D_TCC6-1 nil 3477656172
("" (skeep)
(("" (skosimp*)
(("" (typepred "i!1")
(("" (expand "empty_seq") (("" (propax) nil nil)) nil)) nil))
nil))
nil)
((empty_seq const-decl "fsq" fseqs "structures/")
(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)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil))
nil))
(vs_bands_3D_TCC7 0
(vs_bands_3D_TCC7-2 "" 3504804951
("" (skeep)
(("" (skosimp*)
(("" (expand "add")
(("" (expand "insert")
(("" (expand "empty_seq")
(("" (split 3)
(("1" (expand "vs_fseq?")
(("1" (skosimp*)
(("1" (lift-if)
(("1" (ground)
(("1" (lift-if) (("1" (ground) nil nil)) nil)
("2" (lift-if) (("2" (ground) nil nil)) nil)
("3" (lift-if) (("3" (ground) nil nil)) nil)
("4" (lift-if) (("4" (ground) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (expand "increasing?")
(("2" (skosimp*)
(("2" (typepred "i!1") (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((insert const-decl "fseq" fseqs_ops "structures/")
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(sqv_cont name-judgement "continuous_vr_fun" vect_cont_2D
"vect_analysis/")
(sq_nz_pos application-judgement "posreal" sq "reals/")
(vs_fseq? const-decl "bool" fseqs_aux_vertical nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(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)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(increasing? const-decl "bool" sort_fseq "structures/")
(empty_seq const-decl "fsq" fseqs "structures/")
(add const-decl "fseq" fseqs_ops "structures/"))
shostak)
(vs_bands_3D_TCC7-1 nil 3477744697
("" (skeep)
(("" (skosimp*)
(("" (expand "add")
(("" (expand "insert")
(("" (expand "empty_seq")
(("" (split 3)
(("1" (expand "vs_fseq?")
(("1" (skosimp*)
(("1" (lift-if) (("1" (ground) nil nil)) nil)) nil))
nil)
("2" (expand "increasing?")
(("2" (skosimp*)
(("2" (typepred "i!1") (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((insert const-decl "fseq" fseqs_ops "structures/")
(sq_nz_pos application-judgement "posreal" sq "reals/")
(sqv_cont name-judgement "continuous_vr_fun" vect_cont_2D
"vect_analysis/")
(vs_fseq? const-decl "bool" fseqs_aux_vertical nil)
(increasing? const-decl "bool" sort_fseq "structures/")
(empty_seq const-decl "fsq" fseqs "structures/")
(add const-decl "fseq" fseqs_ops "structures/"))
nil))
(vs_bands_3D_TCC8 0
(vs_bands_3D_TCC8-1 nil 3477744697
("" (skeep)
(("" (skosimp*)
(("" (expand "empty_seq") (("" (propax) nil nil)) nil)) nil))
nil)
((empty_seq const-decl "fsq" fseqs "structures/")) nil))
(vs_bands_3D_TCC9 0
(vs_bands_3D_TCC9-2 "" 3504805194
("" (skeep)
(("" (expand "add")
(("" (expand "insert")
(("" (expand "empty_seq")
(("" (split 3)
(("1" (expand "vs_fseq?")
(("1" (skosimp*)
(("1" (lift-if)
(("1" (ground)
(("1" (lift-if) (("1" (ground) nil nil)) nil)
("2" (lift-if) (("2" (ground) nil nil)) nil)
("3" (lift-if) (("3" (ground) nil nil)) nil)
("4" (lift-if) (("4" (ground) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (expand "increasing?")
(("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil)
((add const-decl "fseq" fseqs_ops "structures/")
(empty_seq const-decl "fsq" fseqs "structures/")
(increasing? const-decl "bool" sort_fseq "structures/")
(int_minus_int_is_int application-judgement "int" integers nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(vs_fseq? const-decl "bool" fseqs_aux_vertical nil)
(sq_nz_pos application-judgement "posreal" sq "reals/")
(sqv_cont name-judgement "continuous_vr_fun" vect_cont_2D
"vect_analysis/")
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(insert const-decl "fseq" fseqs_ops "structures/"))
shostak)
(vs_bands_3D_TCC9-1 nil 3477744697
("" (skeep)
(("" (expand "add")
(("" (expand "insert")
(("" (expand "empty_seq")
(("" (split 3)
(("1" (expand "vs_fseq?")
(("1" (skosimp*)
(("1" (lift-if) (("1" (ground) nil nil)) nil)) nil))
nil)
("2" (expand "increasing?")
(("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil)
((add const-decl "fseq" fseqs_ops "structures/")
(empty_seq const-decl "fsq" fseqs "structures/")
(increasing? const-decl "bool" sort_fseq "structures/")
(vs_fseq? const-decl "bool" fseqs_aux_vertical nil)
(sqv_cont name-judgement "continuous_vr_fun" vect_cont_2D
"vect_analysis/")
(sq_nz_pos application-judgement "posreal" sq "reals/")
(insert const-decl "fseq" fseqs_ops "structures/"))
nil))
(trk_bands_3D_not_empty 0
(trk_bands_3D_not_empty-1 nil 3481653292
("" (skeep)
(("" (expand "trk_bands_3D")
(("" (lift-if)
(("" (ground)
(("1" (lemma "trk_bands_not_empty[D,B,T,gsmin,gsmax]")
(("1" (inst?) nil nil) ("2" (assert) nil nil)) nil)
("2"
(lemma
"trk_bands_not_empty[D, max(Theta_H(s`z, vo`z - vi`z, -1), B),
min(Theta_H(s`z, vo`z - vi`z, 1), T), gsmin, gsmax]")
(("1" (inst?) nil nil) ("2" (assert) nil nil)) nil)
("3" (expand "max")
(("3" (expand "min")
(("3" (expand "add")
(("3" (expand "insert")
(("3" (expand "empty_seq") (("3" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("4"
(lemma "trk_bands_not_empty
[D, max(Theta_H(s`z, vo`z - vi`z, -1), B),
min(Theta_H(s`z, vo`z - vi`z, 1), T), gsmin, gsmax]")
(("1" (inst?) nil nil) ("2" (assert) nil nil)) nil)
("5" (expand "add")
(("5" (expand "insert")
(("5" (expand "empty_seq") (("5" (assert) nil nil)) nil))
nil))
nil)
("6" (expand "add")
(("6" (expand "empty_seq")
(("6" (expand "insert") (("6" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((trk_bands_3D const-decl
"{fs: (trk_fseq?[gsmin, gsmax]) | increasing?(fs)}" bands_3D nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx "trig_fnd/")
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(nzv2 application-judgement "Nz_vect2" definitions_3D nil)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(Vect3 type-eq-decl nil vectors_3D_def "vectors/")
(vect2 const-decl "Vect2" vect_3D_2D "vectors/")
(Vector type-eq-decl nil vectors_2D "vectors/")
(/= const-decl "boolean" notequal nil)
(zero const-decl "Vector" vectors_2D "vectors/")
(Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
(Nzv2_vect3 type-eq-decl nil definitions_3D nil)
(< const-decl "bool" reals nil)
(trk_bands_not_empty formula-decl nil bands_2D nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans 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)
(bool nonempty-type-eq-decl nil booleans 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)
(D formal-const-decl "posreal" bands_3D nil)
(nnreal type-eq-decl nil real_types nil)
(B formal-const-decl "nnreal" bands_3D nil)
(T formal-const-decl "{x: posreal | x > B}" bands_3D nil)
(gsmin formal-const-decl "posreal" bands_3D nil)
(gsmax formal-const-decl "{x: posreal | x > gsmin}" bands_3D nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(nzint nonempty-type-eq-decl nil integers nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(Sign type-eq-decl nil sign "reals/")
(H formal-const-decl "posreal" bands_3D nil)
(Theta_H const-decl "real" vertical nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(<= const-decl "bool" reals nil)
(min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
(insert const-decl "fseq" fseqs_ops "structures/")
(empty_seq const-decl "fsq" fseqs "structures/")
(add const-decl "fseq" fseqs_ops "structures/"))
shostak))
(trk_bands_last_TCC1 0
(trk_bands_last_TCC1-1 nil 3482239733
("" (skeep)
(("" (lemma "trk_bands_3D_not_empty")
(("" (inst?) (("" (assert) nil nil)) nil)) nil))
nil)
((trk_bands_3D_not_empty formula-decl nil bands_3D nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(Nzv2_vect3 type-eq-decl nil definitions_3D nil)
(zero const-decl "Vector" vectors_2D "vectors/")
(vect2 const-decl "Vect2" vect_3D_2D "vectors/")
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(/= const-decl "boolean" notequal nil)
(boolean nonempty-type-decl nil booleans nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(Vect3 type-eq-decl nil vectors_3D_def "vectors/")
(real nonempty-type-from-decl nil reals nil))
nil))
(trk_bands_last 0
(trk_bands_last-2 "" 3504805750
("" (skeep)
(("" (name "trkbb" "trk_bands_3D(s, vo, vi)")
(("" (replace -1)
(("" (assert)
(("" (case "member(2*pi,trkbb)")
(("1" (expand "member")
(("1" (skosimp*)
(("1" (typepred "trkbb")
(("1" (expand "increasing?")
(("1" (inst - "i!1" "trkbb`length-1")
(("1" (assert)
(("1" (expand "trk_fseq?")
(("1" (inst - "trkbb`length-1")
(("1" (flatten) (("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (hide -)
(("2" (expand "trkbb")
(("2" (expand "trk_bands_3D")
(("2" (lift-if)
(("2" (ground)
(("1"
(lemma
"trk_bands_critical[D,B,T,gsmin,gsmax]")
(("1" (inst?)
(("1" (assert)
(("1"
(hide 2)
(("1"
(flatten)
(("1"
(hide 1)
(("1"
(expand "to2pi")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil)
("2"
(lemma
"trk_bands_critical[D, max(Theta_H(s`z, vo`z - vi`z, -1), B),
min(Theta_H(s`z, vo`z - vi`z, 1), T), gsmin, gsmax]")
(("1" (inst?)
(("1" (assert)
(("1"
(flatten)
(("1"
(expand "to2pi")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil)
("3" (expand "member")
(("3" (inst + "1")
(("1" (expand "add")
(("1"
(expand "insert")
(("1"
(assert)
(("1"
(expand "empty_seq")
(("1" (propax) nil nil))
nil))
nil))
nil))
nil)
("2" (expand "add")
(("2"
(expand "insert")
(("2"
(expand "empty_seq")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("4"
(lemma
"trk_bands_critical[D, max(Theta_H(s`z, vo`z - vi`z, -1), B),
min(Theta_H(s`z, vo`z - vi`z, 1), T), gsmin, gsmax]")
(("1" (inst?)
(("1" (assert)
(("1"
(flatten)
(("1"
(expand "to2pi")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil)
("5" (expand "member")
(("5" (inst + "1")
(("1" (expand "add")
(("1"
(expand "insert")
(("1"
(expand "empty_seq")
(("1" (assert) nil nil))
nil))
nil))
nil)
("2" (expand "add")
(("2"
(expand "insert")
(("2"
(expand "empty_seq")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("6" (expand "member")
(("6" (inst + "1")
(("1" (expand "add")
(("1"
(expand "insert")
(("1"
(expand "empty_seq")
(("1" (assert) nil nil))
nil))
nil))
nil)
("2" (expand "add")
(("2"
(expand "insert")
(("2"
(expand "empty_seq")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((trk_bands_3D const-decl
"{fs: (trk_fseq?[gsmin, gsmax]) | increasing?(fs)}" bands_3D nil)
(increasing? const-decl "bool" sort_fseq "structures/")
(<= const-decl "bool" reals nil)
(trk_fseq? const-decl "bool" fseqs_aux_2D nil)
(gsmax formal-const-decl "{x: posreal | x > gsmin}" bands_3D nil)
(gsmin formal-const-decl "posreal" bands_3D nil)
(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)
(Nzv2_vect3 type-eq-decl nil definitions_3D nil)
(zero const-decl "Vector" vectors_2D "vectors/")
(vect2 const-decl "Vect2" vect_3D_2D "vectors/")
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(/= const-decl "boolean" notequal nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(Vect3 type-eq-decl nil vectors_3D_def "vectors/")
(= const-decl "[T, T -> boolean]" equalities nil)
(fseq type-eq-decl nil fseqs "structures/")
(barray type-eq-decl nil fseqs "structures/")
(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)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx "trig_fnd/")
(trkbb skolem-const-decl
"{fs: (trk_fseq?[gsmin, gsmax]) | increasing?(fs)}" bands_3D nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(insert const-decl "fseq" fseqs_ops "structures/")
(empty_seq const-decl "fsq" fseqs "structures/")
(fsq type-eq-decl nil fsq "structures/")
(add const-decl "fseq" fseqs_ops "structures/")
(min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
(Theta_H const-decl "real" vertical nil)
(H formal-const-decl "posreal" bands_3D nil)
(Sign type-eq-decl nil sign "reals/")
(- const-decl "[numfield -> numfield]" number_fields nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(nzint nonempty-type-eq-decl nil integers nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(trk_bands_critical formula-decl nil bands_2D nil)
(D formal-const-decl "posreal" bands_3D nil)
(nnreal type-eq-decl nil real_types nil)
(B formal-const-decl "nnreal" bands_3D nil)
(T formal-const-decl "{x: posreal | x > B}" bands_3D nil)
(nonneg_floor_is_nat application-judgement "nat" floor_ceil nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(to2pi const-decl "nnreal_lt_2pi" to2pi "trig_fnd/")
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
(nzv2 application-judgement "Nz_vect2" definitions_3D nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(below type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(pi const-decl "posreal" atan "trig_fnd/")
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(member const-decl "bool" fseqs "structures/"))
shostak)
(trk_bands_last-1 nil 3482239733
("" (skeep)
(("" (name "trkbb" "trk_bands_3D(s, vo, vi)")
(("" (replace -1)
(("" (assert)
(("" (case "member(2*pi,trkbb)")
(("1" (expand "member")
(("1" (skosimp*)
(("1" (typepred "trkbb")
(("1" (expand "increasing?")
(("1" (inst - "i!1" "trkbb`length-1")
(("1" (assert)
(("1" (expand "trk_fseq?")
(("1" (inst - "trkbb`length-1")
(("1" (flatten) (("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (hide -)
(("2" (expand "trkbb")
(("2" (expand "trk_bands_3D")
(("2" (lift-if)
(("2" (ground)
(("1"
(lemma
"trk_bands_critical[D,B,T,gsmin,gsmax]")
(("1" (inst?)
(("1" (assert)
(("1"
(hide 2)
(("1"
(flatten)
(("1"
(hide 1)
(("1"
(expand "to2pi")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil)
("2"
(lemma
"trk_bands_critical[D, max(Theta_H(s`z, vo`z - vi`z, -1), B),
min(Theta_H(s`z, vo`z - vi`z, 1), T), gsmin, gsmax]")
(("1" (inst?)
(("1" (assert)
(("1"
(flatten)
(("1"
(expand "to2pi")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil)
("3" (expand "member")
(("3" (inst + "1")
(("1" (expand "add")
(("1"
(expand "insert")
(("1"
(expand "empty_seq")
(("1" (propax) nil nil))
nil))
nil))
nil)
("2" (expand "add")
(("2"
(expand "insert")
(("2"
(expand "empty_seq")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("4"
(lemma
"trk_bands_critical[D, max(Theta_H(s`z, vo`z - vi`z, -1), B),
min(Theta_H(s`z, vo`z - vi`z, 1), T), gsmin, gsmax]")
(("1" (inst?)
(("1" (assert)
(("1"
(flatten)
(("1"
(expand "to2pi")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil)
("5" (expand "member")
(("5" (inst + "1")
(("1" (expand "add")
(("1"
(expand "insert")
(("1"
(expand "empty_seq")
(("1" (propax) nil nil))
nil))
nil))
nil)
("2" (expand "add")
(("2"
(expand "insert")
(("2"
(expand "empty_seq")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("6" (expand "member")
(("6" (inst + "1")
(("1" (expand "add")
(("1"
(expand "insert")
(("1"
(expand "empty_seq")
(("1" (propax) nil nil))
nil))
nil))
nil)
("2" (expand "add")
(("2"
(expand "insert")
(("2"
(expand "empty_seq")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((increasing? const-decl "bool" sort_fseq "structures/")
(trk_fseq? const-decl "bool" fseqs_aux_2D nil)
(Nzv2_vect3 type-eq-decl nil definitions_3D nil)
(zero const-decl "Vector" vectors_2D "vectors/")
(vect2 const-decl "Vect2" vect_3D_2D "vectors/")
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(Vector type-eq-decl nil vectors_2D "vectors/")
(Vect3 type-eq-decl nil vectors_3D_def "vectors/")
(fseq type-eq-decl nil fseqs "structures/")
(barray type-eq-decl nil fseqs "structures/")
(pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx "trig_fnd/")
(insert const-decl "fseq" fseqs_ops "structures/")
(add const-decl "fseq" fseqs_ops "structures/")
(fsq type-eq-decl nil fsq "structures/")
(empty_seq const-decl "fsq" fseqs "structures/")
(Theta_H const-decl "real" vertical nil)
(Sign type-eq-decl nil sign "reals/")
(trk_bands_critical formula-decl nil bands_2D nil)
(to2pi const-decl "nnreal_lt_2pi" to2pi "trig_fnd/")
(Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
(nzv2 application-judgement "Nz_vect2" definitions_3D nil)
(pi const-decl "posreal" atan "trig_fnd/")
(member const-decl "bool" fseqs "structures/"))
shostak))
(trk_bands_first 0
(trk_bands_first-1 nil 3482241439
("" (skeep)
(("" (name "trkbb" "trk_bands_3D(s, vo, vi)")
(("" (replace -1)
(("" (assert)
(("" (case "member(0,trkbb)")
(("1" (typepred "trkbb")
(("1" (expand "increasing?")
(("1" (expand "member")
(("1" (skosimp*)
(("1" (inst - "0" "i!1")
(("1" (assert)
(("1" (expand "trk_fseq?")
(("1" (inst - "0") (("1" (assert) nil nil))
nil))
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.70 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
