1: \begin{abstract}

2:   \noindent

3:   We study S1S and Büchi automata 

4:   in the constructive type theory 

5:   of the Coq proof assistant.  

6:   For UP semantics (ultimately periodic sequences), 

7:   we verify Büchi's translation of formulas to automata 

8:   and thereby establish decidability of S1S constructively.  

9:   For AS semantics (all sequences), 

10:   we verify Büchi's translation assuming that 

11:   sequences over finite semigroups have Ramseyan factorisations (RF).  

12:   Assuming RF, UP semantics and AS semantics agree.  

13:   RF is a consequence of Ramsey's theorem 

14:   and implies the infinite pigeonhole principle, 

15:   which is known to be unprovable constructively.  

16:   We show that each of the following properties holds for UP semantics 

17:   but is equivalent to RF for AS semantics: 

18:   excluded middle of formula satisfaction, 

19:   excluded middle of automaton acceptance, and 

20:   existence of complement automata.

21:   % We also show that RF is equivalent to

22:   % AU (UP equivalence implies CS equivalence of automata).

23: \end{abstract}

24: