[STATEMENT]
lemma (in disc_market_pos_stock) arbitrage_portfolio_properties:
  assumes "price_structure der matur \<pi> pr"
  and "replicating_portfolio pf der matur"
  and  "(coincides_on Mkt Mkt2 (stocks Mkt))"
  and "(prices Mkt2 x = pr)"
  and "x\<notin> stocks Mkt"
  and "diff_inv = (\<pi> - initial_value pf) / constant_image (prices Mkt pos_stock 0)"
  and "diff_inv \<noteq> 0"
  and "arb_pf = (\<lambda> (x::'b) (n::nat) (w::'a). 0::real)(x:= (\<lambda> n w. -1), pos_stock := (\<lambda> n w. diff_inv))"
  and "contr_pf = qty_sum arb_pf pf"
shows "self_financing Mkt2 contr_pf"
  and "trading_strategy contr_pf"
  and "\<forall>w\<in> space M. cls_val_process Mkt2 contr_pf 0 w = 0"
  and "0 < diff_inv \<longrightarrow> (AE w in M. 0 < cls_val_process Mkt2 contr_pf matur w)"
  and "diff_inv < 0 \<longrightarrow> (AE w in M. 0 > cls_val_process Mkt2 contr_pf matur w)"
  and "support_set arb_pf = {x, pos_stock}"
  and "portfolio contr_pf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (self_financing Mkt2 contr_pf &&& trading_strategy contr_pf &&& \<forall>w\<in>space M. cls_val_process Mkt2 contr_pf 0 w = 0) &&& (0 < diff_inv \<longrightarrow> (AE w in M. 0 < cls_val_process Mkt2 contr_pf matur w) &&& diff_inv < 0 \<longrightarrow> (AE w in M. cls_val_process Mkt2 contr_pf matur w < 0)) &&& support_set arb_pf = {x, pos_stock} &&& portfolio contr_pf
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. self_financing Mkt2 contr_pf
 2. trading_strategy contr_pf
 3. \<forall>w\<in>space M. cls_val_process Mkt2 contr_pf 0 w = 0
 4. 0 < diff_inv \<longrightarrow> (AE w in M. 0 < cls_val_process Mkt2 contr_pf matur w)
 5. diff_inv < 0 \<longrightarrow> (AE w in M. cls_val_process Mkt2 contr_pf matur w < 0)
 6. support_set arb_pf = {x, pos_stock}
 7. portfolio contr_pf
[PROOF STEP]
have "0 < constant_image (prices Mkt pos_stock 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < constant_image (prices Mkt pos_stock 0)
[PROOF STEP]
using trading_strategy_init
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>trading_strategy ?p; support_adapt Mkt ?p\<rbrakk> \<Longrightarrow> \<exists>c. \<forall>w\<in>space M. val_process Mkt ?p 0 w = c

goal (1 subgoal):
 1. 0 < constant_image (prices Mkt pos_stock 0)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>p. \<lbrakk>trading_strategy p; support_adapt Mkt p\<rbrakk> \<Longrightarrow> \<exists>c. \<forall>w\<in>space M. val_process Mkt p 0 w = c) \<Longrightarrow> 0 < constant_image (prices Mkt pos_stock 0)
[PROOF STEP]
have "borel_adapt_stoch_proc F (prices Mkt pos_stock)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. borel_adapt_stoch_proc F (prices Mkt pos_stock)
[PROOF STEP]
using pos_stock_borel_adapted
[PROOF STATE]
proof (prove)
using this:
borel_adapt_stoch_proc F (prices Mkt pos_stock)

goal (1 subgoal):
 1. borel_adapt_stoch_proc F (prices Mkt pos_stock)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
borel_adapt_stoch_proc F (prices Mkt pos_stock)

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>trading_strategy p; support_adapt Mkt p\<rbrakk> \<Longrightarrow> \<exists>c. \<forall>w\<in>space M. val_process Mkt p 0 w = c) \<Longrightarrow> 0 < constant_image (prices Mkt pos_stock 0)
[PROOF STEP]
hence "\<exists>c. \<forall>w\<in>space M. prices Mkt pos_stock 0 w = c"
[PROOF STATE]
proof (prove)
using this:
borel_adapt_stoch_proc F (prices Mkt pos_stock)

goal (1 subgoal):
 1. \<exists>c. \<forall>w\<in>space M. prices Mkt pos_stock 0 w = c
[PROOF STEP]
using  adapted_init[of "prices Mkt pos_stock"]
[PROOF STATE]
proof (prove)
using this:
borel_adapt_stoch_proc F (prices Mkt pos_stock)
borel_adapt_stoch_proc F (prices Mkt pos_stock) \<Longrightarrow> \<exists>c. \<forall>w\<in>space M. prices Mkt pos_stock 0 w = c

goal (1 subgoal):
 1. \<exists>c. \<forall>w\<in>space M. prices Mkt pos_stock 0 w = c
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>c. \<forall>w\<in>space M. prices Mkt pos_stock 0 w = c

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>trading_strategy p; support_adapt Mkt p\<rbrakk> \<Longrightarrow> \<exists>c. \<forall>w\<in>space M. val_process Mkt p 0 w = c) \<Longrightarrow> 0 < constant_image (prices Mkt pos_stock 0)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<exists>c. \<forall>w\<in>space M. prices Mkt pos_stock 0 w = c

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>trading_strategy p; support_adapt Mkt p\<rbrakk> \<Longrightarrow> \<exists>c. \<forall>w\<in>space M. val_process Mkt p 0 w = c) \<Longrightarrow> 0 < constant_image (prices Mkt pos_stock 0)
[PROOF STEP]
have "\<forall>w\<in> space M. 0 < prices Mkt pos_stock 0 w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>w\<in>space M. 0 < prices Mkt pos_stock 0 w
[PROOF STEP]
using positive
[PROOF STATE]
proof (prove)
using this:
\<forall>n w. 0 < prices Mkt pos_stock n w

goal (1 subgoal):
 1. \<forall>w\<in>space M. 0 < prices Mkt pos_stock 0 w
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>w\<in>space M. 0 < prices Mkt pos_stock 0 w

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>trading_strategy p; support_adapt Mkt p\<rbrakk> \<Longrightarrow> \<exists>c. \<forall>w\<in>space M. val_process Mkt p 0 w = c) \<Longrightarrow> 0 < constant_image (prices Mkt pos_stock 0)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<exists>c. \<forall>w\<in>space M. prices Mkt pos_stock 0 w = c
\<forall>w\<in>space M. 0 < prices Mkt pos_stock 0 w
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>c. \<forall>w\<in>space M. prices Mkt pos_stock 0 w = c
\<forall>w\<in>space M. 0 < prices Mkt pos_stock 0 w

goal (1 subgoal):
 1. 0 < constant_image (prices Mkt pos_stock 0)
[PROOF STEP]
using constant_image_pos
[PROOF STATE]
proof (prove)
using this:
\<exists>c. \<forall>w\<in>space M. prices Mkt pos_stock 0 w = c
\<forall>w\<in>space M. 0 < prices Mkt pos_stock 0 w
\<lbrakk>\<forall>x\<in>space M. 0 < ?f x; \<exists>c. \<forall>x\<in>space M. ?f x = c\<rbrakk> \<Longrightarrow> 0 < constant_image ?f

goal (1 subgoal):
 1. 0 < constant_image (prices Mkt pos_stock 0)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 < constant_image (prices Mkt pos_stock 0)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
0 < constant_image (prices Mkt pos_stock 0)

goal (7 subgoals):
 1. self_financing Mkt2 contr_pf
 2. trading_strategy contr_pf
 3. \<forall>w\<in>space M. cls_val_process Mkt2 contr_pf 0 w = 0
 4. 0 < diff_inv \<longrightarrow> (AE w in M. 0 < cls_val_process Mkt2 contr_pf matur w)
 5. diff_inv < 0 \<longrightarrow> (AE w in M. cls_val_process Mkt2 contr_pf matur w < 0)
 6. support_set arb_pf = {x, pos_stock}
 7. portfolio contr_pf
[PROOF STEP]
show "support_set arb_pf = {x, pos_stock}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. support_set arb_pf = {x, pos_stock}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. support_set arb_pf = {x, pos_stock}
[PROOF STEP]
have "arb_pf = (\<lambda> (x::'b) (n::nat) (w::'a). 0::real)(x:= (\<lambda> n w. -1), pos_stock := (\<lambda> n w. diff_inv))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. arb_pf = (\<lambda>x n w. 0)(x := \<lambda>n w. - 1, pos_stock := \<lambda>n w. diff_inv)
[PROOF STEP]
using \<open>arb_pf = (\<lambda> (x::'b) (n::nat) (w::'a). 0::real)(x:= (\<lambda> n w. -1), pos_stock := (\<lambda> n w. diff_inv))\<close>
[PROOF STATE]
proof (prove)
using this:
arb_pf = (\<lambda>x n w. 0)(x := \<lambda>n w. - 1, pos_stock := \<lambda>n w. diff_inv)

goal (1 subgoal):
 1. arb_pf = (\<lambda>x n w. 0)(x := \<lambda>n w. - 1, pos_stock := \<lambda>n w. diff_inv)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
arb_pf = (\<lambda>x n w. 0)(x := \<lambda>n w. - 1, pos_stock := \<lambda>n w. diff_inv)

goal (1 subgoal):
 1. support_set arb_pf = {x, pos_stock}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
arb_pf = (\<lambda>x n w. 0)(x := \<lambda>n w. - 1, pos_stock := \<lambda>n w. diff_inv)

goal (1 subgoal):
 1. support_set arb_pf = {x, pos_stock}
[PROOF STEP]
have "\<exists>n w. diff_inv \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>n w. diff_inv \<noteq> 0
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
price_structure der matur \<pi> pr
replicating_portfolio pf der matur
coincides_on Mkt Mkt2 (stocks Mkt)
prices Mkt2 x = pr
x \<notin> stocks Mkt
diff_inv = (\<pi> - initial_value pf) / constant_image (prices Mkt pos_stock 0)
diff_inv \<noteq> 0
arb_pf = (\<lambda>x n w. 0)(x := \<lambda>n w. - 1, pos_stock := \<lambda>n w. diff_inv)
contr_pf = qty_sum arb_pf pf

goal (1 subgoal):
 1. \<exists>n w. diff_inv \<noteq> 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>n w. diff_inv \<noteq> 0

goal (1 subgoal):
 1. support_set arb_pf = {x, pos_stock}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<exists>n w. diff_inv \<noteq> 0

goal (1 subgoal):
 1. support_set arb_pf = {x, pos_stock}
[PROOF STEP]
have "x\<noteq> pos_stock"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<noteq> pos_stock
[PROOF STEP]
using \<open>x \<notin> stocks Mkt\<close> in_stock
[PROOF STATE]
proof (prove)
using this:
x \<notin> stocks Mkt
pos_stock \<in> stocks Mkt

goal (1 subgoal):
 1. x \<noteq> pos_stock
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<noteq> pos_stock

goal (1 subgoal):
 1. support_set arb_pf = {x, pos_stock}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
arb_pf = (\<lambda>x n w. 0)(x := \<lambda>n w. - 1, pos_stock := \<lambda>n w. diff_inv)
\<exists>n w. diff_inv \<noteq> 0
x \<noteq> pos_stock
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
arb_pf = (\<lambda>x n w. 0)(x := \<lambda>n w. - 1, pos_stock := \<lambda>n w. diff_inv)
\<exists>n w. diff_inv \<noteq> 0
x \<noteq> pos_stock

goal (1 subgoal):
 1. support_set arb_pf = {x, pos_stock}
[PROOF STEP]
by (simp add:two_component_support_set)
[PROOF STATE]
proof (state)
this:
support_set arb_pf = {x, pos_stock}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
support_set arb_pf = {x, pos_stock}

goal (6 subgoals):
 1. self_financing Mkt2 contr_pf
 2. trading_strategy contr_pf
 3. \<forall>w\<in>space M. cls_val_process Mkt2 contr_pf 0 w = 0
 4. 0 < diff_inv \<longrightarrow> (AE w in M. 0 < cls_val_process Mkt2 contr_pf matur w)
 5. diff_inv < 0 \<longrightarrow> (AE w in M. cls_val_process Mkt2 contr_pf matur w < 0)
 6. portfolio contr_pf
[PROOF STEP]
hence "portfolio arb_pf"
[PROOF STATE]
proof (prove)
using this:
support_set arb_pf = {x, pos_stock}

goal (1 subgoal):
 1. portfolio arb_pf
[PROOF STEP]
unfolding portfolio_def
[PROOF STATE]
proof (prove)
using this:
support_set arb_pf = {x, pos_stock}

goal (1 subgoal):
 1. finite (support_set arb_pf)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
portfolio arb_pf

goal (6 subgoals):
 1. self_financing Mkt2 contr_pf
 2. trading_strategy contr_pf
 3. \<forall>w\<in>space M. cls_val_process Mkt2 contr_pf 0 w = 0
 4. 0 < diff_inv \<longrightarrow> (AE w in M. 0 < cls_val_process Mkt2 contr_pf matur w)
 5. diff_inv < 0 \<longrightarrow> (AE w in M. cls_val_process Mkt2 contr_pf matur w < 0)
 6. portfolio contr_pf
[PROOF STEP]
have arb_vp:"\<forall>n w. val_process Mkt2 arb_pf n w = prices Mkt2 pos_stock n w * diff_inv - pr n w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n w. val_process Mkt2 arb_pf n w = prices Mkt2 pos_stock n w * diff_inv - pr n w
[PROOF STEP]
proof (intro allI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n w. val_process Mkt2 arb_pf n w = prices Mkt2 pos_stock n w * diff_inv - pr n w
[PROOF STEP]
fix n w
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n w. val_process Mkt2 arb_pf n w = prices Mkt2 pos_stock n w * diff_inv - pr n w
[PROOF STEP]
have "val_process Mkt2 arb_pf n w = prices Mkt2 pos_stock n w * (\<lambda> n w. diff_inv) n w + prices Mkt2 x n w * (\<lambda> n w. -1) n w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_process Mkt2 arb_pf n w = prices Mkt2 pos_stock n w * diff_inv + prices Mkt2 x n w * - 1
[PROOF STEP]
proof (rule two_component_val_process)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. arb_pf = (\<lambda>x n w. 0)(x := \<lambda>a b. - 1, pos_stock := \<lambda>a b. diff_inv)
 2. portfolio arb_pf
 3. x \<noteq> pos_stock
 4. \<exists>n w. - 1 \<noteq> 0
 5. \<exists>n w. diff_inv \<noteq> 0
[PROOF STEP]
show "x\<noteq> pos_stock"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<noteq> pos_stock
[PROOF STEP]
using \<open>x \<notin> stocks Mkt\<close> in_stock
[PROOF STATE]
proof (prove)
using this:
x \<notin> stocks Mkt
pos_stock \<in> stocks Mkt

goal (1 subgoal):
 1. x \<noteq> pos_stock
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<noteq> pos_stock

goal (4 subgoals):
 1. arb_pf = (\<lambda>x n w. 0)(x := \<lambda>a b. - 1, pos_stock := \<lambda>a b. diff_inv)
 2. portfolio arb_pf
 3. \<exists>n w. - 1 \<noteq> 0
 4. \<exists>n w. diff_inv \<noteq> 0
[PROOF STEP]
show "arb_pf = (\<lambda>x n w. 0)(x := \<lambda>a b. - 1, pos_stock := \<lambda>a b. diff_inv)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. arb_pf = (\<lambda>x n w. 0)(x := \<lambda>a b. - 1, pos_stock := \<lambda>a b. diff_inv)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
price_structure der matur \<pi> pr
replicating_portfolio pf der matur
coincides_on Mkt Mkt2 (stocks Mkt)
prices Mkt2 x = pr
x \<notin> stocks Mkt
diff_inv = (\<pi> - initial_value pf) / constant_image (prices Mkt pos_stock 0)
diff_inv \<noteq> 0
arb_pf = (\<lambda>x n w. 0)(x := \<lambda>n w. - 1, pos_stock := \<lambda>n w. diff_inv)
contr_pf = qty_sum arb_pf pf

goal (1 subgoal):
 1. arb_pf = (\<lambda>x n w. 0)(x := \<lambda>a b. - 1, pos_stock := \<lambda>a b. diff_inv)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
arb_pf = (\<lambda>x n w. 0)(x := \<lambda>a b. - 1, pos_stock := \<lambda>a b. diff_inv)

goal (3 subgoals):
 1. portfolio arb_pf
 2. \<exists>n w. - 1 \<noteq> 0
 3. \<exists>n w. diff_inv \<noteq> 0
[PROOF STEP]
show "portfolio arb_pf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. portfolio arb_pf
[PROOF STEP]
using \<open>portfolio arb_pf\<close>
[PROOF STATE]
proof (prove)
using this:
portfolio arb_pf

goal (1 subgoal):
 1. portfolio arb_pf
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
portfolio arb_pf

goal (2 subgoals):
 1. \<exists>n w. - 1 \<noteq> 0
 2. \<exists>n w. diff_inv \<noteq> 0
[PROOF STEP]
show "\<exists>n w. - (1::real) \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>n w. - 1 \<noteq> 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>n w. - 1 \<noteq> 0

goal (1 subgoal):
 1. \<exists>n w. diff_inv \<noteq> 0
[PROOF STEP]
show "\<exists>n w. diff_inv \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>n w. diff_inv \<noteq> 0
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
price_structure der matur \<pi> pr
replicating_portfolio pf der matur
coincides_on Mkt Mkt2 (stocks Mkt)
prices Mkt2 x = pr
x \<notin> stocks Mkt
diff_inv = (\<pi> - initial_value pf) / constant_image (prices Mkt pos_stock 0)
diff_inv \<noteq> 0
arb_pf = (\<lambda>x n w. 0)(x := \<lambda>n w. - 1, pos_stock := \<lambda>n w. diff_inv)
contr_pf = qty_sum arb_pf pf

goal (1 subgoal):
 1. \<exists>n w. diff_inv \<noteq> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>n w. diff_inv \<noteq> 0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
val_process Mkt2 arb_pf n w = prices Mkt2 pos_stock n w * diff_inv + prices Mkt2 x n w * - 1

goal (1 subgoal):
 1. \<And>n w. val_process Mkt2 arb_pf n w = prices Mkt2 pos_stock n w * diff_inv - pr n w
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
val_process Mkt2 arb_pf n w = prices Mkt2 pos_stock n w * diff_inv + prices Mkt2 x n w * - 1

goal (1 subgoal):
 1. \<And>n w. val_process Mkt2 arb_pf n w = prices Mkt2 pos_stock n w * diff_inv - pr n w
[PROOF STEP]
have "... = prices Mkt2 pos_stock n w * diff_inv - pr n w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prices Mkt2 pos_stock n w * diff_inv + prices Mkt2 x n w * - 1 = prices Mkt2 pos_stock n w * diff_inv - pr n w
[PROOF STEP]
using \<open>prices Mkt2 x = pr\<close>
[PROOF STATE]
proof (prove)
using this:
prices Mkt2 x = pr

goal (1 subgoal):
 1. prices Mkt2 pos_stock n w * diff_inv + prices Mkt2 x n w * - 1 = prices Mkt2 pos_stock n w * diff_inv - pr n w
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
prices Mkt2 pos_stock n w * diff_inv + prices Mkt2 x n w * - 1 = prices Mkt2 pos_stock n w * diff_inv - pr n w

goal (1 subgoal):
 1. \<And>n w. val_process Mkt2 arb_pf n w = prices Mkt2 pos_stock n w * diff_inv - pr n w
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
val_process Mkt2 arb_pf n w = prices Mkt2 pos_stock n w * diff_inv - pr n w
[PROOF STEP]
show "val_process Mkt2 arb_pf n w = prices Mkt2 pos_stock n w * diff_inv - pr n w"
[PROOF STATE]
proof (prove)
using this:
val_process Mkt2 arb_pf n w = prices Mkt2 pos_stock n w * diff_inv - pr n w

goal (1 subgoal):
 1. val_process Mkt2 arb_pf n w = prices Mkt2 pos_stock n w * diff_inv - pr n w
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
val_process Mkt2 arb_pf n w = prices Mkt2 pos_stock n w * diff_inv - pr n w

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>n w. val_process Mkt2 arb_pf n w = prices Mkt2 pos_stock n w * diff_inv - pr n w

goal (6 subgoals):
 1. self_financing Mkt2 contr_pf
 2. trading_strategy contr_pf
 3. \<forall>w\<in>space M. cls_val_process Mkt2 contr_pf 0 w = 0
 4. 0 < diff_inv \<longrightarrow> (AE w in M. 0 < cls_val_process Mkt2 contr_pf matur w)
 5. diff_inv < 0 \<longrightarrow> (AE w in M. cls_val_process Mkt2 contr_pf matur w < 0)
 6. portfolio contr_pf
[PROOF STEP]
have "static_quantities arb_pf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. static_quantities arb_pf
[PROOF STEP]
unfolding static_quantities_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>asset\<in>support_set arb_pf. \<exists>c. arb_pf asset = (\<lambda>n w. c)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>asset. asset \<in> support_set arb_pf \<Longrightarrow> \<exists>c. arb_pf asset = (\<lambda>n w. c)
[PROOF STEP]
fix asset
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>asset. asset \<in> support_set arb_pf \<Longrightarrow> \<exists>c. arb_pf asset = (\<lambda>n w. c)
[PROOF STEP]
assume "asset \<in> support_set arb_pf"
[PROOF STATE]
proof (state)
this:
asset \<in> support_set arb_pf

goal (1 subgoal):
 1. \<And>asset. asset \<in> support_set arb_pf \<Longrightarrow> \<exists>c. arb_pf asset = (\<lambda>n w. c)
[PROOF STEP]
thus "\<exists>c. arb_pf asset = (\<lambda>n w. c)"
[PROOF STATE]
proof (prove)
using this:
asset \<in> support_set arb_pf

goal (1 subgoal):
 1. \<exists>c. arb_pf asset = (\<lambda>n w. c)
[PROOF STEP]
proof (cases "asset = x")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>asset \<in> support_set arb_pf; asset = x\<rbrakk> \<Longrightarrow> \<exists>c. arb_pf asset = (\<lambda>n w. c)
 2. \<lbrakk>asset \<in> support_set arb_pf; asset \<noteq> x\<rbrakk> \<Longrightarrow> \<exists>c. arb_pf asset = (\<lambda>n w. c)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
asset = x

goal (2 subgoals):
 1. \<lbrakk>asset \<in> support_set arb_pf; asset = x\<rbrakk> \<Longrightarrow> \<exists>c. arb_pf asset = (\<lambda>n w. c)
 2. \<lbrakk>asset \<in> support_set arb_pf; asset \<noteq> x\<rbrakk> \<Longrightarrow> \<exists>c. arb_pf asset = (\<lambda>n w. c)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
asset = x

goal (1 subgoal):
 1. \<exists>c. arb_pf asset = (\<lambda>n w. c)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
asset = x
price_structure der matur \<pi> pr
replicating_portfolio pf der matur
coincides_on Mkt Mkt2 (stocks Mkt)
prices Mkt2 x = pr
x \<notin> stocks Mkt
diff_inv = (\<pi> - initial_value pf) / constant_image (prices Mkt pos_stock 0)
diff_inv \<noteq> 0
arb_pf = (\<lambda>x n w. 0)(x := \<lambda>n w. - 1, pos_stock := \<lambda>n w. diff_inv)
contr_pf = qty_sum arb_pf pf

goal (1 subgoal):
 1. \<exists>c. arb_pf asset = (\<lambda>n w. c)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>c. arb_pf asset = (\<lambda>n w. c)

goal (1 subgoal):
 1. \<lbrakk>asset \<in> support_set arb_pf; asset \<noteq> x\<rbrakk> \<Longrightarrow> \<exists>c. arb_pf asset = (\<lambda>n w. c)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>asset \<in> support_set arb_pf; asset \<noteq> x\<rbrakk> \<Longrightarrow> \<exists>c. arb_pf asset = (\<lambda>n w. c)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
asset \<noteq> x

goal (1 subgoal):
 1. \<lbrakk>asset \<in> support_set arb_pf; asset \<noteq> x\<rbrakk> \<Longrightarrow> \<exists>c. arb_pf asset = (\<lambda>n w. c)
[PROOF STEP]
hence "asset = pos_stock"
[PROOF STATE]
proof (prove)
using this:
asset \<noteq> x

goal (1 subgoal):
 1. asset = pos_stock
[PROOF STEP]
using \<open>support_set arb_pf = {x, pos_stock}\<close>
[PROOF STATE]
proof (prove)
using this:
asset \<noteq> x
support_set arb_pf = {x, pos_stock}

goal (1 subgoal):
 1. asset = pos_stock
[PROOF STEP]
using \<open>asset \<in> support_set arb_pf\<close>
[PROOF STATE]
proof (prove)
using this:
asset \<noteq> x
support_set arb_pf = {x, pos_stock}
asset \<in> support_set arb_pf

goal (1 subgoal):
 1. asset = pos_stock
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
asset = pos_stock

goal (1 subgoal):
 1. \<lbrakk>asset \<in> support_set arb_pf; asset \<noteq> x\<rbrakk> \<Longrightarrow> \<exists>c. arb_pf asset = (\<lambda>n w. c)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
asset = pos_stock

goal (1 subgoal):
 1. \<exists>c. arb_pf asset = (\<lambda>n w. c)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
asset = pos_stock
price_structure der matur \<pi> pr
replicating_portfolio pf der matur
coincides_on Mkt Mkt2 (stocks Mkt)
prices Mkt2 x = pr
x \<notin> stocks Mkt
diff_inv = (\<pi> - initial_value pf) / constant_image (prices Mkt pos_stock 0)
diff_inv \<noteq> 0
arb_pf = (\<lambda>x n w. 0)(x := \<lambda>n w. - 1, pos_stock := \<lambda>n w. diff_inv)
contr_pf = qty_sum arb_pf pf

goal (1 subgoal):
 1. \<exists>c. arb_pf asset = (\<lambda>n w. c)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>c. arb_pf asset = (\<lambda>n w. c)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>c. arb_pf asset = (\<lambda>n w. c)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
static_quantities arb_pf

goal (6 subgoals):
 1. self_financing Mkt2 contr_pf
 2. trading_strategy contr_pf
 3. \<forall>w\<in>space M. cls_val_process Mkt2 contr_pf 0 w = 0
 4. 0 < diff_inv \<longrightarrow> (AE w in M. 0 < cls_val_process Mkt2 contr_pf matur w)
 5. diff_inv < 0 \<longrightarrow> (AE w in M. cls_val_process Mkt2 contr_pf matur w < 0)
 6. portfolio contr_pf
[PROOF STEP]
hence "trading_strategy arb_pf"
[PROOF STATE]
proof (prove)
using this:
static_quantities arb_pf

goal (1 subgoal):
 1. trading_strategy arb_pf
[PROOF STEP]
using \<open>portfolio arb_pf\<close> portfolio_def static_quantities_trading_strat
[PROOF STATE]
proof (prove)
using this:
static_quantities arb_pf
portfolio arb_pf
portfolio ?p = finite (support_set ?p)
\<lbrakk>static_quantities ?p; finite (support_set ?p)\<rbrakk> \<Longrightarrow> trading_strategy ?p

goal (1 subgoal):
 1. trading_strategy arb_pf
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
trading_strategy arb_pf

goal (6 subgoals):
 1. self_financing Mkt2 contr_pf
 2. trading_strategy contr_pf
 3. \<forall>w\<in>space M. cls_val_process Mkt2 contr_pf 0 w = 0
 4. 0 < diff_inv \<longrightarrow> (AE w in M. 0 < cls_val_process Mkt2 contr_pf matur w)
 5. diff_inv < 0 \<longrightarrow> (AE w in M. cls_val_process Mkt2 contr_pf matur w < 0)
 6. portfolio contr_pf
[PROOF STEP]
have "self_financing Mkt2 arb_pf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. self_financing Mkt2 arb_pf
[PROOF STEP]
by (simp add: static_portfolio_self_financing \<open>arb_pf = (\<lambda>x n w. 0) (x := \<lambda>n w. -1, pos_stock := \<lambda>n w. diff_inv)\<close>)
[PROOF STATE]
proof (state)
this:
self_financing Mkt2 arb_pf

goal (6 subgoals):
 1. self_financing Mkt2 contr_pf
 2. trading_strategy contr_pf
 3. \<forall>w\<in>space M. cls_val_process Mkt2 contr_pf 0 w = 0
 4. 0 < diff_inv \<longrightarrow> (AE w in M. 0 < cls_val_process Mkt2 contr_pf matur w)
 5. diff_inv < 0 \<longrightarrow> (AE w in M. cls_val_process Mkt2 contr_pf matur w < 0)
 6. portfolio contr_pf
[PROOF STEP]
hence arb_uvp: "\<forall>n w. cls_val_process Mkt2 arb_pf n w = prices Mkt2 pos_stock n w * diff_inv - pr n w"
[PROOF STATE]
proof (prove)
using this:
self_financing Mkt2 arb_pf

goal (1 subgoal):
 1. \<forall>n w. cls_val_process Mkt2 arb_pf n w = prices Mkt2 pos_stock n w * diff_inv - pr n w
[PROOF STEP]
using assms arb_vp
[PROOF STATE]
proof (prove)
using this:
self_financing Mkt2 arb_pf
price_structure der matur \<pi> pr
replicating_portfolio pf der matur
coincides_on Mkt Mkt2 (stocks Mkt)
prices Mkt2 x = pr
x \<notin> stocks Mkt
diff_inv = (\<pi> - initial_value pf) / constant_image (prices Mkt pos_stock 0)
diff_inv \<noteq> 0
arb_pf = (\<lambda>x n w. 0)(x := \<lambda>n w. - 1, pos_stock := \<lambda>n w. diff_inv)
contr_pf = qty_sum arb_pf pf
\<forall>n w. val_process Mkt2 arb_pf n w = prices Mkt2 pos_stock n w * diff_inv - pr n w

goal (1 subgoal):
 1. \<forall>n w. cls_val_process Mkt2 arb_pf n w = prices Mkt2 pos_stock n w * diff_inv - pr n w
[PROOF STEP]
by (simp add:self_financingE)
[PROOF STATE]
proof (state)
this:
\<forall>n w. cls_val_process Mkt2 arb_pf n w = prices Mkt2 pos_stock n w * diff_inv - pr n w

goal (6 subgoals):
 1. self_financing Mkt2 contr_pf
 2. trading_strategy contr_pf
 3. \<forall>w\<in>space M. cls_val_process Mkt2 contr_pf 0 w = 0
 4. 0 < diff_inv \<longrightarrow> (AE w in M. 0 < cls_val_process Mkt2 contr_pf matur w)
 5. diff_inv < 0 \<longrightarrow> (AE w in M. cls_val_process Mkt2 contr_pf matur w < 0)
 6. portfolio contr_pf
[PROOF STEP]
show "portfolio contr_pf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. portfolio contr_pf
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
price_structure der matur \<pi> pr
replicating_portfolio pf der matur
coincides_on Mkt Mkt2 (stocks Mkt)
prices Mkt2 x = pr
x \<notin> stocks Mkt
diff_inv = (\<pi> - initial_value pf) / constant_image (prices Mkt pos_stock 0)
diff_inv \<noteq> 0
arb_pf = (\<lambda>x n w. 0)(x := \<lambda>n w. - 1, pos_stock := \<lambda>n w. diff_inv)
contr_pf = qty_sum arb_pf pf

goal (1 subgoal):
 1. portfolio contr_pf
[PROOF STEP]
by (metis \<open>support_set arb_pf = {x, pos_stock}\<close> replicating_portfolio_def
          finite.emptyI finite.insertI portfolio_def stock_portfolio_def sum_portfolio)
[PROOF STATE]
proof (state)
this:
portfolio contr_pf

goal (5 subgoals):
 1. self_financing Mkt2 contr_pf
 2. trading_strategy contr_pf
 3. \<forall>w\<in>space M. cls_val_process Mkt2 contr_pf 0 w = 0
 4. 0 < diff_inv \<longrightarrow> (AE w in M. 0 < cls_val_process Mkt2 contr_pf matur w)
 5. diff_inv < 0 \<longrightarrow> (AE w in M. cls_val_process Mkt2 contr_pf matur w < 0)
[PROOF STEP]
have "support_set contr_pf \<subseteq> stocks Mkt \<union> {x}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. support_set contr_pf \<subseteq> stocks Mkt \<union> {x}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. support_set contr_pf \<subseteq> stocks Mkt \<union> {x}
[PROOF STEP]
have "support_set contr_pf \<subseteq> support_set arb_pf \<union> support_set pf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. support_set contr_pf \<subseteq> support_set arb_pf \<union> support_set pf
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
price_structure der matur \<pi> pr
replicating_portfolio pf der matur
coincides_on Mkt Mkt2 (stocks Mkt)
prices Mkt2 x = pr
x \<notin> stocks Mkt
diff_inv = (\<pi> - initial_value pf) / constant_image (prices Mkt pos_stock 0)
diff_inv \<noteq> 0
arb_pf = (\<lambda>x n w. 0)(x := \<lambda>n w. - 1, pos_stock := \<lambda>n w. diff_inv)
contr_pf = qty_sum arb_pf pf

goal (1 subgoal):
 1. support_set contr_pf \<subseteq> support_set arb_pf \<union> support_set pf
[PROOF STEP]
by (simp add:sum_support_set)
[PROOF STATE]
proof (state)
this:
support_set contr_pf \<subseteq> support_set arb_pf \<union> support_set pf

goal (1 subgoal):
 1. support_set contr_pf \<subseteq> stocks Mkt \<union> {x}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
support_set contr_pf \<subseteq> support_set arb_pf \<union> support_set pf

goal (1 subgoal):
 1. support_set contr_pf \<subseteq> stocks Mkt \<union> {x}
[PROOF STEP]
have "support_set arb_pf \<subseteq> stocks Mkt \<union> {x}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. support_set arb_pf \<subseteq> stocks Mkt \<union> {x}
[PROOF STEP]
using \<open>support_set arb_pf = {x, pos_stock}\<close> in_stock
[PROOF STATE]
proof (prove)
using this:
support_set arb_pf = {x, pos_stock}
pos_stock \<in> stocks Mkt

goal (1 subgoal):
 1. support_set arb_pf \<subseteq> stocks Mkt \<union> {x}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
support_set arb_pf \<subseteq> stocks Mkt \<union> {x}

goal (1 subgoal):
 1. support_set contr_pf \<subseteq> stocks Mkt \<union> {x}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
support_set arb_pf \<subseteq> stocks Mkt \<union> {x}

goal (1 subgoal):
 1. support_set contr_pf \<subseteq> stocks Mkt \<union> {x}
[PROOF STEP]
have "support_set pf \<subseteq> stocks Mkt \<union> {x}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. support_set pf \<subseteq> stocks Mkt \<union> {x}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
price_structure der matur \<pi> pr
replicating_portfolio pf der matur
coincides_on Mkt Mkt2 (stocks Mkt)
prices Mkt2 x = pr
x \<notin> stocks Mkt
diff_inv = (\<pi> - initial_value pf) / constant_image (prices Mkt pos_stock 0)
diff_inv \<noteq> 0
arb_pf = (\<lambda>x n w. 0)(x := \<lambda>n w. - 1, pos_stock := \<lambda>n w. diff_inv)
contr_pf = qty_sum arb_pf pf

goal (1 subgoal):
 1. support_set pf \<subseteq> stocks Mkt \<union> {x}
[PROOF STEP]
unfolding replicating_portfolio_def
      stock_portfolio_def
[PROOF STATE]
proof (prove)
using this:
price_structure der matur \<pi> pr
(portfolio pf \<and> support_set pf \<subseteq> stocks Mkt) \<and> trading_strategy pf \<and> self_financing Mkt pf \<and> AEeq M (cls_val_process Mkt pf matur) der
coincides_on Mkt Mkt2 (stocks Mkt)
prices Mkt2 x = pr
x \<notin> stocks Mkt
diff_inv = (\<pi> - initial_value pf) / constant_image (prices Mkt pos_stock 0)
diff_inv \<noteq> 0
arb_pf = (\<lambda>x n w. 0)(x := \<lambda>n w. - 1, pos_stock := \<lambda>n w. diff_inv)
contr_pf = qty_sum arb_pf pf

goal (1 subgoal):
 1. support_set pf \<subseteq> stocks Mkt \<union> {x}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
support_set pf \<subseteq> stocks Mkt \<union> {x}

goal (1 subgoal):
 1. support_set contr_pf \<subseteq> stocks Mkt \<union> {x}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
support_set contr_pf \<subseteq> support_set arb_pf \<union> support_set pf
support_set arb_pf \<subseteq> stocks Mkt \<union> {x}
support_set pf \<subseteq> stocks Mkt \<union> {x}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
support_set contr_pf \<subseteq> support_set arb_pf \<union> support_set pf
support_set arb_pf \<subseteq> stocks Mkt \<union> {x}
support_set pf \<subseteq> stocks Mkt \<union> {x}

goal (1 subgoal):
 1. support_set contr_pf \<subseteq> stocks Mkt \<union> {x}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
support_set contr_pf \<subseteq> stocks Mkt \<union> {x}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
support_set contr_pf \<subseteq> stocks Mkt \<union> {x}

goal (5 subgoals):
 1. self_financing Mkt2 contr_pf
 2. trading_strategy contr_pf
 3. \<forall>w\<in>space M. cls_val_process Mkt2 contr_pf 0 w = 0
 4. 0 < diff_inv \<longrightarrow> (AE w in M. 0 < cls_val_process Mkt2 contr_pf matur w)
 5. diff_inv < 0 \<longrightarrow> (AE w in M. cls_val_process Mkt2 contr_pf matur w < 0)
[PROOF STEP]
show "self_financing Mkt2 contr_pf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. self_financing Mkt2 contr_pf
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. self_financing Mkt2 contr_pf
[PROOF STEP]
have "self_financing Mkt2 (qty_sum arb_pf pf)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. self_financing Mkt2 (qty_sum arb_pf pf)
[PROOF STEP]
proof (rule sum_self_financing)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. portfolio arb_pf
 2. portfolio pf
 3. self_financing Mkt2 arb_pf
 4. self_financing Mkt2 pf
[PROOF STEP]
show "portfolio arb_pf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. portfolio arb_pf
[PROOF STEP]
using  \<open>support_set arb_pf = {x, pos_stock}\<close>
[PROOF STATE]
proof (prove)
using this:
support_set arb_pf = {x, pos_stock}

goal (1 subgoal):
 1. portfolio arb_pf
[PROOF STEP]
unfolding portfolio_def
[PROOF STATE]
proof (prove)
using this:
support_set arb_pf = {x, pos_stock}

goal (1 subgoal):
 1. finite (support_set arb_pf)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
portfolio arb_pf

goal (3 subgoals):
 1. portfolio pf
 2. self_financing Mkt2 arb_pf
 3. self_financing Mkt2 pf
[PROOF STEP]
show "portfolio pf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. portfolio pf
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
price_structure der matur \<pi> pr
replicating_portfolio pf der matur
coincides_on Mkt Mkt2 (stocks Mkt)
prices Mkt2 x = pr
x \<notin> stocks Mkt
diff_inv = (\<pi> - initial_value pf) / constant_image (prices Mkt pos_stock 0)
diff_inv \<noteq> 0
arb_pf = (\<lambda>x n w. 0)(x := \<lambda>n w. - 1, pos_stock := \<lambda>n w. diff_inv)
contr_pf = qty_sum arb_pf pf

goal (1 subgoal):
 1. portfolio pf
[PROOF STEP]
unfolding replicating_portfolio_def stock_portfolio_def
[PROOF STATE]
proof (prove)
using this:
price_structure der matur \<pi> pr
(portfolio pf \<and> support_set pf \<subseteq> stocks Mkt) \<and> trading_strategy pf \<and> self_financing Mkt pf \<and> AEeq M (cls_val_process Mkt pf matur) der
coincides_on Mkt Mkt2 (stocks Mkt)
prices Mkt2 x = pr
x \<notin> stocks Mkt
diff_inv = (\<pi> - initial_value pf) / constant_image (prices Mkt pos_stock 0)
diff_inv \<noteq> 0
arb_pf = (\<lambda>x n w. 0)(x := \<lambda>n w. - 1, pos_stock := \<lambda>n w. diff_inv)
contr_pf = qty_sum arb_pf pf

goal (1 subgoal):
 1. portfolio pf
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
portfolio pf

goal (2 subgoals):
 1. self_financing Mkt2 arb_pf
 2. self_financing Mkt2 pf
[PROOF STEP]
show "self_financing Mkt2 pf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. self_financing Mkt2 pf
[PROOF STEP]
using coincides_on_self_financing
        \<open>(coincides_on Mkt Mkt2 (stocks Mkt))\<close> \<open>(prices Mkt2 x = pr)\<close> assms(2)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>coincides_on ?Mkt ?Mkt2.0 ?A; support_set ?p \<subseteq> ?A; self_financing ?Mkt ?p\<rbrakk> \<Longrightarrow> self_financing ?Mkt2.0 ?p
coincides_on Mkt Mkt2 (stocks Mkt)
prices Mkt2 x = pr
replicating_portfolio pf der matur

goal (1 subgoal):
 1. self_financing Mkt2 pf
[PROOF STEP]
unfolding replicating_portfolio_def stock_portfolio_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>coincides_on ?Mkt ?Mkt2.0 ?A; support_set ?p \<subseteq> ?A; self_financing ?Mkt ?p\<rbrakk> \<Longrightarrow> self_financing ?Mkt2.0 ?p
coincides_on Mkt Mkt2 (stocks Mkt)
prices Mkt2 x = pr
(portfolio pf \<and> support_set pf \<subseteq> stocks Mkt) \<and> trading_strategy pf \<and> self_financing Mkt pf \<and> AEeq M (cls_val_process Mkt pf matur) der

goal (1 subgoal):
 1. self_financing Mkt2 pf
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
self_financing Mkt2 pf

goal (1 subgoal):
 1. self_financing Mkt2 arb_pf
[PROOF STEP]
show "self_financing Mkt2 arb_pf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. self_financing Mkt2 arb_pf
[PROOF STEP]
by (simp add: static_portfolio_self_financing \<open>arb_pf = (\<lambda>x n w. 0) (x := \<lambda>n w. -1, pos_stock := \<lambda>n w. diff_inv)\<close>)
[PROOF STATE]
proof (state)
this:
self_financing Mkt2 arb_pf

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
self_financing Mkt2 (qty_sum arb_pf pf)

goal (1 subgoal):
 1. self_financing Mkt2 contr_pf
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
self_financing Mkt2 (qty_sum arb_pf pf)

goal (1 subgoal):
 1. self_financing Mkt2 contr_pf
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
self_financing Mkt2 (qty_sum arb_pf pf)
price_structure der matur \<pi> pr
replicating_portfolio pf der matur
coincides_on Mkt Mkt2 (stocks Mkt)
prices Mkt2 x = pr
x \<notin> stocks Mkt
diff_inv = (\<pi> - initial_value pf) / constant_image (prices Mkt pos_stock 0)
diff_inv \<noteq> 0
arb_pf = (\<lambda>x n w. 0)(x := \<lambda>n w. - 1, pos_stock := \<lambda>n w. diff_inv)
contr_pf = qty_sum arb_pf pf

goal (1 subgoal):
 1. self_financing Mkt2 contr_pf
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
self_financing Mkt2 contr_pf

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
self_financing Mkt2 contr_pf

goal (4 subgoals):
 1. trading_strategy contr_pf
 2. \<forall>w\<in>space M. cls_val_process Mkt2 contr_pf 0 w = 0
 3. 0 < diff_inv \<longrightarrow> (AE w in M. 0 < cls_val_process Mkt2 contr_pf matur w)
 4. diff_inv < 0 \<longrightarrow> (AE w in M. cls_val_process Mkt2 contr_pf matur w < 0)
[PROOF STEP]
show "trading_strategy contr_pf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trading_strategy contr_pf
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. trading_strategy contr_pf
[PROOF STEP]
have "trading_strategy (qty_sum arb_pf pf)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trading_strategy (qty_sum arb_pf pf)
[PROOF STEP]
proof (rule sum_trading_strat)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. trading_strategy arb_pf
 2. trading_strategy pf
[PROOF STEP]
show "trading_strategy pf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trading_strategy pf
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
price_structure der matur \<pi> pr
replicating_portfolio pf der matur
coincides_on Mkt Mkt2 (stocks Mkt)
prices Mkt2 x = pr
x \<notin> stocks Mkt
diff_inv = (\<pi> - initial_value pf) / constant_image (prices Mkt pos_stock 0)
diff_inv \<noteq> 0
arb_pf = (\<lambda>x n w. 0)(x := \<lambda>n w. - 1, pos_stock := \<lambda>n w. diff_inv)
contr_pf = qty_sum arb_pf pf

goal (1 subgoal):
 1. trading_strategy pf
[PROOF STEP]
unfolding replicating_portfolio_def
[PROOF STATE]
proof (prove)
using this:
price_structure der matur \<pi> pr
stock_portfolio Mkt pf \<and> trading_strategy pf \<and> self_financing Mkt pf \<and> AEeq M (cls_val_process Mkt pf matur) der
coincides_on Mkt Mkt2 (stocks Mkt)
prices Mkt2 x = pr
x \<notin> stocks Mkt
diff_inv = (\<pi> - initial_value pf) / constant_image (prices Mkt pos_stock 0)
diff_inv \<noteq> 0
arb_pf = (\<lambda>x n w. 0)(x := \<lambda>n w. - 1, pos_stock := \<lambda>n w. diff_inv)
contr_pf = qty_sum arb_pf pf

goal (1 subgoal):
 1. trading_strategy pf
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
trading_strategy pf

goal (1 subgoal):
 1. trading_strategy arb_pf
[PROOF STEP]
show "trading_strategy arb_pf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trading_strategy arb_pf
[PROOF STEP]
using \<open>trading_strategy arb_pf\<close>
[PROOF STATE]
proof (prove)
using this:
trading_strategy arb_pf

goal (1 subgoal):
 1. trading_strategy arb_pf
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
trading_strategy arb_pf

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
trading_strategy (qty_sum arb_pf pf)

goal (1 subgoal):
 1. trading_strategy contr_pf
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
trading_strategy (qty_sum arb_pf pf)

goal (1 subgoal):
 1. trading_strategy contr_pf
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
trading_strategy (qty_sum arb_pf pf)
price_structure der matur \<pi> pr
replicating_portfolio pf der matur
coincides_on Mkt Mkt2 (stocks Mkt)
prices Mkt2 x = pr
x \<notin> stocks Mkt
diff_inv = (\<pi> - initial_value pf) / constant_image (prices Mkt pos_stock 0)
diff_inv \<noteq> 0
arb_pf = (\<lambda>x n w. 0)(x := \<lambda>n w. - 1, pos_stock := \<lambda>n w. diff_inv)
contr_pf = qty_sum arb_pf pf

goal (1 subgoal):
 1. trading_strategy contr_pf
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
trading_strategy contr_pf

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
trading_strategy contr_pf

goal (3 subgoals):
 1. \<forall>w\<in>space M. cls_val_process Mkt2 contr_pf 0 w = 0
 2. 0 < diff_inv \<longrightarrow> (AE w in M. 0 < cls_val_process Mkt2 contr_pf matur w)
 3. diff_inv < 0 \<longrightarrow> (AE w in M. cls_val_process Mkt2 contr_pf matur w < 0)
[PROOF STEP]
show "\<forall>w\<in> space M. cls_val_process Mkt2 contr_pf 0 w = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>w\<in>space M. cls_val_process Mkt2 contr_pf 0 w = 0
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>w. w \<in> space M \<Longrightarrow> cls_val_process Mkt2 contr_pf 0 w = 0
[PROOF STEP]
fix w
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>w. w \<in> space M \<Longrightarrow> cls_val_process Mkt2 contr_pf 0 w = 0
[PROOF STEP]
assume "w\<in> space M"
[PROOF STATE]
proof (state)
this:
w \<in> space M

goal (1 subgoal):
 1. \<And>w. w \<in> space M \<Longrightarrow> cls_val_process Mkt2 contr_pf 0 w = 0
[PROOF STEP]
have "cls_val_process Mkt2 contr_pf 0 w = cls_val_process Mkt2 arb_pf 0 w + cls_val_process Mkt2 pf 0 w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cls_val_process Mkt2 contr_pf 0 w = cls_val_process Mkt2 arb_pf 0 w + cls_val_process Mkt2 pf 0 w
[PROOF STEP]
using sum_cls_val_process0[of arb_pf pf Mkt2]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>portfolio arb_pf; portfolio pf\<rbrakk> \<Longrightarrow> \<forall>w. cls_val_process Mkt2 (qty_sum arb_pf pf) 0 w = cls_val_process Mkt2 arb_pf 0 w + cls_val_process Mkt2 pf 0 w

goal (1 subgoal):
 1. cls_val_process Mkt2 contr_pf 0 w = cls_val_process Mkt2 arb_pf 0 w + cls_val_process Mkt2 pf 0 w
[PROOF STEP]
using \<open>portfolio arb_pf\<close> assms replicating_portfolio_def stock_portfolio_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>portfolio arb_pf; portfolio pf\<rbrakk> \<Longrightarrow> \<forall>w. cls_val_process Mkt2 (qty_sum arb_pf pf) 0 w = cls_val_process Mkt2 arb_pf 0 w + cls_val_process Mkt2 pf 0 w
portfolio arb_pf
price_structure der matur \<pi> pr
replicating_portfolio pf der matur
coincides_on Mkt Mkt2 (stocks Mkt)
prices Mkt2 x = pr
x \<notin> stocks Mkt
diff_inv = (\<pi> - initial_value pf) / constant_image (prices Mkt pos_stock 0)
diff_inv \<noteq> 0
arb_pf = (\<lambda>x n w. 0)(x := \<lambda>n w. - 1, pos_stock := \<lambda>n w. diff_inv)
contr_pf = qty_sum arb_pf pf
replicating_portfolio ?pf ?der ?matur = (stock_portfolio Mkt ?pf \<and> trading_strategy ?pf \<and> self_financing Mkt ?pf \<and> AEeq M (cls_val_process Mkt ?pf ?matur) ?der)
stock_portfolio ?Mkt ?p = (portfolio ?p \<and> support_set ?p \<subseteq> stocks ?Mkt)

goal (1 subgoal):
 1. cls_val_process Mkt2 contr_pf 0 w = cls_val_process Mkt2 arb_pf 0 w + cls_val_process Mkt2 pf 0 w
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
cls_val_process Mkt2 contr_pf 0 w = cls_val_process Mkt2 arb_pf 0 w + cls_val_process Mkt2 pf 0 w

goal (1 subgoal):
 1. \<And>w. w \<in> space M \<Longrightarrow> cls_val_process Mkt2 contr_pf 0 w = 0
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
cls_val_process Mkt2 contr_pf 0 w = cls_val_process Mkt2 arb_pf 0 w + cls_val_process Mkt2 pf 0 w

goal (1 subgoal):
 1. \<And>w. w \<in> space M \<Longrightarrow> cls_val_process Mkt2 contr_pf 0 w = 0
[PROOF STEP]
have "... = prices Mkt2 pos_stock 0 w * diff_inv - pr 0 w + cls_val_process Mkt2 pf 0 w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cls_val_process Mkt2 arb_pf 0 w + cls_val_process Mkt2 pf 0 w = prices Mkt2 pos_stock 0 w * diff_inv - pr 0 w + cls_val_process Mkt2 pf 0 w
[PROOF STEP]
using arb_uvp
[PROOF STATE]
proof (prove)
using this:
\<forall>n w. cls_val_process Mkt2 arb_pf n w = prices Mkt2 pos_stock n w * diff_inv - pr n w

goal (1 subgoal):
 1. cls_val_process Mkt2 arb_pf 0 w + cls_val_process Mkt2 pf 0 w = prices Mkt2 pos_stock 0 w * diff_inv - pr 0 w + cls_val_process Mkt2 pf 0 w
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cls_val_process Mkt2 arb_pf 0 w + cls_val_process Mkt2 pf 0 w = prices Mkt2 pos_stock 0 w * diff_inv - pr 0 w + cls_val_process Mkt2 pf 0 w

goal (1 subgoal):
 1. \<And>w. w \<in> space M \<Longrightarrow> cls_val_process Mkt2 contr_pf 0 w = 0
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
cls_val_process Mkt2 arb_pf 0 w + cls_val_process Mkt2 pf 0 w = prices Mkt2 pos_stock 0 w * diff_inv - pr 0 w + cls_val_process Mkt2 pf 0 w

goal (1 subgoal):
 1. \<And>w. w \<in> space M \<Longrightarrow> cls_val_process Mkt2 contr_pf 0 w = 0
[PROOF STEP]
have "... = constant_image (prices Mkt pos_stock 0) * diff_inv - pr 0 w + cls_val_process Mkt2 pf 0 w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prices Mkt2 pos_stock 0 w * diff_inv - pr 0 w + cls_val_process Mkt2 pf 0 w = constant_image (prices Mkt pos_stock 0) * diff_inv - pr 0 w + cls_val_process Mkt2 pf 0 w
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. prices Mkt2 pos_stock 0 w * diff_inv - pr 0 w + cls_val_process Mkt2 pf 0 w = constant_image (prices Mkt pos_stock 0) * diff_inv - pr 0 w + cls_val_process Mkt2 pf 0 w
[PROOF STEP]
have f1: "prices Mkt pos_stock = prices Mkt2 pos_stock"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prices Mkt pos_stock = prices Mkt2 pos_stock
[PROOF STEP]
using \<open>coincides_on Mkt Mkt2 (stocks Mkt)\<close>  in_stock
[PROOF STATE]
proof (prove)
using this:
coincides_on Mkt Mkt2 (stocks Mkt)
pos_stock \<in> stocks Mkt

goal (1 subgoal):
 1. prices Mkt pos_stock = prices Mkt2 pos_stock
[PROOF STEP]
unfolding coincides_on_def
[PROOF STATE]
proof (prove)
using this:
stocks Mkt = stocks Mkt2 \<and> (\<forall>x. x \<in> stocks Mkt \<longrightarrow> prices Mkt x = prices Mkt2 x)
pos_stock \<in> stocks Mkt

goal (1 subgoal):
 1. prices Mkt pos_stock = prices Mkt2 pos_stock
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
prices Mkt pos_stock = prices Mkt2 pos_stock

goal (1 subgoal):
 1. prices Mkt2 pos_stock 0 w * diff_inv - pr 0 w + cls_val_process Mkt2 pf 0 w = constant_image (prices Mkt pos_stock 0) * diff_inv - pr 0 w + cls_val_process Mkt2 pf 0 w
[PROOF STEP]
have "prices Mkt pos_stock 0 w = constant_image (prices Mkt pos_stock 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prices Mkt pos_stock 0 w = constant_image (prices Mkt pos_stock 0)
[PROOF STEP]
using \<open>w \<in> space M\<close> adapted_init constant_imageI pos_stock_borel_adapted
[PROOF STATE]
proof (prove)
using this:
w \<in> space M
borel_adapt_stoch_proc F ?x \<Longrightarrow> \<exists>c. \<forall>w\<in>space M. ?x 0 w = c
\<exists>c. \<forall>x\<in>space M. ?f x = c \<Longrightarrow> \<forall>x\<in>space M. ?f x = constant_image ?f
borel_adapt_stoch_proc F (prices Mkt pos_stock)

goal (1 subgoal):
 1. prices Mkt pos_stock 0 w = constant_image (prices Mkt pos_stock 0)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
prices Mkt pos_stock 0 w = constant_image (prices Mkt pos_stock 0)

goal (1 subgoal):
 1. prices Mkt2 pos_stock 0 w * diff_inv - pr 0 w + cls_val_process Mkt2 pf 0 w = constant_image (prices Mkt pos_stock 0) * diff_inv - pr 0 w + cls_val_process Mkt2 pf 0 w
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
prices Mkt pos_stock 0 w = constant_image (prices Mkt pos_stock 0)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
prices Mkt pos_stock 0 w = constant_image (prices Mkt pos_stock 0)

goal (1 subgoal):
 1. prices Mkt2 pos_stock 0 w * diff_inv - pr 0 w + cls_val_process Mkt2 pf 0 w = constant_image (prices Mkt pos_stock 0) * diff_inv - pr 0 w + cls_val_process Mkt2 pf 0 w
[PROOF STEP]
using f1
[PROOF STATE]
proof (prove)
using this:
prices Mkt pos_stock 0 w = constant_image (prices Mkt pos_stock 0)
prices Mkt pos_stock = prices Mkt2 pos_stock

goal (1 subgoal):
 1. prices Mkt2 pos_stock 0 w * diff_inv - pr 0 w + cls_val_process Mkt2 pf 0 w = constant_image (prices Mkt pos_stock 0) * diff_inv - pr 0 w + cls_val_process Mkt2 pf 0 w
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
prices Mkt2 pos_stock 0 w * diff_inv - pr 0 w + cls_val_process Mkt2 pf 0 w = constant_image (prices Mkt pos_stock 0) * diff_inv - pr 0 w + cls_val_process Mkt2 pf 0 w

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
prices Mkt2 pos_stock 0 w * diff_inv - pr 0 w + cls_val_process Mkt2 pf 0 w = constant_image (prices Mkt pos_stock 0) * diff_inv - pr 0 w + cls_val_process Mkt2 pf 0 w

goal (1 subgoal):
 1. \<And>w. w \<in> space M \<Longrightarrow> cls_val_process Mkt2 contr_pf 0 w = 0
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
prices Mkt2 pos_stock 0 w * diff_inv - pr 0 w + cls_val_process Mkt2 pf 0 w = constant_image (prices Mkt pos_stock 0) * diff_inv - pr 0 w + cls_val_process Mkt2 pf 0 w

goal (1 subgoal):
 1. \<And>w. w \<in> space M \<Longrightarrow> cls_val_process Mkt2 contr_pf 0 w = 0
[PROOF STEP]
have "... = (\<pi> - initial_value pf) - pr 0 w + cls_val_process Mkt2 pf 0 w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. constant_image (prices Mkt pos_stock 0) * diff_inv - pr 0 w + cls_val_process Mkt2 pf 0 w = \<pi> - initial_value pf - pr 0 w + cls_val_process Mkt2 pf 0 w
[PROOF STEP]
using \<open>0 < constant_image (prices Mkt pos_stock 0)\<close> assms
[PROOF STATE]
proof (prove)
using this:
0 < constant_image (prices Mkt pos_stock 0)
price_structure der matur \<pi> pr
replicating_portfolio pf der matur
coincides_on Mkt Mkt2 (stocks Mkt)
prices Mkt2 x = pr
x \<notin> stocks Mkt
diff_inv = (\<pi> - initial_value pf) / constant_image (prices Mkt pos_stock 0)
diff_inv \<noteq> 0
arb_pf = (\<lambda>x n w. 0)(x := \<lambda>n w. - 1, pos_stock := \<lambda>n w. diff_inv)
contr_pf = qty_sum arb_pf pf

goal (1 subgoal):
 1. constant_image (prices Mkt pos_stock 0) * diff_inv - pr 0 w + cls_val_process Mkt2 pf 0 w = \<pi> - initial_value pf - pr 0 w + cls_val_process Mkt2 pf 0 w
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
constant_image (prices Mkt pos_stock 0) * diff_inv - pr 0 w + cls_val_process Mkt2 pf 0 w = \<pi> - initial_value pf - pr 0 w + cls_val_process Mkt2 pf 0 w

goal (1 subgoal):
 1. \<And>w. w \<in> space M \<Longrightarrow> cls_val_process Mkt2 contr_pf 0 w = 0
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
constant_image (prices Mkt pos_stock 0) * diff_inv - pr 0 w + cls_val_process Mkt2 pf 0 w = \<pi> - initial_value pf - pr 0 w + cls_val_process Mkt2 pf 0 w

goal (1 subgoal):
 1. \<And>w. w \<in> space M \<Longrightarrow> cls_val_process Mkt2 contr_pf 0 w = 0
[PROOF STEP]
have "... = (\<pi> - initial_value pf) - \<pi> + cls_val_process Mkt2 pf 0 w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> - initial_value pf - pr 0 w + cls_val_process Mkt2 pf 0 w = \<pi> - initial_value pf - \<pi> + cls_val_process Mkt2 pf 0 w
[PROOF STEP]
using \<open>price_structure der matur \<pi> pr\<close>
      price_structure_init[of der matur \<pi> pr]
[PROOF STATE]
proof (prove)
using this:
price_structure der matur \<pi> pr
price_structure der matur \<pi> pr \<Longrightarrow> \<forall>w\<in>space M. pr 0 w = \<pi>

goal (1 subgoal):
 1. \<pi> - initial_value pf - pr 0 w + cls_val_process Mkt2 pf 0 w = \<pi> - initial_value pf - \<pi> + cls_val_process Mkt2 pf 0 w
[PROOF STEP]
by (simp add: \<open>w \<in> space M\<close>)
[PROOF STATE]
proof (state)
this:
\<pi> - initial_value pf - pr 0 w + cls_val_process Mkt2 pf 0 w = \<pi> - initial_value pf - \<pi> + cls_val_process Mkt2 pf 0 w

goal (1 subgoal):
 1. \<And>w. w \<in> space M \<Longrightarrow> cls_val_process Mkt2 contr_pf 0 w = 0
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<pi> - initial_value pf - pr 0 w + cls_val_process Mkt2 pf 0 w = \<pi> - initial_value pf - \<pi> + cls_val_process Mkt2 pf 0 w

goal (1 subgoal):
 1. \<And>w. w \<in> space M \<Longrightarrow> cls_val_process Mkt2 contr_pf 0 w = 0
[PROOF STEP]
have "... = (\<pi> - initial_value pf) - \<pi> + (initial_value pf)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> - initial_value pf - \<pi> + cls_val_process Mkt2 pf 0 w = \<pi> - initial_value pf - \<pi> + initial_value pf
[PROOF STEP]
using initial_valueI assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>trading_strategy ?pf; support_adapt Mkt ?pf\<rbrakk> \<Longrightarrow> \<forall>w\<in>space M. val_process Mkt ?pf 0 w = initial_value ?pf
price_structure der matur \<pi> pr
replicating_portfolio pf der matur
coincides_on Mkt Mkt2 (stocks Mkt)
prices Mkt2 x = pr
x \<notin> stocks Mkt
diff_inv = (\<pi> - initial_value pf) / constant_image (prices Mkt pos_stock 0)
diff_inv \<noteq> 0
arb_pf = (\<lambda>x n w. 0)(x := \<lambda>n w. - 1, pos_stock := \<lambda>n w. diff_inv)
contr_pf = qty_sum arb_pf pf

goal (1 subgoal):
 1. \<pi> - initial_value pf - \<pi> + cls_val_process Mkt2 pf 0 w = \<pi> - initial_value pf - \<pi> + initial_value pf
[PROOF STEP]
unfolding replicating_portfolio_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>trading_strategy ?pf; support_adapt Mkt ?pf\<rbrakk> \<Longrightarrow> \<forall>w\<in>space M. val_process Mkt ?pf 0 w = initial_value ?pf
price_structure der matur \<pi> pr
stock_portfolio Mkt pf \<and> trading_strategy pf \<and> self_financing Mkt pf \<and> AEeq M (cls_val_process Mkt pf matur) der
coincides_on Mkt Mkt2 (stocks Mkt)
prices Mkt2 x = pr
x \<notin> stocks Mkt
diff_inv = (\<pi> - initial_value pf) / constant_image (prices Mkt pos_stock 0)
diff_inv \<noteq> 0
arb_pf = (\<lambda>x n w. 0)(x := \<lambda>n w. - 1, pos_stock := \<lambda>n w. diff_inv)
contr_pf = qty_sum arb_pf pf

goal (1 subgoal):
 1. \<pi> - initial_value pf - \<pi> + cls_val_process Mkt2 pf 0 w = \<pi> - initial_value pf - \<pi> + initial_value pf
[PROOF STEP]
using \<open>w \<in> space M\<close> coincides_stocks_cls_val_process self_financingE readable
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>trading_strategy ?pf; support_adapt Mkt ?pf\<rbrakk> \<Longrightarrow> \<forall>w\<in>space M. val_process Mkt ?pf 0 w = initial_value ?pf
price_structure der matur \<pi> pr
stock_portfolio Mkt pf \<and> trading_strategy pf \<and> self_financing Mkt pf \<and> AEeq M (cls_val_process Mkt pf matur) der
coincides_on Mkt Mkt2 (stocks Mkt)
prices Mkt2 x = pr
x \<notin> stocks Mkt
diff_inv = (\<pi> - initial_value pf) / constant_image (prices Mkt pos_stock 0)
diff_inv \<noteq> 0
arb_pf = (\<lambda>x n w. 0)(x := \<lambda>n w. - 1, pos_stock := \<lambda>n w. diff_inv)
contr_pf = qty_sum arb_pf pf
w \<in> space M
\<lbrakk>stock_portfolio ?Mkt ?pf; coincides_on ?Mkt ?Mkt2.0 (stocks ?Mkt)\<rbrakk> \<Longrightarrow> \<forall>n w. cls_val_process ?Mkt ?pf n w = cls_val_process ?Mkt2.0 ?pf n w
self_financing ?Mkt ?p \<Longrightarrow> \<forall>n. val_process ?Mkt ?p n = cls_val_process ?Mkt ?p n
\<forall>asset\<in>stocks Mkt. borel_adapt_stoch_proc F (prices Mkt asset)

goal (1 subgoal):
 1. \<pi> - initial_value pf - \<pi> + cls_val_process Mkt2 pf 0 w = \<pi> - initial_value pf - \<pi> + initial_value pf
[PROOF STEP]
by (metis (no_types, opaque_lifting) support_adapt_def stock_portfolio_def subsetCE)
[PROOF STATE]
proof (state)
this:
\<pi> - initial_value pf - \<pi> + cls_val_process Mkt2 pf 0 w = \<pi> - initial_value pf - \<pi> + initial_value pf

goal (1 subgoal):
 1. \<And>w. w \<in> space M \<Longrightarrow> cls_val_process Mkt2 contr_pf 0 w = 0
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<pi> - initial_value pf - \<pi> + cls_val_process Mkt2 pf 0 w = \<pi> - initial_value pf - \<pi> + initial_value pf

goal (1 subgoal):
 1. \<And>w. w \<in> space M \<Longrightarrow> cls_val_process Mkt2 contr_pf 0 w = 0
[PROOF STEP]
have "... = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> - initial_value pf - \<pi> + initial_value pf = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<pi> - initial_value pf - \<pi> + initial_value pf = 0

goal (1 subgoal):
 1. \<And>w. w \<in> space M \<Longrightarrow> cls_val_process Mkt2 contr_pf 0 w = 0
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
cls_val_process Mkt2 contr_pf 0 w = 0
[PROOF STEP]
show "cls_val_process Mkt2 contr_pf 0 w = 0"
[PROOF STATE]
proof (prove)
using this:
cls_val_process Mkt2 contr_pf 0 w = 0

goal (1 subgoal):
 1. cls_val_process Mkt2 contr_pf 0 w = 0
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
cls_val_process Mkt2 contr_pf 0 w = 0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>w\<in>space M. cls_val_process Mkt2 contr_pf 0 w = 0

goal (2 subgoals):
 1. 0 < diff_inv \<longrightarrow> (AE w in M. 0 < cls_val_process Mkt2 contr_pf matur w)
 2. diff_inv < 0 \<longrightarrow> (AE w in M. cls_val_process Mkt2 contr_pf matur w < 0)
[PROOF STEP]
show "0 < diff_inv \<longrightarrow> (AE w in M. 0 < cls_val_process Mkt2 contr_pf matur w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < diff_inv \<longrightarrow> (AE w in M. 0 < cls_val_process Mkt2 contr_pf matur w)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 0 < diff_inv \<Longrightarrow> AE w in M. 0 < cls_val_process Mkt2 contr_pf matur w
[PROOF STEP]
assume "0 < diff_inv"
[PROOF STATE]
proof (state)
this:
0 < diff_inv

goal (1 subgoal):
 1. 0 < diff_inv \<Longrightarrow> AE w in M. 0 < cls_val_process Mkt2 contr_pf matur w
[PROOF STEP]
show "AE w in M. 0 < cls_val_process Mkt2 contr_pf matur w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AE w in M. 0 < cls_val_process Mkt2 contr_pf matur w
[PROOF STEP]
proof (rule AE_mp)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. almost_everywhere M ?P
 2. AE w in M. ?P w \<longrightarrow> 0 < cls_val_process Mkt2 contr_pf matur w
[PROOF STEP]
have "AE w in M. prices Mkt2 x matur w = der w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AEeq M (prices Mkt2 x matur) der
[PROOF STEP]
using \<open>price_structure der matur \<pi> pr\<close> \<open>prices Mkt2 x = pr\<close>
[PROOF STATE]
proof (prove)
using this:
price_structure der matur \<pi> pr
prices Mkt2 x = pr

goal (1 subgoal):
 1. AEeq M (prices Mkt2 x matur) der
[PROOF STEP]
unfolding price_structure_def
[PROOF STATE]
proof (prove)
using this:
(\<forall>w\<in>space M. pr 0 w = \<pi>) \<and> AEeq M (pr matur) der \<and> pr matur \<in> borel_measurable (F matur)
prices Mkt2 x = pr

goal (1 subgoal):
 1. AEeq M (prices Mkt2 x matur) der
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
AEeq M (prices Mkt2 x matur) der

goal (2 subgoals):
 1. almost_everywhere M ?P
 2. AE w in M. ?P w \<longrightarrow> 0 < cls_val_process Mkt2 contr_pf matur w
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
AEeq M (prices Mkt2 x matur) der

goal (2 subgoals):
 1. almost_everywhere M ?P
 2. AE w in M. ?P w \<longrightarrow> 0 < cls_val_process Mkt2 contr_pf matur w
[PROOF STEP]
have "AE w in M. cls_val_process Mkt2 pf matur  w = der w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AEeq M (cls_val_process Mkt2 pf matur) der
[PROOF STEP]
using assms coincides_stocks_cls_val_process[of Mkt pf Mkt2]
        \<open>coincides_on Mkt Mkt2 (stocks Mkt)\<close>
[PROOF STATE]
proof (prove)
using this:
price_structure der matur \<pi> pr
replicating_portfolio pf der matur
coincides_on Mkt Mkt2 (stocks Mkt)
prices Mkt2 x = pr
x \<notin> stocks Mkt
diff_inv = (\<pi> - initial_value pf) / constant_image (prices Mkt pos_stock 0)
diff_inv \<noteq> 0
arb_pf = (\<lambda>x n w. 0)(x := \<lambda>n w. - 1, pos_stock := \<lambda>n w. diff_inv)
contr_pf = qty_sum arb_pf pf
\<lbrakk>stock_portfolio Mkt pf; coincides_on Mkt Mkt2 (stocks Mkt)\<rbrakk> \<Longrightarrow> \<forall>n w. cls_val_process Mkt pf n w = cls_val_process Mkt2 pf n w
coincides_on Mkt Mkt2 (stocks Mkt)

goal (1 subgoal):
 1. AEeq M (cls_val_process Mkt2 pf matur) der
[PROOF STEP]
unfolding replicating_portfolio_def
[PROOF STATE]
proof (prove)
using this:
price_structure der matur \<pi> pr
stock_portfolio Mkt pf \<and> trading_strategy pf \<and> self_financing Mkt pf \<and> AEeq M (cls_val_process Mkt pf matur) der
coincides_on Mkt Mkt2 (stocks Mkt)
prices Mkt2 x = pr
x \<notin> stocks Mkt
diff_inv = (\<pi> - initial_value pf) / constant_image (prices Mkt pos_stock 0)
diff_inv \<noteq> 0
arb_pf = (\<lambda>x n w. 0)(x := \<lambda>n w. - 1, pos_stock := \<lambda>n w. diff_inv)
contr_pf = qty_sum arb_pf pf
\<lbrakk>stock_portfolio Mkt pf; coincides_on Mkt Mkt2 (stocks Mkt)\<rbrakk> \<Longrightarrow> \<forall>n w. cls_val_process Mkt pf n w = cls_val_process Mkt2 pf n w
coincides_on Mkt Mkt2 (stocks Mkt)

goal (1 subgoal):
 1. AEeq M (cls_val_process Mkt2 pf matur) der
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
AEeq M (cls_val_process Mkt2 pf matur) der

goal (2 subgoals):
 1. almost_everywhere M ?P
 2. AE w in M. ?P w \<longrightarrow> 0 < cls_val_process Mkt2 contr_pf matur w
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
AEeq M (prices Mkt2 x matur) der
AEeq M (cls_val_process Mkt2 pf matur) der
[PROOF STEP]
show "AE w in M. prices Mkt2 x matur w = cls_val_process Mkt2 pf matur w"
[PROOF STATE]
proof (prove)
using this:
AEeq M (prices Mkt2 x matur) der
AEeq M (cls_val_process Mkt2 pf matur) der

goal (1 subgoal):
 1. AEeq M (prices Mkt2 x matur) (cls_val_process Mkt2 pf matur)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
AEeq M (prices Mkt2 x matur) (cls_val_process Mkt2 pf matur)

goal (1 subgoal):
 1. AE w in M. prices Mkt2 x matur w = cls_val_process Mkt2 pf matur w \<longrightarrow> 0 < cls_val_process Mkt2 contr_pf matur w
[PROOF STEP]
show "AE w in M. prices Mkt2 x matur w = cls_val_process Mkt2 pf matur w \<longrightarrow> 0 < cls_val_process Mkt2 contr_pf matur w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AE w in M. prices Mkt2 x matur w = cls_val_process Mkt2 pf matur w \<longrightarrow> 0 < cls_val_process Mkt2 contr_pf matur w
[PROOF STEP]
proof (rule AE_I2, rule impI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>w. \<lbrakk>w \<in> space M; prices Mkt2 x matur w = cls_val_process Mkt2 pf matur w\<rbrakk> \<Longrightarrow> 0 < cls_val_process Mkt2 contr_pf matur w
[PROOF STEP]
fix w
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>w. \<lbrakk>w \<in> space M; prices Mkt2 x matur w = cls_val_process Mkt2 pf matur w\<rbrakk> \<Longrightarrow> 0 < cls_val_process Mkt2 contr_pf matur w
[PROOF STEP]
assume "w\<in> space M"
        and "prices Mkt2 x matur w = cls_val_process Mkt2 pf matur w"
[PROOF STATE]
proof (state)
this:
w \<in> space M
prices Mkt2 x matur w = cls_val_process Mkt2 pf matur w

goal (1 subgoal):
 1. \<And>w. \<lbrakk>w \<in> space M; prices Mkt2 x matur w = cls_val_process Mkt2 pf matur w\<rbrakk> \<Longrightarrow> 0 < cls_val_process Mkt2 contr_pf matur w
[PROOF STEP]
have "cls_val_process Mkt2 contr_pf matur w = cls_val_process Mkt2 arb_pf matur w + cls_val_process Mkt2 pf matur w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cls_val_process Mkt2 contr_pf matur w = cls_val_process Mkt2 arb_pf matur w + cls_val_process Mkt2 pf matur w
[PROOF STEP]
using sum_cls_val_process[of arb_pf pf Mkt2]
          \<open>portfolio arb_pf\<close> assms replicating_portfolio_def stock_portfolio_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>portfolio arb_pf; portfolio pf\<rbrakk> \<Longrightarrow> \<forall>n w. cls_val_process Mkt2 (qty_sum arb_pf pf) n w = cls_val_process Mkt2 arb_pf n w + cls_val_process Mkt2 pf n w
portfolio arb_pf
price_structure der matur \<pi> pr
replicating_portfolio pf der matur
coincides_on Mkt Mkt2 (stocks Mkt)
prices Mkt2 x = pr
x \<notin> stocks Mkt
diff_inv = (\<pi> - initial_value pf) / constant_image (prices Mkt pos_stock 0)
diff_inv \<noteq> 0
arb_pf = (\<lambda>x n w. 0)(x := \<lambda>n w. - 1, pos_stock := \<lambda>n w. diff_inv)
contr_pf = qty_sum arb_pf pf
replicating_portfolio ?pf ?der ?matur = (stock_portfolio Mkt ?pf \<and> trading_strategy ?pf \<and> self_financing Mkt ?pf \<and> AEeq M (cls_val_process Mkt ?pf ?matur) ?der)
stock_portfolio ?Mkt ?p = (portfolio ?p \<and> support_set ?p \<subseteq> stocks ?Mkt)

goal (1 subgoal):
 1. cls_val_process Mkt2 contr_pf matur w = cls_val_process Mkt2 arb_pf matur w + cls_val_process Mkt2 pf matur w
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
cls_val_process Mkt2 contr_pf matur w = cls_val_process Mkt2 arb_pf matur w + cls_val_process Mkt2 pf matur w

goal (1 subgoal):
 1. \<And>w. \<lbrakk>w \<in> space M; prices Mkt2 x matur w = cls_val_process Mkt2 pf matur w\<rbrakk> \<Longrightarrow> 0 < cls_val_process Mkt2 contr_pf matur w
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
cls_val_process Mkt2 contr_pf matur w = cls_val_process Mkt2 arb_pf matur w + cls_val_process Mkt2 pf matur w

goal (1 subgoal):
 1. \<And>w. \<lbrakk>w \<in> space M; prices Mkt2 x matur w = cls_val_process Mkt2 pf matur w\<rbrakk> \<Longrightarrow> 0 < cls_val_process Mkt2 contr_pf matur w
[PROOF STEP]
have "... = prices Mkt2 pos_stock matur w * diff_inv - pr matur w + cls_val_process Mkt2 pf matur w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cls_val_process Mkt2 arb_pf matur w + cls_val_process Mkt2 pf matur w = prices Mkt2 pos_stock matur w * diff_inv - pr matur w + cls_val_process Mkt2 pf matur w
[PROOF STEP]
using arb_uvp
[PROOF STATE]
proof (prove)
using this:
\<forall>n w. cls_val_process Mkt2 arb_pf n w = prices Mkt2 pos_stock n w * diff_inv - pr n w

goal (1 subgoal):
 1. cls_val_process Mkt2 arb_pf matur w + cls_val_process Mkt2 pf matur w = prices Mkt2 pos_stock matur w * diff_inv - pr matur w + cls_val_process Mkt2 pf matur w
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cls_val_process Mkt2 arb_pf matur w + cls_val_process Mkt2 pf matur w = prices Mkt2 pos_stock matur w * diff_inv - pr matur w + cls_val_process Mkt2 pf matur w

goal (1 subgoal):
 1. \<And>w. \<lbrakk>w \<in> space M; prices Mkt2 x matur w = cls_val_process Mkt2 pf matur w\<rbrakk> \<Longrightarrow> 0 < cls_val_process Mkt2 contr_pf matur w
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
cls_val_process Mkt2 arb_pf matur w + cls_val_process Mkt2 pf matur w = prices Mkt2 pos_stock matur w * diff_inv - pr matur w + cls_val_process Mkt2 pf matur w

goal (1 subgoal):
 1. \<And>w. \<lbrakk>w \<in> space M; prices Mkt2 x matur w = cls_val_process Mkt2 pf matur w\<rbrakk> \<Longrightarrow> 0 < cls_val_process Mkt2 contr_pf matur w
[PROOF STEP]
have "... = prices Mkt2 pos_stock matur w * diff_inv - prices Mkt2 x matur w + cls_val_process Mkt2 pf matur w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prices Mkt2 pos_stock matur w * diff_inv - pr matur w + cls_val_process Mkt2 pf matur w = prices Mkt2 pos_stock matur w * diff_inv - prices Mkt2 x matur w + cls_val_process Mkt2 pf matur w
[PROOF STEP]
using \<open>prices Mkt2 x = pr\<close>
[PROOF STATE]
proof (prove)
using this:
prices Mkt2 x = pr

goal (1 subgoal):
 1. prices Mkt2 pos_stock matur w * diff_inv - pr matur w + cls_val_process Mkt2 pf matur w = prices Mkt2 pos_stock matur w * diff_inv - prices Mkt2 x matur w + cls_val_process Mkt2 pf matur w
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
prices Mkt2 pos_stock matur w * diff_inv - pr matur w + cls_val_process Mkt2 pf matur w = prices Mkt2 pos_stock matur w * diff_inv - prices Mkt2 x matur w + cls_val_process Mkt2 pf matur w

goal (1 subgoal):
 1. \<And>w. \<lbrakk>w \<in> space M; prices Mkt2 x matur w = cls_val_process Mkt2 pf matur w\<rbrakk> \<Longrightarrow> 0 < cls_val_process Mkt2 contr_pf matur w
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
prices Mkt2 pos_stock matur w * diff_inv - pr matur w + cls_val_process Mkt2 pf matur w = prices Mkt2 pos_stock matur w * diff_inv - prices Mkt2 x matur w + cls_val_process Mkt2 pf matur w

goal (1 subgoal):
 1. \<And>w. \<lbrakk>w \<in> space M; prices Mkt2 x matur w = cls_val_process Mkt2 pf matur w\<rbrakk> \<Longrightarrow> 0 < cls_val_process Mkt2 contr_pf matur w
[PROOF STEP]
have "... = prices Mkt2 pos_stock matur w * diff_inv"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prices Mkt2 pos_stock matur w * diff_inv - prices Mkt2 x matur w + cls_val_process Mkt2 pf matur w = prices Mkt2 pos_stock matur w * diff_inv
[PROOF STEP]
using \<open>prices Mkt2 x matur w = cls_val_process Mkt2 pf matur w\<close>
[PROOF STATE]
proof (prove)
using this:
prices Mkt2 x matur w = cls_val_process Mkt2 pf matur w

goal (1 subgoal):
 1. prices Mkt2 pos_stock matur w * diff_inv - prices Mkt2 x matur w + cls_val_process Mkt2 pf matur w = prices Mkt2 pos_stock matur w * diff_inv
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
prices Mkt2 pos_stock matur w * diff_inv - prices Mkt2 x matur w + cls_val_process Mkt2 pf matur w = prices Mkt2 pos_stock matur w * diff_inv

goal (1 subgoal):
 1. \<And>w. \<lbrakk>w \<in> space M; prices Mkt2 x matur w = cls_val_process Mkt2 pf matur w\<rbrakk> \<Longrightarrow> 0 < cls_val_process Mkt2 contr_pf matur w
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
prices Mkt2 pos_stock matur w * diff_inv - prices Mkt2 x matur w + cls_val_process Mkt2 pf matur w = prices Mkt2 pos_stock matur w * diff_inv

goal (1 subgoal):
 1. \<And>w. \<lbrakk>w \<in> space M; prices Mkt2 x matur w = cls_val_process Mkt2 pf matur w\<rbrakk> \<Longrightarrow> 0 < cls_val_process Mkt2 contr_pf matur w
[PROOF STEP]
have "... > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < prices Mkt2 pos_stock matur w * diff_inv
[PROOF STEP]
using positive \<open>0 < diff_inv\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>n w. 0 < prices Mkt pos_stock n w
0 < diff_inv

goal (1 subgoal):
 1. 0 < prices Mkt2 pos_stock matur w * diff_inv
[PROOF STEP]
by (metis \<open>coincides_on Mkt Mkt2 (stocks Mkt)\<close> coincides_on_def in_stock mult_pos_pos)
[PROOF STATE]
proof (state)
this:
0 < prices Mkt2 pos_stock matur w * diff_inv

goal (1 subgoal):
 1. \<And>w. \<lbrakk>w \<in> space M; prices Mkt2 x matur w = cls_val_process Mkt2 pf matur w\<rbrakk> \<Longrightarrow> 0 < cls_val_process Mkt2 contr_pf matur w
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
0 < cls_val_process Mkt2 contr_pf matur w
[PROOF STEP]
have "cls_val_process Mkt2 contr_pf matur w > 0"
[PROOF STATE]
proof (prove)
using this:
0 < cls_val_process Mkt2 contr_pf matur w

goal (1 subgoal):
 1. 0 < cls_val_process Mkt2 contr_pf matur w
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
0 < cls_val_process Mkt2 contr_pf matur w

goal (1 subgoal):
 1. \<And>w. \<lbrakk>w \<in> space M; prices Mkt2 x matur w = cls_val_process Mkt2 pf matur w\<rbrakk> \<Longrightarrow> 0 < cls_val_process Mkt2 contr_pf matur w
[PROOF STEP]
thus "0 < cls_val_process Mkt2 contr_pf matur w"
[PROOF STATE]
proof (prove)
using this:
0 < cls_val_process Mkt2 contr_pf matur w

goal (1 subgoal):
 1. 0 < cls_val_process Mkt2 contr_pf matur w
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 < cls_val_process Mkt2 contr_pf matur w

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
AE w in M. prices Mkt2 x matur w = cls_val_process Mkt2 pf matur w \<longrightarrow> 0 < cls_val_process Mkt2 contr_pf matur w

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
AE w in M. 0 < cls_val_process Mkt2 contr_pf matur w

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
0 < diff_inv \<longrightarrow> (AE w in M. 0 < cls_val_process Mkt2 contr_pf matur w)

goal (1 subgoal):
 1. diff_inv < 0 \<longrightarrow> (AE w in M. cls_val_process Mkt2 contr_pf matur w < 0)
[PROOF STEP]
show "diff_inv < 0 \<longrightarrow> (AE w in M. 0 > cls_val_process Mkt2 contr_pf matur w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. diff_inv < 0 \<longrightarrow> (AE w in M. cls_val_process Mkt2 contr_pf matur w < 0)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. diff_inv < 0 \<Longrightarrow> AE w in M. cls_val_process Mkt2 contr_pf matur w < 0
[PROOF STEP]
assume "diff_inv < 0"
[PROOF STATE]
proof (state)
this:
diff_inv < 0

goal (1 subgoal):
 1. diff_inv < 0 \<Longrightarrow> AE w in M. cls_val_process Mkt2 contr_pf matur w < 0
[PROOF STEP]
show "AE w in M. 0 > cls_val_process Mkt2 contr_pf matur w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AE w in M. cls_val_process Mkt2 contr_pf matur w < 0
[PROOF STEP]
proof (rule AE_mp)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. almost_everywhere M ?P
 2. AE w in M. ?P w \<longrightarrow> cls_val_process Mkt2 contr_pf matur w < 0
[PROOF STEP]
have "AE w in M. prices Mkt2 x matur w = der w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AEeq M (prices Mkt2 x matur) der
[PROOF STEP]
using \<open>price_structure der matur \<pi> pr\<close> \<open>prices Mkt2 x = pr\<close>
[PROOF STATE]
proof (prove)
using this:
price_structure der matur \<pi> pr
prices Mkt2 x = pr

goal (1 subgoal):
 1. AEeq M (prices Mkt2 x matur) der
[PROOF STEP]
unfolding price_structure_def
[PROOF STATE]
proof (prove)
using this:
(\<forall>w\<in>space M. pr 0 w = \<pi>) \<and> AEeq M (pr matur) der \<and> pr matur \<in> borel_measurable (F matur)
prices Mkt2 x = pr

goal (1 subgoal):
 1. AEeq M (prices Mkt2 x matur) der
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
AEeq M (prices Mkt2 x matur) der

goal (2 subgoals):
 1. almost_everywhere M ?P
 2. AE w in M. ?P w \<longrightarrow> cls_val_process Mkt2 contr_pf matur w < 0
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
AEeq M (prices Mkt2 x matur) der

goal (2 subgoals):
 1. almost_everywhere M ?P
 2. AE w in M. ?P w \<longrightarrow> cls_val_process Mkt2 contr_pf matur w < 0
[PROOF STEP]
have "AE w in M. cls_val_process Mkt2 pf matur  w = der w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AEeq M (cls_val_process Mkt2 pf matur) der
[PROOF STEP]
using assms coincides_stocks_cls_val_process[of Mkt pf Mkt2]
        \<open>coincides_on Mkt Mkt2 (stocks Mkt)\<close>
[PROOF STATE]
proof (prove)
using this:
price_structure der matur \<pi> pr
replicating_portfolio pf der matur
coincides_on Mkt Mkt2 (stocks Mkt)
prices Mkt2 x = pr
x \<notin> stocks Mkt
diff_inv = (\<pi> - initial_value pf) / constant_image (prices Mkt pos_stock 0)
diff_inv \<noteq> 0
arb_pf = (\<lambda>x n w. 0)(x := \<lambda>n w. - 1, pos_stock := \<lambda>n w. diff_inv)
contr_pf = qty_sum arb_pf pf
\<lbrakk>stock_portfolio Mkt pf; coincides_on Mkt Mkt2 (stocks Mkt)\<rbrakk> \<Longrightarrow> \<forall>n w. cls_val_process Mkt pf n w = cls_val_process Mkt2 pf n w
coincides_on Mkt Mkt2 (stocks Mkt)

goal (1 subgoal):
 1. AEeq M (cls_val_process Mkt2 pf matur) der
[PROOF STEP]
unfolding replicating_portfolio_def
[PROOF STATE]
proof (prove)
using this:
price_structure der matur \<pi> pr
stock_portfolio Mkt pf \<and> trading_strategy pf \<and> self_financing Mkt pf \<and> AEeq M (cls_val_process Mkt pf matur) der
coincides_on Mkt Mkt2 (stocks Mkt)
prices Mkt2 x = pr
x \<notin> stocks Mkt
diff_inv = (\<pi> - initial_value pf) / constant_image (prices Mkt pos_stock 0)
diff_inv \<noteq> 0
arb_pf = (\<lambda>x n w. 0)(x := \<lambda>n w. - 1, pos_stock := \<lambda>n w. diff_inv)
contr_pf = qty_sum arb_pf pf
\<lbrakk>stock_portfolio Mkt pf; coincides_on Mkt Mkt2 (stocks Mkt)\<rbrakk> \<Longrightarrow> \<forall>n w. cls_val_process Mkt pf n w = cls_val_process Mkt2 pf n w
coincides_on Mkt Mkt2 (stocks Mkt)

goal (1 subgoal):
 1. AEeq M (cls_val_process Mkt2 pf matur) der
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
AEeq M (cls_val_process Mkt2 pf matur) der

goal (2 subgoals):
 1. almost_everywhere M ?P
 2. AE w in M. ?P w \<longrightarrow> cls_val_process Mkt2 contr_pf matur w < 0
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
AEeq M (prices Mkt2 x matur) der
AEeq M (cls_val_process Mkt2 pf matur) der
[PROOF STEP]
show "AE w in M. prices Mkt2 x matur w = cls_val_process Mkt2 pf matur w"
[PROOF STATE]
proof (prove)
using this:
AEeq M (prices Mkt2 x matur) der
AEeq M (cls_val_process Mkt2 pf matur) der

goal (1 subgoal):
 1. AEeq M (prices Mkt2 x matur) (cls_val_process Mkt2 pf matur)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
AEeq M (prices Mkt2 x matur) (cls_val_process Mkt2 pf matur)

goal (1 subgoal):
 1. AE w in M. prices Mkt2 x matur w = cls_val_process Mkt2 pf matur w \<longrightarrow> cls_val_process Mkt2 contr_pf matur w < 0
[PROOF STEP]
show "AE w in M. prices Mkt2 x matur w = cls_val_process Mkt2 pf matur w \<longrightarrow> 0 > cls_val_process Mkt2 contr_pf matur w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AE w in M. prices Mkt2 x matur w = cls_val_process Mkt2 pf matur w \<longrightarrow> cls_val_process Mkt2 contr_pf matur w < 0
[PROOF STEP]
proof (rule AE_I2, rule impI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>w. \<lbrakk>w \<in> space M; prices Mkt2 x matur w = cls_val_process Mkt2 pf matur w\<rbrakk> \<Longrightarrow> cls_val_process Mkt2 contr_pf matur w < 0
[PROOF STEP]
fix w
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>w. \<lbrakk>w \<in> space M; prices Mkt2 x matur w = cls_val_process Mkt2 pf matur w\<rbrakk> \<Longrightarrow> cls_val_process Mkt2 contr_pf matur w < 0
[PROOF STEP]
assume "w\<in> space M"
        and "prices Mkt2 x matur w = cls_val_process Mkt2 pf matur w"
[PROOF STATE]
proof (state)
this:
w \<in> space M
prices Mkt2 x matur w = cls_val_process Mkt2 pf matur w

goal (1 subgoal):
 1. \<And>w. \<lbrakk>w \<in> space M; prices Mkt2 x matur w = cls_val_process Mkt2 pf matur w\<rbrakk> \<Longrightarrow> cls_val_process Mkt2 contr_pf matur w < 0
[PROOF STEP]
have "cls_val_process Mkt2 contr_pf matur w = cls_val_process Mkt2 arb_pf matur w + cls_val_process Mkt2 pf matur w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cls_val_process Mkt2 contr_pf matur w = cls_val_process Mkt2 arb_pf matur w + cls_val_process Mkt2 pf matur w
[PROOF STEP]
using sum_cls_val_process[of arb_pf pf Mkt2]
          \<open>portfolio arb_pf\<close> assms replicating_portfolio_def stock_portfolio_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>portfolio arb_pf; portfolio pf\<rbrakk> \<Longrightarrow> \<forall>n w. cls_val_process Mkt2 (qty_sum arb_pf pf) n w = cls_val_process Mkt2 arb_pf n w + cls_val_process Mkt2 pf n w
portfolio arb_pf
price_structure der matur \<pi> pr
replicating_portfolio pf der matur
coincides_on Mkt Mkt2 (stocks Mkt)
prices Mkt2 x = pr
x \<notin> stocks Mkt
diff_inv = (\<pi> - initial_value pf) / constant_image (prices Mkt pos_stock 0)
diff_inv \<noteq> 0
arb_pf = (\<lambda>x n w. 0)(x := \<lambda>n w. - 1, pos_stock := \<lambda>n w. diff_inv)
contr_pf = qty_sum arb_pf pf
replicating_portfolio ?pf ?der ?matur = (stock_portfolio Mkt ?pf \<and> trading_strategy ?pf \<and> self_financing Mkt ?pf \<and> AEeq M (cls_val_process Mkt ?pf ?matur) ?der)
stock_portfolio ?Mkt ?p = (portfolio ?p \<and> support_set ?p \<subseteq> stocks ?Mkt)

goal (1 subgoal):
 1. cls_val_process Mkt2 contr_pf matur w = cls_val_process Mkt2 arb_pf matur w + cls_val_process Mkt2 pf matur w
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
cls_val_process Mkt2 contr_pf matur w = cls_val_process Mkt2 arb_pf matur w + cls_val_process Mkt2 pf matur w

goal (1 subgoal):
 1. \<And>w. \<lbrakk>w \<in> space M; prices Mkt2 x matur w = cls_val_process Mkt2 pf matur w\<rbrakk> \<Longrightarrow> cls_val_process Mkt2 contr_pf matur w < 0
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
cls_val_process Mkt2 contr_pf matur w = cls_val_process Mkt2 arb_pf matur w + cls_val_process Mkt2 pf matur w

goal (1 subgoal):
 1. \<And>w. \<lbrakk>w \<in> space M; prices Mkt2 x matur w = cls_val_process Mkt2 pf matur w\<rbrakk> \<Longrightarrow> cls_val_process Mkt2 contr_pf matur w < 0
[PROOF STEP]
have "... = prices Mkt2 pos_stock matur w * diff_inv - pr matur w + cls_val_process Mkt2 pf matur w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cls_val_process Mkt2 arb_pf matur w + cls_val_process Mkt2 pf matur w = prices Mkt2 pos_stock matur w * diff_inv - pr matur w + cls_val_process Mkt2 pf matur w
[PROOF STEP]
using arb_uvp
[PROOF STATE]
proof (prove)
using this:
\<forall>n w. cls_val_process Mkt2 arb_pf n w = prices Mkt2 pos_stock n w * diff_inv - pr n w

goal (1 subgoal):
 1. cls_val_process Mkt2 arb_pf matur w + cls_val_process Mkt2 pf matur w = prices Mkt2 pos_stock matur w * diff_inv - pr matur w + cls_val_process Mkt2 pf matur w
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cls_val_process Mkt2 arb_pf matur w + cls_val_process Mkt2 pf matur w = prices Mkt2 pos_stock matur w * diff_inv - pr matur w + cls_val_process Mkt2 pf matur w

goal (1 subgoal):
 1. \<And>w. \<lbrakk>w \<in> space M; prices Mkt2 x matur w = cls_val_process Mkt2 pf matur w\<rbrakk> \<Longrightarrow> cls_val_process Mkt2 contr_pf matur w < 0
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
cls_val_process Mkt2 arb_pf matur w + cls_val_process Mkt2 pf matur w = prices Mkt2 pos_stock matur w * diff_inv - pr matur w + cls_val_process Mkt2 pf matur w

goal (1 subgoal):
 1. \<And>w. \<lbrakk>w \<in> space M; prices Mkt2 x matur w = cls_val_process Mkt2 pf matur w\<rbrakk> \<Longrightarrow> cls_val_process Mkt2 contr_pf matur w < 0
[PROOF STEP]
have "... = prices Mkt2 pos_stock matur w * diff_inv - prices Mkt2 x matur w + cls_val_process Mkt2 pf matur w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prices Mkt2 pos_stock matur w * diff_inv - pr matur w + cls_val_process Mkt2 pf matur w = prices Mkt2 pos_stock matur w * diff_inv - prices Mkt2 x matur w + cls_val_process Mkt2 pf matur w
[PROOF STEP]
using \<open>prices Mkt2 x = pr\<close>
[PROOF STATE]
proof (prove)
using this:
prices Mkt2 x = pr

goal (1 subgoal):
 1. prices Mkt2 pos_stock matur w * diff_inv - pr matur w + cls_val_process Mkt2 pf matur w = prices Mkt2 pos_stock matur w * diff_inv - prices Mkt2 x matur w + cls_val_process Mkt2 pf matur w
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
prices Mkt2 pos_stock matur w * diff_inv - pr matur w + cls_val_process Mkt2 pf matur w = prices Mkt2 pos_stock matur w * diff_inv - prices Mkt2 x matur w + cls_val_process Mkt2 pf matur w

goal (1 subgoal):
 1. \<And>w. \<lbrakk>w \<in> space M; prices Mkt2 x matur w = cls_val_process Mkt2 pf matur w\<rbrakk> \<Longrightarrow> cls_val_process Mkt2 contr_pf matur w < 0
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
prices Mkt2 pos_stock matur w * diff_inv - pr matur w + cls_val_process Mkt2 pf matur w = prices Mkt2 pos_stock matur w * diff_inv - prices Mkt2 x matur w + cls_val_process Mkt2 pf matur w

goal (1 subgoal):
 1. \<And>w. \<lbrakk>w \<in> space M; prices Mkt2 x matur w = cls_val_process Mkt2 pf matur w\<rbrakk> \<Longrightarrow> cls_val_process Mkt2 contr_pf matur w < 0
[PROOF STEP]
have "... = prices Mkt2 pos_stock matur w * diff_inv"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prices Mkt2 pos_stock matur w * diff_inv - prices Mkt2 x matur w + cls_val_process Mkt2 pf matur w = prices Mkt2 pos_stock matur w * diff_inv
[PROOF STEP]
using \<open>prices Mkt2 x matur w = cls_val_process Mkt2 pf matur w\<close>
[PROOF STATE]
proof (prove)
using this:
prices Mkt2 x matur w = cls_val_process Mkt2 pf matur w

goal (1 subgoal):
 1. prices Mkt2 pos_stock matur w * diff_inv - prices Mkt2 x matur w + cls_val_process Mkt2 pf matur w = prices Mkt2 pos_stock matur w * diff_inv
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
prices Mkt2 pos_stock matur w * diff_inv - prices Mkt2 x matur w + cls_val_process Mkt2 pf matur w = prices Mkt2 pos_stock matur w * diff_inv

goal (1 subgoal):
 1. \<And>w. \<lbrakk>w \<in> space M; prices Mkt2 x matur w = cls_val_process Mkt2 pf matur w\<rbrakk> \<Longrightarrow> cls_val_process Mkt2 contr_pf matur w < 0
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
prices Mkt2 pos_stock matur w * diff_inv - prices Mkt2 x matur w + cls_val_process Mkt2 pf matur w = prices Mkt2 pos_stock matur w * diff_inv

goal (1 subgoal):
 1. \<And>w. \<lbrakk>w \<in> space M; prices Mkt2 x matur w = cls_val_process Mkt2 pf matur w\<rbrakk> \<Longrightarrow> cls_val_process Mkt2 contr_pf matur w < 0
[PROOF STEP]
have "... < 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prices Mkt2 pos_stock matur w * diff_inv < 0
[PROOF STEP]
using positive \<open>diff_inv < 0\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>n w. 0 < prices Mkt pos_stock n w
diff_inv < 0

goal (1 subgoal):
 1. prices Mkt2 pos_stock matur w * diff_inv < 0
[PROOF STEP]
by (metis \<open>coincides_on Mkt Mkt2 (stocks Mkt)\<close> coincides_on_def in_stock mult_pos_neg)
[PROOF STATE]
proof (state)
this:
prices Mkt2 pos_stock matur w * diff_inv < 0

goal (1 subgoal):
 1. \<And>w. \<lbrakk>w \<in> space M; prices Mkt2 x matur w = cls_val_process Mkt2 pf matur w\<rbrakk> \<Longrightarrow> cls_val_process Mkt2 contr_pf matur w < 0
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
cls_val_process Mkt2 contr_pf matur w < 0
[PROOF STEP]
have "cls_val_process Mkt2 contr_pf matur w < 0"
[PROOF STATE]
proof (prove)
using this:
cls_val_process Mkt2 contr_pf matur w < 0

goal (1 subgoal):
 1. cls_val_process Mkt2 contr_pf matur w < 0
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
cls_val_process Mkt2 contr_pf matur w < 0

goal (1 subgoal):
 1. \<And>w. \<lbrakk>w \<in> space M; prices Mkt2 x matur w = cls_val_process Mkt2 pf matur w\<rbrakk> \<Longrightarrow> cls_val_process Mkt2 contr_pf matur w < 0
[PROOF STEP]
thus "0 > cls_val_process Mkt2 contr_pf matur w"
[PROOF STATE]
proof (prove)
using this:
cls_val_process Mkt2 contr_pf matur w < 0

goal (1 subgoal):
 1. cls_val_process Mkt2 contr_pf matur w < 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cls_val_process Mkt2 contr_pf matur w < 0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
AE w in M. prices Mkt2 x matur w = cls_val_process Mkt2 pf matur w \<longrightarrow> cls_val_process Mkt2 contr_pf matur w < 0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
AE w in M. cls_val_process Mkt2 contr_pf matur w < 0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
diff_inv < 0 \<longrightarrow> (AE w in M. cls_val_process Mkt2 contr_pf matur w < 0)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma D_compE1':
  assumes "\<D> e \<lfloor>set(V#Vs)\<rfloor>" and "fv e \<subseteq> set(V#Vs)" and "distinct(V#Vs)"
  shows "\<D> (compE1 (V#Vs) e) \<lfloor>{..length Vs}\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D> (compE1 (V # Vs) e) \<lfloor>{..length Vs}\<rfloor>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<D> (compE1 (V # Vs) e) \<lfloor>{..length Vs}\<rfloor>
[PROOF STEP]
have "{..size Vs} = {..<size(V#Vs)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {..length Vs} = {..<length (V # Vs)}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{..length Vs} = {..<length (V # Vs)}

goal (1 subgoal):
 1. \<D> (compE1 (V # Vs) e) \<lfloor>{..length Vs}\<rfloor>
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
{..length Vs} = {..<length (V # Vs)}

goal (1 subgoal):
 1. \<D> (compE1 (V # Vs) e) \<lfloor>{..length Vs}\<rfloor>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
{..length Vs} = {..<length (V # Vs)}
\<D> e \<lfloor>set (V # Vs)\<rfloor>
fv e \<subseteq> set (V # Vs)
distinct (V # Vs)

goal (1 subgoal):
 1. \<D> (compE1 (V # Vs) e) \<lfloor>{..length Vs}\<rfloor>
[PROOF STEP]
by (simp only:)(rule D_compE1)
[PROOF STATE]
proof (state)
this:
\<D> (compE1 (V # Vs) e) \<lfloor>{..length Vs}\<rfloor>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma unat_lt2p [iff]:
  \<open>unat x < 2 ^ LENGTH('a)\<close> for x :: \<open>'a::len word\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unat x < 2 ^ LENGTH('a)
[PROOF STEP]
by transfer simp


[STATEMENT]
lemma unat_of_nat_len:
  "x < 2 ^ LENGTH('a) \<Longrightarrow> unat (of_nat x :: 'a::len word) = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x < 2 ^ LENGTH('a) \<Longrightarrow> unat (word_of_nat x) = x
[PROOF STEP]
by (simp add: unsigned_of_nat take_bit_nat_eq_self_iff)