[STATEMENT]
lemma make_observable_transitions_mono: "ts |\<subseteq>| (make_observable_transitions base_trans nexts dones ts)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ts |\<subseteq>| make_observable_transitions base_trans nexts dones ts
[PROOF STEP]
proof (induction rule: make_observable_transitions.induct[of "\<lambda> base_trans nexts dones ts . ts |\<subseteq>| (make_observable_transitions base_trans nexts dones ts)"])
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>base_trans nexts dones ts. (\<And>x xa xb xc. \<lbrakk>x = ffUnion ((\<lambda>q. let qts = ffilter (\<lambda>t. t_source t |\<in>| q) base_trans in Let ((\<lambda>t. (t_input t, t_output t)) |`| qts) ((|`|) (\<lambda>(x, y). (q, x, y, t_target |`| ffilter (\<lambda>t. (t_input t, t_output t) = (x, y)) qts)))) |`| nexts); xa = dones |\<union>| nexts; xb = ts |\<union>| x; xc = t_target |`| x |-| xa; xc \<noteq> {||}\<rbrakk> \<Longrightarrow> xb |\<subseteq>| make_observable_transitions base_trans xc xa xb) \<Longrightarrow> ts |\<subseteq>| make_observable_transitions base_trans nexts dones ts
[PROOF STEP]
case (1 base_trans nexts dones ts)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x = ffUnion ((\<lambda>q. let qts = ffilter (\<lambda>t. t_source t |\<in>| q) base_trans in Let ((\<lambda>t. (t_input t, t_output t)) |`| qts) ((|`|) (\<lambda>(x, y). (q, x, y, t_target |`| ffilter (\<lambda>t. (t_input t, t_output t) = (x, y)) qts)))) |`| nexts); ?xa = dones |\<union>| nexts; ?xb = ts |\<union>| ?x; ?xc = t_target |`| ?x |-| ?xa; ?xc \<noteq> {||}\<rbrakk> \<Longrightarrow> ?xb |\<subseteq>| make_observable_transitions base_trans ?xc ?xa ?xb

goal (1 subgoal):
 1. \<And>base_trans nexts dones ts. (\<And>x xa xb xc. \<lbrakk>x = ffUnion ((\<lambda>q. let qts = ffilter (\<lambda>t. t_source t |\<in>| q) base_trans in Let ((\<lambda>t. (t_input t, t_output t)) |`| qts) ((|`|) (\<lambda>(x, y). (q, x, y, t_target |`| ffilter (\<lambda>t. (t_input t, t_output t) = (x, y)) qts)))) |`| nexts); xa = dones |\<union>| nexts; xb = ts |\<union>| x; xc = t_target |`| x |-| xa; xc \<noteq> {||}\<rbrakk> \<Longrightarrow> xb |\<subseteq>| make_observable_transitions base_trans xc xa xb) \<Longrightarrow> ts |\<subseteq>| make_observable_transitions base_trans nexts dones ts
[PROOF STEP]
define qtrans where qtrans_def: "qtrans = ffUnion (fimage (\<lambda> q . (let qts = ffilter (\<lambda>t . t_source t |\<in>| q) base_trans;
                                           ios = fimage (\<lambda> t . (t_input t, t_output t)) qts
                                       in fimage (\<lambda>(x,y) . (q,x,y, t_target |`| ((ffilter (\<lambda>t . (t_input t, t_output t) = (x,y)) qts)))) ios)) nexts)"
[PROOF STATE]
proof (state)
this:
qtrans = ffUnion ((\<lambda>q. let qts = ffilter (\<lambda>t. t_source t |\<in>| q) base_trans in Let ((\<lambda>t. (t_input t, t_output t)) |`| qts) ((|`|) (\<lambda>(x, y). (q, x, y, t_target |`| ffilter (\<lambda>t. (t_input t, t_output t) = (x, y)) qts)))) |`| nexts)

goal (1 subgoal):
 1. \<And>base_trans nexts dones ts. (\<And>x xa xb xc. \<lbrakk>x = ffUnion ((\<lambda>q. let qts = ffilter (\<lambda>t. t_source t |\<in>| q) base_trans in Let ((\<lambda>t. (t_input t, t_output t)) |`| qts) ((|`|) (\<lambda>(x, y). (q, x, y, t_target |`| ffilter (\<lambda>t. (t_input t, t_output t) = (x, y)) qts)))) |`| nexts); xa = dones |\<union>| nexts; xb = ts |\<union>| x; xc = t_target |`| x |-| xa; xc \<noteq> {||}\<rbrakk> \<Longrightarrow> xb |\<subseteq>| make_observable_transitions base_trans xc xa xb) \<Longrightarrow> ts |\<subseteq>| make_observable_transitions base_trans nexts dones ts
[PROOF STEP]
have qtrans_prop: "\<And> t . t |\<in>| qtrans \<longleftrightarrow> t_source t |\<in>| nexts \<and> t_target t \<noteq> {||} \<and> fset (t_target t) = t_target ` {t' | t' . t' |\<in>| base_trans \<and> t_source t' |\<in>| t_source t \<and> t_input t' = t_input t \<and> t_output t' = t_output t}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t. (t |\<in>| qtrans) = (t_source t |\<in>| nexts \<and> t_target t \<noteq> {||} \<and> fset (t_target t) = t_target ` {t' |t'. t' |\<in>| base_trans \<and> t_source t' |\<in>| t_source t \<and> t_input t' = t_input t \<and> t_output t' = t_output t})
[PROOF STEP]
using make_observable_transitions_qtrans_helper[OF qtrans_def]
[PROOF STATE]
proof (prove)
using this:
(?t |\<in>| qtrans) = (t_source ?t |\<in>| nexts \<and> t_target ?t \<noteq> {||} \<and> fset (t_target ?t) = t_target ` {t'. t' |\<in>| base_trans \<and> t_source t' |\<in>| t_source ?t \<and> t_input t' = t_input ?t \<and> t_output t' = t_output ?t})

goal (1 subgoal):
 1. \<And>t. (t |\<in>| qtrans) = (t_source t |\<in>| nexts \<and> t_target t \<noteq> {||} \<and> fset (t_target t) = t_target ` {t' |t'. t' |\<in>| base_trans \<and> t_source t' |\<in>| t_source t \<and> t_input t' = t_input t \<and> t_output t' = t_output t})
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
(?t |\<in>| qtrans) = (t_source ?t |\<in>| nexts \<and> t_target ?t \<noteq> {||} \<and> fset (t_target ?t) = t_target ` {t' |t'. t' |\<in>| base_trans \<and> t_source t' |\<in>| t_source ?t \<and> t_input t' = t_input ?t \<and> t_output t' = t_output ?t})

goal (1 subgoal):
 1. \<And>base_trans nexts dones ts. (\<And>x xa xb xc. \<lbrakk>x = ffUnion ((\<lambda>q. let qts = ffilter (\<lambda>t. t_source t |\<in>| q) base_trans in Let ((\<lambda>t. (t_input t, t_output t)) |`| qts) ((|`|) (\<lambda>(x, y). (q, x, y, t_target |`| ffilter (\<lambda>t. (t_input t, t_output t) = (x, y)) qts)))) |`| nexts); xa = dones |\<union>| nexts; xb = ts |\<union>| x; xc = t_target |`| x |-| xa; xc \<noteq> {||}\<rbrakk> \<Longrightarrow> xb |\<subseteq>| make_observable_transitions base_trans xc xa xb) \<Longrightarrow> ts |\<subseteq>| make_observable_transitions base_trans nexts dones ts
[PROOF STEP]
let ?dones' = "dones |\<union>| nexts"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>base_trans nexts dones ts. (\<And>x xa xb xc. \<lbrakk>x = ffUnion ((\<lambda>q. let qts = ffilter (\<lambda>t. t_source t |\<in>| q) base_trans in Let ((\<lambda>t. (t_input t, t_output t)) |`| qts) ((|`|) (\<lambda>(x, y). (q, x, y, t_target |`| ffilter (\<lambda>t. (t_input t, t_output t) = (x, y)) qts)))) |`| nexts); xa = dones |\<union>| nexts; xb = ts |\<union>| x; xc = t_target |`| x |-| xa; xc \<noteq> {||}\<rbrakk> \<Longrightarrow> xb |\<subseteq>| make_observable_transitions base_trans xc xa xb) \<Longrightarrow> ts |\<subseteq>| make_observable_transitions base_trans nexts dones ts
[PROOF STEP]
let ?ts'    = "ts |\<union>| qtrans"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>base_trans nexts dones ts. (\<And>x xa xb xc. \<lbrakk>x = ffUnion ((\<lambda>q. let qts = ffilter (\<lambda>t. t_source t |\<in>| q) base_trans in Let ((\<lambda>t. (t_input t, t_output t)) |`| qts) ((|`|) (\<lambda>(x, y). (q, x, y, t_target |`| ffilter (\<lambda>t. (t_input t, t_output t) = (x, y)) qts)))) |`| nexts); xa = dones |\<union>| nexts; xb = ts |\<union>| x; xc = t_target |`| x |-| xa; xc \<noteq> {||}\<rbrakk> \<Longrightarrow> xb |\<subseteq>| make_observable_transitions base_trans xc xa xb) \<Longrightarrow> ts |\<subseteq>| make_observable_transitions base_trans nexts dones ts
[PROOF STEP]
let ?nexts' = "(fimage t_target qtrans) |-| ?dones'"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>base_trans nexts dones ts. (\<And>x xa xb xc. \<lbrakk>x = ffUnion ((\<lambda>q. let qts = ffilter (\<lambda>t. t_source t |\<in>| q) base_trans in Let ((\<lambda>t. (t_input t, t_output t)) |`| qts) ((|`|) (\<lambda>(x, y). (q, x, y, t_target |`| ffilter (\<lambda>t. (t_input t, t_output t) = (x, y)) qts)))) |`| nexts); xa = dones |\<union>| nexts; xb = ts |\<union>| x; xc = t_target |`| x |-| xa; xc \<noteq> {||}\<rbrakk> \<Longrightarrow> xb |\<subseteq>| make_observable_transitions base_trans xc xa xb) \<Longrightarrow> ts |\<subseteq>| make_observable_transitions base_trans nexts dones ts
[PROOF STEP]
have res_cases: "make_observable_transitions base_trans nexts dones ts = (if ?nexts' = {||} 
            then ?ts'
            else make_observable_transitions base_trans ?nexts' ?dones' ?ts')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. make_observable_transitions base_trans nexts dones ts = (if t_target |`| qtrans |-| (dones |\<union>| nexts) = {||} then ts |\<union>| qtrans else make_observable_transitions base_trans (t_target |`| qtrans |-| (dones |\<union>| nexts)) (dones |\<union>| nexts) (ts |\<union>| qtrans))
[PROOF STEP]
unfolding make_observable_transitions.simps[of base_trans nexts dones ts] qtrans_def Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if t_target |`| ffUnion ((\<lambda>q. (\<lambda>(x, y). (q, x, y, t_target |`| ffilter (\<lambda>t. (t_input t, t_output t) = (x, y)) (ffilter (\<lambda>t. t_source t |\<in>| q) base_trans))) |`| (\<lambda>t. (t_input t, t_output t)) |`| ffilter (\<lambda>t. t_source t |\<in>| q) base_trans) |`| nexts) |-| (dones |\<union>| nexts) = {||} then ts |\<union>| ffUnion ((\<lambda>q. (\<lambda>(x, y). (q, x, y, t_target |`| ffilter (\<lambda>t. (t_input t, t_output t) = (x, y)) (ffilter (\<lambda>t. t_source t |\<in>| q) base_trans))) |`| (\<lambda>t. (t_input t, t_output t)) |`| ffilter (\<lambda>t. t_source t |\<in>| q) base_trans) |`| nexts) else make_observable_transitions base_trans (t_target |`| ffUnion ((\<lambda>q. (\<lambda>(x, y). (q, x, y, t_target |`| ffilter (\<lambda>t. (t_input t, t_output t) = (x, y)) (ffilter (\<lambda>t. t_source t |\<in>| q) base_trans))) |`| (\<lambda>t. (t_input t, t_output t)) |`| ffilter (\<lambda>t. t_source t |\<in>| q) base_trans) |`| nexts) |-| (dones |\<union>| nexts)) (dones |\<union>| nexts) (ts |\<union>| ffUnion ((\<lambda>q. (\<lambda>(x, y). (q, x, y, t_target |`| ffilter (\<lambda>t. (t_input t, t_output t) = (x, y)) (ffilter (\<lambda>t. t_source t |\<in>| q) base_trans))) |`| (\<lambda>t. (t_input t, t_output t)) |`| ffilter (\<lambda>t. t_source t |\<in>| q) base_trans) |`| nexts))) = (if t_target |`| ffUnion ((\<lambda>q. (\<lambda>(x, y). (q, x, y, t_target |`| ffilter (\<lambda>t. (t_input t, t_output t) = (x, y)) (ffilter (\<lambda>t. t_source t |\<in>| q) base_trans))) |`| (\<lambda>t. (t_input t, t_output t)) |`| ffilter (\<lambda>t. t_source t |\<in>| q) base_trans) |`| nexts) |-| (dones |\<union>| nexts) = {||} then ts |\<union>| ffUnion ((\<lambda>q. (\<lambda>(x, y). (q, x, y, t_target |`| ffilter (\<lambda>t. (t_input t, t_output t) = (x, y)) (ffilter (\<lambda>t. t_source t |\<in>| q) base_trans))) |`| (\<lambda>t. (t_input t, t_output t)) |`| ffilter (\<lambda>t. t_source t |\<in>| q) base_trans) |`| nexts) else make_observable_transitions base_trans (t_target |`| ffUnion ((\<lambda>q. (\<lambda>(x, y). (q, x, y, t_target |`| ffilter (\<lambda>t. (t_input t, t_output t) = (x, y)) (ffilter (\<lambda>t. t_source t |\<in>| q) base_trans))) |`| (\<lambda>t. (t_input t, t_output t)) |`| ffilter (\<lambda>t. t_source t |\<in>| q) base_trans) |`| nexts) |-| (dones |\<union>| nexts)) (dones |\<union>| nexts) (ts |\<union>| ffUnion ((\<lambda>q. (\<lambda>(x, y). (q, x, y, t_target |`| ffilter (\<lambda>t. (t_input t, t_output t) = (x, y)) (ffilter (\<lambda>t. t_source t |\<in>| q) base_trans))) |`| (\<lambda>t. (t_input t, t_output t)) |`| ffilter (\<lambda>t. t_source t |\<in>| q) base_trans) |`| nexts)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
make_observable_transitions base_trans nexts dones ts = (if t_target |`| qtrans |-| (dones |\<union>| nexts) = {||} then ts |\<union>| qtrans else make_observable_transitions base_trans (t_target |`| qtrans |-| (dones |\<union>| nexts)) (dones |\<union>| nexts) (ts |\<union>| qtrans))

goal (1 subgoal):
 1. \<And>base_trans nexts dones ts. (\<And>x xa xb xc. \<lbrakk>x = ffUnion ((\<lambda>q. let qts = ffilter (\<lambda>t. t_source t |\<in>| q) base_trans in Let ((\<lambda>t. (t_input t, t_output t)) |`| qts) ((|`|) (\<lambda>(x, y). (q, x, y, t_target |`| ffilter (\<lambda>t. (t_input t, t_output t) = (x, y)) qts)))) |`| nexts); xa = dones |\<union>| nexts; xb = ts |\<union>| x; xc = t_target |`| x |-| xa; xc \<noteq> {||}\<rbrakk> \<Longrightarrow> xb |\<subseteq>| make_observable_transitions base_trans xc xa xb) \<Longrightarrow> ts |\<subseteq>| make_observable_transitions base_trans nexts dones ts
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ts |\<subseteq>| make_observable_transitions base_trans nexts dones ts
[PROOF STEP]
proof (cases "?nexts' = {||}")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. t_target |`| qtrans |-| (dones |\<union>| nexts) = {||} \<Longrightarrow> ts |\<subseteq>| make_observable_transitions base_trans nexts dones ts
 2. t_target |`| qtrans |-| (dones |\<union>| nexts) \<noteq> {||} \<Longrightarrow> ts |\<subseteq>| make_observable_transitions base_trans nexts dones ts
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
t_target |`| qtrans |-| (dones |\<union>| nexts) = {||}

goal (2 subgoals):
 1. t_target |`| qtrans |-| (dones |\<union>| nexts) = {||} \<Longrightarrow> ts |\<subseteq>| make_observable_transitions base_trans nexts dones ts
 2. t_target |`| qtrans |-| (dones |\<union>| nexts) \<noteq> {||} \<Longrightarrow> ts |\<subseteq>| make_observable_transitions base_trans nexts dones ts
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
t_target |`| qtrans |-| (dones |\<union>| nexts) = {||}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
t_target |`| qtrans |-| (dones |\<union>| nexts) = {||}

goal (1 subgoal):
 1. ts |\<subseteq>| make_observable_transitions base_trans nexts dones ts
[PROOF STEP]
using res_cases
[PROOF STATE]
proof (prove)
using this:
t_target |`| qtrans |-| (dones |\<union>| nexts) = {||}
make_observable_transitions base_trans nexts dones ts = (if t_target |`| qtrans |-| (dones |\<union>| nexts) = {||} then ts |\<union>| qtrans else make_observable_transitions base_trans (t_target |`| qtrans |-| (dones |\<union>| nexts)) (dones |\<union>| nexts) (ts |\<union>| qtrans))

goal (1 subgoal):
 1. ts |\<subseteq>| make_observable_transitions base_trans nexts dones ts
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ts |\<subseteq>| make_observable_transitions base_trans nexts dones ts

goal (1 subgoal):
 1. t_target |`| qtrans |-| (dones |\<union>| nexts) \<noteq> {||} \<Longrightarrow> ts |\<subseteq>| make_observable_transitions base_trans nexts dones ts
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. t_target |`| qtrans |-| (dones |\<union>| nexts) \<noteq> {||} \<Longrightarrow> ts |\<subseteq>| make_observable_transitions base_trans nexts dones ts
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
t_target |`| qtrans |-| (dones |\<union>| nexts) \<noteq> {||}

goal (1 subgoal):
 1. t_target |`| qtrans |-| (dones |\<union>| nexts) \<noteq> {||} \<Longrightarrow> ts |\<subseteq>| make_observable_transitions base_trans nexts dones ts
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
t_target |`| qtrans |-| (dones |\<union>| nexts) \<noteq> {||}
[PROOF STEP]
have "make_observable_transitions base_trans nexts dones ts = make_observable_transitions base_trans ?nexts' ?dones' ?ts'"
[PROOF STATE]
proof (prove)
using this:
t_target |`| qtrans |-| (dones |\<union>| nexts) \<noteq> {||}

goal (1 subgoal):
 1. make_observable_transitions base_trans nexts dones ts = make_observable_transitions base_trans (t_target |`| qtrans |-| (dones |\<union>| nexts)) (dones |\<union>| nexts) (ts |\<union>| qtrans)
[PROOF STEP]
using res_cases
[PROOF STATE]
proof (prove)
using this:
t_target |`| qtrans |-| (dones |\<union>| nexts) \<noteq> {||}
make_observable_transitions base_trans nexts dones ts = (if t_target |`| qtrans |-| (dones |\<union>| nexts) = {||} then ts |\<union>| qtrans else make_observable_transitions base_trans (t_target |`| qtrans |-| (dones |\<union>| nexts)) (dones |\<union>| nexts) (ts |\<union>| qtrans))

goal (1 subgoal):
 1. make_observable_transitions base_trans nexts dones ts = make_observable_transitions base_trans (t_target |`| qtrans |-| (dones |\<union>| nexts)) (dones |\<union>| nexts) (ts |\<union>| qtrans)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
make_observable_transitions base_trans nexts dones ts = make_observable_transitions base_trans (t_target |`| qtrans |-| (dones |\<union>| nexts)) (dones |\<union>| nexts) (ts |\<union>| qtrans)

goal (1 subgoal):
 1. t_target |`| qtrans |-| (dones |\<union>| nexts) \<noteq> {||} \<Longrightarrow> ts |\<subseteq>| make_observable_transitions base_trans nexts dones ts
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
make_observable_transitions base_trans nexts dones ts = make_observable_transitions base_trans (t_target |`| qtrans |-| (dones |\<union>| nexts)) (dones |\<union>| nexts) (ts |\<union>| qtrans)

goal (1 subgoal):
 1. t_target |`| qtrans |-| (dones |\<union>| nexts) \<noteq> {||} \<Longrightarrow> ts |\<subseteq>| make_observable_transitions base_trans nexts dones ts
[PROOF STEP]
have "ts |\<union>| qtrans |\<subseteq>| make_observable_transitions base_trans ?nexts' ?dones' ?ts'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ts |\<union>| qtrans |\<subseteq>| make_observable_transitions base_trans (t_target |`| qtrans |-| (dones |\<union>| nexts)) (dones |\<union>| nexts) (ts |\<union>| qtrans)
[PROOF STEP]
using "1"[OF qtrans_def _ _ _ False, of ?dones' ?ts']
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>dones |\<union>| nexts = dones |\<union>| nexts; ts |\<union>| qtrans = ts |\<union>| qtrans; t_target |`| qtrans |-| (dones |\<union>| nexts) = t_target |`| qtrans |-| (dones |\<union>| nexts)\<rbrakk> \<Longrightarrow> ts |\<union>| qtrans |\<subseteq>| make_observable_transitions base_trans (t_target |`| qtrans |-| (dones |\<union>| nexts)) (dones |\<union>| nexts) (ts |\<union>| qtrans)

goal (1 subgoal):
 1. ts |\<union>| qtrans |\<subseteq>| make_observable_transitions base_trans (t_target |`| qtrans |-| (dones |\<union>| nexts)) (dones |\<union>| nexts) (ts |\<union>| qtrans)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ts |\<union>| qtrans |\<subseteq>| make_observable_transitions base_trans (t_target |`| qtrans |-| (dones |\<union>| nexts)) (dones |\<union>| nexts) (ts |\<union>| qtrans)

goal (1 subgoal):
 1. t_target |`| qtrans |-| (dones |\<union>| nexts) \<noteq> {||} \<Longrightarrow> ts |\<subseteq>| make_observable_transitions base_trans nexts dones ts
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
make_observable_transitions base_trans nexts dones ts = make_observable_transitions base_trans (t_target |`| qtrans |-| (dones |\<union>| nexts)) (dones |\<union>| nexts) (ts |\<union>| qtrans)
ts |\<union>| qtrans |\<subseteq>| make_observable_transitions base_trans (t_target |`| qtrans |-| (dones |\<union>| nexts)) (dones |\<union>| nexts) (ts |\<union>| qtrans)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
make_observable_transitions base_trans nexts dones ts = make_observable_transitions base_trans (t_target |`| qtrans |-| (dones |\<union>| nexts)) (dones |\<union>| nexts) (ts |\<union>| qtrans)
ts |\<union>| qtrans |\<subseteq>| make_observable_transitions base_trans (t_target |`| qtrans |-| (dones |\<union>| nexts)) (dones |\<union>| nexts) (ts |\<union>| qtrans)

goal (1 subgoal):
 1. ts |\<subseteq>| make_observable_transitions base_trans nexts dones ts
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ts |\<subseteq>| make_observable_transitions base_trans nexts dones ts

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
ts |\<subseteq>| make_observable_transitions base_trans nexts dones ts

goal:
No subgoals!
[PROOF STEP]
qed