Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2003-03-06 02:45:27 -0800 (Thu, 06 Mar 2003)
Revision: 4158
Log message:

      - Proved that for if there is a positive number x such that P[x], then there
        is a smallest positive number k such that P[k], as long as P[y] is well-formed
        and decidable for any integer y. (rule "smallest_positive")
      - Stated as a separate rule that for any integer k>0 and m, there exists
        integer r>=0 and q such that m=k*q+r. Not proved yet. (rule "int_div_rem")
      - Now "Every non-trivial subgroup of a cyclic group is cyclic" "should" be
        provable other than "type"{(y^a)_g in s.car} is needed for y in g.car and
        a in int, which is not true. Have I made any mistake along the way or is
        this theorem just incorrect here?! (see "/itt_cyclic_group/subg_cycGroup/1/1"
        for example)
        I'll move "If S is a non-trivial subgroup of a cyclic group G generated by b,
        there exists a positive number k such that (b^k)_g in S" as a separate rule.
      

Changes	Path
+80 -51	metaprl/theories/itt/itt_cyclic_group.ml
+2 -0	metaprl/theories/itt/itt_cyclic_group.mli
+6389 -2330	metaprl/theories/itt/itt_cyclic_group.prla