206 apply (case_tac "Ex1 (subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (P, xa, ya))))") |
206 apply (case_tac "Ex1 (subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (P, xa, ya))))") |
207 apply simp_all[2] |
207 apply simp_all[2] |
208 apply auto[1] |
208 apply auto[1] |
209 apply (erule_tac x="x" in allE) |
209 apply (erule_tac x="x" in allE) |
210 apply simp |
210 apply simp |
211 apply (thin_tac "\<forall>p\<Colon>perm. |
211 apply(thin_tac "\<forall>p. p \<bullet> The (subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (P, xa, ya)))) = |
212 p \<bullet> The (subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (P, xa, ya)))) = |
212 (if \<exists>!x. subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (p \<bullet> P, p \<bullet> xa, p \<bullet> ya))) x |
213 (if \<exists>!x\<Colon>guardedTerm_mix + sumList_mix + piMix. |
213 then THE x. subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (p \<bullet> P, p \<bullet> xa, p \<bullet> ya))) x |
214 subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (p \<bullet> P, p \<bullet> xa, p \<bullet> ya))) x |
214 else Inr (Inr undefined))") |
215 then THE x\<Colon>guardedTerm_mix + sumList_mix + piMix. |
215 apply(thin_tac "\<forall>p. p \<bullet> (if \<exists>!x. subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (Pa, xa, ya))) x |
216 subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (p \<bullet> P, p \<bullet> xa, p \<bullet> ya))) x |
216 then THE x. subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (Pa, xa, ya))) x |
217 else Inr (Inr undefined))") |
217 else Inr (Inr undefined)) = |
218 apply (thin_tac "\<forall>p\<Colon>perm. |
218 (if \<exists>!x. subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (p \<bullet> Pa, p \<bullet> xa, p \<bullet> ya))) x |
219 p \<bullet> (if \<exists>!x\<Colon>guardedTerm_mix + sumList_mix + piMix. |
219 then THE x. subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (p \<bullet> Pa, p \<bullet> xa, p \<bullet> ya))) x |
220 subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (Pa, xa, ya))) x |
220 else Inr (Inr undefined))") |
221 then THE x\<Colon>guardedTerm_mix + sumList_mix + piMix. |
|
222 subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (Pa, xa, ya))) x |
|
223 else Inr (Inr undefined)) = |
|
224 (if \<exists>!x\<Colon>guardedTerm_mix + sumList_mix + piMix. |
|
225 subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (p \<bullet> Pa, p \<bullet> xa, p \<bullet> ya))) x |
|
226 then THE x\<Colon>guardedTerm_mix + sumList_mix + piMix. |
|
227 subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (p \<bullet> Pa, p \<bullet> xa, p \<bullet> ya))) x |
|
228 else Inr (Inr undefined))") |
|
229 apply (thin_tac "atom b \<sharp> (xa, ya)") |
221 apply (thin_tac "atom b \<sharp> (xa, ya)") |
230 apply (thin_tac "atom ba \<sharp> (xa, ya)") |
222 apply (thin_tac "atom ba \<sharp> (xa, ya)") |
231 apply (thin_tac "[[atom b]]lst. P = [[atom ba]]lst. Pa") |
223 apply (thin_tac "[[atom b]]lst. P = [[atom ba]]lst. Pa") |
232 apply(cases rule: subsGuard_mix_subsList_mix_subs_mix_graph.cases) |
224 apply(cases rule: subsGuard_mix_subsList_mix_subs_mix_graph.cases) |
233 apply assumption |
225 apply assumption |
299 apply (case_tac "Ex1 (subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (P, xa, ya))))") |
291 apply (case_tac "Ex1 (subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (P, xa, ya))))") |
300 apply simp_all[2] |
292 apply simp_all[2] |
301 apply auto[1] |
293 apply auto[1] |
302 apply (erule_tac x="x" in allE) |
294 apply (erule_tac x="x" in allE) |
303 apply simp |
295 apply simp |
304 apply (thin_tac "\<forall>p\<Colon>perm. |
296 apply(thin_tac "\<forall>p. p \<bullet> The (subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (P, xa, ya)))) = |
305 p \<bullet> The (subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (P, xa, ya)))) = |
297 (if \<exists>!x. subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (p \<bullet> P, p \<bullet> xa, p \<bullet> ya))) x |
306 (if \<exists>!x\<Colon>guardedTerm_mix + sumList_mix + piMix. |
298 then THE x. subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (p \<bullet> P, p \<bullet> xa, p \<bullet> ya))) x |
307 subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (p \<bullet> P, p \<bullet> xa, p \<bullet> ya))) x |
299 else Inr (Inr undefined))") |
308 then THE x\<Colon>guardedTerm_mix + sumList_mix + piMix. |
300 apply(thin_tac "\<forall>p. p \<bullet> (if \<exists>!x. subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (Pa, xa, ya))) x |
309 subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (p \<bullet> P, p \<bullet> xa, p \<bullet> ya))) x |
301 then THE x. subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (Pa, xa, ya))) x |
310 else Inr (Inr undefined))") |
302 else Inr (Inr undefined)) = |
311 apply (thin_tac "\<forall>p\<Colon>perm. |
303 (if \<exists>!x. subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (p \<bullet> Pa, p \<bullet> xa, p \<bullet> ya))) x |
312 p \<bullet> (if \<exists>!x\<Colon>guardedTerm_mix + sumList_mix + piMix. |
304 then THE x. subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (p \<bullet> Pa, p \<bullet> xa, p \<bullet> ya))) x |
313 subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (Pa, xa, ya))) x |
305 else Inr (Inr undefined))") |
314 then THE x\<Colon>guardedTerm_mix + sumList_mix + piMix. |
|
315 subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (Pa, xa, ya))) x |
|
316 else Inr (Inr undefined)) = |
|
317 (if \<exists>!x\<Colon>guardedTerm_mix + sumList_mix + piMix. |
|
318 subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (p \<bullet> Pa, p \<bullet> xa, p \<bullet> ya))) x |
|
319 then THE x\<Colon>guardedTerm_mix + sumList_mix + piMix. |
|
320 subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (p \<bullet> Pa, p \<bullet> xa, p \<bullet> ya))) x |
|
321 else Inr (Inr undefined))") |
|
322 apply (thin_tac "atom b \<sharp> (xa, ya)") |
306 apply (thin_tac "atom b \<sharp> (xa, ya)") |
323 apply (thin_tac "atom ba \<sharp> (xa, ya)") |
307 apply (thin_tac "atom ba \<sharp> (xa, ya)") |
324 apply (thin_tac "[[atom b]]lst. P = [[atom ba]]lst. Pa") |
308 apply (thin_tac "[[atom b]]lst. P = [[atom ba]]lst. Pa") |
325 apply(cases rule: subsGuard_mix_subsList_mix_subs_mix_graph.cases) |
309 apply(cases rule: subsGuard_mix_subsList_mix_subs_mix_graph.cases) |
326 apply assumption |
310 apply assumption |