|
(well_ordered_finite
(nonempty_has_least 0
(nonempty_has_least-1 nil 3318621627
("" (skolem-typepred)
(("" (expand* "nonempty?" "empty?" "member")
(("" (skolem!)
(("" (lemma "non_empty_finite_has_least")
((""
(inst - "{t | x!1(t) AND reflexive_closure(<)(t, x!2)}"
"reflexive_closure(<)")
(("1" (expand "has_least?")
(("1" (skolem!)
(("1" (inst + "t!1")
(("1" (typepred "<")
(("1" (grind :if-match nil)
(("1" (inst -7 "r!1")
(("1" (assert) nil nil)
("2" (inst - "t!1" "r!1")
(("2" (inst - "r!1" "t!1" "x!2")
(("2" (assert) nil nil)) nil))
nil))
nil)
("2" (inst - "r!1" "x!2")
(("2" (assert)
(("2" (inst -6 "r!1")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (split)
(("1" (use "finite_below")
(("1" (expand "is_finite")
(("1" (skolem!)
(("1"
(inst + "N!1 + 1"
"LAMBDA (r: ({t | x!1(t) AND reflexive_closure[T](<)(t, x!2)})): IF r = x!2 THEN 0 ELSE f!1(r) + 1 ENDIF")
(("1" (expand "injective?")
(("1" (skosimp :preds? t)
(("1" (lift-if)
(("1" (lift-if)
(("1"
(ground)
(("1"
(lift-if)
(("1"
(split -1)
(("1"
(flatten)
(("1" (assert) nil nil))
nil)
("2"
(flatten)
(("2"
(inst - "x1!1" "x2!1")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp) (("2" (assert) nil nil)) nil)
("3" (skosimp :preds? t)
(("3"
(expand* "below" "reflexive_closure" "union"
"irreflexive_kernel" "difference" "member")
(("3" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand* "reflexive_closure" "union" "empty?" "member")
(("2" (inst - "x!2") nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((empty? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(non_empty_finite_has_least formula-decl nil minmax_orders nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(order? const-decl "bool" relations_extra nil)
(prefix? const-decl "bool" ordered_subset nil)
(below const-decl "(LAMBDA (S): prefix?(S, ord))" ordered_subset
nil)
(f!1 skolem-const-decl "[(below(x!2, <)) -> below[N!1]]"
well_ordered_finite nil)
(below type-eq-decl nil nat_types nil)
(N!1 skolem-const-decl "nat" well_ordered_finite 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)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(< const-decl "bool" reals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(injective? const-decl "bool" functions nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(irreflexive_kernel const-decl "(irreflexive?)" closure_ops nil)
(difference const-decl "set" sets nil)
(finite_below formula-decl nil well_ordered_finite nil)
(has_least? const-decl "bool" minmax_orders nil)
(least? const-decl "bool" minmax_orders nil)
(lower_bound? const-decl "bool" bounded_orders nil)
(union const-decl "set" sets nil)
(trichotomous? const-decl "bool" orders nil)
(strict_order? const-decl "bool" orders nil)
(transitive? const-decl "bool" relations nil)
(irreflexive? const-decl "bool" relations nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(r!1 skolem-const-decl "(x!1)" well_ordered_finite nil)
(total_order? const-decl "bool" orders nil)
(non_empty_finite_set type-eq-decl nil finite_sets nil)
(finite_set type-eq-decl nil finite_sets nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(is_finite const-decl "bool" finite_sets nil)
(x!1 skolem-const-decl "(nonempty?[T])" well_ordered_finite nil)
(pred type-eq-decl nil defined_types nil)
(PRED type-eq-decl nil defined_types nil)
(reflexive? const-decl "bool" relations nil)
(reflexive_closure const-decl "(reflexive?)" closure_ops nil)
(strict_total_order? const-decl "bool" orders nil)
(< formal-const-decl "(strict_total_order?[T])" well_ordered_finite
nil)
(x!2 skolem-const-decl "T" well_ordered_finite nil)
(linear_order_to_total_order application-judgement "(total_order?)"
well_ordered_finite nil)
(nonempty? const-decl "bool" sets nil)
(set type-eq-decl nil sets nil)
(T formal-type-decl nil well_ordered_finite nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
nil))
(finite_well_ordered 0
(finite_well_ordered-1 nil 3318621627
("" (expand* "well_ordered?" "well_founded?")
(("" (skosimp*)
(("" (use "nonempty_has_least")
(("1" (assert)
(("1" (typepred "least[T](reflexive_closure[T](<))(p!1)")
(("1" (inst + "least(reflexive_closure[T](<))(p!1)")
(("1" (skolem!)
(("1" (expand* "least?" "lower_bound?")
(("1" (inst - "x!1")
(("1" (expand "reflexive_closure" -2 :occurrence 1)
(("1" (expand* "union" "member")
(("1" (typepred "<")
(("1"
(expand* "strict_total_order?"
"strict_order?" "irreflexive?"
"transitive?")
(("1" (flatten)
(("1"
(inst - "x!1")
(("1"
(inst
-
"x!1"
"least(reflexive_closure[T](<))(p!1)"
"x!1")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand* "nonempty?" "empty?" "member")
(("2" (inst?) nil nil)) nil))
nil))
nil))
nil)
((empty? const-decl "bool" sets nil)
(linear_order_to_total_order application-judgement "(total_order?)"
well_ordered_finite nil)
(lower_bound? const-decl "bool" bounded_orders nil)
(irreflexive? const-decl "bool" relations nil)
(transitive? const-decl "bool" relations nil)
(strict_order? const-decl "bool" orders nil)
(union const-decl "set" sets nil)
(member const-decl "bool" sets nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(has_least? const-decl "bool" minmax_orders nil)
(least? const-decl "bool" minmax_orders nil)
(least const-decl "{t: (S) | least?(t, S, <=)}" minmax_orders nil)
(PRED type-eq-decl nil defined_types nil)
(reflexive? const-decl "bool" relations nil)
(reflexive_closure const-decl "(reflexive?)" closure_ops nil)
(strict_total_order? const-decl "bool" orders nil)
(< formal-const-decl "(strict_total_order?[T])" well_ordered_finite
nil)
(p!1 skolem-const-decl "pred[T]" well_ordered_finite nil)
(pred type-eq-decl nil defined_types nil)
(nonempty? const-decl "bool" 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 well_ordered_finite nil)
(nonempty_has_least judgement-tcc nil well_ordered_finite nil)
(well_ordered? const-decl "bool" orders nil)
(well_founded? const-decl "bool" orders nil))
nil))
(nonlast_has_next 0
(nonlast_has_next-1 nil 3318621627
("" (skolem-typepred)
(("" (typepred "<")
((""
(case "EXISTS (t: T): FORALL (r: (fullset[T])): (r < t) OR (r = t)")
(("1" (grind :if-match nil)
(("1" (typepred "greatest(union(<, =))(fullset[T])")
(("1" (expand* "greatest?" "upper_bound?" "fullset")
(("1" (inst - "x!1")
(("1" (expand "union" -1 :occurrence 1)
(("1" (expand "member")
(("1" (assert)
(("1"
(inst -7
"greatest(union(<, =))({x: T | TRUE})")
(("1" (assert) nil nil)
("2" (inst + "t!1")
(("2" (skosimp)
(("2" (inst - "r!1")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (inst + "t!1") nil nil))
nil))
nil)
("2" (inst + "x!1")
(("2" (skosimp)
(("2"
(expand* "has_next?" "above" "nonempty?" "empty?"
"irreflexive_kernel" "difference" "member"
"well_ordered?" "strict_total_order?" "trichotomous?")
(("2" (flatten)
(("2" (inst - "r!1" "x!1")
(("2" (inst - "r!1") (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((finite_well_ordered name-judgement "(well_ordered?)"
well_ordered_finite nil)
(irreflexive? const-decl "bool" relations nil)
(transitive? const-decl "bool" relations nil)
(strict_order? const-decl "bool" orders nil)
(trichotomous? const-decl "bool" orders nil)
(well_founded? const-decl "bool" orders nil)
(reflexive_closure const-decl "(reflexive?)" closure_ops nil)
(member const-decl "bool" sets nil)
(union const-decl "set" sets nil)
(upper_bound? const-decl "bool" bounded_orders nil)
(greatest? const-decl "bool" minmax_orders nil)
(has_greatest? const-decl "bool" minmax_orders nil)
(has_last? const-decl "bool" well_ordered_traversal nil)
(last const-decl
"(LAMBDA (t: T): greatest?(t, fullset[T], reflexive_closure(<)))"
well_ordered_traversal nil)
(irreflexive_kernel const-decl "(irreflexive?)" closure_ops nil)
(difference const-decl "set" sets nil)
(above const-decl "(LAMBDA (S): suffix?(S, ord))" ordered_subset
nil)
(empty? const-decl "bool" sets nil)
(nonempty? const-decl "bool" sets nil)
(has_next? const-decl "bool" well_ordered_traversal nil)
(linear_order_to_total_order application-judgement "(total_order?)"
well_ordered_finite nil)
(TRUE const-decl "bool" booleans nil)
(greatest const-decl "{t: (S) | greatest?(t, S, <=)}" minmax_orders
nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(fullset const-decl "set" sets nil)
(< formal-const-decl "(strict_total_order?[T])" well_ordered_finite
nil)
(strict_total_order? const-decl "bool" orders nil)
(nonlast const-decl "set[T]" well_ordered_traversal nil)
(set type-eq-decl nil sets nil)
(well_ordered? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_types nil)
(T formal-type-decl nil well_ordered_finite nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
nil))
(nonfirst_has_prev 0
(nonfirst_has_prev-1 nil 3318621627
("" (skolem-typepred)
(("" (use "nonempty_has_least")
(("1" (typepred "<")
(("1" (use "finite_below")
(("1" (lemma "non_empty_finite_has_greatest")
(("1" (inst - "below(x!1, <)" "reflexive_closure(<)")
(("1"
(expand* "has_greatest?" "greatest?" "upper_bound?"
"has_prev?")
(("1" (skosimp)
(("1" (inst + "t!1")
(("1" (typepred "next(<)(t!1)")
(("1" (expand* "least?" "lower_bound?")
(("1" (flatten)
(("1" (expand "below" -3)
(("1"
(expand* "above" "irreflexive_kernel"
"difference" "reflexive_closure" "union"
"member")
(("1"
(flatten)
(("1"
(inst - "x!1")
(("1"
(assert)
(("1"
(inst - "next(<)(t!1)")
(("1"
(assert)
(("1"
(expand*
"well_ordered?"
"strict_total_order?"
"strict_order?"
"irreflexive?"
"transitive?")
(("1"
(flatten)
(("1"
(inst - "t!1")
(("1"
(inst
-
"t!1"
"next(<)(t!1)"
"t!1")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand*
"below"
"irreflexive_kernel"
"difference"
"member")
nil
nil))
nil))
nil)
("2"
(expand*
"above"
"irreflexive_kernel"
"difference"
"member")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand* "has_next?" "nonempty?" "empty?"
"member" "above" "below" "irreflexive_kernel"
"difference" "member")
(("2" (flatten)
(("2" (inst - "x!1") (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert)
(("2" (rewrite "nonfirst")
(("2" (lift-if)
(("2" (expand "emptyset")
(("2" (ground)
(("2" (expand "first")
(("2"
(typepred
"least(reflexive_closure(<))(fullset[T])")
(("2"
(expand* "least?" "fullset"
"lower_bound?")
(("2"
(expand
"reflexive_closure"
-1
:occurrence
1)
(("2"
(expand* "union" "member")
(("2"
(inst - "x!1")
(("2"
(assert)
(("2"
(expand "below" -5)
(("2"
(expand*
"empty?"
"irreflexive_kernel"
"difference"
"member")
(("2"
(inst
-
"least(reflexive_closure(<))({x: T | TRUE})")
(("1" (assert) nil nil)
("2"
(expand "has_least?" +)
(("2"
(expand*
"well_ordered?"
"well_founded?")
(("2"
(flatten)
(("2"
(inst
-
"{x: T | TRUE}")
(("2"
(split)
(("1"
(skolem!)
(("1"
(inst
+
"y!1")
(("1"
(expand*
"least?"
"lower_bound?"
"reflexive_closure"
"union"
"member")
(("1"
(skosimp)
(("1"
(inst
-
"r!1")
(("1"
(expand*
"strict_total_order?"
"trichotomous?")
(("1"
(flatten)
(("1"
(inst
-
"r!1"
"y!1")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(inst + "x!1")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (grind :if-match all) nil nil))
nil))
nil)
((nonempty_has_least judgement-tcc nil well_ordered_finite nil)
(nonempty? const-decl "bool" sets nil)
(finite_well_ordered name-judgement "(well_ordered?)"
well_ordered_finite nil)
(finite_below formula-decl nil well_ordered_finite nil)
(linear_order_to_total_order application-judgement "(total_order?)"
well_ordered_finite nil)
(empty? const-decl "bool" sets nil)
(x!1 skolem-const-decl "(nonfirst(<))" well_ordered_finite nil)
(below const-decl "(LAMBDA (S): prefix?(S, ord))" ordered_subset
nil)
(prefix? const-decl "bool" ordered_subset nil)
(order? const-decl "bool" relations_extra nil)
(is_finite const-decl "bool" finite_sets nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(finite_set type-eq-decl nil finite_sets nil)
(non_empty_finite_set type-eq-decl nil finite_sets nil)
(total_order? const-decl "bool" orders nil)
(PRED type-eq-decl nil defined_types nil)
(reflexive? const-decl "bool" relations nil)
(reflexive_closure const-decl "(reflexive?)" closure_ops nil)
(least? const-decl "bool" minmax_orders nil)
(suffix? const-decl "bool" ordered_subset nil)
(above const-decl "(LAMBDA (S): suffix?(S, ord))" ordered_subset
nil)
(next const-decl
"(LAMBDA (t_1: T): least?(t_1, above(t, <), reflexive_closure(<)))"
well_ordered_traversal nil)
(irreflexive_kernel const-decl "(irreflexive?)" closure_ops nil)
(member const-decl "bool" sets nil)
(union const-decl "set" sets nil)
(difference const-decl "set" sets nil)
(irreflexive? const-decl "bool" relations nil)
(transitive? const-decl "bool" relations nil)
(strict_order? const-decl "bool" orders nil)
(lower_bound? const-decl "bool" bounded_orders nil)
(t!1 skolem-const-decl "T" well_ordered_finite nil)
(has_next? const-decl "bool" well_ordered_traversal nil)
(has_greatest? const-decl "bool" minmax_orders nil)
(upper_bound? const-decl "bool" bounded_orders nil)
(has_prev? const-decl "bool" well_ordered_traversal nil)
(greatest? const-decl "bool" minmax_orders nil)
(emptyset const-decl "set" sets nil)
(first const-decl
"(LAMBDA (t: T): least?(t, fullset[T], reflexive_closure(<)))"
well_ordered_traversal nil)
(trichotomous? const-decl "bool" orders nil)
(well_founded? const-decl "bool" orders nil)
(TRUE const-decl "bool" booleans nil)
(least const-decl "{t: (S) | least?(t, S, <=)}" minmax_orders nil)
(has_least? const-decl "bool" minmax_orders nil)
(fullset const-decl "set" sets nil)
(non_empty_finite_has_greatest formula-decl nil minmax_orders nil)
(has_first? const-decl "bool" well_ordered_traversal nil)
(finite_emptyset name-judgement "finite_set" finite_sets nil)
(finite_emptyset name-judgement "finite_set[T]" well_ordered_finite
nil)
(< formal-const-decl "(strict_total_order?[T])" well_ordered_finite
nil)
(strict_total_order? const-decl "bool" orders nil)
(nonfirst const-decl "set[T]" well_ordered_traversal nil)
(set type-eq-decl nil sets nil)
(well_ordered? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_types nil)
(T formal-type-decl nil well_ordered_finite nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
nil))
(finite_last 0
(finite_last-1 nil 3318636396
("" (typepred "<")
((""
(expand* "has_last?" "has_greatest?" "greatest?" "fullset"
"upper_bound?" "reflexive_closure" "union" "member")
(("" (skosimp*)
(("" (use "finite_below")
(("" (expand* "is_finite" "is_finite_type")
(("" (skolem!)
((""
(inst + "1 + N!1"
"LAMBDA (r: T): IF r = t!1 THEN N!1 ELSE f!1(r) ENDIF")
(("1" (expand "injective?")
(("1" (skosimp)
(("1" (lift-if)
(("1" (lift-if)
(("1" (ground)
(("1" (inst - "x1!1" "x2!1")
(("1" (assert)
(("1"
(lift-if)
(("1"
(split -1)
(("1"
(flatten)
(("1" (assert) nil nil))
nil)
("2" (flatten) nil nil))
nil))
nil))
nil)
("2" (assert)
(("2"
(lift-if)
(("2"
(split -1)
(("1"
(flatten)
(("1" (assert) nil nil))
nil)
("2"
(expand*
"below"
"irreflexive_kernel"
"difference"
"member"
"well_ordered?"
"strict_total_order?"
"trichotomous?")
(("2"
(flatten)
(("2"
(ground)
(("2"
(inst -5 "x2!1")
(("2" (ground) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp) (("2" (assert) nil nil)) nil)
("3" (skosimp)
(("3"
(expand* "below" "irreflexive_kernel" "difference"
"member" "well_ordered?" "strict_total_order?"
"trichotomous?")
(("3" (flatten)
(("3" (inst - "r!1")
(("3" (inst - "r!1" "t!1")
(("3" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((has_greatest? const-decl "bool" minmax_orders nil)
(fullset const-decl "set" sets nil)
(reflexive_closure const-decl "(reflexive?)" closure_ops nil)
(member const-decl "bool" sets nil)
(union const-decl "set" sets nil)
(upper_bound? const-decl "bool" bounded_orders nil)
(greatest? const-decl "bool" minmax_orders nil)
(has_last? const-decl "bool" well_ordered_traversal nil)
(finite_below formula-decl nil well_ordered_finite nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(injective? const-decl "bool" functions nil)
(TRUE const-decl "bool" booleans nil)
(difference const-decl "set" sets nil)
(trichotomous? const-decl "bool" orders nil)
(irreflexive_kernel const-decl "(irreflexive?)" closure_ops nil)
(x2!1 skolem-const-decl "T" well_ordered_finite nil)
(IF const-decl "[boolean, T, T -> T]" if_def 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)
(N!1 skolem-const-decl "nat" well_ordered_finite nil)
(below type-eq-decl nil nat_types nil)
(f!1 skolem-const-decl "[(below(t!1, <)) -> below[N!1]]"
well_ordered_finite nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(below const-decl "(LAMBDA (S): prefix?(S, ord))" ordered_subset
nil)
(prefix? const-decl "bool" ordered_subset nil)
(set type-eq-decl nil sets nil)
(order? const-decl "bool" relations_extra nil)
(t!1 skolem-const-decl "T" well_ordered_finite nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(is_finite const-decl "bool" finite_sets nil)
(is_finite_type const-decl "bool" finite_sets nil)
(finite_well_ordered name-judgement "(well_ordered?)"
well_ordered_finite 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 well_ordered_finite nil)
(pred type-eq-decl nil defined_types nil)
(well_ordered? const-decl "bool" orders nil)
(strict_total_order? const-decl "bool" orders nil)
(< formal-const-decl "(strict_total_order?[T])" well_ordered_finite
nil))
shostak)))
¤ Dauer der Verarbeitung: 0.76 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.
|
