Update
This commit is contained in:
parent
73e23b3b2a
commit
646f516c8c
718
thue-morse.v
718
thue-morse.v
@ -1,683 +1,6 @@
|
|||||||
(*
|
(*
|
||||||
|
https://oeis.org/A010060
|
||||||
A010060 Thue-Morse sequence: let A_k denote the first 2^k terms; then A_0 = 0 and for k >= 0, A_{k+1} 541
|
https://en.wikipedia.org/wiki/Thue%E2%80%93Morse_sequence
|
||||||
= A_k B_k, where B_k is obtained from A_k by interchanging 0's and 1's.
|
|
||||||
0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0,
|
|
||||||
1, 0, 1, 1, 0, 0, 1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 1,
|
|
||||||
1, 0, 0, 1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1, 0, 1, 1, 0, 0, 1, 1, 0, 1, 0, 0, 1, 1
|
|
||||||
(list; graph; refs; listen; history; text; internal format)
|
|
||||||
OFFSET 0,1
|
|
||||||
COMMENTS Named after Axel Thue, whose name is pronounced as if it were spelled "Tü" where the ü sound
|
|
||||||
is roughly as in the German word üben. (It is incorrect to say "Too-ee" or "Too-eh".) - N. J.
|
|
||||||
A. Sloane, Jun 12 2018
|
|
||||||
|
|
||||||
Also called the Thue-Morse infinite word, or the Morse-Hedlund sequence, or the parity
|
|
||||||
sequence.
|
|
||||||
|
|
||||||
Fixed point of the morphism 0 --> 01, 1 --> 10, see example. - Joerg Arndt, Mar 12 2013
|
|
||||||
|
|
||||||
The sequence is cubefree (does not contain three consecutive identical blocks) [see Offner for
|
|
||||||
a direct proof] and is overlap-free (does not contain XYXYX where X is 0 or 1 and Y is any
|
|
||||||
string of 0's and 1's).
|
|
||||||
|
|
||||||
a(n) = "parity sequence" = parity of number of 1's in binary representation of n.
|
|
||||||
|
|
||||||
To construct the sequence: alternate blocks of 0's and 1's of successive lengths A003159(k) -
|
|
||||||
A003159(k-1), k = 1, 2, 3, ... (A003159(0) = 0). Example: since the first seven differences of
|
|
||||||
A003159 are 1, 2, 1, 1, 2, 2, 2, the sequence starts with 0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0. -
|
|
||||||
Emeric Deutsch, Jan 10 2003
|
|
||||||
|
|
||||||
Characteristic function of A000069 (odious numbers). - Ralf Stephan, Jun 20 2003
|
|
||||||
|
|
||||||
a(n) = S2(n) mod 2, where S2(n) = sum of digits of n, n in base-2 notation. There is a class
|
|
||||||
of generalized Thue-Morse sequences: Let Sk(n) = sum of digits of n; n in base-k notation. Let
|
|
||||||
F(t) be some arithmetic function. Then a(n)= F(Sk(n)) mod m is a generalized Thue-Morse
|
|
||||||
sequence. The classical Thue-Morse sequence is the case k=2, m=2, F(t)= 1*t. - Ctibor O.
|
|
||||||
Zizka, Feb 12 2008 (with correction from Daniel Hug, May 19 2017)
|
|
||||||
|
|
||||||
More generally, the partial sums of the generalized Thue-Morse sequences a(n) = F(Sk(n)) mod m
|
|
||||||
are fractal, where Sk(n) is sum of digits of n, n in base k; F(t) is an arithmetic function; m
|
|
||||||
integer. - Ctibor O. Zizka, Feb 25 2008
|
|
||||||
|
|
||||||
Starting with offset 1, = running sums mod 2 of the kneading sequence (A035263, 1, 0, 1, 1, 1,
|
|
||||||
0, 1, 0, 1, 0, 1, 1, 1, ...); also parity of A005187: (1, 3, 4, 7, 8, 10, 11, 15, 16, 18, 19,
|
|
||||||
...). - Gary W. Adamson, Jun 15 2008
|
|
||||||
|
|
||||||
Generalized Thue-Morse sequences mod n (n>1) = the array shown in A141803. As n -> infinity
|
|
||||||
the sequences -> (1, 2, 3, ...). - Gary W. Adamson, Jul 10 2008
|
|
||||||
|
|
||||||
The Thue-Morse sequence for N = 3 = A053838, (sum of digits of n in base 3, mod 3): (0, 1, 2,
|
|
||||||
1, 2, 0, 2, 0, 1, 1, 2, ...) = A004128 mod 3. - Gary W. Adamson, Aug 24 2008
|
|
||||||
|
|
||||||
For all positive integers k, the subsequence a(0) to a(2^k-1) is identical to the subsequence
|
|
||||||
a(2^k+2^(k-1)) to a(2^(k+1)+2^(k-1)-1). That is to say, the first half of A_k is identical to
|
|
||||||
the second half of B_k, and the second half of A_k is identical to the first quarter of
|
|
||||||
B_{k+1}, which consists of the k/2 terms immediately following B_k.
|
|
||||||
|
|
||||||
Proof: The subsequence a(2^k+2^(k-1)) to a(2^(k+1)-1), the second half of B_k, is by
|
|
||||||
definition formed from the subsequence a(2^(k-1)) to a(2^k-1), the second half of A_k, by
|
|
||||||
interchanging its 0's and 1's. In turn, the subsequence a(2^(k-1)) to a(2^k-1), the second
|
|
||||||
half of A_k, which is by definition also B_{k-1}, is by definition formed from the subsequence
|
|
||||||
a(0) to a(2^(k-1)-1), the first half of A_k, which is by definition also A_{k-1}, by
|
|
||||||
interchanging its 0's and 1's. Interchanging the 0's and 1's of a subsequence twice leaves it
|
|
||||||
unchanged, so the subsequence a(2^k+2^(k-1)) to a(2^(k+1)-1), the second half of B_k, must be
|
|
||||||
identical to the subsequence a(0) to a(2^(k-1)-1), the first half of A_k.
|
|
||||||
|
|
||||||
Also, the subsequence a(2^(k+1)) to a(2^(k+1)+2^(k-1)-1), the first quarter of B_{k+1}, is by
|
|
||||||
definition formed from the subsequence a(0) to a(2^(k-1)-1), the first quarter of A_{k+1}, by
|
|
||||||
interchanging its 0's and 1's. As noted above, the subsequence a(2^(k-1)) to a(2^k-1), the
|
|
||||||
second half of A_k, which is by definition also B_{k-1}, is by definition formed from the
|
|
||||||
subsequence a(0) to a(2^(k-1)-1), which is by definition A_{k-1}, by interchanging its 0's and
|
|
||||||
1's, as well. If two subsequences are formed from the same subsequence by interchanging its
|
|
||||||
0's and 1's then they must be identical, so the subsequence a(2^(k+1)) to
|
|
||||||
a(2^(k+1)+2^(k-1)-1), the first quarter of B_{k+1}, must be identical to the subsequence
|
|
||||||
a(2^(k-1)) to a(2^k-1), the second half of A_k.
|
|
||||||
|
|
||||||
Therefore the subsequence a(0), ..., a(2^(k-1)-1), a(2^(k-1)), ..., a(2^k-1) is identical to
|
|
||||||
the subsequence a(2^k+2^(k-1)), ..., a(2^(k+1)-1), a(2^(k+1)), ..., a(2^(k+1)+2^(k-1)-1), QED.
|
|
||||||
|
|
||||||
According to the German chess rules of 1929 a game of chess was drawn if the same sequence of
|
|
||||||
moves was repeated three times consecutively. Euwe, see the references, proved that this rule
|
|
||||||
could lead to infinite games. For his proof he reinvented the Thue-Morse sequence. - Johannes
|
|
||||||
W. Meijer, Feb 04 2010
|
|
||||||
|
|
||||||
"Thue-Morse 0->01 & 1->10, at each stage append the previous with its complement. Start with
|
|
||||||
0, 1, 2, 3 and write them in binary. Next calculate the sum of the digits (mod 2) - that is
|
|
||||||
divide the sum by 2 and use the remainder." Pickover, The Math Book.
|
|
||||||
|
|
||||||
Let s_2(n) be the sum of the base-2 digits of n and epsilon(n) = (-1)^s_2(n), the Thue-Morse
|
|
||||||
sequence, then prod(n >= 0, ((2*n+1)/(2*n+2))^epsilon(n) ) = 1/sqrt(2). - Jonathan Vos Post,
|
|
||||||
Jun 06 2012
|
|
||||||
|
|
||||||
Dekking shows that the constant obtained by interpreting this sequence as a binary expansion
|
|
||||||
is transcendental; see also "The Ubiquitous Prouhet-Thue-Morse Sequence". - Charles R
|
|
||||||
Greathouse IV, Jul 23 2013
|
|
||||||
|
|
||||||
Drmota, Mauduit, and Rivat proved that the subsequence a(n^2) is normal--see A228039. -
|
|
||||||
Jonathan Sondow, Sep 03 2013
|
|
||||||
|
|
||||||
Although the probability of a 0 or 1 is equal, guesses predicated on the latest bit seen
|
|
||||||
produce a correct match 2 out of 3 times. - Bill McEachen, Mar 13 2015
|
|
||||||
|
|
||||||
From a(0) to a(2n+1), there are n+1 terms equal to 0 and n+1 terms equal to 1 (see Hassan
|
|
||||||
Tarfaoui link, Concours Général 1990). - Bernard Schott, Jan 21 2022
|
|
||||||
REFERENCES J.-P. Allouche and J. Shallit, Automatic Sequences, Cambridge Univ. Press, 2003, p. 15.
|
|
||||||
|
|
||||||
Jason Bell, Michael Coons, and Eric Rowland, "The Rational-Transcendental Dichotomy of Mahler
|
|
||||||
Functions", Journal of Integer Sequences, Vol. 16 (2013), #13.2.10.
|
|
||||||
|
|
||||||
J. Berstel and J. Karhumaki, Combinatorics on words - a tutorial, Bull. EATCS, #79 (2003), pp.
|
|
||||||
178-228.
|
|
||||||
|
|
||||||
B. Bollobas, The Art of Mathematics: Coffee Time in Memphis, Cambridge, 2006, p. 224.
|
|
||||||
|
|
||||||
S. Brlek, Enumeration of factors in the Thue-Morse word, Discrete Applied Math., 24 (1989),
|
|
||||||
83-96. doi:10.1016/0166-218X(92)90274-E.
|
|
||||||
|
|
||||||
Yann Bugeaud and Guo-Niu Han, A combinatorial proof of the non-vanishing of Hankel
|
|
||||||
determinants of the Thue-Morse sequence, Electronic Journal of Combinatorics 21(3) (2014),
|
|
||||||
#P3.26.
|
|
||||||
|
|
||||||
Y. Bugeaud and M. Queffélec, On Rational Approximation of the Binary Thue-Morse-Mahler Number,
|
|
||||||
Journal of Integer Sequences, 16 (2013), #13.2.3.
|
|
||||||
|
|
||||||
J. Cooper and A. Dutle, Greedy Galois Games, Amer. Math. Mnthly, 120 (2013), 441-451.
|
|
||||||
|
|
||||||
Currie, James D. "Non-repetitive words: Ages and essences." Combinatorica 16.1 (1996): 19-40
|
|
||||||
|
|
||||||
A. de Luca and S. Varricchio, Some combinatorial properties of the Thue-Morse sequence and a
|
|
||||||
problem in semigroups, Theoret. Comput. Sci. 63 (1989), 333-348.
|
|
||||||
|
|
||||||
Colin Defant, Anti-Power Prefixes of the Thue-Morse Word Journal of Combinatorics, 24(1)
|
|
||||||
(2017), #P1.32
|
|
||||||
|
|
||||||
F. M. Dekking, Transcendance du nombre de Thue-Morse, Comptes Rendus de l'Academie des
|
|
||||||
Sciences de Paris 285 (1977), pp. 157-160.
|
|
||||||
|
|
||||||
F. M. Dekking, On repetitions of blocks in binary sequences. J. Combinatorial Theory Ser. A 20
|
|
||||||
(1976), no. 3, pp. 292-299. MR0429728(55 #2739)
|
|
||||||
|
|
||||||
Dekking, Michel, Michel Mendès France, and Alf van der Poorten. "Folds." The Mathematical
|
|
||||||
Intelligencer, 4.3 (1982): 130-138 & front cover, and 4:4 (1982): 173-181 (printed in two
|
|
||||||
parts).
|
|
||||||
|
|
||||||
Dubickas, Artūras. On a sequence related to that of Thue-Morse and its applications. Discrete
|
|
||||||
Math. 307 (2007), no. 9-10, 1082--1093. MR2292537 (2008b:11086).
|
|
||||||
|
|
||||||
Fabien Durand, Julien Leroy, and Gwenaël Richomme, "Do the Properties of an S-adic
|
|
||||||
Representation Determine Factor Complexity?", Journal of Integer Sequences, Vol. 16 (2013),
|
|
||||||
#13.2.6.
|
|
||||||
|
|
||||||
M. Euwe, Mengentheoretische Betrachtungen Über das Schachspiel, Proceedings Koninklijke
|
|
||||||
Nederlandse Akademie van Wetenschappen, Amsterdam, Vol. 32 (5): 633-642, 1929.
|
|
||||||
|
|
||||||
S. Ferenczi, Complexity of sequences and dynamical systems, Discrete Math., 206 (1999),
|
|
||||||
145-154.
|
|
||||||
|
|
||||||
S. R. Finch, Mathematical Constants, Cambridge, 2003, Section 6.8.
|
|
||||||
|
|
||||||
W. H. Gottschalk and G. A. Hedlund, Topological Dynamics. American Mathematical Society,
|
|
||||||
Colloquium Publications, Vol. 36, Providence, RI, 1955, p. 105.
|
|
||||||
|
|
||||||
J. Grytczuk, Thue type problems for graphs, points and numbers, Discrete Math., 308 (2008),
|
|
||||||
4419-4429.
|
|
||||||
|
|
||||||
A. Hof, O. Knill and B. Simon, Singular continuous spectrum for palindromic Schroedinger
|
|
||||||
operators, Commun. Math. Phys. 174 (1995), 149-159.
|
|
||||||
|
|
||||||
Mari Huova and Juhani Karhumäki, "On Unavoidability of k-abelian Squares in Pure Morphic
|
|
||||||
Words", Journal of Integer Sequences, Vol. 16 (2013), #13.2.9.
|
|
||||||
|
|
||||||
B. Kitchens, Review of "Computational Ergodic Theory" by G. H. Choe, Bull. Amer. Math. Soc.,
|
|
||||||
44 (2007), 147-155.
|
|
||||||
|
|
||||||
Le Breton, Xavier, Linear independence of automatic formal power series. Discrete Math. 306
|
|
||||||
(2006), no. 15, 1776-1780.
|
|
||||||
|
|
||||||
M. Lothaire, Combinatorics on Words. Addison-Wesley, Reading, MA, 1983, p. 23.
|
|
||||||
|
|
||||||
Donald MacMurray, A mathematician gives an hour to chess, Chess Review 6 (No. 10, 1938), 238.
|
|
||||||
[Discusses Marston's 1938 article]
|
|
||||||
|
|
||||||
Mauduit, Christian. Multiplicative properties of the Thue-Morse sequence. Period. Math.
|
|
||||||
Hungar. 43 (2001), no. 1-2, 137--153. MR1830572 (2002i:11081)
|
|
||||||
|
|
||||||
Mignosi, F.; Restivo, A.; Sciortino, M. Words and forbidden factors. WORDS (Rouen, 1999).
|
|
||||||
Theoret. Comput. Sci. 273 (2002), no. 1-2, 99--117. MR1872445 (2002m:68096)
|
|
||||||
|
|
||||||
Marston Morse, Title?, Bull. Amer. Math. Soc., 44 (No. 9, 1938), p. 632. [Mentions an
|
|
||||||
application to chess]
|
|
||||||
|
|
||||||
C. A. Pickover, Wonders of Numbers, Adventures in Mathematics, Mind and Meaning, Chapter 17,
|
|
||||||
'The Pipes of Papua,' Oxford University Press, Oxford, England, 2000, pages 34-38.
|
|
||||||
|
|
||||||
C. A. Pickover, A Passion for Mathematics, Wiley, 2005; see p. 60.
|
|
||||||
|
|
||||||
Clifford A. Pickover, The Math Book, From Pythagoras to the 57th Dimension, 250 Milestones in
|
|
||||||
the History of Mathematics, Sterling Publ., NY, 2009, page 316.
|
|
||||||
|
|
||||||
Narad Rampersad and Elise Vaslet, "On Highly Repetitive and Power Free Words", Journal of
|
|
||||||
Integer Sequences, Vol. 16 (2013), #13.2.7.
|
|
||||||
|
|
||||||
G. Richomme, K. Saari, L. Q. Zamboni, Abelian complexity in minimal subshifts, J. London Math.
|
|
||||||
Soc. 83(1) (2011) 79-95.
|
|
||||||
|
|
||||||
Michel Rigo, Formal Languages, Automata and Numeration Systems, 2 vols., Wiley, 2014. Mentions
|
|
||||||
this sequence - see "List of Sequences" in Vol. 2.
|
|
||||||
|
|
||||||
M. Rigo, P. Salimov, and E. Vandomme, "Some Properties of Abelian Return Words", Journal of
|
|
||||||
Integer Sequences, Vol. 16 (2013), #13.2.5.
|
|
||||||
|
|
||||||
Benoit Rittaud, Elise Janvresse, Emmanuel Lesigne and Jean-Christophe Novelli, Quand les maths
|
|
||||||
se font discrètes, Le Pommier, 2008 (ISBN 978-2-7465-0370-0).
|
|
||||||
|
|
||||||
A. Salomaa, Jewels of Formal Language Theory. Computer Science Press, Rockville, MD, 1981, p.
|
|
||||||
6.
|
|
||||||
|
|
||||||
Shallit, J. O. "On Infinite Products Associated with Sums of Digits." J. Number Th. 21,
|
|
||||||
128-134, 1985.
|
|
||||||
|
|
||||||
Ian Stewart, "Feedback", Mathematical Recreations Column, Scientific American, 274 (No. 3,
|
|
||||||
1996), page 109 [Historical notes on this sequence]
|
|
||||||
|
|
||||||
Thomas Stoll, On digital blocks of polynomial values and extractions in the Rudin-Shapiro
|
|
||||||
sequence, RAIRO - Theoretical Informatics and Applications (RAIRO: ITA), EDP Sciences, 2016,
|
|
||||||
50, pp. 93-99. <hal-01278708>.
|
|
||||||
|
|
||||||
A. Thue. Über unendliche Zeichenreihen, Norske Vid. Selsk. Skr. I. Mat. Nat. Kl. Christiania,
|
|
||||||
No. 7 (1906), 1-22.
|
|
||||||
|
|
||||||
A. Thue, Über die gegenseitige Lage gleicher Teile gewisser Zeichenreihen, Norske Vid. Selsk.
|
|
||||||
Skr. I. Mat. Nat. Kl. Christiania, 1 (1912), 1-67.
|
|
||||||
|
|
||||||
S. Wolfram, A New Kind of Science, Wolfram Media, 2002; p. 890.
|
|
||||||
LINKS N. J. A. Sloane, Table of n, a(n) for n = 0..16383
|
|
||||||
|
|
||||||
A. G. M. Ahmed, AA Weaving. In: Proceedings of Bridges 2013: Mathematics, Music, Art, ...,
|
|
||||||
2013.
|
|
||||||
|
|
||||||
A. Aksenov, The Newman phenomenon and Lucas sequence, arXiv preprint arXiv:1108.5352
|
|
||||||
[math.NT], 2011-2012.
|
|
||||||
|
|
||||||
Max A. Alekseyev and N. J. A. Sloane, On Kaprekar's Junction Numbers, arXiv:2112.14365, 2021;
|
|
||||||
Journal of Combinatorics and Number Theory, 2022 (to appear).
|
|
||||||
|
|
||||||
J.-P. Allouche, Series and infinite products related to binary expansions of integers,
|
|
||||||
Behaviour, 4.4 (1992): p. 5.
|
|
||||||
|
|
||||||
J.-P. Allouche, Lecture notes on automatic sequences, Krakow October 2013.
|
|
||||||
|
|
||||||
J.-P. Allouche, Thue, Combinatorics on words, and conjectures inspired by the Thue-Morse
|
|
||||||
sequence, J. de Théorie des Nombres de Bordeaux, 27, no. 2 (2015), 375-388.
|
|
||||||
|
|
||||||
J.-P. Allouche, Andre Arnold, Jean Berstel, Srecko Brlek, William Jockusch, Simon Plouffe and
|
|
||||||
Bruce E. Sagan, A relative of the Thue-Morse sequence, Discrete Math., 139 (1995), 455-461.
|
|
||||||
|
|
||||||
Jean-Paul Allouche, Julien Cassaigne, Jeffrey Shallit and Luca Q. Zamboni, A Taxonomy of
|
|
||||||
Morphic Sequences, arXiv preprint arXiv:1711.10807 [cs.FL], Nov 29 2017.
|
|
||||||
|
|
||||||
J.-P. Allouche and H. Cohen, Dirichlet Series and Curious Infinite Products, Bull. London
|
|
||||||
Math. Soc. 17, 531-538, 1985.
|
|
||||||
|
|
||||||
J.-P. Allouche and M. Mendes France, Automata and Automatic Sequences, in: Axel F. and Gratias
|
|
||||||
D. (eds), Beyond Quasicrystals. Centre de Physique des Houches, vol 3. Springer, Berlin,
|
|
||||||
Heidelberg, pp. 293-367, 1995; DOI https://doi.org/10.1007/978-3-662-03130-8_11.
|
|
||||||
|
|
||||||
J.-P. Allouche and M. Mendes France, Automata and Automatic Sequences, in: Axel F. and Gratias
|
|
||||||
D. (eds), Beyond Quasicrystals. Centre de Physique des Houches, vol 3. Springer, Berlin,
|
|
||||||
Heidelberg, pp. 293-367, 1995; DOI https://doi.org/10.1007/978-3-662-03130-8_11. [Local copy]
|
|
||||||
|
|
||||||
J.-P. Allouche and Jeffrey Shallit, The Ubiquitous Prouhet-Thue-Morse Sequence, in C. Ding. T.
|
|
||||||
Helleseth and H. Niederreiter, eds., Sequences and Their Applications: Proceedings of SETA
|
|
||||||
'98, Springer-Verlag, 1999, pp. 1-16.
|
|
||||||
|
|
||||||
J.-P. Allouche and J. Shallit, The Ring of k-regular Sequences, II, Theoretical Computer
|
|
||||||
Science 307.1 (2003): 3-29. doi:10.1016/S0304-3975(03)00090-2
|
|
||||||
|
|
||||||
Jorge Almeida and Ondrej Klíma, Binary patterns in the Prouhet-Thue-Morse sequence,
|
|
||||||
arXiv:1904.07137 [math.CO], 2019.
|
|
||||||
|
|
||||||
Joerg Arndt, Matters Computational (The Fxtbook), p. 44.
|
|
||||||
|
|
||||||
G. N. Arzhantseva, C. H. Cashen, D. Gruber and D. Hume, Contracting geodesics in infinitely
|
|
||||||
presented graphical small cancellation groups, arXiv preprint arXiv:1602.03767 [math.GR],
|
|
||||||
2016-2018.
|
|
||||||
|
|
||||||
Ricardo Astudillo, On a Class of Thue-Morse Type Sequences, J. Integer Seqs., Vol. 6, 2003.
|
|
||||||
|
|
||||||
F. Axel et al., Vibrational modes in a one dimensional "quasi-alloy": the Morse case, J. de
|
|
||||||
Physique, Colloq. C3, Supp. to No. 7, Vol. 47 (Jul 1986), pp. C3-181-C3-186; see Eq. (10).
|
|
||||||
|
|
||||||
M. Baake, U. Grimm and J. Nilsson, Scaling of the Thue-Morse diffraction measure, arXiv
|
|
||||||
preprint arXiv:1311.4371 [math-ph], 2013.
|
|
||||||
|
|
||||||
Scott Balchin and Dan Rust, Computations for Symbolic Substitutions, Journal of Integer
|
|
||||||
Sequences, Vol. 20 (2017), Article 17.4.1.
|
|
||||||
|
|
||||||
Lucilla Baldini and Josef Eschgfäller, Random functions from coupled dynamical systems, arXiv
|
|
||||||
preprint arXiv:1609.01750 [math.CO], 2016. See Example 3.11.
|
|
||||||
|
|
||||||
J. Berstel, Axel Thue's papers on repetitions in words: a translation, July 21 1994.
|
|
||||||
Publications du LaCIM, Département de mathématiques et d'informatique 20, Université du Québec
|
|
||||||
à Montréal, 1995, 85 pages. [Cached copy]
|
|
||||||
|
|
||||||
J.-F. Bertazzon, Resolution of an integral equation with the Thue-Morse sequence,
|
|
||||||
arXiv:1201.2502v1 [math.CO], Jan 12, 2012.
|
|
||||||
|
|
||||||
Françoise Dejean, Sur un Théorème de Thue, J. Combinatorial Theory, vol. 13 A, iss. 1 (1972)
|
|
||||||
90-99.
|
|
||||||
|
|
||||||
F. Michel Dekking, Morphisms, Symbolic sequences, and their Standard Forms, arXiv:1509.00260
|
|
||||||
[math.CO], 2015.
|
|
||||||
|
|
||||||
E. Deutsch and B. E. Sagan, Congruences for Catalan and Motzkin numbers and related sequences,
|
|
||||||
J. Num. Theory 117 (2006), 191-215.
|
|
||||||
|
|
||||||
M. Drmota, C. Mauduit and J. Rivat, The Thue-Morse Sequence Along The Squares is Normal,
|
|
||||||
Abstract, ÖMG-DMV Congress, 2013.
|
|
||||||
|
|
||||||
Arthur Dolgopolov, Equitable Sequencing and Allocation Under Uncertainty, Preprint, 2016.
|
|
||||||
|
|
||||||
J. Endrullis, D. Hendriks and J. W. Klop, Degrees of streams, Journal of Integers B 11 (2011):
|
|
||||||
1-40..
|
|
||||||
|
|
||||||
A. S. Fraenkel, New games related to old and new sequences, INTEGERS, Electronic J. of
|
|
||||||
Combinatorial Number Theory, Vol. 4, Paper G6, 2004.
|
|
||||||
|
|
||||||
Hao Fu and G.-N. Han, Computer assisted proof for Apwenian sequences related to Hankel
|
|
||||||
determinants, arXiv preprint arXiv:1601.04370 [math.NT], 2016.
|
|
||||||
|
|
||||||
Maciej Gawro and Maciej Ulas, "On formal inverse of the Prouhet-Thue-Morse sequence." Discrete
|
|
||||||
Mathematics 339.5 (2016): 1459-1470. Also arXiv:1601.04840, 2016.
|
|
||||||
|
|
||||||
Michael Gilleland, Some Self-Similar Integer Sequences
|
|
||||||
|
|
||||||
Daniel Goc, Luke Schaeffer and Jeffrey Shallit, The Subword Complexity of k-Automatic
|
|
||||||
Sequences is k-Synchronized, arXiv 1206.5352 [cs.FL], Jun 28 2012.
|
|
||||||
|
|
||||||
G. A. Hedlund, Remarks on the work of Axel Thue on sequences, Nordisk Mat. Tid., 15 (1967),
|
|
||||||
148-150.
|
|
||||||
|
|
||||||
Dimitri Hendriks, Frits G. W. Dannenberg, Jorg Endrullis, Mark Dow and Jan Willem Klop,
|
|
||||||
Arithmetic Self-Similarity of Infinite Sequences, arXiv preprint 1201.3786 [math.CO], 2012.
|
|
||||||
|
|
||||||
A. M. Hinz, S. Klavžar, U. Milutinović and C. Petr, The Tower of Hanoi - Myths and Maths,
|
|
||||||
Birkhäuser 2013. See page 79. Website for book
|
|
||||||
|
|
||||||
Tanya Khovanova, There are no coincidences, arXiv preprint 1410.2193 [math.CO], 2014.
|
|
||||||
|
|
||||||
Clark Kimberling, Intriguing infinite words composed of zeros and ones, Elemente der
|
|
||||||
Mathematik (2021).
|
|
||||||
|
|
||||||
Naoki Kobayashi, Kazutaka Matsuda and Ayumi Shinohara, Functional Programs as Compressed Data,
|
|
||||||
Higher-Order and Symbolic Computation, 25, no. 1 (2012): 39-84..
|
|
||||||
|
|
||||||
Philip Lafrance, Narad Rampersad and Randy Yee, Some properties of a Rudin-Shapiro-like
|
|
||||||
sequence, arXiv:1408.2277 [math.CO], 2014.
|
|
||||||
|
|
||||||
C. Mauduit, J. Rivat, La somme des chiffres des carres, Acta Mathem. 203 (1) (2009) 107-148.
|
|
||||||
|
|
||||||
M. Morse, Recurrent geodesics on a surface of negative curvature, Trans. Amer. Math. Soc., 22
|
|
||||||
(1921), 84-100.
|
|
||||||
|
|
||||||
K. Nakano, Shall We Juggle, Coinductively?, in Certified Programs and Proofs, Lecture Notes in
|
|
||||||
Computer Science Volume 7679, 2012, pp. 160-172.
|
|
||||||
|
|
||||||
Hieu D. Nguyen, A mixing of Prouhet-Thue-Morse sequences and Rademacher functions, arXiv
|
|
||||||
preprint arXiv:1405.6958 [math.NT], 2014.
|
|
||||||
|
|
||||||
Hieu D. Nguyen, A Generalization of the Digital Binomial Theorem , J. Int. Seq. 18 (2015) #
|
|
||||||
15.5.7.
|
|
||||||
|
|
||||||
C. D. Offner, Repetitions of Words and the Thue-Morse sequence. Preprint, no date.
|
|
||||||
|
|
||||||
Matt Parker, The Fairest Sharing Sequence Ever, YouTube video, Nov 27 2015
|
|
||||||
|
|
||||||
A. Parreau, M. Rigo, E. Rowland and E. Vandomme, A new approach to the 2-regularity of the
|
|
||||||
l-abelian complexity of 2-automatic sequences, arXiv preprint arXiv:1405.3532 [cs.FL], 2014.
|
|
||||||
|
|
||||||
C. A. Pickover, "Wonders of Numbers, Adventures in Mathematics, Mind and Meaning,"
|
|
||||||
Zentralblatt review
|
|
||||||
|
|
||||||
E. Prouhet, Mémoire sur quelques relations entre les puissances des nombres, Comptes Rendus
|
|
||||||
Acad. des Sciences, 33 (No. 8, 1851), p. 225. [Said to implicitly mention this sequence]
|
|
||||||
|
|
||||||
Michel Rigo, Relations on words, arXiv preprint arXiv:1602.03364 [cs.FL], 2016.
|
|
||||||
|
|
||||||
Luke Schaeffer and Jeffrey Shallit, Closed, Palindromic, Rich, Privileged, Trapezoidal, and
|
|
||||||
Balanced Words in Automatic Sequences, Electronic Journal of Combinatorics 23(1) (2016),
|
|
||||||
#P1.25.
|
|
||||||
|
|
||||||
M. R. Schroeder & N. J. A. Sloane, Correspondence, 1991
|
|
||||||
|
|
||||||
R. Schroeppel and R. W. Gosper, HACKMEM #122 (1972).
|
|
||||||
|
|
||||||
Vladimir Shevelev, Two analogs of Thue-Morse sequence, arXiv preprint arXiv:1603.04434
|
|
||||||
[math.NT], 2016-2017.
|
|
||||||
|
|
||||||
N. J. A. Sloane, The first 1000 terms as a string
|
|
||||||
|
|
||||||
L. Spiegelhofer, Normality of the Thue-Morse Sequence along Piatetski-Shapiro sequences,
|
|
||||||
Quart. J. Math. 66 (3) (2015).
|
|
||||||
|
|
||||||
Hassan Tarfaoui, Concours Général 1990 - Exercice 1 (in French).
|
|
||||||
|
|
||||||
Eric Weisstein's World of Mathematics, Thue-Morse Sequence
|
|
||||||
|
|
||||||
Eric Weisstein's World of Mathematics, Thue-Morse Constant
|
|
||||||
|
|
||||||
Eric Weisstein's World of Mathematics, Parity
|
|
||||||
|
|
||||||
Joost Winter, Marcello M. Bonsangue, and Jan J. M. M. Rutten, Context-free coalgebras, Journal
|
|
||||||
of Computer and System Sciences, 81.5 (2015): 911-939.
|
|
||||||
|
|
||||||
Hans Zantema, Complexity of Automatic Sequences, International Conference on Language and
|
|
||||||
Automata Theory and Applications (LATA 2020): Language and Automata Theory and Applications,
|
|
||||||
260-271.
|
|
||||||
|
|
||||||
Index entries for sequences that are fixed points of mappings
|
|
||||||
|
|
||||||
Index entries for "core" sequences
|
|
||||||
|
|
||||||
Index entries for sequences related to binary expansion of n
|
|
||||||
|
|
||||||
Index entries for characteristic functions
|
|
||||||
|
|
||||||
Index to sequences related to Olympiads and other Mathematical competitions.
|
|
||||||
FORMULA a(2n) = a(n), a(2n+1) = 1 - a(n), a(0) = 0. Also, a(k+2^m) = 1 - a(k) if 0 <= k < 2^m.
|
|
||||||
|
|
||||||
If n = Sum b_i*2^i is the binary expansion of n then a(n) = Sum b_i (mod 2).
|
|
||||||
|
|
||||||
Let S(0) = 0 and for k >= 1, construct S(k) from S(k-1) by mapping 0 -> 01 and 1 -> 10;
|
|
||||||
sequence is S(infinity).
|
|
||||||
|
|
||||||
G.f.: (1/(1 - x) - Product_{k >= 0} (1 - x^(2^k)))/2. - Benoit Cloitre, Apr 23 2003
|
|
||||||
|
|
||||||
a(0) = 0, a(n) = (n + a(floor(n/2))) mod 2; also a(0) = 0, a(n) = (n - a(floor(n/2))) mod 2. -
|
|
||||||
Benoit Cloitre, Dec 10 2003
|
|
||||||
|
|
||||||
a(n) = -1 + (Sum_{k=0..n} binomial(n,k) mod 2) mod 3 = -1 + A001316(n) mod 3. - Benoit
|
|
||||||
Cloitre, May 09 2004
|
|
||||||
|
|
||||||
Let b(1) = 1 and b(n) = b(ceiling(n/2)) - b(floor(n/2)) then a(n-1) = (1/2)*(1 - b(2n-1)). -
|
|
||||||
Benoit Cloitre, Apr 26 2005
|
|
||||||
|
|
||||||
a(n) = 1 - A010059(n) = A001285(n) - 1. - Ralf Stephan, Jun 20 2003
|
|
||||||
|
|
||||||
a(n) = A001969(n) - 2n. - Franklin T. Adams-Watters, Aug 28 2006
|
|
||||||
|
|
||||||
a(n) = A115384(n) - A115384(n-1) for n > 0. - Reinhard Zumkeller, Aug 26 2007
|
|
||||||
|
|
||||||
For n >= 0, a(A004760(n+1)) = 1 - a(n). - Vladimir Shevelev, Apr 25 2009
|
|
||||||
|
|
||||||
a(A160217(n)) = 1 - a(n). - Vladimir Shevelev, May 05 2009
|
|
||||||
|
|
||||||
a(n) == A000069(n) (mod 2). - Robert G. Wilson v, Jan 18 2012
|
|
||||||
|
|
||||||
a(n) = A000035(A000120(n)). - Omar E. Pol, Oct 26 2013
|
|
||||||
|
|
||||||
a(n) = A000035(A193231(n)). - Antti Karttunen, Dec 27 2013
|
|
||||||
|
|
||||||
a(n) + A181155(n-1) = 2n for n >= 1. - Clark Kimberling, Oct 06 2014
|
|
||||||
|
|
||||||
G.f. A(x) satisfies: A(x) = x / (1 - x^2) + (1 - x) * A(x^2). - Ilya Gutkovskiy, Jul 29 2021
|
|
||||||
|
|
||||||
From Bernard Schott, Jan 21 2022: (Start)
|
|
||||||
|
|
||||||
a(n) = a(n*2^k) for k >= 0.
|
|
||||||
|
|
||||||
a((2^m-1)^2) = (1-(-1)^m))/2 (see Hassan Tarfaoui link, Concours Général 1990). (End)
|
|
||||||
EXAMPLE The evolution starting at 0 is:
|
|
||||||
|
|
||||||
.0
|
|
||||||
|
|
||||||
.0, 1
|
|
||||||
|
|
||||||
.0, 1, 1, 0
|
|
||||||
|
|
||||||
.0, 1, 1, 0, 1, 0, 0, 1
|
|
||||||
|
|
||||||
.0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1, 0, 1, 1, 0
|
|
||||||
|
|
||||||
.0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 0, 1, 1, 0, 1, 0, 0,
|
|
||||||
1
|
|
||||||
|
|
||||||
.......
|
|
||||||
|
|
||||||
A_2 = 0 1 1 0, so B_2 = 1 0 0 1 and A_3 = A_2 B_2 = 0 1 1 0 1 0 0 1.
|
|
||||||
|
|
||||||
From Joerg Arndt, Mar 12 2013: (Start)
|
|
||||||
|
|
||||||
The first steps of the iterated substitution are
|
|
||||||
|
|
||||||
Start: 0
|
|
||||||
|
|
||||||
Rules:
|
|
||||||
|
|
||||||
0 --> 01
|
|
||||||
|
|
||||||
1 --> 10
|
|
||||||
|
|
||||||
-------------
|
|
||||||
|
|
||||||
0: (#=1)
|
|
||||||
|
|
||||||
0
|
|
||||||
|
|
||||||
1: (#=2)
|
|
||||||
|
|
||||||
01
|
|
||||||
|
|
||||||
2: (#=4)
|
|
||||||
|
|
||||||
0110
|
|
||||||
|
|
||||||
3: (#=8)
|
|
||||||
|
|
||||||
01101001
|
|
||||||
|
|
||||||
4: (#=16)
|
|
||||||
|
|
||||||
0110100110010110
|
|
||||||
|
|
||||||
5: (#=32)
|
|
||||||
|
|
||||||
01101001100101101001011001101001
|
|
||||||
|
|
||||||
6: (#=64)
|
|
||||||
|
|
||||||
0110100110010110100101100110100110010110011010010110100110010110
|
|
||||||
|
|
||||||
(End)
|
|
||||||
|
|
||||||
From Omar E. Pol, Oct 28 2013: (Start)
|
|
||||||
|
|
||||||
Written as an irregular triangle in which row lengths is A011782, the sequence begins:
|
|
||||||
|
|
||||||
0;
|
|
||||||
|
|
||||||
1;
|
|
||||||
|
|
||||||
1,0;
|
|
||||||
|
|
||||||
1,0,0,1;
|
|
||||||
|
|
||||||
1,0,0,1,0,1,1,0;
|
|
||||||
|
|
||||||
1,0,0,1,0,1,1,0,0,1,1,0,1,0,0,1;
|
|
||||||
|
|
||||||
1,0,0,1,0,1,1,0,0,1,1,0,1,0,0,1,0,1,1,0,1,0,0,1,1,0,0,1,0,1,1,0;
|
|
||||||
|
|
||||||
It appears that: row j lists the first A011782(j) terms of A010059, with j >= 0; row sums give
|
|
||||||
A166444 which is also 0 together with A011782; right border gives A000035.
|
|
||||||
|
|
||||||
(End)
|
|
||||||
MAPLE s := proc(k) local i, ans; ans := [ 0, 1 ]; for i from 0 to k do ans := [ op(ans),
|
|
||||||
op(map(n->(n+1) mod 2, ans)) ] od; return ans; end; t1 := s(6); A010060 := n->t1[n]; # s(k)
|
|
||||||
gives first 2^(k+2) terms.
|
|
||||||
|
|
||||||
a := proc(k) b := [0]: for n from 1 to k do b := subs({0=[0, 1], 1=[1, 0]}, b) od: b; end; #
|
|
||||||
a(k), after the removal of the brackets, gives the first 2^k terms. # Example: a(3); gives
|
|
||||||
[[[[0, 1], [1, 0]], [[1, 0], [0, 1]]]]
|
|
||||||
|
|
||||||
A010060:=proc(n)
|
|
||||||
|
|
||||||
add(i, i=convert(n, base, 2)) mod 2 ;
|
|
||||||
|
|
||||||
end proc:
|
|
||||||
|
|
||||||
seq(A010060(n), n=0..104); # Emeric Deutsch, Mar 19 2005
|
|
||||||
|
|
||||||
map(`-`, convert(StringTools[ThueMorse](1000), bytes), 48); # Robert Israel, Sep 22 2014
|
|
||||||
MATHEMATICA Table[ If[ OddQ[ Count[ IntegerDigits[n, 2], 1]], 1, 0], {n, 0, 100}];
|
|
||||||
|
|
||||||
mt = 0; Do[ mt = ToString[mt] <> ToString[(10^(2^n) - 1)/9 - ToExpression[mt] ], {n, 0, 6} ];
|
|
||||||
Prepend[ RealDigits[ N[ ToExpression[mt], 2^7] ] [ [1] ], 0]
|
|
||||||
|
|
||||||
Mod[ Count[ #, 1 ]& /@Table[ IntegerDigits[ i, 2 ], {i, 0, 2^7 - 1} ], 2 ] (* Harlan J.
|
|
||||||
Brothers, Feb 05 2005 *)
|
|
||||||
|
|
||||||
Nest[ Flatten[ # /. {0 -> {0, 1}, 1 -> {1, 0}}] &, {0}, 7] (* Robert G. Wilson v Sep 26 2006
|
|
||||||
*)
|
|
||||||
|
|
||||||
a[n_] := If[n == 0, 0, If[Mod[n, 2] == 0, a[n/2], 1 - a[(n - 1)/2]]] (* Ben Branman, Oct 22
|
|
||||||
2010 *)
|
|
||||||
|
|
||||||
a[n_] := Mod[Length[FixedPointList[BitAnd[#, # - 1] &, n]], 2] (* Jan Mangaldan, Jul 23 2015
|
|
||||||
*)
|
|
||||||
|
|
||||||
Table[2/3 (1 - Cos[Pi/3 (n - Sum[(-1)^Binomial[n, k], {k, 1, n}])]), {n, 0, 100}] (* or, for
|
|
||||||
version 10.2 or higher *) Table[ThueMorse[n], {n, 0, 100}] (* Vladimir Reshetnikov, May 06
|
|
||||||
2016 *)
|
|
||||||
|
|
||||||
ThueMorse[Range[0, 100]] (* The program uses the ThueMorse function from Mathematica version
|
|
||||||
11 *) (* Harvey P. Dale, Aug 11 2016 *)
|
|
||||||
PROG (Haskell)
|
|
||||||
|
|
||||||
a010060 n = a010060_list !! n
|
|
||||||
|
|
||||||
a010060_list =
|
|
||||||
|
|
||||||
0 : interleave (complement a010060_list) (tail a010060_list)
|
|
||||||
|
|
||||||
where complement = map (1 - )
|
|
||||||
|
|
||||||
interleave (x:xs) ys = x : interleave ys xs
|
|
||||||
|
|
||||||
-- Doug McIlroy (doug(AT)cs.dartmouth.edu), Jun 29 2003
|
|
||||||
|
|
||||||
-- Edited by Reinhard Zumkeller, Oct 03 2012
|
|
||||||
|
|
||||||
(PARI) a(n)=if(n<1, 0, sum(k=0, length(binary(n))-1, bittest(n, k))%2)
|
|
||||||
|
|
||||||
(PARI) a(n)=if(n<1, 0, subst(Pol(binary(n)), x, 1)%2)
|
|
||||||
|
|
||||||
(PARI) default(realprecision, 6100); x=0.0; m=20080; for (n=1, m-1, x=x+x; x=x+sum(k=0,
|
|
||||||
length(binary(n))-1, bittest(n, k))%2); x=2*x/2^m; for (n=0, 20000, d=floor(x); x=(x-d)*2;
|
|
||||||
write("b010060.txt", n, " ", d)); \\ Harry J. Smith, Apr 28 2009
|
|
||||||
|
|
||||||
(PARI) a(n)=hammingweight(n)%2 \\ Charles R Greathouse IV, Mar 22 2013
|
|
||||||
|
|
||||||
(Python)
|
|
||||||
|
|
||||||
A010060_list = [0]
|
|
||||||
|
|
||||||
for _ in range(14):
|
|
||||||
|
|
||||||
A010060_list += [1-d for d in A010060_list] # Chai Wah Wu, Mar 04 2016
|
|
||||||
|
|
||||||
(R)
|
|
||||||
|
|
||||||
maxrow <- 8 # by choice
|
|
||||||
|
|
||||||
b01 <- 1
|
|
||||||
|
|
||||||
for(m in 0:maxrow) for(k in 0:(2^m-1)){
|
|
||||||
|
|
||||||
b01[2^(m+1)+ k] <- b01[2^m+k]
|
|
||||||
|
|
||||||
b01[2^(m+1)+2^m+k] <- 1-b01[2^m+k]
|
|
||||||
|
|
||||||
}
|
|
||||||
|
|
||||||
(b01 <- c(0, b01))
|
|
||||||
|
|
||||||
# Yosu Yurramendi, Apr 10 2017
|
|
||||||
CROSSREFS Cf. A001285 (for 1, 2 version), A010059 (for 1, 0 version), A106400 (for +1, -1 version),
|
|
||||||
A048707. A010060(n)=A000120(n) mod 2.
|
|
||||||
|
|
||||||
Cf. A007413, A080813, A080814, A036581, A108694. See also the Thue (or Roth) constant A014578,
|
|
||||||
also A014571.
|
|
||||||
|
|
||||||
Cf. also A001969, A035263, A005187, A115384, A132680, A141803, A104248, A193231.
|
|
||||||
|
|
||||||
Run lengths give A026465. Backward first differences give A029883.
|
|
||||||
|
|
||||||
Cf. A004128, A053838, A059448, A171900, A161916, A214212, A005942 (subword complexity),
|
|
||||||
A010693 (Abelian complexity), A225186 (squares), A228039 (a(n^2)), A282317.
|
|
||||||
|
|
||||||
Sequences mentioned in the Allouche et al. "Taxonomy" paper, listed by example number: 1:
|
|
||||||
A003849, 2: A010060, 3: A010056, 4: A020985 and A020987, 5: A191818, 6: A316340 and A273129,
|
|
||||||
18: A316341, 19: A030302, 20: A063438, 21: A316342, 22: A316343, 23: A003849 minus its first
|
|
||||||
term, 24: A316344, 25: A316345 and A316824, 26: A020985 and A020987, 27: A316825, 28: A159689,
|
|
||||||
29: A049320, 30: A003849, 31: A316826, 32: A316827, 33: A316828, 34: A316344, 35: A043529, 36:
|
|
||||||
A316829, 37: A010060.
|
|
||||||
|
|
||||||
Sequence in context: A143222 A286490 A217831 * A316569 A284848 A286484
|
|
||||||
|
|
||||||
Adjacent sequences: A010057 A010058 A010059 * A010061 A010062 A010063
|
|
||||||
KEYWORD nonn,core,easy,nice
|
|
||||||
AUTHOR N. J. A. Sloane
|
|
||||||
STATUS approved
|
|
||||||
|
|
||||||
Lookup | Welcome | Wiki | Register | Music | Plot 2 | Demos | Index | Browse | More | WebCam
|
|
||||||
Contribute new seq. or comment | Format | Style Sheet | Transforms | Superseeker | Recents
|
|
||||||
The OEIS Community | Maintained by The OEIS Foundation Inc.
|
|
||||||
|
|
||||||
License Agreements, Terms of Use, Privacy Policy. .
|
|
||||||
|
|
||||||
Last modified November 20 14:06 EST 2022. Contains 358247 sequences. (Running on oeis4.)
|
|
||||||
|
|
||||||
*)
|
*)
|
||||||
|
|
||||||
Require Import Coq.Lists.List.
|
Require Import Coq.Lists.List.
|
||||||
@ -1152,24 +475,17 @@ Proof.
|
|||||||
+ rewrite Nat.mul_lt_mono_pos_r with (p := 2^m) in H1.
|
+ rewrite Nat.mul_lt_mono_pos_r with (p := 2^m) in H1.
|
||||||
rewrite <- Nat.pow_add_r in H1. rewrite Nat.add_comm.
|
rewrite <- Nat.pow_add_r in H1. rewrite Nat.add_comm.
|
||||||
assumption. rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
|
assumption. rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
|
||||||
+ rewrite nth_error_app1. rewrite nth_error_app1.
|
+ assert (L: forall l, l < 2^m -> k*2^m + l < length (tm_step (m+n))).
|
||||||
|
intro l. intro M. rewrite tm_size_power2.
|
||||||
|
destruct k. simpl. assert (2^m <= 2^(m+n)).
|
||||||
|
apply Nat.pow_le_mono_r. easy. apply Nat.le_add_r.
|
||||||
|
generalize H3. generalize M. apply Nat.lt_le_trans.
|
||||||
|
apply lt_split_bits. apply Nat.lt_0_succ. assumption.
|
||||||
|
assumption.
|
||||||
|
|
||||||
|
rewrite nth_error_app1. rewrite nth_error_app1.
|
||||||
generalize H1. apply IHn.
|
generalize H1. apply IHn.
|
||||||
|
apply L. assumption. apply L. assumption.
|
||||||
rewrite tm_size_power2.
|
|
||||||
assert (k * 2^m + j < 2^(m+n)).
|
|
||||||
destruct k. simpl. assert (2^m <= 2^(m+n)).
|
|
||||||
apply Nat.pow_le_mono_r. easy. apply Nat.le_add_r.
|
|
||||||
generalize H3. generalize I. apply Nat.lt_le_trans.
|
|
||||||
apply lt_split_bits. apply Nat.lt_0_succ.
|
|
||||||
assumption. assumption. assumption.
|
|
||||||
|
|
||||||
rewrite tm_size_power2.
|
|
||||||
assert (k * 2^m + i < 2^(m+n)).
|
|
||||||
destruct k. simpl. assert (2^m <= 2^(m+n)).
|
|
||||||
apply Nat.pow_le_mono_r. easy. apply Nat.le_add_r.
|
|
||||||
generalize H3. generalize H. apply Nat.lt_le_trans.
|
|
||||||
apply lt_split_bits. apply Nat.lt_0_succ.
|
|
||||||
assumption. assumption. assumption.
|
|
||||||
|
|
||||||
+ assert (J: 2 ^ (m + n) <= k * 2 ^ m).
|
+ assert (J: 2 ^ (m + n) <= k * 2 ^ m).
|
||||||
rewrite Nat.pow_add_r. rewrite Nat.mul_comm.
|
rewrite Nat.pow_add_r. rewrite Nat.mul_comm.
|
||||||
@ -1308,6 +624,16 @@ Proof.
|
|||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
(* TODO: supprimer head_2 *)
|
||||||
|
|
||||||
|
|
||||||
Require Import BinNat.
|
Require Import BinNat.
|
||||||
|
|
||||||
|
|
||||||
|
Loading…
Reference in New Issue
Block a user