|
(min_seq
(Imin_TCC1 0
(Imin_TCC1-1 nil 3284470600 ("" (skosimp*) (("" (assert) nil)) 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))
nil))
(Imin_TCC2 0
(Imin_TCC2-1 nil 3284470600 ("" (subtype-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans 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)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(below type-eq-decl nil nat_types nil)
(T formal-nonempty-type-decl nil min_seq nil)
(finite_sequence type-eq-decl nil finite_sequences nil)
(ne_seqs type-eq-decl nil seqs 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) (dom type-eq-decl nil min_seq nil)
(<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(abv type-eq-decl nil min_seq nil)
(subrange type-eq-decl nil integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props 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_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
nil))
(Imin_TCC3 0
(Imin_TCC3-2 nil 3284470891
(""
(inst 1 "(LAMBDA ((s: ne_seqs), (ii: dom(s)), (jj:abv(ii, s))):
Imin[length(s),T,<=](seq(s),ii,jj))")
(("" (skosimp*)
(("" (typepred "Imin[length(s!1), T, <=](seq(s!1), ii!1, jj!1)")
(("" (inst?) (("1" (assert) nil nil) ("2" (assert) nil nil))
nil))
nil))
nil))
nil)
((real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(Imin const-decl
"{i: subrange(ii, jj) | (FORALL j: ii <= j AND j <= jj IMPLIES A(i) <= A(j))}"
min_array_def nil)
(abv type-eq-decl nil min_array_def nil)
(below type-eq-decl nil naturalnumbers nil)
(<= formal-const-decl "(total_order?[T])" min_seq 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_seq nil) (< const-decl "bool" reals nil)
(<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans 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)
(dom type-eq-decl nil min_seq nil)
(ne_seqs type-eq-decl nil seqs nil) (> const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans 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)
(finite_sequence type-eq-decl nil finite_sequences nil)
(T formal-nonempty-type-decl nil min_seq nil)
(below type-eq-decl nil nat_types nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil))
nil)
(Imin_TCC3-1 nil 3284470600
(""
(inst 1 "(LAMBDA ((s: seqs), (ii: dom(s)), (jj:abv(ii, s))):
Imin[length(s),T,<=](seq(s),ii,jj))")
(("" (skosimp*)
(("" (typepred "Imin[length(s!1), T, <=](seq(s!1), ii!1, jj!1)")
(("" (inst?) (("1" (assert) nil) ("2" (assert) nil))))))))
nil)
nil nil))
(Imin_seq_1_TCC1 0
(Imin_seq_1_TCC1-1 nil 3284470600 ("" (subtype-tcc) nil nil) nil
nil))
(Imin_seq_1 0
(Imin_seq_1-1 nil 3284470600
("" (skosimp*)
(("" (typepred "Imin(s!1, ii!1, ii!1)")
(("1" (inst?) (("1" (assert) nil) ("2" (assert) nil)))
("2" (skosimp*) (("2" (assert) nil))))))
nil)
((Imin const-decl "{i: subrange(ii, jj) |
(FORALL j: ii <= j AND j <= jj IMPLIES seq(s)(i) <= seq(s)(j))}"
min_seq nil)
(<= formal-const-decl "(total_order?[T])" min_seq 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_seq nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(dom type-eq-decl nil min_seq nil)
(ne_seqs type-eq-decl nil seqs nil) (> const-decl "bool" reals nil)
(finite_sequence type-eq-decl nil finite_sequences nil)
(T formal-nonempty-type-decl nil min_seq nil)
(below type-eq-decl nil nat_types 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))
nil))
(imin_TCC1 0
(imin_TCC1-1 nil 3284470600
("" (inst 1 "(LAMBDA s: Imin(s,0,length(s)-1))")
(("" (skosimp*)
(("" (typepred "Imin(s!1, 0, length(s!1) - 1)")
(("1" (assert)
(("1" (skosimp*) (("1" (inst?) (("1" (assert) nil)))))))
("2" (hide 2) (("2" (skosimp*) (("2" (assert) nil))))))))))
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 seq(s)(i) <= seq(s)(j))}"
min_seq nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(subrange type-eq-decl nil integers nil)
(abv type-eq-decl nil min_seq nil) (<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<= formal-const-decl "(total_order?[T])" min_seq nil)
(total_order? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_types nil)
(dom type-eq-decl nil min_seq nil) (< const-decl "bool" reals 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)
(ne_seqs type-eq-decl nil seqs nil) (> const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans 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)
(finite_sequence type-eq-decl nil finite_sequences nil)
(T formal-nonempty-type-decl nil min_seq nil)
(below type-eq-decl nil nat_types nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(int_minus_int_is_int application-judgement "int" integers nil))
nil))
(min_TCC1 0
(min_TCC1-1 nil 3284470600
("" (inst 1 "(LAMBDA s: seq(s)(imin(s)))")
(("" (skosimp*)
(("" (prop)
(("1" (skosimp*)
(("1" (typepred "imin(s!1)") (("1" (inst?) nil)))))
("2" (inst?) nil))))))
nil)
((NOT const-decl "[bool -> bool]" booleans nil)
(imin const-decl
"{i: dom(s) | (FORALL (ii: dom(s)): seq(s)(i) <= seq(s)(ii))}"
min_seq nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(<= formal-const-decl "(total_order?[T])" min_seq nil)
(total_order? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_types nil)
(dom type-eq-decl nil min_seq nil) (< const-decl "bool" reals 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)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(ne_seqs type-eq-decl nil seqs nil) (> const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans 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)
(finite_sequence type-eq-decl nil finite_sequences nil)
(T formal-nonempty-type-decl nil min_seq nil)
(below type-eq-decl nil nat_types nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil))
nil))
(min_seq_lem 0
(min_seq_lem-1 nil 3284470600
("" (skosimp*) (("" (typepred "min(s!1)") (("" (inst?) nil)))) nil)
((min const-decl "{t: T |
(FORALL (ii: dom(s)): t <= seq(s)(ii)) AND
(EXISTS (jj: dom(s)): seq(s)(jj) = t)}" min_seq nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<= formal-const-decl "(total_order?[T])" min_seq nil)
(total_order? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_types nil)
(dom type-eq-decl nil min_seq nil)
(ne_seqs type-eq-decl nil seqs nil) (> const-decl "bool" reals nil)
(finite_sequence type-eq-decl nil finite_sequences nil)
(T formal-nonempty-type-decl nil min_seq nil)
(below type-eq-decl nil nat_types 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_seq_in? 0
(min_seq_in?-1 nil 3284470600
("" (skosimp*)
(("" (expand "in?")
(("" (typepred "min(s!1)")
(("" (skosimp*)
(("" (hide -1) (("" (inst?) (("" (assert) nil))))))))))))
nil)
((in? const-decl "bool" seqs nil)
(below type-eq-decl nil naturalnumbers nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans 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)
(below type-eq-decl nil nat_types nil)
(T formal-nonempty-type-decl nil min_seq nil)
(finite_sequence type-eq-decl nil finite_sequences nil)
(> const-decl "bool" reals nil) (ne_seqs type-eq-decl nil seqs nil)
(dom type-eq-decl nil min_seq nil)
(pred type-eq-decl nil defined_types nil)
(total_order? const-decl "bool" orders nil)
(<= formal-const-decl "(total_order?[T])" min_seq nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(min const-decl "{t: T |
(FORALL (ii: dom(s)): t <= seq(s)(ii)) AND
(EXISTS (jj: dom(s)): seq(s)(jj) = t)}" min_seq nil))
nil))
(min_seq_def 0
(min_seq_def-1 nil 3284470600
("" (skosimp*)
(("" (prop)
(("1" (rewrite "min_seq_lem") nil)
("2" (rewrite "min_seq_in?") nil))))
nil)
((dom type-eq-decl nil min_seq nil) (< const-decl "bool" reals 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)
(ne_seqs type-eq-decl nil seqs nil) (> const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans 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)
(finite_sequence type-eq-decl nil finite_sequences nil)
(T formal-nonempty-type-decl nil min_seq nil)
(below type-eq-decl nil nat_types nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(min_seq_lem formula-decl nil min_seq nil)
(min_seq_in? formula-decl nil min_seq nil))
nil))
(min_seq_it_is 0
(min_seq_it_is-1 nil 3284470600
("" (skosimp*)
(("" (typepred "min(s!1)")
(("" (expand "in?")
(("" (skosimp*)
(("" (replace -2 * rl)
(("" (hide -2)
(("" (replace -3)
(("" (hide -3)
(("" (inst?)
(("" (inst -2 "jj!1")
(("" (typepred "<=")
(("" (expand "total_order?")
(("" (expand "partial_order?")
(("" (flatten)
((""
(expand "antisymmetric?")
((""
(inst?)
((""
(assert)
nil))))))))))))))))))))))))))))))))
nil)
((min const-decl "{t: T |
(FORALL (ii: dom(s)): t <= seq(s)(ii)) AND
(EXISTS (jj: dom(s)): seq(s)(jj) = t)}" min_seq nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<= formal-const-decl "(total_order?[T])" min_seq nil)
(total_order? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_types nil)
(dom type-eq-decl nil min_seq nil)
(ne_seqs type-eq-decl nil seqs nil) (> const-decl "bool" reals nil)
(finite_sequence type-eq-decl nil finite_sequences nil)
(T formal-nonempty-type-decl nil min_seq nil)
(below type-eq-decl nil nat_types 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)
(below type-eq-decl nil naturalnumbers nil)
(in? const-decl "bool" seqs nil))
nil))
(imin_seq_lem 0
(imin_seq_lem-1 nil 3284470600
("" (skosimp*)
(("" (typepred "imin(s!1)")
(("" (typepred "min(s!1)")
(("" (skosimp*)
(("" (replace -2 * rl)
(("" (hide -2)
(("" (inst?)
(("" (inst -3 "jj!1")
(("" (typepred "min_seq.<=")
(("" (expand "total_order?")
(("" (expand "partial_order?")
(("" (flatten)
(("" (expand "antisymmetric?")
(("" (inst?)
((""
(assert)
nil))))))))))))))))))))))))))))
nil)
((imin const-decl
"{i: dom(s) | (FORALL (ii: dom(s)): seq(s)(i) <= seq(s)(ii))}"
min_seq nil)
(<= formal-const-decl "(total_order?[T])" min_seq nil)
(total_order? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_types nil)
(dom type-eq-decl nil min_seq 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)
(ne_seqs type-eq-decl nil seqs nil) (> const-decl "bool" reals nil)
(finite_sequence type-eq-decl nil finite_sequences nil)
(T formal-nonempty-type-decl nil min_seq nil)
(below type-eq-decl nil nat_types nil)
(nat nonempty-type-eq-decl nil naturalnumbers 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: dom(s)): t <= seq(s)(ii)) AND
(EXISTS (jj: dom(s)): seq(s)(jj) = t)}" min_seq nil))
nil))
(imin_seq_1 0
(imin_seq_1-1 nil 3284470600
("" (skosimp*) (("" (typepred "imin(s!1)") (("" (assert) nil))))
nil)
((imin const-decl
"{i: dom(s) | (FORALL (ii: dom(s)): seq(s)(i) <= seq(s)(ii))}"
min_seq nil)
(<= formal-const-decl "(total_order?[T])" min_seq nil)
(total_order? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_types nil)
(dom type-eq-decl nil min_seq 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)
(ne_seqs type-eq-decl nil seqs nil) (> const-decl "bool" reals nil)
(finite_sequence type-eq-decl nil finite_sequences nil)
(T formal-nonempty-type-decl nil min_seq nil)
(below type-eq-decl nil nat_types nil)
(nat nonempty-type-eq-decl nil naturalnumbers 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_seq_2_TCC1 0
(min_seq_2_TCC1-1 nil 3284470600 ("" (subtype-tcc) nil nil) nil nil))
(min_seq_2_TCC2 0
(min_seq_2_TCC2-1 nil 3284470600 ("" (subtype-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans 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)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(below type-eq-decl nil nat_types nil)
(T formal-nonempty-type-decl nil min_seq nil)
(finite_sequence type-eq-decl nil finite_sequences nil)
(ne_seqs type-eq-decl nil seqs 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))
nil))
(min_seq_2 0
(min_seq_2-1 nil 3284470600
("" (skosimp*)
(("" (typepred "min(s!1)")
(("" (skosimp*)
(("" (replace -2 * rl)
(("" (hide -2)
(("" (inst-cp -1 "0")
(("" (inst -1 "1")
(("1" (lift-if)
(("1" (ground)
(("1" (typepred "jj!1")
(("1" (case-replace "jj!1 = 0 OR jj!1 = 1")
(("1" (prop)
(("1" (assert) nil)
("2" (replace -1)
(("2" (hide -1)
(("2"
(typepred "min_seq.<=")
(("2"
(expand "total_order?")
(("2"
(expand "partial_order?")
(("2"
(flatten)
(("2"
(expand "antisymmetric?")
(("2"
(inst?)
(("2"
(assert)
nil)))))))))))))))))))
("2" (assert) nil)))))))))
("2" (assert) nil))))))))))))))
nil)
((min const-decl "{t: T |
(FORALL (ii: dom(s)): t <= seq(s)(ii)) AND
(EXISTS (jj: dom(s)): seq(s)(jj) = t)}" min_seq nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<= formal-const-decl "(total_order?[T])" min_seq nil)
(total_order? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_types nil)
(dom type-eq-decl nil min_seq nil)
(ne_seqs type-eq-decl nil seqs nil) (> const-decl "bool" reals nil)
(finite_sequence type-eq-decl nil finite_sequences nil)
(T formal-nonempty-type-decl nil min_seq nil)
(below type-eq-decl nil nat_types 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)
(s!1 skolem-const-decl "ne_seqs[T]" min_seq nil))
nil)))
¤ Dauer der Verarbeitung: 0.32 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
