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

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

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 34  Line 34 
34     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)}}}
35    
36  prim_rw unfold_cyc_subg : cyc_subg{'s; 'g; 'a} <-->  prim_rw unfold_cyc_subg : cyc_subg{'s; 'g; 'a} <-->
37     (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})))
38    
39  let fold_power = makeFoldC << power{'g; 'z; 'n} >> unfold_power  let fold_power = makeFoldC << power{'g; 'z; 'n} >> unfold_power
40  let fold_cyc_subg = makeFoldC << cyc_subg{'s; 'g; 'a} >> unfold_cyc_subg  let fold_cyc_subg = makeFoldC << cyc_subg{'s; 'g; 'a} >> unfold_cyc_subg
# Line 128  Line 128 
128     sequent [squash] { 'H >- isset{'a} } -->     sequent [squash] { 'H >- isset{'a} } -->
129     sequent ['ext] { 'H >- mem{'a; car{'g}} } -->     sequent ['ext] { 'H >- mem{'a; car{'g}} } -->
130     sequent ['ext] { 'H >- equal{car{'s}; collect{int; x. power{'g; 'a; 'x}}} } -->     sequent ['ext] { 'H >- equal{car{'s}; collect{int; x. power{'g; 'a; 'x}}} } -->
131     sequent ['ext] { 'H; a: set; b: set; x: mem{'a; car{'s}}; y: mem{'b; car{'s}} >- equal{op{'s; 'a; 'b}; op{'g; 'a; 'b}} } -->     sequent ['ext] { 'H; b: set; c: set; x: mem{'b; car{'s}}; y: mem{'c; car{'s}} >- equiv{car{'s}; eqG{'s}; op{'s; 'b; 'c}; op{'g; 'b; 'c}} } -->
132     sequent ['ext] { 'H; a: set; b: set; x: equiv{car{'s}; eqG{'s}; 'a; 'b} >- equiv{car{'g}; eqG{'g}; 'a; 'b} } -->     sequent ['ext] { 'H; d: set; e: set; u: equiv{car{'s}; eqG{'s}; 'd; 'e} >- equiv{car{'g}; eqG{'g}; 'd; 'e} } -->
133       sequent ['ext] { 'H; p: set; q: set; x: mem{'p; car{'s}}; y: mem{'q; car{'s}}; v: equiv{car{'g}; eqG{'g}; 'p; 'q} >- equiv{car{'s}; eqG{'s}; 'p; 'q} } -->
134     sequent ['ext] { 'H >- cyc_subg{'s; 'g; 'a} }     sequent ['ext] { 'H >- cyc_subg{'s; 'g; 'a} }
135    
136  interactive cyc_subg_subgroup 'H 'a :  interactive cycsubg_subgroup 'H 'a :
137     sequent [squash] { 'H >- 'g IN label } -->     sequent [squash] { 'H >- 'g IN label } -->
138     sequent [squash] { 'H >- 's IN label } -->     sequent [squash] { 'H >- 's IN label } -->
139     sequent ['ext] { 'H >- group{'g} } -->     sequent ['ext] { 'H >- group{'g} } -->
# Line 143  Line 144 
144     sequent ['ext] { 'H >- subgroup{'s; 'g} }     sequent ['ext] { 'H >- subgroup{'s; 'g} }
145    
146  let cycsubgSubgroupT t p =  let cycsubgSubgroupT t p =
147     cyc_subg_subgroup (hyp_count_addr p) t p     cycsubg_subgroup (hyp_count_addr p) t p

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

  ViewVC Help
Powered by ViewVC 1.1.26