New failing problem, which shows that we need to change special_k

diff --git a/ocaml/problems.ml b/ocaml/problems.ml
index f586c5d9a34a9133bca8ab638bf32b3adb329655..ca3a0d05dd2de7e9d22765e4d551df8241ff18a0 100644 (file)
--- a/ocaml/problems.ml
+++ b/ocaml/problems.ml
@@ -398,7 +398,20 @@ solve_many [
  ]*)
 ];;
 
-(*failwith "OKAy";;*)
+(* This now fails *)
+solve (problem_of
+ (Some"x PAC PAC PAC PAC PAC a")
+ ["x PAC PAC PAC PAC PAC b"]
+ ["y x"; "y z"]
+ (* In general:
+ DIV x (n times PAC) a
+ CON x (n times PAC) b
+ 1 y (m times lambda. x) 0
+ 2 y z 0
+ when x steps on the n+1-th argument,
+ y must apply n+m+1 variables
+ Thus special_k must be >=n+m+1 *)
+);;
 
 solve_many ([
  p2 ; p4 ; p5 ; p6 ; p7 ; p8 ; p9 ; p10 ; p11 ; p12 ; p13 ;