%% 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") ((