[STATEMENT]
lemma containID:
assumes a:"At i xs \<in># \<Gamma> \<and> At i xs \<in># \<Delta>"
    and b:"Ax \<subseteq> R"
shows "(\<Gamma> \<Rightarrow>* \<Delta>,0) \<in> derivable R*"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ( \<Gamma> \<Rightarrow>* \<Delta>, 0) \<in> derivable  R*
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ( \<Gamma> \<Rightarrow>* \<Delta>, 0) \<in> derivable  R*
[PROOF STEP]
from a
[PROOF STATE]
proof (chain)
picking this:
At i xs \<in># \<Gamma> \<and> At i xs \<in># \<Delta>
[PROOF STEP]
have "\<Gamma> = \<Gamma> \<ominus> At i xs \<oplus> At i xs \<and> \<Delta> = \<Delta> \<ominus> At i xs \<oplus> At i xs"
[PROOF STATE]
proof (prove)
using this:
At i xs \<in># \<Gamma> \<and> At i xs \<in># \<Delta>

goal (1 subgoal):
 1. \<Gamma> = \<Gamma> \<ominus> At i xs \<oplus> At i xs \<and> \<Delta> = \<Delta> \<ominus> At i xs \<oplus> At i xs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<Gamma> = \<Gamma> \<ominus> At i xs \<oplus> At i xs \<and> \<Delta> = \<Delta> \<ominus> At i xs \<oplus> At i xs

goal (1 subgoal):
 1. ( \<Gamma> \<Rightarrow>* \<Delta>, 0) \<in> derivable  R*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<Gamma> = \<Gamma> \<ominus> At i xs \<oplus> At i xs \<and> \<Delta> = \<Delta> \<ominus> At i xs \<oplus> At i xs
[PROOF STEP]
have "extend ((\<Gamma> \<ominus> At i xs) \<Rightarrow>* (\<Delta> \<ominus> At i xs)) (\<LM> At i xs \<RM> \<Rightarrow>* \<LM> At i xs \<RM>) = (\<Gamma> \<Rightarrow>* \<Delta>)"
[PROOF STATE]
proof (prove)
using this:
\<Gamma> = \<Gamma> \<ominus> At i xs \<oplus> At i xs \<and> \<Delta> = \<Delta> \<ominus> At i xs \<oplus> At i xs

goal (1 subgoal):
 1. extend ( \<Gamma> \<ominus> At i xs \<Rightarrow>* \<Delta> \<ominus> At i xs) ( \<LM> At i xs  \<RM> \<Rightarrow>* \<LM> At i xs  \<RM>) = ( \<Gamma> \<Rightarrow>* \<Delta>)
[PROOF STEP]
using extend_def[where forms="\<Gamma> \<ominus> At i xs \<Rightarrow>* \<Delta> \<ominus> At i xs" and seq="\<LM>At i xs\<RM> \<Rightarrow>* \<LM>At i xs\<RM>"]
[PROOF STATE]
proof (prove)
using this:
\<Gamma> = \<Gamma> \<ominus> At i xs \<oplus> At i xs \<and> \<Delta> = \<Delta> \<ominus> At i xs \<oplus> At i xs
extend ( \<Gamma> \<ominus> At i xs \<Rightarrow>* \<Delta> \<ominus> At i xs) ( \<LM> At i xs  \<RM> \<Rightarrow>* \<LM> At i xs  \<RM>) \<equiv>  antec ( \<Gamma> \<ominus> At i xs \<Rightarrow>* \<Delta> \<ominus> At i xs) + antec ( \<LM> At i xs  \<RM> \<Rightarrow>* \<LM> At i xs  \<RM>) \<Rightarrow>* succ ( \<Gamma> \<ominus> At i xs \<Rightarrow>* \<Delta> \<ominus> At i xs) + succ ( \<LM> At i xs  \<RM> \<Rightarrow>* \<LM> At i xs  \<RM>)

goal (1 subgoal):
 1. extend ( \<Gamma> \<ominus> At i xs \<Rightarrow>* \<Delta> \<ominus> At i xs) ( \<LM> At i xs  \<RM> \<Rightarrow>* \<LM> At i xs  \<RM>) = ( \<Gamma> \<Rightarrow>* \<Delta>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
extend ( \<Gamma> \<ominus> At i xs \<Rightarrow>* \<Delta> \<ominus> At i xs) ( \<LM> At i xs  \<RM> \<Rightarrow>* \<LM> At i xs  \<RM>) = ( \<Gamma> \<Rightarrow>* \<Delta>)

goal (1 subgoal):
 1. ( \<Gamma> \<Rightarrow>* \<Delta>, 0) \<in> derivable  R*
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
extend ( \<Gamma> \<ominus> At i xs \<Rightarrow>* \<Delta> \<ominus> At i xs) ( \<LM> At i xs  \<RM> \<Rightarrow>* \<LM> At i xs  \<RM>) = ( \<Gamma> \<Rightarrow>* \<Delta>)

goal (1 subgoal):
 1. ( \<Gamma> \<Rightarrow>* \<Delta>, 0) \<in> derivable  R*
[PROOF STEP]
have "([],\<LM> At i xs \<RM> \<Rightarrow>* \<LM> At i xs \<RM>) \<in> R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ([],  \<LM> At i xs  \<RM> \<Rightarrow>* \<LM> At i xs  \<RM>) \<in> R
[PROOF STEP]
using b
[PROOF STATE]
proof (prove)
using this:
Ax \<subseteq> R

goal (1 subgoal):
 1. ([],  \<LM> At i xs  \<RM> \<Rightarrow>* \<LM> At i xs  \<RM>) \<in> R
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
([],  \<LM> At i xs  \<RM> \<Rightarrow>* \<LM> At i xs  \<RM>) \<in> R

goal (1 subgoal):
 1. ( \<Gamma> \<Rightarrow>* \<Delta>, 0) \<in> derivable  R*
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
extend ( \<Gamma> \<ominus> At i xs \<Rightarrow>* \<Delta> \<ominus> At i xs) ( \<LM> At i xs  \<RM> \<Rightarrow>* \<LM> At i xs  \<RM>) = ( \<Gamma> \<Rightarrow>* \<Delta>)
([],  \<LM> At i xs  \<RM> \<Rightarrow>* \<LM> At i xs  \<RM>) \<in> R
[PROOF STEP]
have "([],\<Gamma> \<Rightarrow>* \<Delta>) \<in> extRules R"
[PROOF STATE]
proof (prove)
using this:
extend ( \<Gamma> \<ominus> At i xs \<Rightarrow>* \<Delta> \<ominus> At i xs) ( \<LM> At i xs  \<RM> \<Rightarrow>* \<LM> At i xs  \<RM>) = ( \<Gamma> \<Rightarrow>* \<Delta>)
([],  \<LM> At i xs  \<RM> \<Rightarrow>* \<LM> At i xs  \<RM>) \<in> R

goal (1 subgoal):
 1. ([],  \<Gamma> \<Rightarrow>* \<Delta>) \<in>  R*
[PROOF STEP]
using extRules.id[where R=R and r="([],  \<LM>At i xs\<RM> \<Rightarrow>* \<LM>At i xs\<RM>)" and S="\<Gamma> \<ominus> At i xs \<Rightarrow>* \<Delta> \<ominus> At i xs"] 
       and extendRule_def[where forms="\<Gamma> \<ominus> At i xs \<Rightarrow>* \<Delta> \<ominus> At i xs" and R="([],  \<LM>At i xs\<RM> \<Rightarrow>* \<LM>At i xs\<RM>)"]
[PROOF STATE]
proof (prove)
using this:
extend ( \<Gamma> \<ominus> At i xs \<Rightarrow>* \<Delta> \<ominus> At i xs) ( \<LM> At i xs  \<RM> \<Rightarrow>* \<LM> At i xs  \<RM>) = ( \<Gamma> \<Rightarrow>* \<Delta>)
([],  \<LM> At i xs  \<RM> \<Rightarrow>* \<LM> At i xs  \<RM>) \<in> R
\<lbrakk>([],  \<LM> At i xs  \<RM> \<Rightarrow>* \<LM> At i xs  \<RM>) \<in> R; case ([],  \<LM> At i xs  \<RM> \<Rightarrow>* \<LM> At i xs  \<RM>) of (x, xa) \<Rightarrow> (x, xa) \<in> Ax\<rbrakk> \<Longrightarrow> extendRule ( \<Gamma> \<ominus> At i xs \<Rightarrow>* \<Delta> \<ominus> At i xs) ([],  \<LM> At i xs  \<RM> \<Rightarrow>* \<LM> At i xs  \<RM>) \<in>  R*
extendRule ( \<Gamma> \<ominus> At i xs \<Rightarrow>* \<Delta> \<ominus> At i xs) ([],  \<LM> At i xs  \<RM> \<Rightarrow>* \<LM> At i xs  \<RM>) \<equiv> (map (extend ( \<Gamma> \<ominus> At i xs \<Rightarrow>* \<Delta> \<ominus> At i xs)) (fst ([],  \<LM> At i xs  \<RM> \<Rightarrow>* \<LM> At i xs  \<RM>)), extend ( \<Gamma> \<ominus> At i xs \<Rightarrow>* \<Delta> \<ominus> At i xs) (snd ([],  \<LM> At i xs  \<RM> \<Rightarrow>* \<LM> At i xs  \<RM>)))

goal (1 subgoal):
 1. ([],  \<Gamma> \<Rightarrow>* \<Delta>) \<in>  R*
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
([],  \<Gamma> \<Rightarrow>* \<Delta>) \<in>  R*

goal (1 subgoal):
 1. ( \<Gamma> \<Rightarrow>* \<Delta>, 0) \<in> derivable  R*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
([],  \<Gamma> \<Rightarrow>* \<Delta>) \<in>  R*
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
([],  \<Gamma> \<Rightarrow>* \<Delta>) \<in>  R*

goal (1 subgoal):
 1. ( \<Gamma> \<Rightarrow>* \<Delta>, 0) \<in> derivable  R*
[PROOF STEP]
using derivable.base[where R="R*" and C="\<Gamma> \<Rightarrow>* \<Delta>"]
[PROOF STATE]
proof (prove)
using this:
([],  \<Gamma> \<Rightarrow>* \<Delta>) \<in>  R*
([],  \<Gamma> \<Rightarrow>* \<Delta>) \<in>  R* \<Longrightarrow> ( \<Gamma> \<Rightarrow>* \<Delta>, 0) \<in> derivable  R*

goal (1 subgoal):
 1. ( \<Gamma> \<Rightarrow>* \<Delta>, 0) \<in> derivable  R*
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
( \<Gamma> \<Rightarrow>* \<Delta>, 0) \<in> derivable  R*

goal:
No subgoals!
[PROOF STEP]
qed