theory ArchVSpace_AI

lemma vs_lookup_pages1_rtrancl_iterations:
  "(tup, tup') \<in> (vs_lookup_pages1 s)\<^sup>*
    \<Longrightarrow> (length (fst tup) \<le> length (fst tup')) \<and>
       (tup, tup') \<in> ((vs_lookup_pages1 s)
           ^^ (length (fst tup') - length (fst tup)))" apply (erule rtrancl_induct) apply simp apply (elim conjE) apply (subgoal_tac "length (fst z) = Suc (length (fst y))") apply (simp add: Suc_diff_le) apply (erule(1) relcompI) apply (clarsimp simp: vs_lookup_pages1_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (tup, tup') \<in> (vs_lookup_pages1 s)\<^sup>* \<Longrightarrow> length (fst tup) \<le> length (fst tup') \<and> (tup, tup') \<in> vs_lookup_pages1 s ^^ (length (fst tup') - length (fst tup)) proof (prove)
goal (2 subgoals):
 1. length (fst tup) \<le> length (fst tup) \<and> (tup, tup) \<in> vs_lookup_pages1 s ^^ (length (fst tup) - length (fst tup))
 2. \<And>y z. \<lbrakk>(tup, y) \<in> (vs_lookup_pages1 s)\<^sup>*; (y, z) \<in> vs_lookup_pages1 s; length (fst tup) \<le> length (fst y) \<and> (tup, y) \<in> vs_lookup_pages1 s ^^ (length (fst y) - length (fst tup))\<rbrakk> \<Longrightarrow> length (fst tup) \<le> length (fst z) \<and> (tup, z) \<in> vs_lookup_pages1 s ^^ (length (fst z) - length (fst tup)) proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(tup, y) \<in> (vs_lookup_pages1 s)\<^sup>*; (y, z) \<in> vs_lookup_pages1 s; length (fst tup) \<le> length (fst y) \<and> (tup, y) \<in> vs_lookup_pages1 s ^^ (length (fst y) - length (fst tup))\<rbrakk> \<Longrightarrow> length (fst tup) \<le> length (fst z) \<and> (tup, z) \<in> vs_lookup_pages1 s ^^ (length (fst z) - length (fst tup)) proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(tup, y) \<in> (vs_lookup_pages1 s)\<^sup>*; (y, z) \<in> vs_lookup_pages1 s; length (fst tup) \<le> length (fst y); (tup, y) \<in> vs_lookup_pages1 s ^^ (length (fst y) - length (fst tup))\<rbrakk> \<Longrightarrow> length (fst tup) \<le> length (fst z) \<and> (tup, z) \<in> vs_lookup_pages1 s ^^ (length (fst z) - length (fst tup)) proof (prove)
goal (2 subgoals):
 1. \<And>y z. \<lbrakk>(tup, y) \<in> (vs_lookup_pages1 s)\<^sup>*; (y, z) \<in> vs_lookup_pages1 s; length (fst tup) \<le> length (fst y); (tup, y) \<in> vs_lookup_pages1 s ^^ (length (fst y) - length (fst tup)); length (fst z) = Suc (length (fst y))\<rbrakk> \<Longrightarrow> length (fst tup) \<le> length (fst z) \<and> (tup, z) \<in> vs_lookup_pages1 s ^^ (length (fst z) - length (fst tup))
 2. \<And>y z. \<lbrakk>(tup, y) \<in> (vs_lookup_pages1 s)\<^sup>*; (y, z) \<in> vs_lookup_pages1 s; length (fst tup) \<le> length (fst y); (tup, y) \<in> vs_lookup_pages1 s ^^ (length (fst y) - length (fst tup))\<rbrakk> \<Longrightarrow> length (fst z) = Suc (length (fst y)) proof (prove)
goal (2 subgoals):
 1. \<And>y z. \<lbrakk>(tup, y) \<in> (vs_lookup_pages1 s)\<^sup>*; (y, z) \<in> vs_lookup_pages1 s; length (fst tup) \<le> length (fst y); (tup, y) \<in> vs_lookup_pages1 s ^^ (length (fst y) - length (fst tup)); length (fst z) = Suc (length (fst y))\<rbrakk> \<Longrightarrow> (tup, z) \<in> vs_lookup_pages1 s ^^ (length (fst y) - length (fst tup)) O vs_lookup_pages1 s
 2. \<And>y z. \<lbrakk>(tup, y) \<in> (vs_lookup_pages1 s)\<^sup>*; (y, z) \<in> vs_lookup_pages1 s; length (fst tup) \<le> length (fst y); (tup, y) \<in> vs_lookup_pages1 s ^^ (length (fst y) - length (fst tup))\<rbrakk> \<Longrightarrow> length (fst z) = Suc (length (fst y)) proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(tup, y) \<in> (vs_lookup_pages1 s)\<^sup>*; (y, z) \<in> vs_lookup_pages1 s; length (fst tup) \<le> length (fst y); (tup, y) \<in> vs_lookup_pages1 s ^^ (length (fst y) - length (fst tup))\<rbrakk> \<Longrightarrow> length (fst z) = Suc (length (fst y)) proof (prove)
goal:
No subgoals!