# [PVS-Help] Decompose-equality after assert

```Hi, I'm hoping someone can explain the following behaviour to me.

Consider the following proof steps (understanding the formula isn't
necessary, just that it is an equality between tuples):

====================================================================
cinv_ssn.10 :

[-1,(main)]
(c0`n(ppp), 1 + c0`ss(ppp)`2) = c0`ss(q)
|-------

Rule? (decompose-equality)
Applying decompose-equality,
this simplifies to:
cinv_ssn.10 :

{-1}  c0`n(ppp) = c0`ss(q)`1
{-2}  1 + c0`ss(ppp)`2 = c0`ss(q)`2
|-------

====================================================================

This is what I would expect.  However, if I execute 'record' before
decomposing the equality I get the empty sequent, eg.

====================================================================
cinv_ssn.10 :

[-1,(main)]
(c0`n(ppp), 1 + c0`ss(ppp)`2) = c0`ss(q)
|-------

Rule? (record)
Simplifying and recording with decision procedures,
this simplifies to:
cinv_ssn.10 :

[-1,(main)]
(c0`n(ppp), 1 + c0`ss(ppp)`2) = c0`ss(q)
|-------

Rule? (decompose-equality)
Applying decompose-equality,
this simplifies to:
cinv_ssn.10 :

|-------

====================================================================

I don't understand why the equality decomposes to true after
recording (I noticed this when doing an 'assert') .
Any help appreciated.
(Btw, there are formulas which I have 'hidden', but my understanding
is they should not affect what is going on).

Thanks,
Rob

Below is the output from (decompose-equality\$) after 'record'ing.

====================================================================
cinv_ssn.10 :

[-1,(main)]
(c0`n(ppp), 1 + c0`ss(ppp)`2) = c0`ss(q)
|-------

Rule? (decompose-equality\$)
Case splitting on
(c0`n(ppp), 1 + c0`ss(ppp)`2)`1 = c0`ss(q)`1 AND
(c0`n(ppp), 1 + c0`ss(ppp)`2)`2 = c0`ss(q)`2,
this yields  2 subgoals:
cinv_ssn.10.1 :

{-1}  (c0`n(ppp), 1 + c0`ss(ppp)`2)`1 = c0`ss(q)`1 AND
(c0`n(ppp), 1 + c0`ss(ppp)`2)`2 = c0`ss(q)`2
[-2,(main)]
(c0`n(ppp), 1 + c0`ss(ppp)`2) = c0`ss(q)
|-------

Simplifying with decision procedures,
this simplifies to:
cinv_ssn.10.1 :

{-1}  TRUE AND TRUE
[-2,(main)]
(c0`n(ppp), 1 + c0`ss(ppp)`2) = c0`ss(q)
|-------

Deleting some formulas,
this simplifies to:
cinv_ssn.10.1 :

[-1]  TRUE AND TRUE
|-------

Applying disjunctive simplification to flatten sequent,
this simplifies to:
cinv_ssn.10.1 :

|-------

Postponing cinv_ssn.10.1.

cinv_ssn.10.2 :

[-1,(main)]
(c0`n(ppp), 1 + c0`ss(ppp)`2) = c0`ss(q)
|-------
{1}   (c0`n(ppp), 1 + c0`ss(ppp)`2)`1 = c0`ss(q)`1 AND
(c0`n(ppp), 1 + c0`ss(ppp)`2)`2 = c0`ss(q)`2

No change on: (flatten)
cinv_ssn.10.2 :

[-1,(main)]
(c0`n(ppp), 1 + c0`ss(ppp)`2) = c0`ss(q)
|-------
{1}   (c0`n(ppp), 1 + c0`ss(ppp)`2)`1 = c0`ss(q)`1 AND
(c0`n(ppp), 1 + c0`ss(ppp)`2)`2 = c0`ss(q)`2

Repeatedly applying the replace rule,

This completes the proof of cinv_ssn.10.2.

cinv_ssn.10.1 :

|-------

====================================================================

```