| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/ACCoRD/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 338 kB |
|
SSL bands_2D.prfInteraktion undPortierbarkeitLisp |
|||||||||||||||
|
(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)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (hide-all-but (-1 3 4)) (("2" (case "trk2 = 0 or trk2 = 2*pi") (("1" (expand "member") (("1" (inst + "0") (("1" (inst + "0") (("1" (expand "addend") (("1" (expand "empty_seq") (("1" (assert) nil nil)) nil)) nil) ("2" (expand "addend") (("2" (expand "empty_seq") (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (expand "addend") (("2" (expand "empty_seq") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (typepred "trk2") (("2" (case "trk2 < 2*pi") (("1" (lemma "to2pi_id") (("1" (inst - "trk2") (("1" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (expand "trk_critical?") (("2" (assert) (("2" (flatten) (("2" (expand "trk_line?") (("2" (assert) (("2" (expand "trk_only_circle?") (("2" (expand "trk2v2") (("2" (assert) (("2" (label "tl" 1) (("2" (label "toc" 2) (("2" (label "tocb" 3) (("2" (split -) (("1" (lift-if) (("1" (split -) (("1" (flatten) (("1" (assert) (("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" (split -) (("1" (flatten) (("1" (inst + "1") (("1" (replace -1) (("1" (typepred "trk_only_circle(s, vo, vi, T, -1, 1)") (("1" (assert) (("1" (expand "trk_only?") (("1" (replace -1 :dir rl) (("1" (rewrite "trkgs2vect_id") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (inst + "-1") (("2" (replace -1) (("2" (typepred "trk_only_circle(s, vo, vi, T, -1, -1)") (("2" (assert) (("2" (expand "trk_only?") (("2" (replace -1 :dir rl) (("2" (rewrite "trkgs2vect_id") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (flatten) (("3" (inst + "1" "1") (("3" (replace -1) (("3" (typepred "trk_line_eps_irt(s, vo, vi, 1, 1)") (("3" (assert) (("3" (expand "trk_only?") (("3" (replace -1 :dir rl) (("3" (rewrite "trkgs2vect_id") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (flatten) (("4" (inst + "1" "-1") (("4" (replace -1) (("4" (typepred "trk_line_eps_irt(s, vo, vi, 1, -1)") (("4" (assert) (("4" (expand "trk_only?") (("4" (replace -1 :dir rl) (("4" (rewrite "trkgs2vect_id") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("5" (flatten) (("5" (inst + "-1" "1") (("5" (replace -1) (("5" (typepred "trk_line_eps_irt(s, vo, vi, -1, 1)") (("5" (assert) (("5" (expand "trk_only?") (("5" (replace -1 :dir rl) (("5" (rewrite "trkgs2vect_id") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("6" (lemma "member_trk_critical") (("6" (inst?) (("6" (assert) (("6" (lemma "trkgs2vect_id") (("6" (inst?) (("6" (typepred "trk_line_eps_irt(s, vo, vi, -1, -1)") (("6" (split -1) (("1" (expand "trk_only?") (("1" (inst + "-1" "-1") (("1" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (expand "member") (("2" (skosimp*) (("2" (typepred "i!1") (("2" (expand "empty_seq") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lift-if) (("2" (split -) (("1" (flatten) (("1" (rewrite "trk_critical_composition") (("1" (split -) (("1" (flatten) (("1" (assert) (("1" (inst + "1") (("1" (inst + "1") (("1" (replace -1) (("1" (typepred "trk_only_circle(s, vo, vi, B, 1, 1)") (("1" (assert) (("1" (expand "trk_only?") (("1" (replace -1 :dir rl) (("1" (rewrite "trkgs2vect_id") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (lemma "member_trk_critical") (("2" (inst?) (("2" (assert) (("2" (replace -1) (("2" (inst + "-1") (("2" (inst + "-1") (("2" (typepred "trk_only_circle(s, vo, vi, B, 1, -1)") (("2" (split -1) (("1" (expand "trk_only?") (("1" (replace -1 :dir rl) (("1" (rewrite "trkgs2vect_id") nil nil)) nil)) nil) ("2" (flatten) (("2" (replace -1) (("2" (expand "trk_critical") (("2" (expand "member") (("2" (skosimp*) (("2" (typepred "i!1") (("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) ("2" (flatten) (("2" (expand "member") (("2" (skosimp*) (("2" (typepred "i!1") (("2" (expand "empty_seq") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "member") (("3" (skosimp*) (("3" (case "i!1 = 0") (("1" (replace -1) (("1" (expand "addend") (("1" (expand "empty_seq") (("1" (replace -2) (("1" (expand "to2pi") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "i!1") (("2" (expand "addend") (("2" (expand "empty_seq") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (expand "member") (("4" (skosimp*) (("4" (case "i!1 = 0") (("1" (replace -1) (("1" (expand "addend") (("1" (expand "empty_seq") (("1" (replace -2) (("1" (expand "to2pi") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "i!1") (("2" (expand "addend") (("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) ((trk_bands const-decl "{fs: (trk_fseq?) | increasing?(fs)}" bands_2D nil) (member_composition formula-decl nil fseqs "structures/") (member_trk_critical formula-decl nil bands_2D nil) (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (real_times_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (atan_value const-decl "real" atan "trig_fnd/") (Integral const-decl "real" integral_def "analysis/") (nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (trk2 skolem-const-decl "{r: real | 0 <= r AND r <= 2 * pi}" bands_2D nil) (nz_norm_gt_0 application-judgement "posreal" vectors_2D "vectors/") (norm const-decl "nnreal" vectors_2D "vectors/") (trk2v2_continuous application-judgement "continuous_rv_fun" trk_bands_2D nil) (trk_critical_composition formula-decl nil bands_2D nil) (trk_line? const-decl "bool" trk_line nil) (track const-decl "nnreal_lt_2pi" track nil) (member const-decl "bool" fseqs "structures/") (below type-eq-decl nil naturalnumbers nil) (vi skolem-const-decl "Nz_vect2" bands_2D nil) (vo skolem-const-decl "Nz_vect2" bands_2D nil) (s skolem-const-decl "Vect2" bands_2D nil) (trkgs2vect_id formula-decl nil track nil) (NOT const-decl "[bool -> bool]" booleans nil) (irt!1 skolem-const-decl "Sign" bands_2D nil) (eps!1 skolem-const-decl "Sign" bands_2D nil) (trk2v2 const-decl "(trk_only?(vo2))" bands_util nil) (trk_only_circle_solution formula-decl nil trk_only nil) (- const-decl "Vector" vectors_2D "vectors/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (add_zero_right formula-decl nil vectors_2D "vectors/") (scal_0 formula-decl nil vectors_2D "vectors/") (circle_solution_2D_horizontal_sep formula-decl nil horizontal nil) (trk_only_circle? const-decl "bool" trk_only nil) (irt!1 skolem-const-decl "Sign" bands_2D nil) (irt!1 skolem-const-decl "Sign" bands_2D nil) (trk_critical? const-decl "bool" trk_bands_2D nil) (trk2v2_Nzv application-judgement "Nz_vect2" bands_util nil) (track_id formula-decl nil track nil) (to2pi_id formula-decl nil to2pi "trig_fnd/") (to2pi const-decl "nnreal_lt_2pi" to2pi "trig_fnd/") (nnreal_lt_2pi nonempty-type-eq-decl nil atan2 "trig_fnd/") (< const-decl "bool" reals nil) (comp_trk_fseq application-judgement "(trk_fseq?)" bands_2D nil) (real_ge_is_total_order name-judgement "(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/") (real_gt_is_strict_total_order name-judgement "(strict_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) (AND const-decl "[bool, bool -> bool]" booleans nil) (pi const-decl "posreal" atan "trig_fnd/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (addend const-decl "fseq" fseqs_ops "structures/") (empty_seq const-decl "fsq" fseqs "structures/") (fsq type-eq-decl nil fsq "structures/") (T formal-const-decl "{AB: posreal | AB > B}" bands_2D nil) (B formal-const-decl "nnreal" bands_2D nil) (trk_only_circle const-decl "{nvo | nvo /= zero => trk_only?(vo)(nvo)}" trk_only nil) (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (trk_line_eps_irt const-decl "{nvo: Vect2 | nvo /= zero => trk_only?(vo)(nvo)}" trk_line nil) (trk_only? const-decl "bool" definitions nil) (zero const-decl "Vector" vectors_2D "vectors/") (IMPLIES const-decl "[bool, bool -> bool]" booleans 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) (/= const-decl "boolean" notequal nil) (Sp_vect2 type-eq-decl nil horizontal 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) (D formal-const-decl "posreal" bands_2D nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (sq const-decl "nonneg_real" sq "reals/") (nonneg_real nonempty-type-eq-decl nil real_types nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (sqv const-decl "nnreal" vectors_2D "vectors/") (nnreal type-eq-decl nil real_types nil) (Vector type-eq-decl nil vectors_2D "vectors/") (IF const-decl "[boolean, T, T -> T]" if_def 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) (O const-decl "fseq" fseqs "structures/") (fseq type-eq-decl nil fseqs "structures/") (barray type-eq-decl nil fseqs "structures/") (nat nonempty-type-eq-decl nil naturalnumbers nil) (member_sort formula-decl nil sort_fseq "structures/") (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) (minus_odd_is_odd application-judgement "odd_int" integers nil) (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}" atan_approx "trig_fnd/")) nil)) (gs_critical_TCC1 0 (gs_critical_TCC1-1 nil 3477392567 ("" (skeep) (("" (expand "gs_fseq?") (("" (skosimp*) (("" (expand "addend") (("" (expand "empty_seq") (("" (lift-if) (("" (typepred "i!1") (("" (expand "addend") (("" (expand "empty_seq") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((gs_fseq? const-decl "bool" fseqs_aux_2D nil) (addend 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) (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/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (nnreal type-eq-decl nil real_types nil) (gs const-decl "nnreal" definitions nil) (fsq type-eq-decl nil fsq "structures/") (below type-eq-decl nil naturalnumbers nil) (empty_seq const-decl "fsq" fseqs "structures/")) nil)) (gs_critical_TCC2 0 (gs_critical_TCC2-1 nil 3477392567 ("" (skeep) (("" (hide 1) (("" (ground) (("1" (skosimp*) (("1" (expand "emptyseq") (("1" (expand "empty_seq") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (expand "gs_fseq?") (("2" (skosimp*) (("2" (typepred "i!1") (("2" (expand "emptyseq") (("2" (expand "empty_seq") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((gs_fseq? const-decl "bool" fseqs_aux_2D nil) (below type-eq-decl nil naturalnumbers nil) (fsq type-eq-decl nil fsq "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) (empty_seq const-decl "fsq" fseqs "structures/") (emptyseq macro-decl "fsq" fseqs "structures/")) nil)) (gs_critical_rew 0 (gs_critical_rew-2 "" 3504827928 ("" (skeep) (("" (lift-if) (("" (ground) (("1" (expand "gs_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 + "gs(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 "gs_critical") (("2" (propax) nil nil)) nil) ("3" (expand "gs_critical") (("3" (propax) nil nil)) nil) ("4" (expand "gs_critical") (("4" (propax) nil nil)) nil)) nil)) nil)) nil) ((gs_critical const-decl "(gs_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) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (nnreal type-eq-decl nil real_types nil) (gs const-decl "nnreal" definitions nil) (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/") (empty_gs_fseq name-judgement "(gs_fseq?)" bands_2D nil) (empty_trk_fseq name-judgement "(trk_fseq?)" bands_2D nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil)) shostak) (gs_critical_rew-1 nil 3477392799 ("" (skeep) (("" (lift-if) (("" (ground) (("1" (expand "gs_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))) ("2" (expand "singleton?") (("2" (inst + "gs(nvo)") nil))))))))))) ("2" (decompose-equality) (("2" (lift-if) (("2" (ground) (("1" (expand "empty_seq") (("1" (assert) nil))) ("2" (expand "empty_seq") (("2" (case "x!1 = 0") (("1" (replace -1) (("1" (expand "singleton") (("1" (propax) nil))))) ("2" (assert) nil))))) ("3" (expand "empty_seq") (("3" (expand "singleton") (("3" (propax) nil))))))))))))))))) ("2" (expand "gs_critical") (("2" (propax) nil))) ("3" (expand "gs_critical") (("3" (propax) nil))) ("4" (expand "gs_critical") (("4" (propax) nil)))))))) nil) ((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/") (gs const-decl "nnreal" definitions nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (empty_seq const-decl "fsq" fseqs "structures/") (fsq type-eq-decl nil fsq "structures/")) nil)) (member_gs_critical 0 (member_gs_critical-1 nil 3477392821 ("" (skeep) (("" (expand "member") (("" (skosimp*) (("" (expand "gs_critical") (("" (lift-if) (("" (ground) (("1" (expand "addend") (("1" (expand "empty_seq") (("1" (lift-if) (("1" (ground) (("1" (typepred "i!1") (("1" (expand "gs_critical") (("1" (expand "addend") (("1" (expand "empty_seq") (("1" (propax) nil))))))))))))))))) ("2" (typepred "i!1") (("2" (expand "gs_critical") (("2" (expand "empty_seq") (("2" (assert) nil))))))) ("3" (typepred "i!1") (("3" (expand "gs_critical") (("3" (expand "empty_seq") (("3" (assert) nil))))))) ("4" (typepred "i!1") (("4" (expand "gs_critical") (("4" (expand "empty_seq") (("4" (assert) nil)))))))))))))))))) nil) ((member const-decl "bool" fseqs "structures/") (gs_critical const-decl "(gs_fseq?)" bands_2D nil) (real_le_is_total_order name-judgement "(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/") (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) (gs_fseq? const-decl "bool" fseqs_aux_2D nil) (below type-eq-decl nil naturalnumbers nil) (addend const-decl "fseq" fseqs_ops "structures/")) nil)) (gs_critical_composition 0 (gs_critical_composition-1 nil 3477392834 ("" (skeep) (("" (split) (("1" (flatten) (("1" (expand "member") (("1" (skosimp*) (("1" (label "xeq" -1) (("1" (typepred "i!1") (("1" (name "compos" "gsfs o gs_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))) ("2" (flatten) (("2" (replace "composname" :dir rl) (("2" (assert) (("2" (lemma "gs_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(gs(nvo)))") (("1" (assert) (("1" (reveal "rew") (("1" (assert) (("1" (replace "rew" :dir rl) (("1" (replace -3) (("1" (case "i!1 = gsfs`length") (("1" (replace -1) (("1" (replace "rew" "xeq") (("1" (assert) (("1" (expand "singleton") (("1" (propax) nil))))))))) ("2" (assert) nil))))))))))))) ("2" (expand "singleton?") (("2" (inst + "gs(nvo)") nil))))))))))) ("2" (flatten) (("2" (expand "gs_critical") (("2" (lift-if) (("2" (replace 1) (("2" (expand "empty_seq") (("2" (propax) nil))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ("2" (flatten) (("2" (split) (("1" (flatten) (("1" (expand "member") (("1" (inst + "gsfs`length") (("1" (expand "o") (("1" (lemma "gs_critical_rew") (("1" (inst - "nvo") (("1" (replace -1) (("1" (assert) (("1" (expand "singleton" +) (("1" (propax) nil))))))))))))) ("2" (expand "o") (("2" (lemma "gs_critical_rew") (("2" (inst - "nvo") (("2" (replace -1) (("2" (assert) nil))))))))))))))) ("2" (expand "member") (("2" (skosimp*) (("2" (inst + "i!1") (("1" (expand "o") (("1" (propax) nil))) ("2" (expand "o") (("2" (assert) nil)))))))))))))))) nil) ((member const-decl "bool" fseqs "structures/") (comp_gs_fseq application-judgement "(gs_fseq?)" bands_2D nil) (= const-decl "[T, T -> boolean]" equalities nil) (int_minus_int_is_int application-judgement "int" integers nil) (empty_seq const-decl "fsq" fseqs "structures/") (gs const-decl "nnreal" definitions nil) (nnreal type-eq-decl nil real_types nil) (singleton const-decl "ne_fseq" fseqs "structures/") (ne_fseq type-eq-decl nil fseqs "structures/") (real_le_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) (minus_odd_is_odd application-judgement "odd_int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (singleton? const-decl "bool" fseqs "structures/") (singleton_length formula-decl nil fseqs "structures/") (gs_critical_rew formula-decl nil bands_2D nil) (i!1 skolem-const-decl "below((gsfs o gs_critical(nvo))`length)" bands_2D nil) (nvo skolem-const-decl "Vect2" bands_2D nil) (gsfs skolem-const-decl "(gs_fseq?)" 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/") (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) (gs_fseq? const-decl "bool" fseqs_aux_2D nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (gs_critical const-decl "(gs_fseq?)" bands_2D nil) (below type-eq-decl nil naturalnumbers nil) (i!1 skolem-const-decl "below(gsfs`length)" bands_2D nil)) nil)) (gs_bands_TCC1 0 (gs_bands_TCC1-2 nil 3477403072 ("" (skosimp*) (("" (hide-all-but 2) (("" (grind) nil nil)) nil)) nil) ((empty_gs_fseq name-judgement "(gs_fseq?)" bands_2D nil) (empty_trk_fseq name-judgement "(trk_fseq?)" bands_2D nil) (gs_fseq? const-decl "bool" fseqs_aux_2D 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) (gsmin formal-const-decl "posreal" bands_2D nil) (gsmax formal-const-decl "posreal" bands_2D nil) (empty_seq const-decl "fsq" fseqs "structures/") (default const-decl "T" fseqs "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)) nil) (gs_bands_TCC1-1 nil 3477392567 ("" (subtype-tcc) nil nil) nil nil)) (gs_bands_TCC2 0 (gs_bands_TCC2-1 nil 3563728607 ("" (skosimp*) (("" (hide-all-but 2) (("" (grind) nil nil)) nil)) nil) ((empty_gs_fseq name-judgement "(gs_fseq?)" bands_2D nil) (empty_trk_fseq name-judgement "(trk_fseq?)" bands_2D nil) (gs_fseq? const-decl "bool" fseqs_aux_2D 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) (gsmin formal-const-decl "posreal" bands_2D nil) (gsmax formal-const-decl "posreal" bands_2D nil) (empty_seq const-decl "fsq" fseqs "structures/") (default const-decl "T" fseqs "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) (sq_nz_pos application-judgement "posreal" sq "reals/") (nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/")) nil)) (gs_bands_TCC3 0 (gs_bands_TCC3-1 nil 3563728607 ("" (skosimp*) (("" (hide-all-but 1) (("" (grind) nil nil)) nil)) 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/") (empty_gs_fseq name-judgement "(gs_fseq?)" bands_2D nil) (empty_trk_fseq name-judgement "(trk_fseq?)" bands_2D nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/")) nil)) (gs_bands_TCC4 0 (gs_bands_TCC4-2 nil 3563805843 ("" (skeep) (("" (assert) (("" (rewrite "sort_gs_fseq") (("" (hide-all-but 1) (("" (rewrite "comp_gs_fseq") (("" (hide 2) (("" (rewrite "comp_gs_fseq") (("1" (hide 2) (("1" (expand "addend") (("1" (expand "empty_seq") (("1" (expand "gs_fseq?") (("1" (lemma "gs_min_lt_max") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "addend") (("2" (expand "empty_seq") (("2" (expand "gs_fseq?") (("2" (lemma "gs_min_lt_max") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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_gs_fseq application-judgement "(gs_fseq?)" bands_2D nil) (gs_min_lt_max formula-decl nil bands_2D nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (comp_gs_fseq judgement-tcc nil 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) (>= 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) (addend const-decl "fseq" fseqs_ops "structures/") (empty_seq const-decl "fsq" fseqs "structures/") (fsq type-eq-decl nil fsq "structures/") (T formal-const-decl "{AB: posreal | AB > B}" bands_2D nil) (B formal-const-decl "nnreal" bands_2D nil) (gs_only_circle const-decl "{nvo | nvo /= zero => gs_only?(vnzo)(nvo)}" gs_only nil) (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (gs_line_eps const-decl "{nvo | nvo /= zero => gs_only?(vo)(nvo)}" gs_line nil) (gs_only? const-decl "bool" definitions nil) (zero const-decl "Vector" vectors_2D "vectors/") (IMPLIES const-decl "[bool, bool -> bool]" booleans 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) (/= const-decl "boolean" notequal nil) (Sp_vect2 type-eq-decl nil horizontal nil) (gs_critical const-decl "(gs_fseq?)" bands_2D nil) (D formal-const-decl "posreal" bands_2D nil) (sq const-decl "nonneg_real" sq "reals/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (sqv const-decl "nnreal" vectors_2D "vectors/") (nnreal type-eq-decl nil real_types nil) (Vector type-eq-decl nil vectors_2D "vectors/") (IF const-decl "[boolean, T, T -> T]" if_def 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) (O const-decl "fseq" fseqs "structures/") (gs_fseq? const-decl "bool" fseqs_aux_2D nil) (fseq type-eq-decl nil fseqs "structures/") (barray type-eq-decl nil fseqs "structures/") (nat nonempty-type-eq-decl nil naturalnumbers nil) (sort_gs_fseq judgement-tcc nil fseqs_aux_2D nil) (minus_odd_is_odd application-judgement "odd_int" integers nil)) nil) (gs_bands_TCC4-1 nil 3563728607 ("" (subtype-tcc) nil nil) nil nil)) (gs_bands_not_empty 0 (gs_bands_not_empty-2 "" 3504828021 ("" (skeep) (("" (expand "gs_bands") (("" (lift-if) (("" (lift-if) (("" (ground) (("1" (expand "addend") (("1" (expand "o") (("1" (assert) nil nil)) nil)) nil) ("2" (expand "addend") (("2" (expand "o") (("2" (assert) nil nil)) nil)) nil) ("3" (lift-if) (("3" (ground) (("1" (expand "addend") (("1" (expand "o") (("1" (assert) nil nil)) nil)) nil) ("2" (expand "addend") (("2" (expand "o") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((gs_bands const-decl "{fs: (gs_fseq?) | increasing?(fs)}" bands_2D nil) (even_plus_even_is_even application-judgement "even_int" integers nil) (comp_trk_fseq application-judgement "(trk_fseq?)" bands_2D nil) (addend const-decl "fseq" fseqs_ops "structures/") (O const-decl "fseq" fseqs "structures/") (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (even_times_int_is_even application-judgement "even_int" integers nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (empty_gs_fseq name-judgement "(gs_fseq?)" bands_2D nil) (empty_trk_fseq name-judgement "(trk_fseq?)" bands_2D nil) (comp_gs_fseq application-judgement "(gs_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) (sort_length 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)) shostak) (gs_bands_not_empty-1 nil 3481653002 ("" (skeep) (("" (expand "gs_bands") (("" (lift-if) (("" (lift-if) (("" (ground) (("1" (expand "addend") (("1" (expand "o") (("1" (assert) nil nil)) nil)) nil) ("2" (expand "addend") (("2" (expand "o") (("2" (assert) nil nil)) nil)) nil) ("3" (expand "addend") (("3" (expand "o") (("3" (assert) nil nil)) nil)) nil) ("4" (expand "addend") (("4" (expand "o") (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((addend const-decl "fseq" fseqs_ops "structures/") (O const-decl "fseq" fseqs "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)) (gs_bands_critical_TCC1 0 (gs_bands_critical_TCC1-1 nil 3477392567 ("" (skeep) (("" (typepred "gsp") (("" (typepred "gsmin") (("" (assert) nil nil)) nil)) nil)) nil) ((gsmax formal-const-decl "posreal" bands_2D nil) (AND const-decl "[bool, bool -> bool]" booleans 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) (<= 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_le_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) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (gs_bands_critical 0 (gs_bands_critical-2 nil 3477398303 ("" (skeep) (("" (case "gsp = gs(gs2v2(vo)(gsp))") (("1" (case "gs2v2(vo)(gsp) /= zero") (("1" (flatten) (("1" (expand "gs_bands") (("1" (rewrite "member_sort" :dir rl) (("1" (rewrite "member_composition") (("1" (rewrite "member_composition") (("1" (rewrite "member_composition") (("1" (split) (("1" (flatten) (("1" (split -) (("1" (expand "gs_critical?") (("1" (split -) (("1" (flatten) (("1" (assert) (("1" (hide (2 3 4 4 5 6 7)) (("1" (rewrite "gs_critical_composition") (("1" (rewrite "gs_critical_composition") (("1" (rewrite "gs_critical_composition") (("1" (flatten) (("1" (case "(gs_line_eps(s, vo, vi, -1) /= zero AND gsp = gs(gs_line_eps(s, vo, vi, -1)) AND gsmin <= gs(gs_line_eps(s, vo, vi, -1)) AND gs(gs_line_eps(s, vo, vi, -1)) <= gsmax)") (("1" (flatten) (("1" (expand "member") (("1" (inst + "0") (("1" (expand "gs_critical") (("1" (expand "empty_seq") (("1" (expand "addend") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (expand "gs_critical") (("2" (expand "empty_seq") (("2" (expand "addend") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "gs_line?") (("2" (skosimp*) (("2" (typepred "eps!1") (("2" (typepred "gs_line_eps(s,vo,vi,eps!1)") (("2" (assert) (("2" (lemma "gs2v2_id") (("2" (inst?) (("2" (assert) (("2" (replace -6 -1 :dir rl) (("2" (split -) (("1" (assert) nil nil) ("2" (case "gsp = gs(gs2v2(vo)(gsp))") (("1" (assert) nil nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "gs_only_circle_solution") (("2" (inst?) (("2" (assert) (("2" (lemma "circle_solution_2D_horizontal_sep") (("2" (inst?) (("2" (assert) (("2" (inst - "0") (("2" (assert) (("2" (hide (2 3 4 4 5 6 7)) (("2" (rewrite "gs_critical_composition") (("2" (rewrite "gs_critical_composition") (("2" (rewrite "gs_critical_composition") (("2" (flatten) (("2" (expand "gs_only_circle?") (("2" (skosimp*) (("2" (typepred "irt!1") (("2" (typepred "gs_only_circle(s, vo, vi, T, -1, irt!1)") (("2" (assert) (("2" (split -) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (flatten) (("3" (assert) (("3" (hide (1 3 4 5 6 7)) (("3" (rewrite "gs_critical_composition") (("3" (flatten) (("3" (case "(gs_only_circle(s, vo, vi, B, 1, -1) /= zero AND gsp = gs(gs_only_circle(s, vo, vi, B, 1, -1)) AND gsmin <= gs(gs_only_circle(s, vo, vi, B, 1, -1)) AND gs(gs_only_circle(s, vo, vi, B, 1, -1)) <= gsmax)") (("1" (flatten) (("1" (expand "member") (("1" (inst + "0") (("1" (expand "gs_critical") (("1" (expand "empty_seq") (("1" (expand "addend") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (expand "gs_critical") (("2" (expand "empty_seq") (("2" (expand "addend") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "gs_only_circle?") (("2" (skosimp*) (("2" (typepred "irt!1") (("2" (split -) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide (1 2 4)) (("2" (expand "member") (("2" (inst + "0") (("1" (expand "addend") (("1" (expand "empty_seq") (("1" (propax) nil nil)) nil)) nil) ("2" (expand "addend") (("2" (expand "empty_seq") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide (1 2 3)) (("3" (expand "member") (("3" (inst + "0") (("1" (expand "addend") (("1" (expand "empty_seq") (("1" (propax) nil nil)) nil)) nil) ("2" (expand "addend") (("2" (expand "empty_seq") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (split -) (("1" (lift-if) (("1" (split -) (("1" (flatten) (("1" (rewrite "gs_critical_composition") (("1" (rewrite "gs_critical_composition") (("1" (rewrite "gs_critical_composition") (("1" (expand "gs_critical?") (("1" (flatten) (("1" (assert) (("1" (split -) (("1" (flatten) (("1" (expand "gs_only_circle?") (("1" (assert) (("1" (inst + "1") (("1" (lemma "gs2v2_id") (("1" (inst - "gs_only_circle(s, vo, vi, T, -1, 1)" "vo") (("1" (assert) (("1" (typepred "gs_only_circle(s, vo, vi, T, -1, 1)") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (expand "gs_only_circle?") (("2" (inst + "-1") (("2" (lemma "gs2v2_id") (("2" (inst - "gs_only_circle(s, vo, vi, T, -1, -1)" "vo") (("1" (typepred "gs_only_circle(s, vo, vi, T, -1, -1)") (("1" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (flatten) (("3" (expand "gs_line?") (("3" (inst + "1") (("3" (lemma "gs2v2_id") (("3" (inst - "gs_line_eps(s, vo, vi, 1)" "vo") (("1" (typepred "gs_line_eps(s, vo, vi, 1)") (("1" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("4" (lemma "member_gs_critical") (("4" (inst - "gs_line_eps(s, vo, vi, -1)" "gsp") (("4" (assert) (("4" (expand "gs_line?") (("4" (inst + "-1") (("4" (lemma "gs2v2_id") (("4" (inst - "gs_line_eps(s, vo, vi, -1)" "vo") (("1" (assert) (("1" (typepred "gs_line_eps(s, vo, vi, -1)") (("1" (assert) (("1" (flatten) (("1" (replace -1) (("1" (expand "gs_critical") (("1" (expand "member") (("1" (skosimp*) (("1" (typepred "i!1") (("1" (expand "empty_seq") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (replace -1) (("2" (expand "gs_critical") (("2" (expand "member") (("2" (skosimp*) (("2" (typepred "i!1") (("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) ("2" (flatten) (("2" (expand "member") (("2" (skosimp*) (("2" (typepred "i!1") (("2" (expand "empty_seq") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lift-if) (("2" (split -) (("1" (flatten) (("1" (rewrite "gs_critical_composition") (("1" (split -) (("1" (flatten) (("1" (expand "gs_critical?") (("1" (flatten) (("1" (expand "gs_only_circle?") (("1" (assert) (("1" (inst + "1") (("1" (inst + "1") (("1" (lemma "gs2v2_id") (("1" (inst - "gs_only_circle(s, vo, vi, B, 1, 1)" "vo") (("1" (typepred "gs_only_circle(s, vo, vi, B, 1, 1)") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "gsp = gs(gs_only_circle(s, vo, vi, B, 1, -1))") (("1" (expand "gs_critical?") (("1" (flatten) (("1" (assert) (("1" (expand "gs_only_circle?") (("1" (inst + "-1") (("1" (inst + "-1") (("1" (lemma "gs2v2_id") (("1" (inst - "gs_only_circle(s, vo, vi, B, 1, -1)" "vo") (("1" (assert) (("1" (typepred "gs_only_circle(s, vo, vi, B, 1, -1)") (("1" (assert) (("1" (flatten) (("1" (replace -1) (("1" (expand "gs") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (replace -1) (("2" (expand "gs") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "member_gs_critical") nil nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (expand "member") (("2" (skosimp*) (("2" (typepred "i!1") (("2" (expand "empty_seq") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "member") (("3" (skosimp*) (("3" (typepred "i!1") (("3" (case "i!1 = 0") (("1" (replace -1) (("1" (expand "addend") (("1" (expand "empty_seq") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (expand "addend") (("2" (expand "empty_seq") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (expand "member") (("4" (skosimp*) (("4" (typepred "i!1") (("4" (case "i!1 = 0") (("1" (replace -1) (("1" (expand "addend") (("1" (expand "empty_seq") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (expand "addend") (("2" (expand "empty_seq") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "gs") (("2" (flatten) (("2" (replace -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "gs2v2") (("2" (expand "^") (("2" (expand "gs") (("2" (rewrite "norm_scal") (("2" (rewrite "norm_scal") (("2" (expand "abs") (("2" (lift-if) (("2" (assert) (("2" (typepred "gsp") (("2" (typepred "gsmin") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((gs2v2 const-decl "Vect2" bands_util 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/") (gs const-decl "nnreal" definitions nil) (nnreal type-eq-decl nil real_types nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (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) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans 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) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (empty_trk_fseq name-judgement "(trk_fseq?)" bands_2D nil) (empty_gs_fseq name-judgement "(gs_fseq?)" bands_2D nil) (member_sort formula-decl nil sort_fseq "structures/") (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) (IF const-decl "[boolean, T, T -> T]" if_def nil) (sqv const-decl "nnreal" vectors_2D "vectors/") (sq const-decl "nonneg_real" sq "reals/") (D formal-const-decl "posreal" bands_2D nil) (gs_fseq? const-decl "bool" fseqs_aux_2D nil) (gs_critical const-decl "(gs_fseq?)" bands_2D nil) (Sp_vect2 type-eq-decl nil horizontal nil) (nzint nonempty-type-eq-decl nil integers nil) (OR const-decl "[bool, bool -> bool]" booleans 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) (gs_only? const-decl "bool" definitions nil) (gs_line_eps const-decl "{nvo | nvo /= zero => gs_only?(vo)(nvo)}" gs_line nil) (gs_only_circle const-decl "{nvo | nvo /= zero => gs_only?(vnzo)(nvo)}" gs_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/") (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) (comp_gs_fseq application-judgement "(gs_fseq?)" bands_2D nil) (gs2v2_continuous application-judgement "continuous_rv_fun" gs_bands_2D nil) (gs_critical_composition formula-decl nil bands_2D nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (member const-decl "bool" fseqs "structures/") (below type-eq-decl nil naturalnumbers nil) (vi skolem-const-decl "Nz_vect2" bands_2D nil) (vo skolem-const-decl "Nz_vect2" bands_2D nil) (s skolem-const-decl "Vect2" bands_2D nil) (< const-decl "bool" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (gs2v2_id formula-decl nil bands_util nil) (NOT const-decl "[bool -> bool]" booleans nil) (gs_line? const-decl "bool" gs_line nil) (circle_solution_2D_horizontal_sep formula-decl nil horizontal nil) (scal_0 formula-decl nil vectors_2D "vectors/") (add_zero_right formula-decl nil vectors_2D "vectors/") (gs_only_circle? const-decl "bool" gs_only nil) (- const-decl "Vector" vectors_2D "vectors/") (gs_only_circle_solution formula-decl nil gs_only nil) (gs_critical? const-decl "bool" gs_bands_2D nil) (member_gs_critical formula-decl nil bands_2D nil) (norm_zero formula-decl nil vectors_2D "vectors/") (member_composition formula-decl nil fseqs "structures/") (gs_bands const-decl "{fs: (gs_fseq?) | increasing?(fs)}" bands_2D nil) (nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}" real_defs nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (minus_real_is_real application-judgement "real" reals nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (nz_nzv application-judgement "Nz_vector" vectors_2D "vectors/") (nz_norm_gt_0 application-judgement "posreal" vectors_2D "vectors/") (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (norm_scal formula-decl nil vectors_2D "vectors/") (* const-decl "Vector" vectors_2D "vectors/") (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (norm const-decl "nnreal" vectors_2D "vectors/") (^ const-decl "Normalized" vectors_2D "vectors/")) nil) (gs_bands_critical-1 nil 3477392853 (";;; Proof gs_bands_critical-1 for formula bands.gs_bands_critical" (skeep) ((";;; Proof gs_bands_critical-1 for formula bands.gs_bands_critical" (expand "gs_bands") ((";;; Proof gs_bands_critical-1 for formula bands.gs_bands_critical" (rewrite "member_sort" :dir rl) ((";;; Proof gs_bands_critical-1 for formula bands.gs_bands_critical" (rewrite "member_composition") ((";;; Proof gs_bands_critical-1 for formula bands.gs_bands_critical" (ground) (("1" (hide 2) (("1" (rewrite "gs_critical_composition") (("1" (rewrite "gs_critical_composition") (("1" (rewrite "gs_critical_composition") (("1" (rewrite "gs_critical_composition") (("1" (lift-if) (("1" (split) (("1" (flatten) (("1" (rewrite "gs_critical_composition") (("1" (rewrite "gs_critical_composition") (("1" (rewrite "gs_critical_composition") (("1" (flatten) (("1" (case "gs_line_eps(vect2(sp), vect2(vo), vect2(vi), -1) /= zero AND gsp = gs(gs_line_eps(vect2( (("1" (flatten) (("1" (expand "member") (("1" (inst + "0") (("1" (expand "gs_critical") (("1" (assert) (("1" (expand "addend") (("1" (expand "empty_seq") (("1" (propax) nil))))))))) ("2" (expand "gs_critical") (("2" (assert) (("2" (expand "addend") (("2" (expand "empty_seq") (("2" (assert) nil))))))))))))))) ("2" (expand "gs_critical_3D?") (("2" (assert) (("2" (expand "gs_critical?") (("2" (expand "gs_only_circle?") (("2" (expand "gs_line?") (("2" (expand "gs_circle?") (("2" (rewrite "vect2_gs2v3") (("2" (expand "gs2v2") (("2" (split -) (("1" (flatten) (("1" (skosimp*) (("1" (typepred "eps!1") (("1" (split -2) (("1" (replace -1) (("1" (assert) (("1" (expand "^") (("1" (replace -3 :dir rl) (("1" (expand "gs") (("1" (rewrite "norm_scal") (("1" (rewrite "norm_scal") (("1" (expand "abs") (("1" (propax) nil))))))))))))))))) ("2" (assert) (("2" (replace -1) (("2" (replace -3 :dir rl) (("2" (assert) (("2" (expand "^") (("2" (expand "gs") (("2" (rewrite "norm_scal") (("2" (rewrite "norm_scal") (("2" (expand "abs") (("2" (assert) nil))))))))))))))))))))))))))) ("2" (flatten) (("2" (skosimp*) (("2" (typepred "irt!1") (("2" (split -2) (("1" (replace -1) (("1" (replace -3 :dir rl) (("1" (assert) (("1" (expand "^") (("1" (expand "gs") (("1" (rewrite "norm_scal") (("1" (rewrite "norm_scal") (("1" (expand "abs") (("1" (propax) nil))))))))))))))))) ("2" (assert) (("2" (replace -1) (("2" (replace -3 :dir rl) (("2" (assert) (("2" (expand "^") (("2" (expand "gs") (("2" (rewrite "norm_scal") (("2" (rewrite "norm_scal") (("2" (expand "abs") (("2" (propax) nil))))))))))))))))))))))))))) ("3" (assert) (("3" (skosimp*) (("3" (typepred "dir!1") (("3" (typepred "irt!1") (("3" (split -2) (("1" (replace -1) (("1" (split -4) (("1" (replace -1) (("1" (replace -5 :dir rl) (("1" (rewrite "vect2_gs2v3") (("1" (assert) (("1" (expand "gs2v2") (("1" (expand "^") (("1" (expand "gs") (("1" (rewrite "norm_scal") (("1" (rewrite "norm_scal") (("1" (expand "abs") (("1" (propax) nil))))))))))))))))))))) ("2" (assert) (("2" (replace -1) (("2" (replace -5 :dir rl) (("2" (rewrite "vect2_gs2v3") (("2" (expand "gs2v2") (("2" (expand "gs") (("2" (expand "^") (("2" (rewrite "norm_scal") (("2" (rewrite "norm_scal") (("2" (expand "abs") (("2" (propax) nil))))))))))))))))))))))))) ("2" (assert) (("2" (replace -1) (("2" (split -4) (("1" (replace -1) (("1" (replace -5 :dir rl) (("1" (rewrite "vect2_gs2v3") (("1" (expand "gs2v2") (("1" (expand "gs") (("1" (expand "^") (("1" (rewrite "norm_scal") (("1" (rewrite "norm_scal") (("1" (expand "abs") (("1" (propax) nil))))))))))))))))))) ("2" (assert) (("2" (replace -1) (("2" (replace -5 :dir rl) (("2" (rewrite "vect2_gs2v3") (("2" (expand "gs2v2") (("2" (expand "gs") (("2" (expand "^") (("2" (rewrite "norm_scal") (("2" (rewrite "norm_scal") (("2" (expand "abs") (("2" (propax) nil))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ("2" (flatten) (("2" (expand "gs_critical_3D?") (("2" (assert) (("2" (skosimp*) (("2" (expand "gs_circle?") (("2" (flatten) (("2" (skosimp*) (("2" (typepred "gs_circle(sp, vo, vi, dir!1, irt!1)") (("2" (split -1) (("1" (flatten) (("1" (label "hyp" -3) (("1" (typepred "dir!1") (("1" (split -2) (("1" (replace -1) (("1" (typepred "irt!1") (("1" (split -2) (("1" (replace -1) (("1" (replace "hyp" :dir rl) (("1" (assert) (("1" (expand "gs") (("1" (rewrite "vect2_gs2v3") (("1" (expand "gs2v2") (("1" (expand "^") (("1" (rewrite "norm_scal") (("1" (rewrite "norm_scal") (("1" (expand "abs") (("1" (propax) nil))))))))))))))))))))) ("2" (assert) (("2" (replace -1) (("2" (replace "hyp" :dir rl) (("2" (assert) (("2" (rewrite "vect2_gs2v3") (("2" (expand "gs") (("2" (expand "gs2v2") (("2" (expand "^") (("2" (rewrite "norm_scal") (("2" (rewrite "norm_scal") (("2" (expand "abs") (("2" (propax) nil))))))))))))))))))))))))))))) ("2" (assert) (("2" (replace -1) (("2" (typepred "irt!1") (("2" (split -2) (("1" (replace -1) (("1" (replace "hyp" :dir rl) (("1" (assert) (("1" (rewrite "vect2_gs2v3") (("1" (expand "gs") (("1" (expand "gs2v2") (("1" (expand "^") (("1" (rewrite "norm_scal") (("1" (rewrite "norm_scal") (("1" (expand "abs") (("1" (propax) nil))))))))))))))))))))) ("2" (assert) (("2" (replace -1) (("2" (replace "hyp" :dir rl) (("2" (assert) (("2" (rewrite "vect2_gs2v3") (("2" (expand "gs") (("2" (expand "gs2v2") (("2" (expand "^") (("2" (rewrite "norm_scal") (("2" (rewrite "norm_scal") (("2" (expand "abs") (("2" (propax) nil))))))))))))))))))))))))))))))))))))))) ("2" (assert) nil))))))))))))))))))))))))))))))))) ("2" (hide 1) (("2" (rewrite "member_composition") (("2" (flatten) (("2" (expand "member" 1) (("2" (inst + "0") (("1" (expand "addend") (("1" (assert) (("1" (expand "empty_seq") (("1" (propax) nil))))))) ("2" (expand "addend") (("2" (expand "empty_seq") (("2" (assert) nil))))))))))))))) ("3" (hide 1) (("3" (rewrite "member_composition") (("3" (flatten) (("3" (expand "member" 2) (("3" (inst + "0") (("1" (expand "addend") (("1" (assert) (("1" (expand "empty_seq") (("1" (propax) nil))))))) ("2" (expand "addend") (("2" (expand "empty_seq") (("2" (assert) nil))))))))))))))) ("4" (hide 2) (("4" (hide 2) (("4" (lift-if) (("4" (split) (("1" (flatten) (("1" (rewrite "gs_critical_composition") (("1" (rewrite "gs_critical_composition") (("1" (rewrite "gs_critical_composition") (("1" (rewrite "gs_critical_composition") (("1" (rewrite "gs_critical_composition") (("1" (rewrite "gs_critical_composition") (("1" (rewrite "gs_critical_composition") (("1" (expand "gs_critical_3D?") (("1" (assert) (("1" (flatten) (("1" (expand "gs_critical?") (("1" (flatten) (("1" (expand "gs_line?") (("1" (assert) (("1" (expand "gs_only_circle?") (("1" (expand "gs_circle?") (("1" (rewrite "vect2_gs2v3") (("1" (expand "gs2v2") (("1" (expand "^") (("1" (label "gl" 1) (("1" (label "goc" 2) (("1" (label "gc" 3) (("1" (case "gsp * ((1 / norm(vect2(vo))) * vect2(vo)) /= zero") (("1" (assert) (("1" (split -) (("1" (flatten) (("1" (inst "gc" 1) (("1" (replace -1) (("1" (expand "gs2v3") (("1" (rewrite "gs2v2_id") (("1" (typepred "gs_circle(sp,vo,vi,1,1)") (("1" (assert) (("1" (flatten) (("1" (inst "gc" 1) (("1" (replace -2) (("1" (assert) nil))))))))))) ("2" (typepred "gs_circle(sp,vo,vi,1,1)") (("2" (assert) nil))))))))))))) ("2" (inst "gc" "1") (("2" (assert) (("2" (flatten) (("2" (inst "gc" "-1") (("2" (typepred "gs_circle(sp,vo,vi,1,-1)") (("2" (assert) (("2" (flatten) (("2" (expand "gs2v3") (("2" (replace -3) (("2" (rewrite "gs2v2_id") (("2" (replace -2) (("2" (assert) nil))))))))))))))))))))))) ("3" (flatten) (("3" (assert) (("3" (inst "gc" "-1") (("3" (inst "gc" "1") (("3" (replace -1) (("3" (expand "gs2v3") (("3" (typepred "gs_circle(sp,vo,vi,-1,1)") (("3" (assert) (("3" (flatten) (("3" (rewrite "gs2v2_id") (("3" (replace -2) (("3" (assert) nil))))))))))))))))))))))) ("4" (flatten) (("4" (assert) (("4" (inst "gc" "-1") (("4" (inst "gc" "-1") (("4" (replace -1) (("4" (expand "gs2v3") (("4" (typepred "gs_circle(sp,vo,vi,-1,-1)") (("4" (assert) (("4" (flatten) (("4" (rewrite "gs2v2_id") (("4" (replace -2) (("4" (assert) nil))))))))))))))))))))))) ("5" (flatten) (("5" (assert) (("5" (inst "goc" "1") (("5" (typepred "gs_only_circle(vect2(sp), vect2(vo), vect2(vi), T, -1, 1)") (("5" (assert) (("5" (lemma "gs2v2_id") (("5" (inst?) (("5" (assert) (("5" (replace -3 :dir rl) (("5" (expand "gs2v2") (("5" (expand "^") (("5" (assert) nil))))))))))))))))))))))) ("6" (flatten) (("6" (assert) (("6" (inst "goc" "-1") (("6" (typepred "gs_only_circle(vect2(sp), vect2(vo), vect2(vi), T, -1, -1)") (("6" (assert) (("6" (lemma "gs2v2_id") (("6" (inst?) (("6" (assert) (("6" (replace -3 :dir rl) (("6" (expand "gs2v2") (("6" (expand "^") (("6" (assert) nil))))))))))))))))))))))) ("7" (flatten) (("7" (assert) (("7" (inst "gl" "1") (("7" (typepred "gs_line_eps(vect2(sp), vect2(vo), vect2(vi), 1)") (("7" (assert) (("7" (lemma "gs2v2_id") (("7" (inst?) (("7" (assert) (("7" (replace -3 :dir rl) (("7" (expand "gs2v2") (("7" (expand "^") (("7" (assert) nil))))))))))))))))))))))) ("8" (lemma "gs_critical_rew") (("8" (inst?) (("8" (replace -1) (("8" (hide -1) (("8" (lift-if) (("8" (ground) (("1" (rewrite "member_singleton") (("1" (typepred "gs_line_eps(vect2(sp), vect2(vo), vect2(vi), -1)") (("1" (assert) (("1" (lemma "gs2v2_id") (("1" (inst?) (("1" (assert) (("1" (expand "gs2v2") (("1" (expand "^") (("1" (inst "gl" "-1") (("1" (assert) nil))))))))))))))))))) ("2" (expand "member") (("2" (skosimp*) (("2" (typepred "i!1") (("2" (expand "empty_seq") (("2" (assert) nil))))))))) ("3" (expand "member") (("3" (skosimp*) (("3" (typepred "i!1") (("3" (expand "empty_seq") (("3" (assert) nil))))))))) ("4" (expand "member") (("4" (skosimp*) (("4" (typepred "i!1") (("4" (expand "empty_seq") (("4" (assert) nil))))))))))))))))))))))))) ("2" (hide-all-but 1) (("2" (typepred "vo") (("2" (typepred "gsp") (("2" (typepred "gsmin") (("2" (assert) (("2" (lemma "vectors_2D.scal_eq_zero") (("2" (inst?) (("2" (assert) nil))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ("2" (flatten) (("2" (expand "gs_critical_3D?") (("2" (assert) (("2" (expand "gs_circle?") (("2" (rewrite "vect2_gs2v3") (("2" (expand "gs2v2") (("2" (expand "^") (("2" (case "gsp * ((1 / norm(vect2(vo))) * vect2(vo)) /= zero") (("1" (flatten) (("1" (rewrite "gs_critical_composition") (("1" (rewrite "gs_critical_composition") (("1" (rewrite "gs_critical_composition") (("1" (rewrite "gs_critical_composition") (("1" (split -1) (("1" (flatten) (("1" (inst 4 "1") (("1" (assert) (("1" (inst 4 "1") (("1" (replace -1) (("1" (expand "gs2v3") (("1" (rewrite "gs2v2_id") (("1" (typepred "gs_circle(sp,vo,vi,1,1)") (("1" (assert) (("1" (flatten) (("1" (replace -2) (("1" (assert) nil))))))))) ("2" (typepred "gs_circle(sp,vo,vi,1,1)") (("2" (assert) nil))))))))))))))))) ("2" (flatten) (("2" (inst 4 "1") (("2" (assert) (("2" (inst 4 "-1") (("2" (replace -1) (("2" (typepred "gs_circle(sp,vo,vi,1,-1)") (("2" (assert) (("2" (flatten) (("2" (expand "gs2v3") (("2" (rewrite "gs2v2_id") (("2" (replace -2) (("2" (assert) nil))))))))))))))))))))))) ("3" (flatten) (("3" (inst 4 "-1") (("3" (assert) (("3" (inst 4 "1") (("3" (replace -1) (("3" (typepred "gs_circle(sp,vo,vi,-1,1)") (("3" (assert) (("3" (flatten) (("3" (expand "gs2v3") (("3" (rewrite "gs2v2_id") (("3" (replace -2) (("3" (assert) nil))))))))))))))))))))))) ("4" (flatten) (("4" (inst 4 "-1") (("4" (assert) (("4" (inst 4 "-1") (("4" (replace -1) (("4" (expand "gs2v3") (("4" (typepred "gs_circle(sp,vo,vi,-1,-1)") (("4" (assert) (("4" (flatten) (("4" (rewrite "gs2v2_id") (("4" (replace -2) (("4" (assert) nil))))))))))))))))))))))) ("5" (expand "member") (("5" (skosimp*) (("5" (typepred "i!1") (("5" (expand "empty_seq") (("5" (assert) nil))))))))))))))))))))) ("2" (hide-all-but 1) (("2" (lemma "vectors_2D.scal_eq_zero") (("2" (assert) (("2" (inst?) (("2" (assert) nil))))))))))))))))))))))))))))))))) ("5" (hide 1) (("5" (rewrite "member_composition") (("5" (expand "member") (("5" (expand "addend") (("5" (expand "empty_seq") (("5" (split -1) (("1" (skosimp*) (("1" (typepred "i!1") (("1" (expand "addend") (("1" (expand "empty_seq") (("1" (assert) nil))))))))) ("2" (skosimp*) (("2" (typepred "i!1") (("2" (expand "addend") (("2" (expand "empty_seq") (("2" (assert) nil)))))))))))))))))))))))))))))) ";;; developed with shostak decision procedures") nil nil)) (red_trk_band?_TCC1 0 (red_trk_band?_TCC1-1 nil 3477392567 ("" (skeep) (("" (assert) nil nil)) nil) ((real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (red_trk_band?_TCC2 0 (red_trk_band?_TCC2-1 nil 3477392567 ("" (skeep) (("" (assert) nil nil)) nil) ((int_plus_int_is_int application-judgement "int" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (trk_red_bands 0 (trk_red_bands-1 nil 3477392877 ("" (skeep) (("" (assert) (("" (skeep) (("" (ground) (("1" (expand "red_trk_band?") (("1" (name "bband" "{ y: real | trk_bands(s,vo,vi)`seq(i) < y AND y < trk_bands(s,vo,vi)`seq(1 + i)}") (("1" (lemma "trk_red_band") (("1" (skosimp*) (("1" (inst - "bband" "s" "vi" "vo" "(trk_bands(s,vo,vi)`seq(1 + i) + trk_bands(s,vo,vi)`seq(i)) / 2") (("1" (assert) (("1" (split -1) (("1" (expand "trk_red?") (("1" (inst - "x!1") (("1" (replace -1 :dir rl) (("1" (typepred "x!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "trk_band?") (("2" (skosimp*) (("2" (typepred "trko!1") (("2" (replace -3 :dir rl) (("2" (assert) (("2" (flatten) (("2" (lemma "trk_bands_critical") (("2" (inst - "s" "trko!1" "vi" "vo") (("1" (assert) (("1" (expand "member") (("1" (skosimp*) (("1" (typepred "trk_bands(s,vo,vi)") (("1" (expand "increasing?") (("1" (case "i!1 < i") (("1" (inst - "i!1" "i") (("1" (assert) nil nil)) nil) ("2" (case "i!1 > 1+i") (("1" (inst - "1+i" "i!1") (("1" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "trk_bands(s,vo,vi)") (("2" (expand "trk_fseq?") (("2" (inst-cp -1 "i") (("2" (inst -1 "1+i") (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1 :dir rl) (("2" (assert) nil nil)) nil) ("3" (split) (("1" (skosimp*) (("1" (typepred "a!1") (("1" (typepred "b!1") (("1" (replace -5 :dir rl) (("1" (assert) (("1" (flatten) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (typepred "trk_bands(s,vo,vi)") (("2" (expand "trk_fseq?") (("2" (inst-cp -1 "i") (("2" (inst -1 "1+i") (("2" (flatten) (("2" (typepred "z!1") (("2" (replace -7 :dir rl) (("2" (assert) (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "red_trk_band?") (("2" (inst - "(trk_bands(s,vo,vi)`seq(1 + i) + trk_bands(s,vo,vi)`seq(i)) / 2") (("1" (rewrite "cd2d[D,B,T]") nil nil) ("2" (typepred "trk_bands(s,vo,vi)") (("2" (expand "increasing?") (("2" (inst - "i" "1+i") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (NOT const-decl "[bool -> bool]" booleans nil) (subrange type-eq-decl nil integers nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields 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) (trk_bands const-decl "{fs: (trk_fseq?) | increasing?(fs)}" bands_2D 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 "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) (fseq type-eq-decl nil fseqs "structures/") (barray type-eq-decl nil fseqs "structures/") (nat nonempty-type-eq-decl nil naturalnumbers 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/") (< const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities 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) (int_plus_int_is_int application-judgement "int" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (Vtrk_continuous application-judgement "continuous_rv_fun" trk_bands_2D nil) (trk_band? const-decl "bool" trk_bands_2D nil) (trk_bands_critical formula-decl nil bands_2D nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (below type-eq-decl nil naturalnumbers nil) (member const-decl "bool" fseqs "structures/") (trko!1 skolem-const-decl "(bband)" bands_2D nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (trk_red? const-decl "bool" trk_bands_2D nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (x!1 skolem-const-decl "{x | trk_bands(s, vo, vi)`seq(i) < x AND x < trk_bands(s, vo, vi)`seq(1 + i)}" bands_2D nil) (set type-eq-decl nil sets nil) (Connected type-eq-decl nil connected_set "reals/") (ConnectedGeLt type-eq-decl nil connected_set "reals/") (i skolem-const-decl "{ii: subrange(0, trk_bands(s, vo, vi)`length - 2) | NOT trk_bands(s, vo, vi)`seq(ii) = trk_bands(s, vo, vi)`seq(1 + ii)}" bands_2D nil) (vi skolem-const-decl "Nz_vect2" bands_2D nil) (vo skolem-const-decl "Nz_vect2" bands_2D nil) (s skolem-const-decl "Vect2" bands_2D nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (pi const-decl "posreal" atan "trig_fnd/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (bband skolem-const-decl "[real -> boolean]" bands_2D nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}" atan_approx "trig_fnd/") (T formal-const-decl "{AB: posreal | AB > B}" bands_2D nil) (B formal-const-decl "nnreal" bands_2D nil) (nnreal type-eq-decl nil real_types nil) (D formal-const-decl "posreal" bands_2D nil) (trk_red_band formula-decl nil trk_bands_2D nil) (red_trk_band? const-decl "bool" bands_2D nil) (real_plus_real_is_real application-judgement "real" reals nil) (cd2d formula-decl nil cd2d nil) (Vtrk const-decl "Vect2" bands_util nil)) nil)) (trk_green_bands 0 (trk_green_bands-1 nil 3477392890 ("" (skeep) (("" (assert) (("" (skeep) (("" (name "bband" "{ y: real | trk_bands(s,vo,vi)`seq(i) < y AND y < trk_bands(s,vo,vi)`seq(1 + i)}") (("" (case "trk_band?(s,vo,vi)(bband)") (("1" (label "bbn" -2) (("1" (ground) (("1" (skosimp*) (("1" (typepred "x!1") (("1" (expand "red_trk_band?") (("1" (lemma "trk_red_band") (("1" (inst-cp - "bband" "s" "vi" "vo" "(trk_bands(s,vo,vi)`seq(1 + i) + trk_bands(s,vo,vi)`seq(i)) / 2") (("1" (inst - "bband" "s" "vi" "vo" "x!1") (("1" (assert) (("1" (lemma "cd2d[D,B,T]") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (replace "bbn" :dir rl) (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (replace "bbn" :dir rl) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "red_trk_band?") (("2" (inst - "(trk_bands(s,vo,vi)`seq(1 + i) + trk_bands(s,vo,vi)`seq(i)) / 2") (("1" (rewrite "cd2d[D,B,T]") nil nil) ("2" (typepred "trk_bands(s,vo,vi)") (("2" (expand "increasing?") (("2" (inst - "i" "1+i") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (replace -1 :dir rl) (("2" (expand "trk_band?") (("2" (skosimp*) (("2" (typepred "trko!1") (("2" (lemma "trk_bands_critical") (("2" (inst - "s" "trko!1" "vi" "vo") (("1" (assert) (("1" (expand "member") (("1" (skosimp*) (("1" (typepred "trk_bands(s,vo,vi)") (("1" (expand "increasing?") (("1" (case "i!1 < i") (("1" (inst - "i!1" "i") (("1" (assert) nil nil)) nil) ("2" (case "i!1 > 1+i") (("1" (inst - "1+i" "i!1") (("1" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "trk_bands(s,vo,vi)") (("2" (expand "trk_fseq?") (("2" (inst-cp -1 "i") (("2" (inst -1 "1+i") (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (split) (("1" (skosimp*) (("1" (typepred "a!1") (("1" (typepred "b!1") (("1" (replace -5 :dir rl) (("1" (assert) (("1" (flatten) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (typepred "trk_bands(s,vo,vi)") (("2" (expand "trk_fseq?") (("2" (inst-cp -1 "i") (("2" (inst -1 "1+i") (("2" (flatten) (("2" (typepred "z!1") (("2" (replace -7 :dir rl) (("2" (assert) (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (NOT const-decl "[bool -> bool]" booleans nil) (subrange type-eq-decl nil integers nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields 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) (trk_bands const-decl "{fs: (trk_fseq?) | increasing?(fs)}" bands_2D 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 "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) (fseq type-eq-decl nil fseqs "structures/") (barray type-eq-decl nil fseqs "structures/") (nat nonempty-type-eq-decl nil naturalnumbers 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/") (< const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities 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) (int_plus_int_is_int application-judgement "int" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans 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) (trko!1 skolem-const-decl "({y: real | trk_bands(s, vo, vi)`seq(i) < y AND y < trk_bands(s, vo, vi)`seq(1 + i)})" bands_2D nil) (member const-decl "bool" fseqs "structures/") (below type-eq-decl nil naturalnumbers 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) (real_div_nzreal_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (red_trk_band? const-decl "bool" bands_2D nil) (bband skolem-const-decl "[real -> boolean]" bands_2D nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (s skolem-const-decl "Vect2" bands_2D nil) (vo skolem-const-decl "Nz_vect2" bands_2D nil) (vi skolem-const-decl "Nz_vect2" bands_2D nil) (i skolem-const-decl "{ii: subrange(0, trk_bands(s, vo, vi)`length - 2) | NOT trk_bands(s, vo, vi)`seq(ii) = trk_bands(s, vo, vi)`seq(1 + ii)}" bands_2D nil) (Vtrk_continuous application-judgement "continuous_rv_fun" trk_bands_2D nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (Vtrk const-decl "Vect2" bands_util nil) (cd2d formula-decl nil cd2d nil) (x!1 skolem-const-decl "{x | trk_bands(s, vo, vi)`seq(i) < x AND x < trk_bands(s, vo, vi)`seq(1 + i)}" bands_2D nil) (trk_red_band formula-decl nil trk_bands_2D nil) (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}" atan_approx "trig_fnd/") (trk_band? const-decl "bool" trk_bands_2D nil) (T formal-const-decl "{AB: posreal | AB > B}" bands_2D nil) (B formal-const-decl "nnreal" bands_2D nil) (nnreal type-eq-decl nil real_types nil) (D formal-const-decl "posreal" bands_2D nil) (ConnectedGeLt type-eq-decl nil connected_set "reals/") (pi const-decl "posreal" atan "trig_fnd/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (Connected type-eq-decl nil connected_set "reals/") (set type-eq-decl nil sets nil)) nil)) (red_gs_band?_TCC1 0 (red_gs_band?_TCC1-1 nil 3477392567 ("" (skeep) (("" (assert) nil nil)) nil) ((real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (red_gs_band?_TCC2 0 (red_gs_band?_TCC2-1 nil 3477392567 ("" (skeep) (("" (assert) nil nil)) nil) ((int_plus_int_is_int application-judgement "int" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (gs_red_bands 0 (gs_red_bands-1 nil 3477392906 ("" (skeep) (("" (assert) (("" (skeep) (("" (ground) (("1" (expand "red_gs_band?") (("1" (name "bband" "{ y: real | gs_bands(s,vo,vi)`seq(i) < y AND y < gs_bands(s,vo,vi)`seq(1 + i)}") (("1" (lemma "gs_red_band") (("1" (skosimp*) (("1" (inst - "bband" "s" "vi" "vo" "(gs_bands(s,vo,vi)`seq(1 + i) + gs_bands(s,vo,vi)`seq(i)) / 2") (("1" (assert) (("1" (split -1) (("1" (expand "gs_red?") (("1" (inst - "x!1") (("1" (replace -1 :dir rl) (("1" (typepred "x!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "gs_band?") (("2" (skosimp*) (("2" (typepred "gso!1") (("2" (replace -3 :dir rl) (("2" (assert) (("2" (flatten) (("2" (lemma "gs_bands_critical") (("2" (inst - "gso!1" "s" "vi" "vo") (("1" (assert) (("1" (expand "member") (("1" (skosimp*) (("1" (typepred "gs_bands(s,vo,vi)") (("1" (expand "increasing?") (("1" (case "i!1 < i") (("1" (inst - "i!1" "i") (("1" (assert) nil nil)) nil) ("2" (case "i!1 > 1+i") (("1" (inst - "1+i" "i!1") (("1" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "gs_bands(s,vo,vi)") (("2" (expand "gs_fseq?") (("2" (inst-cp -1 "i") (("2" (assert) (("2" (flatten) (("2" (assert) (("2" (inst - "1+i") (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1 :dir rl) (("2" (assert) nil nil)) nil) ("3" (split) (("1" (skosimp*) (("1" (typepred "a!1") (("1" (typepred "b!1") (("1" (replace -5 :dir rl) (("1" (assert) (("1" (flatten) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (typepred "gs_bands(s,vo,vi)") (("2" (expand "gs_fseq?") (("2" (inst-cp -1 "i") (("2" (inst -1 "1+i") (("2" (typepred "z!1") (("2" (replace -5 :dir rl) (("2" (assert) (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "red_gs_band?") (("2" (inst - "(gs_bands(s,vo,vi)`seq(1 + i) + gs_bands(s,vo,vi)`seq(i)) / 2") (("1" (rewrite "cd2d[D,B,T]") nil nil) ("2" (typepred "gs_bands(s,vo,vi)") (("2" (expand "increasing?") (("2" (inst - "i" "1+i") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (NOT const-decl "[bool -> bool]" booleans nil) (subrange type-eq-decl nil integers nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields 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) (gs_bands const-decl "{fs: (gs_fseq?) | increasing?(fs)}" bands_2D nil) (increasing? const-decl "bool" sort_fseq "structures/") (<= const-decl "bool" reals nil) (gs_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) (>= const-decl "bool" reals nil) (fseq type-eq-decl nil fseqs "structures/") (barray type-eq-decl nil fseqs "structures/") (nat nonempty-type-eq-decl nil naturalnumbers 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/") (< const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities 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) (int_plus_int_is_int application-judgement "int" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (Vgs_continuous application-judgement "continuous_rv_fun" bands_2D nil) (gs_band? const-decl "bool" gs_bands_2D nil) (gs_bands_critical formula-decl nil bands_2D nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (below type-eq-decl nil naturalnumbers nil) (member const-decl "bool" fseqs "structures/") (gso!1 skolem-const-decl "(bband)" bands_2D nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (gs_red? const-decl "bool" gs_bands_2D nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (x!1 skolem-const-decl "{x | gs_bands(s, vo, vi)`seq(i) < x AND x < gs_bands(s, vo, vi)`seq(1 + i)}" bands_2D nil) (set type-eq-decl nil sets nil) (Connected type-eq-decl nil connected_set "reals/") (ConnectedGt type-eq-decl nil connected_set "reals/") (i skolem-const-decl "{ii: subrange(0, gs_bands(s, vo, vi)`length - 2) | NOT gs_bands(s, vo, vi)`seq(ii) = gs_bands(s, vo, vi)`seq(1 + ii)}" bands_2D nil) (vi skolem-const-decl "Nz_vect2" bands_2D nil) (vo skolem-const-decl "Nz_vect2" bands_2D nil) (s skolem-const-decl "Vect2" bands_2D nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (bband skolem-const-decl "[real -> boolean]" bands_2D nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (T formal-const-decl "{AB: posreal | AB > B}" bands_2D nil) (B formal-const-decl "nnreal" bands_2D nil) (nnreal type-eq-decl nil real_types nil) (D formal-const-decl "posreal" bands_2D nil) (gs_red_band formula-decl nil gs_bands_2D nil) (red_gs_band? const-decl "bool" bands_2D nil) (real_plus_real_is_real application-judgement "real" reals nil) (cd2d formula-decl nil cd2d nil) (Vgs const-decl "Vect2" gs_bands_2D nil)) nil)) (gs_green_bands 0 (gs_green_bands-1 nil 3477392919 ("" (skeep) (("" (assert) (("" (skeep) (("" (name "bband" "{ y: real | gs_bands(s,vo,vi)`seq(i) < y AND y < gs_bands(s,vo,vi)`seq(1 + i)}") (("" (case "gs_band?(s,vo,vi)(bband)") (("1" (label "bbn" -2) (("1" (ground) (("1" (skosimp*) (("1" (typepred "x!1") (("1" (expand "red_gs_band?") (("1" (lemma "gs_red_band") (("1" (inst-cp - "bband" "s" "vi" "vo" "(gs_bands(s,vo,vi)`seq(1 + i) + gs_bands(s,vo,vi)`seq(i)) / 2") (("1" (inst - "bband" "s" "vi" "vo" "x!1") (("1" (assert) (("1" (lemma "cd2d[D,B,T]") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (replace "bbn" :dir rl) (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (replace "bbn" :dir rl) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "red_gs_band?") (("2" (inst - "(gs_bands(s,vo,vi)`seq(1 + i) + gs_bands(s,vo,vi)`seq(i)) / 2") (("1" (rewrite "cd2d[D,B,T]") nil nil) ("2" (typepred "gs_bands(s,vo,vi)") (("2" (expand "increasing?") (("2" (inst - "i" "1+i") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (replace -1 :dir rl) (("2" (expand "gs_band?") (("2" (skosimp*) (("2" (typepred "gso!1") (("2" (lemma "gs_bands_critical") (("2" (inst - "gso!1" "s" "vi" "vo") (("1" (assert) (("1" (expand "member") (("1" (skosimp*) (("1" (typepred "gs_bands(s,vo,vi)") (("1" (expand "increasing?") (("1" (case "i!1 < i") (("1" (inst - "i!1" "i") (("1" (assert) nil nil)) nil) ("2" (case "i!1 > 1+i") (("1" (inst - "1+i" "i!1") (("1" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "gs_bands(s,vo,vi)") (("2" (expand "gs_fseq?") (("2" (inst-cp -1 "i") (("2" (assert) (("2" (inst - "1+i") (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (split) (("1" (skosimp*) (("1" (typepred "a!1") (("1" (typepred "b!1") (("1" (replace -5 :dir rl) (("1" (assert) (("1" (flatten) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (typepred "gs_bands(s,vo,vi)") (("2" (expand "gs_fseq?") (("2" (inst-cp -1 "i") (("2" (typepred "z!1") (("2" (assert) (("2" (replace -5 :dir rl) (("2" (assert) (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (NOT const-decl "[bool -> bool]" booleans nil) (subrange type-eq-decl nil integers nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields 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) (gs_bands const-decl "{fs: (gs_fseq?) | increasing?(fs)}" bands_2D nil) (increasing? const-decl "bool" sort_fseq "structures/") (<= const-decl "bool" reals nil) (gs_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) (>= const-decl "bool" reals nil) (fseq type-eq-decl nil fseqs "structures/") (barray type-eq-decl nil fseqs "structures/") (nat nonempty-type-eq-decl nil naturalnumbers 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/") (< const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities 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) (int_plus_int_is_int application-judgement "int" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (gso!1 skolem-const-decl "({y: real | gs_bands(s, vo, vi)`seq(i) < y AND y < gs_bands(s, vo, vi)`seq(1 + i)})" bands_2D nil) (member const-decl "bool" fseqs "structures/") (below type-eq-decl nil naturalnumbers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (gs_bands_critical formula-decl nil bands_2D nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (red_gs_band? const-decl "bool" bands_2D nil) (bband skolem-const-decl "[real -> boolean]" bands_2D nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (s skolem-const-decl "Vect2" bands_2D nil) (vo skolem-const-decl "Nz_vect2" bands_2D nil) (vi skolem-const-decl "Nz_vect2" bands_2D nil) (i skolem-const-decl "{ii: subrange(0, gs_bands(s, vo, vi)`length - 2) | NOT gs_bands(s, vo, vi)`seq(ii) = gs_bands(s, vo, vi)`seq(1 + ii)}" bands_2D nil) (Vgs_continuous application-judgement "continuous_rv_fun" bands_2D nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (Vgs const-decl "Vect2" gs_bands_2D nil) (cd2d formula-decl nil cd2d nil) (x!1 skolem-const-decl "{x | gs_bands(s, vo, vi)`seq(i) < x AND x < gs_bands(s, vo, vi)`seq(1 + i)}" bands_2D nil) (gs_red_band formula-decl nil gs_bands_2D nil) (gs_band? const-decl "bool" gs_bands_2D nil) (T formal-const-decl "{AB: posreal | AB > B}" bands_2D nil) (B formal-const-decl "nnreal" bands_2D nil) (nnreal type-eq-decl nil real_types nil) (D formal-const-decl "posreal" bands_2D nil) (ConnectedGt type-eq-decl nil connected_set "reals/") (Connected type-eq-decl nil connected_set "reals/") (set type-eq-decl nil sets nil)) nil)))
¤ Dauer der Verarbeitung: 0.482 Sekunden (vorverarbeitet am 2026-05-02) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-05-26