equal
deleted
inserted
replaced
351 |
351 |
352 with s app1 |
352 with s app1 |
353 obtain a X ST where |
353 obtain a X ST where |
354 s1: "s1 = (a @ X # ST, b1)" and |
354 s1: "s1 = (a @ X # ST, b1)" and |
355 l: "length a = length list" |
355 l: "length a = length list" |
356 by (simp, elim exE conjE, simp) |
356 by (simp, elim exE conjE, simp (no_asm_simp)) |
357 |
357 |
358 from Invoke s app2 |
358 from Invoke s app2 |
359 obtain a' X' ST' where |
359 obtain a' X' ST' where |
360 s2: "s2 = (a' @ X' # ST', b2)" and |
360 s2: "s2 = (a' @ X' # ST', b2)" and |
361 l': "length a' = length list" |
361 l': "length a' = length list" |
362 by (simp, elim exE conjE, simp) |
362 by (simp, elim exE conjE, simp (no_asm_simp)) |
363 |
363 |
364 from l l' |
364 from l l' |
365 have lr: "length a = length a'" by simp |
365 have lr: "length a = length a'" by simp |
366 |
366 |
367 from lr G s s1 s2 |
367 from lr G s1 s2 |
368 have "G \<turnstile> (ST, b1) <=s (ST', b2)" |
368 have "G \<turnstile> (ST, b1) <=s (ST', b2)" |
369 by (simp add: sup_state_append_fst sup_state_Cons1) |
369 by (simp add: sup_state_append_fst sup_state_Cons1) |
370 |
370 |
371 moreover |
371 moreover |
372 |
372 |