240 (res_inst_tac [("t","Y(i)")] ssubst 1), |
240 (res_inst_tac [("t","Y(i)")] ssubst 1), |
241 (atac 1), |
241 (atac 1), |
242 (rtac trans 1), |
242 (rtac trans 1), |
243 (rtac cfun_arg_cong 1), |
243 (rtac cfun_arg_cong 1), |
244 (rtac Iwhen2 1), |
244 (rtac Iwhen2 1), |
245 (res_inst_tac [("P","Y(i)=UU")] swap 1), |
245 (res_inst_tac [("Pa","Y(i)=UU")] swap 1), |
246 (fast_tac HOL_cs 1), |
246 (fast_tac HOL_cs 1), |
247 (rtac (inst_ssum_pcpo RS ssubst) 1), |
247 (rtac (inst_ssum_pcpo RS ssubst) 1), |
248 (res_inst_tac [("t","Y(i)")] ssubst 1), |
248 (res_inst_tac [("t","Y(i)")] ssubst 1), |
249 (atac 1), |
249 (atac 1), |
250 (fast_tac HOL_cs 1), |
250 (fast_tac HOL_cs 1), |
251 (rtac (Iwhen2 RS ssubst) 1), |
251 (rtac (Iwhen2 RS ssubst) 1), |
252 (res_inst_tac [("P","Y(i)=UU")] swap 1), |
252 (res_inst_tac [("Pa","Y(i)=UU")] swap 1), |
253 (fast_tac HOL_cs 1), |
253 (fast_tac HOL_cs 1), |
254 (rtac (inst_ssum_pcpo RS ssubst) 1), |
254 (rtac (inst_ssum_pcpo RS ssubst) 1), |
255 (res_inst_tac [("t","Y(i)")] ssubst 1), |
255 (res_inst_tac [("t","Y(i)")] ssubst 1), |
256 (atac 1), |
256 (atac 1), |
257 (fast_tac HOL_cs 1), |
257 (fast_tac HOL_cs 1), |
300 (res_inst_tac [("t","Y(i)")] ssubst 1), |
300 (res_inst_tac [("t","Y(i)")] ssubst 1), |
301 (atac 1), |
301 (atac 1), |
302 (rtac trans 1), |
302 (rtac trans 1), |
303 (rtac cfun_arg_cong 1), |
303 (rtac cfun_arg_cong 1), |
304 (rtac Iwhen3 1), |
304 (rtac Iwhen3 1), |
305 (res_inst_tac [("P","Y(i)=UU")] swap 1), |
305 (res_inst_tac [("Pa","Y(i)=UU")] swap 1), |
306 (fast_tac HOL_cs 1), |
306 (fast_tac HOL_cs 1), |
307 (dtac notnotD 1), |
307 (dtac notnotD 1), |
308 (rtac (inst_ssum_pcpo RS ssubst) 1), |
308 (rtac (inst_ssum_pcpo RS ssubst) 1), |
309 (rtac (strict_IsinlIsinr RS ssubst) 1), |
309 (rtac (strict_IsinlIsinr RS ssubst) 1), |
310 (res_inst_tac [("t","Y(i)")] ssubst 1), |
310 (res_inst_tac [("t","Y(i)")] ssubst 1), |
311 (atac 1), |
311 (atac 1), |
312 (fast_tac HOL_cs 1), |
312 (fast_tac HOL_cs 1), |
313 (rtac (Iwhen3 RS ssubst) 1), |
313 (rtac (Iwhen3 RS ssubst) 1), |
314 (res_inst_tac [("P","Y(i)=UU")] swap 1), |
314 (res_inst_tac [("Pa","Y(i)=UU")] swap 1), |
315 (fast_tac HOL_cs 1), |
315 (fast_tac HOL_cs 1), |
316 (dtac notnotD 1), |
316 (dtac notnotD 1), |
317 (rtac (inst_ssum_pcpo RS ssubst) 1), |
317 (rtac (inst_ssum_pcpo RS ssubst) 1), |
318 (rtac (strict_IsinlIsinr RS ssubst) 1), |
318 (rtac (strict_IsinlIsinr RS ssubst) 1), |
319 (res_inst_tac [("t","Y(i)")] ssubst 1), |
319 (res_inst_tac [("t","Y(i)")] ssubst 1), |