# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1264510708 -3600
# Node ID 624af16bb6e4546429d54e713dc26342cd813ee9
# Parent  2c72447cdc0c6a7590bff4d4cd96524c103de907
Found a term that does not regularize.

diff -r 2c72447cdc0c -r 624af16bb6e4 Quot/Examples/FSet.thy
--- a/Quot/Examples/FSet.thy	Tue Jan 26 13:53:56 2010 +0100
+++ b/Quot/Examples/FSet.thy	Tue Jan 26 13:58:28 2010 +0100
@@ -398,4 +398,23 @@
 apply(lifting test3)
 done
 
+lemma test4: "\<forall> (x :: 'a list, y, z) \<in> Respects(
+  prod_rel (op \<approx>) (prod_rel (op \<approx>) (op \<approx>))
+). x = y \<and> y = z"
+sorry
+
+lemma "All (\<lambda> (x :: 'a fset, y, z). x = y \<and> y = z)"
+apply (lifting test4)
+sorry
+
+lemma test5: "\<forall> (x :: 'a list \<Rightarrow> 'a list, y, z) \<in> Respects(
+  prod_rel (op \<approx> ===> op \<approx>) (prod_rel (op \<approx> ===> op \<approx>) (op \<approx> ===> op \<approx>))
+). x = y \<and> y = z"
+sorry
+
+lemma "All (\<lambda> (x :: 'a fset \<Rightarrow> 'a fset, y, z). x = y \<and> y = z)"
+apply (lifting test5)
+sorry
+
+
 end