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
0 is empty ordinal natural V11() real integer Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V34() FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V53() V54() V55() V56() V63() V64() V65() V66() V67() V68() V69() V70() with_common_domain Element of NAT
RAT is non empty V34() V64() V65() V66() V67() V70() set
the empty Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V34() FinSequence-like FinSubsequence-like FinSequence-membered V53() V54() V55() V56() V64() V65() V66() V67() V68() V69() V70() with_common_domain set is empty Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V34() FinSequence-like FinSubsequence-like FinSequence-membered V53() V54() V55() V56() V64() V65() V66() V67() V68() V69() V70() with_common_domain 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
[:NAT,REAL:] is Relation-like V53() V54() V55() set
bool [:NAT,REAL:] is non empty set
[:COMPLEX,COMPLEX:] is non empty Relation-like V53() set
bool [:COMPLEX,COMPLEX:] is non empty set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty Relation-like V53() set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty set
[:REAL,REAL:] is non empty Relation-like V53() V54() V55() set
bool [:REAL,REAL:] is non empty set
[:[:REAL,REAL:],REAL:] is non empty Relation-like V53() V54() V55() set
bool [:[:REAL,REAL:],REAL:] is non empty set
[:RAT,RAT:] is non empty Relation-like RAT -valued V53() V54() V55() set
bool [:RAT,RAT:] is non empty set
[:[:RAT,RAT:],RAT:] is non empty Relation-like RAT -valued V53() V54() V55() set
bool [:[:RAT,RAT:],RAT:] is non empty set
[:INT,INT:] is non empty Relation-like RAT -valued INT -valued V53() V54() V55() set
bool [:INT,INT:] is non empty set
[:[:INT,INT:],INT:] is non empty Relation-like RAT -valued INT -valued V53() V54() V55() set
bool [:[:INT,INT:],INT:] is non empty set
[:NAT,NAT:] is Relation-like RAT -valued INT -valued V53() V54() V55() V56() set
[:[:NAT,NAT:],NAT:] is Relation-like RAT -valued INT -valued V53() V54() V55() V56() set
bool [:[:NAT,NAT:],NAT:] 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
TOP-REAL 2 is non empty TopSpace-like right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V200() L15()
the carrier of (TOP-REAL 2) is non empty set
{} is empty Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V34() FinSequence-like FinSubsequence-like FinSequence-membered V53() V54() V55() V56() V64() V65() V66() V67() V68() V69() V70() with_common_domain 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
BOOLEAN * is non empty functional FinSequence-membered FinSequenceSet of BOOLEAN
FALSE is boolean Element of BOOLEAN
<*FALSE*> is non empty Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
'not' <*FALSE*> is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
TRUE is boolean Element of BOOLEAN
<*TRUE*> is non empty Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
{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}
<*0*> is non empty Relation-like NAT -defined NAT -valued Function-like V34() V41(1) FinSequence-like FinSubsequence-like V53() V54() V55() V56() FinSequence of NAT
<*1*> is non empty Relation-like NAT -defined NAT -valued Function-like V34() V41(1) FinSequence-like FinSubsequence-like V53() V54() V55() V56() FinSequence of NAT
n is non empty Reflexive discerning symmetric triangle Discerning MetrStruct
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
<*0*> is non empty Relation-like NAT -defined REAL -valued Function-like V34() V41(1) FinSequence-like FinSubsequence-like V53() V54() V55() FinSequence of REAL
<*1*> is non empty Relation-like NAT -defined REAL -valued Function-like V34() V41(1) FinSequence-like FinSubsequence-like V53() V54() V55() FinSequence of REAL
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 is non empty Tree-like finite-order binary full set
FinSeqLevel (y1,y) is Relation-like NAT -defined y -level y1 -valued Function-like one-to-one V34() FinSequence-like FinSubsequence-like FinSequence of y -level y1
y -level y1 is V34() Level of y
f2 is Relation-like NAT -defined proj1 x -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of proj1 x
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
0* g is Relation-like NAT -defined REAL -valued Function-like V34() V41(g) FinSequence-like FinSubsequence-like V53() V54() V55() Element of REAL g
REAL g is non empty functional FinSequence-membered FinSequenceSet of REAL
g -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
REAL * is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V34() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = g } is set
g |-> 0 is Relation-like empty-yielding NAT -defined REAL -valued Function-like V34() V41(g) FinSequence-like FinSubsequence-like V53() V54() V55() Element of g -tuples_on REAL
Seg g is V34() V41(g) V64() V65() V66() V67() V68() V69() Element of bool NAT
K153((Seg g),0) is Relation-like Seg g -defined RAT -valued INT -valued {0} -valued Function-like total quasi_total V34() FinSequence-like FinSubsequence-like V53() V54() V55() V56() Element of bool [:(Seg g),{0}:]
{0} is non empty functional V64() V65() V66() V67() V68() V69() set
[:(Seg g),{0}:] is Relation-like RAT -valued INT -valued V53() V54() V55() V56() set
bool [:(Seg g),{0}:] 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
0* (g + 1) is Relation-like NAT -defined REAL -valued Function-like V34() V41(g + 1) FinSequence-like FinSubsequence-like V53() V54() V55() Element of REAL (g + 1)
REAL (g + 1) is non empty functional FinSequence-membered FinSequenceSet of REAL
(g + 1) -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V34() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = g + 1 } is set
(g + 1) |-> 0 is Relation-like empty-yielding NAT -defined REAL -valued Function-like V34() V41(g + 1) FinSequence-like FinSubsequence-like V53() V54() V55() Element of (g + 1) -tuples_on REAL
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 {0} -valued Function-like total quasi_total V34() FinSequence-like FinSubsequence-like V53() V54() V55() V56() Element of bool [:(Seg (g + 1)),{0}:]
[:(Seg (g + 1)),{0}:] is non empty Relation-like RAT -valued INT -valued V53() V54() V55() V56() set
bool [:(Seg (g + 1)),{0}:] is non empty set
x . (0* (g + 1)) is set
(x . (0* (g + 1))) `1 is set
g2 is Relation-like NAT -defined NAT -valued Function-like V34() FinSequence-like FinSubsequence-like V53() V54() V55() V56() Element of proj1 x
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
g2 ^ <*0*> is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
x . (g2 ^ <*0*>) is set
c is Element of the carrier of n
g2 ^ <*1*> is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
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 ^ <*0*>)) `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
0* 0 is Relation-like NAT -defined REAL -valued Function-like V34() V41( 0 ) FinSequence-like FinSubsequence-like V53() V54() V55() Element of REAL 0
REAL 0 is non empty functional FinSequence-membered FinSequenceSet of REAL
0 -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
REAL * is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V34() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = 0 } is set
0 |-> 0 is Relation-like empty-yielding NAT -defined REAL -valued Function-like V34() V41( 0 ) FinSequence-like FinSubsequence-like V53() V54() V55() Element of 0 -tuples_on REAL
Seg 0 is empty Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V34() V41( 0 ) FinSequence-like FinSubsequence-like FinSequence-membered V53() V54() V55() V56() V64() V65() V66() V67() V68() V69() V70() with_common_domain Element of bool NAT
K153((Seg 0),0) is empty Relation-like non-empty empty-yielding Seg 0 -defined RAT -valued INT -valued {0} -valued Function-like one-to-one constant functional total quasi_total V34() FinSequence-like FinSubsequence-like FinSequence-membered V53() V54() V55() V56() V64() V65() V66() V67() V68() V69() V70() with_common_domain Element of bool [:(Seg 0),{0}:]
{0} is non empty functional V64() V65() V66() V67() V68() V69() set
[:(Seg 0),{0}:] is Relation-like RAT -valued INT -valued V53() V54() V55() V56() set
bool [:(Seg 0),{0}:] is non empty set
x . (0* 0) is set
(x . (0* 0)) `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
g is non empty ordinal natural V11() real integer ext-real positive non negative set
0* g is Relation-like NAT -defined REAL -valued Function-like V34() V41(g) FinSequence-like FinSubsequence-like V53() V54() V55() Element of REAL g
REAL g is non empty functional FinSequence-membered FinSequenceSet of REAL
g -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V34() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = g } is set
g |-> 0 is Relation-like empty-yielding NAT -defined REAL -valued Function-like V34() V41(g) FinSequence-like FinSubsequence-like V53() V54() V55() Element of g -tuples_on REAL
Seg g is non empty V34() V41(g) V64() V65() V66() V67() V68() V69() Element of bool NAT
K153((Seg g),0) is non empty Relation-like Seg g -defined RAT -valued INT -valued {0} -valued Function-like total quasi_total V34() FinSequence-like FinSubsequence-like V53() V54() V55() V56() Element of bool [:(Seg g),{0}:]
[:(Seg g),{0}:] is non empty Relation-like RAT -valued INT -valued V53() V54() V55() V56() set
bool [:(Seg g),{0}:] 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
0* (g + 1) is Relation-like NAT -defined REAL -valued Function-like V34() V41(g + 1) FinSequence-like FinSubsequence-like V53() V54() V55() Element of REAL (g + 1)
REAL (g + 1) is non empty functional FinSequence-membered FinSequenceSet of REAL
(g + 1) -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V34() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = g + 1 } is set
(g + 1) |-> 0 is Relation-like empty-yielding NAT -defined REAL -valued Function-like V34() V41(g + 1) FinSequence-like FinSubsequence-like V53() V54() V55() Element of (g + 1) -tuples_on REAL
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 {0} -valued Function-like total quasi_total V34() FinSequence-like FinSubsequence-like V53() V54() V55() V56() Element of bool [:(Seg (g + 1)),{0}:]
[:(Seg (g + 1)),{0}:] is non empty Relation-like RAT -valued INT -valued V53() V54() V55() V56() set
bool [:(Seg (g + 1)),{0}:] is non empty set
g2 is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(g + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
'not' g2 is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(g + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
x . ('not' g2) is set
(x . ('not' g2)) `2 is set
g -tuples_on BOOLEAN is non empty functional FinSequence-membered FinSequenceSet of BOOLEAN
{ b1 where b1 is Relation-like NAT -defined BOOLEAN -valued Function-like V34() FinSequence-like FinSubsequence-like Element of BOOLEAN * : len b1 = g } is set
g3 is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(g) FinSequence-like FinSubsequence-like Element of g -tuples_on BOOLEAN
a is boolean Element of BOOLEAN
<*a*> is non empty Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
g3 ^ <*a*> is non empty Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(g + 1) V41(K371(g,1)) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
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
(0* g) ^ <*0*> is non empty Relation-like NAT -defined REAL -valued Function-like V34() V41(g + 1) V41(K371(g,1)) FinSequence-like FinSubsequence-like V53() V54() V55() FinSequence of REAL
'not' g3 is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(g) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
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
((g + 1) |-> 0) . (g + 1) is empty V11() real Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V34() FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V53() V54() V55() V56() V64() V65() V66() V67() V68() V69() V70() with_common_domain set
'not' a is boolean Element of BOOLEAN
1 - a is set
('not' g3) ^ <*1*> is non empty Relation-like NAT -defined Function-like V34() V41(g + 1) FinSequence-like FinSubsequence-like set
c is Relation-like NAT -defined NAT -valued Function-like V34() FinSequence-like FinSubsequence-like V53() V54() V55() V56() Element of proj1 x
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
c ^ <*0*> is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
x . (c ^ <*0*>) is set
FSL1j is Element of the carrier of n
c ^ <*1*> is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
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
0* 1 is Relation-like NAT -defined REAL -valued Function-like V34() V41(1) FinSequence-like FinSubsequence-like V53() V54() V55() Element of REAL 1
REAL 1 is non empty functional FinSequence-membered FinSequenceSet of REAL
1 -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V34() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = 1 } is set
1 |-> 0 is Relation-like empty-yielding NAT -defined REAL -valued Function-like V34() V41(1) FinSequence-like FinSubsequence-like V53() V54() V55() Element of 1 -tuples_on REAL
K153((Seg 1),0) is non empty Relation-like Seg 1 -defined RAT -valued INT -valued {0} -valued Function-like total quasi_total V34() FinSequence-like FinSubsequence-like V53() V54() V55() V56() Element of bool [:(Seg 1),{0}:]
[:(Seg 1),{0}:] is non empty Relation-like RAT -valued INT -valued V53() V54() V55() V56() set
bool [:(Seg 1),{0}:] is non empty set
<*> {0,1} is empty Relation-like non-empty empty-yielding NAT -defined {0,1} -valued RAT -valued Function-like one-to-one constant functional V34() FinSequence-like FinSubsequence-like FinSequence-membered V53() V54() V55() V56() V64() V65() V66() V67() V68() V69() V70() with_common_domain FinSequence of {0,1}
g2 is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
'not' g2 is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
x . ('not' g2) is set
(x . ('not' g2)) `2 is set
g is Relation-like NAT -defined NAT -valued Function-like V34() FinSequence-like FinSubsequence-like V53() V54() V55() V56() Element of proj1 x
g ^ <*0*> is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
x . (g ^ <*0*>) is set
g ^ <*1*> is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like 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
g is Relation-like NAT -defined the carrier of n -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
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
g ^ <*X*> 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 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) + (len <*X*>) 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
0* y1 is Relation-like NAT -defined REAL -valued Function-like V34() V41(y1) FinSequence-like FinSubsequence-like V53() V54() V55() Element of REAL y1
REAL y1 is non empty functional FinSequence-membered FinSequenceSet of REAL
y1 -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V34() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = y1 } is set
y1 |-> 0 is Relation-like empty-yielding NAT -defined REAL -valued Function-like V34() V41(y1) FinSequence-like FinSubsequence-like V53() V54() V55() Element of y1 -tuples_on REAL
Seg y1 is non empty V34() V41(y1) V64() V65() V66() V67() V68() V69() Element of bool NAT
K153((Seg y1),0) is non empty Relation-like Seg y1 -defined RAT -valued INT -valued {0} -valued Function-like total quasi_total V34() FinSequence-like FinSubsequence-like V53() V54() V55() V56() Element of bool [:(Seg y1),{0}:]
[:(Seg y1),{0}:] is non empty Relation-like RAT -valued INT -valued V53() V54() V55() V56() set
bool [:(Seg y1),{0}:] 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
y1 -tuples_on BOOLEAN is non empty functional FinSequence-membered FinSequenceSet of BOOLEAN
{ b1 where b1 is Relation-like NAT -defined BOOLEAN -valued Function-like V34() FinSequence-like FinSubsequence-like Element of BOOLEAN * : len b1 = y1 } is set
g3 is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(y1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
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
FinSeqLevel (c1,y) is Relation-like NAT -defined y -level c1 -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of y -level c1
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 is ordinal natural V11() real integer ext-real non negative set
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
FinSeqLevel (j,y) is Relation-like NAT -defined y -level j -valued Function-like one-to-one V34() FinSequence-like FinSubsequence-like FinSequence of y -level j
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
c1 -tuples_on BOOLEAN is non empty functional FinSequence-membered FinSequenceSet of BOOLEAN
{ b1 where b1 is Relation-like NAT -defined BOOLEAN -valued Function-like V34() FinSequence-like FinSubsequence-like Element of BOOLEAN * : len b1 = c1 } is set
b is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(c1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
FSLlprim is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(c1) FinSequence-like FinSubsequence-like Element of c1 -tuples_on BOOLEAN
FSLlprim is Relation-like NAT -defined NAT -valued Function-like V34() FinSequence-like FinSubsequence-like V53() V54() V55() V56() Element of proj1 x
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
FSLl is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(c1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
d is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(c1) FinSequence-like FinSubsequence-like Element of c1 -tuples_on BOOLEAN
DF1 is Relation-like NAT -defined NAT -valued Function-like V34() FinSequence-like FinSubsequence-like V53() V54() V55() V56() Element of proj1 x
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
DF1 ^ <*0*> is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
x . (DF1 ^ <*0*>) is set
x1 is Element of the carrier of n
DF1 ^ <*1*> is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
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
FSLlprim ^ <*0*> is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
x . (FSLlprim ^ <*0*>) is set
x1 is Element of the carrier of n
FSLlprim ^ <*1*> is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
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
d ^ <*0*> is non empty Relation-like NAT -defined Function-like V34() V41(c1 + 1) FinSequence-like FinSubsequence-like set
x . (d ^ <*0*>) is set
(x . (d ^ <*0*>)) `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
FSLlprim ^ <*0*> is non empty Relation-like NAT -defined Function-like V34() V41(c1 + 1) FinSequence-like FinSubsequence-like set
x . (FSLlprim ^ <*0*>) is set
(x . (FSLlprim ^ <*0*>)) `1 is set
d ^ <*1*> is non empty Relation-like NAT -defined Function-like V34() V41(c1 + 1) FinSequence-like FinSubsequence-like 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
FinSeqLevel (1,y) is Relation-like NAT -defined y -level 1 -valued Function-like one-to-one V34() FinSequence-like FinSubsequence-like FinSequence of y -level 1
y -level 1 is V34() Level of y
<*> {0,1} is empty Relation-like non-empty empty-yielding NAT -defined {0,1} -valued RAT -valued Function-like one-to-one constant functional V34() FinSequence-like FinSubsequence-like FinSequence-membered V53() V54() V55() V56() V64() V65() V66() V67() V68() V69() V70() with_common_domain FinSequence of {0,1}
j is ordinal natural V11() real integer ext-real non negative set
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
c1 is Relation-like NAT -defined NAT -valued Function-like V34() FinSequence-like FinSubsequence-like V53() V54() V55() V56() Element of proj1 x
c1 ^ <*0*> is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
x . (c1 ^ <*0*>) is set
c1 ^ <*1*> is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like 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 ^ <*0*>)) `2 is set
x . <*0*> is set
(x . <*0*>) `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
a is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(y1) FinSequence-like FinSubsequence-like Element of y1 -tuples_on BOOLEAN
'not' a is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(y1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
x . ('not' a) is set
(x . ('not' a)) `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
FinSeqLevel (c1,y) is Relation-like NAT -defined y -level c1 -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of y -level c1
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
FinSeqLevel (FSL1j,y) is Relation-like NAT -defined y -level FSL1j -valued Function-like one-to-one V34() FinSequence-like FinSubsequence-like FinSequence of y -level FSL1j
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
c1 -tuples_on BOOLEAN is non empty functional FinSequence-membered FinSequenceSet of BOOLEAN
{ b1 where b1 is Relation-like NAT -defined BOOLEAN -valued Function-like V34() FinSequence-like FinSubsequence-like Element of BOOLEAN * : len b1 = c1 } is set
FSLlprim is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(c1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
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
FSLl1 is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(c1 + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
FSLl is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(c1) FinSequence-like FinSubsequence-like Element of c1 -tuples_on BOOLEAN
d is boolean Element of BOOLEAN
<*d*> is non empty Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
FSLl ^ <*d*> is non empty Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(c1 + 1) V41(K371(c1,1)) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
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
Fj is Relation-like NAT -defined NAT -valued Function-like V34() FinSequence-like FinSubsequence-like V53() V54() V55() V56() Element of proj1 x
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
NFSLl is Relation-like NAT -defined NAT -valued Function-like V34() FinSequence-like FinSubsequence-like V53() V54() V55() V56() Element of proj1 x
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
NFSLl ^ <*0*> is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
x . (NFSLl ^ <*0*>) is set
x1 is Element of the carrier of n
NFSLl ^ <*1*> is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
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
FSLlprim is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(c1) FinSequence-like FinSubsequence-like Element of c1 -tuples_on BOOLEAN
(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
FinSeqLevel (1,y) is Relation-like NAT -defined y -level 1 -valued Function-like one-to-one V34() FinSequence-like FinSubsequence-like FinSequence of y -level 1
y -level 1 is V34() Level of y
(dist (S,X)) / (2 to_power 1) is V11() real ext-real Element of REAL
<*> {0,1} is empty Relation-like non-empty empty-yielding NAT -defined {0,1} -valued RAT -valued Function-like one-to-one constant functional V34() FinSequence-like FinSubsequence-like FinSequence-membered V53() V54() V55() V56() V64() V65() V66() V67() V68() V69() V70() with_common_domain FinSequence of {0,1}
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
c1 is Relation-like NAT -defined NAT -valued Function-like V34() FinSequence-like FinSubsequence-like V53() V54() V55() V56() Element of proj1 x
c1 ^ <*0*> is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
x . (c1 ^ <*0*>) is set
c1 ^ <*1*> is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
x . (c1 ^ <*1*>) is set
x . <*0*> is set
FSL1j is Relation-like NAT -defined NAT -valued Function-like V34() FinSequence-like FinSubsequence-like V53() V54() V55() V56() Element of proj1 x
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