# mcrl2/lps/sumelm.h¶

Include file:

#include "mcrl2/lps/sumelm.h"


Provides an implemenation of the sum elimination lemma, as well as the removal of unused summation variables. The sum elimination lemma is the following: sum d:D . d == e -> X(d) = X(e). Removal of unused summation variables is according to the following lemma: d not in x implies sum d:D . x = x.

## Functions¶

bool mcrl2::lps::sumelm(action_summand &s)

Apply the sum elimination lemma to summand s.

Parameters:

• s an action summand

Returns: true if any summation variables have been removed, or false otherwise.

bool mcrl2::lps::sumelm(stochastic_action_summand &s)

Apply the sum elimination lemma to summand s.

Parameters:

• s a stochastic action summand

Returns: true if any summation variables have been removed, or false otherwise.

bool mcrl2::lps::sumelm(deadlock_summand &s)

Apply the sum elimination lemma to summand s.

Parameters: