[STATEMENT]
lemma propa_dom_invariant_aux':
  fixes a b ss w
assumes propa: "propa f (step (hd b) (a ! hd b)) a (tl b) = (ss, w) "
    and b_n_nil: "b \<noteq> [] "
    and a_in_A: "\<forall>\<tau>\<in>set a. \<tau> \<in> A  "
    and ass: "\<forall>p<length ss0.
          sorted (rev ( (a ! p))) \<and>
          (a ! p \<noteq> rev [0..<length ss0] \<longrightarrow> (\<forall>x\<in>set ( (a ! p)). x < p)) \<and>
          (a ! p = rev [0..<length ss0] \<longrightarrow>  (\<exists>x\<in> set b. (x,p)\<in> g_E G \<and> x < p)) \<and>
          (p \<notin> set b \<longrightarrow> stable r step a p)"
    and sorted_b: "sorted b  "
    and n_len: "n = length ss0  "
    and len_eq:  "length a = length ss0  "
    and b_lt_n: "\<forall>x\<in>set b. x < length ss0  "
  shows "(\<forall>\<tau>\<in>set ss. \<tau> \<in> A) \<and>
         (\<forall>p<length ss0.
           sorted (rev ( (ss ! p))) \<and>
           (ss ! p \<noteq> rev [0..<length ss0] \<longrightarrow> (\<forall>x\<in>set (ss ! p). x < p)) \<and>
           (ss ! p = rev [0..<length ss0] \<longrightarrow>  (\<exists>x\<in> set w. (x,p)\<in> g_E G \<and> x < p)) \<and>
           (p \<notin> set w \<longrightarrow> stable r step ss p)) \<and>
         sorted w \<and> length ss = length ss0 \<and> (\<forall>x\<in>set w. x < length ss0) "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>\<tau>\<in>set ss. \<tau> \<in> A) \<and> (\<forall>p<length ss0. Sorted_Less.sorted (rev (ss ! p)) \<and> (ss ! p \<noteq> rev [0..<length ss0] \<longrightarrow> (\<forall>x\<in>set (ss ! p). x < p)) \<and> (ss ! p = rev [0..<length ss0] \<longrightarrow> (\<exists>x\<in>set w. (x, p) \<in> g_E G \<and> x < p)) \<and> (p \<notin> set w \<longrightarrow> Typing_Framework_1.stable r step ss p)) \<and> Sorted_Less.sorted w \<and> length ss = length ss0 \<and> (\<forall>x\<in>set w. x < length ss0)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
propa f (step (hd b) (a ! hd b)) a (tl b) = (ss, w)
b \<noteq> []
\<forall>\<tau>\<in>set a. \<tau> \<in> A
\<forall>p<length ss0. Sorted_Less.sorted (rev (a ! p)) \<and> (a ! p \<noteq> rev [0..<length ss0] \<longrightarrow> (\<forall>x\<in>set (a ! p). x < p)) \<and> (a ! p = rev [0..<length ss0] \<longrightarrow> (\<exists>x\<in>set b. (x, p) \<in> g_E G \<and> x < p)) \<and> (p \<notin> set b \<longrightarrow> Typing_Framework_1.stable r step a p)
Sorted_Less.sorted b
n = length ss0
length a = length ss0
\<forall>x\<in>set b. x < length ss0

goal (1 subgoal):
 1. (\<forall>\<tau>\<in>set ss. \<tau> \<in> A) \<and> (\<forall>p<length ss0. Sorted_Less.sorted (rev (ss ! p)) \<and> (ss ! p \<noteq> rev [0..<length ss0] \<longrightarrow> (\<forall>x\<in>set (ss ! p). x < p)) \<and> (ss ! p = rev [0..<length ss0] \<longrightarrow> (\<exists>x\<in>set w. (x, p) \<in> g_E G \<and> x < p)) \<and> (p \<notin> set w \<longrightarrow> Typing_Framework_1.stable r step ss p)) \<and> Sorted_Less.sorted w \<and> length ss = length ss0 \<and> (\<forall>x\<in>set w. x < length ss0)
[PROOF STEP]
by (auto dest: propa_dom_invariant_aux)


[STATEMENT]
lemma propa_dom_invariant:
  assumes wf_ss_w: "wf_dom ss w "
      and w_n_nil: "w \<noteq> []"
      and propa: "propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ss', w') "
    shows "wf_dom ss' w'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_dom ss' w'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
wf_dom ss w
w \<noteq> []
propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ss', w')

goal (1 subgoal):
 1. wf_dom ss' w'
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>wf_dom ss w; w \<noteq> []; propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ss', w')\<rbrakk> \<Longrightarrow> wf_dom ss' w'
[PROOF STEP]
from wf_ss_w
[PROOF STATE]
proof (chain)
picking this:
wf_dom ss w
[PROOF STEP]
have ass:
    "(\<forall>p< n. sorted (rev (ss!p)) \<and>
             (ss!p \<noteq> rev [0..< n] \<longrightarrow> (\<forall>x\<in>set (ss!p). x < p)) \<and>
             (ss!p = rev [0..< n] \<longrightarrow>  (\<exists>x\<in> set w. (x,p)\<in> g_E G \<and> x < p)) \<and>
             (p \<notin> set w \<longrightarrow> stable r step ss p)) "
  and sorted_b: "sorted w"
  and a_in_A: "\<forall>\<tau>\<in>set ss. \<tau> \<in> A"
  and len_eq: "length ss = n"
  and b_lt_n: "(\<forall>x\<in>set w. x < n)"
[PROOF STATE]
proof (prove)
using this:
wf_dom ss w

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

goal (1 subgoal):
 1. \<lbrakk>wf_dom ss w; w \<noteq> []; propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ss', w')\<rbrakk> \<Longrightarrow> wf_dom ss' w'
[PROOF STEP]
from propa w_n_nil a_in_A ass sorted_b len_eq b_lt_n
[PROOF STATE]
proof (chain)
picking this:
propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ss', w')
w \<noteq> []
\<forall>\<tau>\<in>set ss. \<tau> \<in> A
\<forall>p<n. Sorted_Less.sorted (rev (ss ! p)) \<and> (ss ! p \<noteq> rev [0..<n] \<longrightarrow> (\<forall>x\<in>set (ss ! p). x < p)) \<and> (ss ! p = rev [0..<n] \<longrightarrow> (\<exists>x\<in>set w. (x, p) \<in> g_E G \<and> x < p)) \<and> (p \<notin> set w \<longrightarrow> Typing_Framework_1.stable r step ss p)
Sorted_Less.sorted w
length ss = n
\<forall>x\<in>set w. x < n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ss', w')
w \<noteq> []
\<forall>\<tau>\<in>set ss. \<tau> \<in> A
\<forall>p<n. Sorted_Less.sorted (rev (ss ! p)) \<and> (ss ! p \<noteq> rev [0..<n] \<longrightarrow> (\<forall>x\<in>set (ss ! p). x < p)) \<and> (ss ! p = rev [0..<n] \<longrightarrow> (\<exists>x\<in>set w. (x, p) \<in> g_E G \<and> x < p)) \<and> (p \<notin> set w \<longrightarrow> Typing_Framework_1.stable r step ss p)
Sorted_Less.sorted w
length ss = n
\<forall>x\<in>set w. x < n

goal (1 subgoal):
 1. wf_dom ss' w'
[PROOF STEP]
by (unfold wf_dom_def) (rule propa_dom_invariant_aux)
[PROOF STATE]
proof (state)
this:
wf_dom ss' w'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma step_dom_mono_aux:
  fixes \<tau> p \<tau>' a b
  assumes sorted: "sorted (rev (transf p  \<tau>)) "
      and a_b_step: "(a, b) \<in> set (step p  \<tau>) "
      and "\<tau> \<in> A " and " p < n " and " \<tau> \<sqsubseteq>\<^bsub>r\<^esub> \<tau>'"
    shows "\<exists>\<tau>''. (a, \<tau>'') \<in> set (step p \<tau>') \<and> b \<sqsubseteq>\<^bsub>r\<^esub> \<tau>''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>\<tau>''. (a, \<tau>'') \<in> set (step p \<tau>') \<and> b \<sqsubseteq>\<^bsub>r\<^esub> \<tau>''
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>\<tau>''. (a, \<tau>'') \<in> set (step p \<tau>') \<and> b \<sqsubseteq>\<^bsub>r\<^esub> \<tau>''
[PROOF STEP]
have step1: "step p \<tau> = map (\<lambda>pc. (pc, (transf  p \<tau>))) (rev (sorted_list_of_set(succs p)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. step p \<tau> = map (\<lambda>pc. (pc, transf p \<tau>)) (rev (sorted_list_of_set (succs p)))
[PROOF STEP]
by (simp add:step_def exec_def)
[PROOF STATE]
proof (state)
this:
step p \<tau> = map (\<lambda>pc. (pc, transf p \<tau>)) (rev (sorted_list_of_set (succs p)))

goal (1 subgoal):
 1. \<exists>\<tau>''. (a, \<tau>'') \<in> set (step p \<tau>') \<and> b \<sqsubseteq>\<^bsub>r\<^esub> \<tau>''
[PROOF STEP]
from a_b_step
[PROOF STATE]
proof (chain)
picking this:
(a, b) \<in> set (step p \<tau>)
[PROOF STEP]
have "set (step p \<tau>) \<noteq> {}"
[PROOF STATE]
proof (prove)
using this:
(a, b) \<in> set (step p \<tau>)

goal (1 subgoal):
 1. set (step p \<tau>) \<noteq> {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (step p \<tau>) \<noteq> {}

goal (1 subgoal):
 1. \<exists>\<tau>''. (a, \<tau>'') \<in> set (step p \<tau>') \<and> b \<sqsubseteq>\<^bsub>r\<^esub> \<tau>''
[PROOF STEP]
with step1
[PROOF STATE]
proof (chain)
picking this:
step p \<tau> = map (\<lambda>pc. (pc, transf p \<tau>)) (rev (sorted_list_of_set (succs p)))
set (step p \<tau>) \<noteq> {}
[PROOF STEP]
have succ_p_n_nil: "(rev (sorted_list_of_set(succs p))) \<noteq> []"
[PROOF STATE]
proof (prove)
using this:
step p \<tau> = map (\<lambda>pc. (pc, transf p \<tau>)) (rev (sorted_list_of_set (succs p)))
set (step p \<tau>) \<noteq> {}

goal (1 subgoal):
 1. rev (sorted_list_of_set (succs p)) \<noteq> []
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rev (sorted_list_of_set (succs p)) \<noteq> []

goal (1 subgoal):
 1. \<exists>\<tau>''. (a, \<tau>'') \<in> set (step p \<tau>') \<and> b \<sqsubseteq>\<^bsub>r\<^esub> \<tau>''
[PROOF STEP]
from \<open>p<n\<close>
[PROOF STATE]
proof (chain)
picking this:
p < n
[PROOF STEP]
have "p \<in> set (g_V G)"
[PROOF STATE]
proof (prove)
using this:
p < n

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

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

goal (1 subgoal):
 1. \<exists>\<tau>''. (a, \<tau>'') \<in> set (step p \<tau>') \<and> b \<sqsubseteq>\<^bsub>r\<^esub> \<tau>''
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p \<in> set (g_V G)
[PROOF STEP]
have fin: "finite (succs p)"
[PROOF STATE]
proof (prove)
using this:
p \<in> set (g_V G)

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

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

goal (1 subgoal):
 1. \<exists>\<tau>''. (a, \<tau>'') \<in> set (step p \<tau>') \<and> b \<sqsubseteq>\<^bsub>r\<^esub> \<tau>''
[PROOF STEP]
with step1
[PROOF STATE]
proof (chain)
picking this:
step p \<tau> = map (\<lambda>pc. (pc, transf p \<tau>)) (rev (sorted_list_of_set (succs p)))
finite (succs p)
[PROOF STEP]
have "\<forall>(x,y)\<in> set (step p \<tau>). x \<in> succs p"
               and step2: "\<forall>(x,y)\<in> set (step p \<tau>). y = transf p \<tau>"
[PROOF STATE]
proof (prove)
using this:
step p \<tau> = map (\<lambda>pc. (pc, transf p \<tau>)) (rev (sorted_list_of_set (succs p)))
finite (succs p)

goal (1 subgoal):
 1. \<forall>(x, y)\<in>set (step p \<tau>). x \<in> succs p &&& \<forall>(x, y)\<in>set (step p \<tau>). y = transf p \<tau>
[PROOF STEP]
by (auto simp add:step_def exec_def)
[PROOF STATE]
proof (state)
this:
\<forall>(x, y)\<in>set (step p \<tau>). x \<in> succs p
\<forall>(x, y)\<in>set (step p \<tau>). y = transf p \<tau>

goal (1 subgoal):
 1. \<exists>\<tau>''. (a, \<tau>'') \<in> set (step p \<tau>') \<and> b \<sqsubseteq>\<^bsub>r\<^esub> \<tau>''
[PROOF STEP]
with a_b_step
[PROOF STATE]
proof (chain)
picking this:
(a, b) \<in> set (step p \<tau>)
\<forall>(x, y)\<in>set (step p \<tau>). x \<in> succs p
\<forall>(x, y)\<in>set (step p \<tau>). y = transf p \<tau>
[PROOF STEP]
have "a \<in> succs p"
[PROOF STATE]
proof (prove)
using this:
(a, b) \<in> set (step p \<tau>)
\<forall>(x, y)\<in>set (step p \<tau>). x \<in> succs p
\<forall>(x, y)\<in>set (step p \<tau>). y = transf p \<tau>

goal (1 subgoal):
 1. a \<in> succs p
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a \<in> succs p

goal (1 subgoal):
 1. \<exists>\<tau>''. (a, \<tau>'') \<in> set (step p \<tau>') \<and> b \<sqsubseteq>\<^bsub>r\<^esub> \<tau>''
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<in> succs p
[PROOF STEP]
have "succs p \<noteq> {}"
[PROOF STATE]
proof (prove)
using this:
a \<in> succs p

goal (1 subgoal):
 1. succs p \<noteq> {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
succs p \<noteq> {}

goal (1 subgoal):
 1. \<exists>\<tau>''. (a, \<tau>'') \<in> set (step p \<tau>') \<and> b \<sqsubseteq>\<^bsub>r\<^esub> \<tau>''
[PROOF STEP]
from step2 a_b_step
[PROOF STATE]
proof (chain)
picking this:
\<forall>(x, y)\<in>set (step p \<tau>). y = transf p \<tau>
(a, b) \<in> set (step p \<tau>)
[PROOF STEP]
have b:  "b = transf p \<tau>"
[PROOF STATE]
proof (prove)
using this:
\<forall>(x, y)\<in>set (step p \<tau>). y = transf p \<tau>
(a, b) \<in> set (step p \<tau>)

goal (1 subgoal):
 1. b = transf p \<tau>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
b = transf p \<tau>

goal (1 subgoal):
 1. \<exists>\<tau>''. (a, \<tau>'') \<in> set (step p \<tau>') \<and> b \<sqsubseteq>\<^bsub>r\<^esub> \<tau>''
[PROOF STEP]
have step2: "step p \<tau>' = map (\<lambda>pc. (pc, (transf  p \<tau>'))) (rev (sorted_list_of_set(succs p)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. step p \<tau>' = map (\<lambda>pc. (pc, transf p \<tau>')) (rev (sorted_list_of_set (succs p)))
[PROOF STEP]
by (simp add:step_def exec_def)
[PROOF STATE]
proof (state)
this:
step p \<tau>' = map (\<lambda>pc. (pc, transf p \<tau>')) (rev (sorted_list_of_set (succs p)))

goal (1 subgoal):
 1. \<exists>\<tau>''. (a, \<tau>'') \<in> set (step p \<tau>') \<and> b \<sqsubseteq>\<^bsub>r\<^esub> \<tau>''
[PROOF STEP]
with fin
[PROOF STATE]
proof (chain)
picking this:
finite (succs p)
step p \<tau>' = map (\<lambda>pc. (pc, transf p \<tau>')) (rev (sorted_list_of_set (succs p)))
[PROOF STEP]
have g1: "\<forall>(x,y)\<in> set (step p \<tau>'). x \<in> succs p"
                and g2: "\<forall>(x,y)\<in> set (step p \<tau>'). y = transf p \<tau>'"
[PROOF STATE]
proof (prove)
using this:
finite (succs p)
step p \<tau>' = map (\<lambda>pc. (pc, transf p \<tau>')) (rev (sorted_list_of_set (succs p)))

goal (1 subgoal):
 1. \<forall>(x, y)\<in>set (step p \<tau>'). x \<in> succs p &&& \<forall>(x, y)\<in>set (step p \<tau>'). y = transf p \<tau>'
[PROOF STEP]
by (auto simp add:step_def exec_def)
[PROOF STATE]
proof (state)
this:
\<forall>(x, y)\<in>set (step p \<tau>'). x \<in> succs p
\<forall>(x, y)\<in>set (step p \<tau>'). y = transf p \<tau>'

goal (1 subgoal):
 1. \<exists>\<tau>''. (a, \<tau>'') \<in> set (step p \<tau>') \<and> b \<sqsubseteq>\<^bsub>r\<^esub> \<tau>''
[PROOF STEP]
with \<open>a \<in> succs p\<close>
[PROOF STATE]
proof (chain)
picking this:
a \<in> succs p
\<forall>(x, y)\<in>set (step p \<tau>'). x \<in> succs p
\<forall>(x, y)\<in>set (step p \<tau>'). y = transf p \<tau>'
[PROOF STEP]
have "\<exists>t. (a,t)\<in> set (step p \<tau>')"
[PROOF STATE]
proof (prove)
using this:
a \<in> succs p
\<forall>(x, y)\<in>set (step p \<tau>'). x \<in> succs p
\<forall>(x, y)\<in>set (step p \<tau>'). y = transf p \<tau>'

goal (1 subgoal):
 1. \<exists>t. (a, t) \<in> set (step p \<tau>')
[PROOF STEP]
using fin
[PROOF STATE]
proof (prove)
using this:
a \<in> succs p
\<forall>(x, y)\<in>set (step p \<tau>'). x \<in> succs p
\<forall>(x, y)\<in>set (step p \<tau>'). y = transf p \<tau>'
finite (succs p)

goal (1 subgoal):
 1. \<exists>t. (a, t) \<in> set (step p \<tau>')
[PROOF STEP]
by (auto simp add:step_def exec_def)
[PROOF STATE]
proof (state)
this:
\<exists>t. (a, t) \<in> set (step p \<tau>')

goal (1 subgoal):
 1. \<exists>\<tau>''. (a, \<tau>'') \<in> set (step p \<tau>') \<and> b \<sqsubseteq>\<^bsub>r\<^esub> \<tau>''
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>t. (a, t) \<in> set (step p \<tau>')
[PROOF STEP]
obtain t where ex: "(a,t)\<in> set (step p \<tau>')"
[PROOF STATE]
proof (prove)
using this:
\<exists>t. (a, t) \<in> set (step p \<tau>')

goal (1 subgoal):
 1. (\<And>t. (a, t) \<in> set (step p \<tau>') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(a, t) \<in> set (step p \<tau>')

goal (1 subgoal):
 1. \<exists>\<tau>''. (a, \<tau>'') \<in> set (step p \<tau>') \<and> b \<sqsubseteq>\<^bsub>r\<^esub> \<tau>''
[PROOF STEP]
with g2
[PROOF STATE]
proof (chain)
picking this:
\<forall>(x, y)\<in>set (step p \<tau>'). y = transf p \<tau>'
(a, t) \<in> set (step p \<tau>')
[PROOF STEP]
have t: "t = transf p \<tau>'"
[PROOF STATE]
proof (prove)
using this:
\<forall>(x, y)\<in>set (step p \<tau>'). y = transf p \<tau>'
(a, t) \<in> set (step p \<tau>')

goal (1 subgoal):
 1. t = transf p \<tau>'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
t = transf p \<tau>'

goal (1 subgoal):
 1. \<exists>\<tau>''. (a, \<tau>'') \<in> set (step p \<tau>') \<and> b \<sqsubseteq>\<^bsub>r\<^esub> \<tau>''
[PROOF STEP]
from\<open> \<tau> \<sqsubseteq>\<^bsub>r\<^esub> \<tau>'\<close>
[PROOF STATE]
proof (chain)
picking this:
\<tau> \<sqsubseteq>\<^bsub>r\<^esub> \<tau>'
[PROOF STEP]
have g: "sorted (rev \<tau>) \<and> sorted (rev \<tau>')\<and> set \<tau>' \<subseteq> set \<tau> \<or> \<tau> = \<tau>'"
[PROOF STATE]
proof (prove)
using this:
\<tau> \<sqsubseteq>\<^bsub>r\<^esub> \<tau>'

goal (1 subgoal):
 1. Sorted_Less.sorted (rev \<tau>) \<and> Sorted_Less.sorted (rev \<tau>') \<and> set \<tau>' \<subseteq> set \<tau> \<or> \<tau> = \<tau>'
[PROOF STEP]
by (auto simp add:r_def lesssub_def lesub_def nodes_le_def)
[PROOF STATE]
proof (state)
this:
Sorted_Less.sorted (rev \<tau>) \<and> Sorted_Less.sorted (rev \<tau>') \<and> set \<tau>' \<subseteq> set \<tau> \<or> \<tau> = \<tau>'

goal (1 subgoal):
 1. \<exists>\<tau>''. (a, \<tau>'') \<in> set (step p \<tau>') \<and> b \<sqsubseteq>\<^bsub>r\<^esub> \<tau>''
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Sorted_Less.sorted (rev \<tau>) \<and> Sorted_Less.sorted (rev \<tau>') \<and> set \<tau>' \<subseteq> set \<tau> \<or> \<tau> = \<tau>'
[PROOF STEP]
have subset_p: "set (p#\<tau>') \<subseteq> set (p# \<tau>)" and "set  \<tau>' \<subseteq> set \<tau>"
[PROOF STATE]
proof (prove)
using this:
Sorted_Less.sorted (rev \<tau>) \<and> Sorted_Less.sorted (rev \<tau>') \<and> set \<tau>' \<subseteq> set \<tau> \<or> \<tau> = \<tau>'

goal (1 subgoal):
 1. set (p # \<tau>') \<subseteq> set (p # \<tau>) &&& set \<tau>' \<subseteq> set \<tau>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (p # \<tau>') \<subseteq> set (p # \<tau>)
set \<tau>' \<subseteq> set \<tau>

goal (1 subgoal):
 1. \<exists>\<tau>''. (a, \<tau>'') \<in> set (step p \<tau>') \<and> b \<sqsubseteq>\<^bsub>r\<^esub> \<tau>''
[PROOF STEP]
from sorted
[PROOF STATE]
proof (chain)
picking this:
Sorted_Less.sorted (rev (transf p \<tau>))
[PROOF STEP]
have "\<forall>x\<in> set \<tau>. x < p" and "sorted (rev \<tau>')"
[PROOF STATE]
proof (prove)
using this:
Sorted_Less.sorted (rev (transf p \<tau>))

goal (1 subgoal):
 1. \<forall>x\<in>set \<tau>. x < p &&& Sorted_Less.sorted (rev \<tau>')
[PROOF STEP]
using g
[PROOF STATE]
proof (prove)
using this:
Sorted_Less.sorted (rev (transf p \<tau>))
Sorted_Less.sorted (rev \<tau>) \<and> Sorted_Less.sorted (rev \<tau>') \<and> set \<tau>' \<subseteq> set \<tau> \<or> \<tau> = \<tau>'

goal (1 subgoal):
 1. \<forall>x\<in>set \<tau>. x < p &&& Sorted_Less.sorted (rev \<tau>')
[PROOF STEP]
by (auto simp add:sorted_wrt_append transf_def)
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>set \<tau>. x < p
Sorted_Less.sorted (rev \<tau>')

goal (1 subgoal):
 1. \<exists>\<tau>''. (a, \<tau>'') \<in> set (step p \<tau>') \<and> b \<sqsubseteq>\<^bsub>r\<^esub> \<tau>''
[PROOF STEP]
with \<open>set \<tau>' \<subseteq> set \<tau>\<close>
[PROOF STATE]
proof (chain)
picking this:
set \<tau>' \<subseteq> set \<tau>
\<forall>x\<in>set \<tau>. x < p
Sorted_Less.sorted (rev \<tau>')
[PROOF STEP]
have "\<forall>x\<in> set \<tau>'. x < p"
[PROOF STATE]
proof (prove)
using this:
set \<tau>' \<subseteq> set \<tau>
\<forall>x\<in>set \<tau>. x < p
Sorted_Less.sorted (rev \<tau>')

goal (1 subgoal):
 1. \<forall>x\<in>set \<tau>'. x < p
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>set \<tau>'. x < p

goal (1 subgoal):
 1. \<exists>\<tau>''. (a, \<tau>'') \<in> set (step p \<tau>') \<and> b \<sqsubseteq>\<^bsub>r\<^esub> \<tau>''
[PROOF STEP]
with \<open>sorted (rev \<tau>')\<close>
[PROOF STATE]
proof (chain)
picking this:
Sorted_Less.sorted (rev \<tau>')
\<forall>x\<in>set \<tau>'. x < p
[PROOF STEP]
have "sorted (rev (p#\<tau>'))"
[PROOF STATE]
proof (prove)
using this:
Sorted_Less.sorted (rev \<tau>')
\<forall>x\<in>set \<tau>'. x < p

goal (1 subgoal):
 1. Sorted_Less.sorted (rev (p # \<tau>'))
[PROOF STEP]
by (auto simp add:sorted_wrt_append)
[PROOF STATE]
proof (state)
this:
Sorted_Less.sorted (rev (p # \<tau>'))

goal (1 subgoal):
 1. \<exists>\<tau>''. (a, \<tau>'') \<in> set (step p \<tau>') \<and> b \<sqsubseteq>\<^bsub>r\<^esub> \<tau>''
[PROOF STEP]
with sorted b t subset_p
[PROOF STATE]
proof (chain)
picking this:
Sorted_Less.sorted (rev (transf p \<tau>))
b = transf p \<tau>
t = transf p \<tau>'
set (p # \<tau>') \<subseteq> set (p # \<tau>)
Sorted_Less.sorted (rev (p # \<tau>'))
[PROOF STEP]
have "b \<sqsubseteq>\<^bsub>r\<^esub> t"
[PROOF STATE]
proof (prove)
using this:
Sorted_Less.sorted (rev (transf p \<tau>))
b = transf p \<tau>
t = transf p \<tau>'
set (p # \<tau>') \<subseteq> set (p # \<tau>)
Sorted_Less.sorted (rev (p # \<tau>'))

goal (1 subgoal):
 1. b \<sqsubseteq>\<^bsub>r\<^esub> t
[PROOF STEP]
by (auto simp add:r_def lesssub_def lesub_def nodes_le_def transf_def)
[PROOF STATE]
proof (state)
this:
b \<sqsubseteq>\<^bsub>r\<^esub> t

goal (1 subgoal):
 1. \<exists>\<tau>''. (a, \<tau>'') \<in> set (step p \<tau>') \<and> b \<sqsubseteq>\<^bsub>r\<^esub> \<tau>''
[PROOF STEP]
with ex
[PROOF STATE]
proof (chain)
picking this:
(a, t) \<in> set (step p \<tau>')
b \<sqsubseteq>\<^bsub>r\<^esub> t
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(a, t) \<in> set (step p \<tau>')
b \<sqsubseteq>\<^bsub>r\<^esub> t

goal (1 subgoal):
 1. \<exists>\<tau>''. (a, \<tau>'') \<in> set (step p \<tau>') \<and> b \<sqsubseteq>\<^bsub>r\<^esub> \<tau>''
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>\<tau>''. (a, \<tau>'') \<in> set (step p \<tau>') \<and> b \<sqsubseteq>\<^bsub>r\<^esub> \<tau>''

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma step_dom_mono:
"(\<forall>\<tau> p \<tau>'. \<tau> \<in> A \<and> p<n \<and> \<tau> \<sqsubseteq>\<^sub>r \<tau>' \<longrightarrow>
           sorted (rev (transf p \<tau>)) \<longrightarrow>
           set (step p \<tau>) {\<sqsubseteq>\<^bsub>r\<^esub>} set (step p \<tau>'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<tau> p \<tau>'. \<tau> \<in> A \<and> p < n \<and> \<tau> \<sqsubseteq>\<^bsub>r\<^esub> \<tau>' \<longrightarrow> Sorted_Less.sorted (rev (transf p \<tau>)) \<longrightarrow> set (step p \<tau>) {\<sqsubseteq>\<^bsub>r\<^esub>} set (step p \<tau>')
[PROOF STEP]
apply(unfold mono_def lesubstep_type_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<tau> p \<tau>'. \<tau> \<in> A \<and> p < n \<and> \<tau> \<sqsubseteq>\<^bsub>r\<^esub> \<tau>' \<longrightarrow> Sorted_Less.sorted (rev (transf p \<tau>)) \<longrightarrow> (\<forall>(pa, \<tau>)\<in>set (step p \<tau>). \<exists>\<tau>''. (pa, \<tau>'') \<in> set (step p \<tau>') \<and> \<tau> \<sqsubseteq>\<^bsub>r\<^esub> \<tau>'')
[PROOF STEP]
by(auto simp add:step_dom_mono_aux n_def nodes_def transf_def)


[STATEMENT]
lemma propa_termination:
  fixes a b
  assumes wf_a_b: "wf_dom a b"
      and b_n_nil: "b \<noteq> [] "
    shows "(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 STATE]
proof (prove)
goal (1 subgoal):
 1. (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]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (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]
let ?qs = "(step (hd b) (a ! hd b))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (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]
from wf_a_b
[PROOF STATE]
proof (chain)
picking this:
wf_dom a b
[PROOF STEP]
have "\<forall>x\<in>set b. x < n" and n_len: "length a = n"  and sorted_b: "sorted b"
               and set_a: "set a \<subseteq> A"
[PROOF STATE]
proof (prove)
using this:
wf_dom a b

goal (1 subgoal):
 1. (\<forall>x\<in>set b. x < n &&& length a = n) &&& Sorted_Less.sorted b &&& set a \<subseteq> A
[PROOF STEP]
by (auto simp add:wf_dom_def)
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>set b. x < n
length a = n
Sorted_Less.sorted b
set a \<subseteq> A

goal (1 subgoal):
 1. (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]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>set b. x < n
length a = n
Sorted_Less.sorted b
set a \<subseteq> A
[PROOF STEP]
have sorted_tl_b: "sorted (tl b)" and hd_b_lt_n: "hd b < n"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>set b. x < n
length a = n
Sorted_Less.sorted b
set a \<subseteq> A

goal (1 subgoal):
 1. Sorted_Less.sorted (tl b) &&& hd b < n
[PROOF STEP]
using b_n_nil
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>set b. x < n
length a = n
Sorted_Less.sorted b
set a \<subseteq> A
b \<noteq> []

goal (1 subgoal):
 1. Sorted_Less.sorted (tl b) &&& hd b < n
[PROOF STEP]
by (induct b) (auto simp add:sorted_wrt_append)
[PROOF STATE]
proof (state)
this:
Sorted_Less.sorted (tl b)
hd b < n

goal (1 subgoal):
 1. (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]
from set_a
[PROOF STATE]
proof (chain)
picking this:
set a \<subseteq> A
[PROOF STEP]
have a_inA: "a \<in> nlists n A"
[PROOF STATE]
proof (prove)
using this:
set a \<subseteq> A

goal (1 subgoal):
 1. a \<in> nlists n A
[PROOF STEP]
using n_len
[PROOF STATE]
proof (prove)
using this:
set a \<subseteq> A
length a = n

goal (1 subgoal):
 1. a \<in> nlists n A
[PROOF STEP]
by (auto intro: nlistsI)
[PROOF STATE]
proof (state)
this:
a \<in> nlists n A

goal (1 subgoal):
 1. (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]
from hd_b_lt_n
[PROOF STATE]
proof (chain)
picking this:
hd b < n
[PROOF STEP]
have dist: "distinct (map fst ?qs)"
[PROOF STATE]
proof (prove)
using this:
hd b < n

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

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

goal (1 subgoal):
 1. (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]
from wf_a_b b_n_nil
[PROOF STATE]
proof (chain)
picking this:
wf_dom a b
b \<noteq> []
[PROOF STEP]
have step_pres_bounded: "\<forall>(q, \<tau>)\<in>set ?qs. q < n \<and> \<tau> \<in> A"
[PROOF STATE]
proof (prove)
using this:
wf_dom a b
b \<noteq> []

goal (1 subgoal):
 1. \<forall>(q, \<tau>)\<in>set (step (hd b) (a ! hd b)). q < n \<and> \<tau> \<in> A
[PROOF STEP]
using propa_dom_invariant_auxi n_len
[PROOF STATE]
proof (prove)
using this:
wf_dom a b
b \<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)
length a = n

goal (1 subgoal):
 1. \<forall>(q, \<tau>)\<in>set (step (hd b) (a ! hd b)). q < n \<and> \<tau> \<in> A
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<forall>(q, \<tau>)\<in>set (step (hd b) (a ! hd b)). q < n \<and> \<tau> \<in> A

goal (1 subgoal):
 1. (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]
with sorted_tl_b set_a n_len
[PROOF STATE]
proof (chain)
picking this:
Sorted_Less.sorted (tl b)
set a \<subseteq> A
length a = n
\<forall>(q, \<tau>)\<in>set (step (hd b) (a ! hd b)). q < n \<and> \<tau> \<in> A
[PROOF STEP]
have propa: "propa f ?qs a (tl b) = (merges f ?qs a, (sorted_list_of_set ({q. \<exists>t.(q,t)\<in>set ?qs \<and> t \<squnion>\<^bsub>f\<^esub> (a!q) \<noteq> a!q} \<union> set(tl b))))"
[PROOF STATE]
proof (prove)
using this:
Sorted_Less.sorted (tl b)
set a \<subseteq> A
length a = n
\<forall>(q, \<tau>)\<in>set (step (hd b) (a ! hd b)). q < n \<and> \<tau> \<in> A

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

goal (1 subgoal):
 1. (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]
from a_inA step_pres_bounded sorted_b b_n_nil  dist
[PROOF STATE]
proof (chain)
picking this:
a \<in> nlists n A
\<forall>(q, \<tau>)\<in>set (step (hd b) (a ! hd b)). q < n \<and> \<tau> \<in> A
Sorted_Less.sorted b
b \<noteq> []
distinct (map fst (step (hd b) (a ! hd b)))
[PROOF STEP]
have "((merges f ?qs a, (sorted_list_of_set ({q. \<exists>t.(q,t)\<in>set ?qs \<and> t \<squnion>\<^bsub>f\<^esub> (a!q) \<noteq> a!q} \<union> set(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 STATE]
proof (prove)
using this:
a \<in> nlists n A
\<forall>(q, \<tau>)\<in>set (step (hd b) (a ! hd b)). q < n \<and> \<tau> \<in> A
Sorted_Less.sorted b
b \<noteq> []
distinct (map fst (step (hd b) (a ! hd b)))

goal (1 subgoal):
 1. ((merges f (step (hd b) (a ! hd b)) a, sorted_list_of_set ({q. \<exists>t. (q, t) \<in> set (step (hd b) (a ! hd b)) \<and> t \<squnion>\<^bsub>f\<^esub> a ! q \<noteq> a ! q} \<union> set (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]
by (auto simp add: finite_psubset_def dest: termination_lemma)
[PROOF STATE]
proof (state)
this:
((merges f (step (hd b) (a ! hd b)) a, sorted_list_of_set ({q. \<exists>t. (q, t) \<in> set (step (hd b) (a ! hd b)) \<and> t \<squnion>\<^bsub>f\<^esub> a ! q \<noteq> a ! q} \<union> set (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

goal (1 subgoal):
 1. (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]
with propa
[PROOF STATE]
proof (chain)
picking this:
propa f (step (hd b) (a ! hd b)) a (tl b) = (merges f (step (hd b) (a ! hd b)) a, sorted_list_of_set ({q. \<exists>t. (q, t) \<in> set (step (hd b) (a ! hd b)) \<and> t \<squnion>\<^bsub>f\<^esub> a ! q \<noteq> a ! q} \<union> set (tl b)))
((merges f (step (hd b) (a ! hd b)) a, sorted_list_of_set ({q. \<exists>t. (q, t) \<in> set (step (hd b) (a ! hd b)) \<and> t \<squnion>\<^bsub>f\<^esub> a ! q \<noteq> a ! q} \<union> set (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]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
propa f (step (hd b) (a ! hd b)) a (tl b) = (merges f (step (hd b) (a ! hd b)) a, sorted_list_of_set ({q. \<exists>t. (q, t) \<in> set (step (hd b) (a ! hd b)) \<and> t \<squnion>\<^bsub>f\<^esub> a ! q \<noteq> a ! q} \<union> set (tl b)))
((merges f (step (hd b) (a ! hd b)) a, sorted_list_of_set ({q. \<exists>t. (q, t) \<in> set (step (hd b) (a ! hd b)) \<and> t \<squnion>\<^bsub>f\<^esub> a ! q \<noteq> a ! q} \<union> set (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

goal (1 subgoal):
 1. (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]
by auto
[PROOF STATE]
proof (state)
this:
(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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma iter_dom_invariant:
  assumes "wf_dom ss0 w0"
    shows "iter f step ss0 w0 = (ss',w') \<longrightarrow> wf_dom ss' w'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iter f step ss0 w0 = (ss', w') \<longrightarrow> wf_dom ss' w'
[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'
[PROOF STEP]
apply (unfold iter_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'
[PROOF STEP]
apply(rule_tac
      P = "(\<lambda>(ss, w). wf_dom ss w )" 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 (x, xa) \<Rightarrow> wf_dom x xa
 2. \<And>s. \<lbrakk>wf_dom ss0 w0; case s of (x, xa) \<Rightarrow> wf_dom x xa; 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 (x, xa) \<Rightarrow> wf_dom x xa
 3. \<And>s. \<lbrakk>wf_dom ss0 w0; case s of (x, xa) \<Rightarrow> wf_dom x xa; \<not> (case s of (\<tau>s, w) \<Rightarrow> w \<noteq> [])\<rbrakk> \<Longrightarrow> s = (ss', w') \<longrightarrow> wf_dom ss' w'
 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 (x, xa) \<Rightarrow> wf_dom x xa; 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)

  \<comment> \<open>Invariant is preserved:\<close>
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>s. \<lbrakk>wf_dom ss0 w0; case s of (x, xa) \<Rightarrow> wf_dom x xa; 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 (x, xa) \<Rightarrow> wf_dom x xa
 2. \<And>s. \<lbrakk>wf_dom ss0 w0; case s of (x, xa) \<Rightarrow> wf_dom x xa; \<not> (case s of (\<tau>s, w) \<Rightarrow> w \<noteq> [])\<rbrakk> \<Longrightarrow> s = (ss', w') \<longrightarrow> wf_dom ss' w'
 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 (x, xa) \<Rightarrow> wf_dom x xa; 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)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>s. \<lbrakk>(\<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); case s of (ss, w) \<Rightarrow> (\<forall>\<tau>\<in>set ss. \<tau> \<in> A) \<and> (\<forall>p<n. Sorted_Less.sorted (rev (ss ! p)) \<and> (ss ! p \<noteq> rev [0..<n] \<longrightarrow> (\<forall>x\<in>set (ss ! p). x < p)) \<and> (ss ! p = rev [0..<n] \<longrightarrow> (\<exists>x\<in>set w. (x, p) \<in> g_E G \<and> x < p)) \<and> (p \<notin> set w \<longrightarrow> Typing_Framework_1.stable r step ss p)) \<and> Sorted_Less.sorted w \<and> length ss = n \<and> (\<forall>x\<in>set w. x < n); case s of (\<tau>s, w) \<Rightarrow> w \<noteq> []\<rbrakk> \<Longrightarrow> case case s of (\<tau>s, w) \<Rightarrow> propa f (step (hd w) (\<tau>s ! hd w)) \<tau>s (tl w) of (ss, w) \<Rightarrow> (\<forall>\<tau>\<in>set ss. \<tau> \<in> A) \<and> (\<forall>p<n. Sorted_Less.sorted (rev (ss ! p)) \<and> (ss ! p \<noteq> rev [0..<n] \<longrightarrow> (\<forall>x\<in>set (ss ! p). x < p)) \<and> (ss ! p = rev [0..<n] \<longrightarrow> (\<exists>x\<in>set w. (x, p) \<in> g_E G \<and> x < p)) \<and> (p \<notin> set w \<longrightarrow> Typing_Framework_1.stable r step ss p)) \<and> Sorted_Less.sorted w \<and> length ss = n \<and> (\<forall>x\<in>set w. x < n)
 2. \<And>s. \<lbrakk>wf_dom ss0 w0; case s of (x, xa) \<Rightarrow> wf_dom x xa; \<not> (case s of (\<tau>s, w) \<Rightarrow> w \<noteq> [])\<rbrakk> \<Longrightarrow> s = (ss', w') \<longrightarrow> wf_dom ss' w'
 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 (x, xa) \<Rightarrow> wf_dom x xa; 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>b \<noteq> []; propa f (step (hd b) (a ! hd b)) a (tl b) = (ss, w); \<forall>\<tau>\<in>set ss0. \<tau> \<in> A; \<forall>\<tau>\<in>set a. \<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); \<forall>p<length ss0. Sorted_Less.sorted (rev (a ! p)) \<and> (a ! p \<noteq> rev [0..<length ss0] \<longrightarrow> (\<forall>x\<in>set (a ! p). x < p)) \<and> (a ! p = rev [0..<length ss0] \<longrightarrow> (\<exists>x\<in>set b. (x, p) \<in> g_E G \<and> x < p)) \<and> (p \<notin> set b \<longrightarrow> Typing_Framework_1.stable r step a p); Sorted_Less.sorted w0; Sorted_Less.sorted b; \<forall>x\<in>set w0. x < length ss0; n = length ss0; length a = length ss0; \<forall>x\<in>set b. x < length ss0\<rbrakk> \<Longrightarrow> (\<forall>\<tau>\<in>set ss. \<tau> \<in> A) \<and> (\<forall>p<length ss0. Sorted_Less.sorted (rev (ss ! p)) \<and> (ss ! p \<noteq> rev [0..<length ss0] \<longrightarrow> (\<forall>x\<in>set (ss ! p). x < p)) \<and> (ss ! p = rev [0..<length ss0] \<longrightarrow> (\<exists>x\<in>set w. (x, p) \<in> g_E G \<and> x < p)) \<and> (p \<notin> set w \<longrightarrow> Typing_Framework_1.stable r step ss p)) \<and> Sorted_Less.sorted w \<and> length ss = length ss0 \<and> (\<forall>x\<in>set w. x < length ss0)
 2. \<And>s. \<lbrakk>wf_dom ss0 w0; case s of (x, xa) \<Rightarrow> wf_dom x xa; \<not> (case s of (\<tau>s, w) \<Rightarrow> w \<noteq> [])\<rbrakk> \<Longrightarrow> s = (ss', w') \<longrightarrow> wf_dom ss' w'
 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 (x, xa) \<Rightarrow> wf_dom x xa; 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_aux')
[PROOF STATE]
proof (prove)
goal (11 subgoals):
 1. \<And>a b ss w. \<lbrakk>b \<noteq> []; propa f (step (hd b) (a ! hd b)) a (tl b) = (ss, w); \<forall>\<tau>\<in>set ss0. \<tau> \<in> A; \<forall>\<tau>\<in>set a. \<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); \<forall>p<length ss0. Sorted_Less.sorted (rev (a ! p)) \<and> (a ! p \<noteq> rev [0..<length ss0] \<longrightarrow> (\<forall>x\<in>set (a ! p). x < p)) \<and> (a ! p = rev [0..<length ss0] \<longrightarrow> (\<exists>x\<in>set b. (x, p) \<in> g_E G \<and> x < p)) \<and> (p \<notin> set b \<longrightarrow> Typing_Framework_1.stable r step a p); Sorted_Less.sorted w0; Sorted_Less.sorted b; \<forall>x\<in>set w0. x < length ss0; n = length ss0; length a = length ss0; \<forall>x\<in>set b. x < length ss0\<rbrakk> \<Longrightarrow> propa f (step (hd (?b16 a b ss w)) (?a16 a b ss w ! hd (?b16 a b ss w))) (?a16 a b ss w) (tl (?b16 a b ss w)) = (ss, w)
 2. \<And>a b ss w. \<lbrakk>b \<noteq> []; propa f (step (hd b) (a ! hd b)) a (tl b) = (ss, w); \<forall>\<tau>\<in>set ss0. \<tau> \<in> A; \<forall>\<tau>\<in>set a. \<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); \<forall>p<length ss0. Sorted_Less.sorted (rev (a ! p)) \<and> (a ! p \<noteq> rev [0..<length ss0] \<longrightarrow> (\<forall>x\<in>set (a ! p). x < p)) \<and> (a ! p = rev [0..<length ss0] \<longrightarrow> (\<exists>x\<in>set b. (x, p) \<in> g_E G \<and> x < p)) \<and> (p \<notin> set b \<longrightarrow> Typing_Framework_1.stable r step a p); Sorted_Less.sorted w0; Sorted_Less.sorted b; \<forall>x\<in>set w0. x < length ss0; n = length ss0; length a = length ss0; \<forall>x\<in>set b. x < length ss0\<rbrakk> \<Longrightarrow> ?b16 a b ss w \<noteq> []
 3. \<And>a b ss w. \<lbrakk>b \<noteq> []; propa f (step (hd b) (a ! hd b)) a (tl b) = (ss, w); \<forall>\<tau>\<in>set ss0. \<tau> \<in> A; \<forall>\<tau>\<in>set a. \<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); \<forall>p<length ss0. Sorted_Less.sorted (rev (a ! p)) \<and> (a ! p \<noteq> rev [0..<length ss0] \<longrightarrow> (\<forall>x\<in>set (a ! p). x < p)) \<and> (a ! p = rev [0..<length ss0] \<longrightarrow> (\<exists>x\<in>set b. (x, p) \<in> g_E G \<and> x < p)) \<and> (p \<notin> set b \<longrightarrow> Typing_Framework_1.stable r step a p); Sorted_Less.sorted w0; Sorted_Less.sorted b; \<forall>x\<in>set w0. x < length ss0; n = length ss0; length a = length ss0; \<forall>x\<in>set b. x < length ss0\<rbrakk> \<Longrightarrow> \<forall>\<tau>\<in>set (?a16 a b ss w). \<tau> \<in> A
 4. \<And>a b ss w. \<lbrakk>b \<noteq> []; propa f (step (hd b) (a ! hd b)) a (tl b) = (ss, w); \<forall>\<tau>\<in>set ss0. \<tau> \<in> A; \<forall>\<tau>\<in>set a. \<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); \<forall>p<length ss0. Sorted_Less.sorted (rev (a ! p)) \<and> (a ! p \<noteq> rev [0..<length ss0] \<longrightarrow> (\<forall>x\<in>set (a ! p). x < p)) \<and> (a ! p = rev [0..<length ss0] \<longrightarrow> (\<exists>x\<in>set b. (x, p) \<in> g_E G \<and> x < p)) \<and> (p \<notin> set b \<longrightarrow> Typing_Framework_1.stable r step a p); Sorted_Less.sorted w0; Sorted_Less.sorted b; \<forall>x\<in>set w0. x < length ss0; n = length ss0; length a = length ss0; \<forall>x\<in>set b. x < length ss0\<rbrakk> \<Longrightarrow> \<forall>p<length ss0. Sorted_Less.sorted (rev (?a16 a b ss w ! p)) \<and> (?a16 a b ss w ! p \<noteq> rev [0..<length ss0] \<longrightarrow> (\<forall>x\<in>set (?a16 a b ss w ! p). x < p)) \<and> (?a16 a b ss w ! p = rev [0..<length ss0] \<longrightarrow> (\<exists>x\<in>set (?b16 a b ss w). (x, p) \<in> g_E G \<and> x < p)) \<and> (p \<notin> set (?b16 a b ss w) \<longrightarrow> Typing_Framework_1.stable r step (?a16 a b ss w) p)
 5. \<And>a b ss w. \<lbrakk>b \<noteq> []; propa f (step (hd b) (a ! hd b)) a (tl b) = (ss, w); \<forall>\<tau>\<in>set ss0. \<tau> \<in> A; \<forall>\<tau>\<in>set a. \<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); \<forall>p<length ss0. Sorted_Less.sorted (rev (a ! p)) \<and> (a ! p \<noteq> rev [0..<length ss0] \<longrightarrow> (\<forall>x\<in>set (a ! p). x < p)) \<and> (a ! p = rev [0..<length ss0] \<longrightarrow> (\<exists>x\<in>set b. (x, p) \<in> g_E G \<and> x < p)) \<and> (p \<notin> set b \<longrightarrow> Typing_Framework_1.stable r step a p); Sorted_Less.sorted w0; Sorted_Less.sorted b; \<forall>x\<in>set w0. x < length ss0; n = length ss0; length a = length ss0; \<forall>x\<in>set b. x < length ss0\<rbrakk> \<Longrightarrow> Sorted_Less.sorted (?b16 a b ss w)
 6. \<And>a b ss w. \<lbrakk>b \<noteq> []; propa f (step (hd b) (a ! hd b)) a (tl b) = (ss, w); \<forall>\<tau>\<in>set ss0. \<tau> \<in> A; \<forall>\<tau>\<in>set a. \<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); \<forall>p<length ss0. Sorted_Less.sorted (rev (a ! p)) \<and> (a ! p \<noteq> rev [0..<length ss0] \<longrightarrow> (\<forall>x\<in>set (a ! p). x < p)) \<and> (a ! p = rev [0..<length ss0] \<longrightarrow> (\<exists>x\<in>set b. (x, p) \<in> g_E G \<and> x < p)) \<and> (p \<notin> set b \<longrightarrow> Typing_Framework_1.stable r step a p); Sorted_Less.sorted w0; Sorted_Less.sorted b; \<forall>x\<in>set w0. x < length ss0; n = length ss0; length a = length ss0; \<forall>x\<in>set b. x < length ss0\<rbrakk> \<Longrightarrow> n = length ss0
 7. \<And>a b ss w. \<lbrakk>b \<noteq> []; propa f (step (hd b) (a ! hd b)) a (tl b) = (ss, w); \<forall>\<tau>\<in>set ss0. \<tau> \<in> A; \<forall>\<tau>\<in>set a. \<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); \<forall>p<length ss0. Sorted_Less.sorted (rev (a ! p)) \<and> (a ! p \<noteq> rev [0..<length ss0] \<longrightarrow> (\<forall>x\<in>set (a ! p). x < p)) \<and> (a ! p = rev [0..<length ss0] \<longrightarrow> (\<exists>x\<in>set b. (x, p) \<in> g_E G \<and> x < p)) \<and> (p \<notin> set b \<longrightarrow> Typing_Framework_1.stable r step a p); Sorted_Less.sorted w0; Sorted_Less.sorted b; \<forall>x\<in>set w0. x < length ss0; n = length ss0; length a = length ss0; \<forall>x\<in>set b. x < length ss0\<rbrakk> \<Longrightarrow> length (?a16 a b ss w) = length ss0
 8. \<And>a b ss w. \<lbrakk>b \<noteq> []; propa f (step (hd b) (a ! hd b)) a (tl b) = (ss, w); \<forall>\<tau>\<in>set ss0. \<tau> \<in> A; \<forall>\<tau>\<in>set a. \<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); \<forall>p<length ss0. Sorted_Less.sorted (rev (a ! p)) \<and> (a ! p \<noteq> rev [0..<length ss0] \<longrightarrow> (\<forall>x\<in>set (a ! p). x < p)) \<and> (a ! p = rev [0..<length ss0] \<longrightarrow> (\<exists>x\<in>set b. (x, p) \<in> g_E G \<and> x < p)) \<and> (p \<notin> set b \<longrightarrow> Typing_Framework_1.stable r step a p); Sorted_Less.sorted w0; Sorted_Less.sorted b; \<forall>x\<in>set w0. x < length ss0; n = length ss0; length a = length ss0; \<forall>x\<in>set b. x < length ss0\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (?b16 a b ss w). x < length ss0
 9. \<And>s. \<lbrakk>wf_dom ss0 w0; case s of (x, xa) \<Rightarrow> wf_dom x xa; \<not> (case s of (\<tau>s, w) \<Rightarrow> w \<noteq> [])\<rbrakk> \<Longrightarrow> s = (ss', w') \<longrightarrow> wf_dom ss' w'
 10. 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)
A total of 11 subgoals...
[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 (x, xa) \<Rightarrow> wf_dom x xa; \<not> (case s of (\<tau>s, w) \<Rightarrow> w \<noteq> [])\<rbrakk> \<Longrightarrow> s = (ss', w') \<longrightarrow> wf_dom ss' w'
 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 (x, xa) \<Rightarrow> wf_dom x xa; 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

  \<comment> \<open>Well-foundedness of the termination relation:\<close>
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. 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)
 2. \<And>s. \<lbrakk>wf_dom ss0 w0; case s of (x, xa) \<Rightarrow> wf_dom x xa; 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 (x, xa) \<Rightarrow> wf_dom x xa; 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; wf_dom a b; b \<noteq> []\<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