diff -r 3a60a028cfc5 -r aaac8274f08c Quot/Nominal/Terms.thy
--- a/Quot/Nominal/Terms.thy	Wed Feb 03 11:47:37 2010 +0100
+++ b/Quot/Nominal/Terms.thy	Wed Feb 03 12:11:23 2010 +0100
@@ -649,6 +649,12 @@
   by (simp_all add: alpha4_equivp alpha4list_equivp)
 
 
+
+
+
+
+
+
 datatype rtrm5 =
   rVr5 "name"
 | rAp5 "rtrm5" "rtrm5"
@@ -708,8 +714,21 @@
 apply(simp_all add: pt_rtrm5_zero pt_rtrm5_plus)
 done
 
-
 end
 
+inductive
+  alpha5 :: "rtrm5 \<Rightarrow> rtrm5 \<Rightarrow> bool" ("_ \<approx>5 _" [100, 100] 100)
+and
+  alphalts :: "rlts \<Rightarrow> rlts \<Rightarrow> bool" ("_ \<approx>l _" [100, 100] 100)
+where
+  a1: "a = b \<Longrightarrow> (rVr5 a) \<approx>5 (rVr5 b)"
+| a2: "\<lbrakk>t1 \<approx>5 t2; s1 \<approx>5 s2\<rbrakk> \<Longrightarrow> rAp5 t1 s1 \<approx>5 rAp5 t2 s2"
+| a3: "\<exists>pi. ((bv5 l1, t1) \<approx>gen alpha5 rfv_trm5 pi (bv5 l2, t2) \<and>
+             (bv5 l1, l1) \<approx>gen alphalts rfv_lts pi (bv5 l2, l2) \<and>
+              (pi \<bullet> (bv5 l1) = bv5 l2))
+        \<Longrightarrow> rLt5 l1 t1 \<approx>5 rLt5 l2 t2"
+| a4: "rLnil \<approx>l rLnil"
+| a5: "ls1 \<approx>l ls2 \<Longrightarrow> t1 \<approx>5 t2 \<Longrightarrow> rLcons n1 t1 ls1 \<approx>l rLcons n2 t2 ls2"
 
+thm a3[simplified alpha_gen]
 end