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

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

Parent Directory Parent Directory | Revision Log Revision Log


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

Revision 3553 - (view) (download) (annotate) - [select for diffs]
Modified Tue Apr 2 07:45:26 2002 UTC (19 years, 3 months ago) by xiny
File length: 151041 byte(s)
Diff to previous 3535 , to selected 3516
1. Added "eqG" to the definition of groups which denotes the equivalence
   relation related with the group. Every group has an equivalence
   relation, which is now explicitly described.
2. Accordingly, all rules related with equivalence relations in groups
   are updated and reproved.
3. Added tactics "uniqueInvLeftT" and "uniqueInvRightT" which might not
   be very useful though.


Revision 3535 - (view) (download) (annotate) - [select for diffs]
Modified Mon Mar 11 09:57:39 2002 UTC (19 years, 4 months ago) by xiny
File length: 138414 byte(s)
Diff to previous 3530 , to selected 3516
Added the elimination form of the unique inverse rule.


Revision 3530 - (view) (download) (annotate) - [select for diffs]
Modified Thu Mar 7 23:13:10 2002 UTC (19 years, 4 months ago) by xiny
File length: 136215 byte(s)
Diff to previous 3527 , to selected 3516
1. Added properties that "e * a = a * e" and "a * e = e * a".
2. Changed the definition of groups to one-sided (left) definition,
   i.e., groups are defined by the left axioms, and proved the right
   axioms.
3. Removed the introduction forms of group cancellation laws which
   were put in comments in the last version.


Revision 3527 - (view) (download) (annotate) - [select for diffs]
Modified Mon Mar 4 02:20:01 2002 UTC (19 years, 4 months ago) by xiny
File length: 120257 byte(s)
Diff to previous 3516
1. Replaced equality relations with equivalence relations in
   the definition axioms for "op", "inv", and "id".
2. Defined the equivalence functionality for "op" and "inv".
3. Changed the tactics for "left and right cancellation laws"
   (i.e., groupCancelLeftT and groupCancelRightT) to make it
   easier to use.
4. Re-proved all properties.


Revision 3516 - (view) (download) (annotate) - [selected]
Modified Mon Feb 25 02:24:42 2002 UTC (19 years, 5 months ago) by xiny
File length: 96837 byte(s)
Diff to previous 3498
Replaced equality relations with equivalence relations everywhere in the
context of groups, and re-proved the rules.


Revision 3498 - (view) (download) (annotate) - [select for diffs]
Modified Sun Feb 17 02:09:08 2002 UTC (19 years, 5 months ago) by xiny
File length: 94358 byte(s)
Diff to previous 3494 , to selected 3516
Changed the definition of groups completely.
The former version is awkward for defining specific groups like
<Z, +> and is lack of generality since only ONE general group is
defined.
The current version adopts a parameter which makes it capable of
handling complicated situations.


Revision 3494 - (view) (download) (annotate) - [select for diffs]
Modified Thu Feb 7 23:19:33 2002 UTC (19 years, 5 months ago) by xiny
File length: 122272 byte(s)
Diff to previous 3484 , to selected 3516
Removed tactics "op_assoc1T", "op_assoc2T" (previously as comments),
and "id_elim2T".


Revision 3484 - (view) (download) (annotate) - [select for diffs]
Modified Wed Jan 30 00:36:09 2002 UTC (19 years, 5 months ago) by xiny
File length: 124393 byte(s)
Diff to previous 3463 , to selected 3516
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 3463 - (view) (download) (annotate) - [select for diffs]
Modified Sat Dec 8 03:17:49 2001 UTC (19 years, 7 months ago) by nogin
File length: 117380 byte(s)
Diff to previous 3405 , to selected 3516
Fixed bug #10 - now the term_match_table fall-back mechanism is more complete.
This broke couple of proofs, I fixed them.


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


Revision 3404 - (view) (download) (annotate) - [select for diffs]
Modified Sun Sep 23 07:25:28 2001 UTC (19 years, 10 months ago) by xiny
File length: 123630 byte(s)
Diff to previous 3379 , to selected 3516
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.


Revision 3379 - (view) (download) (annotate) - [select for diffs]
Added Fri Sep 14 07:00:13 2001 UTC (19 years, 10 months ago) by xiny
File length: 103995 byte(s)
Diff to selected 3516
Definition of algebraic group.


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