|
(csequence_generate
(generate_TCC1 0
(generate_TCC1-1 nil 3513557144
(""
(case "FORALL (x: nat, f: [T -> T], t: T): NOT has_length(coreduce[T, [[T -> T], T]](generate_struct)(f, t), x)")
(("1" (skolem!)
(("1" (rewrite "is_finite_def")
(("1" (skolem!) (("1" (inst - "n!1" "f!1" "t!1") nil nil))
nil))
nil))
nil)
("2" (delete 2)
(("2" (induct "x")
(("1" (skolem!)
(("1" (expand* "has_length" "generate_struct" "coreduce") nil
nil))
nil)
("2" (skosimp*)
(("2" (inst - "f!1" "f!1(t!1)")
(("2" (expand "generate_struct")
(("2" (expand "coreduce" -)
(("2" (expand "has_length" -) (("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((nat_induction formula-decl nil naturalnumbers nil)
(pred type-eq-decl nil defined_types nil)
(is_finite_def formula-decl nil csequence_props 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)
(T formal-type-decl nil csequence_generate nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(csequence type-decl nil csequence_codt nil)
(has_length def-decl "bool" csequence_props nil)
(csequence_struct type-decl nil csequence_codt_coreduce nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(inj_empty? adt-recognizer-decl "[csequence_struct -> boolean]"
csequence_codt_coreduce nil)
(empty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt
nil)
(inj_nonempty? adt-recognizer-decl "[csequence_struct -> boolean]"
csequence_codt_coreduce nil)
(nonempty? adt-recognizer-decl "[csequence -> boolean]"
csequence_codt nil)
(coreduce adt-def-decl "{c: csequence[T] |
inj_empty?(op(x)) AND empty?(c) OR
inj_nonempty?(op(x)) AND nonempty?(c)}"
csequence_codt_coreduce nil)
(generate_struct const-decl "csequence_struct" csequence_generate
nil))
nil))
(generate_first 0
(generate_first-1 nil 3513557263
("" (expand* "generate" "generate_struct" "coreduce") nil nil)
((coreduce adt-def-decl "{c: csequence[T] |
inj_empty?(op(x)) AND empty?(c) OR
inj_nonempty?(op(x)) AND nonempty?(c)}"
csequence_codt_coreduce nil)
(generate_struct const-decl "csequence_struct" csequence_generate
nil)
(generate const-decl "infinite_csequence" csequence_generate nil))
shostak))
(generate_rest 0
(generate_rest-1 nil 3513557286
("" (expand* "generate" "generate_struct")
(("" (expand "coreduce" 1 1) (("" (propax) nil nil)) nil)) nil)
((coreduce adt-def-decl "{c: csequence[T] |
inj_empty?(op(x)) AND empty?(c) OR
inj_nonempty?(op(x)) AND nonempty?(c)}"
csequence_codt_coreduce nil)
(generate const-decl "infinite_csequence" csequence_generate nil)
(generate_struct const-decl "csequence_struct" csequence_generate
nil))
shostak))
(generate_nth_TCC1 0
(generate_nth_TCC1-1 nil 3513557144
("" (skolem!) (("" (use "index?_infinite") nil nil)) 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)
(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)
(generate const-decl "infinite_csequence" csequence_generate nil)
(infinite_csequence type-eq-decl nil csequence_props nil)
(is_finite inductive-decl "bool" csequence_props nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(csequence type-decl nil csequence_codt nil)
(index?_infinite formula-decl nil csequence_nth nil)
(T formal-type-decl nil csequence_generate nil))
nil))
(generate_nth 0
(generate_nth-1 nil 3513557325
("" (induct "n")
(("1" (skolem!)
(("1"
(expand* "iterate" "nth" "generate" "generate_struct"
"coreduce")
nil nil))
nil)
("2" (skosimp*)
(("2" (expand "iterate" +)
(("2" (expand "nth" +)
(("2" (inst - "f!1" "f!1(t!1)")
(("2" (rewrite "generate_rest")
(("2" (rewrite "iterate_invariant") nil nil)) nil))
nil))
nil))
nil))
nil)
("3" (skolem!) (("3" (use "generate_nth_TCC1") nil nil)) nil))
nil)
((generate_nth_TCC1 subtype-tcc nil csequence_generate nil)
(generate_rest formula-decl nil csequence_generate nil)
(iterate_invariant formula-decl nil function_iterate nil)
(coreduce adt-def-decl "{c: csequence[T] |
inj_empty?(op(x)) AND empty?(c) OR
inj_nonempty?(op(x)) AND nonempty?(c)}"
csequence_codt_coreduce nil)
(generate_struct const-decl "csequence_struct" csequence_generate
nil)
(nat_induction formula-decl nil naturalnumbers nil)
(iterate def-decl "T" function_iterate nil)
(nth def-decl "T" csequence_nth nil)
(indexes type-eq-decl nil csequence_nth nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(pred type-eq-decl nil defined_types 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)
(T formal-type-decl nil csequence_generate nil)
(csequence type-decl nil csequence_codt nil)
(index? def-decl "bool" csequence_nth nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(is_finite inductive-decl "bool" csequence_props nil)
(infinite_csequence type-eq-decl nil csequence_props nil)
(generate const-decl "infinite_csequence" csequence_generate nil))
shostak))
(generate_add 0
(generate_add-1 nil 3513557394
("" (skosimp)
(("" (expand* "generate" "generate_struct")
(("" (expand "coreduce" 1 2) (("" (assert) nil nil)) nil)) nil))
nil)
((generate_struct const-decl "csequence_struct" csequence_generate
nil)
(generate const-decl "infinite_csequence" csequence_generate nil)
(coreduce adt-def-decl "{c: csequence[T] |
inj_empty?(op(x)) AND empty?(c) OR
inj_nonempty?(op(x)) AND nonempty?(c)}"
csequence_codt_coreduce nil))
shostak))
(generate_some 0
(generate_some-1 nil 3513557413
("" (auto-rewrite "generate_nth")
(("" (skolem!)
(("" (use "nth_some")
(("" (ground)
(("1" (skolem!) (("1" (inst?) nil nil)) nil)
("2" (skolem!)
(("2" (inst + "n!1")
(("2" (use "generate_nth_TCC1") nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((generate_nth formula-decl nil csequence_generate nil)
(indexes type-eq-decl nil csequence_nth nil)
(index? def-decl "bool" csequence_nth 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)
(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)
(n!1 skolem-const-decl "nat" csequence_generate nil)
(t!1 skolem-const-decl "T" csequence_generate nil)
(f!1 skolem-const-decl "[T -> T]" csequence_generate nil)
(generate_nth_TCC1 subtype-tcc nil csequence_generate nil)
(csequence type-decl nil csequence_codt nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(is_finite inductive-decl "bool" csequence_props nil)
(infinite_csequence type-eq-decl nil csequence_props nil)
(generate const-decl "infinite_csequence" csequence_generate nil)
(pred type-eq-decl nil defined_types nil)
(T formal-type-decl nil csequence_generate nil)
(nth_some formula-decl nil csequence_nth nil))
shostak))
(generate_every 0
(generate_every-1 nil 3513557494
("" (auto-rewrite "generate_nth")
(("" (skolem!)
(("" (use "nth_every")
(("" (ground)
(("1" (skolem!)
(("1" (inst - "n!1")
(("1" (use "generate_nth_TCC1") nil nil)) nil))
nil)
("2" (skolem!) (("2" (inst - "i!1") nil nil)) nil))
nil))
nil))
nil))
nil)
((generate_nth formula-decl nil csequence_generate 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)
(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)
(index? def-decl "bool" csequence_nth nil)
(indexes type-eq-decl nil csequence_nth nil)
(n!1 skolem-const-decl "nat" csequence_generate nil)
(t!1 skolem-const-decl "T" csequence_generate nil)
(f!1 skolem-const-decl "[T -> T]" csequence_generate nil)
(generate_nth_TCC1 subtype-tcc nil csequence_generate nil)
(csequence type-decl nil csequence_codt nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(is_finite inductive-decl "bool" csequence_props nil)
(infinite_csequence type-eq-decl nil csequence_props nil)
(generate const-decl "infinite_csequence" csequence_generate nil)
(pred type-eq-decl nil defined_types nil)
(T formal-type-decl nil csequence_generate nil)
(nth_every formula-decl nil csequence_nth nil))
shostak)))
¤ Dauer der Verarbeitung: 0.27 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
