|
(finite_below
(nth_TCC1 0
(nth_TCC1-1 nil 3324310156
("" (skosimp :preds? t)
(("" (use "nonempty_card[T]")
(("" (assert)
(("" (expand "nonempty?")
(("" (use "non_empty_finite_has_least") nil nil)) nil))
nil))
nil))
nil)
((nonempty_card formula-decl nil finite_sets nil)
(nonempty? const-decl "bool" sets nil)
(non_empty_finite_has_least formula-decl nil minmax_orders nil)
(reflexive_closure const-decl "(reflexive?)" closure_ops nil)
(reflexive? const-decl "bool" relations nil)
(PRED type-eq-decl nil defined_types nil)
(total_order? const-decl "bool" orders nil)
(non_empty_finite_set type-eq-decl nil finite_sets nil)
(empty? const-decl "bool" sets nil)
(S!1 skolem-const-decl "finite_set[T]" finite_below nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(reflexive_closure_preserves_transitive application-judgement
"(preorder?)" finite_below nil)
(reflexive_closure_preserves_antisymmetric application-judgement
"(antisymmetric?)" finite_below nil)
(order_to_partial_order application-judgement "(partial_order?)"
finite_below nil)
(reflexive_closure_dichotomous application-judgement
"(dichotomous?)" finite_below nil)
(linear_order_to_total_order application-judgement "(total_order?)"
finite_below nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(T formal-type-decl nil finite_below 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)
(pred type-eq-decl nil defined_types nil)
(strict_total_order? const-decl "bool" orders nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(< const-decl "bool" reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(= 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)
(below type-eq-decl nil nat_types nil))
nil))
(nth_TCC2 0
(nth_TCC2-1 nil 3324310156
("" (skosimp :preds? t)
(("" (use "nonempty_card[T]")
(("" (assert)
(("" (expand "nonempty?")
(("" (use "non_empty_finite_has_least") nil nil)) nil))
nil))
nil))
nil)
((nonempty_card formula-decl nil finite_sets nil)
(nonempty? const-decl "bool" sets nil)
(non_empty_finite_has_least formula-decl nil minmax_orders nil)
(reflexive_closure const-decl "(reflexive?)" closure_ops nil)
(reflexive? const-decl "bool" relations nil)
(PRED type-eq-decl nil defined_types nil)
(total_order? const-decl "bool" orders nil)
(non_empty_finite_set type-eq-decl nil finite_sets nil)
(empty? const-decl "bool" sets nil)
(S!1 skolem-const-decl "finite_set[T]" finite_below nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(reflexive_closure_preserves_transitive application-judgement
"(preorder?)" finite_below nil)
(reflexive_closure_preserves_antisymmetric application-judgement
"(antisymmetric?)" finite_below nil)
(order_to_partial_order application-judgement "(partial_order?)"
finite_below nil)
(reflexive_closure_dichotomous application-judgement
"(dichotomous?)" finite_below nil)
(linear_order_to_total_order application-judgement "(total_order?)"
finite_below nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(T formal-type-decl nil finite_below 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)
(pred type-eq-decl nil defined_types nil)
(strict_total_order? const-decl "bool" orders nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(< const-decl "bool" reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(= 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)
(below type-eq-decl nil nat_types nil))
nil))
(nth_TCC3 0
(nth_TCC3-1 nil 3324310156
("" (skosimp :preds? t)
(("" (use "card_remove[T]")
(("1" (lift-if) (("1" (ground) nil nil)) nil)
("2" (lemma "non_empty_finite_has_least")
(("2" (inst?)
(("2" (use "nonempty_card[T]")
(("2" (assert)
(("2" (expand "nonempty?") (("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((card_remove formula-decl nil finite_sets nil)
(least? const-decl "bool" minmax_orders nil)
(least const-decl "{t: (S) | least?(t, S, <=)}" minmax_orders nil)
(lessp!1 skolem-const-decl "(strict_total_order?[T])" finite_below
nil)
(reflexive_closure const-decl "(reflexive?)" closure_ops nil)
(reflexive? const-decl "bool" relations nil)
(PRED type-eq-decl nil defined_types nil)
(S!1 skolem-const-decl "finite_set[T]" finite_below nil)
(has_least? const-decl "bool" minmax_orders nil)
(reflexive_closure_preserves_transitive application-judgement
"(preorder?)" finite_below nil)
(reflexive_closure_preserves_antisymmetric application-judgement
"(antisymmetric?)" finite_below nil)
(order_to_partial_order application-judgement "(partial_order?)"
finite_below nil)
(reflexive_closure_dichotomous application-judgement
"(dichotomous?)" finite_below nil)
(linear_order_to_total_order application-judgement "(total_order?)"
finite_below nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(finite_remove application-judgement "finite_set[T]" finite_below
nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(total_order? const-decl "bool" orders nil)
(non_empty_finite_set type-eq-decl nil finite_sets nil)
(empty? const-decl "bool" sets nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nonempty? const-decl "bool" sets nil)
(nonempty_card formula-decl nil finite_sets nil)
(non_empty_finite_has_least formula-decl nil minmax_orders nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(T formal-type-decl nil finite_below 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)
(pred type-eq-decl nil defined_types nil)
(strict_total_order? const-decl "bool" orders nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(< const-decl "bool" reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(= 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)
(below type-eq-decl nil nat_types nil))
nil))
(nth_TCC4 0
(nth_TCC4-1 nil 3324310156 ("" (termination-tcc) nil nil) nil nil))
(nth_TCC5 0
(nth_TCC5-1 nil 3324310156
("" (skosimp :preds? t) (("" (expand* "remove" "member") nil nil))
nil)
((remove const-decl "set" sets nil)
(member const-decl "bool" sets nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(T formal-type-decl nil finite_below 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)
(pred type-eq-decl nil defined_types nil)
(strict_total_order? const-decl "bool" orders nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(< const-decl "bool" reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(= 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)
(below type-eq-decl nil nat_types nil))
nil))
(nth_one_step 0
(nth_one_step-1 nil 3324310455
("" (measure-induct+ "card(S)" ("S"))
(("" (skosimp :preds? t)
(("" (expand "nth" +)
(("" (lift-if)
(("" (prop)
(("1"
(inst -
"remove(least(reflexive_closure(lessp!1))(x!1), x!1)")
(("1" (expand "nth" +)
(("1" (assert)
(("1" (hide -4)
(("1"
(typepred
"least(reflexive_closure(lessp!1))(x!1)")
(("1" (expand* "least?" "lower_bound?")
(("1"
(inst -
"least(reflexive_closure(lessp!1))(remove(least(reflexive_closure(lessp!1))(x!1), x!1))")
(("1" (expand "reflexive_closure" -2 1)
(("1" (expand* "union" "member")
(("1"
(typepred
"least(reflexive_closure(lessp!1))(remove(least(reflexive_closure(lessp!1))(x!1), x!1))")
(("1"
(expand "remove" -1 1)
(("1"
(expand "member")
(("1" (flatten) nil nil))
nil))
nil))
nil))
nil))
nil)
("2"
(typepred
"least(reflexive_closure(lessp!1))(remove(least(reflexive_closure(lessp!1))(x!1), x!1))")
(("2" (expand "remove" -1 1)
(("2"
(expand "member")
(("2" (flatten) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(inst -
"remove(least(reflexive_closure(lessp!1))(x!1), x!1)")
(("2" (assert)
(("2" (inst - "lessp!1" "n!1 - 1")
(("2" (use "card_remove[T]") (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((NOT const-decl "[bool -> bool]" booleans nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(card_remove formula-decl nil finite_sets nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(finite_remove application-judgement "finite_set[T]" finite_below
nil)
(linear_order_to_total_order application-judgement "(total_order?)"
finite_below nil)
(reflexive_closure_dichotomous application-judgement
"(dichotomous?)" finite_below nil)
(order_to_partial_order application-judgement "(partial_order?)"
finite_below nil)
(reflexive_closure_preserves_antisymmetric application-judgement
"(antisymmetric?)" finite_below nil)
(reflexive_closure_preserves_transitive application-judgement
"(preorder?)" finite_below nil)
(reflexive_closure const-decl "(reflexive?)" closure_ops nil)
(reflexive? const-decl "bool" relations nil)
(PRED type-eq-decl nil defined_types nil)
(least const-decl "{t: (S) | least?(t, S, <=)}" minmax_orders nil)
(least? const-decl "bool" minmax_orders nil)
(has_least? const-decl "bool" minmax_orders nil)
(remove const-decl "set" sets nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(x!1 skolem-const-decl "finite_set[T]" finite_below nil)
(lessp!1 skolem-const-decl "(strict_total_order?[T])" finite_below
nil)
(member const-decl "bool" sets nil)
(union const-decl "set" sets nil)
(lower_bound? const-decl "bool" bounded_orders nil)
(nth def-decl "(S)" finite_below nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(below type-eq-decl nil nat_types nil)
(strict_total_order? const-decl "bool" orders nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(wf_nat formula-decl nil naturalnumbers nil)
(< const-decl "bool" reals 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)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(naturalnumber 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)
(finite_set type-eq-decl nil finite_sets nil)
(is_finite const-decl "bool" finite_sets nil)
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T formal-type-decl nil finite_below nil)
(measure_induction formula-decl nil measure_induction nil)
(well_founded? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_types nil))
shostak))
(nth_monotonic 0
(nth_monotonic-1 nil 3324311285
("" (skolem-typepred)
(("" (expand* "restrict" "preserves")
(("" (induct "x1" :name "below_induction[card(S!1)]")
(("1" (flatten)
(("1" (induct "x2" :name "below_induction[card(S!1)]")
(("1" (assert) nil nil)
("2" (skosimp :preds? t)
(("2" (expand "nth" -3 1)
(("2" (expand "nth" +)
(("2"
(typepred "least(reflexive_closure(lessp!1))(S!1)")
(("2" (expand* "least?" "lower_bound?")
(("2"
(inst -
"nth(remove(least(reflexive_closure(lessp!1))(S!1), S!1), lessp!1)(jb!1)")
(("1" (expand "reflexive_closure" -2 1)
(("1" (expand* "union" "member")
(("1" (assert)
(("1"
(typepred
"nth(remove(least(reflexive_closure(lessp!1))(S!1), S!1), lessp!1)(jb!1)")
(("1"
(expand "remove" -1 1)
(("1" (propax) nil nil))
nil))
nil))
nil))
nil))
nil)
("2"
(typepred
"nth(remove(least(reflexive_closure(lessp!1))(S!1), S!1), lessp!1)(jb!1)")
(("2" (expand "remove" -1 1)
(("2" (expand "member")
(("2" (flatten) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp)
(("2" (induct "x2" :name "below_induction[card(S!1)]")
(("1" (assert) nil nil)
("2" (skosimp)
(("2" (split)
(("1" (lemma "nth_one_step")
(("1" (inst - "S!1" "lessp!1" "jb!2")
(("1" (assert)
(("1"
(expand* "strict_total_order?" "strict_order?"
"transitive?")
(("1" (flatten)
(("1"
(inst - "nth(S!1, lessp!1)(1 + jb!1)"
"nth(S!1, lessp!1)(jb!2)"
"nth(S!1, lessp!1)(1 + jb!2)")
(("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (lemma "nth_one_step")
(("2" (inst - "S!1" "lessp!1" "jb!2")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil)
("3" (skosimp :preds? t) (("3" (assert) nil nil)) nil)
("4" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
((preserves const-decl "bool" functions nil)
(restrict const-decl "R" restrict nil)
(nth_one_step formula-decl nil finite_below nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(transitive? const-decl "bool" relations nil)
(strict_order? const-decl "bool" orders nil)
(jb!1 skolem-const-decl "below(card(S!1))" finite_below nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(lower_bound? const-decl "bool" bounded_orders nil)
(nnint_plus_posint_is_posint application-judgement "posint"
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)
(union const-decl "set" sets nil)
(member const-decl "bool" sets nil)
(jb!1 skolem-const-decl "below(card(S!1))" finite_below nil)
(lessp!1 skolem-const-decl "(strict_total_order?[T])" finite_below
nil)
(remove const-decl "set" sets nil)
(S!1 skolem-const-decl "finite_set[T]" finite_below nil)
(finite_remove application-judgement "finite_set[T]" finite_below
nil)
(reflexive_closure const-decl "(reflexive?)" closure_ops nil)
(reflexive? const-decl "bool" relations nil)
(PRED type-eq-decl nil defined_types nil)
(least const-decl "{t: (S) | least?(t, S, <=)}" minmax_orders nil)
(least? const-decl "bool" minmax_orders nil)
(has_least? const-decl "bool" minmax_orders nil)
(linear_order_to_total_order application-judgement "(total_order?)"
finite_below nil)
(reflexive_closure_dichotomous application-judgement
"(dichotomous?)" finite_below nil)
(order_to_partial_order application-judgement "(partial_order?)"
finite_below nil)
(reflexive_closure_preserves_antisymmetric application-judgement
"(antisymmetric?)" finite_below nil)
(reflexive_closure_preserves_transitive application-judgement
"(preorder?)" finite_below nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(below_induction formula-decl nil bounded_nat_inductions nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(= 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)
(nth def-decl "(S)" finite_below nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(below type-eq-decl nil nat_types nil)
(below type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(strict_total_order? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_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)
(T formal-type-decl nil finite_below nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
shostak))
(nth_surjective 0
(nth_surjective-1 nil 3324311589
("" (measure-induct+ "card(S)" ("S"))
(("" (skolem-typepred)
(("" (expand "surjective?")
(("" (skolem!)
(("" (case "least(reflexive_closure(lessp!1))(x!1) = y!1")
(("1" (inst + 0)
(("1" (expand "nth" +) (("1" (propax) nil nil)) nil)
("2" (use "empty_card[T]")
(("2" (assert)
(("2" (expand* "empty?" "member")
(("2" (inst - "y!1") (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (expand "nth" +)
(("2"
(inst -
"remove(least(reflexive_closure(lessp!1))(x!1), x!1)")
(("2" (inst - "lessp!1")
(("2" (use "card_remove[T]")
(("2"
(typepred
"least(reflexive_closure(lessp!1))(x!1)")
(("2" (assert)
(("2" (inst - "y!1")
(("1" (skolem-typepred)
(("1" (inst + "x!2 + 1")
(("1" (assert) nil nil)) nil))
nil)
("2" (expand* "remove" "member") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (use "non_empty_finite_has_least")
(("3" (expand* "empty?" "member")
(("3" (inst - "y!1") (("3" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((NOT const-decl "[bool -> bool]" booleans nil)
(non_empty_finite_has_least formula-decl nil minmax_orders nil)
(non_empty_finite_set type-eq-decl nil finite_sets nil)
(total_order? const-decl "bool" orders nil)
(lessp!1 skolem-const-decl "(strict_total_order?[T])" finite_below
nil)
(y!1 skolem-const-decl "(x!1)" finite_below nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(card_remove formula-decl nil finite_sets nil)
(remove const-decl "set" sets nil)
(finite_remove application-judgement "finite_set[T]" finite_below
nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(x!1 skolem-const-decl "finite_set[T]" finite_below nil)
(empty? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(empty_card formula-decl nil finite_sets nil)
(reflexive_closure const-decl "(reflexive?)" closure_ops nil)
(reflexive? const-decl "bool" relations nil)
(PRED type-eq-decl nil defined_types nil)
(least const-decl "{t: (S) | least?(t, S, <=)}" minmax_orders nil)
(least? const-decl "bool" minmax_orders nil)
(has_least? const-decl "bool" minmax_orders nil)
(linear_order_to_total_order application-judgement "(total_order?)"
finite_below nil)
(reflexive_closure_dichotomous application-judgement
"(dichotomous?)" finite_below nil)
(order_to_partial_order application-judgement "(partial_order?)"
finite_below nil)
(reflexive_closure_preserves_antisymmetric application-judgement
"(antisymmetric?)" finite_below nil)
(reflexive_closure_preserves_transitive application-judgement
"(preorder?)" finite_below nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(nth def-decl "(S)" finite_below nil)
(surjective? const-decl "bool" functions nil)
(below type-eq-decl nil nat_types nil)
(strict_total_order? const-decl "bool" orders nil)
(wf_nat formula-decl nil naturalnumbers nil)
(< const-decl "bool" reals 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)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(naturalnumber 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)
(finite_set type-eq-decl nil finite_sets nil)
(is_finite const-decl "bool" finite_sets nil)
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T formal-type-decl nil finite_below nil)
(measure_induction formula-decl nil measure_induction nil)
(well_founded? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_types nil))
shostak))
(nth_bijective 0
(nth_bijective-1 nil 3324311229
("" (skolem-typepred)
(("" (expand* "bijective?" "injective?")
(("" (use "nth_surjective")
(("" (assert)
(("" (skosimp :preds? t)
(("" (use "nth_monotonic")
(("" (expand* "restrict" "preserves")
(("" (inst-cp - "x2!1" "x1!1")
(("" (inst - "x1!1" "x2!1")
((""
(expand* "strict_total_order?" "strict_order?"
"irreflexive?")
(("" (flatten)
(("" (inst - "nth(S!1, lessp!1)(x1!1)")
(("" (ground) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((injective? const-decl "bool" functions nil)
(bijective? const-decl "bool" functions nil)
(nth_monotonic formula-decl nil finite_below nil)
(strict_order? const-decl "bool" orders nil)
(irreflexive? const-decl "bool" relations nil)
(nth def-decl "(S)" finite_below nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(restrict const-decl "R" restrict nil)
(preserves const-decl "bool" functions nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(< const-decl "bool" reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(= 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)
(below type-eq-decl nil nat_types nil)
(nth_surjective formula-decl nil finite_below 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)
(strict_total_order? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_types nil)
(T formal-type-decl nil finite_below nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
nil))
(index_TCC1 0
(index_TCC1-1 nil 3324310156
("" (skosimp)
(("" (use "empty_card")
(("" (assert)
(("" (expand* "empty?" "member")
(("" (inst - "t!1") (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil)
((empty_card formula-decl nil finite_sets nil)
(T formal-type-decl nil finite_below 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)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(member const-decl "bool" sets nil)
(empty? const-decl "bool" sets nil)
(reflexive_closure_preserves_transitive application-judgement
"(preorder?)" finite_below nil)
(reflexive_closure_preserves_antisymmetric application-judgement
"(antisymmetric?)" finite_below nil)
(order_to_partial_order application-judgement "(partial_order?)"
finite_below nil)
(reflexive_closure_dichotomous application-judgement
"(dichotomous?)" finite_below nil)
(linear_order_to_total_order application-judgement "(total_order?)"
finite_below nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
nil))
(index_TCC2 0
(index_TCC2-1 nil 3324310156
("" (skosimp)
(("" (expand* "remove" "member") (("" (assert) nil nil)) nil)) nil)
((member const-decl "bool" sets nil)
(remove const-decl "set" sets nil)
(reflexive_closure_preserves_transitive application-judgement
"(preorder?)" finite_below nil)
(reflexive_closure_preserves_antisymmetric application-judgement
"(antisymmetric?)" finite_below nil)
(order_to_partial_order application-judgement "(partial_order?)"
finite_below nil)
(reflexive_closure_dichotomous application-judgement
"(dichotomous?)" finite_below nil)
(linear_order_to_total_order application-judgement "(total_order?)"
finite_below nil))
nil))
(index_TCC3 0
(index_TCC3-1 nil 3324310156
("" (skosimp :preds? t)
(("" (use "non_empty_finite_has_least")
(("" (expand* "empty?" "member") (("" (inst?) nil nil)) nil))
nil))
nil)
((non_empty_finite_has_least formula-decl nil minmax_orders nil)
(S!1 skolem-const-decl "finite_set[T]" finite_below nil)
(reflexive_closure const-decl "(reflexive?)" closure_ops nil)
(reflexive? const-decl "bool" relations nil)
(PRED type-eq-decl nil defined_types nil)
(total_order? const-decl "bool" orders nil)
(non_empty_finite_set type-eq-decl nil finite_sets nil)
(empty? const-decl "bool" sets nil)
(reflexive_closure_preserves_transitive application-judgement
"(preorder?)" finite_below nil)
(reflexive_closure_preserves_antisymmetric application-judgement
"(antisymmetric?)" finite_below nil)
(order_to_partial_order application-judgement "(partial_order?)"
finite_below nil)
(reflexive_closure_dichotomous application-judgement
"(dichotomous?)" finite_below nil)
(linear_order_to_total_order application-judgement "(total_order?)"
finite_below nil)
(member const-decl "bool" sets nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(T formal-type-decl nil finite_below 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)
(pred type-eq-decl nil defined_types nil)
(strict_total_order? const-decl "bool" orders nil))
nil))
(index_TCC4 0
(index_TCC4-1 nil 3324310156
("" (skosimp :preds? t)
(("" (use "card_remove[T]") (("" (assert) nil nil)) nil)) nil)
((card_remove formula-decl nil finite_sets nil)
(reflexive_closure const-decl "(reflexive?)" closure_ops nil)
(reflexive? const-decl "bool" relations nil)
(PRED type-eq-decl nil defined_types nil)
(least const-decl "{t: (S) | least?(t, S, <=)}" minmax_orders nil)
(least? const-decl "bool" minmax_orders nil)
(has_least? const-decl "bool" minmax_orders nil)
(reflexive_closure_preserves_transitive application-judgement
"(preorder?)" finite_below nil)
(reflexive_closure_preserves_antisymmetric application-judgement
"(antisymmetric?)" finite_below nil)
(order_to_partial_order application-judgement "(partial_order?)"
finite_below nil)
(reflexive_closure_dichotomous application-judgement
"(dichotomous?)" finite_below nil)
(linear_order_to_total_order application-judgement "(total_order?)"
finite_below nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(finite_remove application-judgement "finite_set[T]" finite_below
nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(T formal-type-decl nil finite_below 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)
(pred type-eq-decl nil defined_types nil)
(strict_total_order? const-decl "bool" orders nil))
nil))
(index_TCC5 0
(index_TCC5-1 nil 3324310156
("" (skosimp :preds? t)
(("" (use "card_remove[T]") (("" (assert) nil nil)) nil)) nil)
((card_remove formula-decl nil finite_sets nil)
(reflexive_closure const-decl "(reflexive?)" closure_ops nil)
(reflexive? const-decl "bool" relations nil)
(PRED type-eq-decl nil defined_types nil)
(least const-decl "{t: (S) | least?(t, S, <=)}" minmax_orders nil)
(least? const-decl "bool" minmax_orders nil)
(has_least? const-decl "bool" minmax_orders nil)
(reflexive_closure_preserves_transitive application-judgement
"(preorder?)" finite_below nil)
(reflexive_closure_preserves_antisymmetric application-judgement
"(antisymmetric?)" finite_below nil)
(order_to_partial_order application-judgement "(partial_order?)"
finite_below nil)
(reflexive_closure_dichotomous application-judgement
"(dichotomous?)" finite_below nil)
(linear_order_to_total_order application-judgement "(total_order?)"
finite_below nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(finite_remove application-judgement "finite_set[T]" finite_below
nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(T formal-type-decl nil finite_below 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)
(pred type-eq-decl nil defined_types nil)
(strict_total_order? const-decl "bool" orders nil))
nil))
(index_monotonic 0
(index_monotonic-1 nil 3324312063
("" (measure-induct+ "card(S)" ("S"))
(("" (skolem-typepred)
(("" (expand* "restrict" "preserves")
(("" (skosimp)
(("" (expand "index" +)
(("" (smash)
(("1" (lemma "least_unique")
(("1"
(inst - "x!1" "reflexive_closure(lessp!1)" "x1!1"
"x2!1")
(("1"
(expand* "strict_total_order?" "strict_order?"
"irreflexive?")
(("1" (flatten)
(("1" (inst - "x1!1") (("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "least?" -4)
(("2" (expand "reflexive_closure" -4)
(("2" (expand* "lower_bound?" "union" "member")
(("2" (inst -4 "x1!1")
(("2" (assert)
(("2"
(expand* "strict_total_order?"
"strict_order?" "transitive?"
"irreflexive?")
(("2" (flatten)
(("2" (inst - "x1!1")
(("2"
(inst - "x1!1" "x2!1" "x1!1")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3"
(inst -
"remove(least(reflexive_closure(lessp!1))(x!1), x!1)")
(("3" (inst - "lessp!1")
(("3" (use "card_remove[T]")
(("3" (assert)
(("3" (inst - "x1!1" "x2!1")
(("3" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((NOT const-decl "[bool -> bool]" booleans nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(reflexive_closure_preserves_transitive application-judgement
"(preorder?)" finite_below nil)
(reflexive_closure_preserves_antisymmetric application-judgement
"(antisymmetric?)" finite_below nil)
(order_to_partial_order application-judgement "(partial_order?)"
finite_below nil)
(reflexive_closure_dichotomous application-judgement
"(dichotomous?)" finite_below nil)
(linear_order_to_total_order application-judgement "(total_order?)"
finite_below nil)
(finite_remove application-judgement "finite_set[T]" finite_below
nil)
(least? const-decl "bool" minmax_orders nil)
(reflexive_closure const-decl "(reflexive?)" closure_ops nil)
(reflexive? const-decl "bool" relations nil)
(antisymmetric? const-decl "bool" relations nil)
(irreflexive? const-decl "bool" relations nil)
(strict_order? const-decl "bool" orders nil)
(least_unique formula-decl nil minmax_orders nil)
(transitive? const-decl "bool" relations nil)
(lower_bound? const-decl "bool" bounded_orders nil)
(member const-decl "bool" sets nil)
(union const-decl "set" sets nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(card_remove formula-decl nil finite_sets nil)
(remove const-decl "set" sets nil)
(has_least? const-decl "bool" minmax_orders nil)
(least const-decl "{t: (S) | least?(t, S, <=)}" minmax_orders nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(restrict const-decl "R" restrict nil)
(index def-decl "below[card(S)]" finite_below nil)
(below type-eq-decl nil nat_types nil)
(preserves const-decl "bool" functions nil)
(PRED type-eq-decl nil defined_types nil)
(strict_total_order? const-decl "bool" orders nil)
(wf_nat formula-decl nil naturalnumbers nil)
(< const-decl "bool" reals 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)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(naturalnumber 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)
(finite_set type-eq-decl nil finite_sets nil)
(is_finite const-decl "bool" finite_sets nil)
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T formal-type-decl nil finite_below nil)
(measure_induction formula-decl nil measure_induction nil)
(well_founded? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_types nil))
shostak))
(index_nth_left_inverse 0
(index_nth_left_inverse-1 nil 3324312246
("" (measure-induct+ "card(S)" ("S"))
(("" (skolem-typepred)
(("" (expand "left_inverse?")
(("" (skolem-typepred)
(("" (expand "index" +)
(("" (lift-if)
(("" (prop)
(("1" (expand "nth" +)
(("1" (rewrite "least_def") nil nil)) nil)
("2" (expand "nth" +)
(("2" (lift-if)
(("2" (ground)
(("2"
(inst -
"remove(least(reflexive_closure(lessp!1))(x!1), x!1)")
(("2" (inst - "lessp!1")
(("2" (use "card_remove[T]")
(("2" (assert)
(("2" (inst - "d!1") nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((NOT const-decl "[bool -> bool]" booleans nil)
(finite_remove application-judgement "finite_set[T]" finite_below
nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(nth_bijective application-judgement
"(bijective?[below[card(S)], (S)])" finite_below 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)
(card_remove formula-decl nil finite_sets nil)
(remove const-decl "set" sets nil)
(least? const-decl "bool" minmax_orders nil)
(least const-decl "{t: (S) | least?(t, S, <=)}" minmax_orders nil)
(reflexive_closure_preserves_transitive application-judgement
"(preorder?)" finite_below nil)
(reflexive_closure_preserves_antisymmetric application-judgement
"(antisymmetric?)" finite_below nil)
(order_to_partial_order application-judgement "(partial_order?)"
finite_below nil)
(reflexive_closure_dichotomous application-judgement
"(dichotomous?)" finite_below nil)
(linear_order_to_total_order application-judgement "(total_order?)"
finite_below nil)
(least_def formula-decl nil minmax_orders nil)
(PRED type-eq-decl nil defined_types nil)
(antisymmetric? const-decl "bool" relations nil)
(reflexive? const-decl "bool" relations nil)
(reflexive_closure const-decl "(reflexive?)" closure_ops nil)
(has_least? const-decl "bool" minmax_orders nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(index def-decl "below[card(S)]" finite_below nil)
(nth def-decl "(S)" finite_below nil)
(left_inverse? const-decl "bool" function_inverse_def nil)
(below type-eq-decl nil nat_types nil)
(strict_total_order? const-decl "bool" orders nil)
(wf_nat formula-decl nil naturalnumbers nil)
(< const-decl "bool" reals 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)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(naturalnumber 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)
(finite_set type-eq-decl nil finite_sets nil)
(is_finite const-decl "bool" finite_sets nil)
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T formal-type-decl nil finite_below nil)
(measure_induction formula-decl nil measure_induction nil)
(well_founded? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_types nil))
shostak))
(index_nth_right_inverse 0
(index_nth_right_inverse-1 nil 3324312339
("" (measure-induct+ "card(S)" ("S"))
(("" (skolem-typepred)
(("" (expand "right_inverse?")
(("" (skolem-typepred)
(("" (expand "nth" +)
(("" (lift-if)
(("" (prop)
(("1" (expand "index" +)
(("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)
("2" (expand "index" +)
(("2" (lift-if)
(("2" (ground)
(("1" (lemma "least_unique")
(("1"
(inst - "x!1" "reflexive_closure(lessp!1)"
"least(reflexive_closure(lessp!1))(x!1)"
"nth(remove(least(reflexive_closure(lessp!1))(x!1), x!1), lessp!1)(r!1 - 1)")
(("1" (expand "least?")
(("1" (flatten)
(("1"
(typepred
"nth(remove(least(reflexive_closure(lessp!1))(x!1), x!1), lessp!1)(r!1 - 1)")
(("1"
(expand "remove" -1 1)
(("1"
(expand "member")
(("1" (flatten) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(inst -
"remove(least(reflexive_closure(lessp!1))(x!1), x!1)")
(("2" (inst - "lessp!1")
(("2" (use "card_remove[T]")
(("2" (assert)
(("2"
(inst - "r!1 - 1")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((NOT const-decl "[bool -> bool]" booleans nil)
(nth_bijective application-judgement
"(bijective?[below[card(S)], (S)])" finite_below nil)
(finite_remove application-judgement "finite_set[T]" finite_below
nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(remove const-decl "set" sets nil)
(least const-decl "{t: (S) | least?(t, S, <=)}" minmax_orders nil)
(has_least? const-decl "bool" minmax_orders nil)
(least? const-decl "bool" minmax_orders nil)
(reflexive_closure const-decl "(reflexive?)" closure_ops nil)
(reflexive? const-decl "bool" relations nil)
(antisymmetric? const-decl "bool" relations nil)
(PRED type-eq-decl nil defined_types nil)
(member const-decl "bool" sets nil)
(least_unique formula-decl nil minmax_orders nil)
(card_remove formula-decl nil finite_sets nil)
(reflexive_closure_preserves_transitive application-judgement
"(preorder?)" finite_below nil)
(reflexive_closure_preserves_antisymmetric application-judgement
"(antisymmetric?)" finite_below nil)
(order_to_partial_order application-judgement "(partial_order?)"
finite_below nil)
(reflexive_closure_dichotomous application-judgement
"(dichotomous?)" finite_below nil)
(linear_order_to_total_order application-judgement "(total_order?)"
finite_below nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(index def-decl "below[card(S)]" finite_below nil)
(nth def-decl "(S)" finite_below nil)
(right_inverse? const-decl "bool" function_inverse_def nil)
(below type-eq-decl nil nat_types nil)
(strict_total_order? const-decl "bool" orders nil)
(wf_nat formula-decl nil naturalnumbers nil)
(< const-decl "bool" reals 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)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(naturalnumber 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)
(finite_set type-eq-decl nil finite_sets nil)
(is_finite const-decl "bool" finite_sets nil)
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T formal-type-decl nil finite_below nil)
(measure_induction formula-decl nil measure_induction nil)
(well_founded? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_types nil))
shostak))
(index_bijective 0
(index_bijective-1 nil 3324311229
("" (skolem!)
(("" (use "index_nth_left_inverse")
(("" (use "index_nth_right_inverse")
(("" (forward-chain "left_right_bij[(S!1), below[card(S!1)]]")
nil nil))
nil))
nil))
nil)
((index_nth_left_inverse formula-decl nil finite_below nil)
(strict_total_order? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_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)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T formal-type-decl nil finite_below nil)
(left_right_bij formula-decl nil function_inverse_def nil)
(index def-decl "below[card(S)]" finite_below nil)
(nth def-decl "(S)" finite_below nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals 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)
(below type-eq-decl nil nat_types nil)
(index_nth_right_inverse formula-decl nil finite_below nil))
nil)))
¤ Dauer der Verarbeitung: 0.109 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.
|
