%% PVS Version 3.1 %% 6.2 [Linux (x86)] (Feb 14, 2003 18:46) $$$top.pvs %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Lee Pike % leepike @ galois.com % Formal Methods Group, NASA Langley Research Center % % PVS Version 3.1 % % Proofs for TPHOLs 2004 paper % % ("Sec." refers the to section from the paper, "Abstractions for % Fault-Tolerant Distributed System Verification" formalized. The % paper is available at % .) % % abstract_msg : The message datatype (Sec. 4.2) % (imported by send.pvs) % % send : A formalization of the send function % (Sec. 5.3) % % fault_masking_vote : fundamental results of bags including % the equivalence of mid_val selection and % majority selection (Sec. 6.2) % % single_stage_bag_maj : proves validity and agreement results % of majority voting over bags after a % round of exact communication (Sec. 7.3) % % single_stage_bag_mid_val : proves validity and agreement results % of middle value selection over bags after a % round of inexact communiction (Sec. 7.4) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% top: THEORY BEGIN IMPORTING send, structures@fault_masking_vote, single_stage_bag_maj, single_stage_bag_mid_val END top $$$min_max_ineq.pvs %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % NASA Langley Formal Methods % http://shemesh.larc.nasa.gov/fm/spider/fm-now-spider.html % % PVS 3.1 % % Design : SPIDER Version 2 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% min_max_ineq : THEORY BEGIN a, b, c, d: VAR real min_le : LEMMA min(a,b) <= c IFF (a <= c OR b <= c) min_lt : LEMMA min(a,b) < c IFF (a < c OR b < c) min_ge : LEMMA min(a,b) >= c IFF (a >= c AND b >= c) min_gt : LEMMA min(a,b) > c IFF (a > c AND b > c) le_min : LEMMA a <= min(b,c) IFF (a <= b AND a <= c) lt_min : LEMMA a < min(b,c) IFF (a < b AND a < c) ge_min : LEMMA a >= min(b,c) IFF (a >= b OR a >= c) gt_min : LEMMA a > min(b,c) IFF (a > b OR a > c) max_le : LEMMA max(a,b) <= c IFF (a <= c AND b <= c) max_lt : LEMMA max(a,b) < c IFF (a < c AND b < c) max_ge : LEMMA max(a,b) >= c IFF (a >= c OR b >= c) max_gt : LEMMA max(a,b) > c IFF (a > c OR b > c) le_max : LEMMA a <= max(b,c) IFF (a <= b OR a <= c) lt_max : LEMMA a < max(b,c) IFF (a < b OR a < c) ge_max : LEMMA a >= max(b,c) IFF (a >= b AND a >= c) gt_max : LEMMA a > max(b,c) IFF (a > b AND a > c) max_triangle: LEMMA max(a+c,b+d) <= max(a,b) + max(c,d) min_commutative: LEMMA min(a,b) = min(b,a) max_commutative: LEMMA max(a,b) = max(b,a) END min_max_ineq $$$min_max_ineq.prf (min_max_ineq (min_le 0 (min_le-1 nil 3276016566 nil ("" (grind) nil nil) unchecked nil nil nil nil nil)) (min_lt 0 (min_lt-1 nil 3276016566 nil ("" (grind) nil nil) unchecked nil nil nil nil nil)) (min_ge 0 (min_ge-1 nil 3276016566 nil ("" (grind) nil nil) unchecked nil nil nil nil nil)) (min_gt 0 (min_gt-1 nil 3276016566 nil ("" (grind) nil nil) unchecked nil nil nil nil nil)) (le_min 0 (le_min-1 nil 3276016566 nil ("" (grind) nil nil) unchecked nil nil nil nil nil)) (lt_min 0 (lt_min-1 nil 3276016566 nil ("" (grind) nil nil) unchecked nil nil nil nil nil)) (ge_min 0 (ge_min-1 nil 3276016566 nil ("" (grind) nil nil) unchecked nil nil nil nil nil)) (gt_min 0 (gt_min-1 nil 3276016566 nil ("" (grind) nil nil) unchecked nil nil nil nil nil)) (max_le 0 (max_le-1 nil 3276016566 nil ("" (skosimp*) (("" (expand "max") (("" (case "a!1 < b!1") (("1" (assert) (("1" (prop) (("1" (assert) nil nil)) nil)) nil) ("2" (assert) (("2" (prop) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) unchecked nil nil nil nil nil)) (max_lt 0 (max_lt-1 nil 3276016566 nil ("" (skosimp*) (("" (expand "max") (("" (case "a!1 < b!1") (("1" (assert) (("1" (prop) (("1" (assert) nil nil)) nil)) nil) ("2" (assert) (("2" (prop) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) unchecked nil nil nil nil nil)) (max_ge 0 (max_ge-1 nil 3276016566 nil ("" (skosimp*) (("" (expand "max") (("" (case "a!1 < b!1") (("1" (assert) (("1" (prop) (("1" (assert) nil nil)) nil)) nil) ("2" (assert) (("2" (prop) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) unchecked nil nil nil nil nil)) (max_gt 0 (max_gt-1 nil 3276016566 nil ("" (skosimp*) (("" (expand "max") (("" (case "a!1 < b!1") (("1" (assert) (("1" (prop) (("1" (assert) nil nil)) nil)) nil) ("2" (assert) (("2" (prop) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) unchecked nil nil nil nil nil)) (le_max 0 (le_max-1 nil 3276016566 nil ("" (skosimp*) (("" (expand "max") (("" (case "b!1 < c!1") (("1" (assert) (("1" (prop) (("1" (assert) nil nil)) nil)) nil) ("2" (assert) (("2" (prop) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) unchecked nil nil nil nil nil)) (lt_max 0 (lt_max-1 nil 3276016566 nil ("" (skosimp*) (("" (expand "max") (("" (case "b!1 < c!1") (("1" (assert) (("1" (prop) (("1" (assert) nil nil)) nil)) nil) ("2" (assert) (("2" (prop) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) unchecked nil nil nil nil nil)) (ge_max 0 (ge_max-1 nil 3276016566 nil ("" (skosimp*) (("" (expand "max") (("" (case "b!1 < c!1") (("1" (assert) (("1" (prop) (("1" (assert) nil nil)) nil)) nil) ("2" (assert) (("2" (prop) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) unchecked nil nil nil nil nil)) (gt_max 0 (gt_max-1 nil 3276016566 nil ("" (skosimp*) (("" (expand "max") (("" (case "b!1 < c!1") (("1" (assert) (("1" (prop) (("1" (assert) nil nil)) nil)) nil) ("2" (assert) (("2" (prop) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) unchecked nil nil nil nil nil)) (max_triangle 0 (max_triangle-1 nil 3276016567 3276017067 ("" (skosimp*) (("" (expand "max") (("" (lift-if) (("" (lift-if) (("" (lift-if) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) unchecked ((max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)) 63219 1060 t shostak)) (min_commutative 0 (min_commutative-1 nil 3276018406 3276018450 ("" (skosimp*) (("" (expand "min") (("" (lift-if) (("" (assert) (("" (lift-if) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) proved ((min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)) 18043 900 t shostak)) (max_commutative 0 (max_commutative-1 nil 3276018453 3276018464 ("" (skosimp*) (("" (expand "max") (("" (lift-if) (("" (assert) (("" (lift-if) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) proved ((max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)) 10869 900 t shostak))) $$$abs_props.pvs %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % NASA Langley Formal Methods % http://shemesh.larc.nasa.gov/fm/spider/fm-now-spider.html % % PVS 3.1 % % Design : SPIDER Version 2 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% abs_props: THEORY BEGIN IMPORTING min_max_ineq x, y: VAR real nny: VAR nnreal abs_max: LEMMA abs(x) = max(-x,x) abs_add: LEMMA x*y >= 0 IMPLIES abs(x+y) = abs(x) + abs(y) abs_le_nonneg: LEMMA abs(x) <= nny IFF -nny <= x AND x <= nny abs_diff_commutes: LEMMA abs(x-y) = abs(y-x) % from hacks END abs_props $$$abs_props.prf (abs_props (abs_max 0 (abs_max-1 nil 3276280183 3276280186 ("" (grind) nil nil) proved ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (abs const-decl "{n: nonneg_real | n >= m}" real_defs nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)) 3703 650 t shostak)) (abs_add 0 (abs_add-1 nil 3276280191 3276280752 ("" (skosimp*) (("" (expand "abs") (("" (rewrite "pos_times_ge" -1) (("" (prop) (("1" (assert) (("1" (case "x!1 = 0 OR y!1 = 0") (("1" (split -) (("1" (replace*) (("1" (assert) nil nil)) nil) ("2" (replace*) (("2" (assert) nil nil)) nil)) nil) ("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) proved ((abs const-decl "{n: nonneg_real | n >= m}" real_defs nil) (= const-decl "[T, T -> boolean]" equalities nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (pos_times_ge formula-decl nil real_props nil)) 45992 6930 t shostak)) (abs_le_nonneg 0 (abs_le_nonneg-1 nil 3276280210 3276280213 ("" (grind) nil nil) proved ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (abs const-decl "{n: nonneg_real | n >= m}" real_defs nil)) 2243 660 t shostak)) (abs_diff_commutes 0 (abs_diff_commutes-1 nil 3276018898 3276279807 ("" (skosimp*) (("" (expand "abs") (("" (lift-if) (("" (assert) (("" (lift-if) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) proved ((abs const-decl "{n: nonneg_real | n >= m}" real_defs nil)) 156 150 t shostak))) $$$aux.pvs % Lee Pike % Formal Methods Group % NASA Langley % leepike @ galois.com % Auxillary results aux[T, R: TYPE, zero:R, +:[R,R -> R] ]: THEORY BEGIN ASSUMING r,r1,r2,r3 : VAR R zero_identity: ASSUMPTION identity?(+)(zero) plus_ac: ASSUMPTION associative?(+) AND commutative?(+) ENDASSUMING IMPORTING finite_sets@finite_sets_sum[T, R, zero, +] f,g: VAR [T -> R] S, A, B: VAR finite_set x,t: VAR T sum_particular2: THEOREM sum(S,f) = sum(S, LAMBDA t: IF t = x THEN zero ELSE f(t) ENDIF) + IF S(x) THEN f(x) ELSE zero ENDIF END aux $$$aux.prf (aux (IMP_finite_sets_sum_TCC1 0 (IMP_finite_sets_sum_TCC1-1 nil 3292682981 3292683005 ("" (use "zero_identity") nil nil) proved ((zero_identity formula-decl nil aux nil)) 9952 280 t shostak)) (IMP_finite_sets_sum_TCC2 0 (IMP_finite_sets_sum_TCC2-1 nil 3292682981 3292683019 ("" (use "plus_ac") nil nil) proved ((plus_ac formula-decl nil aux nil)) 8586 260 t shostak)) (sum_particular2 0 (sum_particular2-1 nil 3292683078 3292683094 ("" (auto-rewrite "plus_zero_right" "plus_zero_left") (("" (skolem!) (("" (smash) (("1" (use "sum_x") (("1" (use "sum_x" ("f" "LAMBDA t: IF t = x!1 THEN zero ELSE f!1(t) ENDIF")) (("1" (assert) (("1" (rewrite "plus_comm" -2) (("1" (use "sum_f_g" ("S" "remove(x!1, S!1)" "f" "f!1")) (("1" (assert) (("1" (delete -1 -2 -3 2) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "sum_f_g") nil nil)) nil)) nil)) nil) proved ((sum_x formula-decl nil finite_sets_sum "finite_sets/") (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (plus_zero_left formula-decl nil finite_sets_sum "finite_sets/") (sum_f_g formula-decl nil finite_sets_sum "finite_sets/") (NOT const-decl "[bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (member const-decl "bool" sets nil) (plus_comm formula-decl nil finite_sets_sum "finite_sets/") (sum def-decl "R" finite_sets_sum "finite_sets/") (remove const-decl "set" sets nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (= const-decl "[T, T -> boolean]" equalities nil) (plus_zero_right formula-decl nil finite_sets_sum "finite_sets/") (T formal-type-decl nil aux nil) (R formal-type-decl nil aux nil) (zero formal-const-decl "R" aux nil) (+ formal-const-decl "[R, R -> R]" aux nil)) 10163 3380 t nil))) $$$mid_val_equiv.pvs %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Lee Pike % leepike @ galois.com % Formal Methods Group, NASA Langley Research Center % % PVS Version 3.1 % % PURPOSE: Prove the equivalence between middle value selection % over bags and over vectors (functions). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% mid_val_equiv[S: posnat, T: NONEMPTY_TYPE, leq: (total_order?[T])]: THEORY BEGIN IMPORTING make_bag[S, T], middle_value_index[S, T, leq], structures@middle_value_select[T, leq], aux[T, real, 0, +] good_senders : VAR finite_set[below(S)] eligible_set : VAR non_empty_finite_set[below(S)] actual : VAR [below(S) -> T] s,a : VAR below(S) Set : VAR finite_set[below(S)] t : VAR T P : VAR pred[below(S)] mid_val_l: LEMMA middle_value(eligible_set)(actual)(s) AND t = actual(s) IMPLIES 2 * card(l_filter(make_bag(eligible_set, actual), t)) > card(make_bag(eligible_set, actual)) mid_val_u: LEMMA middle_value(eligible_set)(actual)(s) AND t = actual(s) IMPLIES 2 * card(u_filter(make_bag(eligible_set, actual), t)) >= card(make_bag(eligible_set, actual)) exists_mid_val: LEMMA (EXISTS (s: ({s | middle_value(eligible_set)(actual)(s)})): t = actual(s) ) IMPLIES mid_val?(make_bag(eligible_set, actual))(t) nonempty_choose: COROLLARY 2 * card(l_filter(make_bag(eligible_set, actual), t)) > card(make_bag(eligible_set, actual)) AND 2 * card(u_filter(make_bag(eligible_set, actual), t)) >= card(make_bag(eligible_set, actual)) IMPLIES nonempty?({s: (eligible_set) | actual(s) = t}) filter_l: LEMMA 2 * card(l_filter(make_bag(eligible_set, actual), t)) > card(make_bag(eligible_set, actual)) AND 2 * card(u_filter(make_bag(eligible_set, actual), t)) >= card(make_bag(eligible_set, actual)) IMPLIES 2 * card(filter(leq)(eligible_set)(actual) (choose({s: (eligible_set) | actual(s) = t}))) > card(eligible_set) filter_u: LEMMA 2 * card(l_filter(make_bag(eligible_set, actual), t)) > card(make_bag(eligible_set, actual)) AND 2 * card(u_filter(make_bag(eligible_set, actual), t)) >= card(make_bag(eligible_set, actual)) IMPLIES 2 * card(filter(geq)(eligible_set)(actual) (choose({s: (eligible_set) | actual(s) = t}))) >= card(eligible_set) choose_eligible: LEMMA 2 * card(l_filter(make_bag(eligible_set, actual), t)) > card(make_bag(eligible_set, actual)) AND 2 * card(u_filter(make_bag(eligible_set, actual), t)) >= card(make_bag(eligible_set, actual)) IMPLIES eligible_set(choose({s: (eligible_set) | actual(s) = t})) mid_val_exists: LEMMA mid_val?(make_bag(eligible_set, actual))(t) IMPLIES (EXISTS (s: ({s | middle_value(eligible_set)(actual)(s)})): t = actual(s)) restrict_actual: LEMMA image(actual, {s | middle_value(eligible_set)(actual)(s)}) = mid_val?(make_bag(eligible_set, actual)) mid_val_is_middle_value: LEMMA middle_value(eligible_set, actual) = mid_val(make_bag(eligible_set, actual)) END mid_val_equiv $$$mid_val_equiv.prf (mid_val_equiv (IMP_aux_TCC1 0 (IMP_aux_TCC1-1 nil 3292683126 3292683252 ("" (grind) nil nil) proved ((restrict const-decl "R" restrict nil) (identity? const-decl "bool" operator_defs nil)) 3080 290 t shostak)) (IMP_aux_TCC2 0 (IMP_aux_TCC2-1 nil 3292683126 3292683261 ("" (grind) nil nil) proved ((associative? const-decl "bool" operator_defs nil) (commutative? const-decl "bool" operator_defs nil) (restrict const-decl "R" restrict nil)) 1701 330 t shostak)) (mid_val_l 0 (mid_val_l-4 nil 3287344908 3292683142 ("" (skolem + ("f" "e" _ "t")) (("" (skosimp*) (("" (expand "middle_value") (("" (flatten) (("" (hide -3) (("" (use "card_make_bag") (("" (replace -1 :hide? t) (("" (case-replace "card(l_filter(make_bag(e, f), t)) = card(filter(leq)(e)(f)(s!1))") (("" (hide -2 2) (("" (expand "card") (("" (typepred! "e") (("" (replace -3 :hide? t) (("" (lemma "finite_set_ind_modified[below(S)]") (("" (inst - "LAMBDA (ee: finite_set[below(S)]): sum(bag_to_set(l_filter(make_bag(ee, f), f(s!1))), LAMBDA (t: T): l_filter(make_bag(ee, f), f(s!1))(t)) = card(filter(leq)(ee)(f)(s!1))") (("" (split) (("1" (inst?) nil nil) ("2" (hide 3) (("2" (expand "filter") (("2" (lemma "card_empty?[below(S)]") (("2" (inst?) (("1" (case "empty?[below(S)] (LAMBDA (j: below(S)): emptyset(j) AND leq(f(j), f(s!1)))") (("1" (assert) (("1" (replace -2 :hide? t) (("1" (expand "bag_to_set") (("1" (expand "make_bag") (("1" (expand "l_filter") (("1" (case "{t: T | IF leq(t, f(s!1)) THEN card({s: below(S) | emptyset(s) AND f(s) = t}) ELSE 0 ENDIF > 0} = emptyset[T]") (("1" (replace -1 :hide? t) (("1" (use "sum_emptyset[T,real,0,+]") (("1" (skosimp*) (("1" (use "finite_empty") nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (decompose-equality +) (("1" (grind) (("1" (use "card_emptyset[below(S)]") (("1" (expand "emptyset") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (use "finite_empty") nil nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (use "finite_empty") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2 -1) (("2" (grind) nil nil)) nil)) nil) ("2" (use "finite_empty") nil nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (hide 4) (("3" (case "leq(f(e!1),f(s!1))") (("1" (case-replace "card(filter(leq)(add(e!1, S!1))(f)(s!1)) = card(filter(leq)(S!1)(f)(s!1)) + 1") (("1" (replace -3 :dir rl :hide? t) (("1" (hide -1) (("1" (case "bag_to_set(l_filter(make_bag(S!1, f), f(s!1)))(f(e!1))") (("1" (case "l_filter(make_bag(add(e!1, S!1), f), f(s!1))(f(e!1)) = l_filter(make_bag(S!1, f), f(s!1))(f(e!1)) + 1") (("1" (lemma "sum_x[T,real,0,+]") (("1" (inst-cp - "bag_to_set(l_filter(make_bag(add(e!1, S!1), f), f(s!1)))" "LAMBDA (t: T): l_filter(make_bag(add(e!1, S!1), f), f(s!1))(t)" "f(e!1)") (("1" (inst - "bag_to_set(l_filter(make_bag(S!1, f), f(s!1)))" "LAMBDA (t: T): l_filter(make_bag(S!1, f), f(s!1))(t)" "f(e!1)") (("1" (replace*) (("1" (hide -1 -2 -3) (("1" (assert) (("1" (lemma "sum_particular2[T,real,0,+]") (("1" (inst - "remove(f(e!1), bag_to_set(l_filter(make_bag(add(e!1, S!1), f), f(s!1))))" "LAMBDA (t: T): l_filter(make_bag(add(e!1, S!1), f), f(s!1))(t)" "f(e!1)") (("1" (replace - :hide? t) (("1" (lift-if) (("1" (split) (("1" (flatten) (("1" (hide-all-but -1) (("1" (grind) nil nil)) nil)) nil) ("2" (flatten) (("2" (hide 1) (("2" (assert) (("2" (name-replace "g" "LAMBDA (t: T): l_filter(make_bag(add(e!1, S!1), f), f(s!1))(t)") (("2" (case-replace "remove(f(e!1), bag_to_set(l_filter(make_bag(add(e!1, S!1), f), f(s!1)))) = remove(f(e!1), bag_to_set(l_filter(make_bag(S!1, f), f(s!1))))") (("1" (hide -1) (("1" (use "sum_f_g[T,real,0,+]") (("1" (split) (("1" (propax) nil nil) ("2" (skosimp*) (("2" (hide 2) (("2" (lift-if) (("2" (typepred! "x!1") (("2" (split) (("1" (flatten) (("1" (grind) nil nil)) nil) ("2" (flatten) (("2" (hide -4 -5 4) (("2" (grind) (("2" (case-replace "{s: below(S) | (e!1 = s OR S!1(s)) AND f(s) = x!1} = {s: below(S) | S!1(s) AND f(s) = x!1}") (("2" (hide 3) (("2" (decompose-equality +) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (decompose-equality +) (("2" (expand "remove") (("2" (iff) (("2" (prop) (("1" (expand "member") (("1" (expand "bag_to_set") (("1" (expand "l_filter") (("1" (lift-if) (("1" (prop) (("1" (expand "make_bag") (("1" (lemma "nonempty_card[below(S)]") (("1" (inst - "{s: below(S) | S!1(s) AND f(s) = f(e!1)}") (("1" (assert) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (skosimp*) (("1" (expand "member") (("1" (flatten) (("1" (lemma "nonempty_card[below(S)]") (("1" (inst?) (("1" (assert) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (skosimp*) (("1" (expand "member") (("1" (expand "add") (("1" (flatten) (("1" (split) (("1" (lemma "nonempty_card[below(S)]") (("1" (inst - "{s: below(S) | S!1(s) AND f(s) = x!1}") (("1" (assert) nil nil) ("2" (use "finite_intersect") nil nil)) nil)) nil) ("2" (expand "member") (("2" (lemma "nonempty_card[below(S)]") (("2" (inst - "{s: below(S) | S!1(s) AND f(s) = x!1}") (("1" (assert) (("1" (grind) nil nil)) nil) ("2" (use "finite_intersect") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (use "finite_add") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (use "finite_intersect") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (grind) (("2" (lemma "nonempty_card[below(S)]") (("2" (inst - "{s: below(S) | S!1(s) AND f(s) = x!1}") (("1" (assert) (("1" (skosimp*) (("1" (lemma "nonempty_card[below(S)]") (("1" (inst?) (("1" (assert) (("1" (inst?) (("1" (prop) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (use "finite_add") (("2" (inst - "LAMBDA (s: below(S)): f(s) = x!1" "S!1" "e!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (use "finite_intersect") (("2" (inst - "LAMBDA (s: below(S)): f(s) = x!1" "S!1") (("2" (grind) 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 3) (("2" (expand "bag_to_set") (("2" (expand "l_filter") (("2" (lift-if) (("2" (prop) (("2" (expand "make_bag") (("2" (lemma "nonempty_card[below(S)]") (("2" (inst - "{s: below(S) | S!1(s) AND f(s) = f(e!1)}") (("1" (assert) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (skosimp*) (("1" (expand "member") (("1" (flatten) (("1" (lemma "nonempty_card[below(S)]") (("1" (inst - "{s: below(S) | add[below(S)](e!1, S!1)(s) AND f(s) = f(e!1)}") (("1" (assert) (("1" (expand "nonempty?") (("1" (grind) nil nil)) nil)) nil) ("2" (use "finite_add") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (use "finite_intersect") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 3) (("2" (expand "l_filter") (("2" (lift-if) (("2" (split) (("1" (flatten) (("1" (expand "make_bag") (("1" (case-replace "{s: below(S) | add(e!1, S!1)(s) AND f(s) = f(e!1)} = add(e!1, {s: below(S) | S!1(s) AND f(s) = f(e!1)})") (("1" (lemma "card_add[below(S)]") (("1" (inst - "{s: below(S) | S!1(s) AND f(s) = f(e!1)}" "e!1") (("1" (replace -1) (("1" (assert) nil nil)) nil) ("2" (use "finite_intersect") nil nil)) nil)) nil) ("2" (hide -2 2) (("2" (decompose-equality +) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "sum_x[T,real,0,+]") (("2" (inst?) (("2" (inst - "f(e!1)") (("1" (replace - :hide? t) (("1" (case-replace "remove(f(e!1), bag_to_set(l_filter(make_bag(add(e!1, S!1), f), f(s!1)))) = bag_to_set(l_filter(make_bag(S!1, f), f(s!1)))") (("1" (lemma "sum_particular2[T,real,0,+]") (("1" (inst?) (("1" (inst?) (("1" (replace -1 :hide? t) (("1" (assert) (("1" (case "l_filter(make_bag(add(e!1, S!1), f), f(s!1))(f(e!1)) = 1") (("1" (replace - :hide? t) (("1" (assert) (("1" (case-replace "(LAMBDA (t_1: T): IF t_1 = f(e!1) THEN 0 ELSE l_filter(make_bag(add(e!1, S!1), f), f(s!1))(t_1) ENDIF) = LAMBDA (t: T): l_filter(make_bag(S!1, f), f(s!1))(t)") (("1" (hide 4) (("1" (decompose-equality +) (("1" (lift-if) (("1" (split) (("1" (flatten) (("1" (expand "bag_to_set") (("1" (assert) nil nil)) nil)) nil) ("2" (flatten) (("2" (hide -1) (("2" (expand "bag_to_set") (("2" (expand "l_filter") (("2" (lift-if) (("2" (split) (("1" (flatten) (("1" (expand "make_bag") (("1" (expand "add") (("1" (expand "member") (("1" (case-replace "{s: below(S) | (e!1 = s OR S!1(s)) AND f(s) = x!1} = {s: below(S) | S!1(s) AND f(s) = x!1}") (("1" (hide 2) (("1" (decompose-equality +) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 4) (("2" (expand "bag_to_set") (("2" (expand "l_filter") (("2" (expand "make_bag") (("2" (lemma "nonempty_card[below(S)]") (("2" (inst - "{s: below(S) | S!1(s) AND f(s) = f(e!1)}") (("1" (assert) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (lemma "card_one[below(S)]") (("1" (inst - "{s: below(S) | add(e!1, S!1)(s) AND f(s) = f(e!1)}") (("1" (assert) (("1" (inst?) (("1" (expand "singleton") (("1" (decompose-equality +) (("1" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (use "finite_add") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (use "finite_intersect") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 4) (("2" (decompose-equality +) (("2" (iff) (("2" (grind) (("1" (lemma "nonempty_card[below(S)]") (("1" (inst-cp - "{s: below(S) | (e!1 = s OR S!1(s)) AND f(s) = x!1}") (("1" (assert) (("1" (skosimp*) (("1" (split) (("1" (replace*) nil nil) ("2" (inst - "{s: below(S) | S!1(s) AND f(s) = x!1}") (("1" (assert) (("1" (inst?) (("1" (split) (("1" (propax) nil nil) ("2" (propax) nil nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (use "finite_intersect") (("2" (inst - "LAMBDA (s: below(S)): f(s) = x!1" "S!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (use "finite_add") (("2" (inst - "LAMBDA (s: below(S)): f(s) = x!1" "S!1" "e!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "nonempty_card[below(S)]") (("2" (inst - "{s: below(S) | S!1(s) AND f(s) = x!1}") (("1" (assert) (("1" (skosimp*) (("1" (lemma "nonempty_card[below(S)]") (("1" (inst - "{s: below(S) | (e!1 = s OR S!1(s)) AND f(s) = x!1}") (("1" (assert) (("1" (inst?) (("1" (prop) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (use "finite_add") (("2" (inst - "LAMBDA (s: below(S)): f(s) = x!1" "S!1" "e!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (use "finite_intersect") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 4) (("2" (grind) (("2" (lemma "nonempty_card[below(S)]") (("2" (inst - "{s: below(S) | (e!1 = s OR S!1(s)) AND f(s) = f(e!1)}") (("1" (assert) (("1" (inst?) nil nil)) nil) ("2" (hide-all-but 1) (("2" (use "finite_add") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -2 3) (("2" (expand "filter") (("2" (expand "add") (("2" (expand "member") (("2" (case-replace "(LAMBDA (j: below(S)): (e!1 = j OR S!1(j)) AND leq(f(j), f(s!1))) = add(e!1, LAMBDA (j: below(S)): S!1(j) AND leq(f(j), f(s!1)))") (("1" (lemma "card_add[below(S)]") (("1" (inst - "LAMBDA (j: below(S)): S!1(j) AND leq(f(j), f(s!1))" "e!1") (("1" (replace -) (("1" (assert) nil nil)) nil) ("2" (use "finite_intersect") nil nil)) nil)) nil) ("2" (hide 2) (("2" (decompose-equality +) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case-replace "filter(leq)(add(e!1, S!1))(f)(s!1) = filter(leq)(S!1)(f)(s!1)") (("1" (replace -2 :dir rl :hide? t) (("1" (case-replace "bag_to_set(l_filter(make_bag(add(e!1, S!1), f), f(s!1))) = bag_to_set(l_filter(make_bag(S!1, f), f(s!1)))") (("1" (lemma "sum_particular2[T,real,0,+]") (("1" (inst?) (("1" (inst - "f(e!1)") (("1" (replace -1 :hide? t) (("1" (lift-if) (("1" (split) (("1" (flatten) (("1" (case-replace "l_filter(make_bag(add(e!1, S!1), f), f(s!1))(f(e!1)) = 0") (("1" (assert) (("1" (hide -2 -3 -4) (("1" (case-replace "(LAMBDA (t_1: T): IF t_1 = f(e!1) THEN 0 ELSE l_filter(make_bag(add(e!1, S!1), f), f(s!1))(t_1) ENDIF) = LAMBDA (t: T): l_filter(make_bag(S!1, f), f(s!1))(t)") (("1" (hide 2) (("1" (decompose-equality +) (("1" (lift-if) (("1" (split) (("1" (flatten) (("1" (grind) nil nil)) nil) ("2" (flatten) (("2" (expand "l_filter") (("2" (lift-if) (("2" (split) (("1" (flatten) (("1" (expand "make_bag") (("1" (case-replace "{s: below(S) | add(e!1, S!1)(s) AND f(s) = x!1} = {s: below(S) | S!1(s) AND f(s) = x!1}") (("1" (hide 2) (("1" (decompose-equality +) (("1" (iff) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 -2 -3 2) (("2" (grind) nil nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) (("2" (case-replace "(LAMBDA (t_1: T): IF t_1 = f(e!1) THEN 0 ELSE l_filter(make_bag(add(e!1, S!1), f), f(s!1))(t_1) ENDIF) = LAMBDA (t: T): l_filter(make_bag(S!1, f), f(s!1))(t)") (("2" (hide 3) (("2" (decompose-equality +) (("2" (lift-if) (("2" (split) (("1" (flatten) (("1" (expand "bag_to_set") (("1" (assert) nil nil)) nil)) nil) ("2" (flatten) (("2" (hide -1 -2) (("2" (expand "bag_to_set") (("2" (expand "l_filter") (("2" (lift-if) (("2" (split) (("1" (flatten) (("1" (expand "make_bag") (("1" (expand "add") (("1" (expand "member") (("1" (case-replace "{s: below(S) | (e!1 = s OR S!1(s)) AND f(s) = x!1} = {s: below(S) | S!1(s) AND f(s) = x!1}") (("1" (hide 2) (("1" (decompose-equality +) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 4) (("2" (decompose-equality +) (("2" (grind) (("1" (case "x!1 = f(e!1)") (("1" (hide-all-but (-1 -4 2)) (("1" (typepred! "leq") (("1" (grind) nil nil)) nil)) nil) ("2" (lemma "nonempty_card[below(S)]") (("2" (inst-cp - "{s: below(S) | (e!1 = s OR S!1(s)) AND f(s) = x!1}") (("1" (assert) (("1" (skosimp*) (("1" (split) (("1" (replace*) nil nil) ("2" (inst - "{s: below(S) | S!1(s) AND f(s) = x!1}") (("1" (assert) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (use "finite_intersect") (("2" (inst - "LAMBDA (s: below(S)): f(s) = x!1" "S!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (use "finite_add") (("2" (inst - "LAMBDA (s: below(S)): f(s) = x!1" "S!1" "e!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "nonempty_card[below(S)]") (("2" (inst-cp - "{s: below(S) | S!1(s) AND f(s) = x!1}") (("1" (assert) (("1" (skosimp*) (("1" (inst - "{s: below(S) | (e!1 = s OR S!1(s)) AND f(s) = x!1}") (("1" (assert) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (use "finite_add") (("2" (inst - "LAMBDA (s: below(S)): f(s) = x!1" "S!1" "e!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (use "finite_intersect") (("2" (inst - "LAMBDA (s: below(S)): f(s) = x!1" "S!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 4) (("2" (decompose-equality +) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((card_make_bag formula-decl nil make_bag nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (S formal-const-decl "posnat" mid_val_equiv nil) (T formal-nonempty-type-decl nil mid_val_equiv nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (empty? const-decl "bool" sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (set type-eq-decl nil sets nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (= const-decl "[T, T -> boolean]" equalities nil) (bag type-eq-decl nil bags "structures/") (is_finite const-decl "bool" finite_bags "structures/") (finite_bag type-eq-decl nil finite_bags "structures/") (card const-decl "nat" finite_bags "structures/") (pred type-eq-decl nil defined_types nil) (total_order? const-decl "bool" orders nil) (leq formal-const-decl "(total_order?[T])" mid_val_equiv nil) (l_filter const-decl "bag" bag_filters "structures/") (make_bag const-decl "finite_bag[T]" make_bag nil) (Card const-decl "nat" finite_sets nil) (card const-decl "{n: nat | n = Card(S)}" finite_sets nil) (filter const-decl "bool" index_filters nil) (bag_to_set const-decl "set[T]" bags_to_sets "structures/") (sum def-decl "R" finite_sets_sum "finite_sets/") (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (restrict const-decl "R" restrict nil) (numfield nonempty-type-eq-decl nil number_fields nil) (card_add formula-decl nil finite_sets nil) (sum_x formula-decl nil finite_sets_sum "finite_sets/") (sum_particular2 formula-decl nil aux nil) (x!1 skolem-const-decl "T" mid_val_equiv nil) (finite_intersect formula-decl nil make_bag nil) (finite_add formula-decl nil make_bag nil) (nonempty_card formula-decl nil finite_sets nil) (below type-eq-decl nil nat_types nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (sum_f_g formula-decl nil finite_sets_sum "finite_sets/") (remove const-decl "set" sets nil) (S!1 skolem-const-decl "finite_set[below(S)]" mid_val_equiv nil) (e!1 skolem-const-decl "below(S)" mid_val_equiv nil) (x!1 skolem-const-decl "T" mid_val_equiv nil) (/= const-decl "boolean" notequal nil) (card_one formula-decl nil finite_sets nil) (singleton const-decl "(singleton?)" sets nil) (nonempty? const-decl "bool" sets nil) (add const-decl "(nonempty?)" sets nil) (x!1 skolem-const-decl "T" mid_val_equiv nil) (reflexive? const-decl "bool" relations nil) (transitive? const-decl "bool" relations nil) (preorder? const-decl "bool" orders nil) (antisymmetric? const-decl "bool" relations nil) (partial_order? const-decl "bool" orders nil) (dichotomous? const-decl "bool" orders nil) (card_empty? formula-decl nil finite_sets nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (sum_emptyset formula-decl nil finite_sets_sum "finite_sets/") (finite_empty formula-decl nil make_bag nil) (card_emptyset formula-decl nil finite_sets nil) (member const-decl "bool" sets nil) (injective? const-decl "bool" functions nil) (s!1 skolem-const-decl "below(S)" mid_val_equiv nil) (f skolem-const-decl "[below(S) -> T]" mid_val_equiv nil) (emptyset const-decl "set" sets nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (finite_set_ind_modified formula-decl nil finite_sets_inductions "finite_sets/") (middle_value const-decl "bool" middle_value_index nil)) 15715 11960 t nil) (mid_val_l-3 nil 3287343585 3287344891 ("" (skolem + ("f" "e" _ "t")) (("" (skosimp*) (("" (expand "middle_value") (("" (flatten) (("" (hide -3) (("" (use "card_make_bag") (("" (replace -1 :hide? t) (("" (case-replace "card(l_filter(make_bag(e, f), t)) = card(filter(leq)(e)(f)(s!1))") (("" (hide -2 2) (("" (expand "card") (("" (typepred! "e") (("" (replace -3 :hide? t) (("" (lemma "finite_set_ind_modified[below(S)]") (("" (inst - "LAMBDA (ee: finite_set[below(S)]): sum(bag_to_set(l_filter(make_bag(ee, f), f(s!1))), LAMBDA (t: T): l_filter(make_bag(ee, f), f(s!1))(t)) = card(filter(leq)(ee)(f)(s!1))") (("" (split) (("1" (inst?) nil) ("2" (hide 3) (("2" (expand "filter") (("2" (lemma "card_empty?[below(S)]") (("2" (inst?) (("1" (case "empty?[below(S)] (LAMBDA (j: below(S)): emptyset(j) AND leq(f(j), f(s!1)))") (("1" (assert) (("1" (replace -2 :hide? t) (("1" (expand "bag_to_set") (("1" (expand "make_bag") (("1" (expand "l_filter") (("1" (case "{t: T | IF leq(t, f(s!1)) THEN card({s: below(S) | emptyset(s) AND f(s) = t}) ELSE 0 ENDIF > 0} = emptyset[T]") (("1" (replace -1 :hide? t) (("1" (use "sum_emptyset[T,real,0,+]") (("1" (skosimp*) (("1" (use "finite_empty") nil))))))) ("2" (hide 2) (("2" (decompose-equality +) (("1" (grind) (("1" (use "card_emptyset[below(S)]") (("1" (expand "emptyset") (("1" (assert) nil))))))) ("2" (skosimp*) (("2" (use "finite_empty") nil))))))) ("3" (skosimp*) (("3" (use "finite_empty") nil))))))))))))))) ("2" (hide 2 -1) (("2" (grind) nil))))) ("2" (use "finite_empty") nil))))))))) ("3" (skosimp*) (("3" (hide 4) (("3" (case "leq(f(e!1),f(s!1))") (("1" (case-replace "card(filter(leq)(add(e!1, S!1))(f)(s!1)) = card(filter(leq)(S!1)(f)(s!1)) + 1") (("1" (replace -3 :dir rl :hide? t) (("1" (hide -1) (("1" (case "bag_to_set(l_filter(make_bag(S!1, f), f(s!1)))(f(e!1))") (("1" (case "l_filter(make_bag(add(e!1, S!1), f), f(s!1))(f(e!1)) = l_filter(make_bag(S!1, f), f(s!1))(f(e!1)) + 1") (("1" (lemma "sum_x[T,real,0,+]") (("1" (inst-cp - "bag_to_set(l_filter(make_bag(add(e!1, S!1), f), f(s!1)))" "LAMBDA (t: T): l_filter(make_bag(add(e!1, S!1), f), f(s!1))(t)" "f(e!1)") (("1" (inst - "bag_to_set(l_filter(make_bag(S!1, f), f(s!1)))" "LAMBDA (t: T): l_filter(make_bag(S!1, f), f(s!1))(t)" "f(e!1)") (("1" (replace*) (("1" (hide -1 -2 -3) (("1" (assert) (("1" (lemma "sum_particular[T,real,0,+]") (("1" (inst - "remove(f(e!1), bag_to_set(l_filter(make_bag(add(e!1, S!1), f), f(s!1))))" "LAMBDA (t: T): l_filter(make_bag(add(e!1, S!1), f), f(s!1))(t)" "f(e!1)") (("1" (replace - :hide? t) (("1" (lift-if) (("1" (split) (("1" (flatten) (("1" (hide-all-but -1) (("1" (grind) nil))))) ("2" (flatten) (("2" (hide 1) (("2" (assert) (("2" (name-replace "g" "LAMBDA (t: T): l_filter(make_bag(add(e!1, S!1), f), f(s!1))(t)") (("2" (case-replace "remove(f(e!1), bag_to_set(l_filter(make_bag(add(e!1, S!1), f), f(s!1)))) = remove(f(e!1), bag_to_set(l_filter(make_bag(S!1, f), f(s!1))))") (("1" (postpone) nil) ("2" (hide 2) (("2" (decompose-equality +) (("2" (expand "remove") (("2" (iff) (("2" (prop) (("1" (expand "member") (("1" (expand "bag_to_set") (("1" (expand "l_filter") (("1" (lift-if) (("1" (prop) (("1" (expand "make_bag") (("1" (lemma "nonempty_card[below(S)]") (("1" (inst - "{s: below(S) | S!1(s) AND f(s) = f(e!1)}") (("1" (assert) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (skosimp*) (("1" (expand "member") (("1" (flatten) (("1" (lemma "nonempty_card[below(S)]") (("1" (inst?) (("1" (assert) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (skosimp*) (("1" (expand "member") (("1" (expand "add") (("1" (flatten) (("1" (split) (("1" (lemma "nonempty_card[below(S)]") (("1" (inst - "{s: below(S) | S!1(s) AND f(s) = x!1}") (("1" (assert) nil) ("2" (use "finite_intersect") nil))))) ("2" (expand "member") (("2" (lemma "nonempty_card[below(S)]") (("2" (inst - "{s: below(S) | S!1(s) AND f(s) = x!1}") (("1" (assert) (("1" (grind) nil))) ("2" (use "finite_intersect") nil))))))))))))))))))))))) ("2" (use "finite_add") nil))))))))))))))))) ("2" (use "finite_intersect") nil))))))))))))))))) ("2" (grind) (("2" (lemma "nonempty_card[below(S)]") (("2" (inst - "{s: below(S) | S!1(s) AND f(s) = x!1}") (("1" (assert) (("1" (skosimp*) (("1" (lemma "nonempty_card[below(S)]") (("1" (inst?) (("1" (assert) (("1" (inst?) (("1" (prop) nil))))) ("2" (hide-all-but 1) (("2" (use "finite_add") (("2" (inst - "LAMBDA (s: below(S)): f(s) = x!1" "S!1" "e!1") (("2" (grind) nil))))))))))))))) ("2" (hide-all-but 1) (("2" (use "finite_intersect") (("2" (inst - "LAMBDA (s: below(S)): f(s) = x!1" "S!1") (("2" (grind) nil))))))))))))))))))))))))))))))))))))))))))))))))))) ("2" (hide -1 3) (("2" (expand "bag_to_set") (("2" (expand "l_filter") (("2" (lift-if) (("2" (prop) (("2" (expand "make_bag") (("2" (lemma "nonempty_card[below(S)]") (("2" (inst - "{s: below(S) | S!1(s) AND f(s) = f(e!1)}") (("1" (assert) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (skosimp*) (("1" (expand "member") (("1" (flatten) (("1" (lemma "nonempty_card[below(S)]") (("1" (inst - "{s: below(S) | add[below(S)](e!1, S!1)(s) AND f(s) = f(e!1)}") (("1" (assert) (("1" (expand "nonempty?") (("1" (grind) nil))))) ("2" (use "finite_add") nil))))))))))))))))) ("2" (use "finite_intersect") nil))))))))))))))))))))) ("2" (hide 3) (("2" (expand "l_filter") (("2" (lift-if) (("2" (split) (("1" (flatten) (("1" (expand "make_bag") (("1" (case-replace "{s: below(S) | add(e!1, S!1)(s) AND f(s) = f(e!1)} = add(e!1, {s: below(S) | S!1(s) AND f(s) = f(e!1)})") (("1" (lemma "card_add[below(S)]") (("1" (inst - "{s: below(S) | S!1(s) AND f(s) = f(e!1)}" "e!1") (("1" (replace -1) (("1" (assert) nil))) ("2" (use "finite_intersect") nil))))) ("2" (hide -2 2) (("2" (decompose-equality +) (("2" (grind) nil))))))))))) ("2" (flatten) nil))))))))))) ("2" (lemma "sum_x[T,real,0,+]") (("2" (inst?) (("2" (inst - "f(e!1)") (("1" (replace - :hide? t) (("1" (case-replace "remove(f(e!1), bag_to_set(l_filter(make_bag(add(e!1, S!1), f), f(s!1)))) = bag_to_set(l_filter(make_bag(S!1, f), f(s!1)))") (("1" (lemma "sum_particular[T,real,0,+]") (("1" (inst?) (("1" (inst?) (("1" (replace -1 :hide? t) (("1" (assert) (("1" (case "l_filter(make_bag(add(e!1, S!1), f), f(s!1))(f(e!1)) = 1") (("1" (replace - :hide? t) (("1" (assert) (("1" (postpone) nil))))) ("2" (hide -1 4) (("2" (expand "bag_to_set") (("2" (expand "l_filter") (("2" (expand "make_bag") (("2" (lemma "nonempty_card[below(S)]") (("2" (inst - "{s: below(S) | S!1(s) AND f(s) = f(e!1)}") (("1" (assert) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (lemma "card_one[below(S)]") (("1" (inst - "{s: below(S) | add(e!1, S!1)(s) AND f(s) = f(e!1)}") (("1" (assert) (("1" (inst?) (("1" (expand "singleton") (("1" (decompose-equality +) (("1" (grind) nil))))))))) ("2" (use "finite_add") nil))))))))))))) ("2" (use "finite_intersect") nil))))))))))))))))))))))))) ("2" (hide 4) (("2" (decompose-equality +) (("2" (iff) (("2" (grind) (("1" (lemma "nonempty_card[below(S)]") (("1" (inst-cp - "{s: below(S) | (e!1 = s OR S!1(s)) AND f(s) = x!1}") (("1" (assert) (("1" (skosimp*) (("1" (split) (("1" (replace*) nil) ("2" (inst - "{s: below(S) | S!1(s) AND f(s) = x!1}") (("1" (assert) (("1" (inst?) (("1" (split) (("1" (propax) nil) ("2" (propax) nil))))))) ("2" (hide-all-but 1) (("2" (use "finite_intersect") (("2" (inst - "LAMBDA (s: below(S)): f(s) = x!1" "S!1") (("2" (grind) nil))))))))))))))) ("2" (hide-all-but 1) (("2" (use "finite_add") (("2" (inst - "LAMBDA (s: below(S)): f(s) = x!1" "S!1" "e!1") (("2" (grind) nil))))))))))) ("2" (lemma "nonempty_card[below(S)]") (("2" (inst - "{s: below(S) | S!1(s) AND f(s) = x!1}") (("1" (assert) (("1" (skosimp*) (("1" (lemma "nonempty_card[below(S)]") (("1" (inst - "{s: below(S) | (e!1 = s OR S!1(s)) AND f(s) = x!1}") (("1" (assert) (("1" (inst?) (("1" (prop) nil))))) ("2" (hide-all-but 1) (("2" (use "finite_add") (("2" (inst - "LAMBDA (s: below(S)): f(s) = x!1" "S!1" "e!1") (("2" (grind) nil))))))))))))))) ("2" (use "finite_intersect") (("2" (grind) nil))))))))))))))))))) ("2" (hide 4) (("2" (grind) (("2" (lemma "nonempty_card[below(S)]") (("2" (inst - "{s: below(S) | (e!1 = s OR S!1(s)) AND f(s) = f(e!1)}") (("1" (assert) (("1" (inst?) nil))) ("2" (hide-all-but 1) (("2" (use "finite_add") (("2" (grind) nil))))))))))))))))))))))))) ("2" (hide -2 3) (("2" (expand "filter") (("2" (expand "add") (("2" (expand "member") (("2" (case-replace "(LAMBDA (j: below(S)): (e!1 = j OR S!1(j)) AND leq(f(j), f(s!1))) = add(e!1, LAMBDA (j: below(S)): S!1(j) AND leq(f(j), f(s!1)))") (("1" (lemma "card_add[below(S)]") (("1" (inst - "LAMBDA (j: below(S)): S!1(j) AND leq(f(j), f(s!1))" "e!1") (("1" (replace -) (("1" (assert) nil))) ("2" (use "finite_intersect") nil))))) ("2" (hide 2) (("2" (decompose-equality +) (("2" (grind) nil))))))))))))))))) ("2" (case-replace "filter(leq)(add(e!1, S!1))(f)(s!1) = filter(leq)(S!1)(f)(s!1)") (("1" (replace -2 :dir rl :hide? t) (("1" (case-replace "bag_to_set(l_filter(make_bag(add(e!1, S!1), f), f(s!1))) = bag_to_set(l_filter(make_bag(S!1, f), f(s!1)))") (("1" (lemma "sum_particular[T,real,0,+]") (("1" (inst?) (("1" (inst - "f(e!1)") (("1" (replace -1 :hide? t) (("1" (lift-if) (("1" (split) (("1" (flatten) (("1" (case-replace "l_filter(make_bag(add(e!1, S!1), f), f(s!1))(f(e!1)) = 0") (("1" (assert) (("1" (postpone) nil))) ("2" (hide -1 -2 -3 2) (("2" (grind) nil))))))) ("2" (flatten) (("2" (assert) (("2" (postpone) nil))))))))))))))))) ("2" (hide -1 4) (("2" (decompose-equality +) (("2" (grind) (("1" (case "x!1 = f(e!1)") (("1" (hide-all-but (-1 -4 2)) (("1" (typepred! "leq") (("1" (grind) nil))))) ("2" (lemma "nonempty_card[below(S)]") (("2" (inst-cp - "{s: below(S) | (e!1 = s OR S!1(s)) AND f(s) = x!1}") (("1" (assert) (("1" (skosimp*) (("1" (split) (("1" (replace*) nil) ("2" (inst - "{s: below(S) | S!1(s) AND f(s) = x!1}") (("1" (assert) (("1" (inst?) (("1" (assert) nil))))) ("2" (hide-all-but 1) (("2" (use "finite_intersect") (("2" (inst - "LAMBDA (s: below(S)): f(s) = x!1" "S!1") (("2" (grind) nil))))))))))))))) ("2" (hide-all-but 1) (("2" (use "finite_add") (("2" (inst - "LAMBDA (s: below(S)): f(s) = x!1" "S!1" "e!1") (("2" (grind) nil))))))))))))) ("2" (lemma "nonempty_card[below(S)]") (("2" (inst-cp - "{s: below(S) | S!1(s) AND f(s) = x!1}") (("1" (assert) (("1" (skosimp*) (("1" (inst - "{s: below(S) | (e!1 = s OR S!1(s)) AND f(s) = x!1}") (("1" (assert) (("1" (inst?) (("1" (assert) nil))))) ("2" (hide-all-but 1) (("2" (use "finite_add") (("2" (inst - "LAMBDA (s: below(S)): f(s) = x!1" "S!1" "e!1") (("2" (grind) nil))))))))))))) ("2" (hide-all-but 1) (("2" (use "finite_intersect") (("2" (inst - "LAMBDA (s: below(S)): f(s) = x!1" "S!1") (("2" (grind) nil))))))))))))))))))))) ("2" (hide -1 4) (("2" (decompose-equality +) (("2" (grind) nil)))))))))))))))))))))))))))))))))))))))))) nil) unfinished nil 20259 4280 t nil) (mid_val_l-2 nil 3287342858 3287343563 ("" (skolem + ("f" "e" _ "t")) (("" (skosimp*) (("" (expand "middle_value") (("" (flatten) (("" (hide -3) (("" (use "card_make_bag") (("" (replace -1 :hide? t) (("" (case-replace "card(l_filter(make_bag(e, f), t)) = card(filter(leq)(e)(f)(s!1))") (("" (hide -2 2) (("" (expand "card") (("" (typepred! "e") (("" (replace -3 :hide? t) (("" (lemma "finite_set_ind_modified[below(S)]") (("" (inst - "LAMBDA (ee: finite_set[below(S)]): sum(bag_to_set(l_filter(make_bag(ee, f), f(s!1))), LAMBDA (t: T): l_filter(make_bag(ee, f), f(s!1))(t)) = card(filter(leq)(ee)(f)(s!1))") (("" (split) (("1" (inst?) nil) ("2" (hide 3) (("2" (expand "filter") (("2" (lemma "card_empty?[below(S)]") (("2" (inst?) (("1" (case "empty?[below(S)] (LAMBDA (j: below(S)): emptyset(j) AND leq(f(j), f(s!1)))") (("1" (assert) (("1" (replace -2 :hide? t) (("1" (expand "bag_to_set") (("1" (expand "make_bag") (("1" (expand "l_filter") (("1" (case "{t: T | IF leq(t, f(s!1)) THEN card({s: below(S) | emptyset(s) AND f(s) = t}) ELSE 0 ENDIF > 0} = emptyset[T]") (("1" (replace -1 :hide? t) (("1" (use "sum_emptyset[T,real,0,+]") (("1" (skosimp*) (("1" (use "finite_empty") nil))))))) ("2" (hide 2) (("2" (decompose-equality +) (("1" (grind) (("1" (use "card_emptyset[below(S)]") (("1" (expand "emptyset") (("1" (assert) nil))))))) ("2" (skosimp*) (("2" (use "finite_empty") nil))))))) ("3" (skosimp*) (("3" (use "finite_empty") nil))))))))))))))) ("2" (hide 2 -1) (("2" (grind) nil))))) ("2" (use "finite_empty") nil))))))))) ("3" (skosimp*) (("3" (hide 4) (("3" (case "leq(f(e!1),f(s!1))") (("1" (case-replace "card(filter(leq)(add(e!1, S!1))(f)(s!1)) = card(filter(leq)(S!1)(f)(s!1)) + 1") (("1" (replace -3 :dir rl :hide? t) (("1" (hide -1) (("1" (case "bag_to_set(l_filter(make_bag(S!1, f), f(s!1)))(f(e!1))") (("1" (case "l_filter(make_bag(add(e!1, S!1), f), f(s!1))(f(e!1)) = l_filter(make_bag(S!1, f), f(s!1))(f(e!1)) + 1") (("1" (lemma "sum_x[T,real,0,+]") (("1" (inst-cp - "bag_to_set(l_filter(make_bag(add(e!1, S!1), f), f(s!1)))" "LAMBDA (t: T): l_filter(make_bag(add(e!1, S!1), f), f(s!1))(t)" "f(e!1)") (("1" (inst - "bag_to_set(l_filter(make_bag(S!1, f), f(s!1)))" "LAMBDA (t: T): l_filter(make_bag(S!1, f), f(s!1))(t)" "f(e!1)") (("1" (replace*) (("1" (hide -1 -2 -3) (("1" (assert) (("1" (lemma "sum_particular2[T,real,0,+]") (("1" (inst - "remove(f(e!1), bag_to_set(l_filter(make_bag(add(e!1, S!1), f), f(s!1))))" "LAMBDA (t: T): l_filter(make_bag(add(e!1, S!1), f), f(s!1))(t)" "f(e!1)") (("1" (replace - :hide? t) (("1" (lift-if) (("1" (split) (("1" (flatten) (("1" (hide-all-but -1) (("1" (grind) nil))))) ("2" (flatten) (("2" (hide 1) (("2" (assert) (("2" (name-replace "g" "LAMBDA (t: T): l_filter(make_bag(add(e!1, S!1), f), f(s!1))(t)") (("2" (case-replace "remove(f(e!1), bag_to_set(l_filter(make_bag(add(e!1, S!1), f), f(s!1)))) = remove(f(e!1), bag_to_set(l_filter(make_bag(S!1, f), f(s!1))))") (("1" (postpone) nil) ("2" (hide 2) (("2" (decompose-equality +) (("2" (expand "remove") (("2" (iff) (("2" (prop) (("1" (expand "member") (("1" (expand "bag_to_set") (("1" (expand "l_filter") (("1" (lift-if) (("1" (prop) (("1" (expand "make_bag") (("1" (lemma "nonempty_card[below(S)]") (("1" (inst - "{s: below(S) | S!1(s) AND f(s) = f(e!1)}") (("1" (assert) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (skosimp*) (("1" (expand "member") (("1" (flatten) (("1" (lemma "nonempty_card[below(S)]") (("1" (inst?) (("1" (assert) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (skosimp*) (("1" (expand "member") (("1" (expand "add") (("1" (flatten) (("1" (split) (("1" (lemma "nonempty_card[below(S)]") (("1" (inst - "{s: below(S) | S!1(s) AND f(s) = x!1}") (("1" (assert) nil) ("2" (use "finite_intersect") nil))))) ("2" (expand "member") (("2" (lemma "nonempty_card[below(S)]") (("2" (inst - "{s: below(S) | S!1(s) AND f(s) = x!1}") (("1" (assert) (("1" (grind) nil))) ("2" (use "finite_intersect") nil))))))))))))))))))))))) ("2" (use "finite_add") nil))))))))))))))))) ("2" (use "finite_intersect") nil))))))))))))))))) ("2" (grind) (("2" (lemma "nonempty_card[below(S)]") (("2" (inst - "{s: below(S) | S!1(s) AND f(s) = x!1}") (("1" (assert) (("1" (skosimp*) (("1" (lemma "nonempty_card[below(S)]") (("1" (inst?) (("1" (assert) (("1" (inst?) (("1" (prop) nil))))) ("2" (hide-all-but 1) (("2" (use "finite_add") (("2" (inst - "LAMBDA (s: below(S)): f(s) = x!1" "S!1" "e!1") (("2" (grind) nil))))))))))))))) ("2" (hide-all-but 1) (("2" (use "finite_intersect") (("2" (inst - "LAMBDA (s: below(S)): f(s) = x!1" "S!1") (("2" (grind) nil))))))))))))))))))))))))))))))))))))))))))))))))))) ("2" (hide -1 3) (("2" (expand "bag_to_set") (("2" (expand "l_filter") (("2" (lift-if) (("2" (prop) (("2" (expand "make_bag") (("2" (lemma "nonempty_card[below(S)]") (("2" (inst - "{s: below(S) | S!1(s) AND f(s) = f(e!1)}") (("1" (assert) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (skosimp*) (("1" (expand "member") (("1" (flatten) (("1" (lemma "nonempty_card[below(S)]") (("1" (inst - "{s: below(S) | add[below(S)](e!1, S!1)(s) AND f(s) = f(e!1)}") (("1" (assert) (("1" (expand "nonempty?") (("1" (grind) nil))))) ("2" (use "finite_add") nil))))))))))))))))) ("2" (use "finite_intersect") nil))))))))))))))))))))) ("2" (hide 3) (("2" (expand "l_filter") (("2" (lift-if) (("2" (split) (("1" (flatten) (("1" (expand "make_bag") (("1" (case-replace "{s: below(S) | add(e!1, S!1)(s) AND f(s) = f(e!1)} = add(e!1, {s: below(S) | S!1(s) AND f(s) = f(e!1)})") (("1" (lemma "card_add[below(S)]") (("1" (inst - "{s: below(S) | S!1(s) AND f(s) = f(e!1)}" "e!1") (("1" (replace -1) (("1" (assert) nil))) ("2" (use "finite_intersect") nil))))) ("2" (hide -2 2) (("2" (decompose-equality +) (("2" (grind) nil))))))))))) ("2" (flatten) nil))))))))))) ("2" (lemma "sum_x[T,real,0,+]") (("2" (inst?) (("2" (inst - "f(e!1)") (("1" (replace - :hide? t) (("1" (case-replace "remove(f(e!1), bag_to_set(l_filter(make_bag(add(e!1, S!1), f), f(s!1)))) = bag_to_set(l_filter(make_bag(S!1, f), f(s!1)))") (("1" (lemma "sum_particular2[T,real,0,+]") (("1" (inst?) (("1" (inst?) (("1" (replace -1 :hide? t) (("1" (assert) (("1" (case "l_filter(make_bag(add(e!1, S!1), f), f(s!1))(f(e!1)) = 1") (("1" (replace - :hide? t) (("1" (assert) (("1" (postpone) nil))))) ("2" (hide -1 4) (("2" (expand "bag_to_set") (("2" (expand "l_filter") (("2" (expand "make_bag") (("2" (lemma "nonempty_card[below(S)]") (("2" (inst - "{s: below(S) | S!1(s) AND f(s) = f(e!1)}") (("1" (assert) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (lemma "card_one[below(S)]") (("1" (inst - "{s: below(S) | add(e!1, S!1)(s) AND f(s) = f(e!1)}") (("1" (assert) (("1" (inst?) (("1" (expand "singleton") (("1" (decompose-equality +) (("1" (grind) nil))))))))) ("2" (use "finite_add") nil))))))))))))) ("2" (use "finite_intersect") nil))))))))))))))))))))))))) ("2" (hide 4) (("2" (decompose-equality +) (("2" (iff) (("2" (grind) (("1" (lemma "nonempty_card[below(S)]") (("1" (inst-cp - "{s: below(S) | (e!1 = s OR S!1(s)) AND f(s) = x!1}") (("1" (assert) (("1" (skosimp*) (("1" (split) (("1" (replace*) nil) ("2" (inst - "{s: below(S) | S!1(s) AND f(s) = x!1}") (("1" (assert) (("1" (inst?) (("1" (split) (("1" (propax) nil) ("2" (propax) nil))))))) ("2" (hide-all-but 1) (("2" (use "finite_intersect") (("2" (inst - "LAMBDA (s: below(S)): f(s) = x!1" "S!1") (("2" (grind) nil))))))))))))))) ("2" (hide-all-but 1) (("2" (use "finite_add") (("2" (inst - "LAMBDA (s: below(S)): f(s) = x!1" "S!1" "e!1") (("2" (grind) nil))))))))))) ("2" (lemma "nonempty_card[below(S)]") (("2" (inst - "{s: below(S) | S!1(s) AND f(s) = x!1}") (("1" (assert) (("1" (skosimp*) (("1" (lemma "nonempty_card[below(S)]") (("1" (inst - "{s: below(S) | (e!1 = s OR S!1(s)) AND f(s) = x!1}") (("1" (assert) (("1" (inst?) (("1" (prop) nil))))) ("2" (hide-all-but 1) (("2" (use "finite_add") (("2" (inst - "LAMBDA (s: below(S)): f(s) = x!1" "S!1" "e!1") (("2" (grind) nil))))))))))))))) ("2" (use "finite_intersect") (("2" (grind) nil))))))))))))))))))) ("2" (hide 4) (("2" (grind) (("2" (lemma "nonempty_card[below(S)]") (("2" (inst - "{s: below(S) | (e!1 = s OR S!1(s)) AND f(s) = f(e!1)}") (("1" (assert) (("1" (inst?) nil))) ("2" (hide-all-but 1) (("2" (use "finite_add") (("2" (grind) nil))))))))))))))))))))))))) ("2" (hide -2 3) (("2" (expand "filter") (("2" (expand "add") (("2" (expand "member") (("2" (case-replace "(LAMBDA (j: below(S)): (e!1 = j OR S!1(j)) AND leq(f(j), f(s!1))) = add(e!1, LAMBDA (j: below(S)): S!1(j) AND leq(f(j), f(s!1)))") (("1" (lemma "card_add[below(S)]") (("1" (inst - "LAMBDA (j: below(S)): S!1(j) AND leq(f(j), f(s!1))" "e!1") (("1" (replace -) (("1" (assert) nil))) ("2" (use "finite_intersect") nil))))) ("2" (hide 2) (("2" (decompose-equality +) (("2" (grind) nil))))))))))))))))) ("2" (case-replace "filter(leq)(add(e!1, S!1))(f)(s!1) = filter(leq)(S!1)(f)(s!1)") (("1" (replace -2 :dir rl :hide? t) (("1" (case-replace "bag_to_set(l_filter(make_bag(add(e!1, S!1), f), f(s!1))) = bag_to_set(l_filter(make_bag(S!1, f), f(s!1)))") (("1" (lemma "sum_particular2[T,real,0,+]") (("1" (inst?) (("1" (inst - "f(e!1)") (("1" (replace -1 :hide? t) (("1" (lift-if) (("1" (split) (("1" (flatten) (("1" (case-replace "l_filter(make_bag(add(e!1, S!1), f), f(s!1))(f(e!1)) = 0") (("1" (assert) (("1" (postpone) nil))) ("2" (hide -1 -2 -3 2) (("2" (grind) nil))))))) ("2" (flatten) (("2" (assert) (("2" (postpone) nil))))))))))))))))) ("2" (hide -1 4) (("2" (decompose-equality +) (("2" (grind) (("1" (case "x!1 = f(e!1)") (("1" (hide-all-but (-1 -4 2)) (("1" (typepred! "leq") (("1" (grind) nil))))) ("2" (lemma "nonempty_card[below(S)]") (("2" (inst-cp - "{s: below(S) | (e!1 = s OR S!1(s)) AND f(s) = x!1}") (("1" (assert) (("1" (skosimp*) (("1" (split) (("1" (replace*) nil) ("2" (inst - "{s: below(S) | S!1(s) AND f(s) = x!1}") (("1" (assert) (("1" (inst?) (("1" (assert) nil))))) ("2" (hide-all-but 1) (("2" (use "finite_intersect") (("2" (inst - "LAMBDA (s: below(S)): f(s) = x!1" "S!1") (("2" (grind) nil))))))))))))))) ("2" (hide-all-but 1) (("2" (use "finite_add") (("2" (inst - "LAMBDA (s: below(S)): f(s) = x!1" "S!1" "e!1") (("2" (grind) nil))))))))))))) ("2" (lemma "nonempty_card[below(S)]") (("2" (inst-cp - "{s: below(S) | S!1(s) AND f(s) = x!1}") (("1" (assert) (("1" (skosimp*) (("1" (inst - "{s: below(S) | (e!1 = s OR S!1(s)) AND f(s) = x!1}") (("1" (assert) (("1" (inst?) (("1" (assert) nil))))) ("2" (hide-all-but 1) (("2" (use "finite_add") (("2" (inst - "LAMBDA (s: below(S)): f(s) = x!1" "S!1" "e!1") (("2" (grind) nil))))))))))))) ("2" (hide-all-but 1) (("2" (use "finite_intersect") (("2" (inst - "LAMBDA (s: below(S)): f(s) = x!1" "S!1") (("2" (grind) nil))))))))))))))))))))) ("2" (hide -1 4) (("2" (decompose-equality +) (("2" (grind) nil)))))))))))))))))))))))))))))))))))))))))) nil) unfinished nil 9459 290 t nil) (mid_val_l-1 nil 3287341697 3287342318 ("" (skolem + ("f" "e" _ "t")) (("" (skosimp*) (("" (expand "middle_value") (("" (flatten) (("" (hide -3) (("" (use "card_make_bag") (("" (replace -1 :hide? t) (("" (case-replace "card(l_filter(make_bag(e, f), t)) = card(filter(leq)(e)(f)(s!1))") (("" (hide -2 2) (("" (expand "card") (("" (typepred! "e") (("" (replace -3 :hide? t) (("" (lemma "finite_set_ind_modified[below(S)]") (("" (inst - "LAMBDA (ee: finite_set[below(S)]): sum(bag_to_set(l_filter(make_bag(ee, f), f(s!1))), LAMBDA (t: T): l_filter(make_bag(ee, f), f(s!1))(t)) = card(filter(leq)(ee)(f)(s!1))") (("" (split) (("1" (inst?) nil nil) ("2" (hide 3) (("2" (expand "filter") (("2" (lemma "card_empty?[below(S)]") (("2" (inst?) (("1" (case "empty?[below(S)] (LAMBDA (j: below(S)): emptyset(j) AND leq(f(j), f(s!1)))") (("1" (assert) (("1" (replace -2 :hide? t) (("1" (expand "bag_to_set") (("1" (expand "make_bag") (("1" (expand "l_filter") (("1" (case "{t: T | IF leq(t, f(s!1)) THEN card({s: below(S) | emptyset(s) AND f(s) = t}) ELSE 0 ENDIF > 0} = emptyset[T]") (("1" (replace -1 :hide? t) (("1" (use "sum_emptyset[T,real,0,+]") (("1" (skosimp*) (("1" (use "finite_empty") nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (decompose-equality +) (("1" (grind) (("1" (use "card_emptyset[below(S)]") (("1" (expand "emptyset") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (use "finite_empty") nil nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (use "finite_empty") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2 -1) (("2" (grind) nil nil)) nil)) nil) ("2" (use "finite_empty") nil nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (hide 4) (("3" (case "leq(f(e!1),f(s!1))") (("1" (case-replace "card(filter(leq)(add(e!1, S!1))(f)(s!1)) = card(filter(leq)(S!1)(f)(s!1)) + 1") (("1" (replace -3 :dir rl :hide? t) (("1" (hide -1) (("1" (case "bag_to_set(l_filter(make_bag(S!1, f), f(s!1)))(f(e!1))") (("1" (case "l_filter(make_bag(add(e!1, S!1), f), f(s!1))(f(e!1)) = l_filter(make_bag(S!1, f), f(s!1))(f(e!1)) + 1") (("1" (lemma "sum_x[T,real,0,+]") (("1" (inst-cp - "bag_to_set(l_filter(make_bag(add(e!1, S!1), f), f(s!1)))" "LAMBDA (t: T): l_filter(make_bag(add(e!1, S!1), f), f(s!1))(t)" "f(e!1)") (("1" (inst - "bag_to_set(l_filter(make_bag(S!1, f), f(s!1)))" "LAMBDA (t: T): l_filter(make_bag(S!1, f), f(s!1))(t)" "f(e!1)") (("1" (replace*) (("1" (hide -1 -2 -3) (("1" (assert) (("1" (lemma "sum_particular[T,real,0,+]") (("1" (inst - "remove(f(e!1), bag_to_set(l_filter(make_bag(add(e!1, S!1), f), f(s!1))))" "LAMBDA (t: T): l_filter(make_bag(add(e!1, S!1), f), f(s!1))(t)" "f(e!1)") (("1" (replace - :hide? t) (("1" (lift-if) (("1" (split) (("1" (flatten) (("1" (hide-all-but -1) (("1" (grind) nil nil)) nil)) nil) ("2" (flatten) (("2" (hide 1) (("2" (assert) (("2" (name-replace "g" "LAMBDA (t: T): l_filter(make_bag(add(e!1, S!1), f), f(s!1))(t)") (("2" (case-replace "remove(f(e!1), bag_to_set(l_filter(make_bag(add(e!1, S!1), f), f(s!1)))) = remove(f(e!1), bag_to_set(l_filter(make_bag(S!1, f), f(s!1))))") (("1" (postpone) nil nil) ("2" (hide 2) (("2" (decompose-equality +) (("2" (expand "remove") (("2" (iff) (("2" (prop) (("1" (expand "member") (("1" (expand "bag_to_set") (("1" (expand "l_filter") (("1" (lift-if) (("1" (prop) (("1" (expand "make_bag") (("1" (lemma "nonempty_card[below(S)]") (("1" (inst - "{s: below(S) | S!1(s) AND f(s) = f(e!1)}") (("1" (assert) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (skosimp*) (("1" (expand "member") (("1" (flatten) (("1" (lemma "nonempty_card[below(S)]") (("1" (inst?) (("1" (assert) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (skosimp*) (("1" (expand "member") (("1" (expand "add") (("1" (flatten) (("1" (split) (("1" (lemma "nonempty_card[below(S)]") (("1" (inst - "{s: below(S) | S!1(s) AND f(s) = x!1}") (("1" (assert) nil nil) ("2" (use "finite_intersect") nil nil)) nil)) nil) ("2" (expand "member") (("2" (lemma "nonempty_card[below(S)]") (("2" (inst - "{s: below(S) | S!1(s) AND f(s) = x!1}") (("1" (assert) (("1" (grind) nil nil)) nil) ("2" (use "finite_intersect") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (use "finite_add") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (use "finite_intersect") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (grind) (("2" (lemma "nonempty_card[below(S)]") (("2" (inst - "{s: below(S) | S!1(s) AND f(s) = x!1}") (("1" (assert) (("1" (skosimp*) (("1" (lemma "nonempty_card[below(S)]") (("1" (inst?) (("1" (assert) (("1" (inst?) (("1" (prop) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (use "finite_add") (("2" (inst - "LAMBDA (s: below(S)): f(s) = x!1" "S!1" "e!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (use "finite_intersect") (("2" (inst - "LAMBDA (s: below(S)): f(s) = x!1" "S!1") (("2" (grind) 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 3) (("2" (expand "bag_to_set") (("2" (expand "l_filter") (("2" (lift-if) (("2" (prop) (("2" (expand "make_bag") (("2" (lemma "nonempty_card[below(S)]") (("2" (inst - "{s: below(S) | S!1(s) AND f(s) = f(e!1)}") (("1" (assert) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (skosimp*) (("1" (expand "member") (("1" (flatten) (("1" (lemma "nonempty_card[below(S)]") (("1" (inst - "{s: below(S) | add[below(S)](e!1, S!1)(s) AND f(s) = f(e!1)}") (("1" (assert) (("1" (expand "nonempty?") (("1" (grind) nil nil)) nil)) nil) ("2" (use "finite_add") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (use "finite_intersect") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 3) (("2" (expand "l_filter") (("2" (lift-if) (("2" (split) (("1" (flatten) (("1" (expand "make_bag") (("1" (case-replace "{s: below(S) | add(e!1, S!1)(s) AND f(s) = f(e!1)} = add(e!1, {s: below(S) | S!1(s) AND f(s) = f(e!1)})") (("1" (lemma "card_add[below(S)]") (("1" (inst - "{s: below(S) | S!1(s) AND f(s) = f(e!1)}" "e!1") (("1" (replace -1) (("1" (assert) nil nil)) nil) ("2" (use "finite_intersect") nil nil)) nil)) nil) ("2" (hide -2 2) (("2" (decompose-equality +) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "sum_x[T,real,0,+]") (("2" (inst?) (("2" (inst - "f(e!1)") (("1" (replace - :hide? t) (("1" (case-replace "remove(f(e!1), bag_to_set(l_filter(make_bag(add(e!1, S!1), f), f(s!1)))) = bag_to_set(l_filter(make_bag(S!1, f), f(s!1)))") (("1" (lemma "sum_particular[T,real,0,+]") (("1" (inst?) (("1" (inst?) (("1" (replace -1 :hide? t) (("1" (assert) (("1" (case "l_filter(make_bag(add(e!1, S!1), f), f(s!1))(f(e!1)) = 1") (("1" (replace - :hide? t) (("1" (assert) (("1" (postpone) nil nil)) nil)) nil) ("2" (hide -1 4) (("2" (expand "bag_to_set") (("2" (expand "l_filter") (("2" (expand "make_bag") (("2" (lemma "nonempty_card[below(S)]") (("2" (inst - "{s: below(S) | S!1(s) AND f(s) = f(e!1)}") (("1" (assert) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (lemma "card_one[below(S)]") (("1" (inst - "{s: below(S) | add(e!1, S!1)(s) AND f(s) = f(e!1)}") (("1" (assert) (("1" (inst?) (("1" (expand "singleton") (("1" (decompose-equality +) (("1" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (use "finite_add") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (use "finite_intersect") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 4) (("2" (decompose-equality +) (("2" (iff) (("2" (grind) (("1" (lemma "nonempty_card[below(S)]") (("1" (inst-cp - "{s: below(S) | (e!1 = s OR S!1(s)) AND f(s) = x!1}") (("1" (assert) (("1" (skosimp*) (("1" (split) (("1" (replace*) nil nil) ("2" (inst - "{s: below(S) | S!1(s) AND f(s) = x!1}") (("1" (assert) (("1" (inst?) (("1" (split) (("1" (propax) nil nil) ("2" (propax) nil nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (use "finite_intersect") (("2" (inst - "LAMBDA (s: below(S)): f(s) = x!1" "S!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (use "finite_add") (("2" (inst - "LAMBDA (s: below(S)): f(s) = x!1" "S!1" "e!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "nonempty_card[below(S)]") (("2" (inst - "{s: below(S) | S!1(s) AND f(s) = x!1}") (("1" (assert) (("1" (skosimp*) (("1" (lemma "nonempty_card[below(S)]") (("1" (inst - "{s: below(S) | (e!1 = s OR S!1(s)) AND f(s) = x!1}") (("1" (assert) (("1" (inst?) (("1" (prop) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (use "finite_add") (("2" (inst - "LAMBDA (s: below(S)): f(s) = x!1" "S!1" "e!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (use "finite_intersect") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 4) (("2" (grind) (("2" (lemma "nonempty_card[below(S)]") (("2" (inst - "{s: below(S) | (e!1 = s OR S!1(s)) AND f(s) = f(e!1)}") (("1" (assert) (("1" (inst?) nil nil)) nil) ("2" (hide-all-but 1) (("2" (use "finite_add") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -2 3) (("2" (expand "filter") (("2" (expand "add") (("2" (expand "member") (("2" (case-replace "(LAMBDA (j: below(S)): (e!1 = j OR S!1(j)) AND leq(f(j), f(s!1))) = add(e!1, LAMBDA (j: below(S)): S!1(j) AND leq(f(j), f(s!1)))") (("1" (lemma "card_add[below(S)]") (("1" (inst - "LAMBDA (j: below(S)): S!1(j) AND leq(f(j), f(s!1))" "e!1") (("1" (replace -) (("1" (assert) nil nil)) nil) ("2" (use "finite_intersect") nil nil)) nil)) nil) ("2" (hide 2) (("2" (decompose-equality +) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case-replace "filter(leq)(add(e!1, S!1))(f)(s!1) = filter(leq)(S!1)(f)(s!1)") (("1" (replace -2 :dir rl :hide? t) (("1" (case-replace "bag_to_set(l_filter(make_bag(add(e!1, S!1), f), f(s!1))) = bag_to_set(l_filter(make_bag(S!1, f), f(s!1)))") (("1" (lemma "sum_particular[T,real,0,+]") (("1" (inst?) (("1" (inst - "f(e!1)") (("1" (replace -1 :hide? t) (("1" (lift-if) (("1" (split) (("1" (flatten) (("1" (case-replace "l_filter(make_bag(add(e!1, S!1), f), f(s!1))(f(e!1)) = 0") (("1" (assert) (("1" (postpone) nil nil)) nil) ("2" (hide -1 -2 -3 2) (("2" (grind) nil nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) (("2" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 4) (("2" (decompose-equality +) (("2" (grind) (("1" (case "x!1 = f(e!1)") (("1" (hide-all-but (-1 -4 2)) (("1" (typepred! "leq") (("1" (grind) nil nil)) nil)) nil) ("2" (lemma "nonempty_card[below(S)]") (("2" (inst-cp - "{s: below(S) | (e!1 = s OR S!1(s)) AND f(s) = x!1}") (("1" (assert) (("1" (skosimp*) (("1" (split) (("1" (replace*) nil nil) ("2" (inst - "{s: below(S) | S!1(s) AND f(s) = x!1}") (("1" (assert) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (use "finite_intersect") (("2" (inst - "LAMBDA (s: below(S)): f(s) = x!1" "S!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (use "finite_add") (("2" (inst - "LAMBDA (s: below(S)): f(s) = x!1" "S!1" "e!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "nonempty_card[below(S)]") (("2" (inst-cp - "{s: below(S) | S!1(s) AND f(s) = x!1}") (("1" (assert) (("1" (skosimp*) (("1" (inst - "{s: below(S) | (e!1 = s OR S!1(s)) AND f(s) = x!1}") (("1" (assert) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (use "finite_add") (("2" (inst - "LAMBDA (s: below(S)): f(s) = x!1" "S!1" "e!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (use "finite_intersect") (("2" (inst - "LAMBDA (s: below(S)): f(s) = x!1" "S!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 4) (("2" (decompose-equality +) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unchecked nil 620668 102730 t shostak)) (mid_val_u 0 (mid_val_u-8 nil 3287751459 3292683160 ("" (skolem + ("f" "e" _ "t")) (("" (skosimp*) (("" (expand "middle_value") (("" (flatten) (("" (hide -2) (("" (use "card_make_bag") (("" (replace -1 :hide? t) (("" (case-replace "card(u_filter(make_bag(e, f), t)) = card(filter(geq)(e)(f)(s!1))") (("" (hide -2 2) (("" (expand "card") (("" (typepred! "e") (("" (replace -3 :hide? t) (("" (lemma "finite_set_ind_modified[below(S)]") (("" (inst - "LAMBDA (ee: finite_set[below(S)]): sum(bag_to_set(u_filter(make_bag(ee, f), f(s!1))), LAMBDA (t: T): u_filter(make_bag(ee, f), f(s!1))(t)) = card(filter(geq)(ee)(f)(s!1))") (("" (split) (("1" (inst?) nil nil) ("2" (hide 3) (("2" (expand "filter") (("2" (lemma "card_empty?[below(S)]") (("2" (inst?) (("1" (case "empty?[below(S)] (LAMBDA (j: below(S)): emptyset(j) AND geq(f(j), f(s!1)))") (("1" (assert) (("1" (replace -2 :hide? t) (("1" (expand "bag_to_set") (("1" (expand "make_bag") (("1" (expand "u_filter") (("1" (case "{t: T | IF leq(f(s!1), t) THEN card({s: below(S) | emptyset(s) AND f(s) = t}) ELSE 0 ENDIF > 0} = emptyset[T]") (("1" (replace -1 :hide? t) (("1" (use "sum_emptyset[T,real,0,+]") (("1" (skosimp*) (("1" (use "finite_empty") nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (decompose-equality +) (("1" (grind) (("1" (use "card_emptyset[below(S)]") (("1" (expand "emptyset") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (use "finite_empty") nil nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (use "finite_empty") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2 -1) (("2" (grind) nil nil)) nil)) nil) ("2" (use "finite_empty") nil nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (hide 4) (("3" (case "geq(f(e!1), f(s!1))") (("1" (case-replace "card(filter(geq)(add(e!1, S!1))(f)(s!1)) = card(filter(geq)(S!1)(f)(s!1)) + 1") (("1" (replace -3 :dir rl :hide? t) (("1" (hide -1) (("1" (case "bag_to_set(u_filter(make_bag(S!1, f), f(s!1)))(f(e!1))") (("1" (case "u_filter(make_bag(add(e!1, S!1), f), f(s!1))(f(e!1)) = u_filter(make_bag(S!1, f), f(s!1))(f(e!1)) + 1") (("1" (lemma "sum_x[T,real,0,+]") (("1" (inst-cp - "bag_to_set(u_filter(make_bag(add(e!1, S!1), f), f(s!1)))" "LAMBDA (t: T): u_filter(make_bag(add(e!1, S!1), f), f(s!1))(t)" "f(e!1)") (("1" (inst - "bag_to_set(u_filter(make_bag(S!1, f), f(s!1)))" "LAMBDA (t: T): u_filter(make_bag(S!1, f), f(s!1))(t)" "f(e!1)") (("1" (replace*) (("1" (hide -1 -2 -3) (("1" (assert) (("1" (lemma "sum_particular2[T,real,0,+]") (("1" (inst - "remove(f(e!1), bag_to_set(u_filter(make_bag(add(e!1, S!1), f), f(s!1))))" "LAMBDA (t: T): u_filter(make_bag(add(e!1, S!1), f), f(s!1))(t)" "f(e!1)") (("1" (replace - :hide? t) (("1" (lift-if) (("1" (split) (("1" (flatten) (("1" (hide-all-but -1) (("1" (grind) nil nil)) nil)) nil) ("2" (flatten) (("2" (hide 1) (("2" (assert) (("2" (name-replace "g" "LAMBDA (t: T): u_filter(make_bag(add(e!1, S!1), f), f(s!1))(t)") (("2" (case-replace "remove(f(e!1), bag_to_set(u_filter(make_bag(add(e!1, S!1), f), f(s!1)))) = remove(f(e!1), bag_to_set(u_filter(make_bag(S!1, f), f(s!1))))") (("1" (hide -1) (("1" (use "sum_f_g[T,real,0,+]") (("1" (split) (("1" (propax) nil nil) ("2" (skosimp*) (("2" (hide 2) (("2" (lift-if) (("2" (typepred! "x!1") (("2" (split) (("1" (flatten) (("1" (grind) nil nil)) nil) ("2" (flatten) (("2" (hide -4 -5 4) (("2" (grind) (("2" (case-replace "{s: below(S) | (e!1 = s OR S!1(s)) AND f(s) = x!1} = {s: below(S) | S!1(s) AND f(s) = x!1}") (("2" (hide 3) (("2" (decompose-equality +) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (decompose-equality +) (("2" (expand "remove") (("2" (iff) (("2" (prop) (("1" (expand "member") (("1" (expand "bag_to_set") (("1" (expand "u_filter") (("1" (lift-if) (("1" (expand "geq") (("1" (assert) (("1" (prop) (("1" (expand "make_bag") (("1" (lemma "nonempty_card[below(S)]") (("1" (inst - "{s: below(S) | S!1(s) AND f(s) = f(e!1)}") (("1" (assert) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (skosimp*) (("1" (expand "member") (("1" (flatten) (("1" (lemma "nonempty_card[below(S)]") (("1" (inst?) (("1" (assert) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (skosimp*) (("1" (expand "member") (("1" (expand "add") (("1" (flatten) (("1" (split) (("1" (lemma "nonempty_card[below(S)]") (("1" (inst - "{s: below(S) | S!1(s) AND f(s) = x!1}") (("1" (assert) nil nil) ("2" (use "finite_intersect") nil nil)) nil)) nil) ("2" (expand "member") (("2" (lemma "nonempty_card[below(S)]") (("2" (inst - "{s: below(S) | S!1(s) AND f(s) = x!1}") (("1" (assert) (("1" (grind) nil nil)) nil) ("2" (use "finite_intersect") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (use "finite_add") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (use "finite_intersect") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (grind) (("2" (lemma "nonempty_card[below(S)]") (("2" (inst - "{s: below(S) | S!1(s) AND f(s) = x!1}") (("1" (assert) (("1" (skosimp*) (("1" (lemma "nonempty_card[below(S)]") (("1" (inst?) (("1" (assert) (("1" (inst?) (("1" (prop) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (use "finite_add") (("2" (inst - "LAMBDA (s: below(S)): f(s) = x!1" "S!1" "e!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (use "finite_intersect") (("2" (inst - "LAMBDA (s: below(S)): f(s) = x!1" "S!1") (("2" (grind) 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 3) (("2" (expand "bag_to_set") (("2" (expand "u_filter") (("2" (lift-if) (("2" (prop) (("2" (expand "make_bag") (("2" (lemma "nonempty_card[below(S)]") (("2" (inst - "{s: below(S) | S!1(s) AND f(s) = f(e!1)}") (("1" (assert) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (skosimp*) (("1" (expand "member") (("1" (flatten) (("1" (lemma "nonempty_card[below(S)]") (("1" (inst - "{s: below(S) | add[below(S)](e!1, S!1)(s) AND f(s) = f(e!1)}") (("1" (assert) (("1" (expand "nonempty?") (("1" (grind) nil nil)) nil)) nil) ("2" (use "finite_add") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (use "finite_intersect") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 3) (("2" (expand "u_filter") (("2" (lift-if) (("2" (split) (("1" (flatten) (("1" (expand "make_bag") (("1" (case-replace "{s: below(S) | add(e!1, S!1)(s) AND f(s) = f(e!1)} = add(e!1, {s: below(S) | S!1(s) AND f(s) = f(e!1)})") (("1" (lemma "card_add[below(S)]") (("1" (inst - "{s: below(S) | S!1(s) AND f(s) = f(e!1)}" "e!1") (("1" (replace -1) (("1" (assert) nil nil)) nil) ("2" (use "finite_intersect") nil nil)) nil)) nil) ("2" (hide -2 2) (("2" (decompose-equality +) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "geq") (("2" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "sum_x[T,real,0,+]") (("2" (inst?) (("2" (inst - "f(e!1)") (("1" (replace - :hide? t) (("1" (case-replace "remove(f(e!1), bag_to_set(u_filter(make_bag(add(e!1, S!1), f), f(s!1)))) = bag_to_set(u_filter(make_bag(S!1, f), f(s!1)))") (("1" (lemma "sum_particular2[T,real,0,+]") (("1" (inst?) (("1" (inst?) (("1" (replace -1 :hide? t) (("1" (assert) (("1" (case "u_filter(make_bag(add(e!1, S!1), f), f(s!1))(f(e!1)) = 1") (("1" (replace - :hide? t) (("1" (assert) (("1" (case-replace "(LAMBDA (t_1: T): IF t_1 = f(e!1) THEN 0 ELSE u_filter(make_bag(add(e!1, S!1), f), f(s!1))(t_1) ENDIF) = LAMBDA (t: T): u_filter(make_bag(S!1, f), f(s!1))(t)") (("1" (hide 4) (("1" (decompose-equality +) (("1" (lift-if) (("1" (split) (("1" (flatten) (("1" (expand "bag_to_set") (("1" (assert) nil nil)) nil)) nil) ("2" (flatten) (("2" (hide -1) (("2" (expand "bag_to_set") (("2" (expand "u_filter") (("2" (lift-if) (("2" (split) (("1" (flatten) (("1" (expand "make_bag") (("1" (expand "add") (("1" (expand "member") (("1" (case-replace "{s: below(S) | (e!1 = s OR S!1(s)) AND f(s) = x!1} = {s: below(S) | S!1(s) AND f(s) = x!1}") (("1" (hide 2) (("1" (decompose-equality +) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 4) (("2" (expand "bag_to_set") (("2" (expand "u_filter") (("2" (expand "make_bag") (("2" (lemma "nonempty_card[below(S)]") (("2" (inst - "{s: below(S) | S!1(s) AND f(s) = f(e!1)}") (("1" (assert) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (lemma "card_one[below(S)]") (("1" (expand "geq") (("1" (inst - "{s: below(S) | add(e!1, S!1)(s) AND f(s) = f(e!1)}") (("1" (assert) (("1" (assert) (("1" (inst?) (("1" (expand "singleton") (("1" (decompose-equality +) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (use "finite_add") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (use "finite_intersect") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 4) (("2" (decompose-equality +) (("2" (iff) (("2" (grind) (("1" (lemma "nonempty_card[below(S)]") (("1" (inst-cp - "{s: below(S) | (e!1 = s OR S!1(s)) AND f(s) = x!1}") (("1" (assert) (("1" (skosimp*) (("1" (split) (("1" (replace*) nil nil) ("2" (inst - "{s: below(S) | S!1(s) AND f(s) = x!1}") (("1" (assert) (("1" (inst?) (("1" (split) (("1" (propax) nil nil) ("2" (propax) nil nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (use "finite_intersect") (("2" (inst - "LAMBDA (s: below(S)): f(s) = x!1" "S!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (use "finite_add") (("2" (inst - "LAMBDA (s: below(S)): f(s) = x!1" "S!1" "e!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "nonempty_card[below(S)]") (("2" (inst - "{s: below(S) | S!1(s) AND f(s) = x!1}") (("1" (assert) (("1" (skosimp*) (("1" (lemma "nonempty_card[below(S)]") (("1" (inst - "{s: below(S) | (e!1 = s OR S!1(s)) AND f(s) = x!1}") (("1" (assert) (("1" (inst?) (("1" (prop) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (use "finite_add") (("2" (inst - "LAMBDA (s: below(S)): f(s) = x!1" "S!1" "e!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (use "finite_intersect") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 4) (("2" (grind) (("2" (lemma "nonempty_card[below(S)]") (("2" (inst - "{s: below(S) | (e!1 = s OR S!1(s)) AND f(s) = f(e!1)}") (("1" (assert) (("1" (inst?) nil nil)) nil) ("2" (hide-all-but 1) (("2" (use "finite_add") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -2 3) (("2" (expand "filter") (("2" (expand "add") (("2" (expand "member") (("2" (expand "geq") (("2" (case-replace "(LAMBDA (j: below(S)): (e!1 = j OR S!1(j)) AND leq(f(s!1), f(j))) = add(e!1, LAMBDA (j: below(S)): S!1(j) AND leq(f(s!1), f(j)))") (("1" (lemma "card_add[below(S)]") (("1" (inst - "LAMBDA (j: below(S)): S!1(j) AND leq(f(s!1), f(j))" "e!1") (("1" (replace -) (("1" (assert) nil nil)) nil) ("2" (use "finite_intersect") nil nil)) nil)) nil) ("2" (hide 2) (("2" (decompose-equality +) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case-replace "filter(geq)(add(e!1, S!1))(f)(s!1) = filter(geq)(S!1)(f)(s!1)") (("1" (replace -2 :dir rl :hide? t) (("1" (case-replace "bag_to_set(u_filter(make_bag(add(e!1, S!1), f), f(s!1))) = bag_to_set(u_filter(make_bag(S!1, f), f(s!1)))") (("1" (lemma "sum_particular2[T,real,0,+]") (("1" (inst?) (("1" (inst - "f(e!1)") (("1" (replace -1 :hide? t) (("1" (lift-if) (("1" (split) (("1" (flatten) (("1" (case-replace "u_filter(make_bag(add(e!1, S!1), f), f(s!1))(f(e!1)) = 0") (("1" (assert) (("1" (hide -2 -3 -4) (("1" (case-replace "(LAMBDA (t_1: T): IF t_1 = f(e!1) THEN 0 ELSE u_filter(make_bag(add(e!1, S!1), f), f(s!1))(t_1) ENDIF) = LAMBDA (t: T): u_filter(make_bag(S!1, f), f(s!1))(t)") (("1" (hide 2) (("1" (decompose-equality +) (("1" (lift-if) (("1" (split) (("1" (flatten) (("1" (grind) nil nil)) nil) ("2" (flatten) (("2" (expand "u_filter") (("2" (lift-if) (("2" (split) (("1" (flatten) (("1" (expand "make_bag") (("1" (case-replace "{s: below(S) | add(e!1, S!1)(s) AND f(s) = x!1} = {s: below(S) | S!1(s) AND f(s) = x!1}") (("1" (hide 2) (("1" (decompose-equality +) (("1" (iff) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil))