| products/Sources/formale Sprachen/PVS/fault_tolerance/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: reduce_properties.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(reduce_properties
(lowset_TCC1 0 (lowset_TCC1-1 nil 3414332066 ("" (subtype-tcc) nil nil) ((T formal-nonempty-type-decl nil reduce_properties nil) (N formal-const-decl "posnat" reduce_properties nil) (posnat 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) (vec2seq const-decl "finite_sequence[T]" node nil) (<= formal-const-decl "(total_order?[T])" reduce_properties nil) (total_order? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil) (sort_length formula-decl nil sort_seq "structures/")) nil)) (card_lower_leq_lowset_TCC1 0 (card_lower_leq_lowset_TCC1-1 nil 3414517228 ("" (subtype-tcc) nil nil) nil nil)) (card_lower_leq_lowset 0 (card_lower_leq_lowset-1 nil 3414360330 ("" (skosimp*) (("" (rewrite "injection_and_cardinal") (("" (hide 2) (("" (inst + "m(enabled!1)") (("1" (assert) (("1" (use "injective_restrict[below(card[below(N)](enabled!1)), (lower[T, <=] (vec2seq(v!1,enabled!1), card[below(N)](enabled!1), i!1)), (enabled!1)]") (("1" (prop) (("1" (expand "injective?") (("1" (propax) nil nil)) nil) ("2" (assert) (("2" (typepred "m(enabled!1)") (("2" (expand "bijective?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp* t) (("2" (expand "lowset") (("2" (expand "lower") (("2" (flatten) (("2" (expand "vec2seq") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((vec2seq_type application-judgement "ne_seqs[T]" reduce_properties nil) (injection_and_cardinal formula-decl nil finite_sets_card_eq "finite_sets/") (below type-eq-decl nil nat_types nil) (T formal-nonempty-type-decl nil reduce_properties nil) (finite_sequence type-eq-decl nil finite_sequences nil) (ne_seqs type-eq-decl nil seqs "structures/") (pred type-eq-decl nil defined_types nil) (total_order? const-decl "bool" orders nil) (<= formal-const-decl "(total_order?[T])" reduce_properties nil) (lower const-decl "finite_set[below(k)]" ordered_finite_sequences nil) (vec type-eq-decl nil node nil) (nodeid_set type-eq-decl nil node nil) (vec2seq const-decl "finite_sequence[T]" node nil) (lowset const-decl "finite_set[below(N)]" reduce_properties 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) (< 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) (N formal-const-decl "posnat" reduce_properties 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) (= const-decl "[T, T -> boolean]" equalities nil) (Card const-decl "nat" finite_sets nil) (card const-decl "{n: nat | n = Card(S)}" finite_sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (empty? const-decl "bool" sets nil) (non_empty_finite_set type-eq-decl nil finite_sets 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) (restrict_of_inj_is_inj application-judgement "(injective?[S, R])" restrict nil) (m const-decl "(bijective?[below(card(enabled)), (enabled)])" node nil) (bijective? const-decl "bool" functions nil) (nodeid_nonempty type-eq-decl nil node nil) (i!1 skolem-const-decl "below(card(enabled!1))" reduce_properties nil) (v!1 skolem-const-decl "vec[N, T]" reduce_properties nil) (enabled!1 skolem-const-decl "non_empty_finite_set[below(N)]" reduce_properties nil) (restrict const-decl "R" restrict nil) (injective_restrict formula-decl nil restrict nil) (injective? const-decl "bool" functions nil)) nil)) (card_lowset 0 (card_lowset-1 nil 3414360315 ("" (skosimp*) (("" (use "card_lower_leq_lowset") (("" (use "card_lower") (("" (assert) (("" (expand "vec2seq") (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ((card_lower_leq_lowset formula-decl nil reduce_properties nil) (card const-decl "{n: nat | n = Card(S)}" finite_sets nil) (Card const-decl "nat" finite_sets nil) (= const-decl "[T, T -> boolean]" equalities nil) (vec type-eq-decl nil node nil) (T formal-nonempty-type-decl nil reduce_properties nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (empty? const-decl "bool" sets nil) (NOT const-decl "[bool -> bool]" booleans 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) (below type-eq-decl nil naturalnumbers nil) (N formal-const-decl "posnat" reduce_properties nil) (posnat 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) (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) (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) (int_minus_int_is_int application-judgement "int" integers nil) (vec2seq_type application-judgement "ne_seqs[T]" reduce_properties nil) (vec2seq const-decl "finite_sequence[T]" node nil) (nodeid_set type-eq-decl nil node nil) (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) (card_lower formula-decl nil ordered_finite_sequences nil) (pred type-eq-decl nil defined_types nil) (total_order? const-decl "bool" orders nil) (<= formal-const-decl "(total_order?[T])" reduce_properties nil)) nil)) (card_upper_leq_highset 0 (card_upper_leq_highset-1 nil 3414360497 ("" (skosimp*) (("" (rewrite "injection_and_cardinal") (("" (hide 2) (("" (inst + "m(enabled!1)") (("1" (assert) (("1" (use "injective_restrict[below(card[below(N)](enabled!1)), (upper[T, <=] (vec2seq(v!1,enabled!1), card[below(N)](enabled!1), i!1)), (enabled!1)]") (("1" (prop) (("1" (expand "injective?") (("1" (propax) nil nil)) nil) ("2" (typepred "m(enabled!1)") (("2" (expand "bijective?") (("2" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp* t) (("2" (expand "upper") (("2" (expand "highset") (("2" (flatten) (("2" (expand "vec2seq") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((vec2seq_type application-judgement "ne_seqs[T]" reduce_properties nil) (injection_and_cardinal formula-decl nil finite_sets_card_eq "finite_sets/") (below type-eq-decl nil nat_types nil) (T formal-nonempty-type-decl nil reduce_properties nil) (finite_sequence type-eq-decl nil finite_sequences nil) (ne_seqs type-eq-decl nil seqs "structures/") (pred type-eq-decl nil defined_types nil) (total_order? const-decl "bool" orders nil) (<= formal-const-decl "(total_order?[T])" reduce_properties nil) (upper const-decl "finite_set[below(k)]" ordered_finite_sequences nil) (vec type-eq-decl nil node nil) (nodeid_set type-eq-decl nil node nil) (vec2seq const-decl "finite_sequence[T]" node nil) (highset const-decl "finite_set[below(N)]" reduce_properties 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) (< 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) (N formal-const-decl "posnat" reduce_properties 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) (= const-decl "[T, T -> boolean]" equalities nil) (Card const-decl "nat" finite_sets nil) (card const-decl "{n: nat | n = Card(S)}" finite_sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (empty? const-decl "bool" sets nil) (non_empty_finite_set type-eq-decl nil finite_sets 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) (restrict_of_inj_is_inj application-judgement "(injective?[S, R])" restrict nil) (m const-decl "(bijective?[below(card(enabled)), (enabled)])" node nil) (bijective? const-decl "bool" functions nil) (nodeid_nonempty type-eq-decl nil node nil) (i!1 skolem-const-decl "below(card(enabled!1))" reduce_properties nil) (v!1 skolem-const-decl "vec[N, T]" reduce_properties nil) (enabled!1 skolem-const-decl "non_empty_finite_set[below(N)]" reduce_properties nil) (restrict const-decl "R" restrict nil) (injective_restrict formula-decl nil restrict nil) (injective? const-decl "bool" functions nil)) nil)) (card_highset 0 (card_highset-1 nil 3414360535 ("" (skosimp*) (("" (use "card_upper_leq_highset") (("" (use "card_upper") (("" (assert) (("" (expand "vec2seq") (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ((card_upper_leq_highset formula-decl nil reduce_properties nil) (card const-decl "{n: nat | n = Card(S)}" finite_sets nil) (Card const-decl "nat" finite_sets nil) (= const-decl "[T, T -> boolean]" equalities nil) (vec type-eq-decl nil node nil) (T formal-nonempty-type-decl nil reduce_properties nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (empty? const-decl "bool" sets nil) (NOT const-decl "[bool -> bool]" booleans 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) (below type-eq-decl nil naturalnumbers nil) (N formal-const-decl "posnat" reduce_properties nil) (posnat 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) (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) (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) (vec2seq_type application-judgement "ne_seqs[T]" reduce_properties nil) (vec2seq const-decl "finite_sequence[T]" node nil) (nodeid_set type-eq-decl nil node nil) (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) (card_upper formula-decl nil ordered_finite_sequences nil) (pred type-eq-decl nil defined_types nil) (total_order? const-decl "bool" orders nil) (<= formal-const-decl "(total_order?[T])" reduce_properties nil)) nil)) (reduce_TCC1 0 (reduce_TCC1-1 nil 3410868997 ("" (subtype-tcc) nil nil) ((T formal-nonempty-type-decl nil reduce_properties nil) (N formal-const-decl "posnat" reduce_properties nil) (posnat 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) (vec2seq const-decl "finite_sequence[T]" node nil)) nil)) (reduce_TCC2 0 (reduce_TCC2-1 nil 3410868997 ("" (subtype-tcc) nil nil) ((T formal-nonempty-type-decl nil reduce_properties nil) (N formal-const-decl "posnat" reduce_properties nil) (posnat 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) (vec2seq const-decl "finite_sequence[T]" node nil) (int_minus_int_is_int application-judgement "int" integers nil)) nil)) (reduce_TCC3 0 (reduce_TCC3-1 nil 3410868997 ("" (subtype-tcc) nil nil) ((T formal-nonempty-type-decl nil reduce_properties nil) (N formal-const-decl "posnat" reduce_properties nil) (posnat 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) (vec2seq const-decl "finite_sequence[T]" node nil) (<= formal-const-decl "(total_order?[T])" reduce_properties nil) (total_order? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil) (sort_length formula-decl nil sort_seq "structures/") (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (^ const-decl "finseq" finite_sequences 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) (posint_plus_nnint_is_posint application-judgement "posint" integers nil)) nil)) (min_reduce_TCC1 0 (min_reduce_TCC1-1 nil 3414417122 ("" (skosimp*) (("" (typepred "enabled!1") (("" (use "nonempty_card[below(N)]") (("" (expand "nonempty?") (("" (propax) nil nil)) nil)) nil)) nil)) nil) ((non_empty_finite_set type-eq-decl nil finite_sets nil) (empty? const-decl "bool" sets 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) (below type-eq-decl nil naturalnumbers nil) (N formal-const-decl "posnat" reduce_properties nil) (posnat 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) (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) (nonempty? const-decl "bool" sets nil) (nonempty_card formula-decl nil finite_sets nil)) nil)) (min_reduce_TCC2 0 (min_reduce_TCC2-1 nil 3414517228 ("" (subtype-tcc) nil nil) ((NOT const-decl "[bool -> bool]" booleans nil) (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) (is_finite const-decl "bool" finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (empty? const-decl "bool" sets nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (member const-decl "bool" sets nil) (injective? const-decl "bool" functions nil) (T formal-nonempty-type-decl nil reduce_properties nil) (N formal-const-decl "posnat" reduce_properties nil) (posnat 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) (vec2seq const-decl "finite_sequence[T]" node nil) (<= formal-const-decl "(total_order?[T])" reduce_properties nil) (total_order? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil) (sort_length formula-decl nil sort_seq "structures/")) nil)) (min_reduce 0 (min_reduce-2 nil 3414419521 ("" (skosimp*) (("" (expand "reduce") (("" (rewrite "min_extract") (("" (expand "vec2seq") (("" (propax) nil nil)) nil)) nil)) nil)) nil) ((int_minus_int_is_int application-judgement "int" integers nil) (reduce const-decl "ne_seqs" reduce_properties 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) (<= formal-const-decl "(total_order?[T])" reduce_properties 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 reduce_properties nil) (ne_seqs type-eq-decl nil seqs "structures/") (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (empty? const-decl "bool" sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (finite_set type-eq-decl nil finite_sets nil) (vec2seq const-decl "finite_sequence[T]" node nil) (finite_sequence type-eq-decl nil finite_sequences nil) (below type-eq-decl nil nat_types nil) (nodeid_set type-eq-decl nil node nil) (is_finite const-decl "bool" finite_sets nil) (set type-eq-decl nil sets nil) (vec type-eq-decl nil node nil) (below type-eq-decl nil naturalnumbers nil) (N formal-const-decl "posnat" reduce_properties nil) (tau_type type-eq-decl nil tau_declaration nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (< const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers 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) (min_extract formula-decl nil ordered_finite_sequences nil) (vec2seq_type application-judgement "ne_seqs[T]" reduce_properties nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil) (min_reduce-1 nil 3414417123 ("" (skosimp*) (("" (rewrite "min_reduce_0") (("" (expand "reduce") (("" (expand "^") (("" (rewrite "vec2seq_length") (("" (assert) (("" (rewrite "vec2seq_length") (("" (assert) (("" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((vec type-eq-decl nil node nil) (tau_type type-eq-decl nil tau_declaration nil)) shostak)) (max_reduce_TCC1 0 (max_reduce_TCC1-1 nil 3414417329 ("" (subtype-tcc) nil nil) ((NOT const-decl "[bool -> bool]" booleans nil) (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) (is_finite const-decl "bool" finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (empty? const-decl "bool" sets nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (member const-decl "bool" sets nil) (injective? const-decl "bool" functions nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (T formal-nonempty-type-decl nil reduce_properties nil) (N formal-const-decl "posnat" reduce_properties nil) (posnat 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) (vec2seq const-decl "finite_sequence[T]" node nil) (<= formal-const-decl "(total_order?[T])" reduce_properties nil) (total_order? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil) (sort_length formula-decl nil sort_seq "structures/") (int_minus_int_is_int application-judgement "int" integers nil)) nil)) (max_reduce 0 (max_reduce-2 nil 3414419428 ("" (skosimp*) (("" (expand "reduce") (("" (rewrite "max_extract") (("" (expand "vec2seq") (("" (propax) nil nil)) nil)) nil)) nil)) nil) ((int_minus_int_is_int application-judgement "int" integers nil) (reduce const-decl "ne_seqs" reduce_properties 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) (<= formal-const-decl "(total_order?[T])" reduce_properties 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 reduce_properties nil) (ne_seqs type-eq-decl nil seqs "structures/") (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (empty? const-decl "bool" sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (finite_set type-eq-decl nil finite_sets nil) (vec2seq const-decl "finite_sequence[T]" node nil) (finite_sequence type-eq-decl nil finite_sequences nil) (below type-eq-decl nil nat_types nil) (nodeid_set type-eq-decl nil node nil) (is_finite const-decl "bool" finite_sets nil) (set type-eq-decl nil sets nil) (vec type-eq-decl nil node nil) (below type-eq-decl nil naturalnumbers nil) (N formal-const-decl "posnat" reduce_properties nil) (tau_type type-eq-decl nil tau_declaration nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (< const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers 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) (max_extract formula-decl nil ordered_finite_sequences nil) (vec2seq_type application-judgement "ne_seqs[T]" reduce_properties nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil) (max_reduce-1 nil 3414417330 ("" (skosimp*) (("" (rewrite "max_reduce_last") (("" (expand "reduce") (("" (expand "^") (("" (rewrite "vec2seq_length") (("" (assert) (("" (rewrite "vec2seq_length") (("" (assert) (("" (expand "min") (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((vec type-eq-decl nil node nil) (tau_type type-eq-decl nil tau_declaration nil)) shostak)) (reduce_length 0 (reduce_length-1 nil 3410269193 ("" (expand "reduce") (("" (expand "M") (("" (expand "^") (("" (skosimp*) (("" (lift-if) (("" (assert) (("" (expand "vec2seq") (("" (assert) (("" (expand "min") (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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) (M const-decl "posnat" pigeonhole nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (vec2seq_type application-judgement "ne_seqs[T]" reduce_properties nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (<= formal-const-decl "(total_order?[T])" reduce_properties 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 reduce_properties nil) (sort_length formula-decl nil sort_seq "structures/") (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (vec2seq const-decl "finite_sequence[T]" node nil) (^ const-decl "finseq" finite_sequences nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (reduce const-decl "ne_seqs" reduce_properties nil) (int_minus_int_is_int application-judgement "int" integers nil)) shostak)) (reduce_rewrite_TCC1 0 (reduce_rewrite_TCC1-1 nil 3414419829 ("" (subtype-tcc) nil nil) ((non_empty_finite_set type-eq-decl nil finite_sets nil) (empty? const-decl "bool" sets 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) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (injective? const-decl "bool" functions nil) (member const-decl "bool" sets nil) (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_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_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (M const-decl "posnat" pigeonhole nil) (T formal-nonempty-type-decl nil reduce_properties nil) (N formal-const-decl "posnat" reduce_properties nil) (posnat 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) (vec2seq const-decl "finite_sequence[T]" node nil) (<= formal-const-decl "(total_order?[T])" reduce_properties nil) (total_order? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil) (sort_length formula-decl nil sort_seq "structures/") (reduce const-decl "ne_seqs" reduce_properties 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) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (int_minus_int_is_int application-judgement "int" integers nil)) nil)) (reduce_rewrite_TCC2 0 (reduce_rewrite_TCC2-1 nil 3414419829 ("" (subtype-tcc) nil nil) ((non_empty_finite_set type-eq-decl nil finite_sets nil) (empty? const-decl "bool" sets 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) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (injective? const-decl "bool" functions nil) (member const-decl "bool" sets nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_lt_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) (M const-decl "posnat" pigeonhole nil) (T formal-nonempty-type-decl nil reduce_properties nil) (N formal-const-decl "posnat" reduce_properties nil) (posnat 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) (vec2seq const-decl "finite_sequence[T]" node nil) (<= formal-const-decl "(total_order?[T])" reduce_properties nil) (total_order? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil) (sort_length formula-decl nil sort_seq "structures/") (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)) nil)) (reduce_rewrite 0 (reduce_rewrite-1 nil 3414419830 ("" (skosimp*) (("" (expand* "reduce" "M" "^" "vec2seq") (("" (assert) nil nil)) nil)) nil) ((M const-decl "posnat" pigeonhole nil) (vec2seq const-decl "finite_sequence[T]" node nil) (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) (int_minus_int_is_int application-judgement "int" integers nil) (^ const-decl "finseq" finite_sequences nil) (reduce const-decl "ne_seqs" reduce_properties 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) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (sort_length formula-decl nil sort_seq "structures/") (T formal-nonempty-type-decl nil reduce_properties 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])" reduce_properties nil)) shostak)) (reduce_overlap_TCC1 0 (reduce_overlap_TCC1-1 nil 3403463828 ("" (subtype-tcc) nil nil) ((non_empty_finite_set type-eq-decl nil finite_sets nil) (empty? const-decl "bool" sets 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) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (real_lt_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) (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) (int_plus_int_is_int application-judgement "int" integers nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (^ const-decl "finseq" finite_sequences nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (member const-decl "bool" sets nil) (injective? const-decl "bool" functions nil) (M const-decl "posnat" pigeonhole nil) (T formal-nonempty-type-decl nil reduce_properties nil) (N formal-const-decl "posnat" reduce_properties nil) (posnat 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) (vec2seq const-decl "finite_sequence[T]" node nil) (<= formal-const-decl "(total_order?[T])" reduce_properties nil) (total_order? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil) (sort_length formula-decl nil sort_seq "structures/") (reduce const-decl "ne_seqs" reduce_properties 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) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (int_minus_int_is_int application-judgement "int" integers nil)) nil)) (reduce_overlap 0 (reduce_overlap-2 nil 3410883954 ("" (skosimp*) (("" (rewrite "reduce_rewrite") (("" (rewrite "reduce_rewrite") (("" (expand "M") (("" (lemma "sort_overlap") (("" (inst - "card(enabled!1)" "vec2seq(v2!1, enabled!1)" "vec2seq(v1!1, enabled!1)") (("" (expand "vec2seq") (("" (inst?) (("1" (skosimp*) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((reduce_rewrite formula-decl nil reduce_properties 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) (< 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) (N formal-const-decl "posnat" reduce_properties 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) (NOT const-decl "[bool -> bool]" booleans nil) (empty? const-decl "bool" sets nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (tau_type type-eq-decl nil tau_declaration nil) (T formal-nonempty-type-decl nil reduce_properties nil) (vec type-eq-decl nil node nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (vec2seq_type application-judgement "ne_seqs[T]" reduce_properties nil) (M const-decl "posnat" pigeonhole nil) (vec2seq const-decl "finite_sequence[T]" node nil) (nodeid_set type-eq-decl nil node nil) (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) (card const-decl "{n: nat | n = Card(S)}" finite_sets nil) (Card const-decl "nat" finite_sets nil) (= const-decl "[T, T -> boolean]" equalities nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (tau!1 skolem-const-decl "tau_type" reduce_properties nil) (enabled!1 skolem-const-decl "non_empty_finite_set[below(N)]" reduce_properties nil) (i!1 skolem-const-decl "nat" reduce_properties nil) (m const-decl "(bijective?[below(card(enabled)), (enabled)])" node nil) (bijective? const-decl "bool" functions nil) (nodeid_nonempty type-eq-decl nil node nil) (int_minus_int_is_int application-judgement "int" 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) (<= formal-const-decl "(total_order?[T])" reduce_properties nil) (total_order? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil) (sort_overlap formula-decl nil ordered_finite_sequences nil)) nil) (reduce_overlap-1 nil 3403464275 ("" (skosimp*) (("" (expand "reduce") (("" (expand "M") (("" (use "index_overlap") (("1" (assert) nil nil) ("2" (use "card_below") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((card_below formula-decl nil finite_sets_below "finite_sets/") (M const-decl "posnat" pigeonhole nil)) shostak)) (reduce_agreement 0 (reduce_agreement-2 nil 3403436930 ("" (skosimp*) (("" (use "vec2seq_agreement") (("" (expand "reduce") (("" (assert) nil nil)) nil)) nil)) nil) ((vec2seq_agreement formula-decl nil node 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) (N formal-const-decl "posnat" reduce_properties nil) (T formal-nonempty-type-decl nil reduce_properties nil) (vec type-eq-decl nil node nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (empty? const-decl "bool" sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (finite_set type-eq-decl nil finite_sets nil) (nodeid_set type-eq-decl nil node nil) (is_finite const-decl "bool" finite_sets 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) (int_minus_int_is_int application-judgement "int" integers nil) (vec2seq_type application-judgement "ne_seqs[T]" reduce_properties nil) (reduce const-decl "ne_seqs" reduce_properties nil)) nil) (reduce_agreement-1 nil 3403436637 ("" (skosimp*) (("" (expand "reduce") (("" (apply-extensionality :hide? t) (("1" (postpone) nil nil) ("2" (postpone) nil nil)) nil)) nil)) nil) nil shostak)) (min_validity 0 (min_validity-3 nil 3410196979 ("" (skosimp*) (("" (expand "quorum?") (("" (rewrite "min_reduce") (("" (lemma "pigeonhole_difference[below(N)]") (("" (inst?) (("" (assert) (("" (inst - "lowset(v!1, enabled!1, tau!1(card(enabled!1)))") (("" (assert) (("" (prop) (("1" (expand "lowset") (("1" (skosimp*) (("1" (inst?) (("1" (prop) nil nil)) nil)) nil)) nil) ("2" (expand* "subset?" "lowset" "member") (("2" (skosimp*) nil nil)) nil) ("3" (use "card_lowset") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((quorum? const-decl "bool" pigeonhole nil) (pigeonhole_difference formula-decl nil pigeonhole 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) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (card_lowset formula-decl nil reduce_properties nil) (int_minus_int_is_int application-judgement "int" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (member const-decl "bool" sets nil) (subset? const-decl "bool" sets nil) (lowset const-decl "finite_set[below(N)]" reduce_properties nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (= const-decl "[T, T -> boolean]" equalities nil) (Card const-decl "nat" finite_sets nil) (card const-decl "{n: nat | n = Card(S)}" finite_sets nil) (vec2seq_type application-judgement "ne_seqs[T]" reduce_properties nil) (vec type-eq-decl nil node nil) (T formal-nonempty-type-decl nil reduce_properties nil) (tau_type type-eq-decl nil tau_declaration nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (empty? const-decl "bool" sets nil) (NOT const-decl "[bool -> bool]" booleans 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) (below type-eq-decl nil naturalnumbers nil) (N formal-const-decl "posnat" reduce_properties nil) (posnat 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) (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) (min_reduce formula-decl nil reduce_properties nil)) nil) (min_validity-2 nil 3410101921 ("" (skosimp*) (("" (expand "quorum?") (("" (expand "reduce") (("" (lemma "pigeonhole_difference[below(N)]") (("" (inst?) (("" (assert) (("" (typepred "filter(f!1,enabled!1)") (("" (skosimp*) (("" (inst -4 "image(map_maker(enabled!1, lower(filter(f!1, enabled!1), card(enabled!1), tau!1 (("" (prop) (("1" (skosimp*) (("1" (inst + "x!1") (("1" (assert) (("1" (expand "extend") (("1" (ground) (("1" (expand "image") (("1" (skosimp*) (("1" (inst - "x!2") (("1" (typepred "x!2") (("1" (expand "lower") (("1" (rewrite "min_index_0") (("1" (invoke (case "%1 = %2") (! -2 r) (! 1 r)) (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (expand "reduce") (("2" (expand "^") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "subset?") (("2" (expand "member") (("2" (expand "extend") (("2" (skosimp*) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (use "map_maker_bijective") (("3" (use "card_lower") (("3" (assert) (("3" (lemma "card_eq_bij[below(card(enabled!1)), below(N)]") (("3" (inst?) (("3" (inst - "extend [below(N), (image[below(card(enabled!1)), (enabled!1)] (m!1, lower[T, <=] (filter(f!1, enabled!1), card[below(N)](enabled!1), tau!1(card[below(N)](enabled!1))))), bool, FALSE] (image(map_maker(enabled!1, lower(filter(f!1, enabled!1), card(enabled!1), tau!1(card(enabled!1))), m!1), restrict [below(card[below(N)](enabled!1)), (lower[T, <=] (filter(f!1, enabled!1), card[below(N)](enabled!1), tau!1(card[below(N)](enabled!1)))), boolean] (lower(filter(f!1, enabled!1), card(enabled!1), tau!1(card(enabled!1))))))") (("3" (flatten) (("3" (hide -1) (("3" (ground) (("3" (hide 2 3) (("3" (inst + "map_maker(enabled!1, lower(filter(f!1, enabled!1), card(enabled!1), tau!1(card(enabled!1))), m!1)") (("1" (hide -1) (("1" (assert) (("1" (expand "bijective?") (("1" (flatten) (("1" (assert) (("1" (ground) (("1" (expand "injective?") (("1" (propax) nil nil)) nil) ("2" (expand "surjective?") (("2" (assert) (("2" (skosimp*) (("2" (inst - "y!1") (("2" (typepred "y!1") (("2" (expand "extend") (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "extend") (("2" (expand "image") (("2" (inst + "x1!1") (("2" (expand --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.47 Sekunden (vorverarbeitet) ¤ |
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
