[STATEMENT]
lemma call_inline_call [simp]:
  "call e = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} e) = call e'"
  "calls es = \<lfloor>aMvs\<rfloor> \<Longrightarrow> calls (inline_calls {v:T=vo;e'} es) = call e'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (call e = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} e) = call e') &&& (calls es = \<lfloor>aMvs\<rfloor> \<Longrightarrow> calls (inline_calls {v:T=vo; e'} es) = call e')
[PROOF STEP]
apply(induct e and es rule: call.induct calls.induct)
[PROOF STATE]
proof (prove)
goal (25 subgoals):
 1. \<And>x. call (new x) = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} (new x)) = call e'
 2. \<And>x1 x2. \<lbrakk>call x2 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x2) = call e'; call (newA x1\<lfloor>x2\<rceil>) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (newA x1\<lfloor>x2\<rceil>)) = call e'
 3. \<And>x1 x2. \<lbrakk>call x2 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x2) = call e'; call (Cast x1 x2) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (Cast x1 x2)) = call e'
 4. \<And>x1 x2. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call (x1 instanceof x2) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1 instanceof x2)) = call e'
 5. \<And>x. call (Val x) = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} (Val x)) = call e'
 6. \<And>x1 x2 x3. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call x3 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x3) = call e'; call (x1 \<guillemotleft>x2\<guillemotright> x3) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1 \<guillemotleft>x2\<guillemotright> x3)) = call e'
 7. \<And>x. call (Var x) = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} (Var x)) = call e'
 8. \<And>x1 x2. \<lbrakk>call x2 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x2) = call e'; call (x1:=x2) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1:=x2)) = call e'
 9. \<And>x1 x2. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call x2 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x2) = call e'; call (x1\<lfloor>x2\<rceil>) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1\<lfloor>x2\<rceil>)) = call e'
 10. \<And>x1 x2 x3. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call x2 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x2) = call e'; call x3 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x3) = call e'; call (x1\<lfloor>x2\<rceil> := x3) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1\<lfloor>x2\<rceil> := x3)) = call e'
A total of 25 subgoals...
[PROOF STEP]
apply(fastforce)
[PROOF STATE]
proof (prove)
goal (24 subgoals):
 1. \<And>x1 x2. \<lbrakk>call x2 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x2) = call e'; call (newA x1\<lfloor>x2\<rceil>) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (newA x1\<lfloor>x2\<rceil>)) = call e'
 2. \<And>x1 x2. \<lbrakk>call x2 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x2) = call e'; call (Cast x1 x2) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (Cast x1 x2)) = call e'
 3. \<And>x1 x2. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call (x1 instanceof x2) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1 instanceof x2)) = call e'
 4. \<And>x. call (Val x) = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} (Val x)) = call e'
 5. \<And>x1 x2 x3. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call x3 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x3) = call e'; call (x1 \<guillemotleft>x2\<guillemotright> x3) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1 \<guillemotleft>x2\<guillemotright> x3)) = call e'
 6. \<And>x. call (Var x) = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} (Var x)) = call e'
 7. \<And>x1 x2. \<lbrakk>call x2 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x2) = call e'; call (x1:=x2) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1:=x2)) = call e'
 8. \<And>x1 x2. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call x2 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x2) = call e'; call (x1\<lfloor>x2\<rceil>) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1\<lfloor>x2\<rceil>)) = call e'
 9. \<And>x1 x2 x3. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call x2 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x2) = call e'; call x3 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x3) = call e'; call (x1\<lfloor>x2\<rceil> := x3) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1\<lfloor>x2\<rceil> := x3)) = call e'
 10. \<And>x. \<lbrakk>call x = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x) = call e'; call (x\<bullet>length) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x\<bullet>length)) = call e'
A total of 24 subgoals...
[PROOF STEP]
apply(fastforce)
[PROOF STATE]
proof (prove)
goal (23 subgoals):
 1. \<And>x1 x2. \<lbrakk>call x2 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x2) = call e'; call (Cast x1 x2) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (Cast x1 x2)) = call e'
 2. \<And>x1 x2. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call (x1 instanceof x2) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1 instanceof x2)) = call e'
 3. \<And>x. call (Val x) = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} (Val x)) = call e'
 4. \<And>x1 x2 x3. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call x3 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x3) = call e'; call (x1 \<guillemotleft>x2\<guillemotright> x3) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1 \<guillemotleft>x2\<guillemotright> x3)) = call e'
 5. \<And>x. call (Var x) = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} (Var x)) = call e'
 6. \<And>x1 x2. \<lbrakk>call x2 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x2) = call e'; call (x1:=x2) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1:=x2)) = call e'
 7. \<And>x1 x2. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call x2 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x2) = call e'; call (x1\<lfloor>x2\<rceil>) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1\<lfloor>x2\<rceil>)) = call e'
 8. \<And>x1 x2 x3. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call x2 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x2) = call e'; call x3 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x3) = call e'; call (x1\<lfloor>x2\<rceil> := x3) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1\<lfloor>x2\<rceil> := x3)) = call e'
 9. \<And>x. \<lbrakk>call x = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x) = call e'; call (x\<bullet>length) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x\<bullet>length)) = call e'
 10. \<And>x1 x2 x3. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call (x1\<bullet>x2{x3}) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1\<bullet>x2{x3})) = call e'
A total of 23 subgoals...
[PROOF STEP]
apply(fastforce)
[PROOF STATE]
proof (prove)
goal (22 subgoals):
 1. \<And>x1 x2. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call (x1 instanceof x2) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1 instanceof x2)) = call e'
 2. \<And>x. call (Val x) = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} (Val x)) = call e'
 3. \<And>x1 x2 x3. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call x3 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x3) = call e'; call (x1 \<guillemotleft>x2\<guillemotright> x3) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1 \<guillemotleft>x2\<guillemotright> x3)) = call e'
 4. \<And>x. call (Var x) = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} (Var x)) = call e'
 5. \<And>x1 x2. \<lbrakk>call x2 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x2) = call e'; call (x1:=x2) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1:=x2)) = call e'
 6. \<And>x1 x2. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call x2 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x2) = call e'; call (x1\<lfloor>x2\<rceil>) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1\<lfloor>x2\<rceil>)) = call e'
 7. \<And>x1 x2 x3. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call x2 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x2) = call e'; call x3 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x3) = call e'; call (x1\<lfloor>x2\<rceil> := x3) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1\<lfloor>x2\<rceil> := x3)) = call e'
 8. \<And>x. \<lbrakk>call x = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x) = call e'; call (x\<bullet>length) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x\<bullet>length)) = call e'
 9. \<And>x1 x2 x3. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call (x1\<bullet>x2{x3}) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1\<bullet>x2{x3})) = call e'
 10. \<And>x1 x2 x3 x4. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call x4 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x4) = call e'; call (x1\<bullet>x2{x3} := x4) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1\<bullet>x2{x3} := x4)) = call e'
A total of 22 subgoals...
[PROOF STEP]
apply(fastforce)
[PROOF STATE]
proof (prove)
goal (21 subgoals):
 1. \<And>x. call (Val x) = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} (Val x)) = call e'
 2. \<And>x1 x2 x3. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call x3 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x3) = call e'; call (x1 \<guillemotleft>x2\<guillemotright> x3) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1 \<guillemotleft>x2\<guillemotright> x3)) = call e'
 3. \<And>x. call (Var x) = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} (Var x)) = call e'
 4. \<And>x1 x2. \<lbrakk>call x2 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x2) = call e'; call (x1:=x2) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1:=x2)) = call e'
 5. \<And>x1 x2. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call x2 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x2) = call e'; call (x1\<lfloor>x2\<rceil>) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1\<lfloor>x2\<rceil>)) = call e'
 6. \<And>x1 x2 x3. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call x2 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x2) = call e'; call x3 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x3) = call e'; call (x1\<lfloor>x2\<rceil> := x3) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1\<lfloor>x2\<rceil> := x3)) = call e'
 7. \<And>x. \<lbrakk>call x = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x) = call e'; call (x\<bullet>length) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x\<bullet>length)) = call e'
 8. \<And>x1 x2 x3. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call (x1\<bullet>x2{x3}) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1\<bullet>x2{x3})) = call e'
 9. \<And>x1 x2 x3 x4. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call x4 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x4) = call e'; call (x1\<bullet>x2{x3} := x4) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1\<bullet>x2{x3} := x4)) = call e'
 10. \<And>x1 x2 x3 x4 x5. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call x4 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x4) = call e'; call x5 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x5) = call e'; call (x1\<bullet>compareAndSwap(x2\<bullet>x3, x4, x5)) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1\<bullet>compareAndSwap(x2\<bullet>x3, x4, x5))) = call e'
A total of 21 subgoals...
[PROOF STEP]
apply(fastforce)
[PROOF STATE]
proof (prove)
goal (20 subgoals):
 1. \<And>x1 x2 x3. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call x3 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x3) = call e'; call (x1 \<guillemotleft>x2\<guillemotright> x3) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1 \<guillemotleft>x2\<guillemotright> x3)) = call e'
 2. \<And>x. call (Var x) = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} (Var x)) = call e'
 3. \<And>x1 x2. \<lbrakk>call x2 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x2) = call e'; call (x1:=x2) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1:=x2)) = call e'
 4. \<And>x1 x2. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call x2 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x2) = call e'; call (x1\<lfloor>x2\<rceil>) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1\<lfloor>x2\<rceil>)) = call e'
 5. \<And>x1 x2 x3. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call x2 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x2) = call e'; call x3 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x3) = call e'; call (x1\<lfloor>x2\<rceil> := x3) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1\<lfloor>x2\<rceil> := x3)) = call e'
 6. \<And>x. \<lbrakk>call x = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x) = call e'; call (x\<bullet>length) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x\<bullet>length)) = call e'
 7. \<And>x1 x2 x3. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call (x1\<bullet>x2{x3}) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1\<bullet>x2{x3})) = call e'
 8. \<And>x1 x2 x3 x4. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call x4 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x4) = call e'; call (x1\<bullet>x2{x3} := x4) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1\<bullet>x2{x3} := x4)) = call e'
 9. \<And>x1 x2 x3 x4 x5. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call x4 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x4) = call e'; call x5 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x5) = call e'; call (x1\<bullet>compareAndSwap(x2\<bullet>x3, x4, x5)) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1\<bullet>compareAndSwap(x2\<bullet>x3, x4, x5))) = call e'
 10. \<And>x1 x2 x3. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; calls x3 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> calls (inline_calls {v:T=vo; e'} x3) = call e'; call (x1\<bullet>x2(x3)) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1\<bullet>x2(x3))) = call e'
A total of 20 subgoals...
[PROOF STEP]
apply(fastforce split: if_split)
[PROOF STATE]
proof (prove)
goal (19 subgoals):
 1. \<And>x. call (Var x) = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} (Var x)) = call e'
 2. \<And>x1 x2. \<lbrakk>call x2 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x2) = call e'; call (x1:=x2) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1:=x2)) = call e'
 3. \<And>x1 x2. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call x2 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x2) = call e'; call (x1\<lfloor>x2\<rceil>) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1\<lfloor>x2\<rceil>)) = call e'
 4. \<And>x1 x2 x3. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call x2 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x2) = call e'; call x3 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x3) = call e'; call (x1\<lfloor>x2\<rceil> := x3) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1\<lfloor>x2\<rceil> := x3)) = call e'
 5. \<And>x. \<lbrakk>call x = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x) = call e'; call (x\<bullet>length) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x\<bullet>length)) = call e'
 6. \<And>x1 x2 x3. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call (x1\<bullet>x2{x3}) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1\<bullet>x2{x3})) = call e'
 7. \<And>x1 x2 x3 x4. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call x4 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x4) = call e'; call (x1\<bullet>x2{x3} := x4) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1\<bullet>x2{x3} := x4)) = call e'
 8. \<And>x1 x2 x3 x4 x5. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call x4 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x4) = call e'; call x5 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x5) = call e'; call (x1\<bullet>compareAndSwap(x2\<bullet>x3, x4, x5)) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1\<bullet>compareAndSwap(x2\<bullet>x3, x4, x5))) = call e'
 9. \<And>x1 x2 x3. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; calls x3 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> calls (inline_calls {v:T=vo; e'} x3) = call e'; call (x1\<bullet>x2(x3)) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1\<bullet>x2(x3))) = call e'
 10. \<And>x1 x2 x3 x4. \<lbrakk>call x4 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x4) = call e'; call {x1:x2=x3; x4} = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} {x1:x2=x3; x4}) = call e'
A total of 19 subgoals...
[PROOF STEP]
apply(fastforce)
[PROOF STATE]
proof (prove)
goal (18 subgoals):
 1. \<And>x1 x2. \<lbrakk>call x2 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x2) = call e'; call (x1:=x2) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1:=x2)) = call e'
 2. \<And>x1 x2. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call x2 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x2) = call e'; call (x1\<lfloor>x2\<rceil>) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1\<lfloor>x2\<rceil>)) = call e'
 3. \<And>x1 x2 x3. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call x2 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x2) = call e'; call x3 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x3) = call e'; call (x1\<lfloor>x2\<rceil> := x3) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1\<lfloor>x2\<rceil> := x3)) = call e'
 4. \<And>x. \<lbrakk>call x = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x) = call e'; call (x\<bullet>length) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x\<bullet>length)) = call e'
 5. \<And>x1 x2 x3. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call (x1\<bullet>x2{x3}) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1\<bullet>x2{x3})) = call e'
 6. \<And>x1 x2 x3 x4. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call x4 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x4) = call e'; call (x1\<bullet>x2{x3} := x4) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1\<bullet>x2{x3} := x4)) = call e'
 7. \<And>x1 x2 x3 x4 x5. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call x4 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x4) = call e'; call x5 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x5) = call e'; call (x1\<bullet>compareAndSwap(x2\<bullet>x3, x4, x5)) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1\<bullet>compareAndSwap(x2\<bullet>x3, x4, x5))) = call e'
 8. \<And>x1 x2 x3. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; calls x3 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> calls (inline_calls {v:T=vo; e'} x3) = call e'; call (x1\<bullet>x2(x3)) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1\<bullet>x2(x3))) = call e'
 9. \<And>x1 x2 x3 x4. \<lbrakk>call x4 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x4) = call e'; call {x1:x2=x3; x4} = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} {x1:x2=x3; x4}) = call e'
 10. \<And>x1 x2 x3. \<lbrakk>call x2 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x2) = call e'; call x3 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x3) = call e'; call (sync\<^bsub>x1\<^esub> (x2) x3) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (sync\<^bsub>x1\<^esub> (x2) x3)) = call e'
A total of 18 subgoals...
[PROOF STEP]
apply(fastforce)
[PROOF STATE]
proof (prove)
goal (17 subgoals):
 1. \<And>x1 x2. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call x2 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x2) = call e'; call (x1\<lfloor>x2\<rceil>) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1\<lfloor>x2\<rceil>)) = call e'
 2. \<And>x1 x2 x3. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call x2 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x2) = call e'; call x3 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x3) = call e'; call (x1\<lfloor>x2\<rceil> := x3) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1\<lfloor>x2\<rceil> := x3)) = call e'
 3. \<And>x. \<lbrakk>call x = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x) = call e'; call (x\<bullet>length) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x\<bullet>length)) = call e'
 4. \<And>x1 x2 x3. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call (x1\<bullet>x2{x3}) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1\<bullet>x2{x3})) = call e'
 5. \<And>x1 x2 x3 x4. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call x4 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x4) = call e'; call (x1\<bullet>x2{x3} := x4) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1\<bullet>x2{x3} := x4)) = call e'
 6. \<And>x1 x2 x3 x4 x5. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call x4 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x4) = call e'; call x5 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x5) = call e'; call (x1\<bullet>compareAndSwap(x2\<bullet>x3, x4, x5)) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1\<bullet>compareAndSwap(x2\<bullet>x3, x4, x5))) = call e'
 7. \<And>x1 x2 x3. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; calls x3 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> calls (inline_calls {v:T=vo; e'} x3) = call e'; call (x1\<bullet>x2(x3)) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1\<bullet>x2(x3))) = call e'
 8. \<And>x1 x2 x3 x4. \<lbrakk>call x4 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x4) = call e'; call {x1:x2=x3; x4} = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} {x1:x2=x3; x4}) = call e'
 9. \<And>x1 x2 x3. \<lbrakk>call x2 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x2) = call e'; call x3 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x3) = call e'; call (sync\<^bsub>x1\<^esub> (x2) x3) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (sync\<^bsub>x1\<^esub> (x2) x3)) = call e'
 10. \<And>x1 x2 x3. \<lbrakk>call x3 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x3) = call e'; call (insync\<^bsub>x1\<^esub> (x2) x3) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (insync\<^bsub>x1\<^esub> (x2) x3)) = call e'
A total of 17 subgoals...
[PROOF STEP]
apply(fastforce split: if_split)
[PROOF STATE]
proof (prove)
goal (16 subgoals):
 1. \<And>x1 x2 x3. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call x2 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x2) = call e'; call x3 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x3) = call e'; call (x1\<lfloor>x2\<rceil> := x3) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1\<lfloor>x2\<rceil> := x3)) = call e'
 2. \<And>x. \<lbrakk>call x = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x) = call e'; call (x\<bullet>length) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x\<bullet>length)) = call e'
 3. \<And>x1 x2 x3. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call (x1\<bullet>x2{x3}) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1\<bullet>x2{x3})) = call e'
 4. \<And>x1 x2 x3 x4. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call x4 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x4) = call e'; call (x1\<bullet>x2{x3} := x4) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1\<bullet>x2{x3} := x4)) = call e'
 5. \<And>x1 x2 x3 x4 x5. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call x4 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x4) = call e'; call x5 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x5) = call e'; call (x1\<bullet>compareAndSwap(x2\<bullet>x3, x4, x5)) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1\<bullet>compareAndSwap(x2\<bullet>x3, x4, x5))) = call e'
 6. \<And>x1 x2 x3. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; calls x3 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> calls (inline_calls {v:T=vo; e'} x3) = call e'; call (x1\<bullet>x2(x3)) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1\<bullet>x2(x3))) = call e'
 7. \<And>x1 x2 x3 x4. \<lbrakk>call x4 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x4) = call e'; call {x1:x2=x3; x4} = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} {x1:x2=x3; x4}) = call e'
 8. \<And>x1 x2 x3. \<lbrakk>call x2 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x2) = call e'; call x3 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x3) = call e'; call (sync\<^bsub>x1\<^esub> (x2) x3) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (sync\<^bsub>x1\<^esub> (x2) x3)) = call e'
 9. \<And>x1 x2 x3. \<lbrakk>call x3 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x3) = call e'; call (insync\<^bsub>x1\<^esub> (x2) x3) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (insync\<^bsub>x1\<^esub> (x2) x3)) = call e'
 10. \<And>x1 x2. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call x2 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x2) = call e'; call (x1;; x2) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1;; x2)) = call e'
A total of 16 subgoals...
[PROOF STEP]
apply(clarsimp)
[PROOF STATE]
proof (prove)
goal (17 subgoals):
 1. \<And>x2 x3. \<lbrakk>call (inline_call {v:T=vo; e'} x2) = call e'; call x3 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x3) = call e'; \<not> is_val x2; call x2 = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> (if is_val (inline_call {v:T=vo; e'} x2) then call x3 else call (inline_call {v:T=vo; e'} x2)) = call e'
 2. \<And>x1 x2 x3. \<lbrakk>call (inline_call {v:T=vo; e'} x1) = call e'; call x2 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x2) = call e'; call x3 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x3) = call e'; \<not> is_val x1; call x1 = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> (if is_val (inline_call {v:T=vo; e'} x1) then if is_val x2 then call x3 else call x2 else call (inline_call {v:T=vo; e'} x1)) = call e'
 3. \<And>x. \<lbrakk>call x = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x) = call e'; call (x\<bullet>length) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x\<bullet>length)) = call e'
 4. \<And>x1 x2 x3. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call (x1\<bullet>x2{x3}) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1\<bullet>x2{x3})) = call e'
 5. \<And>x1 x2 x3 x4. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call x4 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x4) = call e'; call (x1\<bullet>x2{x3} := x4) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1\<bullet>x2{x3} := x4)) = call e'
 6. \<And>x1 x2 x3 x4 x5. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call x4 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x4) = call e'; call x5 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x5) = call e'; call (x1\<bullet>compareAndSwap(x2\<bullet>x3, x4, x5)) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1\<bullet>compareAndSwap(x2\<bullet>x3, x4, x5))) = call e'
 7. \<And>x1 x2 x3. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; calls x3 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> calls (inline_calls {v:T=vo; e'} x3) = call e'; call (x1\<bullet>x2(x3)) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1\<bullet>x2(x3))) = call e'
 8. \<And>x1 x2 x3 x4. \<lbrakk>call x4 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x4) = call e'; call {x1:x2=x3; x4} = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} {x1:x2=x3; x4}) = call e'
 9. \<And>x1 x2 x3. \<lbrakk>call x2 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x2) = call e'; call x3 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x3) = call e'; call (sync\<^bsub>x1\<^esub> (x2) x3) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (sync\<^bsub>x1\<^esub> (x2) x3)) = call e'
 10. \<And>x1 x2 x3. \<lbrakk>call x3 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x3) = call e'; call (insync\<^bsub>x1\<^esub> (x2) x3) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (insync\<^bsub>x1\<^esub> (x2) x3)) = call e'
A total of 17 subgoals...
[PROOF STEP]
apply(fastforce split: if_split)
[PROOF STATE]
proof (prove)
goal (16 subgoals):
 1. \<And>x1 x2 x3. \<lbrakk>call (inline_call {v:T=vo; e'} x1) = call e'; call x2 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x2) = call e'; call x3 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x3) = call e'; \<not> is_val x1; call x1 = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> (if is_val (inline_call {v:T=vo; e'} x1) then if is_val x2 then call x3 else call x2 else call (inline_call {v:T=vo; e'} x1)) = call e'
 2. \<And>x. \<lbrakk>call x = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x) = call e'; call (x\<bullet>length) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x\<bullet>length)) = call e'
 3. \<And>x1 x2 x3. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call (x1\<bullet>x2{x3}) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1\<bullet>x2{x3})) = call e'
 4. \<And>x1 x2 x3 x4. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call x4 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x4) = call e'; call (x1\<bullet>x2{x3} := x4) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1\<bullet>x2{x3} := x4)) = call e'
 5. \<And>x1 x2 x3 x4 x5. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call x4 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x4) = call e'; call x5 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x5) = call e'; call (x1\<bullet>compareAndSwap(x2\<bullet>x3, x4, x5)) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1\<bullet>compareAndSwap(x2\<bullet>x3, x4, x5))) = call e'
 6. \<And>x1 x2 x3. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; calls x3 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> calls (inline_calls {v:T=vo; e'} x3) = call e'; call (x1\<bullet>x2(x3)) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1\<bullet>x2(x3))) = call e'
 7. \<And>x1 x2 x3 x4. \<lbrakk>call x4 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x4) = call e'; call {x1:x2=x3; x4} = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} {x1:x2=x3; x4}) = call e'
 8. \<And>x1 x2 x3. \<lbrakk>call x2 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x2) = call e'; call x3 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x3) = call e'; call (sync\<^bsub>x1\<^esub> (x2) x3) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (sync\<^bsub>x1\<^esub> (x2) x3)) = call e'
 9. \<And>x1 x2 x3. \<lbrakk>call x3 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x3) = call e'; call (insync\<^bsub>x1\<^esub> (x2) x3) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (insync\<^bsub>x1\<^esub> (x2) x3)) = call e'
 10. \<And>x1 x2. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call x2 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x2) = call e'; call (x1;; x2) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1;; x2)) = call e'
A total of 16 subgoals...
[PROOF STEP]
apply(fastforce split: if_split)
[PROOF STATE]
proof (prove)
goal (15 subgoals):
 1. \<And>x. \<lbrakk>call x = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x) = call e'; call (x\<bullet>length) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x\<bullet>length)) = call e'
 2. \<And>x1 x2 x3. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call (x1\<bullet>x2{x3}) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1\<bullet>x2{x3})) = call e'
 3. \<And>x1 x2 x3 x4. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call x4 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x4) = call e'; call (x1\<bullet>x2{x3} := x4) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1\<bullet>x2{x3} := x4)) = call e'
 4. \<And>x1 x2 x3 x4 x5. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call x4 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x4) = call e'; call x5 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x5) = call e'; call (x1\<bullet>compareAndSwap(x2\<bullet>x3, x4, x5)) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1\<bullet>compareAndSwap(x2\<bullet>x3, x4, x5))) = call e'
 5. \<And>x1 x2 x3. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; calls x3 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> calls (inline_calls {v:T=vo; e'} x3) = call e'; call (x1\<bullet>x2(x3)) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1\<bullet>x2(x3))) = call e'
 6. \<And>x1 x2 x3 x4. \<lbrakk>call x4 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x4) = call e'; call {x1:x2=x3; x4} = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} {x1:x2=x3; x4}) = call e'
 7. \<And>x1 x2 x3. \<lbrakk>call x2 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x2) = call e'; call x3 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x3) = call e'; call (sync\<^bsub>x1\<^esub> (x2) x3) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (sync\<^bsub>x1\<^esub> (x2) x3)) = call e'
 8. \<And>x1 x2 x3. \<lbrakk>call x3 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x3) = call e'; call (insync\<^bsub>x1\<^esub> (x2) x3) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (insync\<^bsub>x1\<^esub> (x2) x3)) = call e'
 9. \<And>x1 x2. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call x2 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x2) = call e'; call (x1;; x2) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1;; x2)) = call e'
 10. \<And>x1 x2 x3. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call x2 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x2) = call e'; call x3 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x3) = call e'; call (if (x1) x2 else x3) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (if (x1) x2 else x3)) = call e'
A total of 15 subgoals...
[PROOF STEP]
apply(fastforce)
[PROOF STATE]
proof (prove)
goal (14 subgoals):
 1. \<And>x1 x2 x3. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call (x1\<bullet>x2{x3}) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1\<bullet>x2{x3})) = call e'
 2. \<And>x1 x2 x3 x4. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call x4 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x4) = call e'; call (x1\<bullet>x2{x3} := x4) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1\<bullet>x2{x3} := x4)) = call e'
 3. \<And>x1 x2 x3 x4 x5. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call x4 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x4) = call e'; call x5 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x5) = call e'; call (x1\<bullet>compareAndSwap(x2\<bullet>x3, x4, x5)) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1\<bullet>compareAndSwap(x2\<bullet>x3, x4, x5))) = call e'
 4. \<And>x1 x2 x3. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; calls x3 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> calls (inline_calls {v:T=vo; e'} x3) = call e'; call (x1\<bullet>x2(x3)) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1\<bullet>x2(x3))) = call e'
 5. \<And>x1 x2 x3 x4. \<lbrakk>call x4 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x4) = call e'; call {x1:x2=x3; x4} = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} {x1:x2=x3; x4}) = call e'
 6. \<And>x1 x2 x3. \<lbrakk>call x2 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x2) = call e'; call x3 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x3) = call e'; call (sync\<^bsub>x1\<^esub> (x2) x3) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (sync\<^bsub>x1\<^esub> (x2) x3)) = call e'
 7. \<And>x1 x2 x3. \<lbrakk>call x3 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x3) = call e'; call (insync\<^bsub>x1\<^esub> (x2) x3) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (insync\<^bsub>x1\<^esub> (x2) x3)) = call e'
 8. \<And>x1 x2. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call x2 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x2) = call e'; call (x1;; x2) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1;; x2)) = call e'
 9. \<And>x1 x2 x3. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call x2 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x2) = call e'; call x3 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x3) = call e'; call (if (x1) x2 else x3) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (if (x1) x2 else x3)) = call e'
 10. \<And>x1 x2. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call x2 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x2) = call e'; call (while (x1) x2) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (while (x1) x2)) = call e'
A total of 14 subgoals...
[PROOF STEP]
apply(fastforce)
[PROOF STATE]
proof (prove)
goal (13 subgoals):
 1. \<And>x1 x2 x3 x4. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call x4 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x4) = call e'; call (x1\<bullet>x2{x3} := x4) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1\<bullet>x2{x3} := x4)) = call e'
 2. \<And>x1 x2 x3 x4 x5. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call x4 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x4) = call e'; call x5 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x5) = call e'; call (x1\<bullet>compareAndSwap(x2\<bullet>x3, x4, x5)) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1\<bullet>compareAndSwap(x2\<bullet>x3, x4, x5))) = call e'
 3. \<And>x1 x2 x3. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; calls x3 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> calls (inline_calls {v:T=vo; e'} x3) = call e'; call (x1\<bullet>x2(x3)) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1\<bullet>x2(x3))) = call e'
 4. \<And>x1 x2 x3 x4. \<lbrakk>call x4 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x4) = call e'; call {x1:x2=x3; x4} = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} {x1:x2=x3; x4}) = call e'
 5. \<And>x1 x2 x3. \<lbrakk>call x2 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x2) = call e'; call x3 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x3) = call e'; call (sync\<^bsub>x1\<^esub> (x2) x3) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (sync\<^bsub>x1\<^esub> (x2) x3)) = call e'
 6. \<And>x1 x2 x3. \<lbrakk>call x3 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x3) = call e'; call (insync\<^bsub>x1\<^esub> (x2) x3) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (insync\<^bsub>x1\<^esub> (x2) x3)) = call e'
 7. \<And>x1 x2. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call x2 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x2) = call e'; call (x1;; x2) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1;; x2)) = call e'
 8. \<And>x1 x2 x3. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call x2 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x2) = call e'; call x3 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x3) = call e'; call (if (x1) x2 else x3) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (if (x1) x2 else x3)) = call e'
 9. \<And>x1 x2. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call x2 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x2) = call e'; call (while (x1) x2) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (while (x1) x2)) = call e'
 10. \<And>x. \<lbrakk>call x = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x) = call e'; call (throw x) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (throw x)) = call e'
A total of 13 subgoals...
[PROOF STEP]
apply(fastforce split: if_split)
[PROOF STATE]
proof (prove)
goal (12 subgoals):
 1. \<And>x1 x2 x3 x4 x5. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call x4 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x4) = call e'; call x5 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x5) = call e'; call (x1\<bullet>compareAndSwap(x2\<bullet>x3, x4, x5)) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1\<bullet>compareAndSwap(x2\<bullet>x3, x4, x5))) = call e'
 2. \<And>x1 x2 x3. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; calls x3 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> calls (inline_calls {v:T=vo; e'} x3) = call e'; call (x1\<bullet>x2(x3)) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1\<bullet>x2(x3))) = call e'
 3. \<And>x1 x2 x3 x4. \<lbrakk>call x4 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x4) = call e'; call {x1:x2=x3; x4} = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} {x1:x2=x3; x4}) = call e'
 4. \<And>x1 x2 x3. \<lbrakk>call x2 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x2) = call e'; call x3 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x3) = call e'; call (sync\<^bsub>x1\<^esub> (x2) x3) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (sync\<^bsub>x1\<^esub> (x2) x3)) = call e'
 5. \<And>x1 x2 x3. \<lbrakk>call x3 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x3) = call e'; call (insync\<^bsub>x1\<^esub> (x2) x3) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (insync\<^bsub>x1\<^esub> (x2) x3)) = call e'
 6. \<And>x1 x2. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call x2 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x2) = call e'; call (x1;; x2) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1;; x2)) = call e'
 7. \<And>x1 x2 x3. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call x2 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x2) = call e'; call x3 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x3) = call e'; call (if (x1) x2 else x3) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (if (x1) x2 else x3)) = call e'
 8. \<And>x1 x2. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call x2 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x2) = call e'; call (while (x1) x2) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (while (x1) x2)) = call e'
 9. \<And>x. \<lbrakk>call x = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x) = call e'; call (throw x) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (throw x)) = call e'
 10. \<And>x1 x2 x3 x4. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call x4 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x4) = call e'; call (try x1 catch(x2 x3) x4) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (try x1 catch(x2 x3) x4)) = call e'
A total of 12 subgoals...
[PROOF STEP]
apply(fastforce split: if_split)
[PROOF STATE]
proof (prove)
goal (11 subgoals):
 1. \<And>x1 x2 x3. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; calls x3 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> calls (inline_calls {v:T=vo; e'} x3) = call e'; call (x1\<bullet>x2(x3)) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1\<bullet>x2(x3))) = call e'
 2. \<And>x1 x2 x3 x4. \<lbrakk>call x4 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x4) = call e'; call {x1:x2=x3; x4} = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} {x1:x2=x3; x4}) = call e'
 3. \<And>x1 x2 x3. \<lbrakk>call x2 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x2) = call e'; call x3 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x3) = call e'; call (sync\<^bsub>x1\<^esub> (x2) x3) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (sync\<^bsub>x1\<^esub> (x2) x3)) = call e'
 4. \<And>x1 x2 x3. \<lbrakk>call x3 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x3) = call e'; call (insync\<^bsub>x1\<^esub> (x2) x3) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (insync\<^bsub>x1\<^esub> (x2) x3)) = call e'
 5. \<And>x1 x2. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call x2 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x2) = call e'; call (x1;; x2) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1;; x2)) = call e'
 6. \<And>x1 x2 x3. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call x2 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x2) = call e'; call x3 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x3) = call e'; call (if (x1) x2 else x3) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (if (x1) x2 else x3)) = call e'
 7. \<And>x1 x2. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call x2 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x2) = call e'; call (while (x1) x2) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (while (x1) x2)) = call e'
 8. \<And>x. \<lbrakk>call x = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x) = call e'; call (throw x) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (throw x)) = call e'
 9. \<And>x1 x2 x3 x4. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call x4 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x4) = call e'; call (try x1 catch(x2 x3) x4) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (try x1 catch(x2 x3) x4)) = call e'
 10. calls [] = \<lfloor>aMvs\<rfloor> \<Longrightarrow> calls (inline_calls {v:T=vo; e'} []) = call e'
A total of 11 subgoals...
[PROOF STEP]
apply(fastforce split: if_split)
[PROOF STATE]
proof (prove)
goal (10 subgoals):
 1. \<And>x1 x2 x3 x4. \<lbrakk>call x4 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x4) = call e'; call {x1:x2=x3; x4} = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} {x1:x2=x3; x4}) = call e'
 2. \<And>x1 x2 x3. \<lbrakk>call x2 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x2) = call e'; call x3 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x3) = call e'; call (sync\<^bsub>x1\<^esub> (x2) x3) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (sync\<^bsub>x1\<^esub> (x2) x3)) = call e'
 3. \<And>x1 x2 x3. \<lbrakk>call x3 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x3) = call e'; call (insync\<^bsub>x1\<^esub> (x2) x3) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (insync\<^bsub>x1\<^esub> (x2) x3)) = call e'
 4. \<And>x1 x2. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call x2 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x2) = call e'; call (x1;; x2) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1;; x2)) = call e'
 5. \<And>x1 x2 x3. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call x2 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x2) = call e'; call x3 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x3) = call e'; call (if (x1) x2 else x3) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (if (x1) x2 else x3)) = call e'
 6. \<And>x1 x2. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call x2 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x2) = call e'; call (while (x1) x2) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (while (x1) x2)) = call e'
 7. \<And>x. \<lbrakk>call x = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x) = call e'; call (throw x) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (throw x)) = call e'
 8. \<And>x1 x2 x3 x4. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call x4 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x4) = call e'; call (try x1 catch(x2 x3) x4) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (try x1 catch(x2 x3) x4)) = call e'
 9. calls [] = \<lfloor>aMvs\<rfloor> \<Longrightarrow> calls (inline_calls {v:T=vo; e'} []) = call e'
 10. \<And>x1 x2. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; calls x2 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> calls (inline_calls {v:T=vo; e'} x2) = call e'; calls (x1 # x2) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> calls (inline_calls {v:T=vo; e'} (x1 # x2)) = call e'
[PROOF STEP]
apply(fastforce)
[PROOF STATE]
proof (prove)
goal (9 subgoals):
 1. \<And>x1 x2 x3. \<lbrakk>call x2 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x2) = call e'; call x3 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x3) = call e'; call (sync\<^bsub>x1\<^esub> (x2) x3) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (sync\<^bsub>x1\<^esub> (x2) x3)) = call e'
 2. \<And>x1 x2 x3. \<lbrakk>call x3 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x3) = call e'; call (insync\<^bsub>x1\<^esub> (x2) x3) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (insync\<^bsub>x1\<^esub> (x2) x3)) = call e'
 3. \<And>x1 x2. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call x2 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x2) = call e'; call (x1;; x2) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1;; x2)) = call e'
 4. \<And>x1 x2 x3. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call x2 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x2) = call e'; call x3 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x3) = call e'; call (if (x1) x2 else x3) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (if (x1) x2 else x3)) = call e'
 5. \<And>x1 x2. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call x2 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x2) = call e'; call (while (x1) x2) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (while (x1) x2)) = call e'
 6. \<And>x. \<lbrakk>call x = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x) = call e'; call (throw x) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (throw x)) = call e'
 7. \<And>x1 x2 x3 x4. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call x4 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x4) = call e'; call (try x1 catch(x2 x3) x4) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (try x1 catch(x2 x3) x4)) = call e'
 8. calls [] = \<lfloor>aMvs\<rfloor> \<Longrightarrow> calls (inline_calls {v:T=vo; e'} []) = call e'
 9. \<And>x1 x2. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; calls x2 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> calls (inline_calls {v:T=vo; e'} x2) = call e'; calls (x1 # x2) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> calls (inline_calls {v:T=vo; e'} (x1 # x2)) = call e'
[PROOF STEP]
apply(fastforce)
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<And>x1 x2 x3. \<lbrakk>call x3 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x3) = call e'; call (insync\<^bsub>x1\<^esub> (x2) x3) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (insync\<^bsub>x1\<^esub> (x2) x3)) = call e'
 2. \<And>x1 x2. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call x2 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x2) = call e'; call (x1;; x2) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1;; x2)) = call e'
 3. \<And>x1 x2 x3. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call x2 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x2) = call e'; call x3 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x3) = call e'; call (if (x1) x2 else x3) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (if (x1) x2 else x3)) = call e'
 4. \<And>x1 x2. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call x2 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x2) = call e'; call (while (x1) x2) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (while (x1) x2)) = call e'
 5. \<And>x. \<lbrakk>call x = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x) = call e'; call (throw x) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (throw x)) = call e'
 6. \<And>x1 x2 x3 x4. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call x4 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x4) = call e'; call (try x1 catch(x2 x3) x4) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (try x1 catch(x2 x3) x4)) = call e'
 7. calls [] = \<lfloor>aMvs\<rfloor> \<Longrightarrow> calls (inline_calls {v:T=vo; e'} []) = call e'
 8. \<And>x1 x2. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; calls x2 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> calls (inline_calls {v:T=vo; e'} x2) = call e'; calls (x1 # x2) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> calls (inline_calls {v:T=vo; e'} (x1 # x2)) = call e'
[PROOF STEP]
apply(fastforce)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>x1 x2. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call x2 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x2) = call e'; call (x1;; x2) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (x1;; x2)) = call e'
 2. \<And>x1 x2 x3. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call x2 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x2) = call e'; call x3 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x3) = call e'; call (if (x1) x2 else x3) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (if (x1) x2 else x3)) = call e'
 3. \<And>x1 x2. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call x2 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x2) = call e'; call (while (x1) x2) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (while (x1) x2)) = call e'
 4. \<And>x. \<lbrakk>call x = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x) = call e'; call (throw x) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (throw x)) = call e'
 5. \<And>x1 x2 x3 x4. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call x4 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x4) = call e'; call (try x1 catch(x2 x3) x4) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (try x1 catch(x2 x3) x4)) = call e'
 6. calls [] = \<lfloor>aMvs\<rfloor> \<Longrightarrow> calls (inline_calls {v:T=vo; e'} []) = call e'
 7. \<And>x1 x2. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; calls x2 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> calls (inline_calls {v:T=vo; e'} x2) = call e'; calls (x1 # x2) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> calls (inline_calls {v:T=vo; e'} (x1 # x2)) = call e'
[PROOF STEP]
apply(fastforce)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>x1 x2 x3. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call x2 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x2) = call e'; call x3 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x3) = call e'; call (if (x1) x2 else x3) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (if (x1) x2 else x3)) = call e'
 2. \<And>x1 x2. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call x2 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x2) = call e'; call (while (x1) x2) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (while (x1) x2)) = call e'
 3. \<And>x. \<lbrakk>call x = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x) = call e'; call (throw x) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (throw x)) = call e'
 4. \<And>x1 x2 x3 x4. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call x4 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x4) = call e'; call (try x1 catch(x2 x3) x4) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (try x1 catch(x2 x3) x4)) = call e'
 5. calls [] = \<lfloor>aMvs\<rfloor> \<Longrightarrow> calls (inline_calls {v:T=vo; e'} []) = call e'
 6. \<And>x1 x2. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; calls x2 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> calls (inline_calls {v:T=vo; e'} x2) = call e'; calls (x1 # x2) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> calls (inline_calls {v:T=vo; e'} (x1 # x2)) = call e'
[PROOF STEP]
apply(fastforce)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x1 x2. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call x2 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x2) = call e'; call (while (x1) x2) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (while (x1) x2)) = call e'
 2. \<And>x. \<lbrakk>call x = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x) = call e'; call (throw x) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (throw x)) = call e'
 3. \<And>x1 x2 x3 x4. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call x4 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x4) = call e'; call (try x1 catch(x2 x3) x4) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (try x1 catch(x2 x3) x4)) = call e'
 4. calls [] = \<lfloor>aMvs\<rfloor> \<Longrightarrow> calls (inline_calls {v:T=vo; e'} []) = call e'
 5. \<And>x1 x2. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; calls x2 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> calls (inline_calls {v:T=vo; e'} x2) = call e'; calls (x1 # x2) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> calls (inline_calls {v:T=vo; e'} (x1 # x2)) = call e'
[PROOF STEP]
apply(fastforce)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>call x = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x) = call e'; call (throw x) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (throw x)) = call e'
 2. \<And>x1 x2 x3 x4. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call x4 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x4) = call e'; call (try x1 catch(x2 x3) x4) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (try x1 catch(x2 x3) x4)) = call e'
 3. calls [] = \<lfloor>aMvs\<rfloor> \<Longrightarrow> calls (inline_calls {v:T=vo; e'} []) = call e'
 4. \<And>x1 x2. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; calls x2 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> calls (inline_calls {v:T=vo; e'} x2) = call e'; calls (x1 # x2) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> calls (inline_calls {v:T=vo; e'} (x1 # x2)) = call e'
[PROOF STEP]
apply(fastforce)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x1 x2 x3 x4. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; call x4 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x4) = call e'; call (try x1 catch(x2 x3) x4) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> call (inline_call {v:T=vo; e'} (try x1 catch(x2 x3) x4)) = call e'
 2. calls [] = \<lfloor>aMvs\<rfloor> \<Longrightarrow> calls (inline_calls {v:T=vo; e'} []) = call e'
 3. \<And>x1 x2. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; calls x2 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> calls (inline_calls {v:T=vo; e'} x2) = call e'; calls (x1 # x2) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> calls (inline_calls {v:T=vo; e'} (x1 # x2)) = call e'
[PROOF STEP]
apply(fastforce)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. calls [] = \<lfloor>aMvs\<rfloor> \<Longrightarrow> calls (inline_calls {v:T=vo; e'} []) = call e'
 2. \<And>x1 x2. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; calls x2 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> calls (inline_calls {v:T=vo; e'} x2) = call e'; calls (x1 # x2) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> calls (inline_calls {v:T=vo; e'} (x1 # x2)) = call e'
[PROOF STEP]
apply(fastforce)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>call x1 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> call (inline_call {v:T=vo; e'} x1) = call e'; calls x2 = \<lfloor>aMvs\<rfloor> \<Longrightarrow> calls (inline_calls {v:T=vo; e'} x2) = call e'; calls (x1 # x2) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> calls (inline_calls {v:T=vo; e'} (x1 # x2)) = call e'
[PROOF STEP]
apply(fastforce split: if_split)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma fv_inline_call: "fv (inline_call e' e) \<subseteq> fv e \<union> fv e'"
  and fvs_inline_calls: "fvs (inline_calls e' es) \<subseteq> fvs es \<union> fv e'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fv (inline_call e' e) \<subseteq> fv e \<union> fv e' &&& fvs (inline_calls e' es) \<subseteq> fvs es \<union> fv e'
[PROOF STEP]
by(induct e and es rule: call.induct calls.induct)(fastforce split: if_split_asm)+


[STATEMENT]
lemma contains_insync_inline_call_conv:
  "contains_insync (inline_call e e') \<longleftrightarrow> contains_insync e \<and> call e' \<noteq> None \<or> contains_insync e'"
  and contains_insyncs_inline_calls_conv:
  "contains_insyncs (inline_calls e es') \<longleftrightarrow> contains_insync e \<and> calls es' \<noteq> None \<or> contains_insyncs es'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. contains_insync (inline_call e e') = (contains_insync e \<and> call e' \<noteq> None \<or> contains_insync e') &&& contains_insyncs (inline_calls e es') = (contains_insync e \<and> calls es' \<noteq> None \<or> contains_insyncs es')
[PROOF STEP]
by(induct e' and es' rule: call.induct calls.induct)(auto split: if_split_asm simp add: is_vals_conv)


[STATEMENT]
lemma contains_insync_inline_call [simp]:
  "call e' = \<lfloor>aMvs\<rfloor> \<Longrightarrow> contains_insync (inline_call e e') \<longleftrightarrow> contains_insync e \<or> contains_insync e'"
  and contains_insyncs_inline_calls [simp]:
  "calls es' = \<lfloor>aMvs\<rfloor> \<Longrightarrow> contains_insyncs (inline_calls e es') \<longleftrightarrow> contains_insync e \<or> contains_insyncs es'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (call e' = \<lfloor>aMvs\<rfloor> \<Longrightarrow> contains_insync (inline_call e e') = (contains_insync e \<or> contains_insync e')) &&& (calls es' = \<lfloor>aMvs\<rfloor> \<Longrightarrow> contains_insyncs (inline_calls e es') = (contains_insync e \<or> contains_insyncs es'))
[PROOF STEP]
by(simp_all add: contains_insync_inline_call_conv contains_insyncs_inline_calls_conv)


[STATEMENT]
lemma collapse_append [simp]:
  "collapse (e, es @ es') = collapse (collapse (e, es), es')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. collapse (e, es @ es') = collapse (collapse (e, es), es')
[PROOF STEP]
by(induct es arbitrary: e, auto)


[STATEMENT]
lemma collapse_conv_foldl:
  "collapse (e, es) = foldl inline_call e es"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. collapse (e, es) = foldl inline_call e es
[PROOF STEP]
by(induct es arbitrary: e) simp_all


[STATEMENT]
lemma fv_collapse: "\<forall>e \<in> set es. is_call e \<Longrightarrow> fv (collapse (e, es)) \<subseteq> fvs (e # es)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>e\<in>set es. is_call e \<Longrightarrow> fv (collapse (e, es)) \<subseteq> fvs (e # es)
[PROOF STEP]
apply(induct es arbitrary: e)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>e. Ball (set []) is_call \<Longrightarrow> fv (collapse (e, [])) \<subseteq> fvs [e]
 2. \<And>a es e. \<lbrakk>\<And>e. Ball (set es) is_call \<Longrightarrow> fv (collapse (e, es)) \<subseteq> fvs (e # es); Ball (set (a # es)) is_call\<rbrakk> \<Longrightarrow> fv (collapse (e, a # es)) \<subseteq> fvs (e # a # es)
[PROOF STEP]
apply(insert fv_inline_call)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>e. \<lbrakk>Ball (set []) is_call; \<And>e' e. fv (inline_call e' e) \<subseteq> fv e \<union> fv e'\<rbrakk> \<Longrightarrow> fv (collapse (e, [])) \<subseteq> fvs [e]
 2. \<And>a es e. \<lbrakk>\<And>e. Ball (set es) is_call \<Longrightarrow> fv (collapse (e, es)) \<subseteq> fvs (e # es); Ball (set (a # es)) is_call; \<And>e' e. fv (inline_call e' e) \<subseteq> fv e \<union> fv e'\<rbrakk> \<Longrightarrow> fv (collapse (e, a # es)) \<subseteq> fvs (e # a # es)
[PROOF STEP]
apply(fastforce dest: subsetD)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma final_inline_callD: "\<lbrakk> final (inline_call E e); is_call e \<rbrakk> \<Longrightarrow> final E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>final (inline_call E e); is_call e\<rbrakk> \<Longrightarrow> final E
[PROOF STEP]
by(induct e)(auto simp add: is_call_def split: if_split_asm)


[STATEMENT]
lemma collapse_finalD: "\<lbrakk> final (collapse (e, es)); \<forall>e\<in>set es. is_call e \<rbrakk> \<Longrightarrow> final e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>final (collapse (e, es)); \<forall>e\<in>set es. is_call e\<rbrakk> \<Longrightarrow> final e
[PROOF STEP]
by(induct es arbitrary: e)(auto dest: final_inline_callD)


[STATEMENT]
lemma synthesized_call_conv:
  "synthesized_call P h (a, M, vs) =
   (\<exists>T Ts Tr D. typeof_addr h a = \<lfloor>T\<rfloor> \<and> P \<turnstile> class_type_of T sees M:Ts\<rightarrow>Tr = Native in D)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. synthesized_call P h (a, M, vs) = (\<exists>T Ts Tr D. typeof_addr h a = \<lfloor>T\<rfloor> \<and> P \<turnstile> class_type_of T sees M: Ts\<rightarrow>Tr = Native in D)
[PROOF STEP]
by(simp add: synthesized_call_def)


[STATEMENT]
lemma max_stack1: "P,E \<turnstile>\<^sub>1 e :: T \<Longrightarrow> 1 \<le> max_stack e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P,E \<turnstile>\<^sub>1 e :: T \<Longrightarrow> 1 \<le> max_stack e
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P,E \<turnstile>\<^sub>1 e :: T \<Longrightarrow> 1 \<le> max_stack e
[PROOF STEP]
using max_stack1'[OF WT\<^sub>1_nsub_RI]
[PROOF STATE]
proof (prove)
using this:
?P1,?E1 \<turnstile>\<^sub>1 ?e :: ?T1 \<Longrightarrow> 1 \<le> max_stack ?e

goal (1 subgoal):
 1. P,E \<turnstile>\<^sub>1 e :: T \<Longrightarrow> 1 \<le> max_stack e
[PROOF STEP]
by simp


[STATEMENT]
lemma (in TC0) ty_def2 [simp]: "P,E \<turnstile>\<^sub>1 e :: T \<Longrightarrow> ty E e = T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P,E \<turnstile>\<^sub>1 e :: T \<Longrightarrow> ty E e = T
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P,E \<turnstile>\<^sub>1 e :: T \<Longrightarrow> ty E e = T
[PROOF STEP]
by(unfold ty_def) (blast intro: the_equality WT\<^sub>1_unique)


[STATEMENT]
lemma (in TC0) [simp]: "ty\<^sub>i' ST E None = None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ty\<^sub>i' ST E None = None
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ty\<^sub>i' ST E None = None
[PROOF STEP]
by (simp add: ty\<^sub>i'_def)


[STATEMENT]
lemma (in TC0) ty\<^sub>l_app_diff[simp]:
 "ty\<^sub>l (E@[T]) (A - {size E}) = ty\<^sub>l E A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ty\<^sub>l (E @ [T]) (A - {length E}) = ty\<^sub>l E A
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ty\<^sub>l (E @ [T]) (A - {length E}) = ty\<^sub>l E A
[PROOF STEP]
by(auto simp add:ty\<^sub>l_def hyperset_defs)


[STATEMENT]
lemma (in TC0) ty\<^sub>i'_app_diff[simp]:
 "ty\<^sub>i' ST (E @ [T]) (A \<ominus> size E) = ty\<^sub>i' ST E A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ty\<^sub>i' ST (E @ [T]) (A \<ominus> length E) = ty\<^sub>i' ST E A
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ty\<^sub>i' ST (E @ [T]) (A \<ominus> length E) = ty\<^sub>i' ST E A
[PROOF STEP]
by(auto simp add:ty\<^sub>i'_def hyperset_defs)


[STATEMENT]
lemma (in TC0) ty\<^sub>l_antimono:
 "A \<subseteq> A' \<Longrightarrow> P \<turnstile> ty\<^sub>l E A' [\<le>\<^sub>\<top>] ty\<^sub>l E A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<subseteq> A' \<Longrightarrow> P \<turnstile> ty\<^sub>l E A' [\<le>\<^sub>\<top>] ty\<^sub>l E A
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<subseteq> A' \<Longrightarrow> P \<turnstile> ty\<^sub>l E A' [\<le>\<^sub>\<top>] ty\<^sub>l E A
[PROOF STEP]
by(auto simp:ty\<^sub>l_def list_all2_conv_all_nth)


[STATEMENT]
lemma (in TC0) ty\<^sub>i'_antimono:
 "A \<subseteq> A' \<Longrightarrow> P \<turnstile> ty\<^sub>i' ST E \<lfloor>A'\<rfloor> \<le>' ty\<^sub>i' ST E \<lfloor>A\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<subseteq> A' \<Longrightarrow> P \<turnstile> ty\<^sub>i' ST E \<lfloor>A'\<rfloor> \<le>' ty\<^sub>i' ST E \<lfloor>A\<rfloor>
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<subseteq> A' \<Longrightarrow> P \<turnstile> ty\<^sub>i' ST E \<lfloor>A'\<rfloor> \<le>' ty\<^sub>i' ST E \<lfloor>A\<rfloor>
[PROOF STEP]
by(auto simp:ty\<^sub>i'_def ty\<^sub>l_def list_all2_conv_all_nth)


[STATEMENT]
lemma (in TC0) ty\<^sub>l_env_antimono:
 "P \<turnstile> ty\<^sub>l (E@[T]) A [\<le>\<^sub>\<top>] ty\<^sub>l E A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> ty\<^sub>l (E @ [T]) A [\<le>\<^sub>\<top>] ty\<^sub>l E A
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> ty\<^sub>l (E @ [T]) A [\<le>\<^sub>\<top>] ty\<^sub>l E A
[PROOF STEP]
by(auto simp:ty\<^sub>l_def list_all2_conv_all_nth)


[STATEMENT]
lemma (in TC0) ty\<^sub>i'_env_antimono:
 "P \<turnstile> ty\<^sub>i' ST (E@[T]) A \<le>' ty\<^sub>i' ST E A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> ty\<^sub>i' ST (E @ [T]) A \<le>' ty\<^sub>i' ST E A
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> ty\<^sub>i' ST (E @ [T]) A \<le>' ty\<^sub>i' ST E A
[PROOF STEP]
by(auto simp:ty\<^sub>i'_def ty\<^sub>l_def list_all2_conv_all_nth)


[STATEMENT]
lemma (in TC0) ty\<^sub>i'_incr:
 "P \<turnstile> ty\<^sub>i' ST (E @ [T]) \<lfloor>insert (size E) A\<rfloor> \<le>' ty\<^sub>i' ST E \<lfloor>A\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> ty\<^sub>i' ST (E @ [T]) \<lfloor>insert (length E) A\<rfloor> \<le>' ty\<^sub>i' ST E \<lfloor>A\<rfloor>
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> ty\<^sub>i' ST (E @ [T]) \<lfloor>insert (length E) A\<rfloor> \<le>' ty\<^sub>i' ST E \<lfloor>A\<rfloor>
[PROOF STEP]
by(auto simp:ty\<^sub>i'_def ty\<^sub>l_def list_all2_conv_all_nth)


[STATEMENT]
lemma (in TC0) ty\<^sub>l_incr:
 "P \<turnstile> ty\<^sub>l (E @ [T]) (insert (size E) A) [\<le>\<^sub>\<top>] ty\<^sub>l E A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> ty\<^sub>l (E @ [T]) (insert (length E) A) [\<le>\<^sub>\<top>] ty\<^sub>l E A
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> ty\<^sub>l (E @ [T]) (insert (length E) A) [\<le>\<^sub>\<top>] ty\<^sub>l E A
[PROOF STEP]
by(auto simp: hyperset_defs ty\<^sub>l_def list_all2_conv_all_nth)


[STATEMENT]
lemma (in TC0) ty\<^sub>l_in_types:
 "set E \<subseteq> types P \<Longrightarrow> ty\<^sub>l E A \<in> nlists mxl (err (types P))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set E \<subseteq> types P \<Longrightarrow> ty\<^sub>l E A \<in> nlists mxl (err (types P))
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set E \<subseteq> types P \<Longrightarrow> ty\<^sub>l E A \<in> nlists mxl (err (types P))
[PROOF STEP]
by(auto simp add:ty\<^sub>l_def intro!:nlistsI dest!: nth_mem)


[STATEMENT]
lemma compE\<^sub>2_not_Nil[simp]: "P,E \<turnstile>\<^sub>1 e :: T \<Longrightarrow> compE\<^sub>2 e \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P,E \<turnstile>\<^sub>1 e :: T \<Longrightarrow> compE\<^sub>2 e \<noteq> []
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P,E \<turnstile>\<^sub>1 e :: T \<Longrightarrow> compE\<^sub>2 e \<noteq> []
[PROOF STEP]
by(simp add: compE\<^sub>2_not_Nil' WT\<^sub>1_nsub_RI)


[STATEMENT]
lemma (in TC1) compT_sizes':
shows "\<And>E A ST. \<not>sub_RI e \<Longrightarrow> size(compT E A ST e) = size(compE\<^sub>2 e) - 1"
and "\<And>E A ST. \<not>sub_RIs es \<Longrightarrow> size(compTs E A ST es) = size(compEs\<^sub>2 es)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>E A ST. \<not> sub_RI e \<Longrightarrow> length (compT E A ST e) = length (compE\<^sub>2 e) - 1) &&& (\<And>E A ST. \<not> sub_RIs es \<Longrightarrow> length (compTs E A ST es) = length (compEs\<^sub>2 es))
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>E A ST. \<not> sub_RI e \<Longrightarrow> length (compT E A ST e) = length (compE\<^sub>2 e) - 1) &&& (\<And>E A ST. \<not> sub_RIs es \<Longrightarrow> length (compTs E A ST es) = length (compEs\<^sub>2 es))
[PROOF STEP]
by(induct e and es rule: compE\<^sub>2.induct compEs\<^sub>2.induct)
  (auto split:bop.splits nat_diff_split simp: compE\<^sub>2_not_Nil')


[STATEMENT]
lemma (in TC1) compT_sizes[simp]:
shows "\<And>E A ST. P,E \<turnstile>\<^sub>1 e :: T \<Longrightarrow> size(compT E A ST e) = size(compE\<^sub>2 e) - 1"
and "\<And>E A ST. P,E \<turnstile>\<^sub>1 es [::] Ts \<Longrightarrow> size(compTs E A ST es) = size(compEs\<^sub>2 es)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>E A ST. P,E \<turnstile>\<^sub>1 e :: T \<Longrightarrow> length (compT E A ST e) = length (compE\<^sub>2 e) - 1) &&& (\<And>E A ST. P,E \<turnstile>\<^sub>1 es [::] Ts \<Longrightarrow> length (compTs E A ST es) = length (compEs\<^sub>2 es))
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>E A ST. P,E \<turnstile>\<^sub>1 e :: T \<Longrightarrow> length (compT E A ST e) = length (compE\<^sub>2 e) - 1) &&& (\<And>E A ST. P,E \<turnstile>\<^sub>1 es [::] Ts \<Longrightarrow> length (compTs E A ST es) = length (compEs\<^sub>2 es))
[PROOF STEP]
using compT_sizes' WT\<^sub>1_nsub_RI WTs\<^sub>1_nsub_RIs
[PROOF STATE]
proof (prove)
using this:
\<not> sub_RI ?e \<Longrightarrow> length (compT ?E ?A ?ST ?e) = length (compE\<^sub>2 ?e) - 1
\<not> sub_RIs ?es \<Longrightarrow> length (compTs ?E ?A ?ST ?es) = length (compEs\<^sub>2 ?es)
?P,?E \<turnstile>\<^sub>1 ?e :: ?T \<Longrightarrow> \<not> sub_RI ?e
?P,?E \<turnstile>\<^sub>1 ?es [::] ?Ts \<Longrightarrow> \<not> sub_RIs ?es

goal (1 subgoal):
 1. (\<And>E A ST. P,E \<turnstile>\<^sub>1 e :: T \<Longrightarrow> length (compT E A ST e) = length (compE\<^sub>2 e) - 1) &&& (\<And>E A ST. P,E \<turnstile>\<^sub>1 es [::] Ts \<Longrightarrow> length (compTs E A ST es) = length (compEs\<^sub>2 es))
[PROOF STEP]
by auto


[STATEMENT]
lemma (in TC1) [simp]: "\<And>ST E. \<lfloor>\<tau>\<rfloor> \<notin> set (compT E None ST e)"
and [simp]: "\<And>ST E. \<lfloor>\<tau>\<rfloor> \<notin> set (compTs E None ST es)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>ST E. \<lfloor>\<tau>\<rfloor> \<notin> set (compT E None ST e)) &&& (\<And>ST E. \<lfloor>\<tau>\<rfloor> \<notin> set (compTs E None ST es))
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>ST E. \<lfloor>\<tau>\<rfloor> \<notin> set (compT E None ST e)) &&& (\<And>ST E. \<lfloor>\<tau>\<rfloor> \<notin> set (compTs E None ST es))
[PROOF STEP]
by(induct e and es rule: compT.induct compTs.induct) (simp_all add:after_def)


[STATEMENT]
lemma (in TC0) pair_eq_ty\<^sub>i'_conv:
  "(\<lfloor>(ST, LT)\<rfloor> = ty\<^sub>i' ST\<^sub>0 E A) =
  (case A of None \<Rightarrow> False | Some A \<Rightarrow> (ST = ST\<^sub>0 \<and> LT = ty\<^sub>l E A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lfloor>(ST, LT)\<rfloor> = ty\<^sub>i' ST\<^sub>0 E A) = (case A of None \<Rightarrow> False | \<lfloor>A\<rfloor> \<Rightarrow> ST = ST\<^sub>0 \<and> LT = ty\<^sub>l E A)
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lfloor>(ST, LT)\<rfloor> = ty\<^sub>i' ST\<^sub>0 E A) = (case A of None \<Rightarrow> False | \<lfloor>A\<rfloor> \<Rightarrow> ST = ST\<^sub>0 \<and> LT = ty\<^sub>l E A)
[PROOF STEP]
by(simp add:ty\<^sub>i'_def)


[STATEMENT]
lemma (in TC0) pair_conv_ty\<^sub>i':
  "\<lfloor>(ST, ty\<^sub>l E A)\<rfloor> = ty\<^sub>i' ST E \<lfloor>A\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>(ST, ty\<^sub>l E A)\<rfloor> = ty\<^sub>i' ST E \<lfloor>A\<rfloor>
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>(ST, ty\<^sub>l E A)\<rfloor> = ty\<^sub>i' ST E \<lfloor>A\<rfloor>
[PROOF STEP]
by(simp add:ty\<^sub>i'_def)