:: GOBOARD3 semantic presentation
begin
theorem
:: GOBOARD3:1
for
f
being ( ( ) (
V16
()
V19
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V20
( the
U1
of
(
TOP-REAL
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
V100
()
V146
()
V147
()
V148
()
V149
()
V150
()
V151
()
V152
()
strict
)
RLTopStruct
) : ( ( ) ( non
empty
)
set
) )
Function-like
V33
()
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) )
for
G
being ( ( non
empty-yielding
tabular
X_equal-in-line
Y_equal-in-column
Y_increasing-in-line
X_increasing-in-column
) (
V16
() non
empty-yielding
V19
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V20
(
K292
( the
U1
of
(
TOP-REAL
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
V100
()
V146
()
V147
()
V148
()
V149
()
V150
()
V151
()
V152
()
strict
)
RLTopStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
functional
FinSequence-membered
)
M11
( the
U1
of
(
TOP-REAL
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
V100
()
V146
()
V147
()
V148
()
V149
()
V150
()
V151
()
V152
()
strict
)
RLTopStruct
) : ( ( ) ( non
empty
)
set
) )) )
Function-like
V33
()
FinSequence-like
FinSubsequence-like
tabular
X_equal-in-line
Y_equal-in-column
Y_increasing-in-line
X_increasing-in-column
)
Go-board
) st ( for
n
being ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) st
n
: ( ( ) (
V16
()
V19
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V20
( the
U1
of
(
TOP-REAL
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
V100
()
V146
()
V147
()
V148
()
V149
()
V150
()
V151
()
V152
()
strict
)
RLTopStruct
) : ( ( ) ( non
empty
)
set
) )
Function-like
V33
()
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) )
in
dom
f
: ( ( ) (
V16
()
V19
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V20
( the
U1
of
(
TOP-REAL
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
V100
()
V146
()
V147
()
V148
()
V149
()
V150
()
V151
()
V152
()
strict
)
RLTopStruct
) : ( ( ) ( non
empty
)
set
) )
Function-like
V33
()
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of
bool
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) : ( ( ) (
V33
() )
set
) ) holds
ex
i
,
j
being ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) st
(
[
i
: ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) ,
j
: ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
]
: ( ( ) ( )
set
)
in
Indices
G
: ( ( non
empty-yielding
tabular
X_equal-in-line
Y_equal-in-column
Y_increasing-in-line
X_increasing-in-column
) (
V16
() non
empty-yielding
V19
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V20
(
K292
( the
U1
of
(
TOP-REAL
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
V100
()
V146
()
V147
()
V148
()
V149
()
V150
()
V151
()
V152
()
strict
)
RLTopStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
functional
FinSequence-membered
)
M11
( the
U1
of
(
TOP-REAL
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
V100
()
V146
()
V147
()
V148
()
V149
()
V150
()
V151
()
V152
()
strict
)
RLTopStruct
) : ( ( ) ( non
empty
)
set
) )) )
Function-like
V33
()
FinSequence-like
FinSubsequence-like
tabular
X_equal-in-line
Y_equal-in-column
Y_increasing-in-line
X_increasing-in-column
)
Go-board
) : ( ( ) ( )
set
) &
f
: ( ( ) (
V16
()
V19
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V20
( the
U1
of
(
TOP-REAL
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
V100
()
V146
()
V147
()
V148
()
V149
()
V150
()
V151
()
V152
()
strict
)
RLTopStruct
) : ( ( ) ( non
empty
)
set
) )
Function-like
V33
()
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) )
/.
n
: ( ( ) (
V16
()
V19
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V20
( the
U1
of
(
TOP-REAL
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
V100
()
V146
()
V147
()
V148
()
V149
()
V150
()
V151
()
V152
()
strict
)
RLTopStruct
) : ( ( ) ( non
empty
)
set
) )
Function-like
V33
()
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
V40
(2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) )
FinSequence-like
V126
() )
Element
of the
U1
of
(
TOP-REAL
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
V100
()
V146
()
V147
()
V148
()
V149
()
V150
()
V151
()
V152
()
strict
)
RLTopStruct
) : ( ( ) ( non
empty
)
set
) )
=
G
: ( ( non
empty-yielding
tabular
X_equal-in-line
Y_equal-in-column
Y_increasing-in-line
X_increasing-in-column
) (
V16
() non
empty-yielding
V19
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V20
(
K292
( the
U1
of
(
TOP-REAL
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
V100
()
V146
()
V147
()
V148
()
V149
()
V150
()
V151
()
V152
()
strict
)
RLTopStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
functional
FinSequence-membered
)
M11
( the
U1
of
(
TOP-REAL
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
V100
()
V146
()
V147
()
V148
()
V149
()
V150
()
V151
()
V152
()
strict
)
RLTopStruct
) : ( ( ) ( non
empty
)
set
) )) )
Function-like
V33
()
FinSequence-like
FinSubsequence-like
tabular
X_equal-in-line
Y_equal-in-column
Y_increasing-in-line
X_increasing-in-column
)
Go-board
)
*
(
i
: ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) ,
j
: ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) ) : ( ( ) (
V40
(2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) )
FinSequence-like
V126
() )
Element
of the
U1
of
(
TOP-REAL
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
V100
()
V146
()
V147
()
V148
()
V149
()
V150
()
V151
()
V152
()
strict
)
RLTopStruct
) : ( ( ) ( non
empty
)
set
) ) ) ) &
f
: ( ( ) (
V16
()
V19
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V20
( the
U1
of
(
TOP-REAL
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
V100
()
V146
()
V147
()
V148
()
V149
()
V150
()
V151
()
V152
()
strict
)
RLTopStruct
) : ( ( ) ( non
empty
)
set
) )
Function-like
V33
()
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) is
one-to-one
&
f
: ( ( ) (
V16
()
V19
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V20
( the
U1
of
(
TOP-REAL
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
V100
()
V146
()
V147
()
V148
()
V149
()
V150
()
V151
()
V152
()
strict
)
RLTopStruct
) : ( ( ) ( non
empty
)
set
) )
Function-like
V33
()
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) is
unfolded
&
f
: ( ( ) (
V16
()
V19
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V20
( the
U1
of
(
TOP-REAL
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
V100
()
V146
()
V147
()
V148
()
V149
()
V150
()
V151
()
V152
()
strict
)
RLTopStruct
) : ( ( ) ( non
empty
)
set
) )
Function-like
V33
()
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) is
s.n.c.
&
f
: ( ( ) (
V16
()
V19
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V20
( the
U1
of
(
TOP-REAL
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
V100
()
V146
()
V147
()
V148
()
V149
()
V150
()
V151
()
V152
()
strict
)
RLTopStruct
) : ( ( ) ( non
empty
)
set
) )
Function-like
V33
()
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) is
special
holds
ex
g
being ( ( ) (
V16
()
V19
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V20
( the
U1
of
(
TOP-REAL
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
V100
()
V146
()
V147
()
V148
()
V149
()
V150
()
V151
()
V152
()
strict
)
RLTopStruct
) : ( ( ) ( non
empty
)
set
) )
Function-like
V33
()
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) st
(
g
: ( ( ) (
V16
()
V19
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V20
( the
U1
of
(
TOP-REAL
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
V100
()
V146
()
V147
()
V148
()
V149
()
V150
()
V151
()
V152
()
strict
)
RLTopStruct
) : ( ( ) ( non
empty
)
set
) )
Function-like
V33
()
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) )
is_sequence_on
G
: ( ( non
empty-yielding
tabular
X_equal-in-line
Y_equal-in-column
Y_increasing-in-line
X_increasing-in-column
) (
V16
() non
empty-yielding
V19
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V20
(
K292
( the
U1
of
(
TOP-REAL
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
V100
()
V146
()
V147
()
V148
()
V149
()
V150
()
V151
()
V152
()
strict
)
RLTopStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
functional
FinSequence-membered
)
M11
( the
U1
of
(
TOP-REAL
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
V100
()
V146
()
V147
()
V148
()
V149
()
V150
()
V151
()
V152
()
strict
)
RLTopStruct
) : ( ( ) ( non
empty
)
set
) )) )
Function-like
V33
()
FinSequence-like
FinSubsequence-like
tabular
X_equal-in-line
Y_equal-in-column
Y_increasing-in-line
X_increasing-in-column
)
Go-board
) &
g
: ( ( ) (
V16
()
V19
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V20
( the
U1
of
(
TOP-REAL
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
V100
()
V146
()
V147
()
V148
()
V149
()
V150
()
V151
()
V152
()
strict
)
RLTopStruct
) : ( ( ) ( non
empty
)
set
) )
Function-like
V33
()
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) is
one-to-one
&
g
: ( ( ) (
V16
()
V19
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V20
( the
U1
of
(
TOP-REAL
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
V100
()
V146
()
V147
()
V148
()
V149
()
V150
()
V151
()
V152
()
strict
)
RLTopStruct
) : ( ( ) ( non
empty
)
set
) )
Function-like
V33
()
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) is
unfolded
&
g
: ( ( ) (
V16
()
V19
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V20
( the
U1
of
(
TOP-REAL
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
V100
()
V146
()
V147
()
V148
()
V149
()
V150
()
V151
()
V152
()
strict
)
RLTopStruct
) : ( ( ) ( non
empty
)
set
) )
Function-like
V33
()
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) is
s.n.c.
&
g
: ( ( ) (
V16
()
V19
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V20
( the
U1
of
(
TOP-REAL
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
V100
()
V146
()
V147
()
V148
()
V149
()
V150
()
V151
()
V152
()
strict
)
RLTopStruct
) : ( ( ) ( non
empty
)
set
) )
Function-like
V33
()
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) is
special
&
L~
f
: ( ( ) (
V16
()
V19
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V20
( the
U1
of
(
TOP-REAL
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
V100
()
V146
()
V147
()
V148
()
V149
()
V150
()
V151
()
V152
()
strict
)
RLTopStruct
) : ( ( ) ( non
empty
)
set
) )
Function-like
V33
()
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of
bool
the
U1
of
(
TOP-REAL
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
V100
()
V146
()
V147
()
V148
()
V149
()
V150
()
V151
()
V152
()
strict
)
RLTopStruct
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) )
=
L~
g
: ( ( ) (
V16
()
V19
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V20
( the
U1
of
(
TOP-REAL
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
V100
()
V146
()
V147
()
V148
()
V149
()
V150
()
V151
()
V152
()
strict
)
RLTopStruct
) : ( ( ) ( non
empty
)
set
) )
Function-like
V33
()
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of
bool
the
U1
of
(
TOP-REAL
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
V100
()
V146
()
V147
()
V148
()
V149
()
V150
()
V151
()
V152
()
strict
)
RLTopStruct
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) &
f
: ( ( ) (
V16
()
V19
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V20
( the
U1
of
(
TOP-REAL
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
V100
()
V146
()
V147
()
V148
()
V149
()
V150
()
V151
()
V152
()
strict
)
RLTopStruct
) : ( ( ) ( non
empty
)
set
) )
Function-like
V33
()
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) )
/.
1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) : ( ( ) (
V40
(2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) )
FinSequence-like
V126
() )
Element
of the
U1
of
(
TOP-REAL
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
V100
()
V146
()
V147
()
V148
()
V149
()
V150
()
V151
()
V152
()
strict
)
RLTopStruct
) : ( ( ) ( non
empty
)
set
) )
=
g
: ( ( ) (
V16
()
V19
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V20
( the
U1
of
(
TOP-REAL
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
V100
()
V146
()
V147
()
V148
()
V149
()
V150
()
V151
()
V152
()
strict
)
RLTopStruct
) : ( ( ) ( non
empty
)
set
) )
Function-like
V33
()
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) )
/.
1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) : ( ( ) (
V40
(2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) )
FinSequence-like
V126
() )
Element
of the
U1
of
(
TOP-REAL
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
V100
()
V146
()
V147
()
V148
()
V149
()
V150
()
V151
()
V152
()
strict
)
RLTopStruct
) : ( ( ) ( non
empty
)
set
) ) &
f
: ( ( ) (
V16
()
V19
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V20
( the
U1
of
(
TOP-REAL
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
V100
()
V146
()
V147
()
V148
()
V149
()
V150
()
V151
()
V152
()
strict
)
RLTopStruct
) : ( ( ) ( non
empty
)
set
) )
Function-like
V33
()
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) )
/.
(
len
f
: ( ( ) (
V16
()
V19
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V20
( the
U1
of
(
TOP-REAL
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
V100
()
V146
()
V147
()
V148
()
V149
()
V150
()
V151
()
V152
()
strict
)
RLTopStruct
) : ( ( ) ( non
empty
)
set
) )
Function-like
V33
()
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) : ( ( ) (
V40
(2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) )
FinSequence-like
V126
() )
Element
of the
U1
of
(
TOP-REAL
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
V100
()
V146
()
V147
()
V148
()
V149
()
V150
()
V151
()
V152
()
strict
)
RLTopStruct
) : ( ( ) ( non
empty
)
set
) )
=
g
: ( ( ) (
V16
()
V19
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V20
( the
U1
of
(
TOP-REAL
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
V100
()
V146
()
V147
()
V148
()
V149
()
V150
()
V151
()
V152
()
strict
)
RLTopStruct
) : ( ( ) ( non
empty
)
set
) )
Function-like
V33
()
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) )
/.
(
len
g
: ( ( ) (
V16
()
V19
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V20
( the
U1
of
(
TOP-REAL
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
V100
()
V146
()
V147
()
V148
()
V149
()
V150
()
V151
()
V152
()
strict
)
RLTopStruct
) : ( ( ) ( non
empty
)
set
) )
Function-like
V33
()
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) : ( ( ) (
V40
(2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) )
FinSequence-like
V126
() )
Element
of the
U1
of
(
TOP-REAL
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
V100
()
V146
()
V147
()
V148
()
V149
()
V150
()
V151
()
V152
()
strict
)
RLTopStruct
) : ( ( ) ( non
empty
)
set
) ) &
len
f
: ( ( ) (
V16
()
V19
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V20
( the
U1
of
(
TOP-REAL
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
V100
()
V146
()
V147
()
V148
()
V149
()
V150
()
V151
()
V152
()
strict
)
RLTopStruct
) : ( ( ) ( non
empty
)
set
) )
Function-like
V33
()
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
<=
len
g
: ( ( ) (
V16
()
V19
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V20
( the
U1
of
(
TOP-REAL
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
V100
()
V146
()
V147
()
V148
()
V149
()
V150
()
V151
()
V152
()
strict
)
RLTopStruct
) : ( ( ) ( non
empty
)
set
) )
Function-like
V33
()
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) ) ;
theorem
:: GOBOARD3:2
for
f
being ( ( ) (
V16
()
V19
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V20
( the
U1
of
(
TOP-REAL
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
V100
()
V146
()
V147
()
V148
()
V149
()
V150
()
V151
()
V152
()
strict
)
RLTopStruct
) : ( ( ) ( non
empty
)
set
) )
Function-like
V33
()
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) )
for
G
being ( ( non
empty-yielding
tabular
X_equal-in-line
Y_equal-in-column
Y_increasing-in-line
X_increasing-in-column
) (
V16
() non
empty-yielding
V19
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V20
(
K292
( the
U1
of
(
TOP-REAL
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
V100
()
V146
()
V147
()
V148
()
V149
()
V150
()
V151
()
V152
()
strict
)
RLTopStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
functional
FinSequence-membered
)
M11
( the
U1
of
(
TOP-REAL
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
V100
()
V146
()
V147
()
V148
()
V149
()
V150
()
V151
()
V152
()
strict
)
RLTopStruct
) : ( ( ) ( non
empty
)
set
) )) )
Function-like
V33
()
FinSequence-like
FinSubsequence-like
tabular
X_equal-in-line
Y_equal-in-column
Y_increasing-in-line
X_increasing-in-column
)
Go-board
) st ( for
n
being ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) st
n
: ( ( ) (
V16
()
V19
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V20
( the
U1
of
(
TOP-REAL
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
V100
()
V146
()
V147
()
V148
()
V149
()
V150
()
V151
()
V152
()
strict
)
RLTopStruct
) : ( ( ) ( non
empty
)
set
) )
Function-like
V33
()
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) )
in
dom
f
: ( ( ) (
V16
()
V19
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V20
( the
U1
of
(
TOP-REAL
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
V100
()
V146
()
V147
()
V148
()
V149
()
V150
()
V151
()
V152
()
strict
)
RLTopStruct
) : ( ( ) ( non
empty
)
set
) )
Function-like
V33
()
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of
bool
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) : ( ( ) (
V33
() )
set
) ) holds
ex
i
,
j
being ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) st
(
[
i
: ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) ,
j
: ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
]
: ( ( ) ( )
set
)
in
Indices
G
: ( ( non
empty-yielding
tabular
X_equal-in-line
Y_equal-in-column
Y_increasing-in-line
X_increasing-in-column
) (
V16
() non
empty-yielding
V19
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V20
(
K292
( the
U1
of
(
TOP-REAL
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
V100
()
V146
()
V147
()
V148
()
V149
()
V150
()
V151
()
V152
()
strict
)
RLTopStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
functional
FinSequence-membered
)
M11
( the
U1
of
(
TOP-REAL
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
V100
()
V146
()
V147
()
V148
()
V149
()
V150
()
V151
()
V152
()
strict
)
RLTopStruct
) : ( ( ) ( non
empty
)
set
) )) )
Function-like
V33
()
FinSequence-like
FinSubsequence-like
tabular
X_equal-in-line
Y_equal-in-column
Y_increasing-in-line
X_increasing-in-column
)
Go-board
) : ( ( ) ( )
set
) &
f
: ( ( ) (
V16
()
V19
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V20
( the
U1
of
(
TOP-REAL
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
V100
()
V146
()
V147
()
V148
()
V149
()
V150
()
V151
()
V152
()
strict
)
RLTopStruct
) : ( ( ) ( non
empty
)
set
) )
Function-like
V33
()
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) )
/.
n
: ( ( ) (
V16
()
V19
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V20
( the
U1
of
(
TOP-REAL
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
V100
()
V146
()
V147
()
V148
()
V149
()
V150
()
V151
()
V152
()
strict
)
RLTopStruct
) : ( ( ) ( non
empty
)
set
) )
Function-like
V33
()
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
V40
(2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) )
FinSequence-like
V126
() )
Element
of the
U1
of
(
TOP-REAL
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
V100
()
V146
()
V147
()
V148
()
V149
()
V150
()
V151
()
V152
()
strict
)
RLTopStruct
) : ( ( ) ( non
empty
)
set
) )
=
G
: ( ( non
empty-yielding
tabular
X_equal-in-line
Y_equal-in-column
Y_increasing-in-line
X_increasing-in-column
) (
V16
() non
empty-yielding
V19
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V20
(
K292
( the
U1
of
(
TOP-REAL
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
V100
()
V146
()
V147
()
V148
()
V149
()
V150
()
V151
()
V152
()
strict
)
RLTopStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
functional
FinSequence-membered
)
M11
( the
U1
of
(
TOP-REAL
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
V100
()
V146
()
V147
()
V148
()
V149
()
V150
()
V151
()
V152
()
strict
)
RLTopStruct
) : ( ( ) ( non
empty
)
set
) )) )
Function-like
V33
()
FinSequence-like
FinSubsequence-like
tabular
X_equal-in-line
Y_equal-in-column
Y_increasing-in-line
X_increasing-in-column
)
Go-board
)
*
(
i
: ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) ,
j
: ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) ) : ( ( ) (
V40
(2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) )
FinSequence-like
V126
() )
Element
of the
U1
of
(
TOP-REAL
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
V100
()
V146
()
V147
()
V148
()
V149
()
V150
()
V151
()
V152
()
strict
)
RLTopStruct
) : ( ( ) ( non
empty
)
set
) ) ) ) &
f
: ( ( ) (
V16
()
V19
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V20
( the
U1
of
(
TOP-REAL
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
V100
()
V146
()
V147
()
V148
()
V149
()
V150
()
V151
()
V152
()
strict
)
RLTopStruct
) : ( ( ) ( non
empty
)
set
) )
Function-like
V33
()
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) is
being_S-Seq
holds
ex
g
being ( ( ) (
V16
()
V19
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V20
( the
U1
of
(
TOP-REAL
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
V100
()
V146
()
V147
()
V148
()
V149
()
V150
()
V151
()
V152
()
strict
)
RLTopStruct
) : ( ( ) ( non
empty
)
set
) )
Function-like
V33
()
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) st
(
g
: ( ( ) (
V16
()
V19
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V20
( the
U1
of
(
TOP-REAL
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
V100
()
V146
()
V147
()
V148
()
V149
()
V150
()
V151
()
V152
()
strict
)
RLTopStruct
) : ( ( ) ( non
empty
)
set
) )
Function-like
V33
()
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) )
is_sequence_on
G
: ( ( non
empty-yielding
tabular
X_equal-in-line
Y_equal-in-column
Y_increasing-in-line
X_increasing-in-column
) (
V16
() non
empty-yielding
V19
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V20
(
K292
( the
U1
of
(
TOP-REAL
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
V100
()
V146
()
V147
()
V148
()
V149
()
V150
()
V151
()
V152
()
strict
)
RLTopStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
functional
FinSequence-membered
)
M11
( the
U1
of
(
TOP-REAL
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
V100
()
V146
()
V147
()
V148
()
V149
()
V150
()
V151
()
V152
()
strict
)
RLTopStruct
) : ( ( ) ( non
empty
)
set
) )) )
Function-like
V33
()
FinSequence-like
FinSubsequence-like
tabular
X_equal-in-line
Y_equal-in-column
Y_increasing-in-line
X_increasing-in-column
)
Go-board
) &
g
: ( ( ) (
V16
()
V19
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V20
( the
U1
of
(
TOP-REAL
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
V100
()
V146
()
V147
()
V148
()
V149
()
V150
()
V151
()
V152
()
strict
)
RLTopStruct
) : ( ( ) ( non
empty
)
set
) )
Function-like
V33
()
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) is
being_S-Seq
&
L~
f
: ( ( ) (
V16
()
V19
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V20
( the
U1
of
(
TOP-REAL
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
V100
()
V146
()
V147
()
V148
()
V149
()
V150
()
V151
()
V152
()
strict
)
RLTopStruct
) : ( ( ) ( non
empty
)
set
) )
Function-like
V33
()
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of
bool
the
U1
of
(
TOP-REAL
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
V100
()
V146
()
V147
()
V148
()
V149
()
V150
()
V151
()
V152
()
strict
)
RLTopStruct
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) )
=
L~
g
: ( ( ) (
V16
()
V19
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V20
( the
U1
of
(
TOP-REAL
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
V100
()
V146
()
V147
()
V148
()
V149
()
V150
()
V151
()
V152
()
strict
)
RLTopStruct
) : ( ( ) ( non
empty
)
set
) )
Function-like
V33
()
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of
bool
the
U1
of
(
TOP-REAL
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
V100
()
V146
()
V147
()
V148
()
V149
()
V150
()
V151
()
V152
()
strict
)
RLTopStruct
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) &
f
: ( ( ) (
V16
()
V19
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V20
( the
U1
of
(
TOP-REAL
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
V100
()
V146
()
V147
()
V148
()
V149
()
V150
()
V151
()
V152
()
strict
)
RLTopStruct
) : ( ( ) ( non
empty
)
set
) )
Function-like
V33
()
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) )
/.
1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) : ( ( ) (
V40
(2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) )
FinSequence-like
V126
() )
Element
of the
U1
of
(
TOP-REAL
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
V100
()
V146
()
V147
()
V148
()
V149
()
V150
()
V151
()
V152
()
strict
)
RLTopStruct
) : ( ( ) ( non
empty
)
set
) )
=
g
: ( ( ) (
V16
()
V19
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V20
( the
U1
of
(
TOP-REAL
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
V100
()
V146
()
V147
()
V148
()
V149
()
V150
()
V151
()
V152
()
strict
)
RLTopStruct
) : ( ( ) ( non
empty
)
set
) )
Function-like
V33
()
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) )
/.
1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) : ( ( ) (
V40
(2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) )
FinSequence-like
V126
() )
Element
of the
U1
of
(
TOP-REAL
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
V100
()
V146
()
V147
()
V148
()
V149
()
V150
()
V151
()
V152
()
strict
)
RLTopStruct
) : ( ( ) ( non
empty
)
set
) ) &
f
: ( ( ) (
V16
()
V19
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V20
( the
U1
of
(
TOP-REAL
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
V100
()
V146
()
V147
()
V148
()
V149
()
V150
()
V151
()
V152
()
strict
)
RLTopStruct
) : ( ( ) ( non
empty
)
set
) )
Function-like
V33
()
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) )
/.
(
len
f
: ( ( ) (
V16
()
V19
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V20
( the
U1
of
(
TOP-REAL
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
V100
()
V146
()
V147
()
V148
()
V149
()
V150
()
V151
()
V152
()
strict
)
RLTopStruct
) : ( ( ) ( non
empty
)
set
) )
Function-like
V33
()
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) : ( ( ) (
V40
(2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) )
FinSequence-like
V126
() )
Element
of the
U1
of
(
TOP-REAL
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
V100
()
V146
()
V147
()
V148
()
V149
()
V150
()
V151
()
V152
()
strict
)
RLTopStruct
) : ( ( ) ( non
empty
)
set
) )
=
g
: ( ( ) (
V16
()
V19
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V20
( the
U1
of
(
TOP-REAL
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
V100
()
V146
()
V147
()
V148
()
V149
()
V150
()
V151
()
V152
()
strict
)
RLTopStruct
) : ( ( ) ( non
empty
)
set
) )
Function-like
V33
()
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) )
/.
(
len
g
: ( ( ) (
V16
()
V19
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V20
( the
U1
of
(
TOP-REAL
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
V100
()
V146
()
V147
()
V148
()
V149
()
V150
()
V151
()
V152
()
strict
)
RLTopStruct
) : ( ( ) ( non
empty
)
set
) )
Function-like
V33
()
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) : ( ( ) (
V40
(2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) )
FinSequence-like
V126
() )
Element
of the
U1
of
(
TOP-REAL
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
V100
()
V146
()
V147
()
V148
()
V149
()
V150
()
V151
()
V152
()
strict
)
RLTopStruct
) : ( ( ) ( non
empty
)
set
) ) &
len
f
: ( ( ) (
V16
()
V19
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V20
( the
U1
of
(
TOP-REAL
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
V100
()
V146
()
V147
()
V148
()
V149
()
V150
()
V151
()
V152
()
strict
)
RLTopStruct
) : ( ( ) ( non
empty
)
set
) )
Function-like
V33
()
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
<=
len
g
: ( ( ) (
V16
()
V19
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V20
( the
U1
of
(
TOP-REAL
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
V100
()
V146
()
V147
()
V148
()
V149
()
V150
()
V151
()
V152
()
strict
)
RLTopStruct
) : ( ( ) ( non
empty
)
set
) )
Function-like
V33
()
FinSequence-like
FinSubsequence-like
)
FinSequence
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
ext-real
non
negative
V33
()
V38
()
V71
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V33
()
V38
()
V39
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) ) ;