# Re: [isabelle] Calculational reasoning proof structure

Somehow related question:
Why switching from second form to calculation one (using "also have")
I ocaasionally get "*** Vacuous calculation result" error. Any common
reasons for such problem?
Vadim
On Aug 19, 2014, at 11:35 , Vadim Zaliva <vzaliva at cmu.edu> wrote:
> Hi!
>
> I am doing a proof which includes series of steps. Something like this:
>
> have "x0 = x1"
> also have "... = x2"
> also have "... = x3"
> ...
> finally have "x0=xN"
>
> The proof is rather long and sometimes I need to prove some intermediate facts
> between the steps to get to the next one. This breaks the computation chain and I could not
> use "..." in the next step. What is the common way of dealing with such proofs?
> Right now I am forced to do something like this:
>
>
> have "x0 = x1"
> hence s2:"x0=x2"
>
> have "some fact"
>
> hence "x0 = x3" using s2
> ...
> hence "x0=xN"
>
> Thanks!
>
> Sincerely,
> Vadim Zaliva
>
> --
> CMU ECE PhD student
> Mobile: +1(510)220-1060
> Skype: vzaliva
>
Sincerely,
Vadim Zaliva
--
CMU ECE PhD student
Mobile: +1(510)220-1060
Skype: vzaliva

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