Substitution related query formulation

[Manjeet Dahiya]

Hello,

I have a boolean fourmula f(a, b, x, y). Where a and b are boolean expressions and x and y are bitvector expressions.

I want to define the following query for validity:

f(a, b, x, y) such that a = false && b = false
->
f(a, b, x, y) such that a = true && b = false

In a way, I need to substitute the values of a and b in the formula on both the sides of implication.

Please advise how to create such a query.

Thanks,
Manjeet Dahiya