199.26/60.08 MAYBE 199.26/60.09 199.26/60.09 Problem: 199.26/60.09 .(R,.(T,U)) -> .(.(R,T),U) 199.26/60.09 .(R,id()) -> R 199.26/60.09 .(id(),R) -> R 199.26/60.09 and(id(),id()) -> id() 199.26/60.09 sub(id(),id()) -> id() 199.26/60.09 .(and(R,T),and(U,V)) -> and(.(R,U),.(T,V)) 199.26/60.09 .(sub(R,T),sub(U,V)) -> sub(.(U,R),.(T,V)) 199.26/60.09 .(and(R,T),w1()) -> .(w1(),R) 199.26/60.09 .(and(R,T),w2()) -> .(w2(),T) 199.26/60.09 .(R,c()) -> .(c(),and(R,R)) 199.26/60.09 .(c(),w1()) -> id() 199.26/60.09 .(c(),w2()) -> id() 199.26/60.09 .(R,i()) -> .(i(),sub(id(),and(R,id()))) 199.26/60.09 .(and(.(i(),sub(id(),R)),T),e()) -> .(and(id(),T),R) 199.26/60.09 .(.(W,and(R,T)),and(U,V)) -> .(W,and(.(R,U),.(T,V))) 199.26/60.09 .(.(W,sub(R,T)),sub(U,V)) -> .(W,sub(.(U,R),.(T,V))) 199.26/60.09 .(.(W,and(R,T)),w1()) -> .(.(W,w1()),R) 199.26/60.09 .(.(W,and(R,T)),w2()) -> .(.(W,w2()),T) 199.26/60.09 .(and(i(),R),e()) -> and(id(),R) 199.26/60.09 .(.(W,and(i(),R)),e()) -> .(W,and(id(),R)) 199.26/60.09 .(.(W,and(.(i(),sub(id(),R)),T)),e()) -> .(.(W,and(id(),T)),R) 199.26/60.09 199.26/60.09 Proof: 199.26/60.09 Open 199.26/60.09 EOF