$$$requirements.pvs requirements: THEORY BEGIN IMPORTING requirements_aux %inductive in context allslots1_aux allslots1: THEOREM invariant(LAMBDA (s: State): s`pc`Bank = b1 IMPLIES (FORALL (i, j: below(s`reportSize)): i /= j IMPLIES s`bReport(i)`currency /= s`bReport(j)`currency)) %inductive in context allslots2_aux allslots2: THEOREM invariant(LAMBDA (s: State): s`pc`Bank = b1 IMPLIES (FORALL (i: below(pSlotCount)): s`vSlots(i)`inUse IMPLIES (EXISTS (j: below(s`reportSize)): s`bReport(j)`currency = s`vSlots(i)`currency))) END requirements $$$requirements.prf (|requirements| (|allslots1| "" (LEMMA "invariant_rule") (("" (INST?) (("" (SPLIT) (("1" (PROPAX) NIL NIL) ("2" (HIDE 2) (("2" (SKOLEM 1 "r") (("2" (TYPEPRED "r") (("2" (SPLIT) (("1" (HIDE -1) (("1" (GRIND) NIL NIL)) NIL) ("2" (HIDE -2) (("2" (SKOLEM 1 "n") (("2" (TYPEPRED "n") (("2" (FLATTEN) (("2" (SKOLEM 1 ("i" "w")) (("2" (TYPEPRED "i") (("2" (TYPEPRED "w") (("2" (EXPAND "run_fragment") (("2" (INST -6 "n") (("2" (GRIND :IF-MATCH NIL) (("1" (INST-CP -11 "i") (("1" (INST-CP -11 "w") (("1" (INST -4 "i" "w") (("1" (GRIND :IF-MATCH NIL) (("1" (LEMMA "allslots1_aux") (("1" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST-CP -10 "i") (("2" (INST-CP -10 "w") (("2" (LEMMA "allslots1_aux") (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|allslots2| "" (LEMMA "invariant_rule") (("" (INST?) (("" (SPLIT) (("1" (PROPAX) NIL NIL) ("2" (HIDE 2) (("2" (SKOLEM 1 "r") (("2" (TYPEPRED "r") (("2" (SPLIT) (("1" (HIDE -1) (("1" (GRIND) NIL NIL)) NIL) ("2" (HIDE -2) (("2" (SKOLEM 1 "n") (("2" (TYPEPRED "n") (("2" (FLATTEN) (("2" (SKOLEM 1 "w") (("2" (EXPAND "run_fragment") (("2" (INST -4 "n") (("2" (GRIND :IF-MATCH NIL) (("1" (TYPEPRED "w") (("1" (LEMMA "allslots2_aux") (("1" (GRIND) NIL NIL)) NIL)) NIL) ("2" (TYPEPRED "w") (("2" (LEMMA "allslots2_aux") (("2" (EXPAND "invariant") (("2" (INST?) (("2" (GROUND) (("2" (INST -1 "w") (("2" (GROUND) (("2" (SKOLEM -1 "j0") (("2" (TYPEPRED "j0") (("2" (INST -11 "j0") (("2" (INST 2 "j0") (("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)) NIL)) $$$finite_sets/more_finite_sets.pvs more_finite_sets[T1: TYPE+,T2: TYPE]: THEORY BEGIN IMPORTING finite_sets[T1] %the image of a finite set through a function is finite finite_image : LEMMA FORALL (S: finite_set[T1], f: [(S) -> T2]) : is_finite({y: T2 | EXISTS (x :(S)) : y = f(x)}) %the inverse of an injective function (from its range to its domain) is % a bijection. Domain need not be finite. inverse_bijection : LEMMA FORALL (f: [T1 -> T2]) : LET range = {y:T2| EXISTS (x:T1) : y = f(x)} IN LET f_1:[(range) -> T1] = LAMBDA(y : (range)): epsilon({x:T1|y = f(x)}) IN injective?(f) IMPLIES bijective?(f_1) END more_finite_sets $$$finite_sets/more_finite_sets.prf (|more_finite_sets| (|finite_image| "" (SKOLEM 1 ("S" "f")) (("" (TYPEPRED "S") (("" (EXPAND "is_finite") (("" (SKOLEM -1 ("M" "g")) (("" (TYPEPRED "M") (("" (INSTANTIATE 1 ("M" "_")) (("" (INST 1 "LAMBDA (y:{y: T2 | EXISTS (x: (S)): y = f(x)}) : g(epsilon({x:(S) | y = f(x)}))") (("1" (EXPAND "injective?" 1) (("1" (GROUND) (("1" (SKOLEM 1 ("x1" "x2")) (("1" (EXPAND "injective?") (("1" (INSTANTIATE -2 ("epsilon({x: (S) | x1 = f(x)})" "epsilon({x: (S) | x2 = f(x)})")) (("1" (GROUND) (("1" (HIDE -2 -3) (("1" (NAME "y1" "epsilon({x: (S) | x1 = f(x)})") (("1" (NAME "y2" "epsilon({x: (S) | x2 = f(x)})") (("1" (REPLACE -1) (("1" (REPLACE -2) (("1" (CASE "x1 = f(y1)") (("1" (CASE "x2 = f(y2)") (("1" (ASSERT) NIL NIL) ("2" (HIDE -1 -3 -4 2) (("2" (LEMMA "epsilons[(S)].epsilon_ax") (("2" (INST?) (("2" (SPLIT) (("1" (ASSERT) NIL NIL) ("2" (TYPEPRED "x2") (("2" (SKOLEM -1 "x_1444") (("2" (INST 1 "x_1444") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE -1 -3 2) (("2" (LEMMA "epsilons[(S)].epsilon_ax") (("2" (INST?) (("2" (SPLIT) (("1" (GRIND) NIL NIL) ("2" (TYPEPRED "x1") (("2" (SKOLEM -1 "x_1444") (("2" (INST 1 "x_1444") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (TYPEPRED "x1") (("2" (GROUND) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (TYPEPRED "x1") (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOLEM 1 "y") (("2" (TYPEPRED "y") (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|inverse_bijection| "" (SKOLEM 1 "f") (("" (EXPAND "bijective?") (("" (FLATTEN) (("" (SPLIT) (("1" (EXPAND "injective?") (("1" (HIDE -1) (("1" (SKOLEM 1 ("x1" "x2")) (("1" (FLATTEN) (("1" (LEMMA "epsilons[T1].epsilon_ax") (("1" (INST?) (("1" (SPLIT) (("1" (LEMMA "epsilons[T1].epsilon_ax") (("1" (INST -1 "{xx: T1 | x2 = f(xx)}") (("1" (SPLIT) (("1" (ASSERT) NIL NIL) ("2" (TYPEPRED "x2") (("2" (SKOLEM -1 "w") (("2" (INST 1 "w") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (TYPEPRED "x1") (("2" (SKOLEM -1 "w") (("2" (INST 1 "w") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (EXPAND "surjective?") (("2" (SKOLEM 1 "y") (("2" (INST 1 "f(y)") (("1" (LEMMA "epsilons[T1].epsilon_ax") (("1" (INST?) (("1" (SPLIT) (("1" (GROUND) (("1" (GRIND) NIL NIL)) NIL) ("2" (HIDE -1 2) (("2" (INST 1 "y") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST 1 "y") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) $$$finite_sets/finite_sets_eq.pvs finite_sets_eq[T1, T2 : TYPE] : THEORY %------------------------------------------------------------------------- % % by Bruno Dutertre Royal Holloway & Bedford New College % % Equipotence of finite sets % %------------------------------------------------------------------------- BEGIN N: VAR nat IMPORTING finite_sets, func_composition E: VAR finite_set[T1] F: VAR finite_set[T2] S: VAR set[T1] U: VAR set[T2] injection_to_finite_set : LEMMA (EXISTS (f: [(S)->(F)]): injective?(f)) IMPLIES is_finite(S) surjection_from_finite_set : LEMMA (EXISTS (f: [(E)->(U)]): surjective?(f)) IMPLIES is_finite(U) injection_to_finite_set2 : LEMMA (FORALL S, F, (f: [(S)->(F)]): injective?(f) IMPLIES is_finite(S)) surjection_from_finite_set2: LEMMA (FORALL E, U, (f: [(E)->(U)]): surjective?(f) IMPLIES is_finite(U)) bijection_finite_set1 : LEMMA (EXISTS (f: [(S)->(F)]): bijective?(f)) IMPLIES is_finite(S) bijection_finite_set2 : LEMMA (EXISTS (f: [(E)->(U)]): bijective?(f)) IMPLIES is_finite(U) END finite_sets_eq $$$finite_sets/finite_sets_eq.prf (|finite_sets_eq| (|injection_to_finite_set| "" (SKOSIMP*) (("" (NAME "n" "card(F!1)") (("" (REWRITE "card_bij") (("" (EXPAND "bijective?") (("" (SKOSIMP) (("" (EXPAND "is_finite") (("" (INST 1 "n" "f!2 o f!1") (("" (REWRITE "composition_injective") NIL))))))))))))))) (|surjection_from_finite_set| "" (SKOSIMP*) (("" (CASE "empty?(E!1)") (("1" (CASE "U!1 = emptyset[T2]") (("1" (REPLACE -1) (("1" (REWRITE "finite_emptyset") NIL))) ("2" (REWRITE "emptyset_is_empty?" :DIR RL) (("2" (DELETE 2) (("2" (GRIND) NIL))))))) ("2" (ASSERT) (("2" (NAME "g" "inverse(f!1)") (("1" (TYPEPRED "E!1") (("1" (EXPAND "is_finite") (("1" (SKOLEM!) (("1" (INST 2 "N!1" "f!2 o g") (("1" (REWRITE "composition_injective") (("1" (REPLACE -2 1 RL) (("1" (REWRITE "inj_inv") NIL))))))))))))) ("2" (DELETE -1 3) (("2" (GRIND) (("2" (INST + "x!1") NIL))))))))))))) (|injection_to_finite_set2| "" (SKOSIMP) (("" (USE "injection_to_finite_set" ("F" "F!1")) (("" (ASSERT) (("" (INST?) NIL))))))) (|surjection_from_finite_set2| "" (SKOSIMP) (("" (USE "surjection_from_finite_set" ("E" "E!1")) (("" (ASSERT) (("" (INST?) NIL))))))) (|bijection_finite_set1| "" (EXPAND "bijective?") (("" (SKOSIMP*) (("" (LEMMA "injection_to_finite_set" ("S" "S!1" "F" "F!1")) (("" (ASSERT) (("" (INST?) NIL))))))))) (|bijection_finite_set2| "" (EXPAND "bijective?") (("" (SKOSIMP*) (("" (LEMMA "surjection_from_finite_set" ("E" "E!1" "U" "U!1")) (("" (ASSERT) (("" (INST?) NIL)))))))))) $$$finite_sets/func_composition.pvs func_composition [ T1, T2, T3 : TYPE ] : THEORY %------------------------------------------------------------------------ % Author: Bruno Dutertre % % Composition of injective, surjective, bijective functions %------------------------------------------------------------------------ BEGIN f1 : VAR [T1 -> T2] f2 : VAR [T2 -> T3] composition_injective : LEMMA injective?(f1) AND injective?(f2) IMPLIES injective?(f2 o f1) composition_surjective: LEMMA surjective?(f1) AND surjective?(f2) IMPLIES surjective?(f2 o f1) composition_bijective : LEMMA bijective?(f1) AND bijective?(f2) IMPLIES bijective?(f2 o f1) % ---------------- Cancellation laws ---------------- f, g : VAR [T1 -> T2] h, k : VAR [T2 -> T3] composition_def : LEMMA (FORALL (x : T1) : h(f(x)) = (h o f)(x)) composition_left_cancel1 : LEMMA injective?(h) IMPLIES (h o f = h o g IFF f = g) composition_left_cancel2 : LEMMA bijective?(h) IMPLIES (h o f = h o g IFF f = g) composition_right_cancel1: LEMMA surjective?(f) IMPLIES (h o f = k o f IFF h = k) composition_right_cancel2: LEMMA bijective?(f) IMPLIES (h o f = k o f IFF h = k) END func_composition $$$finite_sets/func_composition.prf (|func_composition| (|composition_injective| "" (GRIND :IF-MATCH NIL) (("" (INST -2 "f1!1(x1!1)" "f1!1(x2!1)") (("" (INST -1 "x1!1" "x2!1") (("" (GROUND) NIL))))))) (|composition_surjective| "" (GRIND) NIL) (|composition_bijective| "" (EXPAND "bijective?") (("" (SKOSIMP) (("" (SPLIT) (("1" (REWRITE "composition_injective") NIL) ("2" (REWRITE "composition_surjective") NIL))))))) (|composition_def| "" (EXPAND "o") (("" (PROPAX) NIL))) (|composition_left_cancel1| "" (SKOSIMP) (("" (PROP) (("1" (APPLY-EXTENSIONALITY :HIDE? T) (("1" (EXPAND "injective?") (("1" (INST? -2) (("1" (ASSERT) (("1" (REWRITE "composition_def") (("1" (REWRITE "composition_def") (("1" (ASSERT) NIL))))))))))))) ("2" (ASSERT) NIL))))) (|composition_left_cancel2| "" (EXPAND "bijective?") (("" (SKOSIMP) (("" (REWRITE "composition_left_cancel1") NIL))))) (|composition_right_cancel1| "" (SKOSIMP) (("" (PROP) (("1" (APPLY-EXTENSIONALITY :HIDE? T) (("1" (EXPAND "surjective?") (("1" (INST?) (("1" (SKOLEM!) (("1" (REPLACE -2 + RL) (("1" (REWRITE "composition_def") (("1" (REWRITE "composition_def") (("1" (ASSERT) NIL))))))))))))))) ("2" (ASSERT) NIL))))) (|composition_right_cancel2| "" (EXPAND "bijective?") (("" (SKOSIMP) (("" (REWRITE "composition_right_cancel1") NIL)))))) $$$finite_sets/finite_sets_card_eq.pvs finite_sets_card_eq[T1, T2 : TYPE] : THEORY %------------------------------------------------------------------------- % % by Bruno Dutertre Royal Holloway & Bedford New College % % Establishes: % % card_eq_bij : LEMMA card(E) = card(F) IFF % EXISTS (f: [(E)->(F)]): bijective?(f) % %------------------------------------------------------------------------- BEGIN IMPORTING finite_sets, func_composition E: VAR finite_set[T1] F: VAR finite_set[T2] N: VAR nat card_injection : LEMMA (EXISTS (f : [(E)->below[N]]) : injective?(f)) IMPLIES card(E) <= N card_surjection : LEMMA (EXISTS (f : [(E)->below[N]]) : surjective?(f)) IMPLIES N <= card(E) injection_and_cardinal : LEMMA (EXISTS (f : [(E)->(F)]): injective?(f)) IMPLIES card(E) <= card(F) surjection_and_cardinal: LEMMA (EXISTS (f: [(E)->(F)]): surjective?(f)) IMPLIES card(F) <= card(E) card_eq_bij : LEMMA card(E) = card(F) IFF EXISTS (f: [(E)->(F)]): bijective?(f) END finite_sets_card_eq $$$finite_sets/finite_sets_card_eq.prf (|finite_sets_card_eq| (|card_injection| "" (SKOSIMP*) (("" (REWRITE "card_def") (("" (REWRITE "Card_injection") (("" (INST?) NIL))))))) (|card_surjection| "" (SKOSIMP*) (("" (REWRITE "card_def") (("" (REWRITE "Card_surjection") (("" (INST?) NIL))))))) (|injection_and_cardinal| "" (SKOSIMP*) (("" (NAME-REPLACE "n" "card(F!1)" :HIDE? NIL) (("" (REWRITE "card_bij") (("" (EXPAND "bijective?") (("" (SKOSIMP) (("" (REWRITE "card_injection") (("" (INST 1 "f!2 o f!1") (("" (REWRITE "composition_injective") NIL))))))))))))))) (|surjection_and_cardinal| "" (SKOSIMP*) (("" (NAME-REPLACE "n" "card(F!1)" :HIDE? NIL) (("" (REWRITE "card_bij") (("" (EXPAND "bijective?") (("" (SKOSIMP) (("" (REWRITE "card_surjection") (("" (INST 1 "f!2 o f!1") (("" (REWRITE "composition_surjective") NIL))))))))))))))) (|card_eq_bij| "" (SKOSIMP*) (("" (USE "empty_card[T2]") (("" (GROUND) (("1" (REPLACE -3) (("1" (REWRITE "empty_card[T1]" :DIR RL) (("1" (DELETE -3) (("1" (INST 1 "LAMBDA (x : (E!1)) : epsilon! (y : (F!1)) : true") (("1" (GRIND :IF-MATCH NIL) (("1" (INST?) NIL) ("2" (INST?) NIL))) ("2" (DELETE -2) (("2" (GRIND) NIL))))))))))) ("2" (REPLACE -3) (("2" (REWRITE "empty_card[T1]" :DIR RL) (("2" (SKOLEM!) (("2" (DELETE -1 -3) (("2" (GRIND :IF-MATCH NIL) (("2" (INST - "f!1(x!1)") (("2" (ASSERT) NIL))))))))))))) ("3" (DELETE 2) (("3" (NAME-REPLACE "n" "card(F!1)" :HIDE? NIL) (("3" (REWRITE "card_bij") (("3" (REWRITE "card_bij") (("3" (SKOSIMP*) (("3" (INST 1 "inverse(f!1) o f!2") (("1" (REWRITE "composition_bijective") (("1" (REWRITE "bij_inv_is_bij") (("1" (DELETE -1 -2 2 3) (("1" (GRIND) NIL))))) ("2" (DELETE -) (("2" (EXPAND "empty?") (("2" (SKOSIMP*) (("2" (EXPAND "member") (("2" (INST + "x!1") NIL))))))))))) ("2" (EXPAND "empty?") (("2" (EXPAND "member") (("2" (SKOSIMP*) (("2" (INST + "x!1") NIL))))))))))))))))))) ("4" (NAME-REPLACE "n" "card(F!1)" :HIDE? NIL) (("4" (DELETE 2) (("4" (REWRITE "card_bij") (("4" (REWRITE "card_bij") (("4" (SKOSIMP*) (("4" (INST 1 "f!1 o f!2") (("4" (REWRITE "composition_bijective") NIL)))))))))))))))))))) $$$finite_sets/finite_sets_below.pvs finite_sets_below[N: nat]: THEORY BEGIN IMPORTING finite_sets A,B,BS: VAR set[below(N)] US: VAR set[upto(N)] finite_below : LEMMA is_finite[below(N)](BS) card_below_fullset: LEMMA card[below(N)](fullset[below(N)]) = N card_below : LEMMA card[below(N)](BS) <= N finite_upto : LEMMA is_finite[upto(N)](US) card_upto_fullset : LEMMA card[upto(N)](fullset[upto(N)]) = N + 1 card_upto : LEMMA card[upto(N)](US) <= N + 1 k: VAR nat pidgeon_hole : LEMMA card(A) + card(B) >= N + k IMPLIES card(intersection(A,B)) >= k END finite_sets_below $$$finite_sets/finite_sets_below.prf (|finite_sets_below| (|finite_below| "" (SKOSIMP*) (("" (EXPAND "is_finite") (("" (INST 1 "N" "(LAMBDA (i:(BS!1)): i)") (("" (EXPAND "injective?") (("" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|card_below_fullset_TCC1| "" (REWRITE "finite_below") NIL NIL) (|card_below_fullset| "" (EXPAND "fullset") (("" (LEMMA "card_bij[below(N)]") (("" (INST -1 "N" "{x: below(N) | TRUE}") (("1" (REPLACE -1) (("1" (HIDE -1) (("1" (INST 1 "(LAMBDA (x: {x: below(N) | TRUE}): x)") (("1" (EXPAND "bijective?") (("1" (PROP) (("1" (EXPAND "injective?") (("1" (PROPAX) NIL NIL)) NIL) ("2" (EXPAND "surjective?") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (REWRITE "finite_below") NIL NIL)) NIL)) NIL)) NIL) (|card_below_TCC1| "" (SKOSIMP*) (("" (REWRITE "finite_below") NIL NIL)) NIL) (|card_below| "" (SKOSIMP*) (("" (LEMMA "card_subset[below(N)]") (("" (INST -1 "BS!1" "fullset[below(N)]") (("1" (LEMMA "card_below_fullset") (("1" (REPLACE -1) (("1" (HIDE -1) (("1" (ASSERT) (("1" (HIDE 2) (("1" (EXPAND "subset?") (("1" (EXPAND "fullset") (("1" (EXPAND "member") (("1" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (REWRITE "finite_below") NIL NIL) ("3" (REWRITE "finite_below") NIL NIL)) NIL)) NIL)) NIL) (|finite_upto| "" (SKOSIMP*) (("" (EXPAND "is_finite") (("" (INST 1 "N+1" "(LAMBDA (i:(US!1)): i)") (("" (EXPAND "injective?") (("" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|card_upto_fullset_TCC1| "" (REWRITE "finite_upto") NIL NIL) (|card_upto_fullset| "" (EXPAND "fullset") (("" (LEMMA "card_bij[upto(N)]") (("" (INST -1 "N+1" "{x: upto(N) | TRUE}") (("1" (REPLACE -1) (("1" (HIDE -1) (("1" (INST 1 "(LAMBDA (x: {x: upto(N) | TRUE}): x)") (("1" (EXPAND "bijective?") (("1" (PROP) (("1" (EXPAND "injective?") (("1" (PROPAX) NIL NIL)) NIL) ("2" (EXPAND "surjective?") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (REWRITE "finite_upto") NIL NIL)) NIL)) NIL)) NIL) (|card_upto_TCC1| "" (SKOSIMP*) (("" (REWRITE "finite_upto") NIL NIL)) NIL) (|card_upto| "" (SKOSIMP*) (("" (LEMMA "card_subset[upto(N)]") (("" (INST -1 "US!1" "fullset[upto(N)]") (("1" (LEMMA "card_upto_fullset") (("1" (REPLACE -1) (("1" (HIDE -1) (("1" (ASSERT) (("1" (HIDE 2) (("1" (EXPAND "subset?") (("1" (EXPAND "fullset") (("1" (EXPAND "member") (("1" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (REWRITE "finite_upto") NIL NIL) ("3" (REWRITE "finite_upto") NIL NIL)) NIL)) NIL)) NIL) (|pidgeon_hole_TCC1| "" (SKOSIMP*) (("" (REWRITE "finite_intersection") (("1" (REWRITE "finite_below") NIL NIL) ("2" (REWRITE "finite_below") NIL NIL)) NIL)) NIL) (|pidgeon_hole| "" (SKOSIMP*) (("" (LEMMA "card_union[below(N)]") (("" (INST?) (("1" (LEMMA "card_below") (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (REWRITE "finite_below") NIL NIL) ("3" (REWRITE "finite_below") NIL NIL)) NIL)) NIL)) NIL)) $$$finite_sets/finite_sets_pred.pvs finite_sets_pred[T: TYPE]: THEORY BEGIN IMPORTING finite_sets P, P1, P2: VAR pred[T] finite_pred: LEMMA is_finite(fullset[T]) IMPLIES is_finite[T]({x: T | P(x)}) card_implies: LEMMA is_finite(fullset[T]) AND (FORALL (x: T): P1(x) IMPLIES P2(x)) IMPLIES card({x: T | P1(x)}) <= card({x: T | P2(x)}) END finite_sets_pred $$$finite_sets/finite_sets_pred.prf (|finite_sets_pred| (|finite_pred| "" (EXPAND "fullset") (("" (EXPAND "is_finite") (("" (SKOSIMP*) (("" (INST 1 "N!1" "(LAMBDA (x: {x: T | P!1(x)}): f!1(x))") (("" (EXPAND "injective?") (("" (SKOSIMP*) (("" (INST?) (("" (ASSERT) NIL))))))))))))))) (|card_implies_TCC1| "" (SKOSIMP*) (("" (REWRITE "finite_pred") NIL))) (|card_implies_TCC2| "" (SKOSIMP*) (("" (REWRITE "finite_pred") NIL))) (|card_implies| "" (SKOSIMP*) (("" (CASE "subset?({x: T | P1!1(x)},{x: T | P2!1(x)})") (("1" (LEMMA "card_subset[T]") (("1" (INST?) (("1" (ASSERT) NIL) ("2" (HIDE -1 -3 2) (("2" (REWRITE "finite_pred") NIL))) ("3" (REWRITE "finite_pred") NIL))))) ("2" (HIDE -1 2) (("2" (EXPAND "subset?") (("2" (EXPAND "member") (("2" (PROPAX) NIL)))))))))))) $$$finite_sets/finite_sets_nat.pvs finite_sets_nat: THEORY BEGIN IMPORTING finite_sets[nat] n, N: VAR nat i, j: VAR nat p: VAR pred[nat] finite_bounded : LEMMA is_finite({j: nat | j < N }) card_bounded : LEMMA card({j: nat | j < N}) = N finite_bounded_subset: LEMMA is_finite({j: nat | j < N AND p(j)}) card_bounded_subset : LEMMA card({j: nat | j < N AND p(j)}) <= N % ------------------------------------------------------------------------ % The following lemmas apply is_finite[nat] and card[nat] to subtype % sets. This should be avoided if possible. See finite_subint for % preferred lemmas. % ------------------------------------------------------------------------ finite_nat_below : LEMMA is_finite[nat]({x: below(n) | TRUE}) card_nat_below : LEMMA card[nat]({x: below(n) | TRUE}) = n finite_nat_upto : LEMMA is_finite[nat]({x: upto(n) | TRUE}) card_nat_upto : LEMMA card[nat]({x: upto(n) | TRUE}) = n + 1 finite_nat_subrange: LEMMA is_finite[nat](restrict[int, nat, bool]({x: subrange(i, j) | TRUE})) card_nat_subrange : LEMMA card[nat](restrict[int, nat, bool]({x: subrange(i, j) | TRUE})) = IF i <= j THEN j - i + 1 ELSE 0 ENDIF END finite_sets_nat $$$finite_sets/finite_sets_nat.prf (|finite_sets_nat| (|finite_bounded| "" (SKOSIMP*) (("" (EXPAND "is_finite") (("" (INST 1 "N!1" "(lambda (x: below(N!1)): x)") (("" (EXPAND "injective?") (("" (SKOSIMP*) NIL))))))))) (|card_bounded_TCC1| "" (SKOSIMP*) (("" (ASSERT) (("" (EXPAND "is_finite") (("" (INST 1 "N!1" "(lambda (x: below(N!1)): x)") (("" (EXPAND "injective?") (("" (SKOSIMP*) NIL))))))))))) (|card_bounded| "" (SKOSIMP*) (("" (REWRITE "card_bij") (("1" (INST 1 "(lambda (x:below(N!1)):x)") (("1" (EXPAND "bijective?") (("1" (SPLIT 1) (("1" (EXPAND "injective?") (("1" (SKOSIMP*) NIL))) ("2" (EXPAND "surjective?") (("2" (SKOSIMP*) (("2" (INST 1 "y!1") NIL))))))))))) ("2" (REWRITE "finite_bounded") NIL))))) (|finite_bounded_subset| "" (SKOSIMP*) (("" (LEMMA "finite_subset") (("" (INST -1 "{j: nat | j < N!1}" "{j: nat | j < N!1 AND p!1(j)}") (("1" (ASSERT) (("1" (HIDE 2) (("1" (EXPAND "subset?") (("1" (EXPAND "member") (("1" (SKOSIMP*) NIL))))))))) ("2" (REWRITE "finite_bounded") NIL))))))) (|card_bounded_subset_TCC1| "" (SKOSIMP*) (("" (LEMMA "finite_bounded_subset") (("" (INST?) NIL))))) (|card_bounded_subset| "" (SKOSIMP*) (("" (LEMMA "card_bounded") (("" (INST -1 "N!1") (("" (LEMMA "card_subset") (("" (INST -1 "{j: nat | j < N!1 AND p!1(j)}" "{j: nat | j < N!1}") (("1" (SPLIT -1) (("1" (ASSERT) NIL) ("2" (HIDE -1 2) (("2" (EXPAND "subset?") (("2" (SKOSIMP*) (("2" (EXPAND "member") (("2" (ASSERT) NIL))))))))))) ("2" (REWRITE "finite_bounded") NIL) ("3" (REWRITE "finite_bounded_subset") NIL))))))))))) (|finite_nat_below| "" (SKOSIMP*) (("" (EXPAND "is_finite") (("" (INST 1 "n!1" "(LAMBDA (x: (extend[nat, below(n!1), bool, FALSE]({x: below(n!1) | TRUE}))): x)") (("1" (EXPAND "injective?") (("1" (SKOSIMP*) NIL))) ("2" (SKOSIMP*) (("2" (ASSERT) (("2" (TYPEPRED "x!1") (("2" (EXPAND "extend") (("2" (PROPAX) NIL))))))))))))))) (|card_nat_below_TCC1| "" (SKOSIMP*) (("" (LEMMA "finite_nat_below") (("" (INST?) NIL))))) (|card_nat_below| "" (SKOSIMP*) (("" (LEMMA "card_bij") (("" (INST -1 "n!1" "extend[nat, below(n!1), bool, FALSE]({x: below(n!1) | TRUE})") (("1" (REPLACE -1) (("1" (HIDE -1) (("1" (INST 1 "(LAMBDA (x: (extend[nat, below(n!1), bool, FALSE]({x: below(n!1) | TRUE}))): x)") (("1" (EXPAND "bijective?") (("1" (PROP) (("1" (EXPAND "injective?") (("1" (SKOSIMP*) NIL))) ("2" (EXPAND "surjective?") (("2" (SKOSIMP*) (("2" (INST 1 "y!1") (("2" (EXPAND "extend") (("2" (PROPAX) NIL))))))))))))) ("2" (SKOSIMP*) (("2" (TYPEPRED "x!1") (("2" (EXPAND "extend") (("2" (ASSERT) NIL))))))))))))) ("2" (LEMMA "finite_nat_below") (("2" (INST?) NIL))))))))) (|finite_nat_upto| "" (SKOSIMP*) (("" (EXPAND "is_finite") (("" (INST 1 "n!1+1" "(LAMBDA (x: (extend[nat, upto(n!1), bool, FALSE]({x: upto(n!1) | TRUE}))): x)") (("1" (EXPAND "injective?") (("1" (SKOSIMP*) NIL))) ("2" (SKOSIMP*) (("2" (TYPEPRED "x!1") (("2" (EXPAND "extend") (("2" (ASSERT) NIL))))))))))))) (|card_nat_upto_TCC1| "" (SKOSIMP*) (("" (LEMMA "finite_nat_upto") (("" (INST?) NIL))))) (|card_nat_upto| "" (SKOSIMP*) (("" (LEMMA "card_bij") (("" (INST -1 "n!1+1" "extend[nat, upto(n!1), bool, FALSE]({x: upto(n!1) | TRUE})") (("1" (REPLACE -1) (("1" (HIDE -1) (("1" (INST 1 "(LAMBDA (x: {x: upto(n!1) | TRUE}): x)") (("1" (EXPAND "bijective?") (("1" (PROP) (("1" (EXPAND "injective?") (("1" (SKOSIMP*) NIL))) ("2" (EXPAND "surjective?") (("2" (SKOSIMP*) (("2" (INST 1 "y!1") (("2" (EXPAND "extend") (("2" (PROPAX) NIL))))))))))))) ("2" (SKOSIMP*) (("2" (PROP) (("1" (EXPAND "extend") (("1" (ASSERT) NIL))) ("2" (EXPAND "extend") (("2" (ASSERT) NIL))))))) ("3" (SKOSIMP*) (("3" (EXPAND "extend") (("3" (PROPAX) NIL))))))))))) ("2" (LEMMA "finite_nat_upto") (("2" (INST?) NIL))))))))) (|finite_nat_subrange| "" (SKOSIMP*) (("" (EXPAND "is_finite") (("" (INST 1 "j!1+1" "(LAMBDA (x: (restrict[int, nat, bool](extend[int, subrange(i!1, j!1), bool, FALSE]({x: subrange(i!1, j!1) | TRUE})))): x)") (("1" (EXPAND "injective?") (("1" (SKOSIMP*) NIL))) ("2" (SKOSIMP*) (("2" (ASSERT) (("2" (TYPEPRED "x!1") (("2" (EXPAND "restrict") (("2" (EXPAND "extend") (("2" (PROPAX) NIL))))))))))))))))) (|card_nat_subrange_TCC1| "" (SKOSIMP*) (("" (LEMMA "finite_nat_subrange") (("" (INST?) NIL))))) (|card_nat_subrange| "" (SKOSIMP*) (("" (LEMMA "card_bij") (("" (INST?) (("1" (REPLACE -1) (("1" (HIDE -1) (("1" (INST 1 "(LAMBDA (x: (restrict[int, nat, bool](extend[int, subrange(i!1, j!1), bool, FALSE]({x: subrange(i!1, j!1) | TRUE})))): IF i!1 <= j!1 THEN x-i!1 ELSE 0 ENDIF)") (("1" (EXPAND "bijective?") (("1" (PROP) (("1" (EXPAND "injective?") (("1" (SKOSIMP*) (("1" (TYPEPRED "x1!1") (("1" (TYPEPRED "x2!1") (("1" (GRIND) NIL))))))))) ("2" (EXPAND "surjective?") (("2" (SKOSIMP*) (("2" (INST 1 "y!1+i!1") (("1" (TYPEPRED "y!1") (("1" (GRIND) NIL))) ("2" (TYPEPRED "y!1") (("2" (GRIND) NIL))))))))))))) ("2" (SKOSIMP*) (("2" (TYPEPRED "x!1") (("2" (GRIND) NIL))))) ("3" (SKOSIMP*) (("3" (TYPEPRED "x!1") (("3" (GRIND) NIL))))))))))) ("2" (HIDE 2) (("2" (REWRITE "finite_nat_subrange") NIL))) ("3" (HIDE 2) (("3" (FLATTEN) (("3" (ASSERT) NIL)))))))))))) $$$finite_sets/finite_sets_int.pvs finite_sets_int: THEORY BEGIN IMPORTING finite_sets[int] i, j, x: VAR int p: VAR pred[int] in_subrng(x,i,j): bool = (i <= x) AND (x <= j) finite_subrng : LEMMA is_finite({x | in_subrng(x,i,j)}) finite_subrng_subset: LEMMA is_finite({x | in_subrng(x,i,j) AND p(x)}) card_subrng : LEMMA card({x | in_subrng(x,i,j)}) = IF i <= j THEN abs(j-i+1) ELSE 0 ENDIF % ------------------------------------------------------------------------ % The following lemmas apply is_finite[nat] and card[nat] to subtype % sets. This should be avoided if possible. See finite_subint for % preferred lemmas. % ------------------------------------------------------------------------ finite_int_subrange : LEMMA is_finite[int]({x: subrange(i, j) | TRUE}) finite_int_subrange_pred: LEMMA is_finite[int]({x: subrange(i, j) | p(x)}) card_int_subrange : LEMMA card[int]({x: subrange(i, j) | TRUE}) = IF i <= j THEN abs(j-i+1) ELSE 0 ENDIF END finite_sets_int $$$finite_sets/finite_sets_int.prf (|finite_sets_int| (|finite_subrng| "" (SKOSIMP*) (("" (EXPAND "in_subrng") (("" (EXPAND "is_finite") (("" (INST 1 "abs(j!1-i!1+1)" "(LAMBDA (x: {x: int | i!1 <= x AND x <= j!1}): x - i!1)") (("1" (GRIND) NIL NIL) ("2" (SKOSIMP*) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|finite_subrng_subset| "" (SKOSIMP*) (("" (CASE "subset?({x: int | in_subrng(x, i!1, j!1) AND p!1(x)},{x: int | in_subrng(x, i!1, j!1)})") (("1" (LEMMA "finite_subset") (("1" (INST?) (("1" (ASSERT) NIL NIL) ("2" (HIDE -1 2) (("2" (REWRITE "finite_subrng") NIL NIL)) NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (EXPAND "subset?") (("2" (EXPAND "member") (("2" (SKOSIMP*) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|card_subrng_TCC1| "" (SKOSIMP*) (("" (REWRITE "finite_subrng") NIL NIL)) NIL) (|card_subrng| "" (SKOSIMP*) (("" (CASE "i!1 > j!1") (("1" (ASSERT) (("1" (CASE "{x: int | in_subrng(x, i!1, j!1)} = emptyset") (("1" (REPLACE -1) (("1" (HIDE -1) (("1" (LEMMA "card_emptyset") (("1" (PROPAX) NIL NIL)) NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (APPLY-EXTENSIONALITY 1 :HIDE? T) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) (("2" (LEMMA "card_bij") (("2" (INST -1 "abs(j!1-i!1+1)" "{x | in_subrng(x, i!1, j!1)}") (("1" (REPLACE -1) (("1" (HIDE -1) (("1" (INST 2 "(LAMBDA (x: {x | in_subrng(x, i!1, j!1)}): abs(x -i!1))") (("1" (EXPAND "bijective?") (("1" (PROP) (("1" (EXPAND "injective?") (("1" (SKOSIMP*) (("1" (TYPEPRED "x1!1") (("1" (TYPEPRED "x2!1") (("1" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (EXPAND "surjective?") (("2" (SKOSIMP*) (("2" (TYPEPRED "y!1") (("2" (INST 1 "y!1+i!1") (("1" (GRIND) NIL NIL) ("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (TYPEPRED "x!1") (("2" (EXPAND "in_subrng") (("2" (FLATTEN) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE 2 3) (("2" (REWRITE "finite_subrng") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|finite_int_subrange| "" (SKOSIMP*) (("" (EXPAND "is_finite") (("" (INST 1 "abs(j!1-i!1+1)" "(LAMBDA (x: (extend[int, subrange(i!1, j!1), bool, FALSE]({x: subrange(i!1, j!1) | TRUE}))): x - i!1)") (("1" (EXPAND "injective?") (("1" (SKOSIMP*) NIL NIL)) NIL) ("2" (SKOSIMP*) (("2" (EXPAND "abs") (("2" (GROUND) (("1" (TYPEPRED "x!1") (("1" (EXPAND "extend") (("1" (PROPAX) NIL NIL)) NIL)) NIL) ("2" (LIFT-IF) (("2" (GROUND) (("1" (TYPEPRED "x!1") (("1" (EXPAND "extend") (("1" (PROPAX) NIL NIL)) NIL)) NIL) ("2" (TYPEPRED "x!1") (("2" (EXPAND "extend") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|finite_int_subrange_pred| "" (SKOSIMP*) (("" (CASE "is_finite({x: subrange(i!1, j!1) | TRUE})") (("1" (LEMMA "finite_subset") (("1" (INST -1 "{x: subrange(i!1, j!1) | TRUE}" "{x: subrange(i!1, j!1) | p!1(x)}") (("1" (ASSERT) (("1" (HIDE -1 2) (("1" (EXPAND "subset?") (("1" (SKOSIMP*) (("1" (EXPAND "member") (("1" (EXPAND "extend") (("1" (PROP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (EXPAND "is_finite") (("2" (SKOSIMP) (("2" (INST 1 "N!1" "LAMBDA (x: (extend[int, subrange(i!1, j!1), bool, FALSE] ({x: subrange(i!1, j!1) | TRUE}))): IF i!1 <= x and x <= j!1 then f!1(x) ELSE 0 ENDIF") (("1" (GRIND :IF-MATCH NIL) (("1" (INST -6 "x1!1" "x2!1") (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (ASSERT) (("2" (TYPEPRED "x!1") (("2" (EXPAND "extend") (("2" (ASSERT) (("2" (REPLACE 1) (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (SKOSIMP*) (("3" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (LEMMA "finite_int_subrange") (("2" (INST?) (("2" (EXPAND "is_finite") (("2" (SKOSIMP*) (("2" (INST 1 "N!1" "lambda (x: ({x: subrange(i!1, j!1) | TRUE})): f!1(x)") (("1" (GRIND :IF-MATCH NIL) (("1" (INST -5 "x1!1" "x2!1") (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|card_int_subrange_TCC1| "" (SKOSIMP*) (("" (REWRITE "finite_int_subrange") NIL NIL)) NIL) (|card_int_subrange| "" (SKOSIMP*) (("" (CASE "i!1 > j!1") (("1" (ASSERT) (("1" (CASE "extend[int, subrange(i!1, j!1), bool, FALSE]({x: subrange(i!1, j!1) | TRUE}) = emptyset") (("1" (REPLACE -1) (("1" (HIDE -1) (("1" (LEMMA "card_emptyset") (("1" (PROPAX) NIL NIL)) NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (EXPAND "extend") (("2" (APPLY-EXTENSIONALITY) (("2" (LIFT-IF) (("2" (HIDE 2) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) (("2" (LEMMA "card_bij") (("2" (INST -1 "abs(j!1-i!1+1)" "extend[int, subrange(i!1, j!1), bool, FALSE]({x: subrange(i!1, j!1) | TRUE})") (("1" (REPLACE -1) (("1" (HIDE -1) (("1" (INST 2 "(LAMBDA (x: (extend[int, subrange(i!1, j!1), bool, FALSE]({x: subrange(i!1, j!1) | TRUE}))): abs(x -i!1))") (("1" (EXPAND "bijective?") (("1" (PROP) (("1" (EXPAND "injective?") (("1" (SKOSIMP*) (("1" (TYPEPRED "x1!1") (("1" (TYPEPRED "x2!1") (("1" (EXPAND "extend") (("1" (EXPAND "abs") (("1" (PROP) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (EXPAND "surjective?") (("2" (SKOSIMP*) (("2" (INST 1 "y!1+i!1") (("1" (EXPAND "abs") (("1" (PROPAX) NIL NIL)) NIL) ("2" (EXPAND "extend") (("2" (ASSERT) (("2" (PROP) (("2" (TYPEPRED "y!1") (("2" (EXPAND "abs") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (EXPAND "abs") (("2" (TYPEPRED "x!1") (("2" (EXPAND "extend") (("2" (PROP) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (REWRITE "finite_int_subrange") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) $$$finite_sets/prelude_aux.pvs prelude_aux[T: TYPE]: THEORY BEGIN % these lemmas should go in prelude rest_emptyset: LEMMA (FORALL (S: set[T], t:T): rest(S) = emptyset[T] AND S(t) IMPLIES choose(S) = t) END prelude_aux $$$finite_sets/prelude_aux.prf (|prelude_aux| (|rest_emptyset_TCC1| "" (SUBTYPE-TCC) NIL) (|rest_emptyset| "" (SKOSIMP*) (("" (LEMMA "rest_empty_lem[T]") (("" (INST?) (("" (ASSERT) (("" (SPLIT -1) (("1" (EXPAND "singleton") (("1" (EXPAND "extend") (("1" (REPLACE -1) (("1" (HIDE -1) (("1" (HIDE -1) (("1" (ASSERT) NIL))))))))))) ("2" (ASSERT) (("2" (EXPAND "empty?") (("2" (EXPAND "member") (("2" (INST?) NIL))))))) ("3" (REWRITE "emptyset_is_empty?[T]") NIL)))))))))))) $$$finite_sets/finite_sets_sum_real.pvs finite_sets_sum_real[T: TYPE]: THEORY %------------------------------------------------------------------------ % % finite sum over real-valued functions % % Authors: Ricky W. Butler % David Griffioen % % NOTES: % -- there are several theorems which are virtually idential to % theorems in finite_sets_sum. They are repeated here to prevent % the need for commands such as (LEMMA sum_emptyset[T,real,0,+]) % -- the theorems with names ending in "_rew" are especially useful % for rewriting. Some of these take advantage of the fact that % since we have real-valued functions we have a "-" available. %------------------------------------------------------------------------ BEGIN IMPORTING finite_sets_sum[T,real,0,+], prelude_aux S, A, B: VAR finite_set[T] t: VAR T c,N: VAR real f,g: VAR function[T -> real] sum_const : THEOREM sum(S, (LAMBDA t: c)) = c*card(S) sum_1_is_card : COROLLARY sum(S,(LAMBDA t: 1)) = card(S) sum_mult : THEOREM sum(S,(LAMBDA t: c*f(t))) = c*sum(S,f) % ----------- Some rewrite rules using "-" ------------------ sum_empty? : THEOREM empty?(S) IMPLIES sum(S,f) = 0 sum_emptyset_rew : THEOREM S = emptyset[T] IMPLIES sum(S,f) = 0 sum_singleton_rew: THEOREM card(S) = 1 AND S(t) IMPLIES sum(S,f) = f(t) sum_remove_rew : THEOREM sum(remove(t,S),f) = sum(S,f) - IF member(t,S) THEN f(t) ELSE 0 ENDIF sum_rest_rew : THEOREM NOT empty?(S) IMPLIES sum(rest(S),f) = sum(S,f) - f(choose(S)) sum_union_rew : THEOREM sum(union(A,B),f) = sum(A,f) + sum(B,f) - sum(intersection(A,B),f) % -------- sums of slightly modified functions ---------- sum_eq_funs : THEOREM (FORALL (t: (S)): f(t) = g(t)) IMPLIES sum(S, f) = sum(S, g) sum_particular_gen: THEOREM sum(S,f) = sum(S, f WITH [t := c]) + IF S(t) THEN f(t) - c ELSE 0 ENDIF % ----- some order relationships involving sum ----- sum_bound : THEOREM (FORALL (t: (S)): f(t) <= N) IMPLIES sum(S,f) <= N*card(S) sum_order : THEOREM (FORALL (t:T): f(t) <= g(t)) IMPLIES sum(S,f) <= sum(S,g) sum_nonneg : LEMMA (FORALL (t: (S)): f(t) >= 0) IMPLIES sum(S,f) >= 0 sum_pos : LEMMA (FORALL (t: (S)): f(t) > 0) IMPLIES sum(S,f) > 0 OR S = emptyset[T] JUDGEMENT sum(A: non_empty_finite_set[T], f: [T -> posreal]) HAS_TYPE posreal JUDGEMENT sum(A: finite_set[T], f: [T -> int]) HAS_TYPE int JUDGEMENT sum(A: finite_set[T], f: [T -> nat]) HAS_TYPE nat % ----- Special properties non-negative valued functions ----- fnr,gnr: VAR [T -> nonneg_real] sum_subset : THEOREM subset?(A,B) IMPLIES sum(A,fnr) <= sum(B,fnr) sum_order_sub: THEOREM subset?(A,B) AND (FORALL (t:T): fnr(t) <= gnr(t)) IMPLIES sum(A,fnr) <= sum(B,gnr) gn: VAR function[T -> nat] gi: VAR function[T -> nonneg_int] sum_0_nat : THEOREM sum(S,gn) = 0 IMPLIES S = emptyset[T] OR (FORALL (t:(S)): gn(t) = 0) sum_is_null : COROLLARY sum(S,gn) = 0 => (S(t) => gn(t) = 0) sum_0_int : THEOREM sum(S,gi) = 0 IMPLIES S = emptyset[T] OR (FORALL (t:(S)): gi(t) = 0) sum_0_non_neg : THEOREM sum(S,f) = 0 AND (FORALL (t: (S)): f(t) >= 0) IMPLIES S = emptyset[T] OR (FORALL (t:(S)): f(t) = 0) JUDGEMENT sum(A: finite_set[T], f: [T -> nonneg_real]) HAS_TYPE nonneg_real JUDGEMENT sum(A: finite_set[T], f: [T -> nonneg_int]) HAS_TYPE nonneg_int JUDGEMENT sum(A: non_empty_finite_set[T], f: [T->posnat]) HAS_TYPE posnat % JUDGEMENT sum(A: non_empty_finite_set[T], f: [T->negreal]) HAS_TYPE negreal % JUDGEMENT sum(A: finite_set[T], f: [T -> nonpos_real]) HAS_TYPE nonpos_real % JUDGEMENT sum(A: finite_set[T], f: [T -> negint]) HAS_TYPE negint END finite_sets_sum_real $$$finite_sets/finite_sets_sum_real.prf (|finite_sets_sum_real| (|IMP_finite_sets_sum_TCC1| "" (TCC :DEFS !) NIL NIL) (|IMP_finite_sets_sum_TCC2| "" (TCC :DEFS !) NIL NIL) (|sum_const| "" (INDUCT "S" 1 "finite_set_induction_rest") (("1" (SKOSIMP*) (("1" (REWRITE "sum_emptyset") (("1" (LEMMA "card_emptyset") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (EXPAND "sum" 1) (("2" (INST?) (("2" (REPLACE -1) (("2" (HIDE -1) (("2" (LEMMA "card_rest") (("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sum_1_is_card| "" (LEMMA "sum_const") (("" (SKOSIMP*) (("" (INST -1 "S!1" "1") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|sum_mult| "" (INDUCT "S" 1 "finite_set_induction_rest") (("1" (SKOSIMP*) (("1" (LEMMA "sum_emptyset") (("1" (INST?) (("1" (REPLACE -1) (("1" (HIDE -1) (("1" (LEMMA "sum_emptyset") (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (EXPAND "sum" 1) (("2" (INST?) (("2" (REPLACE -1) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sum_empty?| "" (SKOSIMP*) (("" (REWRITE "emptyset_is_empty?[T]") (("" (LEMMA "sum_emptyset[T,real,0,+]") (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|sum_emptyset_rew| "" (SKOSIMP*) (("" (LEMMA "sum_emptyset[T,real,0,+]") (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|sum_singleton_rew| "" (SKOSIMP*) (("" (REWRITE "card_one") (("" (SKOSIMP*) (("" (REPLACE -1) (("" (REWRITE "sum_singleton[T,real,0,+]") (("" (HIDE -1) (("" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sum_remove_rew| "" (SKOSIMP*) (("" (LEMMA "sum_remove[T,real,0,+]") (("" (INST?) (("" (REPLACE -1 + RL) (("" (HIDE -1) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sum_rest_rew_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|sum_rest_rew| "" (SKOSIMP*) (("" (LEMMA "sum_rest") (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|sum_union_rew| "" (SKOSIMP*) (("" (LEMMA "sum_union") (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|sum_eq_funs| "" (SKOSIMP*) (("" (REWRITE "sum_f_g") NIL NIL)) NIL) (|sum_particular_gen| "" (AUTO-REWRITE "member") (("" (INDUCT "S" 1 "finite_set_induction_rest[T]") (("1" (SKOSIMP*) (("1" (REWRITE "sum_emptyset") (("1" (REWRITE "sum_emptyset") (("1" (EXPAND "emptyset") (("1" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (EXPAND "sum" 1) (("2" (LIFT-IF) (("2" (SPLIT 1) (("1" (FLATTEN) (("1" (INST?) (("1" (ASSERT) (("1" (REPLACE -2 :HIDE? T) (("1" (CASE "rest(SS!1)(t!1)") (("1" (EXPAND "rest") (("1" (REPLACE -2 * RL) (("1" (EXPAND "remove") (("1" (PROPAX) NIL NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (FLATTEN) (("2" (INST?) (("2" (CASE " SS!1(t!1)") (("1" (ASSERT) (("1" (REPLACE -2 :HIDE? T) (("1" (EXPAND "rest") (("1" (EXPAND "remove") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (REPLACE -1 :HIDE? T) (("2" (EXPAND "rest") (("2" (EXPAND "remove") (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sum_bound| "" (INDUCT "S" 1 "finite_set_induction_rest") (("1" (SKOSIMP*) (("1" (REWRITE "sum_emptyset") (("1" (REWRITE "card_emptyset") (("1" (HIDE -1) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (EXPAND "sum" 1) (("2" (INST -1 "N!1" "f!1") (("2" (SPLIT -1) (("1" (INST -2 "choose(SS!1)") (("1" (REWRITE "card_rest") (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (SKOSIMP*) (("2" (INST -1 "t!1") (("2" (TYPEPRED "t!1") (("2" (GRIND :EXCLUDE "choose") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sum_order| "" (INDUCT-AND-SIMPLIFY "S" 1 "finite_set_induction_rest" :EXCLUDE ("rest" "choose")) NIL NIL) (|sum_nonneg| "" (INDUCT "S" 1 "finite_set_induction_rest") (("1" (SKOSIMP*) (("1" (REWRITE "sum_emptyset") (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (EXPAND "sum" 1) (("2" (INST?) (("2" (SPLIT -1) (("1" (INST -2 "choose(SS!1)") (("1" (ASSERT) NIL NIL)) NIL) ("2" (HIDE 2) (("2" (SKOSIMP*) (("2" (INST?) (("2" (TYPEPRED "t!1") (("2" (LEMMA "rest_member[T]") (("2" (EXPAND "member") (("2" (INST -1 "SS!1" "t!1") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sum_pos| "" (INDUCT "S" 1 "finite_set_induction_rest") (("1" (SKOSIMP*) NIL NIL) ("2" (SKOSIMP*) (("2" (EXPAND "sum" 1) (("2" (INST?) (("2" (SPLIT -1) (("1" (INST -2 "choose(SS!1)") (("1" (ASSERT) NIL NIL)) NIL) ("2" (HIDE 2) (("2" (REPLACE -1) (("2" (HIDE -1) (("2" (REWRITE "sum_emptyset") (("2" (ASSERT) (("2" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (HIDE 2) (("3" (SKOSIMP*) (("3" (INST?) (("3" (TYPEPRED "t!1") (("3" (LEMMA "rest_member[T]") (("3" (EXPAND "member") (("3" (INST -1 "SS!1" "t!1") (("3" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sum_TCC1| "" (AUTO-REWRITE-THEORY "rationals") (("" (AUTO-REWRITE-THEORY "integers") (("" (INDUCT "A" 1 "finite_set_induction_rest") (("1" (TYPEPRED "A!1") (("1" (PROPAX) NIL NIL)) NIL) ("2" (SKOSIMP*) (("2" (HIDE 2) (("2" (LEMMA "emptyset_is_empty?[T]") (("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("3" (SKOSIMP*) (("3" (ASSERT) (("3" (SPLIT -1) (("1" (INST?) (("1" (FLATTEN) (("1" (ASSERT) (("1" (EXPAND "sum" 2) (("1" (ASSERT) (("1" (TYPEPRED "f!1(choose(SS!1))") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (EXPAND "sum" 2) (("2" (TYPEPRED "f!1(choose(SS!1))") (("2" (CASE "rest(SS!1) = emptyset") (("1" (REPLACE -1) (("1" (HIDE -1) (("1" (REWRITE "sum_emptyset") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (HIDE -1 -2 2 3) (("2" (LEMMA "emptyset_is_empty?[T]") (("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sum_TCC2| "" (AUTO-REWRITE-THEORY "rationals") (("" (AUTO-REWRITE-THEORY "integers") (("" (INDUCT-AND-SIMPLIFY "x1" 1 "finite_set_induction_rest") (("" (INDUCT-AND-SIMPLIFY "A" 1 "finite_set_induction_rest") NIL NIL)) NIL)) NIL)) NIL) (|sum_TCC3| "" (SKOSIMP*) (("" (LEMMA "sum_nonneg") (("" (INST?) (("" (ASSERT) (("" (SKOSIMP*) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sum_subset| "" (SKOSIMP*) (("" (CASE "B!1 = union(A!1,difference(B!1,A!1))") (("1" (REPLACE -1 +) (("1" (HIDE -1) (("1" (LEMMA "sum_union") (("1" (INST?) (("1" (CASE "sum(intersection(A!1, difference(B!1, A!1)), fnr!1) = 0") (("1" (REPLACE -1) (("1" (HIDE -1) (("1" (ASSERT) (("1" (REPLACE -1) (("1" (HIDE -1) (("1" (LEMMA "sum_nonneg") (("1" (INST -1 "difference(B!1, A!1)" "fnr!1") (("1" (ASSERT) (("1" (HIDE -1) (("1" (SKOSIMP*) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE -1 2) (("2" (CASE "intersection(A!1, difference(B!1, A!1)) = emptyset") (("1" (REPLACE -1) (("1" (HIDE -1) (("1" (REWRITE "sum_emptyset") NIL NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (APPLY-EXTENSIONALITY 1 :HIDE? T) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (APPLY-EXTENSIONALITY 1 :HIDE? T) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|sum_order_sub| "" (SKOSIMP*) (("" (LEMMA "sum_subset") (("" (INST?) (("" (INST -1 "B!1") (("" (ASSERT) (("" (LEMMA "sum_order") (("" (INST -1 "B!1" "fnr!1" "gnr!1") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sum_0_nat| "" (INDUCT "S" 1 "finite_set_induction_rest") (("1" (SKOSIMP*) NIL NIL) ("2" (SKOSIMP*) (("2" (EXPAND "sum" -2) (("2" (INST?) (("2" (TYPEPRED "sum(rest(SS!1), gn!1)") (("2" (ASSERT) (("2" (TYPEPRED "t!1") (("2" (SPLIT -3) (("1" (ASSERT) (("1" (LEMMA "rest_emptyset[T]") (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (LEMMA "choose_rest_or[T]") (("2" (INST?) (("2" (EXPAND "member") (("2" (INST?) (("2" (ASSERT) (("2" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sum_is_null| "" (SKOSIMP*) (("" (LEMMA "sum_0_nat") (("" (INST?) (("" (ASSERT) (("" (SPLIT -1) (("1" (HIDE -2 1) (("1" (REWRITE "emptyset_is_empty?[T]" :DIR RL) (("1" (EXPAND "empty?") (("1" (EXPAND "member") (("1" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sum_0_int| "" (INDUCT "S" 1 "finite_set_induction_rest") (("1" (SKOSIMP*) NIL NIL) ("2" (SKOSIMP*) (("2" (EXPAND "sum" -2) (("2" (INST?) (("2" (TYPEPRED "sum(rest(SS!1), gi!1)") (("2" (ASSERT) (("2" (TYPEPRED "t!1") (("2" (SPLIT -3) (("1" (LEMMA "rest_emptyset[T]") (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (LEMMA "choose_rest_or[T]") (("2" (INST?) (("2" (EXPAND "member") (("2" (INST?) (("2" (ASSERT) (("2" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sum_0_non_neg| "" (INDUCT "S" 1 "finite_set_induction_rest") (("1" (SKOSIMP*) NIL NIL) ("2" (SKOSIMP*) (("2" (EXPAND "sum" -2) (("2" (INST?) (("2" (LEMMA "sum_nonneg") (("2" (INST?) (("2" (CASE "(FORALL (t: (rest(SS!1))): f!1(t) >= 0)") (("1" (REPLACE -1) (("1" (ASSERT) (("1" (CASE "f!1(choose(SS!1)) = 0") (("1" (REPLACE -1) (("1" (HIDE -1) (("1" (ASSERT) (("1" (SPLIT -3) (("1" (CASE "t!1 = choose(SS!1)") (("1" (REVEAL -1) (("1" (ASSERT) NIL NIL)) NIL) ("2" (HIDE -2 -3 -4 -5 3) (("2" (LEMMA "rest_emptyset[T]") (("2" (INST?) (("2" (INST -1 "t!1") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (LEMMA "choose_rest_or[T]") (("2" (EXPAND "member") (("2" (INST?) (("2" (INST -1 "t!1") (("2" (ASSERT) (("2" (INST -2 "t!1") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) (("2" (INST -5 "choose(SS!1)") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE -1 -2 -3 3) (("2" (SKOSIMP*) (("2" (INST -1 "t!2") (("2" (TYPEPRED "t!2") (("2" (LEMMA "rest_member[T]") (("2" (INST?) (("2" (EXPAND "member") (("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sum_TCC4| "" (LEMMA "sum_nonneg") (("" (SKOSIMP*) (("" (INST?) (("" (ASSERT) (("" (HIDE 2) (("" (SKOSIMP*) (("" (TYPEPRED "f!1(t!1)") (("" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sum_TCC5| "" (SUBTYPE-TCC) NIL NIL)) $$$finite_sets/finite_sets_minmax.pvs finite_sets_minmax[T: TYPE, <= : (total_order?[T])]: THEORY BEGIN IMPORTING finite_sets_inductions[T] %, sets_aux[T] min(x,y:T): T = IF x <= y THEN x ELSE y ENDIF max(x,y:T): T = IF x <= y THEN y ELSE x ENDIF a,x,y: VAR T SS: VAR non_empty_finite_set minrec(SS): RECURSIVE T = IF empty?(rest(SS)) THEN choose(SS) ELSE min(choose(SS),minrec(rest(SS))) ENDIF MEASURE (LAMBDA SS: card(SS)) maxrec(SS): RECURSIVE T = IF empty?(rest(SS)) THEN choose(SS) ELSE max(choose(SS),maxrec(rest(SS))) ENDIF MEASURE (LAMBDA SS: card(SS)) lt_reflexive: LEMMA FORALL (x: T): <=(x, x) lt_transitive: LEMMA FORALL (x,y,z:T): <=(x, y) & <=(y, z) => <=(x, z) lt_total: LEMMA FORALL (x,y:T) : x <= y OR y <= x lt_antisymmetric: LEMMA FORALL (x,y: T): <=(x, y) & <=(y, x) => x = y min(SS): {a: T | SS(a) AND (FORALL (x: T): SS(x) IMPLIES a <= x)} max(SS): {a: T | SS(a) AND (FORALL (x: T): SS(x) IMPLIES x <= a)} min_lem: LEMMA (min(SS) = a IFF SS(a) AND (FORALL (x: (SS)): a <= x)) max_lem: LEMMA (max(SS) = a IFF SS(a) AND (FORALL (x: (SS)): x <= a)) A,B: VAR non_empty_finite_set min_union: LEMMA min(A) = x AND min(B) = y IMPLIES min(union(A,B)) = min(x,y) max_union: LEMMA max(A) = x AND max(B) = y IMPLIES max(union(A,B)) = max(x,y) END finite_sets_minmax $$$finite_sets/finite_sets_minmax.prf (|finite_sets_minmax| (|minrec_TCC1| "" (SKOSIMP*) (("" (REWRITE "card_rest") (("" (ASSERT) NIL))))) (|lt_reflexive| "" (SKOSIMP*) (("" (TYPEPRED "finite_sets_minmax.<=") (("" (EXPAND "total_order?") (("" (EXPAND "partial_order?") (("" (FLATTEN) (("" (HIDE -2 3) (("" (EXPAND "preorder?") (("" (FLATTEN) (("" (EXPAND "reflexive?") (("" (INST?) NIL))))))))))))))))))) (|lt_transitive| "" (SKOSIMP*) (("" (TYPEPRED "finite_sets_minmax.<=") (("" (EXPAND "total_order?") (("" (EXPAND "partial_order?") (("" (FLATTEN) (("" (HIDE -2 3) (("" (EXPAND "preorder?") (("" (FLATTEN) (("" (HIDE -1 -3) (("" (EXPAND "transitive?") (("" (INST -1 "x!1" "y!1" "z!1") (("" (ASSERT) NIL))))))))))))))))))))))) (|lt_total| "" (SKOSIMP*) (("" (TYPEPRED "finite_sets_minmax.<=") (("" (EXPAND "total_order?") (("" (EXPAND "partial_order?") (("" (FLATTEN) (("" (HIDE -1 -2) (("" (EXPAND "dichotomous?") (("" (INST?) (("" (ASSERT) NIL))))))))))))))))) (|lt_antisymmetric| "" (SKOSIMP*) (("" (TYPEPRED "finite_sets_minmax.<=") (("" (EXPAND "total_order?") (("" (EXPAND "partial_order?") (("" (FLATTEN) (("" (HIDE -1 -3) (("" (EXPAND "antisymmetric?") (("" (INST?) (("" (ASSERT) NIL))))))))))))))))) (|min_TCC1| "" (INST 1 "(LAMBDA SS: minrec(SS))") (("" (INDUCT "SS" 1 "finite_set_induction_rest") (("1" (TYPEPRED "SS!1") (("1" (PROPAX) NIL))) ("2" (TYPEPRED "SS!1") (("2" (PROPAX) NIL))) ("3" (ASSERT) (("3" (AUTO-REWRITE-THEORY "sets[T]") (("3" (ASSERT) NIL))))) ("4" (SKOSIMP*) (("4" (EXPAND "minrec" +) (("4" (SPLIT 2) (("1" (ASSERT) NIL) ("2" (FLATTEN) (("2" (AUTO-REWRITE-THEORY "sets[T]") (("2" (ASSERT) (("2" (SKOSIMP*) (("2" (EXPAND "min") (("2" (ASSERT) (("2" (SPLIT) (("1" (FLATTEN) (("1" (LEMMA "epsilon_ax[T]") (("1" (INST?) (("1" (ASSERT) (("1" (INST 1 "x!1") NIL))))))))) ("2" (ASSERT) NIL))))))))))))))) ("3" (SKOSIMP*) (("3" (LIFT-IF) (("3" (SPLIT 1) (("1" (HIDE -2) (("1" (FLATTEN) (("1" (LEMMA "choose_rest_or[T]") (("1" (INST?) (("1" (EXPAND "member") (("1" (INST?) (("1" (ASSERT) (("1" (SPLIT -1) (("1" (EXPAND "empty?") (("1" (INST?) (("1" (EXPAND "member") (("1" (PROPAX) NIL))))))) ("2" (REPLACE -1) (("2" (HIDE -1) (("2" (REWRITE "lt_reflexive") NIL))))))))))))))))))))) ("2" (FLATTEN) (("2" (ASSERT) (("2" (FLATTEN) (("2" (EXPAND "min") (("2" (LIFT-IF) (("2" (ASSERT) (("2" (GROUND) (("1" (LEMMA "choose_rest_or[T]") (("1" (EXPAND "member") (("1" (INST -1 "SS!1" "x!1") (("1" (ASSERT) (("1" (SPLIT -1) (("1" (INST -5 "x!1") (("1" (ASSERT) (("1" (HIDE -1 -3 -4 2 3) (("1" (LEMMA "lt_transitive") (("1" (INST -1 "choose(SS!1)" " minrec(rest(SS!1))" "x!1") (("1" (ASSERT) NIL))))))))))) ("2" (REPLACE -1) (("2" (HIDE -1) (("2" (HIDE -1 -2 -3 -4) (("2" (REWRITE "lt_reflexive") NIL))))))))))))))))) ("2" (INST -3 "x!1") (("2" (SPLIT -3) (("1" (PROPAX) NIL) ("2" (CASE-REPLACE "x!1 = choose(SS!1)") (("1" (HIDE -1 -2 -3 1 4 5) (("1" (LEMMA "lt_total") (("1" (INST?) (("1" (GROUND) NIL))))))) ("2" (HIDE 3 4 5 6) (("2" (LEMMA "choose_rest_or[T]") (("2" (INST?) (("2" (EXPAND "member") (("2" (GROUND) NIL))))))))))))))))))))))))))))))))))))))))))))) (|max_TCC1| "" (INST 1 "(LAMBDA SS: maxrec(SS))") (("" (INDUCT "SS" 1 "finite_set_induction_rest") (("1" (TYPEPRED "SS!1") (("1" (PROPAX) NIL))) ("2" (TYPEPRED "SS!1") (("2" (PROPAX) NIL))) ("3" (ASSERT) (("3" (AUTO-REWRITE-THEORY "sets[T]") (("3" (ASSERT) NIL))))) ("4" (SKOSIMP*) (("4" (EXPAND "maxrec" +) (("4" (SPLIT 2) (("1" (ASSERT) NIL) ("2" (FLATTEN) (("2" (AUTO-REWRITE-THEORY "sets[T]") (("2" (ASSERT) (("2" (SKOSIMP*) (("2" (EXPAND "max") (("2" (ASSERT) (("2" (SPLIT 2) (("1" (ASSERT) NIL) ("2" (FLATTEN) (("2" (LEMMA "epsilon_ax[T]") (("2" (INST?) (("2" (ASSERT) (("2" (INST 1 "x!1") NIL))))))))))))))))))))))) ("3" (SKOSIMP*) (("3" (LIFT-IF) (("3" (SPLIT 1) (("1" (HIDE -2) (("1" (FLATTEN) (("1" (CASE-REPLACE "x!1=choose(SS!1)") (("1" (REWRITE "lt_reflexive") NIL) ("2" (HIDE 2) (("2" (LEMMA "choose_rest_or[T]") (("2" (EXPAND "member") (("2" (INST?) (("2" (ASSERT) (("2" (EXPAND "empty?") (("2" (EXPAND "member") (("2" (INST?) NIL))))))))))))))))))))) ("2" (FLATTEN) (("2" (ASSERT) (("2" (FLATTEN) (("2" (EXPAND "max") (("2" (LIFT-IF) (("2" (ASSERT) (("2" (PROP) (("1" (HIDE -4) (("1" (LEMMA "choose_rest_or[T]") (("1" (EXPAND "member") (("1" (INST -1 "SS!1" "x!1") (("1" (ASSERT) (("1" (REVEAL -2) (("1" (INST -1 "x!1") (("1" (ASSERT) NIL))))))))))))))) ("2" (ASSERT) (("2" (INST -3 "x!1") (("2" (SPLIT -3) (("1" (HIDE -2 -3 3 4) (("1" (LEMMA "lt_total") (("1" (INST -1 "maxrec(rest(SS!1))" "choose(SS!1) ") (("1" (PROP) (("1" (LEMMA "lt_transitive") (("1" (INST -1 "x!1" "maxrec(rest(SS!1))" "choose(SS!1)") (("1" (ASSERT) NIL))))))))))))) ("2" (LEMMA "choose_rest_or[T]") (("2" (EXPAND "member") (("2" (INST?) (("2" (ASSERT) (("2" (REPLACE -1) (("2" (HIDE -1) (("2" (REWRITE "lt_reflexive") NIL))))))))))))))))))))))))))))))))))))))))))))))))) (|min_lem| "" (SKOSIMP*) (("" (TYPEPRED "min(SS!1)") (("" (PROP) (("1" (ASSERT) NIL) ("2" (SKOSIMP*) (("2" (REPLACE -1) (("2" (HIDE -1) (("2" (TYPEPRED "x!1") (("2" (INST?) (("2" (ASSERT) NIL))))))))))) ("3" (INST -4 "a!1") (("3" (ASSERT) (("3" (INST -2 "min(SS!1)") (("3" (ASSERT) (("3" (HIDE -1 -3) (("3" (REWRITE "lt_antisymmetric") NIL))))))))))))))))) (|max_lem| "" (SKOSIMP*) (("" (TYPEPRED "max(SS!1)") (("" (PROP) (("1" (ASSERT) NIL) ("2" (SKOSIMP*) (("2" (REPLACE -1) (("2" (HIDE -1) (("2" (TYPEPRED "x!1") (("2" (INST?) (("2" (ASSERT) NIL))))))))))) ("3" (INST -4 "a!1") (("3" (ASSERT) (("3" (INST -2 "max(SS!1)") (("3" (ASSERT) (("3" (HIDE -1 -3) (("3" (REWRITE "lt_antisymmetric") NIL))))))))))))))))) (|min_union| "" (SKOSIMP*) (("" (AUTO-REWRITE "member" "union") (("" (LEMMA "min_lem") (("" (INST-CP -1 "A!1" "x!1") (("" (INST -1 "B!1" "y!1") (("" (ASSERT) (("" (LEMMA "min_lem") (("" (INST -1 "union(A!1,B!1)" "min(x!1, y!1)") (("" (FLATTEN) (("" (HIDE -1) (("" (ASSERT) (("" (HIDE 2) (("" (SPLIT 1) (("1" (FLATTEN) (("1" (EXPAND "min") (("1" (CASE "x!1 <= y!1") (("1" (ASSERT) NIL) ("2" (ASSERT) NIL))))))) ("2" (SKOSIMP*) (("2" (TYPEPRED "x!2") (("2" (EXPAND "union") (("2" (EXPAND "min") (("2" (EXPAND "member") (("2" (LIFT-IF) (("2" (SPLIT 1) (("1" (FLATTEN) (("1" (SPLIT -2) (("1" (INST -4 "x!2") NIL) ("2" (INST -3 "x!2") (("2" (HIDE -1 -4 -5 -6) (("2" (LEMMA "lt_transitive") (("2" (INST -1 "x!1" "y!1" "x!2") (("2" (ASSERT) NIL))))))))))))) ("2" (FLATTEN) (("2" (SPLIT -1) (("1" (INST -3 "x!2") (("1" (ASSERT) (("1" (HIDE -1 -2 -4 -5) (("1" (LEMMA "lt_transitive") (("1" (INST -1 "x!1" "x!2" "y!1") (("1" (ASSERT) (("1" (HIDE -1 2) (("1" (LEMMA "lt_total") (("1" (INST?) (("1" (ASSERT) NIL))))))))))))))))))) ("2" (INST -2 "x!2") NIL))))))))))))))))))))))))))))))))))))))))))))) (|max_union| "" (SKOSIMP*) (("" (AUTO-REWRITE "member" "union") (("" (LEMMA "max_lem") (("" (INST-CP -1 "A!1" "x!1") (("" (INST -1 "B!1" "y!1") (("" (ASSERT) (("" (LEMMA "max_lem") (("" (INST -1 "union(A!1,B!1)" "max(x!1, y!1)") (("" (FLATTEN) (("" (HIDE -1) (("" (ASSERT) (("" (HIDE 2) (("" (SPLIT 1) (("1" (FLATTEN) (("1" (EXPAND "max") (("1" (CASE "x!1 <= y!1") (("1" (ASSERT) NIL) ("2" (ASSERT) NIL))))))) ("2" (SKOSIMP*) (("2" (TYPEPRED "x!2") (("2" (EXPAND "union") (("2" (EXPAND "max") (("2" (EXPAND "member") (("2" (LIFT-IF) (("2" (SPLIT 1) (("1" (FLATTEN) (("1" (SPLIT -2) (("1" (INST -4 "x!2") (("1" (HIDE -1 -3 -5 -6) (("1" (LEMMA "lt_transitive") (("1" (INST -1 "x!2" "x!1" "y!1") (("1" (ASSERT) NIL))))))))) ("2" (INST -3 "x!2") NIL))))) ("2" (FLATTEN) (("2" (SPLIT -1) (("1" (INST -3 "x!2") NIL) ("2" (INST -2 "x!2") (("2" (HIDE -1 -3 -4 -5) (("2" (LEMMA "lt_transitive") (("2" (INST -1 "x!2" "y!1" "x!1") (("2" (ASSERT) (("2" (HIDE -1 3) (("2" (LEMMA "lt_total") (("2" (INST?) (("2" (ASSERT) NIL)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) $$$finite_sets/finite_sets_inductions.pvs finite_sets_inductions[T: TYPE]: THEORY BEGIN IMPORTING finite_sets[T] S, S1, S2 : VAR finite_set SS,U : VAR non_empty_finite_set e : VAR T P : VAR pred[finite_set] Q : VAR pred[non_empty_finite_set] n : VAR nat cardinal_induction : LEMMA (FORALL S : P(S)) IFF (FORALL n, S : card(S) = n IMPLIES P(S)) finite_set_induction : THEOREM P(emptyset[T]) AND (FORALL e,S: P(S) IMPLIES P(add(e,S))) IMPLIES (FORALL S: P(S)) finite_set_ind_modified : THEOREM P(emptyset[T]) AND (FORALL e,S: NOT S(e) AND P(S) IMPLIES P(add(e,S))) IMPLIES (FORALL S: P(S)) finite_set_induction_rest: THEOREM P(emptyset[T]) AND (FORALL SS : P(rest(SS)) IMPLIES P(SS)) IMPLIES (FORALL S : P(S)) finite_set_induction_union: THEOREM P(emptyset[T]) AND (FORALL e: P(singleton(e))) AND (FORALL S1,S2: P(S1) AND P(S2) IMPLIES P(union(S1,S2))) IMPLIES (FORALL S: P(S)) finite_set_induction_gen: THEOREM (FORALL S: (FORALL S2: card(S2) < card(S) IMPLIES P(S2)) IMPLIES P(S)) IMPLIES (FORALL S: P(S)) % -------- Induction rules for non empty sets ---------------- nonempty_card_induction : LEMMA (FORALL U : Q(U)) IFF (FORALL S, n : n > 0 AND card(S) = n IMPLIES Q(S)) nonempty_finite_set_induct : THEOREM (FORALL e : Q(singleton(e))) AND (FORALL e, U : Q(U) AND NOT U(e) IMPLIES Q(add(e, U))) IMPLIES (FORALL U : Q(U)) END finite_sets_inductions $$$finite_sets/finite_sets_inductions.prf (|finite_sets_inductions| (|cardinal_induction| "" (GRIND :DEFS NIL) NIL NIL) (|finite_set_induction| "" (SKOSIMP) (("" (CASE "(FORALL n, S: card(S) = n IMPLIES P!1(S))") (("1" (ASSERT) NIL NIL) ("2" (HIDE 2) (("2" (INDUCT "n") (("1" (SKOSIMP) (("1" (REWRITE "empty_card" :DIR RL) (("1" (REWRITE "emptyset_is_empty?") (("1" (EXPAND "emptyset") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (USE "nonempty_card") (("2" (ASSERT) (("2" (REWRITE "nonempty_member") (("2" (SKOLEM!) (("2" (INST -2 "remove(x!1, S!1)") (("2" (INST -5 "x!1" "remove(x!1, S!1)") (("2" (AUTO-REWRITE "card_remove" "add_remove_member") (("2" (ASSERT) (("2" (EXPAND "member") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|finite_set_ind_modified| "" (SKOSIMP*) (("" (LEMMA "finite_set_induction") (("" (INST?) (("" (SPLIT -1) (("1" (INST -1 "S!1") NIL NIL) ("2" (PROPAX) NIL NIL) ("3" (SKOSIMP*) (("3" (INST -3 "e!1" "S!2") (("3" (ASSERT) (("3" (CASE-REPLACE "add(e!1, S!2) = S!2") (("3" (APPLY-EXTENSIONALITY 1 :HIDE? T) (("3" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|finite_set_induction_rest| "" (SKOSIMP) (("" (CASE "(FORALL n, S: card(S) = n IMPLIES P!1(S))") (("1" (ASSERT) NIL NIL) ("2" (HIDE 2) (("2" (INDUCT "n") (("1" (SKOSIMP*) (("1" (HIDE -3) (("1" (CASE-REPLACE "S!1 = emptyset") (("1" (REWRITE "card_empty?") (("1" (REWRITE "emptyset_is_empty?") NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (AUTO-REWRITE "card_rest" "nonempty?") (("2" (SKOSIMP*) (("2" (USE "nonempty_card") (("2" (ASSERT) (("2" (INST? -4) (("2" (INST -1 "rest(S!1)") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|finite_set_induction_union| "" (SKOSIMP) (("" (REWRITE "finite_set_induction") (("" (SKOSIMP) (("" (INST? -3) (("" (AUTO-REWRITE "add_as_union" "singleton") (("" (INST -4 "S!1" "singleton(e!1)") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|finite_set_induction_gen| "" (SKOSIMP) (("" (CASE "(FORALL n, S: card(S) = n IMPLIES P!1(S))") (("1" (ASSERT) NIL NIL) ("2" (HIDE 2) (("2" (INDUCT "n" 1 "NAT_induction") (("2" (SKOSIMP*) (("2" (INST -3 "S!1") (("2" (SPLIT -3) (("1" (PROPAX) NIL NIL) ("2" (SKOSIMP*) (("2" (INST -2 "card(S2!1)") (("2" (ASSERT) (("2" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|nonempty_card_induction_TCC1| "" (SKOSIMP) (("" (REWRITE "empty_card") (("" (ASSERT) NIL NIL)) NIL)) NIL) (|nonempty_card_induction| "" (SKOLEM!) (("" (PROP) (("1" (SKOSIMP) (("1" (INST? -1) (("1" (REWRITE "empty_card") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP :PREDS? T) (("2" (REWRITE "empty_card") (("2" (INST -2 "U!1" "card(U!1)") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|nonempty_finite_set_induct| "" (SKOSIMP*) (("" (CASE "FORALL S : empty?(S) OR Q!1(S)") (("1" (INST? -1) (("1" (ASSERT) NIL NIL)) NIL) ("2" (AUTO-REWRITE "emptyset_is_empty?[T]" "Emptyset" "Singleton" "singleton_as_add") (("2" (REWRITE "finite_set_ind_modified") (("2" (HIDE 2 3) (("2" (SKOSIMP*) (("2" (SPLIT -1) (("1" (ASSERT) (("1" (INST? -2) (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (GROUND) (("2" (INST?) (("2" (INST?) (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) $$$finite_sets/finite_sets_sum.pvs finite_sets_sum[T, R: TYPE, zero:R, +:[R,R -> R] ]: THEORY %---------------------------------------------------------------------- % % ---- % \ % sum(S: finite_set[T], f:[T->R]) = zero + f(i) % / % ---- % member(i,S) % %---------------------------------------------------------------------- BEGIN ASSUMING r,r1,r2,r3 : VAR R zero_identity: ASSUMPTION identity?(+)(zero) plus_ac: ASSUMPTION associative?(+) AND commutative?(+) ENDASSUMING plus_zero_right: LEMMA r + zero = r plus_zero_left : LEMMA zero + r = r plus_assoc : LEMMA (r1 + r2) + r3 = r1 + (r2 + r3) plus_comm : LEMMA r1 + r2 = r2 + r1 IMPORTING finite_sets[T], finite_sets_inductions[T], sets_lemmas[T] f,g: VAR [T -> R] S, A, B: VAR finite_set x: VAR T sum(S,f) : RECURSIVE R = IF (empty?(S)) THEN zero ELSE f(choose(S)) + sum(rest(S),f) ENDIF MEASURE (LAMBDA S,f: card(S)) sum_emptyset : THEOREM sum(emptyset[T],f) = zero sum_singleton : THEOREM sum(singleton(x),f) = f(x) + zero ; sum_x : THEOREM (FORALL (x: (S)): sum(S, f) = f(x) + sum(remove(x, S), f)) sum_x1_x2 : LEMMA (FORALL (x1,x2: (S)): f(x1) + sum(remove(x1,S),f) = f(x2) + sum(remove(x2,S),f)) sum_add : THEOREM sum(add(x,S),f) = sum(S,f) + IF member(x,S) THEN zero ELSE f(x) ENDIF sum_remove : THEOREM sum(remove(x,S),f) + IF member(x,S) THEN f(x) ELSE zero ENDIF = sum(S,f) sum_rest : THEOREM NOT empty?(S) IMPLIES f(choose(S)) + sum(rest(S),f) = sum(S,f) sum_disj_union: THEOREM disjoint?(A,B) IMPLIES sum(union(A,B),f) = sum(A,f) + sum(B,f) sum_diff_subset: THEOREM subset?(A, B) IMPLIES sum(difference(B, A), f) + sum(A, f) = sum(B, f) sum_union : THEOREM sum(union(A,B),f) + sum(intersection(A,B),f) = sum(A,f) + sum(B,f) sum_diff_intersection: THEOREM sum(A,f) = sum(difference(A,B),f) + sum(intersection(A,B),f) sum_f_g : LEMMA (FORALL (x: (S)): f(x) = g(x)) IMPLIES sum(S, f) = sum(S, g) sum_particular : THEOREM sum(S,f) = sum(S, f WITH [x := zero]) + IF S(x) THEN f(x) ELSE zero ENDIF sum_distributive: THEOREM sum(A,f) + sum(A,g) = sum(A,(LAMBDA x: f(x) + g(x))) END finite_sets_sum $$$finite_sets/finite_sets_sum.prf (|finite_sets_sum| (|plus_zero_right| "" (SKOSIMP*) (("" (LEMMA "zero_identity") (("" (EXPAND "identity?") (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|plus_zero_left| "" (SKOSIMP*) (("" (LEMMA "zero_identity") (("" (EXPAND "identity?") (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|plus_assoc| "" (LEMMA "plus_ac") (("" (FLATTEN) (("" (EXPAND "associative?") (("" (PROPAX) NIL NIL)) NIL)) NIL)) NIL) (|plus_comm| "" (LEMMA "plus_ac") (("" (FLATTEN) (("" (EXPAND "commutative?") (("" (PROPAX) NIL NIL)) NIL)) NIL)) NIL) (|sum_TCC1| "" (GRIND) NIL NIL) (|sum_TCC2| "" (SKOSIMP*) (("" (REWRITE "card_rest") (("" (ASSERT) NIL NIL)) NIL)) NIL) (|sum_emptyset| "" (GRIND) NIL NIL) (|sum_singleton| "" (SKOLEM!) (("" (EXPAND "sum") (("" (AUTO-REWRITE "choose_singleton[T]" "rest_singleton[T]" "sum_emptyset") (("" (SMASH) NIL NIL)) NIL)) NIL)) NIL) (|sum_x| "" (INDUCT "S" :NAME "finite_set_induction_gen") (("" (AUTO-REWRITE "card_rest" "card_remove" "nonempty?[T]") (("" (SKOSIMP*) (("" (EXPAND "sum" 1 1) (("" (SMASH) (("1" (DELETE -1) (("1" (GRIND :EXCLUDE "sum") NIL NIL)) NIL) ("2" (INST-CP - "rest(S!1)") (("2" (INST - "remove(x!1, S!1)") (("2" (ASSERT) (("2" (INST - "f!1" "choose(S!1)") (("1" (INST - "f!1" "x!1") (("1" (CASE-REPLACE "remove(choose(S!1), remove(x!1, S!1)) = remove(x!1, rest(S!1))") (("1" (REPLACE*) (("1" (REWRITE "plus_assoc" :DIR RL) (("1" (REWRITE "plus_assoc" :DIR RL) (("1" (LEMMA "plus_comm" ("r1" "f!1(x!1)" "r2" "f!1(choose(S!1))")) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (DELETE -1 -2 2 3) (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (GRIND :EXCLUDE ("choose")) NIL NIL)) NIL)) NIL)) NIL) ("2" (DELETE -1 2) (("2" (GRIND :EXCLUDE ("sum" "choose")) NIL NIL)) NIL)) NIL) ("2" (DELETE -1 2) (("2" (GRIND :EXCLUDE ("sum" "choose")) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sum_x1_x2| "" (SKOLEM!) (("" (REWRITE "sum_x" :DIR RL) (("" (REWRITE "sum_x" :DIR RL) NIL NIL)) NIL)) NIL) (|sum_add| "" (SKOLEM!) (("" (SMASH) (("1" (REWRITE "member_add") (("1" (REWRITE "plus_zero_right") NIL NIL)) NIL) ("2" (USE "sum_x" ("S" "add(x!1, S!1)")) (("1" (REWRITE "remove_add_member") (("1" (REWRITE "plus_comm") NIL NIL)) NIL) ("2" (EXPAND "add") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|sum_remove| "" (SKOLEM!) (("" (SMASH) (("1" (USE "sum_x") (("1" (REWRITE "plus_comm") (("1" (ASSERT) NIL NIL)) NIL) ("2" (EXPAND "member") (("2" (PROPAX) NIL NIL)) NIL)) NIL) ("2" (REWRITE "member_remove") (("2" (REWRITE "plus_zero_right") NIL NIL)) NIL)) NIL)) NIL) (|sum_rest_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|sum_rest| "" (SKOSIMP) (("" (ASSERT) (("" (EXPAND "sum" 2 2) (("" (PROPAX) NIL NIL)) NIL)) NIL)) NIL) (|sum_disj_union| "" (SKOLEM + ("A!1" _ "f!1")) (("" (AUTO-REWRITE "union_empty[T]" "sum_emptyset" "sum_add" "plus_zero_left" "plus_zero_right" "plus_assoc" "member") (("" (INDUCT "B" :NAME "finite_set_ind_modified") (("1" (ASSERT) NIL NIL) ("2" (SKOSIMP) (("2" (GROUND) (("1" (CASE-REPLACE "union(A!1, add(e!1, S!1)) = add(e!1, union(A!1, S!1))") (("1" (ASSERT) (("1" (SMASH) (("1" (DELETE -1 -2 2) (("1" (GRIND) NIL NIL)) NIL) ("2" (REPLACE -2) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (DELETE -1 -2 2 3) (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL) ("2" (DELETE 2 3) (("2" (GRIND :IF-MATCH NIL) (("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sum_diff_subset| "" (SKOSIMP) (("" (FORWARD-CHAIN "union_diff_subset") (("" (USE "sum_disj_union" ("A" "A!1")) (("" (REWRITE "difference_disjoint") (("" (GROUND) (("" (REPLACE*) (("" (REWRITE "plus_comm") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sum_union| "" (AUTO-REWRITE "union_subset1[T]" "intersection_subset1[T]" "plus_assoc") (("" (SKOLEM!) (("" (LEMMA "sum_diff_subset" ("f" "f!1")) (("" (INST-CP - "A!1" "union(A!1, B!1)") (("" (INST - "intersection(A!1, B!1)" "B!1") (("" (GROUND) (("1" (USE "diff_union_inter") (("1" (REWRITE "plus_comm" -2) (("1" (REPLACE -2 + RL) (("1" (REPLACE -3 + RL) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (REWRITE "intersection_commutative") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sum_diff_intersection| "" (SKOLEM!) (("" (AUTO-REWRITE "sum_emptyset" "plus_zero_right" "plus_zero_left" "plus_assoc") (("" (REWRITE "sum_union" :DIR RL) (("" (CASE-REPLACE "union(difference(A!1, B!1), intersection(A!1, B!1)) = A!1") (("1" (CASE-REPLACE "intersection(difference(A!1, B!1), intersection(A!1, B!1)) = emptyset") (("1" (ASSERT) NIL NIL) ("2" (DELETE -1 2) (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL) ("2" (DELETE 2) (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sum_f_g| "" (AUTO-REWRITE "sum_emptyset" "sum_add" "member") (("" (SKOLEM + (_ "f!1" "g!1")) (("" (INDUCT "S" :NAME "finite_set_ind_modified") (("1" (ASSERT) NIL NIL) ("2" (SKOSIMP) (("2" (GROUND) (("1" (INST?) (("1" (ASSERT) NIL NIL) ("2" (EXPAND "add") (("2" (PROPAX) NIL NIL)) NIL)) NIL) ("2" (DELETE 2 3) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sum_particular| "" (AUTO-REWRITE "plus_zero_right" "plus_zero_left") (("" (SKOLEM!) (("" (SMASH) (("1" (USE "sum_x") (("1" (USE "sum_x" ("f" "f!1 WITH [x!1 := zero]")) (("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) (|sum_distributive| "" (AUTO-REWRITE "sum_emptyset" "sum_add" "plus_zero_right" "plus_zero_left" "plus_assoc" "member") (("" (SKOLEM + (_ "f!1" "g!1")) (("" (INDUCT "A" :NAME "finite_set_ind_modified") (("1" (ASSERT) NIL NIL) ("2" (SKOSIMP) (("2" (ASSERT) (("2" (REPLACE -1 + RL) (("2" (LEMMA "plus_comm" ("r1" "f!1(e!1)" "r2" "sum(S!1, g!1) + g!1(e!1)")) (("2" (LEMMA "plus_comm" ("r1" "f!1(e!1)" "r2" "g!1(e!1)")) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) $$$finite_sets/nat_fun_props.pvs nat_fun_props : THEORY %------------------------------------------------------------------------ % Author: Bruno Dutertre % % Special properties of injective/surgective functions over nats %------------------------------------------------------------------------ BEGIN n, m : VAR nat injection_n_to_m : THEOREM (EXISTS (f : [below[n] -> below[m]]) : injective?(f)) IMPLIES n <= m surjection_n_to_m : THEOREM (EXISTS (f : [below[n] -> below[m]]) : surjective?(f)) IMPLIES m <= n bijection_n_to_m : THEOREM (EXISTS (f : [below[n] -> below[m]]) : bijective?(f)) IFF n = m END nat_fun_props $$$finite_sets/nat_fun_props.prf (|nat_fun_props| (|injection_n_to_m| "" (INDUCT "n") (("1" (ASSERT) NIL) ("2" (SKOSIMP*) (("2" (TYPEPRED "f!1(0)") (("2" (ASSERT) (("2" (HIDE -1) (("2" (INST -1 "m!1 - 1") (("2" (ASSERT) (("2" (DELETE 2) (("2" (INST 1 "LAMBDA (x : below[j!1]) : IF f!1(x) = m!1 - 1 THEN f!1(j!1) ELSE f!1(x) ENDIF") (("1" (EXPAND "injective?") (("1" (SKOSIMP) (("1" (LIFT-IF) (("1" (LIFT-IF) (("1" (INST-CP -2 "x1!1" "j!1") (("1" (INST-CP -2 "x2!1" "j!1") (("1" (INST -2 "x1!1" "x2!1") (("1" (ASSERT) (("1" (ASSERT) NIL))))))))))))))))) ("2" (SKOSIMP) (("2" (ASSERT) NIL))) ("3" (SKOSIMP) (("3" (EXPAND "injective?") (("3" (INST -2 "x!1" "j!1") (("3" (ASSERT) NIL))))))))))))))))))))))))) (|surjection_n_to_m| "" (SKOSIMP*) (("" (REWRITE "injection_n_to_m") (("" (EXPAND "surjective?") (("" (INST -1 "0") (("" (SKOSIMP) (("" (ASSERT) (("" (INST 1 "inverse(f!1)") (("1" (REWRITE "inj_inv") (("1" (INST 1 "x!1") NIL))) ("2" (INST 1 "x!1") NIL))))))))))))))) (|bijection_n_to_m| "" (SKOLEM!) (("" (PROP) (("1" (EXPAND "bijective?") (("1" (SKOSIMP) (("1" (LEMMA "injection_n_to_m" ("n" "n!1" "m" "m!1")) (("1" (LEMMA "surjection_n_to_m" ("n" "n!1" "m" "m!1")) (("1" (SPLIT) (("1" (ASSERT) (("1" (INST?) NIL))) ("2" (INST?) NIL))))))))))) ("2" (INST 1 "LAMBDA (x : below[n!1]) : x") (("1" (GRIND) NIL) ("2" (SKOLEM!) (("2" (ASSERT) NIL)))))))))) $$$finite_sets/card_def.pvs card_def[T: TYPE]: THEORY %------------------------------------------------------------------------ % % Fundamental definition of card % % Authors: Bruno Dutertre % Ricky W. Butler %------------------------------------------------------------------------ BEGIN IMPORTING finite_sets_def[T], nat_fun_props %, more_function_props % For proof only S, S2: VAR finite_set n,m: VAR nat x: VAR T p : VAR posnat inj_set(S): (nonempty?[nat]) = { n | EXISTS (f : [(S)->below[n]]) : injective?(f) } Card(S): nat = min(inj_set(S)) inj_Card : LEMMA Card(S) = n IMPLIES (EXISTS (f : [(S) -> below[n]]) : injective?(f)) reduce_inj : LEMMA (FORALL (f : [(S)->below[p]]) : injective?(f) AND NOT surjective?(f) IMPLIES (EXISTS (g: [(S)->below[p-1]]): injective?(g))) Card_injection: LEMMA (EXISTS (f : [(S)->below[n]]) : injective?(f)) IMPLIES Card(S) <= n Card_surjection : LEMMA (EXISTS (f : [(S)->below[n]]) : surjective?(f)) IMPLIES n <= Card(S) Card_bijection : THEOREM Card(S) = n IFF (EXISTS (f : [(S)->below[n]]) : bijective?(f)) Card_disj_union: THEOREM disjoint?(S,S2) IMPLIES Card(union(S,S2)) = Card(S) + Card(S2) % ------------------------------------------------------------------------ card(S): {n: nat| n = Card(S)} % inhibit expansion card_def : THEOREM card(S) = Card(S) % But if you really need to END card_def $$$finite_sets/card_def.prf (|card_def| (|inj_set_TCC1| "" (SKOLEM-TYPEPRED) (("" (EXPAND "is_finite") (("" (SKOSIMP*) (("" (EXPAND "nonempty?") (("" (EXPAND "empty?") (("" (EXPAND "member") (("" (INST -2 "N!1") (("" (INST?) NIL))))))))))))))) (|inj_Card| "" (SKOSIMP) (("" (EXPAND "Card") (("" (REWRITE "min_def") (("" (EXPAND "minimum?") (("" (FLATTEN) (("" (EXPAND "inj_set") (("" (PROPAX) NIL))))))))))))) (|reduce_inj_TCC1| "" (ASSERT) NIL) (|reduce_inj_TCC2| "" (ASSERT) NIL) (|reduce_inj| "" (SKOSIMP) (("" (GRIND :IF-MATCH NIL) (("" (INST 2 "LAMBDA (x : (S!1)) : IF f!1(x) = p!1 - 1 THEN y!1 ELSE f!1(x) ENDIF") (("1" (BETA) (("1" (SKOSIMP) (("1" (INST -2 "x1!1" "x2!1") (("1" (LIFT-IF) (("1" (LIFT-IF) (("1" (ASSERT) (("1" (PROP) (("1" (INST?) NIL) ("2" (INST 3 "x2!1") (("2" (ASSERT) NIL))))))))))))))))) ("2" (SKOSIMP) (("2" (ASSERT) NIL))) ("3" (SKOSIMP) (("3" (INST 2 "x!1") (("3" (ASSERT) NIL))))))))))) (|Card_injection| "" (SKOSIMP*) (("" (EXPAND "Card") (("" (TYPEPRED "min(inj_set(S!1))") (("" (INST?) (("" (ASSERT) (("" (EXPAND "inj_set") (("" (INST?) NIL))))))))))))) (|Card_surjection| "" (SKOSIMP*) (("" (NAME "CS" "Card(S!1)") (("" (REPLACE -1) (("" (FORWARD-CHAIN "inj_Card") (("" (SKOLEM!) (("" (REWRITE "injection_n_to_m") (("" (COPY -3) (("" (EXPAND "surjective?" -1) (("" (INST -1 "0") (("" (SKOSIMP*) (("" (INST 1 "f!2 o inverse(f!1)") (("1" (HIDE -3 2) (("1" (FORWARD-CHAIN "inj_inv[(S!1),below[n!1]]") (("1" (HIDE -4) (("1" (GRIND :IF-MATCH NIL :EXCLUDE INVERSE) (("1" (INST -6 "epsilon! (x: (S!1)): f!1(x) = x1!1" "epsilon! (x: (S!1)): f!1(x) = x2!1") (("1" (INST -3 "x1!1" "x2!1") (("1" (ASSERT) NIL))) ("2" (INST 1 "x!1") NIL))))))) ("2" (INST 1 "x!1") NIL))))) ("2" (INST 1 "x!1") NIL))))))))))))))))))))))) (|Card_bijection| "" (SKOLEM!) (("" (PROP) (("1" (FORWARD-CHAIN "inj_Card") (("1" (SKOLEM!) (("1" (INST?) (("1" (EXPAND "bijective?") (("1" (ASSERT) (("1" (CASE "n!1 = 0") (("1" (DELETE -2 -3) (("1" (GRIND) NIL))) ("2" (ASSERT) (("2" (FORWARD-CHAIN "reduce_inj") (("2" (FORWARD-CHAIN "Card_injection") (("2" (ASSERT) NIL))))))))))))))))))) ("2" (EXPAND "bijective?") (("2" (SKOSIMP) (("2" (LEMMA "Card_injection" ("S" "S!1" "n" "n!1")) (("2" (SPLIT) (("1" (LEMMA "Card_surjection" ("S" "S!1" "n" "n!1")) (("1" (GROUND) (("1" (INST?) NIL))))) ("2" (INST?) NIL))))))))))))) (|Card_disj_union| "" (SKOSIMP) (("" (NAME-REPLACE "N1" "Card(S!1)" :HIDE? NIL) (("" (NAME-REPLACE "N2" "Card(S2!1)" :HIDE? NIL) (("" (AUTO-REWRITE "Card_bijection") (("" (DO-REWRITE) (("" (SKOSIMP*) (("" (INST 1 "LAMBDA (x : (union(S!1, S2!1))) : IF S!1(x) THEN f!2(x) ELSE N1 + f!1(x) ENDIF") (("1" (EXPAND "bijective?") (("1" (PROP) (("1" (DELETE -2 -4) (("1" (GRIND) NIL))) ("2" (DELETE -1 -3) (("2" (GRIND :IF-MATCH NIL) (("2" (INST -3 "y!1") (("1" (SKOLEM!) (("1" (INST? 1) (("1" (ASSERT) NIL))))) ("2" (ASSERT) (("2" (INST -2 "y!1 - N1") (("2" (SKOLEM!) (("2" (GRIND) NIL))))))))))))))))) ("2" (SKOSIMP) (("2" (ASSERT) NIL))) ("3" (DELETE -1 -2) (("3" (GRIND) NIL))) ("4" (SKOSIMP) (("4" (ASSERT) NIL))))))))))))))))) (|card_TCC1| "" (INST 1 "(LAMBDA S: Card(S))") NIL) (|card_def| "" (SKOSIMP*) (("" (ASSERT) NIL)))) $$$finite_sets/finite_sets.pvs finite_sets[T: TYPE]: THEORY BEGIN IMPORTING card_def[T] A, B, S: VAR finite_set x: VAR T n: VAR nat card_emptyset : THEOREM card(emptyset[T]) = 0 empty_card : THEOREM empty?(S) IFF card(S) = 0 card_empty? : THEOREM (card(S) = 0) = empty?(S) card_is_0 : THEOREM (card(S) = 0) = (S = emptyset) nonempty_card : THEOREM nonempty?(S) IFF card(S) > 0 card_singleton : THEOREM card(singleton(x)) = 1 card_one : THEOREM card(S) = 1 IFF (EXISTS x : S = singleton(x)) card_disj_union : THEOREM disjoint?(A,B) IMPLIES card(union(A,B)) = card(A) + card(B) card_diff_subset: THEOREM subset?(A, B) IMPLIES card(difference(B, A)) = card(B) - card(A) card_subset : THEOREM subset?(A,B) IMPLIES card(A) <= card(B) card_plus : THEOREM card(A) + card(B) = card(union(A, B)) + card(intersection(A,B)) card_union : THEOREM card(union(A,B)) = card(A) + card(B) - card(intersection(A,B)) card_add : THEOREM card(add(x, S)) = card(S) + IF S(x) THEN 0 ELSE 1 ENDIF card_remove : THEOREM card(remove(x, S)) = card(S) - IF S(x) THEN 1 ELSE 0 ENDIF card_rest : THEOREM NOT empty?(S) IMPLIES card(rest(S)) = card(S) - 1 same_card_subset: THEOREM subset?(A, B) AND card(A) = card(B) IMPLIES A = B smaller_card_subset : THEOREM subset?(A, B) AND card(A) < card(B) IMPLIES (EXISTS x : member(x, B) AND NOT member(x, A)) card_1_has_1 : THEOREM card(S) >= 1 IMPLIES (EXISTS (x: T): S(x)) card_2_has_2 : THEOREM card(S) >= 2 IMPLIES (EXISTS (x,y: T): x /= y AND S(x) AND S(y)) card_intersection_le: THEOREM card(intersection(A,B)) <= card(A) AND card(intersection(A,B)) <= card(B) N: VAR nat card_bij : THEOREM card(S) = N IFF (EXISTS (f: [(S) -> below[N]]): bijective?(f)) bij_exists : COROLLARY (EXISTS (f: [(S) -> below(card(S))]): bijective?(f)) % card_n_has_n : THEOREM card(S) >= n IMPLIES % (EXISTS (X: [below[N] -> T]): % (FORALL (i: below[N]): S(X(i))) AND % (FORALL (i,j: below[N]): X(i) /= X(j))) END finite_sets $$$finite_sets/finite_sets.prf (|finite_sets| (|card_emptyset| "" (REWRITE "card_def") (("" (REWRITE "Card_bijection") (("" (INST 1 "LAMBDA (x : {x: T | FALSE}) : 0") (("1" (EXPAND "bijective?") (("1" (PROP) (("1" (EXPAND "injective?") (("1" (SKOSIMP*) (("1" (TYPEPRED "x1!1") (("1" (EXPAND "emptyset") (("1" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (EXPAND "surjective?") (("2" (SKOSIMP*) NIL NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (EXPAND "emptyset") (("2" (PROPAX) NIL NIL)) NIL)) NIL) ("3" (SKOSIMP*) NIL NIL)) NIL)) NIL)) NIL) (|empty_card| "" (SKOLEM!) (("" (PROP) (("1" (REWRITE "emptyset_is_empty?[T]") (("1" (REPLACE -1) (("1" (USE "card_emptyset") NIL NIL)) NIL)) NIL) ("2" (REWRITE "card_def") (("2" (REWRITE "Card_bijection") (("2" (SKOLEM!) (("2" (DELETE -) (("2" (GRIND) (("2" (TYPEPRED "f!1(x!1)") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|card_empty?| "" (SKOSIMP*) (("" (REWRITE "empty_card") NIL NIL)) NIL) (|card_is_0| "" (SKOSIMP*) (("" (REWRITE "card_empty?") (("" (REWRITE "emptyset_is_empty?") NIL NIL)) NIL)) NIL) (|nonempty_card| "" (SKOSIMP) (("" (EXPAND "nonempty?") (("" (REWRITE "empty_card") (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL) (|card_singleton| "" (SKOSIMP*) (("" (REWRITE "card_def") (("" (REWRITE "Card_bijection") (("" (INST 1 "LAMBDA (y : (singleton(x!1))) : 0") (("" (GRIND) (("" (INST 1 "x!1") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|card_one| "" (SKOSIMP*) (("" (REWRITE "card_def") (("" (PROP) (("1" (REWRITE "Card_bijection") (("1" (SKOLEM!) (("1" (GRIND :IF-MATCH NIL) (("1" (INST -2 "0") (("1" (SKOLEM!) (("1" (INST? 1) (("1" (APPLY-EXTENSIONALITY :HIDE? T) (("1" (IFF) (("1" (GROUND) (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOLEM!) (("2" (REPLACE -1) (("2" (HIDE -1) (("2" (REWRITE "card_def" :DIR RL) (("2" (REWRITE "card_singleton") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|card_disj_union| "" (SKOSIMP*) (("" (REWRITE "card_def") (("" (REWRITE "card_def") (("" (REWRITE "card_def") (("" (REWRITE "Card_disj_union") NIL NIL)) NIL)) NIL)) NIL)) NIL) (|card_diff_subset| "" (SKOSIMP) (("" (FORWARD-CHAIN "union_diff_subset") (("" (LEMMA "card_disj_union") (("" (INST?) (("" (ASSERT) (("" (REWRITE "difference_disjoint") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|card_subset| "" (SKOSIMP) (("" (FORWARD-CHAIN "card_diff_subset") (("" (ASSERT) NIL NIL)) NIL)) NIL) (|card_plus| "" (AUTO-REWRITE "union_subset1[T]" "intersection_subset1[T]") (("" (SKOLEM!) (("" (LEMMA "card_diff_subset") (("" (INST-CP -1 "A!1" "union(A!1, B!1)") (("" (REWRITE "diff_union_inter[T]") (("" (INST? -1) (("" (GROUND) (("" (REWRITE "intersection_commutative" 1) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|card_union| "" (SKOSIMP*) (("" (LEMMA "card_plus") (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|card_add| "" (SKOSIMP*) (("" (LIFT-IF) (("" (PROP) (("1" (REWRITE "member_add") (("1" (ASSERT) NIL NIL) ("2" (EXPAND "member") (("2" (PROPAX) NIL NIL)) NIL)) NIL) ("2" (REWRITE "add_as_union") (("2" (REWRITE "singleton" :DIR RL) (("2" (REWRITE "union_commutative") (("2" (REWRITE "card_disj_union") (("1" (REWRITE "card_singleton") (("1" (ASSERT) (("1" (EXPAND "singleton") (("1" (PROPAX) NIL NIL)) NIL)) NIL)) NIL) ("2" (REWRITE "singleton_disjoint") (("2" (EXPAND "member") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|card_remove| "" (SKOLEM!) (("" (LIFT-IF) (("" (PROP) (("1" (REWRITE "remove_as_difference") (("1" (REWRITE "card_diff_subset") (("1" (REWRITE "card_singleton") NIL NIL) ("2" (LEMMA "singleton_subset[T]") (("2" (INST?) (("2" (EXPAND "member") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (REWRITE "member_remove") (("1" (ASSERT) NIL NIL) ("2" (EXPAND "member") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|card_rest| "" (SKOSIMP) (("" (EXPAND "rest") (("" (REWRITE "card_remove") (("1" (LEMMA "choose_member[T]") (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (EXPAND "nonempty?") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|same_card_subset| "" (SKOSIMP) (("" (CASE "EXISTS x : member(x, B!1) AND subset?(A!1, remove(x, B!1))") (("1" (SKOSIMP) (("1" (EXPAND "member") (("1" (FORWARD-CHAIN "card_subset") (("1" (REWRITE "card_remove") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (GRIND :EXCLUDE "Card" :IF-MATCH NIL) (("1" (INST? -) (("1" (ASSERT) NIL NIL)) NIL) ("2" (INST? +) (("2" (ASSERT) (("2" (SKOSIMP) (("2" (ASSERT) (("2" (INST - "x!2") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|smaller_card_subset| "" (SKOSIMP) (("" (FORWARD-CHAIN "card_subset") (("" (CASE-REPLACE "A!1 = B!1") (("1" (ASSERT) NIL NIL) ("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|card_1_has_1| "" (SKOSIMP*) (("" (USE "card_empty?") (("" (IFF) (("" (FLATTEN) (("" (ASSERT) (("" (EXPAND "empty?") (("" (SKOSIMP*) (("" (EXPAND "member") (("" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|card_2_has_2| "" (SKOSIMP*) (("" (LEMMA "card_1_has_1") (("" (INST?) (("" (ASSERT) (("" (SKOSIMP*) (("" (LEMMA "card_1_has_1") (("" (INST -1 "remove(x!1,S!1)") (("" (REWRITE "card_remove") (("" (LIFT-IF) (("" (ASSERT) (("" (SKOSIMP*) (("" (EXPAND "remove") (("" (EXPAND "member") (("" (FLATTEN) (("" (INST 2 "x!1" "x!2") (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|card_intersection_le| "" (SKOSIMP*) (("" (CASE "subset?(intersection(A!1, B!1),A!1) AND subset?(intersection(A!1, B!1),B!1)") (("1" (FLATTEN) (("1" (LEMMA "card_subset") (("1" (SPLIT 1) (("1" (INST -1 "intersection(A!1, B!1)" "A!1") (("1" (ASSERT) NIL NIL)) NIL) ("2" (INST -1 "intersection(A!1, B!1)" "B!1") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (EXPAND "subset?") (("2" (EXPAND "intersection") (("2" (EXPAND "member") (("2" (SPLIT 1) (("1" (SKOSIMP*) NIL NIL) ("2" (SKOSIMP*) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|card_bij| "" (SKOSIMP*) (("" (REWRITE "card_def") (("" (REWRITE "Card_bijection") NIL NIL)) NIL)) NIL) (|bij_exists| "" (SKOSIMP*) (("" (LEMMA "card_bij") (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) $$$finite_sets/top.pvs %------------------------------------------------------------------------ % % Top of finite sets theory Version 2.2 5/22/97 % -------------------------------------------------------------- % Authors: Ricky W. Butler NASA Langley Research Center % Bruno Dutertre Royal Holloway & Bedford New College % Damir Jamsek Odyssey Research Associates % Sam Owre SRI International % David Griffioen CWI and KUN (Catholic University % Nijmegen), the Netherlands. % % Index: % ------ % finite_sets -- main theory that is imported % (provides basic type and cardinality) % finite_sets_sum -- summation over a set % finite_sets_minmax -- min and max over a set % finite_sets_inductions -- induction schemes % finite_sets_sum_real -- additional properties for summations % over real-valued functions % finite_sets_int -- special properties of integer sets % finite_sets_nat -- special properties of natural sets % finite_sets_pred -- lemmas involving predicate subtypes % finite_sets_below -- lemmas involving sets of below and upto % finite_sets_eq -- lemmas to show set is finite via mappings % finite_sets_card_eq -- equal cardinality of two dissimilar sets % finite_sets_rules -- experimental AUTO-REWRITE-THEORY rules % % % This theory was designed for making libraries and is not intended % for importing. One should directly import one of the above listed % theories. % %------------------------------------------------------------------------ top: THEORY BEGIN IMPORTING finite_sets, finite_sets_sum, finite_sets_minmax, finite_sets_inductions, finite_sets_sum_real, finite_sets_int, finite_sets_nat, finite_sets_pred, finite_sets_below, finite_sets_card_eq, finite_sets_eq END top $$$finite_sets/top.prf (|top| (IMPORTING1_TCC1 "" (REWRITE "zero_identity") NIL) (IMPORTING1_TCC2 "" (REWRITE "plus_ac") NIL)) $$$runs.pvs runs[State : TYPE, initial : PRED[State], transition : [State, State -> bool]] : THEORY BEGIN %runs are infinite sequences of transition-related states, starting in an initial state run_fragment: pred[sequence[State]] = {r : sequence[State] | FORALL (n : nat): transition(r(n),r(n+1))} run : pred[(run_fragment)] = {r : (run_fragment) | initial(r(0))} r: VAR (run) p :VAR [State->boolean] invariant(p) : bool = FORALL (r : (run), n:nat ): p(r(n)) invariant_rule : LEMMA (FORALL (r : (run)) : p(r(0)) AND FORALL (n : nat) : p(r(n)) IMPLIES p(r(n+1))) IMPLIES invariant(p) END runs $$$runs.prf (|runs| (|invariant_rule| "" (SKOSIMP*) (("" (EXPAND "invariant") (("" (INDUCT-AND-SIMPLIFY "n") NIL NIL)) NIL)) NIL)) $$$terminal_bank_query.pvs terminal_bank_query: THEORY BEGIN StatusType: TYPE = {OK, DONE} SlotType: TYPE = [# inUse: boolean, currency: int, balance: int #] pSlotCount: posnat SlotArray: TYPE = [nat -> SlotType] InquiryType: TYPE = {FIRST_SLOT, NEXT_SLOT} SlotReportType: TYPE = [# index: nat, currency: int, balance: int, status: StatusType #] SlotReportArray: TYPE = [int -> SlotReportType] Action: DATATYPE BEGIN SLOT_INQUIRY(mInquiry: InquiryType): SLOT_INQUIRY? SLOT_REPORT(mSlotInfo: SlotReportType): SLOT_REPORT? SEND_BANK(fRep: SlotReportArray, mBegin: nat, mEnd: nat): SEND_BANK? tau_CepSIQInit_InUse: tau_CepSIQInit_InUse? tau_CepSIQInit_NotInUse: tau_CepSIQInit_NotInUse? tau_CepSIQInit_Complete: tau_CepSIQInit_Complete? tau: tau? END Action Term_Location: TYPE = {l0, l1, l2, l3, l4} Bank_Location: TYPE = {b0, b1} Query_Location: TYPE = {Init, InquirySequence, Reply, Ready} Location: TYPE = [# Term: Term_Location, Bank: Bank_Location, Query: Query_Location #] State: TYPE = [# pc: Location, vSlots: SlotArray, slotsReported: [nat -> boolean], reportSize: nat, report: SlotReportArray, bReport: SlotReportArray, vSlotIndex: nat, vSlotsReported: nat #] initial(s: State): bool = s`pc = (# Term := l0, Bank := b0, Query := Init #) AND (FORALL (i, j: below(pSlotCount)): i /= j AND s`vSlots(i)`inUse AND s`vSlots(j)`inUse IMPLIES s`vSlots(i)`currency /= s`vSlots(j)`currency) next(s: State, a: Action, s_: State): bool = s`pc = (# Term := l0, Bank := b0, Query := Init #) AND SLOT_INQUIRY?(a) AND mInquiry(a) = FIRST_SLOT AND s_ = s WITH [vSlotIndex := 0, vSlotsReported := 0, reportSize := 0, pc := (# Term := l1, Bank := b0, Query := InquirySequence #)] OR s`pc = (# Term := l1, Bank := b0, Query := InquirySequence #) AND tau_CepSIQInit_InUse?(a) AND s`vSlotIndex < pSlotCount AND s`vSlots(s`vSlotIndex)`inUse AND s_ = s WITH [pc := (# Term := l1, Bank := b0, Query := InquirySequence #), vSlotIndex := s`vSlotIndex + 1, slotsReported := s`slotsReported WITH [(s`vSlotIndex) := FALSE]] OR s`pc = (# Term := l1, Bank := b0, Query := InquirySequence #) AND tau_CepSIQInit_NotInUse?(a) AND s`vSlotIndex < pSlotCount AND NOT s`vSlots(s`vSlotIndex)`inUse AND s_ = s WITH [pc := (# Term := l1, Bank := b0, Query := InquirySequence #), vSlotIndex := s`vSlotIndex + 1, vSlotsReported := s`vSlotsReported + 1, slotsReported := s`slotsReported WITH [(s`vSlotIndex) := TRUE]] OR s`pc = (# Term := l1, Bank := b0, Query := InquirySequence #) AND tau_CepSIQInit_Complete?(a) AND s`vSlotIndex = pSlotCount AND s_ = s WITH [pc := (# Term := l1, Bank := b0, Query := Reply #)] OR s`pc = (# Term := l1, Bank := b0, Query := Reply #) AND SLOT_REPORT?(a) AND s`vSlotsReported < pSlotCount AND mSlotInfo(a)`index >= 0 AND mSlotInfo(a)`index < pSlotCount AND NOT s`slotsReported(mSlotInfo(a)`index) AND s`vSlots(mSlotInfo(a)`index)`inUse AND mSlotInfo(a)`currency = s`vSlots(mSlotInfo(a)`index)`currency AND mSlotInfo(a)`status = OK AND s_ = s WITH [pc := (# Term := l3, Bank := b0, Query := Ready #), slotsReported := s`slotsReported WITH [(mSlotInfo(a)`index) := TRUE], vSlotsReported := s`vSlotsReported + 1, reportSize := s`reportSize + 1, report := s`report WITH [(s`reportSize)`currency := mSlotInfo(a)`currency]] OR s`pc = (# Term := l3, Bank := b0, Query := Ready #) AND SLOT_INQUIRY?(a) AND mInquiry(a) = NEXT_SLOT AND s_ = s WITH [pc := (# Term := l1, Bank := b0, Query := Reply #)] OR s`pc = (# Term := l1, Bank := b0, Query := Reply #) AND SLOT_REPORT?(a) AND s`vSlotsReported >= pSlotCount AND mSlotInfo(a)`status = DONE AND s_ = s WITH [pc := (# Term := l4, Bank := b0, Query := Init #)] OR s`pc = (# Term := l4, Bank := b0, Query := Init #) AND SEND_BANK?(a) AND mBegin(a) = 0 AND mEnd(a) = s`reportSize - 1 AND (FORALL (i: below(s`reportSize)): fRep(a)(i) = s`report(i)) AND s_ = s WITH [pc := (# Term := l0, Bank := b1, Query := Init #), bReport := LAMBDA (i: int): IF mBegin(a) <= i AND i <= mEnd(a) THEN fRep(a)(i) ELSE s`bReport(i) ENDIF] OR s`pc = (# Term := l0, Bank := b1, Query := Init #) AND tau?(a) AND s_ = s WITH [pc := (# Term := l0, Bank := b0, Query := Init #)] IMPORTING runs[State, initial, LAMBDA (s, s_: State): EXISTS (a: Action): next(s, a, s_)] END terminal_bank_query $$$requirements_aux.pvs requirements_aux: THEORY BEGIN IMPORTING terminal_bank_query %inductive aux: LEMMA invariant(LAMBDA (s: State): (FORALL (i, j: below(pSlotCount)): i /= j AND s`vSlots(i)`inUse AND s`vSlots(j)`inUse IMPLIES s`vSlots(i)`currency /= s`vSlots(j)`currency)) %inductive allslots1_aux1: LEMMA invariant(LAMBDA (s: State): s`pc`Query = InquirySequence IMPLIES s`reportSize = 0) %inductive in the context aux, allslots1_aux1 allslots1_aux0: LEMMA invariant(LAMBDA (s: State): (s`pc`Query = Reply OR s`pc`Query = Ready) IMPLIES (FORALL (i: below(s`reportSize), w: below(pSlotCount)): s`vSlots(w)`currency = s`report(i)`currency AND s`vSlots(w)`inUse IMPLIES s`slotsReported(w))) %inductive in the context allslots1_aux0 allslots1_aux: LEMMA invariant(LAMBDA (s: State): (s`pc`Query = Reply OR s`pc`Query = InquirySequence OR s`pc`Query = Ready OR s`pc = (# Term := l4, Bank := b0, Query := Init #)) IMPLIES (FORALL (i, j: below(s`reportSize)): i /= j IMPLIES s`report(i)`currency /= s`report(j)`currency)) lib: LIBRARY = "finite_sets" IMPORTING lib@top, lib@more_finite_sets inUse(s: State): setof[int] = {c: int | EXISTS (k: below(pSlotCount)): s`vSlots(k)`inUse AND c = s`vSlots(k)`currency} inUse_is_finite: JUDGEMENT inUse HAS_TYPE [State -> finite_set[int]] reported(s: State): setof[int] = {c: int | EXISTS (k: below(s`reportSize)): c = s`report(k)`currency} reported_is_finite: JUDGEMENT reported HAS_TYPE [State -> finite_set[int]] used_indices(s:State): setof[nat] = {k: nat | k < pSlotCount AND s`vSlots(k)`inUse} used_indices_is_finite : JUDGEMENT used_indices HAS_TYPE [State->finite_set[nat]] unused_indices(s: State): setof[nat] = {k: nat | k < s`vSlotIndex AND s`vSlotIndex <= pSlotCount AND NOT s`vSlots(k)`inUse} finite_unused_indices: JUDGEMENT unused_indices HAS_TYPE [State -> finite_set[nat]] inuse_and_reported(s: State): setof[nat] = {k: nat | k < s`vSlotIndex AND s`vSlotIndex <= pSlotCount AND s`slotsReported(k) AND s`vSlots(k)`inUse} finite_inuse_and_reported: JUDGEMENT inuse_and_reported HAS_TYPE [State -> finite_set[nat]] %inductive allslots2_aux10: LEMMA invariant(LAMBDA (s: State): s`pc`Query = InquirySequence IMPLIES (FORALL (i: nat): (i < s`vSlotIndex AND s`vSlotIndex <= pSlotCount AND s`vSlots(i)`inUse) IMPLIES NOT s`slotsReported(i))) %inductive allslots2_aux9: LEMMA invariant(LAMBDA (s: State): (s`pc`Query = Reply OR s`pc`Query = Ready) IMPLIES s`vSlotIndex = pSlotCount) %inductive in context allslots2_aux9 allslots2_aux8: LEMMA invariant(LAMBDA (s: State): (s`pc`Query = Reply OR s`pc`Query = Ready OR s`pc`Query = InquirySequence) IMPLIES (s`vSlotsReported <= s`vSlotIndex AND s`vSlotIndex <= pSlotCount)) %inductive in context allslots2_aux8, allslots2_aux9, allslots2_aux10 allslots2_aux7: LEMMA invariant(LAMBDA (s: State): (s`pc`Query = Reply OR s`pc`Query = Ready OR s`pc`Query = InquirySequence) IMPLIES s`reportSize = card(inuse_and_reported(s))) %inductive in context allslots2_aux9, allslots2_aux10 allslots2_aux6: LEMMA invariant(LAMBDA (s: State): (s`pc`Query = Reply OR s`pc`Query = Ready OR s`pc`Query = InquirySequence) IMPLIES card(unused_indices(s)) + card(inuse_and_reported(s)) = s`vSlotsReported) %inductive allslots2_aux5: LEMMA invariant(LAMBDA (s: State): (s`vSlotsReported = pSlotCount AND s`vSlotIndex = pSlotCount) IMPLIES card(unused_indices(s)) + card(used_indices(s)) = s`vSlotsReported) %inductive in context allslots2_aux5, allslots2_aux6,allslots2_aux7, allslots2_aux8, allslots2_aux9 allslots2_aux4: LEMMA invariant(LAMBDA (s: State): ((s`pc`Query = Reply OR s`pc`Query = Ready OR s`pc`Query = InquirySequence) AND s`vSlotsReported >= pSlotCount) IMPLIES card(used_indices(s)) = s`reportSize) %inductive in context aux allslots2_aux3: LEMMA invariant(LAMBDA (s: State): ((s`pc`Query = Reply OR s`pc`Query = Ready OR s`pc`Query = InquirySequence) AND s`vSlotsReported >= pSlotCount) IMPLIES card(inUse(s)) = s`reportSize) %inductive in context allslots2_aux10 allslots2_aux2: LEMMA invariant(LAMBDA (s: State): (s`pc`Query = Reply OR s`pc`Query = Ready OR s`pc`Query = InquirySequence) IMPLIES s`reportSize = card(reported(s))) %inductive in context allslots2_aux2, allslots2_aux3 allslots2_aux1: LEMMA invariant(LAMBDA (s: State): s`pc = (# Term := l4, Bank := b0, Query := Init #) IMPLIES card(inUse(s)) = card(reported(s))) %inductive allslots2_aux0: LEMMA invariant(LAMBDA (s: State): ((s`pc`Query = Reply OR s`pc`Query = Ready OR s`pc`Query = InquirySequence OR s`pc = (# Term := l4, Bank := b0, Query := Init #)) IMPLIES (FORALL (j: below(s`reportSize)): (EXISTS (i: below(pSlotCount)): s`vSlots(i)`inUse AND s`report(j)`currency = s`vSlots(i)`currency)))) %inductive in context allslots2_aux0, allslots2_aux1 allslots2_aux: LEMMA invariant(LAMBDA (s: State): s`pc = (# Term := l4, Bank := b0, Query := Init #) IMPLIES (FORALL (i: below(pSlotCount)): s`vSlots(i)`inUse IMPLIES (EXISTS (j: below(s`reportSize)): s`report(j)`currency = s`vSlots(i)`currency))) END requirements_aux $$$requirements_aux.prf (|requirements_aux| (|aux| "" (LEMMA "invariant_rule") (("" (INST?) (("" (SPLIT) (("1" (PROPAX) NIL NIL) ("2" (HIDE 2) (("2" (SKOLEM 1 "r") (("2" (TYPEPRED "r") (("2" (SPLIT) (("1" (HIDE -1) (("1" (GRIND) NIL NIL)) NIL) ("2" (HIDE -2) (("2" (SKOLEM 1 "n") (("2" (TYPEPRED "n") (("2" (FLATTEN) (("2" (SKOLEM 1 ("i" "j")) (("2" (INST -2 "i" "j") (("2" (EXPAND "run_fragment") (("2" (INST -3 "n") (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|allslots1_aux1| "" (LEMMA "invariant_rule") (("" (INST?) (("" (SPLIT) (("1" (PROPAX) NIL NIL) ("2" (HIDE 2) (("2" (SKOLEM 1 "r") (("2" (TYPEPRED "r") (("2" (SPLIT) (("1" (HIDE -1) (("1" (GRIND) NIL NIL)) NIL) ("2" (HIDE -2) (("2" (SKOLEM 1 "n") (("2" (TYPEPRED "n") (("2" (FLATTEN) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|allslots1_aux0| "" (LEMMA "invariant_rule") (("" (INST?) (("" (SPLIT) (("1" (PROPAX) NIL NIL) ("2" (HIDE 2) (("2" (SKOLEM 1 "r") (("2" (TYPEPRED "r") (("2" (SPLIT) (("1" (HIDE -1) (("1" (GRIND) NIL NIL)) NIL) ("2" (HIDE -2) (("2" (SKOLEM 1 "n") (("2" (TYPEPRED "n") (("2" (FLATTEN) (("2" (SKOLEM 1 ("i" "w")) (("2" (TYPEPRED "i") (("2" (TYPEPRED "w") (("2" (SPLIT) (("1" (EXPAND "run_fragment") (("1" (INST -6 "n") (("1" (GRIND :IF-MATCH NIL) (("1" (INST -1 "i" "w") (("1" (GRIND) NIL NIL)) NIL) ("2" (INST -1 "i" "w") (("2" (GRIND) NIL NIL)) NIL) ("3" (LEMMA "aux") (("3" (HIDE -2) (("3" (GRIND) NIL NIL)) NIL)) NIL) ("4" (INST -1 "i" "w") (("4" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (GRIND) (("2" (LEMMA "allslots1_aux1") (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|allslots1_aux| "" (LEMMA "invariant_rule") (("" (INST?) (("" (SPLIT) (("1" (PROPAX) NIL NIL) ("2" (HIDE 2) (("2" (SKOLEM 1 "r") (("2" (TYPEPRED "r") (("2" (SPLIT) (("1" (HIDE -1) (("1" (GRIND) NIL NIL)) NIL) ("2" (HIDE -2) (("2" (SKOLEM 1 "n") (("2" (TYPEPRED "n") (("2" (FLATTEN) (("2" (SKOLEM 1 ("i" "w")) (("2" (TYPEPRED "i") (("2" (TYPEPRED "w") (("2" (EXPAND "run_fragment") (("2" (INST -6 "n") (("2" (SPLIT) (("1" (GRIND :IF-MATCH NIL) (("1" (INST -1 "i" "w") (("1" (GRIND) NIL NIL)) NIL) ("2" (INST -1 "i" "w") (("2" (GRIND) NIL NIL)) NIL) ("3" (INST -1 "i" "w") (("3" (GRIND) NIL NIL)) NIL) ("4" (INST -1 "i" "w") (("4" (GRIND) NIL NIL)) NIL) ("5" (LEMMA "allslots1_aux0") (("5" (HIDE -2) (("5" (GRIND) NIL NIL)) NIL)) NIL) ("6" (LEMMA "allslots1_aux0") (("6" (HIDE -2) (("6" (GRIND) NIL NIL)) NIL)) NIL) ("7" (GRIND) NIL NIL) ("8" (INST -1 "i" "w") (("8" (GRIND) NIL NIL)) NIL)) NIL) ("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|inUse_is_finite| "" (SKOLEM 1 "s") (("" (LEMMA "more_finite_sets[nat,int].finite_image") (("" (INST -1 "{k:nat| k < pSlotCount}" "LAMBDA(p:below(pSlotCount)) : s`vSlots(p)`currency") (("1" (NAME "currencies" "{y: int | EXISTS (x: ({k: nat | k < pSlotCount})): y = s`vSlots(x)`currency}") (("1" (REPLACE -1) (("1" (EXPAND "is_finite") (("1" (SKOLEM -2 ("N" "f")) (("1" (INST 1 "N" "LAMBDA (c : (inUse(s))) : f(c)") (("1" (EXPAND "injective?") (("1" (SKOLEM + ("x1" "x2")) (("1" (TYPEPRED "x1") (("1" (TYPEPRED "x2") (("1" (INST - "x1" "x2") (("1" (EXPAND* "inUse" "currencies") (("1" (SKOLEM - "k") (("1" (INST + "k") (("1" (GROUND) NIL NIL)) NIL)) NIL)) NIL) ("2" (EXPAND* "inUse" "currencies") (("2" (SKOLEM -2 "k") (("2" (INST + "k") (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (EXPAND* "InUse" "currencies") (("2" (SKOLEM 1 "c") (("2" (TYPEPRED "c") (("2" (EXPAND "inUse") (("2" (SKOLEM - "k") (("2" (TYPEPRED "k") (("2" (INST + "k") (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (EXPAND "is_finite") (("2" (INST 1 "pSlotCount" "LAMBDA(p: below(pSlotCount)) : p") (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|reported_is_finite| "" (SKOLEM 1 "s") (("" (LEMMA "more_finite_sets[nat,int].finite_image") (("" (INST -1 "{k:nat| k < s`reportSize}" "LAMBDA(p:below(s`reportSize)) : s`report(p)`currency") (("1" (NAME "currencies" "{y: int | EXISTS (x: ({k: nat | k < s`reportSize})): y = s`report(x)`currency}") (("1" (REPLACE -1) (("1" (EXPAND "is_finite") (("1" (SKOLEM -2 ("N" "f")) (("1" (INST 1 "N" "LAMBDA (c : (reported(s))) : f(c)") (("1" (EXPAND "injective?") (("1" (SKOLEM + ("x1" "x2")) (("1" (TYPEPRED "x1") (("1" (TYPEPRED "x2") (("1" (INST - "x1" "x2") (("1" (EXPAND* "reported" "currencies") NIL NIL) ("2" (EXPAND* "reported" "currencies") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (EXPAND* "reported" "currencies") (("2" (SKOLEM 1 "c") (("2" (TYPEPRED "c") (("2" (EXPAND "reported") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (EXPAND "is_finite") (("2" (INST 1 "s`reportSize" "LAMBDA(p: below(s`reportSize)) : p") (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|used_indices_is_finite| "" (SKOLEM 1 "s") (("" (EXPAND* "is_finite" "used_indices") (("" (INST 1 "pSlotCount" "LAMBDA (n : (used_indices(s))) :n") (("1" (GRIND) NIL NIL) ("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL) (|finite_unused_indices| "" (EXPAND* "is_finite" "unused_indices") (("" (SKOLEM 1 "s") (("" (INST 1 "pSlotCount" "LAMBDA (x : (unused_indices(s))) : x") (("1" (GRIND) NIL NIL) ("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL) (|finite_inuse_and_reported| "" (SKOLEM 1 "s") (("" (EXPAND* "is_finite" "inuse_and_reported") (("" (INST 1 "pSlotCount" "LAMBDA (x : (inuse_and_reported(s))) : x") (("1" (GRIND) NIL NIL) ("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL) (|allslots2_aux10| "" (LEMMA "invariant_rule") (("" (INST?) (("" (SPLIT) (("1" (PROPAX) NIL NIL) ("2" (HIDE 2) (("2" (SKOLEM 1 "r") (("2" (TYPEPRED "r") (("2" (SPLIT) (("1" (HIDE -1) (("1" (GRIND) NIL NIL)) NIL) ("2" (HIDE -2) (("2" (SKOLEM 1 "n") (("2" (EXPAND "run_fragment") (("2" (INST -1 "n") (("2" (FLATTEN) (("2" (SKOLEM 1 "i") (("2" (SPLIT) (("1" (INST -1 "i") (("1" (GRIND) NIL NIL)) NIL) ("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|allslots2_aux9| "" (LEMMA "invariant_rule") (("" (INST?) (("" (SPLIT) (("1" (PROPAX) NIL NIL) ("2" (HIDE 2) (("2" (SKOLEM 1 "r") (("2" (TYPEPRED "r") (("2" (SPLIT) (("1" (HIDE -1) (("1" (GRIND) NIL NIL)) NIL) ("2" (HIDE -2) (("2" (SKOLEM 1 "n") (("2" (TYPEPRED "n") (("2" (FLATTEN) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|allslots2_aux8| "" (LEMMA "invariant_rule") (("" (INST?) (("" (SPLIT) (("1" (PROPAX) NIL NIL) ("2" (HIDE 2) (("2" (SKOLEM 1 "r") (("2" (TYPEPRED "r") (("2" (SPLIT) (("1" (HIDE -1) (("1" (GRIND) NIL NIL)) NIL) ("2" (HIDE -2) (("2" (SKOLEM 1 "n") (("2" (TYPEPRED "n") (("2" (FLATTEN) (("2" (GRIND) (("2" (LEMMA "allslots2_aux9") (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|allslots2_aux7| "" (LEMMA "invariant_rule") (("" (INST?) (("1" (SPLIT) (("1" (PROPAX) NIL NIL) ("2" (HIDE 2) (("2" (SKOLEM 1 "r") (("2" (TYPEPRED "r") (("2" (SPLIT) (("1" (HIDE -1) (("1" (GRIND) NIL NIL)) NIL) ("2" (HIDE -2) (("2" (SKOLEM 1 "n") (("2" (EXPAND "run_fragment") (("2" (INST -1 "n") (("2" (FLATTEN) (("2" (GRIND) (("1" (CASE "inuse_and_reported(r(n)) = inuse_and_reported(r(n) WITH [pc := (# Term := l1, Bank := b0, Query := Reply #)])") (("1" (ASSERT) NIL NIL) ("2" (EXPAND "inuse_and_reported") (("2" (PROPAX) NIL NIL)) NIL)) NIL) ("2" (CASE "inuse_and_reported(r(n)) = inuse_and_reported(r(n) WITH [pc := (# Term := l1, Bank := b0, Query := Reply #)])") (("1" (ASSERT) NIL NIL) ("2" (EXPAND "inuse_and_reported") (("2" (PROPAX) NIL NIL)) NIL)) NIL) ("3" (HIDE 2 3 4 5) (("3" (HIDE -2 -4 -10 -11) (("3" (NAME "m" "mSlotInfo(a!1)`index") (("3" (REPLACE -1) (("3" (CASE "inuse_and_reported(r(n) WITH [pc := (# Term := l3, Bank := b0, Query := Ready #), slotsReported := r(n)`slotsReported WITH [(m) := TRUE], vSlotsReported := 1 + r(n)`vSlotsReported, reportSize := 1 + card(inuse_and_reported(r(n))), report := r(n)`report WITH [(card (inuse_and_reported(r(n)))) `currency := r(n)`vSlots (m)`currency]]) = add(m,inuse_and_reported(r(n)))") (("1" (REPLACE -1) (("1" (HIDE -1) (("1" (LEMMA "finite_sets[nat].card_add") (("1" (INST?) (("1" (GROUND) NIL NIL) ("2" (HIDE -) (("2" (HIDE 2 3) (("2" (INST 1 "pSlotCount" "LAMBDA (x: (inuse_and_reported(r(n)))) : x") (("1" (GRIND) NIL NIL) ("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (EXPAND* "inuse_and_reported" "add" "member") (("2" (APPLY-EXTENSIONALITY) (("2" (GRIND 1) (("1" (LEMMA "allslots2_aux8") (("1" (GRIND) NIL NIL)) NIL) ("2" (LEMMA "allslots2_aux9") (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (HIDE -) (("3" (HIDE 2 3) (("3" (INST 1 "pSlotCount" "LAMBDA (x: (inuse_and_reported(r(n)))) : x") (("1" (GRIND) NIL NIL) ("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("4" (LEMMA "finite_sets[nat].card_emptyset") (("4" (CASE "inuse_and_reported(r(n) WITH [vSlotIndex := 0, vSlotsReported := 0, reportSize := 0, pc := (# Term := l1, Bank := b0, Query := InquirySequence #)]) = emptyset") (("1" (ASSERT) NIL NIL) ("2" (EXPAND* "inuse_and_reported" "emptyset") NIL NIL)) NIL)) NIL) ("5" (CASE "inuse_and_reported(r(n)) = inuse_and_reported(r(n) WITH [pc := (# Term := l1, Bank := b0, Query := InquirySequence #), vSlotIndex := 1 + r(n)`vSlotIndex, slotsReported := r(n)`slotsReported WITH [(r(n)`vSlotIndex) := FALSE]])") (("1" (ASSERT) NIL NIL) ("2" (EXPAND "inuse_and_reported") (("2" (APPLY-EXTENSIONALITY) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL) ("6" (CASE "inuse_and_reported(r(n)) = inuse_and_reported(r(n) WITH [pc := (# Term := l1, Bank := b0, Query := InquirySequence #), vSlotIndex := 1 + r(n)`vSlotIndex, vSlotsReported := 1 + r(n)`vSlotsReported, slotsReported := r(n)`slotsReported WITH [(r(n)`vSlotIndex) := TRUE]])") (("1" (ASSERT) NIL NIL) ("2" (APPLY-EXTENSIONALITY) (("2" (LEMMA "allslots2_aux10") (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL) ("7" (CASE "inuse_and_reported(r(n) WITH [vSlotIndex := 0, vSlotsReported := 0, reportSize := 0, pc := (# Term := l1, Bank := b0, Query := InquirySequence #)]) = emptyset") (("1" (LEMMA "finite_sets[nat].card_emptyset") (("1" (ASSERT) NIL NIL)) NIL) ("2" (EXPAND* "inuse_and_reported" "emptyset") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (LEMMA "finite_inuse_and_reported") (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|allslots2_aux6| "" (LEMMA "invariant_rule") (("" (INST?) (("1" (SPLIT) (("1" (PROPAX) NIL NIL) ("2" (HIDE 2) (("2" (SKOLEM 1 "r") (("2" (TYPEPRED "r") (("2" (SPLIT) (("1" (HIDE -1) (("1" (GRIND) NIL NIL)) NIL) ("2" (HIDE -2) (("2" (SKOLEM 1 "n") (("2" (EXPAND "run_fragment") (("2" (INST -1 "n") (("2" (FLATTEN) (("2" (GRIND) (("1" (CASE "inuse_and_reported(r(n)) = inuse_and_reported(r(n) WITH [pc := (# Term := l1, Bank := b0, Query := Reply #)])") (("1" (CASE "unused_indices(r(n)) = unused_indices(r(n) WITH [pc := (# Term := l1, Bank := b0, Query := Reply #)])") (("1" (REPLACE -1) (("1" (REPLACE -2) (("1" (PROPAX) NIL NIL)) NIL)) NIL) ("2" (HIDE -1 -2 -3 -4 -5 -6 2 3) (("2" (EXPAND "unused_indices") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL) ("2" (EXPAND "inuse_and_reported") (("2" (PROPAX) NIL NIL)) NIL)) NIL) ("2" (CASE "inuse_and_reported(r(n)) = inuse_and_reported(r(n) WITH [pc := (# Term := l1, Bank := b0, Query := Reply #)])") (("1" (CASE "unused_indices(r(n)) = unused_indices(r(n) WITH [pc := (# Term := l1, Bank := b0, Query := Reply #)])") (("1" (ASSERT) NIL NIL) ("2" (EXPAND "unused_indices") (("2" (PROPAX) NIL NIL)) NIL)) NIL) ("2" (EXPAND "inuse_and_reported") (("2" (PROPAX) NIL NIL)) NIL)) NIL) ("3" (HIDE 2 3 4 5) (("3" (HIDE -2 -4 -9 -10 -11) (("3" (NAME "m" "mSlotInfo(a!1)`index") (("3" (REPLACE -1) (("3" (HIDE -1) (("3" (NAME "inuse_and_reported1" "inuse_and_reported(r(n) WITH [pc := (# Term := l3, Bank := b0, Query := Ready #), slotsReported := r(n)`slotsReported WITH [(m) := TRUE], vSlotsReported := 1 + r(n)`vSlotsReported, reportSize := 1 + r(n)`reportSize, report := r(n)`report WITH [(r(n)`reportSize)`currency := r(n)`vSlots (m)`currency]])") (("3" (REPLACE -1) (("3" (NAME "unused_indices1" "unused_indices(r(n) WITH [pc := (# Term := l3, Bank := b0, Query := Ready #), slotsReported := r(n)`slotsReported WITH [(m) := TRUE], vSlotsReported := 1 + r(n)`vSlotsReported, reportSize := 1 + r(n)`reportSize, report := r(n)`report WITH [(r(n)`reportSize)`currency := r(n)`vSlots (m)`currency]])") (("3" (REPLACE -1) (("3" (CASE "inuse_and_reported1 = add(m,inuse_and_reported(r(n)))") (("1" (REPLACE -1) (("1" (CASE "unused_indices1 = unused_indices(r(n))") (("1" (REPLACE -1) (("1" (REPLACE -5 (1) RL) (("1" (SIMPLIFY 1) (("1" (HIDE -1 -2 -3 -4 -5) (("1" (LEMMA "finite_sets[nat].card_add") (("1" (INST?) (("1" (GROUND) NIL NIL) ("2" (HIDE -) (("2" (HIDE 2 3) (("2" (INST 1 "pSlotCount" "LAMBDA(w: (inuse_and_reported(r(n)))) : w") (("1" (GRIND) NIL NIL) ("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (REPLACE -2 (1) RL) (("2" (EXPAND "unused_indices") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (REPLACE -2 (1) RL) (("2" (HIDE -1 -2 -3 2) (("2" (EXPAND* "inuse_and_reported" "add" "member") (("2" (APPLY-EXTENSIONALITY) (("2" (HIDE 2) (("2" (GRIND) (("1" (LEMMA "allslots2_aux9") (("1" (GRIND) NIL NIL)) NIL) ("2" (LEMMA "allslots2_aux9") (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("4" (CASE "inuse_and_reported(r(n) WITH [vSlotIndex := 0, vSlotsReported := 0, reportSize := 0, pc := (# Term := l1, Bank := b0, Query := InquirySequence #)]) = emptyset") (("1" (CASE "unused_indices(r(n) WITH [vSlotIndex := 0, vSlotsReported := 0, reportSize := 0, pc := (# Term := l1, Bank := b0, Query := InquirySequence #)]) = emptyset") (("1" (REPLACE -1) (("1" (REPLACE -2) (("1" (LEMMA "finite_sets[nat].card_emptyset") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (EXPAND "unused_indices") (("2" (EXPAND "emptyset") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL) ("2" (EXPAND* "inuse_and_reported" "emptyset") NIL NIL)) NIL) ("5" (HIDE -2 -4 -7 2) (("5" (CASE "inuse_and_reported(r(n) WITH [pc := (# Term := l1, Bank := b0, Query := InquirySequence #), vSlotIndex := 1 + r(n)`vSlotIndex, slotsReported := r(n)`slotsReported WITH [(r(n)`vSlotIndex) := FALSE]]) = inuse_and_reported(r(n))") (("1" (REPLACE -1) (("1" (CASE "unused_indices(r(n)) = unused_indices(r(n) WITH [pc := (# Term := l1, Bank := b0, Query := InquirySequence #), vSlotIndex := 1 + r(n)`vSlotIndex, slotsReported := r(n)`slotsReported WITH [(r(n)`vSlotIndex) := FALSE]])") (("1" (REPLACE -1) (("1" (PROPAX) NIL NIL)) NIL) ("2" (HIDE -1 -2 2) (("2" (EXPAND "unused_indices") (("2" (APPLY-EXTENSIONALITY) (("2" (HIDE 2) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE -1 2) (("2" (EXPAND "inuse_and_reported") (("2" (APPLY-EXTENSIONALITY) (("2" (HIDE 2) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("6" (HIDE -2 -5 -6 2 3) (("6" (CASE "inuse_and_reported(r(n)) = inuse_and_reported(r(n) WITH [pc := (# Term := l1, Bank := b0, Query := InquirySequence #), vSlotIndex := 1 + r(n)`vSlotIndex, vSlotsReported := 1 + r(n)`vSlotsReported, slotsReported := r(n)`slotsReported WITH [(r(n)`vSlotIndex) := TRUE]])") (("1" (REPLACE -1 (1) RL) (("1" (HIDE -1) (("1" (CASE "unused_indices(r(n) WITH [pc := (# Term := l1, Bank := b0, Query := InquirySequence #), vSlotIndex := 1 + r(n)`vSlotIndex, vSlotsReported := 1 + r(n)`vSlotsReported, slotsReported := r(n)`slotsReported WITH [(r(n)`vSlotIndex) := TRUE]]) = add(r(n)`vSlotIndex,unused_indices(r(n)))") (("1" (REPLACE -1) (("1" (HIDE -1) (("1" (REPLACE -1 (1) RL) (("1" (SIMPLIFY 1) (("1" (HIDE -1) (("1" (LEMMA "finite_sets[nat].card_add") (("1" (INST?) (("1" (GROUND) NIL NIL) ("2" (HIDE -1 -2 2 3) (("2" (INST 1 "pSlotCount" "LAMBDA(x : (unused_indices(r(n)))) :x ") (("1" (GRIND) NIL NIL) ("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE -1 2) (("2" (EXPAND* "unused_indices" "add" "member") (("2" (APPLY-EXTENSIONALITY) (("2" (HIDE 2) (("2" (LEMMA "allslots2_aux10") (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE 2 -1) (("2" (EXPAND "inuse_and_reported") (("2" (APPLY-EXTENSIONALITY) (("2" (HIDE 2) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("7" (CASE "inuse_and_reported(r(n) WITH [vSlotIndex := 0, vSlotsReported := 0, reportSize := 0, pc := (# Term := l1, Bank := b0, Query := InquirySequence #)]) = emptyset") (("1" (CASE "unused_indices(r(n) WITH [vSlotIndex := 0, vSlotsReported := 0, reportSize := 0, pc := (# Term := l1, Bank := b0, Query := InquirySequence #)]) = emptyset") (("1" (REPLACE -1) (("1" (REPLACE -2) (("1" (LEMMA "finite_sets[nat].card_emptyset") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (EXPAND* "unused_indices" "emptyset") NIL NIL)) NIL) ("2" (EXPAND* "inuse_and_reported" "emptyset") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (LEMMA "finite_inuse_and_reported") (("2" (GRIND) NIL NIL)) NIL)) NIL) ("3" (HIDE 2) (("3" (LEMMA "finite_unused_indices") (("3" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|allslots2_aux5| "" (EXPAND "invariant") (("" (SKOLEM 1 ("r" "n")) (("" (FLATTEN) (("" (EXPAND* "unused_indices" "used_indices") (("" (REPLACE -1) (("" (REPLACE -2) (("" (HIDE -1 -2) (("" (SIMPLIFY) (("" (LEMMA "finite_sets[nat]. card_disj_union") (("" (INST -1 "{k: nat | k < pSlotCount AND r(n)`vSlots(k)`inUse}" "{k: nat | k < pSlotCount AND NOT r(n)`vSlots(k)`inUse}") (("1" (SPLIT) (("1" (REPLACE -1 (1) RL) (("1" (HIDE -1) (("1" (CASE "union({k: nat | k < pSlotCount AND r(n)`vSlots(k)`inUse}, {k: nat | k < pSlotCount AND NOT r(n)`vSlots(k)`inUse}) = {k:nat | k < pSlotCount}") (("1" (REPLACE -1) (("1" (HIDE -1) (("1" (LEMMA "card_def[nat].Card_bijection") (("1" (LEMMA "card_def[nat].card_def") (("1" (INST?) (("1" (INST?) (("1" (INST -2 "pSlotCount") (("1" (BDDSIMP) (("1" (REPLACE -2) (("1" (PROPAX) NIL NIL)) NIL) ("2" (HIDE -1 1 3) (("2" (INST 1 "LAMBDA (x : {k: nat | k < pSlotCount}) : x") (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE -1 2) (("2" (EXPAND "is_finite") (("2" (INST 1 "pSlotCount" "LAMBDA (x : {k: nat | k < pSlotCount}) : x") (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE -1 2) (("2" (EXPAND "is_finite") (("2" (INST 1 "pSlotCount" "LAMBDA (x : {k: nat | k < pSlotCount}) : x") (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (EXPAND* "union" "member") (("2" (APPLY-EXTENSIONALITY) (("2" (HIDE 2) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (EXPAND* "disjoint?" "member") (("2" (EXPAND* "empty?" "intersection" "member") (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (EXPAND "is_finite") (("2" (INST 1 "pSlotCount" "LAMBDA (x : {k: nat | k < pSlotCount AND NOT r(n)`vSlots(k)`inUse}) : x") (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL) ("3" (HIDE 2) (("3" (EXPAND "is_finite") (("3" (INST 1 "pSlotCount" "LAMBDA (x : {k: nat | k < pSlotCount AND r(n)`vSlots(k)`inUse}) : x") (("3" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|allslots2_aux4| "" (LEMMA "allslots2_aux5") (("" (LEMMA "allslots2_aux6") (("" (LEMMA "allslots2_aux7") (("" (LEMMA "allslots2_aux8") (("" (LEMMA "allslots2_aux9") (("" (EXPAND "invariant") (("" (SKOLEM 1 ("r" "n")) (("" (INST -1 "r" "n") (("" (INST -2 "r" "n") (("" (INST -3 "r" "n") (("" (INST -4 "r" "n") (("" (INST -5 "r" "n") (("" (EXPAND* "inuse_and_reported" "used_indices" "unused_indices") (("" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|allslots2_aux3| "" (LEMMA "allslots2_aux4") (("" (EXPAND "invariant") (("" (SKOLEM 1 ("r" "n")) (("" (INST -1 "r" "n") (("" (FLATTEN) (("" (NAME "p" "r(n)`pc`Query = Reply OR r(n)`pc`Query = Ready OR r(n)`pc`Query = InquirySequence") (("" (REPLACE -1) (("" (SPLIT -2) (("1" (REPLACE -1 (1) RL) (("1" (HIDE -) (("1" (CASE "used_indices(r(n)) = emptyset") (("1" (EXPAND* "used_indices" "emptyset" "member" "inUse") (("1" (GRIND) (("1" (LEMMA "finite_sets[nat].card_emptyset") (("1" (EXPAND "emptyset") (("1" (REPLACE -1) (("1" (HIDE -1) (("1" (CASE "{c: int | EXISTS (k: below(pSlotCount)): r(n)`vSlots(k)`inUse AND c = r(n)`vSlots(k)`currency} = emptyset[int]") (("1" (REPLACE -1) (("1" (LEMMA "finite_sets[int].card_emptyset") (("1" (PROPAX) NIL NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (EXPAND "emptyset") (("2" (APPLY-EXTENSIONALITY) (("2" (SKOLEM -1 "m") (("2" (FLATTEN) (("2" (CASE "{k: nat | k < pSlotCount AND r(n)`vSlots(k)`inUse}(m)") (("1" (REPLACE -4) (("1" (ASSERT) NIL NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (LEMMA "more_finite_sets[{k:nat | k < pSlotCount AND r(n)`vSlots(k)`inUse},int].inverse_bijection") (("1" (INST -1 "LAMBDA (w : {k: nat | k < pSlotCount AND r(n)`vSlots(k)`inUse}) : r(n)`vSlots(w)`currency ") (("1" (BETA) (("1" (SPLIT) (("1" (LEMMA "finite_sets_card_eq[int,nat].card_eq_bij") (("1" (INST?) (("1" (GROUND) (("1" (HIDE 2 3 4) (("1" (INST?) (("1" (EXPAND "bijective?") (("1" (BDDSIMP) (("1" (HIDE -1) (("1" (EXPAND "surjective?") (("1" (SKOLEM 1 "y") (("1" (INST -1 "y") (("1" (SKOLEM -1 "w") (("1" (INST 1 "w") (("1" (LEMMA "epsilons[{x_762: {k: nat | k < pSlotCount AND inUse(vSlots(r(n))(k))} | w = r(n)`vSlots(x_762)`currency}].epsilon_ax") (("1" (INST -1 "{x_762: {k: nat | k < pSlotCount AND inUse(vSlots(r(n))(k))} | w = r(n)`vSlots(x_762)`currency}") (("1" (EXPAND "restrict") (("1" (TYPEPRED "w") (("1" (SKOLEM - "xx") (("1" (EXPAND "inUse") (("1" (SPLIT) (("1" (REPLACE -1) (("1" (INST 1 "xx") (("1" (GRIND) NIL NIL)) NIL)) NIL) ("2" (INST 2 "xx") (("2" (GRIND :IF-MATCH NIL) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE -1 2) (("2" (TYPEPRED "w") (("2" (SKOLEM -1 "x") (("2" (INST 1 "x") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (TYPEPRED "y") (("2" (HIDE 2) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE -2) (("2" (EXPAND "injective?") (("2" (SKOLEM 1 ("x1" "x2")) (("2" (INST -1 "x1" "x2") (("1" (HIDE 2) (("1" (TYPEPRED "x2") (("1" (EXPAND "inUse") (("1" (SKOLEM - "k") (("1" (INST 1 "k") (("1" (GRIND) NIL NIL) ("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (TYPEPRED "x1") (("2" (EXPAND "inUse") (("2" (SKOLEM - "k") (("2" (INST 1 "k") (("1" (GRIND) NIL NIL) ("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE -) (("2" (SKOLEM 1 "x1") (("2" (BDDSIMP) (("1" (EXPAND "inUse") (("1" (SKOLEM -1 "k") (("1" (INST 1 "k") (("1" (TYPEPRED "k") (("1" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (EXPAND "inUse") (("2" (SKOLEM -1 "k") (("2" (INST 1 "k") (("1" (GRIND) NIL NIL) ("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (HIDE -1) (("3" (GRIND) NIL NIL)) NIL) ("4" (HIDE -1) (("4" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE -1 2 3) (("2" (LEMMA "used_indices_is_finite") (("2" (GRIND) NIL NIL)) NIL)) NIL) ("3" (HIDE -1 2 3) (("3" (LEMMA "inUse_is_finite") (("3" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE 2 3) (("2" (EXPAND "injective?") (("2" (LEMMA "aux") (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (EXPAND* "used_indices" "emptyset") (("2" (APPLY-EXTENSIONALITY) (("2" (INST 1 "x!1") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (PROPAX) NIL NIL) ("3" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|allslots2_aux2| "" (LEMMA "invariant_rule") (("" (INST?) (("1" (SPLIT) (("1" (PROPAX) NIL NIL) ("2" (HIDE 2) (("2" (SKOLEM 1 "r") (("2" (TYPEPRED "r") (("2" (SPLIT) (("1" (HIDE -1) (("1" (GRIND) NIL NIL)) NIL) ("2" (HIDE -2) (("2" (SKOLEM 1 "n") (("2" (TYPEPRED "n") (("2" (FLATTEN) (("2" (EXPAND "run_fragment") (("2" (INST - "n") (("2" (GRIND) (("1" (NAME "r1" "reported(r(n))") (("1" (NAME "r2" "reported(r(n) WITH [pc := (# Term := l1, Bank := b0, Query := Reply #)])") (("1" (REPLACE -1) (("1" (REPLACE -2) (("1" (CASE "r1 = r2") (("1" (ASSERT) NIL NIL) ("2" (APPLY-EXTENSIONALITY) (("2" (REPLACE -1 (1) RL) (("2" (REPLACE -2 (1) RL) (("2" (EXPAND "reported" 1) (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (NAME "r1" "reported(r(n))") (("2" (NAME "r2" "reported(r(n) WITH [pc := (# Term := l1, Bank := b0, Query := Reply #)])") (("2" (REPLACE -1) (("2" (REPLACE -2) (("2" (CASE "r1 = r2") (("1" (ASSERT) NIL NIL) ("2" (APPLY-EXTENSIONALITY) (("2" (REPLACE -1 (1) RL) (("2" (REPLACE -2 (1) RL) (("2" (EXPAND "reported" 1) (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (NAME "r1" "reported(r(n))") (("3" (NAME "r2" "reported(r(n) WITH [pc := (# Term := l3, Bank := b0, Query := Ready #), slotsReported := r(n)`slotsReported WITH [(mSlotInfo(a!1)`index) := TRUE], vSlotsReported := 1 + r(n)`vSlotsReported, reportSize := 1 + card(reported(r(n))), report := r(n)`report WITH [(card(reported(r(n))))`currency := r(n)`vSlots (mSlotInfo (a!1)`index)`currency]])") (("1" (REPLACE -1) (("1" (REPLACE -2) (("1" (NAME "m" "mSlotInfo(a!1)`index") (("1" (REPLACE -1) (("1" (HIDE -1 -4 -6 -8 -13 -14 -15 2 3 4 5) (("1" (LEMMA "allslots1_aux0") (("1" (EXPAND "invariant") (("1" (INST?) (("1" (GROUND) (("1" (INST - "_" "m") (("1" (REPLACE*) (("1" (CASE "r2 = add(r(n)`vSlots(m)`currency,r1)") (("1" (REPLACE -1) (("1" (LEMMA "finite_sets[int].card_add") (("1" (INST - "r1" "r(n)`vSlots(m)`currency") (("1" (REPLACE -1) (("1" (SIMPLIFY 1) (("1" (LIFT-IF) (("1" (BDDSIMP) (("1" (REWRITE "forall_not") (("1" (REPLACE -5 (-1) RL) (("1" (EXPAND "reported" -1) (("1" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE -1 -2 -3 -5 -6 -7 -8 -9 -10 2 3) (("2" (LEMMA "reported_is_finite") (("2" (INST -1 "r(n)") (("2" (EXPAND "is_finite") (("2" (SKOLEM - ("N" "f")) (("2" (INST 1 "N" "f") (("1" (EXPAND "injective?") (("1" (SKOLEM 1 ("x1" "x2")) (("1" (INST -1 "x1" "x2") NIL NIL)) NIL)) NIL) ("2" (REPLACE -2 (1) RL) (("2" (EXPAND "reported") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (EXPAND* "add" "member") (("2" (APPLY-EXTENSIONALITY 1) (("2" (IFF) (("2" (BDDSIMP 1) (("1" (REWRITE "forall_not") (("1" (HIDE -5 -6 -9 3 5 6) (("1" (REPLACE -2 (-1) RL) (("1" (HIDE -2) (("1" (REPLACE -2 (-3 2) RL) (("1" (EXPAND "reported") (("1" (SKOLEM - "k") (("1" (TYPEPRED "k") (("1" (REPLACE -2) (("1" (HIDE -2) (("1" (REPLACE -2) (("1" (REPLACE -2 (+) RL) (("1" (REPLACE -2 (-) RL) (("1" (HIDE -2) (("1" (INST 2 "k") (("1" (INST 3 "k") (("1" (GRIND) NIL NIL) ("2" (GRIND) NIL NIL)) NIL) ("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (REPLACE -1 (1) RL) (("2" (REPLACE -3 (1) RL) (("2" (EXPAND "reported") (("2" (INST 1 "card(r1)") (("1" (ASSERT) NIL NIL) ("2" (HIDE -1 -2 -3 -5 -6 -7 -8 -9 -10 2 3 4) (("2" (LEMMA "reported_is_finite") (("2" (INST - "r(n)") (("2" (EXPAND "is_finite") (("2" (SKOLEM -1 ("N" "f")) (("2" (INST 1 "N" "f") (("1" (EXPAND "injective?") (("1" (SKOLEM 1 ("x1" "x2")) (("1" (INST -1 "x1" "x2") NIL NIL)) NIL)) NIL) ("2" (REPLACE -2 (1) RL) (("2" (HIDE -1) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (REPLACE -3 (1) RL) (("3" (REPLACE -4 (-1) RL) (("3" (EXPAND "reported") (("3" (SKOLEM - "k") (("3" (INST -2 "k") (("3" (INST 1 "k") (("3" (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) ("2" (HIDE -1 -2 -3 -4 -5 -6 -7 -8 -9 -10 -11 -12 -13 2 3 4 5 6 7) (("2" (LEMMA "reported_is_finite") (("2" (INST - "r(n)") (("2" (EXPAND "is_finite") (("2" (SKOLEM -1 ("N" "f")) (("2" (INST 1 "N" "f") (("2" (EXPAND "injective?") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("4" (NAME "r1" "reported(r(n) WITH [vSlotIndex := 0, vSlotsReported := 0, reportSize := 0, pc := (# Term := l1, Bank := b0, Query := InquirySequence #)])") (("4" (REPLACE -1) (("4" (CASE "r1 = emptyset") (("1" (LEMMA "finite_sets[int].card_emptyset") (("1" (ASSERT) NIL NIL)) NIL) ("2" (REPLACE -1 (1) RL) (("2" (EXPAND* "reported" "emptyset" "empty" "member") (("2" (APPLY-EXTENSIONALITY) (("2" (SKOLEM - "k") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("5" (NAME "r1" "reported(r(n))") (("5" (NAME "r2" "reported(r(n) WITH [pc := (# Term := l1, Bank := b0, Query := InquirySequence #), vSlotIndex := 1 + r(n)`vSlotIndex, slotsReported := r(n)`slotsReported WITH [(r(n)`vSlotIndex) := FALSE]])") (("5" (REPLACE -1) (("5" (REPLACE -2) (("5" (CASE "r1 = r2") (("1" (ASSERT) NIL NIL) ("2" (REPLACE -1 (1) RL) (("2" (REPLACE -2 (1) RL) (("2" (EXPAND "reported") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("6" (NAME "r1" "reported(r(n))") (("6" (NAME "r2" "reported(r(n) WITH [pc := (# Term := l1, Bank := b0, Query := InquirySequence #), vSlotIndex := 1 + r(n)`vSlotIndex, vSlotsReported := 1 + r(n)`vSlotsReported, slotsReported := r(n)`slotsReported WITH [(r(n)`vSlotIndex) := TRUE]])") (("6" (REPLACE -1) (("6" (REPLACE -2) (("6" (CASE "r1 = r2") (("1" (ASSERT) NIL NIL) ("2" (REPLACE -1 (1) RL) (("2" (REPLACE -2 (1) RL) (("2" (EXPAND "reported") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("7" (NAME "r1" "reported(r(n) WITH [vSlotIndex := 0, vSlotsReported := 0, reportSize := 0, pc := (# Term := l1, Bank := b0, Query := InquirySequence #)])") (("7" (REPLACE -1) (("7" (CASE "r1 = emptyset") (("1" (LEMMA "finite_sets[int].card_emptyset") (("1" (ASSERT) NIL NIL)) NIL) ("2" (REPLACE -1 (1) RL) (("2" (EXPAND* "reported" "emptyset" "empty" "member") (("2" (APPLY-EXTENSIONALITY) (("2" (SKOLEM - "k") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (LEMMA "reported_is_finite") (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|allslots2_aux1| "" (LEMMA "invariant_rule") (("" (INST?) (("1" (SPLIT) (("1" (PROPAX) NIL NIL) ("2" (HIDE 2) (("2" (SKOLEM 1 "r") (("2" (TYPEPRED "r") (("2" (SPLIT) (("1" (HIDE -1) (("1" (GRIND) NIL NIL)) NIL) ("2" (HIDE -2) (("2" (SKOLEM 1 "n") (("2" (TYPEPRED "n") (("2" (FLATTEN) (("2" (EXPAND "run_fragment") (("2" (INST - "n") (("2" (GRIND) (("1" (EXPAND "inUse") (("1" (EXPAND "reported") (("1" (PROPAX) NIL NIL)) NIL)) NIL) ("2" (EXPAND "inUse") (("2" (EXPAND "reported") (("2" (LEMMA "allslots2_aux3") (("2" (LEMMA "allslots2_aux2") (("2" (EXPAND "invariant") (("2" (INST?) (("2" (INST?) (("2" (GROUND) (("2" (EXPAND* "inUse" "reported") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (LEMMA "reported_is_finite") (("2" (GRIND) NIL NIL)) NIL)) NIL) ("3" (HIDE 2) (("3" (LEMMA "inUse_is_finite") (("3" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|allslots2_aux0| "" (LEMMA "invariant_rule") (("" (INST?) (("" (SPLIT) (("1" (PROPAX) NIL NIL) ("2" (HIDE 2) (("2" (SKOLEM 1 "r") (("2" (TYPEPRED "r") (("2" (SPLIT) (("1" (HIDE -1) (("1" (GRIND) NIL NIL)) NIL) ("2" (HIDE -2) (("2" (SKOLEM 1 "n") (("2" (TYPEPRED "n") (("2" (FLATTEN) (("2" (SKOLEM 1 "j") (("2" (TYPEPRED "j") (("2" (EXPAND "run_fragment") (("2" (INST -5 "n") (("2" (GRIND :IF-MATCH NIL) (("1" (INST -3 "j") NIL NIL) ("2" (INST -3 "j") NIL NIL) ("3" (INST 1 "mSlotInfo(a!1)`index") NIL NIL) ("4" (INST -3 "j") NIL NIL) ("5" (INST -3 "j") NIL NIL) ("6" (INST -3 "j") NIL NIL) ("7" (INST -3 "j") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|allslots2_aux| "" (LEMMA "allslots2_aux0") (("" (LEMMA "allslots2_aux1") (("" (EXPAND "invariant") (("" (SKOLEM 1 ("r" "n")) (("" (INST -1 "r" "n") (("" (INST -2 "r" "n") (("" (GROUND) (("" (SKOLEM 1 "i") (("" (TYPEPRED "i") (("" (FLATTEN) (("" (CASE "subset?(reported(r(n)), inUse(r(n)))") (("1" (HIDE -3) (("1" (CASE "subset?(inUse(r(n)), reported(r(n)))") (("1" (HIDE -2) (("1" (EXPAND* "reported" "inUse") (("1" (EXPAND* "subset?" "member") (("1" (INST -1 "r(n)`vSlots(i)`currency") (("1" (SPLIT) (("1" (SKOLEM - "j") (("1" (INST + "j") (("1" (GRIND) NIL NIL)) NIL)) NIL) ("2" (INST 1 "i") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE -2 -4 -5 2) (("2" (LEMMA "finite_sets[int].same_card_subset") (("2" (INST - "reported(r(n))" "inUse(r(n))") (("1" (GROUND) NIL NIL) ("2" (HIDE -1 -2 2) (("2" (LEMMA "inUse_is_finite") (("2" (GRIND) NIL NIL)) NIL)) NIL) ("3" (HIDE -1 -2 2) (("3" (LEMMA "reported_is_finite") (("3" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (EXPAND* "subset?" "member") (("2" (EXPAND* "reported" "inUse") (("2" (SKOLEM 1 "x") (("2" (FLATTEN) (("2" (SKOLEM - "k") (("2" (TYPEPRED "k") (("2" (INST -4 "k") (("2" (SKOLEM - "w") (("2" (TYPEPRED "w") (("2" (INST + "w") (("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))