[STATEMENT]
theorem SF2:
  assumes h1: "|~ \<langle>N \<and> B\<rangle>_f \<longrightarrow> \<langle>M\<rangle>_g"
      and h2: "|~ P \<and> \<circle>P \<and> \<langle>N \<and> A\<rangle>_f \<longrightarrow> B"
      and h3: "\<turnstile> P \<and> Enabled \<langle>M\<rangle>_g \<longrightarrow> Enabled \<langle>A\<rangle>_f"
      and h4: "\<turnstile> \<box>[N \<and> \<not>B]_f \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<longrightarrow> \<diamond>\<box>P"
  shows "\<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<longrightarrow> SF(M)_g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<longrightarrow> SF(M)_g
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<longrightarrow> SF(M)_g
[PROOF STEP]
have "\<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<not>\<box>\<diamond>\<langle>M\<rangle>_g \<longrightarrow> \<box>\<diamond>\<langle>M\<rangle>_g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<not> \<box>\<diamond>\<langle>M\<rangle>_g \<longrightarrow> \<box>\<diamond>\<langle>M\<rangle>_g
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<not> \<box>\<diamond>\<langle>M\<rangle>_g \<longrightarrow> \<box>\<diamond>\<langle>M\<rangle>_g
[PROOF STEP]
have 1: "\<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<not>\<box>\<diamond>\<langle>M\<rangle>_g \<longrightarrow> \<diamond>\<box>P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<not> \<box>\<diamond>\<langle>M\<rangle>_g \<longrightarrow> \<diamond>\<box>P
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<not> \<box>\<diamond>\<langle>M\<rangle>_g \<longrightarrow> \<diamond>\<box>P
[PROOF STEP]
have A: "\<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<not>\<box>\<diamond>\<langle>M\<rangle>_g \<longrightarrow>
                 \<box>(\<box>[N]_f \<and> SF(A)_f \<and> \<box>F) \<and> \<diamond>\<box>(\<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<box>[\<not>M]_g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<not> \<box>\<diamond>\<langle>M\<rangle>_g \<longrightarrow> \<box>(\<box>[N]_f \<and> SF(A)_f \<and> \<box>F) \<and> \<diamond>\<box>(\<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<box>[\<not> M]_g)
[PROOF STEP]
unfolding STL6[int_rewrite]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<not> \<box>\<diamond>\<langle>M\<rangle>_g \<longrightarrow> \<box>(\<box>[N]_f \<and> SF(A)_f \<and> \<box>F) \<and> \<diamond>\<box>\<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<diamond>\<box>\<box>[\<not> M]_g
[PROOF STEP]
(* important to do this before STL5 is applied *)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<not> \<box>\<diamond>\<langle>M\<rangle>_g \<longrightarrow> \<box>(\<box>[N]_f \<and> SF(A)_f \<and> \<box>F) \<and> \<diamond>\<box>\<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<diamond>\<box>\<box>[\<not> M]_g
[PROOF STEP]
by (auto simp: STL5[int_rewrite] dualization_rew)
[PROOF STATE]
proof (state)
this:
\<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<not> \<box>\<diamond>\<langle>M\<rangle>_g \<longrightarrow> \<box>(\<box>[N]_f \<and> SF(A)_f \<and> \<box>F) \<and> \<diamond>\<box>(\<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<box>[\<not> M]_g)

goal (1 subgoal):
 1. \<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<not> \<box>\<diamond>\<langle>M\<rangle>_g \<longrightarrow> \<diamond>\<box>P
[PROOF STEP]
have B: "\<turnstile> \<box>(\<box>[N]_f \<and> SF(A)_f \<and> \<box>F) \<and> \<diamond>\<box>(\<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<box>[\<not>M]_g) \<longrightarrow>
                 \<diamond>((\<box>[N]_f \<and> SF(A)_f \<and> \<box>F) \<and> \<box>(\<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<box>[\<not>M]_g))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile> \<box>(\<box>[N]_f \<and> SF(A)_f \<and> \<box>F) \<and> \<diamond>\<box>(\<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<box>[\<not> M]_g) \<longrightarrow> \<diamond>((\<box>[N]_f \<and> SF(A)_f \<and> \<box>F) \<and> \<box>(\<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<box>[\<not> M]_g))
[PROOF STEP]
by (rule SE2)
[PROOF STATE]
proof (state)
this:
\<turnstile> \<box>(\<box>[N]_f \<and> SF(A)_f \<and> \<box>F) \<and> \<diamond>\<box>(\<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<box>[\<not> M]_g) \<longrightarrow> \<diamond>((\<box>[N]_f \<and> SF(A)_f \<and> \<box>F) \<and> \<box>(\<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<box>[\<not> M]_g))

goal (1 subgoal):
 1. \<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<not> \<box>\<diamond>\<langle>M\<rangle>_g \<longrightarrow> \<diamond>\<box>P
[PROOF STEP]
from lift_imp_trans[OF A B]
[PROOF STATE]
proof (chain)
picking this:
\<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<not> \<box>\<diamond>\<langle>M\<rangle>_g \<longrightarrow> \<diamond>((\<box>[N]_f \<and> SF(A)_f \<and> \<box>F) \<and> \<box>(\<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<box>[\<not> M]_g))
[PROOF STEP]
have "\<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<not>\<box>\<diamond>\<langle>M\<rangle>_g \<longrightarrow>
              \<diamond>((\<box>[N]_f \<and> SF(A)_f \<and> \<box>F) \<and> (\<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<box>[\<not>M]_g))"
[PROOF STATE]
proof (prove)
using this:
\<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<not> \<box>\<diamond>\<langle>M\<rangle>_g \<longrightarrow> \<diamond>((\<box>[N]_f \<and> SF(A)_f \<and> \<box>F) \<and> \<box>(\<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<box>[\<not> M]_g))

goal (1 subgoal):
 1. \<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<not> \<box>\<diamond>\<langle>M\<rangle>_g \<longrightarrow> \<diamond>((\<box>[N]_f \<and> SF(A)_f \<and> \<box>F) \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<box>[\<not> M]_g)
[PROOF STEP]
by (simp add: STL5[int_rewrite])
[PROOF STATE]
proof (state)
this:
\<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<not> \<box>\<diamond>\<langle>M\<rangle>_g \<longrightarrow> \<diamond>((\<box>[N]_f \<and> SF(A)_f \<and> \<box>F) \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<box>[\<not> M]_g)

goal (1 subgoal):
 1. \<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<not> \<box>\<diamond>\<langle>M\<rangle>_g \<longrightarrow> \<diamond>\<box>P
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<not> \<box>\<diamond>\<langle>M\<rangle>_g \<longrightarrow> \<diamond>((\<box>[N]_f \<and> SF(A)_f \<and> \<box>F) \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<box>[\<not> M]_g)

goal (1 subgoal):
 1. \<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<not> \<box>\<diamond>\<langle>M\<rangle>_g \<longrightarrow> \<diamond>\<box>P
[PROOF STEP]
from h1
[PROOF STATE]
proof (chain)
picking this:
|~ \<langle>N \<and> B\<rangle>_f \<longrightarrow> \<langle>M\<rangle>_g
[PROOF STEP]
have "|~ [N]_f \<longrightarrow> [\<not>M]_g \<longrightarrow> [N \<and> \<not>B]_f"
[PROOF STATE]
proof (prove)
using this:
|~ \<langle>N \<and> B\<rangle>_f \<longrightarrow> \<langle>M\<rangle>_g

goal (1 subgoal):
 1. |~ _actrans N f \<longrightarrow> _actrans (\<not> M) g \<longrightarrow> _actrans (N \<and> \<not> B) f
[PROOF STEP]
by (auto simp: actrans_def angle_actrans_def)
[PROOF STATE]
proof (state)
this:
|~ _actrans N f \<longrightarrow> _actrans (\<not> M) g \<longrightarrow> _actrans (N \<and> \<not> B) f

goal (1 subgoal):
 1. \<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<not> \<box>\<diamond>\<langle>M\<rangle>_g \<longrightarrow> \<diamond>\<box>P
[PROOF STEP]
hence "\<turnstile> \<box>[[N]_f]_f \<longrightarrow> \<box>[[\<not>M]_g \<longrightarrow> [N \<and> \<not>B]_f]_f"
[PROOF STATE]
proof (prove)
using this:
|~ _actrans N f \<longrightarrow> _actrans (\<not> M) g \<longrightarrow> _actrans (N \<and> \<not> B) f

goal (1 subgoal):
 1. \<turnstile> \<box>[_actrans N f]_f \<longrightarrow> \<box>[_actrans (\<not> M) g \<longrightarrow> _actrans (N \<and> \<not> B) f]_f
[PROOF STEP]
by (rule M2)
[PROOF STATE]
proof (state)
this:
\<turnstile> \<box>[_actrans N f]_f \<longrightarrow> \<box>[_actrans (\<not> M) g \<longrightarrow> _actrans (N \<and> \<not> B) f]_f

goal (1 subgoal):
 1. \<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<not> \<box>\<diamond>\<langle>M\<rangle>_g \<longrightarrow> \<diamond>\<box>P
[PROOF STEP]
from lift_imp_trans[OF this ax4]
[PROOF STATE]
proof (chain)
picking this:
\<turnstile> \<box>[_actrans N f]_f \<longrightarrow> \<box>[_actrans (\<not> M) g]_f \<longrightarrow> \<box>[_actrans (N \<and> \<not> B) f]_f
[PROOF STEP]
have "\<turnstile> \<box>[N]_f \<and> \<box>[\<not>M]_g \<longrightarrow> \<box>[N \<and> \<not>B]_f"
[PROOF STATE]
proof (prove)
using this:
\<turnstile> \<box>[_actrans N f]_f \<longrightarrow> \<box>[_actrans (\<not> M) g]_f \<longrightarrow> \<box>[_actrans (N \<and> \<not> B) f]_f

goal (1 subgoal):
 1. \<turnstile> \<box>[N]_f \<and> \<box>[\<not> M]_g \<longrightarrow> \<box>[N \<and> \<not> B]_f
[PROOF STEP]
by (force intro: T4[unlift_rule])
[PROOF STATE]
proof (state)
this:
\<turnstile> \<box>[N]_f \<and> \<box>[\<not> M]_g \<longrightarrow> \<box>[N \<and> \<not> B]_f

goal (1 subgoal):
 1. \<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<not> \<box>\<diamond>\<langle>M\<rangle>_g \<longrightarrow> \<diamond>\<box>P
[PROOF STEP]
with h4
[PROOF STATE]
proof (chain)
picking this:
\<turnstile> \<box>[N \<and> \<not> B]_f \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<longrightarrow> \<diamond>\<box>P
\<turnstile> \<box>[N]_f \<and> \<box>[\<not> M]_g \<longrightarrow> \<box>[N \<and> \<not> B]_f
[PROOF STEP]
have "\<turnstile> (\<box>[N]_f \<and> SF(A)_f \<and> \<box>F) \<and> (\<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<box>[\<not>M]_g) \<longrightarrow> \<diamond>\<box>P"
[PROOF STATE]
proof (prove)
using this:
\<turnstile> \<box>[N \<and> \<not> B]_f \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<longrightarrow> \<diamond>\<box>P
\<turnstile> \<box>[N]_f \<and> \<box>[\<not> M]_g \<longrightarrow> \<box>[N \<and> \<not> B]_f

goal (1 subgoal):
 1. \<turnstile> (\<box>[N]_f \<and> SF(A)_f \<and> \<box>F) \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<box>[\<not> M]_g \<longrightarrow> \<diamond>\<box>P
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<turnstile> (\<box>[N]_f \<and> SF(A)_f \<and> \<box>F) \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<box>[\<not> M]_g \<longrightarrow> \<diamond>\<box>P

goal (1 subgoal):
 1. \<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<not> \<box>\<diamond>\<langle>M\<rangle>_g \<longrightarrow> \<diamond>\<box>P
[PROOF STEP]
from STL4_eve[OF this]
[PROOF STATE]
proof (chain)
picking this:
\<turnstile> \<diamond>((\<box>[N]_f \<and> SF(A)_f \<and> \<box>F) \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<box>[\<not> M]_g) \<longrightarrow> \<diamond>\<diamond>\<box>P
[PROOF STEP]
have "\<turnstile> \<diamond>((\<box>[N]_f \<and> SF(A)_f \<and> \<box>F) \<and> (\<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<box>[\<not>M]_g)) \<longrightarrow> \<diamond>\<box>P"
[PROOF STATE]
proof (prove)
using this:
\<turnstile> \<diamond>((\<box>[N]_f \<and> SF(A)_f \<and> \<box>F) \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<box>[\<not> M]_g) \<longrightarrow> \<diamond>\<diamond>\<box>P

goal (1 subgoal):
 1. \<turnstile> \<diamond>((\<box>[N]_f \<and> SF(A)_f \<and> \<box>F) \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<box>[\<not> M]_g) \<longrightarrow> \<diamond>\<box>P
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<turnstile> \<diamond>((\<box>[N]_f \<and> SF(A)_f \<and> \<box>F) \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<box>[\<not> M]_g) \<longrightarrow> \<diamond>\<box>P

goal (1 subgoal):
 1. \<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<not> \<box>\<diamond>\<langle>M\<rangle>_g \<longrightarrow> \<diamond>\<box>P
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<not> \<box>\<diamond>\<langle>M\<rangle>_g \<longrightarrow> \<diamond>((\<box>[N]_f \<and> SF(A)_f \<and> \<box>F) \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<box>[\<not> M]_g)
\<turnstile> \<diamond>((\<box>[N]_f \<and> SF(A)_f \<and> \<box>F) \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<box>[\<not> M]_g) \<longrightarrow> \<diamond>\<box>P
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<not> \<box>\<diamond>\<langle>M\<rangle>_g \<longrightarrow> \<diamond>((\<box>[N]_f \<and> SF(A)_f \<and> \<box>F) \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<box>[\<not> M]_g)
\<turnstile> \<diamond>((\<box>[N]_f \<and> SF(A)_f \<and> \<box>F) \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<box>[\<not> M]_g) \<longrightarrow> \<diamond>\<box>P

goal (1 subgoal):
 1. \<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<not> \<box>\<diamond>\<langle>M\<rangle>_g \<longrightarrow> \<diamond>\<box>P
[PROOF STEP]
by (rule lift_imp_trans)
[PROOF STATE]
proof (state)
this:
\<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<not> \<box>\<diamond>\<langle>M\<rangle>_g \<longrightarrow> \<diamond>\<box>P

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<not> \<box>\<diamond>\<langle>M\<rangle>_g \<longrightarrow> \<diamond>\<box>P

goal (1 subgoal):
 1. \<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<not> \<box>\<diamond>\<langle>M\<rangle>_g \<longrightarrow> \<box>\<diamond>\<langle>M\<rangle>_g
[PROOF STEP]
have 2: "\<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<diamond>\<box>P \<longrightarrow> \<box>\<diamond>\<langle>M\<rangle>_g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<diamond>\<box>P \<longrightarrow> \<box>\<diamond>\<langle>M\<rangle>_g
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<diamond>\<box>P \<longrightarrow> \<box>\<diamond>\<langle>M\<rangle>_g
[PROOF STEP]
have "\<turnstile> \<box>\<diamond>(P \<and> Enabled \<langle>M\<rangle>_g) \<and> SF(A)_f \<longrightarrow> \<box>\<diamond>\<langle>A\<rangle>_f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile> \<box>\<diamond>(P \<and> Enabled \<langle>M\<rangle>_g) \<and> SF(A)_f \<longrightarrow> \<box>\<diamond>\<langle>A\<rangle>_f
[PROOF STEP]
using h3[THEN STL4_eve, THEN STL4]
[PROOF STATE]
proof (prove)
using this:
\<turnstile> \<box>\<diamond>(P \<and> Enabled \<langle>M\<rangle>_g) \<longrightarrow> \<box>\<diamond>Enabled \<langle>A\<rangle>_f

goal (1 subgoal):
 1. \<turnstile> \<box>\<diamond>(P \<and> Enabled \<langle>M\<rangle>_g) \<and> SF(A)_f \<longrightarrow> \<box>\<diamond>\<langle>A\<rangle>_f
[PROOF STEP]
by (auto simp: StrongF_def)
[PROOF STATE]
proof (state)
this:
\<turnstile> \<box>\<diamond>(P \<and> Enabled \<langle>M\<rangle>_g) \<and> SF(A)_f \<longrightarrow> \<box>\<diamond>\<langle>A\<rangle>_f

goal (1 subgoal):
 1. \<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<diamond>\<box>P \<longrightarrow> \<box>\<diamond>\<langle>M\<rangle>_g
[PROOF STEP]
with E28
[PROOF STATE]
proof (chain)
picking this:
\<turnstile> \<diamond>\<box>?F \<and> \<box>\<diamond>?G \<longrightarrow> \<box>\<diamond>(?F \<and> ?G)
\<turnstile> \<box>\<diamond>(P \<and> Enabled \<langle>M\<rangle>_g) \<and> SF(A)_f \<longrightarrow> \<box>\<diamond>\<langle>A\<rangle>_f
[PROOF STEP]
have A: "\<turnstile> \<diamond>\<box>P \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> SF(A)_f \<longrightarrow> \<box>\<diamond>\<langle>A\<rangle>_f"
[PROOF STATE]
proof (prove)
using this:
\<turnstile> \<diamond>\<box>?F \<and> \<box>\<diamond>?G \<longrightarrow> \<box>\<diamond>(?F \<and> ?G)
\<turnstile> \<box>\<diamond>(P \<and> Enabled \<langle>M\<rangle>_g) \<and> SF(A)_f \<longrightarrow> \<box>\<diamond>\<langle>A\<rangle>_f

goal (1 subgoal):
 1. \<turnstile> \<diamond>\<box>P \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> SF(A)_f \<longrightarrow> \<box>\<diamond>\<langle>A\<rangle>_f
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<turnstile> \<diamond>\<box>P \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> SF(A)_f \<longrightarrow> \<box>\<diamond>\<langle>A\<rangle>_f

goal (1 subgoal):
 1. \<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<diamond>\<box>P \<longrightarrow> \<box>\<diamond>\<langle>M\<rangle>_g
[PROOF STEP]
have B: "\<turnstile> \<box>[N]_f \<and> \<diamond>\<box>P \<and>  \<box>\<diamond>\<langle>A\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>M\<rangle>_g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile> \<box>[N]_f \<and> \<diamond>\<box>P \<and> \<box>\<diamond>\<langle>A\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>M\<rangle>_g
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<turnstile> \<box>[N]_f \<and> \<diamond>\<box>P \<and> \<box>\<diamond>\<langle>A\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>M\<rangle>_g
[PROOF STEP]
from M1[of P f]
[PROOF STATE]
proof (chain)
picking this:
\<turnstile> \<box>P \<longrightarrow> \<box>[P \<and> \<circle>P]_f
[PROOF STEP]
have "\<turnstile> \<box>P \<and> \<box>\<diamond>\<langle>N \<and> A\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>(P \<and> \<circle>P) \<and> (N \<and> A)\<rangle>_f"
[PROOF STATE]
proof (prove)
using this:
\<turnstile> \<box>P \<longrightarrow> \<box>[P \<and> \<circle>P]_f

goal (1 subgoal):
 1. \<turnstile> \<box>P \<and> \<box>\<diamond>\<langle>N \<and> A\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>(P \<and> \<circle>P) \<and> N \<and> A\<rangle>_f
[PROOF STEP]
by (force intro: AA29[unlift_rule])
[PROOF STATE]
proof (state)
this:
\<turnstile> \<box>P \<and> \<box>\<diamond>\<langle>N \<and> A\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>(P \<and> \<circle>P) \<and> N \<and> A\<rangle>_f

goal (1 subgoal):
 1. \<turnstile> \<box>[N]_f \<and> \<diamond>\<box>P \<and> \<box>\<diamond>\<langle>A\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>M\<rangle>_g
[PROOF STEP]
hence "\<turnstile> \<diamond>\<box>(\<box>P \<and> \<box>\<diamond>\<langle>N \<and> A\<rangle>_f) \<longrightarrow> \<diamond>\<box>\<box>\<diamond>\<langle>(P \<and> \<circle>P) \<and> (N \<and> A)\<rangle>_f"
[PROOF STATE]
proof (prove)
using this:
\<turnstile> \<box>P \<and> \<box>\<diamond>\<langle>N \<and> A\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>(P \<and> \<circle>P) \<and> N \<and> A\<rangle>_f

goal (1 subgoal):
 1. \<turnstile> \<diamond>\<box>(\<box>P \<and> \<box>\<diamond>\<langle>N \<and> A\<rangle>_f) \<longrightarrow> \<diamond>\<box>\<box>\<diamond>\<langle>(P \<and> \<circle>P) \<and> N \<and> A\<rangle>_f
[PROOF STEP]
by (rule STL4_eve[OF STL4])
[PROOF STATE]
proof (state)
this:
\<turnstile> \<diamond>\<box>(\<box>P \<and> \<box>\<diamond>\<langle>N \<and> A\<rangle>_f) \<longrightarrow> \<diamond>\<box>\<box>\<diamond>\<langle>(P \<and> \<circle>P) \<and> N \<and> A\<rangle>_f

goal (1 subgoal):
 1. \<turnstile> \<box>[N]_f \<and> \<diamond>\<box>P \<and> \<box>\<diamond>\<langle>A\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>M\<rangle>_g
[PROOF STEP]
hence "\<turnstile> \<diamond>\<box>P \<and> \<box>\<diamond>\<langle>N \<and> A\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>(P \<and> \<circle>P) \<and> (N \<and> A)\<rangle>_f"
[PROOF STATE]
proof (prove)
using this:
\<turnstile> \<diamond>\<box>(\<box>P \<and> \<box>\<diamond>\<langle>N \<and> A\<rangle>_f) \<longrightarrow> \<diamond>\<box>\<box>\<diamond>\<langle>(P \<and> \<circle>P) \<and> N \<and> A\<rangle>_f

goal (1 subgoal):
 1. \<turnstile> \<diamond>\<box>P \<and> \<box>\<diamond>\<langle>N \<and> A\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>(P \<and> \<circle>P) \<and> N \<and> A\<rangle>_f
[PROOF STEP]
by (simp add: STL6[int_rewrite])
[PROOF STATE]
proof (state)
this:
\<turnstile> \<diamond>\<box>P \<and> \<box>\<diamond>\<langle>N \<and> A\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>(P \<and> \<circle>P) \<and> N \<and> A\<rangle>_f

goal (1 subgoal):
 1. \<turnstile> \<box>[N]_f \<and> \<diamond>\<box>P \<and> \<box>\<diamond>\<langle>A\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>M\<rangle>_g
[PROOF STEP]
with AA29[of N f A]
[PROOF STATE]
proof (chain)
picking this:
\<turnstile> \<box>[N]_f \<and> \<box>\<diamond>\<langle>A\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>N \<and> A\<rangle>_f
\<turnstile> \<diamond>\<box>P \<and> \<box>\<diamond>\<langle>N \<and> A\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>(P \<and> \<circle>P) \<and> N \<and> A\<rangle>_f
[PROOF STEP]
have B1: "\<turnstile> \<box>[N]_f \<and> \<diamond>\<box>P \<and>  \<box>\<diamond>\<langle>A\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>(P \<and> \<circle>P) \<and> (N \<and> A)\<rangle>_f"
[PROOF STATE]
proof (prove)
using this:
\<turnstile> \<box>[N]_f \<and> \<box>\<diamond>\<langle>A\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>N \<and> A\<rangle>_f
\<turnstile> \<diamond>\<box>P \<and> \<box>\<diamond>\<langle>N \<and> A\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>(P \<and> \<circle>P) \<and> N \<and> A\<rangle>_f

goal (1 subgoal):
 1. \<turnstile> \<box>[N]_f \<and> \<diamond>\<box>P \<and> \<box>\<diamond>\<langle>A\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>(P \<and> \<circle>P) \<and> N \<and> A\<rangle>_f
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<turnstile> \<box>[N]_f \<and> \<diamond>\<box>P \<and> \<box>\<diamond>\<langle>A\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>(P \<and> \<circle>P) \<and> N \<and> A\<rangle>_f

goal (1 subgoal):
 1. \<turnstile> \<box>[N]_f \<and> \<diamond>\<box>P \<and> \<box>\<diamond>\<langle>A\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>M\<rangle>_g
[PROOF STEP]
from h2
[PROOF STATE]
proof (chain)
picking this:
|~ P \<and> \<circle>P \<and> \<langle>N \<and> A\<rangle>_f \<longrightarrow> B
[PROOF STEP]
have "|~ \<langle>(P \<and> \<circle>P) \<and> (N \<and> A)\<rangle>_f \<longrightarrow> \<langle>N \<and> B\<rangle>_f"
[PROOF STATE]
proof (prove)
using this:
|~ P \<and> \<circle>P \<and> \<langle>N \<and> A\<rangle>_f \<longrightarrow> B

goal (1 subgoal):
 1. |~ \<langle>(P \<and> \<circle>P) \<and> N \<and> A\<rangle>_f \<longrightarrow> \<langle>N \<and> B\<rangle>_f
[PROOF STEP]
by (auto simp: angle_actrans_sem[unlifted])
[PROOF STATE]
proof (state)
this:
|~ \<langle>(P \<and> \<circle>P) \<and> N \<and> A\<rangle>_f \<longrightarrow> \<langle>N \<and> B\<rangle>_f

goal (1 subgoal):
 1. \<turnstile> \<box>[N]_f \<and> \<diamond>\<box>P \<and> \<box>\<diamond>\<langle>A\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>M\<rangle>_g
[PROOF STEP]
from B1 this[THEN AA25, THEN STL4]
[PROOF STATE]
proof (chain)
picking this:
\<turnstile> \<box>[N]_f \<and> \<diamond>\<box>P \<and> \<box>\<diamond>\<langle>A\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>(P \<and> \<circle>P) \<and> N \<and> A\<rangle>_f
\<turnstile> \<box>\<diamond>\<langle>(P \<and> \<circle>P) \<and> N \<and> A\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>N \<and> B\<rangle>_f
[PROOF STEP]
have "\<turnstile> \<box>[N]_f \<and> \<diamond>\<box>P \<and>  \<box>\<diamond>\<langle>A\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>N \<and> B\<rangle>_f"
[PROOF STATE]
proof (prove)
using this:
\<turnstile> \<box>[N]_f \<and> \<diamond>\<box>P \<and> \<box>\<diamond>\<langle>A\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>(P \<and> \<circle>P) \<and> N \<and> A\<rangle>_f
\<turnstile> \<box>\<diamond>\<langle>(P \<and> \<circle>P) \<and> N \<and> A\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>N \<and> B\<rangle>_f

goal (1 subgoal):
 1. \<turnstile> \<box>[N]_f \<and> \<diamond>\<box>P \<and> \<box>\<diamond>\<langle>A\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>N \<and> B\<rangle>_f
[PROOF STEP]
by (rule lift_imp_trans)
[PROOF STATE]
proof (state)
this:
\<turnstile> \<box>[N]_f \<and> \<diamond>\<box>P \<and> \<box>\<diamond>\<langle>A\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>N \<and> B\<rangle>_f

goal (1 subgoal):
 1. \<turnstile> \<box>[N]_f \<and> \<diamond>\<box>P \<and> \<box>\<diamond>\<langle>A\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>M\<rangle>_g
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<turnstile> \<box>[N]_f \<and> \<diamond>\<box>P \<and> \<box>\<diamond>\<langle>A\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>N \<and> B\<rangle>_f

goal (1 subgoal):
 1. \<turnstile> \<box>[N]_f \<and> \<diamond>\<box>P \<and> \<box>\<diamond>\<langle>A\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>M\<rangle>_g
[PROOF STEP]
have "\<turnstile> \<box>\<diamond>\<langle>N \<and> B\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>M\<rangle>_g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile> \<box>\<diamond>\<langle>N \<and> B\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>M\<rangle>_g
[PROOF STEP]
by (rule h1[THEN AA25, THEN STL4])
[PROOF STATE]
proof (state)
this:
\<turnstile> \<box>\<diamond>\<langle>N \<and> B\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>M\<rangle>_g

goal (1 subgoal):
 1. \<turnstile> \<box>[N]_f \<and> \<diamond>\<box>P \<and> \<box>\<diamond>\<langle>A\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>M\<rangle>_g
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<turnstile> \<box>[N]_f \<and> \<diamond>\<box>P \<and> \<box>\<diamond>\<langle>A\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>N \<and> B\<rangle>_f
\<turnstile> \<box>\<diamond>\<langle>N \<and> B\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>M\<rangle>_g
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<turnstile> \<box>[N]_f \<and> \<diamond>\<box>P \<and> \<box>\<diamond>\<langle>A\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>N \<and> B\<rangle>_f
\<turnstile> \<box>\<diamond>\<langle>N \<and> B\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>M\<rangle>_g

goal (1 subgoal):
 1. \<turnstile> \<box>[N]_f \<and> \<diamond>\<box>P \<and> \<box>\<diamond>\<langle>A\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>M\<rangle>_g
[PROOF STEP]
by (rule lift_imp_trans)
[PROOF STATE]
proof (state)
this:
\<turnstile> \<box>[N]_f \<and> \<diamond>\<box>P \<and> \<box>\<diamond>\<langle>A\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>M\<rangle>_g

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<turnstile> \<box>[N]_f \<and> \<diamond>\<box>P \<and> \<box>\<diamond>\<langle>A\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>M\<rangle>_g

goal (1 subgoal):
 1. \<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<diamond>\<box>P \<longrightarrow> \<box>\<diamond>\<langle>M\<rangle>_g
[PROOF STEP]
from A B
[PROOF STATE]
proof (chain)
picking this:
\<turnstile> \<diamond>\<box>P \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> SF(A)_f \<longrightarrow> \<box>\<diamond>\<langle>A\<rangle>_f
\<turnstile> \<box>[N]_f \<and> \<diamond>\<box>P \<and> \<box>\<diamond>\<langle>A\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>M\<rangle>_g
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<turnstile> \<diamond>\<box>P \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> SF(A)_f \<longrightarrow> \<box>\<diamond>\<langle>A\<rangle>_f
\<turnstile> \<box>[N]_f \<and> \<diamond>\<box>P \<and> \<box>\<diamond>\<langle>A\<rangle>_f \<longrightarrow> \<box>\<diamond>\<langle>M\<rangle>_g

goal (1 subgoal):
 1. \<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<diamond>\<box>P \<longrightarrow> \<box>\<diamond>\<langle>M\<rangle>_g
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<diamond>\<box>P \<longrightarrow> \<box>\<diamond>\<langle>M\<rangle>_g

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<diamond>\<box>P \<longrightarrow> \<box>\<diamond>\<langle>M\<rangle>_g

goal (1 subgoal):
 1. \<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<not> \<box>\<diamond>\<langle>M\<rangle>_g \<longrightarrow> \<box>\<diamond>\<langle>M\<rangle>_g
[PROOF STEP]
from 1 2
[PROOF STATE]
proof (chain)
picking this:
\<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<not> \<box>\<diamond>\<langle>M\<rangle>_g \<longrightarrow> \<diamond>\<box>P
\<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<diamond>\<box>P \<longrightarrow> \<box>\<diamond>\<langle>M\<rangle>_g
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<not> \<box>\<diamond>\<langle>M\<rangle>_g \<longrightarrow> \<diamond>\<box>P
\<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<diamond>\<box>P \<longrightarrow> \<box>\<diamond>\<langle>M\<rangle>_g

goal (1 subgoal):
 1. \<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<not> \<box>\<diamond>\<langle>M\<rangle>_g \<longrightarrow> \<box>\<diamond>\<langle>M\<rangle>_g
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<not> \<box>\<diamond>\<langle>M\<rangle>_g \<longrightarrow> \<box>\<diamond>\<langle>M\<rangle>_g

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<not> \<box>\<diamond>\<langle>M\<rangle>_g \<longrightarrow> \<box>\<diamond>\<langle>M\<rangle>_g

goal (1 subgoal):
 1. \<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<longrightarrow> SF(M)_g
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled \<langle>M\<rangle>_g \<and> \<not> \<box>\<diamond>\<langle>M\<rangle>_g \<longrightarrow> \<box>\<diamond>\<langle>M\<rangle>_g

goal (1 subgoal):
 1. \<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<longrightarrow> SF(M)_g
[PROOF STEP]
by (auto simp: StrongF_def)
[PROOF STATE]
proof (state)
this:
\<turnstile> \<box>[N]_f \<and> SF(A)_f \<and> \<box>F \<longrightarrow> SF(M)_g

goal:
No subgoals!
[PROOF STEP]
qed