[STATEMENT]
lemma (in ptrace_top) suff_ptop_nhd_base:
  assumes unhd: "u \<in> nhds t"
  and H: "\<And>r. \<lbrakk> r \<in> pfinpref A t; suff A r \<subseteq> u \<rbrakk> \<Longrightarrow> R"
  shows "R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. R
[PROOF STEP]
from unhd
[PROOF STATE]
proof (chain)
picking this:
u \<in> nhds t
[PROOF STEP]
obtain m where
    uA: "u \<subseteq> A\<^sup>\<spadesuit>" and
    mopen: "m open" and
    tm: "t \<in> m" and
    mu: "m \<subseteq> u"
[PROOF STATE]
proof (prove)
using this:
u \<in> nhds t

goal (1 subgoal):
 1. (\<And>m. \<lbrakk>u \<subseteq> A\<^sup>\<spadesuit>; m open; t \<in> m; m \<subseteq> u\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: ptop_carrier)
[PROOF STATE]
proof (state)
this:
u \<subseteq> A\<^sup>\<spadesuit>
m open
t \<in> m
m \<subseteq> u

goal (1 subgoal):
 1. R
[PROOF STEP]
from mopen tm
[PROOF STATE]
proof (chain)
picking this:
m open
t \<in> m
[PROOF STEP]
have
    "\<exists>r \<in> pfinpref A t. suff A r \<subseteq> m"
[PROOF STATE]
proof (prove)
using this:
m open
t \<in> m

goal (1 subgoal):
 1. \<exists>r\<in>pfinpref A t. suff A r \<subseteq> m
[PROOF STEP]
proof (induct "m")
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>x \<in> B; t \<in> x\<rbrakk> \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> x
 2. \<And>x y. \<lbrakk>x open; t \<in> x \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> x; y open; t \<in> y \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> y; t \<in> x \<inter> y\<rbrakk> \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> x \<inter> y
 3. \<And>M. \<lbrakk>\<forall>ta\<in>M. ta open \<and> (t \<in> ta \<longrightarrow> (\<exists>r\<in>pfinpref A t. suff A r \<subseteq> ta)); t \<in> \<Union> M\<rbrakk> \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> \<Union> M
[PROOF STEP]
case (basic a)
[PROOF STATE]
proof (state)
this:
a \<in> B
t \<in> a

goal (3 subgoals):
 1. \<And>x. \<lbrakk>x \<in> B; t \<in> x\<rbrakk> \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> x
 2. \<And>x y. \<lbrakk>x open; t \<in> x \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> x; y open; t \<in> y \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> y; t \<in> x \<inter> y\<rbrakk> \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> x \<inter> y
 3. \<And>M. \<lbrakk>\<forall>ta\<in>M. ta open \<and> (t \<in> ta \<longrightarrow> (\<exists>r\<in>pfinpref A t. suff A r \<subseteq> ta)); t \<in> \<Union> M\<rbrakk> \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> \<Union> M
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<in> B
t \<in> a
[PROOF STEP]
obtain s where sA: "s \<in> A\<^sup>\<clubsuit>" and as: "a = suff A s" and ta: "t \<in> a"
[PROOF STATE]
proof (prove)
using this:
a \<in> B
t \<in> a

goal (1 subgoal):
 1. (\<And>s. \<lbrakk>s \<in> A\<^sup>\<clubsuit>; a = suff A s; t \<in> a\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
s \<in> A\<^sup>\<clubsuit>
a = suff A s
t \<in> a

goal (3 subgoals):
 1. \<And>x. \<lbrakk>x \<in> B; t \<in> x\<rbrakk> \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> x
 2. \<And>x y. \<lbrakk>x open; t \<in> x \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> x; y open; t \<in> y \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> y; t \<in> x \<inter> y\<rbrakk> \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> x \<inter> y
 3. \<And>M. \<lbrakk>\<forall>ta\<in>M. ta open \<and> (t \<in> ta \<longrightarrow> (\<exists>r\<in>pfinpref A t. suff A r \<subseteq> ta)); t \<in> \<Union> M\<rbrakk> \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> \<Union> M
[PROOF STEP]
from sA as ta
[PROOF STATE]
proof (chain)
picking this:
s \<in> A\<^sup>\<clubsuit>
a = suff A s
t \<in> a
[PROOF STEP]
have "s \<in> pfinpref A t"
[PROOF STATE]
proof (prove)
using this:
s \<in> A\<^sup>\<clubsuit>
a = suff A s
t \<in> a

goal (1 subgoal):
 1. s \<in> pfinpref A t
[PROOF STEP]
by (auto simp: pfinpref_def dest: suff_finpref)
[PROOF STATE]
proof (state)
this:
s \<in> pfinpref A t

goal (3 subgoals):
 1. \<And>x. \<lbrakk>x \<in> B; t \<in> x\<rbrakk> \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> x
 2. \<And>x y. \<lbrakk>x open; t \<in> x \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> x; y open; t \<in> y \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> y; t \<in> x \<inter> y\<rbrakk> \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> x \<inter> y
 3. \<And>M. \<lbrakk>\<forall>ta\<in>M. ta open \<and> (t \<in> ta \<longrightarrow> (\<exists>r\<in>pfinpref A t. suff A r \<subseteq> ta)); t \<in> \<Union> M\<rbrakk> \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> \<Union> M
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
s \<in> pfinpref A t

goal (1 subgoal):
 1. \<exists>r\<in>pfinpref A t. suff A r \<subseteq> a
[PROOF STEP]
using as
[PROOF STATE]
proof (prove)
using this:
s \<in> pfinpref A t
a = suff A s

goal (1 subgoal):
 1. \<exists>r\<in>pfinpref A t. suff A r \<subseteq> a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>r\<in>pfinpref A t. suff A r \<subseteq> a

goal (2 subgoals):
 1. \<And>x y. \<lbrakk>x open; t \<in> x \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> x; y open; t \<in> y \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> y; t \<in> x \<inter> y\<rbrakk> \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> x \<inter> y
 2. \<And>M. \<lbrakk>\<forall>ta\<in>M. ta open \<and> (t \<in> ta \<longrightarrow> (\<exists>r\<in>pfinpref A t. suff A r \<subseteq> ta)); t \<in> \<Union> M\<rbrakk> \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> \<Union> M
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>x open; t \<in> x \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> x; y open; t \<in> y \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> y; t \<in> x \<inter> y\<rbrakk> \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> x \<inter> y
 2. \<And>M. \<lbrakk>\<forall>ta\<in>M. ta open \<and> (t \<in> ta \<longrightarrow> (\<exists>r\<in>pfinpref A t. suff A r \<subseteq> ta)); t \<in> \<Union> M\<rbrakk> \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> \<Union> M
[PROOF STEP]
case (inter a b)
[PROOF STATE]
proof (state)
this:
a open
t \<in> a \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> a
b open
t \<in> b \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> b
t \<in> a \<inter> b

goal (2 subgoals):
 1. \<And>x y. \<lbrakk>x open; t \<in> x \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> x; y open; t \<in> y \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> y; t \<in> x \<inter> y\<rbrakk> \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> x \<inter> y
 2. \<And>M. \<lbrakk>\<forall>ta\<in>M. ta open \<and> (t \<in> ta \<longrightarrow> (\<exists>r\<in>pfinpref A t. suff A r \<subseteq> ta)); t \<in> \<Union> M\<rbrakk> \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> \<Union> M
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a open
t \<in> a \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> a
b open
t \<in> b \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> b
t \<in> a \<inter> b
[PROOF STEP]
obtain r r' where
      rt: "r \<in> pfinpref A t" and ra: "suff A r \<subseteq> a" and
      r't: "r' \<in> pfinpref A t" and r'b: "suff A r' \<subseteq> b"
[PROOF STATE]
proof (prove)
using this:
a open
t \<in> a \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> a
b open
t \<in> b \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> b
t \<in> a \<inter> b

goal (1 subgoal):
 1. (\<And>r r'. \<lbrakk>r \<in> pfinpref A t; suff A r \<subseteq> a; r' \<in> pfinpref A t; suff A r' \<subseteq> b\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
r \<in> pfinpref A t
suff A r \<subseteq> a
r' \<in> pfinpref A t
suff A r' \<subseteq> b

goal (2 subgoals):
 1. \<And>x y. \<lbrakk>x open; t \<in> x \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> x; y open; t \<in> y \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> y; t \<in> x \<inter> y\<rbrakk> \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> x \<inter> y
 2. \<And>M. \<lbrakk>\<forall>ta\<in>M. ta open \<and> (t \<in> ta \<longrightarrow> (\<exists>r\<in>pfinpref A t. suff A r \<subseteq> ta)); t \<in> \<Union> M\<rbrakk> \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> \<Union> M
[PROOF STEP]
from rt r't
[PROOF STATE]
proof (chain)
picking this:
r \<in> pfinpref A t
r' \<in> pfinpref A t
[PROOF STEP]
have "r \<le> r' \<or> r' \<le> r"
[PROOF STATE]
proof (prove)
using this:
r \<in> pfinpref A t
r' \<in> pfinpref A t

goal (1 subgoal):
 1. r \<le> r' \<or> r' \<le> r
[PROOF STEP]
by (auto simp: pfinpref_def finpref_def dest: pref_locally_linear)
[PROOF STATE]
proof (state)
this:
r \<le> r' \<or> r' \<le> r

goal (2 subgoals):
 1. \<And>x y. \<lbrakk>x open; t \<in> x \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> x; y open; t \<in> y \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> y; t \<in> x \<inter> y\<rbrakk> \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> x \<inter> y
 2. \<And>M. \<lbrakk>\<forall>ta\<in>M. ta open \<and> (t \<in> ta \<longrightarrow> (\<exists>r\<in>pfinpref A t. suff A r \<subseteq> ta)); t \<in> \<Union> M\<rbrakk> \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> \<Union> M
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
r \<le> r' \<or> r' \<le> r

goal (1 subgoal):
 1. \<exists>r\<in>pfinpref A t. suff A r \<subseteq> a \<inter> b
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. r \<le> r' \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> a \<inter> b
 2. r' \<le> r \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> a \<inter> b
[PROOF STEP]
assume "r \<le> r'"
[PROOF STATE]
proof (state)
this:
r \<le> r'

goal (2 subgoals):
 1. r \<le> r' \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> a \<inter> b
 2. r' \<le> r \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> a \<inter> b
[PROOF STEP]
hence "suff A r' \<subseteq> suff A r"
[PROOF STATE]
proof (prove)
using this:
r \<le> r'

goal (1 subgoal):
 1. suff A r' \<subseteq> suff A r
[PROOF STEP]
by (rule suff_mono2)
[PROOF STATE]
proof (state)
this:
suff A r' \<subseteq> suff A r

goal (2 subgoals):
 1. r \<le> r' \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> a \<inter> b
 2. r' \<le> r \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> a \<inter> b
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
suff A r' \<subseteq> suff A r

goal (1 subgoal):
 1. \<exists>r\<in>pfinpref A t. suff A r \<subseteq> a \<inter> b
[PROOF STEP]
using r't ra r'b
[PROOF STATE]
proof (prove)
using this:
suff A r' \<subseteq> suff A r
r' \<in> pfinpref A t
suff A r \<subseteq> a
suff A r' \<subseteq> b

goal (1 subgoal):
 1. \<exists>r\<in>pfinpref A t. suff A r \<subseteq> a \<inter> b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>r\<in>pfinpref A t. suff A r \<subseteq> a \<inter> b

goal (1 subgoal):
 1. r' \<le> r \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> a \<inter> b
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. r' \<le> r \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> a \<inter> b
[PROOF STEP]
assume "r' \<le> r"
[PROOF STATE]
proof (state)
this:
r' \<le> r

goal (1 subgoal):
 1. r' \<le> r \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> a \<inter> b
[PROOF STEP]
hence "suff A r \<subseteq> suff A r'"
[PROOF STATE]
proof (prove)
using this:
r' \<le> r

goal (1 subgoal):
 1. suff A r \<subseteq> suff A r'
[PROOF STEP]
by (rule suff_mono2)
[PROOF STATE]
proof (state)
this:
suff A r \<subseteq> suff A r'

goal (1 subgoal):
 1. r' \<le> r \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> a \<inter> b
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
suff A r \<subseteq> suff A r'

goal (1 subgoal):
 1. \<exists>r\<in>pfinpref A t. suff A r \<subseteq> a \<inter> b
[PROOF STEP]
using rt r'b ra
[PROOF STATE]
proof (prove)
using this:
suff A r \<subseteq> suff A r'
r \<in> pfinpref A t
suff A r' \<subseteq> b
suff A r \<subseteq> a

goal (1 subgoal):
 1. \<exists>r\<in>pfinpref A t. suff A r \<subseteq> a \<inter> b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>r\<in>pfinpref A t. suff A r \<subseteq> a \<inter> b

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>r\<in>pfinpref A t. suff A r \<subseteq> a \<inter> b

goal (1 subgoal):
 1. \<And>M. \<lbrakk>\<forall>ta\<in>M. ta open \<and> (t \<in> ta \<longrightarrow> (\<exists>r\<in>pfinpref A t. suff A r \<subseteq> ta)); t \<in> \<Union> M\<rbrakk> \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> \<Union> M
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>M. \<lbrakk>\<forall>ta\<in>M. ta open \<and> (t \<in> ta \<longrightarrow> (\<exists>r\<in>pfinpref A t. suff A r \<subseteq> ta)); t \<in> \<Union> M\<rbrakk> \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> \<Union> M
[PROOF STEP]
case (union M)
[PROOF STATE]
proof (state)
this:
\<forall>ta\<in>M. ta open \<and> (t \<in> ta \<longrightarrow> (\<exists>r\<in>pfinpref A t. suff A r \<subseteq> ta))
t \<in> \<Union> M

goal (1 subgoal):
 1. \<And>M. \<lbrakk>\<forall>ta\<in>M. ta open \<and> (t \<in> ta \<longrightarrow> (\<exists>r\<in>pfinpref A t. suff A r \<subseteq> ta)); t \<in> \<Union> M\<rbrakk> \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> \<Union> M
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>ta\<in>M. ta open \<and> (t \<in> ta \<longrightarrow> (\<exists>r\<in>pfinpref A t. suff A r \<subseteq> ta))
t \<in> \<Union> M
[PROOF STEP]
obtain v where
      "t \<in> v" and vM: "v \<in> M"
[PROOF STATE]
proof (prove)
using this:
\<forall>ta\<in>M. ta open \<and> (t \<in> ta \<longrightarrow> (\<exists>r\<in>pfinpref A t. suff A r \<subseteq> ta))
t \<in> \<Union> M

goal (1 subgoal):
 1. (\<And>v. \<lbrakk>t \<in> v; v \<in> M\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
t \<in> v
v \<in> M

goal (1 subgoal):
 1. \<And>M. \<lbrakk>\<forall>ta\<in>M. ta open \<and> (t \<in> ta \<longrightarrow> (\<exists>r\<in>pfinpref A t. suff A r \<subseteq> ta)); t \<in> \<Union> M\<rbrakk> \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> \<Union> M
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
t \<in> v
v \<in> M
[PROOF STEP]
obtain r where "r\<in>pfinpref A t" "suff A r \<subseteq> v"
[PROOF STATE]
proof (prove)
using this:
t \<in> v
v \<in> M

goal (1 subgoal):
 1. (\<And>r. \<lbrakk>r \<in> pfinpref A t; suff A r \<subseteq> v\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using union
[PROOF STATE]
proof (prove)
using this:
t \<in> v
v \<in> M
\<forall>ta\<in>M. ta open \<and> (t \<in> ta \<longrightarrow> (\<exists>r\<in>pfinpref A t. suff A r \<subseteq> ta))
t \<in> \<Union> M

goal (1 subgoal):
 1. (\<And>r. \<lbrakk>r \<in> pfinpref A t; suff A r \<subseteq> v\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
r \<in> pfinpref A t
suff A r \<subseteq> v

goal (1 subgoal):
 1. \<And>M. \<lbrakk>\<forall>ta\<in>M. ta open \<and> (t \<in> ta \<longrightarrow> (\<exists>r\<in>pfinpref A t. suff A r \<subseteq> ta)); t \<in> \<Union> M\<rbrakk> \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> \<Union> M
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
r \<in> pfinpref A t
suff A r \<subseteq> v

goal (1 subgoal):
 1. \<exists>r\<in>pfinpref A t. suff A r \<subseteq> \<Union> M
[PROOF STEP]
using vM
[PROOF STATE]
proof (prove)
using this:
r \<in> pfinpref A t
suff A r \<subseteq> v
v \<in> M

goal (1 subgoal):
 1. \<exists>r\<in>pfinpref A t. suff A r \<subseteq> \<Union> M
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>r\<in>pfinpref A t. suff A r \<subseteq> \<Union> M

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>r\<in>pfinpref A t. suff A r \<subseteq> m

goal (1 subgoal):
 1. R
[PROOF STEP]
with mu
[PROOF STATE]
proof (chain)
picking this:
m \<subseteq> u
\<exists>r\<in>pfinpref A t. suff A r \<subseteq> m
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
m \<subseteq> u
\<exists>r\<in>pfinpref A t. suff A r \<subseteq> m

goal (1 subgoal):
 1. R
[PROOF STEP]
by (auto intro: H)
[PROOF STATE]
proof (state)
this:
R

goal:
No subgoals!
[PROOF STEP]
qed