Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2003-03-04 18:45:52 -0800 (Tue, 04 Mar 2003)
Revision: 4157
Log message:
- Added some properties and reduction rules of the group power operation.
- **Partially proved "Every subgroup of a cyclic group is cyclic" with 2 assumptions:
1. there is a smallest positive number k such that (a^k)_g in s^car;
2. exst q,c in int. m=q*k+r & 0<=r<k.
The first one should be provable with induction.
The second is a common theorem in mathematics.
(I just found that for 2nd assumption, I used r>0 instead of r>=0, but
this is minor.)
Besides, there are two problems:
1. Why can't I apply reduceC for "m * 0" in "/itt_cyclic_group/group_power_power_reduce/2" or "/itt_cyclic_group/group_power_power_reduce/2/1"
and for "mul_uni_Assoc" in "/itt_cyclic_group/group_power_power_reduce/3/1/1/1/1/1/2".
2. I'll try writing rules like "group_power_0" as reduce resources.