THEORY exercises IS

  xx\x => ff(xx,x);
  
  x\xx => ff(xx,x);
  
  x\xx => ff(x,xx);
  
  xx\x => ff(x,xx);
  
  bvrb(x) & x\xx => ff(xx,x);
  
  bvrb(x) & x\xx => ff(x,xx);

  bvrb(x) & xx\x => ff(x,xx);
  
  bvrb(x,z,xx) => ff(xx,x);
  
  bvrb(x,z,xx) => ff(x,xx);
  
  bvrb(x) => ff(x,!x.pp(x));
  
  bvrb(x) => ff(x,!xx.pp(x))
      
TAC

  DED;testX;WRITE
  
END
  
&

THEORY testX IS
  
  bwritef("\n      FAILURE: % is (or can be) free in %\n",x,y) 
  => 
  ff(x,y);
  
  x\y & 
  bwritef("\n      SUCCESS: % is not free in %\n",x,y)
  =>
  ff(x,y)
  
END
