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

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

Parent Directory Parent Directory | Revision Log Revision Log | View Patch Patch

revision 3569 by xiny, Wed Apr 3 05:29:19 2002 UTC revision 3570 by xiny, Tue Apr 9 05:59:41 2002 UTC
# Line 1  Line 1 
1  include Czf_itt_group  include Czf_itt_group
2    include Czf_itt_group_bvd
3  include Czf_itt_subgroup  include Czf_itt_subgroup
4  include Itt_int_base  include Itt_int_base
5    
# Line 32  Line 33 
33     ind{'n; i, j. op{'g; inv{'g; 'z}; power{'g; 'z; ('n +@ 1)}}; id{'g}; k, l. op{'g; 'z; power{'g; 'z; ('n -@ 1)}}}     ind{'n; i, j. op{'g; inv{'g; 'z}; power{'g; 'z; ('n +@ 1)}}; id{'g}; k, l. op{'g; 'z; power{'g; 'z; ('n -@ 1)}}}
34    
35  rewrite unfold_cyc_subg : cyc_subg{'s; 'g; 'a} <-->  rewrite unfold_cyc_subg : cyc_subg{'s; 'g; 'a} <-->
36     (group{'s} & group{'g} & mem{'a; car{'g}} & equal{car{'s}; collect{int; x. power{'g; 'a; 'x}}} & (all b: set. all c: set. (mem{'b; car{'s}} => mem{'c; car{'s}} => equiv{car{'s}; eqG{'s}; op{'s; 'b; 'c}; op{'g; 'b; 'c}})) & (all b: set. all c: set. (equiv{car{'s}; eqG{'s}; 'b; 'c} => equiv{car{'g}; eqG{'g}; 'b; 'c})) & (all b: set. all c:set. (mem{'b; car{'s}} => mem{'c; car{'s}} => equiv{car{'g}; eqG{'g}; 'b; 'c} => equiv{car{'s}; eqG{'s}; 'b; 'c})))     (group{'s} & group{'g} & mem{'a; car{'g}} & group_bvd{'s; 'g; collect{int; x. power{'g; 'a; 'x}}})
37    
38  topval fold_power : conv  topval fold_power : conv
39  topval fold_cyc_subg : conv  topval fold_cyc_subg : conv

Legend:
Removed from v.3569  
changed lines
  Added in v.3570

  ViewVC Help
Powered by ViewVC 1.1.26