|
(fseqs_aux_2D
(empty_trk_fseq 0
(empty_trk_fseq-1 nil 3477413547 ("" (judgement-tcc) nil nil)
((empty_seq_fseq name-judgement "fseq[real]" fseqs_aux_2D nil)
(trk_fseq? const-decl "bool" fseqs_aux_2D nil)
(pi const-decl "posreal" atan "trig_fnd/")
(atan_value const-decl "real" atan "trig_fnd/")
(Integral const-decl "real" integral_def "analysis/")
(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_trk_fseq 0
(comp_trk_fseq-1 nil 3477413547 ("" (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_times_real_is_real application-judgement "real" reals 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)
(trkb1!1 skolem-const-decl "(trk_fseq?)" fseqs_aux_2D nil)
(trkb2!1 skolem-const-decl "(trk_fseq?)" fseqs_aux_2D nil)
(i!1 skolem-const-decl "below(trkb1!1`length + trkb2!1`length)"
fseqs_aux_2D 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/")
(Integral const-decl "real" integral_def "analysis/")
(atan_value const-decl "real" atan "trig_fnd/")
(pi const-decl "posreal" atan "trig_fnd/")
(trk_fseq? const-decl "bool" fseqs_aux_2D nil))
nil))
(sort_trk_fseq 0
(sort_trk_fseq-2 nil 3477413547
("" (skeep)
(("" (expand "trk_fseq?")
(("" (skeep)
(("" (lemma "sort_fseq_lem")
(("" (inst - "trkb")
(("" (flatten)
(("" (expand "permutation?")
(("" (skosimp*)
(("" (expand "bijective?")
(("" (flatten)
(("" (expand "surjective?")
(("" (inst - "i")
(("" (skosimp*)
(("" (inst - "x!1")
((""
(typepred "trkb")
((""
(expand "trk_fseq?")
((""
(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)
((pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx "trig_fnd/")
(trk_fseq? const-decl "bool" fseqs_aux_2D 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)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(NOT const-decl "[bool -> bool]" booleans 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_trk_fseq-1 nil 3477413547 ("" (judgement-tcc) nil nil) nil
nil))
(empty_gs_fseq 0
(empty_gs_fseq-1 nil 3477413547 ("" (judgement-tcc) nil nil)
((empty_trk_fseq name-judgement "(trk_fseq?)" fseqs_aux_2D nil)
(gs_fseq? const-decl "bool" fseqs_aux_2D 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_gs_fseq 0
(comp_gs_fseq-1 nil 3477413547 ("" (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)
(gsb1!1 skolem-const-decl "(gs_fseq?)" fseqs_aux_2D nil)
(gsb2!1 skolem-const-decl "(gs_fseq?)" fseqs_aux_2D nil)
(i!1 skolem-const-decl "below(gsb1!1`length + gsb2!1`length)"
fseqs_aux_2D 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/")
(gs_fseq? const-decl "bool" fseqs_aux_2D nil))
nil))
(sort_gs_fseq 0
(sort_gs_fseq-2 nil 3477413585
("" (skeep)
(("" (expand "gs_fseq?")
(("" (skeep)
(("" (lemma "sort_fseq_lem")
(("" (inst - "gsb")
(("" (flatten)
(("" (expand "permutation?")
(("" (skosimp*)
(("" (expand "bijective?")
(("" (flatten)
(("" (expand "surjective?")
(("" (inst - "i")
(("" (skosimp*)
(("" (inst - "x!1")
((""
(assert)
((""
(typepred "gsb")
((""
(expand "gs_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)
((gs_fseq? const-decl "bool" fseqs_aux_2D 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_gs_fseq-1 nil 3477413547 ("" (judgement-tcc) nil nil) nil nil)))
¤ Dauer der Verarbeitung: 0.20 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
