[STATEMENT]
lemma wt_ge_0[simp]:
assumes "proper c" and "i < brn c"
shows "0 \<le> wt c s i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> wt c s i
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
proper c
i < brn c

goal (1 subgoal):
 1. 0 \<le> wt c s i
[PROOF STEP]
proof (induct c arbitrary: i s rule: proper_induct)
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<And>i s. i < brn Done \<Longrightarrow> 0 \<le> wt Done s i
 2. \<And>atm i s. i < brn (Atm atm) \<Longrightarrow> 0 \<le> wt (Atm atm) s i
 3. \<And>c1 c2 i s. \<lbrakk>\<And>i s. i < brn c1 \<Longrightarrow> 0 \<le> wt c1 s i; \<And>i s. i < brn c2 \<Longrightarrow> 0 \<le> wt c2 s i; i < brn (c1 ;; c2)\<rbrakk> \<Longrightarrow> 0 \<le> wt (c1 ;; c2) s i
 4. \<And>tst c i s. \<lbrakk>\<And>i s. i < brn c \<Longrightarrow> 0 \<le> wt c s i; i < brn (While tst c)\<rbrakk> \<Longrightarrow> 0 \<le> wt (While tst c) s i
 5. \<And>ch c1 c2 i s. \<lbrakk>\<And>i s. i < brn c1 \<Longrightarrow> 0 \<le> wt c1 s i; \<And>i s. i < brn c2 \<Longrightarrow> 0 \<le> wt c2 s i; i < brn (Ch ch c1 c2)\<rbrakk> \<Longrightarrow> 0 \<le> wt (Ch ch c1 c2) s i
 6. \<And>cl i s. \<lbrakk>properL cl; \<And>c i s. \<lbrakk>c \<in> set cl; i < brn c\<rbrakk> \<Longrightarrow> 0 \<le> wt c s i; i < brn (Par cl)\<rbrakk> \<Longrightarrow> 0 \<le> wt (Par cl) s i
 7. \<And>cl i s. \<lbrakk>properL cl; \<And>c i s. \<lbrakk>c \<in> set cl; i < brn c\<rbrakk> \<Longrightarrow> 0 \<le> wt c s i; i < brn (ParT cl)\<rbrakk> \<Longrightarrow> 0 \<le> wt (ParT cl) s i
[PROOF STEP]
case (Ch ch c1 c2)
[PROOF STATE]
proof (state)
this:
?i < brn c1 \<Longrightarrow> 0 \<le> wt c1 ?s ?i
?i < brn c2 \<Longrightarrow> 0 \<le> wt c2 ?s ?i
i < brn (Ch ch c1 c2)

goal (7 subgoals):
 1. \<And>i s. i < brn Done \<Longrightarrow> 0 \<le> wt Done s i
 2. \<And>atm i s. i < brn (Atm atm) \<Longrightarrow> 0 \<le> wt (Atm atm) s i
 3. \<And>c1 c2 i s. \<lbrakk>\<And>i s. i < brn c1 \<Longrightarrow> 0 \<le> wt c1 s i; \<And>i s. i < brn c2 \<Longrightarrow> 0 \<le> wt c2 s i; i < brn (c1 ;; c2)\<rbrakk> \<Longrightarrow> 0 \<le> wt (c1 ;; c2) s i
 4. \<And>tst c i s. \<lbrakk>\<And>i s. i < brn c \<Longrightarrow> 0 \<le> wt c s i; i < brn (While tst c)\<rbrakk> \<Longrightarrow> 0 \<le> wt (While tst c) s i
 5. \<And>ch c1 c2 i s. \<lbrakk>\<And>i s. i < brn c1 \<Longrightarrow> 0 \<le> wt c1 s i; \<And>i s. i < brn c2 \<Longrightarrow> 0 \<le> wt c2 s i; i < brn (Ch ch c1 c2)\<rbrakk> \<Longrightarrow> 0 \<le> wt (Ch ch c1 c2) s i
 6. \<And>cl i s. \<lbrakk>properL cl; \<And>c i s. \<lbrakk>c \<in> set cl; i < brn c\<rbrakk> \<Longrightarrow> 0 \<le> wt c s i; i < brn (Par cl)\<rbrakk> \<Longrightarrow> 0 \<le> wt (Par cl) s i
 7. \<And>cl i s. \<lbrakk>properL cl; \<And>c i s. \<lbrakk>c \<in> set cl; i < brn c\<rbrakk> \<Longrightarrow> 0 \<le> wt c s i; i < brn (ParT cl)\<rbrakk> \<Longrightarrow> 0 \<le> wt (ParT cl) s i
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
?i < brn c1 \<Longrightarrow> 0 \<le> wt c1 ?s ?i
?i < brn c2 \<Longrightarrow> 0 \<le> wt c2 ?s ?i
i < brn (Ch ch c1 c2)

goal (1 subgoal):
 1. 0 \<le> wt (Ch ch c1 c2) s i
[PROOF STEP]
using properCh
[PROOF STATE]
proof (prove)
using this:
?i < brn c1 \<Longrightarrow> 0 \<le> wt c1 ?s ?i
?i < brn c2 \<Longrightarrow> 0 \<le> wt c2 ?s ?i
i < brn (Ch ch c1 c2)
0 \<le> cval ?ch ?s \<and> cval ?ch ?s \<le> 1

goal (1 subgoal):
 1. 0 \<le> wt (Ch ch c1 c2) s i
[PROOF STEP]
by (cases i) (auto simp: algebra_simps)
[PROOF STATE]
proof (state)
this:
0 \<le> wt (Ch ch c1 c2) s i

goal (6 subgoals):
 1. \<And>i s. i < brn Done \<Longrightarrow> 0 \<le> wt Done s i
 2. \<And>atm i s. i < brn (Atm atm) \<Longrightarrow> 0 \<le> wt (Atm atm) s i
 3. \<And>c1 c2 i s. \<lbrakk>\<And>i s. i < brn c1 \<Longrightarrow> 0 \<le> wt c1 s i; \<And>i s. i < brn c2 \<Longrightarrow> 0 \<le> wt c2 s i; i < brn (c1 ;; c2)\<rbrakk> \<Longrightarrow> 0 \<le> wt (c1 ;; c2) s i
 4. \<And>tst c i s. \<lbrakk>\<And>i s. i < brn c \<Longrightarrow> 0 \<le> wt c s i; i < brn (While tst c)\<rbrakk> \<Longrightarrow> 0 \<le> wt (While tst c) s i
 5. \<And>cl i s. \<lbrakk>properL cl; \<And>c i s. \<lbrakk>c \<in> set cl; i < brn c\<rbrakk> \<Longrightarrow> 0 \<le> wt c s i; i < brn (Par cl)\<rbrakk> \<Longrightarrow> 0 \<le> wt (Par cl) s i
 6. \<And>cl i s. \<lbrakk>properL cl; \<And>c i s. \<lbrakk>c \<in> set cl; i < brn c\<rbrakk> \<Longrightarrow> 0 \<le> wt c s i; i < brn (ParT cl)\<rbrakk> \<Longrightarrow> 0 \<le> wt (ParT cl) s i
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>i s. i < brn Done \<Longrightarrow> 0 \<le> wt Done s i
 2. \<And>atm i s. i < brn (Atm atm) \<Longrightarrow> 0 \<le> wt (Atm atm) s i
 3. \<And>c1 c2 i s. \<lbrakk>\<And>i s. i < brn c1 \<Longrightarrow> 0 \<le> wt c1 s i; \<And>i s. i < brn c2 \<Longrightarrow> 0 \<le> wt c2 s i; i < brn (c1 ;; c2)\<rbrakk> \<Longrightarrow> 0 \<le> wt (c1 ;; c2) s i
 4. \<And>tst c i s. \<lbrakk>\<And>i s. i < brn c \<Longrightarrow> 0 \<le> wt c s i; i < brn (While tst c)\<rbrakk> \<Longrightarrow> 0 \<le> wt (While tst c) s i
 5. \<And>cl i s. \<lbrakk>properL cl; \<And>c i s. \<lbrakk>c \<in> set cl; i < brn c\<rbrakk> \<Longrightarrow> 0 \<le> wt c s i; i < brn (Par cl)\<rbrakk> \<Longrightarrow> 0 \<le> wt (Par cl) s i
 6. \<And>cl i s. \<lbrakk>properL cl; \<And>c i s. \<lbrakk>c \<in> set cl; i < brn c\<rbrakk> \<Longrightarrow> 0 \<le> wt c s i; i < brn (ParT cl)\<rbrakk> \<Longrightarrow> 0 \<le> wt (ParT cl) s i
[PROOF STEP]
case (Par cl ii)
[PROOF STATE]
proof (state)
this:
properL cl
\<lbrakk>?c \<in> set cl; ?i < brn ?c\<rbrakk> \<Longrightarrow> 0 \<le> wt ?c ?s ?i
ii < brn (Par cl)

goal (6 subgoals):
 1. \<And>i s. i < brn Done \<Longrightarrow> 0 \<le> wt Done s i
 2. \<And>atm i s. i < brn (Atm atm) \<Longrightarrow> 0 \<le> wt (Atm atm) s i
 3. \<And>c1 c2 i s. \<lbrakk>\<And>i s. i < brn c1 \<Longrightarrow> 0 \<le> wt c1 s i; \<And>i s. i < brn c2 \<Longrightarrow> 0 \<le> wt c2 s i; i < brn (c1 ;; c2)\<rbrakk> \<Longrightarrow> 0 \<le> wt (c1 ;; c2) s i
 4. \<And>tst c i s. \<lbrakk>\<And>i s. i < brn c \<Longrightarrow> 0 \<le> wt c s i; i < brn (While tst c)\<rbrakk> \<Longrightarrow> 0 \<le> wt (While tst c) s i
 5. \<And>cl i s. \<lbrakk>properL cl; \<And>c i s. \<lbrakk>c \<in> set cl; i < brn c\<rbrakk> \<Longrightarrow> 0 \<le> wt c s i; i < brn (Par cl)\<rbrakk> \<Longrightarrow> 0 \<le> wt (Par cl) s i
 6. \<And>cl i s. \<lbrakk>properL cl; \<And>c i s. \<lbrakk>c \<in> set cl; i < brn c\<rbrakk> \<Longrightarrow> 0 \<le> wt c s i; i < brn (ParT cl)\<rbrakk> \<Longrightarrow> 0 \<le> wt (ParT cl) s i
[PROOF STEP]
have "properL cl" and "ii < brnL cl (length cl)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. properL cl &&& ii < brnL cl (length cl)
[PROOF STEP]
using Par
[PROOF STATE]
proof (prove)
using this:
properL cl
\<lbrakk>?c \<in> set cl; ?i < brn ?c\<rbrakk> \<Longrightarrow> 0 \<le> wt ?c ?s ?i
ii < brn (Par cl)

goal (1 subgoal):
 1. properL cl &&& ii < brnL cl (length cl)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
properL cl
ii < brnL cl (length cl)

goal (6 subgoals):
 1. \<And>i s. i < brn Done \<Longrightarrow> 0 \<le> wt Done s i
 2. \<And>atm i s. i < brn (Atm atm) \<Longrightarrow> 0 \<le> wt (Atm atm) s i
 3. \<And>c1 c2 i s. \<lbrakk>\<And>i s. i < brn c1 \<Longrightarrow> 0 \<le> wt c1 s i; \<And>i s. i < brn c2 \<Longrightarrow> 0 \<le> wt c2 s i; i < brn (c1 ;; c2)\<rbrakk> \<Longrightarrow> 0 \<le> wt (c1 ;; c2) s i
 4. \<And>tst c i s. \<lbrakk>\<And>i s. i < brn c \<Longrightarrow> 0 \<le> wt c s i; i < brn (While tst c)\<rbrakk> \<Longrightarrow> 0 \<le> wt (While tst c) s i
 5. \<And>cl i s. \<lbrakk>properL cl; \<And>c i s. \<lbrakk>c \<in> set cl; i < brn c\<rbrakk> \<Longrightarrow> 0 \<le> wt c s i; i < brn (Par cl)\<rbrakk> \<Longrightarrow> 0 \<le> wt (Par cl) s i
 6. \<And>cl i s. \<lbrakk>properL cl; \<And>c i s. \<lbrakk>c \<in> set cl; i < brn c\<rbrakk> \<Longrightarrow> 0 \<le> wt c s i; i < brn (ParT cl)\<rbrakk> \<Longrightarrow> 0 \<le> wt (ParT cl) s i
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
properL cl
ii < brnL cl (length cl)

goal (1 subgoal):
 1. 0 \<le> wt (Par cl) s ii
[PROOF STEP]
apply (cases rule: brnL_cases)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n i. \<lbrakk>n < length cl; i < brn (cl ! n); ii = brnL cl n + i\<rbrakk> \<Longrightarrow> 0 \<le> wt (Par cl) s ii
[PROOF STEP]
using Par
[PROOF STATE]
proof (prove)
using this:
properL cl
\<lbrakk>?c \<in> set cl; ?i < brn ?c\<rbrakk> \<Longrightarrow> 0 \<le> wt ?c ?s ?i
ii < brn (Par cl)

goal (1 subgoal):
 1. \<And>n i. \<lbrakk>n < length cl; i < brn (cl ! n); ii = brnL cl n + i\<rbrakk> \<Longrightarrow> 0 \<le> wt (Par cl) s ii
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 \<le> wt (Par cl) s ii

goal (5 subgoals):
 1. \<And>i s. i < brn Done \<Longrightarrow> 0 \<le> wt Done s i
 2. \<And>atm i s. i < brn (Atm atm) \<Longrightarrow> 0 \<le> wt (Atm atm) s i
 3. \<And>c1 c2 i s. \<lbrakk>\<And>i s. i < brn c1 \<Longrightarrow> 0 \<le> wt c1 s i; \<And>i s. i < brn c2 \<Longrightarrow> 0 \<le> wt c2 s i; i < brn (c1 ;; c2)\<rbrakk> \<Longrightarrow> 0 \<le> wt (c1 ;; c2) s i
 4. \<And>tst c i s. \<lbrakk>\<And>i s. i < brn c \<Longrightarrow> 0 \<le> wt c s i; i < brn (While tst c)\<rbrakk> \<Longrightarrow> 0 \<le> wt (While tst c) s i
 5. \<And>cl i s. \<lbrakk>properL cl; \<And>c i s. \<lbrakk>c \<in> set cl; i < brn c\<rbrakk> \<Longrightarrow> 0 \<le> wt c s i; i < brn (ParT cl)\<rbrakk> \<Longrightarrow> 0 \<le> wt (ParT cl) s i
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>i s. i < brn Done \<Longrightarrow> 0 \<le> wt Done s i
 2. \<And>atm i s. i < brn (Atm atm) \<Longrightarrow> 0 \<le> wt (Atm atm) s i
 3. \<And>c1 c2 i s. \<lbrakk>\<And>i s. i < brn c1 \<Longrightarrow> 0 \<le> wt c1 s i; \<And>i s. i < brn c2 \<Longrightarrow> 0 \<le> wt c2 s i; i < brn (c1 ;; c2)\<rbrakk> \<Longrightarrow> 0 \<le> wt (c1 ;; c2) s i
 4. \<And>tst c i s. \<lbrakk>\<And>i s. i < brn c \<Longrightarrow> 0 \<le> wt c s i; i < brn (While tst c)\<rbrakk> \<Longrightarrow> 0 \<le> wt (While tst c) s i
 5. \<And>cl i s. \<lbrakk>properL cl; \<And>c i s. \<lbrakk>c \<in> set cl; i < brn c\<rbrakk> \<Longrightarrow> 0 \<le> wt c s i; i < brn (ParT cl)\<rbrakk> \<Longrightarrow> 0 \<le> wt (ParT cl) s i
[PROOF STEP]
case (ParT cl ii)
[PROOF STATE]
proof (state)
this:
properL cl
\<lbrakk>?c \<in> set cl; ?i < brn ?c\<rbrakk> \<Longrightarrow> 0 \<le> wt ?c ?s ?i
ii < brn (ParT cl)

goal (5 subgoals):
 1. \<And>i s. i < brn Done \<Longrightarrow> 0 \<le> wt Done s i
 2. \<And>atm i s. i < brn (Atm atm) \<Longrightarrow> 0 \<le> wt (Atm atm) s i
 3. \<And>c1 c2 i s. \<lbrakk>\<And>i s. i < brn c1 \<Longrightarrow> 0 \<le> wt c1 s i; \<And>i s. i < brn c2 \<Longrightarrow> 0 \<le> wt c2 s i; i < brn (c1 ;; c2)\<rbrakk> \<Longrightarrow> 0 \<le> wt (c1 ;; c2) s i
 4. \<And>tst c i s. \<lbrakk>\<And>i s. i < brn c \<Longrightarrow> 0 \<le> wt c s i; i < brn (While tst c)\<rbrakk> \<Longrightarrow> 0 \<le> wt (While tst c) s i
 5. \<And>cl i s. \<lbrakk>properL cl; \<And>c i s. \<lbrakk>c \<in> set cl; i < brn c\<rbrakk> \<Longrightarrow> 0 \<le> wt c s i; i < brn (ParT cl)\<rbrakk> \<Longrightarrow> 0 \<le> wt (ParT cl) s i
[PROOF STEP]
have "properL cl" and "ii < brnL cl (length cl)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. properL cl &&& ii < brnL cl (length cl)
[PROOF STEP]
using ParT
[PROOF STATE]
proof (prove)
using this:
properL cl
\<lbrakk>?c \<in> set cl; ?i < brn ?c\<rbrakk> \<Longrightarrow> 0 \<le> wt ?c ?s ?i
ii < brn (ParT cl)

goal (1 subgoal):
 1. properL cl &&& ii < brnL cl (length cl)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
properL cl
ii < brnL cl (length cl)

goal (5 subgoals):
 1. \<And>i s. i < brn Done \<Longrightarrow> 0 \<le> wt Done s i
 2. \<And>atm i s. i < brn (Atm atm) \<Longrightarrow> 0 \<le> wt (Atm atm) s i
 3. \<And>c1 c2 i s. \<lbrakk>\<And>i s. i < brn c1 \<Longrightarrow> 0 \<le> wt c1 s i; \<And>i s. i < brn c2 \<Longrightarrow> 0 \<le> wt c2 s i; i < brn (c1 ;; c2)\<rbrakk> \<Longrightarrow> 0 \<le> wt (c1 ;; c2) s i
 4. \<And>tst c i s. \<lbrakk>\<And>i s. i < brn c \<Longrightarrow> 0 \<le> wt c s i; i < brn (While tst c)\<rbrakk> \<Longrightarrow> 0 \<le> wt (While tst c) s i
 5. \<And>cl i s. \<lbrakk>properL cl; \<And>c i s. \<lbrakk>c \<in> set cl; i < brn c\<rbrakk> \<Longrightarrow> 0 \<le> wt c s i; i < brn (ParT cl)\<rbrakk> \<Longrightarrow> 0 \<le> wt (ParT cl) s i
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
properL cl
ii < brnL cl (length cl)

goal (1 subgoal):
 1. 0 \<le> wt (ParT cl) s ii
[PROOF STEP]
proof(cases rule: brnL_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n i. \<lbrakk>n < length cl; i < brn (cl ! n); ii = brnL cl n + i\<rbrakk> \<Longrightarrow> 0 \<le> wt (ParT cl) s ii
[PROOF STEP]
case (Local n i)
[PROOF STATE]
proof (state)
this:
n < length cl
i < brn (cl ! n)
ii = brnL cl n + i

goal (1 subgoal):
 1. \<And>n i. \<lbrakk>n < length cl; i < brn (cl ! n); ii = brnL cl n + i\<rbrakk> \<Longrightarrow> 0 \<le> wt (ParT cl) s ii
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> wt (ParT cl) s ii
[PROOF STEP]
proof (cases "WtFT cl = 1")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. WtFT cl = 1 \<Longrightarrow> 0 \<le> wt (ParT cl) s ii
 2. WtFT cl \<noteq> 1 \<Longrightarrow> 0 \<le> wt (ParT cl) s ii
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
WtFT cl = 1

goal (2 subgoals):
 1. WtFT cl = 1 \<Longrightarrow> 0 \<le> wt (ParT cl) s ii
 2. WtFT cl \<noteq> 1 \<Longrightarrow> 0 \<le> wt (ParT cl) s ii
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
WtFT cl = 1

goal (1 subgoal):
 1. 0 \<le> wt (ParT cl) s ii
[PROOF STEP]
using Local ParT
[PROOF STATE]
proof (prove)
using this:
WtFT cl = 1
n < length cl
i < brn (cl ! n)
ii = brnL cl n + i
properL cl
\<lbrakk>?c \<in> set cl; ?i < brn ?c\<rbrakk> \<Longrightarrow> 0 \<le> wt ?c ?s ?i
ii < brn (ParT cl)

goal (1 subgoal):
 1. 0 \<le> wt (ParT cl) s ii
[PROOF STEP]
by (cases "n = pickFT cl \<and> i = 0") auto
[PROOF STATE]
proof (state)
this:
0 \<le> wt (ParT cl) s ii

goal (1 subgoal):
 1. WtFT cl \<noteq> 1 \<Longrightarrow> 0 \<le> wt (ParT cl) s ii
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. WtFT cl \<noteq> 1 \<Longrightarrow> 0 \<le> wt (ParT cl) s ii
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
WtFT cl \<noteq> 1

goal (1 subgoal):
 1. WtFT cl \<noteq> 1 \<Longrightarrow> 0 \<le> wt (ParT cl) s ii
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
WtFT cl \<noteq> 1

goal (1 subgoal):
 1. 0 \<le> wt (ParT cl) s ii
[PROOF STEP]
using Local ParT
[PROOF STATE]
proof (prove)
using this:
WtFT cl \<noteq> 1
n < length cl
i < brn (cl ! n)
ii = brnL cl n + i
properL cl
\<lbrakk>?c \<in> set cl; ?i < brn ?c\<rbrakk> \<Longrightarrow> 0 \<le> wt ?c ?s ?i
ii < brn (ParT cl)

goal (1 subgoal):
 1. 0 \<le> wt (ParT cl) s ii
[PROOF STEP]
by (cases "finished (cl ! n)") auto
[PROOF STATE]
proof (state)
this:
0 \<le> wt (ParT cl) s ii

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
0 \<le> wt (ParT cl) s ii

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
0 \<le> wt (ParT cl) s ii

goal (4 subgoals):
 1. \<And>i s. i < brn Done \<Longrightarrow> 0 \<le> wt Done s i
 2. \<And>atm i s. i < brn (Atm atm) \<Longrightarrow> 0 \<le> wt (Atm atm) s i
 3. \<And>c1 c2 i s. \<lbrakk>\<And>i s. i < brn c1 \<Longrightarrow> 0 \<le> wt c1 s i; \<And>i s. i < brn c2 \<Longrightarrow> 0 \<le> wt c2 s i; i < brn (c1 ;; c2)\<rbrakk> \<Longrightarrow> 0 \<le> wt (c1 ;; c2) s i
 4. \<And>tst c i s. \<lbrakk>\<And>i s. i < brn c \<Longrightarrow> 0 \<le> wt c s i; i < brn (While tst c)\<rbrakk> \<Longrightarrow> 0 \<le> wt (While tst c) s i
[PROOF STEP]
qed auto