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