[STATEMENT]
lemma propa_dom_invariant_aux2:
  fixes ss w ssa wa
  assumes wf_dom_ss0_w0: "wf_dom ss0 w0"
      and w_n_nil: "w \<noteq> [] "
      and propa: "propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ssa, wa) "
      and wf_ss_w: "wf_dom ss w "
      and ss0_lt_ss: "ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ss"
      and sta: " \<forall>ts\<in>nlists n A. ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> (\<forall>p<n. stable r step ts p) \<longrightarrow> ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts"
    shows "ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ssa \<and>
           (\<forall>ts\<in>nlists n A. ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> (\<forall>p<n. stable r step ts p) \<longrightarrow> ssa [\<sqsubseteq>\<^bsub>r\<^esub>] ts)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ssa \<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> ssa [\<sqsubseteq>\<^bsub>r\<^esub>] ts)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
wf_dom ss0 w0
w \<noteq> []
propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ssa, wa)
wf_dom ss w
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

goal (1 subgoal):
 1. ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ssa \<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> ssa [\<sqsubseteq>\<^bsub>r\<^esub>] ts)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>wf_dom ss0 w0; w \<noteq> []; propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ssa, wa); wf_dom ss w; 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\<rbrakk> \<Longrightarrow> ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ssa \<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> ssa [\<sqsubseteq>\<^bsub>r\<^esub>] ts)
[PROOF STEP]
let ?ss_hdw = "ss!hd w"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>wf_dom ss0 w0; w \<noteq> []; propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ssa, wa); wf_dom ss w; 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\<rbrakk> \<Longrightarrow> ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ssa \<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> ssa [\<sqsubseteq>\<^bsub>r\<^esub>] ts)
[PROOF STEP]
from wf_dom_ss0_w0
[PROOF STATE]
proof (chain)
picking this:
wf_dom ss0 w0
[PROOF STEP]
have len_ss0: "length ss0 = n" and "\<forall>x\<in> set ss0. x \<in> A"
[PROOF STATE]
proof (prove)
using this:
wf_dom ss0 w0

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

goal (1 subgoal):
 1. \<lbrakk>wf_dom ss0 w0; w \<noteq> []; propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ssa, wa); wf_dom ss w; 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\<rbrakk> \<Longrightarrow> ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ssa \<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> ssa [\<sqsubseteq>\<^bsub>r\<^esub>] ts)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length ss0 = n
\<forall>x\<in>set ss0. x \<in> A
[PROOF STEP]
have ss0_inA:  "ss0 \<in> nlists n A"  and set_ss0: "set ss0 \<subseteq> A"
[PROOF STATE]
proof (prove)
using this:
length ss0 = n
\<forall>x\<in>set ss0. x \<in> A

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

goal (1 subgoal):
 1. \<lbrakk>wf_dom ss0 w0; w \<noteq> []; propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ssa, wa); wf_dom ss w; 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\<rbrakk> \<Longrightarrow> ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ssa \<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> ssa [\<sqsubseteq>\<^bsub>r\<^esub>] ts)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ss0 \<in> nlists n A
set ss0 \<subseteq> A
[PROOF STEP]
have ss0_nth_inA: "\<forall>i<length ss0. ss0!i \<in> A"
[PROOF STATE]
proof (prove)
using this:
ss0 \<in> nlists n A
set ss0 \<subseteq> A

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

goal (1 subgoal):
 1. \<lbrakk>wf_dom ss0 w0; w \<noteq> []; propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ssa, wa); wf_dom ss w; 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\<rbrakk> \<Longrightarrow> ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ssa \<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> ssa [\<sqsubseteq>\<^bsub>r\<^esub>] ts)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>i<length ss0. ss0 ! i \<in> A
[PROOF STEP]
have ss0_p_subset: "\<forall>p< length ss0. set (ss0!p) \<subseteq> set nodes"
[PROOF STATE]
proof (prove)
using this:
\<forall>i<length ss0. ss0 ! i \<in> A

goal (1 subgoal):
 1. \<forall>p<length ss0. set (ss0 ! p) \<subseteq> set nodes
[PROOF STEP]
by (auto simp add:inpow_subset_nodes A_def)
[PROOF STATE]
proof (state)
this:
\<forall>p<length ss0. set (ss0 ! p) \<subseteq> set nodes

goal (1 subgoal):
 1. \<lbrakk>wf_dom ss0 w0; w \<noteq> []; propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ssa, wa); wf_dom ss w; 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\<rbrakk> \<Longrightarrow> ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ssa \<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> ssa [\<sqsubseteq>\<^bsub>r\<^esub>] ts)
[PROOF STEP]
from len_ss0 n_def nodes_def len_verts_gt0
[PROOF STATE]
proof (chain)
picking this:
length ss0 = n
n \<equiv> length nodes
nodes \<equiv> g_V G
0 < length (g_V G)
[PROOF STEP]
have "0 < length ss0"
[PROOF STATE]
proof (prove)
using this:
length ss0 = n
n \<equiv> length nodes
nodes \<equiv> g_V G
0 < length (g_V G)

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

goal (1 subgoal):
 1. \<lbrakk>wf_dom ss0 w0; w \<noteq> []; propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ssa, wa); wf_dom ss w; 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\<rbrakk> \<Longrightarrow> ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ssa \<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> ssa [\<sqsubseteq>\<^bsub>r\<^esub>] ts)
[PROOF STEP]
from ss0_lt_ss
[PROOF STATE]
proof (chain)
picking this:
ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ss
[PROOF STEP]
have "list_all2 (\<lambda>x y. x \<sqsubseteq>\<^sub>r y) ss0 ss"
[PROOF STATE]
proof (prove)
using this:
ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ss

goal (1 subgoal):
 1. list_all2 (\<lambda>x. lesub x r) ss0 ss
[PROOF STEP]
by (auto simp add:lesssub_def lesub_def list_all2_def Listn.le_def)
[PROOF STATE]
proof (state)
this:
list_all2 (\<lambda>x. lesub x r) ss0 ss

goal (1 subgoal):
 1. \<lbrakk>wf_dom ss0 w0; w \<noteq> []; propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ssa, wa); wf_dom ss w; 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\<rbrakk> \<Longrightarrow> ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ssa \<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> ssa [\<sqsubseteq>\<^bsub>r\<^esub>] ts)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
list_all2 (\<lambda>x. lesub x r) ss0 ss
[PROOF STEP]
have lt1: "\<forall>p<length ss0. ss0 !p \<sqsubseteq>\<^bsub>r\<^esub> ss!p"
[PROOF STATE]
proof (prove)
using this:
list_all2 (\<lambda>x. lesub x r) ss0 ss

goal (1 subgoal):
 1. \<forall>p<length ss0. ss0 ! p \<sqsubseteq>\<^bsub>r\<^esub> ss ! p
[PROOF STEP]
by (auto simp add: list_all2_conv_all_nth)
[PROOF STATE]
proof (state)
this:
\<forall>p<length ss0. ss0 ! p \<sqsubseteq>\<^bsub>r\<^esub> ss ! p

goal (1 subgoal):
 1. \<lbrakk>wf_dom ss0 w0; w \<noteq> []; propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ssa, wa); wf_dom ss w; 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\<rbrakk> \<Longrightarrow> ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ssa \<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> ssa [\<sqsubseteq>\<^bsub>r\<^esub>] ts)
[PROOF STEP]
from wf_ss_w
[PROOF STATE]
proof (chain)
picking this:
wf_dom ss w
[PROOF STEP]
have  "\<forall>\<tau>\<in>set ss. \<tau> \<in> A"
                and ass1: "\<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_w: "sorted w"
                and len_ss: "length ss = n"
                and w_lt_n: "\<forall>x\<in>set w. x < n  "
[PROOF STATE]
proof (prove)
using this:
wf_dom ss w

goal (1 subgoal):
 1. (\<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]
by (auto simp add:wf_dom_def)
[PROOF STATE]
proof (state)
this:
\<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. \<lbrakk>wf_dom ss0 w0; w \<noteq> []; propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ssa, wa); wf_dom ss w; 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\<rbrakk> \<Longrightarrow> ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ssa \<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> ssa [\<sqsubseteq>\<^bsub>r\<^esub>] ts)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<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]
have ss_inA: "ss \<in> nlists n A" and set_ss: "set ss \<subseteq> A"
[PROOF STATE]
proof (prove)
using this:
\<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. ss \<in> nlists n A &&& set ss \<subseteq> A
[PROOF STEP]
by (auto intro:nlistsI)
[PROOF STATE]
proof (state)
this:
ss \<in> nlists n A
set ss \<subseteq> A

goal (1 subgoal):
 1. \<lbrakk>wf_dom ss0 w0; w \<noteq> []; propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ssa, wa); wf_dom ss w; 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\<rbrakk> \<Longrightarrow> ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ssa \<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> ssa [\<sqsubseteq>\<^bsub>r\<^esub>] ts)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ss \<in> nlists n A
set ss \<subseteq> A
[PROOF STEP]
have ss_nth_inA: "\<forall>i<length ss. ss!i \<in> A"
[PROOF STATE]
proof (prove)
using this:
ss \<in> nlists n A
set ss \<subseteq> A

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

goal (1 subgoal):
 1. \<lbrakk>wf_dom ss0 w0; w \<noteq> []; propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ssa, wa); wf_dom ss w; 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\<rbrakk> \<Longrightarrow> ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ssa \<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> ssa [\<sqsubseteq>\<^bsub>r\<^esub>] ts)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>i<length ss. ss ! i \<in> A
[PROOF STEP]
have ss_p_subset: "\<forall>p< length ss. set (ss!p) \<subseteq> set nodes"
[PROOF STATE]
proof (prove)
using this:
\<forall>i<length ss. ss ! i \<in> A

goal (1 subgoal):
 1. \<forall>p<length ss. set (ss ! p) \<subseteq> set nodes
[PROOF STEP]
by (auto simp add:inpow_subset_nodes A_def)
[PROOF STATE]
proof (state)
this:
\<forall>p<length ss. set (ss ! p) \<subseteq> set nodes

goal (1 subgoal):
 1. \<lbrakk>wf_dom ss0 w0; w \<noteq> []; propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ssa, wa); wf_dom ss w; 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\<rbrakk> \<Longrightarrow> ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ssa \<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> ssa [\<sqsubseteq>\<^bsub>r\<^esub>] ts)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>p<length ss. set (ss ! p) \<subseteq> set nodes
[PROOF STEP]
have ss_hdw_nodes: "set ?ss_hdw \<subseteq> set nodes"
[PROOF STATE]
proof (prove)
using this:
\<forall>p<length ss. set (ss ! p) \<subseteq> set nodes

goal (1 subgoal):
 1. set (ss ! hd w) \<subseteq> set nodes
[PROOF STEP]
using w_lt_n w_n_nil len_ss
[PROOF STATE]
proof (prove)
using this:
\<forall>p<length ss. set (ss ! p) \<subseteq> set nodes
\<forall>x\<in>set w. x < n
w \<noteq> []
length ss = n

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

goal (1 subgoal):
 1. \<lbrakk>wf_dom ss0 w0; w \<noteq> []; propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ssa, wa); wf_dom ss w; 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\<rbrakk> \<Longrightarrow> ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ssa \<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> ssa [\<sqsubseteq>\<^bsub>r\<^esub>] ts)
[PROOF STEP]
let ?qs = "step (hd w) ?ss_hdw"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>wf_dom ss0 w0; w \<noteq> []; propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ssa, wa); wf_dom ss w; 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\<rbrakk> \<Longrightarrow> ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ssa \<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> ssa [\<sqsubseteq>\<^bsub>r\<^esub>] ts)
[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>wf_dom ss0 w0; w \<noteq> []; propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ssa, wa); wf_dom ss w; 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\<rbrakk> \<Longrightarrow> ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ssa \<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> ssa [\<sqsubseteq>\<^bsub>r\<^esub>] ts)
[PROOF STEP]
then
[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>wf_dom ss0 w0; w \<noteq> []; propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ssa, wa); wf_dom ss w; 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\<rbrakk> \<Longrightarrow> ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ssa \<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> ssa [\<sqsubseteq>\<^bsub>r\<^esub>] ts)
[PROOF STEP]
from ss_nth_inA
[PROOF STATE]
proof (chain)
picking this:
\<forall>i<length ss. ss ! i \<in> A
[PROOF STEP]
have ss_hdw_inA: "?ss_hdw \<in> A"
[PROOF STATE]
proof (prove)
using this:
\<forall>i<length ss. ss ! i \<in> A

goal (1 subgoal):
 1. ss ! hd w \<in> A
[PROOF STEP]
using w_lt_n w_n_nil len_ss
[PROOF STATE]
proof (prove)
using this:
\<forall>i<length ss. ss ! i \<in> A
\<forall>x\<in>set w. x < n
w \<noteq> []
length ss = n

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

goal (1 subgoal):
 1. \<lbrakk>wf_dom ss0 w0; w \<noteq> []; propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ssa, wa); wf_dom ss w; 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\<rbrakk> \<Longrightarrow> ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ssa \<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> ssa [\<sqsubseteq>\<^bsub>r\<^esub>] ts)
[PROOF STEP]
from ass1
[PROOF STATE]
proof (chain)
picking 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)
[PROOF STEP]
have sorted_ss_hdw: "sorted (rev ?ss_hdw)"
[PROOF STATE]
proof (prove)
using 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)

goal (1 subgoal):
 1. Sorted_Less.sorted (rev (ss ! hd w))
[PROOF STEP]
using w_lt_n w_n_nil
[PROOF STATE]
proof (prove)
using 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)
\<forall>x\<in>set w. x < n
w \<noteq> []

goal (1 subgoal):
 1. Sorted_Less.sorted (rev (ss ! hd w))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Sorted_Less.sorted (rev (ss ! hd w))

goal (1 subgoal):
 1. \<lbrakk>wf_dom ss0 w0; w \<noteq> []; propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ssa, wa); wf_dom ss w; 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\<rbrakk> \<Longrightarrow> ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ssa \<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> ssa [\<sqsubseteq>\<^bsub>r\<^esub>] ts)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Sorted_Less.sorted (rev (ss ! hd w))
[PROOF STEP]
have "\<forall>q\<in>succs (hd w). q \<in> set (g_V G)"
[PROOF STATE]
proof (prove)
using this:
Sorted_Less.sorted (rev (ss ! hd w))

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

goal (1 subgoal):
 1. \<lbrakk>wf_dom ss0 w0; w \<noteq> []; propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ssa, wa); wf_dom ss w; 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\<rbrakk> \<Longrightarrow> ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ssa \<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> ssa [\<sqsubseteq>\<^bsub>r\<^esub>] ts)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>q\<in>succs (hd w). q \<in> set (g_V G)
[PROOF STEP]
have hd_w_suc_lt_n: "\<forall>q\<in>succs (hd w). q < n"
[PROOF STATE]
proof (prove)
using this:
\<forall>q\<in>succs (hd w). q \<in> set (g_V G)

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

goal (1 subgoal):
 1. \<forall>q\<in>succs (hd w). q < n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>q\<in>succs (hd w). q < n

goal (1 subgoal):
 1. \<lbrakk>wf_dom ss0 w0; w \<noteq> []; propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ssa, wa); wf_dom ss w; 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\<rbrakk> \<Longrightarrow> ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ssa \<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> ssa [\<sqsubseteq>\<^bsub>r\<^esub>] ts)
[PROOF STEP]
have hdw_in_nodes:"hd w \<in> set (g_V G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hd w \<in> set (g_V G)
[PROOF STEP]
using verts_set n_def nodes_def w_lt_n w_n_nil
[PROOF STATE]
proof (prove)
using this:
set (g_V G) = {0..<length (g_V G)}
n \<equiv> length nodes
nodes \<equiv> g_V G
\<forall>x\<in>set w. x < n
w \<noteq> []

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>wf_dom ss0 w0; w \<noteq> []; propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ssa, wa); wf_dom ss w; 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\<rbrakk> \<Longrightarrow> ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ssa \<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> ssa [\<sqsubseteq>\<^bsub>r\<^esub>] ts)
[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
[PROOF STATE]
proof (prove)
using this:
hd w \<in> set (g_V G)
\<forall>v\<in>set (g_V G). finite (succs v)

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>wf_dom ss0 w0; w \<noteq> []; propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ssa, wa); wf_dom ss w; 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\<rbrakk> \<Longrightarrow> ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ssa \<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> ssa [\<sqsubseteq>\<^bsub>r\<^esub>] ts)
[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]
using w_n_nil
[PROOF STATE]
proof (prove)
using this:
Sorted_Less.sorted w
w \<noteq> []

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>wf_dom ss0 w0; w \<noteq> []; propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ssa, wa); wf_dom ss w; 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\<rbrakk> \<Longrightarrow> ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ssa \<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> ssa [\<sqsubseteq>\<^bsub>r\<^esub>] ts)
[PROOF STEP]
from wf_ss_w w_n_nil
[PROOF STATE]
proof (chain)
picking this:
wf_dom ss w
w \<noteq> []
[PROOF STEP]
have ss_hd_w_neq_all: "?ss_hdw \<noteq> (rev [0..<n])"
                        and sorted_hd_w_ss: "sorted (rev (hd w # ?ss_hdw))"
                        and hdb_subset_nodes: "set (hd w # ?ss_hdw) \<subseteq> set nodes"
                        and hd_w_ss_in_A: " (hd w # ?ss_hdw) \<in> A"
                        and step_pres_bounded: " \<forall>(q, \<tau>)\<in>set (step (hd w) ?ss_hdw). q < length ss \<and> \<tau> \<in> A"
[PROOF STATE]
proof (prove)
using this:
wf_dom ss w
w \<noteq> []

goal (1 subgoal):
 1. (ss ! hd w \<noteq> rev [0..<n] &&& Sorted_Less.sorted (rev (hd w # ss ! hd w))) &&& set (hd w # ss ! hd w) \<subseteq> set nodes &&& 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. (ss ! hd w \<noteq> rev [0..<n] &&& Sorted_Less.sorted (rev (hd w # ss ! hd w))) &&& set (hd w # ss ! hd w) \<subseteq> set nodes &&& 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:
ss ! hd w \<noteq> rev [0..<n]
Sorted_Less.sorted (rev (hd w # ss ! hd w))
set (hd w # ss ! hd w) \<subseteq> set nodes
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>wf_dom ss0 w0; w \<noteq> []; propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ssa, wa); wf_dom ss w; 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\<rbrakk> \<Longrightarrow> ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ssa \<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> ssa [\<sqsubseteq>\<^bsub>r\<^esub>] ts)
[PROOF STEP]
from ss_hd_w_neq_all
[PROOF STATE]
proof (chain)
picking this:
ss ! hd w \<noteq> rev [0..<n]
[PROOF STEP]
have ss_lt_hd_w: "\<forall>x\<in>set ?ss_hdw. x < hd w"
[PROOF STATE]
proof (prove)
using this:
ss ! hd w \<noteq> rev [0..<n]

goal (1 subgoal):
 1. \<forall>x\<in>set (ss ! hd w). x < hd w
[PROOF STEP]
using hd_w_lt_n wf_ss_w
[PROOF STATE]
proof (prove)
using this:
ss ! hd w \<noteq> rev [0..<n]
hd w < n
wf_dom ss w

goal (1 subgoal):
 1. \<forall>x\<in>set (ss ! hd w). x < hd w
[PROOF STEP]
by (auto simp add:wf_dom_def)
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>set (ss ! hd w). x < hd w

goal (1 subgoal):
 1. \<lbrakk>wf_dom ss0 w0; w \<noteq> []; propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ssa, wa); wf_dom ss w; 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\<rbrakk> \<Longrightarrow> ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ssa \<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> ssa [\<sqsubseteq>\<^bsub>r\<^esub>] ts)
[PROOF STEP]
from wf_ss_w w_n_nil propa
[PROOF STATE]
proof (chain)
picking this:
wf_dom ss w
w \<noteq> []
propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ssa, wa)
[PROOF STEP]
have wf_ssa_wa: "wf_dom ssa wa"
[PROOF STATE]
proof (prove)
using this:
wf_dom ss w
w \<noteq> []
propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ssa, wa)

goal (1 subgoal):
 1. wf_dom ssa wa
[PROOF STEP]
using propa_dom_invariant
[PROOF STATE]
proof (prove)
using this:
wf_dom ss w
w \<noteq> []
propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ssa, wa)
\<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'

goal (1 subgoal):
 1. wf_dom ssa wa
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
wf_dom ssa wa

goal (1 subgoal):
 1. \<lbrakk>wf_dom ss0 w0; w \<noteq> []; propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ssa, wa); wf_dom ss w; 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\<rbrakk> \<Longrightarrow> ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ssa \<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> ssa [\<sqsubseteq>\<^bsub>r\<^esub>] ts)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
wf_dom ssa wa
[PROOF STEP]
have sorted_ssa_p: "\<forall>p<n. sorted (rev (ssa!p))"
        and len_ssa: "length ssa = n"
        and "\<forall>x\<in> set ssa. x \<in> A"
        and sorted_wa: "sorted wa"
        and len_ssa: "length ssa = n"
        and wa_lt_n: "\<forall>x\<in> set wa. x < n"
[PROOF STATE]
proof (prove)
using this:
wf_dom ssa wa

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

goal (1 subgoal):
 1. \<lbrakk>wf_dom ss0 w0; w \<noteq> []; propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ssa, wa); wf_dom ss w; 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\<rbrakk> \<Longrightarrow> ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ssa \<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> ssa [\<sqsubseteq>\<^bsub>r\<^esub>] ts)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>p<n. Sorted_Less.sorted (rev (ssa ! p))
length ssa = n
\<forall>x\<in>set ssa. x \<in> A
Sorted_Less.sorted wa
length ssa = n
\<forall>x\<in>set wa. x < n
[PROOF STEP]
have ssa_inA: "ssa\<in> nlists n A" and set_ssa: "set ssa \<subseteq> A"
[PROOF STATE]
proof (prove)
using this:
\<forall>p<n. Sorted_Less.sorted (rev (ssa ! p))
length ssa = n
\<forall>x\<in>set ssa. x \<in> A
Sorted_Less.sorted wa
length ssa = n
\<forall>x\<in>set wa. x < n

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

goal (1 subgoal):
 1. \<lbrakk>wf_dom ss0 w0; w \<noteq> []; propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ssa, wa); wf_dom ss w; 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\<rbrakk> \<Longrightarrow> ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ssa \<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> ssa [\<sqsubseteq>\<^bsub>r\<^esub>] ts)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ssa \<in> nlists n A
set ssa \<subseteq> A
[PROOF STEP]
have ssa_nth_inA: "\<forall>i<length ssa. ssa!i \<in> A"
[PROOF STATE]
proof (prove)
using this:
ssa \<in> nlists n A
set ssa \<subseteq> A

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

goal (1 subgoal):
 1. \<lbrakk>wf_dom ss0 w0; w \<noteq> []; propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ssa, wa); wf_dom ss w; 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\<rbrakk> \<Longrightarrow> ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ssa \<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> ssa [\<sqsubseteq>\<^bsub>r\<^esub>] ts)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>i<length ssa. ssa ! i \<in> A
[PROOF STEP]
have ssa_p_subset: "\<forall>p< length ssa. set (ssa!p) \<subseteq> set nodes"
[PROOF STATE]
proof (prove)
using this:
\<forall>i<length ssa. ssa ! i \<in> A

goal (1 subgoal):
 1. \<forall>p<length ssa. set (ssa ! p) \<subseteq> set nodes
[PROOF STEP]
by (auto simp add:inpow_subset_nodes A_def)
[PROOF STATE]
proof (state)
this:
\<forall>p<length ssa. set (ssa ! p) \<subseteq> set nodes

goal (1 subgoal):
 1. \<lbrakk>wf_dom ss0 w0; w \<noteq> []; propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ssa, wa); wf_dom ss w; 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\<rbrakk> \<Longrightarrow> ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ssa \<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> ssa [\<sqsubseteq>\<^bsub>r\<^esub>] ts)
[PROOF STEP]
from len_ss0 len_ssa
[PROOF STATE]
proof (chain)
picking this:
length ss0 = n
length ssa = n
[PROOF STEP]
have len_ss0_ssa: "length ss0 = length ssa"
[PROOF STATE]
proof (prove)
using this:
length ss0 = n
length ssa = n

goal (1 subgoal):
 1. length ss0 = length ssa
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length ss0 = length ssa

goal (1 subgoal):
 1. \<lbrakk>wf_dom ss0 w0; w \<noteq> []; propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ssa, wa); wf_dom ss w; 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\<rbrakk> \<Longrightarrow> ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ssa \<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> ssa [\<sqsubseteq>\<^bsub>r\<^esub>] ts)
[PROOF STEP]
from len_ss0 len_ss
[PROOF STATE]
proof (chain)
picking this:
length ss0 = n
length ss = n
[PROOF STEP]
have len_ss0_ss:  "length ss0 = length ss"
[PROOF STATE]
proof (prove)
using this:
length ss0 = n
length ss = n

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

goal (1 subgoal):
 1. \<lbrakk>wf_dom ss0 w0; w \<noteq> []; propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ssa, wa); wf_dom ss w; 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\<rbrakk> \<Longrightarrow> ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ssa \<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> ssa [\<sqsubseteq>\<^bsub>r\<^esub>] ts)
[PROOF STEP]
have "\<forall>(q, \<tau>)\<in>set ?qs. \<tau> = transf (hd w) (ss!(hd w))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>(q, \<tau>)\<in>set (step (hd w) (ss ! hd w)). \<tau> = transf (hd w) (ss ! hd w)
[PROOF STEP]
by (simp add:step_def exec_def)
[PROOF STATE]
proof (state)
this:
\<forall>(q, \<tau>)\<in>set (step (hd w) (ss ! hd w)). \<tau> = transf (hd w) (ss ! hd w)

goal (1 subgoal):
 1. \<lbrakk>wf_dom ss0 w0; w \<noteq> []; propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ssa, wa); wf_dom ss w; 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\<rbrakk> \<Longrightarrow> ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ssa \<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> ssa [\<sqsubseteq>\<^bsub>r\<^esub>] ts)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>(q, \<tau>)\<in>set (step (hd w) (ss ! hd w)). \<tau> = transf (hd w) (ss ! hd w)
[PROOF STEP]
have transf_ss_hd_w: "\<forall>(q, \<tau>)\<in>set ?qs. \<tau> =  (hd w # ?ss_hdw)"
[PROOF STATE]
proof (prove)
using this:
\<forall>(q, \<tau>)\<in>set (step (hd w) (ss ! hd w)). \<tau> = transf (hd w) (ss ! hd w)

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

goal (1 subgoal):
 1. \<lbrakk>wf_dom ss0 w0; w \<noteq> []; propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ssa, wa); wf_dom ss w; 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\<rbrakk> \<Longrightarrow> ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ssa \<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> ssa [\<sqsubseteq>\<^bsub>r\<^esub>] ts)
[PROOF STEP]
from set_ss step_pres_bounded sorted_tl_w' len_ss dist
[PROOF STATE]
proof (chain)
picking this:
set ss \<subseteq> A
\<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)))
[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:
set ss \<subseteq> A
\<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)))

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>wf_dom ss0 w0; w \<noteq> []; propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ssa, wa); wf_dom ss w; 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\<rbrakk> \<Longrightarrow> ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ssa \<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> ssa [\<sqsubseteq>\<^bsub>r\<^esub>] ts)
[PROOF STEP]
with propa
[PROOF STATE]
proof (chain)
picking this:
propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ssa, wa)
\<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_ss: "\<forall>(q, \<tau>) \<in> set ?qs. ssa!q = \<tau> \<squnion>\<^bsub>f\<^esub>ss!q"
[PROOF STATE]
proof (prove)
using this:
propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ssa, wa)
\<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)). ssa ! q = \<tau> \<squnion>\<^bsub>f\<^esub> ss ! q
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>(q, \<tau>)\<in>set (step (hd w) (ss ! hd w)). ssa ! q = \<tau> \<squnion>\<^bsub>f\<^esub> ss ! q

goal (1 subgoal):
 1. \<lbrakk>wf_dom ss0 w0; w \<noteq> []; propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ssa, wa); wf_dom ss w; 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\<rbrakk> \<Longrightarrow> ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ssa \<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> ssa [\<sqsubseteq>\<^bsub>r\<^esub>] ts)
[PROOF STEP]
with transf_ss_hd_w
[PROOF STATE]
proof (chain)
picking this:
\<forall>(q, \<tau>)\<in>set (step (hd w) (ss ! hd w)). \<tau> = hd w # ss ! hd w
\<forall>(q, \<tau>)\<in>set (step (hd w) (ss ! hd w)). ssa ! q = \<tau> \<squnion>\<^bsub>f\<^esub> ss ! q
[PROOF STEP]
have propa_ss1:  "\<forall>(q, \<tau>) \<in> set ?qs. ssa!q =  (hd w # ?ss_hdw) \<squnion>\<^bsub>f\<^esub>ss!q"
[PROOF STATE]
proof (prove)
using this:
\<forall>(q, \<tau>)\<in>set (step (hd w) (ss ! hd w)). \<tau> = hd w # ss ! hd w
\<forall>(q, \<tau>)\<in>set (step (hd w) (ss ! hd w)). ssa ! q = \<tau> \<squnion>\<^bsub>f\<^esub> ss ! q

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

goal (1 subgoal):
 1. \<lbrakk>wf_dom ss0 w0; w \<noteq> []; propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ssa, wa); wf_dom ss w; 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\<rbrakk> \<Longrightarrow> ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ssa \<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> ssa [\<sqsubseteq>\<^bsub>r\<^esub>] ts)
[PROOF STEP]
from ss_nth_inA step_pres_bounded
[PROOF STATE]
proof (chain)
picking this:
\<forall>i<length ss. ss ! i \<in> A
\<forall>(q, \<tau>)\<in>set (step (hd w) (ss ! hd w)). q < length ss \<and> \<tau> \<in> A
[PROOF STEP]
have "\<forall>(q, \<tau>) \<in> set ?qs. ss!q \<in> A"
[PROOF STATE]
proof (prove)
using this:
\<forall>i<length ss. ss ! i \<in> A
\<forall>(q, \<tau>)\<in>set (step (hd w) (ss ! hd w)). q < length ss \<and> \<tau> \<in> A

goal (1 subgoal):
 1. \<forall>(q, \<tau>)\<in>set (step (hd w) (ss ! hd w)). ss ! q \<in> A
[PROOF STEP]
using hd_w_suc_lt_n fin_succ_hd_w
[PROOF STATE]
proof (prove)
using this:
\<forall>i<length ss. ss ! i \<in> A
\<forall>(q, \<tau>)\<in>set (step (hd w) (ss ! hd w)). q < length ss \<and> \<tau> \<in> A
\<forall>q\<in>succs (hd w). q < n
finite (succs (hd w))

goal (1 subgoal):
 1. \<forall>(q, \<tau>)\<in>set (step (hd w) (ss ! hd w)). ss ! q \<in> A
[PROOF STEP]
by (auto simp add:step_def exec_def)
[PROOF STATE]
proof (state)
this:
\<forall>(q, \<tau>)\<in>set (step (hd w) (ss ! hd w)). ss ! q \<in> A

goal (1 subgoal):
 1. \<lbrakk>wf_dom ss0 w0; w \<noteq> []; propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ssa, wa); wf_dom ss w; 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\<rbrakk> \<Longrightarrow> ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ssa \<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> ssa [\<sqsubseteq>\<^bsub>r\<^esub>] ts)
[PROOF STEP]
from hd_w_ss_in_A this propa_ss1
[PROOF STATE]
proof (chain)
picking this:
hd w # ss ! hd w \<in> A
\<forall>(q, \<tau>)\<in>set (step (hd w) (ss ! hd w)). ss ! q \<in> A
\<forall>(q, \<tau>)\<in>set (step (hd w) (ss ! hd w)). ssa ! q = hd w # ss ! hd w \<squnion>\<^bsub>f\<^esub> ss ! q
[PROOF STEP]
have ss_lt_ssa_q: "\<forall>(q, \<tau>) \<in> set ?qs. ss!q \<sqsubseteq>\<^bsub>r\<^esub> ssa!q"
[PROOF STATE]
proof (prove)
using this:
hd w # ss ! hd w \<in> A
\<forall>(q, \<tau>)\<in>set (step (hd w) (ss ! hd w)). ss ! q \<in> A
\<forall>(q, \<tau>)\<in>set (step (hd w) (ss ! hd w)). ssa ! q = hd w # ss ! hd w \<squnion>\<^bsub>f\<^esub> ss ! q

goal (1 subgoal):
 1. \<forall>(q, \<tau>)\<in>set (step (hd w) (ss ! hd w)). ss ! q \<sqsubseteq>\<^bsub>r\<^esub> ssa ! q
[PROOF STEP]
by (fastforce dest:Semilat.ub2[OF Semilat.intro, OF is_semi])
[PROOF STATE]
proof (state)
this:
\<forall>(q, \<tau>)\<in>set (step (hd w) (ss ! hd w)). ss ! q \<sqsubseteq>\<^bsub>r\<^esub> ssa ! q

goal (1 subgoal):
 1. \<lbrakk>wf_dom ss0 w0; w \<noteq> []; propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ssa, wa); wf_dom ss w; 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\<rbrakk> \<Longrightarrow> ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ssa \<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> ssa [\<sqsubseteq>\<^bsub>r\<^esub>] ts)
[PROOF STEP]
from step_pres_bounded sorted_tl_w' set_ss len_ss 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>wf_dom ss0 w0; w \<noteq> []; propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ssa, wa); wf_dom ss w; 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\<rbrakk> \<Longrightarrow> ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ssa \<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> ssa [\<sqsubseteq>\<^bsub>r\<^esub>] ts)
[PROOF STEP]
with propa
[PROOF STATE]
proof (chain)
picking this:
propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ssa, wa)
\<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 exec2: "\<And>q. q \<notin> set(map fst ?qs) \<Longrightarrow> q < length ss \<Longrightarrow> ssa!q = ss!q"
[PROOF STATE]
proof (prove)
using this:
propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ssa, wa)
\<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> ssa ! 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> ssa ! ?q = ss ! ?q

goal (1 subgoal):
 1. \<lbrakk>wf_dom ss0 w0; w \<noteq> []; propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ssa, wa); wf_dom ss w; 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\<rbrakk> \<Longrightarrow> ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ssa \<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> ssa [\<sqsubseteq>\<^bsub>r\<^esub>] ts)
[PROOF STEP]
have tran_ss_ssa: "\<forall>p<length ss. ss!p \<sqsubseteq>\<^bsub>r\<^esub> ssa!p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>p<length ss. ss ! p \<sqsubseteq>\<^bsub>r\<^esub> ssa ! p
[PROOF STEP]
proof(intro strip)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p. p < length ss \<Longrightarrow> ss ! p \<sqsubseteq>\<^bsub>r\<^esub> ssa ! p
[PROOF STEP]
fix p
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p. p < length ss \<Longrightarrow> ss ! p \<sqsubseteq>\<^bsub>r\<^esub> ssa ! p
[PROOF STEP]
assume "p < length ss"
[PROOF STATE]
proof (state)
this:
p < length ss

goal (1 subgoal):
 1. \<And>p. p < length ss \<Longrightarrow> ss ! p \<sqsubseteq>\<^bsub>r\<^esub> ssa ! p
[PROOF STEP]
with ssa_nth_inA
[PROOF STATE]
proof (chain)
picking this:
\<forall>i<length ssa. ssa ! i \<in> A
p < length ss
[PROOF STEP]
have ssa_p_inA: "ssa!p \<in> A"
[PROOF STATE]
proof (prove)
using this:
\<forall>i<length ssa. ssa ! i \<in> A
p < length ss

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

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

goal (1 subgoal):
 1. \<And>p. p < length ss \<Longrightarrow> ss ! p \<sqsubseteq>\<^bsub>r\<^esub> ssa ! p
[PROOF STEP]
from ss_nth_inA
[PROOF STATE]
proof (chain)
picking this:
\<forall>i<length ss. ss ! i \<in> A
[PROOF STEP]
have ss_p_inA: "ss!p \<in> A"
[PROOF STATE]
proof (prove)
using this:
\<forall>i<length ss. ss ! i \<in> A

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

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

goal (1 subgoal):
 1. \<And>p. p < length ss \<Longrightarrow> ss ! p \<sqsubseteq>\<^bsub>r\<^esub> ssa ! p
[PROOF STEP]
show " ss ! p \<sqsubseteq>\<^bsub>r\<^esub> ssa ! p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ss ! p \<sqsubseteq>\<^bsub>r\<^esub> ssa ! p
[PROOF STEP]
proof(cases "p \<in> succs (hd w)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. p \<in> succs (hd w) \<Longrightarrow> ss ! p \<sqsubseteq>\<^bsub>r\<^esub> ssa ! p
 2. p \<notin> succs (hd w) \<Longrightarrow> ss ! p \<sqsubseteq>\<^bsub>r\<^esub> ssa ! p
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
p \<in> succs (hd w)

goal (2 subgoals):
 1. p \<in> succs (hd w) \<Longrightarrow> ss ! p \<sqsubseteq>\<^bsub>r\<^esub> ssa ! p
 2. p \<notin> succs (hd w) \<Longrightarrow> ss ! p \<sqsubseteq>\<^bsub>r\<^esub> ssa ! p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p \<in> succs (hd w)
[PROOF STEP]
show "ss!p \<sqsubseteq>\<^bsub>r\<^esub>  ssa!p"
[PROOF STATE]
proof (prove)
using this:
p \<in> succs (hd w)

goal (1 subgoal):
 1. ss ! p \<sqsubseteq>\<^bsub>r\<^esub> ssa ! p
[PROOF STEP]
using ss_lt_ssa_q
[PROOF STATE]
proof (prove)
using this:
p \<in> succs (hd w)
\<forall>(q, \<tau>)\<in>set (step (hd w) (ss ! hd w)). ss ! q \<sqsubseteq>\<^bsub>r\<^esub> ssa ! q

goal (1 subgoal):
 1. ss ! p \<sqsubseteq>\<^bsub>r\<^esub> ssa ! p
[PROOF STEP]
using fin_succ_hd_w
[PROOF STATE]
proof (prove)
using this:
p \<in> succs (hd w)
\<forall>(q, \<tau>)\<in>set (step (hd w) (ss ! hd w)). ss ! q \<sqsubseteq>\<^bsub>r\<^esub> ssa ! q
finite (succs (hd w))

goal (1 subgoal):
 1. ss ! p \<sqsubseteq>\<^bsub>r\<^esub> ssa ! p
[PROOF STEP]
by (auto simp add:step_def exec_def)
[PROOF STATE]
proof (state)
this:
ss ! p \<sqsubseteq>\<^bsub>r\<^esub> ssa ! p

goal (1 subgoal):
 1. p \<notin> succs (hd w) \<Longrightarrow> ss ! p \<sqsubseteq>\<^bsub>r\<^esub> ssa ! p
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. p \<notin> succs (hd w) \<Longrightarrow> ss ! p \<sqsubseteq>\<^bsub>r\<^esub> ssa ! p
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
p \<notin> succs (hd w)

goal (1 subgoal):
 1. p \<notin> succs (hd w) \<Longrightarrow> ss ! p \<sqsubseteq>\<^bsub>r\<^esub> ssa ! p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p \<notin> succs (hd w)
[PROOF STEP]
have "p \<notin> set (map fst ?qs)"
[PROOF STATE]
proof (prove)
using this:
p \<notin> succs (hd w)

goal (1 subgoal):
 1. p \<notin> set (map fst (step (hd w) (ss ! hd w)))
[PROOF STEP]
using fin_succ_hd_w
[PROOF STATE]
proof (prove)
using this:
p \<notin> succs (hd w)
finite (succs (hd w))

goal (1 subgoal):
 1. p \<notin> set (map fst (step (hd w) (ss ! hd w)))
[PROOF STEP]
by (auto simp add:step_def exec_def)
[PROOF STATE]
proof (state)
this:
p \<notin> set (map fst (step (hd w) (ss ! hd w)))

goal (1 subgoal):
 1. p \<notin> succs (hd w) \<Longrightarrow> ss ! p \<sqsubseteq>\<^bsub>r\<^esub> ssa ! p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p \<notin> set (map fst (step (hd w) (ss ! hd w)))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
p \<notin> set (map fst (step (hd w) (ss ! hd w)))

goal (1 subgoal):
 1. ss ! p \<sqsubseteq>\<^bsub>r\<^esub> ssa ! p
[PROOF STEP]
using exec2 \<open>p < length ss\<close>
[PROOF STATE]
proof (prove)
using this:
p \<notin> set (map fst (step (hd w) (ss ! hd w)))
\<lbrakk>?q \<notin> set (map fst (step (hd w) (ss ! hd w))); ?q < length ss\<rbrakk> \<Longrightarrow> ssa ! ?q = ss ! ?q
p < length ss

goal (1 subgoal):
 1. ss ! p \<sqsubseteq>\<^bsub>r\<^esub> ssa ! p
[PROOF STEP]
using ssa_p_inA ss_p_inA
[PROOF STATE]
proof (prove)
using this:
p \<notin> set (map fst (step (hd w) (ss ! hd w)))
\<lbrakk>?q \<notin> set (map fst (step (hd w) (ss ! hd w))); ?q < length ss\<rbrakk> \<Longrightarrow> ssa ! ?q = ss ! ?q
p < length ss
ssa ! p \<in> A
ss ! p \<in> A

goal (1 subgoal):
 1. ss ! p \<sqsubseteq>\<^bsub>r\<^esub> ssa ! p
[PROOF STEP]
by(auto simp add:step_def exec_def intro: Semilat.orderI[OF Semilat.intro, OF is_semi])
[PROOF STATE]
proof (state)
this:
ss ! p \<sqsubseteq>\<^bsub>r\<^esub> ssa ! p

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
ss ! p \<sqsubseteq>\<^bsub>r\<^esub> ssa ! p

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>p<length ss. ss ! p \<sqsubseteq>\<^bsub>r\<^esub> ssa ! p

goal (1 subgoal):
 1. \<lbrakk>wf_dom ss0 w0; w \<noteq> []; propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ssa, wa); wf_dom ss w; 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\<rbrakk> \<Longrightarrow> ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ssa \<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> ssa [\<sqsubseteq>\<^bsub>r\<^esub>] ts)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>p<length ss. ss ! p \<sqsubseteq>\<^bsub>r\<^esub> ssa ! p
[PROOF STEP]
have "\<forall>p<length ss0. ss ! p \<sqsubseteq>\<^bsub>r\<^esub> ssa ! p"
[PROOF STATE]
proof (prove)
using this:
\<forall>p<length ss. ss ! p \<sqsubseteq>\<^bsub>r\<^esub> ssa ! p

goal (1 subgoal):
 1. \<forall>p<length ss0. ss ! p \<sqsubseteq>\<^bsub>r\<^esub> ssa ! p
[PROOF STEP]
using len_ss0_ss
[PROOF STATE]
proof (prove)
using this:
\<forall>p<length ss. ss ! p \<sqsubseteq>\<^bsub>r\<^esub> ssa ! p
length ss0 = length ss

goal (1 subgoal):
 1. \<forall>p<length ss0. ss ! p \<sqsubseteq>\<^bsub>r\<^esub> ssa ! p
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>p<length ss0. ss ! p \<sqsubseteq>\<^bsub>r\<^esub> ssa ! p

goal (1 subgoal):
 1. \<lbrakk>wf_dom ss0 w0; w \<noteq> []; propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ssa, wa); wf_dom ss w; 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\<rbrakk> \<Longrightarrow> ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ssa \<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> ssa [\<sqsubseteq>\<^bsub>r\<^esub>] ts)
[PROOF STEP]
with lt1
[PROOF STATE]
proof (chain)
picking this:
\<forall>p<length ss0. ss0 ! p \<sqsubseteq>\<^bsub>r\<^esub> ss ! p
\<forall>p<length ss0. ss ! p \<sqsubseteq>\<^bsub>r\<^esub> ssa ! p
[PROOF STEP]
have "\<forall>p<length ss0. ss0!p \<sqsubseteq>\<^bsub>r\<^esub> ssa!p"
[PROOF STATE]
proof (prove)
using this:
\<forall>p<length ss0. ss0 ! p \<sqsubseteq>\<^bsub>r\<^esub> ss ! p
\<forall>p<length ss0. ss ! p \<sqsubseteq>\<^bsub>r\<^esub> ssa ! p

goal (1 subgoal):
 1. \<forall>p<length ss0. ss0 ! p \<sqsubseteq>\<^bsub>r\<^esub> ssa ! p
[PROOF STEP]
using ss0_nth_inA ssa_nth_inA  ss_nth_inA
[PROOF STATE]
proof (prove)
using this:
\<forall>p<length ss0. ss0 ! p \<sqsubseteq>\<^bsub>r\<^esub> ss ! p
\<forall>p<length ss0. ss ! p \<sqsubseteq>\<^bsub>r\<^esub> ssa ! p
\<forall>i<length ss0. ss0 ! i \<in> A
\<forall>i<length ssa. ssa ! i \<in> A
\<forall>i<length ss. ss ! i \<in> A

goal (1 subgoal):
 1. \<forall>p<length ss0. ss0 ! p \<sqsubseteq>\<^bsub>r\<^esub> ssa ! p
[PROOF STEP]
using len_ss0_ss len_ss0_ssa
[PROOF STATE]
proof (prove)
using this:
\<forall>p<length ss0. ss0 ! p \<sqsubseteq>\<^bsub>r\<^esub> ss ! p
\<forall>p<length ss0. ss ! p \<sqsubseteq>\<^bsub>r\<^esub> ssa ! p
\<forall>i<length ss0. ss0 ! i \<in> A
\<forall>i<length ssa. ssa ! i \<in> A
\<forall>i<length ss. ss ! i \<in> A
length ss0 = length ss
length ss0 = length ssa

goal (1 subgoal):
 1. \<forall>p<length ss0. ss0 ! p \<sqsubseteq>\<^bsub>r\<^esub> ssa ! p
[PROOF STEP]
by (auto intro: order_trans Semilat.orderI[OF Semilat.intro, OF is_semi])
[PROOF STATE]
proof (state)
this:
\<forall>p<length ss0. ss0 ! p \<sqsubseteq>\<^bsub>r\<^esub> ssa ! p

goal (1 subgoal):
 1. \<lbrakk>wf_dom ss0 w0; w \<noteq> []; propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ssa, wa); wf_dom ss w; 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\<rbrakk> \<Longrightarrow> ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ssa \<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> ssa [\<sqsubseteq>\<^bsub>r\<^esub>] ts)
[PROOF STEP]
with len_ss0_ssa
[PROOF STATE]
proof (chain)
picking this:
length ss0 = length ssa
\<forall>p<length ss0. ss0 ! p \<sqsubseteq>\<^bsub>r\<^esub> ssa ! p
[PROOF STEP]
have g1: "ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ssa"
[PROOF STATE]
proof (prove)
using this:
length ss0 = length ssa
\<forall>p<length ss0. ss0 ! p \<sqsubseteq>\<^bsub>r\<^esub> ssa ! p

goal (1 subgoal):
 1. ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ssa
[PROOF STEP]
by (auto simp only:Listn.le_def lesssub_def lesub_def intro:list_all2_all_nthI)
[PROOF STATE]
proof (state)
this:
ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ssa

goal (1 subgoal):
 1. \<lbrakk>wf_dom ss0 w0; w \<noteq> []; propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ssa, wa); wf_dom ss w; 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\<rbrakk> \<Longrightarrow> ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ssa \<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> ssa [\<sqsubseteq>\<^bsub>r\<^esub>] ts)
[PROOF STEP]
have "(\<forall>ts\<in>nlists n A. ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> (\<forall>p<n. stable r step ts p) \<longrightarrow> ssa [\<sqsubseteq>\<^bsub>r\<^esub>] ts)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<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> ssa [\<sqsubseteq>\<^bsub>r\<^esub>] ts
[PROOF STEP]
proof(intro strip)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ts. \<lbrakk>ts \<in> nlists n A; ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> (\<forall>p<n. Typing_Framework_1.stable r step ts p)\<rbrakk> \<Longrightarrow> ssa [\<sqsubseteq>\<^bsub>r\<^esub>] ts
[PROOF STEP]
fix ts
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ts. \<lbrakk>ts \<in> nlists n A; ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> (\<forall>p<n. Typing_Framework_1.stable r step ts p)\<rbrakk> \<Longrightarrow> ssa [\<sqsubseteq>\<^bsub>r\<^esub>] ts
[PROOF STEP]
assume ts_inA: "ts \<in> nlists n A" and ass: "ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> (\<forall>p<n. stable r step ts p)"
[PROOF STATE]
proof (state)
this:
ts \<in> nlists n A
ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> (\<forall>p<n. Typing_Framework_1.stable r step ts p)

goal (1 subgoal):
 1. \<And>ts. \<lbrakk>ts \<in> nlists n A; ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> (\<forall>p<n. Typing_Framework_1.stable r step ts p)\<rbrakk> \<Longrightarrow> ssa [\<sqsubseteq>\<^bsub>r\<^esub>] ts
[PROOF STEP]
let ?ts_hdw = "ts!(hd w)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ts. \<lbrakk>ts \<in> nlists n A; ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> (\<forall>p<n. Typing_Framework_1.stable r step ts p)\<rbrakk> \<Longrightarrow> ssa [\<sqsubseteq>\<^bsub>r\<^esub>] ts
[PROOF STEP]
from ts_inA sta ass
[PROOF STATE]
proof (chain)
picking this:
ts \<in> nlists n 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> ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts
ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> (\<forall>p<n. Typing_Framework_1.stable r step ts p)
[PROOF STEP]
have ss_ts: "ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts" and sta_ts: "(\<forall>p<n. stable r step ts p)"
[PROOF STATE]
proof (prove)
using this:
ts \<in> nlists n 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> ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts
ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> (\<forall>p<n. Typing_Framework_1.stable r step ts p)

goal (1 subgoal):
 1. ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts &&& \<forall>p<n. Typing_Framework_1.stable r step ts p
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts
\<forall>p<n. Typing_Framework_1.stable r step ts p

goal (1 subgoal):
 1. \<And>ts. \<lbrakk>ts \<in> nlists n A; ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> (\<forall>p<n. Typing_Framework_1.stable r step ts p)\<rbrakk> \<Longrightarrow> ssa [\<sqsubseteq>\<^bsub>r\<^esub>] ts
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts
\<forall>p<n. Typing_Framework_1.stable r step ts p
[PROOF STEP]
have len_ss_ts: "length ss = length ts" and
              ss_ts_hdw: "?ss_hdw \<sqsubseteq>\<^bsub>r\<^esub> ?ts_hdw "
[PROOF STATE]
proof (prove)
using this:
ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts
\<forall>p<n. Typing_Framework_1.stable r step ts p

goal (1 subgoal):
 1. length ss = length ts &&& ss ! hd w \<sqsubseteq>\<^bsub>r\<^esub> ts ! hd w
[PROOF STEP]
using le_listD len_ss hd_w_lt_n
[PROOF STATE]
proof (prove)
using this:
ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts
\<forall>p<n. Typing_Framework_1.stable r step ts p
\<lbrakk>?xs [\<sqsubseteq>\<^bsub>?r\<^esub>] ?ys; ?p < length ?xs\<rbrakk> \<Longrightarrow> ?xs ! ?p \<sqsubseteq>\<^bsub>?r\<^esub> ?ys ! ?p
length ss = n
hd w < n

goal (1 subgoal):
 1. length ss = length ts &&& ss ! hd w \<sqsubseteq>\<^bsub>r\<^esub> ts ! hd w
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length ss = length ts
ss ! hd w \<sqsubseteq>\<^bsub>r\<^esub> ts ! hd w

goal (1 subgoal):
 1. \<And>ts. \<lbrakk>ts \<in> nlists n A; ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> (\<forall>p<n. Typing_Framework_1.stable r step ts p)\<rbrakk> \<Longrightarrow> ssa [\<sqsubseteq>\<^bsub>r\<^esub>] ts
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length ss = length ts
ss ! hd w \<sqsubseteq>\<^bsub>r\<^esub> ts ! hd w
[PROOF STEP]
have "sorted (rev (?ts_hdw)) \<and> set ?ts_hdw \<subseteq> set ?ss_hdw \<or> ?ss_hdw =?ts_hdw "
[PROOF STATE]
proof (prove)
using this:
length ss = length ts
ss ! hd w \<sqsubseteq>\<^bsub>r\<^esub> ts ! hd w

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

goal (1 subgoal):
 1. \<And>ts. \<lbrakk>ts \<in> nlists n A; ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> (\<forall>p<n. Typing_Framework_1.stable r step ts p)\<rbrakk> \<Longrightarrow> ssa [\<sqsubseteq>\<^bsub>r\<^esub>] ts
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Sorted_Less.sorted (rev (ts ! hd w)) \<and> set (ts ! hd w) \<subseteq> set (ss ! hd w) \<or> ss ! hd w = ts ! hd w
[PROOF STEP]
have sorted_ts_hdw: "sorted (rev (?ts_hdw))"
          and ts_ss_subset: "set ?ts_hdw \<subseteq> set ?ss_hdw"
[PROOF STATE]
proof (prove)
using this:
Sorted_Less.sorted (rev (ts ! hd w)) \<and> set (ts ! hd w) \<subseteq> set (ss ! hd w) \<or> ss ! hd w = ts ! hd w

goal (1 subgoal):
 1. Sorted_Less.sorted (rev (ts ! hd w)) &&& set (ts ! hd w) \<subseteq> set (ss ! hd w)
[PROOF STEP]
using sorted_ss_hdw
[PROOF STATE]
proof (prove)
using this:
Sorted_Less.sorted (rev (ts ! hd w)) \<and> set (ts ! hd w) \<subseteq> set (ss ! hd w) \<or> ss ! hd w = ts ! hd w
Sorted_Less.sorted (rev (ss ! hd w))

goal (1 subgoal):
 1. Sorted_Less.sorted (rev (ts ! hd w)) &&& set (ts ! hd w) \<subseteq> set (ss ! hd w)
[PROOF STEP]
by (auto simp add:r_def lesssub_def lesub_def  nodes_le_def)
[PROOF STATE]
proof (state)
this:
Sorted_Less.sorted (rev (ts ! hd w))
set (ts ! hd w) \<subseteq> set (ss ! hd w)

goal (1 subgoal):
 1. \<And>ts. \<lbrakk>ts \<in> nlists n A; ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> (\<forall>p<n. Typing_Framework_1.stable r step ts p)\<rbrakk> \<Longrightarrow> ssa [\<sqsubseteq>\<^bsub>r\<^esub>] ts
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Sorted_Less.sorted (rev (ts ! hd w))
set (ts ! hd w) \<subseteq> set (ss ! hd w)
[PROOF STEP]
have "\<forall>x\<in> set ?ts_hdw. x < hd w"
[PROOF STATE]
proof (prove)
using this:
Sorted_Less.sorted (rev (ts ! hd w))
set (ts ! hd w) \<subseteq> set (ss ! hd w)

goal (1 subgoal):
 1. \<forall>x\<in>set (ts ! hd w). x < hd w
[PROOF STEP]
using ss_lt_hd_w
[PROOF STATE]
proof (prove)
using this:
Sorted_Less.sorted (rev (ts ! hd w))
set (ts ! hd w) \<subseteq> set (ss ! hd w)
\<forall>x\<in>set (ss ! hd w). x < hd w

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

goal (1 subgoal):
 1. \<And>ts. \<lbrakk>ts \<in> nlists n A; ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> (\<forall>p<n. Typing_Framework_1.stable r step ts p)\<rbrakk> \<Longrightarrow> ssa [\<sqsubseteq>\<^bsub>r\<^esub>] ts
[PROOF STEP]
with sorted_ts_hdw
[PROOF STATE]
proof (chain)
picking this:
Sorted_Less.sorted (rev (ts ! hd w))
\<forall>x\<in>set (ts ! hd w). x < hd w
[PROOF STEP]
have sorted_hd_w_ts: "sorted (rev (hd w # ?ts_hdw))"
[PROOF STATE]
proof (prove)
using this:
Sorted_Less.sorted (rev (ts ! hd w))
\<forall>x\<in>set (ts ! hd w). x < hd w

goal (1 subgoal):
 1. Sorted_Less.sorted (rev (hd w # ts ! hd w))
[PROOF STEP]
by (auto simp add:sorted_wrt_append)
[PROOF STATE]
proof (state)
this:
Sorted_Less.sorted (rev (hd w # ts ! hd w))

goal (1 subgoal):
 1. \<And>ts. \<lbrakk>ts \<in> nlists n A; ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> (\<forall>p<n. Typing_Framework_1.stable r step ts p)\<rbrakk> \<Longrightarrow> ssa [\<sqsubseteq>\<^bsub>r\<^esub>] ts
[PROOF STEP]
with sorted_hd_w_ss ts_ss_subset
[PROOF STATE]
proof (chain)
picking this:
Sorted_Less.sorted (rev (hd w # ss ! hd w))
set (ts ! hd w) \<subseteq> set (ss ! hd w)
Sorted_Less.sorted (rev (hd w # ts ! hd w))
[PROOF STEP]
have "(hd w # ?ss_hdw) \<sqsubseteq>\<^bsub>r\<^esub> (hd w # ?ts_hdw)"
[PROOF STATE]
proof (prove)
using this:
Sorted_Less.sorted (rev (hd w # ss ! hd w))
set (ts ! hd w) \<subseteq> set (ss ! hd w)
Sorted_Less.sorted (rev (hd w # ts ! hd w))

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

goal (1 subgoal):
 1. \<And>ts. \<lbrakk>ts \<in> nlists n A; ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> (\<forall>p<n. Typing_Framework_1.stable r step ts p)\<rbrakk> \<Longrightarrow> ssa [\<sqsubseteq>\<^bsub>r\<^esub>] ts
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
hd w # ss ! hd w \<sqsubseteq>\<^bsub>r\<^esub> hd w # ts ! hd w
[PROOF STEP]
have transf_ss_ts: "transf (hd w) ?ss_hdw \<sqsubseteq>\<^bsub>r\<^esub> transf (hd w) ?ts_hdw"
[PROOF STATE]
proof (prove)
using this:
hd w # ss ! hd w \<sqsubseteq>\<^bsub>r\<^esub> hd w # ts ! hd w

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

goal (1 subgoal):
 1. \<And>ts. \<lbrakk>ts \<in> nlists n A; ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> (\<forall>p<n. Typing_Framework_1.stable r step ts p)\<rbrakk> \<Longrightarrow> ssa [\<sqsubseteq>\<^bsub>r\<^esub>] ts
[PROOF STEP]
from sta_ts hd_w_lt_n
[PROOF STATE]
proof (chain)
picking this:
\<forall>p<n. Typing_Framework_1.stable r step ts p
hd w < n
[PROOF STEP]
have sta_ts_hdw: "stable r step ts (hd w)"
[PROOF STATE]
proof (prove)
using this:
\<forall>p<n. Typing_Framework_1.stable r step ts p
hd w < n

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

goal (1 subgoal):
 1. \<And>ts. \<lbrakk>ts \<in> nlists n A; ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> (\<forall>p<n. Typing_Framework_1.stable r step ts p)\<rbrakk> \<Longrightarrow> ssa [\<sqsubseteq>\<^bsub>r\<^esub>] ts
[PROOF STEP]
from ss_hdw_nodes ts_ss_subset
[PROOF STATE]
proof (chain)
picking this:
set (ss ! hd w) \<subseteq> set nodes
set (ts ! hd w) \<subseteq> set (ss ! hd w)
[PROOF STEP]
have "set ?ts_hdw \<subseteq> set nodes"
[PROOF STATE]
proof (prove)
using this:
set (ss ! hd w) \<subseteq> set nodes
set (ts ! hd w) \<subseteq> set (ss ! hd w)

goal (1 subgoal):
 1. set (ts ! hd w) \<subseteq> set nodes
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (ts ! hd w) \<subseteq> set nodes

goal (1 subgoal):
 1. \<And>ts. \<lbrakk>ts \<in> nlists n A; ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> (\<forall>p<n. Typing_Framework_1.stable r step ts p)\<rbrakk> \<Longrightarrow> ssa [\<sqsubseteq>\<^bsub>r\<^esub>] ts
[PROOF STEP]
with hd_w_lt_n
[PROOF STATE]
proof (chain)
picking this:
hd w < n
set (ts ! hd w) \<subseteq> set nodes
[PROOF STEP]
have hdw_ts_subset_nodes: "set (hd w # ?ts_hdw) \<subseteq> set nodes"
[PROOF STATE]
proof (prove)
using this:
hd w < n
set (ts ! hd w) \<subseteq> set nodes

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

goal (1 subgoal):
 1. set (hd w # ts ! hd w) \<subseteq> set nodes
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (hd w # ts ! hd w) \<subseteq> set nodes

goal (1 subgoal):
 1. \<And>ts. \<lbrakk>ts \<in> nlists n A; ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> (\<forall>p<n. Typing_Framework_1.stable r step ts p)\<rbrakk> \<Longrightarrow> ssa [\<sqsubseteq>\<^bsub>r\<^esub>] ts
[PROOF STEP]
with sorted_hd_w_ts
[PROOF STATE]
proof (chain)
picking this:
Sorted_Less.sorted (rev (hd w # ts ! hd w))
set (hd w # ts ! hd w) \<subseteq> set nodes
[PROOF STEP]
have "(hd w # ?ts_hdw) \<in> ( (rev \<circ> sorted_list_of_set) ` (Pow (set nodes)))"
[PROOF STATE]
proof (prove)
using this:
Sorted_Less.sorted (rev (hd w # ts ! hd w))
set (hd w # ts ! hd w) \<subseteq> set nodes

goal (1 subgoal):
 1. hd w # ts ! hd w \<in> (rev \<circ> sorted_list_of_set) ` Pow (set nodes)
[PROOF STEP]
by (fastforce intro: subset_nodes_inpow)
[PROOF STATE]
proof (state)
this:
hd w # ts ! hd w \<in> (rev \<circ> sorted_list_of_set) ` Pow (set nodes)

goal (1 subgoal):
 1. \<And>ts. \<lbrakk>ts \<in> nlists n A; ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> (\<forall>p<n. Typing_Framework_1.stable r step ts p)\<rbrakk> \<Longrightarrow> ssa [\<sqsubseteq>\<^bsub>r\<^esub>] ts
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
hd w # ts ! hd w \<in> (rev \<circ> sorted_list_of_set) ` Pow (set nodes)
[PROOF STEP]
have transf_ts_inA: "(hd w #?ts_hdw) \<in> A"
[PROOF STATE]
proof (prove)
using this:
hd w # ts ! hd w \<in> (rev \<circ> sorted_list_of_set) ` Pow (set nodes)

goal (1 subgoal):
 1. hd w # ts ! hd w \<in> A
[PROOF STEP]
by (simp add:A_def)
[PROOF STATE]
proof (state)
this:
hd w # ts ! hd w \<in> A

goal (1 subgoal):
 1. \<And>ts. \<lbrakk>ts \<in> nlists n A; ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> (\<forall>p<n. Typing_Framework_1.stable r step ts p)\<rbrakk> \<Longrightarrow> ssa [\<sqsubseteq>\<^bsub>r\<^esub>] ts
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
hd w # ts ! hd w \<in> A
[PROOF STEP]
have sorted_hdw_ts_hdw:  "sorted (rev (hd w # ?ts_hdw))"
[PROOF STATE]
proof (prove)
using this:
hd w # ts ! hd w \<in> A

goal (1 subgoal):
 1. Sorted_Less.sorted (rev (hd w # ts ! hd w))
[PROOF STEP]
by (rule inA_is_sorted)
[PROOF STATE]
proof (state)
this:
Sorted_Less.sorted (rev (hd w # ts ! hd w))

goal (1 subgoal):
 1. \<And>ts. \<lbrakk>ts \<in> nlists n A; ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> (\<forall>p<n. Typing_Framework_1.stable r step ts p)\<rbrakk> \<Longrightarrow> ssa [\<sqsubseteq>\<^bsub>r\<^esub>] ts
[PROOF STEP]
have "\<forall>p<length ssa. ssa!p \<sqsubseteq>\<^bsub>r\<^esub> ts!p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>p<length ssa. ssa ! p \<sqsubseteq>\<^bsub>r\<^esub> ts ! p
[PROOF STEP]
proof(intro strip)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p. p < length ssa \<Longrightarrow> ssa ! p \<sqsubseteq>\<^bsub>r\<^esub> ts ! p
[PROOF STEP]
fix p
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p. p < length ssa \<Longrightarrow> ssa ! p \<sqsubseteq>\<^bsub>r\<^esub> ts ! p
[PROOF STEP]
assume p_lt_len_ssa: "p < length ssa"
[PROOF STATE]
proof (state)
this:
p < length ssa

goal (1 subgoal):
 1. \<And>p. p < length ssa \<Longrightarrow> ssa ! p \<sqsubseteq>\<^bsub>r\<^esub> ts ! p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p < length ssa
[PROOF STEP]
have "p < length ss" and "p < n"
[PROOF STATE]
proof (prove)
using this:
p < length ssa

goal (1 subgoal):
 1. p < length ss &&& p < n
[PROOF STEP]
using len_ssa len_ss
[PROOF STATE]
proof (prove)
using this:
p < length ssa
length ssa = n
length ss = n

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

goal (1 subgoal):
 1. \<And>p. p < length ssa \<Longrightarrow> ssa ! p \<sqsubseteq>\<^bsub>r\<^esub> ts ! p
[PROOF STEP]
with ss_ts
[PROOF STATE]
proof (chain)
picking this:
ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts
p < length ss
p < n
[PROOF STEP]
have ss_ts_p: "ss!p \<sqsubseteq>\<^bsub>r\<^esub> ts!p "
[PROOF STATE]
proof (prove)
using this:
ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts
p < length ss
p < n

goal (1 subgoal):
 1. ss ! p \<sqsubseteq>\<^bsub>r\<^esub> ts ! p
[PROOF STEP]
using le_listD
[PROOF STATE]
proof (prove)
using this:
ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts
p < length ss
p < n
\<lbrakk>?xs [\<sqsubseteq>\<^bsub>?r\<^esub>] ?ys; ?p < length ?xs\<rbrakk> \<Longrightarrow> ?xs ! ?p \<sqsubseteq>\<^bsub>?r\<^esub> ?ys ! ?p

goal (1 subgoal):
 1. ss ! p \<sqsubseteq>\<^bsub>r\<^esub> ts ! p
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ss ! p \<sqsubseteq>\<^bsub>r\<^esub> ts ! p

goal (1 subgoal):
 1. \<And>p. p < length ssa \<Longrightarrow> ssa ! p \<sqsubseteq>\<^bsub>r\<^esub> ts ! p
[PROOF STEP]
show "ssa ! p \<sqsubseteq>\<^bsub>r\<^esub> ts ! p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ssa ! p \<sqsubseteq>\<^bsub>r\<^esub> ts ! p
[PROOF STEP]
proof(cases "p \<in> succs (hd w)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. p \<in> succs (hd w) \<Longrightarrow> ssa ! p \<sqsubseteq>\<^bsub>r\<^esub> ts ! p
 2. p \<notin> succs (hd w) \<Longrightarrow> ssa ! p \<sqsubseteq>\<^bsub>r\<^esub> ts ! p
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
p \<in> succs (hd w)

goal (2 subgoals):
 1. p \<in> succs (hd w) \<Longrightarrow> ssa ! p \<sqsubseteq>\<^bsub>r\<^esub> ts ! p
 2. p \<notin> succs (hd w) \<Longrightarrow> ssa ! p \<sqsubseteq>\<^bsub>r\<^esub> ts ! p
[PROOF STEP]
note p_in_succs_hdw = this
[PROOF STATE]
proof (state)
this:
p \<in> succs (hd w)

goal (2 subgoals):
 1. p \<in> succs (hd w) \<Longrightarrow> ssa ! p \<sqsubseteq>\<^bsub>r\<^esub> ts ! p
 2. p \<notin> succs (hd w) \<Longrightarrow> ssa ! p \<sqsubseteq>\<^bsub>r\<^esub> ts ! p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p \<in> succs (hd w)
[PROOF STEP]
have "ss!p \<sqsubseteq>\<^bsub>r\<^esub> ssa!p"
[PROOF STATE]
proof (prove)
using this:
p \<in> succs (hd w)

goal (1 subgoal):
 1. ss ! p \<sqsubseteq>\<^bsub>r\<^esub> ssa ! p
[PROOF STEP]
using ss_lt_ssa_q
[PROOF STATE]
proof (prove)
using this:
p \<in> succs (hd w)
\<forall>(q, \<tau>)\<in>set (step (hd w) (ss ! hd w)). ss ! q \<sqsubseteq>\<^bsub>r\<^esub> ssa ! q

goal (1 subgoal):
 1. ss ! p \<sqsubseteq>\<^bsub>r\<^esub> ssa ! p
[PROOF STEP]
using fin_succ_hd_w
[PROOF STATE]
proof (prove)
using this:
p \<in> succs (hd w)
\<forall>(q, \<tau>)\<in>set (step (hd w) (ss ! hd w)). ss ! q \<sqsubseteq>\<^bsub>r\<^esub> ssa ! q
finite (succs (hd w))

goal (1 subgoal):
 1. ss ! p \<sqsubseteq>\<^bsub>r\<^esub> ssa ! p
[PROOF STEP]
by (auto simp add:step_def exec_def)
[PROOF STATE]
proof (state)
this:
ss ! p \<sqsubseteq>\<^bsub>r\<^esub> ssa ! p

goal (2 subgoals):
 1. p \<in> succs (hd w) \<Longrightarrow> ssa ! p \<sqsubseteq>\<^bsub>r\<^esub> ts ! p
 2. p \<notin> succs (hd w) \<Longrightarrow> ssa ! p \<sqsubseteq>\<^bsub>r\<^esub> ts ! p
[PROOF STEP]
from p_in_succs_hdw
[PROOF STATE]
proof (chain)
picking this:
p \<in> succs (hd w)
[PROOF STEP]
have ssa_p: "ssa!p = transf (hd w) (ss!hd w) \<squnion>\<^bsub>f\<^esub>ss!p"
[PROOF STATE]
proof (prove)
using this:
p \<in> succs (hd w)

goal (1 subgoal):
 1. ssa ! p = transf (hd w) (ss ! hd w) \<squnion>\<^bsub>f\<^esub> ss ! p
[PROOF STEP]
using propa_ss fin_succ_hd_w
[PROOF STATE]
proof (prove)
using this:
p \<in> succs (hd w)
\<forall>(q, \<tau>)\<in>set (step (hd w) (ss ! hd w)). ssa ! q = \<tau> \<squnion>\<^bsub>f\<^esub> ss ! q
finite (succs (hd w))

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

goal (2 subgoals):
 1. p \<in> succs (hd w) \<Longrightarrow> ssa ! p \<sqsubseteq>\<^bsub>r\<^esub> ts ! p
 2. p \<notin> succs (hd w) \<Longrightarrow> ssa ! p \<sqsubseteq>\<^bsub>r\<^esub> ts ! p
[PROOF STEP]
from sta_ts_hdw
[PROOF STATE]
proof (chain)
picking this:
Typing_Framework_1.stable r step ts (hd w)
[PROOF STEP]
have transf_hdw_ts_hdw: "transf (hd w) (ts!hd w) \<sqsubseteq>\<^bsub>r\<^esub> ts!p"
[PROOF STATE]
proof (prove)
using this:
Typing_Framework_1.stable r step ts (hd w)

goal (1 subgoal):
 1. transf (hd w) (ts ! hd w) \<sqsubseteq>\<^bsub>r\<^esub> ts ! p
[PROOF STEP]
using p_in_succs_hdw fin_succ_hd_w
[PROOF STATE]
proof (prove)
using this:
Typing_Framework_1.stable r step ts (hd w)
p \<in> succs (hd w)
finite (succs (hd w))

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

goal (2 subgoals):
 1. p \<in> succs (hd w) \<Longrightarrow> ssa ! p \<sqsubseteq>\<^bsub>r\<^esub> ts ! p
 2. p \<notin> succs (hd w) \<Longrightarrow> ssa ! p \<sqsubseteq>\<^bsub>r\<^esub> ts ! p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
transf (hd w) (ts ! hd w) \<sqsubseteq>\<^bsub>r\<^esub> ts ! p
[PROOF STEP]
have ts_p_subset: "(hd w # ?ts_hdw) \<sqsubseteq>\<^bsub>r\<^esub> ts!p"
[PROOF STATE]
proof (prove)
using this:
transf (hd w) (ts ! hd w) \<sqsubseteq>\<^bsub>r\<^esub> ts ! p

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

goal (2 subgoals):
 1. p \<in> succs (hd w) \<Longrightarrow> ssa ! p \<sqsubseteq>\<^bsub>r\<^esub> ts ! p
 2. p \<notin> succs (hd w) \<Longrightarrow> ssa ! p \<sqsubseteq>\<^bsub>r\<^esub> ts ! p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
hd w # ts ! hd w \<sqsubseteq>\<^bsub>r\<^esub> ts ! p
[PROOF STEP]
have "(sorted (rev (ts!p)) \<and> set (ts!p)\<subseteq> set (hd w # ?ts_hdw)\<and> sorted (rev (hd w # ?ts_hdw))) \<or>
                   hd w # ?ts_hdw = ts!p"
[PROOF STATE]
proof (prove)
using this:
hd w # ts ! hd w \<sqsubseteq>\<^bsub>r\<^esub> ts ! p

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

goal (2 subgoals):
 1. p \<in> succs (hd w) \<Longrightarrow> ssa ! p \<sqsubseteq>\<^bsub>r\<^esub> ts ! p
 2. p \<notin> succs (hd w) \<Longrightarrow> ssa ! p \<sqsubseteq>\<^bsub>r\<^esub> ts ! p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Sorted_Less.sorted (rev (ts ! p)) \<and> set (ts ! p) \<subseteq> set (hd w # ts ! hd w) \<and> Sorted_Less.sorted (rev (hd w # ts ! hd w)) \<or> hd w # ts ! hd w = ts ! p
[PROOF STEP]
have "sorted (rev (ts!p)) \<and> set (ts!p)\<subseteq> set (hd w # ?ts_hdw)"
[PROOF STATE]
proof (prove)
using this:
Sorted_Less.sorted (rev (ts ! p)) \<and> set (ts ! p) \<subseteq> set (hd w # ts ! hd w) \<and> Sorted_Less.sorted (rev (hd w # ts ! hd w)) \<or> hd w # ts ! hd w = ts ! p

goal (1 subgoal):
 1. Sorted_Less.sorted (rev (ts ! p)) \<and> set (ts ! p) \<subseteq> set (hd w # ts ! hd w)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Sorted_Less.sorted (rev (ts ! p)) \<and> set (ts ! p) \<subseteq> set (hd w # ts ! hd w) \<and> Sorted_Less.sorted (rev (hd w # ts ! hd w)) \<Longrightarrow> Sorted_Less.sorted (rev (ts ! p)) \<and> set (ts ! p) \<subseteq> set (hd w # ts ! hd w)
 2. hd w # ts ! hd w = ts ! p \<Longrightarrow> Sorted_Less.sorted (rev (ts ! p)) \<and> set (ts ! p) \<subseteq> set (hd w # ts ! hd w)
[PROOF STEP]
assume "sorted (rev (ts ! p)) \<and> set (ts ! p) \<subseteq> set (hd w # ts ! hd w) \<and> sorted (rev (hd w # ts ! hd w))"
[PROOF STATE]
proof (state)
this:
Sorted_Less.sorted (rev (ts ! p)) \<and> set (ts ! p) \<subseteq> set (hd w # ts ! hd w) \<and> Sorted_Less.sorted (rev (hd w # ts ! hd w))

goal (2 subgoals):
 1. Sorted_Less.sorted (rev (ts ! p)) \<and> set (ts ! p) \<subseteq> set (hd w # ts ! hd w) \<and> Sorted_Less.sorted (rev (hd w # ts ! hd w)) \<Longrightarrow> Sorted_Less.sorted (rev (ts ! p)) \<and> set (ts ! p) \<subseteq> set (hd w # ts ! hd w)
 2. hd w # ts ! hd w = ts ! p \<Longrightarrow> Sorted_Less.sorted (rev (ts ! p)) \<and> set (ts ! p) \<subseteq> set (hd w # ts ! hd w)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Sorted_Less.sorted (rev (ts ! p)) \<and> set (ts ! p) \<subseteq> set (hd w # ts ! hd w) \<and> Sorted_Less.sorted (rev (hd w # ts ! hd w))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Sorted_Less.sorted (rev (ts ! p)) \<and> set (ts ! p) \<subseteq> set (hd w # ts ! hd w) \<and> Sorted_Less.sorted (rev (hd w # ts ! hd w))

goal (1 subgoal):
 1. Sorted_Less.sorted (rev (ts ! p)) \<and> set (ts ! p) \<subseteq> set (hd w # ts ! hd w)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Sorted_Less.sorted (rev (ts ! p)) \<and> set (ts ! p) \<subseteq> set (hd w # ts ! hd w)

goal (1 subgoal):
 1. hd w # ts ! hd w = ts ! p \<Longrightarrow> Sorted_Less.sorted (rev (ts ! p)) \<and> set (ts ! p) \<subseteq> set (hd w # ts ! hd w)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. hd w # ts ! hd w = ts ! p \<Longrightarrow> Sorted_Less.sorted (rev (ts ! p)) \<and> set (ts ! p) \<subseteq> set (hd w # ts ! hd w)
[PROOF STEP]
assume " hd w # ts ! hd w = ts ! p"
[PROOF STATE]
proof (state)
this:
hd w # ts ! hd w = ts ! p

goal (1 subgoal):
 1. hd w # ts ! hd w = ts ! p \<Longrightarrow> Sorted_Less.sorted (rev (ts ! p)) \<and> set (ts ! p) \<subseteq> set (hd w # ts ! hd w)
[PROOF STEP]
with sorted_hdw_ts_hdw
[PROOF STATE]
proof (chain)
picking this:
Sorted_Less.sorted (rev (hd w # ts ! hd w))
hd w # ts ! hd w = ts ! p
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Sorted_Less.sorted (rev (hd w # ts ! hd w))
hd w # ts ! hd w = ts ! p

goal (1 subgoal):
 1. Sorted_Less.sorted (rev (ts ! p)) \<and> set (ts ! p) \<subseteq> set (hd w # ts ! hd w)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Sorted_Less.sorted (rev (ts ! p)) \<and> set (ts ! p) \<subseteq> set (hd w # ts ! hd w)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Sorted_Less.sorted (rev (ts ! p)) \<and> set (ts ! p) \<subseteq> set (hd w # ts ! hd w)

goal (2 subgoals):
 1. p \<in> succs (hd w) \<Longrightarrow> ssa ! p \<sqsubseteq>\<^bsub>r\<^esub> ts ! p
 2. p \<notin> succs (hd w) \<Longrightarrow> ssa ! p \<sqsubseteq>\<^bsub>r\<^esub> ts ! p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Sorted_Less.sorted (rev (ts ! p)) \<and> set (ts ! p) \<subseteq> set (hd w # ts ! hd w)
[PROOF STEP]
have sorted_ts_p: "sorted (rev (ts!p))"
              and ts_as_subset: "set (ts!p)\<subseteq> set (hd w # ?ts_hdw)"
[PROOF STATE]
proof (prove)
using this:
Sorted_Less.sorted (rev (ts ! p)) \<and> set (ts ! p) \<subseteq> set (hd w # ts ! hd w)

goal (1 subgoal):
 1. Sorted_Less.sorted (rev (ts ! p)) &&& set (ts ! p) \<subseteq> set (hd w # ts ! hd w)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Sorted_Less.sorted (rev (ts ! p))
set (ts ! p) \<subseteq> set (hd w # ts ! hd w)

goal (2 subgoals):
 1. p \<in> succs (hd w) \<Longrightarrow> ssa ! p \<sqsubseteq>\<^bsub>r\<^esub> ts ! p
 2. p \<notin> succs (hd w) \<Longrightarrow> ssa ! p \<sqsubseteq>\<^bsub>r\<^esub> ts ! p
[PROOF STEP]
with hdw_ts_subset_nodes
[PROOF STATE]
proof (chain)
picking this:
set (hd w # ts ! hd w) \<subseteq> set nodes
Sorted_Less.sorted (rev (ts ! p))
set (ts ! p) \<subseteq> set (hd w # ts ! hd w)
[PROOF STEP]
have "set (ts!p) \<subseteq> set nodes"
[PROOF STATE]
proof (prove)
using this:
set (hd w # ts ! hd w) \<subseteq> set nodes
Sorted_Less.sorted (rev (ts ! p))
set (ts ! p) \<subseteq> set (hd w # ts ! hd w)

goal (1 subgoal):
 1. set (ts ! p) \<subseteq> set nodes
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (ts ! p) \<subseteq> set nodes

goal (2 subgoals):
 1. p \<in> succs (hd w) \<Longrightarrow> ssa ! p \<sqsubseteq>\<^bsub>r\<^esub> ts ! p
 2. p \<notin> succs (hd w) \<Longrightarrow> ssa ! p \<sqsubseteq>\<^bsub>r\<^esub> ts ! p
[PROOF STEP]
with sorted_ts_p
[PROOF STATE]
proof (chain)
picking this:
Sorted_Less.sorted (rev (ts ! p))
set (ts ! p) \<subseteq> set nodes
[PROOF STEP]
have "(ts!p) \<in> ( (rev \<circ> sorted_list_of_set) ` (Pow (set nodes)))"
[PROOF STATE]
proof (prove)
using this:
Sorted_Less.sorted (rev (ts ! p))
set (ts ! p) \<subseteq> set nodes

goal (1 subgoal):
 1. ts ! p \<in> (rev \<circ> sorted_list_of_set) ` Pow (set nodes)
[PROOF STEP]
by (fastforce intro: subset_nodes_inpow)
[PROOF STATE]
proof (state)
this:
ts ! p \<in> (rev \<circ> sorted_list_of_set) ` Pow (set nodes)

goal (2 subgoals):
 1. p \<in> succs (hd w) \<Longrightarrow> ssa ! p \<sqsubseteq>\<^bsub>r\<^esub> ts ! p
 2. p \<notin> succs (hd w) \<Longrightarrow> ssa ! p \<sqsubseteq>\<^bsub>r\<^esub> ts ! p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ts ! p \<in> (rev \<circ> sorted_list_of_set) ` Pow (set nodes)
[PROOF STEP]
have ts_p_inA: "ts!p \<in> A"
[PROOF STATE]
proof (prove)
using this:
ts ! p \<in> (rev \<circ> sorted_list_of_set) ` Pow (set nodes)

goal (1 subgoal):
 1. ts ! p \<in> A
[PROOF STEP]
by (simp add:A_def)
[PROOF STATE]
proof (state)
this:
ts ! p \<in> A

goal (2 subgoals):
 1. p \<in> succs (hd w) \<Longrightarrow> ssa ! p \<sqsubseteq>\<^bsub>r\<^esub> ts ! p
 2. p \<notin> succs (hd w) \<Longrightarrow> ssa ! p \<sqsubseteq>\<^bsub>r\<^esub> ts ! p
[PROOF STEP]
from sorted_hdw_ts_hdw
[PROOF STATE]
proof (chain)
picking this:
Sorted_Less.sorted (rev (hd w # ts ! hd w))
[PROOF STEP]
have "\<forall>x\<in> set ?ts_hdw. x < hd w"
[PROOF STATE]
proof (prove)
using this:
Sorted_Less.sorted (rev (hd w # ts ! hd w))

goal (1 subgoal):
 1. \<forall>x\<in>set (ts ! hd w). x < hd w
[PROOF STEP]
by (auto simp add:sorted_wrt_append)
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>set (ts ! hd w). x < hd w

goal (2 subgoals):
 1. p \<in> succs (hd w) \<Longrightarrow> ssa ! p \<sqsubseteq>\<^bsub>r\<^esub> ts ! p
 2. p \<notin> succs (hd w) \<Longrightarrow> ssa ! p \<sqsubseteq>\<^bsub>r\<^esub> ts ! p
[PROOF STEP]
with \<open>hd w < n\<close>
[PROOF STATE]
proof (chain)
picking this:
hd w < n
\<forall>x\<in>set (ts ! hd w). x < hd w
[PROOF STEP]
have "\<forall>x\<in> set ?ts_hdw. x < n"
[PROOF STATE]
proof (prove)
using this:
hd w < n
\<forall>x\<in>set (ts ! hd w). x < hd w

goal (1 subgoal):
 1. \<forall>x\<in>set (ts ! hd w). x < n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>set (ts ! hd w). x < n

goal (2 subgoals):
 1. p \<in> succs (hd w) \<Longrightarrow> ssa ! p \<sqsubseteq>\<^bsub>r\<^esub> ts ! p
 2. p \<notin> succs (hd w) \<Longrightarrow> ssa ! p \<sqsubseteq>\<^bsub>r\<^esub> ts ! p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>set (ts ! hd w). x < n
[PROOF STEP]
have "set(hd w # ?ts_hdw) \<subseteq> set nodes"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>set (ts ! hd w). x < n

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

goal (1 subgoal):
 1. set (hd w # ts ! hd w) \<subseteq> set nodes
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (hd w # ts ! hd w) \<subseteq> set nodes

goal (2 subgoals):
 1. p \<in> succs (hd w) \<Longrightarrow> ssa ! p \<sqsubseteq>\<^bsub>r\<^esub> ts ! p
 2. p \<notin> succs (hd w) \<Longrightarrow> ssa ! p \<sqsubseteq>\<^bsub>r\<^esub> ts ! p
[PROOF STEP]
with sorted_hdw_ts_hdw
[PROOF STATE]
proof (chain)
picking this:
Sorted_Less.sorted (rev (hd w # ts ! hd w))
set (hd w # ts ! hd w) \<subseteq> set nodes
[PROOF STEP]
have "hd w # ?ts_hdw  \<in> ( (rev \<circ> sorted_list_of_set) ` (Pow (set nodes)))"
[PROOF STATE]
proof (prove)
using this:
Sorted_Less.sorted (rev (hd w # ts ! hd w))
set (hd w # ts ! hd w) \<subseteq> set nodes

goal (1 subgoal):
 1. hd w # ts ! hd w \<in> (rev \<circ> sorted_list_of_set) ` Pow (set nodes)
[PROOF STEP]
by (fastforce intro: subset_nodes_inpow)
[PROOF STATE]
proof (state)
this:
hd w # ts ! hd w \<in> (rev \<circ> sorted_list_of_set) ` Pow (set nodes)

goal (2 subgoals):
 1. p \<in> succs (hd w) \<Longrightarrow> ssa ! p \<sqsubseteq>\<^bsub>r\<^esub> ts ! p
 2. p \<notin> succs (hd w) \<Longrightarrow> ssa ! p \<sqsubseteq>\<^bsub>r\<^esub> ts ! p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
hd w # ts ! hd w \<in> (rev \<circ> sorted_list_of_set) ` Pow (set nodes)
[PROOF STEP]
have "(hd w # ?ts_hdw) \<in> A"
[PROOF STATE]
proof (prove)
using this:
hd w # ts ! hd w \<in> (rev \<circ> sorted_list_of_set) ` Pow (set nodes)

goal (1 subgoal):
 1. hd w # ts ! hd w \<in> A
[PROOF STEP]
by (auto simp add:A_def)
[PROOF STATE]
proof (state)
this:
hd w # ts ! hd w \<in> A

goal (2 subgoals):
 1. p \<in> succs (hd w) \<Longrightarrow> ssa ! p \<sqsubseteq>\<^bsub>r\<^esub> ts ! p
 2. p \<notin> succs (hd w) \<Longrightarrow> ssa ! p \<sqsubseteq>\<^bsub>r\<^esub> ts ! p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
hd w # ts ! hd w \<in> A
[PROOF STEP]
have trans_hdw_ts_inA: "transf (hd w) (ts!hd w) \<in> A"
[PROOF STATE]
proof (prove)
using this:
hd w # ts ! hd w \<in> A

goal (1 subgoal):
 1. transf (hd w) (ts ! hd w) \<in> A
[PROOF STEP]
by (auto simp add:transf_def)
[PROOF STATE]
proof (state)
this:
transf (hd w) (ts ! hd w) \<in> A

goal (2 subgoals):
 1. p \<in> succs (hd w) \<Longrightarrow> ssa ! p \<sqsubseteq>\<^bsub>r\<^esub> ts ! p
 2. p \<notin> succs (hd w) \<Longrightarrow> ssa ! p \<sqsubseteq>\<^bsub>r\<^esub> ts ! p
[PROOF STEP]
have transf_hdw_ss_inA: "transf (hd w) ?ss_hdw \<in> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. transf (hd w) (ss ! hd w) \<in> A
[PROOF STEP]
using hd_w_ss_in_A
[PROOF STATE]
proof (prove)
using this:
hd w # ss ! hd w \<in> A

goal (1 subgoal):
 1. transf (hd w) (ss ! hd w) \<in> A
[PROOF STEP]
by (auto simp add:transf_def)
[PROOF STATE]
proof (state)
this:
transf (hd w) (ss ! hd w) \<in> A

goal (2 subgoals):
 1. p \<in> succs (hd w) \<Longrightarrow> ssa ! p \<sqsubseteq>\<^bsub>r\<^esub> ts ! p
 2. p \<notin> succs (hd w) \<Longrightarrow> ssa ! p \<sqsubseteq>\<^bsub>r\<^esub> ts ! p
[PROOF STEP]
have ss_p_inA: "ss!p \<in> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ss ! p \<in> A
[PROOF STEP]
using \<open>p<length ss\<close> ss_inA
[PROOF STATE]
proof (prove)
using this:
p < length ss
ss \<in> nlists n A

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

goal (2 subgoals):
 1. p \<in> succs (hd w) \<Longrightarrow> ssa ! p \<sqsubseteq>\<^bsub>r\<^esub> ts ! p
 2. p \<notin> succs (hd w) \<Longrightarrow> ssa ! p \<sqsubseteq>\<^bsub>r\<^esub> ts ! p
[PROOF STEP]
from transf_ss_ts  transf_hdw_ts_hdw transf_hdw_ss_inA trans_hdw_ts_inA  ts_p_inA
[PROOF STATE]
proof (chain)
picking this:
transf (hd w) (ss ! hd w) \<sqsubseteq>\<^bsub>r\<^esub> transf (hd w) (ts ! hd w)
transf (hd w) (ts ! hd w) \<sqsubseteq>\<^bsub>r\<^esub> ts ! p
transf (hd w) (ss ! hd w) \<in> A
transf (hd w) (ts ! hd w) \<in> A
ts ! p \<in> A
[PROOF STEP]
have "transf (hd w) ?ss_hdw \<sqsubseteq>\<^bsub>r\<^esub> ts ! p"
[PROOF STATE]
proof (prove)
using this:
transf (hd w) (ss ! hd w) \<sqsubseteq>\<^bsub>r\<^esub> transf (hd w) (ts ! hd w)
transf (hd w) (ts ! hd w) \<sqsubseteq>\<^bsub>r\<^esub> ts ! p
transf (hd w) (ss ! hd w) \<in> A
transf (hd w) (ts ! hd w) \<in> A
ts ! p \<in> A

goal (1 subgoal):
 1. transf (hd w) (ss ! hd w) \<sqsubseteq>\<^bsub>r\<^esub> ts ! p
[PROOF STEP]
by (auto intro: order_trans  Semilat.orderI[OF Semilat.intro, OF is_semi])
[PROOF STATE]
proof (state)
this:
transf (hd w) (ss ! hd w) \<sqsubseteq>\<^bsub>r\<^esub> ts ! p

goal (2 subgoals):
 1. p \<in> succs (hd w) \<Longrightarrow> ssa ! p \<sqsubseteq>\<^bsub>r\<^esub> ts ! p
 2. p \<notin> succs (hd w) \<Longrightarrow> ssa ! p \<sqsubseteq>\<^bsub>r\<^esub> ts ! p
[PROOF STEP]
with \<open>ss!p \<sqsubseteq>\<^bsub>r\<^esub> ts ! p\<close> trans_hdw_ts_inA ss_p_inA transf_hdw_ss_inA ssa_p ts_p_inA
[PROOF STATE]
proof (chain)
picking this:
ss ! p \<sqsubseteq>\<^bsub>r\<^esub> ts ! p
transf (hd w) (ts ! hd w) \<in> A
ss ! p \<in> A
transf (hd w) (ss ! hd w) \<in> A
ssa ! p = transf (hd w) (ss ! hd w) \<squnion>\<^bsub>f\<^esub> ss ! p
ts ! p \<in> A
transf (hd w) (ss ! hd w) \<sqsubseteq>\<^bsub>r\<^esub> ts ! p
[PROOF STEP]
show "ssa ! p \<sqsubseteq>\<^bsub>r\<^esub> ts ! p"
[PROOF STATE]
proof (prove)
using this:
ss ! p \<sqsubseteq>\<^bsub>r\<^esub> ts ! p
transf (hd w) (ts ! hd w) \<in> A
ss ! p \<in> A
transf (hd w) (ss ! hd w) \<in> A
ssa ! p = transf (hd w) (ss ! hd w) \<squnion>\<^bsub>f\<^esub> ss ! p
ts ! p \<in> A
transf (hd w) (ss ! hd w) \<sqsubseteq>\<^bsub>r\<^esub> ts ! p

goal (1 subgoal):
 1. ssa ! p \<sqsubseteq>\<^bsub>r\<^esub> ts ! p
[PROOF STEP]
by (auto intro: Semilat.lub[OF Semilat.intro, OF is_semi])
[PROOF STATE]
proof (state)
this:
ssa ! p \<sqsubseteq>\<^bsub>r\<^esub> ts ! p

goal (1 subgoal):
 1. p \<notin> succs (hd w) \<Longrightarrow> ssa ! p \<sqsubseteq>\<^bsub>r\<^esub> ts ! p
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. p \<notin> succs (hd w) \<Longrightarrow> ssa ! p \<sqsubseteq>\<^bsub>r\<^esub> ts ! p
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
p \<notin> succs (hd w)

goal (1 subgoal):
 1. p \<notin> succs (hd w) \<Longrightarrow> ssa ! p \<sqsubseteq>\<^bsub>r\<^esub> ts ! p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p \<notin> succs (hd w)
[PROOF STEP]
have "p \<notin> set (map fst ?qs)"
[PROOF STATE]
proof (prove)
using this:
p \<notin> succs (hd w)

goal (1 subgoal):
 1. p \<notin> set (map fst (step (hd w) (ss ! hd w)))
[PROOF STEP]
using fin_succ_hd_w
[PROOF STATE]
proof (prove)
using this:
p \<notin> succs (hd w)
finite (succs (hd w))

goal (1 subgoal):
 1. p \<notin> set (map fst (step (hd w) (ss ! hd w)))
[PROOF STEP]
by (auto simp add:step_def exec_def)
[PROOF STATE]
proof (state)
this:
p \<notin> set (map fst (step (hd w) (ss ! hd w)))

goal (1 subgoal):
 1. p \<notin> succs (hd w) \<Longrightarrow> ssa ! p \<sqsubseteq>\<^bsub>r\<^esub> ts ! p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p \<notin> set (map fst (step (hd w) (ss ! hd w)))
[PROOF STEP]
have "ssa!p = ss!p"
[PROOF STATE]
proof (prove)
using this:
p \<notin> set (map fst (step (hd w) (ss ! hd w)))

goal (1 subgoal):
 1. ssa ! p = ss ! p
[PROOF STEP]
using exec2 p_lt_len_ssa len_ss len_ssa
[PROOF STATE]
proof (prove)
using this:
p \<notin> set (map fst (step (hd w) (ss ! hd w)))
\<lbrakk>?q \<notin> set (map fst (step (hd w) (ss ! hd w))); ?q < length ss\<rbrakk> \<Longrightarrow> ssa ! ?q = ss ! ?q
p < length ssa
length ss = n
length ssa = n

goal (1 subgoal):
 1. ssa ! p = ss ! p
[PROOF STEP]
by(auto simp add:step_def exec_def)
[PROOF STATE]
proof (state)
this:
ssa ! p = ss ! p

goal (1 subgoal):
 1. p \<notin> succs (hd w) \<Longrightarrow> ssa ! p \<sqsubseteq>\<^bsub>r\<^esub> ts ! p
[PROOF STEP]
with ss_ts_p
[PROOF STATE]
proof (chain)
picking this:
ss ! p \<sqsubseteq>\<^bsub>r\<^esub> ts ! p
ssa ! p = ss ! p
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ss ! p \<sqsubseteq>\<^bsub>r\<^esub> ts ! p
ssa ! p = ss ! p

goal (1 subgoal):
 1. ssa ! p \<sqsubseteq>\<^bsub>r\<^esub> ts ! p
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ssa ! p \<sqsubseteq>\<^bsub>r\<^esub> ts ! p

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
ssa ! p \<sqsubseteq>\<^bsub>r\<^esub> ts ! p

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>p<length ssa. ssa ! p \<sqsubseteq>\<^bsub>r\<^esub> ts ! p

goal (1 subgoal):
 1. \<And>ts. \<lbrakk>ts \<in> nlists n A; ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> (\<forall>p<n. Typing_Framework_1.stable r step ts p)\<rbrakk> \<Longrightarrow> ssa [\<sqsubseteq>\<^bsub>r\<^esub>] ts
[PROOF STEP]
with \<open>length ss = length ts\<close> len_ss len_ssa
[PROOF STATE]
proof (chain)
picking this:
length ss = length ts
length ss = n
length ssa = n
\<forall>p<length ssa. ssa ! p \<sqsubseteq>\<^bsub>r\<^esub> ts ! p
[PROOF STEP]
show "ssa [\<sqsubseteq>\<^bsub>r\<^esub>] ts"
[PROOF STATE]
proof (prove)
using this:
length ss = length ts
length ss = n
length ssa = n
\<forall>p<length ssa. ssa ! p \<sqsubseteq>\<^bsub>r\<^esub> ts ! p

goal (1 subgoal):
 1. ssa [\<sqsubseteq>\<^bsub>r\<^esub>] ts
[PROOF STEP]
by (auto simp only:Listn.le_def lesssub_def lesub_def intro:list_all2_all_nthI)
[PROOF STATE]
proof (state)
this:
ssa [\<sqsubseteq>\<^bsub>r\<^esub>] ts

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<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> ssa [\<sqsubseteq>\<^bsub>r\<^esub>] ts

goal (1 subgoal):
 1. \<lbrakk>wf_dom ss0 w0; w \<noteq> []; propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ssa, wa); wf_dom ss w; 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\<rbrakk> \<Longrightarrow> ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ssa \<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> ssa [\<sqsubseteq>\<^bsub>r\<^esub>] ts)
[PROOF STEP]
with g1
[PROOF STATE]
proof (chain)
picking this:
ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ssa
\<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> ssa [\<sqsubseteq>\<^bsub>r\<^esub>] ts
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ssa
\<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> ssa [\<sqsubseteq>\<^bsub>r\<^esub>] ts

goal (1 subgoal):
 1. ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ssa \<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> ssa [\<sqsubseteq>\<^bsub>r\<^esub>] ts)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ssa \<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> ssa [\<sqsubseteq>\<^bsub>r\<^esub>] ts)

goal:
No subgoals!
[PROOF STEP]
qed