63.01/17.77 MAYBE 63.01/17.77 63.01/17.77 Problem: 63.01/17.77 +(a(),b()) -> b() 63.01/17.77 +(c(),a()) -> a() 63.01/17.77 +(x,y) -> +(y,x) 63.01/17.77 +(+(x,y),z) -> +(x,+(y,z)) 63.01/17.77 63.01/17.77 Proof: 63.01/17.77 Open 63.11/17.77 EOF