[STATEMENT]
lemma KB4_5:
  assumes \<open>AxB \<le> A\<close> \<open>Ax4 \<le> A\<close>
  shows \<open>A \<turnstile> L i p \<^bold>\<longrightarrow> K i (L i p)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<turnstile> L i p \<^bold>\<longrightarrow> K i (L i p)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A \<turnstile> L i p \<^bold>\<longrightarrow> K i (L i p)
[PROOF STEP]
have \<open>A \<turnstile> L i p \<^bold>\<longrightarrow> K i (L i (L i p))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<turnstile> L i p \<^bold>\<longrightarrow> K i (L i (L i p))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
AxB \<le> A
Ax4 \<le> A

goal (1 subgoal):
 1. A \<turnstile> L i p \<^bold>\<longrightarrow> K i (L i (L i p))
[PROOF STEP]
by (auto intro: Ax AxB.intros)
[PROOF STATE]
proof (state)
this:
A \<turnstile> L i p \<^bold>\<longrightarrow> K i (L i (L i p))

goal (1 subgoal):
 1. A \<turnstile> L i p \<^bold>\<longrightarrow> K i (L i p)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
A \<turnstile> L i p \<^bold>\<longrightarrow> K i (L i (L i p))

goal (1 subgoal):
 1. A \<turnstile> L i p \<^bold>\<longrightarrow> K i (L i p)
[PROOF STEP]
have \<open>A \<turnstile> L i (L i p) \<^bold>\<longrightarrow> L i p\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<turnstile> L i (L i p) \<^bold>\<longrightarrow> L i p
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
AxB \<le> A
Ax4 \<le> A

goal (1 subgoal):
 1. A \<turnstile> L i (L i p) \<^bold>\<longrightarrow> L i p
[PROOF STEP]
by (auto intro: K4_L)
[PROOF STATE]
proof (state)
this:
A \<turnstile> L i (L i p) \<^bold>\<longrightarrow> L i p

goal (1 subgoal):
 1. A \<turnstile> L i p \<^bold>\<longrightarrow> K i (L i p)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
A \<turnstile> L i (L i p) \<^bold>\<longrightarrow> L i p
[PROOF STEP]
have \<open>A \<turnstile> K i (L i (L i p)) \<^bold>\<longrightarrow> K i (L i p)\<close>
[PROOF STATE]
proof (prove)
using this:
A \<turnstile> L i (L i p) \<^bold>\<longrightarrow> L i p

goal (1 subgoal):
 1. A \<turnstile> K i (L i (L i p)) \<^bold>\<longrightarrow> K i (L i p)
[PROOF STEP]
using K_map
[PROOF STATE]
proof (prove)
using this:
A \<turnstile> L i (L i p) \<^bold>\<longrightarrow> L i p
?A \<turnstile> ?p \<^bold>\<longrightarrow> ?q \<Longrightarrow> ?A \<turnstile> K ?i ?p \<^bold>\<longrightarrow> K ?i ?q

goal (1 subgoal):
 1. A \<turnstile> K i (L i (L i p)) \<^bold>\<longrightarrow> K i (L i p)
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
A \<turnstile> K i (L i (L i p)) \<^bold>\<longrightarrow> K i (L i p)

goal (1 subgoal):
 1. A \<turnstile> L i p \<^bold>\<longrightarrow> K i (L i p)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
A \<turnstile> L i p \<^bold>\<longrightarrow> K i (L i (L i p))
A \<turnstile> K i (L i (L i p)) \<^bold>\<longrightarrow> K i (L i p)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
A \<turnstile> L i p \<^bold>\<longrightarrow> K i (L i (L i p))
A \<turnstile> K i (L i (L i p)) \<^bold>\<longrightarrow> K i (L i p)

goal (1 subgoal):
 1. A \<turnstile> L i p \<^bold>\<longrightarrow> K i (L i p)
[PROOF STEP]
using K_trans R1
[PROOF STATE]
proof (prove)
using this:
A \<turnstile> L i p \<^bold>\<longrightarrow> K i (L i (L i p))
A \<turnstile> K i (L i (L i p)) \<^bold>\<longrightarrow> K i (L i p)
?A \<turnstile> (?p \<^bold>\<longrightarrow> ?q) \<^bold>\<longrightarrow> (?q \<^bold>\<longrightarrow> ?r) \<^bold>\<longrightarrow> ?p \<^bold>\<longrightarrow> ?r
\<lbrakk>?A \<turnstile> ?p; ?A \<turnstile> ?p \<^bold>\<longrightarrow> ?q\<rbrakk> \<Longrightarrow> ?A \<turnstile> ?q

goal (1 subgoal):
 1. A \<turnstile> L i p \<^bold>\<longrightarrow> K i (L i p)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
A \<turnstile> L i p \<^bold>\<longrightarrow> K i (L i p)

goal:
No subgoals!
[PROOF STEP]
qed