/[mojave]/metaprl/theories/czf/czf_itt_cyclic_subgroup.mli
ViewVC logotype

Log of /metaprl/theories/czf/czf_itt_cyclic_subgroup.mli

Parent Directory Parent Directory | Revision Log Revision Log


Links to HEAD: (view) (download) (annotate)
Sticky Revision:

Revision 3557 - (view) (download) (annotate) - [select for diffs]
Modified Tue Apr 2 08:18:40 2002 UTC (19 years, 2 months ago) by xiny
File length: 1196 byte(s)
Diff to previous 3537
1. Changed the representation of cyclic subgroups; it looks more
   natural now.
2. Updated the definition of cyclic subgroups. Since "eqG" was added
   to the def. of groups, the def. of a cyclic subgroup must give the
   description for "eqG" too.
3. Updated all rules and reproved them.

The same problems as in subgroups exist here also. Will fix soon.


Revision 3537 - (view) (download) (annotate) - [select for diffs]
Modified Mon Mar 11 10:03:46 2002 UTC (19 years, 3 months ago) by xiny
File length: 1097 byte(s)
Diff to previous 3502
1. Changed the definition of cyclic subgroups from cyclic_subgroup{'g;
   'a} to cyc_subg{'g; 's; 'a} where 's was added to represent the group
   of the cyclic_subgroup itself;
2. Added the functionality (both equality and equivalence) of the "power"
   operation;
3. Updated the properties of the power operation from "equal" to "equiv";
4. Updated and proved rules about cyclic subgroups;
5. Added tactic "cycsubgSubgroupT".

Problem:
  czf_itt_cyclic_subgroup.prla could not be committed. It gave the message
   "cvs server: sticky tag `1.5' for file `czf_itt_cyclic_subgroup.prla'
    is not a branch".


Revision 3502 - (view) (download) (annotate) - [select for diffs]
Modified Tue Feb 19 04:19:26 2002 UTC (19 years, 4 months ago) by xiny
File length: 928 byte(s)
Diff to previous 3493
Changed the definitions of cyclic subgroups and cyclic groups where
they both have the type "set". I'm considering defining them as
"types". So the properties are not proven in this commission. I commit
them only to enable metaprl to compile.


Revision 3493 - (view) (download) (annotate) - [select for diffs]
Modified Tue Feb 5 20:51:44 2002 UTC (19 years, 4 months ago) by xiny
File length: 926 byte(s)
Diff to previous 3491
Removed rule lt_Id and tactic lt_IdT since they are provable by tactic lt_AsymT
in module "itt_int_base".


Revision 3491 - (view) (download) (annotate) - [select for diffs]
Modified Tue Feb 5 08:20:00 2002 UTC (19 years, 4 months ago) by xiny
File length: 1103 byte(s)
Diff to previous 3488
Proved all rules related to the properties of cyclic subgroups.

TODO:
   rule lt_Id and tactic lt_IdT are better to be moved into module "itt_int_base" upon Yegor's approval.


Revision 3488 - (view) (download) (annotate) - [select for diffs]
Modified Wed Jan 30 22:36:50 2002 UTC (19 years, 4 months ago) by xiny
File length: 926 byte(s)
Diff to previous 3487
1. Small modifications in the proofs for "power_property2".
2. Changed the definition of cyclic subgroups to increase generality.
3. Added (more) properties for the changed cyclic subgroups.


Revision 3487 - (view) (download) (annotate) - [select for diffs]
Modified Wed Jan 30 08:41:01 2002 UTC (19 years, 4 months ago) by xiny
File length: 906 byte(s)
Diff to previous 3404
Removed some comments.


Revision 3404 - (view) (download) (annotate) - [select for diffs]
Added Sun Sep 23 07:25:28 2001 UTC (19 years, 9 months ago) by xiny
File length: 1073 byte(s)
1. Minor changes in czf_itt_group;
2. Define subgroup and abelian group;
3. Define cyclic subgroup and cyclic group. However, there are
   problems with the proofs in czf_itt_cyclic_subgroup.


This form allows you to request diffs between any two revisions of this file. For each of the two "sides" of the diff, enter a numeric revision.

  Diffs between and
  Type of Diff should be a

  ViewVC Help
Powered by ViewVC 1.1.26