[STATEMENT]
lemma MStep_Exec1_Aux[rule_format]:
"(M, l, s, kb, l1, t) \<in> MStep \<Longrightarrow>
 (\<forall> hh v . (\<exists> k . (M, l, s, k, hh, v) \<in> Exec) \<longrightarrow> (\<exists> n. (M, l1, t, n, hh, v) \<in> Exec))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (M, l, s, kb, l1, t) \<in> MStep \<Longrightarrow> \<forall>hh v. (\<exists>k. (M, l, s, k, hh, v) \<in> Exec) \<longrightarrow> (\<exists>n. (M, l1, t, n, hh, v) \<in> Exec)
[PROOF STEP]
apply (erule MStep.induct)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>k t s ll l M. \<lbrakk>k = 0; t = s; ll = l\<rbrakk> \<Longrightarrow> \<forall>hh v. (\<exists>k. (M, l, s, k, hh, v) \<in> Exec) \<longrightarrow> (\<exists>n. (M, ll, t, n, hh, v) \<in> Exec)
 2. \<And>M l s n l1 r k l2 t m. \<lbrakk>(M, l, s, n, l1, r) \<in> Step; (M, l1, r, k, l2, t) \<in> MStep; \<forall>hh v. (\<exists>k. (M, l1, r, k, hh, v) \<in> Exec) \<longrightarrow> (\<exists>n. (M, l2, t, n, hh, v) \<in> Exec); m = Suc k + n\<rbrakk> \<Longrightarrow> \<forall>hh v. (\<exists>k. (M, l, s, k, hh, v) \<in> Exec) \<longrightarrow> (\<exists>n. (M, l2, t, n, hh, v) \<in> Exec)
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>M l s n l1 r k l2 t m. \<lbrakk>(M, l, s, n, l1, r) \<in> Step; (M, l1, r, k, l2, t) \<in> MStep; \<forall>hh v. (\<exists>k. (M, l1, r, k, hh, v) \<in> Exec) \<longrightarrow> (\<exists>n. (M, l2, t, n, hh, v) \<in> Exec); m = Suc k + n\<rbrakk> \<Longrightarrow> \<forall>hh v. (\<exists>k. (M, l, s, k, hh, v) \<in> Exec) \<longrightarrow> (\<exists>n. (M, l2, t, n, hh, v) \<in> Exec)
[PROOF STEP]
apply (rule, rule, rule)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>M l s n l1 r k l2 t m hh v. \<lbrakk>(M, l, s, n, l1, r) \<in> Step; (M, l1, r, k, l2, t) \<in> MStep; \<forall>hh v. (\<exists>k. (M, l1, r, k, hh, v) \<in> Exec) \<longrightarrow> (\<exists>n. (M, l2, t, n, hh, v) \<in> Exec); m = Suc k + n; \<exists>k. (M, l, s, k, hh, v) \<in> Exec\<rbrakk> \<Longrightarrow> \<exists>n. (M, l2, t, n, hh, v) \<in> Exec
[PROOF STEP]
apply (erule exE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>M l s n l1 r k l2 t m hh v ka. \<lbrakk>(M, l, s, n, l1, r) \<in> Step; (M, l1, r, k, l2, t) \<in> MStep; \<forall>hh v. (\<exists>k. (M, l1, r, k, hh, v) \<in> Exec) \<longrightarrow> (\<exists>n. (M, l2, t, n, hh, v) \<in> Exec); m = Suc k + n; (M, l, s, ka, hh, v) \<in> Exec\<rbrakk> \<Longrightarrow> \<exists>n. (M, l2, t, n, hh, v) \<in> Exec
[PROOF STEP]
apply (erule_tac x=hh in allE, erule_tac x=v in allE, erule mp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>M l s n l1 r k l2 t m hh v ka. \<lbrakk>(M, l, s, n, l1, r) \<in> Step; (M, l1, r, k, l2, t) \<in> MStep; m = Suc k + n; (M, l, s, ka, hh, v) \<in> Exec\<rbrakk> \<Longrightarrow> \<exists>k. (M, l1, r, k, hh, v) \<in> Exec
[PROOF STEP]
apply (case_tac s, clarify)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a aa b l ab ac ba n l1 ad ae bb k l2 af ag bc m hh v ka ah bd c. \<lbrakk>((a, aa, b), l, (ah, bd, c), n, l1, ad, ae, bb) \<in> Step; ((a, aa, b), l1, (ad, ae, bb), k, l2, af, ag, bc) \<in> MStep; ((a, aa, b), l, (ah, bd, c), ka, hh, v) \<in> Exec\<rbrakk> \<Longrightarrow> \<exists>k. ((a, aa, b), l1, (ad, ae, bb), k, hh, v) \<in> Exec
[PROOF STEP]
apply (drule ExecElim1, clarsimp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a aa b l n l1 ad ae bb k l2 af ag bc hh v ka ah bd c. \<lbrakk>((a, aa, b), l, (ah, bd, c), n, l1, ad, ae, bb) \<in> Step; ((a, aa, b), l1, (ad, ae, bb), k, l2, af, ag, bc) \<in> MStep; get_ins (a, aa, b) l = Some vreturn \<and> (\<exists>ops. ah = v # ops) \<and> ka = Suc 0 \<and> hh = c \<or> (\<exists>n m ab ac ba ll. ((a, aa, b), l, (ah, bd, c), n, ll, ab, ac, ba) \<in> Step \<and> ((a, aa, b), ll, (ab, ac, ba), m, hh, v) \<in> Exec \<and> ka = Suc (max n m))\<rbrakk> \<Longrightarrow> \<exists>k. ((a, aa, b), l1, (ad, ae, bb), k, hh, v) \<in> Exec
[PROOF STEP]
apply (erule disjE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a aa b l n l1 ad ae bb k l2 af ag bc hh v ka ah bd c. \<lbrakk>((a, aa, b), l, (ah, bd, c), n, l1, ad, ae, bb) \<in> Step; ((a, aa, b), l1, (ad, ae, bb), k, l2, af, ag, bc) \<in> MStep; get_ins (a, aa, b) l = Some vreturn \<and> (\<exists>ops. ah = v # ops) \<and> ka = Suc 0 \<and> hh = c\<rbrakk> \<Longrightarrow> \<exists>k. ((a, aa, b), l1, (ad, ae, bb), k, hh, v) \<in> Exec
 2. \<And>a aa b l n l1 ad ae bb k l2 af ag bc hh v ka ah bd c. \<lbrakk>((a, aa, b), l, (ah, bd, c), n, l1, ad, ae, bb) \<in> Step; ((a, aa, b), l1, (ad, ae, bb), k, l2, af, ag, bc) \<in> MStep; \<exists>n m ab ac ba ll. ((a, aa, b), l, (ah, bd, c), n, ll, ab, ac, ba) \<in> Step \<and> ((a, aa, b), ll, (ab, ac, ba), m, hh, v) \<in> Exec \<and> ka = Suc (max n m)\<rbrakk> \<Longrightarrow> \<exists>k. ((a, aa, b), l1, (ad, ae, bb), k, hh, v) \<in> Exec
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a aa b l n l1 ad ae bb k l2 af ag bc hh v bd ops. \<lbrakk>((a, aa, b), l, (v # ops, bd, hh), n, l1, ad, ae, bb) \<in> Step; ((a, aa, b), l1, (ad, ae, bb), k, l2, af, ag, bc) \<in> MStep; get_ins (a, aa, b) l = Some vreturn\<rbrakk> \<Longrightarrow> \<exists>k. ((a, aa, b), l1, (ad, ae, bb), k, hh, v) \<in> Exec
 2. \<And>a aa b l n l1 ad ae bb k l2 af ag bc hh v ka ah bd c. \<lbrakk>((a, aa, b), l, (ah, bd, c), n, l1, ad, ae, bb) \<in> Step; ((a, aa, b), l1, (ad, ae, bb), k, l2, af, ag, bc) \<in> MStep; \<exists>n m ab ac ba ll. ((a, aa, b), l, (ah, bd, c), n, ll, ab, ac, ba) \<in> Step \<and> ((a, aa, b), ll, (ab, ac, ba), m, hh, v) \<in> Exec \<and> ka = Suc (max n m)\<rbrakk> \<Longrightarrow> \<exists>k. ((a, aa, b), l1, (ad, ae, bb), k, hh, v) \<in> Exec
[PROOF STEP]
apply (drule RetElim1, simp,simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a aa b l n l1 ad ae bb k l2 af ag bc hh v ka ah bd c. \<lbrakk>((a, aa, b), l, (ah, bd, c), n, l1, ad, ae, bb) \<in> Step; ((a, aa, b), l1, (ad, ae, bb), k, l2, af, ag, bc) \<in> MStep; \<exists>n m ab ac ba ll. ((a, aa, b), l, (ah, bd, c), n, ll, ab, ac, ba) \<in> Step \<and> ((a, aa, b), ll, (ab, ac, ba), m, hh, v) \<in> Exec \<and> ka = Suc (max n m)\<rbrakk> \<Longrightarrow> \<exists>k. ((a, aa, b), l1, (ad, ae, bb), k, hh, v) \<in> Exec
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a aa b l n l1 ad ae bb k l2 af ag bc hh v ah bd c na m ab ac ba ll. \<lbrakk>((a, aa, b), l, (ah, bd, c), n, l1, ad, ae, bb) \<in> Step; ((a, aa, b), l1, (ad, ae, bb), k, l2, af, ag, bc) \<in> MStep; ((a, aa, b), l, (ah, bd, c), na, ll, ab, ac, ba) \<in> Step; ((a, aa, b), ll, (ab, ac, ba), m, hh, v) \<in> Exec\<rbrakk> \<Longrightarrow> \<exists>k. ((a, aa, b), l1, (ad, ae, bb), k, hh, v) \<in> Exec
[PROOF STEP]
apply (drule Step_determ, assumption, clarsimp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a aa b l l1 ad ae bb k l2 af ag bc hh v ah bd c na m. \<lbrakk>((a, aa, b), l1, (ad, ae, bb), k, l2, af, ag, bc) \<in> MStep; ((a, aa, b), l, (ah, bd, c), na, l1, ad, ae, bb) \<in> Step; ((a, aa, b), l1, (ad, ae, bb), m, hh, v) \<in> Exec\<rbrakk> \<Longrightarrow> \<exists>k. ((a, aa, b), l1, (ad, ae, bb), k, hh, v) \<in> Exec
[PROOF STEP]
apply (rule, assumption)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma MStep_Exec1:
  "\<lbrakk>(M, l, s, kb, l1, t) \<in> MStep; (M, l, s, k, hh, v) \<in> Exec\<rbrakk>
  \<Longrightarrow> \<exists> n. (M, l1, t, n, hh, v) \<in> Exec"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(M, l, s, kb, l1, t) \<in> MStep; (M, l, s, k, hh, v) \<in> Exec\<rbrakk> \<Longrightarrow> \<exists>n. (M, l1, t, n, hh, v) \<in> Exec
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(M, l, s, kb, l1, t) \<in> MStep; (M, l, s, k, hh, v) \<in> Exec\<rbrakk> \<Longrightarrow> \<exists>n. (M, l1, t, n, hh, v) \<in> Exec
[PROOF STEP]
by (erule MStep_Exec1_Aux, fast)


[STATEMENT]
lemma MStep_Exec2_Aux[rule_format]:
"(M, l, s, kb, l1, t) \<in> MStep \<Longrightarrow>
 (\<forall> hh v . (\<exists> k . (M, l1, t, k, hh, v) \<in> Exec) \<longrightarrow> (\<exists> n. (M, l, s, n, hh, v) \<in> Exec))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (M, l, s, kb, l1, t) \<in> MStep \<Longrightarrow> \<forall>hh v. (\<exists>k. (M, l1, t, k, hh, v) \<in> Exec) \<longrightarrow> (\<exists>n. (M, l, s, n, hh, v) \<in> Exec)
[PROOF STEP]
apply (erule MStep.induct)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>k t s ll l M. \<lbrakk>k = 0; t = s; ll = l\<rbrakk> \<Longrightarrow> \<forall>hh v. (\<exists>k. (M, ll, t, k, hh, v) \<in> Exec) \<longrightarrow> (\<exists>n. (M, l, s, n, hh, v) \<in> Exec)
 2. \<And>M l s n l1 r k l2 t m. \<lbrakk>(M, l, s, n, l1, r) \<in> Step; (M, l1, r, k, l2, t) \<in> MStep; \<forall>hh v. (\<exists>k. (M, l2, t, k, hh, v) \<in> Exec) \<longrightarrow> (\<exists>n. (M, l1, r, n, hh, v) \<in> Exec); m = Suc k + n\<rbrakk> \<Longrightarrow> \<forall>hh v. (\<exists>k. (M, l2, t, k, hh, v) \<in> Exec) \<longrightarrow> (\<exists>n. (M, l, s, n, hh, v) \<in> Exec)
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>M l s n l1 r k l2 t m. \<lbrakk>(M, l, s, n, l1, r) \<in> Step; (M, l1, r, k, l2, t) \<in> MStep; \<forall>hh v. (\<exists>k. (M, l2, t, k, hh, v) \<in> Exec) \<longrightarrow> (\<exists>n. (M, l1, r, n, hh, v) \<in> Exec); m = Suc k + n\<rbrakk> \<Longrightarrow> \<forall>hh v. (\<exists>k. (M, l2, t, k, hh, v) \<in> Exec) \<longrightarrow> (\<exists>n. (M, l, s, n, hh, v) \<in> Exec)
[PROOF STEP]
apply (rule, rule, rule)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>M l s n l1 r k l2 t m hh v. \<lbrakk>(M, l, s, n, l1, r) \<in> Step; (M, l1, r, k, l2, t) \<in> MStep; \<forall>hh v. (\<exists>k. (M, l2, t, k, hh, v) \<in> Exec) \<longrightarrow> (\<exists>n. (M, l1, r, n, hh, v) \<in> Exec); m = Suc k + n; \<exists>k. (M, l2, t, k, hh, v) \<in> Exec\<rbrakk> \<Longrightarrow> \<exists>n. (M, l, s, n, hh, v) \<in> Exec
[PROOF STEP]
apply (erule exE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>M l s n l1 r k l2 t m hh v ka. \<lbrakk>(M, l, s, n, l1, r) \<in> Step; (M, l1, r, k, l2, t) \<in> MStep; \<forall>hh v. (\<exists>k. (M, l2, t, k, hh, v) \<in> Exec) \<longrightarrow> (\<exists>n. (M, l1, r, n, hh, v) \<in> Exec); m = Suc k + n; (M, l2, t, ka, hh, v) \<in> Exec\<rbrakk> \<Longrightarrow> \<exists>n. (M, l, s, n, hh, v) \<in> Exec
[PROOF STEP]
apply (erule_tac x=hh in allE, erule_tac x=v in allE, erule impE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>M l s n l1 r k l2 t m hh v ka. \<lbrakk>(M, l, s, n, l1, r) \<in> Step; (M, l1, r, k, l2, t) \<in> MStep; m = Suc k + n; (M, l2, t, ka, hh, v) \<in> Exec\<rbrakk> \<Longrightarrow> \<exists>k. (M, l2, t, k, hh, v) \<in> Exec
 2. \<And>M l s n l1 r k l2 t m hh v ka. \<lbrakk>(M, l, s, n, l1, r) \<in> Step; (M, l1, r, k, l2, t) \<in> MStep; m = Suc k + n; (M, l2, t, ka, hh, v) \<in> Exec; \<exists>n. (M, l1, r, n, hh, v) \<in> Exec\<rbrakk> \<Longrightarrow> \<exists>n. (M, l, s, n, hh, v) \<in> Exec
[PROOF STEP]
apply (rule, assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>M l s n l1 r k l2 t m hh v ka. \<lbrakk>(M, l, s, n, l1, r) \<in> Step; (M, l1, r, k, l2, t) \<in> MStep; m = Suc k + n; (M, l2, t, ka, hh, v) \<in> Exec; \<exists>n. (M, l1, r, n, hh, v) \<in> Exec\<rbrakk> \<Longrightarrow> \<exists>n. (M, l, s, n, hh, v) \<in> Exec
[PROOF STEP]
apply (erule exE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>M l s n l1 r k l2 t m hh v ka na. \<lbrakk>(M, l, s, n, l1, r) \<in> Step; (M, l1, r, k, l2, t) \<in> MStep; m = Suc k + n; (M, l2, t, ka, hh, v) \<in> Exec; (M, l1, r, na, hh, v) \<in> Exec\<rbrakk> \<Longrightarrow> \<exists>n. (M, l, s, n, hh, v) \<in> Exec
[PROOF STEP]
apply (rule, rule Run)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>M l s n l1 r k l2 t m hh v ka na. \<lbrakk>(M, l, s, n, l1, r) \<in> Step; (M, l1, r, k, l2, t) \<in> MStep; m = Suc k + n; (M, l2, t, ka, hh, v) \<in> Exec; (M, l1, r, na, hh, v) \<in> Exec\<rbrakk> \<Longrightarrow> (M, l, s, ?n22 M l s n l1 r k l2 t m hh v ka na, ?ll22 M l s n l1 r k l2 t m hh v ka na, ?t22 M l s n l1 r k l2 t m hh v ka na) \<in> Step
 2. \<And>M l s n l1 r k l2 t m hh v ka na. \<lbrakk>(M, l, s, n, l1, r) \<in> Step; (M, l1, r, k, l2, t) \<in> MStep; m = Suc k + n; (M, l2, t, ka, hh, v) \<in> Exec; (M, l1, r, na, hh, v) \<in> Exec\<rbrakk> \<Longrightarrow> (M, ?ll22 M l s n l1 r k l2 t m hh v ka na, ?t22 M l s n l1 r k l2 t m hh v ka na, ?m22 M l s n l1 r k l2 t m hh v ka na, hh, v) \<in> Exec
 3. \<And>M l s n l1 r k l2 t m hh v ka na. \<lbrakk>(M, l, s, n, l1, r) \<in> Step; (M, l1, r, k, l2, t) \<in> MStep; m = Suc k + n; (M, l2, t, ka, hh, v) \<in> Exec; (M, l1, r, na, hh, v) \<in> Exec\<rbrakk> \<Longrightarrow> ?n20 M l s n l1 r k l2 t m hh v ka na = max (?n22 M l s n l1 r k l2 t m hh v ka na) (?m22 M l s n l1 r k l2 t m hh v ka na) + 1
[PROOF STEP]
apply assumption+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>M l s n l1 r k l2 t m hh v ka na. \<lbrakk>(M, l, s, n, l1, r) \<in> Step; (M, l1, r, k, l2, t) \<in> MStep; m = Suc k + n; (M, l2, t, ka, hh, v) \<in> Exec; (M, l1, r, na, hh, v) \<in> Exec\<rbrakk> \<Longrightarrow> ?n20 M l s n l1 r k l2 t m hh v ka na = max n na + 1
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma MStep_Exec2:
  "\<lbrakk> (M, l, s, kb, l1, t) \<in> MStep; (M, l1, t, k, hh, v) \<in> Exec\<rbrakk>
  \<Longrightarrow> \<exists> n. (M, l, s, n, hh, v) \<in> Exec"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(M, l, s, kb, l1, t) \<in> MStep; (M, l1, t, k, hh, v) \<in> Exec\<rbrakk> \<Longrightarrow> \<exists>n. (M, l, s, n, hh, v) \<in> Exec
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(M, l, s, kb, l1, t) \<in> MStep; (M, l1, t, k, hh, v) \<in> Exec\<rbrakk> \<Longrightarrow> \<exists>n. (M, l, s, n, hh, v) \<in> Exec
[PROOF STEP]
by (erule MStep_Exec2_Aux, fast)


[STATEMENT]
theorem ts_prop:
  fixes k::cnf
  shows "\<And>id. \<parallel>id\<parallel>\<^bsub>k\<^esub> \<Longrightarrow> id = the_singleton"
    and "\<parallel>the_singleton\<parallel>\<^bsub>k\<^esub>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>id. \<parallel>id\<parallel>\<^bsub>k\<^esub> \<Longrightarrow> id = the_singleton) &&& \<parallel>the_singleton\<parallel>\<^bsub>k\<^esub>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>id. \<parallel>id\<parallel>\<^bsub>k\<^esub> \<Longrightarrow> id = the_singleton
 2. \<parallel>the_singleton\<parallel>\<^bsub>k\<^esub>
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>id. \<parallel>id\<parallel>\<^bsub>k\<^esub> \<Longrightarrow> id = the_singleton
 2. \<parallel>the_singleton\<parallel>\<^bsub>k\<^esub>
[PROOF STEP]
fix id
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>id. \<parallel>id\<parallel>\<^bsub>k\<^esub> \<Longrightarrow> id = the_singleton
 2. \<parallel>the_singleton\<parallel>\<^bsub>k\<^esub>
[PROOF STEP]
assume a1: "\<parallel>id\<parallel>\<^bsub>k\<^esub>"
[PROOF STATE]
proof (state)
this:
\<parallel>id\<parallel>\<^bsub>k\<^esub>

goal (2 subgoals):
 1. \<And>id. \<parallel>id\<parallel>\<^bsub>k\<^esub> \<Longrightarrow> id = the_singleton
 2. \<parallel>the_singleton\<parallel>\<^bsub>k\<^esub>
[PROOF STEP]
have "(THE id. \<forall>k. \<forall>id'. \<parallel>id'\<parallel>\<^bsub>k\<^esub> \<longrightarrow> id' = id) = id"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (THE id. \<forall>k id'. \<parallel>id'\<parallel>\<^bsub>k\<^esub> \<longrightarrow> id' = id) = id
[PROOF STEP]
proof (rule the_equality)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<forall>k id'. \<parallel>id'\<parallel>\<^bsub>k\<^esub> \<longrightarrow> id' = id
 2. \<And>ida. \<forall>k id'. \<parallel>id'\<parallel>\<^bsub>k\<^esub> \<longrightarrow> id' = ida \<Longrightarrow> ida = id
[PROOF STEP]
show "\<forall>k id'. \<parallel>id'\<parallel>\<^bsub>k\<^esub> \<longrightarrow> id' = id"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>k id'. \<parallel>id'\<parallel>\<^bsub>k\<^esub> \<longrightarrow> id' = id
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. \<forall>id'. \<parallel>id'\<parallel>\<^bsub>k\<^esub> \<longrightarrow> id' = id
[PROOF STEP]
fix k
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. \<forall>id'. \<parallel>id'\<parallel>\<^bsub>k\<^esub> \<longrightarrow> id' = id
[PROOF STEP]
show "\<forall>id'. \<parallel>id'\<parallel>\<^bsub>k\<^esub> \<longrightarrow> id' = id"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>id'. \<parallel>id'\<parallel>\<^bsub>k\<^esub> \<longrightarrow> id' = id
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>id'. \<parallel>id'\<parallel>\<^bsub>k\<^esub> \<longrightarrow> id' = id
[PROOF STEP]
fix id'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>id'. \<parallel>id'\<parallel>\<^bsub>k\<^esub> \<longrightarrow> id' = id
[PROOF STEP]
show "\<parallel>id'\<parallel>\<^bsub>k\<^esub> \<longrightarrow> id' = id"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>id'\<parallel>\<^bsub>k\<^esub> \<longrightarrow> id' = id
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<parallel>id'\<parallel>\<^bsub>k\<^esub> \<Longrightarrow> id' = id
[PROOF STEP]
assume "\<parallel>id'\<parallel>\<^bsub>k\<^esub>"
[PROOF STATE]
proof (state)
this:
\<parallel>id'\<parallel>\<^bsub>k\<^esub>

goal (1 subgoal):
 1. \<parallel>id'\<parallel>\<^bsub>k\<^esub> \<Longrightarrow> id' = id
[PROOF STEP]
from unique
[PROOF STATE]
proof (chain)
picking this:
\<exists>id. \<forall>k id'. \<parallel>id'\<parallel>\<^bsub>k\<^esub> \<longrightarrow> id = id'
[PROOF STEP]
have "\<exists>id. \<forall>k. \<forall>id'. (\<parallel>id'\<parallel>\<^bsub>k\<^esub> \<longrightarrow> id = id')"
[PROOF STATE]
proof (prove)
using this:
\<exists>id. \<forall>k id'. \<parallel>id'\<parallel>\<^bsub>k\<^esub> \<longrightarrow> id = id'

goal (1 subgoal):
 1. \<exists>id. \<forall>k id'. \<parallel>id'\<parallel>\<^bsub>k\<^esub> \<longrightarrow> id = id'
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<exists>id. \<forall>k id'. \<parallel>id'\<parallel>\<^bsub>k\<^esub> \<longrightarrow> id = id'

goal (1 subgoal):
 1. \<parallel>id'\<parallel>\<^bsub>k\<^esub> \<Longrightarrow> id' = id
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>id. \<forall>k id'. \<parallel>id'\<parallel>\<^bsub>k\<^esub> \<longrightarrow> id = id'
[PROOF STEP]
obtain i'' where "\<forall>k. \<forall>id'. (\<parallel>id'\<parallel>\<^bsub>k\<^esub> \<longrightarrow> i'' = id')"
[PROOF STATE]
proof (prove)
using this:
\<exists>id. \<forall>k id'. \<parallel>id'\<parallel>\<^bsub>k\<^esub> \<longrightarrow> id = id'

goal (1 subgoal):
 1. (\<And>i''. \<forall>k id'. \<parallel>id'\<parallel>\<^bsub>k\<^esub> \<longrightarrow> i'' = id' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>k id'. \<parallel>id'\<parallel>\<^bsub>k\<^esub> \<longrightarrow> i'' = id'

goal (1 subgoal):
 1. \<parallel>id'\<parallel>\<^bsub>k\<^esub> \<Longrightarrow> id' = id
[PROOF STEP]
with \<open>\<parallel>id'\<parallel>\<^bsub>k\<^esub>\<close>
[PROOF STATE]
proof (chain)
picking this:
\<parallel>id'\<parallel>\<^bsub>k\<^esub>
\<forall>k id'. \<parallel>id'\<parallel>\<^bsub>k\<^esub> \<longrightarrow> i'' = id'
[PROOF STEP]
have "id=i''" and "id'=i''"
[PROOF STATE]
proof (prove)
using this:
\<parallel>id'\<parallel>\<^bsub>k\<^esub>
\<forall>k id'. \<parallel>id'\<parallel>\<^bsub>k\<^esub> \<longrightarrow> i'' = id'

goal (1 subgoal):
 1. id = i'' &&& id' = i''
[PROOF STEP]
using a1
[PROOF STATE]
proof (prove)
using this:
\<parallel>id'\<parallel>\<^bsub>k\<^esub>
\<forall>k id'. \<parallel>id'\<parallel>\<^bsub>k\<^esub> \<longrightarrow> i'' = id'
\<parallel>id\<parallel>\<^bsub>k\<^esub>

goal (1 subgoal):
 1. id = i'' &&& id' = i''
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
id = i''
id' = i''

goal (1 subgoal):
 1. \<parallel>id'\<parallel>\<^bsub>k\<^esub> \<Longrightarrow> id' = id
[PROOF STEP]
thus "id' = id"
[PROOF STATE]
proof (prove)
using this:
id = i''
id' = i''

goal (1 subgoal):
 1. id' = id
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
id' = id

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<parallel>id'\<parallel>\<^bsub>k\<^esub> \<longrightarrow> id' = id

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>id'. \<parallel>id'\<parallel>\<^bsub>k\<^esub> \<longrightarrow> id' = id

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>k id'. \<parallel>id'\<parallel>\<^bsub>k\<^esub> \<longrightarrow> id' = id

goal (1 subgoal):
 1. \<And>ida. \<forall>k id'. \<parallel>id'\<parallel>\<^bsub>k\<^esub> \<longrightarrow> id' = ida \<Longrightarrow> ida = id
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ida. \<forall>k id'. \<parallel>id'\<parallel>\<^bsub>k\<^esub> \<longrightarrow> id' = ida \<Longrightarrow> ida = id
[PROOF STEP]
fix i''
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ida. \<forall>k id'. \<parallel>id'\<parallel>\<^bsub>k\<^esub> \<longrightarrow> id' = ida \<Longrightarrow> ida = id
[PROOF STEP]
show "\<forall>k id'. \<parallel>id'\<parallel>\<^bsub>k\<^esub> \<longrightarrow> id' = i'' \<Longrightarrow> i'' = id"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>k id'. \<parallel>id'\<parallel>\<^bsub>k\<^esub> \<longrightarrow> id' = i'' \<Longrightarrow> i'' = id
[PROOF STEP]
using a1
[PROOF STATE]
proof (prove)
using this:
\<parallel>id\<parallel>\<^bsub>k\<^esub>

goal (1 subgoal):
 1. \<forall>k id'. \<parallel>id'\<parallel>\<^bsub>k\<^esub> \<longrightarrow> id' = i'' \<Longrightarrow> i'' = id
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>k id'. \<parallel>id'\<parallel>\<^bsub>k\<^esub> \<longrightarrow> id' = i'' \<Longrightarrow> i'' = id

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(THE id. \<forall>k id'. \<parallel>id'\<parallel>\<^bsub>k\<^esub> \<longrightarrow> id' = id) = id

goal (2 subgoals):
 1. \<And>id. \<parallel>id\<parallel>\<^bsub>k\<^esub> \<Longrightarrow> id = the_singleton
 2. \<parallel>the_singleton\<parallel>\<^bsub>k\<^esub>
[PROOF STEP]
hence "\<parallel>id\<parallel>\<^bsub>k\<^esub> \<Longrightarrow> id = the_singleton"
[PROOF STATE]
proof (prove)
using this:
(THE id. \<forall>k id'. \<parallel>id'\<parallel>\<^bsub>k\<^esub> \<longrightarrow> id' = id) = id

goal (1 subgoal):
 1. \<parallel>id\<parallel>\<^bsub>k\<^esub> \<Longrightarrow> id = the_singleton
[PROOF STEP]
by (simp add: the_singleton_def)
[PROOF STATE]
proof (state)
this:
\<parallel>id\<parallel>\<^bsub>k\<^esub> \<Longrightarrow> id = the_singleton

goal (2 subgoals):
 1. \<And>id. \<parallel>id\<parallel>\<^bsub>k\<^esub> \<Longrightarrow> id = the_singleton
 2. \<parallel>the_singleton\<parallel>\<^bsub>k\<^esub>
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<parallel>?id4\<parallel>\<^bsub>k\<^esub>; \<parallel>?id4\<parallel>\<^bsub>k\<^esub>\<rbrakk> \<Longrightarrow> ?id4 = the_singleton

goal (2 subgoals):
 1. \<And>id. \<parallel>id\<parallel>\<^bsub>k\<^esub> \<Longrightarrow> id = the_singleton
 2. \<parallel>the_singleton\<parallel>\<^bsub>k\<^esub>
[PROOF STEP]
note g1 = this
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<parallel>?id4\<parallel>\<^bsub>k\<^esub>; \<parallel>?id4\<parallel>\<^bsub>k\<^esub>\<rbrakk> \<Longrightarrow> ?id4 = the_singleton

goal (2 subgoals):
 1. \<And>id. \<parallel>id\<parallel>\<^bsub>k\<^esub> \<Longrightarrow> id = the_singleton
 2. \<parallel>the_singleton\<parallel>\<^bsub>k\<^esub>
[PROOF STEP]
thus "\<And>id. \<parallel>id\<parallel>\<^bsub>k\<^esub> \<Longrightarrow> id = the_singleton"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<parallel>?id4\<parallel>\<^bsub>k\<^esub>; \<parallel>?id4\<parallel>\<^bsub>k\<^esub>\<rbrakk> \<Longrightarrow> ?id4 = the_singleton

goal (1 subgoal):
 1. \<And>id. \<parallel>id\<parallel>\<^bsub>k\<^esub> \<Longrightarrow> id = the_singleton
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<parallel>?id2\<parallel>\<^bsub>k\<^esub> \<Longrightarrow> ?id2 = the_singleton

goal (1 subgoal):
 1. \<parallel>the_singleton\<parallel>\<^bsub>k\<^esub>
[PROOF STEP]
from alwaysActive
[PROOF STATE]
proof (chain)
picking this:
\<exists>id. \<parallel>id\<parallel>\<^bsub>?k\<^esub>
[PROOF STEP]
obtain id where "\<parallel>id\<parallel>\<^bsub>k\<^esub>"
[PROOF STATE]
proof (prove)
using this:
\<exists>id. \<parallel>id\<parallel>\<^bsub>?k\<^esub>

goal (1 subgoal):
 1. (\<And>id. \<parallel>id\<parallel>\<^bsub>k\<^esub> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<parallel>id\<parallel>\<^bsub>k\<^esub>

goal (1 subgoal):
 1. \<parallel>the_singleton\<parallel>\<^bsub>k\<^esub>
[PROOF STEP]
with g1
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<parallel>?id4\<parallel>\<^bsub>k\<^esub>; \<parallel>?id4\<parallel>\<^bsub>k\<^esub>\<rbrakk> \<Longrightarrow> ?id4 = the_singleton
\<parallel>id\<parallel>\<^bsub>k\<^esub>
[PROOF STEP]
have "id = the_singleton"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<parallel>?id4\<parallel>\<^bsub>k\<^esub>; \<parallel>?id4\<parallel>\<^bsub>k\<^esub>\<rbrakk> \<Longrightarrow> ?id4 = the_singleton
\<parallel>id\<parallel>\<^bsub>k\<^esub>

goal (1 subgoal):
 1. id = the_singleton
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
id = the_singleton

goal (1 subgoal):
 1. \<parallel>the_singleton\<parallel>\<^bsub>k\<^esub>
[PROOF STEP]
with \<open>\<parallel>id\<parallel>\<^bsub>k\<^esub>\<close>
[PROOF STATE]
proof (chain)
picking this:
\<parallel>id\<parallel>\<^bsub>k\<^esub>
id = the_singleton
[PROOF STEP]
show "\<parallel>the_singleton\<parallel>\<^bsub>k\<^esub>"
[PROOF STATE]
proof (prove)
using this:
\<parallel>id\<parallel>\<^bsub>k\<^esub>
id = the_singleton

goal (1 subgoal):
 1. \<parallel>the_singleton\<parallel>\<^bsub>k\<^esub>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<parallel>the_singleton\<parallel>\<^bsub>k\<^esub>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lNact_active[simp]:
  fixes cid t n
  shows "\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n\<^esub> = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n\<^esub> = n
[PROOF STEP]
using lNact_active ts_prop(2)
[PROOF STATE]
proof (prove)
using this:
\<forall>k<?n. \<parallel>?cid\<parallel>\<^bsub>?t k\<^esub> \<Longrightarrow> \<langle>?cid \<Leftarrow> ?t\<rangle>\<^bsub>?n\<^esub> = ?n
\<parallel>the_singleton\<parallel>\<^bsub>?k\<^esub>

goal (1 subgoal):
 1. \<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n\<^esub> = n
[PROOF STEP]
by auto


[STATEMENT]
lemma lNxt_active[simp]:
  fixes cid t n
  shows "\<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n\<^esub> = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n\<^esub> = n
[PROOF STEP]
by (simp add: nxtAct_active)


[STATEMENT]
lemma baI[intro]:
  fixes t n a
  assumes "\<phi> (\<sigma>\<^bsub>the_singleton\<^esub>(t n))"
  shows "eval the_singleton t t' n [\<phi>]\<^sub>b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval the_singleton t t' n [\<phi>]\<^sub>b
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<phi> (\<sigma>\<^bsub>the_singleton\<^esub>t n)

goal (1 subgoal):
 1. eval the_singleton t t' n [\<phi>]\<^sub>b
[PROOF STEP]
by (simp add: baIANow)


[STATEMENT]
lemma baE[elim]:
  fixes t n a
  assumes "eval the_singleton t t' n [\<phi>]\<^sub>b"
  shows "\<phi> (\<sigma>\<^bsub>the_singleton\<^esub>(t n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> (\<sigma>\<^bsub>the_singleton\<^esub>t n)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
eval the_singleton t t' n [\<phi>]\<^sub>b

goal (1 subgoal):
 1. \<phi> (\<sigma>\<^bsub>the_singleton\<^esub>t n)
[PROOF STEP]
by (simp add: baEANow)


[STATEMENT]
lemma evtE[elim]:
  fixes t id n a
  assumes "eval the_singleton t t' n (\<diamond>\<^sub>b \<gamma>)"
  shows "\<exists>n'\<ge>n. eval the_singleton t t' n' \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>n'\<ge>n. eval the_singleton t t' n' \<gamma>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>n'\<ge>n. eval the_singleton t t' n' \<gamma>
[PROOF STEP]
have "\<parallel>the_singleton\<parallel>\<^bsub>t n\<^esub>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>the_singleton\<parallel>\<^bsub>t n\<^esub>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<parallel>the_singleton\<parallel>\<^bsub>t n\<^esub>

goal (1 subgoal):
 1. \<exists>n'\<ge>n. eval the_singleton t t' n' \<gamma>
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
eval the_singleton t t' n (\<diamond>\<^sub>b\<gamma>)
\<parallel>the_singleton\<parallel>\<^bsub>t n\<^esub>
[PROOF STEP]
obtain n' where "n'\<ge>\<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n\<^esub>" and "(\<exists>i\<ge>n'. \<parallel>the_singleton\<parallel>\<^bsub>t i\<^esub> \<and>
    (\<forall>n''\<ge>\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub>. n'' \<le> \<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n'\<^esub> \<longrightarrow> eval the_singleton t t' n'' \<gamma>)) \<or>
    \<not> (\<exists>i\<ge>n'. \<parallel>the_singleton\<parallel>\<^bsub>t i\<^esub>) \<and> eval the_singleton t t' n' \<gamma>"
[PROOF STATE]
proof (prove)
using this:
eval the_singleton t t' n (\<diamond>\<^sub>b\<gamma>)
\<parallel>the_singleton\<parallel>\<^bsub>t n\<^esub>

goal (1 subgoal):
 1. (\<And>n'. \<lbrakk>\<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n\<^esub> \<le> n'; (\<exists>i\<ge>n'. \<parallel>the_singleton\<parallel>\<^bsub>t i\<^esub> \<and> (\<forall>n''\<ge>\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub>. n'' \<le> \<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n'\<^esub> \<longrightarrow> eval the_singleton t t' n'' \<gamma>)) \<or> \<not> (\<exists>i\<ge>n'. \<parallel>the_singleton\<parallel>\<^bsub>t i\<^esub>) \<and> eval the_singleton t t' n' \<gamma>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using evtEA[of n "the_singleton" t]
[PROOF STATE]
proof (prove)
using this:
eval the_singleton t t' n (\<diamond>\<^sub>b\<gamma>)
\<parallel>the_singleton\<parallel>\<^bsub>t n\<^esub>
\<lbrakk>\<exists>i\<ge>n. \<parallel>the_singleton\<parallel>\<^bsub>t i\<^esub>; eval the_singleton t ?t' n (\<diamond>\<^sub>b?\<gamma>)\<rbrakk> \<Longrightarrow> \<exists>n'\<ge>\<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. (\<exists>i\<ge>n'. \<parallel>the_singleton\<parallel>\<^bsub>t i\<^esub> \<and> (\<forall>n''\<ge>\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub>. n'' \<le> \<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n'\<^esub> \<longrightarrow> eval the_singleton t ?t' n'' ?\<gamma>)) \<or> \<not> (\<exists>i\<ge>n'. \<parallel>the_singleton\<parallel>\<^bsub>t i\<^esub>) \<and> eval the_singleton t ?t' n' ?\<gamma>

goal (1 subgoal):
 1. (\<And>n'. \<lbrakk>\<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n\<^esub> \<le> n'; (\<exists>i\<ge>n'. \<parallel>the_singleton\<parallel>\<^bsub>t i\<^esub> \<and> (\<forall>n''\<ge>\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub>. n'' \<le> \<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n'\<^esub> \<longrightarrow> eval the_singleton t t' n'' \<gamma>)) \<or> \<not> (\<exists>i\<ge>n'. \<parallel>the_singleton\<parallel>\<^bsub>t i\<^esub>) \<and> eval the_singleton t t' n' \<gamma>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n\<^esub> \<le> n'
(\<exists>i\<ge>n'. \<parallel>the_singleton\<parallel>\<^bsub>t i\<^esub> \<and> (\<forall>n''\<ge>\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub>. n'' \<le> \<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n'\<^esub> \<longrightarrow> eval the_singleton t t' n'' \<gamma>)) \<or> \<not> (\<exists>i\<ge>n'. \<parallel>the_singleton\<parallel>\<^bsub>t i\<^esub>) \<and> eval the_singleton t t' n' \<gamma>

goal (1 subgoal):
 1. \<exists>n'\<ge>n. eval the_singleton t t' n' \<gamma>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n\<^esub> \<le> n'
(\<exists>i\<ge>n'. \<parallel>the_singleton\<parallel>\<^bsub>t i\<^esub> \<and> (\<forall>n''\<ge>\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub>. n'' \<le> \<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n'\<^esub> \<longrightarrow> eval the_singleton t t' n'' \<gamma>)) \<or> \<not> (\<exists>i\<ge>n'. \<parallel>the_singleton\<parallel>\<^bsub>t i\<^esub>) \<and> eval the_singleton t t' n' \<gamma>

goal (1 subgoal):
 1. \<exists>n'\<ge>n. eval the_singleton t t' n' \<gamma>
[PROOF STEP]
have "\<parallel>the_singleton\<parallel>\<^bsub>t n'\<^esub>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>the_singleton\<parallel>\<^bsub>t n'\<^esub>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<parallel>the_singleton\<parallel>\<^bsub>t n'\<^esub>

goal (1 subgoal):
 1. \<exists>n'\<ge>n. eval the_singleton t t' n' \<gamma>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n\<^esub> \<le> n'
(\<exists>i\<ge>n'. \<parallel>the_singleton\<parallel>\<^bsub>t i\<^esub> \<and> (\<forall>n''\<ge>\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub>. n'' \<le> \<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n'\<^esub> \<longrightarrow> eval the_singleton t t' n'' \<gamma>)) \<or> \<not> (\<exists>i\<ge>n'. \<parallel>the_singleton\<parallel>\<^bsub>t i\<^esub>) \<and> eval the_singleton t t' n' \<gamma>
\<parallel>the_singleton\<parallel>\<^bsub>t n'\<^esub>
[PROOF STEP]
have
    "\<forall>n''\<ge>\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub>. n'' \<le> \<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n'\<^esub> \<longrightarrow> eval the_singleton t t' n'' \<gamma>"
[PROOF STATE]
proof (prove)
using this:
\<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n\<^esub> \<le> n'
(\<exists>i\<ge>n'. \<parallel>the_singleton\<parallel>\<^bsub>t i\<^esub> \<and> (\<forall>n''\<ge>\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub>. n'' \<le> \<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n'\<^esub> \<longrightarrow> eval the_singleton t t' n'' \<gamma>)) \<or> \<not> (\<exists>i\<ge>n'. \<parallel>the_singleton\<parallel>\<^bsub>t i\<^esub>) \<and> eval the_singleton t t' n' \<gamma>
\<parallel>the_singleton\<parallel>\<^bsub>t n'\<^esub>

goal (1 subgoal):
 1. \<forall>n''\<ge>\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub>. n'' \<le> \<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n'\<^esub> \<longrightarrow> eval the_singleton t t' n'' \<gamma>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>n''\<ge>\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub>. n'' \<le> \<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n'\<^esub> \<longrightarrow> eval the_singleton t t' n'' \<gamma>

goal (1 subgoal):
 1. \<exists>n'\<ge>n. eval the_singleton t t' n' \<gamma>
[PROOF STEP]
hence "eval the_singleton t t' n' \<gamma>"
[PROOF STATE]
proof (prove)
using this:
\<forall>n''\<ge>\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub>. n'' \<le> \<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n'\<^esub> \<longrightarrow> eval the_singleton t t' n'' \<gamma>

goal (1 subgoal):
 1. eval the_singleton t t' n' \<gamma>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval the_singleton t t' n' \<gamma>

goal (1 subgoal):
 1. \<exists>n'\<ge>n. eval the_singleton t t' n' \<gamma>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
eval the_singleton t t' n' \<gamma>

goal (1 subgoal):
 1. \<exists>n'\<ge>n. eval the_singleton t t' n' \<gamma>
[PROOF STEP]
from \<open>n'\<ge>\<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<close>
[PROOF STATE]
proof (chain)
picking this:
\<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n\<^esub> \<le> n'
[PROOF STEP]
have "n'\<ge>n"
[PROOF STATE]
proof (prove)
using this:
\<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n\<^esub> \<le> n'

goal (1 subgoal):
 1. n \<le> n'
[PROOF STEP]
by (simp add: nxtAct_active)
[PROOF STATE]
proof (state)
this:
n \<le> n'

goal (1 subgoal):
 1. \<exists>n'\<ge>n. eval the_singleton t t' n' \<gamma>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
eval the_singleton t t' n' \<gamma>
n \<le> n'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
eval the_singleton t t' n' \<gamma>
n \<le> n'

goal (1 subgoal):
 1. \<exists>n'\<ge>n. eval the_singleton t t' n' \<gamma>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>n'\<ge>n. eval the_singleton t t' n' \<gamma>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma globE[elim]:
  fixes t id n a
  assumes "eval the_singleton t t' n (\<box>\<^sub>b \<gamma>)"
  shows "\<forall>n'\<ge>n. eval the_singleton t t' n' \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n'\<ge>n. eval the_singleton t t' n' \<gamma>
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n'. n \<le> n' \<longrightarrow> eval the_singleton t t' n' \<gamma>
[PROOF STEP]
fix n'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n'. n \<le> n' \<longrightarrow> eval the_singleton t t' n' \<gamma>
[PROOF STEP]
show "n \<le> n' \<longrightarrow> eval the_singleton t t' n' \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<le> n' \<longrightarrow> eval the_singleton t t' n' \<gamma>
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n \<le> n' \<Longrightarrow> eval the_singleton t t' n' \<gamma>
[PROOF STEP]
assume "n\<le>n'"
[PROOF STATE]
proof (state)
this:
n \<le> n'

goal (1 subgoal):
 1. n \<le> n' \<Longrightarrow> eval the_singleton t t' n' \<gamma>
[PROOF STEP]
hence "\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n\<^esub> \<le> n'"
[PROOF STATE]
proof (prove)
using this:
n \<le> n'

goal (1 subgoal):
 1. \<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n\<^esub> \<le> n'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n\<^esub> \<le> n'

goal (1 subgoal):
 1. n \<le> n' \<Longrightarrow> eval the_singleton t t' n' \<gamma>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n\<^esub> \<le> n'

goal (1 subgoal):
 1. n \<le> n' \<Longrightarrow> eval the_singleton t t' n' \<gamma>
[PROOF STEP]
have "\<parallel>the_singleton\<parallel>\<^bsub>t n\<^esub>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>the_singleton\<parallel>\<^bsub>t n\<^esub>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<parallel>the_singleton\<parallel>\<^bsub>t n\<^esub>

goal (1 subgoal):
 1. n \<le> n' \<Longrightarrow> eval the_singleton t t' n' \<gamma>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n\<^esub> \<le> n'
\<parallel>the_singleton\<parallel>\<^bsub>t n\<^esub>
[PROOF STEP]
show "eval the_singleton t t' n' \<gamma>"
[PROOF STATE]
proof (prove)
using this:
\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n\<^esub> \<le> n'
\<parallel>the_singleton\<parallel>\<^bsub>t n\<^esub>

goal (1 subgoal):
 1. eval the_singleton t t' n' \<gamma>
[PROOF STEP]
using \<open>eval the_singleton t t' n (\<box>\<^sub>b \<gamma>)\<close> globEA
[PROOF STATE]
proof (prove)
using this:
\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n\<^esub> \<le> n'
\<parallel>the_singleton\<parallel>\<^bsub>t n\<^esub>
eval the_singleton t t' n (\<box>\<^sub>b\<gamma>)
\<lbrakk>\<exists>i\<ge>?n. \<parallel>?c\<parallel>\<^bsub>?t i\<^esub>; eval ?c ?t ?t' ?n (\<box>\<^sub>b?\<gamma>); \<langle>?c \<Leftarrow> ?t\<rangle>\<^bsub>?n\<^esub> \<le> ?n'\<rbrakk> \<Longrightarrow> eval ?c ?t ?t' ?n' ?\<gamma>

goal (1 subgoal):
 1. eval the_singleton t t' n' \<gamma>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
eval the_singleton t t' n' \<gamma>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
n \<le> n' \<longrightarrow> eval the_singleton t t' n' \<gamma>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma untilI[intro]:
  fixes t::"nat \<Rightarrow> cnf"
    and t'::"nat \<Rightarrow> 'cmp"
    and n::nat
    and n'::nat
  assumes "n'\<ge>n"
    and "eval the_singleton t t' n' \<gamma>"
    and "\<And>n''. \<lbrakk>n\<le>n''; n''<n'\<rbrakk> \<Longrightarrow> eval the_singleton t t' n'' \<gamma>'"
  shows "eval the_singleton t t' n (\<gamma>' \<UU>\<^sub>b \<gamma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval the_singleton t t' n (\<gamma>' \<UU>\<^sub>b \<gamma>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eval the_singleton t t' n (\<gamma>' \<UU>\<^sub>b \<gamma>)
[PROOF STEP]
have "\<parallel>the_singleton\<parallel>\<^bsub>t n\<^esub>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>the_singleton\<parallel>\<^bsub>t n\<^esub>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<parallel>the_singleton\<parallel>\<^bsub>t n\<^esub>

goal (1 subgoal):
 1. eval the_singleton t t' n (\<gamma>' \<UU>\<^sub>b \<gamma>)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<parallel>the_singleton\<parallel>\<^bsub>t n\<^esub>

goal (1 subgoal):
 1. eval the_singleton t t' n (\<gamma>' \<UU>\<^sub>b \<gamma>)
[PROOF STEP]
from \<open>n'\<ge>n\<close>
[PROOF STATE]
proof (chain)
picking this:
n \<le> n'
[PROOF STEP]
have "\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n\<^esub> \<le> n'"
[PROOF STATE]
proof (prove)
using this:
n \<le> n'

goal (1 subgoal):
 1. \<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n\<^esub> \<le> n'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n\<^esub> \<le> n'

goal (1 subgoal):
 1. eval the_singleton t t' n (\<gamma>' \<UU>\<^sub>b \<gamma>)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n\<^esub> \<le> n'

goal (1 subgoal):
 1. eval the_singleton t t' n (\<gamma>' \<UU>\<^sub>b \<gamma>)
[PROOF STEP]
have "\<parallel>the_singleton\<parallel>\<^bsub>t n'\<^esub>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>the_singleton\<parallel>\<^bsub>t n'\<^esub>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<parallel>the_singleton\<parallel>\<^bsub>t n'\<^esub>

goal (1 subgoal):
 1. eval the_singleton t t' n (\<gamma>' \<UU>\<^sub>b \<gamma>)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<parallel>the_singleton\<parallel>\<^bsub>t n'\<^esub>

goal (1 subgoal):
 1. eval the_singleton t t' n (\<gamma>' \<UU>\<^sub>b \<gamma>)
[PROOF STEP]
have
    "\<exists>n''\<ge>\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub>. n'' \<le> \<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n'\<^esub> \<and> eval the_singleton t t' n'' \<gamma> \<and>
    (\<forall>n'''\<ge>\<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. n''' < \<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n''\<^esub> \<longrightarrow>
      (\<exists>n''''\<ge>\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n'''\<^esub>. n'''' \<le> \<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n'''\<^esub> \<and> eval the_singleton t t' n'''' \<gamma>'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>n''\<ge>\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub>. n'' \<le> \<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n'\<^esub> \<and> eval the_singleton t t' n'' \<gamma> \<and> (\<forall>n'''\<ge>\<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. n''' < \<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n''\<^esub> \<longrightarrow> (\<exists>n''''\<ge>\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n'''\<^esub>. n'''' \<le> \<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n'''\<^esub> \<and> eval the_singleton t t' n'''' \<gamma>'))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>n''\<ge>\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub>. n'' \<le> \<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n'\<^esub> \<and> eval the_singleton t t' n'' \<gamma> \<and> (\<forall>n'''\<ge>\<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. n''' < \<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n''\<^esub> \<longrightarrow> (\<exists>n''''\<ge>\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n'''\<^esub>. n'''' \<le> \<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n'''\<^esub> \<and> eval the_singleton t t' n'''' \<gamma>'))
[PROOF STEP]
have "n'\<ge>\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub> \<le> n'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub> \<le> n'

goal (1 subgoal):
 1. \<exists>n''\<ge>\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub>. n'' \<le> \<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n'\<^esub> \<and> eval the_singleton t t' n'' \<gamma> \<and> (\<forall>n'''\<ge>\<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. n''' < \<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n''\<^esub> \<longrightarrow> (\<exists>n''''\<ge>\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n'''\<^esub>. n'''' \<le> \<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n'''\<^esub> \<and> eval the_singleton t t' n'''' \<gamma>'))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub> \<le> n'

goal (1 subgoal):
 1. \<exists>n''\<ge>\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub>. n'' \<le> \<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n'\<^esub> \<and> eval the_singleton t t' n'' \<gamma> \<and> (\<forall>n'''\<ge>\<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. n''' < \<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n''\<^esub> \<longrightarrow> (\<exists>n''''\<ge>\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n'''\<^esub>. n'''' \<le> \<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n'''\<^esub> \<and> eval the_singleton t t' n'''' \<gamma>'))
[PROOF STEP]
have "n' \<le> \<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n'\<^esub>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n' \<le> \<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n'\<^esub>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
n' \<le> \<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n'\<^esub>

goal (1 subgoal):
 1. \<exists>n''\<ge>\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub>. n'' \<le> \<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n'\<^esub> \<and> eval the_singleton t t' n'' \<gamma> \<and> (\<forall>n'''\<ge>\<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. n''' < \<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n''\<^esub> \<longrightarrow> (\<exists>n''''\<ge>\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n'''\<^esub>. n'''' \<le> \<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n'''\<^esub> \<and> eval the_singleton t t' n'''' \<gamma>'))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
n' \<le> \<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n'\<^esub>

goal (1 subgoal):
 1. \<exists>n''\<ge>\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub>. n'' \<le> \<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n'\<^esub> \<and> eval the_singleton t t' n'' \<gamma> \<and> (\<forall>n'''\<ge>\<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. n''' < \<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n''\<^esub> \<longrightarrow> (\<exists>n''''\<ge>\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n'''\<^esub>. n'''' \<le> \<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n'''\<^esub> \<and> eval the_singleton t t' n'''' \<gamma>'))
[PROOF STEP]
from assms(3)
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>n \<le> ?n''2; ?n''2 < n'\<rbrakk> \<Longrightarrow> eval the_singleton t t' ?n''2 \<gamma>'
[PROOF STEP]
have "(\<forall>n''\<ge>\<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. n'' < \<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub> \<longrightarrow>
      (\<exists>n'''\<ge>\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n''\<^esub>. n''' \<le> \<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n''\<^esub> \<and> eval the_singleton t t' n''' \<gamma>'))"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>n \<le> ?n''2; ?n''2 < n'\<rbrakk> \<Longrightarrow> eval the_singleton t t' ?n''2 \<gamma>'

goal (1 subgoal):
 1. \<forall>n''\<ge>\<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. n'' < \<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub> \<longrightarrow> (\<exists>n'''\<ge>\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n''\<^esub>. n''' \<le> \<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n''\<^esub> \<and> eval the_singleton t t' n''' \<gamma>')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>n''\<ge>\<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. n'' < \<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub> \<longrightarrow> (\<exists>n'''\<ge>\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n''\<^esub>. n''' \<le> \<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n''\<^esub> \<and> eval the_singleton t t' n''' \<gamma>')

goal (1 subgoal):
 1. \<exists>n''\<ge>\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub>. n'' \<le> \<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n'\<^esub> \<and> eval the_singleton t t' n'' \<gamma> \<and> (\<forall>n'''\<ge>\<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. n''' < \<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n''\<^esub> \<longrightarrow> (\<exists>n''''\<ge>\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n'''\<^esub>. n'''' \<le> \<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n'''\<^esub> \<and> eval the_singleton t t' n'''' \<gamma>'))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub> \<le> n'
n' \<le> \<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n'\<^esub>
\<forall>n''\<ge>\<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. n'' < \<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub> \<longrightarrow> (\<exists>n'''\<ge>\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n''\<^esub>. n''' \<le> \<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n''\<^esub> \<and> eval the_singleton t t' n''' \<gamma>')
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub> \<le> n'
n' \<le> \<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n'\<^esub>
\<forall>n''\<ge>\<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. n'' < \<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub> \<longrightarrow> (\<exists>n'''\<ge>\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n''\<^esub>. n''' \<le> \<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n''\<^esub> \<and> eval the_singleton t t' n''' \<gamma>')

goal (1 subgoal):
 1. \<exists>n''\<ge>\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub>. n'' \<le> \<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n'\<^esub> \<and> eval the_singleton t t' n'' \<gamma> \<and> (\<forall>n'''\<ge>\<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. n''' < \<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n''\<^esub> \<longrightarrow> (\<exists>n''''\<ge>\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n'''\<^esub>. n'''' \<le> \<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n'''\<^esub> \<and> eval the_singleton t t' n'''' \<gamma>'))
[PROOF STEP]
using \<open>eval the_singleton t t' n' \<gamma>\<close>
[PROOF STATE]
proof (prove)
using this:
\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub> \<le> n'
n' \<le> \<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n'\<^esub>
\<forall>n''\<ge>\<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. n'' < \<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub> \<longrightarrow> (\<exists>n'''\<ge>\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n''\<^esub>. n''' \<le> \<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n''\<^esub> \<and> eval the_singleton t t' n''' \<gamma>')
eval the_singleton t t' n' \<gamma>

goal (1 subgoal):
 1. \<exists>n''\<ge>\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub>. n'' \<le> \<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n'\<^esub> \<and> eval the_singleton t t' n'' \<gamma> \<and> (\<forall>n'''\<ge>\<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. n''' < \<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n''\<^esub> \<longrightarrow> (\<exists>n''''\<ge>\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n'''\<^esub>. n'''' \<le> \<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n'''\<^esub> \<and> eval the_singleton t t' n'''' \<gamma>'))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>n''\<ge>\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub>. n'' \<le> \<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n'\<^esub> \<and> eval the_singleton t t' n'' \<gamma> \<and> (\<forall>n'''\<ge>\<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. n''' < \<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n''\<^esub> \<longrightarrow> (\<exists>n''''\<ge>\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n'''\<^esub>. n'''' \<le> \<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n'''\<^esub> \<and> eval the_singleton t t' n'''' \<gamma>'))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>n''\<ge>\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub>. n'' \<le> \<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n'\<^esub> \<and> eval the_singleton t t' n'' \<gamma> \<and> (\<forall>n'''\<ge>\<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. n''' < \<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n''\<^esub> \<longrightarrow> (\<exists>n''''\<ge>\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n'''\<^esub>. n'''' \<le> \<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n'''\<^esub> \<and> eval the_singleton t t' n'''' \<gamma>'))

goal (1 subgoal):
 1. eval the_singleton t t' n (\<gamma>' \<UU>\<^sub>b \<gamma>)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<parallel>the_singleton\<parallel>\<^bsub>t n\<^esub>
\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n\<^esub> \<le> n'
\<parallel>the_singleton\<parallel>\<^bsub>t n'\<^esub>
\<exists>n''\<ge>\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub>. n'' \<le> \<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n'\<^esub> \<and> eval the_singleton t t' n'' \<gamma> \<and> (\<forall>n'''\<ge>\<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. n''' < \<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n''\<^esub> \<longrightarrow> (\<exists>n''''\<ge>\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n'''\<^esub>. n'''' \<le> \<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n'''\<^esub> \<and> eval the_singleton t t' n'''' \<gamma>'))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<parallel>the_singleton\<parallel>\<^bsub>t n\<^esub>
\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n\<^esub> \<le> n'
\<parallel>the_singleton\<parallel>\<^bsub>t n'\<^esub>
\<exists>n''\<ge>\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub>. n'' \<le> \<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n'\<^esub> \<and> eval the_singleton t t' n'' \<gamma> \<and> (\<forall>n'''\<ge>\<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. n''' < \<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n''\<^esub> \<longrightarrow> (\<exists>n''''\<ge>\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n'''\<^esub>. n'''' \<le> \<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n'''\<^esub> \<and> eval the_singleton t t' n'''' \<gamma>'))

goal (1 subgoal):
 1. eval the_singleton t t' n (\<gamma>' \<UU>\<^sub>b \<gamma>)
[PROOF STEP]
using untilIA[of n "the_singleton" t n' t' \<gamma> \<gamma>']
[PROOF STATE]
proof (prove)
using this:
\<parallel>the_singleton\<parallel>\<^bsub>t n\<^esub>
\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n\<^esub> \<le> n'
\<parallel>the_singleton\<parallel>\<^bsub>t n'\<^esub>
\<exists>n''\<ge>\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub>. n'' \<le> \<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n'\<^esub> \<and> eval the_singleton t t' n'' \<gamma> \<and> (\<forall>n'''\<ge>\<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. n''' < \<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n''\<^esub> \<longrightarrow> (\<exists>n''''\<ge>\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n'''\<^esub>. n'''' \<le> \<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n'''\<^esub> \<and> eval the_singleton t t' n'''' \<gamma>'))
\<lbrakk>\<exists>i\<ge>n. \<parallel>the_singleton\<parallel>\<^bsub>t i\<^esub>; \<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n\<^esub> \<le> n'; \<exists>i\<ge>n'. \<parallel>the_singleton\<parallel>\<^bsub>t i\<^esub> \<Longrightarrow> \<exists>n''\<ge>\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub>. n'' \<le> \<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n'\<^esub> \<and> eval the_singleton t t' n'' \<gamma> \<and> (\<forall>n'''\<ge>\<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. n''' < \<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n''\<^esub> \<longrightarrow> (\<exists>n''''\<ge>\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n'''\<^esub>. n'''' \<le> \<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n'''\<^esub> \<and> eval the_singleton t t' n'''' \<gamma>')); \<not> (\<exists>i\<ge>n'. \<parallel>the_singleton\<parallel>\<^bsub>t i\<^esub>) \<Longrightarrow> eval the_singleton t t' n' \<gamma> \<and> (\<forall>n''\<ge>\<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. n'' < n' \<longrightarrow> (\<exists>i\<ge>n''. \<parallel>the_singleton\<parallel>\<^bsub>t i\<^esub>) \<and> (\<exists>n'''\<ge>\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n''\<^esub>. n''' \<le> \<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n''\<^esub> \<and> eval the_singleton t t' n''' \<gamma>') \<or> \<not> (\<exists>i\<ge>n''. \<parallel>the_singleton\<parallel>\<^bsub>t i\<^esub>) \<and> eval the_singleton t t' n'' \<gamma>')\<rbrakk> \<Longrightarrow> eval the_singleton t t' n (\<gamma>' \<UU>\<^sub>b \<gamma>)

goal (1 subgoal):
 1. eval the_singleton t t' n (\<gamma>' \<UU>\<^sub>b \<gamma>)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
eval the_singleton t t' n (\<gamma>' \<UU>\<^sub>b \<gamma>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma untilE[elim]:
  fixes t id n \<gamma>' \<gamma>
  assumes "eval the_singleton t t' n (\<gamma>' \<UU>\<^sub>b \<gamma>)"
  shows "\<exists>n'\<ge>n. eval the_singleton t t' n' \<gamma> \<and> (\<forall>n''\<ge>n. n'' < n' \<longrightarrow> eval the_singleton t t' n'' \<gamma>')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>n'\<ge>n. eval the_singleton t t' n' \<gamma> \<and> (\<forall>n''\<ge>n. n'' < n' \<longrightarrow> eval the_singleton t t' n'' \<gamma>')
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>n'\<ge>n. eval the_singleton t t' n' \<gamma> \<and> (\<forall>n''\<ge>n. n'' < n' \<longrightarrow> eval the_singleton t t' n'' \<gamma>')
[PROOF STEP]
have "\<parallel>the_singleton\<parallel>\<^bsub>t n\<^esub>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>the_singleton\<parallel>\<^bsub>t n\<^esub>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<parallel>the_singleton\<parallel>\<^bsub>t n\<^esub>

goal (1 subgoal):
 1. \<exists>n'\<ge>n. eval the_singleton t t' n' \<gamma> \<and> (\<forall>n''\<ge>n. n'' < n' \<longrightarrow> eval the_singleton t t' n'' \<gamma>')
[PROOF STEP]
with \<open>eval the_singleton t t' n (\<gamma>' \<UU>\<^sub>b \<gamma>)\<close>
[PROOF STATE]
proof (chain)
picking this:
eval the_singleton t t' n (\<gamma>' \<UU>\<^sub>b \<gamma>)
\<parallel>the_singleton\<parallel>\<^bsub>t n\<^esub>
[PROOF STEP]
obtain n' where "n'\<ge>\<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n\<^esub>" and
   "(\<exists>i\<ge>n'. \<parallel>the_singleton\<parallel>\<^bsub>t i\<^esub>) \<and>
   (\<forall>n''\<ge>\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub>. n'' \<le> \<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n'\<^esub> \<longrightarrow> eval the_singleton t t' n'' \<gamma>) \<and>
   (\<forall>n''\<ge>\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n\<^esub>. n'' < \<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub> \<longrightarrow> eval the_singleton t t' n'' \<gamma>') \<or>
   \<not> (\<exists>i\<ge>n'. \<parallel>the_singleton\<parallel>\<^bsub>t i\<^esub>) \<and>
   eval the_singleton t t' n' \<gamma> \<and> (\<forall>n''\<ge>\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n\<^esub>. n'' < n' \<longrightarrow> eval the_singleton t t' n'' \<gamma>')"
[PROOF STATE]
proof (prove)
using this:
eval the_singleton t t' n (\<gamma>' \<UU>\<^sub>b \<gamma>)
\<parallel>the_singleton\<parallel>\<^bsub>t n\<^esub>

goal (1 subgoal):
 1. (\<And>n'. \<lbrakk>\<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n\<^esub> \<le> n'; (\<exists>i\<ge>n'. \<parallel>the_singleton\<parallel>\<^bsub>t i\<^esub>) \<and> (\<forall>n''\<ge>\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub>. n'' \<le> \<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n'\<^esub> \<longrightarrow> eval the_singleton t t' n'' \<gamma>) \<and> (\<forall>n''\<ge>\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n\<^esub>. n'' < \<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub> \<longrightarrow> eval the_singleton t t' n'' \<gamma>') \<or> \<not> (\<exists>i\<ge>n'. \<parallel>the_singleton\<parallel>\<^bsub>t i\<^esub>) \<and> eval the_singleton t t' n' \<gamma> \<and> (\<forall>n''\<ge>\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n\<^esub>. n'' < n' \<longrightarrow> eval the_singleton t t' n'' \<gamma>')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using untilEA[of n "the_singleton" t t' \<gamma>' \<gamma>]
[PROOF STATE]
proof (prove)
using this:
eval the_singleton t t' n (\<gamma>' \<UU>\<^sub>b \<gamma>)
\<parallel>the_singleton\<parallel>\<^bsub>t n\<^esub>
\<lbrakk>\<exists>i\<ge>n. \<parallel>the_singleton\<parallel>\<^bsub>t i\<^esub>; eval the_singleton t t' n (\<gamma>' \<UU>\<^sub>b \<gamma>)\<rbrakk> \<Longrightarrow> \<exists>n'\<ge>\<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n\<^esub>. (\<exists>i\<ge>n'. \<parallel>the_singleton\<parallel>\<^bsub>t i\<^esub>) \<and> (\<forall>n''\<ge>\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub>. n'' \<le> \<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n'\<^esub> \<longrightarrow> eval the_singleton t t' n'' \<gamma>) \<and> (\<forall>n''\<ge>\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n\<^esub>. n'' < \<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub> \<longrightarrow> eval the_singleton t t' n'' \<gamma>') \<or> \<not> (\<exists>i\<ge>n'. \<parallel>the_singleton\<parallel>\<^bsub>t i\<^esub>) \<and> eval the_singleton t t' n' \<gamma> \<and> (\<forall>n''\<ge>\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n\<^esub>. n'' < n' \<longrightarrow> eval the_singleton t t' n'' \<gamma>')

goal (1 subgoal):
 1. (\<And>n'. \<lbrakk>\<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n\<^esub> \<le> n'; (\<exists>i\<ge>n'. \<parallel>the_singleton\<parallel>\<^bsub>t i\<^esub>) \<and> (\<forall>n''\<ge>\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub>. n'' \<le> \<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n'\<^esub> \<longrightarrow> eval the_singleton t t' n'' \<gamma>) \<and> (\<forall>n''\<ge>\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n\<^esub>. n'' < \<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub> \<longrightarrow> eval the_singleton t t' n'' \<gamma>') \<or> \<not> (\<exists>i\<ge>n'. \<parallel>the_singleton\<parallel>\<^bsub>t i\<^esub>) \<and> eval the_singleton t t' n' \<gamma> \<and> (\<forall>n''\<ge>\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n\<^esub>. n'' < n' \<longrightarrow> eval the_singleton t t' n'' \<gamma>')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n\<^esub> \<le> n'
(\<exists>i\<ge>n'. \<parallel>the_singleton\<parallel>\<^bsub>t i\<^esub>) \<and> (\<forall>n''\<ge>\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub>. n'' \<le> \<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n'\<^esub> \<longrightarrow> eval the_singleton t t' n'' \<gamma>) \<and> (\<forall>n''\<ge>\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n\<^esub>. n'' < \<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub> \<longrightarrow> eval the_singleton t t' n'' \<gamma>') \<or> \<not> (\<exists>i\<ge>n'. \<parallel>the_singleton\<parallel>\<^bsub>t i\<^esub>) \<and> eval the_singleton t t' n' \<gamma> \<and> (\<forall>n''\<ge>\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n\<^esub>. n'' < n' \<longrightarrow> eval the_singleton t t' n'' \<gamma>')

goal (1 subgoal):
 1. \<exists>n'\<ge>n. eval the_singleton t t' n' \<gamma> \<and> (\<forall>n''\<ge>n. n'' < n' \<longrightarrow> eval the_singleton t t' n'' \<gamma>')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n\<^esub> \<le> n'
(\<exists>i\<ge>n'. \<parallel>the_singleton\<parallel>\<^bsub>t i\<^esub>) \<and> (\<forall>n''\<ge>\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub>. n'' \<le> \<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n'\<^esub> \<longrightarrow> eval the_singleton t t' n'' \<gamma>) \<and> (\<forall>n''\<ge>\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n\<^esub>. n'' < \<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub> \<longrightarrow> eval the_singleton t t' n'' \<gamma>') \<or> \<not> (\<exists>i\<ge>n'. \<parallel>the_singleton\<parallel>\<^bsub>t i\<^esub>) \<and> eval the_singleton t t' n' \<gamma> \<and> (\<forall>n''\<ge>\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n\<^esub>. n'' < n' \<longrightarrow> eval the_singleton t t' n'' \<gamma>')

goal (1 subgoal):
 1. \<exists>n'\<ge>n. eval the_singleton t t' n' \<gamma> \<and> (\<forall>n''\<ge>n. n'' < n' \<longrightarrow> eval the_singleton t t' n'' \<gamma>')
[PROOF STEP]
have "\<parallel>the_singleton\<parallel>\<^bsub>t n'\<^esub>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>the_singleton\<parallel>\<^bsub>t n'\<^esub>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<parallel>the_singleton\<parallel>\<^bsub>t n'\<^esub>

goal (1 subgoal):
 1. \<exists>n'\<ge>n. eval the_singleton t t' n' \<gamma> \<and> (\<forall>n''\<ge>n. n'' < n' \<longrightarrow> eval the_singleton t t' n'' \<gamma>')
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n\<^esub> \<le> n'
(\<exists>i\<ge>n'. \<parallel>the_singleton\<parallel>\<^bsub>t i\<^esub>) \<and> (\<forall>n''\<ge>\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub>. n'' \<le> \<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n'\<^esub> \<longrightarrow> eval the_singleton t t' n'' \<gamma>) \<and> (\<forall>n''\<ge>\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n\<^esub>. n'' < \<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub> \<longrightarrow> eval the_singleton t t' n'' \<gamma>') \<or> \<not> (\<exists>i\<ge>n'. \<parallel>the_singleton\<parallel>\<^bsub>t i\<^esub>) \<and> eval the_singleton t t' n' \<gamma> \<and> (\<forall>n''\<ge>\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n\<^esub>. n'' < n' \<longrightarrow> eval the_singleton t t' n'' \<gamma>')
\<parallel>the_singleton\<parallel>\<^bsub>t n'\<^esub>
[PROOF STEP]
have
    "(\<forall>n''\<ge>\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub>. n'' \<le> \<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n'\<^esub> \<longrightarrow> eval the_singleton t t' n'' \<gamma>) \<and>
    (\<forall>n''\<ge>\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n\<^esub>. n'' < \<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub> \<longrightarrow> eval the_singleton t t' n'' \<gamma>')"
[PROOF STATE]
proof (prove)
using this:
\<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n\<^esub> \<le> n'
(\<exists>i\<ge>n'. \<parallel>the_singleton\<parallel>\<^bsub>t i\<^esub>) \<and> (\<forall>n''\<ge>\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub>. n'' \<le> \<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n'\<^esub> \<longrightarrow> eval the_singleton t t' n'' \<gamma>) \<and> (\<forall>n''\<ge>\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n\<^esub>. n'' < \<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub> \<longrightarrow> eval the_singleton t t' n'' \<gamma>') \<or> \<not> (\<exists>i\<ge>n'. \<parallel>the_singleton\<parallel>\<^bsub>t i\<^esub>) \<and> eval the_singleton t t' n' \<gamma> \<and> (\<forall>n''\<ge>\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n\<^esub>. n'' < n' \<longrightarrow> eval the_singleton t t' n'' \<gamma>')
\<parallel>the_singleton\<parallel>\<^bsub>t n'\<^esub>

goal (1 subgoal):
 1. (\<forall>n''\<ge>\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub>. n'' \<le> \<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n'\<^esub> \<longrightarrow> eval the_singleton t t' n'' \<gamma>) \<and> (\<forall>n''\<ge>\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n\<^esub>. n'' < \<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub> \<longrightarrow> eval the_singleton t t' n'' \<gamma>')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<forall>n''\<ge>\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub>. n'' \<le> \<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n'\<^esub> \<longrightarrow> eval the_singleton t t' n'' \<gamma>) \<and> (\<forall>n''\<ge>\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n\<^esub>. n'' < \<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub> \<longrightarrow> eval the_singleton t t' n'' \<gamma>')

goal (1 subgoal):
 1. \<exists>n'\<ge>n. eval the_singleton t t' n' \<gamma> \<and> (\<forall>n''\<ge>n. n'' < n' \<longrightarrow> eval the_singleton t t' n'' \<gamma>')
[PROOF STEP]
hence "eval the_singleton t t' n' \<gamma>" and "(\<forall>n''\<ge>n. n'' < n' \<longrightarrow> eval the_singleton t t' n'' \<gamma>')"
[PROOF STATE]
proof (prove)
using this:
(\<forall>n''\<ge>\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub>. n'' \<le> \<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n'\<^esub> \<longrightarrow> eval the_singleton t t' n'' \<gamma>) \<and> (\<forall>n''\<ge>\<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n\<^esub>. n'' < \<langle>the_singleton \<Leftarrow> t\<rangle>\<^bsub>n'\<^esub> \<longrightarrow> eval the_singleton t t' n'' \<gamma>')

goal (1 subgoal):
 1. eval the_singleton t t' n' \<gamma> &&& \<forall>n''\<ge>n. n'' < n' \<longrightarrow> eval the_singleton t t' n'' \<gamma>'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eval the_singleton t t' n' \<gamma>
\<forall>n''\<ge>n. n'' < n' \<longrightarrow> eval the_singleton t t' n'' \<gamma>'

goal (1 subgoal):
 1. \<exists>n'\<ge>n. eval the_singleton t t' n' \<gamma> \<and> (\<forall>n''\<ge>n. n'' < n' \<longrightarrow> eval the_singleton t t' n'' \<gamma>')
[PROOF STEP]
with \<open>eval the_singleton t t' n' \<gamma>\<close> \<open>n'\<ge>\<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n\<^esub>\<close>
[PROOF STATE]
proof (chain)
picking this:
eval the_singleton t t' n' \<gamma>
\<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n\<^esub> \<le> n'
eval the_singleton t t' n' \<gamma>
\<forall>n''\<ge>n. n'' < n' \<longrightarrow> eval the_singleton t t' n'' \<gamma>'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
eval the_singleton t t' n' \<gamma>
\<langle>the_singleton \<rightarrow> t\<rangle>\<^bsub>n\<^esub> \<le> n'
eval the_singleton t t' n' \<gamma>
\<forall>n''\<ge>n. n'' < n' \<longrightarrow> eval the_singleton t t' n'' \<gamma>'

goal (1 subgoal):
 1. \<exists>n'\<ge>n. eval the_singleton t t' n' \<gamma> \<and> (\<forall>n''\<ge>n. n'' < n' \<longrightarrow> eval the_singleton t t' n'' \<gamma>')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>n'\<ge>n. eval the_singleton t t' n' \<gamma> \<and> (\<forall>n''\<ge>n. n'' < n' \<longrightarrow> eval the_singleton t t' n'' \<gamma>')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Act_tau_eq_iff [simp]:
    "Act \<tau> x1 = Act \<alpha> x2 \<longleftrightarrow> \<alpha> = \<tau> \<and> x2 = x1"
    (is "?l \<longleftrightarrow> ?r")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Act \<tau> x1 = Act \<alpha> x2) = (\<alpha> = \<tau> \<and> x2 = x1)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Act \<tau> x1 = Act \<alpha> x2 \<Longrightarrow> \<alpha> = \<tau> \<and> x2 = x1
 2. \<alpha> = \<tau> \<and> x2 = x1 \<Longrightarrow> Act \<tau> x1 = Act \<alpha> x2
[PROOF STEP]
assume "?l"
[PROOF STATE]
proof (state)
this:
Act \<tau> x1 = Act \<alpha> x2

goal (2 subgoals):
 1. Act \<tau> x1 = Act \<alpha> x2 \<Longrightarrow> \<alpha> = \<tau> \<and> x2 = x1
 2. \<alpha> = \<tau> \<and> x2 = x1 \<Longrightarrow> Act \<tau> x1 = Act \<alpha> x2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Act \<tau> x1 = Act \<alpha> x2
[PROOF STEP]
obtain p where p_\<alpha>: "p \<bullet> \<tau> = \<alpha>" and p_x: "p \<bullet> x1 = x2" and fresh: "(supp x1 - bn \<tau>) \<sharp>* p"
[PROOF STATE]
proof (prove)
using this:
Act \<tau> x1 = Act \<alpha> x2

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>p \<bullet> \<tau> = \<alpha>; p \<bullet> x1 = x2; (supp x1 - bn \<tau>) \<sharp>* p\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis Act_eq_iff_perm)
[PROOF STATE]
proof (state)
this:
p \<bullet> \<tau> = \<alpha>
p \<bullet> x1 = x2
(supp x1 - bn \<tau>) \<sharp>* p

goal (2 subgoals):
 1. Act \<tau> x1 = Act \<alpha> x2 \<Longrightarrow> \<alpha> = \<tau> \<and> x2 = x1
 2. \<alpha> = \<tau> \<and> x2 = x1 \<Longrightarrow> Act \<tau> x1 = Act \<alpha> x2
[PROOF STEP]
from p_\<alpha>
[PROOF STATE]
proof (chain)
picking this:
p \<bullet> \<tau> = \<alpha>
[PROOF STEP]
have "\<alpha> = \<tau>"
[PROOF STATE]
proof (prove)
using this:
p \<bullet> \<tau> = \<alpha>

goal (1 subgoal):
 1. \<alpha> = \<tau>
[PROOF STEP]
by (metis tau_eqvt)
[PROOF STATE]
proof (state)
this:
\<alpha> = \<tau>

goal (2 subgoals):
 1. Act \<tau> x1 = Act \<alpha> x2 \<Longrightarrow> \<alpha> = \<tau> \<and> x2 = x1
 2. \<alpha> = \<tau> \<and> x2 = x1 \<Longrightarrow> Act \<tau> x1 = Act \<alpha> x2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<alpha> = \<tau>

goal (2 subgoals):
 1. Act \<tau> x1 = Act \<alpha> x2 \<Longrightarrow> \<alpha> = \<tau> \<and> x2 = x1
 2. \<alpha> = \<tau> \<and> x2 = x1 \<Longrightarrow> Act \<tau> x1 = Act \<alpha> x2
[PROOF STEP]
from fresh and p_x
[PROOF STATE]
proof (chain)
picking this:
(supp x1 - bn \<tau>) \<sharp>* p
p \<bullet> x1 = x2
[PROOF STEP]
have "x2 = x1"
[PROOF STATE]
proof (prove)
using this:
(supp x1 - bn \<tau>) \<sharp>* p
p \<bullet> x1 = x2

goal (1 subgoal):
 1. x2 = x1
[PROOF STEP]
by (simp add: supp_perm_eq)
[PROOF STATE]
proof (state)
this:
x2 = x1

goal (2 subgoals):
 1. Act \<tau> x1 = Act \<alpha> x2 \<Longrightarrow> \<alpha> = \<tau> \<and> x2 = x1
 2. \<alpha> = \<tau> \<and> x2 = x1 \<Longrightarrow> Act \<tau> x1 = Act \<alpha> x2
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<alpha> = \<tau>
x2 = x1
[PROOF STEP]
show "?r"
[PROOF STATE]
proof (prove)
using this:
\<alpha> = \<tau>
x2 = x1

goal (1 subgoal):
 1. \<alpha> = \<tau> \<and> x2 = x1
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<alpha> = \<tau> \<and> x2 = x1

goal (1 subgoal):
 1. \<alpha> = \<tau> \<and> x2 = x1 \<Longrightarrow> Act \<tau> x1 = Act \<alpha> x2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<alpha> = \<tau> \<and> x2 = x1 \<Longrightarrow> Act \<tau> x1 = Act \<alpha> x2
[PROOF STEP]
assume "?r"
[PROOF STATE]
proof (state)
this:
\<alpha> = \<tau> \<and> x2 = x1

goal (1 subgoal):
 1. \<alpha> = \<tau> \<and> x2 = x1 \<Longrightarrow> Act \<tau> x1 = Act \<alpha> x2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<alpha> = \<tau> \<and> x2 = x1
[PROOF STEP]
show "?l"
[PROOF STATE]
proof (prove)
using this:
\<alpha> = \<tau> \<and> x2 = x1

goal (1 subgoal):
 1. Act \<tau> x1 = Act \<alpha> x2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Act \<tau> x1 = Act \<alpha> x2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma card_idx_nat' [simp]:
    "|UNIV::nat set| <o natLeq +c |UNIV::'idx set|"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. |UNIV| <o natLeq +c |UNIV|
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. |UNIV| <o natLeq +c |UNIV|
[PROOF STEP]
note card_idx_nat
[PROOF STATE]
proof (state)
this:
|UNIV| <o |UNIV|

goal (1 subgoal):
 1. |UNIV| <o natLeq +c |UNIV|
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
|UNIV| <o |UNIV|

goal (1 subgoal):
 1. |UNIV| <o natLeq +c |UNIV|
[PROOF STEP]
have "|UNIV :: 'idx set| \<le>o natLeq +c |UNIV :: 'idx set|"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. |UNIV| \<le>o natLeq +c |UNIV|
[PROOF STEP]
by (metis Cnotzero_UNIV ordLeq_csum2)
[PROOF STATE]
proof (state)
this:
|UNIV| \<le>o natLeq +c |UNIV|

goal (1 subgoal):
 1. |UNIV| <o natLeq +c |UNIV|
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
|UNIV| <o natLeq +c |UNIV|
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
|UNIV| <o natLeq +c |UNIV|

goal (1 subgoal):
 1. |UNIV| <o natLeq +c |UNIV|
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
|UNIV| <o natLeq +c |UNIV|

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma tau_steps_eqvt (*[eqvt]*) [simp]:
    "p \<bullet> tau_steps x n = tau_steps (p \<bullet> x) (p \<bullet> n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<bullet> tau_steps x n = tau_steps (p \<bullet> x) (p \<bullet> n)
[PROOF STEP]
by (induct n) (simp_all add: permute_nat_def tau_eqvt)


[STATEMENT]
lemma tau_steps_eqvt' [simp]:
    "p \<bullet> tau_steps x = tau_steps (p \<bullet> x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<bullet> tau_steps x = tau_steps (p \<bullet> x)
[PROOF STEP]
by (simp add: permute_fun_def)


[STATEMENT]
lemma tau_steps_eqvt_raw [simp]:
    "p \<bullet> tau_steps = tau_steps"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<bullet> tau_steps = tau_steps
[PROOF STEP]
by (simp add: permute_fun_def)


[STATEMENT]
lemma tau_steps_add [simp]:
    "tau_steps (tau_steps x m) n = tau_steps x (m + n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tau_steps (tau_steps x m) n = tau_steps x (m + n)
[PROOF STEP]
by (induct n) auto


[STATEMENT]
lemma tau_steps_not_self:
    "x = tau_steps x n \<longleftrightarrow> n = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x = tau_steps x n) = (n = 0)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x = tau_steps x n \<Longrightarrow> n = 0
 2. n = 0 \<Longrightarrow> x = tau_steps x n
[PROOF STEP]
assume "x = tau_steps x n"
[PROOF STATE]
proof (state)
this:
x = tau_steps x n

goal (2 subgoals):
 1. x = tau_steps x n \<Longrightarrow> n = 0
 2. n = 0 \<Longrightarrow> x = tau_steps x n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x = tau_steps x n
[PROOF STEP]
show "n = 0"
[PROOF STATE]
proof (prove)
using this:
x = tau_steps x n

goal (1 subgoal):
 1. n = 0
[PROOF STEP]
proof (induct n arbitrary: x)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x = tau_steps x 0 \<Longrightarrow> 0 = 0
 2. \<And>n x. \<lbrakk>\<And>x. x = tau_steps x n \<Longrightarrow> n = 0; x = tau_steps x (Suc n)\<rbrakk> \<Longrightarrow> Suc n = 0
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
x = tau_steps x 0

goal (2 subgoals):
 1. \<And>x. x = tau_steps x 0 \<Longrightarrow> 0 = 0
 2. \<And>n x. \<lbrakk>\<And>x. x = tau_steps x n \<Longrightarrow> n = 0; x = tau_steps x (Suc n)\<rbrakk> \<Longrightarrow> Suc n = 0
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 = 0
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
0 = 0

goal (1 subgoal):
 1. \<And>n x. \<lbrakk>\<And>x. x = tau_steps x n \<Longrightarrow> n = 0; x = tau_steps x (Suc n)\<rbrakk> \<Longrightarrow> Suc n = 0
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n x. \<lbrakk>\<And>x. x = tau_steps x n \<Longrightarrow> n = 0; x = tau_steps x (Suc n)\<rbrakk> \<Longrightarrow> Suc n = 0
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
?x7 = tau_steps ?x7 n \<Longrightarrow> n = 0
x = tau_steps x (Suc n)

goal (1 subgoal):
 1. \<And>n x. \<lbrakk>\<And>x. x = tau_steps x n \<Longrightarrow> n = 0; x = tau_steps x (Suc n)\<rbrakk> \<Longrightarrow> Suc n = 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?x7 = tau_steps ?x7 n \<Longrightarrow> n = 0
x = tau_steps x (Suc n)
[PROOF STEP]
have "x = Act \<tau> (tau_steps x n)"
[PROOF STATE]
proof (prove)
using this:
?x7 = tau_steps ?x7 n \<Longrightarrow> n = 0
x = tau_steps x (Suc n)

goal (1 subgoal):
 1. x = Act \<tau> (tau_steps x n)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x = Act \<tau> (tau_steps x n)

goal (1 subgoal):
 1. \<And>n x. \<lbrakk>\<And>x. x = tau_steps x n \<Longrightarrow> n = 0; x = tau_steps x (Suc n)\<rbrakk> \<Longrightarrow> Suc n = 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x = Act \<tau> (tau_steps x n)
[PROOF STEP]
show "Suc n = 0"
[PROOF STATE]
proof (prove)
using this:
x = Act \<tau> (tau_steps x n)

goal (1 subgoal):
 1. Suc n = 0
[PROOF STEP]
proof (induct x)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>xset. \<lbrakk>finite (supp xset); \<And>x. \<lbrakk>x \<in> set_bset xset; x = Act \<tau> (tau_steps x n)\<rbrakk> \<Longrightarrow> Suc n = 0; Conj xset = Act \<tau> (tau_steps (Conj xset) n)\<rbrakk> \<Longrightarrow> Suc n = 0
 2. \<And>x. \<lbrakk>x = Act \<tau> (tau_steps x n) \<Longrightarrow> Suc n = 0; Formula.Not x = Act \<tau> (tau_steps (Formula.Not x) n)\<rbrakk> \<Longrightarrow> Suc n = 0
 3. \<And>pred. Pred pred = Act \<tau> (tau_steps (Pred pred) n) \<Longrightarrow> Suc n = 0
 4. \<And>act x. \<lbrakk>x = Act \<tau> (tau_steps x n) \<Longrightarrow> Suc n = 0; Act act x = Act \<tau> (tau_steps (Act act x) n)\<rbrakk> \<Longrightarrow> Suc n = 0
[PROOF STEP]
case (Act \<alpha> x)
[PROOF STATE]
proof (state)
this:
x = Act \<tau> (tau_steps x n) \<Longrightarrow> Suc n = 0
Act \<alpha> x = Act \<tau> (tau_steps (Act \<alpha> x) n)

goal (4 subgoals):
 1. \<And>xset. \<lbrakk>finite (supp xset); \<And>x. \<lbrakk>x \<in> set_bset xset; x = Act \<tau> (tau_steps x n)\<rbrakk> \<Longrightarrow> Suc n = 0; Conj xset = Act \<tau> (tau_steps (Conj xset) n)\<rbrakk> \<Longrightarrow> Suc n = 0
 2. \<And>x. \<lbrakk>x = Act \<tau> (tau_steps x n) \<Longrightarrow> Suc n = 0; Formula.Not x = Act \<tau> (tau_steps (Formula.Not x) n)\<rbrakk> \<Longrightarrow> Suc n = 0
 3. \<And>pred. Pred pred = Act \<tau> (tau_steps (Pred pred) n) \<Longrightarrow> Suc n = 0
 4. \<And>act x. \<lbrakk>x = Act \<tau> (tau_steps x n) \<Longrightarrow> Suc n = 0; Act act x = Act \<tau> (tau_steps (Act act x) n)\<rbrakk> \<Longrightarrow> Suc n = 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x = Act \<tau> (tau_steps x n) \<Longrightarrow> Suc n = 0
Act \<alpha> x = Act \<tau> (tau_steps (Act \<alpha> x) n)
[PROOF STEP]
have "x = tau_steps (Act \<tau> x) n"
[PROOF STATE]
proof (prove)
using this:
x = Act \<tau> (tau_steps x n) \<Longrightarrow> Suc n = 0
Act \<alpha> x = Act \<tau> (tau_steps (Act \<alpha> x) n)

goal (1 subgoal):
 1. x = tau_steps (Act \<tau> x) n
[PROOF STEP]
by (metis Act_tau_eq_iff)
[PROOF STATE]
proof (state)
this:
x = tau_steps (Act \<tau> x) n

goal (4 subgoals):
 1. \<And>xset. \<lbrakk>finite (supp xset); \<And>x. \<lbrakk>x \<in> set_bset xset; x = Act \<tau> (tau_steps x n)\<rbrakk> \<Longrightarrow> Suc n = 0; Conj xset = Act \<tau> (tau_steps (Conj xset) n)\<rbrakk> \<Longrightarrow> Suc n = 0
 2. \<And>x. \<lbrakk>x = Act \<tau> (tau_steps x n) \<Longrightarrow> Suc n = 0; Formula.Not x = Act \<tau> (tau_steps (Formula.Not x) n)\<rbrakk> \<Longrightarrow> Suc n = 0
 3. \<And>pred. Pred pred = Act \<tau> (tau_steps (Pred pred) n) \<Longrightarrow> Suc n = 0
 4. \<And>act x. \<lbrakk>x = Act \<tau> (tau_steps x n) \<Longrightarrow> Suc n = 0; Act act x = Act \<tau> (tau_steps (Act act x) n)\<rbrakk> \<Longrightarrow> Suc n = 0
[PROOF STEP]
with Act.hyps
[PROOF STATE]
proof (chain)
picking this:
x = Act \<tau> (tau_steps x n) \<Longrightarrow> Suc n = 0
x = tau_steps (Act \<tau> x) n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x = Act \<tau> (tau_steps x n) \<Longrightarrow> Suc n = 0
x = tau_steps (Act \<tau> x) n

goal (1 subgoal):
 1. Suc n = 0
[PROOF STEP]
by (metis add_Suc tau_steps.simps(2) tau_steps_add)
[PROOF STATE]
proof (state)
this:
Suc n = 0

goal (3 subgoals):
 1. \<And>xset. \<lbrakk>finite (supp xset); \<And>x. \<lbrakk>x \<in> set_bset xset; x = Act \<tau> (tau_steps x n)\<rbrakk> \<Longrightarrow> Suc n = 0; Conj xset = Act \<tau> (tau_steps (Conj xset) n)\<rbrakk> \<Longrightarrow> Suc n = 0
 2. \<And>x. \<lbrakk>x = Act \<tau> (tau_steps x n) \<Longrightarrow> Suc n = 0; Formula.Not x = Act \<tau> (tau_steps (Formula.Not x) n)\<rbrakk> \<Longrightarrow> Suc n = 0
 3. \<And>pred. Pred pred = Act \<tau> (tau_steps (Pred pred) n) \<Longrightarrow> Suc n = 0
[PROOF STEP]
qed simp_all
[PROOF STATE]
proof (state)
this:
Suc n = 0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
n = 0

goal (1 subgoal):
 1. n = 0 \<Longrightarrow> x = tau_steps x n
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n = 0 \<Longrightarrow> x = tau_steps x n
[PROOF STEP]
assume "n = 0"
[PROOF STATE]
proof (state)
this:
n = 0

goal (1 subgoal):
 1. n = 0 \<Longrightarrow> x = tau_steps x n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n = 0
[PROOF STEP]
show "x = tau_steps x n"
[PROOF STATE]
proof (prove)
using this:
n = 0

goal (1 subgoal):
 1. x = tau_steps x n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x = tau_steps x n

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma finite_supp_map_bset_tau_steps [simp]:
    "finite (supp (map_bset (tau_steps x) (Abs_bset UNIV :: nat set['idx])))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (supp (map_bset (tau_steps x) (Abs_bset UNIV)))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite (supp (map_bset (tau_steps x) (Abs_bset UNIV)))
[PROOF STEP]
have "eqvt map_bset" and "eqvt tau_steps"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqvt map_bset &&& eqvt tau_steps
[PROOF STEP]
by (simp add: eqvtI)+
[PROOF STATE]
proof (state)
this:
eqvt map_bset
eqvt tau_steps

goal (1 subgoal):
 1. finite (supp (map_bset (tau_steps x) (Abs_bset UNIV)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eqvt map_bset
eqvt tau_steps
[PROOF STEP]
have "supp (map_bset (tau_steps x)) \<subseteq> supp x"
[PROOF STATE]
proof (prove)
using this:
eqvt map_bset
eqvt tau_steps

goal (1 subgoal):
 1. supp (map_bset (tau_steps x)) \<subseteq> supp x
[PROOF STEP]
using supp_fun_eqvt supp_fun_app supp_fun_app_eqvt
[PROOF STATE]
proof (prove)
using this:
eqvt map_bset
eqvt tau_steps
eqvt ?f \<Longrightarrow> supp ?f = {}
supp (?f ?x) \<subseteq> supp ?f \<union> supp ?x
eqvt ?f \<Longrightarrow> supp (?f ?x) \<subseteq> supp ?x

goal (1 subgoal):
 1. supp (map_bset (tau_steps x)) \<subseteq> supp x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
supp (map_bset (tau_steps x)) \<subseteq> supp x

goal (1 subgoal):
 1. finite (supp (map_bset (tau_steps x) (Abs_bset UNIV)))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
supp (map_bset (tau_steps x)) \<subseteq> supp x

goal (1 subgoal):
 1. finite (supp (map_bset (tau_steps x) (Abs_bset UNIV)))
[PROOF STEP]
have "supp (Abs_bset UNIV :: nat set['idx]) = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. supp (Abs_bset UNIV) = {}
[PROOF STEP]
by (simp add: eqvtI supp_fun_eqvt)
[PROOF STATE]
proof (state)
this:
supp (Abs_bset UNIV) = {}

goal (1 subgoal):
 1. finite (supp (map_bset (tau_steps x) (Abs_bset UNIV)))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
supp (map_bset (tau_steps x)) \<subseteq> supp x
supp (Abs_bset UNIV) = {}
[PROOF STEP]
have "supp (map_bset (tau_steps x) (Abs_bset UNIV :: nat set['idx])) \<subseteq> supp x"
[PROOF STATE]
proof (prove)
using this:
supp (map_bset (tau_steps x)) \<subseteq> supp x
supp (Abs_bset UNIV) = {}

goal (1 subgoal):
 1. supp (map_bset (tau_steps x) (Abs_bset UNIV)) \<subseteq> supp x
[PROOF STEP]
using supp_fun_app
[PROOF STATE]
proof (prove)
using this:
supp (map_bset (tau_steps x)) \<subseteq> supp x
supp (Abs_bset UNIV) = {}
supp (?f ?x) \<subseteq> supp ?f \<union> supp ?x

goal (1 subgoal):
 1. supp (map_bset (tau_steps x) (Abs_bset UNIV)) \<subseteq> supp x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
supp (map_bset (tau_steps x) (Abs_bset UNIV)) \<subseteq> supp x

goal (1 subgoal):
 1. finite (supp (map_bset (tau_steps x) (Abs_bset UNIV)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
supp (map_bset (tau_steps x) (Abs_bset UNIV)) \<subseteq> supp x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
supp (map_bset (tau_steps x) (Abs_bset UNIV)) \<subseteq> supp x

goal (1 subgoal):
 1. finite (supp (map_bset (tau_steps x) (Abs_bset UNIV)))
[PROOF STEP]
by (metis finite_subset finite_supp)
[PROOF STATE]
proof (state)
this:
finite (supp (map_bset (tau_steps x) (Abs_bset UNIV)))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma weak_tau_modality_eqvt (*[eqvt]*) [simp]:
    "p \<bullet> weak_tau_modality x = weak_tau_modality (p \<bullet> x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<bullet> weak_tau_modality x = weak_tau_modality (p \<bullet> x)
[PROOF STEP]
unfolding weak_tau_modality_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<bullet> Disj (map_bset (tau_steps x) (Abs_bset UNIV)) = Disj (map_bset (tau_steps (p \<bullet> x)) (Abs_bset UNIV))
[PROOF STEP]
by (simp add: map_bset_eqvt)


[STATEMENT]
lemma weak_tau_modality_eq_iff [simp]:
    "weak_tau_modality x = weak_tau_modality y \<longleftrightarrow> x = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (weak_tau_modality x = weak_tau_modality y) = (x = y)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. weak_tau_modality x = weak_tau_modality y \<Longrightarrow> x = y
 2. x = y \<Longrightarrow> weak_tau_modality x = weak_tau_modality y
[PROOF STEP]
assume "weak_tau_modality x = weak_tau_modality y"
[PROOF STATE]
proof (state)
this:
weak_tau_modality x = weak_tau_modality y

goal (2 subgoals):
 1. weak_tau_modality x = weak_tau_modality y \<Longrightarrow> x = y
 2. x = y \<Longrightarrow> weak_tau_modality x = weak_tau_modality y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
weak_tau_modality x = weak_tau_modality y
[PROOF STEP]
have "map_bset (tau_steps x) (Abs_bset UNIV :: _ set['idx]) = map_bset (tau_steps y) (Abs_bset UNIV)"
[PROOF STATE]
proof (prove)
using this:
weak_tau_modality x = weak_tau_modality y

goal (1 subgoal):
 1. map_bset (tau_steps x) (Abs_bset UNIV) = map_bset (tau_steps y) (Abs_bset UNIV)
[PROOF STEP]
unfolding weak_tau_modality_def
[PROOF STATE]
proof (prove)
using this:
Disj (map_bset (tau_steps x) (Abs_bset UNIV)) = Disj (map_bset (tau_steps y) (Abs_bset UNIV))

goal (1 subgoal):
 1. map_bset (tau_steps x) (Abs_bset UNIV) = map_bset (tau_steps y) (Abs_bset UNIV)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
map_bset (tau_steps x) (Abs_bset UNIV) = map_bset (tau_steps y) (Abs_bset UNIV)

goal (2 subgoals):
 1. weak_tau_modality x = weak_tau_modality y \<Longrightarrow> x = y
 2. x = y \<Longrightarrow> weak_tau_modality x = weak_tau_modality y
[PROOF STEP]
with card_idx_nat'
[PROOF STATE]
proof (chain)
picking this:
|UNIV| <o natLeq +c |UNIV|
map_bset (tau_steps x) (Abs_bset UNIV) = map_bset (tau_steps y) (Abs_bset UNIV)
[PROOF STEP]
have "range (tau_steps x) = range (tau_steps y)"
      (is "?X = ?Y")
[PROOF STATE]
proof (prove)
using this:
|UNIV| <o natLeq +c |UNIV|
map_bset (tau_steps x) (Abs_bset UNIV) = map_bset (tau_steps y) (Abs_bset UNIV)

goal (1 subgoal):
 1. range (tau_steps x) = range (tau_steps y)
[PROOF STEP]
by (metis Abs_bset_inverse' map_bset.rep_eq)
[PROOF STATE]
proof (state)
this:
range (tau_steps x) = range (tau_steps y)

goal (2 subgoals):
 1. weak_tau_modality x = weak_tau_modality y \<Longrightarrow> x = y
 2. x = y \<Longrightarrow> weak_tau_modality x = weak_tau_modality y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
range (tau_steps x) = range (tau_steps y)
[PROOF STEP]
have "x \<in> range (tau_steps y)" and "y \<in> range (tau_steps x)"
[PROOF STATE]
proof (prove)
using this:
range (tau_steps x) = range (tau_steps y)

goal (1 subgoal):
 1. x \<in> range (tau_steps y) &&& y \<in> range (tau_steps x)
[PROOF STEP]
by (metis range_eqI tau_steps.simps(1))+
[PROOF STATE]
proof (state)
this:
x \<in> range (tau_steps y)
y \<in> range (tau_steps x)

goal (2 subgoals):
 1. weak_tau_modality x = weak_tau_modality y \<Longrightarrow> x = y
 2. x = y \<Longrightarrow> weak_tau_modality x = weak_tau_modality y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> range (tau_steps y)
y \<in> range (tau_steps x)
[PROOF STEP]
obtain nx ny where x: "x = tau_steps y nx" and y: "y = tau_steps x ny"
[PROOF STATE]
proof (prove)
using this:
x \<in> range (tau_steps y)
y \<in> range (tau_steps x)

goal (1 subgoal):
 1. (\<And>nx ny. \<lbrakk>x = tau_steps y nx; y = tau_steps x ny\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x = tau_steps y nx
y = tau_steps x ny

goal (2 subgoals):
 1. weak_tau_modality x = weak_tau_modality y \<Longrightarrow> x = y
 2. x = y \<Longrightarrow> weak_tau_modality x = weak_tau_modality y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x = tau_steps y nx
y = tau_steps x ny
[PROOF STEP]
have "ny + nx = 0"
[PROOF STATE]
proof (prove)
using this:
x = tau_steps y nx
y = tau_steps x ny

goal (1 subgoal):
 1. ny + nx = 0
[PROOF STEP]
by (simp add: tau_steps_not_self)
[PROOF STATE]
proof (state)
this:
ny + nx = 0

goal (2 subgoals):
 1. weak_tau_modality x = weak_tau_modality y \<Longrightarrow> x = y
 2. x = y \<Longrightarrow> weak_tau_modality x = weak_tau_modality y
[PROOF STEP]
with x and y
[PROOF STATE]
proof (chain)
picking this:
x = tau_steps y nx
y = tau_steps x ny
ny + nx = 0
[PROOF STEP]
show "x = y"
[PROOF STATE]
proof (prove)
using this:
x = tau_steps y nx
y = tau_steps x ny
ny + nx = 0

goal (1 subgoal):
 1. x = y
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x = y

goal (1 subgoal):
 1. x = y \<Longrightarrow> weak_tau_modality x = weak_tau_modality y
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x = y \<Longrightarrow> weak_tau_modality x = weak_tau_modality y
[PROOF STEP]
assume "x = y"
[PROOF STATE]
proof (state)
this:
x = y

goal (1 subgoal):
 1. x = y \<Longrightarrow> weak_tau_modality x = weak_tau_modality y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x = y
[PROOF STEP]
show "weak_tau_modality x = weak_tau_modality y"
[PROOF STATE]
proof (prove)
using this:
x = y

goal (1 subgoal):
 1. weak_tau_modality x = weak_tau_modality y
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
weak_tau_modality x = weak_tau_modality y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma supp_weak_tau_modality [simp]:
    "supp (weak_tau_modality x) = supp x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. supp (weak_tau_modality x) = supp x
[PROOF STEP]
unfolding supp_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {a. infinite {b. (a \<rightleftharpoons> b) \<bullet> weak_tau_modality x \<noteq> weak_tau_modality x}} = {a. infinite {b. (a \<rightleftharpoons> b) \<bullet> x \<noteq> x}}
[PROOF STEP]
by simp


[STATEMENT]
lemma Act_weak_tau_modality_eq_iff [simp]:
    "Act \<alpha>1 (weak_tau_modality x1) = Act \<alpha>2 (weak_tau_modality x2) \<longleftrightarrow> Act \<alpha>1 x1 = Act \<alpha>2 x2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Act \<alpha>1 (weak_tau_modality x1) = Act \<alpha>2 (weak_tau_modality x2)) = (Act \<alpha>1 x1 = Act \<alpha>2 x2)
[PROOF STEP]
by (simp add: Act_eq_iff_perm)


[STATEMENT]
lemma weak_action_modality_eqvt (*[eqvt]*) [simp]:
    "p \<bullet> (\<langle>\<langle>\<alpha>\<rangle>\<rangle>x) = \<langle>\<langle>p \<bullet> \<alpha>\<rangle>\<rangle>(p \<bullet> x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<bullet> \<langle>\<langle>\<alpha>\<rangle>\<rangle>x = \<langle>\<langle>p \<bullet> \<alpha>\<rangle>\<rangle>p \<bullet> x
[PROOF STEP]
using tau_eqvt weak_action_modality_def
[PROOF STATE]
proof (prove)
using this:
?p \<bullet> \<tau> = \<tau>
\<langle>\<langle>?\<alpha>\<rangle>\<rangle>?x \<equiv> if ?\<alpha> = \<tau> then weak_tau_modality ?x else weak_tau_modality (Act ?\<alpha> (weak_tau_modality ?x))

goal (1 subgoal):
 1. p \<bullet> \<langle>\<langle>\<alpha>\<rangle>\<rangle>x = \<langle>\<langle>p \<bullet> \<alpha>\<rangle>\<rangle>p \<bullet> x
[PROOF STEP]
by fastforce