(SID_2 (|Count_TCC1| 0 (|Count_TCC1-1| NIL 3444061012 3444485013 ("" (TERMINATION-TCC) NIL NIL) PROVED-COMPLETE ((<< ADT-DEF-DECL "(well_founded?[list])" |list_adt| NIL) (|int| NONEMPTY-TYPE-EQ-DECL NIL |integers| NIL) (|slist| TYPE-EQ-DECL NIL SID_2 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) (AND CONST-DECL "[bool, bool -> bool]" |booleans| NIL) NIL (|list| TYPE-DECL NIL |list_adt| NIL) (PRED TYPE-EQ-DECL NIL |defined_types| 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)) (|Count_lemma| 0 (|Count_lemma-1| NIL 3444068068 3444068260 ("" (SKOSIMP) (("" (EXPAND "Count" 1 2) (("" (LIFT-IF) (("" (CASE "j!1=k!1") (("1" (GROUND) NIL NIL) ("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL) UNCHECKED ((|Count| DEF-DECL "nat" SID_2 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) (|posint_plus_nnint_is_posint| APPLICATION-JUDGEMENT "posint" |integers| NIL) (|real_le_is_total_order| NAME-JUDGEMENT "(total_order?[real])" |real_props| NIL) (|nnint_plus_nnint_is_nnint| APPLICATION-JUDGEMENT "nonneg_int" |integers| NIL)) 4107 9 T SHOSTAK)) (|glist_TCC1| 0 (|glist_TCC1-1| NIL 3444485004 3444485089 ("" (SKOSIMP) (("" (EXPAND "Count") (("" (ASSERT) NIL NIL)) NIL)) NIL) UNFINISHED ((|Count| DEF-DECL "nat" SID_2 NIL) (|real_le_is_total_order| NAME-JUDGEMENT "(total_order?[real])" |real_props| NIL)) 2381 2 T NIL)) (S_TCC1 0 (S_TCC1-1 NIL 3444061012 3445269446 ("" (EXPAND "well_founded?") (("" (SKOLEM 1 "P") (("" (PROP) (("" (INST 1 "null") (("1" (INDUCT "x") (("1" (EXPAND "restrict") (("1" (ASSERT) NIL NIL)) NIL) ("2" (EXPAND "restrict") (("2" (ASSERT) NIL NIL)) NIL) ("3" (PROP) (("3" (EXPAND "restrict") (("3" (ASSERT) (("3" (EXPAND "<<") (("3" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("4" (SKOLEM 1 ("N" "L")) (("4" (PROP) (("1" (EXPAND "restrict" -3) (("1" (ASSERT) (("1" (EXPAND "<<" -3) (("1" (PROPAX) NIL NIL)) NIL)) NIL)) NIL) ("2" (HIDE -1 -2 -4 1) (("2" (EXPAND "restrict") (("2" (EXPAND "<<") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL) ("3" (HIDE -1 -2 -4 1) (("3" (EXPAND "restrict") (("3" (ASSERT) (("3" (EXPAND "<<") (("3" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("5" (EXPAND "restrict" -2) (("5" (EXPAND "<<") (("5" (PROPAX) NIL NIL)) NIL)) NIL)) NIL) ("2" (PROP) (("1" (SKOSIMP) (("1" (EXPAND "Count") (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (SKOSIMP) (("2" (POSTPONE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) UNFINISHED NIL 106347 213 T NIL)) (S_TCC2 0 (S_TCC2-1 NIL 3444061012 3444485014 ("" (SUBTYPE-TCC) NIL NIL) PROVED-INCOMPLETE ((|real_le_is_total_order| NAME-JUDGEMENT "(total_order?[real])" |real_props| NIL) (|glist| TYPE-EQ-DECL NIL SID_2 NIL) (|Count| DEF-DECL "nat" SID_2 NIL) (|nat| NONEMPTY-TYPE-EQ-DECL NIL |naturalnumbers| NIL) (>= CONST-DECL "bool" |reals| NIL) (<= CONST-DECL "bool" |reals| NIL) (|int| NONEMPTY-TYPE-EQ-DECL NIL |integers| NIL) (|slist| TYPE-EQ-DECL NIL SID_2 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) (AND CONST-DECL "[bool, bool -> bool]" |booleans| NIL) NIL (|list| TYPE-DECL NIL |list_adt| NIL) (PRED TYPE-EQ-DECL NIL |defined_types| 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)) 113 113 NIL NIL)) (S_TCC3 0 (S_TCC3-1 NIL 3444061012 3444485015 ("" (SUBTYPE-TCC) NIL NIL) UNFINISHED NIL 93 93 NIL NIL)) (|S_spec_a| 0 (|S_spec_a-1| NIL 3444061049 3445268351 ("" (INDUCT "l") (("1" (TYPEPRED "l!1") (("1" (PROPAX) NIL NIL)) NIL) ("2" (FLATTEN) (("2" (SKOLEM 1 "K") (("2" (GRIND) NIL NIL)) NIL)) NIL) ("3" (SKOLEM 1 ("J" "L")) (("3" (FLATTEN) (("3" (SKOLEM 1 "N") (("3" (EXPAND "Count" -2) (("3" (PROP) (("1" (EXPAND "S" 1) (("1" (LIFT-IF) (("1" (CASE "N=J") (("1" (ASSERT) NIL NIL) ("2" (ASSERT) (("2" (INST -1 "N") (("2" (CASE "cons?(S(N,L))") (("1" (ASSERT) NIL NIL) ("2" (ASSERT) (("2" (HIDE -1) (("2" (EXPAND "S" -2) (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOLEM 1 "M") (("2" (INST -1 "M") (("2" (CASE "J=M") (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) UNFINISHED ((|list| TYPE-DECL NIL |list_adt| NIL) (|bool| NONEMPTY-TYPE-EQ-DECL NIL |booleans| NIL) (PRED TYPE-EQ-DECL NIL |defined_types| NIL) (AND CONST-DECL "[bool, bool -> bool]" |booleans| NIL) (IMPLIES CONST-DECL "[bool, bool -> bool]" |booleans| NIL) (<= CONST-DECL "bool" |reals| NIL) (|slist| TYPE-EQ-DECL NIL SID_2 NIL) (>= CONST-DECL "bool" |reals| NIL) (|nat| NONEMPTY-TYPE-EQ-DECL NIL |naturalnumbers| NIL) (|Count| DEF-DECL "nat" SID_2 NIL) (|cons?| ADT-RECOGNIZER-DECL "[list -> boolean]" |list_adt| NIL) (|glist| TYPE-EQ-DECL NIL SID_2 NIL) (S DEF-DECL "glist" SID_2 NIL) (= CONST-DECL "[T, T -> boolean]" |equalities| NIL) (|car| ADT-ACCESSOR-DECL "[(cons?) -> T]" |list_adt| 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) (NOT CONST-DECL "[bool -> bool]" |booleans| NIL) (|nnint_plus_nnint_is_nnint| APPLICATION-JUDGEMENT "nonneg_int" |integers| NIL) (|real_le_is_total_order| NAME-JUDGEMENT "(total_order?[real])" |real_props| NIL)) 1250 0 T SHOSTAK)) (D_TCC1 0 (D_TCC1-1 NIL 3444061012 3444485016 ("" (INDUCT "l") (("1" (TYPEPRED "l!1") (("1" (PROPAX) NIL NIL)) NIL) ("2" (PROP) (("2" (COMMENT "null is never equal to cons(,), so I suspect GRIND prove this subgoal") (("2" (GRIND) NIL ";;; null is never equal to cons(,), so I suspect GRIND prove this subgoal")) NIL)) NIL) ("3" (SKOLEM 1 ("K" "L")) (("3" (PROP) (("1" (SKOLEM 1 ("N" "M" "TL")) (("1" (PROP) (("1" (GROUND) (("1" (INST -1 "M" "N" "TL") (("1" (SPLIT -1) (("1" (PROPAX) NIL NIL) ("2" (SKOLEM 2 "K_1") (("2" (INST-CP -1 "K_1") (("2" (EXPAND "Count" -2) (("2" (CASE "K=K_1") (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("3" (SKOLEM 2 "K_1") (("3" (INST -1 "K_1") (("3" (REPLACE -3 -1) (("3" (EXPAND "Count" -1) (("3" (GROUND) (("3" (LIFT-IF -1) (("3" (CASE "M = K_1") (("1" (GROUND) NIL NIL) ("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOLEM 2 ("N" "M" "TL")) (("2" (PROP) (("2" (SKOLEM 2 "K_1") (("2" (INST -1 "K_1") (("2" (REPLACE -3 -1) (("2" (EXPAND "Count" -1) (("2" (CASE "M=K_1") (("1" (GROUND) NIL NIL) ("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) PROVED-INCOMPLETE ((|posint_plus_nnint_is_posint| APPLICATION-JUDGEMENT "posint" |integers| NIL) (|nnint_plus_nnint_is_nnint| APPLICATION-JUDGEMENT "nonneg_int" |integers| NIL) (|real_le_is_total_order| NAME-JUDGEMENT "(total_order?[real])" |real_props| NIL) (NOT CONST-DECL "[bool -> bool]" |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) (|list_induction| FORMULA-DECL NIL |list_adt| NIL) (|cons| ADT-CONSTRUCTOR-DECL "[[T, list] -> (cons?)]" |list_adt| NIL) (|cons?| ADT-RECOGNIZER-DECL "[list -> boolean]" |list_adt| NIL) (= CONST-DECL "[T, T -> boolean]" |equalities| NIL) (|Count| DEF-DECL "nat" SID_2 NIL) (|nat| NONEMPTY-TYPE-EQ-DECL NIL |naturalnumbers| NIL) (>= CONST-DECL "bool" |reals| NIL) (|slist| TYPE-EQ-DECL NIL SID_2 NIL) (<= CONST-DECL "bool" |reals| NIL) (IMPLIES CONST-DECL "[bool, bool -> bool]" |booleans| NIL) (AND CONST-DECL "[bool, bool -> bool]" |booleans| NIL) NIL (PRED TYPE-EQ-DECL NIL |defined_types| NIL) (|bool| NONEMPTY-TYPE-EQ-DECL NIL |booleans| NIL) (|list| TYPE-DECL NIL |list_adt| NIL) (|glist| TYPE-EQ-DECL NIL SID_2 NIL)) 76 76 T NIL)) (D_TCC2 0 (D_TCC2-1 NIL 3444061012 3444485017 ("" (INDUCT "l") (("1" (TYPEPRED "l!1") (("1" (PROPAX) NIL NIL)) NIL) ("2" (PROP) (("2" (SKOSIMP) (("2" (ASSERT) NIL NIL)) NIL)) NIL) ("3" (SKOLEM 1 ("K" "L")) (("3" (PROP) (("1" (SKOLEM 1 ("N" "M" "TL")) (("1" (PROP) (("1" (SKOLEM 2 "K_1") (("1" (INST -1 "_" "_" "TL") (("1" (INST -2 "K_1") (("1" (REPLACE -3 -2) (("1" (EXPAND "Count" -2) (("1" (CASE "M=K_1") (("1" (GROUND) NIL NIL) ("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (SKOSIMP) (("2" (INST?) (("2" (EXPAND "Count" -1) (("2" (LIFT-IF) (("2" (CASE "K=k!1") (("1" (GROUND) NIL NIL) ("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) PROVED-INCOMPLETE ((|posint_plus_nnint_is_posint| APPLICATION-JUDGEMENT "posint" |integers| NIL) (|real_le_is_total_order| NAME-JUDGEMENT "(total_order?[real])" |real_props| NIL) (|nnint_plus_nnint_is_nnint| APPLICATION-JUDGEMENT "nonneg_int" |integers| 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) (|cons| ADT-CONSTRUCTOR-DECL "[[T, list] -> (cons?)]" |list_adt| NIL) (|cons?| ADT-RECOGNIZER-DECL "[list -> boolean]" |list_adt| NIL) (= CONST-DECL "[T, T -> boolean]" |equalities| NIL) (NOT CONST-DECL "[bool -> bool]" |booleans| NIL) (|Count| DEF-DECL "nat" SID_2 NIL) (|nat| NONEMPTY-TYPE-EQ-DECL NIL |naturalnumbers| NIL) (>= CONST-DECL "bool" |reals| NIL) (|slist| TYPE-EQ-DECL NIL SID_2 NIL) (<= CONST-DECL "bool" |reals| NIL) (IMPLIES CONST-DECL "[bool, bool -> bool]" |booleans| NIL) (AND CONST-DECL "[bool, bool -> bool]" |booleans| NIL) NIL (PRED TYPE-EQ-DECL NIL |defined_types| NIL) (|bool| NONEMPTY-TYPE-EQ-DECL NIL |booleans| NIL) (|list| TYPE-DECL NIL |list_adt| NIL) (|glist| TYPE-EQ-DECL NIL SID_2 NIL)) 123 124 T NIL)) (D_TCC3 0 (D_TCC3-1 NIL 3444061012 3444485017 ("" (TERMINATION-TCC) NIL NIL) PROVED-INCOMPLETE ((|restrict| CONST-DECL "R" |restrict| NIL) (<< ADT-DEF-DECL "(well_founded?[list])" |list_adt| NIL) (|glist| TYPE-EQ-DECL NIL SID_2 NIL) (|Count| DEF-DECL "nat" SID_2 NIL) (|nat| NONEMPTY-TYPE-EQ-DECL NIL |naturalnumbers| NIL) (>= CONST-DECL "bool" |reals| NIL) (<= CONST-DECL "bool" |reals| NIL) (|slist| TYPE-EQ-DECL NIL SID_2 NIL) (AND CONST-DECL "[bool, bool -> bool]" |booleans| NIL) 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)) 12 12 NIL NIL)) (D_TCC4 0 (D_TCC4-1 NIL 3444061012 3444485019 ("" (SUBTYPE-TCC) NIL NIL) UNFINISHED NIL 134 134 NIL NIL)) (|SD_spec_a| 0 (|SD_spec_a-1| NIL 3444068861 3444069518 ("" (INDUCT "l") (("1" (HIDE 2) (("1" (TYPEPRED "l!1") (("1" (PROPAX) NIL NIL)) NIL)) NIL) ("2" (PROP) (("2" (SKOSIMP) (("2" (AUTO-REWRITE "S" "D") (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL) ("3" (SKOLEM 1 ("K" "L")) (("3" (PROP) (("1" (SKOSIMP) (("1" (EXPAND "D" 1) (("1" (LIFT-IF) (("1" (CASE "K=k!1") (("1" (ASSERT) (("1" (POSTPONE) NIL NIL)) NIL) ("2" (POSTPONE) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (POSTPONE) NIL NIL)) NIL)) NIL)) NIL) UNFINISHED NIL 23536 36 T SHOSTAK)) (I_TCC1 0 (I_TCC1-1 NIL 3444061012 3444485020 ("" (SUBTYPE-TCC) NIL NIL) UNFINISHED NIL 90 90 NIL NIL)) (|SI_spec_a_TCC1| 0 (|SI_spec_a_TCC1-1| NIL 3444061012 3444485021 ("" (SUBTYPE-TCC) NIL NIL) UNFINISHED NIL 88 88 NIL NIL)) (|SI_spec_a| 0 (|SI_spec_a-1| NIL 3444068275 3444068582 ("" (INDUCT "l") (("1" (SKOLEM 2 "K") (("1" (EXPAND "I" 2) (("1" (EXPAND "S" 2) (("1" (PROPAX) NIL NIL)) NIL)) NIL)) NIL) ("2" (PROP) (("2" (SKOSIMP) (("2" (AUTO-REWRITE "S" "I") (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL) ("3" (SKOLEM 1 ("K" "L")) (("3" (PROP) (("1" (SKOLEM 1 "J") (("1" (EXPAND "I" 1) (("1" (EXPAND "S" 1) (("1" (PROPAX) NIL NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP) (("2" (INST?) (("2" (EXPAND "Count" -1) (("2" (GROUND) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("4" (SKOLEM 1 "L") (("4" (PROP) (("4" (SKOLEM 1 "J") (("4" (AUTO-REWRITE "S" "I") (("4" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) UNCHECKED ((D DEF-DECL "glist" SID_2 NIL) (|nnint_plus_nnint_is_nnint| APPLICATION-JUDGEMENT "nonneg_int" |integers| NIL) (|real_le_is_total_order| NAME-JUDGEMENT "(total_order?[real])" |real_props| 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) (|list| TYPE-DECL NIL |list_adt| NIL) (|bool| NONEMPTY-TYPE-EQ-DECL NIL |booleans| NIL) (PRED TYPE-EQ-DECL NIL |defined_types| NIL) (AND CONST-DECL "[bool, bool -> bool]" |booleans| NIL) (IMPLIES CONST-DECL "[bool, bool -> bool]" |booleans| NIL) (<= CONST-DECL "bool" |reals| NIL) (|slist| TYPE-EQ-DECL NIL SID_2 NIL) (>= CONST-DECL "bool" |reals| NIL) (|nat| NONEMPTY-TYPE-EQ-DECL NIL |naturalnumbers| NIL) (|Count| DEF-DECL "nat" SID_2 NIL) (|cons?| ADT-RECOGNIZER-DECL "[list -> boolean]" |list_adt| NIL) (|glist| TYPE-EQ-DECL NIL SID_2 NIL) (S DEF-DECL "glist" SID_2 NIL) (I CONST-DECL "glist" SID_2 NIL) (|car| ADT-ACCESSOR-DECL "[(cons?) -> T]" |list_adt| NIL) (= CONST-DECL "[T, T -> boolean]" |equalities| NIL)) 30689 125 T SHOSTAK)) (|SID_spec_b_TCC1| 0 (|SID_spec_b_TCC1-1| NIL 3444061012 3444485021 ("" (SUBTYPE-TCC) NIL NIL) UNFINISHED NIL 91 92 NIL NIL)))