:: SIN_COS5 semantic presentation

REAL is V45() V46() V47() V51() set
NAT is V45() V46() V47() V48() V49() V50() V51() M2(K6(REAL))
K6(REAL) is set
COMPLEX is V45() V51() set
RAT is V45() V46() V47() V48() V51() set
INT is V45() V46() V47() V48() V49() V51() set
K7(COMPLEX,COMPLEX) is V35() set
K6(K7(COMPLEX,COMPLEX)) is set
K7(K7(COMPLEX,COMPLEX),COMPLEX) is V35() set
K6(K7(K7(COMPLEX,COMPLEX),COMPLEX)) is set
K7(REAL,REAL) is V35() V36() V37() set
K6(K7(REAL,REAL)) is set
K7(K7(REAL,REAL),REAL) is V35() V36() V37() set
K6(K7(K7(REAL,REAL),REAL)) is set
K7(RAT,RAT) is V20( RAT ) V35() V36() V37() set
K6(K7(RAT,RAT)) is set
K7(K7(RAT,RAT),RAT) is V20( RAT ) V35() V36() V37() set
K6(K7(K7(RAT,RAT),RAT)) is set
K7(INT,INT) is V20( RAT ) V20( INT ) V35() V36() V37() set
K6(K7(INT,INT)) is set
K7(K7(INT,INT),INT) is V20( RAT ) V20( INT ) V35() V36() V37() set
K6(K7(K7(INT,INT),INT)) is set
K7(NAT,NAT) is V20( RAT ) V20( INT ) V35() V36() V37() V38() set
K7(K7(NAT,NAT),NAT) is V20( RAT ) V20( INT ) V35() V36() V37() V38() set
K6(K7(K7(NAT,NAT),NAT)) is set
K7(NAT,REAL) is V35() V36() V37() set
K6(K7(NAT,REAL)) is set
K7(NAT,COMPLEX) is V35() set
K6(K7(NAT,COMPLEX)) is set
omega is V45() V46() V47() V48() V49() V50() V51() set
K6(omega) is set
K6(NAT) is set
0 is natural V11() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() M3( REAL , NAT )
1 is V1() natural V11() real ext-real positive V33() V34() V45() V46() V47() V48() V49() V50() M3( REAL , NAT )
exp_R is V16() V19( REAL ) V20( REAL ) V21() V30( REAL , REAL ) V35() V36() V37() M2(K6(K7(REAL,REAL)))
sinh is V16() V19( REAL ) V20( REAL ) V21() V30( REAL , REAL ) V35() V36() V37() M2(K6(K7(REAL,REAL)))
2 is V1() natural V11() real ext-real positive V33() V34() V45() V46() V47() V48() V49() V50() M3( REAL , NAT )
cosh is V16() V19( REAL ) V20( REAL ) V21() V30( REAL , REAL ) V35() V36() V37() M2(K6(K7(REAL,REAL)))
tanh is V16() V19( REAL ) V20( REAL ) V21() V30( REAL , REAL ) V35() V36() V37() M2(K6(K7(REAL,REAL)))
cosh . 0 is V11() real ext-real M2( REAL )
sinh . 0 is V11() real ext-real M2( REAL )
x is V11() real ext-real set
cos x is V11() real ext-real set
cosec x is V11() real ext-real M2( REAL )
sin x is V11() real ext-real set
1 / (sin x) is V11() real ext-real set
sec x is V11() real ext-real M2( REAL )
1 / (cos x) is V11() real ext-real set
tan x is V11() real ext-real M2( REAL )
(sin x) / (cos x) is V11() real ext-real set
(sec x) / (tan x) is V11() real ext-real M2( REAL )
1 / (cos x) is V11() real ext-real M2( REAL )
(1 / (cos x)) * (cos x) is V11() real ext-real M2( REAL )
(sin x) / (cos x) is V11() real ext-real M2( COMPLEX )
((sin x) / (cos x)) * (cos x) is V11() real ext-real set
((1 / (cos x)) * (cos x)) / (((sin x) / (cos x)) * (cos x)) is V11() real ext-real M2( REAL )
1 / (((sin x) / (cos x)) * (cos x)) is V11() real ext-real M2( REAL )
1 / (sin x) is V11() real ext-real M2( REAL )
x is V11() real ext-real set
sin x is V11() real ext-real set
cos x is V11() real ext-real set
cot x is V11() real ext-real M2( REAL )
(cos x) / (sin x) is V11() real ext-real set
(sin x) * (cot x) is V11() real ext-real M2( REAL )
(sin x) / (sin x) is V11() real ext-real M2( COMPLEX )
((sin x) / (sin x)) * (cos x) is V11() real ext-real set
x is V11() real ext-real set
sin x is V11() real ext-real set
cot x is V11() real ext-real M2( REAL )
cos x is V11() real ext-real set
(cos x) / (sin x) is V11() real ext-real set
x2 is V11() real ext-real set
sin x2 is V11() real ext-real set
x + x2 is V11() real ext-real set
(sin x) * (sin x2) is V11() real ext-real set
cot x2 is V11() real ext-real M2( REAL )
cos x2 is V11() real ext-real set
(cos x2) / (sin x2) is V11() real ext-real set
(cot x) * (cot x2) is V11() real ext-real M2( REAL )
a is V11() real ext-real set
sin a is V11() real ext-real set
(x + x2) + a is V11() real ext-real set
sin ((x + x2) + a) is V11() real ext-real set
((sin x) * (sin x2)) * (sin a) is V11() real ext-real set
cot a is V11() real ext-real M2( REAL )
cos a is V11() real ext-real set
(cos a) / (sin a) is V11() real ext-real set
(cot x2) * (cot a) is V11() real ext-real M2( REAL )
(cot x) * (cot a) is V11() real ext-real M2( REAL )
((cot x2) * (cot a)) + ((cot x) * (cot a)) is V11() real ext-real M2( REAL )
(((cot x2) * (cot a)) + ((cot x) * (cot a))) + ((cot x) * (cot x2)) is V11() real ext-real M2( REAL )
((((cot x2) * (cot a)) + ((cot x) * (cot a))) + ((cot x) * (cot x2))) - 1 is V11() real ext-real M2( REAL )
(((sin x) * (sin x2)) * (sin a)) * (((((cot x2) * (cot a)) + ((cot x) * (cot a))) + ((cot x) * (cot x2))) - 1) is V11() real ext-real M2( REAL )
x2 + a is V11() real ext-real set
x + (x2 + a) is V11() real ext-real set
sin (x + (x2 + a)) is V11() real ext-real set
cos (x2 + a) is V11() real ext-real set
(sin x) * (cos (x2 + a)) is V11() real ext-real set
sin (x2 + a) is V11() real ext-real set
(cos x) * (sin (x2 + a)) is V11() real ext-real set
((sin x) * (cos (x2 + a))) + ((cos x) * (sin (x2 + a))) is V11() real ext-real set
(cos x2) * (cos a) is V11() real ext-real set
(sin x2) * (sin a) is V11() real ext-real set
((cos x2) * (cos a)) - ((sin x2) * (sin a)) is V11() real ext-real set
(sin x) * (((cos x2) * (cos a)) - ((sin x2) * (sin a))) is V11() real ext-real set
((sin x) * (((cos x2) * (cos a)) - ((sin x2) * (sin a)))) + ((cos x) * (sin (x2 + a))) is V11() real ext-real set
(sin x) * ((cos x2) * (cos a)) is V11() real ext-real set
(sin x) * ((sin x2) * (sin a)) is V11() real ext-real set
((sin x) * ((cos x2) * (cos a))) - ((sin x) * ((sin x2) * (sin a))) is V11() real ext-real set
(sin x2) * (cos a) is V11() real ext-real set
(cos x2) * (sin a) is V11() real ext-real set
((sin x2) * (cos a)) + ((cos x2) * (sin a)) is V11() real ext-real set
(cos x) * (((sin x2) * (cos a)) + ((cos x2) * (sin a))) is V11() real ext-real set
(((sin x) * ((cos x2) * (cos a))) - ((sin x) * ((sin x2) * (sin a)))) + ((cos x) * (((sin x2) * (cos a)) + ((cos x2) * (sin a)))) is V11() real ext-real set
(sin x) * (cos x2) is V11() real ext-real set
((sin x) * (cos x2)) * (cos a) is V11() real ext-real set
(((sin x) * (cos x2)) * (cos a)) - (((sin x) * (sin x2)) * (sin a)) is V11() real ext-real set
(cos x) * (sin x2) is V11() real ext-real set
((cos x) * (sin x2)) * (cos a) is V11() real ext-real set
(cos x) * (cos x2) is V11() real ext-real set
((cos x) * (cos x2)) * (sin a) is V11() real ext-real set
(((cos x) * (sin x2)) * (cos a)) + (((cos x) * (cos x2)) * (sin a)) is V11() real ext-real set
((((sin x) * (cos x2)) * (cos a)) - (((sin x) * (sin x2)) * (sin a))) + ((((cos x) * (sin x2)) * (cos a)) + (((cos x) * (cos x2)) * (sin a))) is V11() real ext-real set
(sin x2) * (cot x2) is V11() real ext-real M2( REAL )
(sin x) * ((sin x2) * (cot x2)) is V11() real ext-real M2( REAL )
((sin x) * ((sin x2) * (cot x2))) * (cos a) is V11() real ext-real M2( REAL )
(((sin x) * ((sin x2) * (cot x2))) * (cos a)) - (((sin x) * (sin x2)) * (sin a)) is V11() real ext-real M2( REAL )
((((sin x) * ((sin x2) * (cot x2))) * (cos a)) - (((sin x) * (sin x2)) * (sin a))) + ((((cos x) * (sin x2)) * (cos a)) + (((cos x) * (cos x2)) * (sin a))) is V11() real ext-real M2( REAL )
(sin a) * (cot a) is V11() real ext-real M2( REAL )
((sin x) * ((sin x2) * (cot x2))) * ((sin a) * (cot a)) is V11() real ext-real M2( REAL )
(((sin x) * ((sin x2) * (cot x2))) * ((sin a) * (cot a))) - (((sin x) * (sin x2)) * (sin a)) is V11() real ext-real M2( REAL )
((((sin x) * ((sin x2) * (cot x2))) * ((sin a) * (cot a))) - (((sin x) * (sin x2)) * (sin a))) + ((((cos x) * (sin x2)) * (cos a)) + (((cos x) * (cos x2)) * (sin a))) is V11() real ext-real M2( REAL )
((cot x2) * (cot a)) - 1 is V11() real ext-real M2( REAL )
(((sin x) * (sin x2)) * (sin a)) * (((cot x2) * (cot a)) - 1) is V11() real ext-real M2( REAL )
(sin x) * (cot x) is V11() real ext-real M2( REAL )
((sin x) * (cot x)) * (sin x2) is V11() real ext-real M2( REAL )
(((sin x) * (cot x)) * (sin x2)) * (cos a) is V11() real ext-real M2( REAL )
((((sin x) * (cot x)) * (sin x2)) * (cos a)) + (((cos x) * (cos x2)) * (sin a)) is V11() real ext-real M2( REAL )
((((sin x) * (sin x2)) * (sin a)) * (((cot x2) * (cot a)) - 1)) + (((((sin x) * (cot x)) * (sin x2)) * (cos a)) + (((cos x) * (cos x2)) * (sin a))) is V11() real ext-real M2( REAL )
(((sin x) * (cot x)) * (sin x2)) * ((sin a) * (cot a)) is V11() real ext-real M2( REAL )
((((sin x) * (cot x)) * (sin x2)) * ((sin a) * (cot a))) + (((cos x) * (cos x2)) * (sin a)) is V11() real ext-real M2( REAL )
((((sin x) * (sin x2)) * (sin a)) * (((cot x2) * (cot a)) - 1)) + (((((sin x) * (cot x)) * (sin x2)) * ((sin a) * (cot a))) + (((cos x) * (cos x2)) * (sin a))) is V11() real ext-real M2( REAL )
(((sin x) * (sin x2)) * (sin a)) * (cot x) is V11() real ext-real M2( REAL )
((((sin x) * (sin x2)) * (sin a)) * (cot x)) * (cot a) is V11() real ext-real M2( REAL )
((((sin x) * (sin x2)) * (sin a)) * (((cot x2) * (cot a)) - 1)) + (((((sin x) * (sin x2)) * (sin a)) * (cot x)) * (cot a)) is V11() real ext-real M2( REAL )
(((((sin x) * (sin x2)) * (sin a)) * (((cot x2) * (cot a)) - 1)) + (((((sin x) * (sin x2)) * (sin a)) * (cot x)) * (cot a))) + (((cos x) * (cos x2)) * (sin a)) is V11() real ext-real M2( REAL )
(((cot x2) * (cot a)) - 1) + ((cot x) * (cot a)) is V11() real ext-real M2( REAL )
(((sin x) * (sin x2)) * (sin a)) * ((((cot x2) * (cot a)) - 1) + ((cot x) * (cot a))) is V11() real ext-real M2( REAL )
((sin x) * (cot x)) * (cos x2) is V11() real ext-real M2( REAL )
(((sin x) * (cot x)) * (cos x2)) * (sin a) is V11() real ext-real M2( REAL )
((((sin x) * (sin x2)) * (sin a)) * ((((cot x2) * (cot a)) - 1) + ((cot x) * (cot a)))) + ((((sin x) * (cot x)) * (cos x2)) * (sin a)) is V11() real ext-real M2( REAL )
((sin x) * (cot x)) * ((sin x2) * (cot x2)) is V11() real ext-real M2( REAL )
(((sin x) * (cot x)) * ((sin x2) * (cot x2))) * (sin a) is V11() real ext-real M2( REAL )
((((sin x) * (sin x2)) * (sin a)) * ((((cot x2) * (cot a)) - 1) + ((cot x) * (cot a)))) + ((((sin x) * (cot x)) * ((sin x2) * (cot x2))) * (sin a)) is V11() real ext-real M2( REAL )
x is V11() real ext-real set
sin x is V11() real ext-real set
cot x is V11() real ext-real M2( REAL )
cos x is V11() real ext-real set
(cos x) / (sin x) is V11() real ext-real set
x2 is V11() real ext-real set
sin x2 is V11() real ext-real set
x + x2 is V11() real ext-real set
(sin x) * (sin x2) is V11() real ext-real set
cot x2 is V11() real ext-real M2( REAL )
cos x2 is V11() real ext-real set
(cos x2) / (sin x2) is V11() real ext-real set
(cot x) + (cot x2) is V11() real ext-real M2( REAL )
(cot x) * (cot x2) is V11() real ext-real M2( REAL )
a is V11() real ext-real set
sin a is V11() real ext-real set
(x + x2) + a is V11() real ext-real set
cos ((x + x2) + a) is V11() real ext-real set
((sin x) * (sin x2)) * (sin a) is V11() real ext-real set
cot a is V11() real ext-real M2( REAL )
cos a is V11() real ext-real set
(cos a) / (sin a) is V11() real ext-real set
((cot x) + (cot x2)) + (cot a) is V11() real ext-real M2( REAL )
((cot x) * (cot x2)) * (cot a) is V11() real ext-real M2( REAL )
(((cot x) + (cot x2)) + (cot a)) - (((cot x) * (cot x2)) * (cot a)) is V11() real ext-real M2( REAL )
(((sin x) * (sin x2)) * (sin a)) * ((((cot x) + (cot x2)) + (cot a)) - (((cot x) * (cot x2)) * (cot a))) is V11() real ext-real M2( REAL )
- ((((sin x) * (sin x2)) * (sin a)) * ((((cot x) + (cot x2)) + (cot a)) - (((cot x) * (cot x2)) * (cot a)))) is V11() real ext-real M2( REAL )
x2 + a is V11() real ext-real set
x + (x2 + a) is V11() real ext-real set
cos (x + (x2 + a)) is V11() real ext-real set
cos (x2 + a) is V11() real ext-real set
(cos x) * (cos (x2 + a)) is V11() real ext-real set
sin (x2 + a) is V11() real ext-real set
(sin x) * (sin (x2 + a)) is V11() real ext-real set
((cos x) * (cos (x2 + a))) - ((sin x) * (sin (x2 + a))) is V11() real ext-real set
(cos x2) * (cos a) is V11() real ext-real set
(sin x2) * (sin a) is V11() real ext-real set
((cos x2) * (cos a)) - ((sin x2) * (sin a)) is V11() real ext-real set
(cos x) * (((cos x2) * (cos a)) - ((sin x2) * (sin a))) is V11() real ext-real set
((cos x) * (((cos x2) * (cos a)) - ((sin x2) * (sin a)))) - ((sin x) * (sin (x2 + a))) is V11() real ext-real set
(cos x) * ((cos x2) * (cos a)) is V11() real ext-real set
(cos x) * ((sin x2) * (sin a)) is V11() real ext-real set
((cos x) * ((cos x2) * (cos a))) - ((cos x) * ((sin x2) * (sin a))) is V11() real ext-real set
(sin x2) * (cos a) is V11() real ext-real set
(cos x2) * (sin a) is V11() real ext-real set
((sin x2) * (cos a)) + ((cos x2) * (sin a)) is V11() real ext-real set
(sin x) * (((sin x2) * (cos a)) + ((cos x2) * (sin a))) is V11() real ext-real set
(((cos x) * ((cos x2) * (cos a))) - ((cos x) * ((sin x2) * (sin a)))) - ((sin x) * (((sin x2) * (cos a)) + ((cos x2) * (sin a)))) is V11() real ext-real set
(cos x) * (cos x2) is V11() real ext-real set
((cos x) * (cos x2)) * (cos a) is V11() real ext-real set
(cos x) * (sin x2) is V11() real ext-real set
((cos x) * (sin x2)) * (sin a) is V11() real ext-real set
(((cos x) * (cos x2)) * (cos a)) - (((cos x) * (sin x2)) * (sin a)) is V11() real ext-real set
((sin x) * (sin x2)) * (cos a) is V11() real ext-real set
(sin x) * (sin a) is V11() real ext-real set
((sin x) * (sin a)) * (cos x2) is V11() real ext-real set
(((sin x) * (sin x2)) * (cos a)) + (((sin x) * (sin a)) * (cos x2)) is V11() real ext-real set
((((cos x) * (cos x2)) * (cos a)) - (((cos x) * (sin x2)) * (sin a))) - ((((sin x) * (sin x2)) * (cos a)) + (((sin x) * (sin a)) * (cos x2))) is V11() real ext-real set
(sin a) * (cot a) is V11() real ext-real M2( REAL )
((sin x) * (sin x2)) * ((sin a) * (cot a)) is V11() real ext-real M2( REAL )
(((sin x) * (sin x2)) * ((sin a) * (cot a))) + (((sin x) * (sin a)) * (cos x2)) is V11() real ext-real M2( REAL )
((((cos x) * (cos x2)) * (cos a)) - (((cos x) * (sin x2)) * (sin a))) - ((((sin x) * (sin x2)) * ((sin a) * (cot a))) + (((sin x) * (sin a)) * (cos x2))) is V11() real ext-real M2( REAL )
(sin x2) * (cot x2) is V11() real ext-real M2( REAL )
((sin x) * (sin a)) * ((sin x2) * (cot x2)) is V11() real ext-real M2( REAL )
(((sin x) * (sin x2)) * ((sin a) * (cot a))) + (((sin x) * (sin a)) * ((sin x2) * (cot x2))) is V11() real ext-real M2( REAL )
((((cos x) * (cos x2)) * (cos a)) - (((cos x) * (sin x2)) * (sin a))) - ((((sin x) * (sin x2)) * ((sin a) * (cot a))) + (((sin x) * (sin a)) * ((sin x2) * (cot x2)))) is V11() real ext-real M2( REAL )
(sin x) * (cot x) is V11() real ext-real M2( REAL )
((sin x) * (cot x)) * (cos x2) is V11() real ext-real M2( REAL )
(((sin x) * (cot x)) * (cos x2)) * (cos a) is V11() real ext-real M2( REAL )
((((sin x) * (cot x)) * (cos x2)) * (cos a)) - (((cos x) * (sin x2)) * (sin a)) is V11() real ext-real M2( REAL )
(cot a) + (cot x2) is V11() real ext-real M2( REAL )
(((sin x) * (sin x2)) * (sin a)) * ((cot a) + (cot x2)) is V11() real ext-real M2( REAL )
(((((sin x) * (cot x)) * (cos x2)) * (cos a)) - (((cos x) * (sin x2)) * (sin a))) - ((((sin x) * (sin x2)) * (sin a)) * ((cot a) + (cot x2))) is V11() real ext-real M2( REAL )
((sin x) * (cot x)) * ((sin x2) * (cot x2)) is V11() real ext-real M2( REAL )
(((sin x) * (cot x)) * ((sin x2) * (cot x2))) * (cos a) is V11() real ext-real M2( REAL )
((((sin x) * (cot x)) * ((sin x2) * (cot x2))) * (cos a)) - (((cos x) * (sin x2)) * (sin a)) is V11() real ext-real M2( REAL )
(((((sin x) * (cot x)) * ((sin x2) * (cot x2))) * (cos a)) - (((cos x) * (sin x2)) * (sin a))) - ((((sin x) * (sin x2)) * (sin a)) * ((cot a) + (cot x2))) is V11() real ext-real M2( REAL )
(((sin x) * (cot x)) * ((sin x2) * (cot x2))) * ((sin a) * (cot a)) is V11() real ext-real M2( REAL )
((((sin x) * (cot x)) * ((sin x2) * (cot x2))) * ((sin a) * (cot a))) - (((cos x) * (sin x2)) * (sin a)) is V11() real ext-real M2( REAL )
(((((sin x) * (cot x)) * ((sin x2) * (cot x2))) * ((sin a) * (cot a))) - (((cos x) * (sin x2)) * (sin a))) - ((((sin x) * (sin x2)) * (sin a)) * ((cot a) + (cot x2))) is V11() real ext-real M2( REAL )
(((sin x) * (sin x2)) * (sin a)) * (((cot x) * (cot x2)) * (cot a)) is V11() real ext-real M2( REAL )
((sin x) * (cot x)) * (sin x2) is V11() real ext-real M2( REAL )
(((sin x) * (cot x)) * (sin x2)) * (sin a) is V11() real ext-real M2( REAL )
((((sin x) * (sin x2)) * (sin a)) * (((cot x) * (cot x2)) * (cot a))) - ((((sin x) * (cot x)) * (sin x2)) * (sin a)) is V11() real ext-real M2( REAL )
(((((sin x) * (sin x2)) * (sin a)) * (((cot x) * (cot x2)) * (cot a))) - ((((sin x) * (cot x)) * (sin x2)) * (sin a))) - ((((sin x) * (sin x2)) * (sin a)) * ((cot a) + (cot x2))) is V11() real ext-real M2( REAL )
x is V11() real ext-real set
2 * x is V11() real ext-real M2( REAL )
sin (2 * x) is V11() real ext-real M2( REAL )
sin x is V11() real ext-real set
2 * (sin x) is V11() real ext-real M2( REAL )
cos x is V11() real ext-real set
(2 * (sin x)) * (cos x) is V11() real ext-real M2( REAL )
x + x is V11() real ext-real set
sin (x + x) is V11() real ext-real set
(sin x) * (cos x) is V11() real ext-real set
(cos x) * (sin x) is V11() real ext-real set
((sin x) * (cos x)) + ((cos x) * (sin x)) is V11() real ext-real set
x is V11() real ext-real set
cos x is V11() real ext-real set
2 * x is V11() real ext-real M2( REAL )
sin (2 * x) is V11() real ext-real M2( REAL )
tan x is V11() real ext-real M2( REAL )
sin x is V11() real ext-real set
(sin x) / (cos x) is V11() real ext-real set
2 * (tan x) is V11() real ext-real M2( REAL )
(tan x) ^2 is V11() real ext-real M2( REAL )
(tan x) * (tan x) is V11() real ext-real set
1 + ((tan x) ^2) is V11() real ext-real M2( REAL )
(2 * (tan x)) / (1 + ((tan x) ^2)) is V11() real ext-real M2( REAL )
(cos x) ^2 is V11() real ext-real set
(cos x) * (cos x) is V11() real ext-real set
2 * (sin x) is V11() real ext-real M2( REAL )
(2 * (sin x)) * (cos x) is V11() real ext-real M2( REAL )
((2 * (sin x)) * (cos x)) * 1 is V11() real ext-real M2( REAL )
(cos x) / (cos x) is V11() real ext-real M2( COMPLEX )
((2 * (sin x)) * (cos x)) * ((cos x) / (cos x)) is V11() real ext-real M2( REAL )
((2 * (sin x)) * (cos x)) * (cos x) is V11() real ext-real M2( REAL )
(((2 * (sin x)) * (cos x)) * (cos x)) / (cos x) is V11() real ext-real M2( REAL )
2 * ((cos x) ^2) is V11() real ext-real M2( REAL )
(2 * ((cos x) ^2)) * (sin x) is V11() real ext-real M2( REAL )
((2 * ((cos x) ^2)) * (sin x)) / (cos x) is V11() real ext-real M2( REAL )
(2 * ((cos x) ^2)) * (tan x) is V11() real ext-real M2( REAL )
((2 * ((cos x) ^2)) * (tan x)) / 1 is V11() real ext-real M2( REAL )
(2 * (tan x)) * ((cos x) ^2) is V11() real ext-real M2( REAL )
(sin x) ^2 is V11() real ext-real set
(sin x) * (sin x) is V11() real ext-real set
((sin x) ^2) + ((cos x) ^2) is V11() real ext-real set
((2 * (tan x)) * ((cos x) ^2)) / (((sin x) ^2) + ((cos x) ^2)) is V11() real ext-real M2( REAL )
(((sin x) ^2) + ((cos x) ^2)) / ((cos x) ^2) is V11() real ext-real M2( COMPLEX )
(2 * (tan x)) / ((((sin x) ^2) + ((cos x) ^2)) / ((cos x) ^2)) is V11() real ext-real M2( REAL )
((sin x) ^2) / ((cos x) ^2) is V11() real ext-real M2( COMPLEX )
((cos x) ^2) / ((cos x) ^2) is V11() real ext-real M2( COMPLEX )
(((sin x) ^2) / ((cos x) ^2)) + (((cos x) ^2) / ((cos x) ^2)) is V11() real ext-real M2( COMPLEX )
(2 * (tan x)) / ((((sin x) ^2) / ((cos x) ^2)) + (((cos x) ^2) / ((cos x) ^2))) is V11() real ext-real M2( REAL )
(((sin x) ^2) / ((cos x) ^2)) + 1 is V11() real ext-real M2( REAL )
(2 * (tan x)) / ((((sin x) ^2) / ((cos x) ^2)) + 1) is V11() real ext-real M2( REAL )
((tan x) ^2) + 1 is V11() real ext-real M2( REAL )
(2 * (tan x)) / (((tan x) ^2) + 1) is V11() real ext-real M2( REAL )
x is V11() real ext-real set
2 * x is V11() real ext-real M2( REAL )
cos (2 * x) is V11() real ext-real M2( REAL )
cos x is V11() real ext-real set
(cos x) ^2 is V11() real ext-real set
(cos x) * (cos x) is V11() real ext-real set
sin x is V11() real ext-real set
(sin x) ^2 is V11() real ext-real set
(sin x) * (sin x) is V11() real ext-real set
((cos x) ^2) - ((sin x) ^2) is V11() real ext-real set
2 * ((cos x) ^2) is V11() real ext-real M2( REAL )
(2 * ((cos x) ^2)) - 1 is V11() real ext-real M2( REAL )
2 * ((sin x) ^2) is V11() real ext-real M2( REAL )
1 - (2 * ((sin x) ^2)) is V11() real ext-real M2( REAL )
x + x is V11() real ext-real set
cos (x + x) is V11() real ext-real set
(((cos x) ^2) - ((sin x) ^2)) - 1 is V11() real ext-real M2( REAL )
((((cos x) ^2) - ((sin x) ^2)) - 1) + 1 is V11() real ext-real M2( REAL )
((cos x) ^2) + ((sin x) ^2) is V11() real ext-real set
(((cos x) ^2) - ((sin x) ^2)) - (((cos x) ^2) + ((sin x) ^2)) is V11() real ext-real set
((((cos x) ^2) - ((sin x) ^2)) - (((cos x) ^2) + ((sin x) ^2))) + 1 is V11() real ext-real M2( REAL )
- 1 is V11() real ext-real M2( REAL )
(- 1) + (2 * ((sin x) ^2)) is V11() real ext-real M2( REAL )
- ((- 1) + (2 * ((sin x) ^2))) is V11() real ext-real M2( REAL )
x is V11() real ext-real set
cos x is V11() real ext-real set
2 * x is V11() real ext-real M2( REAL )
cos (2 * x) is V11() real ext-real M2( REAL )
tan x is V11() real ext-real M2( REAL )
sin x is V11() real ext-real set
(sin x) / (cos x) is V11() real ext-real set
(tan x) ^2 is V11() real ext-real M2( REAL )
(tan x) * (tan x) is V11() real ext-real set
1 - ((tan x) ^2) is V11() real ext-real M2( REAL )
1 + ((tan x) ^2) is V11() real ext-real M2( REAL )
(1 - ((tan x) ^2)) / (1 + ((tan x) ^2)) is V11() real ext-real M2( REAL )
(cos x) ^2 is V11() real ext-real set
(cos x) * (cos x) is V11() real ext-real set
(sin x) ^2 is V11() real ext-real set
(sin x) * (sin x) is V11() real ext-real set
((cos x) ^2) - ((sin x) ^2) is V11() real ext-real set
(((cos x) ^2) - ((sin x) ^2)) * 1 is V11() real ext-real M2( REAL )
((cos x) ^2) / ((cos x) ^2) is V11() real ext-real M2( COMPLEX )
(((cos x) ^2) - ((sin x) ^2)) * (((cos x) ^2) / ((cos x) ^2)) is V11() real ext-real set
(((cos x) ^2) - ((sin x) ^2)) / ((cos x) ^2) is V11() real ext-real M2( COMPLEX )
((((cos x) ^2) - ((sin x) ^2)) / ((cos x) ^2)) * ((cos x) ^2) is V11() real ext-real set
((sin x) ^2) / ((cos x) ^2) is V11() real ext-real M2( COMPLEX )
(((cos x) ^2) / ((cos x) ^2)) - (((sin x) ^2) / ((cos x) ^2)) is V11() real ext-real M2( COMPLEX )
((((cos x) ^2) / ((cos x) ^2)) - (((sin x) ^2) / ((cos x) ^2))) * ((cos x) ^2) is V11() real ext-real set
1 - (((sin x) ^2) / ((cos x) ^2)) is V11() real ext-real M2( REAL )
(1 - (((sin x) ^2) / ((cos x) ^2))) * ((cos x) ^2) is V11() real ext-real M2( REAL )
(1 - ((tan x) ^2)) * ((cos x) ^2) is V11() real ext-real M2( REAL )
((1 - ((tan x) ^2)) * ((cos x) ^2)) / 1 is V11() real ext-real M2( REAL )
((cos x) ^2) + ((sin x) ^2) is V11() real ext-real set
((1 - ((tan x) ^2)) * ((cos x) ^2)) / (((cos x) ^2) + ((sin x) ^2)) is V11() real ext-real M2( REAL )
(((cos x) ^2) + ((sin x) ^2)) / ((cos x) ^2) is V11() real ext-real M2( COMPLEX )
(1 - ((tan x) ^2)) / ((((cos x) ^2) + ((sin x) ^2)) / ((cos x) ^2)) is V11() real ext-real M2( REAL )
(((cos x) ^2) / ((cos x) ^2)) + (((sin x) ^2) / ((cos x) ^2)) is V11() real ext-real M2( COMPLEX )
(1 - ((tan x) ^2)) / ((((cos x) ^2) / ((cos x) ^2)) + (((sin x) ^2) / ((cos x) ^2))) is V11() real ext-real M2( REAL )
1 + (((sin x) ^2) / ((cos x) ^2)) is V11() real ext-real M2( REAL )
(1 - ((tan x) ^2)) / (1 + (((sin x) ^2) / ((cos x) ^2))) is V11() real ext-real M2( REAL )
x is V11() real ext-real set
cos x is V11() real ext-real set
2 * x is V11() real ext-real M2( REAL )
tan (2 * x) is V11() real ext-real M2( REAL )
sin (2 * x) is V11() real ext-real set
cos (2 * x) is V11() real ext-real set
(sin (2 * x)) / (cos (2 * x)) is V11() real ext-real set
tan x is V11() real ext-real M2( REAL )
sin x is V11() real ext-real set
(sin x) / (cos x) is V11() real ext-real set
2 * (tan x) is V11() real ext-real M2( REAL )
(tan x) ^2 is V11() real ext-real M2( REAL )
(tan x) * (tan x) is V11() real ext-real set
1 - ((tan x) ^2) is V11() real ext-real M2( REAL )
(2 * (tan x)) / (1 - ((tan x) ^2)) is V11() real ext-real M2( REAL )
x + x is V11() real ext-real set
tan (x + x) is V11() real ext-real M2( REAL )
sin (x + x) is V11() real ext-real set
cos (x + x) is V11() real ext-real set
(sin (x + x)) / (cos (x + x)) is V11() real ext-real set
(tan x) + (tan x) is V11() real ext-real M2( REAL )
(tan x) * (tan x) is V11() real ext-real M2( REAL )
1 - ((tan x) * (tan x)) is V11() real ext-real M2( REAL )
((tan x) + (tan x)) / (1 - ((tan x) * (tan x))) is V11() real ext-real M2( REAL )
(2 * (tan x)) / (1 - ((tan x) * (tan x))) is V11() real ext-real M2( REAL )
x is V11() real ext-real set
sin x is V11() real ext-real set
2 * x is V11() real ext-real M2( REAL )
cot (2 * x) is V11() real ext-real M2( REAL )
cos (2 * x) is V11() real ext-real set
sin (2 * x) is V11() real ext-real set
(cos (2 * x)) / (sin (2 * x)) is V11() real ext-real set
cot x is V11() real ext-real M2( REAL )
cos x is V11() real ext-real set
(cos x) / (sin x) is V11() real ext-real set
(cot x) ^2 is V11() real ext-real M2( REAL )
(cot x) * (cot x) is V11() real ext-real set
((cot x) ^2) - 1 is V11() real ext-real M2( REAL )
2 * (cot x) is V11() real ext-real M2( REAL )
(((cot x) ^2) - 1) / (2 * (cot x)) is V11() real ext-real M2( REAL )
x + x is V11() real ext-real set
cot (x + x) is V11() real ext-real M2( REAL )
cos (x + x) is V11() real ext-real set
sin (x + x) is V11() real ext-real set
(cos (x + x)) / (sin (x + x)) is V11() real ext-real set
(cot x) * (cot x) is V11() real ext-real M2( REAL )
((cot x) * (cot x)) - 1 is V11() real ext-real M2( REAL )
(cot x) + (cot x) is V11() real ext-real M2( REAL )
(((cot x) * (cot x)) - 1) / ((cot x) + (cot x)) is V11() real ext-real M2( REAL )
(((cot x) * (cot x)) - 1) / (2 * (cot x)) is V11() real ext-real M2( REAL )
x is V11() real ext-real set
cos x is V11() real ext-real set
sec x is V11() real ext-real M2( REAL )
1 / (cos x) is V11() real ext-real set
(sec x) ^2 is V11() real ext-real M2( REAL )
(sec x) * (sec x) is V11() real ext-real set
tan x is V11() real ext-real M2( REAL )
sin x is V11() real ext-real set
(sin x) / (cos x) is V11() real ext-real set
(tan x) ^2 is V11() real ext-real M2( REAL )
(tan x) * (tan x) is V11() real ext-real set
1 + ((tan x) ^2) is V11() real ext-real M2( REAL )
(cos x) ^2 is V11() real ext-real set
(cos x) * (cos x) is V11() real ext-real set
1 ^2 is V11() real ext-real M2( REAL )
1 * 1 is V11() real ext-real set
(1 ^2) / ((cos x) ^2) is V11() real ext-real M2( REAL )
(sin x) ^2 is V11() real ext-real set
(sin x) * (sin x) is V11() real ext-real set
((sin x) ^2) + ((cos x) ^2) is V11() real ext-real set
(((sin x) ^2) + ((cos x) ^2)) / ((cos x) ^2) is V11() real ext-real M2( COMPLEX )
((sin x) ^2) / ((cos x) ^2) is V11() real ext-real M2( COMPLEX )
((cos x) ^2) / ((cos x) ^2) is V11() real ext-real M2( COMPLEX )
(((sin x) ^2) / ((cos x) ^2)) + (((cos x) ^2) / ((cos x) ^2)) is V11() real ext-real M2( COMPLEX )
(((sin x) ^2) / ((cos x) ^2)) + 1 is V11() real ext-real M2( REAL )
(sin x) / (cos x) is V11() real ext-real M2( COMPLEX )
((sin x) / (cos x)) ^2 is V11() real ext-real M2( COMPLEX )
((sin x) / (cos x)) * ((sin x) / (cos x)) is V11() real ext-real set
(((sin x) / (cos x)) ^2) + 1 is V11() real ext-real M2( REAL )
x is V11() real ext-real set
cot x is V11() real ext-real M2( REAL )
cos x is V11() real ext-real set
sin x is V11() real ext-real set
(cos x) / (sin x) is V11() real ext-real set
tan x is V11() real ext-real M2( REAL )
(sin x) / (cos x) is V11() real ext-real set
1 / (tan x) is V11() real ext-real M2( REAL )
x is V11() real ext-real set
cos x is V11() real ext-real set
sin x is V11() real ext-real set
2 * x is V11() real ext-real M2( REAL )
sec (2 * x) is V11() real ext-real M2( REAL )
cos (2 * x) is V11() real ext-real set
1 / (cos (2 * x)) is V11() real ext-real set
sec x is V11() real ext-real M2( REAL )
1 / (cos x) is V11() real ext-real set
(sec x) ^2 is V11() real ext-real M2( REAL )
(sec x) * (sec x) is V11() real ext-real set
tan x is V11() real ext-real M2( REAL )
(sin x) / (cos x) is V11() real ext-real set
(tan x) ^2 is V11() real ext-real M2( REAL )
(tan x) * (tan x) is V11() real ext-real set
1 - ((tan x) ^2) is V11() real ext-real M2( REAL )
((sec x) ^2) / (1 - ((tan x) ^2)) is V11() real ext-real M2( REAL )
cot x is V11() real ext-real M2( REAL )
(cos x) / (sin x) is V11() real ext-real set
(cot x) + (tan x) is V11() real ext-real M2( REAL )
(cot x) - (tan x) is V11() real ext-real M2( REAL )
((cot x) + (tan x)) / ((cot x) - (tan x)) is V11() real ext-real M2( REAL )
1 + ((tan x) ^2) is V11() real ext-real M2( REAL )
(1 - ((tan x) ^2)) / (1 + ((tan x) ^2)) is V11() real ext-real M2( REAL )
1 / ((1 - ((tan x) ^2)) / (1 + ((tan x) ^2))) is V11() real ext-real M2( REAL )
(1 + ((tan x) ^2)) / (1 - ((tan x) ^2)) is V11() real ext-real M2( REAL )
(1 + ((tan x) ^2)) / (tan x) is V11() real ext-real M2( REAL )
(1 - ((tan x) ^2)) / (tan x) is V11() real ext-real M2( REAL )
((1 + ((tan x) ^2)) / (tan x)) / ((1 - ((tan x) ^2)) / (tan x)) is V11() real ext-real M2( REAL )
1 / (tan x) is V11() real ext-real M2( REAL )
((tan x) ^2) / (tan x) is V11() real ext-real M2( REAL )
(1 / (tan x)) + (((tan x) ^2) / (tan x)) is V11() real ext-real M2( REAL )
((1 / (tan x)) + (((tan x) ^2) / (tan x))) / ((1 - ((tan x) ^2)) / (tan x)) is V11() real ext-real M2( REAL )
(cot x) + (((tan x) ^2) / (tan x)) is V11() real ext-real M2( REAL )
((cot x) + (((tan x) ^2) / (tan x))) / ((1 - ((tan x) ^2)) / (tan x)) is V11() real ext-real M2( REAL )
(1 / (tan x)) - (((tan x) ^2) / (tan x)) is V11() real ext-real M2( REAL )
((cot x) + (((tan x) ^2) / (tan x))) / ((1 / (tan x)) - (((tan x) ^2) / (tan x))) is V11() real ext-real M2( REAL )
(tan x) * (tan x) is V11() real ext-real M2( REAL )
((tan x) * (tan x)) / (tan x) is V11() real ext-real M2( REAL )
(cot x) + (((tan x) * (tan x)) / (tan x)) is V11() real ext-real M2( REAL )
(cot x) - (((tan x) ^2) / (tan x)) is V11() real ext-real M2( REAL )
((cot x) + (((tan x) * (tan x)) / (tan x))) / ((cot x) - (((tan x) ^2) / (tan x))) is V11() real ext-real M2( REAL )
(cot x) - (((tan x) * (tan x)) / (tan x)) is V11() real ext-real M2( REAL )
((cot x) + (tan x)) / ((cot x) - (((tan x) * (tan x)) / (tan x))) is V11() real ext-real M2( REAL )
x is V11() real ext-real set
sin x is V11() real ext-real set
cosec x is V11() real ext-real M2( REAL )
1 / (sin x) is V11() real ext-real set
(cosec x) ^2 is V11() real ext-real M2( REAL )
(cosec x) * (cosec x) is V11() real ext-real set
cot x is V11() real ext-real M2( REAL )
cos x is V11() real ext-real set
(cos x) / (sin x) is V11() real ext-real set
(cot x) ^2 is V11() real ext-real M2( REAL )
(cot x) * (cot x) is V11() real ext-real set
1 + ((cot x) ^2) is V11() real ext-real M2( REAL )
(sin x) ^2 is V11() real ext-real set
(sin x) * (sin x) is V11() real ext-real set
1 ^2 is V11() real ext-real M2( REAL )
1 * 1 is V11() real ext-real set
(1 ^2) / ((sin x) ^2) is V11() real ext-real M2( REAL )
(cos x) ^2 is V11() real ext-real set
(cos x) * (cos x) is V11() real ext-real set
((sin x) ^2) + ((cos x) ^2) is V11() real ext-real set
(((sin x) ^2) + ((cos x) ^2)) / ((sin x) ^2) is V11() real ext-real M2( COMPLEX )
((sin x) ^2) / ((sin x) ^2) is V11() real ext-real M2( COMPLEX )
((cos x) ^2) / ((sin x) ^2) is V11() real ext-real M2( COMPLEX )
(((sin x) ^2) / ((sin x) ^2)) + (((cos x) ^2) / ((sin x) ^2)) is V11() real ext-real M2( COMPLEX )
1 + (((cos x) ^2) / ((sin x) ^2)) is V11() real ext-real M2( REAL )
(cos x) / (sin x) is V11() real ext-real M2( COMPLEX )
((cos x) / (sin x)) ^2 is V11() real ext-real M2( COMPLEX )
((cos x) / (sin x)) * ((cos x) / (sin x)) is V11() real ext-real set
1 + (((cos x) / (sin x)) ^2) is V11() real ext-real M2( REAL )
x is V11() real ext-real set
cos x is V11() real ext-real set
sin x is V11() real ext-real set
2 * x is V11() real ext-real M2( REAL )
cosec (2 * x) is V11() real ext-real M2( REAL )
sin (2 * x) is V11() real ext-real set
1 / (sin (2 * x)) is V11() real ext-real set
sec x is V11() real ext-real M2( REAL )
1 / (cos x) is V11() real ext-real set
cosec x is V11() real ext-real M2( REAL )
1 / (sin x) is V11() real ext-real set
(sec x) * (cosec x) is V11() real ext-real M2( REAL )
((sec x) * (cosec x)) / 2 is V11() real ext-real M2( REAL )
tan x is V11() real ext-real M2( REAL )
(sin x) / (cos x) is V11() real ext-real set
cot x is V11() real ext-real M2( REAL )
(cos x) / (sin x) is V11() real ext-real set
(tan x) + (cot x) is V11() real ext-real M2( REAL )
((tan x) + (cot x)) / 2 is V11() real ext-real M2( REAL )
2 * (tan x) is V11() real ext-real M2( REAL )
(tan x) ^2 is V11() real ext-real M2( REAL )
(tan x) * (tan x) is V11() real ext-real set
1 + ((tan x) ^2) is V11() real ext-real M2( REAL )
(2 * (tan x)) / (1 + ((tan x) ^2)) is V11() real ext-real M2( REAL )
1 / ((2 * (tan x)) / (1 + ((tan x) ^2))) is V11() real ext-real M2( REAL )
(1 + ((tan x) ^2)) / (2 * (tan x)) is V11() real ext-real M2( REAL )
(1 + ((tan x) ^2)) / (tan x) is V11() real ext-real M2( REAL )
((1 + ((tan x) ^2)) / (tan x)) / 2 is V11() real ext-real M2( REAL )
(sin x) / (cos x) is V11() real ext-real M2( COMPLEX )
1 / ((sin x) / (cos x)) is V11() real ext-real M2( REAL )
((tan x) ^2) / (tan x) is V11() real ext-real M2( REAL )
(1 / ((sin x) / (cos x))) + (((tan x) ^2) / (tan x)) is V11() real ext-real M2( REAL )
((1 / ((sin x) / (cos x))) + (((tan x) ^2) / (tan x))) / 2 is V11() real ext-real M2( REAL )
(tan x) * (tan x) is V11() real ext-real M2( REAL )
((tan x) * (tan x)) / (tan x) is V11() real ext-real M2( REAL )
(cot x) + (((tan x) * (tan x)) / (tan x)) is V11() real ext-real M2( REAL )
((cot x) + (((tan x) * (tan x)) / (tan x))) / 2 is V11() real ext-real M2( REAL )
(cot x) + (tan x) is V11() real ext-real M2( REAL )
((cot x) + (tan x)) / 2 is V11() real ext-real M2( REAL )
(sec x) ^2 is V11() real ext-real M2( REAL )
(sec x) * (sec x) is V11() real ext-real set
((sec x) ^2) / (2 * (tan x)) is V11() real ext-real M2( REAL )
(sec x) * (sec x) is V11() real ext-real M2( REAL )
((sec x) * (sec x)) / (tan x) is V11() real ext-real M2( REAL )
(((sec x) * (sec x)) / (tan x)) / 2 is V11() real ext-real M2( REAL )
(sec x) / ((sin x) / (cos x)) is V11() real ext-real M2( REAL )
(sec x) * ((sec x) / ((sin x) / (cos x))) is V11() real ext-real M2( REAL )
((sec x) * ((sec x) / ((sin x) / (cos x)))) / 2 is V11() real ext-real M2( REAL )
(sec x) * (cos x) is V11() real ext-real M2( REAL )
((sec x) * (cos x)) / (sin x) is V11() real ext-real M2( REAL )
(sec x) * (((sec x) * (cos x)) / (sin x)) is V11() real ext-real M2( REAL )
((sec x) * (((sec x) * (cos x)) / (sin x))) / 2 is V11() real ext-real M2( REAL )
3 is V1() natural V11() real ext-real positive V33() V34() V45() V46() V47() V48() V49() V50() M3( REAL , NAT )
4 is V1() natural V11() real ext-real positive V33() V34() V45() V46() V47() V48() V49() V50() M3( REAL , NAT )
x is V11() real ext-real set
3 * x is V11() real ext-real M2( REAL )
sin (3 * x) is V11() real ext-real M2( REAL )
sin x is V11() real ext-real set
(sin x) |^ 3 is V11() real ext-real set
4 * ((sin x) |^ 3) is V11() real ext-real M2( REAL )
- (4 * ((sin x) |^ 3)) is V11() real ext-real M2( REAL )
3 * (sin x) is V11() real ext-real M2( REAL )
(- (4 * ((sin x) |^ 3))) + (3 * (sin x)) is V11() real ext-real M2( REAL )
x + x is V11() real ext-real set
(x + x) + x is V11() real ext-real set
sin ((x + x) + x) is V11() real ext-real set
2 * x is V11() real ext-real M2( REAL )
sin (2 * x) is V11() real ext-real M2( REAL )
cos x is V11() real ext-real set
(sin (2 * x)) * (cos x) is V11() real ext-real M2( REAL )
cos (x + x) is V11() real ext-real set
(cos (x + x)) * (sin x) is V11() real ext-real set
((sin (2 * x)) * (cos x)) + ((cos (x + x)) * (sin x)) is V11() real ext-real M2( REAL )
2 * (sin x) is V11() real ext-real M2( REAL )
(2 * (sin x)) * (cos x) is V11() real ext-real M2( REAL )
((2 * (sin x)) * (cos x)) * (cos x) is V11() real ext-real M2( REAL )
cos (2 * x) is V11() real ext-real M2( REAL )
(cos (2 * x)) * (sin x) is V11() real ext-real M2( REAL )
(((2 * (sin x)) * (cos x)) * (cos x)) + ((cos (2 * x)) * (sin x)) is V11() real ext-real M2( REAL )
(cos x) * (cos x) is V11() real ext-real set
(2 * (sin x)) * ((cos x) * (cos x)) is V11() real ext-real M2( REAL )
(sin x) ^2 is V11() real ext-real set
(sin x) * (sin x) is V11() real ext-real set
2 * ((sin x) ^2) is V11() real ext-real M2( REAL )
1 - (2 * ((sin x) ^2)) is V11() real ext-real M2( REAL )
(1 - (2 * ((sin x) ^2))) * (sin x) is V11() real ext-real M2( REAL )
((2 * (sin x)) * ((cos x) * (cos x))) + ((1 - (2 * ((sin x) ^2))) * (sin x)) is V11() real ext-real M2( REAL )
1 - ((sin x) ^2) is V11() real ext-real M2( REAL )
(2 * (sin x)) * (1 - ((sin x) ^2)) is V11() real ext-real M2( REAL )
((2 * (sin x)) * (1 - ((sin x) ^2))) + ((1 - (2 * ((sin x) ^2))) * (sin x)) is V11() real ext-real M2( REAL )
(2 * (sin x)) * 1 is V11() real ext-real M2( REAL )
(2 * (sin x)) * ((sin x) * (sin x)) is V11() real ext-real M2( REAL )
((2 * (sin x)) * 1) - ((2 * (sin x)) * ((sin x) * (sin x))) is V11() real ext-real M2( REAL )
1 * (sin x) is V11() real ext-real M2( REAL )
(2 * ((sin x) ^2)) * (sin x) is V11() real ext-real M2( REAL )
(1 * (sin x)) - ((2 * ((sin x) ^2)) * (sin x)) is V11() real ext-real M2( REAL )
(((2 * (sin x)) * 1) - ((2 * (sin x)) * ((sin x) * (sin x)))) + ((1 * (sin x)) - ((2 * ((sin x) ^2)) * (sin x))) is V11() real ext-real M2( REAL )
(sin x) |^ 1 is V11() real ext-real set
((sin x) |^ 1) * (sin x) is V11() real ext-real set
2 * (((sin x) |^ 1) * (sin x)) is V11() real ext-real M2( REAL )
(2 * (((sin x) |^ 1) * (sin x))) * (sin x) is V11() real ext-real M2( REAL )
((2 * (sin x)) * 1) - ((2 * (((sin x) |^ 1) * (sin x))) * (sin x)) is V11() real ext-real M2( REAL )
(((2 * (sin x)) * 1) - ((2 * (((sin x) |^ 1) * (sin x))) * (sin x))) + ((1 * (sin x)) - ((2 * ((sin x) ^2)) * (sin x))) is V11() real ext-real M2( REAL )
1 + 1 is natural V11() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() M3( REAL , NAT )
(sin x) |^ (1 + 1) is V11() real ext-real set
2 * ((sin x) |^ (1 + 1)) is V11() real ext-real M2( REAL )
(2 * ((sin x) |^ (1 + 1))) * (sin x) is V11() real ext-real M2( REAL )
((2 * (sin x)) * 1) - ((2 * ((sin x) |^ (1 + 1))) * (sin x)) is V11() real ext-real M2( REAL )
(((2 * (sin x)) * 1) - ((2 * ((sin x) |^ (1 + 1))) * (sin x))) + ((1 * (sin x)) - ((2 * ((sin x) ^2)) * (sin x))) is V11() real ext-real M2( REAL )
(sin x) |^ 2 is V11() real ext-real set
((sin x) |^ 2) * (sin x) is V11() real ext-real set
2 * (((sin x) |^ 2) * (sin x)) is V11() real ext-real M2( REAL )
((2 * (sin x)) * 1) - (2 * (((sin x) |^ 2) * (sin x))) is V11() real ext-real M2( REAL )
(((2 * (sin x)) * 1) - (2 * (((sin x) |^ 2) * (sin x)))) + ((1 * (sin x)) - ((2 * ((sin x) ^2)) * (sin x))) is V11() real ext-real M2( REAL )
2 + 1 is natural V11() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() M3( REAL , NAT )
(sin x) |^ (2 + 1) is V11() real ext-real set
2 * ((sin x) |^ (2 + 1)) is V11() real ext-real M2( REAL )
((2 * (sin x)) * 1) - (2 * ((sin x) |^ (2 + 1))) is V11() real ext-real M2( REAL )
(((2 * (sin x)) * 1) - (2 * ((sin x) |^ (2 + 1)))) + ((1 * (sin x)) - ((2 * ((sin x) ^2)) * (sin x))) is V11() real ext-real M2( REAL )
2 * ((sin x) |^ 3) is V11() real ext-real M2( REAL )
(2 * (sin x)) - (2 * ((sin x) |^ 3)) is V11() real ext-real M2( REAL )
(sin x) - ((2 * (((sin x) |^ 1) * (sin x))) * (sin x)) is V11() real ext-real M2( REAL )
((2 * (sin x)) - (2 * ((sin x) |^ 3))) + ((sin x) - ((2 * (((sin x) |^ 1) * (sin x))) * (sin x))) is V11() real ext-real M2( REAL )
(sin x) - ((2 * ((sin x) |^ (1 + 1))) * (sin x)) is V11() real ext-real M2( REAL )
((2 * (sin x)) - (2 * ((sin x) |^ 3))) + ((sin x) - ((2 * ((sin x) |^ (1 + 1))) * (sin x))) is V11() real ext-real M2( REAL )
((sin x) |^ (1 + 1)) * (sin x) is V11() real ext-real set
2 * (((sin x) |^ (1 + 1)) * (sin x)) is V11() real ext-real M2( REAL )
(sin x) - (2 * (((sin x) |^ (1 + 1)) * (sin x))) is V11() real ext-real M2( REAL )
((2 * (sin x)) - (2 * ((sin x) |^ 3))) + ((sin x) - (2 * (((sin x) |^ (1 + 1)) * (sin x)))) is V11() real ext-real M2( REAL )
(sin x) - (2 * ((sin x) |^ (2 + 1))) is V11() real ext-real M2( REAL )
((2 * (sin x)) - (2 * ((sin x) |^ 3))) + ((sin x) - (2 * ((sin x) |^ (2 + 1)))) is V11() real ext-real M2( REAL )
- (3 * (sin x)) is V11() real ext-real M2( REAL )
(- (3 * (sin x))) + (4 * ((sin x) |^ 3)) is V11() real ext-real M2( REAL )
- ((- (3 * (sin x))) + (4 * ((sin x) |^ 3))) is V11() real ext-real M2( REAL )
x is V11() real ext-real set
3 * x is V11() real ext-real M2( REAL )
cos (3 * x) is V11() real ext-real M2( REAL )
cos x is V11() real ext-real set
(cos x) |^ 3 is V11() real ext-real set
4 * ((cos x) |^ 3) is V11() real ext-real M2( REAL )
3 * (cos x) is V11() real ext-real M2( REAL )
(4 * ((cos x) |^ 3)) - (3 * (cos x)) is V11() real ext-real M2( REAL )
x + x is V11() real ext-real set
(x + x) + x is V11() real ext-real set
cos ((x + x) + x) is V11() real ext-real set
2 * x is V11() real ext-real M2( REAL )
cos (2 * x) is V11() real ext-real M2( REAL )
(cos (2 * x)) * (cos x) is V11() real ext-real M2( REAL )
sin (x + x) is V11() real ext-real set
sin x is V11() real ext-real set
(sin (x + x)) * (sin x) is V11() real ext-real set
((cos (2 * x)) * (cos x)) - ((sin (x + x)) * (sin x)) is V11() real ext-real M2( REAL )
(cos x) ^2 is V11() real ext-real set
(cos x) * (cos x) is V11() real ext-real set
2 * ((cos x) ^2) is V11() real ext-real M2( REAL )
(2 * ((cos x) ^2)) - 1 is V11() real ext-real M2( REAL )
((2 * ((cos x) ^2)) - 1) * (cos x) is V11() real ext-real M2( REAL )
sin (2 * x) is V11() real ext-real M2( REAL )
(sin (2 * x)) * (sin x) is V11() real ext-real M2( REAL )
(((2 * ((cos x) ^2)) - 1) * (cos x)) - ((sin (2 * x)) * (sin x)) is V11() real ext-real M2( REAL )
((cos x) * (cos x)) * (cos x) is V11() real ext-real set
2 * (((cos x) * (cos x)) * (cos x)) is V11() real ext-real M2( REAL )
1 * (cos x) is V11() real ext-real M2( REAL )
(2 * (((cos x) * (cos x)) * (cos x))) - (1 * (cos x)) is V11() real ext-real M2( REAL )
((2 * (((cos x) * (cos x)) * (cos x))) - (1 * (cos x))) - ((sin (2 * x)) * (sin x)) is V11() real ext-real M2( REAL )
(cos x) |^ 1 is V11() real ext-real set
((cos x) |^ 1) * (cos x) is V11() real ext-real set
(((cos x) |^ 1) * (cos x)) * (cos x) is V11() real ext-real set
2 * ((((cos x) |^ 1) * (cos x)) * (cos x)) is V11() real ext-real M2( REAL )
(2 * ((((cos x) |^ 1) * (cos x)) * (cos x))) - (1 * (cos x)) is V11() real ext-real M2( REAL )
((2 * ((((cos x) |^ 1) * (cos x)) * (cos x))) - (1 * (cos x))) - ((sin (2 * x)) * (sin x)) is V11() real ext-real M2( REAL )
1 + 1 is natural V11() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() M3( REAL , NAT )
(cos x) |^ (1 + 1) is V11() real ext-real set
((cos x) |^ (1 + 1)) * (cos x) is V11() real ext-real set
2 * (((cos x) |^ (1 + 1)) * (cos x)) is V11() real ext-real M2( REAL )
(2 * (((cos x) |^ (1 + 1)) * (cos x))) - (1 * (cos x)) is V11() real ext-real M2( REAL )
((2 * (((cos x) |^ (1 + 1)) * (cos x))) - (1 * (cos x))) - ((sin (2 * x)) * (sin x)) is V11() real ext-real M2( REAL )
2 + 1 is natural V11() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() M3( REAL , NAT )
(cos x) |^ (2 + 1) is V11() real ext-real set
2 * ((cos x) |^ (2 + 1)) is V11() real ext-real M2( REAL )
(2 * ((cos x) |^ (2 + 1))) - (cos x) is V11() real ext-real M2( REAL )
((2 * ((cos x) |^ (2 + 1))) - (cos x)) - ((sin (2 * x)) * (sin x)) is V11() real ext-real M2( REAL )
2 * ((cos x) |^ 3) is V11() real ext-real M2( REAL )
(2 * ((cos x) |^ 3)) - (cos x) is V11() real ext-real M2( REAL )
2 * (sin x) is V11() real ext-real M2( REAL )
(2 * (sin x)) * (cos x) is V11() real ext-real M2( REAL )
((2 * (sin x)) * (cos x)) * (sin x) is V11() real ext-real M2( REAL )
((2 * ((cos x) |^ 3)) - (cos x)) - (((2 * (sin x)) * (cos x)) * (sin x)) is V11() real ext-real M2( REAL )
2 * (cos x) is V11() real ext-real M2( REAL )
(sin x) * (sin x) is V11() real ext-real set
(2 * (cos x)) * ((sin x) * (sin x)) is V11() real ext-real M2( REAL )
((2 * ((cos x) |^ 3)) - (cos x)) - ((2 * (cos x)) * ((sin x) * (sin x))) is V11() real ext-real M2( REAL )
1 - ((cos x) * (cos x)) is V11() real ext-real M2( REAL )
(2 * (cos x)) * (1 - ((cos x) * (cos x))) is V11() real ext-real M2( REAL )
((2 * ((cos x) |^ 3)) - (cos x)) - ((2 * (cos x)) * (1 - ((cos x) * (cos x)))) is V11() real ext-real M2( REAL )
(2 * (cos x)) - (2 * (((cos x) * (cos x)) * (cos x))) is V11() real ext-real M2( REAL )
((2 * ((cos x) |^ 3)) - (cos x)) - ((2 * (cos x)) - (2 * (((cos x) * (cos x)) * (cos x)))) is V11() real ext-real M2( REAL )
(2 * (cos x)) - (2 * ((((cos x) |^ 1) * (cos x)) * (cos x))) is V11() real ext-real M2( REAL )
((2 * ((cos x) |^ 3)) - (cos x)) - ((2 * (cos x)) - (2 * ((((cos x) |^ 1) * (cos x)) * (cos x)))) is V11() real ext-real M2( REAL )
(2 * (cos x)) - (2 * (((cos x) |^ (1 + 1)) * (cos x))) is V11() real ext-real M2( REAL )
((2 * ((cos x) |^ 3)) - (cos x)) - ((2 * (cos x)) - (2 * (((cos x) |^ (1 + 1)) * (cos x)))) is V11() real ext-real M2( REAL )
(2 * (cos x)) - (2 * ((cos x) |^ (2 + 1))) is V11() real ext-real M2( REAL )
((2 * ((cos x) |^ 3)) - (cos x)) - ((2 * (cos x)) - (2 * ((cos x) |^ (2 + 1)))) is V11() real ext-real M2( REAL )
(2 * ((cos x) |^ 3)) + (2 * ((cos x) |^ 3)) is V11() real ext-real M2( REAL )
((2 * ((cos x) |^ 3)) + (2 * ((cos x) |^ 3))) - (3 * (cos x)) is V11() real ext-real M2( REAL )
x is V11() real ext-real set
cos x is V11() real ext-real set
3 * x is V11() real ext-real M2( REAL )
tan (3 * x) is V11() real ext-real M2( REAL )
sin (3 * x) is V11() real ext-real set
cos (3 * x) is V11() real ext-real set
(sin (3 * x)) / (cos (3 * x)) is V11() real ext-real set
tan x is V11() real ext-real M2( REAL )
sin x is V11() real ext-real set
(sin x) / (cos x) is V11() real ext-real set
3 * (tan x) is V11() real ext-real M2( REAL )
(tan x) |^ 3 is V11() real ext-real M2( REAL )
(3 * (tan x)) - ((tan x) |^ 3) is V11() real ext-real M2( REAL )
(tan x) ^2 is V11() real ext-real M2( REAL )
(tan x) * (tan x) is V11() real ext-real set
3 * ((tan x) ^2) is V11() real ext-real M2( REAL )
1 - (3 * ((tan x) ^2)) is V11() real ext-real M2( REAL )
((3 * (tan x)) - ((tan x) |^ 3)) / (1 - (3 * ((tan x) ^2))) is V11() real ext-real M2( REAL )
x + x is V11() real ext-real set
(x + x) + x is V11() real ext-real set
tan ((x + x) + x) is V11() real ext-real M2( REAL )
sin ((x + x) + x) is V11() real ext-real set
cos ((x + x) + x) is V11() real ext-real set
(sin ((x + x) + x)) / (cos ((x + x) + x)) is V11() real ext-real set
(tan x) + (tan x) is V11() real ext-real M2( REAL )
((tan x) + (tan x)) + (tan x) is V11() real ext-real M2( REAL )
(tan x) * (tan x) is V11() real ext-real M2( REAL )
((tan x) * (tan x)) * (tan x) is V11() real ext-real M2( REAL )
(((tan x) + (tan x)) + (tan x)) - (((tan x) * (tan x)) * (tan x)) is V11() real ext-real M2( REAL )
1 - ((tan x) * (tan x)) is V11() real ext-real M2( REAL )
(1 - ((tan x) * (tan x))) - ((tan x) * (tan x)) is V11() real ext-real M2( REAL )
((1 - ((tan x) * (tan x))) - ((tan x) * (tan x))) - ((tan x) * (tan x)) is V11() real ext-real M2( REAL )
((((tan x) + (tan x)) + (tan x)) - (((tan x) * (tan x)) * (tan x))) / (((1 - ((tan x) * (tan x))) - ((tan x) * (tan x))) - ((tan x) * (tan x))) is V11() real ext-real M2( REAL )
(tan x) |^ 1 is V11() real ext-real M2( REAL )
((tan x) |^ 1) * (tan x) is V11() real ext-real M2( REAL )
(((tan x) |^ 1) * (tan x)) * (tan x) is V11() real ext-real M2( REAL )
(3 * (tan x)) - ((((tan x) |^ 1) * (tan x)) * (tan x)) is V11() real ext-real M2( REAL )
(3 * (tan x)) * (tan x) is V11() real ext-real M2( REAL )
1 - ((3 * (tan x)) * (tan x)) is V11() real ext-real M2( REAL )
((3 * (tan x)) - ((((tan x) |^ 1) * (tan x)) * (tan x))) / (1 - ((3 * (tan x)) * (tan x))) is V11() real ext-real M2( REAL )
1 + 1 is natural V11() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() M3( REAL , NAT )
(tan x) |^ (1 + 1) is V11() real ext-real M2( REAL )
((tan x) |^ (1 + 1)) * (tan x) is V11() real ext-real M2( REAL )
(3 * (tan x)) - (((tan x) |^ (1 + 1)) * (tan x)) is V11() real ext-real M2( REAL )
((3 * (tan x)) - (((tan x) |^ (1 + 1)) * (tan x))) / (1 - ((3 * (tan x)) * (tan x))) is V11() real ext-real M2( REAL )
2 + 1 is natural V11() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() M3( REAL , NAT )
(tan x) |^ (2 + 1) is V11() real ext-real M2( REAL )
(3 * (tan x)) - ((tan x) |^ (2 + 1)) is V11() real ext-real M2( REAL )
3 * ((tan x) * (tan x)) is V11() real ext-real M2( REAL )
1 - (3 * ((tan x) * (tan x))) is V11() real ext-real M2( REAL )
((3 * (tan x)) - ((tan x) |^ (2 + 1))) / (1 - (3 * ((tan x) * (tan x)))) is V11() real ext-real M2( REAL )
x is V11() real ext-real set
sin x is V11() real ext-real set
3 * x is V11() real ext-real M2( REAL )
cot (3 * x) is V11() real ext-real M2( REAL )
cos (3 * x) is V11() real ext-real set
sin (3 * x) is V11() real ext-real set
(cos (3 * x)) / (sin (3 * x)) is V11() real ext-real set
cot x is V11() real ext-real M2( REAL )
cos x is V11() real ext-real set
(cos x) / (sin x) is V11() real ext-real set
(cot x) |^ 3 is V11() real ext-real M2( REAL )
3 * (cot x) is V11() real ext-real M2( REAL )
((cot x) |^ 3) - (3 * (cot x)) is V11() real ext-real M2( REAL )
(cot x) ^2 is V11() real ext-real M2( REAL )
(cot x) * (cot x) is V11() real ext-real set
3 * ((cot x) ^2) is V11() real ext-real M2( REAL )
(3 * ((cot x) ^2)) - 1 is V11() real ext-real M2( REAL )
(((cot x) |^ 3) - (3 * (cot x))) / ((3 * ((cot x) ^2)) - 1) is V11() real ext-real M2( REAL )
x + x is V11() real ext-real set
(x + x) + x is V11() real ext-real set
cot ((x + x) + x) is V11() real ext-real M2( REAL )
cos ((x + x) + x) is V11() real ext-real set
sin ((x + x) + x) is V11() real ext-real set
(cos ((x + x) + x)) / (sin ((x + x) + x)) is V11() real ext-real set
(cot x) * (cot x) is V11() real ext-real M2( REAL )
((cot x) * (cot x)) * (cot x) is V11() real ext-real M2( REAL )
(((cot x) * (cot x)) * (cot x)) - (cot x) is V11() real ext-real M2( REAL )
((((cot x) * (cot x)) * (cot x)) - (cot x)) - (cot x) is V11() real ext-real M2( REAL )
(((((cot x) * (cot x)) * (cot x)) - (cot x)) - (cot x)) - (cot x) is V11() real ext-real M2( REAL )
((cot x) * (cot x)) + ((cot x) * (cot x)) is V11() real ext-real M2( REAL )
(((cot x) * (cot x)) + ((cot x) * (cot x))) + ((cot x) * (cot x)) is V11() real ext-real M2( REAL )
((((cot x) * (cot x)) + ((cot x) * (cot x))) + ((cot x) * (cot x))) - 1 is V11() real ext-real M2( REAL )
((((((cot x) * (cot x)) * (cot x)) - (cot x)) - (cot x)) - (cot x)) / (((((cot x) * (cot x)) + ((cot x) * (cot x))) + ((cot x) * (cot x))) - 1) is V11() real ext-real M2( REAL )
(((cot x) * (cot x)) * (cot x)) - (3 * (cot x)) is V11() real ext-real M2( REAL )
((((cot x) * (cot x)) * (cot x)) - (3 * (cot x))) / ((3 * ((cot x) ^2)) - 1) is V11() real ext-real M2( REAL )
(cot x) |^ 1 is V11() real ext-real M2( REAL )
((cot x) |^ 1) * (cot x) is V11() real ext-real M2( REAL )
(((cot x) |^ 1) * (cot x)) * (cot x) is V11() real ext-real M2( REAL )
((((cot x) |^ 1) * (cot x)) * (cot x)) - (3 * (cot x)) is V11() real ext-real M2( REAL )
(((((cot x) |^ 1) * (cot x)) * (cot x)) - (3 * (cot x))) / ((3 * ((cot x) ^2)) - 1) is V11() real ext-real M2( REAL )
1 + 1 is natural V11() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() M3( REAL , NAT )
(cot x) |^ (1 + 1) is V11() real ext-real M2( REAL )
((cot x) |^ (1 + 1)) * (cot x) is V11() real ext-real M2( REAL )
(((cot x) |^ (1 + 1)) * (cot x)) - (3 * (cot x)) is V11() real ext-real M2( REAL )
((((cot x) |^ (1 + 1)) * (cot x)) - (3 * (cot x))) / ((3 * ((cot x) ^2)) - 1) is V11() real ext-real M2( REAL )
2 + 1 is natural V11() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() M3( REAL , NAT )
(cot x) |^ (2 + 1) is V11() real ext-real M2( REAL )
((cot x) |^ (2 + 1)) - (3 * (cot x)) is V11() real ext-real M2( REAL )
(((cot x) |^ (2 + 1)) - (3 * (cot x))) / ((3 * ((cot x) ^2)) - 1) is V11() real ext-real M2( REAL )
x is V11() real ext-real set
sin x is V11() real ext-real set
(sin x) ^2 is V11() real ext-real set
(sin x) * (sin x) is V11() real ext-real set
2 * x is V11() real ext-real M2( REAL )
cos (2 * x) is V11() real ext-real M2( REAL )
1 - (cos (2 * x)) is V11() real ext-real M2( REAL )
(1 - (cos (2 * x))) / 2 is V11() real ext-real M2( REAL )
2 * ((sin x) ^2) is V11() real ext-real M2( REAL )
1 - (2 * ((sin x) ^2)) is V11() real ext-real M2( REAL )
1 - (1 - (2 * ((sin x) ^2))) is V11() real ext-real M2( REAL )
(1 - (1 - (2 * ((sin x) ^2)))) / 2 is V11() real ext-real M2( REAL )
((sin x) ^2) * 2 is V11() real ext-real M2( REAL )
(((sin x) ^2) * 2) / 2 is V11() real ext-real M2( REAL )
x is V11() real ext-real set
cos x is V11() real ext-real set
(cos x) ^2 is V11() real ext-real set
(cos x) * (cos x) is V11() real ext-real set
2 * x is V11() real ext-real M2( REAL )
cos (2 * x) is V11() real ext-real M2( REAL )
1 + (cos (2 * x)) is V11() real ext-real M2( REAL )
(1 + (cos (2 * x))) / 2 is V11() real ext-real M2( REAL )
2 * ((cos x) ^2) is V11() real ext-real M2( REAL )
(2 * ((cos x) ^2)) - 1 is V11() real ext-real M2( REAL )
1 + ((2 * ((cos x) ^2)) - 1) is V11() real ext-real M2( REAL )
(1 + ((2 * ((cos x) ^2)) - 1)) / 2 is V11() real ext-real M2( REAL )
((cos x) ^2) * 2 is V11() real ext-real M2( REAL )
(((cos x) ^2) * 2) / 2 is V11() real ext-real M2( REAL )
x is V11() real ext-real set
sin x is V11() real ext-real set
(sin x) |^ 3 is V11() real ext-real set
3 * (sin x) is V11() real ext-real M2( REAL )
3 * x is V11() real ext-real M2( REAL )
sin (3 * x) is V11() real ext-real M2( REAL )
(3 * (sin x)) - (sin (3 * x)) is V11() real ext-real M2( REAL )
((3 * (sin x)) - (sin (3 * x))) / 4 is V11() real ext-real M2( REAL )
4 * ((sin x) |^ 3) is V11() real ext-real M2( REAL )
- (4 * ((sin x) |^ 3)) is V11() real ext-real M2( REAL )
(- (4 * ((sin x) |^ 3))) + (3 * (sin x)) is V11() real ext-real M2( REAL )
(3 * (sin x)) - ((- (4 * ((sin x) |^ 3))) + (3 * (sin x))) is V11() real ext-real M2( REAL )
((3 * (sin x)) - ((- (4 * ((sin x) |^ 3))) + (3 * (sin x)))) / 4 is V11() real ext-real M2( REAL )
(4 * ((sin x) |^ 3)) / 4 is V11() real ext-real M2( REAL )
x is V11() real ext-real set
cos x is V11() real ext-real set
(cos x) |^ 3 is V11() real ext-real set
3 * (cos x) is V11() real ext-real M2( REAL )
3 * x is V11() real ext-real M2( REAL )
cos (3 * x) is V11() real ext-real M2( REAL )
(3 * (cos x)) + (cos (3 * x)) is V11() real ext-real M2( REAL )
((3 * (cos x)) + (cos (3 * x))) / 4 is V11() real ext-real M2( REAL )
4 * ((cos x) |^ 3) is V11() real ext-real M2( REAL )
(4 * ((cos x) |^ 3)) - (3 * (cos x)) is V11() real ext-real M2( REAL )
(3 * (cos x)) + ((4 * ((cos x) |^ 3)) - (3 * (cos x))) is V11() real ext-real M2( REAL )
((3 * (cos x)) + ((4 * ((cos x) |^ 3)) - (3 * (cos x)))) / 4 is V11() real ext-real M2( REAL )
(4 * ((cos x) |^ 3)) / 4 is V11() real ext-real M2( REAL )
8 is V1() natural V11() real ext-real positive V33() V34() V45() V46() V47() V48() V49() V50() M3( REAL , NAT )
x is V11() real ext-real set
sin x is V11() real ext-real set
(sin x) |^ 4 is V11() real ext-real set
2 * x is V11() real ext-real M2( REAL )
cos (2 * x) is V11() real ext-real M2( REAL )
4 * (cos (2 * x)) is V11() real ext-real M2( REAL )
3 - (4 * (cos (2 * x))) is V11() real ext-real M2( REAL )
4 * x is V11() real ext-real M2( REAL )
cos (4 * x) is V11() real ext-real M2( REAL )
(3 - (4 * (cos (2 * x)))) + (cos (4 * x)) is V11() real ext-real M2( REAL )
((3 - (4 * (cos (2 * x)))) + (cos (4 * x))) / 8 is V11() real ext-real M2( REAL )
2 * 2 is natural V11() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() M3( REAL , NAT )
(2 * 2) * x is V11() real ext-real M2( REAL )
cos ((2 * 2) * x) is V11() real ext-real M2( REAL )
(3 - (4 * (cos (2 * x)))) + (cos ((2 * 2) * x)) is V11() real ext-real M2( REAL )
((3 - (4 * (cos (2 * x)))) + (cos ((2 * 2) * x))) / 8 is V11() real ext-real M2( REAL )
2 * (2 * x) is V11() real ext-real M2( REAL )
cos (2 * (2 * x)) is V11() real ext-real M2( REAL )
(3 - (4 * (cos (2 * x)))) + (cos (2 * (2 * x))) is V11() real ext-real M2( REAL )
((3 - (4 * (cos (2 * x)))) + (cos (2 * (2 * x)))) / 8 is V11() real ext-real M2( REAL )
sin (2 * x) is V11() real ext-real M2( REAL )
(sin (2 * x)) ^2 is V11() real ext-real M2( REAL )
(sin (2 * x)) * (sin (2 * x)) is V11() real ext-real set
2 * ((sin (2 * x)) ^2) is V11() real ext-real M2( REAL )
1 - (2 * ((sin (2 * x)) ^2)) is V11() real ext-real M2( REAL )
(3 - (4 * (cos (2 * x)))) + (1 - (2 * ((sin (2 * x)) ^2))) is V11() real ext-real M2( REAL )
((3 - (4 * (cos (2 * x)))) + (1 - (2 * ((sin (2 * x)) ^2)))) / 8 is V11() real ext-real M2( REAL )
2 * (sin x) is V11() real ext-real M2( REAL )
cos x is V11() real ext-real set
(2 * (sin x)) * (cos x) is V11() real ext-real M2( REAL )
((2 * (sin x)) * (cos x)) ^2 is V11() real ext-real M2( REAL )
((2 * (sin x)) * (cos x)) * ((2 * (sin x)) * (cos x)) is V11() real ext-real set
2 * (((2 * (sin x)) * (cos x)) ^2) is V11() real ext-real M2( REAL )
1 - (2 * (((2 * (sin x)) * (cos x)) ^2)) is V11() real ext-real M2( REAL )
(3 - (4 * (cos (2 * x)))) + (1 - (2 * (((2 * (sin x)) * (cos x)) ^2))) is V11() real ext-real M2( REAL )
((3 - (4 * (cos (2 * x)))) + (1 - (2 * (((2 * (sin x)) * (cos x)) ^2)))) / 8 is V11() real ext-real M2( REAL )
(sin x) ^2 is V11() real ext-real set
(sin x) * (sin x) is V11() real ext-real set
2 * ((sin x) ^2) is V11() real ext-real M2( REAL )
1 - (2 * ((sin x) ^2)) is V11() real ext-real M2( REAL )
4 * (1 - (2 * ((sin x) ^2))) is V11() real ext-real M2( REAL )
3 - (4 * (1 - (2 * ((sin x) ^2)))) is V11() real ext-real M2( REAL )
8 * ((sin x) ^2) is V11() real ext-real M2( REAL )
(cos x) ^2 is V11() real ext-real set
(cos x) * (cos x) is V11() real ext-real set
(8 * ((sin x) ^2)) * ((cos x) ^2) is V11() real ext-real M2( REAL )
1 - ((8 * ((sin x) ^2)) * ((cos x) ^2)) is V11() real ext-real M2( REAL )
(3 - (4 * (1 - (2 * ((sin x) ^2))))) + (1 - ((8 * ((sin x) ^2)) * ((cos x) ^2))) is V11() real ext-real M2( REAL )
((3 - (4 * (1 - (2 * ((sin x) ^2))))) + (1 - ((8 * ((sin x) ^2)) * ((cos x) ^2)))) / 8 is V11() real ext-real M2( REAL )
1 - ((cos x) * (cos x)) is V11() real ext-real M2( REAL )
((sin x) ^2) * (1 - ((cos x) * (cos x))) is V11() real ext-real M2( REAL )
((sin x) * (sin x)) * ((sin x) * (sin x)) is V11() real ext-real set
(sin x) |^ 1 is V11() real ext-real set
((sin x) |^ 1) * (sin x) is V11() real ext-real set
(((sin x) |^ 1) * (sin x)) * ((sin x) * (sin x)) is V11() real ext-real set
1 + 1 is natural V11() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() M3( REAL , NAT )
(sin x) |^ (1 + 1) is V11() real ext-real set
((sin x) |^ (1 + 1)) * ((sin x) * (sin x)) is V11() real ext-real set
((sin x) |^ (1 + 1)) * (sin x) is V11() real ext-real set
(((sin x) |^ (1 + 1)) * (sin x)) * (sin x) is V11() real ext-real set
2 + 1 is natural V11() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() M3( REAL , NAT )
(sin x) |^ (2 + 1) is V11() real ext-real set
((sin x) |^ (2 + 1)) * (sin x) is V11() real ext-real set
3 + 1 is natural V11() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() M3( REAL , NAT )
(sin x) |^ (3 + 1) is V11() real ext-real set
x is V11() real ext-real set
cos x is V11() real ext-real set
(cos x) |^ 4 is V11() real ext-real set
2 * x is V11() real ext-real M2( REAL )
cos (2 * x) is V11() real ext-real M2( REAL )
4 * (cos (2 * x)) is V11() real ext-real M2( REAL )
3 + (4 * (cos (2 * x))) is V11() real ext-real M2( REAL )
4 * x is V11() real ext-real M2( REAL )
cos (4 * x) is V11() real ext-real M2( REAL )
(3 + (4 * (cos (2 * x)))) + (cos (4 * x)) is V11() real ext-real M2( REAL )
((3 + (4 * (cos (2 * x)))) + (cos (4 * x))) / 8 is V11() real ext-real M2( REAL )
2 * (2 * x) is V11() real ext-real M2( REAL )
cos (2 * (2 * x)) is V11() real ext-real M2( REAL )
(3 + (4 * (cos (2 * x)))) + (cos (2 * (2 * x))) is V11() real ext-real M2( REAL )
((3 + (4 * (cos (2 * x)))) + (cos (2 * (2 * x)))) / 8 is V11() real ext-real M2( REAL )
sin (2 * x) is V11() real ext-real M2( REAL )
(sin (2 * x)) ^2 is V11() real ext-real M2( REAL )
(sin (2 * x)) * (sin (2 * x)) is V11() real ext-real set
2 * ((sin (2 * x)) ^2) is V11() real ext-real M2( REAL )
1 - (2 * ((sin (2 * x)) ^2)) is V11() real ext-real M2( REAL )
(3 + (4 * (cos (2 * x)))) + (1 - (2 * ((sin (2 * x)) ^2))) is V11() real ext-real M2( REAL )
((3 + (4 * (cos (2 * x)))) + (1 - (2 * ((sin (2 * x)) ^2)))) / 8 is V11() real ext-real M2( REAL )
sin x is V11() real ext-real set
2 * (sin x) is V11() real ext-real M2( REAL )
(2 * (sin x)) * (cos x) is V11() real ext-real M2( REAL )
((2 * (sin x)) * (cos x)) ^2 is V11() real ext-real M2( REAL )
((2 * (sin x)) * (cos x)) * ((2 * (sin x)) * (cos x)) is V11() real ext-real set
2 * (((2 * (sin x)) * (cos x)) ^2) is V11() real ext-real M2( REAL )
1 - (2 * (((2 * (sin x)) * (cos x)) ^2)) is V11() real ext-real M2( REAL )
(3 + (4 * (cos (2 * x)))) + (1 - (2 * (((2 * (sin x)) * (cos x)) ^2))) is V11() real ext-real M2( REAL )
((3 + (4 * (cos (2 * x)))) + (1 - (2 * (((2 * (sin x)) * (cos x)) ^2)))) / 8 is V11() real ext-real M2( REAL )
(sin x) ^2 is V11() real ext-real set
(sin x) * (sin x) is V11() real ext-real set
2 * ((sin x) ^2) is V11() real ext-real M2( REAL )
1 - (2 * ((sin x) ^2)) is V11() real ext-real M2( REAL )
4 * (1 - (2 * ((sin x) ^2))) is V11() real ext-real M2( REAL )
3 + (4 * (1 - (2 * ((sin x) ^2)))) is V11() real ext-real M2( REAL )
8 * ((sin x) ^2) is V11() real ext-real M2( REAL )
(cos x) ^2 is V11() real ext-real set
(cos x) * (cos x) is V11() real ext-real set
(8 * ((sin x) ^2)) * ((cos x) ^2) is V11() real ext-real M2( REAL )
1 - ((8 * ((sin x) ^2)) * ((cos x) ^2)) is V11() real ext-real M2( REAL )
(3 + (4 * (1 - (2 * ((sin x) ^2))))) + (1 - ((8 * ((sin x) ^2)) * ((cos x) ^2))) is V11() real ext-real M2( REAL )
((3 + (4 * (1 - (2 * ((sin x) ^2))))) + (1 - ((8 * ((sin x) ^2)) * ((cos x) ^2)))) / 8 is V11() real ext-real M2( REAL )
1 + ((cos x) ^2) is V11() real ext-real M2( REAL )
((sin x) * (sin x)) * (1 + ((cos x) ^2)) is V11() real ext-real M2( REAL )
1 - (((sin x) * (sin x)) * (1 + ((cos x) ^2))) is V11() real ext-real M2( REAL )
1 ^2 is V11() real ext-real M2( REAL )
1 * 1 is V11() real ext-real set
(1 ^2) - ((cos x) ^2) is V11() real ext-real M2( REAL )
(1 ^2) + ((cos x) ^2) is V11() real ext-real M2( REAL )
((1 ^2) - ((cos x) ^2)) * ((1 ^2) + ((cos x) ^2)) is V11() real ext-real M2( REAL )
1 - (((1 ^2) - ((cos x) ^2)) * ((1 ^2) + ((cos x) ^2))) is V11() real ext-real M2( REAL )
((cos x) * (cos x)) * (cos x) is V11() real ext-real set
(((cos x) * (cos x)) * (cos x)) * (cos x) is V11() real ext-real set
(cos x) |^ 1 is V11() real ext-real set
((cos x) |^ 1) * (cos x) is V11() real ext-real set
(((cos x) |^ 1) * (cos x)) * (cos x) is V11() real ext-real set
((((cos x) |^ 1) * (cos x)) * (cos x)) * (cos x) is V11() real ext-real set
1 + 1 is natural V11() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() M3( REAL , NAT )
(cos x) |^ (1 + 1) is V11() real ext-real set
((cos x) |^ (1 + 1)) * (cos x) is V11() real ext-real set
(((cos x) |^ (1 + 1)) * (cos x)) * (cos x) is V11() real ext-real set
2 + 1 is natural V11() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() M3( REAL , NAT )
(cos x) |^ (2 + 1) is V11() real ext-real set
((cos x) |^ (2 + 1)) * (cos x) is V11() real ext-real set
3 + 1 is natural V11() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() M3( REAL , NAT )
(cos x) |^ (3 + 1) is V11() real ext-real set
x is V11() real ext-real set
x / 2 is V11() real ext-real M2( REAL )
sin (x / 2) is V11() real ext-real M2( REAL )
cos x is V11() real ext-real set
1 - (cos x) is V11() real ext-real M2( REAL )
(1 - (cos x)) / 2 is V11() real ext-real M2( REAL )
sqrt ((1 - (cos x)) / 2) is V11() real ext-real M2( REAL )
- (sqrt ((1 - (cos x)) / 2)) is V11() real ext-real M2( REAL )
2 * (x / 2) is V11() real ext-real M2( REAL )
cos (2 * (x / 2)) is V11() real ext-real M2( REAL )
1 - (cos (2 * (x / 2))) is V11() real ext-real M2( REAL )
(1 - (cos (2 * (x / 2)))) / 2 is V11() real ext-real M2( REAL )
sqrt ((1 - (cos (2 * (x / 2)))) / 2) is V11() real ext-real M2( REAL )
(sin (x / 2)) ^2 is V11() real ext-real M2( REAL )
(sin (x / 2)) * (sin (x / 2)) is V11() real ext-real set
2 * ((sin (x / 2)) ^2) is V11() real ext-real M2( REAL )
1 - (2 * ((sin (x / 2)) ^2)) is V11() real ext-real M2( REAL )
1 - (1 - (2 * ((sin (x / 2)) ^2))) is V11() real ext-real M2( REAL )
(1 - (1 - (2 * ((sin (x / 2)) ^2)))) / 2 is V11() real ext-real M2( REAL )
sqrt ((1 - (1 - (2 * ((sin (x / 2)) ^2)))) / 2) is V11() real ext-real M2( REAL )
abs (sin (x / 2)) is V11() real ext-real M2( REAL )
- 1 is V11() real ext-real M2( REAL )
(sqrt ((1 - (cos x)) / 2)) * (- 1) is V11() real ext-real M2( REAL )
- (sin (x / 2)) is V11() real ext-real M2( REAL )
(- (sin (x / 2))) * (- 1) is V11() real ext-real M2( REAL )
x is V11() real ext-real set
x / 2 is V11() real ext-real M2( REAL )
cos (x / 2) is V11() real ext-real M2( REAL )
cos x is V11() real ext-real set
1 + (cos x) is V11() real ext-real M2( REAL )
(1 + (cos x)) / 2 is V11() real ext-real M2( REAL )
sqrt ((1 + (cos x)) / 2) is V11() real ext-real M2( REAL )
- (sqrt ((1 + (cos x)) / 2)) is V11() real ext-real M2( REAL )
2 * (x / 2) is V11() real ext-real M2( REAL )
cos (2 * (x / 2)) is V11() real ext-real M2( REAL )
1 + (cos (2 * (x / 2))) is V11() real ext-real M2( REAL )
(1 + (cos (2 * (x / 2)))) / 2 is V11() real ext-real M2( REAL )
sqrt ((1 + (cos (2 * (x / 2)))) / 2) is V11() real ext-real M2( REAL )
(cos (x / 2)) ^2 is V11() real ext-real M2( REAL )
(cos (x / 2)) * (cos (x / 2)) is V11() real ext-real set
2 * ((cos (x / 2)) ^2) is V11() real ext-real M2( REAL )
(2 * ((cos (x / 2)) ^2)) - 1 is V11() real ext-real M2( REAL )
1 + ((2 * ((cos (x / 2)) ^2)) - 1) is V11() real ext-real M2( REAL )
(1 + ((2 * ((cos (x / 2)) ^2)) - 1)) / 2 is V11() real ext-real M2( REAL )
sqrt ((1 + ((2 * ((cos (x / 2)) ^2)) - 1)) / 2) is V11() real ext-real M2( REAL )
abs (cos (x / 2)) is V11() real ext-real M2( REAL )
- 1 is V11() real ext-real M2( REAL )
(sqrt ((1 + (cos x)) / 2)) * (- 1) is V11() real ext-real M2( REAL )
- (cos (x / 2)) is V11() real ext-real M2( REAL )
(- (cos (x / 2))) * (- 1) is V11() real ext-real M2( REAL )
x is V11() real ext-real set
x / 2 is V11() real ext-real M2( REAL )
sin (x / 2) is V11() real ext-real M2( REAL )
tan (x / 2) is V11() real ext-real M2( REAL )
sin (x / 2) is V11() real ext-real set
cos (x / 2) is V11() real ext-real set
(sin (x / 2)) / (cos (x / 2)) is V11() real ext-real set
cos x is V11() real ext-real set
1 - (cos x) is V11() real ext-real M2( REAL )
sin x is V11() real ext-real set
(1 - (cos x)) / (sin x) is V11() real ext-real M2( REAL )
2 * (sin (x / 2)) is V11() real ext-real M2( REAL )
(sin (x / 2)) ^2 is V11() real ext-real M2( REAL )
(sin (x / 2)) * (sin (x / 2)) is V11() real ext-real set
2 * ((sin (x / 2)) ^2) is V11() real ext-real M2( REAL )
1 - (2 * ((sin (x / 2)) ^2)) is V11() real ext-real M2( REAL )
1 - (1 - (2 * ((sin (x / 2)) ^2))) is V11() real ext-real M2( REAL )
2 * (x / 2) is V11() real ext-real M2( REAL )
sin (2 * (x / 2)) is V11() real ext-real M2( REAL )
(1 - (1 - (2 * ((sin (x / 2)) ^2)))) / (sin (2 * (x / 2))) is V11() real ext-real M2( REAL )
(2 * (sin (x / 2))) * (sin (x / 2)) is V11() real ext-real M2( REAL )
cos (x / 2) is V11() real ext-real M2( REAL )
(2 * (sin (x / 2))) * (cos (x / 2)) is V11() real ext-real M2( REAL )
((2 * (sin (x / 2))) * (sin (x / 2))) / ((2 * (sin (x / 2))) * (cos (x / 2))) is V11() real ext-real M2( REAL )
x is V11() real ext-real set
x / 2 is V11() real ext-real M2( REAL )
cos (x / 2) is V11() real ext-real M2( REAL )
tan (x / 2) is V11() real ext-real M2( REAL )
sin (x / 2) is V11() real ext-real set
cos (x / 2) is V11() real ext-real set
(sin (x / 2)) / (cos (x / 2)) is V11() real ext-real set
sin x is V11() real ext-real set
cos x is V11() real ext-real set
1 + (cos x) is V11() real ext-real M2( REAL )
(sin x) / (1 + (cos x)) is V11() real ext-real M2( REAL )
2 * (cos (x / 2)) is V11() real ext-real M2( REAL )
sin (x / 2) is V11() real ext-real M2( REAL )
2 * (sin (x / 2)) is V11() real ext-real M2( REAL )
(2 * (sin (x / 2))) * (cos (x / 2)) is V11() real ext-real M2( REAL )
2 * (x / 2) is V11() real ext-real M2( REAL )
cos (2 * (x / 2)) is V11() real ext-real M2( REAL )
1 + (cos (2 * (x / 2))) is V11() real ext-real M2( REAL )
((2 * (sin (x / 2))) * (cos (x / 2))) / (1 + (cos (2 * (x / 2)))) is V11() real ext-real M2( REAL )
(cos (x / 2)) ^2 is V11() real ext-real M2( REAL )
(cos (x / 2)) * (cos (x / 2)) is V11() real ext-real set
2 * ((cos (x / 2)) ^2) is V11() real ext-real M2( REAL )
(2 * ((cos (x / 2)) ^2)) - 1 is V11() real ext-real M2( REAL )
1 + ((2 * ((cos (x / 2)) ^2)) - 1) is V11() real ext-real M2( REAL )
((2 * (sin (x / 2))) * (cos (x / 2))) / (1 + ((2 * ((cos (x / 2)) ^2)) - 1)) is V11() real ext-real M2( REAL )
(2 * (cos (x / 2))) * (sin (x / 2)) is V11() real ext-real M2( REAL )
(2 * (cos (x / 2))) * (cos (x / 2)) is V11() real ext-real M2( REAL )
((2 * (cos (x / 2))) * (sin (x / 2))) / ((2 * (cos (x / 2))) * (cos (x / 2))) is V11() real ext-real M2( REAL )
(sin (x / 2)) / (cos (x / 2)) is V11() real ext-real M2( REAL )
x is V11() real ext-real set
x / 2 is V11() real ext-real M2( REAL )
tan (x / 2) is V11() real ext-real M2( REAL )
sin (x / 2) is V11() real ext-real set
cos (x / 2) is V11() real ext-real set
(sin (x / 2)) / (cos (x / 2)) is V11() real ext-real set
cos x is V11() real ext-real set
1 - (cos x) is V11() real ext-real M2( REAL )
1 + (cos x) is V11() real ext-real M2( REAL )
(1 - (cos x)) / (1 + (cos x)) is V11() real ext-real M2( REAL )
sqrt ((1 - (cos x)) / (1 + (cos x))) is V11() real ext-real M2( REAL )
- (sqrt ((1 - (cos x)) / (1 + (cos x)))) is V11() real ext-real M2( REAL )
sin (x / 2) is V11() real ext-real M2( REAL )
(sin (x / 2)) ^2 is V11() real ext-real M2( REAL )
(sin (x / 2)) * (sin (x / 2)) is V11() real ext-real set
2 * ((sin (x / 2)) ^2) is V11() real ext-real M2( REAL )
1 - (2 * ((sin (x / 2)) ^2)) is V11() real ext-real M2( REAL )
1 - (1 - (2 * ((sin (x / 2)) ^2))) is V11() real ext-real M2( REAL )
2 * (x / 2) is V11() real ext-real M2( REAL )
cos (2 * (x / 2)) is V11() real ext-real M2( REAL )
1 + (cos (2 * (x / 2))) is V11() real ext-real M2( REAL )
(1 - (1 - (2 * ((sin (x / 2)) ^2)))) / (1 + (cos (2 * (x / 2)))) is V11() real ext-real M2( REAL )
sqrt ((1 - (1 - (2 * ((sin (x / 2)) ^2)))) / (1 + (cos (2 * (x / 2))))) is V11() real ext-real M2( REAL )
1 - 1 is V11() real ext-real M2( REAL )
(1 - 1) + (2 * ((sin (x / 2)) ^2)) is V11() real ext-real M2( REAL )
cos (x / 2) is V11() real ext-real M2( REAL )
(cos (x / 2)) ^2 is V11() real ext-real M2( REAL )
(cos (x / 2)) * (cos (x / 2)) is V11() real ext-real set
2 * ((cos (x / 2)) ^2) is V11() real ext-real M2( REAL )
(2 * ((cos (x / 2)) ^2)) - 1 is V11() real ext-real M2( REAL )
1 + ((2 * ((cos (x / 2)) ^2)) - 1) is V11() real ext-real M2( REAL )
((1 - 1) + (2 * ((sin (x / 2)) ^2))) / (1 + ((2 * ((cos (x / 2)) ^2)) - 1)) is V11() real ext-real M2( REAL )
sqrt (((1 - 1) + (2 * ((sin (x / 2)) ^2))) / (1 + ((2 * ((cos (x / 2)) ^2)) - 1))) is V11() real ext-real M2( REAL )
((sin (x / 2)) ^2) / ((cos (x / 2)) ^2) is V11() real ext-real M2( REAL )
sqrt (((sin (x / 2)) ^2) / ((cos (x / 2)) ^2)) is V11() real ext-real M2( REAL )
(tan (x / 2)) ^2 is V11() real ext-real M2( REAL )
(tan (x / 2)) * (tan (x / 2)) is V11() real ext-real set
sqrt ((tan (x / 2)) ^2) is V11() real ext-real M2( REAL )
abs (tan (x / 2)) is V11() real ext-real M2( REAL )
- 1 is V11() real ext-real M2( REAL )
(sqrt ((1 - (cos x)) / (1 + (cos x)))) * (- 1) is V11() real ext-real M2( REAL )
- (tan (x / 2)) is V11() real ext-real M2( REAL )
(- (tan (x / 2))) * (- 1) is V11() real ext-real M2( REAL )
x is V11() real ext-real set
x / 2 is V11() real ext-real M2( REAL )
cos (x / 2) is V11() real ext-real M2( REAL )
cot (x / 2) is V11() real ext-real M2( REAL )
cos (x / 2) is V11() real ext-real set
sin (x / 2) is V11() real ext-real set
(cos (x / 2)) / (sin (x / 2)) is V11() real ext-real set
cos x is V11() real ext-real set
1 + (cos x) is V11() real ext-real M2( REAL )
sin x is V11() real ext-real set
(1 + (cos x)) / (sin x) is V11() real ext-real M2( REAL )
2 * (cos (x / 2)) is V11() real ext-real M2( REAL )
(cos (x / 2)) ^2 is V11() real ext-real M2( REAL )
(cos (x / 2)) * (cos (x / 2)) is V11() real ext-real set
2 * ((cos (x / 2)) ^2) is V11() real ext-real M2( REAL )
(2 * ((cos (x / 2)) ^2)) - 1 is V11() real ext-real M2( REAL )
1 + ((2 * ((cos (x / 2)) ^2)) - 1) is V11() real ext-real M2( REAL )
2 * (x / 2) is V11() real ext-real M2( REAL )
sin (2 * (x / 2)) is V11() real ext-real M2( REAL )
(1 + ((2 * ((cos (x / 2)) ^2)) - 1)) / (sin (2 * (x / 2))) is V11() real ext-real M2( REAL )
(cos (x / 2)) * (cos (x / 2)) is V11() real ext-real M2( REAL )
2 * ((cos (x / 2)) * (cos (x / 2))) is V11() real ext-real M2( REAL )
sin (x / 2) is V11() real ext-real M2( REAL )
2 * (sin (x / 2)) is V11() real ext-real M2( REAL )
(2 * (sin (x / 2))) * (cos (x / 2)) is V11() real ext-real M2( REAL )
(2 * ((cos (x / 2)) * (cos (x / 2)))) / ((2 * (sin (x / 2))) * (cos (x / 2))) is V11() real ext-real M2( REAL )
(2 * (cos (x / 2))) * (cos (x / 2)) is V11() real ext-real M2( REAL )
(2 * (cos (x / 2))) * (sin (x / 2)) is V11() real ext-real M2( REAL )
((2 * (cos (x / 2))) * (cos (x / 2))) / ((2 * (cos (x / 2))) * (sin (x / 2))) is V11() real ext-real M2( REAL )
x is V11() real ext-real set
x / 2 is V11() real ext-real M2( REAL )
sin (x / 2) is V11() real ext-real M2( REAL )
cot (x / 2) is V11() real ext-real M2( REAL )
cos (x / 2) is V11() real ext-real set
sin (x / 2) is V11() real ext-real set
(cos (x / 2)) / (sin (x / 2)) is V11() real ext-real set
sin x is V11() real ext-real set
cos x is V11() real ext-real set
1 - (cos x) is V11() real ext-real M2( REAL )
(sin x) / (1 - (cos x)) is V11() real ext-real M2( REAL )
2 * (sin (x / 2)) is V11() real ext-real M2( REAL )
cos (x / 2) is V11() real ext-real M2( REAL )
(2 * (sin (x / 2))) * (cos (x / 2)) is V11() real ext-real M2( REAL )
2 * (x / 2) is V11() real ext-real M2( REAL )
cos (2 * (x / 2)) is V11() real ext-real M2( REAL )
1 - (cos (2 * (x / 2))) is V11() real ext-real M2( REAL )
((2 * (sin (x / 2))) * (cos (x / 2))) / (1 - (cos (2 * (x / 2)))) is V11() real ext-real M2( REAL )
(sin (x / 2)) ^2 is V11() real ext-real M2( REAL )
(sin (x / 2)) * (sin (x / 2)) is V11() real ext-real set
2 * ((sin (x / 2)) ^2) is V11() real ext-real M2( REAL )
1 - (2 * ((sin (x / 2)) ^2)) is V11() real ext-real M2( REAL )
1 - (1 - (2 * ((sin (x / 2)) ^2))) is V11() real ext-real M2( REAL )
((2 * (sin (x / 2))) * (cos (x / 2))) / (1 - (1 - (2 * ((sin (x / 2)) ^2)))) is V11() real ext-real M2( REAL )
(2 * (sin (x / 2))) * (sin (x / 2)) is V11() real ext-real M2( REAL )
((2 * (sin (x / 2))) * (cos (x / 2))) / ((2 * (sin (x / 2))) * (sin (x / 2))) is V11() real ext-real M2( REAL )
(cos (x / 2)) / (sin (x / 2)) is V11() real ext-real M2( REAL )
x is V11() real ext-real set
x / 2 is V11() real ext-real M2( REAL )
cot (x / 2) is V11() real ext-real M2( REAL )
cos (x / 2) is V11() real ext-real set
sin (x / 2) is V11() real ext-real set
(cos (x / 2)) / (sin (x / 2)) is V11() real ext-real set
cos x is V11() real ext-real set
1 + (cos x) is V11() real ext-real M2( REAL )
1 - (cos x) is V11() real ext-real M2( REAL )
(1 + (cos x)) / (1 - (cos x)) is V11() real ext-real M2( REAL )
sqrt ((1 + (cos x)) / (1 - (cos x))) is V11() real ext-real M2( REAL )
- (sqrt ((1 + (cos x)) / (1 - (cos x)))) is V11() real ext-real M2( REAL )
cos (x / 2) is V11() real ext-real M2( REAL )
(cos (x / 2)) ^2 is V11() real ext-real M2( REAL )
(cos (x / 2)) * (cos (x / 2)) is V11() real ext-real set
2 * ((cos (x / 2)) ^2) is V11() real ext-real M2( REAL )
(2 * ((cos (x / 2)) ^2)) - 1 is V11() real ext-real M2( REAL )
1 + ((2 * ((cos (x / 2)) ^2)) - 1) is V11() real ext-real M2( REAL )
2 * (x / 2) is V11() real ext-real M2( REAL )
cos (2 * (x / 2)) is V11() real ext-real M2( REAL )
1 - (cos (2 * (x / 2))) is V11() real ext-real M2( REAL )
(1 + ((2 * ((cos (x / 2)) ^2)) - 1)) / (1 - (cos (2 * (x / 2)))) is V11() real ext-real M2( REAL )
sqrt ((1 + ((2 * ((cos (x / 2)) ^2)) - 1)) / (1 - (cos (2 * (x / 2))))) is V11() real ext-real M2( REAL )
1 - (2 * ((cos (x / 2)) ^2)) is V11() real ext-real M2( REAL )
1 - (1 - (2 * ((cos (x / 2)) ^2))) is V11() real ext-real M2( REAL )
sin (x / 2) is V11() real ext-real M2( REAL )
(sin (x / 2)) ^2 is V11() real ext-real M2( REAL )
(sin (x / 2)) * (sin (x / 2)) is V11() real ext-real set
2 * ((sin (x / 2)) ^2) is V11() real ext-real M2( REAL )
1 - (2 * ((sin (x / 2)) ^2)) is V11() real ext-real M2( REAL )
1 - (1 - (2 * ((sin (x / 2)) ^2))) is V11() real ext-real M2( REAL )
(1 - (1 - (2 * ((cos (x / 2)) ^2)))) / (1 - (1 - (2 * ((sin (x / 2)) ^2)))) is V11() real ext-real M2( REAL )
sqrt ((1 - (1 - (2 * ((cos (x / 2)) ^2)))) / (1 - (1 - (2 * ((sin (x / 2)) ^2))))) is V11() real ext-real M2( REAL )
((cos (x / 2)) ^2) / ((sin (x / 2)) ^2) is V11() real ext-real M2( REAL )
sqrt (((cos (x / 2)) ^2) / ((sin (x / 2)) ^2)) is V11() real ext-real M2( REAL )
(cot (x / 2)) ^2 is V11() real ext-real M2( REAL )
(cot (x / 2)) * (cot (x / 2)) is V11() real ext-real set
sqrt ((cot (x / 2)) ^2) is V11() real ext-real M2( REAL )
abs (cot (x / 2)) is V11() real ext-real M2( REAL )
- 1 is V11() real ext-real M2( REAL )
(sqrt ((1 + (cos x)) / (1 - (cos x)))) * (- 1) is V11() real ext-real M2( REAL )
- (cot (x / 2)) is V11() real ext-real M2( REAL )
(- (cot (x / 2))) * (- 1) is V11() real ext-real M2( REAL )
x is V11() real ext-real set
x / 2 is V11() real ext-real M2( REAL )
sin (x / 2) is V11() real ext-real M2( REAL )
cos (x / 2) is V11() real ext-real M2( REAL )
tan (x / 2) is V11() real ext-real M2( REAL )
sin (x / 2) is V11() real ext-real set
cos (x / 2) is V11() real ext-real set
(sin (x / 2)) / (cos (x / 2)) is V11() real ext-real set
(tan (x / 2)) ^2 is V11() real ext-real M2( REAL )
(tan (x / 2)) * (tan (x / 2)) is V11() real ext-real set
1 - ((tan (x / 2)) ^2) is V11() real ext-real M2( REAL )
sec (x / 2) is V11() real ext-real M2( REAL )
1 / (cos (x / 2)) is V11() real ext-real set
sec x is V11() real ext-real M2( REAL )
cos x is V11() real ext-real set
1 / (cos x) is V11() real ext-real set
2 * (sec x) is V11() real ext-real M2( REAL )
(sec x) + 1 is V11() real ext-real M2( REAL )
(2 * (sec x)) / ((sec x) + 1) is V11() real ext-real M2( REAL )
sqrt ((2 * (sec x)) / ((sec x) + 1)) is V11() real ext-real M2( REAL )
- (sqrt ((2 * (sec x)) / ((sec x) + 1))) is V11() real ext-real M2( REAL )
(sec (x / 2)) ^2 is V11() real ext-real M2( REAL )
(sec (x / 2)) * (sec (x / 2)) is V11() real ext-real set
(1 - ((tan (x / 2)) ^2)) + ((sec (x / 2)) ^2) is V11() real ext-real M2( REAL )
1 + ((tan (x / 2)) ^2) is V11() real ext-real M2( REAL )
(1 + ((tan (x / 2)) ^2)) + (1 - ((tan (x / 2)) ^2)) is V11() real ext-real M2( REAL )
1 + 1 is natural V11() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() M3( REAL , NAT )
((sec (x / 2)) ^2) / (1 - ((tan (x / 2)) ^2)) is V11() real ext-real M2( REAL )
2 * (((sec (x / 2)) ^2) / (1 - ((tan (x / 2)) ^2))) is V11() real ext-real M2( REAL )
2 * (x / 2) is V11() real ext-real M2( REAL )
sec (2 * (x / 2)) is V11() real ext-real M2( REAL )
cos (2 * (x / 2)) is V11() real ext-real set
1 / (cos (2 * (x / 2))) is V11() real ext-real set
(sec (2 * (x / 2))) + 1 is V11() real ext-real M2( REAL )
(2 * (((sec (x / 2)) ^2) / (1 - ((tan (x / 2)) ^2)))) / ((sec (2 * (x / 2))) + 1) is V11() real ext-real M2( REAL )
sqrt ((2 * (((sec (x / 2)) ^2) / (1 - ((tan (x / 2)) ^2)))) / ((sec (2 * (x / 2))) + 1)) is V11() real ext-real M2( REAL )
(((sec (x / 2)) ^2) / (1 - ((tan (x / 2)) ^2))) + 1 is V11() real ext-real M2( REAL )
(2 * (((sec (x / 2)) ^2) / (1 - ((tan (x / 2)) ^2)))) / ((((sec (x / 2)) ^2) / (1 - ((tan (x / 2)) ^2))) + 1) is V11() real ext-real M2( REAL )
sqrt ((2 * (((sec (x / 2)) ^2) / (1 - ((tan (x / 2)) ^2)))) / ((((sec (x / 2)) ^2) / (1 - ((tan (x / 2)) ^2))) + 1)) is V11() real ext-real M2( REAL )
(2 * (((sec (x / 2)) ^2) / (1 - ((tan (x / 2)) ^2)))) * (1 - ((tan (x / 2)) ^2)) is V11() real ext-real M2( REAL )
((((sec (x / 2)) ^2) / (1 - ((tan (x / 2)) ^2))) + 1) * (1 - ((tan (x / 2)) ^2)) is V11() real ext-real M2( REAL )
((2 * (((sec (x / 2)) ^2) / (1 - ((tan (x / 2)) ^2)))) * (1 - ((tan (x / 2)) ^2))) / (((((sec (x / 2)) ^2) / (1 - ((tan (x / 2)) ^2))) + 1) * (1 - ((tan (x / 2)) ^2))) is V11() real ext-real M2( REAL )
sqrt (((2 * (((sec (x / 2)) ^2) / (1 - ((tan (x / 2)) ^2)))) * (1 - ((tan (x / 2)) ^2))) / (((((sec (x / 2)) ^2) / (1 - ((tan (x / 2)) ^2))) + 1) * (1 - ((tan (x / 2)) ^2)))) is V11() real ext-real M2( REAL )
(((sec (x / 2)) ^2) / (1 - ((tan (x / 2)) ^2))) * (1 - ((tan (x / 2)) ^2)) is V11() real ext-real M2( REAL )
2 * ((((sec (x / 2)) ^2) / (1 - ((tan (x / 2)) ^2))) * (1 - ((tan (x / 2)) ^2))) is V11() real ext-real M2( REAL )
1 * (1 - ((tan (x / 2)) ^2)) is V11() real ext-real M2( REAL )
((((sec (x / 2)) ^2) / (1 - ((tan (x / 2)) ^2))) * (1 - ((tan (x / 2)) ^2))) + (1 * (1 - ((tan (x / 2)) ^2))) is V11() real ext-real M2( REAL )
(2 * ((((sec (x / 2)) ^2) / (1 - ((tan (x / 2)) ^2))) * (1 - ((tan (x / 2)) ^2)))) / (((((sec (x / 2)) ^2) / (1 - ((tan (x / 2)) ^2))) * (1 - ((tan (x / 2)) ^2))) + (1 * (1 - ((tan (x / 2)) ^2)))) is V11() real ext-real M2( REAL )
sqrt ((2 * ((((sec (x / 2)) ^2) / (1 - ((tan (x / 2)) ^2))) * (1 - ((tan (x / 2)) ^2)))) / (((((sec (x / 2)) ^2) / (1 - ((tan (x / 2)) ^2))) * (1 - ((tan (x / 2)) ^2))) + (1 * (1 - ((tan (x / 2)) ^2))))) is V11() real ext-real M2( REAL )
((sec (x / 2)) ^2) + (1 - ((tan (x / 2)) ^2)) is V11() real ext-real M2( REAL )
(2 * ((((sec (x / 2)) ^2) / (1 - ((tan (x / 2)) ^2))) * (1 - ((tan (x / 2)) ^2)))) / (((sec (x / 2)) ^2) + (1 - ((tan (x / 2)) ^2))) is V11() real ext-real M2( REAL )
sqrt ((2 * ((((sec (x / 2)) ^2) / (1 - ((tan (x / 2)) ^2))) * (1 - ((tan (x / 2)) ^2)))) / (((sec (x / 2)) ^2) + (1 - ((tan (x / 2)) ^2)))) is V11() real ext-real M2( REAL )
2 * ((sec (x / 2)) ^2) is V11() real ext-real M2( REAL )
(2 * ((sec (x / 2)) ^2)) / 2 is V11() real ext-real M2( REAL )
sqrt ((2 * ((sec (x / 2)) ^2)) / 2) is V11() real ext-real M2( REAL )
abs (sec (x / 2)) is V11() real ext-real M2( REAL )
- 1 is V11() real ext-real M2( REAL )
(sqrt ((2 * (sec x)) / ((sec x) + 1))) * (- 1) is V11() real ext-real M2( REAL )
- (sec (x / 2)) is V11() real ext-real M2( REAL )
(- (sec (x / 2))) * (- 1) is V11() real ext-real M2( REAL )
x is V11() real ext-real set
x / 2 is V11() real ext-real M2( REAL )
sin (x / 2) is V11() real ext-real M2( REAL )
cos (x / 2) is V11() real ext-real M2( REAL )
tan (x / 2) is V11() real ext-real M2( REAL )
sin (x / 2) is V11() real ext-real set
cos (x / 2) is V11() real ext-real set
(sin (x / 2)) / (cos (x / 2)) is V11() real ext-real set
(tan (x / 2)) ^2 is V11() real ext-real M2( REAL )
(tan (x / 2)) * (tan (x / 2)) is V11() real ext-real set
1 - ((tan (x / 2)) ^2) is V11() real ext-real M2( REAL )
cosec (x / 2) is V11() real ext-real M2( REAL )
1 / (sin (x / 2)) is V11() real ext-real set
sec x is V11() real ext-real M2( REAL )
cos x is V11() real ext-real set
1 / (cos x) is V11() real ext-real set
2 * (sec x) is V11() real ext-real M2( REAL )
(sec x) - 1 is V11() real ext-real M2( REAL )
(2 * (sec x)) / ((sec x) - 1) is V11() real ext-real M2( REAL )
sqrt ((2 * (sec x)) / ((sec x) - 1)) is V11() real ext-real M2( REAL )
- (sqrt ((2 * (sec x)) / ((sec x) - 1))) is V11() real ext-real M2( REAL )
sec (x / 2) is V11() real ext-real M2( REAL )
1 / (cos (x / 2)) is V11() real ext-real set
(sec (x / 2)) ^2 is V11() real ext-real M2( REAL )
(sec (x / 2)) * (sec (x / 2)) is V11() real ext-real set
((sec (x / 2)) ^2) - (1 - ((tan (x / 2)) ^2)) is V11() real ext-real M2( REAL )
1 + ((tan (x / 2)) ^2) is V11() real ext-real M2( REAL )
(1 + ((tan (x / 2)) ^2)) - (1 - ((tan (x / 2)) ^2)) is V11() real ext-real M2( REAL )
2 * ((tan (x / 2)) ^2) is V11() real ext-real M2( REAL )
((sec (x / 2)) ^2) / (1 - ((tan (x / 2)) ^2)) is V11() real ext-real M2( REAL )
2 * (((sec (x / 2)) ^2) / (1 - ((tan (x / 2)) ^2))) is V11() real ext-real M2( REAL )
2 * (x / 2) is V11() real ext-real M2( REAL )
sec (2 * (x / 2)) is V11() real ext-real M2( REAL )
cos (2 * (x / 2)) is V11() real ext-real set
1 / (cos (2 * (x / 2))) is V11() real ext-real set
(sec (2 * (x / 2))) - 1 is V11() real ext-real M2( REAL )
(2 * (((sec (x / 2)) ^2) / (1 - ((tan (x / 2)) ^2)))) / ((sec (2 * (x / 2))) - 1) is V11() real ext-real M2( REAL )
sqrt ((2 * (((sec (x / 2)) ^2) / (1 - ((tan (x / 2)) ^2)))) / ((sec (2 * (x / 2))) - 1)) is V11() real ext-real M2( REAL )
(((sec (x / 2)) ^2) / (1 - ((tan (x / 2)) ^2))) - 1 is V11() real ext-real M2( REAL )
(2 * (((sec (x / 2)) ^2) / (1 - ((tan (x / 2)) ^2)))) / ((((sec (x / 2)) ^2) / (1 - ((tan (x / 2)) ^2))) - 1) is V11() real ext-real M2( REAL )
sqrt ((2 * (((sec (x / 2)) ^2) / (1 - ((tan (x / 2)) ^2)))) / ((((sec (x / 2)) ^2) / (1 - ((tan (x / 2)) ^2))) - 1)) is V11() real ext-real M2( REAL )
(2 * (((sec (x / 2)) ^2) / (1 - ((tan (x / 2)) ^2)))) * (1 - ((tan (x / 2)) ^2)) is V11() real ext-real M2( REAL )
((((sec (x / 2)) ^2) / (1 - ((tan (x / 2)) ^2))) - 1) * (1 - ((tan (x / 2)) ^2)) is V11() real ext-real M2( REAL )
((2 * (((sec (x / 2)) ^2) / (1 - ((tan (x / 2)) ^2)))) * (1 - ((tan (x / 2)) ^2))) / (((((sec (x / 2)) ^2) / (1 - ((tan (x / 2)) ^2))) - 1) * (1 - ((tan (x / 2)) ^2))) is V11() real ext-real M2( REAL )
sqrt (((2 * (((sec (x / 2)) ^2) / (1 - ((tan (x / 2)) ^2)))) * (1 - ((tan (x / 2)) ^2))) / (((((sec (x / 2)) ^2) / (1 - ((tan (x / 2)) ^2))) - 1) * (1 - ((tan (x / 2)) ^2)))) is V11() real ext-real M2( REAL )
(((sec (x / 2)) ^2) / (1 - ((tan (x / 2)) ^2))) * (1 - ((tan (x / 2)) ^2)) is V11() real ext-real M2( REAL )
2 * ((((sec (x / 2)) ^2) / (1 - ((tan (x / 2)) ^2))) * (1 - ((tan (x / 2)) ^2))) is V11() real ext-real M2( REAL )
1 * (1 - ((tan (x / 2)) ^2)) is V11() real ext-real M2( REAL )
((((sec (x / 2)) ^2) / (1 - ((tan (x / 2)) ^2))) * (1 - ((tan (x / 2)) ^2))) - (1 * (1 - ((tan (x / 2)) ^2))) is V11() real ext-real M2( REAL )
(2 * ((((sec (x / 2)) ^2) / (1 - ((tan (x / 2)) ^2))) * (1 - ((tan (x / 2)) ^2)))) / (((((sec (x / 2)) ^2) / (1 - ((tan (x / 2)) ^2))) * (1 - ((tan (x / 2)) ^2))) - (1 * (1 - ((tan (x / 2)) ^2)))) is V11() real ext-real M2( REAL )
sqrt ((2 * ((((sec (x / 2)) ^2) / (1 - ((tan (x / 2)) ^2))) * (1 - ((tan (x / 2)) ^2)))) / (((((sec (x / 2)) ^2) / (1 - ((tan (x / 2)) ^2))) * (1 - ((tan (x / 2)) ^2))) - (1 * (1 - ((tan (x / 2)) ^2))))) is V11() real ext-real M2( REAL )
(2 * ((((sec (x / 2)) ^2) / (1 - ((tan (x / 2)) ^2))) * (1 - ((tan (x / 2)) ^2)))) / (((sec (x / 2)) ^2) - (1 - ((tan (x / 2)) ^2))) is V11() real ext-real M2( REAL )
sqrt ((2 * ((((sec (x / 2)) ^2) / (1 - ((tan (x / 2)) ^2))) * (1 - ((tan (x / 2)) ^2)))) / (((sec (x / 2)) ^2) - (1 - ((tan (x / 2)) ^2)))) is V11() real ext-real M2( REAL )
2 * ((sec (x / 2)) ^2) is V11() real ext-real M2( REAL )
(2 * ((sec (x / 2)) ^2)) / (2 * ((tan (x / 2)) ^2)) is V11() real ext-real M2( REAL )
sqrt ((2 * ((sec (x / 2)) ^2)) / (2 * ((tan (x / 2)) ^2))) is V11() real ext-real M2( REAL )
((sec (x / 2)) ^2) / ((tan (x / 2)) ^2) is V11() real ext-real M2( REAL )
sqrt (((sec (x / 2)) ^2) / ((tan (x / 2)) ^2)) is V11() real ext-real M2( REAL )
(sec (x / 2)) / (tan (x / 2)) is V11() real ext-real M2( REAL )
((sec (x / 2)) / (tan (x / 2))) ^2 is V11() real ext-real M2( REAL )
((sec (x / 2)) / (tan (x / 2))) * ((sec (x / 2)) / (tan (x / 2))) is V11() real ext-real set
sqrt (((sec (x / 2)) / (tan (x / 2))) ^2) is V11() real ext-real M2( REAL )
(cosec (x / 2)) ^2 is V11() real ext-real M2( REAL )
(cosec (x / 2)) * (cosec (x / 2)) is V11() real ext-real set
sqrt ((cosec (x / 2)) ^2) is V11() real ext-real M2( REAL )
abs (cosec (x / 2)) is V11() real ext-real M2( REAL )
- 1 is V11() real ext-real M2( REAL )
(sqrt ((2 * (sec x)) / ((sec x) - 1))) * (- 1) is V11() real ext-real M2( REAL )
- (cosec (x / 2)) is V11() real ext-real M2( REAL )
(- (cosec (x / 2))) * (- 1) is V11() real ext-real M2( REAL )
x is V11() real ext-real set
cosh x is V11() real ext-real M2( REAL )
sinh x is V11() real ext-real M2( REAL )
(cosh x) / (sinh x) is V11() real ext-real M2( REAL )
1 / (cosh x) is V11() real ext-real M2( REAL )
1 / (sinh x) is V11() real ext-real M2( REAL )
x is V11() real ext-real set
(x) is V11() real ext-real M2( REAL )
cosh x is V11() real ext-real M2( REAL )
sinh x is V11() real ext-real M2( REAL )
(cosh x) / (sinh x) is V11() real ext-real M2( REAL )
exp_R x is V11() real ext-real set
- x is V11() real ext-real set
exp_R (- x) is V11() real ext-real set
(exp_R x) + (exp_R (- x)) is V11() real ext-real set
(exp_R x) - (exp_R (- x)) is V11() real ext-real set
((exp_R x) + (exp_R (- x))) / ((exp_R x) - (exp_R (- x))) is V11() real ext-real M2( COMPLEX )
(x) is V11() real ext-real M2( REAL )
1 / (cosh x) is V11() real ext-real M2( REAL )
2 / ((exp_R x) + (exp_R (- x))) is V11() real ext-real M2( REAL )
(x) is V11() real ext-real M2( REAL )
1 / (sinh x) is V11() real ext-real M2( REAL )
2 / ((exp_R x) - (exp_R (- x))) is V11() real ext-real M2( REAL )
cosh . x is V11() real ext-real M2( REAL )
1 / (cosh . x) is V11() real ext-real M2( REAL )
exp_R . x is V11() real ext-real M2( REAL )
exp_R . (- x) is V11() real ext-real M2( REAL )
(exp_R . x) + (exp_R . (- x)) is V11() real ext-real M2( REAL )
((exp_R . x) + (exp_R . (- x))) / 2 is V11() real ext-real M2( REAL )
1 / (((exp_R . x) + (exp_R . (- x))) / 2) is V11() real ext-real M2( REAL )
1 * 2 is natural V11() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() M3( REAL , NAT )
(((exp_R . x) + (exp_R . (- x))) / 2) * 2 is V11() real ext-real M2( REAL )
(1 * 2) / ((((exp_R . x) + (exp_R . (- x))) / 2) * 2) is V11() real ext-real M2( REAL )
(exp_R . x) + (exp_R (- x)) is V11() real ext-real M2( REAL )
2 / ((exp_R . x) + (exp_R (- x))) is V11() real ext-real M2( REAL )
sinh . x is V11() real ext-real M2( REAL )
1 / (sinh . x) is V11() real ext-real M2( REAL )
(exp_R . x) - (exp_R . (- x)) is V11() real ext-real M2( REAL )
((exp_R . x) - (exp_R . (- x))) / 2 is V11() real ext-real M2( REAL )
1 / (((exp_R . x) - (exp_R . (- x))) / 2) is V11() real ext-real M2( REAL )
(((exp_R . x) - (exp_R . (- x))) / 2) * 2 is V11() real ext-real M2( REAL )
(1 * 2) / ((((exp_R . x) - (exp_R . (- x))) / 2) * 2) is V11() real ext-real M2( REAL )
(exp_R . x) - (exp_R (- x)) is V11() real ext-real M2( REAL )
2 / ((exp_R . x) - (exp_R (- x))) is V11() real ext-real M2( REAL )
(cosh . x) / (sinh x) is V11() real ext-real M2( REAL )
(cosh . x) / (sinh . x) is V11() real ext-real M2( REAL )
(((exp_R . x) + (exp_R . (- x))) / 2) / (sinh . x) is V11() real ext-real M2( REAL )
(((exp_R . x) + (exp_R . (- x))) / 2) / (((exp_R . x) - (exp_R . (- x))) / 2) is V11() real ext-real M2( REAL )
((((exp_R . x) + (exp_R . (- x))) / 2) * 2) / ((((exp_R . x) - (exp_R . (- x))) / 2) * 2) is V11() real ext-real M2( REAL )
((exp_R . x) + (exp_R . (- x))) / ((exp_R . x) - (exp_R (- x))) is V11() real ext-real M2( REAL )
((exp_R . x) + (exp_R . (- x))) / ((exp_R x) - (exp_R (- x))) is V11() real ext-real M2( REAL )
((exp_R . x) + (exp_R (- x))) / ((exp_R x) - (exp_R (- x))) is V11() real ext-real M2( REAL )
x is V11() real ext-real set
exp_R x is V11() real ext-real set
- x is V11() real ext-real set
exp_R (- x) is V11() real ext-real set
(exp_R x) - (exp_R (- x)) is V11() real ext-real set
tanh x is V11() real ext-real M2( REAL )
(x) is V11() real ext-real M2( REAL )
cosh x is V11() real ext-real M2( REAL )
sinh x is V11() real ext-real M2( REAL )
(cosh x) / (sinh x) is V11() real ext-real M2( REAL )
(tanh x) * (x) is V11() real ext-real M2( REAL )
(exp_R x) + (exp_R (- x)) is V11() real ext-real set
0 + 0 is natural V11() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() M3( REAL , NAT )
tanh . x is V11() real ext-real M2( REAL )
(tanh . x) * (x) is V11() real ext-real M2( REAL )
exp_R . x is V11() real ext-real M2( REAL )
exp_R . (- x) is V11() real ext-real M2( REAL )
(exp_R . x) - (exp_R . (- x)) is V11() real ext-real M2( REAL )
(exp_R . x) + (exp_R . (- x)) is V11() real ext-real M2( REAL )
((exp_R . x) - (exp_R . (- x))) / ((exp_R . x) + (exp_R . (- x))) is V11() real ext-real M2( REAL )
(((exp_R . x) - (exp_R . (- x))) / ((exp_R . x) + (exp_R . (- x)))) * (x) is V11() real ext-real M2( REAL )
((exp_R x) + (exp_R (- x))) / ((exp_R x) - (exp_R (- x))) is V11() real ext-real M2( COMPLEX )
(((exp_R . x) - (exp_R . (- x))) / ((exp_R . x) + (exp_R . (- x)))) * (((exp_R x) + (exp_R (- x))) / ((exp_R x) - (exp_R (- x)))) is V11() real ext-real M2( REAL )
(exp_R . x) + (exp_R (- x)) is V11() real ext-real M2( REAL )
((exp_R . x) - (exp_R . (- x))) / ((exp_R . x) + (exp_R (- x))) is V11() real ext-real M2( REAL )
(((exp_R . x) - (exp_R . (- x))) / ((exp_R . x) + (exp_R (- x)))) * (((exp_R x) + (exp_R (- x))) / ((exp_R x) - (exp_R (- x)))) is V11() real ext-real M2( REAL )
(exp_R x) - (exp_R . (- x)) is V11() real ext-real M2( REAL )
((exp_R x) - (exp_R . (- x))) / ((exp_R . x) + (exp_R (- x))) is V11() real ext-real M2( REAL )
(((exp_R x) - (exp_R . (- x))) / ((exp_R . x) + (exp_R (- x)))) * (((exp_R x) + (exp_R (- x))) / ((exp_R x) - (exp_R (- x)))) is V11() real ext-real M2( REAL )
((exp_R x) - (exp_R (- x))) / ((exp_R . x) + (exp_R (- x))) is V11() real ext-real M2( REAL )
(((exp_R x) - (exp_R (- x))) / ((exp_R . x) + (exp_R (- x)))) * (((exp_R x) + (exp_R (- x))) / ((exp_R x) - (exp_R (- x)))) is V11() real ext-real M2( REAL )
((exp_R x) - (exp_R (- x))) / ((exp_R x) + (exp_R (- x))) is V11() real ext-real M2( COMPLEX )
(((exp_R x) - (exp_R (- x))) / ((exp_R x) + (exp_R (- x)))) * (((exp_R x) + (exp_R (- x))) / ((exp_R x) - (exp_R (- x)))) is V11() real ext-real M2( COMPLEX )
(((exp_R x) - (exp_R (- x))) / ((exp_R x) + (exp_R (- x)))) * ((exp_R x) + (exp_R (- x))) is V11() real ext-real set
((((exp_R x) - (exp_R (- x))) / ((exp_R x) + (exp_R (- x)))) * ((exp_R x) + (exp_R (- x)))) / ((exp_R x) - (exp_R (- x))) is V11() real ext-real M2( COMPLEX )
((exp_R x) - (exp_R (- x))) / ((exp_R x) - (exp_R (- x))) is V11() real ext-real M2( COMPLEX )
x is V11() real ext-real set
(x) is V11() real ext-real M2( REAL )
cosh x is V11() real ext-real M2( REAL )
1 / (cosh x) is V11() real ext-real M2( REAL )
(x) ^2 is V11() real ext-real M2( REAL )
(x) * (x) is V11() real ext-real set
tanh x is V11() real ext-real M2( REAL )
(tanh x) ^2 is V11() real ext-real M2( REAL )
(tanh x) * (tanh x) is V11() real ext-real set
((x) ^2) + ((tanh x) ^2) is V11() real ext-real M2( REAL )
cosh . x is V11() real ext-real M2( REAL )
(cosh . x) ^2 is V11() real ext-real M2( REAL )
(cosh . x) * (cosh . x) is V11() real ext-real set
(1 / (cosh x)) ^2 is V11() real ext-real M2( REAL )
(1 / (cosh x)) * (1 / (cosh x)) is V11() real ext-real set
tanh . x is V11() real ext-real M2( REAL )
(tanh . x) ^2 is V11() real ext-real M2( REAL )
(tanh . x) * (tanh . x) is V11() real ext-real set
((1 / (cosh x)) ^2) + ((tanh . x) ^2) is V11() real ext-real M2( REAL )
1 / (cosh . x) is V11() real ext-real M2( REAL )
(1 / (cosh . x)) ^2 is V11() real ext-real M2( REAL )
(1 / (cosh . x)) * (1 / (cosh . x)) is V11() real ext-real set
((1 / (cosh . x)) ^2) + ((tanh . x) ^2) is V11() real ext-real M2( REAL )
1 ^2 is V11() real ext-real M2( REAL )
1 * 1 is V11() real ext-real set
(1 ^2) / ((cosh . x) ^2) is V11() real ext-real M2( REAL )
((1 ^2) / ((cosh . x) ^2)) + ((tanh . x) ^2) is V11() real ext-real M2( REAL )
sinh . x is V11() real ext-real M2( REAL )
(sinh . x) / (cosh . x) is V11() real ext-real M2( REAL )
((sinh . x) / (cosh . x)) ^2 is V11() real ext-real M2( REAL )
((sinh . x) / (cosh . x)) * ((sinh . x) / (cosh . x)) is V11() real ext-real set
((1 ^2) / ((cosh . x) ^2)) + (((sinh . x) / (cosh . x)) ^2) is V11() real ext-real M2( REAL )
1 / ((cosh . x) ^2) is V11() real ext-real M2( REAL )
(sinh . x) ^2 is V11() real ext-real M2( REAL )
(sinh . x) * (sinh . x) is V11() real ext-real set
((sinh . x) ^2) / ((cosh . x) ^2) is V11() real ext-real M2( REAL )
(1 / ((cosh . x) ^2)) + (((sinh . x) ^2) / ((cosh . x) ^2)) is V11() real ext-real M2( REAL )
1 + ((sinh . x) ^2) is V11() real ext-real M2( REAL )
(1 + ((sinh . x) ^2)) / ((cosh . x) ^2) is V11() real ext-real M2( REAL )
((cosh . x) ^2) - ((sinh . x) ^2) is V11() real ext-real M2( REAL )
(((cosh . x) ^2) - ((sinh . x) ^2)) + ((sinh . x) ^2) is V11() real ext-real M2( REAL )
((((cosh . x) ^2) - ((sinh . x) ^2)) + ((sinh . x) ^2)) / ((cosh . x) ^2) is V11() real ext-real M2( REAL )
((cosh . x) ^2) / ((cosh . x) ^2) is V11() real ext-real M2( REAL )
x is V11() real ext-real set
sinh x is V11() real ext-real M2( REAL )
(x) is V11() real ext-real M2( REAL )
cosh x is V11() real ext-real M2( REAL )
(cosh x) / (sinh x) is V11() real ext-real M2( REAL )
(x) ^2 is V11() real ext-real M2( REAL )
(x) * (x) is V11() real ext-real set
(x) is V11() real ext-real M2( REAL )
1 / (sinh x) is V11() real ext-real M2( REAL )
(x) ^2 is V11() real ext-real M2( REAL )
(x) * (x) is V11() real ext-real set
((x) ^2) - ((x) ^2) is V11() real ext-real M2( REAL )
(sinh x) ^2 is V11() real ext-real M2( REAL )
(sinh x) * (sinh x) is V11() real ext-real set
(cosh x) ^2 is V11() real ext-real M2( REAL )
(cosh x) * (cosh x) is V11() real ext-real set
((cosh x) ^2) / ((sinh x) ^2) is V11() real ext-real M2( REAL )
(1 / (sinh x)) ^2 is V11() real ext-real M2( REAL )
(1 / (sinh x)) * (1 / (sinh x)) is V11() real ext-real set
(((cosh x) ^2) / ((sinh x) ^2)) - ((1 / (sinh x)) ^2) is V11() real ext-real M2( REAL )
1 ^2 is V11() real ext-real M2( REAL )
1 * 1 is V11() real ext-real set
(1 ^2) / ((sinh x) ^2) is V11() real ext-real M2( REAL )
(((cosh x) ^2) / ((sinh x) ^2)) - ((1 ^2) / ((sinh x) ^2)) is V11() real ext-real M2( REAL )
((cosh x) ^2) - 1 is V11() real ext-real M2( REAL )
(((cosh x) ^2) - 1) / ((sinh x) ^2) is V11() real ext-real M2( REAL )
cosh . x is V11() real ext-real M2( REAL )
(cosh . x) ^2 is V11() real ext-real M2( REAL )
(cosh . x) * (cosh . x) is V11() real ext-real set
sinh . x is V11() real ext-real M2( REAL )
(sinh . x) ^2 is V11() real ext-real M2( REAL )
(sinh . x) * (sinh . x) is V11() real ext-real set
((cosh . x) ^2) - ((sinh . x) ^2) is V11() real ext-real M2( REAL )
((cosh x) ^2) - (((cosh . x) ^2) - ((sinh . x) ^2)) is V11() real ext-real M2( REAL )
(((cosh x) ^2) - (((cosh . x) ^2) - ((sinh . x) ^2))) / ((sinh x) ^2) is V11() real ext-real M2( REAL )
((cosh x) ^2) - ((cosh . x) ^2) is V11() real ext-real M2( REAL )
(((cosh x) ^2) - ((cosh . x) ^2)) + ((sinh . x) ^2) is V11() real ext-real M2( REAL )
((((cosh x) ^2) - ((cosh . x) ^2)) + ((sinh . x) ^2)) / ((sinh x) ^2) is V11() real ext-real M2( REAL )
((cosh x) ^2) - ((cosh x) ^2) is V11() real ext-real M2( REAL )
(((cosh x) ^2) - ((cosh x) ^2)) + ((sinh . x) ^2) is V11() real ext-real M2( REAL )
((((cosh x) ^2) - ((cosh x) ^2)) + ((sinh . x) ^2)) / ((sinh x) ^2) is V11() real ext-real M2( REAL )
0 + ((sinh x) ^2) is V11() real ext-real M2( REAL )
(0 + ((sinh x) ^2)) / ((sinh x) ^2) is V11() real ext-real M2( REAL )
x is V11() real ext-real set
- x is V11() real ext-real set
((- x)) is V11() real ext-real M2( REAL )
cosh (- x) is V11() real ext-real M2( REAL )
sinh (- x) is V11() real ext-real M2( REAL )
(cosh (- x)) / (sinh (- x)) is V11() real ext-real M2( REAL )
(x) is V11() real ext-real M2( REAL )
cosh x is V11() real ext-real M2( REAL )
sinh x is V11() real ext-real M2( REAL )
(cosh x) / (sinh x) is V11() real ext-real M2( REAL )
- (x) is V11() real ext-real M2( REAL )
cosh . (- x) is V11() real ext-real M2( REAL )
(cosh . (- x)) / (sinh (- x)) is V11() real ext-real M2( REAL )
sinh . (- x) is V11() real ext-real M2( REAL )
(cosh . (- x)) / (sinh . (- x)) is V11() real ext-real M2( REAL )
cosh . x is V11() real ext-real M2( REAL )
(cosh . x) / (sinh . (- x)) is V11() real ext-real M2( REAL )
sinh . x is V11() real ext-real M2( REAL )
- (sinh . x) is V11() real ext-real M2( REAL )
(cosh . x) / (- (sinh . x)) is V11() real ext-real M2( REAL )
(cosh . x) / (sinh . x) is V11() real ext-real M2( REAL )
- ((cosh . x) / (sinh . x)) is V11() real ext-real M2( REAL )
(cosh x) / (sinh . x) is V11() real ext-real M2( REAL )
- ((cosh x) / (sinh . x)) is V11() real ext-real M2( REAL )
x is V11() real ext-real set
sinh x is V11() real ext-real M2( REAL )
(x) is V11() real ext-real M2( REAL )
cosh x is V11() real ext-real M2( REAL )
(cosh x) / (sinh x) is V11() real ext-real M2( REAL )
x2 is V11() real ext-real set
sinh x2 is V11() real ext-real M2( REAL )
x + x2 is V11() real ext-real set
((x + x2)) is V11() real ext-real M2( REAL )
cosh (x + x2) is V11() real ext-real M2( REAL )
sinh (x + x2) is V11() real ext-real M2( REAL )
(cosh (x + x2)) / (sinh (x + x2)) is V11() real ext-real M2( REAL )
(x2) is V11() real ext-real M2( REAL )
cosh x2 is V11() real ext-real M2( REAL )
(cosh x2) / (sinh x2) is V11() real ext-real M2( REAL )
(x) * (x2) is V11() real ext-real M2( REAL )
1 + ((x) * (x2)) is V11() real ext-real M2( REAL )
(x) + (x2) is V11() real ext-real M2( REAL )
(1 + ((x) * (x2))) / ((x) + (x2)) is V11() real ext-real M2( REAL )
sinh . x is V11() real ext-real M2( REAL )
sinh . x2 is V11() real ext-real M2( REAL )
cosh . (x + x2) is V11() real ext-real M2( REAL )
(cosh . (x + x2)) / (sinh (x + x2)) is V11() real ext-real M2( REAL )
sinh . (x + x2) is V11() real ext-real M2( REAL )
(cosh . (x + x2)) / (sinh . (x + x2)) is V11() real ext-real M2( REAL )
cosh . x is V11() real ext-real M2( REAL )
cosh . x2 is V11() real ext-real M2( REAL )
(cosh . x) * (cosh . x2) is V11() real ext-real M2( REAL )
(sinh . x) * (sinh . x2) is V11() real ext-real M2( REAL )
((cosh . x) * (cosh . x2)) + ((sinh . x) * (sinh . x2)) is V11() real ext-real M2( REAL )
(((cosh . x) * (cosh . x2)) + ((sinh . x) * (sinh . x2))) / (sinh . (x + x2)) is V11() real ext-real M2( REAL )
(sinh . x) * (cosh . x2) is V11() real ext-real M2( REAL )
(cosh . x) * (sinh . x2) is V11() real ext-real M2( REAL )
((sinh . x) * (cosh . x2)) + ((cosh . x) * (sinh . x2)) is V11() real ext-real M2( REAL )
(((cosh . x) * (cosh . x2)) + ((sinh . x) * (sinh . x2))) / (((sinh . x) * (cosh . x2)) + ((cosh . x) * (sinh . x2))) is V11() real ext-real M2( REAL )
(((cosh . x) * (cosh . x2)) + ((sinh . x) * (sinh . x2))) / ((sinh . x) * (sinh . x2)) is V11() real ext-real M2( REAL )
(((sinh . x) * (cosh . x2)) + ((cosh . x) * (sinh . x2))) / ((sinh . x) * (sinh . x2)) is V11() real ext-real M2( REAL )
((((cosh . x) * (cosh . x2)) + ((sinh . x) * (sinh . x2))) / ((sinh . x) * (sinh . x2))) / ((((sinh . x) * (cosh . x2)) + ((cosh . x) * (sinh . x2))) / ((sinh . x) * (sinh . x2))) is V11() real ext-real M2( REAL )
((cosh . x) * (cosh . x2)) / ((sinh . x) * (sinh . x2)) is V11() real ext-real M2( REAL )
((sinh . x) * (sinh . x2)) / ((sinh . x) * (sinh . x2)) is V11() real ext-real M2( REAL )
(((cosh . x) * (cosh . x2)) / ((sinh . x) * (sinh . x2))) + (((sinh . x) * (sinh . x2)) / ((sinh . x) * (sinh . x2))) is V11() real ext-real M2( REAL )
((((cosh . x) * (cosh . x2)) / ((sinh . x) * (sinh . x2))) + (((sinh . x) * (sinh . x2)) / ((sinh . x) * (sinh . x2)))) / ((((sinh . x) * (cosh . x2)) + ((cosh . x) * (sinh . x2))) / ((sinh . x) * (sinh . x2))) is V11() real ext-real M2( REAL )
(((cosh . x) * (cosh . x2)) / ((sinh . x) * (sinh . x2))) + 1 is V11() real ext-real M2( REAL )
((((cosh . x) * (cosh . x2)) / ((sinh . x) * (sinh . x2))) + 1) / ((((sinh . x) * (cosh . x2)) + ((cosh . x) * (sinh . x2))) / ((sinh . x) * (sinh . x2))) is V11() real ext-real M2( REAL )
(cosh . x) / (sinh . x) is V11() real ext-real M2( REAL )
((cosh . x) / (sinh . x)) * (cosh . x2) is V11() real ext-real M2( REAL )
(((cosh . x) / (sinh . x)) * (cosh . x2)) / (sinh . x2) is V11() real ext-real M2( REAL )
((((cosh . x) / (sinh . x)) * (cosh . x2)) / (sinh . x2)) + 1 is V11() real ext-real M2( REAL )
(((((cosh . x) / (sinh . x)) * (cosh . x2)) / (sinh . x2)) + 1) / ((((sinh . x) * (cosh . x2)) + ((cosh . x) * (sinh . x2))) / ((sinh . x) * (sinh . x2))) is V11() real ext-real M2( REAL )
(cosh . x2) / (sinh . x2) is V11() real ext-real M2( REAL )
((cosh . x) / (sinh . x)) * ((cosh . x2) / (sinh . x2)) is V11() real ext-real M2( REAL )
(((cosh . x) / (sinh . x)) * ((cosh . x2) / (sinh . x2))) + 1 is V11() real ext-real M2( REAL )
((((cosh . x) / (sinh . x)) * ((cosh . x2) / (sinh . x2))) + 1) / ((((sinh . x) * (cosh . x2)) + ((cosh . x) * (sinh . x2))) / ((sinh . x) * (sinh . x2))) is V11() real ext-real M2( REAL )
((sinh . x) * (cosh . x2)) / ((sinh . x) * (sinh . x2)) is V11() real ext-real M2( REAL )
((cosh . x) * (sinh . x2)) / ((sinh . x) * (sinh . x2)) is V11() real ext-real M2( REAL )
(((sinh . x) * (cosh . x2)) / ((sinh . x) * (sinh . x2))) + (((cosh . x) * (sinh . x2)) / ((sinh . x) * (sinh . x2))) is V11() real ext-real M2( REAL )
((((cosh . x) / (sinh . x)) * ((cosh . x2) / (sinh . x2))) + 1) / ((((sinh . x) * (cosh . x2)) / ((sinh . x) * (sinh . x2))) + (((cosh . x) * (sinh . x2)) / ((sinh . x) * (sinh . x2)))) is V11() real ext-real M2( REAL )
(sinh . x) / (sinh . x) is V11() real ext-real M2( REAL )
((sinh . x) / (sinh . x)) * (cosh . x2) is V11() real ext-real M2( REAL )
(((sinh . x) / (sinh . x)) * (cosh . x2)) / (sinh . x2) is V11() real ext-real M2( REAL )
((((sinh . x) / (sinh . x)) * (cosh . x2)) / (sinh . x2)) + (((cosh . x) * (sinh . x2)) / ((sinh . x) * (sinh . x2))) is V11() real ext-real M2( REAL )
((((cosh . x) / (sinh . x)) * ((cosh . x2) / (sinh . x2))) + 1) / (((((sinh . x) / (sinh . x)) * (cosh . x2)) / (sinh . x2)) + (((cosh . x) * (sinh . x2)) / ((sinh . x) * (sinh . x2)))) is V11() real ext-real M2( REAL )
((cosh . x) / (sinh . x)) * (sinh . x2) is V11() real ext-real M2( REAL )
(((cosh . x) / (sinh . x)) * (sinh . x2)) / (sinh . x2) is V11() real ext-real M2( REAL )
((((sinh . x) / (sinh . x)) * (cosh . x2)) / (sinh . x2)) + ((((cosh . x) / (sinh . x)) * (sinh . x2)) / (sinh . x2)) is V11() real ext-real M2( REAL )
((((cosh . x) / (sinh . x)) * ((cosh . x2) / (sinh . x2))) + 1) / (((((sinh . x) / (sinh . x)) * (cosh . x2)) / (sinh . x2)) + ((((cosh . x) / (sinh . x)) * (sinh . x2)) / (sinh . x2))) is V11() real ext-real M2( REAL )
1 * (cosh . x2) is V11() real ext-real M2( REAL )
(1 * (cosh . x2)) / (sinh . x2) is V11() real ext-real M2( REAL )
((1 * (cosh . x2)) / (sinh . x2)) + ((((cosh . x) / (sinh . x)) * (sinh . x2)) / (sinh . x2)) is V11() real ext-real M2( REAL )
((((cosh . x) / (sinh . x)) * ((cosh . x2) / (sinh . x2))) + 1) / (((1 * (cosh . x2)) / (sinh . x2)) + ((((cosh . x) / (sinh . x)) * (sinh . x2)) / (sinh . x2))) is V11() real ext-real M2( REAL )
((cosh . x2) / (sinh . x2)) + ((cosh . x) / (sinh . x)) is V11() real ext-real M2( REAL )
((((cosh . x) / (sinh . x)) * ((cosh . x2) / (sinh . x2))) + 1) / (((cosh . x2) / (sinh . x2)) + ((cosh . x) / (sinh . x))) is V11() real ext-real M2( REAL )
(cosh x) / (sinh . x) is V11() real ext-real M2( REAL )
((cosh x) / (sinh . x)) * ((cosh . x2) / (sinh . x2)) is V11() real ext-real M2( REAL )
(((cosh x) / (sinh . x)) * ((cosh . x2) / (sinh . x2))) + 1 is V11() real ext-real M2( REAL )
((((cosh x) / (sinh . x)) * ((cosh . x2) / (sinh . x2))) + 1) / (((cosh . x2) / (sinh . x2)) + ((cosh . x) / (sinh . x))) is V11() real ext-real M2( REAL )
(cosh x2) / (sinh . x2) is V11() real ext-real M2( REAL )
((cosh x) / (sinh . x)) * ((cosh x2) / (sinh . x2)) is V11() real ext-real M2( REAL )
(((cosh x) / (sinh . x)) * ((cosh x2) / (sinh . x2))) + 1 is V11() real ext-real M2( REAL )
((((cosh x) / (sinh . x)) * ((cosh x2) / (sinh . x2))) + 1) / (((cosh . x2) / (sinh . x2)) + ((cosh . x) / (sinh . x))) is V11() real ext-real M2( REAL )
((cosh x2) / (sinh . x2)) + ((cosh . x) / (sinh . x)) is V11() real ext-real M2( REAL )
((((cosh x) / (sinh . x)) * ((cosh x2) / (sinh . x2))) + 1) / (((cosh x2) / (sinh . x2)) + ((cosh . x) / (sinh . x))) is V11() real ext-real M2( REAL )
((cosh x2) / (sinh . x2)) + ((cosh x) / (sinh . x)) is V11() real ext-real M2( REAL )
((((cosh x) / (sinh . x)) * ((cosh x2) / (sinh . x2))) + 1) / (((cosh x2) / (sinh . x2)) + ((cosh x) / (sinh . x))) is V11() real ext-real M2( REAL )
((cosh x) / (sinh x)) * ((cosh x2) / (sinh . x2)) is V11() real ext-real M2( REAL )
(((cosh x) / (sinh x)) * ((cosh x2) / (sinh . x2))) + 1 is V11() real ext-real M2( REAL )
((((cosh x) / (sinh x)) * ((cosh x2) / (sinh . x2))) + 1) / (((cosh x2) / (sinh . x2)) + ((cosh x) / (sinh . x))) is V11() real ext-real M2( REAL )
((cosh x2) / (sinh x2)) + ((cosh x) / (sinh . x)) is V11() real ext-real M2( REAL )
((((cosh x) / (sinh x)) * ((cosh x2) / (sinh . x2))) + 1) / (((cosh x2) / (sinh x2)) + ((cosh x) / (sinh . x))) is V11() real ext-real M2( REAL )
((cosh x2) / (sinh x2)) + ((cosh x) / (sinh x)) is V11() real ext-real M2( REAL )
((((cosh x) / (sinh x)) * ((cosh x2) / (sinh . x2))) + 1) / (((cosh x2) / (sinh x2)) + ((cosh x) / (sinh x))) is V11() real ext-real M2( REAL )
((x) * (x2)) + 1 is V11() real ext-real M2( REAL )
(x2) + (x) is V11() real ext-real M2( REAL )
(((x) * (x2)) + 1) / ((x2) + (x)) is V11() real ext-real M2( REAL )
x is V11() real ext-real set
sinh x is V11() real ext-real M2( REAL )
(x) is V11() real ext-real M2( REAL )
cosh x is V11() real ext-real M2( REAL )
(cosh x) / (sinh x) is V11() real ext-real M2( REAL )
x2 is V11() real ext-real set
sinh x2 is V11() real ext-real M2( REAL )
x - x2 is V11() real ext-real set
((x - x2)) is V11() real ext-real M2( REAL )
cosh (x - x2) is V11() real ext-real M2( REAL )
sinh (x - x2) is V11() real ext-real M2( REAL )
(cosh (x - x2)) / (sinh (x - x2)) is V11() real ext-real M2( REAL )
(x2) is V11() real ext-real M2( REAL )
cosh x2 is V11() real ext-real M2( REAL )
(cosh x2) / (sinh x2) is V11() real ext-real M2( REAL )
(x) * (x2) is V11() real ext-real M2( REAL )
1 - ((x) * (x2)) is V11() real ext-real M2( REAL )
(x) - (x2) is V11() real ext-real M2( REAL )
(1 - ((x) * (x2))) / ((x) - (x2)) is V11() real ext-real M2( REAL )
sinh . x2 is V11() real ext-real M2( REAL )
- (sinh . x2) is V11() real ext-real M2( REAL )
- x2 is V11() real ext-real set
sinh . (- x2) is V11() real ext-real M2( REAL )
sinh (- x2) is V11() real ext-real M2( REAL )
x + (- x2) is V11() real ext-real set
((x + (- x2))) is V11() real ext-real M2( REAL )
cosh (x + (- x2)) is V11() real ext-real M2( REAL )
sinh (x + (- x2)) is V11() real ext-real M2( REAL )
(cosh (x + (- x2))) / (sinh (x + (- x2))) is V11() real ext-real M2( REAL )
((- x2)) is V11() real ext-real M2( REAL )
cosh (- x2) is V11() real ext-real M2( REAL )
(cosh (- x2)) / (sinh (- x2)) is V11() real ext-real M2( REAL )
(x) * ((- x2)) is V11() real ext-real M2( REAL )
1 + ((x) * ((- x2))) is V11() real ext-real M2( REAL )
(x) + ((- x2)) is V11() real ext-real M2( REAL )
(1 + ((x) * ((- x2)))) / ((x) + ((- x2))) is V11() real ext-real M2( REAL )
- (x2) is V11() real ext-real M2( REAL )
(x) * (- (x2)) is V11() real ext-real M2( REAL )
1 + ((x) * (- (x2))) is V11() real ext-real M2( REAL )
(1 + ((x) * (- (x2)))) / ((x) + ((- x2))) is V11() real ext-real M2( REAL )
(x) + (- (x2)) is V11() real ext-real M2( REAL )
(1 - ((x) * (x2))) / ((x) + (- (x2))) is V11() real ext-real M2( REAL )
x is V11() real ext-real set
sinh x is V11() real ext-real M2( REAL )
(x) is V11() real ext-real M2( REAL )
cosh x is V11() real ext-real M2( REAL )
(cosh x) / (sinh x) is V11() real ext-real M2( REAL )
x2 is V11() real ext-real set
sinh x2 is V11() real ext-real M2( REAL )
(x2) is V11() real ext-real M2( REAL )
cosh x2 is V11() real ext-real M2( REAL )
(cosh x2) / (sinh x2) is V11() real ext-real M2( REAL )
(x) + (x2) is V11() real ext-real M2( REAL )
x + x2 is V11() real ext-real set
sinh (x + x2) is V11() real ext-real M2( REAL )
(sinh x) * (sinh x2) is V11() real ext-real M2( REAL )
(sinh (x + x2)) / ((sinh x) * (sinh x2)) is V11() real ext-real M2( REAL )
(x) - (x2) is V11() real ext-real M2( REAL )
x - x2 is V11() real ext-real set
sinh (x - x2) is V11() real ext-real M2( REAL )
(sinh (x - x2)) / ((sinh x) * (sinh x2)) is V11() real ext-real M2( REAL )
- ((sinh (x - x2)) / ((sinh x) * (sinh x2))) is V11() real ext-real M2( REAL )
sinh . x is V11() real ext-real M2( REAL )
sinh . x2 is V11() real ext-real M2( REAL )
sinh . (x - x2) is V11() real ext-real M2( REAL )
(sinh . (x - x2)) / ((sinh x) * (sinh x2)) is V11() real ext-real M2( REAL )
- ((sinh . (x - x2)) / ((sinh x) * (sinh x2))) is V11() real ext-real M2( REAL )
(sinh . x) * (sinh x2) is V11() real ext-real M2( REAL )
(sinh . (x - x2)) / ((sinh . x) * (sinh x2)) is V11() real ext-real M2( REAL )
- ((sinh . (x - x2)) / ((sinh . x) * (sinh x2))) is V11() real ext-real M2( REAL )
(sinh . x) * (sinh . x2) is V11() real ext-real M2( REAL )
(sinh . (x - x2)) / ((sinh . x) * (sinh . x2)) is V11() real ext-real M2( REAL )
- ((sinh . (x - x2)) / ((sinh . x) * (sinh . x2))) is V11() real ext-real M2( REAL )
cosh . x2 is V11() real ext-real M2( REAL )
(sinh . x) * (cosh . x2) is V11() real ext-real M2( REAL )
cosh . x is V11() real ext-real M2( REAL )
(cosh . x) * (sinh . x2) is V11() real ext-real M2( REAL )
((sinh . x) * (cosh . x2)) - ((cosh . x) * (sinh . x2)) is V11() real ext-real M2( REAL )
(((sinh . x) * (cosh . x2)) - ((cosh . x) * (sinh . x2))) / ((sinh . x) * (sinh . x2)) is V11() real ext-real M2( REAL )
- ((((sinh . x) * (cosh . x2)) - ((cosh . x) * (sinh . x2))) / ((sinh . x) * (sinh . x2))) is V11() real ext-real M2( REAL )
((sinh . x) * (cosh . x2)) / ((sinh . x) * (sinh . x2)) is V11() real ext-real M2( REAL )
((cosh . x) * (sinh . x2)) / ((sinh . x) * (sinh . x2)) is V11() real ext-real M2( REAL )
(((sinh . x) * (cosh . x2)) / ((sinh . x) * (sinh . x2))) - (((cosh . x) * (sinh . x2)) / ((sinh . x) * (sinh . x2))) is V11() real ext-real M2( REAL )
- ((((sinh . x) * (cosh . x2)) / ((sinh . x) * (sinh . x2))) - (((cosh . x) * (sinh . x2)) / ((sinh . x) * (sinh . x2)))) is V11() real ext-real M2( REAL )
(sinh . x) / (sinh . x) is V11() real ext-real M2( REAL )
((sinh . x) / (sinh . x)) * (cosh . x2) is V11() real ext-real M2( REAL )
(((sinh . x) / (sinh . x)) * (cosh . x2)) / (sinh . x2) is V11() real ext-real M2( REAL )
((((sinh . x) / (sinh . x)) * (cosh . x2)) / (sinh . x2)) - (((cosh . x) * (sinh . x2)) / ((sinh . x) * (sinh . x2))) is V11() real ext-real M2( REAL )
- (((((sinh . x) / (sinh . x)) * (cosh . x2)) / (sinh . x2)) - (((cosh . x) * (sinh . x2)) / ((sinh . x) * (sinh . x2)))) is V11() real ext-real M2( REAL )
(sinh . x2) / (sinh . x2) is V11() real ext-real M2( REAL )
((sinh . x2) / (sinh . x2)) * (cosh . x) is V11() real ext-real M2( REAL )
(((sinh . x2) / (sinh . x2)) * (cosh . x)) / (sinh . x) is V11() real ext-real M2( REAL )
((((sinh . x) / (sinh . x)) * (cosh . x2)) / (sinh . x2)) - ((((sinh . x2) / (sinh . x2)) * (cosh . x)) / (sinh . x)) is V11() real ext-real M2( REAL )
- (((((sinh . x) / (sinh . x)) * (cosh . x2)) / (sinh . x2)) - ((((sinh . x2) / (sinh . x2)) * (cosh . x)) / (sinh . x))) is V11() real ext-real M2( REAL )
1 * (cosh . x2) is V11() real ext-real M2( REAL )
(1 * (cosh . x2)) / (sinh . x2) is V11() real ext-real M2( REAL )
((1 * (cosh . x2)) / (sinh . x2)) - ((((sinh . x2) / (sinh . x2)) * (cosh . x)) / (sinh . x)) is V11() real ext-real M2( REAL )
- (((1 * (cosh . x2)) / (sinh . x2)) - ((((sinh . x2) / (sinh . x2)) * (cosh . x)) / (sinh . x))) is V11() real ext-real M2( REAL )
(cosh . x2) / (sinh . x2) is V11() real ext-real M2( REAL )
1 * (cosh . x) is V11() real ext-real M2( REAL )
(1 * (cosh . x)) / (sinh . x) is V11() real ext-real M2( REAL )
((cosh . x2) / (sinh . x2)) - ((1 * (cosh . x)) / (sinh . x)) is V11() real ext-real M2( REAL )
- (((cosh . x2) / (sinh . x2)) - ((1 * (cosh . x)) / (sinh . x))) is V11() real ext-real M2( REAL )
(cosh x2) / (sinh . x2) is V11() real ext-real M2( REAL )
(cosh . x) / (sinh . x) is V11() real ext-real M2( REAL )
((cosh x2) / (sinh . x2)) - ((cosh . x) / (sinh . x)) is V11() real ext-real M2( REAL )
- (((cosh x2) / (sinh . x2)) - ((cosh . x) / (sinh . x))) is V11() real ext-real M2( REAL )
(cosh x) / (sinh . x) is V11() real ext-real M2( REAL )
((cosh x2) / (sinh . x2)) - ((cosh x) / (sinh . x)) is V11() real ext-real M2( REAL )
- (((cosh x2) / (sinh . x2)) - ((cosh x) / (sinh . x))) is V11() real ext-real M2( REAL )
((cosh x2) / (sinh x2)) - ((cosh x) / (sinh . x)) is V11() real ext-real M2( REAL )
- (((cosh x2) / (sinh x2)) - ((cosh x) / (sinh . x))) is V11() real ext-real M2( REAL )
(x2) - ((cosh x) / (sinh x)) is V11() real ext-real M2( REAL )
- ((x2) - ((cosh x) / (sinh x))) is V11() real ext-real M2( REAL )
sinh . (x + x2) is V11() real ext-real M2( REAL )
(sinh . (x + x2)) / ((sinh x) * (sinh x2)) is V11() real ext-real M2( REAL )
((sinh . x) * (cosh . x2)) + ((cosh . x) * (sinh . x2)) is V11() real ext-real M2( REAL )
(((sinh . x) * (cosh . x2)) + ((cosh . x) * (sinh . x2))) / ((sinh x) * (sinh x2)) is V11() real ext-real M2( REAL )
(((sinh . x) * (cosh . x2)) + ((cosh . x) * (sinh . x2))) / ((sinh . x) * (sinh x2)) is V11() real ext-real M2( REAL )
(((sinh . x) * (cosh . x2)) + ((cosh . x) * (sinh . x2))) / ((sinh . x) * (sinh . x2)) is V11() real ext-real M2( REAL )
(((sinh . x) * (cosh . x2)) / ((sinh . x) * (sinh . x2))) + (((cosh . x) * (sinh . x2)) / ((sinh . x) * (sinh . x2))) is V11() real ext-real M2( REAL )
((((sinh . x) / (sinh . x)) * (cosh . x2)) / (sinh . x2)) + (((cosh . x) * (sinh . x2)) / ((sinh . x) * (sinh . x2))) is V11() real ext-real M2( REAL )
((1 * (cosh . x2)) / (sinh . x2)) + (((cosh . x) * (sinh . x2)) / ((sinh . x) * (sinh . x2))) is V11() real ext-real M2( REAL )
((cosh . x) / (sinh . x)) * (sinh . x2) is V11() real ext-real M2( REAL )
(((cosh . x) / (sinh . x)) * (sinh . x2)) / (sinh . x2) is V11() real ext-real M2( REAL )
((cosh . x2) / (sinh . x2)) + ((((cosh . x) / (sinh . x)) * (sinh . x2)) / (sinh . x2)) is V11() real ext-real M2( REAL )
((cosh . x) / (sinh . x)) * ((sinh . x2) / (sinh . x2)) is V11() real ext-real M2( REAL )
((cosh . x2) / (sinh . x2)) + (((cosh . x) / (sinh . x)) * ((sinh . x2) / (sinh . x2))) is V11() real ext-real M2( REAL )
((cosh . x) / (sinh . x)) * 1 is V11() real ext-real M2( REAL )
((cosh . x2) / (sinh . x2)) + (((cosh . x) / (sinh . x)) * 1) is V11() real ext-real M2( REAL )
(cosh . x) / (sinh x) is V11() real ext-real M2( REAL )
((cosh . x2) / (sinh . x2)) + ((cosh . x) / (sinh x)) is V11() real ext-real M2( REAL )
(cosh . x2) / (sinh x2) is V11() real ext-real M2( REAL )
((cosh . x2) / (sinh x2)) + ((cosh . x) / (sinh x)) is V11() real ext-real M2( REAL )
((cosh x2) / (sinh x2)) + ((cosh . x) / (sinh x)) is V11() real ext-real M2( REAL )
(x2) + (x) is V11() real ext-real M2( REAL )
x is V11() real ext-real set
cosh . x is V11() real ext-real M2( REAL )
(cosh . x) ^2 is V11() real ext-real M2( REAL )
(cosh . x) * (cosh . x) is V11() real ext-real set
sinh . x is V11() real ext-real M2( REAL )
(sinh . x) ^2 is V11() real ext-real M2( REAL )
(sinh . x) * (sinh . x) is V11() real ext-real set
1 + ((sinh . x) ^2) is V11() real ext-real M2( REAL )
((cosh . x) ^2) - ((sinh . x) ^2) is V11() real ext-real M2( REAL )
(((cosh . x) ^2) - ((sinh . x) ^2)) + ((sinh . x) ^2) is V11() real ext-real M2( REAL )
x is V11() real ext-real set
cosh . x is V11() real ext-real M2( REAL )
(cosh . x) ^2 is V11() real ext-real M2( REAL )
(cosh . x) * (cosh . x) is V11() real ext-real set
((cosh . x) ^2) - 1 is V11() real ext-real M2( REAL )
sinh . x is V11() real ext-real M2( REAL )
(sinh . x) ^2 is V11() real ext-real M2( REAL )
(sinh . x) * (sinh . x) is V11() real ext-real set
((cosh . x) ^2) - ((sinh . x) ^2) is V11() real ext-real M2( REAL )
(((cosh . x) ^2) - ((sinh . x) ^2)) + ((sinh . x) ^2) is V11() real ext-real M2( REAL )
1 + ((sinh . x) ^2) is V11() real ext-real M2( REAL )
x is V11() real ext-real set
3 * x is V11() real ext-real M2( REAL )
sinh (3 * x) is V11() real ext-real M2( REAL )
sinh x is V11() real ext-real M2( REAL )
3 * (sinh x) is V11() real ext-real M2( REAL )
(sinh x) |^ 3 is V11() real ext-real M2( REAL )
4 * ((sinh x) |^ 3) is V11() real ext-real M2( REAL )
(3 * (sinh x)) + (4 * ((sinh x) |^ 3)) is V11() real ext-real M2( REAL )
x + x is V11() real ext-real set
(x + x) + x is V11() real ext-real set
sinh . ((x + x) + x) is V11() real ext-real M2( REAL )
2 * x is V11() real ext-real M2( REAL )
sinh . (2 * x) is V11() real ext-real M2( REAL )
cosh . x is V11() real ext-real M2( REAL )
(sinh . (2 * x)) * (cosh . x) is V11() real ext-real M2( REAL )
cosh . (2 * x) is V11() real ext-real M2( REAL )
sinh . x is V11() real ext-real M2( REAL )
(cosh . (2 * x)) * (sinh . x) is V11() real ext-real M2( REAL )
((sinh . (2 * x)) * (cosh . x)) + ((cosh . (2 * x)) * (sinh . x)) is V11() real ext-real M2( REAL )
2 * (sinh . x) is V11() real ext-real M2( REAL )
(2 * (sinh . x)) * (cosh . x) is V11() real ext-real M2( REAL )
((2 * (sinh . x)) * (cosh . x)) * (cosh . x) is V11() real ext-real M2( REAL )
(((2 * (sinh . x)) * (cosh . x)) * (cosh . x)) + ((cosh . (2 * x)) * (sinh . x)) is V11() real ext-real M2( REAL )
(cosh . x) ^2 is V11() real ext-real M2( REAL )
(cosh . x) * (cosh . x) is V11() real ext-real set
(2 * (sinh . x)) * ((cosh . x) ^2) is V11() real ext-real M2( REAL )
2 * ((cosh . x) ^2) is V11() real ext-real M2( REAL )
(2 * ((cosh . x) ^2)) - 1 is V11() real ext-real M2( REAL )
((2 * ((cosh . x) ^2)) - 1) * (sinh . x) is V11() real ext-real M2( REAL )
((2 * (sinh . x)) * ((cosh . x) ^2)) + (((2 * ((cosh . x) ^2)) - 1) * (sinh . x)) is V11() real ext-real M2( REAL )
(sinh . x) ^2 is V11() real ext-real M2( REAL )
(sinh . x) * (sinh . x) is V11() real ext-real set
1 + ((sinh . x) ^2) is V11() real ext-real M2( REAL )
(2 * (sinh . x)) * (1 + ((sinh . x) ^2)) is V11() real ext-real M2( REAL )
((2 * (sinh . x)) * (1 + ((sinh . x) ^2))) + (((2 * ((cosh . x) ^2)) - 1) * (sinh . x)) is V11() real ext-real M2( REAL )
2 * (1 + ((sinh . x) ^2)) is V11() real ext-real M2( REAL )
(2 * (1 + ((sinh . x) ^2))) - 1 is V11() real ext-real M2( REAL )
((2 * (1 + ((sinh . x) ^2))) - 1) * (sinh . x) is V11() real ext-real M2( REAL )
((2 * (sinh . x)) * (1 + ((sinh . x) ^2))) + (((2 * (1 + ((sinh . x) ^2))) - 1) * (sinh . x)) is V11() real ext-real M2( REAL )
2 + 2 is natural V11() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() M3( REAL , NAT )
(2 + 2) * (sinh . x) is V11() real ext-real M2( REAL )
((2 + 2) * (sinh . x)) * ((sinh . x) ^2) is V11() real ext-real M2( REAL )
(2 * (sinh . x)) + (((2 + 2) * (sinh . x)) * ((sinh . x) ^2)) is V11() real ext-real M2( REAL )
((2 * (sinh . x)) + (((2 + 2) * (sinh . x)) * ((sinh . x) ^2))) + (sinh . x) is V11() real ext-real M2( REAL )
(sinh . x) |^ 1 is V11() real ext-real M2( REAL )
4 * ((sinh . x) |^ 1) is V11() real ext-real M2( REAL )
(4 * ((sinh . x) |^ 1)) * ((sinh . x) ^2) is V11() real ext-real M2( REAL )
(2 * (sinh . x)) + ((4 * ((sinh . x) |^ 1)) * ((sinh . x) ^2)) is V11() real ext-real M2( REAL )
((2 * (sinh . x)) + ((4 * ((sinh . x) |^ 1)) * ((sinh . x) ^2))) + (sinh . x) is V11() real ext-real M2( REAL )
3 * (sinh . x) is V11() real ext-real M2( REAL )
((sinh . x) |^ 1) * (sinh . x) is V11() real ext-real M2( REAL )
(((sinh . x) |^ 1) * (sinh . x)) * (sinh . x) is V11() real ext-real M2( REAL )
4 * ((((sinh . x) |^ 1) * (sinh . x)) * (sinh . x)) is V11() real ext-real M2( REAL )
(3 * (sinh . x)) + (4 * ((((sinh . x) |^ 1) * (sinh . x)) * (sinh . x))) is V11() real ext-real M2( REAL )
1 + 1 is natural V11() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() M3( REAL , NAT )
(sinh . x) |^ (1 + 1) is V11() real ext-real M2( REAL )
((sinh . x) |^ (1 + 1)) * (sinh . x) is V11() real ext-real M2( REAL )
4 * (((sinh . x) |^ (1 + 1)) * (sinh . x)) is V11() real ext-real M2( REAL )
(3 * (sinh . x)) + (4 * (((sinh . x) |^ (1 + 1)) * (sinh . x))) is V11() real ext-real M2( REAL )
2 + 1 is natural V11() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() M3( REAL , NAT )
(sinh . x) |^ (2 + 1) is V11() real ext-real M2( REAL )
4 * ((sinh . x) |^ (2 + 1)) is V11() real ext-real M2( REAL )
(3 * (sinh . x)) + (4 * ((sinh . x) |^ (2 + 1))) is V11() real ext-real M2( REAL )
(sinh . x) |^ 3 is V11() real ext-real M2( REAL )
4 * ((sinh . x) |^ 3) is V11() real ext-real M2( REAL )
(3 * (sinh x)) + (4 * ((sinh . x) |^ 3)) is V11() real ext-real M2( REAL )
x is V11() real ext-real set
3 * x is V11() real ext-real M2( REAL )
cosh (3 * x) is V11() real ext-real M2( REAL )
cosh x is V11() real ext-real M2( REAL )
(cosh x) |^ 3 is V11() real ext-real M2( REAL )
4 * ((cosh x) |^ 3) is V11() real ext-real M2( REAL )
3 * (cosh x) is V11() real ext-real M2( REAL )
(4 * ((cosh x) |^ 3)) - (3 * (cosh x)) is V11() real ext-real M2( REAL )
x + x is V11() real ext-real set
(x + x) + x is V11() real ext-real set
cosh . ((x + x) + x) is V11() real ext-real M2( REAL )
2 * x is V11() real ext-real M2( REAL )
cosh . (2 * x) is V11() real ext-real M2( REAL )
cosh . x is V11() real ext-real M2( REAL )
(cosh . (2 * x)) * (cosh . x) is V11() real ext-real M2( REAL )
sinh . (2 * x) is V11() real ext-real M2( REAL )
sinh . x is V11() real ext-real M2( REAL )
(sinh . (2 * x)) * (sinh . x) is V11() real ext-real M2( REAL )
((cosh . (2 * x)) * (cosh . x)) + ((sinh . (2 * x)) * (sinh . x)) is V11() real ext-real M2( REAL )
(cosh . x) ^2 is V11() real ext-real M2( REAL )
(cosh . x) * (cosh . x) is V11() real ext-real set
2 * ((cosh . x) ^2) is V11() real ext-real M2( REAL )
(2 * ((cosh . x) ^2)) - 1 is V11() real ext-real M2( REAL )
((2 * ((cosh . x) ^2)) - 1) * (cosh . x) is V11() real ext-real M2( REAL )
(((2 * ((cosh . x) ^2)) - 1) * (cosh . x)) + ((sinh . (2 * x)) * (sinh . x)) is V11() real ext-real M2( REAL )
2 * (sinh . x) is V11() real ext-real M2( REAL )
(2 * (sinh . x)) * (cosh . x) is V11() real ext-real M2( REAL )
((2 * (sinh . x)) * (cosh . x)) * (sinh . x) is V11() real ext-real M2( REAL )
(((2 * ((cosh . x) ^2)) - 1) * (cosh . x)) + (((2 * (sinh . x)) * (cosh . x)) * (sinh . x)) is V11() real ext-real M2( REAL )
(sinh . x) ^2 is V11() real ext-real M2( REAL )
(sinh . x) * (sinh . x) is V11() real ext-real set
2 * ((sinh . x) ^2) is V11() real ext-real M2( REAL )
(2 * ((sinh . x) ^2)) * (cosh . x) is V11() real ext-real M2( REAL )
(((2 * ((cosh . x) ^2)) - 1) * (cosh . x)) + ((2 * ((sinh . x) ^2)) * (cosh . x)) is V11() real ext-real M2( REAL )
((cosh . x) ^2) - 1 is V11() real ext-real M2( REAL )
2 * (((cosh . x) ^2) - 1) is V11() real ext-real M2( REAL )
(2 * (((cosh . x) ^2) - 1)) * (cosh . x) is V11() real ext-real M2( REAL )
(((2 * ((cosh . x) ^2)) - 1) * (cosh . x)) + ((2 * (((cosh . x) ^2) - 1)) * (cosh . x)) is V11() real ext-real M2( REAL )
(cosh . x) * (cosh . x) is V11() real ext-real M2( REAL )
((cosh . x) * (cosh . x)) * (cosh . x) is V11() real ext-real M2( REAL )
4 * (((cosh . x) * (cosh . x)) * (cosh . x)) is V11() real ext-real M2( REAL )
3 * (cosh . x) is V11() real ext-real M2( REAL )
(4 * (((cosh . x) * (cosh . x)) * (cosh . x))) - (3 * (cosh . x)) is V11() real ext-real M2( REAL )
(cosh . x) |^ 1 is V11() real ext-real M2( REAL )
((cosh . x) |^ 1) * (cosh . x) is V11() real ext-real M2( REAL )
(((cosh . x) |^ 1) * (cosh . x)) * (cosh . x) is V11() real ext-real M2( REAL )
4 * ((((cosh . x) |^ 1) * (cosh . x)) * (cosh . x)) is V11() real ext-real M2( REAL )
(4 * ((((cosh . x) |^ 1) * (cosh . x)) * (cosh . x))) - (3 * (cosh . x)) is V11() real ext-real M2( REAL )
1 + 1 is natural V11() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() M3( REAL , NAT )
(cosh . x) |^ (1 + 1) is V11() real ext-real M2( REAL )
((cosh . x) |^ (1 + 1)) * (cosh . x) is V11() real ext-real M2( REAL )
4 * (((cosh . x) |^ (1 + 1)) * (cosh . x)) is V11() real ext-real M2( REAL )
(4 * (((cosh . x) |^ (1 + 1)) * (cosh . x))) - (3 * (cosh . x)) is V11() real ext-real M2( REAL )
2 + 1 is natural V11() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() M3( REAL , NAT )
(cosh . x) |^ (2 + 1) is V11() real ext-real M2( REAL )
4 * ((cosh . x) |^ (2 + 1)) is V11() real ext-real M2( REAL )
(4 * ((cosh . x) |^ (2 + 1))) - (3 * (cosh . x)) is V11() real ext-real M2( REAL )
(cosh . x) |^ 3 is V11() real ext-real M2( REAL )
4 * ((cosh . x) |^ 3) is V11() real ext-real M2( REAL )
(4 * ((cosh . x) |^ 3)) - (3 * (cosh x)) is V11() real ext-real M2( REAL )
x is V11() real ext-real set
sinh x is V11() real ext-real M2( REAL )
2 * x is V11() real ext-real M2( REAL )
((2 * x)) is V11() real ext-real M2( REAL )
cosh (2 * x) is V11() real ext-real M2( REAL )
sinh (2 * x) is V11() real ext-real M2( REAL )
(cosh (2 * x)) / (sinh (2 * x)) is V11() real ext-real M2( REAL )
(x) is V11() real ext-real M2( REAL )
cosh x is V11() real ext-real M2( REAL )
(cosh x) / (sinh x) is V11() real ext-real M2( REAL )
(x) ^2 is V11() real ext-real M2( REAL )
(x) * (x) is V11() real ext-real set
1 + ((x) ^2) is V11() real ext-real M2( REAL )
2 * (x) is V11() real ext-real M2( REAL )
(1 + ((x) ^2)) / (2 * (x)) is V11() real ext-real M2( REAL )
sinh . x is V11() real ext-real M2( REAL )
(sinh . x) ^2 is V11() real ext-real M2( REAL )
(sinh . x) * (sinh . x) is V11() real ext-real set
cosh . (2 * x) is V11() real ext-real M2( REAL )
(cosh . (2 * x)) / (sinh (2 * x)) is V11() real ext-real M2( REAL )
sinh . (2 * x) is V11() real ext-real M2( REAL )
(cosh . (2 * x)) / (sinh . (2 * x)) is V11() real ext-real M2( REAL )
cosh . x is V11() real ext-real M2( REAL )
(cosh . x) ^2 is V11() real ext-real M2( REAL )
(cosh . x) * (cosh . x) is V11() real ext-real set
2 * ((cosh . x) ^2) is V11() real ext-real M2( REAL )
(2 * ((cosh . x) ^2)) - 1 is V11() real ext-real M2( REAL )
((2 * ((cosh . x) ^2)) - 1) / (sinh . (2 * x)) is V11() real ext-real M2( REAL )
2 * (sinh . x) is V11() real ext-real M2( REAL )
(2 * (sinh . x)) * (cosh . x) is V11() real ext-real M2( REAL )
((2 * ((cosh . x) ^2)) - 1) / ((2 * (sinh . x)) * (cosh . x)) is V11() real ext-real M2( REAL )
((2 * ((cosh . x) ^2)) - 1) / ((sinh . x) ^2) is V11() real ext-real M2( REAL )
((2 * (sinh . x)) * (cosh . x)) / ((sinh . x) ^2) is V11() real ext-real M2( REAL )
(((2 * ((cosh . x) ^2)) - 1) / ((sinh . x) ^2)) / (((2 * (sinh . x)) * (cosh . x)) / ((sinh . x) ^2)) is V11() real ext-real M2( REAL )
((cosh . x) ^2) - ((sinh . x) ^2) is V11() real ext-real M2( REAL )
(2 * ((cosh . x) ^2)) - (((cosh . x) ^2) - ((sinh . x) ^2)) is V11() real ext-real M2( REAL )
((2 * ((cosh . x) ^2)) - (((cosh . x) ^2) - ((sinh . x) ^2))) / ((sinh . x) ^2) is V11() real ext-real M2( REAL )
(((2 * ((cosh . x) ^2)) - (((cosh . x) ^2) - ((sinh . x) ^2))) / ((sinh . x) ^2)) / (((2 * (sinh . x)) * (cosh . x)) / ((sinh . x) ^2)) is V11() real ext-real M2( REAL )
2 - 1 is V11() real ext-real M2( REAL )
(2 - 1) * ((cosh . x) ^2) is V11() real ext-real M2( REAL )
((2 - 1) * ((cosh . x) ^2)) + ((sinh . x) ^2) is V11() real ext-real M2( REAL )
(((2 - 1) * ((cosh . x) ^2)) + ((sinh . x) ^2)) / ((sinh . x) ^2) is V11() real ext-real M2( REAL )
((((2 - 1) * ((cosh . x) ^2)) + ((sinh . x) ^2)) / ((sinh . x) ^2)) / (((2 * (sinh . x)) * (cosh . x)) / ((sinh . x) ^2)) is V11() real ext-real M2( REAL )
((cosh . x) ^2) / ((sinh . x) ^2) is V11() real ext-real M2( REAL )
((sinh . x) ^2) / ((sinh . x) ^2) is V11() real ext-real M2( REAL )
(((cosh . x) ^2) / ((sinh . x) ^2)) + (((sinh . x) ^2) / ((sinh . x) ^2)) is V11() real ext-real M2( REAL )
((((cosh . x) ^2) / ((sinh . x) ^2)) + (((sinh . x) ^2) / ((sinh . x) ^2))) / (((2 * (sinh . x)) * (cosh . x)) / ((sinh . x) ^2)) is V11() real ext-real M2( REAL )
(cosh . x) / (sinh . x) is V11() real ext-real M2( REAL )
((cosh . x) / (sinh . x)) ^2 is V11() real ext-real M2( REAL )
((cosh . x) / (sinh . x)) * ((cosh . x) / (sinh . x)) is V11() real ext-real set
(((cosh . x) / (sinh . x)) ^2) + (((sinh . x) ^2) / ((sinh . x) ^2)) is V11() real ext-real M2( REAL )
((((cosh . x) / (sinh . x)) ^2) + (((sinh . x) ^2) / ((sinh . x) ^2))) / (((2 * (sinh . x)) * (cosh . x)) / ((sinh . x) ^2)) is V11() real ext-real M2( REAL )
(sinh . x) / (sinh . x) is V11() real ext-real M2( REAL )
((sinh . x) / (sinh . x)) ^2 is V11() real ext-real M2( REAL )
((sinh . x) / (sinh . x)) * ((sinh . x) / (sinh . x)) is V11() real ext-real set
(((cosh . x) / (sinh . x)) ^2) + (((sinh . x) / (sinh . x)) ^2) is V11() real ext-real M2( REAL )
((((cosh . x) / (sinh . x)) ^2) + (((sinh . x) / (sinh . x)) ^2)) / (((2 * (sinh . x)) * (cosh . x)) / ((sinh . x) ^2)) is V11() real ext-real M2( REAL )
1 ^2 is V11() real ext-real M2( REAL )
1 * 1 is V11() real ext-real set
(((cosh . x) / (sinh . x)) ^2) + (1 ^2) is V11() real ext-real M2( REAL )
2 * (cosh . x) is V11() real ext-real M2( REAL )
(2 * (cosh . x)) * (sinh . x) is V11() real ext-real M2( REAL )
(sinh . x) * (sinh . x) is V11() real ext-real M2( REAL )
((2 * (cosh . x)) * (sinh . x)) / ((sinh . x) * (sinh . x)) is V11() real ext-real M2( REAL )
((((cosh . x) / (sinh . x)) ^2) + (1 ^2)) / (((2 * (cosh . x)) * (sinh . x)) / ((sinh . x) * (sinh . x))) is V11() real ext-real M2( REAL )
(((cosh . x) / (sinh . x)) ^2) + 1 is V11() real ext-real M2( REAL )
((2 * (cosh . x)) * (sinh . x)) / (sinh . x) is V11() real ext-real M2( REAL )
(((2 * (cosh . x)) * (sinh . x)) / (sinh . x)) / (sinh . x) is V11() real ext-real M2( REAL )
((((cosh . x) / (sinh . x)) ^2) + 1) / ((((2 * (cosh . x)) * (sinh . x)) / (sinh . x)) / (sinh . x)) is V11() real ext-real M2( REAL )
(2 * (cosh . x)) / (sinh . x) is V11() real ext-real M2( REAL )
((((cosh . x) / (sinh . x)) ^2) + 1) / ((2 * (cosh . x)) / (sinh . x)) is V11() real ext-real M2( REAL )
2 * ((cosh . x) / (sinh . x)) is V11() real ext-real M2( REAL )
((((cosh . x) / (sinh . x)) ^2) + 1) / (2 * ((cosh . x) / (sinh . x))) is V11() real ext-real M2( REAL )
(cosh x) / (sinh . x) is V11() real ext-real M2( REAL )
((cosh x) / (sinh . x)) ^2 is V11() real ext-real M2( REAL )
((cosh x) / (sinh . x)) * ((cosh x) / (sinh . x)) is V11() real ext-real set
(((cosh x) / (sinh . x)) ^2) + 1 is V11() real ext-real M2( REAL )
((((cosh x) / (sinh . x)) ^2) + 1) / (2 * ((cosh . x) / (sinh . x))) is V11() real ext-real M2( REAL )
2 * ((cosh x) / (sinh . x)) is V11() real ext-real M2( REAL )
((((cosh x) / (sinh . x)) ^2) + 1) / (2 * ((cosh x) / (sinh . x))) is V11() real ext-real M2( REAL )
((cosh x) / (sinh x)) ^2 is V11() real ext-real M2( REAL )
((cosh x) / (sinh x)) * ((cosh x) / (sinh x)) is V11() real ext-real set
(((cosh x) / (sinh x)) ^2) + 1 is V11() real ext-real M2( REAL )
((((cosh x) / (sinh x)) ^2) + 1) / (2 * ((cosh x) / (sinh . x))) is V11() real ext-real M2( REAL )
((x) ^2) + 1 is V11() real ext-real M2( REAL )
2 * ((cosh x) / (sinh x)) is V11() real ext-real M2( REAL )
(((x) ^2) + 1) / (2 * ((cosh x) / (sinh x))) is V11() real ext-real M2( REAL )
x is V11() real ext-real set
sinh x is V11() real ext-real M2( REAL )
- x is V11() real ext-real set
x + (- x) is V11() real ext-real set
0 + (- x) is V11() real ext-real M2( REAL )
exp_R . (- x) is V11() real ext-real M2( REAL )
exp_R . x is V11() real ext-real M2( REAL )
1 - 1 is V11() real ext-real M2( REAL )
(exp_R . x) - (exp_R . (- x)) is V11() real ext-real M2( REAL )
((exp_R . x) - (exp_R . (- x))) / 2 is V11() real ext-real M2( REAL )
sinh . x is V11() real ext-real M2( REAL )
x is V11() real ext-real set
sinh x is V11() real ext-real M2( REAL )
x is V11() real ext-real set
sinh x is V11() real ext-real M2( REAL )
- x is V11() real ext-real set
exp_R . (- x) is V11() real ext-real M2( REAL )
exp_R . x is V11() real ext-real M2( REAL )
(exp_R . x) - (exp_R . (- x)) is V11() real ext-real M2( REAL )
1 - 1 is V11() real ext-real M2( REAL )
((exp_R . x) - (exp_R . (- x))) / 2 is V11() real ext-real M2( REAL )
sinh . x is V11() real ext-real M2( REAL )
x is V11() real ext-real set
x / 2 is V11() real ext-real M2( REAL )
cosh (x / 2) is V11() real ext-real M2( REAL )
cosh x is V11() real ext-real M2( REAL )
(cosh x) + 1 is V11() real ext-real M2( REAL )
((cosh x) + 1) / 2 is V11() real ext-real M2( REAL )
sqrt (((cosh x) + 1) / 2) is V11() real ext-real M2( REAL )
cosh . (x / 2) is V11() real ext-real M2( REAL )
2 * (x / 2) is V11() real ext-real M2( REAL )
cosh . (2 * (x / 2)) is V11() real ext-real M2( REAL )
(cosh . (2 * (x / 2))) + 1 is V11() real ext-real M2( REAL )
((cosh . (2 * (x / 2))) + 1) / 2 is V11() real ext-real M2( REAL )
sqrt (((cosh . (2 * (x / 2))) + 1) / 2) is V11() real ext-real M2( REAL )
(cosh . (x / 2)) ^2 is V11() real ext-real M2( REAL )
(cosh . (x / 2)) * (cosh . (x / 2)) is V11() real ext-real set
2 * ((cosh . (x / 2)) ^2) is V11() real ext-real M2( REAL )
(2 * ((cosh . (x / 2)) ^2)) - 1 is V11() real ext-real M2( REAL )
((2 * ((cosh . (x / 2)) ^2)) - 1) + 1 is V11() real ext-real M2( REAL )
(((2 * ((cosh . (x / 2)) ^2)) - 1) + 1) / 2 is V11() real ext-real M2( REAL )
sqrt ((((2 * ((cosh . (x / 2)) ^2)) - 1) + 1) / 2) is V11() real ext-real M2( REAL )
x is V11() real ext-real set
x / 2 is V11() real ext-real M2( REAL )
sinh (x / 2) is V11() real ext-real M2( REAL )
tanh (x / 2) is V11() real ext-real M2( REAL )
cosh x is V11() real ext-real M2( REAL )
(cosh x) - 1 is V11() real ext-real M2( REAL )
sinh x is V11() real ext-real M2( REAL )
((cosh x) - 1) / (sinh x) is V11() real ext-real M2( REAL )
sinh . (x / 2) is V11() real ext-real M2( REAL )
2 * (sinh . (x / 2)) is V11() real ext-real M2( REAL )
2 * (x / 2) is V11() real ext-real M2( REAL )
cosh . (2 * (x / 2)) is V11() real ext-real M2( REAL )
(cosh . (2 * (x / 2))) - 1 is V11() real ext-real M2( REAL )
sinh (2 * (x / 2)) is V11() real ext-real M2( REAL )
((cosh . (2 * (x / 2))) - 1) / (sinh (2 * (x / 2))) is V11() real ext-real M2( REAL )
cosh . (x / 2) is V11() real ext-real M2( REAL )
(cosh . (x / 2)) ^2 is V11() real ext-real M2( REAL )
(cosh . (x / 2)) * (cosh . (x / 2)) is V11() real ext-real set
2 * ((cosh . (x / 2)) ^2) is V11() real ext-real M2( REAL )
(2 * ((cosh . (x / 2)) ^2)) - 1 is V11() real ext-real M2( REAL )
((2 * ((cosh . (x / 2)) ^2)) - 1) - 1 is V11() real ext-real M2( REAL )
(((2 * ((cosh . (x / 2)) ^2)) - 1) - 1) / (sinh (2 * (x / 2))) is V11() real ext-real M2( REAL )
((cosh . (x / 2)) ^2) - 1 is V11() real ext-real M2( REAL )
2 * (((cosh . (x / 2)) ^2) - 1) is V11() real ext-real M2( REAL )
(2 * (((cosh . (x / 2)) ^2) - 1)) / (sinh (2 * (x / 2))) is V11() real ext-real M2( REAL )
(sinh . (x / 2)) ^2 is V11() real ext-real M2( REAL )
(sinh . (x / 2)) * (sinh . (x / 2)) is V11() real ext-real set
2 * ((sinh . (x / 2)) ^2) is V11() real ext-real M2( REAL )
(2 * ((sinh . (x / 2)) ^2)) / (sinh (2 * (x / 2))) is V11() real ext-real M2( REAL )
sinh . (2 * (x / 2)) is V11() real ext-real M2( REAL )
(2 * ((sinh . (x / 2)) ^2)) / (sinh . (2 * (x / 2))) is V11() real ext-real M2( REAL )
(2 * (sinh . (x / 2))) * (sinh . (x / 2)) is V11() real ext-real M2( REAL )
(2 * (sinh . (x / 2))) * (cosh . (x / 2)) is V11() real ext-real M2( REAL )
((2 * (sinh . (x / 2))) * (sinh . (x / 2))) / ((2 * (sinh . (x / 2))) * (cosh . (x / 2))) is V11() real ext-real M2( REAL )
(sinh . (x / 2)) / (cosh . (x / 2)) is V11() real ext-real M2( REAL )
tanh . (x / 2) is V11() real ext-real M2( REAL )
x is V11() real ext-real set
x / 2 is V11() real ext-real M2( REAL )
cosh (x / 2) is V11() real ext-real M2( REAL )
tanh (x / 2) is V11() real ext-real M2( REAL )
sinh x is V11() real ext-real M2( REAL )
cosh x is V11() real ext-real M2( REAL )
(cosh x) + 1 is V11() real ext-real M2( REAL )
(sinh x) / ((cosh x) + 1) is V11() real ext-real M2( REAL )
cosh . (x / 2) is V11() real ext-real M2( REAL )
2 * (cosh . (x / 2)) is V11() real ext-real M2( REAL )
2 * (x / 2) is V11() real ext-real M2( REAL )
sinh . (2 * (x / 2)) is V11() real ext-real M2( REAL )
cosh (2 * (x / 2)) is V11() real ext-real M2( REAL )
(cosh (2 * (x / 2))) + 1 is V11() real ext-real M2( REAL )
(sinh . (2 * (x / 2))) / ((cosh (2 * (x / 2))) + 1) is V11() real ext-real M2( REAL )
cosh . (2 * (x / 2)) is V11() real ext-real M2( REAL )
(cosh . (2 * (x / 2))) + 1 is V11() real ext-real M2( REAL )
(sinh . (2 * (x / 2))) / ((cosh . (2 * (x / 2))) + 1) is V11() real ext-real M2( REAL )
sinh . (x / 2) is V11() real ext-real M2( REAL )
2 * (sinh . (x / 2)) is V11() real ext-real M2( REAL )
(2 * (sinh . (x / 2))) * (cosh . (x / 2)) is V11() real ext-real M2( REAL )
((2 * (sinh . (x / 2))) * (cosh . (x / 2))) / ((cosh . (2 * (x / 2))) + 1) is V11() real ext-real M2( REAL )
(cosh . (x / 2)) ^2 is V11() real ext-real M2( REAL )
(cosh . (x / 2)) * (cosh . (x / 2)) is V11() real ext-real set
2 * ((cosh . (x / 2)) ^2) is V11() real ext-real M2( REAL )
(2 * ((cosh . (x / 2)) ^2)) - 1 is V11() real ext-real M2( REAL )
((2 * ((cosh . (x / 2)) ^2)) - 1) + 1 is V11() real ext-real M2( REAL )
((2 * (sinh . (x / 2))) * (cosh . (x / 2))) / (((2 * ((cosh . (x / 2)) ^2)) - 1) + 1) is V11() real ext-real M2( REAL )
(2 * (cosh . (x / 2))) * (sinh . (x / 2)) is V11() real ext-real M2( REAL )
(2 * (cosh . (x / 2))) * (cosh . (x / 2)) is V11() real ext-real M2( REAL )
((2 * (cosh . (x / 2))) * (sinh . (x / 2))) / ((2 * (cosh . (x / 2))) * (cosh . (x / 2))) is V11() real ext-real M2( REAL )
(sinh . (x / 2)) / (cosh . (x / 2)) is V11() real ext-real M2( REAL )
tanh . (x / 2) is V11() real ext-real M2( REAL )
x is V11() real ext-real set
x / 2 is V11() real ext-real M2( REAL )
sinh (x / 2) is V11() real ext-real M2( REAL )
((x / 2)) is V11() real ext-real M2( REAL )
cosh (x / 2) is V11() real ext-real M2( REAL )
(cosh (x / 2)) / (sinh (x / 2)) is V11() real ext-real M2( REAL )
sinh x is V11() real ext-real M2( REAL )
cosh x is V11() real ext-real M2( REAL )
(cosh x) - 1 is V11() real ext-real M2( REAL )
(sinh x) / ((cosh x) - 1) is V11() real ext-real M2( REAL )
sinh . (x / 2) is V11() real ext-real M2( REAL )
2 * (sinh . (x / 2)) is V11() real ext-real M2( REAL )
2 * (x / 2) is V11() real ext-real M2( REAL )
sinh . (2 * (x / 2)) is V11() real ext-real M2( REAL )
cosh (2 * (x / 2)) is V11() real ext-real M2( REAL )
(cosh (2 * (x / 2))) - 1 is V11() real ext-real M2( REAL )
(sinh . (2 * (x / 2))) / ((cosh (2 * (x / 2))) - 1) is V11() real ext-real M2( REAL )
cosh . (2 * (x / 2)) is V11() real ext-real M2( REAL )
(cosh . (2 * (x / 2))) - 1 is V11() real ext-real M2( REAL )
(sinh . (2 * (x / 2))) / ((cosh . (2 * (x / 2))) - 1) is V11() real ext-real M2( REAL )
cosh . (x / 2) is V11() real ext-real M2( REAL )
(2 * (sinh . (x / 2))) * (cosh . (x / 2)) is V11() real ext-real M2( REAL )
((2 * (sinh . (x / 2))) * (cosh . (x / 2))) / ((cosh . (2 * (x / 2))) - 1) is V11() real ext-real M2( REAL )
(cosh . (x / 2)) ^2 is V11() real ext-real M2( REAL )
(cosh . (x / 2)) * (cosh . (x / 2)) is V11() real ext-real set
2 * ((cosh . (x / 2)) ^2) is V11() real ext-real M2( REAL )
(2 * ((cosh . (x / 2)) ^2)) - 1 is V11() real ext-real M2( REAL )
((2 * ((cosh . (x / 2)) ^2)) - 1) - 1 is V11() real ext-real M2( REAL )
((2 * (sinh . (x / 2))) * (cosh . (x / 2))) / (((2 * ((cosh . (x / 2)) ^2)) - 1) - 1) is V11() real ext-real M2( REAL )
((cosh . (x / 2)) ^2) - 1 is V11() real ext-real M2( REAL )
2 * (((cosh . (x / 2)) ^2) - 1) is V11() real ext-real M2( REAL )
((2 * (sinh . (x / 2))) * (cosh . (x / 2))) / (2 * (((cosh . (x / 2)) ^2) - 1)) is V11() real ext-real M2( REAL )
(sinh . (x / 2)) ^2 is V11() real ext-real M2( REAL )
(sinh . (x / 2)) * (sinh . (x / 2)) is V11() real ext-real set
2 * ((sinh . (x / 2)) ^2) is V11() real ext-real M2( REAL )
((2 * (sinh . (x / 2))) * (cosh . (x / 2))) / (2 * ((sinh . (x / 2)) ^2)) is V11() real ext-real M2( REAL )
(2 * (sinh . (x / 2))) * (sinh . (x / 2)) is V11() real ext-real M2( REAL )
((2 * (sinh . (x / 2))) * (cosh . (x / 2))) / ((2 * (sinh . (x / 2))) * (sinh . (x / 2))) is V11() real ext-real M2( REAL )
(cosh . (x / 2)) / (sinh . (x / 2)) is V11() real ext-real M2( REAL )
(cosh (x / 2)) / (sinh . (x / 2)) is V11() real ext-real M2( REAL )
x is V11() real ext-real set
x / 2 is V11() real ext-real M2( REAL )
cosh (x / 2) is V11() real ext-real M2( REAL )
((x / 2)) is V11() real ext-real M2( REAL )
sinh (x / 2) is V11() real ext-real M2( REAL )
(cosh (x / 2)) / (sinh (x / 2)) is V11() real ext-real M2( REAL )
cosh x is V11() real ext-real M2( REAL )
(cosh x) + 1 is V11() real ext-real M2( REAL )
sinh x is V11() real ext-real M2( REAL )
((cosh x) + 1) / (sinh x) is V11() real ext-real M2( REAL )
cosh . (x / 2) is V11() real ext-real M2( REAL )
2 * (cosh . (x / 2)) is V11() real ext-real M2( REAL )
2 * (x / 2) is V11() real ext-real M2( REAL )
cosh . (2 * (x / 2)) is V11() real ext-real M2( REAL )
(cosh . (2 * (x / 2))) + 1 is V11() real ext-real M2( REAL )
sinh (2 * (x / 2)) is V11() real ext-real M2( REAL )
((cosh . (2 * (x / 2))) + 1) / (sinh (2 * (x / 2))) is V11() real ext-real M2( REAL )
(cosh . (x / 2)) ^2 is V11() real ext-real M2( REAL )
(cosh . (x / 2)) * (cosh . (x / 2)) is V11() real ext-real set
2 * ((cosh . (x / 2)) ^2) is V11() real ext-real M2( REAL )
(2 * ((cosh . (x / 2)) ^2)) - 1 is V11() real ext-real M2( REAL )
((2 * ((cosh . (x / 2)) ^2)) - 1) + 1 is V11() real ext-real M2( REAL )
(((2 * ((cosh . (x / 2)) ^2)) - 1) + 1) / (sinh (2 * (x / 2))) is V11() real ext-real M2( REAL )
sinh . (2 * (x / 2)) is V11() real ext-real M2( REAL )
(2 * ((cosh . (x / 2)) ^2)) / (sinh . (2 * (x / 2))) is V11() real ext-real M2( REAL )
(cosh . (x / 2)) * (cosh . (x / 2)) is V11() real ext-real M2( REAL )
2 * ((cosh . (x / 2)) * (cosh . (x / 2))) is V11() real ext-real M2( REAL )
sinh . (x / 2) is V11() real ext-real M2( REAL )
2 * (sinh . (x / 2)) is V11() real ext-real M2( REAL )
(2 * (sinh . (x / 2))) * (cosh . (x / 2)) is V11() real ext-real M2( REAL )
(2 * ((cosh . (x / 2)) * (cosh . (x / 2)))) / ((2 * (sinh . (x / 2))) * (cosh . (x / 2))) is V11() real ext-real M2( REAL )
(2 * (cosh . (x / 2))) * (cosh . (x / 2)) is V11() real ext-real M2( REAL )
(2 * (cosh . (x / 2))) * (sinh . (x / 2)) is V11() real ext-real M2( REAL )
((2 * (cosh . (x / 2))) * (cosh . (x / 2))) / ((2 * (cosh . (x / 2))) * (sinh . (x / 2))) is V11() real ext-real M2( REAL )
(cosh . (x / 2)) / (sinh . (x / 2)) is V11() real ext-real M2( REAL )
(cosh (x / 2)) / (sinh . (x / 2)) is V11() real ext-real M2( REAL )