SSL robinsonunification.prf
Interaktion und
(robinsonunificationnil 3467989055"" (lemma var_countable) (("" (propax) nil nil )) nil )nil robinsonunification nil )) nil ))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 )"bool" sets nil )"bool" sets nil )nil robinsonunification nil )nil robinsonunification nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"[symbol -> nat]" robinsonunification nil )nil term_adt nil ) (set type-eq-decl nil sets nil )"set[term]" variables_term nil )"term[variable, symbol, arity]" nil )"bool" sets nil )nil robinsonunification nil ))nil ))nil 3474208611"" (lemma symbol_nonempty)"" (expand * nonempty? empty?)"" (skosimp)"" (expand member) (("" (inst 1 x!1) nil nil )) nil )) nil ))nil ))nil )"bool" sets nil )"bool" sets nil )"bool" sets nil )"symbol" robinsonunification nil )"[symbol -> nat]" robinsonunification nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )"[T, T -> boolean]" equalities nil )nil booleans nil )nil numbers nil )nil robinsonunification nil )nil robinsonunification nil ))nil ))nil 3467989055"" (typepred ff) (("" (assert ) (("" (grind) nil nil )) nil )) nil )nil term_adt nil )nil robinsonunification nil )"finite_sequence[T]" set2seq "structures/" )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[T, T -> boolean]" equalities nil )nil robinsonunification nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"[symbol -> nat]" robinsonunification nil )"{f: symbol | arity(f) = 1}" robinsonunificationnil ))nil ))nil 3474208611"" (expand Sub?)"" "Dom((id[(V)] ") "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 )"non_empty_finite_set" robinsonunification nil )"non_empty_finite_set[term]" robinsonunification nil )nil robinsonunification nil )nil robinsonunification nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"[symbol -> nat]" robinsonunification nil )nil term_adt nil ) (set type-eq-decl nil sets nil )"set[term]" variables_term nil )"[T, T -> boolean]" equalities nil )"set[(V)]" substitution nil )"bool" functions nil )"(bijective?[T, T])" identity nil )nil nat_types nil )nil finite_sequences nil )"[term -> boolean]" term_adt nil )"[[f: symbol, {args: finite_sequence[term] | args`length = arity(f)}] -> " term_adt nil) "{f: symbol | arity(f) = 1}" robinsonunificationnil )"finite_sequence[T]" set2seq "structures/" )"(V)" robinsonunification nil )"bool" sets nil )"(singleton?)" sets nil )nil finite_sets nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" substitution nil ))nil ))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 )"[symbol -> nat]" robinsonunification nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil robinsonunification nil )nil robinsonunification nil )nil positions nil )NOT const-decl "[bool -> bool]" booleans nil )"symbol" robinsonunification nil )"{args: finite_sequence[term[variable, symbol, arity]] | " robinsonunification nil) "below[length(stp!1)]" robinsonunificationnil )"term[variable, symbol, arity]" nil )"[d: (app?) -> {args: finite_sequence[term] | args`length = arity(f(d))}]" nil )"[(app?) -> symbol]" term_adt nil )"[T, T -> boolean]" equalities nil )nil finite_sequences nil )nil nat_types nil )"bool" reals nil )"[term -> boolean]" term_adt nil )nil term_adt nil )"(strict_total_order?[real])" real_props nil ))nil ))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 )"[symbol -> nat]" robinsonunification nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil robinsonunification nil )nil robinsonunification nil )nil positions nil )NOT const-decl "[bool -> bool]" booleans nil )"symbol" robinsonunification nil )"{args: finite_sequence[term[variable, symbol, arity]] | " robinsonunification nil) "below[length(stp!1)]" robinsonunificationnil )"term[variable, symbol, arity]" nil )"{t: term | s!1 /= t}" robinsonunificationnil )"[d: (app?) -> {args: finite_sequence[term] | args`length = arity(f(d))}]" nil )"[(app?) -> symbol]" term_adt nil )"[T, T -> boolean]" equalities nil )nil finite_sequences nil )nil nat_types nil )"bool" reals nil )"boolean" notequal nil )"[term -> boolean]" term_adt nil )nil term_adt nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3467989055"" (skosimp*) (("" (assert ) nil nil )) nil )"posint" nil )"posint" nil ))nil ))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 )"(strict_well_founded?[term])" term_adt nil )"posint" nil )"int" integers nil )"{k: int | k <= i AND k <= j}" nil )"{k: nat | k <= i AND k <= j}" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"boolean" term_adt nil )"term" subterm nil )"finseq" seq_extras "structures/" )"finseq" finite_sequences nil )"finseq" finite_sequences nil )"T" seq_extras "structures/" )"[below[length(fs)] -> T]" finite_sequencesnil )"finite_sequence[T]" set2seq "structures/" )nil integers nil )"bool" reals nil )nil integers nil )"posint" nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )nil nat_types nil )nil robinsonunification nil )nil robinsonunification nil )"[symbol -> nat]" robinsonunification nil )nil term_adt nil )nil finite_sequences nil )"[T, T -> boolean]" equalities nil )"symbol" robinsonunification nil )"{args: finite_sequence[term[variable, symbol, arity]] | " robinsonunification nil) "below[length(stp!1)]" robinsonunificationnil )"[term -> boolean]" term_adt nil )"[(app?) -> symbol]" term_adt nil )"[d: (app?) -> {args: finite_sequence[term] | args`length = arity(f(d))}]" nil )"term[variable, symbol, arity]" nil )"(strict_total_order?[real])" real_props nil ))nil ))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 )"[symbol -> nat]" robinsonunification nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil robinsonunification nil )nil robinsonunification nil )nil positions nil )"symbol" robinsonunification nil )"{args: finite_sequence[term[variable, symbol, arity]] | " robinsonunification nil) "below[length(stp!1)]" robinsonunificationnil )"term[variable, symbol, arity]" nil )"[d: (app?) -> {args: finite_sequence[term] | args`length = arity(f(d))}]" nil )"[(app?) -> symbol]" term_adt nil )"[T, T -> boolean]" equalities nil )nil finite_sequences nil )nil nat_types nil )"bool" reals nil )"[term -> boolean]" term_adt nil )nil term_adt nil )"(strict_total_order?[real])" real_props nil ))nil ))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 )"[symbol -> nat]" robinsonunification nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil robinsonunification nil )nil robinsonunification nil )nil positions nil )NOT const-decl "[bool -> bool]" booleans nil )"symbol" robinsonunification nil )"{args: finite_sequence[term[variable, symbol, arity]] | " robinsonunification nil) "below[length(stp!1)]" robinsonunificationnil )"term[variable, symbol, arity]" nil )"{t: term | s!1 /= t}" robinsonunificationnil )"[d: (app?) -> {args: finite_sequence[term] | args`length = arity(f(d))}]" nil )"[(app?) -> symbol]" term_adt nil )"[T, T -> boolean]" equalities nil )nil finite_sequences nil )nil nat_types nil )"bool" reals nil )"boolean" notequal nil )"[term -> boolean]" term_adt nil )nil term_adt nil )"(strict_total_order?[real])" real_props nil ))nil ))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 )"[T, T -> boolean]" equalities nil )nil finite_sequences nil )nil term_adt nil )"[symbol -> nat]" robinsonunification nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil robinsonunification nil )nil robinsonunification nil )nil nat_types nil )nil naturalnumbers nil )"posint" nil )"bool" reals nil ) (empty? const-decl "bool" sets nil )"bool" sets nil )"bool" sets nil )"term" subterm nil )nil integers nil )"bool" reals nil )nil integers nil )"finite_sequence[T]" set2seq "structures/" )"[below[length(fs)] -> T]" finite_sequencesnil )"T" seq_extras "structures/" )"finseq" finite_sequences nil )"finseq" finite_sequences nil )"finseq" seq_extras "structures/" )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"{k: nat | k <= i AND k <= j}" nil )"{k: int | k <= i AND k <= j}" nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )NOT const-decl "[bool -> bool]" booleans nil ))nil ))nil 3468654719"" (skosimp) (("" (typepred "t!1" ) (("" (assert ) nil nil )) nil ))nil )"boolean" notequal nil )nil term_adt nil )"[symbol -> nat]" robinsonunification nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil robinsonunification nil )nil robinsonunification nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil ))nil ))nil 3468654726"" (measure-induct+ "length(p)" "p" )"" (skosimp)"" (expand "first_diff" -2)"" (lift-if)"" (assert )"" "k!11" "min({kk: below[length(args(t!1))] | NOT " 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" "first_diff(subtermOF(s!1, #(k!1)), ") "4" "subtermOF(s!1, #(k!1))" "subtermOF(t!1, #(k!1))" )"4" (prop)"1" (expand "first_diff" 4)"1" (assert )"1" "k!22" "min({kk: below[length(args(s!1))] | NOT " nil )"1" "k!2" "1 + k!22" )"1" "1" replace -3 -1 rl)"1" replace -7 -2 rl)"1" "1" case "k!1 = k!2" )"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" "myset" " min({kk: below[length(args(s!1))] | NOT subtermOF(t!1, #(1 + kk)) = subtermOF(s!1, #(1 + kk))})" nil )"1" rewrite "1" rewrite "1" "1" expand "1" "1" "1" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" "s!1" "t!1" "f(s!1)" "args(s!1)" )"2" case "s!1 = app(f(s!1), args(s!1))" )"1" assert )"1" "1" "f(t!1)" "args(t!1)" )"1" case "t!1 = app(f(t!1), args(t!1))" )"1" assert )nil nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "3" "positions_of_arg" )"3" "t!1" "kk!1" )"3" assert )nil nil ))nil ))nil ))nil ))nil )"4" "4" "4" "positions_of_arg" )"4" "s!1" "kk!1" )"4" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "t!1" "s!1" "f(t!1)" "args(t!1)" )"2" case "t!1 = app(f(t!1), args(t!1))" )"1" assert )"1" "1" "f(s!1)" "args(s!1)" )"1" case "s!1 = app(f(s!1), args(s!1))" )"1" assert )nil nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "3" "positions_of_arg" )"3" "s!1" "kk!1" )"3" assert )nil nil ))nil ))nil ))nil ))nil )"4" "4" "4" "positions_of_arg" )"4" "t!1" "kk!1" )"4" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "t!1" "s!1" "f(t!1)" "args(t!1)" )"2" case "t!1 = app(f(t!1), args(t!1))" )"1" assert )"1" "1" "f(s!1)" "args(s!1)" )"1" case "s!1 = app(f(s!1), args(s!1))" )"1" assert )nil nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "3" "positions_of_arg" )"3" "s!1" "kk!1" )"3" assert )nil nil ))nil ))nil ))nil ))nil )"4" "4" "4" "positions_of_arg" )"4" "t!1" "kk!1" )"4" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "t!1" "s!1" "f(t!1)" "args(t!1)" )"2" case "t!1 = app(f(t!1), args(t!1))" )"1" assert )"1" "1" "f(s!1)" "args(s!1)" )"1" case "s!1 = app(f(s!1), args(s!1))" )"1" (assert ) nil nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "3" "positions_of_arg" )"3" "s!1" "kk!1" )"3" (assert ) nil nil ))nil ))nil ))nil ))nil )"4" "4" "4" "positions_of_arg" )"4" "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" "1" (propax) nil nil ))nil ))nil )"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 )"4" (hide -1)"4" (prop)"1" (hide 1)"1" (expand "first_diff" )"1" (lift-if) (("1" (prop) nil nil )) nil ))nil ))nil )"2" (hide 2)"2" (expand "first_diff" )"2" (lift-if)"2" (prop) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil )"3" (hide 3)"3" (expand "first_diff" )"3" (assert ) nil nil )) nil ))nil )"4" (hide -2 5)"4" (skosimp*)"4" (lemma "positions_of_arg" )"4" (inst -1 "s!1" "kk!1" )"1" (assert ) nil nil )"2" (hide 5)"2" (typepred "kk!1" )"2" "equal_symbol_equal_length_arg" )"2" "s!1" "t!1" "f(s!1)" "f(t!1)" "args(s!1)" "args(t!1)" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"5" (hide 5)"5" (expand "first_diff" )"5" (assert ) nil nil )) nil ))nil ))nil ))nil )"5" (prop)"1" (hide -3)"1" (expand "first_diff" ) (("1" (assert ) nil nil ))nil ))nil )"2" (hide -3)"2" (expand "first_diff" ) (("2" (assert ) nil nil ))nil ))nil )"3" (hide -3)"3" (expand "first_diff" ) (("3" (assert ) nil nil ))nil ))nil )"4" (assert ) nil nil ) ("5" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"posint" nil )"[term -> boolean]" term_adt nil )nil finite_sequences nil )"[(app?) -> symbol]" term_adt nil )"[d: (app?) -> {args: finite_sequence[term] | args`length = arity(f(d))}]" nil )set type-eq-decl nil sets nil )"bool" sets nil )"bool" reals nil )min const-decl "{a | S(a) AND (FORALL x: S(x) IMPLIES a <= x)}" nil )NOT const-decl "[bool -> bool]" booleans nil )nil positions nil )"positions" positions nil )nil positions nil )"term" subterm nil )"finite_sequence[T]" set2seq "structures/" )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"posint" nil )"finseq" seq_extras "structures/" )"finseq" seq_extras "structures/" )nil min_nat nil )nil positions nil )nil term_adt nil )"[[f: symbol, {args: finite_sequence[term] | args`length = arity(f)}] -> " term_adt nil) nil robinsonunification nil )"(total_order?[real])" nil )"bool" min_nat nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )nil integers nil )"term[variable, symbol, arity]" nil )"{t: term | s!1 /= t}" robinsonunificationnil )"below[length(args[variable, symbol, arity](t!1))]" nil )nil positions nil )AND const-decl "[bool, bool -> bool]" booleans nil )"position" robinsonunification nil )"[T, T -> boolean]" equalities nil )"[bool, bool -> bool]" booleans nil )"boolean" notequal nil )nil term_adt nil )nil naturalnumbers nil )"bool" reals nil )nil naturalnumbers nil )nil positions nil )"[symbol -> nat]" robinsonunification nil )nil robinsonunification nil )nil robinsonunification nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil nat_types nil )nil naturalnumbers nil )nil measure_induction nil )"bool" orders nil )nil defined_types nil ))nil 3468178714"" (measure-induct+ "length(p)" "p" )"" (skosimp)"" (expand "first_diff" -2)"" (lift-if)"" (prop)"1" (hide -3)"1" (replaces -2)"1" (expand "positionsOF" )"1" (assert )"1" (expand "only_empty_seq" )"1" (propax) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (hide -3)"2" (replaces -2)"2" (expand "positionsOF" )"2" (assert )"2" (expand "only_empty_seq" )"2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil )"3" (hide -3)"3" (replaces -2)"3" (expand "positionsOF" )"3" (assert )"3" expand * "union" "only_empty_seq" "IUnion" "member" )nil nil ))nil ))nil ))nil ))nil )"4" (assert )"4" "k!11" "min({kk: below[length(args(t!1))] | NOT ") "1" (name-replace "k!1" "1 + k!11" )"1" "first_diff(subtermOF(s!1, #(k!1)), subtermOF(t!1, #(k!1)))" "subtermOF(s!1, #(k!1))" "subtermOF(t!1, #(k!1))" )"1" (assert )"1" (hide -1)"1" (replace -1 -2)"1" (expand "add_first" -2)"1" (expand "insert?" -2)"1" rewrite "add_first_is_o" )"1" "pos_o_term" )"1" "1" assert )"1" "1" "1" replace -1 1 rl)"1" "1" "positions_of_arg" )"1" "s!1" "k!11" )"1" assert )nil nil )"2" "k!11" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide - 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" "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 - 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 - 5)"4" (skosimp*)"4" (lemma "positions_of_arg" )"4" (inst -1 "s!1" "kk!1" )"1" (assert ) nil nil )"2" (typepred "kk!1" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"5" (replaces -1)"5" (hide -1 1 2)"5" (expand "positionsOF" )"5" (assert )"5" expand * "union" "IUnion" "member" "only_empty_seq" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"posint" nil )"below[length(args[variable, symbol, arity](t!1))]" nil )nil term_adt nil )"[[f: symbol, {args: finite_sequence[term] | args`length = arity(f)}] -> " term_adt nil) nil robinsonunification nil )nil integers nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"finseq" seq_extras "structures/" )nil subterm nil )"term[variable, symbol, arity]" nil )"{t: term | s!1 /= t}" robinsonunificationnil )"{a | NOT subtermOF(s!1, #(1 + a)) = subtermOF(t!1, #(1 + a)) AND NOT subtermOF(s!1, #(1 + x)) = subtermOF(t!1, #(1 + x))" robinsonunification nil) nil positions nil )nil seq_extras "structures/" )nil finite_sequences nil )"finseq" seq_extras "structures/" )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"finite_sequence[T]" set2seq "structures/" )"term" subterm nil )nil positions nil )NOT const-decl "[bool -> bool]" booleans nil )min const-decl "{a | S(a) AND (FORALL x: S(x) IMPLIES a <= x)}" nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" sets nil )set type-eq-decl nil sets nil )"[d: (app?) -> {args: finite_sequence[term] | args`length = arity(f(d))}]" nil )"[(app?) -> symbol]" term_adt nil )nil finite_sequences nil )"[term -> boolean]" term_adt nil )"posint" nil )"set" sets nil )"set[T]" indexed_sets nil )"bool" sets nil )"positions" positions nil )"positions" positions nil )nil positions nil )"position" robinsonunification nil )"[T, T -> boolean]" equalities nil )"[bool, bool -> bool]" booleans nil )"boolean" notequal nil )nil term_adt nil )nil naturalnumbers nil )"bool" reals nil )nil naturalnumbers nil )nil positions nil )"[symbol -> nat]" robinsonunification nil )nil robinsonunification nil )nil robinsonunification nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil nat_types nil )nil naturalnumbers nil )nil measure_induction nil )"bool" orders nil )nil defined_types nil ))nil 3468768340"" (lemma comutative_first_diff)"" (lemma position_s_first_diff)"" (skosimp*)"" (inst -1 t!1 s!1 p!1)"" (inst -2 s!1 t!1 p!1) (("" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )nil robinsonunification nil )nil robinsonunification nil )nil robinsonunification nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"[symbol -> nat]" robinsonunification nil )nil term_adt nil )"boolean" notequal nil )nil nat_types nil )nil integers nil )"bool" reals nil )nil integers nil )nil positions nil )nil robinsonunification nil ))nil 3469282256"" (skosimp)"" (lemma position_s_first_diff)"" (inst -1 s!1 t!1 p!1) (("" (assert ) nil nil )) nil )) nil ))nil )nil robinsonunification nil )nil positions nil )nil integers nil )"bool" reals nil )nil integers nil )nil nat_types nil )"boolean" notequal nil )nil term_adt nil )"[symbol -> nat]" robinsonunification nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil robinsonunification nil )nil robinsonunification nil ))nil ))nil 3469282256"" (skosimp) (("" (rewrite position_t_first_diff) nil nil )) nil )nil robinsonunification nil )nil robinsonunification nil )nil robinsonunification nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"[symbol -> nat]" robinsonunification nil )nil term_adt nil )"boolean" notequal nil )nil nat_types nil )nil integers nil )"bool" reals nil )nil integers nil )nil positions nil ))nil ))nil 3469282257"" (measure-induct+ "length(p)" "p" )"1" (skosimp)"1" (expand first_diff -2)"1" (lift-if)"1" (prop)"1" (replaces -2)"1" (hide -1 -2)"1" (expand subtermOF)"1" (rewrite empty_0)"1" (typepred t!1) (("1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (replaces -2)"2" (hide -1 -2 1)"2" (expand subtermOF)"2" (rewrite empty_0)"2" (typepred t!1) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"3" (replaces -2)"3" (hide -1 -2 1 2)"3" (expand subtermOF)"3" (rewrite empty_0)"3" (typepred t!1) (("3" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"4" (assert )"4" "k!11" "min({kk: below[length(args(t!1))] | NOT subtermOF(s!1, #(1 + kk)) = subtermOF(t!1, #(1 + kk))})") "1" (name-replace "k!1" "1+k!11" )"1" "first_diff(subtermOF(s!1, #(k!1)), ") "1" "subtermOF(s!1, #(k!1))" "subtermOF(t!1, #(k!1))" )"1" (replace -2 -3)"1" (expand add_first -3)"1" (expand insert? -3)"1" (flatten)"1" "p!1" "first_diff(subtermOF(s!1, #(k!1)), " nil )"1" "1" "1" assert )"1" "1" "1" (assert ) nil nil )"2" "2" "2" replace -1 1 rl)"2" "2" "2" "f(s!1)" "args(s!1)" )"2" case "s!1 = app(f(s!1), args(s!1))" )"1" assert )"1" "1" "f(t!1)" "args(t!1)" )"1" case "t!1 = app(f(t!1), args(t!1))" )"1" assert )"1" "1" "k!11" )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" "2" "f(s!1)" "args(s!1)" )"2" case "s!1 = app(f(s!1), args(s!1))" )"1" assert )"1" "1" "f(t!1)" "args(t!1)" )"1" case "t!1 = app(f(t!1), args(t!1))" )"1" assert )"1" "1" "k!11" )"1" assert )nil nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -)"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" "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 -)"3" (skosimp*)"3" (lemma "positions_of_arg" )"3" (inst -1 "t!1" "kk!1" )"3" (assert ) nil nil )) nil ))nil ))nil ))nil )"4" (hide -)"4" (skosimp*)"4" (lemma "positions_of_arg" )"4" (inst -1 "s!1" "kk!1" )"1" (assert ) nil nil )"2" (typepred "kk!1" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"5" (hide -2 +)"5" (replaces -1)"5" (expand subtermOF)"5" (rewrite empty_0)"5" (typepred t!1) (("5" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but (-1 1))"2" (rewrite position_t_first_diff) nil nil )) nil )"3" (hide-all-but (-1 1))"3" (lemma position_s_first_diff)"3" (inst -1 s!1 t!1 y!1) (("3" (assert ) nil nil )) nil ))nil ))nil )"4" (hide 2) (("4" (rewrite position_t_first_diff) nil nil )) nil )"5" (hide 2)"5" (lemma position_s_first_diff)"5" (inst -1 s!1 t!1 p!1) (("5" (assert ) nil nil )) nil ))nil ))nil ))nil )nil robinsonunification nil )nil robinsonunification nil )"posint" nil )"below[length(args[variable, symbol, arity](t!1))]" nil )"(strict_total_order?[real])" real_props nil )nil positions nil )nil robinsonunification nil )nil integers nil )"int" integers nil )"finseq" seq_extras "structures/" )nil subterm nil )nil robinsonunification nil )"{t: term | s!1 /= t}" robinsonunificationnil )nil term_adt nil )"[[f: symbol, {args: finite_sequence[term] | args`length = arity(f)}] -> " term_adt nil) nil robinsonunification nil )"posint" robinsonunification nil )"term[variable, symbol, arity]" nil )"finseq" seq_extras "structures/" )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"finite_sequence[T]" set2seq "structures/" )min const-decl "{a | S(a) AND (FORALL x: S(x) IMPLIES a <= x)}" nil )"bool" reals nil )"bool" sets nil )set type-eq-decl nil sets nil )"[d: (app?) -> {args: finite_sequence[term] | args`length = arity(f(d))}]" nil )"[(app?) -> symbol]" term_adt nil )nil finite_sequences nil )"[term -> boolean]" term_adt nil )"posint" nil )NOT const-decl "[bool -> bool]" booleans nil )nil seq_extras "structures/" )nil finite_sequences nil )"finseq" finite_sequences nil )AND const-decl "[bool, bool -> bool]" booleans nil )"term" subterm nil )nil positions nil )nil term_adt nil )"boolean" notequal nil )"[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )"position" robinsonunification nil )nil positions nil )"positions" positions nil )nil naturalnumbers nil )"bool" reals nil )nil naturalnumbers nil )nil positions nil )"[symbol -> nat]" robinsonunification nil )nil robinsonunification nil )nil robinsonunification nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil nat_types nil )nil naturalnumbers nil )nil measure_induction nil )"bool" orders nil )nil defined_types nil ))nil 3469352101"" (measure-induct+ "length(p)" "p" )"1" (skosimp)"1" (expand first_diff -2)"1" (lift-if)"1" (prop)"1" (hide -3 -4 2)"1" (replaces -2)"1" (expand subtermOF)"1" (rewrite empty_0) nil nil )) nil ))nil ))nil )"2" (hide -3)"2" (expand unifiable)"2" (skeep -3)"2" (expand unifier)"2" (expand ext -3 1)"2" (assert )"2" (replaces -2)"2" (expand subtermOF)"2" (rewrite empty_0)"2" "2" "2" "2" expand ext -2)"2" assert )"2" "2" "2" "2" "2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide -3 -4 1 2 3)"3" (replaces -2)"3" (expand subtermOF)"3" (rewrite empty_0) nil nil )) nil ))nil ))nil )"4" (assert )"4" "k!11" "min({kk: below[length(args(t!1))] | NOT subtermOF(s!1, #(1 + kk)) = subtermOF(t!1, #(1 + kk))})") "1" (name-replace "k!1" "1+k!11" )"1" " first_diff(subtermOF(s!1, #(k!1)), ") "1" "subtermOF(s!1, #(k!1))" "subtermOF(t!1, #(k!1))" )"1" (replace -2 -3)"1" (expand add_first -3)"1" (expand insert? -3)"1" (prop)"1" "1" "first_diff(subtermOF(s!1, #(k!1)), " "1" (assert ) nil nil )"2" "2" "2" "2" "2" "s!1" "t!1" "f(s!1)" "args(s!1)" )"2" case "s!1 = app(f(s!1), args(s!1))" )"1" assert )"1" "1" "f(t!1)" "args(t!1)" )"1" case "t!1 = app(f(t!1), args(t!1))" )"1" assert )"1" "1" "k!11" )"1" assert )nil nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "first_diff(subtermOF(s!1, #(k!1)), " "1" (assert ) nil nil )"2" "2" "2" "2" "2" "s!1" "t!1" "f(s!1)" "args(s!1)" )"2" case "s!1 = app(f(s!1), args(s!1))" )"1" assert )"1" "1" "f(t!1)" "args(t!1)" )"1" case "t!1 = app(f(t!1), args(t!1))" )"1" assert )"1" "1" "k!11" )"1" assert )nil nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "3" expand unifiable)"3" "3" "3" "#(k!1)" )"1" expand * member U)"1" (assert ) nil nil ))nil )"2" "2" "2" "2" "s!1" "t!1" "f(s!1)" "args(s!1)" )"2" case "s!1 = app(f(s!1), args(s!1))" )"1" assert )"1" "1" "f(t!1)" "args(t!1)" )"1" case "t!1 = app(f(t!1), args(t!1))" )"1" assert )"1" "1" "k!11" )"1" assert )"1" "1" "s!1" "t!1" "f(s!1)" "args(s!1)" )"1" case "s!1 = app(f(s!1), args(s!1))" )"1" assert )"1" "1" "f(t!1)" "args(t!1)" )"1" case "t!1 = app(f(t!1), args(t!1))" )"1" assert )"1" "1" "k!11" )"1" assert )nil nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -2 -3 -4 5 6)"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" "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 - (5 6))"3" (skosimp*)"3" (lemma "positions_of_arg" )"3" (inst -1 "t!1" "kk!1" )"3" (assert ) nil nil )) nil ))nil ))nil ))nil )"4" (hide - (5 6))"4" (skosimp*)"4" (lemma "positions_of_arg" )"4" (inst -1 "s!1" "kk!1" )"1" (assert ) nil nil )"2" (typepred "kk!1" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"5" (hide -1 -2 5 6)"5" (expand unifiable)"5" (skeep -1)"5" (expand unifier)"5" (expand ext )"5" (assert )"5" (lift-if)"5" (prop)"1" (decompose-equality -2) nil nil )"2" (decompose-equality -1) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but (-1 2))"2" (rewrite position_t_first_diff) nil nil )) nil )"3" (hide-all-but (-1 1))"3" (lemma position_s_first_diff)"3" (inst -1 s!1 t!1 y!1) (("3" (assert ) nil nil )) nil ))nil ))nil )"4" (hide-all-but (-1 2))"4" (rewrite position_t_first_diff) nil nil )) nil )"5" (hide-all-but (-1 1))"5" (lemma position_s_first_diff)"5" (inst -1 s!1 t!1 p!1) (("5" (assert ) nil nil )) nil ))nil ))nil ))nil )nil robinsonunification nil )nil robinsonunification nil )"posint" nil )"below[length(args[variable, symbol, arity](t!1))]" nil )"(strict_total_order?[real])" real_props nil )nil positions nil )nil robinsonunification nil )nil integers nil )"int" integers nil )"finseq" seq_extras "structures/" )"term[variable, symbol, arity]" nil )"posint" robinsonunification nil )nil robinsonunification nil )nil term_adt nil )nil subterm nil )"{t: term | s!1 /= t}" robinsonunificationnil )nil robinsonunification nil )nil unification nil )"bool" sets nil )"set[Sub]" unification nil )"finseq" seq_extras "structures/" )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"finite_sequence[T]" set2seq "structures/" )min const-decl "{a | S(a) AND (FORALL x: S(x) IMPLIES a <= x)}" nil )"bool" reals nil )"bool" sets nil )"posint" nil )ext def-decl "term" substitution nil )"[term -> boolean]" term_adt nil )"[(app?) -> symbol]" term_adt nil )nil finite_sequences nil )"[[f: symbol, {args: finite_sequence[term] | args`length = arity(f)}] -> " term_adt nil) "[d: (app?) -> {args: finite_sequence[term] | args`length = arity(f(d))}]" nil )set type-eq-decl nil sets nil )"set[term]" variables_term nil )"bool" substitution nil )nil substitution nil )"[below[length(fs)] -> T]" finite_sequencesnil )"bool" unification nil )nil seq_extras "structures/" )nil finite_sequences nil )"finseq" finite_sequences nil )OR const-decl "[bool, bool -> bool]" booleans nil )NOT const-decl "[bool -> bool]" booleans nil )"[term -> boolean]" term_adt nil )nil positions nil )"term" subterm nil )nil term_adt nil )"boolean" notequal nil )"[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )"position" robinsonunification nil )"bool" unification nil )nil positions nil )"positions" positions nil )nil naturalnumbers nil )"bool" reals nil )nil naturalnumbers nil )nil positions nil )"[symbol -> nat]" robinsonunification nil )nil robinsonunification nil )nil robinsonunification nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil nat_types nil )nil naturalnumbers nil )nil measure_induction nil )"bool" orders nil )nil defined_types nil ))nil 3512858302"" (skosimp*)"" (lemma position_s_first_diff)"" (inst -1 s!1 t!1 fd!1)"" (assert )"" (typepred p!1)"" (hide -2)"" (hide -3)"" (lemma app_term)"" (inst -1 fd!1 p!1 s!1) (("" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil robinsonunification nil )nil subterm nil )NOT const-decl "[bool -> bool]" booleans nil )nil positions nil )"positions" positions nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil positions nil )nil integers nil )"bool" reals nil )nil integers nil )nil nat_types nil )"boolean" notequal nil )nil term_adt nil )"[symbol -> nat]" robinsonunification nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil robinsonunification nil )nil robinsonunification nil ))nil ))nil 3512858302"" (skosimp*)"" (lemma position_t_first_diff)"" (inst -1 s!1 t!1 fd!1)"" (assert )"" (typepred p!1)"" (hide -1 -4)"" (lemma app_term)"" (inst -1 fd!1 p!1 t!1) (("" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil robinsonunification nil )nil subterm nil )NOT const-decl "[bool -> bool]" booleans nil )nil positions nil )"positions" positions nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil positions nil )nil integers nil )"bool" reals nil )nil integers nil )nil nat_types nil )"boolean" notequal nil )nil term_adt nil )"[symbol -> nat]" robinsonunification nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil robinsonunification nil )nil robinsonunification nil ))nil ))nil 3512858302"" (measure-induct+ "length(first_diff(s, t))" ("s" "t" ))"1" (skosimp)"1" (name-replace "fd" "first_diff(x!1, x!2)" :hide? nil )"1" (expand first_diff -1)"1" (lift-if)"1" (prop)"1" (hide-all-but (-2 -4))"1" (replace -1 -2 rl)"1" (hide -1)"1" (expand child)"1" (skosimp)"1" (lemma seq_empty[posnat])"1" (inst -1 p!1 p1!1)"1" (assert )"1" "1" (rewrite empty_0 -2) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but (-2 -4))"2" (replace -1 -2 rl)"2" (hide -1)"2" (expand child)"2" (skosimp)"2" (lemma seq_empty[posnat])"2" (inst -1 p!1 p1!1)"2" (assert )"2" "2" (rewrite empty_0 -2) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide-all-but (-2 -4))"3" (replace -1 -2 rl)"3" (hide -1)"3" (expand child)"3" (skosimp)"3" (lemma seq_empty[posnat])"3" (inst -1 p!1 p1!1)"3" (assert )"3" "3" (rewrite empty_0 -2) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" (case "p!1 = empty_seq" )"1" (hide-all-but (-1 -2 4))"1" (replaces -1)"1" (rewrite subterm_empty_seq)"1" (rewrite subterm_empty_seq) nil nil )) nil ))nil ))nil )"2" "kk" "min({kk: below[length(args(x!2))] | " nil )"1" (assert )"1" "subtermOF(x!1, #(1 + kk))" "subtermOF(x!2, #(1 + kk))" )"1" (replace -3 -4 rl)"1" (expand add_first -4)"1" (expand insert? -4)"1" (inst -4 "rest(p!1)" )"1" "1" "1" "#(1 + kk)" "rest(p!1)" "x!1" )"1" "#(1 + kk)" "rest(p!1)" "x!2" )"1" "1" "1" replace -1 -3 rl)"1" replace -2 -3 rl)"1" case "#(1 + kk) o rest(p!1) = p!1" )"1" (assert ) nil nil )"2" "2" expand child)"2" "2" case "first(p!1) = first(fd)" )"1" case "first(fd) = 1 + kk" )"1" "1" "1" "1" "1" assert )"1" "1" "1" rewrite nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" replace "2" "2" rewrite nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" rewrite "2" "2" "2" rewrite nil nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "3" rewrite "3" "3" nil nil ))nil ))nil ))nil ))nil )"4" "4" "4" rewrite nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand child)"2" "2" case "first(p!1) = 1 + kk" )"1" "1" "1" assert )"1" "1" "1" rewrite nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" "2" "2" assert )"2" replace "2" replace "2" replace "2" "2" rewrite nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "3" rewrite nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand child)"2" "2" case "first(p!1) = 1 + kk" )"1" "1" "1" assert )"1" "1" "1" rewrite nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" "2" "2" assert )"2" replace "2" replace "2" replace "2" "2" rewrite nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "3" rewrite nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand child)"2" "2" "2" assert )"2" "2" "2" "2" "2" assert )"2" replace -1 2 rl)"2" "2" "first_diff(subtermOF(x!1, #(1 + kk)), subtermOF(x!2, #(1 + kk)))" "1 + kk" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "p!1 = #(1 + kk) o rest(p!1)" )"1" "1" "1" rewrite pos_subterm_ax)"1" rewrite pos_subterm_ax)nil nil ))nil ))nil ))nil )"2" "2" "2" "2" "2" "2" assert )"2" expand child)"2" "2" replace -2 -3 rl)"2" "2" "2" "first_diff(subtermOF(x!1, #(1 + kk)), " "1 + kk" )"2" replace "2" "2" rewrite "2" 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 (-1 1 3 4 5))"2" (lemma first_diff_TCC7)"2" (inst -1 x!1 x!2 "f(x!1)" "args(x!1)" )"2" (assert )"2" (case "x!1 = app(f(x!1), args(x!1))" )"1" (assert )"1" "f(x!2)" "args(x!2)" )"1" case "x!2 = app(f(x!2), args(x!2))" )"1" (assert ) nil nil )"2" "2" nil nil ))nil ))nil ))nil ))nil )"2" (hide-all-but (1 5))"2" (decompose-equality) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (skosimp)"3" (rewrite positions_of_arg) nil nil )) nil )"4" (hide -2 -3 -4 2 6)"4" (skosimp)"4" (rewrite positions_of_arg)"4" (typepred kk!1)"4" (typepred "args(x!2)" )"4" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"5" (hide-all-but (-1 -3))"5" (replace -1 -2 rl)"5" (hide -1)"5" (expand child)"5" (skosimp)"5" (lemma seq_empty[posnat])"5" (inst -1 p!1 p1!1)"5" (assert )"5" "5" (rewrite empty_0 -2) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but (-1 1))"2" (lemma position_t_first_diff)"2" (inst -1 y!1 y!2 "first_diff(y!1, y!2)" )"2" (name-replace "fd" "first_diff(y!1, y!2)" )"2" (expand child)"2" (skosimp)"2" (lemma pos_subterm_ax)"2" (inst -1 p!1 p1!1 y!2)"2" (assert )"2" (lemma not_var)"2" (lemma seq_first_rest[posnat])"2" (inst -1 p1!1)"2" (lemma empty_0[posnat])"2" "2" assert )"2" "first(p1!1)" "p1!1" "rest(p1!1)" "subtermOF(y!2, p!1)" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide-all-but (-1 1))"3" (lemma position_s_first_diff)"3" (inst -1 y!1 y!2 "first_diff(y!1, y!2)" )"3" (name-replace "fd" "first_diff(y!1, y!2)" )"3" (expand child)"3" (skosimp)"3" (lemma pos_subterm_ax)"3" (inst -1 p!1 p1!1 y!1)"3" (assert )"3" (lemma not_var)"3" (lemma seq_first_rest[posnat])"3" (inst -1 p1!1)"3" (lemma empty_0[posnat])"3" "3" assert )"3" "first(p1!1)" "p1!1" "rest(p1!1)" "subtermOF(y!1, p!1)" )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" (hide-all-but 1)"4" (skosimp)"4" (lemma position_t_first_diff)"4" (inst -1 y!1 y!2 "first_diff(y!1, y!2)" )"4" (name-replace "fd" "first_diff(y!1, y!2)" )"4" (expand child)"4" (skosimp)"4" (lemma pos_subterm_ax)"4" (inst -1 p!1 p1!1 y!2)"4" (assert )"4" (lemma not_var)"4" (lemma seq_first_rest[posnat])"4" (inst -1 p1!1)"4" "4" "4" assert )"4" "first(p1!1)" "p1!1" "rest(p1!1)" "subtermOF(y!2, p!1)" )"4" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"5" (hide-all-but 1)"5" (skosimp)"5" (lemma position_s_first_diff)"5" (inst -1 y!1 y!2 "first_diff(y!1, y!2)" )"5" (name-replace "fd" "first_diff(y!1, y!2)" )"5" (expand child)"5" (skosimp)"5" (lemma pos_subterm_ax)"5" (inst -1 p!1 p1!1 y!1)"5" (assert )"5" (lemma not_var)"5" (lemma seq_first_rest[posnat])"5" (inst -1 p1!1)"5" "5" "5" assert )"5" "first(p1!1)" "p1!1" "rest(p1!1)" "subtermOF(y!1, p!1)" )"5" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"6" (hide-all-but 1)"6" (skosimp)"6" (lemma position_t_first_diff)"6" (inst?)"6" (inst?)"6" (name-replace "fd" "first_diff(x!1`1, x!1`2)" )"6" (expand child)"6" (skosimp)"6" (lemma pos_subterm_ax)"6" (inst?)"6" (inst?)"6" (lemma seq_first_rest[posnat])"6" (inst -1 p1!2)"6" "6" "6" assert )"6" "6" "6" "6" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"7" (hide-all-but (-1 1))"7" (lemma position_t_first_diff)"7" (inst?)"7" (inst?)"7" (name-replace "fd" "first_diff(y!1`1, y!1`2)" )"7" (expand child)"7" (skosimp)"7" (lemma pos_subterm_ax)"7" (inst?)"7" (inst?)"7" (lemma seq_first_rest[posnat])"7" (inst -1 p1!1)"7" (lemma empty_0[posnat])"7" "7" assert )"7" "7" "7" "7" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"8" (hide-all-but (-1 1))"8" (lemma position_s_first_diff)"8" (inst?)"8" (inst?)"8" (name-replace "fd" "first_diff(y!1`1, y!1`2)" )"8" (expand child)"8" (skosimp)"8" (lemma pos_subterm_ax)"8" (inst?)"8" (inst?)"8" (lemma seq_first_rest[posnat])"8" (inst -1 p1!1)"8" (lemma empty_0[posnat])"8" "8" assert )"8" "8" "8" "8" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"9" (hide-all-but 1)"9" (skosimp)"9" (lemma position_s_first_diff)"9" (inst?)"9" (inst?)"9" (name-replace "fd" "first_diff(x!1`1, x!1`2)" )"9" (expand child)"9" (skosimp)"9" (lemma pos_subterm_ax)"9" (inst?)"9" (inst?)"9" (lemma seq_first_rest[posnat])"9" (inst -1 p1!2)"9" "9" "9" assert )"9" "9" "9" "9" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"10" (hide-all-but (-1 1))"10" (lemma position_t_first_diff)"10" (inst?)"10" (inst?)"10" (name-replace "fd" "first_diff(y!1`1, y!1`2)" )"10" (expand child)"10" (skosimp)"10" (lemma pos_subterm_ax)"10" (inst?)"10" (inst?)"10" (lemma seq_first_rest[posnat])"10" (inst -1 p1!1)"10" (lemma empty_0[posnat])"10" "10" assert )"10" "10" "10" "10" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"11" (hide-all-but (-1 1))"11" (lemma position_s_first_diff)"11" (inst?)"11" (inst?)"11" (name-replace "fd" "first_diff(y!1`1, y!1`2)" )"11" (expand child)"11" (skosimp)"11" (lemma pos_subterm_ax)"11" (inst?)"11" (inst?)"11" (lemma seq_first_rest[posnat])"11" (inst -1 p1!1)"11" (lemma empty_0[posnat])"11" "11" assert )"11" "11" "11" "11" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"12" (hide-all-but 1)"12" (skosimp)"12" (lemma position_t_first_diff)"12" (inst?)"12" (inst?)"12" (name-replace "fd" "first_diff(y!1`1, y!1`2)" )"12" (expand child)"12" (skosimp)"12" (lemma pos_subterm_ax)"12" (inst?)"12" (inst?)"12" (lemma seq_first_rest[posnat])"12" (inst -1 p1!1)"12" "12" "12" assert )"12" "12" "12" "12" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"13" (hide-all-but 1)"13" (skosimp)"13" (lemma position_s_first_diff)"13" (inst?)"13" (inst?)"13" (name-replace "fd" "first_diff(y!1`1, y!1`2)" )"13" (expand child)"13" (skosimp)"13" (lemma pos_subterm_ax)"13" (inst?)"13" (inst?)"13" (lemma seq_first_rest[posnat])"13" (inst -1 p1!1)"13" "13" "13" assert )"13" "13" "13" "13" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"14" (hide 2)"14" (skosimp)"14" (lemma position_t_first_diff)"14" (inst?)"14" (assert )"14" (hide -2)"14" (expand child)"14" (skosimp)"14" (lemma pos_subterm_ax)"14" (inst?)"14" (inst?)"14" (lemma seq_first_rest[posnat])"14" (inst -1 p1!1)"14" "14" "14" assert )"14" "14" "14" "14" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"15" (hide 2)"15" (skosimp)"15" (lemma position_s_first_diff)"15" (inst?)"15" (assert )"15" (hide -2)"15" (expand child)"15" (skosimp)"15" (lemma pos_subterm_ax)"15" (inst?)"15" (inst?)"15" (lemma seq_first_rest[posnat])"15" (inst -1 p1!1)"15" "15" "15" assert )"15" "15" "15" "15" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil robinsonunification nil )nil seq_extras "structures/" )nil positions nil )nil robinsonunification nil )nil seq_extras "structures/" )nil seq_extras "structures/" )nil finite_sequences nil )"posint" nil )nil finite_sequences nil )"[d: (app?) -> {args: finite_sequence[term] | args`length = arity(f(d))}]" nil )set type-eq-decl nil sets nil )"bool" sets nil )"bool" reals nil )min const-decl "{a | S(a) AND (FORALL x: S(x) IMPLIES a <= x)}" nil )"finite_sequence[T]" set2seq "structures/" )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )NOT const-decl "[bool -> bool]" booleans nil )"posint" nil )"finseq" seq_extras "structures/" )"term[variable, symbol, arity]" nil )"{t: term | x!1 /= t}" robinsonunificationnil )"{a | NOT subtermOF(x!1, #(1 + a)) = subtermOF(x!2, #(1 + a)) AND NOT subtermOF(x!1, #(1 + x)) = subtermOF(x!2, #(1 + x))" robinsonunification nil) "finseq" seq_extras "structures/" )"{p: position | positionsOF(x!1)(p) AND positionsOF(x!2)(p)}" nil )nil seq_extras "structures/" )nil seq_extras "structures/" )nil subterm nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"{k: nat | k <= i AND k <= j}" nil )"{k: int | k <= i AND k <= j}" nil )"int" integers nil )"[below[length(fs)] -> T]" finite_sequencesnil )"finseq" finite_sequences nil )nil seq_extras "structures/" )nil seq_extras "structures/" )nil seq_extras "structures/" )"T" seq_extras "structures/" )nil seq_extras "structures/" )"finseq" finite_sequences nil )nil subterm nil )"finseq" seq_extras "structures/" )nil robinsonunification nil )nil term_adt nil )"[[f: symbol, {args: finite_sequence[term] | args`length = arity(f)}] -> " term_adt nil) "odd_int" integersnil )"(strict_total_order?[real])" real_props nil )"[numfield, numfield -> numfield]" number_fields nil )nil positions nil )nil subterm nil )"finseq" finite_sequences nil )"[(app?) -> symbol]" term_adt nil )"[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil positions nil )"positions" positions nil )"bool" positions nil )"[term -> boolean]" term_adt nil )nil positions nil )"term" subterm nil )nil naturalnumbers nil )"bool" reals nil )"position" robinsonunification nil )nil positions nil )nil integers nil )"bool" reals nil )nil integers nil )nil nat_types nil )nil naturalnumbers nil )"boolean" notequal nil )nil term_adt nil )"[symbol -> nat]" robinsonunification nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil robinsonunification nil )nil robinsonunification nil )nil measure_induction nil )"bool" orders nil )nil defined_types nil ))nil 3467989055"" (skosimp*)"" (hide -1 -2 -4) (("" (expand V) (("" (propax) nil nil )) nil ))nil ))nil )"set[term]" variables_term nil )) nil ))nil 3467989055"" (skosimp*)"" (lemma "Vars_is_var" )"" (lemma "vars_of_term_finite" )"" (inst -1 "sp!1" )"" (inst -2 "sp!1" )"" (assert )"" (expand * "Sub?" "Dom" )"" (replaces -2)"" (expand "is_finite" )"" (skosimp)"" (inst 2 "N!1" "f!1" )"1" (hide-all-but (-1 2))"1" (expand "injective?" )"1" (skeep)"1" "x1" "x2" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (skeep)"2" (prop)"1" (assert )"1" "1" "1" "first_diff_has_diff_argument" )"1" "s!1" "t!1" "k!1" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"[symbol -> nat]" robinsonunification nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil robinsonunification nil )nil robinsonunification nil )nil subterm nil )nil term_adt nil )nil positions nil )nil integers nil )"bool" reals nil )nil integers nil )nil robinsonunificationnil )"bool" functions nil )nil nat_types nil )"bool" reals nil ) (set type-eq-decl nil sets nil )"set[term]" variables_term nil )"[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )"term[variable, symbol, arity]" nil )"boolean" notequal nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"term[variable, symbol, arity]" nil )"bool" finite_sets nil )"bool" substitution nil )"set[(V)]" substitution nil )nil subterm nil ))nil ))nil 3467989055 ("" (subtype-tcc) nil nil )NOT const-decl "[bool -> bool]" booleans nil )nil term_adt nil )"boolean" notequal nil )"[symbol -> nat]" robinsonunification nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil robinsonunification nil )nil robinsonunification nil )"set[term]" variables_term nil )"posint" nil ))nil ))nil 3467989055"" (skosimp*)"" (lemma "Vars_is_var" )"" (lemma "vars_of_term_finite" )"" (inst -1 "tp!1" )"" (inst -2 "tp!1" )"" (assert )"" (expand * "Sub?" "Dom" )"" (replaces -2)"" (expand "is_finite" )"" (skosimp)"" (inst 3 "N!1" "f!1" )"1" (hide-all-but (-1 3))"1" (expand "injective?" )"1" (skeep)"1" "x1" "x2" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (skeep)"2" (prop)"1" (assert ) nil nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"[symbol -> nat]" robinsonunification nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil robinsonunification nil )nil robinsonunification nil )nil subterm nil )nil term_adt nil )"bool" functions nil )nil nat_types nil )"bool" reals nil ) (set type-eq-decl nil sets nil )"set[term]" variables_term nil )"[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )"term[variable, symbol, arity]" nil )"boolean" notequal nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"term[variable, symbol, arity]" nil )"bool" finite_sets nil )"bool" substitution nil )"set[(V)]" substitution nil )nil subterm nil ))nil ))nil 3468666181"" (skosimp)"" (assert )"" "sig!1" "link_of_frst_diff(s!1, t!1)" :hide? nil )"" (prop)"1" (expand * "restrict" "singleton" )"1" (decompose-equality 1)"1" (iff)"1" (prop)"1" (copy -3)"1" (decompose-equality -1)"1" (inst -1 "x!1" )"1" (expand "Dom" )"1" (expand "link_of_frst_diff" -1)"1" (assert )"1" "1" "1" (assert ) nil nil )"2" expand "link_of_frst_diff" -4)"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (replace -3 1 rl)"2" (expand "link_of_frst_diff" 1)"2" (assert )"2" (prop)"1" (expand "Dom" )"1" (replace -5 1 rl)"1" replace -2 1 rl)"1" "1" expand * "member" "subtermOF" )"1" "1" "1" expand "Vars" )"1" "empty_seq" )"1" expand "subtermOF" )"1" "1" "1" "1" rewrite "empty_0" )nil nil ))nil ))nil ))nil ))nil )"2" "2" expand "positionsOF" )"2" "2" "1" expand "only_empty_seq" )"1" nil nil ))nil )"2" expand "only_empty_seq" )"2" nil nil ))nil )"3" expand *"union" "IUnion" "member" "only_empty_seq" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "finseq_appl" )"2" "2" (assert ) nil nil ))nil ))nil )"3" "3" (assert ) nil nil ))nil )"4" expand "Vars" )"4" expand "finseq_appl" )"4" "empty_seq" )"1" "1" replace -1 -2 rl)"1" expand "subtermOF" "1" rewrite "empty_0" nil nil ))nil ))nil ))nil )"2" "2" expand "finseq_appl" )"2" expand "positionsOF" )"2" "2" "1" expand "only_empty_seq" )"1" nil nil ))nil )"2" expand "only_empty_seq" )"2" nil nil ))nil )"3" "3" expand *"union" "IUnion" "member" "only_empty_seq" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "link_of_frst_diff" -4)"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand * "restrict" "singleton" )"2" (decompose-equality 2)"1" (iff)"1" (prop)"1" (copy -2)"1" (decompose-equality -1)"1" (inst -1 "x!1" )"1" (expand "Dom" )"1" (replace -1 -2 rl)"1" (expand "link_of_frst_diff" -2)"1" assert )"1" case "vars?(subtermOF(t!1, first_diff(s!1, t!1)))" )"1" assert )"1" "1" "1" expand "link_of_frst_diff" "1" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" assert )"2" replace -3 1 rl)"2" expand "link_of_frst_diff" -2)"2" (assert ) nil nil ))nil ))nil ))nil )"3" "3" "position_s_first_diff" )"3" "comutative_first_diff" )"3" "t!1" "s!1" "first_diff(s!1,t!1)" )"3" assert )"3" "3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (copy -2)"2" (decompose-equality -1)"2" (inst -1 "x!1" )"2" (expand "link_of_frst_diff" -1)"2" (assert )"2" (lift-if)"2" "1" expand "Dom" )"1" (assert ) nil nil ))nil )"2" expand "link_of_frst_diff" -5)"2" (assert ) nil nil ))nil )"3" assert )"3" expand "link_of_frst_diff" -3)"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -1 2 3)"2" (skosimp)"2" (lemma "position_s_first_diff" )"2" (inst -1 "t!1" "s!1" "p!1" )"2" (lemma "comutative_first_diff" )"2" (assert )"2" (inst -1 s!1 t!1 p!1)"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"set[(V)]" substitution nil )nil nat_types nil )nil integers nil )"bool" reals nil )nil integers nil )nil positions nil )nil positions nil )"positions" positions nil )nil positions nil )"term" subterm nil )"finseq" seq_extras "structures/" )"position[variable, symbol, arity]" nil )"T" seq_extras "structures/" )nil seq_extras "structures/" )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[d: (app?) -> {args: finite_sequence[term] | args`length = arity(f(d))}]" nil )"[(app?) -> symbol]" term_adt nil )nil finite_sequences nil )"[term -> boolean]" term_adt nil )"bool" reals nil )"[below[length(fs)] -> T]" finite_sequencesnil )"int" integers nil )"set[(V)]" subterm nil )"set" sets nil )"set[T]" indexed_sets nil )"positions" positions nil )nil seq_extras "structures/" )"finseq" finite_sequences nil )nil finite_sequences nil )"{t: term | s!1 /= t}" robinsonunificationnil )"term[variable, symbol, arity]" nil )"bool" sets nil )"R" restrict nil )"(singleton?)" sets nil )"[term -> boolean]" term_adt nil )"position" robinsonunification nil )nil robinsonunification nil )nil robinsonunification nil )"Sub" robinsonunification nil )nil substitution nil )"bool" substitution nil )"boolean" notequal nil )"[T, T -> boolean]" equalities nil )"set[term]" variables_term nil )set type-eq-decl nil sets nil ) (term type-decl nil term_adt nil )"[symbol -> nat]" robinsonunification nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil robinsonunification nil )nil robinsonunification nil ))nil 3468741400"" (assert )"" (skosimp*)"" "sig!1" "link_of_frst_diff(s!1, t!1)" :hide? nil )"" (typepred "x!1" )"" (typepred "r!1" )"" (hide -2)"" (expand "member" )"" (replace -3 -1)"" (replace -3 -2)"" (expand "Dom" )"" (expand "Ran" )"" (skosimp)"" (expand * "member" "Dom" )"" (lemma "dom_link_of_frst_diff_is" )"" "first_diff(s!1, t!1)" "s!1" "t!1" )"" assert )"" replace -4 -1)"" assert )"" "p!1" "first_diff(s!1, t!1)" nil )"" expand *"restrict" "singleton" )"" "1" "1" "1" "x!1" )"1" "1" assert )"1" "x!1" )"1" expand "member" )"1" assert )"1" "1" replace "1" "1" "x!2" )"1" expand "Dom" )"1" expand "link_of_frst_diff" "1" assert )"1" "1" "1" replace "1" replace "1" replace "1" replace "1" "1" expand "member" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace "2" "2" expand "link_of_frst_diff" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "vars?(subtermOF(t!1, p!1))" )"1" "1" "1" "x!1" )"1" expand "Dom" -1)"1" "1" "x!2" )"1" expand "Dom" "1" replace "1" expand "link_of_frst_diff" "1" assert )"1" "1" "1" replace "1" replace "1" replace "1" replace "1" "1" expand "member" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace "2" "2" expand "link_of_frst_diff" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "link_of_frst_diff" )"2" assert )nil nil ))nil ))nil )"3" "3" "position_s_first_diff" )"3" "t!1" "s!1" "p!1" )"3" assert )"3" "3" "comutative_first_diff" )"3" "s!1" "t!1" "p!1" )"3" 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 )"set[(V)]" substitution nil )"bool" sets nil )NOT const-decl "[bool -> bool]" booleans nil )nil robinsonunification nil )"(singleton?)" sets nil )"R" restrict nil )"[term -> boolean]" term_adt nil )nil robinsonunification nil )nil robinsonunification nil )nil positions nil )"positions" positions nil )nil positions nil )"term" subterm nil )nil nat_types nil )nil integers nil )"bool" reals nil )nil integers nil )nil positions nil )"position" robinsonunification nil )"set[term]" substitution nil )"Sub" robinsonunification nil )nil substitution nil )"bool" substitution nil )"boolean" notequal nil )"[T, T -> boolean]" equalities nil )"set[term]" variables_term nil )set type-eq-decl nil sets nil ) (term type-decl nil term_adt nil )"[symbol -> nat]" robinsonunification nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil robinsonunification nil )nil robinsonunification nil ))nil 3468745076"" (skosimp)"" (assert )"" (flatten)"" "sig!1" "link_of_frst_diff(s!1, t!1)" :hide?nil )"" (prop)"1" (lemma "vars_subst_not_in" )"1" (inst -1 "s!1" "sig!1" "x!1" )"1" (assert )"1" (skosimp)"1" (lemma "dom_ran_link_disjoint" )"1" (inst -1 "s!1" "t!1" )"1" (assert )"1" (inst -1 "x!1" "r!1" )"1" (replaces -4)"1" "1" expand "member" )"1" (propax) nil nil ))nil ))nil ))nil )"2" (replaces -4)"2" "2" expand "member" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "vars_subst_not_in" )"2" (inst -1 "t!1" "sig!1" "x!1" )"2" (assert )"2" (skosimp)"2" (lemma "dom_ran_link_disjoint" )"2" (inst -1 "s!1" "t!1" )"2" (assert )"2" (inst -1 "x!1" "r!1" )"1" (replaces -4)"1" "1" expand "member" )"1" (propax) nil nil ))nil ))nil ))nil )"2" (replaces -4)"2" "2" expand "member" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil robinsonunification nil )nil robinsonunification nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"[symbol -> nat]" robinsonunification nil )nil term_adt nil ) (set type-eq-decl nil sets nil )"set[term]" variables_term nil )"[T, T -> boolean]" equalities nil )"boolean" notequal nil )"bool" substitution nil )nil substitution nil )"Sub" robinsonunification nil )"term[variable, symbol, arity]" nil )nil substitution nil )nil robinsonunification nil )"term[variable, symbol, arity]" nil )"(V)" robinsonunification nil )"term[variable, symbol, arity]" nil )"{t: term | s!1 /= t}" robinsonunificationnil )"set[term]" substitution nil )"set[(V)]" substitution nil )"bool" sets nil ))nil 3469270552"" (skosimp)"" (assert )"" (flatten)"" "sig!1" "link_of_frst_diff(s!1,t!1)" :hide?nil )"" (expand * "subset?" )"" (skosimp)"" (expand * "union" "member" )"" (flatten)"" (case "member(x!1, VRan(sig!1))" )"1" (expand * "member" "VRan" )"1" (expand "IUnion" )"1" (skosimp)"1" (lemma "dom_link_of_frst_diff_is" )"1" "first_diff(s!1, t!1)" "s!1" "t!1" )"1" assert )"1" replace -3 -1)"1" assert )"1" expand * "restrict" "singleton" )"1" "1" "1" "i!1" )"1" "i!1" )"1" assert )"1" "1" "1" replace "1" expand "link_of_frst_diff" "1" "p!1" "first_diff(s!1, t!1)" nil )"1" "1" "1" expand "Vars" )"1" "1" "p!2" )"1" "pos_o_term" )"1" "p!1" "p!2" "t!1" )"1" assert )"1" "1" "p!1 o p!2" )"1" rewrite "pos_subterm" )nil nil ))nil )"2" "2" "2" "position_s_first_diff" )"2" "t!1" "s!1" "p!1" )"2" assert )"2" "2" rewrite "comutative_first_diff" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "link_of_frst_diff" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "1" "i!1" )"1" "i!1" )"1" assert )"1" "1" expand "V" )"1" replace "1" expand "link_of_frst_diff" "1" "p!1" "first_diff(s!1, t!1)" nil )"1" "1" "1" expand "Vars" )"1" "1" "p!2" )"1" "pos_o_term" )"1" "p!1" "p!2" "s!1" )"1" assert )"1" "1" "p!1 o p!2" )"1" rewrite "pos_subterm" )nil nil ))nil )"2" "2" "2" "position_s_first_diff" )"2" "s!1" "t!1" "p!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "link_of_frst_diff" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "member" )"2" (name "p!1" "first_diff(s!1,t!1)" )"2" (case "vars?(subtermOF(s!1,p!1))" )"1" case "VRan(sig!1) = Vars(subtermOF(t!1,p!1))" )"1" (replaces -1)"1" "link_remove_x" )"1" "x!1" "s!1" "t!1" )"1" assert )"1" replace -4 -1)"1" assert )"1" expand "member" )"1" "positions_of_ext" )"1" "sig!1" "s!1" )"1" "1" expand "Vars" -5)"1" "1" "p!2" )"1" assert )"1" expand "union" )"1" "1" expand "member" )"1" "1" rewrite "subterm_ext_commute" )"1" "1" "1" "1" expand "ext" )"1" assert )"1" "1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "x!1" )"2" expand "V" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "member" )"2" "2" replace "2" rewrite "pos_subterm" )"2" rewrite "subterm_ext_commute" )"2" expand "ext" "2" assert )"2" case "subtermOF(s!1, p1!1) = subtermOF(s!1, p!1)" )"1" replace "1" expand "link_of_frst_diff" "1" assert )"1" "1" "1" replace "1" "1" expand "Vars" )"1" "p2!1" )nil nil ))nil ))nil ))nil )"2" expand "link_of_frst_diff" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace "2" expand "link_of_frst_diff" "2" assert )"2" "2" "1" replace "1" expand "ext" "1" expand "link_of_frst_diff" "1" assert )"1" "pos_o_term" )"1" "p1!1" "p2!1" "s!1" )"1" assert )"1" "pos_subterm" )"1" "p1!1" "p2!1" "s!1" )"1" assert )"1" replace "1" "1" expand "Vars" )"1" "p1!1 o p2!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "link_of_frst_diff" "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 )"2" (decompose-equality 1)"2" "2" "1" expand "VRan" -1)"1" expand "IUnion" )"1" "1" "dom_link_of_frst_diff_is" )"1" "p!1" "s!1" "t!1" )"1" assert )"1" expand *"restrict" "singleton" )"1" replace -5 -1)"1" "1" "i!1" )"1" assert )"1" "1" replace "1" expand "link_of_frst_diff" "1" "1" "1" assert )nil nil ))nil )"2" expand "link_of_frst_diff" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "VRan" 1)"2" expand "IUnion" )"2" "subtermOF(s!1, p!1)" )"1" replace -4 1 rl)"1" expand "link_of_frst_diff" "1" "1" "1" assert )nil nil ))nil )"2" expand "link_of_frst_diff" "2" assert )nil nil ))nil ))nil ))nil ))nil )"2" expand V)"2" expand "Dom" )"2" "2" "subtermOF(s!1, p!1)" )"2" expand "link_of_frst_diff" "2" assert )"2" "2" "1" assert )"1" replace "1" replace "1" "1" "1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "sig!1 = link_of_frst_diff(s!1,t!1)" )"1" expand "1" assert )nil nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide-all-but (-2 1))"3" rewrite position_t_first_diff)nil nil ))nil ))nil )"2" (case "vars?(subtermOF(t!1,p!1))" )"1" case "VRan(sig!1) = Vars(subtermOF(s!1,p!1))" )"1" "1" "link_remove_x" )"1" "x!1" "s!1" "t!1" )"1" assert )"1" replace -4 -1)"1" assert )"1" expand "member" )"1" "positions_of_ext" )"1" "sig!1" "s!1" )"1" "1" expand "Vars" -5)"1" "1" "p!2" )"1" assert )"1" expand "union" )"1" "1" expand "member" )"1" "1" rewrite "subterm_ext_commute" )"1" "1" "1" "1" expand "ext" )"1" assert )"1" "1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "x!1" )"2" expand "V" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "member" )"2" "2" replace "2" rewrite "pos_subterm" )"2" rewrite "subterm_ext_commute" )"2" expand "ext" "2" assert )"2" case "subtermOF(s!1, p1!1) = subtermOF(t!1, p!1)" )"1" replace "1" expand "link_of_frst_diff" "1" assert )"1" "1" "1" replace "1" "1" expand "Vars" )"1" "p2!1" )nil nil ))nil ))nil ))nil )"2" expand "link_of_frst_diff" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace "2" expand "link_of_frst_diff" "2" assert )"2" "2" "1" replace "1" expand "ext" "1" expand "link_of_frst_diff" "1" assert )"1" "pos_o_term" )"1" "p1!1" "p2!1" "s!1" )"1" assert )"1" "pos_subterm" )"1" "p1!1" "p2!1" "s!1" )"1" assert )"1" replace "1" "1" expand "Vars" )"1" "p1!1 o p2!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "link_of_frst_diff" "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 )"2" "2" "2" "1" expand "VRan" -1)"1" expand "IUnion" )"1" "1" "dom_link_of_frst_diff_is" )"1" "p!1" "s!1" "t!1" )"1" assert )"1" expand *"restrict" "singleton" )"1" replace -5 -1)"1" "1" "i!1" )"1" assert )"1" "1" replace "1" expand "link_of_frst_diff" "1" "1" assert )nil nil )"2" expand "link_of_frst_diff" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "VRan" 1)"2" expand "IUnion" )"2" "subtermOF(t!1, p!1)" )"1" replace -4 1 rl)"1" expand "link_of_frst_diff" "1" "1" (assert ) nil nil )"2" expand "link_of_frst_diff" "2" assert )nil nil ))nil ))nil ))nil ))nil )"2" expand V)"2" expand "Dom" )"2" "2" "subtermOF(t!1, p!1)" )"2" expand "link_of_frst_diff" "2" assert )"2" "2" "1" assert )nil nil )"2" case "sig!1 = link_of_frst_diff(s!1,t!1)" )"1" expand "1" assert )nil nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand link_of_frst_diff)"2" (assert ) nil nil )) nil )"3" (hide-all-but (-1 1))"3" rewrite position_t_first_diff)nil nil ))nil ))nil )"3" (hide-all-but (-1 1))"3" (lemma position_s_first_diff)"3" "3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"(partial_order?[set[T]])" nil )nil robinsonunification nil )nil robinsonunification nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"[symbol -> nat]" robinsonunification nil )nil term_adt nil ) (set type-eq-decl nil sets nil )"set[term]" variables_term nil )"[T, T -> boolean]" equalities nil )"boolean" notequal nil )"bool" substitution nil )nil substitution nil )"Sub" robinsonunification nil )"[term -> boolean]" term_adt nil )"non_empty_finite_set[term]" robinsonunification nil )"finite_set[S]" nil )nil robinsonunificationnil )"Sub[variable, symbol, arity]" nil )"position[variable, symbol, arity]" nil )nil substitution nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[(vars?) -> variable]" term_adt nil )"[term -> boolean]" term_adt nil )"[(app?) -> symbol]" term_adt nil )nil finite_sequences nil )"[d: (app?) -> {args: finite_sequence[term] | args`length = arity(f(d))}]" nil )ext def-decl "term" substitution nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil substitution nil )nil robinsonunification nil )"position" robinsonunification nil )nil positions nil )nil integers nil )"bool" reals nil )nil integers nil )nil nat_types nil )"(singleton?)" sets nil )"R" restrict nil )"[bool, bool -> bool]" booleans nil )"position[variable, symbol, arity]" nil )"positions?[variable, symbol, arity](subtermOF(s!1, p!1))" nil )nil robinsonunification nil )"term" subterm nil )nil positions nil )"positions" positions nil )nil positions nil )"set[(V)]" substitution nil )nil subterm nil )nil robinsonunification nil )nil robinsonunification nil )"term[variable, symbol, arity]" nil )"{t: term | s!1 /= t}" robinsonunificationnil )nil finite_sequences nil )"finseq" finite_sequences nil )"position[variable, symbol, arity]" nil )"positions?[variable, symbol, arity](subtermOF(t!1, p!1))" nil )nil subterm nil )"set[(V)]" subterm nil )NOT const-decl "[bool -> bool]" booleans nil )nil robinsonunification nil )"set[T]" indexed_sets nil )"set[(V)]" substitution nil )"set" sets nil )"bool" sets nil )"bool" sets nil ))nil 3469378012"" (skosimp*)"" (lemma comutative_first_diff)"" (inst?)"" (assert )"" (prop)"" (inst -1 "first_diff(t!1, s!1)" )"" (expand link_of_frst_diff)"" (lift-if)"" (assert )"" (name-replace position "first_diff(s!1, t!1)" )"" (replace -1)"" (case " vars?(subtermOF(t!1, position))" )"1" (assert ) nil nil )"2" (assert ) nil nil )"3" (hide 2 3)"3" (replace -1 1 rl)"3" "3" "3" "first_diff(t!1, s!1)" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil robinsonunification nil )nil nat_types nil )nil integers nil )"bool" reals nil )nil integers nil )nil positions nil )"position" robinsonunification nil )"[T, T -> boolean]" equalities nil )"term" subterm nil )nil positions nil )"positions" positions nil )nil positions nil )"[term -> boolean]" term_adt nil )nil robinsonunification nil )"Sub" robinsonunification nil )"boolean" notequal nil )nil term_adt nil )"[symbol -> nat]" robinsonunification nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil robinsonunification nil )nil robinsonunification nil ))nil 3469369542"" (lemma comutative_link_fd)"" (lemma link_of_frst_diff_s_is_subset_union)"" (skosimp*)"" (assert )"" (case "NOT vars?(subtermOF(s!1, first_diff(s!1, t!1)))" )"1" (inst -1 t!1 s!1)"1" (inst -2 s!1 t!1)"1" (assert )"1" (prop)"1" (replace -2)"1" (hide -2 1 2)"1" (expand subset?)"1" (skosimp*)"1" (inst -1 x!1)"1" assert )"1" "1" expand * member union)"1" (prop) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (hide -3 -2)"2" (prop)"2" "sig!1" "link_of_frst_diff(s!1,t!1)" nil )"2" "p!1" "first_diff(s!1, t!1)" :hide?nil )"2" (expand * "subset?" )"2" (skosimp)"2" (expand * "union" "member" )"2" (flatten)"2" (case "member(x!1, VRan(sig!1))" )"1" expand * "member" "VRan" )"1" expand "IUnion" )"1" "1" "dom_link_of_frst_diff_is" )"1" "first_diff(s!1, t!1)" "s!1" "t!1" )"1" assert )"1" replace -3 -1)"1" assert )"1" expand *"restrict" "singleton" )"1" replace -4 -1)"1" "1" "i!1" )"1" "i!1" )"1" assert )"1" "1" "1" replace "1" expand "link_of_frst_diff" "1" "1" "1" expand "Vars" )"1" "1" "p!2" )"1" "pos_o_term" )"1" "p!1" "p!2" "t!1" )"1" assert )"1" "1" "p!1 o p!2" )"1" rewrite "pos_subterm" )"1" assert )nil nil ))nil ))nil )"2" "2" rewrite nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "link_of_frst_diff" )"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 )"2" expand "member" )"2" case "VRan(sig!1) = Vars(subtermOF(t!1,p!1))" )"1" "1" "link_remove_x" )"1" "x!1" "s!1" "t!1" )"1" assert )"1" replace -3 -1)"1" assert )"1" expand "member" )"1" "positions_of_ext" )"1" "sig!1" "t!1" )"1" "1" expand "Vars" "1" "1" "p!2" )"1" assert )"1" expand "union" )"1" "1" expand "member" )"1" "1" rewrite "subterm_ext_commute" )"1" "1" "1" "1" expand "ext" )"1" assert )"1" "1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "x!1" )"2" expand "V" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "member" )"2" "2" replace "2" rewrite "pos_subterm" )"2" rewrite "subterm_ext_commute" )"2" expand "ext" "2" assert )"2" case "subtermOF(t!1, p1!1) = subtermOF(t!1, p!1)" )"1" replace "1" expand "link_of_frst_diff" "1" assert )"1" "1" "1" replace "1" "1" expand "Vars" )"1" "p2!1" )nil nil ))nil ))nil ))nil )"2" replace "2" "2" expand "Vars" )"2" "p2!1" )nil nil ))nil ))nil ))nil )"3" expand "link_of_frst_diff" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace "2" expand "link_of_frst_diff" "2" assert )"2" "2" "1" replace "1" expand "ext" "1" expand "link_of_frst_diff" "1" assert )"1" "pos_o_term" )"1" "p!1" "p2!1" "t!1" )"1" assert )"1" "pos_subterm" )"1" "p!1" "p2!1" "t!1" )"1" case "positionsOF(t!1)(p!1)" )"1" assert )"1" assert )"1" replace "1" replace "1" "1" expand "Vars" )"1" "p!1 o p2!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand ext "2" replace "2" expand "2" assert )"2" "2" "p1!1" "p2!1" "t!1" )"2" assert )"2" "pos_subterm" )"2" "p1!1" "p2!1" "t!1" )"2" assert )"2" replace "2" "2" expand "Vars" )"2" "p1!1 o p2!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" expand "3" 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 )"2" "2" "2" "1" expand "VRan" -1)"1" expand "IUnion" )"1" "1" "dom_link_of_frst_diff_is" )"1" "p!1" "s!1" "t!1" )"1" assert )"1" expand *"restrict" "singleton" )"1" replace -4 -1)"1" "1" "i!1" )"1" assert )"1" "1" replace "1" expand "link_of_frst_diff" "1" "1" assert )nil nil )"2" expand "link_of_frst_diff" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "VRan" 1)"2" expand "IUnion" )"2" "subtermOF(s!1, p!1)" )"1" replace -3 1 rl)"1" expand "link_of_frst_diff" "1" "1" assert )nil nil )"2" expand "link_of_frst_diff" "2" assert )nil nil ))nil ))nil ))nil ))nil )"2" expand V)"2" expand "Dom" )"2" "2" "2" assert )"2" replace "2" expand *"2" "2" "subtermOF(s!1, p!1)" )"2" assert )"2" expand "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" rewrite position_t_first_diff)nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide-all-but 1)"3" (lemma position_s_first_diff)"3" (inst?) (("3" (inst?) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )nil nil )"(partial_order?[set[T]])" nil )nil robinsonunification nil )"Sub" robinsonunification nil )nil substitution nil )"bool" substitution nil )"[T, T -> boolean]" equalities nil )"set[(V)]" substitution nil )"set[T]" indexed_sets nil )nil robinsonunification nil )nil subterm nil )nil robinsonunification nil )"term[variable, symbol, arity]" nil )"{t: term | s!1 /= t}" robinsonunificationnil )nil finite_sequences nil )"finseq" finite_sequences nil )"position[variable, symbol, arity]" nil )"positions?[variable, symbol, arity](subtermOF(t!1, first_diff(s!1, t!1)))" nil )nil subterm nil )"set[(V)]" subterm nil )"set[(V)]" substitution nil )"R" restrict nil )"(singleton?)" sets nil )nil robinsonunification nil )nil substitution nil )AND const-decl "[bool, bool -> bool]" booleans nil )ext def-decl "term" substitution nil )"[d: (app?) -> {args: finite_sequence[term] | args`length = arity(f(d))}]" nil )nil finite_sequences nil )"[(app?) -> symbol]" term_adt nil )"[term -> boolean]" term_adt nil )"[(vars?) -> variable]" term_adt nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil substitution nil )"Sub[variable, symbol, arity]" nil )"finite_set[S]" nil )"non_empty_finite_set[term]" robinsonunification nil )"bool" sets nil )"set[term]" variables_term nil )set type-eq-decl nil sets nil ) (member const-decl "bool" sets nil )"set" sets nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil robinsonunification nil )nil robinsonunification nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"[symbol -> nat]" robinsonunification nil )nil term_adt nil )"[term -> boolean]" term_adt nil )nil nat_types nil )nil integers nil )"bool" reals nil )nil integers nil )nil positions nil )nil positions nil )"positions" positions nil )nil positions nil )"term" subterm nil )"boolean" notequal nil )"position" robinsonunification nil )nil robinsonunification nil ))nil 3468747509"" (skosimp*)"" (assert )"" (flatten)"" "sig!1" "link_of_frst_diff(s!1, t!1)" :hide?nil )"" (decompose-equality 2)"" (iff)"" (prop)"1" (expand "difference" )"1" (expand "union" )"1" (expand "member" )"1" (prop)"1" "link_of_frst_diff_s_is_subset_union" )"1" (inst -1 "s!1" "t!1" )"1" (assert )"1" expand "subset?" )"1" "x!1" )"1" expand * "union" "member" )nil nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "link_remove_x" )"2" (inst -1 "x!1" "s!1" "t!1" )"2" (assert )"2" assert )"2" "2" expand "member" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "link_of_frst_diff_t_is_subset_union" )"3" (inst -1 "s!1" "t!1" )"3" (assert )"3" expand "subset?" )"3" "x!1" )"3" expand * "union" "member" )nil nil ))nil ))nil ))nil ))nil ))nil )"4" (lemma "link_remove_x" )"4" (inst -1 "x!1" "s!1" "t!1" )"4" (assert )"4" assert )"4" "4" assert )"4" expand member)"4" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand * "difference" "union" "member" )"2" (prop)"1" (hide 3)"1" (expand "Vars" )"1" (skosimp)"1" (inst 2 "p!1" )"1" (rewrite "subterm_ext_commute" )"1" "1" "x!1" )"1" expand * "V" "Dom" "ext" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (hide -1 2)"2" rewrite "ext_preserv_pos" )nil nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (expand "Vars" )"2" (skosimp)"2" (inst 2 "p!1" )"1" (rewrite "subterm_ext_commute" )"1" "1" "x!1" )"1" expand * "V" "Dom" "ext" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (hide -1 2)"2" rewrite "ext_preserv_pos" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil robinsonunification nil )nil robinsonunification nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"[symbol -> nat]" robinsonunification nil )nil term_adt nil ) (set type-eq-decl nil sets nil )"set[term]" variables_term nil )"[T, T -> boolean]" equalities nil )"boolean" notequal nil )"bool" substitution nil )nil substitution nil )"Sub" robinsonunification nil )"{t: term | s!1 /= t}" robinsonunificationnil )"positions?[variable, symbol, arity](t!1)" nil )nil substitution nil )nil substitution nil )NOT const-decl "[bool -> bool]" booleans nil )nil nat_types nil )nil integers nil )"bool" reals nil )nil integers nil )nil positions nil )nil positions nil )"positions" positions nil )"Sub[variable, symbol, arity]" nil )"term[variable, symbol, arity]" nil )nil positions nil )"positions?[variable, symbol, arity](s!1)" nil )"bool" sets nil )nil nil )nil robinsonunification nil )nil nil )"(partial_order?[set[T]])" nil )"bool" sets nil )"set[(V)]" substitution nil )"set" sets nil )ext def-decl "term" substitution nil )"set[(V)]" subterm nil )"set" sets nil ))nil 3468654228"" (skosimp)"" (rewrite "finite_union" )"1" (hide -1 2) (("1" (rewrite "vars_of_term_finite" ) nil nil ))nil )"2" (hide -1 2) (("2" (rewrite "vars_of_term_finite" ) nil nil ))nil ))nil ))nil )nil finite_sets nil )"bool" finite_sets nil )nil finite_sets nil )"set[(V)]" subterm nil )"bool" substitution nil )nil substitution nil )ext def-decl "term" substitution nil )"boolean" notequal nil )nil robinsonunification nil )nil robinsonunification nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"[symbol -> nat]" robinsonunification nil )nil term_adt nil ) (set type-eq-decl nil sets nil )"set[term]" variables_term nil )nil subterm nil ))nil ))nil 3468654228"" (skosimp)"" (hide -)"" (rewrite "finite_union" )"1" (hide 2) (("1" (rewrite "vars_of_term_finite" ) nil nil ))nil )"2" (hide 2) (("2" (rewrite "vars_of_term_finite" ) nil nil ))nil ))nil ))nil ))nil )nil subterm nil )"set[term]" variables_term nil )set type-eq-decl nil sets nil ) (term type-decl nil term_adt nil )"[symbol -> nat]" robinsonunification nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil robinsonunification nil )nil robinsonunification nil )"boolean" notequal nil )"set[(V)]" subterm nil )nil finite_sets nil )"bool" finite_sets nil )nil finite_sets nil ))nil ))nil 3468683546"" (skosimp*)"" (assert )"" (prop)"" "sig1" "link_of_frst_diff(s!1, t!1)" :hide?nil )"" (lemma "card_diff_subset[(V)]" )"" (lemma "union_vars_ext_link" )"" (inst -1 "s!1" "t!1" )"" (assert )"" (replace -3 -1)"" (assert )"" (replaces -1)"" "Dom(sig1)" "union(Vars(s!1), Vars(t!1))" )"1" (prop)"1" (case-replace "card(Dom(sig1)) = 1" )"1" (assert ) nil nil )"2" "2" rewrite "card_one" )"2" "dom_link_of_frst_diff_is" )"2" "first_diff(s!1, t!1)" "s!1" "t!1" )"2" assert )"2" "1" expand "restrict" )"1" "1" "subtermOF(s!1, first_diff(s!1, t!1))" )"1" "1" "x!1" )"1" "1" replace -1 -2)"1" assert )"1" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "V" )"2" nil nil ))nil ))nil ))nil ))nil )"2" expand "restrict" )"2" case "vars?(subtermOF(t!1, first_diff(s!1, t!1)))" )"1" "subtermOF(t!1, first_diff(s!1, t!1))" )"1" "1" "1" "x!1" )"1" "1" assert )"1" replace "1" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "V" )"2" nil nil ))nil ))nil )"2" "2" "2" "2" expand "link_of_frst_diff" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"3" "3" "position_s_first_diff" )"3" "t!1" "s!1" "first_diff(s!1,t!1)" )"3" "3" "3" "comutative_first_diff" )"3" "s!1" "t!1" "first_diff(s!1, t!1)" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "dom_link_of_frst_diff_is" )"2" "first_diff(s!1,t!1)" "s!1" "t!1" )"2" assert )"2" replace -2 -1)"2" "p!1" "first_diff(s!1, t!1)" nil )"2" expand "restrict" )"2" "1" "1" "1" expand "subset?" )"1" "1" "x!1" )"1" expand "member" )"1" "1" assert )"1" expand "singleton" )"1" expand "union" )"1" "1" "1" expand *"member" "Vars" )"1" "p!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "vars?(subtermOF(t!1, p!1))" )"1" "1" expand "subset?" )"1" "1" "1" "x!1" )"1" expand "member" )"1" "1" assert )"1" "1" expand *"union" "member" )"1" "1" "1" expand "Vars" )"1" "p!1" )"1" expand "singleton" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "link_of_frst_diff" )"2" "2" assert )nil nil ))nil ))nil ))nil )"3" "3" "position_s_first_diff" )"3" "t!1" "s!1" "p!1" )"3" assert )"3" "3" "comutative_first_diff" )"3" "s!1" "t!1" "p!1" )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (typepred "sig1" )"2" (hide -2 2 3)"2" expand "Sub?" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"(strict_total_order?[real])" real_props nil )nil robinsonunification nil )nil robinsonunification nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"[symbol -> nat]" robinsonunification nil )nil term_adt nil ) (set type-eq-decl nil sets nil )"set[term]" variables_term nil )"[T, T -> boolean]" equalities nil )"boolean" notequal nil )"bool" substitution nil )nil substitution nil )"Sub" robinsonunification nil )nil robinsonunification nil )"bool" finite_sets nil )"set[(V)]" substitution nil )"Sub[variable, symbol, arity]" nil )nil finite_sets nil )"set" sets nil )"set[(V)]" subterm nil )"(partial_order?[set[T]])" nil )"bool" sets nil )"bool" sets nil )"{n: nat | n = Card(S)}" finite_sets nil )"nat" finite_sets nil )"int" integers nil )nil finite_sets nil )"position" robinsonunification nil )nil positions nil )nil integers nil )"bool" reals nil )nil integers nil )nil nat_types nil )"term" subterm nil )nil positions nil )"positions" positions nil )nil positions nil )"(singleton?)" sets nil )"bool" sets nil )"non_empty_finite_set[term]" robinsonunification nil )"non_empty_finite_set" robinsonunification nil )"posint" nil )"{t: term | s!1 /= t}" robinsonunificationnil )"term[variable, symbol, arity]" nil )"R" restrict nil )"[term -> boolean]" term_adt nil )nil robinsonunification nil )nil robinsonunification nil )nil robinsonunification nil )NOT const-decl "[bool -> bool]" booleans nil )nil finite_sets nil ))nil 3469312693"" (skosimp)"" (assert )"" (name "sig!1" "link_of_frst_diff(s!1, t!1)" )"" (prop)"" (expand link_of_frst_diff -3)"" (lift-if)"" (prop)"1" (name "p!1" "first_diff(s!1, t!1)" )"1" (replace -1)"1" (decompose-equality -2)"1" (case "xx = subtermOF(s!1, p!1)" )"1" (inst -2 "xx" )"1" (assert )"1" (expand fail -2)"1" replace -1 1 rl)"1" replace -2 1)"1" "1" expand * member Vars)"1" "#(1)" )"1" expand subtermOF 1)"1" rewrite empty_0)"1" "1" "1" "1" nil nil ))nil )"2" expand finseq_appl)"2" case "#(xx)`seq(first( #(1)) - 1) = xx" )"1" replace -1 2)"1" case "rest( #(1)) = empty_seq" )"1" replace "1" "1" expand "1" rewrite nil nil ))nil ))nil ))nil )"2" "2" "2" "#(1)" )"2" "1" "1" rewrite nil nil ))nil )"2" expand "#" "2" assert )nil nil ))nil )"3" expand "#" "3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "#" )"2" nil nil ))nil ))nil )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand positionsOF)"2" assert )"2" expand *"2" "1" expand "#" )"1" assert )nil nil ))nil )"2" "2" "1" expand catenate)"1" expand "1" "1" "1" expand "1" expand "1" "1" "1" expand "1" nil nil ))nil )"2" expand "2" nil nil ))nil )"3" expand *nil nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (inst -1 "subtermOF(s!1, p!1)" )"2" (expand fail)"2" (assert )"2" expand id)"2" "2" "2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma var_term_unifiable_not_var_in_term)"2" "subtermOF(s!1, first_diff(s!1, t!1))" "subtermOF(t!1, first_diff(s!1, t!1))" )"2" (assert )"2" (hide -1 -2)"2" (split)"1" (lemma unifiable_terms_unifiable_args)"1" (expand unifiable)"1" "1" "1" "first_diff(s!1, t!1)" )"1" expand * member U)"1" (assert ) nil nil ))nil )"2" "2" rewrite position_t_first_diff)"2" "2" "2" (inst?) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma first_diff_has_diff_argument)"2" (inst?) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"3" (decompose-equality -1)"3" (name "p!1" "first_diff(s!1, t!1)" )"3" (replace -1)"3" (case "xx = subtermOF(t!1, p!1)" )"1" (inst -3 "subtermOF(t!1, p!1)" )"1" (expand fail)"1" (assert )"1" replace -1 1 rl)"1" replace -3 1)"1" "1" expand * member Vars)"1" "#(1)" )"1" expand subtermOF 1)"1" rewrite empty_0)"1" "1" "1" "1" nil nil ))nil )"2" expand finseq_appl)"2" case "#(xx)`seq(first( #(1)) - 1) = xx" )"1" replace -1 2)"1" case "rest( #(1)) = empty_seq" )"1" replace "1" "1" expand "1" rewrite nil nil ))nil ))nil ))nil )"2" "2" "2" "#(1)" )"2" "1" "1" rewrite nil nil ))nil )"2" expand "#" "2" assert )nil nil ))nil )"3" expand "#" "3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "#" )"2" nil nil ))nil ))nil )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand positionsOF)"2" assert )"2" expand *"2" "1" "1" nil nil ))nil )"2" "2" "1" expand catenate)"1" expand "1" "1" "1" expand "1" expand "1" "1" "1" expand "1" nil nil ))nil )"2" expand "2" nil nil ))nil )"3" expand *nil nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (inst -2 "subtermOF(t!1, p!1)" )"2" (expand fail)"2" (assert )"2" expand id)"2" "2" "2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" (lemma var_term_unifiable_not_var_in_term)"4" "subtermOF(t!1, first_diff(s!1, t!1))" "subtermOF(s!1, first_diff(s!1, t!1))" )"4" (assert )"4" (hide -1 -2 -3 2)"4" (lemma unifiable_terms_unifiable_args)"4" (expand unifiable)"4" (skosimp)"4" "4" "first_diff(s!1, t!1)" )"1" expand * member U)"1" assert )"1" "1" expand unifier)"1" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" "2" rewrite position_t_first_diff)"2" "2" "first_diff(s!1, t!1)" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"5" (lemma first_diff_unifiable_vars)"5" (inst -1 s!1 t!1 "first_diff(s!1, t!1)" )"5" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil robinsonunificationnil )"bool" unification nil )nil unificationnil )"bool" unification nil )nil robinsonunification nil )nil robinsonunification nil )"set[Sub]" unification nil )"{t: term | s!1 /= t}" robinsonunificationnil )"term[variable, symbol, arity]" nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil unification nil )"position" robinsonunification nil )nil positions nil )nil integers nil )"bool" reals nil )nil integers nil )nil nat_types nil )IF const-decl "[boolean, T, T -> T]" if_def nil )nil positions nil )"positions" positions nil )nil positions nil )"term" subterm nil )"Sub" robinsonunification nil )nil robinsonunificationnil )"(bijective?[T, T])" identity nil )"set[(V)]" subterm nil )"bool" sets nil )"set[T]" indexed_sets nil )"set" sets nil )"positions" positions nil )"finseq" seq_extras "structures/" )"finseq" seq_extras "structures/" )"positions" positions nil )nil IUnion_extra nil )"bool" reals nil )"(total_order?[real])" nil )"[below[length(fs)] -> T]" finite_sequencesnil )nil seq_extras "structures/" )"finseq" seq_extras "structures/" )"(total_order?[real])" nil )"T" seq_extras "structures/" )nil seq_extras "structures/" )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"int" integers nil )"finseq" finite_sequences nil )"posint" nil )nil seq_extras "structures/" )nil finite_sequences nil )"finite_sequence[T]" set2seq "structures/" )"{f: symbol | arity(f) = 1}" robinsonunificationnil )"[[f: symbol, {args: finite_sequence[term] | args`length = arity(f)}] -> " term_adt nil) "[term -> boolean]" term_adt nil )nil finite_sequences nil )"(V)" robinsonunification nil )nil robinsonunification nil )nil robinsonunification nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"[symbol -> nat]" robinsonunification nil )nil term_adt nil ) (set type-eq-decl nil sets nil )"set[term]" variables_term nil )"[T, T -> boolean]" equalities nil )"boolean" notequal nil )"bool" substitution nil )nil substitution nil )"Sub" robinsonunification nil ))nil 3469363975"" (skosimp)"" (assert )"" (inst 1 rho!1)"" "sig!1" "link_of_frst_diff(s!1, t!1)" :hide?nil )"" (decompose-equality 1)"" (copy -1)"" (expand link_of_frst_diff -1)"" (lift-if)"" (prop)"1" "p!1" "first_diff(s!1, t!1)" :hide?nil )"1" (decompose-equality -2)"1" (inst -1 x!1)"1" (lift-if)"1" (prop)"1" expand comp 2)"1" replace -2 2 rl)"1" replace -1 2)"1" "1" "1" assert )"1" "1" expand *"1" expand ext -1 1)"1" nil nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "2"
Messung V0.5 in Prozent C=100 H=100 G=100
¤ 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.1.257Bemerkung:
(vorverarbeitet am 2026-04-27)
¤ *Bot Zugriff
2026-05-26
