# Bertrand, Mannheim, and Schell's theorems

with(dtrisys): interface(prompt=`GEOTHER> `);
ord := [s, _s, a1, a2, a3, u11, u12, u13, u21, u22, u23, 
        u31, u32, u33, kappa, tau, _kappa, _tau]:
depend(ord):
H_1 := df(_s)*u11-1+a2*kappa: 
H_2 := -df(a2): 
H_3 := df(_s)*u13-a2*tau: 
H_4 := -df(u11): 
H_5 := df(_s)*_kappa-kappa*u12+tau*u13: 
H_6 := -df(u13): 
H_7 := df(_s)*_kappa*u11-df(_s)*_tau*u31-kappa: 
H_8 := df(_s)*_kappa*u13-df(_s)*_tau*u33+tau: 
H_9 := -df(u31): 
H_10 := -df(_s)*_tau-kappa*u31+tau*u33: 
H_11 := -df(u33): 
H_12 := u11-u33: 
H_13 := u13+u31: 
H_14 := u11^2+u13^2-1:
hyp := {'cat(H_,i)'$'i'=1..14}:
con := [df(kappa)*df(tau,2)-df(kappa,2)*df(tau),
        df((1+a2*_kappa)*(1-a2*kappa)),
        df(_tau*tau)]:
BertrandMannheimSchell := dTheorem(hyp, con, ord);

Remark(
`   For more details, see`,
`D. Wang: A Method for Proving Theorems in Differential Geometry and`,
`   Mechanics. J. Univ. Comput. Sci. 1 (1995): 658-673.`, 
`W.-t. Wu: Mechanical Theorem Proving of Differential Geometries and Some`,
`   of Its Applications in Mechanics. J. Automat. Reason.7 (1991): 171-191.` 
):
