solver deficiency with substitutable equations

[GoogleCodeExporter]

What steps will reproduce the problem?
1. ensure that you are running the Nov 8 2007 version with fix for issue34 
applied.
2.
load 
<http://svn.berlios.de/svnroot/repos/al4nin/trunk/found-bugs/issue35-HenkTest.om
g>
3. increase narrowing bound:
:bounds narrow 300
4. :reload file

What is the expected output? What do you see instead?
I expect no problems (possibly a typecheck problem that is eclipsed)
but I get:

**** Near line: 131 column: 1

While type checking in the scope of:
   the pattern (Bind (SE (LV cl)) (a@(Lit qf)) (b@(Lit (Spine' 1v))))
We need to prove:
   Equal {strat h} {strat h}, Equal {diff g {strat h}} 0t, Equal {strat h} 2t, Equal {diff g {strat h}} 0t, 
Equal {strat h} 2t
From the truths:Climber' (Spine 2t),Climber' (Spine 3t),LE 1t (1+_i)t,
And the rules:SE,LV,Spine',Step,Base,S,Z,S,Z,
But, The equations: ({strat h}={strat h}, {diff g {strat h}}=0t, {strat h}=2t, 
{diff g {strat h}}=0t, {strat 
h}=2t) =>  have no solution

The equations, simplified manually:
({diff g {strat h}}=0t, {strat h}=2t)

However if I do equational reasoning, I can show:

{diff g {strat h}}=0t
----{strat h}=2t---->
{diff g 2t}=0t
----guess g=2t---->
Success

My first idea how to fix this problem would be to add equations with a constant 
side {strat h}=2t 
as truths. Not sure whether this results in a sound logic, though.

Original issue reported on code.google.com by ggr...@gmail.com on 9 Nov 2007 at 11:23

[GoogleCodeExporter]

This is another form of Cross Fertilization (Infer2.hs:3000), but of a 
simplifying kind.

Original comment by ggr...@gmail.com on 8 Dec 2007 at 8:11

[GoogleCodeExporter]

also there is quite a bit of duplication in the
rules (S,Z,S,Z) and the equations too.
Maybe some value-numbering algorithm
could be used to weed out the redundance?

Original comment by ggr...@gmail.com on 9 Dec 2007 at 12:47

[GoogleCodeExporter]

Original comment by ggr...@gmail.com on 12 Dec 2007 at 10:55

• Changed title: solver deficiency with substitutable equations