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

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

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

revision 3552 by xiny, Mon Mar 11 09:57:39 2002 UTC revision 3553 by xiny, Tue Apr 2 07:45:26 2002 UTC
# Line 1  Line 1 
1  include Itt_record_label0  include Itt_record_label0
 include Czf_itt_set  
2  include Czf_itt_member  include Czf_itt_member
3  include Czf_itt_eq  include Czf_itt_eq
4  include Czf_itt_dall  include Czf_itt_dall
# Line 30  Line 29 
29  open Base_auto_tactic  open Base_auto_tactic
30    
31  declare group{'g}  declare group{'g}
32  declare car{'g}   (* The "carrier" set for the group *)  declare car{'g}         (* The "carrier" set for the group *)
33    declare eqG{'g}         (* The equivalence relation for the group *)
34    (* declare eqG{'g; 'a; 'b} (* a and b are equivalent in the group *) *)
35  declare op{'g; 'a; 'b}  declare op{'g; 'a; 'b}
36  declare id{'g}  declare id{'g}
37  declare inv{'g; 'a}  declare inv{'g; 'a}
38    (*
39    prim_rw unfold_eqG : eqG{'g; 'a; 'b} <-->
40       equiv{car{'g}; eqG{'g}; 'a; 'b}
41    
42  prec prec_op  let fold_eqG = makeFoldC << eqG{'g; 'a; 'b} >> unfold_eqG
43    *)
44  dform group_df : except_mode[src] :: group{'g} =  dform group_df : except_mode[src] :: group{'g} =
45     slot{'g} `" group"     slot{'g} `" group"
46    
47  dform car_df : except_mode[src] :: car{'g} =  dform car_df : except_mode[src] :: car{'g} =
48     `"car(" slot{'g} `")"     `"car(" slot{'g} `")"
49    
50    dform eqG_df1 : except_mode[src] :: eqG{'g} =
51       `"eqG(" slot{'g} `")"
52    
53    (*dform eqG_df2 : except_mode[src] :: eqG{'g; 'a; 'b} =
54       `"eqG(" slot{'g} `"; " slot{'a}  `"; " slot{'b} `")"
55    *)
56  dform id_df : except_mode[src] :: id{'g} =  dform id_df : except_mode[src] :: id{'g} =
57     `"id(" slot{'g} `")"     `"id(" slot{'g} `")"
58    
59  dform op_df : parens :: "prec"[prec_op] :: except_mode[src] :: op{'g; 'a; 'b} =  dform op_df : parens :: except_mode[src] :: op{'g; 'a; 'b} =
60     `"op(" slot{'g} `"; " slot{'a}  `"; " slot{'b} `")"     `"op(" slot{'g} `"; " slot{'a}  `"; " slot{'b} `")"
61    
62  dform inv_df : parens :: except_mode[src] :: inv{'g; 'a} =  dform inv_df : parens :: except_mode[src] :: inv{'g; 'a} =
# Line 61  Line 71 
71    
72  interactive car_wf {| intro[] |} 'H :  interactive car_wf {| intro[] |} 'H :
73     sequent [squash] { 'H >- 'g IN label } -->     sequent [squash] { 'H >- 'g IN label } -->
    sequent ['ext] { 'H >- group{'g} } -->  
74     sequent ['ext] { 'H >- isset{car{'g}} }     sequent ['ext] { 'H >- isset{car{'g}} }
75    
76  interactive op_wf1 {| intro[] |} 'H :  interactive eqG_wf1 {| intro[] |} 'H :
77       sequent [squash] { 'H >- 'g IN label } -->
78       sequent ['ext] { 'H >- isset{eqG{'g}} }
79    
80    interactive eqG_wf2 {| intro[] |} 'H :
81     sequent [squash] { 'H >- 'g IN label } -->     sequent [squash] { 'H >- 'g IN label } -->
82     sequent ['ext] { 'H >- group{'g} } -->     sequent ['ext] { 'H >- group{'g} } -->
83       sequent ['ext] { 'H >- equiv{car{'g}; eqG{'g}} }
84    
85    (*interactive eqG_elem_wf1 {| intro[] |} 'H :
86       sequent [squash] { 'H >- 'g IN label } -->
87       sequent [squash] { 'H >- isset{'a} } -->
88       sequent [squash] { 'H >- isset{'b} } -->
89       sequent ['ext] { 'H >- "type"{equiv{car{'g}; eqG{'g}; 'a; 'b}} }
90    *)
91    (*interactive eqG_elem_wf2 {| intro[] |} 'H :
92       sequent [squash] { 'H >- 'g IN label } -->
93       sequent ['ext] { 'H >- group{'g} } -->
94       sequent [squash] { 'H >- isset{'a} } -->
95       sequent [squash] { 'H >- isset{'b} } -->
96       sequent ['ext] { 'H >- mem{'a; car{'g}} } -->
97       sequent ['ext] { 'H >- mem{'b; car{'g}} } -->
98       sequent ['ext] { 'H >- mem{pair{'a; 'b}; eqG{'g}} } -->
99       sequent ['ext] { 'H >- equiv{car{'g}; eqG{'g}; 'a; 'b} }
100    *)
101    interactive op_wf {| intro[] |} 'H :
102       sequent [squash] { 'H >- 'g IN label } -->
103     sequent [squash] { 'H >- isset{'s1} } -->     sequent [squash] { 'H >- isset{'s1} } -->
104     sequent [squash] { 'H >- isset{'s2} } -->     sequent [squash] { 'H >- isset{'s2} } -->
105     sequent ['ext] { 'H >- isset{op{'g; 's1; 's2}} }     sequent ['ext] { 'H >- isset{op{'g; 's1; 's2}} }
106    
107  interactive op_wf2 {| intro[] |} 'H :  interactive op_closure {| intro[] |} 'H :
108     sequent [squash] { 'H >- isset{'s1} } -->     sequent [squash] { 'H >- isset{'s1} } -->
109     sequent [squash] { 'H >- isset{'s2} } -->     sequent [squash] { 'H >- isset{'s2} } -->
110     sequent [squash] { 'H >- 'g IN label } -->     sequent [squash] { 'H >- 'g IN label } -->
# Line 80  Line 113 
113     sequent ['ext] { 'H >- mem{'s2; car{'g}} } -->     sequent ['ext] { 'H >- mem{'s2; car{'g}} } -->
114     sequent ['ext] { 'H >- mem{op{'g; 's1; 's2}; car{'g}} }     sequent ['ext] { 'H >- mem{op{'g; 's1; 's2}; car{'g}} }
115    
116  interactive op_equiv1 {| intro[] |} 'H :  interactive op_eqG1 {| intro[] |} 'H :
117     sequent [squash] { 'H >- isset{'s1} } -->     sequent [squash] { 'H >- isset{'s1} } -->
118     sequent [squash] { 'H >- isset{'s2} } -->     sequent [squash] { 'H >- isset{'s2} } -->
119     sequent [squash] { 'H >- isset{'s3} } -->     sequent [squash] { 'H >- isset{'s3} } -->
    sequent [squash] { 'H >- isset{'R} } -->  
120     sequent [squash] { 'H >- 'g IN label } -->     sequent [squash] { 'H >- 'g IN label } -->
121     sequent ['ext] { 'H >- group{'g} } -->     sequent ['ext] { 'H >- group{'g} } -->
    sequent ['ext] { 'H >- equiv{car{'g}; 'R} } -->  
122     sequent ['ext] { 'H >- mem{'s1; car{'g}} } -->     sequent ['ext] { 'H >- mem{'s1; car{'g}} } -->
123     sequent ['ext] { 'H >- mem{'s2; car{'g}} } -->     sequent ['ext] { 'H >- mem{'s2; car{'g}} } -->
124     sequent ['ext] { 'H >- mem{'s3; car{'g}} } -->     sequent ['ext] { 'H >- mem{'s3; car{'g}} } -->
125     sequent ['ext] { 'H >- equiv{car{'g}; 'R; 's1; 's2} } -->     sequent ['ext] { 'H >- equiv{car{'g}; eqG{'g}; 's1; 's2} } -->
126     sequent ['ext] { 'H >- equiv{car{'g}; 'R; op{'g; 's3; 's1}; op{'g; 's3; 's2}} }     sequent ['ext] { 'H >- equiv{car{'g}; eqG{'g}; op{'g; 's3; 's1}; op{'g; 's3; 's2}} }
127    
128  interactive op_equiv2 {| intro[] |} 'H :  interactive op_eqG2 {| intro[] |} 'H :
129     sequent [squash] { 'H >- isset{'s1} } -->     sequent [squash] { 'H >- isset{'s1} } -->
130     sequent [squash] { 'H >- isset{'s2} } -->     sequent [squash] { 'H >- isset{'s2} } -->
131     sequent [squash] { 'H >- isset{'s3} } -->     sequent [squash] { 'H >- isset{'s3} } -->
    sequent [squash] { 'H >- isset{'R} } -->  
132     sequent [squash] { 'H >- 'g IN label } -->     sequent [squash] { 'H >- 'g IN label } -->
133     sequent ['ext] { 'H >- group{'g} } -->     sequent ['ext] { 'H >- group{'g} } -->
    sequent ['ext] { 'H >- equiv{car{'g}; 'R} } -->  
134     sequent ['ext] { 'H >- mem{'s1; car{'g}} } -->     sequent ['ext] { 'H >- mem{'s1; car{'g}} } -->
135     sequent ['ext] { 'H >- mem{'s2; car{'g}} } -->     sequent ['ext] { 'H >- mem{'s2; car{'g}} } -->
136     sequent ['ext] { 'H >- mem{'s3; car{'g}} } -->     sequent ['ext] { 'H >- mem{'s3; car{'g}} } -->
137     sequent ['ext] { 'H >- equiv{car{'g}; 'R; 's1; 's2} } -->     sequent ['ext] { 'H >- equiv{car{'g}; eqG{'g}; 's1; 's2} } -->
138     sequent ['ext] { 'H >- equiv{car{'g}; 'R; op{'g; 's1; 's3}; op{'g; 's2; 's3}} }     sequent ['ext] { 'H >- equiv{car{'g}; eqG{'g}; op{'g; 's1; 's3}; op{'g; 's2; 's3}} }
139    
140  interactive op_equiv_fun1 {| intro[] |} 'H :  interactive op_eqG_fun1 {| intro[] |} 'H :
141     sequent [squash] { 'H >- isset{'s} } -->     sequent [squash] { 'H >- isset{'s} } -->
    sequent [squash] { 'H >- isset{'R} } -->  
142     sequent [squash] { 'H >- 'g IN label } -->     sequent [squash] { 'H >- 'g IN label } -->
143     sequent ['ext] { 'H >- group{'g} } -->     sequent ['ext] { 'H >- group{'g} } -->
144     sequent ['ext] { 'H >- equiv{car{'g}; 'R} } -->     sequent ['ext] { 'H >- equiv_fun_set{car{'g}; eqG{'g}; z. op{'g; 'z; 's}} }
    sequent ['ext] { 'H >- equiv_fun_set{car{'g}; 'R; z. op{'g; 'z; 's}} }  
145    
146  interactive op_equiv_fun2 {| intro[] |} 'H :  interactive op_equiv_fun2 {| intro[] |} 'H :
147     sequent [squash] { 'H >- isset{'s} } -->     sequent [squash] { 'H >- isset{'s} } -->
    sequent [squash] { 'H >- isset{'R} } -->  
148     sequent [squash] { 'H >- 'g IN label } -->     sequent [squash] { 'H >- 'g IN label } -->
149     sequent ['ext] { 'H >- group{'g} } -->     sequent ['ext] { 'H >- group{'g} } -->
150     sequent ['ext] { 'H >- equiv{car{'g}; 'R} } -->     sequent ['ext] { 'H >- equiv_fun_set{car{'g}; eqG{'g}; z. op{'g; 's; 'z}} }
    sequent ['ext] { 'H >- equiv_fun_set{car{'g}; 'R; z. op{'g; 's; 'z}} }  
151    
152  interactive op_eq_fun1 {| intro[] |} 'H :  interactive op_eq_fun1 {| intro[] |} 'H :
153     sequent [squash] { 'H >- isset{'s} } -->     sequent [squash] { 'H >- isset{'s} } -->
# Line 140  Line 165 
165     sequent [squash] { 'H >- isset{'s1} } -->     sequent [squash] { 'H >- isset{'s1} } -->
166     sequent [squash] { 'H >- isset{'s2} } -->     sequent [squash] { 'H >- isset{'s2} } -->
167     sequent [squash] { 'H >- isset{'s3} } -->     sequent [squash] { 'H >- isset{'s3} } -->
    sequent [squash] { 'H >- isset{'R} } -->  
168     sequent [squash] { 'H >- 'g IN label } -->     sequent [squash] { 'H >- 'g IN label } -->
169     sequent ['ext] { 'H >- group{'g} } -->     sequent ['ext] { 'H >- group{'g} } -->
    sequent ['ext] { 'H >- equiv{car{'g}; 'R} } -->  
170     sequent ['ext] { 'H >- mem{'s1; car{'g}} } -->     sequent ['ext] { 'H >- mem{'s1; car{'g}} } -->
171     sequent ['ext] { 'H >- mem{'s2; car{'g}} } -->     sequent ['ext] { 'H >- mem{'s2; car{'g}} } -->
172     sequent ['ext] { 'H >- mem{'s3; car{'g}} } -->     sequent ['ext] { 'H >- mem{'s3; car{'g}} } -->
173     sequent ['ext] { 'H >- equiv{car{'g}; 'R; op{'g; op{'g; 's1; 's2}; 's3}; op{'g; 's1; op{'g; 's2; 's3}}} }     sequent ['ext] { 'H >- equiv{car{'g}; eqG{'g}; op{'g; op{'g; 's1; 's2}; 's3}; op{'g; 's1; op{'g; 's2; 's3}}} }
174    
175  interactive op_assoc2 {| intro[] |} 'H :  interactive op_assoc2 {| intro[] |} 'H :
176     sequent [squash] { 'H >- isset{'s1} } -->     sequent [squash] { 'H >- isset{'s1} } -->
177     sequent [squash] { 'H >- isset{'s2} } -->     sequent [squash] { 'H >- isset{'s2} } -->
178     sequent [squash] { 'H >- isset{'s3} } -->     sequent [squash] { 'H >- isset{'s3} } -->
    sequent [squash] { 'H >- isset{'R} } -->  
179     sequent [squash] { 'H >- 'g IN label } -->     sequent [squash] { 'H >- 'g IN label } -->
180     sequent ['ext] { 'H >- group{'g} } -->     sequent ['ext] { 'H >- group{'g} } -->
    sequent ['ext] { 'H >- equiv{car{'g}; 'R} } -->  
181     sequent ['ext] { 'H >- mem{'s1; car{'g}} } -->     sequent ['ext] { 'H >- mem{'s1; car{'g}} } -->
182     sequent ['ext] { 'H >- mem{'s2; car{'g}} } -->     sequent ['ext] { 'H >- mem{'s2; car{'g}} } -->
183     sequent ['ext] { 'H >- mem{'s3; car{'g}} } -->     sequent ['ext] { 'H >- mem{'s3; car{'g}} } -->
184     sequent ['ext] { 'H >- equiv{car{'g}; 'R; op{'g; 's1; op{'g; 's2; 's3}}; op{'g; op{'g; 's1; 's2}; 's3}} }     sequent ['ext] { 'H >- equiv{car{'g}; eqG{'g}; op{'g; 's1; op{'g; 's2; 's3}}; op{'g; op{'g; 's1; 's2}; 's3}} }
185    
186  interactive id_wf1 {| intro [] |} 'H :  interactive id_wf1 {| intro [] |} 'H :
187     sequent [squash] { 'H >- 'g IN label } -->     sequent [squash] { 'H >- 'g IN label } -->
    sequent ['ext] { 'H >- group{'g} } -->  
188     sequent ['ext] { 'H >- isset{id{'g}} }     sequent ['ext] { 'H >- isset{id{'g}} }
189    
190  interactive id_wf2 {| intro[] |} 'H :  interactive id_wf2 {| intro[] |} 'H :
# Line 174  Line 194 
194    
195  interactive id_eq1 {| intro[] |} 'H :  interactive id_eq1 {| intro[] |} 'H :
196     sequent [squash] { 'H >- isset{'s} } -->     sequent [squash] { 'H >- isset{'s} } -->
    sequent [squash] { 'H >- isset{'R} } -->  
197     sequent [squash] { 'H >- 'g IN label } -->     sequent [squash] { 'H >- 'g IN label } -->
198     sequent ['ext] { 'H >- group{'g} } -->     sequent ['ext] { 'H >- group{'g} } -->
    sequent ['ext] { 'H >- equiv{car{'g}; 'R} } -->  
199     sequent ['ext] { 'H >- mem{'s; car{'g}} } -->     sequent ['ext] { 'H >- mem{'s; car{'g}} } -->
200     sequent ['ext] { 'H >- equiv{car{'g}; 'R; op{'g; id{'g}; 's}; 's} }     sequent ['ext] { 'H >- equiv{car{'g}; eqG{'g}; op{'g; id{'g}; 's}; 's} }
201    
202  interactive inv_wf1 {| intro[] |} 'H :  interactive inv_wf1 {| intro[] |} 'H :
203     sequent [squash] { 'H >- isset{'s1} } -->     sequent [squash] { 'H >- isset{'s1} } -->
204     sequent [squash] { 'H >- 'g IN label } -->     sequent [squash] { 'H >- 'g IN label } -->
    sequent ['ext] { 'H >- group{'g} } -->  
    sequent ['ext] { 'H >- mem{'s1; car{'g}} } -->  
205     sequent ['ext] { 'H >- isset{inv{'g; 's1}} }     sequent ['ext] { 'H >- isset{inv{'g; 's1}} }
206    
207  interactive inv_wf2 {| intro[] |} 'H :  interactive inv_wf2 {| intro[] |} 'H :
# Line 196  Line 212 
212     sequent ['ext] { 'H >- mem{inv{'g; 's1}; car{'g}} }     sequent ['ext] { 'H >- mem{inv{'g; 's1}; car{'g}} }
213    
214  interactive inv_equiv_fun1 {| intro[] |} 'H :  interactive inv_equiv_fun1 {| intro[] |} 'H :
    sequent [squash] { 'H >- isset{'R} } -->  
215     sequent [squash] { 'H >- 'g IN label } -->     sequent [squash] { 'H >- 'g IN label } -->
216     sequent ['ext] { 'H >- group{'g} } -->     sequent ['ext] { 'H >- group{'g} } -->
217     sequent ['ext] { 'H >- equiv{car{'g}; 'R} } -->     sequent ['ext] { 'H >- equiv_fun_set{car{'g}; eqG{'g}; z. inv{'g; 'z}} }
    sequent ['ext] { 'H >- equiv_fun_set{car{'g}; 'R; z. inv{'g; 'z}} }  
218    
219  interactive inv_eq_fun1 {| intro[] |} 'H :  interactive inv_eq_fun1 {| intro[] |} 'H :
220     sequent [squash] { 'H >- 'g IN label } -->     sequent [squash] { 'H >- 'g IN label } -->
# Line 209  Line 223 
223    
224  interactive inv_id1 {| intro[] |} 'H :  interactive inv_id1 {| intro[] |} 'H :
225     sequent [squash] { 'H >- isset{'s1} } -->     sequent [squash] { 'H >- isset{'s1} } -->
    sequent [squash] { 'H >- isset{'R} } -->  
226     sequent [squash] { 'H >- 'g IN label } -->     sequent [squash] { 'H >- 'g IN label } -->
227     sequent ['ext] { 'H >- group{'g} } -->     sequent ['ext] { 'H >- group{'g} } -->
    sequent ['ext] { 'H >- equiv{car{'g}; 'R} } -->  
228     sequent ['ext] { 'H >- mem{'s1; car{'g}} } -->     sequent ['ext] { 'H >- mem{'s1; car{'g}} } -->
229     sequent ['ext] { 'H >- equiv{car{'g}; 'R; op{'g; inv{'g; 's1}; 's1}; id{'g}} }     sequent ['ext] { 'H >- equiv{car{'g}; eqG{'g}; op{'g; inv{'g; 's1}; 's1}; id{'g}} }
230    
231  (*  (*
232   * lemmas   * lemmas
233   *)   *)
234  interactive id_judge_elim {| elim [] |} 'H 'J :  interactive id_judge_elim {| elim [] |} 'H 'J :
235     sequent [squash] { 'H; x: equiv{car{'g}; 'R; op{'g; 's; 's}; 's}; 'J['x] >- isset{'s} } -->     sequent [squash] { 'H; x: equiv{car{'g}; eqG{'g}; op{'g; 's; 's}; 's}; 'J['x] >- isset{'s} } -->
236     sequent [squash] { 'H; x: equiv{car{'g}; 'R; op{'g; 's; 's}; 's}; 'J['x] >- isset{'R} } -->     sequent [squash] { 'H; x: equiv{car{'g}; eqG{'g}; op{'g; 's; 's}; 's}; 'J['x] >- 'g IN label } -->
237     sequent [squash] { 'H; x: equiv{car{'g}; 'R; op{'g; 's; 's}; 's}; 'J['x] >- 'g IN label } -->     sequent ['ext] { 'H; x: equiv{car{'g}; eqG{'g}; op{'g; 's; 's}; 's}; 'J['x] >- group{'g} } -->
238     sequent ['ext] { 'H; x: equiv{car{'g}; 'R; op{'g; 's; 's}; 's}; 'J['x] >- group{'g} } -->     sequent ['ext] { 'H; x: equiv{car{'g}; eqG{'g}; op{'g; 's; 's}; 's}; 'J['x]; y: equiv{car{'g}; eqG{'g}; 's; id{'g}} >- 'C['x] } -->
239     sequent ['ext] { 'H; x: equiv{car{'g}; 'R; op{'g; 's; 's}; 's}; 'J['x] >- equiv{car{'g}; 'R} } -->     sequent ['ext] { 'H; x: equiv{car{'g}; eqG{'g}; op{'g; 's; 's}; 's}; 'J['x] >- 'C['x] }
    sequent ['ext] { 'H; x: equiv{car{'g}; 'R; op{'g; 's; 's}; 's}; 'J['x]; y: equiv{car{'g}; 'R; 's; id{'g}} >- 'C['x] } -->  
    sequent ['ext] { 'H; x: equiv{car{'g}; 'R; op{'g; 's; 's}; 's}; 'J['x] >- 'C['x] }  
240    
241  interactive inv_id2 {| intro[] |} 'H :  interactive inv_id2 {| intro[] |} 'H :
242     sequent [squash] { 'H >- isset{'s} } -->     sequent [squash] { 'H >- isset{'s} } -->
    sequent [squash] { 'H >- isset{'R} } -->  
243     sequent [squash] { 'H >- 'g IN label } -->     sequent [squash] { 'H >- 'g IN label } -->
244     sequent ['ext] { 'H >- group{'g} } -->     sequent ['ext] { 'H >- group{'g} } -->
    sequent ['ext] { 'H >- equiv{car{'g}; 'R} } -->  
245     sequent ['ext] { 'H >- mem{'s; car{'g}} } -->     sequent ['ext] { 'H >- mem{'s; car{'g}} } -->
246     sequent ['ext] { 'H >- equiv{car{'g}; 'R; op{'g; 's; inv{'g; 's}}; id{'g}} }     sequent ['ext] { 'H >- equiv{car{'g}; eqG{'g}; op{'g; 's; inv{'g; 's}}; id{'g}} }
247    
248  interactive id_eq2 {| intro[] |} 'H :  interactive id_eq2 {| intro[] |} 'H :
249     sequent [squash] { 'H >- isset{'s} } -->     sequent [squash] { 'H >- isset{'s} } -->
    sequent [squash] { 'H >- isset{'R} } -->  
250     sequent [squash] { 'H >- 'g IN label } -->     sequent [squash] { 'H >- 'g IN label } -->
251     sequent ['ext] { 'H >- group{'g} } -->     sequent ['ext] { 'H >- group{'g} } -->
    sequent ['ext] { 'H >- equiv{car{'g}; 'R} } -->  
252     sequent ['ext] { 'H >- mem{'s; car{'g}} } -->     sequent ['ext] { 'H >- mem{'s; car{'g}} } -->
253     sequent ['ext] { 'H >- equiv{car{'g}; 'R; op{'g; 's; id{'g}}; 's} }     sequent ['ext] { 'H >- equiv{car{'g}; eqG{'g}; op{'g; 's; id{'g}}; 's} }
254    
255  (*  (*
256   * theorems   * theorems
# Line 252  Line 258 
258  interactive equiv_op_fun1 {| intro[] |} 'H :  interactive equiv_op_fun1 {| intro[] |} 'H :
259     sequent [squash] { 'H >- isset{'a} } -->     sequent [squash] { 'H >- isset{'a} } -->
260     sequent [squash] { 'H >- isset{'b} } -->     sequent [squash] { 'H >- isset{'b} } -->
    sequent [squash] { 'H >- isset{'R} } -->  
261     sequent [squash] { 'H >- 'g IN label } -->     sequent [squash] { 'H >- 'g IN label } -->
262     sequent ['ext] { 'H >- group{'g} } -->     sequent ['ext] { 'H >- group{'g} } -->
    sequent ['ext] { 'H >- equiv{car{'g}; 'R} } -->  
263     sequent ['ext] { 'H >- mem{'a; car{'g}} } -->     sequent ['ext] { 'H >- mem{'a; car{'g}} } -->
264     sequent ['ext] { 'H >- mem{'b; car{'g}} } -->     sequent ['ext] { 'H >- mem{'b; car{'g}} } -->
265     sequent ['ext] { 'H >- equiv_fun_prop{car{'g}; 'R; z. equiv{car{'g}; 'R; op{'g; 'z; 'a}; op{'g; 'z; 'b}}} }     sequent ['ext] { 'H >- equiv_fun_prop{car{'g}; eqG{'g}; z. equiv{car{'g}; eqG{'g}; op{'g; 'z; 'a}; op{'g; 'z; 'b}}} }
266    
267  interactive equiv_op_fun2 {| intro[] |} 'H :  interactive equiv_op_fun2 {| intro[] |} 'H :
268     sequent [squash] { 'H >- isset{'a} } -->     sequent [squash] { 'H >- isset{'a} } -->
269     sequent [squash] { 'H >- isset{'b} } -->     sequent [squash] { 'H >- isset{'b} } -->
    sequent [squash] { 'H >- isset{'R} } -->  
270     sequent [squash] { 'H >- 'g IN label } -->     sequent [squash] { 'H >- 'g IN label } -->
271     sequent ['ext] { 'H >- group{'g} } -->     sequent ['ext] { 'H >- group{'g} } -->
    sequent ['ext] { 'H >- equiv{car{'g}; 'R} } -->  
272     sequent ['ext] { 'H >- mem{'a; car{'g}} } -->     sequent ['ext] { 'H >- mem{'a; car{'g}} } -->
273     sequent ['ext] { 'H >- mem{'b; car{'g}} } -->     sequent ['ext] { 'H >- mem{'b; car{'g}} } -->
274     sequent ['ext] { 'H >- equiv_fun_prop{car{'g}; 'R; z. equiv{car{'g}; 'R; op{'g; 'a; 'z}; op{'g; 'b; 'z}}} }     sequent ['ext] { 'H >- equiv_fun_prop{car{'g}; eqG{'g}; z. equiv{car{'g}; eqG{'g}; op{'g; 'a; 'z}; op{'g; 'b; 'z}}} }
275    
276  (* Cancellation: a * b = a * c => b = c *)  (* Cancellation: a * b = a * c => b = c *)
277  interactive cancel1 (*{| elim [] |}*) 'H 'J :  interactive cancel1 (*{| elim [] |}*) 'H 'J :
278     sequent [squash] { 'H; x: equiv{car{'g}; 'R; op{'g; 's1; 's2}; op{'g; 's1; 's3}}; 'J['x] >- isset{'s1} } -->     sequent [squash] { 'H; x: equiv{car{'g}; eqG{'g}; op{'g; 's1; 's2}; op{'g; 's1; 's3}}; 'J['x] >- isset{'s1} } -->
279     sequent [squash] { 'H; x: equiv{car{'g}; 'R; op{'g; 's1; 's2}; op{'g; 's1; 's3}}; 'J['x] >- isset{'s2} } -->     sequent [squash] { 'H; x: equiv{car{'g}; eqG{'g}; op{'g; 's1; 's2}; op{'g; 's1; 's3}}; 'J['x] >- isset{'s2} } -->
280     sequent [squash] { 'H; x: equiv{car{'g}; 'R; op{'g; 's1; 's2}; op{'g; 's1; 's3}}; 'J['x] >- isset{'s3} } -->     sequent [squash] { 'H; x: equiv{car{'g}; eqG{'g}; op{'g; 's1; 's2}; op{'g; 's1; 's3}}; 'J['x] >- isset{'s3} } -->
281     sequent [squash] { 'H; x: equiv{car{'g}; 'R; op{'g; 's1; 's2}; op{'g; 's1; 's3}}; 'J['x] >- isset{'R} } -->     sequent [squash] { 'H; x: equiv{car{'g}; eqG{'g}; op{'g; 's1; 's2}; op{'g; 's1; 's3}}; 'J['x] >- 'g IN label } -->
282     sequent [squash] { 'H; x: equiv{car{'g}; 'R; op{'g; 's1; 's2}; op{'g; 's1; 's3}}; 'J['x] >- 'g IN label } -->     sequent ['ext] { 'H; x: equiv{car{'g}; eqG{'g}; op{'g; 's1; 's2}; op{'g; 's1; 's3}}; 'J['x] >- group{'g} } -->
283     sequent ['ext] { 'H; x: equiv{car{'g}; 'R; op{'g; 's1; 's2}; op{'g; 's1; 's3}}; 'J['x] >- group{'g} } -->     sequent ['ext] { 'H; x: equiv{car{'g}; eqG{'g}; op{'g; 's1; 's2}; op{'g; 's1; 's3}}; 'J['x] >- mem{'s1; car{'g}} } -->
284     sequent ['ext] { 'H; x: equiv{car{'g}; 'R; op{'g; 's1; 's2}; op{'g; 's1; 's3}}; 'J['x] >- equiv{car{'g}; 'R} } -->     sequent ['ext] { 'H; x: equiv{car{'g}; eqG{'g}; op{'g; 's1; 's2}; op{'g; 's1; 's3}}; 'J['x] >- mem{'s2; car{'g}} } -->
285     sequent ['ext] { 'H; x: equiv{car{'g}; 'R; op{'g; 's1; 's2}; op{'g; 's1; 's3}}; 'J['x] >- mem{'s1; car{'g}} } -->     sequent ['ext] { 'H; x: equiv{car{'g}; eqG{'g}; op{'g; 's1; 's2}; op{'g; 's1; 's3}}; 'J['x] >- mem{'s3; car{'g}} } -->
286     sequent ['ext] { 'H; x: equiv{car{'g}; 'R; op{'g; 's1; 's2}; op{'g; 's1; 's3}}; 'J['x] >- mem{'s2; car{'g}} } -->     sequent ['ext] { 'H; x: equiv{car{'g}; eqG{'g}; op{'g; 's1; 's2}; op{'g; 's1; 's3}}; 'J['x] >- equiv{car{'g}; eqG{'g}; 's2; 's3} }
    sequent ['ext] { 'H; x: equiv{car{'g}; 'R; op{'g; 's1; 's2}; op{'g; 's1; 's3}}; 'J['x] >- mem{'s3; car{'g}} } -->  
    sequent ['ext] { 'H; x: equiv{car{'g}; 'R; op{'g; 's1; 's2}; op{'g; 's1; 's3}}; 'J['x] >- equiv{car{'g}; 'R; 's2; 's3} }  
287    
288  (* Cancellation: b * a = c * a => b = c *)  (* Cancellation: b * a = c * a => b = c *)
289  interactive cancel2 (*{| elim [] |}*) 'H 'J :  interactive cancel2 (*{| elim [] |}*) 'H 'J :
290     sequent [squash] { 'H; x: equiv{car{'g}; 'R; op{'g; 's1; 's3}; op{'g; 's2; 's3}}; 'J['x] >- isset{'s1} } -->     sequent [squash] { 'H; x: equiv{car{'g}; eqG{'g}; op{'g; 's1; 's3}; op{'g; 's2; 's3}}; 'J['x] >- isset{'s1} } -->
291     sequent [squash] { 'H; x: equiv{car{'g}; 'R; op{'g; 's1; 's3}; op{'g; 's2; 's3}}; 'J['x] >- isset{'s2} } -->     sequent [squash] { 'H; x: equiv{car{'g}; eqG{'g}; op{'g; 's1; 's3}; op{'g; 's2; 's3}}; 'J['x] >- isset{'s2} } -->
292     sequent [squash] { 'H; x: equiv{car{'g}; 'R; op{'g; 's1; 's3}; op{'g; 's2; 's3}}; 'J['x] >- isset{'s3} } -->     sequent [squash] { 'H; x: equiv{car{'g}; eqG{'g}; op{'g; 's1; 's3}; op{'g; 's2; 's3}}; 'J['x] >- isset{'s3} } -->
293     sequent [squash] { 'H; x: equiv{car{'g}; 'R; op{'g; 's1; 's3}; op{'g; 's2; 's3}}; 'J['x] >- isset{'R} } -->     sequent [squash] { 'H; x: equiv{car{'g}; eqG{'g}; op{'g; 's1; 's3}; op{'g; 's2; 's3}}; 'J['x] >- 'g IN label } -->
294     sequent [squash] { 'H; x: equiv{car{'g}; 'R; op{'g; 's1; 's3}; op{'g; 's2; 's3}}; 'J['x] >- 'g IN label } -->     sequent ['ext] { 'H; x: equiv{car{'g}; eqG{'g}; op{'g; 's1; 's3}; op{'g; 's2; 's3}}; 'J['x] >- group{'g} } -->
295     sequent ['ext] { 'H; x: equiv{car{'g}; 'R; op{'g; 's1; 's3}; op{'g; 's2; 's3}}; 'J['x] >- group{'g} } -->     sequent ['ext] { 'H; x: equiv{car{'g}; eqG{'g}; op{'g; 's1; 's3}; op{'g; 's2; 's3}}; 'J['x] >- mem{'s1; car{'g}} } -->
296     sequent ['ext] { 'H; x: equiv{car{'g}; 'R; op{'g; 's1; 's3}; op{'g; 's2; 's3}}; 'J['x] >- equiv{car{'g}; 'R} } -->     sequent ['ext] { 'H; x: equiv{car{'g}; eqG{'g}; op{'g; 's1; 's3}; op{'g; 's2; 's3}}; 'J['x] >- mem{'s2; car{'g}} } -->
297     sequent ['ext] { 'H; x: equiv{car{'g}; 'R; op{'g; 's1; 's3}; op{'g; 's2; 's3}}; 'J['x] >- mem{'s1; car{'g}} } -->     sequent ['ext] { 'H; x: equiv{car{'g}; eqG{'g}; op{'g; 's1; 's3}; op{'g; 's2; 's3}}; 'J['x] >- mem{'s3; car{'g}} } -->
298     sequent ['ext] { 'H; x: equiv{car{'g}; 'R; op{'g; 's1; 's3}; op{'g; 's2; 's3}}; 'J['x] >- mem{'s2; car{'g}} } -->     sequent ['ext] { 'H; x: equiv{car{'g}; eqG{'g}; op{'g; 's1; 's3}; op{'g; 's2; 's3}}; 'J['x] >- equiv{car{'g}; eqG{'g}; 's1; 's2} }
    sequent ['ext] { 'H; x: equiv{car{'g}; 'R; op{'g; 's1; 's3}; op{'g; 's2; 's3}}; 'J['x] >- mem{'s3; car{'g}} } -->  
    sequent ['ext] { 'H; x: equiv{car{'g}; 'R; op{'g; 's1; 's3}; op{'g; 's2; 's3}}; 'J['x] >- equiv{car{'g}; 'R; 's1; 's2} }  
299    
300  let groupCancelLeftT i p =  let groupCancelLeftT i p =
301     let j, k = Sequent.hyp_indices p i in     let j, k = Sequent.hyp_indices p i in
# Line 308  Line 306 
306        cancel2 j k p        cancel2 j k p
307    
308  (* Unique Id *)  (* Unique Id *)
309  interactive unique_id1 {| intro [] |} 'H :  interactive unique_id1 'H :
310     sequent [squash] { 'H >- isset{'e2} } -->     sequent [squash] { 'H >- isset{'e2} } -->
    sequent [squash] { 'H >- isset{'R} } -->  
311     sequent [squash] { 'H >- 'g IN label } -->     sequent [squash] { 'H >- 'g IN label } -->
312     sequent ['ext] { 'H >- group{'g} } -->     sequent ['ext] { 'H >- group{'g} } -->
    sequent ['ext] { 'H >- equiv{car{'g}; 'R} } -->  
313     sequent ['ext] { 'H >- mem{'e2; car{'g}} } -->     sequent ['ext] { 'H >- mem{'e2; car{'g}} } -->
314     sequent ['ext] { 'H >- "dall"{car{'g}; s. equiv{car{'g}; 'R; op{'g; 'e2; 's}; 's}} } -->     sequent ['ext] { 'H >- "dall"{car{'g}; s. equiv{car{'g}; eqG{'g}; op{'g; 'e2; 's}; 's}} } -->
315     sequent ['ext] { 'H >- equiv{car{'g}; 'R; 'e2; id{'g}} }     sequent ['ext] { 'H >- equiv{car{'g}; eqG{'g}; 'e2; id{'g}} }
316    
317  interactive unique_id2 {| intro [] |} 'H :  interactive unique_id2 'H :
318     sequent [squash] { 'H >- isset{'e2} } -->     sequent [squash] { 'H >- isset{'e2} } -->
    sequent [squash] { 'H >- isset{'R} } -->  
319     sequent [squash] { 'H >- 'g IN label } -->     sequent [squash] { 'H >- 'g IN label } -->
320     sequent ['ext] { 'H >- group{'g} } -->     sequent ['ext] { 'H >- group{'g} } -->
    sequent ['ext] { 'H >- equiv{car{'g}; 'R} } -->  
321     sequent ['ext] { 'H >- mem{'e2; car{'g}} } -->     sequent ['ext] { 'H >- mem{'e2; car{'g}} } -->
322     sequent ['ext] { 'H >- "dall"{car{'g}; s. equiv{car{'g}; 'R; op{'g; 's; 'e2}; 's}} } -->     sequent ['ext] { 'H >- "dall"{car{'g}; s. equiv{car{'g}; eqG{'g}; op{'g; 's; 'e2}; 's}} } -->
323     sequent ['ext] { 'H >- equiv{car{'g}; 'R; 'e2; id{'g}} }     sequent ['ext] { 'H >- equiv{car{'g}; eqG{'g}; 'e2; id{'g}} }
324    
325  interactive unique_inv1 {| intro [] |} 'H :  interactive unique_inv1 {| intro [] |} 'H :
326     sequent [squash] { 'H >- isset{'s} } -->     sequent [squash] { 'H >- isset{'s} } -->
327     sequent [squash] { 'H >- isset{'s2} } -->     sequent [squash] { 'H >- isset{'s2} } -->
    sequent [squash] { 'H >- isset{'R} } -->  
328     sequent [squash] { 'H >- 'g IN label } -->     sequent [squash] { 'H >- 'g IN label } -->
329     sequent ['ext] { 'H >- group{'g} } -->     sequent ['ext] { 'H >- group{'g} } -->
    sequent ['ext] { 'H >- equiv{car{'g}; 'R} } -->  
330     sequent ['ext] { 'H >- mem{'s; car{'g}} } -->     sequent ['ext] { 'H >- mem{'s; car{'g}} } -->
331     sequent ['ext] { 'H >- mem{'s2; car{'g}} } -->     sequent ['ext] { 'H >- mem{'s2; car{'g}} } -->
332     sequent ['ext] { 'H >- equiv{car{'g}; 'R; op{'g; 's2; 's}; id{'g}} } -->     sequent ['ext] { 'H >- equiv{car{'g}; eqG{'g}; op{'g; 's2; 's}; id{'g}} } -->
333     sequent ['ext] { 'H >- equiv{car{'g}; 'R; 's2; inv{'g; 's}} }     sequent ['ext] { 'H >- equiv{car{'g}; eqG{'g}; 's2; inv{'g; 's}} }
   
 interactive unique_inv_elim1 {| elim [] |} 'H 'J :  
    sequent [squash] { 'H; x: equiv{car{'g}; 'R; op{'g; 's2; 's}; id{'g}}; 'J['x] >- isset{'s} } -->  
    sequent [squash] { 'H; x: equiv{car{'g}; 'R; op{'g; 's2; 's}; id{'g}}; 'J['x] >- isset{'s2} } -->  
    sequent [squash] { 'H; x: equiv{car{'g}; 'R; op{'g; 's2; 's}; id{'g}}; 'J['x] >- isset{'R} } -->  
    sequent [squash] { 'H; x: equiv{car{'g}; 'R; op{'g; 's2; 's}; id{'g}}; 'J['x] >- 'g IN label } -->  
    sequent ['ext] { 'H; x: equiv{car{'g}; 'R; op{'g; 's2; 's}; id{'g}}; 'J['x] >- group{'g} } -->  
    sequent ['ext] { 'H; x: equiv{car{'g}; 'R; op{'g; 's2; 's}; id{'g}}; 'J['x] >- equiv{car{'g}; 'R} } -->  
    sequent ['ext] { 'H; x: equiv{car{'g}; 'R; op{'g; 's2; 's}; id{'g}}; 'J['x] >- mem{'s; car{'g}} } -->  
    sequent ['ext] { 'H; x: equiv{car{'g}; 'R; op{'g; 's2; 's}; id{'g}}; 'J['x] >- mem{'s2; car{'g}} } -->  
    sequent ['ext] { 'H; x: equiv{car{'g}; 'R; op{'g; 's2; 's}; id{'g}}; 'J['x]; y: equiv{car{'g}; 'R; 's2; inv{'g; 's}} >- 'C['x] } -->  
    sequent ['ext] { 'H; x: equiv{car{'g}; 'R; op{'g; 's2; 's}; id{'g}}; 'J['x] >- 'C['x] }  
334    
335  interactive unique_inv2 {| intro [] |} 'H :  interactive unique_inv2 {| intro [] |} 'H :
336     sequent [squash] { 'H >- isset{'s} } -->     sequent [squash] { 'H >- isset{'s} } -->
337     sequent [squash] { 'H >- isset{'s2} } -->     sequent [squash] { 'H >- isset{'s2} } -->
338     sequent [squash] { 'H >- 'g IN label } -->     sequent [squash] { 'H >- 'g IN label } -->
    sequent [squash] { 'H >- isset{'R} } -->  
339     sequent ['ext] { 'H >- group{'g} } -->     sequent ['ext] { 'H >- group{'g} } -->
    sequent ['ext] { 'H >- equiv{car{'g}; 'R} } -->  
340     sequent ['ext] { 'H >- mem{'s; car{'g}} } -->     sequent ['ext] { 'H >- mem{'s; car{'g}} } -->
341     sequent ['ext] { 'H >- mem{'s2; car{'g}} } -->     sequent ['ext] { 'H >- mem{'s2; car{'g}} } -->
342     sequent ['ext] { 'H >- equiv{car{'g}; 'R; op{'g; 's; 's2}; id{'g}} } -->     sequent ['ext] { 'H >- equiv{car{'g}; eqG{'g}; op{'g; 's; 's2}; id{'g}} } -->
343     sequent ['ext] { 'H >- equiv{car{'g}; 'R; 's2; inv{'g; 's}} }     sequent ['ext] { 'H >- equiv{car{'g}; eqG{'g}; 's2; inv{'g; 's}} }
344    
345    interactive unique_inv_elim1 (*{| elim [] |}*) 'H 'J :
346       sequent [squash] { 'H; x: equiv{car{'g}; eqG{'g}; op{'g; 's2; 's}; id{'g}}; 'J['x] >- isset{'s} } -->
347       sequent [squash] { 'H; x: equiv{car{'g}; eqG{'g}; op{'g; 's2; 's}; id{'g}}; 'J['x] >- isset{'s2} } -->
348       sequent [squash] { 'H; x: equiv{car{'g}; eqG{'g}; op{'g; 's2; 's}; id{'g}}; 'J['x] >- 'g IN label } -->
349       sequent ['ext] { 'H; x: equiv{car{'g}; eqG{'g}; op{'g; 's2; 's}; id{'g}}; 'J['x] >- group{'g} } -->
350       sequent ['ext] { 'H; x: equiv{car{'g}; eqG{'g}; op{'g; 's2; 's}; id{'g}}; 'J['x] >- mem{'s; car{'g}} } -->
351       sequent ['ext] { 'H; x: equiv{car{'g}; eqG{'g}; op{'g; 's2; 's}; id{'g}}; 'J['x] >- mem{'s2; car{'g}} } -->
352       sequent ['ext] { 'H; x: equiv{car{'g}; eqG{'g}; op{'g; 's2; 's}; id{'g}}; 'J['x]; y: equiv{car{'g}; eqG{'g}; 's2; inv{'g; 's}} >- 'C['x] } -->
353       sequent ['ext] { 'H; x: equiv{car{'g}; eqG{'g}; op{'g; 's2; 's}; id{'g}}; 'J['x] >- 'C['x] }
354    
355    interactive unique_inv_elim2 (*{| elim [] |}*) 'H 'J :
356       sequent [squash] { 'H; x: equiv{car{'g}; eqG{'g}; op{'g; 's; 's2}; id{'g}}; 'J['x] >- isset{'s} } -->
357       sequent [squash] { 'H; x: equiv{car{'g}; eqG{'g}; op{'g; 's; 's2}; id{'g}}; 'J['x] >- isset{'s2} } -->
358       sequent [squash] { 'H; x: equiv{car{'g}; eqG{'g}; op{'g; 's; 's2}; id{'g}}; 'J['x] >- 'g IN label } -->
359       sequent ['ext] { 'H; x: equiv{car{'g}; eqG{'g}; op{'g; 's; 's2}; id{'g}}; 'J['x] >- group{'g} } -->
360       sequent ['ext] { 'H; x: equiv{car{'g}; eqG{'g}; op{'g; 's; 's2}; id{'g}}; 'J['x] >- mem{'s; car{'g}} } -->
361       sequent ['ext] { 'H; x: equiv{car{'g}; eqG{'g}; op{'g; 's; 's2}; id{'g}}; 'J['x] >- mem{'s2; car{'g}} } -->
362       sequent ['ext] { 'H; x: equiv{car{'g}; eqG{'g}; op{'g; 's; 's2}; id{'g}}; 'J['x]; y: equiv{car{'g}; eqG{'g}; 's2; inv{'g; 's}} >- 'C['x] } -->
363       sequent ['ext] { 'H; x: equiv{car{'g}; eqG{'g}; op{'g; 's; 's2}; id{'g}}; 'J['x] >- 'C['x] }
364    
365    let uniqueInvLeftT i p =
366       let j, k = Sequent.hyp_indices p i in
367          unique_inv_elim1 j k p
368    
369    let uniqueInvRightT i p =
370       let j, k = Sequent.hyp_indices p i in
371          unique_inv_elim2 j k p
372    
373  (* Unique solution for a * x = b : x = a' * b *)  (* Unique solution for a * x = b : x = a' * b *)
374  interactive unique_sol1 {| intro [] |} 'H :  interactive unique_sol1 {| intro [] |} 'H :
375     sequent [squash] { 'H >- isset{'a} } -->     sequent [squash] { 'H >- isset{'a} } -->
376     sequent [squash] { 'H >- isset{'b} } -->     sequent [squash] { 'H >- isset{'b} } -->
377     sequent [squash] { 'H >- isset{'x} } -->     sequent [squash] { 'H >- isset{'x} } -->
    sequent [squash] { 'H >- isset{'R} } -->  
378     sequent [squash] { 'H >- 'g IN label } -->     sequent [squash] { 'H >- 'g IN label } -->
379     sequent ['ext] { 'H >- group{'g} } -->     sequent ['ext] { 'H >- group{'g} } -->
    sequent ['ext] { 'H >- equiv{car{'g}; 'R} } -->  
380     sequent ['ext] { 'H >- mem{'a; car{'g}} } -->     sequent ['ext] { 'H >- mem{'a; car{'g}} } -->
381     sequent ['ext] { 'H >- mem{'b; car{'g}} } -->     sequent ['ext] { 'H >- mem{'b; car{'g}} } -->
382     sequent ['ext] { 'H >- mem{'x; car{'g}} } -->     sequent ['ext] { 'H >- mem{'x; car{'g}} } -->
383     sequent ['ext] { 'H >- equiv{car{'g}; 'R; op{'g; 'a; 'x}; 'b} } -->     sequent ['ext] { 'H >- equiv{car{'g}; eqG{'g}; op{'g; 'a; 'x}; 'b} } -->
384     sequent ['ext] { 'H >- equiv{car{'g}; 'R; 'x; op{'g; inv{'g; 'a}; 'b}} }     sequent ['ext] { 'H >- equiv{car{'g}; eqG{'g}; 'x; op{'g; inv{'g; 'a}; 'b}} }
385    
386  (* Unique solution for y * a = b : y = b * a' *)  (* Unique solution for y * a = b : y = b * a' *)
387  interactive unique_sol2 {| intro [] |} 'H :  interactive unique_sol2 {| intro [] |} 'H :
388     sequent [squash] { 'H >- isset{'a} } -->     sequent [squash] { 'H >- isset{'a} } -->
389     sequent [squash] { 'H >- isset{'b} } -->     sequent [squash] { 'H >- isset{'b} } -->
390     sequent [squash] { 'H >- isset{'y} } -->     sequent [squash] { 'H >- isset{'y} } -->
    sequent [squash] { 'H >- isset{'R} } -->  
391     sequent [squash] { 'H >- 'g IN label } -->     sequent [squash] { 'H >- 'g IN label } -->
392     sequent ['ext] { 'H >- group{'g} } -->     sequent ['ext] { 'H >- group{'g} } -->
    sequent ['ext] { 'H >- equiv{car{'g}; 'R} } -->  
393     sequent ['ext] { 'H >- mem{'a; car{'g}} } -->     sequent ['ext] { 'H >- mem{'a; car{'g}} } -->
394     sequent ['ext] { 'H >- mem{'b; car{'g}} } -->     sequent ['ext] { 'H >- mem{'b; car{'g}} } -->
395     sequent ['ext] { 'H >- mem{'y; car{'g}} } -->     sequent ['ext] { 'H >- mem{'y; car{'g}} } -->
396     sequent ['ext] { 'H >- equiv{car{'g}; 'R; op{'g; 'y; 'a}; 'b} } -->     sequent ['ext] { 'H >- equiv{car{'g}; eqG{'g}; op{'g; 'y; 'a}; 'b} } -->
397     sequent ['ext] { 'H >- equiv{car{'g}; 'R; 'y; op{'g; 'b; inv{'g; 'a}}} }     sequent ['ext] { 'H >- equiv{car{'g}; eqG{'g}; 'y; op{'g; 'b; inv{'g; 'a}}} }
398    
399  (* (a * b)' = b' * a'  *)  (* (a * b)' = b' * a'  *)
400  interactive inv_simplify {| intro [] |} 'H :  interactive inv_simplify {| intro [] |} 'H :
401     sequent [squash] { 'H >- isset{'a} } -->     sequent [squash] { 'H >- isset{'a} } -->
402     sequent [squash] { 'H >- isset{'b} } -->     sequent [squash] { 'H >- isset{'b} } -->
    sequent [squash] { 'H >- isset{'R} } -->  
403     sequent [squash] { 'H >- 'g IN label } -->     sequent [squash] { 'H >- 'g IN label } -->
404     sequent ['ext] { 'H >- group{'g} } -->     sequent ['ext] { 'H >- group{'g} } -->
    sequent ['ext] { 'H >- equiv{car{'g}; 'R} } -->  
405     sequent ['ext] { 'H >- mem{'a; car{'g}} } -->     sequent ['ext] { 'H >- mem{'a; car{'g}} } -->
406     sequent ['ext] { 'H >- mem{'b; car{'g}} } -->     sequent ['ext] { 'H >- mem{'b; car{'g}} } -->
407     sequent ['ext] { 'H >- equiv{car{'g}; 'R; inv{'g; op{'g; 'a; 'b}}; op{'g; inv{'g; 'b}; inv{'g; 'a}}} }     sequent ['ext] { 'H >- equiv{car{'g}; eqG{'g}; inv{'g; op{'g; 'a; 'b}}; op{'g; inv{'g; 'b}; inv{'g; 'a}}} }
408    
409  (* Inverse of id *)  (* Inverse of id *)
410  interactive inv_of_id {| intro [] |} 'H :  interactive inv_of_id {| intro [] |} 'H :
    sequent [squash] { 'H >- isset{'R} } -->  
411     sequent [squash] { 'H >- 'g IN label } -->     sequent [squash] { 'H >- 'g IN label } -->
412     sequent ['ext] { 'H >- group{'g} } -->     sequent ['ext] { 'H >- group{'g} } -->
413     sequent ['ext] { 'H >- equiv{car{'g}; 'R} } -->     sequent ['ext] { 'H >- equiv{car{'g}; eqG{'g}; inv{'g; id{'g}}; id{'g}} }
    sequent ['ext] { 'H >- equiv{car{'g}; 'R; inv{'g; id{'g}}; id{'g}} }  
414    
415  (* e * a = a * e *)  (* e * a = a * e *)
416  interactive id_commut1 {| intro [] |} 'H :  interactive id_commut1 {| intro [] |} 'H :
417     sequent [squash] { 'H >- isset{'a} } -->     sequent [squash] { 'H >- isset{'a} } -->
    sequent [squash] { 'H >- isset{'R} } -->  
418     sequent [squash] { 'H >- 'g IN label } -->     sequent [squash] { 'H >- 'g IN label } -->
419     sequent ['ext] { 'H >- group{'g} } -->     sequent ['ext] { 'H >- group{'g} } -->
420     sequent ['ext] { 'H >- mem{'a; car{'g}} } -->     sequent ['ext] { 'H >- mem{'a; car{'g}} } -->
421     sequent ['ext] { 'H >- equiv{car{'g}; 'R} } -->     sequent ['ext] { 'H >- equiv{car{'g}; eqG{'g}; op{'g; id{'g}; 'a}; op{'g; 'a; id{'g}}} }
    sequent ['ext] { 'H >- equiv{car{'g}; 'R; op{'g; id{'g}; 'a}; op{'g; 'a; id{'g}}} }  
422    
423  (* a * e = e * a *)  (* a * e = e * a *)
424  interactive id_commut2 {| intro [] |} 'H :  interactive id_commut2 {| intro [] |} 'H :
425     sequent [squash] { 'H >- isset{'a} } -->     sequent [squash] { 'H >- isset{'a} } -->
    sequent [squash] { 'H >- isset{'R} } -->  
426     sequent [squash] { 'H >- 'g IN label } -->     sequent [squash] { 'H >- 'g IN label } -->
427     sequent ['ext] { 'H >- group{'g} } -->     sequent ['ext] { 'H >- group{'g} } -->
428     sequent ['ext] { 'H >- mem{'a; car{'g}} } -->     sequent ['ext] { 'H >- mem{'a; car{'g}} } -->
429     sequent ['ext] { 'H >- equiv{car{'g}; 'R} } -->     sequent ['ext] { 'H >- equiv{car{'g}; eqG{'g}; op{'g; 'a; id{'g}}; op{'g; id{'g}; 'a}} }
    sequent ['ext] { 'H >- equiv{car{'g}; 'R; op{'g; 'a; id{'g}}; op{'g; id{'g}; 'a}} }  

Legend:
Removed from v.3552  
changed lines
  Added in v.3553

  ViewVC Help
Powered by ViewVC 1.1.26