[STATEMENT]
lemma unfold:
  "(\<box> P) \<sigma> = (P \<^bold>\<and> \<circle>\<box>P) \<sigma>"
  "(\<diamond> P) \<sigma> = (P \<^bold>\<or> \<circle>\<diamond>P) \<sigma>"
  "(P \<W> Q) \<sigma> = (Q \<^bold>\<or> (P \<^bold>\<and> \<circle>(P \<W> Q))) \<sigma>"
  "(P \<U> Q) \<sigma> = (Q \<^bold>\<or> (P \<^bold>\<and> \<circle>(P \<U> Q))) \<sigma>"
  "(P \<R> Q) \<sigma> = (Q \<^bold>\<and> (P \<^bold>\<or> \<circle>(P \<R> Q))) \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<box>P) \<sigma> = (P \<sigma> \<and> (\<circle>\<box>P) \<sigma>) &&& (\<diamond>P) \<sigma> = (P \<sigma> \<or> (\<circle>\<diamond>P) \<sigma>)) &&& (P \<W> Q) \<sigma> = (Q \<sigma> \<or> P \<sigma> \<and> (\<circle>(P \<W> Q)) \<sigma>) &&& (P \<U> Q) \<sigma> = (Q \<sigma> \<or> P \<sigma> \<and> (\<circle>(P \<U> Q)) \<sigma>) &&& (P \<R> Q) \<sigma> = (Q \<sigma> \<and> (P \<sigma> \<or> (\<circle>(P \<R> Q)) \<sigma>))
[PROOF STEP]
unfolding defs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<forall>i. P (\<sigma> |\<^sub>s i)) = (P \<sigma> \<and> (\<forall>i. P (\<sigma> |\<^sub>s 1 |\<^sub>s i))) &&& (\<exists>i. P (\<sigma> |\<^sub>s i) \<and> (\<forall>k<i. True)) = (P \<sigma> \<or> (\<exists>i. P (\<sigma> |\<^sub>s 1 |\<^sub>s i) \<and> (\<forall>k<i. True)))) &&& ((\<exists>i. Q (\<sigma> |\<^sub>s i) \<and> (\<forall>k<i. P (\<sigma> |\<^sub>s k))) \<or> (\<forall>i. P (\<sigma> |\<^sub>s i))) = (Q \<sigma> \<or> P \<sigma> \<and> ((\<exists>i. Q (\<sigma> |\<^sub>s 1 |\<^sub>s i) \<and> (\<forall>k<i. P (\<sigma> |\<^sub>s 1 |\<^sub>s k))) \<or> (\<forall>i. P (\<sigma> |\<^sub>s 1 |\<^sub>s i)))) &&& (\<exists>i. Q (\<sigma> |\<^sub>s i) \<and> (\<forall>k<i. P (\<sigma> |\<^sub>s k))) = (Q \<sigma> \<or> P \<sigma> \<and> (\<exists>i. Q (\<sigma> |\<^sub>s 1 |\<^sub>s i) \<and> (\<forall>k<i. P (\<sigma> |\<^sub>s 1 |\<^sub>s k)))) &&& (\<nexists>i. \<not> Q (\<sigma> |\<^sub>s i) \<and> (\<forall>k<i. \<not> P (\<sigma> |\<^sub>s k))) = (Q \<sigma> \<and> (P \<sigma> \<or> (\<nexists>i. \<not> Q (\<sigma> |\<^sub>s 1 |\<^sub>s i) \<and> (\<forall>k<i. \<not> P (\<sigma> |\<^sub>s 1 |\<^sub>s k)))))
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. (\<forall>i. P (\<sigma> |\<^sub>s i)) = (P \<sigma> \<and> (\<forall>i. P (\<sigma> |\<^sub>s 1 |\<^sub>s i)))
 2. (\<exists>i. P (\<sigma> |\<^sub>s i) \<and> (\<forall>k<i. True)) = (P \<sigma> \<or> (\<exists>i. P (\<sigma> |\<^sub>s 1 |\<^sub>s i) \<and> (\<forall>k<i. True)))
 3. ((\<exists>i. Q (\<sigma> |\<^sub>s i) \<and> (\<forall>k<i. P (\<sigma> |\<^sub>s k))) \<or> (\<forall>i. P (\<sigma> |\<^sub>s i))) = (Q \<sigma> \<or> P \<sigma> \<and> ((\<exists>i. Q (\<sigma> |\<^sub>s 1 |\<^sub>s i) \<and> (\<forall>k<i. P (\<sigma> |\<^sub>s 1 |\<^sub>s k))) \<or> (\<forall>i. P (\<sigma> |\<^sub>s 1 |\<^sub>s i))))
 4. (\<exists>i. Q (\<sigma> |\<^sub>s i) \<and> (\<forall>k<i. P (\<sigma> |\<^sub>s k))) = (Q \<sigma> \<or> P \<sigma> \<and> (\<exists>i. Q (\<sigma> |\<^sub>s 1 |\<^sub>s i) \<and> (\<forall>k<i. P (\<sigma> |\<^sub>s 1 |\<^sub>s k))))
 5. (\<nexists>i. \<not> Q (\<sigma> |\<^sub>s i) \<and> (\<forall>k<i. \<not> P (\<sigma> |\<^sub>s k))) = (Q \<sigma> \<and> (P \<sigma> \<or> (\<nexists>i. \<not> Q (\<sigma> |\<^sub>s 1 |\<^sub>s i) \<and> (\<forall>k<i. \<not> P (\<sigma> |\<^sub>s 1 |\<^sub>s k)))))
[PROOF STEP]
apply (metis (full_types) add.commute add_diff_inverse_nat less_one suffix_plus suffix_zero)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. (\<exists>i. P (\<sigma> |\<^sub>s i) \<and> (\<forall>k<i. True)) = (P \<sigma> \<or> (\<exists>i. P (\<sigma> |\<^sub>s 1 |\<^sub>s i) \<and> (\<forall>k<i. True)))
 2. ((\<exists>i. Q (\<sigma> |\<^sub>s i) \<and> (\<forall>k<i. P (\<sigma> |\<^sub>s k))) \<or> (\<forall>i. P (\<sigma> |\<^sub>s i))) = (Q \<sigma> \<or> P \<sigma> \<and> ((\<exists>i. Q (\<sigma> |\<^sub>s 1 |\<^sub>s i) \<and> (\<forall>k<i. P (\<sigma> |\<^sub>s 1 |\<^sub>s k))) \<or> (\<forall>i. P (\<sigma> |\<^sub>s 1 |\<^sub>s i))))
 3. (\<exists>i. Q (\<sigma> |\<^sub>s i) \<and> (\<forall>k<i. P (\<sigma> |\<^sub>s k))) = (Q \<sigma> \<or> P \<sigma> \<and> (\<exists>i. Q (\<sigma> |\<^sub>s 1 |\<^sub>s i) \<and> (\<forall>k<i. P (\<sigma> |\<^sub>s 1 |\<^sub>s k))))
 4. (\<nexists>i. \<not> Q (\<sigma> |\<^sub>s i) \<and> (\<forall>k<i. \<not> P (\<sigma> |\<^sub>s k))) = (Q \<sigma> \<and> (P \<sigma> \<or> (\<nexists>i. \<not> Q (\<sigma> |\<^sub>s 1 |\<^sub>s i) \<and> (\<forall>k<i. \<not> P (\<sigma> |\<^sub>s 1 |\<^sub>s k)))))
[PROOF STEP]
apply (metis (full_types) One_nat_def add.right_neutral add_Suc_right lessI less_Suc_eq_0_disj suffix_plus suffix_zero)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. ((\<exists>i. Q (\<sigma> |\<^sub>s i) \<and> (\<forall>k<i. P (\<sigma> |\<^sub>s k))) \<or> (\<forall>i. P (\<sigma> |\<^sub>s i))) = (Q \<sigma> \<or> P \<sigma> \<and> ((\<exists>i. Q (\<sigma> |\<^sub>s 1 |\<^sub>s i) \<and> (\<forall>k<i. P (\<sigma> |\<^sub>s 1 |\<^sub>s k))) \<or> (\<forall>i. P (\<sigma> |\<^sub>s 1 |\<^sub>s i))))
 2. (\<exists>i. Q (\<sigma> |\<^sub>s i) \<and> (\<forall>k<i. P (\<sigma> |\<^sub>s k))) = (Q \<sigma> \<or> P \<sigma> \<and> (\<exists>i. Q (\<sigma> |\<^sub>s 1 |\<^sub>s i) \<and> (\<forall>k<i. P (\<sigma> |\<^sub>s 1 |\<^sub>s k))))
 3. (\<nexists>i. \<not> Q (\<sigma> |\<^sub>s i) \<and> (\<forall>k<i. \<not> P (\<sigma> |\<^sub>s k))) = (Q \<sigma> \<and> (P \<sigma> \<or> (\<nexists>i. \<not> Q (\<sigma> |\<^sub>s 1 |\<^sub>s i) \<and> (\<forall>k<i. \<not> P (\<sigma> |\<^sub>s 1 |\<^sub>s k)))))
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (14 subgoals):
 1. \<And>i. \<lbrakk>Q (\<sigma> |\<^sub>s i); \<forall>k<i. P (\<sigma> |\<^sub>s k); \<not> Q \<sigma>\<rbrakk> \<Longrightarrow> P \<sigma>
 2. \<And>i ia. \<lbrakk>Q (\<sigma> |\<^sub>s i); \<forall>k<i. P (\<sigma> |\<^sub>s k); \<not> Q \<sigma>; \<forall>i. Q (\<sigma> |\<^sub>s Suc i) \<longrightarrow> (\<exists>k<i. \<not> P (\<sigma> |\<^sub>s Suc k))\<rbrakk> \<Longrightarrow> P (\<sigma> |\<^sub>s Suc ia)
 3. \<lbrakk>\<forall>i. P (\<sigma> |\<^sub>s i); \<not> Q \<sigma>\<rbrakk> \<Longrightarrow> P \<sigma>
 4. \<And>i. \<lbrakk>\<forall>i. Q (\<sigma> |\<^sub>s i) \<longrightarrow> (\<exists>k<i. \<not> P (\<sigma> |\<^sub>s k)); Q \<sigma>\<rbrakk> \<Longrightarrow> P (\<sigma> |\<^sub>s i)
 5. \<And>i ia. \<lbrakk>\<forall>i. Q (\<sigma> |\<^sub>s i) \<longrightarrow> (\<exists>k<i. \<not> P (\<sigma> |\<^sub>s k)); P \<sigma>; Q (\<sigma> |\<^sub>s Suc ia); \<forall>k<ia. P (\<sigma> |\<^sub>s Suc k)\<rbrakk> \<Longrightarrow> P (\<sigma> |\<^sub>s i)
 6. \<And>i. \<lbrakk>\<forall>i. Q (\<sigma> |\<^sub>s i) \<longrightarrow> (\<exists>k<i. \<not> P (\<sigma> |\<^sub>s k)); P \<sigma>; \<forall>i. P (\<sigma> |\<^sub>s Suc i)\<rbrakk> \<Longrightarrow> P (\<sigma> |\<^sub>s i)
 7. \<And>i. \<lbrakk>Q (\<sigma> |\<^sub>s i); \<forall>k<i. P (\<sigma> |\<^sub>s k); \<not> Q \<sigma>\<rbrakk> \<Longrightarrow> P \<sigma>
 8. \<And>i. \<lbrakk>Q (\<sigma> |\<^sub>s i); \<forall>k<i. P (\<sigma> |\<^sub>s k); \<not> Q \<sigma>\<rbrakk> \<Longrightarrow> \<exists>i. Q (\<sigma> |\<^sub>s Suc i) \<and> (\<forall>k<i. P (\<sigma> |\<^sub>s Suc k))
 9. Q \<sigma> \<Longrightarrow> \<exists>i. Q (\<sigma> |\<^sub>s i) \<and> (\<forall>k<i. P (\<sigma> |\<^sub>s k))
 10. \<And>i. \<lbrakk>P \<sigma>; Q (\<sigma> |\<^sub>s Suc i); \<forall>k<i. P (\<sigma> |\<^sub>s Suc k)\<rbrakk> \<Longrightarrow> \<exists>i. Q (\<sigma> |\<^sub>s i) \<and> (\<forall>k<i. P (\<sigma> |\<^sub>s k))
A total of 14 subgoals...
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal (13 subgoals):
 1. \<And>i ia. \<lbrakk>Q (\<sigma> |\<^sub>s i); \<forall>k<i. P (\<sigma> |\<^sub>s k); \<not> Q \<sigma>; \<forall>i. Q (\<sigma> |\<^sub>s Suc i) \<longrightarrow> (\<exists>k<i. \<not> P (\<sigma> |\<^sub>s Suc k))\<rbrakk> \<Longrightarrow> P (\<sigma> |\<^sub>s Suc ia)
 2. \<lbrakk>\<forall>i. P (\<sigma> |\<^sub>s i); \<not> Q \<sigma>\<rbrakk> \<Longrightarrow> P \<sigma>
 3. \<And>i. \<lbrakk>\<forall>i. Q (\<sigma> |\<^sub>s i) \<longrightarrow> (\<exists>k<i. \<not> P (\<sigma> |\<^sub>s k)); Q \<sigma>\<rbrakk> \<Longrightarrow> P (\<sigma> |\<^sub>s i)
 4. \<And>i ia. \<lbrakk>\<forall>i. Q (\<sigma> |\<^sub>s i) \<longrightarrow> (\<exists>k<i. \<not> P (\<sigma> |\<^sub>s k)); P \<sigma>; Q (\<sigma> |\<^sub>s Suc ia); \<forall>k<ia. P (\<sigma> |\<^sub>s Suc k)\<rbrakk> \<Longrightarrow> P (\<sigma> |\<^sub>s i)
 5. \<And>i. \<lbrakk>\<forall>i. Q (\<sigma> |\<^sub>s i) \<longrightarrow> (\<exists>k<i. \<not> P (\<sigma> |\<^sub>s k)); P \<sigma>; \<forall>i. P (\<sigma> |\<^sub>s Suc i)\<rbrakk> \<Longrightarrow> P (\<sigma> |\<^sub>s i)
 6. \<And>i. \<lbrakk>Q (\<sigma> |\<^sub>s i); \<forall>k<i. P (\<sigma> |\<^sub>s k); \<not> Q \<sigma>\<rbrakk> \<Longrightarrow> P \<sigma>
 7. \<And>i. \<lbrakk>Q (\<sigma> |\<^sub>s i); \<forall>k<i. P (\<sigma> |\<^sub>s k); \<not> Q \<sigma>\<rbrakk> \<Longrightarrow> \<exists>i. Q (\<sigma> |\<^sub>s Suc i) \<and> (\<forall>k<i. P (\<sigma> |\<^sub>s Suc k))
 8. Q \<sigma> \<Longrightarrow> \<exists>i. Q (\<sigma> |\<^sub>s i) \<and> (\<forall>k<i. P (\<sigma> |\<^sub>s k))
 9. \<And>i. \<lbrakk>P \<sigma>; Q (\<sigma> |\<^sub>s Suc i); \<forall>k<i. P (\<sigma> |\<^sub>s Suc k)\<rbrakk> \<Longrightarrow> \<exists>i. Q (\<sigma> |\<^sub>s i) \<and> (\<forall>k<i. P (\<sigma> |\<^sub>s k))
 10. \<forall>i. Q (\<sigma> |\<^sub>s i) \<or> (\<exists>k<i. P (\<sigma> |\<^sub>s k)) \<Longrightarrow> Q \<sigma>
A total of 13 subgoals...
[PROOF STEP]
apply (metis gr0_conv_Suc nat_neq_iff not_less_eq suffix_zero)
[PROOF STATE]
proof (prove)
goal (12 subgoals):
 1. \<lbrakk>\<forall>i. P (\<sigma> |\<^sub>s i); \<not> Q \<sigma>\<rbrakk> \<Longrightarrow> P \<sigma>
 2. \<And>i. \<lbrakk>\<forall>i. Q (\<sigma> |\<^sub>s i) \<longrightarrow> (\<exists>k<i. \<not> P (\<sigma> |\<^sub>s k)); Q \<sigma>\<rbrakk> \<Longrightarrow> P (\<sigma> |\<^sub>s i)
 3. \<And>i ia. \<lbrakk>\<forall>i. Q (\<sigma> |\<^sub>s i) \<longrightarrow> (\<exists>k<i. \<not> P (\<sigma> |\<^sub>s k)); P \<sigma>; Q (\<sigma> |\<^sub>s Suc ia); \<forall>k<ia. P (\<sigma> |\<^sub>s Suc k)\<rbrakk> \<Longrightarrow> P (\<sigma> |\<^sub>s i)
 4. \<And>i. \<lbrakk>\<forall>i. Q (\<sigma> |\<^sub>s i) \<longrightarrow> (\<exists>k<i. \<not> P (\<sigma> |\<^sub>s k)); P \<sigma>; \<forall>i. P (\<sigma> |\<^sub>s Suc i)\<rbrakk> \<Longrightarrow> P (\<sigma> |\<^sub>s i)
 5. \<And>i. \<lbrakk>Q (\<sigma> |\<^sub>s i); \<forall>k<i. P (\<sigma> |\<^sub>s k); \<not> Q \<sigma>\<rbrakk> \<Longrightarrow> P \<sigma>
 6. \<And>i. \<lbrakk>Q (\<sigma> |\<^sub>s i); \<forall>k<i. P (\<sigma> |\<^sub>s k); \<not> Q \<sigma>\<rbrakk> \<Longrightarrow> \<exists>i. Q (\<sigma> |\<^sub>s Suc i) \<and> (\<forall>k<i. P (\<sigma> |\<^sub>s Suc k))
 7. Q \<sigma> \<Longrightarrow> \<exists>i. Q (\<sigma> |\<^sub>s i) \<and> (\<forall>k<i. P (\<sigma> |\<^sub>s k))
 8. \<And>i. \<lbrakk>P \<sigma>; Q (\<sigma> |\<^sub>s Suc i); \<forall>k<i. P (\<sigma> |\<^sub>s Suc k)\<rbrakk> \<Longrightarrow> \<exists>i. Q (\<sigma> |\<^sub>s i) \<and> (\<forall>k<i. P (\<sigma> |\<^sub>s k))
 9. \<forall>i. Q (\<sigma> |\<^sub>s i) \<or> (\<exists>k<i. P (\<sigma> |\<^sub>s k)) \<Longrightarrow> Q \<sigma>
 10. \<And>i. \<lbrakk>\<forall>i. Q (\<sigma> |\<^sub>s i) \<or> (\<exists>k<i. P (\<sigma> |\<^sub>s k)); \<not> P \<sigma>; \<forall>k<i. \<not> P (\<sigma> |\<^sub>s Suc k)\<rbrakk> \<Longrightarrow> Q (\<sigma> |\<^sub>s Suc i)
A total of 12 subgoals...
[PROOF STEP]
apply (metis suffix_zero)
[PROOF STATE]
proof (prove)
goal (11 subgoals):
 1. \<And>i. \<lbrakk>\<forall>i. Q (\<sigma> |\<^sub>s i) \<longrightarrow> (\<exists>k<i. \<not> P (\<sigma> |\<^sub>s k)); Q \<sigma>\<rbrakk> \<Longrightarrow> P (\<sigma> |\<^sub>s i)
 2. \<And>i ia. \<lbrakk>\<forall>i. Q (\<sigma> |\<^sub>s i) \<longrightarrow> (\<exists>k<i. \<not> P (\<sigma> |\<^sub>s k)); P \<sigma>; Q (\<sigma> |\<^sub>s Suc ia); \<forall>k<ia. P (\<sigma> |\<^sub>s Suc k)\<rbrakk> \<Longrightarrow> P (\<sigma> |\<^sub>s i)
 3. \<And>i. \<lbrakk>\<forall>i. Q (\<sigma> |\<^sub>s i) \<longrightarrow> (\<exists>k<i. \<not> P (\<sigma> |\<^sub>s k)); P \<sigma>; \<forall>i. P (\<sigma> |\<^sub>s Suc i)\<rbrakk> \<Longrightarrow> P (\<sigma> |\<^sub>s i)
 4. \<And>i. \<lbrakk>Q (\<sigma> |\<^sub>s i); \<forall>k<i. P (\<sigma> |\<^sub>s k); \<not> Q \<sigma>\<rbrakk> \<Longrightarrow> P \<sigma>
 5. \<And>i. \<lbrakk>Q (\<sigma> |\<^sub>s i); \<forall>k<i. P (\<sigma> |\<^sub>s k); \<not> Q \<sigma>\<rbrakk> \<Longrightarrow> \<exists>i. Q (\<sigma> |\<^sub>s Suc i) \<and> (\<forall>k<i. P (\<sigma> |\<^sub>s Suc k))
 6. Q \<sigma> \<Longrightarrow> \<exists>i. Q (\<sigma> |\<^sub>s i) \<and> (\<forall>k<i. P (\<sigma> |\<^sub>s k))
 7. \<And>i. \<lbrakk>P \<sigma>; Q (\<sigma> |\<^sub>s Suc i); \<forall>k<i. P (\<sigma> |\<^sub>s Suc k)\<rbrakk> \<Longrightarrow> \<exists>i. Q (\<sigma> |\<^sub>s i) \<and> (\<forall>k<i. P (\<sigma> |\<^sub>s k))
 8. \<forall>i. Q (\<sigma> |\<^sub>s i) \<or> (\<exists>k<i. P (\<sigma> |\<^sub>s k)) \<Longrightarrow> Q \<sigma>
 9. \<And>i. \<lbrakk>\<forall>i. Q (\<sigma> |\<^sub>s i) \<or> (\<exists>k<i. P (\<sigma> |\<^sub>s k)); \<not> P \<sigma>; \<forall>k<i. \<not> P (\<sigma> |\<^sub>s Suc k)\<rbrakk> \<Longrightarrow> Q (\<sigma> |\<^sub>s Suc i)
 10. \<And>i. \<lbrakk>Q \<sigma>; \<forall>k<i. \<not> P (\<sigma> |\<^sub>s k); P \<sigma>\<rbrakk> \<Longrightarrow> Q (\<sigma> |\<^sub>s i)
A total of 11 subgoals...
[PROOF STEP]
apply force
[PROOF STATE]
proof (prove)
goal (10 subgoals):
 1. \<And>i ia. \<lbrakk>\<forall>i. Q (\<sigma> |\<^sub>s i) \<longrightarrow> (\<exists>k<i. \<not> P (\<sigma> |\<^sub>s k)); P \<sigma>; Q (\<sigma> |\<^sub>s Suc ia); \<forall>k<ia. P (\<sigma> |\<^sub>s Suc k)\<rbrakk> \<Longrightarrow> P (\<sigma> |\<^sub>s i)
 2. \<And>i. \<lbrakk>\<forall>i. Q (\<sigma> |\<^sub>s i) \<longrightarrow> (\<exists>k<i. \<not> P (\<sigma> |\<^sub>s k)); P \<sigma>; \<forall>i. P (\<sigma> |\<^sub>s Suc i)\<rbrakk> \<Longrightarrow> P (\<sigma> |\<^sub>s i)
 3. \<And>i. \<lbrakk>Q (\<sigma> |\<^sub>s i); \<forall>k<i. P (\<sigma> |\<^sub>s k); \<not> Q \<sigma>\<rbrakk> \<Longrightarrow> P \<sigma>
 4. \<And>i. \<lbrakk>Q (\<sigma> |\<^sub>s i); \<forall>k<i. P (\<sigma> |\<^sub>s k); \<not> Q \<sigma>\<rbrakk> \<Longrightarrow> \<exists>i. Q (\<sigma> |\<^sub>s Suc i) \<and> (\<forall>k<i. P (\<sigma> |\<^sub>s Suc k))
 5. Q \<sigma> \<Longrightarrow> \<exists>i. Q (\<sigma> |\<^sub>s i) \<and> (\<forall>k<i. P (\<sigma> |\<^sub>s k))
 6. \<And>i. \<lbrakk>P \<sigma>; Q (\<sigma> |\<^sub>s Suc i); \<forall>k<i. P (\<sigma> |\<^sub>s Suc k)\<rbrakk> \<Longrightarrow> \<exists>i. Q (\<sigma> |\<^sub>s i) \<and> (\<forall>k<i. P (\<sigma> |\<^sub>s k))
 7. \<forall>i. Q (\<sigma> |\<^sub>s i) \<or> (\<exists>k<i. P (\<sigma> |\<^sub>s k)) \<Longrightarrow> Q \<sigma>
 8. \<And>i. \<lbrakk>\<forall>i. Q (\<sigma> |\<^sub>s i) \<or> (\<exists>k<i. P (\<sigma> |\<^sub>s k)); \<not> P \<sigma>; \<forall>k<i. \<not> P (\<sigma> |\<^sub>s Suc k)\<rbrakk> \<Longrightarrow> Q (\<sigma> |\<^sub>s Suc i)
 9. \<And>i. \<lbrakk>Q \<sigma>; \<forall>k<i. \<not> P (\<sigma> |\<^sub>s k); P \<sigma>\<rbrakk> \<Longrightarrow> Q (\<sigma> |\<^sub>s i)
 10. \<And>i. \<lbrakk>Q \<sigma>; \<forall>k<i. \<not> P (\<sigma> |\<^sub>s k); \<forall>i. Q (\<sigma> |\<^sub>s Suc i) \<or> (\<exists>k<i. P (\<sigma> |\<^sub>s Suc k))\<rbrakk> \<Longrightarrow> Q (\<sigma> |\<^sub>s i)
[PROOF STEP]
using less_Suc_eq_0_disj
[PROOF STATE]
proof (prove)
using this:
(?m < Suc ?n) = (?m = 0 \<or> (\<exists>j. ?m = Suc j \<and> j < ?n))

goal (10 subgoals):
 1. \<And>i ia. \<lbrakk>\<forall>i. Q (\<sigma> |\<^sub>s i) \<longrightarrow> (\<exists>k<i. \<not> P (\<sigma> |\<^sub>s k)); P \<sigma>; Q (\<sigma> |\<^sub>s Suc ia); \<forall>k<ia. P (\<sigma> |\<^sub>s Suc k)\<rbrakk> \<Longrightarrow> P (\<sigma> |\<^sub>s i)
 2. \<And>i. \<lbrakk>\<forall>i. Q (\<sigma> |\<^sub>s i) \<longrightarrow> (\<exists>k<i. \<not> P (\<sigma> |\<^sub>s k)); P \<sigma>; \<forall>i. P (\<sigma> |\<^sub>s Suc i)\<rbrakk> \<Longrightarrow> P (\<sigma> |\<^sub>s i)
 3. \<And>i. \<lbrakk>Q (\<sigma> |\<^sub>s i); \<forall>k<i. P (\<sigma> |\<^sub>s k); \<not> Q \<sigma>\<rbrakk> \<Longrightarrow> P \<sigma>
 4. \<And>i. \<lbrakk>Q (\<sigma> |\<^sub>s i); \<forall>k<i. P (\<sigma> |\<^sub>s k); \<not> Q \<sigma>\<rbrakk> \<Longrightarrow> \<exists>i. Q (\<sigma> |\<^sub>s Suc i) \<and> (\<forall>k<i. P (\<sigma> |\<^sub>s Suc k))
 5. Q \<sigma> \<Longrightarrow> \<exists>i. Q (\<sigma> |\<^sub>s i) \<and> (\<forall>k<i. P (\<sigma> |\<^sub>s k))
 6. \<And>i. \<lbrakk>P \<sigma>; Q (\<sigma> |\<^sub>s Suc i); \<forall>k<i. P (\<sigma> |\<^sub>s Suc k)\<rbrakk> \<Longrightarrow> \<exists>i. Q (\<sigma> |\<^sub>s i) \<and> (\<forall>k<i. P (\<sigma> |\<^sub>s k))
 7. \<forall>i. Q (\<sigma> |\<^sub>s i) \<or> (\<exists>k<i. P (\<sigma> |\<^sub>s k)) \<Longrightarrow> Q \<sigma>
 8. \<And>i. \<lbrakk>\<forall>i. Q (\<sigma> |\<^sub>s i) \<or> (\<exists>k<i. P (\<sigma> |\<^sub>s k)); \<not> P \<sigma>; \<forall>k<i. \<not> P (\<sigma> |\<^sub>s Suc k)\<rbrakk> \<Longrightarrow> Q (\<sigma> |\<^sub>s Suc i)
 9. \<And>i. \<lbrakk>Q \<sigma>; \<forall>k<i. \<not> P (\<sigma> |\<^sub>s k); P \<sigma>\<rbrakk> \<Longrightarrow> Q (\<sigma> |\<^sub>s i)
 10. \<And>i. \<lbrakk>Q \<sigma>; \<forall>k<i. \<not> P (\<sigma> |\<^sub>s k); \<forall>i. Q (\<sigma> |\<^sub>s Suc i) \<or> (\<exists>k<i. P (\<sigma> |\<^sub>s Suc k))\<rbrakk> \<Longrightarrow> Q (\<sigma> |\<^sub>s i)
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal (9 subgoals):
 1. \<And>i. \<lbrakk>\<forall>i. Q (\<sigma> |\<^sub>s i) \<longrightarrow> (\<exists>k<i. \<not> P (\<sigma> |\<^sub>s k)); P \<sigma>; \<forall>i. P (\<sigma> |\<^sub>s Suc i)\<rbrakk> \<Longrightarrow> P (\<sigma> |\<^sub>s i)
 2. \<And>i. \<lbrakk>Q (\<sigma> |\<^sub>s i); \<forall>k<i. P (\<sigma> |\<^sub>s k); \<not> Q \<sigma>\<rbrakk> \<Longrightarrow> P \<sigma>
 3. \<And>i. \<lbrakk>Q (\<sigma> |\<^sub>s i); \<forall>k<i. P (\<sigma> |\<^sub>s k); \<not> Q \<sigma>\<rbrakk> \<Longrightarrow> \<exists>i. Q (\<sigma> |\<^sub>s Suc i) \<and> (\<forall>k<i. P (\<sigma> |\<^sub>s Suc k))
 4. Q \<sigma> \<Longrightarrow> \<exists>i. Q (\<sigma> |\<^sub>s i) \<and> (\<forall>k<i. P (\<sigma> |\<^sub>s k))
 5. \<And>i. \<lbrakk>P \<sigma>; Q (\<sigma> |\<^sub>s Suc i); \<forall>k<i. P (\<sigma> |\<^sub>s Suc k)\<rbrakk> \<Longrightarrow> \<exists>i. Q (\<sigma> |\<^sub>s i) \<and> (\<forall>k<i. P (\<sigma> |\<^sub>s k))
 6. \<forall>i. Q (\<sigma> |\<^sub>s i) \<or> (\<exists>k<i. P (\<sigma> |\<^sub>s k)) \<Longrightarrow> Q \<sigma>
 7. \<And>i. \<lbrakk>\<forall>i. Q (\<sigma> |\<^sub>s i) \<or> (\<exists>k<i. P (\<sigma> |\<^sub>s k)); \<not> P \<sigma>; \<forall>k<i. \<not> P (\<sigma> |\<^sub>s Suc k)\<rbrakk> \<Longrightarrow> Q (\<sigma> |\<^sub>s Suc i)
 8. \<And>i. \<lbrakk>Q \<sigma>; \<forall>k<i. \<not> P (\<sigma> |\<^sub>s k); P \<sigma>\<rbrakk> \<Longrightarrow> Q (\<sigma> |\<^sub>s i)
 9. \<And>i. \<lbrakk>Q \<sigma>; \<forall>k<i. \<not> P (\<sigma> |\<^sub>s k); \<forall>i. Q (\<sigma> |\<^sub>s Suc i) \<or> (\<exists>k<i. P (\<sigma> |\<^sub>s Suc k))\<rbrakk> \<Longrightarrow> Q (\<sigma> |\<^sub>s i)
[PROOF STEP]
apply (metis gr0_conv_Suc nat_neq_iff not_less0 suffix_zero)
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<And>i. \<lbrakk>Q (\<sigma> |\<^sub>s i); \<forall>k<i. P (\<sigma> |\<^sub>s k); \<not> Q \<sigma>\<rbrakk> \<Longrightarrow> P \<sigma>
 2. \<And>i. \<lbrakk>Q (\<sigma> |\<^sub>s i); \<forall>k<i. P (\<sigma> |\<^sub>s k); \<not> Q \<sigma>\<rbrakk> \<Longrightarrow> \<exists>i. Q (\<sigma> |\<^sub>s Suc i) \<and> (\<forall>k<i. P (\<sigma> |\<^sub>s Suc k))
 3. Q \<sigma> \<Longrightarrow> \<exists>i. Q (\<sigma> |\<^sub>s i) \<and> (\<forall>k<i. P (\<sigma> |\<^sub>s k))
 4. \<And>i. \<lbrakk>P \<sigma>; Q (\<sigma> |\<^sub>s Suc i); \<forall>k<i. P (\<sigma> |\<^sub>s Suc k)\<rbrakk> \<Longrightarrow> \<exists>i. Q (\<sigma> |\<^sub>s i) \<and> (\<forall>k<i. P (\<sigma> |\<^sub>s k))
 5. \<forall>i. Q (\<sigma> |\<^sub>s i) \<or> (\<exists>k<i. P (\<sigma> |\<^sub>s k)) \<Longrightarrow> Q \<sigma>
 6. \<And>i. \<lbrakk>\<forall>i. Q (\<sigma> |\<^sub>s i) \<or> (\<exists>k<i. P (\<sigma> |\<^sub>s k)); \<not> P \<sigma>; \<forall>k<i. \<not> P (\<sigma> |\<^sub>s Suc k)\<rbrakk> \<Longrightarrow> Q (\<sigma> |\<^sub>s Suc i)
 7. \<And>i. \<lbrakk>Q \<sigma>; \<forall>k<i. \<not> P (\<sigma> |\<^sub>s k); P \<sigma>\<rbrakk> \<Longrightarrow> Q (\<sigma> |\<^sub>s i)
 8. \<And>i. \<lbrakk>Q \<sigma>; \<forall>k<i. \<not> P (\<sigma> |\<^sub>s k); \<forall>i. Q (\<sigma> |\<^sub>s Suc i) \<or> (\<exists>k<i. P (\<sigma> |\<^sub>s Suc k))\<rbrakk> \<Longrightarrow> Q (\<sigma> |\<^sub>s i)
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>i. \<lbrakk>Q (\<sigma> |\<^sub>s i); \<forall>k<i. P (\<sigma> |\<^sub>s k); \<not> Q \<sigma>\<rbrakk> \<Longrightarrow> \<exists>i. Q (\<sigma> |\<^sub>s Suc i) \<and> (\<forall>k<i. P (\<sigma> |\<^sub>s Suc k))
 2. Q \<sigma> \<Longrightarrow> \<exists>i. Q (\<sigma> |\<^sub>s i) \<and> (\<forall>k<i. P (\<sigma> |\<^sub>s k))
 3. \<And>i. \<lbrakk>P \<sigma>; Q (\<sigma> |\<^sub>s Suc i); \<forall>k<i. P (\<sigma> |\<^sub>s Suc k)\<rbrakk> \<Longrightarrow> \<exists>i. Q (\<sigma> |\<^sub>s i) \<and> (\<forall>k<i. P (\<sigma> |\<^sub>s k))
 4. \<forall>i. Q (\<sigma> |\<^sub>s i) \<or> (\<exists>k<i. P (\<sigma> |\<^sub>s k)) \<Longrightarrow> Q \<sigma>
 5. \<And>i. \<lbrakk>\<forall>i. Q (\<sigma> |\<^sub>s i) \<or> (\<exists>k<i. P (\<sigma> |\<^sub>s k)); \<not> P \<sigma>; \<forall>k<i. \<not> P (\<sigma> |\<^sub>s Suc k)\<rbrakk> \<Longrightarrow> Q (\<sigma> |\<^sub>s Suc i)
 6. \<And>i. \<lbrakk>Q \<sigma>; \<forall>k<i. \<not> P (\<sigma> |\<^sub>s k); P \<sigma>\<rbrakk> \<Longrightarrow> Q (\<sigma> |\<^sub>s i)
 7. \<And>i. \<lbrakk>Q \<sigma>; \<forall>k<i. \<not> P (\<sigma> |\<^sub>s k); \<forall>i. Q (\<sigma> |\<^sub>s Suc i) \<or> (\<exists>k<i. P (\<sigma> |\<^sub>s Suc k))\<rbrakk> \<Longrightarrow> Q (\<sigma> |\<^sub>s i)
[PROOF STEP]
apply (case_tac i; auto)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. Q \<sigma> \<Longrightarrow> \<exists>i. Q (\<sigma> |\<^sub>s i) \<and> (\<forall>k<i. P (\<sigma> |\<^sub>s k))
 2. \<And>i. \<lbrakk>P \<sigma>; Q (\<sigma> |\<^sub>s Suc i); \<forall>k<i. P (\<sigma> |\<^sub>s Suc k)\<rbrakk> \<Longrightarrow> \<exists>i. Q (\<sigma> |\<^sub>s i) \<and> (\<forall>k<i. P (\<sigma> |\<^sub>s k))
 3. \<forall>i. Q (\<sigma> |\<^sub>s i) \<or> (\<exists>k<i. P (\<sigma> |\<^sub>s k)) \<Longrightarrow> Q \<sigma>
 4. \<And>i. \<lbrakk>\<forall>i. Q (\<sigma> |\<^sub>s i) \<or> (\<exists>k<i. P (\<sigma> |\<^sub>s k)); \<not> P \<sigma>; \<forall>k<i. \<not> P (\<sigma> |\<^sub>s Suc k)\<rbrakk> \<Longrightarrow> Q (\<sigma> |\<^sub>s Suc i)
 5. \<And>i. \<lbrakk>Q \<sigma>; \<forall>k<i. \<not> P (\<sigma> |\<^sub>s k); P \<sigma>\<rbrakk> \<Longrightarrow> Q (\<sigma> |\<^sub>s i)
 6. \<And>i. \<lbrakk>Q \<sigma>; \<forall>k<i. \<not> P (\<sigma> |\<^sub>s k); \<forall>i. Q (\<sigma> |\<^sub>s Suc i) \<or> (\<exists>k<i. P (\<sigma> |\<^sub>s Suc k))\<rbrakk> \<Longrightarrow> Q (\<sigma> |\<^sub>s i)
[PROOF STEP]
apply force
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>i. \<lbrakk>P \<sigma>; Q (\<sigma> |\<^sub>s Suc i); \<forall>k<i. P (\<sigma> |\<^sub>s Suc k)\<rbrakk> \<Longrightarrow> \<exists>i. Q (\<sigma> |\<^sub>s i) \<and> (\<forall>k<i. P (\<sigma> |\<^sub>s k))
 2. \<forall>i. Q (\<sigma> |\<^sub>s i) \<or> (\<exists>k<i. P (\<sigma> |\<^sub>s k)) \<Longrightarrow> Q \<sigma>
 3. \<And>i. \<lbrakk>\<forall>i. Q (\<sigma> |\<^sub>s i) \<or> (\<exists>k<i. P (\<sigma> |\<^sub>s k)); \<not> P \<sigma>; \<forall>k<i. \<not> P (\<sigma> |\<^sub>s Suc k)\<rbrakk> \<Longrightarrow> Q (\<sigma> |\<^sub>s Suc i)
 4. \<And>i. \<lbrakk>Q \<sigma>; \<forall>k<i. \<not> P (\<sigma> |\<^sub>s k); P \<sigma>\<rbrakk> \<Longrightarrow> Q (\<sigma> |\<^sub>s i)
 5. \<And>i. \<lbrakk>Q \<sigma>; \<forall>k<i. \<not> P (\<sigma> |\<^sub>s k); \<forall>i. Q (\<sigma> |\<^sub>s Suc i) \<or> (\<exists>k<i. P (\<sigma> |\<^sub>s Suc k))\<rbrakk> \<Longrightarrow> Q (\<sigma> |\<^sub>s i)
[PROOF STEP]
using less_Suc_eq_0_disj
[PROOF STATE]
proof (prove)
using this:
(?m < Suc ?n) = (?m = 0 \<or> (\<exists>j. ?m = Suc j \<and> j < ?n))

goal (5 subgoals):
 1. \<And>i. \<lbrakk>P \<sigma>; Q (\<sigma> |\<^sub>s Suc i); \<forall>k<i. P (\<sigma> |\<^sub>s Suc k)\<rbrakk> \<Longrightarrow> \<exists>i. Q (\<sigma> |\<^sub>s i) \<and> (\<forall>k<i. P (\<sigma> |\<^sub>s k))
 2. \<forall>i. Q (\<sigma> |\<^sub>s i) \<or> (\<exists>k<i. P (\<sigma> |\<^sub>s k)) \<Longrightarrow> Q \<sigma>
 3. \<And>i. \<lbrakk>\<forall>i. Q (\<sigma> |\<^sub>s i) \<or> (\<exists>k<i. P (\<sigma> |\<^sub>s k)); \<not> P \<sigma>; \<forall>k<i. \<not> P (\<sigma> |\<^sub>s Suc k)\<rbrakk> \<Longrightarrow> Q (\<sigma> |\<^sub>s Suc i)
 4. \<And>i. \<lbrakk>Q \<sigma>; \<forall>k<i. \<not> P (\<sigma> |\<^sub>s k); P \<sigma>\<rbrakk> \<Longrightarrow> Q (\<sigma> |\<^sub>s i)
 5. \<And>i. \<lbrakk>Q \<sigma>; \<forall>k<i. \<not> P (\<sigma> |\<^sub>s k); \<forall>i. Q (\<sigma> |\<^sub>s Suc i) \<or> (\<exists>k<i. P (\<sigma> |\<^sub>s Suc k))\<rbrakk> \<Longrightarrow> Q (\<sigma> |\<^sub>s i)
[PROOF STEP]
apply force
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<forall>i. Q (\<sigma> |\<^sub>s i) \<or> (\<exists>k<i. P (\<sigma> |\<^sub>s k)) \<Longrightarrow> Q \<sigma>
 2. \<And>i. \<lbrakk>\<forall>i. Q (\<sigma> |\<^sub>s i) \<or> (\<exists>k<i. P (\<sigma> |\<^sub>s k)); \<not> P \<sigma>; \<forall>k<i. \<not> P (\<sigma> |\<^sub>s Suc k)\<rbrakk> \<Longrightarrow> Q (\<sigma> |\<^sub>s Suc i)
 3. \<And>i. \<lbrakk>Q \<sigma>; \<forall>k<i. \<not> P (\<sigma> |\<^sub>s k); P \<sigma>\<rbrakk> \<Longrightarrow> Q (\<sigma> |\<^sub>s i)
 4. \<And>i. \<lbrakk>Q \<sigma>; \<forall>k<i. \<not> P (\<sigma> |\<^sub>s k); \<forall>i. Q (\<sigma> |\<^sub>s Suc i) \<or> (\<exists>k<i. P (\<sigma> |\<^sub>s Suc k))\<rbrakk> \<Longrightarrow> Q (\<sigma> |\<^sub>s i)
[PROOF STEP]
apply force
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>i. \<lbrakk>\<forall>i. Q (\<sigma> |\<^sub>s i) \<or> (\<exists>k<i. P (\<sigma> |\<^sub>s k)); \<not> P \<sigma>; \<forall>k<i. \<not> P (\<sigma> |\<^sub>s Suc k)\<rbrakk> \<Longrightarrow> Q (\<sigma> |\<^sub>s Suc i)
 2. \<And>i. \<lbrakk>Q \<sigma>; \<forall>k<i. \<not> P (\<sigma> |\<^sub>s k); P \<sigma>\<rbrakk> \<Longrightarrow> Q (\<sigma> |\<^sub>s i)
 3. \<And>i. \<lbrakk>Q \<sigma>; \<forall>k<i. \<not> P (\<sigma> |\<^sub>s k); \<forall>i. Q (\<sigma> |\<^sub>s Suc i) \<or> (\<exists>k<i. P (\<sigma> |\<^sub>s Suc k))\<rbrakk> \<Longrightarrow> Q (\<sigma> |\<^sub>s i)
[PROOF STEP]
using less_Suc_eq_0_disj
[PROOF STATE]
proof (prove)
using this:
(?m < Suc ?n) = (?m = 0 \<or> (\<exists>j. ?m = Suc j \<and> j < ?n))

goal (3 subgoals):
 1. \<And>i. \<lbrakk>\<forall>i. Q (\<sigma> |\<^sub>s i) \<or> (\<exists>k<i. P (\<sigma> |\<^sub>s k)); \<not> P \<sigma>; \<forall>k<i. \<not> P (\<sigma> |\<^sub>s Suc k)\<rbrakk> \<Longrightarrow> Q (\<sigma> |\<^sub>s Suc i)
 2. \<And>i. \<lbrakk>Q \<sigma>; \<forall>k<i. \<not> P (\<sigma> |\<^sub>s k); P \<sigma>\<rbrakk> \<Longrightarrow> Q (\<sigma> |\<^sub>s i)
 3. \<And>i. \<lbrakk>Q \<sigma>; \<forall>k<i. \<not> P (\<sigma> |\<^sub>s k); \<forall>i. Q (\<sigma> |\<^sub>s Suc i) \<or> (\<exists>k<i. P (\<sigma> |\<^sub>s Suc k))\<rbrakk> \<Longrightarrow> Q (\<sigma> |\<^sub>s i)
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>i. \<lbrakk>Q \<sigma>; \<forall>k<i. \<not> P (\<sigma> |\<^sub>s k); P \<sigma>\<rbrakk> \<Longrightarrow> Q (\<sigma> |\<^sub>s i)
 2. \<And>i. \<lbrakk>Q \<sigma>; \<forall>k<i. \<not> P (\<sigma> |\<^sub>s k); \<forall>i. Q (\<sigma> |\<^sub>s Suc i) \<or> (\<exists>k<i. P (\<sigma> |\<^sub>s Suc k))\<rbrakk> \<Longrightarrow> Q (\<sigma> |\<^sub>s i)
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>Q \<sigma>; \<forall>k<i. \<not> P (\<sigma> |\<^sub>s k); \<forall>i. Q (\<sigma> |\<^sub>s Suc i) \<or> (\<exists>k<i. P (\<sigma> |\<^sub>s Suc k))\<rbrakk> \<Longrightarrow> Q (\<sigma> |\<^sub>s i)
[PROOF STEP]
apply (case_tac i; auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma mono:
  "\<lbrakk>(\<box>P) \<sigma>; \<And>\<sigma>. P \<sigma> \<Longrightarrow>  P' \<sigma>\<rbrakk> \<Longrightarrow> (\<box>P') \<sigma>"
  "\<lbrakk>(\<diamond>P) \<sigma>; \<And>\<sigma>. P \<sigma> \<Longrightarrow>  P' \<sigma>\<rbrakk> \<Longrightarrow> (\<diamond>P') \<sigma>"
  "\<lbrakk>(P \<U> Q) \<sigma>; \<And>\<sigma>. P \<sigma> \<Longrightarrow> P' \<sigma>; \<And>\<sigma>. Q \<sigma> \<Longrightarrow> Q' \<sigma>\<rbrakk> \<Longrightarrow> (P' \<U> Q') \<sigma>"
  "\<lbrakk>(P \<W> Q) \<sigma>; \<And>\<sigma>. P \<sigma> \<Longrightarrow> P' \<sigma>; \<And>\<sigma>. Q \<sigma> \<Longrightarrow> Q' \<sigma>\<rbrakk> \<Longrightarrow> (P' \<W> Q') \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lbrakk>(\<box>P) \<sigma>; \<And>\<sigma>. P \<sigma> \<Longrightarrow> P' \<sigma>\<rbrakk> \<Longrightarrow> (\<box>P') \<sigma>) &&& (\<lbrakk>(\<diamond>P) \<sigma>; \<And>\<sigma>. P \<sigma> \<Longrightarrow> P' \<sigma>\<rbrakk> \<Longrightarrow> (\<diamond>P') \<sigma>)) &&& (\<lbrakk>(P \<U> Q) \<sigma>; \<And>\<sigma>. P \<sigma> \<Longrightarrow> P' \<sigma>; \<And>\<sigma>. Q \<sigma> \<Longrightarrow> Q' \<sigma>\<rbrakk> \<Longrightarrow> (P' \<U> Q') \<sigma>) &&& (\<lbrakk>(P \<W> Q) \<sigma>; \<And>\<sigma>. P \<sigma> \<Longrightarrow> P' \<sigma>; \<And>\<sigma>. Q \<sigma> \<Longrightarrow> Q' \<sigma>\<rbrakk> \<Longrightarrow> (P' \<W> Q') \<sigma>)
[PROOF STEP]
unfolding defs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lbrakk>\<forall>i. P (\<sigma> |\<^sub>s i); \<And>\<sigma>. P \<sigma> \<Longrightarrow> P' \<sigma>\<rbrakk> \<Longrightarrow> \<forall>i. P' (\<sigma> |\<^sub>s i)) &&& (\<lbrakk>\<exists>i. P (\<sigma> |\<^sub>s i) \<and> (\<forall>k<i. True); \<And>\<sigma>. P \<sigma> \<Longrightarrow> P' \<sigma>\<rbrakk> \<Longrightarrow> \<exists>i. P' (\<sigma> |\<^sub>s i) \<and> (\<forall>k<i. True))) &&& (\<lbrakk>\<exists>i. Q (\<sigma> |\<^sub>s i) \<and> (\<forall>k<i. P (\<sigma> |\<^sub>s k)); \<And>\<sigma>. P \<sigma> \<Longrightarrow> P' \<sigma>; \<And>\<sigma>. Q \<sigma> \<Longrightarrow> Q' \<sigma>\<rbrakk> \<Longrightarrow> \<exists>i. Q' (\<sigma> |\<^sub>s i) \<and> (\<forall>k<i. P' (\<sigma> |\<^sub>s k))) &&& (\<lbrakk>(\<exists>i. Q (\<sigma> |\<^sub>s i) \<and> (\<forall>k<i. P (\<sigma> |\<^sub>s k))) \<or> (\<forall>i. P (\<sigma> |\<^sub>s i)); \<And>\<sigma>. P \<sigma> \<Longrightarrow> P' \<sigma>; \<And>\<sigma>. Q \<sigma> \<Longrightarrow> Q' \<sigma>\<rbrakk> \<Longrightarrow> (\<exists>i. Q' (\<sigma> |\<^sub>s i) \<and> (\<forall>k<i. P' (\<sigma> |\<^sub>s k))) \<or> (\<forall>i. P' (\<sigma> |\<^sub>s i)))
[PROOF STEP]
by force+


[STATEMENT]
lemma always_imp_mono:
  "\<lbrakk>(\<box>P) \<sigma>; (P \<^bold>\<hookrightarrow> P') \<sigma>\<rbrakk> \<Longrightarrow> (\<box>P') \<sigma>"
  "\<lbrakk>(\<diamond>P) \<sigma>; (P \<^bold>\<hookrightarrow> P') \<sigma>\<rbrakk> \<Longrightarrow> (\<diamond>P') \<sigma>"
  "\<lbrakk>(P \<U> Q) \<sigma>; (P \<^bold>\<hookrightarrow> P') \<sigma>; (Q \<^bold>\<hookrightarrow> Q') \<sigma>\<rbrakk> \<Longrightarrow> (P' \<U> Q') \<sigma>"
  "\<lbrakk>(P \<W> Q) \<sigma>; (P \<^bold>\<hookrightarrow> P') \<sigma>; (Q \<^bold>\<hookrightarrow> Q') \<sigma>\<rbrakk> \<Longrightarrow> (P' \<W> Q') \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lbrakk>(\<box>P) \<sigma>; (\<box>(\<lambda>s. P s \<longrightarrow> P' s)) \<sigma>\<rbrakk> \<Longrightarrow> (\<box>P') \<sigma>) &&& (\<lbrakk>(\<diamond>P) \<sigma>; (\<box>(\<lambda>s. P s \<longrightarrow> P' s)) \<sigma>\<rbrakk> \<Longrightarrow> (\<diamond>P') \<sigma>)) &&& (\<lbrakk>(P \<U> Q) \<sigma>; (\<box>(\<lambda>s. P s \<longrightarrow> P' s)) \<sigma>; (\<box>(\<lambda>s. Q s \<longrightarrow> Q' s)) \<sigma>\<rbrakk> \<Longrightarrow> (P' \<U> Q') \<sigma>) &&& (\<lbrakk>(P \<W> Q) \<sigma>; (\<box>(\<lambda>s. P s \<longrightarrow> P' s)) \<sigma>; (\<box>(\<lambda>s. Q s \<longrightarrow> Q' s)) \<sigma>\<rbrakk> \<Longrightarrow> (P' \<W> Q') \<sigma>)
[PROOF STEP]
unfolding defs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lbrakk>\<forall>i. P (\<sigma> |\<^sub>s i); \<forall>i. P (\<sigma> |\<^sub>s i) \<longrightarrow> P' (\<sigma> |\<^sub>s i)\<rbrakk> \<Longrightarrow> \<forall>i. P' (\<sigma> |\<^sub>s i)) &&& (\<lbrakk>\<exists>i. P (\<sigma> |\<^sub>s i) \<and> (\<forall>k<i. True); \<forall>i. P (\<sigma> |\<^sub>s i) \<longrightarrow> P' (\<sigma> |\<^sub>s i)\<rbrakk> \<Longrightarrow> \<exists>i. P' (\<sigma> |\<^sub>s i) \<and> (\<forall>k<i. True))) &&& (\<lbrakk>\<exists>i. Q (\<sigma> |\<^sub>s i) \<and> (\<forall>k<i. P (\<sigma> |\<^sub>s k)); \<forall>i. P (\<sigma> |\<^sub>s i) \<longrightarrow> P' (\<sigma> |\<^sub>s i); \<forall>i. Q (\<sigma> |\<^sub>s i) \<longrightarrow> Q' (\<sigma> |\<^sub>s i)\<rbrakk> \<Longrightarrow> \<exists>i. Q' (\<sigma> |\<^sub>s i) \<and> (\<forall>k<i. P' (\<sigma> |\<^sub>s k))) &&& (\<lbrakk>(\<exists>i. Q (\<sigma> |\<^sub>s i) \<and> (\<forall>k<i. P (\<sigma> |\<^sub>s k))) \<or> (\<forall>i. P (\<sigma> |\<^sub>s i)); \<forall>i. P (\<sigma> |\<^sub>s i) \<longrightarrow> P' (\<sigma> |\<^sub>s i); \<forall>i. Q (\<sigma> |\<^sub>s i) \<longrightarrow> Q' (\<sigma> |\<^sub>s i)\<rbrakk> \<Longrightarrow> (\<exists>i. Q' (\<sigma> |\<^sub>s i) \<and> (\<forall>k<i. P' (\<sigma> |\<^sub>s k))) \<or> (\<forall>i. P' (\<sigma> |\<^sub>s i)))
[PROOF STEP]
by force+


[STATEMENT]
lemma next_conj_distrib:
  "(\<circle>(P \<^bold>\<and> Q)) = (\<circle>P \<^bold>\<and> \<circle>Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<circle>(\<lambda>s. P s \<and> Q s) = (\<lambda>s. (\<circle>P) s \<and> (\<circle>Q) s)
[PROOF STEP]
unfolding defs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>\<sigma>. P (\<sigma> |\<^sub>s 1) \<and> Q (\<sigma> |\<^sub>s 1)) = (\<lambda>s. P (s |\<^sub>s 1) \<and> Q (s |\<^sub>s 1))
[PROOF STEP]
by auto


[STATEMENT]
lemma next_disj_distrib:
  "(\<circle>(P \<^bold>\<or> Q)) = (\<circle>P \<^bold>\<or> \<circle>Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<circle>(\<lambda>s. P s \<or> Q s) = (\<lambda>s. (\<circle>P) s \<or> (\<circle>Q) s)
[PROOF STEP]
unfolding defs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>\<sigma>. P (\<sigma> |\<^sub>s 1) \<or> Q (\<sigma> |\<^sub>s 1)) = (\<lambda>s. P (s |\<^sub>s 1) \<or> Q (s |\<^sub>s 1))
[PROOF STEP]
by auto


[STATEMENT]
lemma until_next_distrib:
  "(\<circle>(P \<U> Q)) = (\<circle>P \<U> \<circle>Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<circle>(P \<U> Q) = (\<circle>P \<U> \<circle>Q)
[PROOF STEP]
unfolding defs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>\<sigma>. \<exists>i. Q (\<sigma> |\<^sub>s 1 |\<^sub>s i) \<and> (\<forall>k<i. P (\<sigma> |\<^sub>s 1 |\<^sub>s k))) = (\<lambda>\<sigma>. \<exists>i. Q (\<sigma> |\<^sub>s i |\<^sub>s 1) \<and> (\<forall>k<i. P (\<sigma> |\<^sub>s k |\<^sub>s 1)))
[PROOF STEP]
by (auto simp: fun_eq_iff)


[STATEMENT]
lemma until_imp_eventually:
  "((P \<U> Q) \<^bold>\<longrightarrow> \<diamond>Q) \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P \<U> Q) \<sigma> \<longrightarrow> (\<diamond>Q) \<sigma>
[PROOF STEP]
unfolding defs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>i. Q (\<sigma> |\<^sub>s i) \<and> (\<forall>k<i. P (\<sigma> |\<^sub>s k))) \<longrightarrow> (\<exists>i. Q (\<sigma> |\<^sub>s i) \<and> (\<forall>k<i. True))
[PROOF STEP]
by auto


[STATEMENT]
lemma until_until_disj:
  assumes "(P \<U> Q \<U> R) \<sigma>"
  shows "((P \<^bold>\<or> Q) \<U> R) \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>s. P s \<or> Q s) \<U> R) \<sigma>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(P \<U> Q \<U> R) \<sigma>

goal (1 subgoal):
 1. ((\<lambda>s. P s \<or> Q s) \<U> R) \<sigma>
[PROOF STEP]
unfolding defs
[PROOF STATE]
proof (prove)
using this:
\<exists>i. (\<exists>ia. R (\<sigma> |\<^sub>s i |\<^sub>s ia) \<and> (\<forall>k<ia. Q (\<sigma> |\<^sub>s i |\<^sub>s k))) \<and> (\<forall>k<i. P (\<sigma> |\<^sub>s k))

goal (1 subgoal):
 1. \<exists>i. R (\<sigma> |\<^sub>s i) \<and> (\<forall>k<i. P (\<sigma> |\<^sub>s k) \<or> Q (\<sigma> |\<^sub>s k))
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i ia. \<lbrakk>\<forall>k<i. P (\<sigma> |\<^sub>s k); R (\<sigma> |\<^sub>s i + ia); \<forall>k<ia. Q (\<sigma> |\<^sub>s i + k)\<rbrakk> \<Longrightarrow> \<exists>i. R (\<sigma> |\<^sub>s i) \<and> (\<forall>k<i. P (\<sigma> |\<^sub>s k) \<or> Q (\<sigma> |\<^sub>s k))
[PROOF STEP]
apply (metis (full_types) add_diff_inverse_nat nat_add_left_cancel_less)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma unless_unless_disj:
  assumes "(P \<W> Q \<W> R) \<sigma>"
  shows "((P \<^bold>\<or> Q) \<W> R) \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>s. P s \<or> Q s) \<W> R) \<sigma>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(P \<W> Q \<W> R) \<sigma>

goal (1 subgoal):
 1. ((\<lambda>s. P s \<or> Q s) \<W> R) \<sigma>
[PROOF STEP]
unfolding defs
[PROOF STATE]
proof (prove)
using this:
(\<exists>i. ((\<exists>ia. R (\<sigma> |\<^sub>s i |\<^sub>s ia) \<and> (\<forall>k<ia. Q (\<sigma> |\<^sub>s i |\<^sub>s k))) \<or> (\<forall>ia. Q (\<sigma> |\<^sub>s i |\<^sub>s ia))) \<and> (\<forall>k<i. P (\<sigma> |\<^sub>s k))) \<or> (\<forall>i. P (\<sigma> |\<^sub>s i))

goal (1 subgoal):
 1. (\<exists>i. R (\<sigma> |\<^sub>s i) \<and> (\<forall>k<i. P (\<sigma> |\<^sub>s k) \<or> Q (\<sigma> |\<^sub>s k))) \<or> (\<forall>i. P (\<sigma> |\<^sub>s i) \<or> Q (\<sigma> |\<^sub>s i))
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>i ia ib. \<lbrakk>\<forall>i. R (\<sigma> |\<^sub>s i) \<longrightarrow> (\<exists>k<i. \<not> P (\<sigma> |\<^sub>s k) \<and> \<not> Q (\<sigma> |\<^sub>s k)); \<not> Q (\<sigma> |\<^sub>s i); \<forall>k<ia. P (\<sigma> |\<^sub>s k); R (\<sigma> |\<^sub>s ia + ib); \<forall>k<ib. Q (\<sigma> |\<^sub>s ia + k)\<rbrakk> \<Longrightarrow> P (\<sigma> |\<^sub>s i)
 2. \<And>i ia. \<lbrakk>\<forall>i. R (\<sigma> |\<^sub>s i) \<longrightarrow> (\<exists>k<i. \<not> P (\<sigma> |\<^sub>s k) \<and> \<not> Q (\<sigma> |\<^sub>s k)); \<not> Q (\<sigma> |\<^sub>s i); \<forall>k<ia. P (\<sigma> |\<^sub>s k); \<forall>i. Q (\<sigma> |\<^sub>s ia + i)\<rbrakk> \<Longrightarrow> P (\<sigma> |\<^sub>s i)
[PROOF STEP]
apply (metis add.commute add_diff_inverse_nat leI less_diff_conv2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i ia. \<lbrakk>\<forall>i. R (\<sigma> |\<^sub>s i) \<longrightarrow> (\<exists>k<i. \<not> P (\<sigma> |\<^sub>s k) \<and> \<not> Q (\<sigma> |\<^sub>s k)); \<not> Q (\<sigma> |\<^sub>s i); \<forall>k<ia. P (\<sigma> |\<^sub>s k); \<forall>i. Q (\<sigma> |\<^sub>s ia + i)\<rbrakk> \<Longrightarrow> P (\<sigma> |\<^sub>s i)
[PROOF STEP]
apply (metis add_diff_inverse_nat)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma until_conj_distrib:
  "((P \<^bold>\<and> Q) \<U> R) = ((P \<U> R) \<^bold>\<and> (Q \<U> R))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>s. P s \<and> Q s) \<U> R) = (\<lambda>s. (P \<U> R) s \<and> (Q \<U> R) s)
[PROOF STEP]
unfolding defs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>\<sigma>. \<exists>i. R (\<sigma> |\<^sub>s i) \<and> (\<forall>k<i. P (\<sigma> |\<^sub>s k) \<and> Q (\<sigma> |\<^sub>s k))) = (\<lambda>s. (\<exists>i. R (s |\<^sub>s i) \<and> (\<forall>k<i. P (s |\<^sub>s k))) \<and> (\<exists>i. R (s |\<^sub>s i) \<and> (\<forall>k<i. Q (s |\<^sub>s k))))
[PROOF STEP]
apply (auto simp: fun_eq_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x i ia. \<lbrakk>R (x |\<^sub>s i); \<forall>k<i. P (x |\<^sub>s k); R (x |\<^sub>s ia); \<forall>k<ia. Q (x |\<^sub>s k)\<rbrakk> \<Longrightarrow> \<exists>i. R (x |\<^sub>s i) \<and> (\<forall>k<i. P (x |\<^sub>s k) \<and> Q (x |\<^sub>s k))
[PROOF STEP]
apply (metis dual_order.strict_trans nat_neq_iff)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma until_disj_distrib:
  "(P \<U> (Q \<^bold>\<or> R)) = ((P \<U> Q) \<^bold>\<or> (P \<U> R))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P \<U> (\<lambda>s. Q s \<or> R s)) = (\<lambda>s. (P \<U> Q) s \<or> (P \<U> R) s)
[PROOF STEP]
unfolding defs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>\<sigma>. \<exists>i. (Q (\<sigma> |\<^sub>s i) \<or> R (\<sigma> |\<^sub>s i)) \<and> (\<forall>k<i. P (\<sigma> |\<^sub>s k))) = (\<lambda>s. (\<exists>i. Q (s |\<^sub>s i) \<and> (\<forall>k<i. P (s |\<^sub>s k))) \<or> (\<exists>i. R (s |\<^sub>s i) \<and> (\<forall>k<i. P (s |\<^sub>s k))))
[PROOF STEP]
by (auto simp: fun_eq_iff)


[STATEMENT]
lemma eventually_until:
  "(\<diamond>P) = (\<^bold>\<not>P \<U> P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<diamond>P = ((\<lambda>s. \<not> P s) \<U> P)
[PROOF STEP]
unfolding defs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>\<sigma>. \<exists>i. P (\<sigma> |\<^sub>s i) \<and> (\<forall>k<i. True)) = (\<lambda>\<sigma>. \<exists>i. P (\<sigma> |\<^sub>s i) \<and> (\<forall>k<i. \<not> P (\<sigma> |\<^sub>s k)))
[PROOF STEP]
apply (auto simp: fun_eq_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x i. P (x |\<^sub>s i) \<Longrightarrow> \<exists>i. P (x |\<^sub>s i) \<and> (\<forall>k<i. \<not> P (x |\<^sub>s k))
[PROOF STEP]
apply (case_tac "P (x |\<^sub>s 0)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x i. \<lbrakk>P (x |\<^sub>s i); P (x |\<^sub>s 0)\<rbrakk> \<Longrightarrow> \<exists>i. P (x |\<^sub>s i) \<and> (\<forall>k<i. \<not> P (x |\<^sub>s k))
 2. \<And>x i. \<lbrakk>P (x |\<^sub>s i); \<not> P (x |\<^sub>s 0)\<rbrakk> \<Longrightarrow> \<exists>i. P (x |\<^sub>s i) \<and> (\<forall>k<i. \<not> P (x |\<^sub>s k))
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x i. \<lbrakk>P (x |\<^sub>s i); \<not> P (x |\<^sub>s 0)\<rbrakk> \<Longrightarrow> \<exists>i. P (x |\<^sub>s i) \<and> (\<forall>k<i. \<not> P (x |\<^sub>s k))
[PROOF STEP]
apply (drule (1) ex_least_nat_less)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x i. \<lbrakk>\<not> P (x |\<^sub>s 0); \<exists>k<i. (\<forall>i\<le>k. \<not> P (x |\<^sub>s i)) \<and> P (x |\<^sub>s Suc k)\<rbrakk> \<Longrightarrow> \<exists>i. P (x |\<^sub>s i) \<and> (\<forall>k<i. \<not> P (x |\<^sub>s k))
[PROOF STEP]
apply (metis le_simps(2))
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma eventually_until_eventually:
  "(\<diamond>(P \<U> Q)) = (\<diamond>Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<diamond>(P \<U> Q) = \<diamond>Q
[PROOF STEP]
unfolding defs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>\<sigma>. \<exists>i. (\<exists>ia. Q (\<sigma> |\<^sub>s i |\<^sub>s ia) \<and> (\<forall>k<ia. P (\<sigma> |\<^sub>s i |\<^sub>s k))) \<and> (\<forall>k<i. True)) = (\<lambda>\<sigma>. \<exists>i. Q (\<sigma> |\<^sub>s i) \<and> (\<forall>k<i. True))
[PROOF STEP]
by force


[STATEMENT]
lemma eventually_unless_until:
  "((P \<W> Q) \<^bold>\<and> \<diamond>Q) = (P \<U> Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>s. (P \<W> Q) s \<and> (\<diamond>Q) s) = (P \<U> Q)
[PROOF STEP]
unfolding defs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>s. ((\<exists>i. Q (s |\<^sub>s i) \<and> (\<forall>k<i. P (s |\<^sub>s k))) \<or> (\<forall>i. P (s |\<^sub>s i))) \<and> (\<exists>i. Q (s |\<^sub>s i) \<and> (\<forall>k<i. True))) = (\<lambda>\<sigma>. \<exists>i. Q (\<sigma> |\<^sub>s i) \<and> (\<forall>k<i. P (\<sigma> |\<^sub>s k)))
[PROOF STEP]
by force


[STATEMENT]
lemma eventually_always_imp_always_eventually:
  assumes "(\<diamond>\<box>P) \<sigma>"
  shows "(\<box>\<diamond>P) \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<box>\<diamond>P) \<sigma>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(\<diamond>\<box>P) \<sigma>

goal (1 subgoal):
 1. (\<box>\<diamond>P) \<sigma>
[PROOF STEP]
unfolding defs
[PROOF STATE]
proof (prove)
using this:
\<exists>i. (\<forall>ia. P (\<sigma> |\<^sub>s i |\<^sub>s ia)) \<and> (\<forall>k<i. True)

goal (1 subgoal):
 1. \<forall>i. \<exists>ia. P (\<sigma> |\<^sub>s i |\<^sub>s ia) \<and> (\<forall>k<ia. True)
[PROOF STEP]
by (metis suffix_commute)


[STATEMENT]
lemma eventually_always_next_stable:
  assumes "(\<diamond>P) \<sigma>"
  assumes "(P \<^bold>\<hookrightarrow> \<circle>P) \<sigma>"
  shows "(\<diamond>\<box>P) \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<diamond>\<box>P) \<sigma>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(\<diamond>P) \<sigma>
(\<box>(\<lambda>s. P s \<longrightarrow> (\<circle>P) s)) \<sigma>

goal (1 subgoal):
 1. (\<diamond>\<box>P) \<sigma>
[PROOF STEP]
by (metis (no_types) eventuallyI alwaysD always_induct eventuallyE norm(15))


[STATEMENT]
lemma next_stable_imp_eventually_always:
  assumes "(P \<^bold>\<hookrightarrow> \<circle>P) \<sigma>"
  shows "(\<diamond>P \<^bold>\<longrightarrow> \<diamond>\<box>P) \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<diamond>P) \<sigma> \<longrightarrow> (\<diamond>\<box>P) \<sigma>
[PROOF STEP]
using assms eventually_always_next_stable
[PROOF STATE]
proof (prove)
using this:
(\<box>(\<lambda>s. P s \<longrightarrow> (\<circle>P) s)) \<sigma>
\<lbrakk>(\<diamond>?P) ?\<sigma>; (\<box>(\<lambda>s. ?P s \<longrightarrow> (\<circle>?P) s)) ?\<sigma>\<rbrakk> \<Longrightarrow> (\<diamond>\<box>?P) ?\<sigma>

goal (1 subgoal):
 1. (\<diamond>P) \<sigma> \<longrightarrow> (\<diamond>\<box>P) \<sigma>
[PROOF STEP]
by blast


[STATEMENT]
lemma always_eventually_always:
  "\<diamond>\<box>\<diamond>P = \<box>\<diamond>P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<diamond>\<box>\<diamond>P = \<box>\<diamond>P
[PROOF STEP]
unfolding defs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>\<sigma>. \<exists>i. (\<forall>ia. \<exists>ib. P (\<sigma> |\<^sub>s i |\<^sub>s ia |\<^sub>s ib) \<and> (\<forall>k<ib. True)) \<and> (\<forall>k<i. True)) = (\<lambda>\<sigma>. \<forall>i. \<exists>ia. P (\<sigma> |\<^sub>s i |\<^sub>s ia) \<and> (\<forall>k<ia. True))
[PROOF STEP]
by (clarsimp simp: fun_eq_iff) (metis add.left_commute semiring_normalization_rules(25))


[STATEMENT]
lemma stable_unless:
  assumes "(P \<^bold>\<hookrightarrow> \<circle>(P \<^bold>\<or> Q)) \<sigma>"
  shows "(P \<^bold>\<hookrightarrow> (P \<W> Q)) \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<box>(\<lambda>s. P s \<longrightarrow> (P \<W> Q) s)) \<sigma>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(\<box>(\<lambda>s. P s \<longrightarrow> (\<circle>(\<lambda>s. P s \<or> Q s)) s)) \<sigma>

goal (1 subgoal):
 1. (\<box>(\<lambda>s. P s \<longrightarrow> (P \<W> Q) s)) \<sigma>
[PROOF STEP]
unfolding defs
[PROOF STATE]
proof (prove)
using this:
\<forall>i. P (\<sigma> |\<^sub>s i) \<longrightarrow> P (\<sigma> |\<^sub>s i |\<^sub>s 1) \<or> Q (\<sigma> |\<^sub>s i |\<^sub>s 1)

goal (1 subgoal):
 1. \<forall>i. P (\<sigma> |\<^sub>s i) \<longrightarrow> (\<exists>ia. Q (\<sigma> |\<^sub>s i |\<^sub>s ia) \<and> (\<forall>k<ia. P (\<sigma> |\<^sub>s i |\<^sub>s k))) \<or> (\<forall>ia. P (\<sigma> |\<^sub>s i |\<^sub>s ia))
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i. P (\<sigma> |\<^sub>s i) \<longrightarrow> P (\<sigma> |\<^sub>s i |\<^sub>s 1) \<or> Q (\<sigma> |\<^sub>s i |\<^sub>s 1) \<Longrightarrow> \<forall>i. P (\<sigma> |\<^sub>s i) \<longrightarrow> (\<exists>ia. Q (\<sigma> |\<^sub>s i |\<^sub>s ia) \<and> (\<forall>k<ia. P (\<sigma> |\<^sub>s i |\<^sub>s k))) \<or> (\<forall>ia. P (\<sigma> |\<^sub>s i |\<^sub>s ia))
[PROOF STEP]
apply (rule ccontr)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>i. P (\<sigma> |\<^sub>s i) \<longrightarrow> P (\<sigma> |\<^sub>s i |\<^sub>s 1) \<or> Q (\<sigma> |\<^sub>s i |\<^sub>s 1); \<not> (\<forall>i. P (\<sigma> |\<^sub>s i) \<longrightarrow> (\<exists>ia. Q (\<sigma> |\<^sub>s i |\<^sub>s ia) \<and> (\<forall>k<ia. P (\<sigma> |\<^sub>s i |\<^sub>s k))) \<or> (\<forall>ia. P (\<sigma> |\<^sub>s i |\<^sub>s ia)))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i ia. \<lbrakk>\<forall>i. P (\<sigma> |\<^sub>s i) \<longrightarrow> P (\<sigma> |\<^sub>s Suc i) \<or> Q (\<sigma> |\<^sub>s Suc i); P (\<sigma> |\<^sub>s i); \<forall>ia. Q (\<sigma> |\<^sub>s i + ia) \<longrightarrow> (\<exists>k<ia. \<not> P (\<sigma> |\<^sub>s i + k)); \<not> P (\<sigma> |\<^sub>s i + ia)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (drule (1) ex_least_nat_less[where P="\<lambda>j. \<not>P (\<sigma> |\<^sub>s i + j)" for i, simplified])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i ia. \<lbrakk>\<forall>i. P (\<sigma> |\<^sub>s i) \<longrightarrow> P (\<sigma> |\<^sub>s Suc i) \<or> Q (\<sigma> |\<^sub>s Suc i); P (\<sigma> |\<^sub>s i); \<forall>ia. Q (\<sigma> |\<^sub>s i + ia) \<longrightarrow> (\<exists>k<ia. \<not> P (\<sigma> |\<^sub>s i + k)); \<exists>k<ia. (\<forall>ia\<le>k. P (\<sigma> |\<^sub>s i + ia)) \<and> \<not> P (\<sigma> |\<^sub>s Suc (i + k))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i ia k. \<lbrakk>\<forall>i. P (\<sigma> |\<^sub>s i) \<longrightarrow> P (\<sigma> |\<^sub>s Suc i) \<or> Q (\<sigma> |\<^sub>s Suc i); P (\<sigma> |\<^sub>s i); \<forall>ia. Q (\<sigma> |\<^sub>s i + ia) \<longrightarrow> (\<exists>k<ia. \<not> P (\<sigma> |\<^sub>s i + k)); k < ia; \<forall>ia\<le>k. P (\<sigma> |\<^sub>s i + ia); \<not> P (\<sigma> |\<^sub>s Suc (i + k))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (metis add_Suc_right le_less less_Suc_eq)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma unless_induct: \<comment>\<open> Rule \texttt{WAIT} from @{cite [cite_macro=citet] \<open>Fig~3.3\<close> "MannaPnueli:1995"}\<close>
  assumes I: "(I \<^bold>\<hookrightarrow> \<circle>(I \<^bold>\<or> R)) \<sigma>"
  assumes P: "(P \<^bold>\<hookrightarrow> I \<^bold>\<or> R) \<sigma>"
  assumes Q: "(I \<^bold>\<hookrightarrow> Q) \<sigma>"
  shows "(P \<^bold>\<hookrightarrow> Q \<W> R) \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<box>(\<lambda>s. P s \<longrightarrow> (Q \<W> R) s)) \<sigma>
[PROOF STEP]
apply (intro alwaysI impI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. P (\<sigma> |\<^sub>s i) \<Longrightarrow> (Q \<W> R) (\<sigma> |\<^sub>s i)
[PROOF STEP]
apply (erule impE[OF alwaysD[OF P]])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. I (\<sigma> |\<^sub>s i) \<or> R (\<sigma> |\<^sub>s i) \<Longrightarrow> (Q \<W> R) (\<sigma> |\<^sub>s i)
[PROOF STEP]
apply (erule disjE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>i. I (\<sigma> |\<^sub>s i) \<Longrightarrow> (Q \<W> R) (\<sigma> |\<^sub>s i)
 2. \<And>i. R (\<sigma> |\<^sub>s i) \<Longrightarrow> (Q \<W> R) (\<sigma> |\<^sub>s i)
[PROOF STEP]
apply (rule always_imp_mono(4)[where P=I and Q=R])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>i. I (\<sigma> |\<^sub>s i) \<Longrightarrow> (I \<W> R) (\<sigma> |\<^sub>s i)
 2. \<And>i. I (\<sigma> |\<^sub>s i) \<Longrightarrow> (\<box>(\<lambda>s. I s \<longrightarrow> Q s)) (\<sigma> |\<^sub>s i)
 3. \<And>i. I (\<sigma> |\<^sub>s i) \<Longrightarrow> (\<box>(\<lambda>s. R s \<longrightarrow> R s)) (\<sigma> |\<^sub>s i)
 4. \<And>i. R (\<sigma> |\<^sub>s i) \<Longrightarrow> (Q \<W> R) (\<sigma> |\<^sub>s i)
[PROOF STEP]
apply (erule mp[OF alwaysD[OF stable_unless[OF I]]])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>i. I (\<sigma> |\<^sub>s i) \<Longrightarrow> (\<box>(\<lambda>s. I s \<longrightarrow> Q s)) (\<sigma> |\<^sub>s i)
 2. \<And>i. I (\<sigma> |\<^sub>s i) \<Longrightarrow> (\<box>(\<lambda>s. R s \<longrightarrow> R s)) (\<sigma> |\<^sub>s i)
 3. \<And>i. R (\<sigma> |\<^sub>s i) \<Longrightarrow> (Q \<W> R) (\<sigma> |\<^sub>s i)
[PROOF STEP]
apply (simp add: Q alwaysD)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>i. I (\<sigma> |\<^sub>s i) \<Longrightarrow> (\<box>(\<lambda>s. R s \<longrightarrow> R s)) (\<sigma> |\<^sub>s i)
 2. \<And>i. R (\<sigma> |\<^sub>s i) \<Longrightarrow> (Q \<W> R) (\<sigma> |\<^sub>s i)
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. R (\<sigma> |\<^sub>s i) \<Longrightarrow> (Q \<W> R) (\<sigma> |\<^sub>s i)
[PROOF STEP]
apply (simp add: unfold)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma leads_to_refl:
  shows "(P \<^bold>\<leadsto> P) \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<box>(\<lambda>s. P s \<longrightarrow> (\<diamond>P) s)) \<sigma>
[PROOF STEP]
by (metis (no_types, lifting) necessitation(1) unfold(2))


[STATEMENT]
lemma leads_to_trans:
  assumes "(P \<^bold>\<leadsto> Q) \<sigma>"
  assumes "(Q \<^bold>\<leadsto> R) \<sigma>"
  shows "(P \<^bold>\<leadsto> R) \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<box>(\<lambda>s. P s \<longrightarrow> (\<diamond>R) s)) \<sigma>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(\<box>(\<lambda>s. P s \<longrightarrow> (\<diamond>Q) s)) \<sigma>
(\<box>(\<lambda>s. Q s \<longrightarrow> (\<diamond>R) s)) \<sigma>

goal (1 subgoal):
 1. (\<box>(\<lambda>s. P s \<longrightarrow> (\<diamond>R) s)) \<sigma>
[PROOF STEP]
unfolding defs
[PROOF STATE]
proof (prove)
using this:
\<forall>i. P (\<sigma> |\<^sub>s i) \<longrightarrow> (\<exists>ia. Q (\<sigma> |\<^sub>s i |\<^sub>s ia) \<and> (\<forall>k<ia. True))
\<forall>i. Q (\<sigma> |\<^sub>s i) \<longrightarrow> (\<exists>ia. R (\<sigma> |\<^sub>s i |\<^sub>s ia) \<and> (\<forall>k<ia. True))

goal (1 subgoal):
 1. \<forall>i. P (\<sigma> |\<^sub>s i) \<longrightarrow> (\<exists>ia. R (\<sigma> |\<^sub>s i |\<^sub>s ia) \<and> (\<forall>k<ia. True))
[PROOF STEP]
by clarsimp (metis semiring_normalization_rules(25))


[STATEMENT]
lemma leads_to_eventuallyE:
  assumes "(P \<^bold>\<leadsto> Q) \<sigma>"
  assumes "(\<diamond>P) \<sigma>"
  shows "(\<diamond>Q) \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<diamond>Q) \<sigma>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(\<box>(\<lambda>s. P s \<longrightarrow> (\<diamond>Q) s)) \<sigma>
(\<diamond>P) \<sigma>

goal (1 subgoal):
 1. (\<diamond>Q) \<sigma>
[PROOF STEP]
unfolding defs
[PROOF STATE]
proof (prove)
using this:
\<forall>i. P (\<sigma> |\<^sub>s i) \<longrightarrow> (\<exists>ia. Q (\<sigma> |\<^sub>s i |\<^sub>s ia) \<and> (\<forall>k<ia. True))
\<exists>i. P (\<sigma> |\<^sub>s i) \<and> (\<forall>k<i. True)

goal (1 subgoal):
 1. \<exists>i. Q (\<sigma> |\<^sub>s i) \<and> (\<forall>k<i. True)
[PROOF STEP]
by auto


[STATEMENT]
lemma leads_to_mono:
  assumes "(P' \<^bold>\<hookrightarrow> P) \<sigma>"
  assumes "(Q \<^bold>\<hookrightarrow> Q') \<sigma>"
  assumes "(P \<^bold>\<leadsto> Q) \<sigma>"
  shows "(P' \<^bold>\<leadsto> Q') \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<box>(\<lambda>s. P' s \<longrightarrow> (\<diamond>Q') s)) \<sigma>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(\<box>(\<lambda>s. P' s \<longrightarrow> P s)) \<sigma>
(\<box>(\<lambda>s. Q s \<longrightarrow> Q' s)) \<sigma>
(\<box>(\<lambda>s. P s \<longrightarrow> (\<diamond>Q) s)) \<sigma>

goal (1 subgoal):
 1. (\<box>(\<lambda>s. P' s \<longrightarrow> (\<diamond>Q') s)) \<sigma>
[PROOF STEP]
unfolding defs
[PROOF STATE]
proof (prove)
using this:
\<forall>i. P' (\<sigma> |\<^sub>s i) \<longrightarrow> P (\<sigma> |\<^sub>s i)
\<forall>i. Q (\<sigma> |\<^sub>s i) \<longrightarrow> Q' (\<sigma> |\<^sub>s i)
\<forall>i. P (\<sigma> |\<^sub>s i) \<longrightarrow> (\<exists>ia. Q (\<sigma> |\<^sub>s i |\<^sub>s ia) \<and> (\<forall>k<ia. True))

goal (1 subgoal):
 1. \<forall>i. P' (\<sigma> |\<^sub>s i) \<longrightarrow> (\<exists>ia. Q' (\<sigma> |\<^sub>s i |\<^sub>s ia) \<and> (\<forall>k<ia. True))
[PROOF STEP]
by clarsimp blast


[STATEMENT]
lemma leads_to_eventually:
  shows "(P \<^bold>\<leadsto> Q \<^bold>\<longrightarrow> \<diamond>P \<^bold>\<longrightarrow> \<diamond>Q) \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<box>(\<lambda>s. P s \<longrightarrow> (\<diamond>(\<lambda>s. Q s \<longrightarrow> (\<diamond>P) s \<longrightarrow> (\<diamond>Q) s)) s)) \<sigma>
[PROOF STEP]
by (metis (no_types, lifting) alwaysI unfold(2))


[STATEMENT]
lemma leads_to_disj:
  assumes "(P \<^bold>\<leadsto> R) \<sigma>"
  assumes "(Q \<^bold>\<leadsto> R) \<sigma>"
  shows "((P \<^bold>\<or> Q) \<^bold>\<leadsto> R) \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<box>(\<lambda>s. P s \<or> Q s \<longrightarrow> (\<diamond>R) s)) \<sigma>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(\<box>(\<lambda>s. P s \<longrightarrow> (\<diamond>R) s)) \<sigma>
(\<box>(\<lambda>s. Q s \<longrightarrow> (\<diamond>R) s)) \<sigma>

goal (1 subgoal):
 1. (\<box>(\<lambda>s. P s \<or> Q s \<longrightarrow> (\<diamond>R) s)) \<sigma>
[PROOF STEP]
unfolding defs
[PROOF STATE]
proof (prove)
using this:
\<forall>i. P (\<sigma> |\<^sub>s i) \<longrightarrow> (\<exists>ia. R (\<sigma> |\<^sub>s i |\<^sub>s ia) \<and> (\<forall>k<ia. True))
\<forall>i. Q (\<sigma> |\<^sub>s i) \<longrightarrow> (\<exists>ia. R (\<sigma> |\<^sub>s i |\<^sub>s ia) \<and> (\<forall>k<ia. True))

goal (1 subgoal):
 1. \<forall>i. P (\<sigma> |\<^sub>s i) \<or> Q (\<sigma> |\<^sub>s i) \<longrightarrow> (\<exists>ia. R (\<sigma> |\<^sub>s i |\<^sub>s ia) \<and> (\<forall>k<ia. True))
[PROOF STEP]
by simp


[STATEMENT]
lemma leads_to_leads_to_viaE:
  shows "((P \<^bold>\<hookrightarrow> P \<U> Q) \<^bold>\<longrightarrow> P \<^bold>\<leadsto> Q) \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<box>(\<lambda>s. P s \<longrightarrow> (P \<U> Q) s)) \<sigma> \<longrightarrow> (\<box>(\<lambda>s. P s \<longrightarrow> (\<diamond>Q) s)) \<sigma>
[PROOF STEP]
unfolding defs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>i. P (\<sigma> |\<^sub>s i) \<longrightarrow> (\<exists>ia. Q (\<sigma> |\<^sub>s i |\<^sub>s ia) \<and> (\<forall>k<ia. P (\<sigma> |\<^sub>s i |\<^sub>s k)))) \<longrightarrow> (\<forall>i. P (\<sigma> |\<^sub>s i) \<longrightarrow> (\<exists>ia. Q (\<sigma> |\<^sub>s i |\<^sub>s ia) \<and> (\<forall>k<ia. True)))
[PROOF STEP]
by clarsimp blast


[STATEMENT]
lemma leads_to_via_concl_weaken:
  assumes "(R \<^bold>\<hookrightarrow> R') \<sigma>"
  assumes "(P \<^bold>\<hookrightarrow> Q \<U> R) \<sigma>"
  shows "(P \<^bold>\<hookrightarrow> Q \<U> R') \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<box>(\<lambda>s. P s \<longrightarrow> (Q \<U> R') s)) \<sigma>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(\<box>(\<lambda>s. R s \<longrightarrow> R' s)) \<sigma>
(\<box>(\<lambda>s. P s \<longrightarrow> (Q \<U> R) s)) \<sigma>

goal (1 subgoal):
 1. (\<box>(\<lambda>s. P s \<longrightarrow> (Q \<U> R') s)) \<sigma>
[PROOF STEP]
unfolding LTL.defs
[PROOF STATE]
proof (prove)
using this:
\<forall>i. R (\<sigma> |\<^sub>s i) \<longrightarrow> R' (\<sigma> |\<^sub>s i)
\<forall>i. P (\<sigma> |\<^sub>s i) \<longrightarrow> (\<exists>ia. R (\<sigma> |\<^sub>s i |\<^sub>s ia) \<and> (\<forall>k<ia. Q (\<sigma> |\<^sub>s i |\<^sub>s k)))

goal (1 subgoal):
 1. \<forall>i. P (\<sigma> |\<^sub>s i) \<longrightarrow> (\<exists>ia. R' (\<sigma> |\<^sub>s i |\<^sub>s ia) \<and> (\<forall>k<ia. Q (\<sigma> |\<^sub>s i |\<^sub>s k)))
[PROOF STEP]
by force


[STATEMENT]
lemma leads_to_via_trans:
  assumes "(A \<^bold>\<hookrightarrow> B \<U> C) \<sigma>"
  assumes "(C \<^bold>\<hookrightarrow> D \<U> E) \<sigma>"
  shows "(A \<^bold>\<hookrightarrow> (B \<^bold>\<or> D) \<U> E) \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<box>(\<lambda>s. A s \<longrightarrow> ((\<lambda>s. B s \<or> D s) \<U> E) s)) \<sigma>
[PROOF STEP]
proof(rule alwaysI, rule impI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. A (\<sigma> |\<^sub>s i) \<Longrightarrow> ((\<lambda>s. B s \<or> D s) \<U> E) (\<sigma> |\<^sub>s i)
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. A (\<sigma> |\<^sub>s i) \<Longrightarrow> ((\<lambda>s. B s \<or> D s) \<U> E) (\<sigma> |\<^sub>s i)
[PROOF STEP]
assume "A (\<sigma> |\<^sub>s i)"
[PROOF STATE]
proof (state)
this:
A (\<sigma> |\<^sub>s i)

goal (1 subgoal):
 1. \<And>i. A (\<sigma> |\<^sub>s i) \<Longrightarrow> ((\<lambda>s. B s \<or> D s) \<U> E) (\<sigma> |\<^sub>s i)
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
(\<box>(\<lambda>s. A s \<longrightarrow> (B \<U> C) s)) \<sigma>
(\<box>(\<lambda>s. C s \<longrightarrow> (D \<U> E) s)) \<sigma>
A (\<sigma> |\<^sub>s i)
[PROOF STEP]
show "((B \<^bold>\<or> D) \<U> E) (\<sigma> |\<^sub>s i)"
[PROOF STATE]
proof (prove)
using this:
(\<box>(\<lambda>s. A s \<longrightarrow> (B \<U> C) s)) \<sigma>
(\<box>(\<lambda>s. C s \<longrightarrow> (D \<U> E) s)) \<sigma>
A (\<sigma> |\<^sub>s i)

goal (1 subgoal):
 1. ((\<lambda>s. B s \<or> D s) \<U> E) (\<sigma> |\<^sub>s i)
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<box>(\<lambda>s. A s \<longrightarrow> (B \<U> C) s)) \<sigma>; (\<box>(\<lambda>s. C s \<longrightarrow> (D \<U> E) s)) \<sigma>; A (\<sigma> |\<^sub>s i)\<rbrakk> \<Longrightarrow> ((\<lambda>s. B s \<or> D s) \<U> E) (\<sigma> |\<^sub>s i)
[PROOF STEP]
apply (erule alwaysE[where i=i])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<box>(\<lambda>s. C s \<longrightarrow> (D \<U> E) s)) \<sigma>; A (\<sigma> |\<^sub>s i); A (\<sigma> |\<^sub>s i) \<longrightarrow> (B \<U> C) (\<sigma> |\<^sub>s i)\<rbrakk> \<Longrightarrow> ((\<lambda>s. B s \<or> D s) \<U> E) (\<sigma> |\<^sub>s i)
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<box>(\<lambda>s. C s \<longrightarrow> (D \<U> E) s)) \<sigma>; A (\<sigma> |\<^sub>s i); (B \<U> C) (\<sigma> |\<^sub>s i)\<rbrakk> \<Longrightarrow> ((\<lambda>s. B s \<or> D s) \<U> E) (\<sigma> |\<^sub>s i)
[PROOF STEP]
apply (erule untilE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ia. \<lbrakk>(\<box>(\<lambda>s. C s \<longrightarrow> (D \<U> E) s)) \<sigma>; A (\<sigma> |\<^sub>s i); C (\<sigma> |\<^sub>s i |\<^sub>s ia); \<forall>k<ia. B (\<sigma> |\<^sub>s i |\<^sub>s k)\<rbrakk> \<Longrightarrow> ((\<lambda>s. B s \<or> D s) \<U> E) (\<sigma> |\<^sub>s i)
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ia. \<lbrakk>(\<box>(\<lambda>s. C s \<longrightarrow> (D \<U> E) s)) \<sigma>; A (\<sigma> |\<^sub>s i); C (\<sigma> |\<^sub>s i + ia); \<forall>k<ia. B (\<sigma> |\<^sub>s i + k)\<rbrakk> \<Longrightarrow> ((\<lambda>s. B s \<or> D s) \<U> E) (\<sigma> |\<^sub>s i)
[PROOF STEP]
(* suffix *)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ia. \<lbrakk>(\<box>(\<lambda>s. C s \<longrightarrow> (D \<U> E) s)) \<sigma>; A (\<sigma> |\<^sub>s i); C (\<sigma> |\<^sub>s i + ia); \<forall>k<ia. B (\<sigma> |\<^sub>s i + k)\<rbrakk> \<Longrightarrow> ((\<lambda>s. B s \<or> D s) \<U> E) (\<sigma> |\<^sub>s i)
[PROOF STEP]
apply (drule (1) always_imp_mp_suffix)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ia. \<lbrakk>A (\<sigma> |\<^sub>s i); C (\<sigma> |\<^sub>s i + ia); \<forall>k<ia. B (\<sigma> |\<^sub>s i + k); (D \<U> E) (\<sigma> |\<^sub>s i + ia)\<rbrakk> \<Longrightarrow> ((\<lambda>s. B s \<or> D s) \<U> E) (\<sigma> |\<^sub>s i)
[PROOF STEP]
apply (erule untilE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ia iaa. \<lbrakk>A (\<sigma> |\<^sub>s i); C (\<sigma> |\<^sub>s i + ia); \<forall>k<ia. B (\<sigma> |\<^sub>s i + k); E (\<sigma> |\<^sub>s i + ia |\<^sub>s iaa); \<forall>k<iaa. D (\<sigma> |\<^sub>s i + ia |\<^sub>s k)\<rbrakk> \<Longrightarrow> ((\<lambda>s. B s \<or> D s) \<U> E) (\<sigma> |\<^sub>s i)
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ia iaa. \<lbrakk>A (\<sigma> |\<^sub>s i); C (\<sigma> |\<^sub>s i + ia); \<forall>k<ia. B (\<sigma> |\<^sub>s i + k); E (\<sigma> |\<^sub>s i + ia + iaa); \<forall>k<iaa. D (\<sigma> |\<^sub>s i + ia + k)\<rbrakk> \<Longrightarrow> ((\<lambda>s. B s \<or> D s) \<U> E) (\<sigma> |\<^sub>s i)
[PROOF STEP]
(* suffix *)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ia iaa. \<lbrakk>A (\<sigma> |\<^sub>s i); C (\<sigma> |\<^sub>s i + ia); \<forall>k<ia. B (\<sigma> |\<^sub>s i + k); E (\<sigma> |\<^sub>s i + ia + iaa); \<forall>k<iaa. D (\<sigma> |\<^sub>s i + ia + k)\<rbrakk> \<Longrightarrow> ((\<lambda>s. B s \<or> D s) \<U> E) (\<sigma> |\<^sub>s i)
[PROOF STEP]
apply (rule_tac i="ia + iaa" in untilI; simp add: ac_simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ia iaa. \<lbrakk>A (\<sigma> |\<^sub>s i); C (\<sigma> |\<^sub>s ia + i); \<forall>k<ia. B (\<sigma> |\<^sub>s k + i); E (\<sigma> |\<^sub>s ia + (iaa + i)); \<forall>k<iaa. D (\<sigma> |\<^sub>s ia + (k + i))\<rbrakk> \<Longrightarrow> \<forall>k<ia + iaa. B (\<sigma> |\<^sub>s k + i) \<or> D (\<sigma> |\<^sub>s k + i)
[PROOF STEP]
apply (metis (full_types) add.assoc leI le_Suc_ex nat_add_left_cancel_less)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
(* arithmetic *)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
((\<lambda>s. B s \<or> D s) \<U> E) (\<sigma> |\<^sub>s i)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma leads_to_via_disj: \<comment> \<open> useful for case distinctions \<close>
  assumes "(P \<^bold>\<hookrightarrow> Q \<U> R) \<sigma>"
  assumes "(P' \<^bold>\<hookrightarrow> Q' \<U> R) \<sigma>"
  shows "(P \<^bold>\<or> P' \<^bold>\<hookrightarrow> (Q \<^bold>\<or> Q') \<U> R) \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<box>(\<lambda>s. P s \<or> P' s \<longrightarrow> ((\<lambda>s. Q s \<or> Q' s) \<U> R) s)) \<sigma>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(\<box>(\<lambda>s. P s \<longrightarrow> (Q \<U> R) s)) \<sigma>
(\<box>(\<lambda>s. P' s \<longrightarrow> (Q' \<U> R) s)) \<sigma>

goal (1 subgoal):
 1. (\<box>(\<lambda>s. P s \<or> P' s \<longrightarrow> ((\<lambda>s. Q s \<or> Q' s) \<U> R) s)) \<sigma>
[PROOF STEP]
unfolding defs
[PROOF STATE]
proof (prove)
using this:
\<forall>i. P (\<sigma> |\<^sub>s i) \<longrightarrow> (\<exists>ia. R (\<sigma> |\<^sub>s i |\<^sub>s ia) \<and> (\<forall>k<ia. Q (\<sigma> |\<^sub>s i |\<^sub>s k)))
\<forall>i. P' (\<sigma> |\<^sub>s i) \<longrightarrow> (\<exists>ia. R (\<sigma> |\<^sub>s i |\<^sub>s ia) \<and> (\<forall>k<ia. Q' (\<sigma> |\<^sub>s i |\<^sub>s k)))

goal (1 subgoal):
 1. \<forall>i. P (\<sigma> |\<^sub>s i) \<or> P' (\<sigma> |\<^sub>s i) \<longrightarrow> (\<exists>ia. R (\<sigma> |\<^sub>s i |\<^sub>s ia) \<and> (\<forall>k<ia. Q (\<sigma> |\<^sub>s i |\<^sub>s k) \<or> Q' (\<sigma> |\<^sub>s i |\<^sub>s k)))
[PROOF STEP]
by (auto 10 0)


[STATEMENT]
lemma leads_to_via_disj': \<comment> \<open> more like a chaining rule \<close>
  assumes "(A \<^bold>\<hookrightarrow> B \<U> C) \<sigma>"
  assumes "(C \<^bold>\<hookrightarrow> D \<U> E) \<sigma>"
  shows "(A \<^bold>\<or> C \<^bold>\<hookrightarrow> (B \<^bold>\<or> D) \<U> E) \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<box>(\<lambda>s. A s \<or> C s \<longrightarrow> ((\<lambda>s. B s \<or> D s) \<U> E) s)) \<sigma>
[PROOF STEP]
proof(rule alwaysI, rule impI, erule disjE)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i. A (\<sigma> |\<^sub>s i) \<Longrightarrow> ((\<lambda>s. B s \<or> D s) \<U> E) (\<sigma> |\<^sub>s i)
 2. \<And>i. C (\<sigma> |\<^sub>s i) \<Longrightarrow> ((\<lambda>s. B s \<or> D s) \<U> E) (\<sigma> |\<^sub>s i)
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i. A (\<sigma> |\<^sub>s i) \<Longrightarrow> ((\<lambda>s. B s \<or> D s) \<U> E) (\<sigma> |\<^sub>s i)
 2. \<And>i. C (\<sigma> |\<^sub>s i) \<Longrightarrow> ((\<lambda>s. B s \<or> D s) \<U> E) (\<sigma> |\<^sub>s i)
[PROOF STEP]
assume "A (\<sigma> |\<^sub>s i)"
[PROOF STATE]
proof (state)
this:
A (\<sigma> |\<^sub>s i)

goal (2 subgoals):
 1. \<And>i. A (\<sigma> |\<^sub>s i) \<Longrightarrow> ((\<lambda>s. B s \<or> D s) \<U> E) (\<sigma> |\<^sub>s i)
 2. \<And>i. C (\<sigma> |\<^sub>s i) \<Longrightarrow> ((\<lambda>s. B s \<or> D s) \<U> E) (\<sigma> |\<^sub>s i)
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
(\<box>(\<lambda>s. A s \<longrightarrow> (B \<U> C) s)) \<sigma>
(\<box>(\<lambda>s. C s \<longrightarrow> (D \<U> E) s)) \<sigma>
A (\<sigma> |\<^sub>s i)
[PROOF STEP]
show "((B \<^bold>\<or> D) \<U> E) (\<sigma> |\<^sub>s i)"
[PROOF STATE]
proof (prove)
using this:
(\<box>(\<lambda>s. A s \<longrightarrow> (B \<U> C) s)) \<sigma>
(\<box>(\<lambda>s. C s \<longrightarrow> (D \<U> E) s)) \<sigma>
A (\<sigma> |\<^sub>s i)

goal (1 subgoal):
 1. ((\<lambda>s. B s \<or> D s) \<U> E) (\<sigma> |\<^sub>s i)
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<box>(\<lambda>s. A s \<longrightarrow> (B \<U> C) s)) \<sigma>; (\<box>(\<lambda>s. C s \<longrightarrow> (D \<U> E) s)) \<sigma>; A (\<sigma> |\<^sub>s i)\<rbrakk> \<Longrightarrow> ((\<lambda>s. B s \<or> D s) \<U> E) (\<sigma> |\<^sub>s i)
[PROOF STEP]
apply (erule alwaysE[where i=i])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<box>(\<lambda>s. C s \<longrightarrow> (D \<U> E) s)) \<sigma>; A (\<sigma> |\<^sub>s i); A (\<sigma> |\<^sub>s i) \<longrightarrow> (B \<U> C) (\<sigma> |\<^sub>s i)\<rbrakk> \<Longrightarrow> ((\<lambda>s. B s \<or> D s) \<U> E) (\<sigma> |\<^sub>s i)
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<box>(\<lambda>s. C s \<longrightarrow> (D \<U> E) s)) \<sigma>; A (\<sigma> |\<^sub>s i); (B \<U> C) (\<sigma> |\<^sub>s i)\<rbrakk> \<Longrightarrow> ((\<lambda>s. B s \<or> D s) \<U> E) (\<sigma> |\<^sub>s i)
[PROOF STEP]
apply (erule untilE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ia. \<lbrakk>(\<box>(\<lambda>s. C s \<longrightarrow> (D \<U> E) s)) \<sigma>; A (\<sigma> |\<^sub>s i); C (\<sigma> |\<^sub>s i |\<^sub>s ia); \<forall>k<ia. B (\<sigma> |\<^sub>s i |\<^sub>s k)\<rbrakk> \<Longrightarrow> ((\<lambda>s. B s \<or> D s) \<U> E) (\<sigma> |\<^sub>s i)
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ia. \<lbrakk>(\<box>(\<lambda>s. C s \<longrightarrow> (D \<U> E) s)) \<sigma>; A (\<sigma> |\<^sub>s i); C (\<sigma> |\<^sub>s i + ia); \<forall>k<ia. B (\<sigma> |\<^sub>s i + k)\<rbrakk> \<Longrightarrow> ((\<lambda>s. B s \<or> D s) \<U> E) (\<sigma> |\<^sub>s i)
[PROOF STEP]
(* suffix *)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ia. \<lbrakk>(\<box>(\<lambda>s. C s \<longrightarrow> (D \<U> E) s)) \<sigma>; A (\<sigma> |\<^sub>s i); C (\<sigma> |\<^sub>s i + ia); \<forall>k<ia. B (\<sigma> |\<^sub>s i + k)\<rbrakk> \<Longrightarrow> ((\<lambda>s. B s \<or> D s) \<U> E) (\<sigma> |\<^sub>s i)
[PROOF STEP]
apply (drule (1) always_imp_mp_suffix)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ia. \<lbrakk>A (\<sigma> |\<^sub>s i); C (\<sigma> |\<^sub>s i + ia); \<forall>k<ia. B (\<sigma> |\<^sub>s i + k); (D \<U> E) (\<sigma> |\<^sub>s i + ia)\<rbrakk> \<Longrightarrow> ((\<lambda>s. B s \<or> D s) \<U> E) (\<sigma> |\<^sub>s i)
[PROOF STEP]
apply (erule untilE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ia iaa. \<lbrakk>A (\<sigma> |\<^sub>s i); C (\<sigma> |\<^sub>s i + ia); \<forall>k<ia. B (\<sigma> |\<^sub>s i + k); E (\<sigma> |\<^sub>s i + ia |\<^sub>s iaa); \<forall>k<iaa. D (\<sigma> |\<^sub>s i + ia |\<^sub>s k)\<rbrakk> \<Longrightarrow> ((\<lambda>s. B s \<or> D s) \<U> E) (\<sigma> |\<^sub>s i)
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ia iaa. \<lbrakk>A (\<sigma> |\<^sub>s i); C (\<sigma> |\<^sub>s i + ia); \<forall>k<ia. B (\<sigma> |\<^sub>s i + k); E (\<sigma> |\<^sub>s i + ia + iaa); \<forall>k<iaa. D (\<sigma> |\<^sub>s i + ia + k)\<rbrakk> \<Longrightarrow> ((\<lambda>s. B s \<or> D s) \<U> E) (\<sigma> |\<^sub>s i)
[PROOF STEP]
(* suffix *)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ia iaa. \<lbrakk>A (\<sigma> |\<^sub>s i); C (\<sigma> |\<^sub>s i + ia); \<forall>k<ia. B (\<sigma> |\<^sub>s i + k); E (\<sigma> |\<^sub>s i + ia + iaa); \<forall>k<iaa. D (\<sigma> |\<^sub>s i + ia + k)\<rbrakk> \<Longrightarrow> ((\<lambda>s. B s \<or> D s) \<U> E) (\<sigma> |\<^sub>s i)
[PROOF STEP]
apply (rule_tac i="ia + iaa" in untilI; simp add: ac_simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ia iaa. \<lbrakk>A (\<sigma> |\<^sub>s i); C (\<sigma> |\<^sub>s ia + i); \<forall>k<ia. B (\<sigma> |\<^sub>s k + i); E (\<sigma> |\<^sub>s ia + (iaa + i)); \<forall>k<iaa. D (\<sigma> |\<^sub>s ia + (k + i))\<rbrakk> \<Longrightarrow> \<forall>k<ia + iaa. B (\<sigma> |\<^sub>s k + i) \<or> D (\<sigma> |\<^sub>s k + i)
[PROOF STEP]
apply (metis (full_types) add.assoc leI le_Suc_ex nat_add_left_cancel_less)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
(* arithmetic *)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
((\<lambda>s. B s \<or> D s) \<U> E) (\<sigma> |\<^sub>s i)

goal (1 subgoal):
 1. \<And>i. C (\<sigma> |\<^sub>s i) \<Longrightarrow> ((\<lambda>s. B s \<or> D s) \<U> E) (\<sigma> |\<^sub>s i)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. C (\<sigma> |\<^sub>s i) \<Longrightarrow> ((\<lambda>s. B s \<or> D s) \<U> E) (\<sigma> |\<^sub>s i)
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. C (\<sigma> |\<^sub>s i) \<Longrightarrow> ((\<lambda>s. B s \<or> D s) \<U> E) (\<sigma> |\<^sub>s i)
[PROOF STEP]
assume "C (\<sigma> |\<^sub>s i)"
[PROOF STATE]
proof (state)
this:
C (\<sigma> |\<^sub>s i)

goal (1 subgoal):
 1. \<And>i. C (\<sigma> |\<^sub>s i) \<Longrightarrow> ((\<lambda>s. B s \<or> D s) \<U> E) (\<sigma> |\<^sub>s i)
[PROOF STEP]
with assms(2)
[PROOF STATE]
proof (chain)
picking this:
(\<box>(\<lambda>s. C s \<longrightarrow> (D \<U> E) s)) \<sigma>
C (\<sigma> |\<^sub>s i)
[PROOF STEP]
show "((B \<^bold>\<or> D) \<U> E) (\<sigma> |\<^sub>s i)"
[PROOF STATE]
proof (prove)
using this:
(\<box>(\<lambda>s. C s \<longrightarrow> (D \<U> E) s)) \<sigma>
C (\<sigma> |\<^sub>s i)

goal (1 subgoal):
 1. ((\<lambda>s. B s \<or> D s) \<U> E) (\<sigma> |\<^sub>s i)
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<box>(\<lambda>s. C s \<longrightarrow> (D \<U> E) s)) \<sigma>; C (\<sigma> |\<^sub>s i)\<rbrakk> \<Longrightarrow> ((\<lambda>s. B s \<or> D s) \<U> E) (\<sigma> |\<^sub>s i)
[PROOF STEP]
apply (erule alwaysE[where i=i])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>C (\<sigma> |\<^sub>s i); C (\<sigma> |\<^sub>s i) \<longrightarrow> (D \<U> E) (\<sigma> |\<^sub>s i)\<rbrakk> \<Longrightarrow> ((\<lambda>s. B s \<or> D s) \<U> E) (\<sigma> |\<^sub>s i)
[PROOF STEP]
apply (simp add: mono)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
((\<lambda>s. B s \<or> D s) \<U> E) (\<sigma> |\<^sub>s i)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma leads_to_via_stable_augmentation:
  assumes stable: "(P \<^bold>\<and> Q \<^bold>\<hookrightarrow> \<circle>Q) \<sigma>"
  assumes U: "(A \<^bold>\<hookrightarrow> P \<U> C) \<sigma>"
  shows "((A \<^bold>\<and> Q) \<^bold>\<hookrightarrow> P \<U> (C \<^bold>\<and> Q)) \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<box>(\<lambda>s. A s \<and> Q s \<longrightarrow> (P \<U> (\<lambda>s. C s \<and> Q s)) s)) \<sigma>
[PROOF STEP]
proof(intro alwaysI impI, elim conjE)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>A (\<sigma> |\<^sub>s i); Q (\<sigma> |\<^sub>s i)\<rbrakk> \<Longrightarrow> (P \<U> (\<lambda>s. C s \<and> Q s)) (\<sigma> |\<^sub>s i)
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>A (\<sigma> |\<^sub>s i); Q (\<sigma> |\<^sub>s i)\<rbrakk> \<Longrightarrow> (P \<U> (\<lambda>s. C s \<and> Q s)) (\<sigma> |\<^sub>s i)
[PROOF STEP]
assume AP: "A (\<sigma> |\<^sub>s i)" "Q (\<sigma> |\<^sub>s i)"
[PROOF STATE]
proof (state)
this:
A (\<sigma> |\<^sub>s i)
Q (\<sigma> |\<^sub>s i)

goal (1 subgoal):
 1. \<And>i. \<lbrakk>A (\<sigma> |\<^sub>s i); Q (\<sigma> |\<^sub>s i)\<rbrakk> \<Longrightarrow> (P \<U> (\<lambda>s. C s \<and> Q s)) (\<sigma> |\<^sub>s i)
[PROOF STEP]
have "Q (\<sigma> |\<^sub>s (j + i))" if "Q (\<sigma> |\<^sub>s i)" and "\<forall>k<j. P (\<sigma> |\<^sub>s (k + i))" for j
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Q (\<sigma> |\<^sub>s j + i)
[PROOF STEP]
using that stable
[PROOF STATE]
proof (prove)
using this:
Q (\<sigma> |\<^sub>s i)
\<forall>k<j. P (\<sigma> |\<^sub>s k + i)
(\<box>(\<lambda>s. P s \<and> Q s \<longrightarrow> (\<circle>Q) s)) \<sigma>

goal (1 subgoal):
 1. Q (\<sigma> |\<^sub>s j + i)
[PROOF STEP]
by (induct j; force simp: defs)
[PROOF STATE]
proof (state)
this:
\<lbrakk>Q (\<sigma> |\<^sub>s i); \<forall>k<?j. P (\<sigma> |\<^sub>s k + i)\<rbrakk> \<Longrightarrow> Q (\<sigma> |\<^sub>s ?j + i)

goal (1 subgoal):
 1. \<And>i. \<lbrakk>A (\<sigma> |\<^sub>s i); Q (\<sigma> |\<^sub>s i)\<rbrakk> \<Longrightarrow> (P \<U> (\<lambda>s. C s \<and> Q s)) (\<sigma> |\<^sub>s i)
[PROOF STEP]
with U AP
[PROOF STATE]
proof (chain)
picking this:
(\<box>(\<lambda>s. A s \<longrightarrow> (P \<U> C) s)) \<sigma>
A (\<sigma> |\<^sub>s i)
Q (\<sigma> |\<^sub>s i)
\<lbrakk>Q (\<sigma> |\<^sub>s i); \<forall>k<?j. P (\<sigma> |\<^sub>s k + i)\<rbrakk> \<Longrightarrow> Q (\<sigma> |\<^sub>s ?j + i)
[PROOF STEP]
show "(P \<U> (\<lambda>\<sigma>. C \<sigma> \<and> Q \<sigma>)) (\<sigma> |\<^sub>s i)"
[PROOF STATE]
proof (prove)
using this:
(\<box>(\<lambda>s. A s \<longrightarrow> (P \<U> C) s)) \<sigma>
A (\<sigma> |\<^sub>s i)
Q (\<sigma> |\<^sub>s i)
\<lbrakk>Q (\<sigma> |\<^sub>s i); \<forall>k<?j. P (\<sigma> |\<^sub>s k + i)\<rbrakk> \<Longrightarrow> Q (\<sigma> |\<^sub>s ?j + i)

goal (1 subgoal):
 1. (P \<U> (\<lambda>\<sigma>. C \<sigma> \<and> Q \<sigma>)) (\<sigma> |\<^sub>s i)
[PROOF STEP]
unfolding defs
[PROOF STATE]
proof (prove)
using this:
\<forall>i. A (\<sigma> |\<^sub>s i) \<longrightarrow> (\<exists>ia. C (\<sigma> |\<^sub>s i |\<^sub>s ia) \<and> (\<forall>k<ia. P (\<sigma> |\<^sub>s i |\<^sub>s k)))
A (\<sigma> |\<^sub>s i)
Q (\<sigma> |\<^sub>s i)
\<lbrakk>Q (\<sigma> |\<^sub>s i); \<forall>k<?j. P (\<sigma> |\<^sub>s k + i)\<rbrakk> \<Longrightarrow> Q (\<sigma> |\<^sub>s ?j + i)

goal (1 subgoal):
 1. \<exists>ia. (C (\<sigma> |\<^sub>s i |\<^sub>s ia) \<and> Q (\<sigma> |\<^sub>s i |\<^sub>s ia)) \<and> (\<forall>k<ia. P (\<sigma> |\<^sub>s i |\<^sub>s k))
[PROOF STEP]
by clarsimp (metis (full_types) add.commute)
[PROOF STATE]
proof (state)
this:
(P \<U> (\<lambda>\<sigma>. C \<sigma> \<and> Q \<sigma>)) (\<sigma> |\<^sub>s i)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma leads_to_via_wf:
  assumes "wf R"
  assumes indhyp: "\<And>t. (A \<^bold>\<and> \<lceil>\<delta> \<^bold>= \<langle>t\<rangle>\<rceil> \<^bold>\<hookrightarrow> B \<U> (A \<^bold>\<and> \<lceil>\<delta> \<^bold>\<otimes> \<langle>t\<rangle> \<^bold>\<in> \<langle>R\<rangle>\<rceil> \<^bold>\<or> C)) \<sigma>"
  shows "(A \<^bold>\<hookrightarrow> B \<U> C) \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<box>(\<lambda>s. A s \<longrightarrow> (B \<U> C) s)) \<sigma>
[PROOF STEP]
proof(intro alwaysI impI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. A (\<sigma> |\<^sub>s i) \<Longrightarrow> (B \<U> C) (\<sigma> |\<^sub>s i)
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. A (\<sigma> |\<^sub>s i) \<Longrightarrow> (B \<U> C) (\<sigma> |\<^sub>s i)
[PROOF STEP]
assume "A (\<sigma> |\<^sub>s i)"
[PROOF STATE]
proof (state)
this:
A (\<sigma> |\<^sub>s i)

goal (1 subgoal):
 1. \<And>i. A (\<sigma> |\<^sub>s i) \<Longrightarrow> (B \<U> C) (\<sigma> |\<^sub>s i)
[PROOF STEP]
with \<open>wf R\<close>
[PROOF STATE]
proof (chain)
picking this:
wf R
A (\<sigma> |\<^sub>s i)
[PROOF STEP]
show "(B \<U> C) (\<sigma> |\<^sub>s i)"
[PROOF STATE]
proof (prove)
using this:
wf R
A (\<sigma> |\<^sub>s i)

goal (1 subgoal):
 1. (B \<U> C) (\<sigma> |\<^sub>s i)
[PROOF STEP]
proof(induct "\<delta> (\<sigma> i)" arbitrary: i)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>\<And>ia. \<lbrakk>(\<delta> (\<sigma> ia), \<delta> (\<sigma> i)) \<in> R; A (\<sigma> |\<^sub>s ia)\<rbrakk> \<Longrightarrow> (B \<U> C) (\<sigma> |\<^sub>s ia); A (\<sigma> |\<^sub>s i)\<rbrakk> \<Longrightarrow> (B \<U> C) (\<sigma> |\<^sub>s i)
[PROOF STEP]
case (less i)
[PROOF STATE]
proof (state)
this:
\<lbrakk>(\<delta> (\<sigma> ?i), \<delta> (\<sigma> i)) \<in> R; A (\<sigma> |\<^sub>s ?i)\<rbrakk> \<Longrightarrow> (B \<U> C) (\<sigma> |\<^sub>s ?i)
A (\<sigma> |\<^sub>s i)

goal (1 subgoal):
 1. \<And>i. \<lbrakk>\<And>ia. \<lbrakk>(\<delta> (\<sigma> ia), \<delta> (\<sigma> i)) \<in> R; A (\<sigma> |\<^sub>s ia)\<rbrakk> \<Longrightarrow> (B \<U> C) (\<sigma> |\<^sub>s ia); A (\<sigma> |\<^sub>s i)\<rbrakk> \<Longrightarrow> (B \<U> C) (\<sigma> |\<^sub>s i)
[PROOF STEP]
with indhyp[where t="\<delta> (\<sigma> i)"]
[PROOF STATE]
proof (chain)
picking this:
(\<box>(\<lambda>s. A s \<and> \<lceil>\<lambda>s. \<delta> s = \<delta> (\<sigma> i)\<rceil> s \<longrightarrow> (B \<U> (\<lambda>s. A s \<and> \<lceil>\<lambda>s. (\<delta> s, \<delta> (\<sigma> i)) \<in> R\<rceil> s \<or> C s)) s)) \<sigma>
\<lbrakk>(\<delta> (\<sigma> ?i), \<delta> (\<sigma> i)) \<in> R; A (\<sigma> |\<^sub>s ?i)\<rbrakk> \<Longrightarrow> (B \<U> C) (\<sigma> |\<^sub>s ?i)
A (\<sigma> |\<^sub>s i)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(\<box>(\<lambda>s. A s \<and> \<lceil>\<lambda>s. \<delta> s = \<delta> (\<sigma> i)\<rceil> s \<longrightarrow> (B \<U> (\<lambda>s. A s \<and> \<lceil>\<lambda>s. (\<delta> s, \<delta> (\<sigma> i)) \<in> R\<rceil> s \<or> C s)) s)) \<sigma>
\<lbrakk>(\<delta> (\<sigma> ?i), \<delta> (\<sigma> i)) \<in> R; A (\<sigma> |\<^sub>s ?i)\<rbrakk> \<Longrightarrow> (B \<U> C) (\<sigma> |\<^sub>s ?i)
A (\<sigma> |\<^sub>s i)

goal (1 subgoal):
 1. (B \<U> C) (\<sigma> |\<^sub>s i)
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<box>(\<lambda>s. A s \<and> \<lceil>\<lambda>s. \<delta> s = \<delta> (\<sigma> i)\<rceil> s \<longrightarrow> (B \<U> (\<lambda>s. A s \<and> \<lceil>\<lambda>s. (\<delta> s, \<delta> (\<sigma> i)) \<in> R\<rceil> s \<or> C s)) s)) \<sigma>; \<And>i. \<lbrakk>(\<delta> (\<sigma> i), \<delta> (\<sigma> i)) \<in> R; A (\<sigma> |\<^sub>s i)\<rbrakk> \<Longrightarrow> (B \<U> C) (\<sigma> |\<^sub>s i); A (\<sigma> |\<^sub>s i)\<rbrakk> \<Longrightarrow> (B \<U> C) (\<sigma> |\<^sub>s i)
[PROOF STEP]
apply (drule alwaysD[where i=i])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>i. \<lbrakk>(\<delta> (\<sigma> i), \<delta> (\<sigma> i)) \<in> R; A (\<sigma> |\<^sub>s i)\<rbrakk> \<Longrightarrow> (B \<U> C) (\<sigma> |\<^sub>s i); A (\<sigma> |\<^sub>s i); A (\<sigma> |\<^sub>s i) \<and> \<lceil>\<lambda>s. \<delta> s = \<delta> (\<sigma> i)\<rceil> (\<sigma> |\<^sub>s i) \<longrightarrow> (B \<U> (\<lambda>s. A s \<and> \<lceil>\<lambda>s. (\<delta> s, \<delta> (\<sigma> i)) \<in> R\<rceil> s \<or> C s)) (\<sigma> |\<^sub>s i)\<rbrakk> \<Longrightarrow> (B \<U> C) (\<sigma> |\<^sub>s i)
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>i. \<lbrakk>(\<delta> (\<sigma> i), \<delta> (\<sigma> i)) \<in> R; A (\<sigma> |\<^sub>s i)\<rbrakk> \<Longrightarrow> (B \<U> C) (\<sigma> |\<^sub>s i); A (\<sigma> |\<^sub>s i); (B \<U> (\<lambda>s. A s \<and> \<lceil>\<lambda>s. (\<delta> s, \<delta> (\<sigma> i)) \<in> R\<rceil> s \<or> C s)) (\<sigma> |\<^sub>s i)\<rbrakk> \<Longrightarrow> (B \<U> C) (\<sigma> |\<^sub>s i)
[PROOF STEP]
apply (erule untilE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>\<And>i. \<lbrakk>(\<delta> (\<sigma> i), \<delta> (\<sigma> i)) \<in> R; A (\<sigma> |\<^sub>s i)\<rbrakk> \<Longrightarrow> (B \<U> C) (\<sigma> |\<^sub>s i); A (\<sigma> |\<^sub>s i); A (\<sigma> |\<^sub>s i |\<^sub>s i) \<and> \<lceil>\<lambda>s. (\<delta> s, \<delta> (\<sigma> i)) \<in> R\<rceil> (\<sigma> |\<^sub>s i |\<^sub>s i) \<or> C (\<sigma> |\<^sub>s i |\<^sub>s i); \<forall>k<i. B (\<sigma> |\<^sub>s i |\<^sub>s k)\<rbrakk> \<Longrightarrow> (B \<U> C) (\<sigma> |\<^sub>s i)
[PROOF STEP]
apply (rename_tac j)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>\<And>i. \<lbrakk>(\<delta> (\<sigma> i), \<delta> (\<sigma> i)) \<in> R; A (\<sigma> |\<^sub>s i)\<rbrakk> \<Longrightarrow> (B \<U> C) (\<sigma> |\<^sub>s i); A (\<sigma> |\<^sub>s i); A (\<sigma> |\<^sub>s i |\<^sub>s j) \<and> \<lceil>\<lambda>s. (\<delta> s, \<delta> (\<sigma> i)) \<in> R\<rceil> (\<sigma> |\<^sub>s i |\<^sub>s j) \<or> C (\<sigma> |\<^sub>s i |\<^sub>s j); \<forall>k<j. B (\<sigma> |\<^sub>s i |\<^sub>s k)\<rbrakk> \<Longrightarrow> (B \<U> C) (\<sigma> |\<^sub>s i)
[PROOF STEP]
apply (erule disjE; clarsimp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>j. \<lbrakk>\<And>i. \<lbrakk>(\<delta> (\<sigma> i), \<delta> (\<sigma> i)) \<in> R; A (\<sigma> |\<^sub>s i)\<rbrakk> \<Longrightarrow> (B \<U> C) (\<sigma> |\<^sub>s i); A (\<sigma> |\<^sub>s i); \<forall>k<j. B (\<sigma> |\<^sub>s i + k); A (\<sigma> |\<^sub>s i + j); (\<delta> (\<sigma> (i + j)), \<delta> (\<sigma> i)) \<in> R\<rbrakk> \<Longrightarrow> (B \<U> C) (\<sigma> |\<^sub>s i)
 2. \<And>j. \<lbrakk>\<And>i. \<lbrakk>(\<delta> (\<sigma> i), \<delta> (\<sigma> i)) \<in> R; A (\<sigma> |\<^sub>s i)\<rbrakk> \<Longrightarrow> (B \<U> C) (\<sigma> |\<^sub>s i); A (\<sigma> |\<^sub>s i); \<forall>k<j. B (\<sigma> |\<^sub>s i + k); C (\<sigma> |\<^sub>s i + j)\<rbrakk> \<Longrightarrow> (B \<U> C) (\<sigma> |\<^sub>s i)
[PROOF STEP]
apply (drule_tac x="i + j" in meta_spec; clarsimp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>j. \<lbrakk>A (\<sigma> |\<^sub>s i); \<forall>k<j. B (\<sigma> |\<^sub>s i + k); A (\<sigma> |\<^sub>s i + j); (\<delta> (\<sigma> (i + j)), \<delta> (\<sigma> i)) \<in> R; (B \<U> C) (\<sigma> |\<^sub>s i + j)\<rbrakk> \<Longrightarrow> (B \<U> C) (\<sigma> |\<^sub>s i)
 2. \<And>j. \<lbrakk>\<And>i. \<lbrakk>(\<delta> (\<sigma> i), \<delta> (\<sigma> i)) \<in> R; A (\<sigma> |\<^sub>s i)\<rbrakk> \<Longrightarrow> (B \<U> C) (\<sigma> |\<^sub>s i); A (\<sigma> |\<^sub>s i); \<forall>k<j. B (\<sigma> |\<^sub>s i + k); C (\<sigma> |\<^sub>s i + j)\<rbrakk> \<Longrightarrow> (B \<U> C) (\<sigma> |\<^sub>s i)
[PROOF STEP]
apply (erule untilE; clarsimp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>j i. \<lbrakk>A (\<sigma> |\<^sub>s i); \<forall>k<j. B (\<sigma> |\<^sub>s i + k); A (\<sigma> |\<^sub>s i + j); (\<delta> (\<sigma> (i + j)), \<delta> (\<sigma> i)) \<in> R; C (\<sigma> |\<^sub>s i + j + i); \<forall>k<i. B (\<sigma> |\<^sub>s i + j + k)\<rbrakk> \<Longrightarrow> (B \<U> C) (\<sigma> |\<^sub>s i)
 2. \<And>j. \<lbrakk>\<And>i. \<lbrakk>(\<delta> (\<sigma> i), \<delta> (\<sigma> i)) \<in> R; A (\<sigma> |\<^sub>s i)\<rbrakk> \<Longrightarrow> (B \<U> C) (\<sigma> |\<^sub>s i); A (\<sigma> |\<^sub>s i); \<forall>k<j. B (\<sigma> |\<^sub>s i + k); C (\<sigma> |\<^sub>s i + j)\<rbrakk> \<Longrightarrow> (B \<U> C) (\<sigma> |\<^sub>s i)
[PROOF STEP]
apply (rename_tac j k)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>j k. \<lbrakk>A (\<sigma> |\<^sub>s i); \<forall>k<j. B (\<sigma> |\<^sub>s i + k); A (\<sigma> |\<^sub>s i + j); (\<delta> (\<sigma> (i + j)), \<delta> (\<sigma> i)) \<in> R; C (\<sigma> |\<^sub>s i + j + k); \<forall>ka<k. B (\<sigma> |\<^sub>s i + j + ka)\<rbrakk> \<Longrightarrow> (B \<U> C) (\<sigma> |\<^sub>s i)
 2. \<And>j. \<lbrakk>\<And>i. \<lbrakk>(\<delta> (\<sigma> i), \<delta> (\<sigma> i)) \<in> R; A (\<sigma> |\<^sub>s i)\<rbrakk> \<Longrightarrow> (B \<U> C) (\<sigma> |\<^sub>s i); A (\<sigma> |\<^sub>s i); \<forall>k<j. B (\<sigma> |\<^sub>s i + k); C (\<sigma> |\<^sub>s i + j)\<rbrakk> \<Longrightarrow> (B \<U> C) (\<sigma> |\<^sub>s i)
[PROOF STEP]
apply (rule_tac i="j + k" in untilI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>j k. \<lbrakk>A (\<sigma> |\<^sub>s i); \<forall>k<j. B (\<sigma> |\<^sub>s i + k); A (\<sigma> |\<^sub>s i + j); (\<delta> (\<sigma> (i + j)), \<delta> (\<sigma> i)) \<in> R; C (\<sigma> |\<^sub>s i + j + k); \<forall>ka<k. B (\<sigma> |\<^sub>s i + j + ka)\<rbrakk> \<Longrightarrow> C (\<sigma> |\<^sub>s i |\<^sub>s j + k)
 2. \<And>j k. \<lbrakk>A (\<sigma> |\<^sub>s i); \<forall>k<j. B (\<sigma> |\<^sub>s i + k); A (\<sigma> |\<^sub>s i + j); (\<delta> (\<sigma> (i + j)), \<delta> (\<sigma> i)) \<in> R; C (\<sigma> |\<^sub>s i + j + k); \<forall>ka<k. B (\<sigma> |\<^sub>s i + j + ka)\<rbrakk> \<Longrightarrow> \<forall>ka<j + k. B (\<sigma> |\<^sub>s i |\<^sub>s ka)
 3. \<And>j. \<lbrakk>\<And>i. \<lbrakk>(\<delta> (\<sigma> i), \<delta> (\<sigma> i)) \<in> R; A (\<sigma> |\<^sub>s i)\<rbrakk> \<Longrightarrow> (B \<U> C) (\<sigma> |\<^sub>s i); A (\<sigma> |\<^sub>s i); \<forall>k<j. B (\<sigma> |\<^sub>s i + k); C (\<sigma> |\<^sub>s i + j)\<rbrakk> \<Longrightarrow> (B \<U> C) (\<sigma> |\<^sub>s i)
[PROOF STEP]
apply (simp add: add.assoc)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>j k. \<lbrakk>A (\<sigma> |\<^sub>s i); \<forall>k<j. B (\<sigma> |\<^sub>s i + k); A (\<sigma> |\<^sub>s i + j); (\<delta> (\<sigma> (i + j)), \<delta> (\<sigma> i)) \<in> R; C (\<sigma> |\<^sub>s i + j + k); \<forall>ka<k. B (\<sigma> |\<^sub>s i + j + ka)\<rbrakk> \<Longrightarrow> \<forall>ka<j + k. B (\<sigma> |\<^sub>s i |\<^sub>s ka)
 2. \<And>j. \<lbrakk>\<And>i. \<lbrakk>(\<delta> (\<sigma> i), \<delta> (\<sigma> i)) \<in> R; A (\<sigma> |\<^sub>s i)\<rbrakk> \<Longrightarrow> (B \<U> C) (\<sigma> |\<^sub>s i); A (\<sigma> |\<^sub>s i); \<forall>k<j. B (\<sigma> |\<^sub>s i + k); C (\<sigma> |\<^sub>s i + j)\<rbrakk> \<Longrightarrow> (B \<U> C) (\<sigma> |\<^sub>s i)
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>j k ka. \<lbrakk>A (\<sigma> |\<^sub>s i); \<forall>k<j. B (\<sigma> |\<^sub>s i + k); A (\<sigma> |\<^sub>s i + j); (\<delta> (\<sigma> (i + j)), \<delta> (\<sigma> i)) \<in> R; C (\<sigma> |\<^sub>s i + j + k); \<forall>ka<k. B (\<sigma> |\<^sub>s i + j + ka); ka < j + k\<rbrakk> \<Longrightarrow> B (\<sigma> |\<^sub>s i + ka)
 2. \<And>j. \<lbrakk>\<And>i. \<lbrakk>(\<delta> (\<sigma> i), \<delta> (\<sigma> i)) \<in> R; A (\<sigma> |\<^sub>s i)\<rbrakk> \<Longrightarrow> (B \<U> C) (\<sigma> |\<^sub>s i); A (\<sigma> |\<^sub>s i); \<forall>k<j. B (\<sigma> |\<^sub>s i + k); C (\<sigma> |\<^sub>s i + j)\<rbrakk> \<Longrightarrow> (B \<U> C) (\<sigma> |\<^sub>s i)
[PROOF STEP]
apply (metis add.assoc add.commute add_diff_inverse_nat less_diff_conv2 not_le)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>\<And>i. \<lbrakk>(\<delta> (\<sigma> i), \<delta> (\<sigma> i)) \<in> R; A (\<sigma> |\<^sub>s i)\<rbrakk> \<Longrightarrow> (B \<U> C) (\<sigma> |\<^sub>s i); A (\<sigma> |\<^sub>s i); \<forall>k<j. B (\<sigma> |\<^sub>s i + k); C (\<sigma> |\<^sub>s i + j)\<rbrakk> \<Longrightarrow> (B \<U> C) (\<sigma> |\<^sub>s i)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(B \<U> C) (\<sigma> |\<^sub>s i)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(B \<U> C) (\<sigma> |\<^sub>s i)

goal:
No subgoals!
[PROOF STEP]
qed