[STATEMENT]
lemma in_list_nA_refl: "ss \<in> nlists n A  \<Longrightarrow>  ss [\<sqsubseteq>\<^bsub>r\<^esub>] ss"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ss \<in> nlists n A \<Longrightarrow> ss [\<sqsubseteq>\<^bsub>r\<^esub>] ss
[PROOF STEP]
apply (unfold Listn.le_def lesssub_def lesub_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ss \<in> nlists n A \<Longrightarrow> list_all2 r ss ss
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ss \<in> nlists n A \<Longrightarrow> list_all2 r ss ss
[PROOF STEP]
assume "ss \<in> nlists n A"
[PROOF STATE]
proof (state)
this:
ss \<in> nlists n A

goal (1 subgoal):
 1. ss \<in> nlists n A \<Longrightarrow> list_all2 r ss ss
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ss \<in> nlists n A
[PROOF STEP]
have "set ss \<subseteq> A" and "length ss = n"
[PROOF STATE]
proof (prove)
using this:
ss \<in> nlists n A

goal (1 subgoal):
 1. set ss \<subseteq> A &&& length ss = n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set ss \<subseteq> A
length ss = n

goal (1 subgoal):
 1. ss \<in> nlists n A \<Longrightarrow> list_all2 r ss ss
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
set ss \<subseteq> A
length ss = n
[PROOF STEP]
have "\<forall>i<n. ss!i \<in> A"
[PROOF STATE]
proof (prove)
using this:
set ss \<subseteq> A
length ss = n

goal (1 subgoal):
 1. \<forall>i<n. ss ! i \<in> A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>i<n. ss ! i \<in> A

goal (1 subgoal):
 1. ss \<in> nlists n A \<Longrightarrow> list_all2 r ss ss
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>i<n. ss ! i \<in> A
[PROOF STEP]
have "\<forall>i<length ss. ss!i \<sqsubseteq>\<^bsub>r\<^esub> ss!i"
[PROOF STATE]
proof (prove)
using this:
\<forall>i<n. ss ! i \<in> A

goal (1 subgoal):
 1. \<forall>i<length ss. ss ! i \<sqsubseteq>\<^bsub>r\<^esub> ss ! i
[PROOF STEP]
by (auto simp add:r_def lesssub_def lesub_def nodes_le_def )
[PROOF STATE]
proof (state)
this:
\<forall>i<length ss. ss ! i \<sqsubseteq>\<^bsub>r\<^esub> ss ! i

goal (1 subgoal):
 1. ss \<in> nlists n A \<Longrightarrow> list_all2 r ss ss
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>i<length ss. ss ! i \<sqsubseteq>\<^bsub>r\<^esub> ss ! i
[PROOF STEP]
show " list_all2 r ss ss"
[PROOF STATE]
proof (prove)
using this:
\<forall>i<length ss. ss ! i \<sqsubseteq>\<^bsub>r\<^esub> ss ! i

goal (1 subgoal):
 1. list_all2 r ss ss
[PROOF STEP]
by (auto simp add:lesssub_def lesub_def intro: list_all2_all_nthI)
[PROOF STATE]
proof (state)
this:
list_all2 r ss ss

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma iter_dom:
 assumes "wf_dom ss0 w0"
 shows "iter f step ss0 w0 = (ss',w') \<longrightarrow>
        wf_dom ss' w' \<and>
        stables r step ss' \<and>
        ss0 [\<sqsubseteq>\<^sub>r] ss' \<and>
        (\<forall>ts\<in>nlists n A. ss0 [\<sqsubseteq>\<^sub>r] ts \<and> stables r step ts \<longrightarrow> ss' [\<sqsubseteq>\<^sub>r] ts)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iter f step ss0 w0 = (ss', w') \<longrightarrow> wf_dom ss' w' \<and> stables r step ss' \<and> ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ss' \<and> (\<forall>ts\<in>nlists n A. ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> stables r step ts \<longrightarrow> ss' [\<sqsubseteq>\<^bsub>r\<^esub>] ts)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
wf_dom ss0 w0

goal (1 subgoal):
 1. iter f step ss0 w0 = (ss', w') \<longrightarrow> wf_dom ss' w' \<and> stables r step ss' \<and> ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ss' \<and> (\<forall>ts\<in>nlists n A. ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> stables r step ts \<longrightarrow> ss' [\<sqsubseteq>\<^bsub>r\<^esub>] ts)
[PROOF STEP]
apply (unfold iter_def stables_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_dom ss0 w0 \<Longrightarrow> while (\<lambda>(\<tau>s, w). w \<noteq> []) (\<lambda>(\<tau>s, w). let p = hd w in propa f (step p (\<tau>s ! p)) \<tau>s (tl w)) (ss0, w0) = (ss', w') \<longrightarrow> wf_dom ss' w' \<and> (\<forall>p<length ss'. Typing_Framework_1.stable r step ss' p) \<and> ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ss' \<and> (\<forall>ts\<in>nlists n A. ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> (\<forall>p<length ts. Typing_Framework_1.stable r step ts p) \<longrightarrow> ss' [\<sqsubseteq>\<^bsub>r\<^esub>] ts)
[PROOF STEP]
apply (rule_tac P = "\<lambda>(ss,w). wf_dom ss w \<and> ss0 [\<sqsubseteq>\<^sub>r] ss \<and> (\<forall>ts\<in>nlists n A. ss0 [\<sqsubseteq>\<^sub>r] ts \<and> stables r step ts \<longrightarrow> ss [\<sqsubseteq>\<^sub>r] ts)"
              and r =  "{(ss',ss). ss [\<sqsubset>\<^sub>r] ss'} <*lex*> (\<lambda>(x,y). (sorted_list_of_set x, sorted_list_of_set y)) ` finite_psubset"
         in while_rule)

  \<comment> \<open>Invariant holds initially:\<close>
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. wf_dom ss0 w0 \<Longrightarrow> case (ss0, w0) of (ss, w) \<Rightarrow> wf_dom ss w \<and> ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ss \<and> (\<forall>ts\<in>nlists n A. ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> stables r step ts \<longrightarrow> ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts)
 2. \<And>s. \<lbrakk>wf_dom ss0 w0; case s of (ss, w) \<Rightarrow> wf_dom ss w \<and> ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ss \<and> (\<forall>ts\<in>nlists n A. ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> stables r step ts \<longrightarrow> ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts); case s of (\<tau>s, w) \<Rightarrow> w \<noteq> []\<rbrakk> \<Longrightarrow> case case s of (\<tau>s, w) \<Rightarrow> let p = hd w in propa f (step p (\<tau>s ! p)) \<tau>s (tl w) of (ss, w) \<Rightarrow> wf_dom ss w \<and> ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ss \<and> (\<forall>ts\<in>nlists n A. ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> stables r step ts \<longrightarrow> ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts)
 3. \<And>s. \<lbrakk>wf_dom ss0 w0; case s of (ss, w) \<Rightarrow> wf_dom ss w \<and> ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ss \<and> (\<forall>ts\<in>nlists n A. ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> stables r step ts \<longrightarrow> ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts); \<not> (case s of (\<tau>s, w) \<Rightarrow> w \<noteq> [])\<rbrakk> \<Longrightarrow> s = (ss', w') \<longrightarrow> wf_dom ss' w' \<and> (\<forall>p<length ss'. Typing_Framework_1.stable r step ss' p) \<and> ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ss' \<and> (\<forall>ts\<in>nlists n A. ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> (\<forall>p<length ts. Typing_Framework_1.stable r step ts p) \<longrightarrow> ss' [\<sqsubseteq>\<^bsub>r\<^esub>] ts)
 4. wf_dom ss0 w0 \<Longrightarrow> wf ({(ss', ss). ss [\<sqsubset>\<^bsub>r\<^esub>] ss'} <*lex*> (\<lambda>(x, y). (sorted_list_of_set x, sorted_list_of_set y)) ` finite_psubset)
 5. \<And>s. \<lbrakk>wf_dom ss0 w0; case s of (ss, w) \<Rightarrow> wf_dom ss w \<and> ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ss \<and> (\<forall>ts\<in>nlists n A. ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> stables r step ts \<longrightarrow> ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts); case s of (\<tau>s, w) \<Rightarrow> w \<noteq> []\<rbrakk> \<Longrightarrow> (case s of (\<tau>s, w) \<Rightarrow> let p = hd w in propa f (step p (\<tau>s ! p)) \<tau>s (tl w), s) \<in> {(ss', ss). ss [\<sqsubset>\<^bsub>r\<^esub>] ss'} <*lex*> (\<lambda>(x, y). (sorted_list_of_set x, sorted_list_of_set y)) ` finite_psubset
[PROOF STEP]
apply(fastforce simp add: wf_dom_def intro:wf_dom_le)

  \<comment> \<open>Invariant is preserved:\<close>
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>s. \<lbrakk>wf_dom ss0 w0; case s of (ss, w) \<Rightarrow> wf_dom ss w \<and> ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ss \<and> (\<forall>ts\<in>nlists n A. ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> stables r step ts \<longrightarrow> ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts); case s of (\<tau>s, w) \<Rightarrow> w \<noteq> []\<rbrakk> \<Longrightarrow> case case s of (\<tau>s, w) \<Rightarrow> let p = hd w in propa f (step p (\<tau>s ! p)) \<tau>s (tl w) of (ss, w) \<Rightarrow> wf_dom ss w \<and> ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ss \<and> (\<forall>ts\<in>nlists n A. ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> stables r step ts \<longrightarrow> ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts)
 2. \<And>s. \<lbrakk>wf_dom ss0 w0; case s of (ss, w) \<Rightarrow> wf_dom ss w \<and> ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ss \<and> (\<forall>ts\<in>nlists n A. ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> stables r step ts \<longrightarrow> ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts); \<not> (case s of (\<tau>s, w) \<Rightarrow> w \<noteq> [])\<rbrakk> \<Longrightarrow> s = (ss', w') \<longrightarrow> wf_dom ss' w' \<and> (\<forall>p<length ss'. Typing_Framework_1.stable r step ss' p) \<and> ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ss' \<and> (\<forall>ts\<in>nlists n A. ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> (\<forall>p<length ts. Typing_Framework_1.stable r step ts p) \<longrightarrow> ss' [\<sqsubseteq>\<^bsub>r\<^esub>] ts)
 3. wf_dom ss0 w0 \<Longrightarrow> wf ({(ss', ss). ss [\<sqsubset>\<^bsub>r\<^esub>] ss'} <*lex*> (\<lambda>(x, y). (sorted_list_of_set x, sorted_list_of_set y)) ` finite_psubset)
 4. \<And>s. \<lbrakk>wf_dom ss0 w0; case s of (ss, w) \<Rightarrow> wf_dom ss w \<and> ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ss \<and> (\<forall>ts\<in>nlists n A. ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> stables r step ts \<longrightarrow> ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts); case s of (\<tau>s, w) \<Rightarrow> w \<noteq> []\<rbrakk> \<Longrightarrow> (case s of (\<tau>s, w) \<Rightarrow> let p = hd w in propa f (step p (\<tau>s ! p)) \<tau>s (tl w), s) \<in> {(ss', ss). ss [\<sqsubset>\<^bsub>r\<^esub>] ss'} <*lex*> (\<lambda>(x, y). (sorted_list_of_set x, sorted_list_of_set y)) ` finite_psubset
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a b ss w. \<lbrakk>wf_dom ss0 w0; b \<noteq> []; propa f (step (hd b) (a ! hd b)) a (tl b) = (ss, w); wf_dom a b; ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] a; \<forall>ts\<in>nlists n A. ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> stables r step ts \<longrightarrow> a [\<sqsubseteq>\<^bsub>r\<^esub>] ts\<rbrakk> \<Longrightarrow> wf_dom ss w \<and> ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ss \<and> (\<forall>ts\<in>nlists n A. ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> stables r step ts \<longrightarrow> ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts)
 2. \<And>s. \<lbrakk>wf_dom ss0 w0; case s of (ss, w) \<Rightarrow> wf_dom ss w \<and> ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ss \<and> (\<forall>ts\<in>nlists n A. ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> stables r step ts \<longrightarrow> ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts); \<not> (case s of (\<tau>s, w) \<Rightarrow> w \<noteq> [])\<rbrakk> \<Longrightarrow> s = (ss', w') \<longrightarrow> wf_dom ss' w' \<and> (\<forall>p<length ss'. Typing_Framework_1.stable r step ss' p) \<and> ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ss' \<and> (\<forall>ts\<in>nlists n A. ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> (\<forall>p<length ts. Typing_Framework_1.stable r step ts p) \<longrightarrow> ss' [\<sqsubseteq>\<^bsub>r\<^esub>] ts)
 3. wf_dom ss0 w0 \<Longrightarrow> wf ({(ss', ss). ss [\<sqsubset>\<^bsub>r\<^esub>] ss'} <*lex*> (\<lambda>(x, y). (sorted_list_of_set x, sorted_list_of_set y)) ` finite_psubset)
 4. \<And>s. \<lbrakk>wf_dom ss0 w0; case s of (ss, w) \<Rightarrow> wf_dom ss w \<and> ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ss \<and> (\<forall>ts\<in>nlists n A. ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> stables r step ts \<longrightarrow> ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts); case s of (\<tau>s, w) \<Rightarrow> w \<noteq> []\<rbrakk> \<Longrightarrow> (case s of (\<tau>s, w) \<Rightarrow> let p = hd w in propa f (step p (\<tau>s ! p)) \<tau>s (tl w), s) \<in> {(ss', ss). ss [\<sqsubset>\<^bsub>r\<^esub>] ss'} <*lex*> (\<lambda>(x, y). (sorted_list_of_set x, sorted_list_of_set y)) ` finite_psubset
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>a b ss w. \<lbrakk>wf_dom ss0 w0; b \<noteq> []; propa f (step (hd b) (a ! hd b)) a (tl b) = (ss, w); wf_dom a b; ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] a; \<forall>ts\<in>nlists n A. ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> stables r step ts \<longrightarrow> a [\<sqsubseteq>\<^bsub>r\<^esub>] ts\<rbrakk> \<Longrightarrow> wf_dom ss w
 2. \<And>a b ss w. \<lbrakk>wf_dom ss0 w0; b \<noteq> []; propa f (step (hd b) (a ! hd b)) a (tl b) = (ss, w); wf_dom a b; ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] a; \<forall>ts\<in>nlists n A. ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> stables r step ts \<longrightarrow> a [\<sqsubseteq>\<^bsub>r\<^esub>] ts\<rbrakk> \<Longrightarrow> ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ss \<and> (\<forall>ts\<in>nlists n A. ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> stables r step ts \<longrightarrow> ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts)
 3. \<And>s. \<lbrakk>wf_dom ss0 w0; case s of (ss, w) \<Rightarrow> wf_dom ss w \<and> ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ss \<and> (\<forall>ts\<in>nlists n A. ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> stables r step ts \<longrightarrow> ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts); \<not> (case s of (\<tau>s, w) \<Rightarrow> w \<noteq> [])\<rbrakk> \<Longrightarrow> s = (ss', w') \<longrightarrow> wf_dom ss' w' \<and> (\<forall>p<length ss'. Typing_Framework_1.stable r step ss' p) \<and> ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ss' \<and> (\<forall>ts\<in>nlists n A. ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> (\<forall>p<length ts. Typing_Framework_1.stable r step ts p) \<longrightarrow> ss' [\<sqsubseteq>\<^bsub>r\<^esub>] ts)
 4. wf_dom ss0 w0 \<Longrightarrow> wf ({(ss', ss). ss [\<sqsubset>\<^bsub>r\<^esub>] ss'} <*lex*> (\<lambda>(x, y). (sorted_list_of_set x, sorted_list_of_set y)) ` finite_psubset)
 5. \<And>s. \<lbrakk>wf_dom ss0 w0; case s of (ss, w) \<Rightarrow> wf_dom ss w \<and> ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ss \<and> (\<forall>ts\<in>nlists n A. ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> stables r step ts \<longrightarrow> ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts); case s of (\<tau>s, w) \<Rightarrow> w \<noteq> []\<rbrakk> \<Longrightarrow> (case s of (\<tau>s, w) \<Rightarrow> let p = hd w in propa f (step p (\<tau>s ! p)) \<tau>s (tl w), s) \<in> {(ss', ss). ss [\<sqsubset>\<^bsub>r\<^esub>] ss'} <*lex*> (\<lambda>(x, y). (sorted_list_of_set x, sorted_list_of_set y)) ` finite_psubset
[PROOF STEP]
apply(fastforce dest:propa_dom_invariant)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a b ss w. \<lbrakk>wf_dom ss0 w0; b \<noteq> []; propa f (step (hd b) (a ! hd b)) a (tl b) = (ss, w); wf_dom a b; ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] a; \<forall>ts\<in>nlists n A. ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> stables r step ts \<longrightarrow> a [\<sqsubseteq>\<^bsub>r\<^esub>] ts\<rbrakk> \<Longrightarrow> ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ss \<and> (\<forall>ts\<in>nlists n A. ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> stables r step ts \<longrightarrow> ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts)
 2. \<And>s. \<lbrakk>wf_dom ss0 w0; case s of (ss, w) \<Rightarrow> wf_dom ss w \<and> ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ss \<and> (\<forall>ts\<in>nlists n A. ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> stables r step ts \<longrightarrow> ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts); \<not> (case s of (\<tau>s, w) \<Rightarrow> w \<noteq> [])\<rbrakk> \<Longrightarrow> s = (ss', w') \<longrightarrow> wf_dom ss' w' \<and> (\<forall>p<length ss'. Typing_Framework_1.stable r step ss' p) \<and> ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ss' \<and> (\<forall>ts\<in>nlists n A. ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> (\<forall>p<length ts. Typing_Framework_1.stable r step ts p) \<longrightarrow> ss' [\<sqsubseteq>\<^bsub>r\<^esub>] ts)
 3. wf_dom ss0 w0 \<Longrightarrow> wf ({(ss', ss). ss [\<sqsubset>\<^bsub>r\<^esub>] ss'} <*lex*> (\<lambda>(x, y). (sorted_list_of_set x, sorted_list_of_set y)) ` finite_psubset)
 4. \<And>s. \<lbrakk>wf_dom ss0 w0; case s of (ss, w) \<Rightarrow> wf_dom ss w \<and> ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ss \<and> (\<forall>ts\<in>nlists n A. ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> stables r step ts \<longrightarrow> ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts); case s of (\<tau>s, w) \<Rightarrow> w \<noteq> []\<rbrakk> \<Longrightarrow> (case s of (\<tau>s, w) \<Rightarrow> let p = hd w in propa f (step p (\<tau>s ! p)) \<tau>s (tl w), s) \<in> {(ss', ss). ss [\<sqsubset>\<^bsub>r\<^esub>] ss'} <*lex*> (\<lambda>(x, y). (sorted_list_of_set x, sorted_list_of_set y)) ` finite_psubset
[PROOF STEP]
apply(simp add:stables_def)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a b ss w. \<lbrakk>wf_dom ss0 w0; b \<noteq> []; propa f (step (hd b) (a ! hd b)) a (tl b) = (ss, w); wf_dom a b; ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] a; \<forall>ts\<in>nlists n A. ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> (\<forall>p<n. Typing_Framework_1.stable r step ts p) \<longrightarrow> a [\<sqsubseteq>\<^bsub>r\<^esub>] ts\<rbrakk> \<Longrightarrow> ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ss \<and> (\<forall>ts\<in>nlists n A. ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> (\<forall>p<n. Typing_Framework_1.stable r step ts p) \<longrightarrow> ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts)
 2. \<And>s. \<lbrakk>wf_dom ss0 w0; case s of (ss, w) \<Rightarrow> wf_dom ss w \<and> ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ss \<and> (\<forall>ts\<in>nlists n A. ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> stables r step ts \<longrightarrow> ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts); \<not> (case s of (\<tau>s, w) \<Rightarrow> w \<noteq> [])\<rbrakk> \<Longrightarrow> s = (ss', w') \<longrightarrow> wf_dom ss' w' \<and> (\<forall>p<length ss'. Typing_Framework_1.stable r step ss' p) \<and> ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ss' \<and> (\<forall>ts\<in>nlists n A. ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> (\<forall>p<length ts. Typing_Framework_1.stable r step ts p) \<longrightarrow> ss' [\<sqsubseteq>\<^bsub>r\<^esub>] ts)
 3. wf_dom ss0 w0 \<Longrightarrow> wf ({(ss', ss). ss [\<sqsubset>\<^bsub>r\<^esub>] ss'} <*lex*> (\<lambda>(x, y). (sorted_list_of_set x, sorted_list_of_set y)) ` finite_psubset)
 4. \<And>s. \<lbrakk>wf_dom ss0 w0; case s of (ss, w) \<Rightarrow> wf_dom ss w \<and> ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ss \<and> (\<forall>ts\<in>nlists n A. ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> stables r step ts \<longrightarrow> ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts); case s of (\<tau>s, w) \<Rightarrow> w \<noteq> []\<rbrakk> \<Longrightarrow> (case s of (\<tau>s, w) \<Rightarrow> let p = hd w in propa f (step p (\<tau>s ! p)) \<tau>s (tl w), s) \<in> {(ss', ss). ss [\<sqsubset>\<^bsub>r\<^esub>] ss'} <*lex*> (\<lambda>(x, y). (sorted_list_of_set x, sorted_list_of_set y)) ` finite_psubset
[PROOF STEP]
apply (rule propa_dom_invariant_aux2)
[PROOF STATE]
proof (prove)
goal (9 subgoals):
 1. \<And>a b ss w. \<lbrakk>wf_dom ss0 w0; b \<noteq> []; propa f (step (hd b) (a ! hd b)) a (tl b) = (ss, w); wf_dom a b; ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] a; \<forall>ts\<in>nlists n A. ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> (\<forall>p<n. Typing_Framework_1.stable r step ts p) \<longrightarrow> a [\<sqsubseteq>\<^bsub>r\<^esub>] ts\<rbrakk> \<Longrightarrow> wf_dom ss0 (?w0.124 a b ss w)
 2. \<And>a b ss w. \<lbrakk>wf_dom ss0 w0; b \<noteq> []; propa f (step (hd b) (a ! hd b)) a (tl b) = (ss, w); wf_dom a b; ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] a; \<forall>ts\<in>nlists n A. ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> (\<forall>p<n. Typing_Framework_1.stable r step ts p) \<longrightarrow> a [\<sqsubseteq>\<^bsub>r\<^esub>] ts\<rbrakk> \<Longrightarrow> ?w124 a b ss w \<noteq> []
 3. \<And>a b ss w. \<lbrakk>wf_dom ss0 w0; b \<noteq> []; propa f (step (hd b) (a ! hd b)) a (tl b) = (ss, w); wf_dom a b; ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] a; \<forall>ts\<in>nlists n A. ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> (\<forall>p<n. Typing_Framework_1.stable r step ts p) \<longrightarrow> a [\<sqsubseteq>\<^bsub>r\<^esub>] ts\<rbrakk> \<Longrightarrow> propa f (step (hd (?w124 a b ss w)) (?ss124 a b ss w ! hd (?w124 a b ss w))) (?ss124 a b ss w) (tl (?w124 a b ss w)) = (ss, ?wa124 a b ss w)
 4. \<And>a b ss w. \<lbrakk>wf_dom ss0 w0; b \<noteq> []; propa f (step (hd b) (a ! hd b)) a (tl b) = (ss, w); wf_dom a b; ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] a; \<forall>ts\<in>nlists n A. ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> (\<forall>p<n. Typing_Framework_1.stable r step ts p) \<longrightarrow> a [\<sqsubseteq>\<^bsub>r\<^esub>] ts\<rbrakk> \<Longrightarrow> wf_dom (?ss124 a b ss w) (?w124 a b ss w)
 5. \<And>a b ss w. \<lbrakk>wf_dom ss0 w0; b \<noteq> []; propa f (step (hd b) (a ! hd b)) a (tl b) = (ss, w); wf_dom a b; ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] a; \<forall>ts\<in>nlists n A. ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> (\<forall>p<n. Typing_Framework_1.stable r step ts p) \<longrightarrow> a [\<sqsubseteq>\<^bsub>r\<^esub>] ts\<rbrakk> \<Longrightarrow> ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ?ss124 a b ss w
 6. \<And>a b ss w. \<lbrakk>wf_dom ss0 w0; b \<noteq> []; propa f (step (hd b) (a ! hd b)) a (tl b) = (ss, w); wf_dom a b; ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] a; \<forall>ts\<in>nlists n A. ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> (\<forall>p<n. Typing_Framework_1.stable r step ts p) \<longrightarrow> a [\<sqsubseteq>\<^bsub>r\<^esub>] ts\<rbrakk> \<Longrightarrow> \<forall>ts\<in>nlists n A. ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> (\<forall>p<n. Typing_Framework_1.stable r step ts p) \<longrightarrow> ?ss124 a b ss w [\<sqsubseteq>\<^bsub>r\<^esub>] ts
 7. \<And>s. \<lbrakk>wf_dom ss0 w0; case s of (ss, w) \<Rightarrow> wf_dom ss w \<and> ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ss \<and> (\<forall>ts\<in>nlists n A. ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> stables r step ts \<longrightarrow> ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts); \<not> (case s of (\<tau>s, w) \<Rightarrow> w \<noteq> [])\<rbrakk> \<Longrightarrow> s = (ss', w') \<longrightarrow> wf_dom ss' w' \<and> (\<forall>p<length ss'. Typing_Framework_1.stable r step ss' p) \<and> ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ss' \<and> (\<forall>ts\<in>nlists n A. ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> (\<forall>p<length ts. Typing_Framework_1.stable r step ts p) \<longrightarrow> ss' [\<sqsubseteq>\<^bsub>r\<^esub>] ts)
 8. wf_dom ss0 w0 \<Longrightarrow> wf ({(ss', ss). ss [\<sqsubset>\<^bsub>r\<^esub>] ss'} <*lex*> (\<lambda>(x, y). (sorted_list_of_set x, sorted_list_of_set y)) ` finite_psubset)
 9. \<And>s. \<lbrakk>wf_dom ss0 w0; case s of (ss, w) \<Rightarrow> wf_dom ss w \<and> ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ss \<and> (\<forall>ts\<in>nlists n A. ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> stables r step ts \<longrightarrow> ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts); case s of (\<tau>s, w) \<Rightarrow> w \<noteq> []\<rbrakk> \<Longrightarrow> (case s of (\<tau>s, w) \<Rightarrow> let p = hd w in propa f (step p (\<tau>s ! p)) \<tau>s (tl w), s) \<in> {(ss', ss). ss [\<sqsubset>\<^bsub>r\<^esub>] ss'} <*lex*> (\<lambda>(x, y). (sorted_list_of_set x, sorted_list_of_set y)) ` finite_psubset
[PROOF STEP]
apply assumption+

  \<comment> \<open>Postcondition holds upon termination:\<close>
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>wf_dom ss0 w0; case s of (ss, w) \<Rightarrow> wf_dom ss w \<and> ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ss \<and> (\<forall>ts\<in>nlists n A. ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> stables r step ts \<longrightarrow> ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts); \<not> (case s of (\<tau>s, w) \<Rightarrow> w \<noteq> [])\<rbrakk> \<Longrightarrow> s = (ss', w') \<longrightarrow> wf_dom ss' w' \<and> (\<forall>p<length ss'. Typing_Framework_1.stable r step ss' p) \<and> ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ss' \<and> (\<forall>ts\<in>nlists n A. ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> (\<forall>p<length ts. Typing_Framework_1.stable r step ts p) \<longrightarrow> ss' [\<sqsubseteq>\<^bsub>r\<^esub>] ts)
 2. wf_dom ss0 w0 \<Longrightarrow> wf ({(ss', ss). ss [\<sqsubset>\<^bsub>r\<^esub>] ss'} <*lex*> (\<lambda>(x, y). (sorted_list_of_set x, sorted_list_of_set y)) ` finite_psubset)
 3. \<And>s. \<lbrakk>wf_dom ss0 w0; case s of (ss, w) \<Rightarrow> wf_dom ss w \<and> ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ss \<and> (\<forall>ts\<in>nlists n A. ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> stables r step ts \<longrightarrow> ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts); case s of (\<tau>s, w) \<Rightarrow> w \<noteq> []\<rbrakk> \<Longrightarrow> (case s of (\<tau>s, w) \<Rightarrow> let p = hd w in propa f (step p (\<tau>s ! p)) \<tau>s (tl w), s) \<in> {(ss', ss). ss [\<sqsubset>\<^bsub>r\<^esub>] ss'} <*lex*> (\<lambda>(x, y). (sorted_list_of_set x, sorted_list_of_set y)) ` finite_psubset
[PROOF STEP]
apply(clarsimp simp add: stables_def split_paired_all)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>p. \<lbrakk>wf_dom ss0 w0; wf_dom ss' []; ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ss'; \<forall>ts\<in>nlists n A. ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> (\<forall>p<n. Typing_Framework_1.stable r step ts p) \<longrightarrow> ss' [\<sqsubseteq>\<^bsub>r\<^esub>] ts; w' = []; p < length ss0\<rbrakk> \<Longrightarrow> Typing_Framework_1.stable r step ss' p
 2. wf_dom ss0 w0 \<Longrightarrow> wf ({(ss', ss). ss [\<sqsubset>\<^bsub>r\<^esub>] ss'} <*lex*> (\<lambda>(x, y). (sorted_list_of_set x, sorted_list_of_set y)) ` finite_psubset)
 3. \<And>s. \<lbrakk>wf_dom ss0 w0; case s of (ss, w) \<Rightarrow> wf_dom ss w \<and> ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ss \<and> (\<forall>ts\<in>nlists n A. ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> stables r step ts \<longrightarrow> ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts); case s of (\<tau>s, w) \<Rightarrow> w \<noteq> []\<rbrakk> \<Longrightarrow> (case s of (\<tau>s, w) \<Rightarrow> let p = hd w in propa f (step p (\<tau>s ! p)) \<tau>s (tl w), s) \<in> {(ss', ss). ss [\<sqsubset>\<^bsub>r\<^esub>] ss'} <*lex*> (\<lambda>(x, y). (sorted_list_of_set x, sorted_list_of_set y)) ` finite_psubset
[PROOF STEP]
apply(subgoal_tac "length ss0 = n")
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>p. \<lbrakk>wf_dom ss0 w0; wf_dom ss' []; ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ss'; \<forall>ts\<in>nlists n A. ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> (\<forall>p<n. Typing_Framework_1.stable r step ts p) \<longrightarrow> ss' [\<sqsubseteq>\<^bsub>r\<^esub>] ts; w' = []; p < length ss0; length ss0 = n\<rbrakk> \<Longrightarrow> Typing_Framework_1.stable r step ss' p
 2. \<And>p. \<lbrakk>wf_dom ss0 w0; wf_dom ss' []; ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ss'; \<forall>ts\<in>nlists n A. ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> (\<forall>p<n. Typing_Framework_1.stable r step ts p) \<longrightarrow> ss' [\<sqsubseteq>\<^bsub>r\<^esub>] ts; w' = []; p < length ss0\<rbrakk> \<Longrightarrow> length ss0 = n
 3. wf_dom ss0 w0 \<Longrightarrow> wf ({(ss', ss). ss [\<sqsubset>\<^bsub>r\<^esub>] ss'} <*lex*> (\<lambda>(x, y). (sorted_list_of_set x, sorted_list_of_set y)) ` finite_psubset)
 4. \<And>s. \<lbrakk>wf_dom ss0 w0; case s of (ss, w) \<Rightarrow> wf_dom ss w \<and> ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ss \<and> (\<forall>ts\<in>nlists n A. ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> stables r step ts \<longrightarrow> ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts); case s of (\<tau>s, w) \<Rightarrow> w \<noteq> []\<rbrakk> \<Longrightarrow> (case s of (\<tau>s, w) \<Rightarrow> let p = hd w in propa f (step p (\<tau>s ! p)) \<tau>s (tl w), s) \<in> {(ss', ss). ss [\<sqsubset>\<^bsub>r\<^esub>] ss'} <*lex*> (\<lambda>(x, y). (sorted_list_of_set x, sorted_list_of_set y)) ` finite_psubset
[PROOF STEP]
apply(simp add:wf_dom_def)+

  \<comment> \<open>Well-foundedness of the termination relation:\<close>
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (\<forall>\<tau>\<in>set ss0. \<tau> \<in> A) \<and> (\<forall>p<n. Sorted_Less.sorted (rev (ss0 ! p)) \<and> (ss0 ! p \<noteq> rev [0..<n] \<longrightarrow> (\<forall>x\<in>set (ss0 ! p). x < p)) \<and> (ss0 ! p = rev [0..<n] \<longrightarrow> (\<exists>x\<in>set w0. (x, p) \<in> g_E G \<and> x < p)) \<and> (p \<notin> set w0 \<longrightarrow> Typing_Framework_1.stable r step ss0 p)) \<and> Sorted_Less.sorted w0 \<and> length ss0 = n \<and> (\<forall>x\<in>set w0. x < n) \<Longrightarrow> wf ({(ss', ss). ss [\<sqsubset>\<^bsub>r\<^esub>] ss'} <*lex*> (\<lambda>x. case x of (x, y) \<Rightarrow> (sorted_list_of_set x, sorted_list_of_set y)) ` finite_psubset)
 2. \<And>s. \<lbrakk>wf_dom ss0 w0; case s of (ss, w) \<Rightarrow> wf_dom ss w \<and> ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ss \<and> (\<forall>ts\<in>nlists n A. ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> stables r step ts \<longrightarrow> ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts); case s of (\<tau>s, w) \<Rightarrow> w \<noteq> []\<rbrakk> \<Longrightarrow> (case s of (\<tau>s, w) \<Rightarrow> let p = hd w in propa f (step p (\<tau>s ! p)) \<tau>s (tl w), s) \<in> {(ss', ss). ss [\<sqsubset>\<^bsub>r\<^esub>] ss'} <*lex*> (\<lambda>(x, y). (sorted_list_of_set x, sorted_list_of_set y)) ` finite_psubset
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>\<tau>\<in>set ss0. \<tau> \<in> A; \<forall>p<length ss0. Sorted_Less.sorted (rev (ss0 ! p)) \<and> (ss0 ! p \<noteq> rev [0..<length ss0] \<longrightarrow> (\<forall>x\<in>set (ss0 ! p). x < p)) \<and> (ss0 ! p = rev [0..<length ss0] \<longrightarrow> (\<exists>x\<in>set w0. (x, p) \<in> g_E G \<and> x < p)) \<and> (p \<notin> set w0 \<longrightarrow> Typing_Framework_1.stable r step ss0 p); Sorted_Less.sorted w0; \<forall>x\<in>set w0. x < length ss0; n = length ss0\<rbrakk> \<Longrightarrow> wf ({(ss', ss). ss [\<sqsubset>\<^bsub>r\<^esub>] ss'} <*lex*> (\<lambda>x. case x of (x, y) \<Rightarrow> (sorted_list_of_set x, sorted_list_of_set y)) ` finite_psubset)
 2. \<And>s. \<lbrakk>wf_dom ss0 w0; case s of (ss, w) \<Rightarrow> wf_dom ss w \<and> ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ss \<and> (\<forall>ts\<in>nlists n A. ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> stables r step ts \<longrightarrow> ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts); case s of (\<tau>s, w) \<Rightarrow> w \<noteq> []\<rbrakk> \<Longrightarrow> (case s of (\<tau>s, w) \<Rightarrow> let p = hd w in propa f (step p (\<tau>s ! p)) \<tau>s (tl w), s) \<in> {(ss', ss). ss [\<sqsubset>\<^bsub>r\<^esub>] ss'} <*lex*> (\<lambda>(x, y). (sorted_list_of_set x, sorted_list_of_set y)) ` finite_psubset
[PROOF STEP]
apply(simp add:wf_listn_termination_rel)

  \<comment> \<open>Loop decreases along termination relation:\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>wf_dom ss0 w0; case s of (ss, w) \<Rightarrow> wf_dom ss w \<and> ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ss \<and> (\<forall>ts\<in>nlists n A. ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> stables r step ts \<longrightarrow> ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts); case s of (\<tau>s, w) \<Rightarrow> w \<noteq> []\<rbrakk> \<Longrightarrow> (case s of (\<tau>s, w) \<Rightarrow> let p = hd w in propa f (step p (\<tau>s ! p)) \<tau>s (tl w), s) \<in> {(ss', ss). ss [\<sqsubset>\<^bsub>r\<^esub>] ss'} <*lex*> (\<lambda>(x, y). (sorted_list_of_set x, sorted_list_of_set y)) ` finite_psubset
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>wf_dom ss0 w0; b \<noteq> []; wf_dom a b; ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] a; \<forall>ts\<in>nlists n A. ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> stables r step ts \<longrightarrow> a [\<sqsubseteq>\<^bsub>r\<^esub>] ts\<rbrakk> \<Longrightarrow> (propa f (step (hd b) (a ! hd b)) a (tl b), a, b) \<in> {(ss', ss). ss [\<sqsubset>\<^bsub>r\<^esub>] ss'} <*lex*> (\<lambda>x. case x of (x, y) \<Rightarrow> (sorted_list_of_set x, sorted_list_of_set y)) ` finite_psubset
[PROOF STEP]
apply (fastforce intro:propa_termination)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma wf_start: "wf_dom start (unstables r step start)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_dom start (unstables r step start)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. wf_dom start (unstables r step start)
[PROOF STEP]
let ?w0 = "unstables r step start"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. wf_dom start (unstables r step start)
[PROOF STEP]
have sorted_w: "sorted ?w0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Sorted_Less.sorted (unstables r step start)
[PROOF STEP]
using unstables_def
[PROOF STATE]
proof (prove)
using this:
unstables ?r ?step ?\<tau>s = sorted_list_of_set {p. p < length ?\<tau>s \<and> \<not> Typing_Framework_1.stable ?r ?step ?\<tau>s p}

goal (1 subgoal):
 1. Sorted_Less.sorted (unstables r step start)
[PROOF STEP]
by (simp add:sorted_less_sorted_list_of_set)
[PROOF STATE]
proof (state)
this:
Sorted_Less.sorted (unstables r step start)

goal (1 subgoal):
 1. wf_dom start (unstables r step start)
[PROOF STEP]
have w0_lt_n: "\<forall>x\<in>set ?w0. x < n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>set (unstables r step start). x < n
[PROOF STEP]
using unstables_def len_start_is_n
[PROOF STATE]
proof (prove)
using this:
unstables ?r ?step ?\<tau>s = sorted_list_of_set {p. p < length ?\<tau>s \<and> \<not> Typing_Framework_1.stable ?r ?step ?\<tau>s p}
length start = n

goal (1 subgoal):
 1. \<forall>x\<in>set (unstables r step start). x < n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>set (unstables r step start). x < n

goal (1 subgoal):
 1. wf_dom start (unstables r step start)
[PROOF STEP]
have neq_all: "\<forall>p < n. start!p \<noteq> rev [0..< n] \<longrightarrow> (\<forall>x\<in>set (start!p). x < p) "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>p<n. start ! p \<noteq> rev [0..<n] \<longrightarrow> (\<forall>x\<in>set (start ! p). x < p)
[PROOF STEP]
proof(intro strip)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p x. \<lbrakk>p < n; start ! p \<noteq> rev [0..<n]; x \<in> set (start ! p)\<rbrakk> \<Longrightarrow> x < p
[PROOF STEP]
fix p x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p x. \<lbrakk>p < n; start ! p \<noteq> rev [0..<n]; x \<in> set (start ! p)\<rbrakk> \<Longrightarrow> x < p
[PROOF STEP]
assume p_lt_n: "p < n" and p_neq_all: "start ! p \<noteq> rev [0..< n]" and x_in: "x \<in> set (start ! p)"
[PROOF STATE]
proof (state)
this:
p < n
start ! p \<noteq> rev [0..<n]
x \<in> set (start ! p)

goal (1 subgoal):
 1. \<And>p x. \<lbrakk>p < n; start ! p \<noteq> rev [0..<n]; x \<in> set (start ! p)\<rbrakk> \<Longrightarrow> x < p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p < n
start ! p \<noteq> rev [0..<n]
x \<in> set (start ! p)
[PROOF STEP]
have "p = 0"
[PROOF STATE]
proof (prove)
using this:
p < n
start ! p \<noteq> rev [0..<n]
x \<in> set (start ! p)

goal (1 subgoal):
 1. p = 0
[PROOF STEP]
using start_nth_lt0_all len_start_is_n
[PROOF STATE]
proof (prove)
using this:
p < n
start ! p \<noteq> rev [0..<n]
x \<in> set (start ! p)
\<forall>p\<in>{1..<length start}. start ! p = rev [0..<n]
length start = n

goal (1 subgoal):
 1. p = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p = 0

goal (1 subgoal):
 1. \<And>p x. \<lbrakk>p < n; start ! p \<noteq> rev [0..<n]; x \<in> set (start ! p)\<rbrakk> \<Longrightarrow> x < p
[PROOF STEP]
with start_nth0_empty
[PROOF STATE]
proof (chain)
picking this:
start ! 0 = []
p = 0
[PROOF STEP]
show "x < p"
[PROOF STATE]
proof (prove)
using this:
start ! 0 = []
p = 0

goal (1 subgoal):
 1. x < p
[PROOF STEP]
using x_in
[PROOF STATE]
proof (prove)
using this:
start ! 0 = []
p = 0
x \<in> set (start ! p)

goal (1 subgoal):
 1. x < p
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x < p

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>p<n. start ! p \<noteq> rev [0..<n] \<longrightarrow> (\<forall>x\<in>set (start ! p). x < p)

goal (1 subgoal):
 1. wf_dom start (unstables r step start)
[PROOF STEP]
have eq_all:"(\<forall>p < n. start!p = rev [0..< n] \<longrightarrow> (\<exists>x\<in> set ?w0. (x,p)\<in> g_E G \<and> x < p))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>p<n. start ! p = rev [0..<n] \<longrightarrow> (\<exists>x\<in>set (unstables r step start). (x, p) \<in> g_E G \<and> x < p)
[PROOF STEP]
proof(intro strip)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>p < n; start ! p = rev [0..<n]\<rbrakk> \<Longrightarrow> \<exists>x\<in>set (unstables r step start). (x, p) \<in> g_E G \<and> x < p
[PROOF STEP]
fix p
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>p < n; start ! p = rev [0..<n]\<rbrakk> \<Longrightarrow> \<exists>x\<in>set (unstables r step start). (x, p) \<in> g_E G \<and> x < p
[PROOF STEP]
assume p_lt_n: "p < n" and p_eq_all: "start ! p = rev [0..< n]"
[PROOF STATE]
proof (state)
this:
p < n
start ! p = rev [0..<n]

goal (1 subgoal):
 1. \<And>p. \<lbrakk>p < n; start ! p = rev [0..<n]\<rbrakk> \<Longrightarrow> \<exists>x\<in>set (unstables r step start). (x, p) \<in> g_E G \<and> x < p
[PROOF STEP]
from \<open>p < n\<close>
[PROOF STATE]
proof (chain)
picking this:
p < n
[PROOF STEP]
have "p = 0 \<or> p > 0 \<and> p < length start"
[PROOF STATE]
proof (prove)
using this:
p < n

goal (1 subgoal):
 1. p = 0 \<or> 0 < p \<and> p < length start
[PROOF STEP]
using len_start_is_n
[PROOF STATE]
proof (prove)
using this:
p < n
length start = n

goal (1 subgoal):
 1. p = 0 \<or> 0 < p \<and> p < length start
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p = 0 \<or> 0 < p \<and> p < length start

goal (1 subgoal):
 1. \<And>p. \<lbrakk>p < n; start ! p = rev [0..<n]\<rbrakk> \<Longrightarrow> \<exists>x\<in>set (unstables r step start). (x, p) \<in> g_E G \<and> x < p
[PROOF STEP]
with p_eq_all
[PROOF STATE]
proof (chain)
picking this:
start ! p = rev [0..<n]
p = 0 \<or> 0 < p \<and> p < length start
[PROOF STEP]
have "p > 0" and p_lt_len_start: "p < length start"
[PROOF STATE]
proof (prove)
using this:
start ! p = rev [0..<n]
p = 0 \<or> 0 < p \<and> p < length start

goal (1 subgoal):
 1. 0 < p &&& p < length start
[PROOF STEP]
using start_nth0_empty n_def nodes_def len_verts_gt0
[PROOF STATE]
proof (prove)
using this:
start ! p = rev [0..<n]
p = 0 \<or> 0 < p \<and> p < length start
start ! 0 = []
n \<equiv> length nodes
nodes \<equiv> g_V G
0 < length (g_V G)

goal (1 subgoal):
 1. 0 < p &&& p < length start
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < p
p < length start

goal (1 subgoal):
 1. \<And>p. \<lbrakk>p < n; start ! p = rev [0..<n]\<rbrakk> \<Longrightarrow> \<exists>x\<in>set (unstables r step start). (x, p) \<in> g_E G \<and> x < p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < p
p < length start
[PROOF STEP]
have "p \<in> set (g_V G) - {0}"
[PROOF STATE]
proof (prove)
using this:
0 < p
p < length start

goal (1 subgoal):
 1. p \<in> set (g_V G) - {0}
[PROOF STEP]
using len_start_is_n n_def nodes_def verts_set
[PROOF STATE]
proof (prove)
using this:
0 < p
p < length start
length start = n
n \<equiv> length nodes
nodes \<equiv> g_V G
set (g_V G) = {0..<length (g_V G)}

goal (1 subgoal):
 1. p \<in> set (g_V G) - {0}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p \<in> set (g_V G) - {0}

goal (1 subgoal):
 1. \<And>p. \<lbrakk>p < n; start ! p = rev [0..<n]\<rbrakk> \<Longrightarrow> \<exists>x\<in>set (unstables r step start). (x, p) \<in> g_E G \<and> x < p
[PROOF STEP]
with dfst
[PROOF STATE]
proof (chain)
picking this:
\<forall>v\<in>set (g_V G) - {0}. \<exists>prev. (prev, v) \<in> g_E G \<and> prev < v
p \<in> set (g_V G) - {0}
[PROOF STEP]
obtain prev where "(prev, p) \<in> g_E G" and "prev < p"
[PROOF STATE]
proof (prove)
using this:
\<forall>v\<in>set (g_V G) - {0}. \<exists>prev. (prev, v) \<in> g_E G \<and> prev < v
p \<in> set (g_V G) - {0}

goal (1 subgoal):
 1. (\<And>prev. \<lbrakk>(prev, p) \<in> g_E G; prev < p\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(prev, p) \<in> g_E G
prev < p

goal (1 subgoal):
 1. \<And>p. \<lbrakk>p < n; start ! p = rev [0..<n]\<rbrakk> \<Longrightarrow> \<exists>x\<in>set (unstables r step start). (x, p) \<in> g_E G \<and> x < p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(prev, p) \<in> g_E G
prev < p
[PROOF STEP]
have "succs prev \<noteq> {}" and "prev < length start"
[PROOF STATE]
proof (prove)
using this:
(prev, p) \<in> g_E G
prev < p

goal (1 subgoal):
 1. succs prev \<noteq> {} &&& prev < length start
[PROOF STEP]
using p_lt_len_start
[PROOF STATE]
proof (prove)
using this:
(prev, p) \<in> g_E G
prev < p
p < length start

goal (1 subgoal):
 1. succs prev \<noteq> {} &&& prev < length start
[PROOF STEP]
by (auto simp add:succs_def)
[PROOF STATE]
proof (state)
this:
succs prev \<noteq> {}
prev < length start

goal (1 subgoal):
 1. \<And>p. \<lbrakk>p < n; start ! p = rev [0..<n]\<rbrakk> \<Longrightarrow> \<exists>x\<in>set (unstables r step start). (x, p) \<in> g_E G \<and> x < p
[PROOF STEP]
with unstable_start
[PROOF STATE]
proof (chain)
picking this:
unstables r step start = sorted_list_of_set {p. succs p \<noteq> {} \<and> p < length start}
succs prev \<noteq> {}
prev < length start
[PROOF STEP]
have "prev \<in> set ?w0"
[PROOF STATE]
proof (prove)
using this:
unstables r step start = sorted_list_of_set {p. succs p \<noteq> {} \<and> p < length start}
succs prev \<noteq> {}
prev < length start

goal (1 subgoal):
 1. prev \<in> set (unstables r step start)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
prev \<in> set (unstables r step start)

goal (1 subgoal):
 1. \<And>p. \<lbrakk>p < n; start ! p = rev [0..<n]\<rbrakk> \<Longrightarrow> \<exists>x\<in>set (unstables r step start). (x, p) \<in> g_E G \<and> x < p
[PROOF STEP]
with \<open>(prev, p) \<in> g_E G\<close> \<open>prev < p\<close>
[PROOF STATE]
proof (chain)
picking this:
(prev, p) \<in> g_E G
prev < p
prev \<in> set (unstables r step start)
[PROOF STEP]
show "\<exists>x\<in>set (unstables r step start). (x, p) \<in> g_E G \<and> x < p"
[PROOF STATE]
proof (prove)
using this:
(prev, p) \<in> g_E G
prev < p
prev \<in> set (unstables r step start)

goal (1 subgoal):
 1. \<exists>x\<in>set (unstables r step start). (x, p) \<in> g_E G \<and> x < p
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>x\<in>set (unstables r step start). (x, p) \<in> g_E G \<and> x < p

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>p<n. start ! p = rev [0..<n] \<longrightarrow> (\<exists>x\<in>set (unstables r step start). (x, p) \<in> g_E G \<and> x < p)

goal (1 subgoal):
 1. wf_dom start (unstables r step start)
[PROOF STEP]
have "\<forall>p<n. (p \<notin> set (unstables r step start)\<longrightarrow> stable r step start p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>p<n. p \<notin> set (unstables r step start) \<longrightarrow> Typing_Framework_1.stable r step start p
[PROOF STEP]
by (unfold unstables_def) (simp add:n_def start_def nodes_def)
[PROOF STATE]
proof (state)
this:
\<forall>p<n. p \<notin> set (unstables r step start) \<longrightarrow> Typing_Framework_1.stable r step start p

goal (1 subgoal):
 1. wf_dom start (unstables r step start)
[PROOF STEP]
with sorted_start_nth neq_all eq_all start_subset_A sorted_w len_start_is_n w0_lt_n
[PROOF STATE]
proof (chain)
picking this:
?i < n \<Longrightarrow> Sorted_Less.sorted (rev (start ! ?i))
\<forall>p<n. start ! p \<noteq> rev [0..<n] \<longrightarrow> (\<forall>x\<in>set (start ! p). x < p)
\<forall>p<n. start ! p = rev [0..<n] \<longrightarrow> (\<exists>x\<in>set (unstables r step start). (x, p) \<in> g_E G \<and> x < p)
set start \<subseteq> A
Sorted_Less.sorted (unstables r step start)
length start = n
\<forall>x\<in>set (unstables r step start). x < n
\<forall>p<n. p \<notin> set (unstables r step start) \<longrightarrow> Typing_Framework_1.stable r step start p
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
?i < n \<Longrightarrow> Sorted_Less.sorted (rev (start ! ?i))
\<forall>p<n. start ! p \<noteq> rev [0..<n] \<longrightarrow> (\<forall>x\<in>set (start ! p). x < p)
\<forall>p<n. start ! p = rev [0..<n] \<longrightarrow> (\<exists>x\<in>set (unstables r step start). (x, p) \<in> g_E G \<and> x < p)
set start \<subseteq> A
Sorted_Less.sorted (unstables r step start)
length start = n
\<forall>x\<in>set (unstables r step start). x < n
\<forall>p<n. p \<notin> set (unstables r step start) \<longrightarrow> Typing_Framework_1.stable r step start p

goal (1 subgoal):
 1. wf_dom start (unstables r step start)
[PROOF STEP]
by (auto simp only:wf_dom_def)
[PROOF STATE]
proof (state)
this:
wf_dom start (unstables r step start)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma iter_dom_properties:
 "iter f step start (unstables r step start) = (ss',w') \<longrightarrow>
  wf_dom ss' w' \<and>
  stables r step ss' \<and>
  start [\<sqsubseteq>\<^sub>r] ss' \<and>
  (\<forall>ts\<in>nlists n A. start [\<sqsubseteq>\<^sub>r] ts \<and> stables r step ts \<longrightarrow> ss' [\<sqsubseteq>\<^sub>r] ts)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iter f step start (unstables r step start) = (ss', w') \<longrightarrow> wf_dom ss' w' \<and> stables r step ss' \<and> start [\<sqsubseteq>\<^bsub>r\<^esub>] ss' \<and> (\<forall>ts\<in>nlists n A. start [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> stables r step ts \<longrightarrow> ss' [\<sqsubseteq>\<^bsub>r\<^esub>] ts)
[PROOF STEP]
using iter_dom[OF wf_start]
[PROOF STATE]
proof (prove)
using this:
iter f step start (unstables r step start) = (?ss', ?w') \<longrightarrow> wf_dom ?ss' ?w' \<and> stables r step ?ss' \<and> start [\<sqsubseteq>\<^bsub>r\<^esub>] ?ss' \<and> (\<forall>ts\<in>nlists n A. start [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> stables r step ts \<longrightarrow> ?ss' [\<sqsubseteq>\<^bsub>r\<^esub>] ts)

goal (1 subgoal):
 1. iter f step start (unstables r step start) = (ss', w') \<longrightarrow> wf_dom ss' w' \<and> stables r step ss' \<and> start [\<sqsubseteq>\<^bsub>r\<^esub>] ss' \<and> (\<forall>ts\<in>nlists n A. start [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> stables r step ts \<longrightarrow> ss' [\<sqsubseteq>\<^bsub>r\<^esub>] ts)
[PROOF STEP]
by auto


[STATEMENT]
lemma iter_dom_properties2:
 "iter f step start (unstables r step start) = (ss',w') \<longrightarrow> ss' \<in> nlists n A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iter f step start (unstables r step start) = (ss', w') \<longrightarrow> ss' \<in> nlists n A
[PROOF STEP]
using iter_dom_properties
[PROOF STATE]
proof (prove)
using this:
iter f step start (unstables r step start) = (?ss', ?w') \<longrightarrow> wf_dom ?ss' ?w' \<and> stables r step ?ss' \<and> start [\<sqsubseteq>\<^bsub>r\<^esub>] ?ss' \<and> (\<forall>ts\<in>nlists n A. start [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> stables r step ts \<longrightarrow> ?ss' [\<sqsubseteq>\<^bsub>r\<^esub>] ts)

goal (1 subgoal):
 1. iter f step start (unstables r step start) = (ss', w') \<longrightarrow> ss' \<in> nlists n A
[PROOF STEP]
by (auto simp only:wf_dom_def nlists_def)


[STATEMENT]
lemma iter_dom_termination:
  "iter f step start (unstables r step start) = (ss,w) \<longrightarrow>
   w \<noteq> [] \<longrightarrow>
   propa f (step (hd w) (ss!(hd w))) ss (tl w) = (ss, tl w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iter f step start (unstables r step start) = (ss, w) \<longrightarrow> w \<noteq> [] \<longrightarrow> propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ss, tl w)
[PROOF STEP]
proof (intro strip)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>iter f step start (unstables r step start) = (ss, w); w \<noteq> []\<rbrakk> \<Longrightarrow> propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ss, tl w)
[PROOF STEP]
assume iter: "iter f step start (unstables r step start) = (ss, w)" and w_n_nil: "w \<noteq> []"
[PROOF STATE]
proof (state)
this:
iter f step start (unstables r step start) = (ss, w)
w \<noteq> []

goal (1 subgoal):
 1. \<lbrakk>iter f step start (unstables r step start) = (ss, w); w \<noteq> []\<rbrakk> \<Longrightarrow> propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ss, tl w)
[PROOF STEP]
with iter_dom_properties
[PROOF STATE]
proof (chain)
picking this:
iter f step start (unstables r step start) = (?ss', ?w') \<longrightarrow> wf_dom ?ss' ?w' \<and> stables r step ?ss' \<and> start [\<sqsubseteq>\<^bsub>r\<^esub>] ?ss' \<and> (\<forall>ts\<in>nlists n A. start [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> stables r step ts \<longrightarrow> ?ss' [\<sqsubseteq>\<^bsub>r\<^esub>] ts)
iter f step start (unstables r step start) = (ss, w)
w \<noteq> []
[PROOF STEP]
have stas: "stables r step ss"
   and wf_ss_w: "wf_dom ss w"
   and start_le_ss: "start [\<sqsubseteq>\<^sub>r] ss"
[PROOF STATE]
proof (prove)
using this:
iter f step start (unstables r step start) = (?ss', ?w') \<longrightarrow> wf_dom ?ss' ?w' \<and> stables r step ?ss' \<and> start [\<sqsubseteq>\<^bsub>r\<^esub>] ?ss' \<and> (\<forall>ts\<in>nlists n A. start [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> stables r step ts \<longrightarrow> ?ss' [\<sqsubseteq>\<^bsub>r\<^esub>] ts)
iter f step start (unstables r step start) = (ss, w)
w \<noteq> []

goal (1 subgoal):
 1. stables r step ss &&& wf_dom ss w &&& start [\<sqsubseteq>\<^bsub>r\<^esub>] ss
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
stables r step ss
wf_dom ss w
start [\<sqsubseteq>\<^bsub>r\<^esub>] ss

goal (1 subgoal):
 1. \<lbrakk>iter f step start (unstables r step start) = (ss, w); w \<noteq> []\<rbrakk> \<Longrightarrow> propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ss, tl w)
[PROOF STEP]
from stas
[PROOF STATE]
proof (chain)
picking this:
stables r step ss
[PROOF STEP]
have sta_p: "(\<forall>p < size ss. stable r step ss p)"
[PROOF STATE]
proof (prove)
using this:
stables r step ss

goal (1 subgoal):
 1. \<forall>p<length ss. Typing_Framework_1.stable r step ss p
[PROOF STEP]
by (auto simp add:stables_def)
[PROOF STATE]
proof (state)
this:
\<forall>p<length ss. Typing_Framework_1.stable r step ss p

goal (1 subgoal):
 1. \<lbrakk>iter f step start (unstables r step start) = (ss, w); w \<noteq> []\<rbrakk> \<Longrightarrow> propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ss, tl w)
[PROOF STEP]
from wf_ss_w
[PROOF STATE]
proof (chain)
picking this:
wf_dom ss w
[PROOF STEP]
have n_w_sta:  "\<forall>p<n. p \<notin>set w \<longrightarrow>  stable r step ss p"
                      and len_eq: "length ss = n"
                      and w_lt_n: "\<forall>x\<in> set w. x < n"
                      and ss_inA: "\<forall>x\<in>set ss. x \<in>  A"
                      and sorted_w: "sorted w "
[PROOF STATE]
proof (prove)
using this:
wf_dom ss w

goal (1 subgoal):
 1. (\<forall>p<n. p \<notin> set w \<longrightarrow> Typing_Framework_1.stable r step ss p &&& length ss = n) &&& \<forall>x\<in>set w. x < n &&& \<forall>x\<in>set ss. x \<in> A &&& Sorted_Less.sorted w
[PROOF STEP]
by (auto simp add:wf_dom_def)
[PROOF STATE]
proof (state)
this:
\<forall>p<n. p \<notin> set w \<longrightarrow> Typing_Framework_1.stable r step ss p
length ss = n
\<forall>x\<in>set w. x < n
\<forall>x\<in>set ss. x \<in> A
Sorted_Less.sorted w

goal (1 subgoal):
 1. \<lbrakk>iter f step start (unstables r step start) = (ss, w); w \<noteq> []\<rbrakk> \<Longrightarrow> propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ss, tl w)
[PROOF STEP]
from w_lt_n
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>set w. x < n
[PROOF STEP]
have hd_w_lt_n: "hd w < n"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>set w. x < n

goal (1 subgoal):
 1. hd w < n
[PROOF STEP]
using w_n_nil
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>set w. x < n
w \<noteq> []

goal (1 subgoal):
 1. hd w < n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
hd w < n

goal (1 subgoal):
 1. \<lbrakk>iter f step start (unstables r step start) = (ss, w); w \<noteq> []\<rbrakk> \<Longrightarrow> propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ss, tl w)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
hd w < n
[PROOF STEP]
have hd_w_in_verts: "hd w \<in> set (g_V G)"
[PROOF STATE]
proof (prove)
using this:
hd w < n

goal (1 subgoal):
 1. hd w \<in> set (g_V G)
[PROOF STEP]
using n_def nodes_def verts_set
[PROOF STATE]
proof (prove)
using this:
hd w < n
n \<equiv> length nodes
nodes \<equiv> g_V G
set (g_V G) = {0..<length (g_V G)}

goal (1 subgoal):
 1. hd w \<in> set (g_V G)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
hd w \<in> set (g_V G)

goal (1 subgoal):
 1. \<lbrakk>iter f step start (unstables r step start) = (ss, w); w \<noteq> []\<rbrakk> \<Longrightarrow> propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ss, tl w)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
hd w \<in> set (g_V G)
[PROOF STEP]
have fin_succ_hd_w: "finite (succs (hd w))"
[PROOF STATE]
proof (prove)
using this:
hd w \<in> set (g_V G)

goal (1 subgoal):
 1. finite (succs (hd w))
[PROOF STEP]
using fin_succs hd_w_in_verts
[PROOF STATE]
proof (prove)
using this:
hd w \<in> set (g_V G)
\<forall>v\<in>set (g_V G). finite (succs v)
hd w \<in> set (g_V G)

goal (1 subgoal):
 1. finite (succs (hd w))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite (succs (hd w))

goal (1 subgoal):
 1. \<lbrakk>iter f step start (unstables r step start) = (ss, w); w \<noteq> []\<rbrakk> \<Longrightarrow> propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ss, tl w)
[PROOF STEP]
let ?ss_hdw = "ss!hd w"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>iter f step start (unstables r step start) = (ss, w); w \<noteq> []\<rbrakk> \<Longrightarrow> propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ss, tl w)
[PROOF STEP]
let ?qs = "step (hd w) ?ss_hdw"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>iter f step start (unstables r step start) = (ss, w); w \<noteq> []\<rbrakk> \<Longrightarrow> propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ss, tl w)
[PROOF STEP]
from hd_w_lt_n
[PROOF STATE]
proof (chain)
picking this:
hd w < n
[PROOF STEP]
have dist: "distinct (map fst ?qs)"
[PROOF STATE]
proof (prove)
using this:
hd w < n

goal (1 subgoal):
 1. distinct (map fst (step (hd w) (ss ! hd w)))
[PROOF STEP]
using distinct_p
[PROOF STATE]
proof (prove)
using this:
hd w < n
?p < n \<longrightarrow> distinct (map fst (step ?p (?ss ! ?p)))

goal (1 subgoal):
 1. distinct (map fst (step (hd w) (ss ! hd w)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
distinct (map fst (step (hd w) (ss ! hd w)))

goal (1 subgoal):
 1. \<lbrakk>iter f step start (unstables r step start) = (ss, w); w \<noteq> []\<rbrakk> \<Longrightarrow> propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ss, tl w)
[PROOF STEP]
from wf_ss_w w_n_nil
[PROOF STATE]
proof (chain)
picking this:
wf_dom ss w
w \<noteq> []
[PROOF STEP]
have hdw_ss_subset_nodes: "set (hd w # ?ss_hdw) \<subseteq> set nodes"
                        and sorted_hd_w_ss: "sorted (rev (hd w # ?ss_hdw))"
                        and hd_w_ss_in_A: " ((hd w # ?ss_hdw)) \<in> A"
                        and step_pres_bounded: "\<forall>(q, \<tau>)\<in>set ?qs. q < length ss \<and> \<tau> \<in> A"
[PROOF STATE]
proof (prove)
using this:
wf_dom ss w
w \<noteq> []

goal (1 subgoal):
 1. (set (hd w # ss ! hd w) \<subseteq> set nodes &&& Sorted_Less.sorted (rev (hd w # ss ! hd w))) &&& hd w # ss ! hd w \<in> A &&& \<forall>(q, \<tau>)\<in>set (step (hd w) (ss ! hd w)). q < length ss \<and> \<tau> \<in> A
[PROOF STEP]
using propa_dom_invariant_auxi
[PROOF STATE]
proof (prove)
using this:
wf_dom ss w
w \<noteq> []
\<lbrakk>wf_dom ?a ?b; ?b \<noteq> []\<rbrakk> \<Longrightarrow> ?a ! hd ?b \<noteq> rev [0..<n] \<and> Sorted_Less.sorted (rev (hd ?b # ?a ! hd ?b)) \<and> set (hd ?b # ?a ! hd ?b) \<subseteq> set nodes \<and> hd ?b # ?a ! hd ?b \<in> A \<and> (\<forall>(q, \<tau>)\<in>set (step (hd ?b) (?a ! hd ?b)). q < length ?a \<and> \<tau> \<in> A)

goal (1 subgoal):
 1. (set (hd w # ss ! hd w) \<subseteq> set nodes &&& Sorted_Less.sorted (rev (hd w # ss ! hd w))) &&& hd w # ss ! hd w \<in> A &&& \<forall>(q, \<tau>)\<in>set (step (hd w) (ss ! hd w)). q < length ss \<and> \<tau> \<in> A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (hd w # ss ! hd w) \<subseteq> set nodes
Sorted_Less.sorted (rev (hd w # ss ! hd w))
hd w # ss ! hd w \<in> A
\<forall>(q, \<tau>)\<in>set (step (hd w) (ss ! hd w)). q < length ss \<and> \<tau> \<in> A

goal (1 subgoal):
 1. \<lbrakk>iter f step start (unstables r step start) = (ss, w); w \<noteq> []\<rbrakk> \<Longrightarrow> propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ss, tl w)
[PROOF STEP]
let ?res = "propa f (step (hd w) (ss!(hd w))) ss (tl w) "
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>iter f step start (unstables r step start) = (ss, w); w \<noteq> []\<rbrakk> \<Longrightarrow> propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ss, tl w)
[PROOF STEP]
have "propa f (step (hd w) (ss!(hd w))) ss (tl w) = ?res"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. propa f (step (hd w) (ss ! hd w)) ss (tl w) = propa f (step (hd w) (ss ! hd w)) ss (tl w)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
propa f (step (hd w) (ss ! hd w)) ss (tl w) = propa f (step (hd w) (ss ! hd w)) ss (tl w)

goal (1 subgoal):
 1. \<lbrakk>iter f step start (unstables r step start) = (ss, w); w \<noteq> []\<rbrakk> \<Longrightarrow> propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ss, tl w)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
propa f (step (hd w) (ss ! hd w)) ss (tl w) = propa f (step (hd w) (ss ! hd w)) ss (tl w)
[PROOF STEP]
obtain ss' w' where propa: "propa f (step (hd w) (ss!(hd w))) ss (tl w) = (ss', w')"
[PROOF STATE]
proof (prove)
using this:
propa f (step (hd w) (ss ! hd w)) ss (tl w) = propa f (step (hd w) (ss ! hd w)) ss (tl w)

goal (1 subgoal):
 1. (\<And>ss' w'. propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ss', w') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases ?res) auto
[PROOF STATE]
proof (state)
this:
propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ss', w')

goal (1 subgoal):
 1. \<lbrakk>iter f step start (unstables r step start) = (ss, w); w \<noteq> []\<rbrakk> \<Longrightarrow> propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ss, tl w)
[PROOF STEP]
from sorted_w
[PROOF STATE]
proof (chain)
picking this:
Sorted_Less.sorted w
[PROOF STEP]
have sorted_tl_b: "sorted (tl w)"
[PROOF STATE]
proof (prove)
using this:
Sorted_Less.sorted w

goal (1 subgoal):
 1. Sorted_Less.sorted (tl w)
[PROOF STEP]
by (induct w) auto
[PROOF STATE]
proof (state)
this:
Sorted_Less.sorted (tl w)

goal (1 subgoal):
 1. \<lbrakk>iter f step start (unstables r step start) = (ss, w); w \<noteq> []\<rbrakk> \<Longrightarrow> propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ss, tl w)
[PROOF STEP]
from ss_inA
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>set ss. x \<in> A
[PROOF STEP]
have set_a: "set ss \<subseteq> A"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>set ss. x \<in> A

goal (1 subgoal):
 1. set ss \<subseteq> A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set ss \<subseteq> A

goal (1 subgoal):
 1. \<lbrakk>iter f step start (unstables r step start) = (ss, w); w \<noteq> []\<rbrakk> \<Longrightarrow> propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ss, tl w)
[PROOF STEP]
with step_pres_bounded sorted_tl_b len_eq dist
[PROOF STATE]
proof (chain)
picking this:
\<forall>(q, \<tau>)\<in>set (step (hd w) (ss ! hd w)). q < length ss \<and> \<tau> \<in> A
Sorted_Less.sorted (tl w)
length ss = n
distinct (map fst (step (hd w) (ss ! hd w)))
set ss \<subseteq> A
[PROOF STEP]
have "\<forall>(q, \<tau>) \<in> set ?qs. (fst(propa f ?qs ss (tl w)))!q = \<tau> \<squnion>\<^bsub>f\<^esub>ss!q"
[PROOF STATE]
proof (prove)
using this:
\<forall>(q, \<tau>)\<in>set (step (hd w) (ss ! hd w)). q < length ss \<and> \<tau> \<in> A
Sorted_Less.sorted (tl w)
length ss = n
distinct (map fst (step (hd w) (ss ! hd w)))
set ss \<subseteq> A

goal (1 subgoal):
 1. \<forall>(q, \<tau>)\<in>set (step (hd w) (ss ! hd w)). fst (propa f (step (hd w) (ss ! hd w)) ss (tl w)) ! q = \<tau> \<squnion>\<^bsub>f\<^esub> ss ! q
[PROOF STEP]
by (auto dest:propa_property1)
[PROOF STATE]
proof (state)
this:
\<forall>(q, \<tau>)\<in>set (step (hd w) (ss ! hd w)). fst (propa f (step (hd w) (ss ! hd w)) ss (tl w)) ! q = \<tau> \<squnion>\<^bsub>f\<^esub> ss ! q

goal (1 subgoal):
 1. \<lbrakk>iter f step start (unstables r step start) = (ss, w); w \<noteq> []\<rbrakk> \<Longrightarrow> propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ss, tl w)
[PROOF STEP]
with propa
[PROOF STATE]
proof (chain)
picking this:
propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ss', w')
\<forall>(q, \<tau>)\<in>set (step (hd w) (ss ! hd w)). fst (propa f (step (hd w) (ss ! hd w)) ss (tl w)) ! q = \<tau> \<squnion>\<^bsub>f\<^esub> ss ! q
[PROOF STEP]
have propa_ss1:  "\<forall>(q, \<tau>) \<in> set ?qs. ss'!q =  (hd w # ?ss_hdw) \<squnion>\<^bsub>f\<^esub>ss!q"
[PROOF STATE]
proof (prove)
using this:
propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ss', w')
\<forall>(q, \<tau>)\<in>set (step (hd w) (ss ! hd w)). fst (propa f (step (hd w) (ss ! hd w)) ss (tl w)) ! q = \<tau> \<squnion>\<^bsub>f\<^esub> ss ! q

goal (1 subgoal):
 1. \<forall>(q, \<tau>)\<in>set (step (hd w) (ss ! hd w)). ss' ! q = hd w # ss ! hd w \<squnion>\<^bsub>f\<^esub> ss ! q
[PROOF STEP]
by (simp add:step_def exec_def transf_def)
[PROOF STATE]
proof (state)
this:
\<forall>(q, \<tau>)\<in>set (step (hd w) (ss ! hd w)). ss' ! q = hd w # ss ! hd w \<squnion>\<^bsub>f\<^esub> ss ! q

goal (1 subgoal):
 1. \<lbrakk>iter f step start (unstables r step start) = (ss, w); w \<noteq> []\<rbrakk> \<Longrightarrow> propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ss, tl w)
[PROOF STEP]
from step_pres_bounded sorted_tl_b set_a  len_eq dist
[PROOF STATE]
proof (chain)
picking this:
\<forall>(q, \<tau>)\<in>set (step (hd w) (ss ! hd w)). q < length ss \<and> \<tau> \<in> A
Sorted_Less.sorted (tl w)
set ss \<subseteq> A
length ss = n
distinct (map fst (step (hd w) (ss ! hd w)))
[PROOF STEP]
have  "\<And>q. q \<notin> set(map fst ?qs) \<Longrightarrow> q < length ss \<Longrightarrow> (fst(propa f ?qs ss (tl w)))!q = ss!q"
[PROOF STATE]
proof (prove)
using this:
\<forall>(q, \<tau>)\<in>set (step (hd w) (ss ! hd w)). q < length ss \<and> \<tau> \<in> A
Sorted_Less.sorted (tl w)
set ss \<subseteq> A
length ss = n
distinct (map fst (step (hd w) (ss ! hd w)))

goal (1 subgoal):
 1. \<And>q. \<lbrakk>q \<notin> set (map fst (step (hd w) (ss ! hd w))); q < length ss\<rbrakk> \<Longrightarrow> fst (propa f (step (hd w) (ss ! hd w)) ss (tl w)) ! q = ss ! q
[PROOF STEP]
by (auto intro:propa_property2)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?q \<notin> set (map fst (step (hd w) (ss ! hd w))); ?q < length ss\<rbrakk> \<Longrightarrow> fst (propa f (step (hd w) (ss ! hd w)) ss (tl w)) ! ?q = ss ! ?q

goal (1 subgoal):
 1. \<lbrakk>iter f step start (unstables r step start) = (ss, w); w \<noteq> []\<rbrakk> \<Longrightarrow> propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ss, tl w)
[PROOF STEP]
with propa
[PROOF STATE]
proof (chain)
picking this:
propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ss', w')
\<lbrakk>?q \<notin> set (map fst (step (hd w) (ss ! hd w))); ?q < length ss\<rbrakk> \<Longrightarrow> fst (propa f (step (hd w) (ss ! hd w)) ss (tl w)) ! ?q = ss ! ?q
[PROOF STEP]
have g2: "\<And>q. q \<notin> set(map fst ?qs) \<Longrightarrow> q < length ss \<Longrightarrow> ss'!q = ss!q"
[PROOF STATE]
proof (prove)
using this:
propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ss', w')
\<lbrakk>?q \<notin> set (map fst (step (hd w) (ss ! hd w))); ?q < length ss\<rbrakk> \<Longrightarrow> fst (propa f (step (hd w) (ss ! hd w)) ss (tl w)) ! ?q = ss ! ?q

goal (1 subgoal):
 1. \<And>q. \<lbrakk>q \<notin> set (map fst (step (hd w) (ss ! hd w))); q < length ss\<rbrakk> \<Longrightarrow> ss' ! q = ss ! q
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>?q \<notin> set (map fst (step (hd w) (ss ! hd w))); ?q < length ss\<rbrakk> \<Longrightarrow> ss' ! ?q = ss ! ?q

goal (1 subgoal):
 1. \<lbrakk>iter f step start (unstables r step start) = (ss, w); w \<noteq> []\<rbrakk> \<Longrightarrow> propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ss, tl w)
[PROOF STEP]
from sorted_w
[PROOF STATE]
proof (chain)
picking this:
Sorted_Less.sorted w
[PROOF STEP]
have sorted_tl_w: "sorted (tl w)"
[PROOF STATE]
proof (prove)
using this:
Sorted_Less.sorted w

goal (1 subgoal):
 1. Sorted_Less.sorted (tl w)
[PROOF STEP]
by (induct w)  auto
[PROOF STATE]
proof (state)
this:
Sorted_Less.sorted (tl w)

goal (1 subgoal):
 1. \<lbrakk>iter f step start (unstables r step start) = (ss, w); w \<noteq> []\<rbrakk> \<Longrightarrow> propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ss, tl w)
[PROOF STEP]
with step_pres_bounded set_a
[PROOF STATE]
proof (chain)
picking this:
\<forall>(q, \<tau>)\<in>set (step (hd w) (ss ! hd w)). q < length ss \<and> \<tau> \<in> A
set ss \<subseteq> A
Sorted_Less.sorted (tl w)
[PROOF STEP]
have fst_propa: "fst (propa f ?qs ss (tl w)) = (merges f ?qs ss)"
   and snd_propa: "snd (propa f ?qs ss (tl w)) = (sorted_list_of_set ({q. \<exists>t.(q,t)\<in>set ?qs \<and> t \<squnion>\<^bsub>f\<^esub> (ss!q) \<noteq> ss!q} \<union> set (tl w)))"
[PROOF STATE]
proof (prove)
using this:
\<forall>(q, \<tau>)\<in>set (step (hd w) (ss ! hd w)). q < length ss \<and> \<tau> \<in> A
set ss \<subseteq> A
Sorted_Less.sorted (tl w)

goal (1 subgoal):
 1. fst (propa f (step (hd w) (ss ! hd w)) ss (tl w)) = merges f (step (hd w) (ss ! hd w)) ss &&& snd (propa f (step (hd w) (ss ! hd w)) ss (tl w)) = sorted_list_of_set ({q. \<exists>t. (q, t) \<in> set (step (hd w) (ss ! hd w)) \<and> t \<squnion>\<^bsub>f\<^esub> ss ! q \<noteq> ss ! q} \<union> set (tl w))
[PROOF STEP]
using decomp_propa
[PROOF STATE]
proof (prove)
using this:
\<forall>(q, \<tau>)\<in>set (step (hd w) (ss ! hd w)). q < length ss \<and> \<tau> \<in> A
set ss \<subseteq> A
Sorted_Less.sorted (tl w)
\<lbrakk>\<forall>(q, t)\<in>set ?qs. q < length ?ss \<and> t \<in> A; Sorted_Less.sorted ?w; set ?ss \<subseteq> A\<rbrakk> \<Longrightarrow> propa f ?qs ?ss ?w = (merges f ?qs ?ss, sorted_list_of_set ({q. \<exists>t. (q, t) \<in> set ?qs \<and> t \<squnion>\<^bsub>f\<^esub> ?ss ! q \<noteq> ?ss ! q} \<union> set ?w))

goal (1 subgoal):
 1. fst (propa f (step (hd w) (ss ! hd w)) ss (tl w)) = merges f (step (hd w) (ss ! hd w)) ss &&& snd (propa f (step (hd w) (ss ! hd w)) ss (tl w)) = sorted_list_of_set ({q. \<exists>t. (q, t) \<in> set (step (hd w) (ss ! hd w)) \<and> t \<squnion>\<^bsub>f\<^esub> ss ! q \<noteq> ss ! q} \<union> set (tl w))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
fst (propa f (step (hd w) (ss ! hd w)) ss (tl w)) = merges f (step (hd w) (ss ! hd w)) ss
snd (propa f (step (hd w) (ss ! hd w)) ss (tl w)) = sorted_list_of_set ({q. \<exists>t. (q, t) \<in> set (step (hd w) (ss ! hd w)) \<and> t \<squnion>\<^bsub>f\<^esub> ss ! q \<noteq> ss ! q} \<union> set (tl w))

goal (1 subgoal):
 1. \<lbrakk>iter f step start (unstables r step start) = (ss, w); w \<noteq> []\<rbrakk> \<Longrightarrow> propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ss, tl w)
[PROOF STEP]
with propa
[PROOF STATE]
proof (chain)
picking this:
propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ss', w')
fst (propa f (step (hd w) (ss ! hd w)) ss (tl w)) = merges f (step (hd w) (ss ! hd w)) ss
snd (propa f (step (hd w) (ss ! hd w)) ss (tl w)) = sorted_list_of_set ({q. \<exists>t. (q, t) \<in> set (step (hd w) (ss ! hd w)) \<and> t \<squnion>\<^bsub>f\<^esub> ss ! q \<noteq> ss ! q} \<union> set (tl w))
[PROOF STEP]
have len_ss_eq_ss': "length ss' = length ss"
[PROOF STATE]
proof (prove)
using this:
propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ss', w')
fst (propa f (step (hd w) (ss ! hd w)) ss (tl w)) = merges f (step (hd w) (ss ! hd w)) ss
snd (propa f (step (hd w) (ss ! hd w)) ss (tl w)) = sorted_list_of_set ({q. \<exists>t. (q, t) \<in> set (step (hd w) (ss ! hd w)) \<and> t \<squnion>\<^bsub>f\<^esub> ss ! q \<noteq> ss ! q} \<union> set (tl w))

goal (1 subgoal):
 1. length ss' = length ss
[PROOF STEP]
using length_merges
[PROOF STATE]
proof (prove)
using this:
propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ss', w')
fst (propa f (step (hd w) (ss ! hd w)) ss (tl w)) = merges f (step (hd w) (ss ! hd w)) ss
snd (propa f (step (hd w) (ss ! hd w)) ss (tl w)) = sorted_list_of_set ({q. \<exists>t. (q, t) \<in> set (step (hd w) (ss ! hd w)) \<and> t \<squnion>\<^bsub>f\<^esub> ss ! q \<noteq> ss ! q} \<union> set (tl w))
length (merges ?f ?ps ?ss) = length ?ss

goal (1 subgoal):
 1. length ss' = length ss
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length ss' = length ss

goal (1 subgoal):
 1. \<lbrakk>iter f step start (unstables r step start) = (ss, w); w \<noteq> []\<rbrakk> \<Longrightarrow> propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ss, tl w)
[PROOF STEP]
have ss_ss'_eq:  "\<forall>i<n. (fst (propa f ?qs ss (tl w)))!i = ss!i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i<n. fst (propa f (step (hd w) (ss ! hd w)) ss (tl w)) ! i = ss ! i
[PROOF STEP]
proof(intro strip)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i < n \<Longrightarrow> fst (propa f (step (hd w) (ss ! hd w)) ss (tl w)) ! i = ss ! i
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i < n \<Longrightarrow> fst (propa f (step (hd w) (ss ! hd w)) ss (tl w)) ! i = ss ! i
[PROOF STEP]
assume "i < n"
[PROOF STATE]
proof (state)
this:
i < n

goal (1 subgoal):
 1. \<And>i. i < n \<Longrightarrow> fst (propa f (step (hd w) (ss ! hd w)) ss (tl w)) ! i = ss ! i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i < n
[PROOF STEP]
have i_lt_len_ss: "i < length ss"
[PROOF STATE]
proof (prove)
using this:
i < n

goal (1 subgoal):
 1. i < length ss
[PROOF STEP]
using \<open>length ss = n\<close>
[PROOF STATE]
proof (prove)
using this:
i < n
length ss = n

goal (1 subgoal):
 1. i < length ss
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i < length ss

goal (1 subgoal):
 1. \<And>i. i < n \<Longrightarrow> fst (propa f (step (hd w) (ss ! hd w)) ss (tl w)) ! i = ss ! i
[PROOF STEP]
show "fst (propa f ?qs ss (tl w)) ! i = ss ! i "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (propa f (step (hd w) (ss ! hd w)) ss (tl w)) ! i = ss ! i
[PROOF STEP]
proof(cases "i \<in> set(map fst ?qs)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. i \<in> set (map fst (step (hd w) (ss ! hd w))) \<Longrightarrow> fst (propa f (step (hd w) (ss ! hd w)) ss (tl w)) ! i = ss ! i
 2. i \<notin> set (map fst (step (hd w) (ss ! hd w))) \<Longrightarrow> fst (propa f (step (hd w) (ss ! hd w)) ss (tl w)) ! i = ss ! i
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
i \<in> set (map fst (step (hd w) (ss ! hd w)))

goal (2 subgoals):
 1. i \<in> set (map fst (step (hd w) (ss ! hd w))) \<Longrightarrow> fst (propa f (step (hd w) (ss ! hd w)) ss (tl w)) ! i = ss ! i
 2. i \<notin> set (map fst (step (hd w) (ss ! hd w))) \<Longrightarrow> fst (propa f (step (hd w) (ss ! hd w)) ss (tl w)) ! i = ss ! i
[PROOF STEP]
assume ass1: "i \<in> set (map fst ?qs)"
[PROOF STATE]
proof (state)
this:
i \<in> set (map fst (step (hd w) (ss ! hd w)))

goal (2 subgoals):
 1. i \<in> set (map fst (step (hd w) (ss ! hd w))) \<Longrightarrow> fst (propa f (step (hd w) (ss ! hd w)) ss (tl w)) ! i = ss ! i
 2. i \<notin> set (map fst (step (hd w) (ss ! hd w))) \<Longrightarrow> fst (propa f (step (hd w) (ss ! hd w)) ss (tl w)) ! i = ss ! i
[PROOF STEP]
with propa_ss1
[PROOF STATE]
proof (chain)
picking this:
\<forall>(q, \<tau>)\<in>set (step (hd w) (ss ! hd w)). ss' ! q = hd w # ss ! hd w \<squnion>\<^bsub>f\<^esub> ss ! q
i \<in> set (map fst (step (hd w) (ss ! hd w)))
[PROOF STEP]
have ss': "ss'!i = (hd w # ?ss_hdw) \<squnion>\<^bsub>f\<^esub>ss!i"
[PROOF STATE]
proof (prove)
using this:
\<forall>(q, \<tau>)\<in>set (step (hd w) (ss ! hd w)). ss' ! q = hd w # ss ! hd w \<squnion>\<^bsub>f\<^esub> ss ! q
i \<in> set (map fst (step (hd w) (ss ! hd w)))

goal (1 subgoal):
 1. ss' ! i = hd w # ss ! hd w \<squnion>\<^bsub>f\<^esub> ss ! i
[PROOF STEP]
by (auto simp add: step_def exec_def)
[PROOF STATE]
proof (state)
this:
ss' ! i = hd w # ss ! hd w \<squnion>\<^bsub>f\<^esub> ss ! i

goal (2 subgoals):
 1. i \<in> set (map fst (step (hd w) (ss ! hd w))) \<Longrightarrow> fst (propa f (step (hd w) (ss ! hd w)) ss (tl w)) ! i = ss ! i
 2. i \<notin> set (map fst (step (hd w) (ss ! hd w))) \<Longrightarrow> fst (propa f (step (hd w) (ss ! hd w)) ss (tl w)) ! i = ss ! i
[PROOF STEP]
from ass1
[PROOF STATE]
proof (chain)
picking this:
i \<in> set (map fst (step (hd w) (ss ! hd w)))
[PROOF STEP]
have "i \<in> set (g_V G)"
[PROOF STATE]
proof (prove)
using this:
i \<in> set (map fst (step (hd w) (ss ! hd w)))

goal (1 subgoal):
 1. i \<in> set (g_V G)
[PROOF STEP]
using succ_in_G fin_succ_hd_w
[PROOF STATE]
proof (prove)
using this:
i \<in> set (map fst (step (hd w) (ss ! hd w)))
\<forall>v\<in>succs ?n. v \<in> set (g_V G)
finite (succs (hd w))

goal (1 subgoal):
 1. i \<in> set (g_V G)
[PROOF STEP]
by (auto simp add:step_def exec_def)
[PROOF STATE]
proof (state)
this:
i \<in> set (g_V G)

goal (2 subgoals):
 1. i \<in> set (map fst (step (hd w) (ss ! hd w))) \<Longrightarrow> fst (propa f (step (hd w) (ss ! hd w)) ss (tl w)) ! i = ss ! i
 2. i \<notin> set (map fst (step (hd w) (ss ! hd w))) \<Longrightarrow> fst (propa f (step (hd w) (ss ! hd w)) ss (tl w)) ! i = ss ! i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<in> set (g_V G)
[PROOF STEP]
have q_lt_len_ss: "i < length ss"
[PROOF STATE]
proof (prove)
using this:
i \<in> set (g_V G)

goal (1 subgoal):
 1. i < length ss
[PROOF STEP]
using len_eq
[PROOF STATE]
proof (prove)
using this:
i \<in> set (g_V G)
length ss = n

goal (1 subgoal):
 1. i < length ss
[PROOF STEP]
by (auto simp add:n_def nodes_def verts_set)
[PROOF STATE]
proof (state)
this:
i < length ss

goal (2 subgoals):
 1. i \<in> set (map fst (step (hd w) (ss ! hd w))) \<Longrightarrow> fst (propa f (step (hd w) (ss ! hd w)) ss (tl w)) ! i = ss ! i
 2. i \<notin> set (map fst (step (hd w) (ss ! hd w))) \<Longrightarrow> fst (propa f (step (hd w) (ss ! hd w)) ss (tl w)) ! i = ss ! i
[PROOF STEP]
from hd_w_lt_n len_eq stas
[PROOF STATE]
proof (chain)
picking this:
hd w < n
length ss = n
stables r step ss
[PROOF STEP]
have "stable r step ss (hd w)"
[PROOF STATE]
proof (prove)
using this:
hd w < n
length ss = n
stables r step ss

goal (1 subgoal):
 1. Typing_Framework_1.stable r step ss (hd w)
[PROOF STEP]
by (auto simp add:stables_def)
[PROOF STATE]
proof (state)
this:
Typing_Framework_1.stable r step ss (hd w)

goal (2 subgoals):
 1. i \<in> set (map fst (step (hd w) (ss ! hd w))) \<Longrightarrow> fst (propa f (step (hd w) (ss ! hd w)) ss (tl w)) ! i = ss ! i
 2. i \<notin> set (map fst (step (hd w) (ss ! hd w))) \<Longrightarrow> fst (propa f (step (hd w) (ss ! hd w)) ss (tl w)) ! i = ss ! i
[PROOF STEP]
with ass1
[PROOF STATE]
proof (chain)
picking this:
i \<in> set (map fst (step (hd w) (ss ! hd w)))
Typing_Framework_1.stable r step ss (hd w)
[PROOF STEP]
have "(hd w # ?ss_hdw) \<sqsubseteq>\<^sub>r ss!i"
[PROOF STATE]
proof (prove)
using this:
i \<in> set (map fst (step (hd w) (ss ! hd w)))
Typing_Framework_1.stable r step ss (hd w)

goal (1 subgoal):
 1. hd w # ss ! hd w \<sqsubseteq>\<^bsub>r\<^esub> ss ! i
[PROOF STEP]
by (auto simp add:stables_def stable_def step_def exec_def transf_def)
[PROOF STATE]
proof (state)
this:
hd w # ss ! hd w \<sqsubseteq>\<^bsub>r\<^esub> ss ! i

goal (2 subgoals):
 1. i \<in> set (map fst (step (hd w) (ss ! hd w))) \<Longrightarrow> fst (propa f (step (hd w) (ss ! hd w)) ss (tl w)) ! i = ss ! i
 2. i \<notin> set (map fst (step (hd w) (ss ! hd w))) \<Longrightarrow> fst (propa f (step (hd w) (ss ! hd w)) ss (tl w)) ! i = ss ! i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
hd w # ss ! hd w \<sqsubseteq>\<^bsub>r\<^esub> ss ! i
[PROOF STEP]
have "set (ss!i) \<subseteq> set (hd w # ?ss_hdw) \<or> (hd w # ?ss_hdw) = ss!i"
[PROOF STATE]
proof (prove)
using this:
hd w # ss ! hd w \<sqsubseteq>\<^bsub>r\<^esub> ss ! i

goal (1 subgoal):
 1. set (ss ! i) \<subseteq> set (hd w # ss ! hd w) \<or> hd w # ss ! hd w = ss ! i
[PROOF STEP]
by (auto simp add:lesssub_def lesub_def r_def nodes_le_def)
[PROOF STATE]
proof (state)
this:
set (ss ! i) \<subseteq> set (hd w # ss ! hd w) \<or> hd w # ss ! hd w = ss ! i

goal (2 subgoals):
 1. i \<in> set (map fst (step (hd w) (ss ! hd w))) \<Longrightarrow> fst (propa f (step (hd w) (ss ! hd w)) ss (tl w)) ! i = ss ! i
 2. i \<notin> set (map fst (step (hd w) (ss ! hd w))) \<Longrightarrow> fst (propa f (step (hd w) (ss ! hd w)) ss (tl w)) ! i = ss ! i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
set (ss ! i) \<subseteq> set (hd w # ss ! hd w) \<or> hd w # ss ! hd w = ss ! i
[PROOF STEP]
have set_ss_q_subst_hdw_ss: "set (ss!i) \<subseteq> set (hd w # ?ss_hdw)"
[PROOF STATE]
proof (prove)
using this:
set (ss ! i) \<subseteq> set (hd w # ss ! hd w) \<or> hd w # ss ! hd w = ss ! i

goal (1 subgoal):
 1. set (ss ! i) \<subseteq> set (hd w # ss ! hd w)
[PROOF STEP]
by (rule disjE)(auto simp add:lesssub_def lesub_def r_def nodes_le_def)
[PROOF STATE]
proof (state)
this:
set (ss ! i) \<subseteq> set (hd w # ss ! hd w)

goal (2 subgoals):
 1. i \<in> set (map fst (step (hd w) (ss ! hd w))) \<Longrightarrow> fst (propa f (step (hd w) (ss ! hd w)) ss (tl w)) ! i = ss ! i
 2. i \<notin> set (map fst (step (hd w) (ss ! hd w))) \<Longrightarrow> fst (propa f (step (hd w) (ss ! hd w)) ss (tl w)) ! i = ss ! i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
set (ss ! i) \<subseteq> set (hd w # ss ! hd w)
[PROOF STEP]
have ss_q: "set (ss!i) \<inter> set (hd w # ?ss_hdw) = set (ss!i)"
[PROOF STATE]
proof (prove)
using this:
set (ss ! i) \<subseteq> set (hd w # ss ! hd w)

goal (1 subgoal):
 1. set (ss ! i) \<inter> set (hd w # ss ! hd w) = set (ss ! i)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (ss ! i) \<inter> set (hd w # ss ! hd w) = set (ss ! i)

goal (2 subgoals):
 1. i \<in> set (map fst (step (hd w) (ss ! hd w))) \<Longrightarrow> fst (propa f (step (hd w) (ss ! hd w)) ss (tl w)) ! i = ss ! i
 2. i \<notin> set (map fst (step (hd w) (ss ! hd w))) \<Longrightarrow> fst (propa f (step (hd w) (ss ! hd w)) ss (tl w)) ! i = ss ! i
[PROOF STEP]
from wf_ss_w q_lt_len_ss
[PROOF STATE]
proof (chain)
picking this:
wf_dom ss w
i < length ss
[PROOF STEP]
have sorted_ss_q: "sorted (rev (ss!i))"
[PROOF STATE]
proof (prove)
using this:
wf_dom ss w
i < length ss

goal (1 subgoal):
 1. Sorted_Less.sorted (rev (ss ! i))
[PROOF STEP]
by (simp add:wf_dom_def)
[PROOF STATE]
proof (state)
this:
Sorted_Less.sorted (rev (ss ! i))

goal (2 subgoals):
 1. i \<in> set (map fst (step (hd w) (ss ! hd w))) \<Longrightarrow> fst (propa f (step (hd w) (ss ! hd w)) ss (tl w)) ! i = ss ! i
 2. i \<notin> set (map fst (step (hd w) (ss ! hd w))) \<Longrightarrow> fst (propa f (step (hd w) (ss ! hd w)) ss (tl w)) ! i = ss ! i
[PROOF STEP]
with sorted_hd_w_ss
[PROOF STATE]
proof (chain)
picking this:
Sorted_Less.sorted (rev (hd w # ss ! hd w))
Sorted_Less.sorted (rev (ss ! i))
[PROOF STEP]
have ss_q': "set (ss'!i) = set (ss!i) \<inter> set (hd w # ?ss_hdw)"
                           and sorrted_ss_q': "sorted (rev (ss'!i))"
[PROOF STATE]
proof (prove)
using this:
Sorted_Less.sorted (rev (hd w # ss ! hd w))
Sorted_Less.sorted (rev (ss ! i))

goal (1 subgoal):
 1. set (ss' ! i) = set (ss ! i) \<inter> set (hd w # ss ! hd w) &&& Sorted_Less.sorted (rev (ss' ! i))
[PROOF STEP]
using ss'
[PROOF STATE]
proof (prove)
using this:
Sorted_Less.sorted (rev (hd w # ss ! hd w))
Sorted_Less.sorted (rev (ss ! i))
ss' ! i = hd w # ss ! hd w \<squnion>\<^bsub>f\<^esub> ss ! i

goal (1 subgoal):
 1. set (ss' ! i) = set (ss ! i) \<inter> set (hd w # ss ! hd w) &&& Sorted_Less.sorted (rev (ss' ! i))
[PROOF STEP]
by (auto simp add:plussub_def f_def nodes_sup_def inter_sorted_correct)
[PROOF STATE]
proof (state)
this:
set (ss' ! i) = set (ss ! i) \<inter> set (hd w # ss ! hd w)
Sorted_Less.sorted (rev (ss' ! i))

goal (2 subgoals):
 1. i \<in> set (map fst (step (hd w) (ss ! hd w))) \<Longrightarrow> fst (propa f (step (hd w) (ss ! hd w)) ss (tl w)) ! i = ss ! i
 2. i \<notin> set (map fst (step (hd w) (ss ! hd w))) \<Longrightarrow> fst (propa f (step (hd w) (ss ! hd w)) ss (tl w)) ! i = ss ! i
[PROOF STEP]
with ss_q sorted_ss_q sorrted_ss_q'
[PROOF STATE]
proof (chain)
picking this:
set (ss ! i) \<inter> set (hd w # ss ! hd w) = set (ss ! i)
Sorted_Less.sorted (rev (ss ! i))
Sorted_Less.sorted (rev (ss' ! i))
set (ss' ! i) = set (ss ! i) \<inter> set (hd w # ss ! hd w)
Sorted_Less.sorted (rev (ss' ! i))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
set (ss ! i) \<inter> set (hd w # ss ! hd w) = set (ss ! i)
Sorted_Less.sorted (rev (ss ! i))
Sorted_Less.sorted (rev (ss' ! i))
set (ss' ! i) = set (ss ! i) \<inter> set (hd w # ss ! hd w)
Sorted_Less.sorted (rev (ss' ! i))

goal (1 subgoal):
 1. fst (propa f (step (hd w) (ss ! hd w)) ss (tl w)) ! i = ss ! i
[PROOF STEP]
using sorted_less_rev_set_unique propa
[PROOF STATE]
proof (prove)
using this:
set (ss ! i) \<inter> set (hd w # ss ! hd w) = set (ss ! i)
Sorted_Less.sorted (rev (ss ! i))
Sorted_Less.sorted (rev (ss' ! i))
set (ss' ! i) = set (ss ! i) \<inter> set (hd w # ss ! hd w)
Sorted_Less.sorted (rev (ss' ! i))
\<lbrakk>Sorted_Less.sorted (rev ?xs); Sorted_Less.sorted (rev ?ys); set ?xs = set ?ys\<rbrakk> \<Longrightarrow> ?xs = ?ys
propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ss', w')

goal (1 subgoal):
 1. fst (propa f (step (hd w) (ss ! hd w)) ss (tl w)) ! i = ss ! i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
fst (propa f (step (hd w) (ss ! hd w)) ss (tl w)) ! i = ss ! i

goal (1 subgoal):
 1. i \<notin> set (map fst (step (hd w) (ss ! hd w))) \<Longrightarrow> fst (propa f (step (hd w) (ss ! hd w)) ss (tl w)) ! i = ss ! i
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i \<notin> set (map fst (step (hd w) (ss ! hd w))) \<Longrightarrow> fst (propa f (step (hd w) (ss ! hd w)) ss (tl w)) ! i = ss ! i
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
i \<notin> set (map fst (step (hd w) (ss ! hd w)))

goal (1 subgoal):
 1. i \<notin> set (map fst (step (hd w) (ss ! hd w))) \<Longrightarrow> fst (propa f (step (hd w) (ss ! hd w)) ss (tl w)) ! i = ss ! i
[PROOF STEP]
note i_nin = this
[PROOF STATE]
proof (state)
this:
i \<notin> set (map fst (step (hd w) (ss ! hd w)))

goal (1 subgoal):
 1. i \<notin> set (map fst (step (hd w) (ss ! hd w))) \<Longrightarrow> fst (propa f (step (hd w) (ss ! hd w)) ss (tl w)) ! i = ss ! i
[PROOF STEP]
from step_pres_bounded sorted_tl_b set_a len_eq dist propa i_lt_len_ss i_nin
[PROOF STATE]
proof (chain)
picking this:
\<forall>(q, \<tau>)\<in>set (step (hd w) (ss ! hd w)). q < length ss \<and> \<tau> \<in> A
Sorted_Less.sorted (tl w)
set ss \<subseteq> A
length ss = n
distinct (map fst (step (hd w) (ss ! hd w)))
propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ss', w')
i < length ss
i \<notin> set (map fst (step (hd w) (ss ! hd w)))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>(q, \<tau>)\<in>set (step (hd w) (ss ! hd w)). q < length ss \<and> \<tau> \<in> A
Sorted_Less.sorted (tl w)
set ss \<subseteq> A
length ss = n
distinct (map fst (step (hd w) (ss ! hd w)))
propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ss', w')
i < length ss
i \<notin> set (map fst (step (hd w) (ss ! hd w)))

goal (1 subgoal):
 1. fst (propa f (step (hd w) (ss ! hd w)) ss (tl w)) ! i = ss ! i
[PROOF STEP]
by (fastforce dest:propa_property2)
[PROOF STATE]
proof (state)
this:
fst (propa f (step (hd w) (ss ! hd w)) ss (tl w)) ! i = ss ! i

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
fst (propa f (step (hd w) (ss ! hd w)) ss (tl w)) ! i = ss ! i

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>i<n. fst (propa f (step (hd w) (ss ! hd w)) ss (tl w)) ! i = ss ! i

goal (1 subgoal):
 1. \<lbrakk>iter f step start (unstables r step start) = (ss, w); w \<noteq> []\<rbrakk> \<Longrightarrow> propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ss, tl w)
[PROOF STEP]
with len_ss_eq_ss'
[PROOF STATE]
proof (chain)
picking this:
length ss' = length ss
\<forall>i<n. fst (propa f (step (hd w) (ss ! hd w)) ss (tl w)) ! i = ss ! i
[PROOF STEP]
have eq_ss: "ss' = ss"
[PROOF STATE]
proof (prove)
using this:
length ss' = length ss
\<forall>i<n. fst (propa f (step (hd w) (ss ! hd w)) ss (tl w)) ! i = ss ! i

goal (1 subgoal):
 1. ss' = ss
[PROOF STEP]
using len_eq propa
[PROOF STATE]
proof (prove)
using this:
length ss' = length ss
\<forall>i<n. fst (propa f (step (hd w) (ss ! hd w)) ss (tl w)) ! i = ss ! i
length ss = n
propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ss', w')

goal (1 subgoal):
 1. ss' = ss
[PROOF STEP]
by (auto simp add:list_eq_iff_nth_eq)
[PROOF STATE]
proof (state)
this:
ss' = ss

goal (1 subgoal):
 1. \<lbrakk>iter f step start (unstables r step start) = (ss, w); w \<noteq> []\<rbrakk> \<Longrightarrow> propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ss, tl w)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ss' = ss
[PROOF STEP]
have qs_empty: "(({q. \<exists>t.(q,t)\<in>set ?qs \<and> t \<squnion>\<^bsub>f\<^esub> (ss!q) \<noteq> ss!q} \<union> set (tl w))) =  (set (tl w))"
[PROOF STATE]
proof (prove)
using this:
ss' = ss

goal (1 subgoal):
 1. {q. \<exists>t. (q, t) \<in> set (step (hd w) (ss ! hd w)) \<and> t \<squnion>\<^bsub>f\<^esub> ss ! q \<noteq> ss ! q} \<union> set (tl w) = set (tl w)
[PROOF STEP]
using propa_ss1 propa transf_def step_def exec_def
[PROOF STATE]
proof (prove)
using this:
ss' = ss
\<forall>(q, \<tau>)\<in>set (step (hd w) (ss ! hd w)). ss' ! q = hd w # ss ! hd w \<squnion>\<^bsub>f\<^esub> ss ! q
propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ss', w')
transf ?n ?input \<equiv> ?n # ?input
step \<equiv> exec
exec ?n ?xs = map (\<lambda>pc. (pc, transf ?n ?xs)) (rev (sorted_list_of_set (succs ?n)))

goal (1 subgoal):
 1. {q. \<exists>t. (q, t) \<in> set (step (hd w) (ss ! hd w)) \<and> t \<squnion>\<^bsub>f\<^esub> ss ! q \<noteq> ss ! q} \<union> set (tl w) = set (tl w)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
{q. \<exists>t. (q, t) \<in> set (step (hd w) (ss ! hd w)) \<and> t \<squnion>\<^bsub>f\<^esub> ss ! q \<noteq> ss ! q} \<union> set (tl w) = set (tl w)

goal (1 subgoal):
 1. \<lbrakk>iter f step start (unstables r step start) = (ss, w); w \<noteq> []\<rbrakk> \<Longrightarrow> propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ss, tl w)
[PROOF STEP]
with snd_propa
[PROOF STATE]
proof (chain)
picking this:
snd (propa f (step (hd w) (ss ! hd w)) ss (tl w)) = sorted_list_of_set ({q. \<exists>t. (q, t) \<in> set (step (hd w) (ss ! hd w)) \<and> t \<squnion>\<^bsub>f\<^esub> ss ! q \<noteq> ss ! q} \<union> set (tl w))
{q. \<exists>t. (q, t) \<in> set (step (hd w) (ss ! hd w)) \<and> t \<squnion>\<^bsub>f\<^esub> ss ! q \<noteq> ss ! q} \<union> set (tl w) = set (tl w)
[PROOF STEP]
have "snd (propa f ?qs ss (tl w)) = sorted_list_of_set (set (tl w))"
[PROOF STATE]
proof (prove)
using this:
snd (propa f (step (hd w) (ss ! hd w)) ss (tl w)) = sorted_list_of_set ({q. \<exists>t. (q, t) \<in> set (step (hd w) (ss ! hd w)) \<and> t \<squnion>\<^bsub>f\<^esub> ss ! q \<noteq> ss ! q} \<union> set (tl w))
{q. \<exists>t. (q, t) \<in> set (step (hd w) (ss ! hd w)) \<and> t \<squnion>\<^bsub>f\<^esub> ss ! q \<noteq> ss ! q} \<union> set (tl w) = set (tl w)

goal (1 subgoal):
 1. snd (propa f (step (hd w) (ss ! hd w)) ss (tl w)) = sorted_list_of_set (set (tl w))
[PROOF STEP]
using sorted_w
[PROOF STATE]
proof (prove)
using this:
snd (propa f (step (hd w) (ss ! hd w)) ss (tl w)) = sorted_list_of_set ({q. \<exists>t. (q, t) \<in> set (step (hd w) (ss ! hd w)) \<and> t \<squnion>\<^bsub>f\<^esub> ss ! q \<noteq> ss ! q} \<union> set (tl w))
{q. \<exists>t. (q, t) \<in> set (step (hd w) (ss ! hd w)) \<and> t \<squnion>\<^bsub>f\<^esub> ss ! q \<noteq> ss ! q} \<union> set (tl w) = set (tl w)
Sorted_Less.sorted w

goal (1 subgoal):
 1. snd (propa f (step (hd w) (ss ! hd w)) ss (tl w)) = sorted_list_of_set (set (tl w))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
snd (propa f (step (hd w) (ss ! hd w)) ss (tl w)) = sorted_list_of_set (set (tl w))

goal (1 subgoal):
 1. \<lbrakk>iter f step start (unstables r step start) = (ss, w); w \<noteq> []\<rbrakk> \<Longrightarrow> propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ss, tl w)
[PROOF STEP]
with sorted_tl_w
[PROOF STATE]
proof (chain)
picking this:
Sorted_Less.sorted (tl w)
snd (propa f (step (hd w) (ss ! hd w)) ss (tl w)) = sorted_list_of_set (set (tl w))
[PROOF STEP]
have "snd (propa f ?qs ss (tl w)) = tl w"
[PROOF STATE]
proof (prove)
using this:
Sorted_Less.sorted (tl w)
snd (propa f (step (hd w) (ss ! hd w)) ss (tl w)) = sorted_list_of_set (set (tl w))

goal (1 subgoal):
 1. snd (propa f (step (hd w) (ss ! hd w)) ss (tl w)) = tl w
[PROOF STEP]
by (fastforce dest:sorted_less_set_eq)
[PROOF STATE]
proof (state)
this:
snd (propa f (step (hd w) (ss ! hd w)) ss (tl w)) = tl w

goal (1 subgoal):
 1. \<lbrakk>iter f step start (unstables r step start) = (ss, w); w \<noteq> []\<rbrakk> \<Longrightarrow> propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ss, tl w)
[PROOF STEP]
with propa
[PROOF STATE]
proof (chain)
picking this:
propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ss', w')
snd (propa f (step (hd w) (ss ! hd w)) ss (tl w)) = tl w
[PROOF STEP]
have "w' = tl w"
[PROOF STATE]
proof (prove)
using this:
propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ss', w')
snd (propa f (step (hd w) (ss ! hd w)) ss (tl w)) = tl w

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

goal (1 subgoal):
 1. \<lbrakk>iter f step start (unstables r step start) = (ss, w); w \<noteq> []\<rbrakk> \<Longrightarrow> propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ss, tl w)
[PROOF STEP]
with eq_ss
[PROOF STATE]
proof (chain)
picking this:
ss' = ss
w' = tl w
[PROOF STEP]
show "propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ss, tl w)"
[PROOF STATE]
proof (prove)
using this:
ss' = ss
w' = tl w

goal (1 subgoal):
 1. propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ss, tl w)
[PROOF STEP]
using propa
[PROOF STATE]
proof (prove)
using this:
ss' = ss
w' = tl w
propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ss', w')

goal (1 subgoal):
 1. propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ss, tl w)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ss, tl w)

goal:
No subgoals!
[PROOF STEP]
qed