[STATEMENT]
theorem (in trace_top) alpern_schneider:
assumes Psub:     "P \<subseteq> A\<^sup>\<infinity>"
  shows "\<exists> S L. safety A S \<and> liveness A L \<and> P = S \<inter> L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>S L. safety A S \<and> liveness A L \<and> P = S \<inter> L
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>S L. safety A S \<and> liveness A L \<and> P = S \<inter> L
[PROOF STEP]
from Psub
[PROOF STATE]
proof (chain)
picking this:
P \<subseteq> A\<^sup>\<infinity>
[PROOF STEP]
have "P \<subseteq> carrier"
[PROOF STATE]
proof (prove)
using this:
P \<subseteq> A\<^sup>\<infinity>

goal (1 subgoal):
 1. P \<subseteq> carrier
[PROOF STEP]
by (simp add: ttop_carrier)
[PROOF STATE]
proof (state)
this:
P \<subseteq> carrier

goal (1 subgoal):
 1. \<exists>S L. safety A S \<and> liveness A L \<and> P = S \<inter> L
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
P \<subseteq> carrier
[PROOF STEP]
obtain L S where
    Lsub: "L \<subseteq> carrier" and
    Ssub: "S \<subseteq> carrier" and
    Sclosed: "S closed" and
    Ldense: "L dense" and
    Pinter: "P = S \<inter> L"
[PROOF STATE]
proof (prove)
using this:
P \<subseteq> carrier

goal (1 subgoal):
 1. (\<And>L S. \<lbrakk>L \<subseteq> carrier; S \<subseteq> carrier; S closed; L dense; P = S \<inter> L\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (blast elim: topology.ex_dense_closure_interE [OF topology])
[PROOF STATE]
proof (state)
this:
L \<subseteq> carrier
S \<subseteq> carrier
S closed
L dense
P = S \<inter> L

goal (1 subgoal):
 1. \<exists>S L. safety A S \<and> liveness A L \<and> P = S \<inter> L
[PROOF STEP]
from Ssub Sclosed
[PROOF STATE]
proof (chain)
picking this:
S \<subseteq> carrier
S closed
[PROOF STEP]
have "safety A S"
[PROOF STATE]
proof (prove)
using this:
S \<subseteq> carrier
S closed

goal (1 subgoal):
 1. safety A S
[PROOF STEP]
by (simp add: safety_closed_iff ttop_carrier)
[PROOF STATE]
proof (state)
this:
safety A S

goal (1 subgoal):
 1. \<exists>S L. safety A S \<and> liveness A L \<and> P = S \<inter> L
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
safety A S

goal (1 subgoal):
 1. \<exists>S L. safety A S \<and> liveness A L \<and> P = S \<inter> L
[PROOF STEP]
from Lsub Ldense
[PROOF STATE]
proof (chain)
picking this:
L \<subseteq> carrier
L dense
[PROOF STEP]
have "liveness A L"
[PROOF STATE]
proof (prove)
using this:
L \<subseteq> carrier
L dense

goal (1 subgoal):
 1. liveness A L
[PROOF STEP]
by (simp add: liveness_dense_iff ttop_carrier)
[PROOF STATE]
proof (state)
this:
liveness A L

goal (1 subgoal):
 1. \<exists>S L. safety A S \<and> liveness A L \<and> P = S \<inter> L
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
safety A S
liveness A L
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
safety A S
liveness A L

goal (1 subgoal):
 1. \<exists>S L. safety A S \<and> liveness A L \<and> P = S \<inter> L
[PROOF STEP]
using Pinter
[PROOF STATE]
proof (prove)
using this:
safety A S
liveness A L
P = S \<inter> L

goal (1 subgoal):
 1. \<exists>S L. safety A S \<and> liveness A L \<and> P = S \<inter> L
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>S L. safety A S \<and> liveness A L \<and> P = S \<inter> L

goal:
No subgoals!
[PROOF STEP]
qed