environ
vocabularies HIDDEN, FINSEQ_8, ARYTM_1, RELAT_1, FINSEQ_1, FUNCT_1, FINSEQ_5, RFINSEQ, JORDAN3, ARYTM_3, NUMBERS, ORDINAL4, TARSKI, XBOOLE_0, XXREAL_0, CARD_1, SUBSET_1, NAT_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, NAT_1, NAT_D, RELAT_1, RFINSEQ, FINSEQ_1, FUNCT_1, FINSEQ_6, FINSEQ_5;
definitions ;
theorems NAT_1, NAT_2, FINSEQ_1, FINSEQ_3, FINSEQ_5, FINSEQ_6, RFINSEQ, RELAT_1, XREAL_1, XBOOLE_1, XXREAL_0, ORDINAL1, XREAL_0, NAT_D;
schemes NAT_1;
registrations RELSET_1, XXREAL_0, XREAL_0, NAT_1, FINSEQ_1, ORDINAL1, XBOOLE_0, CARD_1;
constructors HIDDEN, SQUARE_1, NAT_1, RFINSEQ, NAT_D, FINSEQ_5, FINSEQ_6, REAL_1;
requirements HIDDEN, NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
equalities FINSEQ_1;
expansions FINSEQ_1;
definition
let D be non
empty set ;
let f,
g be
FinSequence of
D;
existence
ex b1 being FinSequence of D st
( len b1 <= len g & b1 = smid (g,1,(len b1)) & b1 = smid (f,(((len f) -' (len b1)) + 1),(len f)) & ( for j being Nat st j <= len g & smid (g,1,j) = smid (f,(((len f) -' j) + 1),(len f)) holds
j <= len b1 ) )
uniqueness
for b1, b2 being FinSequence of D st len b1 <= len g & b1 = smid (g,1,(len b1)) & b1 = smid (f,(((len f) -' (len b1)) + 1),(len f)) & ( for j being Nat st j <= len g & smid (g,1,j) = smid (f,(((len f) -' j) + 1),(len f)) holds
j <= len b1 ) & len b2 <= len g & b2 = smid (g,1,(len b2)) & b2 = smid (f,(((len f) -' (len b2)) + 1),(len f)) & ( for j being Nat st j <= len g & smid (g,1,j) = smid (f,(((len f) -' j) + 1),(len f)) holds
j <= len b2 ) holds
b1 = b2
end;
::
deftheorem Def2 defines
ovlpart FINSEQ_8:def 2 :
for D being non empty set
for f, g, b4 being FinSequence of D holds
( b4 = ovlpart (f,g) iff ( len b4 <= len g & b4 = smid (g,1,(len b4)) & b4 = smid (f,(((len f) -' (len b4)) + 1),(len f)) & ( for j being Nat st j <= len g & smid (g,1,j) = smid (f,(((len f) -' j) + 1),(len f)) holds
j <= len b4 ) ) );