| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/analysis/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 491 kB |
|
Impressum bounded_variation.prfSprache: Lisp |
|||||||||||||||
|
(bounded_variation (IMP_rs_partition_TCC1 0 (IMP_rs_partition_TCC1-2 nil 3511196898 ("" (lemma "connected_domain") (("" (propax) nil nil)) nil) ((connected_domain formula-decl nil bounded_variation nil)) nil) (IMP_rs_partition_TCC1-1 nil 3511191467 ("" (assuming-tcc) nil nil) nil nil)) (IMP_rs_partition_TCC2 0 (IMP_rs_partition_TCC2-1 nil 3511191467 ("" (lemma "not_one_element") (("" (propax) nil nil)) nil) ((not_one_element formula-decl nil bounded_variation nil)) nil)) (variation_on_TCC1 0 (variation_on_TCC1-1 nil 3491555814 ("" (subtype-tcc) nil nil) nil nil)) (variation_on_TCC2 0 (variation_on_TCC2-1 nil 3491555814 ("" (subtype-tcc) nil nil) nil nil)) (variation_on_TCC3 0 (variation_on_TCC3-1 nil 3491555814 ("" (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) (T_pred const-decl "[real -> boolean]" bounded_variation nil) (T formal-nonempty-subtype-decl nil bounded_variation nil) (< const-decl "bool" reals nil) (> const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (barray type-eq-decl nil fseqs "structures/") (fseq type-eq-decl nil fseqs "structures/") (AND const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (restrict const-decl "R" restrict nil) (<= const-decl "bool" reals nil) (increasing? const-decl "bool" sort_fseq "structures/") (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) (below type-eq-decl nil naturalnumbers nil) (partition type-eq-decl nil rs_partition nil) (integer nonempty-type-from-decl nil integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_le_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_minus_int_is_int application-judgement "int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (variation_on_strictly_sort_TCC1 0 (variation_on_strictly_sort_TCC1-1 nil 3493026057 ("" (lemma "partition_strictly_sort") (("" (beta) (("" (propax) nil nil)) nil)) nil) ((partition_strictly_sort formula-decl nil rs_partition 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) (T_pred const-decl "[real -> boolean]" bounded_variation nil) (T formal-nonempty-subtype-decl nil bounded_variation nil)) nil)) (variation_on_strictly_sort 0 (variation_on_strictly_sort-2 nil 3493039771 ("" (skeep) (("" (skeep) (("" (lemma "partition_union_is_strictly_sort") (("" (inst - "a" "b") (("" (assert) (("" (inst - "P") (("" (case "FORALL (ff:[T->real]): variation_on(a, b, P)(ff) = variation_on(a, b, strictly_sort (("1" (decompose-equality +) nil nil) ("2" (hide 2) (("2" (skeep) (("2" (name "ssm" "strictly_sort_map(P)") (("2" (label "ssmname" -1) (("2" (label "ssunion" -2) (("2" (label "altb" -3) (("2" (name "SSP" "strictly_sort(P)") (("2" (replace -1) (("2" (label "SSPname" -1) (("2" (expand "variation_on") (("2" (case "FORALL (nn:below(SSP`length-1)): sigma[below(P`length - 1)] (0, ssm(nn), LAMBDA (n: below(P`length - 1)): abs(ff(P`seq(1 + n)) - ff(P`seq(n)))) = sigma[below(SSP`length - 1)] (0, nn, LAMBDA (n: below(SSP`length - 1)): abs(ff(SSP`seq(1 + n)) - ff(SSP`seq(n))))") (("1" (inst - "SSP`length-2") (("1" (lemma "sigma_split[below(P`length-1)]") (("1" (inst - "LAMBDA (n: below(P`length - 1)): abs(ff(P`seq(1 + n)) - ff(P`seq(n)))" "P`length-2" "0" "ssm(SSP`length - 2)") (("1" (case "sigma(ssm(SSP`length - 2) + 1, P`length - 2, LAMBDA (n: below(P`length - 1)): abs(ff(P`seq(1 + n)) - ff(P`seq(n)))) = 0") (("1" (assert) (("1" (case "ssm(SSP`length-2) = P`length-1") (("1" (assert) (("1" (lemma "strictly_sort_map_increasing") (("1" (inst - "P") (("1" (assert) (("1" (inst - "SSP`length-2" "SSP`length-1") (("1" (assert) (("1" (replace "ssmname") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (case "SSP`length >= 2") (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (expand "SSP") (("2" (lemma "partition_strictly_sort") (("2" (inst - "a" "b") (("2" (assert) (("2" (inst - "P") (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (rewrite "sigma_restrict_eq_0") (("1" (hide 2) (("1" (hide -1) (("1" (hide -1) (("1" (skosimp*) (("1" (typepred "i!1") (("1" (typepred "ssm") (("1" (assert) (("1" (inst - "SSP`length-2") (("1" (assert) (("1" (flatten) (("1" (lemma "partition_strictly_sort") (("1" (inst - "a" "b") (("1" (assert) (("1" (inst - "P") (("1" (flatten) (("1" (assert) (("1" (typepred "P") (("1" (expand "increasing?") (("1" (inst-cp - "i!1" "1+i!1") (("1" (assert) (("1" (inst - "1 + ssm(SSP`length - 2)" "i!1") (("1" (assert) (("1" (inst-cp - "i!1+1") (("1" (inst - "i!1") (("1" (assert) (("1" (flatten) (("1" (assert) (("1" (expand "abs") (("1" (lift-if) (("1" (ground) 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" (hide-all-but 1) (("2" (case "strictly_sort(P)`length >= 2") (("1" (expand "SSP") (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (lemma "partition_strictly_sort") (("2" (inst - "a" "b") (("2" (assert) (("2" (inst - "P") (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (assert) (("1" (flatten) (("1" (inst + "0") (("1" (assert) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (case "strictly_sort(P)`length>=2") (("1" (expand "SSP") (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (lemma "partition_strictly_sort") (("2" (inst - "a" "b") (("2" (assert) (("2" (inst - "P") (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (hide-all-but 1) (("4" (expand "SSP") (("4" (lemma "partition_strictly_sort") (("4" (inst - "a" "b") (("4" (assert) (("4" (inst - "P") (("4" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "SSP") (("2" (lemma "partition_strictly_sort") (("2" (inst - "a" "b") (("2" (assert) (("2" (inst - "P") (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "SSP") (("2" (lemma "partition_strictly_sort") (("2" (inst - "a" "b") (("2" (assert) (("2" (inst - "P") (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (induct "nn") (("1" (flatten) (("1" (expand "sigma" +) (("1" (assert) (("1" (lift-if) (("1" (assert) (("1" (case "sigma(0, ssm(0) - 1, LAMBDA (n: below(P`length - 1)): abs(ff(P`seq(1 + n)) - ff(P`seq(n)))) = 0") (("1" (replace -1) (("1" (typepred "ssm") (("1" (assert) (("1" (inst - "0") (("1" (assert) (("1" (flatten) (("1" (replace "SSPname") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (rewrite "sigma_restrict_eq_0") (("2" (hide 2) (("2" (skosimp*) (("2" (typepred "i!1") (("2" (case "P`seq(1+i!1) = a") (("1" (typepred "P") (("1" (expand "increasing?") (("1" (inst - "i!1" "1+i!1") (("1" (assert) (("1" (inst - "i!1") (("1" (flatten) (("1" (assert) (("1" (expand "abs") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (typepred "ssm") (("2" (inst - "0") (("2" (assert) (("2" (flatten) (("2" (replace "SSPname") (("2" (typepred "P") (("2" (expand "increasing?") (("2" (inst - "i!1+1" "ssm(0)") (("2" (assert) (("2" (inst - "1+i!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (case "strictly_sort(P)`length>=2") (("1" (expand "SSP") (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (lemma "partition_strictly_sort") (("2" (inst - "a" "b") (("2" (assert) (("2" (inst - "P") (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skolem 1 "mm") (("2" (assert) (("2" (flatten) (("2" (expand "sigma" +) (("2" (lift-if) (("2" (assert) (("2" (typepred "ssm(1+mm)") (("2" (assert) (("2" (replace -3 :dir rl) (("2" (lemma "sigma_split[below(P`length-1)]") (("1" (inst - "LAMBDA (n: below(P`length - 1)): abs(ff(P`seq(1 + n)) - ff(P`seq(n)))" "ssm(1+mm)-1" "0" "ssm(mm)") (("1" (assert) (("1" (case "ssm(mm)<=ssm(1+mm)-1") (("1" (assert) (("1" (hide -1) (("1" (case "ff(P`seq(1 + ssm(1 + mm))) - ff(P`seq(ssm(1 + mm))) = ff(SSP`seq(2 + mm)) - ff(SSP`seq(1 + mm)) (("1" (case "sigma(1 + ssm(mm), ssm(1 + mm) - 1, LAMBDA (n: below(P`length - 1)): abs(ff(P`seq(1 + n)) - ff(P`seq(n)))) = 0") (("1" (assert) nil nil) ("2" (hide 2) (("2" (hide -2) (("2" (hide -4) (("2" (rewrite "sigma_restrict_eq_0") (("2" (hide 2) (("2" (skosimp*) (("2" (typepred "i!1") (("2" (case "P`seq(i!1) = P`seq(1+i!1)") (("1" (expand "abs" +) (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "strictly_sort_map_between") (("2" (inst - "P") (("2" (replace "SSPname") (("2" (assert) (("2" (replace "ssmname") (("2" (inst - "mm") (("2" (inst-cp - "i!1") (("2" (inst - "i!1+1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (case "P`seq(1+ssm(1+mm)) = SSP`seq(2+mm)") (("1" (typepred "ssm") (("1" (inst - "1+mm") (("1" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (hide -1) (("2" (hide -3) (("2" (typepred "ssm") (("2" (assert) (("2" (inst - "1+mm") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (hide -1) (("2" (hide -3) (("2" (lemma "strictly_sort_map_increasing") (("2" (inst - "P") (("2" (assert) (("2" (inst - "mm" "1+mm") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil) ("4" (hide 2) (("4" (skosimp*) (("4" (assert) nil nil)) nil)) nil) ("5" (hide 2) (("5" (skosimp*) (("5" (assert) (("5" (hide 2) (("5" (assert) (("5" (assert) (("5" (typepred "nn!2") (("5" (typepred "SSP") (("5" (expand "strictly_increasing?") (("5" (inst - "nn!2" "SSP`length-1") (("5" (assert) (("5" (flatten) (("5" (case "P`seq(ssm(nn!2)) < b") (("1" (assert) nil nil) ("2" (typepred "ssm") (("2" (inst - "nn!2") (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("6" (hide 2) (("6" (skosimp*) (("6" (assert) nil nil)) nil)) nil) ("7" (hide 2) (("7" (assert) nil nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil) ("4" (skosimp*) (("4" (assert) nil nil)) nil) ("5" (hide 2) (("5" (skosimp*) (("5" (hide 2) (("5" (assert) (("5" (assert) (("5" (assert) (("5" (case "NOT ssm(nn!1) = P`length-1") (("1" (assert) nil nil) ("2" (hide +) (("2" (typepred "nn!1") (("2" (typepred "ssm") (("2" (inst - "nn!1") (("2" (assert) (("2" (flatten) (("2" (replace "SSPname") (("2" (replace -5) (("2" (assert) (("2" (typepred "SSP") (("2" (expand "strictly_increasing?") (("2" (inst - "nn!1" "SSP`length-1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("6" (hide 2) (("6" (skosimp*) (("6" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nat nonempty-type-eq-decl nil naturalnumbers nil) (barray type-eq-decl nil fseqs "structures/") (fseq type-eq-decl nil fseqs "structures/") (bool nonempty-type-eq-decl nil booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (> const-decl "bool" reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (restrict const-decl "R" restrict nil) (<= const-decl "bool" reals nil) (increasing? const-decl "bool" sort_fseq "structures/") (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) (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (partition type-eq-decl nil rs_partition nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (strictly_sort_map const-decl "{sq: [below(strictly_sort(s)`length) -> below(s`length)] | LET sss = strictly_sort(s) IN (increasing?(s) AND sss`length >= 1 IMPLIES sq(sss`length - 1) = s`length - 1) AND (FORALL (ii: below(sss`length)): (sss`seq(ii) = s`seq(sq(ii)) AND (increasing?(s) AND ii < sss`length - 1 IMPLIES sss`seq(ii + 1) = s`seq(sq(ii) + 1))))}" sort_fseq "structures/") (sigma_nnreal application-judgement "nnreal" sigma_below "reals/") (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (T_low type-eq-decl nil sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (sigma def-decl "real" sigma "reals/") (nonneg_real nonempty-type-eq-decl nil real_types nil) (- const-decl "[numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (integer nonempty-type-from-decl nil integers nil) (sigma_split formula-decl nil sigma "reals/") (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (partition_strictly_sort formula-decl nil rs_partition nil) (strictly_sort_map_increasing formula-decl nil sort_fseq "structures/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sigma_restrict_eq_0 formula-decl nil sigma "reals/") (minus_real_is_real application-judgement "real" reals nil) (int_plus_int_is_int application-judgement "int" integers nil) (subrange type-eq-decl nil integers nil) (NOT const-decl "[bool -> bool]" booleans nil) (SSP skolem-const-decl "{ss: fseq[T] | strictly_increasing?(ss) AND (FORALL (x: T): member(x, P) IFF member(x, ss))}" bounded_variation nil) (P skolem-const-decl "partition[T](a, b)" bounded_variation nil) (b skolem-const-decl "T" bounded_variation nil) (a skolem-const-decl "T" bounded_variation nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (ssm skolem-const-decl "{sq: [below(strictly_sort(P)`length) -> below(P`length)] | (strictly_sort(P)`length >= 1 IMPLIES sq(strictly_sort(P)`length - 1) = P`length - 1) AND (FORALL (ii: below(strictly_sort(P)`length)): (strictly_sort(P)`seq(ii) = P`seq(sq(ii)) AND (ii < strictly_sort(P)`length - 1 IMPLIES strictly_sort(P)`seq(1 + ii) = P`seq(1 + sq(ii)))))}" bounded_variation nil) (pred type-eq-decl nil defined_types nil) (below_induction formula-decl nil bounded_nat_inductions nil) (sigma_0_neg formula-decl nil sigma_below "reals/") (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (strictly_sort_map_between formula-decl nil sort_fseq "structures/") (real_minus_real_is_real application-judgement "real" reals nil) (strictly_sort const-decl "{ss: fseq | strictly_increasing?(ss) AND (FORALL (x: T): member(x, s) IFF member(x, ss))}" sort_fseq "structures/") (member const-decl "bool" fseqs "structures/") (IFF const-decl "[bool, bool -> bool]" booleans nil) (strictly_increasing? const-decl "bool" sort_fseq "structures/") (variation_on const-decl "nnreal" bounded_variation nil) (nnreal type-eq-decl nil real_types nil) (reflexive_restrict application-judgement "(reflexive?[S])" restrict_order_props nil) (antisymmetric_restrict application-judgement "(antisymmetric?[S])" restrict_order_props nil) (transitive_restrict application-judgement "(transitive?[S])" restrict_order_props nil) (preorder_restrict application-judgement "(preorder?[S])" restrict_order_props nil) (partial_order_restrict application-judgement "(partial_order?[S])" restrict_order_props nil) (dichotomous_restrict application-judgement "(dichotomous?[S])" restrict_order_props nil) (total_order_restrict application-judgement "(total_order?[S])" restrict_order_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (partition_union_is_strictly_sort formula-decl nil rs_partition 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) (T_pred const-decl "[real -> boolean]" bounded_variation nil) (T formal-nonempty-subtype-decl nil bounded_variation nil)) nil) (variation_on_strictly_sort-1 nil 3493025984 ("" (case "FORALL (nn:nat): FORALL (a:real,(b:real|a<b),P:partition(a,b)): P`length=nn+2 IM (("1" (skeep) (("1" (skeep) (("1" (inst - "P`length-2") (("1" (inst - "a" "b" "P") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (induct "nn") (("1" (skosimp*) (("1" (case "P!1 = strictly_sort(P!1)") (("1" (assert) nil nil) ("2" (hide 2) (("2" (assert) (("2" (lemma "partition_union_is_strictly_sort") (("2" (inst - "a!1" "b!1") (("2" (assert) (("2" (inst - "P!1") (("2" (lemma "partition_union_unique") (("2" (inst - "a!1" "b!1") (("2" (assert) (("2" (inst - "P!1" "P!1" "P!1") (("2" (assert) (("2" (hide 2) (("2" (split +) (("1" (skeep) (("1" (ground) nil nil)) nil) ("2" (hide -1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skolem 1 "nn") (("2" (flatten) (("2" (assert) (("2" (skosimp*) (("2" (name "Prem" "(# length := 2+nn, seq:= (LAMBDA (mm:nat): IF mm<=nn+1 THEN P!1`seq(mm) ELSE default[real] EN (("2" (case "P!1`seq(nn+2) = P!1`seq(nn+1)") (("1" (inst - "a!1" "b!1" "Prem") (("1" (assert) (("1" (case "variation_on(a!1,b!1,Prem) = variation_on(a!1,b!1,P!1)") (("1" (case "strictly_sort(Prem) = strictly_sort(P!1)") (("1" (assert) nil nil) ("2" (hide 2) (("2" (lemma "partition_union_is_strictly_sort") (("2" (inst - "a!1" "b!1") (("2" (assert) (("2" (inst - "P!1") (("2" (lemma "partition_union_unique") (("2" (inst - "a!1" "b!1") (("2" (assert) (("2" (inst - "P!1" "P!1" "strictly_sort(Prem)") (("2" (assert) (("2" (hide 2) (("2" (skeep) (("2" (split +) (("1" (flatten) (("1" (hide 2) (("1" (typepred "strictly_sort(Prem)") (("1" (inst - "x") (("1" (assert) (("1" (replace -3) (("1" (hide -3) (("1" (assert) (("1" (skosimp*) (("1" (inst + "i!1") (("1" (expand "Prem" -2) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) (("2" (case "member(x,P!1)") (("1" (hide -2) (("1" (typepred "strictly_sort(Prem)") (("1" (inst - "x") (("1" (assert) (("1" (replace -2 :dir rl) (("1" (hide -2) (("1" (skosimp*) (("1" (case "i!1 = nn+2") (("1" (inst + "nn+1") (("1" (expand "Prem" +) (("1" (assert) nil nil)) nil)) nil) ("2" (inst + "i!1") (("1" (expand "Prem" +) (("1" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "Prem" +) (("2" (expand "variation_on" +) (("2" (decompose-equality +) (("1" (replace -4) (("1" (assert) (("1" (expand "sigma" + 2) (("1" (assert) (("1" (replace -1) (("1" (assert) (("1" (expand "abs" + 2) (("1" (case "FORALL (mm:below(1+nn)): sigma[below(1 + nn)] (0, mm, LAMBDA (n: below(1 + nn)): abs(x!1(P!1`seq(1 + n)) - x!1(P!1`seq(n)))) = sigma(0, mm, LAMBDA (n: below(P!1`length - 1)): abs(x!1(P!1`seq(1 + n)) - x!1(P!1`seq(n))))") (("1" (inst - "nn") nil nil) ("2" (assert) (("2" (hide 2) (("2" (induct "mm") (("1" (assert) (("1" (expand "sigma" +) (("1" (expand "sigma" +) (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (skolem 1 "mm") (("2" (flatten) (("2" (expand "sigma" +) (("2" (propax) nil nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil) ("4" (hide 2) (("4" (skosimp*) (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil) ("4" (hide 2) (("4" (skosimp*) (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "Prem" +) (("2" (assert) (("2" (split +) (("1" (skeep) (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil) ("2" (expand "increasing?") (("2" (skosimp*) (("2" (lift-if) (("2" (lift-if) (("2" (assert) (("2" (typepred "P!1") (("2" (expand "increasing?") (("2" (inst - "i!1" "j!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skeep) (("3" (typepred "P!1") (("3" (inst - "i") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst - "a!1" "P!1`seq(1+nn)" "Prem") (("1" (assert) (("1" (case "FORALL (ff:[real->real]): variation_on(a!1, b!1, P!1)(ff) = variation_on(a!1, b!1, strictly_sort(P!1))(ff)") (("1" (decompose-equality 2) nil nil) ("2" (hide 3) (("2" (skeep) (("2" (case "variation_on(a!1,P!1`seq(1 + nn),Prem)(ff) + abs(ff(P!1`seq(2 + nn)) - ff(P!1`seq(1 + nn) (("1" (case "variation_on(a!1, P!1`seq(1 + nn), strictly_sort(Prem))(ff) + abs(ff(P!1`seq(2 + nn)) - f (("1" (assert) nil nil) ("2" (hide 2) (("2" (hide -1) (("2" (expand "variation_on" +) (("2" (expand "sigma" + 2) (("2" (assert) (("1" (case "strictly_sort(P!1)`length >= 2") (("1" (assert) (("1" (case "strictly_sort(P!1)`seq(strictly_sort(P!1)`length - 2) = P!1`seq(P!1`length-2)") (("1" (lemma "partition_strictly_sort") (("1" (inst - "a!1" "b!1") (("1" (assert) (("1" (inst - "P!1") (("1" (flatten) (("1" (case "sigma(0, strictly_sort(P!1)`length - 3, LAMBDA (n: below(strictly_sort(P!1)`length - 1)): abs(ff(strictly_sort(P!1)`seq(1 + n)) - ff(strictly_sort(P!1)`seq(n)))) = sigma[below(strictly_sort(Prem)`length - 1)] (0, strictly_sort(Prem)`length - 2, LAMBDA (n: below(strictly_sort(Prem)`length - 1)): abs(ff(strictly_sort(Prem)`seq(1 + n)) - ff(strictly_sort(Prem)`seq(n))))") (("1" (assert) nil nil) ("2" (hide 2) (("2" (hide -1) (("2" (hide -1) (("2" (hide -1) (("2" (hide -1) (("2" (hide -1) (("2" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (postpone) nil nil) ("4" (postpone) nil nil)) nil)) nil)) nil) ("2" (postpone) nil nil)) nil)) nil)) nil) ("2" (postpone) nil nil)) nil) ("2" (postpone) nil nil) ("3" (postpone) nil nil)) nil) ("2" (postpone) nil nil)) nil) ("2" (postpone) nil nil) ("3" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (postpone) nil nil) ("3" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (postpone) nil nil)) nil)) nil) ("3" (postpone) nil nil)) nil) nil shostak)) (monotonic_BV_TCC1 0 (monotonic_BV_TCC1-1 nil 3610719231 ("" (subtype-tcc) nil nil) nil nil)) (monotonic_BV 0 (monotonic_BV-1 nil 3491555814 ("" (skeep) (("" (expand "monotonic?") (("" (split -) (("1" (expand "bounded_variation?") (("1" (case "NOT f(bb) - f(a) >= 0") (("1" (hide 2) (("1" (expand "increasing?") (("1" (inst - "a" "bb") (("1" (assert) (("1" (expand "restrict") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (inst + "f(bb)-f(a)") (("2" (skeep) (("2" (expand "variation_on") (("2" (case "FORALL (mm:below(P`length-1)): sigma[below(P`length - 1)] (0, mm, LAMBDA (n: below(P`length-1)): abs(f(P`seq(1 + n)) - f(P`seq(n)))) = f(P`seq(mm+1)) -f(P`s (("1" (inst - "P`length-2") (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (induct "mm") (("1" (assert) (("1" (expand "sigma") (("1" (expand "sigma") (("1" (expand "increasing?") (("1" (inst - "P`seq(0)" "P`seq(1)") (("1" (assert) (("1" (expand "restrict") (("1" (typepred "P") (("1" (expand "increasing?") (("1" (inst - "0" "1") (("1" (assert) (("1" (expand "abs") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "P") (("2" (inst - "1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skolem 1 "nn") (("2" (assert) (("2" (flatten) (("2" (expand "sigma" +) (("2" (replace -2) (("2" (expand "increasing?") (("2" (inst - "P`seq(1+nn)" "P`seq(2+nn)") (("1" (expand "restrict") (("1" (typepred "P") (("1" (expand "increasing?") (("1" (inst - "1+nn" "2+nn") (("1" (ground) (("1" (expand "abs" +) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "P") (("2" (inst - "2+nn") (("2" (assert) nil nil)) nil)) nil) ("3" (typepred "P") (("3" (inst - "1+nn") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "bounded_variation?") (("2" (case "NOT f(a)-f(bb) >= 0") (("1" (expand "decreasing?") (("1" (inst - "a" "bb") (("1" (expand "restrict") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (inst + "f(a)-f(bb)") (("2" (skeep) (("2" (expand "variation_on") (("2" (case "FORALL (mm:below(P`length-1)): sigma[below(P`length - 1)] (0, mm, LAMBDA (n: below(P`length-1)): abs(f(P`seq(1 + n)) - f(P`seq(n)))) = f(P`seq(0)) -f(P`seq( (("1" (inst - "P`length-2") (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (induct "mm") (("1" (assert) (("1" (expand "sigma") (("1" (expand "sigma") (("1" (expand "decreasing?") (("1" (inst - "P`seq(0)" "P`seq(1)") (("1" (assert) (("1" (expand "restrict") (("1" (typepred "P") (("1" (expand "increasing?") (("1" (inst - "0" "1") (("1" (assert) (("1" (expand "abs") (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "P") (("2" (inst - "1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skolem 1 "nn") (("2" (assert) (("2" (flatten) (("2" (expand "sigma" +) (("2" (replace -2) (("2" (expand "decreasing?") (("2" (inst - "P`seq(1+nn)" "P`seq(2+nn)") (("1" (expand "restrict") (("1" (typepred "P") (("1" (expand "increasing?") (("1" (inst - "1+nn" "2+nn") (("1" (ground) (("1" (expand "abs" +) (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "P") (("2" (inst - "2+nn") (("2" (assert) nil nil)) nil)) nil) ("3" (typepred "P") (("3" (inst - "1+nn") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((monotonic? const-decl "bool" real_fun_preds "reals/") (f skolem-const-decl "[T -> real]" bounded_variation nil) (nn skolem-const-decl "below(P`length - 1)" bounded_variation nil) (real_times_real_is_real application-judgement "real" reals nil) (minus_real_is_real application-judgement "real" reals nil) (P skolem-const-decl "partition[T](a, bb)" bounded_variation nil) (decreasing? const-decl "bool" real_fun_preds "reals/") (bounded_variation? const-decl "bool" bounded_variation nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield -> numfield]" number_fields nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (sigma def-decl "real" sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (OR const-decl "[bool, bool -> bool]" booleans nil) (partition type-eq-decl nil rs_partition nil) (below type-eq-decl nil naturalnumbers nil) (increasing? const-decl "bool" sort_fseq "structures/") (= const-decl "[T, T -> boolean]" equalities nil) (> const-decl "bool" reals nil) (fseq type-eq-decl nil fseqs "structures/") (barray type-eq-decl nil fseqs "structures/") (nat nonempty-type-eq-decl nil naturalnumbers 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) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (sigma_nnreal application-judgement "nnreal" sigma_below "reals/") (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (integer nonempty-type-from-decl nil integers nil) (int_plus_int_is_int application-judgement "int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (a skolem-const-decl "T" bounded_variation nil) (bb skolem-const-decl "{bb: T | a < bb}" bounded_variation nil) (P skolem-const-decl "partition[T](a, bb)" bounded_variation nil) (pred type-eq-decl nil defined_types nil) (below_induction formula-decl nil bounded_nat_inductions nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_plus_real_is_real application-judgement "real" reals nil) (nn skolem-const-decl "below(P`length - 1)" bounded_variation nil) (variation_on const-decl "nnreal" bounded_variation nil) (nnreal type-eq-decl nil real_types nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (restrict const-decl "R" restrict nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (increasing? const-decl "bool" real_fun_preds "reals/") (real_minus_real_is_real application-judgement "real" reals 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) (>= const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (T_pred const-decl "[real -> boolean]" bounded_variation nil) (T formal-nonempty-subtype-decl nil bounded_variation nil) (< const-decl "bool" reals nil)) shostak)) (BV_bounded 0 (BV_bounded-1 nil 3491557700 ("" (skeep) (("" (expand "bounded_variation?") (("" (skosimp*) (("" (expand "bounded_on?") (("" (inst + "abs(f(a)) + M!1") (("" (skosimp*) (("" (name "P" "(# length := 3, seq := (LAMBDA (n:nat): If n = 0 THEN a ELSIF n = 1 then x!1 ELSIF n = 2 THEN b ELSE defau (("" (inst - "P") (("1" (expand "variation_on") (("1" (replace -1 :dir rl) (("1" (assert) (("1" (expand "sigma") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (hide -1) (("1" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (replace -1 :dir rl) (("2" (assert) (("2" (hide -1) (("2" (split +) (("1" (skeep) (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil) ("2" (expand "increasing?") (("2" (skeep) (("2" (lift-if) (("2" (lift-if) (("2" (assert) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (skeep) (("3" (lift-if) (("3" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((bounded_variation? const-decl "bool" bounded_variation nil) (bounded_on? const-decl "bool" rs_partition 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) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (P skolem-const-decl "[# length: posint, seq: [nat -> T] #]" bounded_variation nil) (a skolem-const-decl "T" bounded_variation nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (b skolem-const-decl "T" bounded_variation nil) (barray type-eq-decl nil fseqs "structures/") (fseq type-eq-decl nil fseqs "structures/") (restrict const-decl "R" restrict nil) (increasing? const-decl "bool" sort_fseq "structures/") (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (partition type-eq-decl nil rs_partition nil) (sigma def-decl "real" sigma "reals/") (minus_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (sigma_nnreal application-judgement "nnreal" sigma_below "reals/") (odd_minus_even_is_odd application-judgement "odd_int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (variation_on const-decl "nnreal" bounded_variation nil) (real_minus_real_is_real application-judgement "real" 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) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posint nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (= const-decl "[T, T -> boolean]" equalities nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (<= const-decl "bool" reals nil) (closed_interval type-eq-decl nil intervals_real "reals/") (default const-decl "T" fseqs "structures/") (nnreal type-eq-decl nil real_types nil) (T formal-nonempty-subtype-decl nil bounded_variation nil) (T_pred const-decl "[real -> boolean]" bounded_variation nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield -> numfield]" number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields 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) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil)) nil)) (BV_bound 0 (BV_bound-1 nil 3491557803 ("" (skeep) (("" (skosimp*) (("" (name "P" "(# length := 3, seq := (LAMBDA (n:nat): If n = 0 THEN a ELSIF n = 1 then x!1 ELSIF n = 2 THEN b ELSE defau (("" (inst - "P") (("1" (expand "variation_on") (("1" (replace -1 :dir rl) (("1" (assert) (("1" (expand "sigma") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (hide -1) (("1" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (replace -1 :dir rl) (("2" (assert) (("2" (hide -1) (("2" (split +) (("1" (skeep) (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil) ("2" (expand "increasing?") (("2" (skeep) (("2" (lift-if) (("2" (lift-if) (("2" (assert) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (skeep) (("3" (lift-if) (("3" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (increasing? const-decl "bool" sort_fseq "structures/") (restrict const-decl "R" restrict nil) (fseq type-eq-decl nil fseqs "structures/") (barray type-eq-decl nil fseqs "structures/") (b skolem-const-decl "T" bounded_variation nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (a skolem-const-decl "T" bounded_variation nil) (P skolem-const-decl "[# length: posint, seq: [nat -> T] #]" bounded_variation nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (partition type-eq-decl nil rs_partition nil) (sigma def-decl "real" sigma "reals/") (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (minus_real_is_real application-judgement "real" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (sigma_nnreal application-judgement "nnreal" sigma_below "reals/") (odd_minus_even_is_odd application-judgement "odd_int" integers nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (variation_on const-decl "nnreal" bounded_variation nil) (real_minus_real_is_real application-judgement "real" reals 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) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posint nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (T_pred const-decl "[real -> boolean]" bounded_variation nil) (T formal-nonempty-subtype-decl nil bounded_variation nil) (= const-decl "[T, T -> boolean]" equalities nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (default const-decl "T" fseqs "structures/")) nil)) (BV_add 0 (BV_add-1 nil 3491558160 ("" (skeep) (("" (expand "bounded_variation?") (("" (skosimp*) (("" (inst + "M!1+M!2") (("" (skeep) (("" (inst - "P") (("" (inst - "P") (("" (expand "variation_on") (("" (name "FF" "LAMBDA (n: below(P`length - 1)): abs(f(P`seq(1 + n)) - f(P`seq(n)))") (("" (replace -1) (("" (name "GG" "LAMBDA (n: below(P`length - 1)): abs(g(P`seq(1 + n)) - g(P`seq(n)))") (("" (replace -1) (("" (name "FG" "LAMBDA (n: below(P`length - 1)): abs(f(P`seq(1 + n)) + g(P`seq(1 + n)) - f(P`seq(n)) - g(P`seq(n)))") (("" (replace -1) (("" (lemma "sigma[below(P`length-1)].sigma_le") (("1" (inst - "FG" "LAMBDa (n:below(P`length-1)): FF(n) + GG(n)" "P`length-2" "0") (("1" (assert) (("1" (split -) (("1" (lemma "sigma[below(P`length-1)].sigma_sum") (("1" (inst - "FF" "GG" "P`length-2" "0") (("1" (assert) nil nil)) nil)) nil) ("2" (skolem 1 "mm") (("2" (expand "FG" 1) (("2" (expand "GG" 1) (("2" (expand "FF" 1) (("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((bounded_variation? const-decl "bool" bounded_variation nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types 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) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (T_pred const-decl "[real -> boolean]" bounded_variation nil) (T formal-nonempty-subtype-decl nil bounded_variation nil) (barray type-eq-decl nil fseqs "structures/") (fseq type-eq-decl nil fseqs "structures/") (AND const-decl "[bool, bool -> bool]" booleans nil) (> const-decl "bool" reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (restrict const-decl "R" restrict nil) (<= const-decl "bool" reals nil) (increasing? const-decl "bool" sort_fseq "structures/") (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) (below type-eq-decl nil naturalnumbers nil) (partition type-eq-decl nil rs_partition nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (variation_on const-decl "nnreal" bounded_variation nil) (int_minus_int_is_int application-judgement "int" integers nil) (T_low type-eq-decl nil sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (OR const-decl "[bool, bool -> bool]" booleans nil) (sigma_sum formula-decl nil sigma "reals/") (FG skolem-const-decl "[n: below(P`length - 1) -> {n_1: nonneg_real | n_1 >= f(P`seq(1 + n)) + g(P`seq(1 + n)) - f(P`seq(n)) - g(P`seq(n)) AND n_1 >= -(f(P`seq(1 + n)) + g(P`seq(1 + n)) - f(P`seq(n)) - g(P`seq(n)))}]" bounded_variation nil) (FF skolem-const-decl "[n: below(P`length - 1) -> {n_1: nonneg_real | n_1 >= f(P`seq(1 + n)) - f(P`seq(n)) AND n_1 >= -(f(P`seq(1 + n)) - f(P`seq(n)))}]" bounded_variation nil) (int_plus_int_is_int application-judgement "int" integers nil) (minus_real_is_real application-judgement "real" reals nil) (GG skolem-const-decl "[n: below(P`length - 1) -> {n_1: nonneg_real | n_1 >= g(P`seq(1 + n)) - g(P`seq(n)) AND n_1 >= -(g(P`seq(1 + n)) - g(P`seq(n)))}]" bounded_variation nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (sigma_nnreal application-judgement "nnreal" sigma_below "reals/") (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) (integer nonempty-type-from-decl nil integers nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (sigma_le formula-decl nil sigma "reals/") (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield -> numfield]" number_fields nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil)) shostak)) (BV_scal 0 (BV_scal-1 nil 3491559567 ("" (skeep) (("" (expand "bounded_variation?") (("" (skosimp*) (("" (inst + "abs(D)*M!1") (("" (skeep) (("" (inst - "P") (("" (expand "variation_on") (("" (name "FF" "LAMBDA (n: below(P`length - 1)): abs(f(P`seq(1 + n)) - f(P`seq(n)))") (("" (lemma "sigma[below(P`length-1)].sigma_scal") (("1" (inst - "FF" "abs(D)" "P`length-2" "0") (("1" (assert) (("1" (case "(LAMBDA (i: below(P`length - 1)): abs(D) * FF(i)) = (LAMBDA (n: below(P`length - 1)): abs(D * f(P`seq(1 + n)) - D * f(P`seq(n))))") (("1" (assert) (("1" (mult-by -5 "abs(D)") (("1" (assert) nil nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (decompose-equality) (("2" (expand "FF" +) (("2" (hide -) (("2" (lemma "abs_mult") (("2" (inst - "D" "f(P`seq(1 + x!1)) - f(P`seq(x!1))") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((bounded_variation? const-decl "bool" bounded_variation nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types 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) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (- const-decl "[numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (T_pred const-decl "[real -> boolean]" bounded_variation nil) (T formal-nonempty-subtype-decl nil bounded_variation nil) (barray type-eq-decl nil fseqs "structures/") (fseq type-eq-decl nil fseqs "structures/") (> const-decl "bool" reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (restrict const-decl "R" restrict nil) (<= const-decl "bool" reals nil) (increasing? const-decl "bool" sort_fseq "structures/") (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) (below type-eq-decl nil naturalnumbers nil) (partition type-eq-decl nil rs_partition nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (int_minus_int_is_int application-judgement "int" integers nil) (T_low type-eq-decl nil sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (OR const-decl "[bool, bool -> bool]" booleans nil) (both_sides_times_pos_le1_imp formula-decl nil extra_real_props nil) (sigma def-decl "real" sigma "reals/") (P skolem-const-decl "partition[T](a, b)" bounded_variation nil) (b skolem-const-decl "T" bounded_variation nil) (a skolem-const-decl "T" bounded_variation nil) (abs_mult formula-decl nil real_props nil) (FF skolem-const-decl "[n: below(P`length - 1) -> {n_1: nonneg_real | n_1 >= f(P`seq(1 + n)) - f(P`seq(n)) AND n_1 >= -(f(P`seq(1 + n)) - f(P`seq(n)))}]" bounded_variation nil) (sigma_nnreal application-judgement "nnreal" sigma_below "reals/") (real_le_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_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) (integer nonempty-type-from-decl nil integers nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (sigma_scal formula-decl nil sigma "reals/") (variation_on const-decl "nnreal" bounded_variation nil) (real_times_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil)) shostak)) (BV_sub 0 (BV_sub-1 nil 3491559859 ("" (skeep) (("" (lemma "BV_scal") (("" (inst - "-1" "a" "b" "g") (("" (assert) (("" (lemma "BV_add") (("" (inst - "a" "b" "f" "LAMBDA (x: T): -1 * g(x)") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((BV_scal formula-decl nil bounded_variation nil) (real_times_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (BV_add formula-decl nil bounded_variation nil) (T formal-nonempty-subtype-decl nil bounded_variation nil) (T_pred const-decl "[real -> boolean]" bounded_variation nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields 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) (minus_odd_is_odd application-judgement "odd_int" integers nil)) shostak)) (BV_mult 0 (BV_mult-1 nil 3491559948 ("" (skeep) (("" (label "altb" -1) (("" (label "fBV" -2) (("" (label "gBV" -3) (("" (lemma "BV_bounded") (("" (inst-cp - "a" "b" "f") (("" (inst - "a" "b" "g") (("" (assert) (("" (label "fbounded" -2) (("" (label "gbounded" -1) (("" (expand "bounded_on?") (("" (skolem "gbounded" "gM") (("" (skolem "fbounded" "fM") (("" (expand "bounded_variation?") (("" (skolem "fBV" "fB") (("" (skolem "gBV" "gB") (("" (inst + "gM*fB + fM*gB") (("1" (skeep) (("1" (inst "fBV" "P") (("1" (inst "gBV" "P") (("1" (expand "variation_on") (("1" (name "FG" "LAMBDA (n: below(P`length - 1)): abs(f(P`seq(1 + n)) * g(P`seq(1 + n)) - f(P`seq(n)) * g(P`seq(n)))") (("1" (replace -1) (("1" (name "FF" "LAMBDA (n: below(P`length - 1)): abs(f(P`seq(1 + n)) - f(P`seq(n)))") (("1" (replace -1) (("1" (name "GG" "LAMBDA (n: below(P`length - 1)): abs(g(P`seq(1 + n)) - g(P`seq(n)))") (("1" (replace -1) (("1" (label "FGname" -3) (("1" (label "FFname" -2) (("1" (label "GGname" -1) (("1" (case "FORALL (mm:below(P`length-1)): FG(mm) <= fM*GG(mm) + gM*FF(mm)") (("1" (lemma "sigma[below(P`length-1)].sigma_le") (("1" (inst - "FG" "(LAMBDA (mm:below(P`length-1)): fM * GG(mm) + gM * FF(mm))" "P`length-2" "0") (("1" (assert) (("1" (split -) (("1" (lemma "sigma[below(P`length-1)].sigma_sum") (("1" (inst - "(LAMBDA (mm:below(P`length-1)): fM*GG(mm))" "(LAMBDA (mm:below(P`length-1)): gM*FF(mm))" "P`length-2" "0") (("1" (replace -1 :dir rl) (("1" (lemma "sigma[below(P`length-1)].sigma_scal") (("1" (copy -1) (("1" (inst - "GG" "fM" "P`length-2" "0") (("1" (inst - "FF" "gM" "P`length-2" "0") (("1" (assert) (("1" (replace -2) (("1" (copy "fBV") (("1" (mult-by -1 "gM") (("1" (copy "gBV") (("1" (mult-by -1 "fM") (("1" (assert) nil nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil) ("3" (inst "fbounded" "a") (("3" (assert) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil) ("3" (inst "gbounded" "a") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (assert) (("2" (skeep) (("2" (inst - "n") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (skeep) (("2" (case "FG(mm) <= abs(g(P`seq(mm+1))*(f(P`seq(mm+1))-f(P`seq(mm)))) + abs(f(P`seq(mm))*(g(P` (("1" (rewrite "abs_mult") (("1" (rewrite "abs_mult") (("1" (inst "gbounded" "P`seq(1+mm)") (("1" (inst "fbounded" "P`seq(mm)") (("1" (copy "gbounded") (("1" (mult-by -1 "abs((f(P`seq(1 + mm)) - f(P`seq(mm))))") (("1" (copy "fbounded") (("1" (mult-by -1 "abs((g(P`seq(1 + mm)) - g(P`seq(mm))))") (("1" (assert) (("1" (expand "GG" +) (("1" (expand "FF" +) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "P") (("2" (inst - "mm") nil nil)) nil)) nil) ("2" (typepred "P") (("2" (inst - "1+mm") nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "FG" +) (("2" (hide -) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (case "gM >= 0 AND fM >= 0") (("1" (case "fB >= 0 AND gB >= 0") (("1" (flatten) (("1" (lemma "nnreal_times_nnreal_is_nnreal") (("1" (inst-cp - "fM" "gB") (("1" (inst - "gM" "fB") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (name "P" "(# length := 2, seq:= (LAMBDA (mm:nat): if mm = 0 THEN a elsif mm = 1 then b else default[T] endif) # (("2" (inst "fBV" "P") (("1" (inst "gBV" "P") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (inst - "a") (("2" (inst - "a") (("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) ((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) (T_pred const-decl "[real -> boolean]" bounded_variation nil) (T formal-nonempty-subtype-decl nil bounded_variation nil) (real_times_real_is_real application-judgement "real" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (bounded_variation? const-decl "bool" bounded_variation nil) (nnreal_times_nnreal_is_nnreal judgement-tcc nil real_types nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posint nonempty-type-eq-decl nil integers nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (default const-decl "T" fseqs "structures/") (P skolem-const-decl "[# length: posint, seq: [nat -> T] #]" bounded_variation nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (- const-decl "[numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (GG skolem-const-decl "[n: below(P`length - 1) -> {n_1: nonneg_real | n_1 >= g(P`seq(1 + n)) - g(P`seq(n)) AND n_1 >= -(g(P`seq(1 + n)) - g(P`seq(n)))}]" bounded_variation nil) (FF skolem-const-decl "[n: below(P`length - 1) -> {n_1: nonneg_real | n_1 >= f(P`seq(1 + n)) - f(P`seq(n)) AND n_1 >= -(f(P`seq(1 + n)) - f(P`seq(n)))}]" bounded_variation nil) (NOT const-decl "[bool -> bool]" booleans nil) (mm skolem-const-decl "below(P`length - 1)" bounded_variation nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (abs_mult formula-decl nil real_props nil) (FG skolem-const-decl "[n: below(P`length - 1) -> {n_1: nonneg_real | n_1 >= f(P`seq(1 + n)) * g(P`seq(1 + n)) - f(P`seq(n)) * g(P`seq(n)) AND n_1 >= -(f(P`seq(1 + n)) * g(P`seq(1 + n)) - f(P`seq(n)) * g(P`seq(n)))}]" bounded_variation nil) (minus_real_is_real application-judgement "real" reals nil) (sigma_le formula-decl nil sigma "reals/") (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (integer nonempty-type-from-decl nil integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sigma_nnreal application-judgement "nnreal" sigma_below "reals/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (subrange type-eq-decl nil integers nil) (sigma_sum formula-decl nil sigma "reals/") (both_sides_times_pos_le1_imp formula-decl nil extra_real_props nil) (sigma def-decl "real" sigma "reals/") (P skolem-const-decl "partition[T](a, b)" bounded_variation nil) (b skolem-const-decl "T" bounded_variation nil) (a skolem-const-decl "T" bounded_variation nil) (closed_interval type-eq-decl nil intervals_real "reals/") (sigma_scal formula-decl nil sigma "reals/") (OR const-decl "[bool, bool -> bool]" booleans nil) (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (int_minus_int_is_int application-judgement "int" integers nil) (variation_on const-decl "nnreal" bounded_variation nil) (real_minus_real_is_real application-judgement "real" reals nil) (partition type-eq-decl nil rs_partition nil) (below 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) (increasing? const-decl "bool" sort_fseq "structures/") (<= const-decl "bool" reals nil) (restrict const-decl "R" restrict nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (> const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (fseq type-eq-decl nil fseqs "structures/") (barray type-eq-decl nil fseqs "structures/") (nat nonempty-type-eq-decl nil naturalnumbers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (fM skolem-const-decl "real" bounded_variation nil) (nnreal type-eq-decl nil real_types nil) (gB skolem-const-decl "nnreal" bounded_variation nil) (gM skolem-const-decl "real" bounded_variation nil) (fB skolem-const-decl "nnreal" bounded_variation nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (bounded_on? const-decl "bool" rs_partition nil) (BV_bounded formula-decl nil bounded_variation nil)) shostak)) (variation_on_subset_TCC1 0 (variation_on_subset_TCC1-1 nil 3492515681 ("" (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) (T_pred const-decl "[real -> boolean]" bounded_variation nil) (T formal-nonempty-subtype-decl nil bounded_variation nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props 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) (partition type-eq-decl nil rs_partition nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals 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) (increasing? const-decl "bool" sort_fseq "structures/") (<= const-decl "bool" reals nil) (restrict const-decl "R" restrict nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (fseq type-eq-decl nil fseqs "structures/") (barray type-eq-decl nil fseqs "structures/") (nat nonempty-type-eq-decl nil naturalnumbers nil) (> const-decl "bool" reals nil)) nil)) (variation_on_subset 0 (variation_on_subset-2 nil 3495206655 ("" (auto-rewrite + "member") (("" (skeep) (("" (skeep) (("" (name "Pab" "(# length := Pcd`length+2, seq:= (LAMBDA (nn:nat): IF nn = 0 THEN a ELSIF nn = Pcd`length+1 THEN (("1" (inst + "Pab") (("1" (hide -1) (("1" (expand "Pab" +) (("1" (expand "variation_on") (("1" (expand "sigma" + 2) (("1" (case "sigma[below(Pcd`length - 1)] (0, Pcd`length - 2, LAMBDA (n: below(Pcd`length - 1)): abs(f(Pcd`seq(1 + n)) - f(Pcd`seq(n)))) <= sigma(0, Pcd`length - 1, LAMBDA (n: below(1 + Pcd`length)): abs(IF n = Pcd`length THEN f(b) ELSE f(Pcd`seq(n)) ENDIF - IF n = 0 THEN f(a) ELSE f(Pcd`seq(n - 1)) ENDIF))") (("1" (assert) nil nil) ("2" (hide 2) (("2" (lemma "sigma_split[below(1+Pcd`length)]") (("2" (inst - "LAMBDA (n: below(1 + Pcd`length)): abs(IF n = Pcd`length THEN f(b) ELSE f(Pcd`seq(n)) ENDIF - IF n = 0 THEN f(a) ELSE f(Pcd`seq(n - 1)) ENDIF)" "Pcd`length-1" "0" "0") (("1" (assert) (("1" (expand "sigma" - 2) (("1" (expand "sigma" - 2) (("1" (case "sigma[below(Pcd`length - 1)] (0, Pcd`length - 2, LAMBDA (n: below(Pcd`length - 1)): abs(f(Pcd`seq(1 + n)) - f(Pcd`seq(n)))) = sigma[below(1+Pcd`length)](1, Pcd`length - 1, LAMBDA (n: below(1 + Pcd`length)): abs(IF n = Pcd`length THEN f(b) ELSE f(Pcd`seq(n)) ENDIF - IF n = 0 THEN f(a) ELSE f(Pcd`seq(n - 1)) ENDIF))") (("1" (assert) nil nil) ("2" (hide 2) (("2" (hide -1) (("2" (case "FORALL (nn:nat): nn <= Pcd`length-2 IMPLIES sigma[below(Pcd`length - 1)] (0, nn, LAMBDA (n: below(Pcd`length - 1)): abs(f(Pcd`seq(1 + n)) - f(Pcd`seq(n)))) = sigma[below(1 + Pcd`length)] (1, 1+nn, LAMBDA (n: below(1 + Pcd`length)): abs(IF n = Pcd`length THEN f(b) ELSE f(Pcd`seq(n)) ENDIF - IF n = 0 THEN f(a) ELSE f(Pcd`seq(n - 1)) ENDIF))") (("1" (inst - "Pcd`length-2") (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (induct "nn") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (propax) nil nil)) nil)) nil) ("2" (skolem 1 "nn") (("2" (flatten) (("2" (assert) (("2" (expand "sigma" +) (("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil) ("4" (hide 2) (("4" (skosimp*) (("4" (assert) nil nil)) nil)) nil) ("5" (hide 2) (("5" (skosimp*) (("5" (assert) nil nil)) nil)) nil) ("6" (hide 2) (("6" (skosimp*) (("6" (assert) nil nil)) nil)) nil) ("7" (hide 2) (("7" (skosimp*) (("7" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil) ("4" (hide 2) (("4" (skosimp*) (("4" (assert) nil nil)) nil)) nil) ("5" (hide 2) (("5" (skosimp*) (("5" (assert) nil nil)) nil)) nil) ("6" (hide 2) (("6" (skosimp*) (("6" (assert) nil nil)) nil)) nil) ("7" (hide 2) (("7" (skosimp*) (("7" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil) ("4" (hide 2) (("4" (skosimp*) (("4" (assert) nil nil)) nil)) nil) ("5" (hide 2) (("5" (skosimp*) (("5" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (assert) (("2" (expand "Pab" +) (("2" (split +) (("1" (skeep) (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil) ("2" (expand "increasing?") (("2" (skosimp*) (("2" (lift-if) (("2" (lift-if) (("2" (lift-if) (("2" (lift-if) (("2" (lift-if) (("2" (assert) (("2" (ground) (("1" (typepred "Pcd") (("1" (inst - "j!1-1") (("1" (ground) nil nil)) nil)) nil) ("2" (typepred "Pcd") (("2" (inst - "i!1-1") (("2" (ground) nil nil)) nil)) nil) ("3" (typepred "Pcd") (("3" (expand "increasing?") (("3" (inst - "i!1-1" "j!1-1") (("3" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skeep) (("3" (lift-if) (("3" (assert) (("3" (typepred "Pcd") (("3" (inst - "i-1") (("1" (ground) nil nil) ("2" (assert) (("2" (typepred "i") (("2" (expand "Pab" -1) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((default const-decl "T" fseqs "structures/") (IF const-decl "[boolean, T, T -> T]" if_def nil) (partition type-eq-decl nil rs_partition nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (increasing? const-decl "bool" sort_fseq "structures/") (<= const-decl "bool" reals nil) (restrict const-decl "R" restrict nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (fseq type-eq-decl nil fseqs "structures/") (barray type-eq-decl nil fseqs "structures/") (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (T formal-nonempty-subtype-decl nil bounded_variation nil) (T_pred const-decl "[real -> boolean]" bounded_variation nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (posint nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers 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) (int_minus_int_is_int application-judgement "int" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (NOT const-decl "[bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (i skolem-const-decl "below(Pab`length)" bounded_variation nil) (real_minus_real_is_real application-judgement "real" reals nil) (variation_on const-decl "nnreal" bounded_variation nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (T_low type-eq-decl nil sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (nonneg_real nonempty-type-eq-decl nil real_types nil) (- const-decl "[numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (integer nonempty-type-from-decl nil integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (sigma_nnreal application-judgement "nnreal" sigma_below "reals/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (sigma_split formula-decl nil sigma "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (pred type-eq-decl nil defined_types nil) (nat_induction formula-decl nil naturalnumbers nil) (Pcd skolem-const-decl "partition[T](c, d)" bounded_variation nil) (d skolem-const-decl "T" bounded_variation nil) (c skolem-const-decl "T" bounded_variation nil) (sigma def-decl "real" sigma "reals/") (b skolem-const-decl "T" bounded_variation nil) (a skolem-const-decl "T" bounded_variation nil) (Pab skolem-const-decl "[# length: posint, seq: [nat -> T] #]" bounded_variation nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil) (variation_on_subset-1 nil 3492515681 ("" (skeep) (("" (skeep) (("" (name "Pab" "(# length := Pcd`length+2, seq:= (LAMBDA (nn:nat): IF nn = 0 THEN a ELSIF nn = Pcd`length+1 THEN (("1" (inst + "Pab") (("1" (hide -1) (("1" (expand "Pab" +) (("1" (expand "variation_on") (("1" (expand "sigma" + 2) (("1" (case "sigma[below(Pcd`length - 1)] (0, Pcd`length - 2, LAMBDA (n: below(Pcd`length - 1)): abs(f(Pcd`seq(1 + n)) - f(Pcd`seq(n)))) <= sigma(0, Pcd`length - 1, LAMBDA (n: below(1 + Pcd`length)): abs(IF n = Pcd`length THEN f(b) ELSE f(Pcd`seq(n)) ENDIF - IF n = 0 THEN f(a) ELSE f(Pcd`seq(n - 1)) ENDIF))") (("1" (assert) nil nil) ("2" (hide 2) (("2" (lemma "sigma_split[below(1+Pcd`length)]") (("2" (inst - "LAMBDA (n: below(1 + Pcd`length)): abs(IF n = Pcd`length THEN f(b) ELSE f(Pcd`seq(n)) ENDIF - IF n = 0 THEN f(a) ELSE f(Pcd`seq(n - 1)) ENDIF)" "Pcd`length-1" "0" "0") (("1" (assert) (("1" (expand "sigma" - 2) (("1" (expand "sigma" - 2) (("1" (case "sigma[below(Pcd`length - 1)] (0, Pcd`length - 2, LAMBDA (n: below(Pcd`length - 1)): abs(f(Pcd`seq(1 + n)) - f(Pcd`seq(n)))) = sigma[below(1+Pcd`length)](1, Pcd`length - 1, LAMBDA (n: below(1 + Pcd`length)): abs(IF n = Pcd`length THEN f(b) ELSE f(Pcd`seq(n)) ENDIF - IF n = 0 THEN f(a) ELSE f(Pcd`seq(n - 1)) ENDIF))") (("1" (assert) nil nil) ("2" (hide 2) (("2" (hide -1) (("2" (case "FORALL (nn:nat): nn <= Pcd`length-2 IMPLIES sigma[below(Pcd`length - 1)] (0, nn, LAMBDA (n: below(Pcd`length - 1)): abs(f(Pcd`seq(1 + n)) - f(Pcd`seq(n)))) = sigma[below(1 + Pcd`length)] (1, 1+nn, LAMBDA (n: below(1 + Pcd`length)): abs(IF n = Pcd`length THEN f(b) ELSE f(Pcd`seq(n)) ENDIF - IF n = 0 THEN f(a) ELSE f(Pcd`seq(n - 1)) ENDIF))") (("1" (inst - "Pcd`length-2") (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (induct "nn") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (propax) nil nil)) nil)) nil) ("2" (skolem 1 "nn") (("2" (flatten) (("2" (assert) (("2" (expand "sigma" +) (("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil) ("4" (hide 2) (("4" (skosimp*) (("4" (assert) nil nil)) nil)) nil) ("5" (hide 2) (("5" (skosimp*) (("5" (assert) nil nil)) nil)) nil) ("6" (hide 2) (("6" (skosimp*) (("6" (assert) nil nil)) nil)) nil) ("7" (hide 2) (("7" (skosimp*) (("7" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil) ("4" (hide 2) (("4" (skosimp*) (("4" (assert) nil nil)) nil)) nil) ("5" (hide 2) (("5" (skosimp*) (("5" (assert) nil nil)) nil)) nil) ("6" (hide 2) (("6" (skosimp*) (("6" (assert) nil nil)) nil)) nil) ("7" (hide 2) (("7" (skosimp*) (("7" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil) ("4" (hide 2) (("4" (skosimp*) (("4" (assert) nil nil)) nil)) nil) ("5" (hide 2) (("5" (skosimp*) (("5" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (assert) (("2" (expand "Pab" +) (("2" (split +) (("1" (skeep) (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil) ("2" (expand "increasing?") (("2" (skosimp*) (("2" (lift-if) (("2" (lift-if) (("2" (assert) (("2" (ground) (("1" (typepred "Pcd") (("1" (inst - "i!1-1") (("1" (ground) nil nil)) nil)) nil) ("2" (typepred "Pcd") (("2" (inst - "j!1-1") (("2" (ground) nil nil)) nil)) nil) ("3" (typepred "Pcd") (("3" (expand "increasing?") (("3" (inst - "i!1-1" "j!1-1") (("3" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skeep) (("3" (lift-if) (("3" (assert) (("3" (typepred "Pcd") (("3" (inst - "i-1") (("1" (ground) nil nil) ("2" (assert) (("2" (typepred "i") (("2" (expand "Pab" -1) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ((sigma def-decl "real" sigma "reals/") (sigma_split formula-decl nil sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (barray type-eq-decl nil fseqs "structures/") (fseq type-eq-decl nil fseqs "structures/") (increasing? const-decl "bool" sort_fseq "structures/") (default const-decl "T" fseqs "structures/")) shostak)) (BV_subset_TCC1 0 (BV_subset_TCC1-1 nil 3492516564 ("" (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) (T_pred const-decl "[real -> boolean]" bounded_variation nil) (T formal-nonempty-subtype-decl nil bounded_variation nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (BV_subset 0 (BV_subset-1 nil 3492516564 ("" (skeep) (("" (expand "bounded_variation?") (("" (skosimp*) (("" (inst + "M!1") (("" (skosimp*) (("" (lemma "variation_on_subset") (("" (inst - "a" "b" "c" "d" "f") (("" (assert) (("" (inst - "P!1") (("" (skosimp*) (("" (inst - "Pab!1") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((bounded_variation? const-decl "bool" bounded_variation 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) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (variation_on_subset formula-decl nil bounded_variation nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (partition type-eq-decl nil rs_partition nil) (below 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) (increasing? const-decl "bool" sort_fseq "structures/") (<= const-decl "bool" reals nil) (restrict const-decl "R" restrict nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (> const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (fseq type-eq-decl nil fseqs "structures/") (barray type-eq-decl nil fseqs "structures/") (nat nonempty-type-eq-decl nil naturalnumbers nil) (T_pred const-decl "[real -> boolean]" bounded_variation nil) (T formal-nonempty-subtype-decl nil bounded_variation nil)) shostak)) (total_variation_TCC1 0 (total_variation_TCC1-1 nil 3492517261 ("" (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) (T_pred const-decl "[real -> boolean]" bounded_variation nil) (T formal-nonempty-subtype-decl nil bounded_variation nil) (< const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_le_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) (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) (partition type-eq-decl nil rs_partition nil) (below type-eq-decl nil naturalnumbers 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) (increasing? const-decl "bool" sort_fseq "structures/") (restrict const-decl "R" restrict nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (fseq type-eq-decl nil fseqs "structures/") (barray type-eq-decl nil fseqs "structures/") (nat nonempty-type-eq-decl nil naturalnumbers nil) (> const-decl "bool" reals nil)) nil)) (total_variation_TCC2 0 (total_variation_TCC2-1 nil 3492517261 ("" (subtype-tcc) nil nil) ((nnreal type-eq-decl nil real_types nil) (bounded_variation? const-decl "bool" bounded_variation nil) (NOT const-decl "[bool -> bool]" booleans 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) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (variation_on const-decl "nnreal" bounded_variation nil) (real_minus_real_is_real application-judgement "real" reals nil) (int_minus_int_is_int application-judgement "int" integers nil) (partition type-eq-decl nil rs_partition nil) (below 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) (increasing? const-decl "bool" sort_fseq "structures/") (restrict const-decl "R" restrict nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (> const-decl "bool" reals nil) (fseq type-eq-decl nil fseqs "structures/") (barray type-eq-decl nil fseqs "structures/") (nat nonempty-type-eq-decl nil naturalnumbers nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (< const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (T formal-nonempty-subtype-decl nil bounded_variation nil) (T_pred const-decl "[real -> boolean]" bounded_variation 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)) nil)) (total_variation_TCC3 0 (total_variation_TCC3-1 nil 3492517261 ("" (case "FORALL (a: T, b: {b | a < b}, f:(bounded_variation?(a, b)), x:(closed_intv(a,b))): EXIS (x>a IMPLIES FORALL (P:partition(a,x)): variation_on(a,x,P)(f)<=M) AND (FORALL (M1: nnreal): M1 < M IMPLIES EXISTS (P:partition(a,x)): variation_on(a,x,P)(f) > M1)") (("1" (inst + "(LAMBDA (a: T, b: {b | a < b}, f: (bounded_variation?(a, b))): (LAMBDA (x:(closed_intv(a,b))) (x > a IMPLIES (FORALL (P: partition(a, x)): variation_on(a, x, P)(f) <= M)) AND (FORALL (M1: nnreal): M1 < M IMPLIES (EXISTS (P: partition(a, x)): variation_on(a, x, P)(f) > M1))})))") (("1" (skeep) (("1" (inst - "a" "b" "f" "x") (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (skosimp*) (("1" (inst - "M!1") (("1" (expand "member") (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skeep) (("2" (skeep) (("2" (skeep) (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (skeep) (("3" (skeep) (("3" (lemma "not_one_element") (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (case "NOT a!1<x!1") (("1" (assert) (("1" (inst + "0") (("1" (assert) nil nil)) nil)) nil) ("2" (assert) (("2" (name "Aset" "{M : nnreal | FORALL (P: partition(a!1, x!1)): variation_on(a!1, x!1, P)(f!1) <= M}") (("2" (name "MM" "glb(Aset)") (("1" (inst + "MM") (("1" (typepred "MM") (("1" (expand "greatest_lower_bound?") (("1" (flatten) (("1" (split) (("1" (skosimp*) (("1" (inst?) (("1" (assert) (("1" (hide 1) (("1" (expand "lower_bound?" +) (("1" (skeep) (("1" (typepred "s") (("1" (expand "extend" -1) (("1" (ground) (("1" (expand "Aset" -2) (("1" (inst - "P!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skeep) (("2" (expand "lower_bound?" -2) (("2" (inst - "M1") (("1" (assert) nil nil) ("2" (expand "extend" +) (("2" (expand "Aset" +) (("2" (skosimp*) (("2" (inst + "P!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "MM") (("2" (expand "greatest_lower_bound?") (("2" (flatten) (("2" (inst - "0") (("2" (assert) (("2" (expand "lower_bound?" +) (("2" (skeep) (("2" (typepred "s") (("2" (expand "extend" -1) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (name "MZ" "glb(extend[real, nnreal, bool, FALSE](Aset))") (("2" (replace -1) (("2" (expand "greatest_lower_bound?") (("2" (split) (("1" (expand "lower_bound?" +) (("1" (skeep) (("1" (typepred "s") (("1" (typepred "MZ") (("1" (expand "greatest_lower_bound?") (("1" (flatten) (("1" (expand "lower_bound?" -1) (("1" (inst - "s") (("1" (expand "extend") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "MZ") (("2" (expand "greatest_lower_bound?") (("2" (flatten) (("2" (skeep) (("2" (inst - "y") (("2" (assert) (("2" (expand "lower_bound?" (+ -2)) (("2" (skeep) (("2" (inst - "s") (("2" (typepred "s") (("2" (assert) (("2" (expand "extend" -1) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (split +) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (typepred "f!1") (("1" (expand "bounded_variation?") (("1" (skosimp*) (("1" (inst -2 "M!1") (("1" (expand "member") (("1" (expand "extend") (("1" (expand "Aset" +) (("1" (skeep) (("1" (lemma "variation_on_subset") (("1" (inst - "a!1" "b!1" "a!1" "x!1" "f!1") (("1" (assert) (("1" (inst - "P") (("1" (skosimp*) (("1" (inst - "Pab!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "bounded_below?") (("2" (inst + "0") (("2" (expand "lower_bound?") (("2" (skeep) (("2" (typepred "s") (("2" (expand "extend") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skeep) (("3" (skeep) (("3" (skeep) (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("4" (hide 2) (("4" (skeep) (("4" (skeep) (("4" (lemma "not_one_element") (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((NOT const-decl "[bool -> bool]" booleans nil) (variation_on_subset formula-decl nil bounded_variation nil) (s skolem-const-decl "(Aset)" bounded_variation nil) (s skolem-const-decl "(extend[real, nnreal, bool, FALSE](Aset))" bounded_variation nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (Aset skolem-const-decl "[nnreal -> boolean]" bounded_variation nil) (MM skolem-const-decl "{x | greatest_lower_bound?(x, extend[real, nnreal, bool, FALSE](Aset))}" bounded_variation nil) (lower_bound? const-decl "bool" bounded_real_defs nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (M1 skolem-const-decl "nnreal" bounded_variation nil) (extend const-decl "R" extend nil) (FALSE const-decl "bool" booleans nil) (glb const-decl "{x | greatest_lower_bound?(x, SB)}" bounded_real_defs nil) (greatest_lower_bound? const-decl "bool" bounded_real_defs nil) (bounded_below? const-decl "bool" bounded_real_defs nil) (set type-eq-decl nil sets nil) (nonempty? const-decl "bool" sets nil) (choose const-decl "(p)" sets nil) (empty? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (not_one_element formula-decl nil bounded_variation 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) (T_pred const-decl "[real -> boolean]" bounded_variation nil) (T formal-nonempty-subtype-decl nil bounded_variation nil) (bool nonempty-type-eq-decl nil booleans nil) (< const-decl "bool" reals nil) (bounded_variation? const-decl "bool" bounded_variation nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (> const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (barray type-eq-decl nil fseqs "structures/") (fseq type-eq-decl nil fseqs "structures/") (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (restrict const-decl "R" restrict nil) (increasing? const-decl "bool" sort_fseq "structures/") (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) (below type-eq-decl nil naturalnumbers nil) (partition type-eq-decl nil rs_partition nil) (variation_on const-decl "nnreal" bounded_variation nil)) nil)) (total_variation_approx_TCC1 0 (total_variation_approx_TCC1-1 nil 3492522957 ("" (subtype-tcc) nil nil) ((NOT const-decl "[bool -> bool]" booleans nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props 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) (nnreal type-eq-decl nil real_types nil) (variation_on const-decl "nnreal" bounded_variation nil) (bounded_variation? const-decl "bool" bounded_variation nil) (/= const-decl "boolean" notequal nil) (real_minus_real_is_real application-judgement "real" reals nil) (int_minus_int_is_int application-judgement "int" integers nil) (partition type-eq-decl nil rs_partition nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals 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) (increasing? const-decl "bool" sort_fseq "structures/") (<= const-decl "bool" reals nil) (restrict const-decl "R" restrict nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (> const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (fseq type-eq-decl nil fseqs "structures/") (barray type-eq-decl nil fseqs "structures/") (nat nonempty-type-eq-decl nil naturalnumbers nil) (T formal-nonempty-subtype-decl nil bounded_variation nil) (T_pred const-decl "[real -> boolean]" bounded_variation 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)) nil)) (total_variation_approx 0 (total_variation_approx-1 nil 3492522958 ("" (skeep) (("" (skosimp 1) (("" (skeep 2) (("" (typepred "x!1") (("" (name "MM" "total_variation(a,b,f)(x!1)") (("1" (replace -1) (("1" (case "epsi > MM") (("1" (lemma "partition_exists") (("1" (inst - "a" "x!1" "1") (("1" (assert) (("1" (skeep -) (("1" (inst + "P") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "MM") (("2" (inst - "MM-epsi") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ((<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (T formal-nonempty-subtype-decl nil bounded_variation nil) (T_pred const-decl "[real -> boolean]" bounded_variation 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) (minus_odd_is_odd application-judgement "odd_int" integers nil) (a skolem-const-decl "T" bounded_variation nil) (b skolem-const-decl "T" bounded_variation nil) (x!1 skolem-const-decl "(LAMBDA (x: T): a <= x AND x <= b)" bounded_variation nil) (f skolem-const-decl "[T -> real]" bounded_variation nil) (MM skolem-const-decl "{M: nnreal | (x!1 = a IMPLIES M = 0) AND (x!1 > a IMPLIES (FORALL (P: partition(a, x!1)): variation_on(a, x!1, P)(f) <= M)) AND (FORALL (M1: nnreal): M1 < M IMPLIES (EXISTS (P: partition(a, x!1)): variation_on(a, x!1, P)(f) > M1))}" bounded_variation nil) (epsi skolem-const-decl "posreal" bounded_variation nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (partition_exists formula-decl nil rs_partition nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_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) (real_minus_real_is_real application-judgement "real" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (< const-decl "bool" reals nil) (bounded_variation? const-decl "bool" bounded_variation nil) (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (> const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (barray type-eq-decl nil fseqs "structures/") (fseq type-eq-decl nil fseqs "structures/") (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (restrict const-decl "R" restrict nil) (increasing? const-decl "bool" sort_fseq "structures/") (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) (below type-eq-decl nil naturalnumbers nil) (partition type-eq-decl nil rs_partition nil) (variation_on const-decl "nnreal" bounded_variation nil) (total_variation const-decl "{M: nnreal | (x = a IMPLIES M = 0) AND (x > a IMPLIES (FORALL (P: partition(a, x)): variation_on(a, x, P)(f) <= M)) AND (FORALL (M1: nnreal): M1 < M IMPLIES (EXISTS (P: partition(a, x)): variation_on(a, x, P)(f) > M1))}" bounded_variation nil)) shostak)) (BV_decomposition 0 (BV_decomposition-3 nil 3495206845 ("" (auto-rewrite + "member") (("" (skeep) (("" (name "CI" "closed_intv(a,b)") (("1" (replace -1) (("1" (label "CIname" -1) (("1" (ground) (("1" (label "fBV" -1) (("1" (label "altb" -3) (("1" (name "gg" "(LAMBDA (x:T): IF CI(x) THEN total_variation(a,b,f)(x) ELSE f(x) ENDIF)") (("1" (name "hh" "(LAMBDA (x:T): IF CI(x) THEN total_variation(a,b,f)(x)-f(x) ELSE 0 ENDIF)") (("1" (inst + "gg" "hh") (("1" (case "NOT increasing?[(CI)](restrict[T, (CI), real](gg))") (("1" (hide 2) (("1" (hide (-1 -2)) (("1" (expand "increasing?") (("1" (skosimp*) (("1" (case "y!1 = a or x!1 = a") (("1" (split -) (("1" (expand "restrict") (("1" (typepred "x!1") (("1" (typepred "y!1") (("1" (expand "CI") (("1" (ground) nil nil)) nil)) nil)) nil)) nil) ("2" (typepred "total_variation(a, b, f)(x!1)") (("1" (expand "restrict") (("1" (expand "gg") (("1" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (assert) (("2" (flatten) (("2" (lemma "total_variation_approx") (("2" (inst - "a" "b" "f") (("2" (assert) (("2" (inst - "x!1") (("1" (assert) (("1" (inst - "total_variation(a, b, f)(x!1) - total_variation(a, b, f)(y!1)") (("1" (skosimp*) (("1" (assert) (("1" (lemma "variation_on_subset") (("1" (inst - "a" "y!1" "a" "x!1" "f") (("1" (assert) (("1" (split -) (("1" (inst - "P!1") (("1" (skeep -) (("1" (typepred "total_variation(a,b,f)(y!1)") (("1" (split -3) (("1" (inst - "Pab") (("1" (assert) nil nil)) nil) ("2" (typepred "y!1") (("2" (expand "CI") (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "x!1") (("2" (expand "CI") (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "restrict") (("2" (expand "gg") (("2" (assert) nil nil)) nil)) nil) ("3" (typepred "y!1") (("3" (expand "CI") (("3" (propax) nil nil)) nil)) nil) ("4" (typepred "x!1") (("4" (expand "CI") (("4" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (typepred "x!1") (("2" (expand "CI") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (label "gginc" -1) (("2" (hide (-2 -3)) (("2" (split +) (("1" (decompose-equality) (("1" (expand "gg" +) (("1" (expand "hh" +) (("1" (lift-if) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil) ("3" (expand "increasing?" +) (("3" (skosimp*) (("3" (expand "restrict") (("3" (typepred "x!1") (("3" (typepred "y!1") (("3" (expand "CI" -) (("3" (flatten) (("3" (expand "hh") (("3" (name "epsi" "total_variation(a, b, f)(x!1) - f(x!1) - total_variation(a, b, f)(y!1) + f(y!1)") (("3" (case "f(x!1) >= f(y!1)") (("1" (case "total_variation(a,b,f)(x!1) <= total_variation(a,b,f)(y!1)") (("1" (assert) nil nil) ("2" (hide 2) (("2" (expand "increasing?") (("2" (inst - "x!1" "y!1") (("2" (assert) (("2" (expand "gg") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "NOT f(x!1)<f(y!1)") (("1" (assert) nil nil) ("2" (hide 1) (("2" (label "fxylt" -1) (("2" (lemma "total_variation_approx") (("2" (inst - "a" "b" "f") (("2" (assert) (("2" (inst - "x!1") (("2" (assert) (("2" (case "a<x!1") (("1" (assert) (("1" (label "altx" -1) (("1" (inst - "epsi") (("1" (skolem -2 "Pax") (("1" (case "variation_on(a,x!1,Pax)(f) + f(y!1)-f(x!1) <= total_variation(a,b,f)(y!1)") (("1" (assert) nil nil) ("2" (hide 2) (("2" (case "EXISTS (Pay:partition(a,y!1)): variation_on(a, x!1, Pax)(f) + f(y!1) - f(x!1) = variation (("1" (skeep -) (("1" (replace -1) (("1" (typepred "total_variation(a,b,f)(y!1)") (("1" (assert) (("1" (inst - "Pay") nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (name "Pay" "(# length := Pax`length+1, seq:= (LAMBDA (nn:nat): IF nn>=Pax`length+1 THEN default[T] ELSI (("2" (inst + "Pay") (("1" (expand "variation_on" +) (("1" (expand "sigma" + 2) (("1" (assert) (("1" (expand "Pay" +) (("1" (assert) (("1" (expand "abs" + 2) (("1" (case "FORALL (mm:below(Pax`length-1)): sigma[below(Pax`length - 1)] (0, mm, LAMBDA (n: below(Pax`length - 1)): abs(f(Pax`seq(1 + n)) - f(Pax`seq(n)))) = sigma(0, mm, LAMBDA (n: below(Pay`length - 1)): abs(IF 1 + n = Pax`length THEN f(y!1) ELSE f(Pax`seq(1 + n)) ENDIF - f(Pax`seq(n))))") (("1" (inst - "Pax`length-2") (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (induct "mm") (("1" (assert) (("1" (expand "sigma") (("1" (expand "sigma") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (skolem 1 "mm") (("2" (flatten) (("2" (expand "sigma" +) (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil) ("4" (hide 2) (("4" (skosimp*) (("4" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil) ("4" (hide 2) (("4" (skosimp*) (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "Pay" +) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "Pay" +) (("2" (assert) (("2" (split +) (("1" (skeep) (("1" (lift-if) (("1" (assert) nil nil)) nil)) nil) ("2" (expand "increasing?") (("2" (skeep) (("2" (lift-if) (("2" (lift-if) (("2" (lift-if) (("2" (lift-if) (("2" (assert) (("2" (typepred "Pax") (("2" (inst - "i") (("2" (assert) (("2" (flatten) (("2" (expand "increasing?") (("2" (inst - "i" "j") (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skeep) (("3" (lift-if) (("3" (assert) (("3" (typepred "Pax") (("3" (inst - "i") (("1" (ground) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "a = x!1") (("1" (hide -2) (("1" (case "total_variation(a,b,f)(x!1) = 0") (("1" (replace -1) (("1" (assert) (("1" (name "Pxy" "(# length := 2, seq := (LAMBDA (nn:nat): IF nn=0 THEN a ELSIF nn = 1 THEN y!1 ELSE default[T] ENDIF (("1" (typepred "total_variation(a,b,f)(y!1)") (("1" (assert) (("1" (inst - "Pxy") (("1" (case "variation_on(a,y!1,Pxy)(f) = abs(f(y!1)-f(x!1))") (("1" (expand "abs") (("1" (assert) nil nil)) nil) ("2" (expand "Pxy" +) (("2" (expand "variation_on" +) (("2" (expand "sigma" +) (("2" (expand "sigma" +) (("2" (replace -7) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 3) (("2" (split +) (("1" (skeep) (("1" (assert) (("1" (expand "Pxy") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (expand "Pxy") (("2" (propax) nil nil)) nil) ("3" (expand "Pxy") (("3" (propax) nil nil)) nil) ("4" (expand "increasing?") (("4" (skeep) (("4" (expand "Pxy") (("4" (lift-if) (("4" (lift-if) (("4" (lift-if) (("4" (lift-if) (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("5" (skeep) (("5" (expand "Pxy") (("5" (lift-if) (("5" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "total_variation(a,b,f)(x!1)") (("2" (assert) nil nil)) nil)) nil)) nil) ("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)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skeep) (("2" (expand "CI") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skeep -) (("2" (lemma "BV_sub") (("2" (inst - "a" "b" "g" "h") (("2" (assert) (("2" (lemma "monotonic_BV") (("2" (inst-cp - "a" "g" "b") (("2" (inst - "a" "h" "b") (("2" (split +) (("1" (assert) (("1" (expand "monotonic?" +) (("1" (flatten) (("1" (expand "increasing?") (("1" (skosimp*) (("1" (inst - "x!1" "y!1") (("1" (assert) (("1" (expand "restrict") (("1" (propax) nil nil)) nil)) nil) ("2" (expand "CI") (("2" (propax) nil nil)) nil) ("3" (expand "CI") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "monotonic?" +) (("2" (flatten) (("2" (expand "increasing?") (("2" (skosimp*) (("2" (inst - "x!1" "y!1") (("1" (inst - "x!1" "y!1") (("1" (assert) (("1" (expand "restrict") (("1" (propax) nil nil)) nil)) nil) ("2" (expand "CI") (("2" (propax) nil nil)) nil) ("3" (expand "CI") (("3" (propax) nil nil)) nil)) nil) ("2" (expand "CI") (("2" (propax) nil nil)) nil) ("3" (expand "CI") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ((real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_minus_real_is_real application-judgement "real" reals nil) (NOT const-decl "[bool -> bool]" booleans nil) (increasing? const-decl "bool" real_fun_preds "reals/") (total_variation_approx formula-decl nil bounded_variation nil) (variation_on_subset formula-decl nil bounded_variation nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (posreal nonempty-type-eq-decl nil real_types nil) (f skolem-const-decl "[T -> real]" bounded_variation nil) (y!1 skolem-const-decl "(CI)" bounded_variation nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (b skolem-const-decl "T" bounded_variation nil) (x!1 skolem-const-decl "(CI)" bounded_variation nil) (a skolem-const-decl "T" bounded_variation nil) (CI skolem-const-decl "[T -> bool]" bounded_variation nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (gg skolem-const-decl "[T -> real]" bounded_variation nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (real_plus_real_is_real application-judgement "real" reals nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (int_minus_int_is_int application-judgement "int" integers nil) (Pay skolem-const-decl "[# length: posint, seq: [nat -> T] #]" bounded_variation nil) (y!1 skolem-const-decl "(CI)" bounded_variation nil) (sigma def-decl "real" sigma "reals/") (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (below_induction formula-decl nil bounded_nat_inductions nil) (pred type-eq-decl nil defined_types nil) (Pax skolem-const-decl "partition[T](a, x!1)" bounded_variation nil) (x!1 skolem-const-decl "(CI)" bounded_variation nil) (integer nonempty-type-from-decl nil integers nil) (- const-decl "[numfield -> numfield]" number_fields nil) (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (sigma_nnreal application-judgement "nnreal" sigma_below "reals/") (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (i skolem-const-decl "below(Pay`length)" bounded_variation nil) (default const-decl "T" fseqs "structures/") (posint nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_times_real_is_real application-judgement "real" reals nil) (Pxy skolem-const-decl "[# length: posint, seq: [nat -> T] #]" bounded_variation nil) (hh skolem-const-decl "[T -> real]" bounded_variation nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (< const-decl "bool" reals nil) (bounded_variation? const-decl "bool" bounded_variation nil) (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (> const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (barray type-eq-decl nil fseqs "structures/") (fseq type-eq-decl nil fseqs "structures/") (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (restrict const-decl "R" restrict nil) (increasing? const-decl "bool" sort_fseq "structures/") (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) (below type-eq-decl nil naturalnumbers nil) (partition type-eq-decl nil rs_partition nil) (variation_on const-decl "nnreal" bounded_variation nil) (total_variation const-decl "{M: nnreal | (x = a IMPLIES M = 0) AND (x > a IMPLIES (FORALL (P: partition(a, x)): variation_on(a, x, P)(f) <= M)) AND (FORALL (M1: nnreal): M1 < M IMPLIES (EXISTS (P: partition(a, x)): variation_on(a, x, P)(f) > M1))}" bounded_variation nil) (BV_sub formula-decl nil bounded_variation nil) (monotonic? const-decl "bool" real_fun_preds "reals/") (x!1 skolem-const-decl "(LAMBDA (x: T): a <= x AND x <= b)" bounded_variation nil) (y!1 skolem-const-decl "(LAMBDA (x: T): a <= x AND x <= b)" bounded_variation nil) (x!1 skolem-const-decl "(LAMBDA (x: T): a <= x AND x <= b)" bounded_variation nil) (y!1 skolem-const-decl "(LAMBDA (x: T): a <= x AND x <= b)" bounded_variation nil) (monotonic_BV formula-decl nil bounded_variation nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props 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) (T_pred const-decl "[real -> boolean]" bounded_variation nil) (T formal-nonempty-subtype-decl nil bounded_variation nil) (bool nonempty-type-eq-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil)) nil) (BV_decomposition-2 nil 3494862354 ("" (skeep) (("" (name "CI" "closed_intv(a,b)") (("" (replace -1) (("" (label "CIname" -1) (("" (ground) (("1" (label "fBV" -1) (("1" (label "altb" -3) (("1" (name "gg" "(LAMBDA (x:T): IF CI(x) THEN total_variation(a,b,f)(x) ELSE f(x) ENDIF)") (("1" (name "hh" "(LAMBDA (x:T): IF CI(x) THEN total_variation(a,b,f)(x)-f(x) ELSE 0 ENDIF)") (("1" (inst + "gg" "hh") (("1" (case "NOT increasing?[(CI)](restrict[T, (CI), real](gg))") (("1" (hide 2) (("1" (hide (-1 -2)) (("1" (expand "increasing?") (("1" (skosimp*) (("1" (case "y!1 = a or x!1 = a") (("1" (split -) (("1" (expand "restrict") (("1" (typepred "x!1") (("1" (typepred "y!1") (("1" (expand "CI") (("1" (ground) nil nil)) nil)) nil)) nil)) nil) ("2" (typepred "total_variation(a, b, f)(x!1)") (("1" (expand "restrict") (("1" (expand "gg") (("1" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (assert) (("2" (flatten) (("2" (lemma "total_variation_approx") (("2" (inst - "a" "b" "f") (("2" (assert) (("2" (inst - "x!1") (("1" (assert) (("1" (inst - "total_variation(a, b, f)(x!1) - total_variation(a, b, f)(y!1)") (("1" (skosimp*) (("1" (assert) (("1" (lemma "variation_on_subset") (("1" (inst - "a" "y!1" "a" "x!1" "f") (("1" (assert) (("1" (split -) (("1" (inst - "P!1") (("1" (skeep -) (("1" (typepred "total_variation(a,b,f)(y!1)") (("1" (split -3) (("1" (inst - "Pab") (("1" (assert) nil nil)) nil) ("2" (typepred "y!1") (("2" (expand "CI") (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "x!1") (("2" (expand "CI") (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "restrict") (("2" (expand "gg") (("2" (assert) nil nil)) nil)) nil) ("3" (typepred "y!1") (("3" (expand "CI") (("3" (propax) nil nil)) nil)) nil) ("4" (typepred "x!1") (("4" (expand "CI") (("4" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (typepred "x!1") (("2" (expand "CI") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (label "gginc" -1) (("2" (hide (-2 -3)) (("2" (split +) (("1" (decompose-equality) (("1" (expand "gg" +) (("1" (expand "hh" +) (("1" (lift-if) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil) ("3" (expand "increasing?" +) (("3" (skosimp*) (("3" (expand "restrict") (("3" (typepred "x!1") (("3" (typepred "y!1") (("3" (expand "CI" -) (("3" (flatten) (("3" (expand "hh") (("3" (name "epsi" "total_variation(a, b, f)(x!1) - f(x!1) - total_variation(a, b, f)(y!1) + f(y!1)") (("3" (case "f(x!1) >= f(y!1)") (("1" (case "total_variation(a,b,f)(x!1) <= total_variation(a,b,f)(y!1)") (("1" (assert) nil nil) ("2" (hide 2) (("2" (expand "increasing?") (("2" (inst - "x!1" "y!1") (("2" (assert) (("2" (expand "gg") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "NOT f(x!1)<f(y!1)") (("1" (assert) nil nil) ("2" (hide 1) (("2" (label "fxylt" -1) (("2" (lemma "total_variation_approx") (("2" (inst - "a" "b" "f") (("2" (assert) (("2" (inst - "x!1") (("2" (assert) (("2" (case "a<x!1") (("1" (assert) (("1" (label "altx" -1) (("1" (inst - "epsi") (("1" (skolem -2 "Pax") (("1" (case "variation_on(a,x!1,Pax)(f) + f(y!1)-f(x!1) <= total_variation(a,b,f)(y!1)") (("1" (assert) nil nil) ("2" (hide 2) (("2" (case "EXISTS (Pay:partition(a,y!1)): variation_on(a, x!1, Pax)(f) + f(y!1) - f(x!1) = variation (("1" (skeep -) (("1" (replace -1) (("1" (typepred "total_variation(a,b,f)(y!1)") (("1" (assert) (("1" (inst - "Pay") nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (name "Pay" "(# length := Pax`length+1, seq:= (LAMBDA (nn:nat): IF nn>=Pax`length+1 THEN default[T] ELSI (("2" (inst + "Pay") (("1" (expand "variation_on" +) (("1" (expand "sigma" + 2) (("1" (assert) (("1" (expand "Pay" +) (("1" (assert) (("1" (expand "abs" + 2) (("1" (case "FORALL (mm:below(Pax`length-1)): sigma[below(Pax`length - 1)] (0, mm, LAMBDA (n: below(Pax`length - 1)): abs(f(Pax`seq(1 + n)) - f(Pax`seq(n)))) = sigma(0, mm, LAMBDA (n: below(Pay`length - 1)): abs(IF 1 + n = Pax`length THEN f(y!1) ELSE f(Pax`seq(1 + n)) ENDIF - f(Pax`seq(n))))") (("1" (inst - "Pax`length-2") (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (induct "mm") (("1" (assert) (("1" (expand "sigma") (("1" (expand "sigma") (("1" (propax) nil nil)) nil)) nil) ("2" (hide 2) (("2" (expand "Pay" +) (("2" (propax) nil nil)) nil)) nil)) nil) ("2" (skolem 1 "mm") (("2" (flatten) (("2" (expand "sigma" +) (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil) ("4" (hide 2) (("4" (skosimp*) (("4" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil) ("4" (hide 2) (("4" (skosimp*) (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "Pay" +) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "Pay" +) (("2" (assert) (("2" (split +) (("1" (skeep) (("1" (lift-if) (("1" (assert) nil nil)) nil)) nil) ("2" (expand "increasing?") (("2" (skeep) (("2" (lift-if) (("2" (lift-if) (("2" (assert) (("2" (typepred "Pax") (("2" (inst - "i") (("2" (assert) (("2" (flatten) (("2" (expand "increasing?") (("2" (inst - "i" "j") (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skeep) (("3" (lift-if) (("3" (assert) (("3" (typepred "Pax") (("3" (inst - "i") (("1" (ground) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "a = x!1") (("1" (hide -2) (("1" (case "total_variation(a,b,f)(x!1) = 0") (("1" (replace -1) (("1" (assert) (("1" (name "Pxy" "(# length := 2, seq := (LAMBDA (nn:nat): IF nn=0 THEN a ELSIF nn = 1 THEN y!1 ELSE default[T] ENDIF (("1" (typepred "total_variation(a,b,f)(y!1)") (("1" (assert) (("1" (inst - "Pxy") (("1" (case "variation_on(a,y!1,Pxy)(f) = abs(f(y!1)-f(x!1))") (("1" (expand "abs") (("1" (assert) nil nil)) nil) ("2" (expand "Pxy" +) (("2" (expand "variation_on" +) (("2" (expand "sigma" +) (("2" (expand "sigma" +) (("2" (replace -7) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 3) (("2" (split +) (("1" (skeep) (("1" (assert) (("1" (expand "Pxy") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (expand "Pxy") (("2" (propax) nil nil)) nil) ("3" (expand "Pxy") (("3" (propax) nil nil)) nil) ("4" (expand "increasing?") (("4" (skeep) (("4" (expand "Pxy") (("4" (lift-if) (("4" (lift-if) (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("5" (skeep) (("5" (expand "Pxy") (("5" (lift-if) (("5" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "total_variation(a,b,f)(x!1)") (("2" (assert) nil nil)) nil)) nil)) nil) ("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)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skeep) (("2" (expand "CI") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skeep -) (("2" (lemma "BV_sub") (("2" (inst - "a" "b" "g" "h") (("2" (assert) (("2" (lemma "monotonic_BV") (("2" (inst-cp - "a" "g" "b") (("2" (inst - "a" "h" "b") (("2" (split +) (("1" (assert) (("1" (expand "monotonic?" +) (("1" (flatten) (("1" (expand "increasing?") (("1" (skosimp*) (("1" (inst - "x!1" "y!1") (("1" (assert) (("1" (expand "restrict") (("1" (propax) nil nil)) nil)) nil) ("2" (expand "CI") (("2" (propax) nil nil)) nil) ("3" (expand "CI") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "monotonic?" +) (("2" (flatten) (("2" (expand "increasing?") (("2" (skosimp*) (("2" (inst - "x!1" "y!1") (("1" (inst - "x!1" "y!1") (("1" (assert) (("1" (expand "restrict") (("1" (propax) nil nil)) nil)) nil) ("2" (expand "CI") (("2" (propax) nil nil)) nil) ("3" (expand "CI") (("3" (propax) nil nil)) nil)) nil) ("2" (expand "CI") (("2" (propax) nil nil)) nil) ("3" (expand "CI") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((increasing? const-decl "bool" real_fun_preds "reals/") (sigma def-decl "real" sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (default const-decl "T" fseqs "structures/") (barray type-eq-decl nil fseqs "structures/") (fseq type-eq-decl nil fseqs "structures/") (increasing? const-decl "bool" sort_fseq "structures/") (monotonic? const-decl "bool" real_fun_preds "reals/")) nil) (BV_decomposition-1 nil 3492521877 ("" (skeep) (("" (name "CI" "closed_intv(a,b)") (("" (replace -1) (("" (label "CIname" -1) (("" (ground) (("1" (label "fBV" -1) (("1" (label "altb" -3) (("1" (name "gg" "(LAMBDA (x:T): IF CI(x) THEN total_variation(a,b,f)(x) ELSE f(x) ENDIF)") (("1" (name "hh" "(LAMBDA (x:T): IF CI(x) THEN total_variation(a,b,f)(x)-f(x) ELSE 0 ENDIF)") (("1" (inst + "gg" "hh") (("1" (case "NOT increasing?[(CI)](restrict[real, (CI), real](gg))") (("1" (hide 2) (("1" (hide (-1 -2)) (("1" (expand "increasing?") (("1" (skosimp*) (("1" (case "y!1 = a or x!1 = a") (("1" (split -) (("1" (expand "restrict") (("1" (typepred "x!1") (("1" (typepred "y!1") (("1" (expand "CI") (("1" (ground) nil nil)) nil)) nil)) nil)) nil) ("2" (typepred "total_variation(a, b, f)(x!1)") (("1" (expand "restrict") (("1" (expand "gg") (("1" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (assert) (("2" (flatten) (("2" (lemma "total_variation_approx") (("2" (inst - "a" "b" "f") (("2" (assert) (("2" (inst - "x!1") (("1" (assert) (("1" (inst - "total_variation(a, b, f)(x!1) - total_variation(a, b, f)(y!1)") (("1" (skosimp*) (("1" (assert) (("1" (lemma "variation_on_subset") (("1" (inst - "a" "y!1" "a" "x!1" "f") (("1" (assert) (("1" (split -) (("1" (inst - "P!1") (("1" (skeep -) (("1" (typepred "total_variation(a,b,f)(y!1)") (("1" (split -3) (("1" (inst - "Pab") (("1" (assert) nil nil)) nil) ("2" (typepred "y!1") (("2" (expand "CI") (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "x!1") (("2" (expand "CI") (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "restrict") (("2" (expand "gg") (("2" (assert) nil nil)) nil)) nil) ("3" (typepred "y!1") (("3" (expand "CI") (("3" (propax) nil nil)) nil)) nil) ("4" (typepred "x!1") (("4" (expand "CI") (("4" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (typepred "x!1") (("2" (expand "CI") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (label "gginc" -1) (("2" (hide (-2 -3)) (("2" (split +) (("1" (decompose-equality) (("1" (expand "gg" +) (("1" (expand "hh" +) (("1" (lift-if) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "increasing?" +) (("2" (skosimp*) (("2" (typepred "x!1") (("2" (typepred "y!1") (("2" (expand "CI" -) (("2" (flatten) (("2" (expand "restrict") (("2" (expand "gg" +) (("2" (expand "increasing?") (("2" (inst - "x!1" "y!1") (("2" (expand "gg") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "increasing?" +) (("3" (skosimp*) (("3" (expand "restrict") (("3" (typepred "x!1") (("3" (typepred "y!1") (("3" (expand "CI" -) (("3" (flatten) (("3" (expand "hh") (("3" (name "epsi" "total_variation(a, b, f)(x!1) - f(x!1) - total_variation(a, b, f)(y!1) + f(y!1)") (("3" (case "f(x!1) >= f(y!1)") (("1" (case "total_variation(a,b,f)(x!1) <= total_variation(a,b,f)(y!1)") (("1" (assert) nil nil) ("2" (hide 2) (("2" (expand "increasing?") (("2" (inst - "x!1" "y!1") (("2" (assert) (("2" (expand "gg") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "NOT f(x!1)<f(y!1)") (("1" (assert) nil nil) ("2" (hide 1) (("2" (label "fxylt" -1) (("2" (lemma "total_variation_approx") (("2" (inst - "a" "b" "f") (("2" (assert) (("2" (inst - "x!1") (("2" (assert) (("2" (case "a<x!1") (("1" (assert) (("1" (label "altx" -1) (("1" (inst - "epsi") (("1" (skolem -2 "Pax") (("1" (case "variation_on(a,x!1,Pax)(f) + f(y!1)-f(x!1) <= total_variation(a,b,f)(y!1)") (("1" (assert) nil nil) ("2" (hide 2) (("2" (case "EXISTS (Pay:partition(a,y!1)): variation_on(a, x!1, Pax)(f) + f(y!1) - f(x!1) = variation (("1" (skeep -) (("1" (replace -1) (("1" (typepred "total_variation(a,b,f)(y!1)") (("1" (assert) (("1" (inst - "Pay") nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (name "Pay" "(# length := Pax`length+1, seq:= (LAMBDA (nn:nat): IF nn>=Pax`length+1 THEN default[T] ELSI (("2" (inst + "Pay") (("1" (expand "variation_on" +) (("1" (expand "sigma" + 2) (("1" (assert) (("1" (expand "Pay" +) (("1" (assert) (("1" (expand "abs" + 2) (("1" (case "FORALL (mm:below(Pax`length-1)): sigma[below(Pax`length - 1)] (0, mm, LAMBDA (n: below(Pax`length - 1)): abs(f(Pax`seq(1 + n)) - f(Pax`seq(n)))) = sigma(0, mm, LAMBDA (n: below(Pay`length - 1)): abs(IF 1 + n = Pax`length THEN f(y!1) ELSE f(Pax`seq(1 + n)) ENDIF - f(Pax`seq(n))))") (("1" (inst - "Pax`length-2") (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (induct "mm") (("1" (assert) (("1" (expand "sigma") (("1" (expand "sigma") (("1" (propax) nil nil)) nil)) nil) ("2" (hide 2) (("2" (expand "Pay" +) (("2" (propax) nil nil)) nil)) nil)) nil) ("2" (skolem 1 "mm") (("2" (flatten) (("2" (expand "sigma" +) (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil) ("4" (hide 2) (("4" (skosimp*) (("4" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil) ("4" (hide 2) (("4" (skosimp*) (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "Pay" +) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "Pay" +) (("2" (assert) (("2" (split +) (("1" (skeep) (("1" (lift-if) (("1" (assert) nil nil)) nil)) nil) ("2" (expand "increasing?") (("2" (skeep) (("2" (lift-if) (("2" (lift-if) (("2" (assert) (("2" (typepred "Pax") (("2" (inst - "i") (("2" (assert) (("2" (flatten) (("2" (expand "increasing?") (("2" (inst - "i" "j") (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skeep) (("3" (lift-if) (("3" (assert) (("3" (typepred "Pax") (("3" (inst - "i") (("1" (ground) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "a = x!1") (("1" (hide -2) (("1" (case "total_variation(a,b,f)(x!1) = 0") (("1" (replace -1) (("1" (assert) (("1" (name "Pxy" "(# length := 2, seq := (LAMBDA (nn:nat): IF nn=0 THEN a ELSIF nn = 1 THEN y!1 ELSE default[T] ENDIF (("1" (typepred "total_variation(a,b,f)(y!1)") (("1" (assert) (("1" (inst - "Pxy") (("1" (case "variation_on(a,y!1,Pxy)(f) = abs(f(y!1)-f(x!1))") (("1" (expand "abs") (("1" (assert) nil nil)) nil) ("2" (expand "Pxy" +) (("2" (expand "variation_on" +) (("2" (expand "sigma" +) (("2" (expand "sigma" +) (("2" (replace -7) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 3) (("2" (split +) (("1" (skeep) (("1" (assert) (("1" (expand "Pxy") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (expand "Pxy") (("2" (propax) nil nil)) nil) ("3" (expand "Pxy") (("3" (propax) nil nil)) nil) ("4" (expand "increasing?") (("4" (skeep) (("4" (expand "Pxy") (("4" (lift-if) (("4" (lift-if) (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("5" (skeep) (("5" (expand "Pxy") (("5" (lift-if) (("5" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "total_variation(a,b,f)(x!1)") (("2" (assert) nil nil)) nil)) nil)) nil) ("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)) nil)) nil) ("3" (postpone) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skeep) (("2" (expand "CI") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skeep -) (("2" (lemma "BV_sub") (("2" (inst - "a" "b" "g" "h") (("2" (assert) (("2" (lemma "monotonic_BV") (("2" (inst-cp - "a" "g" "b") (("2" (inst - "a" "h" "b") (("2" (split +) (("1" (assert) (("1" (expand "monotonic?" +) (("1" (flatten) (("1" (expand "increasing?") (("1" (skosimp*) (("1" (inst - "x!1" "y!1") (("1" (assert) (("1" (expand "restrict") (("1" (propax) nil nil)) nil)) nil) ("2" (expand "CI") (("2" (propax) nil nil)) nil) ("3" (expand "CI") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "monotonic?" +) (("2" (flatten) (("2" (expand "increasing?") (("2" (skosimp*) (("2" (inst - "x!1" "y!1") (("1" (inst - "x!1" "y!1") (("1" (assert) (("1" (expand "restrict") (("1" (propax) nil nil)) nil)) nil) ("2" (expand "CI") (("2" (propax) nil nil)) nil) ("3" (expand "CI") (("3" (propax) nil nil)) nil)) nil) ("2" (expand "CI") (("2" (propax) nil nil)) nil) ("3" (expand "CI") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((monotonic? const-decl "bool" real_fun_preds "reals/") (increasing? const-decl "bool" sort_fseq "structures/") (fseq type-eq-decl nil fseqs "structures/") (barray type-eq-decl nil fseqs "structures/") (default const-decl "T" fseqs "structures/") (T_low type-eq-decl nil sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (sigma def-decl "real" sigma "reals/") (increasing? const-decl "bool" real_fun_preds "reals/")) shostak)))
¤ 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.0.775Bemerkung: (vorverarbeitet am 2026-04-28) ¤*Bot Zugriff |
|
||||||||||||||
2026-05-26