40 (*WN0510 see simliar rules 'isolate_' 'separate_' (by RL) |
41 (*WN0510 see simliar rules 'isolate_' 'separate_' (by RL) |
41 [bdv_1,bdv_2,bdv_3,bdv_4] work also for 2 and 3 bdvs, ugly !*) |
42 [bdv_1,bdv_2,bdv_3,bdv_4] work also for 2 and 3 bdvs, ugly !*) |
42 separate_bdvs_add |
43 separate_bdvs_add |
43 "[| [] from_ [bdv_1,bdv_2,bdv_3,bdv_4] occur_exactly_in a |]\ |
44 "[| [] from_ [bdv_1,bdv_2,bdv_3,bdv_4] occur_exactly_in a |]\ |
44 \ ==> (a + b = c) = (b = c + -1*a)" |
45 \ ==> (a + b = c) = (b = c + -1*a)" |
|
46 separate_bdvs0 |
|
47 "[| some_of [bdv_1,bdv_2,bdv_3,bdv_4] occur_in b; Not (b=!=0) |]\ |
|
48 \ ==> (a = b) = (a + -1*b = 0)" |
45 separate_bdvs_add1 |
49 separate_bdvs_add1 |
46 "[| some_of [bdv_1,bdv_2,bdv_3,bdv_4] occur_in c |]\ |
50 "[| some_of [bdv_1,bdv_2,bdv_3,bdv_4] occur_in c |]\ |
47 \ ==> (a = b + c) = (a + -1*c = b)" |
51 \ ==> (a = b + c) = (a + -1*c = b)" |
48 (* |
52 separate_bdvs_add2 |
49 separate_bdvs_add3 |
53 "[| Not (some_of [bdv_1,bdv_2,bdv_3,bdv_4] occur_in a) |]\ |
50 "[| [bdv_3] from_ [bdv_1,bdv_2,bdv_3,bdv_4] occur_exactly_in a |]\ |
54 \ ==> (a + b = c) = (b = -1*a + c)" |
51 \ ==> (a + b = c) = (b = c + -1*a)" |
55 |
52 separate_bdvs_add4 |
56 |
53 "[| [bdv_4] from_ [bdv_1,bdv_2,bdv_3,bdv_4] occur_exactly_in a |]\ |
|
54 \ ==> (a + b = c) = (b = c + -1*a)" |
|
55 *) |
|
56 |
57 |
57 separate_bdvs_mult |
58 separate_bdvs_mult |
58 "[| [] from_ [bdv_1,bdv_2,bdv_3,bdv_4] occur_exactly_in a; Not (a=!=0) |]\ |
59 "[| [] from_ [bdv_1,bdv_2,bdv_3,bdv_4] occur_exactly_in a; Not (a=!=0) |]\ |
59 \ ==>(a * b = c) = (b = c / a)" |
60 \ ==>(a * b = c) = (b = c / a)" |
60 |
61 |