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

Re: Strange problems



Harald Ruess wrote:
>  maybe it helps to investigate the structure of your
>  proof sequent with the command Meta-X show-expanded-sequent

Thanks, I see now what is going on. I've included the expanded sequent
below. I am still confused about how to deal with it, though. Can PVS
prove
this sequent, or should I try to restructure my specification in such
a way that the situation does not arise?
--
pertti


action_superposition.3.1.1.1.1 :  

{-1}  semantics.sem
          (action_semantics_utilities.variable_assignments
               (action_semantics_utilities.role_of_object
                    (ob!1, ra!1,
                     action_expr_adt[semantic_base.id].roles(a!1)),
                list_props[semantic_base.id].append
                   
(DisCo_action_refinement_adt[semantic_base.id].new_fields
                         (ref!1),
                     action_expr_adt[semantic_base.id].fields(a!1)),
               
list_props[action_expr_adt[semantic_base.id].action_expr].append
                   
(DisCo_action_refinement_adt[semantic_base.id].new_assignments
                         (ref!1),
                     action_expr_adt[semantic_base.id].body(a!1))),
           ra!1, b!1)
  |-------
{1}   semantics.sem
          (action_semantics_utilities.variable_assignments
               (action_semantics_utilities.role_of_object
                    (ob!1, ra!1,
                     action_expr_adt[semantic_base.id].roles(a!1)),
                list_props[semantic_base.id].append
                   
(DisCo_action_refinement_adt[semantic_base.id].new_fields
                         (ref!1),
                     action_expr_adt[semantic_base.id].fields(a!1)),
               
list_props[((action_syntactic_constraints[id].explicit_assign?))].append
                   
(DisCo_action_refinement_adt[semantic_base.id].new_assignments
                         (ref!1),
                     action_expr_adt[semantic_base.id].body(a!1))),
           ra!1, b!1)