[STATEMENT]
lemma B_accessible[intro]: "(i, j) \<in> B.acc"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (i, j) \<in> B.acc
[PROOF STEP]
proof (cases i j rule: linorder_le_cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. i \<le> j \<Longrightarrow> (i, j) \<in> B.acc
 2. j \<le> i \<Longrightarrow> (i, j) \<in> B.acc
[PROOF STEP]
assume "i \<le> j"
[PROOF STATE]
proof (state)
this:
i \<le> j

goal (2 subgoals):
 1. i \<le> j \<Longrightarrow> (i, j) \<in> B.acc
 2. j \<le> i \<Longrightarrow> (i, j) \<in> B.acc
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<le> j
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
i \<le> j

goal (1 subgoal):
 1. (i, j) \<in> B.acc
[PROOF STEP]
by (induct rule: inc_induct) (auto intro: B_E_Suc converse_rtrancl_into_rtrancl)
[PROOF STATE]
proof (state)
this:
(i, j) \<in> B.acc

goal (1 subgoal):
 1. j \<le> i \<Longrightarrow> (i, j) \<in> B.acc
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. j \<le> i \<Longrightarrow> (i, j) \<in> B.acc
[PROOF STEP]
assume "j \<le> i"
[PROOF STATE]
proof (state)
this:
j \<le> i

goal (1 subgoal):
 1. j \<le> i \<Longrightarrow> (i, j) \<in> B.acc
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
j \<le> i
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
j \<le> i

goal (1 subgoal):
 1. (i, j) \<in> B.acc
[PROOF STEP]
by (induct rule: dec_induct) (auto intro: B_E_Suc converse_rtrancl_into_rtrancl)
[PROOF STATE]
proof (state)
this:
(i, j) \<in> B.acc

goal:
No subgoals!
[PROOF STEP]
qed