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

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

Parent Directory Parent Directory | Revision Log Revision Log


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

Revision 3561 - (view) (download) (annotate) - [select for diffs]
Modified Wed Apr 3 05:29:19 2002 UTC (19 years, 2 months ago) by xiny
File length: 252229 byte(s)
Diff to previous 3557
Changed the definition of cyclic subgroups; fixed the previous error in
defining the operation and equivalence relation for cyclic subgroups.
Updated related rules.


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: 255157 byte(s)
Diff to previous 3539
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 3539 - (view) (download) (annotate) - [select for diffs]
Modified Mon Mar 11 10:35:54 2002 UTC (19 years, 3 months ago) by xiny
File length: 165135 byte(s)
Diff to previous 3502
This completes the committion of czf_itt_cyclic_subgroup.


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: 43677 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: 209640 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: 212726 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: 187931 byte(s)
Diff to previous 3484
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 3484 - (view) (download) (annotate) - [select for diffs]
Modified Wed Jan 30 00:36:09 2002 UTC (19 years, 4 months ago) by xiny
File length: 164965 byte(s)
Diff to previous 3405
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.


Revision 3405 - (view) (download) (annotate) - [select for diffs]
Modified Sun Sep 23 07:33:50 2001 UTC (19 years, 9 months ago) by xiny
File length: 93748 byte(s)
Diff to previous 3404
recommit .prla files


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: 93637 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