/[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 3556 by xiny, Mon Mar 11 10:03:46 2002 UTC revision 3557 by xiny, Tue Apr 2 08:18:40 2002 UTC
# Line 26  Line 26 
26  open Base_auto_tactic  open Base_auto_tactic
27    
28  declare power{'g; 'z; 'n}  declare power{'g; 'z; 'n}
29  declare cyc_subg{'g; 's; 'a}  declare cyc_subg{'s; 'g; 'a}
30    
31  rewrite unfold_power : power{'g; 'z; 'n} <-->  rewrite unfold_power : power{'g; 'z; 'n} <-->
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{'g; 's; 'a} <-->  rewrite unfold_cyc_subg : cyc_subg{'s; 'g; 'a} <-->
35     (group{'g} & group{'s} & 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}})))     (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})))
   
 prec prec_power  
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.3556  
changed lines
  Added in v.3557

  ViewVC Help
Powered by ViewVC 1.1.26