|
(event_sequences
(increasing_ind 0
(increasing_ind-1 nil 3381416761
("" (induct "j")
(("1" (assert)
(("1" (skosimp*)
(("1" (typepred "es!1")
(("1" (expand "increasing?") (("1" (inst?) nil nil)) nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2" (inst?)
(("2" (typepred "es!1")
(("2" (expand "increasing?")
(("2" (inst - "i!1 + 1 + j!1") (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
((real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(nat_induction formula-decl nil naturalnumbers nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(< const-decl "bool" reals nil)
(event_sequence type-eq-decl nil event_sequences nil)
(unbounded? const-decl "bool" event_sequences nil)
(increasing? const-decl "bool" event_sequences nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(pred type-eq-decl nil defined_types nil)
(nat nonempty-type-eq-decl nil naturalnumbers 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)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil))
shostak))
(nondecreasing 0
(nondecreasing-1 nil 3399998653
("" (skosimp*)
(("" (lemma "increasing_ind")
(("" (inst - _ "i!1" "j!1 - i!1 - 1")
(("1" (inst?) (("1" (assert) nil nil)) nil)
("2" (assert) nil nil))
nil))
nil))
nil)
((increasing_ind formula-decl nil event_sequences nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(event_sequence type-eq-decl nil event_sequences nil)
(unbounded? const-decl "bool" event_sequences nil)
(increasing? const-decl "bool" event_sequences nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(i!1 skolem-const-decl "nat" event_sequences nil)
(j!1 skolem-const-decl "nat" event_sequences nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil))
shostak))
(future_events_nonempty 0
(future_events_nonempty-2 nil 3399291236
("" (skosimp*)
(("" (auto-rewrite-defs)
(("" (typepred "es!1")
(("" (assert)
(("" (inst -2 "t!1")
(("" (skosimp*)
(("" (inst -3 "k!1")
(("" (inst?) (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((future_events const-decl "boolean" event_sequences nil)
(member const-decl "bool" sets nil)
(empty? const-decl "bool" sets nil)
(nonempty? const-decl "bool" sets nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers 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)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(increasing? const-decl "bool" event_sequences nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(unbounded? const-decl "bool" event_sequences nil)
(event_sequence type-eq-decl nil event_sequences nil))
nil)
(future_events_nonempty-1 nil 3399291132 ("" (judgement-tcc) nil nil)
nil nil))
(index_le 0
(index_le-1 nil 3381390698
("" (skosimp*)
(("" (expand "index_of")
(("" (invoke (name-replace "m" "%1") (! 1 l 1))
(("" (case-replace "m = 0")
(("" (typepred "m")
(("" (inst - "m - 1")
(("1" (expand "future_events") (("1" (assert) nil nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
((index_of const-decl "nat" event_sequences nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(es!1 skolem-const-decl "event_sequence" event_sequences nil)
(t!1 skolem-const-decl "real" event_sequences nil)
(m skolem-const-decl "{a |
future_events(es!1)(t!1)(a) AND
(FORALL (x: nat): future_events(es!1)(t!1)(x) IMPLIES a <= x)}"
event_sequences nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(future_events_nonempty application-judgement "(nonempty?[nat])"
event_sequences nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(set type-eq-decl nil sets nil)
(nonempty? const-decl "bool" sets nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(min const-decl "{a | S(a) AND (FORALL x: S(x) IMPLIES a <= x)}"
min_nat nil)
(increasing? const-decl "bool" event_sequences nil)
(unbounded? const-decl "bool" event_sequences nil)
(event_sequence type-eq-decl nil event_sequences nil)
(future_events const-decl "boolean" event_sequences nil))
shostak))
(lt_index 0
(lt_index-2 "" 3399290589
("" (skosimp*)
(("" (expand* "index_of" "future_events") (("" (assert) nil nil))
nil))
nil)
((future_events const-decl "boolean" event_sequences nil)
(index_of const-decl "nat" event_sequences nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil))
shostak)
(lt_index-1 nil 3399290293
("" (skosimp*)
(("" (invoke (name "K" "%1") (! 1 r 1 1))
(("" (replace*)
(("" (use "index_of_char") (("" (assert) nil nil)) nil)) nil))
nil))
nil)
nil nil))
(index_le_alt 0
(index_le_alt-1 nil 3399307062
("" (skosimp*)
(("" (expand "index_of")
(("" (invoke (name-replace "m" "%1") (! 1 l 1))
(("" (typepred "m")
(("" (inst - "m - 1")
(("1" (expand "future_events") (("1" (assert) nil nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
((index_of const-decl "nat" event_sequences nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(m skolem-const-decl "{a |
future_events(es!1)(t!1)(a) AND
(FORALL (x: nat): future_events(es!1)(t!1)(x) IMPLIES a <= x)}"
event_sequences nil)
(t!1 skolem-const-decl "real" event_sequences nil)
(es!1 skolem-const-decl "event_sequence" event_sequences nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(future_events_nonempty application-judgement "(nonempty?[nat])"
event_sequences nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(set type-eq-decl nil sets nil)
(nonempty? const-decl "bool" sets nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(min const-decl "{a | S(a) AND (FORALL x: S(x) IMPLIES a <= x)}"
min_nat nil)
(increasing? const-decl "bool" event_sequences nil)
(unbounded? const-decl "bool" event_sequences nil)
(event_sequence type-eq-decl nil event_sequences nil)
(future_events const-decl "boolean" event_sequences nil))
nil))
(index_rewrite 0
(index_rewrite-1 nil 3399377491
("" (skosimp*)
(("" (expand "index_of")
(("" (rewrite "min_def")
(("" (expand "minimum?")
(("" (prop)
(("1" (expand "future_events")
(("1" (typepred "es!1")
(("1" (expand "increasing?") (("1" (inst?) nil nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2" (expand "future_events")
(("2" (lemma "nondecreasing")
(("2" (inst - "es!1" "x!1 + 1" "i!1")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((index_of const-decl "nat" event_sequences nil)
(minimum? const-decl "bool" min_nat nil)
(nondecreasing formula-decl nil event_sequences nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(nat nonempty-type-eq-decl nil naturalnumbers 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)
(future_events const-decl "boolean" event_sequences nil)
(event_sequence type-eq-decl nil event_sequences nil)
(unbounded? const-decl "bool" event_sequences nil)
(increasing? const-decl "bool" event_sequences nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(nonempty? const-decl "bool" sets nil)
(set type-eq-decl nil sets nil)
(min_def formula-decl nil min_nat nil)
(future_events_nonempty application-judgement "(nonempty?[nat])"
event_sequences nil))
shostak))
(index_conversion_left 0
(index_conversion_left-1 nil 3399998729
("" (skosimp*)
(("" (use "index_le_alt")
(("" (assert)
(("" (lemma "nondecreasing")
(("" (inst - "es!1" "1 + k!1" "index_of(es!1)(t!1)")
(("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
((index_le_alt formula-decl nil event_sequences nil)
(event_sequence type-eq-decl nil event_sequences nil)
(unbounded? const-decl "bool" event_sequences nil)
(increasing? const-decl "bool" event_sequences nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(nat nonempty-type-eq-decl nil naturalnumbers 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)
(nondecreasing formula-decl nil event_sequences nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(index_of const-decl "nat" event_sequences nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers 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))
shostak))
(index_conversion_right 0
(index_conversion_right-1 nil 3399998767
("" (skosimp*)
(("" (use "lt_index")
(("" (lemma "nondecreasing")
(("" (inst - "es!1" "index_of(es!1)(t!1) + 1" "k!1")
(("" (assert) nil nil)) nil))
nil))
nil))
nil)
((lt_index formula-decl nil event_sequences nil)
(event_sequence type-eq-decl nil event_sequences nil)
(unbounded? const-decl "bool" event_sequences nil)
(increasing? const-decl "bool" event_sequences nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(nat nonempty-type-eq-decl nil naturalnumbers 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)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(odd_minus_odd_is_even application-judgement "even_int" integers
nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(index_of const-decl "nat" event_sequences nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nondecreasing formula-decl nil event_sequences nil))
shostak))
(index_ordered 0
(index_ordered-2 "" 3399305759
("" (skosimp*)
(("" (rewrite "index_conversion_right")
(("" (inst?)
(("" (lemma "index_le_alt")
(("" (inst - "es2!1" _)
(("" (inst?) (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil)
((index_conversion_right formula-decl nil event_sequences nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(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)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(increasing? const-decl "bool" event_sequences nil)
(unbounded? const-decl "bool" event_sequences nil)
(event_sequence type-eq-decl nil event_sequences nil)
(index_of const-decl "nat" event_sequences nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(index_le_alt formula-decl nil event_sequences nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
shostak)
(index_ordered-1 nil 3398707979
("" (skosimp*)
(("" (invoke (name "K1" "%1") (! 1 r))
(("" (invoke (name "K2" "%1") (! 1 l))
(("" (replace*)
(("" (rewrite "index_of_char")
(("" (rewrite "index_of_char")
(("" (assert)
(("" (flatten)
(("" (case "t!1 < es1!1(1 + K1)")
(("1" (hide -4)
(("1" (inst - "K1 + 1")
(("1" (case "K2 = K1 + 1")
(("1" (assert) nil nil)
("2" (lemma "increasing_ind")
(("2"
(inst - "es2!1" "K1 + 1" "K2 - K1 - 2")
(("1" (assert) nil nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
nil shostak))
(cross_nondecreasing 0
(cross_nondecreasing-1 nil 3400000731
("" (skosimp*)
(("" (expand "nonoverlap?")
(("" (inst?)
(("" (lemma "nondecreasing")
(("" (inst - "es2!1" "j!1 + 1" "k!1") (("" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
((nonoverlap? const-decl "bool" event_sequences nil)
(nondecreasing formula-decl nil event_sequences nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(event_sequence type-eq-decl nil event_sequences nil)
(unbounded? const-decl "bool" event_sequences nil)
(increasing? const-decl "bool" event_sequences nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(nat nonempty-type-eq-decl nil naturalnumbers 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)
(int_minus_int_is_int application-judgement "int" integers nil))
nil))
(nonoverlap_index_bound 0
(nonoverlap_index_bound-1 nil 3294156560
("" (skosimp*)
(("" (rewrite "index_conversion_left")
(("" (use "lt_index")
(("" (expand "nonoverlap?")
(("" (inst?) (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil)
((nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(index_conversion_left formula-decl nil event_sequences nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(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)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(increasing? const-decl "bool" event_sequences nil)
(unbounded? const-decl "bool" event_sequences nil)
(event_sequence type-eq-decl nil event_sequences nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(index_of const-decl "nat" event_sequences nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nonoverlap? const-decl "bool" event_sequences nil)
(odd_minus_odd_is_even application-judgement "even_int" integers
nil)
(even_minus_odd_is_odd application-judgement "odd_int" integers
nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(lt_index formula-decl nil event_sequences nil))
shostak)))
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.31Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Entwicklung einer Software für die statische Quellcodeanalyse
|
