[STATEMENT]
theorem WF1_general:
  assumes h1: "|~ P \<and> N \<longrightarrow> \<circle>P \<or> \<circle>Q"
      and h2: "|~ P \<and> N \<and> \<langle>A\<rangle>_v \<longrightarrow> \<circle>Q"
      and h3: "\<turnstile> P \<and> N \<longrightarrow> Enabled \<langle>A\<rangle>_v"
      and h4: "|~ P \<and> Unchanged w \<longrightarrow> \<circle>P"
  shows "\<turnstile> \<box>N \<and> WF(A)_v \<longrightarrow> (P \<leadsto> Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile> \<box>N \<and> WF(A)_v \<longrightarrow> P \<leadsto> Q
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<turnstile> \<box>N \<and> WF(A)_v \<longrightarrow> P \<leadsto> Q
[PROOF STEP]
have "\<turnstile> \<box>(\<box>N \<and> WF(A)_v) \<longrightarrow> \<box>(\<box>P \<longrightarrow> \<diamond>\<langle>A\<rangle>_v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile> \<box>(\<box>N \<and> WF(A)_v) \<longrightarrow> \<box>(\<box>P \<longrightarrow> \<diamond>\<langle>A\<rangle>_v)
[PROOF STEP]
proof (rule STL4)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<turnstile> \<box>N \<and> WF(A)_v \<longrightarrow> \<box>P \<longrightarrow> \<diamond>\<langle>A\<rangle>_v
[PROOF STEP]
have "\<turnstile> \<box>(P \<and> N) \<longrightarrow> \<diamond>\<box>Enabled \<langle>A\<rangle>_v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile> \<box>(P \<and> N) \<longrightarrow> \<diamond>\<box>Enabled \<langle>A\<rangle>_v
[PROOF STEP]
by (rule lift_imp_trans[OF h3[THEN STL4] E3])
[PROOF STATE]
proof (state)
this:
\<turnstile> \<box>(P \<and> N) \<longrightarrow> \<diamond>\<box>Enabled \<langle>A\<rangle>_v

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

goal (1 subgoal):
 1. \<turnstile> \<box>P \<and> \<box>N \<and> WF(A)_v \<longrightarrow> \<box>\<diamond>\<langle>A\<rangle>_v
[PROOF STEP]
by (auto simp: WeakF_def STL5[int_rewrite])
[PROOF STATE]
proof (state)
this:
\<turnstile> \<box>P \<and> \<box>N \<and> WF(A)_v \<longrightarrow> \<box>\<diamond>\<langle>A\<rangle>_v

goal (1 subgoal):
 1. \<turnstile> \<box>N \<and> WF(A)_v \<longrightarrow> \<box>P \<longrightarrow> \<diamond>\<langle>A\<rangle>_v
[PROOF STEP]
with ax1[of "TEMP \<diamond>\<langle>A\<rangle>_v"]
[PROOF STATE]
proof (chain)
picking this:
\<turnstile> \<box>\<diamond>\<langle>A\<rangle>_v \<longrightarrow> \<diamond>\<langle>A\<rangle>_v
\<turnstile> \<box>P \<and> \<box>N \<and> WF(A)_v \<longrightarrow> \<box>\<diamond>\<langle>A\<rangle>_v
[PROOF STEP]
show "\<turnstile> \<box>N \<and> WF(A)_v \<longrightarrow> \<box>P \<longrightarrow> \<diamond>\<langle>A\<rangle>_v"
[PROOF STATE]
proof (prove)
using this:
\<turnstile> \<box>\<diamond>\<langle>A\<rangle>_v \<longrightarrow> \<diamond>\<langle>A\<rangle>_v
\<turnstile> \<box>P \<and> \<box>N \<and> WF(A)_v \<longrightarrow> \<box>\<diamond>\<langle>A\<rangle>_v

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

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

goal (1 subgoal):
 1. \<turnstile> \<box>N \<and> WF(A)_v \<longrightarrow> P \<leadsto> Q
[PROOF STEP]
hence "\<turnstile> \<box>N \<and> WF(A)_v \<longrightarrow> \<box>(\<box>P \<longrightarrow> \<diamond>\<langle>A\<rangle>_v)"
[PROOF STATE]
proof (prove)
using this:
\<turnstile> \<box>(\<box>N \<and> WF(A)_v) \<longrightarrow> \<box>(\<box>P \<longrightarrow> \<diamond>\<langle>A\<rangle>_v)

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

goal (1 subgoal):
 1. \<turnstile> \<box>N \<and> WF(A)_v \<longrightarrow> P \<leadsto> Q
[PROOF STEP]
with AA22[OF h1 h2 h4]
[PROOF STATE]
proof (chain)
picking this:
\<turnstile> \<box>N \<and> \<box>(\<box>P \<longrightarrow> \<diamond>\<langle>A\<rangle>_v) \<longrightarrow> P \<leadsto> Q
\<turnstile> \<box>N \<and> WF(A)_v \<longrightarrow> \<box>(\<box>P \<longrightarrow> \<diamond>\<langle>A\<rangle>_v)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<turnstile> \<box>N \<and> \<box>(\<box>P \<longrightarrow> \<diamond>\<langle>A\<rangle>_v) \<longrightarrow> P \<leadsto> Q
\<turnstile> \<box>N \<and> WF(A)_v \<longrightarrow> \<box>(\<box>P \<longrightarrow> \<diamond>\<langle>A\<rangle>_v)

goal (1 subgoal):
 1. \<turnstile> \<box>N \<and> WF(A)_v \<longrightarrow> P \<leadsto> Q
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<turnstile> \<box>N \<and> WF(A)_v \<longrightarrow> P \<leadsto> Q

goal:
No subgoals!
[PROOF STEP]
qed