(min_array
(imin_TCC1 0
(imin_TCC1-1 nil 3281095831
("" (inst 1 "(LAMBDA A: Imin(A,0,N-1))")
(("1" (skosimp*)
(("1" (typepred "Imin(A!1, 0, N - 1)")
(("1" (prop)
(("1" (inst?)
(("1" (assert) nil nil) ("2" (assert) nil nil)
("3" (assert) nil nil))
nil)
("2" (assert) nil nil)
("3" (inst?)
(("1" (assert)
(("1" (assert)
(("1" (skosimp*)
(("1" (assert)
(("1" (typepred "Imin(A!1, 0, N - 1)")
(("1" (inst?) (("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp*) (("2" (assert) nil nil)) nil)
("3" (assert) nil nil))
nil))
nil)
("2" (assert) nil nil) ("3" (assert) nil nil))
nil))
nil)
("2" (skosimp*) (("2" (assert) nil nil)) nil)
("3" (skosimp*) (("3" (assert) nil nil)) nil))
nil)
((A!1 skolem-const-decl "[below(N) -> T]" min_array nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(Imin const-decl
"{i: subrange(ii, jj) | (FORALL j: ii <= j AND j <= jj IMPLIES A(i) <= A(j))}"
min_array_def nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(subrange type-eq-decl nil integers nil)
(abv type-eq-decl nil min_array_def nil)
(<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<= formal-const-decl "(total_order?[T])" min_array nil)
(total_order? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_types nil)
(T formal-type-decl nil min_array nil)
(below type-eq-decl nil naturalnumbers nil)
(N formal-const-decl "posnat" min_array 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)
(int_minus_int_is_int application-judgement "int" integers nil))
nil))
(min_TCC1 0
(min_TCC1-1 nil 3281095831
("" (inst 1 "(LAMBDA A: A(imin(A)))")
(("" (skosimp*)
(("" (prop)
(("1" (skosimp*)
(("1" (typepred "imin(A!1)") (("1" (inst?) nil)))))
("2" (inst?) nil))))))
nil)
((NOT const-decl "[bool -> bool]" booleans nil)
(imin const-decl "{i: below(N) | (FORALL ii: A(i) <= A(ii))}"
min_array nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(<= formal-const-decl "(total_order?[T])" min_array nil)
(total_order? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_types nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(T formal-type-decl nil min_array nil)
(below type-eq-decl nil naturalnumbers nil)
(N formal-const-decl "posnat" min_array 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))
nil))
(min_lem 0
(min_lem-1 nil 3281095831
("" (skosimp*) (("" (typepred "min(A!1)") (("" (inst?) nil)))) nil)
((min const-decl
"{t: T | (FORALL ii: t <= A(ii)) AND (EXISTS jj: A(jj) = t)}"
min_array nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<= formal-const-decl "(total_order?[T])" min_array nil)
(total_order? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_types nil)
(T formal-type-decl nil min_array nil)
(below type-eq-decl nil naturalnumbers nil)
(N formal-const-decl "posnat" min_array 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))
nil))
(min_in? 0
(min_in?-1 nil 3281095831
("" (skosimp*)
(("" (typepred "min(A!1)")
(("" (skosimp*)
(("" (expand "in?")
(("" (hide -1) (("" (inst?) (("" (assert) nil))))))))))))
nil)
((min const-decl
"{t: T | (FORALL ii: t <= A(ii)) AND (EXISTS jj: A(jj) = t)}"
min_array nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<= formal-const-decl "(total_order?[T])" min_array nil)
(total_order? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_types nil)
(T formal-type-decl nil min_array nil)
(below type-eq-decl nil naturalnumbers nil)
(N formal-const-decl "posnat" min_array 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)
(in? const-decl "bool" below_arrays nil))
nil))
(min_def 0
(min_def-1 nil 3281095831
("" (skosimp*)
(("" (typepred "min(A!1)")
(("" (skosimp*)
(("" (inst?)
(("" (assert) (("" (hide -1) (("" (grind) nil))))))))))))
nil)
((min const-decl
"{t: T | (FORALL ii: t <= A(ii)) AND (EXISTS jj: A(jj) = t)}"
min_array nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<= formal-const-decl "(total_order?[T])" min_array nil)
(total_order? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_types nil)
(T formal-type-decl nil min_array nil)
(below type-eq-decl nil naturalnumbers nil)
(N formal-const-decl "posnat" min_array 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)
(in? const-decl "bool" below_arrays nil))
nil))
(min_it_is 0
(min_it_is-1 nil 3281095831
("" (skosimp*)
(("" (expand "in?")
(("" (skosimp*)
(("" (replace -2)
(("" (hide -2)
(("" (typepred "min(A!1)")
(("" (skosimp*)
(("" (replace -2 * rl)
(("" (hide -2)
(("" (inst?)
(("" (inst?)
(("" (assert)
(("" (typepred "<=")
(("" (expand "total_order?")
((""
(expand "partial_order?")
((""
(flatten)
((""
(expand "antisymmetric?")
((""
(inst?)
((""
(assert)
nil))))))))))))))))))))))))))))))))))))
nil)
((in? const-decl "bool" below_arrays nil)
(min const-decl
"{t: T | (FORALL ii: t <= A(ii)) AND (EXISTS jj: A(jj) = t)}"
min_array nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<= formal-const-decl "(total_order?[T])" min_array nil)
(total_order? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_types nil)
(T formal-type-decl nil min_array nil)
(below type-eq-decl nil naturalnumbers nil)
(N formal-const-decl "posnat" min_array 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)
(antisymmetric? const-decl "bool" relations nil)
(partial_order? const-decl "bool" orders nil))
nil))
(imin_lem 0
(imin_lem-1 nil 3281095831
("" (skosimp*)
(("" (typepred "imin(A!1)")
(("" (typepred "min(A!1)")
(("" (skosimp*)
(("" (replace -2 * rl)
(("" (hide -2)
(("" (inst?)
(("" (inst -3 "jj!1")
(("" (typepred "min_array.<=")
(("" (expand "total_order?")
(("" (expand "partial_order?")
(("" (flatten)
(("" (expand "antisymmetric?")
(("" (inst?)
((""
(assert)
nil))))))))))))))))))))))))))))
nil)
((imin const-decl "{i: below(N) | (FORALL ii: A(i) <= A(ii))}"
min_array nil)
(<= formal-const-decl "(total_order?[T])" min_array nil)
(total_order? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_types nil)
(T formal-type-decl nil min_array nil)
(below type-eq-decl nil naturalnumbers nil)
(N formal-const-decl "posnat" min_array nil)
(posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(nonneg_int 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)
(< 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)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(antisymmetric? const-decl "bool" relations nil)
(partial_order? const-decl "bool" orders nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(min const-decl
"{t: T | (FORALL ii: t <= A(ii)) AND (EXISTS jj: A(jj) = t)}"
min_array nil))
nil))
(imin_1 0
(imin_1-1 nil 3281095831
("" (skosimp*) (("" (typepred "imin(A!1)") (("" (assert) nil))))
nil)
((imin const-decl "{i: below(N) | (FORALL ii: A(i) <= A(ii))}"
min_array nil)
(<= formal-const-decl "(total_order?[T])" min_array nil)
(total_order? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_types nil)
(T formal-type-decl nil min_array nil)
(below type-eq-decl nil naturalnumbers nil)
(N formal-const-decl "posnat" min_array nil)
(posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(nonneg_int 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)
(< 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)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
nil))
(min_2_TCC1 0
(min_2_TCC1-1 nil 3281095831 ("" (subtype-tcc) nil nil)
((real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
nil))
(min_2_TCC2 0
(min_2_TCC2-1 nil 3281095831 ("" (subtype-tcc) nil nil)
((real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
nil))
(min_2 0
(min_2-1 nil 3281095831
("" (skosimp*)
(("" (typepred "min(A!1)")
(("" (skosimp*)
(("" (replace -2 * rl)
(("" (case "jj!1 = 0 OR jj!1 = 1")
(("1" (split -1)
(("1" (replace -1)
(("1" (hide -1)
(("1" (lift-if)
(("1" (inst -1 "1")
(("1" (ground) nil) ("2" (assert) nil)))))))))
("2" (replace -1)
(("2" (hide -1)
(("2" (inst -1 "0")
(("2" (lift-if)
(("2" (ground)
(("2" (hide -3 -4)
(("2" (typepred "min_array.<=")
(("2" (expand "total_order?")
(("2"
(expand "partial_order?")
(("2"
(flatten)
(("2"
(hide -1 -3)
(("2"
(expand "antisymmetric?")
(("2"
(inst?)
(("2"
(assert)
nil)))))))))))))))))))))))))))))
("2" (hide 2 -1 -2)
(("2" (typepred "jj!1")
(("2" (replace -2) (("2" (ground) nil))))))))))))))))
nil)
((min const-decl
"{t: T | (FORALL ii: t <= A(ii)) AND (EXISTS jj: A(jj) = t)}"
min_array nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<= formal-const-decl "(total_order?[T])" min_array nil)
(total_order? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_types nil)
(T formal-type-decl nil min_array nil)
(below type-eq-decl nil naturalnumbers nil)
(N formal-const-decl "posnat" min_array 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)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(antisymmetric? const-decl "bool" relations nil)
(partial_order? const-decl "bool" orders nil)
(OR const-decl "[bool, bool -> bool]" booleans nil))
nil)))
¤ Dauer der Verarbeitung: 0.14 Sekunden
(vorverarbeitet)
¤
*© Formatika GbR, Deutschland
|
|
