:: VECTMETR semantic presentation

REAL is non empty V34() V64() V65() V66() V70() set
NAT is V64() V65() V66() V67() V68() V69() V70() Element of bool REAL
bool REAL is non empty set
BOOLEAN is non empty set

RAT is non empty V34() V64() V65() V66() V67() V70() set

1 is non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
{0,1} is non empty V64() V65() V66() V67() V68() V69() set
COMPLEX is non empty V34() V64() V70() set
NAT is V64() V65() V66() V67() V68() V69() V70() set
bool NAT is non empty set
bool NAT is non empty set
K218(NAT) is V49() set
INT is non empty V34() V64() V65() V66() V67() V68() V70() set
is Relation-like V53() V54() V55() set
bool is non empty set
is non empty Relation-like V53() set
bool is non empty set

is non empty Relation-like V53() V54() V55() set
bool is non empty set
is non empty Relation-like V53() V54() V55() set
bool is non empty set
is non empty Relation-like RAT -valued V53() V54() V55() set
bool is non empty set
is non empty Relation-like RAT -valued V53() V54() V55() set
bool is non empty set
is non empty Relation-like RAT -valued INT -valued V53() V54() V55() set
bool is non empty set

bool is non empty set

bool is non empty set
[:1,1:] is non empty Relation-like RAT -valued INT -valued V53() V54() V55() V56() set
bool [:1,1:] is non empty set
[:[:1,1:],1:] is non empty Relation-like RAT -valued INT -valued V53() V54() V55() V56() set
bool [:[:1,1:],1:] is non empty set
[:[:1,1:],REAL:] is non empty Relation-like V53() V54() V55() set
bool [:[:1,1:],REAL:] is non empty set
2 is non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
[:2,2:] is non empty Relation-like RAT -valued INT -valued V53() V54() V55() V56() set
[:[:2,2:],REAL:] is non empty Relation-like V53() V54() V55() set
bool [:[:2,2:],REAL:] is non empty set

the carrier of () is non empty set

3 is non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
Seg 1 is non empty V34() V41(1) V64() V65() V66() V67() V68() V69() Element of bool NAT
{1} is non empty V64() V65() V66() V67() V68() V69() set
Seg 2 is non empty V34() V41(2) V64() V65() V66() V67() V68() V69() Element of bool NAT
{1,2} is non empty V64() V65() V66() V67() V68() V69() set

{0,1} is non empty V64() V65() V66() V67() V68() V69() Element of bool NAT
{0,1} * is non empty functional FinSequence-membered FinSequenceSet of {0,1}

the carrier of n is non empty set
S is Element of the carrier of n
X is Element of the carrier of n
dist (S,X) is V11() real ext-real Element of REAL
[: the carrier of n, the carrier of n:] is non empty Relation-like set
x is Element of [: the carrier of n, the carrier of n:]
y is set
z is set
[y,z] is V26() set
{y,z} is non empty set
{y} is non empty set
{{y,z},{y}} is non empty set
x1 is Element of the carrier of n
1 / 2 is V11() real ext-real non negative Element of REAL
y1 is Element of the carrier of n
dist (x1,y1) is V11() real ext-real Element of REAL
(1 / 2) * (dist (x1,y1)) is V11() real ext-real Element of REAL
1 - (1 / 2) is V11() real ext-real Element of REAL
(1 - (1 / 2)) * (dist (x1,y1)) is V11() real ext-real Element of REAL
z1 is Element of the carrier of n
dist (x1,z1) is V11() real ext-real Element of REAL
dist (z1,y1) is V11() real ext-real Element of REAL
[x1,z1] is V26() Element of [: the carrier of n, the carrier of n:]
{x1,z1} is non empty set
{x1} is non empty set
{{x1,z1},{x1}} is non empty set
f is V26() Element of [: the carrier of n, the carrier of n:]
[z1,y1] is V26() Element of [: the carrier of n, the carrier of n:]
{z1,y1} is non empty set
{z1} is non empty set
{{z1,y1},{z1}} is non empty set
f2 is V26() Element of [: the carrier of n, the carrier of n:]
f3 is Element of the carrier of n
g is Element of the carrier of n
[f3,g] is V26() Element of [: the carrier of n, the carrier of n:]
{f3,g} is non empty set
{f3} is non empty set
{{f3,g},{f3}} is non empty set
dist (f3,g) is V11() real ext-real Element of REAL
[f3,z1] is V26() Element of [: the carrier of n, the carrier of n:]
{f3,z1} is non empty set
{{f3,z1},{f3}} is non empty set
[z1,g] is V26() Element of [: the carrier of n, the carrier of n:]
{z1,g} is non empty set
{{z1,g},{z1}} is non empty set
dist (f3,z1) is V11() real ext-real Element of REAL
2 * (dist (f3,z1)) is V11() real ext-real Element of REAL
dist (z1,g) is V11() real ext-real Element of REAL
2 * (dist (z1,g)) is V11() real ext-real Element of REAL
{0,1} is non empty V64() V65() V66() V67() V68() V69() Element of bool REAL
{0,1} * is non empty functional FinSequence-membered FinSequenceSet of {0,1}
[S,X] is V26() Element of [: the carrier of n, the carrier of n:]
{S,X} is non empty set
{S} is non empty set
{{S,X},{S}} is non empty set

x is Relation-like [: the carrier of n, the carrier of n:] -valued Function-like DecoratedTree-like binary set
proj1 x is non empty Tree-like set
x . {} is set
z is V11() real ext-real Element of REAL
(dist (S,X)) / z is V11() real ext-real Element of REAL
log (2,1) is V11() real ext-real Element of REAL
log (2,((dist (S,X)) / z)) is V11() real ext-real Element of REAL
[\(log (2,((dist (S,X)) / z)))/] is V11() real integer ext-real set
x1 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
x1 + 1 is non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
y1 is non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
2 to_power y1 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
z1 is non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
(dist (S,X)) / z1 is V11() real ext-real Element of REAL

y -level y1 is V34() Level of y

f3 is Relation-like NAT -defined [: the carrier of n, the carrier of n:] -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of [: the carrier of n, the carrier of n:]
len f3 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
dom f3 is V64() V65() V66() V67() V68() V69() Element of bool NAT
Seg z1 is non empty V34() V41(z1) V64() V65() V66() V67() V68() V69() Element of bool NAT
g is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT

{ } is set

Seg g is V34() V41(g) V64() V65() V66() V67() V68() V69() Element of bool NAT

is non empty functional V64() V65() V66() V67() V68() V69() set
[:(Seg g),:] is Relation-like RAT -valued INT -valued V53() V54() V55() V56() set
bool [:(Seg g),:] is non empty set
x . (0* g) is set
(x . (0* g)) `1 is set
g + 1 is non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT

REAL (g + 1) is non empty functional FinSequence-membered FinSequenceSet of REAL

{ } is set

Seg (g + 1) is non empty V34() V41(g + 1) V64() V65() V66() V67() V68() V69() Element of bool NAT
K153((Seg (g + 1)),0) is non empty Relation-like Seg (g + 1) -defined RAT -valued INT -valued -valued Function-like total quasi_total V34() FinSequence-like FinSubsequence-like V53() V54() V55() V56() Element of bool [:(Seg (g + 1)),:]
[:(Seg (g + 1)),:] is non empty Relation-like RAT -valued INT -valued V53() V54() V55() V56() set
bool [:(Seg (g + 1)),:] is non empty set
x . (0* (g + 1)) is set
(x . (0* (g + 1))) `1 is set

x . g2 is Element of [: the carrier of n, the carrier of n:]
g3 is set
a is set
[g3,a] is V26() set
{g3,a} is non empty set
{g3} is non empty set
{{g3,a},{g3}} is non empty set

x . (g2 ^ ) is set
c is Element of the carrier of n

x . (g2 ^ <*1*>) is set
c1 is Element of the carrier of n
dist (c,c1) is V11() real ext-real Element of REAL
(x . (g2 ^ )) `1 is set
j is Element of the carrier of n
[c,j] is V26() Element of [: the carrier of n, the carrier of n:]
{c,j} is non empty set
{c} is non empty set
{{c,j},{c}} is non empty set
[j,c1] is V26() Element of [: the carrier of n, the carrier of n:]
{j,c1} is non empty set
{j} is non empty set
{{j,c1},{j}} is non empty set
dist (c,j) is V11() real ext-real Element of REAL
2 * (dist (c,j)) is V11() real ext-real Element of REAL
dist (j,c1) is V11() real ext-real Element of REAL
2 * (dist (j,c1)) is V11() real ext-real Element of REAL

{ } is set

is non empty functional V64() V65() V66() V67() V68() V69() set

bool [:(),:] is non empty set
x . () is set
(x . ()) `1 is set
0 + 1 is non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
len (FinSeqLevel (y1,y)) is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT

{ } is set

Seg g is non empty V34() V41(g) V64() V65() V66() V67() V68() V69() Element of bool NAT

[:(Seg g),:] is non empty Relation-like RAT -valued INT -valued V53() V54() V55() V56() set
bool [:(Seg g),:] is non empty set
g + 1 is non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT

REAL (g + 1) is non empty functional FinSequence-membered FinSequenceSet of REAL

{ } is set

Seg (g + 1) is non empty V34() V41(g + 1) V64() V65() V66() V67() V68() V69() Element of bool NAT
K153((Seg (g + 1)),0) is non empty Relation-like Seg (g + 1) -defined RAT -valued INT -valued -valued Function-like total quasi_total V34() FinSequence-like FinSubsequence-like V53() V54() V55() V56() Element of bool [:(Seg (g + 1)),:]
[:(Seg (g + 1)),:] is non empty Relation-like RAT -valued INT -valued V53() V54() V55() V56() set
bool [:(Seg (g + 1)),:] is non empty set

x . ('not' g2) is set
(x . ('not' g2)) `2 is set

{ } is set

K371(g,1) is non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT

x . ('not' g3) is set
(x . ('not' g3)) `2 is set
len g3 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
(len g3) + 1 is non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
g2 . ((len g3) + 1) is set

1 - a is set

x . c is Element of [: the carrier of n, the carrier of n:]
c1 is set
j is set
[c1,j] is V26() set
{c1,j} is non empty set
{c1} is non empty set
{{c1,j},{c1}} is non empty set

x . () is set
FSL1j is Element of the carrier of n

x . (c ^ <*1*>) is set
DF1 is Element of the carrier of n
dist (FSL1j,DF1) is V11() real ext-real Element of REAL
DF2 is Element of the carrier of n
[FSL1j,DF2] is V26() Element of [: the carrier of n, the carrier of n:]
{FSL1j,DF2} is non empty set
{FSL1j} is non empty set
{{FSL1j,DF2},{FSL1j}} is non empty set
[DF2,DF1] is V26() Element of [: the carrier of n, the carrier of n:]
{DF2,DF1} is non empty set
{DF2} is non empty set
{{DF2,DF1},{DF2}} is non empty set
dist (FSL1j,DF2) is V11() real ext-real Element of REAL
2 * (dist (FSL1j,DF2)) is V11() real ext-real Element of REAL
dist (DF2,DF1) is V11() real ext-real Element of REAL
2 * (dist (DF2,DF1)) is V11() real ext-real Element of REAL

{ } is set

[:(Seg 1),:] is non empty Relation-like RAT -valued INT -valued V53() V54() V55() V56() set
bool [:(Seg 1),:] is non empty set

x . ('not' g2) is set
(x . ('not' g2)) `2 is set

x . () is set

x . (g ^ <*1*>) is set
(x . (g ^ <*1*>)) `2 is set
g3 is Element of the carrier of n
[S,g3] is V26() Element of [: the carrier of n, the carrier of n:]
{S,g3} is non empty set
{{S,g3},{S}} is non empty set
[g3,X] is V26() Element of [: the carrier of n, the carrier of n:]
{g3,X} is non empty set
{g3} is non empty set
{{g3,X},{g3}} is non empty set
dist (S,g3) is V11() real ext-real Element of REAL
2 * (dist (S,g3)) is V11() real ext-real Element of REAL
dist (g3,X) is V11() real ext-real Element of REAL
2 * (dist (g3,X)) is V11() real ext-real Element of REAL

len g is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
dom g is V64() V65() V66() V67() V68() V69() Element of bool NAT
<*X*> is non empty Relation-like NAT -defined the carrier of n -valued Function-like V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of the carrier of n

g2 is non empty Relation-like NAT -defined the carrier of n -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
g2 /. 1 is Element of the carrier of n
len g2 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
g2 /. (len g2) is Element of the carrier of n
(len g2) - 1 is V11() real integer ext-real Element of REAL
len <*X*> is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
(len g) + () is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
(len g) + 1 is non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
z1 + 1 is non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
g2 . 1 is set
g . 1 is set
f3 /. 1 is Element of [: the carrier of n, the carrier of n:]
(f3 /. 1) `1 is Element of the carrier of n
f3 . 1 is set
(f3 . 1) `1 is set
f2 /. 1 is Element of proj1 x
x . (f2 /. 1) is Element of [: the carrier of n, the carrier of n:]
(x . (f2 /. 1)) `1 is Element of the carrier of n
(FinSeqLevel (y1,y)) . 1 is set
x . ((FinSeqLevel (y1,y)) . 1) is set
(x . ((FinSeqLevel (y1,y)) . 1)) `1 is set

{ } is set

Seg y1 is non empty V34() V41(y1) V64() V65() V66() V67() V68() V69() Element of bool NAT

[:(Seg y1),:] is non empty Relation-like RAT -valued INT -valued V53() V54() V55() V56() set
bool [:(Seg y1),:] is non empty set
x . (0* y1) is set
(x . (0* y1)) `1 is set
Seg (len g2) is V34() V41( len g2) V64() V65() V66() V67() V68() V69() Element of bool NAT
dom g2 is non empty V64() V65() V66() V67() V68() V69() Element of bool NAT
(g ^ <*X*>) . ((len g) + 1) is set

{ } is set

c is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
g2 /. c is Element of the carrier of n
c + 1 is non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
g2 /. (c + 1) is Element of the carrier of n
dist ((g2 /. c),(g2 /. (c + 1))) is V11() real ext-real Element of REAL
len f2 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
(len g2) -' 1 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
(c + 1) - 1 is V11() real integer ext-real Element of REAL
(2 to_power y1) - 1 is V11() real integer ext-real Element of REAL
c1 is non empty ordinal natural V11() real integer ext-real positive non negative set
2 to_power c1 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
(2 to_power c1) - 1 is V11() real integer ext-real Element of REAL

y -level c1 is Level of y
c1 + 1 is non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
2 to_power (c1 + 1) is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
(2 to_power (c1 + 1)) - 1 is V11() real integer ext-real Element of REAL
FinSeqLevel ((c1 + 1),y) is Relation-like NAT -defined y -level (c1 + 1) -valued Function-like one-to-one V34() FinSequence-like FinSubsequence-like FinSequence of y -level (c1 + 1)
y -level (c1 + 1) is V34() Level of y

DF1 + 1 is non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
(FinSeqLevel ((c1 + 1),y)) . (DF1 + 1) is set
x . ((FinSeqLevel ((c1 + 1),y)) . (DF1 + 1)) is set
(x . ((FinSeqLevel ((c1 + 1),y)) . (DF1 + 1))) `1 is set
(FinSeqLevel ((c1 + 1),y)) . DF1 is set
x . ((FinSeqLevel ((c1 + 1),y)) . DF1) is set
(x . ((FinSeqLevel ((c1 + 1),y)) . DF1)) `2 is set
1 + 1 is non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
(DF1 + 1) div 2 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
(2 to_power (c1 + 1)) -' 1 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
((2 to_power (c1 + 1)) -' 1) + 1 is non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
((2 to_power (c1 + 1)) - 1) + 1 is V11() real integer ext-real Element of REAL
2 to_power 1 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
(2 to_power c1) * (2 to_power 1) is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
(2 to_power c1) * 2 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
(DF1 + 1) + 1 is non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
((DF1 + 1) + 1) div 2 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
Seg (2 to_power c1) is V34() V41(2 to_power c1) V64() V65() V66() V67() V68() V69() Element of bool NAT
j is non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT

y -level j is V34() Level of y
dom (FinSeqLevel (j,y)) is V64() V65() V66() V67() V68() V69() Element of bool NAT
(FinSeqLevel (c1,y)) . (((DF1 + 1) + 1) div 2) is set
FSL1j is non empty set
(FinSeqLevel (j,y)) . (((DF1 + 1) + 1) div 2) is set

{ } is set

x . FSLlprim is Element of [: the carrier of n, the carrier of n:]
Fj is set
FSLl1 is set
[Fj,FSLl1] is V26() set
{Fj,FSLl1} is non empty set
{Fj} is non empty set
{{Fj,FSLl1},{Fj}} is non empty set
(FinSeqLevel (c1,y)) . ((DF1 + 1) div 2) is set
(FinSeqLevel (j,y)) . ((DF1 + 1) div 2) is set

x . DF1 is Element of [: the carrier of n, the carrier of n:]
DF2 is set
NFSLl is set
[DF2,NFSLl] is V26() set
{DF2,NFSLl} is non empty set
{DF2} is non empty set
{{DF2,NFSLl},{DF2}} is non empty set

x . (DF1 ^ ) is set
x1 is Element of the carrier of n

x . (DF1 ^ <*1*>) is set
y1 is Element of the carrier of n
dist (x1,y1) is V11() real ext-real Element of REAL
b is Element of the carrier of n
[x1,b] is V26() Element of [: the carrier of n, the carrier of n:]
{x1,b} is non empty set
{x1} is non empty set
{{x1,b},{x1}} is non empty set
[b,y1] is V26() Element of [: the carrier of n, the carrier of n:]
{b,y1} is non empty set
{b} is non empty set
{{b,y1},{b}} is non empty set
dist (x1,b) is V11() real ext-real Element of REAL
2 * (dist (x1,b)) is V11() real ext-real Element of REAL
dist (b,y1) is V11() real ext-real Element of REAL
2 * (dist (b,y1)) is V11() real ext-real Element of REAL

x . (FSLlprim ^ ) is set
x1 is Element of the carrier of n

x . (FSLlprim ^ <*1*>) is set
y1 is Element of the carrier of n
dist (x1,y1) is V11() real ext-real Element of REAL
d9 is Element of the carrier of n
[x1,d9] is V26() Element of [: the carrier of n, the carrier of n:]
{x1,d9} is non empty set
{x1} is non empty set
{{x1,d9},{x1}} is non empty set
[d9,y1] is V26() Element of [: the carrier of n, the carrier of n:]
{d9,y1} is non empty set
{d9} is non empty set
{{d9,y1},{d9}} is non empty set
dist (x1,d9) is V11() real ext-real Element of REAL
2 * (dist (x1,d9)) is V11() real ext-real Element of REAL
dist (d9,y1) is V11() real ext-real Element of REAL
2 * (dist (d9,y1)) is V11() real ext-real Element of REAL
(DF1 + 1) - 1 is V11() real integer ext-real Element of REAL
(DF1 + 1) -' 1 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
DF1 mod 2 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
(DF1 + 1) mod 2 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
2 * 1 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
(2 * 1) + DF1 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
((2 * 1) + DF1) mod 2 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
<*(((2 * 1) + DF1) mod 2)*> is non empty Relation-like NAT -defined Function-like V34() V41(1) FinSequence-like FinSubsequence-like set
FSLlprim ^ <*(((2 * 1) + DF1) mod 2)*> is non empty Relation-like NAT -defined Function-like V34() V41(c1 + 1) FinSequence-like FinSubsequence-like set
x . (FSLlprim ^ <*(((2 * 1) + DF1) mod 2)*>) is set
(x . (FSLlprim ^ <*(((2 * 1) + DF1) mod 2)*>)) `1 is set
FSLlprim ^ <*1*> is non empty Relation-like NAT -defined Function-like V34() V41(c1 + 1) FinSequence-like FinSubsequence-like set
x . (FSLlprim ^ <*1*>) is set
(x . (FSLlprim ^ <*1*>)) `1 is set

x . () is set
(x . ()) `2 is set
DF2 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
DF2 + 1 is non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
(DF2 + 1) mod 2 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
<*((DF2 + 1) mod 2)*> is non empty Relation-like NAT -defined Function-like V34() V41(1) FinSequence-like FinSubsequence-like set
d ^ <*((DF2 + 1) mod 2)*> is non empty Relation-like NAT -defined Function-like V34() V41(c1 + 1) FinSequence-like FinSubsequence-like set
x . (d ^ <*((DF2 + 1) mod 2)*>) is set
(x . (d ^ <*((DF2 + 1) mod 2)*>)) `2 is set
(FinSeqLevel ((c1 + 1),y)) . DF2 is set
x . ((FinSeqLevel ((c1 + 1),y)) . DF2) is set
(x . ((FinSeqLevel ((c1 + 1),y)) . DF2)) `2 is set
DF1 mod 2 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
DF1 -' 1 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
(DF1 -' 1) mod 2 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
2 * 1 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
(DF1 -' 1) + (2 * 1) is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
((DF1 -' 1) + (2 * 1)) mod 2 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
(DF1 -' 1) + 1 is non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
((DF1 -' 1) + 1) + 1 is non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
(((DF1 -' 1) + 1) + 1) mod 2 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
(DF1 + 1) mod 2 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
1 + DF1 is non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
1 + (1 + DF1) is non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
(1 + 1) + (DF1 -' 1) is non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
DF1 - 1 is V11() real integer ext-real Element of REAL
(1 + 1) + (DF1 - 1) is V11() real integer ext-real Element of REAL
(1 + 1) + DF1 is non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
((1 + 1) + DF1) - 1 is V11() real integer ext-real Element of REAL
((1 + 1) + DF1) -' 1 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
(((1 + 1) + DF1) -' 1) mod 2 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
((1 + 1) + DF1) mod 2 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
2 * (((DF1 + 1) + 1) div 2) is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
(2 * (((DF1 + 1) + 1) div 2)) + 0 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
((DF1 + 1) + 1) -' 1 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
(((DF1 + 1) + 1) -' 1) div 2 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
(((DF1 + 1) + 1) div 2) - 1 is V11() real integer ext-real Element of REAL
((DF1 + 1) div 2) + 1 is non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
x . ((FinSeqLevel (c1,y)) . (((DF1 + 1) + 1) div 2)) is set
(x . ((FinSeqLevel (c1,y)) . (((DF1 + 1) + 1) div 2))) `1 is set
x . ((FinSeqLevel (c1,y)) . ((DF1 + 1) div 2)) is set
(x . ((FinSeqLevel (c1,y)) . ((DF1 + 1) div 2))) `2 is set
(2 * 1) + DF1 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
((2 * 1) + DF1) mod 2 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
<*(((2 * 1) + DF1) mod 2)*> is non empty Relation-like NAT -defined Function-like V34() V41(1) FinSequence-like FinSubsequence-like set
FSLlprim ^ <*(((2 * 1) + DF1) mod 2)*> is non empty Relation-like NAT -defined Function-like V34() V41(c1 + 1) FinSequence-like FinSubsequence-like set
x . (FSLlprim ^ <*(((2 * 1) + DF1) mod 2)*>) is set
(x . (FSLlprim ^ <*(((2 * 1) + DF1) mod 2)*>)) `1 is set

x . (FSLlprim ^ ) is set
(x . (FSLlprim ^ )) `1 is set

x . (d ^ <*1*>) is set
(x . (d ^ <*1*>)) `2 is set
DF2 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
(FinSeqLevel ((c1 + 1),y)) . DF2 is set
x . ((FinSeqLevel ((c1 + 1),y)) . DF2) is set
(x . ((FinSeqLevel ((c1 + 1),y)) . DF2)) `2 is set
DF2 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
(FinSeqLevel ((c1 + 1),y)) . DF2 is set
x . ((FinSeqLevel ((c1 + 1),y)) . DF2) is set
(x . ((FinSeqLevel ((c1 + 1),y)) . DF2)) `2 is set
DF2 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
(FinSeqLevel ((c1 + 1),y)) . DF2 is set
x . ((FinSeqLevel ((c1 + 1),y)) . DF2) is set
(x . ((FinSeqLevel ((c1 + 1),y)) . DF2)) `2 is set
2 to_power 1 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
(2 to_power 1) - 1 is V11() real integer ext-real Element of REAL

y -level 1 is V34() Level of y

j + 1 is non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
(FinSeqLevel (1,y)) . (j + 1) is set
x . ((FinSeqLevel (1,y)) . (j + 1)) is set
(x . ((FinSeqLevel (1,y)) . (j + 1))) `1 is set
(FinSeqLevel (1,y)) . j is set
x . ((FinSeqLevel (1,y)) . j) is set
(x . ((FinSeqLevel (1,y)) . j)) `2 is set
1 + 1 is non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
(1 + 1) - 1 is V11() real integer ext-real Element of REAL

x . (c1 ^ ) is set

x . (c1 ^ <*1*>) is set
FSL1j is Element of the carrier of n
[S,FSL1j] is V26() Element of [: the carrier of n, the carrier of n:]
{S,FSL1j} is non empty set
{{S,FSL1j},{S}} is non empty set
[FSL1j,X] is V26() Element of [: the carrier of n, the carrier of n:]
{FSL1j,X} is non empty set
{FSL1j} is non empty set
{{FSL1j,X},{FSL1j}} is non empty set
dist (S,FSL1j) is V11() real ext-real Element of REAL
2 * (dist (S,FSL1j)) is V11() real ext-real Element of REAL
dist (FSL1j,X) is V11() real ext-real Element of REAL
2 * (dist (FSL1j,X)) is V11() real ext-real Element of REAL
x . <*1*> is set
(x . <*1*>) `1 is set
(x . (c1 ^ <*1*>)) `1 is set
(x . (c1 ^ )) `2 is set
x . is set
() `2 is set
1 + c is non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
Seg (len g) is V34() V41( len g) V64() V65() V66() V67() V68() V69() Element of bool NAT
g /. (c + 1) is Element of the carrier of n
g . (c + 1) is set
f3 /. (c + 1) is Element of [: the carrier of n, the carrier of n:]
(f3 /. (c + 1)) `1 is Element of the carrier of n
f3 . (c + 1) is set
(f3 . (c + 1)) `1 is set
f2 /. (c + 1) is Element of proj1 x
x . (f2 /. (c + 1)) is Element of [: the carrier of n, the carrier of n:]
(x . (f2 /. (c + 1))) `1 is Element of the carrier of n
(FinSeqLevel (y1,y)) . (c + 1) is set
x . ((FinSeqLevel (y1,y)) . (c + 1)) is set
(x . ((FinSeqLevel (y1,y)) . (c + 1))) `1 is set
(FinSeqLevel (y1,y)) . c is set
x . ((FinSeqLevel (y1,y)) . c) is set
(x . ((FinSeqLevel (y1,y)) . c)) `2 is set

x . () is set
(x . ()) `2 is set
(FinSeqLevel (y1,y)) . c is set
x . ((FinSeqLevel (y1,y)) . c) is set
(x . ((FinSeqLevel (y1,y)) . c)) `2 is set
(FinSeqLevel (y1,y)) . c is set
x . ((FinSeqLevel (y1,y)) . c) is set
(x . ((FinSeqLevel (y1,y)) . c)) `2 is set
(FinSeqLevel (y1,y)) . c is set
x . ((FinSeqLevel (y1,y)) . c) is set
(x . ((FinSeqLevel (y1,y)) . c)) `2 is set
c1 is non empty ordinal natural V11() real integer ext-real positive non negative set
2 to_power c1 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT

y -level c1 is Level of y
(dist (S,X)) / (2 to_power c1) is V11() real ext-real Element of REAL
c1 + 1 is non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
2 to_power (c1 + 1) is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
FinSeqLevel ((c1 + 1),y) is Relation-like NAT -defined y -level (c1 + 1) -valued Function-like one-to-one V34() FinSequence-like FinSubsequence-like FinSequence of y -level (c1 + 1)
y -level (c1 + 1) is V34() Level of y
(dist (S,X)) / (2 to_power (c1 + 1)) is V11() real ext-real Element of REAL
DF2 is non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
(FinSeqLevel ((c1 + 1),y)) . DF2 is set
x . ((FinSeqLevel ((c1 + 1),y)) . DF2) is set
(x . ((FinSeqLevel ((c1 + 1),y)) . DF2)) `1 is set
(x . ((FinSeqLevel ((c1 + 1),y)) . DF2)) `2 is set
DF2 + 1 is non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
(DF2 + 1) div 2 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
1 + 1 is non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
2 to_power 1 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
(2 to_power c1) * (2 to_power 1) is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
(2 to_power c1) * 2 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
b is non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
Seg (2 to_power c1) is V34() V41(2 to_power c1) V64() V65() V66() V67() V68() V69() Element of bool NAT
FSL1j is non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT

y -level FSL1j is V34() Level of y
dom (FinSeqLevel (FSL1j,y)) is V64() V65() V66() V67() V68() V69() Element of bool NAT
(FinSeqLevel (c1,y)) . ((DF2 + 1) div 2) is set
j is non empty set
(FinSeqLevel (FSL1j,y)) . ((DF2 + 1) div 2) is set

{ } is set

Seg (2 to_power (c1 + 1)) is V34() V41(2 to_power (c1 + 1)) V64() V65() V66() V67() V68() V69() Element of bool NAT
dom (FinSeqLevel ((c1 + 1),y)) is V64() V65() V66() V67() V68() V69() Element of bool NAT
DF1 is non empty set

K371(c1,1) is non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
DF1 is Element of the carrier of n
DF2 is Element of the carrier of n
dist (DF1,DF2) is V11() real ext-real Element of REAL

x . Fj is Element of [: the carrier of n, the carrier of n:]
[DF1,DF2] is V26() Element of [: the carrier of n, the carrier of n:]
{DF1,DF2} is non empty set
{DF1} is non empty set
{{DF1,DF2},{DF1}} is non empty set

x . NFSLl is Element of [: the carrier of n, the carrier of n:]
x1 is set
y1 is set
[x1,y1] is V26() set
{x1,y1} is non empty set
{x1} is non empty set
{{x1,y1},{x1}} is non empty set

x . (NFSLl ^ ) is set
x1 is Element of the carrier of n

x . (NFSLl ^ <*1*>) is set
y1 is Element of the carrier of n
dist (x1,y1) is V11() real ext-real Element of REAL
b is Element of the carrier of n
[x1,b] is V26() Element of [: the carrier of n, the carrier of n:]
{x1,b} is non empty set
{x1} is non empty set
{{x1,b},{x1}} is non empty set
[b,y1] is V26() Element of [: the carrier of n, the carrier of n:]
{b,y1} is non empty set
{b} is non empty set
{{b,y1},{b}} is non empty set
dist (x1,b) is V11() real ext-real Element of REAL
2 * (dist (x1,b)) is V11() real ext-real Element of REAL
dist (b,y1) is V11() real ext-real Element of REAL
2 * (dist (b,y1)) is V11() real ext-real Element of REAL
FSL1j + 1 is non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
FinSeqLevel ((FSL1j + 1),y) is Relation-like NAT -defined y -level (FSL1j + 1) -valued Function-like one-to-one V34() FinSequence-like FinSubsequence-like FinSequence of y -level (FSL1j + 1)
y -level (FSL1j + 1) is V34() Level of y
(FinSeqLevel ((FSL1j + 1),y)) . DF2 is set

(DF2 + 1) mod 2 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
<*((DF2 + 1) mod 2)*> is non empty Relation-like NAT -defined Function-like V34() V41(1) FinSequence-like FinSubsequence-like set
FSLlprim ^ <*((DF2 + 1) mod 2)*> is non empty Relation-like NAT -defined Function-like V34() V41(c1 + 1) FinSequence-like FinSubsequence-like set
(FinSeqLevel (c1,y)) . b is set
x . ((FinSeqLevel (c1,y)) . b) is set
(x . ((FinSeqLevel (c1,y)) . b)) `1 is set
(x . ((FinSeqLevel (c1,y)) . b)) `2 is set
2 * (dist (DF1,DF2)) is V11() real ext-real Element of REAL
((dist (S,X)) / (2 to_power c1)) / 2 is V11() real ext-real Element of REAL
(((dist (S,X)) / (2 to_power c1)) / 2) * 2 is V11() real ext-real Element of REAL
(dist (S,X)) / ((2 to_power c1) * 2) is V11() real ext-real Element of REAL
(dist (S,X)) / ((2 to_power c1) * (2 to_power 1)) is V11() real ext-real Element of REAL
2 * (dist (DF1,DF2)) is V11() real ext-real Element of REAL
((dist (S,X)) / (2 to_power c1)) / 2 is V11() real ext-real Element of REAL
(((dist (S,X)) / (2 to_power c1)) / 2) * 2 is V11() real ext-real Element of REAL
(dist (S,X)) / ((2 to_power c1) * 2) is V11() real ext-real Element of REAL
(dist (S,X)) / ((2 to_power c1) * (2 to_power 1)) is V11() real ext-real Element of REAL
2 to_power 1 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT

y -level 1 is V34() Level of y
(dist (S,X)) / (2 to_power 1) is V11() real ext-real Element of REAL

j is non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
(FinSeqLevel (1,y)) . j is set
x . ((FinSeqLevel (1,y)) . j) is set
(x . ((FinSeqLevel (1,y)) . j)) `1 is set
(x . ((FinSeqLevel (1,y)) . j)) `2 is set
Seg (2 to_power 1) is V34() V41(2 to_power 1) V64() V65() V66() V67() V68() V69() Element of bool NAT
dom (FinSeqLevel (1,y)) is V64() V65() V66() V67() V68() V69() Element of bool NAT
DF1 is Element of the carrier of n
DF2 is Element of the carrier of n
dist (DF1,DF2) is V11() real ext-real Element of REAL

x . (c1 ^ ) is set

x . (c1 ^ <*1*>) is set
x . is set

x . FSL1j is Element of [: the carrier of n, the carrier of n:]
[DF1,DF2] is V26() Element of [: the carrier of n, the carrier of n:]
{DF1,DF2} is non empty set
{DF1} is non empty set
{{DF1,DF2},{DF1}} is non empty set
b is Element of the carrier of n
[S,b] is V26() Element of [: the carrier of n, the carrier of n:]
{S,b} is non empty set
{{S,b},{S}} is non empty set
[b,X] is V26() Element of [: the carrier of n, the carrier of n:]
{b,X} is non empty set
{b} is non empty set
{{b,X},{b}} is non empty set
dist (S,b) is V11() real ext-real Element of REAL
2 * (dist (S,b)) is V11() real ext-real Element of REAL
dist (b,X) is V11() real ext-real Element of REAL
2 * (dist (b,X)) is V11() real ext-real Element of REAL
(dist (S,X)) / 2 is V11() real ext-real Element of REAL
b is