orphaned-proofs.prf

("first_order_substitution" |first_order_substitution| |nice_more_general_is_more_general| 0 (|nice_more_general_is_more_general-1| NIL 3941189896 ("" (GRIND) NIL NIL) ((|nice?| DEF-DECL "bool" |first_order_substitution| NIL) (|sub| TYPE-EQ-DECL NIL |first_order_substitution| NIL) (|list| TYPE-DECL NIL |list_adt| NIL) (|basic_sub| TYPE-EQ-DECL NIL |first_order_substitution| NIL) (|constant| TYPE-EQ-DECL NIL |first_order_terms_properties| NIL) (TRUE CONST-DECL "bool" |booleans| NIL) (AND CONST-DECL "[bool, bool -> bool]" |booleans| NIL) NIL (PRED TYPE-EQ-DECL NIL |defined_types| NIL) (|first_order_term| TYPE-DECL NIL |first_order_term_adt| NIL) (|f_symbol| TYPE-EQ-DECL NIL |first_order_terms_properties| NIL) (|char| TYPE-EQ-DECL NIL |strings| NIL) (|char?| ADT-RECOGNIZER-DECL "[character -> boolean]" |character_adt| NIL) (|character| TYPE-DECL NIL |character_adt| NIL) (|below| TYPE-EQ-DECL NIL |nat_types| NIL) (|nat| NONEMPTY-TYPE-EQ-DECL NIL |naturalnumbers| NIL) (|variable| TYPE-EQ-DECL NIL |first_order_terms_properties| 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) (NOT CONST-DECL "[bool -> bool]" |booleans| NIL) (|bool| NONEMPTY-TYPE-EQ-DECL NIL |booleans| NIL) (|boolean| NONEMPTY-TYPE-DECL NIL |booleans| NIL) (|subs| CONST-DECL "first_order_term" |first_order_substitution| NIL) NIL NIL NIL) SHOSTAK))("first_order_substitution" |first_order_substitution| |nice_more_general_is_more_general_set_vars| 0 (|nice_more_general_is_more_general_set_vars-1| NIL 3941190631 ("" (GRIND) NIL NIL) ((|boolean| NONEMPTY-TYPE-DECL NIL |booleans| NIL) (|bool| NONEMPTY-TYPE-EQ-DECL NIL |booleans| NIL) (NOT CONST-DECL "[bool -> bool]" |booleans| NIL) (|number| NONEMPTY-TYPE-DECL NIL |numbers| NIL) (|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) (|variable| TYPE-EQ-DECL NIL |first_order_terms_properties| NIL) (|set| TYPE-EQ-DECL NIL |sets| NIL) (|is_finite| CONST-DECL "bool" |finite_sets| NIL) (|finite_set| TYPE-EQ-DECL NIL |finite_sets| NIL) (|injective?| CONST-DECL "bool" |functions| NIL) (|nice?| DEF-DECL "bool" |first_order_substitution| NIL) (|sub| TYPE-EQ-DECL NIL |first_order_substitution| NIL) (|list| TYPE-DECL NIL |list_adt| NIL) (|basic_sub| TYPE-EQ-DECL NIL |first_order_substitution| NIL) (|constant| TYPE-EQ-DECL NIL |first_order_terms_properties| NIL) (TRUE CONST-DECL "bool" |booleans| NIL) (AND CONST-DECL "[bool, bool -> bool]" |booleans| NIL) (|every| ADT-DEF-DECL "boolean" |first_order_term_adt| NIL) (PRED TYPE-EQ-DECL NIL |defined_types| NIL) (|first_order_term| TYPE-DECL NIL |first_order_term_adt| NIL) (|f_symbol| TYPE-EQ-DECL NIL |first_order_terms_properties| NIL) (|char| TYPE-EQ-DECL NIL |strings| NIL) (|char?| ADT-RECOGNIZER-DECL "[character -> boolean]" |character_adt| NIL) (|character| TYPE-DECL NIL |character_adt| NIL) (|below| TYPE-EQ-DECL NIL |nat_types| NIL) (|nat| NONEMPTY-TYPE-EQ-DECL NIL |naturalnumbers| NIL) (|member| CONST-DECL "bool" |sets| NIL) (|subs| CONST-DECL "first_order_term" |first_order_substitution| NIL) (|equal?| CONST-DECL "bool" |first_order_substitution| NIL) (|nice_more_general?| CONST-DECL "bool" |first_order_substitution| NIL) (|more_general?| CONST-DECL "bool" |first_order_substitution| NIL)) SHOSTAK))("first_order_substitution" |first_order_substitution| |inv_renaming_TCC1| 0 (|inv_renaming_TCC1-1| NIL 3940933173 ("" (WELL-FOUNDED-TCC) NIL NIL) NIL NIL (|inv_renaming| WELL-FOUNDED "restrict[[list_adt[basic_sub].list, list_adt[basic_sub].list], [renaming, renaming], bool].restrict(list_adt[basic_sub].<<)" "NIL")))("first_order_substitution" |first_order_substitution| |inv_renaming_TCC2| 0 (|inv_renaming_TCC2-1| NIL 3940933173 ("" (SUBTYPE-TCC) NIL NIL) ((|renaming?| CONST-DECL "bool" |first_order_substitution| NIL) (|img| CONST-DECL "finite_set[first_order_term[constant, variable, f_symbol]]" |first_order_substitution| NIL) (|member| CONST-DECL "bool" |sets| NIL) (|dom| CONST-DECL "finite_set[variable]" |first_order_substitution| NIL) (|subs| CONST-DECL "first_order_term" |first_order_substitution| NIL)) NIL (|inv_renaming| SUBTYPE "list_adt[basic_sub].null" "renaming")))("first_order_substitution" |first_order_substitution| |inv_renaming_TCC3| 0 (|inv_renaming_TCC3-1| NIL 3940933173 ("" (SUBTYPE-TCC) NIL NIL) ((|subs| CONST-DECL "first_order_term" |first_order_substitution| NIL) (|dom| CONST-DECL "finite_set[variable]" |first_order_substitution| NIL) (|member| CONST-DECL "bool" |sets| NIL) (|img| CONST-DECL "finite_set[first_order_term[constant, variable, f_symbol]]" |first_order_substitution| NIL) (|renaming| TYPE-EQ-DECL NIL |first_order_substitution| NIL) (|renaming?| CONST-DECL "bool" |first_order_substitution| NIL) (|sub| TYPE-EQ-DECL NIL |first_order_substitution| NIL) (|list| TYPE-DECL NIL |list_adt| NIL) (|basic_sub| TYPE-EQ-DECL NIL |first_order_substitution| NIL) (|constant| TYPE-EQ-DECL NIL |first_order_terms_properties| NIL) (TRUE CONST-DECL "bool" |booleans| NIL) (AND CONST-DECL "[bool, bool -> bool]" |booleans| NIL) (PRED TYPE-EQ-DECL NIL |defined_types| NIL) (|first_order_term| TYPE-DECL NIL |first_order_term_adt| NIL) (|f_symbol| TYPE-EQ-DECL NIL |first_order_terms_properties| NIL) (|char| TYPE-EQ-DECL NIL |strings| NIL) (|char?| ADT-RECOGNIZER-DECL "[character -> boolean]" |character_adt| NIL) (|character| TYPE-DECL NIL |character_adt| NIL) (|below| TYPE-EQ-DECL NIL |nat_types| NIL) (|nat| NONEMPTY-TYPE-EQ-DECL NIL |naturalnumbers| NIL) (|variable| TYPE-EQ-DECL NIL |first_order_terms_properties| 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) (NOT CONST-DECL "[bool -> bool]" |booleans| NIL) (|bool| NONEMPTY-TYPE-EQ-DECL NIL |booleans| NIL) (|boolean| NONEMPTY-TYPE-DECL NIL |booleans| NIL)) NIL (|inv_renaming| SUBTYPE "first_order_substitution.gamma" "(list_adt[basic_sub].cons?)")))("first_order_substitution" |first_order_substitution| |inv_renaming_TCC4| 0 (|inv_renaming_TCC4-1| NIL 3940933173 ("" (SUBTYPE-TCC) NIL NIL) NIL NIL (|inv_renaming| SUBTYPE "list_adt[basic_sub].car(first_order_substitution.gamma)`2" "(first_order_term_adt[constant, variable, f_symbol].var?)")))("first_order_substitution" |first_order_substitution| |inv_renaming_TCC5| 0 (|inv_renaming_TCC5-1| NIL 3940933173 ("" (SUBTYPE-TCC) NIL NIL) NIL NIL (|inv_renaming| SUBTYPE "list_adt[basic_sub].cdr(first_order_substitution.gamma)" "renaming")))("first_order_substitution" |first_order_substitution| |inv_renaming_TCC6| 0 (|inv_renaming_TCC6-1| NIL 3940933173 ("" (TERMINATION-TCC) NIL NIL) ((|restrict| CONST-DECL "R" |restrict| NIL) (|subs| CONST-DECL "first_order_term" |first_order_substitution| NIL) (|dom| CONST-DECL "finite_set[variable]" |first_order_substitution| NIL) (|member| CONST-DECL "bool" |sets| NIL) (|img| CONST-DECL "finite_set[first_order_term[constant, variable, f_symbol]]" |first_order_substitution| NIL) (<< ADT-DEF-DECL "(strict_well_founded?[list])" |list_adt| NIL) (|renaming| TYPE-EQ-DECL NIL |first_order_substitution| NIL) (|renaming?| CONST-DECL "bool" |first_order_substitution| NIL) (|sub| TYPE-EQ-DECL NIL |first_order_substitution| NIL) (|list| TYPE-DECL NIL |list_adt| NIL) (|basic_sub| TYPE-EQ-DECL NIL |first_order_substitution| NIL) (|constant| TYPE-EQ-DECL NIL |first_order_terms_properties| NIL) (TRUE CONST-DECL "bool" |booleans| NIL) (AND CONST-DECL "[bool, bool -> bool]" |booleans| NIL) (PRED TYPE-EQ-DECL NIL |defined_types| NIL) (|first_order_term| TYPE-DECL NIL |first_order_term_adt| NIL) (|f_symbol| TYPE-EQ-DECL NIL |first_order_terms_properties| NIL) (|char| TYPE-EQ-DECL NIL |strings| NIL) (|char?| ADT-RECOGNIZER-DECL "[character -> boolean]" |character_adt| NIL) (|character| TYPE-DECL NIL |character_adt| NIL) (|below| TYPE-EQ-DECL NIL |nat_types| NIL) (|nat| NONEMPTY-TYPE-EQ-DECL NIL |naturalnumbers| NIL) (|variable| TYPE-EQ-DECL NIL |first_order_terms_properties| 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) (NOT CONST-DECL "[bool -> bool]" |booleans| NIL) (|bool| NONEMPTY-TYPE-EQ-DECL NIL |booleans| NIL) (|boolean| NONEMPTY-TYPE-DECL NIL |booleans| NIL)) NIL (|inv_renaming| TERMINATION "first_order_substitution.inv_renaming(list_adt[basic_sub].cdr(first_order_substitution.gamma))" "NIL")))("first_order_substitution" |first_order_substitution| |inv_renaming_TCC7| 0 (|inv_renaming_TCC7-1| NIL 3940933173 ("" (SUBTYPE-TCC) NIL NIL) NIL NIL (|inv_renaming| SUBTYPE "list_adt[[variable, first_order_term[constant, variable, f_symbol]]].cons((first_order_term_adt[constant, variable, f_symbol].V(list_adt[basic_sub].car(first_order_substitution.gamma)`2), first_order_term_adt[constant, variable, f_symbol].variable(list_adt[basic_sub].car(first_order_substitution.gamma)`1)), first_order_substitution.inv_renaming(list_adt[basic_sub].cdr(first_order_substitution.gamma)))" "renaming")))("first_order_substitution" |first_order_substitution| |disj_var_renaming_TCC1| 0 (|disj_var_renaming_TCC1-1| NIL 3940933173 ("" (SUBTYPE-TCC) NIL NIL) ((|renaming?| CONST-DECL "bool" |first_order_substitution| NIL) (|img| CONST-DECL "finite_set[first_order_term[constant, variable, f_symbol]]" |first_order_substitution| NIL) (|dom| CONST-DECL "finite_set[variable]" |first_order_substitution| NIL) (|subs| CONST-DECL "first_order_term" |first_order_substitution| NIL) (|empty?| CONST-DECL "bool" |sets| NIL) (|member| CONST-DECL "bool" |sets| NIL)) NIL (|disj_var_renaming| SUBTYPE "list_adt[basic_sub].null" "renaming")))("first_order_substitution" |first_order_substitution| |disj_var_renaming_TCC2| 0 (|disj_var_renaming_TCC2-1| NIL 3940933173 ("" (TERMINATION-TCC) NIL NIL) NIL NIL (|disj_var_renaming| TERMINATION "first_order_substitution.disj_var_renaming(sets[variable].rest(first_order_substitution.V), sets[variable].add(first_order_substitution.X, sets[variable].add(first_order_substitution.Y, first_order_substitution.DV)))" "NIL")))("first_order_substitution" |first_order_substitution| |disj_var_renaming_TCC3| 0 (|disj_var_renaming_TCC3-1| NIL 3940933173 ("" (SUBTYPE-TCC) NIL NIL) NIL NIL (|disj_var_renaming| SUBTYPE "list_adt[[variable, first_order_term[constant, variable, f_symbol]]].cons((first_order_substitution.X, first_order_term_adt[constant, variable, f_symbol].variable(first_order_substitution.Y)), first_order_substitution.disj_var_renaming(sets[variable].rest(first_order_substitution.V), sets[variable].add(first_order_substitution.X, sets[variable].add(first_order_substitution.Y, first_order_substitution.DV))))" "renaming")))("first_order_substitution" |first_order_substitution| |disj_var_renaming_TCC4| 0 (|disj_var_renaming_TCC4-1| NIL 3940933173 ("" (SUBTYPE-TCC) NIL NIL) ((|nonempty?| CONST-DECL "bool" |sets| NIL) (|empty?| CONST-DECL "bool" |sets| NIL) (|member| CONST-DECL "bool" |sets| NIL) (|finite_set| TYPE-EQ-DECL NIL |finite_sets| NIL) (|is_finite| CONST-DECL "bool" |finite_sets| NIL) (|set| TYPE-EQ-DECL NIL |sets| NIL) (|variable| TYPE-EQ-DECL NIL |first_order_terms_properties| 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) (NOT CONST-DECL "[bool -> bool]" |booleans| NIL) (|bool| NONEMPTY-TYPE-EQ-DECL NIL |booleans| NIL) (|boolean| NONEMPTY-TYPE-DECL NIL |booleans| NIL)) NIL (|disj_var_renaming| SUBTYPE "first_order_substitution.V" "(sets[variable].nonempty?)")))("first_order_substitution" |first_order_substitution| |disj_var_renaming_disj_dom_img| 0 (|disj_var_renaming_disj_dom_img-1| NIL 3941103840 ("" (LEMMA "disj_var_renaming_correct") (("" (SKEEP) (("" (INST?) (("" (FLATTEN) (("" (HIDE -1) (("" (EXPAND "disjoint?") (("" (EXPAND "empty?") (("" (EXPAND "union") (("" (SKEEP) (("" (INST?) (("" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ((|finite_intersection1| APPLICATION-JUDGEMENT "finite_set" |finite_sets| NIL) (|disjoint?| CONST-DECL "bool" |sets| NIL) (|union| CONST-DECL "set" |sets| NIL) (|member| CONST-DECL "bool" |sets| NIL) (|subs| CONST-DECL "first_order_term" |first_order_substitution| NIL) (|dom| CONST-DECL "finite_set[variable]" |first_order_substitution| NIL) (|img| CONST-DECL "finite_set[first_order_term[constant, variable, f_symbol]]" |first_order_substitution| NIL) (|intersection| CONST-DECL "set" |sets| NIL) (|empty?| CONST-DECL "bool" |sets| NIL) (|finite_set| TYPE-EQ-DECL NIL |finite_sets| NIL) (|is_finite| CONST-DECL "bool" |finite_sets| NIL) (|set| TYPE-EQ-DECL NIL |sets| NIL) (|variable| TYPE-EQ-DECL NIL |first_order_terms_properties| 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) (|disj_var_renaming_correct| FORMULA-DECL NIL |first_order_substitution| NIL)) SHOSTAK))("first_order_substitution" |first_order_substitution| |disj_var_renaming_disj_dom_img2| 0 (|disj_var_renaming_disj_dom_img2-1| NIL 3941103949 ("" (LEMMA "disj_var_renaming_correct") (("" (SKEEP) (("" (INST?) (("" (FLATTEN) (("" (HIDE -1) (("" (EXPAND "disjoint?") (("" (EXPAND "empty?") (("" (SKEEP) (("" (INST?) (("" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ((|finite_intersection1| APPLICATION-JUDGEMENT "finite_set" |finite_sets| NIL) (|disjoint?| CONST-DECL "bool" |sets| NIL) (|finite_union| APPLICATION-JUDGEMENT "finite_set" |finite_sets| NIL) (|intersection| CONST-DECL "set" |sets| NIL) (|union| CONST-DECL "set" |sets| NIL) (|img| CONST-DECL "finite_set[first_order_term[constant, variable, f_symbol]]" |first_order_substitution| NIL) (|dom| CONST-DECL "finite_set[variable]" |first_order_substitution| NIL) (|subs| CONST-DECL "first_order_term" |first_order_substitution| NIL) (|member| CONST-DECL "bool" |sets| NIL) (|empty?| CONST-DECL "bool" |sets| NIL) (|finite_set| TYPE-EQ-DECL NIL |finite_sets| NIL) (|is_finite| CONST-DECL "bool" |finite_sets| NIL) (|set| TYPE-EQ-DECL NIL |sets| NIL) (|variable| TYPE-EQ-DECL NIL |first_order_terms_properties| 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) (|disj_var_renaming_correct| FORMULA-DECL NIL |first_order_substitution| NIL)) SHOSTAK))("first_order_substitution" |first_order_substitution| |r_nice_subs_TCC1| 0 (|r_nice_subs_TCC1-1| NIL 3940952571 ("" (SUBTYPE-TCC) NIL NIL) NIL NIL (|r_nice_subs| SUBTYPE "first_order_substitution.SV" "(sets[variable].nonempty?)")))("first_order_substitution" |first_order_substitution| |r_nice_subs_TCC2| 0 (|r_nice_subs_TCC2-1| NIL 3940952571 ("" (SUBTYPE-TCC) NIL NIL) NIL NIL (|r_nice_subs| SUBTYPE "sets[variable].rest(first_order_substitution.SV)" "{SV: finite_sets[variable].finite_set | sets[variable].subset?(SV, first_order_substitution.dom(first_order_substitution.sigma))}")))("first_order_substitution" |first_order_substitution| |r_nice_subs_TCC3| 0 (|r_nice_subs_TCC3-1| NIL 3940952571 ("" (TERMINATION-TCC) NIL NIL) NIL NIL (|r_nice_subs| TERMINATION "first_order_substitution.r_nice_subs(first_order_substitution.sigma)(sets[variable].rest(first_order_substitution.SV))" "NIL")))("first_order_substitution" |first_order_substitution| |r_nice_supset_dom| 0 (|r_nice_supset_dom-1| NIL 3941026310 ("" (MEASURE-INDUCT+ "card(SV)" ("SV")) (("" (SKEEP) (("" (CASE "empty?(x!1)") (("1" (HIDE -2 -3) (("1" (EXPAND "r_nice_subs") (("1" (ASSERT) (("1" (REWRITE "emptyset_is_empty?") (("1" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (EXPAND "r_nice_subs" 2) (("2" (ASSERT) (("2" (INST -1 "rest[variable](x!1)") (("2" (INST?) (("2" (REWRITE "card_rest") (("2" (ASSERT) (("2" (PROP) (("1" (EXPAND "supset_dom" 2) (("1" (REPLACES -1) (("1" (HIDE -1) (("1" (LEMMA "choose_rest[variable]") (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE 3) (("2" (LEMMA "rest_subset[variable]") (("2" (INST?) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ((|rest| CONST-DECL "set" |sets| NIL) (|card_rest| FORMULA-DECL NIL |finite_sets| NIL) (|int_minus_int_is_int| APPLICATION-JUDGEMENT "int" |integers| NIL) (|choose_rest| FORMULA-DECL NIL |sets_lemmas| NIL) (|nonempty_add_finite| APPLICATION-JUDGEMENT "non_empty_finite_set" |finite_sets| NIL) (|rest_subset| FORMULA-DECL NIL |sets_lemmas| NIL) (|nonempty?| CONST-DECL "bool" |sets| NIL) (|finite_remove| APPLICATION-JUDGEMENT "finite_set" |finite_sets| NIL) (|subs| CONST-DECL "first_order_term" |first_order_substitution| NIL) (|remove| CONST-DECL "set" |sets| NIL) (|member| CONST-DECL "bool" |sets| NIL) (/= CONST-DECL "boolean" |notequal| NIL) (NOT CONST-DECL "[bool -> bool]" |booleans| NIL) (|real_ge_is_total_order| NAME-JUDGEMENT "(total_order?[real])" |real_props| NIL) (|choose| CONST-DECL "(p)" |sets| NIL) (|real_lt_is_strict_total_order| NAME-JUDGEMENT "(strict_total_order?[real])" |real_props| NIL) (|finite_rest| APPLICATION-JUDGEMENT "finite_set" |finite_sets| NIL) (|subset_is_partial_order| NAME-JUDGEMENT "(partial_order?[set[T]])" |sets_lemmas| NIL) (|finite_emptyset| NAME-JUDGEMENT "finite_set" |finite_sets| NIL) (|emptyset_is_empty?| FORMULA-DECL NIL |sets_lemmas| NIL) (|empty?| CONST-DECL "bool" |sets| NIL) (|r_nice_subs| DEF-DECL "sub" |first_order_substitution| NIL) (|supset_dom| DEF-DECL "finite_set[variable]" |first_order_substitution| NIL) (|dom| CONST-DECL "finite_set[variable]" |first_order_substitution| NIL) (|subset?| CONST-DECL "bool" |sets| NIL) (IMPLIES CONST-DECL "[bool, bool -> bool]" |booleans| NIL) (|nice?| DEF-DECL "bool" |first_order_substitution| NIL) (|sub| TYPE-EQ-DECL NIL |first_order_substitution| NIL) (|list| TYPE-DECL NIL |list_adt| NIL) (|basic_sub| TYPE-EQ-DECL NIL |first_order_substitution| NIL) (|constant| TYPE-EQ-DECL NIL |first_order_terms_properties| NIL) (TRUE CONST-DECL "bool" |booleans| NIL) (AND CONST-DECL "[bool, bool -> bool]" |booleans| NIL) (PRED TYPE-EQ-DECL NIL |defined_types| NIL) (|first_order_term| TYPE-DECL NIL |first_order_term_adt| NIL) (|f_symbol| TYPE-EQ-DECL NIL |first_order_terms_properties| NIL) (|char| TYPE-EQ-DECL NIL |strings| NIL) (|char?| ADT-RECOGNIZER-DECL "[character -> boolean]" |character_adt| NIL) (|character| TYPE-DECL NIL |character_adt| NIL) (|below| TYPE-EQ-DECL NIL |nat_types| NIL) (|wf_nat| FORMULA-DECL NIL |naturalnumbers| NIL) (< CONST-DECL "bool" |reals| NIL) (|card| CONST-DECL "{n: nat | n = Card(S)}" |finite_sets| NIL) (|Card| CONST-DECL "nat" |finite_sets| NIL) (= CONST-DECL "[T, T -> boolean]" |equalities| NIL) (|nat| NONEMPTY-TYPE-EQ-DECL NIL |naturalnumbers| NIL) (|naturalnumber| TYPE-EQ-DECL NIL |naturalnumbers| NIL) (|finite_set| TYPE-EQ-DECL NIL |finite_sets| NIL) (|is_finite| CONST-DECL "bool" |finite_sets| NIL) (|set| TYPE-EQ-DECL NIL |sets| NIL) (|variable| TYPE-EQ-DECL NIL |first_order_terms_properties| 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) (|measure_induction| FORMULA-DECL NIL |measure_induction| NIL) (|well_founded?| CONST-DECL "bool" |orders| NIL) (|pred| TYPE-EQ-DECL NIL |defined_types| NIL)) SHOSTAK))("first_order_substitution" |first_order_substitution| |r_nice_disj_dom_img| 0 (|r_nice_disj_dom_img-1| NIL 3941000986 ("" (MEASURE-INDUCT+ "card(SV)" ("SV")) (("" (SKEEP) (("" (CASE "empty?(x!1)") (("1" (HIDE -2 -3) (("1" (EXPAND "r_nice_subs") (("1" (ASSERT) (("1" (GRIND) NIL NIL)) NIL)) NIL)) NIL) ("2" (EXPAND "r_nice_subs" 2) (("2" (ASSERT) (("2" (INST -1 "rest[variable](x!1)") (("2" (INST?) (("2" (REWRITE "card_rest") (("2" (ASSERT) (("2" (PROP) (("1" (EXPAND "disjoint?" 2) (("1" (EXPAND "empty?" 2) (("1" (SKEEP) (("1" (EXPAND "member") (("1" (EXPAND "intersection") (("1" (FLATTEN) (("1" (EXPAND "disjoint?") (("1" (EXPAND "empty?" -1) (("1" (INST?) (("1" (LEMMA "vars_img_append") (("1" (INST -1 "cons((choose(x!1), subs(sigma)(choose(x!1))),null)" "r_nice_subs(sigma)(rest[variable](x!1))") (("1" (EXPAND "subset?") (("1" (INST?) (("1" (EXPAND "append") (("1" (EXPAND "append") (("1" (ASSERT) (("1" (EXPAND "member" -1) (("1" (EXPAND "union") (("1" (SPLIT) (("1" (HIDE-ALL-BUT (-1 -2 -3 2)) (("1" (TYPEPRED "sigma") (("1" (LEMMA "nice_disjoint_dom_img") (("1" (INST?) (("1" (ASSERT) (("1" (EXPAND "disjoint?") (("1" (EXPAND "empty?" -1) (("1" (INST?) (("1" (EXPAND "member" 1) (("1" (EXPAND "intersection") (("1" (LEMMA "vars_finset") (("1" (INST -1 "x" "img(cons((choose(x!1), subs(sigma)(choose(x!1))), null))") (("1" (EXPAND "member" -1 1) (("1" (EXPAND "member" -3) (("1" (ASSERT) (("1" (SKEEP) (("1" (EXPAND "member" -1) (("1" (LEMMA "img_basic_sub") (("1" (INST?) (("1" (CASE "member(subs(sigma)(choose(x!1)), img(sigma))") (("1" (SPLIT -2) (("1" (REPLACES -1) (("1" (REWRITE "vars_singleton") (("1" (EXPAND "singleton") (("1" (LEMMA "vars_correct") (("1" (INST -1 "x" "img(sigma)" "t") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST -7 "choose(x!1)") (("2" (REWRITE "choose_member") (("2" (HIDE-ALL-BUT (-1 -2 -5 -7 2)) (("2" (LEMMA "nice_disjoint_dom_img") (("2" (INST?) (("2" (PROP) (("2" (EXPAND "disjoint?") (("2" (EXPAND "empty?" -1) (("2" (INST -1 "choose(x!1)") (("2" (EXPAND "member" 1) (("2" (EXPAND "intersection") (("2" (ASSERT) (("2" (LEMMA "vars_correct") (("2" (INST -1 "choose(x!1)" "img(sigma)" "subs(sigma)(choose(x!1))") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE-ALL-BUT (-4 -6 1 3)) (("2" (EXPAND "member" 1) (("2" (INST -2 "choose(x!1)") (("2" (REWRITE "choose_member") (("2" (EXPAND "img") (("2" (INST 1 "choose(x!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) ("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (LEMMA "rest_subset[variable]") (("2" (INST?) (("2" (HIDE 3) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ((|rest| CONST-DECL "set" |sets| NIL) (|card_rest| FORMULA-DECL NIL |finite_sets| NIL) (|int_minus_int_is_int| APPLICATION-JUDGEMENT "int" |integers| NIL) (|vars_img_append| FORMULA-DECL NIL |first_order_substitution| NIL) (|append| DEF-DECL "list[T]" |list_props| NIL) (|union| CONST-DECL "set" |sets| NIL) (|finite_remove| APPLICATION-JUDGEMENT "finite_set" |finite_sets| NIL) (|remove| CONST-DECL "set" |sets| NIL) (/= CONST-DECL "boolean" |notequal| NIL) (|nice_disjoint_dom_img| FORMULA-DECL NIL |first_order_substitution| NIL) (|vars_finset| FORMULA-DECL NIL |first_order_terms_properties| NIL) (|vars_singleton| FORMULA-DECL NIL |first_order_terms_properties| NIL) (|vars_correct| FORMULA-DECL NIL |first_order_terms_properties| NIL) (|singleton| CONST-DECL "(singleton?)" |sets| NIL) (|choose_member| FORMULA-DECL NIL |sets_lemmas| NIL) (|img_basic_sub| FORMULA-DECL NIL |first_order_substitution| NIL) (NOT CONST-DECL "[bool -> bool]" |booleans| NIL) (|null| ADT-CONSTRUCTOR-DECL "(null?)" |list_adt| NIL) (|null?| ADT-RECOGNIZER-DECL "[list -> boolean]" |list_adt| NIL) (|choose| CONST-DECL "(p)" |sets| NIL) (|nonempty?| CONST-DECL "bool" |sets| NIL) (|cons| ADT-CONSTRUCTOR-DECL "[[T, list] -> (cons?)]" |list_adt| NIL) (|cons?| ADT-RECOGNIZER-DECL "[list -> boolean]" |list_adt| NIL) (|real_ge_is_total_order| NAME-JUDGEMENT "(total_order?[real])" |real_props| NIL) (|rest_subset| FORMULA-DECL NIL |sets_lemmas| NIL) (|real_lt_is_strict_total_order| NAME-JUDGEMENT "(strict_total_order?[real])" |real_props| NIL) (|subset_is_partial_order| NAME-JUDGEMENT "(partial_order?[set[T]])" |sets_lemmas| NIL) (|finite_rest| APPLICATION-JUDGEMENT "finite_set" |finite_sets| NIL) (|member| CONST-DECL "bool" |sets| NIL) (|subs| CONST-DECL "first_order_term" |first_order_substitution| NIL) (|emptyset| CONST-DECL "set" |sets| NIL) (|intersection| CONST-DECL "set" |sets| NIL) (|finite_intersection1| APPLICATION-JUDGEMENT "finite_set" |finite_sets| NIL) (|finite_emptyset| NAME-JUDGEMENT "finite_set" |finite_sets| NIL) (|empty?| CONST-DECL "bool" |sets| NIL) (|r_nice_subs| DEF-DECL "sub" |first_order_substitution| NIL) (|img| CONST-DECL "finite_set[first_order_term[constant, variable, f_symbol]]" |first_order_substitution| NIL) (|disjoint?| CONST-DECL "bool" |sets| NIL) (|dom| CONST-DECL "finite_set[variable]" |first_order_substitution| NIL) (|subset?| CONST-DECL "bool" |sets| NIL) (IMPLIES CONST-DECL "[bool, bool -> bool]" |booleans| NIL) (|nice?| DEF-DECL "bool" |first_order_substitution| NIL) (|sub| TYPE-EQ-DECL NIL |first_order_substitution| NIL) (|list| TYPE-DECL NIL |list_adt| NIL) (|basic_sub| TYPE-EQ-DECL NIL |first_order_substitution| NIL) (|constant| TYPE-EQ-DECL NIL |first_order_terms_properties| NIL) (TRUE CONST-DECL "bool" |booleans| NIL) (AND CONST-DECL "[bool, bool -> bool]" |booleans| NIL) (PRED TYPE-EQ-DECL NIL |defined_types| NIL) (|first_order_term| TYPE-DECL NIL |first_order_term_adt| NIL) (|f_symbol| TYPE-EQ-DECL NIL |first_order_terms_properties| NIL) (|char| TYPE-EQ-DECL NIL |strings| NIL) (|char?| ADT-RECOGNIZER-DECL "[character -> boolean]" |character_adt| NIL) (|character| TYPE-DECL NIL |character_adt| NIL) (|below| TYPE-EQ-DECL NIL |nat_types| NIL) (|wf_nat| FORMULA-DECL NIL |naturalnumbers| NIL) (< CONST-DECL "bool" |reals| NIL) (|card| CONST-DECL "{n: nat | n = Card(S)}" |finite_sets| NIL) (|Card| CONST-DECL "nat" |finite_sets| NIL) (= CONST-DECL "[T, T -> boolean]" |equalities| NIL) (|nat| NONEMPTY-TYPE-EQ-DECL NIL |naturalnumbers| NIL) (|naturalnumber| TYPE-EQ-DECL NIL |naturalnumbers| NIL) (|finite_set| TYPE-EQ-DECL NIL |finite_sets| NIL) (|is_finite| CONST-DECL "bool" |finite_sets| NIL) (|set| TYPE-EQ-DECL NIL |sets| NIL) (|variable| TYPE-EQ-DECL NIL |first_order_terms_properties| 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) (|measure_induction| FORMULA-DECL NIL |measure_induction| NIL) (|well_founded?| CONST-DECL "bool" |orders| NIL) (|pred| TYPE-EQ-DECL NIL |defined_types| NIL)) SHOSTAK))("first_order_substitution" |first_order_substitution| |r_nice_dom_and_niceness| 0 (|r_nice_dom_and_niceness-1| NIL 3941028814 ("" (MEASURE-INDUCT+ "card(SV)" ("SV")) (("" (SKEEP) (("" (CASE "empty?(x!1)") (("1" (EXPAND "r_nice_subs" 1) (("1" (ASSERT) (("1" (HIDE -2 -3) (("1" (REWRITE "dom_null") (("1" (REWRITE "emptyset_is_empty?") (("1" (ASSERT) (("1" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (EXPAND "r_nice_subs" 2) (("2" (ASSERT) (("2" (INST -1 "rest[variable](x!1)") (("2" (INST -1 "sigma") (("2" (REWRITE "card_rest") (("2" (ASSERT) (("2" (SPLIT -1) (("1" (FLATTEN) (("1" (TYPEPRED "sigma") (("1" (LEMMA "nice_disjoint_dom_img") (("1" (LEMMA "nice_append2") (("1" (INST -1 "r_nice_subs(sigma)(rest[variable](x!1))" "cons((choose(x!1), subs(sigma)(choose(x!1))), null)") (("1" (ASSERT) (("1" (EXPAND "append" -1) (("1" (EXPAND "append" -1) (("1" (SPLIT -1) (("1" (ASSERT) (("1" (DECOMPOSE-EQUALITY 2) (("1" (IFF) (("1" (PROP) (("1" (LEMMA "choose_rest[variable]") (("1" (INST -1 "x!1") (("1" (ASSERT) (("1" (LEMMA "dom_append") (("1" (INST -1 "cons((choose(x!1), subs(sigma)(choose(x!1))), null)" "r_nice_subs(sigma)(rest[variable](x!1))") (("1" (EXPAND "append" -1) (("1" (EXPAND "append" -1) (("1" (EXPAND "subset?" -1) (("1" (INST -1 "x!2") (("1" (EXPAND "member") (("1" (EXPAND "union") (("1" (SPLIT) (("1" (LEMMA "dom_basic_sub") (("1" (INST -1 "choose(x!1)" " subs(sigma)(choose(x!1))") (("1" (SPLIT) (("1" (REPLACE -1 -2) (("1" (EXPAND "member" -2) (("1" (EXPAND "singleton" -2) (("1" (HIDE-ALL-BUT (-2 -3 1 2)) (("1" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE-ALL-BUT (-1 -3 -7 -10 2)) (("2" (LEMMA "nice_disjoint_dom_img") (("2" (INST -1 "sigma") (("2" (ASSERT) (("2" (EXPAND "disjoint?") (("2" (EXPAND "empty?") (("2" (INST -1 "choose(x!1)") (("2" (EXPAND "member") (("2" (EXPAND "intersection") (("2" (SPLIT) (("1" (GRIND) NIL NIL) ("2" (EXPAND "member") (("2" (LEMMA "apply_sub_elim_var_t") (("2" (INST -1 "choose(x!1)" "sigma" "variable(choose(x!1))") (("2" (EXPAND "member") (("2" (SPLIT) (("1" (GRIND) NIL NIL) ("2" (GRIND) NIL NIL) ("3" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE-ALL-BUT (-1 -2 -7 1 2)) (("2" (REWRITE "add_as_union") (("2" (EXPAND "member") (("2" (REPLACE -2 1 RL) (("2" (REPLACES -3) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (LEMMA "dom_append2") (("2" (INST -1 "cons((choose(x!1), subs(sigma)(choose(x!1))),null)" "r_nice_subs(sigma)(rest[variable](x!1))") (("2" (REPLACE -6 -1) (("2" (LEMMA "dom_basic_sub") (("2" (INST -1 "choose(x!1)" "subs(sigma)(choose(x!1))") (("2" (SPLIT -1) (("1" (REPLACE -1 -2) (("1" (SPLIT -2) (("1" (EXPAND "append " -1) (("1" (EXPAND "append " -1) (("1" (REPLACE -1 1) (("1" (HIDE-ALL-BUT (-3 +)) (("1" (HIDE +) (("1" (REWRITE "choose_rest[variable]" :DIR RL) (("1" (REVEAL +) (("1" (REWRITE "add_as_union") (("1" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (LEMMA "r_nice_disj_dom_img") (("2" (INST -1 "sigma" "rest[variable](x!1)") (("2" (SPLIT -1) (("1" (HIDE-ALL-BUT (-1 -9 1 3)) (("1" (GRIND) NIL NIL)) NIL) ("2" (HIDE-ALL-BUT (-8 1 4)) (("2" (LEMMA "rest_subset[variable]") (("2" (INST -1 "x!1") (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (HIDE-ALL-BUT (1 3)) (("3" (LEMMA "choose_not_member[variable]") (("3" (INST?) (("3" (ASSERT) (("3" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE-ALL-BUT (-1 -6 2 -9)) (("2" (LEMMA "nice_disjoint_dom_img2") (("2" (INST -1 "sigma" "choose(x!1)" "subs(sigma)(choose(x!1))") (("2" (CASE " member(choose(x!1), dom(sigma)) AND
       member(subs(sigma)(choose(x!1)), img(sigma))") (("1" (ASSERT) NIL NIL) ("2" (HIDE -1) (("2" (EXPAND "member" 1) (("2" (EXPAND "img") (("2" (CASE "dom(sigma)(choose(x!1))") (("1" (ASSERT) (("1" (INST 1 "choose(x!1)") (("1" (EXPAND "member") (("1" (PROPAX) NIL NIL)) NIL)) NIL)) NIL) ("2" (HIDE -1 -2 2) (("2" (LEMMA "choose_member[variable]") (("2" (INST?) (("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) ("2" (EXPAND "nice?" 1) (("2" (HIDE -1 -3 -4 3) (("2" (SPLIT) (("1" (LEMMA "nice_disjoint_dom_img2") (("1" (INST -1 "sigma" "choose(x!1)" "subs(sigma)(choose(x!1))") (("1" (CASE "member(choose(x!1), dom(sigma)) AND
       member(subs(sigma)(choose(x!1)), img(sigma))") (("1" (ASSERT) NIL NIL) ("2" (HIDE -1) (("2" (CASE " member(choose(x!1), dom(sigma))") (("1" (ASSERT) (("1" (EXPAND "member") (("1" (EXPAND "img") (("1" (INST 1 "choose(x!1)") (("1" (EXPAND "member") (("1" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE -1 -2 2) (("2" (LEMMA "choose_member[variable]") (("2" (INST -1 " x!1") (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE -2) (("2" (GRIND) NIL NIL)) NIL) ("3" (HIDE -1) (("3" (GRIND) NIL NIL)) NIL) ("4" (EXPAND "nice?") (("4" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("3" (SKEEP) (("3" (EXPAND "member" -1) (("3" (EXPAND "member" -1) (("3" (FLATTEN) (("3" (HIDE 3) (("3" (SPLIT) (("1" (REPLACES -2) (("1" (LEMMA " r_nice_supset_dom") (("1" (INST -1 "sigma" "rest[variable](x!1)") (("1" (PROP) (("1" (REPLACES -1) (("1" (HIDE-ALL-BUT (-1 1)) (("1" (REWRITE "choose_not_member") NIL NIL)) NIL)) NIL) ("2" (HIDE-ALL-BUT (-7 1 2)) (("2" (LEMMA "rest_subset[variable]") (("2" (INST?) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (LEMMA " r_nice_supset_dom") (("2" (INST -1 "sigma" "rest[variable](x!1)") (("2" (PROP) (("1" (REPLACES -1) (("1" (REPLACES -2) (("1" (INST -2 "sigma") (("1" (ASSERT) (("1" (HIDE -1 -4 -5) (("1" (LEMMA "rest_subset[variable]") (("1" (INST?) (("1" (LEMMA "subset_transitive[variable]") (("1" (INST -1 "rest[variable](x!1)" "x!1" "dom(sigma)") (("1" (ASSERT) (("1" (CASE "member(subs(sigma)(choose(x!1)),img(sigma))") (("1" (EXPAND "disjoint?") (("1" (EXPAND " empty?" 1) (("1" (EXPAND " empty?" -4) (("1" (SKEEP) (("1" (INST -5 "x") (("1" (LEMMA " vars_correct") (("1" (INST -1 "x" "img(sigma)" "subs(sigma)(choose(x!1))") (("1" (EXPAND " member" -5) (("1" (EXPAND " member" 1) (("1" (EXPAND "intersection") (("1" (FLATTEN) (("1" (ASSERT) (("1" (HIDE-ALL-BUT (-3 -6 1 2)) (("1" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE-ALL-BUT (-5 1 3)) (("2" (EXPAND "member") (("2" (EXPAND "img") (("2" (INST 1 "choose(x!1)") (("1" (LEMMA "choose_member[variable]") (("1" (INST?) (("1" (ASSERT) (("1" (GRIND) NIL NIL)) NIL)) NIL)) NIL) ("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE-ALL-BUT (-7 1 3)) (("2" (LEMMA "rest_subset[variable]") (("2" (INST?) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE-ALL-BUT (1 2)) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE 3) (("2" (LEMMA "rest_subset[variable]") (("2" (INST?) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ((|pred| TYPE-EQ-DECL NIL |defined_types| NIL) (|well_founded?| CONST-DECL "bool" |orders| NIL) (|measure_induction| FORMULA-DECL NIL |measure_induction| 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) (|variable| TYPE-EQ-DECL NIL |first_order_terms_properties| NIL) (|set| TYPE-EQ-DECL NIL |sets| NIL) (|is_finite| CONST-DECL "bool" |finite_sets| NIL) (|finite_set| TYPE-EQ-DECL NIL |finite_sets| NIL) (|naturalnumber| TYPE-EQ-DECL NIL |naturalnumbers| NIL) (|nat| NONEMPTY-TYPE-EQ-DECL NIL |naturalnumbers| NIL) (= CONST-DECL "[T, T -> boolean]" |equalities| NIL) (|Card| CONST-DECL "nat" |finite_sets| NIL) (|card| CONST-DECL "{n: nat | n = Card(S)}" |finite_sets| NIL) (< CONST-DECL "bool" |reals| NIL) (|wf_nat| FORMULA-DECL NIL |naturalnumbers| NIL) (|below| TYPE-EQ-DECL NIL |nat_types| NIL) (|character| TYPE-DECL NIL |character_adt| NIL) (|char?| ADT-RECOGNIZER-DECL "[character -> boolean]" |character_adt| NIL) (|char| TYPE-EQ-DECL NIL |strings| NIL) (|f_symbol| TYPE-EQ-DECL NIL |first_order_terms_properties| NIL) (|first_order_term| TYPE-DECL NIL |first_order_term_adt| NIL) (PRED TYPE-EQ-DECL NIL |defined_types| NIL) (AND CONST-DECL "[bool, bool -> bool]" |booleans| NIL) (TRUE CONST-DECL "bool" |booleans| NIL) (|constant| TYPE-EQ-DECL NIL |first_order_terms_properties| NIL) (|basic_sub| TYPE-EQ-DECL NIL |first_order_substitution| NIL) (|list| TYPE-DECL NIL |list_adt| NIL) (|sub| TYPE-EQ-DECL NIL |first_order_substitution| NIL) (|nice?| DEF-DECL "bool" |first_order_substitution| NIL) (IMPLIES CONST-DECL "[bool, bool -> bool]" |booleans| NIL) (|subset?| CONST-DECL "bool" |sets| NIL) (|dom| CONST-DECL "finite_set[variable]" |first_order_substitution| NIL) (|r_nice_subs| DEF-DECL "sub" |first_order_substitution| NIL) (|empty?| CONST-DECL "bool" |sets| NIL) (|subset_is_partial_order| NAME-JUDGEMENT "(partial_order?[set[T]])" |sets_lemmas| NIL) (|dom_null| FORMULA-DECL NIL |first_order_substitution| NIL) (|finite_emptyset| NAME-JUDGEMENT "finite_set" |finite_sets| NIL) (|emptyset_is_empty?| FORMULA-DECL NIL |sets_lemmas| NIL) (|finite_rest| APPLICATION-JUDGEMENT "finite_set" |finite_sets| NIL) (|real_lt_is_strict_total_order| NAME-JUDGEMENT "(strict_total_order?[real])" |real_props| NIL) (|nice_disjoint_dom_img| FORMULA-DECL NIL |first_order_substitution| NIL) (|nonempty?| CONST-DECL "bool" |sets| NIL) (|cons?| ADT-RECOGNIZER-DECL "[list -> boolean]" |list_adt| NIL) (|cons| ADT-CONSTRUCTOR-DECL "[[T, list] -> (cons?)]" |list_adt| NIL) (|choose| CONST-DECL "(p)" |sets| NIL) (|subs| CONST-DECL "first_order_term" |first_order_substitution| NIL) (|null?| ADT-RECOGNIZER-DECL "[list -> boolean]" |list_adt| NIL) (|null| ADT-CONSTRUCTOR-DECL "(null?)" |list_adt| NIL) (|append| DEF-DECL "list[T]" |list_props| NIL) (|dom_append| FORMULA-DECL NIL |first_order_substitution| NIL) (|member| CONST-DECL "bool" |sets| NIL) (|disjoint?| CONST-DECL "bool" |sets| NIL) (|intersection| CONST-DECL "set" |sets| NIL) (|var?| ADT-RECOGNIZER-DECL "[first_order_term -> boolean]" |first_order_term_adt| NIL) (|variable| ADT-CONSTRUCTOR-DECL "[variable -> (var?)]" |first_order_term_adt| NIL) (|img| CONST-DECL "finite_set[first_order_term[constant, variable, f_symbol]]" |first_order_substitution| NIL) (|apply_sub_elim_var_t| FORMULA-DECL NIL |first_order_substitution| NIL) (|finite_remove| APPLICATION-JUDGEMENT "finite_set" |finite_sets| NIL) (|nonempty_singleton_finite| APPLICATION-JUDGEMENT "non_empty_finite_set" |finite_sets| NIL) (|real_ge_is_total_order| NAME-JUDGEMENT "(total_order?[real])" |real_props| NIL) (|finite_intersection1| APPLICATION-JUDGEMENT "finite_set" |finite_sets| NIL) (|nonempty_add_finite| APPLICATION-JUDGEMENT "non_empty_finite_set" |finite_sets| NIL) (|singleton| CONST-DECL "(singleton?)" |sets| NIL) (|dom_basic_sub| FORMULA-DECL NIL |first_order_substitution| NIL) (|add_as_union| FORMULA-DECL NIL |sets_lemmas| NIL) (|nonempty_finite_union2| APPLICATION-JUDGEMENT "non_empty_finite_set" |finite_sets| NIL) (|remove| CONST-DECL "set" |sets| NIL) (|union| CONST-DECL "set" |sets| NIL) (|choose_rest| FORMULA-DECL NIL |sets_lemmas| NIL) (/= CONST-DECL "boolean" |notequal| NIL) (|nonempty_finite_union1| APPLICATION-JUDGEMENT "non_empty_finite_set" |finite_sets| NIL) (|rest_subset| FORMULA-DECL NIL |sets_lemmas| NIL) (|r_nice_disj_dom_img| FORMULA-DECL NIL |first_order_substitution| NIL) (|choose_not_member| FORMULA-DECL NIL |sets_lemmas| NIL) (|nice_disjoint_dom_img2| FORMULA-DECL NIL |first_order_substitution| NIL) (|choose_member| FORMULA-DECL NIL |sets_lemmas| NIL) (|dom_append2| FORMULA-DECL NIL |first_order_substitution| NIL) (|supset_dom| DEF-DECL "finite_set[variable]" |first_order_substitution| NIL) (|emptyset| CONST-DECL "set" |sets| NIL) (|member| DEF-DECL "bool" |list_props| NIL) (|r_nice_supset_dom| FORMULA-DECL NIL |first_order_substitution| NIL) (|vars_correct| FORMULA-DECL NIL |first_order_terms_properties| NIL) (|subset_transitive| FORMULA-DECL NIL |sets_lemmas| NIL) (|nice_append2| FORMULA-DECL NIL |first_order_substitution| NIL) (NOT CONST-DECL "[bool -> bool]" |booleans| NIL) (|int_minus_int_is_int| APPLICATION-JUDGEMENT "int" |integers| NIL) (|card_rest| FORMULA-DECL NIL |finite_sets| NIL) (|rest| CONST-DECL "set" |sets| NIL)) NIL))("first_order_substitution" |first_order_substitution| |r_nice_equality| 0 (|r_nice_equality-1| NIL 3941029339 ("" (MEASURE-INDUCT+ "card(SV)" ("SV")) (("" (CASE "empty?(x!1)") (("1" (HIDE -2) (("1" (SKEEP) (("1" (GRIND) NIL NIL)) NIL)) NIL) ("2" (SKEEP) (("2" (CASE "X = choose(x!1)") (("1" (REPLACES -1) (("1" (HIDE -1) (("1" (EXPAND "r_nice_subs") (("1" (ASSERT) (("1" (LEMMA " r_nice_dom_and_niceness") (("1" (INST -1 "sigma" "rest[variable](x!1)") (("1" (PROP) (("1" (EXPAND "subs" 2 2) (("1" (LEMMA "subs_no_effect_t_var") (("1" (INST -1 "choose(x!1)" " r_nice_subs(sigma)(rest[variable](x!1))" " subs(sigma)(choose(x!1))") (("1" (REPLACE -2 -1) (("1" (LEMMA "choose_not_member[variable]") (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (LEMMA "rest_subset[variable]") (("2" (INST?) (("2" (HIDE -3 3) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST -1 "rest[variable](x!1)") (("2" (INST -1 "X" "sigma") (("2" (REWRITE "card_rest") (("2" (ASSERT) (("2" (CASE "subset?(rest[variable](x!1), dom(sigma)) AND
        member(X, rest[variable](x!1))") (("1" (ASSERT) (("1" (FLATTEN) (("1" (ASSERT) (("1" (EXPAND "r_nice_subs" 3) (("1" (EXPAND "subs" 3 2) (("1" (EXPAND "subs" 3 2) (("1" (EXPAND "subs" -3 2) (("1" (REPLACE -3 3 RL) (("1" (TYPEPRED "sigma") (("1" (HIDE-ALL-BUT (-1 -3 -6 1 2 3)) (("1" (LEMMA "nice_disjoint_dom_img") (("1" (INST?) (("1" (ASSERT) (("1" (REVEAL -2 -4) (("1" (CASE "member(subs(sigma)(X), img(sigma))") (("1" (CASE "NOT member(choose(x!1), vars(subs(sigma)(X)))") (("1" (REWRITE "basic_sub_no_effect") NIL NIL) ("2" (HIDE -3 -6 3) (("2" (CASE "member(choose(x!1), dom(sigma))") (("1" (LEMMA "vars_correct") (("1" (INST -1 "choose(x!1)" "img(sigma)" "subs(sigma)(X)") (("1" (ASSERT) (("1" (EXPAND "disjoint?") (("1" (EXPAND "empty?") (("1" (INST -6 "choose(x!1)") (("1" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE-ALL-BUT (-3 1 3)) (("2" (LEMMA "choose_member[variable]") (("2" (INST?) (("2" (ASSERT) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE-ALL-BUT (-2 -5 -6 1 3)) (("2" (EXPAND "member" 1) (("2" (EXPAND "img") (("2" (INST 1 "X") (("2" (GRIND) 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 -3 1 2 3)) (("2" (PROP) (("1" (LEMMA "rest_subset[variable]") (("1" (INST?) (("1" (GRIND) NIL NIL)) NIL)) NIL) ("2" (HIDE -1) (("2" (LEMMA "choose_rest[variable]") (("2" (INST?) (("2" (ASSERT) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL) ((|empty?| CONST-DECL "bool" |sets| NIL) (|subset_is_partial_order| NAME-JUDGEMENT "(partial_order?[set[T]])" |sets_lemmas| NIL) (|choose| CONST-DECL "(p)" |sets| NIL) (|nonempty?| CONST-DECL "bool" |sets| NIL) (|finite_rest| APPLICATION-JUDGEMENT "finite_set" |finite_sets| NIL) (|rest| CONST-DECL "set" |sets| NIL) (|rest_subset| FORMULA-DECL NIL |sets_lemmas| NIL) (|real_ge_is_total_order| NAME-JUDGEMENT "(total_order?[real])" |real_props| NIL) (NOT CONST-DECL "[bool -> bool]" |booleans| NIL) (/= CONST-DECL "boolean" |notequal| NIL) (|remove| CONST-DECL "set" |sets| NIL) (|finite_remove| APPLICATION-JUDGEMENT "finite_set" |finite_sets| NIL) (|choose_not_member| FORMULA-DECL NIL |sets_lemmas| NIL) (|subs_no_effect_t_var| FORMULA-DECL NIL |first_order_substitution| NIL) (|r_nice_dom_and_niceness| FORMULA-DECL NIL |first_order_substitution| NIL) (|real_lt_is_strict_total_order| NAME-JUDGEMENT "(strict_total_order?[real])" |real_props| NIL) (|nonempty_add_finite| APPLICATION-JUDGEMENT "non_empty_finite_set" |finite_sets| NIL) (|choose_rest| FORMULA-DECL NIL |sets_lemmas| NIL) (|nice_disjoint_dom_img| FORMULA-DECL NIL |first_order_substitution| NIL) (|img| CONST-DECL "finite_set[first_order_term[constant, variable, f_symbol]]" |first_order_substitution| NIL) (|choose_member| FORMULA-DECL NIL |sets_lemmas| NIL) (|vars_correct| FORMULA-DECL NIL |first_order_terms_properties| NIL) (|finite_intersection1| APPLICATION-JUDGEMENT "finite_set" |finite_sets| NIL) (|intersection| CONST-DECL "set" |sets| NIL) (|disjoint?| CONST-DECL "bool" |sets| NIL) (|basic_sub_no_effect| FORMULA-DECL NIL |first_order_substitution| NIL) (|int_minus_int_is_int| APPLICATION-JUDGEMENT "int" |integers| NIL) (|card_rest| FORMULA-DECL NIL |finite_sets| NIL) (|r_nice_subs| DEF-DECL "sub" |first_order_substitution| NIL) (|subs| CONST-DECL "first_order_term" |first_order_substitution| NIL) (|member| CONST-DECL "bool" |sets| NIL) (|dom| CONST-DECL "finite_set[variable]" |first_order_substitution| NIL) (|subset?| CONST-DECL "bool" |sets| NIL) (IMPLIES CONST-DECL "[bool, bool -> bool]" |booleans| NIL) (|nice?| DEF-DECL "bool" |first_order_substitution| NIL) (|sub| TYPE-EQ-DECL NIL |first_order_substitution| NIL) (|list| TYPE-DECL NIL |list_adt| NIL) (|basic_sub| TYPE-EQ-DECL NIL |first_order_substitution| NIL) (|constant| TYPE-EQ-DECL NIL |first_order_terms_properties| NIL) (TRUE CONST-DECL "bool" |booleans| NIL) (AND CONST-DECL "[bool, bool -> bool]" |booleans| NIL) (PRED TYPE-EQ-DECL NIL |defined_types| NIL) (|first_order_term| TYPE-DECL NIL |first_order_term_adt| NIL) (|f_symbol| TYPE-EQ-DECL NIL |first_order_terms_properties| NIL) (|char| TYPE-EQ-DECL NIL |strings| NIL) (|char?| ADT-RECOGNIZER-DECL "[character -> boolean]" |character_adt| NIL) (|character| TYPE-DECL NIL |character_adt| NIL) (|below| TYPE-EQ-DECL NIL |nat_types| NIL) (|wf_nat| FORMULA-DECL NIL |naturalnumbers| NIL) (< CONST-DECL "bool" |reals| NIL) (|card| CONST-DECL "{n: nat | n = Card(S)}" |finite_sets| NIL) (|Card| CONST-DECL "nat" |finite_sets| NIL) (= CONST-DECL "[T, T -> boolean]" |equalities| NIL) (|nat| NONEMPTY-TYPE-EQ-DECL NIL |naturalnumbers| NIL) (|naturalnumber| TYPE-EQ-DECL NIL |naturalnumbers| NIL) (|finite_set| TYPE-EQ-DECL NIL |finite_sets| NIL) (|is_finite| CONST-DECL "bool" |finite_sets| NIL) (|set| TYPE-EQ-DECL NIL |sets| NIL) (|variable| TYPE-EQ-DECL NIL |first_order_terms_properties| 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) (|measure_induction| FORMULA-DECL NIL |measure_induction| NIL) (|well_founded?| CONST-DECL "bool" |orders| NIL) (|pred| TYPE-EQ-DECL NIL |defined_types| NIL)) SHOSTAK))("antiunif" |antiunif| |matchingFuns_generalizer_classification| 0 (|matchingFuns_generalizer_classification-1| NIL 3940310874 ("" (SKEEP) (("" (BETA) (("" (TYPEPRED "c") (("" (TYPEPRED "gamma") (("" (EXPAND "generalizer?") (("" (FLATTEN) (("" (SKEEP) (("" (INST -3 "car(c`unsolved)") (("1" (FLATTEN) (("1" (HIDE -4) (("1" (EXPAND "subs" -3) (("1" (REWRITE "subs_append2") (("1" (LEMMA "subs_ord") (("1" (INST -1 "subs(gamma)(variable(car(c`unsolved)`label))" "tau_l" "subs(tau_l)(subs(gamma)(variable(car(c`unsolved)`label)))") (("1" (EXPAND "subs" 1) (("1" (ASSERT) (("1" (HIDE -2 -5) (("1" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE -1 -3) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ((|car| ADT-ACCESSOR-DECL "[(cons?) -> T]" |list_adt| NIL) (|cons?| ADT-RECOGNIZER-DECL "[list -> boolean]" |list_adt| NIL) (|member| DEF-DECL "bool" |list_props| NIL) (|AUEquation| TYPE-EQ-DECL NIL |antiunif| NIL) (|Term| NONEMPTY-TYPE-EQ-DECL NIL |antiunif| NIL) (|subs_append2| FORMULA-DECL NIL |first_order_substitution| NIL) (|var?| ADT-RECOGNIZER-DECL "[first_order_term -> boolean]" |first_order_term_adt| NIL) (|variable| ADT-CONSTRUCTOR-DECL "[variable -> (var?)]" |first_order_term_adt| NIL) (|sym| CONST-DECL "string" |first_order_terms_properties| NIL) (|list2finseq| CONST-DECL "finseq[T]" |list2finseq| NIL) (|length| DEF-DECL "nat" |list_props| NIL) (|ord| CONST-DECL "upto(4)" |first_order_term_adt| NIL) (|labels| DEF-DECL "finite_set[variable]" |antiunif| NIL) (|subs_ord| FORMULA-DECL NIL |first_order_substitution| NIL) (|subs| CONST-DECL "first_order_term" |first_order_substitution| NIL) (|boolean| NONEMPTY-TYPE-DECL NIL |booleans| NIL) (|bool| NONEMPTY-TYPE-EQ-DECL NIL |booleans| NIL) (NOT CONST-DECL "[bool -> bool]" |booleans| NIL) (|List_eq| TYPE-EQ-DECL NIL |antiunif| 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) (|variable| TYPE-EQ-DECL NIL |first_order_terms_properties| NIL) (|nat| NONEMPTY-TYPE-EQ-DECL NIL |naturalnumbers| NIL) (|below| TYPE-EQ-DECL NIL |nat_types| NIL) (|character| TYPE-DECL NIL |character_adt| NIL) (|char?| ADT-RECOGNIZER-DECL "[character -> boolean]" |character_adt| NIL) (|char| TYPE-EQ-DECL NIL |strings| NIL) (|f_symbol| TYPE-EQ-DECL NIL |first_order_terms_properties| NIL) (|first_order_term| TYPE-DECL NIL |first_order_term_adt| NIL) (PRED TYPE-EQ-DECL NIL |defined_types| NIL) (AND CONST-DECL "[bool, bool -> bool]" |booleans| NIL) (TRUE CONST-DECL "bool" |booleans| NIL) (|constant| TYPE-EQ-DECL NIL |first_order_terms_properties| NIL) (|basic_sub| TYPE-EQ-DECL NIL |first_order_substitution| NIL) (|list| TYPE-DECL NIL |list_adt| NIL) (|sub| TYPE-EQ-DECL NIL |first_order_substitution| NIL) (|nice?| DEF-DECL "bool" |first_order_substitution| NIL) (|Configuration| TYPE-EQ-DECL NIL |antiunif| NIL) (|validConfiguration?| CONST-DECL "bool" |antiunif| NIL) (|matchingFuns_conf?| CONST-DECL "bool" |antiunif| NIL)) SHOSTAK))("antiunif" |antiunif| |r_generalizer_is_generalizer| 0 (|r_generalizer_is_generalizer-1| NIL 3940393140 ("" (SKEEP) (("" (TYPEPRED "gamma") (("" (HIDE -1) (("" (GRIND) NIL NIL)) NIL)) NIL)) NIL) ((|r_generalizer?| CONST-DECL "bool" |antiunif| NIL) (|validConfiguration?| CONST-DECL "bool" |antiunif| NIL) (|Configuration| TYPE-EQ-DECL NIL |antiunif| NIL) (|List_eq| TYPE-EQ-DECL NIL |antiunif| NIL) (|nice?| DEF-DECL "bool" |first_order_substitution| NIL) (|sub| TYPE-EQ-DECL NIL |first_order_substitution| NIL) (|list| TYPE-DECL NIL |list_adt| NIL) (|basic_sub| TYPE-EQ-DECL NIL |first_order_substitution| NIL) (|constant| TYPE-EQ-DECL NIL |first_order_terms_properties| NIL) (TRUE CONST-DECL "bool" |booleans| NIL) (AND CONST-DECL "[bool, bool -> bool]" |booleans| NIL) (PRED TYPE-EQ-DECL NIL |defined_types| NIL) (|first_order_term| TYPE-DECL NIL |first_order_term_adt| NIL) (|f_symbol| TYPE-EQ-DECL NIL |first_order_terms_properties| NIL) (|char| TYPE-EQ-DECL NIL |strings| NIL) (|char?| ADT-RECOGNIZER-DECL "[character -> boolean]" |character_adt| NIL) (|character| TYPE-DECL NIL |character_adt| NIL) (|below| TYPE-EQ-DECL NIL |nat_types| NIL) (|nat| NONEMPTY-TYPE-EQ-DECL NIL |naturalnumbers| NIL) (|variable| TYPE-EQ-DECL NIL |first_order_terms_properties| 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) (NOT CONST-DECL "[bool -> bool]" |booleans| NIL) (|bool| NONEMPTY-TYPE-EQ-DECL NIL |booleans| NIL) (|boolean| NONEMPTY-TYPE-DECL NIL |booleans| NIL) (|antiunification_j| APPLICATION-JUDGEMENT "(validConfiguration?)" |antiunif| NIL) (|disjoint?| CONST-DECL "bool" |sets| NIL) (|intersection| CONST-DECL "set" |sets| NIL) (|union| CONST-DECL "set" |sets| NIL) (|difference| CONST-DECL "set" |sets| NIL) (|empty?| CONST-DECL "bool" |sets| NIL) (|img| CONST-DECL "finite_set[first_order_term[constant, variable, f_symbol]]" |first_order_substitution| NIL) (|member| CONST-DECL "bool" |sets| NIL) (|dom| CONST-DECL "finite_set[variable]" |first_order_substitution| NIL) (|subs| CONST-DECL "first_order_term" |first_order_substitution| NIL)) SHOSTAK))("antiunif" |antiunif| |generalizer_is_r_generalizer_TCC1| 0 (|generalizer_is_r_generalizer_TCC1-1| NIL 3941082920 ("" (SUBTYPE-TCC) NIL NIL) NIL NIL (|generalizer_is_r_generalizer| SUBTYPE "list_props[basic_sub].append(antiunif.rho, antiunif.gamma)" "(first_order_substitution.nice?)")))("antiunif" |antiunif| |generalizer_is_r_generalizer| 0 (|generalizer_is_r_generalizer-1| NIL 3941086710 ("" (SKEEP) (("" (INST 1 "disj_var_renaming(vars(img(gamma)), vars(antiunify(c)))") (("" (EXPAND "r_generalizer?") (("" (LEMMA "renaming_sub_dom_preservation") (("" (INST -1 "gamma" "disj_var_renaming(vars(img(gamma)), vars(antiunify(c)))") (("" (TYPEPRED "gamma") (("" (EXPAND "generalizer?" -2) (("" (FLATTEN -2) (("" (ASSERT) (("" (SPLIT -4) (("1" (POSTPONE) NIL NIL) ("2" (REWRITE "dis_var_renaming_niceness?") NIL NIL) ("3" (HIDE -4 2) (("3" (POSTPONE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) NIL SHOSTAK))("antiunif" |antiunif| |antiunify_preserves_lbls_unsolved| 0 (|antiunify_preserves_lbls_unsolved-1| NIL 3940675731 ("" (MEASURE-INDUCT "size(c`unsolved)" ("c")) (("" (SKEEP) (("" (LEMMA "antiunify_derivability") (("" (INST?) (("" (PROP) (("1" (EXPAND "antiunify" 1) (("1" (EXPAND "matchingFuns_conf?") (("1" (EXPAND "matchingFuns?") (("1" (FLATTEN) (("1" (ASSERT) (("1" (INST -3 "decomposeFuns(x)") (("1" (ASSERT) (("1" (EXPAND "decomposeFuns" -3 1) (("1" (EXPAND "makeEq") (("1" (EXPAND "labels" -3) (("1" (EXPAND "labels" 1) (("1" (REWRITE* "add_as_union") (("1" (REWRITE* "subset_union") (("1" (FLATTEN) (("1" (ASSERT) (("1" (HIDE -3 -4) (("1" (EXPAND "subset?") (("1" (SKEEP) (("1" (EXPAND "member") (("1" (EXPAND "singleton") (("1" (REPLACES -3) (("1" (LEMMA "antiunify_sub_decomposition") (("1" (INST -1 "decomposeFuns(x)") (("1" (SKEEP) (("1" (EXPAND "vars" 1) (("1" (CASE "member(car(x`unsolved)`label, supset_dom(antiunify(decomposeFuns(x))`substitution))") (("1" (EXPAND "union") (("1" (FLATTEN) (("1" (HIDE 1) (("1" (EXPAND "member") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (REPLACES -1) (("2" (EXPAND "member") (("2" (LEMMA "supset_dom_correct") (("2" (INST -1 "car(x`unsolved)`label" "append(theta, decomposeFuns(x)`substitution)") (("2" (PROP) (("1" (EXPAND "member") (("1" (PROPAX) NIL NIL)) NIL) ("2" (HIDE 1) (("2" (EXPAND "subs") (("2" (REWRITE "subs_append2") (("2" (EXPAND "decomposeFuns") (("2" (LEMMA "subs_no_effect_t_var") (("2" (INST -1 "car(x`unsolved)`label" "x`substitution" "app(sym(car(x`unsolved)`lhs),
                          variable(freshLabel(x)))") (("2" (PROP) (("1" (EXPAND "subs" -1) (("1" (REPLACES -1) (("1" (REWRITE "subs_app") (("1" (GRIND) NIL NIL)) NIL)) NIL)) NIL) ("2" (HIDE -2) (("2" (TYPEPRED "x") (("2" (EXPAND "validConfiguration?") (("2" (FLATTEN) (("2" (HIDE -1 -3 -4) (("2" (LEMMA "supset_dom_correct2") (("2" (INST?) (("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)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (EXPAND "antiunify" 1) (("2" (EXPAND "matchingPairs_conf?") (("2" (EXPAND "matchingPairs?") (("2" (FLATTEN) (("2" (LEMMA "matchingPairs_classification") (("2" (INST?) (("2" (EXPAND "normal_configuration?") (("2" (ASSERT) (("2" (EXPAND "matchingPairs_conf?") (("2" (EXPAND "matchingPairs?" -1) (("2" (ASSERT) (("2" (INST -3 "decomposePairs(x)") (("2" (ASSERT) (("2" (EXPAND "decomposePairs" -3 1) (("2" (EXPAND "makeEq") (("2" (EXPAND "labels" -3) (("2" (EXPAND "labels" -3) (("2" (EXPAND "labels" 2) (("2" (REWRITE* "add_as_union") (("2" (REWRITE* "subset_union") (("2" (FLATTEN) (("2" (ASSERT) (("2" (HIDE -3 -4 -5) (("2" (EXPAND "subset?") (("2" (SKEEP) (("2" (EXPAND "member") (("2" (EXPAND "singleton") (("2" (REPLACES -3) (("2" (LEMMA "antiunify_sub_decomposition") (("2" (INST -1 "decomposePairs(x)") (("2" (SKEEP) (("2" (EXPAND "vars" 2) (("2" (CASE "member(car(x`unsolved)`label, supset_dom(antiunify(decomposePairs(x))`substitution))") (("1" (EXPAND "union") (("1" (FLATTEN) (("1" (HIDE 2) (("1" (EXPAND "member") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE 3) (("2" (REPLACES -1) (("2" (EXPAND "member") (("2" (LEMMA "supset_dom_correct") (("2" (INST -1 "car(x`unsolved)`label" "append(theta, decomposePairs(x)`substitution)") (("2" (PROP) (("1" (EXPAND "member") (("1" (PROPAX) NIL NIL)) NIL) ("2" (HIDE 1) (("2" (EXPAND "subs") (("2" (REWRITE "subs_append2") (("2" (EXPAND "decomposePairs") (("2" (LEMMA "subs_no_effect_t_var") (("2" (INST -1 "car(x`unsolved)`label" "x`substitution" "pair(variable(freshLabel(x)),
                           variable(freshLabel(union(vars(x),
                                                     singleton(freshLabel(x))))))") (("2" (PROP) (("1" (EXPAND "subs" -1) (("1" (REPLACES -1) (("1" (REWRITE "subs_pair") (("1" (GRIND) NIL NIL)) NIL)) NIL)) NIL) ("2" (HIDE -2) (("2" (TYPEPRED "x") (("2" (EXPAND "validConfiguration?") (("2" (FLATTEN) (("2" (HIDE -1 -3 -4) (("2" (LEMMA "supset_dom_correct2") (("2" (INST?) (("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)) 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) ("3" (EXPAND "antiunify" 1) (("3" (EXPAND "syntacticallyEq_conf?") (("3" (EXPAND "syntacticallyEq?") (("3" (FLATTEN) (("3" (LEMMA "syntacticallyEq_classification") (("3" (INST?) (("3" (EXPAND "normal_configuration?") (("3" (ASSERT) (("3" (EXPAND "syntacticallyEq_conf?") (("3" (EXPAND "syntacticallyEq?" -1) (("3" (FLATTEN) (("3" (ASSERT) (("3" (INST -3 "trivialSyn_Eqs(x)") (("3" (ASSERT) (("3" (EXPAND "trivialSyn_Eqs" -3 1) (("3" (EXPAND "labels" 3) (("3" (REWRITE "add_as_union") (("3" (REWRITE "subset_union") (("3" (ASSERT) (("3" (HIDE -3) (("3" (EXPAND "subset?") (("3" (SKEEP) (("3" (EXPAND "member") (("3" (EXPAND "singleton") (("3" (REPLACES -3) (("3" (LEMMA "antiunify_sub_decomposition") (("3" (INST -1 "trivialSyn_Eqs(x)") (("3" (SKEEP) (("3" (EXPAND "vars" 3) (("3" (CASE "member(car(x`unsolved)`label, supset_dom(antiunify(trivialSyn_Eqs(x))`substitution))") (("1" (EXPAND "union") (("1" (FLATTEN) (("1" (HIDE 3) (("1" (EXPAND "member") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE 4) (("2" (EXPAND "member") (("2" (LEMMA "supset_dom_correct") (("2" (INST -1 "car(x`unsolved)`label" "antiunify(trivialSyn_Eqs(x))`substitution") (("2" (PROP) (("1" (EXPAND "member") (("1" (PROPAX) NIL NIL)) NIL) ("2" (HIDE 1) (("2" (LEMMA "antiunify_sub_preserves_terms") (("2" (EXPAND "trivialSyn_Eqs" -3 2) (("2" (INST -1 "trivialSyn_Eqs(x)" "car(x`unsolved)`lhs") (("2" (PROP) (("1" (REPLACES -3 -2) (("1" (EXPAND "subs" -2) (("1" (REWRITE "subs_append2") (("1" (EXPAND "subs" -2 2) (("1" (LEMMA "invariance_labels_in_validConf") (("1" (INST -1 "x") (("1" (BETA) (("1" (INST -1 "car(x`unsolved)`label") (("1" (REPLACES -1) (("1" (EXPAND "subs" -2 2) (("1" (REVEAL -4) (("1" (REPLACES -1) (("1" (REWRITE "subs_append2") (("1" (EXPAND "subs" -1 2) (("1" (EXPAND "trivialSyn_Eqs") (("1" (EXPAND "subs" -1 4) (("1" (LEMMA "subs_no_effect_t") (("1" (INST -1 "x`substitution" "car(x`unsolved)`lhs") (("1" (PROP) (("1" (REPLACES -1) (("1" (LEMMA "basic_sub_no_effect") (("1" (INST -1 "car(x`unsolved)`label" "car(x`unsolved)`lhs" "car(x`unsolved)`lhs") (("1" (PROP) (("1" (REPLACES -1) (("1" (REPLACES -1) (("1" (TYPEPRED "x") (("1" (EXPAND "validConfiguration?") (("1" (EXPAND "validEqs?") (("1" (FLATTEN) (("1" (HIDE -2 -3 -4 -5) (("1" (EXPAND "append") (("1" (EXPAND "vars") (("1" (EXPAND "vars" -1 1) (("1" (EXPAND "labels") (("1" (REPLACE -2 -1) (("1" (EXPAND "vars" -1 1) (("1" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE -2 -3) (("2" (TYPEPRED "x") (("2" (EXPAND "validConfiguration?") (("2" (EXPAND "validEqs?") (("2" (FLATTEN) (("2" (HIDE -2 -3 -4 -5) (("2" (EXPAND "append") (("2" (EXPAND "vars" -1) (("2" (EXPAND "vars" -1 1) (("2" (EXPAND "labels") (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE -1 -2) (("2" (TYPEPRED "x") (("2" (EXPAND "validConfiguration?") (("2" (FLATTEN) (("2" (HIDE -1 -2 -3) (("2" (LEMMA "supset_dom_correct2") (("2" (INST?) (("2" (EXPAND "disjoint?") (("2" (EXPAND "empty?") (("2" (SKEEP) (("2" (EXPAND "subset?") (("2" (INST?) (("2" (INST?) (("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) ("2" (HIDE -1 -2) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (REWRITE "syntEq_car_lhs_member_img") NIL NIL) ("3" (HIDE -1 -2) (("3" (POSTPONE) 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)) NIL)) NIL)) NIL) ("4" (POSTPONE) NIL NIL) ("5" (HIDE -2) (("5" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) NIL SHOSTAK))("antiunif" |antiunif| |antiunif_completeness| 0 (|antiunif_completeness-1| NIL 3940393387 ("" (MEASURE-INDUCT+ "size(c`unsolved)" ("c")) (("" (LEMMA "antiunify_derivability") (("" (INST?) (("" (SKEEP) (("" (PROP) (("1" (LEMMA "matchingFuns_generalizer_classification") (("1" (INST?) (("1" (INST -1 "gamma") (("1" (BETA) (("1" (EXPAND "antiunify" 1) (("1" (ASSERT) (("1" (EXPAND "matchingFuns_conf?") (("1" (EXPAND "matchingFuns?") (("1" (FLATTEN) (("1" (ASSERT) (("1" (INST -4 "decomposeFuns(x!1)") (("1" (PROP) (("1" (NAME-REPLACE "Y" "subs(gamma)(car(x!1`unsolved)`label)") (("1" (INST -4 "cons((car(decomposeFuns(x!1)`unsolved)`label, variable(freshLabel(union(vars(img(gamma)),vars(antiunify(decomposeFuns(x!1))))))), r_nice_subs(gamma)(labels(cdr(x!1`unsolved))))") (("1" (ASSERT) (("1" (EXPAND "more_general?") (("1" (SKOLEM -4 "delta_p") (("1" (EXPAND "equal?") (("1" (NAME-REPLACE "gamma_p" "cons((car(decomposeFuns(x!1)`unsolved)`label,
                            variable(freshLabel(union(vars(img(gamma)),
                                                      vars(antiunify(decomposeFuns(x!1))))))),
                           r_nice_subs(gamma)(labels(cdr(x!1`unsolved))))") (("1" (INST 1 "cons((V(Y), subs(antiunify(x!1)`substitution)(car(x!1`unsolved)`label)),
                                          r_nice_subs(delta_p)(labels(cdr(x!1`unsolved))))") (("1" (POSTPONE) NIL NIL) ("2" (POSTPONE) NIL NIL) ("3" (POSTPONE) NIL NIL)) NIL) ("2" (POSTPONE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (POSTPONE) NIL NIL) ("3" (POSTPONE) NIL NIL)) NIL)) NIL) ("2" (POSTPONE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (POSTPONE) NIL NIL)) NIL)) NIL)) NIL) ("2" (POSTPONE) NIL NIL) ("3" (POSTPONE) NIL NIL) ("4" (POSTPONE) NIL NIL) ("5" (POSTPONE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) NIL SHOSTAK))("antiunif" |antiunif| |antiunif_is_complete| 0 (|antiunif_is_complete-1| NIL 3939877632 ("" (SKEEP) (("" (LEMMA "antiunif_completeness") (("" (INST -1 "c" "_") (("" (POSTPONE) NIL NIL)) NIL)) NIL)) NIL) NIL SHOSTAK))