:: CATALAN1 semantic presentation
begin
theorem
:: CATALAN1:1
for
n
being ( (
natural
) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
)
Nat
) st
n
: ( (
natural
) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
)
Nat
)
>
1 : ( ( ) (
ext-real
positive
non
negative
non
empty
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) ) holds
n
: ( (
natural
) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
)
Nat
)
-'
1 : ( ( ) (
ext-real
positive
non
negative
non
empty
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) ) : ( ( ) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) )
<=
(
2 : ( ( ) (
ext-real
positive
non
negative
non
empty
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) )
*
n
: ( (
natural
) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
)
Nat
)
)
: ( ( ) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) )
-'
3 : ( ( ) (
ext-real
positive
non
negative
non
empty
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) ) : ( ( ) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) ) ;
theorem
:: CATALAN1:2
for
n
being ( (
natural
) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
)
Nat
) st
n
: ( (
natural
) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
)
Nat
)
>=
1 : ( ( ) (
ext-real
positive
non
negative
non
empty
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) ) holds
n
: ( (
natural
) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
)
Nat
)
-'
1 : ( ( ) (
ext-real
positive
non
negative
non
empty
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) ) : ( ( ) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) )
<=
(
2 : ( ( ) (
ext-real
positive
non
negative
non
empty
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) )
*
n
: ( (
natural
) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
)
Nat
)
)
: ( ( ) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) )
-'
2 : ( ( ) (
ext-real
positive
non
negative
non
empty
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) ) : ( ( ) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) ) ;
theorem
:: CATALAN1:3
for
n
being ( (
natural
) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
)
Nat
) st
n
: ( (
natural
) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
)
Nat
)
>
1 : ( ( ) (
ext-real
positive
non
negative
non
empty
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) ) holds
n
: ( (
natural
) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
)
Nat
)
<
(
2 : ( ( ) (
ext-real
positive
non
negative
non
empty
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) )
*
n
: ( (
natural
) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
)
Nat
)
)
: ( ( ) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) )
-'
1 : ( ( ) (
ext-real
positive
non
negative
non
empty
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) ) : ( ( ) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) ) ;
theorem
:: CATALAN1:4
for
n
being ( (
natural
) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
)
Nat
) st
n
: ( (
natural
) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
)
Nat
)
>
1 : ( ( ) (
ext-real
positive
non
negative
non
empty
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) ) holds
(
n
: ( (
natural
) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
)
Nat
)
-'
2 : ( ( ) (
ext-real
positive
non
negative
non
empty
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) )
+
1 : ( ( ) (
ext-real
positive
non
negative
non
empty
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) ) : ( ( ) (
ext-real
positive
non
negative
non
empty
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) )
=
n
: ( (
natural
) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
)
Nat
)
-'
1 : ( ( ) (
ext-real
positive
non
negative
non
empty
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) ) : ( ( ) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) ) ;
theorem
:: CATALAN1:5
for
n
being ( (
natural
) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
)
Nat
) st
n
: ( (
natural
) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
)
Nat
)
>
1 : ( ( ) (
ext-real
positive
non
negative
non
empty
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) ) holds
(
(
(
4 : ( ( ) (
ext-real
positive
non
negative
non
empty
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) )
*
n
: ( (
natural
) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
)
Nat
)
)
: ( ( ) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) )
*
n
: ( (
natural
) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
)
Nat
)
)
: ( ( ) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) )
-
(
2 : ( ( ) (
ext-real
positive
non
negative
non
empty
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) )
*
n
: ( (
natural
) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
)
Nat
)
)
: ( ( ) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
ext-real
V14
()
V15
()
integer
)
Element
of
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) )
/
(
n
: ( (
natural
) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
)
Nat
)
+
1 : ( ( ) (
ext-real
positive
non
negative
non
empty
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
ext-real
positive
non
negative
non
empty
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) ) : ( ( ) (
ext-real
V14
()
V15
() )
Element
of
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) )
>
1 : ( ( ) (
ext-real
positive
non
negative
non
empty
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) ) ;
theorem
:: CATALAN1:6
for
n
being ( (
natural
) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
)
Nat
) st
n
: ( (
natural
) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
)
Nat
)
>
1 : ( ( ) (
ext-real
positive
non
negative
non
empty
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) ) holds
(
(
(
(
2 : ( ( ) (
ext-real
positive
non
negative
non
empty
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) )
*
n
: ( (
natural
) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
)
Nat
)
)
: ( ( ) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) )
-'
2 : ( ( ) (
ext-real
positive
non
negative
non
empty
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) )
!
)
: ( ( ) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) )
*
n
: ( (
natural
) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
)
Nat
)
)
: ( ( ) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) )
*
(
n
: ( (
natural
) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
)
Nat
)
+
1 : ( ( ) (
ext-real
positive
non
negative
non
empty
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
ext-real
positive
non
negative
non
empty
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) ) : ( ( ) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) )
<
(
2 : ( ( ) (
ext-real
positive
non
negative
non
empty
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) )
*
n
: ( (
natural
) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
)
Nat
)
)
: ( ( ) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) )
!
: ( ( ) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) ) ;
theorem
:: CATALAN1:7
for
n
being ( (
natural
) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
)
Nat
) holds 2 : ( ( ) (
ext-real
positive
non
negative
non
empty
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) )
*
(
2 : ( ( ) (
ext-real
positive
non
negative
non
empty
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) )
-
(
3 : ( ( ) (
ext-real
positive
non
negative
non
empty
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) )
/
(
n
: ( (
natural
) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
)
Nat
)
+
1 : ( ( ) (
ext-real
positive
non
negative
non
empty
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
ext-real
positive
non
negative
non
empty
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
ext-real
non
negative
V14
()
V15
() )
Element
of
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) )
)
: ( ( ) (
ext-real
V14
()
V15
() )
Element
of
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) ) : ( ( ) (
ext-real
V14
()
V15
() )
Element
of
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) )
<
4 : ( ( ) (
ext-real
positive
non
negative
non
empty
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) ) ;
begin
definition
let
n
be ( (
natural
) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
)
Nat
) ;
func
Catalan
n
->
( ( ) (
ext-real
V14
()
V15
() )
Real
)
equals
:: CATALAN1:def 1
(
(
(
2 : ( ( ) (
ext-real
positive
non
negative
non
empty
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) )
*
n
: ( ( ) ( )
set
)
)
: ( ( ) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) )
-'
2 : ( ( ) (
ext-real
positive
non
negative
non
empty
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) )
choose
(
n
: ( ( ) ( )
set
)
-'
1 : ( ( ) (
ext-real
positive
non
negative
non
empty
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) )
/
n
: ( ( ) ( )
set
) : ( ( ) (
ext-real
V14
()
V15
() )
Element
of
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) ) ;
end;
theorem
:: CATALAN1:8
for
n
being ( (
natural
) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
)
Nat
) st
n
: ( (
natural
) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
)
Nat
)
>
1 : ( ( ) (
ext-real
positive
non
negative
non
empty
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) ) holds
Catalan
n
: ( (
natural
) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
)
Nat
) : ( ( ) (
ext-real
V14
()
V15
() )
Real
)
=
(
(
(
2 : ( ( ) (
ext-real
positive
non
negative
non
empty
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) )
*
n
: ( (
natural
) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
)
Nat
)
)
: ( ( ) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) )
-'
2 : ( ( ) (
ext-real
positive
non
negative
non
empty
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) )
!
)
: ( ( ) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) )
/
(
(
(
n
: ( (
natural
) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
)
Nat
)
-'
1 : ( ( ) (
ext-real
positive
non
negative
non
empty
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) )
!
)
: ( ( ) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) )
*
(
n
: ( (
natural
) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
)
Nat
)
!
)
: ( ( ) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) ) : ( ( ) (
ext-real
non
negative
V14
()
V15
() )
Element
of
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) ) ;
theorem
:: CATALAN1:9
for
n
being ( (
natural
) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
)
Nat
) st
n
: ( (
natural
) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
)
Nat
)
>
1 : ( ( ) (
ext-real
positive
non
negative
non
empty
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) ) holds
Catalan
n
: ( (
natural
) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
)
Nat
) : ( ( ) (
ext-real
V14
()
V15
() )
Real
)
=
(
4 : ( ( ) (
ext-real
positive
non
negative
non
empty
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) )
*
(
(
(
2 : ( ( ) (
ext-real
positive
non
negative
non
empty
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) )
*
n
: ( (
natural
) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
)
Nat
)
)
: ( ( ) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) )
-'
3 : ( ( ) (
ext-real
positive
non
negative
non
empty
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) )
choose
(
n
: ( (
natural
) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
)
Nat
)
-'
1 : ( ( ) (
ext-real
positive
non
negative
non
empty
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) )
-
(
(
(
2 : ( ( ) (
ext-real
positive
non
negative
non
empty
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) )
*
n
: ( (
natural
) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
)
Nat
)
)
: ( ( ) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) )
-'
1 : ( ( ) (
ext-real
positive
non
negative
non
empty
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) )
choose
(
n
: ( (
natural
) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
)
Nat
)
-'
1 : ( ( ) (
ext-real
positive
non
negative
non
empty
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) ) : ( ( ) (
ext-real
V14
()
V15
()
integer
)
Element
of
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) ) ;
theorem
:: CATALAN1:10
Catalan
0
: ( ( ) (
ext-real
non
positive
non
negative
empty
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) ) : ( ( ) (
ext-real
V14
()
V15
() )
Real
)
=
0
: ( ( ) (
ext-real
non
positive
non
negative
empty
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) ) ;
theorem
:: CATALAN1:11
Catalan
1 : ( ( ) (
ext-real
positive
non
negative
non
empty
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) ) : ( ( ) (
ext-real
V14
()
V15
() )
Real
)
=
1 : ( ( ) (
ext-real
positive
non
negative
non
empty
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) ) ;
theorem
:: CATALAN1:12
Catalan
2 : ( ( ) (
ext-real
positive
non
negative
non
empty
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) ) : ( ( ) (
ext-real
V14
()
V15
() )
Real
)
=
1 : ( ( ) (
ext-real
positive
non
negative
non
empty
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) ) ;
theorem
:: CATALAN1:13
for
n
being ( (
natural
) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
)
Nat
) holds
Catalan
n
: ( (
natural
) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
)
Nat
) : ( ( ) (
ext-real
V14
()
V15
() )
Real
) is ( (
integer
) (
ext-real
V14
()
V15
()
integer
)
Integer
) ;
theorem
:: CATALAN1:14
for
k
being ( (
natural
) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
)
Nat
) holds
Catalan
(
k
: ( (
natural
) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
)
Nat
)
+
1 : ( ( ) (
ext-real
positive
non
negative
non
empty
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
ext-real
positive
non
negative
non
empty
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) ) : ( ( ) (
ext-real
V14
()
V15
() )
Real
)
=
(
(
2 : ( ( ) (
ext-real
positive
non
negative
non
empty
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) )
*
k
: ( (
natural
) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
)
Nat
)
)
: ( ( ) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) )
!
)
: ( ( ) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) )
/
(
(
k
: ( (
natural
) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
)
Nat
)
!
)
: ( ( ) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) )
*
(
(
k
: ( (
natural
) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
)
Nat
)
+
1 : ( ( ) (
ext-real
positive
non
negative
non
empty
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
ext-real
positive
non
negative
non
empty
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) )
!
)
: ( ( ) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) ) : ( ( ) (
ext-real
non
negative
V14
()
V15
() )
Element
of
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) ) ;
theorem
:: CATALAN1:15
for
n
being ( (
natural
) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
)
Nat
) st
n
: ( (
natural
) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
)
Nat
)
>
1 : ( ( ) (
ext-real
positive
non
negative
non
empty
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) ) holds
Catalan
n
: ( (
natural
) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
)
Nat
) : ( ( ) (
ext-real
V14
()
V15
() )
Real
)
<
Catalan
(
n
: ( (
natural
) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
)
Nat
)
+
1 : ( ( ) (
ext-real
positive
non
negative
non
empty
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
ext-real
positive
non
negative
non
empty
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) ) : ( ( ) (
ext-real
V14
()
V15
() )
Real
) ;
theorem
:: CATALAN1:16
for
n
being ( (
natural
) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
)
Nat
) holds
Catalan
n
: ( (
natural
) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
)
Nat
) : ( ( ) (
ext-real
V14
()
V15
() )
Real
)
<=
Catalan
(
n
: ( (
natural
) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
)
Nat
)
+
1 : ( ( ) (
ext-real
positive
non
negative
non
empty
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
ext-real
positive
non
negative
non
empty
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) ) : ( ( ) (
ext-real
V14
()
V15
() )
Real
) ;
theorem
:: CATALAN1:17
for
n
being ( (
natural
) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
)
Nat
) holds
Catalan
n
: ( (
natural
) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
)
Nat
) : ( ( ) (
ext-real
V14
()
V15
() )
Real
)
>=
0
: ( ( ) (
ext-real
non
positive
non
negative
empty
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) ) ;
theorem
:: CATALAN1:18
for
n
being ( (
natural
) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
)
Nat
) holds
Catalan
n
: ( (
natural
) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
)
Nat
) : ( ( ) (
ext-real
V14
()
V15
() )
Real
) is ( ( ) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) ) ;
theorem
:: CATALAN1:19
for
n
being ( (
natural
) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
)
Nat
) st
n
: ( (
natural
) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
)
Nat
)
>
0
: ( ( ) (
ext-real
non
positive
non
negative
empty
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) ) holds
Catalan
(
n
: ( (
natural
) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
)
Nat
)
+
1 : ( ( ) (
ext-real
positive
non
negative
non
empty
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
ext-real
positive
non
negative
non
empty
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) ) : ( ( ) (
ext-real
V14
()
V15
() )
Real
)
=
(
2 : ( ( ) (
ext-real
positive
non
negative
non
empty
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) )
*
(
2 : ( ( ) (
ext-real
positive
non
negative
non
empty
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) )
-
(
3 : ( ( ) (
ext-real
positive
non
negative
non
empty
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) )
/
(
n
: ( (
natural
) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
)
Nat
)
+
1 : ( ( ) (
ext-real
positive
non
negative
non
empty
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
ext-real
positive
non
negative
non
empty
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
ext-real
non
negative
V14
()
V15
() )
Element
of
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) )
)
: ( ( ) (
ext-real
V14
()
V15
() )
Element
of
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) )
)
: ( ( ) (
ext-real
V14
()
V15
() )
Element
of
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) )
*
(
Catalan
n
: ( (
natural
) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
)
Nat
)
)
: ( ( ) (
ext-real
V14
()
V15
() )
Real
) : ( ( ) (
ext-real
V14
()
V15
() )
Element
of
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) ) ;
registration
let
n
be ( (
natural
) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
)
Nat
) ;
cluster
Catalan
n
: ( (
natural
) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
)
set
) : ( ( ) (
ext-real
V14
()
V15
() )
Real
)
->
natural
;
end;
theorem
:: CATALAN1:20
for
n
being ( (
natural
) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
)
Nat
) st
n
: ( (
natural
) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
)
Nat
)
>
0
: ( ( ) (
ext-real
non
positive
non
negative
empty
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) ) holds
Catalan
n
: ( (
natural
) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
)
Nat
) : ( ( ) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
)
Real
)
>
0
: ( ( ) (
ext-real
non
positive
non
negative
empty
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) ) ;
registration
let
n
be ( ( non
empty
natural
) (
ext-real
positive
non
negative
non
empty
ordinal
natural
V14
()
V15
()
integer
)
Nat
) ;
cluster
Catalan
n
: ( ( non
empty
natural
) (
ext-real
positive
non
negative
non
empty
ordinal
natural
V14
()
V15
()
integer
)
set
) : ( ( ) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
)
Real
)
->
non
empty
;
end;
theorem
:: CATALAN1:21
for
n
being ( (
natural
) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
)
Nat
) st
n
: ( (
natural
) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
)
Nat
)
>
0
: ( ( ) (
ext-real
non
positive
non
negative
empty
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) ) holds
Catalan
(
n
: ( (
natural
) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
)
Nat
)
+
1 : ( ( ) (
ext-real
positive
non
negative
non
empty
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
ext-real
positive
non
negative
non
empty
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) ) : ( ( ) (
ext-real
positive
non
negative
non
empty
ordinal
natural
V14
()
V15
()
integer
)
Real
)
<
4 : ( ( ) (
ext-real
positive
non
negative
non
empty
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) )
*
(
Catalan
n
: ( (
natural
) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
)
Nat
)
)
: ( ( ) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
)
Real
) : ( ( ) (
ext-real
non
negative
ordinal
natural
V14
()
V15
()
integer
V46
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
NAT
: ( ( ) (
V57
()
V58
()
V59
()
V60
()
V61
()
V62
()
V63
() )
Element
of
bool
REAL
: ( ( ) (
V57
()
V58
()
V59
()
V63
() )
set
) : ( ( ) ( )
set
) ) ) ;