[STATEMENT]
lemma (in trace_top) liveness_dense_iff:
  assumes P: "P \<subseteq> A\<^sup>\<infinity>"
  shows "liveness A P = (P dense)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. liveness A P = (P dense)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. liveness A P = (P dense)
[PROOF STEP]
have "liveness A P = (\<forall>r\<in>A\<^sup>\<star>. \<exists> s \<in> A\<^sup>\<infinity>. r @@ s \<in> P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. liveness A P = (\<forall>r\<in>A\<^sup>\<star>. \<exists>s\<in>A\<^sup>\<infinity>. r @@ s \<in> P)
[PROOF STEP]
by (simp add: liveness_def)
[PROOF STATE]
proof (state)
this:
liveness A P = (\<forall>r\<in>A\<^sup>\<star>. \<exists>s\<in>A\<^sup>\<infinity>. r @@ s \<in> P)

goal (1 subgoal):
 1. liveness A P = (P dense)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
liveness A P = (\<forall>r\<in>A\<^sup>\<star>. \<exists>s\<in>A\<^sup>\<infinity>. r @@ s \<in> P)

goal (1 subgoal):
 1. liveness A P = (P dense)
[PROOF STEP]
have "\<dots> = (\<forall>x\<in>A\<^sup>\<infinity>. \<forall> r \<in> finpref A x. \<exists> s \<in> A\<^sup>\<infinity>. r @@ s \<in> P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>r\<in>A\<^sup>\<star>. \<exists>s\<in>A\<^sup>\<infinity>. r @@ s \<in> P) = (\<forall>x\<in>A\<^sup>\<infinity>. \<forall>r\<in>finpref A x. \<exists>s\<in>A\<^sup>\<infinity>. r @@ s \<in> P)
[PROOF STEP]
by (auto simp: finpref_def dest: finsubsetall)
[PROOF STATE]
proof (state)
this:
(\<forall>r\<in>A\<^sup>\<star>. \<exists>s\<in>A\<^sup>\<infinity>. r @@ s \<in> P) = (\<forall>x\<in>A\<^sup>\<infinity>. \<forall>r\<in>finpref A x. \<exists>s\<in>A\<^sup>\<infinity>. r @@ s \<in> P)

goal (1 subgoal):
 1. liveness A P = (P dense)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<forall>r\<in>A\<^sup>\<star>. \<exists>s\<in>A\<^sup>\<infinity>. r @@ s \<in> P) = (\<forall>x\<in>A\<^sup>\<infinity>. \<forall>r\<in>finpref A x. \<exists>s\<in>A\<^sup>\<infinity>. r @@ s \<in> P)

goal (1 subgoal):
 1. liveness A P = (P dense)
[PROOF STEP]
have "\<dots> = (\<forall>x\<in>A\<^sup>\<infinity>. x adh P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>x\<in>A\<^sup>\<infinity>. \<forall>r\<in>finpref A x. \<exists>s\<in>A\<^sup>\<infinity>. r @@ s \<in> P) = (\<forall>x\<in>A\<^sup>\<infinity>. x adh P)
[PROOF STEP]
using P
[PROOF STATE]
proof (prove)
using this:
P \<subseteq> A\<^sup>\<infinity>

goal (1 subgoal):
 1. (\<forall>x\<in>A\<^sup>\<infinity>. \<forall>r\<in>finpref A x. \<exists>s\<in>A\<^sup>\<infinity>. r @@ s \<in> P) = (\<forall>x\<in>A\<^sup>\<infinity>. x adh P)
[PROOF STEP]
by (simp add: adh_lemma)
[PROOF STATE]
proof (state)
this:
(\<forall>x\<in>A\<^sup>\<infinity>. \<forall>r\<in>finpref A x. \<exists>s\<in>A\<^sup>\<infinity>. r @@ s \<in> P) = (\<forall>x\<in>A\<^sup>\<infinity>. x adh P)

goal (1 subgoal):
 1. liveness A P = (P dense)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<forall>x\<in>A\<^sup>\<infinity>. \<forall>r\<in>finpref A x. \<exists>s\<in>A\<^sup>\<infinity>. r @@ s \<in> P) = (\<forall>x\<in>A\<^sup>\<infinity>. x adh P)

goal (1 subgoal):
 1. liveness A P = (P dense)
[PROOF STEP]
have "\<dots> = (A\<^sup>\<infinity> \<subseteq> closure P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>x\<in>A\<^sup>\<infinity>. x adh P) = (A\<^sup>\<infinity> \<subseteq> closure P)
[PROOF STEP]
using P
[PROOF STATE]
proof (prove)
using this:
P \<subseteq> A\<^sup>\<infinity>

goal (1 subgoal):
 1. (\<forall>x\<in>A\<^sup>\<infinity>. x adh P) = (A\<^sup>\<infinity> \<subseteq> closure P)
[PROOF STEP]
by (auto simp: adh_closure_iff ttop_carrier)
[PROOF STATE]
proof (state)
this:
(\<forall>x\<in>A\<^sup>\<infinity>. x adh P) = (A\<^sup>\<infinity> \<subseteq> closure P)

goal (1 subgoal):
 1. liveness A P = (P dense)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<forall>x\<in>A\<^sup>\<infinity>. x adh P) = (A\<^sup>\<infinity> \<subseteq> closure P)

goal (1 subgoal):
 1. liveness A P = (P dense)
[PROOF STEP]
have "\<dots> = (P dense)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A\<^sup>\<infinity> \<subseteq> closure P) = (P dense)
[PROOF STEP]
by (simp add: liveness_def is_dense_def is_densein_def ttop_carrier)
[PROOF STATE]
proof (state)
this:
(A\<^sup>\<infinity> \<subseteq> closure P) = (P dense)

goal (1 subgoal):
 1. liveness A P = (P dense)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
liveness A P = (P dense)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
liveness A P = (P dense)

goal (1 subgoal):
 1. liveness A P = (P dense)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
liveness A P = (P dense)

goal:
No subgoals!
[PROOF STEP]
qed