| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/TRS/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 569 kB |
|
Impressum unification.prfSprache: Lisp |
|||||||||||||||
|
(unification (IMP_substitution_TCC1 0 (IMP_substitution_TCC1-1 nil 3463226130 ("" (lemma "var_countable") (("" (propax) nil nil)) nil) ((var_countable formula-decl nil unification nil)) nil)) (mg_po 0 (mg_po-1 nil 3455279452 ("" (expand "preorder?") (("" (split) (("1" (expand "reflexive?") (("1" (skeep) (("1" (expand "<=") (("1" (inst 1 "identity") (("1" (decompose-equality) (("1" (expand "comp") (("1" (rewrite "ext_iden") nil nil)) nil)) nil) ("2" (rewrite "iden_subs") nil nil)) nil)) nil)) nil)) nil) ("2" (expand "transitive?") (("2" (skeep) (("2" (expand "<=") (("2" (skosimp*) (("2" (inst 1 "comp(tau!2,tau!1)") (("1" (replaces -1) (("1" (replaces -1) (("1" (rewrite "o_ass") nil nil)) nil)) nil) ("2" (rewrite "subs_o") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((identity const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (Sub? const-decl "bool" substitution nil) (V const-decl "set[term]" variables_term nil) (set type-eq-decl nil sets nil) (term type-decl nil term_adt nil) (arity formal-const-decl "[symbol -> nat]" unification nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (symbol formal-nonempty-type-decl nil unification nil) (variable formal-nonempty-type-decl nil unification nil) (Sub type-eq-decl nil substitution nil) (ext_iden formula-decl nil substitution nil) (comp const-decl "term" substitution nil) (iden_subs formula-decl nil substitution nil) (<= const-decl "bool" unification nil) (reflexive? const-decl "bool" relations nil) (subs_o formula-decl nil substitution nil) (o_ass formula-decl nil substitution nil) (tau!2 skolem-const-decl "Sub[variable, symbol, arity]" unification nil) (tau!1 skolem-const-decl "Sub[variable, symbol, arity]" unification nil) (transitive? const-decl "bool" relations nil) (preorder? const-decl "bool" orders nil)) shostak)) (uni_diff_equal_length_arg 0 (uni_diff_equal_length_arg-1 nil 3448191147 ("" (skosimp*) (("" (typepred t!1) (("" (expand unifiable) (("" (skeep -1) (("" (expand unifier) (("" (replace -2 -1) (("" (replace -3 -1) (("" (expand ext) (("" (lift-if) (("" (assert) (("" (decompose-equality -1) (("" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((/= const-decl "boolean" notequal nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (unifiable const-decl "bool" unification nil) (term type-decl nil term_adt nil) (arity formal-const-decl "[symbol -> nat]" unification nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (symbol formal-nonempty-type-decl nil unification nil) (variable formal-nonempty-type-decl nil unification nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (ext def-decl "term" substitution nil) (args adt-accessor-decl "[d: (app?) -> {args: finite_sequence[term] | args`length = arity(f(d))}]" term_adt nil) (f adt-accessor-decl "[(app?) -> symbol]" term_adt nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (finseq type-eq-decl nil finite_sequences nil) (Sub type-eq-decl nil substitution nil) (Sub? const-decl "bool" substitution nil) (V const-decl "set[term]" variables_term nil) (set type-eq-decl nil sets nil) (< const-decl "bool" reals nil) (app adt-constructor-decl "[[f: symbol, {args: finite_sequence[term] | args`length = arity(f)}] -> (app?)]" term_adt nil) (finite_sequence type-eq-decl nil finite_sequences nil) (below type-eq-decl nil nat_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (app? adt-recognizer-decl "[term -> boolean]" term_adt nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (unifier const-decl "bool" unification nil)) shostak)) (resolving_diff_TCC1 0 (resolving_diff_TCC1-1 nil 3447690997 ("" (skosimp*) (("" (lemma "positions_of_arg") (("" (inst -1 "s!1" "k!1") (("1" (typepred "k!1") (("1" (lemma "uni_diff_equal_length_arg") (("1" (inst -1 "s!1" "t!1" "f!1" "st!1") (("1" (assert) (("1" (inst -1 "fp!1" "stp!1") (("1" (assert) (("1" (flatten) (("1" (replace -4 1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ((arity formal-const-decl "[symbol -> nat]" unification nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (symbol formal-nonempty-type-decl nil unification nil) (variable formal-nonempty-type-decl nil unification nil) (positions_of_arg formula-decl nil positions nil) (NOT const-decl "[bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (unifiable const-decl "bool" unification nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (uni_diff_equal_length_arg formula-decl nil unification nil) (fp!1 skolem-const-decl "symbol" unification nil) (stp!1 skolem-const-decl "{args: finite_sequence[term[variable, symbol, arity]] | args`length = arity(fp!1)}" unification nil) (k!1 skolem-const-decl "below[length(stp!1)]" unification nil) (s!1 skolem-const-decl "term[variable, symbol, arity]" unification nil) (args adt-accessor-decl "[d: (app?) -> {args: finite_sequence[term] | args`length = arity(f(d))}]" term_adt nil) (f adt-accessor-decl "[(app?) -> symbol]" term_adt nil) (= const-decl "[T, T -> boolean]" equalities nil) (finite_sequence type-eq-decl nil finite_sequences nil) (below type-eq-decl nil nat_types nil) (< const-decl "bool" reals nil) (app? adt-recognizer-decl "[term -> boolean]" term_adt nil) (term type-decl nil term_adt nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (resolving_diff_TCC2 0 (resolving_diff_TCC2-1 nil 3447690997 ("" (skosimp*) (("" (lemma "positions_of_arg") (("" (inst -1 "t!1" "k!1") (("1" (typepred "k!1") (("1" (replace -3 1) (("1" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ((arity formal-const-decl "[symbol -> nat]" unification nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (symbol formal-nonempty-type-decl nil unification nil) (variable formal-nonempty-type-decl nil unification nil) (positions_of_arg formula-decl nil positions nil) (NOT const-decl "[bool -> bool]" booleans nil) (fp!1 skolem-const-decl "symbol" unification nil) (stp!1 skolem-const-decl "{args: finite_sequence[term[variable, symbol, arity]] | args`length = arity(fp!1)}" unification nil) (k!1 skolem-const-decl "below[length(stp!1)]" unification nil) (s!1 skolem-const-decl "term[variable, symbol, arity]" unification nil) (t!1 skolem-const-decl "{t: term | unifiable(s!1, t) & s!1 /= t}" unification nil) (args adt-accessor-decl "[d: (app?) -> {args: finite_sequence[term] | args`length = arity(f(d))}]" term_adt nil) (f adt-accessor-decl "[(app?) -> symbol]" term_adt nil) (= const-decl "[T, T -> boolean]" equalities nil) (finite_sequence type-eq-decl nil finite_sequences nil) (below type-eq-decl nil nat_types nil) (< const-decl "bool" reals nil) (/= const-decl "boolean" notequal nil) (unifiable const-decl "bool" unification nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (app? adt-recognizer-decl "[term -> boolean]" term_adt nil) (term type-decl nil term_adt nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (resolving_diff_TCC3 0 (resolving_diff_TCC3-1 nil 3447690997 ("" (skosimp*) (("" (assert) (("" (typepred "t!1") (("" (expand "unifiable" -1) (("" (skeep -1) (("" (replace -2 -1) (("" (replace -3 -1) (("" (expand "unifier" -1) (("" (decompose-equality -1) (("" (assert) (("" (prop) (("1" (hide-all-but (-1 -2 -4 -5)) (("1" (expand "ext") (("1" (propax) nil nil)) nil)) nil) ("2" (expand "ext" -3) (("2" (replace -3 (-2 -4 -6) rl) (("2" (expand "ext" -4) (("2" (flatten) (("2" (decompose-equality -5) (("2" (inst -1 "k!1") (("1" (expand "unifiable") (("1" (inst 3 "sigma") (("1" (grind) nil nil)) nil)) nil) ("2" (expand "unifiable") (("2" (inst 4 "sigma") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nnint_plus_posint_is_posint application-judgement "posint" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (unifier const-decl "bool" unification nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (finseq type-eq-decl nil finite_sequences nil) (< const-decl "bool" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nat_min application-judgement "{k: nat | k <= i AND k <= j}" real_defs nil) (int_min application-judgement "{k: int | k <= i AND k <= j}" real_defs nil) (int_minus_int_is_int application-judgement "int" integers nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (|#| const-decl "finite_sequence[T]" set2seq "structures/") (first const-decl "T" seq_extras "structures/") (empty_seq const-decl "finseq" finite_sequences nil) (^ const-decl "finseq" finite_sequences nil) (rest const-decl "finseq" seq_extras "structures/") (subtermOF def-decl "term" subterm nil) (st!1 skolem-const-decl "{args: finite_sequence[term[variable, symbol, arity]] | args`length = arity(f!1)}" unification nil) (f!1 skolem-const-decl "symbol" unification nil) (k!1 skolem-const-decl "below[length(stp!1)]" unification nil) (stp!1 skolem-const-decl "{args: finite_sequence[term[variable, symbol, arity]] | args`length = arity(fp!1)}" unification nil) (fp!1 skolem-const-decl "symbol" unification nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (args adt-accessor-decl "[d: (app?) -> {args: finite_sequence[term] | args`length = arity(f(d))}]" term_adt nil) (f adt-accessor-decl "[(app?) -> symbol]" term_adt nil) (v adt-accessor-decl "[(vars?) -> variable]" term_adt nil) (app adt-constructor-decl "[[f: symbol, {args: finite_sequence[term] | args`length = arity(f)}] -> (app?)]" term_adt nil) (app? adt-recognizer-decl "[term -> boolean]" term_adt nil) (= const-decl "[T, T -> boolean]" equalities nil) (finite_sequence type-eq-decl nil finite_sequences nil) (below type-eq-decl nil nat_types nil) (ext def-decl "term" substitution nil) (Sub type-eq-decl nil substitution nil) (Sub? const-decl "bool" substitution nil) (V const-decl "set[term]" variables_term nil) (set type-eq-decl nil sets nil) (vars? adt-recognizer-decl "[term -> boolean]" term_adt nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (variable formal-nonempty-type-decl nil unification nil) (symbol formal-nonempty-type-decl nil unification nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (arity formal-const-decl "[symbol -> nat]" unification nil) (term type-decl nil term_adt nil) (unifiable const-decl "bool" unification nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil)) nil)) (resolving_diff_TCC4 0 (resolving_diff_TCC4-1 nil 3449937385 ("" (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" (lemma "uni_diff_equal_length_arg") (("2" (inst -1 "s!1" "t!1" "f!1" "st!1") (("2" (assert) (("2" (inst -1 "fp!1" "stp!1") (("2" (assert) (("2" (flatten) (("2" (replace -3 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((<< adt-def-decl "(strict_well_founded?[term])" term_adt nil) (uni_diff_equal_length_arg formula-decl nil unification nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (unifiable const-decl "bool" unification nil) (/= const-decl "boolean" notequal nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (int_min application-judgement "{k: int | k <= i AND k <= j}" real_defs nil) (nat_min application-judgement "{k: nat | k <= i AND k <= j}" real_defs nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (subterm adt-def-decl "boolean" term_adt nil) (subtermOF def-decl "term" subterm nil) (rest const-decl "finseq" seq_extras "structures/") (^ const-decl "finseq" finite_sequences nil) (empty_seq const-decl "finseq" finite_sequences nil) (first const-decl "T" seq_extras "structures/") (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (|#| const-decl "finite_sequence[T]" set2seq "structures/") (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (bool nonempty-type-eq-decl nil booleans nil) (< const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (variable formal-nonempty-type-decl nil unification nil) (symbol formal-nonempty-type-decl nil unification nil) (arity formal-const-decl "[symbol -> nat]" unification nil) (term type-decl nil term_adt nil) (finite_sequence type-eq-decl nil finite_sequences nil) (= const-decl "[T, T -> boolean]" equalities nil) (fp!1 skolem-const-decl "symbol" unification nil) (stp!1 skolem-const-decl "{args: finite_sequence[term[variable, symbol, arity]] | args`length = arity(fp!1)}" unification nil) (k!1 skolem-const-decl "below[length(stp!1)]" unification nil) (app? adt-recognizer-decl "[term -> boolean]" term_adt nil) (f adt-accessor-decl "[(app?) -> symbol]" term_adt nil) (args adt-accessor-decl "[d: (app?) -> {args: finite_sequence[term] | args`length = arity(f(d))}]" term_adt nil) (s!1 skolem-const-decl "term[variable, symbol, arity]" unification nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) shostak)) (resolving_diff_TCC5 0 (resolving_diff_TCC5-1 nil 3449937623 ("" (skosimp*) (("" (lemma "positions_of_arg") (("" (inst -1 "s!1" "kk!1") (("1" (typepred "kk!1") (("1" (lemma "uni_diff_equal_length_arg") (("1" (inst -1 "s!1" "t!1" "f!1" "st!1") (("1" (assert) (("1" (inst -1 "fp!1" "stp!1") (("1" (assert) (("1" (flatten) (("1" (replace -4 1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ((arity formal-const-decl "[symbol -> nat]" unification nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (symbol formal-nonempty-type-decl nil unification nil) (variable formal-nonempty-type-decl nil unification nil) (positions_of_arg formula-decl nil positions nil) (NOT const-decl "[bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (unifiable const-decl "bool" unification nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (uni_diff_equal_length_arg formula-decl nil unification nil) (fp!1 skolem-const-decl "symbol" unification nil) (stp!1 skolem-const-decl "{args: finite_sequence[term[variable, symbol, arity]] | args`length = arity(fp!1)}" unification nil) (kk!1 skolem-const-decl "below[length(stp!1)]" unification nil) (s!1 skolem-const-decl "term[variable, symbol, arity]" unification nil) (args adt-accessor-decl "[d: (app?) -> {args: finite_sequence[term] | args`length = arity(f(d))}]" term_adt nil) (f adt-accessor-decl "[(app?) -> symbol]" term_adt nil) (= const-decl "[T, T -> boolean]" equalities nil) (finite_sequence type-eq-decl nil finite_sequences nil) (below type-eq-decl nil nat_types nil) (< const-decl "bool" reals nil) (app? adt-recognizer-decl "[term -> boolean]" term_adt nil) (term type-decl nil term_adt nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) shostak)) (resolving_diff_TCC6 0 (resolving_diff_TCC6-1 nil 3516387398 ("" (skosimp*) (("" (lemma "positions_of_arg") (("" (inst -1 "t!1" "kk!1") (("1" (typepred "kk!1") (("1" (replace -3 1) (("1" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ((arity formal-const-decl "[symbol -> nat]" unification nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (symbol formal-nonempty-type-decl nil unification nil) (variable formal-nonempty-type-decl nil unification nil) (positions_of_arg formula-decl nil positions nil) (NOT const-decl "[bool -> bool]" booleans nil) (fp!1 skolem-const-decl "symbol" unification nil) (stp!1 skolem-const-decl "{args: finite_sequence[term[variable, symbol, arity]] | args`length = arity(fp!1)}" unification nil) (kk!1 skolem-const-decl "below[length(stp!1)]" unification nil) (s!1 skolem-const-decl "term[variable, symbol, arity]" unification nil) (t!1 skolem-const-decl "{t: term | unifiable(s!1, t) & s!1 /= t}" unification nil) (args adt-accessor-decl "[d: (app?) -> {args: finite_sequence[term] | args`length = arity(f(d))}]" term_adt nil) (f adt-accessor-decl "[(app?) -> symbol]" term_adt nil) (= const-decl "[T, T -> boolean]" equalities nil) (finite_sequence type-eq-decl nil finite_sequences nil) (below type-eq-decl nil nat_types nil) (< const-decl "bool" reals nil) (/= const-decl "boolean" notequal nil) (unifiable const-decl "bool" unification nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (app? adt-recognizer-decl "[term -> boolean]" term_adt nil) (term type-decl nil term_adt nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (resolving_diff_TCC7 0 (resolving_diff_TCC7-1 nil 3516387398 ("" (skosimp*) (("" (lemma "uni_diff_equal_length_arg") (("" (inst -1 "s!1" "t!1" "f!1" "st!1") (("" (assert) (("" (inst -1 "fp!1" "stp!1") (("" (assert) (("" (flatten) (("" (replace -1 -4 rl) (("" (hide -1) (("" (typepred t!1) (("" (hide -1) (("" (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 -6 "x!1") (("2" (expand "member") (("2" (replace -5 -6) (("2" (replace -4 -6) (("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)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((uni_diff_equal_length_arg formula-decl nil unification nil) (NOT const-decl "[bool -> bool]" booleans nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (< const-decl "bool" reals nil) (empty? const-decl "bool" sets nil) (nonempty? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (subtermOF def-decl "term" subterm nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (|#| const-decl "finite_sequence[T]" set2seq "structures/") (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (first const-decl "T" seq_extras "structures/") (empty_seq const-decl "finseq" finite_sequences nil) (^ const-decl "finseq" finite_sequences nil) (rest const-decl "finseq" seq_extras "structures/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nat_min application-judgement "{k: nat | k <= i AND k <= j}" real_defs nil) (int_min application-judgement "{k: int | k <= i AND k <= j}" real_defs nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (= const-decl "[T, T -> boolean]" equalities nil) (finite_sequence type-eq-decl nil finite_sequences nil) (below type-eq-decl nil nat_types nil) (/= const-decl "boolean" notequal nil) (unifiable const-decl "bool" unification nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (term type-decl nil term_adt nil) (arity formal-const-decl "[symbol -> nat]" unification nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (symbol formal-nonempty-type-decl nil unification nil) (variable formal-nonempty-type-decl nil unification nil)) nil)) (resol_diff_nonempty_implies_funct_terms 0 (resol_diff_nonempty_implies_funct_terms-1 nil 3450707436 ("" (skeep) (("" (expand "resolving_diff") (("" (lift-if) (("" (prop) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ((resolving_diff def-decl "position" unification nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil)) shostak)) (resol_diff_to_rest_resol_diff_TCC1 0 (resol_diff_to_rest_resol_diff_TCC1-1 nil 3451131001 ("" (skeep) (("" (lemma "empty_0[posnat]") (("" (inst -1 "rd") (("" (assert) nil nil)) nil)) nil)) nil) ((posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (empty_0 formula-decl nil seq_extras "structures/") (position type-eq-decl nil positions nil) (arity formal-const-decl "[symbol -> nat]" unification nil) (symbol formal-nonempty-type-decl nil unification nil) (variable formal-nonempty-type-decl nil unification nil) (finseq type-eq-decl nil finite_sequences nil) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil)) nil)) (resol_diff_to_rest_resol_diff_TCC2 0 (resol_diff_to_rest_resol_diff_TCC2-1 nil 3451131001 ("" (skosimp) (("" (expand "resolving_diff" -1) (("" (lift-if) (("" (prop) (("" (assert) (("" (replace -1 5) (("" (rewrite "first_add") (("1" (hide -1 4) (("1" (lemma "resolving_diff_TCC1") (("1" (inst -1 "s!1" "t!1" "f(s!1)" "args(s!1)") (("1" (assert) (("1" (case "s!1 = app( f(s!1), args(s!1))") (("1" (assert) (("1" (inst -2 "f(t!1)" "args(t!1)") (("1" (case "t!1 = app( f(t!1), args(t!1))") (("1" (assert) (("1" (inst -3 "min({kk: below[length(args(t!1))] | NOT subtermOF(s!1, #(1 + kk)) = subtermOF(t!1, #(1 + kk))})") (("1" (hide 5 2 3 4 5) (("1" (lemma "resolving_diff_TCC7") (("1" (inst -1 "s!1" "t!1" "f(s!1)" "args(s!1)") (("1" (assert) (("1" (inst -1 "f(t!1)" "args(t!1)") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2 3 4 5) (("2" (skosimp*) (("2" (lemma "positions_of_arg") (("2" (inst -1 "t!1" "kk!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (hide 2 3 4 5) (("3" (skosimp*) (("3" (lemma "positions_of_arg") (("3" (inst -1 "s!1" "kk!1") (("1" (assert) nil nil) ("2" (typepred "kk!1") (("2" (lemma "uni_diff_equal_length_arg") (("2" (inst -1 "s!1" "t!1" "f(s!1)" "args(s!1)") (("2" (assert) (("2" (inst -1 "f(t!1)" "args(t!1)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 2)) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 4)) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 5 6) (("2" (lemma "resolving_diff_TCC7") (("2" (inst -1 "s!1" "t!1" "f(s!1)" "args(s!1)") (("2" (assert) (("2" (case "s!1 = app( f(s!1), args(s!1))") (("1" (assert) (("1" (inst -2 "f(t!1)" "args(t!1)") (("1" (case "t!1 = app( f(t!1), args(t!1))") (("1" (assert) nil nil) ("2" (hide-all-but (1 3)) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 5)) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide -1 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 -1 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" (lemma "uni_diff_equal_length_arg") (("2" (inst -1 "s!1" "t!1" "f(s!1)" "args(s!1)") (("2" (assert) (("2" (case "s!1 = app( f(s!1), args(s!1))") (("1" (assert) (("1" (inst -2 "f(t!1)" "args(t!1)") (("1" (assert) (("1" (hide-all-but (1 4)) (("1" (decompose-equality) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 6)) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((resolving_diff def-decl "position" unification nil) (kk!1 skolem-const-decl "below[length(args[variable, symbol, arity](t!1))]" unification nil) (app adt-constructor-decl "[[f: symbol, {args: finite_sequence[term] | args`length = arity(f)}] -> (app?)]" term_adt nil) (term_app_extensionality formula-decl nil term_adt nil) (uni_diff_equal_length_arg formula-decl nil unification nil) (kk!1 skolem-const-decl "below[length(args[variable, symbol, arity](t!1))]" unification nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (positions_of_arg formula-decl nil positions nil) (resolving_diff_TCC7 subtype-tcc nil unification nil) (t!1 skolem-const-decl "{t: term | unifiable(s!1, t) & s!1 /= t}" unification nil) (s!1 skolem-const-decl "term[variable, symbol, arity]" unification nil) (resolving_diff_TCC1 subtype-tcc nil unification nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (min const-decl "{a | S(a) AND (FORALL x: S(x) IMPLIES a <= x)}" min_nat nil) (<= const-decl "bool" reals nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (nonempty? const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (args adt-accessor-decl "[d: (app?) -> {args: finite_sequence[term] | args`length = arity(f(d))}]" term_adt nil) (f adt-accessor-decl "[(app?) -> symbol]" term_adt nil) (= const-decl "[T, T -> boolean]" equalities nil) (app? adt-recognizer-decl "[term -> boolean]" term_adt nil) (< const-decl "bool" reals nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (|#| const-decl "finite_sequence[T]" set2seq "structures/") (finite_sequence type-eq-decl nil finite_sequences nil) (subtermOF def-decl "term" subterm nil) (positions? type-eq-decl nil positions nil) (positionsOF def-decl "positions" positions nil) (positions type-eq-decl nil positions nil) (position type-eq-decl nil positions nil) (/= const-decl "boolean" notequal nil) (unifiable const-decl "bool" unification nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (term type-decl nil term_adt nil) (arity formal-const-decl "[symbol -> nat]" unification nil) (symbol formal-nonempty-type-decl nil unification nil) (variable formal-nonempty-type-decl nil unification nil) (finseq type-eq-decl nil finite_sequences nil) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (first_add formula-decl nil seq_extras "structures/") (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil)) nil)) (resol_diff_to_rest_resol_diff_TCC3 0 (resol_diff_to_rest_resol_diff_TCC3-1 nil 3451131001 ("" (skosimp) (("" (expand "resolving_diff") (("" (lift-if) (("" (prop) (("" (assert) (("" (replace -1 5) (("" (rewrite "first_add") (("1" (hide -1 4) (("1" (lemma "resolving_diff_TCC2") (("1" (inst -1 "s!1" "t!1" "f(s!1)" "args(s!1)") (("1" (assert) (("1" (case "s!1 = app( f(s!1), args(s!1))") (("1" (assert) (("1" (inst -2 "f(t!1)" "args(t!1)") (("1" (case "t!1 = app( f(t!1), args(t!1))") (("1" (assert) (("1" (inst -3 "min({kk: below[length(args(t!1))] | NOT subtermOF(s!1, #(1 + kk)) = subtermOF(t!1, #(1 + kk))})") (("1" (hide 2 3 4 5) (("1" (lemma "resolving_diff_TCC7") (("1" (inst -1 "s!1" "t!1" "f(s!1)" "args(s!1)") (("1" (assert) (("1" (inst -1 "f(t!1)" "args(t!1)") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2 3 4 5) (("2" (skosimp*) (("2" (lemma "positions_of_arg") (("2" (inst -1 "t!1" "kk!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (hide 2 3 4 5) (("3" (skosimp*) (("3" (lemma "positions_of_arg") (("3" (inst -1 "s!1" "kk!1") (("1" (assert) nil nil) ("2" (typepred "kk!1") (("2" (lemma "uni_diff_equal_length_arg") (("2" (inst -1 "s!1" "t!1" "f(s!1)" "args(s!1)") (("2" (assert) (("2" (inst -1 "f(t!1)" "args(t!1)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 2)) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 4)) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 5 6) (("2" (lemma "resolving_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" (inst -2 "f(t!1)" "args(t!1)") (("1" (case "t!1 = app( f(t!1), args(t!1))") (("1" (assert) nil nil) ("2" (hide-all-but (1 3)) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 5)) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide -1 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 -1 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" (lemma "uni_diff_equal_length_arg") (("2" (inst -1 "s!1" "t!1" "f(s!1)" "args(s!1)") (("2" (assert) (("2" (case "s!1 = app( f(s!1), args(s!1))") (("1" (assert) (("1" (inst -2 "f(t!1)" "args(t!1)") (("1" (assert) (("1" (hide-all-but (1 5)) (("1" (decompose-equality) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 6)) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((resolving_diff def-decl "position" unification nil) (kk!1 skolem-const-decl "below[length(args[variable, symbol, arity](t!1))]" unification nil) (app adt-constructor-decl "[[f: symbol, {args: finite_sequence[term] | args`length = arity(f)}] -> (app?)]" term_adt nil) (term_app_extensionality formula-decl nil term_adt nil) (uni_diff_equal_length_arg formula-decl nil unification nil) (kk!1 skolem-const-decl "below[length(args[variable, symbol, arity](t!1))]" unification nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (positions_of_arg formula-decl nil positions nil) (resolving_diff_TCC7 subtype-tcc nil unification nil) (t!1 skolem-const-decl "{t: term | unifiable(s!1, t) & s!1 /= t}" unification nil) (s!1 skolem-const-decl "term[variable, symbol, arity]" unification nil) (resolving_diff_TCC2 subtype-tcc nil unification nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (min const-decl "{a | S(a) AND (FORALL x: S(x) IMPLIES a <= x)}" min_nat nil) (<= const-decl "bool" reals nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (nonempty? const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (args adt-accessor-decl "[d: (app?) -> {args: finite_sequence[term] | args`length = arity(f(d))}]" term_adt nil) (f adt-accessor-decl "[(app?) -> symbol]" term_adt nil) (= const-decl "[T, T -> boolean]" equalities nil) (app? adt-recognizer-decl "[term -> boolean]" term_adt nil) (< const-decl "bool" reals nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (|#| const-decl "finite_sequence[T]" set2seq "structures/") (finite_sequence type-eq-decl nil finite_sequences nil) (subtermOF def-decl "term" subterm nil) (positions? type-eq-decl nil positions nil) (positionsOF def-decl "positions" positions nil) (positions type-eq-decl nil positions nil) (position type-eq-decl nil positions nil) (/= const-decl "boolean" notequal nil) (unifiable const-decl "bool" unification nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (term type-decl nil term_adt nil) (arity formal-const-decl "[symbol -> nat]" unification nil) (symbol formal-nonempty-type-decl nil unification nil) (variable formal-nonempty-type-decl nil unification nil) (finseq type-eq-decl nil finite_sequences nil) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (first_add formula-decl nil seq_extras "structures/") (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil)) nil)) (resol_diff_to_rest_resol_diff_TCC4 0 (resol_diff_to_rest_resol_diff_TCC4-1 nil 3451131001 ("" (skosimp) (("" (expand "resolving_diff") (("" (lift-if) (("" (hide 2) (("" (prop) (("" (reveal 1) (("" (assert) (("" (hide 5) (("" (name-replace "k1" "min({kk: below[length(args(t!1))] | NOT subtermOF(s!1, #(1 + kk)) = subtermOF(t!1, #(1 + kk))})") (("1" (name-replace "k" "1+k1") (("1" (replace -1 1) (("1" (hide -1) (("1" (rewrite "first_add[posnat]") (("1" (lemma "resolving_diff_TCC3") (("1" (inst -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" (inst -2 "f(t!1)" "args(t!1)") (("1" (case "t!1 = app(f(t!1), args(t!1))") (("1" (assert) (("1" (inst -3 "k - 1") (("1" (reveal -6) (("1" (reveal -5) (("1" (assert) nil nil)) nil)) nil) ("2" (reveal -6) (("2" (reveal -5) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 3)) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 5)) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "resolving_diff_TCC3") (("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" (inst -2 "f(t!1)" "args(t!1)") (("1" (case "t!1 = app(f(t!1), args(t!1))") (("1" (assert) (("1" (inst -3 "k - 1") (("1" (reveal -6) (("1" (reveal -5) (("1" (assert) nil nil)) nil)) nil) ("2" (reveal -6) (("2" (reveal -5) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 3)) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 5)) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (lemma "resolving_diff_TCC2") (("3" (inst -1 "s!1" "t!1" "f(s!1)" "args(s!1)") (("3" (case "s!1 = app(f(s!1), args(s!1))") (("1" (assert) (("1" (inst -2 "f(t!1)" "args(t!1)") (("1" (case "t!1 = app(f(t!1), args(t!1))") (("1" (assert) (("1" (hide-all-but (-3 1)) (("1" (inst -1 "k - 1") (("1" (reveal -7) (("1" (reveal -8) (("1" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (reveal -7) (("2" (reveal -8) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 3)) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 5)) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil)) nil) ("4" (hide 2) (("4" (lemma "resolving_diff_TCC1") (("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" (inst -2 "f(t!1)" "args(t!1)") (("1" (case "t!1 = app(f(t!1), args(t!1))") (("1" (assert) (("1" (hide-all-but (-3 1)) (("1" (inst -1 "k - 1") (("1" (reveal -7) (("1" (reveal -8) (("1" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (reveal -7) (("2" (reveal -8) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 3)) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 5)) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 2) (("2" (lemma "resolving_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" (inst -2 "f(t!1)" "args(t!1)") (("1" (case "t!1 = app(f(t!1), args(t!1))") (("1" (assert) nil nil) ("2" (hide-all-but (1 3)) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 5)) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide -1 2) (("3" (skosimp*) (("3" (typepred "kk!1") (("3" (lemma "positions_of_arg") (("3" (inst -1 "t!1" "kk!1") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("4" (hide -1 2) (("4" (skosimp*) (("4" (lemma "positions_of_arg") (("4" (inst -1 "s!1" "kk!1") (("1" (assert) nil nil) ("2" (typepred "kk!1") (("2" (lemma "uni_diff_equal_length_arg") (("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" (inst -2 "f(t!1)" "args(t!1)") (("1" (case "t!1 = app(f(t!1), args(t!1))") (("1" (assert) nil nil) ("2" (hide-all-but (1 4)) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 6)) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((resolving_diff def-decl "position" unification nil) (uni_diff_equal_length_arg formula-decl nil unification nil) (kk!1 skolem-const-decl "below[length(args[variable, symbol, arity](t!1))]" unification nil) (positions_of_arg formula-decl nil positions nil) (resolving_diff_TCC7 subtype-tcc nil unification nil) (posint nonempty-type-eq-decl nil integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (resolving_diff_TCC1 subtype-tcc nil unification nil) (resolving_diff_TCC2 subtype-tcc nil unification nil) (resolving_diff_TCC3 subtype-tcc nil unification nil) (app adt-constructor-decl "[[f: symbol, {args: finite_sequence[term] | args`length = arity(f)}] -> (app?)]" term_adt nil) (term_app_extensionality formula-decl nil term_adt nil) (t!1 skolem-const-decl "{t: term | unifiable(s!1, t) & s!1 /= t}" unification nil) (s!1 skolem-const-decl "term[variable, symbol, arity]" unification nil) (k skolem-const-decl "posint" unification nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (first_add formula-decl nil seq_extras "structures/") (finseq type-eq-decl nil finite_sequences nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (|#| const-decl "finite_sequence[T]" set2seq "structures/") (subtermOF def-decl "term" subterm nil) (positions? type-eq-decl nil positions nil) (positionsOF def-decl "positions" positions nil) (positions type-eq-decl nil positions nil) (position type-eq-decl nil positions nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (NOT const-decl "[bool -> bool]" booleans nil) (min const-decl "{a | S(a) AND (FORALL x: S(x) IMPLIES a <= x)}" min_nat nil) (<= const-decl "bool" reals nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (nonempty? const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (/= const-decl "boolean" notequal nil) (unifiable const-decl "bool" unification nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (args adt-accessor-decl "[d: (app?) -> {args: finite_sequence[term] | args`length = arity(f(d))}]" term_adt nil) (f adt-accessor-decl "[(app?) -> symbol]" term_adt nil) (finite_sequence type-eq-decl nil finite_sequences nil) (below type-eq-decl nil nat_types nil) (app? adt-recognizer-decl "[term -> boolean]" term_adt nil) (term type-decl nil term_adt nil) (arity formal-const-decl "[symbol -> nat]" unification nil) (symbol formal-nonempty-type-decl nil unification nil) (variable formal-nonempty-type-decl nil unification nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil)) nil)) (resol_diff_to_rest_resol_diff 0 (resol_diff_to_rest_resol_diff-1 nil 3451229222 ("" (skosimp) (("" (assert) (("" (flatten) (("" (expand "resolving_diff" 1) (("" (lift-if) (("" (prop) (("" (assert) (("" (name-replace "k1" "min({kk: below[length(args(t!1))] | NOT subtermOF(s!1, #(1 + kk)) = subtermOF(t!1, #(1 + kk))})") (("1" (name-replace "k" "1+k1") (("1" (case "resolving_diff(s!1, t!1) = add_first(k, resolving_diff(subtermOF(s!1, #(k)), subtermOF(t!1, #(k))))") (("1" (hide 2) (("1" (replace -1 4) (("1" (rewrite "first_add[posnat]") (("1" (rewrite "rest_add_first[posnat]") nil nil)) nil)) nil)) nil) ("2" (hide-all-but (1 3)) (("2" (reveal -2) (("2" (expand "resolving_diff" 1 1) (("2" (replace -1 1) (("2" (reveal -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 3 6) (("2" (lemma "resolving_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" (inst -2 "f(t!1)" "args(t!1)") (("1" (case "t!1 = app(f(t!1), args(t!1))") (("1" (assert) nil nil) ("2" (hide-all-but (1 3)) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 5)) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 3 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 3 6) (("4" (skosimp*) (("4" (lemma "positions_of_arg") (("4" (inst -1 "s!1" "kk!1") (("1" (typepred "kk!1") (("1" (lemma "uni_diff_equal_length_arg") (("1" (inst -1 "s!1" "t!1" "f(s!1)" "args(s!1)") (("1" (case "s!1 = app(f(s!1), args(s!1))") (("1" (assert) nil nil) ("2" (hide-all-but (1 5)) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "kk!1") (("2" (lemma "uni_diff_equal_length_arg") (("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" (inst -2 "f(t!1)" "args(t!1)") (("1" (case "t!1 = app(f(t!1), args(t!1))") (("1" (assert) nil nil) ("2" (hide-all-but (1 4)) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 6)) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((resolving_diff def-decl "position" unification nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (variable formal-nonempty-type-decl nil unification nil) (symbol formal-nonempty-type-decl nil unification nil) (arity formal-const-decl "[symbol -> nat]" unification nil) (term type-decl nil term_adt nil) (app? adt-recognizer-decl "[term -> boolean]" term_adt nil) (below type-eq-decl nil nat_types nil) (finite_sequence type-eq-decl nil finite_sequences nil) (f adt-accessor-decl "[(app?) -> symbol]" term_adt nil) (args adt-accessor-decl "[d: (app?) -> {args: finite_sequence[term] | args`length = arity(f(d))}]" term_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (unifiable const-decl "bool" unification nil) (/= const-decl "boolean" notequal nil) (set type-eq-decl nil sets nil) (nonempty? const-decl "bool" sets nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (min const-decl "{a | S(a) AND (FORALL x: S(x) IMPLIES a <= x)}" min_nat nil) (NOT const-decl "[bool -> bool]" booleans nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (position type-eq-decl nil positions nil) (positions type-eq-decl nil positions nil) (positionsOF def-decl "positions" positions nil) (positions? type-eq-decl nil positions nil) (subtermOF def-decl "term" subterm nil) (|#| const-decl "finite_sequence[T]" set2seq "structures/") (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (finseq type-eq-decl nil finite_sequences nil) (add_first const-decl "finseq" seq_extras "structures/") (rest_add_first formula-decl nil seq_extras "structures/") (first_add formula-decl nil seq_extras "structures/") (int_minus_int_is_int application-judgement "int" integers nil) (posint nonempty-type-eq-decl nil integers nil) (resolving_diff_TCC7 subtype-tcc nil unification nil) (app adt-constructor-decl "[[f: symbol, {args: finite_sequence[term] | args`length = arity(f)}] -> (app?)]" term_adt nil) (term_app_extensionality formula-decl nil term_adt nil) (positions_of_arg formula-decl nil positions nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (s!1 skolem-const-decl "term[variable, symbol, arity]" unification nil) (t!1 skolem-const-decl "{t: term | unifiable(s!1, t) & s!1 /= t}" unification nil) (kk!1 skolem-const-decl "below[length(args[variable, symbol, arity](t!1))]" unification nil) (uni_diff_equal_length_arg formula-decl nil unification nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil)) shostak)) (position_s_resolving_diff 0 (position_s_resolving_diff-1 nil 3452419921 ("" (measure-induct+ "length(p)" "p") (("" (skosimp) (("" (expand "resolving_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" (name-replace "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" (inst -2 "resolving_diff(subtermOF(s!1, #(k!1)), subtermOF(t!1, #(k!1)))" "subtermOF(s!1, #(k!1))" "subtermOF(t!1, #(k!1))") (("1" (replace -1 -2) (("1" (expand "add_first" -2) (("1" (expand "insert?" -2) (("1" (case "positionsOF(s!1)( #[posnat](k!1))") (("1" (rewrite "add_first_is_o") (("1" (lemma "pos_o_term") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide (-1 -2 5)) (("2" (reveal -5) (("2" (replace -1 1 rl) (("2" (hide -1) (("2" (lemma "positions_of_arg") (("2" (inst -1 "s!1" "k!11") (("1" (assert) nil nil) ("2" (typepred "k!11") (("2" (hide (-2 1 3)) (("2" (lemma "uni_diff_equal_length_arg") (("2" (inst -1 "s!1" "t!1" "f(s!1)" "args(s!1)") (("2" (case "s!1 = app(f(s!1), args(s!1))") (("1" (assert) (("1" (hide -1) (("1" (inst -1 "f(t!1)" "args(t!1)") (("1" (case "t!1 = app(f(t!1), args(t!1))") (("1" (assert) nil nil) ("2" (hide-all-but (1 3)) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 5)) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide - 5) (("2" (lemma "resolving_diff_TCC7") (("2" (inst -1 "s!1" "t!1" "f(s!1)" "args(s!1)") (("2" (case "s!1 = app(f(s!1), args(s!1))") (("1" (assert) (("1" (hide -1) (("1" (inst -1 "f(t!1)" "args(t!1)") (("1" (case "t!1 = app(f(t!1), args(t!1))") (("1" (assert) nil nil) ("2" (hide-all-but (1 3)) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 5)) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide - 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" (lemma "uni_diff_equal_length_arg") (("2" (inst -1 "s!1" "t!1" "f(s!1)" "args(s!1)") (("2" (case "s!1 = app(f(s!1), args(s!1))") (("1" (assert) (("1" (hide -1) (("1" (inst -1 "f(t!1)" "args(t!1)") (("1" (case "t!1 = app(f(t!1), args(t!1))") (("1" (assert) nil nil) ("2" (hide-all-but (1 4)) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 6)) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nnint_plus_posint_is_posint application-judgement "posint" integers nil) (kk!1 skolem-const-decl "below[length(args[variable, symbol, arity](t!1))]" unification nil) (resolving_diff_TCC7 subtype-tcc nil unification nil) (posint nonempty-type-eq-decl nil integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (insert? const-decl "finseq" seq_extras "structures/") (positions_of_arg formula-decl nil positions nil) (uni_diff_equal_length_arg formula-decl nil unification nil) (app adt-constructor-decl "[[f: symbol, {args: finite_sequence[term] | args`length = arity(f)}] -> (app?)]" term_adt nil) (term_app_extensionality formula-decl nil term_adt nil) (k!11 skolem-const-decl "{a | NOT subtermOF(s!1, #(1 + a)) = subtermOF(t!1, #(1 + a)) AND (FORALL (x: below[length(args(t!1))]): NOT subtermOF(s!1, #(1 + x)) = subtermOF(t!1, #(1 + x)) IMPLIES a <= x)}" unification nil) (t!1 skolem-const-decl "{t: term | unifiable(s!1, t) & s!1 /= t}" unification nil) (s!1 skolem-const-decl "term[variable, symbol, arity]" unification nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (finseq type-eq-decl nil finite_sequences nil) (add_first_is_o formula-decl nil seq_extras "structures/") (pos_o_term formula-decl nil subterm nil) (add_first const-decl "finseq" seq_extras "structures/") (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (|#| const-decl "finite_sequence[T]" set2seq "structures/") (subtermOF def-decl "term" subterm nil) (positions? type-eq-decl nil positions nil) (NOT const-decl "[bool -> bool]" booleans nil) (min const-decl "{a | S(a) AND (FORALL x: S(x) IMPLIES a <= x)}" min_nat nil) (<= const-decl "bool" reals nil) (nonempty? const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (args adt-accessor-decl "[d: (app?) -> {args: finite_sequence[term] | args`length = arity(f(d))}]" term_adt nil) (f adt-accessor-decl "[(app?) -> symbol]" term_adt nil) (finite_sequence type-eq-decl nil finite_sequences nil) (app? adt-recognizer-decl "[term -> boolean]" term_adt nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (union const-decl "set" sets nil) (IUnion const-decl "set[T]" indexed_sets nil) (member const-decl "bool" sets nil) (only_empty_seq const-decl "positions" positions nil) (positionsOF def-decl "positions" positions nil) (positions type-eq-decl nil positions nil) (resolving_diff def-decl "position" unification nil) (= const-decl "[T, T -> boolean]" equalities nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (unifiable const-decl "bool" unification nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (term type-decl nil term_adt nil) (wf_nat formula-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (naturalnumber type-eq-decl nil naturalnumbers nil) (position type-eq-decl nil positions nil) (arity formal-const-decl "[symbol -> nat]" unification nil) (symbol formal-nonempty-type-decl nil unification nil) (variable formal-nonempty-type-decl nil unification nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (measure_induction formula-decl nil measure_induction nil) (well_founded? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil)) shostak)) (position_t_resolving_diff 0 (position_t_resolving_diff-1 nil 3452429121 ("" (measure-induct+ "length(p)" "p") (("" (skosimp) (("" (expand "resolving_diff" -2) (("" (lift-if) (("" (prop) (("1" (hide -3) (("1" (replaces -2) (("1" (expand "positionsOF") (("1" (lift-if) (("1" (prop) (("1" (expand "only_empty_seq") (("1" (propax) nil nil)) nil) ("2" (expand "only_empty_seq") (("2" (propax) nil nil)) nil) ("3" (hide-all-but 2) (("3" (expand* "union" "only_empty_seq" "IUnion" "member") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-2 2)) (("2" (replaces -2) (("2" (replaces -1) (("2" (expand "positionsOF") (("2" (lift-if) (("2" (prop) (("1" (expand "only_empty_seq") (("1" (propax) nil nil)) nil) ("2" (expand "only_empty_seq") (("2" (propax) nil nil)) nil) ("3" (expand* "union" "only_empty_seq" "IUnion" "member") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but (-1 -2 3)) (("3" (replaces -2) (("3" (expand "positionsOF") (("3" (assert) (("3" (expand "only_empty_seq") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("4" (assert) (("4" (name-replace "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" (inst -2 "resolving_diff(subtermOF(s!1, #(k!1)), subtermOF(t!1, #(k!1)))" "subtermOF(s!1, #(k!1))" "subtermOF(t!1, #(k!1))") (("1" (replace -1 -2) (("1" (expand "add_first" -2) (("1" (expand "insert?" -2) (("1" (case "positionsOF(t!1)( #[posnat](k!1))") (("1" (rewrite "add_first_is_o") (("1" (lemma "pos_o_term") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide - 5) (("2" (reveal -5) (("2" (replace -1 1 rl) (("2" (hide -1) (("2" (lemma "positions_of_arg") (("2" (inst -1 "t!1" "k!11") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide - 5) (("2" (lemma "resolving_diff_TCC7") (("2" (inst -1 "s!1" "t!1" "f(s!1)" "args(s!1)") (("2" (case "s!1 = app(f(s!1), args(s!1))") (("1" (assert) (("1" (hide -1) (("1" (inst -1 "f(t!1)" "args(t!1)") (("1" (case "t!1 = app(f(t!1), args(t!1))") (("1" (assert) nil nil) ("2" (hide-all-but (1 3)) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 5)) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide - 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" (lemma "uni_diff_equal_length_arg") (("2" (inst -1 "s!1" "t!1" "f(s!1)" "args(s!1)") (("2" (case "s!1 = app(f(s!1), args(s!1))") (("1" (assert) (("1" (hide -1) (("1" (inst -1 "f(t!1)" "args(t!1)") (("1" (case "t!1 = app(f(t!1), args(t!1))") (("1" (assert) nil nil) ("2" (hide-all-but (1 4)) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 6)) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nnint_plus_posint_is_posint application-judgement "posint" integers nil) (uni_diff_equal_length_arg formula-decl nil unification nil) (kk!1 skolem-const-decl "below[length(args[variable, symbol, arity](t!1))]" unification nil) (t!1 skolem-const-decl "{t: term | unifiable(s!1, t) & s!1 /= t}" unification nil) (s!1 skolem-const-decl "term[variable, symbol, arity]" unification nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (term_app_extensionality formula-decl nil term_adt nil) (app adt-constructor-decl "[[f: symbol, {args: finite_sequence[term] | args`length = arity(f)}] -> (app?)]" term_adt nil) (resolving_diff_TCC7 subtype-tcc nil unification nil) (posint nonempty-type-eq-decl nil integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (insert? const-decl "finseq" seq_extras "structures/") (positions_of_arg formula-decl nil positions nil) (finseq type-eq-decl nil finite_sequences nil) (add_first_is_o formula-decl nil seq_extras "structures/") (pos_o_term formula-decl nil subterm nil) (add_first const-decl "finseq" seq_extras "structures/") (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (|#| const-decl "finite_sequence[T]" set2seq "structures/") (subtermOF def-decl "term" subterm nil) (positions? type-eq-decl nil positions nil) (NOT const-decl "[bool -> bool]" booleans nil) (min const-decl "{a | S(a) AND (FORALL x: S(x) IMPLIES a <= x)}" min_nat nil) (<= const-decl "bool" reals nil) (nonempty? const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (args adt-accessor-decl "[d: (app?) -> {args: finite_sequence[term] | args`length = arity(f(d))}]" term_adt nil) (f adt-accessor-decl "[(app?) -> symbol]" term_adt nil) (finite_sequence type-eq-decl nil finite_sequences nil) (app? adt-recognizer-decl "[term -> boolean]" term_adt nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (only_empty_seq const-decl "positions" positions nil) (union const-decl "set" sets nil) (IUnion const-decl "set[T]" indexed_sets nil) (member const-decl "bool" sets nil) (positionsOF def-decl "positions" positions nil) (positions type-eq-decl nil positions nil) (resolving_diff def-decl "position" unification nil) (= const-decl "[T, T -> boolean]" equalities nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (unifiable const-decl "bool" unification nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (term type-decl nil term_adt nil) (wf_nat formula-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (naturalnumber type-eq-decl nil naturalnumbers nil) (position type-eq-decl nil positions nil) (arity formal-const-decl "[symbol -> nat]" unification nil) (symbol formal-nonempty-type-decl nil unification nil) (variable formal-nonempty-type-decl nil unification nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (measure_induction formula-decl nil measure_induction nil) (well_founded? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil)) shostak)) (resolving_diff_has_diff_argument 0 (resolving_diff_has_diff_argument-1 nil 3452342602 ("" (induct "s") (("1" (skosimp*) (("1" (typepred "t!1") (("1" (hide -1) (("1" (expand "resolving_diff") (("1" (replaces -2) (("1" (expand "subtermOF") (("1" (rewrite "empty_0") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "resolving_diff" -2) (("2" (lift-if) (("2" (prop) (("1" (hide -1 -3) (("1" (replaces -1) (("1" (typepred "t!1") (("1" (hide -1) (("1" (expand "subtermOF") (("1" (rewrite "empty_0") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 -3 1) (("2" (replaces -1) (("2" (typepred "t!1") (("2" (hide -1) (("2" (expand "subtermOF") (("2" (rewrite "empty_0") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (assert) (("3" (name-replace "k!11" "min({kk: below[length(args(t!1))] | NOT subtermOF(app(app1_var!1, app2_var!1), #(1 + kk)) = subtermOF(t!1, #(1 + kk))})") (("1" (name-replace "k!1" "1 + k!11") (("1" (inst -2 "k!1 - 1") (("1" (inst -2 "subtermOF(t!1, #(k!1))" "resolving_diff(subtermOF(app(app1_var!1, app2_var!1), #(k!1)), subtermOF(t!1, #(k!1)))") (("1" (case "subtermOF(app(app1_var!1, app2_var!1), #(k!1)) = app2_var!1`seq(k!1 - 1)") (("1" (replace -1 -3 rl) (("1" (hide -1) (("1" (lemma "subt_of_subt_is_subt_of_term") (("1" (inst -1 "app(app1_var!1, app2_var!1)" "k!1" "resolving_diff(subtermOF(app(app1_var!1, app2_var!1), #(k!1)), subtermOF(t!1, #(k!1)))" "p!1") (("1" (assert) (("1" (lemma "subt_of_subt_is_subt_of_term") (("1" (inst -1 "t!1" "k!1" "resolving_diff(subtermOF(app(app1_var!1, app2_var!1), #(k!1)), subtermOF(t!1, #(k!1)))" "p!1") (("1" (assert) nil nil) ("2" (hide -) (("2" (lemma "resolving_diff_TCC2") (("2" (inst -1 "app(app1_var!1, app2_var!1)" "t!1" "app1_var!1" "app2_var!1") (("2" (assert) (("2" (inst -1 "f(t!1)" "args(t!1)") (("2" (case "t!1 = app(f(t!1), args(t!1))") (("1" (assert) (("1" (hide -1) (("1" (inst -1 "k!11") (("1" (reveal -14) (("1" (reveal -13) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 3)) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -) (("2" (lemma "resolving_diff_TCC1") (("2" (inst -1 "app(app1_var!1, app2_var!1)" "t!1" "app1_var!1" "app2_var!1") (("2" (assert) (("2" (inst -1 "f(t!1)" "args(t!1)") (("2" (case "t!1 = app(f(t!1), args(t!1))") (("1" (assert) (("1" (hide -1) (("1" (inst -1 "k!11") (("1" (reveal -13) (("1" (reveal -12) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 3)) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "#") (("2" (expand "subtermOF") (("2" (expand "finseq_appl") (("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but (1 3)) (("3" (reveal -6) (("3" (reveal -7) (("3" (assert) (("3" (hide -) (("3" (lemma "uni_diff_equal_length_arg") (("3" (inst -1 "app(app1_var!1, app2_var!1)" "t!1" "app1_var!1" " app2_var!1") (("3" (assert) (("3" (inst -1 "f(t!1)" "args(t!1)") (("3" (case "t!1 = app(f(t!1), args(t!1))") (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (reveal 3) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (split) (("1" (hide -) (("1" (lemma "position_s_resolving_diff") (("1" (inst -1 "app2_var!1`seq(k!1 - 1)" "subtermOF(t!1, #(k!1))" "resolving_diff(subtermOF(app(app1_var!1, app2_var!1), #(k!1)), subtermOF(t!1, #[posnat](k!1)))") (("1" (case "subtermOF(app(app1_var!1, app2_var!1), #(k!1)) = app2_var!1`seq(k!1 - 1)") (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil) ("3" (hide-all-but 1) (("3" (reveal -7) (("3" (assert) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "resolving_diff_TCC3") (("2" (inst -1 "app(app1_var!1, app2_var!1)" "t!1" "app1_var!1" "app2_var!1") (("2" (assert) (("2" (inst -1 "f(t!1)" "args(t!1)") (("2" (case "t!1 = app(f(t!1), args(t!1))") (("1" (assert) (("1" (hide -1) (("1" (inst -1 "k!11") (("1" (reveal -10) (("1" (reveal -11) (("1" (assert) (("1" (case "subtermOF(app(app1_var!1, app2_var!1), #(k!1)) = app2_var!1`seq(k!1 - 1)") (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil) ("3" (hide (-3 2)) (("3" (lemma "uni_diff_equal_length_arg") (("3" (inst -1 "app(app1_var!1, app2_var!1)" "t!1" "app1_var!1" "app2_var!1") (("3" (assert) (("3" (inst -1 "f(t!1)" "args(t!1)") (("3" (case "t!1 = app(f(t!1), args(t!1))") (("1" (assert) nil nil) ("2" (hide-all-but (1 3)) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (hide (-3 2)) (("4" (replace -2 1 rl) (("4" (hide -2) (("4" (lemma "resolving_diff_TCC1") (("4" (inst -1 "app(app1_var!1, app2_var!1)" "t!1" "app1_var!1" "app2_var!1") (("4" (assert) (("4" (inst -1 "f(t!1)" "args(t!1)") (("4" (case "t!1 = app(f(t!1), args(t!1))") (("1" (assert) (("1" (hide -1) (("1" (inst -1 "k!11") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide-all-but (1 3)) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 3)) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (reveal -6) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -) (("2" (lemma "position_t_resolving_diff") (("2" (inst -1 "subtermOF(app(app1_var!1, app2_var!1), #(k!1))" "subtermOF(t!1, #(k!1))" "resolving_diff(subtermOF(app(app1_var!1, app2_var!1), #(k!1)), subtermOF(t!1, #(k!1)))") nil nil)) nil)) nil)) nil) ("3" (hide -) (("3" (lemma "resolving_diff_TCC3") (("3" (inst -1 "app(app1_var!1, app2_var!1)" "t!1" "app1_var!1" "app2_var!1") (("3" (assert) (("3" (inst -1 "f(t!1)" "args(t!1)") (("3" (case "t!1 = app(f(t!1), args(t!1))") (("1" (assert) (("1" (hide -1) (("1" (reveal -8) (("1" (reveal -9) (("1" (inst -3 "k!11") (("1" (assert) (("1" (case "subtermOF(app(app1_var!1, app2_var!1), #(k!1)) = app2_var!1`seq(k!1 - 1)") (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil) ("3" (hide -3 2) (("3" (lemma "uni_diff_equal_length_arg") (("3" (inst -1 "app(app1_var!1, app2_var!1)" "t!1" "app1_var!1" "app2_var!1") (("3" (assert) (("3" (inst -1 "f(t!1)" "args(t!1)") (("3" (case "t!1 = app(f(t!1), args(t!1))") (("1" (assert) nil nil) ("2" (hide-all-but (1 3)) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (replace -2 1 rl) (("4" (hide (-3 2)) (("4" (lemma "resolving_diff_TCC1") (("4" (inst -1 "app(app1_var!1, app2_var!1)" "t!1" "app1_var!1" "app2_var!1") (("4" (assert) (("4" (inst -1 "f(t!1)" "args(t!1)") (("4" (case "t!1 = app(f(t!1), args(t!1))") (("1" (assert) (("1" (hide -1) (("1" (inst -1 "k!11") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide-all-but (1 3)) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 3)) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (reveal -4) (("2" (replace -1 1 rl) (("2" (assert) (("2" (hide -1) (("2" (lemma "uni_diff_equal_length_arg") (("2" (inst -1 "app(app1_var!1, app2_var!1)" "t!1" "app1_var!1" "app2_var!1") (("2" (assert) (("2" (inst -1 "f(t!1)" "args(t!1)") (("2" (case "t!1 = app(f(t!1), args(t!1))") (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (reveal 2) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -) (("2" (lemma "resolving_diff_TCC7") (("2" (inst -1 "app(app1_var!1, app2_var!1)" "t!1" "app1_var!1" "app2_var!1") (("2" (assert) (("2" (inst -1 "f(t!1)" "args(t!1)") (("2" (case "t!1 = app(f(t!1), args(t!1))") (("1" (assert) nil nil) ("2" (hide-all-but (1 3)) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide -) (("3" (skosimp*) (("3" (lemma "positions_of_arg") (("3" (inst -1 "t!1" "kk!1") (("3" (typepred "kk!1") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("4" (hide -) (("4" (skosimp*) (("4" (lemma "positions_of_arg") (("4" (inst -1 "app(app1_var!1, app2_var!1)" "kk!1") (("1" (assert) nil nil) ("2" (hide 2) (("2" (typepred "kk!1") (("2" (lemma "uni_diff_equal_length_arg") (("2" (inst -1 "app(app1_var!1, app2_var!1)" "t!1" "app1_var!1" "app2_var!1") (("2" (assert) (("2" (inst -1 "f(t!1)" "args(t!1)") (("2" (case "t!1 = app(f(t!1), args(t!1))") (("1" (assert) nil nil) ("2" (hide-all-but (1 3)) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nnint_plus_posint_is_posint application-judgement "posint" integers nil) (kk!1 skolem-const-decl "below[length(args[variable, symbol, arity](t!1))]" unification nil) (positions_of_arg formula-decl nil positions nil) (resolving_diff_TCC7 subtype-tcc nil unification nil) (posint nonempty-type-eq-decl nil integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (t!1 skolem-const-decl "{t: term | unifiable(app(app1_var!1, app2_var!1), t) & app(app1_var!1, app2_var!1) /= t}" unification nil) (uni_diff_equal_length_arg formula-decl nil unification nil) (first const-decl "T" seq_extras "structures/") (^ const-decl "finseq" finite_sequences nil) (rest const-decl "finseq" seq_extras "structures/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nat_min application-judgement "{k: nat | k <= i AND k <= j}" real_defs nil) (int_min application-judgement "{k: int | k <= i AND k <= j}" real_defs nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (subt_of_subt_is_subt_of_term formula-decl nil subterm nil) (resolving_diff_TCC1 subtype-tcc nil unification nil) (resolving_diff_TCC2 subtype-tcc nil unification nil) (term_app_extensionality formula-decl nil term_adt nil) (position_t_resolving_diff formula-decl nil unification nil) (resolving_diff_TCC3 subtype-tcc nil unification nil) (position_s_resolving_diff formula-decl nil unification nil) (app2_var!1 skolem-const-decl "{args: finite_sequence[term[variable, symbol, arity]] | args`length = arity(app1_var!1)}" unification nil) (app1_var!1 skolem-const-decl "symbol" unification nil) (k!1 skolem-const-decl "posint" unification nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (|#| const-decl "finite_sequence[T]" set2seq "structures/") (min const-decl "{a | S(a) AND (FORALL x: S(x) IMPLIES a <= x)}" min_nat nil) (<= const-decl "bool" reals nil) (nonempty? const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (args adt-accessor-decl "[d: (app?) -> {args: finite_sequence[term] | args`length = arity(f(d))}]" term_adt nil) (f adt-accessor-decl "[(app?) -> symbol]" term_adt nil) (< const-decl "bool" reals nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (finite_sequence type-eq-decl nil finite_sequences nil) (app? adt-recognizer-decl "[term -> boolean]" term_adt nil) (app adt-constructor-decl "[[f: symbol, {args: finite_sequence[term] | args`length = arity(f)}] -> (app?)]" term_adt nil) (empty_seq const-decl "finseq" finite_sequences nil) (finseq type-eq-decl nil finite_sequences nil) (empty_0 formula-decl nil seq_extras "structures/") (vars adt-constructor-decl "[variable -> (vars?)]" term_adt nil) (vars? adt-recognizer-decl "[term -> boolean]" term_adt nil) (NOT const-decl "[bool -> bool]" booleans nil) (term_induction formula-decl nil term_adt nil) (variable formal-nonempty-type-decl nil unification nil) (symbol formal-nonempty-type-decl nil unification nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (arity formal-const-decl "[symbol -> nat]" unification nil) (subtermOF def-decl "term" subterm nil) (positions? type-eq-decl nil positions nil) (resolving_diff def-decl "position" unification nil) (= const-decl "[T, T -> boolean]" equalities nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (positionsOF def-decl "positions" positions nil) (positions type-eq-decl nil positions nil) (position type-eq-decl nil positions nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (below type-eq-decl nil nat_types nil) (/= const-decl "boolean" notequal nil) (unifiable const-decl "bool" unification nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (term type-decl nil term_adt nil)) shostak)) (resolving_diff_has_unifiable_argument 0 (resolving_diff_has_unifiable_argument-1 nil 3452440107 ("" (induct "s") (("1" (skosimp*) (("1" (expand "resolving_diff") (("1" (replaces -1) (("1" (expand "subtermOF") (("1" (rewrite "empty_0") (("1" (typepred "t!1") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "resolving_diff" -2) (("2" (lift-if) (("2" (prop) (("1" (hide -3) (("1" (replaces -2) (("1" (expand "subtermOF") (("1" (rewrite "empty_0") (("1" (typepred "t!1") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 -3 1) (("2" (replaces -1) (("2" (expand "subtermOF") (("2" (rewrite "empty_0") (("2" (typepred "t!1") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (assert) (("3" (name-replace "k!11" "min({kk: below[length(args(t!1))] | NOT subtermOF(app(app1_var!1, app2_var!1), #(1 + kk)) = subtermOF(t!1, #(1 + kk))})") (("1" (name-replace "k!1" "1 + k!11") (("1" (inst -2 "k!1 - 1" "subtermOF(t!1, #(k!1))" "resolving_diff(app2_var!1`seq(k!1 - 1), subtermOF(t!1, #(k!1)))") (("1" (case "subtermOF(app(app1_var!1, app2_var!1), #(k!1)) = app2_var!1`seq(k!1 - 1)") (("1" (replace -1 -3 rl) (("1" (hide -1) (("1" (lemma "subt_of_subt_is_subt_of_term") (("1" (inst -1 "app(app1_var!1, app2_var!1)" "k!1" "resolving_diff(subtermOF(app(app1_var!1, app2_var!1), #(k!1)), subtermOF(t!1, #(k!1)))" "p!1") (("1" (assert) (("1" (lemma "subt_of_subt_is_subt_of_term") (("1" (inst -1 "t!1" "k!1" "resolving_diff(subtermOF(app(app1_var!1, app2_var!1), #(k!1)), subtermOF(t!1, #(k!1)))" "p!1") (("1" (assert) nil nil) ("2" (hide - 4) (("2" (lemma "resolving_diff_TCC2") (("2" (inst -1 "app(app1_var!1, app2_var!1)" "t!1" "app1_var!1" "app2_var!1") (("2" (assert) (("2" (inst -1 "f(t!1)" "args(t!1)") (("2" (case "t!1 = app(f(t!1), args(t!1))") (("1" (assert) (("1" (hide -1) (("1" (inst -1 "k!11") (("1" (reveal -12) (("1" (reveal -13) (("1" (replace -2 1 rl) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 3)) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide - 4) (("2" (lemma "resolving_diff_TCC1") (("2" (inst -1 "app(app1_var!1, app2_var!1)" "t!1" "app1_var!1" "app2_var!1") (("2" (assert) (("2" (inst -1 "f(t!1)" "args(t!1)") (("2" (case "t!1 = app(f(t!1), args(t!1))") (("1" (assert) (("1" (hide -1) (("1" (inst -1 "k!11") (("1" (reveal -12) (("1" (reveal -11) (("1" (replace -1 1 rl) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 3)) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil) ("3" (hide-all-but 1) (("3" (reveal -5) (("3" (assert) nil nil)) nil)) nil)) nil) ("2" (split) (("1" (hide - 4) (("1" (lemma "position_s_resolving_diff") (("1" (inst -1 "app2_var!1`seq(k!1 - 1)" "subtermOF(t!1, #(k!1))" "resolving_diff(app2_var!1`seq(k!1 - 1), subtermOF(t!1, #(k!1)))") (("1" (hide-all-but 1) (("1" (reveal -5) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide - 4) (("2" (lemma "position_t_resolving_diff") (("2" (inst -1 "app2_var!1`seq(k!1 - 1)" "subtermOF(t!1, #(k!1))" "resolving_diff(app2_var!1`seq(k!1 - 1), subtermOF(t!1, #(k!1)))") (("2" (hide-all-but 1) (("2" (reveal -5) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide - 4) (("3" (reveal -4) (("3" (reveal -5) (("3" (assert) (("3" (lemma "uni_diff_equal_length_arg") (("3" (inst -1 "app(app1_var!1, app2_var!1)" "t!1" "app1_var!1" "app2_var!1") (("3" (assert) (("3" (inst -1 "f(t!1)" "args(t!1)") (("3" (case "t!1 = app(f(t!1), args(t!1))") (("1" (assert) nil nil) ("2" (hide-all-but (1 3)) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (hide - 4) (("4" (lemma "resolving_diff_TCC3") (("4" (inst -1 "app(app1_var!1, app2_var!1)" "t!1" "app1_var!1" "app2_var!1") (("4" (assert) (("4" (inst -1 "f(t!1)" "args(t!1)") (("4" (case "t!1 = app(f(t!1), args(t!1))") (("1" (assert) (("1" (hide -1) (("1" (inst -1 "k!11") (("1" (reveal -8) (("1" (reveal -9) (("1" (assert) (("1" (case "subtermOF(app(app1_var!1, app2_var!1), #(k!1)) = app2_var!1`seq(k!1 - 1)") (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil) ("3" (hide -3 2) (("3" (lemma "uni_diff_equal_length_arg") (("3" (inst -1 "app(app1_var!1, app2_var!1)" "t!1" "app1_var!1" "app2_var!1") (("3" (assert) (("3" (inst -1 "f(t!1)" "args(t!1)") (("3" (case "t!1 = app(f(t!1), args(t!1))") (("1" (assert) nil nil) ("2" (hide-all-but (1 3)) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (hide (-3 2)) (("4" (lemma "resolving_diff_TCC1") (("4" (inst -1 "app(app1_var!1, app2_var!1)" "t!1" "app1_var!1" "app2_var!1") (("4" (assert) (("4" (inst -1 "f(t!1)" "args(t!1)") (("4" (case "t!1 = app(f(t!1), args(t!1))") (("1" (assert) (("1" (hide -1) (("1" (inst -1 "k!11") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide-all-but (1 3)) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 3)) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("5" (hide - 4) (("5" (reveal -4) (("5" (reveal -3) (("5" (assert) (("5" (hide -) (("5" (lemma "uni_diff_equal_length_arg") (("5" (inst -1 "app(app1_var!1, app2_var!1)" "t!1" "app1_var!1" "app2_var!1") (("5" (assert) (("5" (inst -1 "f(t!1)" "args(t!1)") (("5" (case "t!1 = app(f(t!1), args(t!1))") (("1" (assert) nil nil) ("2" (hide-all-but (1 3)) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide - 4) (("2" (lemma "resolving_diff_TCC7") (("2" (inst -1 "app(app1_var!1, app2_var!1)" "t!1" "app1_var!1" "app2_var!1") (("2" (assert) (("2" (inst -1 "f(t!1)" "args(t!1)") (("2" (case "t!1 = app(f(t!1), args(t!1))") (("1" (assert) nil nil) ("2" (hide-all-but (1 3)) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide - 4) (("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) (("4" (skosimp*) (("4" (lemma "positions_of_arg") (("4" (inst -1 "app(app1_var!1, app2_var!1)" "kk!1") (("1" (assert) nil nil) ("2" (hide 2) (("2" (typepred "kk!1") (("2" (lemma "uni_diff_equal_length_arg") (("2" (inst -1 "app(app1_var!1, app2_var!1)" "t!1" "app1_var!1" "app2_var!1") (("2" (assert) (("2" (inst -1 "f(t!1)" "args(t!1)") (("2" (case "t!1 = app(f(t!1), args(t!1))") (("1" (assert) nil nil) ("2" (hide-all-but (1 3)) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nnint_plus_posint_is_posint application-judgement "posint" integers nil) (kk!1 skolem-const-decl "below[length(args[variable, symbol, arity](t!1))]" unification nil) (positions_of_arg formula-decl nil positions nil) (resolving_diff_TCC7 subtype-tcc nil unification nil) (posint nonempty-type-eq-decl nil integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (resolving_diff_TCC3 subtype-tcc nil unification nil) (uni_diff_equal_length_arg formula-decl nil unification nil) (position_s_resolving_diff formula-decl nil unification nil) (position_t_resolving_diff formula-decl nil unification nil) (term_app_extensionality formula-decl nil term_adt nil) (resolving_diff_TCC2 subtype-tcc nil unification nil) (resolving_diff_TCC1 subtype-tcc nil unification nil) (subt_of_subt_is_subt_of_term formula-decl nil subterm nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (first const-decl "T" seq_extras "structures/") (^ const-decl "finseq" finite_sequences nil) (rest const-decl "finseq" seq_extras "structures/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nat_min application-judgement "{k: nat | k <= i AND k <= j}" real_defs nil) (int_min application-judgement "{k: int | k <= i AND k <= j}" real_defs nil) (t!1 skolem-const-decl "{t: term | unifiable(app(app1_var!1, app2_var!1), t) & app(app1_var!1, app2_var!1) /= t}" unification nil) (app2_var!1 skolem-const-decl "{args: finite_sequence[term[variable, symbol, arity]] | args`length = arity(app1_var!1)}" unification nil) (app1_var!1 skolem-const-decl "symbol" unification nil) (k!1 skolem-const-decl "posint" unification nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (|#| const-decl "finite_sequence[T]" set2seq "structures/") (min const-decl "{a | S(a) AND (FORALL x: S(x) IMPLIES a <= x)}" min_nat nil) (<= const-decl "bool" reals nil) (nonempty? const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (args adt-accessor-decl "[d: (app?) -> {args: finite_sequence[term] | args`length = arity(f(d))}]" term_adt nil) (f adt-accessor-decl "[(app?) -> symbol]" term_adt nil) (< const-decl "bool" reals nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (finite_sequence type-eq-decl nil finite_sequences nil) (app? adt-recognizer-decl "[term -> boolean]" term_adt nil) (app adt-constructor-decl "[[f: symbol, {args: finite_sequence[term] | args`length = arity(f)}] -> (app?)]" term_adt nil) (empty_seq const-decl "finseq" finite_sequences nil) (finseq type-eq-decl nil finite_sequences nil) (empty_0 formula-decl nil seq_extras "structures/") (vars adt-constructor-decl "[variable -> (vars?)]" term_adt nil) (vars? adt-recognizer-decl "[term -> boolean]" term_adt nil) (NOT const-decl "[bool -> bool]" booleans nil) (term_induction formula-decl nil term_adt nil) (variable formal-nonempty-type-decl nil unification nil) (symbol formal-nonempty-type-decl nil unification nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (arity formal-const-decl "[symbol -> nat]" unification nil) (subtermOF def-decl "term" subterm nil) (positions? type-eq-decl nil positions nil) (resolving_diff def-decl "position" unification nil) (= const-decl "[T, T -> boolean]" equalities nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (positionsOF def-decl "positions" positions nil) (positions type-eq-decl nil positions nil) (position type-eq-decl nil positions nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (below type-eq-decl nil nat_types nil) (/= const-decl "boolean" notequal nil) (unifiable const-decl "bool" unification nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (term type-decl nil term_adt nil)) shostak)) (resolving_diff_vars 0 (resolving_diff_vars-1 nil 3452876334 ("" (induct "s") (("1" (skosimp*) (("1" (expand "resolving_diff") (("1" (replaces -1) (("1" (hide 2) (("1" (expand "subtermOF") (("1" (rewrite "empty_0") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "resolving_diff" -2) (("2" (lift-if) (("2" (prop) (("1" (hide -3) (("1" (lemma "resolving_diff_has_unifiable_argument") (("1" (inst -1 "app(app1_var!1, app2_var!1)" "t!1" "p!1") (("1" (expand "resolving_diff") (("1" (assert) (("1" (expand "unifiable") (("1" (skeep -1) (("1" (expand "unifier") (("1" (expand "ext") (("1" (replace -3 -1) (("1" (expand "subtermOF" -1 1) (("1" (rewrite "empty_0") (("1" (assert) (("1" (expand "subtermOF" -1 1) (("1" (rewrite "empty_0") (("1" (lift-if) (("1" (prop) (("1" (expand "subtermOF" -2) (("1" (rewrite "empty_0") (("1" (hide-all-but -2) (("1" (typepred "t!1") (("1" (hide -1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (decompose-equality -1) (("2" (decompose-equality -2) (("2" (hide -2 -3 -5 2 3) (("2" (replaces -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)) nil) ("2" (hide -3 1 2) (("2" (replaces -2) (("2" (expand "subtermOF") (("2" (rewrite "empty_0") nil nil)) nil)) nil)) nil) ("3" (assert) (("3" (name-replace "k!11" "min({kk: below[length(args(t!1))] | NOT subtermOF(app(app1_var!1, app2_var!1), #(1 + kk)) = subtermOF(t!1, #(1 + kk))})") (("1" (name-replace "k!1" "1 + k!11") (("1" (inst -2 "k!1 - 1") (("1" (inst -2 "subtermOF(t!1, #(k!1))" "resolving_diff(app2_var!1`seq(k!1 - 1), subtermOF(t!1, #(k!1)) )") (("1" (prop) (("1" (case "subtermOF(app(app1_var!1, app2_var!1), #(k!1)) = app2_var!1`seq(k!1 - 1)") (("1" (replace -1 -2 rl) (("1" (lemma "subt_of_subt_is_subt_of_term") (("1" (inst -1 "app(app1_var!1, app2_var!1)" "k!1" "resolving_diff( subtermOF(app(app1_var!1, app2_var!1), #(k!1)), subtermOF(t!1, #(k!1)))" "p!1") (("1" (assert) nil nil) ("2" (hide - 4 5) (("2" (lemma "resolving_diff_TCC1") (("2" (inst -1 "app(app1_var!1, app2_var!1)" "t!1" "app1_var!1" " app2_var!1") (("2" (assert) (("2" (inst -1 "f(t!1)" "args(t!1)") (("2" (case "t!1 = app(f(t!1), args(t!1))") (("1" (assert) (("1" (hide -1) (("1" (inst -1 "k!11") (("1" (reveal -11) (("1" (reveal -12) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 3)) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil) ("3" (reveal -3) (("3" (hide-all-but (-1 1)) (("3" (assert) nil nil)) nil)) nil)) nil) ("2" (case "subtermOF(app(app1_var!1, app2_var!1), #(k!1)) = app2_var!1`seq(k!1 - 1)") (("1" (replace -1 -2 rl) (("1" (hide -1) (("1" (lemma "subt_of_subt_is_subt_of_term") (("1" (inst -1 "t!1" "k!1" "resolving_diff( subtermOF(app(app1_var!1, app2_var!1), #(k!1)), subtermOF(t!1, #(k!1)))" "p!1") (("1" (assert) nil nil) ("2" (hide - 4 5) (("2" (lemma "resolving_diff_TCC2") (("2" (inst -1 "app(app1_var!1, app2_var!1)" "t!1" "app1_var!1" " app2_var!1") (("2" (assert) (("2" (inst -1 "f(t!1)" "args(t!1)") (("2" (case "t!1 = app(f(t!1), args(t!1))") (("1" (assert) (("1" (hide -1) (("1" (inst -1 "k!11") (("1" (reveal -11) (("1" (reveal -12) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 3)) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil) ("3" (reveal -3) (("3" (hide-all-but (-1 1)) (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (split) (("1" (case "subtermOF(app(app1_var!1, app2_var!1), #(k!1)) = app2_var!1`seq(k!1 - 1)") (("1" (replace -1 1 rl) (("1" (hide -1) (("1" (lemma "position_s_resolving_diff") (("1" (inst -1 "subtermOF(app(app1_var!1, app2_var!1), #(k!1))" "subtermOF(t!1, #(k!1))" "resolving_diff( subtermOF(app(app1_var!1, app2_var!1), #(k!1)), subtermOF(t!1, #(k!1)))") nil nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil) ("3" (reveal -3) (("3" (hide-all-but (-1 1)) (("3" (assert) nil nil)) nil)) nil)) nil) ("2" (case "subtermOF(app(app1_var!1, app2_var!1), #(k!1)) = app2_var!1`seq(k!1 - 1)") (("1" (replace -1 1 rl) (("1" (hide -1) (("1" (lemma "position_t_resolving_diff") (("1" (inst -1 "subtermOF(app(app1_var!1, app2_var!1), #(k!1))" "subtermOF(t!1, #(k!1))" "resolving_diff( subtermOF(app(app1_var!1, app2_var!1), #(k!1)), subtermOF(t!1, #(k!1)))") nil nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil) ("3" (reveal -3) (("3" (hide-all-but (-1 1)) (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (reveal -3) (("3" (assert) (("3" (hide - 4 5) (("3" (lemma "uni_diff_equal_length_arg") (("3" (inst -1 "app(app1_var!1, app2_var!1)" "t!1" "app1_var!1" " app2_var!1") (("3" (assert) (("3" (inst -1 "f(t!1)" "args(t!1)") (("3" (case "t!1 = app(f(t!1), args(t!1))") (("1" (assert) nil nil) ("2" (hide-all-but (1 3)) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (case "subtermOF(app(app1_var!1, app2_var!1), #(k!1)) = app2_var!1`seq(k!1 - 1)") (("1" (replace -1 1 rl) (("1" (lemma "resolving_diff_TCC3") (("1" (inst -1 "app(app1_var!1, app2_var!1)" "t!1" "app1_var!1" "app2_var!1") (("1" (assert) (("1" (inst -1 "f(t!1)" "args(t!1)") (("1" (case "t!1 = app(f(t!1), args(t!1))") (("1" (assert) (("1" (hide -1) (("1" (inst -1 "k!11") (("1" (reveal -8) (("1" (reveal -7) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 3)) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil) ("3" (hide - 2) (("3" (reveal -4) (("3" (reveal -5) (("3" (assert) (("3" (hide -) (("3" (lemma "uni_diff_equal_length_arg") (("3" (inst -1 "app(app1_var!1, app2_var!1)" "t!1" "app1_var!1" "app2_var!1") (("3" (assert) (("3" (inst -1 "f(t!1)" "args(t!1)") (("3" (case "t!1 = app(f(t!1), args(t!1))") (("1" (assert) nil nil) ("2" (hide-all-but (1 3)) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide - 4) (("2" (reveal -3) (("2" (assert) (("2" (hide -) (("2" (lemma "uni_diff_equal_length_arg") (("2" (inst -1 "app(app1_var!1, app2_var!1)" "t!1" "app1_var!1" "app2_var!1") (("2" (assert) (("2" (inst -1 "f(t!1)" "args(t!1)") (("2" (case "t!1 = app(f(t!1), args(t!1))") (("1" (assert) nil nil) ("2" (hide-all-but (1 3)) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide - 4) (("2" (lemma "resolving_diff_TCC7") (("2" (inst -1 "app(app1_var!1, app2_var!1)" "t!1" "app1_var!1" "app2_var!1") (("2" (assert) (("2" (inst -1 "f(t!1)" "args(t!1)") (("2" (case "t!1 = app(f(t!1), args(t!1))") (("1" (assert) nil nil) ("2" (hide-all-but (1 3)) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide - 4) (("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) (("4" (skosimp*) (("4" (lemma "positions_of_arg") (("4" (inst -1 "app(app1_var!1, app2_var!1)" "kk!1") (("1" (assert) nil nil) ("2" (hide 2) (("2" (typepred "kk!1") (("2" (lemma "uni_diff_equal_length_arg") (("2" (inst -1 "app(app1_var!1, app2_var!1)" "t!1" "app1_var!1" "app2_var!1") (("2" (assert) (("2" (inst -1 "f(t!1)" "args(t!1)") (("2" (case "t!1 = app(f(t!1), args(t!1))") (("1" (assert) nil nil) ("2" (hide-all-but (1 3)) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nnint_plus_posint_is_posint application-judgement "posint" integers nil) (kk!1 skolem-const-decl "below[length(args[variable, symbol, arity](t!1))]" unification nil) (positions_of_arg formula-decl nil positions nil) (resolving_diff_TCC7 subtype-tcc nil unification nil) (posint nonempty-type-eq-decl nil integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (t!1 skolem-const-decl "{t: term | unifiable(app(app1_var!1, app2_var!1), t) & app(app1_var!1, app2_var!1) /= t}" unification nil) (resolving_diff_TCC2 subtype-tcc nil unification nil) (subt_of_subt_is_subt_of_term formula-decl nil subterm nil) (term_app_extensionality formula-decl nil term_adt nil) (resolving_diff_TCC1 subtype-tcc nil unification nil) (first const-decl "T" seq_extras "structures/") (^ const-decl "finseq" finite_sequences nil) (rest const-decl "finseq" seq_extras "structures/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nat_min application-judgement "{k: nat | k <= i AND k <= j}" real_defs nil) (int_min application-judgement "{k: int | k <= i AND k <= j}" real_defs nil) (position_t_resolving_diff formula-decl nil unification nil) (position_s_resolving_diff formula-decl nil unification nil) (uni_diff_equal_length_arg formula-decl nil unification nil) (resolving_diff_TCC3 subtype-tcc nil unification nil) (app2_var!1 skolem-const-decl "{args: finite_sequence[term[variable, symbol, arity]] | args`length = arity(app1_var!1)}" unification nil) (app1_var!1 skolem-const-decl "symbol" unification nil) (k!1 skolem-const-decl "posint" unification nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (|#| const-decl "finite_sequence[T]" set2seq "structures/") (min const-decl "{a | S(a) AND (FORALL x: S(x) IMPLIES a <= x)}" min_nat nil) (<= const-decl "bool" reals nil) (nonempty? const-decl "bool" sets nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (app adt-constructor-decl "[[f: symbol, {args: finite_sequence[term] | args`length = arity(f)}] -> (app?)]" term_adt nil) (app? adt-recognizer-decl "[term -> boolean]" term_adt nil) (finite_sequence type-eq-decl nil finite_sequences nil) (ext def-decl "term" substitution nil) (NOT const-decl "[bool -> bool]" booleans nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (Sub type-eq-decl nil substitution nil) (Sub? const-decl "bool" substitution nil) (V const-decl "set[term]" variables_term nil) (set type-eq-decl nil sets nil) (< const-decl "bool" reals nil) (args adt-accessor-decl "[d: (app?) -> {args: finite_sequence[term] | args`length = arity(f(d))}]" term_adt nil) (f adt-accessor-decl "[(app?) -> symbol]" term_adt nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (unifier const-decl "bool" unification nil) (resolving_diff_has_unifiable_argument formula-decl nil unification nil) (empty_0 formula-decl nil seq_extras "structures/") (finseq type-eq-decl nil finite_sequences nil) (empty_seq const-decl "finseq" finite_sequences nil) (term_induction formula-decl nil term_adt nil) (variable formal-nonempty-type-decl nil unification nil) (symbol formal-nonempty-type-decl nil unification nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (arity formal-const-decl "[symbol -> nat]" unification nil) (subtermOF def-decl "term" subterm nil) (positions? type-eq-decl nil positions nil) (vars? adt-recognizer-decl "[term -> boolean]" term_adt nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (resolving_diff def-decl "position" unification nil) (= const-decl "[T, T -> boolean]" equalities nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (positionsOF def-decl "positions" positions nil) (positions type-eq-decl nil positions nil) (position type-eq-decl nil positions nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (below type-eq-decl nil nat_types nil) (/= const-decl "boolean" notequal nil) (unifiable const-decl "bool" unification nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (term type-decl nil term_adt nil)) shostak)) (unifier_o_TCC1 0 (unifier_o_TCC1-1 nil 3453458634 ("" (skeep) (("" (hide -) (("" (rewrite "subs_o") nil nil)) nil)) nil) ((arity formal-const-decl "[symbol -> nat]" unification nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (symbol formal-nonempty-type-decl nil unification nil) (variable formal-nonempty-type-decl nil unification nil) (Sub type-eq-decl nil substitution nil) (Sub? const-decl "bool" substitution nil) (V const-decl "set[term]" variables_term nil) (set type-eq-decl nil sets nil) (term type-decl nil term_adt nil) (subs_o formula-decl nil substitution nil)) nil)) (unifier_o 0 (unifier_o-1 nil 3453458641 ("" (skeep) (("" (expand "member") (("" (expand "U") (("" (expand "unifier") (("" (lemma "ext_o") (("" (inst -1 "sig" "theta") (("" (replace -1 1) (("" (expand "o" 1) (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((member const-decl "bool" sets nil) (unifier const-decl "bool" unification nil) (term type-decl nil term_adt nil) (set type-eq-decl nil sets nil) (V const-decl "set[term]" variables_term nil) (Sub? const-decl "bool" substitution nil) (Sub type-eq-decl nil substitution nil) (O const-decl "T3" function_props nil) (ext_o formula-decl nil substitution nil) (variable formal-nonempty-type-decl nil unification nil) (symbol formal-nonempty-type-decl nil unification nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (arity formal-const-decl "[symbol -> nat]" unification nil) (U const-decl "set[Sub]" unification nil)) shostak)) (mgu_o_TCC1 0 (mgu_o_TCC1-1 nil 3453191133 ("" (skeep) (("" (rewrite "subs_o") nil nil)) nil) ((subs_o formula-decl nil substitution nil) (term type-decl nil term_adt nil) (set type-eq-decl nil sets nil) (V const-decl "set[term]" variables_term nil) (Sub? const-decl "bool" substitution nil) (Sub type-eq-decl nil substitution nil) (variable formal-nonempty-type-decl nil unification nil) (symbol formal-nonempty-type-decl nil unification nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (arity formal-const-decl "[symbol -> nat]" unification nil)) nil)) (mgu_o_TCC2 0 (mgu_o_TCC2-1 nil 3453191133 ("" (skeep) (("" (rewrite "subs_o") nil nil)) nil) ((subs_o formula-decl nil substitution nil) (term type-decl nil term_adt nil) (set type-eq-decl nil sets nil) (V const-decl "set[term]" variables_term nil) (Sub? const-decl "bool" substitution nil) (Sub type-eq-decl nil substitution nil) (variable formal-nonempty-type-decl nil unification nil) (symbol formal-nonempty-type-decl nil unification nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (arity formal-const-decl "[symbol -> nat]" unification nil)) nil)) (mgu_o 0 (mgu_o-1 nil 3453191134 ("" (skeep) (("" (expand "<=") (("" (skeep -1) (("" (inst 1 "tau") (("" (replaces -1) (("" (lemma "o_ass") (("" (inst -1 "sig" "tau" "theta") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((<= const-decl "bool" unification nil) (variable formal-nonempty-type-decl nil unification nil) (symbol formal-nonempty-type-decl nil unification nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (arity formal-const-decl "[symbol -> nat]" unification nil) (term type-decl nil term_adt nil) (set type-eq-decl nil sets nil) (V const-decl "set[term]" variables_term nil) (Sub? const-decl "bool" substitution nil) (Sub type-eq-decl nil substitution nil) (o_ass formula-decl nil substitution nil)) shostak)) (unifier_and_subs_TCC1 0 (unifier_and_subs_TCC1-1 nil 3454365467 ("" (skosimp*) (("" (typepred "sig!1" "theta!1") (("" (hide -3) (("" (rewrite "subs_o") nil nil)) nil)) nil)) nil) ((Sub type-eq-decl nil substitution nil) (Sub? const-decl "bool" substitution nil) (V const-decl "set[term]" variables_term nil) (set type-eq-decl nil sets nil) (term type-decl nil term_adt nil) (arity formal-const-decl "[symbol -> nat]" unification nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (symbol formal-nonempty-type-decl nil unification nil) (variable formal-nonempty-type-decl nil unification nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (subs_o formula-decl nil substitution nil)) nil)) (unifier_and_subs 0 (unifier_and_subs-1 nil 3454365467 ("" (skosimp*) (("" (expand "member") (("" (expand "U") (("" (expand "unifier") (("" (rewrite "ext_o") (("" (expand "o") (("" (replaces -1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((member const-decl "bool" sets nil) (unifier const-decl "bool" unification nil) (O const-decl "T3" function_props nil) (arity formal-const-decl "[symbol -> nat]" unification nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (symbol formal-nonempty-type-decl nil unification nil) (variable formal-nonempty-type-decl nil unification nil) (Sub type-eq-decl nil substitution nil) (Sub? const-decl "bool" substitution nil) (V const-decl "set[term]" variables_term nil) (set type-eq-decl nil sets nil) (term type-decl nil term_adt nil) (ext_o formula-decl nil substitution nil) (U const-decl "set[Sub]" unification nil)) shostak)) (idemp_mgu_iff_all_unifier 0 (idemp_mgu_iff_all_unifier-1 nil 3454363417 ("" (skosimp*) (("" (prop) (("1" (skosimp*) (("1" (expand "mgu") (("1" (inst -1 "sig!1") (("1" (expand "<=") (("1" (skosimp*) (("1" (expand "idempotent_sub?") (("1" (copy -1) (("1" (replace -3 -2 rl) (("1" (lemma "o_ass") (("1" (inst -1 "theta!1" "tau!1" "theta!1") (("1" (replace -1 -3 rl) (("1" (replace -2 -3 rl) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "mgu") (("2" (skosimp*) (("2" (expand "<=") (("2" (inst -2 "sigma!1") (("2" (inst 1 "sigma!1") nil nil)) nil)) nil)) nil)) nil) ("3" (expand "idempotent_sub?") (("3" (typepred "theta!1") (("3" (hide -1) (("3" (inst -2 "theta!1") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((mgu const-decl "bool" unification nil) (<= const-decl "bool" unification nil) (idempotent_sub? const-decl "bool" substitution nil) (o_ass formula-decl nil substitution nil) (U const-decl "set[Sub]" unification nil) (member const-decl "bool" sets nil) (Sub type-eq-decl nil substitution nil) (Sub? const-decl "bool" substitution nil) (V const-decl "set[term]" variables_term nil) (set type-eq-decl nil sets nil) (term type-decl nil term_adt nil) (arity formal-const-decl "[symbol -> nat]" unification nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (symbol formal-nonempty-type-decl nil unification nil) (variable formal-nonempty-type-decl nil unification nil) (t!1 skolem-const-decl "term[variable, symbol, arity]" unification nil) (s!1 skolem-const-decl "term[variable, symbol, arity]" unification nil) (sigma!1 skolem-const-decl "Sub[variable, symbol, arity]" unification nil) (NOT const-decl "[bool -> bool]" booleans nil)) shostak)) (unifiable_terms_unifiable_args 0 (unifiable_terms_unifiable_args-1 nil 3456581410 ("" (skosimp) (("" (expand* "member" "U" "unifier") (("" (lemma "subterm_ext_commute") (("" (inst -1 "p!1" "s!1" "sig!1") (("" (assert) (("" (lemma "subterm_ext_commute") (("" (inst -1 "p!1" "t!1" "sig!1") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((U const-decl "set[Sub]" unification nil) (unifier const-decl "bool" unification nil) (member const-decl "bool" sets nil) (below type-eq-decl nil nat_types nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (position type-eq-decl nil positions nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (term type-decl nil term_adt nil) (positions type-eq-decl nil positions nil) (positionsOF def-decl "positions" positions nil) (set type-eq-decl nil sets nil) (V const-decl "set[term]" variables_term nil) (Sub? const-decl "bool" substitution nil) (Sub type-eq-decl nil substitution nil) (subterm_ext_commute formula-decl nil substitution nil) (variable formal-nonempty-type-decl nil unification nil) (symbol formal-nonempty-type-decl nil unification nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (arity formal-const-decl "[symbol -> nat]" unification nil)) shostak)) (var_term_unifiable_not_var_in_term_TCC1 0 (var_term_unifiable_not_var_in_term_TCC1-1 nil 3452358872 ("" (subtype-tcc) nil nil) ((unifier const-decl "bool" unification nil) (unifiable const-decl "bool" unification nil) (/= const-decl "boolean" notequal nil) (arity formal-const-decl "[symbol -> nat]" unification nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (symbol formal-nonempty-type-decl nil unification nil) (variable formal-nonempty-type-decl nil unification nil) (V const-decl "set[term]" variables_term nil)) nil)) (var_term_unifiable_not_var_in_term 0 (var_term_unifiable_not_var_in_term-1 nil 3452444318 ("" (skosimp) (("" (case "positionsOF(t!1) = only_empty_seq") (("1" (copy -1) (("1" (expand "positionsOF" -2) (("1" (lift-if) (("1" (prop) (("1" (hide -2 -3 -4) (("1" (lemma "Vars_is_var") (("1" (inst -1 "t!1") (("1" (assert) (("1" (hide -2) (("1" (replaces -1) (("1" (expand "member") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand* "member" "Vars") (("2" (skosimp) (("2" (case "p!1 = empty_seq") (("1" (replaces -1) (("1" (hide-all-but (-5 2)) (("1" (expand "subtermOF") (("1" (rewrite "empty_0") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (typepred "p!1") (("2" (hide-all-but (-1 -3 1)) (("2" (replaces -2) (("2" (expand "only_empty_seq") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "finseq_appl") (("3" (expand "member" -5) (("3" (expand "Vars") (("3" (skosimp) (("3" (hide -1) (("3" (case-replace "p!1 = empty_seq") (("1" (expand "subtermOF") (("1" (rewrite "empty_0") (("1" (assert) nil nil)) nil)) nil) ("2" (hide-all-but (-1 1)) (("2" (decompose-equality -1) (("2" (inst -1 "p!1") (("2" (assert) (("2" (expand "only_empty_seq") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand* "member" "Vars") (("2" (skosimp) (("2" (expand "unifiable") (("2" (skosimp) (("2" (expand "unifier") (("2" (copy -2) (("2" (replace -4 -1 rl) (("2" (lemma "subterm_ext_commute") (("2" (inst?) (("2" (assert) (("2" (replace -1 -2 rl) (("2" (hide -1) (("2" (lemma "term_eq_subterm") (("2" (inst -1 "p!1" "ext(sigma!1)(t!1)") (("2" (assert) (("2" (rewrite "ext_preserv_pos") (("2" (hide-all-but (-1 -5 2)) (("2" (replaces -1) (("2" (expand "subtermOF") (("2" (rewrite "empty_0") (("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) ((only_empty_seq const-decl "positions" positions nil) (positionsOF def-decl "positions" positions nil) (term type-decl nil term_adt nil) (= const-decl "[T, T -> boolean]" equalities nil) (positions type-eq-decl nil positions nil) (position type-eq-decl nil positions nil) (arity formal-const-decl "[symbol -> nat]" unification nil) (symbol formal-nonempty-type-decl nil unification nil) (variable formal-nonempty-type-decl nil unification nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (Vars_is_var formula-decl nil subterm nil) (member const-decl "bool" sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (subtermOF def-decl "term" subterm nil) (empty_0 formula-decl nil seq_extras "structures/") (< const-decl "bool" reals nil) (positions? type-eq-decl nil positions nil) (finseq type-eq-decl nil finite_sequences nil) (empty_seq const-decl "finseq" finite_sequences nil) (Vars const-decl "set[(V)]" subterm nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (subterm_ext_commute formula-decl nil substitution nil) (ext def-decl "term" substitution nil) (ext_preserv_pos formula-decl nil substitution nil) (term_eq_subterm formula-decl nil subterm nil) (set type-eq-decl nil sets nil) (V const-decl "set[term]" variables_term nil) (Sub? const-decl "bool" substitution nil) (Sub type-eq-decl nil substitution nil) (unifier const-decl "bool" unification nil) (unifiable const-decl "bool" unification nil)) shostak)) (sub_of_frst_diff_TCC1 0 (sub_of_frst_diff_TCC1-1 nil 3450001666 ("" (skosimp) (("" (typepred "t!1") (("" (lemma "position_s_resolving_diff") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((/= const-decl "boolean" notequal nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (unifiable const-decl "bool" unification nil) (term type-decl nil term_adt nil) (arity formal-const-decl "[symbol -> nat]" unification nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (symbol formal-nonempty-type-decl nil unification nil) (variable formal-nonempty-type-decl nil unification nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (below type-eq-decl nil nat_types nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (position type-eq-decl nil positions nil) (position_s_resolving_diff formula-decl nil unification nil)) nil)) (sub_of_frst_diff_TCC2 0 (sub_of_frst_diff_TCC2-1 nil 3450001666 ("" (skosimp*) (("" (lemma "position_t_resolving_diff") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil) ((position_t_resolving_diff formula-decl nil unification nil) (position type-eq-decl nil positions nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (below type-eq-decl nil nat_types nil) (/= const-decl "boolean" notequal nil) (unifiable const-decl "bool" unification nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (term type-decl nil term_adt nil) (arity formal-const-decl "[symbol -> nat]" unification nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (symbol formal-nonempty-type-decl nil unification nil) (variable formal-nonempty-type-decl nil unification nil)) nil)) (sub_of_frst_diff_TCC3 0 (sub_of_frst_diff_TCC3-1 nil 3449911225 ("" (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 1 "N!1" "f!1") (("1" (hide-all-but (-1 1)) (("1" (expand "injective?") (("1" (skeep) (("1" (inst -1 "x1" "x2") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (skeep) (("2" (prop) (("1" (assert) (("1" (hide -3 -4 -7) (("1" (lemma "resolving_diff_has_diff_argument") (("1" (inst -1 "s!1" "t!1" "k!1") (("1" (assert) nil nil) ("2" (hide-all-but (-3 1)) (("2" (lemma "position_s_resolving_diff") (("2" (lemma "position_t_resolving_diff") (("2" (inst -1 "s!1" "t!1" "k!1") (("2" (inst -2 "s!1" "t!1" "k!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((arity formal-const-decl "[symbol -> nat]" unification nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (symbol formal-nonempty-type-decl nil unification nil) (variable formal-nonempty-type-decl nil unification nil) (Vars_is_var formula-decl nil subterm nil) (term type-decl nil term_adt nil) (resolving_diff_has_diff_argument formula-decl nil unification nil) (position_t_resolving_diff formula-decl nil unification nil) (position_s_resolving_diff formula-decl nil unification nil) (t!1 skolem-const-decl "{t: term | unifiable(s!1, t) & s!1 /= t}" unification nil) (unifiable const-decl "bool" unification nil) (k!1 skolem-const-decl "position[variable, symbol, arity]" unification nil) (s!1 skolem-const-decl "term[variable, symbol, arity]" unification nil) (positionsOF def-decl "positions" positions nil) (positions type-eq-decl nil positions nil) (position type-eq-decl nil positions nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (injective? const-decl "bool" functions nil) (below type-eq-decl nil nat_types nil) (< const-decl "bool" reals nil) (set type-eq-decl nil sets nil) (V const-decl "set[term]" variables_term nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (sp!1 skolem-const-decl "term[variable, symbol, arity]" unification nil) (/= const-decl "boolean" notequal nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (tp!1 skolem-const-decl "term[variable, symbol, arity]" unification nil) (is_finite const-decl "bool" finite_sets nil) (Sub? const-decl "bool" substitution nil) (Dom const-decl "set[(V)]" substitution nil) (vars_of_term_finite formula-decl nil subterm nil)) nil)) (sub_of_frst_diff_TCC4 0 (sub_of_frst_diff_TCC4-1 nil 3449911225 ("" (skosimp*) (("" (lemma "resolving_diff_vars") (("" (inst -1 "s!1" "t!1" "k!1") (("1" (assert) (("1" (hide 1) (("1" (lemma "Vars_is_var") (("1" (inst -1 "tp!1") (("1" (assert) (("1" (lemma "vars_of_term_finite") (("1" (inst -1 "tp!1") (("1" (replaces -2) (("1" (expand* "Sub?" "Dom" "is_finite") (("1" (skosimp) (("1" (inst 1 "N!1" "f!1") (("1" (hide-all-but (-1 1)) (("1" (expand "injective?") (("1" (skeep) (("1" (inst -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) ("2" (hide-all-but (-1 1)) (("2" (lemma "position_s_resolving_diff") (("2" (lemma "position_t_resolving_diff") (("2" (inst -1 "s!1" "t!1" "k!1") (("2" (inst -2 "s!1" "t!1" "k!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((resolving_diff_vars formula-decl nil unification nil) (position_t_resolving_diff formula-decl nil unification nil) (position_s_resolving_diff formula-decl nil unification nil) (Vars_is_var formula-decl nil subterm nil) (Dom const-decl "set[(V)]" substitution nil) (is_finite const-decl "bool" finite_sets nil) (Sub? const-decl "bool" substitution nil) (set type-eq-decl nil sets nil) (V const-decl "set[term]" variables_term nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (tp!1 skolem-const-decl "term[variable, symbol, arity]" unification nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (sp!1 skolem-const-decl "term[variable, symbol, arity]" unification nil) (< const-decl "bool" reals nil) (injective? const-decl "bool" functions nil) (vars_of_term_finite formula-decl nil subterm nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (variable formal-nonempty-type-decl nil unification nil) (symbol formal-nonempty-type-decl nil unification nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (arity formal-const-decl "[symbol -> nat]" unification nil) (term type-decl nil term_adt nil) (below type-eq-decl nil nat_types nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (position type-eq-decl nil positions nil) (positions type-eq-decl nil positions nil) (positionsOF def-decl "positions" positions nil) (s!1 skolem-const-decl "term[variable, symbol, arity]" unification nil) (k!1 skolem-const-decl "position[variable, symbol, arity]" unification nil) (unifiable const-decl "bool" unification nil) (/= const-decl "boolean" notequal nil) (t!1 skolem-const-decl "{t: term | unifiable(s!1, t) & s!1 /= t}" unification nil)) nil)) (dom_sub_of_frst_diff_is_TCC1 0 (dom_sub_of_frst_diff_is_TCC1-1 nil 3457954512 ("" (skosimp) (("" (hide -1 1) (("" (lemma "position_t_resolving_diff") (("" (inst -1 "s!1" "t!1" "p!1") (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((variable formal-nonempty-type-decl nil unification nil) (symbol formal-nonempty-type-decl nil unification nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (arity formal-const-decl "[symbol -> nat]" unification nil) (term type-decl nil term_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (unifiable const-decl "bool" unification nil) (/= const-decl "boolean" notequal nil) (below type-eq-decl nil nat_types nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (position type-eq-decl nil positions nil) (position_t_resolving_diff formula-decl nil unification nil)) nil)) (dom_sub_of_frst_diff_is 0 (dom_sub_of_frst_diff_is-1 nil 3457717627 ("" (skosimp) (("" (expand* "restrict" "singleton") (("" (prop) (("1" (decompose-equality 1) (("1" (iff) (("1" (prop) (("1" (expand* "Dom" "sub_of_frst_diff") (("1" (decompose-equality -3) (("1" (inst -1 "x!1") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (decompose-equality -3) (("2" (inst -1 "x!1") (("2" (expand* "Dom" "sub_of_frst_diff") (("2" (assert) (("2" (replaces -2) (("2" (prop) (("2" (replaces -2) (("2" (hide -2) (("2" (replaces -2) (("2" (lemma "resolving_diff_has_diff_argument") (("2" (inst -1 "s!1" "t!1" "resolving_diff(s!1, t!1)") (("1" (assert) nil nil) ("2" (hide -) (("2" (rewrite "position_t_resolving_diff") (("2" (lemma "position_s_resolving_diff") (("2" (inst -1 "s!1" "t!1" "resolving_diff(s!1, t!1)") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (decompose-equality 2) (("1" (iff) (("1" (prop) (("1" (decompose-equality -2) (("1" (inst -1 "x!1") (("1" (expand* "Dom" "sub_of_frst_diff") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (decompose-equality -2) (("2" (inst -1 "x!1") (("2" (expand* "Dom" "sub_of_frst_diff") (("2" (assert) (("2" (replaces -2) (("2" (prop) (("2" (replaces -2) (("2" (hide 1) (("2" (lemma "resolving_diff_has_diff_argument") (("2" (inst -1 "s!1" "t!1" "p!1") (("1" (assert) nil nil) ("2" (hide -) (("2" (rewrite "position_t_resolving_diff") (("2" (lemma "position_s_resolving_diff") (("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)) nil)) nil)) nil) ("2" (skosimp) (("2" (hide-all-but 1) (("2" (rewrite "position_t_resolving_diff") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((singleton const-decl "(singleton?)" sets nil) (restrict const-decl "R" restrict nil) (p!1 skolem-const-decl "position[variable, symbol, arity]" unification nil) (Dom const-decl "set[(V)]" substitution nil) (Sub? const-decl "bool" substitution nil) (Sub type-eq-decl nil substitution nil) (= const-decl "[T, T -> boolean]" equalities nil) (below type-eq-decl nil nat_types nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (position type-eq-decl nil positions nil) (positions type-eq-decl nil positions nil) (positionsOF def-decl "positions" positions nil) (positions? type-eq-decl nil positions nil) (subtermOF def-decl "term" subterm nil) (V const-decl "set[term]" variables_term nil) (set type-eq-decl nil sets nil) (term type-decl nil term_adt nil) (arity formal-const-decl "[symbol -> nat]" unification nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (symbol formal-nonempty-type-decl nil unification nil) (variable formal-nonempty-type-decl nil unification nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (unifiable const-decl "bool" unification nil) (/= const-decl "boolean" notequal nil) (resolving_diff def-decl "position" unification nil) (sub_of_frst_diff const-decl "Sub" unification nil) (resolving_diff_has_diff_argument formula-decl nil unification nil) (position_s_resolving_diff formula-decl nil unification nil) (position_t_resolving_diff formula-decl nil unification nil) (t!1 skolem-const-decl "{t: term | unifiable(s!1, t) & s!1 /= t}" unification nil) (s!1 skolem-const-decl "term[variable, symbol, arity]" unification nil)) shostak)) (var_sub_1stdiff_not_member_term 0 (var_sub_1stdiff_not_member_term-1 nil 3452327480 ("" (assert) (("" (skosimp*) (("" (typepred "r!1") (("" (typepred "x!1") (("" (hide -1) (("" (name-replace "sig!1" "sub_of_frst_diff(s!1, t!1)" :hide? nil) (("" (expand* "member" "Dom" "Ran" "Vars") (("" (skosimp*) (("" (expand "member") (("" (lemma "dom_sub_of_frst_diff_is") (("" (inst -1 "resolving_diff(s!1, t!1)" "s!1" "t!1" "sig!1") (("" (assert) (("" (prop) (("1" (expand* "restrict" "singleton") (("1" (decompose-equality -2) (("1" (copy -1) (("1" (inst -2 "x!2") (("1" (inst -1 "x!1") (("1" (assert) (("1" (expand "Dom" -1) (("1" (replaces -1) (("1" (replaces -1) (("1" (hide -2 -3 1) (("1" (lemma "var_term_unifiable_not_var_in_term") (("1" (inst -1 "subtermOF(s!1, resolving_diff(s!1, t!1))" "r!1") (("1" (assert) (("1" (prop) (("1" (expand* "member" "Vars") (("1" (inst 1 "p!1") nil nil)) nil) ("2" (reveal -2) (("2" (replace -1 -3 rl) (("2" (expand "sub_of_frst_diff" -3) (("2" (hide -1 -2 -4) (("2" (replaces -1) (("2" (rewrite "resolving_diff_has_unifiable_argument") (("2" (hide 2) (("2" (rewrite "position_t_resolving_diff") (("2" (lemma "position_s_resolving_diff") (("2" (inst -1 "s!1" "t!1" "resolving_diff(s!1, t!1)") 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" (expand* "restrict" "singleton") (("2" (decompose-equality -1) (("1" (copy -1) (("1" (inst -2 "x!1") (("1" (inst -1 "x!2") (("1" (expand "Dom" -2) (("1" (assert) (("1" (replaces -1) (("1" (replaces -1) (("1" (lemma "resolving_diff_vars") (("1" (inst -1 "s!1" "t!1" "resolving_diff(s!1, t!1)") (("1" (assert) (("1" (lemma "var_term_unifiable_not_var_in_term") (("1" (inst -1 "subtermOF(t!1, resolving_diff(s!1, t!1))" "r!1") (("1" (assert) (("1" (prop) (("1" (hide-all-but (-5 1)) (("1" (expand* "member" "Vars") (("1" (inst 1 "p!1") nil nil)) nil)) nil) ("2" (hide -3 -5 3) (("2" (replace -2 -3 rl) (("2" (expand "sub_of_frst_diff" -3) (("2" (replaces -3) (("2" (hide - 2) (("2" (lemma "resolving_diff_has_unifiable_argument") (("2" (inst -1 "s!1" "t!1" "resolving_diff(s!1, t!1)") (("1" (expand* "unifiable" "unifier") (("1" (skosimp) (("1" (inst 1 "sigma!1") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (rewrite "position_t_resolving_diff") (("2" (lemma "position_s_resolving_diff") (("2" (inst -1 "s!1" "t!1" "resolving_diff(s!1, t!1)") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (rewrite "position_t_resolving_diff") (("2" (lemma "position_s_resolving_diff") (("2" (inst -1 "s!1" "t!1" "resolving_diff(s!1, t!1)") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (rewrite "position_t_resolving_diff") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((Dom const-decl "set[(V)]" substitution nil) (= const-decl "[T, T -> boolean]" equalities nil) (dom_sub_of_frst_diff_is formula-decl nil unification nil) (s!1 skolem-const-decl "term[variable, symbol, arity]" unification nil) (t!1 skolem-const-decl "{t: term | unifiable(s!1, t) & s!1 /= t}" unification nil) (unifier const-decl "bool" unification nil) (resolving_diff_vars formula-decl nil unification nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (singleton const-decl "(singleton?)" sets nil) (restrict const-decl "R" restrict nil) (var_term_unifiable_not_var_in_term formula-decl nil unification nil) (position_s_resolving_diff formula-decl nil unification nil) (position_t_resolving_diff formula-decl nil unification nil) (resolving_diff_has_unifiable_argument formula-decl nil unification nil) (positions type-eq-decl nil positions nil) (positionsOF def-decl "positions" positions nil) (positions? type-eq-decl nil positions nil) (subtermOF def-decl "term" subterm nil) (below type-eq-decl nil nat_types nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (position type-eq-decl nil positions nil) (resolving_diff def-decl "position" unification nil) (Vars const-decl "set[(V)]" subterm nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (variable formal-nonempty-type-decl nil unification nil) (symbol formal-nonempty-type-decl nil unification nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (arity formal-const-decl "[symbol -> nat]" unification nil) (term type-decl nil term_adt nil) (set type-eq-decl nil sets nil) (member const-decl "bool" sets nil) (V const-decl "set[term]" variables_term nil) (Ran const-decl "set[term]" substitution nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (unifiable const-decl "bool" unification nil) (/= const-decl "boolean" notequal nil) (Sub? const-decl "bool" substitution nil) (Sub type-eq-decl nil substitution nil) (sub_of_frst_diff const-decl "Sub" unification nil)) shostak)) (sub_of_frst_diff_unifier_o 0 (sub_of_frst_diff_unifier_o-1 nil 3453566637 ("" (skosimp) (("" (assert) (("" (name-replace "sig!1" "sub_of_frst_diff(s!1, t!1)" :hide? nil) (("" (name "p!1" "resolving_diff(s!1, t!1)") (("" (inst 1 "rho!1") (("" (lemma "unifiable_terms_unifiable_args") (("" (inst -1 "rho!1" "s!1" "t!1" "p!1") (("1" (assert) (("1" (expand* "member" "U" "unifier") (("1" (decompose-equality 1) (("1" (expand "comp") (("1" (case "vars?(subtermOF(s!1, p!1))") (("1" (case "x!1 = subtermOF(s!1, p!1)") (("1" (replace -5 1 rl) (("1" (expand "sub_of_frst_diff" 1) (("1" (assert) (("1" (replace -4 1) (("1" (replace -1 -3 rl) (("1" (hide-all-but (-3 1)) (("1" (expand "ext" -1 1) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -4 2 rl) (("2" (expand "sub_of_frst_diff" 2) (("2" (assert) (("2" (hide-all-but 2) (("2" (typepred "x!1") (("2" (expand* "V" "ext") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "vars?(subtermOF(t!1, p!1))") (("1" (case "x!1 = subtermOF(t!1, p!1)") (("1" (replace -5 2 rl) (("1" (expand "sub_of_frst_diff" 2) (("1" (assert) (("1" (replace -4 2) (("1" (replace -1 -3 rl) (("1" (hide-all-but (-3 2)) (("1" (expand "ext" -1 2) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -4 3 rl) (("2" (expand "sub_of_frst_diff" 3) (("2" (assert) (("2" (hide-all-but 3) (("2" (typepred "x!1") (("2" (expand* "V" "ext") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-2 1 2)) (("2" (lemma "resolving_diff_vars") (("2" (inst -1 "s!1" "t!1" "p!1") (("1" (assert) nil nil) ("2" (hide 2 3) (("2" (rewrite "position_t_resolving_diff") (("2" (lemma "position_s_resolving_diff") (("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) ("2" (hide-all-but (-1 1)) (("2" (rewrite "position_t_resolving_diff") (("2" (lemma "position_s_resolving_diff") (("2" (inst -1 "s!1" "t!1" "p!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((resolving_diff def-decl "position" unification nil) (position type-eq-decl nil positions nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (below type-eq-decl nil nat_types nil) (unifiable_terms_unifiable_args formula-decl nil unification nil) (comp const-decl "term" substitution nil) (vars? adt-recognizer-decl "[term -> boolean]" term_adt nil) (positions? type-eq-decl nil positions nil) (subtermOF def-decl "term" subterm nil) (NOT const-decl "[bool -> bool]" booleans nil) (ext def-decl "term" substitution nil) (position_t_resolving_diff formula-decl nil unification nil) (position_s_resolving_diff formula-decl nil unification nil) (resolving_diff_vars formula-decl nil unification nil) (member const-decl "bool" sets nil) (unifier const-decl "bool" unification nil) (U const-decl "set[Sub]" unification nil) (t!1 skolem-const-decl "{t: term | unifiable(s!1, t) & s!1 /= t}" unification nil) (p!1 skolem-const-decl "position[variable, symbol, arity]" unification nil) (s!1 skolem-const-decl "term[variable, symbol, arity]" unification nil) (positionsOF def-decl "positions" positions nil) (positions type-eq-decl nil positions nil) (sub_of_frst_diff const-decl "Sub" unification nil) (Sub type-eq-decl nil substitution nil) (Sub? const-decl "bool" substitution nil) (/= const-decl "boolean" notequal nil) (unifiable const-decl "bool" unification nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (V const-decl "set[term]" variables_term nil) (set type-eq-decl nil sets nil) (term type-decl nil term_adt nil) (arity formal-const-decl "[symbol -> nat]" unification nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (symbol formal-nonempty-type-decl nil unification nil) (variable formal-nonempty-type-decl nil unification nil)) shostak)) (ext_sub_of_frst_diff_unifiable 0 (ext_sub_of_frst_diff_unifiable-1 nil 3454057906 ("" (skosimp) (("" (lemma "sub_of_frst_diff_unifier_o") (("" (typepred "t!1") (("" (expand* "unifiable" "member" "U") (("" (skeep -1) (("" (inst -2 "sigma" "s!1" "t!1") (("" (assert) (("" (skeep -2) (("" (inst 2 "theta") (("" (replace -2 -1) (("" (expand "unifier") (("" (rewrite "ext_o") (("" (expand "o") (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((sub_of_frst_diff_unifier_o formula-decl nil unification nil) (member const-decl "bool" sets nil) (U const-decl "set[Sub]" unification nil) (set type-eq-decl nil sets nil) (V const-decl "set[term]" variables_term nil) (Sub? const-decl "bool" substitution nil) (Sub type-eq-decl nil substitution nil) (sub_of_frst_diff const-decl "Sub" unification nil) (ext_o formula-decl nil substitution nil) (O const-decl "T3" function_props nil) (unifier const-decl "bool" unification nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (variable formal-nonempty-type-decl nil unification nil) (symbol formal-nonempty-type-decl nil unification nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (arity formal-const-decl "[symbol -> nat]" unification nil) (term type-decl nil term_adt nil) (unifiable const-decl "bool" unification nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil)) shostak)) (sub_of_frst_diff_remove_x 0 (sub_of_frst_diff_remove_x-1 nil 3457715688 ("" (skosimp) (("" (assert) (("" (name-replace "sig!1" "sub_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" (hide -3) (("1" (lemma "var_sub_1stdiff_not_member_term") (("1" (inst -1 "s!1" "t!1") (("1" (replaces -4) (("1" (assert) (("1" (inst -1 "x!1" "r!1") (("1" (hide -2 -3) (("1" (expand "member") (("1" (propax) nil nil)) nil)) nil) ("2" (hide -1 -2) (("2" (expand "member") (("2" (propax) nil 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" (hide -3) (("2" (lemma "var_sub_1stdiff_not_member_term") (("2" (inst -1 "s!1" "t!1") (("2" (replaces -4) (("2" (assert) (("2" (inst -1 "x!1" "r!1") (("1" (hide -2 -3) (("1" (expand "member") (("1" (propax) nil nil)) nil)) nil) ("2" (hide -1 -2) (("2" (expand "member") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((var_sub_1stdiff_not_member_term formula-decl nil unification nil) (Ran const-decl "set[term]" substitution nil) (Dom const-decl "set[(V)]" substitution nil) (member const-decl "bool" sets nil) (x!1 skolem-const-decl "(V)" unification nil) (sig!1 skolem-const-decl "Sub[variable, symbol, arity]" unification nil) (r!1 skolem-const-decl "term[variable, symbol, arity]" unification nil) (vars_subst_not_in formula-decl nil substitution nil) (r!1 skolem-const-decl "term[variable, symbol, arity]" unification nil) (sub_of_frst_diff const-decl "Sub" unification nil) (Sub type-eq-decl nil substitution nil) (Sub? const-decl "bool" substitution nil) (/= const-decl "boolean" notequal nil) (unifiable const-decl "bool" unification nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (V const-decl "set[term]" variables_term nil) (set type-eq-decl nil sets nil) (term type-decl nil term_adt nil) (arity formal-const-decl "[symbol -> nat]" unification nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (symbol formal-nonempty-type-decl nil unification nil) (variable formal-nonempty-type-decl nil unification nil)) shostak)) (vars_sub_of_frst_diff_s_is_subset_union 0 (vars_sub_of_frst_diff_s_is_subset_union-1 nil 3457876813 ("" (skosimp) (("" (assert) (("" (name-replace "sig!1" "sub_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_sub_of_frst_diff_is") (("1" (inst -1 "resolving_diff(s!1, t!1)" "s!1" "t!1" "sig!1") (("1" (assert) (("1" (prop) (("1" (expand* "restrict" "singleton") (("1" (decompose-equality -2) (("1" (typepred "i!1") (("1" (inst -3 "i!1") (("1" (assert) (("1" (replaces -3) (("1" (hide -1) (("1" (replace -4 -3 rl) (("1" (expand "sub_of_frst_diff" -3) (("1" (hide-all-but (-3 2)) (("1" (expand "Vars") (("1" (skosimp) (("1" (typepred "p!1") (("1" (lemma "pos_o_term") (("1" (inst -1 "resolving_diff(s!1, t!1)" "p!1" "t!1") (("1" (assert) (("1" (prop) (("1" (inst 1 "resolving_diff(s!1, t!1) o p!1") (("1" (rewrite "pos_subterm") nil nil)) nil) ("2" (hide-all-but 1) (("2" (rewrite "position_t_resolving_diff") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand* "restrict" "singleton") (("2" (decompose-equality -1) (("1" (typepred "i!1") (("1" (inst -3 "i!1") (("1" (assert) (("1" (replaces -3) (("1" (expand "V") (("1" (replace -4 -3 rl) (("1" (expand "sub_of_frst_diff" -3) (("1" (hide-all-but (-3 2)) (("1" (expand "Vars") (("1" (skosimp) (("1" (typepred "p!1") (("1" (lemma "pos_o_term") (("1" (inst -1 "resolving_diff(s!1, t!1)" "p!1" "s!1") (("1" (assert) (("1" (prop) (("1" (inst 1 "resolving_diff(s!1, t!1) o p!1") (("1" (rewrite "pos_subterm") nil nil)) nil) ("2" (hide-all-but 1) (("2" (lemma "position_s_resolving_diff") (("2" (inst -1 "s!1" "t!1" "resolving_diff(s!1, t!1)") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (rewrite "position_t_resolving_diff") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "member") (("2" (lemma "resolving_diff_vars") (("2" (inst -1 "s!1" "t!1" "resolving_diff(s!1, t!1)") (("1" (split) (("1" (case "VRan(sig!1) = Vars(subtermOF(t!1, resolving_diff(s!1, t!1)))") (("1" (replaces -1) (("1" (lemma "sub_of_frst_diff_remove_x") (("1" (inst -1 "x!1" "s!1" "t!1") (("1" (assert) (("1" (replace -3 -1) (("1" (expand "member") (("1" (lemma "positions_of_ext") (("1" (inst -1 "sig!1" "s!1") (("1" (decompose-equality -1) (("1" (expand "Vars" -4) (("1" (skosimp) (("1" (inst -1 "p!1") (("1" (assert) (("1" (expand "union") (("1" (prop) (("1" (expand "member") (("1" (flatten) (("1" (rewrite "subterm_ext_commute") (("1" (decompose-equality -4) (("1" (prop) (("1" (hide-all-but (-1 1)) (("1" (expand "ext") (("1" (assert) (("1" (lift-if) (("1" (prop) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but -2) (("2" (typepred "x!1") (("2" (expand "V") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "member") (("2" (skosimp) (("2" (replace -1 -7) (("2" (rewrite "pos_subterm") (("2" (rewrite "subterm_ext_commute") (("2" (expand "ext" -7) (("2" (assert) (("2" (case "subtermOF(s!1, p1!1) = subtermOF(s!1, resolving_diff(s!1, t!1))") (("1" (replace -7 -8 rl) (("1" (expand "sub_of_frst_diff" -8) (("1" (assert) (("1" (expand "Vars" 2) (("1" (inst 2 "p2!1") nil nil)) nil)) nil)) nil)) nil) ("2" (replace -6 -7 rl) (("2" (expand "sub_of_frst_diff" -7) (("2" (assert) (("2" (replace -6 -4 rl) (("2" (expand "ext" -4) (("2" (expand "sub_of_frst_diff" -4) (("2" (lemma "pos_o_term") (("2" (inst -1 "p1!1" "p2!1" "s!1") (("2" (assert) (("2" (lemma "pos_subterm") (("2" (inst -1 "p1!1" "p2!1" "s!1") (("2" (assert) (("2" (replace -1 -9 rl) (("2" (hide-all-but (-9 4)) (("2" (expand "Vars") (("2" (inst 1 "p1!1 o p2!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (decompose-equality 1) (("2" (iff) (("2" (prop) (("1" (expand "VRan" -1) (("1" (expand "IUnion") (("1" (skosimp) (("1" (lemma "dom_sub_of_frst_diff_is") (("1" (inst -1 "resolving_diff(s!1, t!1)" "s!1" "t!1" "sig!1") (("1" (assert) (("1" (expand* "restrict" "singleton") (("1" (decompose-equality -1) (("1" (inst -1 "i!1") (("1" (assert) (("1" (replaces -1) (("1" (replace -3 -1 rl) (("1" (expand "sub_of_frst_diff" -1) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "VRan" 1) (("2" (expand "IUnion") (("2" (inst 1 "subtermOF(s!1, resolving_diff(s!1, t!1))") (("1" (replace -3 1 rl) (("1" (expand "sub_of_frst_diff" 1) (("1" (propax) nil nil)) nil)) nil) ("2" (expand "V") (("2" (hide -1 -4 2 3 4) (("2" (expand "Dom") (("2" (replace -2 1 rl) (("2" (expand "sub_of_frst_diff" 1) (("2" (lemma "resolving_diff_has_diff_argument") (("2" (inst -1 "s!1" "t!1" "resolving_diff(s!1, t!1)") (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (rewrite "position_t_resolving_diff") (("2" (lemma "position_s_resolving_diff") (("2" (inst -1 "s!1" "t!1" "resolving_diff(s!1, t!1)") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (rewrite "position_t_resolving_diff") nil nil)) nil)) nil) ("2" (case "vars?(subtermOF(s!1, resolving_diff(s!1, t!1)))") (("1" (case "VRan(sig!1) = Vars(subtermOF(t!1, resolving_diff(s!1, t!1)))") (("1" (replaces -1) (("1" (expand "Vars" 1) (("1" (inst 1 "empty_seq") (("1" (expand "subtermOF" 1 1) (("1" (rewrite "empty_0" 1) (("1" (lemma "positions_of_ext") (("1" (inst -1 "sig!1" "s!1") (("1" (decompose-equality -1) (("1" (expand "Vars" -5) (("1" (skosimp) (("1" (inst -1 "p!1") (("1" (assert) (("1" (expand "union") (("1" (prop) (("1" (expand "member") (("1" (flatten) (("1" (rewrite "subterm_ext_commute") (("1" (decompose-equality -5) (("1" (prop) (("1" (hide-all-but (-1 1)) (("1" (expand "ext") (("1" (assert) (("1" (lift-if) (("1" (prop) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but -2) (("2" (typepred "x!1") (("2" (expand "V") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "member") (("2" (skosimp) (("2" (replace -1 -8) (("2" (rewrite "pos_subterm") (("2" (rewrite "subterm_ext_commute") (("2" (expand "ext" -8) (("2" (assert) (("2" (replace -7 -8 rl) (("2" (expand "sub_of_frst_diff" -8) (("2" (lift-if) (("2" (prop) (("1" (expand "ext" -6) (("1" (replace -9 -6 rl) (("1" (expand "sub_of_frst_diff" -6) (("1" (assert) (("1" (expand "positionsOF" -6) (("1" (expand "only_empty_seq") (("1" (hide-all-but (-2 -6 1)) (("1" (replaces -2) (("1" (expand "subtermOF" -1 1) (("1" (rewrite "empty_0") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 -4 -5 -8 1 3)) (("2" (expand "ext") (("2" (replace -4 -3 rl) (("2" (expand "sub_of_frst_diff" -3) (("2" (assert) (("2" (expand "positionsOF" -3) (("2" (expand "only_empty_seq") (("2" (replaces -3) (("2" (hide -3 1) (("2" (expand "subtermOF" -1 1) (("2" (rewrite "empty_0") (("2" (hide -2) (("2" (expand "Vars") (("2" (inst 1 "p1!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-2 1)) (("2" (expand "positionsOF") (("2" (assert) (("2" (expand "only_empty_seq") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (decompose-equality 1) (("2" (iff) (("2" (prop) (("1" (expand "VRan" -1) (("1" (expand "IUnion") (("1" (skosimp) (("1" (lemma "dom_sub_of_frst_diff_is") (("1" (inst -1 "resolving_diff(s!1, t!1)" "s!1" "t!1" "sig!1") (("1" (assert) (("1" (expand* "restrict" "singleton") (("1" (decompose-equality -1) (("1" (inst -1 "i!1") (("1" (assert) (("1" (replaces -1) (("1" (replace -4 -1 rl) (("1" (expand "sub_of_frst_diff" -1) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "VRan" 1) (("2" (expand "IUnion") (("2" (inst 1 "subtermOF(s!1, resolving_diff(s!1, t!1))") (("1" (replace -4 1 rl) (("1" (expand "sub_of_frst_diff" 1) (("1" (propax) nil nil)) nil)) nil) ("2" (expand "V") (("2" (expand "Dom") (("2" (replace -4 1 rl) (("2" (expand "sub_of_frst_diff" 1) (("2" (hide-all-but -1) (("2" (lemma "resolving_diff_has_diff_argument") (("2" (inst -1 "s!1" "t!1" "resolving_diff(s!1, t!1)") (("1" (assert) nil nil) ("2" (hide -) (("2" (rewrite "position_t_resolving_diff") (("2" (lemma "position_s_resolving_diff") (("2" (inst -1 "s!1" "t!1" "resolving_diff(s!1, t!1)") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "VRan(sig!1) = Vars(subtermOF(s!1, resolving_diff(s!1, t!1)))") (("1" (replaces -1) (("1" (lemma "sub_of_frst_diff_remove_x") (("1" (inst -1 "x!1" "s!1" "t!1") (("1" (assert) (("1" (expand "member") (("1" (replace -2 1) (("1" (lemma "positions_of_ext") (("1" (inst -1 "sig!1" "s!1") (("1" (decompose-equality -1) (("1" (expand "Vars" -4) (("1" (skosimp) (("1" (inst -1 "p!1") (("1" (assert) (("1" (expand "union") (("1" (prop) (("1" (expand "member") (("1" (flatten) (("1" (rewrite "subterm_ext_commute") (("1" (decompose-equality -4) (("1" (prop) (("1" (hide-all-but (-1 1)) (("1" (grind) nil nil)) nil) ("2" (hide-all-but -2) (("2" (typepred "x!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "member") (("2" (skosimp) (("2" (replace -1 -7) (("2" (rewrite "pos_subterm") (("2" (rewrite "subterm_ext_commute") (("2" (expand "ext" -7) (("2" (assert) (("2" (case "subtermOF(s!1, p1!1) = subtermOF(t!1, resolving_diff(s!1, t!1))") (("1" (replace -7 -8 rl) (("1" (expand "sub_of_frst_diff" -8) (("1" (assert) (("1" (replace -1 -5) (("1" (replace -7 -5 rl) (("1" (expand "ext" -5) (("1" (expand "sub_of_frst_diff" -5) (("1" (hide-all-but (-5 -8 4)) (("1" (lemma "pos_o_term") (("1" (inst -1 "resolving_diff(s!1, t!1)" "p2!1" "s!1") (("1" (assert) (("1" (prop) (("1" (expand "Vars") (("1" (inst 1 "resolving_diff(s!1, t!1) o p2!1") (("1" (rewrite "pos_subterm") nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (lemma "position_s_resolving_diff") (("2" (inst -1 "s!1" "t!1" "resolving_diff(s!1, t!1)") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -6 -7 rl) (("2" (expand "sub_of_frst_diff" -7) (("2" (assert) (("2" (expand "ext" -4) (("2" (replace -6 -4 rl) (("2" (expand "sub_of_frst_diff" -4) (("2" (hide-all-but (-2 -4 -7 5)) (("2" (lemma "pos_o_term") (("2" (inst -1 "p1!1" "p2!1" "s!1") (("2" (assert) (("2" (expand "Vars") (("2" (inst 1 "p1!1 o p2!1") (("2" (rewrite "pos_subterm") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (decompose-equality 1) (("2" (iff) (("2" (prop) (("1" (expand "VRan" -1) (("1" (expand "IUnion") (("1" (skosimp) (("1" (lemma "dom_sub_of_frst_diff_is") (("1" (inst -1 "resolving_diff(s!1, t!1)" "s!1" "t!1" "sig!1") (("1" (assert) (("1" (expand* "restrict" "singleton") (("1" (decompose-equality -1) (("1" (inst -1 "i!1") (("1" (assert) (("1" (replaces -1) (("1" (replace -3 -1 rl) (("1" (expand "sub_of_frst_diff" -1) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "VRan" 1) (("2" (expand "IUnion") (("2" (inst 1 "subtermOF(t!1, resolving_diff(s!1, t!1))") (("1" (replace -3 1 rl) (("1" (expand "sub_of_frst_diff" 1) (("1" (propax) nil nil)) nil)) nil) ("2" (expand "V") (("2" (expand "Dom") (("2" (decompose-equality -3) (("2" (inst -1 "subtermOF(t!1, resolving_diff(s!1, t!1))") (("2" (expand "sub_of_frst_diff" -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (lemma "position_s_resolving_diff") (("3" (inst -1 "s!1" "t!1" "resolving_diff(s!1, t!1)") nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (rewrite "position_t_resolving_diff") (("2" (lemma "position_s_resolving_diff") (("2" (inst -1 "s!1" "t!1" "resolving_diff(s!1, t!1)") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (subset? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (union const-decl "set" sets nil) (VRan const-decl "set[(V)]" substitution nil) (IUnion const-decl "set[T]" indexed_sets nil) (dom_sub_of_frst_diff_is formula-decl nil unification nil) (p!1 skolem-const-decl "positions? [variable, symbol, arity](subtermOF(s!1, resolving_diff(s!1, t!1)))" unification nil) (position_s_resolving_diff formula-decl nil unification nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (singleton const-decl "(singleton?)" sets nil) (restrict const-decl "R" restrict nil) (NOT const-decl "[bool -> bool]" booleans nil) (Vars const-decl "set[(V)]" subterm nil) (pos_subterm formula-decl nil subterm nil) (p!1 skolem-const-decl "positions? [variable, symbol, arity](subtermOF(t!1, resolving_diff(s!1, t!1)))" unification nil) (O const-decl "finseq" finite_sequences nil) (finseq type-eq-decl nil finite_sequences nil) (t!1 skolem-const-decl "{t: term | unifiable(s!1, t) & s!1 /= t}" unification nil) (s!1 skolem-const-decl "term[variable, symbol, arity]" unification nil) (position_t_resolving_diff formula-decl nil unification nil) (pos_o_term formula-decl nil subterm nil) (Dom const-decl "set[(V)]" substitution nil) (positions type-eq-decl nil positions nil) (positionsOF def-decl "positions" positions nil) (positions? type-eq-decl nil positions nil) (subtermOF def-decl "term" subterm nil) (below type-eq-decl nil nat_types nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (position type-eq-decl nil positions nil) (resolving_diff def-decl "position" unification nil) (resolving_diff_vars formula-decl nil unification nil) (resolving_diff_has_diff_argument formula-decl nil unification nil) (sig!1 skolem-const-decl "Sub[variable, symbol, arity]" unification nil) (positions_of_ext formula-decl nil substitution nil) (vars? adt-recognizer-decl "[term -> boolean]" term_adt nil) (ext def-decl "term" substitution nil) (args adt-accessor-decl "[d: (app?) -> {args: finite_sequence[term] | args`length = arity(f(d))}]" term_adt nil) (finite_sequence type-eq-decl nil finite_sequences nil) (f adt-accessor-decl "[(app?) -> symbol]" term_adt nil) (app? adt-recognizer-decl "[term -> boolean]" term_adt nil) (v adt-accessor-decl "[(vars?) -> variable]" term_adt nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (subterm_ext_commute formula-decl nil substitution nil) (sub_of_frst_diff_remove_x formula-decl nil unification nil) (p2!1 skolem-const-decl "position[variable, symbol, arity]" unification nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (only_empty_seq const-decl "positions" positions nil) (empty_0 formula-decl nil seq_extras "structures/") (empty_seq const-decl "finseq" finite_sequences nil) (sub_of_frst_diff const-decl "Sub" unification nil) (Sub type-eq-decl nil substitution nil) (Sub? const-decl "bool" substitution nil) (/= const-decl "boolean" notequal nil) (unifiable const-decl "bool" unification nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (V const-decl "set[term]" variables_term nil) (set type-eq-decl nil sets nil) (term type-decl nil term_adt nil) (arity formal-const-decl "[symbol -> nat]" unification nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (symbol formal-nonempty-type-decl nil unification nil) (variable formal-nonempty-type-decl nil unification nil)) shostak)) (vars_sub_of_frst_diff_t_is_subset_union 0 (vars_sub_of_frst_diff_t_is_subset_union-1 nil 3457877610 ("" (skosimp) (("" (assert) (("" (name-replace "sig!1" "sub_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_sub_of_frst_diff_is") (("1" (inst -1 "resolving_diff(s!1, t!1)" "s!1" "t!1" "sig!1") (("1" (assert) (("1" (prop) (("1" (expand* "restrict" "singleton") (("1" (decompose-equality -2) (("1" (inst -1 "i!1") (("1" (assert) (("1" (replaces -1) (("1" (replace -3 -2 rl) (("1" (expand "sub_of_frst_diff" -2) (("1" (hide-all-but (-2 2)) (("1" (expand "Vars") (("1" (skosimp) (("1" (typepred "p!1") (("1" (lemma "pos_o_term") (("1" (inst -1 "resolving_diff(s!1, t!1)" "p!1" "t!1") (("1" (assert) (("1" (prop) (("1" (inst 1 "resolving_diff(s!1, t!1) o p!1") (("1" (rewrite "pos_subterm") nil nil)) nil) ("2" (hide-all-but 1) (("2" (rewrite "position_t_resolving_diff") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand* "restrict" "singleton") (("2" (decompose-equality -1) (("1" (inst -1 "i!1") (("1" (assert) (("1" (replaces -1) (("1" (replace -2 -1 rl) (("1" (expand "sub_of_frst_diff" -1) (("1" (hide-all-but (-1 2)) (("1" (expand "Vars") (("1" (skosimp) (("1" (lemma "pos_o_term") (("1" (inst -1 "resolving_diff(s!1, t!1)" "p!1" "s!1") (("1" (assert) (("1" (prop) (("1" (inst 1 "resolving_diff(s!1, t!1) o p!1") (("1" (rewrite "pos_subterm") nil nil)) nil) ("2" (hide-all-but 1) (("2" (lemma "position_s_resolving_diff") (("2" (inst -1 "s!1" "t!1" "resolving_diff(s!1, t!1)") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (rewrite "position_t_resolving_diff") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "member") (("2" (lemma "resolving_diff_vars") (("2" (inst -1 "s!1" "t!1" "resolving_diff(s!1, t!1)") (("1" (split) (("1" (case "VRan(sig!1) = Vars(subtermOF(t!1, resolving_diff(s!1, t!1)))") (("1" (replaces -1) (("1" (lemma "sub_of_frst_diff_remove_x") (("1" (inst -1 "x!1" "s!1" "t!1") (("1" (assert) (("1" (replace -3 -1) (("1" (expand "member") (("1" (lemma "positions_of_ext") (("1" (inst -1 "sig!1" "t!1") (("1" (decompose-equality -1) (("1" (expand "Vars" -4) (("1" (skosimp) (("1" (inst -1 "p!1") (("1" (assert) (("1" (expand "union") (("1" (prop) (("1" (expand "member") (("1" (flatten) (("1" (rewrite "subterm_ext_commute") (("1" (decompose-equality -4) (("1" (prop) (("1" (hide-all-but (-1 1)) (("1" (grind) nil nil)) nil) ("2" (hide-all-but -2) (("2" (typepred "x!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "member") (("2" (skosimp) (("2" (replace -1 -7) (("2" (rewrite "pos_subterm") (("2" (rewrite "subterm_ext_commute") (("2" (expand "ext" -7) (("2" (assert) (("2" (case "subtermOF(t!1, p1!1) = subtermOF(s!1, resolving_diff(s!1, t!1))") (("1" (replace -7 -8 rl) (("1" (expand "sub_of_frst_diff" -8) (("1" (assert) (("1" (expand "Vars" 2) (("1" (inst 2 "p2!1") nil nil)) nil)) nil)) nil)) nil) ("2" (replace -6 -7 rl) (("2" (expand "sub_of_frst_diff" -7) (("2" (assert) (("2" (replace -6 -4 rl) (("2" (expand "ext" -4) (("2" (expand "sub_of_frst_diff" -4) (("2" (lemma "pos_o_term") (("2" (inst -1 "p1!1" "p2!1" "t!1") (("2" (assert) (("2" (lemma "pos_subterm") (("2" (inst -1 "p1!1" "p2!1" "t!1") (("2" (assert) (("2" (replace -1 -9 rl) (("2" (hide-all-but (-9 5)) (("2" (expand "Vars") (("2" (inst 1 "p1!1 o p2!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (decompose-equality 1) (("2" (iff) (("2" (prop) (("1" (expand "VRan" -1) (("1" (expand "IUnion") (("1" (skosimp) (("1" (lemma "dom_sub_of_frst_diff_is") (("1" (inst -1 "resolving_diff(s!1, t!1)" "s!1" "t!1" "sig!1") (("1" (assert) (("1" (expand* "restrict" "singleton") (("1" (decompose-equality -1) (("1" (inst -1 "i!1") (("1" (assert) (("1" (replaces -1) (("1" (replace -3 -1 rl) (("1" (expand "sub_of_frst_diff" -1) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "VRan" 1) (("2" (expand "IUnion") (("2" (inst 1 "subtermOF(s!1, resolving_diff(s!1, t!1))") (("1" (replace -3 1 rl) (("1" (expand "sub_of_frst_diff" 1) (("1" (propax) nil nil)) nil)) nil) ("2" (expand "V") (("2" (hide -1 -4 2 3 4) (("2" (expand "Dom") (("2" (replace -2 1 rl) (("2" (expand "sub_of_frst_diff" 1) (("2" (lemma "resolving_diff_has_diff_argument") (("2" (inst -1 "s!1" "t!1" "resolving_diff(s!1, t!1)") (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (rewrite "position_t_resolving_diff") (("2" (lemma "position_s_resolving_diff") (("2" (inst -1 "s!1" "t!1" "resolving_diff(s!1, t!1)") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (rewrite "position_t_resolving_diff") nil nil)) nil)) nil) ("2" (case "vars?(subtermOF(s!1, resolving_diff(s!1, t!1)))") (("1" (case "VRan(sig!1) = Vars(subtermOF(t!1, resolving_diff(s!1, t!1)))") (("1" (replaces -1) (("1" (expand "Vars" 1) (("1" (inst 1 "empty_seq") (("1" (expand "subtermOF" 1 1) (("1" (rewrite "empty_0" 1) (("1" (lemma "positions_of_ext") (("1" (inst -1 "sig!1" "t!1") (("1" (decompose-equality -1) (("1" (expand "Vars" -5) (("1" (skosimp) (("1" (inst -1 "p!1") (("1" (assert) (("1" (expand "union") (("1" (prop) (("1" (expand "member") (("1" (flatten) (("1" (rewrite "subterm_ext_commute") (("1" (decompose-equality -5) (("1" (prop) (("1" (hide-all-but (-1 1)) (("1" (grind) nil nil)) nil) ("2" (hide-all-but -2) (("2" (typepred "x!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "member") (("2" (skosimp) (("2" (replace -1 -8) (("2" (rewrite "pos_subterm") (("2" (rewrite "subterm_ext_commute") (("2" (expand "ext" -8) (("2" (assert) (("2" (replace -7 -8 rl) (("2" (expand "sub_of_frst_diff" -8) (("2" (lift-if) (("2" (prop) (("1" (expand "ext" -6) (("1" (replace -9 -6 rl) (("1" (expand "sub_of_frst_diff" -6) (("1" (assert) (("1" (expand "positionsOF" -6) (("1" (expand "only_empty_seq") (("1" (hide-all-but (-2 -6 1)) (("1" (replaces -2) (("1" (expand "subtermOF" -1 1) (("1" (rewrite "empty_0") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 -4 -5 -8 1 4)) (("2" (expand "ext") (("2" (replace -4 -3 rl) (("2" (expand "sub_of_frst_diff" -3) (("2" (assert) (("2" (expand "positionsOF" -3) (("2" (expand "only_empty_seq") (("2" (replaces -3) (("2" (hide -3 1) (("2" (expand "subtermOF" -1 1) (("2" (rewrite "empty_0") (("2" (hide -2) (("2" (expand "Vars") (("2" (inst 1 "p1!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-2 1)) (("2" (expand "positionsOF") (("2" (assert) (("2" (expand "only_empty_seq") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (decompose-equality 1) (("2" (iff) (("2" (prop) (("1" (expand "VRan" -1) (("1" (expand "IUnion") (("1" (skosimp) (("1" (lemma "dom_sub_of_frst_diff_is") (("1" (inst -1 "resolving_diff(s!1, t!1)" "s!1" "t!1" "sig!1") (("1" (assert) (("1" (expand* "restrict" "singleton") (("1" (decompose-equality -1) (("1" (inst -1 "i!1") (("1" (assert) (("1" (replaces -1) (("1" (replace -4 -1 rl) (("1" (expand "sub_of_frst_diff" -1) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "VRan" 1) (("2" (expand "IUnion") (("2" (inst 1 "subtermOF(s!1, resolving_diff(s!1, t!1))") (("1" (replace -4 1 rl) (("1" (expand "sub_of_frst_diff" 1) (("1" (propax) nil nil)) nil)) nil) ("2" (expand "V") (("2" (expand "Dom") (("2" (replace -4 1 rl) (("2" (expand "sub_of_frst_diff" 1) (("2" (hide-all-but -1) (("2" (lemma "resolving_diff_has_diff_argument") (("2" (inst -1 "s!1" "t!1" "resolving_diff(s!1, t!1)") (("1" (assert) nil nil) ("2" (hide -) (("2" (rewrite "position_t_resolving_diff") (("2" (lemma "position_s_resolving_diff") (("2" (inst -1 "s!1" "t!1" "resolving_diff(s!1, t!1)") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "VRan(sig!1) = Vars(subtermOF(s!1, resolving_diff(s!1, t!1)))") (("1" (replaces -1) (("1" (lemma "sub_of_frst_diff_remove_x") (("1" (inst -1 "x!1" "s!1" "t!1") (("1" (assert) (("1" (expand "member") (("1" (replace -2 1) (("1" (lemma "positions_of_ext") (("1" (inst -1 "sig!1" "t!1") (("1" (decompose-equality -1) (("1" (expand "Vars" -4) (("1" (skosimp) (("1" (inst -1 "p!1") (("1" (assert) (("1" (expand "union") (("1" (prop) (("1" (expand "member") (("1" (flatten) (("1" (rewrite "subterm_ext_commute") (("1" (decompose-equality -4) (("1" (prop) (("1" (hide-all-but (-1 1)) (("1" (grind) nil nil)) nil) ("2" (hide-all-but -2) (("2" (typepred "x!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "member") (("2" (skosimp) (("2" (replace -1 -7) (("2" (rewrite "pos_subterm") (("2" (rewrite "subterm_ext_commute") (("2" (expand "ext" -7) (("2" (assert) (("2" (case "subtermOF(t!1, p1!1) = subtermOF(t!1, resolving_diff(s!1, t!1))") (("1" (replace -7 -8 rl) (("1" (expand "sub_of_frst_diff" -8) (("1" (assert) (("1" (replace -1 -5) (("1" (replace -7 -5 rl) (("1" (expand "ext" -5) (("1" (expand "sub_of_frst_diff" -5) (("1" (hide-all-but (-5 -8 4)) (("1" (lemma "pos_o_term") (("1" (inst -1 "resolving_diff(s!1, t!1)" "p2!1" "s!1") (("1" (assert) (("1" (prop) (("1" (expand "Vars") (("1" (inst 1 "resolving_diff(s!1, t!1) o p2!1") (("1" (rewrite "pos_subterm") nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (lemma "position_s_resolving_diff") (("2" (inst -1 "s!1" "t!1" "resolving_diff(s!1, t!1)") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -6 -7 rl) (("2" (expand "sub_of_frst_diff" -7) (("2" (assert) (("2" (expand "ext" -4) (("2" (replace -6 -4 rl) (("2" (expand "sub_of_frst_diff" -4) (("2" (hide-all-but (-2 -4 -7 6)) (("2" (lemma "pos_o_term") (("2" (inst -1 "p1!1" "p2!1" "t!1") (("2" (assert) (("2" (expand "Vars") (("2" (inst 1 "p1!1 o p2!1") (("2" (rewrite "pos_subterm") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (decompose-equality 1) (("2" (iff) (("2" (prop) (("1" (expand "VRan" -1) (("1" (expand "IUnion") (("1" (skosimp) (("1" (lemma "dom_sub_of_frst_diff_is") (("1" (inst -1 "resolving_diff(s!1, t!1)" "s!1" "t!1" "sig!1") (("1" (assert) (("1" (expand* "restrict" "singleton") (("1" (decompose-equality -1) (("1" (inst -1 "i!1") (("1" (assert) (("1" (replaces -1) (("1" (replace -3 -1 rl) (("1" (expand "sub_of_frst_diff" -1) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "VRan" 1) (("2" (expand "IUnion") (("2" (inst 1 "subtermOF(t!1, resolving_diff(s!1, t!1))") (("1" (replace -3 1 rl) (("1" (expand "sub_of_frst_diff" 1) (("1" (propax) nil nil)) nil)) nil) ("2" (expand "V") (("2" (expand "Dom") (("2" (decompose-equality -3) (("2" (inst -1 "subtermOF(t!1, resolving_diff(s!1, t!1))") (("2" (expand "sub_of_frst_diff" -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (lemma "position_s_resolving_diff") (("3" (inst -1 "s!1" "t!1" "resolving_diff(s!1, t!1)") nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (rewrite "position_t_resolving_diff") (("2" (lemma "position_s_resolving_diff") (("2" (inst -1 "s!1" "t!1" "resolving_diff(s!1, t!1)") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) --> -------------------- --> maximum size reached --> --------------------
¤ 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.0.919Bemerkung: (vorverarbeitet am 2026-04-28) ¤*Bot Zugriff |
|
||||||||||||||
2026-05-26