:: ANALOAF semantic presentation

REAL is V16() V17() V18() V22() set
NAT is V16() V17() V18() V19() V20() V21() V22() M2( bool REAL)
bool REAL is non empty set
NAT is V16() V17() V18() V19() V20() V21() V22() set
bool NAT is non empty set
bool NAT is non empty set
{} is empty trivial V16() V17() V18() V19() V20() V21() V22() set
1 is V1() V2() V3() non empty V13() V14() V15() V16() V17() V18() V19() V20() V21() M3( REAL , NAT )
0 is V1() V2() V3() empty trivial V13() V14() V15() V16() V17() V18() V19() V20() V21() V22() M3( REAL , NAT )
- 1 is V1() V14() V15() M2( REAL )
K44(0) is V14() set

the carrier of V is non empty set

the carrier of V is non empty set
S is M2( the carrier of V)
v is M2( the carrier of V)
S - v is M2( the carrier of V)
- v is M2( the carrier of V)
K176(V,S,(- v)) is M2( the carrier of V)
b is M2( the carrier of V)
v - b is M2( the carrier of V)
- b is M2( the carrier of V)
K176(V,v,(- b)) is M2( the carrier of V)
(S - v) + (v - b) is M2( the carrier of V)
S - b is M2( the carrier of V)
K176(V,S,(- b)) is M2( the carrier of V)
v - (v - b) is M2( the carrier of V)
- (v - b) is M2( the carrier of V)
K176(V,v,(- (v - b))) is M2( the carrier of V)
S - (v - (v - b)) is M2( the carrier of V)
- (v - (v - b)) is M2( the carrier of V)
K176(V,S,(- (v - (v - b)))) is M2( the carrier of V)
v - v is M2( the carrier of V)
K176(V,v,(- v)) is M2( the carrier of V)
(v - v) + b is M2( the carrier of V)
S - ((v - v) + b) is M2( the carrier of V)
- ((v - v) + b) is M2( the carrier of V)
K176(V,S,(- ((v - v) + b))) is M2( the carrier of V)
0. V is V59(V) M2( the carrier of V)
the ZeroF of V is M2( the carrier of V)
(0. V) + b is M2( the carrier of V)
S - ((0. V) + b) is M2( the carrier of V)
- ((0. V) + b) is M2( the carrier of V)
K176(V,S,(- ((0. V) + b))) is M2( the carrier of V)

the carrier of V is non empty set
S is M2( the carrier of V)
v is M2( the carrier of V)
S + v is M2( the carrier of V)
b is M2( the carrier of V)
b - v is M2( the carrier of V)
- v is M2( the carrier of V)
K176(V,b,(- v)) is M2( the carrier of V)
c is M2( the carrier of V)
b + c is M2( the carrier of V)
S - c is M2( the carrier of V)
- c is M2( the carrier of V)
K176(V,S,(- c)) is M2( the carrier of V)
0. V is V59(V) M2( the carrier of V)
the ZeroF of V is M2( the carrier of V)
S + (0. V) is M2( the carrier of V)
(S + (0. V)) - c is M2( the carrier of V)
K176(V,(S + (0. V)),(- c)) is M2( the carrier of V)
v - v is M2( the carrier of V)
K176(V,v,(- v)) is M2( the carrier of V)
S + (v - v) is M2( the carrier of V)
(S + (v - v)) - c is M2( the carrier of V)
K176(V,(S + (v - v)),(- c)) is M2( the carrier of V)
(b + c) + (- v) is M2( the carrier of V)
((b + c) + (- v)) - c is M2( the carrier of V)
K176(V,((b + c) + (- v)),(- c)) is M2( the carrier of V)
(b + c) - c is M2( the carrier of V)
K176(V,(b + c),(- c)) is M2( the carrier of V)
(- v) + ((b + c) - c) is M2( the carrier of V)

the carrier of V is non empty set
S is M2( the carrier of V)
v is M2( the carrier of V)
S - v is M2( the carrier of V)
- v is M2( the carrier of V)
K176(V,S,(- v)) is M2( the carrier of V)
v - S is M2( the carrier of V)
- S is M2( the carrier of V)
K176(V,v,(- S)) is M2( the carrier of V)
b is V1() V14() V15() M2( REAL )
b * (S - v) is M2( the carrier of V)
b * (v - S) is M2( the carrier of V)
- (b * (v - S)) is M2( the carrier of V)
(b * (v - S)) + (b * (S - v)) is M2( the carrier of V)
- (v - S) is M2( the carrier of V)
b * (- (v - S)) is M2( the carrier of V)
(b * (v - S)) + (b * (- (v - S))) is M2( the carrier of V)
(b * (v - S)) - (b * (v - S)) is M2( the carrier of V)
K176(V,(b * (v - S)),(- (b * (v - S)))) is M2( the carrier of V)
0. V is V59(V) M2( the carrier of V)
the ZeroF of V is M2( the carrier of V)

the carrier of V is non empty set
S is M2( the carrier of V)
v is M2( the carrier of V)
S - v is M2( the carrier of V)
- v is M2( the carrier of V)
K176(V,S,(- v)) is M2( the carrier of V)
v - S is M2( the carrier of V)
- S is M2( the carrier of V)
K176(V,v,(- S)) is M2( the carrier of V)
b is V1() V14() V15() M2( REAL )
c is V1() V14() V15() M2( REAL )
b - c is V1() V14() V15() M2( REAL )
(b - c) * (S - v) is M2( the carrier of V)
c - b is V1() V14() V15() M2( REAL )
(c - b) * (v - S) is M2( the carrier of V)
- (v - S) is M2( the carrier of V)
- (c - b) is V1() V14() V15() M2( REAL )
(- (c - b)) * (- (v - S)) is M2( the carrier of V)

the carrier of V is non empty set
S is M2( the carrier of V)
v is M2( the carrier of V)
b is V1() V14() V15() M2( REAL )
b * S is M2( the carrier of V)
b " is V1() V14() V15() M2( REAL )
(b ") * v is M2( the carrier of V)
1 * S is M2( the carrier of V)
(b ") * b is V1() V14() V15() M2( REAL )
((b ") * b) * S is M2( the carrier of V)

the carrier of V is non empty set
S is M2( the carrier of V)
v is M2( the carrier of V)
b is V1() V14() V15() M2( REAL )
b * S is M2( the carrier of V)
b " is V1() V14() V15() M2( REAL )
(b ") * v is M2( the carrier of V)
(b ") " is V1() V14() V15() M2( REAL )
((b ") ") * S is M2( the carrier of V)

the carrier of V is non empty set
S is M2( the carrier of V)
v is M2( the carrier of V)
v - S is M2( the carrier of V)
- S is M2( the carrier of V)
K176(V,v,(- S)) is M2( the carrier of V)
b is M2( the carrier of V)
c is M2( the carrier of V)
c - b is M2( the carrier of V)
- b is M2( the carrier of V)
K176(V,c,(- b)) is M2( the carrier of V)
d is V1() V14() V15() M2( REAL )
a9 is V1() V14() V15() M2( REAL )
d * (v - S) is M2( the carrier of V)
a9 * (c - b) is M2( the carrier of V)

the carrier of V is non empty set
S is M2( the carrier of V)
v is M2( the carrier of V)
v - S is M2( the carrier of V)
- S is M2( the carrier of V)
K176(V,v,(- S)) is M2( the carrier of V)
1 * (v - S) is M2( the carrier of V)

the carrier of V is non empty set

the carrier of c is non empty set
S is M2( the carrier of V)
v is M2( the carrier of V)
b is M2( the carrier of V)
d is M2( the carrier of c)
a9 is M2( the carrier of c)
b9 is M2( the carrier of c)

the carrier of V is non empty set
S is M2( the carrier of V)
v is M2( the carrier of V)
v - S is M2( the carrier of V)
- S is M2( the carrier of V)
K176(V,v,(- S)) is M2( the carrier of V)
S - v is M2( the carrier of V)
- v is M2( the carrier of V)
K176(V,S,(- v)) is M2( the carrier of V)
b is V1() V14() V15() M2( REAL )
b * (v - S) is M2( the carrier of V)
c is V1() V14() V15() M2( REAL )
c * (S - v) is M2( the carrier of V)
c * (v - S) is M2( the carrier of V)
- (c * (v - S)) is M2( the carrier of V)
(c * (v - S)) + (b * (v - S)) is M2( the carrier of V)
0. V is V59(V) M2( the carrier of V)
the ZeroF of V is M2( the carrier of V)
c + b is V1() V14() V15() M2( REAL )
(c + b) * (v - S) is M2( the carrier of V)
(- S) + v is M2( the carrier of V)
- (- S) is M2( the carrier of V)

the carrier of V is non empty set
S is M2( the carrier of V)
v is M2( the carrier of V)
b is M2( the carrier of V)
c is M2( the carrier of V)
d is M2( the carrier of V)
a9 is M2( the carrier of V)
v - S is M2( the carrier of V)
- S is M2( the carrier of V)
K176(V,v,(- S)) is M2( the carrier of V)
c - b is M2( the carrier of V)
- b is M2( the carrier of V)
K176(V,c,(- b)) is M2( the carrier of V)
b9 is V1() V14() V15() M2( REAL )
b9 * (v - S) is M2( the carrier of V)
c9 is V1() V14() V15() M2( REAL )
c9 * (c - b) is M2( the carrier of V)
b9 " is V1() V14() V15() M2( REAL )
(b9 ") * c9 is V1() V14() V15() M2( REAL )
a9 - d is M2( the carrier of V)
- d is M2( the carrier of V)
K176(V,a9,(- d)) is M2( the carrier of V)
d9 is V1() V14() V15() M2( REAL )
d9 * (v - S) is M2( the carrier of V)
t9 is V1() V14() V15() M2( REAL )
t9 * (a9 - d) is M2( the carrier of V)
d9 " is V1() V14() V15() M2( REAL )
(d9 ") * (t9 * (a9 - d)) is M2( the carrier of V)
(d9 ") * t9 is V1() V14() V15() M2( REAL )
((d9 ") * t9) * (a9 - d) is M2( the carrier of V)
(b9 ") * (c9 * (c - b)) is M2( the carrier of V)
((b9 ") * c9) * (c - b) is M2( the carrier of V)

the carrier of V is non empty set
S is M2( the carrier of V)
v is M2( the carrier of V)
b is M2( the carrier of V)
c is M2( the carrier of V)
v - S is M2( the carrier of V)
- S is M2( the carrier of V)
K176(V,v,(- S)) is M2( the carrier of V)
c - b is M2( the carrier of V)
- b is M2( the carrier of V)
K176(V,c,(- b)) is M2( the carrier of V)
d is V1() V14() V15() M2( REAL )
d * (v - S) is M2( the carrier of V)
a9 is V1() V14() V15() M2( REAL )
a9 * (c - b) is M2( the carrier of V)
S - v is M2( the carrier of V)
- v is M2( the carrier of V)
K176(V,S,(- v)) is M2( the carrier of V)
d * (S - v) is M2( the carrier of V)
- (a9 * (c - b)) is M2( the carrier of V)
b - c is M2( the carrier of V)
- c is M2( the carrier of V)
K176(V,b,(- c)) is M2( the carrier of V)
a9 * (b - c) is M2( the carrier of V)

the carrier of V is non empty set
S is M2( the carrier of V)
v is M2( the carrier of V)
b is M2( the carrier of V)
v - S is M2( the carrier of V)
- S is M2( the carrier of V)
K176(V,v,(- S)) is M2( the carrier of V)
b - v is M2( the carrier of V)
- v is M2( the carrier of V)
K176(V,b,(- v)) is M2( the carrier of V)
c is V1() V14() V15() M2( REAL )
c * (v - S) is M2( the carrier of V)
d is V1() V14() V15() M2( REAL )
d * (b - v) is M2( the carrier of V)
c + d is V1() V14() V15() M2( REAL )
b - S is M2( the carrier of V)
K176(V,b,(- S)) is M2( the carrier of V)
d * (b - S) is M2( the carrier of V)
(b - v) + (v - S) is M2( the carrier of V)
d * ((b - v) + (v - S)) is M2( the carrier of V)
d * (v - S) is M2( the carrier of V)
(c * (v - S)) + (d * (v - S)) is M2( the carrier of V)
(c + d) * (v - S) is M2( the carrier of V)

the carrier of V is non empty set
S is M2( the carrier of V)
v is M2( the carrier of V)
b is M2( the carrier of V)
v - S is M2( the carrier of V)
- S is M2( the carrier of V)
K176(V,v,(- S)) is M2( the carrier of V)
b - S is M2( the carrier of V)
K176(V,b,(- S)) is M2( the carrier of V)
c is V1() V14() V15() M2( REAL )
c * (v - S) is M2( the carrier of V)
d is V1() V14() V15() M2( REAL )
d * (b - S) is M2( the carrier of V)
b - v is M2( the carrier of V)
- v is M2( the carrier of V)
K176(V,b,(- v)) is M2( the carrier of V)
S - v is M2( the carrier of V)
K176(V,S,(- v)) is M2( the carrier of V)
(b - S) + (S - v) is M2( the carrier of V)
(b - S) - (v - S) is M2( the carrier of V)
- (v - S) is M2( the carrier of V)
K176(V,(b - S),(- (v - S))) is M2( the carrier of V)
c * (b - v) is M2( the carrier of V)
c * (b - S) is M2( the carrier of V)
(c * (b - S)) - (d * (b - S)) is M2( the carrier of V)
- (d * (b - S)) is M2( the carrier of V)
K176(V,(c * (b - S)),(- (d * (b - S)))) is M2( the carrier of V)
c - d is V1() V14() V15() M2( REAL )
(c - d) * (b - S) is M2( the carrier of V)
S - b is M2( the carrier of V)
- b is M2( the carrier of V)
K176(V,S,(- b)) is M2( the carrier of V)
d - c is V1() V14() V15() M2( REAL )
(d - c) * (S - b) is M2( the carrier of V)
v - b is M2( the carrier of V)
K176(V,v,(- b)) is M2( the carrier of V)
(v - S) + (S - b) is M2( the carrier of V)
(v - S) - (b - S) is M2( the carrier of V)
- (b - S) is M2( the carrier of V)
K176(V,(v - S),(- (b - S))) is M2( the carrier of V)
d * (v - b) is M2( the carrier of V)
d * (v - S) is M2( the carrier of V)
(d * (v - S)) - (c * (v - S)) is M2( the carrier of V)
- (c * (v - S)) is M2( the carrier of V)
K176(V,(d * (v - S)),(- (c * (v - S)))) is M2( the carrier of V)
(d - c) * (v - S) is M2( the carrier of V)
(c - d) * (S - v) is M2( the carrier of V)
(- S) + v is M2( the carrier of V)
(- S) + b is M2( the carrier of V)

the carrier of V is non empty set
S is M2( the carrier of V)
v is M2( the carrier of V)
S - v is M2( the carrier of V)
- v is M2( the carrier of V)
K176(V,S,(- v)) is M2( the carrier of V)
b is M2( the carrier of V)
c is M2( the carrier of V)
b - c is M2( the carrier of V)
- c is M2( the carrier of V)
K176(V,b,(- c)) is M2( the carrier of V)
1 * (S - v) is M2( the carrier of V)
1 * (b - c) is M2( the carrier of V)

the carrier of V is non empty set
S is M2( the carrier of V)
v is M2( the carrier of V)
b is M2( the carrier of V)
v + b is M2( the carrier of V)
c is M2( the carrier of V)
(v + b) - c is M2( the carrier of V)
- c is M2( the carrier of V)
K176(V,(v + b),(- c)) is M2( the carrier of V)
((v + b) - c) + c is M2( the carrier of V)
((v + b) - c) - v is M2( the carrier of V)
- v is M2( the carrier of V)
K176(V,((v + b) - c),(- v)) is M2( the carrier of V)
b - c is M2( the carrier of V)
K176(V,b,(- c)) is M2( the carrier of V)
((v + b) - c) - b is M2( the carrier of V)
- b is M2( the carrier of V)
K176(V,((v + b) - c),(- b)) is M2( the carrier of V)
v - c is M2( the carrier of V)
K176(V,v,(- c)) is M2( the carrier of V)

the carrier of V is non empty set
S is M2( the carrier of V)
v is M2( the carrier of V)
b is M2( the carrier of V)
c is M2( the carrier of V)
d is M2( the carrier of V)
c + d is M2( the carrier of V)
(c + d) - b is M2( the carrier of V)
- b is M2( the carrier of V)
K176(V,(c + d),(- b)) is M2( the carrier of V)
a9 is M2( the carrier of V)
d - b is M2( the carrier of V)
K176(V,d,(- b)) is M2( the carrier of V)
c + (d - b) is M2( the carrier of V)
0. V is V59(V) M2( the carrier of V)
the ZeroF of V is M2( the carrier of V)
a9 is M2( the carrier of V)
a9 is M2( the carrier of V)
c9 is M2( the carrier of V)

the carrier of V is non empty set
S is M2( the carrier of V)
v is M2( the carrier of V)
b is M2( the carrier of V)
c is M2( the carrier of V)
S - v is M2( the carrier of V)
- v is M2( the carrier of V)
K176(V,S,(- v)) is M2( the carrier of V)
b - S is M2( the carrier of V)
- S is M2( the carrier of V)
K176(V,b,(- S)) is M2( the carrier of V)
d is V1() V14() V15() M2( REAL )
d * (S - v) is M2( the carrier of V)
a9 is V1() V14() V15() M2( REAL )
a9 * (b - S) is M2( the carrier of V)
S - c is M2( the carrier of V)
- c is M2( the carrier of V)
K176(V,S,(- c)) is M2( the carrier of V)
a9 " is V1() V14() V15() M2( REAL )
(a9 ") * d is V1() V14() V15() M2( REAL )
((a9 ") * d) * (S - c) is M2( the carrier of V)
(((a9 ") * d) * (S - c)) + S is M2( the carrier of V)
((((a9 ") * d) * (S - c)) + S) - S is M2( the carrier of V)
K176(V,((((a9 ") * d) * (S - c)) + S),(- S)) is M2( the carrier of V)
d * (S - c) is M2( the carrier of V)
(a9 ") * (d * (S - c)) is M2( the carrier of V)
((((a9 ") * d) * (S - c)) + S) - b is M2( the carrier of V)
- b is M2( the carrier of V)
K176(V,((((a9 ") * d) * (S - c)) + S),(- b)) is M2( the carrier of V)
S - b is M2( the carrier of V)
K176(V,S,(- b)) is M2( the carrier of V)
(((((a9 ") * d) * (S - c)) + S) - S) + (S - b) is M2( the carrier of V)
(((((a9 ") * d) * (S - c)) + S) - S) - (b - S) is M2( the carrier of V)
- (b - S) is M2( the carrier of V)
K176(V,(((((a9 ") * d) * (S - c)) + S) - S),(- (b - S))) is M2( the carrier of V)
v - c is M2( the carrier of V)
K176(V,v,(- c)) is M2( the carrier of V)
v - S is M2( the carrier of V)
K176(V,v,(- S)) is M2( the carrier of V)
(S - c) + (v - S) is M2( the carrier of V)
(S - c) - (S - v) is M2( the carrier of V)
- (S - v) is M2( the carrier of V)
K176(V,(S - c),(- (S - v))) is M2( the carrier of V)
d * (v - c) is M2( the carrier of V)
(d * (S - c)) - (d * (S - v)) is M2( the carrier of V)
- (d * (S - v)) is M2( the carrier of V)
K176(V,(d * (S - c)),(- (d * (S - v)))) is M2( the carrier of V)
a9 * (((((a9 ") * d) * (S - c)) + S) - S) is M2( the carrier of V)
(a9 * (((((a9 ") * d) * (S - c)) + S) - S)) - (a9 * (b - S)) is M2( the carrier of V)
- (a9 * (b - S)) is M2( the carrier of V)
K176(V,(a9 * (((((a9 ") * d) * (S - c)) + S) - S)),(- (a9 * (b - S)))) is M2( the carrier of V)
a9 * (((((a9 ") * d) * (S - c)) + S) - b) is M2( the carrier of V)
1 * (((((a9 ") * d) * (S - c)) + S) - S) is M2( the carrier of V)
d is M2( the carrier of V)
d is M2( the carrier of V)
a9 is M2( the carrier of V)

the carrier of V is non empty set
0. V is V59(V) M2( the carrier of V)
the ZeroF of V is M2( the carrier of V)
S is M2( the carrier of V)
v is M2( the carrier of V)
S - v is M2( the carrier of V)
- v is M2( the carrier of V)
K176(V,S,(- v)) is M2( the carrier of V)
1 * S is M2( the carrier of V)
(1 * S) + (- v) is M2( the carrier of V)
(- 1) * v is M2( the carrier of V)
(1 * S) + ((- 1) * v) is M2( the carrier of V)
1 * S is M2( the carrier of V)
(1 * S) + (0. V) is M2( the carrier of V)
0 * v is M2( the carrier of V)
(1 * S) + (0 * v) is M2( the carrier of V)
1 * v is M2( the carrier of V)
(0. V) + (1 * v) is M2( the carrier of V)
0 * S is M2( the carrier of V)
(0 * S) + (1 * v) is M2( the carrier of V)

the carrier of V is non empty set
0. V is V59(V) M2( the carrier of V)
the ZeroF of V is M2( the carrier of V)
S is M2( the carrier of V)
v is M2( the carrier of V)
S - (0. V) is M2( the carrier of V)
- (0. V) is M2( the carrier of V)
K176(V,S,(- (0. V))) is M2( the carrier of V)
(0. V) - v is M2( the carrier of V)
- v is M2( the carrier of V)
K176(V,(0. V),(- v)) is M2( the carrier of V)
b is V1() V14() V15() M2( REAL )
c is V1() V14() V15() M2( REAL )
b * (S - (0. V)) is M2( the carrier of V)
c * ((0. V) - v) is M2( the carrier of V)
b * S is M2( the carrier of V)
c * (- v) is M2( the carrier of V)
c * v is M2( the carrier of V)
- (c * v) is M2( the carrier of V)
(b * S) + (c * v) is M2( the carrier of V)
S - (0. V) is M2( the carrier of V)
- (0. V) is M2( the carrier of V)
K176(V,S,(- (0. V))) is M2( the carrier of V)
v - (0. V) is M2( the carrier of V)
K176(V,v,(- (0. V))) is M2( the carrier of V)
b is V1() V14() V15() M2( REAL )
c is V1() V14() V15() M2( REAL )
b * (S - (0. V)) is M2( the carrier of V)
c * (v - (0. V)) is M2( the carrier of V)
b * S is M2( the carrier of V)
c * v is M2( the carrier of V)
(b * S) - (c * v) is M2( the carrier of V)
- (c * v) is M2( the carrier of V)
K176(V,(b * S),(- (c * v))) is M2( the carrier of V)
- v is M2( the carrier of V)
c * (- v) is M2( the carrier of V)
(b * S) + (c * (- v)) is M2( the carrier of V)
- c is V1() V14() V15() M2( REAL )
(- c) * v is M2( the carrier of V)
(b * S) + ((- c) * v) is M2( the carrier of V)

the carrier of V is non empty set
S is M2( the carrier of V)
v is M2( the carrier of V)
S - v is M2( the carrier of V)
- v is M2( the carrier of V)
K176(V,S,(- v)) is M2( the carrier of V)
b is M2( the carrier of V)
c is M2( the carrier of V)
b - c is M2( the carrier of V)
- c is M2( the carrier of V)
K176(V,b,(- c)) is M2( the carrier of V)
d is V1() V14() V15() M2( REAL )
d * (S - v) is M2( the carrier of V)
a9 is V1() V14() V15() M2( REAL )
a9 * (b - c) is M2( the carrier of V)
0. V is V59(V) M2( the carrier of V)
the ZeroF of V is M2( the carrier of V)
- (a9 * (b - c)) is M2( the carrier of V)
- (- (a9 * (b - c))) is M2( the carrier of V)
- (b - c) is M2( the carrier of V)
a9 * (- (b - c)) is M2( the carrier of V)
- (a9 * (- (b - c))) is M2( the carrier of V)
c - b is M2( the carrier of V)
- b is M2( the carrier of V)
K176(V,c,(- b)) is M2( the carrier of V)
a9 * (c - b) is M2( the carrier of V)
- (a9 * (c - b)) is M2( the carrier of V)
- (c - b) is M2( the carrier of V)
a9 * (- (c - b)) is M2( the carrier of V)
- a9 is V1() V14() V15() M2( REAL )
(- a9) * (c - b) is M2( the carrier of V)
- d is V1() V14() V15() M2( REAL )
(- d) * (S - v) is M2( the carrier of V)
- (S - v) is M2( the carrier of V)
d * (- (S - v)) is M2( the carrier of V)
(- a9) * (b - c) is M2( the carrier of V)

the carrier of V is non empty set
S is M2( the carrier of V)
v is M2( the carrier of V)
b is M2( the carrier of V)
c is M2( the carrier of V)
d is M2( the carrier of V)
a9 is M2( the carrier of V)
c - b is M2( the carrier of V)
- b is M2( the carrier of V)
K176(V,c,(- b)) is M2( the carrier of V)
b9 is V1() V14() V15() M2( REAL )
b9 * S is M2( the carrier of V)
c9 is V1() V14() V15() M2( REAL )
c9 * v is M2( the carrier of V)
(b9 * S) + (c9 * v) is M2( the carrier of V)
a9 - d is M2( the carrier of V)
- d is M2( the carrier of V)
K176(V,a9,(- d)) is M2( the carrier of V)
d9 is V1() V14() V15() M2( REAL )
d9 * S is M2( the carrier of V)
t9 is V1() V14() V15() M2( REAL )
t9 * v is M2( the carrier of V)
(d9 * S) + (t9 * v) is M2( the carrier of V)
b9 * t9 is V1() V14() V15() M2( REAL )
d9 * c9 is V1() V14() V15() M2( REAL )
(b9 * t9) - (d9 * c9) is V1() V14() V15() M2( REAL )
0. V is V59(V) M2( the carrier of V)
the ZeroF of V is M2( the carrier of V)
0 * v is M2( the carrier of V)
(0. V) + (0 * v) is M2( the carrier of V)
(0. V) + (0. V) is M2( the carrier of V)
0. V is V59(V) M2( the carrier of V)
the ZeroF of V is M2( the carrier of V)
0 * v is M2( the carrier of V)
(0. V) + (0 * v) is M2( the carrier of V)
(0. V) + (0. V) is M2( the carrier of V)
0. V is V59(V) M2( the carrier of V)
the ZeroF of V is M2( the carrier of V)
0 * v is M2( the carrier of V)
(0. V) + (0 * v) is M2( the carrier of V)
(0. V) + (0. V) is M2( the carrier of V)
0. V is V59(V) M2( the carrier of V)
the ZeroF of V is M2( the carrier of V)
(0. V) + (t9 * v) is M2( the carrier of V)
t9 " is V1() V14() V15() M2( REAL )
(t9 ") * (a9 - d) is M2( the carrier of V)
(t9 ") * t9 is V1() V14() V15() M2( REAL )
((t9 ") * t9) * v is M2( the carrier of V)
1 * v is M2( the carrier of V)
(0. V) + (c9 * v) is M2( the carrier of V)
c9 " is V1() V14() V15() M2( REAL )
(c9 ") * (c - b) is M2( the carrier of V)
(c9 ") * c9 is V1() V14() V15() M2( REAL )
((c9 ") * c9) * v is M2( the carrier of V)
(b9 * S) + (0. V) is M2( the carrier of V)
b9 " is V1() V14() V15() M2( REAL )
(b9 ") * (c - b) is M2( the carrier of V)
(b9 ") * b9 is V1() V14() V15() M2( REAL )
((b9 ") * b9) * S is M2( the carrier of V)
1 * S is M2( the carrier of V)
(d9 * S) + (0. V) is M2( the carrier of V)
d9 " is V1() V14() V15() M2( REAL )
(d9 ") * (a9 - d) is M2( the carrier of V)
(d9 ") * d9 is V1() V14() V15() M2( REAL )
((d9 ") * d9) * S is M2( the carrier of V)
d9 * (c - b) is M2( the carrier of V)
d9 * (b9 * S) is M2( the carrier of V)
d9 * (c9 * v) is M2( the carrier of V)
(d9 * (b9 * S)) + (d9 * (c9 * v)) is M2( the carrier of V)
d9 * b9 is V1() V14() V15() M2( REAL )
(d9 * b9) * S is M2( the carrier of V)
((d9 * b9) * S) + (d9 * (c9 * v)) is M2( the carrier of V)
b9 * d9 is V1() V14() V15() M2( REAL )
(b9 * d9) * S is M2( the carrier of V)
(b9 * t9) * v is M2( the carrier of V)
((b9 * d9) * S) + ((b9 * t9) * v) is M2( the carrier of V)
b9 * (d9 * S) is M2( the carrier of V)
(b9 * (d9 * S)) + ((b9 * t9) * v) is M2( the carrier of V)
b9 * (t9 * v) is M2( the carrier of V)
(b9 * (d9 * S)) + (b9 * (t9 * v)) is M2( the carrier of V)
b9 * (a9 - d) is M2( the carrier of V)
b - d is M2( the carrier of V)
K176(V,b,(- d)) is M2( the carrier of V)
d9 is V1() V14() V15() M2( REAL )
d9 * S is M2( the carrier of V)
d is V1() V14() V15() M2( REAL )
d * v is M2( the carrier of V)
(d9 * S) + (d * v) is M2( the carrier of V)
d9 * d is V1() V14() V15() M2( REAL )
d9 * t9 is V1() V14() V15() M2( REAL )
(d9 * d) - (d9 * t9) is V1() V14() V15() M2( REAL )
b9 * d is V1() V14() V15() M2( REAL )
d9 * c9 is V1() V14() V15() M2( REAL )
(b9 * d) - (d9 * c9) is V1() V14() V15() M2( REAL )
((b9 * d) - (d9 * c9)) * d9 is V1() V14() V15() M2( REAL )
b9 * ((d9 * d) - (d9 * t9)) is V1() V14() V15() M2( REAL )
d9 * ((b9 * t9) - (d9 * c9)) is V1() V14() V15() M2( REAL )
(b9 * ((d9 * d) - (d9 * t9))) + (d9 * ((b9 * t9) - (d9 * c9))) is V1() V14() V15() M2( REAL )
((b9 * t9) - (d9 * c9)) " is V1() V14() V15() M2( REAL )
(((b9 * t9) - (d9 * c9)) ") * ((d9 * d) - (d9 * t9)) is V1() V14() V15() M2( REAL )
((((b9 * t9) - (d9 * c9)) ") * ((d9 * d) - (d9 * t9))) * (c - b) is M2( the carrier of V)
b + (((((b9 * t9) - (d9 * c9)) ") * ((d9 * d) - (d9 * t9))) * (c - b)) is M2( the carrier of V)
(b + (((((b9 * t9) - (d9 * c9)) ") * ((d9 * d) - (d9 * t9))) * (c - b))) - b is M2( the carrier of V)
K176(V,(b + (((((b9 * t9) - (d9 * c9)) ") * ((d9 * d) - (d9 * t9))) * (c - b))),(- b)) is M2( the carrier of V)
((b9 * t9) - (d9 * c9)) * ((b + (((((b9 * t9) - (d9 * c9)) ") * ((d9 * d) - (d9 * t9))) * (c - b))) - b) is M2( the carrier of V)
((b9 * t9) - (d9 * c9)) * (b + (((((b9 * t9) - (d9 * c9)) ") * ((d9 * d) - (d9 * t9))) * (c - b))) is M2( the carrier of V)
((b9 * t9) - (d9 * c9)) * b is M2( the carrier of V)
(((b9 * t9) - (d9 * c9)) * (b + (((((b9 * t9) - (d9 * c9)) ") * ((d9 * d) - (d9 * t9))) * (c - b)))) - (((b9 * t9) - (d9 * c9)) * b) is M2( the carrier of V)
- (((b9 * t9) - (d9 * c9)) * b) is M2( the carrier of V)
K176(V,(((b9 * t9) - (d9 * c9)) * (b + (((((b9 * t9) - (d9 * c9)) ") * ((d9 * d) - (d9 * t9))) * (c - b)))),(- (((b9 * t9) - (d9 * c9)) * b))) is M2( the carrier of V)
((b9 * t9) - (d9 * c9)) * (((((b9 * t9) - (d9 * c9)) ") * ((d9 * d) - (d9 * t9))) * (c - b)) is M2( the carrier of V)
(((b9 * t9) - (d9 * c9)) * b) + (((b9 * t9) - (d9 * c9)) * (((((b9 * t9) - (d9 * c9)) ") * ((d9 * d) - (d9 * t9))) * (c - b))) is M2( the carrier of V)
((((b9 * t9) - (d9 * c9)) * b) + (((b9 * t9) - (d9 * c9)) * (((((b9 * t9) - (d9 * c9)) ") * ((d9 * d) - (d9 * t9))) * (c - b)))) - (((b9 * t9) - (d9 * c9)) * b) is M2( the carrier of V)
K176(V,((((b9 * t9) - (d9 * c9)) * b) + (((b9 * t9) - (d9 * c9)) * (((((b9 * t9) - (d9 * c9)) ") * ((d9 * d) - (d9 * t9))) * (c - b)))),(- (((b9 * t9) - (d9 * c9)) * b))) is M2( the carrier of V)
((b9 * t9) - (d9 * c9)) * ((((b9 * t9) - (d9 * c9)) ") * ((d9 * d) - (d9 * t9))) is V1() V14() V15() M2( REAL )
(((b9 * t9) - (d9 * c9)) * ((((b9 * t9) - (d9 * c9)) ") * ((d9 * d) - (d9 * t9)))) * (c - b) is M2( the carrier of V)
(((b9 * t9) - (d9 * c9)) * b) + ((((b9 * t9) - (d9 * c9)) * ((((b9 * t9) - (d9 * c9)) ") * ((d9 * d) - (d9 * t9)))) * (c - b)) is M2( the carrier of V)
((((b9 * t9) - (d9 * c9)) * b) + ((((b9 * t9) - (d9 * c9)) * ((((b9 * t9) - (d9 * c9)) ") * ((d9 * d) - (d9 * t9)))) * (c - b))) - (((b9 * t9) - (d9 * c9)) * b) is M2( the carrier of V)
K176(V,((((b9 * t9) - (d9 * c9)) * b) + ((((b9 * t9) - (d9 * c9)) * ((((b9 * t9) - (d9 * c9)) ") * ((d9 * d) - (d9 * t9)))) * (c - b))),(- (((b9 * t9) - (d9 * c9)) * b))) is M2( the carrier of V)
((b9 * t9) - (d9 * c9)) * (((b9 * t9) - (d9 * c9)) ") is V1() V14() V15() M2( REAL )
(((b9 * t9) - (d9 * c9)) * (((b9 * t9) - (d9 * c9)) ")) * ((d9 * d) - (d9 * t9)) is V1() V14() V15() M2( REAL )
((((b9 * t9) - (d9 * c9)) * (((b9 * t9) - (d9 * c9)) ")) * ((d9 * d) - (d9 * t9))) * (c - b) is M2( the carrier of V)
(((b9 * t9) - (d9 * c9)) * b) + (((((b9 * t9) - (d9 * c9)) * (((b9 * t9) - (d9 * c9)) ")) * ((d9 * d) - (d9 * t9))) * (c - b)) is M2( the carrier of V)
((((b9 * t9) - (d9 * c9)) * b) + (((((b9 * t9) - (d9 * c9)) * (((b9 * t9) - (d9 * c9)) ")) * ((d9 * d) - (d9 * t9))) * (c - b))) - (((b9 * t9) - (d9 * c9)) * b) is M2( the carrier of V)
K176(V,((((b9 * t9) - (d9 * c9)) * b) + (((((b9 * t9) - (d9 * c9)) * (((b9 * t9) - (d9 * c9)) ")) * ((d9 * d) - (d9 * t9))) * (c - b))),(- (((b9 * t9) - (d9 * c9)) * b))) is M2( the carrier of V)
1 * ((d9 * d) - (d9 * t9)) is V1() V14() V15() M2( REAL )
(1 * ((d9 * d) - (d9 * t9))) * (c - b) is M2( the carrier of V)
(((b9 * t9) - (d9 * c9)) * b) + ((1 * ((d9 * d) - (d9 * t9))) * (c - b)) is M2( the carrier of V)
((((b9 * t9) - (d9 * c9)) * b) + ((1 * ((d9 * d) - (d9 * t9))) * (c - b))) - (((b9 * t9) - (d9 * c9)) * b) is M2( the carrier of V)
K176(V,((((b9 * t9) - (d9 * c9)) * b) + ((1 * ((d9 * d) - (d9 * t9))) * (c - b))),(- (((b9 * t9) - (d9 * c9)) * b))) is M2( the carrier of V)
((d9 * d) - (d9 * t9)) * (c - b) is M2( the carrier of V)
(((b9 * t9) - (d9 * c9)) * b) - (((b9 * t9) - (d9 * c9)) * b) is M2( the carrier of V)
K176(V,(((b9 * t9) - (d9 * c9)) * b),(- (((b9 * t9) - (d9 * c9)) * b))) is M2( the carrier of V)
(((d9 * d) - (d9 * t9)) * (c - b)) + ((((b9 * t9) - (d9 * c9)) * b) - (((b9 * t9) - (d9 * c9)) * b)) is M2( the carrier of V)
(((d9 * d) - (d9 * t9)) * (c - b)) + (0. V) is M2( the carrier of V)
(b + (((((b9 * t9) - (d9 * c9)) ") * ((d9 * d) - (d9 * t9))) * (c - b))) - d is M2( the carrier of V)
K176(V,(b + (((((b9 * t9) - (d9 * c9)) ") * ((d9 * d) - (d9 * t9))) * (c - b))),(- d)) is M2( the carrier of V)
((b9 * t9) - (d9 * c9)) * ((b + (((((b9 * t9) - (d9 * c9)) ") * ((d9 * d) - (d9 * t9))) * (c - b))) - d) is M2( the carrier of V)
((b9 * t9) - (d9 * c9)) * d is M2( the carrier of V)
(((b9 * t9) - (d9 * c9)) * (b + (((((b9 * t9) - (d9 * c9)) ") * ((d9 * d) - (d9 * t9))) * (c - b)))) - (((b9 * t9) - (d9 * c9)) * d) is M2( the carrier of V)
- (((b9 * t9) - (d9 * c9)) * d) is M2( the carrier of V)
K176(V,(((b9 * t9) - (d9 * c9)) * (b + (((((b9 * t9) - (d9 * c9)) ") * ((d9 * d) - (d9 * t9))) * (c - b)))),(- (((b9 * t9) - (d9 * c9)) * d))) is M2( the carrier of V)
((((b9 * t9) - (d9 * c9)) * b) + (((b9 * t9) - (d9 * c9)) * (((((b9 * t9) - (d9 * c9)) ") * ((d9 * d) - (d9 * t9))) * (c - b)))) - (((b9 * t9) - (d9 * c9)) * d) is M2( the carrier of V)
K176(V,((((b9 * t9) - (d9 * c9)) * b) + (((b9 * t9) - (d9 * c9)) * (((((b9 * t9) - (d9 * c9)) ") * ((d9 * d) - (d9 * t9))) * (c - b)))),(- (((b9 * t9) - (d9 * c9)) * d))) is M2( the carrier of V)
((((b9 * t9) - (d9 * c9)) * b) + ((((b9 * t9) - (d9 * c9)) * ((((b9 * t9) - (d9 * c9)) ") * ((d9 * d) - (d9 * t9)))) * (c - b))) - (((b9 * t9) - (d9 * c9)) * d) is M2( the carrier of V)
K176(V,((((b9 * t9) - (d9 * c9)) * b) + ((((b9 * t9) - (d9 * c9)) * ((((b9 * t9) - (d9 * c9)) ") * ((d9 * d) - (d9 * t9)))) * (c - b))),(- (((b9 * t9) - (d9 * c9)) * d))) is M2( the carrier of V)
((((b9 * t9) - (d9 * c9)) * b) + (((((b9 * t9) - (d9 * c9)) * (((b9 * t9) - (d9 * c9)) ")) * ((d9 * d) - (d9 * t9))) * (c - b))) - (((b9 * t9) - (d9 * c9)) * d) is M2( the carrier of V)
K176(V,((((b9 * t9) - (d9 * c9)) * b) + (((((b9 * t9) - (d9 * c9)) * (((b9 * t9) - (d9 * c9)) ")) * ((d9 * d) - (d9 * t9))) * (c - b))),(- (((b9 * t9) - (d9 * c9)) * d))) is M2( the carrier of V)
((((b9 * t9) - (d9 * c9)) * b) + ((1 * ((d9 * d) - (d9 * t9))) * (c - b))) - (((b9 * t9) - (d9 * c9)) * d) is M2( the carrier of V)
K176(V,((((b9 * t9) - (d9 * c9)) * b) + ((1 * ((d9 * d) - (d9 * t9))) * (c - b))),(- (((b9 * t9) - (d9 * c9)) * d))) is M2( the carrier of V)
(((b9 * t9) - (d9 * c9)) * b) - (((b9 * t9) - (d9 * c9)) * d) is M2( the carrier of V)
K176(V,(((b9 * t9) - (d9 * c9)) * b),(- (((b9 * t9) - (d9 * c9)) * d))) is M2( the carrier of V)
(((d9 * d) - (d9 * t9)) * (c - b)) + ((((b9 * t9) - (d9 * c9)) * b) - (((b9 * t9) - (d9 * c9)) * d)) is M2( the carrier of V)
((d9 * d) - (d9 * t9)) * ((b9 * S) + (c9 * v)) is M2( the carrier of V)
((b9 * t9) - (d9 * c9)) * ((d9 * S) + (d * v)) is M2( the carrier of V)
(((d9 * d) - (d9 * t9)) * ((b9 * S) + (c9 * v))) + (((b9 * t9) - (d9 * c9)) * ((d9 * S) + (d * v))) is M2( the carrier of V)
((d9 * d) - (d9 * t9)) * (b9 * S) is M2( the carrier of V)
((d9 * d) - (d9 * t9)) * (c9 * v) is M2( the carrier of V)
(((d9 * d) - (d9 * t9)) * (b9 * S)) + (((d9 * d) - (d9 * t9)) * (c9 * v)) is M2( the carrier of V)
((((d9 * d) - (d9 * t9)) * (b9 * S)) + (((d9 * d) - (d9 * t9)) * (c9 * v))) + (((b9 * t9) - (d9 * c9)) * ((d9 * S) + (d * v))) is M2( the carrier of V)
((b9 * t9) - (d9 * c9)) * (d9 * S) is M2( the carrier of V)
((b9 * t9) - (d9 * c9)) * (d * v) is M2( the carrier of V)
(((b9 * t9) - (d9 * c9)) * (d9 * S)) + (((b9 * t9) - (d9 * c9)) * (d * v)) is M2( the carrier of V)
((((d9 * d) - (d9 * t9)) * (b9 * S)) + (((d9 * d) - (d9 * t9)) * (c9 * v))) + ((((b9 * t9) - (d9 * c9)) * (d9 * S)) + (((b9 * t9) - (d9 * c9)) * (d * v))) is M2( the carrier of V)
((d9 * d) - (d9 * t9)) * b9 is V1() V14() V15() M2( REAL )
(((d9 * d) - (d9 * t9)) * b9) * S is M2( the carrier of V)
((((d9 * d) - (d9 * t9)) * b9) * S) + (((d9 * d) - (d9 * t9)) * (c9 * v)) is M2( the carrier of V)
(((((d9 * d) - (d9 * t9)) * b9) * S) + (((d9 * d) - (d9 * t9)) * (c9 * v))) + ((((b9 * t9) - (d9 * c9)) * (d9 * S)) + (((b9 * t9) - (d9 * c9)) * (d * v))) is M2( the carrier of V)
((d9 * d) - (d9 * t9)) * c9 is V1() V14() V15() M2( REAL )
(((d9 * d) - (d9 * t9)) * c9) * v is M2( the carrier of V)
((((d9 * d) - (d9 * t9)) * b9) * S) + ((((d9 * d) - (d9 * t9)) * c9) * v) is M2( the carrier of V)
(((((d9 * d) - (d9 * t9)) * b9) * S) + ((((d9 * d) - (d9 * t9)) * c9) * v)) + ((((b9 * t9) - (d9 * c9)) * (d9 * S)) + (((b9 * t9) - (d9 * c9)) * (d * v))) is M2( the carrier of V)
((b9 * t9) - (d9 * c9)) * d9 is V1() V14() V15() M2( REAL )
(((b9 * t9) - (d9 * c9)) * d9) * S is M2( the carrier of V)
((((b9 * t9) - (d9 * c9)) * d9) * S) + (((b9 * t9) - (d9 * c9)) * (d * v)) is M2( the carrier of V)
(((((d9 * d) - (d9 * t9)) * b9) * S) + ((((d9 * d) - (d9 * t9)) * c9) * v)) + (((((b9 * t9) - (d9 * c9)) * d9) * S) + (((b9 * t9) - (d9 * c9)) * (d * v))) is M2( the carrier of V)
((b9 * t9) - (d9 * c9)) * d is V1() V14() V15() M2( REAL )
(((b9 * t9) - (d9 * c9)) * d) * v is M2( the carrier of V)
((((b9 * t9) - (d9 * c9)) * d) * v) + ((((b9 * t9) - (d9 * c9)) * d9) * S) is M2( the carrier of V)
(((((d9 * d) - (d9 * t9)) * b9) * S) + ((((d9 * d) - (d9 * t9)) * c9) * v)) + (((((b9 * t9) - (d9 * c9)) * d) * v) + ((((b9 * t9) - (d9 * c9)) * d9) * S)) is M2( the carrier of V)
(((((d9 * d) - (d9 * t9)) * b9) * S) + ((((d9 * d) - (d9 * t9)) * c9) * v)) + ((((b9 * t9) - (d9 * c9)) * d) * v) is M2( the carrier of V)
((((((d9 * d) - (d9 * t9)) * b9) * S) + ((((d9 * d) - (d9 * t9)) * c9) * v)) + ((((b9 * t9) - (d9 * c9)) * d) * v)) + ((((b9 * t9) - (d9 * c9)) * d9) * S) is M2( the carrier of V)
((((d9 * d) - (d9 * t9)) * c9) * v) + ((((b9 * t9) - (d9 * c9)) * d) * v) is M2( the carrier of V)
(((((d9 * d) - (d9 * t9)) * c9) * v) + ((((b9 * t9) - (d9 * c9)) * d) * v)) + ((((d9 * d) - (d9 * t9)) * b9) * S) is M2( the carrier of V)
((((((d9 * d) - (d9 * t9)) * c9) * v) + ((((b9 * t9) - (d9 * c9)) * d) * v)) + ((((d9 * d) - (d9 * t9)) * b9) * S)) + ((((b9 * t9) - (d9 * c9)) * d9) * S) is M2( the carrier of V)
((((d9 * d) - (d9 * t9)) * b9) * S) + ((((b9 * t9) - (d9 * c9)) * d9) * S) is M2( the carrier of V)
(((((d9 * d) - (d9 * t9)) * c9) * v) + ((((b9 * t9) - (d9 * c9)) * d) * v)) + (((((d9 * d) - (d9 * t9)) * b9) * S) + ((((b9 * t9) - (d9 * c9)) * d9) * S)) is M2( the carrier of V)
(((d9 * d) - (d9 * t9)) * c9) + (((b9 * t9) - (d9 * c9)) * d) is V1() V14() V15() M2( REAL )
((((d9 * d) - (d9 * t9)) * c9) + (((b9 * t9) - (d9 * c9)) * d)) * v is M2( the carrier of V)
(((((d9 * d) - (d9 * t9)) * c9) + (((b9 * t9) - (d9 * c9)) * d)) * v) + (((((d9 * d) - (d9 * t9)) * b9) * S) + ((((b9 * t9) - (d9 * c9)) * d9) * S)) is M2( the carrier of V)
((b9 * d) - (d9 * c9)) * t9 is V1() V14() V15() M2( REAL )
(((b9 * d) - (d9 * c9)) * t9) * v is M2( the carrier of V)
(((b9 * d) - (d9 * c9)) * d9) * S is M2( the carrier of V)
((((b9 * d) - (d9 * c9)) * t9) * v) + ((((b9 * d) - (d9 * c9)) * d9) * S) is M2( the carrier of V)
((b9 * d) - (d9 * c9)) * (t9 * v) is M2( the carrier of V)
(((b9 * d) - (d9 * c9)) * (t9 * v)) + ((((b9 * d) - (d9 * c9)) * d9) * S) is M2( the carrier of V)
((b9 * d) - (d9 * c9)) * (d9 * S) is M2( the carrier of V)
(((b9 * d) - (d9 * c9)) * (t9 * v)) + (((b9 * d) - (d9 * c9)) * (d9 * S)) is M2( the carrier of V)
((b9 * d) - (d9 * c9)) * (a9 - d) is M2( the carrier of V)
c9 * ((d9 * d) - (d9 * t9)) is V1() V14() V15() M2( REAL )
d * ((b9 * t9) - (d9 * c9)) is V1() V14() V15() M2( REAL )
(c9 * ((d9 * d) - (d9 * t9))) + (d * ((b9 * t9) - (d9 * c9))) is V1() V14() V15() M2( REAL )
0 * v is M2( the carrier of V)
(0. V) + (0 * v) is M2( the carrier of V)
(0. V) + (0. V) is M2( the carrier of V)
q9 is M2( the carrier of V)
r9 is M2( the carrier of V)
s9 is M2( the carrier of V)
c21 is M2( the carrier of V)
the non empty non trivial set is non empty non trivial set
[: the non empty non trivial set , the non empty non trivial set :] is non empty set
[:[: the non empty non trivial set , the non empty non trivial set :],[: the non empty non trivial set , the non empty non trivial set :]:] is non empty set
bool [:[: the non empty non trivial set , the non empty non trivial set :],[: the non empty non trivial set , the non empty non trivial set :]:] is non empty set
the V26() V29([: the non empty non trivial set , the non empty non trivial set :]) V30([: the non empty non trivial set , the non empty non trivial set :]) M2( bool [:[: the non empty non trivial set , the non empty non trivial set :],[: the non empty non trivial set , the non empty non trivial set :]:]) is V26() V29([: the non empty non trivial set , the non empty non trivial set :]) V30([: the non empty non trivial set , the non empty non trivial set :]) M2( bool [:[: the non empty non trivial set , the non empty non trivial set :],[: the non empty non trivial set , the non empty non trivial set :]:])
( the non empty non trivial set , the V26() V29([: the non empty non trivial set , the non empty non trivial set :]) V30([: the non empty non trivial set , the non empty non trivial set :]) M2( bool [:[: the non empty non trivial set , the non empty non trivial set :],[: the non empty non trivial set , the non empty non trivial set :]:])) is () ()
V is non empty ()
the carrier of V is non empty set

the carrier of V is non empty set
[: the carrier of V, the carrier of V:] is non empty set
[:[: the carrier of V, the carrier of V:],[: the carrier of V, the carrier of V:]:] is non empty set
bool [:[: the carrier of V, the carrier of V:],[: the carrier of V, the carrier of V:]:] is non empty set
v is V26() V29([: the carrier of V, the carrier of V:]) V30([: the carrier of V, the carrier of V:]) M2( bool [:[: the carrier of V, the carrier of V:],[: the carrier of V, the carrier of V:]:])
b is set
c is set
[b,c] is non empty set
d is M2( the carrier of V)
a9 is M2( the carrier of V)
[d,a9] is non empty M2([: the carrier of V, the carrier of V:])
b9 is M2( the carrier of V)
c9 is M2( the carrier of V)
[b9,c9] is non empty M2([: the carrier of V, the carrier of V:])
S is V26() V29([: the carrier of V, the carrier of V:]) V30([: the carrier of V, the carrier of V:]) M2( bool [:[: the carrier of V, the carrier of V:],[: the carrier of V, the carrier of V:]:])
v is V26() V29([: the carrier of V, the carrier of V:]) V30([: the carrier of V, the carrier of V:]) M2( bool [:[: the carrier of V, the carrier of V:],[: the carrier of V, the carrier of V:]:])
b is set
c is set
[b,c] is non empty set
d is M2( the carrier of V)
a9 is M2( the carrier of V)
[d,a9] is non empty M2([: the carrier of V, the carrier of V:])
b9 is M2( the carrier of V)
c9 is M2( the carrier of V)
[b9,c9] is non empty M2([: the carrier of V, the carrier of V:])
d is M2( the carrier of V)
a9 is M2( the carrier of V)
[d,a9] is non empty M2([: the carrier of V, the carrier of V:])
b9 is M2( the carrier of V)
c9 is M2( the carrier of V)
[b9,c9] is non empty M2([: the carrier of V, the carrier of V:])

the carrier of V is non empty set
[: the carrier of V, the carrier of V:] is non empty set
(V) is V26() V29([: the carrier of V, the carrier of V:]) V30([: the carrier of V, the carrier of V:]) M2( bool [:[: the carrier of V, the carrier of V:],[: the carrier of V, the carrier of V:]:])
[:[: the carrier of V, the carrier of V:],[: the carrier of V, the carrier of V:]:] is non empty set
bool [:[: the carrier of V, the carrier of V:],[: the carrier of V, the carrier of V:]:] is non empty set
S is M2( the carrier of V)
v is M2( the carrier of V)
[S,v] is non empty M2([: the carrier of V, the carrier of V:])
b is M2( the carrier of V)
c is M2( the carrier of V)
[b,c] is non empty M2([: the carrier of V, the carrier of V:])
[[S,v],[b,c]] is non empty M2([:[: the carrier of V, the carrier of V:],[: the carrier of V, the carrier of V:]:])
d is M2( the carrier of V)
a9 is M2( the carrier of V)
[d,a9] is non empty M2([: the carrier of V, the carrier of V:])
b9 is M2( the carrier of V)
c9 is M2( the carrier of V)
[b9,c9] is non empty M2([: the carrier of V, the carrier of V:])

the carrier of V is non empty set
(V) is V26() V29([: the carrier of V, the carrier of V:]) V30([: the carrier of V, the carrier of V:]) M2( bool [:[: the carrier of V, the carrier of V:],[: the carrier of V, the carrier of V:]:])
[: the carrier of V, the carrier of V:] is non empty set
[:[: the carrier of V, the carrier of V:],[: the carrier of V, the carrier of V:]:] is non empty set
bool [:[: the carrier of V, the carrier of V:],[: the carrier of V, the carrier of V:]:] is non empty set
( the carrier of V,(V)) is () ()

(V) is () ()
the carrier of V is non empty set
(V) is V26() V29([: the carrier of V, the carrier of V:]) V30([: the carrier of V, the carrier of V:]) M2( bool [:[: the carrier of V, the carrier of V:],[: the carrier of V, the carrier of V:]:])
[: the carrier of V, the carrier of V:] is non empty set
[:[: the carrier of V, the carrier of V:],[: the carrier of V, the carrier of V:]:] is non empty set
bool [:[: the carrier of V, the carrier of V:],[: the carrier of V, the carrier of V:]:] is non empty set
( the carrier of V,(V)) is () ()

the carrier of V is non empty set
0. V is V59(V) M2( the carrier of V)
the ZeroF of V is M2( the carrier of V)
(V) is non empty () ()
(V) is V26() V29([: the carrier of V, the carrier of V:]) V30([: the carrier of V, the carrier of V:]) M2( bool [:[: the carrier of V, the carrier of V:],[: the carrier of V, the carrier of V:]:])
[: the carrier of V, the carrier of V:] is non empty set
[:[: the carrier of V, the carrier of V:],[: the carrier of V, the carrier of V:]:] is non empty set
bool [:[: the carrier of V, the carrier of V:],[: the carrier of V, the carrier of V:]:] is non empty set
( the carrier of V,(V)) is () ()
the carrier of (V) is non empty set
S is M2( the carrier of V)
v is M2( the carrier of V)
c is M2( the carrier of (V))
d is M2( the carrier of (V))
a9 is M2( the carrier of (V))
c9 is M2( the carrier of (V))
d9 is M2( the carrier of (V))
t9 is M2( the carrier of (V))
t is M2( the carrier of (V))
b9 is M2( the carrier of (V))
d9 is M2( the carrier of V)
d is M2( the carrier of V)
c9 is M2( the carrier of V)
[: the carrier of (V), the carrier of (V):] is non empty set
[c,d] is non empty M2([: the carrier of (V), the carrier of (V):])
[a9,a9] is non empty M2([: the carrier of (V), the carrier of (V):])
[[c,d],[a9,a9]] is non empty M2([:[: the carrier of (V), the carrier of (V):],[: the carrier of (V), the carrier of (V):]:])
[:[: the carrier of (V), the carrier of (V):],[: the carrier of (V), the carrier of (V):]:] is non empty set
the of (V) is V26() V29([: the carrier of (V), the carrier of (V):]) V30([: the carrier of (V), the carrier of (V):]) M2( bool [:[: the carrier of (V), the carrier of (V):],[: the carrier of (V), the carrier of (V):]:])
bool [:[: the carrier of (V), the carrier of (V):],[: the carrier of (V), the carrier of (V):]:] is non empty set
[d,c] is non empty M2([: the carrier of (V), the carrier of (V):])
[[c,d],[d,c]] is non empty M2([:[: the carrier of (V), the carrier of (V):],[: the carrier of (V), the carrier of (V):]:])
[c9,d9] is non empty M2([: the carrier of (V), the carrier of (V):])
[[c,d],[c9,d9]] is non empty M2([:[: the carrier of (V), the carrier of (V):],[: the carrier of (V), the carrier of (V):]:])
[t9,t] is non empty M2([: the carrier of (V), the carrier of (V):])
[[c,d],[t9,t]] is non empty M2([:[: the carrier of (V), the carrier of (V):],[: the carrier of (V), the carrier of (V):]:])
p9 is M2( the carrier of V)
q9 is M2( the carrier of V)
r9 is M2( the carrier of V)
s9 is M2( the carrier of V)
[[c9,d9],[t9,t]] is non empty M2([:[: the carrier of (V), the carrier of (V):],[: the carrier of (V), the carrier of (V):]:])
[a9,b9] is non empty M2([: the carrier of (V), the carrier of (V):])
[[c,d],[a9,b9]] is non empty M2([:[: the carrier of (V), the carrier of (V):],[: the carrier of (V), the carrier of (V):]:])
d9 is M2( the carrier of V)
[d,c] is non empty M2([: the carrier of (V), the carrier of (V):])
[b9,a9] is non empty M2([: the carrier of (V), the carrier of (V):])
[[d,c],[b9,a9]] is non empty M2([:[: the carrier of (V), the carrier of (V):],[: the carrier of (V), the carrier of (V):]:])
[d,a9] is non empty M2([: the carrier of (V), the carrier of (V):])
[[c,d],[d,a9]] is non empty M2([:[: the carrier of (V), the carrier of (V):],[: the carrier of (V), the carrier of (V):]:])
[c,a9] is non empty M2([: the carrier of (V), the carrier of (V):])
[[c,d],[c,a9]] is non empty M2([:[: the carrier of (V), the carrier of (V):],[: the carrier of (V), the carrier of (V):]:])
[c,a9] is non empty M2([: the carrier of (V), the carrier of (V):])
[[c,d],[c,a9]] is non empty M2([:[: the carrier of (V), the carrier of (V):],[: the carrier of (V), the carrier of (V):]:])
[d,a9] is non empty M2([: the carrier of (V), the carrier of (V):])
[[c,d],[d,a9]] is non empty M2([:[: the carrier of (V), the carrier of (V):],[: the carrier of (V), the carrier of (V):]:])
[a9,d] is non empty M2([: the carrier of (V), the carrier of (V):])
[[c,a9],[a9,d]] is non empty M2([:[: the carrier of (V), the carrier of (V):],[: the carrier of (V), the carrier of (V):]:])
c is M2( the carrier of V)
d is M2( the carrier of V)
a9 is M2( the carrier of V)
b9 is M2( the carrier of V)
[: the carrier of (V), the carrier of (V):] is non empty set
c9 is M2( the carrier of (V))
d9 is M2( the carrier of (V))
[c9,d9] is non empty M2([: the carrier of (V), the carrier of (V):])
t is M2( the carrier of (V))
t9 is M2( the carrier of (V))
[t,t9] is non empty M2([: the carrier of (V), the carrier of (V):])
[[c9,d9],[t,t9]] is non empty M2([:[: the carrier of (V), the carrier of (V):],[: the carrier of (V), the carrier of (V):]:])
[:[: the carrier of (V), the carrier of (V):],[: the carrier of (V), the carrier of (V):]:] is non empty set
the of (V) is V26() V29([: the carrier of (V), the carrier of (V):]) V30([: the carrier of (V), the carrier of (V):]) M2( bool [:[: the carrier of (V), the carrier of (V):],[: the carrier of (V), the carrier of (V):]:])
bool [:[: the carrier of (V), the carrier of (V):],[: the carrier of (V), the carrier of (V):]:] is non empty set
[t9,t] is non empty M2([: the carrier of (V), the carrier of (V):])
[[c9,d9],[t9,t]] is non empty M2([:[: the carrier of (V), the carrier of (V):],[: the carrier of (V), the carrier of (V):]:])
c is M2( the carrier of (V))
d is M2( the carrier of (V))
a9 is M2( the carrier of (V))
b9 is M2( the carrier of V)
c9 is M2( the carrier of V)
d9 is M2( the carrier of V)
t9 is M2( the carrier of V)
[: the carrier of (V), the carrier of (V):] is non empty set
[c,a9] is non empty M2([: the carrier of (V), the carrier of (V):])
t is M2( the carrier of (V))
[d,t] is non empty M2([: the carrier of (V), the carrier of (V):])
[[c,a9],[d,t]] is non empty M2([:[: the carrier of (V), the carrier of (V):],[: the carrier of (V), the carrier of (V):]:])
[:[: the carrier of (V), the carrier of (V):],[: the carrier of (V), the carrier of (V):]:] is non empty set
the of (V) is V26() V29([: the carrier of (V), the carrier of (V):]) V30([: the carrier of (V), the carrier of (V):]) M2( bool [:[: the carrier of (V), the carrier of (V):],[: the carrier of (V), the carrier of (V):]:])
bool [:[: the carrier of (V), the carrier of (V):],[: the carrier of (V), the carrier of (V):]:] is non empty set
[c,d] is non empty M2([: the carrier of (V), the carrier of (V):])
[a9,t] is non empty M2([: the carrier of (V), the carrier of (V):])
[[c,d],[a9,t]] is non empty M2([:[: the carrier of (V), the carrier of (V):],[: the carrier of (V), the carrier of (V):]:])
c is M2( the carrier of (V))
a9 is M2( the carrier of (V))
b9 is M2( the carrier of (V))
d is M2( the carrier of (V))
[: the carrier of (V), the carrier of (V):] is non empty set
[a9,c] is non empty M2([: the carrier of (V), the carrier of (V):])
[c,b9] is non empty M2([: the carrier of (V), the carrier of (V):])
[[a9,c],[c,b9]] is non empty M2([:[: the carrier of (V), the carrier of (V):],[: the carrier of (V), the carrier of (V):]:])
[:[: the carrier of (V), the carrier of (V):],[: the carrier of (V), the carrier of (V):]:] is non empty set
the of (V) is V26() V29([: the carrier of (V), the carrier of (V):]) V30([: the carrier of (V), the carrier of (V):]) M2( bool [:[: the carrier of (V), the carrier of (V):],[: the carrier of (V), the