|
(reduction
(IMP_rewrite_rules_TCC1 0
(IMP_rewrite_rules_TCC1-1 nil 3416212122
("" (lemma "var_countable") (("" (propax) nil nil)) nil)
((var_countable formula-decl nil reduction nil)) nil))
(closure_close_subs 0
(closure_close_subs-1 nil 3433013930
("" (skeep)
(("" (expand "close_subs?")
(("" (split)
(("1" (skeep)
(("1" (expand "TC")
(("1" (expand "IUnion")
(("1" (skolem * "j")
(("1" (generalize "s" "s" :fnums (-1 1))
(("1" (generalize "t" "t" :fnums 1)
(("1" (generalize "j" "n" :fnums 1)
(("1" (induct "n")
(("1" (assert) nil nil) ("2" (assert) nil nil)
("3" (skosimp*)
(("3" (prop)
(("1" (rewrite "iterate_add_one")
(("1"
(expand "o")
(("1"
(skosimp*)
(("1"
(inst -1 "t!1" "y!1")
(("1"
(assert)
(("1"
(skosimp*)
(("1"
(inst -5 "s!1" "y!1" "sigma")
(("1"
(assert)
(("1"
(inst 1 "i!1 + 1")
(("1"
(rewrite
"iterate_add_one"
1)
(("1"
(expand "o")
(("1"
(inst
1
"ext(sigma)(y!1)")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (typepred "j!1")
(("2"
(case "j!1 = 0")
(("1"
(hide-all-but (-1 -4 -5 2))
(("1"
(replaces -1)
(("1"
(assert)
(("1"
(rewrite "iterate_1")
(("1"
(inst -2 "s!1" "t!1" "sigma")
(("1"
(inst 1 "1")
(("1"
(rewrite "iterate_1")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skeep)
(("2" (expand "RTC")
(("2" (expand "IUnion")
(("2" (skolem * "j")
(("2" (generalize "s" "s" :fnums (-1 1))
(("2" (generalize "t" "t" :fnums 1)
(("2" (generalize "j" "n" :fnums 1)
(("2" (induct "n")
(("1" (skolem * ("s1" "t1"))
(("1" (flatten)
(("1" (inst 1 "0")
(("1"
(hide -2)
(("1"
(expand "iterate")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2" (rewrite "iterate_add_one")
(("2" (expand "o")
(("2"
(skosimp*)
(("2"
(inst -1 "t!1" "y!1")
(("2"
(assert)
(("2"
(skosimp*)
(("2"
(inst -4 "s!1" "y!1" "sigma")
(("2"
(assert)
(("2"
(inst 1 "i!1 + 1")
(("2"
(rewrite
"iterate_add_one"
1)
(("2"
(expand "o")
(("2"
(inst
1
"ext(sigma)(y!1)")
(("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)
("3" (skeep)
(("3" (expand "EC")
(("3" (expand "RTC")
(("3" (expand "IUnion")
(("3" (skolem * "j")
(("3" (generalize "s" "s" :fnums (-1 1))
(("3" (generalize "t" "t" :fnums 1)
(("3" (generalize "j" "n" :fnums 1)
(("3" (induct "n")
(("1" (skolem * ("s1" "t1"))
(("1" (flatten)
(("1"
(hide -2)
(("1"
(inst 1 "0")
(("1"
(expand "iterate")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2" (rewrite "iterate_add_one")
(("2"
(expand "o")
(("2"
(skosimp*)
(("2"
(inst -1 "t!1" "y!1")
(("2"
(assert)
(("2"
(skosimp*)
(("2"
(expand "SC" -2)
(("2"
(expand* "union" "member")
(("2"
(prop)
(("1"
(inst
-4
"s!1"
"y!1"
"sigma")
(("1"
(assert)
(("1"
(lemma
"R_subset_SC")
(("1"
(inst?)
(("1"
(expand
"subset?")
(("1"
(inst
-1
"(ext(sigma)(s!1), ext(sigma)(y!1))")
(("1"
(expand
"member")
(("1"
(assert)
(("1"
(inst
1
"i!1 + 1")
(("1"
(rewrite
"iterate_add_one")
(("1"
(expand
"o")
(("1"
(inst
1
"ext(sigma)(y!1)")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand "converse")
(("2"
(inst 1 "i!1 + 1")
(("2"
(rewrite
"iterate_add_one")
(("2"
(expand "o")
(("2"
(inst
1
"ext(sigma)(y!1)")
(("2"
(assert)
(("2"
(expand
"SC"
1)
(("2"
(expand*
"union"
"member"
"converse")
(("2"
(prop)
(("2"
(inst
-4
"y!1"
"s!1"
"sigma")
(("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))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((close_subs? const-decl "bool" reduction nil)
(subset? const-decl "bool" sets nil)
(R_subset_SC formula-decl nil relations_closure nil)
(converse const-decl "pred[[T2, T1]]" relation_defs nil)
(union const-decl "set" sets nil)
(member const-decl "bool" sets nil)
(PRED type-eq-decl nil defined_types nil)
(symmetric? const-decl "bool" relations nil)
(symmetric type-eq-decl nil relations_closure nil)
(SC const-decl "symmetric" relations_closure nil)
(EC const-decl "equivalence" relations_closure nil)
(RTC const-decl "reflexive_transitive" relations_closure nil)
(IUnion const-decl "set[T]" indexed_sets nil)
(ext def-decl "term" substitution nil)
(Sub type-eq-decl nil substitution nil)
(Sub? const-decl "bool" substitution nil)
(V const-decl "set[term]" variables_term nil)
(set type-eq-decl nil sets nil)
(posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(iterate def-decl "pred[[T, T]]" relation_iterate "orders/")
(pred type-eq-decl nil defined_types nil)
(term type-decl nil term_adt nil)
(arity formal-const-decl "[symbol -> nat]" reduction 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)
(symbol formal-nonempty-type-decl nil reduction nil)
(variable formal-nonempty-type-decl nil reduction nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(even_plus_odd_is_odd application-judgement "odd_int" integers nil)
(iterate_1 formula-decl nil relation_iterate "orders/")
(= const-decl "[T, T -> boolean]" equalities nil)
(iterate_add_one formula-decl nil relation_iterate "orders/")
(int_minus_int_is_int application-judgement "int" integers nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(O const-decl "bool" relation_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nat_induction formula-decl nil naturalnumbers nil)
(TC const-decl "transitive" relations_closure nil))
shostak))
(reduction_is_subs_op 0
(reduction_is_subs_op-1 nil 3433014142
("" (skeep)
(("" (split)
(("1" (expand "close_subs?")
(("1" (skosimp*)
(("1" (expand "reduction?")
(("1" (skosimp*)
(("1" (inst 1 "e!1" "comp(sigma!1, sigma!2)" "p!1")
(("1" (split)
(("1" (rewrite "ext_o")
(("1" (expand "o")
(("1" (rewrite "subterm_ext_commute")
(("1" (assert) nil nil)) nil))
nil))
nil)
("2" (rewrite "ext_o")
(("2" (expand "o")
(("2" (replace -2)
(("2" (lemma "ext_replace_ext")
(("2"
(inst -1 "p!1" "s!1" "sigma!1"
"ext(sigma!2)(rhs(e!1))")
(("2" (typepred "p!1")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (rewrite "ext_preserv_pos") nil nil)
("3" (rewrite "subs_o") nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "comp_op?")
(("2" (skosimp*)
(("2" (expand "reduction?")
(("2" (skosimp*)
(("2" (inst 1 "e!1" "sigma!1" "add_first(i!1 + 1, p!1)")
(("1" (split)
(("1" (expand "subtermOF" 1)
(("1" (lift-if)
(("1" (prop)
(("1" (grind) nil nil)
("2" (expand "finseq_appl")
(("2"
(case-replace
"first(add_first(1 + i!1, p!1)) - 1 = i!1"
:hide? t)
(("1"
(case-replace
"rest(add_first(1 + i!1, p!1)) = p!1"
:hide? t)
(("1"
(hide-all-but 1)
(("1"
(rewrite "rest_add_first")
nil
nil))
nil))
nil)
("2" (hide-all-but 1)
(("2"
(rewrite "first_add")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "finseq_appl")
(("2" (decompose-equality)
(("1" (grind) nil nil)
("2" (expand "replace")
(("2" (expand "finseq_appl")
(("2" (decompose-equality)
(("1" (grind) nil nil)
("2" (decompose-equality)
(("2"
(lift-if)
(("2"
(prop)
(("1" (grind) nil nil)
("2" (grind) nil nil)
("3" (grind) nil nil))
nil))
nil))
nil)
("3" (grind) nil nil))
nil))
nil))
nil)
("3" (grind) nil nil))
nil))
nil))
nil)
("2" (hide (-1 -2))
(("2" (typepred "p!1")
(("2" (expand "finseq_appl")
(("2" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((subs_o formula-decl nil substitution nil)
(ext_preserv_pos formula-decl nil substitution nil)
(O const-decl "T3" function_props nil)
(subterm_ext_commute formula-decl nil substitution nil)
(ext_o formula-decl nil substitution nil)
(ext_replace_ext formula-decl nil substitution nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(rhs const-decl "term" rewrite_rules nil)
(member const-decl "bool" sets nil)
(rewrite_rule type-eq-decl nil rewrite_rules nil)
(rewrite_rule? const-decl "bool" rewrite_rules nil)
(below type-eq-decl nil nat_types nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(posnat nonempty-type-eq-decl nil integers nil)
(position type-eq-decl nil positions nil)
(positions type-eq-decl nil positions nil)
(positionsOF def-decl "positions" positions nil)
(ext def-decl "term" substitution nil)
(s!1 skolem-const-decl "term[variable, symbol, arity]" reduction
nil)
(positions? type-eq-decl nil positions nil)
(p!1 skolem-const-decl "positions?[variable, symbol, arity](s!1)"
reduction nil)
(variable formal-nonempty-type-decl nil reduction nil)
(symbol formal-nonempty-type-decl nil reduction 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)
(arity formal-const-decl "[symbol -> nat]" reduction nil)
(term type-decl nil term_adt nil) (set type-eq-decl nil sets nil)
(V const-decl "set[term]" variables_term nil)
(Sub? const-decl "bool" substitution nil)
(Sub type-eq-decl nil substitution nil)
(comp const-decl "term" substitution nil)
(sigma!1 skolem-const-decl "Sub[variable, symbol, arity]" reduction
nil)
(sigma!2 skolem-const-decl "Sub[variable, symbol, arity]" reduction
nil)
(reduction? const-decl "bool" reduction nil)
(close_subs? const-decl "bool" reduction nil)
(<= const-decl "bool" reals nil)
(upto? nonempty-type-eq-decl nil IUnion_extra nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(union const-decl "set" sets nil)
(IUnion const-decl "set[T]" indexed_sets nil)
(catenate const-decl "positions" positions nil)
(only_empty_seq const-decl "positions" positions nil)
(first_add formula-decl nil seq_extras "structures/")
(rest const-decl "finseq" seq_extras "structures/")
(rest_add_first formula-decl nil seq_extras "structures/")
(int_minus_int_is_int application-judgement "int" integers nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(/= const-decl "boolean" notequal nil)
(not_empty_seq type-eq-decl nil seq_extras "structures/")
(first const-decl "T" seq_extras "structures/")
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(insert? const-decl "finseq" seq_extras "structures/")
(subtermOF def-decl "term" subterm nil)
(e!1 skolem-const-decl "{e | member(e, E)}" reduction nil)
(E skolem-const-decl "set[rewrite_rule]" reduction nil)
(sigma!1 skolem-const-decl "Sub[variable, symbol, arity]" reduction
nil)
(replaceTerm def-decl "term" replacement nil)
(replace const-decl "finseq" seq_extras "structures/")
(term_app_extensionality formula-decl nil term_adt nil)
(empty_seq const-decl "finseq" finite_sequences nil)
(min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
(^ const-decl "finseq" finite_sequences 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_min application-judgement "{k: int | k <= i AND k <= j}"
real_defs nil)
(lhs const-decl "term" rewrite_rules nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(args adt-accessor-decl
"[d: (app?) -> {args: finite_sequence[term] | args`length = arity(f(d))}]"
term_adt nil)
(f adt-accessor-decl "[(app?) -> symbol]" term_adt nil)
(IFF const-decl "[bool, bool -> bool]" booleans nil)
(finite_sequence type-eq-decl nil finite_sequences nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(app? adt-recognizer-decl "[term -> boolean]" term_adt nil)
(app adt-constructor-decl
"[[f: symbol, {args: finite_sequence[term] | args`length = arity(f)}] ->
(app?)]" term_adt nil)
(n!1 skolem-const-decl "nat" reduction nil)
(arity_eq type-eq-decl nil compatibility nil)
(f!1 skolem-const-decl "arity_eq[variable, symbol, arity](n!1)"
reduction nil)
(finseq type-eq-decl nil finite_sequences nil)
(fs_len type-eq-decl nil seq_extras "structures/")
(st1!1 skolem-const-decl
"fs_len[term[variable, symbol, arity]](n!1)" reduction nil)
(add_first const-decl "finseq" seq_extras "structures/")
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(< const-decl "bool" reals nil)
(i!1 skolem-const-decl "below[n!1]" reduction nil)
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil)
(p!1 skolem-const-decl "positions?
[variable, symbol, arity](finseq_appl[term[variable, symbol, arity]]
(st1!1)(i!1))" reduction nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(comp_op? const-decl "bool" compatibility nil))
shostak))
(lhs_reduces_to_rhs 0
(lhs_reduces_to_rhs-1 nil 3433014645
("" (skeep)
(("" (expand "reduction?")
(("" (inst 1 "e" "identity" "empty_seq")
(("1" (expand* "subtermOF" "replaceTerm")
(("1" (lift-if)
(("1" (rewrite "ext_iden")
(("1" (rewrite "ext_iden")
(("1" (rewrite "empty_0") nil nil)) nil))
nil))
nil))
nil)
("2" (expand "positionsOF")
(("2" (lift-if) (("2" (grind) nil nil)) nil)) nil)
("3" (rewrite "iden_subs") nil nil))
nil))
nil))
nil)
((reduction? const-decl "bool" reduction nil)
(iden_subs formula-decl nil substitution nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(only_empty_seq const-decl "positions" positions nil)
(union const-decl "set" sets nil)
(IUnion const-decl "set[T]" indexed_sets nil)
(catenate const-decl "positions" positions nil)
(add_first const-decl "finseq" seq_extras "structures/")
(insert? const-decl "finseq" seq_extras "structures/")
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil)
(replaceTerm def-decl "term" replacement nil)
(subtermOF def-decl "term" subterm nil)
(ext_iden formula-decl nil substitution nil)
(empty_0 formula-decl nil seq_extras "structures/")
(rhs const-decl "term" rewrite_rules nil)
(positions? type-eq-decl nil positions nil)
(Sub type-eq-decl nil substitution nil)
(below type-eq-decl nil nat_types nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(posnat nonempty-type-eq-decl nil integers nil)
(position type-eq-decl nil positions nil)
(positions type-eq-decl nil positions nil)
(positionsOF def-decl "positions" positions nil)
(rewrite_rule? const-decl "bool" rewrite_rules nil)
(rewrite_rule type-eq-decl nil rewrite_rules nil)
(lhs const-decl "term" rewrite_rules nil)
(member const-decl "bool" sets nil)
(E skolem-const-decl "set[rewrite_rule]" reduction nil)
(e skolem-const-decl "{e | member(e, E)}" reduction nil)
(finseq type-eq-decl nil finite_sequences nil)
(empty_seq const-decl "finseq" finite_sequences nil)
(variable formal-nonempty-type-decl nil reduction nil)
(symbol formal-nonempty-type-decl nil reduction 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)
(arity formal-const-decl "[symbol -> nat]" reduction nil)
(term type-decl nil term_adt nil) (set type-eq-decl nil sets nil)
(V const-decl "set[term]" variables_term nil)
(Sub? const-decl "bool" substitution nil)
(bijective? const-decl "bool" functions nil)
(identity const-decl "(bijective?[T, T])" identity nil))
shostak)))
¤ Dauer der Verarbeitung: 0.19 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.
|
