|
(substitution
(Ren?_TCC1 0
(Ren?_TCC1-1 nil 3414773644
("" (skolem-typepred)
(("" (flatten)
(("" (skolem-typepred)
(("" (hide -4)
(("" (expand* "Ran" "member") (("" (inst 1 "x1!1") nil nil))
nil))
nil))
nil))
nil))
nil)
((Ran const-decl "set[term]" substitution nil)
(member const-decl "bool" sets nil)
(Dom const-decl "set[(V)]" 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) (term type-decl nil term_adt nil)
(arity formal-const-decl "[symbol -> nat]" substitution 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 substitution nil)
(variable formal-nonempty-type-decl nil substitution nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
nil))
(range_finite 0
(range_finite-1 nil 3415026692
("" (skolem-typepred)
(("" (expand* "Sub?" "Ren?" "subset?" "member")
(("" (flatten)
((""
(lemma
"function_inverse_def[(Dom(rho!1)), (Ran(rho!1))].bijective_inverse_exists")
(("" (inst -1 "rho!1")
(("" (expand "exists1")
(("" (flatten)
(("" (hide -2)
(("" (skosimp*)
((""
(lemma
"function_inverse_def[(Dom(rho!1)), (Ran(rho!1))].bij_inv_is_bij_alt")
(("" (inst -1 "rho!1" "x!1")
(("" (expand "bijective?" -1)
(("" (flatten)
(("" (expand "is_finite")
((""
(skolem-typepred)
((""
(inst 1 "N!1" "f!1 o x!1")
((""
(lemma
"function_props[(Ran(rho!1)), (Dom(rho!1)), below[N!1]].composition_injective")
(("" (inst?) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((member const-decl "bool" sets nil)
(subset? const-decl "bool" sets nil)
(Ran const-decl "set[term]" substitution nil)
(Dom const-decl "set[(V)]" substitution nil)
(bijective_inverse_exists formula-decl nil function_inverse_def
nil)
(exists1 const-decl "bool" exists1 nil)
(bij_inv_is_bij_alt formula-decl nil function_inverse_def nil)
(is_finite const-decl "bool" finite_sets nil)
(O const-decl "T3" function_props nil)
(below type-eq-decl nil nat_types nil)
(< const-decl "bool" reals nil)
(f!1 skolem-const-decl "[(Dom(rho!1)) -> below[N!1]]" substitution
nil)
(N!1 skolem-const-decl "nat" substitution nil)
(injective? const-decl "bool" functions nil)
(composition_injective judgement-tcc nil function_props nil)
(x!1 skolem-const-decl "[(Ran(rho!1)) -> (Dom(rho!1))]"
substitution nil)
(inverse? const-decl "bool" function_inverse_def nil)
(restrict const-decl "R" restrict nil)
(bijective? const-decl "bool" functions nil)
(rho!1 skolem-const-decl "Ren" substitution nil)
(Ren type-eq-decl nil substitution nil)
(Ren? const-decl "bool" 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) (term type-decl nil term_adt nil)
(arity formal-const-decl "[symbol -> nat]" substitution 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 substitution nil)
(variable formal-nonempty-type-decl nil substitution nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
shostak))
(exists_var 0
(exists_var-1 nil 3414319958
("" (skolem-typepred)
(("" (case "NOT empty?(complement(union(V1!1, V2!1)))")
(("1" (lemma "choose_member")
(("1" (inst -1 "complement(union(V1!1, V2!1))")
(("1" (prop)
(("1" (expand "member")
(("1" (expand "extend" -1 1)
(("1" (prop)
(("1" (expand "complement" -2 1)
(("1" (expand "member") (("1" (inst?) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "empty?")
(("2" (skosimp*)
(("2" (inst?)
(("2" (expand "member")
(("2" (expand "extend") (("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 1)
(("2" (lemma "var_countable")
(("2"
(case-replace
"complement(union(V1!1, V2!1)) = difference(V, union(V1!1, V2!1))"
:hide? T)
(("1"
(lemma
"countable_props[term].countably_infinite_difference")
(("1" (inst -1 "V" "union(V1!1, V2!1)")
(("1" (grind) nil nil)) nil))
nil)
("2" (hide-all-but 1)
(("2" (decompose-equality 1)
(("2" (iff)
(("2" (prop)
(("1" (expand "restrict")
(("1"
(expand* "complement" "difference" "union"
"member")
(("1" (expand "extend")
(("1" (propax) nil nil)) nil))
nil))
nil)
("2"
(expand* "restrict" "complement" "difference"
"union" "member" "extend")
nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((union const-decl "set" sets nil)
(complement const-decl "set" sets nil)
(empty? const-decl "bool" sets nil)
(finite_union application-judgement "finite_set[(V)]" substitution
nil)
(extend const-decl "R" extend nil)
(FALSE const-decl "bool" booleans nil)
(member const-decl "bool" sets nil)
(choose const-decl "(p)" sets nil)
(nonempty? const-decl "bool" sets nil)
(choose_member formula-decl nil sets_lemmas nil)
(var_countable formula-decl nil substitution nil)
(countably_infinite_difference judgement-tcc nil countable_props
"sets_aux/")
(injective? const-decl "bool" functions nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(surjective? const-decl "bool" functions nil)
(V2!1 skolem-const-decl "finite_set[(V)]" substitution nil)
(x!1 skolem-const-decl "(V)" substitution nil)
(V1!1 skolem-const-decl "finite_set[(V)]" substitution nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(bijective? const-decl "bool" functions nil)
(countably_infinite_set type-eq-decl nil countability "sets_aux/")
(is_countably_infinite const-decl "bool" countability "sets_aux/")
(difference const-decl "set" sets nil)
(restrict const-decl "R" restrict nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(finite_extend application-judgement "finite_set[T]"
extend_set_props nil)
(finite_set type-eq-decl nil finite_sets nil)
(is_finite const-decl "bool" finite_sets nil)
(V const-decl "set[term]" variables_term nil)
(set type-eq-decl nil sets nil) (term type-decl nil term_adt nil)
(arity formal-const-decl "[symbol -> nat]" substitution 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 substitution nil)
(variable formal-nonempty-type-decl nil substitution nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
shostak))
(restriction_Dom 0
(restriction_Dom-1 nil 3411923200
("" (skeep)
(("" (expand* "subset?" "member" "Dom" "restriction")
(("" (skeep) (("" (lift-if) (("" (assert) nil nil)) nil)) nil))
nil))
nil)
((member const-decl "bool" sets nil)
(restriction const-decl "term" substitution nil)
(Dom const-decl "set[(V)]" substitution nil)
(subset? const-decl "bool" sets nil))
shostak))
(restriction_Dom_fin 0
(restriction_Dom_fin-1 nil 3411923327
("" (skeep)
(("" (lemma "restriction_Dom")
(("" (inst?)
(("" (lemma "fsetvar.finite_subset")
(("" (typepred "sigma")
(("" (expand "Sub?")
(("" (inst?)
(("" (lemma "fsetvar.finite_subset")
(("" (inst?) (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((restriction_Dom formula-decl nil substitution nil)
(finite_subset formula-decl nil finite_sets nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(restriction const-decl "term" substitution nil)
(finite_set type-eq-decl nil finite_sets nil)
(is_finite const-decl "bool" finite_sets nil)
(Dom const-decl "set[(V)]" substitution nil)
(sigma skolem-const-decl "Sub" substitution nil)
(NOT const-decl "[bool -> bool]" booleans 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) (term type-decl nil term_adt nil)
(arity formal-const-decl "[symbol -> nat]" substitution 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 substitution nil)
(variable formal-nonempty-type-decl nil substitution nil))
shostak))
(restriction_Subs 0
(restriction_Subs-1 nil 3411923411
("" (skeep)
(("" (lemma "restriction_Dom_fin")
(("" (inst?) (("" (expand "Sub?") (("" (propax) nil nil)) nil))
nil))
nil))
nil)
((restriction_Dom_fin formula-decl nil 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) (term type-decl nil term_adt nil)
(arity formal-const-decl "[symbol -> nat]" substitution 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 substitution nil)
(variable formal-nonempty-type-decl nil substitution nil))
shostak))
(dom_restriction 0
(dom_restriction-1 nil 3411923505
("" (skeep)
(("" (expand* "subset?" "member")
(("" (skeep)
(("" (expand "Dom")
(("" (expand "restriction")
(("" (lift-if)
(("" (prop)
(("" (expand "member") (("" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((member const-decl "bool" sets nil)
(subset? const-decl "bool" sets nil)
(Dom const-decl "set[(V)]" substitution nil)
(restriction const-decl "term" substitution nil))
shostak))
(Dom_union 0
(Dom_union-1 nil 3400451836
("" (skeep)
(("" (decompose-equality)
(("" (expand* "Dom" "union_subs" "union" "member")
(("" (lift-if)
(("" (expand "Dom") (("" (propax) nil nil)) nil)) nil))
nil))
nil))
nil)
((Dom const-decl "set[(V)]" substitution nil)
(Sub? const-decl "bool" substitution nil)
(Sub type-eq-decl nil substitution nil)
(disjoint_D? const-decl "bool" substitution nil)
(disjoint_D type-eq-decl nil substitution nil)
(union_subs const-decl "term" substitution nil)
(union const-decl "set" sets nil)
(V const-decl "set[term]" variables_term nil)
(set type-eq-decl nil sets nil) (term type-decl nil term_adt nil)
(arity formal-const-decl "[symbol -> nat]" substitution 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 substitution nil)
(variable formal-nonempty-type-decl nil substitution nil)
(member const-decl "bool" sets nil))
shostak))
(union_is_sub 0
(union_is_sub-1 nil 3400459156
("" (skeep)
(("" (typepred "sgi`1" "sgi`2")
(("" (expand "Sub?")
(("" (lemma "fsetvar.finite_union")
(("" (inst -1 "Dom(sgi`1)" "Dom(sgi`2)")
(("" (lemma "Dom_union")
(("" (inst?) (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil)
((disjoint_D type-eq-decl nil substitution nil)
(disjoint_D? const-decl "bool" 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) (term type-decl nil term_adt nil)
(arity formal-const-decl "[symbol -> nat]" substitution 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 substitution nil)
(variable formal-nonempty-type-decl nil substitution nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(finite_union judgement-tcc nil finite_sets nil)
(Dom_union formula-decl nil substitution nil)
(finite_set type-eq-decl nil finite_sets nil)
(is_finite const-decl "bool" finite_sets nil)
(Dom const-decl "set[(V)]" substitution nil)
(sgi skolem-const-decl "disjoint_D" substitution nil))
shostak))
(union_commute_TCC1 0
(union_commute_TCC1-1 nil 3402055579 ("" (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)
(variable formal-nonempty-type-decl nil substitution nil)
(symbol formal-nonempty-type-decl nil substitution 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)
(arity formal-const-decl "[symbol -> nat]" substitution 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)
(/= const-decl "boolean" notequal nil)
(Dom const-decl "set[(V)]" substitution nil)
(member const-decl "bool" sets nil)
(intersection const-decl "set" sets nil)
(empty? const-decl "bool" sets nil)
(disjoint? const-decl "bool" sets nil)
(disjoint_D? const-decl "bool" substitution nil))
nil))
(union_commute_TCC2 0
(union_commute_TCC2-1 nil 3402055579 ("" (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)
(variable formal-nonempty-type-decl nil substitution nil)
(symbol formal-nonempty-type-decl nil substitution 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)
(arity formal-const-decl "[symbol -> nat]" substitution 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)
(is_finite const-decl "bool" finite_sets nil)
(injective? const-decl "bool" functions nil)
(/= const-decl "boolean" notequal nil)
(Dom const-decl "set[(V)]" substitution nil)
(member const-decl "bool" sets nil)
(intersection const-decl "set" sets nil)
(empty? const-decl "bool" sets nil)
(disjoint? const-decl "bool" sets nil)
(disjoint_D? const-decl "bool" substitution nil))
nil))
(union_commute 0
(union_commute-1 nil 3402055580
("" (skeep)
(("" (decompose-equality)
(("" (expand "union_subs")
(("" (lift-if)
(("" (lift-if)
(("" (prop)
(("" (expand* "disjoint?" "empty?" "intersection")
(("" (inst?)
(("" (expand "member" 2 1) (("" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((Sub? const-decl "bool" substitution nil)
(Sub type-eq-decl nil substitution nil)
(disjoint_D? const-decl "bool" substitution nil)
(disjoint_D type-eq-decl nil substitution nil)
(union_subs const-decl "term" substitution nil)
(V const-decl "set[term]" variables_term nil)
(set type-eq-decl nil sets nil) (term type-decl nil term_adt nil)
(arity formal-const-decl "[symbol -> nat]" substitution 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 substitution nil)
(variable formal-nonempty-type-decl nil substitution nil)
(member const-decl "bool" sets nil)
(disjoint? const-decl "bool" sets nil)
(intersection const-decl "set" sets nil)
(empty? const-decl "bool" sets nil))
shostak))
(ext_TCC1 0
(ext_TCC1-1 nil 3391263310 ("" (subtype-tcc) nil nil)
((NOT const-decl "[bool -> bool]" booleans nil)
(term type-decl nil term_adt nil) (set type-eq-decl nil sets nil)
(Sub? const-decl "bool" substitution nil)
(Sub type-eq-decl nil substitution nil)
(is_finite const-decl "bool" finite_sets nil)
(injective? const-decl "bool" functions nil)
(arity formal-const-decl "[symbol -> nat]" substitution 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 substitution nil)
(variable formal-nonempty-type-decl nil substitution nil)
(V const-decl "set[term]" variables_term nil))
nil))
(ext_TCC2 0
(ext_TCC2-1 nil 3391263310 ("" (termination-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)
(variable formal-nonempty-type-decl nil substitution nil)
(symbol formal-nonempty-type-decl nil substitution 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)
(arity formal-const-decl "[symbol -> nat]" substitution 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)
(= const-decl "[T, T -> boolean]" equalities nil)
(below type-eq-decl nil nat_types nil)
(finite_sequence type-eq-decl nil finite_sequences nil)
(injective? const-decl "bool" functions nil)
(is_finite const-decl "bool" finite_sets nil)
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil))
nil))
(ext_TCC3 0
(ext_TCC3-1 nil 3391263310 ("" (termination-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)
(variable formal-nonempty-type-decl nil substitution nil)
(symbol formal-nonempty-type-decl nil substitution 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)
(arity formal-const-decl "[symbol -> nat]" substitution 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)
(= const-decl "[T, T -> boolean]" equalities nil)
(below type-eq-decl nil nat_types nil)
(finite_sequence type-eq-decl nil finite_sequences nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(injective? const-decl "bool" functions nil)
(is_finite const-decl "bool" finite_sets nil)
(subterm adt-def-decl "boolean" term_adt nil)
(<< adt-def-decl "(strict_well_founded?[term])" term_adt nil)
(< const-decl "bool" reals nil)
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil))
nil))
(iden_subs 0
(iden_subs-1 nil 3397944522
("" (expand "Sub?")
(("" (case-replace "Dom(identity) = emptyset")
(("1" (assert) nil nil)
("2" (hide 2)
(("2" (expand* "Dom" "identity" "emptyset") nil nil)) nil))
nil))
nil)
((finite_emptyset name-judgement "finite_set" finite_sets nil)
(finite_emptyset name-judgement "finite_set" substitution nil)
(variable formal-nonempty-type-decl nil substitution nil)
(symbol formal-nonempty-type-decl nil substitution 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]" substitution nil)
(term type-decl nil term_adt nil) (set type-eq-decl nil sets nil)
(V const-decl "set[term]" variables_term nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(Dom const-decl "set[(V)]" substitution nil)
(bijective? const-decl "bool" functions nil)
(identity const-decl "(bijective?[T, T])" identity nil)
(emptyset const-decl "set" sets nil)
(Sub? const-decl "bool" substitution nil))
shostak))
(iden_rename_TCC1 0
(iden_rename_TCC1-1 nil 3414771081 ("" (rewrite "iden_subs") nil nil)
((iden_subs formula-decl nil substitution nil)) nil))
(iden_rename 0
(iden_rename-1 nil 3414771211
("" (expand "Ren?")
(("" (expand "subset?")
(("" (skosimp*)
(("" (expand "member")
(("" (expand "Ran")
(("" (skosimp*)
(("" (typepred "identity") (("" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((subset? const-decl "bool" sets nil)
(Ran const-decl "set[term]" substitution nil)
(Dom const-decl "set[(V)]" substitution nil)
(restrict const-decl "R" restrict nil)
(surjective? const-decl "bool" functions nil)
(injective? const-decl "bool" functions nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(variable formal-nonempty-type-decl nil substitution nil)
(symbol formal-nonempty-type-decl nil substitution 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)
(arity formal-const-decl "[symbol -> nat]" substitution nil)
(term type-decl nil term_adt nil) (set type-eq-decl nil sets nil)
(V const-decl "set[term]" variables_term nil)
(bijective? const-decl "bool" functions nil)
(identity const-decl "(bijective?[T, T])" identity nil)
(member const-decl "bool" sets nil)
(Ren? const-decl "bool" substitution nil))
shostak))
(ext_iden 0
(ext_iden-1 nil 3391281937
("" (induct "t")
(("1" (skeep) (("1" (grind) nil nil)) nil)
("2" (skeep)
(("2" (decompose-equality 1)
(("1" (grind) nil nil)
("2" (decompose-equality 1)
(("1" (inst?) (("1" (grind) nil nil) ("2" (grind) nil nil))
nil)
("2" (decompose-equality 1)
(("2" (inst?) (("2" (grind) nil nil)) nil)) nil))
nil)
("3" (grind) nil nil))
nil))
nil)
("3" (rewrite "iden_subs") nil nil))
nil)
((iden_subs formula-decl nil substitution 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 "bool" reals nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil)
(app? adt-recognizer-decl "[term -> boolean]" term_adt nil)
(term_app_extensionality formula-decl nil term_adt nil)
(below type-eq-decl nil nat_types 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)
(app1_var skolem-const-decl "symbol" substitution nil)
(app2_var skolem-const-decl
"{args: finite_sequence[term[variable, symbol, arity]] |
args`length = arity(app1_var)}" substitution nil)
(identity_preserves application-judgement "S" identity_props nil)
(term_induction formula-decl nil term_adt nil)
(variable formal-nonempty-type-decl nil substitution nil)
(symbol formal-nonempty-type-decl nil substitution 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]" substitution nil)
(ext def-decl "term" substitution nil)
(Sub type-eq-decl nil substitution nil)
(= const-decl "[T, T -> boolean]" equalities 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))
(restriction_term_TCC1 0
(restriction_term_TCC1-1 nil 3411924525
("" (lemma "restriction_Subs")
(("" (skosimp*) (("" (inst?) nil nil)) nil)) nil)
((variable formal-nonempty-type-decl nil substitution nil)
(symbol formal-nonempty-type-decl nil substitution 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]" substitution 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)
(restriction_Subs formula-decl nil substitution nil))
nil))
(restriction_term 0
(restriction_term-1 nil 3411924525
("" (induct "t")
(("1" (skeep)
(("1" (skeep)
(("1" (expand "ext")
(("1" (expand "subset?")
(("1" (inst?)
(("1" (expand "restriction")
(("1" (lift-if)
(("1" (prop)
(("1" (hide 2)
(("1" (expand* "member" "Vars")
(("1" (inst 2 "empty_seq")
(("1" (expand "subtermOF")
(("1" (lift-if)
(("1" (rewrite "empty_0") nil nil)) nil))
nil)
("2" (expand "positionsOF")
(("2" (expand "only_empty_seq")
(("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skeep)
(("2" (skeep)
(("2" (expand "ext" 1)
(("2" (lift-if)
(("2" (prop)
(("2" (decompose-equality 2)
(("1" (decompose-equality 1)
(("1" (expand "finseq_appl")
(("1" (inst -1 "x!1")
(("1" (inst -1 "Vs" "sigma")
(("1" (assert)
(("1" (hide 1)
(("1" (expand "subset?")
(("1"
(skosimp*)
(("1"
(inst?)
(("1"
(assert)
(("1"
(hide 2)
(("1"
(expand "member")
(("1"
(expand "Vars")
(("1"
(skosimp*)
(("1"
(inst
2
"add_first(x!1 + 1, p!1)")
(("1"
(expand "subtermOF" 2)
(("1"
(lift-if)
(("1"
(prop)
(("1"
(hide-all-but -1)
(("1"
(grind)
nil
nil))
nil)
("2"
(lemma
"fsepn.rest_add_first")
(("2"
(expand
"finseq_appl")
(("2"
(inst
-1
"p!1"
"1 + x!1")
(("2"
(replaces
-1)
(("2"
(rewrite
"first_add")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand "positionsOF")
(("2"
(expand "union")
(("2"
(prop)
(("2"
(hide 1)
(("2"
(expand
"member")
(("2"
(expand
"IUnion")
(("2"
(typepred
"x!1")
(("2"
(inst
1
"x!1 + 1")
(("2"
(expand
"catenate")
(("2"
(inst
1
"p!1")
(("2"
(typepred
"p!1")
(("2"
(expand*
"finseq_appl"
"member")
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" (skosimp*)
(("2" (rewrite "restriction_Subs") nil nil)) nil))
nil)
("2" (skosimp*)
(("2" (rewrite "restriction_Subs") nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (skosimp*) (("3" (rewrite "restriction_Subs") nil nil)) nil))
nil)
((nnint_plus_posint_is_posint application-judgement "posint"
integers 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)
(x!1 skolem-const-decl "below[app2_var`length]" substitution nil)
(p!1 skolem-const-decl
"positions?[variable, symbol, arity](app2_var`seq(x!1))"
substitution nil)
(rest_add_first formula-decl nil seq_extras "structures/")
(first_add formula-decl nil seq_extras "structures/")
(int_minus_int_is_int application-judgement "int" integers nil)
(insert? const-decl "finseq" seq_extras "structures/")
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(union const-decl "set" sets nil)
(IUnion const-decl "set[T]" indexed_sets nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(upto? nonempty-type-eq-decl nil IUnion_extra nil)
(<= const-decl "bool" reals nil)
(catenate const-decl "positions" positions nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(restriction_Subs formula-decl nil substitution nil)
(app? adt-recognizer-decl "[term -> boolean]" term_adt nil)
(term_app_extensionality formula-decl nil term_adt nil)
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil)
(app adt-constructor-decl
"[[f: symbol, {args: finite_sequence[term] | args`length = arity(f)}] ->
(app?)]" term_adt nil)
(< const-decl "bool" reals nil)
(finite_sequence type-eq-decl nil finite_sequences nil)
(app1_var skolem-const-decl "symbol" substitution nil)
(app2_var skolem-const-decl
"{args: finite_sequence[term[variable, symbol, arity]] |
args`length = arity(app1_var)}" substitution nil)
(sigma skolem-const-decl "Sub" substitution nil)
(Vs skolem-const-decl "set[(V)]" substitution nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(vars adt-constructor-decl "[variable -> (vars?)]" term_adt nil)
(vars? adt-recognizer-decl "[term -> boolean]" term_adt 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)
(vars1_var skolem-const-decl "variable" substitution nil)
(finseq type-eq-decl nil finite_sequences nil)
(empty_seq const-decl "finseq" finite_sequences nil)
(positions? type-eq-decl nil positions nil)
(empty_0 formula-decl nil seq_extras "structures/")
(subtermOF def-decl "term" subterm nil)
(only_empty_seq const-decl "positions" positions nil)
(member const-decl "bool" sets nil)
(term_induction formula-decl nil term_adt nil)
(variable formal-nonempty-type-decl nil substitution nil)
(symbol formal-nonempty-type-decl nil substitution 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]" substitution nil)
(ext def-decl "term" substitution nil)
(= const-decl "[T, T -> boolean]" equalities 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)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(subset? const-decl "bool" sets nil)
(Vars const-decl "set[(V)]" subterm nil)
(restriction const-decl "term" substitution nil))
shostak))
(restriction_union_TCC1 0
(restriction_union_TCC1-1 nil 3411923193
("" (skosimp*) (("" (rewrite "union_is_sub") nil nil)) nil)
((union_is_sub formula-decl nil substitution nil)
(variable formal-nonempty-type-decl nil substitution nil)
(symbol formal-nonempty-type-decl nil substitution 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]" substitution 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)
(disjoint_D? const-decl "bool" substitution nil)
(disjoint_D type-eq-decl nil substitution nil))
nil))
(restriction_union 0
(restriction_union-1 nil 3411924894
("" (induct "t")
(("1" (skeep)
(("1" (skeep)
(("1" (expand "ext" 1 1)
(("1" (expand "disjoint?" -2)
(("1" (expand "empty?" -2)
(("1" (expand "union_subs")
(("1" (lift-if)
(("1" (expand "member")
(("1" (prop)
(("1" (expand "ext") (("1" (propax) nil nil))
nil)
("2" (inst -3 "vars(vars1_var)")
(("2" (expand* "intersection" "member")
(("2" (expand "Vars" 3)
(("2" (prop)
(("2"
(inst 1 "empty_seq")
(("1"
(expand "subtermOF")
(("1"
(lift-if)
(("1" (rewrite "empty_0") nil nil))
nil))
nil)
("2"
(expand "positionsOF")
(("2"
(expand "only_empty_seq")
(("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (expand "Dom" 3)
(("3" (prop)
(("3" (expand "ext") (("3" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skeep)
(("2" (skeep)
(("2" (expand "ext" 1)
(("2" (lift-if)
(("2" (prop)
(("2" (decompose-equality 2)
(("1" (decompose-equality 1)
(("1" (expand "finseq_appl")
(("1" (inst?)
(("1" (assert)
(("1" (hide 1)
(("1" (expand "disjoint?" (-2 2))
(("1" (expand "empty?" (-2 2))
(("1"
(skosimp*)
(("1"
(inst?)
(("1"
(expand* "intersection" "member")
(("1"
(prop)
(("1"
(expand "Vars")
(("1"
(skosimp*)
(("1"
(inst
1
"add_first(x!1 + 1, p!1)")
(("1"
(expand "subtermOF" 1)
(("1"
(lift-if)
(("1"
(prop)
(("1"
(hide-all-but -1)
(("1"
(grind)
nil
nil))
nil)
("2"
(lemma
"fsepn.rest_add_first")
(("2"
(inst
-1
"p!1"
"x!1 + 1")
(("2"
(rewrite
"first_add")
(("2"
(replaces -1)
(("2"
(expand
"finseq_appl")
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand "positionsOF")
(("2"
(expand "union")
(("2"
(prop)
(("2"
(hide 1)
(("2"
(expand "member")
(("2"
(expand
"IUnion")
(("2"
(typepred
"x!1")
(("2"
(inst
1
"x!1 + 1")
(("2"
(expand
"catenate")
(("2"
(inst
1
"p!1")
(("2"
(typepred
"p!1")
(("2"
(expand*
"finseq_appl"
"member")
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" (skosimp*)
(("2" (rewrite "union_is_sub") nil nil)) nil)
("3" (skeep)
(("3" (expand "disjoint_D?")
(("3" (propax) nil nil)) nil))
nil))
nil)
("2" (skeep) (("2" (rewrite "union_is_sub") nil nil))
nil)
("3" (skeep)
(("3" (expand "disjoint_D?") (("3" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (hide 2)
(("3" (skeep) (("3" (rewrite "union_is_sub") nil nil)) nil)) nil)
("4" (hide 2)
(("4" (skeep)
(("4" (expand "disjoint_D?") (("4" (propax) nil nil)) nil))
nil))
nil))
nil)
((NOT const-decl "[bool -> bool]" booleans nil)
(catenate const-decl "positions" positions 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)
(IUnion const-decl "set[T]" indexed_sets nil)
(union const-decl "set" sets nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(insert? const-decl "finseq" seq_extras "structures/")
(int_minus_int_is_int application-judgement "int" integers nil)
(first_add formula-decl nil seq_extras "structures/")
(rest_add_first formula-decl nil seq_extras "structures/")
(p!1 skolem-const-decl
"positions?[variable, symbol, arity](app2_var`seq(x!1))"
substitution nil)
(x!1 skolem-const-decl "below[app2_var`length]" substitution nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(add_first const-decl "finseq" seq_extras "structures/")
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(union_is_sub formula-decl nil substitution nil)
(app? adt-recognizer-decl "[term -> boolean]" term_adt nil)
(term_app_extensionality formula-decl nil term_adt nil)
(app adt-constructor-decl
"[[f: symbol, {args: finite_sequence[term] | args`length = arity(f)}] ->
(app?)]" term_adt nil)
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil)
(sg2 skolem-const-decl "Sub" substitution nil)
(sg1 skolem-const-decl "Sub" substitution nil)
(app2_var skolem-const-decl
"{args: finite_sequence[term[variable, symbol, arity]] |
args`length = arity(app1_var)}" substitution nil)
(app1_var skolem-const-decl "symbol" substitution nil)
(finite_sequence type-eq-decl nil finite_sequences nil)
(< const-decl "bool" reals nil) (empty? const-decl "bool" sets nil)
(intersection const-decl "set" sets nil)
(only_empty_seq const-decl "positions" positions nil)
(subtermOF def-decl "term" subterm nil)
(empty_0 formula-decl nil seq_extras "structures/")
(positions? type-eq-decl nil positions nil)
(empty_seq const-decl "finseq" finite_sequences nil)
(finseq type-eq-decl nil finite_sequences nil)
(vars1_var skolem-const-decl "variable" substitution 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)
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.165 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.
|
