symbex

Synopsis: symbex;

Description:

Applies rules until there is no modality on the seuqent. That is, this macro symbolically executes the program to prove.

Arguments:

No arguments required