:: PRGCOR_1 semantic presentation

REAL is set
NAT is V4() V7() V8() V9() Element of K11(REAL)
K11(REAL) is set
COMPLEX is set
NAT is V4() V7() V8() V9() set
K11(NAT) is set
K11(NAT) is set
RAT is set
INT is set
K12(COMPLEX,COMPLEX) is set
K11(K12(COMPLEX,COMPLEX)) is set
K12(K12(COMPLEX,COMPLEX),COMPLEX) is set
K11(K12(K12(COMPLEX,COMPLEX),COMPLEX)) is set
K12(REAL,REAL) is set
K11(K12(REAL,REAL)) is set
K12(K12(REAL,REAL),REAL) is set
K11(K12(K12(REAL,REAL),REAL)) is set
K12(RAT,RAT) is set
K11(K12(RAT,RAT)) is set
K12(K12(RAT,RAT),RAT) is set
K11(K12(K12(RAT,RAT),RAT)) is set
K12(INT,INT) is set
K11(K12(INT,INT)) is set
K12(K12(INT,INT),INT) is set
K11(K12(K12(INT,INT),INT)) is set
K12(NAT,NAT) is set
K12(K12(NAT,NAT),NAT) is set
K11(K12(K12(NAT,NAT),NAT)) is set
K304() is set
1 is ext-real positive non negative V4() V7() V8() V9() V13() V14() V15() integer Element of NAT
0 is ext-real non positive non negative V4() V7() V8() V9() V11() V12() V13() V14() V15() integer Element of NAT
2 is ext-real positive non negative V4() V7() V8() V9() V13() V14() V15() integer Element of NAT
n is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
m2 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
n + m2 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
m is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
m + m2 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
(n + m2) -' (m + m2) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
n -' m is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
(n + m2) - (m + m2) is ext-real V14() V15() integer set
n - m is ext-real V14() V15() integer set
m is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
n is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
2 * m is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
n mod (2 * m) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
(n mod (2 * m)) - m is ext-real V14() V15() integer set
n mod m is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
(n mod m) + m is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
m2 is ext-real non negative V7() V8() V9() V13() V14() V15() integer set
(2 * m) * m2 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
((2 * m) * m2) + (n mod (2 * m)) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
m2 is ext-real non negative V7() V8() V9() V13() V14() V15() integer set
(2 * m) * m2 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
((2 * m) * m2) + (n mod (2 * m)) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
2 * 0 is ext-real non positive non negative V4() V7() V8() V9() V11() V12() V13() V14() V15() integer Element of NAT
(2 * m) - m is ext-real V14() V15() integer set
(n mod (2 * m)) -' m is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
n2 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
2 * n2 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
(2 * n2) + 1 is ext-real positive non negative V4() V7() V8() V9() V13() V14() V15() integer Element of NAT
m * ((2 * n2) + 1) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
(m * ((2 * n2) + 1)) + ((n mod (2 * m)) -' m) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
m is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
n is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
2 * m is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
n mod (2 * m) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
n div m is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
n div (2 * m) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
(n div (2 * m)) * 2 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
((n div (2 * m)) * 2) + 1 is ext-real positive non negative V4() V7() V8() V9() V13() V14() V15() integer Element of NAT
2 * 0 is ext-real non positive non negative V4() V7() V8() V9() V11() V12() V13() V14() V15() integer Element of NAT
(2 * m) * (n div (2 * m)) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
((2 * m) * (n div (2 * m))) + (n mod (2 * m)) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
n mod m is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
(n mod m) + m is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
((2 * m) * (n div (2 * m))) + ((n mod m) + m) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
2 * (n div (2 * m)) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
(2 * (n div (2 * m))) + 1 is ext-real positive non negative V4() V7() V8() V9() V13() V14() V15() integer Element of NAT
m * ((2 * (n div (2 * m))) + 1) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
(m * ((2 * (n div (2 * m))) + 1)) + (n mod m) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
m is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
n is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
2 * m is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
n mod (2 * m) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
n mod m is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
m2 is ext-real non negative V7() V8() V9() V13() V14() V15() integer set
(2 * m) * m2 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
((2 * m) * m2) + (n mod (2 * m)) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
m2 is ext-real non negative V7() V8() V9() V13() V14() V15() integer set
(2 * m) * m2 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
((2 * m) * m2) + (n mod (2 * m)) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
n2 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
2 * n2 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
m * (2 * n2) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
(m * (2 * n2)) + (n mod (2 * m)) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
m is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
n is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
2 * m is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
n mod (2 * m) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
n div m is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
n div (2 * m) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
(n div (2 * m)) * 2 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
2 * 0 is ext-real non positive non negative V4() V7() V8() V9() V11() V12() V13() V14() V15() integer Element of NAT
(2 * m) * (n div (2 * m)) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
((2 * m) * (n div (2 * m))) + (n mod (2 * m)) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
2 * (n div (2 * m)) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
m * (2 * (n div (2 * m))) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
n mod m is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
(m * (2 * (n div (2 * m)))) + (n mod m) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
n is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
m is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
m + 1 is ext-real positive non negative V4() V7() V8() V9() V13() V14() V15() integer Element of NAT
(m + 1) - 1 is ext-real V14() V15() integer set
(m + 1) -' 1 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
0 + 1 is ext-real positive non negative V4() V7() V8() V9() V13() V14() V15() integer Element of NAT
1 * m is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
n * m is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
2 |^ ((m + 1) -' 1) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
n * (2 |^ ((m + 1) -' 1)) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
n * ((m + 1) -' 1) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
m2 is ext-real non negative V7() V8() V9() V13() V14() V15() integer set
2 |^ m2 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of REAL
n * (2 |^ m2) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
m2 is ext-real non negative V7() V8() V9() V13() V14() V15() integer set
2 |^ m2 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of REAL
n * (2 |^ m2) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
n2 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
2 |^ n2 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
n * (2 |^ n2) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
n is ext-real V14() V15() integer set
m is V16() Function-like FinSequence-like set
len m is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
dom m is Element of K11(NAT)
n is ext-real V14() V15() integer set
m is ext-real V14() V15() integer set
n + 1 is ext-real V14() V15() integer set
m2 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
m2 + 1 is ext-real positive non negative V4() V7() V8() V9() V13() V14() V15() integer Element of NAT
Seg (m2 + 1) is Element of K11(NAT)
(Seg (m2 + 1)) --> 1 is V16() V19( Seg (m2 + 1)) V20( NAT ) V20( INT ) Function-like V30( Seg (m2 + 1), NAT ) Element of K11(K12((Seg (m2 + 1)),NAT))
K12((Seg (m2 + 1)),NAT) is set
K11(K12((Seg (m2 + 1)),NAT)) is set
dom ((Seg (m2 + 1)) --> 1) is Element of K11((Seg (m2 + 1)))
K11((Seg (m2 + 1))) is set
ppn is V16() Function-like FinSequence-like set
rng ppn is set
{1} is V4() set
ii0 is set
ii0 is V16() V19( NAT ) V20( INT ) Function-like FinSequence-like FinSequence of INT
len ii0 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
m2 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
n2 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
2 |^ 0 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
n2 * (2 |^ 0) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
n2 * 1 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
m2 + 1 is ext-real positive non negative V4() V7() V8() V9() V13() V14() V15() integer Element of NAT
ppn is V16() Function-like FinSequence-like set
len ppn is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
dom ppn is Element of K11(NAT)
ppn is V16() Function-like FinSequence-like set
len ppn is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
dom ppn is Element of K11(NAT)
Seg (m2 + 1) is Element of K11(NAT)
rng ppn is set
ppn is set
ii0 is set
ppn . ii0 is set
i0 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
ppn . i0 is set
i0 -' 1 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
2 |^ (i0 -' 1) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
n2 * (2 |^ (i0 -' 1)) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
m2 div (n2 * (2 |^ (i0 -' 1))) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
0 + 1 is ext-real positive non negative V4() V7() V8() V9() V13() V14() V15() integer Element of NAT
ppn is V16() V19( NAT ) V20( INT ) Function-like FinSequence-like FinSequence of INT
ppn . 1 is ext-real V14() V15() integer set
1 -' 1 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
2 |^ (1 -' 1) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
n2 * (2 |^ (1 -' 1)) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
m2 div (n2 * (2 |^ (1 -' 1))) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
m2 div n2 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
ii0 is V16() Function-like FinSequence-like set
len ii0 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
dom ii0 is Element of K11(NAT)
ii0 is V16() Function-like FinSequence-like set
len ii0 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
dom ii0 is Element of K11(NAT)
rng ii0 is set
i0 is set
k5 is set
ii0 . k5 is set
ssn is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
ii0 . ssn is set
ssn -' 1 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
2 |^ (ssn -' 1) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
m * (2 |^ (ssn -' 1)) is ext-real V14() V15() integer set
i0 is V16() Function-like FinSequence-like set
len i0 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
dom i0 is Element of K11(NAT)
i0 is V16() Function-like FinSequence-like set
len i0 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
dom i0 is Element of K11(NAT)
rng i0 is set
k5 is set
ssn is set
i0 . ssn is set
ssn is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
i0 . ssn is set
ssn -' 1 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
2 |^ (ssn -' 1) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
n2 * (2 |^ (ssn -' 1)) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
m2 mod (n2 * (2 |^ (ssn -' 1))) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
ssn is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
2 |^ ssn is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
n2 * (2 |^ ssn) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
ssn is ext-real V14() V15() integer set
ssn + 1 is ext-real V14() V15() integer set
ssn - 1 is ext-real V14() V15() integer set
1 + 0 is ext-real positive non negative V4() V7() V8() V9() V13() V14() V15() integer Element of NAT
2 |^ m2 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
1 * (2 |^ m2) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
n2 * (2 |^ m2) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
m * (2 |^ m2) is ext-real V14() V15() integer set
1 + ssn is ext-real positive non negative V4() V7() V8() V9() V13() V14() V15() integer Element of NAT
ssn + 1 is ext-real positive non negative V4() V7() V8() V9() V13() V14() V15() integer Element of NAT
(ssn + 1) -' 1 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
2 |^ ((ssn + 1) -' 1) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
n2 * (2 |^ ((ssn + 1) -' 1)) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
ssm is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
k5 is V16() V19( NAT ) V20( INT ) Function-like FinSequence-like FinSequence of INT
k5 . (ssn + 1) is ext-real V14() V15() integer set
m2 mod (n2 * (2 |^ ((ssn + 1) -' 1))) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
(ssn - 1) + 1 is ext-real V14() V15() integer set
ssn -' 1 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
(ssn -' 1) + 1 is ext-real positive non negative V4() V7() V8() V9() V13() V14() V15() integer Element of NAT
2 |^ (ssn -' 1) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
(2 |^ (ssn -' 1)) * 2 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
ssm is V16() V19( NAT ) V20( INT ) Function-like FinSequence-like FinSequence of INT
ssm . 1 is ext-real V14() V15() integer set
m * (2 |^ (1 -' 1)) is ext-real V14() V15() integer set
m * (2 |^ 0) is ext-real V14() V15() integer set
m * 1 is ext-real V14() V15() integer set
m2 div (n2 * (2 |^ ((ssn + 1) -' 1))) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
ppn . (ssn + 1) is ext-real V14() V15() integer set
k is ext-real V14() V15() integer set
(ssn + 1) - k is ext-real V14() V15() integer set
ssm . ((ssn + 1) - k) is ext-real V14() V15() integer set
k - 1 is ext-real V14() V15() integer set
(ssn + 1) - (k - 1) is ext-real V14() V15() integer set
k5 . ((ssn + 1) - (k - 1)) is ext-real V14() V15() integer set
k5 . ((ssn + 1) - k) is ext-real V14() V15() integer set
(k5 . ((ssn + 1) - (k - 1))) - (ssm . ((ssn + 1) - k)) is ext-real V14() V15() integer set
ppn . ((ssn + 1) - k) is ext-real V14() V15() integer set
ppn . ((ssn + 1) - (k - 1)) is ext-real V14() V15() integer set
(ppn . ((ssn + 1) - (k - 1))) * 2 is ext-real V14() V15() integer set
((ppn . ((ssn + 1) - (k - 1))) * 2) + 1 is ext-real V14() V15() integer set
ssn - k is ext-real V14() V15() integer set
kk is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
ssn -' kk is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
(ssn + 1) -' kk is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
m2 + k is ext-real V14() V15() integer set
(m2 + k) - k is ext-real V14() V15() integer set
((ssn + 1) -' kk) + 1 is ext-real positive non negative V4() V7() V8() V9() V13() V14() V15() integer Element of NAT
k + 1 is ext-real V14() V15() integer set
kk -' 1 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
(ssn + 1) - (kk -' 1) is ext-real V14() V15() integer set
kk + 1 is ext-real positive non negative V4() V7() V8() V9() V13() V14() V15() integer Element of NAT
2 |^ (ssn -' kk) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
n2 * (2 |^ (ssn -' kk)) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
n2 * 0 is ext-real non positive non negative V4() V7() V8() V9() V11() V12() V13() V14() V15() integer Element of NAT
((ssn + 1) -' kk) - 1 is ext-real V14() V15() integer set
((ssn + 1) -' kk) -' 1 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
k5 . ((ssn + 1) -' kk) is ext-real V14() V15() integer set
2 |^ (((ssn + 1) -' kk) -' 1) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
n2 * (2 |^ (((ssn + 1) -' kk) -' 1)) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
m2 mod (n2 * (2 |^ (((ssn + 1) -' kk) -' 1))) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
(ssn - k) + 1 is ext-real V14() V15() integer set
ssm . ((ssn + 1) -' kk) is ext-real V14() V15() integer set
(ssn + 1) -' (kk -' 1) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
((ssn + 1) - k) + 1 is ext-real V14() V15() integer set
((ssn + 1) -' (kk -' 1)) -' 1 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
k5 . ((ssn + 1) -' (kk -' 1)) is ext-real V14() V15() integer set
2 |^ (((ssn + 1) -' (kk -' 1)) -' 1) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
n2 * (2 |^ (((ssn + 1) -' (kk -' 1)) -' 1)) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
m2 mod (n2 * (2 |^ (((ssn + 1) -' (kk -' 1)) -' 1))) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
2 |^ ((ssn + 1) -' kk) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
n2 * (2 |^ ((ssn + 1) -' kk)) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
m2 mod (n2 * (2 |^ ((ssn + 1) -' kk))) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
(ssn -' kk) + 1 is ext-real positive non negative V4() V7() V8() V9() V13() V14() V15() integer Element of NAT
2 |^ ((ssn -' kk) + 1) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
n2 * (2 |^ ((ssn -' kk) + 1)) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
(2 |^ (ssn -' kk)) * 2 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
n2 * ((2 |^ (ssn -' kk)) * 2) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
2 * (n2 * (2 |^ (ssn -' kk))) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
(k5 . ((ssn + 1) -' (kk -' 1))) - (ssm . ((ssn + 1) -' kk)) is ext-real V14() V15() integer set
m2 mod (n2 * (2 |^ (ssn -' kk))) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
ppn . ((ssn + 1) -' kk) is ext-real V14() V15() integer set
m2 div (n2 * (2 |^ (((ssn + 1) -' kk) -' 1))) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
m2 div (n2 * (2 |^ (((ssn + 1) -' (kk -' 1)) -' 1))) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
(m2 div (n2 * (2 |^ (((ssn + 1) -' (kk -' 1)) -' 1)))) * 2 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
((m2 div (n2 * (2 |^ (((ssn + 1) -' (kk -' 1)) -' 1)))) * 2) + 1 is ext-real positive non negative V4() V7() V8() V9() V13() V14() V15() integer Element of NAT
ppn . ((ssn + 1) -' (kk -' 1)) is ext-real V14() V15() integer set
(ppn . ((ssn + 1) -' (kk -' 1))) * 2 is ext-real V14() V15() integer set
((ppn . ((ssn + 1) -' (kk -' 1))) * 2) + 1 is ext-real V14() V15() integer set
k + 1 is ext-real V14() V15() integer set
kk + 1 is ext-real positive non negative V4() V7() V8() V9() V13() V14() V15() integer Element of NAT
kk -' 1 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
(ssn + 1) - (kk -' 1) is ext-real V14() V15() integer set
(ssn + 1) -' kk is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
m2 + k is ext-real V14() V15() integer set
(m2 + k) - k is ext-real V14() V15() integer set
((ssn + 1) -' kk) + 1 is ext-real positive non negative V4() V7() V8() V9() V13() V14() V15() integer Element of NAT
((ssn + 1) -' kk) - 1 is ext-real V14() V15() integer set
((ssn + 1) -' kk) -' 1 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
k5 . ((ssn + 1) -' kk) is ext-real V14() V15() integer set
2 |^ (((ssn + 1) -' kk) -' 1) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
n2 * (2 |^ (((ssn + 1) -' kk) -' 1)) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
m2 mod (n2 * (2 |^ (((ssn + 1) -' kk) -' 1))) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
2 |^ (ssn -' kk) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
n2 * (2 |^ (ssn -' kk)) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
m2 mod (n2 * (2 |^ (ssn -' kk))) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
(ssn - k) + 1 is ext-real V14() V15() integer set
ssm . ((ssn + 1) -' kk) is ext-real V14() V15() integer set
(ssn + 1) -' (kk -' 1) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
((ssn + 1) - k) + 1 is ext-real V14() V15() integer set
((ssn + 1) -' (kk -' 1)) -' 1 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
k5 . ((ssn + 1) -' (kk -' 1)) is ext-real V14() V15() integer set
2 |^ (((ssn + 1) -' (kk -' 1)) -' 1) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
n2 * (2 |^ (((ssn + 1) -' (kk -' 1)) -' 1)) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
m2 mod (n2 * (2 |^ (((ssn + 1) -' (kk -' 1)) -' 1))) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
2 |^ ((ssn + 1) -' kk) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
n2 * (2 |^ ((ssn + 1) -' kk)) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
m2 mod (n2 * (2 |^ ((ssn + 1) -' kk))) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
(ssn -' kk) + 1 is ext-real positive non negative V4() V7() V8() V9() V13() V14() V15() integer Element of NAT
2 |^ ((ssn -' kk) + 1) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
n2 * (2 |^ ((ssn -' kk) + 1)) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
(2 |^ (ssn -' kk)) * 2 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
n2 * ((2 |^ (ssn -' kk)) * 2) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
2 * (n2 * (2 |^ (ssn -' kk))) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
ppn . ((ssn + 1) -' kk) is ext-real V14() V15() integer set
m2 div (n2 * (2 |^ (((ssn + 1) -' kk) -' 1))) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
m2 div (n2 * (2 |^ (((ssn + 1) -' (kk -' 1)) -' 1))) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
(m2 div (n2 * (2 |^ (((ssn + 1) -' (kk -' 1)) -' 1)))) * 2 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
ppn . ((ssn + 1) -' (kk -' 1)) is ext-real V14() V15() integer set
(ppn . ((ssn + 1) -' (kk -' 1))) * 2 is ext-real V14() V15() integer set
k is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
k + 1 is ext-real positive non negative V4() V7() V8() V9() V13() V14() V15() integer Element of NAT
ssm . (k + 1) is ext-real V14() V15() integer set
ssm . k is ext-real V14() V15() integer set
(ssm . k) * 2 is ext-real V14() V15() integer set
k -' 1 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
2 |^ (k -' 1) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
m * (2 |^ (k -' 1)) is ext-real V14() V15() integer set
(k + 1) -' 1 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
2 |^ ((k + 1) -' 1) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
m * (2 |^ ((k + 1) -' 1)) is ext-real V14() V15() integer set
k - 1 is ext-real V14() V15() integer set
(k - 1) + 1 is ext-real V14() V15() integer set
(k -' 1) + 1 is ext-real positive non negative V4() V7() V8() V9() V13() V14() V15() integer Element of NAT
(2 |^ (k -' 1)) * 2 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
k is ext-real V14() V15() integer set
k + 1 is ext-real V14() V15() integer set
ssm . (k + 1) is ext-real V14() V15() integer set
ssm . k is ext-real V14() V15() integer set
(ssm . k) * 2 is ext-real V14() V15() integer set
kk is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
kk + 1 is ext-real positive non negative V4() V7() V8() V9() V13() V14() V15() integer Element of NAT
ssm . (kk + 1) is ext-real V14() V15() integer set
ssm . kk is ext-real V14() V15() integer set
(ssm . kk) * 2 is ext-real V14() V15() integer set
ssm . (ssn + 1) is ext-real V14() V15() integer set
m * (2 |^ ((ssn + 1) -' 1)) is ext-real V14() V15() integer set
m * (2 |^ (ssn -' 1)) is ext-real V14() V15() integer set
(m * (2 |^ (ssn -' 1))) * 2 is ext-real V14() V15() integer set
ssm . ssn is ext-real V14() V15() integer set
(ssm . ssn) * 2 is ext-real V14() V15() integer set
m2 is ext-real V14() V15() integer set
n2 is ext-real V14() V15() integer set
ppn is V16() V19( NAT ) V20( INT ) Function-like FinSequence-like FinSequence of INT
len ppn is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
ppn is V16() V19( NAT ) V20( INT ) Function-like FinSequence-like FinSequence of INT
len ppn is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
ii0 is V16() V19( NAT ) V20( INT ) Function-like FinSequence-like FinSequence of INT
len ii0 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
ppn . 1 is ext-real V14() V15() integer set
i0 is ext-real V14() V15() integer set
i0 + 1 is ext-real V14() V15() integer set
ppn . (i0 + 1) is ext-real V14() V15() integer set
ppn . i0 is ext-real V14() V15() integer set
(ppn . i0) * 2 is ext-real V14() V15() integer set
ii0 . (i0 + 1) is ext-real V14() V15() integer set
ppn . (i0 + 1) is ext-real V14() V15() integer set
ii0 . 1 is ext-real V14() V15() integer set
ppn is V16() V19( NAT ) V20( INT ) Function-like FinSequence-like FinSequence of INT
len ppn is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
ppn is V16() V19( NAT ) V20( INT ) Function-like FinSequence-like FinSequence of INT
len ppn is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
ii0 is V16() V19( NAT ) V20( INT ) Function-like FinSequence-like FinSequence of INT
len ii0 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
ppn . 1 is ext-real V14() V15() integer set
ii0 . 1 is ext-real V14() V15() integer set
i0 is V16() V19( NAT ) V20( INT ) Function-like FinSequence-like FinSequence of INT
len i0 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
k5 is V16() V19( NAT ) V20( INT ) Function-like FinSequence-like FinSequence of INT
len k5 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
ssn is V16() V19( NAT ) V20( INT ) Function-like FinSequence-like FinSequence of INT
len ssn is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
i0 . 1 is ext-real V14() V15() integer set
ssn is ext-real V14() V15() integer set
ssn + 1 is ext-real V14() V15() integer set
i0 . (ssn + 1) is ext-real V14() V15() integer set
i0 . ssn is ext-real V14() V15() integer set
(i0 . ssn) * 2 is ext-real V14() V15() integer set
ssn . (ssn + 1) is ext-real V14() V15() integer set
k5 . (ssn + 1) is ext-real V14() V15() integer set
ssn . 1 is ext-real V14() V15() integer set
i0 is V16() V19( NAT ) V20( INT ) Function-like FinSequence-like FinSequence of INT
len i0 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
k5 is V16() V19( NAT ) V20( INT ) Function-like FinSequence-like FinSequence of INT
len k5 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
ssn is V16() V19( NAT ) V20( INT ) Function-like FinSequence-like FinSequence of INT
len ssn is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
i0 . 1 is ext-real V14() V15() integer set
ssn . 1 is ext-real V14() V15() integer set
ssn is ext-real V14() V15() integer set
ssn + 1 is ext-real V14() V15() integer set
ppn . (ssn + 1) is ext-real V14() V15() integer set
ppn . ssn is ext-real V14() V15() integer set
(ppn . ssn) * 2 is ext-real V14() V15() integer set
ii0 . (ssn + 1) is ext-real V14() V15() integer set
ppn . (ssn + 1) is ext-real V14() V15() integer set
ssn is ext-real V14() V15() integer set
ssn + 1 is ext-real V14() V15() integer set
ppn . (ssn + 1) is ext-real V14() V15() integer set
ppn . ssn is ext-real V14() V15() integer set
(ppn . ssn) * 2 is ext-real V14() V15() integer set
ii0 . (ssn + 1) is ext-real V14() V15() integer set
ppn . (ssn + 1) is ext-real V14() V15() integer set
ssm is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
ssm + 1 is ext-real positive non negative V4() V7() V8() V9() V13() V14() V15() integer Element of NAT
(ssm + 1) + 1 is ext-real positive non negative V4() V7() V8() V9() V13() V14() V15() integer Element of NAT
ssm is ext-real V14() V15() integer set
ssm + 1 is ext-real V14() V15() integer set
i0 . (ssm + 1) is ext-real V14() V15() integer set
i0 . ssm is ext-real V14() V15() integer set
(i0 . ssm) * 2 is ext-real V14() V15() integer set
ssn . (ssm + 1) is ext-real V14() V15() integer set
k5 . (ssm + 1) is ext-real V14() V15() integer set
ssm is ext-real V14() V15() integer set
ssm + 1 is ext-real V14() V15() integer set
i0 . (ssm + 1) is ext-real V14() V15() integer set
i0 . ssm is ext-real V14() V15() integer set
(i0 . ssm) * 2 is ext-real V14() V15() integer set
ssn . (ssm + 1) is ext-real V14() V15() integer set
k5 . (ssm + 1) is ext-real V14() V15() integer set
kk is ext-real V14() V15() integer set
i0 . kk is ext-real V14() V15() integer set
ppn . kk is ext-real V14() V15() integer set
kk - 1 is ext-real V14() V15() integer set
j2 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
j2 -' 1 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
(j2 -' 1) + 1 is ext-real positive non negative V4() V7() V8() V9() V13() V14() V15() integer Element of NAT
e is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
e + 1 is ext-real positive non negative V4() V7() V8() V9() V13() V14() V15() integer Element of NAT
i0 . (e + 1) is ext-real V14() V15() integer set
ppn . (e + 1) is ext-real V14() V15() integer set
(e + 1) + 1 is ext-real positive non negative V4() V7() V8() V9() V13() V14() V15() integer Element of NAT
i0 . ((e + 1) + 1) is ext-real V14() V15() integer set
ppn . ((e + 1) + 1) is ext-real V14() V15() integer set
k is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
k + 1 is ext-real positive non negative V4() V7() V8() V9() V13() V14() V15() integer Element of NAT
((e + 1) + 1) - 1 is ext-real V14() V15() integer set
(ssm + 1) - 1 is ext-real V14() V15() integer set
0 + 1 is ext-real positive non negative V4() V7() V8() V9() V13() V14() V15() integer Element of NAT
(i0 . (e + 1)) * 2 is ext-real V14() V15() integer set
(i0 . (e + 1)) * 2 is ext-real V14() V15() integer set
(i0 . (e + 1)) * 2 is ext-real V14() V15() integer set
(i0 . (e + 1)) * 2 is ext-real V14() V15() integer set
0 + 1 is ext-real positive non negative V4() V7() V8() V9() V13() V14() V15() integer Element of NAT
i0 . (0 + 1) is ext-real V14() V15() integer set
ppn . (0 + 1) is ext-real V14() V15() integer set
e is ext-real V14() V15() integer set
e + 1 is ext-real V14() V15() integer set
ppn . (e + 1) is ext-real V14() V15() integer set
ppn . e is ext-real V14() V15() integer set
(ppn . e) * 2 is ext-real V14() V15() integer set
ii0 . (e + 1) is ext-real V14() V15() integer set
ppn . (e + 1) is ext-real V14() V15() integer set
c₁₈ is ext-real V14() V15() integer set
c₁₈ + 1 is ext-real V14() V15() integer set
i0 . (c₁₈ + 1) is ext-real V14() V15() integer set
i0 . c₁₈ is ext-real V14() V15() integer set
(i0 . c₁₈) * 2 is ext-real V14() V15() integer set
ssn . (c₁₈ + 1) is ext-real V14() V15() integer set
k5 . (c₁₈ + 1) is ext-real V14() V15() integer set
k is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
k + 1 is ext-real positive non negative V4() V7() V8() V9() V13() V14() V15() integer Element of NAT
(ssm + 1) - 1 is ext-real V14() V15() integer set
k is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
0 + 1 is ext-real positive non negative V4() V7() V8() V9() V13() V14() V15() integer Element of NAT
ppn . (ssm + 1) is ext-real V14() V15() integer set
kk is ext-real V14() V15() integer set
ppn . kk is ext-real V14() V15() integer set
i0 . kk is ext-real V14() V15() integer set
kk - 1 is ext-real V14() V15() integer set
j2 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
j2 -' 1 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
(j2 -' 1) + 1 is ext-real positive non negative V4() V7() V8() V9() V13() V14() V15() integer Element of NAT
e is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
e + 1 is ext-real positive non negative V4() V7() V8() V9() V13() V14() V15() integer Element of NAT
ppn . (e + 1) is ext-real V14() V15() integer set
i0 . (e + 1) is ext-real V14() V15() integer set
(e + 1) + 1 is ext-real positive non negative V4() V7() V8() V9() V13() V14() V15() integer Element of NAT
ppn . ((e + 1) + 1) is ext-real V14() V15() integer set
i0 . ((e + 1) + 1) is ext-real V14() V15() integer set
((e + 1) + 1) - 1 is ext-real V14() V15() integer set
(ssn + 1) - 1 is ext-real V14() V15() integer set
(ppn . (e + 1)) * 2 is ext-real V14() V15() integer set
(ppn . (e + 1)) * 2 is ext-real V14() V15() integer set
(ppn . (e + 1)) * 2 is ext-real V14() V15() integer set
(ppn . (e + 1)) * 2 is ext-real V14() V15() integer set
ppn . (0 + 1) is ext-real V14() V15() integer set
i0 . (0 + 1) is ext-real V14() V15() integer set
e is ext-real V14() V15() integer set
e + 1 is ext-real V14() V15() integer set
ppn . (e + 1) is ext-real V14() V15() integer set
ppn . e is ext-real V14() V15() integer set
(ppn . e) * 2 is ext-real V14() V15() integer set
ii0 . (e + 1) is ext-real V14() V15() integer set
ppn . (e + 1) is ext-real V14() V15() integer set
c₁₈ is ext-real V14() V15() integer set
c₁₈ + 1 is ext-real V14() V15() integer set
i0 . (c₁₈ + 1) is ext-real V14() V15() integer set
i0 . c₁₈ is ext-real V14() V15() integer set
(i0 . c₁₈) * 2 is ext-real V14() V15() integer set
ssn . (c₁₈ + 1) is ext-real V14() V15() integer set
k5 . (c₁₈ + 1) is ext-real V14() V15() integer set
(ssn + 1) - 1 is ext-real V14() V15() integer set
i0 . (ssn + 1) is ext-real V14() V15() integer set
kk is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
ppn . kk is ext-real V14() V15() integer set
i0 . kk is ext-real V14() V15() integer set
kk + 1 is ext-real positive non negative V4() V7() V8() V9() V13() V14() V15() integer Element of NAT
ppn . (kk + 1) is ext-real V14() V15() integer set
i0 . (kk + 1) is ext-real V14() V15() integer set
(kk + 1) - 1 is ext-real V14() V15() integer set
(ssm + 1) - 1 is ext-real V14() V15() integer set
(i0 . kk) * 2 is ext-real V14() V15() integer set
(i0 . kk) * 2 is ext-real V14() V15() integer set
(i0 . kk) * 2 is ext-real V14() V15() integer set
(i0 . kk) * 2 is ext-real V14() V15() integer set
j2 is ext-real V14() V15() integer set
j2 + 1 is ext-real V14() V15() integer set
ppn . (j2 + 1) is ext-real V14() V15() integer set
ppn . j2 is ext-real V14() V15() integer set
(ppn . j2) * 2 is ext-real V14() V15() integer set
ii0 . (j2 + 1) is ext-real V14() V15() integer set
ppn . (j2 + 1) is ext-real V14() V15() integer set
e is ext-real V14() V15() integer set
e + 1 is ext-real V14() V15() integer set
i0 . (e + 1) is ext-real V14() V15() integer set
i0 . e is ext-real V14() V15() integer set
(i0 . e) * 2 is ext-real V14() V15() integer set
ssn . (e + 1) is ext-real V14() V15() integer set
k5 . (e + 1) is ext-real V14() V15() integer set
ppn . 0 is ext-real V14() V15() integer set
i0 . 0 is ext-real V14() V15() integer set
kk is ext-real V14() V15() integer set
ppn . kk is ext-real V14() V15() integer set
i0 . kk is ext-real V14() V15() integer set
j2 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
ppn . j2 is ext-real V14() V15() integer set
i0 . j2 is ext-real V14() V15() integer set
kk is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
((ssm + 1) + 1) -' kk is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
ppn . (((ssm + 1) + 1) -' kk) is ext-real V14() V15() integer set
k5 . (((ssm + 1) + 1) -' kk) is ext-real V14() V15() integer set
kk + 1 is ext-real positive non negative V4() V7() V8() V9() V13() V14() V15() integer Element of NAT
((ssm + 1) + 1) -' (kk + 1) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
ppn . (((ssm + 1) + 1) -' (kk + 1)) is ext-real V14() V15() integer set
k5 . (((ssm + 1) + 1) -' (kk + 1)) is ext-real V14() V15() integer set
(kk + 1) - 1 is ext-real V14() V15() integer set
(ssm + 1) - 1 is ext-real V14() V15() integer set
(ssn + 1) - kk is ext-real V14() V15() integer set
(ssm + 1) -' kk is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
kk - 1 is ext-real V14() V15() integer set
kk -' 1 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
(ssn + 1) - (kk -' 1) is ext-real V14() V15() integer set
(ssm + 1) -' (kk -' 1) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
(ssn + 1) - (kk - 1) is ext-real V14() V15() integer set
i0 . ((ssm + 1) -' kk) is ext-real V14() V15() integer set
k5 . ((ssm + 1) -' (kk -' 1)) is ext-real V14() V15() integer set
k5 . ((ssm + 1) -' kk) is ext-real V14() V15() integer set
ssn . ((ssm + 1) -' kk) is ext-real V14() V15() integer set
ssn . ((ssm + 1) -' (kk -' 1)) is ext-real V14() V15() integer set
(ssn . ((ssm + 1) -' (kk -' 1))) * 2 is ext-real V14() V15() integer set
(kk -' 1) + 1 is ext-real positive non negative V4() V7() V8() V9() V13() V14() V15() integer Element of NAT
(k5 . ((ssm + 1) -' (kk -' 1))) - (i0 . ((ssm + 1) -' kk)) is ext-real V14() V15() integer set
((ssn . ((ssm + 1) -' (kk -' 1))) * 2) + 1 is ext-real V14() V15() integer set
ppn . ((ssm + 1) -' kk) is ext-real V14() V15() integer set
ppn . ((ssm + 1) -' (kk -' 1)) is ext-real V14() V15() integer set
ppn . ((ssm + 1) -' kk) is ext-real V14() V15() integer set
ii0 . ((ssm + 1) -' kk) is ext-real V14() V15() integer set
ii0 . ((ssm + 1) -' (kk -' 1)) is ext-real V14() V15() integer set
(ii0 . ((ssm + 1) -' (kk -' 1))) * 2 is ext-real V14() V15() integer set
(ppn . ((ssm + 1) -' (kk -' 1))) - (ppn . ((ssm + 1) -' kk)) is ext-real V14() V15() integer set
((ii0 . ((ssm + 1) -' (kk -' 1))) * 2) + 1 is ext-real V14() V15() integer set
(ssm + 1) -' kk is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
((ssm + 1) + 1) -' 0 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
ppn . (((ssm + 1) + 1) -' 0) is ext-real V14() V15() integer set
k5 . (((ssm + 1) + 1) -' 0) is ext-real V14() V15() integer set
kk is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
((ssm + 1) + 1) -' kk is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
ii0 . (((ssm + 1) + 1) -' kk) is ext-real V14() V15() integer set
ssn . (((ssm + 1) + 1) -' kk) is ext-real V14() V15() integer set
kk + 1 is ext-real positive non negative V4() V7() V8() V9() V13() V14() V15() integer Element of NAT
((ssm + 1) + 1) -' (kk + 1) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
ii0 . (((ssm + 1) + 1) -' (kk + 1)) is ext-real V14() V15() integer set
ssn . (((ssm + 1) + 1) -' (kk + 1)) is ext-real V14() V15() integer set
(kk + 1) - 1 is ext-real V14() V15() integer set
(ssm + 1) - 1 is ext-real V14() V15() integer set
kk -' 1 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
(kk -' 1) + 1 is ext-real positive non negative V4() V7() V8() V9() V13() V14() V15() integer Element of NAT
(ssn + 1) - kk is ext-real V14() V15() integer set
(ssm + 1) -' kk is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
kk - 1 is ext-real V14() V15() integer set
(ssn + 1) - (kk -' 1) is ext-real V14() V15() integer set
(ssm + 1) -' (kk -' 1) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
(ssn + 1) - (kk - 1) is ext-real V14() V15() integer set
ppn . ((ssm + 1) -' kk) is ext-real V14() V15() integer set
i0 . ((ssm + 1) -' kk) is ext-real V14() V15() integer set
ppn . ((ssm + 1) -' (kk -' 1)) is ext-real V14() V15() integer set
ppn . ((ssm + 1) -' kk) is ext-real V14() V15() integer set
ii0 . ((ssm + 1) -' kk) is ext-real V14() V15() integer set
ii0 . ((ssm + 1) -' (kk -' 1)) is ext-real V14() V15() integer set
(ii0 . ((ssm + 1) -' (kk -' 1))) * 2 is ext-real V14() V15() integer set
k5 . ((ssm + 1) -' (kk -' 1)) is ext-real V14() V15() integer set
k5 . ((ssm + 1) -' kk) is ext-real V14() V15() integer set
ssn . ((ssm + 1) -' kk) is ext-real V14() V15() integer set
ssn . ((ssm + 1) -' (kk -' 1)) is ext-real V14() V15() integer set
(ssn . ((ssm + 1) -' (kk -' 1))) * 2 is ext-real V14() V15() integer set
(k5 . ((ssm + 1) -' (kk -' 1))) - (i0 . ((ssm + 1) -' kk)) is ext-real V14() V15() integer set
((ssn . ((ssm + 1) -' (kk -' 1))) * 2) + 1 is ext-real V14() V15() integer set
(ppn . ((ssm + 1) -' (kk -' 1))) - (ppn . ((ssm + 1) -' kk)) is ext-real V14() V15() integer set
((ii0 . ((ssm + 1) -' (kk -' 1))) * 2) + 1 is ext-real V14() V15() integer set
(ssm + 1) -' kk is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
ii0 . (((ssm + 1) + 1) -' 0) is ext-real V14() V15() integer set
ssn . (((ssm + 1) + 1) -' 0) is ext-real V14() V15() integer set
(ssn + 1) + 1 is ext-real V14() V15() integer set
kk is ext-real V14() V15() integer set
((ssn + 1) + 1) - kk is ext-real V14() V15() integer set
ii0 . (((ssn + 1) + 1) - kk) is ext-real V14() V15() integer set
ssn . (((ssn + 1) + 1) - kk) is ext-real V14() V15() integer set
j2 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
((ssm + 1) + 1) - j2 is ext-real V14() V15() integer set
((ssm + 1) + 1) -' j2 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
((ssm + 1) + 1) - kk is ext-real V14() V15() integer set
1 + ssm is ext-real positive non negative V4() V7() V8() V9() V13() V14() V15() integer Element of NAT
((ssn + 1) + 1) - (ssn + 1) is ext-real V14() V15() integer set
n is ext-real V14() V15() integer set
n + 1 is ext-real V14() V15() integer set
m is ext-real V14() V15() integer set
(n,m) is ext-real V14() V15() integer set
n2 is V16() V19( NAT ) V20( INT ) Function-like FinSequence-like FinSequence of INT
len n2 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
ppn is V16() V19( NAT ) V20( INT ) Function-like FinSequence-like FinSequence of INT
len ppn is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
ppn is V16() V19( NAT ) V20( INT ) Function-like FinSequence-like FinSequence of INT
len ppn is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
n2 . 1 is ext-real V14() V15() integer set
ppn . 1 is ext-real V14() V15() integer set
dom n2 is Element of K11(NAT)
dom ppn is Element of K11(NAT)
dom ppn is Element of K11(NAT)
ii0 is ext-real V14() V15() integer set
ii0 + 1 is ext-real V14() V15() integer set
n2 . (ii0 + 1) is ext-real V14() V15() integer set
n2 . ii0 is ext-real V14() V15() integer set
(n2 . ii0) * 2 is ext-real V14() V15() integer set
ppn . (ii0 + 1) is ext-real V14() V15() integer set
ppn . (ii0 + 1) is ext-real V14() V15() integer set
m2 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
m2 + 1 is ext-real positive non negative V4() V7() V8() V9() V13() V14() V15() integer Element of NAT
Seg (len n2) is Element of K11(NAT)
i0 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
i0 + 1 is ext-real positive non negative V4() V7() V8() V9() V13() V14() V15() integer Element of NAT
k5 is ext-real V14() V15() integer set
k5 + 1 is ext-real V14() V15() integer set
n2 . (k5 + 1) is ext-real V14() V15() integer set
n2 . k5 is ext-real V14() V15() integer set
(n2 . k5) * 2 is ext-real V14() V15() integer set
ssn is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
ssn + 1 is ext-real positive non negative V4() V7() V8() V9() V13() V14() V15() integer Element of NAT
Seg (m2 + 1) is Element of K11(NAT)
k5 is ext-real V14() V15() integer set
k5 - 1 is ext-real V14() V15() integer set
(ii0 + 1) - (k5 - 1) is ext-real V14() V15() integer set
(ii0 + 1) - k5 is ext-real V14() V15() integer set
n2 . ((ii0 + 1) - k5) is ext-real V14() V15() integer set
ppn . ((ii0 + 1) - (k5 - 1)) is ext-real V14() V15() integer set
ppn . ((ii0 + 1) - k5) is ext-real V14() V15() integer set
(ppn . ((ii0 + 1) - (k5 - 1))) - (n2 . ((ii0 + 1) - k5)) is ext-real V14() V15() integer set
ppn . ((ii0 + 1) - k5) is ext-real V14() V15() integer set
ppn . ((ii0 + 1) - (k5 - 1)) is ext-real V14() V15() integer set
(ppn . ((ii0 + 1) - (k5 - 1))) * 2 is ext-real V14() V15() integer set
((ppn . ((ii0 + 1) - (k5 - 1))) * 2) + 1 is ext-real V14() V15() integer set
(ii0 + 1) + 0 is ext-real V14() V15() integer set
(ii0 + 1) + (k5 - 1) is ext-real V14() V15() integer set
((ii0 + 1) + (k5 - 1)) - (k5 - 1) is ext-real V14() V15() integer set
ii0 - k5 is ext-real V14() V15() integer set
(ii0 - k5) + 1 is ext-real V14() V15() integer set
0 + 1 is ext-real positive non negative V4() V7() V8() V9() V13() V14() V15() integer Element of NAT
((ii0 - k5) + 1) + 1 is ext-real V14() V15() integer set
ssn is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
(ii0 + 1) + k5 is ext-real V14() V15() integer set
((ii0 + 1) + k5) - k5 is ext-real V14() V15() integer set
Seg (m2 + 1) is Element of K11(NAT)
k5 is ext-real V14() V15() integer set
k5 + 1 is ext-real V14() V15() integer set
n2 . (k5 + 1) is ext-real V14() V15() integer set
n2 . k5 is ext-real V14() V15() integer set
(n2 . k5) * 2 is ext-real V14() V15() integer set
ssn is ext-real V14() V15() integer set
ssn - 1 is ext-real V14() V15() integer set
(ii0 + 1) - (ssn - 1) is ext-real V14() V15() integer set
(ii0 + 1) - ssn is ext-real V14() V15() integer set
n2 . ((ii0 + 1) - ssn) is ext-real V14() V15() integer set
ppn . ((ii0 + 1) - (ssn - 1)) is ext-real V14() V15() integer set
ppn . ((ii0 + 1) - ssn) is ext-real V14() V15() integer set
(ppn . ((ii0 + 1) - (ssn - 1))) - (n2 . ((ii0 + 1) - ssn)) is ext-real V14() V15() integer set
ppn . ((ii0 + 1) - ssn) is ext-real V14() V15() integer set
ppn . ((ii0 + 1) - (ssn - 1)) is ext-real V14() V15() integer set
(ppn . ((ii0 + 1) - (ssn - 1))) * 2 is ext-real V14() V15() integer set
((ppn . ((ii0 + 1) - (ssn - 1))) * 2) + 1 is ext-real V14() V15() integer set
i0 is ext-real V14() V15() integer set
i0 + 1 is ext-real V14() V15() integer set
n2 . (i0 + 1) is ext-real V14() V15() integer set
n2 . i0 is ext-real V14() V15() integer set
(n2 . i0) * 2 is ext-real V14() V15() integer set
k5 is ext-real V14() V15() integer set
k5 - 1 is ext-real V14() V15() integer set
(ii0 + 1) - (k5 - 1) is ext-real V14() V15() integer set
(ii0 + 1) - k5 is ext-real V14() V15() integer set
n2 . ((ii0 + 1) - k5) is ext-real V14() V15() integer set
ppn . ((ii0 + 1) - (k5 - 1)) is ext-real V14() V15() integer set
ppn . ((ii0 + 1) - k5) is ext-real V14() V15() integer set
(ppn . ((ii0 + 1) - (k5 - 1))) - (n2 . ((ii0 + 1) - k5)) is ext-real V14() V15() integer set
ppn . ((ii0 + 1) - k5) is ext-real V14() V15() integer set
ppn . ((ii0 + 1) - (k5 - 1)) is ext-real V14() V15() integer set
(ppn . ((ii0 + 1) - (k5 - 1))) * 2 is ext-real V14() V15() integer set
((ppn . ((ii0 + 1) - (k5 - 1))) * 2) + 1 is ext-real V14() V15() integer set
m is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
n is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
(n,m) is ext-real V14() V15() integer set
n div m is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
n2 is ext-real V14() V15() integer set
m2 is ext-real V14() V15() integer set
n + 1 is ext-real positive non negative V4() V7() V8() V9() V13() V14() V15() integer Element of NAT
Seg (n + 1) is Element of K11(NAT)
(Seg (n + 1)) --> 1 is V16() V19( Seg (n + 1)) V20( NAT ) V20( INT ) Function-like V30( Seg (n + 1), NAT ) Element of K11(K12((Seg (n + 1)),NAT))
K12((Seg (n + 1)),NAT) is set
K11(K12((Seg (n + 1)),NAT)) is set
dom ((Seg (n + 1)) --> 1) is Element of K11((Seg (n + 1)))
K11((Seg (n + 1))) is set
ppn is V16() Function-like FinSequence-like set
rng ppn is set
{1} is V4() set
ii0 is set
ii0 is V16() V19( NAT ) V20( INT ) Function-like FinSequence-like FinSequence of INT
len ii0 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
m2 + 1 is ext-real V14() V15() integer set
n2 is ext-real V14() V15() integer set
m2 is ext-real V14() V15() integer set
n + 1 is ext-real positive non negative V4() V7() V8() V9() V13() V14() V15() integer Element of NAT
ppn is V16() Function-like FinSequence-like set
len ppn is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
dom ppn is Element of K11(NAT)
ppn is V16() Function-like FinSequence-like set
len ppn is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
dom ppn is Element of K11(NAT)
Seg (n + 1) is Element of K11(NAT)
rng ppn is set
ppn is set
ii0 is set
ppn . ii0 is set
i0 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
ppn . i0 is set
i0 -' 1 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
2 |^ (i0 -' 1) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
m * (2 |^ (i0 -' 1)) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
n div (m * (2 |^ (i0 -' 1))) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
ii0 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
2 |^ ii0 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
m * (2 |^ ii0) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
0 + 1 is ext-real positive non negative V4() V7() V8() V9() V13() V14() V15() integer Element of NAT
i0 is ext-real V14() V15() integer set
i0 + 1 is ext-real V14() V15() integer set
1 + 0 is ext-real positive non negative V4() V7() V8() V9() V13() V14() V15() integer Element of NAT
2 |^ n is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
1 * (2 |^ n) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
m * (2 |^ n) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
n2 * (2 |^ n) is ext-real V14() V15() integer set
1 + ii0 is ext-real positive non negative V4() V7() V8() V9() V13() V14() V15() integer Element of NAT
ii0 + 1 is ext-real positive non negative V4() V7() V8() V9() V13() V14() V15() integer Element of NAT
(ii0 + 1) -' 1 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
2 |^ ((ii0 + 1) -' 1) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
m * (2 |^ ((ii0 + 1) -' 1)) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
n div (m * (2 |^ ((ii0 + 1) -' 1))) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
ppn is V16() V19( NAT ) V20( INT ) Function-like FinSequence-like FinSequence of INT
ppn . (i0 + 1) is ext-real V14() V15() integer set
ppn . 1 is ext-real V14() V15() integer set
1 -' 1 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
2 |^ (1 -' 1) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
m * (2 |^ (1 -' 1)) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
n div (m * (2 |^ (1 -' 1))) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
2 |^ 0 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
m * (2 |^ 0) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
n div (m * (2 |^ 0)) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
m * 1 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
n div (m * 1) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
i0 - 1 is ext-real V14() V15() integer set
k5 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
(i0 - 1) + 1 is ext-real V14() V15() integer set
ii0 -' 1 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
(ii0 -' 1) + 1 is ext-real positive non negative V4() V7() V8() V9() V13() V14() V15() integer Element of NAT
2 |^ (ii0 -' 1) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
(2 |^ (ii0 -' 1)) * 2 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
ssn is V16() Function-like FinSequence-like set
len ssn is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
dom ssn is Element of K11(NAT)
ssn is V16() Function-like FinSequence-like set
len ssn is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
dom ssn is Element of K11(NAT)
rng ssn is set
ssn is set
ssm is set
ssn . ssm is set
ssm is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
ssn . ssm is set
ssm -' 1 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
2 |^ (ssm -' 1) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
m * (2 |^ (ssm -' 1)) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
n mod (m * (2 |^ (ssm -' 1))) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
ssm is V16() Function-like FinSequence-like set
len ssm is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
dom ssm is Element of K11(NAT)
ssm is V16() Function-like FinSequence-like set
len ssm is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
dom ssm is Element of K11(NAT)
rng ssm is set
ssm is set
k is set
ssm . k is set
kk is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
ssm . kk is set
kk -' 1 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
2 |^ (kk -' 1) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
n2 * (2 |^ (kk -' 1)) is ext-real V14() V15() integer set
ssm is V16() V19( NAT ) V20( INT ) Function-like FinSequence-like FinSequence of INT
ssm . 1 is ext-real V14() V15() integer set
n2 * (2 |^ (1 -' 1)) is ext-real V14() V15() integer set
n2 * (2 |^ 0) is ext-real V14() V15() integer set
n2 * 1 is ext-real V14() V15() integer set
ssn is V16() V19( NAT ) V20( INT ) Function-like FinSequence-like FinSequence of INT
k is ext-real V14() V15() integer set
(i0 + 1) - k is ext-real V14() V15() integer set
ssm . ((i0 + 1) - k) is ext-real V14() V15() integer set
k - 1 is ext-real V14() V15() integer set
(i0 + 1) - (k - 1) is ext-real V14() V15() integer set
ssn . ((i0 + 1) - (k - 1)) is ext-real V14() V15() integer set
ssn . ((i0 + 1) - k) is ext-real V14() V15() integer set
(ssn . ((i0 + 1) - (k - 1))) - (ssm . ((i0 + 1) - k)) is ext-real V14() V15() integer set
ppn . ((i0 + 1) - k) is ext-real V14() V15() integer set
ppn . ((i0 + 1) - (k - 1)) is ext-real V14() V15() integer set
(ppn . ((i0 + 1) - (k - 1))) * 2 is ext-real V14() V15() integer set
((ppn . ((i0 + 1) - (k - 1))) * 2) + 1 is ext-real V14() V15() integer set
i0 - k is ext-real V14() V15() integer set
kk is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
ii0 -' kk is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
(ii0 + 1) -' kk is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
n + k is ext-real V14() V15() integer set
(n + k) - k is ext-real V14() V15() integer set
((ii0 + 1) -' kk) + 1 is ext-real positive non negative V4() V7() V8() V9() V13() V14() V15() integer Element of NAT
k + 1 is ext-real V14() V15() integer set
kk + 1 is ext-real positive non negative V4() V7() V8() V9() V13() V14() V15() integer Element of NAT
kk -' 1 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
(ii0 + 1) - (kk -' 1) is ext-real V14() V15() integer set
2 |^ (ii0 -' kk) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
m * (2 |^ (ii0 -' kk)) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
m * 0 is ext-real non positive non negative V4() V7() V8() V9() V11() V12() V13() V14() V15() integer Element of NAT
((ii0 + 1) -' kk) - 1 is ext-real V14() V15() integer set
((ii0 + 1) -' kk) -' 1 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
(ii0 + 1) -' (kk -' 1) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
((i0 + 1) - k) + 1 is ext-real V14() V15() integer set
((ii0 + 1) -' (kk -' 1)) -' 1 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
2 |^ ((ii0 + 1) -' kk) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
m * (2 |^ ((ii0 + 1) -' kk)) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
(ii0 -' kk) + 1 is ext-real positive non negative V4() V7() V8() V9() V13() V14() V15() integer Element of NAT
2 |^ ((ii0 -' kk) + 1) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
m * (2 |^ ((ii0 -' kk) + 1)) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
(2 |^ (ii0 -' kk)) * 2 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
m * ((2 |^ (ii0 -' kk)) * 2) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
2 * (m * (2 |^ (ii0 -' kk))) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
ssn . ((ii0 + 1) -' kk) is ext-real V14() V15() integer set
2 |^ (((ii0 + 1) -' kk) -' 1) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
m * (2 |^ (((ii0 + 1) -' kk) -' 1)) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
n mod (m * (2 |^ (((ii0 + 1) -' kk) -' 1))) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
(i0 - k) + 1 is ext-real V14() V15() integer set
ssm . ((ii0 + 1) -' kk) is ext-real V14() V15() integer set
ssn . ((ii0 + 1) -' (kk -' 1)) is ext-real V14() V15() integer set
(((ii0 + 1) -' kk) + 1) -' 1 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
2 |^ ((((ii0 + 1) -' kk) + 1) -' 1) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
m * (2 |^ ((((ii0 + 1) -' kk) + 1) -' 1)) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
n mod (m * (2 |^ ((((ii0 + 1) -' kk) + 1) -' 1))) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
n mod (m * (2 |^ ((ii0 + 1) -' kk))) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
(ssn . ((ii0 + 1) -' (kk -' 1))) - (ssm . ((ii0 + 1) -' kk)) is ext-real V14() V15() integer set
n mod (m * (2 |^ (ii0 -' kk))) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
ppn . ((ii0 + 1) -' kk) is ext-real V14() V15() integer set
n div (m * (2 |^ (((ii0 + 1) -' kk) -' 1))) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
2 |^ (((ii0 + 1) -' (kk -' 1)) -' 1) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
m * (2 |^ (((ii0 + 1) -' (kk -' 1)) -' 1)) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
n div (m * (2 |^ (((ii0 + 1) -' (kk -' 1)) -' 1))) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
(n div (m * (2 |^ (((ii0 + 1) -' (kk -' 1)) -' 1)))) * 2 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
((n div (m * (2 |^ (((ii0 + 1) -' (kk -' 1)) -' 1)))) * 2) + 1 is ext-real positive non negative V4() V7() V8() V9() V13() V14() V15() integer Element of NAT
ppn . ((ii0 + 1) -' (kk -' 1)) is ext-real V14() V15() integer set
(ppn . ((ii0 + 1) -' (kk -' 1))) * 2 is ext-real V14() V15() integer set
((ppn . ((ii0 + 1) -' (kk -' 1))) * 2) + 1 is ext-real V14() V15() integer set
(i0 + 1) - (kk -' 1) is ext-real V14() V15() integer set
((i0 - k) + 1) - 1 is ext-real V14() V15() integer set
ssn . (i0 + 1) is ext-real V14() V15() integer set
n mod (m * (2 |^ ((ii0 + 1) -' 1))) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
k is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
k + 1 is ext-real positive non negative V4() V7() V8() V9() V13() V14() V15() integer Element of NAT
ssm . (k + 1) is ext-real V14() V15() integer set
ssm . k is ext-real V14() V15() integer set
(ssm . k) * 2 is ext-real V14() V15() integer set
k -' 1 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
2 |^ (k -' 1) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
n2 * (2 |^ (k -' 1)) is ext-real V14() V15() integer set
(k + 1) -' 1 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
2 |^ ((k + 1) -' 1) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
n2 * (2 |^ ((k + 1) -' 1)) is ext-real V14() V15() integer set
k - 1 is ext-real V14() V15() integer set
(k - 1) + 1 is ext-real V14() V15() integer set
(k -' 1) + 1 is ext-real positive non negative V4() V7() V8() V9() V13() V14() V15() integer Element of NAT
(2 |^ (k -' 1)) * 2 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
k is ext-real V14() V15() integer set
k + 1 is ext-real V14() V15() integer set
ssm . (k + 1) is ext-real V14() V15() integer set
ssm . k is ext-real V14() V15() integer set
(ssm . k) * 2 is ext-real V14() V15() integer set
kk is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
kk + 1 is ext-real positive non negative V4() V7() V8() V9() V13() V14() V15() integer Element of NAT
ssm . (kk + 1) is ext-real V14() V15() integer set
ssm . kk is ext-real V14() V15() integer set
(ssm . kk) * 2 is ext-real V14() V15() integer set
ssm . (i0 + 1) is ext-real V14() V15() integer set
n2 * (2 |^ ((ii0 + 1) -' 1)) is ext-real V14() V15() integer set
n2 * (2 |^ (ii0 -' 1)) is ext-real V14() V15() integer set
(n2 * (2 |^ (ii0 -' 1))) * 2 is ext-real V14() V15() integer set
ssm . i0 is ext-real V14() V15() integer set
(ssm . i0) * 2 is ext-real V14() V15() integer set
m2 + 1 is ext-real V14() V15() integer set
n2 is ext-real V14() V15() integer set
m2 is ext-real V14() V15() integer set
m2 + 1 is ext-real V14() V15() integer set
m2 is ext-real V14() V15() integer set
m2 + 1 is ext-real V14() V15() integer set
n2 is ext-real V14() V15() integer set
ppn is V16() V19( NAT ) V20( INT ) Function-like FinSequence-like FinSequence of INT
len ppn is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
ppn is V16() V19( NAT ) V20( INT ) Function-like FinSequence-like FinSequence of INT
len ppn is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
ii0 is V16() V19( NAT ) V20( INT ) Function-like FinSequence-like FinSequence of INT
len ii0 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
ppn . 1 is ext-real V14() V15() integer set
i0 is ext-real V14() V15() integer set
i0 + 1 is ext-real V14() V15() integer set
ppn . (i0 + 1) is ext-real V14() V15() integer set
ppn . i0 is ext-real V14() V15() integer set
(ppn . i0) * 2 is ext-real V14() V15() integer set
ii0 . (i0 + 1) is ext-real V14() V15() integer set
ppn . (i0 + 1) is ext-real V14() V15() integer set
ii0 . 1 is ext-real V14() V15() integer set
n is ext-real V14() V15() integer set
m is ext-real V14() V15() integer set
(n,m) is ext-real V14() V15() integer set
n div m is ext-real V14() V15() integer set
m2 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
n2 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
m2 div n2 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
m is ext-real V14() V15() integer set
n is ext-real V14() V15() integer set
n div m is ext-real V14() V15() integer set
- m is ext-real V14() V15() integer set
- n is ext-real V14() V15() integer set
m2 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
n2 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
m2 div n2 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
n2 * (m2 div n2) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
- (m2 div n2) is ext-real non positive V14() V15() integer set
(- (m2 div n2)) - 1 is ext-real non positive negative V4() V14() V15() integer set
m2 mod n2 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
(n2 * (m2 div n2)) + (m2 mod n2) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
n / m is ext-real V14() V15() set
[\(n / m)/] is ext-real V14() V15() integer set
(- n) / (- m) is ext-real V14() V15() set
[\((- n) / (- m))/] is ext-real V14() V15() integer set
- m2 is ext-real non positive V14() V15() integer set
(- m2) div n2 is ext-real V14() V15() integer set
m2 mod n2 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
(n2 * (m2 div n2)) + (m2 mod n2) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
- m2 is ext-real non positive V14() V15() integer set
(- m2) div n2 is ext-real V14() V15() integer set
((- m2) div n2) + 1 is ext-real V14() V15() integer set
n / m is ext-real V14() V15() set
[\(n / m)/] is ext-real V14() V15() integer set
(- n) / (- m) is ext-real V14() V15() set
[\((- n) / (- m))/] is ext-real V14() V15() integer set
m2 mod n2 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
(n2 * (m2 div n2)) + (m2 mod n2) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
- m2 is ext-real non positive V14() V15() integer set
(- m2) div m is ext-real V14() V15() integer set
m2 mod n2 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
(n2 * (m2 div n2)) + (m2 mod n2) is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
- m2 is ext-real non positive V14() V15() integer set
(- m2) div n2 is ext-real V14() V15() integer set
((- m2) div n2) + 1 is ext-real V14() V15() integer set
n / m is ext-real V14() V15() set
[\(n / m)/] is ext-real V14() V15() integer set
(- n) / (- m) is ext-real V14() V15() set
[\((- n) / (- m))/] is ext-real V14() V15() integer set
m is ext-real V14() V15() integer set
n is ext-real V14() V15() integer set
(n,m) is ext-real V14() V15() integer set
- m is ext-real V14() V15() integer set
(n,(- m)) is ext-real V14() V15() integer set
- n is ext-real V14() V15() integer set
((- n),m) is ext-real V14() V15() integer set
((- n),(- m)) is ext-real V14() V15() integer set
n div m is ext-real V14() V15() integer set
(- m) * (n,m) is ext-real V14() V15() integer set
- (n,m) is ext-real V14() V15() integer set
(- (n,m)) - 1 is ext-real V14() V15() integer set
m * (n,m) is ext-real V14() V15() integer set
(- m) * (n,(- m)) is ext-real V14() V15() integer set
n div (- m) is ext-real V14() V15() integer set
m2 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
n2 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
m2 div n2 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
- (m2 div n2) is ext-real non positive V14() V15() integer set
(- m) * (n,(- m)) is ext-real V14() V15() integer set
n div (- m) is ext-real V14() V15() integer set
m2 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
n2 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
m2 div n2 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
- (m2 div n2) is ext-real non positive V14() V15() integer set
(- (m2 div n2)) - 1 is ext-real non positive negative V4() V14() V15() integer set
(- m) * (n,(- m)) is ext-real V14() V15() integer set
(- m) * (n,(- m)) is ext-real V14() V15() integer set
ppn is ext-real V14() V15() integer set
(- m) * ppn is ext-real V14() V15() integer set
- ppn is ext-real V14() V15() integer set
(- ppn) - 1 is ext-real V14() V15() integer set
m * ppn is ext-real V14() V15() integer set
ppn is ext-real V14() V15() integer set
(- m) * ppn is ext-real V14() V15() integer set
- ppn is ext-real V14() V15() integer set
(- ppn) - 1 is ext-real V14() V15() integer set
m * ppn is ext-real V14() V15() integer set
m2 is ext-real V14() V15() integer set
(- m) * m2 is ext-real V14() V15() integer set
- m2 is ext-real V14() V15() integer set
(- m2) - 1 is ext-real V14() V15() integer set
m * m2 is ext-real V14() V15() integer set
n2 is ext-real V14() V15() integer set
(- m) * n2 is ext-real V14() V15() integer set
- n2 is ext-real V14() V15() integer set
(- n2) - 1 is ext-real V14() V15() integer set
m * n2 is ext-real V14() V15() integer set
n / m is ext-real V14() V15() set
[\(n / m)/] is ext-real V14() V15() integer set
(- n) / (- m) is ext-real V14() V15() set
[\((- n) / (- m))/] is ext-real V14() V15() integer set
(- n) div (- m) is ext-real V14() V15() integer set
(- m) * ((- n),(- m)) is ext-real V14() V15() integer set
- ((- n),(- m)) is ext-real V14() V15() integer set
(- ((- n),(- m))) - 1 is ext-real V14() V15() integer set
m * ((- n),(- m)) is ext-real V14() V15() integer set
m * ((- n),m) is ext-real V14() V15() integer set
(- n) div m is ext-real V14() V15() integer set
m2 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
n2 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
m2 div n2 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
- (m2 div n2) is ext-real non positive V14() V15() integer set
m * ((- n),m) is ext-real V14() V15() integer set
(- n) div m is ext-real V14() V15() integer set
m2 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
n2 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
m2 div n2 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
- (m2 div n2) is ext-real non positive V14() V15() integer set
(- (m2 div n2)) - 1 is ext-real non positive negative V4() V14() V15() integer set
m * ((- n),m) is ext-real V14() V15() integer set
m * ((- n),m) is ext-real V14() V15() integer set
ppn is ext-real V14() V15() integer set
(- m) * ppn is ext-real V14() V15() integer set
- ppn is ext-real V14() V15() integer set
(- ppn) - 1 is ext-real V14() V15() integer set
m * ppn is ext-real V14() V15() integer set
ppn is ext-real V14() V15() integer set
(- m) * ppn is ext-real V14() V15() integer set
- ppn is ext-real V14() V15() integer set
(- ppn) - 1 is ext-real V14() V15() integer set
m * ppn is ext-real V14() V15() integer set
m2 is ext-real V14() V15() integer set
(- m) * m2 is ext-real V14() V15() integer set
- m2 is ext-real V14() V15() integer set
(- m2) - 1 is ext-real V14() V15() integer set
m * m2 is ext-real V14() V15() integer set
n2 is ext-real V14() V15() integer set
(- m) * n2 is ext-real V14() V15() integer set
- n2 is ext-real V14() V15() integer set
(- n2) - 1 is ext-real V14() V15() integer set
m * n2 is ext-real V14() V15() integer set
m2 is ext-real V14() V15() integer set
(- m) * m2 is ext-real V14() V15() integer set
- m2 is ext-real V14() V15() integer set
(- m2) - 1 is ext-real V14() V15() integer set
m * m2 is ext-real V14() V15() integer set
n2 is ext-real V14() V15() integer set
(- m) * n2 is ext-real V14() V15() integer set
- n2 is ext-real V14() V15() integer set
(- n2) - 1 is ext-real V14() V15() integer set
m * n2 is ext-real V14() V15() integer set
m2 is ext-real V14() V15() integer set
ppn is ext-real V14() V15() integer set
(- m) * ppn is ext-real V14() V15() integer set
- ppn is ext-real V14() V15() integer set
(- ppn) - 1 is ext-real V14() V15() integer set
m * ppn is ext-real V14() V15() integer set
n2 is ext-real V14() V15() integer set
ppn is ext-real V14() V15() integer set
(- m) * ppn is ext-real V14() V15() integer set
- ppn is ext-real V14() V15() integer set
(- ppn) - 1 is ext-real V14() V15() integer set
m * ppn is ext-real V14() V15() integer set
n is ext-real V14() V15() integer set
m is ext-real V14() V15() integer set
(n,m) is ext-real V14() V15() integer set
n div m is ext-real V14() V15() integer set
(n,m) is ext-real V14() V15() integer set
- m is ext-real V14() V15() integer set
(n,(- m)) is ext-real V14() V15() integer set
(- m) * (n,(- m)) is ext-real V14() V15() integer set
n2 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
m2 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
n2 div m2 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
- (n,(- m)) is ext-real V14() V15() integer set
- m is ext-real V14() V15() integer set
(n,(- m)) is ext-real V14() V15() integer set
(- m) * (n,(- m)) is ext-real V14() V15() integer set
n2 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
m2 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
n2 div m2 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
- (n,(- m)) is ext-real V14() V15() integer set
(- (n,(- m))) - 1 is ext-real V14() V15() integer set
- m is ext-real V14() V15() integer set
(n,(- m)) is ext-real V14() V15() integer set
(- m) * (n,(- m)) is ext-real V14() V15() integer set
- m is ext-real V14() V15() integer set
(n,(- m)) is ext-real V14() V15() integer set
(- m) * (n,(- m)) is ext-real V14() V15() integer set
- m is ext-real V14() V15() integer set
n / m is ext-real V14() V15() set
[\(n / m)/] is ext-real V14() V15() integer set
- n is ext-real V14() V15() integer set
(- n) / (- m) is ext-real V14() V15() set
[\((- n) / (- m))/] is ext-real V14() V15() integer set
(- n) div (- m) is ext-real V14() V15() integer set
((- n),(- m)) is ext-real V14() V15() integer set
- n is ext-real V14() V15() integer set
((- n),m) is ext-real V14() V15() integer set
m * ((- n),m) is ext-real V14() V15() integer set
n2 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
m2 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
n2 div m2 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
- ((- n),m) is ext-real V14() V15() integer set
- n is ext-real V14() V15() integer set
((- n),m) is ext-real V14() V15() integer set
m * ((- n),m) is ext-real V14() V15() integer set
n2 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
m2 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
n2 div m2 is ext-real non negative V7() V8() V9() V13() V14() V15() integer Element of NAT
- ((- n),m) is ext-real V14() V15() integer set
(- ((- n),m)) - 1 is ext-real V14() V15() integer set
- n is ext-real V14() V15() integer set
((- n),m) is ext-real V14() V15() integer set
m * ((- n),m) is ext-real V14() V15() integer set
- n is ext-real V14() V15() integer set
((- n),m) is ext-real V14() V15() integer set
m * ((- n),m) is ext-real V14() V15() integer set