「xを0に近づけたときのsin(x)/xの極限値がyである」という式の入力と出力です．RedLog rlqe(rlcnf(rlpnf( all(p,p>0 impl ex(q,q>0 and all({x,s,c},(0<x<q and 0<s<x and 0<c*x<s and c^2+s^2=1) impl (y-p)*x<s<(y+p)*x))) ))); 8*y**2 + 8*y + 1 > 0 and 8*y**2 - 8*y + 1 > 0 and 8*y**2 - 8*y - 1 0 and 2*y**2 - 3 そして rlqe(ex(y,8*y**2 + 8*y +</x<q>…

「線形変換(p,q)|->(p+aq,p+q)による円板p^2+q^2 rlgsn(rlqe( ex({p,q},x=p+a*q and y=p+q and p^2+q^2 QEPCAD B (a,x,y,p,q) 3 (E p)(E q)[x=p+a q /\ y=p+q /\ p^2+q^2 Mathematica FullSimplify[Reduce[Exists[{p,q},x==p+a*q && y==p+q && p^2+q^2 この…