|
(bands_2D
(trk_critical_TCC1 0
(trk_critical_TCC1-1 nil 3477392567
("" (skeep)
(("" (expand "trk_fseq?")
(("" (skosimp*)
(("" (expand "addend")
(("" (expand "empty_seq")
(("" (lift-if)
(("" (ground)
(("1" (typepred "i!1")
(("1" (expand "addend")
(("1" (expand "empty_seq") (("1" (propax) nil nil))
nil))
nil))
nil)
("2" (typepred "i!1")
(("2" (expand "addend")
(("2" (expand "empty_seq") (("2" (propax) nil 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/")
(trk_fseq? const-decl "bool" fseqs_aux_2D nil)
(addend const-decl "fseq" fseqs_ops "structures/")
(below type-eq-decl nil naturalnumbers nil)
(fsq type-eq-decl nil fsq "structures/")
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(track const-decl "nnreal_lt_2pi" track nil)
(nnreal_lt_2pi nonempty-type-eq-decl nil atan2 "trig_fnd/")
(pi const-decl "posreal" atan "trig_fnd/")
(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 "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(nnreal 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/")
(fseq type-eq-decl nil fseqs "structures/")
(barray type-eq-decl nil fseqs "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)
(< 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)
(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)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(empty_seq const-decl "fsq" fseqs "structures/"))
nil))
(trk_critical_TCC2 0
(trk_critical_TCC2-1 nil 3477392567 ("" (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/")
(emptyseq macro-decl "fsq" fseqs "structures/")
(Integral const-decl "real" integral_def "analysis/")
(atan_value const-decl "real" atan "trig_fnd/")
(pi const-decl "posreal" atan "trig_fnd/")
(gsmax formal-const-decl "posreal" bands_2D nil)
(gsmin formal-const-decl "posreal" bands_2D 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)
(trk_fseq? const-decl "bool" fseqs_aux_2D nil))
nil))
(trk_critical_rew 0
(trk_critical_rew-2 "" 3504815249
("" (skeep)
(("" (lift-if)
(("" (ground)
(("1" (expand "trk_critical")
(("1" (expand "addend")
(("1" (decompose-equality 2)
(("1" (expand "empty_seq")
(("1" (lemma "singleton_length")
(("1" (inst?)
(("1" (ground)
(("1" (expand "singleton?")
(("1" (inst + "track(nvo)") nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (decompose-equality)
(("2" (lift-if)
(("2" (ground)
(("1" (expand "empty_seq") (("1" (assert) nil nil))
nil)
("2" (expand "empty_seq")
(("2" (case "x!1 = 0")
(("1" (replace -1)
(("1" (expand "singleton")
(("1" (propax) nil nil)) nil))
nil)
("2" (assert) nil nil))
nil))
nil)
("3" (expand "empty_seq")
(("3" (expand "singleton")
(("3" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "trk_critical") (("2" (propax) nil nil)) nil))
nil))
nil))
nil)
((trk_critical const-decl "(trk_fseq?)" bands_2D nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(fsq type-eq-decl nil fsq "structures/")
(empty_seq const-decl "fsq" fseqs "structures/")
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(< const-decl "bool" reals nil)
(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/")
(nnreal type-eq-decl nil real_types nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(pi const-decl "posreal" atan "trig_fnd/")
(nnreal_lt_2pi nonempty-type-eq-decl nil atan2 "trig_fnd/")
(track const-decl "nnreal_lt_2pi" track nil)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(default const-decl "T" fseqs "structures/")
(barray type-eq-decl nil fseqs "structures/")
(fseq type-eq-decl nil fseqs "structures/")
(ne_fseq type-eq-decl nil fseqs "structures/")
(singleton const-decl "ne_fseq" fseqs "structures/")
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(posint nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans 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)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(singleton_length formula-decl nil fseqs "structures/")
(singleton? const-decl "bool" fseqs "structures/")
(= const-decl "[T, T -> boolean]" equalities nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(addend const-decl "fseq" fseqs_ops "structures/")
(pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx "trig_fnd/")
(empty_gs_fseq name-judgement "(gs_fseq?)" bands_2D nil)
(empty_trk_fseq name-judgement "(trk_fseq?)" bands_2D nil))
shostak)
(trk_critical_rew-1 nil 3477392730
("" (skeep)
(("" (lift-if)
(("" (ground)
(("1" (expand "trk_critical")
(("1" (expand "addend")
(("1" (decompose-equality 2)
(("1" (expand "empty_seq")
(("1" (lemma "singleton_length")
(("1" (inst?)
(("1" (ground)
(("1" (replace -2) (("1" (propax) nil nil)) nil)
("2" (expand "singleton?")
(("2" (inst + "track(nvo)") nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (decompose-equality)
(("2" (lift-if)
(("2" (ground)
(("1" (expand "empty_seq") (("1" (assert) nil nil))
nil)
("2" (expand "empty_seq")
(("2" (case "x!1 = 0")
(("1" (replace -1)
(("1" (expand "singleton")
(("1" (propax) nil nil)) nil))
nil)
("2" (assert) nil nil))
nil))
nil)
("3" (expand "empty_seq")
(("3" (expand "singleton")
(("3" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "trk_critical") (("2" (propax) nil nil)) nil))
nil))
nil))
nil)
((pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx "trig_fnd/")
(addend const-decl "fseq" fseqs_ops "structures/")
(singleton? const-decl "bool" fseqs "structures/")
(singleton_length formula-decl nil fseqs "structures/")
(singleton const-decl "ne_fseq" fseqs "structures/")
(ne_fseq type-eq-decl nil fseqs "structures/")
(fseq type-eq-decl nil fseqs "structures/")
(barray type-eq-decl nil fseqs "structures/")
(default const-decl "T" fseqs "structures/")
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(track const-decl "nnreal_lt_2pi" track nil)
(nnreal_lt_2pi nonempty-type-eq-decl nil atan2 "trig_fnd/")
(pi const-decl "posreal" atan "trig_fnd/")
(Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
(zero const-decl "Vector" vectors_2D "vectors/")
(Vector type-eq-decl nil vectors_2D "vectors/")
(empty_seq const-decl "fsq" fseqs "structures/")
(fsq type-eq-decl nil fsq "structures/"))
nil))
(member_trk_critical_TCC1 0
(member_trk_critical_TCC1-1 nil 3477392567 ("" (subtype-tcc) nil nil)
((bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(empty_trk_fseq name-judgement "(trk_fseq?)" bands_2D nil)
(empty_gs_fseq name-judgement "(gs_fseq?)" bands_2D nil)
(empty_seq const-decl "fsq" fseqs "structures/")
(default const-decl "T" fseqs "structures/")
(below type-eq-decl nil naturalnumbers nil)
(trk_critical const-decl "(trk_fseq?)" bands_2D nil)
(trk_fseq? const-decl "bool" fseqs_aux_2D nil)
(gsmax formal-const-decl "posreal" bands_2D nil)
(gsmin formal-const-decl "posreal" bands_2D 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)
(fseq type-eq-decl nil fseqs "structures/")
(barray type-eq-decl nil fseqs "structures/")
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(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)
(< const-decl "bool" reals 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)
(member const-decl "bool" fseqs "structures/"))
nil))
(member_trk_critical 0
(member_trk_critical-1 nil 3477392748
("" (skeep)
(("" (expand "member")
(("" (skosimp*)
(("" (expand "trk_critical")
(("" (lift-if)
(("" (ground)
(("1" (expand "addend")
(("1" (expand "empty_seq")
(("1" (lift-if)
(("1" (ground)
(("1" (typepred "i!1")
(("1" (expand "trk_critical")
(("1" (expand "addend")
(("1" (expand "empty_seq")
(("1" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (typepred "i!1")
(("2" (expand "trk_critical")
(("2" (expand "empty_seq") (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((member const-decl "bool" fseqs "structures/")
(trk_critical const-decl "(trk_fseq?)" bands_2D nil)
(empty_trk_fseq name-judgement "(trk_fseq?)" bands_2D nil)
(empty_gs_fseq name-judgement "(gs_fseq?)" bands_2D nil)
(pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx "trig_fnd/")
(empty_seq const-decl "fsq" fseqs "structures/")
(real_lt_is_strict_total_order name-judgement
"(strict_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)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(barray type-eq-decl nil fseqs "structures/")
(fseq type-eq-decl nil fseqs "structures/")
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(gsmin formal-const-decl "posreal" bands_2D nil)
(gsmax formal-const-decl "posreal" bands_2D nil)
(trk_fseq? const-decl "bool" fseqs_aux_2D nil)
(below type-eq-decl nil naturalnumbers nil)
(addend const-decl "fseq" fseqs_ops "structures/"))
nil))
(trk_critical_composition 0
(trk_critical_composition-1 nil 3477392763
("" (skeep)
(("" (split)
(("1" (flatten)
(("1" (expand "member")
(("1" (skosimp*)
(("1" (label "xeq" -1)
(("1" (typepred "i!1")
(("1" (name "compos" "trkfs o trk_critical(nvo)")
(("1" (replace -1)
(("1" (label "composname" -1)
(("1" (expand "o")
(("1" (replace "composname" -3 :dir rl)
(("1" (assert)
(("1" (lift-if)
(("1"
(split "xeq")
(("1"
(flatten)
(("1" (inst + "i!1") nil nil))
nil)
("2"
(flatten)
(("2"
(replace "composname" :dir rl)
(("2"
(assert)
(("2"
(lemma "trk_critical_rew")
(("2"
(inst - "nvo")
(("2"
(replace -1 -2)
(("2"
(label "rew" -1)
(("2"
(hide "rew")
(("2"
(lift-if)
(("2"
(split -1)
(("1"
(flatten)
(("1"
(lemma
"singleton_length")
(("1"
(inst?)
(("1"
(case
"singleton?(singleton(track(nvo)))")
(("1"
(assert)
(("1"
(reveal
"rew")
(("1"
(assert)
(("1"
(replace
"rew"
:dir
rl)
(("1"
(replace
-3)
(("1"
(case
"i!1 = trkfs`length")
(("1"
(replace
-1)
(("1"
(replace
"rew"
"xeq")
(("1"
(expand
"singleton"
"xeq")
(("1"
(propax)
nil
nil))
nil))
nil))
nil)
("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand
"singleton?")
(("2"
(inst
+
"track(nvo)")
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(flatten)
(("2"
(expand
"trk_critical")
(("2"
(expand
"empty_seq")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (split)
(("1" (flatten)
(("1" (expand "member")
(("1" (inst + "trkfs`length")
(("1" (expand "o")
(("1" (lemma "trk_critical_rew")
(("1" (inst - "nvo")
(("1" (replace -1)
(("1" (assert)
(("1" (expand "singleton" +)
(("1" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "o")
(("2" (lemma "trk_critical_rew")
(("2" (inst - "nvo")
(("2" (replace -1) (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "member")
(("2" (skosimp*)
(("2" (inst + "i!1")
(("1" (expand "o") (("1" (propax) nil nil)) nil)
("2" (expand "o") (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((member const-decl "bool" fseqs "structures/")
(= const-decl "[T, T -> boolean]" equalities nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(empty_seq const-decl "fsq" fseqs "structures/")
(track const-decl "nnreal_lt_2pi" track nil)
(nnreal_lt_2pi nonempty-type-eq-decl nil atan2 "trig_fnd/")
(pi const-decl "posreal" atan "trig_fnd/")
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(nnreal 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/")
(singleton const-decl "ne_fseq" fseqs "structures/")
(ne_fseq type-eq-decl nil fseqs "structures/")
(pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx "trig_fnd/")
(empty_gs_fseq name-judgement "(gs_fseq?)" bands_2D nil)
(empty_trk_fseq name-judgement "(trk_fseq?)" bands_2D nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(singleton? const-decl "bool" fseqs "structures/")
(singleton_length formula-decl nil fseqs "structures/")
(trk_critical_rew formula-decl nil bands_2D nil)
(i!1 skolem-const-decl "below((trkfs o trk_critical(nvo))`length)"
bands_2D nil)
(nvo skolem-const-decl "Vect2" bands_2D nil)
(trkfs skolem-const-decl "fseq[real]" bands_2D nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_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)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(barray type-eq-decl nil fseqs "structures/")
(fseq type-eq-decl nil fseqs "structures/")
(O const-decl "fseq" fseqs "structures/")
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(gsmin formal-const-decl "posreal" bands_2D nil)
(gsmax formal-const-decl "posreal" bands_2D nil)
(trk_fseq? const-decl "bool" fseqs_aux_2D nil)
(trk_critical const-decl "(trk_fseq?)" bands_2D nil)
(below type-eq-decl nil naturalnumbers nil)
(i!1 skolem-const-decl "below(trkfs`length)" bands_2D nil))
nil))
(trk_bands_TCC1 0
(trk_bands_TCC1-2 nil 3477402860
("" (skeep)
(("" (assert)
(("" (lemma "sort_fseq_lem")
(("" (inst?)
(("" (flatten)
(("" (rewrite "sort_trk_fseq")
(("" (hide-all-but 1)
(("" (rewrite "comp_trk_fseq")
(("" (hide 2)
(("" (rewrite "comp_trk_fseq")
(("1" (hide 2)
(("1" (expand "addend")
(("1" (expand "empty_seq")
(("1" (expand "trk_fseq?")
(("1" (propax) nil nil)) nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (expand "addend")
(("2" (expand "empty_seq")
(("2" (expand "trk_fseq?")
(("2" (propax) nil nil)) nil))
nil))
nil))
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/")
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(sq_nz_pos application-judgement "posreal" sq "reals/")
(sqv_cont name-judgement "continuous_vr_fun" vect_cont_2D
"vect_analysis/")
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(empty_gs_fseq name-judgement "(gs_fseq?)" bands_2D nil)
(empty_trk_fseq name-judgement "(trk_fseq?)" bands_2D nil)
(comp_trk_fseq application-judgement "(trk_fseq?)" bands_2D nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(barray type-eq-decl nil fseqs "structures/")
(fseq type-eq-decl nil fseqs "structures/")
(O const-decl "fseq" fseqs "structures/")
(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)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(nnreal type-eq-decl nil real_types nil)
(sqv const-decl "nnreal" vectors_2D "vectors/")
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(sq const-decl "nonneg_real" sq "reals/")
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(D formal-const-decl "posreal" bands_2D nil)
(gsmin formal-const-decl "posreal" bands_2D nil)
(gsmax formal-const-decl "posreal" bands_2D nil)
(trk_fseq? const-decl "bool" fseqs_aux_2D nil)
(trk_critical const-decl "(trk_fseq?)" bands_2D nil)
(Sp_vect2 type-eq-decl nil horizontal nil)
(/= const-decl "boolean" notequal 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/")
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(zero const-decl "Vector" vectors_2D "vectors/")
(trk_only? const-decl "bool" definitions nil)
(trk_line_eps_irt const-decl
"{nvo: Vect2 | nvo /= zero => trk_only?(vo)(nvo)}" trk_line nil)
(Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
(trk_only_circle const-decl
"{nvo | nvo /= zero => trk_only?(vo)(nvo)}" trk_only nil)
(B formal-const-decl "nnreal" bands_2D nil)
(T formal-const-decl "{AB: posreal | AB > B}" bands_2D nil)
(fsq type-eq-decl nil fsq "structures/")
(empty_seq const-decl "fsq" fseqs "structures/")
(addend const-decl "fseq" fseqs_ops "structures/")
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(pi const-decl "posreal" atan "trig_fnd/")
(sort_trk_fseq judgement-tcc nil fseqs_aux_2D nil)
(comp_trk_fseq judgement-tcc nil fseqs_aux_2D nil)
(sort_fseq_lem formula-decl nil sort_fseq "structures/")
(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))
nil)
(trk_bands_TCC1-1 nil 3477392567
("" (skeep) (("" (assert) (("" (postpone) nil nil)) nil)) nil) nil
nil))
(trk_bands_not_empty 0
(trk_bands_not_empty-2 "" 3504815380
("" (skeep)
(("" (expand "trk_bands")
(("" (lift-if)
(("" (lift-if)
(("" (ground)
(("1" (expand "o")
(("1" (assert)
(("1" (expand "addend") (("1" (assert) nil nil)) nil))
nil))
nil)
("2" (expand "addend")
(("2" (expand "o") (("2" (assert) nil nil)) nil)) nil)
("3" (lift-if)
(("3" (ground)
(("1" (expand "o ")
(("1" (expand "addend")
(("1" (expand "empty_seq") (("1" (assert) nil nil))
nil))
nil))
nil)
("2" (expand "addend")
(("2" (expand "o") (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((trk_bands const-decl "{fs: (trk_fseq?) | increasing?(fs)}"
bands_2D nil)
(pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx "trig_fnd/")
(even_plus_even_is_even application-judgement "even_int" integers
nil)
(empty_seq const-decl "fsq" fseqs "structures/")
(comp_gs_fseq application-judgement "(gs_fseq?)" bands_2D nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(O const-decl "fseq" fseqs "structures/")
(addend const-decl "fseq" fseqs_ops "structures/")
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(nnint_times_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(even_times_int_is_even application-judgement "even_int" integers
nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(empty_gs_fseq name-judgement "(gs_fseq?)" bands_2D nil)
(empty_trk_fseq name-judgement "(trk_fseq?)" bands_2D nil)
(comp_trk_fseq application-judgement "(trk_fseq?)" bands_2D nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(sq_nz_pos application-judgement "posreal" sq "reals/")
(sqv_cont name-judgement "continuous_vr_fun" vect_cont_2D
"vect_analysis/")
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props 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)
(sort_length formula-decl nil sort_fseq "structures/"))
shostak)
(trk_bands_not_empty-1 nil 3481652813
("" (skeep)
(("" (expand "trk_bands")
(("" (lift-if)
(("" (lift-if)
(("" (ground)
(("1" (expand "o")
(("1" (assert)
(("1" (expand "addend") (("1" (assert) nil nil)) nil))
nil))
nil)
("2" (expand "addend")
(("2" (expand "o") (("2" (assert) nil nil)) nil)) nil)
("3" (expand "o ")
(("3" (expand "addend")
(("3" (expand "empty_seq") (("3" (assert) nil nil))
nil))
nil))
nil)
("4" (expand "addend")
(("4" (expand "o") (("4" (assert) 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/")
(empty_seq const-decl "fsq" fseqs "structures/")
(O const-decl "fseq" fseqs "structures/")
(addend 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/")
(sort_length formula-decl nil sort_fseq "structures/"))
shostak))
(trk_bands_critical 0
(trk_bands_critical-1 nil 3477392783
("" (skeep)
(("" (expand "trk_bands")
(("" (rewrite "member_sort" :dir rl)
(("" (rewrite "member_composition")
(("" (rewrite "member_composition")
(("" (rewrite "member_composition")
(("" (split)
(("1" (flatten)
(("1" (case "to2pi(trk2) /= 0")
(("1" (assert)
(("1" (case "trk2 < 2*pi")
(("1" (flatten)
(("1" (lemma "to2pi_id")
(("1" (inst - "trk2")
(("1"
(lemma "track_id")
(("1"
(inst - "norm(vo)" "trk2")
(("1"
(expand "trk_critical?")
(("1"
(split -)
(("1"
(flatten)
(("1"
(assert)
(("1"
(hide (3 4 5 6 7))
(("1"
(rewrite
"trk_critical_composition")
(("1"
(rewrite
"trk_critical_composition")
(("1"
(rewrite
"trk_critical_composition")
(("1"
(rewrite
"trk_critical_composition")
(("1"
(rewrite
"trk_critical_composition")
(("1"
(flatten)
(("1"
(expand
"trk_line?")
(("1"
(skosimp*)
(("1"
(case
"(trk_line_eps_irt(s, vo, vi, -1, -1) /= zero AND
trk2 = track(trk_line_eps_irt(s, vo, vi, -1, -1)))")
(("1"
(flatten)
(("1"
(expand
"member")
(("1"
(inst
+
"0")
(("1"
(expand
"trk_critical")
(("1"
(expand
"addend")
(("1"
(expand
"empty_seq")
(("1"
(assert)
nil
nil))
nil))
nil))
nil)
("2"
(expand
"trk_critical")
(("2"
(expand
"empty_seq")
(("2"
(expand
"addend")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand
"trk2v2")
(("2"
(lemma
"trkgs2vect_id")
(("2"
(inst
-
"trk_line_eps_irt(s, vo, vi, eps!1, irt!1)")
(("1"
(typepred
"irt!1")
(("1"
(typepred
"eps!1")
(("1"
(split
-)
(("1"
(split
-)
(("1"
(assert)
nil
nil)
("2"
(assert)
nil
nil))
nil)
("2"
(split
-)
(("1"
(assert)
nil
nil)
("2"
(assert)
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)
("2"
(case "sqv(s) >= sq(D)")
(("1"
(assert)
(("1"
(hide (3 4 5 6 7))
(("1"
(rewrite
"trk_critical_composition")
(("1"
(rewrite
"trk_critical_composition")
(("1"
(rewrite
"trk_critical_composition")
(("1"
(rewrite
"trk_critical_composition")
(("1"
(rewrite
"trk_critical_composition")
(("1"
(flatten)
(("1"
(expand
"trk_only_circle?")
(("1"
(skosimp*)
(("1"
(expand
"trk2v2")
(("1"
(lemma
"trkgs2vect_id")
(("1"
(inst
-
"trk_only_circle(s, vo, vi, T, -1, irt!1)")
(("1"
(typepred
"irt!1")
(("1"
(split
-)
(("1"
(assert)
nil
nil)
("2"
(assert)
nil
nil))
nil))
nil)
("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(lemma
"trk_only_circle_solution")
(("2"
(inst
-
"-1"
"trk2v2(vo)(trk2)"
"s"
"T"
"vi"
"vo")
(("2"
(assert)
(("2"
(lemma
"circle_solution_2D_horizontal_sep")
(("2"
(inst?)
(("2"
(assert)
(("2"
(inst - "0")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3"
(assert)
(("3"
(hide (2 4 5 6 7))
(("3"
(flatten)
(("3"
(assert)
(("3"
(rewrite
"trk_critical_composition")
(("3"
(flatten)
(("3"
(case
"(trk_only_circle(s, vo, vi, B, 1, -1) /= zero AND
trk2 = track(trk_only_circle(s, vo, vi, B, 1, -1)))")
(("1"
(flatten)
(("1"
(expand
"member")
(("1"
(inst + "0")
(("1"
(expand
"trk_critical")
(("1"
(expand
"addend")
(("1"
(expand
"empty_seq")
(("1"
(assert)
nil
nil))
nil))
nil))
nil)
("2"
(expand
"trk_critical")
(("2"
(expand
"addend")
(("2"
(expand
"empty_seq")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand
"trk_only_circle?")
(("2"
(skosimp*)
(("2"
(lemma
"trkgs2vect_id")
(("2"
(inst
-
"trk_only_circle(s, vo, vi, B, 1, irt!1)")
(("1"
(expand
"trk2v2")
(("1"
(typepred
"irt!1")
(("1"
(split
-)
(("1"
(assert)
nil
nil)
("2"
(assert)
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" (hide-all-but (-1 1))
(("2" (typepred "trk2")
(("2" (case "trk2 = 2*pi")
(("1"
(replace -1)
(("1"
(expand "to2pi")
(("1" (grind) nil nil))
nil))
nil)
("2" (assert) nil nil))
nil))
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.83 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.
|
