[ ] Add direct manipulation using the association list. Here, a non-temporary association should be used, deleted, and finally reinstating the prior association (if any).
[ ] Exists(f, begin, end) and Exists(f, c)
[ ] ForAll(f, begin, end) and ForAll(f, c)
[ ] RelProd(f, g, begin, end) and RelProd(f, g, c)
[ ] Substitute(f, begin, end) and Substitute(f, m)
[ ] VarSubstitute(f, begin, end) and VarSubstitute(f, m)
BDD
[ ] Add direct manipulation using the association list. Again, a non-temporary association should be used, deleted, and finally the prior association (if any) should be reinstated.
[ ] Exists(begin, end) and Exists(c)
[ ] ForAll(begin, end) and ForAll(c)
[ ] RelProd(g, begin, end) and RelProd(g, c)
[ ] Substitute(begin, end) and Substitute(m)
[ ] VarSubstitute(begin, end) and VarSubstitute(m)
Cal
Exists(f, begin, end)
andExists(f, c)
ForAll(f, begin, end)
andForAll(f, c)
RelProd(f, g, begin, end)
andRelProd(f, g, c)
Substitute(f, begin, end)
andSubstitute(f, m)
VarSubstitute(f, begin, end)
andVarSubstitute(f, m)
BDD
Exists(begin, end)
andExists(c)
ForAll(begin, end)
andForAll(c)
RelProd(g, begin, end)
andRelProd(g, c)
Substitute(begin, end)
andSubstitute(m)
VarSubstitute(begin, end)
andVarSubstitute(m)