[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)