This is not verified by Dafny:
assert forall p,q,p',q' :: (p==>p' && q==>q') ==> (p||q ==> p'||q') ;
And, more generally, I'm having trouble verifying calculations involving disjunction.
Reasoning with disjunction
Tato
0
Viewed 28
1 Answers
assert forall p,q,p',q' :: ((p==>p') && (q==>q')) ==> (p||q ==> p'||q') ;
Don't forget the parentheses around ==>, otherwise your second condition is treated as p ==> ((p' && q) ==> q')
Related