Impressum rs_partition.prf
Sprache: Lisp
(rs_partitionnil 3511259225 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rs_partition nil )nil rs_partition nil )"bool" reals nil ) (>= const-decl "bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"T" fseqs "structures/" )"[T, T -> boolean]" equalities nil )nil fseqs "structures/" )nil fseqs "structures/" )"[bool, bool -> bool]" booleans nil ))nil ))nil 3491659656"" (auto-rewrite + "member" )"" (skeep)"" (skeep)"" (assert )"" (case "NOT strictly_sort(P)`length > 1" )"1" (hide 2)"1" (typepred "strictly_sort(P)" )"1" (inst-cp - "a" )"1" (inst - "b" )"1" (case "member(a,P) and member(b,P)" )"1" (flatten)"1" (replace -1)"1" (replace -2)"1" (expand "member" )"1" "1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (split +)"1" (inst + "0" ) (("1" (assert ) nil nil ))nil )"2" (inst + "P`length-1" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (split +)"1" (typepred "strictly_sort(P)" )"1" (inst-cp - "strictly_sort(P)`seq(0)" )"1" (inst - "a" )"1" case "member(a,P) AND member(strictly_sort(P)`seq(0), strictly_sort(P))" )"1" (flatten)"1" (replace -1)"1" (replace -2)"1" assert )"1" "1" "1" "1" expand "strictly_increasing?" )"1" "0" "i!1" )"1" assert )"1" "P" )"1" expand "increasing?" )"1" "0" "i!2" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (assert )"2" (split)"1" "0" )"1" (assert ) nil nil ))nil )"2" (inst + "0" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (typepred "strictly_sort(P)" )"2" "strictly_sort(P)`seq(strictly_sort(P)`length-1)" )"2" (inst - "b" )"2" case "member(b,P) AND member(strictly_sort(P)`seq(strictly_sort(P)`length-1), strictly_sort(P))" )"1" (flatten)"1" (replace -1)"1" replace -2)"1" assert )"1" "1" "1" "1" expand "strictly_increasing?" )"1" "i!1" "strictly_sort(P)`length-1" )"1" assert )"1" "P" )"1" expand "increasing?" )"1" "i!2" "P`length-1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (assert )"2" "1" "P`length-1" )"1" (assert ) nil nil ))nil )"2" "strictly_sort(P)`length-1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (typepred "strictly_sort(P)" )"3" (expand "strictly_increasing?" )"3" (expand "increasing?" )"3" (skeep)"3" (inst - "i" "j" ) (("3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"4" (skeep)"4" (typepred "strictly_sort(P)" )"4" (inst - "strictly_sort(P)`seq(i)" )"4" case "member(strictly_sort(P)`seq(i),strictly_sort(P))" )"1" (replace -1)"1" (hide -1)"1" (assert )"1" "iz" )"1" replace -2)"1" "P" )"1" (inst - "iz" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (assert ) (("2" (inst + "i" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"[bool, bool -> bool]" booleans nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"(total_order?[S])" nil )"(dichotomous?[S])" nil )"(partial_order?[S])" nil )"(preorder?[S])" nil )"(transitive?[S])" nil )"(antisymmetric?[S])" nil )"(reflexive?[S])" nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil naturalnumbers nil )"[real -> boolean]" rs_partition nil )nil rs_partition nil )nil fseqs "structures/" )nil fseqs "structures/" )AND const-decl "[bool, bool -> bool]" booleans nil )"R" restrict nil )"bool" reals nil )"bool" sort_fseq "structures/" )"[bool, bool -> bool]" booleans nil )"bool" fseqs "structures/" )"{ss: fseq | AND " sort_fseq "structures/" )"[T, T -> boolean]" equalities nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"bool" sort_fseq "structures/" )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil ) (< const-decl "bool" reals nil )nil naturalnumbers nil )nil rs_partition nil ))nil 3253536795"" (skeep)"" (skeep)"" (split +)"1" (lemma "is_finite_surj[real]" )"1" (inst?)"1" (assert )"1" (hide 2)"1" "N" "(LAMBDA (ij:below[N]): IF ij = N-1 THEN xx(ij)-xx(ij-1) ELSE xx(ij+1)-xx(ij) ENDIF)" )"1" (expand "surjective?" )"1" (skosimp*)"1" (typepred "y!1" )"1" (skosimp*)"1" (inst + "ii!1" )"1" (lift-if) (("1" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (inst + "ij!1" ) (("2" (assert ) nil nil ))nil ))nil )"3" (skosimp*)"3" (replace -1)"3" (assert )"3" (inst + "N-2" ) (("3" (assert ) nil nil ))nil ))nil ))nil ))nil )"4" (skosimp*) (("4" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "empty?" )"2" (inst - "xx(1)-xx(0)" )"2" (assert )"2" (inst + "0" ) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil )"bool" sets nil )"bool" sets nil )"odd_int" integers nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil finite_sets nil )"real" reals nil )"int" integers nil )"nat" rs_partition nil )nil nat_types nil )"barray[T](P`length)" rs_partition nil )"partition(a, b)" rs_partition nil )"{x: T | a < x}" rs_partition nil )"T" rs_partition nil )NOT const-decl "[bool -> bool]" booleans nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"posint" nil )"(strict_total_order?[real])" real_props nil )"bool" functions nil )"below[N]" rs_partition nil )"(total_order?[real])" nil )"int" integers nil )"[numfield, numfield -> numfield]" number_fields nil )"T" fseqs "structures/" )nil rs_partition nil )"bool" sort_fseq "structures/" )"bool" reals nil )"R" restrict nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil fseqs "structures/" )nil fseqs "structures/" )"[bool, bool -> bool]" booleans nil )nil rs_partition nil )"[real -> boolean]" rs_partition nil )"[T, T -> boolean]" equalities nil )nil naturalnumbers nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )set type-eq-decl nil sets nil )nil booleans nil )"posint" nil ))nil ))nil 3253536795"" (skosimp*)"" case "max[real, <=] ") "1" (assert ) nil nil )"2" (hide 2)"2" (typepred "P!1" )"2" case "EXISTS (ii: below(N!1 - 1)): xx!1(ii + 1) - xx!1(ii) > 0" )"1" "mm" "max[real, <=] ") "1" (replace -1)"1" (typepred "mm" )"1" (skosimp*)"1" (inst -2 "xx!1(ii!2 + 1) - xx!1(ii!2)" )"1" (assert ) (("1" (inst + "ii!2" ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (lemma "width_TCC1" )"2" (inst?)"2" (assert )"2" (inst - "N!1" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (case "FORALL (ii:below(N!1)): xx!1(ii) = a!1" )"1" (inst - "N!1-1" )"1" (assert ) nil nil ) ("2" (assert ) nil nil )) nil )"2" (induct "ii" )"1" (assert ) nil nil )"2" (skosimp*)"2" (assert )"2" (inst + "jb!1" )"2" (assert )"2" (inst - "jb!1+1" )"2" (inst - "jb!1+1" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (lemma "width_TCC1" )"3" (inst?)"3" (assert )"3" (inst - "N!1" ) (("3" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )"[numfield, numfield -> numfield]" number_fields nil )"T" fseqs "structures/" )nil rs_partition nil )"bool" sort_fseq "structures/" )"R" restrict nil )nil fseqs "structures/" )nil fseqs "structures/" )nil rs_partition nil )"[real -> boolean]" rs_partition nil )"[T, T -> boolean]" equalities nil )nil naturalnumbers nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )max const-decl"{a: T | SS(a) AND (FORALL (x: T): SS(x) IMPLIES x <= a)}" "finite_sets/" )"bool" reals nil )"[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil finite_sets nil )"bool" sets nil )NOT const-decl "[bool -> bool]" booleans nil )nil finite_sets nil )"bool" finite_sets nil )set type-eq-decl nil sets nil ) (> const-decl "bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"(total_order?[real])" nil )"posint" nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil defined_types nil )nil bounded_nat_inductions nil )"(strict_total_order?[real])" real_props nil )"nat" rs_partition nil )"posint" nil )"int" integers nil )nil rs_partition nil ))nil ))nil 3253536795"" (skosimp*)"" (assert )"" (expand "width" )"" "max({l: real | ") "1" (skosimp*)"1" (inst -2 "P!1`seq(1 + ii!1) - P!1`seq(ii!1)" )"1" (assert )"1" (hide -1 2) (("1" (inst?) nil nil )) nil )) nil ))nil ))nil )"2" (hide 2)"2" (lemma "width_TCC1" )"2" (inst - "a!1" "b!1" "P!1" "P!1`seq" )"2" (inst - "P!1`length" ) (("2" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"posint" nil )"real" reals nil )"(total_order?[real])" nil )"[numfield, numfield -> numfield]" number_fields nil )max const-decl"{a: T | SS(a) AND (FORALL (x: T): SS(x) IMPLIES x <= a)}" "finite_sets/" )"[bool, bool -> bool]" booleans nil )nil finite_sets nil )"bool" sets nil )nil finite_sets nil )"bool" finite_sets nil )set type-eq-decl nil sets nil )nil rs_partition nil )nil naturalnumbers nil )"bool" sort_fseq "structures/" )"bool" reals nil )"R" restrict nil )"[T, T -> boolean]" equalities nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil fseqs "structures/" )nil fseqs "structures/" )nil rs_partition nil )"[real -> boolean]" rs_partition nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"(total_order?[real])" nil )"posint" nil )nil rs_partition nil )"T" fseqs "structures/" )"posreal" rs_partition nil ))nil ))nil 3489487957"" (skeep)"" (skeep)"" (expand "width" )"" "max({l: real | ") "1" (propax) nil nil )"2" (hide 2)"2" (assert )"2" (lemma "width_TCC1" )"2" (inst - "a" "b" "P" "P`seq" )"2" (assert ) (("2" (inst - "P`length" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"[numfield, numfield -> numfield]" number_fields nil )max const-decl"{a: T | SS(a) AND (FORALL (x: T): SS(x) IMPLIES x <= a)}" "finite_sets/" )"[bool, bool -> bool]" booleans nil )nil finite_sets nil )"bool" sets nil )nil finite_sets nil )"bool" finite_sets nil )set type-eq-decl nil sets nil )nil rs_partition nil )nil naturalnumbers nil )"bool" sort_fseq "structures/" )"bool" reals nil )"R" restrict nil )"[T, T -> boolean]" equalities nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil fseqs "structures/" )nil fseqs "structures/" )nil rs_partition nil )"[real -> boolean]" rs_partition nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"(total_order?[real])" nil )"posint" nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"T" fseqs "structures/" )nil rs_partition nil )"posreal" rs_partition nil ))nil 3253536795"" (skeep)"" (typepred "P" )"" (expand "increasing?" )"" (inst?) (("" (assert ) nil nil )) nil )) nil ))nil ))nil )nil rs_partition nil )nil naturalnumbers nil )"bool" reals nil ) (>= const-decl "bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"bool" sort_fseq "structures/" )"bool" reals nil )"R" restrict nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[T, T -> boolean]" equalities nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil fseqs "structures/" )nil fseqs "structures/" )nil rs_partition nil )"[real -> boolean]" rs_partition nil )nil naturalnumbers nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3253536795"" (skosimp*)"" (case "ii!1 < jj!1" )"1" (case-replace "seq(P!1)(ii!1+1) < seq(P!1)(jj!1)" )"1" (assert ) nil nil )"2" (case "ii!1 + 1 = jj!1" )"1" (replace -1) (("1" (assert ) nil nil )) nil )"2" (lemma "parts_order" )"2" (inst - "a!1" "b!1" "P!1" "ii!1+1" "jj!1" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil )"2" (case-replace "seq(P!1)(jj!1+1) < seq(P!1)(ii!1)" )"1" (assert ) nil nil )"2" (case "jj!1 + 1 = ii!1" )"1" (replace -1) (("1" (assert ) nil nil )) nil )"2" (lemma "parts_order" )"2" (inst -1 "a!1" "b!1" "P!1" "jj!1+1" "ii!1" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )nil rs_partition nil )nil naturalnumbers nil )"bool" sort_fseq "structures/" )"bool" reals nil )"R" restrict nil )"[T, T -> boolean]" equalities nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil fseqs "structures/" )nil fseqs "structures/" )nil rs_partition nil )"[real -> boolean]" rs_partition nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"real" reals nil )"(total_order?[real])" nil )nil rs_partition nil )"posint" nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"[numfield, numfield -> numfield]" number_fields nil )"posint" nil ))nil ))nil 3281209744"" (skosimp*) (("" (assert ) nil nil )) nil )"int" integers nil )"(total_order?[real])" nil ))nil 3253536795"" (skeep)"" "mm" "max({ij:real | (EXISTS (km:below(length(P)-1)): ij = km) AND ij >= 0 AND x>=P`seq(ij)})" )"1" (typepred "mm" )"1" (skeep -1)"1" (inst + "km" )"1" (assert )"1" (inst - "1+mm" )"1" (assert ) (("1" (inst + "1+mm" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (split +)"1" (lemma "is_finite_surj" )"1" (inst?)"1" (assert )"1" (hide 2)"1" "P`length-1" "(LAMBDA (pz:below[P`length-1]): IF x>=P`seq(pz) THEN pz ELSE 0 ENDIF)" )"1" (expand "surjective?" )"1" (skosimp*)"1" (typepred "y!1" )"1" (skosimp*)"1" (inst + "km!1" )"1" "1" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*) (("2" (inst + "0" ) nil nil )) nil )"3" (skosimp*)"3" (assert ) (("3" (inst + "pz!1" ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skosimp*) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil )"2" (expand "empty?" )"2" (inst - "0" )"2" (expand "member" )"2" (assert ) (("2" (inst + "0" ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )"3" (hide 2) (("3" (skosimp*) (("3" (assert ) nil nil )) nil ))nil ))nil ))nil )nil rs_partition nil )nil naturalnumbers nil )"bool" sort_fseq "structures/" )"R" restrict nil )"bool" reals nil )nil fseqs "structures/" )nil fseqs "structures/" )nil rs_partition nil )"[real -> boolean]" rs_partition nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )max const-decl"{a: T | SS(a) AND (FORALL (x: T): SS(x) IMPLIES x <= a)}" "finite_sets/" )"bool" reals nil )"[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil finite_sets nil )"bool" sets nil )NOT const-decl "[bool -> bool]" booleans nil )nil finite_sets nil )"bool" finite_sets nil )set type-eq-decl nil sets nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )"[T, T -> boolean]" equalities nil )nil booleans nil )nil numbers nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"posint" nil )"int" integers nil )"[numfield, numfield -> numfield]" number_fields nil )"posreal" nil )"T" rs_partition nil )"T" rs_partition nil )"partition(a, b)" rs_partition nil )"bool" functions nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"T" rs_partition nil )nil nat_types nil )nil finite_sets nil )"bool" sets nil ))nil ))nil 3491222014"" (skeep)"" "mm" "max({ij:real | (EXISTS (km:below(length(P)-1)): ij = km) AND ij >= 0 AND x>P`seq(ij)})" )"1" (typepred "mm" )"1" (skeep -1)"1" (inst + "km" )"1" (assert )"1" (inst - "1+mm" )"1" (assert ) (("1" (inst + "1+mm" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (split +)"1" (lemma "is_finite_surj" )"1" (inst?)"1" (assert )"1" (hide 2)"1" "P`length-1" "(LAMBDA (pz:below[P`length-1]): IF x>P`seq(pz) THEN pz ELSE 0 ENDIF)" )"1" (expand "surjective?" )"1" (skosimp*)"1" (typepred "y!1" )"1" (skosimp*)"1" (inst + "km!1" )"1" "1" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*) (("2" (inst + "0" ) nil nil )) nil )"3" (skosimp*)"3" (assert ) (("3" (inst + "pz!1" ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skosimp*) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil )"2" (expand "empty?" )"2" (inst - "0" )"2" (expand "member" )"2" (assert ) (("2" (inst + "0" ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )"3" (hide 2) (("3" (skosimp*) (("3" (assert ) nil nil )) nil ))nil ))nil ))nil )nil rs_partition nil )nil naturalnumbers nil )"bool" sort_fseq "structures/" )"R" restrict nil )"bool" reals nil )nil fseqs "structures/" )nil fseqs "structures/" )nil rs_partition nil )"[real -> boolean]" rs_partition nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )max const-decl"{a: T | SS(a) AND (FORALL (x: T): SS(x) IMPLIES x <= a)}" "finite_sets/" )"bool" reals nil )"[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil finite_sets nil )"bool" sets nil )NOT const-decl "[bool -> bool]" booleans nil )nil finite_sets nil )"bool" finite_sets nil )set type-eq-decl nil sets nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )"[T, T -> boolean]" equalities nil )nil booleans nil )nil numbers nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"posint" nil )"int" integers nil )"[numfield, numfield -> numfield]" number_fields nil )"posreal" nil )"T" rs_partition nil )"T" rs_partition nil )"partition(a, b)" rs_partition nil )"bool" functions nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"T" rs_partition nil )nil nat_types nil )nil finite_sets nil )"bool" sets nil ))nil )nil 3491221650"" (skeep) (("" (postpone) nil nil )) nil ) nil shostak))nil 3280828196"" (skosimp*)"" (lemma "parts_order" )"" (inst - "a!1" "b!1" "P!1" "ii!1+1" "jj!1" )"" (assert )"" (lemma "parts_order" )"" (inst - "a!1" "b!1" "P!1" "jj!1" "ii!1" )"" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )nil rs_partition nil )"(total_order?[real])" nil )"posint" nil )"[numfield, numfield -> numfield]" number_fields nil )nil rs_partition nil )nil naturalnumbers nil )"bool" reals nil ) (>= const-decl "bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"bool" sort_fseq "structures/" )"bool" reals nil )"R" restrict nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[T, T -> boolean]" equalities nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )nil fseqs "structures/" )nil fseqs "structures/" )nil naturalnumbers nil )nil rs_partition nil )"[real -> boolean]" rs_partition nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"posint" nil )"(strict_total_order?[real])" real_props nil ))nil 3253536795"" (skosimp*)"" (assert )"" (skosimp*)"" case "(FORALL (n: below(length(P!1)-1)): (FORALL (ii: below(n + 1)): seq(P!1)(ii) <= x!1 AND x!1 <= seq(P!1)(1 + ii) IMPLIES Prop!1(x!1)) IMPLIES Prop!1(x!1) OR x!1 > seq(P!1)(1+n))" )"1" (inst -1 "length(P!1)-2" )"1" (assert )"1" (skosimp*)"1" (inst?) (("1" (assert ) nil nil )) nil )) nil ))nil ))nil )"2" (hide -1 2)"2" (induct "n" 1 "below_induction[length(P!1) - 1]" )"1" (assert )"1" (skosimp*)"1" (inst?) (("1" (assert ) nil nil )) nil )) nil ))nil )"2" (skosimp*)"2" (split -2)"1" (propax) nil nil )"2" (inst - "jb!1+1" ) (("2" (assert ) nil nil )) nil )"3" (skosimp*)"3" (inst?) (("3" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil intervals_real "reals/" )"[numfield, numfield -> numfield]" number_fields nil )"[bool, bool -> bool]" booleans nil )nil rs_partition nil )nil naturalnumbers nil )"bool" sort_fseq "structures/" )"bool" reals nil )"R" restrict nil )"[T, T -> boolean]" equalities nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil fseqs "structures/" )nil fseqs "structures/" )nil rs_partition nil )"[real -> boolean]" rs_partition nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"posint" nil )"int" integers nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil defined_types nil )nil bounded_nat_inductions nil )"odd_int" integers nil )"(total_order?[real])" nil )"even_int" integersnil )"(strict_total_order?[real])" real_props nil )"posint" nil ))nil ))nil 3253536795 ("" (subtype-tcc) nil nil ) nil nil ))nil 3253536795"" (skosimp*)"" (lemma "connected_domain" )"" (expand "connected?" )"" "a!1" "b!1" "a!1 + ii!1 * (b!1 - a!1) / (N!1 - 1)" )"" (assert )"" (hide 2)"" (assert )"" (split)"1" (typepred "b!1" )"1" (typepred "ii!1" )"1" (case "ii!1/(N!1-1) > 0" )"1" (mult-by -4 "ii!1/(N!1-1)" )"1" (assert ) nil nil )) nil )"2" (cross-mult 1) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" case "(b!1 * ii!1 - a!1 * ii!1) / (N!1 - 1) <= b!1-a!1" )"1" (assert ) nil nil )"2" (hide 2)"2" (cross-mult 1)"2" (case "N!1-1 >= ii!1" )"1" (mult-by -1 "b!1-a!1" )"1" (assert ) nil nil )) nil )"2" (hide 2) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil rs_partition nil )"real" reals nil )"int" integers nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rs_partition nil )nil rs_partition nil )nil booleans nil )"bool" reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"[numfield, numfield -> numfield]" number_fields nil )"bool" reals nil )nil integers nil )nil extra_real_props nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )nil real_props nil )nil real_types nil )nil real_types nil )"above(1)" rs_partition nil )"nat" rs_partition nil )AND const-decl "[bool, bool -> bool]" booleans nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"rat" rationals nil )NOT const-decl "[bool -> bool]" booleans nil )nil extra_real_propsnil )nil real_props nil )"bool" reals nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"real" reals nil )"real" reals nil )"(total_order?[real])" nil )"bool" deriv_domain_def nil ))nil ))nil 3489310835"" (skosimp*)"" (split)"1" (assert )"1" (skosimp*)"1" (ground)"1" (name "cv" "(ii!1 * b!1 - ii!1 * a!1) / (N!1 - 1)" )"1" (case "cv >=0 AND cv <= b!1-a!1" )"1" (flatten)"1" (lemma "connected_domain" )"1" (expand "connected?" )"1" (inst - "a!1" "b!1" "a!1+cv" )"1" (assert )"1" (replace -4) (("1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (split)"1" (expand "cv" +)"1" (cross-mult 1)"1" (typepred "b!1" )"1" (mult-by -2 "ii!1" )"1" (assert ) nil nil )) nil ))nil ))nil ))nil )"2" (expand "cv" +)"2" (cross-mult 1)"2" (case "ii!1<=N!1-1" )"1" (mult-by -1 "b!1-a!1" )"1" (assert ) nil nil )) nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*) (("2" (lift-if) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil )nil integers nil )"bool" reals nil ) (< const-decl "bool" reals nil )nil rs_partition nil )"[real -> boolean]" rs_partition nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )"[T, T -> boolean]" equalities nil )nil booleans nil )nil numbers nil )nil extra_real_propsnil )nil real_props nil )"real" rs_partition nil )NOT const-decl "[bool -> bool]" booleans nil )nil real_props nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"(strict_total_order?[real])" real_props nil )nil real_types nil )nil real_types nil )nil real_props nil )"bool" deriv_domain_def nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"[numfield, numfield -> numfield]" number_fields nil )nil rs_partition nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"real" reals nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"real" reals nil )"int" integers nil ))nil )nil 3253536795"" (skosimp*)"" (assert )"" (prop)"1" (move-terms 1 l 2)"1" (mult-by 1 "N!1-1" ) (("1" (assert ) nil nil )) nil )) nil )"2" (expand "increasing?" )"2" (skosimp*)"2" (lift-if)"2" (lift-if)"2" (assert )"2" (case "(b!1-a!1)/(N!1-1)>0" )"1" (mult-by -1 "j!1-i!1" )"1" (assert ) nil nil )) nil )"2" (assert )"2" (cross-mult 1) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (skeep)"3" (case "(b!1-a!1)/(N!1-1)>0" )"1" (assert ) nil nil )"2" (cross-mult 1) (("2" (assert ) nil nil )) nil ))nil ))nil )"4" (skosimp*)"4" (assert )"4" (split +)"1" (case "(b!1-a!1)/(N!1-1)>0" )"1" (mult-by -1 "i!1" ) (("1" (assert ) nil nil )) nil )"2" (cross-mult 1) (("2" (assert ) nil nil )) nil ))nil )"2" (case "i!1/(N!1-1) < 1" )"1" (mult-by -1 "b!1-a!1" ) (("1" (assert ) nil nil ))nil )"2" (cross-mult 1) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" sort_fseq "structures/" )) nil ))nil 3494850114"" (skosimp*)"" (split)"1" (assert ) nil nil ) ("2" (ground) nil nil )"3" (lift-if) (("3" (ground) (("3" (field) nil nil )) nil )) nil )"4" (expand "increasing?" )"4" (skosimp*)"4" (lift-if)"4" (lift-if)"4" (assert )"4" (case "(b!1-a!1)/(N!1-1)>=0" )"1" (mult-by -1 "j!1-i!1" ) (("1" (assert ) nil nil ))nil )"2" (hide 2)"2" (cross-mult 1) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"5" (skosimp*)"5" (assert )"5" (ground)"1" (case "i!1/(N!1-1)>0" )"1" (mult-by -1 "b!1-a!1" ) (("1" (assert ) nil nil ))nil )"2" (cross-mult 1) (("2" (assert ) nil nil )) nil ))nil )"2" (case "i!1/(N!1-1)<=1" )"1" (mult-by -1 "b!1-a!1" ) (("1" (assert ) nil nil ))nil )"2" (cross-mult 1) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"real" reals nil )"real" reals nil )"real" reals nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )nil integers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )"boolean" notequal nil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"bool" booleans nil )"(bijective?[T, T])" identity nil )"bool" functions nil )"bool" reals nil )nil rs_partition nil )"[real -> boolean]" rs_partition nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil reals nil )nil real_props nil )"[numfield -> numfield]" number_fields nil )"odd_int" integers nil )"[T, T -> boolean]" equalities nil )"bool" reals nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"(total_order?[real])" nil )nil naturalnumbers nil )nil real_types nil )nil extra_real_propsnil )nil real_props nil )nil real_types nil )"(total_order?[real])" nil )"bool" sort_fseq "structures/" )"bool" reals nil )nil extra_real_propsnil )nil real_props nil )nil naturalnumbers nil )"rat" rationals nil )nil real_props nil )nil extra_real_props nil ))nil )nil 3494850020 ("" (subtype-tcc) nil nil ) nil nil ))nil 3253536795 ("" (grind) nil nil )nil rs_partition nil )"[real -> boolean]" rs_partition nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"T" fseqs "structures/" )"partition(a, b)" rs_partition nil )"int" integers nil )"real" reals nil )"real" reals nil ))nil ))nil 3253536795 ("" (grind) nil nil )nil rs_partition nil )"[real -> boolean]" rs_partition nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"T" fseqs "structures/" )"partition(a, b)" rs_partition nil )"rat" rationals nil )"int" integers nil )"real" reals nil )"real" reals nil ))nil ))nil 3253536795 ("" (subtype-tcc) nil nil ) nil nil ))nil 3253536795"" (skosimp*)"" (expand "eq_partition" )"" (move-terms 1 l 2)"" (mult-by 1 "N!1-1" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil )"real" reals nil )"real" reals nil )"int" integers nil )"real" reals nil )"partition(a, b)" rs_partition nil )nil real_props nil )nil reals nil )nil real_props nil )"(strict_total_order?[real])" real_props nil )"odd_int" integers nil )nil rs_partition nil )"[real -> boolean]" rs_partition nil )nil integers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )"[numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )"[T, T -> boolean]" equalities nil )nil numbers nil )"[bool, bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"real" reals nil ))nil ))nil 3253536795"" (skosimp*) (("" (grind) nil nil )) nil )"int" integers nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3253536795"" (skosimp*)"" (name-replace "PP" "eq_partition(a!1, b!1, N!1)" )"" (typepred "width(a!1, b!1, PP)" )"" (expand "width" )"" "max({l: real | ") "1" (skosimp*)"1" (replace -1)"1" (reveal -1)"1" (expand "eq_partition" )"1" (replace -1 + rl) (("1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "width_TCC1" )"2" (inst -1 "a!1" "b!1" "PP" "seq(PP)" )"2" (inst?) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )nil naturalnumbers nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rs_partition nil )nil rs_partition nil )nil fseqs "structures/" )nil fseqs "structures/" )"[T, T -> boolean]" equalities nil )nil booleans nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil integers nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"R" restrict nil )"bool" reals nil )"bool" sort_fseq "structures/" )"bool" reals nil )nil naturalnumbers nil )nil rs_partition nil )"partition(a, b)" rs_partition nil )nil rs_partition nil )"T" fseqs "structures/" )"T" rs_partition nil )"T" rs_partition nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"real" reals nil )"real" reals nil )"int" integers nil )"real" reals nil )"posint" nil )"(total_order?[real])" nil )set type-eq-decl nil sets nil )"bool" finite_sets nil )nil finite_sets nil )"bool" sets nil )nil finite_sets nil )"[bool, bool -> bool]" booleans nil )max const-decl"{a: T | SS(a) AND (FORALL (x: T): SS(x) IMPLIES x <= a)}" "finite_sets/" )"[numfield, numfield -> numfield]" number_fields nil )NOT const-decl "[bool -> bool]" booleans nil )nil real_types nil )nil real_types nil )"posreal" rs_partition nil ))nil ))nil 3282565249"" (skosimp*)"" (case-replace "(b!1 - a!1) / delta!1 > 0" )"1" (assert ) nil nil )"2" (cross-mult 1) (("2" (assert ) nil nil )) nil ))nil ))nil )"real" reals nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )"bool" reals nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[real -> boolean]" rs_partition nil )nil rs_partition nil )"bool" reals nil )nil real_types nil )nil real_types nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )nil extra_real_props nil )"nnreal" nil )"real" reals nil ))nil 3306078556"" (skosimp*)"" (assert )"" (case "(b!1 - a!1) / delta!1 > 0" )"1" (lemma "width_eq_part" )"1" (inst?)"1" (assert )"1" "EP" "eq_partition(a!1, b!1, 2 + floor((b!1 - a!1) / delta!1))" )"1" (typepred "floor((b!1 - a!1) / delta!1)" )"1" "FL" "floor((b!1 - a!1) / delta!1)" )"1" (replace -3)"1" (hide -3)"1" (cross-mult -1)"1" (cross-mult -2)"1" (cross-mult 1)"1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" (hide 2) (("2" (cross-mult 1) nil nil )) nil ))nil ))nil ))nil )"real" reals nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"nnreal" nil )nil extra_real_props nil )nil rs_partition nil )"(strict_total_order?[real])" real_props nil )NOT const-decl "[bool -> bool]" booleans nil )"(total_order?[real])" nil )"real" reals nil )nil real_props nil )"(total_order?[real])" nil )"real" reals nil )nil real_props nil )"partition(a, b)" rs_partition nil )nil rs_partition nil )nil naturalnumbers nil )"bool" sort_fseq "structures/" )"R" restrict nil )"[T, T -> boolean]" equalities nil )nil fseqs "structures/" )nil fseqs "structures/" )nil naturalnumbers nil )"{i | i <= x & x < i + 1}" floor_ceil nil )"bool" reals nil ) (<= const-decl "bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil integers nil )"[numfield, numfield -> numfield]" number_fields nil )nil integers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )"bool" reals nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[real -> boolean]" rs_partition nil )nil rs_partition nil )"bool" reals nil )nil real_types nil )nil real_types nil )"real" reals nil ))nil )nil 3282497555"" (skosimp*)"" (assert )"" (case "(b!1 - a!1) / delta!1 > 0" )"1" (lemma "width_eq_part[T]" )"1" (inst?)"1" (assert )"1" "EP" "eq_partition(a!1, b!1, 2 + floor((b!1 - a!1) / delta!1))" )"1" (typepred "floor((b!1 - a!1) / delta!1)" )"1" "FL" "floor((b!1 - a!1) / delta!1)" )"1" (replace -3)"1" (hide -3)"1" (cross-mult -1)"1" (cross-mult -2)"1" (cross-mult 1)"1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" (hide 2) (("2" (cross-mult 1) nil nil )) nil ))nil ))nil ))nil )nil nil ))nil 3489488404"" (skeep)"" (lemma "N_from_delta" )"" (inst - "a" "b" "delta" )"" (assert ) (("" (inst?) nil nil )) nil )) nil ))nil ))nil )nil rs_partition nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )nil naturalnumbers nil )nil fseqs "structures/" )nil fseqs "structures/" )AND const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"R" restrict nil )"bool" reals nil )"bool" sort_fseq "structures/" )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )nil rs_partition nil )nil integers nil )"partition(a, b)" rs_partition nil )"[numfield, numfield -> numfield]" number_fields nil )nil integers nil )"{i | i <= x & x < i + 1}" floor_ceil nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil rs_partition nil )"[real -> boolean]" rs_partition nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"real" reals nil ))nil 3489488725 ("" (subtype-tcc) nil nil ) nil nil ))nil 3489488725 ("" (subtype-tcc) nil nil ) nil nil ))nil 3489488780"" (skosimp*)"" (expand "increasing?" )"" (split)"1" (expand "concat" )"1" (expand "o" ) (("1" (assert ) nil nil )) nil )) nil )"2" (expand "concat" )"2" (expand "o" ) (("2" (assert ) nil nil )) nil )) nil )"3" (expand "concat" )"3" (expand "o" )"3" (lift-if)"3" (assert )"3" (ground)"1" (case "delete[T](0,Pbc!1)`length >= 1" )"1" (assert ) nil nil )"2" (hide 2)"2" (hide -1)"2" (expand "delete" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil )"2" (hide 1)"2" (expand "delete" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" (assert )"4" (skeep)"4" (expand "concat" )"4" (expand "o" )"4" (expand "delete" )"4" (lift-if)"4" (lift-if)"4" (assert )"4" (ground)"1" (lemma "parts_order" )"1" (inst?) (("1" (assert ) nil nil ))nil ))nil )"2" (typepred "Pab!1" )"2" (inst - "i" )"2" "Pbc!1" )"2" "1-Pab!1`length+j" )"2" assert )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (lemma "parts_order" )"3" (inst?) (("3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"5" (skosimp*)"5" (typepred "i!1" )"5" (expand "concat" )"5" (expand "o" )"5" (lift-if)"5" (assert )"5" (ground)"1" (typepred "Pab!1" )"1" (ground)"1" (inst?) (("1" (flatten) nil nil )) nil ))nil ))nil )"2" (typepred "Pab!1" )"2" (inst - "i!1" )"2" (flatten) (("2" (assert ) nil nil ))nil ))nil ))nil )"3" (expand "delete" )"3" (typepred "Pbc!1" )"3" (inst - "1-Pab!1`length+i!1" )"1" (assert ) nil nil )"2" (assert ) nil nil ))nil ))nil ))nil )"4" (expand "delete" )"4" (typepred "Pbc!1" )"4" (inst - "1-Pab!1`length+i!1" )"1" (ground) nil nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" sort_fseq "structures/" )"below((Pab!1 o delete(0, Pbc!1))`length)" nil )"partition(b!1, c!1)" rs_partition nil )"{cc: T | b!1 < cc}" rs_partition nil )"partition(a!1, b!1)" rs_partition nil )"{bb: T | a!1 < bb}" rs_partition nil )"T" rs_partition nil )"(total_order?[real])" nil )"int" integers nil )nil rs_partition nil )"[numfield, numfield -> numfield]" number_fields nil )NOT const-decl "[bool -> bool]" booleans nil )"(total_order?[real])" nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"[real -> boolean]" rs_partition nil )nil rs_partition nil )nil fseqs "structures/" )nil fseqs "structures/" )"bool" reals nil )nil fseqs "structures/" )"fseq" fseqs_ops "structures/" )AND const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )"bool" reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"R" restrict nil )"bool" reals nil )nil naturalnumbers nil )nil rs_partition nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"fseq" fseqs "structures/" )"nonneg_int" nil )"(strict_total_order?[real])" real_props nil )"fseq" fseqs "structures/" ))nil )nil 3489488725 ("" (subtype-tcc) nil nil ) nil nil ))nil 3489490276 ("" (subtype-tcc) nil nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"odd_int" integers nil )nil rs_partition nil )nil naturalnumbers nil )"bool" reals nil )"bool" sort_fseq "structures/" )"bool" reals nil )"R" restrict nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[T, T -> boolean]" equalities nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil fseqs "structures/" )nil fseqs "structures/" )"bool" reals nil )nil rs_partition nil )"[real -> boolean]" rs_partition nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"fseq" fseqs_ops "structures/" )"T" fseqs "structures/" )"fseq" fseqs "structures/" )"partition(a, c)" rs_partition nil )"nonneg_int" nil )"posint" nil ))nil ))nil 3489490276"" (skeep)"" (skeep)"" (skoletin 1)"1" (assert )"1" (ground)"1" (expand "Pac" )"1" (expand "partjoin" 1)"1" (expand "o" ) (("1" (propax) nil nil )) nil )) nil ))nil )"2" (case "n = Pab`length -1" )"1" (replace -1 +)"1" (assert )"1" (expand "Pac" +)"1" (expand "partjoin" +)"1" (expand "o" +)"1" (typepred "Pab" )"1" (typepred "Pbc" )"1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "Pac" +)"2" (expand "partjoin" +)"2" (expand "o" )"2" (assert )"2" (lift-if)"2" (ground)"1" (expand "delete" )"1" (propax) nil nil )) nil )"2" (expand "delete" )"2" (expand "Pac" -2)"2" expand "partjoin" -2)"2" expand "o" )"2" expand "delete" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (hide -)"2" (skosimp*) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )NOT const-decl "[bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )"odd_int" integers nil )"nonneg_int" nil )"fseq" fseqs_ops "structures/" )"partition(a, c)" rs_partition nil )"fseq" fseqs "structures/" )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )"partition(a, c)" rs_partition nil )"[bool, bool -> bool]" booleans nil )nil rs_partition nil )nil naturalnumbers nil )"bool" reals nil ) (>= const-decl "bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"bool" sort_fseq "structures/" )"bool" reals nil )"R" restrict nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[T, T -> boolean]" equalities nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil fseqs "structures/" )nil fseqs "structures/" )nil rs_partition nil )"[real -> boolean]" rs_partition nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil naturalnumbers nil )"bool" booleans nil )"(bijective?[T, T])" identity nil )"bool" functions nil )nil booleans nil )nil booleans nil )"int" integers nil )"int" integers nil ))nil 3489488725 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rs_partition nil )nil rs_partition nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )nil rs_partition nil )nil naturalnumbers nil )"bool" reals nil ) (>= const-decl "bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"bool" sort_fseq "structures/" )"bool" reals nil )"R" restrict nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[T, T -> boolean]" equalities nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil fseqs "structures/" )nil fseqs "structures/" )nil naturalnumbers nil )"bool" reals nil ))nil ))nil 3495196567"" (auto-rewrite + "member" )"" (skeep)"" (skeep)"" case "width(a, c, partjoin(a, b, c)(Pab, Pbc)) >= max(width(a, b, Pab), width(b, c, Pbc))" )"1" (lemma "width_lem_exists" )"1" (inst - "a" "c" )"1" (assert )"1" (inst - "partjoin(a, b, c)(Pab, Pbc)" )"1" (skosimp*)"1" (lemma "width_lem_exists" )"1" (inst - "a" "b" )"1" (assert )"1" (inst - "Pab" )"1" (skosimp*)"1" "width_lem_exists" )"1" "b" "c" )"1" assert )"1" "Pbc" )"1" "1" assert )"1" "PJ" "partjoin(a, b, c)(Pab, Pbc)" )"1" replace -1)"1" "wab" "width(a,b,Pab)" )"1" replace -1)"1" "wbc" "width(b,c,Pbc)" )"1" replace -1)"1" "wac" "width(a,c,PJ)" )"1" replace -1)"1" expand "partjoin" )"1" expand "o" )"1" replace "1" assert )"1" expand "delete" )"1" assert )"1" "1" "1" "1" "1" assert )"1" "1" "width_lem" )"1" "a" "b" "Pab" "ii!1" )"1" assert )nil nil ))nil ))nil )"2" case "1+ii!1 /= Pab`length" )"1" assert )nil nil )"2" "2" "2" case "Pab`seq(ii!1) = Pbc`seq(0)" )"1" assert )"1" case "delete(0, Pbc)`seq(1 - Pab`length + ii!1) = Pbc`seq(1)" )"1" expand "delete" )"1" "width_lem" )"1" "b" "c" "Pbc" "0" )"1" assert )nil nil ))nil ))nil ))nil )"2" expand "delete" )"2" assert )nil nil ))nil ))nil ))nil )"2" "Pab" )"2" "Pbc" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "width_lem" )"3" "b" "c" "Pbc" "1 - Pab`length + ii!1" )"3" assert )nil nil ))nil ))nil )"4" "ii!1" )"4" expand "partjoin" "4" expand "o" "4" expand "delete" "4" 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 ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (expand "max" )"2" (lift-if)"2" (ground)"1" (lemma "width_lem_exists" )"1" (inst - "b" "c" )"1" (assert )"1" (inst?)"1" (skosimp*)"1" (replace -1)"1" "1" "1" "width_lem" )"1" "a" "c" "partjoin(a,b,c)(Pab,Pbc)" "Pab`length-1+ii!1" )"1" assert )"1" "partjoin_def" )"1" "a" "b" "c" "Pab`length + ii!1" )"1" "a" "b" "c" "Pab`length-1 + ii!1" )"1" assert )"1" "Pab" "Pbc" )"1" "Pab" "Pbc" )"1" "1" assert )"1" "1" "1" "1" replace "1" "1" replace "1" nil nil ))nil )"2" expand "partjoin" )"2" expand "o" "2" expand "delete" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "partjoin" )"2" expand "o" "2" expand "delete" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "partjoin" 1)"2" expand "o" )"2" expand "delete" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 1)"2" (lemma "width_lem_exists" )"2" (inst - "a" "b" )"2" (assert )"2" (inst - "Pab" )"2" (skosimp*)"2" replace -1)"2" "2" "width_lem" )"2" "a" "c" "partjoin(a, b, c)(Pab, Pbc)" "ii!1" )"1" case "partjoin(a, b, c)(Pab, Pbc)`seq(ii!1 + 1) - ") "1" (assert ) nil nil )"2" "2" "2" expand "partjoin" )"2" expand "o" )"2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "partjoin" 1)"2" expand "o" )"2" expand "delete" )"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 )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"partition(a, c)" rs_partition nil )"posreal" rs_partition nil )nil real_types nil )nil real_types nil )nil rs_partition nil )nil naturalnumbers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"bool" sort_fseq "structures/" )"bool" reals nil )"R" restrict nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[T, T -> boolean]" equalities nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil fseqs "structures/" )nil fseqs "structures/" )nil naturalnumbers nil )"bool" reals nil )"[real -> boolean]" rs_partition nil )nil rs_partition nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"posint" nil )"real" reals nil )"fseq" fseqs "structures/" )"nonneg_int" nil )"int" integers nil )"posint" nil )nil rs_partition nil )nil fseqs "structures/" )"(strict_total_order?[real])" real_props nil )"odd_int" integers nil )NOT const-decl "[bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )"boolean" notequal nil )"fseq" fseqs_ops "structures/" )"int" integers nil )"(total_order?[real])" nil )"{z: posreal | z >= x AND z >= y}" real_defs nil )"(strict_total_order?[real])" real_props nil )nil rs_partition nil )"T" rs_partition nil )"T" rs_partition nil )"partition(a, b)" rs_partition nil )"T" rs_partition nil )"partition(b, c)" rs_partition nil )"below(Pbc`length - 1)" rs_partition nil )nil rs_partition nil )"odd_int" integers nil )"(total_order?[real])" nil )"below(Pab`length - 1)" rs_partition nil ))nil )nil 3489488854"" (skeep)"" (skeep)"" case "width(a, c, partjoin(a, b, c)(Pab, Pbc)) >= max(width(a, b, Pab), width(b, c, Pbc))" )"1" (lemma "width_lem_exists" )"1" (inst - "a" "c" )"1" (assert )"1" (inst - "partjoin(a, b, c)(Pab, Pbc)" )"1" (skosimp*)"1" (lemma "width_lem_exists" )"1" (inst - "a" "b" )"1" (assert )"1" (inst - "Pab" )"1" (skosimp*)"1" (lemma "width_lem_exists" )"1" "b" "c" )"1" assert )"1" "Pbc" )"1" "1" assert )"1" "PJ" "partjoin(a, b, c)(Pab, Pbc)" )"1" replace -1)"1" "wab" "width(a,b,Pab)" )"1" replace -1)"1" "wbc" "width(b,c,Pbc)" )"1" replace -1)"1" "wac" "width(a,c,PJ)" )"1" replace -1)"1" expand "partjoin" )"1" expand "o" )"1" replace "1" assert )"1" expand "delete" )"1" assert )"1" "1" "1" assert )"1" "1" "width_lem" )"1" "a" "b" "Pab" "ii!1" )"1" assert )nil nil ))nil ))nil )"2" case "1+ii!1 /= Pab`length" )"1" assert )nil nil )"2" "2" "2" case "Pab`seq(ii!1) = Pbc`seq(0)" )"1" assert )"1" case "delete(0, Pbc)`seq(1 - Pab`length + ii!1) = Pbc`seq(1)" )"1" expand "delete" )"1" "width_lem" )"1" "b" "c" "Pbc" "0" )"1" assert )nil nil ))nil ))nil ))nil )"2" expand "delete" )"2" assert )nil nil ))nil ))nil ))nil )"2" "Pab" )"2" "Pbc" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "width_lem" )"3" "b" "c" "Pbc" "1 - Pab`length + ii!1" )"3" assert )nil nil ))nil ))nil )"4" "ii!1" )"4" expand "partjoin" "4" expand "o" "4" expand "delete" "4" 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 ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (expand "max" )"2" (lift-if)"2" (ground)"1" (lemma "width_lem_exists" )"1" (inst - "b" "c" )"1" (assert )"1" (inst?)"1" (skosimp*)"1" (replace -1)"1" (hide -1)"1" "1" "width_lem" )"1" "a" "c" "partjoin(a,b,c)(Pab,Pbc)" "Pab`length-1+ii!1" )"1" assert )"1" "partjoin_def" )"1" "a" "b" "c" "Pab`length + ii!1" )"1" "a" "b" "c" "Pab`length-1 + ii!1" )"1" assert )"1" "Pab" "Pbc" )"1" "Pab" "Pbc" )"1" "1" assert )"1" "1" "1" "1" replace "1" "1" replace "1" nil nil ))nil )"2" expand "partjoin" )"2" expand "o" "2" expand "delete" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "partjoin" )"2" expand "o" "2" expand "delete" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "partjoin" 1)"2" expand "o" )"2" expand "delete" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 1)"2" (lemma "width_lem_exists" )"2" (inst - "a" "b" )"2" (assert )"2" (inst - "Pab" )"2" (skosimp*)"2" (replace -1)"2" "2" "width_lem" )"2" "a" "c" "partjoin(a, b, c)(Pab, Pbc)" "ii!1" )"1" case "partjoin(a, b, c)(Pab, Pbc)`seq(ii!1 + 1) - ") "1" (assert ) nil nil )"2" "2" "2" expand "partjoin" )"2" expand "o" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "partjoin" 1)"2" expand "o" )"2" expand "delete" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"fseq" fseqs_ops "structures/" )nil fseqs "structures/" )"fseq" fseqs "structures/" )nil fseqs "structures/" )nil fseqs "structures/" )"bool" sort_fseq "structures/" ))nil 3490961433 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rs_partition nil )nil rs_partition nil )"int" integers nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3495198360"" (auto-rewrite + "member" )"" case "(FORALL (aa1:T,(bb1:T|aa1<bb1),aa2:T,(bb2:T|aa2<bb2),P1:partition(aa1,bb1),P2:partition(aa2,bb2)): (EXISTS (PQ:partition(min(aa1,aa2),max(bb1,bb2))): (FORALL (x:T): member(x,PQ) IFF (member(x,P1) or member(x,P2))) AND strictly_increasing?(PQ)))" )"1" "xone" "LAMBDA (a:T,(b | a<b)): (LAMBDA (Pone,Ptwo:partition(a,b)): choose({PQ:partition(a,b) | (FORALl (x:T): member[T](x, PQ) IFF OR AND strictly_increasing?(PQ)}))") "1" (inst + "xone" ) nil nil )"2" (hide 2) (("2" (skosimp*) (("2" (assert ) nil nil )) nil ))nil )"3" (hide 2)"3" (skosimp*)"3" (expand "nonempty?" )"3" (inst - "a!1" "b!1" "a!1" "b!1" "Pone!1" "Ptwo!1" )"3" (skosimp*)"3" (expand "empty?" )"3" (inst -1 "PQ!1" )"1" (expand "member" ) (("1" (ground) nil nil ))nil )"2" (typepred "PQ!1" )"2" (expand "min" )"2" (expand "max" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skeep)"2" (name "PQZ" "strictly_sort(concat(P1,P2))" )"2" case "NOT (FORALL (x:T): member(x, PQZ) IFF (member(x, P1) OR member(x, P2)))" )"1" (hide 2)"1" (skosimp*)"1" (typepred "PQZ" )"1" (inst - "x!1" )"1" (replace -2 :dir rl)"1" (lemma "member_composition" )"1" (inst - "P1" "P2" "x!1" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (inst + "PQZ" )"1" (assert ) nil nil )"2" (label "PQZmember" -1)"2" (hide "PQZmember" )"2" (replace -1 + :dir rl)"2" (hide -1)"2" case "strictly_sort((P1 o P2))`length > 1" )"1" (assert )"1" case "strictly_sort((P1 o P2))`seq(0) = min(aa1, aa2)" )"1" assert )"1" case "strictly_sort((P1 o P2))`seq(strictly_sort((P1 o P2))`length - 1) = max (bb1, bb2)") "1" assert )"1" case "increasing?[T, <=](strictly_sort((P1 o P2)))" )"1" assert )"1" case "(FORALL (i: below(PQZ`length - 1)): ") "1" assert )"1" case "FORALL (i: below(PQZ`length)): min (aa1, aa2) <= strictly_sort((P1 o P2))`seq(i) AND max (bb1, bb2)") "1" (propax) nil nil )"2" "2" "2" "2" "1" expand "increasing?" "1" "0" "i" )"1" assert )"1" "i" )"1" expand "PQZ" "1" nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "increasing?" "2" "i" "strictly_sort((P1 o P2))`length - 1" )"2" assert )"2" "i" )"2" expand "PQZ" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "strictly_sort(concat(P1,P2))" )"2" expand "strictly_increasing?" )"2" "i" "i+1" )"2" assert )"2" "1" "1" assert )nil nil ))nil )"2" assert )"2" "i" )"2" expand "PQZ" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" "strictly_sort(concat(P1,P2))" )"2" expand "strictly_increasing?" )"2" expand "increasing?" )"2" "2" "i" "j" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "strictly_sort(concat(P1,P2))" )"2" case "member(max(bb1,bb2),strictly_sort((P1 o P2)))" )"1" expand "member" -1)"1" "1" expand "strictly_increasing?" )"1" "i!1" "strictly_sort((P1 o P2))`length - 1" )"1" assert )"1" replace "1" "PQZmember" )"1" "myx" "seq(strictly_sort((P1 o P2)))(strictly_sort((P1 o P2))`length - 1)" )"1" "myx" )"1" case "NOT member(myx,PQZ)" )"1" "1" expand "PQZ" )"1" expand "member" )"1" expand "myx" )"1" "strictly_sort((P1 o P2))`length - 1" )nil nil ))nil ))nil ))nil ))nil )"2" replace "2" assert )"2" replace "2" "PQZmember" )"1" "1" "P1" )"1" expand "increasing?" "1" "i!2" "P1`length-1" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" "P2" )"2" expand "increasing?" "2" "i!2" "P2`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 )"2" "max(bb1,bb2)" )"2" replace -2 :dir rl)"2" "member_composition" )"2" "2" replace -1)"2" case "member(bb1,P1) AND member(bb2,P2)" )"1" expand "max" 1)"1" "1" nil nil ))nil ))nil )"2" "2" "1" "P1" )"1" expand "member" )"1" "P1`length-1" )"1" assert )nil nil ))nil ))nil ))nil )"2" expand "member" )"2" "P2" )"2" "P2`length-1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" expand "max" )"3" "3" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "PQZmember" )"2" "PQZmember" )"2" "PQZmember" )"2" "min(aa1,aa2)" )"1" case "(member(min(aa1, aa2), P1) OR member(min(aa1, aa2), P2))" )"1" replace -1)"1" assert )"1" "1" "1" replace -1)"1" expand "PQZ" )"1" "myx" "strictly_sort((P1 o P2))`seq(0)" )"1" replace -1)"1" "newx" "strictly_sort((P1 o P2))`seq(i!1)" )"1" replace "1" "PQZ" )"1" expand "strictly_increasing?" )"1" "0" "i!1" )"1" "myx" )"1" case "NOT member(myx,PQZ)" )"1" "1" expand "myx" )"1" expand "PQZ" )"1" expand "member" )"1" "0" )nil nil ))nil ))nil ))nil ))nil )"2" "member_composition" )"2" "P1" "P2" "myx" )"2" replace "2" "2" replace "2" assert )"2" expand "PQZ" )"2" replace "2" replace "2" "1" "1" "P1" )"1" expand "increasing?" )"1" "0" "i!2" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" "P2" )"2" expand "increasing?" )"2" "0" "i!2" )"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 ))nil ))nil ))nil )"2" "2" "2" case "member(aa1,P1) AND member(aa2,P2)" )"1" "1" expand "min" )"1" "1" nil nil ))nil ))nil ))nil )"2" "2" "1" "P1" )"1" expand "member" )"1" "0" )"1" assert )nil nil ))nil ))nil ))nil )"2" expand "member" )"2" "P2" )"2" "0" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "min" )"2" "2" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" case "strictly_sort((P1 o P2))`length /= 1" )"1" assert )"1" "strictly_sort(concat(P1,P2))" )"1" "P1`seq(0)" )"1" case "member(P1`seq(0),concat(P1,P2))" )"1" replace -1)"1" assert )"1" (skosimp*) nil nil ))nil ))nil )"2" "member_composition" )"2" "P1" "P2" "P1`seq(0)" )"2" assert )"2" replace -1)"2" "2" "0" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "strictly_sort(concat(P1,P2))" )"2" "aa1" )"2" "bb1" )"2" case "aa1 < bb1" )"1" case "member(aa1,concat(P1,P2)) and member(bb1,concat(P1,P2))" )"1" "1" replace -1)"1" replace -2)"1" assert )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" case "member(aa1,P1) AND member(bb1,P1)" )"1" "1" "member_composition" )"1" "P1" "P2" "aa1" )"1" "P1" "P2" "bb1" )"1" nil nil ))nil ))nil ))nil ))nil )"2" "2" "P1" )"2" expand "member" )"2" "1" "0" )"1" assert )nil nil ))nil )"2" "P1`length-1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "P1" )"2" case "P1`length-1 = 1" )"1" "0" )"1" assert )nil nil ))nil )"2" "0" )"2" expand "increasing?" )"2" "1" "P1`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 ))nil ))nil ))nil ))nil ))nil ))nil )"bool" sort_fseq "structures/" )OR const-decl "[bool, bool -> bool]" booleans nil )"bool" fseqs "structures/" )"[bool, bool -> bool]" booleans nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )nil rs_partition nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"bool" sort_fseq "structures/" )"bool" reals nil )"R" restrict nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[T, T -> boolean]" equalities nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil fseqs "structures/" )nil fseqs "structures/" )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil rs_partition nil )"[real -> boolean]" rs_partition nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"(reflexive?[S])" nil )"(antisymmetric?[S])" nil )"(transitive?[S])" nil )"(preorder?[S])" nil )"(partial_order?[S])" nil )"(dichotomous?[S])" nil )"(total_order?[S])" nil )"T" rs_partition nil )"{b | a!1 < b}" rs_partition nil )"partition(min(a!1, a!1), max(b!1, b!1))" nil )"bool" sets nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" sets nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"[bool, bool -> bool]" booleans nil )"(p)" sets nil )"bool" sets nil )set type-eq-decl nil sets nil )"int" integers nil )nil fseqs "structures/" )"(total_order?[real])" nil )"posint" nil )"[numfield, numfield -> numfield]" number_fields nil )"(strict_total_order?[real])" real_props nil )"posint" nil )"T" rs_partition nil )"T" rs_partition nil )"boolean" notequal nil )"{ss: fseq[T] | AND " nil )"partition(aa2, bb2)" rs_partition nil )"{bb2: T | aa2 < bb2}" rs_partition nil )"T" rs_partition nil )"partition(aa1, bb1)" rs_partition nil )"{bb1: T | aa1 < bb1}" rs_partition nil )"T" rs_partition nil )"fseq" fseqs "structures/" )"{ss: fseq | AND " sort_fseq "structures/" ))nil )nil 3490961433"" case "(FORALL (aa1:T,(bb1:T|aa1<bb1),aa2:T,(bb2:T|aa2<bb2),P1:partition(aa1,bb1),P2:partition(aa2,bb2)): (EXISTS (PQ:partition(min(aa1,aa2),max(bb1,bb2))): (FORALL (x:T): member(x,PQ) IFF (member(x,P1) or member(x,P2))) AND strictly_increasing?(PQ)))" )"1" "xone" "LAMBDA (a:T,(b | a<b)): (LAMBDA (Pone,Ptwo:partition(a,b)): choose({PQ:partition(a,b) | (FORALl (x:T): member[T](x, PQ) IFF OR AND strictly_increasing?(PQ)}))") "1" (inst + "xone" ) nil nil )"2" (hide 2) (("2" (skosimp*) (("2" (assert ) nil nil )) nil ))nil )"3" (hide 2)"3" (skosimp*)"3" (expand "nonempty?" )"3" (inst - "a!1" "b!1" "a!1" "b!1" "Pone!1" "Ptwo!1" )"3" (skosimp*)"3" (expand "empty?" )"3" (inst -1 "PQ!1" )"1" (expand "member" ) (("1" (ground) nil nil ))nil )"2" (typepred "PQ!1" )"2" (expand "min" )"2" (expand "max" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skeep)"2" (name "PQZ" "strictly_sort(concat(P1,P2))" )"2" case "NOT (FORALL (x:T): member(x, PQZ) IFF (member(x, P1) OR member(x, P2)))" )"1" (hide 2)"1" (skosimp*)"1" (typepred "PQZ" )"1" (inst - "x!1" )"1" (replace -2 :dir rl)"1" (lemma "member_composition" )"1" (inst - "P1" "P2" "x!1" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (inst + "PQZ" )"1" (assert ) nil nil )"2" (label "PQZmember" -1)"2" (hide "PQZmember" )"2" (replace -1 + :dir rl)"2" (hide -1)"2" case "strictly_sort((P1 o P2))`length > 1" )"1" (assert )"1" case "strictly_sort((P1 o P2))`seq(0) = min(aa1, aa2)" )"1" (assert )"1" case "strictly_sort((P1 o P2))`seq(strictly_sort((P1 o P2))`length - 1) = max (bb1, bb2)") "1" assert )"1" case "increasing?[T, <=](strictly_sort((P1 o P2)))" )"1" assert )"1" case "(FORALL (i: below(PQZ`length - 1)): ") "1" assert )"1" case "FORALL (i: below(PQZ`length)): min (aa1, aa2) <= strictly_sort((P1 o P2))`seq(i) AND max (bb1, bb2)") "1" (propax) nil nil )"2" "2" "2" "2" "1" expand "increasing?" "1" "0" "i" )"1" assert )"1" "i" )"1" expand "PQZ" "1" nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "increasing?" "2" "i" "strictly_sort((P1 o P2))`length - 1" )"2" assert )"2" "i" )"2" expand "PQZ" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "strictly_sort(concat(P1,P2))" )"2" expand "strictly_increasing?" )"2" "i" "i+1" )"2" assert )"2" "1" "1" assert )nil nil ))nil )"2" assert )"2" "i" )"2" expand "PQZ" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" "strictly_sort(concat(P1,P2))" )"2" expand "strictly_increasing?" )"2" expand "increasing?" )"2" "2" "i" "j" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "strictly_sort(concat(P1,P2))" )"2" case "member(max(bb1,bb2),strictly_sort((P1 o P2)))" )"1" expand "member" -1)"1" "1" expand "strictly_increasing?" )"1" "i!1" "strictly_sort((P1 o P2))`length - 1" )"1" assert )"1" replace -1 :dir rl)"1" "PQZmember" )"1" "myx" "seq(strictly_sort((P1 o P2)))(strictly_sort((P1 o P2))`length - 1)" )"1" "myx" )"1" case "NOT member(myx,PQZ)" )"1" "1" expand "PQZ" )"1" expand "member" )"1" expand "myx" )"1" "strictly_sort((P1 o P2))`length - 1" )nil nil ))nil ))nil ))nil ))nil )"2" replace "2" assert )"2" replace "2" "PQZmember" )"1" "1" "P1" )"1" expand "increasing?" "1" "i!2" "P1`length-1" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" "P2" )"2" expand "increasing?" "2" "i!2" "P2`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 )"2" "max(bb1,bb2)" )"2" replace -2 :dir rl)"2" "member_composition" )"2" "2" replace -1)"2" case "member(bb1,P1) AND member(bb2,P2)" )"1" expand "max" 1)"1" "1" nil nil ))nil ))nil )"2" "2" "1" "P1" )"1" expand "member" )"1" "P1`length-1" )"1" assert )nil nil ))nil ))nil ))nil )"2" expand "member" )"2" "P2" )"2" "P2`length-1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" expand "max" )"3" "3" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" "PQZmember" )"2" "PQZmember" )"2" "PQZmember" )"2" "min(aa1,aa2)" )"1" case "(member(min(aa1, aa2), P1) OR member(min(aa1, aa2), P2))" )"1" replace -1)"1" assert )"1" "1" "1" replace -1)"1" expand "PQZ" )"1" "myx" "strictly_sort((P1 o P2))`seq(0)" )"1" replace -1)"1" "newx" "strictly_sort((P1 o P2))`seq(i!1)" )"1" replace "1" "PQZ" )"1" expand "strictly_increasing?" )"1" "0" "i!1" )"1" "myx" )"1" case "NOT member(myx,PQZ)" )"1" "1" expand "myx" )"1" expand "PQZ" )"1" expand "member" )"1" "0" )nil nil ))nil ))nil ))nil ))nil )"2" "member_composition" )"2" "P1" "P2" "myx" )"2" replace "2" "2" replace "2" assert )"2" expand "PQZ" )"2" replace "2" replace "2" "1" "1" "P1" )"1" expand "increasing?" )"1" "0" "i!2" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" "P2" )"2" expand "increasing?" )"2" "0" "i!2" )"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 ))nil ))nil ))nil )"2" "2" "2" case "member(aa1,P1) AND member(aa2,P2)" )"1" "1" expand "min" )"1" "1" nil nil ))nil ))nil ))nil )"2" "2" "1" "P1" )"1" expand "member" )"1" "0" )"1" assert )nil nil ))nil ))nil ))nil )"2" expand "member" )"2" "P2" )"2" "0" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "min" )"2" "2" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" case "strictly_sort((P1 o P2))`length /= 1" )"1" (assert )"1" "strictly_sort(concat(P1,P2))" )"1" "P1`seq(0)" )"1" case "member(P1`seq(0),concat(P1,P2))" )"1" replace -1)"1" assert )"1" (skosimp*) nil nil ))nil ))nil )"2" "member_composition" )"2" "P1" "P2" "P1`seq(0)" )"2" assert )"2" replace -1)"2" "2" "0" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" "strictly_sort(concat(P1,P2))" )"2" "aa1" )"2" "bb1" )"2" case "aa1 < bb1" )"1" case "member(aa1,concat(P1,P2)) and member(bb1,concat(P1,P2))" )"1" "1" replace -1)"1" replace -2)"1" assert )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" case "member(aa1,P1) AND member(bb1,P1)" )"1" "1" "member_composition" )"1" "P1" "P2" "aa1" )"1" "P1" "P2" "bb1" )"1" nil nil ))nil ))nil ))nil ))nil )"2" "2" "P1" )"2" expand "member" )"2" "1" "0" )"1" assert )nil nil ))nil )"2" "P1`length-1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "P1" )"2" case "P1`length-1 = 1" )"1" "0" )"1" (assert ) nil nil ))nil )"2" "0" )"2" expand "increasing?" )"2" "1" "P1`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 ))nil ))nil ))nil ))nil ))nil )"{ss: fseq | AND " sort_fseq "structures/" )"fseq" fseqs "structures/" )nil fseqs "structures/" )nil fseqs "structures/" )nil fseqs "structures/" )"bool" sort_fseq "structures/" )"bool" fseqs "structures/" )"bool" sort_fseq "structures/" ))nil ))nil 3495198221"" (auto-rewrite + "member" )"" (skeep)"" (skeep)"" (name "PQ" "partition_union(a,b)(P,Q)" )"" (replace -1)"" (name "QP" "partition_union(a,b)(Q,P)" )"" (replace -1)"" (name "Le" "min(PQ`length,QP`length)" )"" (label "Lename" -1)"" (label "QPname" -2)"" (label "PQname" -3)"" (label "altb" -4)"" case "FORALL (mm: below(Le)): PQ`seq(mm) = QP`seq(mm)" )"1" (case "NOT PQ`length = QP`length" )"1" "1" case "PQ`length > QP`length" )"1" expand "min" )"1" assert )"1" "QP`length-1" )"1" "PQ" )"1" expand "strictly_increasing?" )"1" "QP`length-1" "PQ`length-1" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "min" )"2" assert )"2" "PQ`length-1" )"2" "QP" )"2" expand "strictly_increasing?" )"2" "PQ`length-1" "QP`length-1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "seqeq" -2)"2" "lengtheq" -1)"2" expand "min" )"2" assert )"2" case "FORALL (mm:below(Le)): PQ`seq(mm) = QP`seq(mm)" )"1" "1" "1" "x!1" )"1" assert )"1" "x!1" )"1" "PQ" )"1" "PQ`seq" )"1" "x!1" )"1" "QP`seq" )"1" "x!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" "mm" )"1" "1" (assert ) nil nil ))nil )"2" "mm" )"2" "2" "pq" "PQ`seq(mm+1)" )"2" replace -1)"2" "qp" "QP`seq(mm+1)" )"2" replace -1)"2" case "member(qp,PQ) and member(pq,QP)" )"1" "1" assert )"1" "1" case "i!1 > mm and i!2 > mm" )"1" "1" "PQ" )"1" expand "strictly_increasing?" )"1" "1+mm" "i!1" )"1" assert )"1" "QP" )"1" expand "strictly_increasing?" )"1" "1+mm" "i!2" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "1" case "qp <= PQ`seq(mm)" )"1" "QP" )"1" expand "strictly_increasing?" )"1" "mm" "1+mm" )"1" assert )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "PQ" )"2" expand "increasing?" )"2" "i!1" "mm" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" case "pq <= QP`seq(mm)" )"1" "PQ" )"1" expand "strictly_increasing?" )"1" "mm" "1+mm" )"1" assert )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "QP" )"2" expand "increasing?" )"2" "i!2" "mm" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "member(pq,PQ) and member(qp,QP)" )"1" "1" "PQ" )"1" "1" "pq" )"1" "qp" )"1" "QP" )"1" "1" "qp" )"1" "pq" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "1" expand "member" )"1" "1" assert )nil nil )"2" assert )nil nil ))nil ))nil )"2" expand "member" )"2" "1" assert )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 ))nil )"{PQ: partition(a, b) | OR member(x, Q)))AND strictly_increasing?(PQ)}" rs_partition nil) "bool" sort_fseq "structures/" )OR const-decl "[bool, bool -> bool]" booleans nil )"bool" fseqs "structures/" )"[bool, bool -> bool]" booleans nil )nil rs_partition nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"bool" sort_fseq "structures/" )"bool" reals nil )"R" restrict nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil booleans nil )"[T, T -> boolean]" equalities nil )nil fseqs "structures/" )nil fseqs "structures/" )nil rs_partition nil )"[real -> boolean]" rs_partition nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil naturalnumbers nil )"{k: nat | k <= i AND k <= j}" nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"posint" nil )"[numfield, numfield -> numfield]" number_fields nil )"posint" nil )"(total_order?[real])" nil )"below(Le)" rs_partition nil )nil bounded_nat_inductions nil )nil defined_types nil )NOT const-decl "[bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"(total_order?[real])" nil )"{k: nat | k <= PQ`length AND k <= QP`length}" rs_partition nil )"{PQ: partition(a, b) | OR member(x, P)))AND strictly_increasing?(PQ)}" rs_partition nil) "{PQ: partition(a, b) | OR member(x, Q)))AND strictly_increasing?(PQ)}" rs_partition nil) "partition(a, b)" rs_partition nil )"partition(a, b)" rs_partition nil )"T" rs_partition nil )"T" rs_partition nil )"nat" rs_partition nil )"[bool, bool -> bool]" booleans nil )"T" fseqs "structures/" ))nil )nil 3491567687"" (skeep)"" (skeep)"" (name "PQ" "partition_union(a,b)(P,Q)" )"" (replace -1)"" (name "QP" "partition_union(a,b)(Q,P)" )"" (replace -1)"" (name "Le" "min(PQ`length,QP`length)" )"" (label "Lename" -1)"" (label "QPname" -2)"" (label "PQname" -3)"" (label "altb" -4)"" case "FORALL (mm: below(Le)): PQ`seq(mm) = QP`seq(mm)" )"1" (case "NOT PQ`length = QP`length" )"1" (hide 2)"1" case "PQ`length > QP`length" )"1" expand "min" )"1" assert )"1" "QP`length-1" )"1" "PQ" )"1" expand "strictly_increasing?" )"1" "QP`length-1" "PQ`length-1" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "min" )"2" assert )"2" "PQ`length-1" )"2" "QP" )"2" expand "strictly_increasing?" )"2" "PQ`length-1" "QP`length-1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (label "seqeq" -2)"2" "lengtheq" -1)"2" expand "min" )"2" assert )"2" case "FORALL (mm:below(Le)): PQ`seq(mm) = QP`seq(mm)" )"1" "1" "1" "x!1" )"1" assert )"1" "x!1" )"1" "PQ" )"1" "PQ`seq" )"1" "x!1" )"1" "QP`seq" )"1" "x!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (induct "mm" )"1" "1" (assert ) nil nil ))nil )"2" "mm" )"2" "2" "pq" "PQ`seq(mm+1)" )"2" replace -1)"2" "qp" "QP`seq(mm+1)" )"2" replace -1)"2" case "member(qp,PQ) and member(pq,QP)" )"1" "1" assert )"1" "1" case "i!1 > mm and i!2 > mm" )"1" "1" "PQ" )"1" expand "strictly_increasing?" )"1" "1+mm" "i!1" )"1" assert )"1" "QP" )"1" expand "strictly_increasing?" )"1" "1+mm" "i!2" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "1" case "qp <= PQ`seq(mm)" )"1" "QP" )"1" expand "strictly_increasing?" )"1" "mm" "1+mm" )"1" assert )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "PQ" )"2" expand "increasing?" )"2" "i!1" "mm" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" case "pq <= QP`seq(mm)" )"1" "PQ" )"1" expand "strictly_increasing?" )"1" "mm" "1+mm" )"1" assert )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "QP" )"2" expand "increasing?" )"2" "i!2" "mm" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "member(pq,PQ) and member(qp,QP)" )"1" "1" "PQ" )"1" "1" "pq" )"1" "qp" )"1" "QP" )"1" "1" "qp" )"1" "pq" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "1" expand "member" )"1" "1" assert )nil nil )"2" assert )nil nil ))nil ))nil )"2" expand "member" )"2" "1" assert )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 )"T" fseqs "structures/" )nil fseqs "structures/" )nil fseqs "structures/" )"bool" sort_fseq "structures/" )"bool" fseqs "structures/" )"bool" sort_fseq "structures/" ))nil 3495198265"" (auto-rewrite + "member" )"" (skeep)"" (skeep)"" (name "QP" "partition_union(a,b)(P,Q)" )"" (replace -1)"" (name "Le" "min(PQ`length,QP`length)" )"" (label "Lename" -1)"" (label "QPname" -2)"" (ground)"1" case "FORALL (mm: below(Le)): PQ`seq(mm) = QP`seq(mm)" )"1" (case "NOT PQ`length = QP`length" )"1" (hide 2)"1" (case "PQ`length > QP`length" )"1" (expand "min" )"1" assert )"1" "QP`length-1" )"1" "PQ" )"1" expand "strictly_increasing?" )"1" "QP`length-1" "PQ`length-1" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "min" )"2" assert )"2" "PQ`length-1" )"2" "QP" )"2" expand "strictly_increasing?" )"2" "PQ`length-1" "QP`length-1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (label "seqeq" -2)"2" (label "lengtheq" -1)"2" (expand "min" )"2" assert )"2" case "FORALL (mm:below(Le)): PQ`seq(mm) = QP`seq(mm)" )"1" "1" "1" "x!1" )"1" assert )"1" "x!1" )"1" "PQ`seq" )"1" "x!1" )"1" "QP`seq" )"1" "x!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (induct "mm" )"1" (flatten) (("1" (assert ) nil nil )) nil )"2" (skolem 1 "mm" )"2" (flatten)"2" "pq" "PQ`seq(mm+1)" )"2" replace -1)"2" "qp" "QP`seq(mm+1)" )"2" replace -1)"2" case "member(qp,PQ) and member(pq,QP)" )"1" "1" assert )"1" "1" case "i!1 > mm and i!2 > mm" )"1" "1" "PQ" )"1" expand "strictly_increasing?" )"1" "1+mm" "i!1" )"1" assert )"1" "QP" )"1" expand "strictly_increasing?" )"1" "1+mm" "i!2" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "1" case "qp <= PQ`seq(mm)" )"1" "QP" )"1" expand "strictly_increasing?" )"1" "mm" "1+mm" )"1" assert )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "PQ" )"2" expand "increasing?" )"2" "i!1" "mm" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" case "pq <= QP`seq(mm)" )"1" "PQ" )"1" expand "strictly_increasing?" )"1" "mm" "1+mm" )"1" assert )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "QP" )"2" expand "increasing?" )"2" "i!2" "mm" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "member(pq,PQ) and member(qp,QP)" )"1" "1" "1" "pq" )"1" "qp" )"1" "QP" )"1" "1" "qp" )"1" "pq" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "1" expand "member" )"1" "1" assert )nil nil )"2" assert )nil nil ))nil ))nil )"2" expand "member" )"2" "1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (typepred "QP" )"2" (skeep)"2" (inst -6 "x" )"2" (assert )"2" (split +)"1" "1" "1" "1" (propax) nil nil )"2" (propax) nil nil )"3" "i!1" )"3" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" "2" "1" assert )"1" replace -1)"1" "1" "i!2" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" replace -1)"2" "2" "i!2" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"{PQ: partition(a, b) | OR member(x, Q)))AND strictly_increasing?(PQ)}" rs_partition nil) "bool" sort_fseq "structures/" )OR const-decl "[bool, bool -> bool]" booleans nil )"bool" fseqs "structures/" )"[bool, bool -> bool]" booleans nil )nil rs_partition nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"bool" sort_fseq "structures/" )"bool" reals nil )"R" restrict nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil booleans nil )"[T, T -> boolean]" equalities nil )nil fseqs "structures/" )nil fseqs "structures/" )nil rs_partition nil )"[real -> boolean]" rs_partition nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil naturalnumbers nil )"{k: nat | k <= i AND k <= j}" nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"[bool, bool -> bool]" booleans nil )"T" fseqs "structures/" )"nat" rs_partition nil )"T" rs_partition nil )"T" rs_partition nil )"partition(a, b)" rs_partition nil )"partition(a, b)" rs_partition nil )"partition(a, b)" rs_partition nil )"{PQ: partition(a, b) | OR member(x, Q)))AND strictly_increasing?(PQ)}" rs_partition nil) "{k: nat | k <= PQ`length AND k <= QP`length}" rs_partition nil )"(total_order?[real])" nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )NOT const-decl "[bool -> bool]" booleans nil )nil defined_types nil )nil bounded_nat_inductions nil )"below(Le)" rs_partition nil )"(total_order?[real])" nil )"posint" nil )"[numfield, numfield -> numfield]" number_fields nil )"posint" nil )"(strict_total_order?[real])" real_props nil ))nil )nil 3492190502"" (skeep)"" (skeep)"" (name "QP" "partition_union(a,b)(P,Q)" )"" (replace -1)"" (name "Le" "min(PQ`length,QP`length)" )"" (label "Lename" -1)"" (label "QPname" -2)"" (ground)"1" case "FORALL (mm: below(Le)): PQ`seq(mm) = QP`seq(mm)" )"1" (case "NOT PQ`length = QP`length" )"1" (hide 2)"1" (case "PQ`length > QP`length" )"1" (expand "min" )"1" (assert )"1" "QP`length-1" )"1" "PQ" )"1" expand "strictly_increasing?" )"1" "QP`length-1" "PQ`length-1" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "min" )"2" (assert )"2" "PQ`length-1" )"2" "QP" )"2" expand "strictly_increasing?" )"2" "PQ`length-1" "QP`length-1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (label "seqeq" -2)"2" (label "lengtheq" -1)"2" (expand "min" )"2" (assert )"2" case "FORALL (mm:below(Le)): PQ`seq(mm) = QP`seq(mm)" )"1" "1" "1" "x!1" )"1" assert )"1" "x!1" )"1" "PQ`seq" )"1" "x!1" )"1" "QP`seq" )"1" "x!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (induct "mm" )"1" (flatten) (("1" (assert ) nil nil )) nil )"2" (skolem 1 "mm" )"2" (flatten)"2" (name "pq" "PQ`seq(mm+1)" )"2" replace -1)"2" "qp" "QP`seq(mm+1)" )"2" replace -1)"2" case "member(qp,PQ) and member(pq,QP)" )"1" "1" assert )"1" "1" case "i!1 > mm and i!2 > mm" )"1" "1" "PQ" )"1" expand "strictly_increasing?" )"1" "1+mm" "i!1" )"1" assert )"1" "QP" )"1" expand "strictly_increasing?" )"1" "1+mm" "i!2" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "1" case "qp <= PQ`seq(mm)" )"1" "QP" )"1" expand "strictly_increasing?" )"1" "mm" "1+mm" )"1" assert )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "PQ" )"2" expand "increasing?" )"2" "i!1" "mm" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" case "pq <= QP`seq(mm)" )"1" "PQ" )"1" expand "strictly_increasing?" )"1" "mm" "1+mm" )"1" assert )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "QP" )"2" expand "increasing?" )"2" "i!2" "mm" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "member(pq,PQ) and member(qp,QP)" )"1" "1" "1" "pq" )"1" "qp" )"1" "QP" )"1" "1" "qp" )"1" "pq" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "1" expand "member" )"1" "1" (assert ) nil nil )"2" assert )nil nil ))nil ))nil )"2" expand "member" )"2" "1" (assert ) nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (typepred "QP" )"2" (skeep)"2" (inst -6 "x" )"2" (assert )"2" (split +)"1" (flatten)"1" "1" "1" (propax) nil nil )"2" (propax) nil nil )"3" "i!1" )"3" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" "1" assert )"1" replace -1)"1" "1" "i!2" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" replace -1)"2" "2" "i!2" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"T" fseqs "structures/" )nil fseqs "structures/" )nil fseqs "structures/" )"bool" sort_fseq "structures/" )"bool" fseqs "structures/" )"bool" sort_fseq "structures/" ))nil ))nil 3495198286"" (auto-rewrite + "member" )"" (lemma "part_in_strict_left" )"" (label "partin" -1)"" (hide "partin" )"" (skeep)"" (skeep)"" (expand "min" )"" (lift-if)"" (ground)"1" (hide -1)"1" "newwid" "width(a, b, partition_union(a, b)(P, Q))" )"1" (replace -1)"1" (name "Qwid" "width(a,b,Q)" )"1" (replace -1)"1" "width_lem" )"1" "Qwidmax" -1)"1" "Qwidname" -2)"1" "newwidname" -3)"1" "width_lem_exists" )"1" "a" "b" )"1" assert )"1" "partition_union(a, b)(P, Q)" )"1" "pqi" )"1" "newidPQdiff" "1" "PQ" "partition_union(a,b)(P,Q)" )"1" "PQname" "1" replace -1)"1" "partin" )"1" "a" "b" "PQ`seq(1+pqi)" "Q" )"1" assert )"1" "PQ" )"1" "1+pqi" )"1" assert )"1" "1" assert )"1" case "a < PQ`seq(1+pqi)" )"1" assert )"1" "partin" "PQname" "newidPQdiff" "Qwidmax" "Qwidname" "newidname" "1" "ti" )"1" "1" case "Q`seq(ti) <= PQ`seq(pqi) and PQ`seq(pqi) <= Q`seq(1 + ti)" )"1" "1" case "NOT newwid <= Q`seq(1+ti)-Q`seq(ti)" )"1" assert )nil nil )"2" "thisid" "Q`seq(1 + ti) - Q`seq(ti)" )"2" assert )"2" "Qwidmax" "a" "b" "Q" "ti" )"2" replace "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "PQ" )"2" "2" "Q`seq(ti)" )"2" case "member(Q`seq(ti),Q)" )"1" replace "1" "1" "1" "pqti" )"1" replace "1" "PQ" )"1" "1" expand "increasing?" )"1" "pqti" "pqi" )"1" assert )"1" "PQ" )"1" "1" expand "increasing?" )"1" "1+pqi" "pqti" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "member" )"2" "ti" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "PQ`seq(pqi) >= a" )"1" assert )nil nil )"2" "2" "PQ" )"2" "pqi" )"2" "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 ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 1)"2" "newwid" "width(a, b, partition_union(a, b)(P, Q))" )"2" (replace -1)"2" (name "Pwid" "width(a,b,P)" )"2" (replace -1)"2" "width_lem" )"2" "Pwidmax" -1)"2" "Pwidname" -2)"2" "newwidname" -3)"2" "width_lem_exists" )"2" "a" "b" )"2" assert )"2" "partition_union(a, b)(P, Q)" )"2" "pqi" )"2" "newidPQdiff" "2" "PQ" "partition_union(a,b)(P,Q)" )"2" "PQname" "2" replace -1)"2" "partin" )"2" "a" "b" "PQ`seq(1+pqi)" "P" )"2" assert )"2" "PQ" )"2" "1+pqi" )"2" assert )"2" "2" assert )"2" case "a < PQ`seq(1+pqi)" )"1" assert )"1" "partin" "PQname" "newidPQdiff" "Pwidmax" "Pwidname" "newidname" "1" "ti" )"1" "1" case "P`seq(ti) <= PQ`seq(pqi) and PQ`seq(pqi) <= P`seq(1 + ti)" )"1" "1" case "NOT newwid <= P`seq(1+ti)-P`seq(ti)" )"1" assert )nil nil )"2" "thisid" "P`seq(1 + ti) - P`seq(ti)" )"2" assert )"2" "Pwidmax" "a" "b" "P" "ti" )"2" replace "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "PQ" )"2" "2" "P`seq(ti)" )"2" case "member(P`seq(ti),P)" )"1" replace "1" "1" "1" "pqti" )"1" replace "1" "PQ" )"1" "1" expand "increasing?" )"1" "pqti" "pqi" )"1" assert )"1" "PQ" )"1" "1" expand "increasing?" )"1" "1+pqi" "pqti" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "member" )"2" "ti" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "PQ`seq(pqi) >= a" )"1" assert )nil nil )"2" "2" "PQ" )"2" "pqi" )"2" "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 ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil rs_partition nil )"real" reals nil )"(total_order?[real])" nil )"odd_int" integers nil )"int" integers nil )NOT const-decl "[bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )"posint" nil )nil rs_partition nil )nil rs_partition nil )nil numbers nil )nil booleans nil )"[T, T -> boolean]" equalities nil )nil rs_partition nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rs_partition nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )nil fseqs "structures/" )nil fseqs "structures/" )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"R" restrict nil )"bool" reals nil )"bool" sort_fseq "structures/" )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )nil rs_partition nil )nil real_types nil )nil real_types nil )"posreal" rs_partition nil )"[bool, bool -> bool]" booleans nil )"bool" fseqs "structures/" )OR const-decl "[bool, bool -> bool]" booleans nil )"bool" sort_fseq "structures/" )"{PQ: partition(a, b) | OR member(x, Q)))AND strictly_increasing?(PQ)}" rs_partition nil) "(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil ))nil )nil 3491045482"" (lemma "part_in_strict_left" )"" (label "partin" -1)"" (hide "partin" )"" (skeep)"" (skeep)"" (expand "min" )"" (lift-if)"" (ground)"1" (hide -1)"1" "newwid" "width(a, b, partition_union(a, b)(P, Q))" )"1" (replace -1)"1" (name "Qwid" "width(a,b,Q)" )"1" (replace -1)"1" (lemma "width_lem" )"1" "Qwidmax" -1)"1" "Qwidname" -2)"1" "newwidname" -3)"1" "width_lem_exists" )"1" "a" "b" )"1" assert )"1" "partition_union(a, b)(P, Q)" )"1" "pqi" )"1" "newidPQdiff" "1" "PQ" "partition_union(a,b)(P,Q)" )"1" "PQname" -1)"1" replace -1)"1" "partin" )"1" "a" "b" "PQ`seq(1+pqi)" "Q" )"1" assert )"1" "PQ" )"1" "1+pqi" )"1" assert )"1" "1" assert )"1" case "a < PQ`seq(1+pqi)" )"1" assert )"1" "partin" "PQname" "newidPQdiff" "Qwidmax" "Qwidname" "newidname" "1" "ti" )"1" "1" case "Q`seq(ti) <= PQ`seq(pqi) and PQ`seq(pqi) <= Q`seq(1 + ti)" )"1" "1" case "NOT newwid <= Q`seq(1+ti)-Q`seq(ti)" )"1" assert )nil nil )"2" "thisid" "Q`seq(1 + ti) - Q`seq(ti)" )"2" assert )"2" "Qwidmax" "a" "b" "Q" "ti" )"2" replace "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "PQ" )"2" "2" "Q`seq(ti)" )"2" case "member(Q`seq(ti),Q)" )"1" replace "1" "1" "1" "pqti" )"1" replace "1" "PQ" )"1" "1" expand "increasing?" )"1" "pqti" "pqi" )"1" assert )"1" "PQ" )"1" "1" expand "increasing?" )"1" "1+pqi" "pqti" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "member" )"2" "ti" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "PQ`seq(pqi) >= a" )"1" assert )nil nil )"2" "2" "PQ" )"2" "pqi" )"2" "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 ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 1)"2" "newwid" "width(a, b, partition_union(a, b)(P, Q))" )"2" (replace -1)"2" (name "Pwid" "width(a,b,P)" )"2" (replace -1)"2" (lemma "width_lem" )"2" "Pwidmax" -1)"2" "Pwidname" -2)"2" "newwidname" -3)"2" "width_lem_exists" )"2" "a" "b" )"2" assert )"2" "partition_union(a, b)(P, Q)" )"2" "pqi" )"2" "newidPQdiff" "2" "PQ" "partition_union(a,b)(P,Q)" )"2" "PQname" -1)"2" replace -1)"2" "partin" )"2" "a" "b" "PQ`seq(1+pqi)" "P" )"2" assert )"2" "PQ" )"2" "1+pqi" )"2" assert )"2" "2" assert )"2" case "a < PQ`seq(1+pqi)" )"1" assert )"1" "partin" "PQname" "newidPQdiff" "Pwidmax" "Pwidname" "newidname" "1" "ti" )"1" "1" case "P`seq(ti) <= PQ`seq(pqi) and PQ`seq(pqi) <= P`seq(1 + ti)" )"1" "1" case "NOT newwid <= P`seq(1+ti)-P`seq(ti)" )"1" assert )nil nil )"2" "thisid" "P`seq(1 + ti) - P`seq(ti)" )"2" assert )"2" "Pwidmax" "a" "b" "P" "ti" )"2" replace "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "PQ" )"2" "2" "P`seq(ti)" )"2" case "member(P`seq(ti),P)" )"1" replace "1" "1" "1" "pqti" )"1" replace "1" "PQ" )"1" "1" expand "increasing?" )"1" "pqti" "pqi" )"1" assert )"1" "PQ" )"1" "1" expand "increasing?" )"1" "1+pqi" "pqti" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "member" )"2" "ti" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "PQ`seq(pqi) >= a" )"1" assert )nil nil )"2" "2" "PQ" )"2" "pqi" )"2" "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 ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" sort_fseq "structures/" )"bool" fseqs "structures/" )"bool" sort_fseq "structures/" )nil fseqs "structures/" )nil fseqs "structures/" ))nil 3491903086"" (skeep)"" (skeep)"" (lemma "partition_strictly_sort" )"" (inst - "a" "b" )"" (assert ) (("" (inst - "P" ) nil nil )) nil )) nil ))nil ))nil ))nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rs_partition nil )nil rs_partition nil )nil naturalnumbers nil )nil fseqs "structures/" )nil fseqs "structures/" )nil booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )"[T, T -> boolean]" equalities nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"R" restrict nil )"bool" reals nil )"bool" sort_fseq "structures/" )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil ) (< const-decl "bool" reals nil )nil naturalnumbers nil )nil rs_partition nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )nil rs_partition nil ))nil ))nil 3495198312"" (auto-rewrite + "member" )"" (skeep)"" (skeep)"" (name "PQ" "partition_union(a, b)(P, Q)" )"" (replace -1)"" (hide -1)"" "PPQ" "partition_union(a, b)(strictly_sort(P), Q)" )"" (replace -1)"" (hide -1)"" case "FORALL (x:T): member(x,PQ) IFF member(x,PPQ)" )"1" (label "memberlem" -1)"1" (hide "memberlem" )"1" (name "ml" "min(PQ`length,PPQ`length)" )"1" case "FORALL (nn:below(ml)): PQ`seq(nn) = PPQ`seq(nn)" )"1" case "PQ`length = PPQ`length" )"1" rewrite "fseqs_eq" )"1" assert )"1" "1" "n" )"1" expand "min" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" "ml-1" )"1" expand "min" )"1" "1" "1" replace -2 :dir rl)"1" case "PQ`seq(PPQ`length-1) = b" )"1" "PQ" )"1" "1" expand "strictly_increasing?" "1" "PPQ`length-1" "PQ`length-1" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" replace -1 :dir rl)"2" case "PPQ`seq(PQ`length-1) = b" )"1" "PPQ" )"1" "1" expand "strictly_increasing?" "1" "PQ`length-1" "PPQ`length-1" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "min" )"2" "2" (ground) nil nil ))nil ))nil ))nil ))nil )"2" "2" "nn" )"1" (assert ) nil nil )"2" "nn" )"2" assert )"2" "2" assert )"2" case "PQ`seq(1+nn) <= PPQ`seq(1+nn) AND PPQ`seq(1+nn) <= PQ`seq(1+nn)" )"1" "1" (assert ) nil nil ))nil )"2" "2" "1" "memberlem" )"1" "memberlem" )"1" "memberlem" )"1" "PPQ`seq(1+nn)" )"1" case "member(PPQ`seq(1+nn),PPQ)" )"1" replace "1" assert )"1" "1" "1" replace "1" "PQ" )"1" "1" expand "strictly_increasing?" "1" "1+nn" "i!1" )"1" assert )"1" case "1+nn<=i!1" )"1" assert )nil nil )"2" case "PQ`seq(nn) < PQ`seq(i!1)" )"1" "1" expand "strictly_increasing?" "1" "i!1" "nn" )"1" assert )nil nil ))nil ))nil ))nil )"2" "PPQ" )"2" "2" expand "strictly_increasing?" "2" "nn" "1+nn" )"2" assert )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "member" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "memberlem" )"2" "memberlem" )"2" "memberlem" )"2" "PQ`seq(1+nn)" )"2" case "member(PQ`seq(1+nn),PQ)" )"1" replace "1" assert )"1" "1" "1" replace "1" "PPQ" )"1" "1" expand "strictly_increasing?" "1" "1+nn" "i!1" )"1" assert )"1" case "1+nn<=i!1" )"1" assert )nil nil )"2" case "PPQ`seq(nn) < PPQ`seq(i!1)" )"1" "1" expand "strictly_increasing?" "1" "i!1" "nn" )"1" assert )nil nil ))nil ))nil ))nil )"2" "PQ" )"2" "2" expand "strictly_increasing?" "2" "nn" "1+nn" )"2" assert )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "member" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (typepred "PQ" )"2" (label "pqm" -6)"2" (typepred "PPQ" )"2" (label "ppqm" -6)"2" "pqm" "ppqm" +))"2" "2" "x" )"2" "x" )"2" "strictly_sort(P)" )"2" "x" )"2" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"{PQ: partition(a, b) | OR member(x, Q)))AND strictly_increasing?(PQ)}" rs_partition nil) "bool" sort_fseq "structures/" )OR const-decl "[bool, bool -> bool]" booleans nil )"bool" fseqs "structures/" )"[bool, bool -> bool]" booleans nil )nil rs_partition nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"bool" sort_fseq "structures/" )"bool" reals nil )"R" restrict nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil booleans nil )"[T, T -> boolean]" equalities nil )nil fseqs "structures/" )nil fseqs "structures/" )nil rs_partition nil )"[real -> boolean]" rs_partition nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil naturalnumbers nil )"(total_order?[real])" nil )"int" integers nil )NOT const-decl "[bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )
Messung V0.5 in Prozent C=100 H=100 G=100
¤ 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.1.206Bemerkung:
(vorverarbeitet am 2026-04-28)
¤ *Bot Zugriff
2026-05-26
