|
(bands_1D
(vs_critical_TCC1 0
(vs_critical_TCC1-1 nil 3477649051 ("" (subtype-tcc) nil nil)
((NOT const-decl "[bool -> bool]" booleans nil)
(below type-eq-decl nil naturalnumbers 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)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(default const-decl "T" fseqs "structures/")
(empty_seq const-decl "fsq" fseqs "structures/")
(addend const-decl "fseq" fseqs_ops "structures/")
(vsmax formal-const-decl "{x: real | x > vsmin}" bands_1D nil)
(> const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(vsmin formal-const-decl "real" bands_1D nil)
(vs_fseq? const-decl "bool" fseqs_aux_vertical nil))
nil))
(vs_critical_TCC2 0
(vs_critical_TCC2-1 nil 3477649051 ("" (subtype-tcc) nil nil)
((NOT const-decl "[bool -> bool]" 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)
(default const-decl "T" fseqs "structures/")
(empty_seq const-decl "fsq" fseqs "structures/")
(emptyseq macro-decl "fsq" fseqs "structures/")
(vsmax formal-const-decl "{x: real | x > vsmin}" bands_1D nil)
(> const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(vsmin formal-const-decl "real" bands_1D nil)
(vs_fseq? const-decl "bool" fseqs_aux_vertical nil))
nil))
(vs_critical_rew 0
(vs_critical_rew-3 "" 3504831886
("" (skeep)
(("" (lift-if)
(("" (ground)
(("1" (expand "vs_critical")
(("1" (expand "addend")
(("1" (decompose-equality)
(("1" (expand "empty_seq")
(("1" (lemma "singleton_length")
(("1" (inst?)
(("1" (ground)
(("1" (expand "singleton?")
(("1" (inst + "voz") nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (decompose-equality)
(("2" (lift-if)
(("2" (ground)
(("1" (expand "empty_seq") (("1" (assert) nil nil))
nil)
("2" (expand "empty_seq")
(("2" (case "x!1 = 0")
(("1" (replace -1)
(("1" (expand "singleton")
(("1" (propax) nil nil)) nil))
nil)
("2" (assert) nil nil))
nil))
nil)
("3" (expand "empty_seq")
(("3" (expand "singleton")
(("3" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "vs_critical") (("2" (propax) nil nil)) nil)
("3" (expand "vs_critical") (("3" (propax) nil nil)) nil)
("4" (expand "vs_critical") (("4" (propax) nil nil)) nil))
nil))
nil))
nil)
((vs_critical const-decl "(vs_fseq?)" bands_1D nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(fsq type-eq-decl nil fsq "structures/")
(empty_seq const-decl "fsq" fseqs "structures/")
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(< const-decl "bool" reals nil)
(default const-decl "T" fseqs "structures/")
(barray type-eq-decl nil fseqs "structures/")
(fseq type-eq-decl nil fseqs "structures/")
(ne_fseq type-eq-decl nil fseqs "structures/")
(singleton const-decl "ne_fseq" fseqs "structures/")
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(posint 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)
(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)
(singleton_length formula-decl nil fseqs "structures/")
(singleton? const-decl "bool" fseqs "structures/")
(= const-decl "[T, T -> boolean]" equalities nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(addend const-decl "fseq" fseqs_ops "structures/")
(empty_vs_fseq name-judgement "(vs_fseq?)" bands_1D nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil))
shostak)
(vs_critical_rew-2 nil 3477649146
("" (skeep)
(("" (lift-if)
(("" (ground)
(("1" (expand "vs_critical")
(("1" (expand "addend")
(("1" (decompose-equality)
(("1" (expand "empty_seq")
(("1" (lemma "singleton_length")
(("1" (inst?)
(("1" (ground)
(("1" (replace -2) (("1" (propax) nil nil)) nil)
("2" (expand "singleton?")
(("2" (inst + "voz") nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (decompose-equality)
(("2" (lift-if)
(("2" (ground)
(("1" (expand "empty_seq") (("1" (assert) nil nil))
nil)
("2" (expand "empty_seq")
(("2" (case "x!1 = 0")
(("1" (replace -1)
(("1" (expand "singleton")
(("1" (propax) nil nil)) nil))
nil)
("2" (assert) nil nil))
nil))
nil)
("3" (expand "empty_seq")
(("3" (expand "singleton")
(("3" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "vs_critical") (("2" (propax) nil nil)) nil)
("3" (expand "vs_critical") (("3" (propax) nil nil)) nil)
("4" (expand "vs_critical") (("4" (propax) nil nil)) nil))
nil))
nil))
nil)
((fsq type-eq-decl nil fsq "structures/")
(empty_seq const-decl "fsq" fseqs "structures/")
(default const-decl "T" fseqs "structures/")
(barray type-eq-decl nil fseqs "structures/")
(fseq type-eq-decl nil fseqs "structures/")
(ne_fseq type-eq-decl nil fseqs "structures/")
(singleton const-decl "ne_fseq" fseqs "structures/")
(singleton_length formula-decl nil fseqs "structures/")
(singleton? const-decl "bool" fseqs "structures/")
(addend const-decl "fseq" fseqs_ops "structures/"))
nil)
(vs_critical_rew-1 nil 3477649118
("" (skeep)
(("" (lift-if)
(("" (ground)
(("1" (expand "trk_critical")
(("1" (expand "addend")
(("1" (decompose-equality 2)
(("1" (expand "empty_seq")
(("1" (lemma "singleton_length")
(("1" (inst?)
(("1" (ground)
(("1" (replace -2) (("1" (propax) nil)))
("2" (expand "singleton?")
(("2" (inst + "track(nvo)") nil)))))))))))
("2" (decompose-equality)
(("2" (lift-if)
(("2" (ground)
(("1" (expand "empty_seq") (("1" (assert) nil)))
("2" (expand "empty_seq")
(("2" (case "x!1 = 0")
(("1" (replace -1)
(("1" (expand "singleton")
(("1" (propax) nil)))))
("2" (assert) nil)))))
("3" (expand "empty_seq")
(("3" (expand "singleton")
(("3" (propax) nil)))))))))))))))))
("2" (expand "trk_critical") (("2" (propax) nil))))))))
nil)
nil nil))
(member_vs_critical 0
(member_vs_critical-1 nil 3477649270
("" (skeep)
(("" (split)
(("1" (flatten)
(("1" (expand "member")
(("1" (skosimp*)
(("1" (expand "vs_critical")
(("1" (lift-if)
(("1" (split -)
(("1" (flatten)
(("1" (assert)
(("1" (expand "addend")
(("1" (expand "empty_seq")
(("1" (lift-if)
(("1" (ground)
(("1"
(typepred "i!1")
(("1"
(expand "vs_critical")
(("1"
(expand "addend")
(("1"
(expand "empty_seq")
(("1" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (typepred "i!1")
(("2" (expand "vs_critical")
(("2" (expand "empty_seq")
(("2" (lift-if)
(("2" (split -)
(("1"
(flatten)
(("1"
(expand "addend")
(("1"
(typepred "i!1")
(("1" (assert) nil nil))
nil))
nil))
nil)
("2"
(flatten)
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (expand "member")
(("2" (inst + "0")
(("1" (expand "vs_critical")
(("1" (lift-if)
(("1" (split)
(("1" (flatten)
(("1" (expand "addend")
(("1" (expand "empty_seq")
(("1" (propax) nil nil)) nil))
nil))
nil)
("2" (flatten) (("2" (assert) nil nil)) nil))
nil))
nil))
nil)
("2" (expand "vs_critical")
(("2" (expand "addend")
(("2" (expand "empty_seq") (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((member const-decl "bool" fseqs "structures/")
(vs_critical const-decl "(vs_fseq?)" bands_1D nil)
(empty_vs_fseq name-judgement "(vs_fseq?)" bands_1D nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(empty_seq const-decl "fsq" fseqs "structures/")
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props 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)
(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)
(barray type-eq-decl nil fseqs "structures/")
(fseq type-eq-decl nil fseqs "structures/")
(vsmin formal-const-decl "real" bands_1D nil)
(> const-decl "bool" reals nil)
(vsmax formal-const-decl "{x: real | x > vsmin}" bands_1D nil)
(vs_fseq? const-decl "bool" fseqs_aux_vertical nil)
(below type-eq-decl nil naturalnumbers nil)
(addend const-decl "fseq" fseqs_ops "structures/")
(TF skolem-const-decl "bool" bands_1D nil)
(voz skolem-const-decl "real" bands_1D nil))
nil))
(vs_critical_composition 0
(vs_critical_composition-1 nil 3477649542
("" (skeep)
(("" (split)
(("1" (flatten)
(("1" (expand "member")
(("1" (skosimp*)
(("1" (label "xeq" -1)
(("1" (typepred "i!1")
(("1" (name "compos" "vsfs o vs_critical(TF,voz)")
(("1" (replace -1)
(("1" (label "composname" -1)
(("1" (expand "o")
(("1" (replace "composname" -3 :dir rl)
(("1" (assert)
(("1" (lift-if)
(("1"
(split "xeq")
(("1"
(flatten)
(("1" (inst + "i!1") nil nil))
nil)
("2"
(flatten)
(("2"
(replace "composname" :dir rl)
(("2"
(assert)
(("2"
(lemma "vs_critical_rew")
(("2"
(inst - "TF" "voz")
(("2"
(replace -1 -2)
(("2"
(label "rew" -1)
(("2"
(hide "rew")
(("2"
(lift-if)
(("2"
(split -1)
(("1"
(flatten)
(("1"
(lemma
"singleton_length")
(("1"
(inst?)
(("1"
(case
"singleton?(singleton(voz))")
(("1"
(assert)
(("1"
(reveal
"rew")
(("1"
(assert)
(("1"
(replace
"rew"
:dir
rl)
(("1"
(replace
-3)
(("1"
(case
"i!1 = vsfs`length")
(("1"
(replace
-1)
(("1"
(replace
"rew"
"xeq")
(("1"
(assert)
(("1"
(expand
"singleton")
(("1"
(propax)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand
"singleton?")
(("2"
(inst
+
"voz")
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(flatten)
(("2"
(expand
"vs_critical")
(("2"
(lift-if)
(("2"
(replace 1)
(("2"
(expand
"empty_seq")
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (split)
(("1" (flatten)
(("1" (expand "member")
(("1" (inst + "vsfs`length")
(("1" (expand "o")
(("1" (lemma "vs_critical_rew")
(("1" (inst - "TF" "voz")
(("1" (replace -1)
(("1" (assert)
(("1" (expand "singleton" +)
(("1" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "o")
(("2" (lemma "vs_critical_rew")
(("2" (inst - "TF" "voz")
(("2" (replace -1) (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "member")
(("2" (skosimp*)
(("2" (inst + "i!1")
(("1" (expand "o") (("1" (propax) nil nil)) nil)
("2" (expand "o") (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((member const-decl "bool" fseqs "structures/")
(comp_vs_fseq application-judgement "(vs_fseq?)" bands_1D nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(empty_seq const-decl "fsq" fseqs "structures/")
(singleton const-decl "ne_fseq" fseqs "structures/")
(ne_fseq type-eq-decl nil fseqs "structures/")
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(empty_vs_fseq name-judgement "(vs_fseq?)" bands_1D nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(singleton? const-decl "bool" fseqs "structures/")
(singleton_length formula-decl nil fseqs "structures/")
(vs_critical_rew formula-decl nil bands_1D nil)
(i!1 skolem-const-decl
"below((vsfs o vs_critical(TF, voz))`length)" bands_1D nil)
(voz skolem-const-decl "real" bands_1D nil)
(TF skolem-const-decl "bool" bands_1D nil)
(vsfs skolem-const-decl "(vs_fseq?)" bands_1D 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)
(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)
(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)
(barray type-eq-decl nil fseqs "structures/")
(fseq type-eq-decl nil fseqs "structures/")
(O const-decl "fseq" fseqs "structures/")
(vsmin formal-const-decl "real" bands_1D nil)
(> const-decl "bool" reals nil)
(vsmax formal-const-decl "{x: real | x > vsmin}" bands_1D nil)
(vs_fseq? const-decl "bool" fseqs_aux_vertical nil)
(vs_critical const-decl "(vs_fseq?)" bands_1D nil)
(below type-eq-decl nil naturalnumbers nil)
(i!1 skolem-const-decl "below(vsfs`length)" bands_1D nil))
nil))
(vs_bands_TCC1 0
(vs_bands_TCC1-2 nil 3477653957
("" (skeep)
(("" (assert)
(("" (rewrite "sort_vs_fseq")
(("" (hide-all-but 1)
(("" (rewrite "comp_vs_fseq")
(("" (hide 2)
(("" (rewrite "comp_vs_fseq")
(("1" (hide 2)
(("1" (expand "addend")
(("1" (expand "empty_seq")
(("1" (expand "vs_fseq?")
(("1" (lemma "vs_min_lt_max")
(("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (expand "addend")
(("2" (expand "empty_seq")
(("2" (expand "vs_fseq?")
(("2" (lemma "vs_min_lt_max")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((comp_vs_fseq application-judgement "(vs_fseq?)" bands_1D nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props 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)
(empty_vs_fseq name-judgement "(vs_fseq?)" bands_1D nil)
(comp_vs_fseq judgement-tcc nil fseqs_aux_vertical nil)
(vsmax formal-const-decl "{x: real | x > vsmin}" bands_1D nil)
(> const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(vsmin formal-const-decl "real" bands_1D 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)
(addend const-decl "fseq" fseqs_ops "structures/")
(T formal-const-decl "{AB: posreal | AB > B}" bands_1D nil)
(empty_seq const-decl "fsq" fseqs "structures/")
(fsq type-eq-decl nil fsq "structures/")
(sign const-decl "Sign" sign "reals/")
(vs_circle_at const-decl "[bool, real]" vertical nil)
(Sign type-eq-decl nil sign "reals/")
(= const-decl "[T, T -> boolean]" equalities nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(nzint nonempty-type-eq-decl nil integers nil)
(/= const-decl "boolean" notequal nil)
(vs_critical const-decl "(vs_fseq?)" bands_1D nil)
(B formal-const-decl "nnreal" bands_1D nil)
(nnreal type-eq-decl nil real_types nil)
(H formal-const-decl "posreal" bands_1D nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(< const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(IF const-decl "[boolean, T, T -> T]" if_def 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)
(O const-decl "fseq" fseqs "structures/")
(vs_fseq? const-decl "bool" fseqs_aux_vertical nil)
(fseq type-eq-decl nil fseqs "structures/")
(barray type-eq-decl nil fseqs "structures/")
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(sort_vs_fseq judgement-tcc nil fseqs_aux_vertical nil)
(sign_neg_clos application-judgement "Sign" sign "reals/")
(minus_odd_is_odd application-judgement "odd_int" integers nil))
nil)
(vs_bands_TCC1-1 nil 3477649051 ("" (subtype-tcc) nil nil) nil nil))
(vs_bands_not_empty 0
(vs_bands_not_empty-2 "" 3504831976
("" (skeep)
(("" (expand "vs_bands")
(("" (lift-if)
(("" (lift-if)
(("" (ground)
(("1" (expand "addend")
(("1" (expand "o") (("1" (assert) nil nil)) nil)) nil)
("2" (expand "o ")
(("2" (expand "addend") (("2" (assert) nil nil)) nil))
nil)
("3" (expand "addend")
(("3" (expand "o ") (("3" (assert) nil nil)) nil)) nil)
("4" (expand "addend")
(("4" (expand "o") (("4" (assert) nil nil)) nil)) nil)
("5" (lift-if)
(("5" (ground)
(("1" (expand "addend")
(("1" (expand "o") (("1" (assert) nil nil)) nil))
nil)
("2" (expand "addend")
(("2" (expand "o") (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((vs_bands const-decl "{fs: (vs_fseq?) | increasing?(fs)}" bands_1D
nil)
(even_plus_even_is_even application-judgement "even_int" integers
nil)
(addend const-decl "fseq" fseqs_ops "structures/")
(O const-decl "fseq" fseqs "structures/")
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(even_times_int_is_even application-judgement "even_int" integers
nil)
(nnint_times_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(sign_neg_clos application-judgement "Sign" sign "reals/")
(minus_odd_is_odd application-judgement "odd_int" integers 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)
(empty_vs_fseq name-judgement "(vs_fseq?)" bands_1D nil)
(comp_vs_fseq application-judgement "(vs_fseq?)" bands_1D nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(sort_length formula-decl nil sort_fseq "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)
(bool nonempty-type-eq-decl nil booleans nil)
(<= const-decl "bool" reals nil))
shostak)
(vs_bands_not_empty-1 nil 3481653156
("" (skeep)
(("" (expand "vs_bands")
(("" (lift-if)
(("" (lift-if)
(("" (ground)
(("1" (expand "addend")
(("1" (expand "o") (("1" (assert) nil nil)) nil)) nil)
("2" (expand "o ")
(("2" (expand "addend") (("2" (assert) nil nil)) nil))
nil)
("3" (expand "addend")
(("3" (expand "o ") (("3" (assert) nil nil)) nil)) nil)
("4" (expand "addend")
(("4" (expand "o") (("4" (assert) nil nil)) nil)) nil)
("5" (expand "addend")
(("5" (expand "o") (("5" (assert) nil nil)) nil)) nil)
("6" (expand "addend")
(("6" (expand "o") (("6" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil)
((addend const-decl "fseq" fseqs_ops "structures/")
(O const-decl "fseq" fseqs "structures/")
(sign_neg_clos application-judgement "Sign" sign "reals/")
(sort_length formula-decl nil sort_fseq "structures/"))
shostak))
(vs_bands_critical 0
(vs_bands_critical-1 nil 3477650288
("" (skeep)
(("" (expand "vs_bands")
(("" (rewrite "member_sort" :dir rl)
(("" (rewrite "member_composition")
(("" (rewrite "member_composition")
(("" (rewrite "member_composition")
(("" (split)
(("1" (flatten)
(("1" (split -)
(("1" (expand "vs_critical?")
(("1" (expand "vs_circle_at?")
(("1" (flatten)
(("1" (split -)
(("1" (flatten)
(("1"
(assert)
(("1"
(rewrite "member_composition")
(("1"
(flatten)
(("1"
(split -)
(("1"
(flatten)
(("1"
(lemma "member_vs_critical")
(("1"
(inst
-
"vs_circle_at(sz, viz, B, -1, 1)`1"
"vs_circle_at(sz, viz, B, -1, 1)`2"
"vsp")
(("1" (assert) nil nil))
nil))
nil))
nil)
("2"
(flatten)
(("2"
(lemma "member_vs_critical")
(("2"
(inst
-
"vs_circle_at(sz, viz, B, 1, 1)`1"
"vs_circle_at(sz, viz, B, 1, 1)`2"
"vsp")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (flatten)
(("2"
(assert)
(("2"
(lemma "member_vs_critical")
(("2"
(inst
-
"vs_circle_at(sz, viz, B, -sign(sz), 1)`1"
"vs_circle_at(sz, viz, B, -sign(sz), 1)`2"
"vsp")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil)
("3" (flatten)
(("3"
(assert)
(("3"
(lemma "member_vs_critical")
(("3"
(inst
-
"vs_circle_at(sz, viz, T, sign(sz), -1)`1"
"vs_circle_at(sz, viz, T, sign(sz), -1)`2"
"vsp")
(("3" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide (1 2 4))
(("2" (expand "member")
(("2" (inst + "0")
(("1" (expand "addend")
(("1" (expand "empty_seq")
(("1" (propax) nil nil)) nil))
nil)
("2" (expand "addend")
(("2" (expand "empty_seq")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
("3" (hide (1 2 3))
(("3" (expand "member")
(("3" (inst + "0")
(("1" (expand "addend")
(("1" (expand "empty_seq")
(("1" (propax) nil nil)) nil))
nil)
("2" (expand "addend")
(("2" (expand "empty_seq")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (split -)
(("1" (lift-if)
(("1" (split -)
(("1" (flatten)
(("1" (expand "vs_critical?")
(("1" (expand "vs_circle_at?")
(("1"
(assert)
(("1"
(rewrite "member_composition")
(("1"
(split -)
(("1"
(lemma "member_vs_critical")
(("1"
(inst
-
"vs_circle_at(sz, viz, B, -1, 1)`1"
"vs_circle_at(sz, viz, B, -1, 1)`2"
"vsp")
(("1"
(assert)
(("1"
(flatten)
(("1" (assert) nil nil))
nil))
nil))
nil))
nil)
("2"
(lemma "member_vs_critical")
(("2"
(inst
-
"vs_circle_at(sz, viz, B, 1, 1)`1"
"vs_circle_at(sz, viz, B, 1, 1)`2"
"vsp")
(("2"
(assert)
(("2"
(flatten)
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (split -)
(("1" (flatten)
(("1"
(expand "vs_critical?")
(("1"
(expand "vs_circle_at?")
(("1"
(assert)
(("1"
(typepred "T")
(("1"
(assert)
(("1"
(lemma "member_vs_critical")
(("1"
(inst
-
"vs_circle_at(sz, viz, B, -sign(sz), 1)`1"
"vs_circle_at(sz, viz, B, -sign(sz), 1)`2"
"vsp")
(("1"
(assert)
(("1"
(flatten)
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (flatten)
(("2"
(expand "member")
(("2"
(skosimp*)
(("2"
(typepred "i!1")
(("2"
(expand "empty_seq")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (lift-if)
(("2" (split -)
(("1" (flatten)
(("1" (expand "vs_critical?")
(("1" (expand "vs_circle_at?")
(("1"
(assert)
(("1"
(flatten)
(("1"
(lemma "member_vs_critical")
(("1"
(inst
-
"vs_circle_at(sz, viz, T, sign(sz), -1)`1"
"vs_circle_at(sz, viz, T, sign(sz), -1)`2"
"vsp")
(("1"
(assert)
(("1"
(flatten)
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (expand "member")
(("2" (skosimp*)
(("2"
(typepred "i!1")
(("2"
(expand "empty_seq")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (expand "member")
(("3" (skosimp*)
(("3" (case "i!1 = 0")
(("1" (replace -1)
(("1" (expand "addend")
(("1"
(expand "empty_seq")
(("1" (propax) nil nil))
nil))
nil))
nil)
("2" (typepred "i!1")
(("2" (expand "addend")
(("2"
(expand "empty_seq")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("4" (expand "member")
(("4" (skosimp*)
(("4" (case "i!1 = 0")
(("1" (replace -1)
(("1" (expand "addend")
(("1"
(expand "empty_seq")
(("1" (propax) nil nil))
nil))
nil))
nil)
("2" (typepred "i!1")
(("2" (expand "addend")
(("2"
(expand "empty_seq")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((vs_bands const-decl "{fs: (vs_fseq?) | increasing?(fs)}" bands_1D
nil)
(member_composition formula-decl nil fseqs "structures/")
(NOT const-decl "[bool -> bool]" booleans nil)
(below type-eq-decl nil naturalnumbers nil)
(member const-decl "bool" fseqs "structures/")
(vs_critical? const-decl "bool" vs_bands nil)
(member_vs_critical formula-decl nil bands_1D nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(vs_circle_at? const-decl "bool" vertical nil)
(comp_vs_fseq application-judgement "(vs_fseq?)" bands_1D 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)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props 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)
(addend const-decl "fseq" fseqs_ops "structures/")
(T formal-const-decl "{AB: posreal | AB > B}" bands_1D nil)
(empty_seq const-decl "fsq" fseqs "structures/")
(fsq type-eq-decl nil fsq "structures/")
(sign const-decl "Sign" sign "reals/")
(vs_circle_at const-decl "[bool, real]" vertical nil)
(Sign type-eq-decl nil sign "reals/")
(= const-decl "[T, T -> boolean]" equalities nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(nzint nonempty-type-eq-decl nil integers nil)
(/= const-decl "boolean" notequal nil)
(vs_critical const-decl "(vs_fseq?)" bands_1D nil)
(B formal-const-decl "nnreal" bands_1D nil)
(nnreal type-eq-decl nil real_types nil)
(H formal-const-decl "posreal" bands_1D nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(< const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(IF const-decl "[boolean, T, T -> T]" if_def 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)
(vs_fseq? const-decl "bool" fseqs_aux_vertical nil)
(vsmax formal-const-decl "{x: real | x > vsmin}" bands_1D nil)
(> const-decl "bool" reals nil)
(vsmin formal-const-decl "real" bands_1D nil)
(O const-decl "fseq" fseqs "structures/")
(fseq type-eq-decl nil fseqs "structures/")
(barray type-eq-decl nil fseqs "structures/")
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(member_sort formula-decl nil sort_fseq "structures/")
(empty_vs_fseq name-judgement "(vs_fseq?)" bands_1D nil)
(sign_neg_clos application-judgement "Sign" sign "reals/")
(minus_odd_is_odd application-judgement "odd_int" integers nil))
nil))
(red_vs_band?_TCC1 0
(red_vs_band?_TCC1-1 nil 3477649051 ("" (subtype-tcc) nil nil) nil
nil))
(red_vs_band?_TCC2 0
(red_vs_band?_TCC2-1 nil 3477649051 ("" (subtype-tcc) nil nil) nil
nil))
(vs_red_bands 0
(vs_red_bands-1 nil 3477650631
("" (skeep)
(("" (assert)
(("" (skeep)
(("" (ground)
(("1" (expand "red_vs_band?")
(("1"
(name "bband" "{x: real
| vs_bands(sz, viz)`seq(i) < x AND
x < vs_bands(sz, viz)`seq(1 + i)}")
(("1" (lemma "vs_red_band")
(("1" (skosimp*)
(("1"
(inst - "bband" "sz" "viz"
"(vs_bands(sz, viz)`seq(1 + i) +
vs_bands(sz, viz)`seq(i))
/ 2")
(("1" (assert)
(("1" (split -1)
(("1" (expand "vs_red?")
(("1" (inst - "x!1")
(("1" (replace -1 :dir rl)
(("1"
(typepred "x!1")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil)
("2" (expand "vs_band?")
(("2" (skosimp*)
(("2" (typepred "vsp!1")
(("2"
(replace -3 :dir rl)
(("2"
(assert)
(("2"
(flatten)
(("2"
(lemma "vs_bands_critical")
(("2"
(inst - "sz" "viz" "vsp!1")
(("1"
(assert)
(("1"
(expand "member")
(("1"
(skosimp*)
(("1"
(typepred
"vs_bands(sz,viz)")
(("1"
(expand
"increasing?")
(("1"
(case "i!1 < i")
(("1"
(inst
-
"i!1"
"i")
(("1"
(assert)
nil
nil))
nil)
("2"
(case
"i!1 > 1+i")
(("1"
(inst
-
"1+i"
"i!1")
(("1"
(assert)
nil
nil))
nil)
("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(typepred "vs_bands(sz,viz)")
(("2"
(expand "vs_fseq?")
(("2"
(inst-cp -1 "i")
(("2"
(assert)
(("2"
(flatten)
(("2"
(assert)
(("2"
(inst - "1+i")
(("2"
(flatten)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (replace -1 :dir rl) (("2" (assert) nil nil))
nil)
("3" (skosimp*)
(("3" (typepred "a!1")
(("3" (typepred "b!1")
(("3" (replace -5 :dir rl)
(("3" (assert)
(("3"
(flatten)
(("3" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "red_vs_band?")
(("2" (inst?)
(("1" (rewrite "cd_vertical") nil nil)
("2" (typepred "vs_bands(sz,viz)")
(("2" (expand "increasing?")
(("2" (inst - "i" "1+i") (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(subrange type-eq-decl nil integers nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields 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)
(vs_bands const-decl "{fs: (vs_fseq?) | increasing?(fs)}" bands_1D
nil)
(increasing? const-decl "bool" sort_fseq "structures/")
(<= const-decl "bool" reals nil)
(vs_fseq? const-decl "bool" fseqs_aux_vertical nil)
(vsmax formal-const-decl "{x: real | x > vsmin}" bands_1D nil)
(> const-decl "bool" reals nil)
(vsmin formal-const-decl "real" bands_1D nil)
(fseq type-eq-decl nil fseqs "structures/")
(barray type-eq-decl nil fseqs "structures/")
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(= const-decl "[T, T -> boolean]" equalities 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_plus_int_is_int application-judgement "int" integers nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(>= const-decl "bool" reals nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(vs_band? const-decl "bool" vs_bands nil)
(vs_bands_critical formula-decl nil bands_1D nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(below type-eq-decl nil naturalnumbers nil)
(member const-decl "bool" fseqs "structures/")
(vsp!1 skolem-const-decl "(bband)" bands_1D nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.56 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.
|
