From: acondolu <andrea.condoluci@unibo.it>
Date: Fri, 14 Jul 2017 08:28:09 +0000 (+0200)
Subject: New failing problem, which shows that we need to change special_k
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=40626d5b73d1eefdde923c80530fec20ff3880d6;p=fireball-separation.git

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

diff --git a/ocaml/problems.ml b/ocaml/problems.ml
index f586c5d..ca3a0d0 100644
--- 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 ;