ArchiveEntry "10: Simple rotational dynamics" Description "10.3.7 Simple rotational dynamics". Definitions Real r; /* radius r of circle around origin */ End. ProgramVariables Real v,w; /* direction in x/y-axis */ End. Problem v^2+w^2-r^2=0 -> [{v'=w,w'=-v}@invariant(v^2+w^2-r^2=0)] v^2+w^2-r^2=0 End. Tactic "10: Simple rotational dynamics: Proof 1" implyR(1) ; dI(1) End. End. ArchiveEntry "10: Self-crossing invariant" Description "Example 10.7: Self-crossing". Definitions Real c; End. ProgramVariables Real x,y; End. Problem x^2+x^3-y^2-c=0 -> [{x' = -2*y, y' = -2*x - 3*x^2}] x^2+x^3-y^2-c=0 End. Tactic "10: Self-crossing invariant: Proof 1" implyR(1) ; dI(1) End. Illustration "https://lfcps.org/info/fig-self-crossing.png". End. ArchiveEntry "10: Motzkin polynomial invariant" Description "Example 10.8: Motzkin". Definitions Real c; End. ProgramVariables Real x; Real y; End. Problem x^4*y^2+x^2*y^4-3*x^2*y^2+1=c -> [ {x'=2*x^4*y+4*x^2*y^3-6*x^2*y, y'=-4*x^3*y^2-2*x*y^4+6*x*y^2}@invariant(x^4*y^2+x^2*y^4-3*x^2*y^2+1-c=0) ] x^4*y^2+x^2*y^4-3*x^2*y^2+1=c End. Tactic "10: Motzkin polynomial invariant: Proof 1" implyR(1) ; dI(1) End. Illustration "https://lfcps.org/info/fig-DI-dynamics2.png". End. ArchiveEntry "10: Henon-Heiles motion of a star" Description "Henon-Heiles system for the motion of a star around the center of the galaxy". Definitions Real eps; Real A; Real B; End. ProgramVariables Real x, y; /* x/y-position */ Real u, v; /* x/y-direction */ End. Problem 1/2 * (u^2 + v^2 + A*x^2 + B*y^2) + x^2*y - 1/3 * eps * y^3 = 0 -> [{x'=u,y'=v,u'=-A*x - 2*x*y, v'= -B*y + eps*y^2 - x^2}]1/2 * (u^2 + v^2 + A*x^2 + B*y^2) + x^2*y - 1/3 * eps * y^3 = 0 End. Tactic "10: Henon-Heiles motion of a star: Proof 1" implyR(1) ; dI(1) End. End.