|
(replacement
(replaceTerm_TCC1 0
(replaceTerm_TCC1-1 nil 3389903609
("" (skosimp*)
(("" (lemma "not_var")
(("" (inst -1 "first(p!1)" "p!1" "rest(p!1)" "s!1")
(("1" (typepred "p!1")
(("1" (assert)
(("1"
(lemma "finite_sequences_extras[posnat].seq_first_rest")
(("1" (inst?) (("1" (assert) nil nil)) nil)) nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil)
nil nil))
(replaceTerm_TCC2 0
(replaceTerm_TCC2-1 nil 3389903609
("" (skosimp*)
(("" (typepred "p!1")
(("" (expand "positionsOF")
(("" (lift-if)
(("" (prop)
(("1" (expand "only_empty_seq")
(("1" (rewrite "empty_0") nil nil)) nil)
("2" (expand "only_empty_seq")
(("2" (rewrite "empty_0") nil nil)) nil)
("3" (expand "only_empty_seq")
(("3" (hide -1) (("3" (rewrite "empty_0") nil nil)) nil))
nil)
("4" (expand "only_empty_seq")
(("4" (hide -1) (("4" (rewrite "empty_0") nil nil)) nil))
nil)
("5" (assert) nil nil)
("6" (replaces -2)
(("6" (expand* "union" "member")
(("6" (prop)
(("1" (expand "only_empty_seq")
(("1" (rewrite "empty_0") nil nil)) nil)
("2" (expand "IUnion")
(("2" (skolem * "j")
(("2" (expand "catenate")
(("2" (skolem * "p1")
(("2" (flatten)
(("2" (hide -1)
(("2"
(lemma "fsepn.seq_first_rest")
(("2"
(inst?)
(("2"
(assert)
(("2"
(replace -1 -2)
(("2"
(hide -1)
(("2"
(lemma "fsepn.first_equal")
(("2"
(inst?)
(("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)
((positions? type-eq-decl nil positions nil)
(positionsOF def-decl "positions" positions nil)
(positions type-eq-decl nil positions nil)
(position type-eq-decl nil positions nil)
(posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(below type-eq-decl nil nat_types nil)
(term type-decl nil term_adt nil)
(arity formal-const-decl "[symbol -> nat]" replacement 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 replacement nil)
(variable formal-nonempty-type-decl nil replacement nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(first_equal formula-decl nil seq_extras "structures/")
(upto? nonempty-type-eq-decl nil IUnion_extra 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)
(= const-decl "[T, T -> boolean]" equalities nil)
(finite_sequence type-eq-decl nil finite_sequences nil)
(app? adt-recognizer-decl "[term -> boolean]" term_adt nil)
(<= const-decl "bool" reals nil)
(first const-decl "T" seq_extras "structures/")
(not_empty_seq type-eq-decl nil seq_extras "structures/")
(/= const-decl "boolean" notequal nil)
(rest const-decl "finseq" seq_extras "structures/")
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(seq_first_rest formula-decl nil seq_extras "structures/")
(catenate const-decl "positions" positions nil)
(IUnion const-decl "set[T]" indexed_sets nil)
(union const-decl "set" sets nil)
(member const-decl "bool" sets nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(only_empty_seq const-decl "positions" positions nil)
(finseq type-eq-decl nil finite_sequences nil)
(empty_0 formula-decl nil seq_extras "structures/"))
nil))
(replaceTerm_TCC3 0
(replaceTerm_TCC3-1 nil 3389903609
("" (skosimp*)
(("" (typepred "p!1")
(("" (expand "positionsOF" -1)
(("" (lift-if)
(("" (prop)
(("1" (expand "only_empty_seq")
(("1" (rewrite "empty_0") nil nil)) nil)
("2" (expand "only_empty_seq")
(("2" (rewrite "empty_0") nil nil)) nil)
("3" (expand* "union" "member")
(("3" (prop)
(("1" (expand "only_empty_seq")
(("1" (rewrite "empty_0") nil nil)) nil)
("2" (expand "IUnion")
(("2" (skolem * "i1")
(("2" (expand "catenate")
(("2" (skolem * "y1")
(("2" (expand "member")
(("2" (flatten)
(("2" (lemma "fsepn.first_equal")
(("2"
(inst -1 "q!1" "y1" "i!1" "i1")
(("2"
(prop)
(("1"
(replaces -1)
(("1"
(replaces -1)
(("1" (replaces -3) nil nil))
nil))
nil)
("2"
(lemma "fsepn.seq_first_rest")
(("2"
(inst?)
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((positions? type-eq-decl nil positions nil)
(positionsOF def-decl "positions" positions nil)
(positions type-eq-decl nil positions nil)
(position type-eq-decl nil positions nil)
(posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(below type-eq-decl nil nat_types nil)
(term type-decl nil term_adt nil)
(arity formal-const-decl "[symbol -> nat]" replacement 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 replacement nil)
(variable formal-nonempty-type-decl nil replacement nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(member const-decl "bool" sets nil)
(union const-decl "set" sets nil)
(IUnion const-decl "set[T]" indexed_sets nil)
(catenate const-decl "positions" positions nil)
(first_equal formula-decl nil seq_extras "structures/")
(int_minus_int_is_int application-judgement "int" integers nil)
(seq_first_rest formula-decl nil seq_extras "structures/")
(<= const-decl "bool" reals nil)
(app? adt-recognizer-decl "[term -> boolean]" term_adt nil)
(finite_sequence type-eq-decl nil finite_sequences nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(f adt-accessor-decl "[(app?) -> symbol]" term_adt nil)
(args adt-accessor-decl
"[d: (app?) -> {args: finite_sequence[term] | args`length = arity(f(d))}]"
term_adt nil)
(upto? nonempty-type-eq-decl nil IUnion_extra nil)
(only_empty_seq const-decl "positions" positions nil)
(finseq type-eq-decl nil finite_sequences nil)
(empty_0 formula-decl nil seq_extras "structures/"))
nil))
(replaceTerm_TCC4 0
(replaceTerm_TCC4-1 nil 3389903609
("" (skosimp*)
(("" (replaces -3) (("" (rewrite "length_rest") nil nil)) nil))
nil)
((posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers 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)
(positions? type-eq-decl nil positions nil)
(positionsOF def-decl "positions" positions nil)
(positions type-eq-decl nil positions nil)
(term type-decl nil term_adt nil)
(position type-eq-decl nil positions nil)
(arity formal-const-decl "[symbol -> nat]" replacement nil)
(symbol formal-nonempty-type-decl nil replacement nil)
(variable formal-nonempty-type-decl nil replacement nil)
(finseq type-eq-decl nil finite_sequences nil)
(below type-eq-decl nil nat_types nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(length_rest formula-decl nil seq_extras "structures/"))
nil))
(replaceTerm_TCC5 0
(replaceTerm_TCC5-1 nil 3389903609 ("" (termination-tcc) nil nil)
((positions? type-eq-decl nil positions nil)
(positionsOF def-decl "positions" positions nil)
(positions type-eq-decl nil positions nil)
(position type-eq-decl nil positions nil)
(below type-eq-decl nil nat_types nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(real_ge_is_total_order name-judgement "(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)
(only_empty_seq const-decl "positions" positions nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(finite_sequence type-eq-decl nil finite_sequences nil)
(app? adt-recognizer-decl "[term -> boolean]" term_adt nil)
(f adt-accessor-decl "[(app?) -> symbol]" term_adt nil)
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil)
(posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers 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)
(first const-decl "T" seq_extras "structures/")
(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)
(rest const-decl "finseq" seq_extras "structures/")
(term type-decl nil term_adt nil)
(arity formal-const-decl "[symbol -> nat]" replacement nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(symbol formal-nonempty-type-decl nil replacement nil)
(variable formal-nonempty-type-decl nil replacement nil)
(replace const-decl "finseq" seq_extras "structures/")
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil))
nil))
(replaceTerm_TCC6 0
(replaceTerm_TCC6-1 nil 3389903609 ("" (termination-tcc) nil nil)
((positions? type-eq-decl nil positions nil)
(positionsOF def-decl "positions" positions nil)
(positions type-eq-decl nil positions nil)
(position type-eq-decl nil positions nil)
(below type-eq-decl nil nat_types nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(real_ge_is_total_order name-judgement "(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)
(= const-decl "[T, T -> boolean]" equalities nil)
(finite_sequence type-eq-decl nil finite_sequences nil)
(app? adt-recognizer-decl "[term -> boolean]" term_adt nil)
(f adt-accessor-decl "[(app?) -> symbol]" term_adt nil)
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil)
(posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers 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)
(first const-decl "T" seq_extras "structures/")
(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)
(rest const-decl "finseq" seq_extras "structures/")
(term type-decl nil term_adt nil)
(arity formal-const-decl "[symbol -> nat]" replacement nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(symbol formal-nonempty-type-decl nil replacement nil)
(variable formal-nonempty-type-decl nil replacement nil)
(replace const-decl "finseq" seq_extras "structures/")
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil))
nil))
(replaceTerm_TCC7 0
(replaceTerm_TCC7-1 nil 3516386077
("" (skosimp*)
(("" (lemma "not_var")
(("" (inst -1 "first(p!1)" "p!1" "rest(p!1)" "s!1")
(("1" (typepred "p!1")
(("1" (assert)
(("1" (lemma "seq_extras[posnat].seq_first_rest")
(("1" (inst?) (("1" (assert) nil nil)) nil)) nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil)
((arity formal-const-decl "[symbol -> nat]" replacement 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)
(symbol formal-nonempty-type-decl nil replacement nil)
(variable formal-nonempty-type-decl nil replacement nil)
(not_var formula-decl nil positions nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(seq_first_rest formula-decl nil seq_extras "structures/")
(rest const-decl "finseq" seq_extras "structures/")
(first const-decl "T" seq_extras "structures/")
(not_empty_seq type-eq-decl nil seq_extras "structures/")
(finseq type-eq-decl nil finite_sequences nil)
(/= const-decl "boolean" notequal 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)
(term type-decl nil term_adt nil)
(positions type-eq-decl nil positions nil)
(positionsOF def-decl "positions" positions nil)
(s!1 skolem-const-decl "term[variable, symbol, arity]" replacement
nil)
(positions? type-eq-decl nil positions nil)
(p!1 skolem-const-decl "positions?[variable, symbol, arity](s!1)"
replacement nil))
nil))
(replace_preserv_pos 0
(replace_preserv_pos-1 nil 3432995634
("" (measure-induct+ "length(p)" "p")
(("" (skeep)
(("" (name-replace "rp" "replaceTerm(s, t, x!1)" :hide? nil)
(("" (expand "replaceTerm" -1)
(("" (lift-if)
(("" (prop)
(("1" (hide -3)
(("1" (expand "positionsOF" 1)
(("1" (lift-if)
(("1" (prop)
(("1" (expand "only_empty_seq")
(("1" (rewrite "empty_0") nil nil)) nil)
("2" (expand "only_empty_seq")
(("2" (rewrite "empty_0") nil nil)) nil)
("3" (expand* "union" "member")
(("3" (prop)
(("3" (expand "only_empty_seq")
(("3" (rewrite "empty_0") nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (copy -1)
(("2" (decompose-equality -1)
(("2" (hide (-1 -2))
(("2" (expand "positionsOF" 2)
(("2" (lift-if)
(("2" (prop)
(("1" (assert) nil nil)
("2" (expand "replace" -2)
(("2" (lift-if)
(("2"
(prop)
(("1"
(hide-all-but (-1 -6 1 2))
(("1"
(expand "positionsOF")
(("1"
(lift-if)
(("1" (prop) nil nil))
nil))
nil))
nil)
("2"
(decompose-equality -1)
(("2"
(hide (-2 -4))
(("2"
(expand "positionsOF" -4)
(("2"
(lift-if)
(("2"
(prop)
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (expand* "union" "member")
(("3" (prop)
(("3"
(expand "only_empty_seq")
(("3"
(expand "finseq_appl")
(("3"
(inst -3 "rest(x!1)")
(("3"
(inst
-3
"args(s)(first(x!1) - 1)"
"t")
(("1"
(prop)
(("1"
(hide -3)
(("1"
(expand "IUnion")
(("1"
(inst 3 "first(x!1)")
(("1"
(expand "catenate")
(("1"
(inst 3 "rest(x!1)")
(("1"
(prop)
(("1"
(expand "member")
(("1"
(replace
-2
1
rl)
(("1"
(hide -2)
(("1"
(lemma
"fset.nth_x")
(("1"
(inst
-1
"args(s)"
"replaceTerm(args(s)(first(x!1) - 1), t, rest(x!1))"
"first(x!1) - 1")
(("1"
(expand
"finseq_appl")
(("1"
(assert)
nil
nil))
nil)
("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but
(1 5))
(("2"
(lemma
"fsepn.seq_first_rest")
(("2"
(inst?)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide -1)
(("2"
(expand "replace")
(("2"
(lift-if)
(("2"
(prop)
(("1"
(expand
"positionsOF")
(("1"
(lift-if)
(("1"
(prop)
(("1"
(expand
"only_empty_seq")
(("1"
(propax)
nil
nil))
nil)
("2"
(expand
"only_empty_seq")
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(decompose-equality)
(("2"
(hide -2)
(("2"
(replace
-1
2
rl)
(("2"
(hide -1)
(("2"
(expand
"positionsOF")
(("2"
(lift-if)
(("2"
(prop)
(("1"
(expand
"only_empty_seq")
(("1"
(propax)
nil
nil))
nil)
("2"
(expand
"only_empty_seq")
(("2"
(expand*
"union"
"member")
(("2"
(prop)
(("2"
(expand
"IUnion")
(("2"
(skolem
*
"i1")
(("2"
(expand
"catenate")
(("2"
(skolem
*
"y1")
(("2"
(expand
"member")
(("2"
(flatten)
(("2"
(hide
-1)
(("2"
(typepred
"i1")
(("2"
(lemma
"fsepn.first_equal")
(("2"
(inst
-1
"rest(x!1)"
"y1"
"first(x!1)"
"i1")
(("2"
(assert)
(("2"
(hide-all-but
(-3
1
7))
(("2"
(lemma
"fsepn.seq_first_rest")
(("2"
(inst
-1
"x!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))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but (-3 1 3))
(("2"
(expand "positionsOF" -1)
(("2"
(lift-if)
(("2"
(prop)
(("1"
(expand
"only_empty_seq")
(("1"
(propax)
nil
nil))
nil)
("2"
(expand
"only_empty_seq")
(("2"
(propax)
nil
nil))
nil)
("3"
(expand*
"union"
"member")
(("3"
(prop)
(("1"
(expand
"only_empty_seq")
(("1"
(propax)
nil
nil))
nil)
("2"
(expand "IUnion")
(("2"
(skolem * "i1")
(("2"
(expand
"catenate")
(("2"
(skolem
*
"y1")
(("2"
(expand
"member")
(("2"
(flatten)
(("2"
(lemma
"fsepn.first_equal")
(("2"
(inst
-1
"rest(x!1)"
"y1"
"first(x!1)"
"i1")
(("2"
(prop)
(("1"
(assert)
nil
nil)
("2"
(hide-all-but
(-2
1
5))
(("2"
(lemma
"fsepn.seq_first_rest")
(("2"
(inst
-1
"x!1")
(("2"
(assert)
(("2"
(prop)
(("2"
(rewrite
"empty_0")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3"
(hide-all-but (1 6))
(("3"
(rewrite "length_rest")
nil
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((finseq type-eq-decl nil finite_sequences nil)
(empty_0 formula-decl nil seq_extras "structures/")
(only_empty_seq const-decl "positions" positions nil)
(union const-decl "set" sets nil)
(member const-decl "bool" sets nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(app? adt-recognizer-decl "[term -> boolean]" term_adt nil)
(f adt-accessor-decl "[(app?) -> symbol]" term_adt nil)
(finite_sequence type-eq-decl nil finite_sequences nil)
(app adt-constructor-decl
"[[f: symbol, {args: finite_sequence[term] | args`length = arity(f)}] ->
(app?)]" term_adt nil)
(replace const-decl "finseq" seq_extras "structures/")
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil)
(args adt-accessor-decl
"[d: (app?) -> {args: finite_sequence[term] | args`length = arity(f(d))}]"
term_adt nil)
(numfield nonempty-type-eq-decl nil number_fields 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/")
(rest const-decl "finseq" seq_extras "structures/")
(IFF const-decl "[bool, bool -> bool]" booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(x!1 skolem-const-decl "position[variable, symbol, arity]"
replacement nil)
(length_rest formula-decl nil seq_extras "structures/")
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(<= const-decl "bool" reals nil)
(rp skolem-const-decl "term[variable, symbol, arity]" replacement
nil)
(upto? nonempty-type-eq-decl nil IUnion_extra nil)
(seq_first_rest formula-decl nil seq_extras "structures/")
(nth_x formula-decl nil seq_extras "structures/")
(catenate const-decl "positions" positions nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(first_equal formula-decl nil seq_extras "structures/")
(IUnion const-decl "set[T]" indexed_sets nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(replaceTerm def-decl "term" replacement nil)
(positions? type-eq-decl nil positions nil)
(positionsOF def-decl "positions" positions nil)
(positions type-eq-decl nil positions nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(term type-decl nil term_adt nil)
(wf_nat formula-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(naturalnumber type-eq-decl nil naturalnumbers nil)
(position type-eq-decl nil positions nil)
(arity formal-const-decl "[symbol -> nat]" replacement nil)
(symbol formal-nonempty-type-decl nil replacement nil)
(variable formal-nonempty-type-decl nil replacement nil)
(posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers 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)
(below type-eq-decl nil nat_types nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(measure_induction formula-decl nil measure_induction nil)
(well_founded? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_types nil))
shostak))
(replace_compose_pos 0
(replace_compose_pos-1 nil 3432997519
("" (measure-induct+ "length(p)" "p")
(("" (skeep)
(("" (expand "positionsOF" -3)
(("" (lift-if)
(("" (prop)
(("1" (hide -3)
(("1" (expand "only_empty_seq")
(("1" (lemma "fsepn.empty_0")
(("1" (inst -1 "x!1")
(("1" (assert)
(("1" (expand "replaceTerm")
(("1" (replaces -5)
(("1" (replaces -3)
(("1" (rewrite "empty_o_seq") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide -3)
(("2" (expand "only_empty_seq")
(("2" (lemma "fsepn.empty_0")
(("2" (inst -1 "x!1")
(("2" (assert)
(("2" (expand "replaceTerm")
(("2" (replaces -5)
(("2" (replaces -3)
(("2" (rewrite "empty_o_seq") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (expand* "union" "member")
(("3" (prop)
(("1" (hide -2)
(("1" (expand "only_empty_seq")
(("1" (lemma "fsepn.empty_0")
(("1" (inst -1 "x!1")
(("1" (assert)
(("1" (expand "replaceTerm")
(("1" (replaces -5)
(("1"
(replaces -4)
(("1"
(replaces -2)
(("1"
(rewrite "empty_o_seq")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(name-replace "rp" "replaceTerm(s, t, x!1)" :hide?
nil)
(("2" (expand "replaceTerm" -1)
(("2" (lift-if)
(("2" (prop)
(("1" (hide (-3 -4))
(("1" (rewrite "empty_0")
(("1" (replaces -1)
(("1"
(replaces -1)
(("1" (rewrite "empty_o_seq") nil nil))
nil))
nil))
nil))
nil)
("2" (expand "IUnion")
(("2" (skolem * "i1")
(("2" (expand "catenate")
(("2"
(skolem * "y1")
(("2"
(expand "member")
(("2"
(flatten)
(("2"
(inst -4 "rest(x!1)")
(("2"
(inst
-4
"q"
"args(s)(first(x!1) - 1)"
"t")
(("1"
(rewrite "length_rest")
(("1"
(assert)
(("1"
(lemma
"fsepn.seq_first_rest")
(("1"
(inst?)
(("1"
(assert)
(("1"
(replace -1 -4)
(("1"
(lemma
"fsepn.first_equal")
(("1"
(inst
-1
"rest(x!1)"
"y1"
"first(x!1)"
"i1")
(("1"
(assert)
(("1"
(flatten)
(("1"
(hide -6)
(("1"
(replace
-1
*
rl)
(("1"
(replace
-2
*
rl)
(("1"
(hide
(-1
-2))
(("1"
(decompose-equality
-2)
(("1"
(hide
-1)
(("1"
(copy
-1)
(("1"
(expand
"replace"
-1)
(("1"
(decompose-equality
-1)
(("1"
(hide
-2)
(("1"
(expand
"positionsOF"
4)
(("1"
(prop)
(("1"
(assert)
nil
nil)
("2"
(hide
-2)
(("2"
(expand*
"union"
"member")
(("2"
(prop)
(("2"
(expand
"IUnion")
(("2"
(inst
3
"first(x!1)")
(("1"
(expand
"catenate")
(("1"
(inst
3
"rest(x!1) o q")
(("1"
(prop)
(("1"
(expand
"member")
(("1"
(replace
-2
*
rl)
(("1"
(lemma
"fset.nth_x")
(("1"
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.49 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.
|
