|
(fseqs_aux_vertical
(empty_vs_fseq 0
(empty_vs_fseq-1 nil 3477413667 ("" (judgement-tcc) nil nil)
((empty_seq_fseq name-judgement "fseq[real]" fseqs_aux_vertical nil)
(vs_fseq? const-decl "bool" fseqs_aux_vertical nil)
(emptyseq macro-decl "fsq" fseqs "structures/")
(empty_seq const-decl "fsq" fseqs "structures/")
(default const-decl "T" fseqs "structures/")
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans 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))
nil))
(comp_vs_fseq 0
(comp_vs_fseq-1 nil 3477413667 ("" (judgement-tcc) nil nil)
((bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(barray type-eq-decl nil fseqs "structures/")
(fseq type-eq-decl nil fseqs "structures/")
(< 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)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(below type-eq-decl nil naturalnumbers nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers 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)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(vsb1!1 skolem-const-decl "(vs_fseq?)" fseqs_aux_vertical nil)
(vsb2!1 skolem-const-decl "(vs_fseq?)" fseqs_aux_vertical nil)
(i!1 skolem-const-decl "below(vsb1!1`length + vsb2!1`length)"
fseqs_aux_vertical 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)
(default const-decl "T" fseqs "structures/")
(O const-decl "fseq" fseqs "structures/")
(vs_fseq? const-decl "bool" fseqs_aux_vertical nil))
nil))
(sort_vs_fseq 0
(sort_vs_fseq-2 nil 3477413667
("" (skeep)
(("" (expand "vs_fseq?")
(("" (skeep)
(("" (lemma "sort_fseq_lem")
(("" (inst - "vsb")
(("" (flatten)
(("" (expand "permutation?")
(("" (skosimp*)
(("" (expand "bijective?")
(("" (flatten)
(("" (expand "surjective?")
(("" (inst - "i")
(("" (skosimp*)
(("" (inst - "x!1")
((""
(assert)
((""
(typepred "vsb")
((""
(expand "vs_fseq?")
((""
(replace -3)
((""
(inst - "x!1")
((""
(flatten)
(("" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((vs_fseq? const-decl "bool" fseqs_aux_vertical 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)
(sort_fseq_lem formula-decl nil sort_fseq "structures/")
(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) (< const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(fsq type-eq-decl nil fsq "structures/")
(increasing? const-decl "bool" sort_fseq "structures/")
(sort const-decl
"{ss: fseq | permutation?[T, <=](s, ss) AND increasing?(ss)}"
sort_fseq "structures/")
(below type-eq-decl nil naturalnumbers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(surjective? const-decl "bool" functions nil)
(bijective? const-decl "bool" functions nil)
(permutation? const-decl "bool" permutations_fseq "structures/")
(fseq type-eq-decl nil fseqs "structures/")
(barray type-eq-decl nil fseqs "structures/")
(nat nonempty-type-eq-decl nil naturalnumbers nil))
nil)
(sort_vs_fseq-1 nil 3477413667 ("" (judgement-tcc) nil nil) nil nil)))
¤ Dauer der Verarbeitung: 0.15 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.
|
