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

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

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

revision 3569 by xiny, Wed Apr 3 05:27:01 2002 UTC revision 3570 by xiny, Tue Apr 9 05:59:41 2002 UTC
# Line 2  Line 2 
2  include Czf_itt_eq  include Czf_itt_eq
3  include Czf_itt_subset  include Czf_itt_subset
4  include Czf_itt_isect  include Czf_itt_isect
5    include Czf_itt_group_bvd
6    
7  open Refiner.Refiner  open Refiner.Refiner
8  open Refiner.Refiner.Term  open Refiner.Refiner.Term
# Line 22  Line 23 
23  declare subgroup{'s; 'g}  declare subgroup{'s; 'g}
24    
25  rewrite unfold_subgroup : subgroup{'s; 'g} <-->  rewrite unfold_subgroup : subgroup{'s; 'g} <-->
26     (group{'s} & group{'g} & subset{car{'s}; car{'g}} & (all a: set. all b: set. (mem{'a; car{'s}} => mem{'b; car{'s}} => equiv{car{'s}; eqG{'s}; 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})) & (all a: set. all b: set. (mem{'a; car{'s}} => mem{'b; car{'s}} => equiv{car{'g}; eqG{'g}; 'a; 'b} => equiv{car{'s}; eqG{'s}; 'a; 'b})))     (group{'s} & group{'g} & subset{car{'s}; car{'g}} & group_bvd{'s; 'g; car{'s}})
27    
28  topval subgroupIsectT: term -> term -> tactic  topval subgroupIsectT: term -> term -> tactic

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

  ViewVC Help
Powered by ViewVC 1.1.26