[isabelle] Instantiation problem



Hello everybody,
during a proof I have obtained:
(getPc (stof (snd s)) ! (cinc i) = S) /\ getDir (stof (snd s)) ! (cinc i) =
right /\ getPc (stof (snd s)) ! i = ER
where (cinc i)::nat.

Now I want demonstrate the goal:
EX i::nat. ((getPc (stof (snd s)) ! i = S) /\ getDir (stof (snd s)) ! i =
right /\ getPc (stof (snd s)) ! cdec i = ER)

It follow from a simple instantiation ( i <-- (cinc i) ) but I don't find
how to help Isabelle to execute it and using normal proof methods Isabelle
don't find the solution.

Can you help me?

Sorry, I know that this is a very trivial problem but I don't understand it.

Thanks

Gabriele




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.