:: NUMERAL1 semantic presentation

REAL is non empty V12() V45() V50() V51() V52() V56() set
NAT is non empty V12() V21() V22() V23() V45() V50() V51() V52() V53() V54() V55() V56() V68() V69() Element of K19(REAL)
K19(REAL) is V12() V45() set
K20(NAT,REAL) is Relation-like V12() V35() V36() V37() V45() set
K19(K20(NAT,REAL)) is V12() V45() set
COMPLEX is non empty V12() V45() V50() V56() set
RAT is non empty V12() V45() V50() V51() V52() V53() V56() set
INT is non empty V12() V45() V50() V51() V52() V53() V54() V56() set
{} is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty V21() V22() V23() V25() V26() V27() V28() V29() ext-real non positive non negative V34() V35() V36() V37() V38() V45() V46() V49() V50() V51() V52() V53() V54() V55() V56() V66() V68() V70( {} ) V143() set
1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
{{},1} is non empty V45() V49() V50() V51() V52() V53() V54() V55() set
NAT is non empty V12() V21() V22() V23() V45() V50() V51() V52() V53() V54() V55() V56() V68() V69() set
K19(NAT) is V12() V45() set
K19(NAT) is V12() V45() set
K20(COMPLEX,COMPLEX) is Relation-like V12() V35() V45() set
K19(K20(COMPLEX,COMPLEX)) is V12() V45() set
K20(K20(COMPLEX,COMPLEX),COMPLEX) is Relation-like V12() V35() V45() set
K19(K20(K20(COMPLEX,COMPLEX),COMPLEX)) is V12() V45() set
K20(REAL,REAL) is Relation-like V12() V35() V36() V37() V45() set
K19(K20(REAL,REAL)) is V12() V45() set
K20(K20(REAL,REAL),REAL) is Relation-like V12() V35() V36() V37() V45() set
K19(K20(K20(REAL,REAL),REAL)) is V12() V45() set
K20(RAT,RAT) is Relation-like RAT -valued V12() V35() V36() V37() V45() set
K19(K20(RAT,RAT)) is V12() V45() set
K20(K20(RAT,RAT),RAT) is Relation-like RAT -valued V12() V35() V36() V37() V45() set
K19(K20(K20(RAT,RAT),RAT)) is V12() V45() set
K20(INT,INT) is Relation-like RAT -valued INT -valued V12() V35() V36() V37() V45() set
K19(K20(INT,INT)) is V12() V45() set
K20(K20(INT,INT),INT) is Relation-like RAT -valued INT -valued V12() V35() V36() V37() V45() set
K19(K20(K20(INT,INT),INT)) is V12() V45() set
K20(NAT,NAT) is Relation-like RAT -valued INT -valued V12() V35() V36() V37() V38() V45() V66() set
K20(K20(NAT,NAT),NAT) is Relation-like RAT -valued INT -valued V12() V35() V36() V37() V38() V45() V66() set
K19(K20(K20(NAT,NAT),NAT)) is V12() V45() set
2 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
3 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
0 is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty V21() V22() V23() V25() V26() V27() V28() V29() V30() ext-real non positive non negative V34() V35() V36() V37() V38() V45() V46() V49() V50() V51() V52() V53() V54() V55() V56() V66() V68() V70( {} ) V143() Element of NAT
{{}} is functional non empty V12() V45() V49() V50() V51() V52() V53() V54() V55() V70(1) set
addnat is Relation-like K20(NAT,NAT) -defined NAT -valued INT -valued Function-like V14(K20(NAT,NAT)) V18(K20(NAT,NAT), NAT ) V35() V36() V37() V38() V66() V135( NAT ) V144( NAT ) V145( NAT ) Element of K19(K20(K20(NAT,NAT),NAT))
d is V21() V22() V23() V27() V28() V29() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() set
d GeoSeq is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
n is V21() V22() V23() V27() V28() V29() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() set
n (#) (d GeoSeq) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
i is V21() V22() V23() V27() V28() V29() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() set
(n (#) (d GeoSeq)) | i is Relation-like NAT -defined i -defined NAT -defined REAL -valued Function-like V35() V36() V37() V45() Element of K19(K20(NAT,REAL))
dom (n (#) (d GeoSeq)) is non empty V50() V51() V52() V53() V54() V55() Element of K19(NAT)
dom ((n (#) (d GeoSeq)) | i) is V45() V50() V51() V52() V53() V54() V55() Element of K19(i)
K19(i) is V45() V49() set
d9 is Relation-like NAT -defined Function-like V25() V45() V143() set
rng d9 is V45() set
l is set
dz is set
((n (#) (d GeoSeq)) | i) . dz is V28() ext-real V34() set
l is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
((n (#) (d GeoSeq)) | i) . l is V28() ext-real V34() set
(n (#) (d GeoSeq)) . l is V28() ext-real V34() Element of REAL
(d GeoSeq) . l is V28() ext-real V34() Element of REAL
n * ((d GeoSeq) . l) is V28() ext-real V34() Element of REAL
d |^ l is V21() V22() V23() V27() V28() V29() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() set
n * (d |^ l) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
n is Relation-like NAT -defined NAT -valued Function-like V25() V35() V36() V37() V38() V45() V66() V143() set
dom n is V21() V22() V23() V27() V28() V29() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of K19(NAT)
Sum n is V21() V22() V23() V27() V28() V29() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of COMPLEX
d is V21() V22() V23() V27() V28() V29() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() set
len n is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
dom n is V21() V22() V23() V27() V28() V29() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() set
len n is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
dom n is V21() V22() V23() V27() V28() V29() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() set
K19(K20(NAT,NAT)) is V12() V45() set
n . 0 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
addnat "**" n is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
(len n) - 1 is V28() V29() V30() ext-real V34() Element of INT
i is Relation-like NAT -defined NAT -valued Function-like non empty V14( NAT ) V18( NAT , NAT ) V35() V36() V37() V38() V66() Element of K19(K20(NAT,NAT))
i . 0 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
i . ((len n) - 1) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
j is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
i . j is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
j + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
i . (j + 1) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
n . (j + 1) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
addnat . ((i . j),(n . (j + 1))) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
(i . j) + (n . (j + 1)) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
j is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
len n is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
dom n is V21() V22() V23() V27() V28() V29() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() set
n is Relation-like NAT -defined NAT -valued Function-like V25() V35() V36() V37() V38() V45() V66() V143() set
dom n is V21() V22() V23() V27() V28() V29() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of K19(NAT)
d is Relation-like NAT -defined NAT -valued Function-like V25() V35() V36() V37() V38() V45() V66() V143() set
dom d is V21() V22() V23() V27() V28() V29() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of K19(NAT)
Sum n is V21() V22() V23() V27() V28() V29() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of COMPLEX
Sum d is V21() V22() V23() V27() V28() V29() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of COMPLEX
i is V21() V22() V23() V27() V28() V29() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() set
(Sum n) mod i is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
(Sum d) mod i is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
j is Relation-like NAT -defined NAT -valued Function-like V25() V35() V36() V37() V38() V45() V66() V143() set
dom j is V21() V22() V23() V27() V28() V29() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of K19(NAT)
Sum j is V21() V22() V23() V27() V28() V29() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of COMPLEX
(Sum j) mod i is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
d9 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
<%d9%> is Relation-like NAT -defined NAT -valued Function-like constant non empty V12() V25() V35() V36() V37() V38() V39() V40() V41() V42() V45() V66() V70(1) V143() set
j ^ <%d9%> is Relation-like NAT -defined NAT -valued Function-like non empty V25() V35() V36() V37() V38() V45() V66() V143() set
dom (j ^ <%d9%>) is non empty V21() V22() V23() V27() V28() V29() ext-real positive non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of K19(NAT)
Sum (j ^ <%d9%>) is V21() V22() V23() V27() V28() V29() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of COMPLEX
(Sum (j ^ <%d9%>)) mod i is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
dz is Relation-like NAT -defined NAT -valued Function-like V25() V35() V36() V37() V38() V45() V66() V143() set
dom dz is V21() V22() V23() V27() V28() V29() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of K19(NAT)
Sum dz is V21() V22() V23() V27() V28() V29() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of COMPLEX
(Sum dz) mod i is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
l is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
l is V21() V22() V23() V27() V28() V29() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() set
j . l is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
(j . l) mod i is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
l is Relation-like NAT -defined NAT -valued Function-like V25() V35() V36() V37() V38() V45() V66() V143() set
dom l is V21() V22() V23() V27() V28() V29() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of K19(NAT)
E is V21() V22() V23() V27() V28() V29() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() set
len j is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
dom j is V21() V22() V23() V27() V28() V29() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() set
(len j) + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
len <%d9%> is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
dom <%d9%> is non empty V12() V21() V22() V23() V27() V28() V29() ext-real positive non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() V70(1) set
(len j) + (len <%d9%>) is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
dz . E is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
(j ^ <%d9%>) . E is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
((j ^ <%d9%>) . E) mod i is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
j . E is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
(j . E) mod i is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
l . E is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
E is V21() V22() V23() V27() V28() V29() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() set
d9 mod i is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
<%(d9 mod i)%> is Relation-like NAT -defined NAT -valued Function-like constant non empty V12() V25() V35() V36() V37() V38() V39() V40() V41() V42() V45() V66() V70(1) V143() set
dom <%(d9 mod i)%> is non empty V12() V21() V22() V23() V27() V28() V29() ext-real positive non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() V70(1) Element of K19(NAT)
dom <%d9%> is non empty V12() V21() V22() V23() V27() V28() V29() ext-real positive non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() V70(1) Element of K19(NAT)
len l is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
dom l is V21() V22() V23() V27() V28() V29() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() set
(len l) + E is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
dz . ((len l) + E) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
(j ^ <%d9%>) . (len j) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
((j ^ <%d9%>) . (len j)) mod i is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
<%(d9 mod i)%> . E is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
(dom j) + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
len <%(d9 mod i)%> is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
dom <%(d9 mod i)%> is non empty V12() V21() V22() V23() V27() V28() V29() ext-real positive non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() V70(1) set
(len l) + (len <%(d9 mod i)%>) is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
l ^ <%(d9 mod i)%> is Relation-like NAT -defined NAT -valued Function-like non empty V25() V35() V36() V37() V38() V45() V66() V143() set
Sum <%d9%> is V21() V22() V23() V27() V28() V29() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of COMPLEX
(Sum j) + (Sum <%d9%>) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
((Sum j) + (Sum <%d9%>)) mod i is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
(Sum j) + d9 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
((Sum j) + d9) mod i is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
((Sum j) mod i) + d9 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
(((Sum j) mod i) + d9) mod i is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
((Sum j) mod i) + (d9 mod i) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
(((Sum j) mod i) + (d9 mod i)) mod i is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
Sum l is V21() V22() V23() V27() V28() V29() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of COMPLEX
(Sum l) mod i is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
((Sum l) mod i) + (d9 mod i) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
(((Sum l) mod i) + (d9 mod i)) mod i is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
(Sum l) + (d9 mod i) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
((Sum l) + (d9 mod i)) mod i is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
Sum <%(d9 mod i)%> is V21() V22() V23() V27() V28() V29() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of COMPLEX
(Sum l) + (Sum <%(d9 mod i)%>) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
((Sum l) + (Sum <%(d9 mod i)%>)) mod i is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
<%> NAT is Relation-like non-empty empty-yielding NAT -defined NAT -valued Function-like one-to-one constant functional empty V21() V22() V23() V25() V26() V27() V28() V29() ext-real non positive non negative V34() V35() V36() V37() V38() V45() V46() V49() V50() V51() V52() V53() V54() V55() V56() V66() V68() V70( {} ) V143() set
dom (<%> NAT) is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty V21() V22() V23() V25() V26() V27() V28() V29() ext-real non positive non negative V34() V35() V36() V37() V38() V45() V46() V49() V50() V51() V52() V53() V54() V55() V56() V66() V68() V70( {} ) V143() Element of K19(NAT)
Sum (<%> NAT) is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty V21() V22() V23() V25() V26() V27() V28() V29() ext-real non positive non negative V34() V35() V36() V37() V38() V45() V46() V49() V50() V51() V52() V53() V54() V55() V56() V66() V68() V70( {} ) V143() Element of COMPLEX
(Sum (<%> NAT)) mod i is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
j is Relation-like NAT -defined NAT -valued Function-like V25() V35() V36() V37() V38() V45() V66() V143() set
dom j is V21() V22() V23() V27() V28() V29() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of K19(NAT)
Sum j is V21() V22() V23() V27() V28() V29() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of COMPLEX
(Sum j) mod i is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
len j is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
dom j is V21() V22() V23() V27() V28() V29() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() set
n is Relation-like NAT -defined NAT -valued Function-like V25() V35() V36() V37() V38() V45() V66() V143() set
dom n is V21() V22() V23() V27() V28() V29() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of K19(NAT)
d is V21() V22() V23() V27() V28() V29() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() set
len n is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
dom n is V21() V22() V23() V27() V28() V29() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() set
i is Relation-like NAT -defined Function-like V25() V45() V143() set
len i is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
dom i is V21() V22() V23() V27() V28() V29() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() set
rng i is V45() set
j is set
dom i is V21() V22() V23() V27() V28() V29() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of K19(NAT)
d9 is set
i . d9 is set
l is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
n . l is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
d |^ l is V21() V22() V23() V27() V28() V29() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() set
(n . l) * (d |^ l) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
j is Relation-like NAT -defined NAT -valued Function-like V25() V35() V36() V37() V38() V45() V66() V143() set
Sum j is V21() V22() V23() V27() V28() V29() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of COMPLEX
i is V21() V22() V23() V27() V28() V29() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() set
j is V21() V22() V23() V27() V28() V29() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() set
d9 is Relation-like NAT -defined NAT -valued Function-like V25() V35() V36() V37() V38() V45() V66() V143() set
dom d9 is V21() V22() V23() V27() V28() V29() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of K19(NAT)
Sum d9 is V21() V22() V23() V27() V28() V29() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of COMPLEX
l is Relation-like NAT -defined NAT -valued Function-like V25() V35() V36() V37() V38() V45() V66() V143() set
dom l is V21() V22() V23() V27() V28() V29() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of K19(NAT)
Sum l is V21() V22() V23() V27() V28() V29() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of COMPLEX
dz is V21() V22() V23() V27() V28() V29() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() set
d9 . dz is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
n . dz is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
d |^ dz is V21() V22() V23() V27() V28() V29() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() set
(n . dz) * (d |^ dz) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
l . dz is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
d is V21() V22() V23() V27() V28() V29() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() set
n is V21() V22() V23() V27() V28() V29() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() set
<%0%> is Relation-like NAT -defined NAT -valued Function-like constant non empty V12() V25() V35() V36() V37() V38() V39() V40() V41() V42() V45() V66() V70(1) V143() set
d9 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
K19(K20(NAT,NAT)) is V12() V45() set
j is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
l is Relation-like NAT -defined NAT -valued Function-like non empty V14( NAT ) V18( NAT , NAT ) V35() V36() V37() V38() V66() Element of K19(K20(NAT,NAT))
l . 0 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
dz is V21() V22() V23() V27() V28() V29() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() set
dz div d is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
l is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
E is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
l . E is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
E is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
l . E is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
E + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
l . (E + 1) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
dz is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
l . dz is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
dz is V21() V22() V23() V27() V28() V29() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() set
l . dz is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
l is V21() V22() V23() V27() V28() V29() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() set
l + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
dom l is non empty V50() V51() V52() V53() V54() V55() Element of K19(NAT)
E is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
E + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
l | (E + 1) is Relation-like NAT -defined E + 1 -defined NAT -defined NAT -valued RAT -valued Function-like V35() V36() V37() V38() V45() V66() Element of K19(K20(NAT,NAT))
dom (l | (E + 1)) is V45() V50() V51() V52() V53() V54() V55() Element of K19(NAT)
l is Relation-like NAT -defined NAT -valued Function-like V25() V35() V36() V37() V38() V45() V66() V143() set
g is V21() V22() V23() V27() V28() V29() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() set
l . g is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
(l . g) mod d is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
g is Relation-like NAT -defined NAT -valued Function-like V25() V35() V36() V37() V38() V45() V66() V143() set
dom g is V21() V22() V23() V27() V28() V29() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of K19(NAT)
a is V21() V22() V23() V27() V28() V29() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() set
l . a is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
a + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
l . (a + 1) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
0 div d is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
a is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
l . a is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
len g is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
dom g is V21() V22() V23() V27() V28() V29() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() set
a is Relation-like NAT -defined Function-like V25() V45() V143() set
len a is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
dom a is V21() V22() V23() V27() V28() V29() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() set
rng a is V45() set
o is set
dom a is V21() V22() V23() V27() V28() V29() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of K19(NAT)
oo is set
a . oo is set
o1 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
g . o1 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
d |^ o1 is V21() V22() V23() V27() V28() V29() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() set
(g . o1) * (d |^ o1) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
o is Relation-like NAT -defined NAT -valued Function-like V25() V35() V36() V37() V38() V45() V66() V143() set
o . 0 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
len o is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
dom o is V21() V22() V23() V27() V28() V29() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() set
addnat "**" o is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
(len o) - 1 is V28() V29() V30() ext-real V34() Element of INT
oo is Relation-like NAT -defined NAT -valued Function-like non empty V14( NAT ) V18( NAT , NAT ) V35() V36() V37() V38() V66() Element of K19(K20(NAT,NAT))
oo . 0 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
oo . ((len o) - 1) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
o1 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
oo . o1 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
o1 + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
l . (o1 + 1) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
d |^ (o1 + 1) is V21() V22() V23() V27() V28() V29() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() set
(l . (o1 + 1)) * (d |^ (o1 + 1)) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
n - ((l . (o1 + 1)) * (d |^ (o1 + 1))) is V28() V29() V30() ext-real V34() Element of INT
dom o is V21() V22() V23() V27() V28() V29() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of K19(NAT)
oo . (o1 + 1) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
o . (o1 + 1) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
addnat . ((oo . o1),(o . (o1 + 1))) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
(n - ((l . (o1 + 1)) * (d |^ (o1 + 1)))) + (o . (o1 + 1)) is V28() V29() V30() ext-real V34() Element of INT
g . (o1 + 1) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
(g . (o1 + 1)) * (d |^ (o1 + 1)) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
(n - ((l . (o1 + 1)) * (d |^ (o1 + 1)))) + ((g . (o1 + 1)) * (d |^ (o1 + 1))) is V28() V29() V30() ext-real V34() Element of INT
l . (o1 + 1) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
(l . (o1 + 1)) mod d is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
((l . (o1 + 1)) mod d) * (d |^ (o1 + 1)) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
(n - ((l . (o1 + 1)) * (d |^ (o1 + 1)))) + (((l . (o1 + 1)) mod d) * (d |^ (o1 + 1))) is V28() V29() V30() ext-real V34() Element of INT
(l . (o1 + 1)) mod d is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
((l . (o1 + 1)) mod d) * (d |^ (o1 + 1)) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
(n - ((l . (o1 + 1)) * (d |^ (o1 + 1)))) + (((l . (o1 + 1)) mod d) * (d |^ (o1 + 1))) is V28() V29() V30() ext-real V34() Element of INT
(l . (o1 + 1)) div d9 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
d * ((l . (o1 + 1)) div d9) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
(l . (o1 + 1)) - (d * ((l . (o1 + 1)) div d9)) is V28() V29() V30() ext-real V34() Element of INT
((l . (o1 + 1)) - (d * ((l . (o1 + 1)) div d9))) * (d |^ (o1 + 1)) is V28() V29() V30() ext-real V34() Element of INT
(n - ((l . (o1 + 1)) * (d |^ (o1 + 1)))) + (((l . (o1 + 1)) - (d * ((l . (o1 + 1)) div d9))) * (d |^ (o1 + 1))) is V28() V29() V30() ext-real V34() Element of INT
(o1 + 1) + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
l . ((o1 + 1) + 1) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
d * (l . ((o1 + 1) + 1)) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
(l . (o1 + 1)) - (d * (l . ((o1 + 1) + 1))) is V28() V29() V30() ext-real V34() Element of INT
((l . (o1 + 1)) - (d * (l . ((o1 + 1) + 1)))) * (d |^ (o1 + 1)) is V28() V29() V30() ext-real V34() Element of INT
(n - ((l . (o1 + 1)) * (d |^ (o1 + 1)))) + (((l . (o1 + 1)) - (d * (l . ((o1 + 1) + 1)))) * (d |^ (o1 + 1))) is V28() V29() V30() ext-real V34() Element of INT
d * (d |^ (o1 + 1)) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
(l . ((o1 + 1) + 1)) * (d * (d |^ (o1 + 1))) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
((l . (o1 + 1)) * (d |^ (o1 + 1))) - ((l . ((o1 + 1) + 1)) * (d * (d |^ (o1 + 1)))) is V28() V29() V30() ext-real V34() Element of INT
(n - ((l . (o1 + 1)) * (d |^ (o1 + 1)))) + (((l . (o1 + 1)) * (d |^ (o1 + 1))) - ((l . ((o1 + 1) + 1)) * (d * (d |^ (o1 + 1))))) is V28() V29() V30() ext-real V34() Element of INT
d |^ ((o1 + 1) + 1) is V21() V22() V23() V27() V28() V29() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() set
(l . ((o1 + 1) + 1)) * (d |^ ((o1 + 1) + 1)) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
((l . (o1 + 1)) * (d |^ (o1 + 1))) - ((l . ((o1 + 1) + 1)) * (d |^ ((o1 + 1) + 1))) is V28() V29() V30() ext-real V34() Element of INT
(n - ((l . (o1 + 1)) * (d |^ (o1 + 1)))) + (((l . (o1 + 1)) * (d |^ (o1 + 1))) - ((l . ((o1 + 1) + 1)) * (d |^ ((o1 + 1) + 1)))) is V28() V29() V30() ext-real V34() Element of INT
n - ((l . ((o1 + 1) + 1)) * (d |^ ((o1 + 1) + 1))) is V28() V29() V30() ext-real V34() Element of INT
g . 0 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
d |^ 0 is V21() V22() V23() V27() V28() V29() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() set
(g . 0) * (d |^ 0) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
l . 0 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
(l . 0) mod d is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
((l . 0) mod d) * (d |^ 0) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
(l . 0) mod d is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
((l . 0) mod d) * (d |^ 0) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
n mod d is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
(n mod d) * 1 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
j div d9 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
d9 * (j div d9) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
j - (d9 * (j div d9)) is V28() V29() V30() ext-real V34() Element of INT
n div d is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
d |^ 1 is V21() V22() V23() V27() V28() V29() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() set
(n div d) * (d |^ 1) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
n - ((n div d) * (d |^ 1)) is V28() V29() V30() ext-real V34() Element of INT
0 + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
l . (0 + 1) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
d |^ (0 + 1) is V21() V22() V23() V27() V28() V29() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() set
(l . (0 + 1)) * (d |^ (0 + 1)) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
n - ((l . (0 + 1)) * (d |^ (0 + 1))) is V28() V29() V30() ext-real V34() Element of INT
o1 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
oo . o1 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
l . (E + 1) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
d |^ (E + 1) is V21() V22() V23() V27() V28() V29() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() set
(l . (E + 1)) * (d |^ (E + 1)) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
n - ((l . (E + 1)) * (d |^ (E + 1))) is V28() V29() V30() ext-real V34() Element of INT
Sum o is V21() V22() V23() V27() V28() V29() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of COMPLEX
l . E is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
(g,d) is V21() V22() V23() V27() V28() V29() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() set
(len g) - 1 is V28() V29() V30() ext-real V34() Element of INT
g . ((len g) - 1) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
l . E is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
(l . E) div d is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
(l . E) mod d is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
bo1 is V21() V22() V23() V27() V28() V29() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() set
g . bo1 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
l . bo1 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
(l . bo1) mod d is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
i is Relation-like NAT -defined NAT -valued Function-like V25() V35() V36() V37() V38() V45() V66() V143() set
d - 1 is V28() V29() V30() ext-real V34() Element of INT
j is Relation-like NAT -defined NAT -valued Function-like V25() V35() V36() V37() V38() V45() V66() V143() set
(j,d) is V21() V22() V23() V27() V28() V29() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() set
len j is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
dom j is V21() V22() V23() V27() V28() V29() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() set
(len j) - 1 is V28() V29() V30() ext-real V34() Element of INT
j . ((len j) - 1) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
dom j is V21() V22() V23() V27() V28() V29() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of K19(NAT)
d9 is Relation-like NAT -defined NAT -valued Function-like V25() V35() V36() V37() V38() V45() V66() V143() set
(d9,d) is V21() V22() V23() V27() V28() V29() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() set
len d9 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
dom d9 is V21() V22() V23() V27() V28() V29() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() set
(len d9) - 1 is V28() V29() V30() ext-real V34() Element of INT
d9 . ((len d9) - 1) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
dom d9 is V21() V22() V23() V27() V28() V29() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of K19(NAT)
log (2,d) is V28() ext-real V34() set
log (2,1) is V28() ext-real V34() Element of REAL
1 - d is V28() V29() V30() ext-real V34() Element of INT
d GeoSeq is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
i is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
i (#) (d GeoSeq) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
(i (#) (d GeoSeq)) | (len j) is Relation-like NAT -defined len j -defined NAT -defined REAL -valued Function-like V35() V36() V37() V45() Element of K19(K20(NAT,REAL))
dz is Relation-like NAT -defined NAT -valued Function-like V25() V35() V36() V37() V38() V45() V66() V143() set
dom dz is V21() V22() V23() V27() V28() V29() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of K19(NAT)
Sum dz is V21() V22() V23() V27() V28() V29() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of COMPLEX
len dz is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
dom dz is V21() V22() V23() V27() V28() V29() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() set
l is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
d |^ l is V21() V22() V23() V27() V28() V29() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() set
1 * (d |^ l) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
j . l is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
(j . l) * (d |^ l) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
dz . l is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
d to_power l is V28() ext-real V34() set
log (2,(d to_power l)) is V28() ext-real V34() set
log (2,n) is V28() ext-real V34() set
l * (log (2,d)) is V28() ext-real V34() Element of REAL
(l * (log (2,d))) / (log (2,d)) is V28() ext-real V34() Element of REAL
(log (2,n)) / (log (2,d)) is V28() ext-real V34() Element of REAL
l is Relation-like NAT -defined NAT -valued Function-like V25() V35() V36() V37() V38() V45() V66() V143() set
(d - 1) (#) (d GeoSeq) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
l + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
((d - 1) (#) (d GeoSeq)) | (l + 1) is Relation-like NAT -defined l + 1 -defined NAT -defined REAL -valued Function-like V35() V36() V37() V45() Element of K19(K20(NAT,REAL))
Sum l is V21() V22() V23() V27() V28() V29() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of COMPLEX
Partial_Sums ((d - 1) (#) (d GeoSeq)) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
(Partial_Sums ((d - 1) (#) (d GeoSeq))) . l is V28() ext-real V34() Element of REAL
Partial_Sums (d GeoSeq) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
(d - 1) (#) (Partial_Sums (d GeoSeq)) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
((d - 1) (#) (Partial_Sums (d GeoSeq))) . l is V28() ext-real V34() Element of REAL
(Partial_Sums (d GeoSeq)) . l is V28() ext-real V34() Element of REAL
(d - 1) * ((Partial_Sums (d GeoSeq)) . l) is V28() ext-real V34() Element of REAL
d to_power (l + 1) is V28() ext-real V34() set
d |^ (l + 1) is V21() V22() V23() V27() V28() V29() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() set
1 - (d to_power (l + 1)) is V28() ext-real V34() Element of REAL
(1 - (d to_power (l + 1))) / (1 - d) is V28() ext-real V34() Element of REAL
(d - 1) * ((1 - (d to_power (l + 1))) / (1 - d)) is V28() ext-real V34() Element of REAL
1 - (d |^ (l + 1)) is V28() V29() V30() ext-real V34() Element of INT
(1 - (d |^ (l + 1))) / (1 - d) is V28() V30() ext-real V34() Element of RAT
(1 - d) * ((1 - (d |^ (l + 1))) / (1 - d)) is V28() V30() ext-real V34() Element of RAT
- ((1 - d) * ((1 - (d |^ (l + 1))) / (1 - d))) is V28() V30() ext-real V34() Element of RAT
- (1 - (d |^ (l + 1))) is V28() V29() V30() ext-real V34() Element of INT
(d |^ (l + 1)) - 1 is V28() V29() V30() ext-real V34() Element of INT
dom ((d - 1) (#) (d GeoSeq)) is non empty V50() V51() V52() V53() V54() V55() Element of K19(NAT)
len l is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
dom l is V21() V22() V23() V27() V28() V29() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() set
dom l is V21() V22() V23() V27() V28() V29() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of K19(NAT)
E is V21() V22() V23() V27() V28() V29() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() set
dz . E is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
l . E is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
j . E is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
d |^ E is V21() V22() V23() V27() V28() V29() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() set
(j . E) * (d |^ E) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
i + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
l is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
l . l is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V34() V45() V50() V51() V52() V53() V54() V55() V68() Element of NAT
((d - 1) (#) (d GeoSeq)) . l is V28() ext-real V34() Element of REAL
(d GeoSeq) . l is V28() ext-real V34() Element of REAL
(d - 1) * ((d GeoSeq) . l) is V28() ext-real V34() Element of REAL
d |^ l is V21() V22() V23()