| โโu,q. u ฯต ๐๐ & q ฯต u & ๐.u โ t & ๐โq = p
| โโv,u,q. v ฯต ๐๐ & u ฯต ๐๐ & q ฯต u & @v.u โ t & ๐โq = p
| โโv,u,q. v ฯต ๐๐ & u ฯต ๐๐ & q ฯต v & @v.u โ t & ๐ฆโq = p
| โโu,q. u ฯต ๐๐ & q ฯต u & ๐.u โ t & ๐โq = p
| โโv,u,q. v ฯต ๐๐ & u ฯต ๐๐ & q ฯต u & @v.u โ t & ๐โq = p
| โโv,u,q. v ฯต ๐๐ & u ฯต ๐๐ & q ฯต v & @v.u โ t & ๐ฆโq = p