|
(ordered_finite_sequences
(extract_one_TCC1 0
(extract_one_TCC1-1 nil 3410288297 ("" (subtype-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(>= const-decl "bool" reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(> const-decl "bool" reals nil)
(below type-eq-decl nil nat_types nil)
(T formal-nonempty-type-decl nil ordered_finite_sequences nil)
(finite_sequence type-eq-decl nil finite_sequences nil)
(ne_seqs type-eq-decl nil seqs "structures/")
(min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
(^ const-decl "finseq" finite_sequences nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(int_min application-judgement "{k: int | k <= i AND k <= j}"
real_defs nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_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)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil))
nil))
(extract_one_TCC2 0
(extract_one_TCC2-1 nil 3410288297 ("" (subtype-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(>= const-decl "bool" reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(> const-decl "bool" reals nil)
(below type-eq-decl nil nat_types nil)
(T formal-nonempty-type-decl nil ordered_finite_sequences nil)
(finite_sequence type-eq-decl nil finite_sequences nil)
(ne_seqs type-eq-decl nil seqs "structures/")
(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)
(int_minus_int_is_int application-judgement "int" 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)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil))
(extract_one 0
(extract_one-1 nil 3410288310
("" (skosimp*)
(("" (expand "^") (("" (lift-if) (("" (assert) nil nil)) nil))
nil))
nil)
((posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(^ const-decl "finseq" finite_sequences nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(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))
nil))
(extract_upper_TCC1 0
(extract_upper_TCC1-1 nil 3410109370
("" (expand "^")
(("" (expand "min")
(("" (skosimp*)
(("" (lift-if)
(("" (assert)
(("" (assert) (("" (ground) (("" (postpone) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((min const-decl "{p: real | p <= m AND p <= n}" real_defs 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)
(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)
(int_minus_int_is_int application-judgement "int" integers nil)
(^ const-decl "finseq" finite_sequences nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil))
nil))
(extract_upper 0
(extract_upper-2 nil 3410111279
("" (skosimp*)
(("" (expand "^")
(("" (expand "min") (("" (lift-if) (("" (assert) nil nil)) nil))
nil))
nil))
nil)
((posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(^ const-decl "finseq" finite_sequences nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(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)
(int_plus_int_is_int application-judgement "int" integers nil)
(min const-decl "{p: real | p <= m AND p <= n}" real_defs nil))
nil)
(extract_upper-1 nil 3410109221
("" (skosimp*)
(("" (expand "^") (("" (lift-if) (("" (assert) nil nil)) nil))
nil))
nil)
nil nil))
(min_extract_TCC1 0
(min_extract_TCC1-1 nil 3409322352
("" (skosimp*)
(("" (expand "^")
(("" (assert)
(("" (expand "min")
(("" (assert) (("" (lift-if) (("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(^ const-decl "finseq" finite_sequences nil)
(min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
(sort_length formula-decl nil sort_seq "structures/")
(T formal-nonempty-type-decl nil ordered_finite_sequences nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(pred type-eq-decl nil defined_types nil)
(total_order? const-decl "bool" orders nil)
(<= formal-const-decl "(total_order?[T])" ordered_finite_sequences
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)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(int_min application-judgement "{k: int | k <= i AND k <= j}"
real_defs nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(int_plus_int_is_int application-judgement "int" integers nil))
nil))
(min_extract_TCC2 0
(min_extract_TCC2-1 nil 3409325353 ("" (subtype-tcc) nil nil)
((NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(>= const-decl "bool" reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(> const-decl "bool" reals nil)
(below type-eq-decl nil nat_types nil)
(finite_sequence type-eq-decl nil finite_sequences nil)
(ne_seqs type-eq-decl nil seqs "structures/")
(<= formal-const-decl "(total_order?[T])" ordered_finite_sequences
nil)
(total_order? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T formal-nonempty-type-decl nil ordered_finite_sequences nil)
(sort_length formula-decl nil sort_seq "structures/"))
nil))
(min_extract 0
(min_extract-1 nil 3409322581
("" (skosimp*)
(("" (typepred "min(sort(s!1) ^ (i!1, j!1))")
(("" (skosimp*)
(("" (replace -2 :dir RL :hide? T)
(("" (typepred "jj!1")
(("" (expand "^")
(("" (lift-if)
(("" (assert)
(("" (case-replace "jj!1 = 0")
(("1" (assert) nil nil)
("2" (inst - "0")
(("2" (typepred "sort(s!1)")
(("2" (expand "increasing?")
(("2" (inst - "i!1" "i!1+jj!1")
(("2" (assert)
(("2"
(typepred "<=")
(("2"
(expand "total_order?")
(("2"
(expand "partial_order?")
(("2"
(expand "antisymmetric?")
(("2"
(flatten)
(("2"
(inst?)
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((min const-decl "{t: T |
(FORALL (ii: dom(s)): t <= seq(s)(ii)) AND
(EXISTS (jj: dom(s)): seq(s)(jj) = t)}" min_seq
"structures/")
(= const-decl "[T, T -> boolean]" equalities nil)
(dom type-eq-decl nil min_seq "structures/")
(ne_seqs type-eq-decl nil seqs "structures/")
(> const-decl "bool" reals nil)
(sort const-decl
"{ss: seqs | permutation?[T, <=](s, ss) AND increasing?(ss)}"
sort_seq "structures/")
(increasing? const-decl "bool" sort_seq "structures/")
(permutation? const-decl "bool" permutations_seq "structures/")
(finite_sequence type-eq-decl nil finite_sequences nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(seqs type-eq-decl nil sort_seq "structures/")
(<= formal-const-decl "(total_order?[T])" ordered_finite_sequences
nil)
(total_order? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_types nil)
(^ const-decl "finseq" finite_sequences nil)
(finseq type-eq-decl nil finite_sequences nil)
(T formal-nonempty-type-decl nil ordered_finite_sequences nil)
(below type-eq-decl nil nat_types nil)
(< const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(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)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(int_min application-judgement "{k: int | k <= i AND k <= j}"
real_defs nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(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)
(sort_length formula-decl nil sort_seq "structures/")
(antisymmetric? const-decl "bool" relations nil)
(partial_order? const-decl "bool" orders nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields
nil))
shostak))
(max_extract_TCC1 0
(max_extract_TCC1-1 nil 3410102768 ("" (subtype-tcc) nil nil)
((NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(>= const-decl "bool" reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(> const-decl "bool" reals nil)
(below type-eq-decl nil nat_types nil)
(finite_sequence type-eq-decl nil finite_sequences nil)
(ne_seqs type-eq-decl nil seqs "structures/")
(<= formal-const-decl "(total_order?[T])" ordered_finite_sequences
nil)
(total_order? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T formal-nonempty-type-decl nil ordered_finite_sequences nil)
(sort_length formula-decl nil sort_seq "structures/"))
nil))
(max_extract 0
(max_extract-1 nil 3410102772
("" (skosimp*)
(("" (typepred "max(sort(s!1) ^ (i!1, j!1))")
(("" (skosimp*)
(("" (replace -2 :dir RL :hide? T)
(("" (typepred "jj!1")
(("" (expand "^")
(("" (lift-if)
(("" (assert)
(("" (expand "min")
(("" (case-replace "jj!1 = j!1-i!1")
(("1" (assert) nil nil)
("2" (inst - "j!1-i!1")
(("1" (assert)
(("1" (typepred "sort(s!1)")
(("1" (expand "increasing?")
(("1"
(inst - "i!1+jj!1" "j!1")
(("1"
(assert)
(("1"
(typepred "<=")
(("1"
(expand "total_order?")
(("1"
(expand "partial_order?")
(("1"
(expand "antisymmetric?")
(("1"
(flatten)
(("1"
(inst?)
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "^")
(("2" (assert)
(("2" (expand "min")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((max const-decl "{t: T |
(FORALL (ii: dom(s)): seq(s)(ii) <= t) AND
(EXISTS (jj: dom(s)): seq(s)(jj) = t)}" max_seq
"structures/")
(= const-decl "[T, T -> boolean]" equalities nil)
(dom type-eq-decl nil max_seq "structures/")
(ne_seqs type-eq-decl nil seqs "structures/")
(> const-decl "bool" reals nil)
(sort const-decl
"{ss: seqs | permutation?[T, <=](s, ss) AND increasing?(ss)}"
sort_seq "structures/")
(increasing? const-decl "bool" sort_seq "structures/")
(permutation? const-decl "bool" permutations_seq "structures/")
(finite_sequence type-eq-decl nil finite_sequences nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(seqs type-eq-decl nil sort_seq "structures/")
(<= formal-const-decl "(total_order?[T])" ordered_finite_sequences
nil)
(total_order? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_types nil)
(^ const-decl "finseq" finite_sequences nil)
(finseq type-eq-decl nil finite_sequences nil)
(T formal-nonempty-type-decl nil ordered_finite_sequences nil)
(below type-eq-decl nil nat_types nil)
(< const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(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)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(int_min application-judgement "{k: int | k <= i AND k <= j}"
real_defs nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(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)
(sort_length formula-decl nil sort_seq "structures/")
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(antisymmetric? const-decl "bool" relations nil)
(partial_order? const-decl "bool" orders nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(s!1 skolem-const-decl "ne_seqs[T]" ordered_finite_sequences nil)
(i!1 skolem-const-decl "nat" ordered_finite_sequences nil)
(j!1 skolem-const-decl "nat" ordered_finite_sequences nil)
(min const-decl "{p: real | p <= m AND p <= n}" real_defs nil))
nil))
(minmax_TCC1 0
(minmax_TCC1-1 nil 3403444278
("" (skosimp*)
(("" (expand "list2finseq")
(("" (expand "length") (("" (assert) nil nil)) nil)) nil))
nil)
((list2finseq const-decl "finseq[T]" list2finseq 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)
(length def-decl "nat" list_props nil))
nil))
(min_le_max 0
(min_le_max-1 nil 3403441120
("" (skosimp*)
(("" (use "min_seq_in?")
(("" (expand "in?")
(("" (skosimp*)
(("" (replace -1 :hide? t) (("" (use "max_seq_lem") nil nil))
nil))
nil))
nil))
nil))
nil)
((min_seq_in? formula-decl nil min_seq "structures/")
(T formal-nonempty-type-decl nil ordered_finite_sequences nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(pred type-eq-decl nil defined_types nil)
(total_order? const-decl "bool" orders nil)
(<= formal-const-decl "(total_order?[T])" ordered_finite_sequences
nil)
(ne_seqs type-eq-decl nil seqs "structures/")
(> 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)
(finite_sequence type-eq-decl nil finite_sequences nil)
(below type-eq-decl nil nat_types nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(below type-eq-decl nil naturalnumbers nil)
(dom type-eq-decl nil max_seq "structures/")
(< const-decl "bool" reals 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)
(max_seq_lem formula-decl nil max_seq "structures/")
(in? const-decl "bool" seqs "structures/"))
nil))
(min_minmax 0
(min_minmax-1 nil 3403446988
("" (skosimp*)
(("" (use "min_seq_it_is")
(("" (assert)
(("" (hide 2)
(("" (prop)
(("1" (skosimp* t)
(("1" (expand "minmax")
(("1" (expand "list2finseq")
(("1" (expand "length")
(("1" (expand "length")
(("1" (expand "length")
(("1" (expand "nth")
(("1" (expand "nth")
(("1" (assert)
(("1"
(lift-if)
(("1"
(prop)
(("1" (use "reflexive") nil nil)
("2" (use "min_le_max") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "in?")
(("2" (inst + 0)
(("2" (expand "minmax")
(("2" (expand "list2finseq")
(("2" (expand "nth") (("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((min_seq_it_is formula-decl nil min_seq "structures/")
(T formal-nonempty-type-decl nil ordered_finite_sequences nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(pred type-eq-decl nil defined_types nil)
(total_order? const-decl "bool" orders nil)
(<= formal-const-decl "(total_order?[T])" ordered_finite_sequences
nil)
(min const-decl "{t: T |
(FORALL (ii: dom(s)): t <= seq(s)(ii)) AND
(EXISTS (jj: dom(s)): seq(s)(jj) = t)}" min_seq
"structures/")
(= const-decl "[T, T -> boolean]" equalities nil)
(dom type-eq-decl nil min_seq "structures/")
(< const-decl "bool" reals 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)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(minmax const-decl "ne_seqs" ordered_finite_sequences nil)
(ne_seqs type-eq-decl nil seqs "structures/")
(> 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)
(finite_sequence type-eq-decl nil finite_sequences nil)
(below type-eq-decl nil nat_types nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(in? const-decl "bool" seqs "structures/")
(below type-eq-decl nil naturalnumbers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(list2finseq const-decl "finseq[T]" list2finseq nil)
(nth def-decl "T" list_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(reflexive formula-decl nil relations_extra nil)
(reflexive? const-decl "bool" relations nil)
(PRED type-eq-decl nil defined_types nil)
(min_le_max formula-decl nil ordered_finite_sequences nil)
(length def-decl "nat" list_props nil))
shostak))
(max_minmax 0
(max_minmax-1 nil 3403447685
("" (skosimp*)
(("" (use "max_seq_it_is")
(("" (assert)
(("" (hide 2)
(("" (prop)
(("1" (skosimp* t)
(("1" (expand "minmax")
(("1" (expand "list2finseq")
(("1" (expand "length")
(("1" (expand "length")
(("1" (expand "length")
(("1" (expand "nth")
(("1" (expand "nth")
(("1" (assert)
(("1"
(lift-if)
(("1"
(prop)
(("1" (use "min_le_max") nil nil)
("2" (use "reflexive") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "in?")
(("2" (inst + 1)
(("1" (expand "minmax")
(("1" (expand "list2finseq")
(("1" (expand "nth")
(("1" (expand "nth") (("1" (propax) nil nil))
nil))
nil))
nil))
nil)
("2" (expand "minmax")
(("2" (expand "list2finseq")
(("2" (expand "length")
(("2" (expand "length") (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((max_seq_it_is formula-decl nil max_seq "structures/")
(T formal-nonempty-type-decl nil ordered_finite_sequences nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(pred type-eq-decl nil defined_types nil)
(total_order? const-decl "bool" orders nil)
(<= formal-const-decl "(total_order?[T])" ordered_finite_sequences
nil)
(max const-decl "{t: T |
(FORALL (ii: dom(s)): seq(s)(ii) <= t) AND
(EXISTS (jj: dom(s)): seq(s)(jj) = t)}" max_seq
"structures/")
(= const-decl "[T, T -> boolean]" equalities nil)
(dom type-eq-decl nil max_seq "structures/")
(< const-decl "bool" reals 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)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(minmax const-decl "ne_seqs" ordered_finite_sequences nil)
(ne_seqs type-eq-decl nil seqs "structures/")
(> 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)
(finite_sequence type-eq-decl nil finite_sequences nil)
(below type-eq-decl nil nat_types nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(in? const-decl "bool" seqs "structures/")
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(below type-eq-decl nil naturalnumbers nil)
(s!1 skolem-const-decl "ne_seqs[T]" ordered_finite_sequences nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(list2finseq const-decl "finseq[T]" list2finseq nil)
(nth def-decl "T" list_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(min_le_max formula-decl nil ordered_finite_sequences nil)
(reflexive formula-decl nil relations_extra nil)
(reflexive? const-decl "bool" relations nil)
(PRED type-eq-decl nil defined_types nil)
(length def-decl "nat" list_props nil))
shostak))
(min_in_consensus 0
(min_in_consensus-1 nil 3403623583
("" (skosimp*) (("" (use "min_seq_in?") nil nil)) nil)
((ne_seqs type-eq-decl nil seqs "structures/")
(> 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)
(finite_sequence type-eq-decl nil finite_sequences nil)
(below type-eq-decl nil nat_types nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(min_seq_in? formula-decl nil min_seq "structures/")
(T formal-nonempty-type-decl nil ordered_finite_sequences nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(pred type-eq-decl nil defined_types nil)
(total_order? const-decl "bool" orders nil)
(<= formal-const-decl "(total_order?[T])" ordered_finite_sequences
nil))
nil))
(max_in_consensus 0
(max_in_consensus-1 nil 3403623583
("" (skosimp*) (("" (use "max_seq_in?") nil nil)) nil)
((ne_seqs type-eq-decl nil seqs "structures/")
(> 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)
(finite_sequence type-eq-decl nil finite_sequences nil)
(below type-eq-decl nil nat_types nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(max_seq_in? formula-decl nil max_seq "structures/")
(T formal-nonempty-type-decl nil ordered_finite_sequences nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(pred type-eq-decl nil defined_types nil)
(total_order? const-decl "bool" orders nil)
(<= formal-const-decl "(total_order?[T])" ordered_finite_sequences
nil))
nil))
(in_consensus 0
(in_consensus-1 nil 3403441741
("" (skosimp* t)
(("" (typepred "x!1(x1!1)")
(("" (expand "in?")
(("" (skosimp*)
(("" (replace*)
(("" (use "min_seq_lem")
(("" (use "max_seq_lem") (("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((in_consensus_function type-eq-decl nil finite_seqs nil)
(in? const-decl "bool" seqs "structures/")
(<= formal-const-decl "(total_order?[T])" ordered_finite_sequences
nil)
(total_order? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_types nil)
(min_seq_lem formula-decl nil min_seq "structures/")
(below type-eq-decl nil naturalnumbers nil)
(dom type-eq-decl nil min_seq "structures/")
(< const-decl "bool" reals nil) (>= const-decl "bool" reals nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(min_in_consensus name-judgement "in_consensus_function"
ordered_finite_sequences nil)
(max_in_consensus name-judgement "in_consensus_function"
ordered_finite_sequences nil)
(dom type-eq-decl nil max_seq "structures/")
(max_seq_lem formula-decl nil max_seq "structures/")
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(> const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(below type-eq-decl nil nat_types nil)
(T formal-nonempty-type-decl nil ordered_finite_sequences nil)
(finite_sequence type-eq-decl nil finite_sequences nil)
(ne_seqs type-eq-decl nil seqs "structures/"))
nil))
(lower_TCC1 0
(lower_TCC1-1 nil 3403492562 ("" (subtype-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(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)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(below type-eq-decl nil nat_types nil)
(T formal-nonempty-type-decl nil ordered_finite_sequences nil)
(finite_sequence type-eq-decl nil finite_sequences nil)
(ne_seqs type-eq-decl nil seqs "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)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(posnat nonempty-type-eq-decl nil integers nil)
(< const-decl "bool" reals nil)
(below type-eq-decl nil naturalnumbers nil))
nil))
(lower_TCC2 0
(lower_TCC2-1 nil 3403492562
("" (skosimp*) (("" (assert) nil nil)) nil)
((real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(sort_length formula-decl nil sort_seq "structures/")
(T formal-nonempty-type-decl nil ordered_finite_sequences nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(pred type-eq-decl nil defined_types nil)
(total_order? const-decl "bool" orders nil)
(<= formal-const-decl "(total_order?[T])" ordered_finite_sequences
nil))
nil))
(lower_TCC3 0
(lower_TCC3-1 nil 3403495511
("" (skosimp*)
(("" (use "finite_below[k!1]")
(("1" (assert) (("1" (skosimp*) (("1" (assert) nil nil)) nil))
nil)
("2" (skosimp*) (("2" (assert) nil nil)) nil))
nil))
nil)
((<= formal-const-decl "(total_order?[T])" ordered_finite_sequences
nil)
(total_order? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T formal-nonempty-type-decl nil ordered_finite_sequences nil)
(sort_length formula-decl nil sort_seq "structures/")
(finite_below formula-decl nil finite_sets_below "finite_sets/")
(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)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(posnat nonempty-type-eq-decl nil integers nil)
(i!1 skolem-const-decl "below(k!1)" ordered_finite_sequences nil)
(k!1 skolem-const-decl "posnat" ordered_finite_sequences nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(s!1 skolem-const-decl "ne_seqs[T]" ordered_finite_sequences nil)
(sort const-decl
"{ss: seqs | permutation?[T, <=](s, ss) AND increasing?(ss)}"
sort_seq "structures/")
(increasing? const-decl "bool" sort_seq "structures/")
(permutation? const-decl "bool" permutations_seq "structures/")
(seqs type-eq-decl nil sort_seq "structures/")
(ne_seqs type-eq-decl nil seqs "structures/")
(finite_sequence type-eq-decl nil finite_sequences nil)
(below type-eq-decl nil nat_types nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(set type-eq-decl nil sets nil)
(below type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
nil))
(upper_TCC1 0
(upper_TCC1-1 nil 3403492562
("" (skosimp*)
(("" (use "finite_below[k!1]")
(("1" (skosimp*) (("1" (assert) nil nil)) nil)
("2" (skosimp*) (("2" (assert) nil nil)) nil))
nil))
nil)
((<= formal-const-decl "(total_order?[T])" ordered_finite_sequences
nil)
(total_order? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T formal-nonempty-type-decl nil ordered_finite_sequences nil)
(sort_length formula-decl nil sort_seq "structures/")
(finite_below formula-decl nil finite_sets_below "finite_sets/")
(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)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(posnat nonempty-type-eq-decl nil integers nil)
(k!1 skolem-const-decl "posnat" ordered_finite_sequences nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(s!1 skolem-const-decl "ne_seqs[T]" ordered_finite_sequences nil)
(i!1 skolem-const-decl "below(k!1)" ordered_finite_sequences nil)
(sort const-decl
"{ss: seqs | permutation?[T, <=](s, ss) AND increasing?(ss)}"
sort_seq "structures/")
(increasing? const-decl "bool" sort_seq "structures/")
(permutation? const-decl "bool" permutations_seq "structures/")
(seqs type-eq-decl nil sort_seq "structures/")
(ne_seqs type-eq-decl nil seqs "structures/")
(finite_sequence type-eq-decl nil finite_sequences nil)
(below type-eq-decl nil nat_types nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(set type-eq-decl nil sets nil)
(below type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
nil))
(map_set_TCC1 0
(map_set_TCC1-1 nil 3406993589
("" (skosimp*)
(("" (rewrite "finite_below")
(("" (skosimp*) (("" (assert) nil nil)) nil)) nil))
nil)
((real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
nil))
(map_set_TCC2 0
(map_set_TCC2-1 nil 3406994305
("" (skosimp*)
(("" (rewrite "finite_below")
(("" (skosimp*) (("" (assert) nil nil)) nil)) nil))
nil)
((real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
nil))
(map_set_TCC3 0
(map_set_TCC3-1 nil 3407064954
("" (skosimp*)
(("" (rewrite "finite_below")
(("1" (skosimp*) (("1" (assert) nil nil)) nil)
("2" (skosimp*) (("2" (assert) nil nil)) nil))
nil))
nil)
((IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(finite_below formula-decl nil finite_sets_below "finite_sets/")
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(below type-eq-decl nil naturalnumbers nil)
(set type-eq-decl nil sets nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(below type-eq-decl nil nat_types nil)
(T formal-nonempty-type-decl nil ordered_finite_sequences nil)
(finite_sequence type-eq-decl nil finite_sequences nil)
(ne_seqs type-eq-decl nil seqs "structures/")
(is_finite const-decl "bool" finite_sets nil)
(finite_set type-eq-decl nil finite_sets nil)
(pred type-eq-decl nil defined_types nil)
(total_order? const-decl "bool" orders nil)
(<= formal-const-decl "(total_order?[T])" ordered_finite_sequences
nil)
(seqs type-eq-decl nil sort_seq "structures/")
(bijective? const-decl "bool" functions nil)
(permutation? const-decl "bool" permutations_seq "structures/")
(increasing? const-decl "bool" sort_seq "structures/")
(sort const-decl
"{ss: seqs | permutation?[T, <=](s, ss) AND increasing?(ss)}"
sort_seq "structures/")
(sort_map const-decl "{map: [below(length(s)) -> below(length(s))] |
bijective?(map) AND
(FORALL (i: below(length(s))): seq(s)(i) = seq(sort(s))(map(i)))}"
sort_seq "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)
(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)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(posnat nonempty-type-eq-decl nil integers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
nil))
(map_subset_lower_TCC1 0
(map_subset_lower_TCC1-1 nil 3407078876
("" (skosimp*) (("" (rewrite "finite_below") nil nil)) nil)
((finite_below formula-decl nil finite_sets_below "finite_sets/")
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(below type-eq-decl nil naturalnumbers nil)
(set type-eq-decl nil sets nil) (<= const-decl "bool" reals 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)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(posnat nonempty-type-eq-decl nil integers nil))
nil))
(map_subset_lower 0
(map_subset_lower-1 nil 3407078741
("" (skosimp*)
(("" (expand "subset?")
(("" (expand "member")
(("" (expand "lower")
(("" (expand "map_set")
(("" (assert)
(("" (skosimp*)
(("" (typepred "sort_map(s!1)")
(("" (inst?)
(("" (case "sort_map(s!1)(x!1) = i!1")
(("1" (typepred "<=")
(("1" (expand "total_order?")
(("1" (expand "partial_order?")
(("1" (expand "preorder?")
(("1"
(expand "reflexive?")
(("1"
(flatten)
(("1"
(inst - "s!1`seq(x!1)")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (typepred "sort(s!1)")
(("2" (expand "increasing?")
(("2" (inst - "sort_map(s!1)(x!1)" "i!1")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((subset? const-decl "bool" sets nil)
(lower const-decl "finite_set[below(k)]" ordered_finite_sequences
nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(sort_map const-decl "{map: [below(length(s)) -> below(length(s))] |
bijective?(map) AND
(FORALL (i: below(length(s))): seq(s)(i) = seq(sort(s))(map(i)))}"
sort_seq "structures/")
(sort const-decl
"{ss: seqs | permutation?[T, <=](s, ss) AND increasing?(ss)}"
sort_seq "structures/")
(increasing? const-decl "bool" sort_seq "structures/")
(permutation? const-decl "bool" permutations_seq "structures/")
(= const-decl "[T, T -> boolean]" equalities nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(seqs type-eq-decl nil sort_seq "structures/")
(<= formal-const-decl "(total_order?[T])" ordered_finite_sequences
nil)
(total_order? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_types nil)
(bijective? const-decl "bool" functions nil)
(below type-eq-decl nil naturalnumbers nil)
(ne_seqs type-eq-decl nil seqs "structures/")
(> const-decl "bool" reals nil)
(finite_sequence type-eq-decl nil finite_sequences nil)
(T formal-nonempty-type-decl nil ordered_finite_sequences nil)
(below type-eq-decl nil nat_types nil)
(< const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(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)
(preorder? const-decl "bool" orders nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(reflexive? const-decl "bool" relations nil)
(partial_order? const-decl "bool" orders nil)
(sort_length formula-decl nil sort_seq "structures/")
(nonneg_int nonempty-type-eq-decl nil integers nil)
(posnat nonempty-type-eq-decl nil integers nil)
(map_set const-decl "finite_set[below(k)]" ordered_finite_sequences
nil)
(member const-decl "bool" sets nil))
nil))
(map_subset_upper_TCC1 0
(map_subset_upper_TCC1-1 nil 3407081389
("" (skosimp*) (("" (rewrite "finite_below") nil nil)) nil)
((finite_below formula-decl nil finite_sets_below "finite_sets/")
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(below type-eq-decl nil naturalnumbers nil)
(set type-eq-decl nil sets nil) (<= const-decl "bool" reals 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)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(posnat nonempty-type-eq-decl nil integers nil))
nil))
(map_subset_upper 0
(map_subset_upper-2 nil 3407081571
("" (skosimp*)
(("" (expand "subset?")
(("" (expand "member")
(("" (expand "upper")
(("" (expand "map_set")
(("" (assert)
(("" (skosimp*)
(("" (typepred "sort_map(s!1)")
(("" (inst?)
(("" (case "sort_map(s!1)(x!1) = i!1")
(("1" (typepred "<=")
(("1" (expand "total_order?")
(("1" (expand "partial_order?")
(("1" (expand "preorder?")
(("1"
(expand "reflexive?")
(("1"
(flatten)
(("1"
(inst - "s!1`seq(x!1)")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (typepred "sort(s!1)")
(("2" (expand "increasing?")
(("2" (inst - "i!1" "sort_map(s!1)(x!1)")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((subset? const-decl "bool" sets nil)
(upper const-decl "finite_set[below(k)]" ordered_finite_sequences
nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(sort_map const-decl "{map: [below(length(s)) -> below(length(s))] |
bijective?(map) AND
(FORALL (i: below(length(s))): seq(s)(i) = seq(sort(s))(map(i)))}"
sort_seq "structures/")
(sort const-decl
"{ss: seqs | permutation?[T, <=](s, ss) AND increasing?(ss)}"
sort_seq "structures/")
(increasing? const-decl "bool" sort_seq "structures/")
(permutation? const-decl "bool" permutations_seq "structures/")
(= const-decl "[T, T -> boolean]" equalities nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(seqs type-eq-decl nil sort_seq "structures/")
(<= formal-const-decl "(total_order?[T])" ordered_finite_sequences
nil)
(total_order? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_types nil)
(bijective? const-decl "bool" functions nil)
(below type-eq-decl nil naturalnumbers nil)
(ne_seqs type-eq-decl nil seqs "structures/")
(> const-decl "bool" reals nil)
(finite_sequence type-eq-decl nil finite_sequences nil)
(T formal-nonempty-type-decl nil ordered_finite_sequences nil)
(below type-eq-decl nil nat_types nil)
(< const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(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)
(preorder? const-decl "bool" orders nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(reflexive? const-decl "bool" relations nil)
(partial_order? const-decl "bool" orders nil)
(sort_length formula-decl nil sort_seq "structures/")
(nonneg_int nonempty-type-eq-decl nil integers nil)
(posnat nonempty-type-eq-decl nil integers nil)
(map_set const-decl "finite_set[below(k)]" ordered_finite_sequences
nil)
(member const-decl "bool" sets nil))
nil)
(map_subset_upper-1 nil 3407081559 ("" (postpone) nil nil) nil
shostak))
(mapper_TCC1 0
(mapper_TCC1-1 nil 3407078375 ("" (subtype-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(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)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(below type-eq-decl nil nat_types nil)
(T formal-nonempty-type-decl nil ordered_finite_sequences nil)
(finite_sequence type-eq-decl nil finite_sequences nil)
(ne_seqs type-eq-decl nil seqs "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)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(posnat nonempty-type-eq-decl nil integers nil)
(< const-decl "bool" reals nil)
(below type-eq-decl nil naturalnumbers nil)
(set type-eq-decl nil sets nil)
(is_finite const-decl "bool" finite_sets nil)
(finite_set type-eq-decl nil finite_sets nil)
(map_set const-decl "finite_set[below(k)]" ordered_finite_sequences
nil)
(injective? const-decl "bool" functions nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
nil))
(mapper_TCC2 0
(mapper_TCC2-1 nil 3407078375 ("" (subtype-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(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)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(below type-eq-decl nil nat_types nil)
(T formal-nonempty-type-decl nil ordered_finite_sequences nil)
(finite_sequence type-eq-decl nil finite_sequences nil)
(ne_seqs type-eq-decl nil seqs "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)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(posnat nonempty-type-eq-decl nil integers nil)
(< const-decl "bool" reals nil)
(below type-eq-decl nil naturalnumbers nil)
(set type-eq-decl nil sets nil)
(is_finite const-decl "bool" finite_sets nil)
(finite_set type-eq-decl nil finite_sets nil)
(map_set const-decl "finite_set[below(k)]" ordered_finite_sequences
nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(injective? const-decl "bool" functions nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
nil))
(map_card_eq 0
(map_card_eq-1 nil 3407078529
("" (skosimp*)
(("" (use "card_eq_bij[below(k!1), below(k!1)]")
(("" (assert)
(("" (hide 2)
(("" (inst + "mapper(s!1,k!1,a!1)")
(("" (typepred "sort_map(s!1)")
(("" (hide-all-but (-1 1))
(("" (expand "bijective?")
(("" (expand "mapper")
(("" (ground)
(("1" (expand "injective?")
(("1" (skosimp*)
(("1" (inst - "x1!1" "x2!1")
(("1" (assert) nil nil)) nil))
nil))
nil)
("2" (expand "surjective?")
(("2" (skosimp*)
(("2" (inst-cp - "y!1")
(("2" (skosimp*)
(("2"
(inst-cp + "x!1")
(("2"
(expand "map_set")
(("2"
(typepred "y!1")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((card_eq_bij formula-decl nil finite_sets_card_eq "finite_sets/")
(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)
(< const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(posnat nonempty-type-eq-decl nil integers nil)
(below type-eq-decl nil naturalnumbers nil)
(map_set const-decl "finite_set[below(k)]" ordered_finite_sequences
nil)
(ne_seqs type-eq-decl nil seqs "structures/")
(finite_sequence type-eq-decl nil finite_sequences nil)
(T formal-nonempty-type-decl nil ordered_finite_sequences nil)
(below type-eq-decl nil nat_types nil)
(finite_set type-eq-decl nil finite_sets nil)
(is_finite const-decl "bool" finite_sets nil)
(set type-eq-decl nil sets nil)
(sort_map const-decl "{map: [below(length(s)) -> below(length(s))] |
bijective?(map) AND
(FORALL (i: below(length(s))): seq(s)(i) = seq(sort(s))(map(i)))}"
sort_seq "structures/")
(sort const-decl
"{ss: seqs | permutation?[T, <=](s, ss) AND increasing?(ss)}"
sort_seq "structures/")
(increasing? const-decl "bool" sort_seq "structures/")
(permutation? const-decl "bool" permutations_seq "structures/")
(= const-decl "[T, T -> boolean]" equalities nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(seqs type-eq-decl nil sort_seq "structures/")
(<= formal-const-decl "(total_order?[T])" ordered_finite_sequences
nil)
(total_order? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_types nil)
(bijective? const-decl "bool" functions nil)
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.826 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
