:: BINARI_3 semantic presentation
begin
theorem
:: BINARI_3:1
for
n
being ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
for
F
being ( (
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
Tuple
of
n
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ,
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) holds
Absval
F
: ( (
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
Tuple
of
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ,
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) : ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
<
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
to_power
n
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) : ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) ;
theorem
:: BINARI_3:2
for
n
being ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
for
F1
,
F2
being ( (
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
Tuple
of
n
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ,
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) st
Absval
F1
: ( (
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
Tuple
of
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ,
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) : ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
=
Absval
F2
: ( (
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
Tuple
of
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ,
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) : ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) holds
F1
: ( (
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
Tuple
of
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ,
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
=
F2
: ( (
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
Tuple
of
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ,
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) ;
theorem
:: BINARI_3:3
for
t1
,
t2
being ( (
V15
()
Function-like
FinSequence-like
) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
Function-like
V34
()
FinSequence-like
FinSubsequence-like
)
FinSequence
) st
Rev
t1
: ( (
V15
()
Function-like
FinSequence-like
) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
Function-like
V34
()
FinSequence-like
FinSubsequence-like
)
FinSequence
) : ( (
V15
()
Function-like
FinSequence-like
) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
Function-like
V34
()
FinSequence-like
FinSubsequence-like
)
set
)
=
Rev
t2
: ( (
V15
()
Function-like
FinSequence-like
) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
Function-like
V34
()
FinSequence-like
FinSubsequence-like
)
FinSequence
) : ( (
V15
()
Function-like
FinSequence-like
) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
Function-like
V34
()
FinSequence-like
FinSubsequence-like
)
set
) holds
t1
: ( (
V15
()
Function-like
FinSequence-like
) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
Function-like
V34
()
FinSequence-like
FinSubsequence-like
)
FinSequence
)
=
t2
: ( (
V15
()
Function-like
FinSequence-like
) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
Function-like
V34
()
FinSequence-like
FinSubsequence-like
)
FinSequence
) ;
theorem
:: BINARI_3:4
for
n
being ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) holds
0*
n
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) : ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
REAL
: ( ( ) ( )
set
) )
Function-like
V34
()
FinSequence-like
FinSubsequence-like
)
Element
of
REAL
b
1
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) : ( ( ) (
functional
FinSequence-membered
)
FinSequenceSet
of
REAL
: ( ( ) ( )
set
) ) )
in
BOOLEAN
: ( ( ) ( non
empty
)
set
)
*
: ( ( ) ( non
empty
functional
FinSequence-membered
)
FinSequenceSet
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) ;
theorem
:: BINARI_3:5
for
n
being ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
for
y
being ( (
V41
(
b
1
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
Tuple
of
n
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ,
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) st
y
: ( (
V41
(
b
1
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
Tuple
of
b
1
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ,
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
=
0*
n
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) : ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
REAL
: ( ( ) ( )
set
) )
Function-like
V34
()
FinSequence-like
FinSubsequence-like
)
Element
of
REAL
b
1
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) : ( ( ) (
functional
FinSequence-membered
)
FinSequenceSet
of
REAL
: ( ( ) ( )
set
) ) ) holds
'not'
y
: ( (
V41
(
b
1
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
Tuple
of
b
1
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ,
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) : ( (
V41
(
b
1
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
FinSequence
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
=
n
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
|->
1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) : ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
Function-like
V34
()
V41
(
b
1
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
Element
of
b
1
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
-tuples_on
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) : ( ( ) ( non
empty
functional
FinSequence-membered
)
FinSequenceSet
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) ) ;
theorem
:: BINARI_3:6
for
n
being ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
for
F
being ( (
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
Tuple
of
n
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ,
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) st
F
: ( (
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
Tuple
of
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ,
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
=
0*
n
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) : ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
REAL
: ( ( ) ( )
set
) )
Function-like
V34
()
FinSequence-like
FinSubsequence-like
)
Element
of
REAL
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) : ( ( ) (
functional
FinSequence-membered
)
FinSequenceSet
of
REAL
: ( ( ) ( )
set
) ) ) holds
Absval
F
: ( (
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
Tuple
of
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ,
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) : ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
=
0
: ( ( ) (
empty
trivial
V4
()
V5
()
V6
()
V8
()
V9
()
V10
()
V11
()
V12
()
V13
()
functional
FinSequence-membered
ext-real
non
negative
V75
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) ;
theorem
:: BINARI_3:7
for
n
being ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
for
F
being ( (
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
Tuple
of
n
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ,
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) st
F
: ( (
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
Tuple
of
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ,
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
=
0*
n
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) : ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
REAL
: ( ( ) ( )
set
) )
Function-like
V34
()
FinSequence-like
FinSubsequence-like
)
Element
of
REAL
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) : ( ( ) (
functional
FinSequence-membered
)
FinSequenceSet
of
REAL
: ( ( ) ( )
set
) ) ) holds
Absval
(
'not'
F
: ( (
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
Tuple
of
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ,
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
)
: ( (
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
FinSequence
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) : ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
=
(
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
to_power
n
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
)
: ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
-
1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) : ( ( ) (
V11
()
V12
()
V13
()
ext-real
)
set
) ;
theorem
:: BINARI_3:8
for
n
being ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) holds
Rev
(
0*
n
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
REAL
: ( ( ) ( )
set
) )
Function-like
V34
()
FinSequence-like
FinSubsequence-like
)
Element
of
REAL
b
1
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) : ( ( ) (
functional
FinSequence-membered
)
FinSequenceSet
of
REAL
: ( ( ) ( )
set
) ) ) : ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
REAL
: ( ( ) ( )
set
) )
Function-like
V34
()
FinSequence-like
FinSubsequence-like
)
FinSequence
of
REAL
: ( ( ) ( )
set
) )
=
0*
n
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) : ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
REAL
: ( ( ) ( )
set
) )
Function-like
V34
()
FinSequence-like
FinSubsequence-like
)
Element
of
REAL
b
1
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) : ( ( ) (
functional
FinSequence-membered
)
FinSequenceSet
of
REAL
: ( ( ) ( )
set
) ) ) ;
theorem
:: BINARI_3:9
for
n
being ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
for
y
being ( (
V41
(
b
1
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
Tuple
of
n
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ,
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) st
y
: ( (
V41
(
b
1
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
Tuple
of
b
1
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ,
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
=
0*
n
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) : ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
REAL
: ( ( ) ( )
set
) )
Function-like
V34
()
FinSequence-like
FinSubsequence-like
)
Element
of
REAL
b
1
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) : ( ( ) (
functional
FinSequence-membered
)
FinSequenceSet
of
REAL
: ( ( ) ( )
set
) ) ) holds
Rev
(
'not'
y
: ( (
V41
(
b
1
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
Tuple
of
b
1
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ,
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
)
: ( (
V41
(
b
1
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
FinSequence
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) : ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
FinSequence-like
FinSubsequence-like
)
FinSequence
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
=
'not'
y
: ( (
V41
(
b
1
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
Tuple
of
b
1
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ,
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) : ( (
V41
(
b
1
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
FinSequence
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) ;
theorem
:: BINARI_3:10
Bin1
1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) : ( (
V41
(1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) )
FinSequence-like
FinSubsequence-like
)
FinSequence
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
=
<*
TRUE
: ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
boolean
)
Element
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
*>
: ( (
V41
(1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) ) ) ( non
empty
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) )
FinSequence-like
FinSubsequence-like
)
FinSequence
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) ;
theorem
:: BINARI_3:11
for
n
being ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) holds
Absval
(
Bin1
n
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
)
: ( (
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
FinSequence
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) : ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
=
1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) ;
theorem
:: BINARI_3:12
for
x
,
y
being ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
boolean
)
Element
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) holds
( ( not
x
: ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
boolean
)
Element
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
'or'
y
: ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
boolean
)
Element
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) : ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
boolean
)
Element
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
=
TRUE
: ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
boolean
)
Element
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) or
x
: ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
boolean
)
Element
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
=
TRUE
: ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
boolean
)
Element
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) or
y
: ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
boolean
)
Element
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
=
TRUE
: ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
boolean
)
Element
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) ) & ( (
x
: ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
boolean
)
Element
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
=
TRUE
: ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
boolean
)
Element
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) or
y
: ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
boolean
)
Element
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
=
TRUE
: ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
boolean
)
Element
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) ) implies
x
: ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
boolean
)
Element
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
'or'
y
: ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
boolean
)
Element
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) : ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
boolean
)
Element
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
=
TRUE
: ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
boolean
)
Element
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) ) & (
x
: ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
boolean
)
Element
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
'or'
y
: ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
boolean
)
Element
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) : ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
boolean
)
Element
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
=
FALSE
: ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
boolean
)
Element
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) implies (
x
: ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
boolean
)
Element
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
=
FALSE
: ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
boolean
)
Element
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) &
y
: ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
boolean
)
Element
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
=
FALSE
: ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
boolean
)
Element
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) ) ) & (
x
: ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
boolean
)
Element
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
=
FALSE
: ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
boolean
)
Element
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) &
y
: ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
boolean
)
Element
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
=
FALSE
: ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
boolean
)
Element
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) implies
x
: ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
boolean
)
Element
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
'or'
y
: ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
boolean
)
Element
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) : ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
boolean
)
Element
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
=
FALSE
: ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
boolean
)
Element
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) ) ) ;
theorem
:: BINARI_3:13
for
x
,
y
being ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
boolean
)
Element
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) holds
(
add_ovfl
(
<*
x
: ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
boolean
)
Element
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
*>
: ( (
V41
(1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) ) ) ( non
empty
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) )
FinSequence-like
FinSubsequence-like
)
FinSequence
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) ,
<*
y
: ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
boolean
)
Element
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
*>
: ( (
V41
(1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) ) ) ( non
empty
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) )
FinSequence-like
FinSubsequence-like
)
FinSequence
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) ) : ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
boolean
)
Element
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
=
TRUE
: ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
boolean
)
Element
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) iff (
x
: ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
boolean
)
Element
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
=
TRUE
: ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
boolean
)
Element
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) &
y
: ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
boolean
)
Element
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
=
TRUE
: ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
boolean
)
Element
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) ) ) ;
theorem
:: BINARI_3:14
'not'
<*
FALSE
: ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
boolean
)
Element
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
*>
: ( (
V41
(1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) ) ) ( non
empty
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) )
FinSequence-like
FinSubsequence-like
)
FinSequence
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) : ( (
V41
(1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) )
FinSequence-like
FinSubsequence-like
)
FinSequence
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
=
<*
TRUE
: ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
boolean
)
Element
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
*>
: ( (
V41
(1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) ) ) ( non
empty
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) )
FinSequence-like
FinSubsequence-like
)
FinSequence
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) ;
theorem
:: BINARI_3:15
'not'
<*
TRUE
: ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
boolean
)
Element
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
*>
: ( (
V41
(1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) ) ) ( non
empty
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) )
FinSequence-like
FinSubsequence-like
)
FinSequence
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) : ( (
V41
(1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) )
FinSequence-like
FinSubsequence-like
)
FinSequence
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
=
<*
FALSE
: ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
boolean
)
Element
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
*>
: ( (
V41
(1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) ) ) ( non
empty
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) )
FinSequence-like
FinSubsequence-like
)
FinSequence
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) ;
theorem
:: BINARI_3:16
<*
FALSE
: ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
boolean
)
Element
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
*>
: ( (
V41
(1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) ) ) ( non
empty
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) )
FinSequence-like
FinSubsequence-like
)
FinSequence
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
+
<*
FALSE
: ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
boolean
)
Element
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
*>
: ( (
V41
(1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) ) ) ( non
empty
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) )
FinSequence-like
FinSubsequence-like
)
FinSequence
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) : ( (
V41
(1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) )
FinSequence-like
FinSubsequence-like
)
FinSequence
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
=
<*
FALSE
: ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
boolean
)
Element
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
*>
: ( (
V41
(1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) ) ) ( non
empty
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) )
FinSequence-like
FinSubsequence-like
)
FinSequence
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) ;
theorem
:: BINARI_3:17
(
<*
FALSE
: ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
boolean
)
Element
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
*>
: ( (
V41
(1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) ) ) ( non
empty
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) )
FinSequence-like
FinSubsequence-like
)
FinSequence
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
+
<*
TRUE
: ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
boolean
)
Element
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
*>
: ( (
V41
(1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) ) ) ( non
empty
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) )
FinSequence-like
FinSubsequence-like
)
FinSequence
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) : ( (
V41
(1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) )
FinSequence-like
FinSubsequence-like
)
FinSequence
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
=
<*
TRUE
: ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
boolean
)
Element
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
*>
: ( (
V41
(1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) ) ) ( non
empty
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) )
FinSequence-like
FinSubsequence-like
)
FinSequence
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) &
<*
TRUE
: ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
boolean
)
Element
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
*>
: ( (
V41
(1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) ) ) ( non
empty
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) )
FinSequence-like
FinSubsequence-like
)
FinSequence
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
+
<*
FALSE
: ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
boolean
)
Element
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
*>
: ( (
V41
(1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) ) ) ( non
empty
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) )
FinSequence-like
FinSubsequence-like
)
FinSequence
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) : ( (
V41
(1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) )
FinSequence-like
FinSubsequence-like
)
FinSequence
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
=
<*
TRUE
: ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
boolean
)
Element
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
*>
: ( (
V41
(1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) ) ) ( non
empty
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) )
FinSequence-like
FinSubsequence-like
)
FinSequence
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) ) ;
theorem
:: BINARI_3:18
<*
TRUE
: ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
boolean
)
Element
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
*>
: ( (
V41
(1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) ) ) ( non
empty
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) )
FinSequence-like
FinSubsequence-like
)
FinSequence
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
+
<*
TRUE
: ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
boolean
)
Element
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
*>
: ( (
V41
(1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) ) ) ( non
empty
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) )
FinSequence-like
FinSubsequence-like
)
FinSequence
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) : ( (
V41
(1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) )
FinSequence-like
FinSubsequence-like
)
FinSequence
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
=
<*
FALSE
: ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
boolean
)
Element
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
*>
: ( (
V41
(1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) ) ) ( non
empty
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) )
FinSequence-like
FinSubsequence-like
)
FinSequence
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) ;
theorem
:: BINARI_3:19
for
n
being ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
for
x
,
y
being ( (
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
Tuple
of
n
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ,
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) st
x
: ( (
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
Tuple
of
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ,
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
/.
n
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) : ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
boolean
)
Element
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
=
TRUE
: ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
boolean
)
Element
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) &
(
carry
(
x
: ( (
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
Tuple
of
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ,
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) ,
(
Bin1
n
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
)
: ( (
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
FinSequence
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) )
)
: ( (
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
FinSequence
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
/.
n
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) : ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
boolean
)
Element
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
=
TRUE
: ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
boolean
)
Element
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) holds
for
k
being ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) st
k
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
<>
1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) &
k
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
<=
n
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) holds
(
x
: ( (
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
Tuple
of
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ,
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
/.
k
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) : ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
boolean
)
Element
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
=
TRUE
: ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
boolean
)
Element
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) &
(
carry
(
x
: ( (
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
Tuple
of
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ,
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) ,
(
Bin1
n
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
)
: ( (
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
FinSequence
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) )
)
: ( (
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
FinSequence
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
/.
k
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) : ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
boolean
)
Element
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
=
TRUE
: ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
boolean
)
Element
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) ) ;
theorem
:: BINARI_3:20
for
n
being ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
for
x
being ( (
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
Tuple
of
n
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ,
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) st
x
: ( (
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
Tuple
of
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ,
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
/.
n
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) : ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
boolean
)
Element
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
=
TRUE
: ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
boolean
)
Element
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) &
(
carry
(
x
: ( (
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
Tuple
of
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ,
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) ,
(
Bin1
n
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
)
: ( (
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
FinSequence
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) )
)
: ( (
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
FinSequence
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
/.
n
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) : ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
boolean
)
Element
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
=
TRUE
: ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
boolean
)
Element
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) holds
carry
(
x
: ( (
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
Tuple
of
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ,
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) ,
(
Bin1
n
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
)
: ( (
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
FinSequence
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) ) : ( (
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
FinSequence
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
=
'not'
(
Bin1
n
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
)
: ( (
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
FinSequence
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) : ( (
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
FinSequence
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) ;
theorem
:: BINARI_3:21
for
n
being ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
for
x
,
y
being ( (
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
Tuple
of
n
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ,
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) st
y
: ( (
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
Tuple
of
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ,
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
=
0*
n
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) : ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
REAL
: ( ( ) ( )
set
) )
Function-like
V34
()
FinSequence-like
FinSubsequence-like
)
Element
of
REAL
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) : ( ( ) (
functional
FinSequence-membered
)
FinSequenceSet
of
REAL
: ( ( ) ( )
set
) ) ) &
x
: ( (
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
Tuple
of
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ,
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
/.
n
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) : ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
boolean
)
Element
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
=
TRUE
: ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
boolean
)
Element
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) &
(
carry
(
x
: ( (
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
Tuple
of
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ,
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) ,
(
Bin1
n
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
)
: ( (
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
FinSequence
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) )
)
: ( (
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
FinSequence
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
/.
n
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) : ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
boolean
)
Element
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
=
TRUE
: ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
boolean
)
Element
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) holds
x
: ( (
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
Tuple
of
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ,
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
=
'not'
y
: ( (
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
Tuple
of
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ,
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) : ( (
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
FinSequence
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) ;
theorem
:: BINARI_3:22
for
n
being ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
for
y
being ( (
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
Tuple
of
n
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ,
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) st
y
: ( (
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
Tuple
of
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ,
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
=
0*
n
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) : ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
REAL
: ( ( ) ( )
set
) )
Function-like
V34
()
FinSequence-like
FinSubsequence-like
)
Element
of
REAL
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) : ( ( ) (
functional
FinSequence-membered
)
FinSequenceSet
of
REAL
: ( ( ) ( )
set
) ) ) holds
carry
(
(
'not'
y
: ( (
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
Tuple
of
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ,
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
)
: ( (
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
FinSequence
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) ,
(
Bin1
n
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
)
: ( (
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
FinSequence
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) ) : ( (
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
FinSequence
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
=
'not'
(
Bin1
n
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
)
: ( (
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
FinSequence
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) : ( (
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
FinSequence
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) ;
theorem
:: BINARI_3:23
for
n
being ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
for
x
,
y
being ( (
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
Tuple
of
n
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ,
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) st
y
: ( (
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
Tuple
of
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ,
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
=
0*
n
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) : ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
REAL
: ( ( ) ( )
set
) )
Function-like
V34
()
FinSequence-like
FinSubsequence-like
)
Element
of
REAL
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) : ( ( ) (
functional
FinSequence-membered
)
FinSequenceSet
of
REAL
: ( ( ) ( )
set
) ) ) holds
(
add_ovfl
(
x
: ( (
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
Tuple
of
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ,
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) ,
(
Bin1
n
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
)
: ( (
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
FinSequence
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) ) : ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
boolean
)
Element
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
=
TRUE
: ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
boolean
)
Element
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) iff
x
: ( (
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
Tuple
of
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ,
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
=
'not'
y
: ( (
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
Tuple
of
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ,
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) : ( (
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
FinSequence
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) ) ;
theorem
:: BINARI_3:24
for
n
being ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
for
z
being ( (
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
Tuple
of
n
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ,
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) st
z
: ( (
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
Tuple
of
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ,
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
=
0*
n
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) : ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
REAL
: ( ( ) ( )
set
) )
Function-like
V34
()
FinSequence-like
FinSubsequence-like
)
Element
of
REAL
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) : ( ( ) (
functional
FinSequence-membered
)
FinSequenceSet
of
REAL
: ( ( ) ( )
set
) ) ) holds
(
'not'
z
: ( (
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
Tuple
of
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ,
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
)
: ( (
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
FinSequence
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
+
(
Bin1
n
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
)
: ( (
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
FinSequence
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) : ( (
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
FinSequence
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
=
z
: ( (
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
Tuple
of
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ,
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) ;
begin
definition
let
n
,
k
be ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ;
func
n
-BinarySequence
k
->
( (
V41
(
n
: ( (
V12
() ) (
V11
()
V12
()
ext-real
)
set
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
n
: ( (
V12
() ) (
V11
()
V12
()
ext-real
)
set
) )
FinSequence-like
FinSubsequence-like
)
Tuple
of
n
: ( (
V12
() ) (
V11
()
V12
()
ext-real
)
set
) ,
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
means
:: BINARI_3:def 1
for
i
being ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) st
i
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
in
Seg
n
: ( (
V12
() ) (
V11
()
V12
()
ext-real
)
set
) : ( ( ) ( )
Element
of
bool
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) holds
it
: ( (
V12
() ) (
V11
()
V12
()
ext-real
)
set
)
/.
i
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) : ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
boolean
)
Element
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
=
IFEQ
(
(
(
k
: ( (
V12
() ) (
V11
()
V12
()
ext-real
)
set
)
div
(
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
to_power
(
i
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
-'
1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
mod
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) ,
0
: ( ( ) (
empty
trivial
V4
()
V5
()
V6
()
V8
()
V9
()
V10
()
V11
()
V12
()
V13
()
functional
FinSequence-membered
ext-real
non
negative
V75
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) ,
FALSE
: ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
boolean
)
Element
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) ,
TRUE
: ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
boolean
)
Element
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) ) : ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
boolean
)
Element
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) ;
end;
theorem
:: BINARI_3:25
for
n
being ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) holds
n
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
-BinarySequence
0
: ( ( ) (
empty
trivial
V4
()
V5
()
V6
()
V8
()
V9
()
V10
()
V11
()
V12
()
V13
()
functional
FinSequence-membered
ext-real
non
negative
V75
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) : ( (
V41
(
b
1
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
Tuple
of
b
1
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ,
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
=
0*
n
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) : ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
REAL
: ( ( ) ( )
set
) )
Function-like
V34
()
FinSequence-like
FinSubsequence-like
)
Element
of
REAL
b
1
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) : ( ( ) (
functional
FinSequence-membered
)
FinSequenceSet
of
REAL
: ( ( ) ( )
set
) ) ) ;
theorem
:: BINARI_3:26
for
n
,
k
being ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) st
k
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
<
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
to_power
n
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) : ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) holds
(
(
n
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
+
1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
set
)
-BinarySequence
k
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
)
: ( (
V41
(
b
1
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
+
1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
set
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
+
1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
set
) )
FinSequence-like
FinSubsequence-like
)
Tuple
of
b
1
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
+
1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
set
) ,
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
.
(
n
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
+
1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
set
) : ( ( ) ( )
set
)
=
FALSE
: ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
boolean
)
Element
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) ;
theorem
:: BINARI_3:27
for
n
being ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
for
k
being ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) st
k
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
<
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
to_power
n
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) : ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) holds
(
n
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
+
1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
set
)
-BinarySequence
k
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) : ( (
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
+
1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
set
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
+
1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
set
) )
FinSequence-like
FinSubsequence-like
)
Tuple
of
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
+
1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
set
) ,
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
=
(
n
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
-BinarySequence
k
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
)
: ( (
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
Tuple
of
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ,
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
^
<*
FALSE
: ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
boolean
)
Element
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
*>
: ( (
V41
(1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) ) ) ( non
empty
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) )
FinSequence-like
FinSubsequence-like
)
FinSequence
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) : ( (
V41
(
K307
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ,1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) ) ) ( non
empty
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
K192
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ,1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) )
V41
(
K307
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ,1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) )
FinSequence-like
FinSubsequence-like
)
FinSequence
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) ;
theorem
:: BINARI_3:28
for
i
being ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) holds
(
i
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
+
1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
set
)
-BinarySequence
(
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
to_power
i
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
)
: ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) : ( (
V41
(
b
1
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
+
1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
set
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
+
1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
set
) )
FinSequence-like
FinSubsequence-like
)
Tuple
of
b
1
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
+
1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
set
) ,
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
=
(
0*
i
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
REAL
: ( ( ) ( )
set
) )
Function-like
V34
()
FinSequence-like
FinSubsequence-like
)
Element
of
REAL
b
1
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) : ( ( ) (
functional
FinSequence-membered
)
FinSequenceSet
of
REAL
: ( ( ) ( )
set
) ) )
^
<*
1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
*>
: ( (
V41
(1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) ) ) ( non
empty
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
Function-like
V34
()
V41
(1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) )
FinSequence-like
FinSubsequence-like
)
FinSequence
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) : ( (
V15
()
Function-like
FinSequence-like
) ( non
empty
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
Function-like
V34
()
FinSequence-like
FinSubsequence-like
)
set
) ;
theorem
:: BINARI_3:29
for
n
being ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
for
k
being ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) st 2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
to_power
n
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) : ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
<=
k
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) &
k
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
<
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
to_power
(
n
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
+
1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
set
) : ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) holds
(
(
n
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
+
1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
set
)
-BinarySequence
k
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
)
: ( (
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
+
1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
set
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
+
1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
set
) )
FinSequence-like
FinSubsequence-like
)
Tuple
of
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
+
1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
set
) ,
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
.
(
n
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
+
1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
set
) : ( ( ) ( )
set
)
=
TRUE
: ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
boolean
)
Element
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) ;
theorem
:: BINARI_3:30
for
n
being ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
for
k
being ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) st 2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
to_power
n
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) : ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
<=
k
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) &
k
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
<
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
to_power
(
n
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
+
1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
set
) : ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) holds
(
n
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
+
1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
set
)
-BinarySequence
k
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) : ( (
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
+
1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
set
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
+
1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
set
) )
FinSequence-like
FinSubsequence-like
)
Tuple
of
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
+
1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
set
) ,
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
=
(
n
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
-BinarySequence
(
k
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
-'
(
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
to_power
n
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
)
: ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( (
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
Tuple
of
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ,
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
^
<*
TRUE
: ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
boolean
)
Element
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
*>
: ( (
V41
(1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) ) ) ( non
empty
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) )
FinSequence-like
FinSubsequence-like
)
FinSequence
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) : ( (
V41
(
K307
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ,1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) ) ) ( non
empty
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
K192
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ,1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) )
V41
(
K307
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ,1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) )
FinSequence-like
FinSubsequence-like
)
FinSequence
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) ;
theorem
:: BINARI_3:31
for
n
being ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
for
k
being ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) st
k
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
<
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
to_power
n
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) : ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) holds
for
x
being ( (
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
Tuple
of
n
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ,
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) st
x
: ( (
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
Tuple
of
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ,
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
=
0*
n
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) : ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
REAL
: ( ( ) ( )
set
) )
Function-like
V34
()
FinSequence-like
FinSubsequence-like
)
Element
of
REAL
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) : ( ( ) (
functional
FinSequence-membered
)
FinSequenceSet
of
REAL
: ( ( ) ( )
set
) ) ) holds
(
n
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
-BinarySequence
k
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) : ( (
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
Tuple
of
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ,
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
=
'not'
x
: ( (
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
Tuple
of
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ,
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) : ( (
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
FinSequence
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) iff
k
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
=
(
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
to_power
n
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
)
: ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
-
1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) : ( ( ) (
V11
()
V12
()
V13
()
ext-real
)
set
) ) ;
theorem
:: BINARI_3:32
for
n
being ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
for
k
being ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) st
k
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
+
1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
set
)
<
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
to_power
n
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) : ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) holds
add_ovfl
(
(
n
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
-BinarySequence
k
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
)
: ( (
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
Tuple
of
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ,
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) ,
(
Bin1
n
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
)
: ( (
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
FinSequence
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) ) : ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
boolean
)
Element
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
=
FALSE
: ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
boolean
)
Element
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) ;
theorem
:: BINARI_3:33
for
n
being ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
for
k
being ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) st
k
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
+
1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
set
)
<
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
to_power
n
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) : ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) holds
n
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
-BinarySequence
(
k
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
+
1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
set
) : ( (
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
Tuple
of
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ,
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
=
(
n
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
-BinarySequence
k
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
)
: ( (
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
Tuple
of
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ,
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
+
(
Bin1
n
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
)
: ( (
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
FinSequence
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) : ( (
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
FinSequence
of
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) ;
theorem
:: BINARI_3:34
for
n
,
i
being ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) holds
(
n
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
+
1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
set
)
-BinarySequence
i
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) : ( (
V41
(
b
1
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
+
1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
set
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
+
1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
set
) )
FinSequence-like
FinSubsequence-like
)
Tuple
of
b
1
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
+
1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
set
) ,
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
=
<*
(
i
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
mod
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
*>
: ( (
V41
(1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) ) ) ( non
empty
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
Function-like
V34
()
V41
(1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) )
FinSequence-like
FinSubsequence-like
)
FinSequence
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
^
(
n
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
-BinarySequence
(
i
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
div
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( (
V41
(
b
1
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
Tuple
of
b
1
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ,
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) : ( (
V15
()
Function-like
FinSequence-like
) ( non
empty
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
Function-like
V34
()
FinSequence-like
FinSubsequence-like
)
set
) ;
theorem
:: BINARI_3:35
for
n
being ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
for
k
being ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) st
k
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
<
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
positive
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
to_power
n
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) : ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) holds
Absval
(
n
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
-BinarySequence
k
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
)
: ( (
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
Tuple
of
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ,
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) : ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
=
k
: ( (
V10
() ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ;
theorem
:: BINARI_3:36
for
n
being ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
for
x
being ( (
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
Tuple
of
n
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ,
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) holds
n
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
)
-BinarySequence
(
Absval
x
: ( (
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
Tuple
of
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ,
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
)
: ( ( ) (
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) : ( (
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
Tuple
of
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ,
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
=
x
: ( (
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ) ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
V19
(
BOOLEAN
: ( ( ) ( non
empty
)
set
) )
Function-like
V34
()
V41
(
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) )
FinSequence-like
FinSubsequence-like
)
Tuple
of
b
1
: ( ( non
empty
V10
() ) ( non
empty
V4
()
V5
()
V6
()
V10
()
V11
()
V12
()
V13
()
ext-real
non
negative
)
Nat
) ,
BOOLEAN
: ( ( ) ( non
empty
)
set
) ) ;