|
(fseqs
(default_TCC1 0
(default_TCC1-1 nil 3506271677 ("" (subtype-tcc) nil nil)
((member const-decl "bool" sets nil)
(empty? const-decl "bool" sets nil)
(nonempty? const-decl "bool" sets nil))
nil))
(empty_seq_fseq 0
(empty_seq_fseq-1 nil 3410528601 ("" (judgement-tcc) nil nil)
((default const-decl "T" fseqs nil)
(empty_seq const-decl "fsq" fseqs nil))
nil))
(emptyseq_fseq 0
(emptyseq_fseq-1 nil 3411463305 ("" (judgement-tcc) nil nil)
((default const-decl "T" fseqs nil)
(empty_seq const-decl "fsq" fseqs 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)
(default const-decl "T" fseqs 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)
(default const-decl "T" fseqs 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 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 nil)
(default const-decl "T" fseqs nil)
(fsqz skolem-const-decl "fseq" fseqs 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 nil)
(fseq type-eq-decl nil fseqs nil)
(IFF const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(T formal-nonempty-type-decl nil fseqs 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 nil)
(singleton const-decl "ne_fseq" fseqs 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-nonempty-type-decl nil fseqs 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 const-decl "T" fseqs nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(barray type-eq-decl nil fseqs nil)
(fseq type-eq-decl nil fseqs 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 nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(empty_seq_fseq name-judgement "fseq" fseqs nil)
(fseq type-eq-decl nil fseqs nil)
(barray type-eq-decl nil fseqs 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-nonempty-type-decl nil fseqs nil)
(fsq type-eq-decl nil fsq nil)
(empty_seq const-decl "fsq" fseqs nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(default const-decl "T" fseqs 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)
(default const-decl "T" fseqs 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 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 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 nil)
(fseq type-eq-decl nil fseqs 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 nil)
(i!1 skolem-const-decl "below(fs1`length)" fseqs nil)
(fs1 skolem-const-decl "fseq" fseqs nil)
(i!1 skolem-const-decl "below(fs2`length)" fseqs nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(O const-decl "fseq" fseqs 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 nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(empty_seq const-decl "fsq" fseqs nil)
(fsq type-eq-decl nil fsq nil)
(T formal-nonempty-type-decl nil fseqs nil)
(O const-decl "fseq" fseqs nil) (fseq type-eq-decl nil fseqs nil)
(barray type-eq-decl nil fseqs nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(empty_seq_fseq name-judgement "fseq" fseqs 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 nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(empty_seq const-decl "fsq" fseqs nil)
(fsq type-eq-decl nil fsq nil)
(T formal-nonempty-type-decl nil fseqs nil)
(O const-decl "fseq" fseqs nil) (fseq type-eq-decl nil fseqs nil)
(barray type-eq-decl nil fseqs nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(empty_seq_fseq name-judgement "fseq" fseqs 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 nil)
(below type-eq-decl nil naturalnumbers nil)
(ne_fseq type-eq-decl nil fseqs nil)
(> const-decl "bool" reals nil) (fseq type-eq-decl nil fseqs nil)
(barray type-eq-decl nil fseqs nil)
(T formal-nonempty-type-decl nil fseqs 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 nil)
(singleton const-decl "ne_fseq" fseqs 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)
(default const-decl "T" fseqs 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 nil)
(fseq type-eq-decl nil fseqs nil) (O const-decl "fseq" fseqs nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(default const-decl "T" fseqs 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-nonempty-type-decl nil fseqs 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)
(default const-decl "T" fseqs 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)
(default const-decl "T" fseqs nil))
nil))
(fseq1_def 0
(fseq1_def-1 nil 3410692610 ("" (grind) nil nil)
((default const-decl "T" fseqs nil)
(fseq1 const-decl "fseq" fseqs 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)
(default const-decl "T" fseqs 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)
(default const-decl "T" fseqs nil))
nil)))
¤ Dauer der Verarbeitung: 0.40 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.
|
