List of theorems referencing the symbol SHIFT

(373) Theorem 322: [The shift-map of an integer is single-valued and maps Za into Za] ((M in Za) & (N in Za)) •imp (Svm(Shift(M)) & (domain(Shift(M)) = Za) & (range(Shift(M)) •incin Za) & (Shift(M)~[N] = M •PLUS N))
(374) Theorem 323: [Composition of shift-maps yields a shift-map] ((M in Za) & (N in Za)) •imp (Shift(M) @ Shift(N) = Shift(M •PLUS N))
(376) Theorem 325: [Shift(0) is the identity map on Za] (Shift(0) = {[n,n]: n in Za}) & ((Is_map(F) & (domain(F) •incin Za)) •imp (F @ Shift(0) = F))