/[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 3560 by xiny, Tue Apr 2 08:18:40 2002 UTC revision 3561 by xiny, Wed Apr 3 05:29:19 2002 UTC
# Line 32  Line 32 
32     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)}}}
33    
34  rewrite unfold_cyc_subg : cyc_subg{'s; 'g; 'a} <-->  rewrite unfold_cyc_subg : cyc_subg{'s; 'g; 'a} <-->
35     (group{'s} & group{'g} & mem{'a; car{'g}} & equal{car{'s}; collect{int; x. power{'g; 'a; 'x}}} & (all a: set. all b:set. (mem{'a; car{'s}} => mem{'b; car{'s}} => equal{op{'s; 'a; 'b}; op{'g; 'a; 'b}})) & (all a: set. all b: set. (equiv{car{'s}; eqG{'s}; 'a; 'b} => equiv{car{'g}; eqG{'g}; 'a; 'b})))     (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})))
36    
37  topval fold_power : conv  topval fold_power : conv
38  topval fold_cyc_subg : conv  topval fold_cyc_subg : conv

Legend:
Removed from v.3560  
changed lines
  Added in v.3561

  ViewVC Help
Powered by ViewVC 1.1.26