:: JORDAN4 semantic presentation

REAL is V148() V149() V150() V154() set
NAT is V6() V28() V33() V34() V148() V149() V150() V151() V152() V153() V154() Element of K6(REAL)
K6(REAL) is set
COMPLEX is V148() V154() set
NAT is V6() V28() V33() V34() V148() V149() V150() V151() V152() V153() V154() set
K6(NAT) is V28() set
K6(NAT) is V28() set
RAT is V148() V149() V150() V151() V154() set
INT is V148() V149() V150() V151() V152() V154() set
K7(COMPLEX,COMPLEX) is set
K6(K7(COMPLEX,COMPLEX)) is set
K7(K7(COMPLEX,COMPLEX),COMPLEX) is set
K6(K7(K7(COMPLEX,COMPLEX),COMPLEX)) is set
K7(REAL,REAL) is set
K6(K7(REAL,REAL)) is set
K7(K7(REAL,REAL),REAL) is set
K6(K7(K7(REAL,REAL),REAL)) is set
K7(RAT,RAT) is set
K6(K7(RAT,RAT)) is set
K7(K7(RAT,RAT),RAT) is set
K6(K7(K7(RAT,RAT),RAT)) is set
K7(INT,INT) is set
K6(K7(INT,INT)) is set
K7(K7(INT,INT),INT) is set
K6(K7(K7(INT,INT),INT)) is set
K7(NAT,NAT) is set
K7(K7(NAT,NAT),NAT) is set
K6(K7(K7(NAT,NAT),NAT)) is set
K279() is set
1 is non empty V6() V10() V11() V12() V13() V28() V33() V43() ext-real positive non negative V148() V149() V150() V151() V152() V153() Element of NAT
K7(1,1) is set
K6(K7(1,1)) is set
K7(K7(1,1),1) is set
K6(K7(K7(1,1),1)) is set
K7(K7(1,1),REAL) is set
K6(K7(K7(1,1),REAL)) is set
2 is non empty V6() V10() V11() V12() V13() V28() V33() V43() ext-real positive non negative V148() V149() V150() V151() V152() V153() Element of NAT
K7(2,2) is set
K7(K7(2,2),REAL) is set
K6(K7(K7(2,2),REAL)) is set
TOP-REAL 2 is non empty TopSpace-like V114() V160() V161() V162() V163() V164() V165() V166() strict RLTopStruct
the U1 of (TOP-REAL 2) is non empty set
K6( the U1 of (TOP-REAL 2)) is set
{} is empty V6() functional V33() V35( {} ) FinSequence-membered V148() V149() V150() V151() V152() V153() V154() set
3 is non empty V6() V10() V11() V12() V13() V28() V33() V43() ext-real positive non negative V148() V149() V150() V151() V152() V153() Element of NAT
0 is empty V6() V10() V11() V12() V13() functional V28() V33() V35( {} ) FinSequence-membered V43() ext-real non positive non negative V148() V149() V150() V151() V152() V153() V154() Element of NAT
4 is non empty V6() V10() V11() V12() V13() V28() V33() V43() ext-real positive non negative V148() V149() V150() V151() V152() V153() Element of NAT
len {} is empty V6() functional V33() V35( {} ) FinSequence-membered V148() V149() V150() V151() V152() V153() V154() set
f is V6() V10() V11() V12() V28() V33() ext-real non negative set
i1 is V6() V10() V11() V12() V28() V33() ext-real non negative set
i1 + i1 is V6() V10() V11() V12() V28() V33() ext-real non negative set
f mod i1 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
(i1 + i1) - i1 is V11() V12() ext-real set
f - i1 is V11() V12() ext-real set
f -' i1 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
(f -' i1) mod i1 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
(f - i1) + i1 is V11() V12() ext-real set
(f -' i1) + i1 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
((f -' i1) + i1) mod i1 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
i1 mod i1 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
(f -' i1) + (i1 mod i1) is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
((f -' i1) + (i1 mod i1)) mod i1 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
(f -' i1) + 0 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
((f -' i1) + 0) mod i1 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
i1 is V6() V10() V11() V12() V28() V33() ext-real non negative set
f is V6() V10() V11() V12() V28() V33() ext-real non negative set
i1 + i1 is V6() V10() V11() V12() V28() V33() ext-real non negative set
f mod i1 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
f - i1 is V11() V12() ext-real set
f -' i1 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
(i1 + i1) - i1 is V11() V12() ext-real set
(f - i1) + i1 is V11() V12() ext-real set
(f -' i1) + i1 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
((f -' i1) + i1) mod i1 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
i1 mod i1 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
(f -' i1) + (i1 mod i1) is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
((f -' i1) + (i1 mod i1)) mod i1 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
(f -' i1) + 0 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
((f -' i1) + 0) mod i1 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
(f -' i1) mod i1 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
i1 is V6() V10() V11() V12() V28() V33() ext-real non negative set
i1 + i1 is V6() V10() V11() V12() V28() V33() ext-real non negative set
(i1 + i1) mod i1 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
2 * i1 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
(2 * i1) mod i1 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
i1 is V6() V10() V11() V12() V28() V33() ext-real non negative set
f is V6() V10() V11() V12() V28() V33() ext-real non negative set
i1 mod f is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
f is non empty set
i1 is V15() V18( NAT ) V19(f) Function-like V28() FinSequence-like FinSubsequence-like FinSequence of f
len i1 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
i1 . 1 is set
i1 . (len i1) is set
i1 /. 1 is Element of f
i1 /. (len i1) is Element of f
f is non empty set
i1 is V15() V18( NAT ) V19(f) Function-like V28() FinSequence-like FinSubsequence-like FinSequence of f
len i1 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
i1 . (len i1) is set
i1 /. (len i1) is Element of f
i2 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
i1 /^ i2 is V15() V18( NAT ) V19(f) Function-like V28() FinSequence-like FinSubsequence-like FinSequence of f
len (i1 /^ i2) is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
(i1 /^ i2) . (len (i1 /^ i2)) is set
(i1 /^ i2) /. (len (i1 /^ i2)) is Element of f
i2 + 1 is non empty V6() V10() V11() V12() V13() V28() V33() V43() ext-real positive non negative V148() V149() V150() V151() V152() V153() Element of NAT
(i2 + 1) - i2 is V11() V12() ext-real Element of REAL
(len i1) - i2 is V11() V12() ext-real Element of REAL
Seg (len (i1 /^ i2)) is V28() V35( len (i1 /^ i2)) V148() V149() V150() V151() V152() V153() Element of K6(NAT)
dom (i1 /^ i2) is V148() V149() V150() V151() V152() V153() Element of K6(NAT)
(len (i1 /^ i2)) + i2 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
((len i1) - i2) + i2 is V11() V12() ext-real Element of REAL
0 + 1 is non empty V6() V10() V11() V12() V13() V28() V33() V43() ext-real positive non negative V148() V149() V150() V151() V152() V153() Element of NAT
f is V15() V18( NAT ) V19( the U1 of (TOP-REAL 2)) Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
len f is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
i1 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
i1 + 1 is non empty V6() V10() V11() V12() V13() V28() V33() V43() ext-real positive non negative V148() V149() V150() V151() V152() V153() Element of NAT
f /^ i1 is V15() V18( NAT ) V19( the U1 of (TOP-REAL 2)) Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
mid (f,(i1 + 1),(len f)) is V15() V18( NAT ) V19( the U1 of (TOP-REAL 2)) Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
(i1 + 1) -' 1 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
f /^ ((i1 + 1) -' 1) is V15() V18( NAT ) V19( the U1 of (TOP-REAL 2)) Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
f is non empty set
i1 is V15() V18( NAT ) V19(f) Function-like V28() FinSequence-like FinSubsequence-like FinSequence of f
len i1 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
i2 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
g is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
mid (i1,g,i2) is V15() V18( NAT ) V19(f) Function-like V28() FinSequence-like FinSubsequence-like FinSequence of f
len (mid (i1,g,i2)) is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
i2 -' g is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
(i2 -' g) + 1 is non empty V6() V10() V11() V12() V13() V28() V33() V43() ext-real positive non negative V148() V149() V150() V151() V152() V153() Element of NAT
f is non empty set
i1 is V15() V18( NAT ) V19(f) Function-like V28() FinSequence-like FinSubsequence-like FinSequence of f
len i1 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
i2 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
g is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
mid (i1,i2,g) is V15() V18( NAT ) V19(f) Function-like V28() FinSequence-like FinSubsequence-like FinSequence of f
len (mid (i1,i2,g)) is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
i2 -' g is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
(i2 -' g) + 1 is non empty V6() V10() V11() V12() V13() V28() V33() V43() ext-real positive non negative V148() V149() V150() V151() V152() V153() Element of NAT
f is non empty set
i1 is V15() V18( NAT ) V19(f) Function-like V28() FinSequence-like FinSubsequence-like FinSequence of f
len i1 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
i2 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
g is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
mid (i1,i2,g) is V15() V18( NAT ) V19(f) Function-like V28() FinSequence-like FinSubsequence-like FinSequence of f
len (mid (i1,i2,g)) is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
(mid (i1,i2,g)) . (len (mid (i1,i2,g))) is set
i1 . g is set
g -' i2 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
(g -' i2) + 1 is non empty V6() V10() V11() V12() V13() V28() V33() V43() ext-real positive non negative V148() V149() V150() V151() V152() V153() Element of NAT
(len (mid (i1,i2,g))) + i2 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
((len (mid (i1,i2,g))) + i2) -' 1 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
i1 . (((len (mid (i1,i2,g))) + i2) -' 1) is set
((g -' i2) + 1) + i2 is non empty V6() V10() V11() V12() V13() V28() V33() V43() ext-real positive non negative V148() V149() V150() V151() V152() V153() Element of NAT
(((g -' i2) + 1) + i2) -' 1 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
i1 . ((((g -' i2) + 1) + i2) -' 1) is set
g - i2 is V11() V12() ext-real set
(g - i2) + 1 is V11() V12() ext-real Element of REAL
((g - i2) + 1) + i2 is V11() V12() ext-real Element of REAL
g + 1 is non empty V6() V10() V11() V12() V13() V28() V33() V43() ext-real positive non negative V148() V149() V150() V151() V152() V153() Element of NAT
f is non empty set
i1 is V15() V18( NAT ) V19(f) Function-like V28() FinSequence-like FinSubsequence-like FinSequence of f
len i1 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
i2 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
g is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
mid (i1,i2,g) is V15() V18( NAT ) V19(f) Function-like V28() FinSequence-like FinSubsequence-like FinSequence of f
len (mid (i1,i2,g)) is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
(mid (i1,i2,g)) . (len (mid (i1,i2,g))) is set
i1 . g is set
g - 1 is V11() V12() ext-real Element of REAL
i2 - (g - 1) is V11() V12() ext-real Element of REAL
i2 - 0 is V11() V12() ext-real non negative Element of REAL
i2 - g is V11() V12() ext-real set
(i2 - g) + 1 is V11() V12() ext-real Element of REAL
i2 -' g is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
(i2 -' g) + 1 is non empty V6() V10() V11() V12() V13() V28() V33() V43() ext-real positive non negative V148() V149() V150() V151() V152() V153() Element of NAT
i2 -' ((i2 -' g) + 1) is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
(i2 -' ((i2 -' g) + 1)) + 1 is non empty V6() V10() V11() V12() V13() V28() V33() V43() ext-real positive non negative V148() V149() V150() V151() V152() V153() Element of NAT
i2 - ((i2 -' g) + 1) is V11() V12() ext-real Element of REAL
(i2 - ((i2 -' g) + 1)) + 1 is V11() V12() ext-real Element of REAL
i2 - (i2 -' g) is V11() V12() ext-real set
i2 - (i2 - g) is V11() V12() ext-real set
i2 -' (len (mid (i1,i2,g))) is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
(i2 -' (len (mid (i1,i2,g)))) + 1 is non empty V6() V10() V11() V12() V13() V28() V33() V43() ext-real positive non negative V148() V149() V150() V151() V152() V153() Element of NAT
i1 . ((i2 -' (len (mid (i1,i2,g)))) + 1) is set
i1 . ((i2 -' ((i2 -' g) + 1)) + 1) is set
f is non empty set
i1 is V15() V18( NAT ) V19(f) Function-like V28() FinSequence-like FinSubsequence-like FinSequence of f
len i1 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
i2 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
g is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
i2 -' g is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
(i2 -' g) + 1 is non empty V6() V10() V11() V12() V13() V28() V33() V43() ext-real positive non negative V148() V149() V150() V151() V152() V153() Element of NAT
mid (i1,i2,g) is V15() V18( NAT ) V19(f) Function-like V28() FinSequence-like FinSubsequence-like FinSequence of f
g2 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
(mid (i1,i2,g)) . g2 is set
i2 -' g2 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
(i2 -' g2) + 1 is non empty V6() V10() V11() V12() V13() V28() V33() V43() ext-real positive non negative V148() V149() V150() V151() V152() V153() Element of NAT
i1 . ((i2 -' g2) + 1) is set
len (mid (i1,i2,g)) is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
0 + 1 is non empty V6() V10() V11() V12() V13() V28() V33() V43() ext-real positive non negative V148() V149() V150() V151() V152() V153() Element of NAT
g2 + i2 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
(g2 + i2) -' 1 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
1 + i2 is non empty V6() V10() V11() V12() V13() V28() V33() V43() ext-real positive non negative V148() V149() V150() V151() V152() V153() Element of NAT
(1 + i2) -' 1 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
(1 + i2) - 1 is V11() V12() ext-real Element of REAL
i2 - 1 is V11() V12() ext-real Element of REAL
(i2 - 1) + 1 is V11() V12() ext-real Element of REAL
i2 -' 1 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
(i2 -' 1) + 1 is non empty V6() V10() V11() V12() V13() V28() V33() V43() ext-real positive non negative V148() V149() V150() V151() V152() V153() Element of NAT
f is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
i1 is non empty set
i2 is V15() V18( NAT ) V19(i1) Function-like V28() FinSequence-like FinSubsequence-like FinSequence of i1
len i2 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
g is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
g2 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
g -' g2 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
(g -' g2) + 1 is non empty V6() V10() V11() V12() V13() V28() V33() V43() ext-real positive non negative V148() V149() V150() V151() V152() V153() Element of NAT
mid (i2,g,g2) is V15() V18( NAT ) V19(i1) Function-like V28() FinSequence-like FinSubsequence-like FinSequence of i1
(mid (i2,g,g2)) . f is set
mid (i2,g2,g) is V15() V18( NAT ) V19(i1) Function-like V28() FinSequence-like FinSubsequence-like FinSequence of i1
g - g2 is V11() V12() ext-real set
(g - g2) + 1 is V11() V12() ext-real Element of REAL
((g - g2) + 1) - f is V11() V12() ext-real Element of REAL
(((g - g2) + 1) - f) + 1 is V11() V12() ext-real Element of REAL
(mid (i2,g2,g)) . ((((g - g2) + 1) - f) + 1) is set
((g -' g2) + 1) -' f is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
(((g -' g2) + 1) -' f) + 1 is non empty V6() V10() V11() V12() V13() V28() V33() V43() ext-real positive non negative V148() V149() V150() V151() V152() V153() Element of NAT
g2 - 1 is V11() V12() ext-real Element of REAL
g - (g2 - 1) is V11() V12() ext-real Element of REAL
g - 0 is V11() V12() ext-real non negative Element of REAL
1 - f is V11() V12() ext-real Element of REAL
f - f is V11() V12() ext-real set
(g -' g2) + (1 - f) is V11() V12() ext-real Element of REAL
(g -' g2) + 0 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
((g -' g2) + 1) - f is V11() V12() ext-real Element of REAL
(((g -' g2) + 1) - f) + 1 is V11() V12() ext-real Element of REAL
len (mid (i2,g2,g)) is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
(mid (i2,g2,g)) . ((((g -' g2) + 1) -' f) + 1) is set
((((g -' g2) + 1) -' f) + 1) + g2 is non empty V6() V10() V11() V12() V13() V28() V33() V43() ext-real positive non negative V148() V149() V150() V151() V152() V153() Element of NAT
(((((g -' g2) + 1) -' f) + 1) + g2) -' 1 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
i2 . ((((((g -' g2) + 1) -' f) + 1) + g2) -' 1) is set
len (mid (i2,g,g2)) is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
(((((g -' g2) + 1) -' f) + 1) + g2) - 1 is V11() V12() ext-real Element of REAL
g - f is V11() V12() ext-real set
(g - f) + 1 is V11() V12() ext-real Element of REAL
g -' f is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
(g -' f) + 1 is non empty V6() V10() V11() V12() V13() V28() V33() V43() ext-real positive non negative V148() V149() V150() V151() V152() V153() Element of NAT
0 + 1 is non empty V6() V10() V11() V12() V13() V28() V33() V43() ext-real positive non negative V148() V149() V150() V151() V152() V153() Element of NAT
(0 + 1) - 1 is V11() V12() ext-real Element of REAL
((0 + 1) - 1) + 1 is V11() V12() ext-real Element of REAL
f is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
i1 is non empty set
i2 is V15() V18( NAT ) V19(i1) Function-like V28() FinSequence-like FinSubsequence-like FinSequence of i1
len i2 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
g is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
g2 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
g2 -' g is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
(g2 -' g) + 1 is non empty V6() V10() V11() V12() V13() V28() V33() V43() ext-real positive non negative V148() V149() V150() V151() V152() V153() Element of NAT
mid (i2,g,g2) is V15() V18( NAT ) V19(i1) Function-like V28() FinSequence-like FinSubsequence-like FinSequence of i1
(mid (i2,g,g2)) . f is set
mid (i2,g2,g) is V15() V18( NAT ) V19(i1) Function-like V28() FinSequence-like FinSubsequence-like FinSequence of i1
g2 - g is V11() V12() ext-real set
(g2 - g) + 1 is V11() V12() ext-real Element of REAL
((g2 - g) + 1) - f is V11() V12() ext-real Element of REAL
(((g2 - g) + 1) - f) + 1 is V11() V12() ext-real Element of REAL
(mid (i2,g2,g)) . ((((g2 - g) + 1) - f) + 1) is set
((g2 -' g) + 1) -' f is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
(((g2 -' g) + 1) -' f) + 1 is non empty V6() V10() V11() V12() V13() V28() V33() V43() ext-real positive non negative V148() V149() V150() V151() V152() V153() Element of NAT
((g2 -' g) + 1) - f is V11() V12() ext-real Element of REAL
(((g2 -' g) + 1) - f) + 1 is V11() V12() ext-real Element of REAL
((g2 - g) + 1) - ((((g2 -' g) + 1) -' f) + 1) is V11() V12() ext-real Element of REAL
(((g2 - g) + 1) - ((((g2 -' g) + 1) -' f) + 1)) + 1 is V11() V12() ext-real Element of REAL
f - 1 is V11() V12() ext-real Element of REAL
((((g2 -' g) + 1) -' f) + 1) + 0 is non empty V6() V10() V11() V12() V13() V28() V33() V43() ext-real positive non negative V148() V149() V150() V151() V152() V153() Element of NAT
((((g2 -' g) + 1) -' f) + 1) + (f - 1) is V11() V12() ext-real Element of REAL
f is non empty set
i1 is V15() V18( NAT ) V19(f) Function-like V28() FinSequence-like FinSubsequence-like FinSequence of f
len i1 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
i2 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
mid (i1,i2,i2) is V15() V18( NAT ) V19(f) Function-like V28() FinSequence-like FinSubsequence-like FinSequence of f
i1 /. i2 is Element of f
<*(i1 /. i2)*> is non empty V2() V15() V18( NAT ) V19(f) Function-like V28() V35(1) FinSequence-like FinSubsequence-like FinSequence of f
len (mid (i1,i2,i2)) is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
i1 . i2 is set
i2 -' 1 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
(i2 -' 1) + 1 is non empty V6() V10() V11() V12() V13() V28() V33() V43() ext-real positive non negative V148() V149() V150() V151() V152() V153() Element of NAT
((i2 -' 1) + 1) - (i2 -' 1) is V11() V12() ext-real Element of REAL
(len i1) - (i2 -' 1) is V11() V12() ext-real Element of REAL
i1 /^ (i2 -' 1) is V15() V18( NAT ) V19(f) Function-like V28() FinSequence-like FinSubsequence-like FinSequence of f
len (i1 /^ (i2 -' 1)) is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
(len i1) -' (i2 -' 1) is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
(i1 /^ (i2 -' 1)) . 1 is set
i2 -' i2 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
(i2 -' i2) + 1 is non empty V6() V10() V11() V12() V13() V28() V33() V43() ext-real positive non negative V148() V149() V150() V151() V152() V153() Element of NAT
i2 - i2 is V11() V12() ext-real set
(i2 - i2) + 1 is V11() V12() ext-real Element of REAL
(i1 /^ (i2 -' 1)) | 1 is V15() V18( NAT ) V19(f) Function-like V28() FinSequence-like FinSubsequence-like FinSequence of f
(i1 /^ (i2 -' 1)) /. 1 is Element of f
<*((i1 /^ (i2 -' 1)) /. 1)*> is non empty V2() V15() V18( NAT ) V19(f) Function-like V28() V35(1) FinSequence-like FinSubsequence-like FinSequence of f
f is non empty set
i1 is V15() V18( NAT ) V19(f) Function-like V28() FinSequence-like FinSubsequence-like FinSequence of f
mid (i1,0,0) is V15() V18( NAT ) V19(f) Function-like V28() FinSequence-like FinSubsequence-like FinSequence of f
i1 | 1 is V15() V18( NAT ) V19(f) Function-like V28() FinSequence-like FinSubsequence-like FinSequence of f
0 - 1 is non empty V11() V12() ext-real non positive negative Element of REAL
0 -' 1 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
0 -' 0 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
(0 -' 0) + 1 is non empty V6() V10() V11() V12() V13() V28() V33() V43() ext-real positive non negative V148() V149() V150() V151() V152() V153() Element of NAT
0 - 0 is empty V6() V11() V12() functional V33() V35( {} ) FinSequence-membered ext-real non positive non negative V148() V149() V150() V151() V152() V153() V154() Element of REAL
(0 - 0) + 1 is non empty V11() V12() ext-real positive non negative Element of REAL
i1 /^ (0 -' 1) is V15() V18( NAT ) V19(f) Function-like V28() FinSequence-like FinSubsequence-like FinSequence of f
(i1 /^ (0 -' 1)) | 1 is V15() V18( NAT ) V19(f) Function-like V28() FinSequence-like FinSubsequence-like FinSequence of f
f is non empty set
<*> f is empty V6() V10() V11() V12() V15() V18( NAT ) V19(f) Function-like functional V28() V33() V35( {} ) FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V148() V149() V150() V151() V152() V153() V154() FinSequence of f
i1 is V15() V18( NAT ) V19(f) Function-like V28() FinSequence-like FinSubsequence-like FinSequence of f
len i1 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
i2 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
mid (i1,i2,i2) is V15() V18( NAT ) V19(f) Function-like V28() FinSequence-like FinSubsequence-like FinSequence of f
(len i1) + 1 is non empty V6() V10() V11() V12() V13() V28() V33() V43() ext-real positive non negative V148() V149() V150() V151() V152() V153() Element of NAT
((len i1) + 1) - 1 is V11() V12() ext-real Element of REAL
i2 - 1 is V11() V12() ext-real Element of REAL
0 + 1 is non empty V6() V10() V11() V12() V13() V28() V33() V43() ext-real positive non negative V148() V149() V150() V151() V152() V153() Element of NAT
i2 -' 1 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
i1 /^ (i2 -' 1) is V15() V18( NAT ) V19(f) Function-like V28() FinSequence-like FinSubsequence-like FinSequence of f
i2 -' i2 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
(i2 -' i2) + 1 is non empty V6() V10() V11() V12() V13() V28() V33() V43() ext-real positive non negative V148() V149() V150() V151() V152() V153() Element of NAT
i2 - i2 is V11() V12() ext-real set
(i2 - i2) + 1 is V11() V12() ext-real Element of REAL
(i1 /^ (i2 -' 1)) | 1 is V15() V18( NAT ) V19(f) Function-like V28() FinSequence-like FinSubsequence-like FinSequence of f
f is non empty set
i1 is V15() V18( NAT ) V19(f) Function-like V28() FinSequence-like FinSubsequence-like FinSequence of f
i2 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
g is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
mid (i1,i2,g) is V15() V18( NAT ) V19(f) Function-like V28() FinSequence-like FinSubsequence-like FinSequence of f
mid (i1,g,i2) is V15() V18( NAT ) V19(f) Function-like V28() FinSequence-like FinSubsequence-like FinSequence of f
Rev (mid (i1,g,i2)) is V15() V18( NAT ) V19(f) Function-like V28() FinSequence-like FinSubsequence-like FinSequence of f
g -' i2 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
(g -' i2) + 1 is non empty V6() V10() V11() V12() V13() V28() V33() V43() ext-real positive non negative V148() V149() V150() V151() V152() V153() Element of NAT
i2 -' 1 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
i1 /^ (i2 -' 1) is V15() V18( NAT ) V19(f) Function-like V28() FinSequence-like FinSubsequence-like FinSequence of f
(i1 /^ (i2 -' 1)) | ((g -' i2) + 1) is V15() V18( NAT ) V19(f) Function-like V28() FinSequence-like FinSubsequence-like FinSequence of f
Rev (mid (i1,i2,g)) is V15() V18( NAT ) V19(f) Function-like V28() FinSequence-like FinSubsequence-like FinSequence of f
0 + 1 is non empty V6() V10() V11() V12() V13() V28() V33() V43() ext-real positive non negative V148() V149() V150() V151() V152() V153() Element of NAT
i1 | 1 is V15() V18( NAT ) V19(f) Function-like V28() FinSequence-like FinSubsequence-like FinSequence of f
len i1 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
<*> f is empty V6() V10() V11() V12() V15() V18( NAT ) V19(f) Function-like functional V28() V33() V35( {} ) FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V148() V149() V150() V151() V152() V153() V154() FinSequence of f
len i1 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
<*> f is empty V6() V10() V11() V12() V15() V18( NAT ) V19(f) Function-like functional V28() V33() V35( {} ) FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V148() V149() V150() V151() V152() V153() V154() FinSequence of f
i1 /. 1 is Element of f
<*(i1 /. 1)*> is non empty V2() V15() V18( NAT ) V19(f) Function-like V28() V35(1) FinSequence-like FinSubsequence-like FinSequence of f
len i1 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
len i1 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
len i1 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
mid (i1,i2,i2) is V15() V18( NAT ) V19(f) Function-like V28() FinSequence-like FinSubsequence-like FinSequence of f
i1 /. i2 is Element of f
<*(i1 /. i2)*> is non empty V2() V15() V18( NAT ) V19(f) Function-like V28() V35(1) FinSequence-like FinSubsequence-like FinSequence of f
len i1 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
mid (i1,i2,i2) is V15() V18( NAT ) V19(f) Function-like V28() FinSequence-like FinSubsequence-like FinSequence of f
<*> f is empty V6() V10() V11() V12() V15() V18( NAT ) V19(f) Function-like functional V28() V33() V35( {} ) FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V148() V149() V150() V151() V152() V153() V154() FinSequence of f
len i1 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
len i1 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
i2 -' g is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
(i2 -' g) + 1 is non empty V6() V10() V11() V12() V13() V28() V33() V43() ext-real positive non negative V148() V149() V150() V151() V152() V153() Element of NAT
g -' 1 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
i1 /^ (g -' 1) is V15() V18( NAT ) V19(f) Function-like V28() FinSequence-like FinSubsequence-like FinSequence of f
(i1 /^ (g -' 1)) | ((i2 -' g) + 1) is V15() V18( NAT ) V19(f) Function-like V28() FinSequence-like FinSubsequence-like FinSequence of f
Rev ((i1 /^ (g -' 1)) | ((i2 -' g) + 1)) is V15() V18( NAT ) V19(f) Function-like V28() FinSequence-like FinSubsequence-like FinSequence of f
f is V15() V18( NAT ) V19( the U1 of (TOP-REAL 2)) Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
len f is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
i1 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
i2 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
i2 -' i1 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
(i2 -' i1) + 1 is non empty V6() V10() V11() V12() V13() V28() V33() V43() ext-real positive non negative V148() V149() V150() V151() V152() V153() Element of NAT
mid (f,i1,i2) is V15() V18( NAT ) V19( the U1 of (TOP-REAL 2)) Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
g is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
LSeg ((mid (f,i1,i2)),g) is Element of K6( the U1 of (TOP-REAL 2))
g + i1 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
(g + i1) -' 1 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
LSeg (f,((g + i1) -' 1)) is Element of K6( the U1 of (TOP-REAL 2))
((g + i1) -' 1) + 1 is non empty V6() V10() V11() V12() V13() V28() V33() V43() ext-real positive non negative V148() V149() V150() V151() V152() V153() Element of NAT
(g + i1) - 1 is V11() V12() ext-real Element of REAL
((g + i1) - 1) + 1 is V11() V12() ext-real Element of REAL
g + 1 is non empty V6() V10() V11() V12() V13() V28() V33() V43() ext-real positive non negative V148() V149() V150() V151() V152() V153() Element of NAT
(g + 1) + i1 is non empty V6() V10() V11() V12() V13() V28() V33() V43() ext-real positive non negative V148() V149() V150() V151() V152() V153() Element of NAT
((g + 1) + i1) - 1 is V11() V12() ext-real Element of REAL
((g + 1) + i1) -' 1 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
i2 - i1 is V11() V12() ext-real set
(i2 - i1) + 1 is V11() V12() ext-real Element of REAL
((i2 - i1) + 1) + i1 is V11() V12() ext-real Element of REAL
(g + i1) + 1 is non empty V6() V10() V11() V12() V13() V28() V33() V43() ext-real positive non negative V148() V149() V150() V151() V152() V153() Element of NAT
((g + i1) + 1) - 1 is V11() V12() ext-real Element of REAL
i2 + 1 is non empty V6() V10() V11() V12() V13() V28() V33() V43() ext-real positive non negative V148() V149() V150() V151() V152() V153() Element of NAT
(i2 + 1) - 1 is V11() V12() ext-real Element of REAL
1 + 1 is non empty V6() V10() V11() V12() V13() V28() V33() V43() ext-real positive non negative V148() V149() V150() V151() V152() V153() Element of NAT
(1 + 1) - 1 is V11() V12() ext-real Element of REAL
f /. ((g + i1) -' 1) is V35(2) FinSequence-like V140() Element of the U1 of (TOP-REAL 2)
f /. (((g + i1) -' 1) + 1) is V35(2) FinSequence-like V140() Element of the U1 of (TOP-REAL 2)
LSeg ((f /. ((g + i1) -' 1)),(f /. (((g + i1) -' 1) + 1))) is Element of K6( the U1 of (TOP-REAL 2))
{ (((1 - b₁) * (f /. ((g + i1) -' 1))) + (b₁ * (f /. (((g + i1) -' 1) + 1)))) where b₁ is V11() V12() ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
1 + g is non empty V6() V10() V11() V12() V13() V28() V33() V43() ext-real positive non negative V148() V149() V150() V151() V152() V153() Element of NAT
len (mid (f,i1,i2)) is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
(mid (f,i1,i2)) /. g is V35(2) FinSequence-like V140() Element of the U1 of (TOP-REAL 2)
(mid (f,i1,i2)) . g is set
f . ((g + i1) -' 1) is set
(mid (f,i1,i2)) /. (g + 1) is V35(2) FinSequence-like V140() Element of the U1 of (TOP-REAL 2)
(mid (f,i1,i2)) . (g + 1) is set
f . (((g + 1) + i1) -' 1) is set
f /. (((g + 1) + i1) -' 1) is V35(2) FinSequence-like V140() Element of the U1 of (TOP-REAL 2)
f is V15() V18( NAT ) V19( the U1 of (TOP-REAL 2)) Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
len f is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
i1 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
i2 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
i2 -' i1 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
(i2 -' i1) + 1 is non empty V6() V10() V11() V12() V13() V28() V33() V43() ext-real positive non negative V148() V149() V150() V151() V152() V153() Element of NAT
mid (f,i2,i1) is V15() V18( NAT ) V19( the U1 of (TOP-REAL 2)) Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
g is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
LSeg ((mid (f,i2,i1)),g) is Element of K6( the U1 of (TOP-REAL 2))
i2 -' g is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
LSeg (f,(i2 -' g)) is Element of K6( the U1 of (TOP-REAL 2))
len (mid (f,i2,i1)) is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
g + 1 is non empty V6() V10() V11() V12() V13() V28() V33() V43() ext-real positive non negative V148() V149() V150() V151() V152() V153() Element of NAT
(g + 1) - g is V11() V12() ext-real Element of REAL
(len (mid (f,i2,i1))) - g is V11() V12() ext-real Element of REAL
(len (mid (f,i2,i1))) -' g is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
i1 -' 1 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
i2 + (i1 -' 1) is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
i1 - 1 is V11() V12() ext-real Element of REAL
i2 + (i1 - 1) is V11() V12() ext-real Element of REAL
i2 - (i1 - 1) is V11() V12() ext-real Element of REAL
(i2 + (i1 - 1)) - (i1 - 1) is V11() V12() ext-real Element of REAL
i2 - i1 is V11() V12() ext-real set
(i2 - i1) + 1 is V11() V12() ext-real Element of REAL
((i2 -' i1) + 1) -' g is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
(((i2 -' i1) + 1) -' g) + i1 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
((((i2 -' i1) + 1) -' g) + i1) -' 1 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
((((i2 -' i1) + 1) -' g) + i1) - 1 is V11() V12() ext-real Element of REAL
((i2 -' i1) + 1) - g is V11() V12() ext-real Element of REAL
(((i2 -' i1) + 1) - g) + i1 is V11() V12() ext-real Element of REAL
((((i2 -' i1) + 1) - g) + i1) - 1 is V11() V12() ext-real Element of REAL
(i2 -' i1) - g is V11() V12() ext-real set
((i2 -' i1) - g) + i1 is V11() V12() ext-real set
(i2 - i1) - g is V11() V12() ext-real set
((i2 - i1) - g) + i1 is V11() V12() ext-real set
i2 - g is V11() V12() ext-real set
(len (mid (f,i2,i1))) + 1 is non empty V6() V10() V11() V12() V13() V28() V33() V43() ext-real positive non negative V148() V149() V150() V151() V152() V153() Element of NAT
(len (mid (f,i2,i1))) + g is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
((len (mid (f,i2,i1))) + g) - g is V11() V12() ext-real Element of REAL
g + ((len (mid (f,i2,i1))) -' g) is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
Rev (mid (f,i2,i1)) is V15() V18( NAT ) V19( the U1 of (TOP-REAL 2)) Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
LSeg ((Rev (mid (f,i2,i1))),((len (mid (f,i2,i1))) -' g)) is Element of K6( the U1 of (TOP-REAL 2))
mid (f,i1,i2) is V15() V18( NAT ) V19( the U1 of (TOP-REAL 2)) Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
LSeg ((mid (f,i1,i2)),((len (mid (f,i2,i1))) -' g)) is Element of K6( the U1 of (TOP-REAL 2))
((len (mid (f,i2,i1))) -' g) + i1 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
(((len (mid (f,i2,i1))) -' g) + i1) -' 1 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
LSeg (f,((((len (mid (f,i2,i1))) -' g) + i1) -' 1)) is Element of K6( the U1 of (TOP-REAL 2))
f is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
i1 is V15() V18( NAT ) Function-like V28() FinSequence-like FinSubsequence-like set
len i1 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
(len i1) -' 1 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
f mod ((len i1) -' 1) is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
f is V15() V18( NAT ) Function-like V28() FinSequence-like FinSubsequence-like set
len f is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
(len f) -' 1 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
(((len f) -' 1),f) is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
((len f) -' 1) mod ((len f) -' 1) is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
f is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
i1 is V15() V18( NAT ) Function-like V28() FinSequence-like FinSubsequence-like set
len i1 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
(len i1) -' 1 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
(f,i1) is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
f mod ((len i1) -' 1) is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
f is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
i1 is V15() V18( NAT ) Function-like V28() FinSequence-like FinSubsequence-like set
(f,i1) is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
len i1 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
(len i1) -' 1 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
f + ((len i1) -' 1) is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
((f + ((len i1) -' 1)),i1) is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
((len i1) -' 1) + f is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
((((len i1) -' 1) + f),i1) is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
(f + ((len i1) -' 1)) mod ((len i1) -' 1) is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
((len i1) -' 1) * 1 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
f + (((len i1) -' 1) * 1) is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
(f + (((len i1) -' 1) * 1)) mod ((len i1) -' 1) is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
f mod ((len i1) -' 1) is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
f is non empty V15() V18( NAT ) V19( the U1 of (TOP-REAL 2)) Function-like non constant V28() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)
len f is non empty V6() V10() V11() V12() V13() V28() V33() V43() ext-real positive non negative V148() V149() V150() V151() V152() V153() Element of NAT
i1 is V15() V18( NAT ) V19( the U1 of (TOP-REAL 2)) Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
len i1 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
i1 . (len i1) is set
i2 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
g is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
i2 + 1 is non empty V6() V10() V11() V12() V13() V28() V33() V43() ext-real positive non negative V148() V149() V150() V151() V152() V153() Element of NAT
g + 1 is non empty V6() V10() V11() V12() V13() V28() V33() V43() ext-real positive non negative V148() V149() V150() V151() V152() V153() Element of NAT
f . g is set
(len f) + i2 is non empty V6() V10() V11() V12() V13() V28() V33() V43() ext-real positive non negative V148() V149() V150() V151() V152() V153() Element of NAT
g2 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
i1 . g2 is set
i2 + g2 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
(i2 + g2) -' 1 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
(((i2 + g2) -' 1),f) is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
f . (((i2 + g2) -' 1),f) is set
g2 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
i1 . g2 is set
((len f) + i2) -' g2 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
((((len f) + i2) -' g2),f) is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
f . ((((len f) + i2) -' g2),f) is set
g2 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
i1 . g2 is set
i2 + g2 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
(i2 + g2) -' 1 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
(((i2 + g2) -' 1),f) is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
f . (((i2 + g2) -' 1),f) is set
g2 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
i1 . g2 is set
((len f) + i2) -' g2 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
((((len f) + i2) -' g2),f) is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
f . ((((len f) + i2) -' g2),f) is set
g2 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
i1 . g2 is set
i2 + g2 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
(i2 + g2) -' 1 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
(((i2 + g2) -' 1),f) is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
f . (((i2 + g2) -' 1),f) is set
g2 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
i1 . g2 is set
((len f) + i2) -' g2 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
((((len f) + i2) -' g2),f) is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
f . ((((len f) + i2) -' g2),f) is set
f is non empty V15() V18( NAT ) V19( the U1 of (TOP-REAL 2)) Function-like non constant V28() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)
i1 is V15() V18( NAT ) V19( the U1 of (TOP-REAL 2)) Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
len i1 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
i2 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
g is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
g -' i2 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
(g -' i2) + 1 is non empty V6() V10() V11() V12() V13() V28() V33() V43() ext-real positive non negative V148() V149() V150() V151() V152() V153() Element of NAT
mid (f,i2,g) is V15() V18( NAT ) V19( the U1 of (TOP-REAL 2)) Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
i2 + 1 is non empty V6() V10() V11() V12() V13() V28() V33() V43() ext-real positive non negative V148() V149() V150() V151() V152() V153() Element of NAT
len f is non empty V6() V10() V11() V12() V13() V28() V33() V43() ext-real positive non negative V148() V149() V150() V151() V152() V153() Element of NAT
(i2 + 1) - 1 is V11() V12() ext-real Element of REAL
(len f) - 1 is V11() V12() ext-real Element of REAL
(len f) -' 1 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
i2 + (len i1) is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
(i2 + (len i1)) -' 1 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
((i2 + (len i1)) -' 1) mod ((len f) -' 1) is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
(((i2 + (len i1)) -' 1),f) is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
i2 + (len i1) is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
(i2 + (len i1)) -' 1 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
((i2 + (len i1)) -' 1) mod ((len f) -' 1) is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
(((i2 + (len i1)) -' 1),f) is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
i2 + (len i1) is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
(i2 + (len i1)) -' 1 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
((i2 + (len i1)) -' 1) mod ((len f) -' 1) is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
(((i2 + (len i1)) -' 1),f) is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
i2 + (len i1) is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
(i2 + (len i1)) -' 1 is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
((i2 + (len i1)) -' 1) mod ((len f) -' 1) is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
(((i2 + (len i1)) -' 1),f) is V6() V10() V11() V12() V13() V28() V33() V43() ext-real non negative V148() V149() V150() V151() V152() V153() Element of NAT
i1 . (len i1) is set
f . g is set
f . (((i2 + (len i1)) -' 1),f) is set
g + 1 is non empty V6() V10() V11() V12() V13() V28() V33() V43() ext-real positive non negative V148() V149() V150() V151() V152() V153() Element of NAT
0 + 1 is non empty V6() V10() V11() V12() V13() V28() V33() V43() ext-real positive non negative V148() V149() V150() V151() V152() V153() Element of NAT
f /. g is V35(2) FinSequence-like V140() Element of the U1 of (TOP-REAL 2)
f /. (((i2 + (len i1)) -' 1),f) is V35(2) FinSequence-like V140() Element of the U1 of (TOP-REAL 2)
f /. g is V35(2) FinSequence-like V140() Element of the U1 of (TOP-REAL 2)
f /. (((i2 + (len i1)) -' 1),f) is V35(2) FinSequence-like V140() Element of the U1 of (TOP-REAL 2)
g2 is V6() V10() V11() V12() V28() V33() ext-real non negative set
((len f) -' 1) * g2 is V6() V10()