|
(robinsonunification
(IMP_unification_TCC1 0
(IMP_unification_TCC1-1 nil 3467989055
("" (lemma var_countable) (("" (propax) nil nil)) nil)
((var_countable formula-decl nil robinsonunification nil)) nil))
(xx_TCC1 0
(xx_TCC1-1 nil 3468765193
("" (lemma var_nonempty)
(("" (expand* nonempty? empty?)
(("" (skosimp*)
(("" (inst 1 x!1)
(("" (assert)
(("" (expand member) (("" (propax) nil nil)) nil)) nil))
nil))
nil))
nil))
nil)
((empty? const-decl "bool" sets nil)
(nonempty? const-decl "bool" sets nil)
(variable formal-nonempty-type-decl nil robinsonunification nil)
(symbol formal-nonempty-type-decl nil robinsonunification 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]" robinsonunification nil)
(term type-decl nil term_adt nil) (set type-eq-decl nil sets nil)
(V const-decl "set[term]" variables_term nil)
(x!1 skolem-const-decl "term[variable, symbol, arity]"
robinsonunification nil)
(member const-decl "bool" sets nil)
(var_nonempty formula-decl nil robinsonunification nil))
nil))
(ff_TCC1 0
(ff_TCC1-1 nil 3474208611
("" (lemma symbol_nonempty)
(("" (expand* nonempty? empty?)
(("" (skosimp)
(("" (expand member) (("" (inst 1 x!1) nil nil)) nil)) nil))
nil))
nil)
((empty? const-decl "bool" sets nil)
(nonempty? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(x!1 skolem-const-decl "symbol" robinsonunification nil)
(arity formal-const-decl "[symbol -> nat]" robinsonunification 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)
(= const-decl "[T, T -> boolean]" equalities nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(symbol formal-nonempty-type-decl nil robinsonunification nil)
(symbol_nonempty formula-decl nil robinsonunification nil))
nil))
(fail_TCC1 0
(fail_TCC1-1 nil 3467989055
("" (typepred ff) (("" (assert) (("" (grind) nil nil)) nil)) nil)
((term type-decl nil term_adt nil)
(variable formal-nonempty-type-decl nil robinsonunification nil)
(|#| const-decl "finite_sequence[T]" set2seq "structures/")
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(symbol formal-nonempty-type-decl nil robinsonunification 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]" robinsonunification nil)
(ff const-decl "{f: symbol | arity(f) = 1}" robinsonunification
nil))
nil))
(fail_TCC2 0
(fail_TCC2-1 nil 3474208611
("" (expand Sub?)
((""
(case-replace "Dom((id[(V)]
WITH [xx
:= app[variable, symbol, arity]
(ff,
#[term[variable, symbol, arity]]
(xx))])) = singleton(xx)")
(("1" (hide -1) (("1" (rewrite finite_singleton) nil nil)) nil)
("2" (hide 2)
(("2" (decompose-equality)
(("2" (iff)
(("2" (prop)
(("1" (expand singleton)
(("1" (expand Dom)
(("1" (flatten)
(("1" (expand id) (("1" (grind) nil nil)) nil))
nil))
nil))
nil)
("2" (expand* singleton Dom)
(("2" (flatten)
(("2" (grind)
(("2" (replaces -1)
(("2" (typepred xx)
(("2" (expand V) (("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((nonempty_singleton_finite application-judgement
"non_empty_finite_set" robinsonunification nil)
(nonempty_singleton_finite application-judgement
"non_empty_finite_set[term]" robinsonunification nil)
(variable formal-nonempty-type-decl nil robinsonunification nil)
(symbol formal-nonempty-type-decl nil robinsonunification 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]" robinsonunification 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)
(id const-decl "(bijective?[T, T])" identity nil)
(below type-eq-decl nil nat_types nil)
(finite_sequence type-eq-decl nil finite_sequences 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)
(ff const-decl "{f: symbol | arity(f) = 1}" robinsonunification
nil)
(|#| const-decl "finite_sequence[T]" set2seq "structures/")
(xx const-decl "(V)" robinsonunification nil)
(singleton? const-decl "bool" sets nil)
(singleton const-decl "(singleton?)" sets nil)
(finite_singleton judgement-tcc nil finite_sets nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(Sub? const-decl "bool" substitution nil))
nil))
(first_diff_TCC1 0
(first_diff_TCC1-1 nil 3467989055
("" (skosimp*)
(("" (lemma "positions_of_arg")
(("" (inst -1 "s!1" "k!1")
(("1" (typepred "k!1")
(("1" (typepred st!1)
(("1" (typepred stp!1)
(("1" (replace -4 1) (("1" (assert) nil nil)) nil)) nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil)
((arity formal-const-decl "[symbol -> nat]" robinsonunification 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 robinsonunification nil)
(variable formal-nonempty-type-decl nil robinsonunification nil)
(positions_of_arg formula-decl nil positions nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(fp!1 skolem-const-decl "symbol" robinsonunification nil)
(stp!1 skolem-const-decl
"{args: finite_sequence[term[variable, symbol, arity]] |
args`length = arity(fp!1)}" robinsonunification nil)
(k!1 skolem-const-decl "below[length(stp!1)]" robinsonunification
nil)
(s!1 skolem-const-decl "term[variable, symbol, arity]"
robinsonunification 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)
(below type-eq-decl nil nat_types nil)
(< const-decl "bool" reals nil)
(app? adt-recognizer-decl "[term -> boolean]" term_adt nil)
(term type-decl nil term_adt nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
nil))
(first_diff_TCC2 0
(first_diff_TCC2-1 nil 3467989055
("" (skosimp*)
(("" (lemma "positions_of_arg")
(("" (inst -1 "t!1" "k!1")
(("1" (typepred st!1)
(("1" (typepred stp!1)
(("1" (replace -5 1) (("1" (assert) nil nil)) nil)) nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil)
((arity formal-const-decl "[symbol -> nat]" robinsonunification 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 robinsonunification nil)
(variable formal-nonempty-type-decl nil robinsonunification nil)
(positions_of_arg formula-decl nil positions nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(fp!1 skolem-const-decl "symbol" robinsonunification nil)
(stp!1 skolem-const-decl
"{args: finite_sequence[term[variable, symbol, arity]] |
args`length = arity(fp!1)}" robinsonunification nil)
(k!1 skolem-const-decl "below[length(stp!1)]" robinsonunification
nil)
(s!1 skolem-const-decl "term[variable, symbol, arity]"
robinsonunification nil)
(t!1 skolem-const-decl "{t: term | s!1 /= t}" robinsonunification
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)
(below type-eq-decl nil nat_types nil)
(< const-decl "bool" reals nil)
(/= const-decl "boolean" notequal nil)
(app? adt-recognizer-decl "[term -> boolean]" term_adt nil)
(term type-decl nil term_adt nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
nil))
(first_diff_TCC3 0
(first_diff_TCC3-1 nil 3467989055
("" (skosimp*) (("" (assert) nil nil)) nil)
((nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil))
nil))
(first_diff_TCC4 0
(first_diff_TCC4-1 nil 3467989055
("" (skosimp*)
(("" (expand "<<")
(("" (lift-if)
(("" (prop)
(("1" (hide-all-but (-1 -2)) (("1" (assert) nil nil)) nil)
("2" (inst 2 k!1)
(("1" (assert) (("1" (grind) nil nil)) nil)
("2" (replace -1 1) (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((<< adt-def-decl "(strict_well_founded?[term])" term_adt nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(int_min application-judgement "{k: int | k <= i AND k <= j}"
real_defs nil)
(nat_min application-judgement "{k: nat | k <= i AND k <= j}"
real_defs nil)
(real_gt_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)
(subterm adt-def-decl "boolean" term_adt nil)
(subtermOF def-decl "term" subterm nil)
(rest const-decl "finseq" seq_extras "structures/")
(^ const-decl "finseq" finite_sequences nil)
(empty_seq const-decl "finseq" finite_sequences nil)
(first const-decl "T" seq_extras "structures/")
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil)
(|#| const-decl "finite_sequence[T]" set2seq "structures/")
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(posnat nonempty-type-eq-decl nil integers nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers 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)
(bool nonempty-type-eq-decl nil booleans nil)
(< const-decl "bool" 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)
(below type-eq-decl nil nat_types nil)
(variable formal-nonempty-type-decl nil robinsonunification nil)
(symbol formal-nonempty-type-decl nil robinsonunification nil)
(arity formal-const-decl "[symbol -> nat]" robinsonunification nil)
(term type-decl nil term_adt nil)
(finite_sequence type-eq-decl nil finite_sequences nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(fp!1 skolem-const-decl "symbol" robinsonunification nil)
(stp!1 skolem-const-decl
"{args: finite_sequence[term[variable, symbol, arity]] |
args`length = arity(fp!1)}" robinsonunification nil)
(k!1 skolem-const-decl "below[length(stp!1)]" robinsonunification
nil)
(app? adt-recognizer-decl "[term -> boolean]" term_adt 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)
(s!1 skolem-const-decl "term[variable, symbol, arity]"
robinsonunification nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
nil))
(first_diff_TCC5 0
(first_diff_TCC5-1 nil 3468147562
("" (skosimp*)
(("" (lemma "positions_of_arg")
(("" (inst -1 "s!1" "kk!1")
(("1" (replace -1 1) (("1" (assert) nil nil)) nil)
("2" (assert) nil nil))
nil))
nil))
nil)
((arity formal-const-decl "[symbol -> nat]" robinsonunification 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 robinsonunification nil)
(variable formal-nonempty-type-decl nil robinsonunification nil)
(positions_of_arg formula-decl nil positions nil)
(fp!1 skolem-const-decl "symbol" robinsonunification nil)
(stp!1 skolem-const-decl
"{args: finite_sequence[term[variable, symbol, arity]] |
args`length = arity(fp!1)}" robinsonunification nil)
(kk!1 skolem-const-decl "below[length(stp!1)]" robinsonunification
nil)
(s!1 skolem-const-decl "term[variable, symbol, arity]"
robinsonunification 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)
(below type-eq-decl nil nat_types nil)
(< const-decl "bool" reals nil)
(app? adt-recognizer-decl "[term -> boolean]" term_adt nil)
(term type-decl nil term_adt nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
nil))
(first_diff_TCC6 0
(first_diff_TCC6-1 nil 3516387399
("" (skosimp*)
(("" (lemma "positions_of_arg")
(("" (inst -1 "t!1" "kk!1")
(("1" (typepred "kk!1")
(("1" (replace -4 1) (("1" (assert) nil nil)) nil)) nil)
("2" (assert) nil nil))
nil))
nil))
nil)
((arity formal-const-decl "[symbol -> nat]" robinsonunification 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 robinsonunification nil)
(variable formal-nonempty-type-decl nil robinsonunification nil)
(positions_of_arg formula-decl nil positions nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(fp!1 skolem-const-decl "symbol" robinsonunification nil)
(stp!1 skolem-const-decl
"{args: finite_sequence[term[variable, symbol, arity]] |
args`length = arity(fp!1)}" robinsonunification nil)
(kk!1 skolem-const-decl "below[length(stp!1)]" robinsonunification
nil)
(s!1 skolem-const-decl "term[variable, symbol, arity]"
robinsonunification nil)
(t!1 skolem-const-decl "{t: term | s!1 /= t}" robinsonunification
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)
(below type-eq-decl nil nat_types nil)
(< const-decl "bool" reals nil)
(/= const-decl "boolean" notequal nil)
(app? adt-recognizer-decl "[term -> boolean]" term_adt nil)
(term type-decl nil term_adt nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
nil))
(first_diff_TCC7 0
(first_diff_TCC7-1 nil 3516387399
("" (skosimp*)
(("" (case "st!1 = stp!1")
(("1" (hide +) (("1" (grind) nil nil)) nil)
("2" (decompose-equality 1)
(("2" (decompose-equality 1)
(("2" (typepred x!1)
(("2" (expand* "nonempty?" "empty?")
(("2" (inst -5 "x!1")
(("2" (expand "member")
(("2" (replace -2 -5)
(("2" (replace -4 -5)
(("2" (assert)
(("2" (expand subtermOF)
(("2" (lift-if)
(("2" (assert) (("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((= const-decl "[T, T -> boolean]" equalities nil)
(finite_sequence type-eq-decl nil finite_sequences nil)
(term type-decl nil term_adt nil)
(arity formal-const-decl "[symbol -> nat]" robinsonunification 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 robinsonunification nil)
(variable formal-nonempty-type-decl nil robinsonunification nil)
(below type-eq-decl nil nat_types nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(< const-decl "bool" reals nil) (empty? const-decl "bool" sets nil)
(nonempty? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(subtermOF def-decl "term" subterm 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 "finite_sequence[T]" set2seq "structures/")
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil)
(first const-decl "T" seq_extras "structures/")
(empty_seq const-decl "finseq" finite_sequences nil)
(^ const-decl "finseq" finite_sequences nil)
(rest const-decl "finseq" seq_extras "structures/")
(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)
(nat_min application-judgement "{k: nat | k <= i AND k <= j}"
real_defs nil)
(int_min application-judgement "{k: int | k <= i AND k <= j}"
real_defs nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(NOT const-decl "[bool -> bool]" booleans nil))
nil))
(comutative_first_diff_TCC1 0
(comutative_first_diff_TCC1-1 nil 3468654719
("" (skosimp) (("" (typepred "t!1") (("" (assert) nil nil)) nil))
nil)
((/= const-decl "boolean" notequal nil)
(term type-decl nil term_adt nil)
(arity formal-const-decl "[symbol -> nat]" robinsonunification 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 robinsonunification nil)
(variable formal-nonempty-type-decl nil robinsonunification nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
nil))
(comutative_first_diff 0
(comutative_first_diff-1 nil 3468654726
("" (measure-induct+ "length(p)" "p")
(("" (skosimp)
(("" (expand "first_diff" -2)
(("" (lift-if)
(("" (assert)
((""
(name-replace "k!11"
"min({kk: below[length(args(t!1))] | NOT
subtermOF(s!1, #(1 + kk)) = subtermOF (t!1, #(1 + kk))})"
:hide? nil)
(("1" (name-replace "k!1" "1 + k!11")
(("1" (prop)
(("1" (hide -3 -4)
(("1" (expand "first_diff" 1)
(("1" (assert)
(("1" (lift-if) (("1" (prop) nil nil)) nil))
nil))
nil))
nil)
("2" (hide -3 -4)
(("2" (expand "first_diff")
(("2" (assert)
(("2" (lift-if)
(("2" (prop)
(("2" (reveal -1) (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (assert)
(("3" (hide -4)
(("3" (expand "first_diff" 3)
(("3" (propax) nil nil)) nil))
nil))
nil)
("4"
(inst -4 "first_diff(subtermOF(s!1, #(k!1)),
subtermOF(t!1, #(k!1)))")
(("4"
(inst -4 "subtermOF(s!1, #(k!1))"
"subtermOF(t!1, #(k!1))")
(("4" (prop)
(("1" (expand "first_diff" 4)
(("1" (assert)
(("1"
(name-replace "k!22"
"min({kk: below[length(args(s!1))] | NOT
subtermOF(t!1, #(1 + kk)) = subtermOF(s!1, #(1 + kk))})"
:hide? nil)
(("1"
(name-replace "k!2" "1 + k!22")
(("1"
(reveal -4 -1)
(("1"
(replace -3 -1 rl)
(("1"
(replace -7 -2 rl)
(("1"
(hide (-3 -7))
(("1"
(case "k!1 = k!2")
(("1"
(replaces -1)
(("1" (assert) nil nil))
nil)
("2"
(case
"length(args(s!1))=length(args(t!1))")
(("1"
(replace -1)
(("1"
(assert)
(("1"
(replace -2 1 rl)
(("1"
(replace -3 1 rl)
(("1"
(assert)
(("1"
(name-replace
"myset"
" min({kk: below[length(args(s!1))] |
NOT subtermOF(t!1, #(1 + kk)) = subtermOF(s!1, #(1 + kk))})"
:hide?
nil)
(("1"
(rewrite
min_def)
(("1"
(rewrite
min_def)
(("1"
(hide-all-but
(-1 1))
(("1"
(expand
minimum?)
(("1"
(skosimp*)
(("1"
(inst
-1
x!2)
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but
(1
3
4
5))
(("2"
(lemma
first_diff_TCC7)
(("2"
(inst
-1
"s!1"
"t!1"
"f(s!1)"
"args(s!1)")
(("2"
(case
"s!1 = app(f(s!1), args(s!1))")
(("1"
(assert)
(("1"
(hide
-1)
(("1"
(inst
-1
"f(t!1)"
"args(t!1)")
(("1"
(case
"t!1 = app(f(t!1), args(t!1))")
(("1"
(assert)
nil
nil)
("2"
(hide-all-but
(1
3))
(("2"
(decompose-equality)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but
(1
5))
(("2"
(decompose-equality)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("3"
(hide-all-but
(-6
1
3
4
5))
(("3"
(skosimp*)
(("3"
(lemma
"positions_of_arg")
(("3"
(inst
-1
"t!1"
"kk!1")
(("3"
(assert)
nil
nil))
nil))
nil))
nil))
nil)
("4"
(hide
-
6)
(("4"
(skosimp*)
(("4"
(lemma
"positions_of_arg")
(("4"
(inst
-1
"s!1"
"kk!1")
(("4"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but
(-6
1
3
4
5))
(("2"
(lemma
first_diff_TCC7)
(("2"
(inst
-1
"t!1"
"s!1"
"f(t!1)"
"args(t!1)")
(("2"
(case
"t!1 = app(f(t!1), args(t!1))")
(("1"
(assert)
(("1"
(hide
-1)
(("1"
(inst
-1
"f(s!1)"
"args(s!1)")
(("1"
(case
"s!1 = app(f(s!1), args(s!1))")
(("1"
(assert)
nil
nil)
("2"
(hide-all-but
(1
5))
(("2"
(decompose-equality)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but
(1
3))
(("2"
(decompose-equality)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("3"
(hide-all-but
(-6
1
3
4
5))
(("3"
(skosimp*)
(("3"
(lemma
"positions_of_arg")
(("3"
(inst
-1
"s!1"
"kk!1")
(("3"
(assert)
nil
nil))
nil))
nil))
nil))
nil)
("4"
(hide - 6)
(("4"
(skosimp*)
(("4"
(lemma
"positions_of_arg")
(("4"
(inst
-1
"t!1"
"kk!1")
(("4"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but
(-5
1
3
4
5))
(("2"
(lemma
first_diff_TCC7)
(("2"
(inst
-1
"t!1"
"s!1"
"f(t!1)"
"args(t!1)")
(("2"
(case
"t!1 = app(f(t!1), args(t!1))")
(("1"
(assert)
(("1"
(hide
-1)
(("1"
(inst
-1
"f(s!1)"
"args(s!1)")
(("1"
(case
"s!1 = app(f(s!1), args(s!1))")
(("1"
(assert)
nil
nil)
("2"
(hide-all-but
(1
5))
(("2"
(decompose-equality)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but
(1
3))
(("2"
(decompose-equality)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("3"
(hide
-
(2 6))
(("3"
(skosimp*)
(("3"
(lemma
"positions_of_arg")
(("3"
(inst
-1
"s!1"
"kk!1")
(("3"
(assert)
nil
nil))
nil))
nil))
nil))
nil)
("4"
(hide
-
(2 6))
(("4"
(skosimp*)
(("4"
(lemma
"positions_of_arg")
(("4"
(inst
-1
"t!1"
"kk!1")
(("4"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but (-4 1))
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but (-2 1 2 3 4))
(("2"
(lemma first_diff_TCC7)
(("2"
(inst
-1
"t!1"
"s!1"
"f(t!1)"
"args(t!1)")
(("2"
(case
"t!1 = app(f(t!1), args(t!1))")
(("1"
(assert)
(("1"
(hide -1)
(("1"
(inst
-1
"f(s!1)"
"args(s!1)")
(("1"
(case
"s!1 = app(f(s!1), args(s!1))")
(("1" (assert) nil nil)
("2"
(hide-all-but (1 5))
(("2"
(decompose-equality)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but (1 3))
(("2"
(decompose-equality)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("3"
(hide-all-but (-2 1 2 3 4))
(("3"
(skosimp*)
(("3"
(lemma "positions_of_arg")
(("3"
(inst -1 "s!1" "kk!1")
(("3" (assert) nil nil))
nil))
nil))
nil))
nil)
("4"
(hide - 5)
(("4"
(skosimp*)
(("4"
(lemma "positions_of_arg")
(("4"
(inst -1 "t!1" "kk!1")
(("4" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but (-2 1))
(("2" (expand* "add_first" "insert?")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
("5" (hide -2 -3)
(("5" (expand "first_diff")
(("5" (assert) nil nil)) nil))
nil))
nil))
nil)
("2" (prop)
(("1" (hide -3 1)
(("1" (expand "first_diff")
(("1" (assert)
(("1" (lift-if) (("1" (prop) nil nil)) nil))
nil))
nil))
nil)
("2" (hide -3 2)
(("2" (expand "first_diff")
(("2" (assert)
(("2" (lift-if)
(("2" (prop) (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
("3" (hide -3 3)
(("3" (expand "first_diff") (("3" (assert) nil nil))
nil))
nil)
("4" (hide - 5)
(("4" (lemma "first_diff_TCC7")
(("4" (inst -1 "s!1" "t!1" "f(s!1)" "args(s!1)")
(("4" (case "s!1 = app(f(s!1), args(s!1))")
(("1" (assert)
(("1" (hide -1)
(("1" (inst -1 "f(t!1)" "args(t!1)")
(("1"
(case "t!1 = app(f(t!1), args(t!1))")
(("1"
(assert)
(("1"
(reveal -4)
(("1" (propax) nil nil))
nil))
nil)
("2"
(hide-all-but (1 2))
(("2" (decompose-equality) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but (1 4))
(("2" (decompose-equality) nil nil)) nil))
nil))
nil))
nil))
nil)
("5" (hide -2 5)
(("5" (expand "first_diff") (("5" (assert) nil nil))
nil))
nil))
nil)
("3" (prop)
(("1" (hide -3 1)
(("1" (expand "first_diff")
(("1" (assert)
(("1" (lift-if) (("1" (prop) nil nil)) nil))
nil))
nil))
nil)
("2" (hide -3 2)
(("2" (expand "first_diff")
(("2" (lift-if)
(("2" (prop) (("2" (assert) nil nil)) nil)) nil))
nil))
nil)
("3" (hide -3 3)
(("3" (expand "first_diff") (("3" (assert) nil nil))
nil))
nil)
("4" (hide -2 -3 5)
(("4" (skosimp*)
(("4" (lemma "positions_of_arg")
(("4" (inst -1 "t!1" "kk!1")
(("4" (assert) nil nil)) nil))
nil))
nil))
nil)
("5" (hide -)
(("5" (skosimp*)
(("5" (lemma "positions_of_arg")
(("5" (inst -1 "t!1" "kk!1")
(("5" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
--> --------------------
--> maximum size reached
--> --------------------
[ zur Elbe Produktseite wechseln0.58Quellennavigators
Analyse erneut starten
]
|
