[STATEMENT]
lemma while_correct [simplified, intro]:
 "\<lbrakk>bcomp (b, False, size (ccomp c) + 1) @ ccomp c @
    [JMP (- (size (bcomp (b, False, size (ccomp c) + 1) @ ccomp c) + 1))] \<Turnstile> cfs\<box>;
    \<And>cfs. ccomp c \<Turnstile> cfs\<box> \<Longrightarrow> cpred c (cfs ! 0) (cfs ! (length cfs - 1))\<rbrakk> \<Longrightarrow>
  cpred (WHILE b DO c) (cfs ! 0) (cfs ! (length cfs - Suc 0))"
  (is "\<lbrakk>?cb @ ?cc @ [JMP (- ?n)] \<Turnstile> _\<box>; \<And>_. _ \<Longrightarrow> _\<rbrakk> \<Longrightarrow> ?Q cfs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bcomp (b, False, size (ccomp c) + 1) @ ccomp c @ [JMP (- (size (bcomp (b, False, size (ccomp c) + 1) @ ccomp c) + 1))] \<Turnstile> cfs\<box>; \<And>cfs. ccomp c \<Turnstile> cfs\<box> \<Longrightarrow> cpred c (cfs ! 0) (cfs ! (length cfs - 1))\<rbrakk> \<Longrightarrow> cpred (WHILE b DO c) (cfs ! 0) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
proof (induction cfs rule: length_induct, frule bcomp_ccomp, auto)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>xs a ba. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> bcomp (b, False, size (ccomp c) + 1) @ ccomp c @ [JMP (- size (bcomp (b, False, size (ccomp c) + 1)) - size (ccomp c) - 1)] \<Turnstile> ys\<box> \<longrightarrow> cpred (WHILE b DO c) (ys ! 0) (ys ! (length ys - Suc 0)); bcomp (b, False, size (ccomp c) + 1) @ ccomp c @ [JMP (- size (bcomp (b, False, size (ccomp c) + 1)) - size (ccomp c) - 1)] \<Turnstile> xs\<box>; \<And>cfs. ccomp c \<Turnstile> cfs\<box> \<Longrightarrow> cpred c (cfs ! 0) (cfs ! (length cfs - Suc 0)); xs ! 0 = (0, a, ba); \<not> bval b a\<rbrakk> \<Longrightarrow> cpred (WHILE b DO c) (0, a, ba) (xs ! (length xs - Suc 0))
 2. \<And>xs a ba k aa. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> bcomp (b, False, size (ccomp c) + 1) @ ccomp c @ [JMP (- size (bcomp (b, False, size (ccomp c) + 1)) - size (ccomp c) - 1)] \<Turnstile> ys\<box> \<longrightarrow> cpred (WHILE b DO c) (ys ! 0) (ys ! (length ys - Suc 0)); bcomp (b, False, size (ccomp c) + 1) @ ccomp c @ [JMP (- size (bcomp (b, False, size (ccomp c) + 1)) - size (ccomp c) - 1)] \<Turnstile> xs\<box>; \<And>cfs. ccomp c \<Turnstile> cfs\<box> \<Longrightarrow> cpred c (cfs ! 0) (cfs ! (length cfs - Suc 0)); xs ! 0 = (0, a, ba); bval b a; k < length xs; xs ! k = (size (bcomp (b, False, size (ccomp c) + 1)) + size (ccomp c), aa, ba); (c, a) \<Rightarrow> aa\<rbrakk> \<Longrightarrow> cpred (WHILE b DO c) (0, a, ba) (xs ! (length xs - Suc 0))
[PROOF STEP]
fix cfs s stk
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>xs a ba. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> bcomp (b, False, size (ccomp c) + 1) @ ccomp c @ [JMP (- size (bcomp (b, False, size (ccomp c) + 1)) - size (ccomp c) - 1)] \<Turnstile> ys\<box> \<longrightarrow> cpred (WHILE b DO c) (ys ! 0) (ys ! (length ys - Suc 0)); bcomp (b, False, size (ccomp c) + 1) @ ccomp c @ [JMP (- size (bcomp (b, False, size (ccomp c) + 1)) - size (ccomp c) - 1)] \<Turnstile> xs\<box>; \<And>cfs. ccomp c \<Turnstile> cfs\<box> \<Longrightarrow> cpred c (cfs ! 0) (cfs ! (length cfs - Suc 0)); xs ! 0 = (0, a, ba); \<not> bval b a\<rbrakk> \<Longrightarrow> cpred (WHILE b DO c) (0, a, ba) (xs ! (length xs - Suc 0))
 2. \<And>xs a ba k aa. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> bcomp (b, False, size (ccomp c) + 1) @ ccomp c @ [JMP (- size (bcomp (b, False, size (ccomp c) + 1)) - size (ccomp c) - 1)] \<Turnstile> ys\<box> \<longrightarrow> cpred (WHILE b DO c) (ys ! 0) (ys ! (length ys - Suc 0)); bcomp (b, False, size (ccomp c) + 1) @ ccomp c @ [JMP (- size (bcomp (b, False, size (ccomp c) + 1)) - size (ccomp c) - 1)] \<Turnstile> xs\<box>; \<And>cfs. ccomp c \<Turnstile> cfs\<box> \<Longrightarrow> cpred c (cfs ! 0) (cfs ! (length cfs - Suc 0)); xs ! 0 = (0, a, ba); bval b a; k < length xs; xs ! k = (size (bcomp (b, False, size (ccomp c) + 1)) + size (ccomp c), aa, ba); (c, a) \<Rightarrow> aa\<rbrakk> \<Longrightarrow> cpred (WHILE b DO c) (0, a, ba) (xs ! (length xs - Suc 0))
[PROOF STEP]
assume A: "?cb @ ?cc @ [JMP (- size ?cb - size ?cc - 1)] \<Turnstile> cfs\<box>"
[PROOF STATE]
proof (state)
this:
bcomp (b, False, size (ccomp c) + 1) @ ccomp c @ [JMP (- size (bcomp (b, False, size (ccomp c) + 1)) - size (ccomp c) - 1)] \<Turnstile> cfs\<box>

goal (2 subgoals):
 1. \<And>xs a ba. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> bcomp (b, False, size (ccomp c) + 1) @ ccomp c @ [JMP (- size (bcomp (b, False, size (ccomp c) + 1)) - size (ccomp c) - 1)] \<Turnstile> ys\<box> \<longrightarrow> cpred (WHILE b DO c) (ys ! 0) (ys ! (length ys - Suc 0)); bcomp (b, False, size (ccomp c) + 1) @ ccomp c @ [JMP (- size (bcomp (b, False, size (ccomp c) + 1)) - size (ccomp c) - 1)] \<Turnstile> xs\<box>; \<And>cfs. ccomp c \<Turnstile> cfs\<box> \<Longrightarrow> cpred c (cfs ! 0) (cfs ! (length cfs - Suc 0)); xs ! 0 = (0, a, ba); \<not> bval b a\<rbrakk> \<Longrightarrow> cpred (WHILE b DO c) (0, a, ba) (xs ! (length xs - Suc 0))
 2. \<And>xs a ba k aa. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> bcomp (b, False, size (ccomp c) + 1) @ ccomp c @ [JMP (- size (bcomp (b, False, size (ccomp c) + 1)) - size (ccomp c) - 1)] \<Turnstile> ys\<box> \<longrightarrow> cpred (WHILE b DO c) (ys ! 0) (ys ! (length ys - Suc 0)); bcomp (b, False, size (ccomp c) + 1) @ ccomp c @ [JMP (- size (bcomp (b, False, size (ccomp c) + 1)) - size (ccomp c) - 1)] \<Turnstile> xs\<box>; \<And>cfs. ccomp c \<Turnstile> cfs\<box> \<Longrightarrow> cpred c (cfs ! 0) (cfs ! (length cfs - Suc 0)); xs ! 0 = (0, a, ba); bval b a; k < length xs; xs ! k = (size (bcomp (b, False, size (ccomp c) + 1)) + size (ccomp c), aa, ba); (c, a) \<Rightarrow> aa\<rbrakk> \<Longrightarrow> cpred (WHILE b DO c) (0, a, ba) (xs ! (length xs - Suc 0))
[PROOF STEP]
hence "\<exists>k < length cfs. bpred (b, False, size (ccomp c) + 1)
    (off [] (cfs ! 0)) (off [] (cfs ! k))"
[PROOF STATE]
proof (prove)
using this:
bcomp (b, False, size (ccomp c) + 1) @ ccomp c @ [JMP (- size (bcomp (b, False, size (ccomp c) + 1)) - size (ccomp c) - 1)] \<Turnstile> cfs\<box>

goal (1 subgoal):
 1. \<exists>k<length cfs. bpred (b, False, size (ccomp c) + 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) + 1) (off [] (cfs ! 0)) (off [] (cfs ! k))

goal (2 subgoals):
 1. \<And>xs a ba. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> bcomp (b, False, size (ccomp c) + 1) @ ccomp c @ [JMP (- size (bcomp (b, False, size (ccomp c) + 1)) - size (ccomp c) - 1)] \<Turnstile> ys\<box> \<longrightarrow> cpred (WHILE b DO c) (ys ! 0) (ys ! (length ys - Suc 0)); bcomp (b, False, size (ccomp c) + 1) @ ccomp c @ [JMP (- size (bcomp (b, False, size (ccomp c) + 1)) - size (ccomp c) - 1)] \<Turnstile> xs\<box>; \<And>cfs. ccomp c \<Turnstile> cfs\<box> \<Longrightarrow> cpred c (cfs ! 0) (cfs ! (length cfs - Suc 0)); xs ! 0 = (0, a, ba); \<not> bval b a\<rbrakk> \<Longrightarrow> cpred (WHILE b DO c) (0, a, ba) (xs ! (length xs - Suc 0))
 2. \<And>xs a ba k aa. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> bcomp (b, False, size (ccomp c) + 1) @ ccomp c @ [JMP (- size (bcomp (b, False, size (ccomp c) + 1)) - size (ccomp c) - 1)] \<Turnstile> ys\<box> \<longrightarrow> cpred (WHILE b DO c) (ys ! 0) (ys ! (length ys - Suc 0)); bcomp (b, False, size (ccomp c) + 1) @ ccomp c @ [JMP (- size (bcomp (b, False, size (ccomp c) + 1)) - size (ccomp c) - 1)] \<Turnstile> xs\<box>; \<And>cfs. ccomp c \<Turnstile> cfs\<box> \<Longrightarrow> cpred c (cfs ! 0) (cfs ! (length cfs - Suc 0)); xs ! 0 = (0, a, ba); bval b a; k < length xs; xs ! k = (size (bcomp (b, False, size (ccomp c) + 1)) + size (ccomp c), aa, ba); (c, a) \<Rightarrow> aa\<rbrakk> \<Longrightarrow> cpred (WHILE b DO c) (0, a, ba) (xs ! (length xs - Suc 0))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<exists>k<length cfs. bpred (b, False, size (ccomp c) + 1) (off [] (cfs ! 0)) (off [] (cfs ! k))

goal (2 subgoals):
 1. \<And>xs a ba. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> bcomp (b, False, size (ccomp c) + 1) @ ccomp c @ [JMP (- size (bcomp (b, False, size (ccomp c) + 1)) - size (ccomp c) - 1)] \<Turnstile> ys\<box> \<longrightarrow> cpred (WHILE b DO c) (ys ! 0) (ys ! (length ys - Suc 0)); bcomp (b, False, size (ccomp c) + 1) @ ccomp c @ [JMP (- size (bcomp (b, False, size (ccomp c) + 1)) - size (ccomp c) - 1)] \<Turnstile> xs\<box>; \<And>cfs. ccomp c \<Turnstile> cfs\<box> \<Longrightarrow> cpred c (cfs ! 0) (cfs ! (length cfs - Suc 0)); xs ! 0 = (0, a, ba); \<not> bval b a\<rbrakk> \<Longrightarrow> cpred (WHILE b DO c) (0, a, ba) (xs ! (length xs - Suc 0))
 2. \<And>xs a ba k aa. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> bcomp (b, False, size (ccomp c) + 1) @ ccomp c @ [JMP (- size (bcomp (b, False, size (ccomp c) + 1)) - size (ccomp c) - 1)] \<Turnstile> ys\<box> \<longrightarrow> cpred (WHILE b DO c) (ys ! 0) (ys ! (length ys - Suc 0)); bcomp (b, False, size (ccomp c) + 1) @ ccomp c @ [JMP (- size (bcomp (b, False, size (ccomp c) + 1)) - size (ccomp c) - 1)] \<Turnstile> xs\<box>; \<And>cfs. ccomp c \<Turnstile> cfs\<box> \<Longrightarrow> cpred c (cfs ! 0) (cfs ! (length cfs - Suc 0)); xs ! 0 = (0, a, ba); bval b a; k < length xs; xs ! k = (size (bcomp (b, False, size (ccomp c) + 1)) + size (ccomp c), aa, ba); (c, a) \<Rightarrow> aa\<rbrakk> \<Longrightarrow> cpred (WHILE b DO c) (0, a, ba) (xs ! (length xs - 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 (2 subgoals):
 1. \<And>xs a ba. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> bcomp (b, False, size (ccomp c) + 1) @ ccomp c @ [JMP (- size (bcomp (b, False, size (ccomp c) + 1)) - size (ccomp c) - 1)] \<Turnstile> ys\<box> \<longrightarrow> cpred (WHILE b DO c) (ys ! 0) (ys ! (length ys - Suc 0)); bcomp (b, False, size (ccomp c) + 1) @ ccomp c @ [JMP (- size (bcomp (b, False, size (ccomp c) + 1)) - size (ccomp c) - 1)] \<Turnstile> xs\<box>; \<And>cfs. ccomp c \<Turnstile> cfs\<box> \<Longrightarrow> cpred c (cfs ! 0) (cfs ! (length cfs - Suc 0)); xs ! 0 = (0, a, ba); \<not> bval b a\<rbrakk> \<Longrightarrow> cpred (WHILE b DO c) (0, a, ba) (xs ! (length xs - Suc 0))
 2. \<And>xs a ba k aa. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> bcomp (b, False, size (ccomp c) + 1) @ ccomp c @ [JMP (- size (bcomp (b, False, size (ccomp c) + 1)) - size (ccomp c) - 1)] \<Turnstile> ys\<box> \<longrightarrow> cpred (WHILE b DO c) (ys ! 0) (ys ! (length ys - Suc 0)); bcomp (b, False, size (ccomp c) + 1) @ ccomp c @ [JMP (- size (bcomp (b, False, size (ccomp c) + 1)) - size (ccomp c) - 1)] \<Turnstile> xs\<box>; \<And>cfs. ccomp c \<Turnstile> cfs\<box> \<Longrightarrow> cpred c (cfs ! 0) (cfs ! (length cfs - Suc 0)); xs ! 0 = (0, a, ba); bval b a; k < length xs; xs ! k = (size (bcomp (b, False, size (ccomp c) + 1)) + size (ccomp c), aa, ba); (c, a) \<Rightarrow> aa\<rbrakk> \<Longrightarrow> cpred (WHILE b DO c) (0, a, ba) (xs ! (length xs - Suc 0))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<exists>k<length cfs. bpred (b, False, size (ccomp c) + 1) (off [] (cfs ! 0)) (off [] (cfs ! k))
\<not> bval b s
cfs ! 0 = (0, s, stk)
[PROOF STEP]
obtain k where "k < length cfs" and "cfs ! k = (?n, s, stk)"
[PROOF STATE]
proof (prove)
using this:
\<exists>k<length cfs. bpred (b, False, size (ccomp c) + 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) + 1) @ ccomp c) + 1, s, stk)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: bpred_def)
[PROOF STATE]
proof (state)
this:
k < length cfs
cfs ! k = (size (bcomp (b, False, size (ccomp c) + 1) @ ccomp c) + 1, s, stk)

goal (2 subgoals):
 1. \<And>xs a ba. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> bcomp (b, False, size (ccomp c) + 1) @ ccomp c @ [JMP (- size (bcomp (b, False, size (ccomp c) + 1)) - size (ccomp c) - 1)] \<Turnstile> ys\<box> \<longrightarrow> cpred (WHILE b DO c) (ys ! 0) (ys ! (length ys - Suc 0)); bcomp (b, False, size (ccomp c) + 1) @ ccomp c @ [JMP (- size (bcomp (b, False, size (ccomp c) + 1)) - size (ccomp c) - 1)] \<Turnstile> xs\<box>; \<And>cfs. ccomp c \<Turnstile> cfs\<box> \<Longrightarrow> cpred c (cfs ! 0) (cfs ! (length cfs - Suc 0)); xs ! 0 = (0, a, ba); \<not> bval b a\<rbrakk> \<Longrightarrow> cpred (WHILE b DO c) (0, a, ba) (xs ! (length xs - Suc 0))
 2. \<And>xs a ba k aa. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> bcomp (b, False, size (ccomp c) + 1) @ ccomp c @ [JMP (- size (bcomp (b, False, size (ccomp c) + 1)) - size (ccomp c) - 1)] \<Turnstile> ys\<box> \<longrightarrow> cpred (WHILE b DO c) (ys ! 0) (ys ! (length ys - Suc 0)); bcomp (b, False, size (ccomp c) + 1) @ ccomp c @ [JMP (- size (bcomp (b, False, size (ccomp c) + 1)) - size (ccomp c) - 1)] \<Turnstile> xs\<box>; \<And>cfs. ccomp c \<Turnstile> cfs\<box> \<Longrightarrow> cpred c (cfs ! 0) (cfs ! (length cfs - Suc 0)); xs ! 0 = (0, a, ba); bval b a; k < length xs; xs ! k = (size (bcomp (b, False, size (ccomp c) + 1)) + size (ccomp c), aa, ba); (c, a) \<Rightarrow> aa\<rbrakk> \<Longrightarrow> cpred (WHILE b DO c) (0, a, ba) (xs ! (length xs - Suc 0))
[PROOF STEP]
thus "cpred (WHILE b DO c) (0, s, stk) (cfs ! (length cfs - Suc 0))"
[PROOF STATE]
proof (prove)
using this:
k < length cfs
cfs ! k = (size (bcomp (b, False, size (ccomp c) + 1) @ ccomp c) + 1, s, stk)

goal (1 subgoal):
 1. cpred (WHILE b DO c) (0, s, stk) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
using A and B
[PROOF STATE]
proof (prove)
using this:
k < length cfs
cfs ! k = (size (bcomp (b, False, size (ccomp c) + 1) @ ccomp c) + 1, s, stk)
bcomp (b, False, size (ccomp c) + 1) @ ccomp c @ [JMP (- size (bcomp (b, False, size (ccomp c) + 1)) - size (ccomp c) - 1)] \<Turnstile> cfs\<box>
\<not> bval b s

goal (1 subgoal):
 1. cpred (WHILE b DO c) (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 (WHILE b DO c) (0, s, stk) (cfs ! (length cfs - Suc 0))

goal (1 subgoal):
 1. \<And>xs a ba k aa. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> bcomp (b, False, size (ccomp c) + 1) @ ccomp c @ [JMP (- size (bcomp (b, False, size (ccomp c) + 1)) - size (ccomp c) - 1)] \<Turnstile> ys\<box> \<longrightarrow> cpred (WHILE b DO c) (ys ! 0) (ys ! (length ys - Suc 0)); bcomp (b, False, size (ccomp c) + 1) @ ccomp c @ [JMP (- size (bcomp (b, False, size (ccomp c) + 1)) - size (ccomp c) - 1)] \<Turnstile> xs\<box>; \<And>cfs. ccomp c \<Turnstile> cfs\<box> \<Longrightarrow> cpred c (cfs ! 0) (cfs ! (length cfs - Suc 0)); xs ! 0 = (0, a, ba); bval b a; k < length xs; xs ! k = (size (bcomp (b, False, size (ccomp c) + 1)) + size (ccomp c), aa, ba); (c, a) \<Rightarrow> aa\<rbrakk> \<Longrightarrow> cpred (WHILE b DO c) (0, a, ba) (xs ! (length xs - Suc 0))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xs a ba k aa. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> bcomp (b, False, size (ccomp c) + 1) @ ccomp c @ [JMP (- size (bcomp (b, False, size (ccomp c) + 1)) - size (ccomp c) - 1)] \<Turnstile> ys\<box> \<longrightarrow> cpred (WHILE b DO c) (ys ! 0) (ys ! (length ys - Suc 0)); bcomp (b, False, size (ccomp c) + 1) @ ccomp c @ [JMP (- size (bcomp (b, False, size (ccomp c) + 1)) - size (ccomp c) - 1)] \<Turnstile> xs\<box>; \<And>cfs. ccomp c \<Turnstile> cfs\<box> \<Longrightarrow> cpred c (cfs ! 0) (cfs ! (length cfs - Suc 0)); xs ! 0 = (0, a, ba); bval b a; k < length xs; xs ! k = (size (bcomp (b, False, size (ccomp c) + 1)) + size (ccomp c), aa, ba); (c, a) \<Rightarrow> aa\<rbrakk> \<Longrightarrow> cpred (WHILE b DO c) (0, a, ba) (xs ! (length xs - Suc 0))
[PROOF STEP]
fix cfs s s' stk k
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xs a ba k aa. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> bcomp (b, False, size (ccomp c) + 1) @ ccomp c @ [JMP (- size (bcomp (b, False, size (ccomp c) + 1)) - size (ccomp c) - 1)] \<Turnstile> ys\<box> \<longrightarrow> cpred (WHILE b DO c) (ys ! 0) (ys ! (length ys - Suc 0)); bcomp (b, False, size (ccomp c) + 1) @ ccomp c @ [JMP (- size (bcomp (b, False, size (ccomp c) + 1)) - size (ccomp c) - 1)] \<Turnstile> xs\<box>; \<And>cfs. ccomp c \<Turnstile> cfs\<box> \<Longrightarrow> cpred c (cfs ! 0) (cfs ! (length cfs - Suc 0)); xs ! 0 = (0, a, ba); bval b a; k < length xs; xs ! k = (size (bcomp (b, False, size (ccomp c) + 1)) + size (ccomp c), aa, ba); (c, a) \<Rightarrow> aa\<rbrakk> \<Longrightarrow> cpred (WHILE b DO c) (0, a, ba) (xs ! (length xs - Suc 0))
[PROOF STEP]
assume A: "?cb @ ?cc @ [JMP (- size ?cb - size ?cc - 1)] \<Turnstile> cfs\<box>"
    (is "?P \<Turnstile> _\<box>")
[PROOF STATE]
proof (state)
this:
bcomp (b, False, size (ccomp c) + 1) @ ccomp c @ [JMP (- size (bcomp (b, False, size (ccomp c) + 1)) - size (ccomp c) - 1)] \<Turnstile> cfs\<box>

goal (1 subgoal):
 1. \<And>xs a ba k aa. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> bcomp (b, False, size (ccomp c) + 1) @ ccomp c @ [JMP (- size (bcomp (b, False, size (ccomp c) + 1)) - size (ccomp c) - 1)] \<Turnstile> ys\<box> \<longrightarrow> cpred (WHILE b DO c) (ys ! 0) (ys ! (length ys - Suc 0)); bcomp (b, False, size (ccomp c) + 1) @ ccomp c @ [JMP (- size (bcomp (b, False, size (ccomp c) + 1)) - size (ccomp c) - 1)] \<Turnstile> xs\<box>; \<And>cfs. ccomp c \<Turnstile> cfs\<box> \<Longrightarrow> cpred c (cfs ! 0) (cfs ! (length cfs - Suc 0)); xs ! 0 = (0, a, ba); bval b a; k < length xs; xs ! k = (size (bcomp (b, False, size (ccomp c) + 1)) + size (ccomp c), aa, ba); (c, a) \<Rightarrow> aa\<rbrakk> \<Longrightarrow> cpred (WHILE b DO c) (0, a, ba) (xs ! (length xs - Suc 0))
[PROOF STEP]
assume B: "k < length cfs" and "cfs ! k = (size ?cb + size ?cc, s', stk)"
[PROOF STATE]
proof (state)
this:
k < length cfs
cfs ! k = (size (bcomp (b, False, size (ccomp c) + 1)) + size (ccomp c), s', stk)

goal (1 subgoal):
 1. \<And>xs a ba k aa. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> bcomp (b, False, size (ccomp c) + 1) @ ccomp c @ [JMP (- size (bcomp (b, False, size (ccomp c) + 1)) - size (ccomp c) - 1)] \<Turnstile> ys\<box> \<longrightarrow> cpred (WHILE b DO c) (ys ! 0) (ys ! (length ys - Suc 0)); bcomp (b, False, size (ccomp c) + 1) @ ccomp c @ [JMP (- size (bcomp (b, False, size (ccomp c) + 1)) - size (ccomp c) - 1)] \<Turnstile> xs\<box>; \<And>cfs. ccomp c \<Turnstile> cfs\<box> \<Longrightarrow> cpred c (cfs ! 0) (cfs ! (length cfs - Suc 0)); xs ! 0 = (0, a, ba); bval b a; k < length xs; xs ! k = (size (bcomp (b, False, size (ccomp c) + 1)) + size (ccomp c), aa, ba); (c, a) \<Rightarrow> aa\<rbrakk> \<Longrightarrow> cpred (WHILE b DO c) (0, a, ba) (xs ! (length xs - Suc 0))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
k < length cfs
cfs ! k = (size (bcomp (b, False, size (ccomp c) + 1)) + size (ccomp c), s', stk)

goal (1 subgoal):
 1. \<And>xs a ba k aa. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> bcomp (b, False, size (ccomp c) + 1) @ ccomp c @ [JMP (- size (bcomp (b, False, size (ccomp c) + 1)) - size (ccomp c) - 1)] \<Turnstile> ys\<box> \<longrightarrow> cpred (WHILE b DO c) (ys ! 0) (ys ! (length ys - Suc 0)); bcomp (b, False, size (ccomp c) + 1) @ ccomp c @ [JMP (- size (bcomp (b, False, size (ccomp c) + 1)) - size (ccomp c) - 1)] \<Turnstile> xs\<box>; \<And>cfs. ccomp c \<Turnstile> cfs\<box> \<Longrightarrow> cpred c (cfs ! 0) (cfs ! (length cfs - Suc 0)); xs ! 0 = (0, a, ba); bval b a; k < length xs; xs ! k = (size (bcomp (b, False, size (ccomp c) + 1)) + size (ccomp c), aa, ba); (c, a) \<Rightarrow> aa\<rbrakk> \<Longrightarrow> cpred (WHILE b DO c) (0, a, ba) (xs ! (length xs - Suc 0))
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
k < length cfs
cfs ! k = (size (bcomp (b, False, size (ccomp c) + 1)) + size (ccomp c), s', stk)
[PROOF STEP]
have C: "k \<noteq> length cfs - 1"
[PROOF STATE]
proof (prove)
using this:
k < length cfs
cfs ! k = (size (bcomp (b, False, size (ccomp c) + 1)) + size (ccomp c), s', stk)

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

goal (1 subgoal):
 1. k \<noteq> length cfs - 1
[PROOF STEP]
by (rule_tac notI, simp add: execl_all_def)
[PROOF STATE]
proof (state)
this:
k \<noteq> length cfs - 1

goal (1 subgoal):
 1. \<And>xs a ba k aa. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> bcomp (b, False, size (ccomp c) + 1) @ ccomp c @ [JMP (- size (bcomp (b, False, size (ccomp c) + 1)) - size (ccomp c) - 1)] \<Turnstile> ys\<box> \<longrightarrow> cpred (WHILE b DO c) (ys ! 0) (ys ! (length ys - Suc 0)); bcomp (b, False, size (ccomp c) + 1) @ ccomp c @ [JMP (- size (bcomp (b, False, size (ccomp c) + 1)) - size (ccomp c) - 1)] \<Turnstile> xs\<box>; \<And>cfs. ccomp c \<Turnstile> cfs\<box> \<Longrightarrow> cpred c (cfs ! 0) (cfs ! (length cfs - Suc 0)); xs ! 0 = (0, a, ba); bval b a; k < length xs; xs ! k = (size (bcomp (b, False, size (ccomp c) + 1)) + size (ccomp c), aa, ba); (c, a) \<Rightarrow> aa\<rbrakk> \<Longrightarrow> cpred (WHILE b DO c) (0, a, ba) (xs ! (length xs - Suc 0))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
k < length cfs
cfs ! k = (size (bcomp (b, False, size (ccomp c) + 1)) + size (ccomp c), s', stk)
k \<noteq> length cfs - 1
[PROOF STEP]
have D: "cfs ! Suc k = (0, s', stk)"
[PROOF STATE]
proof (prove)
using this:
k < length cfs
cfs ! k = (size (bcomp (b, False, size (ccomp c) + 1)) + size (ccomp c), s', stk)
k \<noteq> length cfs - 1

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

goal (1 subgoal):
 1. cfs ! Suc k = (0, s', stk)
[PROOF STEP]
by (insert execl_next [of ?P cfs k], auto simp: execl_all_def)
[PROOF STATE]
proof (state)
this:
cfs ! Suc k = (0, s', stk)

goal (1 subgoal):
 1. \<And>xs a ba k aa. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> bcomp (b, False, size (ccomp c) + 1) @ ccomp c @ [JMP (- size (bcomp (b, False, size (ccomp c) + 1)) - size (ccomp c) - 1)] \<Turnstile> ys\<box> \<longrightarrow> cpred (WHILE b DO c) (ys ! 0) (ys ! (length ys - Suc 0)); bcomp (b, False, size (ccomp c) + 1) @ ccomp c @ [JMP (- size (bcomp (b, False, size (ccomp c) + 1)) - size (ccomp c) - 1)] \<Turnstile> xs\<box>; \<And>cfs. ccomp c \<Turnstile> cfs\<box> \<Longrightarrow> cpred c (cfs ! 0) (cfs ! (length cfs - Suc 0)); xs ! 0 = (0, a, ba); bval b a; k < length xs; xs ! k = (size (bcomp (b, False, size (ccomp c) + 1)) + size (ccomp c), aa, ba); (c, a) \<Rightarrow> aa\<rbrakk> \<Longrightarrow> cpred (WHILE b DO c) (0, a, ba) (xs ! (length xs - Suc 0))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
cfs ! Suc k = (0, s', stk)

goal (1 subgoal):
 1. \<And>xs a ba k aa. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> bcomp (b, False, size (ccomp c) + 1) @ ccomp c @ [JMP (- size (bcomp (b, False, size (ccomp c) + 1)) - size (ccomp c) - 1)] \<Turnstile> ys\<box> \<longrightarrow> cpred (WHILE b DO c) (ys ! 0) (ys ! (length ys - Suc 0)); bcomp (b, False, size (ccomp c) + 1) @ ccomp c @ [JMP (- size (bcomp (b, False, size (ccomp c) + 1)) - size (ccomp c) - 1)] \<Turnstile> xs\<box>; \<And>cfs. ccomp c \<Turnstile> cfs\<box> \<Longrightarrow> cpred c (cfs ! 0) (cfs ! (length cfs - Suc 0)); xs ! 0 = (0, a, ba); bval b a; k < length xs; xs ! k = (size (bcomp (b, False, size (ccomp c) + 1)) + size (ccomp c), aa, ba); (c, a) \<Rightarrow> aa\<rbrakk> \<Longrightarrow> cpred (WHILE b DO c) (0, a, ba) (xs ! (length xs - Suc 0))
[PROOF STEP]
have E: "Suc k + (length (drop (Suc k) cfs) - 1) = length cfs - 1"
    (is "Suc k + (length ?cfs - 1) = _")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc k + (length (drop (Suc k) cfs) - 1) = length cfs - 1
[PROOF STEP]
using B and C
[PROOF STATE]
proof (prove)
using this:
k < length cfs
k \<noteq> length cfs - 1

goal (1 subgoal):
 1. Suc k + (length (drop (Suc k) cfs) - 1) = length cfs - 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Suc k + (length (drop (Suc k) cfs) - 1) = length cfs - 1

goal (1 subgoal):
 1. \<And>xs a ba k aa. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> bcomp (b, False, size (ccomp c) + 1) @ ccomp c @ [JMP (- size (bcomp (b, False, size (ccomp c) + 1)) - size (ccomp c) - 1)] \<Turnstile> ys\<box> \<longrightarrow> cpred (WHILE b DO c) (ys ! 0) (ys ! (length ys - Suc 0)); bcomp (b, False, size (ccomp c) + 1) @ ccomp c @ [JMP (- size (bcomp (b, False, size (ccomp c) + 1)) - size (ccomp c) - 1)] \<Turnstile> xs\<box>; \<And>cfs. ccomp c \<Turnstile> cfs\<box> \<Longrightarrow> cpred c (cfs ! 0) (cfs ! (length cfs - Suc 0)); xs ! 0 = (0, a, ba); bval b a; k < length xs; xs ! k = (size (bcomp (b, False, size (ccomp c) + 1)) + size (ccomp c), aa, ba); (c, a) \<Rightarrow> aa\<rbrakk> \<Longrightarrow> cpred (WHILE b DO c) (0, a, ba) (xs ! (length xs - Suc 0))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
cfs ! Suc k = (0, s', stk)
Suc k + (length (drop (Suc k) cfs) - 1) = length cfs - 1
[PROOF STEP]
have "?P \<Turnstile> ?cfs\<box>"
[PROOF STATE]
proof (prove)
using this:
cfs ! Suc k = (0, s', stk)
Suc k + (length (drop (Suc k) cfs) - 1) = length cfs - 1

goal (1 subgoal):
 1. bcomp (b, False, size (ccomp c) + 1) @ ccomp c @ [JMP (- size (bcomp (b, False, size (ccomp c) + 1)) - size (ccomp c) - 1)] \<Turnstile> drop (Suc k) cfs\<box>
[PROOF STEP]
using A and B and C
[PROOF STATE]
proof (prove)
using this:
cfs ! Suc k = (0, s', stk)
Suc k + (length (drop (Suc k) cfs) - 1) = length cfs - 1
bcomp (b, False, size (ccomp c) + 1) @ ccomp c @ [JMP (- size (bcomp (b, False, size (ccomp c) + 1)) - size (ccomp c) - 1)] \<Turnstile> cfs\<box>
k < length cfs
k \<noteq> length cfs - 1

goal (1 subgoal):
 1. bcomp (b, False, size (ccomp c) + 1) @ ccomp c @ [JMP (- size (bcomp (b, False, size (ccomp c) + 1)) - size (ccomp c) - 1)] \<Turnstile> drop (Suc k) cfs\<box>
[PROOF STEP]
by (auto simp: execl_all_def intro: execl_drop)
[PROOF STATE]
proof (state)
this:
bcomp (b, False, size (ccomp c) + 1) @ ccomp c @ [JMP (- size (bcomp (b, False, size (ccomp c) + 1)) - size (ccomp c) - 1)] \<Turnstile> drop (Suc k) cfs\<box>

goal (1 subgoal):
 1. \<And>xs a ba k aa. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> bcomp (b, False, size (ccomp c) + 1) @ ccomp c @ [JMP (- size (bcomp (b, False, size (ccomp c) + 1)) - size (ccomp c) - 1)] \<Turnstile> ys\<box> \<longrightarrow> cpred (WHILE b DO c) (ys ! 0) (ys ! (length ys - Suc 0)); bcomp (b, False, size (ccomp c) + 1) @ ccomp c @ [JMP (- size (bcomp (b, False, size (ccomp c) + 1)) - size (ccomp c) - 1)] \<Turnstile> xs\<box>; \<And>cfs. ccomp c \<Turnstile> cfs\<box> \<Longrightarrow> cpred c (cfs ! 0) (cfs ! (length cfs - Suc 0)); xs ! 0 = (0, a, ba); bval b a; k < length xs; xs ! k = (size (bcomp (b, False, size (ccomp c) + 1)) + size (ccomp c), aa, ba); (c, a) \<Rightarrow> aa\<rbrakk> \<Longrightarrow> cpred (WHILE b DO c) (0, a, ba) (xs ! (length xs - Suc 0))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
bcomp (b, False, size (ccomp c) + 1) @ ccomp c @ [JMP (- size (bcomp (b, False, size (ccomp c) + 1)) - size (ccomp c) - 1)] \<Turnstile> drop (Suc k) cfs\<box>

goal (1 subgoal):
 1. \<And>xs a ba k aa. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> bcomp (b, False, size (ccomp c) + 1) @ ccomp c @ [JMP (- size (bcomp (b, False, size (ccomp c) + 1)) - size (ccomp c) - 1)] \<Turnstile> ys\<box> \<longrightarrow> cpred (WHILE b DO c) (ys ! 0) (ys ! (length ys - Suc 0)); bcomp (b, False, size (ccomp c) + 1) @ ccomp c @ [JMP (- size (bcomp (b, False, size (ccomp c) + 1)) - size (ccomp c) - 1)] \<Turnstile> xs\<box>; \<And>cfs. ccomp c \<Turnstile> cfs\<box> \<Longrightarrow> cpred c (cfs ! 0) (cfs ! (length cfs - Suc 0)); xs ! 0 = (0, a, ba); bval b a; k < length xs; xs ! k = (size (bcomp (b, False, size (ccomp c) + 1)) + size (ccomp c), aa, ba); (c, a) \<Rightarrow> aa\<rbrakk> \<Longrightarrow> cpred (WHILE b DO c) (0, a, ba) (xs ! (length xs - Suc 0))
[PROOF STEP]
assume "\<forall>cfs'. length cfs' < length cfs \<longrightarrow> ?P \<Turnstile> cfs'\<box> \<longrightarrow> ?Q cfs'"
[PROOF STATE]
proof (state)
this:
\<forall>cfs'. length cfs' < length cfs \<longrightarrow> bcomp (b, False, size (ccomp c) + 1) @ ccomp c @ [JMP (- size (bcomp (b, False, size (ccomp c) + 1)) - size (ccomp c) - 1)] \<Turnstile> cfs'\<box> \<longrightarrow> cpred (WHILE b DO c) (cfs' ! 0) (cfs' ! (length cfs' - Suc 0))

goal (1 subgoal):
 1. \<And>xs a ba k aa. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> bcomp (b, False, size (ccomp c) + 1) @ ccomp c @ [JMP (- size (bcomp (b, False, size (ccomp c) + 1)) - size (ccomp c) - 1)] \<Turnstile> ys\<box> \<longrightarrow> cpred (WHILE b DO c) (ys ! 0) (ys ! (length ys - Suc 0)); bcomp (b, False, size (ccomp c) + 1) @ ccomp c @ [JMP (- size (bcomp (b, False, size (ccomp c) + 1)) - size (ccomp c) - 1)] \<Turnstile> xs\<box>; \<And>cfs. ccomp c \<Turnstile> cfs\<box> \<Longrightarrow> cpred c (cfs ! 0) (cfs ! (length cfs - Suc 0)); xs ! 0 = (0, a, ba); bval b a; k < length xs; xs ! k = (size (bcomp (b, False, size (ccomp c) + 1)) + size (ccomp c), aa, ba); (c, a) \<Rightarrow> aa\<rbrakk> \<Longrightarrow> cpred (WHILE b DO c) (0, a, ba) (xs ! (length xs - Suc 0))
[PROOF STEP]
hence "length ?cfs < length cfs \<longrightarrow> ?P \<Turnstile> ?cfs\<box> \<longrightarrow> ?Q ?cfs"
[PROOF STATE]
proof (prove)
using this:
\<forall>cfs'. length cfs' < length cfs \<longrightarrow> bcomp (b, False, size (ccomp c) + 1) @ ccomp c @ [JMP (- size (bcomp (b, False, size (ccomp c) + 1)) - size (ccomp c) - 1)] \<Turnstile> cfs'\<box> \<longrightarrow> cpred (WHILE b DO c) (cfs' ! 0) (cfs' ! (length cfs' - Suc 0))

goal (1 subgoal):
 1. length (drop (Suc k) cfs) < length cfs \<longrightarrow> bcomp (b, False, size (ccomp c) + 1) @ ccomp c @ [JMP (- size (bcomp (b, False, size (ccomp c) + 1)) - size (ccomp c) - 1)] \<Turnstile> drop (Suc k) cfs\<box> \<longrightarrow> cpred (WHILE b DO c) (drop (Suc k) cfs ! 0) (drop (Suc k) cfs ! (length (drop (Suc k) cfs) - Suc 0))
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
length (drop (Suc k) cfs) < length cfs \<longrightarrow> bcomp (b, False, size (ccomp c) + 1) @ ccomp c @ [JMP (- size (bcomp (b, False, size (ccomp c) + 1)) - size (ccomp c) - 1)] \<Turnstile> drop (Suc k) cfs\<box> \<longrightarrow> cpred (WHILE b DO c) (drop (Suc k) cfs ! 0) (drop (Suc k) cfs ! (length (drop (Suc k) cfs) - Suc 0))

goal (1 subgoal):
 1. \<And>xs a ba k aa. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> bcomp (b, False, size (ccomp c) + 1) @ ccomp c @ [JMP (- size (bcomp (b, False, size (ccomp c) + 1)) - size (ccomp c) - 1)] \<Turnstile> ys\<box> \<longrightarrow> cpred (WHILE b DO c) (ys ! 0) (ys ! (length ys - Suc 0)); bcomp (b, False, size (ccomp c) + 1) @ ccomp c @ [JMP (- size (bcomp (b, False, size (ccomp c) + 1)) - size (ccomp c) - 1)] \<Turnstile> xs\<box>; \<And>cfs. ccomp c \<Turnstile> cfs\<box> \<Longrightarrow> cpred c (cfs ! 0) (cfs ! (length cfs - Suc 0)); xs ! 0 = (0, a, ba); bval b a; k < length xs; xs ! k = (size (bcomp (b, False, size (ccomp c) + 1)) + size (ccomp c), aa, ba); (c, a) \<Rightarrow> aa\<rbrakk> \<Longrightarrow> cpred (WHILE b DO c) (0, a, ba) (xs ! (length xs - Suc 0))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
bcomp (b, False, size (ccomp c) + 1) @ ccomp c @ [JMP (- size (bcomp (b, False, size (ccomp c) + 1)) - size (ccomp c) - 1)] \<Turnstile> drop (Suc k) cfs\<box>
length (drop (Suc k) cfs) < length cfs \<longrightarrow> bcomp (b, False, size (ccomp c) + 1) @ ccomp c @ [JMP (- size (bcomp (b, False, size (ccomp c) + 1)) - size (ccomp c) - 1)] \<Turnstile> drop (Suc k) cfs\<box> \<longrightarrow> cpred (WHILE b DO c) (drop (Suc k) cfs ! 0) (drop (Suc k) cfs ! (length (drop (Suc k) cfs) - Suc 0))
[PROOF STEP]
have "cpred (WHILE b DO c) (cfs ! Suc k) (cfs ! (length cfs - 1))"
[PROOF STATE]
proof (prove)
using this:
bcomp (b, False, size (ccomp c) + 1) @ ccomp c @ [JMP (- size (bcomp (b, False, size (ccomp c) + 1)) - size (ccomp c) - 1)] \<Turnstile> drop (Suc k) cfs\<box>
length (drop (Suc k) cfs) < length cfs \<longrightarrow> bcomp (b, False, size (ccomp c) + 1) @ ccomp c @ [JMP (- size (bcomp (b, False, size (ccomp c) + 1)) - size (ccomp c) - 1)] \<Turnstile> drop (Suc k) cfs\<box> \<longrightarrow> cpred (WHILE b DO c) (drop (Suc k) cfs ! 0) (drop (Suc k) cfs ! (length (drop (Suc k) cfs) - Suc 0))

goal (1 subgoal):
 1. cpred (WHILE b DO c) (cfs ! Suc k) (cfs ! (length cfs - 1))
[PROOF STEP]
using B and C and E
[PROOF STATE]
proof (prove)
using this:
bcomp (b, False, size (ccomp c) + 1) @ ccomp c @ [JMP (- size (bcomp (b, False, size (ccomp c) + 1)) - size (ccomp c) - 1)] \<Turnstile> drop (Suc k) cfs\<box>
length (drop (Suc k) cfs) < length cfs \<longrightarrow> bcomp (b, False, size (ccomp c) + 1) @ ccomp c @ [JMP (- size (bcomp (b, False, size (ccomp c) + 1)) - size (ccomp c) - 1)] \<Turnstile> drop (Suc k) cfs\<box> \<longrightarrow> cpred (WHILE b DO c) (drop (Suc k) cfs ! 0) (drop (Suc k) cfs ! (length (drop (Suc k) cfs) - Suc 0))
k < length cfs
k \<noteq> length cfs - 1
Suc k + (length (drop (Suc k) cfs) - 1) = length cfs - 1

goal (1 subgoal):
 1. cpred (WHILE b DO c) (cfs ! Suc k) (cfs ! (length cfs - 1))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cpred (WHILE b DO c) (cfs ! Suc k) (cfs ! (length cfs - 1))

goal (1 subgoal):
 1. \<And>xs a ba k aa. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> bcomp (b, False, size (ccomp c) + 1) @ ccomp c @ [JMP (- size (bcomp (b, False, size (ccomp c) + 1)) - size (ccomp c) - 1)] \<Turnstile> ys\<box> \<longrightarrow> cpred (WHILE b DO c) (ys ! 0) (ys ! (length ys - Suc 0)); bcomp (b, False, size (ccomp c) + 1) @ ccomp c @ [JMP (- size (bcomp (b, False, size (ccomp c) + 1)) - size (ccomp c) - 1)] \<Turnstile> xs\<box>; \<And>cfs. ccomp c \<Turnstile> cfs\<box> \<Longrightarrow> cpred c (cfs ! 0) (cfs ! (length cfs - Suc 0)); xs ! 0 = (0, a, ba); bval b a; k < length xs; xs ! k = (size (bcomp (b, False, size (ccomp c) + 1)) + size (ccomp c), aa, ba); (c, a) \<Rightarrow> aa\<rbrakk> \<Longrightarrow> cpred (WHILE b DO c) (0, a, ba) (xs ! (length xs - Suc 0))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
cpred (WHILE b DO c) (cfs ! Suc k) (cfs ! (length cfs - 1))

goal (1 subgoal):
 1. \<And>xs a ba k aa. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> bcomp (b, False, size (ccomp c) + 1) @ ccomp c @ [JMP (- size (bcomp (b, False, size (ccomp c) + 1)) - size (ccomp c) - 1)] \<Turnstile> ys\<box> \<longrightarrow> cpred (WHILE b DO c) (ys ! 0) (ys ! (length ys - Suc 0)); bcomp (b, False, size (ccomp c) + 1) @ ccomp c @ [JMP (- size (bcomp (b, False, size (ccomp c) + 1)) - size (ccomp c) - 1)] \<Turnstile> xs\<box>; \<And>cfs. ccomp c \<Turnstile> cfs\<box> \<Longrightarrow> cpred c (cfs ! 0) (cfs ! (length cfs - Suc 0)); xs ! 0 = (0, a, ba); bval b a; k < length xs; xs ! k = (size (bcomp (b, False, size (ccomp c) + 1)) + size (ccomp c), aa, ba); (c, a) \<Rightarrow> aa\<rbrakk> \<Longrightarrow> cpred (WHILE b DO c) (0, a, ba) (xs ! (length xs - Suc 0))
[PROOF STEP]
assume "bval b s" and "(c, s) \<Rightarrow> s'"
[PROOF STATE]
proof (state)
this:
bval b s
(c, s) \<Rightarrow> s'

goal (1 subgoal):
 1. \<And>xs a ba k aa. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> bcomp (b, False, size (ccomp c) + 1) @ ccomp c @ [JMP (- size (bcomp (b, False, size (ccomp c) + 1)) - size (ccomp c) - 1)] \<Turnstile> ys\<box> \<longrightarrow> cpred (WHILE b DO c) (ys ! 0) (ys ! (length ys - Suc 0)); bcomp (b, False, size (ccomp c) + 1) @ ccomp c @ [JMP (- size (bcomp (b, False, size (ccomp c) + 1)) - size (ccomp c) - 1)] \<Turnstile> xs\<box>; \<And>cfs. ccomp c \<Turnstile> cfs\<box> \<Longrightarrow> cpred c (cfs ! 0) (cfs ! (length cfs - Suc 0)); xs ! 0 = (0, a, ba); bval b a; k < length xs; xs ! k = (size (bcomp (b, False, size (ccomp c) + 1)) + size (ccomp c), aa, ba); (c, a) \<Rightarrow> aa\<rbrakk> \<Longrightarrow> cpred (WHILE b DO c) (0, a, ba) (xs ! (length xs - Suc 0))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
cpred (WHILE b DO c) (cfs ! Suc k) (cfs ! (length cfs - 1))
bval b s
(c, s) \<Rightarrow> s'
[PROOF STEP]
show "cpred (WHILE b DO c) (0, s, stk) (cfs ! (length cfs - Suc 0))"
[PROOF STATE]
proof (prove)
using this:
cpred (WHILE b DO c) (cfs ! Suc k) (cfs ! (length cfs - 1))
bval b s
(c, s) \<Rightarrow> s'

goal (1 subgoal):
 1. cpred (WHILE b DO c) (0, s, stk) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
using D
[PROOF STATE]
proof (prove)
using this:
cpred (WHILE b DO c) (cfs ! Suc k) (cfs ! (length cfs - 1))
bval b s
(c, s) \<Rightarrow> s'
cfs ! Suc k = (0, s', stk)

goal (1 subgoal):
 1. cpred (WHILE b DO c) (0, s, stk) (cfs ! (length cfs - Suc 0))
[PROOF STEP]
by (auto simp: cpred_def)
[PROOF STATE]
proof (state)
this:
cpred (WHILE b DO c) (0, s, stk) (cfs ! (length cfs - Suc 0))

goal:
No subgoals!
[PROOF STEP]
qed