Now a workable version for groups and cyclic subgroups. Rules proved, examples added. Problems left: The proofs for rules "power_property1", "power_property2", and "power_simplify" are not yet finished because of some itt problems.