--- a/Nominal/Term5.thy	Tue Mar 16 15:38:14 2010 +0100
+++ b/Nominal/Term5.thy	Tue Mar 16 16:17:05 2010 +0100
@@ -79,19 +79,59 @@
 apply clarify
 apply (erule alpha_gen_compose_sym)
 apply (simp add: alpha5_eqvt)
+(* Works for non-recursive, proof is done here *)
 apply(clarify)
 apply (rotate_tac 1)
 apply (frule_tac p="- pi" in alpha5_eqvt(1))
 apply simp
 done
 
-
+lemma alpha5_transp:
+"(a \<approx>5 b \<longrightarrow> (\<forall>c. b \<approx>5 c \<longrightarrow> a \<approx>5 c)) \<and>
+(x \<approx>l y \<longrightarrow> (\<forall>z. y \<approx>l z \<longrightarrow> x \<approx>l z)) \<and>
+(alpha_rbv5 p k l \<longrightarrow> (\<forall>m q. alpha_rbv5 q l m \<longrightarrow> alpha_rbv5 (q + p) k m))"
+(*apply (tactic {* transp_tac @{context} @{thm alpha_rtrm5_alpha_rlts_alpha_rbv5.induct} @{thms alpha5_inj} @{thms rtrm5.distinct rtrm5.inject rlts.distinct rlts.inject} [] @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{thms alpha5_eqvt} 1 *})*)
+apply (rule alpha_rtrm5_alpha_rlts_alpha_rbv5.induct)
+apply (rule_tac [!] allI)
+apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *})
+apply (simp_all add: alpha5_inj)
+apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *})
+apply (simp_all add: alpha5_inj)
+apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *})
+apply (simp_all add: alpha5_inj)
+apply (tactic {* eetac @{thm exi_sum} @{context} 1 *})
+apply clarify
+apply simp
+apply (erule alpha_gen_compose_trans)
+apply (assumption)
+apply (simp add: alpha5_eqvt)
+apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *})
+apply (simp_all add: alpha5_inj)
+apply (rule allI)
+apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *})
+apply (simp_all add: alpha5_inj)
+apply (rule allI)
+apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *})
+apply (simp_all add: alpha5_inj)
+(* Works for non-recursive, proof is done here *)
+apply clarify
+apply (rotate_tac 1)
+apply (frule_tac p="- pia" in alpha5_eqvt(1))
+apply (erule_tac x="- pia \<bullet> rtrm5aa" in allE)
+apply simp
+apply (rotate_tac -1)
+apply (frule_tac p="pia" in alpha5_eqvt(1))
+apply simp
+done
 
 lemma alpha5_equivp:
   "equivp alpha_rtrm5"
   "equivp alpha_rlts"
-  "equivp (alpha_rbv5 p)"
-  sorry
+  unfolding equivp_reflp_symp_transp reflp_def symp_def transp_def
+  apply (simp_all only: alpha5_reflp)
+  apply (meson alpha5_symp alpha5_transp)
+  apply (meson alpha5_symp alpha5_transp)
+  done
 
 quotient_type
   trm5 = rtrm5 / alpha_rtrm5