# Re: [isabelle] Calculational reasoning proof structure

```That pops up sometimes if you've flipped one of the inequalities e.g.

have "a = b" .
also have "c = b" .

Dave

On 20/08/14 08:21, Vadim Zaliva wrote:
```
```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?

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,

--
CMU ECE PhD student
Mobile: +1(510)220-1060
Skype: vzaliva

```
```
Sincerely,

--
CMU ECE PhD student
Mobile: +1(510)220-1060
Skype: vzaliva

```
```

```

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