[STATEMENT]
lemma ccomp_correct:
 "ccomp c \<Turnstile> cfs\<box> \<Longrightarrow> cpred c (cfs ! 0) (cfs ! (length cfs - 1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ccomp c \<Turnstile> cfs\<box> \<Longrightarrow> cpred c (cfs ! 0) (cfs ! (length cfs - 1))
[PROOF STEP]
proof (induction c arbitrary: cfs, simp_all add: Let_def, frule_tac [4] bcomp_ccomp,
 frule_tac [3] ccomp_ccomp, auto)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>x1 x2 cfs. acomp x2 @ [STORE x1] \<Turnstile> cfs\<box> \<Longrightarrow> cpred (x1 ::= x2) (cfs ! 0) (cfs ! (length cfs - Suc 0))
 2. \<And>c1 c2 cfs a b k t aa. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); ccomp c1 @ ccomp c2 \<Turnstile> cfs\<box>; cfs ! 0 = (0, a, b); k < length cfs; cfs ! k = (size (ccomp c1) + size (ccomp c2), aa, b); (c1, a) \<Rightarrow> t; (c2, t) \<Rightarrow> aa\<rbrakk> \<Longrightarrow> cpred (c1;; c2) (0, a, b) (cfs ! (length cfs - Suc 0))
 3. \<And>x1 c1 c2 cfs a b. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); bcomp (x1, False, size (ccomp c1) + 1) @ ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>; cfs ! 0 = (0, a, b); \<not> bval x1 a\<rbrakk> \<Longrightarrow> cpred (IF x1 THEN c1 ELSE c2) (0, a, b) (cfs ! (length cfs - Suc 0))
 4. \<And>x1 c1 c2 cfs a b k aa. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); bcomp (x1, False, size (ccomp c1) + 1) @ ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>; cfs ! 0 = (0, a, b); bval x1 a; k < length cfs; cfs ! k = (size (bcomp (x1, False, size (ccomp c1) + 1)) + size (ccomp c1), aa, b); (c1, a) \<Rightarrow> aa\<rbrakk> \<Longrightarrow> cpred (IF x1 THEN c1 ELSE c2) (0, a, b) (cfs ! (length cfs - Suc 0))
 5. \<And>c1 c2 cfs. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); JMPND (size (ccomp c1) + 1) # ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>\<rbrakk> \<Longrightarrow> cpred (c1 OR c2) (cfs ! 0) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
fix a x cfs
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>x1 x2 cfs. acomp x2 @ [STORE x1] \<Turnstile> cfs\<box> \<Longrightarrow> cpred (x1 ::= x2) (cfs ! 0) (cfs ! (length cfs - Suc 0))
 2. \<And>c1 c2 cfs a b k t aa. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); ccomp c1 @ ccomp c2 \<Turnstile> cfs\<box>; cfs ! 0 = (0, a, b); k < length cfs; cfs ! k = (size (ccomp c1) + size (ccomp c2), aa, b); (c1, a) \<Rightarrow> t; (c2, t) \<Rightarrow> aa\<rbrakk> \<Longrightarrow> cpred (c1;; c2) (0, a, b) (cfs ! (length cfs - Suc 0))
 3. \<And>x1 c1 c2 cfs a b. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); bcomp (x1, False, size (ccomp c1) + 1) @ ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>; cfs ! 0 = (0, a, b); \<not> bval x1 a\<rbrakk> \<Longrightarrow> cpred (IF x1 THEN c1 ELSE c2) (0, a, b) (cfs ! (length cfs - Suc 0))
 4. \<And>x1 c1 c2 cfs a b k aa. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); bcomp (x1, False, size (ccomp c1) + 1) @ ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>; cfs ! 0 = (0, a, b); bval x1 a; k < length cfs; cfs ! k = (size (bcomp (x1, False, size (ccomp c1) + 1)) + size (ccomp c1), aa, b); (c1, a) \<Rightarrow> aa\<rbrakk> \<Longrightarrow> cpred (IF x1 THEN c1 ELSE c2) (0, a, b) (cfs ! (length cfs - Suc 0))
 5. \<And>c1 c2 cfs. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); JMPND (size (ccomp c1) + 1) # ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>\<rbrakk> \<Longrightarrow> cpred (c1 OR c2) (cfs ! 0) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
assume A: "acomp a @ [STORE x] \<Turnstile> cfs\<box>"
[PROOF STATE]
proof (state)
this:
acomp a @ [STORE x] \<Turnstile> cfs\<box>

goal (5 subgoals):
 1. \<And>x1 x2 cfs. acomp x2 @ [STORE x1] \<Turnstile> cfs\<box> \<Longrightarrow> cpred (x1 ::= x2) (cfs ! 0) (cfs ! (length cfs - Suc 0))
 2. \<And>c1 c2 cfs a b k t aa. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); ccomp c1 @ ccomp c2 \<Turnstile> cfs\<box>; cfs ! 0 = (0, a, b); k < length cfs; cfs ! k = (size (ccomp c1) + size (ccomp c2), aa, b); (c1, a) \<Rightarrow> t; (c2, t) \<Rightarrow> aa\<rbrakk> \<Longrightarrow> cpred (c1;; c2) (0, a, b) (cfs ! (length cfs - Suc 0))
 3. \<And>x1 c1 c2 cfs a b. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); bcomp (x1, False, size (ccomp c1) + 1) @ ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>; cfs ! 0 = (0, a, b); \<not> bval x1 a\<rbrakk> \<Longrightarrow> cpred (IF x1 THEN c1 ELSE c2) (0, a, b) (cfs ! (length cfs - Suc 0))
 4. \<And>x1 c1 c2 cfs a b k aa. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); bcomp (x1, False, size (ccomp c1) + 1) @ ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>; cfs ! 0 = (0, a, b); bval x1 a; k < length cfs; cfs ! k = (size (bcomp (x1, False, size (ccomp c1) + 1)) + size (ccomp c1), aa, b); (c1, a) \<Rightarrow> aa\<rbrakk> \<Longrightarrow> cpred (IF x1 THEN c1 ELSE c2) (0, a, b) (cfs ! (length cfs - Suc 0))
 5. \<And>c1 c2 cfs. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); JMPND (size (ccomp c1) + 1) # ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>\<rbrakk> \<Longrightarrow> cpred (c1 OR c2) (cfs ! 0) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
hence "\<exists>k < length cfs. apred a (off [] (cfs ! 0)) (off [] (cfs ! k))"
[PROOF STATE]
proof (prove)
using this:
acomp a @ [STORE x] \<Turnstile> cfs\<box>

goal (1 subgoal):
 1. \<exists>k<length cfs. apred a (off [] (cfs ! 0)) (off [] (cfs ! k))
[PROOF STEP]
by (rule_tac execl_all_sub, auto simp: execl_all_def)
[PROOF STATE]
proof (state)
this:
\<exists>k<length cfs. apred a (off [] (cfs ! 0)) (off [] (cfs ! k))

goal (5 subgoals):
 1. \<And>x1 x2 cfs. acomp x2 @ [STORE x1] \<Turnstile> cfs\<box> \<Longrightarrow> cpred (x1 ::= x2) (cfs ! 0) (cfs ! (length cfs - Suc 0))
 2. \<And>c1 c2 cfs a b k t aa. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); ccomp c1 @ ccomp c2 \<Turnstile> cfs\<box>; cfs ! 0 = (0, a, b); k < length cfs; cfs ! k = (size (ccomp c1) + size (ccomp c2), aa, b); (c1, a) \<Rightarrow> t; (c2, t) \<Rightarrow> aa\<rbrakk> \<Longrightarrow> cpred (c1;; c2) (0, a, b) (cfs ! (length cfs - Suc 0))
 3. \<And>x1 c1 c2 cfs a b. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); bcomp (x1, False, size (ccomp c1) + 1) @ ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>; cfs ! 0 = (0, a, b); \<not> bval x1 a\<rbrakk> \<Longrightarrow> cpred (IF x1 THEN c1 ELSE c2) (0, a, b) (cfs ! (length cfs - Suc 0))
 4. \<And>x1 c1 c2 cfs a b k aa. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); bcomp (x1, False, size (ccomp c1) + 1) @ ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>; cfs ! 0 = (0, a, b); bval x1 a; k < length cfs; cfs ! k = (size (bcomp (x1, False, size (ccomp c1) + 1)) + size (ccomp c1), aa, b); (c1, a) \<Rightarrow> aa\<rbrakk> \<Longrightarrow> cpred (IF x1 THEN c1 ELSE c2) (0, a, b) (cfs ! (length cfs - Suc 0))
 5. \<And>c1 c2 cfs. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); JMPND (size (ccomp c1) + 1) # ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>\<rbrakk> \<Longrightarrow> cpred (c1 OR c2) (cfs ! 0) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<exists>k<length cfs. apred a (off [] (cfs ! 0)) (off [] (cfs ! k))

goal (5 subgoals):
 1. \<And>x1 x2 cfs. acomp x2 @ [STORE x1] \<Turnstile> cfs\<box> \<Longrightarrow> cpred (x1 ::= x2) (cfs ! 0) (cfs ! (length cfs - Suc 0))
 2. \<And>c1 c2 cfs a b k t aa. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); ccomp c1 @ ccomp c2 \<Turnstile> cfs\<box>; cfs ! 0 = (0, a, b); k < length cfs; cfs ! k = (size (ccomp c1) + size (ccomp c2), aa, b); (c1, a) \<Rightarrow> t; (c2, t) \<Rightarrow> aa\<rbrakk> \<Longrightarrow> cpred (c1;; c2) (0, a, b) (cfs ! (length cfs - Suc 0))
 3. \<And>x1 c1 c2 cfs a b. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); bcomp (x1, False, size (ccomp c1) + 1) @ ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>; cfs ! 0 = (0, a, b); \<not> bval x1 a\<rbrakk> \<Longrightarrow> cpred (IF x1 THEN c1 ELSE c2) (0, a, b) (cfs ! (length cfs - Suc 0))
 4. \<And>x1 c1 c2 cfs a b k aa. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); bcomp (x1, False, size (ccomp c1) + 1) @ ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>; cfs ! 0 = (0, a, b); bval x1 a; k < length cfs; cfs ! k = (size (bcomp (x1, False, size (ccomp c1) + 1)) + size (ccomp c1), aa, b); (c1, a) \<Rightarrow> aa\<rbrakk> \<Longrightarrow> cpred (IF x1 THEN c1 ELSE c2) (0, a, b) (cfs ! (length cfs - Suc 0))
 5. \<And>c1 c2 cfs. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); JMPND (size (ccomp c1) + 1) # ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>\<rbrakk> \<Longrightarrow> cpred (c1 OR c2) (cfs ! 0) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
obtain s stk where B: "cfs ! 0 = (0, s, stk)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s stk. cfs ! 0 = (0, s, stk) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
acomp a @ [STORE x] \<Turnstile> cfs\<box>

goal (1 subgoal):
 1. (\<And>s stk. cfs ! 0 = (0, s, stk) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases "cfs ! 0", simp add: execl_all_def)
[PROOF STATE]
proof (state)
this:
cfs ! 0 = (0, s, stk)

goal (5 subgoals):
 1. \<And>x1 x2 cfs. acomp x2 @ [STORE x1] \<Turnstile> cfs\<box> \<Longrightarrow> cpred (x1 ::= x2) (cfs ! 0) (cfs ! (length cfs - Suc 0))
 2. \<And>c1 c2 cfs a b k t aa. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); ccomp c1 @ ccomp c2 \<Turnstile> cfs\<box>; cfs ! 0 = (0, a, b); k < length cfs; cfs ! k = (size (ccomp c1) + size (ccomp c2), aa, b); (c1, a) \<Rightarrow> t; (c2, t) \<Rightarrow> aa\<rbrakk> \<Longrightarrow> cpred (c1;; c2) (0, a, b) (cfs ! (length cfs - Suc 0))
 3. \<And>x1 c1 c2 cfs a b. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); bcomp (x1, False, size (ccomp c1) + 1) @ ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>; cfs ! 0 = (0, a, b); \<not> bval x1 a\<rbrakk> \<Longrightarrow> cpred (IF x1 THEN c1 ELSE c2) (0, a, b) (cfs ! (length cfs - Suc 0))
 4. \<And>x1 c1 c2 cfs a b k aa. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); bcomp (x1, False, size (ccomp c1) + 1) @ ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>; cfs ! 0 = (0, a, b); bval x1 a; k < length cfs; cfs ! k = (size (bcomp (x1, False, size (ccomp c1) + 1)) + size (ccomp c1), aa, b); (c1, a) \<Rightarrow> aa\<rbrakk> \<Longrightarrow> cpred (IF x1 THEN c1 ELSE c2) (0, a, b) (cfs ! (length cfs - Suc 0))
 5. \<And>c1 c2 cfs. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); JMPND (size (ccomp c1) + 1) # ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>\<rbrakk> \<Longrightarrow> cpred (c1 OR c2) (cfs ! 0) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<exists>k<length cfs. apred a (off [] (cfs ! 0)) (off [] (cfs ! k))
cfs ! 0 = (0, s, stk)
[PROOF STEP]
obtain k where C: "k < length cfs" and
    D: "cfs ! k = (size (acomp a), s, aval a s # stk)"
[PROOF STATE]
proof (prove)
using this:
\<exists>k<length cfs. apred a (off [] (cfs ! 0)) (off [] (cfs ! k))
cfs ! 0 = (0, s, stk)

goal (1 subgoal):
 1. (\<And>k. \<lbrakk>k < length cfs; cfs ! k = (size (acomp a), s, aval a s # stk)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: apred_def)
[PROOF STATE]
proof (state)
this:
k < length cfs
cfs ! k = (size (acomp a), s, aval a s # stk)

goal (5 subgoals):
 1. \<And>x1 x2 cfs. acomp x2 @ [STORE x1] \<Turnstile> cfs\<box> \<Longrightarrow> cpred (x1 ::= x2) (cfs ! 0) (cfs ! (length cfs - Suc 0))
 2. \<And>c1 c2 cfs a b k t aa. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); ccomp c1 @ ccomp c2 \<Turnstile> cfs\<box>; cfs ! 0 = (0, a, b); k < length cfs; cfs ! k = (size (ccomp c1) + size (ccomp c2), aa, b); (c1, a) \<Rightarrow> t; (c2, t) \<Rightarrow> aa\<rbrakk> \<Longrightarrow> cpred (c1;; c2) (0, a, b) (cfs ! (length cfs - Suc 0))
 3. \<And>x1 c1 c2 cfs a b. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); bcomp (x1, False, size (ccomp c1) + 1) @ ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>; cfs ! 0 = (0, a, b); \<not> bval x1 a\<rbrakk> \<Longrightarrow> cpred (IF x1 THEN c1 ELSE c2) (0, a, b) (cfs ! (length cfs - Suc 0))
 4. \<And>x1 c1 c2 cfs a b k aa. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); bcomp (x1, False, size (ccomp c1) + 1) @ ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>; cfs ! 0 = (0, a, b); bval x1 a; k < length cfs; cfs ! k = (size (bcomp (x1, False, size (ccomp c1) + 1)) + size (ccomp c1), aa, b); (c1, a) \<Rightarrow> aa\<rbrakk> \<Longrightarrow> cpred (IF x1 THEN c1 ELSE c2) (0, a, b) (cfs ! (length cfs - Suc 0))
 5. \<And>c1 c2 cfs. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); JMPND (size (ccomp c1) + 1) # ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>\<rbrakk> \<Longrightarrow> cpred (c1 OR c2) (cfs ! 0) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
hence "cfs ! Suc k = (size (acomp a) + 1, s(x := aval a s), stk)"
[PROOF STATE]
proof (prove)
using this:
k < length cfs
cfs ! k = (size (acomp a), s, aval a s # stk)

goal (1 subgoal):
 1. cfs ! Suc k = (size (acomp a) + 1, s(x := aval a s), stk)
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
k < length cfs
cfs ! k = (size (acomp a), s, aval a s # stk)
acomp a @ [STORE x] \<Turnstile> cfs\<box>

goal (1 subgoal):
 1. cfs ! Suc k = (size (acomp a) + 1, s(x := aval a s), stk)
[PROOF STEP]
by (insert execl_next [of "acomp a @ [STORE x]" cfs k],
     simp add: execl_all_def, drule_tac impI, auto)
[PROOF STATE]
proof (state)
this:
cfs ! Suc k = (size (acomp a) + 1, s(x := aval a s), stk)

goal (5 subgoals):
 1. \<And>x1 x2 cfs. acomp x2 @ [STORE x1] \<Turnstile> cfs\<box> \<Longrightarrow> cpred (x1 ::= x2) (cfs ! 0) (cfs ! (length cfs - Suc 0))
 2. \<And>c1 c2 cfs a b k t aa. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); ccomp c1 @ ccomp c2 \<Turnstile> cfs\<box>; cfs ! 0 = (0, a, b); k < length cfs; cfs ! k = (size (ccomp c1) + size (ccomp c2), aa, b); (c1, a) \<Rightarrow> t; (c2, t) \<Rightarrow> aa\<rbrakk> \<Longrightarrow> cpred (c1;; c2) (0, a, b) (cfs ! (length cfs - Suc 0))
 3. \<And>x1 c1 c2 cfs a b. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); bcomp (x1, False, size (ccomp c1) + 1) @ ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>; cfs ! 0 = (0, a, b); \<not> bval x1 a\<rbrakk> \<Longrightarrow> cpred (IF x1 THEN c1 ELSE c2) (0, a, b) (cfs ! (length cfs - Suc 0))
 4. \<And>x1 c1 c2 cfs a b k aa. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); bcomp (x1, False, size (ccomp c1) + 1) @ ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>; cfs ! 0 = (0, a, b); bval x1 a; k < length cfs; cfs ! k = (size (bcomp (x1, False, size (ccomp c1) + 1)) + size (ccomp c1), aa, b); (c1, a) \<Rightarrow> aa\<rbrakk> \<Longrightarrow> cpred (IF x1 THEN c1 ELSE c2) (0, a, b) (cfs ! (length cfs - Suc 0))
 5. \<And>c1 c2 cfs. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); JMPND (size (ccomp c1) + 1) # ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>\<rbrakk> \<Longrightarrow> cpred (c1 OR c2) (cfs ! 0) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
thus "cpred (x ::= a) (cfs ! 0) (cfs ! (length cfs - Suc 0))"
[PROOF STATE]
proof (prove)
using this:
cfs ! Suc k = (size (acomp a) + 1, s(x := aval a s), stk)

goal (1 subgoal):
 1. cpred (x ::= a) (cfs ! 0) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
using A and B and C and D
[PROOF STATE]
proof (prove)
using this:
cfs ! Suc k = (size (acomp a) + 1, s(x := aval a s), stk)
acomp a @ [STORE x] \<Turnstile> cfs\<box>
cfs ! 0 = (0, s, stk)
k < length cfs
cfs ! k = (size (acomp a), s, aval a s # stk)

goal (1 subgoal):
 1. cpred (x ::= a) (cfs ! 0) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
by (insert execl_last [of "acomp a @ [STORE x]"
     cfs "Suc k"], simp add: execl_all_def cpred_def, drule_tac impI, auto)
[PROOF STATE]
proof (state)
this:
cpred (x ::= a) (cfs ! 0) (cfs ! (length cfs - Suc 0))

goal (4 subgoals):
 1. \<And>c1 c2 cfs a b k t aa. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); ccomp c1 @ ccomp c2 \<Turnstile> cfs\<box>; cfs ! 0 = (0, a, b); k < length cfs; cfs ! k = (size (ccomp c1) + size (ccomp c2), aa, b); (c1, a) \<Rightarrow> t; (c2, t) \<Rightarrow> aa\<rbrakk> \<Longrightarrow> cpred (c1;; c2) (0, a, b) (cfs ! (length cfs - Suc 0))
 2. \<And>x1 c1 c2 cfs a b. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); bcomp (x1, False, size (ccomp c1) + 1) @ ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>; cfs ! 0 = (0, a, b); \<not> bval x1 a\<rbrakk> \<Longrightarrow> cpred (IF x1 THEN c1 ELSE c2) (0, a, b) (cfs ! (length cfs - Suc 0))
 3. \<And>x1 c1 c2 cfs a b k aa. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); bcomp (x1, False, size (ccomp c1) + 1) @ ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>; cfs ! 0 = (0, a, b); bval x1 a; k < length cfs; cfs ! k = (size (bcomp (x1, False, size (ccomp c1) + 1)) + size (ccomp c1), aa, b); (c1, a) \<Rightarrow> aa\<rbrakk> \<Longrightarrow> cpred (IF x1 THEN c1 ELSE c2) (0, a, b) (cfs ! (length cfs - Suc 0))
 4. \<And>c1 c2 cfs. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); JMPND (size (ccomp c1) + 1) # ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>\<rbrakk> \<Longrightarrow> cpred (c1 OR c2) (cfs ! 0) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>c1 c2 cfs a b k t aa. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); ccomp c1 @ ccomp c2 \<Turnstile> cfs\<box>; cfs ! 0 = (0, a, b); k < length cfs; cfs ! k = (size (ccomp c1) + size (ccomp c2), aa, b); (c1, a) \<Rightarrow> t; (c2, t) \<Rightarrow> aa\<rbrakk> \<Longrightarrow> cpred (c1;; c2) (0, a, b) (cfs ! (length cfs - Suc 0))
 2. \<And>x1 c1 c2 cfs a b. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); bcomp (x1, False, size (ccomp c1) + 1) @ ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>; cfs ! 0 = (0, a, b); \<not> bval x1 a\<rbrakk> \<Longrightarrow> cpred (IF x1 THEN c1 ELSE c2) (0, a, b) (cfs ! (length cfs - Suc 0))
 3. \<And>x1 c1 c2 cfs a b k aa. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); bcomp (x1, False, size (ccomp c1) + 1) @ ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>; cfs ! 0 = (0, a, b); bval x1 a; k < length cfs; cfs ! k = (size (bcomp (x1, False, size (ccomp c1) + 1)) + size (ccomp c1), aa, b); (c1, a) \<Rightarrow> aa\<rbrakk> \<Longrightarrow> cpred (IF x1 THEN c1 ELSE c2) (0, a, b) (cfs ! (length cfs - Suc 0))
 4. \<And>c1 c2 cfs. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); JMPND (size (ccomp c1) + 1) # ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>\<rbrakk> \<Longrightarrow> cpred (c1 OR c2) (cfs ! 0) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
fix c\<^sub>1 c\<^sub>2 cfs s s' t stk k
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>c1 c2 cfs a b k t aa. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); ccomp c1 @ ccomp c2 \<Turnstile> cfs\<box>; cfs ! 0 = (0, a, b); k < length cfs; cfs ! k = (size (ccomp c1) + size (ccomp c2), aa, b); (c1, a) \<Rightarrow> t; (c2, t) \<Rightarrow> aa\<rbrakk> \<Longrightarrow> cpred (c1;; c2) (0, a, b) (cfs ! (length cfs - Suc 0))
 2. \<And>x1 c1 c2 cfs a b. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); bcomp (x1, False, size (ccomp c1) + 1) @ ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>; cfs ! 0 = (0, a, b); \<not> bval x1 a\<rbrakk> \<Longrightarrow> cpred (IF x1 THEN c1 ELSE c2) (0, a, b) (cfs ! (length cfs - Suc 0))
 3. \<And>x1 c1 c2 cfs a b k aa. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); bcomp (x1, False, size (ccomp c1) + 1) @ ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>; cfs ! 0 = (0, a, b); bval x1 a; k < length cfs; cfs ! k = (size (bcomp (x1, False, size (ccomp c1) + 1)) + size (ccomp c1), aa, b); (c1, a) \<Rightarrow> aa\<rbrakk> \<Longrightarrow> cpred (IF x1 THEN c1 ELSE c2) (0, a, b) (cfs ! (length cfs - Suc 0))
 4. \<And>c1 c2 cfs. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); JMPND (size (ccomp c1) + 1) # ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>\<rbrakk> \<Longrightarrow> cpred (c1 OR c2) (cfs ! 0) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
assume "ccomp c\<^sub>1 @ ccomp c\<^sub>2 \<Turnstile> cfs\<box>" and "k < length cfs" and
   "cfs ! k = (size (ccomp c\<^sub>1) + size (ccomp c\<^sub>2), s', stk)"
[PROOF STATE]
proof (state)
this:
ccomp c\<^sub>1 @ ccomp c\<^sub>2 \<Turnstile> cfs\<box>
k < length cfs
cfs ! k = (size (ccomp c\<^sub>1) + size (ccomp c\<^sub>2), s', stk)

goal (4 subgoals):
 1. \<And>c1 c2 cfs a b k t aa. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); ccomp c1 @ ccomp c2 \<Turnstile> cfs\<box>; cfs ! 0 = (0, a, b); k < length cfs; cfs ! k = (size (ccomp c1) + size (ccomp c2), aa, b); (c1, a) \<Rightarrow> t; (c2, t) \<Rightarrow> aa\<rbrakk> \<Longrightarrow> cpred (c1;; c2) (0, a, b) (cfs ! (length cfs - Suc 0))
 2. \<And>x1 c1 c2 cfs a b. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); bcomp (x1, False, size (ccomp c1) + 1) @ ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>; cfs ! 0 = (0, a, b); \<not> bval x1 a\<rbrakk> \<Longrightarrow> cpred (IF x1 THEN c1 ELSE c2) (0, a, b) (cfs ! (length cfs - Suc 0))
 3. \<And>x1 c1 c2 cfs a b k aa. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); bcomp (x1, False, size (ccomp c1) + 1) @ ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>; cfs ! 0 = (0, a, b); bval x1 a; k < length cfs; cfs ! k = (size (bcomp (x1, False, size (ccomp c1) + 1)) + size (ccomp c1), aa, b); (c1, a) \<Rightarrow> aa\<rbrakk> \<Longrightarrow> cpred (IF x1 THEN c1 ELSE c2) (0, a, b) (cfs ! (length cfs - Suc 0))
 4. \<And>c1 c2 cfs. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); JMPND (size (ccomp c1) + 1) # ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>\<rbrakk> \<Longrightarrow> cpred (c1 OR c2) (cfs ! 0) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ccomp c\<^sub>1 @ ccomp c\<^sub>2 \<Turnstile> cfs\<box>
k < length cfs
cfs ! k = (size (ccomp c\<^sub>1) + size (ccomp c\<^sub>2), s', stk)

goal (4 subgoals):
 1. \<And>c1 c2 cfs a b k t aa. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); ccomp c1 @ ccomp c2 \<Turnstile> cfs\<box>; cfs ! 0 = (0, a, b); k < length cfs; cfs ! k = (size (ccomp c1) + size (ccomp c2), aa, b); (c1, a) \<Rightarrow> t; (c2, t) \<Rightarrow> aa\<rbrakk> \<Longrightarrow> cpred (c1;; c2) (0, a, b) (cfs ! (length cfs - Suc 0))
 2. \<And>x1 c1 c2 cfs a b. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); bcomp (x1, False, size (ccomp c1) + 1) @ ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>; cfs ! 0 = (0, a, b); \<not> bval x1 a\<rbrakk> \<Longrightarrow> cpred (IF x1 THEN c1 ELSE c2) (0, a, b) (cfs ! (length cfs - Suc 0))
 3. \<And>x1 c1 c2 cfs a b k aa. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); bcomp (x1, False, size (ccomp c1) + 1) @ ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>; cfs ! 0 = (0, a, b); bval x1 a; k < length cfs; cfs ! k = (size (bcomp (x1, False, size (ccomp c1) + 1)) + size (ccomp c1), aa, b); (c1, a) \<Rightarrow> aa\<rbrakk> \<Longrightarrow> cpred (IF x1 THEN c1 ELSE c2) (0, a, b) (cfs ! (length cfs - Suc 0))
 4. \<And>c1 c2 cfs. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); JMPND (size (ccomp c1) + 1) # ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>\<rbrakk> \<Longrightarrow> cpred (c1 OR c2) (cfs ! 0) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
assume "(c\<^sub>1, s) \<Rightarrow> t" and "(c\<^sub>2, t) \<Rightarrow> s'"
[PROOF STATE]
proof (state)
this:
(c\<^sub>1, s) \<Rightarrow> t
(c\<^sub>2, t) \<Rightarrow> s'

goal (4 subgoals):
 1. \<And>c1 c2 cfs a b k t aa. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); ccomp c1 @ ccomp c2 \<Turnstile> cfs\<box>; cfs ! 0 = (0, a, b); k < length cfs; cfs ! k = (size (ccomp c1) + size (ccomp c2), aa, b); (c1, a) \<Rightarrow> t; (c2, t) \<Rightarrow> aa\<rbrakk> \<Longrightarrow> cpred (c1;; c2) (0, a, b) (cfs ! (length cfs - Suc 0))
 2. \<And>x1 c1 c2 cfs a b. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); bcomp (x1, False, size (ccomp c1) + 1) @ ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>; cfs ! 0 = (0, a, b); \<not> bval x1 a\<rbrakk> \<Longrightarrow> cpred (IF x1 THEN c1 ELSE c2) (0, a, b) (cfs ! (length cfs - Suc 0))
 3. \<And>x1 c1 c2 cfs a b k aa. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); bcomp (x1, False, size (ccomp c1) + 1) @ ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>; cfs ! 0 = (0, a, b); bval x1 a; k < length cfs; cfs ! k = (size (bcomp (x1, False, size (ccomp c1) + 1)) + size (ccomp c1), aa, b); (c1, a) \<Rightarrow> aa\<rbrakk> \<Longrightarrow> cpred (IF x1 THEN c1 ELSE c2) (0, a, b) (cfs ! (length cfs - Suc 0))
 4. \<And>c1 c2 cfs. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); JMPND (size (ccomp c1) + 1) # ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>\<rbrakk> \<Longrightarrow> cpred (c1 OR c2) (cfs ! 0) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
ccomp c\<^sub>1 @ ccomp c\<^sub>2 \<Turnstile> cfs\<box>
k < length cfs
cfs ! k = (size (ccomp c\<^sub>1) + size (ccomp c\<^sub>2), s', stk)
(c\<^sub>1, s) \<Rightarrow> t
(c\<^sub>2, t) \<Rightarrow> s'
[PROOF STEP]
show "cpred (c\<^sub>1;; c\<^sub>2) (0, s, stk) (cfs ! (length cfs - Suc 0))"
[PROOF STATE]
proof (prove)
using this:
ccomp c\<^sub>1 @ ccomp c\<^sub>2 \<Turnstile> cfs\<box>
k < length cfs
cfs ! k = (size (ccomp c\<^sub>1) + size (ccomp c\<^sub>2), s', stk)
(c\<^sub>1, s) \<Rightarrow> t
(c\<^sub>2, t) \<Rightarrow> s'

goal (1 subgoal):
 1. cpred (c\<^sub>1;; c\<^sub>2) (0, s, stk) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
by (insert execl_last, auto simp: execl_all_def cpred_def)
[PROOF STATE]
proof (state)
this:
cpred (c\<^sub>1;; c\<^sub>2) (0, s, stk) (cfs ! (length cfs - Suc 0))

goal (3 subgoals):
 1. \<And>x1 c1 c2 cfs a b. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); bcomp (x1, False, size (ccomp c1) + 1) @ ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>; cfs ! 0 = (0, a, b); \<not> bval x1 a\<rbrakk> \<Longrightarrow> cpred (IF x1 THEN c1 ELSE c2) (0, a, b) (cfs ! (length cfs - Suc 0))
 2. \<And>x1 c1 c2 cfs a b k aa. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); bcomp (x1, False, size (ccomp c1) + 1) @ ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>; cfs ! 0 = (0, a, b); bval x1 a; k < length cfs; cfs ! k = (size (bcomp (x1, False, size (ccomp c1) + 1)) + size (ccomp c1), aa, b); (c1, a) \<Rightarrow> aa\<rbrakk> \<Longrightarrow> cpred (IF x1 THEN c1 ELSE c2) (0, a, b) (cfs ! (length cfs - Suc 0))
 3. \<And>c1 c2 cfs. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); JMPND (size (ccomp c1) + 1) # ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>\<rbrakk> \<Longrightarrow> cpred (c1 OR c2) (cfs ! 0) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x1 c1 c2 cfs a b. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); bcomp (x1, False, size (ccomp c1) + 1) @ ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>; cfs ! 0 = (0, a, b); \<not> bval x1 a\<rbrakk> \<Longrightarrow> cpred (IF x1 THEN c1 ELSE c2) (0, a, b) (cfs ! (length cfs - Suc 0))
 2. \<And>x1 c1 c2 cfs a b k aa. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); bcomp (x1, False, size (ccomp c1) + 1) @ ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>; cfs ! 0 = (0, a, b); bval x1 a; k < length cfs; cfs ! k = (size (bcomp (x1, False, size (ccomp c1) + 1)) + size (ccomp c1), aa, b); (c1, a) \<Rightarrow> aa\<rbrakk> \<Longrightarrow> cpred (IF x1 THEN c1 ELSE c2) (0, a, b) (cfs ! (length cfs - Suc 0))
 3. \<And>c1 c2 cfs. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); JMPND (size (ccomp c1) + 1) # ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>\<rbrakk> \<Longrightarrow> cpred (c1 OR c2) (cfs ! 0) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
fix b c\<^sub>1 c\<^sub>2 cfs s stk
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x1 c1 c2 cfs a b. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); bcomp (x1, False, size (ccomp c1) + 1) @ ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>; cfs ! 0 = (0, a, b); \<not> bval x1 a\<rbrakk> \<Longrightarrow> cpred (IF x1 THEN c1 ELSE c2) (0, a, b) (cfs ! (length cfs - Suc 0))
 2. \<And>x1 c1 c2 cfs a b k aa. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); bcomp (x1, False, size (ccomp c1) + 1) @ ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>; cfs ! 0 = (0, a, b); bval x1 a; k < length cfs; cfs ! k = (size (bcomp (x1, False, size (ccomp c1) + 1)) + size (ccomp c1), aa, b); (c1, a) \<Rightarrow> aa\<rbrakk> \<Longrightarrow> cpred (IF x1 THEN c1 ELSE c2) (0, a, b) (cfs ! (length cfs - Suc 0))
 3. \<And>c1 c2 cfs. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); JMPND (size (ccomp c1) + 1) # ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>\<rbrakk> \<Longrightarrow> cpred (c1 OR c2) (cfs ! 0) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
assume A: "bcomp (b, False, size (ccomp c\<^sub>1) + 1) @ ccomp c\<^sub>1 @
    JMP (size (ccomp c\<^sub>2)) # ccomp c\<^sub>2 \<Turnstile> cfs\<box>"
    (is "bcomp ?x @ ?cc\<^sub>1 @ _ # ?cc\<^sub>2 \<Turnstile> _\<box>")
[PROOF STATE]
proof (state)
this:
bcomp (b, False, size (ccomp c\<^sub>1) + 1) @ ccomp c\<^sub>1 @ JMP (size (ccomp c\<^sub>2)) # ccomp c\<^sub>2 \<Turnstile> cfs\<box>

goal (3 subgoals):
 1. \<And>x1 c1 c2 cfs a b. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); bcomp (x1, False, size (ccomp c1) + 1) @ ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>; cfs ! 0 = (0, a, b); \<not> bval x1 a\<rbrakk> \<Longrightarrow> cpred (IF x1 THEN c1 ELSE c2) (0, a, b) (cfs ! (length cfs - Suc 0))
 2. \<And>x1 c1 c2 cfs a b k aa. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); bcomp (x1, False, size (ccomp c1) + 1) @ ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>; cfs ! 0 = (0, a, b); bval x1 a; k < length cfs; cfs ! k = (size (bcomp (x1, False, size (ccomp c1) + 1)) + size (ccomp c1), aa, b); (c1, a) \<Rightarrow> aa\<rbrakk> \<Longrightarrow> cpred (IF x1 THEN c1 ELSE c2) (0, a, b) (cfs ! (length cfs - Suc 0))
 3. \<And>c1 c2 cfs. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); JMPND (size (ccomp c1) + 1) # ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>\<rbrakk> \<Longrightarrow> cpred (c1 OR c2) (cfs ! 0) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
let ?P = "bcomp ?x @ ?cc\<^sub>1 @ [JMP (size ?cc\<^sub>2)]"
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x1 c1 c2 cfs a b. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); bcomp (x1, False, size (ccomp c1) + 1) @ ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>; cfs ! 0 = (0, a, b); \<not> bval x1 a\<rbrakk> \<Longrightarrow> cpred (IF x1 THEN c1 ELSE c2) (0, a, b) (cfs ! (length cfs - Suc 0))
 2. \<And>x1 c1 c2 cfs a b k aa. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); bcomp (x1, False, size (ccomp c1) + 1) @ ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>; cfs ! 0 = (0, a, b); bval x1 a; k < length cfs; cfs ! k = (size (bcomp (x1, False, size (ccomp c1) + 1)) + size (ccomp c1), aa, b); (c1, a) \<Rightarrow> aa\<rbrakk> \<Longrightarrow> cpred (IF x1 THEN c1 ELSE c2) (0, a, b) (cfs ! (length cfs - Suc 0))
 3. \<And>c1 c2 cfs. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); JMPND (size (ccomp c1) + 1) # ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>\<rbrakk> \<Longrightarrow> cpred (c1 OR c2) (cfs ! 0) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
have "\<exists>k < length cfs. bpred ?x (off [] (cfs ! 0)) (off [] (cfs ! k))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>k<length cfs. bpred (b, False, size (ccomp c\<^sub>1) + 1) (off [] (cfs ! 0)) (off [] (cfs ! k))
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
bcomp (b, False, size (ccomp c\<^sub>1) + 1) @ ccomp c\<^sub>1 @ JMP (size (ccomp c\<^sub>2)) # ccomp c\<^sub>2 \<Turnstile> cfs\<box>

goal (1 subgoal):
 1. \<exists>k<length cfs. bpred (b, False, size (ccomp c\<^sub>1) + 1) (off [] (cfs ! 0)) (off [] (cfs ! k))
[PROOF STEP]
by (rule_tac execl_all_sub, auto simp: execl_all_def)
[PROOF STATE]
proof (state)
this:
\<exists>k<length cfs. bpred (b, False, size (ccomp c\<^sub>1) + 1) (off [] (cfs ! 0)) (off [] (cfs ! k))

goal (3 subgoals):
 1. \<And>x1 c1 c2 cfs a b. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); bcomp (x1, False, size (ccomp c1) + 1) @ ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>; cfs ! 0 = (0, a, b); \<not> bval x1 a\<rbrakk> \<Longrightarrow> cpred (IF x1 THEN c1 ELSE c2) (0, a, b) (cfs ! (length cfs - Suc 0))
 2. \<And>x1 c1 c2 cfs a b k aa. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); bcomp (x1, False, size (ccomp c1) + 1) @ ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>; cfs ! 0 = (0, a, b); bval x1 a; k < length cfs; cfs ! k = (size (bcomp (x1, False, size (ccomp c1) + 1)) + size (ccomp c1), aa, b); (c1, a) \<Rightarrow> aa\<rbrakk> \<Longrightarrow> cpred (IF x1 THEN c1 ELSE c2) (0, a, b) (cfs ! (length cfs - Suc 0))
 3. \<And>c1 c2 cfs. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); JMPND (size (ccomp c1) + 1) # ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>\<rbrakk> \<Longrightarrow> cpred (c1 OR c2) (cfs ! 0) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<exists>k<length cfs. bpred (b, False, size (ccomp c\<^sub>1) + 1) (off [] (cfs ! 0)) (off [] (cfs ! k))

goal (3 subgoals):
 1. \<And>x1 c1 c2 cfs a b. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); bcomp (x1, False, size (ccomp c1) + 1) @ ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>; cfs ! 0 = (0, a, b); \<not> bval x1 a\<rbrakk> \<Longrightarrow> cpred (IF x1 THEN c1 ELSE c2) (0, a, b) (cfs ! (length cfs - Suc 0))
 2. \<And>x1 c1 c2 cfs a b k aa. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); bcomp (x1, False, size (ccomp c1) + 1) @ ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>; cfs ! 0 = (0, a, b); bval x1 a; k < length cfs; cfs ! k = (size (bcomp (x1, False, size (ccomp c1) + 1)) + size (ccomp c1), aa, b); (c1, a) \<Rightarrow> aa\<rbrakk> \<Longrightarrow> cpred (IF x1 THEN c1 ELSE c2) (0, a, b) (cfs ! (length cfs - Suc 0))
 3. \<And>c1 c2 cfs. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); JMPND (size (ccomp c1) + 1) # ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>\<rbrakk> \<Longrightarrow> cpred (c1 OR c2) (cfs ! 0) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
assume B: "\<not> bval b s" and "cfs ! 0 = (0, s, stk)"
[PROOF STATE]
proof (state)
this:
\<not> bval b s
cfs ! 0 = (0, s, stk)

goal (3 subgoals):
 1. \<And>x1 c1 c2 cfs a b. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); bcomp (x1, False, size (ccomp c1) + 1) @ ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>; cfs ! 0 = (0, a, b); \<not> bval x1 a\<rbrakk> \<Longrightarrow> cpred (IF x1 THEN c1 ELSE c2) (0, a, b) (cfs ! (length cfs - Suc 0))
 2. \<And>x1 c1 c2 cfs a b k aa. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); bcomp (x1, False, size (ccomp c1) + 1) @ ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>; cfs ! 0 = (0, a, b); bval x1 a; k < length cfs; cfs ! k = (size (bcomp (x1, False, size (ccomp c1) + 1)) + size (ccomp c1), aa, b); (c1, a) \<Rightarrow> aa\<rbrakk> \<Longrightarrow> cpred (IF x1 THEN c1 ELSE c2) (0, a, b) (cfs ! (length cfs - Suc 0))
 3. \<And>c1 c2 cfs. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); JMPND (size (ccomp c1) + 1) # ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>\<rbrakk> \<Longrightarrow> cpred (c1 OR c2) (cfs ! 0) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<exists>k<length cfs. bpred (b, False, size (ccomp c\<^sub>1) + 1) (off [] (cfs ! 0)) (off [] (cfs ! k))
\<not> bval b s
cfs ! 0 = (0, s, stk)
[PROOF STEP]
obtain k where C: "k < length cfs" and D: "cfs ! k = (size ?P, s, stk)"
[PROOF STATE]
proof (prove)
using this:
\<exists>k<length cfs. bpred (b, False, size (ccomp c\<^sub>1) + 1) (off [] (cfs ! 0)) (off [] (cfs ! k))
\<not> bval b s
cfs ! 0 = (0, s, stk)

goal (1 subgoal):
 1. (\<And>k. \<lbrakk>k < length cfs; cfs ! k = (size (bcomp (b, False, size (ccomp c\<^sub>1) + 1) @ ccomp c\<^sub>1 @ [JMP (size (ccomp c\<^sub>2))]), s, stk)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (force simp: bpred_def)
[PROOF STATE]
proof (state)
this:
k < length cfs
cfs ! k = (size (bcomp (b, False, size (ccomp c\<^sub>1) + 1) @ ccomp c\<^sub>1 @ [JMP (size (ccomp c\<^sub>2))]), s, stk)

goal (3 subgoals):
 1. \<And>x1 c1 c2 cfs a b. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); bcomp (x1, False, size (ccomp c1) + 1) @ ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>; cfs ! 0 = (0, a, b); \<not> bval x1 a\<rbrakk> \<Longrightarrow> cpred (IF x1 THEN c1 ELSE c2) (0, a, b) (cfs ! (length cfs - Suc 0))
 2. \<And>x1 c1 c2 cfs a b k aa. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); bcomp (x1, False, size (ccomp c1) + 1) @ ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>; cfs ! 0 = (0, a, b); bval x1 a; k < length cfs; cfs ! k = (size (bcomp (x1, False, size (ccomp c1) + 1)) + size (ccomp c1), aa, b); (c1, a) \<Rightarrow> aa\<rbrakk> \<Longrightarrow> cpred (IF x1 THEN c1 ELSE c2) (0, a, b) (cfs ! (length cfs - Suc 0))
 3. \<And>c1 c2 cfs. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); JMPND (size (ccomp c1) + 1) # ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>\<rbrakk> \<Longrightarrow> cpred (c1 OR c2) (cfs ! 0) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
assume "\<And>cfs. ?cc\<^sub>2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c\<^sub>2 (cfs ! 0) (cfs ! (length cfs - Suc 0))"
[PROOF STATE]
proof (state)
this:
ccomp c\<^sub>2 \<Turnstile> ?cfs\<box> \<Longrightarrow> cpred c\<^sub>2 (?cfs ! 0) (?cfs ! (length ?cfs - Suc 0))

goal (3 subgoals):
 1. \<And>x1 c1 c2 cfs a b. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); bcomp (x1, False, size (ccomp c1) + 1) @ ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>; cfs ! 0 = (0, a, b); \<not> bval x1 a\<rbrakk> \<Longrightarrow> cpred (IF x1 THEN c1 ELSE c2) (0, a, b) (cfs ! (length cfs - Suc 0))
 2. \<And>x1 c1 c2 cfs a b k aa. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); bcomp (x1, False, size (ccomp c1) + 1) @ ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>; cfs ! 0 = (0, a, b); bval x1 a; k < length cfs; cfs ! k = (size (bcomp (x1, False, size (ccomp c1) + 1)) + size (ccomp c1), aa, b); (c1, a) \<Rightarrow> aa\<rbrakk> \<Longrightarrow> cpred (IF x1 THEN c1 ELSE c2) (0, a, b) (cfs ! (length cfs - Suc 0))
 3. \<And>c1 c2 cfs. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); JMPND (size (ccomp c1) + 1) # ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>\<rbrakk> \<Longrightarrow> cpred (c1 OR c2) (cfs ! 0) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
hence "\<exists>k' < length cfs. cpred c\<^sub>2 (off ?P (cfs ! k)) (off ?P (cfs ! k'))"
[PROOF STATE]
proof (prove)
using this:
ccomp c\<^sub>2 \<Turnstile> ?cfs\<box> \<Longrightarrow> cpred c\<^sub>2 (?cfs ! 0) (?cfs ! (length ?cfs - Suc 0))

goal (1 subgoal):
 1. \<exists>k'<length cfs. cpred c\<^sub>2 (off (bcomp (b, False, size (ccomp c\<^sub>1) + 1) @ ccomp c\<^sub>1 @ [JMP (size (ccomp c\<^sub>2))]) (cfs ! k)) (off (bcomp (b, False, size (ccomp c\<^sub>1) + 1) @ ccomp c\<^sub>1 @ [JMP (size (ccomp c\<^sub>2))]) (cfs ! k'))
[PROOF STEP]
using A and C and D
[PROOF STATE]
proof (prove)
using this:
ccomp c\<^sub>2 \<Turnstile> ?cfs\<box> \<Longrightarrow> cpred c\<^sub>2 (?cfs ! 0) (?cfs ! (length ?cfs - Suc 0))
bcomp (b, False, size (ccomp c\<^sub>1) + 1) @ ccomp c\<^sub>1 @ JMP (size (ccomp c\<^sub>2)) # ccomp c\<^sub>2 \<Turnstile> cfs\<box>
k < length cfs
cfs ! k = (size (bcomp (b, False, size (ccomp c\<^sub>1) + 1) @ ccomp c\<^sub>1 @ [JMP (size (ccomp c\<^sub>2))]), s, stk)

goal (1 subgoal):
 1. \<exists>k'<length cfs. cpred c\<^sub>2 (off (bcomp (b, False, size (ccomp c\<^sub>1) + 1) @ ccomp c\<^sub>1 @ [JMP (size (ccomp c\<^sub>2))]) (cfs ! k)) (off (bcomp (b, False, size (ccomp c\<^sub>1) + 1) @ ccomp c\<^sub>1 @ [JMP (size (ccomp c\<^sub>2))]) (cfs ! k'))
[PROOF STEP]
by (rule_tac execl_all_sub [where P'' = "[]"], auto)
[PROOF STATE]
proof (state)
this:
\<exists>k'<length cfs. cpred c\<^sub>2 (off (bcomp (b, False, size (ccomp c\<^sub>1) + 1) @ ccomp c\<^sub>1 @ [JMP (size (ccomp c\<^sub>2))]) (cfs ! k)) (off (bcomp (b, False, size (ccomp c\<^sub>1) + 1) @ ccomp c\<^sub>1 @ [JMP (size (ccomp c\<^sub>2))]) (cfs ! k'))

goal (3 subgoals):
 1. \<And>x1 c1 c2 cfs a b. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); bcomp (x1, False, size (ccomp c1) + 1) @ ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>; cfs ! 0 = (0, a, b); \<not> bval x1 a\<rbrakk> \<Longrightarrow> cpred (IF x1 THEN c1 ELSE c2) (0, a, b) (cfs ! (length cfs - Suc 0))
 2. \<And>x1 c1 c2 cfs a b k aa. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); bcomp (x1, False, size (ccomp c1) + 1) @ ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>; cfs ! 0 = (0, a, b); bval x1 a; k < length cfs; cfs ! k = (size (bcomp (x1, False, size (ccomp c1) + 1)) + size (ccomp c1), aa, b); (c1, a) \<Rightarrow> aa\<rbrakk> \<Longrightarrow> cpred (IF x1 THEN c1 ELSE c2) (0, a, b) (cfs ! (length cfs - Suc 0))
 3. \<And>c1 c2 cfs. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); JMPND (size (ccomp c1) + 1) # ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>\<rbrakk> \<Longrightarrow> cpred (c1 OR c2) (cfs ! 0) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>k'<length cfs. cpred c\<^sub>2 (off (bcomp (b, False, size (ccomp c\<^sub>1) + 1) @ ccomp c\<^sub>1 @ [JMP (size (ccomp c\<^sub>2))]) (cfs ! k)) (off (bcomp (b, False, size (ccomp c\<^sub>1) + 1) @ ccomp c\<^sub>1 @ [JMP (size (ccomp c\<^sub>2))]) (cfs ! k'))
[PROOF STEP]
obtain k' where "k' < length cfs" and "case cfs ! k' of (pc', s', stk') \<Rightarrow>
    pc' = size (?P @ ?cc\<^sub>2) \<and> (c\<^sub>2, s) \<Rightarrow> s' \<and> stk' = stk"
[PROOF STATE]
proof (prove)
using this:
\<exists>k'<length cfs. cpred c\<^sub>2 (off (bcomp (b, False, size (ccomp c\<^sub>1) + 1) @ ccomp c\<^sub>1 @ [JMP (size (ccomp c\<^sub>2))]) (cfs ! k)) (off (bcomp (b, False, size (ccomp c\<^sub>1) + 1) @ ccomp c\<^sub>1 @ [JMP (size (ccomp c\<^sub>2))]) (cfs ! k'))

goal (1 subgoal):
 1. (\<And>k'. \<lbrakk>k' < length cfs; case cfs ! k' of (pc', s', stk') \<Rightarrow> pc' = size ((bcomp (b, False, size (ccomp c\<^sub>1) + 1) @ ccomp c\<^sub>1 @ [JMP (size (ccomp c\<^sub>2))]) @ ccomp c\<^sub>2) \<and> (c\<^sub>2, s) \<Rightarrow> s' \<and> stk' = stk\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using D
[PROOF STATE]
proof (prove)
using this:
\<exists>k'<length cfs. cpred c\<^sub>2 (off (bcomp (b, False, size (ccomp c\<^sub>1) + 1) @ ccomp c\<^sub>1 @ [JMP (size (ccomp c\<^sub>2))]) (cfs ! k)) (off (bcomp (b, False, size (ccomp c\<^sub>1) + 1) @ ccomp c\<^sub>1 @ [JMP (size (ccomp c\<^sub>2))]) (cfs ! k'))
cfs ! k = (size (bcomp (b, False, size (ccomp c\<^sub>1) + 1) @ ccomp c\<^sub>1 @ [JMP (size (ccomp c\<^sub>2))]), s, stk)

goal (1 subgoal):
 1. (\<And>k'. \<lbrakk>k' < length cfs; case cfs ! k' of (pc', s', stk') \<Rightarrow> pc' = size ((bcomp (b, False, size (ccomp c\<^sub>1) + 1) @ ccomp c\<^sub>1 @ [JMP (size (ccomp c\<^sub>2))]) @ ccomp c\<^sub>2) \<and> (c\<^sub>2, s) \<Rightarrow> s' \<and> stk' = stk\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (fastforce simp: cpred_def)
[PROOF STATE]
proof (state)
this:
k' < length cfs
case cfs ! k' of (pc', s', stk') \<Rightarrow> pc' = size ((bcomp (b, False, size (ccomp c\<^sub>1) + 1) @ ccomp c\<^sub>1 @ [JMP (size (ccomp c\<^sub>2))]) @ ccomp c\<^sub>2) \<and> (c\<^sub>2, s) \<Rightarrow> s' \<and> stk' = stk

goal (3 subgoals):
 1. \<And>x1 c1 c2 cfs a b. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); bcomp (x1, False, size (ccomp c1) + 1) @ ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>; cfs ! 0 = (0, a, b); \<not> bval x1 a\<rbrakk> \<Longrightarrow> cpred (IF x1 THEN c1 ELSE c2) (0, a, b) (cfs ! (length cfs - Suc 0))
 2. \<And>x1 c1 c2 cfs a b k aa. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); bcomp (x1, False, size (ccomp c1) + 1) @ ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>; cfs ! 0 = (0, a, b); bval x1 a; k < length cfs; cfs ! k = (size (bcomp (x1, False, size (ccomp c1) + 1)) + size (ccomp c1), aa, b); (c1, a) \<Rightarrow> aa\<rbrakk> \<Longrightarrow> cpred (IF x1 THEN c1 ELSE c2) (0, a, b) (cfs ! (length cfs - Suc 0))
 3. \<And>c1 c2 cfs. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); JMPND (size (ccomp c1) + 1) # ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>\<rbrakk> \<Longrightarrow> cpred (c1 OR c2) (cfs ! 0) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
thus "cpred (IF b THEN c\<^sub>1 ELSE c\<^sub>2) (0, s, stk) (cfs ! (length cfs - Suc 0))"
[PROOF STATE]
proof (prove)
using this:
k' < length cfs
case cfs ! k' of (pc', s', stk') \<Rightarrow> pc' = size ((bcomp (b, False, size (ccomp c\<^sub>1) + 1) @ ccomp c\<^sub>1 @ [JMP (size (ccomp c\<^sub>2))]) @ ccomp c\<^sub>2) \<and> (c\<^sub>2, s) \<Rightarrow> s' \<and> stk' = stk

goal (1 subgoal):
 1. cpred (IF b THEN c\<^sub>1 ELSE c\<^sub>2) (0, s, stk) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
using A and B
[PROOF STATE]
proof (prove)
using this:
k' < length cfs
case cfs ! k' of (pc', s', stk') \<Rightarrow> pc' = size ((bcomp (b, False, size (ccomp c\<^sub>1) + 1) @ ccomp c\<^sub>1 @ [JMP (size (ccomp c\<^sub>2))]) @ ccomp c\<^sub>2) \<and> (c\<^sub>2, s) \<Rightarrow> s' \<and> stk' = stk
bcomp (b, False, size (ccomp c\<^sub>1) + 1) @ ccomp c\<^sub>1 @ JMP (size (ccomp c\<^sub>2)) # ccomp c\<^sub>2 \<Turnstile> cfs\<box>
\<not> bval b s

goal (1 subgoal):
 1. cpred (IF b THEN c\<^sub>1 ELSE c\<^sub>2) (0, s, stk) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
by (insert execl_last, auto simp: execl_all_def cpred_def Let_def)
[PROOF STATE]
proof (state)
this:
cpred (IF b THEN c\<^sub>1 ELSE c\<^sub>2) (0, s, stk) (cfs ! (length cfs - Suc 0))

goal (2 subgoals):
 1. \<And>x1 c1 c2 cfs a b k aa. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); bcomp (x1, False, size (ccomp c1) + 1) @ ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>; cfs ! 0 = (0, a, b); bval x1 a; k < length cfs; cfs ! k = (size (bcomp (x1, False, size (ccomp c1) + 1)) + size (ccomp c1), aa, b); (c1, a) \<Rightarrow> aa\<rbrakk> \<Longrightarrow> cpred (IF x1 THEN c1 ELSE c2) (0, a, b) (cfs ! (length cfs - Suc 0))
 2. \<And>c1 c2 cfs. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); JMPND (size (ccomp c1) + 1) # ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>\<rbrakk> \<Longrightarrow> cpred (c1 OR c2) (cfs ! 0) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x1 c1 c2 cfs a b k aa. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); bcomp (x1, False, size (ccomp c1) + 1) @ ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>; cfs ! 0 = (0, a, b); bval x1 a; k < length cfs; cfs ! k = (size (bcomp (x1, False, size (ccomp c1) + 1)) + size (ccomp c1), aa, b); (c1, a) \<Rightarrow> aa\<rbrakk> \<Longrightarrow> cpred (IF x1 THEN c1 ELSE c2) (0, a, b) (cfs ! (length cfs - Suc 0))
 2. \<And>c1 c2 cfs. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); JMPND (size (ccomp c1) + 1) # ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>\<rbrakk> \<Longrightarrow> cpred (c1 OR c2) (cfs ! 0) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
fix b c\<^sub>1 c\<^sub>2 cfs s s' stk k
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x1 c1 c2 cfs a b k aa. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); bcomp (x1, False, size (ccomp c1) + 1) @ ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>; cfs ! 0 = (0, a, b); bval x1 a; k < length cfs; cfs ! k = (size (bcomp (x1, False, size (ccomp c1) + 1)) + size (ccomp c1), aa, b); (c1, a) \<Rightarrow> aa\<rbrakk> \<Longrightarrow> cpred (IF x1 THEN c1 ELSE c2) (0, a, b) (cfs ! (length cfs - Suc 0))
 2. \<And>c1 c2 cfs. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); JMPND (size (ccomp c1) + 1) # ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>\<rbrakk> \<Longrightarrow> cpred (c1 OR c2) (cfs ! 0) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
assume A: "bcomp (b, False, size (ccomp c\<^sub>1) + 1) @ ccomp c\<^sub>1 @
    JMP (size (ccomp c\<^sub>2)) # ccomp c\<^sub>2 \<Turnstile> cfs\<box>"
    (is "?cb @ ?cc\<^sub>1 @ ?i # ?cc\<^sub>2 \<Turnstile> _\<box>")
[PROOF STATE]
proof (state)
this:
bcomp (b, False, size (ccomp c\<^sub>1) + 1) @ ccomp c\<^sub>1 @ JMP (size (ccomp c\<^sub>2)) # ccomp c\<^sub>2 \<Turnstile> cfs\<box>

goal (2 subgoals):
 1. \<And>x1 c1 c2 cfs a b k aa. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); bcomp (x1, False, size (ccomp c1) + 1) @ ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>; cfs ! 0 = (0, a, b); bval x1 a; k < length cfs; cfs ! k = (size (bcomp (x1, False, size (ccomp c1) + 1)) + size (ccomp c1), aa, b); (c1, a) \<Rightarrow> aa\<rbrakk> \<Longrightarrow> cpred (IF x1 THEN c1 ELSE c2) (0, a, b) (cfs ! (length cfs - Suc 0))
 2. \<And>c1 c2 cfs. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); JMPND (size (ccomp c1) + 1) # ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>\<rbrakk> \<Longrightarrow> cpred (c1 OR c2) (cfs ! 0) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
assume B: "k < length cfs" and C: "cfs ! k = (size ?cb + size ?cc\<^sub>1, s', stk)"
[PROOF STATE]
proof (state)
this:
k < length cfs
cfs ! k = (size (bcomp (b, False, size (ccomp c\<^sub>1) + 1)) + size (ccomp c\<^sub>1), s', stk)

goal (2 subgoals):
 1. \<And>x1 c1 c2 cfs a b k aa. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); bcomp (x1, False, size (ccomp c1) + 1) @ ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>; cfs ! 0 = (0, a, b); bval x1 a; k < length cfs; cfs ! k = (size (bcomp (x1, False, size (ccomp c1) + 1)) + size (ccomp c1), aa, b); (c1, a) \<Rightarrow> aa\<rbrakk> \<Longrightarrow> cpred (IF x1 THEN c1 ELSE c2) (0, a, b) (cfs ! (length cfs - Suc 0))
 2. \<And>c1 c2 cfs. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); JMPND (size (ccomp c1) + 1) # ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>\<rbrakk> \<Longrightarrow> cpred (c1 OR c2) (cfs ! 0) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
hence D: "cfs ! Suc k = (size (?cb @ ?cc\<^sub>1 @ ?i # ?cc\<^sub>2), s', stk)"
    (is "_ = (size ?P, _, _)")
[PROOF STATE]
proof (prove)
using this:
k < length cfs
cfs ! k = (size (bcomp (b, False, size (ccomp c\<^sub>1) + 1)) + size (ccomp c\<^sub>1), s', stk)

goal (1 subgoal):
 1. cfs ! Suc k = (size (bcomp (b, False, size (ccomp c\<^sub>1) + 1) @ ccomp c\<^sub>1 @ JMP (size (ccomp c\<^sub>2)) # ccomp c\<^sub>2), s', stk)
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
k < length cfs
cfs ! k = (size (bcomp (b, False, size (ccomp c\<^sub>1) + 1)) + size (ccomp c\<^sub>1), s', stk)
bcomp (b, False, size (ccomp c\<^sub>1) + 1) @ ccomp c\<^sub>1 @ JMP (size (ccomp c\<^sub>2)) # ccomp c\<^sub>2 \<Turnstile> cfs\<box>

goal (1 subgoal):
 1. cfs ! Suc k = (size (bcomp (b, False, size (ccomp c\<^sub>1) + 1) @ ccomp c\<^sub>1 @ JMP (size (ccomp c\<^sub>2)) # ccomp c\<^sub>2), s', stk)
[PROOF STEP]
by (insert execl_next [of ?P cfs k], simp add: execl_all_def,
     drule_tac impI, auto)
[PROOF STATE]
proof (state)
this:
cfs ! Suc k = (size (bcomp (b, False, size (ccomp c\<^sub>1) + 1) @ ccomp c\<^sub>1 @ JMP (size (ccomp c\<^sub>2)) # ccomp c\<^sub>2), s', stk)

goal (2 subgoals):
 1. \<And>x1 c1 c2 cfs a b k aa. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); bcomp (x1, False, size (ccomp c1) + 1) @ ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>; cfs ! 0 = (0, a, b); bval x1 a; k < length cfs; cfs ! k = (size (bcomp (x1, False, size (ccomp c1) + 1)) + size (ccomp c1), aa, b); (c1, a) \<Rightarrow> aa\<rbrakk> \<Longrightarrow> cpred (IF x1 THEN c1 ELSE c2) (0, a, b) (cfs ! (length cfs - Suc 0))
 2. \<And>c1 c2 cfs. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); JMPND (size (ccomp c1) + 1) # ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>\<rbrakk> \<Longrightarrow> cpred (c1 OR c2) (cfs ! 0) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
assume "bval b s" and "(c\<^sub>1, s) \<Rightarrow> s'"
[PROOF STATE]
proof (state)
this:
bval b s
(c\<^sub>1, s) \<Rightarrow> s'

goal (2 subgoals):
 1. \<And>x1 c1 c2 cfs a b k aa. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); bcomp (x1, False, size (ccomp c1) + 1) @ ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>; cfs ! 0 = (0, a, b); bval x1 a; k < length cfs; cfs ! k = (size (bcomp (x1, False, size (ccomp c1) + 1)) + size (ccomp c1), aa, b); (c1, a) \<Rightarrow> aa\<rbrakk> \<Longrightarrow> cpred (IF x1 THEN c1 ELSE c2) (0, a, b) (cfs ! (length cfs - Suc 0))
 2. \<And>c1 c2 cfs. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); JMPND (size (ccomp c1) + 1) # ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>\<rbrakk> \<Longrightarrow> cpred (c1 OR c2) (cfs ! 0) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
thus "cpred (IF b THEN c\<^sub>1 ELSE c\<^sub>2) (0, s, stk) (cfs ! (length cfs - Suc 0))"
[PROOF STATE]
proof (prove)
using this:
bval b s
(c\<^sub>1, s) \<Rightarrow> s'

goal (1 subgoal):
 1. cpred (IF b THEN c\<^sub>1 ELSE c\<^sub>2) (0, s, stk) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
using A and B and C and D
[PROOF STATE]
proof (prove)
using this:
bval b s
(c\<^sub>1, s) \<Rightarrow> s'
bcomp (b, False, size (ccomp c\<^sub>1) + 1) @ ccomp c\<^sub>1 @ JMP (size (ccomp c\<^sub>2)) # ccomp c\<^sub>2 \<Turnstile> cfs\<box>
k < length cfs
cfs ! k = (size (bcomp (b, False, size (ccomp c\<^sub>1) + 1)) + size (ccomp c\<^sub>1), s', stk)
cfs ! Suc k = (size (bcomp (b, False, size (ccomp c\<^sub>1) + 1) @ ccomp c\<^sub>1 @ JMP (size (ccomp c\<^sub>2)) # ccomp c\<^sub>2), s', stk)

goal (1 subgoal):
 1. cpred (IF b THEN c\<^sub>1 ELSE c\<^sub>2) (0, s, stk) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
by (insert execl_last [of ?P cfs "Suc k"],
     simp add: execl_all_def cpred_def Let_def, drule_tac impI, auto)
[PROOF STATE]
proof (state)
this:
cpred (IF b THEN c\<^sub>1 ELSE c\<^sub>2) (0, s, stk) (cfs ! (length cfs - Suc 0))

goal (1 subgoal):
 1. \<And>c1 c2 cfs. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); JMPND (size (ccomp c1) + 1) # ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>\<rbrakk> \<Longrightarrow> cpred (c1 OR c2) (cfs ! 0) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>c1 c2 cfs. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); JMPND (size (ccomp c1) + 1) # ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>\<rbrakk> \<Longrightarrow> cpred (c1 OR c2) (cfs ! 0) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
fix c\<^sub>1 c\<^sub>2 cfs
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>c1 c2 cfs. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); JMPND (size (ccomp c1) + 1) # ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>\<rbrakk> \<Longrightarrow> cpred (c1 OR c2) (cfs ! 0) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
assume A: "JMPND (size (ccomp c\<^sub>1) + 1) # ccomp c\<^sub>1 @
    JMP (size (ccomp c\<^sub>2)) # ccomp c\<^sub>2 \<Turnstile> cfs\<box>"
    (is "JMPND (?n\<^sub>1 + 1) # ?cc\<^sub>1 @ JMP ?n\<^sub>2 # ?cc\<^sub>2 \<Turnstile> _\<box>")
[PROOF STATE]
proof (state)
this:
JMPND (size (ccomp c\<^sub>1) + 1) # ccomp c\<^sub>1 @ JMP (size (ccomp c\<^sub>2)) # ccomp c\<^sub>2 \<Turnstile> cfs\<box>

goal (1 subgoal):
 1. \<And>c1 c2 cfs. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); JMPND (size (ccomp c1) + 1) # ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>\<rbrakk> \<Longrightarrow> cpred (c1 OR c2) (cfs ! 0) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
let ?P = "JMPND (?n\<^sub>1 + 1) # ?cc\<^sub>1 @ [JMP ?n\<^sub>2]"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>c1 c2 cfs. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); JMPND (size (ccomp c1) + 1) # ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>\<rbrakk> \<Longrightarrow> cpred (c1 OR c2) (cfs ! 0) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
assume
    B: "\<And>cfs. ?cc\<^sub>1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c\<^sub>1 (cfs ! 0) (cfs ! (length cfs - Suc 0))" and
    C: "\<And>cfs. ?cc\<^sub>2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c\<^sub>2 (cfs ! 0) (cfs ! (length cfs - Suc 0))"
[PROOF STATE]
proof (state)
this:
ccomp c\<^sub>1 \<Turnstile> ?cfs\<box> \<Longrightarrow> cpred c\<^sub>1 (?cfs ! 0) (?cfs ! (length ?cfs - Suc 0))
ccomp c\<^sub>2 \<Turnstile> ?cfs\<box> \<Longrightarrow> cpred c\<^sub>2 (?cfs ! 0) (?cfs ! (length ?cfs - Suc 0))

goal (1 subgoal):
 1. \<And>c1 c2 cfs. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); JMPND (size (ccomp c1) + 1) # ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>\<rbrakk> \<Longrightarrow> cpred (c1 OR c2) (cfs ! 0) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
from A
[PROOF STATE]
proof (chain)
picking this:
JMPND (size (ccomp c\<^sub>1) + 1) # ccomp c\<^sub>1 @ JMP (size (ccomp c\<^sub>2)) # ccomp c\<^sub>2 \<Turnstile> cfs\<box>
[PROOF STEP]
obtain s stk where D: "cfs ! 0 = (0, s, stk)"
[PROOF STATE]
proof (prove)
using this:
JMPND (size (ccomp c\<^sub>1) + 1) # ccomp c\<^sub>1 @ JMP (size (ccomp c\<^sub>2)) # ccomp c\<^sub>2 \<Turnstile> cfs\<box>

goal (1 subgoal):
 1. (\<And>s stk. cfs ! 0 = (0, s, stk) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases "cfs ! 0", simp add: execl_all_def)
[PROOF STATE]
proof (state)
this:
cfs ! 0 = (0, s, stk)

goal (1 subgoal):
 1. \<And>c1 c2 cfs. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); JMPND (size (ccomp c1) + 1) # ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>\<rbrakk> \<Longrightarrow> cpred (c1 OR c2) (cfs ! 0) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
with A
[PROOF STATE]
proof (chain)
picking this:
JMPND (size (ccomp c\<^sub>1) + 1) # ccomp c\<^sub>1 @ JMP (size (ccomp c\<^sub>2)) # ccomp c\<^sub>2 \<Turnstile> cfs\<box>
cfs ! 0 = (0, s, stk)
[PROOF STEP]
have "cfs ! 1 = (1, s, stk) \<or> cfs ! 1 = (?n\<^sub>1 + 2, s, stk)"
[PROOF STATE]
proof (prove)
using this:
JMPND (size (ccomp c\<^sub>1) + 1) # ccomp c\<^sub>1 @ JMP (size (ccomp c\<^sub>2)) # ccomp c\<^sub>2 \<Turnstile> cfs\<box>
cfs ! 0 = (0, s, stk)

goal (1 subgoal):
 1. cfs ! 1 = (1, s, stk) \<or> cfs ! 1 = (size (ccomp c\<^sub>1) + 2, s, stk)
[PROOF STEP]
by (insert execl_next [of "?P @ ?cc\<^sub>2" cfs 0], simp add: execl_all_def,
     drule_tac impI, auto)
[PROOF STATE]
proof (state)
this:
cfs ! 1 = (1, s, stk) \<or> cfs ! 1 = (size (ccomp c\<^sub>1) + 2, s, stk)

goal (1 subgoal):
 1. \<And>c1 c2 cfs. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); JMPND (size (ccomp c1) + 1) # ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>\<rbrakk> \<Longrightarrow> cpred (c1 OR c2) (cfs ! 0) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
cfs ! 1 = (1, s, stk) \<or> cfs ! 1 = (size (ccomp c\<^sub>1) + 2, s, stk)

goal (1 subgoal):
 1. \<And>c1 c2 cfs. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); JMPND (size (ccomp c1) + 1) # ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>\<rbrakk> \<Longrightarrow> cpred (c1 OR c2) (cfs ! 0) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
cfs ! 1 = (1, s, stk) \<or> cfs ! 1 = (size (ccomp c\<^sub>1) + 2, s, stk)

goal (1 subgoal):
 1. \<And>c1 c2 cfs. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); JMPND (size (ccomp c1) + 1) # ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>\<rbrakk> \<Longrightarrow> cpred (c1 OR c2) (cfs ! 0) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
assume E: "cfs ! 1 = (1, s, stk)"
[PROOF STATE]
proof (state)
this:
cfs ! 1 = (1, s, stk)

goal (1 subgoal):
 1. \<And>c1 c2 cfs. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); JMPND (size (ccomp c1) + 1) # ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>\<rbrakk> \<Longrightarrow> cpred (c1 OR c2) (cfs ! 0) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
hence "\<exists>k < length cfs. cpred c\<^sub>1 (off [hd ?P] (cfs ! 1)) (off [hd ?P] (cfs ! k))"
[PROOF STATE]
proof (prove)
using this:
cfs ! 1 = (1, s, stk)

goal (1 subgoal):
 1. \<exists>k<length cfs. cpred c\<^sub>1 (off [hd (JMPND (size (ccomp c\<^sub>1) + 1) # ccomp c\<^sub>1 @ [JMP (size (ccomp c\<^sub>2))])] (cfs ! 1)) (off [hd (JMPND (size (ccomp c\<^sub>1) + 1) # ccomp c\<^sub>1 @ [JMP (size (ccomp c\<^sub>2))])] (cfs ! k))
[PROOF STEP]
using A and B
[PROOF STATE]
proof (prove)
using this:
cfs ! 1 = (1, s, stk)
JMPND (size (ccomp c\<^sub>1) + 1) # ccomp c\<^sub>1 @ JMP (size (ccomp c\<^sub>2)) # ccomp c\<^sub>2 \<Turnstile> cfs\<box>
ccomp c\<^sub>1 \<Turnstile> ?cfs\<box> \<Longrightarrow> cpred c\<^sub>1 (?cfs ! 0) (?cfs ! (length ?cfs - Suc 0))

goal (1 subgoal):
 1. \<exists>k<length cfs. cpred c\<^sub>1 (off [hd (JMPND (size (ccomp c\<^sub>1) + 1) # ccomp c\<^sub>1 @ [JMP (size (ccomp c\<^sub>2))])] (cfs ! 1)) (off [hd (JMPND (size (ccomp c\<^sub>1) + 1) # ccomp c\<^sub>1 @ [JMP (size (ccomp c\<^sub>2))])] (cfs ! k))
[PROOF STEP]
by (rule_tac execl_all_sub, auto simp: execl_all_def)
[PROOF STATE]
proof (state)
this:
\<exists>k<length cfs. cpred c\<^sub>1 (off [hd (JMPND (size (ccomp c\<^sub>1) + 1) # ccomp c\<^sub>1 @ [JMP (size (ccomp c\<^sub>2))])] (cfs ! 1)) (off [hd (JMPND (size (ccomp c\<^sub>1) + 1) # ccomp c\<^sub>1 @ [JMP (size (ccomp c\<^sub>2))])] (cfs ! k))

goal (1 subgoal):
 1. \<And>c1 c2 cfs. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); JMPND (size (ccomp c1) + 1) # ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>\<rbrakk> \<Longrightarrow> cpred (c1 OR c2) (cfs ! 0) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>k<length cfs. cpred c\<^sub>1 (off [hd (JMPND (size (ccomp c\<^sub>1) + 1) # ccomp c\<^sub>1 @ [JMP (size (ccomp c\<^sub>2))])] (cfs ! 1)) (off [hd (JMPND (size (ccomp c\<^sub>1) + 1) # ccomp c\<^sub>1 @ [JMP (size (ccomp c\<^sub>2))])] (cfs ! k))
[PROOF STEP]
obtain k where "k < length cfs" and "case cfs ! k of (pc', s', stk') \<Rightarrow>
      pc' = ?n\<^sub>1 + 1 \<and> (c\<^sub>1, s) \<Rightarrow> s' \<and> stk' = stk"
[PROOF STATE]
proof (prove)
using this:
\<exists>k<length cfs. cpred c\<^sub>1 (off [hd (JMPND (size (ccomp c\<^sub>1) + 1) # ccomp c\<^sub>1 @ [JMP (size (ccomp c\<^sub>2))])] (cfs ! 1)) (off [hd (JMPND (size (ccomp c\<^sub>1) + 1) # ccomp c\<^sub>1 @ [JMP (size (ccomp c\<^sub>2))])] (cfs ! k))

goal (1 subgoal):
 1. (\<And>k. \<lbrakk>k < length cfs; case cfs ! k of (pc', s', stk') \<Rightarrow> pc' = size (ccomp c\<^sub>1) + 1 \<and> (c\<^sub>1, s) \<Rightarrow> s' \<and> stk' = stk\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using E
[PROOF STATE]
proof (prove)
using this:
\<exists>k<length cfs. cpred c\<^sub>1 (off [hd (JMPND (size (ccomp c\<^sub>1) + 1) # ccomp c\<^sub>1 @ [JMP (size (ccomp c\<^sub>2))])] (cfs ! 1)) (off [hd (JMPND (size (ccomp c\<^sub>1) + 1) # ccomp c\<^sub>1 @ [JMP (size (ccomp c\<^sub>2))])] (cfs ! k))
cfs ! 1 = (1, s, stk)

goal (1 subgoal):
 1. (\<And>k. \<lbrakk>k < length cfs; case cfs ! k of (pc', s', stk') \<Rightarrow> pc' = size (ccomp c\<^sub>1) + 1 \<and> (c\<^sub>1, s) \<Rightarrow> s' \<and> stk' = stk\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (fastforce simp: cpred_def)
[PROOF STATE]
proof (state)
this:
k < length cfs
case cfs ! k of (pc', s', stk') \<Rightarrow> pc' = size (ccomp c\<^sub>1) + 1 \<and> (c\<^sub>1, s) \<Rightarrow> s' \<and> stk' = stk

goal (1 subgoal):
 1. \<And>c1 c2 cfs. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); JMPND (size (ccomp c1) + 1) # ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>\<rbrakk> \<Longrightarrow> cpred (c1 OR c2) (cfs ! 0) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
k < length cfs
case cfs ! k of (pc', s', stk') \<Rightarrow> pc' = size (ccomp c\<^sub>1) + 1 \<and> (c\<^sub>1, s) \<Rightarrow> s' \<and> stk' = stk

goal (1 subgoal):
 1. \<And>c1 c2 cfs. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); JMPND (size (ccomp c1) + 1) # ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>\<rbrakk> \<Longrightarrow> cpred (c1 OR c2) (cfs ! 0) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
k < length cfs
case cfs ! k of (pc', s', stk') \<Rightarrow> pc' = size (ccomp c\<^sub>1) + 1 \<and> (c\<^sub>1, s) \<Rightarrow> s' \<and> stk' = stk
[PROOF STEP]
have "case cfs ! Suc k of (pc', s', stk') \<Rightarrow>
      pc' = ?n\<^sub>1 + ?n\<^sub>2 + 2 \<and> (c\<^sub>1, s) \<Rightarrow> s' \<and> stk' = stk"
[PROOF STATE]
proof (prove)
using this:
k < length cfs
case cfs ! k of (pc', s', stk') \<Rightarrow> pc' = size (ccomp c\<^sub>1) + 1 \<and> (c\<^sub>1, s) \<Rightarrow> s' \<and> stk' = stk

goal (1 subgoal):
 1. case cfs ! Suc k of (pc', s', stk') \<Rightarrow> pc' = size (ccomp c\<^sub>1) + size (ccomp c\<^sub>2) + 2 \<and> (c\<^sub>1, s) \<Rightarrow> s' \<and> stk' = stk
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
k < length cfs
case cfs ! k of (pc', s', stk') \<Rightarrow> pc' = size (ccomp c\<^sub>1) + 1 \<and> (c\<^sub>1, s) \<Rightarrow> s' \<and> stk' = stk
JMPND (size (ccomp c\<^sub>1) + 1) # ccomp c\<^sub>1 @ JMP (size (ccomp c\<^sub>2)) # ccomp c\<^sub>2 \<Turnstile> cfs\<box>

goal (1 subgoal):
 1. case cfs ! Suc k of (pc', s', stk') \<Rightarrow> pc' = size (ccomp c\<^sub>1) + size (ccomp c\<^sub>2) + 2 \<and> (c\<^sub>1, s) \<Rightarrow> s' \<and> stk' = stk
[PROOF STEP]
by (insert execl_next [of "?P @ ?cc\<^sub>2" cfs k], simp add: execl_all_def,
       drule_tac impI, auto)
[PROOF STATE]
proof (state)
this:
case cfs ! Suc k of (pc', s', stk') \<Rightarrow> pc' = size (ccomp c\<^sub>1) + size (ccomp c\<^sub>2) + 2 \<and> (c\<^sub>1, s) \<Rightarrow> s' \<and> stk' = stk

goal (1 subgoal):
 1. \<And>c1 c2 cfs. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); JMPND (size (ccomp c1) + 1) # ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>\<rbrakk> \<Longrightarrow> cpred (c1 OR c2) (cfs ! 0) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
k < length cfs
case cfs ! k of (pc', s', stk') \<Rightarrow> pc' = size (ccomp c\<^sub>1) + 1 \<and> (c\<^sub>1, s) \<Rightarrow> s' \<and> stk' = stk
case cfs ! Suc k of (pc', s', stk') \<Rightarrow> pc' = size (ccomp c\<^sub>1) + size (ccomp c\<^sub>2) + 2 \<and> (c\<^sub>1, s) \<Rightarrow> s' \<and> stk' = stk
[PROOF STEP]
have "cpred (c\<^sub>1 OR c\<^sub>2) (cfs ! 0) (cfs ! (length cfs - Suc 0))"
[PROOF STATE]
proof (prove)
using this:
k < length cfs
case cfs ! k of (pc', s', stk') \<Rightarrow> pc' = size (ccomp c\<^sub>1) + 1 \<and> (c\<^sub>1, s) \<Rightarrow> s' \<and> stk' = stk
case cfs ! Suc k of (pc', s', stk') \<Rightarrow> pc' = size (ccomp c\<^sub>1) + size (ccomp c\<^sub>2) + 2 \<and> (c\<^sub>1, s) \<Rightarrow> s' \<and> stk' = stk

goal (1 subgoal):
 1. cpred (c\<^sub>1 OR c\<^sub>2) (cfs ! 0) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
using A and D
[PROOF STATE]
proof (prove)
using this:
k < length cfs
case cfs ! k of (pc', s', stk') \<Rightarrow> pc' = size (ccomp c\<^sub>1) + 1 \<and> (c\<^sub>1, s) \<Rightarrow> s' \<and> stk' = stk
case cfs ! Suc k of (pc', s', stk') \<Rightarrow> pc' = size (ccomp c\<^sub>1) + size (ccomp c\<^sub>2) + 2 \<and> (c\<^sub>1, s) \<Rightarrow> s' \<and> stk' = stk
JMPND (size (ccomp c\<^sub>1) + 1) # ccomp c\<^sub>1 @ JMP (size (ccomp c\<^sub>2)) # ccomp c\<^sub>2 \<Turnstile> cfs\<box>
cfs ! 0 = (0, s, stk)

goal (1 subgoal):
 1. cpred (c\<^sub>1 OR c\<^sub>2) (cfs ! 0) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
by (insert execl_last [of "?P @ ?cc\<^sub>2" cfs "Suc k"],
       simp add: execl_all_def cpred_def split_def Let_def, drule_tac impI, auto)
[PROOF STATE]
proof (state)
this:
cpred (c\<^sub>1 OR c\<^sub>2) (cfs ! 0) (cfs ! (length cfs - Suc 0))

goal (1 subgoal):
 1. \<And>c1 c2 cfs. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); JMPND (size (ccomp c1) + 1) # ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>\<rbrakk> \<Longrightarrow> cpred (c1 OR c2) (cfs ! 0) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
cfs ! 1 = (1, s, stk) \<Longrightarrow> cpred (c\<^sub>1 OR c\<^sub>2) (cfs ! 0) (cfs ! (length cfs - Suc 0))

goal (1 subgoal):
 1. \<And>c1 c2 cfs. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); JMPND (size (ccomp c1) + 1) # ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>\<rbrakk> \<Longrightarrow> cpred (c1 OR c2) (cfs ! 0) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
cfs ! 1 = (1, s, stk) \<Longrightarrow> cpred (c\<^sub>1 OR c\<^sub>2) (cfs ! 0) (cfs ! (length cfs - Suc 0))

goal (1 subgoal):
 1. \<And>c1 c2 cfs. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); JMPND (size (ccomp c1) + 1) # ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>\<rbrakk> \<Longrightarrow> cpred (c1 OR c2) (cfs ! 0) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
cfs ! 1 = (1, s, stk) \<Longrightarrow> cpred (c\<^sub>1 OR c\<^sub>2) (cfs ! 0) (cfs ! (length cfs - Suc 0))

goal (1 subgoal):
 1. \<And>c1 c2 cfs. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); JMPND (size (ccomp c1) + 1) # ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>\<rbrakk> \<Longrightarrow> cpred (c1 OR c2) (cfs ! 0) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
assume E: "cfs ! 1 = (?n\<^sub>1 + 2, s, stk)"
[PROOF STATE]
proof (state)
this:
cfs ! 1 = (size (ccomp c\<^sub>1) + 2, s, stk)

goal (1 subgoal):
 1. \<And>c1 c2 cfs. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); JMPND (size (ccomp c1) + 1) # ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>\<rbrakk> \<Longrightarrow> cpred (c1 OR c2) (cfs ! 0) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
with A and C
[PROOF STATE]
proof (chain)
picking this:
JMPND (size (ccomp c\<^sub>1) + 1) # ccomp c\<^sub>1 @ JMP (size (ccomp c\<^sub>2)) # ccomp c\<^sub>2 \<Turnstile> cfs\<box>
ccomp c\<^sub>2 \<Turnstile> ?cfs\<box> \<Longrightarrow> cpred c\<^sub>2 (?cfs ! 0) (?cfs ! (length ?cfs - Suc 0))
cfs ! 1 = (size (ccomp c\<^sub>1) + 2, s, stk)
[PROOF STEP]
have "\<exists>k<length cfs. cpred c\<^sub>2 (off ?P (cfs!1)) (off ?P (cfs!k))"
[PROOF STATE]
proof (prove)
using this:
JMPND (size (ccomp c\<^sub>1) + 1) # ccomp c\<^sub>1 @ JMP (size (ccomp c\<^sub>2)) # ccomp c\<^sub>2 \<Turnstile> cfs\<box>
ccomp c\<^sub>2 \<Turnstile> ?cfs\<box> \<Longrightarrow> cpred c\<^sub>2 (?cfs ! 0) (?cfs ! (length ?cfs - Suc 0))
cfs ! 1 = (size (ccomp c\<^sub>1) + 2, s, stk)

goal (1 subgoal):
 1. \<exists>k<length cfs. cpred c\<^sub>2 (off (JMPND (size (ccomp c\<^sub>1) + 1) # ccomp c\<^sub>1 @ [JMP (size (ccomp c\<^sub>2))]) (cfs ! 1)) (off (JMPND (size (ccomp c\<^sub>1) + 1) # ccomp c\<^sub>1 @ [JMP (size (ccomp c\<^sub>2))]) (cfs ! k))
[PROOF STEP]
by (rule_tac execl_all_sub [where P'' = "[]"], auto simp: execl_all_def)
[PROOF STATE]
proof (state)
this:
\<exists>k<length cfs. cpred c\<^sub>2 (off (JMPND (size (ccomp c\<^sub>1) + 1) # ccomp c\<^sub>1 @ [JMP (size (ccomp c\<^sub>2))]) (cfs ! 1)) (off (JMPND (size (ccomp c\<^sub>1) + 1) # ccomp c\<^sub>1 @ [JMP (size (ccomp c\<^sub>2))]) (cfs ! k))

goal (1 subgoal):
 1. \<And>c1 c2 cfs. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); JMPND (size (ccomp c1) + 1) # ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>\<rbrakk> \<Longrightarrow> cpred (c1 OR c2) (cfs ! 0) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>k<length cfs. cpred c\<^sub>2 (off (JMPND (size (ccomp c\<^sub>1) + 1) # ccomp c\<^sub>1 @ [JMP (size (ccomp c\<^sub>2))]) (cfs ! 1)) (off (JMPND (size (ccomp c\<^sub>1) + 1) # ccomp c\<^sub>1 @ [JMP (size (ccomp c\<^sub>2))]) (cfs ! k))
[PROOF STEP]
obtain k where "k < length cfs" and "case cfs ! k of (pc', s', stk') \<Rightarrow>
      pc' = ?n\<^sub>1 + ?n\<^sub>2 + 2 \<and> (c\<^sub>2, s) \<Rightarrow> s' \<and> stk' = stk"
[PROOF STATE]
proof (prove)
using this:
\<exists>k<length cfs. cpred c\<^sub>2 (off (JMPND (size (ccomp c\<^sub>1) + 1) # ccomp c\<^sub>1 @ [JMP (size (ccomp c\<^sub>2))]) (cfs ! 1)) (off (JMPND (size (ccomp c\<^sub>1) + 1) # ccomp c\<^sub>1 @ [JMP (size (ccomp c\<^sub>2))]) (cfs ! k))

goal (1 subgoal):
 1. (\<And>k. \<lbrakk>k < length cfs; case cfs ! k of (pc', s', stk') \<Rightarrow> pc' = size (ccomp c\<^sub>1) + size (ccomp c\<^sub>2) + 2 \<and> (c\<^sub>2, s) \<Rightarrow> s' \<and> stk' = stk\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using E
[PROOF STATE]
proof (prove)
using this:
\<exists>k<length cfs. cpred c\<^sub>2 (off (JMPND (size (ccomp c\<^sub>1) + 1) # ccomp c\<^sub>1 @ [JMP (size (ccomp c\<^sub>2))]) (cfs ! 1)) (off (JMPND (size (ccomp c\<^sub>1) + 1) # ccomp c\<^sub>1 @ [JMP (size (ccomp c\<^sub>2))]) (cfs ! k))
cfs ! 1 = (size (ccomp c\<^sub>1) + 2, s, stk)

goal (1 subgoal):
 1. (\<And>k. \<lbrakk>k < length cfs; case cfs ! k of (pc', s', stk') \<Rightarrow> pc' = size (ccomp c\<^sub>1) + size (ccomp c\<^sub>2) + 2 \<and> (c\<^sub>2, s) \<Rightarrow> s' \<and> stk' = stk\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (fastforce simp: cpred_def)
[PROOF STATE]
proof (state)
this:
k < length cfs
case cfs ! k of (pc', s', stk') \<Rightarrow> pc' = size (ccomp c\<^sub>1) + size (ccomp c\<^sub>2) + 2 \<and> (c\<^sub>2, s) \<Rightarrow> s' \<and> stk' = stk

goal (1 subgoal):
 1. \<And>c1 c2 cfs. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); JMPND (size (ccomp c1) + 1) # ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>\<rbrakk> \<Longrightarrow> cpred (c1 OR c2) (cfs ! 0) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
with A and D
[PROOF STATE]
proof (chain)
picking this:
JMPND (size (ccomp c\<^sub>1) + 1) # ccomp c\<^sub>1 @ JMP (size (ccomp c\<^sub>2)) # ccomp c\<^sub>2 \<Turnstile> cfs\<box>
cfs ! 0 = (0, s, stk)
k < length cfs
case cfs ! k of (pc', s', stk') \<Rightarrow> pc' = size (ccomp c\<^sub>1) + size (ccomp c\<^sub>2) + 2 \<and> (c\<^sub>2, s) \<Rightarrow> s' \<and> stk' = stk
[PROOF STEP]
have "cpred (c\<^sub>1 OR c\<^sub>2) (cfs ! 0) (cfs ! (length cfs - Suc 0))"
[PROOF STATE]
proof (prove)
using this:
JMPND (size (ccomp c\<^sub>1) + 1) # ccomp c\<^sub>1 @ JMP (size (ccomp c\<^sub>2)) # ccomp c\<^sub>2 \<Turnstile> cfs\<box>
cfs ! 0 = (0, s, stk)
k < length cfs
case cfs ! k of (pc', s', stk') \<Rightarrow> pc' = size (ccomp c\<^sub>1) + size (ccomp c\<^sub>2) + 2 \<and> (c\<^sub>2, s) \<Rightarrow> s' \<and> stk' = stk

goal (1 subgoal):
 1. cpred (c\<^sub>1 OR c\<^sub>2) (cfs ! 0) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
by (insert execl_last, auto simp: execl_all_def cpred_def Let_def)
[PROOF STATE]
proof (state)
this:
cpred (c\<^sub>1 OR c\<^sub>2) (cfs ! 0) (cfs ! (length cfs - Suc 0))

goal (1 subgoal):
 1. \<And>c1 c2 cfs. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); JMPND (size (ccomp c1) + 1) # ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>\<rbrakk> \<Longrightarrow> cpred (c1 OR c2) (cfs ! 0) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
cfs ! 1 = (size (ccomp c\<^sub>1) + 2, s, stk) \<Longrightarrow> cpred (c\<^sub>1 OR c\<^sub>2) (cfs ! 0) (cfs ! (length cfs - Suc 0))

goal (1 subgoal):
 1. \<And>c1 c2 cfs. \<lbrakk>\<And>cfs. ccomp c1 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c1 (cfs ! 0) (cfs ! (length cfs - Suc 0)); \<And>cfs. ccomp c2 \<Turnstile> cfs\<box> \<Longrightarrow> cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0)); JMPND (size (ccomp c1) + 1) # ccomp c1 @ JMP (size (ccomp c2)) # ccomp c2 \<Turnstile> cfs\<box>\<rbrakk> \<Longrightarrow> cpred (c1 OR c2) (cfs ! 0) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
cfs ! 1 = (1, s, stk) \<or> cfs ! 1 = (size (ccomp c\<^sub>1) + 2, s, stk)
cfs ! 1 = (1, s, stk) \<Longrightarrow> cpred (c\<^sub>1 OR c\<^sub>2) (cfs ! 0) (cfs ! (length cfs - Suc 0))
cfs ! 1 = (size (ccomp c\<^sub>1) + 2, s, stk) \<Longrightarrow> cpred (c\<^sub>1 OR c\<^sub>2) (cfs ! 0) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
show "cpred (c\<^sub>1 OR c\<^sub>2) (cfs ! 0) (cfs ! (length cfs - Suc 0))"
[PROOF STATE]
proof (prove)
using this:
cfs ! 1 = (1, s, stk) \<or> cfs ! 1 = (size (ccomp c\<^sub>1) + 2, s, stk)
cfs ! 1 = (1, s, stk) \<Longrightarrow> cpred (c\<^sub>1 OR c\<^sub>2) (cfs ! 0) (cfs ! (length cfs - Suc 0))
cfs ! 1 = (size (ccomp c\<^sub>1) + 2, s, stk) \<Longrightarrow> cpred (c\<^sub>1 OR c\<^sub>2) (cfs ! 0) (cfs ! (length cfs - Suc 0))

goal (1 subgoal):
 1. cpred (c\<^sub>1 OR c\<^sub>2) (cfs ! 0) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
cpred (c\<^sub>1 OR c\<^sub>2) (cfs ! 0) (cfs ! (length cfs - Suc 0))

goal:
No subgoals!
[PROOF STEP]
qed