(SID_1 (S_TCC1 0 (S_TCC1-1 NIL 3443960106 3444056792 ("" (TERMINATION-TCC) NIL NIL) PROVED ((<< ADT-DEF-DECL "(well_founded?[list])" |list_adt| NIL) (|slist| TYPE-EQ-DECL NIL SID_1 NIL) (AND CONST-DECL "[bool, bool -> bool]" |booleans| NIL) (|every| ADT-DEF-DECL "boolean" |list_adt| NIL) (|list| TYPE-DECL NIL |list_adt| NIL) (PRED TYPE-EQ-DECL NIL |defined_types| 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)) 31 31 NIL NIL)) (|SI_spec_a_TCC1| 0 (|SI_spec_a_TCC1-1| NIL 3443960106 3444056983 ("" (INDUCT-AND-SIMPLIFY "l") NIL NIL) PROVED ((|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) (|list_induction| FORMULA-DECL NIL |list_adt| NIL) (I CONST-DECL "slist" SID_1 NIL) (S DEF-DECL "slist" SID_1 NIL) (|cons?| ADT-RECOGNIZER-DECL "[list -> boolean]" |list_adt| NIL) (|slist| TYPE-EQ-DECL NIL SID_1 NIL) (AND CONST-DECL "[bool, bool -> bool]" |booleans| NIL) (|every| ADT-DEF-DECL "boolean" |list_adt| NIL) (PRED TYPE-EQ-DECL NIL |defined_types| NIL) (|bool| NONEMPTY-TYPE-EQ-DECL NIL |booleans| NIL) (|list| TYPE-DECL NIL |list_adt| NIL)) 11894 51 T NIL)) (|SI_spec_a| 0 (|SI_spec_a-1| NIL 3443960107 3444056793 ("" (SKOLEM 1 ("K" "_")) (("" (COMMENT "Induction is not needed here, but in later refinements it will b") (("" (INDUCT "l") (("1" (AUTO-REWRITE "I" "S") (("1" (ASSERT) NIL NIL)) NIL) ("2" (SKOLEM 1 ("J" "L")) (("2" (FLATTEN) (("2" (EXPAND "I" 1) (("2" (EXPAND "S" 1) (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("3" (COMMENT "This is a TCC subgoal generated by the term (car (S(k, I(k, l))). It could have been avoided by declaring I:(cons?[int])") (("3" (COMMENT "This is a TCC subgoal generated by the term (car (S(k, I(k, l))). It could have been avoided by declaring I:(cons?[int])") (("3" (HIDE 2) (("3" (SKOLEM 1 "L") (("3" (AUTO-REWRITE "S" "I") (("3" (ASSERT) NIL NIL)) NIL)) NIL)) ";;; This is a TCC subgoal generated by the term (car (S(k, I(k, l))). It could have been avoided by declaring I:(cons?[int])")) ";;; This is a TCC subgoal generated by the term (car (S(k, I(k, l))). It could have been avoided by declaring I:(cons?[int])")) NIL)) ";;; Induction is not needed here, but in later refinements it will b")) NIL)) NIL) PROVED ((|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) (|list_induction| FORMULA-DECL NIL |list_adt| NIL) (|list| TYPE-DECL NIL |list_adt| NIL) (|bool| NONEMPTY-TYPE-EQ-DECL NIL |booleans| NIL) (PRED TYPE-EQ-DECL NIL |defined_types| NIL) (|every| ADT-DEF-DECL "boolean" |list_adt| NIL) (AND CONST-DECL "[bool, bool -> bool]" |booleans| NIL) (|slist| TYPE-EQ-DECL NIL SID_1 NIL) (|cons?| ADT-RECOGNIZER-DECL "[list -> boolean]" |list_adt| NIL) (S DEF-DECL "slist" SID_1 NIL) (K SKOLEM-CONST-DECL "int" SID_1 NIL) (I CONST-DECL "slist" SID_1 NIL) (|car| ADT-ACCESSOR-DECL "[(cons?) -> T]" |list_adt| NIL) (= CONST-DECL "[T, T -> boolean]" |equalities| NIL)) 32 32 T SHOSTAK)) (|SI_spec_b| 0 (|SI_spec_b-1| NIL 3443960583 3444056793 ("" (SKOLEM 1 ("J" "K" "_")) (("" (INDUCT "l") (("1" (AUTO-REWRITE "S" "I") (("1" (ASSERT) (("1" (FLATTEN) (("1" (LIFT-IF) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOLEM 1 ("N" "L")) (("2" (FLATTEN) (("2" (SPLIT -1) (("1" (EXPAND "I" 2) (("1" (EXPAND "S" 2 2) (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (COMMENT "This subgoal is an artifact of the previous SPLIT. It is trivially true because [1] and [2] are contradictory.") (("2" (GROUND) NIL ";;; This subgoal is an artifact of the previous SPLIT. ;;; It is trivially true because [1] and [2] are contradictory.")) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) PROVED ((|list| TYPE-DECL NIL |list_adt| NIL) (|bool| NONEMPTY-TYPE-EQ-DECL NIL |booleans| NIL) (PRED TYPE-EQ-DECL NIL |defined_types| NIL) (|every| ADT-DEF-DECL "boolean" |list_adt| NIL) (AND CONST-DECL "[bool, bool -> bool]" |booleans| NIL) (|slist| TYPE-EQ-DECL NIL SID_1 NIL) (IMPLIES CONST-DECL "[bool, bool -> bool]" |booleans| NIL) (/= CONST-DECL "boolean" |notequal| NIL) (= CONST-DECL "[T, T -> boolean]" |equalities| NIL) (S DEF-DECL "slist" SID_1 NIL) (I CONST-DECL "slist" SID_1 NIL) (|list_induction| FORMULA-DECL NIL |list_adt| 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)) 12 13 T SHOSTAK)) (D_TCC1 0 (D_TCC1-1 NIL 3443960106 3444056794 ("" (TERMINATION-TCC) NIL NIL) PROVED ((<< ADT-DEF-DECL "(well_founded?[list])" |list_adt| NIL) (|slist| TYPE-EQ-DECL NIL SID_1 NIL) (AND CONST-DECL "[bool, bool -> bool]" |booleans| NIL) (|every| ADT-DEF-DECL "boolean" |list_adt| NIL) (|list| TYPE-DECL NIL |list_adt| NIL) (PRED TYPE-EQ-DECL NIL |defined_types| 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)) 28 28 NIL NIL)) (D_TCC2 0 (D_TCC2-1 NIL 3443960106 3444056794 ("" (TERMINATION-TCC) NIL NIL) PROVED ((<< ADT-DEF-DECL "(well_founded?[list])" |list_adt| NIL) (|slist| TYPE-EQ-DECL NIL SID_1 NIL) (AND CONST-DECL "[bool, bool -> bool]" |booleans| NIL) (|every| ADT-DEF-DECL "boolean" |list_adt| NIL) (|list| TYPE-DECL NIL |list_adt| NIL) (PRED TYPE-EQ-DECL NIL |defined_types| 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)) 11 10 NIL NIL)) (|SD_spec_a| 0 (|SD_spec_a-1| NIL 3443962018 3444056794 ("" (SKOLEM 1 ("K" "_")) (("" (INDUCT "l") (("1" (AUTO-REWRITE "S" "D") (("1" (ASSERT) NIL NIL)) NIL) ("2" (SKOLEM 1 ("J" "L")) (("2" (FLATTEN) (("2" (EXPAND "D" 1) (("2" (LIFT-IF) (("2" (CASE "J=K") (("1" (ASSERT) NIL NIL) ("2" (ASSERT) (("2" (EXPAND "S" 2) (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) PROVED ((|list| TYPE-DECL NIL |list_adt| NIL) (|bool| NONEMPTY-TYPE-EQ-DECL NIL |booleans| NIL) (PRED TYPE-EQ-DECL NIL |defined_types| NIL) (|every| ADT-DEF-DECL "boolean" |list_adt| NIL) (AND CONST-DECL "[bool, bool -> bool]" |booleans| NIL) (|slist| TYPE-EQ-DECL NIL SID_1 NIL) (|null?| ADT-RECOGNIZER-DECL "[list -> boolean]" |list_adt| NIL) (S DEF-DECL "slist" SID_1 NIL) (D DEF-DECL "slist" SID_1 NIL) (|list_induction| FORMULA-DECL NIL |list_adt| 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) (= CONST-DECL "[T, T -> boolean]" |equalities| NIL)) 31 30 T SHOSTAK)) (|SD_spec_b| 0 (|SD_spec_b-1| NIL 3443962174 3444057812 ("" (INDUCT "l") (("1" (GRIND) NIL NIL) ("2" (SKOLEM 1 ("K" "L")) (("2" (FLATTEN) (("2" (SKOLEM 1 ("N" "M")) (("2" (PROP) (("1" (EXPAND "S" -1) (("1" (CASE "M=K") (("1" (ASSERT) NIL NIL) ("2" (ASSERT) (("2" (EXPAND "D" 2) (("2" (ASSERT) (("2" (LIFT-IF) (("2" (CASE "K=N") (("1" (ASSERT) (("1" (INST -3 "N" "M") (("1" (GROUND) NIL NIL)) NIL)) NIL) ("2" (ASSERT) (("2" (EXPAND "S" 3) (("2" (INST -2 "N" "M") (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (EXPAND "D" -1) (("2" (LIFT-IF -1) (("2" (CASE "K=N") (("1" (ASSERT) (("1" (EXPAND "S" 1) (("1" (INST -3 "N" "M") (("1" (PROP) NIL NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) (("2" (EXPAND "S" -1) (("2" (CASE "M=K") (("1" (ASSERT) NIL NIL) ("2" (ASSERT) (("2" (EXPAND "S" 3) (("2" (INST -2 "N" "M") (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) PROVED ((= CONST-DECL "[T, T -> boolean]" |equalities| 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) (|list_induction| FORMULA-DECL NIL |list_adt| NIL) (D DEF-DECL "slist" SID_1 NIL) (S DEF-DECL "slist" SID_1 NIL) (|null?| ADT-RECOGNIZER-DECL "[list -> boolean]" |list_adt| NIL) (IFF CONST-DECL "[bool, bool -> bool]" |booleans| NIL) (/= CONST-DECL "boolean" |notequal| NIL) (IMPLIES CONST-DECL "[bool, bool -> bool]" |booleans| NIL) (|slist| TYPE-EQ-DECL NIL SID_1 NIL) (AND CONST-DECL "[bool, bool -> bool]" |booleans| NIL) (|every| ADT-DEF-DECL "boolean" |list_adt| NIL) (PRED TYPE-EQ-DECL NIL |defined_types| NIL) (|bool| NONEMPTY-TYPE-EQ-DECL NIL |booleans| NIL) (|list| TYPE-DECL NIL |list_adt| NIL)) 79353 67 T SHOSTAK)) (|SID_spec_b_TCC1| 0 (|SID_spec_b_TCC1-1| NIL 3444056792 3444056808 ("" (SUBTYPE-TCC) NIL NIL) UNFINISHED NIL 31 31 NIL NIL)))