[STATEMENT]
lemma Use_value_change_implies_DynPDG_ddep_edge:
  assumes "n -as\<rightarrow>* n'" and "V \<in> Use n'" and "preds (kinds as) s"
  and "preds (kinds as) s'" and "state_val s V = state_val s' V"
  and "state_val (transfers (kinds as) s) V \<noteq>
             state_val (transfers (kinds as) s') V"
  obtains as' a as'' where "as = as'@a#as''"
  and "sourcenode a -{V}a#as''\<rightarrow>\<^sub>d\<^sub>d n'"
  and "state_val (transfers (kinds as) s) V =
       state_val (transfers (kinds (as'@[a])) s) V"
  and "state_val (transfers (kinds as) s') V =
       state_val (transfers (kinds (as'@[a])) s') V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>as' a as''. \<lbrakk>as = as' @ a # as''; sourcenode a -{V}a # as''\<rightarrow>\<^sub>d\<^sub>d n'; state_val (transfers (kinds as) s) V = state_val (transfers (kinds (as' @ [a])) s) V; state_val (transfers (kinds as) s') V = state_val (transfers (kinds (as' @ [a])) s') V\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof(atomize_elim)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>as' a as''. as = as' @ a # as'' \<and> sourcenode a -{V}a # as''\<rightarrow>\<^sub>d\<^sub>d n' \<and> state_val (transfers (kinds as) s) V = state_val (transfers (kinds (as' @ [a])) s) V \<and> state_val (transfers (kinds as) s') V = state_val (transfers (kinds (as' @ [a])) s') V
[PROOF STEP]
show "\<exists>as' a as''. as = as'@a#as'' \<and>
                     sourcenode a -{V}a#as''\<rightarrow>\<^sub>d\<^sub>d n' \<and>
             state_val (transfers (kinds as) s) V =
             state_val (transfers (kinds (as'@[a])) s) V \<and>
             state_val (transfers (kinds as) s') V =
             state_val (transfers (kinds (as'@[a])) s') V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>as' a as''. as = as' @ a # as'' \<and> sourcenode a -{V}a # as''\<rightarrow>\<^sub>d\<^sub>d n' \<and> state_val (transfers (kinds as) s) V = state_val (transfers (kinds (as' @ [a])) s) V \<and> state_val (transfers (kinds as) s') V = state_val (transfers (kinds (as' @ [a])) s') V
[PROOF STEP]
proof(cases "\<forall>as' a as''. as = as'@a#as'' \<longrightarrow>
                 \<not> sourcenode a -{V}a#as''\<rightarrow>\<^sub>d\<^sub>d n'")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<forall>as' a as''. as = as' @ a # as'' \<longrightarrow> \<not> sourcenode a -{V}a # as''\<rightarrow>\<^sub>d\<^sub>d n' \<Longrightarrow> \<exists>as' a as''. as = as' @ a # as'' \<and> sourcenode a -{V}a # as''\<rightarrow>\<^sub>d\<^sub>d n' \<and> state_val (transfers (kinds as) s) V = state_val (transfers (kinds (as' @ [a])) s) V \<and> state_val (transfers (kinds as) s') V = state_val (transfers (kinds (as' @ [a])) s') V
 2. \<not> (\<forall>as' a as''. as = as' @ a # as'' \<longrightarrow> \<not> sourcenode a -{V}a # as''\<rightarrow>\<^sub>d\<^sub>d n') \<Longrightarrow> \<exists>as' a as''. as = as' @ a # as'' \<and> sourcenode a -{V}a # as''\<rightarrow>\<^sub>d\<^sub>d n' \<and> state_val (transfers (kinds as) s) V = state_val (transfers (kinds (as' @ [a])) s) V \<and> state_val (transfers (kinds as) s') V = state_val (transfers (kinds (as' @ [a])) s') V
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<forall>as' a as''. as = as' @ a # as'' \<longrightarrow> \<not> sourcenode a -{V}a # as''\<rightarrow>\<^sub>d\<^sub>d n'

goal (2 subgoals):
 1. \<forall>as' a as''. as = as' @ a # as'' \<longrightarrow> \<not> sourcenode a -{V}a # as''\<rightarrow>\<^sub>d\<^sub>d n' \<Longrightarrow> \<exists>as' a as''. as = as' @ a # as'' \<and> sourcenode a -{V}a # as''\<rightarrow>\<^sub>d\<^sub>d n' \<and> state_val (transfers (kinds as) s) V = state_val (transfers (kinds (as' @ [a])) s) V \<and> state_val (transfers (kinds as) s') V = state_val (transfers (kinds (as' @ [a])) s') V
 2. \<not> (\<forall>as' a as''. as = as' @ a # as'' \<longrightarrow> \<not> sourcenode a -{V}a # as''\<rightarrow>\<^sub>d\<^sub>d n') \<Longrightarrow> \<exists>as' a as''. as = as' @ a # as'' \<and> sourcenode a -{V}a # as''\<rightarrow>\<^sub>d\<^sub>d n' \<and> state_val (transfers (kinds as) s) V = state_val (transfers (kinds (as' @ [a])) s) V \<and> state_val (transfers (kinds as) s') V = state_val (transfers (kinds (as' @ [a])) s') V
[PROOF STEP]
with \<open>n -as\<rightarrow>* n'\<close> \<open>V \<in> Use n'\<close> \<open>preds (kinds as) s\<close> \<open>preds (kinds as) s'\<close>
[PROOF STATE]
proof (chain)
picking this:
n -as\<rightarrow>* n'
V \<in> Use n'
preds (kinds as) s
preds (kinds as) s'
\<forall>as' a as''. as = as' @ a # as'' \<longrightarrow> \<not> sourcenode a -{V}a # as''\<rightarrow>\<^sub>d\<^sub>d n'
[PROOF STEP]
have "state_val (transfers (kinds as) s) V = state_val s V"
      and "state_val (transfers (kinds as) s') V = state_val s' V"
[PROOF STATE]
proof (prove)
using this:
n -as\<rightarrow>* n'
V \<in> Use n'
preds (kinds as) s
preds (kinds as) s'
\<forall>as' a as''. as = as' @ a # as'' \<longrightarrow> \<not> sourcenode a -{V}a # as''\<rightarrow>\<^sub>d\<^sub>d n'

goal (1 subgoal):
 1. state_val (transfers (kinds as) s) V = state_val s V &&& state_val (transfers (kinds as) s') V = state_val s' V
[PROOF STEP]
by(auto intro:no_ddep_same_state)
[PROOF STATE]
proof (state)
this:
state_val (transfers (kinds as) s) V = state_val s V
state_val (transfers (kinds as) s') V = state_val s' V

goal (2 subgoals):
 1. \<forall>as' a as''. as = as' @ a # as'' \<longrightarrow> \<not> sourcenode a -{V}a # as''\<rightarrow>\<^sub>d\<^sub>d n' \<Longrightarrow> \<exists>as' a as''. as = as' @ a # as'' \<and> sourcenode a -{V}a # as''\<rightarrow>\<^sub>d\<^sub>d n' \<and> state_val (transfers (kinds as) s) V = state_val (transfers (kinds (as' @ [a])) s) V \<and> state_val (transfers (kinds as) s') V = state_val (transfers (kinds (as' @ [a])) s') V
 2. \<not> (\<forall>as' a as''. as = as' @ a # as'' \<longrightarrow> \<not> sourcenode a -{V}a # as''\<rightarrow>\<^sub>d\<^sub>d n') \<Longrightarrow> \<exists>as' a as''. as = as' @ a # as'' \<and> sourcenode a -{V}a # as''\<rightarrow>\<^sub>d\<^sub>d n' \<and> state_val (transfers (kinds as) s) V = state_val (transfers (kinds (as' @ [a])) s) V \<and> state_val (transfers (kinds as) s') V = state_val (transfers (kinds (as' @ [a])) s') V
[PROOF STEP]
with \<open>state_val s V = state_val s' V\<close>
      \<open>state_val (transfers (kinds as) s) V \<noteq> state_val (transfers (kinds as) s') V\<close>
[PROOF STATE]
proof (chain)
picking this:
state_val s V = state_val s' V
state_val (transfers (kinds as) s) V \<noteq> state_val (transfers (kinds as) s') V
state_val (transfers (kinds as) s) V = state_val s V
state_val (transfers (kinds as) s') V = state_val s' V
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
state_val s V = state_val s' V
state_val (transfers (kinds as) s) V \<noteq> state_val (transfers (kinds as) s') V
state_val (transfers (kinds as) s) V = state_val s V
state_val (transfers (kinds as) s') V = state_val s' V

goal (1 subgoal):
 1. \<exists>as' a as''. as = as' @ a # as'' \<and> sourcenode a -{V}a # as''\<rightarrow>\<^sub>d\<^sub>d n' \<and> state_val (transfers (kinds as) s) V = state_val (transfers (kinds (as' @ [a])) s) V \<and> state_val (transfers (kinds as) s') V = state_val (transfers (kinds (as' @ [a])) s') V
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>as' a as''. as = as' @ a # as'' \<and> sourcenode a -{V}a # as''\<rightarrow>\<^sub>d\<^sub>d n' \<and> state_val (transfers (kinds as) s) V = state_val (transfers (kinds (as' @ [a])) s) V \<and> state_val (transfers (kinds as) s') V = state_val (transfers (kinds (as' @ [a])) s') V

goal (1 subgoal):
 1. \<not> (\<forall>as' a as''. as = as' @ a # as'' \<longrightarrow> \<not> sourcenode a -{V}a # as''\<rightarrow>\<^sub>d\<^sub>d n') \<Longrightarrow> \<exists>as' a as''. as = as' @ a # as'' \<and> sourcenode a -{V}a # as''\<rightarrow>\<^sub>d\<^sub>d n' \<and> state_val (transfers (kinds as) s) V = state_val (transfers (kinds (as' @ [a])) s) V \<and> state_val (transfers (kinds as) s') V = state_val (transfers (kinds (as' @ [a])) s') V
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (\<forall>as' a as''. as = as' @ a # as'' \<longrightarrow> \<not> sourcenode a -{V}a # as''\<rightarrow>\<^sub>d\<^sub>d n') \<Longrightarrow> \<exists>as' a as''. as = as' @ a # as'' \<and> sourcenode a -{V}a # as''\<rightarrow>\<^sub>d\<^sub>d n' \<and> state_val (transfers (kinds as) s) V = state_val (transfers (kinds (as' @ [a])) s) V \<and> state_val (transfers (kinds as) s') V = state_val (transfers (kinds (as' @ [a])) s') V
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (\<forall>as' a as''. as = as' @ a # as'' \<longrightarrow> \<not> sourcenode a -{V}a # as''\<rightarrow>\<^sub>d\<^sub>d n')

goal (1 subgoal):
 1. \<not> (\<forall>as' a as''. as = as' @ a # as'' \<longrightarrow> \<not> sourcenode a -{V}a # as''\<rightarrow>\<^sub>d\<^sub>d n') \<Longrightarrow> \<exists>as' a as''. as = as' @ a # as'' \<and> sourcenode a -{V}a # as''\<rightarrow>\<^sub>d\<^sub>d n' \<and> state_val (transfers (kinds as) s) V = state_val (transfers (kinds (as' @ [a])) s) V \<and> state_val (transfers (kinds as) s') V = state_val (transfers (kinds (as' @ [a])) s') V
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> (\<forall>as' a as''. as = as' @ a # as'' \<longrightarrow> \<not> sourcenode a -{V}a # as''\<rightarrow>\<^sub>d\<^sub>d n')
[PROOF STEP]
obtain as' a as'' where [simp]:"as = as'@a#as''"
      and "sourcenode a -{V}a#as''\<rightarrow>\<^sub>d\<^sub>d n'"
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>as' a as''. as = as' @ a # as'' \<longrightarrow> \<not> sourcenode a -{V}a # as''\<rightarrow>\<^sub>d\<^sub>d n')

goal (1 subgoal):
 1. (\<And>as' a as''. \<lbrakk>as = as' @ a # as''; sourcenode a -{V}a # as''\<rightarrow>\<^sub>d\<^sub>d n'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
as = as' @ a # as''
sourcenode a -{V}a # as''\<rightarrow>\<^sub>d\<^sub>d n'

goal (1 subgoal):
 1. \<not> (\<forall>as' a as''. as = as' @ a # as'' \<longrightarrow> \<not> sourcenode a -{V}a # as''\<rightarrow>\<^sub>d\<^sub>d n') \<Longrightarrow> \<exists>as' a as''. as = as' @ a # as'' \<and> sourcenode a -{V}a # as''\<rightarrow>\<^sub>d\<^sub>d n' \<and> state_val (transfers (kinds as) s) V = state_val (transfers (kinds (as' @ [a])) s) V \<and> state_val (transfers (kinds as) s') V = state_val (transfers (kinds (as' @ [a])) s') V
[PROOF STEP]
from \<open>preds (kinds as) s\<close>
[PROOF STATE]
proof (chain)
picking this:
preds (kinds as) s
[PROOF STEP]
have "preds (kinds (a#as'')) (transfers (kinds as') s)"
[PROOF STATE]
proof (prove)
using this:
preds (kinds as) s

goal (1 subgoal):
 1. preds (kinds (a # as'')) (transfers (kinds as') s)
[PROOF STEP]
by(simp add:kinds_def preds_split)
[PROOF STATE]
proof (state)
this:
preds (kinds (a # as'')) (transfers (kinds as') s)

goal (1 subgoal):
 1. \<not> (\<forall>as' a as''. as = as' @ a # as'' \<longrightarrow> \<not> sourcenode a -{V}a # as''\<rightarrow>\<^sub>d\<^sub>d n') \<Longrightarrow> \<exists>as' a as''. as = as' @ a # as'' \<and> sourcenode a -{V}a # as''\<rightarrow>\<^sub>d\<^sub>d n' \<and> state_val (transfers (kinds as) s) V = state_val (transfers (kinds (as' @ [a])) s) V \<and> state_val (transfers (kinds as) s') V = state_val (transfers (kinds (as' @ [a])) s') V
[PROOF STEP]
with \<open>sourcenode a -{V}a#as''\<rightarrow>\<^sub>d\<^sub>d n'\<close>
[PROOF STATE]
proof (chain)
picking this:
sourcenode a -{V}a # as''\<rightarrow>\<^sub>d\<^sub>d n'
preds (kinds (a # as'')) (transfers (kinds as') s)
[PROOF STEP]
have all:
      "state_val (transfers (kinds (a#as'')) (transfers (kinds as') s)) V =
       state_val (transfer (kind a) (transfers (kinds as') s)) V"
[PROOF STATE]
proof (prove)
using this:
sourcenode a -{V}a # as''\<rightarrow>\<^sub>d\<^sub>d n'
preds (kinds (a # as'')) (transfers (kinds as') s)

goal (1 subgoal):
 1. state_val (transfers (kinds (a # as'')) (transfers (kinds as') s)) V = state_val (transfer (kind a) (transfers (kinds as') s)) V
[PROOF STEP]
by(auto dest!:DynPDG_ddep_edge_only_first_edge)
[PROOF STATE]
proof (state)
this:
state_val (transfers (kinds (a # as'')) (transfers (kinds as') s)) V = state_val (transfer (kind a) (transfers (kinds as') s)) V

goal (1 subgoal):
 1. \<not> (\<forall>as' a as''. as = as' @ a # as'' \<longrightarrow> \<not> sourcenode a -{V}a # as''\<rightarrow>\<^sub>d\<^sub>d n') \<Longrightarrow> \<exists>as' a as''. as = as' @ a # as'' \<and> sourcenode a -{V}a # as''\<rightarrow>\<^sub>d\<^sub>d n' \<and> state_val (transfers (kinds as) s) V = state_val (transfers (kinds (as' @ [a])) s) V \<and> state_val (transfers (kinds as) s') V = state_val (transfers (kinds (as' @ [a])) s') V
[PROOF STEP]
from \<open>preds (kinds as) s'\<close>
[PROOF STATE]
proof (chain)
picking this:
preds (kinds as) s'
[PROOF STEP]
have "preds (kinds (a#as'')) (transfers (kinds as') s')"
[PROOF STATE]
proof (prove)
using this:
preds (kinds as) s'

goal (1 subgoal):
 1. preds (kinds (a # as'')) (transfers (kinds as') s')
[PROOF STEP]
by(simp add:kinds_def preds_split)
[PROOF STATE]
proof (state)
this:
preds (kinds (a # as'')) (transfers (kinds as') s')

goal (1 subgoal):
 1. \<not> (\<forall>as' a as''. as = as' @ a # as'' \<longrightarrow> \<not> sourcenode a -{V}a # as''\<rightarrow>\<^sub>d\<^sub>d n') \<Longrightarrow> \<exists>as' a as''. as = as' @ a # as'' \<and> sourcenode a -{V}a # as''\<rightarrow>\<^sub>d\<^sub>d n' \<and> state_val (transfers (kinds as) s) V = state_val (transfers (kinds (as' @ [a])) s) V \<and> state_val (transfers (kinds as) s') V = state_val (transfers (kinds (as' @ [a])) s') V
[PROOF STEP]
with \<open>sourcenode a -{V}a#as''\<rightarrow>\<^sub>d\<^sub>d n'\<close>
[PROOF STATE]
proof (chain)
picking this:
sourcenode a -{V}a # as''\<rightarrow>\<^sub>d\<^sub>d n'
preds (kinds (a # as'')) (transfers (kinds as') s')
[PROOF STEP]
have all':
      "state_val (transfers (kinds (a#as'')) (transfers (kinds as') s')) V =
       state_val (transfer (kind a) (transfers (kinds as') s')) V"
[PROOF STATE]
proof (prove)
using this:
sourcenode a -{V}a # as''\<rightarrow>\<^sub>d\<^sub>d n'
preds (kinds (a # as'')) (transfers (kinds as') s')

goal (1 subgoal):
 1. state_val (transfers (kinds (a # as'')) (transfers (kinds as') s')) V = state_val (transfer (kind a) (transfers (kinds as') s')) V
[PROOF STEP]
by(auto dest!:DynPDG_ddep_edge_only_first_edge)
[PROOF STATE]
proof (state)
this:
state_val (transfers (kinds (a # as'')) (transfers (kinds as') s')) V = state_val (transfer (kind a) (transfers (kinds as') s')) V

goal (1 subgoal):
 1. \<not> (\<forall>as' a as''. as = as' @ a # as'' \<longrightarrow> \<not> sourcenode a -{V}a # as''\<rightarrow>\<^sub>d\<^sub>d n') \<Longrightarrow> \<exists>as' a as''. as = as' @ a # as'' \<and> sourcenode a -{V}a # as''\<rightarrow>\<^sub>d\<^sub>d n' \<and> state_val (transfers (kinds as) s) V = state_val (transfers (kinds (as' @ [a])) s) V \<and> state_val (transfers (kinds as) s') V = state_val (transfers (kinds (as' @ [a])) s') V
[PROOF STEP]
hence eq:"\<And>s. transfers (kinds as) s =
      transfers (kinds (a#as'')) (transfers (kinds as') s)"
[PROOF STATE]
proof (prove)
using this:
state_val (transfers (kinds (a # as'')) (transfers (kinds as') s')) V = state_val (transfer (kind a) (transfers (kinds as') s')) V

goal (1 subgoal):
 1. \<And>s. transfers (kinds as) s = transfers (kinds (a # as'')) (transfers (kinds as') s)
[PROOF STEP]
by(simp add:transfers_split[THEN sym] kinds_def)
[PROOF STATE]
proof (state)
this:
transfers (kinds as) ?s = transfers (kinds (a # as'')) (transfers (kinds as') ?s)

goal (1 subgoal):
 1. \<not> (\<forall>as' a as''. as = as' @ a # as'' \<longrightarrow> \<not> sourcenode a -{V}a # as''\<rightarrow>\<^sub>d\<^sub>d n') \<Longrightarrow> \<exists>as' a as''. as = as' @ a # as'' \<and> sourcenode a -{V}a # as''\<rightarrow>\<^sub>d\<^sub>d n' \<and> state_val (transfers (kinds as) s) V = state_val (transfers (kinds (as' @ [a])) s) V \<and> state_val (transfers (kinds as) s') V = state_val (transfers (kinds (as' @ [a])) s') V
[PROOF STEP]
with all
[PROOF STATE]
proof (chain)
picking this:
state_val (transfers (kinds (a # as'')) (transfers (kinds as') s)) V = state_val (transfer (kind a) (transfers (kinds as') s)) V
transfers (kinds as) ?s = transfers (kinds (a # as'')) (transfers (kinds as') ?s)
[PROOF STEP]
have "state_val (transfers (kinds as) s) V =
                   state_val (transfers (kinds (as'@[a])) s) V"
[PROOF STATE]
proof (prove)
using this:
state_val (transfers (kinds (a # as'')) (transfers (kinds as') s)) V = state_val (transfer (kind a) (transfers (kinds as') s)) V
transfers (kinds as) ?s = transfers (kinds (a # as'')) (transfers (kinds as') ?s)

goal (1 subgoal):
 1. state_val (transfers (kinds as) s) V = state_val (transfers (kinds (as' @ [a])) s) V
[PROOF STEP]
by(simp add:transfers_split kinds_def)
[PROOF STATE]
proof (state)
this:
state_val (transfers (kinds as) s) V = state_val (transfers (kinds (as' @ [a])) s) V

goal (1 subgoal):
 1. \<not> (\<forall>as' a as''. as = as' @ a # as'' \<longrightarrow> \<not> sourcenode a -{V}a # as''\<rightarrow>\<^sub>d\<^sub>d n') \<Longrightarrow> \<exists>as' a as''. as = as' @ a # as'' \<and> sourcenode a -{V}a # as''\<rightarrow>\<^sub>d\<^sub>d n' \<and> state_val (transfers (kinds as) s) V = state_val (transfers (kinds (as' @ [a])) s) V \<and> state_val (transfers (kinds as) s') V = state_val (transfers (kinds (as' @ [a])) s') V
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
state_val (transfers (kinds as) s) V = state_val (transfers (kinds (as' @ [a])) s) V

goal (1 subgoal):
 1. \<not> (\<forall>as' a as''. as = as' @ a # as'' \<longrightarrow> \<not> sourcenode a -{V}a # as''\<rightarrow>\<^sub>d\<^sub>d n') \<Longrightarrow> \<exists>as' a as''. as = as' @ a # as'' \<and> sourcenode a -{V}a # as''\<rightarrow>\<^sub>d\<^sub>d n' \<and> state_val (transfers (kinds as) s) V = state_val (transfers (kinds (as' @ [a])) s) V \<and> state_val (transfers (kinds as) s') V = state_val (transfers (kinds (as' @ [a])) s') V
[PROOF STEP]
from eq all'
[PROOF STATE]
proof (chain)
picking this:
transfers (kinds as) ?s = transfers (kinds (a # as'')) (transfers (kinds as') ?s)
state_val (transfers (kinds (a # as'')) (transfers (kinds as') s')) V = state_val (transfer (kind a) (transfers (kinds as') s')) V
[PROOF STEP]
have "state_val (transfers (kinds as) s') V =
                       state_val (transfers (kinds (as'@[a])) s') V"
[PROOF STATE]
proof (prove)
using this:
transfers (kinds as) ?s = transfers (kinds (a # as'')) (transfers (kinds as') ?s)
state_val (transfers (kinds (a # as'')) (transfers (kinds as') s')) V = state_val (transfer (kind a) (transfers (kinds as') s')) V

goal (1 subgoal):
 1. state_val (transfers (kinds as) s') V = state_val (transfers (kinds (as' @ [a])) s') V
[PROOF STEP]
by(simp add:transfers_split kinds_def)
[PROOF STATE]
proof (state)
this:
state_val (transfers (kinds as) s') V = state_val (transfers (kinds (as' @ [a])) s') V

goal (1 subgoal):
 1. \<not> (\<forall>as' a as''. as = as' @ a # as'' \<longrightarrow> \<not> sourcenode a -{V}a # as''\<rightarrow>\<^sub>d\<^sub>d n') \<Longrightarrow> \<exists>as' a as''. as = as' @ a # as'' \<and> sourcenode a -{V}a # as''\<rightarrow>\<^sub>d\<^sub>d n' \<and> state_val (transfers (kinds as) s) V = state_val (transfers (kinds (as' @ [a])) s) V \<and> state_val (transfers (kinds as) s') V = state_val (transfers (kinds (as' @ [a])) s') V
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
state_val (transfers (kinds as) s) V = state_val (transfers (kinds (as' @ [a])) s) V
state_val (transfers (kinds as) s') V = state_val (transfers (kinds (as' @ [a])) s') V
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
state_val (transfers (kinds as) s) V = state_val (transfers (kinds (as' @ [a])) s) V
state_val (transfers (kinds as) s') V = state_val (transfers (kinds (as' @ [a])) s') V

goal (1 subgoal):
 1. \<exists>as' a as''. as = as' @ a # as'' \<and> sourcenode a -{V}a # as''\<rightarrow>\<^sub>d\<^sub>d n' \<and> state_val (transfers (kinds as) s) V = state_val (transfers (kinds (as' @ [a])) s) V \<and> state_val (transfers (kinds as) s') V = state_val (transfers (kinds (as' @ [a])) s') V
[PROOF STEP]
using \<open>sourcenode a -{V}a#as''\<rightarrow>\<^sub>d\<^sub>d n'\<close>
[PROOF STATE]
proof (prove)
using this:
state_val (transfers (kinds as) s) V = state_val (transfers (kinds (as' @ [a])) s) V
state_val (transfers (kinds as) s') V = state_val (transfers (kinds (as' @ [a])) s') V
sourcenode a -{V}a # as''\<rightarrow>\<^sub>d\<^sub>d n'

goal (1 subgoal):
 1. \<exists>as' a as''. as = as' @ a # as'' \<and> sourcenode a -{V}a # as''\<rightarrow>\<^sub>d\<^sub>d n' \<and> state_val (transfers (kinds as) s) V = state_val (transfers (kinds (as' @ [a])) s) V \<and> state_val (transfers (kinds as) s') V = state_val (transfers (kinds (as' @ [a])) s') V
[PROOF STEP]
by simp blast
[PROOF STATE]
proof (state)
this:
\<exists>as' a as''. as = as' @ a # as'' \<and> sourcenode a -{V}a # as''\<rightarrow>\<^sub>d\<^sub>d n' \<and> state_val (transfers (kinds as) s) V = state_val (transfers (kinds (as' @ [a])) s) V \<and> state_val (transfers (kinds as) s') V = state_val (transfers (kinds (as' @ [a])) s') V

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>as' a as''. as = as' @ a # as'' \<and> sourcenode a -{V}a # as''\<rightarrow>\<^sub>d\<^sub>d n' \<and> state_val (transfers (kinds as) s) V = state_val (transfers (kinds (as' @ [a])) s) V \<and> state_val (transfers (kinds as) s') V = state_val (transfers (kinds (as' @ [a])) s') V

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma DynPDG_scd:
  "DynPDG sourcenode targetnode kind valid_edge (_Entry_)
          Def Use state_val (_Exit_) dyn_standard_control_dependence"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. DynPDG sourcenode targetnode kind valid_edge (_Entry_) Def Use state_val (_Exit_) dyn_standard_control_dependence
[PROOF STEP]
proof(unfold_locales)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>n n' as. n controls\<^sub>s n' via as \<Longrightarrow> n' \<noteq> (_Exit_)
 2. \<And>n n' as. n controls\<^sub>s n' via as \<Longrightarrow> n -as\<rightarrow>* n' \<and> as \<noteq> []
[PROOF STEP]
fix n n' as
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>n n' as. n controls\<^sub>s n' via as \<Longrightarrow> n' \<noteq> (_Exit_)
 2. \<And>n n' as. n controls\<^sub>s n' via as \<Longrightarrow> n -as\<rightarrow>* n' \<and> as \<noteq> []
[PROOF STEP]
assume "n controls\<^sub>s n' via as"
[PROOF STATE]
proof (state)
this:
n controls\<^sub>s n' via as

goal (2 subgoals):
 1. \<And>n n' as. n controls\<^sub>s n' via as \<Longrightarrow> n' \<noteq> (_Exit_)
 2. \<And>n n' as. n controls\<^sub>s n' via as \<Longrightarrow> n -as\<rightarrow>* n' \<and> as \<noteq> []
[PROOF STEP]
show "n' \<noteq> (_Exit_)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n' \<noteq> (_Exit_)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n' = (_Exit_) \<Longrightarrow> False
[PROOF STEP]
assume "n' = (_Exit_)"
[PROOF STATE]
proof (state)
this:
n' = (_Exit_)

goal (1 subgoal):
 1. n' = (_Exit_) \<Longrightarrow> False
[PROOF STEP]
with \<open>n controls\<^sub>s n' via as\<close>
[PROOF STATE]
proof (chain)
picking this:
n controls\<^sub>s n' via as
n' = (_Exit_)
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
n controls\<^sub>s n' via as
n' = (_Exit_)

goal (1 subgoal):
 1. False
[PROOF STEP]
by(fastforce intro:Exit_not_dyn_standard_control_dependent)
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
n' \<noteq> (_Exit_)

goal (1 subgoal):
 1. \<And>n n' as. n controls\<^sub>s n' via as \<Longrightarrow> n -as\<rightarrow>* n' \<and> as \<noteq> []
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n n' as. n controls\<^sub>s n' via as \<Longrightarrow> n -as\<rightarrow>* n' \<and> as \<noteq> []
[PROOF STEP]
fix n n' as
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n n' as. n controls\<^sub>s n' via as \<Longrightarrow> n -as\<rightarrow>* n' \<and> as \<noteq> []
[PROOF STEP]
assume "n controls\<^sub>s n' via as"
[PROOF STATE]
proof (state)
this:
n controls\<^sub>s n' via as

goal (1 subgoal):
 1. \<And>n n' as. n controls\<^sub>s n' via as \<Longrightarrow> n -as\<rightarrow>* n' \<and> as \<noteq> []
[PROOF STEP]
thus "n -as\<rightarrow>* n' \<and> as \<noteq> []"
[PROOF STATE]
proof (prove)
using this:
n controls\<^sub>s n' via as

goal (1 subgoal):
 1. n -as\<rightarrow>* n' \<and> as \<noteq> []
[PROOF STEP]
by(fastforce simp:dyn_standard_control_dependence_def)
[PROOF STATE]
proof (state)
this:
n -as\<rightarrow>* n' \<and> as \<noteq> []

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma DynPDG_wcd:
  "DynPDG sourcenode targetnode kind valid_edge (_Entry_)
          Def Use state_val (_Exit_) dyn_weak_control_dependence"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. DynPDG sourcenode targetnode kind valid_edge (_Entry_) Def Use state_val (_Exit_) dyn_weak_control_dependence
[PROOF STEP]
proof(unfold_locales)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>n n' as. n weakly controls n' via as \<Longrightarrow> n' \<noteq> (_Exit_)
 2. \<And>n n' as. n weakly controls n' via as \<Longrightarrow> n -as\<rightarrow>* n' \<and> as \<noteq> []
[PROOF STEP]
fix n n' as
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>n n' as. n weakly controls n' via as \<Longrightarrow> n' \<noteq> (_Exit_)
 2. \<And>n n' as. n weakly controls n' via as \<Longrightarrow> n -as\<rightarrow>* n' \<and> as \<noteq> []
[PROOF STEP]
assume "n weakly controls n' via as"
[PROOF STATE]
proof (state)
this:
n weakly controls n' via as

goal (2 subgoals):
 1. \<And>n n' as. n weakly controls n' via as \<Longrightarrow> n' \<noteq> (_Exit_)
 2. \<And>n n' as. n weakly controls n' via as \<Longrightarrow> n -as\<rightarrow>* n' \<and> as \<noteq> []
[PROOF STEP]
show "n' \<noteq> (_Exit_)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n' \<noteq> (_Exit_)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n' = (_Exit_) \<Longrightarrow> False
[PROOF STEP]
assume "n' = (_Exit_)"
[PROOF STATE]
proof (state)
this:
n' = (_Exit_)

goal (1 subgoal):
 1. n' = (_Exit_) \<Longrightarrow> False
[PROOF STEP]
with \<open>n weakly controls n' via as\<close>
[PROOF STATE]
proof (chain)
picking this:
n weakly controls n' via as
n' = (_Exit_)
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
n weakly controls n' via as
n' = (_Exit_)

goal (1 subgoal):
 1. False
[PROOF STEP]
by(fastforce intro:Exit_not_dyn_weak_control_dependent)
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
n' \<noteq> (_Exit_)

goal (1 subgoal):
 1. \<And>n n' as. n weakly controls n' via as \<Longrightarrow> n -as\<rightarrow>* n' \<and> as \<noteq> []
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n n' as. n weakly controls n' via as \<Longrightarrow> n -as\<rightarrow>* n' \<and> as \<noteq> []
[PROOF STEP]
fix n n' as
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n n' as. n weakly controls n' via as \<Longrightarrow> n -as\<rightarrow>* n' \<and> as \<noteq> []
[PROOF STEP]
assume "n weakly controls n' via as"
[PROOF STATE]
proof (state)
this:
n weakly controls n' via as

goal (1 subgoal):
 1. \<And>n n' as. n weakly controls n' via as \<Longrightarrow> n -as\<rightarrow>* n' \<and> as \<noteq> []
[PROOF STEP]
thus "n -as\<rightarrow>* n' \<and> as \<noteq> []"
[PROOF STATE]
proof (prove)
using this:
n weakly controls n' via as

goal (1 subgoal):
 1. n -as\<rightarrow>* n' \<and> as \<noteq> []
[PROOF STEP]
by(fastforce simp:dyn_weak_control_dependence_def)
[PROOF STATE]
proof (state)
this:
n -as\<rightarrow>* n' \<and> as \<noteq> []

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in CFGExit_wf) DynPDG_scd:
  "DynPDG sourcenode targetnode kind valid_edge (_Entry_)
          Def Use state_val  (_Exit_) empty_control_dependence"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. DynPDG sourcenode targetnode kind valid_edge (_Entry_) Def Use state_val (_Exit_) empty_control_dependence
[PROOF STEP]
proof(unfold_locales)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>n n' as. empty_control_dependence n n' as \<Longrightarrow> n' \<noteq> (_Exit_)
 2. \<And>n n' as. empty_control_dependence n n' as \<Longrightarrow> n -as\<rightarrow>* n' \<and> as \<noteq> []
[PROOF STEP]
fix n n' as
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>n n' as. empty_control_dependence n n' as \<Longrightarrow> n' \<noteq> (_Exit_)
 2. \<And>n n' as. empty_control_dependence n n' as \<Longrightarrow> n -as\<rightarrow>* n' \<and> as \<noteq> []
[PROOF STEP]
assume "empty_control_dependence n n' as"
[PROOF STATE]
proof (state)
this:
empty_control_dependence n n' as

goal (2 subgoals):
 1. \<And>n n' as. empty_control_dependence n n' as \<Longrightarrow> n' \<noteq> (_Exit_)
 2. \<And>n n' as. empty_control_dependence n n' as \<Longrightarrow> n -as\<rightarrow>* n' \<and> as \<noteq> []
[PROOF STEP]
thus "n' \<noteq> (_Exit_)"
[PROOF STATE]
proof (prove)
using this:
empty_control_dependence n n' as

goal (1 subgoal):
 1. n' \<noteq> (_Exit_)
[PROOF STEP]
by(simp add:empty_control_dependence_def)
[PROOF STATE]
proof (state)
this:
n' \<noteq> (_Exit_)

goal (1 subgoal):
 1. \<And>n n' as. empty_control_dependence n n' as \<Longrightarrow> n -as\<rightarrow>* n' \<and> as \<noteq> []
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n n' as. empty_control_dependence n n' as \<Longrightarrow> n -as\<rightarrow>* n' \<and> as \<noteq> []
[PROOF STEP]
fix n n' as
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n n' as. empty_control_dependence n n' as \<Longrightarrow> n -as\<rightarrow>* n' \<and> as \<noteq> []
[PROOF STEP]
assume "empty_control_dependence n n' as"
[PROOF STATE]
proof (state)
this:
empty_control_dependence n n' as

goal (1 subgoal):
 1. \<And>n n' as. empty_control_dependence n n' as \<Longrightarrow> n -as\<rightarrow>* n' \<and> as \<noteq> []
[PROOF STEP]
thus "n -as\<rightarrow>* n' \<and> as \<noteq> []"
[PROOF STATE]
proof (prove)
using this:
empty_control_dependence n n' as

goal (1 subgoal):
 1. n -as\<rightarrow>* n' \<and> as \<noteq> []
[PROOF STEP]
by(simp add:empty_control_dependence_def)
[PROOF STATE]
proof (state)
this:
n -as\<rightarrow>* n' \<and> as \<noteq> []

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma linear_split_alt: "linear_split xs x = (takeWhile (\<lambda>(_,s). s<x) xs, dropWhile (\<lambda>(_,s). s<x) xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. linear_split xs x = (takeWhile (\<lambda>(uu_, s). s < x) xs, dropWhile (\<lambda>(uu_, s). s < x) xs)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. linear_split xs x = (takeWhile (\<lambda>(uu_, s). s < x) xs, dropWhile (\<lambda>(uu_, s). s < x) xs)
[PROOF STEP]
have "linear_split_help xs x prev = (prev @ takeWhile (\<lambda>(_, s). s < x) xs, dropWhile (\<lambda>(_, s). s < x) xs)"
    for prev
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. linear_split_help xs x prev = (prev @ takeWhile (\<lambda>(uu_, s). s < x) xs, dropWhile (\<lambda>(uu_, s). s < x) xs)
[PROOF STEP]
apply (induction xs arbitrary: prev)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>prev. linear_split_help [] x prev = (prev @ takeWhile (\<lambda>(uu_, s). s < x) [], dropWhile (\<lambda>(uu_, s). s < x) [])
 2. \<And>a xs prev. (\<And>prev. linear_split_help xs x prev = (prev @ takeWhile (\<lambda>(uu_, s). s < x) xs, dropWhile (\<lambda>(uu_, s). s < x) xs)) \<Longrightarrow> linear_split_help (a # xs) x prev = (prev @ takeWhile (\<lambda>(uu_, s). s < x) (a # xs), dropWhile (\<lambda>(uu_, s). s < x) (a # xs))
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
linear_split_help xs x ?prev = (?prev @ takeWhile (\<lambda>(uu_, s). s < x) xs, dropWhile (\<lambda>(uu_, s). s < x) xs)

goal (1 subgoal):
 1. linear_split xs x = (takeWhile (\<lambda>(uu_, s). s < x) xs, dropWhile (\<lambda>(uu_, s). s < x) xs)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
linear_split_help xs x ?prev = (?prev @ takeWhile (\<lambda>(uu_, s). s < x) xs, dropWhile (\<lambda>(uu_, s). s < x) xs)

goal (1 subgoal):
 1. linear_split xs x = (takeWhile (\<lambda>(uu_, s). s < x) xs, dropWhile (\<lambda>(uu_, s). s < x) xs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
linear_split xs x = (takeWhile (\<lambda>(uu_, s). s < x) xs, dropWhile (\<lambda>(uu_, s). s < x) xs)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma some_child_sm: "linear_split_help t y xs = (ls,(sub,sep)#rs) \<Longrightarrow> y \<le> sep"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. linear_split_help t y xs = (ls, (sub, sep) # rs) \<Longrightarrow> y \<le> sep
[PROOF STEP]
apply(induction t y xs rule: linear_split_help.induct)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x prev. linear_split_help [] x prev = (ls, (sub, sep) # rs) \<Longrightarrow> x \<le> sep
 2. \<And>suba sepa xs x prev. \<lbrakk>\<lbrakk>sepa < x; linear_split_help xs x (prev @ [(suba, sepa)]) = (ls, (sub, sep) # rs)\<rbrakk> \<Longrightarrow> x \<le> sep; linear_split_help ((suba, sepa) # xs) x prev = (ls, (sub, sep) # rs)\<rbrakk> \<Longrightarrow> x \<le> sep
[PROOF STEP]
apply(simp_all)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>suba sepa xs x prev. \<lbrakk>\<lbrakk>sepa < x; linear_split_help xs x (prev @ [(suba, sepa)]) = (ls, (sub, sep) # rs)\<rbrakk> \<Longrightarrow> x \<le> sep; (if sepa < x then linear_split_help xs x (prev @ [(suba, sepa)]) else (prev, (suba, sepa) # xs)) = (ls, (sub, sep) # rs)\<rbrakk> \<Longrightarrow> x \<le> sep
[PROOF STEP]
by (metis Pair_inject le_less_linear list.inject)


[STATEMENT]
lemma linear_split_append: "linear_split_help xs p ys = (ls,rs) \<Longrightarrow> ls@rs = ys@xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. linear_split_help xs p ys = (ls, rs) \<Longrightarrow> ls @ rs = ys @ xs
[PROOF STEP]
apply(induction xs p ys rule: linear_split_help.induct)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x prev. linear_split_help [] x prev = (ls, rs) \<Longrightarrow> ls @ rs = prev @ []
 2. \<And>sub sep xs x prev. \<lbrakk>\<lbrakk>sep < x; linear_split_help xs x (prev @ [(sub, sep)]) = (ls, rs)\<rbrakk> \<Longrightarrow> ls @ rs = (prev @ [(sub, sep)]) @ xs; linear_split_help ((sub, sep) # xs) x prev = (ls, rs)\<rbrakk> \<Longrightarrow> ls @ rs = prev @ (sub, sep) # xs
[PROOF STEP]
apply(simp_all)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>sub sep xs x prev. \<lbrakk>\<lbrakk>sep < x; linear_split_help xs x (prev @ [(sub, sep)]) = (ls, rs)\<rbrakk> \<Longrightarrow> ls @ rs = prev @ (sub, sep) # xs; (if sep < x then linear_split_help xs x (prev @ [(sub, sep)]) else (prev, (sub, sep) # xs)) = (ls, rs)\<rbrakk> \<Longrightarrow> ls @ rs = prev @ (sub, sep) # xs
[PROOF STEP]
by (metis Pair_inject)


[STATEMENT]
lemma linear_split_sm: "\<lbrakk>linear_split_help xs p ys = (ls,rs); sorted_less (separators (ys@xs)); \<forall>sep \<in> set (separators ys). p > sep\<rbrakk> \<Longrightarrow> \<forall>sep \<in> set (separators ls). p > sep"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>linear_split_help xs p ys = (ls, rs); sorted_less (separators (ys @ xs)); \<forall>sep\<in>set (separators ys). sep < p\<rbrakk> \<Longrightarrow> \<forall>sep\<in>set (separators ls). sep < p
[PROOF STEP]
apply(induction xs p ys rule: linear_split_help.induct)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x prev. \<lbrakk>linear_split_help [] x prev = (ls, rs); sorted_less (separators (prev @ [])); \<forall>sep\<in>set (separators prev). sep < x\<rbrakk> \<Longrightarrow> \<forall>sep\<in>set (separators ls). sep < x
 2. \<And>sub sep xs x prev. \<lbrakk>\<lbrakk>sep < x; linear_split_help xs x (prev @ [(sub, sep)]) = (ls, rs); sorted_less (separators ((prev @ [(sub, sep)]) @ xs)); \<forall>sep\<in>set (separators (prev @ [(sub, sep)])). sep < x\<rbrakk> \<Longrightarrow> \<forall>sep\<in>set (separators ls). sep < x; linear_split_help ((sub, sep) # xs) x prev = (ls, rs); sorted_less (separators (prev @ (sub, sep) # xs)); \<forall>sep\<in>set (separators prev). sep < x\<rbrakk> \<Longrightarrow> \<forall>sep\<in>set (separators ls). sep < x
[PROOF STEP]
apply(simp_all)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>sub sep xs x prev. \<lbrakk>\<lbrakk>linear_split_help xs x (prev @ [(sub, sep)]) = (ls, rs); sep < x\<rbrakk> \<Longrightarrow> \<forall>sep\<in>set ls. snd sep < x; (if sep < x then linear_split_help xs x (prev @ [(sub, sep)]) else (prev, (sub, sep) # xs)) = (ls, rs); sorted_less (separators prev @ sep # separators xs); \<forall>sep\<in>set prev. snd sep < x\<rbrakk> \<Longrightarrow> \<forall>sep\<in>set ls. snd sep < x
[PROOF STEP]
by (metis prod.inject)+


[STATEMENT]
lemma linear_split_gr:
  "\<lbrakk>linear_split_help xs p ys = (ls,rs); sorted_less (separators (ys@xs)); \<forall>(sub,sep) \<in> set ys. p > sep\<rbrakk> \<Longrightarrow>
(case rs of [] \<Rightarrow> True | (_,sep)#_ \<Rightarrow> p \<le> sep)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>linear_split_help xs p ys = (ls, rs); sorted_less (separators (ys @ xs)); \<forall>(sub, sep)\<in>set ys. sep < p\<rbrakk> \<Longrightarrow> case rs of [] \<Rightarrow> True | (x, sep) # xa \<Rightarrow> p \<le> sep
[PROOF STEP]
apply(cases rs)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>linear_split_help xs p ys = (ls, rs); sorted_less (separators (ys @ xs)); \<forall>(sub, sep)\<in>set ys. sep < p; rs = []\<rbrakk> \<Longrightarrow> case rs of [] \<Rightarrow> True | (x, sep) # xa \<Rightarrow> p \<le> sep
 2. \<And>a list. \<lbrakk>linear_split_help xs p ys = (ls, rs); sorted_less (separators (ys @ xs)); \<forall>(sub, sep)\<in>set ys. sep < p; rs = a # list\<rbrakk> \<Longrightarrow> case rs of [] \<Rightarrow> True | (x, sep) # xa \<Rightarrow> p \<le> sep
[PROOF STEP]
by (auto simp add: some_child_sm)


[STATEMENT]
lemma linear_split_req:
  assumes  "linear_split xs p = (ls,(sub,sep)#rs)"
    and "sorted_less (separators xs)"
  shows  "p \<le> sep"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<le> sep
[PROOF STEP]
using assms linear_split_gr
[PROOF STATE]
proof (prove)
using this:
linear_split xs p = (ls, (sub, sep) # rs)
sorted_less (separators xs)
\<lbrakk>linear_split_help ?xs ?p ?ys = (?ls, ?rs); sorted_less (separators (?ys @ ?xs)); \<forall>(sub, sep)\<in>set ?ys. sep < ?p\<rbrakk> \<Longrightarrow> case ?rs of [] \<Rightarrow> True | (x, sep) # xa \<Rightarrow> ?p \<le> sep

goal (1 subgoal):
 1. p \<le> sep
[PROOF STEP]
by fastforce


[STATEMENT]
lemma linear_split_req2:
  assumes  "linear_split xs p = (ls@[(sub,sep)],rs)"
    and "sorted_less (separators xs)"
  shows  "sep < p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sep < p
[PROOF STEP]
using linear_split_sm[of xs p "[]" "ls@[(sub,sep)]" rs]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>linear_split_help xs p [] = (ls @ [(sub, sep)], rs); sorted_less (separators ([] @ xs)); \<forall>sep\<in>set (separators []). sep < p\<rbrakk> \<Longrightarrow> \<forall>sep\<in>set (separators (ls @ [(sub, sep)])). sep < p

goal (1 subgoal):
 1. sep < p
[PROOF STEP]
using assms(1) assms(2)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>linear_split_help xs p [] = (ls @ [(sub, sep)], rs); sorted_less (separators ([] @ xs)); \<forall>sep\<in>set (separators []). sep < p\<rbrakk> \<Longrightarrow> \<forall>sep\<in>set (separators (ls @ [(sub, sep)])). sep < p
linear_split xs p = (ls @ [(sub, sep)], rs)
sorted_less (separators xs)

goal (1 subgoal):
 1. sep < p
[PROOF STEP]
by (metis Nil_is_map_conv Un_iff append_self_conv2 empty_iff empty_set linear_split.elims prod_set_simps(2) separators_split snd_eqD snds.intros)


[STATEMENT]
lemma "binary_split_help as bs cs x = (ls,rs) \<Longrightarrow> (as@bs@cs) = (ls@rs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. binary_split_help as bs cs x = (ls, rs) \<Longrightarrow> as @ bs @ cs = ls @ rs
[PROOF STEP]
apply(induction as bs cs x arbitrary: ls rs rule: binary_split_help.induct)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>ls rs x lsa rsa. binary_split_help ls [] rs x = (lsa, rsa) \<Longrightarrow> ls @ [] @ rs = lsa @ rsa
 2. \<And>ls v va rs x lsa rsa. \<lbrakk>\<And>xa xb y x21 x22 xaa ya lsa rsa. \<lbrakk>xa = split_half (v # va); (xb, y) = xa; y = x21 # x22; (xaa, ya) = x21; x < ya; binary_split_help ls xb (y @ rs) x = (lsa, rsa)\<rbrakk> \<Longrightarrow> ls @ xb @ y @ rs = lsa @ rsa; \<And>xa xb y x21 x22 xaa ya lsa rsa. \<lbrakk>xa = split_half (v # va); (xb, y) = xa; y = x21 # x22; (xaa, ya) = x21; \<not> x < ya; ya < x; binary_split_help (ls @ xb @ [(xaa, ya)]) x22 rs x = (lsa, rsa)\<rbrakk> \<Longrightarrow> (ls @ xb @ [(xaa, ya)]) @ x22 @ rs = lsa @ rsa; binary_split_help ls (v # va) rs x = (lsa, rsa)\<rbrakk> \<Longrightarrow> ls @ (v # va) @ rs = lsa @ rsa
[PROOF STEP]
apply (auto simp add: drop_not_empty split!: list.splits )
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ls a b va rs x lsa rsa aa ba x22. \<lbrakk>\<And>ab y ac xaa lsa rsa. \<lbrakk>ab = take (Suc (length va) div 2) ((a, b) # va); ac = aa; y = (aa, ba) # x22; xaa = aa; x < ba; binary_split_help ls (take (Suc (length va) div 2) ((a, b) # va)) ((aa, ba) # x22 @ rs) x = (lsa, rsa)\<rbrakk> \<Longrightarrow> ls @ take (Suc (length va) div 2) ((a, b) # va) @ (aa, ba) # x22 @ rs = lsa @ rsa; \<And>ab y ac xaa lsa rsa. \<lbrakk>ab = take (Suc (length va) div 2) ((a, b) # va); ac = aa; y = (aa, ba) # x22; xaa = aa; ba < x; binary_split_help (ls @ take (Suc (length va) div 2) ((a, b) # va) @ [(aa, ba)]) x22 rs x = (lsa, rsa)\<rbrakk> \<Longrightarrow> ls @ take (Suc (length va) div 2) ((a, b) # va) @ (aa, ba) # x22 @ rs = lsa @ rsa; drop (Suc (length va) div 2) ((a, b) # va) = (aa, ba) # x22; (if x < ba then binary_split_help ls (take (Suc (length va) div 2) ((a, b) # va)) (drop (Suc (length va) div 2) ((a, b) # va) @ rs) x else if ba < x then binary_split_help (ls @ take (Suc (length va) div 2) ((a, b) # va) @ [(aa, ba)]) x22 rs x else (ls @ take (Suc (length va) div 2) ((a, b) # va), drop (Suc (length va) div 2) ((a, b) # va) @ rs)) = (lsa, rsa)\<rbrakk> \<Longrightarrow> ls @ (a, b) # va @ rs = lsa @ rsa
[PROOF STEP]
subgoal for ls a b va rs  x lsa rsa aa ba x22
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>ab y ac xaa ls rs. \<lbrakk>ab = take (Suc (length va) div 2) ((a, b) # va); ac = aa; y = (aa, ba) # x22; xaa = aa; x < ba; binary_split_help ls (take (Suc (length va) div 2) ((a, b) # va)) ((aa, ba) # x22 @ rs) x = (ls, rs)\<rbrakk> \<Longrightarrow> ls @ take (Suc (length va) div 2) ((a, b) # va) @ (aa, ba) # x22 @ rs = ls @ rs; \<And>ab y ac xaa ls rs. \<lbrakk>ab = take (Suc (length va) div 2) ((a, b) # va); ac = aa; y = (aa, ba) # x22; xaa = aa; ba < x; binary_split_help (ls @ take (Suc (length va) div 2) ((a, b) # va) @ [(aa, ba)]) x22 rs x = (ls, rs)\<rbrakk> \<Longrightarrow> ls @ take (Suc (length va) div 2) ((a, b) # va) @ (aa, ba) # x22 @ rs = ls @ rs; drop (Suc (length va) div 2) ((a, b) # va) = (aa, ba) # x22; (if x < ba then binary_split_help ls (take (Suc (length va) div 2) ((a, b) # va)) (drop (Suc (length va) div 2) ((a, b) # va) @ rs) x else if ba < x then binary_split_help (ls @ take (Suc (length va) div 2) ((a, b) # va) @ [(aa, ba)]) x22 rs x else (ls @ take (Suc (length va) div 2) ((a, b) # va), drop (Suc (length va) div 2) ((a, b) # va) @ rs)) = (lsa, rsa)\<rbrakk> \<Longrightarrow> ls @ (a, b) # va @ rs = lsa @ rsa
[PROOF STEP]
apply(cases "cmp x ba")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<And>ab y ac xaa ls rs. \<lbrakk>ab = take (Suc (length va) div 2) ((a, b) # va); ac = aa; y = (aa, ba) # x22; xaa = aa; x < ba; binary_split_help ls (take (Suc (length va) div 2) ((a, b) # va)) ((aa, ba) # x22 @ rs) x = (ls, rs)\<rbrakk> \<Longrightarrow> ls @ take (Suc (length va) div 2) ((a, b) # va) @ (aa, ba) # x22 @ rs = ls @ rs; \<And>ab y ac xaa ls rs. \<lbrakk>ab = take (Suc (length va) div 2) ((a, b) # va); ac = aa; y = (aa, ba) # x22; xaa = aa; ba < x; binary_split_help (ls @ take (Suc (length va) div 2) ((a, b) # va) @ [(aa, ba)]) x22 rs x = (ls, rs)\<rbrakk> \<Longrightarrow> ls @ take (Suc (length va) div 2) ((a, b) # va) @ (aa, ba) # x22 @ rs = ls @ rs; drop (Suc (length va) div 2) ((a, b) # va) = (aa, ba) # x22; (if x < ba then binary_split_help ls (take (Suc (length va) div 2) ((a, b) # va)) (drop (Suc (length va) div 2) ((a, b) # va) @ rs) x else if ba < x then binary_split_help (ls @ take (Suc (length va) div 2) ((a, b) # va) @ [(aa, ba)]) x22 rs x else (ls @ take (Suc (length va) div 2) ((a, b) # va), drop (Suc (length va) div 2) ((a, b) # va) @ rs)) = (lsa, rsa); cmp x ba = LT\<rbrakk> \<Longrightarrow> ls @ (a, b) # va @ rs = lsa @ rsa
 2. \<lbrakk>\<And>ab y ac xaa ls rs. \<lbrakk>ab = take (Suc (length va) div 2) ((a, b) # va); ac = aa; y = (aa, ba) # x22; xaa = aa; x < ba; binary_split_help ls (take (Suc (length va) div 2) ((a, b) # va)) ((aa, ba) # x22 @ rs) x = (ls, rs)\<rbrakk> \<Longrightarrow> ls @ take (Suc (length va) div 2) ((a, b) # va) @ (aa, ba) # x22 @ rs = ls @ rs; \<And>ab y ac xaa ls rs. \<lbrakk>ab = take (Suc (length va) div 2) ((a, b) # va); ac = aa; y = (aa, ba) # x22; xaa = aa; ba < x; binary_split_help (ls @ take (Suc (length va) div 2) ((a, b) # va) @ [(aa, ba)]) x22 rs x = (ls, rs)\<rbrakk> \<Longrightarrow> ls @ take (Suc (length va) div 2) ((a, b) # va) @ (aa, ba) # x22 @ rs = ls @ rs; drop (Suc (length va) div 2) ((a, b) # va) = (aa, ba) # x22; (if x < ba then binary_split_help ls (take (Suc (length va) div 2) ((a, b) # va)) (drop (Suc (length va) div 2) ((a, b) # va) @ rs) x else if ba < x then binary_split_help (ls @ take (Suc (length va) div 2) ((a, b) # va) @ [(aa, ba)]) x22 rs x else (ls @ take (Suc (length va) div 2) ((a, b) # va), drop (Suc (length va) div 2) ((a, b) # va) @ rs)) = (lsa, rsa); cmp x ba = EQ\<rbrakk> \<Longrightarrow> ls @ (a, b) # va @ rs = lsa @ rsa
 3. \<lbrakk>\<And>ab y ac xaa ls rs. \<lbrakk>ab = take (Suc (length va) div 2) ((a, b) # va); ac = aa; y = (aa, ba) # x22; xaa = aa; x < ba; binary_split_help ls (take (Suc (length va) div 2) ((a, b) # va)) ((aa, ba) # x22 @ rs) x = (ls, rs)\<rbrakk> \<Longrightarrow> ls @ take (Suc (length va) div 2) ((a, b) # va) @ (aa, ba) # x22 @ rs = ls @ rs; \<And>ab y ac xaa ls rs. \<lbrakk>ab = take (Suc (length va) div 2) ((a, b) # va); ac = aa; y = (aa, ba) # x22; xaa = aa; ba < x; binary_split_help (ls @ take (Suc (length va) div 2) ((a, b) # va) @ [(aa, ba)]) x22 rs x = (ls, rs)\<rbrakk> \<Longrightarrow> ls @ take (Suc (length va) div 2) ((a, b) # va) @ (aa, ba) # x22 @ rs = ls @ rs; drop (Suc (length va) div 2) ((a, b) # va) = (aa, ba) # x22; (if x < ba then binary_split_help ls (take (Suc (length va) div 2) ((a, b) # va)) (drop (Suc (length va) div 2) ((a, b) # va) @ rs) x else if ba < x then binary_split_help (ls @ take (Suc (length va) div 2) ((a, b) # va) @ [(aa, ba)]) x22 rs x else (ls @ take (Suc (length va) div 2) ((a, b) # va), drop (Suc (length va) div 2) ((a, b) # va) @ rs)) = (lsa, rsa); cmp x ba = GT\<rbrakk> \<Longrightarrow> ls @ (a, b) # va @ rs = lsa @ rsa
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<And>ab y ac xaa ls. \<lbrakk>ab = take (Suc (length va) div 2) ((a, b) # va); ac = aa; y = (aa, ba) # x22; xaa = aa; lsa = ls\<rbrakk> \<Longrightarrow> ls @ take (Suc (length va) div 2) ((a, b) # va) @ (aa, ba) # x22 @ rs = ls @ rsa; drop (Suc (length va) div 2) ((a, b) # va) = (aa, ba) # x22; binary_split_help ls (take (Suc (length va) div 2) ((a, b) # va)) ((aa, ba) # x22 @ rs) x = (lsa, rsa); x < ba\<rbrakk> \<Longrightarrow> ls @ (a, b) # va @ rs = lsa @ rsa
 2. \<lbrakk>drop (Suc (length va) div 2) ((a, b) # va) = (aa, ba) # x22; x = ba; lsa = ls @ take (Suc (length va) div 2) ((a, b) # va); rsa = (aa, ba) # x22 @ rs\<rbrakk> \<Longrightarrow> (a, b) # va = take (Suc (length va) div 2) ((a, b) # va) @ (aa, ba) # x22
 3. \<lbrakk>\<And>ab y ac xaa ls. \<lbrakk>ab = take (Suc (length va) div 2) ((a, b) # va); ac = aa; y = (aa, ba) # x22; xaa = aa; lsa = ls\<rbrakk> \<Longrightarrow> ls @ take (Suc (length va) div 2) ((a, b) # va) @ (aa, ba) # x22 @ rs = ls @ rsa; drop (Suc (length va) div 2) ((a, b) # va) = (aa, ba) # x22; binary_split_help (ls @ take (Suc (length va) div 2) ((a, b) # va) @ [(aa, ba)]) x22 rs x = (lsa, rsa); ba < x\<rbrakk> \<Longrightarrow> ls @ (a, b) # va @ rs = lsa @ rsa
[PROOF STEP]
apply (metis Cons_eq_appendI append_eq_appendI append_take_drop_id)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>drop (Suc (length va) div 2) ((a, b) # va) = (aa, ba) # x22; x = ba; lsa = ls @ take (Suc (length va) div 2) ((a, b) # va); rsa = (aa, ba) # x22 @ rs\<rbrakk> \<Longrightarrow> (a, b) # va = take (Suc (length va) div 2) ((a, b) # va) @ (aa, ba) # x22
 2. \<lbrakk>\<And>ab y ac xaa ls. \<lbrakk>ab = take (Suc (length va) div 2) ((a, b) # va); ac = aa; y = (aa, ba) # x22; xaa = aa; lsa = ls\<rbrakk> \<Longrightarrow> ls @ take (Suc (length va) div 2) ((a, b) # va) @ (aa, ba) # x22 @ rs = ls @ rsa; drop (Suc (length va) div 2) ((a, b) # va) = (aa, ba) # x22; binary_split_help (ls @ take (Suc (length va) div 2) ((a, b) # va) @ [(aa, ba)]) x22 rs x = (lsa, rsa); ba < x\<rbrakk> \<Longrightarrow> ls @ (a, b) # va @ rs = lsa @ rsa
[PROOF STEP]
apply (metis append_take_drop_id)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>ab y ac xaa ls. \<lbrakk>ab = take (Suc (length va) div 2) ((a, b) # va); ac = aa; y = (aa, ba) # x22; xaa = aa; lsa = ls\<rbrakk> \<Longrightarrow> ls @ take (Suc (length va) div 2) ((a, b) # va) @ (aa, ba) # x22 @ rs = ls @ rsa; drop (Suc (length va) div 2) ((a, b) # va) = (aa, ba) # x22; binary_split_help (ls @ take (Suc (length va) div 2) ((a, b) # va) @ [(aa, ba)]) x22 rs x = (lsa, rsa); ba < x\<rbrakk> \<Longrightarrow> ls @ (a, b) # va @ rs = lsa @ rsa
[PROOF STEP]
by (metis Cons_eq_appendI append_eq_appendI append_take_drop_id)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma "\<lbrakk>sorted_less (separators (as@bs@cs)); binary_split_help as bs cs x = (ls,rs); \<forall>y \<in> set (separators as). y < x\<rbrakk>
\<Longrightarrow> \<forall>y \<in> set (separators ls). y < x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sorted_less (separators (as @ bs @ cs)); binary_split_help as bs cs x = (ls, rs); \<forall>y\<in>set (separators as). y < x\<rbrakk> \<Longrightarrow> \<forall>y\<in>set (separators ls). y < x
[PROOF STEP]
oops


[STATEMENT]
lemma new_Addr_SomeD:
  "new_Addr h = Some a \<Longrightarrow> h a = None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. new_Addr h = \<lfloor>a\<rfloor> \<Longrightarrow> h a = None
[PROOF STEP]
by(auto simp add:new_Addr_def split:if_splits intro: LeastI)


[STATEMENT]
lemma new_Addr_SomeI:
  "finite (dom h) \<Longrightarrow> \<exists>a. new_Addr h = Some a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (dom h) \<Longrightarrow> \<exists>a. new_Addr h = \<lfloor>a\<rfloor>
[PROOF STEP]
by(simp add: new_Addr_def) (metis finite_map_freshness infinite_UNIV_nat)


[STATEMENT]
lemma new_Addr_code_code [code]:
  "new_Addr h = gen_new_Addr h 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. new_Addr h = gen_new_Addr h 0
[PROOF STEP]
by(simp add: new_Addr_def gen_new_Addr_def)


[STATEMENT]
lemma gen_new_Addr_code [code]:
  "gen_new_Addr h n = (if h n = None then Some n else gen_new_Addr h (Suc n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gen_new_Addr h n = (if h n = None then \<lfloor>n\<rfloor> else gen_new_Addr h (Suc n))
[PROOF STEP]
apply(simp add: gen_new_Addr_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>a\<ge>n. h a = None) \<longrightarrow> ((\<exists>a\<ge>Suc n. h a = None) \<longrightarrow> (h n = None \<longrightarrow> (LEAST a. n \<le> a \<and> h a = None) = n) \<and> ((\<exists>y. h n = \<lfloor>y\<rfloor>) \<longrightarrow> (LEAST a. n \<le> a \<and> h a = None) = (LEAST a. Suc n \<le> a \<and> h a = None))) \<and> ((\<forall>a\<ge>Suc n. \<exists>y. h a = \<lfloor>y\<rfloor>) \<longrightarrow> (h n = None \<longrightarrow> (LEAST a. n \<le> a \<and> h a = None) = n) \<and> h n = None)
[PROOF STEP]
apply(rule impI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>a\<ge>n. h a = None \<Longrightarrow> ((\<exists>a\<ge>Suc n. h a = None) \<longrightarrow> (h n = None \<longrightarrow> (LEAST a. n \<le> a \<and> h a = None) = n) \<and> ((\<exists>y. h n = \<lfloor>y\<rfloor>) \<longrightarrow> (LEAST a. n \<le> a \<and> h a = None) = (LEAST a. Suc n \<le> a \<and> h a = None))) \<and> ((\<forall>a\<ge>Suc n. \<exists>y. h a = \<lfloor>y\<rfloor>) \<longrightarrow> (h n = None \<longrightarrow> (LEAST a. n \<le> a \<and> h a = None) = n) \<and> h n = None)
[PROOF STEP]
apply(rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<exists>a\<ge>n. h a = None \<Longrightarrow> (\<exists>a\<ge>Suc n. h a = None) \<longrightarrow> (h n = None \<longrightarrow> (LEAST a. n \<le> a \<and> h a = None) = n) \<and> ((\<exists>y. h n = \<lfloor>y\<rfloor>) \<longrightarrow> (LEAST a. n \<le> a \<and> h a = None) = (LEAST a. Suc n \<le> a \<and> h a = None))
 2. \<exists>a\<ge>n. h a = None \<Longrightarrow> (\<forall>a\<ge>Suc n. \<exists>y. h a = \<lfloor>y\<rfloor>) \<longrightarrow> (h n = None \<longrightarrow> (LEAST a. n \<le> a \<and> h a = None) = n) \<and> h n = None
[PROOF STEP]
apply safe[1]
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a aa. \<lbrakk>n \<le> a; h a = None; Suc n \<le> aa; h aa = None; h n = None\<rbrakk> \<Longrightarrow> (LEAST a. n \<le> a \<and> h a = None) = n
 2. \<And>a aa y. \<lbrakk>n \<le> a; h a = None; Suc n \<le> aa; h aa = None; h n = \<lfloor>y\<rfloor>\<rbrakk> \<Longrightarrow> (LEAST a. n \<le> a \<and> h a = None) = (LEAST a. Suc n \<le> a \<and> h a = None)
 3. \<exists>a\<ge>n. h a = None \<Longrightarrow> (\<forall>a\<ge>Suc n. \<exists>y. h a = \<lfloor>y\<rfloor>) \<longrightarrow> (h n = None \<longrightarrow> (LEAST a. n \<le> a \<and> h a = None) = n) \<and> h n = None
[PROOF STEP]
apply(auto intro: Least_equality)[2]
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a aa y. \<lbrakk>n \<le> a; h a = None; Suc n \<le> aa; h aa = None; h n = \<lfloor>y\<rfloor>\<rbrakk> \<Longrightarrow> (LEAST a. n \<le> a \<and> h a = None) = (LEAST a. Suc n \<le> a \<and> h a = None)
 2. \<exists>a\<ge>n. h a = None \<Longrightarrow> (\<forall>a\<ge>Suc n. \<exists>y. h a = \<lfloor>y\<rfloor>) \<longrightarrow> (h n = None \<longrightarrow> (LEAST a. n \<le> a \<and> h a = None) = n) \<and> h n = None
[PROOF STEP]
apply(rule arg_cong[where f=Least])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a aa y. \<lbrakk>n \<le> a; h a = None; Suc n \<le> aa; h aa = None; h n = \<lfloor>y\<rfloor>\<rbrakk> \<Longrightarrow> (\<lambda>a. n \<le> a \<and> h a = None) = (\<lambda>a. Suc n \<le> a \<and> h a = None)
 2. \<exists>a\<ge>n. h a = None \<Longrightarrow> (\<forall>a\<ge>Suc n. \<exists>y. h a = \<lfloor>y\<rfloor>) \<longrightarrow> (h n = None \<longrightarrow> (LEAST a. n \<le> a \<and> h a = None) = n) \<and> h n = None
[PROOF STEP]
apply(rule ext)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a aa y ab. \<lbrakk>n \<le> a; h a = None; Suc n \<le> aa; h aa = None; h n = \<lfloor>y\<rfloor>\<rbrakk> \<Longrightarrow> (n \<le> ab \<and> h ab = None) = (Suc n \<le> ab \<and> h ab = None)
 2. \<exists>a\<ge>n. h a = None \<Longrightarrow> (\<forall>a\<ge>Suc n. \<exists>y. h a = \<lfloor>y\<rfloor>) \<longrightarrow> (h n = None \<longrightarrow> (LEAST a. n \<le> a \<and> h a = None) = n) \<and> h n = None
[PROOF STEP]
apply auto[1]
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a aa y ab. \<lbrakk>n \<le> a; h a = None; Suc n \<le> aa; h aa = None; h n = \<lfloor>y\<rfloor>; n \<le> ab; h ab = None\<rbrakk> \<Longrightarrow> Suc n \<le> ab
 2. \<exists>a\<ge>n. h a = None \<Longrightarrow> (\<forall>a\<ge>Suc n. \<exists>y. h a = \<lfloor>y\<rfloor>) \<longrightarrow> (h n = None \<longrightarrow> (LEAST a. n \<le> a \<and> h a = None) = n) \<and> h n = None
[PROOF STEP]
apply(case_tac "n = ab")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a aa y ab. \<lbrakk>n \<le> a; h a = None; Suc n \<le> aa; h aa = None; h n = \<lfloor>y\<rfloor>; n \<le> ab; h ab = None; n = ab\<rbrakk> \<Longrightarrow> Suc n \<le> ab
 2. \<And>a aa y ab. \<lbrakk>n \<le> a; h a = None; Suc n \<le> aa; h aa = None; h n = \<lfloor>y\<rfloor>; n \<le> ab; h ab = None; n \<noteq> ab\<rbrakk> \<Longrightarrow> Suc n \<le> ab
 3. \<exists>a\<ge>n. h a = None \<Longrightarrow> (\<forall>a\<ge>Suc n. \<exists>y. h a = \<lfloor>y\<rfloor>) \<longrightarrow> (h n = None \<longrightarrow> (LEAST a. n \<le> a \<and> h a = None) = n) \<and> h n = None
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a aa y ab. \<lbrakk>n \<le> a; h a = None; Suc n \<le> aa; h aa = None; h n = \<lfloor>y\<rfloor>; n \<le> ab; h ab = None; n \<noteq> ab\<rbrakk> \<Longrightarrow> Suc n \<le> ab
 2. \<exists>a\<ge>n. h a = None \<Longrightarrow> (\<forall>a\<ge>Suc n. \<exists>y. h a = \<lfloor>y\<rfloor>) \<longrightarrow> (h n = None \<longrightarrow> (LEAST a. n \<le> a \<and> h a = None) = n) \<and> h n = None
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>a\<ge>n. h a = None \<Longrightarrow> (\<forall>a\<ge>Suc n. \<exists>y. h a = \<lfloor>y\<rfloor>) \<longrightarrow> (h n = None \<longrightarrow> (LEAST a. n \<le> a \<and> h a = None) = n) \<and> h n = None
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>n \<le> a; h a = None; \<forall>a\<ge>Suc n. \<exists>y. h a = \<lfloor>y\<rfloor>\<rbrakk> \<Longrightarrow> (h n = None \<longrightarrow> (LEAST a. n \<le> a \<and> h a = None) = n) \<and> h n = None
[PROOF STEP]
apply(subgoal_tac "a = n")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>n \<le> a; h a = None; \<forall>a\<ge>Suc n. \<exists>y. h a = \<lfloor>y\<rfloor>; a = n\<rbrakk> \<Longrightarrow> (h n = None \<longrightarrow> (LEAST a. n \<le> a \<and> h a = None) = n) \<and> h n = None
 2. \<And>a. \<lbrakk>n \<le> a; h a = None; \<forall>a\<ge>Suc n. \<exists>y. h a = \<lfloor>y\<rfloor>\<rbrakk> \<Longrightarrow> a = n
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>h n = None; \<forall>a\<ge>Suc n. \<exists>y. h a = \<lfloor>y\<rfloor>; a = n\<rbrakk> \<Longrightarrow> (LEAST a. n \<le> a \<and> h a = None) = n
 2. \<And>a. \<lbrakk>n \<le> a; h a = None; \<forall>a\<ge>Suc n. \<exists>y. h a = \<lfloor>y\<rfloor>\<rbrakk> \<Longrightarrow> a = n
[PROOF STEP]
apply(rule Least_equality)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a. \<lbrakk>h n = None; \<forall>a\<ge>Suc n. \<exists>y. h a = \<lfloor>y\<rfloor>; a = n\<rbrakk> \<Longrightarrow> n \<le> n \<and> h n = None
 2. \<And>a y. \<lbrakk>h n = None; \<forall>a\<ge>Suc n. \<exists>y. h a = \<lfloor>y\<rfloor>; a = n; n \<le> y \<and> h y = None\<rbrakk> \<Longrightarrow> n \<le> y
 3. \<And>a. \<lbrakk>n \<le> a; h a = None; \<forall>a\<ge>Suc n. \<exists>y. h a = \<lfloor>y\<rfloor>\<rbrakk> \<Longrightarrow> a = n
[PROOF STEP]
apply auto[2]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>n \<le> a; h a = None; \<forall>a\<ge>Suc n. \<exists>y. h a = \<lfloor>y\<rfloor>\<rbrakk> \<Longrightarrow> a = n
[PROOF STEP]
apply(rule ccontr)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>n \<le> a; h a = None; \<forall>a\<ge>Suc n. \<exists>y. h a = \<lfloor>y\<rfloor>; a \<noteq> n\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(erule_tac x="a" in allE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>n \<le> a; h a = None; a \<noteq> n; Suc n \<le> a \<longrightarrow> (\<exists>y. h a = \<lfloor>y\<rfloor>)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma lnull_lmirror_aux [simp]:
  "lnull (lmirror_aux acc xs) = (lnull xs \<and> lnull acc)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lnull (lmirror_aux acc xs) = (lnull xs \<and> lnull acc)
[PROOF STEP]
by(fact lmirror_aux.simps)


[STATEMENT]
lemma ltl_lmirror_aux:
  "ltl (lmirror_aux acc xs) = (if lnull xs then ltl acc else lmirror_aux (LCons (lhd xs) acc) (ltl xs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ltl (lmirror_aux acc xs) = (if lnull xs then ltl acc else lmirror_aux (LCons (lhd xs) acc) (ltl xs))
[PROOF STEP]
by(cases acc)(simp_all split: llist.split)


[STATEMENT]
lemma lhd_lmirror_aux:
  "lhd (lmirror_aux acc xs) = (if lnull xs then lhd acc else lhd xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lhd (lmirror_aux acc xs) = (if lnull xs then lhd acc else lhd xs)
[PROOF STEP]
by(cases acc)(simp_all split: llist.split)


[STATEMENT]
lemma lfinite_lmirror_aux [simp]:
  "lfinite (lmirror_aux acc xs) \<longleftrightarrow> lfinite xs \<and> lfinite acc"
  (is "?lhs \<longleftrightarrow> ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lfinite (lmirror_aux acc xs) = (lfinite xs \<and> lfinite acc)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. lfinite (lmirror_aux acc xs) \<Longrightarrow> lfinite xs \<and> lfinite acc
 2. lfinite xs \<and> lfinite acc \<Longrightarrow> lfinite (lmirror_aux acc xs)
[PROOF STEP]
assume ?lhs
[PROOF STATE]
proof (state)
this:
lfinite (lmirror_aux acc xs)

goal (2 subgoals):
 1. lfinite (lmirror_aux acc xs) \<Longrightarrow> lfinite xs \<and> lfinite acc
 2. lfinite xs \<and> lfinite acc \<Longrightarrow> lfinite (lmirror_aux acc xs)
[PROOF STEP]
thus ?rhs
[PROOF STATE]
proof (prove)
using this:
lfinite (lmirror_aux acc xs)

goal (1 subgoal):
 1. lfinite xs \<and> lfinite acc
[PROOF STEP]
proof(induct zs\<equiv>"lmirror_aux acc xs" arbitrary: acc xs rule: lfinite_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>acc xs. lnull (lmirror_aux acc xs) \<Longrightarrow> lfinite xs \<and> lfinite acc
 2. \<And>acc xs. \<lbrakk>lfinite (lmirror_aux acc xs); \<not> lnull (lmirror_aux acc xs); \<And>acca xsa. ltl (lmirror_aux acc xs) = lmirror_aux acca xsa \<Longrightarrow> lfinite xsa \<and> lfinite acca\<rbrakk> \<Longrightarrow> lfinite xs \<and> lfinite acc
[PROOF STEP]
case LCons
[PROOF STATE]
proof (state)
this:
lfinite (lmirror_aux acc xs)
\<not> lnull (lmirror_aux acc xs)
ltl (lmirror_aux acc xs) = lmirror_aux ?acc ?xs \<Longrightarrow> lfinite ?xs \<and> lfinite ?acc

goal (2 subgoals):
 1. \<And>acc xs. lnull (lmirror_aux acc xs) \<Longrightarrow> lfinite xs \<and> lfinite acc
 2. \<And>acc xs. \<lbrakk>lfinite (lmirror_aux acc xs); \<not> lnull (lmirror_aux acc xs); \<And>acca xsa. ltl (lmirror_aux acc xs) = lmirror_aux acca xsa \<Longrightarrow> lfinite xsa \<and> lfinite acca\<rbrakk> \<Longrightarrow> lfinite xs \<and> lfinite acc
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
lfinite (lmirror_aux acc xs)
\<not> lnull (lmirror_aux acc xs)
ltl (lmirror_aux acc xs) = lmirror_aux ?acc ?xs \<Longrightarrow> lfinite ?xs \<and> lfinite ?acc

goal (1 subgoal):
 1. lfinite xs \<and> lfinite acc
[PROOF STEP]
proof(cases "lnull xs")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>lfinite (lmirror_aux acc xs); \<not> lnull (lmirror_aux acc xs); \<And>acc xs. ltl (lmirror_aux acc xs) = lmirror_aux acc xs \<Longrightarrow> lfinite xs \<and> lfinite acc; lnull xs\<rbrakk> \<Longrightarrow> lfinite xs \<and> lfinite acc
 2. \<lbrakk>lfinite (lmirror_aux acc xs); \<not> lnull (lmirror_aux acc xs); \<And>acc xs. ltl (lmirror_aux acc xs) = lmirror_aux acc xs \<Longrightarrow> lfinite xs \<and> lfinite acc; \<not> lnull xs\<rbrakk> \<Longrightarrow> lfinite xs \<and> lfinite acc
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
lnull xs

goal (2 subgoals):
 1. \<lbrakk>lfinite (lmirror_aux acc xs); \<not> lnull (lmirror_aux acc xs); \<And>acc xs. ltl (lmirror_aux acc xs) = lmirror_aux acc xs \<Longrightarrow> lfinite xs \<and> lfinite acc; lnull xs\<rbrakk> \<Longrightarrow> lfinite xs \<and> lfinite acc
 2. \<lbrakk>lfinite (lmirror_aux acc xs); \<not> lnull (lmirror_aux acc xs); \<And>acc xs. ltl (lmirror_aux acc xs) = lmirror_aux acc xs \<Longrightarrow> lfinite xs \<and> lfinite acc; \<not> lnull xs\<rbrakk> \<Longrightarrow> lfinite xs \<and> lfinite acc
[PROOF STEP]
with LCons.hyps(3)[of "ltl acc" LNil]
[PROOF STATE]
proof (chain)
picking this:
ltl (lmirror_aux acc xs) = lmirror_aux (ltl acc) LNil \<Longrightarrow> lfinite LNil \<and> lfinite (ltl acc)
lnull xs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ltl (lmirror_aux acc xs) = lmirror_aux (ltl acc) LNil \<Longrightarrow> lfinite LNil \<and> lfinite (ltl acc)
lnull xs

goal (1 subgoal):
 1. lfinite xs \<and> lfinite acc
[PROOF STEP]
by(simp add: ltl_lmirror_aux)
[PROOF STATE]
proof (state)
this:
lfinite xs \<and> lfinite acc

goal (1 subgoal):
 1. \<lbrakk>lfinite (lmirror_aux acc xs); \<not> lnull (lmirror_aux acc xs); \<And>acc xs. ltl (lmirror_aux acc xs) = lmirror_aux acc xs \<Longrightarrow> lfinite xs \<and> lfinite acc; \<not> lnull xs\<rbrakk> \<Longrightarrow> lfinite xs \<and> lfinite acc
[PROOF STEP]
qed(fastforce simp add: ltl_lmirror_aux)
[PROOF STATE]
proof (state)
this:
lfinite xs \<and> lfinite acc

goal (1 subgoal):
 1. \<And>acc xs. lnull (lmirror_aux acc xs) \<Longrightarrow> lfinite xs \<and> lfinite acc
[PROOF STEP]
qed simp
[PROOF STATE]
proof (state)
this:
lfinite xs \<and> lfinite acc

goal (1 subgoal):
 1. lfinite xs \<and> lfinite acc \<Longrightarrow> lfinite (lmirror_aux acc xs)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lfinite xs \<and> lfinite acc \<Longrightarrow> lfinite (lmirror_aux acc xs)
[PROOF STEP]
assume ?rhs
[PROOF STATE]
proof (state)
this:
lfinite xs \<and> lfinite acc

goal (1 subgoal):
 1. lfinite xs \<and> lfinite acc \<Longrightarrow> lfinite (lmirror_aux acc xs)
[PROOF STEP]
hence "lfinite xs" "lfinite acc"
[PROOF STATE]
proof (prove)
using this:
lfinite xs \<and> lfinite acc

goal (1 subgoal):
 1. lfinite xs &&& lfinite acc
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
lfinite xs
lfinite acc

goal (1 subgoal):
 1. lfinite xs \<and> lfinite acc \<Longrightarrow> lfinite (lmirror_aux acc xs)
[PROOF STEP]
thus ?lhs
[PROOF STATE]
proof (prove)
using this:
lfinite xs
lfinite acc

goal (1 subgoal):
 1. lfinite (lmirror_aux acc xs)
[PROOF STEP]
by(induction arbitrary: acc) simp_all
[PROOF STATE]
proof (state)
this:
lfinite (lmirror_aux acc xs)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lmirror_aux_inf:
  "\<not> lfinite xs \<Longrightarrow> lmirror_aux acc xs = xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> lfinite xs \<Longrightarrow> lmirror_aux acc xs = xs
[PROOF STEP]
by(coinduction arbitrary: acc xs)(auto simp add: lhd_lmirror_aux ltl_lmirror_aux)


[STATEMENT]
lemma lmirror_aux_acc:
  "lmirror_aux (lappend ys zs) xs = lappend (lmirror_aux ys xs) zs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lmirror_aux (lappend ys zs) xs = lappend (lmirror_aux ys xs) zs
[PROOF STEP]
proof(cases "lfinite xs")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. lfinite xs \<Longrightarrow> lmirror_aux (lappend ys zs) xs = lappend (lmirror_aux ys xs) zs
 2. \<not> lfinite xs \<Longrightarrow> lmirror_aux (lappend ys zs) xs = lappend (lmirror_aux ys xs) zs
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> lfinite xs

goal (2 subgoals):
 1. lfinite xs \<Longrightarrow> lmirror_aux (lappend ys zs) xs = lappend (lmirror_aux ys xs) zs
 2. \<not> lfinite xs \<Longrightarrow> lmirror_aux (lappend ys zs) xs = lappend (lmirror_aux ys xs) zs
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> lfinite xs

goal (1 subgoal):
 1. lmirror_aux (lappend ys zs) xs = lappend (lmirror_aux ys xs) zs
[PROOF STEP]
by(simp add: lmirror_aux_inf lappend_inf)
[PROOF STATE]
proof (state)
this:
lmirror_aux (lappend ys zs) xs = lappend (lmirror_aux ys xs) zs

goal (1 subgoal):
 1. lfinite xs \<Longrightarrow> lmirror_aux (lappend ys zs) xs = lappend (lmirror_aux ys xs) zs
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lfinite xs \<Longrightarrow> lmirror_aux (lappend ys zs) xs = lappend (lmirror_aux ys xs) zs
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
lfinite xs

goal (1 subgoal):
 1. lfinite xs \<Longrightarrow> lmirror_aux (lappend ys zs) xs = lappend (lmirror_aux ys xs) zs
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
lfinite xs

goal (1 subgoal):
 1. lmirror_aux (lappend ys zs) xs = lappend (lmirror_aux ys xs) zs
[PROOF STEP]
by(induction arbitrary: ys)(simp_all add: lappend_code(2)[symmetric] del: lappend_code(2))
[PROOF STATE]
proof (state)
this:
lmirror_aux (lappend ys zs) xs = lappend (lmirror_aux ys xs) zs

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lmirror_aux_LCons:
  "lmirror_aux acc (LCons x xs) = LCons x (lappend (lmirror_aux LNil xs) (LCons x acc))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lmirror_aux acc (LCons x xs) = LCons x (lappend (lmirror_aux LNil xs) (LCons x acc))
[PROOF STEP]
by (metis lappend_code(1) lmirror_aux_acc lmirror_aux_simps(2))


[STATEMENT]
lemma llength_lmirror_aux: "llength (lmirror_aux acc xs) = 2 * llength xs + llength acc"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. llength (lmirror_aux acc xs) = 2 * llength xs + llength acc
[PROOF STEP]
apply(coinduction arbitrary: acc xs rule: enat_coinduct)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>acc xs. (llength (lmirror_aux acc xs) = 0) = (2 * llength xs + llength acc = 0) \<and> (llength (lmirror_aux acc xs) \<noteq> 0 \<longrightarrow> 2 * llength xs + llength acc \<noteq> 0 \<longrightarrow> (\<exists>acca xsa. epred (llength (lmirror_aux acc xs)) = llength (lmirror_aux acca xsa) \<and> epred (2 * llength xs + llength acc) = 2 * llength xsa + llength acca) \<or> epred (llength (lmirror_aux acc xs)) = epred (2 * llength xs + llength acc))
[PROOF STEP]
apply(auto simp add: iadd_is_0 epred_iadd1 mult_2 epred_llength ltl_lmirror_aux iadd_Suc_right)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>acc xs. \<lbrakk>\<not> lnull xs; llength (lmirror_aux (LCons (lhd xs) acc) (ltl xs)) \<noteq> llength (ltl xs) + llength xs + llength acc\<rbrakk> \<Longrightarrow> \<exists>acca xsa. llength (lmirror_aux (LCons (lhd xs) acc) (ltl xs)) = llength (lmirror_aux acca xsa) \<and> llength (ltl xs) + llength xs + llength acc = llength xsa + llength xsa + llength acca
[PROOF STEP]
apply(rule exI conjI refl)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>acc xs. \<lbrakk>\<not> lnull xs; llength (lmirror_aux (LCons (lhd xs) acc) (ltl xs)) \<noteq> llength (ltl xs) + llength xs + llength acc\<rbrakk> \<Longrightarrow> llength (ltl xs) + llength xs + llength acc = llength (ltl xs) + llength (ltl xs) + llength (LCons (lhd xs) acc)
[PROOF STEP]
apply(simp add: iadd_Suc_right llength_ltl)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>acc xs. \<lbrakk>\<not> lnull xs; llength (lmirror_aux (LCons (lhd xs) acc) (ltl xs)) \<noteq> epred (llength xs) + llength xs + llength acc\<rbrakk> \<Longrightarrow> epred (llength xs) + llength xs + llength acc = eSuc (epred (llength xs) + epred (llength xs) + llength acc)
[PROOF STEP]
by (metis (opaque_lifting, no_types) add.commute epred_llength iadd_Suc_right lhd_LCons_ltl llength_LCons)


[STATEMENT]
lemma lnull_lmirror [simp]: "lnull (lmirror xs) = lnull xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lnull (lmirror xs) = lnull xs
[PROOF STEP]
by(simp add: lmirror_def)


[STATEMENT]
lemma lmirror_LNil [simp]: "lmirror LNil = LNil"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lmirror LNil = LNil
[PROOF STEP]
by(simp add: lmirror_def)


[STATEMENT]
lemma lmirror_LCons [simp]: "lmirror (LCons x xs) = LCons x (lappend (lmirror xs) (LCons x LNil))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lmirror (LCons x xs) = LCons x (lappend (lmirror xs) (LCons x LNil))
[PROOF STEP]
by(simp only: lmirror_aux_LCons lmirror_def)


[STATEMENT]
lemma ltl_lmirror [simp]:
  "\<not> lnull xs \<Longrightarrow> ltl (lmirror xs) = lappend (lmirror (ltl xs)) (LCons (lhd xs) LNil)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> lnull xs \<Longrightarrow> ltl (lmirror xs) = lappend (lmirror (ltl xs)) (LCons (lhd xs) LNil)
[PROOF STEP]
by(clarsimp simp add: not_lnull_conv)


[STATEMENT]
lemma lmap_lmirror_aux: "lmap f (lmirror_aux acc xs) = lmirror_aux (lmap f acc) (lmap f xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lmap f (lmirror_aux acc xs) = lmirror_aux (lmap f acc) (lmap f xs)
[PROOF STEP]
by(coinduction arbitrary: acc xs rule: llist.coinduct_strong)(auto 4 3 simp add: lhd_lmirror_aux ltl_lmirror_aux)


[STATEMENT]
lemma lset_lmirror_aux: "lset (lmirror_aux acc xs) = lset (lappend xs acc)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lset (lmirror_aux acc xs) = lset (lappend xs acc)
[PROOF STEP]
proof(cases "lfinite xs")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. lfinite xs \<Longrightarrow> lset (lmirror_aux acc xs) = lset (lappend xs acc)
 2. \<not> lfinite xs \<Longrightarrow> lset (lmirror_aux acc xs) = lset (lappend xs acc)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
lfinite xs

goal (2 subgoals):
 1. lfinite xs \<Longrightarrow> lset (lmirror_aux acc xs) = lset (lappend xs acc)
 2. \<not> lfinite xs \<Longrightarrow> lset (lmirror_aux acc xs) = lset (lappend xs acc)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
lfinite xs

goal (1 subgoal):
 1. lset (lmirror_aux acc xs) = lset (lappend xs acc)
[PROOF STEP]
by(induction arbitrary: acc) simp_all
[PROOF STATE]
proof (state)
this:
lset (lmirror_aux acc xs) = lset (lappend xs acc)

goal (1 subgoal):
 1. \<not> lfinite xs \<Longrightarrow> lset (lmirror_aux acc xs) = lset (lappend xs acc)
[PROOF STEP]
qed(simp add: lmirror_aux_inf lappend_inf)


[STATEMENT]
lemma lset_lmirror [simp]: "lset (lmirror xs) = lset xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lset (lmirror xs) = lset xs
[PROOF STEP]
by(simp add: lmirror_def lset_lmirror_aux)


[STATEMENT]
lemma llength_lmirror [simp]: "llength (lmirror xs) = 2 * llength xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. llength (lmirror xs) = 2 * llength xs
[PROOF STEP]
by(simp add: lmirror_def llength_lmirror_aux)


[STATEMENT]
lemma list_of_lmirror [simp]: "lfinite xs \<Longrightarrow> list_of (lmirror xs) = list_of xs @ rev (list_of xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lfinite xs \<Longrightarrow> list_of (lmirror xs) = list_of xs @ rev (list_of xs)
[PROOF STEP]
by (metis list_of_llist_of llist_of_list_of lmirror_llist_of)


[STATEMENT]
lemma llist_all2_lmirror_aux:
  "\<lbrakk> llist_all2 P acc acc'; llist_all2 P xs xs' \<rbrakk>
  \<Longrightarrow> llist_all2 P (lmirror_aux acc xs) (lmirror_aux acc' xs')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>llist_all2 P acc acc'; llist_all2 P xs xs'\<rbrakk> \<Longrightarrow> llist_all2 P (lmirror_aux acc xs) (lmirror_aux acc' xs')
[PROOF STEP]
by(coinduction arbitrary: acc acc' xs xs')(auto simp add: lhd_lmirror_aux ltl_lmirror_aux elim: llist_all2_lhdD intro!: llist_all2_ltlI exI dest: llist_all2_lnullD)


[STATEMENT]
lemma enat_mult_cancel1 [simp]:
  "k * m = k * n \<longleftrightarrow> m = n \<or> k = 0 \<or> k = (\<infinity> :: enat) \<and> n \<noteq> 0 \<and> m \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (k * m = k * n) = (m = n \<or> k = 0 \<or> k = \<infinity> \<and> n \<noteq> 0 \<and> m \<noteq> 0)
[PROOF STEP]
by(cases k m n rule: enat.exhaust[case_product enat.exhaust[case_product enat.exhaust]])(simp_all add: zero_enat_def)


[STATEMENT]
lemma llist_all2_lmirror_auxD:
  "\<lbrakk> llist_all2 P (lmirror_aux acc xs) (lmirror_aux acc' xs'); llist_all2 P acc acc'; lfinite acc \<rbrakk>
  \<Longrightarrow> llist_all2 P xs xs'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>llist_all2 P (lmirror_aux acc xs) (lmirror_aux acc' xs'); llist_all2 P acc acc'; lfinite acc\<rbrakk> \<Longrightarrow> llist_all2 P xs xs'
[PROOF STEP]
proof(coinduction arbitrary: xs xs' acc acc')
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>xsa xs' acc acc'. \<lbrakk>llist_all2 P (lmirror_aux acc xsa) (lmirror_aux acc' xs'); llist_all2 P acc acc'; lfinite acc\<rbrakk> \<Longrightarrow> lnull xsa = lnull xs'
 2. \<And>xsa xs' acc acc'. \<lbrakk>llist_all2 P (lmirror_aux acc xsa) (lmirror_aux acc' xs'); llist_all2 P acc acc'; lfinite acc; \<not> lnull xsa; \<not> lnull xs'\<rbrakk> \<Longrightarrow> P (lhd xsa) (lhd xs') \<and> ((\<exists>xs xs'a acc acc'. ltl xsa = xs \<and> ltl xs' = xs'a \<and> llist_all2 P (lmirror_aux acc xs) (lmirror_aux acc' xs'a) \<and> llist_all2 P acc acc' \<and> lfinite acc) \<or> llist_all2 P (ltl xsa) (ltl xs'))
[PROOF STEP]
case (LNil xs xs' acc acc')
[PROOF STATE]
proof (state)
this:
llist_all2 P (lmirror_aux acc xs) (lmirror_aux acc' xs')
llist_all2 P acc acc'
lfinite acc

goal (2 subgoals):
 1. \<And>xsa xs' acc acc'. \<lbrakk>llist_all2 P (lmirror_aux acc xsa) (lmirror_aux acc' xs'); llist_all2 P acc acc'; lfinite acc\<rbrakk> \<Longrightarrow> lnull xsa = lnull xs'
 2. \<And>xsa xs' acc acc'. \<lbrakk>llist_all2 P (lmirror_aux acc xsa) (lmirror_aux acc' xs'); llist_all2 P acc acc'; lfinite acc; \<not> lnull xsa; \<not> lnull xs'\<rbrakk> \<Longrightarrow> P (lhd xsa) (lhd xs') \<and> ((\<exists>xs xs'a acc acc'. ltl xsa = xs \<and> ltl xs' = xs'a \<and> llist_all2 P (lmirror_aux acc xs) (lmirror_aux acc' xs'a) \<and> llist_all2 P acc acc' \<and> lfinite acc) \<or> llist_all2 P (ltl xsa) (ltl xs'))
[PROOF STEP]
from \<open>llist_all2 P (lmirror_aux acc xs) (lmirror_aux acc' xs')\<close>
[PROOF STATE]
proof (chain)
picking this:
llist_all2 P (lmirror_aux acc xs) (lmirror_aux acc' xs')
[PROOF STEP]
have "llength (lmirror_aux acc xs) = llength (lmirror_aux acc' xs')"
[PROOF STATE]
proof (prove)
using this:
llist_all2 P (lmirror_aux acc xs) (lmirror_aux acc' xs')

goal (1 subgoal):
 1. llength (lmirror_aux acc xs) = llength (lmirror_aux acc' xs')
[PROOF STEP]
by(rule llist_all2_llengthD)
[PROOF STATE]
proof (state)
this:
llength (lmirror_aux acc xs) = llength (lmirror_aux acc' xs')

goal (2 subgoals):
 1. \<And>xsa xs' acc acc'. \<lbrakk>llist_all2 P (lmirror_aux acc xsa) (lmirror_aux acc' xs'); llist_all2 P acc acc'; lfinite acc\<rbrakk> \<Longrightarrow> lnull xsa = lnull xs'
 2. \<And>xsa xs' acc acc'. \<lbrakk>llist_all2 P (lmirror_aux acc xsa) (lmirror_aux acc' xs'); llist_all2 P acc acc'; lfinite acc; \<not> lnull xsa; \<not> lnull xs'\<rbrakk> \<Longrightarrow> P (lhd xsa) (lhd xs') \<and> ((\<exists>xs xs'a acc acc'. ltl xsa = xs \<and> ltl xs' = xs'a \<and> llist_all2 P (lmirror_aux acc xs) (lmirror_aux acc' xs'a) \<and> llist_all2 P acc acc' \<and> lfinite acc) \<or> llist_all2 P (ltl xsa) (ltl xs'))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
llength (lmirror_aux acc xs) = llength (lmirror_aux acc' xs')

goal (2 subgoals):
 1. \<And>xsa xs' acc acc'. \<lbrakk>llist_all2 P (lmirror_aux acc xsa) (lmirror_aux acc' xs'); llist_all2 P acc acc'; lfinite acc\<rbrakk> \<Longrightarrow> lnull xsa = lnull xs'
 2. \<And>xsa xs' acc acc'. \<lbrakk>llist_all2 P (lmirror_aux acc xsa) (lmirror_aux acc' xs'); llist_all2 P acc acc'; lfinite acc; \<not> lnull xsa; \<not> lnull xs'\<rbrakk> \<Longrightarrow> P (lhd xsa) (lhd xs') \<and> ((\<exists>xs xs'a acc acc'. ltl xsa = xs \<and> ltl xs' = xs'a \<and> llist_all2 P (lmirror_aux acc xs) (lmirror_aux acc' xs'a) \<and> llist_all2 P acc acc' \<and> lfinite acc) \<or> llist_all2 P (ltl xsa) (ltl xs'))
[PROOF STEP]
from \<open>llist_all2 P acc acc'\<close>
[PROOF STATE]
proof (chain)
picking this:
llist_all2 P acc acc'
[PROOF STEP]
have "llength acc = llength acc'"
[PROOF STATE]
proof (prove)
using this:
llist_all2 P acc acc'

goal (1 subgoal):
 1. llength acc = llength acc'
[PROOF STEP]
by(rule llist_all2_llengthD)
[PROOF STATE]
proof (state)
this:
llength acc = llength acc'

goal (2 subgoals):
 1. \<And>xsa xs' acc acc'. \<lbrakk>llist_all2 P (lmirror_aux acc xsa) (lmirror_aux acc' xs'); llist_all2 P acc acc'; lfinite acc\<rbrakk> \<Longrightarrow> lnull xsa = lnull xs'
 2. \<And>xsa xs' acc acc'. \<lbrakk>llist_all2 P (lmirror_aux acc xsa) (lmirror_aux acc' xs'); llist_all2 P acc acc'; lfinite acc; \<not> lnull xsa; \<not> lnull xs'\<rbrakk> \<Longrightarrow> P (lhd xsa) (lhd xs') \<and> ((\<exists>xs xs'a acc acc'. ltl xsa = xs \<and> ltl xs' = xs'a \<and> llist_all2 P (lmirror_aux acc xs) (lmirror_aux acc' xs'a) \<and> llist_all2 P acc acc' \<and> lfinite acc) \<or> llist_all2 P (ltl xsa) (ltl xs'))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
llength (lmirror_aux acc xs) = llength (lmirror_aux acc' xs')
llength acc = llength acc'
[PROOF STEP]
have "llength xs = llength xs'"
[PROOF STATE]
proof (prove)
using this:
llength (lmirror_aux acc xs) = llength (lmirror_aux acc' xs')
llength acc = llength acc'

goal (1 subgoal):
 1. llength xs = llength xs'
[PROOF STEP]
using \<open>lfinite acc\<close>
[PROOF STATE]
proof (prove)
using this:
llength (lmirror_aux acc xs) = llength (lmirror_aux acc' xs')
llength acc = llength acc'
lfinite acc

goal (1 subgoal):
 1. llength xs = llength xs'
[PROOF STEP]
by(auto simp add: llength_lmirror_aux dest: lfinite_llength_enat)
[PROOF STATE]
proof (state)
this:
llength xs = llength xs'

goal (2 subgoals):
 1. \<And>xsa xs' acc acc'. \<lbrakk>llist_all2 P (lmirror_aux acc xsa) (lmirror_aux acc' xs'); llist_all2 P acc acc'; lfinite acc\<rbrakk> \<Longrightarrow> lnull xsa = lnull xs'
 2. \<And>xsa xs' acc acc'. \<lbrakk>llist_all2 P (lmirror_aux acc xsa) (lmirror_aux acc' xs'); llist_all2 P acc acc'; lfinite acc; \<not> lnull xsa; \<not> lnull xs'\<rbrakk> \<Longrightarrow> P (lhd xsa) (lhd xs') \<and> ((\<exists>xs xs'a acc acc'. ltl xsa = xs \<and> ltl xs' = xs'a \<and> llist_all2 P (lmirror_aux acc xs) (lmirror_aux acc' xs'a) \<and> llist_all2 P acc acc' \<and> lfinite acc) \<or> llist_all2 P (ltl xsa) (ltl xs'))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
llength xs = llength xs'

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

goal (1 subgoal):
 1. \<And>xsa xs' acc acc'. \<lbrakk>llist_all2 P (lmirror_aux acc xsa) (lmirror_aux acc' xs'); llist_all2 P acc acc'; lfinite acc; \<not> lnull xsa; \<not> lnull xs'\<rbrakk> \<Longrightarrow> P (lhd xsa) (lhd xs') \<and> ((\<exists>xs xs'a acc acc'. ltl xsa = xs \<and> ltl xs' = xs'a \<and> llist_all2 P (lmirror_aux acc xs) (lmirror_aux acc' xs'a) \<and> llist_all2 P acc acc' \<and> lfinite acc) \<or> llist_all2 P (ltl xsa) (ltl xs'))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xsa xs' acc acc'. \<lbrakk>llist_all2 P (lmirror_aux acc xsa) (lmirror_aux acc' xs'); llist_all2 P acc acc'; lfinite acc; \<not> lnull xsa; \<not> lnull xs'\<rbrakk> \<Longrightarrow> P (lhd xsa) (lhd xs') \<and> ((\<exists>xs xs'a acc acc'. ltl xsa = xs \<and> ltl xs' = xs'a \<and> llist_all2 P (lmirror_aux acc xs) (lmirror_aux acc' xs'a) \<and> llist_all2 P acc acc' \<and> lfinite acc) \<or> llist_all2 P (ltl xsa) (ltl xs'))
[PROOF STEP]
case (LCons xs xs' acc acc')
[PROOF STATE]
proof (state)
this:
llist_all2 P (lmirror_aux acc xs) (lmirror_aux acc' xs')
llist_all2 P acc acc'
lfinite acc
\<not> lnull xs
\<not> lnull xs'

goal (1 subgoal):
 1. \<And>xsa xs' acc acc'. \<lbrakk>llist_all2 P (lmirror_aux acc xsa) (lmirror_aux acc' xs'); llist_all2 P acc acc'; lfinite acc; \<not> lnull xsa; \<not> lnull xs'\<rbrakk> \<Longrightarrow> P (lhd xsa) (lhd xs') \<and> ((\<exists>xs xs'a acc acc'. ltl xsa = xs \<and> ltl xs' = xs'a \<and> llist_all2 P (lmirror_aux acc xs) (lmirror_aux acc' xs'a) \<and> llist_all2 P acc acc' \<and> lfinite acc) \<or> llist_all2 P (ltl xsa) (ltl xs'))
[PROOF STEP]
from \<open>llist_all2 P (lmirror_aux acc xs) (lmirror_aux acc' xs')\<close> \<open>\<not> lnull xs\<close> \<open>\<not> lnull xs'\<close>
[PROOF STATE]
proof (chain)
picking this:
llist_all2 P (lmirror_aux acc xs) (lmirror_aux acc' xs')
\<not> lnull xs
\<not> lnull xs'
[PROOF STEP]
have ?lhd
[PROOF STATE]
proof (prove)
using this:
llist_all2 P (lmirror_aux acc xs) (lmirror_aux acc' xs')
\<not> lnull xs
\<not> lnull xs'

goal (1 subgoal):
 1. P (lhd xs) (lhd xs')
[PROOF STEP]
by(auto dest: llist_all2_lhdD simp add: lhd_lmirror_aux)
[PROOF STATE]
proof (state)
this:
P (lhd xs) (lhd xs')

goal (1 subgoal):
 1. \<And>xsa xs' acc acc'. \<lbrakk>llist_all2 P (lmirror_aux acc xsa) (lmirror_aux acc' xs'); llist_all2 P acc acc'; lfinite acc; \<not> lnull xsa; \<not> lnull xs'\<rbrakk> \<Longrightarrow> P (lhd xsa) (lhd xs') \<and> ((\<exists>xs xs'a acc acc'. ltl xsa = xs \<and> ltl xs' = xs'a \<and> llist_all2 P (lmirror_aux acc xs) (lmirror_aux acc' xs'a) \<and> llist_all2 P acc acc' \<and> lfinite acc) \<or> llist_all2 P (ltl xsa) (ltl xs'))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
P (lhd xs) (lhd xs')

goal (1 subgoal):
 1. P (lhd xs) (lhd xs') \<and> ((\<exists>xs xs' acc acc'. ltl xs = xs \<and> ltl xs' = xs' \<and> llist_all2 P (lmirror_aux acc xs) (lmirror_aux acc' xs') \<and> llist_all2 P acc acc' \<and> lfinite acc) \<or> llist_all2 P (ltl xs) (ltl xs'))
[PROOF STEP]
using LCons \<open>llist_all2 P (lmirror_aux acc xs) (lmirror_aux acc' xs')\<close>[THEN llist_all2_ltlI]
[PROOF STATE]
proof (prove)
using this:
P (lhd xs) (lhd xs')
llist_all2 P (lmirror_aux acc xs) (lmirror_aux acc' xs')
llist_all2 P acc acc'
lfinite acc
\<not> lnull xs
\<not> lnull xs'
llist_all2 P (ltl (lmirror_aux acc xs)) (ltl (lmirror_aux acc' xs'))

goal (1 subgoal):
 1. P (lhd xs) (lhd xs') \<and> ((\<exists>xs xs' acc acc'. ltl xs = xs \<and> ltl xs' = xs' \<and> llist_all2 P (lmirror_aux acc xs) (lmirror_aux acc' xs') \<and> llist_all2 P acc acc' \<and> lfinite acc) \<or> llist_all2 P (ltl xs) (ltl xs'))
[PROOF STEP]
by(auto 4 3 simp add: ltl_lmirror_aux)
[PROOF STATE]
proof (state)
this:
P (lhd xs) (lhd xs') \<and> ((\<exists>xs xs' acc acc'. ltl xs = xs \<and> ltl xs' = xs' \<and> llist_all2 P (lmirror_aux acc xs) (lmirror_aux acc' xs') \<and> llist_all2 P acc acc' \<and> lfinite acc) \<or> llist_all2 P (ltl xs) (ltl xs'))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma llist_all2_lmirrorI:
  "llist_all2 P xs ys \<Longrightarrow> llist_all2 P (lmirror xs) (lmirror ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. llist_all2 P xs ys \<Longrightarrow> llist_all2 P (lmirror xs) (lmirror ys)
[PROOF STEP]
by(simp add: lmirror_def llist_all2_lmirror_aux)


[STATEMENT]
lemma llist_all2_lmirrorD:
  "llist_all2 P (lmirror xs) (lmirror ys) \<Longrightarrow> llist_all2 P xs ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. llist_all2 P (lmirror xs) (lmirror ys) \<Longrightarrow> llist_all2 P xs ys
[PROOF STEP]
unfolding lmirror_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. llist_all2 P (lmirror_aux LNil xs) (lmirror_aux LNil ys) \<Longrightarrow> llist_all2 P xs ys
[PROOF STEP]
by(erule llist_all2_lmirror_auxD) simp_all


[STATEMENT]
lemma llist_all2_lmirror [simp]:
  "llist_all2 P (lmirror xs) (lmirror ys) \<longleftrightarrow> llist_all2 P xs ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. llist_all2 P (lmirror xs) (lmirror ys) = llist_all2 P xs ys
[PROOF STEP]
by(blast intro: llist_all2_lmirrorI llist_all2_lmirrorD)


[STATEMENT]
lemma lmirror_parametric [transfer_rule]:
  includes lifting_syntax
  shows "(llist_all2 A ===> llist_all2 A) lmirror lmirror"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (llist_all2 A ===> llist_all2 A) lmirror lmirror
[PROOF STEP]
by(rule rel_funI)(rule llist_all2_lmirrorI)


[STATEMENT]
lemma none_MT_rules_vs_notMT: "none_MT_rules  C p \<Longrightarrow> p \<noteq> [] \<Longrightarrow> not_MT C p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>none_MT_rules C p; p \<noteq> []\<rbrakk> \<Longrightarrow> not_MT C p
[PROOF STEP]
apply (induct p)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>none_MT_rules C []; [] \<noteq> []\<rbrakk> \<Longrightarrow> not_MT C []
 2. \<And>a p. \<lbrakk>\<lbrakk>none_MT_rules C p; p \<noteq> []\<rbrakk> \<Longrightarrow> not_MT C p; none_MT_rules C (a # p); a # p \<noteq> []\<rbrakk> \<Longrightarrow> not_MT C (a # p)
[PROOF STEP]
apply (simp_all)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma rmnMT: "none_MT_rules C (rm_MT_rules C p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. none_MT_rules C (rm_MT_rules C p)
[PROOF STEP]
apply (induct p)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. none_MT_rules C (rm_MT_rules C [])
 2. \<And>a p. none_MT_rules C (rm_MT_rules C p) \<Longrightarrow> none_MT_rules C (rm_MT_rules C (a # p))
[PROOF STEP]
apply (simp_all)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma rmnMT2: "none_MT_rules C  p \<Longrightarrow>  (rm_MT_rules C p) = p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. none_MT_rules C p \<Longrightarrow> rm_MT_rules C p = p
[PROOF STEP]
apply (induct p)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. none_MT_rules C [] \<Longrightarrow> rm_MT_rules C [] = []
 2. \<And>a p. \<lbrakk>none_MT_rules C p \<Longrightarrow> rm_MT_rules C p = p; none_MT_rules C (a # p)\<rbrakk> \<Longrightarrow> rm_MT_rules C (a # p) = a # p
[PROOF STEP]
apply (simp_all)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma nMTcharn: "none_MT_rules C p = (\<forall> r \<in> set p. dom (C r) \<noteq> {})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. none_MT_rules C p = (\<forall>r\<in>set p. dom (C r) \<noteq> {})
[PROOF STEP]
apply (induct p)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. none_MT_rules C [] = (\<forall>r\<in>set []. dom (C r) \<noteq> {})
 2. \<And>a p. none_MT_rules C p = (\<forall>r\<in>set p. dom (C r) \<noteq> {}) \<Longrightarrow> none_MT_rules C (a # p) = (\<forall>r\<in>set (a # p). dom (C r) \<noteq> {})
[PROOF STEP]
apply (simp_all)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma nMTeqSet: "set p = set s \<Longrightarrow> none_MT_rules C p = none_MT_rules C s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set p = set s \<Longrightarrow> none_MT_rules C p = none_MT_rules C s
[PROOF STEP]
apply (simp add: nMTcharn)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma notMTnMT: "\<lbrakk>a \<in> set p; none_MT_rules C p\<rbrakk> \<Longrightarrow> dom (C a) \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> set p; none_MT_rules C p\<rbrakk> \<Longrightarrow> dom (C a) \<noteq> {}
[PROOF STEP]
apply (simp add: nMTcharn)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma none_MT_rulesconc: "none_MT_rules C (a@[b]) \<Longrightarrow> none_MT_rules C a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. none_MT_rules C (a @ [b]) \<Longrightarrow> none_MT_rules C a
[PROOF STEP]
apply (induct a)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. none_MT_rules C ([] @ [b]) \<Longrightarrow> none_MT_rules C []
 2. \<And>a1 a2. \<lbrakk>none_MT_rules C (a2 @ [b]) \<Longrightarrow> none_MT_rules C a2; none_MT_rules C ((a1 # a2) @ [b])\<rbrakk> \<Longrightarrow> none_MT_rules C (a1 # a2)
[PROOF STEP]
apply (simp_all)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma nMTtail: "none_MT_rules C p \<Longrightarrow> none_MT_rules C (tl p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. none_MT_rules C p \<Longrightarrow> none_MT_rules C (tl p)
[PROOF STEP]
apply (induct p)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. none_MT_rules C [] \<Longrightarrow> none_MT_rules C (tl [])
 2. \<And>a p. \<lbrakk>none_MT_rules C p \<Longrightarrow> none_MT_rules C (tl p); none_MT_rules C (a # p)\<rbrakk> \<Longrightarrow> none_MT_rules C (tl (a # p))
[PROOF STEP]
apply (simp_all)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma not_MTimpnotMT[simp]: "not_MT C p \<Longrightarrow> p \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. not_MT C p \<Longrightarrow> p \<noteq> []
[PROOF STEP]
apply (auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma SR3nMT: "\<not> not_MT C  p \<Longrightarrow> rm_MT_rules C p = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> not_MT C p \<Longrightarrow> rm_MT_rules C p = []
[PROOF STEP]
apply (induct p)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<not> not_MT C [] \<Longrightarrow> rm_MT_rules C [] = []
 2. \<And>a p. \<lbrakk>\<not> not_MT C p \<Longrightarrow> rm_MT_rules C p = []; \<not> not_MT C (a # p)\<rbrakk> \<Longrightarrow> rm_MT_rules C (a # p) = []
[PROOF STEP]
apply (auto simp: if_splits)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma NMPcharn: "\<lbrakk>a \<in> set p; dom (C a) \<noteq> {}\<rbrakk> \<Longrightarrow> not_MT C  p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> set p; dom (C a) \<noteq> {}\<rbrakk> \<Longrightarrow> not_MT C p
[PROOF STEP]
apply (induct p)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a \<in> set []; dom (C a) \<noteq> {}\<rbrakk> \<Longrightarrow> not_MT C []
 2. \<And>aa p. \<lbrakk>\<lbrakk>a \<in> set p; dom (C a) \<noteq> {}\<rbrakk> \<Longrightarrow> not_MT C p; a \<in> set (aa # p); dom (C a) \<noteq> {}\<rbrakk> \<Longrightarrow> not_MT C (aa # p)
[PROOF STEP]
apply (auto simp: if_splits)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma NMPrm: "not_MT C  p \<Longrightarrow> not_MT C (rm_MT_rules C p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. not_MT C p \<Longrightarrow> not_MT C (rm_MT_rules C p)
[PROOF STEP]
apply (induct p)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. not_MT C [] \<Longrightarrow> not_MT C (rm_MT_rules C [])
 2. \<And>a p. \<lbrakk>not_MT C p \<Longrightarrow> not_MT C (rm_MT_rules C p); not_MT C (a # p)\<rbrakk> \<Longrightarrow> not_MT C (rm_MT_rules C (a # p))
[PROOF STEP]
apply (simp_all)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma mrconc: "applied_rule_rev C x p = Some a \<Longrightarrow> applied_rule_rev C x (b#p) = Some a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. applied_rule_rev C x p = \<lfloor>a\<rfloor> \<Longrightarrow> applied_rule_rev C x (b # p) = \<lfloor>a\<rfloor>
[PROOF STEP]
proof (induct p rule: rev_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. applied_rule_rev C x [] = \<lfloor>a\<rfloor> \<Longrightarrow> applied_rule_rev C x [b] = \<lfloor>a\<rfloor>
 2. \<And>xa xs. \<lbrakk>applied_rule_rev C x xs = \<lfloor>a\<rfloor> \<Longrightarrow> applied_rule_rev C x (b # xs) = \<lfloor>a\<rfloor>; applied_rule_rev C x (xs @ [xa]) = \<lfloor>a\<rfloor>\<rbrakk> \<Longrightarrow> applied_rule_rev C x (b # xs @ [xa]) = \<lfloor>a\<rfloor>
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
applied_rule_rev C x [] = \<lfloor>a\<rfloor>

goal (2 subgoals):
 1. applied_rule_rev C x [] = \<lfloor>a\<rfloor> \<Longrightarrow> applied_rule_rev C x [b] = \<lfloor>a\<rfloor>
 2. \<And>xa xs. \<lbrakk>applied_rule_rev C x xs = \<lfloor>a\<rfloor> \<Longrightarrow> applied_rule_rev C x (b # xs) = \<lfloor>a\<rfloor>; applied_rule_rev C x (xs @ [xa]) = \<lfloor>a\<rfloor>\<rbrakk> \<Longrightarrow> applied_rule_rev C x (b # xs @ [xa]) = \<lfloor>a\<rfloor>
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. applied_rule_rev C x [b] = \<lfloor>a\<rfloor>
[PROOF STEP]
using Nil
[PROOF STATE]
proof (prove)
using this:
applied_rule_rev C x [] = \<lfloor>a\<rfloor>

goal (1 subgoal):
 1. applied_rule_rev C x [b] = \<lfloor>a\<rfloor>
[PROOF STEP]
by (simp add: applied_rule_rev_def)
[PROOF STATE]
proof (state)
this:
applied_rule_rev C x [b] = \<lfloor>a\<rfloor>

goal (1 subgoal):
 1. \<And>xa xs. \<lbrakk>applied_rule_rev C x xs = \<lfloor>a\<rfloor> \<Longrightarrow> applied_rule_rev C x (b # xs) = \<lfloor>a\<rfloor>; applied_rule_rev C x (xs @ [xa]) = \<lfloor>a\<rfloor>\<rbrakk> \<Longrightarrow> applied_rule_rev C x (b # xs @ [xa]) = \<lfloor>a\<rfloor>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa xs. \<lbrakk>applied_rule_rev C x xs = \<lfloor>a\<rfloor> \<Longrightarrow> applied_rule_rev C x (b # xs) = \<lfloor>a\<rfloor>; applied_rule_rev C x (xs @ [xa]) = \<lfloor>a\<rfloor>\<rbrakk> \<Longrightarrow> applied_rule_rev C x (b # xs @ [xa]) = \<lfloor>a\<rfloor>
[PROOF STEP]
case (snoc xs x)
[PROOF STATE]
proof (state)
this:
applied_rule_rev C x x = \<lfloor>a\<rfloor> \<Longrightarrow> applied_rule_rev C x (b # x) = \<lfloor>a\<rfloor>
applied_rule_rev C x (x @ [xs]) = \<lfloor>a\<rfloor>

goal (1 subgoal):
 1. \<And>xa xs. \<lbrakk>applied_rule_rev C x xs = \<lfloor>a\<rfloor> \<Longrightarrow> applied_rule_rev C x (b # xs) = \<lfloor>a\<rfloor>; applied_rule_rev C x (xs @ [xa]) = \<lfloor>a\<rfloor>\<rbrakk> \<Longrightarrow> applied_rule_rev C x (b # xs @ [xa]) = \<lfloor>a\<rfloor>
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. applied_rule_rev C x (b # x @ [xs]) = \<lfloor>a\<rfloor>
[PROOF STEP]
using snoc
[PROOF STATE]
proof (prove)
using this:
applied_rule_rev C x x = \<lfloor>a\<rfloor> \<Longrightarrow> applied_rule_rev C x (b # x) = \<lfloor>a\<rfloor>
applied_rule_rev C x (x @ [xs]) = \<lfloor>a\<rfloor>

goal (1 subgoal):
 1. applied_rule_rev C x (b # x @ [xs]) = \<lfloor>a\<rfloor>
[PROOF STEP]
apply (simp add: applied_rule_rev_def if_splits)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>applied_rule C x (rev x) = \<lfloor>a\<rfloor> \<Longrightarrow> applied_rule C x (rev x @ [b]) = \<lfloor>a\<rfloor>; (if x \<in> dom (C xs) then \<lfloor>xs\<rfloor> else applied_rule C x (rev x)) = \<lfloor>a\<rfloor>\<rbrakk> \<Longrightarrow> (x \<in> dom (C xs) \<longrightarrow> xs = a) \<and> (x \<notin> dom (C xs) \<longrightarrow> applied_rule C x (rev x @ [b]) = \<lfloor>a\<rfloor>)
[PROOF STEP]
by (metis option.inject)
[PROOF STATE]
proof (state)
this:
applied_rule_rev C x (b # x @ [xs]) = \<lfloor>a\<rfloor>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mreq_end: "\<lbrakk>applied_rule_rev C x b = Some r; applied_rule_rev C x c = Some r\<rbrakk> \<Longrightarrow>
 applied_rule_rev C x (a#b) = applied_rule_rev C x (a#c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>applied_rule_rev C x b = \<lfloor>r\<rfloor>; applied_rule_rev C x c = \<lfloor>r\<rfloor>\<rbrakk> \<Longrightarrow> applied_rule_rev C x (a # b) = applied_rule_rev C x (a # c)
[PROOF STEP]
by (simp add: mrconc)