[STATEMENT]
lemma System_sum_bounded:
    "System \<in> Always {s. (\<Sum>i \<in> lessThan Nclients. (tokens o sub i o allocGiv) s)
            \<le> NbT + (\<Sum>i \<in> lessThan Nclients. (tokens o sub i o allocRel) s)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. System \<in> Always {s. (\<Sum>i<Nclients. (sum_list \<circ> sub i \<circ> allocGiv) s) \<le> NbT + (\<Sum>i<Nclients. (sum_list \<circ> sub i \<circ> allocRel) s)}
[PROOF STEP]
apply (simp add: o_apply)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. System \<in> Always {s. (\<Sum>x<Nclients. sum_list (allocGiv s x)) \<le> NbT + (\<Sum>x<Nclients. sum_list (allocRel s x))}
[PROOF STEP]
apply (insert Alloc_Safety [THEN rename_guarantees_sysOfAlloc_I])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rename sysOfAlloc Alloc \<in> rename sysOfAlloc ` (\<Inter>i<Nclients. Increasing (sub i \<circ> allocRel)) guarantees rename sysOfAlloc ` Always {s. (\<Sum>i<Nclients. (sum_list \<circ> sub i \<circ> allocGiv) s) \<le> NbT + (\<Sum>i<Nclients. (sum_list \<circ> sub i \<circ> allocRel) s)} \<Longrightarrow> System \<in> Always {s. (\<Sum>x<Nclients. sum_list (allocGiv s x)) \<le> NbT + (\<Sum>x<Nclients. sum_list (allocRel s x))}
[PROOF STEP]
apply (simp add: o_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rename sysOfAlloc Alloc \<in> (\<Inter>x<Nclients. Increasing (\<lambda>xa. allocRel xa x)) guarantees Always {y. (\<Sum>x<Nclients. sum_list (allocGiv y x)) \<le> NbT + (\<Sum>x<Nclients. sum_list (allocRel y x))} \<Longrightarrow> System \<in> Always {s. (\<Sum>x<Nclients. sum_list (allocGiv s x)) \<le> NbT + (\<Sum>x<Nclients. sum_list (allocRel s x))}
[PROOF STEP]
apply (erule component_guaranteesD)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. rename sysOfAlloc Alloc \<squnion> ?G19 = System
 2. System \<in> (\<Inter>x<Nclients. Increasing (\<lambda>xa. allocRel xa x))
 3. rename sysOfAlloc Alloc ok ?G19
[PROOF STEP]
apply (auto simp add: System_Increasing_allocRel [simplified sub_apply o_def])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done