| products/sources/formale Sprachen/PVS/Sturm/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: clear_denominators.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(remainder_sequence
(is_neg_remainder_list?_TCC1 0 (is_neg_remainder_list?_TCC1-1 nil 3593783802 ("" (subtype-tcc) 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) (/= const-decl "boolean" notequal 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) (list type-decl nil list_adt 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) (int_minus_int_is_int application-judgement "int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (is_neg_remainder_list?_TCC2 0 (is_neg_remainder_list?_TCC2-1 nil 3593783802 ("" (subtype-tcc) 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) (/= const-decl "boolean" notequal 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) (list type-decl nil list_adt 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) (int_minus_int_is_int application-judgement "int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (is_neg_remainder_list?_TCC3 0 (is_neg_remainder_list?_TCC3-1 nil 3593783802 ("" (subtype-tcc) 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) (/= const-decl "boolean" notequal 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) (list type-decl nil list_adt 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) (listn_0 name-judgement "listn[real](0)" polynomial_division nil) (listn_0 name-judgement "listn[int](0)" polynomial_pseudo_divide nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil)) nil)) (is_neg_remainder_list?_TCC4 0 (is_neg_remainder_list?_TCC4-1 nil 3593783802 ("" (subtype-tcc) 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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (list type-decl nil list_adt 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) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (/= const-decl "boolean" notequal nil)) nil)) (is_neg_remainder_list?_TCC5 0 (is_neg_remainder_list?_TCC5-1 nil 3593783802 ("" (subtype-tcc) nil nil) ((bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (list type-decl nil list_adt 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) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (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) (array2list const-decl "{l: listn(n) | FORALL (i: below(n)): a(i) = nth(l, i)}" array2list "structures/") (/= const-decl "boolean" notequal nil)) nil)) (is_neg_remainder_list?_TCC6 0 (is_neg_remainder_list?_TCC6-1 nil 3593783802 ("" (skeep) (("" (assert) (("" (skeep) (("" (skeep) (("" (inst-cp - "1+j" "2+j") (("" (assert) (("" (assert) (("" (inst-cp - "j" "1+j") (("" (assert) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil)) nil)) (is_neg_remainder_list?_TCC7 0 (is_neg_remainder_list?_TCC7-1 nil 3593783802 ("" (skeep) (("" (skeep) (("" (skeep) (("" (skeep) (("" (skeep) (("" (inst - "j" "1+j") (("" (assert) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nnint_plus_posint_is_posint application-judgement "posint" integers nil) (listn_0 name-judgement "listn[real](0)" polynomial_division nil) (listn_0 name-judgement "listn[int](0)" polynomial_pseudo_divide nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields 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) (posint_plus_nnint_is_posint application-judgement "posint" integers nil)) nil)) (is_neg_remainder_list?_TCC8 0 (is_neg_remainder_list?_TCC8-1 nil 3593783802 ("" (skeep) (("" (skeep) (("" (skeep) (("" (skeep) (("" (skeep) (("" (inst - "j" "j+1") (("" (assert) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nnint_plus_posint_is_posint application-judgement "posint" integers nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (listn_0 name-judgement "listn[int](0)" polynomial_pseudo_divide nil) (listn_0 name-judgement "listn[real](0)" polynomial_division nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (is_neg_remainder_list?_TCC9 0 (is_neg_remainder_list?_TCC9-1 nil 3593783802 ("" (skeep) (("" (skeep) (("" (skeep) (("" (skeep) (("" (skeep) (("" (skeep) (("" (assert) (("" (inst - "1+j") (("" (assert) (("" (assert) (("" (replace -9 :dir rl) (("" (lemma "list2array_sound[int]") (("" (inst - "nth(curr,1+j)" "0" "nlittle") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (listn_0 name-judgement "listn[int](0)" polynomial_pseudo_divide nil) (listn_0 name-judgement "listn[real](0)" polynomial_division nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil)) nil)) (is_neg_remainder_list?_TCC10 0 (is_neg_remainder_list?_TCC10-1 nil 3593783802 ("" (skeep) (("" (skeep) (("" (skeep) (("" (skeep) (("" (skeep) (("" (skeep) (("" (assert) (("" (lemma "list2array_sound[int]") (("" (inst - "nth(curr,1+j)" "0" _) (("" (assert) (("" (replace -9) (("" (inst - "nlittle") (("" (assert) (("" (replace -1) (("" (typepred "curr") (("" (inst - "1+j") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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) (list2array_sound formula-decl nil array2list "structures/") (NOT const-decl "[bool -> bool]" booleans nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (nth def-decl "T" list_props nil) (below type-eq-decl nil nat_types nil) (length def-decl "nat" list_props nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals 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) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (listn_0 name-judgement "listn[int](0)" polynomial_pseudo_divide nil) (listn_0 name-judgement "listn[real](0)" polynomial_division nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (is_neg_remainder_list?_TCC11 0 (is_neg_remainder_list?_TCC11-1 nil 3619193861 ("" (skeep) (("" (skeep) (("" (skeep) (("" (skeep) (("" (skeep) (("" (skeep) (("" (assert) (("" (inst - "1+j" "2+j") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((posint_plus_nnint_is_posint application-judgement "posint" integers nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (listn_0 name-judgement "listn[int](0)" polynomial_pseudo_divide nil) (listn_0 name-judgement "listn[real](0)" polynomial_division nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (compute_remainder_seq_TCC1 0 (compute_remainder_seq_TCC1-1 nil 3593536601 ("" (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) (/= const-decl "boolean" notequal 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) (list type-decl nil list_adt 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) (is_neg_remainder_list? const-decl "bool" remainder_sequence nil) (array2list_it def-decl "{l: listn(n - i) | FORALL (j: subrange(i, n - 1)): a(j) = nth(l, j - i)}" array2list "structures/") (array2list const-decl "{l: listn(n) | FORALL (i: below(n)): a(i) = nth(l, i)}" array2list "structures/") (nth def-decl "T" list_props nil) (mod const-decl "{k | abs(k) < abs(j)}" mod nil) (primitize_list const-decl "list[int]" gcd_coeff nil) (nonzero_version const-decl "list[int]" gcd_coeff nil) (adjusted_remainder const-decl "list[int]" polynomial_pseudo_divide nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (even_times_int_is_even application-judgement "even_int" integers nil) (minus_nzint_is_nzint application-judgement "nzint" integers nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (listn_0 name-judgement "listn[real](0)" polynomial_division nil) (listn_0 name-judgement "listn[int](0)" polynomial_pseudo_divide nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil)) nil)) (compute_remainder_seq_TCC2 0 (compute_remainder_seq_TCC2-1 nil 3593536601 ("" (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) (/= const-decl "boolean" notequal 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) (list type-decl nil list_adt 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) (is_neg_remainder_list? const-decl "bool" remainder_sequence nil) (array2list_it def-decl "{l: listn(n - i) | FORALL (j: subrange(i, n - 1)): a(j) = nth(l, j - i)}" array2list "structures/") (array2list const-decl "{l: listn(n) | FORALL (i: below(n)): a(i) = nth(l, i)}" array2list "structures/") (nth def-decl "T" list_props nil) (mod const-decl "{k | abs(k) < abs(j)}" mod nil) (primitize_list const-decl "list[int]" gcd_coeff nil) (nonzero_version const-decl "list[int]" gcd_coeff nil) (adjusted_remainder const-decl "list[int]" polynomial_pseudo_divide nil) (length def-decl "nat" list_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (even_times_int_is_even application-judgement "even_int" integers nil) (minus_nzint_is_nzint application-judgement "nzint" integers nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (listn_0 name-judgement "listn[real](0)" polynomial_division nil) (listn_0 name-judgement "listn[int](0)" polynomial_pseudo_divide nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil)) nil)) (compute_remainder_seq_TCC3 0 (compute_remainder_seq_TCC3-1 nil 3593536601 ("" (skeep) (("" (grind) nil nil)) nil) ((posint_plus_nnint_is_posint application-judgement "posint" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (length def-decl "nat" list_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil)) nil)) (compute_remainder_seq_TCC4 0 (compute_remainder_seq_TCC4-1 nil 3593536601 ("" (skeep) (("" (case "NOT curr = null") (("1" (hide 2) (("1" (grind) nil nil)) nil) ("2" (replace -1) (("2" (expand "is_neg_remainder_list?") (("2" (split) (("1" (skeep) (("1" (case "NOT (icurr = 0 AND jcurr = 1)") (("1" (expand "length" -2) (("1" (expand "length" -2) (("1" (assert) nil nil)) nil)) nil) ("2" (flatten) (("2" (replaces -1) (("2" (replaces -1) (("2" (assert) (("2" (expand "nth" 1) (("2" (expand "nth" 1) (("2" (assert) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skeep) (("2" (expand "length" -1) (("2" (expand "length" -1) (("2" (assert) (("2" (expand "nth" -3 2) (("2" (expand "nth" -3 2) (("2" (expand "nth" -3 2) (("2" (expand "nth" -3 2) (("2" (lift-if) (("2" (split -) (("1" (flatten) (("1" (typepred "array2list[int](1+m)(h)") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) (("2" (typepred "array2list[int](1+n)(g)") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (flatten) (("3" (expand "nth" 1 1) (("3" (lift-if) (("3" (split 1) (("1" (flatten) (("1" (grind) nil nil)) nil) ("2" (flatten) (("2" (expand "length" 2) (("2" (expand "length" 2) (("2" (assert) (("2" (expand "nth" 2) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (flatten) (("4" (expand "length" +) (("4" (expand "length" +) (("4" (assert) (("4" (expand "nth" 1) (("4" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("5" (skeep) (("5" (expand "length" -1) (("5" (expand "length" -1) (("5" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((null adt-constructor-decl "(null?)" list_adt nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (is_neg_remainder_list? const-decl "bool" remainder_sequence nil) (/= const-decl "boolean" notequal nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (list type-decl nil list_adt 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) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (length def-decl "nat" list_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (below type-eq-decl nil nat_types nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (listn type-eq-decl nil listn "structures/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nth def-decl "T" list_props nil) (array2list_it def-decl "{l: listn(n - i) | FORALL (j: subrange(i, n - 1)): a(j) = nth(l, j - i)}" array2list "structures/") (array2list const-decl "{l: listn(n) | FORALL (i: below(n)): a(i) = nth(l, i)}" array2list "structures/") (listn_0 name-judgement "listn[int](0)" polynomial_pseudo_divide nil) (listn_0 name-judgement "listn[real](0)" polynomial_division nil) (length_null formula-decl nil more_list_props "structures/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (compute_remainder_seq_TCC5 0 (compute_remainder_seq_TCC5-1 nil 3593536601 ("" (skeep) (("" (case "NOT curr = null") (("1" (hide 2) (("1" (grind) nil nil)) nil) ("2" (replace -1) (("2" (assert) (("2" (expand "length" 1 1) (("2" (expand "length" 1 1) (("2" (expand "length" 1 1) (("2" (expand "length" 1 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((null adt-constructor-decl "(null?)" list_adt nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (is_neg_remainder_list? const-decl "bool" remainder_sequence nil) (/= const-decl "boolean" notequal nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (list type-decl nil list_adt 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) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (length def-decl "nat" list_props nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (listn_0 name-judgement "listn[real](0)" polynomial_division nil) (listn_0 name-judgement "listn[int](0)" polynomial_pseudo_divide nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (length_null formula-decl nil more_list_props "structures/")) nil)) (compute_remainder_seq_TCC6 0 (compute_remainder_seq_TCC6-2 nil 3619190757 ("" (skeep) (("" (typepred "curr") (("" (hide -1) (("" (expand "is_neg_remainder_list?" + :assert? none) (("" (split +) (("1" (assert) (("1" (skeep) (("1" (case "NOT (jcurr = 1 AND icurr = 0)") (("1" (expand "length" -2) (("1" (assert) nil nil)) nil) ("2" (flatten) (("2" (replaces -1) (("2" (replaces -1) (("2" (expand "length" -2) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skeep) (("2" (assert) (("2" (flatten) (("2" (case "NOT (icurr = 0 OR icurr = 1)") (("1" (expand "length" -1) (("1" (ground) nil nil)) nil) ("2" (split -1) (("1" (replaces -1) (("1" (assert) (("1" (expand "nth" -3 2) (("1" (expand "nth" -3 2) (("1" (typepred "array2list[int](1 + m)(h)") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (expand "nth" -4 2) (("2" (assert) (("2" (expand "nth" -4 3) (("2" (assert) (("2" (expand "is_neg_remainder_list?") (("2" (flatten) (("2" (replace -8 :dir rl) (("2" (replace -7) (("2" (assert) (("2" (replace -6) (("2" (typepred "array2list[int](1 + n)(g)") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (flatten) (("3" (expand "length" 1) (("3" (expand "nth" 1) (("3" (assert) (("3" (expand "is_neg_remainder_list?") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("4" (flatten) (("4" (expand "length" 1) (("4" (expand "nth" 1) (("4" (assert) nil nil)) nil)) nil)) nil) ("5" (skeep) (("5" (skoletin 1) (("5" (skoletin 1) (("5" (skoletin 1) (("5" (skoletin 1) (("5" (expand "length" -5) (("5" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((is_neg_remainder_list? const-decl "bool" remainder_sequence nil) (/= const-decl "boolean" notequal nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt 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) (adjusted_remainder const-decl "list[int]" polynomial_pseudo_divide nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (list2array def-decl "T" array2list "structures/") (bijective? const-decl "bool" functions nil) (id const-decl "(bijective?[T, T])" identity nil) (TRUE const-decl "bool" booleans nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (array2list const-decl "{l: listn(n) | FORALL (i: below(n)): a(i) = nth(l, i)}" array2list "structures/") (below type-eq-decl nil nat_types nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (listn type-eq-decl nil listn "structures/") (nth def-decl "T" list_props nil) (odd_minus_odd_is_even application-judgement "even_int" integers nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (listn_0 name-judgement "listn[int](0)" polynomial_pseudo_divide nil) (listn_0 name-judgement "listn[real](0)" polynomial_division nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (= const-decl "[T, T -> boolean]" equalities nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (length def-decl "nat" list_props nil)) nil) (compute_remainder_seq_TCC6-1 nil 3593536601 ("" (skeep) (("" (assert) (("" (case "NOT curr = null") (("1" (hide 2) (("1" (grind) nil nil)) nil) ("2" (replace -1) (("2" (expand "is_neg_remainder_list?") (("2" (split) (("1" (skeep) (("1" (case "NOT (icurr = 0 AND jcurr = 1)") (("1" (hide 2) (("1" (hide 2) (("1" (expand "length") (("1" (expand "length") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (replaces -1) (("2" (replaces -1) (("2" (assert) (("2" (expand "length" 1 1) (("2" (expand "length" 1 1) (("2" (expand "length" 1 1) (("2" (expand "length" 1 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skeep) (("2" (expand "length" -1 1) (("2" (expand "length" -1 1) (("2" (assert) (("2" (expand "nth" -3 2) (("2" (expand "nth" -3 2) (("2" (expand "nth" -3 2) (("2" (expand "nth" -3 2) (("2" (lift-if) (("2" (split) (("1" (flatten) (("1" (typepred "array2list[int](m + 1)(h)") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (flatten) (("2" (typepred "array2list[int](1+n)(g)") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (flatten) (("3" (expand "nth" 1 1) (("3" (expand "length" 1 1) (("3" (expand "length" 1 1) (("3" (assert) (("3" (expand "nth" 1 1) (("3" (expand "length" 1 1) (("3" (expand "length" 1 1) (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (flatten) (("4" (expand "length" + 1) (("4" (expand "length" + 1) (("4" (assert) (("4" (expand "nth" 1) (("4" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("5" (skeep) (("5" (expand "length" -1 1) (("5" (expand "length" -1 1) (("5" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((listn_0 name-judgement "listn[int](0)" gcd_coeff nil) (length_null formula-decl nil more_list_props "structures/") (listn type-eq-decl nil listn "structures/") (array2list const-decl "{l: listn(n) | FORALL (i: below(n)): a(i) = nth(l, i)}" array2list "structures/") (list type-decl nil list_adt nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (null adt-constructor-decl "(null?)" list_adt nil)) nil)) (compute_remainder_seq_TCC7 0 (compute_remainder_seq_TCC7-1 nil 3593536601 ("" (skeep) (("" (assert) (("" (expand "length" + 1) (("" (expand "length" + 1) (("" (assert) (("" (lift-if) (("" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nnint_plus_posint_is_posint application-judgement "posint" integers nil) (listn_0 name-judgement "listn[real](0)" polynomial_division nil) (listn_0 name-judgement "listn[int](0)" polynomial_pseudo_divide nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (length def-decl "nat" list_props nil)) nil)) (compute_remainder_seq_TCC8 0 (compute_remainder_seq_TCC8-1 nil 3593536601 ("" (skeep) (("" (typepred "curr") (("" (hide -1) (("" (expand "is_neg_remainder_list?" + :assert? none) (("" (split +) (("1" (assert) (("1" (skeep) (("1" (case "NOT (jcurr = 1 AND icurr = 0)") (("1" (expand "length" -2) (("1" (assert) nil nil)) nil) ("2" (flatten) (("2" (replaces -1) (("2" (replaces -1) (("2" (hide (-1 -2)) (("2" (assert) (("2" (expand "length" 1) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skeep) (("2" (assert) (("2" (flatten) (("2" (case "NOT (icurr = 0 OR icurr = 1)") (("1" (expand "length" -1) (("1" (ground) nil nil)) nil) ("2" (split -1) (("1" (replaces -1) (("1" (assert) (("1" (expand "nth" -3 2) (("1" (expand "nth" -3 2) (("1" (assert) (("1" (expand "is_neg_remainder_list?") (("1" (flatten) (("1" (typepred "array2list[int](1 + m)(h)") (("1" (replace -2) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (expand "nth" -4 2) (("2" (assert) (("2" (expand "nth" -4 3) (("2" (assert) (("2" (expand "is_neg_remainder_list?") (("2" (flatten) (("2" (assert) (("2" (replace -9 :dir rl) (("2" (replace -8) (("2" (assert) (("2" (replace -7) (("2" (assert) (("2" (typepred "array2list[int](1 + n)(g)") (("2" (replace -2) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (flatten) (("3" (expand "length" 1) (("3" (expand "nth" 1) (("3" (assert) (("3" (expand "is_neg_remainder_list?") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("4" (flatten) (("4" (expand "length" 1) (("4" (expand "nth" 1) (("4" (assert) nil nil)) nil)) nil)) nil) ("5" (skeep) (("5" (skoletin 1) (("5" (skoletin 1) (("5" (skoletin 1) (("5" (skoletin 1) (("5" (expand "length" -5) (("5" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((is_neg_remainder_list? const-decl "bool" remainder_sequence nil) (/= const-decl "boolean" notequal nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt 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) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (compute_remainder_seq_TCC9 0 (compute_remainder_seq_TCC9-1 nil 3593536601 ("" (skeep) (("" (assert) nil nil)) nil) ((real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (listn_0 name-judgement "listn[real](0)" polynomial_division nil) (listn_0 name-judgement "listn[int](0)" polynomial_pseudo_divide nil)) nil)) (compute_remainder_seq_TCC10 0 (compute_remainder_seq_TCC10-1 nil 3593538922 ("" (skeep) (("" (skeep) (("" (assert) nil nil)) nil)) nil) ((listn_0 name-judgement "listn[real](0)" polynomial_division nil) (listn_0 name-judgement "listn[int](0)" polynomial_pseudo_divide nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (compute_remainder_seq_TCC11 0 (compute_remainder_seq_TCC11-1 nil 3593538922 ("" (skeep*) (("" (assert) (("" (split +) (("1" (flatten) (("1" (lemma "list2array_sound[int]") (("1" (inst - "csplittle" "0" "newm") (("1" (assert) (("1" (typepred "curr") (("1" (hide -1) (("1" (expand "is_neg_remainder_list?") (("1" (flatten) (("1" (inst - "0") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "curr") (("2" (hide -1) (("2" (expand "is_neg_remainder_list?") (("2" (flatten) (("2" (inst - "0" "1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "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) (list2array_sound formula-decl nil array2list "structures/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (is_neg_remainder_list? const-decl "bool" remainder_sequence nil) (/= const-decl "boolean" notequal nil) (NOT const-decl "[bool -> bool]" booleans nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals 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) (listn_0 name-judgement "listn[int](0)" polynomial_pseudo_divide nil) (listn_0 name-judgement "listn[real](0)" polynomial_division nil)) nil)) (compute_remainder_seq_TCC12 0 (compute_remainder_seq_TCC12-1 nil 3593538922 ("" (skeep*) (("" (typepred "curr") (("" (hide -1) (("" (expand "is_neg_remainder_list?") (("" (flatten) (("" (assert) (("" (inst - "1") (("" (inst - "0" "1") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((is_neg_remainder_list? const-decl "bool" remainder_sequence nil) (/= const-decl "boolean" notequal nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt 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) (int_minus_int_is_int application-judgement "int" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (listn_0 name-judgement "listn[int](0)" polynomial_pseudo_divide nil) (listn_0 name-judgement "listn[real](0)" polynomial_division nil)) nil)) (compute_remainder_seq_TCC13 0 (compute_remainder_seq_TCC13-1 nil 3593784421 ("" (skeep*) (("" (case "NOT (newm>=0 AND newh(newm) /= 0)") (("1" (split) (("1" (assert) nil nil) ("2" (flatten) (("2" (replace -8 -1) (("2" (replace -7 -1) (("2" (replace -3 -1) (("2" (typepred "curr") (("2" (hide -1) (("2" (lemma "list2array_sound[int]") (("2" (inst?) (("1" (assert) (("1" (replaces -1) (("1" (expand "is_neg_remainder_list?" -1) (("1" (flatten) (("1" (inst - "0") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) (("2" (typepred "curr") (("2" (hide -1) (("2" (expand "is_neg_remainder_list?") (("2" (flatten) (("2" (split +) (("1" (skeep) (("1" (expand "length" -2) (("1" (expand "nth" 1) (("1" (lift-if) (("1" (lift-if) (("1" (assert) (("1" (split 1) (("1" (flatten) (("1" (lemma "adjusted_remainder_length") (("1" (inst?) (("1" (assert) (("1" (invoke (case "%1 < %2") (! -1 2) (! 1 2)) (("1" (assert) nil nil) ("2" (hide -1) (("2" (replace -16 1) (("2" (replace -11 1) (("2" (inst - "0" "jcurr-1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (inst - "0" "1") (("2" (assert) nil nil)) --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.78 Sekunden (vorverarbeitet) ¤ |
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
