header {* (Infinite) Sequences *} 

theory Sequence
imports Main
begin

text {* Formalises sequence for TLA. We assume all sequences are infinite,
 but we can extract finite segments of them. Finite sequences are 
 postfixed with an infinite chain of stuttering steps. *}

types 'a seq = "nat \<Rightarrow> 'a"

text {* A sequence @{typ "'a seq"} is a function @{typ "nat \<Rightarrow> 'a"}. A sequence is 
 infinite since natural numbers are infinite. The state space @{typ "'a"} is 
 parameterized. *}

section "Some general Sequence functions"

text {* Some general functions on sequences are provided *}

constdefs

 first :: "'a seq \<Rightarrow> 'a"
 "first s \<equiv> s 0"

 second :: "('a seq) \<Rightarrow> 'a"
 "second s \<equiv> s (1::nat)"

 suffix :: "'a seq \<Rightarrow> nat \<Rightarrow> 'a seq" ("_ |\<^sub>s _")
 "s |\<^sub>s i \<equiv> \<lambda> n. s (n+i)"

 prefix :: "'a seq \<Rightarrow> nat \<Rightarrow> 'a seq" ("_[\<dots>_]")
 "s[\<dots>i] \<equiv> \<lambda> n. if n \<le> i then s n else s i"

 tail :: "'a seq \<Rightarrow> 'a seq"
 "tail s \<equiv> s |\<^sub>s 1"

 map :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a seq) \<Rightarrow> ('b seq)"
 "map f \<equiv> \<lambda> s. \<lambda> n. f (s n)"

 app :: "'a \<Rightarrow> ('a seq) \<Rightarrow> ('a seq)" (infixl "##" 60)
 "s ## \<sigma>  \<equiv> \<lambda> n. if n=0 then s else \<sigma> (n-(1::nat))"

 text {* @{text "s |\<^sub>s i"} returns the suffix of sequence @{term s} starting
  at state @{term i}.  @{term first} returns the first state of a sequence
  while  @{term second} returns the second state. @{term tail} returns the
  sequence starting at the second state. @{term "s ## \<sigma>"} prefixes the
  sequence @{term \<sigma>} by state @{term s} *}

subsection "Properties of @{term first} and @{term second}"

lemma first_tail_second: "first(tail s) = second s" 
proof -
 have  "first(tail s) = (tail s) 0" by (simp add: first_def)
 hence "first(tail s) = (s |\<^sub>s 1) 0" by (simp add: tail_def)
 hence "first(tail s) = s (0+1)" by (simp add: suffix_def)
 hence "first(tail s) = s 1" by auto
 thus ?thesis by (unfold second_def)
qed

subsection "Properties of @{term suffix}"

lemma suffix_first: "first (s |\<^sub>s n) = s n"
  by (auto simp add: suffix_def first_def)

lemma suffix_second: "second (s |\<^sub>s n) = s (Suc n)"
  by (auto simp add: suffix_def second_def)

lemma suffix_plus: "s |\<^sub>s n |\<^sub>s m = s |\<^sub>s (m + n)" 
proof -
 have "s |\<^sub>s n = (\<lambda> k. s (k+n))" by (simp add: suffix_def)
 hence "s |\<^sub>s n |\<^sub>s m = ((\<lambda> k. s (k+n)) |\<^sub>s m)" by simp
 hence "s |\<^sub>s n |\<^sub>s m = (\<lambda> l. s (l+m+n))" by (simp add: suffix_def)
 hence "s |\<^sub>s n |\<^sub>s m = (\<lambda> l. s (l+(m+n)))" by (simp add: nat_add_assoc)
 thus  "s |\<^sub>s n |\<^sub>s m = s |\<^sub>s (m + n)" by (simp add: suffix_def)
qed

lemma suffix_commute: "((s |\<^sub>s n) |\<^sub>s m) = ((s |\<^sub>s m) |\<^sub>s n)"
proof -
  have "s |\<^sub>s n |\<^sub>s m = s |\<^sub>s n |\<^sub>s m" ..
  hence "s |\<^sub>s n |\<^sub>s m = s |\<^sub>s (m + n)" by (simp add: suffix_plus) 
  hence "s |\<^sub>s n |\<^sub>s m = s |\<^sub>s (n + m)" by (simp add: nat_add_commute) 
  thus "s |\<^sub>s n |\<^sub>s m = s |\<^sub>s m |\<^sub>s n" by (simp add: suffix_plus)
qed

lemma suffix_plus_com: "s |\<^sub>s m |\<^sub>s n = s |\<^sub>s (m + n)" 
proof -
  have "s |\<^sub>s n |\<^sub>s m = s |\<^sub>s (m + n)" by (rule suffix_plus)
  thus "s |\<^sub>s m |\<^sub>s n = s |\<^sub>s (m + n)" by (simp add: suffix_commute)
qed

lemma suffix_zero[simp]: "s |\<^sub>s 0 = s"
proof -
  have "s |\<^sub>s 0 = (\<lambda> k. s (k+0))" by (simp add: suffix_def)
  hence "s |\<^sub>s 0 = (\<lambda> k. s k)" by simp
  thus ?thesis by simp
qed

lemma suffix_tail: "s |\<^sub>s 1 = tail s"
proof -
  have "s |\<^sub>s 1 = (\<lambda> k. s (k+1))" by (simp add: suffix_def)
  thus ?thesis by (simp add: tail_def)
qed

lemma suffix_tail: "s |\<^sub>s 1 = tail s"
proof -
  have "s |\<^sub>s 1 = (\<lambda> k. s (k+1))" by (simp add: suffix_def)
  thus ?thesis by (simp add: tail_def)
qed

lemma tail_suffix_suc: "s |\<^sub>s (Suc n) = tail (s |\<^sub>s n)"
by (auto simp add: suffix_def tail_def)

subsection "Properties of @{term map}"

lemma seq_map_dist: "\<forall> n. f (s n) = (map f s) n"
proof -
 have "\<forall> n. f (s n) = f (s n)"  by auto
 thus "\<forall> n. f (s n) = (map f s) n" by (unfold map_def)
qed

lemma seq_map_compose: "map (f o g) s = map f (map g s)"
proof -
  have "f o g == \<lambda> s. f(g(s))" by (unfold comp_def)
  hence "map (f o g) = (\<lambda> s. \<lambda>n. f (g (s n)))" by (simp add: map_def)
  hence "map (f o g) s = (\<lambda>n. f (g (s n)))" by simp
  thus ?thesis by (simp add: map_def)
qed

subsection "Properties of  @{term app}"

lemma seq_app_second: "(s ## \<sigma>) 1 = \<sigma> 0"
by (auto simp add: app_def)


lemma seq_app_first: "(s ## \<sigma>) 0 = s" 
by (auto simp add: app_def)

lemma seq_app_first_tail: "(first s) ## (tail s) = s"
proof (rule ext)
  fix x
  show "(first s ## tail s) x = s x"
    by (auto simp add: first_def app_def suffix_def tail_def)
qed

lemma seq_app_tail: "tail (x ## s) = s"
  by (auto simp add: app_def tail_def suffix_def)

lemma seq_app_greather_than_zero: "\<forall> n > 0. (s ## \<sigma>) n = \<sigma> (n-(1::nat))" 
by (auto simp add: app_def)

section "Finite and Empty Sequences"

text{* In this section we identify finite and empty 
  sequences and prove lemmas of them. *}

constdefs 

 fin :: "('a seq) \<Rightarrow> bool"
 "fin s \<equiv> \<exists> i. \<forall> j \<ge> i. s j = s i"

 inf :: "('a seq) \<Rightarrow> bool"
 "inf s \<equiv> \<forall> i. \<exists> j \<ge> i. s j \<noteq> s i"

 last :: "('a seq) \<Rightarrow> nat"
 "last s \<equiv> LEAST i. (\<forall> j \<ge> i. s j = s i)" 

 laststate :: "('a seq) \<Rightarrow> 'a"
 "laststate s \<equiv> s (last s)"

 emptyseq :: "('a seq) \<Rightarrow> bool"
 "emptyseq \<equiv> \<lambda> s. \<forall> i. s i = s 0"

 notemptyseq :: "('a seq) \<Rightarrow> bool"
 "notemptyseq \<equiv> \<lambda> s. \<exists> i. s i \<noteq> s 0"

text {*  Predicate @{term fin} holds if there is an element
  in the sequence such that all succeding elements are identical,
  i.e. the sequence is finite. @{term "last s"} returns the (first occurence 
  of the) last element id (number) in a finite sequence @{term s}. Note that 
  if @{text s} is not finite then an arbitrary number is returned. The 
  @{text i} must be unique: Since we use @{text LEAST} and not @{text THE} this
  holds since @{text LEAST} requires the smallest number where this property 
  holds. @{term laststate} returns the last @{typ "'a"} (i.e. state). We assume 
  that the sequence is finite when using  @{term last} and  @{term laststate}.
  Predicate @{term emptyseq} identifies empty sequences -- i.e. all states in
  the sequence are identical to the initial one, while @{term notemptyseq} holds
  if the given sequence is not empty. *} 


subsection "Properties of @{term fin} and @{term inf}"

lemma inf_not_fin: "(\<not>(fin s)) = inf s"
proof (rule iffI)
  assume a1: "\<not> fin s"
  show "inf s"
  proof (unfold inf_def)
    from a1 have "\<not>(\<exists> i. \<forall> j. j \<ge> i \<longrightarrow> s j = s i)" by (unfold fin_def)
    hence "\<not>(\<exists> i.\<not>(\<exists> j. \<not>(j \<ge> i \<longrightarrow> s j = s i)))" by auto
    hence "\<not>(\<exists> i.\<not>(\<exists> j. (j \<ge> i \<and> s j \<noteq> s i)))" by auto
    thus "\<forall> i. \<exists> j. j \<ge> i \<and> s j \<noteq> s i" by auto
  qed
next
  assume a2: "inf s"
  show "\<not> fin s"
  proof (unfold fin_def)
    from a2 have "\<forall> i. \<exists> j. j \<ge> i \<and> s j \<noteq> s i" by (unfold inf_def)
    hence "\<forall> i. \<exists> j. j \<ge> i \<and> \<not>(s j = s i)" by auto
    hence "\<forall> i. \<not>(\<forall> j.\<not>( j \<ge> i \<and> \<not>(s j = s i)))" by auto
    hence "\<not>(\<exists> i. \<forall> j.\<not>( j \<ge> i \<and> \<not>(s j = s i)))" by auto
    thus "\<not>(\<exists> i. \<forall> j. j \<ge> i \<longrightarrow> s j = s i)" by auto
  qed
qed

lemma fin_not_inf: "(fin s) = (\<not>(inf s))"
proof (rule iffI)
  assume a1: "fin s"
  show "\<not> inf s"
  proof (unfold inf_def)
    from a1 have "(\<exists> i. \<forall> j. j \<ge> i \<longrightarrow> s j = s i)" by (unfold fin_def)
    hence "(\<exists> i.\<not>(\<exists> j. \<not>(j \<ge> i \<longrightarrow> s j = s i)))" by auto
    hence "(\<exists> i.\<not>(\<exists> j. (j \<ge> i \<and> s j \<noteq> s i)))" by auto
    thus "\<not>(\<forall> i. \<exists> j. j \<ge> i \<and> s j \<noteq> s i)" by auto
  qed
next
  assume a2: "\<not> inf s"
  show "fin s"
  proof (unfold fin_def)
    from a2 have "\<not>(\<forall> i. \<exists> j. j \<ge> i \<and> s j \<noteq> s i)" by (unfold inf_def)
    hence "\<not>(\<forall> i. \<exists> j. j \<ge> i \<and> \<not>(s j = s i))" by auto
    hence "\<not>(\<forall> i. \<not>(\<forall> j.\<not>( j \<ge> i \<and> \<not>(s j = s i))))" by auto
    hence "\<exists> i. \<forall> j.\<not>( j \<ge> i \<and> \<not>(s j = s i))" by auto
    thus "\<exists> i. \<forall> j. j \<ge> i \<longrightarrow> s j = s i" by auto
  qed
qed

lemma "\<forall> s. fin s \<or> inf s"
proof
  fix s
  show "fin s \<or> inf s"
  proof (cases "fin s")
   assume "fin s" show "fin s \<or> inf s" by (rule disjI1)
  next
   assume "\<not>(fin s)" hence "inf s" by (auto simp add: inf_not_fin)
   thus "fin s \<or> inf s" by auto
  qed
qed

subsection "Properties of @{term emptyseq}"

lemma empty_is_finite: assumes h1: "emptyseq s" shows "fin s"
proof -
 from h1 have g1:"\<forall> j. s j = s 0" by (unfold emptyseq_def)
 hence "\<exists> i. \<forall> j. s j = s i" by auto
 from g1 this have "\<exists> i. \<forall> j \<ge> i. s j = s i" by auto
 thus ?thesis by (unfold fin_def)
qed

lemma empty_suffix_is_empty: assumes H: "emptyseq s" shows "\<forall> n. emptyseq (s |\<^sub>s n)"
proof (rule allI,unfold emptyseq_def,rule allI)
 fix i n
 from H have a1: "\<forall> i. s i = s 0" by (unfold emptyseq_def)
 hence "s (i+n) = s 0" ..
 hence g1: "(s |\<^sub>s n) i = s 0" by (unfold suffix_def)
 from a1 have "s (0+n) = s 0" ..
 hence g2: "(s |\<^sub>s n) 0 = s 0" by (unfold suffix_def)
 with g1 show "(s |\<^sub>s n) i = (s |\<^sub>s n) 0" by auto
qed

lemma empty_suffix_exteq: assumes H:"emptyseq s" shows "\<forall> m. (s |\<^sub>s n) m = s m"
proof (rule allI,unfold suffix_def)
  fix m n
  from H have a1: "\<forall> n. s n = s 0" by (unfold emptyseq_def) 
  { from a1 have "s m = s 0" ..}
  moreover
  { from a1 have "s (m + n) = s 0" ..}
  ultimately show "s (m + n) = s m" by auto
qed

lemma empty_suffix_eq: assumes H: "emptyseq s" shows "(s |\<^sub>s n) = s"
proof (rule ext)
  fix m
  from  H have "\<forall> m. (s |\<^sub>s n) m = s m" by (rule empty_suffix_exteq)
  thus "(s |\<^sub>s n) m = s m" ..
qed

lemma seq_not_empty_notempty: "(\<not>(emptyseq s)) = notemptyseq s"
proof (rule iffI)
  assume a1: "\<not>(emptyseq s)"
  thus g1: "notemptyseq s" 
  proof -
   from a1 have "\<not>(\<forall> i. s i = s 0)" by (unfold emptyseq_def)
   hence "(\<exists> i. s i \<noteq> s 0)" by auto
   thus ?thesis by (unfold notemptyseq_def)
  qed
next
  assume a2: "notemptyseq s"
  thus g2: "\<not>(emptyseq s)"
  proof -
    from a2 have  "(\<exists> i. s i \<noteq> s 0)" by (unfold notemptyseq_def)
    hence  "\<not>(\<forall> i. s i = s 0)" by auto
    thus ?thesis by (unfold emptyseq_def) 
  qed
qed

lemma seq_notnot_empty_empty: "(emptyseq s) = (\<not>(notemptyseq s))"
proof (rule iffI)
  assume a1: "emptyseq s" show "\<not> notemptyseq s" 
  proof -
    from a1 have "\<forall> i. s i = s 0" by (unfold emptyseq_def)
    hence "\<not>(\<exists> i. s i \<noteq> s 0)" by auto
    thus "\<not> notemptyseq s" by (unfold notemptyseq_def)
  qed
next 
  assume a2: "\<not> notemptyseq s" show "emptyseq s" 
  proof -
    from a2 have "\<not>(\<exists> i. s i \<noteq> s 0)" by (unfold notemptyseq_def)
    hence "\<forall> i. s i = s 0" by blast
    thus ?thesis by (unfold emptyseq_def)
  qed
qed

lemma seq_empty_or_notempty: "emptyseq s \<or> notemptyseq s"
proof -   
  have "emptyseq s \<or> \<not>(emptyseq s)" 
  proof (cases "emptyseq s")
    case True thus ?thesis ..
  next
    case False thus ?thesis ..
  qed
  thus ?thesis by (auto simp add: seq_notnot_empty_empty)
qed

lemma suc_empty: assumes H1: "emptyseq (s |\<^sub>s m) " shows "emptyseq (s |\<^sub>s (Suc m))"
proof (unfold emptyseq_def,rule allI,unfold suffix_def,simp)
  fix i
  from H1 have "\<forall>i. (s |\<^sub>s m) i = (s |\<^sub>s m) 0" by (unfold emptyseq_def)
  hence a1:"\<forall>i. s (i+m) = s (0+m)" by (unfold suffix_def)
  hence "s (1+m) = s (0+m)" ..
  hence g1: "s (Suc m) = s m" by auto
  from a1 have "s ((i+1)+m) = s (0+m)" ..
  hence g2: "s (Suc (i+m)) = s m" by auto
  with g1 show "s (Suc (i+m)) = s (Suc m)" by auto
qed

lemma assumes h: "\<forall> n. s n = s 0" shows "\<forall> n. s n = s (Suc n)"
proof
  fix n
  show "s n = s (Suc n)"
  proof -
    from h have g1: "s n = s 0" ..
    from h have g2: "s (Suc n) = s 0" by auto
    with g1 show ?thesis by auto
  qed
qed

lemma seq_empty_all: assumes H: "\<forall> i. s i = s 0" shows "\<forall> i j. s i = s j"
proof
 fix i
 show "\<forall> j. s i = s j"
 proof
   fix j
   show "s i = s j"
   proof -
     from H have g1: "s i = s 0" ..
     from H have g2: "s j = s 0" ..
     with g1 show "s i = s j" by simp
   qed
 qed
qed

subsection "Properties of @{term last} and @{term laststate}" 

lemma fin_stut_after_last: assumes H: "fin s" shows "(\<forall> j \<ge> (last s). s j =  s (last s))"
proof 
  fix j
  show "last s \<le> j \<longrightarrow> s j = s (last s)"
  proof -
    from H have a1: "\<exists> i. \<forall> j \<ge> i. s j = s i" by (unfold fin_def)
    from a1 obtain i where "\<forall> j \<ge> i. s j = s i" (is "?P i")  .. 
    hence "?P (LEAST x. ?P x)" by (rule LeastI)
    hence "\<forall> j \<ge> (last s). s j = s (last s)"  by (fold last_def)
    thus "(last s) \<le> j \<longrightarrow> s j = s (last s)" by blast
  qed
qed

section "Stuttering Invariance"

text {* This section provides functions for removing stuttering
 steps of sequences, i.e. we formalise Lamports @{text \<natural>} operator.
 However, the semantics differs from Lamports, and is closer to
 Wahab's definition in the PVS prover. *}



constdefs

  nonstutseq :: "('a seq) \<Rightarrow> bool"
  "nonstutseq \<equiv> \<lambda> s. \<forall> i. s i = s (Suc i) \<longrightarrow> (\<forall> j > i. s i = s j)"

  stutstep :: "('a seq) \<Rightarrow> nat \<Rightarrow> bool"
  "stutstep s n \<equiv> (s n = s (Suc n))"

  nextnat :: "('a seq) \<Rightarrow> nat"
  "nextnat \<equiv> \<lambda> s. if emptyseq s then 0 else LEAST i. s i \<noteq> s 0"

  nextsuffix :: "('a seq) \<Rightarrow> ('a seq)"
  "nextsuffix \<equiv> \<lambda> s. s |\<^sub>s (nextnat s)"

consts
  "next" :: "nat \<Rightarrow> ('a seq) \<Rightarrow> ('a seq)"

primrec
 "next 0 = id"
 "next (Suc n) = (nextsuffix) o (next n)"

constdefs 
  collapse :: "('a seq) \<Rightarrow> ('a seq)" ("\<natural>") 
  "\<natural> s \<equiv> \<lambda> n. (next n s) 0"

text {* Predicate @{term nonstutseq} identifies sequences without any 
  stuttering steps -- except for an infinite empty sequence suffix. 
  Further, @{term "stutstep s n"} is a predicate which holds if the step
  after @{term "s n"} is equal to @{term "s n"}, i.e. @{term "Suc n"} is
  a stuttering step.
  @{term "collapse s"} / @{term "\<natural> s"} formalises Lamports  @{term "\<natural>"}
  operator. It returns the first state of the result of @{term "next n s"}. 
  @{term "next n s"} finds suffix of the $n^{th}$ change. Hence the first
  element, which @{term "\<natural> s"} returns, is the state after the $n^{th}$ 
  change.  @{term "next n s"} is defined by primitive recursion on 
  @{term "n"} using function composition of function @{term nextsuffix}. E.g.
  @{term "next 3 s"} equals @{term "nextsuffix (nextsuffix (nextsuffix s))"}.
  @{term "nextsuffix s"} returns the suffix of the sequence starting at the
  next changing state. It uses @{term "nextnat"} to obtain this. All the real
  computation is done in htis function. Firstly, an empty sequence will obviously
  not contain any changes, and @{text 0} is therefore returned. In this case 
  @{term "nextsuffix"} behaves like the identify function. If the sequence is not
  empty then the smallest number @{term "i"} such that @{term "s i"} is different
  from the initial state is returned. This is achieved by @{term "Least"}. *}

subsection "Properties of @{term nonstutseq}"

lemma seq_empty_is_nonstut: assumes H: "emptyseq s" shows "nonstutseq s" 
proof (unfold nonstutseq_def)
  show "\<forall>i. s i = s (Suc i) \<longrightarrow> (\<forall>j. i < j \<longrightarrow> s i = s j)"
  proof
    fix i
    show "s i = s (Suc i) \<longrightarrow> (\<forall>j. i < j \<longrightarrow> s i = s j)"
    proof(rule impI,rule allI,rule impI)
      fix j
      assume a1: "s i = s (Suc i)"
      assume a2: "i < j"
      show "s i = s j"
      proof -
        from H have a3: "\<forall> i. s i = s 0" by (unfold emptyseq_def)
        hence  "\<forall> i j. s i = s j" by (rule seq_empty_all)
        thus "s i = s j" by simp
      qed
    qed
   qed
qed

lemma notempty_exist_nonstut: assumes H: "\<not> emptyseq  (s |\<^sub>s m)" shows "\<exists> i. s i \<noteq> s m \<and> i > m"
proof -
 from H have a1: "\<not>(\<forall> i. (s |\<^sub>s m) i = (s |\<^sub>s m) 0)" by (unfold emptyseq_def)
 hence "\<exists> i. (s |\<^sub>s m) i \<noteq> (s |\<^sub>s m) 0" by auto
 hence "\<exists> i. s (i+m) \<noteq>  s (0+m)" by (auto simp add: suffix_def)
 hence g1: "\<exists> i. s (i+m) \<noteq>  s m" by auto
 from g1 obtain i where g1': "s (i+m) \<noteq> s m" ..
 have "(s (i+m)) \<noteq> (s m) \<longrightarrow> (i \<noteq> 0)"
 proof (rule impI,rule ccontr)
   assume "\<not> i \<noteq> 0" hence a1: "i = 0" by arith
   assume "s (i + m) \<noteq> s m"
   with a1 have "s (0+m) \<noteq> s m" by auto
   hence "s m \<noteq> s m" by auto
   thus False by auto
 qed
 with g1' have "i \<noteq> 0" by auto
 hence g2: "i+m > m" by arith
 with g1' have "s (i+m) \<noteq> s m \<and> (i+m) > m" by auto
 thus "\<exists> j. s j \<noteq> s m \<and> j > m" by auto
qed

subsection "Properties of @{term nextnat}"

lemma nextnat_le_unch: assumes H: "n < nextnat s" shows "s n = s 0"
proof (cases "emptyseq s")
  assume "emptyseq s"
  hence "nextnat s = 0" by (simp add: nextnat_def)
  with H show ?thesis by auto
next
  assume "\<not> emptyseq s"
  hence a1: "nextnat s = (LEAST i. s i \<noteq> s 0)" by (simp add: nextnat_def) 
  show ?thesis
  proof (rule ccontr)
    assume a2: "s n \<noteq> s 0" (is "?P n")
    hence "(LEAST i. s i \<noteq> s 0) \<le> n" by (rule Least_le)
    hence "\<not>(n < (LEAST i. s i \<noteq> s 0))" by auto
    also from H a1 have "n < (LEAST i. s i \<noteq> s 0)" by simp
    ultimately show False by auto
  qed
qed

lemma stutnempty: assumes H: "\<not> stutstep s n" shows "\<not> emptyseq (s |\<^sub>s n)"
proof (unfold emptyseq_def suffix_def)
  from H have "s (Suc n) \<noteq> s n" by (auto simp add: stutstep_def)
  hence "s (1+n) \<noteq> s (0+n)" by auto
  hence "\<exists> i. s (i+n) \<noteq> s (0+n)" .. 
  thus "\<not>(\<forall> i. s (i+n) = s (0+n))" by auto
qed

lemma notstutstep_nexnat1: assumes H: "\<not> stutstep s n" shows "nextnat (s |\<^sub>s n) = 1"
proof -
  from H have h': "nextnat (s |\<^sub>s n) = (LEAST i. (s |\<^sub>s n) i \<noteq> (s |\<^sub>s n) 0)" 
    by (auto simp add: nextnat_def stutnempty)
  from H have "s (Suc n) \<noteq> s n" by (auto simp add: stutstep_def)
  hence "(s |\<^sub>s n) (1::nat) \<noteq> (s |\<^sub>s n) 0" (is "?P (1::nat)") by (auto simp add: suffix_def)
  hence "Least ?P \<le> 1" by (rule Least_le)
  hence g1: "Least ?P = 0 \<or> Least ?P = 1" by auto
  with h' have g1': "nextnat (s |\<^sub>s n) = 0 \<or> nextnat (s |\<^sub>s n) = 1" by auto
  also have "nextnat (s |\<^sub>s n) \<noteq> 0" 
  proof -
    from H have "\<not> emptyseq (s |\<^sub>s n)" by (rule stutnempty)
    hence "notemptyseq (s |\<^sub>s n)" by (simp add: seq_not_empty_notempty)
    hence "\<exists> i. (s |\<^sub>s n) i \<noteq>  (s |\<^sub>s n) 0" by (unfold notemptyseq_def)
    then obtain i where "(s |\<^sub>s n) i \<noteq>  (s |\<^sub>s n) 0" ..
    hence "(s |\<^sub>s n) (LEAST i. (s |\<^sub>s n) i \<noteq> (s |\<^sub>s n) 0) \<noteq> (s |\<^sub>s n) 0" by (rule LeastI)
    with h' have g2: "(s |\<^sub>s n) (nextnat (s |\<^sub>s n)) \<noteq> (s |\<^sub>s n) 0" by auto
    show "(nextnat (s |\<^sub>s n)) \<noteq> 0" 
    proof
      assume "(nextnat (s |\<^sub>s n)) = 0"
      hence "(s |\<^sub>s n) (nextnat (s |\<^sub>s n)) = (s |\<^sub>s n) 0" by auto
      with g2 show False ..
    qed
  qed
  ultimately show  "nextnat (s |\<^sub>s n) = 1" by auto
qed


lemma stutstep_notempty_notempty: 
     assumes h1: "notemptyseq (s |\<^sub>s n)" (is "notemptyseq ?s")
        and h2: "stutstep s n" 
       shows "notemptyseq (s |\<^sub>s (Suc n))" (is "notemptyseq ?sn")
proof (rule ccontr)
  assume a1: "\<not> notemptyseq (s |\<^sub>s (Suc n))" 
  hence a1': "emptyseq ?sn" by (simp add: seq_notnot_empty_empty) 
  hence a2: "\<forall> i. ?sn i = ?sn 0" by (auto simp add: emptyseq_def)
  from h2 have h2':"s n = s (Suc n)" by (simp add: stutstep_def)
  from h1 have "\<exists> i. ?s i \<noteq> ?s 0" by (simp add: notemptyseq_def)
  then obtain i where a3: "?s i \<noteq> ?s 0" ..
  hence g1: "s (i+n) \<noteq> s n" by (simp add: suffix_def)
  have g2:"i > 0" 
  proof (rule ccontr)
    assume "\<not>(i > 0)" hence "i=0" by arith
    hence "s (i+n) = s n" by auto
    with g1 show False by auto
  qed
  from a2 have " ?sn (i-(1::nat)) = ?sn 0" ..
  hence "s ((i-(1::nat))+(Suc n)) = s (Suc n)" by (auto simp add: suffix_def)
  hence "s (i-(1::nat)+(1::nat)+n) = s (Suc n)" by auto
  with g2 have "s (i+n) = s (Suc n)" by auto
  with h2' have "s (i+n) = s n" by simp
  with g1 show False by auto
qed

lemma stutstep_notempty_sucnextnat: 
  assumes h1: "\<not> emptyseq  (s |\<^sub>s n)" and h2: "stutstep s n" 
   shows "(nextnat (s |\<^sub>s n)) = Suc (nextnat (s |\<^sub>s (Suc n)))"
proof -
  from h2 have g1: "\<not>(s (0+n) \<noteq> s (Suc n))" (is "\<not> ?P 0") by (auto simp add: stutstep_def)
  from h1 have "notemptyseq  (s |\<^sub>s n)" by (simp add:  seq_not_empty_notempty)
  hence "\<exists> i. (s |\<^sub>s n) i \<noteq> (s |\<^sub>s n) 0" by (unfold notemptyseq_def)
  then obtain i where "(s |\<^sub>s n) i \<noteq> (s |\<^sub>s n) 0" ..
  hence "s (i+n) \<noteq> s n" by (simp add: suffix_def)
  with h2 have g2: "s (i+n) \<noteq> s (Suc n)" (is "?P i") by (simp add: stutstep_def)
  from g2 g1 have "(LEAST n. ?P n) = Suc (LEAST n. ?P (Suc n))" by (rule Least_Suc)
  from g2 g1 have "(LEAST i. s (i+n) \<noteq> s (Suc n)) = Suc (LEAST i. s ((Suc i)+n) \<noteq> s (Suc n))"
    by (rule Least_Suc)
  hence G1: "(LEAST i. s (i+n) \<noteq> s (Suc n)) = Suc (LEAST i. s (i+Suc n) \<noteq> s (Suc n))" by auto
  from h1 h2 have "\<not> emptyseq  (s |\<^sub>s Suc n)"
    by (simp add: seq_not_empty_notempty stutstep_notempty_notempty)
  hence "nextnat (s |\<^sub>s Suc n) = (LEAST i. (s |\<^sub>s Suc n) i \<noteq> (s |\<^sub>s Suc n) 0)"
    by (auto simp add: nextnat_def)
  hence g1: "nextnat (s |\<^sub>s Suc n) = (LEAST i. s (i+(Suc n)) \<noteq> s (Suc n))"
    by (simp add: suffix_def)
  from h1 have  "nextnat (s |\<^sub>s n) = (LEAST i. (s |\<^sub>s n) i \<noteq> (s |\<^sub>s n) 0)"
    by (auto simp add: nextnat_def)
  hence g2: "nextnat (s |\<^sub>s n) = (LEAST i. s (i+n) \<noteq> s n)" by (simp add: suffix_def)
  with h2 have g2': "nextnat (s |\<^sub>s n) = (LEAST i. s (i+n) \<noteq> s (Suc n))"
    by (auto simp add: stutstep_def)
  from G1 g1 g2' show ?thesis by auto
qed

lemma nextnat_empty_neq: assumes H: "\<not> emptyseq s" shows "s (nextnat s) \<noteq> s 0"
proof -
  from H have a1: "nextnat s =  (LEAST i. s i \<noteq> s 0)" by (simp add: nextnat_def)
  from H have a2: "\<exists> i. s i \<noteq> s 0" by (simp add: seq_not_empty_notempty  notemptyseq_def)
  from this obtain i where "s i \<noteq> s 0" ..
  hence "s (LEAST i. s i \<noteq> s 0) \<noteq> s 0" by (rule LeastI)
  with a1 show ?thesis by auto
qed

lemma nextnat_empty_gzero: assumes H: "\<not> emptyseq s" shows "nextnat s > 0"
proof -
  from H have a1: "s (nextnat s) \<noteq> s 0" by (rule nextnat_empty_neq)
  have "nextnat s \<noteq> 0"
  proof (rule ccontr)
    assume "\<not> nextnat s \<noteq> 0"
    hence "nextnat s = 0" by auto
    hence "s (nextnat s) = s 0" by auto
    with a1 show False by simp
  qed
  thus "nextnat s > 0" by auto
qed

subsection "Properties of @{term nextsuffix}"

lemma empty_nextsuffix: assumes H: "emptyseq s" shows "nextsuffix s = s"
proof -
  from H have "nextnat s = 0" by (simp add: nextnat_def)
  thus ?thesis by (auto simp add: nextsuffix_def)
qed

lemma empty_nextsuffix_id: assumes H: "emptyseq s" shows "nextsuffix s = id s"
proof -
  from H have "nextsuffix s = s" by (rule empty_nextsuffix)
  thus "nextsuffix s = id s" by auto
qed

lemma assumes H: "stutstep s n" shows "nextsuffix (s |\<^sub>s n) = nextsuffix (s |\<^sub>s (Suc n))"
proof (unfold nextsuffix_def)
  show "(s |\<^sub>s n) |\<^sub>s nextnat (s |\<^sub>s n) = (s |\<^sub>s Suc n) |\<^sub>s nextnat (s |\<^sub>s Suc n)"
  proof (cases "emptyseq (s |\<^sub>s n)")
    assume a1: "emptyseq (s |\<^sub>s n)"
    hence a1': "emptyseq (s |\<^sub>s Suc n)" by (rule suc_empty)
    have "(s |\<^sub>s n) = (s |\<^sub>s Suc n)" 
    proof (rule ext, unfold suffix_def)
      fix x
      thm "emptyseq_def"
      { from a1 have "\<forall> i. (s |\<^sub>s n) i =  (s |\<^sub>s n) 0" by (unfold emptyseq_def)
        hence "\<forall> i. s (i+n) = s n" by (simp add: suffix_def)
        hence "s (x+n) = s n" .. }
      moreover
      { from a1' have "\<forall> i. (s |\<^sub>s Suc n) i =  (s |\<^sub>s Suc n) 0" by (unfold emptyseq_def)
        hence "\<forall> i. s (i+Suc n) = s (Suc n)" by (simp add: suffix_def)
        hence "s (x+Suc n) = s (Suc n)" ..  }
      moreover
      from H have "s (Suc n) = s n" by (simp add: stutstep_def)
      ultimately show "s (x + n) = s (x + Suc n)" by simp
    qed
    moreover
    from a1 have "(s |\<^sub>s n) |\<^sub>s nextnat (s |\<^sub>s n) = (s |\<^sub>s n)"
      by (simp add: nextnat_def suffix_zero)
    moreover
    from a1' have "(s |\<^sub>s Suc n) |\<^sub>s nextnat (s |\<^sub>s Suc n) = (s |\<^sub>s Suc n)"
      by (simp add: nextnat_def suffix_zero) 
    ultimately show ?thesis by simp
  next
    assume a1: "\<not> emptyseq (s |\<^sub>s n)"
    with H have "(nextnat (s |\<^sub>s n)) = Suc (nextnat (s |\<^sub>s (Suc n)))" by (simp add: stutstep_notempty_sucnextnat)
    hence "(s |\<^sub>s n) |\<^sub>s nextnat (s |\<^sub>s n) = (s |\<^sub>s n) |\<^sub>s Suc (nextnat (s |\<^sub>s Suc n))" by auto
    also hence "\<dots> = (s |\<^sub>s n) |\<^sub>s (1 + (nextnat (s |\<^sub>s Suc n)))" by auto
    also hence "\<dots> = (s |\<^sub>s n) |\<^sub>s 1 |\<^sub>s (nextnat (s |\<^sub>s Suc n))" by (auto simp: suffix_plus_com)
    also hence "\<dots> = (s |\<^sub>s Suc n) |\<^sub>s (nextnat (s |\<^sub>s Suc n))" by (auto simp: suffix_plus_com)
    finally show ?thesis by auto
  qed
qed

lemma notstutstep_nextsuffix1: assumes H: "\<not> stutstep s n" shows "nextsuffix (s |\<^sub>s n) = s |\<^sub>s (Suc n)"
proof (unfold nextsuffix_def)
  show "(s |\<^sub>s n |\<^sub>s (nextnat (s |\<^sub>s n))) =  s |\<^sub>s (Suc n)"
  proof -
    from H have  "nextnat (s |\<^sub>s n) = 1" by (rule notstutstep_nexnat1)
    hence "(s |\<^sub>s n |\<^sub>s (nextnat (s |\<^sub>s n))) = s |\<^sub>s n |\<^sub>s 1" by auto
    thus ?thesis by (simp add: suffix_def)
  qed
qed

subsection "Properties of @{term next}"

lemma next_first: "next 1 = nextsuffix"
by auto

lemma next_zero: "next 0 s = s"
by auto

lemma next_suc_suffix: "next (Suc n) s = nextsuffix (next n s)"
by auto

lemma next_suffix_com: "nextsuffix (next n s) = (next n (nextsuffix s))"
by (induct n, auto)

lemma next_plus: "next (m+n) s = next m (next n s)" 
by (induct m, auto)

lemma next_empty: assumes H: "emptyseq s" shows "next n s = s"
proof (induct n)
  from H show "next 0 s = s" by auto
next
  fix n
  assume a1: "next n s = s"
  have "next (Suc n) s = nextsuffix (next n s)" by auto
  with a1 have "next (Suc n) s = nextsuffix s" by simp
  with H show "next (Suc n) s = s"
    by (simp add: nextsuffix_def nextnat_def)
qed

lemma notempty_nextnotzero: assumes H: "\<not>emptyseq s" shows "(next (Suc 0) s) 0 \<noteq> s 0"
proof -
  from H have g1: "s (nextnat s) \<noteq> s 0" by (rule nextnat_empty_neq)
  have "next (Suc 0) s = nextsuffix s" by auto
  also hence "\<dots> = s |\<^sub>s (nextnat s)" by (simp add: nextsuffix_def)
  ultimately have "(next (Suc 0) s) 0 =  s |\<^sub>s (nextnat s) 0" by simp
  hence "(next (Suc 0) s) 0 =  s (nextnat s)" by (simp add: suffix_def)
  with g1 show ?thesis by simp
qed

lemma next_ex_id: "\<exists> i. s i = (next m s) 0"
proof -
  have "\<exists> i. (s |\<^sub>s i) = (next m s)"
  proof (induct m)
    have "s |\<^sub>s 0 = next 0 s" by simp
    thus "\<exists> i. (s |\<^sub>s i) = (next 0 s)" ..
  next
    fix m
    assume a1: "\<exists> i. (s |\<^sub>s i) = (next m s)"
    then obtain i where a1': "(s |\<^sub>s i) = (next m s)" ..
    have "next (Suc m) s = nextsuffix (next m s)" by auto
    hence "next (Suc m) s = (next m s) |\<^sub>s (nextnat (next m s))" by (simp add: nextsuffix_def)
    hence "\<exists> i. next (Suc m) s = (next m s) |\<^sub>s i" ..
    then obtain j where "next (Suc m) s = (next m s) |\<^sub>s j" ..
    with a1' have "next (Suc m) s = (s |\<^sub>s i) |\<^sub>s j" by simp
    hence "next (Suc m) s = (s |\<^sub>s (j+i))" by (simp add: suffix_plus)
    hence "(s |\<^sub>s (j+i)) = next (Suc m) s" by simp
    thus "\<exists> i. (s |\<^sub>s i) = (next (Suc m) s)" ..
  qed
  then obtain i where "(s |\<^sub>s i) = (next m s)" ..
  hence "(s |\<^sub>s i) 0 = (next m s) 0" by auto
  hence "s i = (next m s) 0" by (auto simp add: suffix_def)
  thus ?thesis ..
qed
  
subsection "Properties of @{term collapse}"

lemma emptyseq_collapse_eq: assumes A1: "emptyseq s" shows "\<natural> s = s"
proof (unfold collapse_def, rule ext)
  fix n
  from A1 have "next n s = s" by (rule next_empty)
  hence g1: "(next n s) 0 = s 0" by auto
  from A1 have "\<forall> n. s n = s 0" by (auto simp add: emptyseq_def)
  hence g2: "s n = s 0" ..
  with g1 show "(next n s) 0 = s n" by auto
qed

lemma empty_collapse_empty: assumes H: "emptyseq s" shows "emptyseq (\<natural> s)"
proof -
  from H have "\<natural> s = s" by (rule emptyseq_collapse_eq)
  with H show ?thesis by auto
qed

lemma collapse_empty_empty: assumes H: "emptyseq (\<natural> s)" shows "emptyseq s"
proof (rule ccontr)
  assume a1: "\<not>emptyseq s"
  fix i 
  { from H have "\<forall> i. (\<natural> s) i = (\<natural> s) 0" by (unfold emptyseq_def)
    hence "\<forall> i. (next i s) 0 = s 0" by (auto simp add: collapse_def)}
  moreover
  { from a1 have "(next (Suc 0) s) 0 \<noteq> s 0" by (rule notempty_nextnotzero)
    hence "\<exists> i. (next i s) 0 \<noteq> s 0" ..
    hence "\<not>(\<forall> i. (next i s 0) = s 0)" by auto }
  ultimately show False by auto
qed

lemma notempty_collapse_notempty: assumes H: "notemptyseq s" shows "notemptyseq (\<natural> s)"
proof (unfold notemptyseq_def collapse_def)
  from H have "\<not>emptyseq s" by (simp add: seq_not_empty_notempty)
  hence "(next (Suc 0) s 0) \<noteq> s 0" by (rule notempty_nextnotzero)
  hence "\<exists> i. (next i s 0) \<noteq> s 0" ..
  thus "\<exists> i. (next i s 0) \<noteq> (next 0 s 0)" by auto
qed

lemma collapse_notempty_notempty: assumes H: "notemptyseq (\<natural> s)" shows "notemptyseq s"
proof (unfold notemptyseq_def collapse_def)
  from H have "\<exists> i. (\<natural> s) i \<noteq> (\<natural> s) 0" by (unfold notemptyseq_def)
  hence "\<exists> i. (next i s) 0 \<noteq> (next 0 s) 0" by (unfold collapse_def)
  then obtain i where g1: "(next i s) 0 \<noteq> (next 0 s) 0" ..
  have "\<exists> j. s j = (next i s) 0"  by (rule next_ex_id)
  then obtain j where "s j = (next i s) 0" ..
  with g1 have "s j \<noteq> (next 0 s) 0" by simp
  hence "s j \<noteq> s 0" by auto
  thus "\<exists> i. s i \<noteq> s 0" ..
qed

section "Similarity of Sequences"

constdefs
 seqsimilar :: "('a seq) \<Rightarrow> ('a seq) \<Rightarrow> bool" ("_ \<approx> _")
 "\<sigma> \<approx> \<tau> \<equiv> \<forall> n. (\<natural> \<sigma>) n = (\<natural> \<tau>) n"

text {* To sequences @{term s} and @{term t} are \emph{similar} if they 
  are equal up to stuttering, written @{term "s \<approx> t"}. It requires that
  each changing steps are equal -- and is defined using the @{term \<natural>}
  operator. *}

subsection "Properties of @{term seqsimilar}"

lemma seqsim_refl: "s \<approx> s"
by (auto simp add: seqsimilar_def)

lemma seqsim_sym: assumes H: "s \<approx> t" shows "t \<approx> s"
proof (unfold seqsimilar_def, rule allI)
  fix n
  from H have "\<forall> n. (\<natural> s) n = (\<natural> t) n" by (unfold seqsimilar_def)
  hence "(\<natural> s) n = (\<natural> t) n" ..
  thus "(\<natural> t) n = (\<natural> s) n" ..
qed

lemma seqeq_imp_sim: assumes H: "s = t" shows "s \<approx> t"
proof -
  have "s \<approx> s" by (simp add: seqsimilar_def)
  with H show "s \<approx> t" by auto
qed

lemma seqsim_trans: assumes h1: "s \<approx> t" and h2: "t \<approx> z" shows "s \<approx> z" 
proof (unfold seqsimilar_def, rule allI)
  fix n
  { from h1 have "\<forall> n. (\<natural> s) n = (\<natural> t) n" by (unfold seqsimilar_def)
    hence "(\<natural> s) n = (\<natural> t) n" .. }
  moreover
  { from h2 have "\<forall> n. (\<natural> t) n = (\<natural> z) n" by (unfold seqsimilar_def)
    hence "(\<natural> t) n = (\<natural> z) n" .. }
  ultimately show "(\<natural> s) n = (\<natural> z) n" by auto
qed


theorem sim_first: assumes H: "s \<approx> t" shows "first s = first t"
proof -
  { have "(next 0 s) 0 = s 0" by auto
    hence "(\<natural> s) 0 = s 0" by (simp add: collapse_def)}
  moreover
  { have "(next 0 t) 0 = t 0" by auto
    hence "(\<natural> t) 0 = t 0" by (simp add: collapse_def)}
  moreover   
  { from H have "\<forall> n. (\<natural> s) n = (\<natural> t) n" by (simp add: seqsimilar_def)
    hence "(\<natural> s) 0 = (\<natural> t) 0" by auto }
  ultimately show ?thesis by (auto simp add: first_def)
qed

lemma sim_first2: assumes H: "s \<approx> t" shows "s 0 = t 0"
proof -
  from H have "first s = first t" by (rule sim_first)
  thus ?thesis by (simp add: first_def)
qed

lemma tail_sim_second: assumes H: "tail s \<approx> tail t" shows "second s = second t"
proof -
  from H have "first (tail s) = first (tail t)" by (simp add: sim_first)
  thus "second s = second t" by (simp add: first_tail_second)
qed

lemma seqsim_empty_empty: assumes H1: "s \<approx> t" and H2: "emptyseq s" shows "emptyseq t"
proof (rule collapse_empty_empty, unfold emptyseq_def,rule allI)
  fix n
  from H2 have "(next n s) = s" by (rule next_empty)
  hence g1: "(next n s) 0 = s 0" by simp
  from H1 have  "\<forall> n. (\<natural> s) n = (\<natural> t) n" by (unfold seqsimilar_def)
  hence "(\<natural> s) n = (\<natural> t) n" ..
  hence "(next n s) 0 = (next n t) 0" by (unfold collapse_def)
  with g1 have "s 0 = (next n t) 0" by simp
  hence "(next n t) 0 = s 0" ..
  with H1 have "(next n t) 0 = t 0" by (simp add: sim_first2)
  thus "(\<natural> t) n = (\<natural> t) 0" by (auto simp add: collapse_def)
qed

lemma seq_empty_eq: assumes H1: "s 0 = t 0"
                      and   H2: "emptyseq s"
                      and   H3: "emptyseq t"
                     shows  "s = t"
proof -
 from H2 have a1: "\<forall> i. s i = s 0" by (unfold emptyseq_def)
 from H3 have a2: "\<forall> j. t j = t 0" by (unfold emptyseq_def)
 have "\<And> x. s x = t x"
 proof -
  fix x
  show "s x = t x"
  proof -
    fix i
    from a1 have a1a: "s i = s 0" ..
    with H1 have a1b: "s i = t 0" by simp
    from a2 have a2a: "t i = t 0" ..
    with a1b show "s i = t i" by simp
  qed
 qed
 thus "s = t" by (rule ext)
qed

lemma coleq_seqsim: "(\<natural> s = \<natural> t) = (s \<approx> t)"
proof (rule iffI)
  assume "\<natural> s = \<natural> t" thus "s \<approx> t" by (auto simp add: collapse_def seqsimilar_def)
next
  assume "s \<approx> t" thus "\<natural> s = \<natural> t" by (auto simp add: collapse_def seqsimilar_def)
qed

lemma seqsim_notempty_notempty: assumes H1: "s \<approx> t" and H2: "notemptyseq s" shows "notemptyseq t"
proof (rule collapse_notempty_notempty, unfold notemptyseq_def)
  from H1 have g1: "\<natural> s = \<natural> t" by (simp add: coleq_seqsim)
  from H2 have "notemptyseq (\<natural> s)" by (rule notempty_collapse_notempty)
  hence "\<exists>i. (\<natural> s) i \<noteq> (\<natural> s) 0" by (unfold notemptyseq_def)
  with g1 show "\<exists>i. (\<natural> t) i \<noteq> (\<natural> t) 0" by auto
qed

lemma seqsim_notstutstep: assumes H: "\<not> (stutstep s n)" shows "(s |\<^sub>s (Suc n)) \<approx> nextsuffix (s |\<^sub>s n)"
proof -
  have "s |\<^sub>s (Suc n) \<approx> s |\<^sub>s (Suc n)" by (rule seqsim_refl)
  with H show ?thesis by (auto simp add: notstutstep_nextsuffix1)
qed

lemma stut_nextsuf_suc: assumes H: "stutstep s n" shows "nextsuffix (s |\<^sub>s n) = nextsuffix (s |\<^sub>s (Suc n))"
proof (cases "emptyseq (s |\<^sub>s n)")
  assume a1: "emptyseq (s |\<^sub>s n)"
  have a1': "emptyseq (s |\<^sub>s Suc n)" by (rule suc_empty)
  from a1 have "nextnat (s |\<^sub>s n) = 0" by (simp add: nextnat_def)
  hence g1: "nextsuffix (s |\<^sub>s n) = (s |\<^sub>s n)" by (auto simp add: nextsuffix_def suffix_zero)
  from a1' have "nextnat (s |\<^sub>s Suc n) = 0" by (simp add: nextnat_def)
  hence g2: "nextsuffix (s |\<^sub>s Suc n) = (s |\<^sub>s Suc n)" by (auto simp add: nextsuffix_def suffix_zero)  
  have "(s |\<^sub>s n) = (s |\<^sub>s Suc n)"
  proof
    fix x
    show "(s |\<^sub>s n) x = (s |\<^sub>s Suc n) x"
    proof (unfold suffix_def)
      from a1 have "\<forall> i. (s |\<^sub>s n) i = (s |\<^sub>s n) 0" by (unfold emptyseq_def)
      hence a2: "\<forall> i. s (i + n) = s n" by (auto simp add: suffix_def)
      from a2 have "s (x + n) = s n" ..
      also from a2 have "s (Suc x + n) = s n" ..
      hence "s (x + Suc n) = s n" by auto
      ultimately show "s (x + n) = s (x + Suc n)" by simp
    qed
  qed
  with g1 g2 show ?thesis by auto
next
  assume a1: "\<not> emptyseq (s |\<^sub>s n)"
  hence "notemptyseq (s |\<^sub>s n)" by (simp add: seq_not_empty_notempty)
  with H have  "notemptyseq (s |\<^sub>s Suc n)" by (simp add: stutstep_notempty_notempty)
  hence a1': "\<not> emptyseq (s |\<^sub>s Suc n)" by (simp add: seq_not_empty_notempty)
  show ?thesis
  proof (unfold nextsuffix_def)
    from H a1 have "(nextnat (s |\<^sub>s n)) =  Suc (nextnat (s |\<^sub>s Suc n))"
      by (auto simp add: stutstep_notempty_sucnextnat)
    hence "(s |\<^sub>s n) |\<^sub>s (nextnat (s |\<^sub>s n)) = (s |\<^sub>s n) |\<^sub>s (Suc (nextnat (s |\<^sub>s Suc n)))" by auto
    hence "(s |\<^sub>s n) |\<^sub>s (nextnat (s |\<^sub>s n)) = (s |\<^sub>s n) |\<^sub>s (1 + (nextnat (s |\<^sub>s Suc n)))" by simp
    hence "(s |\<^sub>s n) |\<^sub>s (nextnat (s |\<^sub>s n)) = ((s |\<^sub>s n) |\<^sub>s 1) |\<^sub>s (nextnat (s |\<^sub>s Suc n))" by (auto simp add: suffix_plus)
    thus "(s |\<^sub>s n) |\<^sub>s (nextnat (s |\<^sub>s n)) = (s |\<^sub>s Suc n) |\<^sub>s (nextnat (s |\<^sub>s Suc n))" by (auto simp add: suffix_plus)
  qed
qed

lemma seqsim_suffix_seqsim: assumes H: "s \<approx> t" shows "nextsuffix s \<approx> nextsuffix t"
proof (unfold seqsimilar_def collapse_def, rule allI)
  fix n
  { from H have "\<forall> n. (\<natural> s) n = (\<natural> t) n" by (unfold seqsimilar_def)
    hence "\<forall> n. (next n s) 0 = (next n t) 0" by (simp add: collapse_def)
    hence "(next (Suc n) s) 0 = (next (Suc n) t) 0" ..  }
  moreover
  { have "nextsuffix (next n s) = next (Suc n) s" by auto 
    hence "next n (nextsuffix s) = next (Suc n) s" by (simp add: next_suffix_com) }
  moreover
  { have "nextsuffix (next n t) = next (Suc n) t" by auto 
    hence "next n (nextsuffix t) = next (Suc n) t" by (simp add: next_suffix_com) }
  ultimately show "next n (nextsuffix s) 0 = next n (nextsuffix t) 0" by auto
qed

lemma seqsim_stutstep: assumes H: "stutstep s n" shows "(s |\<^sub>s (Suc n)) \<approx> (s |\<^sub>s n)" (is "?sn \<approx> ?s")
proof (unfold seqsimilar_def collapse_def,rule allI)
  fix m
  show "next m (s |\<^sub>s Suc n) 0 = next m (s |\<^sub>s n) 0"
  proof (cases m)
    assume a2: "m=0"
    with H have "(s |\<^sub>s Suc n) 0 = (s |\<^sub>s n) 0"
      by (auto simp add: suffix_def stutstep_def)
    with a2 show "next m (s |\<^sub>s Suc n) 0 = next m (s |\<^sub>s n) 0" by auto
  next
    fix k
    assume a2: "m = Suc k"
    { from a2 have "next m (s |\<^sub>s Suc n) = nextsuffix (next k  (s |\<^sub>s Suc n))" by auto
      hence "next m (s |\<^sub>s Suc n) = next k (nextsuffix  (s |\<^sub>s Suc n))" 
	by (simp add: next_suffix_com) 
      with H have "next m (s |\<^sub>s Suc n) = next k (nextsuffix  (s |\<^sub>s n))" by (simp add: stut_nextsuf_suc)}
    moreover
     { from a2 have "next m (s |\<^sub>s n) = nextsuffix (next k  (s |\<^sub>s n))" by auto
      hence "next m (s |\<^sub>s n) = next k (nextsuffix  (s |\<^sub>s n))" 
	by (simp add: next_suffix_com) }   
    ultimately show "next m (s |\<^sub>s Suc n) 0 = next m (s |\<^sub>s n) 0" by simp
  qed
qed

lemma addfeqstut: assumes H: "s = first t"
                    shows    "stutstep (s ## t) 0"
using H
by (auto simp add: first_def stutstep_def app_def suffix_def)

lemma addfeqsim: assumes H: "s = first t"
                    shows    "(s ## t) \<approx> t"
proof -
  from H have "stutstep (s ## t) 0"
    by (rule addfeqstut)
  hence "((s ## t) |\<^sub>s (Suc 0)) \<approx> ((s ## t) |\<^sub>s 0)"
    by (rule seqsim_stutstep)
  hence "tail (s ## t) \<approx> (s ## t)"
    by (auto simp add: suffix_def tail_def)
  hence "t \<approx> (s ## t)" 
    by (auto simp add: tail_def app_def suffix_def)
  thus ?thesis by (rule seqsim_sym)
qed

lemma addfirststut: assumes H: "first s = second s"
                    shows    "s \<approx> tail s"
proof -
  have g1: "(first s) ## (tail s) = s" by (rule seq_app_first_tail)
  from H have "(first s) = first (tail s)"
    by (auto simp add: first_def second_def tail_def suffix_def)
  hence "(first s) ## (tail s) \<approx> (tail s)" by (rule addfeqsim)
  with g1 show ?thesis by auto
qed


lemma app_seqsimilar: assumes h1: "s \<approx> t"
        shows     "(x ## s) \<approx> (x ## t)"
proof (unfold seqsimilar_def, rule allI)
  fix n
  show "\<natural> (x ## s) n = \<natural> (x ## t) n"
  proof (cases "stutstep (x ## s) 0")
    assume a1: "stutstep (x ## s) 0"
    from h1 have "first s = first t" by (rule sim_first)
    with a1 have a2: "stutstep (x ## t) 0"
      by (auto simp add: stutstep_def first_def suffix_def app_def)
    from a1 have "((x ## s) |\<^sub>s (Suc 0)) \<approx> ((x ## s) |\<^sub>s 0)"
      by (rule seqsim_stutstep)
    hence "tail (x ## s) \<approx> (x ## s)" by (auto simp add: tail_def suffix_def)
    hence g1: "s \<approx> (x ## s)" by (auto simp add: app_def tail_def suffix_def)
    from a2 have "((x ## t) |\<^sub>s (Suc 0)) \<approx> ((x ## t) |\<^sub>s 0)"
      by (rule seqsim_stutstep)
    hence "tail (x ## t) \<approx> (x ## t)" by (auto simp add: tail_def suffix_def)
    hence g2: "t \<approx> (x ## t)" by (auto simp add: app_def tail_def suffix_def)
    from h1 g2 have "s \<approx> (x ## t)" by (rule seqsim_trans)
    from this[THEN seqsim_sym] g1 have "(x ## s) \<approx> (x ## t)"
      by (rule seqsim_sym[OF seqsim_trans])
    hence "\<forall> n. \<natural> (x ## s) n = \<natural> (x ## t) n" by (unfold seqsimilar_def)
    thus ?thesis ..
  next
    assume a1: "\<not> stutstep (x ## s) 0"
    from h1 have "first s = first t" by (rule sim_first)
    with a1 have a2: "\<not> stutstep (x ## t) 0"
      by (auto simp add: stutstep_def first_def suffix_def app_def)
    from a1 have "((x ## s) |\<^sub>s (Suc 0)) \<approx> nextsuffix ((x ## s) |\<^sub>s 0)"
      by (rule seqsim_notstutstep)
    hence "(tail (x ## s)) \<approx> nextsuffix (x ## s)" 
      by (auto simp add: tail_def suffix_zero)
    hence g1: "s \<approx> nextsuffix (x ## s)" by (auto simp add: seq_app_tail)
    from a2 have "((x ## t) |\<^sub>s (Suc 0)) \<approx> nextsuffix ((x ## t) |\<^sub>s 0)"
      by (rule seqsim_notstutstep)
    hence "(tail (x ## t)) \<approx> nextsuffix (x ## t)" 
      by (auto simp add: tail_def suffix_zero)
    hence g2: "t \<approx> nextsuffix (x ## t)" by (auto simp add: seq_app_tail)
    with h1 have "s \<approx> nextsuffix (x ## t)" by (rule seqsim_trans)
    from this[THEN seqsim_sym] g1 have g3: "nextsuffix (x ## s) \<approx> nextsuffix (x ## t)"
      by (rule seqsim_sym[OF seqsim_trans])
    hence "\<forall> n. \<natural>(nextsuffix (x ## s)) n = \<natural>(nextsuffix (x ## t)) n"
      by (unfold seqsimilar_def)
    hence g3': "\<forall> n. next n (nextsuffix (x ## s)) 0 =  next n (nextsuffix (x ## t)) 0"
      by (unfold collapse_def)
    show ?thesis
    proof (unfold collapse_def)
      show "next n (x ## s) 0 = next n (x ## t) 0"
      proof (induct n)
	show "next 0 (x ## s) 0 = next 0 (x ## t) 0"
	  by (auto simp add: app_def)
      next
	fix m
	assume a1: "next m (x ## s) 0 = next m (x ## t) 0"
	from g3' have "next m (nextsuffix (x ## s)) 0 =  next m (nextsuffix (x ## t)) 0" ..
	hence "nextsuffix (next m (x ## s)) 0 = nextsuffix (next m (x ## t)) 0"
	  by (simp add: next_suffix_com)
	thus "next (Suc m) (x ## s) 0 = next (Suc m) (x ## t) 0"
	  by (simp add: next_suc_suffix) 
      qed
    qed
  qed
qed

lemma simstep_disj1: assumes H: "s \<approx> t" shows "\<forall> n. \<exists> m. ((s |\<^sub>s n) \<approx> (t |\<^sub>s m))"
proof
  fix n
  show "\<exists> m. ((s |\<^sub>s n) \<approx> (t |\<^sub>s m))"
  proof (induct n)
    have "((s |\<^sub>s 0) \<approx> (t |\<^sub>s 0))" by (auto simp add: suffix_zero)
    thus "\<exists> m. ((s |\<^sub>s 0) \<approx> (t |\<^sub>s m))" ..
  next
    fix n
    assume a1: "\<exists> m. ((s |\<^sub>s n) \<approx> (t |\<^sub>s m))"
    then obtain m where a1': "((s |\<^sub>s n) \<approx> (t |\<^sub>s m))" ..
    show "\<exists> m. ((s |\<^sub>s (Suc n)) \<approx> (t |\<^sub>s m))"
    proof (cases "stutstep s n")
      assume a2: "stutstep s n"
      hence a2': "(s |\<^sub>s (Suc n)) \<approx> (s |\<^sub>s n)" by (rule seqsim_stutstep)
      from a2' a1' have "((s |\<^sub>s (Suc n)) \<approx> (t |\<^sub>s m))" by (rule seqsim_trans)
      thus ?thesis by auto
    next
      fix k
      assume a2: "\<not> stutstep s n"
      hence "(s |\<^sub>s (Suc n)) \<approx> nextsuffix (s |\<^sub>s n)" by (rule seqsim_notstutstep)
      also from a1' have "nextsuffix (s |\<^sub>s n) \<approx> nextsuffix (t |\<^sub>s m)" by (simp add: seqsim_suffix_seqsim)
      ultimately have "(s |\<^sub>s (Suc n)) \<approx> nextsuffix (t |\<^sub>s m)" by (rule seqsim_trans)
      thm "nextsuffix_def"
      hence "(s |\<^sub>s (Suc n)) \<approx> (t |\<^sub>s m) |\<^sub>s (nextnat (t |\<^sub>s m))" by (unfold nextsuffix_def)
      hence "(s |\<^sub>s (Suc n)) \<approx> t |\<^sub>s m |\<^sub>s (nextnat (t |\<^sub>s m))" by simp
      hence "(s |\<^sub>s (Suc n)) \<approx> t |\<^sub>s (m + (nextnat (t |\<^sub>s m)))" by (simp add: suffix_plus_com)
      thus "\<exists> m. (s |\<^sub>s (Suc n)) \<approx> t |\<^sub>s m" ..
    qed
  qed
qed

lemma nextnat_le_seqsim: "n < nextnat s \<longrightarrow> s \<approx> (s |\<^sub>s n)"
proof (cases "emptyseq s")
  assume "emptyseq s"
  hence "nextnat s = 0" by (simp add: nextnat_def)
  thus ?thesis by auto
next
  assume a1: "\<not> emptyseq s"
  show ?thesis
  proof (induct n)
    show "0 < nextnat s \<longrightarrow> s \<approx> (s |\<^sub>s 0)" 
      by (simp add: suffix_zero seqsim_refl)
  next
    fix n
    assume a2: "n < nextnat s \<longrightarrow> s \<approx> (s |\<^sub>s n)"
    show "(Suc n) < nextnat s \<longrightarrow> s \<approx> (s |\<^sub>s (Suc n))"
    proof
      thm "nextnat_le_unch"
      assume a3: "Suc n < nextnat s"
      hence g1: "s (Suc n) = s 0" by (rule nextnat_le_unch)
      from a3 have a3': "n < nextnat s" by simp
      hence "s n = s 0" by (rule nextnat_le_unch)
      with g1 have "stutstep s n" by (simp add: stutstep_def)
      hence g2: "(s |\<^sub>s n) \<approx> (s |\<^sub>s (Suc n))" by (rule seqsim_stutstep[THEN seqsim_sym])
      from a3' a2 have g3: "s \<approx> (s |\<^sub>s n)" by auto
      from g3 g2 show "s \<approx> (s |\<^sub>s (Suc n))" by (rule seqsim_trans)
    qed
  qed
qed

lemma seqsim_prev_nextnat: "s \<approx> s |\<^sub>s ((nextnat s)-(1::nat))"
proof (cases "emptyseq s")
  assume a1: "emptyseq s"
  hence "nextnat s = 0" by (simp add: nextnat_def)
  hence "(nextnat s)-(1::nat) = 0" by auto
  hence "s |\<^sub>s ((nextnat s)-(1::nat)) = s |\<^sub>s 0" by simp
  thus ?thesis by (simp add: seqsim_refl)
next
  assume a1': "\<not> emptyseq s"
  hence "nextnat s > 0" by (rule nextnat_empty_gzero)
  hence "(nextnat s)-(1::nat) < nextnat s" by auto
  thus ?thesis by (simp add: nextnat_le_seqsim)
qed

lemma gzero_sucpreveq: assumes H: "m > 0" shows "m = Suc (m-(1::nat))"
proof -
  from H show ?thesis by arith
qed


theorem sim_step: assumes H: "s \<approx> t" 
  shows "\<forall> n. \<exists> m. ((s |\<^sub>s n) \<approx> (t |\<^sub>s m)) \<and> (((s |\<^sub>s Suc n) \<approx> (t |\<^sub>s Suc m)) \<or> ((s |\<^sub>s Suc n) \<approx> (t |\<^sub>s m)))"
proof
  fix n
  show "\<exists> m. ((s |\<^sub>s n) \<approx> (t |\<^sub>s m)) \<and> (((s |\<^sub>s Suc n) \<approx> (t |\<^sub>s Suc m)) \<or> ((s |\<^sub>s Suc n) \<approx> (t |\<^sub>s m)))"
  proof (induct n)
    show "\<exists> m. ((s |\<^sub>s 0) \<approx> (t |\<^sub>s m)) \<and> (((s |\<^sub>s Suc 0) \<approx> (t |\<^sub>s Suc m)) \<or> ((s |\<^sub>s Suc 0) \<approx> (t |\<^sub>s m)))"
    proof (cases "stutstep s 0")
      assume a1: "stutstep s 0"
      hence a2: "(s |\<^sub>s Suc 0) \<approx> (s |\<^sub>s 0)" by (rule seqsim_stutstep)
      hence a2': "(s |\<^sub>s Suc 0) \<approx> s" by (simp add: suffix_zero)
      with H have "(s |\<^sub>s 0) \<approx> t" by simp
      also from a2' H have "(s |\<^sub>s Suc 0) \<approx> t" by (rule seqsim_trans)
      ultimately have "((s |\<^sub>s 0) \<approx> t) \<and> ((s |\<^sub>s (Suc 0)) \<approx> t)" by auto
      hence  "((s |\<^sub>s 0) \<approx> (t |\<^sub>s 0)) \<and> ((s |\<^sub>s (Suc 0)) \<approx> (t |\<^sub>s 0))" by (simp add: suffix_zero)
      hence  "((s |\<^sub>s 0) \<approx> (t |\<^sub>s 0)) \<and> (((s |\<^sub>s Suc 0) \<approx> (t |\<^sub>s Suc 0)) \<or> ((s |\<^sub>s (Suc 0)) \<approx> (t |\<^sub>s 0)))" 
	by auto
      thus "\<exists> m. ((s |\<^sub>s 0) \<approx> (t |\<^sub>s m)) \<and> (((s |\<^sub>s Suc 0) \<approx> (t |\<^sub>s Suc m)) \<or> ((s |\<^sub>s Suc 0) \<approx> (t |\<^sub>s m)))" ..
    next
      assume a1: "\<not> stutstep s 0"
      hence "\<not> emptyseq (s |\<^sub>s 0)" by (rule stutnempty)
      hence "\<not> emptyseq s" by simp
      hence "notemptyseq s" by  (simp add: seq_not_empty_notempty)
      with H have "notemptyseq t" by (simp add: seqsim_notempty_notempty)
      hence a2: "\<not> emptyseq t" by (simp add: seq_not_empty_notempty)
      hence g2': "0 < nextnat t" by (rule nextnat_empty_gzero)
      have g3: "t \<approx> t |\<^sub>s ((nextnat t)-(1::nat))" by (rule seqsim_prev_nextnat)
      have "nextsuffix t = t |\<^sub>s (nextnat t)" by (simp add: nextsuffix_def)
      with g2' have g4: "nextsuffix t = t |\<^sub>s Suc ((nextnat t)-(1::nat))" by (simp add: gzero_sucpreveq)
      from H g3 have "s \<approx> t |\<^sub>s ((nextnat t)-(1::nat))" by (rule seqsim_trans)
      hence G1: "(s |\<^sub>s 0) \<approx> t |\<^sub>s ((nextnat t)-(1::nat))" by auto
      from a1 have "(s |\<^sub>s Suc 0) = nextsuffix (s |\<^sub>s 0)" by (rule notstutstep_nextsuffix1[THEN sym])
      hence G1': "(s |\<^sub>s Suc 0) = nextsuffix s" by simp
      from H have "nextsuffix s \<approx> nextsuffix t" by (rule seqsim_suffix_seqsim)
      with G1' g4 have "(s |\<^sub>s Suc 0) \<approx> t |\<^sub>s Suc ((nextnat t)-(1::nat))" by simp
      with G1 have "((s |\<^sub>s 0) \<approx> t |\<^sub>s ((nextnat t)-(1::nat))) \<and> ((s |\<^sub>s Suc 0) \<approx> t |\<^sub>s Suc ((nextnat t)-(1::nat)))"
	by simp
      hence "\<exists> m. ((s |\<^sub>s 0) \<approx> (t |\<^sub>s m)) \<and> ((s |\<^sub>s Suc 0) \<approx> (t |\<^sub>s Suc m))" ..
      thus "\<exists> m. ((s |\<^sub>s 0) \<approx> (t |\<^sub>s m)) \<and> (((s |\<^sub>s Suc 0) \<approx> (t |\<^sub>s Suc m)) \<or> ((s |\<^sub>s Suc 0) \<approx> (t |\<^sub>s m)))" by auto
    qed
  next
    fix n
    assume a1: "\<exists> m. ((s |\<^sub>s n) \<approx> (t |\<^sub>s m)) \<and> (((s |\<^sub>s Suc n) \<approx> (t |\<^sub>s Suc m)) \<or> ((s |\<^sub>s Suc n) \<approx> (t |\<^sub>s m)))"
    then obtain m where "((s |\<^sub>s n) \<approx> (t |\<^sub>s m)) \<and> (((s |\<^sub>s Suc n) \<approx> (t |\<^sub>s Suc m)) \<or> ((s |\<^sub>s Suc n) \<approx> (t |\<^sub>s m)))" ..
    thus "\<exists> m. ((s |\<^sub>s Suc n) \<approx> (t |\<^sub>s m)) \<and> (((s |\<^sub>s Suc (Suc n)) \<approx> (t |\<^sub>s Suc m)) \<or> ((s |\<^sub>s Suc (Suc n)) \<approx> (t |\<^sub>s m)))"
    proof
      assume b1: "(s |\<^sub>s n) \<approx> (t |\<^sub>s m)"
        and  b2: "((s |\<^sub>s Suc n) \<approx> (t |\<^sub>s Suc m)) \<or> ((s |\<^sub>s Suc n) \<approx> (t |\<^sub>s m))"
      from b2 show ?thesis
      proof
	assume b2: "((s |\<^sub>s Suc n) \<approx> (t |\<^sub>s Suc m))" (is "?s \<approx> ?t")
	show ?thesis
	proof (cases "stutstep s (Suc n)")
	  assume "stutstep s (Suc n)"
	  hence a2: "(s |\<^sub>s Suc (Suc n)) \<approx> (s |\<^sub>s (Suc n))" by (rule seqsim_stutstep)
	  from a2 b2 have "(s |\<^sub>s Suc (Suc n)) \<approx> (t |\<^sub>s Suc m)" by (rule seqsim_trans)
	  with b2 have "((s |\<^sub>s Suc n) \<approx> (t |\<^sub>s Suc m)) \<and> ((s |\<^sub>s Suc (Suc n)) \<approx> (t |\<^sub>s Suc m))" 
	    by auto
	  hence "\<exists> m. ((s |\<^sub>s Suc n) \<approx> (t |\<^sub>s m)) \<and> ((s |\<^sub>s Suc (Suc n)) \<approx> (t |\<^sub>s m))" ..
	  thus ?thesis by auto
	next
	  assume A1: "\<not>stutstep s (Suc n)"
	  hence "\<not> emptyseq (s |\<^sub>s Suc n)" by (rule stutnempty)
	  hence "notemptyseq (s |\<^sub>s Suc n)" by  (simp add: seq_not_empty_notempty)
	  with b2 have "notemptyseq (t |\<^sub>s Suc m)" by (simp add: seqsim_notempty_notempty)
	  hence a2: "\<not> emptyseq (t |\<^sub>s Suc m)" by (simp add: seq_not_empty_notempty)
	  hence g2': "0 < nextnat (t |\<^sub>s Suc m)" by (rule nextnat_empty_gzero)
	  have g3: "(t |\<^sub>s Suc m) \<approx> (t |\<^sub>s Suc m) |\<^sub>s ((nextnat (t |\<^sub>s Suc m))-(1::nat))" by (rule seqsim_prev_nextnat)
	  have "nextsuffix (t |\<^sub>s Suc m) = (t |\<^sub>s Suc m) |\<^sub>s (nextnat (t |\<^sub>s Suc m))" by (simp add: nextsuffix_def)
	  with g2' have g4: "nextsuffix (t |\<^sub>s Suc m) = (t |\<^sub>s Suc m) |\<^sub>s Suc ((nextnat (t |\<^sub>s Suc m))-(1::nat))" 
	    by (simp add: gzero_sucpreveq)
	  from b2 g3 have G1: "(s |\<^sub>s Suc n) \<approx> ((t |\<^sub>s Suc m) |\<^sub>s ((nextnat (t |\<^sub>s Suc m))-(1::nat)))" 
	    by (rule seqsim_trans)
	  from A1 have G1': "(s |\<^sub>s Suc (Suc n)) = nextsuffix (s |\<^sub>s Suc n)" 
	    by (rule notstutstep_nextsuffix1[THEN sym])
	  from b2 have "nextsuffix (s |\<^sub>s Suc n) \<approx> nextsuffix (t |\<^sub>s Suc m)" by (rule seqsim_suffix_seqsim)
	  with G1' g4 have "(s |\<^sub>s Suc (Suc n)) \<approx> (t |\<^sub>s Suc m) |\<^sub>s Suc ((nextnat (t |\<^sub>s Suc m))-(1::nat))" by simp
	  with G1 have "((s |\<^sub>s Suc n) \<approx> (t |\<^sub>s Suc m) |\<^sub>s ((nextnat (t |\<^sub>s Suc m))-(1::nat))) 
	    \<and> ((s |\<^sub>s Suc (Suc n)) \<approx>  (t |\<^sub>s Suc m) |\<^sub>s Suc ((nextnat  (t |\<^sub>s Suc m))-(1::nat)))"
	    by simp
	  with G1 have "((s |\<^sub>s Suc n) \<approx> t |\<^sub>s ((Suc m) + ((nextnat (t |\<^sub>s Suc m))-(1::nat))))
	    \<and> ((s |\<^sub>s Suc (Suc n)) \<approx>  t |\<^sub>s ((Suc m) + Suc ((nextnat  (t |\<^sub>s Suc m))-(1::nat))))"
	    by (simp add: suffix_plus_com)
	  hence  "((s |\<^sub>s Suc n) \<approx> (t |\<^sub>s ((Suc m) + ((nextnat (t |\<^sub>s Suc m))-(1::nat))) ))
	    \<and> ((s |\<^sub>s Suc (Suc n)) \<approx> (t |\<^sub>s  Suc ((Suc m) + ((nextnat (t |\<^sub>s Suc m))-(1::nat)))))"
	    by auto
	  hence "\<exists> m. ((s |\<^sub>s Suc n) \<approx> (t |\<^sub>s m)) \<and> ((s |\<^sub>s Suc (Suc n)) \<approx> (t |\<^sub>s Suc m))" by blast
	  thus "\<exists> m. ((s |\<^sub>s Suc n) \<approx> (t |\<^sub>s m)) 
	    \<and> (((s |\<^sub>s Suc (Suc n)) \<approx> (t |\<^sub>s Suc m)) \<or> ((s |\<^sub>s Suc (Suc n)) \<approx> (t |\<^sub>s m)))" by auto
	qed
      next
	assume b2: "((s |\<^sub>s Suc n) \<approx> (t |\<^sub>s m))"
	show ?thesis
	proof (cases "stutstep s (Suc n)")
	  assume "stutstep s (Suc n)"
	  hence a2: "(s |\<^sub>s Suc (Suc n)) \<approx> (s |\<^sub>s (Suc n))" by (rule seqsim_stutstep)
	  from a2 b2 have "(s |\<^sub>s Suc (Suc n)) \<approx> (t |\<^sub>s  m)" by (rule seqsim_trans)
	  with b2 have "((s |\<^sub>s Suc n) \<approx> (t |\<^sub>s m)) \<and> ((s |\<^sub>s Suc (Suc n)) \<approx> (t |\<^sub>s  m))" 
	    by auto
	  hence "\<exists> m. ((s |\<^sub>s Suc n) \<approx> (t |\<^sub>s m)) \<and> ((s |\<^sub>s Suc (Suc n)) \<approx> (t |\<^sub>s m))" ..
	  thus ?thesis by auto
	next
	  assume A1: "\<not>stutstep s (Suc n)"
	  hence "\<not> emptyseq (s |\<^sub>s Suc n)" by (rule stutnempty)
	  hence "notemptyseq (s |\<^sub>s Suc n)" by  (simp add: seq_not_empty_notempty)
	  with b2 have "notemptyseq (t |\<^sub>s m)" by (simp add: seqsim_notempty_notempty)
	  hence a2: "\<not> emptyseq (t |\<^sub>s m)" by (simp add: seq_not_empty_notempty)
	  hence g2': "0 < nextnat (t |\<^sub>s m)" by (rule nextnat_empty_gzero)
	  have g3: "(t |\<^sub>s m) \<approx> (t |\<^sub>s m) |\<^sub>s ((nextnat (t |\<^sub>s m))-(1::nat))" by (rule seqsim_prev_nextnat)
	  have "nextsuffix (t |\<^sub>s m) = (t |\<^sub>s m) |\<^sub>s (nextnat (t |\<^sub>s m))" by (simp add: nextsuffix_def)
	  with g2' have g4: "nextsuffix (t |\<^sub>s m) = (t |\<^sub>s m) |\<^sub>s Suc ((nextnat (t |\<^sub>s m))-(1::nat))" 
	    by (simp add: gzero_sucpreveq)
	  from b2 g3 have G1: "(s |\<^sub>s Suc n) \<approx> ((t |\<^sub>s m) |\<^sub>s ((nextnat (t |\<^sub>s m))-(1::nat)))" 
	    by (rule seqsim_trans)
	  from A1 have G1': "(s |\<^sub>s Suc (Suc n)) = nextsuffix (s |\<^sub>s Suc n)" 
	    by (rule notstutstep_nextsuffix1[THEN sym])
	  from b2 have "nextsuffix (s |\<^sub>s Suc n) \<approx> nextsuffix (t |\<^sub>s m)" by (rule seqsim_suffix_seqsim)
	  with G1' g4 have "(s |\<^sub>s Suc (Suc n)) \<approx> (t |\<^sub>s m) |\<^sub>s Suc ((nextnat (t |\<^sub>s m))-(1::nat))" by simp
	  with G1 have "((s |\<^sub>s Suc n) \<approx> (t |\<^sub>s m) |\<^sub>s ((nextnat (t |\<^sub>s m))-(1::nat))) 
	    \<and> ((s |\<^sub>s Suc (Suc n)) \<approx>  (t |\<^sub>s m) |\<^sub>s Suc ((nextnat  (t |\<^sub>s m))-(1::nat)))"
	    by simp
	  with G1 have "((s |\<^sub>s Suc n) \<approx> t |\<^sub>s (m + ((nextnat (t |\<^sub>s m))-(1::nat))))
	    \<and> ((s |\<^sub>s Suc (Suc n)) \<approx>  t |\<^sub>s (m + Suc ((nextnat  (t |\<^sub>s m))-(1::nat))))"
	    by (simp add: suffix_plus_com)
	  hence  "((s |\<^sub>s Suc n) \<approx> (t |\<^sub>s (m + ((nextnat (t |\<^sub>s m))-(1::nat))) ))
	    \<and> ((s |\<^sub>s Suc (Suc n)) \<approx> (t |\<^sub>s  Suc (m + ((nextnat (t |\<^sub>s m))-(1::nat)))))"
	    by auto
	  hence "\<exists> m. ((s |\<^sub>s Suc n) \<approx> (t |\<^sub>s m)) \<and> ((s |\<^sub>s Suc (Suc n)) \<approx> (t |\<^sub>s Suc m))" by blast
	  thus "\<exists> m. ((s |\<^sub>s Suc n) \<approx> (t |\<^sub>s m)) 
	    \<and> (((s |\<^sub>s Suc (Suc n)) \<approx> (t |\<^sub>s Suc m)) \<or> ((s |\<^sub>s Suc (Suc n)) \<approx> (t |\<^sub>s m)))" by auto
	qed
      qed
    qed
  qed
qed

end