:: Construction of Finite Sequences over Ring and Left-, Right-,
:: and Bi-Modules over a Ring
:: by Micha{\l} Muzalewski and Les{\l}aw W. Szczerba
::
:: Received September 13, 1990
:: Copyright (c) 1990-2017 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, NAT_1, CARD_1, ARYTM_3, XBOOLE_0, XXREAL_0, TARSKI,
STRUCT_0, FUNCT_1, SUPINF_2, FUNCOP_1, SUBSET_1, FINSEQ_1, RELAT_1,
AFINSQ_1, ALGSEQ_1, POLYNOM1, FINSET_1;
notations TARSKI, XBOOLE_0, SUBSET_1, CARD_1, FINSET_1, ORDINAL1, NUMBERS,
MEMBERED, XCMPLX_0, NAT_1, XXREAL_2, RELAT_1, FUNCT_1, FUNCOP_1,
STRUCT_0, FUNCT_2, XXREAL_0, POLYNOM1;
constructors FUNCOP_1, XXREAL_0, XREAL_0, NAT_1, RLVECT_1, RELSET_1, POLYNOM1,
XXREAL_2;
registrations ORDINAL1, RELSET_1, XREAL_0, STRUCT_0, FINSET_1, CARD_1,
XXREAL_2, MEMBERED;
requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
begin
reserve i,k,l,m,n for Nat,
x for set;
::
:: Algebraic Sequences
::
reserve R for non empty ZeroStr;
definition
let R;
let F be sequence of R;
redefine attr F is finite-Support means
:: ALGSEQ_1:def 1
ex n st for i st i >= n holds F.i = 0. R;
end;
registration
let R;
cluster finite-Support for sequence of R;
end;
definition
let R;
mode AlgSequence of R is finite-Support sequence of R;
end;
reserve p,q for AlgSequence of R;
definition
let R,p;
let k be Nat;
pred k is_at_least_length_of p means
:: ALGSEQ_1:def 2
for i st i>=k holds p.i=0.R;
end;
definition
let R,p;
func len p -> Element of NAT means
:: ALGSEQ_1:def 3
it is_at_least_length_of p & for m st m is_at_least_length_of p holds it<=m;
end;
::$CT 7
theorem :: ALGSEQ_1:8
i>=len p implies p.i=0.R;
theorem :: ALGSEQ_1:9
(for i st i < k holds p.i<>0.R) implies len p>=k;
theorem :: ALGSEQ_1:10
len p=k+1 implies p.k<>0.R;
scheme :: ALGSEQ_1:sch 1
AlgSeqLambdaF{R()->non empty ZeroStr,A()->Nat, F(Nat)->Element of R()}: ex p
being AlgSequence of R() st len p <= A() & for k st k < A() holds p.k=F(k);
::$CT
theorem :: ALGSEQ_1:12
len p = len q & (for k st k < len p holds p.k = q.k) implies p=q;
theorem :: ALGSEQ_1:13
the carrier of R <> {0.R} implies for k ex p being AlgSequence of R st
len p = k;
::
:: The Short AlgSequence of R
::
reserve x for Element of R;
definition
::$CD
let R,x;
func <%x%> -> AlgSequence of R means
:: ALGSEQ_1:def 5
len it <= 1 & it.0 = x;
end;
theorem :: ALGSEQ_1:14
p=<%0.R%> iff len p = 0;
::$CT
theorem :: ALGSEQ_1:16
<%0.R%>.i=0.R;
theorem :: ALGSEQ_1:17
p=<%0.R%> iff rng p = {0.R};