[STATEMENT]
lemma Methd_sound: 
  assumes recursive: "G,A\<union>  {{P} Methd-\<succ> {Q} | ms}|\<Turnstile>\<Colon>{{P} body G-\<succ> {Q} | ms}"
  shows "G,A|\<Turnstile>\<Colon>{{P} Methd-\<succ> {Q} | ms}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. G,A|\<Turnstile>\<Colon>{{P} Methd-\<succ> {Q} | ms}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. G,A|\<Turnstile>\<Colon>{{P} Methd-\<succ> {Q} | ms}
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. G,A|\<Turnstile>\<Colon>{{P} Methd-\<succ> {Q} | ms}
[PROOF STEP]
fix n
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. G,A|\<Turnstile>\<Colon>{{P} Methd-\<succ> {Q} | ms}
[PROOF STEP]
assume recursive: "\<And> n. \<forall>t\<in>(A \<union> {{P} Methd-\<succ> {Q} | ms}). G\<Turnstile>n\<Colon>t
                              \<Longrightarrow>  \<forall>t\<in>{{P} body G-\<succ> {Q} | ms}.  G\<Turnstile>n\<Colon>t"
[PROOF STATE]
proof (state)
this:
\<forall>t\<in>A \<union> {{P} Methd-\<succ> {Q} | ms}. G\<Turnstile>?n\<Colon>t \<Longrightarrow> \<forall>t\<in>{{P} body G-\<succ> {Q} | ms}. G\<Turnstile>?n\<Colon>t

goal (1 subgoal):
 1. G,A|\<Turnstile>\<Colon>{{P} Methd-\<succ> {Q} | ms}
[PROOF STEP]
have "\<forall>t\<in>A. G\<Turnstile>n\<Colon>t \<Longrightarrow> \<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}.  G\<Turnstile>n\<Colon>t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>t\<in>A. G\<Turnstile>n\<Colon>t \<Longrightarrow> \<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}. G\<Turnstile>n\<Colon>t
[PROOF STEP]
proof (induct n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Ball A (triple_valid2 G 0) \<Longrightarrow> Ball ({{P} Methd-\<succ> {Q} | ms}) (triple_valid2 G 0)
 2. \<And>n. \<lbrakk>Ball A (triple_valid2 G n) \<Longrightarrow> Ball ({{P} Methd-\<succ> {Q} | ms}) (triple_valid2 G n); Ball A (triple_valid2 G (Suc n))\<rbrakk> \<Longrightarrow> Ball ({{P} Methd-\<succ> {Q} | ms}) (triple_valid2 G (Suc n))
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
\<forall>a\<in>A. G\<Turnstile>0\<Colon>a

goal (2 subgoals):
 1. Ball A (triple_valid2 G 0) \<Longrightarrow> Ball ({{P} Methd-\<succ> {Q} | ms}) (triple_valid2 G 0)
 2. \<And>n. \<lbrakk>Ball A (triple_valid2 G n) \<Longrightarrow> Ball ({{P} Methd-\<succ> {Q} | ms}) (triple_valid2 G n); Ball A (triple_valid2 G (Suc n))\<rbrakk> \<Longrightarrow> Ball ({{P} Methd-\<succ> {Q} | ms}) (triple_valid2 G (Suc n))
[PROOF STEP]
show "\<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}.  G\<Turnstile>0\<Colon>t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}. G\<Turnstile>0\<Colon>t
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}. G\<Turnstile>0\<Colon>t
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}. G\<Turnstile>0\<Colon>t
[PROOF STEP]
fix C sig
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}. G\<Turnstile>0\<Colon>t
[PROOF STEP]
assume "(C,sig) \<in> ms"
[PROOF STATE]
proof (state)
this:
(C, sig) \<in> ms

goal (1 subgoal):
 1. \<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}. G\<Turnstile>0\<Colon>t
[PROOF STEP]
have "G\<Turnstile>0\<Colon>{Normal (P C sig)} Methd C sig-\<succ> {Q C sig}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. G\<Turnstile>0\<Colon>{Normal (P C sig)} Methd C sig-\<succ> {Q C sig}
[PROOF STEP]
by (rule Methd_triple_valid2_0)
[PROOF STATE]
proof (state)
this:
G\<Turnstile>0\<Colon>{Normal (P C sig)} Methd C sig-\<succ> {Q C sig}

goal (1 subgoal):
 1. \<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}. G\<Turnstile>0\<Colon>t
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
(?C2, ?sig2) \<in> ms \<Longrightarrow> G\<Turnstile>0\<Colon>{Normal (P ?C2 ?sig2)} Methd ?C2 ?sig2-\<succ> {Q ?C2 ?sig2}

goal (1 subgoal):
 1. \<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}. G\<Turnstile>0\<Colon>t
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(?C2, ?sig2) \<in> ms \<Longrightarrow> G\<Turnstile>0\<Colon>{Normal (P ?C2 ?sig2)} Methd ?C2 ?sig2-\<succ> {Q ?C2 ?sig2}

goal (1 subgoal):
 1. \<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}. G\<Turnstile>0\<Colon>t
[PROOF STEP]
by (simp add: mtriples_def split_def)
[PROOF STATE]
proof (state)
this:
\<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}. G\<Turnstile>0\<Colon>t

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}. G\<Turnstile>0\<Colon>t

goal (1 subgoal):
 1. \<And>n. \<lbrakk>Ball A (triple_valid2 G n) \<Longrightarrow> Ball ({{P} Methd-\<succ> {Q} | ms}) (triple_valid2 G n); Ball A (triple_valid2 G (Suc n))\<rbrakk> \<Longrightarrow> Ball ({{P} Methd-\<succ> {Q} | ms}) (triple_valid2 G (Suc n))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>Ball A (triple_valid2 G n) \<Longrightarrow> Ball ({{P} Methd-\<succ> {Q} | ms}) (triple_valid2 G n); Ball A (triple_valid2 G (Suc n))\<rbrakk> \<Longrightarrow> Ball ({{P} Methd-\<succ> {Q} | ms}) (triple_valid2 G (Suc n))
[PROOF STEP]
case (Suc m)
[PROOF STATE]
proof (state)
this:
\<forall>a\<in>A. G\<Turnstile>m\<Colon>a \<Longrightarrow> \<forall>a\<in>{{P} Methd-\<succ> {Q} | ms}. G\<Turnstile>m\<Colon>a
\<forall>a\<in>A. G\<Turnstile>Suc m\<Colon>a

goal (1 subgoal):
 1. \<And>n. \<lbrakk>Ball A (triple_valid2 G n) \<Longrightarrow> Ball ({{P} Methd-\<succ> {Q} | ms}) (triple_valid2 G n); Ball A (triple_valid2 G (Suc n))\<rbrakk> \<Longrightarrow> Ball ({{P} Methd-\<succ> {Q} | ms}) (triple_valid2 G (Suc n))
[PROOF STEP]
note hyp = \<open>\<forall>t\<in>A. G\<Turnstile>m\<Colon>t \<Longrightarrow> \<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}.  G\<Turnstile>m\<Colon>t\<close>
[PROOF STATE]
proof (state)
this:
\<forall>t\<in>A. G\<Turnstile>m\<Colon>t \<Longrightarrow> \<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}. G\<Turnstile>m\<Colon>t

goal (1 subgoal):
 1. \<And>n. \<lbrakk>Ball A (triple_valid2 G n) \<Longrightarrow> Ball ({{P} Methd-\<succ> {Q} | ms}) (triple_valid2 G n); Ball A (triple_valid2 G (Suc n))\<rbrakk> \<Longrightarrow> Ball ({{P} Methd-\<succ> {Q} | ms}) (triple_valid2 G (Suc n))
[PROOF STEP]
note prem = \<open>\<forall>t\<in>A. G\<Turnstile>Suc m\<Colon>t\<close>
[PROOF STATE]
proof (state)
this:
\<forall>t\<in>A. G\<Turnstile>Suc m\<Colon>t

goal (1 subgoal):
 1. \<And>n. \<lbrakk>Ball A (triple_valid2 G n) \<Longrightarrow> Ball ({{P} Methd-\<succ> {Q} | ms}) (triple_valid2 G n); Ball A (triple_valid2 G (Suc n))\<rbrakk> \<Longrightarrow> Ball ({{P} Methd-\<succ> {Q} | ms}) (triple_valid2 G (Suc n))
[PROOF STEP]
show "\<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}.  G\<Turnstile>Suc m\<Colon>t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}. G\<Turnstile>Suc m\<Colon>t
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}. G\<Turnstile>Suc m\<Colon>t
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}. G\<Turnstile>Suc m\<Colon>t
[PROOF STEP]
fix C sig
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}. G\<Turnstile>Suc m\<Colon>t
[PROOF STEP]
assume m: "(C,sig) \<in> ms"
[PROOF STATE]
proof (state)
this:
(C, sig) \<in> ms

goal (1 subgoal):
 1. \<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}. G\<Turnstile>Suc m\<Colon>t
[PROOF STEP]
have "G\<Turnstile>Suc m\<Colon>{Normal (P C sig)} Methd C sig-\<succ> {Q C sig}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. G\<Turnstile>Suc m\<Colon>{Normal (P C sig)} Methd C sig-\<succ> {Q C sig}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. G\<Turnstile>Suc m\<Colon>{Normal (P C sig)} Methd C sig-\<succ> {Q C sig}
[PROOF STEP]
from prem
[PROOF STATE]
proof (chain)
picking this:
\<forall>t\<in>A. G\<Turnstile>Suc m\<Colon>t
[PROOF STEP]
have prem_m: "\<forall>t\<in>A. G\<Turnstile>m\<Colon>t"
[PROOF STATE]
proof (prove)
using this:
\<forall>t\<in>A. G\<Turnstile>Suc m\<Colon>t

goal (1 subgoal):
 1. \<forall>t\<in>A. G\<Turnstile>m\<Colon>t
[PROOF STEP]
by (rule triples_valid2_Suc)
[PROOF STATE]
proof (state)
this:
\<forall>t\<in>A. G\<Turnstile>m\<Colon>t

goal (1 subgoal):
 1. G\<Turnstile>Suc m\<Colon>{Normal (P C sig)} Methd C sig-\<succ> {Q C sig}
[PROOF STEP]
hence "\<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}.  G\<Turnstile>m\<Colon>t"
[PROOF STATE]
proof (prove)
using this:
\<forall>t\<in>A. G\<Turnstile>m\<Colon>t

goal (1 subgoal):
 1. \<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}. G\<Turnstile>m\<Colon>t
[PROOF STEP]
by (rule hyp)
[PROOF STATE]
proof (state)
this:
\<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}. G\<Turnstile>m\<Colon>t

goal (1 subgoal):
 1. G\<Turnstile>Suc m\<Colon>{Normal (P C sig)} Methd C sig-\<succ> {Q C sig}
[PROOF STEP]
with prem_m
[PROOF STATE]
proof (chain)
picking this:
\<forall>t\<in>A. G\<Turnstile>m\<Colon>t
\<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}. G\<Turnstile>m\<Colon>t
[PROOF STEP]
have "\<forall>t\<in>(A \<union> {{P} Methd-\<succ> {Q} | ms}). G\<Turnstile>m\<Colon>t"
[PROOF STATE]
proof (prove)
using this:
\<forall>t\<in>A. G\<Turnstile>m\<Colon>t
\<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}. G\<Turnstile>m\<Colon>t

goal (1 subgoal):
 1. \<forall>t\<in>A \<union> {{P} Methd-\<succ> {Q} | ms}. G\<Turnstile>m\<Colon>t
[PROOF STEP]
by (simp add: ball_Un)
[PROOF STATE]
proof (state)
this:
\<forall>t\<in>A \<union> {{P} Methd-\<succ> {Q} | ms}. G\<Turnstile>m\<Colon>t

goal (1 subgoal):
 1. G\<Turnstile>Suc m\<Colon>{Normal (P C sig)} Methd C sig-\<succ> {Q C sig}
[PROOF STEP]
hence "\<forall>t\<in>{{P} body G-\<succ> {Q} | ms}.  G\<Turnstile>m\<Colon>t"
[PROOF STATE]
proof (prove)
using this:
\<forall>t\<in>A \<union> {{P} Methd-\<succ> {Q} | ms}. G\<Turnstile>m\<Colon>t

goal (1 subgoal):
 1. \<forall>t\<in>{{P} body G-\<succ> {Q} | ms}. G\<Turnstile>m\<Colon>t
[PROOF STEP]
by (rule recursive)
[PROOF STATE]
proof (state)
this:
\<forall>t\<in>{{P} body G-\<succ> {Q} | ms}. G\<Turnstile>m\<Colon>t

goal (1 subgoal):
 1. G\<Turnstile>Suc m\<Colon>{Normal (P C sig)} Methd C sig-\<succ> {Q C sig}
[PROOF STEP]
with m
[PROOF STATE]
proof (chain)
picking this:
(C, sig) \<in> ms
\<forall>t\<in>{{P} body G-\<succ> {Q} | ms}. G\<Turnstile>m\<Colon>t
[PROOF STEP]
have "G\<Turnstile>m\<Colon>{Normal (P C sig)} body G C sig-\<succ> {Q C sig}"
[PROOF STATE]
proof (prove)
using this:
(C, sig) \<in> ms
\<forall>t\<in>{{P} body G-\<succ> {Q} | ms}. G\<Turnstile>m\<Colon>t

goal (1 subgoal):
 1. G\<Turnstile>m\<Colon>{Normal (P C sig)} body G C sig-\<succ> {Q C sig}
[PROOF STEP]
by (auto simp add: mtriples_def split_def)
[PROOF STATE]
proof (state)
this:
G\<Turnstile>m\<Colon>{Normal (P C sig)} body G C sig-\<succ> {Q C sig}

goal (1 subgoal):
 1. G\<Turnstile>Suc m\<Colon>{Normal (P C sig)} Methd C sig-\<succ> {Q C sig}
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
G\<Turnstile>m\<Colon>{Normal (P C sig)} body G C sig-\<succ> {Q C sig}

goal (1 subgoal):
 1. G\<Turnstile>Suc m\<Colon>{Normal (P C sig)} Methd C sig-\<succ> {Q C sig}
[PROOF STEP]
by (rule Methd_triple_valid2_SucI)
[PROOF STATE]
proof (state)
this:
G\<Turnstile>Suc m\<Colon>{Normal (P C sig)} Methd C sig-\<succ> {Q C sig}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
G\<Turnstile>Suc m\<Colon>{Normal (P C sig)} Methd C sig-\<succ> {Q C sig}

goal (1 subgoal):
 1. \<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}. G\<Turnstile>Suc m\<Colon>t
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
(?C2, ?sig2) \<in> ms \<Longrightarrow> G\<Turnstile>Suc m\<Colon>{Normal (P ?C2 ?sig2)} Methd ?C2 ?sig2-\<succ> {Q ?C2 ?sig2}

goal (1 subgoal):
 1. \<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}. G\<Turnstile>Suc m\<Colon>t
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(?C2, ?sig2) \<in> ms \<Longrightarrow> G\<Turnstile>Suc m\<Colon>{Normal (P ?C2 ?sig2)} Methd ?C2 ?sig2-\<succ> {Q ?C2 ?sig2}

goal (1 subgoal):
 1. \<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}. G\<Turnstile>Suc m\<Colon>t
[PROOF STEP]
by (simp add: mtriples_def split_def)
[PROOF STATE]
proof (state)
this:
\<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}. G\<Turnstile>Suc m\<Colon>t

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}. G\<Turnstile>Suc m\<Colon>t

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>t\<in>A. G\<Turnstile>n\<Colon>t \<Longrightarrow> \<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}. G\<Turnstile>n\<Colon>t

goal (1 subgoal):
 1. G,A|\<Turnstile>\<Colon>{{P} Methd-\<succ> {Q} | ms}
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<And>n. \<forall>t\<in>A \<union> {{P} Methd-\<succ> {Q} | ms}. G\<Turnstile>n\<Colon>t \<Longrightarrow> \<forall>t\<in>{{P} body G-\<succ> {Q} | ms}. G\<Turnstile>n\<Colon>t; \<forall>t\<in>A. G\<Turnstile>?n2\<Colon>t\<rbrakk> \<Longrightarrow> \<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}. G\<Turnstile>?n2\<Colon>t

goal (1 subgoal):
 1. G,A|\<Turnstile>\<Colon>{{P} Methd-\<succ> {Q} | ms}
[PROOF STEP]
with recursive
[PROOF STATE]
proof (chain)
picking this:
G,A \<union> {{P} Methd-\<succ> {Q} | ms}|\<Turnstile>\<Colon>{{P} body G-\<succ> {Q} | ms}
\<lbrakk>\<And>n. \<forall>t\<in>A \<union> {{P} Methd-\<succ> {Q} | ms}. G\<Turnstile>n\<Colon>t \<Longrightarrow> \<forall>t\<in>{{P} body G-\<succ> {Q} | ms}. G\<Turnstile>n\<Colon>t; \<forall>t\<in>A. G\<Turnstile>?n2\<Colon>t\<rbrakk> \<Longrightarrow> \<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}. G\<Turnstile>?n2\<Colon>t
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
G,A \<union> {{P} Methd-\<succ> {Q} | ms}|\<Turnstile>\<Colon>{{P} body G-\<succ> {Q} | ms}
\<lbrakk>\<And>n. \<forall>t\<in>A \<union> {{P} Methd-\<succ> {Q} | ms}. G\<Turnstile>n\<Colon>t \<Longrightarrow> \<forall>t\<in>{{P} body G-\<succ> {Q} | ms}. G\<Turnstile>n\<Colon>t; \<forall>t\<in>A. G\<Turnstile>?n2\<Colon>t\<rbrakk> \<Longrightarrow> \<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}. G\<Turnstile>?n2\<Colon>t

goal (1 subgoal):
 1. G,A|\<Turnstile>\<Colon>{{P} Methd-\<succ> {Q} | ms}
[PROOF STEP]
by (unfold ax_valids2_def) blast
[PROOF STATE]
proof (state)
this:
G,A|\<Turnstile>\<Colon>{{P} Methd-\<succ> {Q} | ms}

goal:
No subgoals!
[PROOF STEP]
qed