Sufficient ICs

A formula G is a sufficient IC of f if

f(x,t) _ f(y,tí) _ G(x,y,t,tí) _ x=y

Ö provided that:

• it is not equivalent to universal identity:

  ¨_xyttí G(x,y,t,tí) _ x=y
  

• it is not trivially false:

  _xyttí G(x,y,t,tí)
  

Previous slide

Next slide

Back to first slide

View graphic version