|
(fseqs_def
(empty_seq_fseq 0
(empty_seq_fseq-1 nil 3410528601 ("" (judgement-tcc) nil nil)
((empty_seq const-decl "fsq" fseqs_def nil)) nil))
(emptyseq_fseq 0
(emptyseq_fseq-1 nil 3411463305 ("" (judgement-tcc) nil nil)
((empty_seq const-decl "fsq" fseqs_def nil)) nil))
(singleton_TCC1 0
(singleton_TCC1-1 nil 3473180360 ("" (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)
(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)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil))
(tofseq_TCC1 0
(tofseq_TCC1-1 nil 3506271677 ("" (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)
(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)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(real_ge_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))
nil))
(singleton_length 0
(singleton_length-1 nil 3473181682
(""
(case "NOT FORALL (fsqz: fseq): fsqz = singleton(fsqz`seq(0)) IFF fsqz`length = 1")
(("1" (hide 2)
(("1" (skeep)
(("1" (expand "singleton")
(("1" (ground)
(("1" (decompose-equality)
(("1" (decompose-equality)
(("1" (lift-if)
(("1" (ground)
(("1" (typepred "fsqz`seq")
(("1" (inst - "x!1") (("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2" (lift-if) (("2" (ground) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (skeep)
(("2" (inst - "fs")
(("2" (replace -1 :dir rl)
(("2" (hide -1)
(("2" (expand "singleton")
(("2" (expand "singleton?")
(("2" (ground)
(("1" (decompose-equality)
(("1" (skosimp*)
(("1" (expand "singleton")
(("1" (assert) nil nil)) nil))
nil)
("2" (skosimp*)
(("2" (decompose-equality)
(("2" (lift-if)
(("2" (ground)
(("2" (expand "singleton")
(("2"
(replace -1)
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (skeep)
(("3" (lift-if) (("3" (ground) nil nil)) nil))
nil))
nil)
("2" (inst + "fs`seq(0)")
(("2" (replace -1)
(("2" (hide -1)
(("2" (decompose-equality)
(("1" (expand "singleton")
(("1" (propax) nil nil)) nil)
("2" (decompose-equality)
(("2" (lift-if)
(("2"
(ground)
(("1"
(replace -1)
(("1"
(expand "singleton")
(("1" (propax) nil nil))
nil))
nil)
("2"
(expand "singleton")
(("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((fs skolem-const-decl "fseq" fseqs_def nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(posint nonempty-type-eq-decl nil integers nil)
(singleton? const-decl "bool" fseqs_def nil)
(default formal-const-decl "T" fseqs_def nil)
(fsqz skolem-const-decl "fseq" fseqs_def nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(IMPLIES 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)
(real_ge_is_total_order name-judgement "(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)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(barray type-eq-decl nil fseqs_def nil)
(fseq type-eq-decl nil fseqs_def nil)
(IFF const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(T formal-type-decl nil fseqs_def 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)
(ne_fseq type-eq-decl nil fseqs_def nil)
(singleton const-decl "ne_fseq" fseqs_def nil))
shostak))
(fseqs_eq 0
(fseqs_eq-1 nil 3481896970
("" (skeep)
(("" (ground)
(("" (decompose-equality)
(("" (decompose-equality)
(("" (typepred "fs1`seq")
(("" (typepred "fs2`seq")
(("" (case "x!1 >= fs1`length")
(("1" (inst - "x!1")
(("1" (inst - "x!1") (("1" (assert) nil nil)) nil))
nil)
("2" (hide -1)
(("2" (hide -1)
(("2" (inst - "x!1") (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((T formal-type-decl nil fseqs_def 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)
(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)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(default formal-const-decl "T" fseqs_def nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(barray type-eq-decl nil fseqs_def nil)
(fseq type-eq-decl nil fseqs_def nil))
shostak))
(fseq_length_zero 0
(fseq_length_zero-1 nil 3481897245
("" (skeep)
(("" (lemma "fseqs_eq")
(("" (inst - "fs" "emptyseq")
(("1" (assert)
(("1" (expand "empty_seq") (("1" (propax) nil nil)) nil))
nil)
("2" (skeep)
(("2" (assert)
(("2" (expand "emptyseq")
(("2" (expand "empty_seq") (("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((fseqs_eq formula-decl nil fseqs_def nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(empty_seq_fseq name-judgement "fseq" fseqs_def nil)
(fseq type-eq-decl nil fseqs_def nil)
(barray type-eq-decl nil fseqs_def nil)
(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)
(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)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(T formal-type-decl nil fseqs_def nil)
(fsq type-eq-decl nil fsq nil)
(empty_seq const-decl "fsq" fseqs_def nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(default formal-const-decl "T" fseqs_def nil))
shostak))
(oh_TCC1 0
(oh_TCC1-1 nil 3410601808 ("" (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)
(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)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(real_ge_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)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(int_minus_int_is_int application-judgement "int" integers nil))
nil))
(oh_TCC2 0
(oh_TCC2-1 nil 3410601808 ("" (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)
(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)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil))
(concat_length_add 0
(concat_length_add-1 nil 3481897577
("" (skeep) (("" (expand "o") (("" (propax) nil nil)) nil)) nil)
((O const-decl "fseq" fseqs_def nil)) shostak))
(member_composition 0
(member_composition-1 nil 3473180360
("" (skeep)
(("" (expand "member")
(("" (expand "o")
(("" (ground)
(("1" (skosimp*)
(("1" (lift-if)
(("1" (ground)
(("1" (inst + "i!1") nil nil)
("2" (inst 3 "i!1 - fs1`length") nil nil)
("3" (typepred "i!1")
(("3" (hide-all-but (-1 1))
(("3" (expand "o") (("3" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2" (inst + "i!1")
(("1" (typepred "i!1") (("1" (assert) nil nil)) nil)
("2" (typepred "i!1")
(("2" (expand "o") (("2" (assert) nil nil)) nil)) nil))
nil))
nil)
("3" (skosimp*)
(("3" (inst + "fs1`length + i!1")
(("1" (assert) nil nil)
("2" (expand "o") (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((member const-decl "bool" fseqs_def nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(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)
(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)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(barray type-eq-decl nil fseqs_def nil)
(fseq type-eq-decl nil fseqs_def nil)
(below type-eq-decl nil naturalnumbers nil)
(int_minus_int_is_int application-judgement "int" integers 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)
(fs2 skolem-const-decl "fseq" fseqs_def nil)
(i!1 skolem-const-decl "below(fs1`length)" fseqs_def nil)
(fs1 skolem-const-decl "fseq" fseqs_def nil)
(i!1 skolem-const-decl "below(fs2`length)" fseqs_def nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(O const-decl "fseq" fseqs_def nil))
shostak))
(concat_right_emptyseq 0
(concat_right_emptyseq-1 nil 3481897352
("" (skeep)
(("" (lemma "fseqs_eq")
(("" (inst?)
(("" (assert)
(("" (hide 2)
(("" (ground)
(("1" (expand "empty_seq")
(("1" (expand "o") (("1" (propax) nil nil)) nil)) nil)
("2" (skeep)
(("2" (expand "empty_seq")
(("2" (expand "o") (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((fseqs_eq formula-decl nil fseqs_def nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(empty_seq const-decl "fsq" fseqs_def nil)
(fsq type-eq-decl nil fsq nil)
(T formal-type-decl nil fseqs_def nil)
(O const-decl "fseq" fseqs_def nil)
(fseq type-eq-decl nil fseqs_def nil)
(barray type-eq-decl nil fseqs_def nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(empty_seq_fseq name-judgement "fseq" fseqs_def nil))
shostak))
(concat_left_emptyseq 0
(concat_left_emptyseq-1 nil 3481897405
("" (skeep)
(("" (lemma "fseqs_eq")
(("" (inst?)
(("" (assert)
(("" (hide 2)
(("" (ground)
(("1" (expand "empty_seq")
(("1" (expand "o") (("1" (propax) nil nil)) nil)) nil)
("2" (skeep)
(("2" (expand "empty_seq")
(("2" (expand "o") (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((fseqs_eq formula-decl nil fseqs_def nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(empty_seq const-decl "fsq" fseqs_def nil)
(fsq type-eq-decl nil fsq nil)
(T formal-type-decl nil fseqs_def nil)
(O const-decl "fseq" fseqs_def nil)
(fseq type-eq-decl nil fseqs_def nil)
(barray type-eq-decl nil fseqs_def nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(empty_seq_fseq name-judgement "fseq" fseqs_def nil))
shostak))
(member_singleton 0
(member_singleton-1 nil 3473181181
("" (skeep)
(("" (expand "member")
(("" (expand "singleton")
(("" (ground)
(("1" (skosimp*)
(("1" (typepred "i!1")
(("1" (expand "singleton") (("1" (assert) nil nil)) nil))
nil))
nil)
("2" (inst + "0") (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
((member const-decl "bool" fseqs_def nil)
(below type-eq-decl nil naturalnumbers nil)
(ne_fseq type-eq-decl nil fseqs_def nil)
(> const-decl "bool" reals nil)
(fseq type-eq-decl nil fseqs_def nil)
(barray type-eq-decl nil fseqs_def nil)
(T formal-type-decl nil fseqs_def 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_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(y skolem-const-decl "T" fseqs_def nil)
(singleton const-decl "ne_fseq" fseqs_def nil))
shostak))
(caret_TCC1 0
(caret_TCC1-1 nil 3410601808
("" (skosimp*)
(("" (expand "min") (("" (lift-if) (("" (ground) nil nil)) nil))
nil))
nil)
((real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props 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))
nil))
(caret_TCC2 0
(caret_TCC2-1 nil 3410601808 ("" (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)
(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)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(minus_odd_is_odd application-judgement "odd_int" integers 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)
(int_minus_int_is_int application-judgement "int" integers nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil))
nil))
(caret_TCC3 0
(caret_TCC3-1 nil 3411463305 ("" (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)
(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)
(nat nonempty-type-eq-decl nil naturalnumbers 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_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)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil))
nil))
(o_assoc 0
(o_assoc-1 nil 3410258465
("" (skeep)
(("" (apply-extensionality 1 :hide? t)
(("1" (grind) nil nil)
("2" (apply-extensionality 1 :hide? t) (("2" (grind) nil nil))
nil))
nil))
nil)
((nat nonempty-type-eq-decl nil naturalnumbers nil)
(barray type-eq-decl nil fseqs_def nil)
(fseq type-eq-decl nil fseqs_def nil)
(O const-decl "fseq" fseqs_def 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)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(T formal-type-decl nil fseqs_def 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))
shostak))
(fseq1_TCC1 0
(fseq1_TCC1-1 nil 3410692586 ("" (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)
(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)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(real_ge_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))
nil))
(fseq2_TCC1 0
(fseq2_TCC1-1 nil 3411463305 ("" (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)
(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)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil))
(fseq1_def 0
(fseq1_def-1 nil 3410692610 ("" (grind) nil nil)
((fseq1 const-decl "fseq" fseqs_def nil)) shostak))
(const_seq_TCC1 0
(const_seq_TCC1-1 nil 3506271677 ("" (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)
(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)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(real_ge_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))
nil))
(rev_TCC1 0
(rev_TCC1-1 nil 3411463305 ("" (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)
(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)
(nat nonempty-type-eq-decl nil naturalnumbers 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)
(int_minus_int_is_int application-judgement "int" integers nil))
nil))
(rev_TCC2 0
(rev_TCC2-1 nil 3411463305 ("" (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)
(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)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(real_ge_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))
nil)))
¤ Dauer der Verarbeitung: 0.35 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.
|
