nLazy: You
might need it but you don’t,
obecause a later if decides not to use it: x
is false
n t:=L; !A; x → !B(t) Þ !A; x → !B(L) x false
n
nSpeculative:
You might not need it but you do,
obecause a later if decides to use it : x is
true
n !A; x → !B(S) Þ t:=S; !A; x → !B(t) x true
n