|
(csequence_induction
(cseq_induction 0
(cseq_induction-1 nil 3513553237
("" (skosimp)
(("" (lemma "every_weak_coinduction")
((""
(inst - "p!1"
"LAMBDA cseq: (index?(cseq)(0) IMPLIES p!1(nth(cseq, 0))) AND (FORALL n: (index?(cseq)(n) IMPLIES p!1(nth(cseq, n))) IMPLIES (index?(cseq)(n + 1) IMPLIES p!1(nth(cseq, n + 1))))")
(("" (split)
(("1" (inst - "cseq!1") (("1" (prop) nil nil)) nil)
("2" (delete -1 -2 2)
(("2" (skosimp)
(("2" (expand "nth" -)
(("2" (expand "index?" -)
(("2" (expand "nth" 1 1)
(("2" (expand "index?" 1 1)
(("2" (lift-if)
(("2" (ground)
(("1" (inst - 0)
(("1" (expand* "nth" "index?") nil nil))
nil)
("2" (skosimp)
(("2" (inst - "1 + n!1")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((T formal-type-decl nil csequence_induction nil)
(every_weak_coinduction formula-decl nil csequence_codt nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(nth def-decl "T" csequence_nth 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)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(csequence type-decl nil csequence_codt nil)
(pred type-eq-decl nil defined_types nil)
(PRED type-eq-decl nil defined_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil))
shostak))
(cseq_infinite_induction_TCC1 0
(cseq_infinite_induction_TCC1-1 nil 3513553168
("" (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)
(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_induction nil))
nil))
(cseq_infinite_induction_TCC2 0
(cseq_infinite_induction_TCC2-1 nil 3513553168
("" (skosimp*) (("" (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)
(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_induction nil))
nil))
(cseq_infinite_induction_TCC3 0
(cseq_infinite_induction_TCC3-1 nil 3513553168
("" (skosimp*) (("" (use "index?_infinite") nil nil)) nil)
((+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields 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)
(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)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(index?_infinite formula-decl nil csequence_nth nil)
(T formal-type-decl nil csequence_induction nil))
nil))
(cseq_infinite_induction 0
(cseq_infinite_induction-1 nil 3513553548
("" (skosimp)
(("" (use "cseq_induction")
(("" (assert)
(("" (skosimp)
(("" (use "index?_infinite")
(("" (assert)
(("" (inst - "n!1") (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil)
((cseq_induction formula-decl nil csequence_induction nil)
(pred type-eq-decl nil defined_types 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)
(T formal-type-decl nil csequence_induction nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers 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?_infinite formula-decl nil csequence_nth nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil))
shostak))
(CSEQ_induction 0
(CSEQ_induction-1 nil 3513553706
("" (skosimp)
(("" (lemma "every_coinduction")
((""
(inst - "p!1"
"LAMBDA cseq: (index?(cseq)(0) IMPLIES p!1(nth(cseq, 0))) AND (FORALL n: (FORALL m: m < n IMPLIES (index?(cseq)(m) IMPLIES p!1(nth(cseq, m)))) IMPLIES (index?(cseq)(n) IMPLIES p!1(nth(cseq, n))))")
(("" (split)
(("1" (inst - "cseq!1")
(("1" (prop)
(("1" (inst - 0)
(("1" (prop)
(("1" (skosimp) (("1" (assert) nil nil)) nil)) nil))
nil))
nil))
nil)
("2" (delete -1 2)
(("2" (skosimp)
(("2" (lift-if)
(("2" (expand "nth" -1)
(("2" (expand "index?" -1)
(("2" (expand "index?" 1 1)
(("2" (ground)
(("1" (inst - 1)
(("1" (expand "nth" -3 2)
(("1" (expand "index?" -3 2)
(("1"
(expand "index?" -3 2)
(("1"
(skosimp)
(("1"
(expand "nth")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp)
(("2" (inst -4 "1 + n!1")
(("2" (expand "index?" -4 2)
(("2"
(expand "nth" -4 2)
(("2"
(prop)
(("2"
(skosimp)
(("2"
(expand "nth" 1)
(("2"
(ground)
(("2"
(inst - "m!1 - 1")
(("2"
(expand "index?" -2)
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((T formal-type-decl nil csequence_induction nil)
(every_coinduction formula-decl nil csequence_codt 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)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(< const-decl "bool" reals nil)
(nth def-decl "T" csequence_nth 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)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(csequence type-decl nil csequence_codt nil)
(pred type-eq-decl nil defined_types nil)
(PRED type-eq-decl nil defined_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
shostak))
(CSEQ_infinite_induction_TCC1 0
(CSEQ_infinite_induction_TCC1-1 nil 3513553168
("" (skosimp) (("" (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)
(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_induction nil))
nil))
(CSEQ_infinite_induction_TCC2 0
(CSEQ_infinite_induction_TCC2-1 nil 3513553168
("" (skosimp) (("" (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)
(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_induction nil))
nil))
(CSEQ_infinite_induction 0
(CSEQ_infinite_induction-1 nil 3513554388
("" (skosimp)
(("" (use "CSEQ_induction")
(("" (assert)
(("" (skosimp)
(("" (inst -3 "n!1")
(("" (assert)
(("" (skosimp)
(("" (inst - "m!1")
(("" (assert) (("" (use "index?_infinite") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((CSEQ_induction formula-decl nil csequence_induction nil)
(pred type-eq-decl nil defined_types 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)
(T formal-type-decl nil csequence_induction nil)
(index?_infinite formula-decl nil csequence_nth nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props 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))
shostak))
(finite_sequence_induction 0
(finite_sequence_induction-1 nil 3513554466
("" (skosimp*)
(("" (lemma "nat_induction")
((""
(inst -
"LAMBDA (n: nat): FORALL fseq: length(fseq) = n IMPLIES sp!1(fseq)")
(("" (prop)
(("1" (inst - "length(fseq!1)")
(("1" (inst - "fseq!1") nil nil)) nil)
("2" (skosimp)
(("2" (lemma "length_empty?_rew" ("cseq" "fseq!2"))
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((nat_induction formula-decl nil naturalnumbers nil)
(length_empty?_rew formula-decl nil csequence_length nil)
(length def-decl "{n | has_length(fseq, n)}" csequence_length nil)
(has_length def-decl "bool" csequence_props nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(finite_csequence nonempty-type-eq-decl nil csequence_props nil)
(is_finite inductive-decl "bool" csequence_props nil)
(csequence type-decl nil csequence_codt nil)
(T formal-type-decl nil csequence_induction nil)
(pred type-eq-decl nil defined_types nil)
(nat nonempty-type-eq-decl nil naturalnumbers 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))
(FINITE_SEQUENCE_induction 0
(FINITE_SEQUENCE_induction-1 nil 3513554747
("" (skosimp*)
(("" (lemma "NAT_induction")
((""
(inst -
"LAMBDA (n: nat): FORALL fseq: length(fseq) = n IMPLIES sp!1(fseq)")
(("" (prop)
(("1" (inst - "length(fseq!1)")
(("1" (inst - "fseq!1") nil nil)) nil)
("2" (skosimp*)
(("2" (inst -3 "j!1")
(("2" (split)
(("1" (inst - "fseq!2") (("1" (assert) nil nil)) nil)
("2" (skosimp)
(("2" (inst - "length(fseq!3)")
(("2" (assert) (("2" (inst - "fseq!3") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((NAT_induction formula-decl nil naturalnumbers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(length def-decl "{n | has_length(fseq, n)}" csequence_length nil)
(has_length def-decl "bool" csequence_props nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(finite_csequence nonempty-type-eq-decl nil csequence_props nil)
(is_finite inductive-decl "bool" csequence_props nil)
(csequence type-decl nil csequence_codt nil)
(T formal-type-decl nil csequence_induction nil)
(pred type-eq-decl nil defined_types nil)
(nat nonempty-type-eq-decl nil naturalnumbers 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))
(sequence_induction 0
(sequence_induction-1 nil 3513554918
("" (skosimp*)
(("" (use "finite_sequence_induction")
(("" (prop)
(("" (inst - "cseq!1") (("" (inst - "cseq!1") nil nil)) nil))
nil))
nil))
nil)
((finite_sequence_induction formula-decl nil csequence_induction
nil)
(pred type-eq-decl nil defined_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(csequence type-decl nil csequence_codt nil)
(T formal-type-decl nil csequence_induction nil)
(is_finite inductive-decl "bool" csequence_props nil)
(finite_csequence nonempty-type-eq-decl nil csequence_props nil)
(cseq!1 skolem-const-decl "csequence[T]" csequence_induction nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(infinite_csequence type-eq-decl nil csequence_props nil))
shostak))
(SEQUENCE_induction 0
(SEQUENCE_induction-1 nil 3513554944
("" (skosimp*)
(("" (use "FINITE_SEQUENCE_induction")
(("" (prop)
(("" (inst - "cseq!1") (("" (inst - "cseq!1") nil nil)) nil))
nil))
nil))
nil)
((FINITE_SEQUENCE_induction formula-decl nil csequence_induction
nil)
(pred type-eq-decl nil defined_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(csequence type-decl nil csequence_codt nil)
(T formal-type-decl nil csequence_induction nil)
(is_finite inductive-decl "bool" csequence_props nil)
(finite_csequence nonempty-type-eq-decl nil csequence_props nil)
(cseq!1 skolem-const-decl "csequence[T]" csequence_induction nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(infinite_csequence type-eq-decl nil csequence_props nil))
shostak)))
¤ Dauer der Verarbeitung: 0.26 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.
|
