[STATEMENT]
theorem (in finite) update_balanced:
  assumes "\<rho> 0 = 0" and "\<forall>n. \<rho> n < 1" and "0 \<le> i"
  shows "balanced \<L> c = balanced (update_ledger \<rho> i \<L>) ((1 + i) * c)"
    (is "_ = balanced ?\<L>' ((1 + i) * c)")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. balanced \<L> c = balanced (update_ledger \<rho> i \<L>) ((1 + i) * c)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. balanced \<L> c \<Longrightarrow> balanced (update_ledger \<rho> i \<L>) ((1 + i) * c)
 2. balanced (update_ledger \<rho> i \<L>) ((1 + i) * c) \<Longrightarrow> balanced \<L> c
[PROOF STEP]
assume "balanced \<L> c"
[PROOF STATE]
proof (state)
this:
balanced \<L> c

goal (2 subgoals):
 1. balanced \<L> c \<Longrightarrow> balanced (update_ledger \<rho> i \<L>) ((1 + i) * c)
 2. balanced (update_ledger \<rho> i \<L>) ((1 + i) * c) \<Longrightarrow> balanced \<L> c
[PROOF STEP]
have "\<forall>n>0. (\<Sum>a\<in>UNIV. \<pi> (?\<L>' a) n) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n>0. (\<Sum>a\<in>UNIV. \<pi> (update_ledger \<rho> i \<L> a) n) = 0
[PROOF STEP]
proof (rule allI, rule impI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. 0 < n \<Longrightarrow> (\<Sum>a\<in>UNIV. \<pi> (update_ledger \<rho> i \<L> a) n) = 0
[PROOF STEP]
fix n :: nat
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. 0 < n \<Longrightarrow> (\<Sum>a\<in>UNIV. \<pi> (update_ledger \<rho> i \<L> a) n) = 0
[PROOF STEP]
assume "n > 0"
[PROOF STATE]
proof (state)
this:
0 < n

goal (1 subgoal):
 1. \<And>n. 0 < n \<Longrightarrow> (\<Sum>a\<in>UNIV. \<pi> (update_ledger \<rho> i \<L> a) n) = 0
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
0 < n

goal (1 subgoal):
 1. \<And>n. 0 < n \<Longrightarrow> (\<Sum>a\<in>UNIV. \<pi> (update_ledger \<rho> i \<L> a) n) = 0
[PROOF STEP]
fix a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. 0 < n \<Longrightarrow> (\<Sum>a\<in>UNIV. \<pi> (update_ledger \<rho> i \<L> a) n) = 0
[PROOF STEP]
let ?\<alpha>' = "\<lambda>n. (1 - \<rho> n) * \<pi> (\<L> a) n"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. 0 < n \<Longrightarrow> (\<Sum>a\<in>UNIV. \<pi> (update_ledger \<rho> i \<L> a) n) = 0
[PROOF STEP]
have "\<pi> (?\<L>' a) n = ?\<alpha>' n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> (update_ledger \<rho> i \<L> a) n = (1 - \<rho> n) * \<pi> (\<L> a) n
[PROOF STEP]
unfolding
          update_ledger_def
          update_account_def
          Rep_account_plus
          Rep_account_just_cash
          Rep_account_return_loans
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if n = 0 then i * net_asset_value (\<L> a) else 0) + (1 - \<rho> n) * \<pi> (\<L> a) n = (1 - \<rho> n) * \<pi> (\<L> a) n
[PROOF STEP]
using plus_account_def \<open>n > 0\<close>
[PROOF STATE]
proof (prove)
using this:
?\<alpha>\<^sub>1 + ?\<alpha>\<^sub>2 = \<iota> (\<lambda>n. \<pi> ?\<alpha>\<^sub>1 n + \<pi> ?\<alpha>\<^sub>2 n)
0 < n

goal (1 subgoal):
 1. (if n = 0 then i * net_asset_value (\<L> a) else 0) + (1 - \<rho> n) * \<pi> (\<L> a) n = (1 - \<rho> n) * \<pi> (\<L> a) n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<pi> (update_ledger \<rho> i \<L> a) n = (1 - \<rho> n) * \<pi> (\<L> a) n

goal (1 subgoal):
 1. \<And>n. 0 < n \<Longrightarrow> (\<Sum>a\<in>UNIV. \<pi> (update_ledger \<rho> i \<L> a) n) = 0
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<pi> (update_ledger \<rho> i \<L> ?a2) n = (1 - \<rho> n) * \<pi> (\<L> ?a2) n

goal (1 subgoal):
 1. \<And>n. 0 < n \<Longrightarrow> (\<Sum>a\<in>UNIV. \<pi> (update_ledger \<rho> i \<L> a) n) = 0
[PROOF STEP]
hence "(\<Sum>a\<in>UNIV. \<pi> (?\<L>' a) n) =
             (1 - \<rho> n) * (\<Sum>a\<in>UNIV. \<pi> (\<L> a) n)"
[PROOF STATE]
proof (prove)
using this:
\<pi> (update_ledger \<rho> i \<L> ?a2) n = (1 - \<rho> n) * \<pi> (\<L> ?a2) n

goal (1 subgoal):
 1. (\<Sum>a\<in>UNIV. \<pi> (update_ledger \<rho> i \<L> a) n) = (1 - \<rho> n) * (\<Sum>a\<in>UNIV. \<pi> (\<L> a) n)
[PROOF STEP]
using finite_UNIV
[PROOF STATE]
proof (prove)
using this:
\<pi> (update_ledger \<rho> i \<L> ?a2) n = (1 - \<rho> n) * \<pi> (\<L> ?a2) n
finite UNIV

goal (1 subgoal):
 1. (\<Sum>a\<in>UNIV. \<pi> (update_ledger \<rho> i \<L> a) n) = (1 - \<rho> n) * (\<Sum>a\<in>UNIV. \<pi> (\<L> a) n)
[PROOF STEP]
by (metis (mono_tags, lifting) sum.cong sum_distrib_left)
[PROOF STATE]
proof (state)
this:
(\<Sum>a\<in>UNIV. \<pi> (update_ledger \<rho> i \<L> a) n) = (1 - \<rho> n) * (\<Sum>a\<in>UNIV. \<pi> (\<L> a) n)

goal (1 subgoal):
 1. \<And>n. 0 < n \<Longrightarrow> (\<Sum>a\<in>UNIV. \<pi> (update_ledger \<rho> i \<L> a) n) = 0
[PROOF STEP]
thus "(\<Sum>a\<in>UNIV. \<pi> (?\<L>' a) n) = 0"
[PROOF STATE]
proof (prove)
using this:
(\<Sum>a\<in>UNIV. \<pi> (update_ledger \<rho> i \<L> a) n) = (1 - \<rho> n) * (\<Sum>a\<in>UNIV. \<pi> (\<L> a) n)

goal (1 subgoal):
 1. (\<Sum>a\<in>UNIV. \<pi> (update_ledger \<rho> i \<L> a) n) = 0
[PROOF STEP]
using \<open>0 < n\<close> \<open>balanced \<L> c\<close> local.balanced_alt_def
[PROOF STATE]
proof (prove)
using this:
(\<Sum>a\<in>UNIV. \<pi> (update_ledger \<rho> i \<L> a) n) = (1 - \<rho> n) * (\<Sum>a\<in>UNIV. \<pi> (\<L> a) n)
0 < n
balanced \<L> c
balanced ?\<L> ?c = ((\<Sum>a\<in>UNIV. cash_reserve (?\<L> a)) = ?c \<and> (\<forall>n>0. (\<Sum>a\<in>UNIV. \<pi> (?\<L> a) n) = 0))

goal (1 subgoal):
 1. (\<Sum>a\<in>UNIV. \<pi> (update_ledger \<rho> i \<L> a) n) = 0
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
(\<Sum>a\<in>UNIV. \<pi> (update_ledger \<rho> i \<L> a) n) = 0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>n>0. (\<Sum>a\<in>UNIV. \<pi> (update_ledger \<rho> i \<L> a) n) = 0

goal (2 subgoals):
 1. balanced \<L> c \<Longrightarrow> balanced (update_ledger \<rho> i \<L>) ((1 + i) * c)
 2. balanced (update_ledger \<rho> i \<L>) ((1 + i) * c) \<Longrightarrow> balanced \<L> c
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>n>0. (\<Sum>a\<in>UNIV. \<pi> (update_ledger \<rho> i \<L> a) n) = 0

goal (2 subgoals):
 1. balanced \<L> c \<Longrightarrow> balanced (update_ledger \<rho> i \<L>) ((1 + i) * c)
 2. balanced (update_ledger \<rho> i \<L>) ((1 + i) * c) \<Longrightarrow> balanced \<L> c
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<forall>n>0. (\<Sum>a\<in>UNIV. \<pi> (update_ledger \<rho> i \<L> a) n) = 0

goal (2 subgoals):
 1. balanced \<L> c \<Longrightarrow> balanced (update_ledger \<rho> i \<L>) ((1 + i) * c)
 2. balanced (update_ledger \<rho> i \<L>) ((1 + i) * c) \<Longrightarrow> balanced \<L> c
[PROOF STEP]
fix S :: "'a set"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. balanced \<L> c \<Longrightarrow> balanced (update_ledger \<rho> i \<L>) ((1 + i) * c)
 2. balanced (update_ledger \<rho> i \<L>) ((1 + i) * c) \<Longrightarrow> balanced \<L> c
[PROOF STEP]
let ?\<omega> = "shortest_ledger_period \<L>"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. balanced \<L> c \<Longrightarrow> balanced (update_ledger \<rho> i \<L>) ((1 + i) * c)
 2. balanced (update_ledger \<rho> i \<L>) ((1 + i) * c) \<Longrightarrow> balanced \<L> c
[PROOF STEP]
assume "(\<Sum>a\<in>S. cash_reserve (\<L> a)) = c"
    and "\<forall>n>0. (\<Sum>a\<in>S. \<pi> (\<L> a) n) = 0"
[PROOF STATE]
proof (state)
this:
(\<Sum>a\<in>S. cash_reserve (\<L> a)) = c
\<forall>n>0. (\<Sum>a\<in>S. \<pi> (\<L> a) n) = 0

goal (2 subgoals):
 1. balanced \<L> c \<Longrightarrow> balanced (update_ledger \<rho> i \<L>) ((1 + i) * c)
 2. balanced (update_ledger \<rho> i \<L>) ((1 + i) * c) \<Longrightarrow> balanced \<L> c
[PROOF STEP]
have "(\<Sum>a\<in>S. cash_reserve (?\<L>' a)) =
              (\<Sum>a\<in>S. i * (\<Sum> n \<le> ?\<omega>. \<pi> (\<L> a) n) +
                   cash_reserve (\<L> a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>a\<in>S. cash_reserve (update_ledger \<rho> i \<L> a)) = (\<Sum>a\<in>S. i * sum (\<pi> (\<L> a)) {..shortest_ledger_period \<L>} + cash_reserve (\<L> a))
[PROOF STEP]
using finite
[PROOF STATE]
proof (prove)
using this:
finite ?A

goal (1 subgoal):
 1. (\<Sum>a\<in>S. cash_reserve (update_ledger \<rho> i \<L> a)) = (\<Sum>a\<in>S. i * sum (\<pi> (\<L> a)) {..shortest_ledger_period \<L>} + cash_reserve (\<L> a))
[PROOF STEP]
proof (induct S arbitrary: c rule: finite_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<Sum>a\<in>{}. cash_reserve (update_ledger \<rho> i \<L> a)) = (\<Sum>a\<in>{}. i * sum (\<pi> (\<L> a)) {..shortest_ledger_period \<L>} + cash_reserve (\<L> a))
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; (\<Sum>a\<in>F. cash_reserve (update_ledger \<rho> i \<L> a)) = (\<Sum>a\<in>F. i * sum (\<pi> (\<L> a)) {..shortest_ledger_period \<L>} + cash_reserve (\<L> a))\<rbrakk> \<Longrightarrow> (\<Sum>a\<in>insert x F. cash_reserve (update_ledger \<rho> i \<L> a)) = (\<Sum>a\<in>insert x F. i * sum (\<pi> (\<L> a)) {..shortest_ledger_period \<L>} + cash_reserve (\<L> a))
[PROOF STEP]
case empty
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. (\<Sum>a\<in>{}. cash_reserve (update_ledger \<rho> i \<L> a)) = (\<Sum>a\<in>{}. i * sum (\<pi> (\<L> a)) {..shortest_ledger_period \<L>} + cash_reserve (\<L> a))
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; (\<Sum>a\<in>F. cash_reserve (update_ledger \<rho> i \<L> a)) = (\<Sum>a\<in>F. i * sum (\<pi> (\<L> a)) {..shortest_ledger_period \<L>} + cash_reserve (\<L> a))\<rbrakk> \<Longrightarrow> (\<Sum>a\<in>insert x F. cash_reserve (update_ledger \<rho> i \<L> a)) = (\<Sum>a\<in>insert x F. i * sum (\<pi> (\<L> a)) {..shortest_ledger_period \<L>} + cash_reserve (\<L> a))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>a\<in>{}. cash_reserve (update_ledger \<rho> i \<L> a)) = (\<Sum>a\<in>{}. i * sum (\<pi> (\<L> a)) {..shortest_ledger_period \<L>} + cash_reserve (\<L> a))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>a\<in>{}. cash_reserve (update_ledger \<rho> i \<L> a)) = (\<Sum>a\<in>{}. i * sum (\<pi> (\<L> a)) {..shortest_ledger_period \<L>} + cash_reserve (\<L> a))

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; (\<Sum>a\<in>F. cash_reserve (update_ledger \<rho> i \<L> a)) = (\<Sum>a\<in>F. i * sum (\<pi> (\<L> a)) {..shortest_ledger_period \<L>} + cash_reserve (\<L> a))\<rbrakk> \<Longrightarrow> (\<Sum>a\<in>insert x F. cash_reserve (update_ledger \<rho> i \<L> a)) = (\<Sum>a\<in>insert x F. i * sum (\<pi> (\<L> a)) {..shortest_ledger_period \<L>} + cash_reserve (\<L> a))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; (\<Sum>a\<in>F. cash_reserve (update_ledger \<rho> i \<L> a)) = (\<Sum>a\<in>F. i * sum (\<pi> (\<L> a)) {..shortest_ledger_period \<L>} + cash_reserve (\<L> a))\<rbrakk> \<Longrightarrow> (\<Sum>a\<in>insert x F. cash_reserve (update_ledger \<rho> i \<L> a)) = (\<Sum>a\<in>insert x F. i * sum (\<pi> (\<L> a)) {..shortest_ledger_period \<L>} + cash_reserve (\<L> a))
[PROOF STEP]
case (insert x S)
[PROOF STATE]
proof (state)
this:
finite S
x \<notin> S
(\<Sum>a\<in>S. cash_reserve (update_ledger \<rho> i \<L> a)) = (\<Sum>a\<in>S. i * sum (\<pi> (\<L> a)) {..shortest_ledger_period \<L>} + cash_reserve (\<L> a))

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; (\<Sum>a\<in>F. cash_reserve (update_ledger \<rho> i \<L> a)) = (\<Sum>a\<in>F. i * sum (\<pi> (\<L> a)) {..shortest_ledger_period \<L>} + cash_reserve (\<L> a))\<rbrakk> \<Longrightarrow> (\<Sum>a\<in>insert x F. cash_reserve (update_ledger \<rho> i \<L> a)) = (\<Sum>a\<in>insert x F. i * sum (\<pi> (\<L> a)) {..shortest_ledger_period \<L>} + cash_reserve (\<L> a))
[PROOF STEP]
have "(\<Sum>a\<in>insert x S. cash_reserve (?\<L>' a)) =
              (\<Sum>a\<in>insert x S. i * (\<Sum> n \<le> ?\<omega>. \<pi> (\<L> a) n) +
                    cash_reserve (\<L> a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>a\<in>insert x S. cash_reserve (update_ledger \<rho> i \<L> a)) = (\<Sum>a\<in>insert x S. i * sum (\<pi> (\<L> a)) {..shortest_ledger_period \<L>} + cash_reserve (\<L> a))
[PROOF STEP]
unfolding update_ledger_def update_account_def cash_reserve_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>a\<in>insert x S. \<pi> (just_cash (i * net_asset_value (\<L> a)) + return_loans \<rho> (\<L> a)) 0) = (\<Sum>a\<in>insert x S. i * sum (\<pi> (\<L> a)) {..shortest_ledger_period \<L>} + \<pi> (\<L> a) 0)
[PROOF STEP]
by (simp add: \<open>\<rho> 0 = 0\<close>,
            metis (no_types)
                  shortest_ledger_period_bound
                  net_asset_value_shortest_period_ge)
[PROOF STATE]
proof (state)
this:
(\<Sum>a\<in>insert x S. cash_reserve (update_ledger \<rho> i \<L> a)) = (\<Sum>a\<in>insert x S. i * sum (\<pi> (\<L> a)) {..shortest_ledger_period \<L>} + cash_reserve (\<L> a))

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; (\<Sum>a\<in>F. cash_reserve (update_ledger \<rho> i \<L> a)) = (\<Sum>a\<in>F. i * sum (\<pi> (\<L> a)) {..shortest_ledger_period \<L>} + cash_reserve (\<L> a))\<rbrakk> \<Longrightarrow> (\<Sum>a\<in>insert x F. cash_reserve (update_ledger \<rho> i \<L> a)) = (\<Sum>a\<in>insert x F. i * sum (\<pi> (\<L> a)) {..shortest_ledger_period \<L>} + cash_reserve (\<L> a))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
(\<Sum>a\<in>insert x S. cash_reserve (update_ledger \<rho> i \<L> a)) = (\<Sum>a\<in>insert x S. i * sum (\<pi> (\<L> a)) {..shortest_ledger_period \<L>} + cash_reserve (\<L> a))

goal (1 subgoal):
 1. (\<Sum>a\<in>insert x S. cash_reserve (update_ledger \<rho> i \<L> a)) = (\<Sum>a\<in>insert x S. i * sum (\<pi> (\<L> a)) {..shortest_ledger_period \<L>} + cash_reserve (\<L> a))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(\<Sum>a\<in>insert x S. cash_reserve (update_ledger \<rho> i \<L> a)) = (\<Sum>a\<in>insert x S. i * sum (\<pi> (\<L> a)) {..shortest_ledger_period \<L>} + cash_reserve (\<L> a))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Sum>a\<in>S. cash_reserve (update_ledger \<rho> i \<L> a)) = (\<Sum>a\<in>S. i * sum (\<pi> (\<L> a)) {..shortest_ledger_period \<L>} + cash_reserve (\<L> a))

goal (2 subgoals):
 1. balanced \<L> c \<Longrightarrow> balanced (update_ledger \<rho> i \<L>) ((1 + i) * c)
 2. balanced (update_ledger \<rho> i \<L>) ((1 + i) * c) \<Longrightarrow> balanced \<L> c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>a\<in>S. cash_reserve (update_ledger \<rho> i \<L> a)) = (\<Sum>a\<in>S. i * sum (\<pi> (\<L> a)) {..shortest_ledger_period \<L>} + cash_reserve (\<L> a))

goal (2 subgoals):
 1. balanced \<L> c \<Longrightarrow> balanced (update_ledger \<rho> i \<L>) ((1 + i) * c)
 2. balanced (update_ledger \<rho> i \<L>) ((1 + i) * c) \<Longrightarrow> balanced \<L> c
[PROOF STEP]
have "... = (\<Sum>a\<in>S. i * (\<Sum> n = 1 .. ?\<omega>. \<pi> (\<L> a) n) +
                          i * cash_reserve (\<L> a) + cash_reserve (\<L> a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>a\<in>S. i * sum (\<pi> (\<L> a)) {..shortest_ledger_period \<L>} + cash_reserve (\<L> a)) = (\<Sum>a\<in>S. i * sum (\<pi> (\<L> a)) {1..shortest_ledger_period \<L>} + i * cash_reserve (\<L> a) + cash_reserve (\<L> a))
[PROOF STEP]
unfolding cash_reserve_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>a\<in>S. i * sum (\<pi> (\<L> a)) {..shortest_ledger_period \<L>} + \<pi> (\<L> a) 0) = (\<Sum>a\<in>S. i * sum (\<pi> (\<L> a)) {1..shortest_ledger_period \<L>} + i * \<pi> (\<L> a) 0 + \<pi> (\<L> a) 0)
[PROOF STEP]
by (simp add:
            add.commute
            distrib_left
            sum.atMost_shift
            sum_bounds_lt_plus1)
[PROOF STATE]
proof (state)
this:
(\<Sum>a\<in>S. i * sum (\<pi> (\<L> a)) {..shortest_ledger_period \<L>} + cash_reserve (\<L> a)) = (\<Sum>a\<in>S. i * sum (\<pi> (\<L> a)) {1..shortest_ledger_period \<L>} + i * cash_reserve (\<L> a) + cash_reserve (\<L> a))

goal (2 subgoals):
 1. balanced \<L> c \<Longrightarrow> balanced (update_ledger \<rho> i \<L>) ((1 + i) * c)
 2. balanced (update_ledger \<rho> i \<L>) ((1 + i) * c) \<Longrightarrow> balanced \<L> c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>a\<in>S. i * sum (\<pi> (\<L> a)) {..shortest_ledger_period \<L>} + cash_reserve (\<L> a)) = (\<Sum>a\<in>S. i * sum (\<pi> (\<L> a)) {1..shortest_ledger_period \<L>} + i * cash_reserve (\<L> a) + cash_reserve (\<L> a))

goal (2 subgoals):
 1. balanced \<L> c \<Longrightarrow> balanced (update_ledger \<rho> i \<L>) ((1 + i) * c)
 2. balanced (update_ledger \<rho> i \<L>) ((1 + i) * c) \<Longrightarrow> balanced \<L> c
[PROOF STEP]
have "... = (\<Sum>a\<in>S. i * (\<Sum> n = 1 .. ?\<omega>. \<pi> (\<L> a) n) +
                         (1 + i) * cash_reserve (\<L> a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>a\<in>S. i * sum (\<pi> (\<L> a)) {1..shortest_ledger_period \<L>} + i * cash_reserve (\<L> a) + cash_reserve (\<L> a)) = (\<Sum>a\<in>S. i * sum (\<pi> (\<L> a)) {1..shortest_ledger_period \<L>} + (1 + i) * cash_reserve (\<L> a))
[PROOF STEP]
using finite
[PROOF STATE]
proof (prove)
using this:
finite ?A

goal (1 subgoal):
 1. (\<Sum>a\<in>S. i * sum (\<pi> (\<L> a)) {1..shortest_ledger_period \<L>} + i * cash_reserve (\<L> a) + cash_reserve (\<L> a)) = (\<Sum>a\<in>S. i * sum (\<pi> (\<L> a)) {1..shortest_ledger_period \<L>} + (1 + i) * cash_reserve (\<L> a))
[PROOF STEP]
by (induct S rule: finite_induct, auto, simp add: distrib_right)
[PROOF STATE]
proof (state)
this:
(\<Sum>a\<in>S. i * sum (\<pi> (\<L> a)) {1..shortest_ledger_period \<L>} + i * cash_reserve (\<L> a) + cash_reserve (\<L> a)) = (\<Sum>a\<in>S. i * sum (\<pi> (\<L> a)) {1..shortest_ledger_period \<L>} + (1 + i) * cash_reserve (\<L> a))

goal (2 subgoals):
 1. balanced \<L> c \<Longrightarrow> balanced (update_ledger \<rho> i \<L>) ((1 + i) * c)
 2. balanced (update_ledger \<rho> i \<L>) ((1 + i) * c) \<Longrightarrow> balanced \<L> c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>a\<in>S. i * sum (\<pi> (\<L> a)) {1..shortest_ledger_period \<L>} + i * cash_reserve (\<L> a) + cash_reserve (\<L> a)) = (\<Sum>a\<in>S. i * sum (\<pi> (\<L> a)) {1..shortest_ledger_period \<L>} + (1 + i) * cash_reserve (\<L> a))

goal (2 subgoals):
 1. balanced \<L> c \<Longrightarrow> balanced (update_ledger \<rho> i \<L>) ((1 + i) * c)
 2. balanced (update_ledger \<rho> i \<L>) ((1 + i) * c) \<Longrightarrow> balanced \<L> c
[PROOF STEP]
have "... = i * (\<Sum>a\<in>S. (\<Sum> n = 1 .. ?\<omega>. \<pi> (\<L> a) n)) +
                        (1 + i) * (\<Sum>a\<in>S. cash_reserve (\<L> a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>a\<in>S. i * sum (\<pi> (\<L> a)) {1..shortest_ledger_period \<L>} + (1 + i) * cash_reserve (\<L> a)) = i * (\<Sum>a\<in>S. sum (\<pi> (\<L> a)) {1..shortest_ledger_period \<L>}) + (1 + i) * (\<Sum>a\<in>S. cash_reserve (\<L> a))
[PROOF STEP]
by (simp add: sum.distrib sum_distrib_left)
[PROOF STATE]
proof (state)
this:
(\<Sum>a\<in>S. i * sum (\<pi> (\<L> a)) {1..shortest_ledger_period \<L>} + (1 + i) * cash_reserve (\<L> a)) = i * (\<Sum>a\<in>S. sum (\<pi> (\<L> a)) {1..shortest_ledger_period \<L>}) + (1 + i) * (\<Sum>a\<in>S. cash_reserve (\<L> a))

goal (2 subgoals):
 1. balanced \<L> c \<Longrightarrow> balanced (update_ledger \<rho> i \<L>) ((1 + i) * c)
 2. balanced (update_ledger \<rho> i \<L>) ((1 + i) * c) \<Longrightarrow> balanced \<L> c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>a\<in>S. i * sum (\<pi> (\<L> a)) {1..shortest_ledger_period \<L>} + (1 + i) * cash_reserve (\<L> a)) = i * (\<Sum>a\<in>S. sum (\<pi> (\<L> a)) {1..shortest_ledger_period \<L>}) + (1 + i) * (\<Sum>a\<in>S. cash_reserve (\<L> a))

goal (2 subgoals):
 1. balanced \<L> c \<Longrightarrow> balanced (update_ledger \<rho> i \<L>) ((1 + i) * c)
 2. balanced (update_ledger \<rho> i \<L>) ((1 + i) * c) \<Longrightarrow> balanced \<L> c
[PROOF STEP]
have "... = i * (\<Sum> n = 1 .. ?\<omega>. (\<Sum>a\<in>S. \<pi> (\<L> a) n)) +
                        (1 + i) * c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i * (\<Sum>a\<in>S. sum (\<pi> (\<L> a)) {1..shortest_ledger_period \<L>}) + (1 + i) * (\<Sum>a\<in>S. cash_reserve (\<L> a)) = i * (\<Sum>n = 1..shortest_ledger_period \<L>. \<Sum>a\<in>S. \<pi> (\<L> a) n) + (1 + i) * c
[PROOF STEP]
using \<open>(\<Sum>a\<in>S. cash_reserve (\<L> a)) = c\<close> sum.swap
[PROOF STATE]
proof (prove)
using this:
(\<Sum>a\<in>S. cash_reserve (\<L> a)) = c
(\<Sum>i\<in>?A. sum (?g i) ?B) = (\<Sum>j\<in>?B. \<Sum>i\<in>?A. ?g i j)

goal (1 subgoal):
 1. i * (\<Sum>a\<in>S. sum (\<pi> (\<L> a)) {1..shortest_ledger_period \<L>}) + (1 + i) * (\<Sum>a\<in>S. cash_reserve (\<L> a)) = i * (\<Sum>n = 1..shortest_ledger_period \<L>. \<Sum>a\<in>S. \<pi> (\<L> a) n) + (1 + i) * c
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
i * (\<Sum>a\<in>S. sum (\<pi> (\<L> a)) {1..shortest_ledger_period \<L>}) + (1 + i) * (\<Sum>a\<in>S. cash_reserve (\<L> a)) = i * (\<Sum>n = 1..shortest_ledger_period \<L>. \<Sum>a\<in>S. \<pi> (\<L> a) n) + (1 + i) * c

goal (2 subgoals):
 1. balanced \<L> c \<Longrightarrow> balanced (update_ledger \<rho> i \<L>) ((1 + i) * c)
 2. balanced (update_ledger \<rho> i \<L>) ((1 + i) * c) \<Longrightarrow> balanced \<L> c
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>a\<in>S. cash_reserve (update_ledger \<rho> i \<L> a)) = i * (\<Sum>n = 1..shortest_ledger_period \<L>. \<Sum>a\<in>S. \<pi> (\<L> a) n) + (1 + i) * c
[PROOF STEP]
have "(\<Sum>a\<in>S. cash_reserve (?\<L>' a)) = c * (1 + i)"
[PROOF STATE]
proof (prove)
using this:
(\<Sum>a\<in>S. cash_reserve (update_ledger \<rho> i \<L> a)) = i * (\<Sum>n = 1..shortest_ledger_period \<L>. \<Sum>a\<in>S. \<pi> (\<L> a) n) + (1 + i) * c

goal (1 subgoal):
 1. (\<Sum>a\<in>S. cash_reserve (update_ledger \<rho> i \<L> a)) = c * (1 + i)
[PROOF STEP]
using \<open>\<forall>n>0. (\<Sum>a\<in>S. \<pi> (\<L> a) n) = 0\<close>
[PROOF STATE]
proof (prove)
using this:
(\<Sum>a\<in>S. cash_reserve (update_ledger \<rho> i \<L> a)) = i * (\<Sum>n = 1..shortest_ledger_period \<L>. \<Sum>a\<in>S. \<pi> (\<L> a) n) + (1 + i) * c
\<forall>n>0. (\<Sum>a\<in>S. \<pi> (\<L> a) n) = 0

goal (1 subgoal):
 1. (\<Sum>a\<in>S. cash_reserve (update_ledger \<rho> i \<L> a)) = c * (1 + i)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>a\<in>S. cash_reserve (update_ledger \<rho> i \<L> a)) = c * (1 + i)

goal (2 subgoals):
 1. balanced \<L> c \<Longrightarrow> balanced (update_ledger \<rho> i \<L>) ((1 + i) * c)
 2. balanced (update_ledger \<rho> i \<L>) ((1 + i) * c) \<Longrightarrow> balanced \<L> c
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>(\<Sum>a\<in>?S2. cash_reserve (\<L> a)) = c; \<forall>n>0. (\<Sum>a\<in>?S2. \<pi> (\<L> a) n) = 0\<rbrakk> \<Longrightarrow> (\<Sum>a\<in>?S2. cash_reserve (update_ledger \<rho> i \<L> a)) = c * (1 + i)

goal (2 subgoals):
 1. balanced \<L> c \<Longrightarrow> balanced (update_ledger \<rho> i \<L>) ((1 + i) * c)
 2. balanced (update_ledger \<rho> i \<L>) ((1 + i) * c) \<Longrightarrow> balanced \<L> c
[PROOF STEP]
hence "(\<Sum>a\<in>UNIV. cash_reserve (?\<L>' a)) = c * (1 + i)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(\<Sum>a\<in>?S2. cash_reserve (\<L> a)) = c; \<forall>n>0. (\<Sum>a\<in>?S2. \<pi> (\<L> a) n) = 0\<rbrakk> \<Longrightarrow> (\<Sum>a\<in>?S2. cash_reserve (update_ledger \<rho> i \<L> a)) = c * (1 + i)

goal (1 subgoal):
 1. (\<Sum>a\<in>UNIV. cash_reserve (update_ledger \<rho> i \<L> a)) = c * (1 + i)
[PROOF STEP]
using \<open>balanced \<L> c\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(\<Sum>a\<in>?S2. cash_reserve (\<L> a)) = c; \<forall>n>0. (\<Sum>a\<in>?S2. \<pi> (\<L> a) n) = 0\<rbrakk> \<Longrightarrow> (\<Sum>a\<in>?S2. cash_reserve (update_ledger \<rho> i \<L> a)) = c * (1 + i)
balanced \<L> c

goal (1 subgoal):
 1. (\<Sum>a\<in>UNIV. cash_reserve (update_ledger \<rho> i \<L> a)) = c * (1 + i)
[PROOF STEP]
unfolding balanced_alt_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(\<Sum>a\<in>?S2. cash_reserve (\<L> a)) = c; \<forall>n>0. (\<Sum>a\<in>?S2. \<pi> (\<L> a) n) = 0\<rbrakk> \<Longrightarrow> (\<Sum>a\<in>?S2. cash_reserve (update_ledger \<rho> i \<L> a)) = c * (1 + i)
(\<Sum>a\<in>UNIV. cash_reserve (\<L> a)) = c \<and> (\<forall>n>0. (\<Sum>a\<in>UNIV. \<pi> (\<L> a) n) = 0)

goal (1 subgoal):
 1. (\<Sum>a\<in>UNIV. cash_reserve (update_ledger \<rho> i \<L> a)) = c * (1 + i)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
(\<Sum>a\<in>UNIV. cash_reserve (update_ledger \<rho> i \<L> a)) = c * (1 + i)

goal (2 subgoals):
 1. balanced \<L> c \<Longrightarrow> balanced (update_ledger \<rho> i \<L>) ((1 + i) * c)
 2. balanced (update_ledger \<rho> i \<L>) ((1 + i) * c) \<Longrightarrow> balanced \<L> c
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>n>0. (\<Sum>a\<in>UNIV. \<pi> (update_ledger \<rho> i \<L> a) n) = 0
(\<Sum>a\<in>UNIV. cash_reserve (update_ledger \<rho> i \<L> a)) = c * (1 + i)
[PROOF STEP]
show "balanced ?\<L>' ((1 + i) * c)"
[PROOF STATE]
proof (prove)
using this:
\<forall>n>0. (\<Sum>a\<in>UNIV. \<pi> (update_ledger \<rho> i \<L> a) n) = 0
(\<Sum>a\<in>UNIV. cash_reserve (update_ledger \<rho> i \<L> a)) = c * (1 + i)

goal (1 subgoal):
 1. balanced (update_ledger \<rho> i \<L>) ((1 + i) * c)
[PROOF STEP]
unfolding balanced_alt_def
[PROOF STATE]
proof (prove)
using this:
\<forall>n>0. (\<Sum>a\<in>UNIV. \<pi> (update_ledger \<rho> i \<L> a) n) = 0
(\<Sum>a\<in>UNIV. cash_reserve (update_ledger \<rho> i \<L> a)) = c * (1 + i)

goal (1 subgoal):
 1. (\<Sum>a\<in>UNIV. cash_reserve (update_ledger \<rho> i \<L> a)) = (1 + i) * c \<and> (\<forall>n>0. (\<Sum>a\<in>UNIV. \<pi> (update_ledger \<rho> i \<L> a) n) = 0)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
balanced (update_ledger \<rho> i \<L>) ((1 + i) * c)

goal (1 subgoal):
 1. balanced (update_ledger \<rho> i \<L>) ((1 + i) * c) \<Longrightarrow> balanced \<L> c
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. balanced (update_ledger \<rho> i \<L>) ((1 + i) * c) \<Longrightarrow> balanced \<L> c
[PROOF STEP]
assume "balanced ?\<L>' ((1 + i) * c)"
[PROOF STATE]
proof (state)
this:
balanced (update_ledger \<rho> i \<L>) ((1 + i) * c)

goal (1 subgoal):
 1. balanced (update_ledger \<rho> i \<L>) ((1 + i) * c) \<Longrightarrow> balanced \<L> c
[PROOF STEP]
have \<star>: "\<forall>n>0. (\<Sum>a\<in>UNIV. \<pi> (\<L> a) n) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n>0. (\<Sum>a\<in>UNIV. \<pi> (\<L> a) n) = 0
[PROOF STEP]
proof (rule allI, rule impI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. 0 < n \<Longrightarrow> (\<Sum>a\<in>UNIV. \<pi> (\<L> a) n) = 0
[PROOF STEP]
fix n :: nat
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. 0 < n \<Longrightarrow> (\<Sum>a\<in>UNIV. \<pi> (\<L> a) n) = 0
[PROOF STEP]
assume "n > 0"
[PROOF STATE]
proof (state)
this:
0 < n

goal (1 subgoal):
 1. \<And>n. 0 < n \<Longrightarrow> (\<Sum>a\<in>UNIV. \<pi> (\<L> a) n) = 0
[PROOF STEP]
hence "0 = (\<Sum>a\<in>UNIV. \<pi> (?\<L>' a) n)"
[PROOF STATE]
proof (prove)
using this:
0 < n

goal (1 subgoal):
 1. 0 = (\<Sum>a\<in>UNIV. \<pi> (update_ledger \<rho> i \<L> a) n)
[PROOF STEP]
using \<open>balanced ?\<L>' ((1 + i) * c)\<close>
[PROOF STATE]
proof (prove)
using this:
0 < n
balanced (update_ledger \<rho> i \<L>) ((1 + i) * c)

goal (1 subgoal):
 1. 0 = (\<Sum>a\<in>UNIV. \<pi> (update_ledger \<rho> i \<L> a) n)
[PROOF STEP]
unfolding balanced_alt_def
[PROOF STATE]
proof (prove)
using this:
0 < n
(\<Sum>a\<in>UNIV. cash_reserve (update_ledger \<rho> i \<L> a)) = (1 + i) * c \<and> (\<forall>n>0. (\<Sum>a\<in>UNIV. \<pi> (update_ledger \<rho> i \<L> a) n) = 0)

goal (1 subgoal):
 1. 0 = (\<Sum>a\<in>UNIV. \<pi> (update_ledger \<rho> i \<L> a) n)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 = (\<Sum>a\<in>UNIV. \<pi> (update_ledger \<rho> i \<L> a) n)

goal (1 subgoal):
 1. \<And>n. 0 < n \<Longrightarrow> (\<Sum>a\<in>UNIV. \<pi> (\<L> a) n) = 0
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
0 = (\<Sum>a\<in>UNIV. \<pi> (update_ledger \<rho> i \<L> a) n)

goal (1 subgoal):
 1. \<And>n. 0 < n \<Longrightarrow> (\<Sum>a\<in>UNIV. \<pi> (\<L> a) n) = 0
[PROOF STEP]
have "\<dots> = (\<Sum>a\<in>UNIV. (1 - \<rho> n) * \<pi> (\<L> a) n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>a\<in>UNIV. \<pi> (update_ledger \<rho> i \<L> a) n) = (\<Sum>a\<in>UNIV. (1 - \<rho> n) * \<pi> (\<L> a) n)
[PROOF STEP]
unfolding
        update_ledger_def
        update_account_def
        Rep_account_return_loans
        Rep_account_just_cash
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>a\<in>UNIV. \<pi> (just_cash (i * net_asset_value (\<L> a)) + return_loans \<rho> (\<L> a)) n) = (\<Sum>a\<in>UNIV. (1 - \<rho> n) * \<pi> (\<L> a) n)
[PROOF STEP]
using \<open>n > 0\<close>
[PROOF STATE]
proof (prove)
using this:
0 < n

goal (1 subgoal):
 1. (\<Sum>a\<in>UNIV. \<pi> (just_cash (i * net_asset_value (\<L> a)) + return_loans \<rho> (\<L> a)) n) = (\<Sum>a\<in>UNIV. (1 - \<rho> n) * \<pi> (\<L> a) n)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>a\<in>UNIV. \<pi> (update_ledger \<rho> i \<L> a) n) = (\<Sum>a\<in>UNIV. (1 - \<rho> n) * \<pi> (\<L> a) n)

goal (1 subgoal):
 1. \<And>n. 0 < n \<Longrightarrow> (\<Sum>a\<in>UNIV. \<pi> (\<L> a) n) = 0
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>a\<in>UNIV. \<pi> (update_ledger \<rho> i \<L> a) n) = (\<Sum>a\<in>UNIV. (1 - \<rho> n) * \<pi> (\<L> a) n)

goal (1 subgoal):
 1. \<And>n. 0 < n \<Longrightarrow> (\<Sum>a\<in>UNIV. \<pi> (\<L> a) n) = 0
[PROOF STEP]
have "\<dots> = (1 - \<rho> n) * (\<Sum>a\<in>UNIV. \<pi> (\<L> a) n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>a\<in>UNIV. (1 - \<rho> n) * \<pi> (\<L> a) n) = (1 - \<rho> n) * (\<Sum>a\<in>UNIV. \<pi> (\<L> a) n)
[PROOF STEP]
by (simp add: sum_distrib_left)
[PROOF STATE]
proof (state)
this:
(\<Sum>a\<in>UNIV. (1 - \<rho> n) * \<pi> (\<L> a) n) = (1 - \<rho> n) * (\<Sum>a\<in>UNIV. \<pi> (\<L> a) n)

goal (1 subgoal):
 1. \<And>n. 0 < n \<Longrightarrow> (\<Sum>a\<in>UNIV. \<pi> (\<L> a) n) = 0
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
0 = (1 - \<rho> n) * (\<Sum>a\<in>UNIV. \<pi> (\<L> a) n)
[PROOF STEP]
show "(\<Sum>a\<in>UNIV. \<pi> (\<L> a) n) = 0"
[PROOF STATE]
proof (prove)
using this:
0 = (1 - \<rho> n) * (\<Sum>a\<in>UNIV. \<pi> (\<L> a) n)

goal (1 subgoal):
 1. (\<Sum>a\<in>UNIV. \<pi> (\<L> a) n) = 0
[PROOF STEP]
by (metis
            \<open>\<forall> r . \<rho> r < 1\<close>
            diff_gt_0_iff_gt
            less_numeral_extra(3)
            mult_eq_0_iff)
[PROOF STATE]
proof (state)
this:
(\<Sum>a\<in>UNIV. \<pi> (\<L> a) n) = 0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>n>0. (\<Sum>a\<in>UNIV. \<pi> (\<L> a) n) = 0

goal (1 subgoal):
 1. balanced (update_ledger \<rho> i \<L>) ((1 + i) * c) \<Longrightarrow> balanced \<L> c
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>n>0. (\<Sum>a\<in>UNIV. \<pi> (\<L> a) n) = 0

goal (1 subgoal):
 1. balanced (update_ledger \<rho> i \<L>) ((1 + i) * c) \<Longrightarrow> balanced \<L> c
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<forall>n>0. (\<Sum>a\<in>UNIV. \<pi> (\<L> a) n) = 0

goal (1 subgoal):
 1. balanced (update_ledger \<rho> i \<L>) ((1 + i) * c) \<Longrightarrow> balanced \<L> c
[PROOF STEP]
fix S :: "'a set"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. balanced (update_ledger \<rho> i \<L>) ((1 + i) * c) \<Longrightarrow> balanced \<L> c
[PROOF STEP]
let ?\<omega> = "shortest_ledger_period \<L>"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. balanced (update_ledger \<rho> i \<L>) ((1 + i) * c) \<Longrightarrow> balanced \<L> c
[PROOF STEP]
assume "(\<Sum>a\<in>S. cash_reserve (?\<L>' a)) = (1 + i) * c"
    and "\<forall>n>0. (\<Sum>a\<in>S. \<pi> (\<L> a) n) = 0"
[PROOF STATE]
proof (state)
this:
(\<Sum>a\<in>S. cash_reserve (update_ledger \<rho> i \<L> a)) = (1 + i) * c
\<forall>n>0. (\<Sum>a\<in>S. \<pi> (\<L> a) n) = 0

goal (1 subgoal):
 1. balanced (update_ledger \<rho> i \<L>) ((1 + i) * c) \<Longrightarrow> balanced \<L> c
[PROOF STEP]
hence "(1 + i) * c = (\<Sum>a\<in>S. cash_reserve (?\<L>' a))"
[PROOF STATE]
proof (prove)
using this:
(\<Sum>a\<in>S. cash_reserve (update_ledger \<rho> i \<L> a)) = (1 + i) * c
\<forall>n>0. (\<Sum>a\<in>S. \<pi> (\<L> a) n) = 0

goal (1 subgoal):
 1. (1 + i) * c = (\<Sum>a\<in>S. cash_reserve (update_ledger \<rho> i \<L> a))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(1 + i) * c = (\<Sum>a\<in>S. cash_reserve (update_ledger \<rho> i \<L> a))

goal (1 subgoal):
 1. balanced (update_ledger \<rho> i \<L>) ((1 + i) * c) \<Longrightarrow> balanced \<L> c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(1 + i) * c = (\<Sum>a\<in>S. cash_reserve (update_ledger \<rho> i \<L> a))

goal (1 subgoal):
 1. balanced (update_ledger \<rho> i \<L>) ((1 + i) * c) \<Longrightarrow> balanced \<L> c
[PROOF STEP]
have "\<dots> = (\<Sum>a\<in>S. i * (\<Sum> n \<le> ?\<omega>. \<pi> (\<L> a) n) +
                         cash_reserve (\<L> a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>a\<in>S. cash_reserve (update_ledger \<rho> i \<L> a)) = (\<Sum>a\<in>S. i * sum (\<pi> (\<L> a)) {..shortest_ledger_period \<L>} + cash_reserve (\<L> a))
[PROOF STEP]
using finite
[PROOF STATE]
proof (prove)
using this:
finite ?A

goal (1 subgoal):
 1. (\<Sum>a\<in>S. cash_reserve (update_ledger \<rho> i \<L> a)) = (\<Sum>a\<in>S. i * sum (\<pi> (\<L> a)) {..shortest_ledger_period \<L>} + cash_reserve (\<L> a))
[PROOF STEP]
proof (induct S rule: finite_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<Sum>a\<in>{}. cash_reserve (update_ledger \<rho> i \<L> a)) = (\<Sum>a\<in>{}. i * sum (\<pi> (\<L> a)) {..shortest_ledger_period \<L>} + cash_reserve (\<L> a))
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; (\<Sum>a\<in>F. cash_reserve (update_ledger \<rho> i \<L> a)) = (\<Sum>a\<in>F. i * sum (\<pi> (\<L> a)) {..shortest_ledger_period \<L>} + cash_reserve (\<L> a))\<rbrakk> \<Longrightarrow> (\<Sum>a\<in>insert x F. cash_reserve (update_ledger \<rho> i \<L> a)) = (\<Sum>a\<in>insert x F. i * sum (\<pi> (\<L> a)) {..shortest_ledger_period \<L>} + cash_reserve (\<L> a))
[PROOF STEP]
case empty
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. (\<Sum>a\<in>{}. cash_reserve (update_ledger \<rho> i \<L> a)) = (\<Sum>a\<in>{}. i * sum (\<pi> (\<L> a)) {..shortest_ledger_period \<L>} + cash_reserve (\<L> a))
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; (\<Sum>a\<in>F. cash_reserve (update_ledger \<rho> i \<L> a)) = (\<Sum>a\<in>F. i * sum (\<pi> (\<L> a)) {..shortest_ledger_period \<L>} + cash_reserve (\<L> a))\<rbrakk> \<Longrightarrow> (\<Sum>a\<in>insert x F. cash_reserve (update_ledger \<rho> i \<L> a)) = (\<Sum>a\<in>insert x F. i * sum (\<pi> (\<L> a)) {..shortest_ledger_period \<L>} + cash_reserve (\<L> a))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>a\<in>{}. cash_reserve (update_ledger \<rho> i \<L> a)) = (\<Sum>a\<in>{}. i * sum (\<pi> (\<L> a)) {..shortest_ledger_period \<L>} + cash_reserve (\<L> a))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>a\<in>{}. cash_reserve (update_ledger \<rho> i \<L> a)) = (\<Sum>a\<in>{}. i * sum (\<pi> (\<L> a)) {..shortest_ledger_period \<L>} + cash_reserve (\<L> a))

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; (\<Sum>a\<in>F. cash_reserve (update_ledger \<rho> i \<L> a)) = (\<Sum>a\<in>F. i * sum (\<pi> (\<L> a)) {..shortest_ledger_period \<L>} + cash_reserve (\<L> a))\<rbrakk> \<Longrightarrow> (\<Sum>a\<in>insert x F. cash_reserve (update_ledger \<rho> i \<L> a)) = (\<Sum>a\<in>insert x F. i * sum (\<pi> (\<L> a)) {..shortest_ledger_period \<L>} + cash_reserve (\<L> a))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; (\<Sum>a\<in>F. cash_reserve (update_ledger \<rho> i \<L> a)) = (\<Sum>a\<in>F. i * sum (\<pi> (\<L> a)) {..shortest_ledger_period \<L>} + cash_reserve (\<L> a))\<rbrakk> \<Longrightarrow> (\<Sum>a\<in>insert x F. cash_reserve (update_ledger \<rho> i \<L> a)) = (\<Sum>a\<in>insert x F. i * sum (\<pi> (\<L> a)) {..shortest_ledger_period \<L>} + cash_reserve (\<L> a))
[PROOF STEP]
case (insert x S)
[PROOF STATE]
proof (state)
this:
finite S
x \<notin> S
(\<Sum>a\<in>S. cash_reserve (update_ledger \<rho> i \<L> a)) = (\<Sum>a\<in>S. i * sum (\<pi> (\<L> a)) {..shortest_ledger_period \<L>} + cash_reserve (\<L> a))

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; (\<Sum>a\<in>F. cash_reserve (update_ledger \<rho> i \<L> a)) = (\<Sum>a\<in>F. i * sum (\<pi> (\<L> a)) {..shortest_ledger_period \<L>} + cash_reserve (\<L> a))\<rbrakk> \<Longrightarrow> (\<Sum>a\<in>insert x F. cash_reserve (update_ledger \<rho> i \<L> a)) = (\<Sum>a\<in>insert x F. i * sum (\<pi> (\<L> a)) {..shortest_ledger_period \<L>} + cash_reserve (\<L> a))
[PROOF STEP]
have "(\<Sum>a\<in>insert x S. cash_reserve (?\<L>' a)) =
              (\<Sum>a\<in>insert x S.
                  i * (\<Sum> n \<le> ?\<omega>. \<pi> (\<L> a) n) + cash_reserve (\<L> a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>a\<in>insert x S. cash_reserve (update_ledger \<rho> i \<L> a)) = (\<Sum>a\<in>insert x S. i * sum (\<pi> (\<L> a)) {..shortest_ledger_period \<L>} + cash_reserve (\<L> a))
[PROOF STEP]
unfolding update_ledger_def update_account_def cash_reserve_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>a\<in>insert x S. \<pi> (just_cash (i * net_asset_value (\<L> a)) + return_loans \<rho> (\<L> a)) 0) = (\<Sum>a\<in>insert x S. i * sum (\<pi> (\<L> a)) {..shortest_ledger_period \<L>} + \<pi> (\<L> a) 0)
[PROOF STEP]
by (simp add: \<open>\<rho> 0 = 0\<close>,
            metis (no_types)
                  shortest_ledger_period_bound
                  net_asset_value_shortest_period_ge)
[PROOF STATE]
proof (state)
this:
(\<Sum>a\<in>insert x S. cash_reserve (update_ledger \<rho> i \<L> a)) = (\<Sum>a\<in>insert x S. i * sum (\<pi> (\<L> a)) {..shortest_ledger_period \<L>} + cash_reserve (\<L> a))

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; (\<Sum>a\<in>F. cash_reserve (update_ledger \<rho> i \<L> a)) = (\<Sum>a\<in>F. i * sum (\<pi> (\<L> a)) {..shortest_ledger_period \<L>} + cash_reserve (\<L> a))\<rbrakk> \<Longrightarrow> (\<Sum>a\<in>insert x F. cash_reserve (update_ledger \<rho> i \<L> a)) = (\<Sum>a\<in>insert x F. i * sum (\<pi> (\<L> a)) {..shortest_ledger_period \<L>} + cash_reserve (\<L> a))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
(\<Sum>a\<in>insert x S. cash_reserve (update_ledger \<rho> i \<L> a)) = (\<Sum>a\<in>insert x S. i * sum (\<pi> (\<L> a)) {..shortest_ledger_period \<L>} + cash_reserve (\<L> a))

goal (1 subgoal):
 1. (\<Sum>a\<in>insert x S. cash_reserve (update_ledger \<rho> i \<L> a)) = (\<Sum>a\<in>insert x S. i * sum (\<pi> (\<L> a)) {..shortest_ledger_period \<L>} + cash_reserve (\<L> a))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(\<Sum>a\<in>insert x S. cash_reserve (update_ledger \<rho> i \<L> a)) = (\<Sum>a\<in>insert x S. i * sum (\<pi> (\<L> a)) {..shortest_ledger_period \<L>} + cash_reserve (\<L> a))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Sum>a\<in>S. cash_reserve (update_ledger \<rho> i \<L> a)) = (\<Sum>a\<in>S. i * sum (\<pi> (\<L> a)) {..shortest_ledger_period \<L>} + cash_reserve (\<L> a))

goal (1 subgoal):
 1. balanced (update_ledger \<rho> i \<L>) ((1 + i) * c) \<Longrightarrow> balanced \<L> c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>a\<in>S. cash_reserve (update_ledger \<rho> i \<L> a)) = (\<Sum>a\<in>S. i * sum (\<pi> (\<L> a)) {..shortest_ledger_period \<L>} + cash_reserve (\<L> a))

goal (1 subgoal):
 1. balanced (update_ledger \<rho> i \<L>) ((1 + i) * c) \<Longrightarrow> balanced \<L> c
[PROOF STEP]
have "\<dots> = (\<Sum>a\<in>S. i * (\<Sum> n = 1 .. ?\<omega>. \<pi> (\<L> a) n) +
                               i * cash_reserve (\<L> a) + cash_reserve (\<L> a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>a\<in>S. i * sum (\<pi> (\<L> a)) {..shortest_ledger_period \<L>} + cash_reserve (\<L> a)) = (\<Sum>a\<in>S. i * sum (\<pi> (\<L> a)) {1..shortest_ledger_period \<L>} + i * cash_reserve (\<L> a) + cash_reserve (\<L> a))
[PROOF STEP]
unfolding cash_reserve_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>a\<in>S. i * sum (\<pi> (\<L> a)) {..shortest_ledger_period \<L>} + \<pi> (\<L> a) 0) = (\<Sum>a\<in>S. i * sum (\<pi> (\<L> a)) {1..shortest_ledger_period \<L>} + i * \<pi> (\<L> a) 0 + \<pi> (\<L> a) 0)
[PROOF STEP]
by (simp add:
            add.commute
            distrib_left
            sum.atMost_shift
            sum_bounds_lt_plus1)
[PROOF STATE]
proof (state)
this:
(\<Sum>a\<in>S. i * sum (\<pi> (\<L> a)) {..shortest_ledger_period \<L>} + cash_reserve (\<L> a)) = (\<Sum>a\<in>S. i * sum (\<pi> (\<L> a)) {1..shortest_ledger_period \<L>} + i * cash_reserve (\<L> a) + cash_reserve (\<L> a))

goal (1 subgoal):
 1. balanced (update_ledger \<rho> i \<L>) ((1 + i) * c) \<Longrightarrow> balanced \<L> c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>a\<in>S. i * sum (\<pi> (\<L> a)) {..shortest_ledger_period \<L>} + cash_reserve (\<L> a)) = (\<Sum>a\<in>S. i * sum (\<pi> (\<L> a)) {1..shortest_ledger_period \<L>} + i * cash_reserve (\<L> a) + cash_reserve (\<L> a))

goal (1 subgoal):
 1. balanced (update_ledger \<rho> i \<L>) ((1 + i) * c) \<Longrightarrow> balanced \<L> c
[PROOF STEP]
have "\<dots> = (\<Sum>a\<in>S. i * (\<Sum> n = 1 .. ?\<omega>. \<pi> (\<L> a) n) +
                           (1 + i) * cash_reserve (\<L> a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>a\<in>S. i * sum (\<pi> (\<L> a)) {1..shortest_ledger_period \<L>} + i * cash_reserve (\<L> a) + cash_reserve (\<L> a)) = (\<Sum>a\<in>S. i * sum (\<pi> (\<L> a)) {1..shortest_ledger_period \<L>} + (1 + i) * cash_reserve (\<L> a))
[PROOF STEP]
using finite
[PROOF STATE]
proof (prove)
using this:
finite ?A

goal (1 subgoal):
 1. (\<Sum>a\<in>S. i * sum (\<pi> (\<L> a)) {1..shortest_ledger_period \<L>} + i * cash_reserve (\<L> a) + cash_reserve (\<L> a)) = (\<Sum>a\<in>S. i * sum (\<pi> (\<L> a)) {1..shortest_ledger_period \<L>} + (1 + i) * cash_reserve (\<L> a))
[PROOF STEP]
by (induct S rule: finite_induct, auto, simp add: distrib_right)
[PROOF STATE]
proof (state)
this:
(\<Sum>a\<in>S. i * sum (\<pi> (\<L> a)) {1..shortest_ledger_period \<L>} + i * cash_reserve (\<L> a) + cash_reserve (\<L> a)) = (\<Sum>a\<in>S. i * sum (\<pi> (\<L> a)) {1..shortest_ledger_period \<L>} + (1 + i) * cash_reserve (\<L> a))

goal (1 subgoal):
 1. balanced (update_ledger \<rho> i \<L>) ((1 + i) * c) \<Longrightarrow> balanced \<L> c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>a\<in>S. i * sum (\<pi> (\<L> a)) {1..shortest_ledger_period \<L>} + i * cash_reserve (\<L> a) + cash_reserve (\<L> a)) = (\<Sum>a\<in>S. i * sum (\<pi> (\<L> a)) {1..shortest_ledger_period \<L>} + (1 + i) * cash_reserve (\<L> a))

goal (1 subgoal):
 1. balanced (update_ledger \<rho> i \<L>) ((1 + i) * c) \<Longrightarrow> balanced \<L> c
[PROOF STEP]
have "\<dots> = i * (\<Sum>a\<in>S. (\<Sum> n = 1 .. ?\<omega>. \<pi> (\<L> a) n)) +
                        (1 + i) * (\<Sum>a\<in>S. cash_reserve (\<L> a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>a\<in>S. i * sum (\<pi> (\<L> a)) {1..shortest_ledger_period \<L>} + (1 + i) * cash_reserve (\<L> a)) = i * (\<Sum>a\<in>S. sum (\<pi> (\<L> a)) {1..shortest_ledger_period \<L>}) + (1 + i) * (\<Sum>a\<in>S. cash_reserve (\<L> a))
[PROOF STEP]
by (simp add: sum.distrib sum_distrib_left)
[PROOF STATE]
proof (state)
this:
(\<Sum>a\<in>S. i * sum (\<pi> (\<L> a)) {1..shortest_ledger_period \<L>} + (1 + i) * cash_reserve (\<L> a)) = i * (\<Sum>a\<in>S. sum (\<pi> (\<L> a)) {1..shortest_ledger_period \<L>}) + (1 + i) * (\<Sum>a\<in>S. cash_reserve (\<L> a))

goal (1 subgoal):
 1. balanced (update_ledger \<rho> i \<L>) ((1 + i) * c) \<Longrightarrow> balanced \<L> c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>a\<in>S. i * sum (\<pi> (\<L> a)) {1..shortest_ledger_period \<L>} + (1 + i) * cash_reserve (\<L> a)) = i * (\<Sum>a\<in>S. sum (\<pi> (\<L> a)) {1..shortest_ledger_period \<L>}) + (1 + i) * (\<Sum>a\<in>S. cash_reserve (\<L> a))

goal (1 subgoal):
 1. balanced (update_ledger \<rho> i \<L>) ((1 + i) * c) \<Longrightarrow> balanced \<L> c
[PROOF STEP]
have "\<dots> =  i * (\<Sum> n = 1 .. ?\<omega>. (\<Sum>a\<in>S. \<pi> (\<L> a) n)) +
                       (1 + i) * (\<Sum>a\<in>S. cash_reserve (\<L> a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i * (\<Sum>a\<in>S. sum (\<pi> (\<L> a)) {1..shortest_ledger_period \<L>}) + (1 + i) * (\<Sum>a\<in>S. cash_reserve (\<L> a)) = i * (\<Sum>n = 1..shortest_ledger_period \<L>. \<Sum>a\<in>S. \<pi> (\<L> a) n) + (1 + i) * (\<Sum>a\<in>S. cash_reserve (\<L> a))
[PROOF STEP]
using sum.swap
[PROOF STATE]
proof (prove)
using this:
(\<Sum>i\<in>?A. sum (?g i) ?B) = (\<Sum>j\<in>?B. \<Sum>i\<in>?A. ?g i j)

goal (1 subgoal):
 1. i * (\<Sum>a\<in>S. sum (\<pi> (\<L> a)) {1..shortest_ledger_period \<L>}) + (1 + i) * (\<Sum>a\<in>S. cash_reserve (\<L> a)) = i * (\<Sum>n = 1..shortest_ledger_period \<L>. \<Sum>a\<in>S. \<pi> (\<L> a) n) + (1 + i) * (\<Sum>a\<in>S. cash_reserve (\<L> a))
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
i * (\<Sum>a\<in>S. sum (\<pi> (\<L> a)) {1..shortest_ledger_period \<L>}) + (1 + i) * (\<Sum>a\<in>S. cash_reserve (\<L> a)) = i * (\<Sum>n = 1..shortest_ledger_period \<L>. \<Sum>a\<in>S. \<pi> (\<L> a) n) + (1 + i) * (\<Sum>a\<in>S. cash_reserve (\<L> a))

goal (1 subgoal):
 1. balanced (update_ledger \<rho> i \<L>) ((1 + i) * c) \<Longrightarrow> balanced \<L> c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
i * (\<Sum>a\<in>S. sum (\<pi> (\<L> a)) {1..shortest_ledger_period \<L>}) + (1 + i) * (\<Sum>a\<in>S. cash_reserve (\<L> a)) = i * (\<Sum>n = 1..shortest_ledger_period \<L>. \<Sum>a\<in>S. \<pi> (\<L> a) n) + (1 + i) * (\<Sum>a\<in>S. cash_reserve (\<L> a))

goal (1 subgoal):
 1. balanced (update_ledger \<rho> i \<L>) ((1 + i) * c) \<Longrightarrow> balanced \<L> c
[PROOF STEP]
have "\<dots> = (1 + i) * (\<Sum>a\<in>S. cash_reserve (\<L> a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i * (\<Sum>n = 1..shortest_ledger_period \<L>. \<Sum>a\<in>S. \<pi> (\<L> a) n) + (1 + i) * (\<Sum>a\<in>S. cash_reserve (\<L> a)) = (1 + i) * (\<Sum>a\<in>S. cash_reserve (\<L> a))
[PROOF STEP]
using \<open>\<forall>n>0. (\<Sum>a\<in>S. \<pi> (\<L> a) n) = 0\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>n>0. (\<Sum>a\<in>S. \<pi> (\<L> a) n) = 0

goal (1 subgoal):
 1. i * (\<Sum>n = 1..shortest_ledger_period \<L>. \<Sum>a\<in>S. \<pi> (\<L> a) n) + (1 + i) * (\<Sum>a\<in>S. cash_reserve (\<L> a)) = (1 + i) * (\<Sum>a\<in>S. cash_reserve (\<L> a))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
i * (\<Sum>n = 1..shortest_ledger_period \<L>. \<Sum>a\<in>S. \<pi> (\<L> a) n) + (1 + i) * (\<Sum>a\<in>S. cash_reserve (\<L> a)) = (1 + i) * (\<Sum>a\<in>S. cash_reserve (\<L> a))

goal (1 subgoal):
 1. balanced (update_ledger \<rho> i \<L>) ((1 + i) * c) \<Longrightarrow> balanced \<L> c
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(1 + i) * c = (1 + i) * (\<Sum>a\<in>S. cash_reserve (\<L> a))
[PROOF STEP]
have "c = (\<Sum>a\<in>S. cash_reserve (\<L> a))"
[PROOF STATE]
proof (prove)
using this:
(1 + i) * c = (1 + i) * (\<Sum>a\<in>S. cash_reserve (\<L> a))

goal (1 subgoal):
 1. c = (\<Sum>a\<in>S. cash_reserve (\<L> a))
[PROOF STEP]
using \<open>0 \<le> i\<close>
[PROOF STATE]
proof (prove)
using this:
(1 + i) * c = (1 + i) * (\<Sum>a\<in>S. cash_reserve (\<L> a))
0 \<le> i

goal (1 subgoal):
 1. c = (\<Sum>a\<in>S. cash_reserve (\<L> a))
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
c = (\<Sum>a\<in>S. cash_reserve (\<L> a))

goal (1 subgoal):
 1. balanced (update_ledger \<rho> i \<L>) ((1 + i) * c) \<Longrightarrow> balanced \<L> c
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>(\<Sum>a\<in>?S2. cash_reserve (update_ledger \<rho> i \<L> a)) = (1 + i) * c; \<forall>n>0. (\<Sum>a\<in>?S2. \<pi> (\<L> a) n) = 0\<rbrakk> \<Longrightarrow> c = (\<Sum>a\<in>?S2. cash_reserve (\<L> a))

goal (1 subgoal):
 1. balanced (update_ledger \<rho> i \<L>) ((1 + i) * c) \<Longrightarrow> balanced \<L> c
[PROOF STEP]
hence "(\<Sum>a\<in>UNIV. cash_reserve (\<L> a)) = c"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(\<Sum>a\<in>?S2. cash_reserve (update_ledger \<rho> i \<L> a)) = (1 + i) * c; \<forall>n>0. (\<Sum>a\<in>?S2. \<pi> (\<L> a) n) = 0\<rbrakk> \<Longrightarrow> c = (\<Sum>a\<in>?S2. cash_reserve (\<L> a))

goal (1 subgoal):
 1. (\<Sum>a\<in>UNIV. cash_reserve (\<L> a)) = c
[PROOF STEP]
unfolding cash_reserve_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(\<Sum>a\<in>?S2. \<pi> (update_ledger \<rho> i \<L> a) 0) = (1 + i) * c; \<forall>n>0. (\<Sum>a\<in>?S2. \<pi> (\<L> a) n) = 0\<rbrakk> \<Longrightarrow> c = (\<Sum>a\<in>?S2. \<pi> (\<L> a) 0)

goal (1 subgoal):
 1. (\<Sum>a\<in>UNIV. \<pi> (\<L> a) 0) = c
[PROOF STEP]
by (metis
          Rep_account_just_cash
          \<open>balanced ?\<L>' ((1 + i) * c)\<close>
          \<star>
          balanced_def
          finite_Rep_account_ledger)
[PROOF STATE]
proof (state)
this:
(\<Sum>a\<in>UNIV. cash_reserve (\<L> a)) = c

goal (1 subgoal):
 1. balanced (update_ledger \<rho> i \<L>) ((1 + i) * c) \<Longrightarrow> balanced \<L> c
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>n>0. (\<Sum>a\<in>UNIV. \<pi> (\<L> a) n) = 0
(\<Sum>a\<in>UNIV. cash_reserve (\<L> a)) = c
[PROOF STEP]
show "balanced \<L> c"
[PROOF STATE]
proof (prove)
using this:
\<forall>n>0. (\<Sum>a\<in>UNIV. \<pi> (\<L> a) n) = 0
(\<Sum>a\<in>UNIV. cash_reserve (\<L> a)) = c

goal (1 subgoal):
 1. balanced \<L> c
[PROOF STEP]
unfolding balanced_alt_def
[PROOF STATE]
proof (prove)
using this:
\<forall>n>0. (\<Sum>a\<in>UNIV. \<pi> (\<L> a) n) = 0
(\<Sum>a\<in>UNIV. cash_reserve (\<L> a)) = c

goal (1 subgoal):
 1. (\<Sum>a\<in>UNIV. cash_reserve (\<L> a)) = c \<and> (\<forall>n>0. (\<Sum>a\<in>UNIV. \<pi> (\<L> a) n) = 0)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
balanced \<L> c

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma return_loans_plus:
  "return_loans \<rho> (\<alpha> + \<beta>) = return_loans \<rho> \<alpha> + return_loans \<rho> \<beta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. return_loans \<rho> (\<alpha> + \<beta>) = return_loans \<rho> \<alpha> + return_loans \<rho> \<beta>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. return_loans \<rho> (\<alpha> + \<beta>) = return_loans \<rho> \<alpha> + return_loans \<rho> \<beta>
[PROOF STEP]
let ?\<alpha> = "\<pi> \<alpha>"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. return_loans \<rho> (\<alpha> + \<beta>) = return_loans \<rho> \<alpha> + return_loans \<rho> \<beta>
[PROOF STEP]
let ?\<beta> = "\<pi> \<beta>"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. return_loans \<rho> (\<alpha> + \<beta>) = return_loans \<rho> \<alpha> + return_loans \<rho> \<beta>
[PROOF STEP]
let ?\<rho>\<alpha>\<beta> = "\<lambda>n. (1 - \<rho> n) * (?\<alpha> n + ?\<beta> n)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. return_loans \<rho> (\<alpha> + \<beta>) = return_loans \<rho> \<alpha> + return_loans \<rho> \<beta>
[PROOF STEP]
let ?\<rho>\<alpha> = "\<lambda>n. (1 - \<rho> n) * ?\<alpha> n"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. return_loans \<rho> (\<alpha> + \<beta>) = return_loans \<rho> \<alpha> + return_loans \<rho> \<beta>
[PROOF STEP]
let ?\<rho>\<beta> = "\<lambda>n. (1 - \<rho> n) * ?\<beta> n"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. return_loans \<rho> (\<alpha> + \<beta>) = return_loans \<rho> \<alpha> + return_loans \<rho> \<beta>
[PROOF STEP]
have "support 0 UNIV ?\<rho>\<alpha> \<subseteq> support 0 UNIV ?\<alpha>"
       "support 0 UNIV ?\<rho>\<beta> \<subseteq> support 0 UNIV ?\<beta>"
       "support 0 UNIV ?\<rho>\<alpha>\<beta> \<subseteq> support 0 UNIV ?\<alpha> \<union> support 0 UNIV ?\<beta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. support 0 UNIV (\<lambda>n. (1 - \<rho> n) * \<pi> \<alpha> n) \<subseteq> support 0 UNIV (\<pi> \<alpha>) &&& support 0 UNIV (\<lambda>n. (1 - \<rho> n) * \<pi> \<beta> n) \<subseteq> support 0 UNIV (\<pi> \<beta>) &&& support 0 UNIV (\<lambda>n. (1 - \<rho> n) * (\<pi> \<alpha> n + \<pi> \<beta> n)) \<subseteq> support 0 UNIV (\<pi> \<alpha>) \<union> support 0 UNIV (\<pi> \<beta>)
[PROOF STEP]
unfolding support_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x \<in> UNIV. (1 - \<rho> x) * \<pi> \<alpha> x \<noteq> 0} \<subseteq> {x \<in> UNIV. \<pi> \<alpha> x \<noteq> 0} &&& {x \<in> UNIV. (1 - \<rho> x) * \<pi> \<beta> x \<noteq> 0} \<subseteq> {x \<in> UNIV. \<pi> \<beta> x \<noteq> 0} &&& {x \<in> UNIV. (1 - \<rho> x) * (\<pi> \<alpha> x + \<pi> \<beta> x) \<noteq> 0} \<subseteq> {x \<in> UNIV. \<pi> \<alpha> x \<noteq> 0} \<union> {x \<in> UNIV. \<pi> \<beta> x \<noteq> 0}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
support 0 UNIV (\<lambda>n. (1 - \<rho> n) * \<pi> \<alpha> n) \<subseteq> support 0 UNIV (\<pi> \<alpha>)
support 0 UNIV (\<lambda>n. (1 - \<rho> n) * \<pi> \<beta> n) \<subseteq> support 0 UNIV (\<pi> \<beta>)
support 0 UNIV (\<lambda>n. (1 - \<rho> n) * (\<pi> \<alpha> n + \<pi> \<beta> n)) \<subseteq> support 0 UNIV (\<pi> \<alpha>) \<union> support 0 UNIV (\<pi> \<beta>)

goal (1 subgoal):
 1. return_loans \<rho> (\<alpha> + \<beta>) = return_loans \<rho> \<alpha> + return_loans \<rho> \<beta>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
support 0 UNIV (\<lambda>n. (1 - \<rho> n) * \<pi> \<alpha> n) \<subseteq> support 0 UNIV (\<pi> \<alpha>)
support 0 UNIV (\<lambda>n. (1 - \<rho> n) * \<pi> \<beta> n) \<subseteq> support 0 UNIV (\<pi> \<beta>)
support 0 UNIV (\<lambda>n. (1 - \<rho> n) * (\<pi> \<alpha> n + \<pi> \<beta> n)) \<subseteq> support 0 UNIV (\<pi> \<alpha>) \<union> support 0 UNIV (\<pi> \<beta>)

goal (1 subgoal):
 1. return_loans \<rho> (\<alpha> + \<beta>) = return_loans \<rho> \<alpha> + return_loans \<rho> \<beta>
[PROOF STEP]
have
    "?\<alpha> \<in> fin_support 0 UNIV"
    "?\<beta> \<in> fin_support 0 UNIV"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> \<alpha> \<in> fin_support 0 UNIV &&& \<pi> \<beta> \<in> fin_support 0 UNIV
[PROOF STEP]
using Rep_account
[PROOF STATE]
proof (prove)
using this:
\<pi> ?x \<in> fin_support 0 UNIV

goal (1 subgoal):
 1. \<pi> \<alpha> \<in> fin_support 0 UNIV &&& \<pi> \<beta> \<in> fin_support 0 UNIV
[PROOF STEP]
by force+
[PROOF STATE]
proof (state)
this:
\<pi> \<alpha> \<in> fin_support 0 UNIV
\<pi> \<beta> \<in> fin_support 0 UNIV

goal (1 subgoal):
 1. return_loans \<rho> (\<alpha> + \<beta>) = return_loans \<rho> \<alpha> + return_loans \<rho> \<beta>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
support 0 UNIV (\<lambda>n. (1 - \<rho> n) * \<pi> \<alpha> n) \<subseteq> support 0 UNIV (\<pi> \<alpha>)
support 0 UNIV (\<lambda>n. (1 - \<rho> n) * \<pi> \<beta> n) \<subseteq> support 0 UNIV (\<pi> \<beta>)
support 0 UNIV (\<lambda>n. (1 - \<rho> n) * (\<pi> \<alpha> n + \<pi> \<beta> n)) \<subseteq> support 0 UNIV (\<pi> \<alpha>) \<union> support 0 UNIV (\<pi> \<beta>)
\<pi> \<alpha> \<in> fin_support 0 UNIV
\<pi> \<beta> \<in> fin_support 0 UNIV
[PROOF STEP]
have \<star>:
    "?\<rho>\<alpha> \<in> fin_support 0 UNIV"
    "?\<rho>\<beta> \<in> fin_support 0 UNIV"
    "?\<rho>\<alpha>\<beta> \<in> fin_support 0 UNIV"
[PROOF STATE]
proof (prove)
using this:
support 0 UNIV (\<lambda>n. (1 - \<rho> n) * \<pi> \<alpha> n) \<subseteq> support 0 UNIV (\<pi> \<alpha>)
support 0 UNIV (\<lambda>n. (1 - \<rho> n) * \<pi> \<beta> n) \<subseteq> support 0 UNIV (\<pi> \<beta>)
support 0 UNIV (\<lambda>n. (1 - \<rho> n) * (\<pi> \<alpha> n + \<pi> \<beta> n)) \<subseteq> support 0 UNIV (\<pi> \<alpha>) \<union> support 0 UNIV (\<pi> \<beta>)
\<pi> \<alpha> \<in> fin_support 0 UNIV
\<pi> \<beta> \<in> fin_support 0 UNIV

goal (1 subgoal):
 1. (\<lambda>n. (1 - \<rho> n) * \<pi> \<alpha> n) \<in> fin_support 0 UNIV &&& (\<lambda>n. (1 - \<rho> n) * \<pi> \<beta> n) \<in> fin_support 0 UNIV &&& (\<lambda>n. (1 - \<rho> n) * (\<pi> \<alpha> n + \<pi> \<beta> n)) \<in> fin_support 0 UNIV
[PROOF STEP]
unfolding fin_support_def
[PROOF STATE]
proof (prove)
using this:
support 0 UNIV (\<lambda>n. (1 - \<rho> n) * \<pi> \<alpha> n) \<subseteq> support 0 UNIV (\<pi> \<alpha>)
support 0 UNIV (\<lambda>n. (1 - \<rho> n) * \<pi> \<beta> n) \<subseteq> support 0 UNIV (\<pi> \<beta>)
support 0 UNIV (\<lambda>n. (1 - \<rho> n) * (\<pi> \<alpha> n + \<pi> \<beta> n)) \<subseteq> support 0 UNIV (\<pi> \<alpha>) \<union> support 0 UNIV (\<pi> \<beta>)
\<pi> \<alpha> \<in> {f. finite (support 0 UNIV f)}
\<pi> \<beta> \<in> {f. finite (support 0 UNIV f)}

goal (1 subgoal):
 1. (\<lambda>n. (1 - \<rho> n) * \<pi> \<alpha> n) \<in> {f. finite (support 0 UNIV f)} &&& (\<lambda>n. (1 - \<rho> n) * \<pi> \<beta> n) \<in> {f. finite (support 0 UNIV f)} &&& (\<lambda>n. (1 - \<rho> n) * (\<pi> \<alpha> n + \<pi> \<beta> n)) \<in> {f. finite (support 0 UNIV f)}
[PROOF STEP]
using finite_subset
[PROOF STATE]
proof (prove)
using this:
support 0 UNIV (\<lambda>n. (1 - \<rho> n) * \<pi> \<alpha> n) \<subseteq> support 0 UNIV (\<pi> \<alpha>)
support 0 UNIV (\<lambda>n. (1 - \<rho> n) * \<pi> \<beta> n) \<subseteq> support 0 UNIV (\<pi> \<beta>)
support 0 UNIV (\<lambda>n. (1 - \<rho> n) * (\<pi> \<alpha> n + \<pi> \<beta> n)) \<subseteq> support 0 UNIV (\<pi> \<alpha>) \<union> support 0 UNIV (\<pi> \<beta>)
\<pi> \<alpha> \<in> {f. finite (support 0 UNIV f)}
\<pi> \<beta> \<in> {f. finite (support 0 UNIV f)}
\<lbrakk>?A \<subseteq> ?B; finite ?B\<rbrakk> \<Longrightarrow> finite ?A

goal (1 subgoal):
 1. (\<lambda>n. (1 - \<rho> n) * \<pi> \<alpha> n) \<in> {f. finite (support 0 UNIV f)} &&& (\<lambda>n. (1 - \<rho> n) * \<pi> \<beta> n) \<in> {f. finite (support 0 UNIV f)} &&& (\<lambda>n. (1 - \<rho> n) * (\<pi> \<alpha> n + \<pi> \<beta> n)) \<in> {f. finite (support 0 UNIV f)}
[PROOF STEP]
by auto+
[PROOF STATE]
proof (state)
this:
(\<lambda>n. (1 - \<rho> n) * \<pi> \<alpha> n) \<in> fin_support 0 UNIV
(\<lambda>n. (1 - \<rho> n) * \<pi> \<beta> n) \<in> fin_support 0 UNIV
(\<lambda>n. (1 - \<rho> n) * (\<pi> \<alpha> n + \<pi> \<beta> n)) \<in> fin_support 0 UNIV

goal (1 subgoal):
 1. return_loans \<rho> (\<alpha> + \<beta>) = return_loans \<rho> \<alpha> + return_loans \<rho> \<beta>
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
(\<lambda>n. (1 - \<rho> n) * \<pi> \<alpha> n) \<in> fin_support 0 UNIV
(\<lambda>n. (1 - \<rho> n) * \<pi> \<beta> n) \<in> fin_support 0 UNIV
(\<lambda>n. (1 - \<rho> n) * (\<pi> \<alpha> n + \<pi> \<beta> n)) \<in> fin_support 0 UNIV

goal (1 subgoal):
 1. return_loans \<rho> (\<alpha> + \<beta>) = return_loans \<rho> \<alpha> + return_loans \<rho> \<beta>
[PROOF STEP]
fix n
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. return_loans \<rho> (\<alpha> + \<beta>) = return_loans \<rho> \<alpha> + return_loans \<rho> \<beta>
[PROOF STEP]
have "\<pi> (return_loans \<rho> (\<alpha> + \<beta>)) n =
          \<pi> (return_loans \<rho> \<alpha> + return_loans \<rho> \<beta>) n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> (return_loans \<rho> (\<alpha> + \<beta>)) n = \<pi> (return_loans \<rho> \<alpha> + return_loans \<rho> \<beta>) n
[PROOF STEP]
unfolding return_loans_def Rep_account_plus
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> (\<iota> (\<lambda>n. (1 - \<rho> n) * (\<pi> \<alpha> n + \<pi> \<beta> n))) n = \<pi> (\<iota> (\<lambda>n. (1 - \<rho> n) * \<pi> \<alpha> n)) n + \<pi> (\<iota> (\<lambda>n. (1 - \<rho> n) * \<pi> \<beta> n)) n
[PROOF STEP]
using \<star> Abs_account_inverse distrib_left
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. (1 - \<rho> n) * \<pi> \<alpha> n) \<in> fin_support 0 UNIV
(\<lambda>n. (1 - \<rho> n) * \<pi> \<beta> n) \<in> fin_support 0 UNIV
(\<lambda>n. (1 - \<rho> n) * (\<pi> \<alpha> n + \<pi> \<beta> n)) \<in> fin_support 0 UNIV
?y \<in> fin_support 0 UNIV \<Longrightarrow> \<pi> (\<iota> ?y) = ?y
?a * (?b + ?c) = ?a * ?b + ?a * ?c

goal (1 subgoal):
 1. \<pi> (\<iota> (\<lambda>n. (1 - \<rho> n) * (\<pi> \<alpha> n + \<pi> \<beta> n))) n = \<pi> (\<iota> (\<lambda>n. (1 - \<rho> n) * \<pi> \<alpha> n)) n + \<pi> (\<iota> (\<lambda>n. (1 - \<rho> n) * \<pi> \<beta> n)) n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<pi> (return_loans \<rho> (\<alpha> + \<beta>)) n = \<pi> (return_loans \<rho> \<alpha> + return_loans \<rho> \<beta>) n

goal (1 subgoal):
 1. return_loans \<rho> (\<alpha> + \<beta>) = return_loans \<rho> \<alpha> + return_loans \<rho> \<beta>
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<pi> (return_loans \<rho> (\<alpha> + \<beta>)) ?n2 = \<pi> (return_loans \<rho> \<alpha> + return_loans \<rho> \<beta>) ?n2

goal (1 subgoal):
 1. return_loans \<rho> (\<alpha> + \<beta>) = return_loans \<rho> \<alpha> + return_loans \<rho> \<beta>
[PROOF STEP]
hence "\<pi> (return_loans \<rho> (\<alpha> + \<beta>)) =
         \<pi> (return_loans \<rho> \<alpha> + return_loans \<rho> \<beta>)"
[PROOF STATE]
proof (prove)
using this:
\<pi> (return_loans \<rho> (\<alpha> + \<beta>)) ?n2 = \<pi> (return_loans \<rho> \<alpha> + return_loans \<rho> \<beta>) ?n2

goal (1 subgoal):
 1. \<pi> (return_loans \<rho> (\<alpha> + \<beta>)) = \<pi> (return_loans \<rho> \<alpha> + return_loans \<rho> \<beta>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<pi> (return_loans \<rho> (\<alpha> + \<beta>)) = \<pi> (return_loans \<rho> \<alpha> + return_loans \<rho> \<beta>)

goal (1 subgoal):
 1. return_loans \<rho> (\<alpha> + \<beta>) = return_loans \<rho> \<alpha> + return_loans \<rho> \<beta>
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<pi> (return_loans \<rho> (\<alpha> + \<beta>)) = \<pi> (return_loans \<rho> \<alpha> + return_loans \<rho> \<beta>)

goal (1 subgoal):
 1. return_loans \<rho> (\<alpha> + \<beta>) = return_loans \<rho> \<alpha> + return_loans \<rho> \<beta>
[PROOF STEP]
by (metis Rep_account_inverse)
[PROOF STATE]
proof (state)
this:
return_loans \<rho> (\<alpha> + \<beta>) = return_loans \<rho> \<alpha> + return_loans \<rho> \<beta>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma return_loans_zero [simp]: "return_loans \<rho> 0 = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. return_loans \<rho> 0 = 0
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. return_loans \<rho> 0 = 0
[PROOF STEP]
have "(\<lambda>n. (1 - \<rho> n) * 0) = (\<lambda>_. 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. (1 - \<rho> n) * 0) = (\<lambda>_. 0)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
(\<lambda>n. (1 - \<rho> n) * 0) = (\<lambda>_. 0)

goal (1 subgoal):
 1. return_loans \<rho> 0 = 0
[PROOF STEP]
hence "\<iota> (\<lambda>n. (1 - \<rho> n) * 0) = 0"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. (1 - \<rho> n) * 0) = (\<lambda>_. 0)

goal (1 subgoal):
 1. \<iota> (\<lambda>n. (1 - \<rho> n) * 0) = 0
[PROOF STEP]
unfolding zero_account_def
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. (1 - \<rho> n) * 0) = (\<lambda>_. 0)

goal (1 subgoal):
 1. \<iota> (\<lambda>n. (1 - \<rho> n) * 0) = \<iota> (\<lambda>_. 0)
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
\<iota> (\<lambda>n. (1 - \<rho> n) * 0) = 0

goal (1 subgoal):
 1. return_loans \<rho> 0 = 0
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<iota> (\<lambda>n. (1 - \<rho> n) * 0) = 0

goal (1 subgoal):
 1. return_loans \<rho> 0 = 0
[PROOF STEP]
unfolding return_loans_def Rep_account_zero
[PROOF STATE]
proof (prove)
using this:
\<iota> (\<lambda>n. (1 - \<rho> n) * 0) = 0

goal (1 subgoal):
 1. \<iota> (\<lambda>n. (1 - \<rho> n) * 0) = 0
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
return_loans \<rho> 0 = 0

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma return_loans_uminus: "return_loans \<rho> (- \<alpha>) = - return_loans \<rho> \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. return_loans \<rho> (- \<alpha>) = - return_loans \<rho> \<alpha>
[PROOF STEP]
by (metis
        add.left_cancel
        diff_self
        minus_account_def
        return_loans_plus
        return_loans_zero)


[STATEMENT]
lemma return_loans_subtract:
  "return_loans \<rho> (\<alpha> - \<beta>) = return_loans \<rho> \<alpha> - return_loans \<rho> \<beta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. return_loans \<rho> (\<alpha> - \<beta>) = return_loans \<rho> \<alpha> - return_loans \<rho> \<beta>
[PROOF STEP]
by (simp add: additive.diff additive_def return_loans_plus)


[STATEMENT]
lemma return_loans_mono:
  assumes "\<forall> n . \<rho> n < 1"
  and "\<forall> n m . n \<le> m \<longrightarrow> \<rho> n \<le> \<rho> m"
  and "\<alpha> \<le> \<beta>"
  shows "return_loans \<rho> \<alpha> \<le> return_loans \<rho> \<beta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. return_loans \<rho> \<alpha> \<le> return_loans \<rho> \<beta>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. return_loans \<rho> \<alpha> \<le> return_loans \<rho> \<beta>
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. return_loans \<rho> \<alpha> \<le> return_loans \<rho> \<beta>
[PROOF STEP]
fix \<alpha> :: account
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. return_loans \<rho> \<alpha> \<le> return_loans \<rho> \<beta>
[PROOF STEP]
assume "0 \<le> \<alpha>"
[PROOF STATE]
proof (state)
this:
0 \<le> \<alpha>

goal (1 subgoal):
 1. return_loans \<rho> \<alpha> \<le> return_loans \<rho> \<beta>
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
0 \<le> \<alpha>

goal (1 subgoal):
 1. return_loans \<rho> \<alpha> \<le> return_loans \<rho> \<beta>
[PROOF STEP]
fix n :: nat
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. return_loans \<rho> \<alpha> \<le> return_loans \<rho> \<beta>
[PROOF STEP]
let ?\<alpha> = "\<pi> \<alpha>"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. return_loans \<rho> \<alpha> \<le> return_loans \<rho> \<beta>
[PROOF STEP]
let ?\<rho>\<alpha> = "\<lambda>n. (1 - \<rho> n) * ?\<alpha> n"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. return_loans \<rho> \<alpha> \<le> return_loans \<rho> \<beta>
[PROOF STEP]
have "\<forall> n . 0 \<le> (\<Sum> i\<le>n . ?\<alpha> i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n. 0 \<le> sum (\<pi> \<alpha>) {..n}
[PROOF STEP]
using \<open>0 \<le> \<alpha>\<close>
[PROOF STATE]
proof (prove)
using this:
0 \<le> \<alpha>

goal (1 subgoal):
 1. \<forall>n. 0 \<le> sum (\<pi> \<alpha>) {..n}
[PROOF STEP]
unfolding less_eq_account_def Rep_account_zero
[PROOF STATE]
proof (prove)
using this:
\<forall>n. (\<Sum>i\<le>n. 0) \<le> sum (\<pi> \<alpha>) {..n}

goal (1 subgoal):
 1. \<forall>n. 0 \<le> sum (\<pi> \<alpha>) {..n}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>n. 0 \<le> sum (\<pi> \<alpha>) {..n}

goal (1 subgoal):
 1. return_loans \<rho> \<alpha> \<le> return_loans \<rho> \<beta>
[PROOF STEP]
hence "0 \<le> (\<Sum> i\<le>n . ?\<alpha> i)"
[PROOF STATE]
proof (prove)
using this:
\<forall>n. 0 \<le> sum (\<pi> \<alpha>) {..n}

goal (1 subgoal):
 1. 0 \<le> sum (\<pi> \<alpha>) {..n}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 \<le> sum (\<pi> \<alpha>) {..n}

goal (1 subgoal):
 1. return_loans \<rho> \<alpha> \<le> return_loans \<rho> \<beta>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
0 \<le> sum (\<pi> \<alpha>) {..n}

goal (1 subgoal):
 1. return_loans \<rho> \<alpha> \<le> return_loans \<rho> \<beta>
[PROOF STEP]
have "(1 - \<rho> n) * (\<Sum> i\<le>n . ?\<alpha> i) \<le> (\<Sum> i\<le>n . ?\<rho>\<alpha> i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1 - \<rho> n) * sum (\<pi> \<alpha>) {..n} \<le> (\<Sum>i\<le>n. (1 - \<rho> i) * \<pi> \<alpha> i)
[PROOF STEP]
proof (induct n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (1 - \<rho> 0) * sum (\<pi> \<alpha>) {..0} \<le> (\<Sum>i\<le>0. (1 - \<rho> i) * \<pi> \<alpha> i)
 2. \<And>n. (1 - \<rho> n) * sum (\<pi> \<alpha>) {..n} \<le> (\<Sum>i\<le>n. (1 - \<rho> i) * \<pi> \<alpha> i) \<Longrightarrow> (1 - \<rho> (Suc n)) * sum (\<pi> \<alpha>) {..Suc n} \<le> (\<Sum>i\<le>Suc n. (1 - \<rho> i) * \<pi> \<alpha> i)
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. (1 - \<rho> 0) * sum (\<pi> \<alpha>) {..0} \<le> (\<Sum>i\<le>0. (1 - \<rho> i) * \<pi> \<alpha> i)
 2. \<And>n. (1 - \<rho> n) * sum (\<pi> \<alpha>) {..n} \<le> (\<Sum>i\<le>n. (1 - \<rho> i) * \<pi> \<alpha> i) \<Longrightarrow> (1 - \<rho> (Suc n)) * sum (\<pi> \<alpha>) {..Suc n} \<le> (\<Sum>i\<le>Suc n. (1 - \<rho> i) * \<pi> \<alpha> i)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1 - \<rho> 0) * sum (\<pi> \<alpha>) {..0} \<le> (\<Sum>i\<le>0. (1 - \<rho> i) * \<pi> \<alpha> i)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(1 - \<rho> 0) * sum (\<pi> \<alpha>) {..0} \<le> (\<Sum>i\<le>0. (1 - \<rho> i) * \<pi> \<alpha> i)

goal (1 subgoal):
 1. \<And>n. (1 - \<rho> n) * sum (\<pi> \<alpha>) {..n} \<le> (\<Sum>i\<le>n. (1 - \<rho> i) * \<pi> \<alpha> i) \<Longrightarrow> (1 - \<rho> (Suc n)) * sum (\<pi> \<alpha>) {..Suc n} \<le> (\<Sum>i\<le>Suc n. (1 - \<rho> i) * \<pi> \<alpha> i)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. (1 - \<rho> n) * sum (\<pi> \<alpha>) {..n} \<le> (\<Sum>i\<le>n. (1 - \<rho> i) * \<pi> \<alpha> i) \<Longrightarrow> (1 - \<rho> (Suc n)) * sum (\<pi> \<alpha>) {..Suc n} \<le> (\<Sum>i\<le>Suc n. (1 - \<rho> i) * \<pi> \<alpha> i)
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
(1 - \<rho> n) * sum (\<pi> \<alpha>) {..n} \<le> (\<Sum>i\<le>n. (1 - \<rho> i) * \<pi> \<alpha> i)

goal (1 subgoal):
 1. \<And>n. (1 - \<rho> n) * sum (\<pi> \<alpha>) {..n} \<le> (\<Sum>i\<le>n. (1 - \<rho> i) * \<pi> \<alpha> i) \<Longrightarrow> (1 - \<rho> (Suc n)) * sum (\<pi> \<alpha>) {..Suc n} \<le> (\<Sum>i\<le>Suc n. (1 - \<rho> i) * \<pi> \<alpha> i)
[PROOF STEP]
have "0 \<le> (1 - \<rho> (Suc n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> 1 - \<rho> (Suc n)
[PROOF STEP]
by (simp add: \<open>\<forall> n . \<rho> n < 1\<close> less_eq_real_def)
[PROOF STATE]
proof (state)
this:
0 \<le> 1 - \<rho> (Suc n)

goal (1 subgoal):
 1. \<And>n. (1 - \<rho> n) * sum (\<pi> \<alpha>) {..n} \<le> (\<Sum>i\<le>n. (1 - \<rho> i) * \<pi> \<alpha> i) \<Longrightarrow> (1 - \<rho> (Suc n)) * sum (\<pi> \<alpha>) {..Suc n} \<le> (\<Sum>i\<le>Suc n. (1 - \<rho> i) * \<pi> \<alpha> i)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
0 \<le> 1 - \<rho> (Suc n)

goal (1 subgoal):
 1. \<And>n. (1 - \<rho> n) * sum (\<pi> \<alpha>) {..n} \<le> (\<Sum>i\<le>n. (1 - \<rho> i) * \<pi> \<alpha> i) \<Longrightarrow> (1 - \<rho> (Suc n)) * sum (\<pi> \<alpha>) {..Suc n} \<le> (\<Sum>i\<le>Suc n. (1 - \<rho> i) * \<pi> \<alpha> i)
[PROOF STEP]
have "(1 - \<rho> (Suc n)) \<le> (1 - \<rho> n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 - \<rho> (Suc n) \<le> 1 - \<rho> n
[PROOF STEP]
using \<open>\<forall> n m . n \<le> m \<longrightarrow> \<rho> n \<le> \<rho> m\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>n m. n \<le> m \<longrightarrow> \<rho> n \<le> \<rho> m

goal (1 subgoal):
 1. 1 - \<rho> (Suc n) \<le> 1 - \<rho> n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
1 - \<rho> (Suc n) \<le> 1 - \<rho> n

goal (1 subgoal):
 1. \<And>n. (1 - \<rho> n) * sum (\<pi> \<alpha>) {..n} \<le> (\<Sum>i\<le>n. (1 - \<rho> i) * \<pi> \<alpha> i) \<Longrightarrow> (1 - \<rho> (Suc n)) * sum (\<pi> \<alpha>) {..Suc n} \<le> (\<Sum>i\<le>Suc n. (1 - \<rho> i) * \<pi> \<alpha> i)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
0 \<le> 1 - \<rho> (Suc n)
1 - \<rho> (Suc n) \<le> 1 - \<rho> n
[PROOF STEP]
have
          "(1 - \<rho> (Suc n)) * (\<Sum> i\<le>n . ?\<alpha> i) \<le> (1 - \<rho> n) * (\<Sum> i\<le>n . ?\<alpha> i)"
[PROOF STATE]
proof (prove)
using this:
0 \<le> 1 - \<rho> (Suc n)
1 - \<rho> (Suc n) \<le> 1 - \<rho> n

goal (1 subgoal):
 1. (1 - \<rho> (Suc n)) * sum (\<pi> \<alpha>) {..n} \<le> (1 - \<rho> n) * sum (\<pi> \<alpha>) {..n}
[PROOF STEP]
using \<open>\<forall> n . 0 \<le> (\<Sum> i\<le>n . ?\<alpha> i)\<close>
[PROOF STATE]
proof (prove)
using this:
0 \<le> 1 - \<rho> (Suc n)
1 - \<rho> (Suc n) \<le> 1 - \<rho> n
\<forall>n. 0 \<le> sum (\<pi> \<alpha>) {..n}

goal (1 subgoal):
 1. (1 - \<rho> (Suc n)) * sum (\<pi> \<alpha>) {..n} \<le> (1 - \<rho> n) * sum (\<pi> \<alpha>) {..n}
[PROOF STEP]
by (meson le_less mult_mono')
[PROOF STATE]
proof (state)
this:
(1 - \<rho> (Suc n)) * sum (\<pi> \<alpha>) {..n} \<le> (1 - \<rho> n) * sum (\<pi> \<alpha>) {..n}

goal (1 subgoal):
 1. \<And>n. (1 - \<rho> n) * sum (\<pi> \<alpha>) {..n} \<le> (\<Sum>i\<le>n. (1 - \<rho> i) * \<pi> \<alpha> i) \<Longrightarrow> (1 - \<rho> (Suc n)) * sum (\<pi> \<alpha>) {..Suc n} \<le> (\<Sum>i\<le>Suc n. (1 - \<rho> i) * \<pi> \<alpha> i)
[PROOF STEP]
hence
          "(1 - \<rho> (Suc n)) * (\<Sum> i\<le> Suc n . ?\<alpha> i) \<le>
           (1 - \<rho> n) * (\<Sum> i\<le>n . ?\<alpha> i) + (1 - \<rho> (Suc n)) * (?\<alpha> (Suc n))"
          (is "_ \<le> ?X")
[PROOF STATE]
proof (prove)
using this:
(1 - \<rho> (Suc n)) * sum (\<pi> \<alpha>) {..n} \<le> (1 - \<rho> n) * sum (\<pi> \<alpha>) {..n}

goal (1 subgoal):
 1. (1 - \<rho> (Suc n)) * sum (\<pi> \<alpha>) {..Suc n} \<le> (1 - \<rho> n) * sum (\<pi> \<alpha>) {..n} + (1 - \<rho> (Suc n)) * \<pi> \<alpha> (Suc n)
[PROOF STEP]
by (simp add: distrib_left)
[PROOF STATE]
proof (state)
this:
(1 - \<rho> (Suc n)) * sum (\<pi> \<alpha>) {..Suc n} \<le> (1 - \<rho> n) * sum (\<pi> \<alpha>) {..n} + (1 - \<rho> (Suc n)) * \<pi> \<alpha> (Suc n)

goal (1 subgoal):
 1. \<And>n. (1 - \<rho> n) * sum (\<pi> \<alpha>) {..n} \<le> (\<Sum>i\<le>n. (1 - \<rho> i) * \<pi> \<alpha> i) \<Longrightarrow> (1 - \<rho> (Suc n)) * sum (\<pi> \<alpha>) {..Suc n} \<le> (\<Sum>i\<le>Suc n. (1 - \<rho> i) * \<pi> \<alpha> i)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(1 - \<rho> (Suc n)) * sum (\<pi> \<alpha>) {..Suc n} \<le> (1 - \<rho> n) * sum (\<pi> \<alpha>) {..n} + (1 - \<rho> (Suc n)) * \<pi> \<alpha> (Suc n)

goal (1 subgoal):
 1. \<And>n. (1 - \<rho> n) * sum (\<pi> \<alpha>) {..n} \<le> (\<Sum>i\<le>n. (1 - \<rho> i) * \<pi> \<alpha> i) \<Longrightarrow> (1 - \<rho> (Suc n)) * sum (\<pi> \<alpha>) {..Suc n} \<le> (\<Sum>i\<le>Suc n. (1 - \<rho> i) * \<pi> \<alpha> i)
[PROOF STEP]
have
          "?X \<le> (\<Sum> i\<le> Suc n . ?\<rho>\<alpha> i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1 - \<rho> n) * sum (\<pi> \<alpha>) {..n} + (1 - \<rho> (Suc n)) * \<pi> \<alpha> (Suc n) \<le> (\<Sum>i\<le>Suc n. (1 - \<rho> i) * \<pi> \<alpha> i)
[PROOF STEP]
using Suc.hyps
[PROOF STATE]
proof (prove)
using this:
(1 - \<rho> n) * sum (\<pi> \<alpha>) {..n} \<le> (\<Sum>i\<le>n. (1 - \<rho> i) * \<pi> \<alpha> i)

goal (1 subgoal):
 1. (1 - \<rho> n) * sum (\<pi> \<alpha>) {..n} + (1 - \<rho> (Suc n)) * \<pi> \<alpha> (Suc n) \<le> (\<Sum>i\<le>Suc n. (1 - \<rho> i) * \<pi> \<alpha> i)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
(1 - \<rho> n) * sum (\<pi> \<alpha>) {..n} + (1 - \<rho> (Suc n)) * \<pi> \<alpha> (Suc n) \<le> (\<Sum>i\<le>Suc n. (1 - \<rho> i) * \<pi> \<alpha> i)

goal (1 subgoal):
 1. \<And>n. (1 - \<rho> n) * sum (\<pi> \<alpha>) {..n} \<le> (\<Sum>i\<le>n. (1 - \<rho> i) * \<pi> \<alpha> i) \<Longrightarrow> (1 - \<rho> (Suc n)) * sum (\<pi> \<alpha>) {..Suc n} \<le> (\<Sum>i\<le>Suc n. (1 - \<rho> i) * \<pi> \<alpha> i)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(1 - \<rho> (Suc n)) * sum (\<pi> \<alpha>) {..Suc n} \<le> (1 - \<rho> n) * sum (\<pi> \<alpha>) {..n} + (1 - \<rho> (Suc n)) * \<pi> \<alpha> (Suc n)
(1 - \<rho> n) * sum (\<pi> \<alpha>) {..n} + (1 - \<rho> (Suc n)) * \<pi> \<alpha> (Suc n) \<le> (\<Sum>i\<le>Suc n. (1 - \<rho> i) * \<pi> \<alpha> i)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(1 - \<rho> (Suc n)) * sum (\<pi> \<alpha>) {..Suc n} \<le> (1 - \<rho> n) * sum (\<pi> \<alpha>) {..n} + (1 - \<rho> (Suc n)) * \<pi> \<alpha> (Suc n)
(1 - \<rho> n) * sum (\<pi> \<alpha>) {..n} + (1 - \<rho> (Suc n)) * \<pi> \<alpha> (Suc n) \<le> (\<Sum>i\<le>Suc n. (1 - \<rho> i) * \<pi> \<alpha> i)

goal (1 subgoal):
 1. (1 - \<rho> (Suc n)) * sum (\<pi> \<alpha>) {..Suc n} \<le> (\<Sum>i\<le>Suc n. (1 - \<rho> i) * \<pi> \<alpha> i)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(1 - \<rho> (Suc n)) * sum (\<pi> \<alpha>) {..Suc n} \<le> (\<Sum>i\<le>Suc n. (1 - \<rho> i) * \<pi> \<alpha> i)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(1 - \<rho> n) * sum (\<pi> \<alpha>) {..n} \<le> (\<Sum>i\<le>n. (1 - \<rho> i) * \<pi> \<alpha> i)

goal (1 subgoal):
 1. return_loans \<rho> \<alpha> \<le> return_loans \<rho> \<beta>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(1 - \<rho> n) * sum (\<pi> \<alpha>) {..n} \<le> (\<Sum>i\<le>n. (1 - \<rho> i) * \<pi> \<alpha> i)

goal (1 subgoal):
 1. return_loans \<rho> \<alpha> \<le> return_loans \<rho> \<beta>
[PROOF STEP]
have "0 < 1 - \<rho> n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < 1 - \<rho> n
[PROOF STEP]
by (simp add: \<open>\<forall> n . \<rho> n < 1\<close>)
[PROOF STATE]
proof (state)
this:
0 < 1 - \<rho> n

goal (1 subgoal):
 1. return_loans \<rho> \<alpha> \<le> return_loans \<rho> \<beta>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
0 \<le> sum (\<pi> \<alpha>) {..n}
(1 - \<rho> n) * sum (\<pi> \<alpha>) {..n} \<le> (\<Sum>i\<le>n. (1 - \<rho> i) * \<pi> \<alpha> i)
0 < 1 - \<rho> n
[PROOF STEP]
have "0 \<le> (\<Sum> i\<le>n . ?\<rho>\<alpha> i)"
[PROOF STATE]
proof (prove)
using this:
0 \<le> sum (\<pi> \<alpha>) {..n}
(1 - \<rho> n) * sum (\<pi> \<alpha>) {..n} \<le> (\<Sum>i\<le>n. (1 - \<rho> i) * \<pi> \<alpha> i)
0 < 1 - \<rho> n

goal (1 subgoal):
 1. 0 \<le> (\<Sum>i\<le>n. (1 - \<rho> i) * \<pi> \<alpha> i)
[PROOF STEP]
using dual_order.trans
[PROOF STATE]
proof (prove)
using this:
0 \<le> sum (\<pi> \<alpha>) {..n}
(1 - \<rho> n) * sum (\<pi> \<alpha>) {..n} \<le> (\<Sum>i\<le>n. (1 - \<rho> i) * \<pi> \<alpha> i)
0 < 1 - \<rho> n
\<lbrakk>?b \<le> ?a; ?c \<le> ?b\<rbrakk> \<Longrightarrow> ?c \<le> ?a

goal (1 subgoal):
 1. 0 \<le> (\<Sum>i\<le>n. (1 - \<rho> i) * \<pi> \<alpha> i)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
0 \<le> (\<Sum>i\<le>n. (1 - \<rho> i) * \<pi> \<alpha> i)

goal (1 subgoal):
 1. return_loans \<rho> \<alpha> \<le> return_loans \<rho> \<beta>
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
0 \<le> (\<Sum>i\<le>?n2. (1 - \<rho> i) * \<pi> \<alpha> i)

goal (1 subgoal):
 1. return_loans \<rho> \<alpha> \<le> return_loans \<rho> \<beta>
[PROOF STEP]
hence "strictly_solvent (return_loans \<rho> \<alpha>)"
[PROOF STATE]
proof (prove)
using this:
0 \<le> (\<Sum>i\<le>?n2. (1 - \<rho> i) * \<pi> \<alpha> i)

goal (1 subgoal):
 1. strictly_solvent (return_loans \<rho> \<alpha>)
[PROOF STEP]
unfolding strictly_solvent_def Rep_account_return_loans
[PROOF STATE]
proof (prove)
using this:
0 \<le> (\<Sum>i\<le>?n2. (1 - \<rho> i) * \<pi> \<alpha> i)

goal (1 subgoal):
 1. \<forall>n. 0 \<le> (\<Sum>i\<le>n. (1 - \<rho> i) * \<pi> \<alpha> i)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
strictly_solvent (return_loans \<rho> \<alpha>)

goal (1 subgoal):
 1. return_loans \<rho> \<alpha> \<le> return_loans \<rho> \<beta>
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
0 \<le> ?\<alpha>'2 \<Longrightarrow> strictly_solvent (return_loans \<rho> ?\<alpha>'2)

goal (1 subgoal):
 1. return_loans \<rho> \<alpha> \<le> return_loans \<rho> \<beta>
[PROOF STEP]
hence "0 \<le> return_loans \<rho> (\<beta> - \<alpha>)"
[PROOF STATE]
proof (prove)
using this:
0 \<le> ?\<alpha>'2 \<Longrightarrow> strictly_solvent (return_loans \<rho> ?\<alpha>'2)

goal (1 subgoal):
 1. 0 \<le> return_loans \<rho> (\<beta> - \<alpha>)
[PROOF STEP]
using \<open>\<alpha> \<le> \<beta>\<close>
[PROOF STATE]
proof (prove)
using this:
0 \<le> ?\<alpha>'2 \<Longrightarrow> strictly_solvent (return_loans \<rho> ?\<alpha>'2)
\<alpha> \<le> \<beta>

goal (1 subgoal):
 1. 0 \<le> return_loans \<rho> (\<beta> - \<alpha>)
[PROOF STEP]
by (simp add: strictly_solvent_alt_def)
[PROOF STATE]
proof (state)
this:
0 \<le> return_loans \<rho> (\<beta> - \<alpha>)

goal (1 subgoal):
 1. return_loans \<rho> \<alpha> \<le> return_loans \<rho> \<beta>
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
0 \<le> return_loans \<rho> (\<beta> - \<alpha>)

goal (1 subgoal):
 1. return_loans \<rho> \<alpha> \<le> return_loans \<rho> \<beta>
[PROOF STEP]
by (metis
          add_diff_cancel_left'
          diff_ge_0_iff_ge
          minus_account_def
          return_loans_plus)
[PROOF STATE]
proof (state)
this:
return_loans \<rho> \<alpha> \<le> return_loans \<rho> \<beta>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma return_loans_just_cash:
  assumes "\<rho> 0 = 0"
  shows "return_loans \<rho> (just_cash c) = just_cash c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. return_loans \<rho> (just_cash c) = just_cash c
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. return_loans \<rho> (just_cash c) = just_cash c
[PROOF STEP]
have "(\<lambda>n. (1 - \<rho> n) * \<pi> (\<iota> (\<lambda>n. if n = 0 then c else 0)) n)
        = (\<lambda>n. if n = 0 then (1 - \<rho> n) * c else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. (1 - \<rho> n) * \<pi> (\<iota> (\<lambda>n. if n = 0 then c else 0)) n) = (\<lambda>n. if n = 0 then (1 - \<rho> n) * c else 0)
[PROOF STEP]
using Rep_account_just_cash just_cash_def
[PROOF STATE]
proof (prove)
using this:
\<pi> (just_cash ?c) = (\<lambda>n. if n = 0 then ?c else 0)
just_cash ?c = \<iota> (\<lambda>n. if n = 0 then ?c else 0)

goal (1 subgoal):
 1. (\<lambda>n. (1 - \<rho> n) * \<pi> (\<iota> (\<lambda>n. if n = 0 then c else 0)) n) = (\<lambda>n. if n = 0 then (1 - \<rho> n) * c else 0)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
(\<lambda>n. (1 - \<rho> n) * \<pi> (\<iota> (\<lambda>n. if n = 0 then c else 0)) n) = (\<lambda>n. if n = 0 then (1 - \<rho> n) * c else 0)

goal (1 subgoal):
 1. return_loans \<rho> (just_cash c) = just_cash c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<lambda>n. (1 - \<rho> n) * \<pi> (\<iota> (\<lambda>n. if n = 0 then c else 0)) n) = (\<lambda>n. if n = 0 then (1 - \<rho> n) * c else 0)

goal (1 subgoal):
 1. return_loans \<rho> (just_cash c) = just_cash c
[PROOF STEP]
have "\<dots> = (\<lambda>n. if n = 0 then c else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. if n = 0 then (1 - \<rho> n) * c else 0) = (\<lambda>n. if n = 0 then c else 0)
[PROOF STEP]
using \<open>\<rho> 0 = 0\<close>
[PROOF STATE]
proof (prove)
using this:
\<rho> 0 = 0

goal (1 subgoal):
 1. (\<lambda>n. if n = 0 then (1 - \<rho> n) * c else 0) = (\<lambda>n. if n = 0 then c else 0)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
(\<lambda>n. if n = 0 then (1 - \<rho> n) * c else 0) = (\<lambda>n. if n = 0 then c else 0)

goal (1 subgoal):
 1. return_loans \<rho> (just_cash c) = just_cash c
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>n. (1 - \<rho> n) * \<pi> (\<iota> (\<lambda>n. if n = 0 then c else 0)) n) = (\<lambda>n. if n = 0 then c else 0)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. (1 - \<rho> n) * \<pi> (\<iota> (\<lambda>n. if n = 0 then c else 0)) n) = (\<lambda>n. if n = 0 then c else 0)

goal (1 subgoal):
 1. return_loans \<rho> (just_cash c) = just_cash c
[PROOF STEP]
unfolding return_loans_def just_cash_def
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. (1 - \<rho> n) * \<pi> (\<iota> (\<lambda>n. if n = 0 then c else 0)) n) = (\<lambda>n. if n = 0 then c else 0)

goal (1 subgoal):
 1. \<iota> (\<lambda>n. (1 - \<rho> n) * \<pi> (\<iota> (\<lambda>n. if n = 0 then c else 0)) n) = \<iota> (\<lambda>n. if n = 0 then c else 0)
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
return_loans \<rho> (just_cash c) = just_cash c

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma distribute_interest_plus:
   "just_cash (i * net_asset_value (\<alpha> + \<beta>)) =
      just_cash (i * net_asset_value \<alpha>) +
      just_cash (i * net_asset_value \<beta>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. just_cash (i * net_asset_value (\<alpha> + \<beta>)) = just_cash (i * net_asset_value \<alpha>) + just_cash (i * net_asset_value \<beta>)
[PROOF STEP]
unfolding just_cash_def net_asset_value_plus
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<iota> (\<lambda>n. if n = 0 then i * (net_asset_value \<alpha> + net_asset_value \<beta>) else 0) = \<iota> (\<lambda>n. if n = 0 then i * net_asset_value \<alpha> else 0) + \<iota> (\<lambda>n. if n = 0 then i * net_asset_value \<beta> else 0)
[PROOF STEP]
by (metis
        distrib_left
        just_cash_plus
        just_cash_def)


[STATEMENT]
lemma update_account_plus:
  "update_account \<rho> i (\<alpha> + \<beta>) =
     update_account \<rho> i \<alpha> + update_account \<rho> i \<beta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. update_account \<rho> i (\<alpha> + \<beta>) = update_account \<rho> i \<alpha> + update_account \<rho> i \<beta>
[PROOF STEP]
unfolding
    update_account_def
    return_loans_plus
    distribute_interest_plus
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. just_cash (i * net_asset_value \<alpha>) + just_cash (i * net_asset_value \<beta>) + (return_loans \<rho> \<alpha> + return_loans \<rho> \<beta>) = just_cash (i * net_asset_value \<alpha>) + return_loans \<rho> \<alpha> + (just_cash (i * net_asset_value \<beta>) + return_loans \<rho> \<beta>)
[PROOF STEP]
by simp


[STATEMENT]
lemma update_account_zero [simp]: "update_account \<rho> i 0 = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. update_account \<rho> i 0 = 0
[PROOF STEP]
by (metis add_cancel_right_left update_account_plus)


[STATEMENT]
lemma update_account_uminus:
  "update_account \<rho> i (-\<alpha>) = - update_account \<rho> i \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. update_account \<rho> i (- \<alpha>) = - update_account \<rho> i \<alpha>
[PROOF STEP]
unfolding update_account_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. just_cash (i * net_asset_value (- \<alpha>)) + return_loans \<rho> (- \<alpha>) = - (just_cash (i * net_asset_value \<alpha>) + return_loans \<rho> \<alpha>)
[PROOF STEP]
by (simp add: net_asset_value_uminus return_loans_uminus)


[STATEMENT]
lemma update_account_subtract:
  "update_account \<rho> i (\<alpha> - \<beta>) =
     update_account \<rho> i \<alpha> - update_account \<rho> i \<beta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. update_account \<rho> i (\<alpha> - \<beta>) = update_account \<rho> i \<alpha> - update_account \<rho> i \<beta>
[PROOF STEP]
by (simp add: additive.diff additive.intro update_account_plus)


[STATEMENT]
lemma update_account_mono:
  assumes "0 \<le> i"
  and "\<forall> n . \<rho> n < 1"
  and "\<forall> n m . n \<le> m \<longrightarrow> \<rho> n \<le> \<rho> m"
  and "\<alpha> \<le> \<beta>"
  shows "update_account \<rho> i \<alpha> \<le> update_account \<rho> i \<beta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. update_account \<rho> i \<alpha> \<le> update_account \<rho> i \<beta>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. update_account \<rho> i \<alpha> \<le> update_account \<rho> i \<beta>
[PROOF STEP]
have "net_asset_value \<alpha> \<le> net_asset_value \<beta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. net_asset_value \<alpha> \<le> net_asset_value \<beta>
[PROOF STEP]
using \<open>\<alpha> \<le> \<beta>\<close> net_asset_value_mono
[PROOF STATE]
proof (prove)
using this:
\<alpha> \<le> \<beta>
?\<alpha> \<le> ?\<beta> \<Longrightarrow> net_asset_value ?\<alpha> \<le> net_asset_value ?\<beta>

goal (1 subgoal):
 1. net_asset_value \<alpha> \<le> net_asset_value \<beta>
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
net_asset_value \<alpha> \<le> net_asset_value \<beta>

goal (1 subgoal):
 1. update_account \<rho> i \<alpha> \<le> update_account \<rho> i \<beta>
[PROOF STEP]
hence "i * net_asset_value \<alpha> \<le> i * net_asset_value \<beta>"
[PROOF STATE]
proof (prove)
using this:
net_asset_value \<alpha> \<le> net_asset_value \<beta>

goal (1 subgoal):
 1. i * net_asset_value \<alpha> \<le> i * net_asset_value \<beta>
[PROOF STEP]
by (simp add: \<open>0 \<le> i\<close> mult_left_mono)
[PROOF STATE]
proof (state)
this:
i * net_asset_value \<alpha> \<le> i * net_asset_value \<beta>

goal (1 subgoal):
 1. update_account \<rho> i \<alpha> \<le> update_account \<rho> i \<beta>
[PROOF STEP]
hence "just_cash (i * net_asset_value \<alpha>) \<le>
         just_cash (i * net_asset_value \<beta>)"
[PROOF STATE]
proof (prove)
using this:
i * net_asset_value \<alpha> \<le> i * net_asset_value \<beta>

goal (1 subgoal):
 1. just_cash (i * net_asset_value \<alpha>) \<le> just_cash (i * net_asset_value \<beta>)
[PROOF STEP]
by (simp add: just_cash_order_embed)
[PROOF STATE]
proof (state)
this:
just_cash (i * net_asset_value \<alpha>) \<le> just_cash (i * net_asset_value \<beta>)

goal (1 subgoal):
 1. update_account \<rho> i \<alpha> \<le> update_account \<rho> i \<beta>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
just_cash (i * net_asset_value \<alpha>) \<le> just_cash (i * net_asset_value \<beta>)

goal (1 subgoal):
 1. update_account \<rho> i \<alpha> \<le> update_account \<rho> i \<beta>
[PROOF STEP]
have "return_loans \<rho> \<alpha> \<le> return_loans \<rho> \<beta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. return_loans \<rho> \<alpha> \<le> return_loans \<rho> \<beta>
[PROOF STEP]
using assms return_loans_mono
[PROOF STATE]
proof (prove)
using this:
0 \<le> i
\<forall>n. \<rho> n < 1
\<forall>n m. n \<le> m \<longrightarrow> \<rho> n \<le> \<rho> m
\<alpha> \<le> \<beta>
\<lbrakk>\<forall>n. ?\<rho> n < 1; \<forall>n m. n \<le> m \<longrightarrow> ?\<rho> n \<le> ?\<rho> m; ?\<alpha> \<le> ?\<beta>\<rbrakk> \<Longrightarrow> return_loans ?\<rho> ?\<alpha> \<le> return_loans ?\<rho> ?\<beta>

goal (1 subgoal):
 1. return_loans \<rho> \<alpha> \<le> return_loans \<rho> \<beta>
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
return_loans \<rho> \<alpha> \<le> return_loans \<rho> \<beta>

goal (1 subgoal):
 1. update_account \<rho> i \<alpha> \<le> update_account \<rho> i \<beta>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
just_cash (i * net_asset_value \<alpha>) \<le> just_cash (i * net_asset_value \<beta>)
return_loans \<rho> \<alpha> \<le> return_loans \<rho> \<beta>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
just_cash (i * net_asset_value \<alpha>) \<le> just_cash (i * net_asset_value \<beta>)
return_loans \<rho> \<alpha> \<le> return_loans \<rho> \<beta>

goal (1 subgoal):
 1. update_account \<rho> i \<alpha> \<le> update_account \<rho> i \<beta>
[PROOF STEP]
unfolding update_account_def
[PROOF STATE]
proof (prove)
using this:
just_cash (i * net_asset_value \<alpha>) \<le> just_cash (i * net_asset_value \<beta>)
return_loans \<rho> \<alpha> \<le> return_loans \<rho> \<beta>

goal (1 subgoal):
 1. just_cash (i * net_asset_value \<alpha>) + return_loans \<rho> \<alpha> \<le> just_cash (i * net_asset_value \<beta>) + return_loans \<rho> \<beta>
[PROOF STEP]
by (simp add: add_mono)
[PROOF STATE]
proof (state)
this:
update_account \<rho> i \<alpha> \<le> update_account \<rho> i \<beta>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma update_preserves_strictly_solvent:
  assumes "0 \<le> i"
  and "\<forall> n . \<rho> n < 1"
  and "\<forall> n m . n \<le> m \<longrightarrow> \<rho> n \<le> \<rho> m"
  and "strictly_solvent \<alpha>"
  shows "strictly_solvent (update_account \<rho> i \<alpha>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. strictly_solvent (update_account \<rho> i \<alpha>)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
0 \<le> i
\<forall>n. \<rho> n < 1
\<forall>n m. n \<le> m \<longrightarrow> \<rho> n \<le> \<rho> m
strictly_solvent \<alpha>

goal (1 subgoal):
 1. strictly_solvent (update_account \<rho> i \<alpha>)
[PROOF STEP]
unfolding strictly_solvent_alt_def
[PROOF STATE]
proof (prove)
using this:
0 \<le> i
\<forall>n. \<rho> n < 1
\<forall>n m. n \<le> m \<longrightarrow> \<rho> n \<le> \<rho> m
0 \<le> \<alpha>

goal (1 subgoal):
 1. 0 \<le> update_account \<rho> i \<alpha>
[PROOF STEP]
by (metis update_account_mono update_account_zero)


[STATEMENT]
lemma bulk_update_account_plus:
  "bulk_update_account n \<rho> i (\<alpha> + \<beta>) =
     bulk_update_account n \<rho> i \<alpha> + bulk_update_account n \<rho> i \<beta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bulk_update_account n \<rho> i (\<alpha> + \<beta>) = bulk_update_account n \<rho> i \<alpha> + bulk_update_account n \<rho> i \<beta>
[PROOF STEP]
proof (induct n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. bulk_update_account 0 \<rho> i (\<alpha> + \<beta>) = bulk_update_account 0 \<rho> i \<alpha> + bulk_update_account 0 \<rho> i \<beta>
 2. \<And>n. bulk_update_account n \<rho> i (\<alpha> + \<beta>) = bulk_update_account n \<rho> i \<alpha> + bulk_update_account n \<rho> i \<beta> \<Longrightarrow> bulk_update_account (Suc n) \<rho> i (\<alpha> + \<beta>) = bulk_update_account (Suc n) \<rho> i \<alpha> + bulk_update_account (Suc n) \<rho> i \<beta>
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. bulk_update_account 0 \<rho> i (\<alpha> + \<beta>) = bulk_update_account 0 \<rho> i \<alpha> + bulk_update_account 0 \<rho> i \<beta>
 2. \<And>n. bulk_update_account n \<rho> i (\<alpha> + \<beta>) = bulk_update_account n \<rho> i \<alpha> + bulk_update_account n \<rho> i \<beta> \<Longrightarrow> bulk_update_account (Suc n) \<rho> i (\<alpha> + \<beta>) = bulk_update_account (Suc n) \<rho> i \<alpha> + bulk_update_account (Suc n) \<rho> i \<beta>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bulk_update_account 0 \<rho> i (\<alpha> + \<beta>) = bulk_update_account 0 \<rho> i \<alpha> + bulk_update_account 0 \<rho> i \<beta>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
bulk_update_account 0 \<rho> i (\<alpha> + \<beta>) = bulk_update_account 0 \<rho> i \<alpha> + bulk_update_account 0 \<rho> i \<beta>

goal (1 subgoal):
 1. \<And>n. bulk_update_account n \<rho> i (\<alpha> + \<beta>) = bulk_update_account n \<rho> i \<alpha> + bulk_update_account n \<rho> i \<beta> \<Longrightarrow> bulk_update_account (Suc n) \<rho> i (\<alpha> + \<beta>) = bulk_update_account (Suc n) \<rho> i \<alpha> + bulk_update_account (Suc n) \<rho> i \<beta>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. bulk_update_account n \<rho> i (\<alpha> + \<beta>) = bulk_update_account n \<rho> i \<alpha> + bulk_update_account n \<rho> i \<beta> \<Longrightarrow> bulk_update_account (Suc n) \<rho> i (\<alpha> + \<beta>) = bulk_update_account (Suc n) \<rho> i \<alpha> + bulk_update_account (Suc n) \<rho> i \<beta>
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
bulk_update_account n \<rho> i (\<alpha> + \<beta>) = bulk_update_account n \<rho> i \<alpha> + bulk_update_account n \<rho> i \<beta>

goal (1 subgoal):
 1. \<And>n. bulk_update_account n \<rho> i (\<alpha> + \<beta>) = bulk_update_account n \<rho> i \<alpha> + bulk_update_account n \<rho> i \<beta> \<Longrightarrow> bulk_update_account (Suc n) \<rho> i (\<alpha> + \<beta>) = bulk_update_account (Suc n) \<rho> i \<alpha> + bulk_update_account (Suc n) \<rho> i \<beta>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
bulk_update_account n \<rho> i (\<alpha> + \<beta>) = bulk_update_account n \<rho> i \<alpha> + bulk_update_account n \<rho> i \<beta>
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
bulk_update_account n \<rho> i (\<alpha> + \<beta>) = bulk_update_account n \<rho> i \<alpha> + bulk_update_account n \<rho> i \<beta>

goal (1 subgoal):
 1. bulk_update_account (Suc n) \<rho> i (\<alpha> + \<beta>) = bulk_update_account (Suc n) \<rho> i \<alpha> + bulk_update_account (Suc n) \<rho> i \<beta>
[PROOF STEP]
using bulk_update_account.simps(2) update_account_plus
[PROOF STATE]
proof (prove)
using this:
bulk_update_account n \<rho> i (\<alpha> + \<beta>) = bulk_update_account n \<rho> i \<alpha> + bulk_update_account n \<rho> i \<beta>
bulk_update_account (Suc ?n) ?\<rho> ?i ?\<alpha> = update_account ?\<rho> ?i (bulk_update_account ?n ?\<rho> ?i ?\<alpha>)
update_account ?\<rho> ?i (?\<alpha> + ?\<beta>) = update_account ?\<rho> ?i ?\<alpha> + update_account ?\<rho> ?i ?\<beta>

goal (1 subgoal):
 1. bulk_update_account (Suc n) \<rho> i (\<alpha> + \<beta>) = bulk_update_account (Suc n) \<rho> i \<alpha> + bulk_update_account (Suc n) \<rho> i \<beta>
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
bulk_update_account (Suc n) \<rho> i (\<alpha> + \<beta>) = bulk_update_account (Suc n) \<rho> i \<alpha> + bulk_update_account (Suc n) \<rho> i \<beta>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bulk_update_account_zero [simp]: "bulk_update_account n \<rho> i 0 = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bulk_update_account n \<rho> i 0 = 0
[PROOF STEP]
by (metis add_cancel_right_left bulk_update_account_plus)


[STATEMENT]
lemma bulk_update_account_uminus:
  "bulk_update_account n \<rho> i (-\<alpha>) = - bulk_update_account n \<rho> i \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bulk_update_account n \<rho> i (- \<alpha>) = - bulk_update_account n \<rho> i \<alpha>
[PROOF STEP]
by (metis add_eq_0_iff bulk_update_account_plus bulk_update_account_zero)


[STATEMENT]
lemma bulk_update_account_subtract:
  "bulk_update_account n \<rho> i (\<alpha> - \<beta>) =
     bulk_update_account n \<rho> i \<alpha> - bulk_update_account n \<rho> i \<beta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bulk_update_account n \<rho> i (\<alpha> - \<beta>) = bulk_update_account n \<rho> i \<alpha> - bulk_update_account n \<rho> i \<beta>
[PROOF STEP]
by (simp add: additive.diff additive_def bulk_update_account_plus)