[Logiweb] How to instantiate A4'

[Klaus Ebbe Grue]

Hi Kasper and Martin,

Kasper> I am trying to use A4' in my proof, but no matter what I try I get a
Kasper> "false side contition" diagnose.

Martin> Could it be that you need to write:
Martin> ...prime a four at peano t indeed...

Martin is right. But the "false side condition" diagnose is *very* 
misleading.

A4' says
    AcAxAaAb: a=<b|x:=c> ||- Ax:b => a
where I have placed metavariable c first because it has to be 
instantiated explicitly. The 'unification tactic' (x >> y from the base 
page) can guess a, b, and x from the shape of the conclusion. Guessing c 
is possible but beyond the power of the unification tactic.

When using A4' without explicit instantiation of meta-variable c, the 
unification tactic just sets c to an invalid term which is then rejected 
later on by some, arbitrary, diagnose.

So I have to invent some new diagnose like "variable c not instantiated" 
or whatever. But I'm afraid I cannot include such a new diagnose this 
week.

Klaus