|
(min_array_def
(ge_total 0
(ge_total-1 nil 3249306196
("" (expand ">=")
(("" (typepred "min_array_def.<=")
(("" (expand "total_order?")
(("" (flatten)
(("" (expand "partial_order?")
(("" (expand "preorder?")
(("" (prop)
(("1" (expand "reflexive?") (("1" (propax) nil)))
("2" (hide -1 -3 -4)
(("2" (expand "transitive?")
(("2" (skosimp*)
(("2" (inst -3 "z!1" "y!1" "x!1")
(("2" (assert) nil)))))))))
("3" (hide -1 -2 -4)
(("3" (expand "antisymmetric?")
(("3" (skosimp*)
(("3" (inst?) (("3" (assert) nil)))))))))
("4" (expand "dichotomous?")
(("4" (skosimp*)
(("4" (inst?)
(("4" (assert) nil))))))))))))))))))))
nil)
((<= formal-const-decl "(total_order?[T])" min_array_def nil)
(total_order? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_types nil)
(T formal-type-decl nil min_array_def nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(preorder? const-decl "bool" orders nil)
(dichotomous? const-decl "bool" orders nil)
(antisymmetric? const-decl "bool" relations nil)
(transitive? const-decl "bool" relations nil)
(reflexive? const-decl "bool" relations nil)
(partial_order? const-decl "bool" orders nil)
(>= const-decl "bool" min_array_def nil))
nil))
(IMP_max_array_def_TCC1 0
(IMP_max_array_def_TCC1-1 nil 3249306276
("" (rewrite "ge_total") nil nil)
((ge_total formula-decl nil min_array_def nil)) shostak))
(Imin_TCC1 0
(Imin_TCC1-1 nil 3249306196 ("" (subtype-tcc) nil nil) nil nil))
(Imin_TCC2 0
(Imin_TCC2-1 nil 3249306196
("" (inst 1 "(LAMBDA A,ii,(jj: abv(ii)): Imax(A,ii,jj))")
(("1" (skosimp*)
(("1" (typepred "Imax(A!1, ii!1, jj!1)")
(("1" (inst -3 "j!1")
(("1" (assert) (("1" (expand ">=") (("1" (propax) nil)))))))
("2" (rewrite "ge_total") nil)))))
("2" (skosimp*) (("2" (rewrite "ge_total") nil))))
nil)
((ge_total formula-decl nil min_array_def nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(Imax const-decl
"{i: subrange(ii, jj) | (FORALL j: ii <= j AND j <= jj IMPLIES A(j) <= A(i))}"
max_array_def nil)
(abv type-eq-decl nil max_array_def nil)
(>= const-decl "bool" min_array_def nil)
(<= formal-const-decl "(total_order?[T])" min_array_def nil)
(total_order? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_types 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)
(T formal-type-decl nil min_array_def nil)
(below type-eq-decl nil naturalnumbers nil)
(N formal-const-decl "nat" min_array_def 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))
(Imin_1_TCC1 0
(Imin_1_TCC1-1 nil 3249306196 ("" (subtype-tcc) nil nil) nil nil))
(Imin_1 0
(Imin_1-1 nil 3249306196
("" (skosimp*)
(("" (typepred "Imin(A!1, ii!1, ii!1)")
(("" (inst?) (("1" (assert) nil) ("2" (assert) nil))))))
nil)
((Imin const-decl
"{i: subrange(ii, jj) | (FORALL j: ii <= j AND j <= jj IMPLIES A(i) <= A(j))}"
min_array_def nil)
(<= formal-const-decl "(total_order?[T])" min_array_def nil)
(total_order? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_types 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)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(T formal-type-decl nil min_array_def nil)
(below type-eq-decl nil naturalnumbers nil)
(N formal-const-decl "nat" min_array_def 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)
(<= 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_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(A!1 skolem-const-decl "[below(N) -> T]" min_array_def nil)
(ii!1 skolem-const-decl "below(N)" min_array_def nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
nil)))
¤ Dauer der Verarbeitung: 0.18 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.
|
