Lines Matching refs:b2
96 (* can show p divides BAG_PROD b2, so p is also in b2 (because p is prime). *)
97 (* Let b1' = b1-p and b2' = b2-p. Then b1' = b2', by induction hypothesis. *)
98 (* Thus b1=b2. The argument uses a lemma derived from gcdTheory.P_EUCLIDES, *)
104 ``!n b1 b2.
106 (FINITE_BAG b2 /\ (!m. BAG_IN m b2 ==> prime m) /\ (n=BAG_GEN_PROD b2 1))
107 ==> (b1 = b2)``,
112 STRIP_ASSUME_TAC (ISPEC ``b2:num bag`` BAG_cases) THEN
122 `divides e (BAG_GEN_PROD b2 1)` by METIS_TAC [divides_def,MULT_SYM] THEN
123 `BAG_IN e b2` by METIS_TAC [lem1] THEN
124 `?b2'. b2 = BAG_INSERT e b2'` by METIS_TAC [BAG_DECOMPOSE] THEN
126 `FINITE_BAG b2'` by METIS_TAC [FINITE_BAG_THM] THEN
130 `BAG_GEN_PROD b2' 1 < BAG_GEN_PROD (BAG_INSERT e b2') 1`
134 `b2' = b1'` by METIS_TAC[FINITE_BAG_THM,BAG_IN_BAG_INSERT] THEN