(find_linear_modular (c_TCC1 0 (c_TCC1-1 nil 3260646926 3260647883 ("" (subtype-tcc) nil nil) proved-complete ((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) (>= const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil)) 119 80 nil shostak)) (c_TCC2 0 (c_TCC2-1 nil 3260646926 3260647883 ("" (termination-tcc) nil nil) proved-complete nil 11 10 nil shostak)) (constants 0 (constants-1 nil 3260646956 3260720680 ("" (induct "T") (("1" (grind) nil nil) ("2" (grind) nil nil)) nil) proved ((t const-decl "C" find_linear_modular nil) (L1 const-decl "C" find_linear_modular nil) (L2 const-decl "C" find_linear_modular nil) (L3 const-decl "C" find_linear_modular nil) (L4 const-decl "C" find_linear_modular nil) (L5 const-decl "C" find_linear_modular nil) (L6 const-decl "C" find_linear_modular nil) (L7 const-decl "C" find_linear_modular nil) (L8 const-decl "C" find_linear_modular nil) (NOT const-decl "[bool -> bool]" booleans nil) (c def-decl "C" find_linear_modular nil) (nat_induction formula-decl nil naturalnumbers nil) (invar_constants const-decl "bool" find_linear_modular nil) (C type-eq-decl nil find_linear_modular nil) (PCt type-decl nil find_linear_modular nil) (integer nonempty-type-from-decl nil integers nil) (pred type-eq-decl nil defined_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) 29376 980 t nil)) (invar_step 0 (invar_step-1 nil 3260646993 3260721161 ("" (skolem-typepred) (("" (expand "t") (("" (case "c!1`PC=L1") (("1" (assert) (("1" (grind) nil nil)) nil) ("2" (case "c!1`PC=L2") (("1" (assert) (("1" (grind) nil nil)) nil) ("2" (case "c!1`PC=L3") (("1" (assert) (("1" (grind) nil nil)) nil) ("2" (case "c!1`PC=L4") (("1" (assert) (("1" (grind) nil nil)) nil) ("2" (case "c!1`PC=L5") (("1" (assert) (("1" (grind) nil nil)) nil) ("2" (case "c!1`PC=L6") (("1" (assert) (("1" (expand "invar") (("1" (skolem-typepred) (("1" (expand "L6") (("1" (inst - "j!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (case "c!1`PC=L7") (("1" (assert) (("1" (grind) nil nil)) nil) ("2" (case "c!1`PC=L8") (("1" (assert) (("1" (grind) nil nil)) nil) ("2" (case "c!1`PC=LEND") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((t const-decl "C" find_linear_modular nil) (L2? adt-recognizer-decl "[PCt -> boolean]" find_linear_modular nil) (L2 adt-constructor-decl "(L2?)" find_linear_modular nil) (L2 const-decl "C" find_linear_modular nil) (/= const-decl "boolean" notequal nil) (L4? adt-recognizer-decl "[PCt -> boolean]" find_linear_modular nil) (L4 adt-constructor-decl "(L4?)" find_linear_modular nil) (L4 const-decl "C" find_linear_modular nil) (L6? adt-recognizer-decl "[PCt -> boolean]" find_linear_modular nil) (L6 adt-constructor-decl "(L6?)" find_linear_modular nil) (j!1 skolem-const-decl "below(L6(c!1)`i)" find_linear_modular nil) (L6 const-decl "C" find_linear_modular nil) (L7? adt-recognizer-decl "[PCt -> boolean]" find_linear_modular nil) (L7 adt-constructor-decl "(L7?)" find_linear_modular nil) (L7 const-decl "C" find_linear_modular nil) (LEND? adt-recognizer-decl "[PCt -> boolean]" find_linear_modular nil) (LEND adt-constructor-decl "(LEND?)" find_linear_modular nil) (L8 const-decl "C" find_linear_modular nil) (L8 adt-constructor-decl "(L8?)" find_linear_modular nil) (L8? adt-recognizer-decl "[PCt -> boolean]" find_linear_modular nil) (L5 const-decl "C" find_linear_modular nil) (c!1 skolem-const-decl "{c: C | invar(c)}" find_linear_modular nil) (L5 adt-constructor-decl "(L5?)" find_linear_modular nil) (L5? adt-recognizer-decl "[PCt -> boolean]" find_linear_modular nil) (L3 const-decl "C" find_linear_modular 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) (< const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (below type-eq-decl nil naturalnumbers nil) (L3 adt-constructor-decl "(L3?)" find_linear_modular nil) (L3? adt-recognizer-decl "[PCt -> boolean]" find_linear_modular nil) (L1 const-decl "C" find_linear_modular nil) (= const-decl "[T, T -> boolean]" equalities nil) (L1? adt-recognizer-decl "[PCt -> boolean]" find_linear_modular nil) (L1 adt-constructor-decl "(L1?)" find_linear_modular nil) (invar const-decl "bool" find_linear_modular nil) (C type-eq-decl nil find_linear_modular nil) (PCt type-decl nil find_linear_modular nil) (integer nonempty-type-from-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) 426104 8200 t nil)) (invar_holds 0 (invar_holds-1 nil 3260647037 3260718388 ("" (induct "T") (("1" (grind) nil nil) ("2" (skolem-typepred) (("2" (flatten) (("2" (skolem-typepred) (("2" (inst?) (("2" (lemma "invar_step") (("2" (inst - "c(j!1, initial!1)") (("2" (expand "c" +) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((NOT const-decl "[bool -> bool]" booleans nil) (invar_step formula-decl nil find_linear_modular nil) (initial!1 skolem-const-decl "C" find_linear_modular nil) (j!1 skolem-const-decl "nat" find_linear_modular nil) (nat_induction formula-decl nil naturalnumbers nil) (c def-decl "C" find_linear_modular nil) (invar const-decl "bool" find_linear_modular nil) (C type-eq-decl nil find_linear_modular nil) (PCt type-decl nil find_linear_modular nil) (integer nonempty-type-from-decl nil integers nil) (pred type-eq-decl nil defined_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) 5409 1970 t nil)) (c_correct 0 (c_correct-1 nil 3260647129 3260718404 ("" (skolem-typepred) (("" (skolem-typepred) (("" (use "constants" ("initial" "initial!1" "T" "T!1")) (("" (expand "invar_constants") (("" (flatten) (("" (expand "correct_result") (("" (use "invar_holds" ("initial" "initial!1" "T" "T!1")) (("" (expand "invar") (("" (iff) (("" (split) (("1" (flatten) (("1" (assert) (("1" (skolem-typepred -2) (("1" (inst + "j!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) (("2" (skolem-typepred) (("2" (inst + "i!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (PCt type-decl nil find_linear_modular nil) (= const-decl "[T, T -> boolean]" equalities nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (integer nonempty-type-from-decl nil integers nil) (C type-eq-decl nil find_linear_modular nil) (c def-decl "C" find_linear_modular nil) (LEND? adt-recognizer-decl "[PCt -> boolean]" find_linear_modular nil) (LEND adt-constructor-decl "(LEND?)" find_linear_modular nil) (invar_constants const-decl "bool" find_linear_modular nil) (correct_result const-decl "bool" find_linear_modular nil) (invar const-decl "bool" find_linear_modular nil) (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (invar_holds formula-decl nil find_linear_modular nil) (constants formula-decl nil find_linear_modular nil)) 6719 4080 t nil)) (find_linear_correct 0 (find_linear_correct-1 nil 3260647389 3260647715 ("" (skolem-typepred) (("" (assert) (("" (decompose-equality) (("1" (expand "find_linear") (("1" (use "constants" ("initial" "c!1" "T" "epsilon! (T: nat): c(T, c!1)`PC = LEND")) (("1" (expand "invar_constants") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (expand "find_linear") (("2" (use "c_correct" ("initial" "c!1" "T" "epsilon! (T: nat): c(T, c!1)`PC = LEND")) (("1" (use "epsilon_ax[nat]") (("1" (use "termination") (("1" (assert) nil nil)) nil)) nil) ("2" (use "epsilon_ax[nat]") (("2" (assert) (("2" (use "termination") nil nil)) nil)) nil)) nil)) nil) ("3" (use "constants" ("initial" "c!1" "T" "epsilon! (T: nat): c(T, c!1)`PC = LEND")) (("3" (grind) nil nil)) nil) ("4" (use "constants" ("initial" "c!1" "T" "epsilon! (T: nat): c(T, c!1)`PC = LEND")) (("4" (grind) nil nil)) nil)) nil)) nil)) nil) proved-incomplete ((epsilon_ax formula-decl nil epsilons nil) (termination formula-decl nil find_linear_modular nil) (c_correct formula-decl nil find_linear_modular nil) (invar_constants const-decl "bool" find_linear_modular nil) (LEND adt-constructor-decl "(LEND?)" find_linear_modular nil) (LEND? adt-recognizer-decl "[PCt -> boolean]" find_linear_modular nil) (c def-decl "C" find_linear_modular nil) (= const-decl "[T, T -> boolean]" equalities nil) (epsilon const-decl "T" epsilons nil) (pred type-eq-decl nil defined_types 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) (constants formula-decl nil find_linear_modular nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (integer nonempty-type-from-decl nil integers nil) (PCt type-decl nil find_linear_modular nil) (bool nonempty-type-eq-decl nil booleans nil) (C type-eq-decl nil find_linear_modular nil) (correct_result const-decl "bool" find_linear_modular nil) (boolean nonempty-type-decl nil booleans nil) (find_linear const-decl "C" find_linear_modular nil)) 326293 12220 t shostak)))