[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: Identical antecedent and consequent



Murali,

> The exact terms are shown below. The pvs dump file is also attached. The
> theorem I am proving is process_rep_th6 in the OneComponent theory. 
> 
> process_rep_th6 :  
> 
> [-1]  process_rep(choice(c)(InitStates(c), choice_F))
>   |-------
> [1]   process_rep(choice(c)(InitStates(c), choice_F))

If you so M-x show-expanded-sequent at this point, you'll get

process_rep_th6 :  

{-1}  CSPBasics[Store].process_rep
          (Choice[Store,
                  Component,
                  OneComponentDeclarations[Store,
                                           empty,
                                           Component].choice_F,
                  OneComponentDeclarations[Store,
                                           empty,
                                           Component].Psi].choice
               (Choice[Store,
                       Component,
                       OneComponentDeclarations[Store,
                                                empty,
                                                Component].choice_F,
                       OneComponentDeclarations[Store,
                                                empty,
                                                Component].Psi].c)
               (OneComponentDeclarations[Store, empty, Component].InitStates
                    (c),
                OneComponentDeclarations[Store, empty, Component].choice_F))
  |-------
{1}   CSPBasics[Store].process_rep
          (Choice[Store,
                  Component,
                  OneComponentDeclarations[Store,
                                           empty,
                                           Component].choice_F,
                  OneComponentDeclarations[Store,
                                           empty,
                                           Component].Psi].choice
               (c)
               (OneComponentDeclarations[Store, empty, Component].InitStates
                    (c),
                OneComponentDeclarations[Store, empty, Component].choice_F))

from which you can see that when all the type information is expanded
out, the antecedent and consequent are not the same.

I'll leave it to you to figure out why this is so--you may need to
specify the theory instance when invoking the lemma "choice_ax1".

John Rushby
-------