Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-05-19 00:21:32 -0700 (Sun, 19 May 2002)
Revision: 3676
Log message:
The former definition for group builder was not consistent. Now group_bvd{h; g; s} also requires that subset{s; car{g}}. From it, it can be proven that id{h} = id{g} and inv{h; a} = inv{g; a} for all a in car{h}.
Reproved all related rules and updated related comments.