title: Countdown games, and simulation on (succinct) one-counter nets
authors: Petr Jancar Petr Osicka Zdenek Sawa
text: 
  
  
  
  
  
  This paper has arisen by a thorough rewriting of
  a preliminary version
  in the proceedings of the Reachability Problems
  conference 2018, and by adding the topics elaborated in
  Sections <ref> and <ref>.
  
  P. Jančar and P. Osička
  acknowledge the support by the project 18-11193S of the Grant Agency of the
  Czech Republic. Z. Sawa is partially supported by Grant
  of SGS No. SP2022/123, VŠB Technical University of Ostrava, Czech Republic.
  
  P. Jančar]Petr Jančar0000-0002-8738-9850[a]
  P. Osička]Petr Osička0000-0002-7495-7724[a]
  Z. Sawa]Zdeněk Sawa0000-0003-1268-3681[b]
  
  Dept of Comp. Sci., Faculty of Science, Palacký Univ. Olomouc, Czechia
  petr.jancar@upol.cz, petr.osicka@upol.cz
  
  Dept of Comp. Sci., FEI, Techn. Univ. Ostrava, Czechia
  zdenek.sawa@vsb.cz
  
  
  
  
  
  
    We answer an open complexity question by Hofman, Lasota, Mayr,
    Totzke (LMCS 2016) for simulation preorder on the class of succinct
    one-counter nets (, one-counter automata with no zero tests where
    counter increments and decrements are integers written in binary);
    the problem was known to be PSPACE-hard and in EXPSPACE.  We show
    that all relations between bisimulation equivalence and simulation
    preorder are EXPSPACE-hard for these nets; simulation preorder is
    thus EXPSPACE-complete.  The result is proven by a reduction from
    reachability games whose EXPSPACE-completeness in the case of
    succinct one-counter nets was shown by Hunter (RP 2015), by using
    other results.  We also provide a direct self-contained
    EXPSPACE-completeness proof for a special case of such reachability
    games, namely for a modification of countdown games that were shown
    EXPTIME-complete by Jurdzinski, Sproston, Laroussinie (LMCS 2008);
    in our modification the initial counter value is not given but is
    freely chosen by the first player.
  
    We also present an alternative proof for the upper bound by Hofman
    et al. In particular, we give a new simplified proof of the belt
    theorem that yields a simple graphic presentation of simulation
    preorder on (non-succinct) one-counter nets and leads to a
    polynomial-space algorithm (which is trivially extended to an
    exponential-space algorithm for succinct one-counter nets).
  
  
  Countdown games, and simulation on (succinct) one-counter nets
      [
      
  ==============================================================
  
  
  
  
  
  
  
  
  
  
  § INTRODUCTION
  
  One-counter automata (OCA), , finite automata
  equipped with a nonnegative counter,
  are studied as one of the simplest models
  of infinite-state systems. They can be viewed as a special case of
  Minsky counter machines, or as a special case of pushdown automata.
  In general, OCA can test the value of
  the counter for zero, , some transitions could be enabled only if the value
  of the counter is zero. One-counter nets (OCN) are a “monotonic” subclass of OCA where every
  transition enabled for zero is also enabled for nonzero values. As
  usual, we can consider
   deterministic, nondeterministic, and/or alternating versions of OCA
  and/or OCN.
  The basic versions are unary, where the
  counter can be incremented and decremented by one in one step,
  while in the succinct versions
  the possible changes can be arbitrary integers
  (but fixed for a given transition);
  as usual, the changes are assumed to be
  written in binary in a description of a given automaton.
  (Remark. In some papers the term “unary” is used differently,
  for machines with a single-letter input alphabet.)
  
  
  Problems that have been studied on OCA and OCN include reachability,
  equivalence, model checking, and also different kinds of
  games played on these automata.
  One of the earliest results
  showed decidability of (language)
  equivalence for deterministic OCA <cit.>.
  The open polynomiality
  question in <cit.>
  was positively answered in <cit.>, by showing
  that shortest distinguishing words of non-equivalent deterministic OCA have
  polynomial lengths. (We can refer, e.g.,
  to <cit.> for precise bounds in
  some related cases.)
  
  Later other behavioural equivalences (besides language equivalence)
  were studied. Most relevant for us is the research started by
  Abdulla and Čerāns who showed in <cit.> that
  simulation preorder on one-counter nets is decidable. An alternative proof
  of this fact was given in <cit.>;
  it was also noted that simulation
  equivalence is undecidable for OCA.
  A relation to bisimulation problems
  was shown in <cit.>.
  Kučera showed some lower bounds
  in <cit.>;
  Mayr <cit.> showed the undecidability of weak
  bisimulation equivalence on OCN.
  
  Simulation preorder
  on one-counter nets turned out -complete:
  the lower bound was shown by
  Srba <cit.>,
  and the upper bound
  by Hofman, Lasota, Mayr, and
  Totzke <cit.>.
  It was also shown in <cit.>
  that deciding weak simulation on OCN can be reduced to deciding strong simulation
  on OCN, and thus also solved in polynomial space.
  (Strong) bisimulation equivalence on OCA is also known to be
  -complete <cit.>
  (which also holds for a probabilistic version of
  OCA <cit.>).
  We note that -membership of problems for the unary case easily
  yields -membership for the succinct (binary) case.
  
  Succinct (and
  parametric)
  OCA were considered, e.g., in <cit.>, where
  reachability on succinct OCA was shown to be -complete.
  Games studied on OCA include, e.g., parity games
  on one-counter processes (with test for
  zero) <cit.>,
  and are closely related to counter reachability games
  (e.g. <cit.>).
  Model checking problems on OCA were studied for many types of
  logics, ,  LTL <cit.>,
  branching time logics <cit.>, or
  first-order logics <cit.>.
  -lower bounds for some model-checking (and also equivalence checking)
  problems were shown in <cit.>.
  A recent study <cit.>
  deals with parameterized universality problems for one-counter
  nets.
  
  
  An involved result by Göller, Haase, Ouaknine,
  Worrell <cit.> shows that model
  checking a fixed CTL formula on succinct one-counter automata
  is -hard.
  The proof is nontrivial, using two involved
  results from complexity theory.
  The technique of this proof was
  referred to by Hunter <cit.>,
  to derive -hardness of reachability games
  on succinct OCN.
  
  
  
  
    
  Our contribution
  In this paper we close a complexity gap for the simulation problem on
  succinct OCN that
  was mentioned in <cit.>, noting that
  there was a lower bound
  and an upper bound for the problem.
  We show -hardness (and thus -completeness)
  of the problem, using a defender-choice technique
  (cf., e.g., <cit.>)
  to reduce reachability games to any relation between
  simulation preorder and bisimulation equivalence.
  Further contributions are explained below in more detail.
  
  
  As already mentioned, the -hardness of reachability games on
  succinct OCNs was shown
  in <cit.>
  by using <cit.>.
  Here we present a direct proof
  of -hardness (and completeness) even for a special case
  of reachability games,
   which we call the “existential countdown
  games”. It is a mild relaxation
  of the countdown games from <cit.>
  (or their variant from <cit.>),
  which is an interesting -complete problem.
  We thus provide a  simple -hardness proof (in fact, by a
  master reduction via a natural intermediate problem dealing with
  ultimately periodic words)
  that is
  independent
  of <cit.> (and of the
  involved technique from <cit.>
  used by <cit.>).
  
  We now give an informal sketch
  of the results for countdown games.
  
  The left-hand part of Figure <ref> shows an
  example of a very simple countdown
  game. It is, in fact, a special finite automaton, with Eve's states, in our case
  just p_1, and Adam's states,
  in our case just p_2. The game assumes a nonnegative counter whose
  value is modified by transitions; in the countdown
  games the counter is only decreased by transitions. E.g., in the configuration
  p_1(185), i.e. in the situation where the current state is p_1 and the current counter value is
  185, Eve can choose the transition p_1-24p_1, which changes the
  current configuration to p_1(185-24), i.e. to p_1(161), or the transition p_1-1p_2, which changes the
  current configuration to p_2(184). In p_2(184) Adam has two choices,
  either going to p_2(159) or to p_2(181).
  Since the counter cannot become negative, in p_2(17) Adam has
  one choice only, necessarily reaching p_2(2) by several steps, where the respective
  play finishes.
  Eve's goal is that the play finishes
  in p_win(0) for a distinguished state p_win; in our example we
  put p_win=p_2.
  
  It is obvious that an initial configuration p_2(n) is
  winning for Eve iff n ∈{0,3,6,9,12,15, 18,21,24} as partly
  depicted in the right-hand part of
  Figure <ref> by the white points.
  (The black points thus correspond to the configurations where
  Adam has a winning strategy; e.g., p_2(7) is winning for Adam.)
  An initial configurations p_1(n) is winning for Eve
  (i.e., Eve has a strategy guaranteeing reaching
  p_2(0)), iff  n 3=1.
  
  Our concrete example is simple, but also
  in the general case, with states p_1,p_2,…,p_k (distributed
  between Eve and Adam),
  it is straightforward to stepwise fill the respective
  “black-white-points table”
  in the bottom-up fashion that we now describe.
  The “points” p_1(0), p_2(0),…, p_k(0) are black except of
  p_i(0) where p_i=p_win since p_win(0) is white.
  If we have filled the rows 0,1,…,ℓ (hence each p_i(j) where
  i∈{1,2,…,k} and j∈{0,1,…,ℓ} has been determined to
  be black or white), it is trivial to fill the row ℓ+1:
  p_i(ℓ+1) becomes white iff p_i belongs to Eve and there is a
  move from p_i(ℓ+1) to an already established white point (in the
  rows 0,1,…,ℓ), or
   p_i belongs to Adam, there is a move from p_i(ℓ+1), and each
  such move
  leads to an already established white point.
  
  It is thus clear that the question if p(n) is Eve's win is in :
  we fill the “rows” for 0,1,2,…,n, using exponential time and
  space in the input size, since n and the countdown values are given
  in binary or in decimal notation.
  We also note that if m  is the maximum countdown value (which is
  25 in Figure <ref>),
  the row ℓ≥ m is determined by the rows ℓ-1,
  ℓ-2,…,ℓ-m.
  It is thus clear that deciding the “existential version” of the
  countdown games, i.e. the question, given a state p, if there is
  n such that p(n) is winning for Eve, can be decided in exponential
  space. (When filling the table in the bottom-up fashion, we can always keep just last m rows
  in memory.) We can also observe that
  the black-white table is thus (ultimately) periodic,
  with an at most double-exponential period; the period is indeed
  double-exponential in concrete cases, as we also show in this paper.
  
  The lower bounds might look more surprising:
  deciding if p(n) is Eve's win is
  -complete <cit.>, while
  deciding if there is n such that  p(n) is Eve's win is
  -complete, as we show in this paper.
  In fact, these lower bounds (-hardness and -hardness)
  can be also relatively easily established,
  when looking at the “bottom-up” computation-table
  of an exponential-space Turing machine in a convenient way, as is
  depicted in and discussed around Figure <ref>.
  
  
  Regarding the simulation problem, we give an example of a succinct one-counter
  net in Figure <ref>; it is also a finite automaton equipped
  with a nonnegative counter. Now there is no Eve or Adam, and the
  counter changes associated with transitions can be also nonnegative; moreover, the
  transitions have action-labels (a,b in our example).
  
  On the set of all configurations p(n), the simulation preorder
   
  is the maximal relation such that
  for each pair p(m) q(n) and each move
  p(m)ap'(m') there is a move q(n)aq'(n') (with the same
  label a) such that
  p'(m') q'(n').
  In our example we can note that
  p_2(3) p_1(58), since the move
  p_2(3)bp_2(1) cannot be answered by any b-transition from
  p_1(58); on the other hand, we have p_2(1) p_1(58), since
   no transition is enabled in p_2(1). Slightly more subtle is to note that
   p_1(0) p_2(6): the move p_1(0)ap_2(5) is answered by
   p_2(6)ap_2(4), and we check that p_2(5) p_2(4).
  
  
  We can also think in terms of games here.
  In the simulation game a position is not just one configuration, but a
  pair (p(m),q(n)) of configurations. The first player, called
  Attacker (or Spoiler), chooses a move p(m)ap'(m') (Attacker
  loses if there is no such move), and the
  other player, called Defender (or Duplicator), answers by some
   q(n)aq'(n') (with the same label a); Defender loses if
   there is no such answer. The play then continues with the next round,
  with the current pair  (p'(m'),q'(n')).
   An infinite play is deemed to be winning for
   Defender. It is standard to observe that p(m) q(n) iff
   Attacker has a winning strategy from (p(m),q(n))
   (and p(m) q(n) iff
   Defender has a winning strategy from (p(m),q(n))).
  
  Given a succinct one-counter net,
  we can represent the relation  by
  the respective “black-white colourings” C_p,q of the integer points in the
  first quadrant of the plane, for each ordered pair of states
  p,q; white points correspond to Attacker's
  wins, black points correspond to Defender's
  wins.
  In our example we have four ordered pairs of states
  ((p_1,p_1),(p_1,p_2),(p_2,p_1),(p_2,p_2)), and the respective four
  colourings are depicted in Figure <ref>.
  
  E.g., p_2(1) p_1(n) and p_2(2) p_1(n)
  for all n, p_1(0) p_2(5) and   p_1(0) p_2(6),
  etc.
  
  We can easily observe the general monotonicity: if
   p(m) q(n) then p(m') q(n') for all m'≤ m and
   n'≥ n.
  Our example also suggests that the black-white frontier in each
  colouring
  is contained in a “linear belt”, with a rational (or infinite) slope
  and a certain width. Such a belt (two parallel lines)
  in C_p_1,p_2 in
  Figure <ref> can be described as follows:
  the frontier points, which we can define as
  the rightmost black points in each row, have
  coordinates (0,6), (0,7), (1,8), (1,9), (2,10), (2,11), ⋯ and
  are contained in a belt with the slope 2/1 and the vertical
  width 1.
  (A more general form is depicted in Figure <ref>.)
  
  Contemplating a bit,
  it is not difficult to get an intuition captured by a
  “belt theorem”, claiming that also in any general case of (succinct)
  one-counter nets the frontier in each plane is contained in a linear
  belt; moreover, it is intuitively obvious that each frontier is
  periodic, from some row onwards.
  (In this paper, we also show that the periods can be, and are at most,
  double-exponential.)
  By the previous figures and discussions, one can
  also easily get an intuition that deciding the countdown games,
  even in their (-complete) existential form, could be reduced
  to deciding the simulation preorder on (succinct)
  one-counter nets; finding a solution like the one depicted in
  Figure <ref> seems intuitively simpler than
  finding a solution like the one   depicted in
  Figure <ref>.
  This is confirmed in this paper, by a
   reduction based on a “defender-choice technique” that in particular
   enables to mimic Adam's choices in a countdown game by Defender's
   choices in the corresponding simulation game.
  
  The above mentioned belt theorem
  is important for the upper
  bounds, namely for showing that deciding simulation preorder is in for one-counter nets where the counter changes are presented in unary,
  and in for succinct one-counter nets.
  Proving the belt theorem had
  turned out surprisingly difficult; we also contribute to this topic
  here, as we explain below.
  The (non)succinctness of the one-counter
  nets plays no important role in this discussion, so we restrict ourselves to the
  cases in which the counter can change by at most 1 in one move.
  The qualitative form of the belt theorem (claiming just the existence of
  belts, not caring about their slopes, widths, and positions)
  followed from <cit.> where an involved
  mechanism of two-player games was used; this qualitative result was shown
  in <cit.> by another technique, based
  rather on “geometric” ideas. The quantitative form, stating that the
  linear belts, assumed to start in the origin (0,0),
  have the slopes and widths that can be presented as
  (fractions of) numbers with polynomially bounded values, was shown
  in <cit.>, by enhancing the technique
  of games from <cit.>; this is the crux
  of the -membership of simulation preorder for
  OCN <cit.> (which also yields the
  -membership for succinct OCN).
  
  In this paper we give a new self-contained proof for both the qualitative and quantitative
  versions of the belt theorem.
  One important new ingredient is a simple observation that we call
  a black-white vector travel.
  We describe it here, using Figure <ref>,
  but the description can be safely skipped if the
  reader finds it too technical; it is later captured by
  Proposition <ref> and Corollary <ref>.
  
  For any vector v_0 with a positive slope and with a black start and
  a white end in some colouring C_p_0,q_0,
   like the vector v_0 in Figure <ref>,
  there are vectors v_1,v_2,…,v_k of the same size and slope as
  v_0, each v_i being a black-white vector in some colouring C_p_i,q_i,
  such that
  
  	
    * for all i∈{1,2,…,k},
  v_i is a neighbour of v_i-1, i.e.,
  the x-coordinates of the starts of v_i and v_i-1 differ by at most 1, and
  the same constraint holds for their y-coordinates; and
  
    * the start of v_k is on the vertical axis.
  
  This can be easily verified: in the pair of configurations
  corresponding to the white end of v_0 Attacker has an optimal
   transition p_0a,zp_1,
  for which each Defender's response q_0a,z'q
  establishes a “white” pair with a smaller rank, i.e.,
  closer
  to Attacker's final win. Attacker can perform the transition
   p_0a,zp_1
  also
  in the pair of configurations
  corresponding to the black start of v_0, if this start is not on the
  vertical axis (which would entail that Attacker's counter is zero);
  there is at least one Defender's response
  q_0a,z_1q_1 establishing another “black” pair.
  Hence by changing the x-coordinate of v_0 by z and its
  y-coordinate by z_1 we get the vector v_1 that is black-white in the
  colouring C_p_1,q_1. Etc.
  
  This black-white vector travel, together with other enhancements,
  allowed us to substantially simplify
  the proof of the qualitative belt theorem
  from <cit.>. Moreover,
  the quantitative version can be now derived from the qualitative
  version by a few simple observations.
  
  
  
  
    
  Organization of the paper
  Section <ref> gives the basic definitions.
  In Section <ref> we show that the “existential” countdown
  games are -complete (which also yields
  an alternative proof for the known -completeness of countdown
  games).
  Section <ref> describes the reductions
  from reachability games to (bi)simulation relations, in a general
  framework and then in the framework of succinct OCN.
  Section <ref> contains new proofs for both the
  qualitative and quantitative versions of the belt theorem (leading to
  the
  membership for OCN).
  Section <ref> shows that the period of the belts
  in the succinct case can be double-exponential.
  We finish with some additional remarks in Section <ref>.
  
  
  
  
  
  
  
  
  § BASIC DEFINITIONS
  
  
  By , ,
  _>0
  we denote
  the sets of integers, of nonnegative integers, and of positive integers, respectively.
  We use [i,j], where i,j∈,
  for denoting the set {i,i+1,…,j}.
  
  
  
  
    
  Labelled transition systems and (bi)simulations
  A labelled transition system, an LTS for short, is a
  tuple
  
      = (S, Act, (a)_a∈ Act)
  
    where S is the set of states, Act is the set of
    actions,
    and a⊆ S × S is the set
  of  a-transitions (transitions labelled with a), for each
    a∈ Act.
    We write s t instead of
    (s,t) ∈.
  By s a we denote that a is enabled in s,
  , s a t for some t.
  
  
  Given = (S, Act, (a)_a∈ Act),
  a relation R ⊆ S × S is a simulation
    if for every (s,s')∈ R and every
    s  t there is s'  t' such that (t,t')∈ R;
    if, moreover, for every (s,s')∈ R and every
    s'  t' there is s  t such that (t,t')∈ R, then R
  is a bisimulation.
  
  The union of all simulations (on S) is the maximal
    simulation, denoted ; it is a preorder, called
    simulation preorder.
   The union of all bisimulations is the maximal
   bisimulation, denoted ; it is an equivalence, called
   bisimulation equivalence (or bisimilarity).
   We obviously have
   ⊆.
  
  
  We can write
   s_1 s_2 or s_1 s_2 also for states s_1,
   s_2 from different  LTSs _1, _2, in which case
   the LTS arising by the disjoint union of _1 and _2 is
   (implicitly) referred to.
  
  
  It is useful to think in terms of two-player turn-based games,
  played
  by Attacker and Defender (or Spoiler and Duplicator).
  A round
  of the simulation game from a (current) pair (s,s')
  proceeds as follows:
  Attacker chooses
  a transition sat, and Defender responds with some
  s'at' (for the action a chosen by Attacker); the play then
  continues with another round, now from the current pair  (t,t').
  If a player has no legal move in a round, then the other player wins;
  infinite plays are deemed to be Defender's wins.
  It is standard that s s' iff Attacker has a winning
  strategy from (s,s').
  
  The bisimulation game is analogous, but
  in any round starting from  (s,s')
  Attacker can choose to
  play  sat or s'at', and Defender has to respond
  with some s'at' or sat, respectively.
  Here we have s s' iff Attacker has a winning
  strategy from (s,s').
  
  
  
    
  Stratified simulation, and ranks of pairs of states
  Given
  = (S, Act, (a)_a∈ Act),
  we use (transfinite) induction to define the relations _λ
  where λ ranges over the class Ord of ordinals.
  We put _0=S× S. For λ>0 we have
  s_λs' if for each transition sat
  and each λ'<λ there is a
  transition s'at' where t_λ't'.
  
  We note that _λ'⊇_λ when
  λ'≤λ, and that =⋂_λ∈
  Ord_λ. For each pair (s,s')∉, we define
  its rank (s,s') as the least ordinal λ
  such that s_λs'.
  We note in particular that (s,s')=1 iff s enables an action a (i.e.,
  sa) that is not enabled in s' (i.e., s'a).
  
  
  
  
  We use such a general definition for the purpose of the general
  reduction presented in Section <ref>.
  Otherwise   we
  consider just (special cases of) LTSs that
  are image-finite (i.e., in which the sets
  {t| sat} are finite for all s∈ S, a∈ Act); in such
  systems
  we have =⋂_i∈_i and
  (s,s')∈ for each (s,s')∉.
  
  
  We could define the analogous concepts for bisimulation equivalence as
  well.
  
  
  
  
    
  One-counter nets (OCNs and SOCNs), and their
  associated LTSs
  A labelled one-counter net,
  or just a one-counter net or even
  just an OCN for short,
  is a triple
  
      =(Q,Act,δ),
  
  where Q is the finite set of control states, Act the finite
  set of actions,
  and δ⊆ Q × Act×{-1,0,+1}× Q is
  	the
  	set of (labelled transition) rules.
  By allowing δ  to be
  a finite subset of Q × Act×× Q,
  and presenting z∈ in the rules (q,a,z,q')
  in binary, we
  get a succinct one-counter net, or a SOCN for short.
  A rule (q,a,z,q') is usually presented as
  qa,zq'.
  
  Each OCN or SOCN =(Q,Act,δ)  has the associated LTS
  
      _=(Q×,Act,(a)_a∈ Act)
  
  where (q,m)a(q',n) iff qa,n-mq' is a rule in δ.
  We often write a state (q,m), which is also called a configuration,
  in the form q(m), and we view  m as a value of a nonnegative counter.
  A rule  qa,zq' thus induces transitions q(m)aq'(m+z) for
  all m≥max{0,-z}.
  
  We remark that one-counter automata extend one-counter nets
  by the ability to test zero, i.e., by transitions that are enabled only if the counter value is zero.
  
  
  
  
    
  Reachability games (r-games), winning areas, ranks of states
  We are interested in reachability games played in LTSs
  	associated with (succinct) one-counter nets, but we first define the
  	respective notions generally.
  
  By a reachability game, or an r-game for short, we mean
  a tuple
  
      =(V,V_∃, , ),
  
  where V is the set of states (or vertices),
  V_∃⊆ V is the set of Eve's states,
  ⊆V× V is the transition relation
  (or the set of transitions), and ⊆ V is the set
  of target states.
  By  Adam's states we mean  the elements of
  V_∀=V∖ V_∃.
  
  Eve's winning area
  is =⋃_λ∈ OrdW_λ, for Ord being
  the class of ordinals, where the sets W_λ⊆ V are defined
  inductively as follows.
  
  We put W_0=; for λ>0 we put
  W_<λ=⋃_λ'<λW_λ', and we
  stipulate:
  
  	
    * if s∉W_<λ, s∈ V_∃, and
  ss̅ for some s̅∈ W_<λ, then s∈ W_λ;
  	
    * if s∉W_<λ, s∈ V_∀,
  and we have ∅≠{s̅| ss̅}⊆
  W_<λ,
  then s∈ W_λ.
  
  (If (a) applies, then λ is surely a successor ordinal.)
  
  For each s∈, by (s) we denote (the unique)
  λ such that
  s∈ W_λ. A transition ss̅ is
  rank-reducing if (s)>(s̅).
  We note that for any s∈ with (s)>0 we have:
  if s∈ V_∃, then there is at least one rank-reducing
  transition ss̅ (in fact, (s)=(s̅)+1 in
  this case); if s∈ V_∀, then there is at least one
  transition ss̅ and all such transitions are rank-reducing.
  This entails that  is the set of states from which Eve has a
  strategy that guarantees reaching (some state in)  when Eve
  is choosing a next transition in Eve's states
  and Adam is choosing a next transition in Adam's states.
  
  
  
  
  We are primarily interested in the games that have  (at most)
  countably many states and are finitely branching (the sets
  {s̅| ss̅} are finite for all s). In such cases
  we have (s)∈ for each s∈.
  We have again introduced the general definition for the purpose of the
  reduction in Section <ref>.
  
  
  
  
  
  
    
  Reachability games on succinct one-counter nets
  We now define specific r-games,
  presented by SOCNs
   with
  partitioned
  control-state sets; these succinct one-counter nets are
  unlabelled, which means that the set of actions can be always deemed to be
  a singleton.
  
  
  
  By a succinct one-counter net reachability game, a socn-r-game for short, we
  mean a tuple
  
      =(Q,Q_∃,δ,p_win)
  
  where Q is the finite set of (control) states,
  Q_∃⊆ Q is the set of Eve's (control) states,
  p_win∈ Q is the target (control) state, and
  δ⊆ Q×× Q is the finite set of
  (transition) rules.
  We often present a rule (q,z,q')∈δ as
  qzq'.
  By Adam's (control) states we
  mean the elements of Q_∀=Q∖ Q_∃.
  A socn-r-game =(Q,Q_∃,δ,p_win) has the
  associated r-game
  
      _=(Q×,Q_∃×,,{(,0)})
  
  where (q,m)(q',n) iff qn-mq' is a rule (in δ).
  We often write q(m) instead of (q,m) for states of _.
  
  We define the problem (to decide succinct
  one-counter net r-games) as follows:
  
  
  a socn-r-game 
  (with integers z in rules qzq' written in binary), 
  
   and a control state p_0.
  is p_0(0)∈ in the game _ ?
  
  
  
  
  
  We have defined the target states (in _) to be the
  singleton set {(0)}.
  There are other natural variants
  (e.g., one in <cit.> defines the target set
   {p(0)| p≠ p_0})
  that can be easily shown to be essentially equivalent.
  
  
  
  
  The -hardness of was announced in <cit.>, where
  an idea of a proof
  is sketched, also using a reference
  to an involved result <cit.>
  (which is further discussed in Section <ref>).
  In Section <ref> we give a direct self-contained proof that does not rely
  on <cit.>
  or involved techniques from <cit.>, and that
  even shows
  that is -hard already in the special
  case that slightly generalizes the countdown games
  from <cit.>.
  (The -membership follows from <cit.>,
  but we add a short proof to be self-contained.)
  
  
  
  
    
  Countdown games
  We define a countdown game
  as a socn-r-game =(Q,Q_∃,δ,p_win), where in every
  rule q z q' in δ we have z < 0.
  The problem is defined as follows:
  
  
  	(countdown games)
  a countdown game  (with integers in
     rules written in binary), 
  
     and an initial configuration
     p_0(n_0) where n_0∈ (n_0 in binary).
  is p_0(n_0) ∈ ?
  
  
  The problem (in an equivalent form) was shown -complete
  in <cit.>.
  Here we define an existential version, the problem :
  
  
  (existential countdown games)
  a countdown game  and a control state p_0.
  is there some n∈ such that p_0(n) ∈ ?
  
  
  We note that can be viewed as a subproblem of :
  given an instance of , it suffices to add a fresh
  Eve's state p'_0  and rules p'_0 1 p'_0, p'_00p_0;
  the question then is if p'_0(0)∈.
  
  
  
  
  
  
  
  
  § EXPSPACE-COMPLETENESS
  OF EXISTENTIAL COUNTDOWN GAMES
  
  
  
  In this section we prove the following new theorem.
  
  
  (existential countdown game) is -complete.
  
  Our -hardness proof of ECG
  is, in fact, a particular instance of a simple general method.
  A slight modification also yields a proof of
  -hardness of countdown games that is an alternative to the
  proof in <cit.>
  and in <cit.>.
  
  
  	<cit.>
  is -complete.
  
  
  In the rest of this section we present
  the proofs of Theorems <ref>
  and <ref> together, since they
  only differ by a small detail.
  We start with the upper bounds since these are obvious.
  
  
  
   §.§ ECG is in EXPSPACE (and CG in
  EXPTIME)
  
  
  Let us consider an -instance
  =(Q,Q_∃,δ,p_win), p_0.
  By m we denote
  the maximum value by which the counter can be decremented in one
  step (i.e., m=max { |z| ; there is some q z q'
  in δ }); the value m is at most exponential
  in the size of the instance , p_0.
  
  We can stepwise construct
   W(0), W(1), W(2), … where W(j)={q∈ Q| q(j)∈};
  the -instance , p_0 is positive iff p_0∈ W(j) for some
  j.
  We have W(0)={p_win}, and
  for determining W(n) (n≥ 1)
  it suffices to know the segment
  W(n-m'), W(n-m'+1), …, W(n-1)
  where m'=min{m,n}. Hence, during the
  construction of W(j), j=0,1,2,…,
  it suffices to remember just the segment
  W(j-m'), W(j-m'+1), …, W(j-1)
  (where m'≤m). Obviously, if for some j,j', where m≤ j < j', the
  segments
  W(j-m), …, W(j-1) and
  W(j'-m), …, W(j'-1) are the same
  (, if W(j-k) = W(j'-k) for each k=1,2,…,m),
  then also W(j+k) = W(j'+k) for each k∈, so the sequence
  repeats itself with a period j'-j.
  By the pigeonhole principle, this surely happens for some
  j,j' such that j<j'≤m+2^|Q|·m
  because there are at most 2^|Q|·m segments of
  length m.
  This means that in the algorithm that checks whether p_0∈ W(j) for
  some j∈, the computation can be stopped after
  constructing W(m+2^|Q|·m).
  The size of a binary counter serving to count till the
  (at most double-exponential) value m+2^|Q|·m
  is at most exponential.
  Therefore belongs to .
  
  It is also clear that is in , since for the instance
  , p_0(n_0) we can simply construct
  W(0), W(1), W(2), …, W(n_0).
  
  
  
  
  
  
   §.§ ECG is EXPSPACE-hard (and CG EXPTIME-hard)
  
  
  In principle, we use a “master” reduction.
  We fix an arbitrary language L
  in , in an alphabet Σ (hence L⊆Σ^*),
  decided by a (deterministic) Turing machine 
  in space 2^p(n) for a fixed polynomial p.
  For any word w∈Σ^*, w=n,
  there is the respective computation of  using
  at most m=2^p(n) tape cells, which is accepting iff w∈ L.
  Our aim is to show a construction of a countdown game ,
  with a specified control state p_0, such that
  there is k∈ for which p_0(k)∈ if, and only if,
   accepts w. The construction of   will be polynomial,
  in the size n=w; this will establish that  is
  -hard.
  (In fact, this polynomial construction easily yields a
  logspace-reduction, but this detail is unimportant at our level of
  discussion.)
  
  In fact, the same construction of  will also show
  -hardness of . In this case we assume that
  L is decided by a Turing machine 
  in time (and thus also space) 2^p(n), and we construct a concrete
  exponential value n_0 guaranteeing that
  p_0(n_0)∈ iff
   accepts w.
  
  
  
  
  
  
  
  
    
  Construction informally
  The construction of the countdown game  elaborates an
  idea that is already present in
  <cit.> (in Theorem 3.4) and that was
  also used, e.g., in <cit.>.
  We first present the construction informally.
  
  Figure <ref> presents an accepting computation of , on a
  word
  w=a_1a_2… a_n; it starts in the initial control state q_0 with the
  head scanning a_1.  The computation is a sequence of configurations
  C^w_0,C^w_1,…,C^w_t, where C^w_t is accepting (since the control
  state is ). We assume that  never leaves cells 0… m-1
  of its tape during the computation. Hence each C^w_i can be
  presented
  as a word of length m over
  the alphabet Δ=(Q×Γ) ∪Γ where Q and Γ are the
  set of control states and the tape alphabet of , respectively;
  by ∈Γ we denote the special blank tape symbol.
  We refer to the (bottom-up) presentation of
  C^w_0,C^w_1,…,C^w_t depicted in Figure <ref> as to
  a computation table.
  
  Given m,
  each number k∈ determines the cell j
  in the “row” i (i.e., in the potential C^w_i) where i=k÷ m
  (÷ being integer division)
  and j=k m; we refer by (k) to this cell j in the row
  i.
  
  For k>m, if (k) is in the computation table (k≤ t· m
  in Figure <ref>), then
  the symbol β in (k) in the table is surely
   determined by the symbols β_1,β_2,β_3 in
  the cells  (k-m-1),  (k-m), (k-m+1)
  (and by the transition function of the
  respective Turing machine ); see
  Figure <ref> for illustration (where also the cases
  β' and β” on the “border” are depicted). The transition function of  allows
  us to define which triples (β_1,β_2,β_3) are
  eligible for β, i.e., those that can
  be in the cells
  (k-m-1),  (k-m), (k-m+1) when β
  is in (k) (these triples are independent of k, assuming
  k>m).
  
  
  Let us now imagine a game between Eve and Adam
  where Eve, given w, claims that w is
  accepted by , in space m
  (in our case m=2^p(|w|) for a respective polynomial p).
  Eve does not present a respective accepting
  computation table
  but she starts a play by producing a tape-symbol x and
  a number k_0∈, i.e. sets a counter
  to k_0,
  claiming that (k_0) in the computation table
  contains (,x) (in Figure <ref> the correct values
  are k_0=t· m and x=).
  Then the play proceeds as follows.
  If Eve claims that β is the symbol in (k) for the current
  counter value k, while also claiming that k>m, then she
   decreases the counter by m-2 and produces a triple
  (β_1,β_2,β_3) that is eligible for β,
  thus claiming that (k-m-1), (k-m),(k-m+1)
  contain β_1,β_2,β_3, respectively.
  Adam then decreases the counter either by 3, asking to verify the
  claim that
  (k-m-1) contains β_1, or by 2, asking to verify
  that (k-m) contains β_2, or by 1, asking to verify
  that  (k-m+1) contains β_3. Eve then again produces
  an eligible triple for the current symbol, etc., until claiming that
  the counter value is k≤ m (which can be contradicted by Adam
  when he is able to decrease the counter by m+1). The last phase
  just implements checking if the symbol claimed for (k)
  corresponds to the initial configuration.
  
  It is clear that Eve has a winning strategy in this game if
  w is accepted by  (in space m). If w is not accepted,
  then Eve's first claim does not correspond to the real computation
  table. Moreover, if a claim by Eve is incorrect, then at least
  one claim for any respective
  eligible triple is also incorrect (as can be easily
  checked), hence Adam can be always asking to
  verify incorrect claims, which is revealed when the consistency with
  the initial
  configuration is verified in the end. Hence Eve has
  no winning strategy if w is not accepted by .
  
  In the formal construction presented below
  we proceed by introducing an intermediate auxiliary problem (in
  two versions) that
  allows us to avoid some technicalities in the construction
  of countdown games . Roughly speaking, instead of the
  computation of  on w we consider the computation of _w
  on the empty word, which first writes w on the tape and then
  invokes ;
  checking
  the consistency with the (empty) initial configuration is then
  technically easier
  to handle in the constructed countdown game.
  
  
  
  
    
  Construction formally
  Now we formalize the above idea, using the announced intermediate
  problem.
  
  
  
  By a sequence description we mean a tuple =(Δ, D, m),
  where Δ is its finite alphabet, always containing two special symbols
   and 
  (and other symbols),
  D: Δ^3 →Δ is its description function,
  and m≥ 3 is its initial length.
  The sequence description =(Δ,D,m) defines the infinite
  sequence  in Δ^ω, i.e.
  the function  : →Δ, that is defined
   inductively as follows:
  
  
    * (0)=,
  
    * (1)=(2)=⋯=(m)=,
  
    * for i > m we have (i)=D(β_1,β_2,β_3)
  	where β_1=(i-m-1),
  		β_2=(i-m), and β_3=(i-m+1).
  
  The two versions of the announced intermediate problem
  are defined as follows:
  
  (sequence problem)
  A sequence description =(Δ, D, m), n_0∈,
     and β_0∈Δ (with m and n_0 written in binary).
  Is (n_0)=β_0 ?
  
  
  
  (existential sequence problem)
  A sequence description =(Δ, D, m), and
     β_0∈Δ (with m written in binary).
  Is there i∈ such that (i)=β_0 ?
  
  
  Our informal discussion around Figure <ref>
  (including the remark on _w starting with the empty tape)
  makes (almost) clear that
  
  	
    * is -complete, and
  
    * is -complete.
  
  
  
  In fact, we would get the same complexity results even if
  we restricted D in =(Δ, D, m) to D:Δ^2→Δ
  and defined (i)=D((i-m-1,(i-m)) for i>m.
  (We would simulate  by a Turing machine ' that only
  moves to the right in each step, while working on a circular tape of
  length m.) But this technical enhancement would not simplify our construction of the
  countdown games , in fact.
  
  
  
  Formally it suffices for us to claim just the lower bounds:
  
  
  
  is
  -hard
  	and
  is
  -hard.
  
  
  To show -hardness
  	of ,
  we	assume an arbitrary
  fixed language L⊆Σ^* in ,
  decided by a Turing machine  in space  2^p(n) for a
  	polynomial p.
  
  Using a standard notation,
  	let =(Q,Σ,Γ,δ,q_0,{,})
  where Σ⊆Γ,
  ∈Γ∖Σ, ∉Γ,
  and  δ: Q×Γ→
    Q×Γ×{-1,0,+1} is the transition function of
  	, satisfying δ(,x)=(,x,0) and
  	δ(,x)=(,x,0) (hence an accepting or
  	rejecting configuration is formally viewed as repeated forever).
  Moreover, w.l.o.g. we assume that
  the computation of  on w=a_1a_2⋯ a_n∈Σ^*
  starts with w written in tape cells 1,2,…,n with the head
  	scanning the cell 1 (the control state being q_0),
  	the computation never leaves the cells 0,1,…,m-1 for
   m=2^p(n), never rewrites  in the cell 0,
  	and the state
  	, can only be entered when the head is scanning
  	the cell 0 (as is also depicted in
  	Figure <ref>);
  	we also assume that p is such that m=2^p(n) satisfies
  	m>n
  	and m≥ 3.
  
  Given w∈Σ^*, we now aim to show a polynomial construction
  	of _w=(Δ_w,D_w,m), where
  	m=2^p(|w|), such that
  	w∈ L iff there is i∈ such that
  	(i)=(,). (Hence w is reduced to the
  	-instance _w, β_0 where
  	β_0=(,).)
  
  	As already suggested in the previous discussion, for
  	w=a_1a_2⋯ a_n
  	we first construct a Turing machine
  	M_w that starts with the empty tape while scanning the cell 0
  	in its initial state q'_0, then by moving to the right it
  	writes w=a_1a_2⋯ a_n in
  	the cells 1,2,…,n, after which it moves the head to the cell 1 and
  	enters q_0, thus invoking the computation of  on w.
  
  When we consider the computation of M_w on the empty word
  as the sequence S=C_0C_1C_2… of configurations of length m,
  	where m=2^p(|w|), and we view the symbol (q'_0,) as
  	, then we observe that S(0)=,
  	S(1)=S(2)=⋯=S(m)=, and for i>m the symbol
  	S(i) is determined by S(i-m-1), S(i-m),
  S(i-m+1) and the transition function of _w, independently
  	of the actual value of i. The symbols in
  	Δ_w and the function D_w, guaranteeing
  	 =S, are thus obvious.
  
  A polynomial reduction from L to  is therefore clear,
  yielding -hardness of .
  
  In the case of , we assume that  deciding L
  works in time (and thus also space) 2^p(n); to the
  -instance , β_0=(,)
  constructed to w as  above we
  simply add n_0=m^2 (for m=2^p(|w|)), to get a -instance.
  Here it is clear that w∈ L iff
  (n_0)=β_0.
  This yields -hardness of .
  
  
  
  We now show polynomial (in fact, logspace) reductions from to and
  from to . Again, we present both reductions together.
  
  Given a sequence description =(Δ,D,m) (where ,
  ∈Δ), we construct the
  countdown game
  
      = (Q,Q_∃, δ, )
  
  where
  
  
    * Q_∃={, ,p_1} ∪ {s_β|β∈Δ},
  
    * Q_∀={p_2} ∪ { t_(β_1,β_2,β_3) | β_1,β_2,β_3∈Δ}
  
  (recall that Q=Q_∃∪Q_∀),
  and the set δ consists of the rules
  in Figure <ref>
  (for all β,β_1,β_2,β_3∈Δ).
  (Note that the rules for states  and  also
   include the rules of the form (5).)
  
  
  
  
  
  
  The idea is that the configuration s_β(k) of 
  should “claim” that (k)=β (and Eve should have a winning
  strategy from  s_β(k) iff this claim is correct). For technical
  reasons we add 2 to the counter, hence it is s_β(k+2) that “claims”
    (k)=β.
  
  
  
  
  For each β∈Δ we have s_β(0) ∉,
  	s_β(1) ∉,
  	and for each k∈
  	we have s_β(k+2)∈ iff
  (k)=β.
  
  
  We start by noting the following
  facts that are easy to check (recall that Eve wins iff the configuration
  (0) is reached):
  
    
    * (k)∈ iff k=0;  (k)∉ for all k∈;
    
    * p_1(k)∈ iff k ≥ 1;  p_2(k)∈ iff k∈[2, m+1];
    
    * for each β∈Δ, s_β(0) ∉ and
  s_β(1) ∉;
    
    * (2)∈ (recall that
  	  (0)=);
  
    
    * (k+2) ∈ for each k∈[1, m]
  	
  
  		(recall that
  	(1)=(2)=⋯=(m)=).
  
  	The statement of the lemma for s_β(0) and  s_β(1)
  	follows from the fact (c). To prove
  that s_β(k+2)∈ iff (k)=β,
  	we proceed by induction on k:
  
  
    * Base case k∈[0,m]: First we note that Eve cannot win
     in s_β(k+2) by playing any rule of the form (5) because
  		either this
     cannot be played at all, or
  		
      s_β(k+2) -(m-2)(k')
  
     where k'≤ 4, and Adam either cannot continue in (k'), or he
     can play to s_β_ℓ(k”) for some ℓ∈{1,2,3} with k”<2,
     which is losing for Eve (fact (c)).
  		Now it easily follows from the facts (d) and (e) that Eve wins in
     s_β(k+2) exactly in those cases where either β= and
     k=0 (fact (d)), or β= and k∈[1,m]
     (fact (e)).
  
  
    * Induction step for k>m:  Eve
  	cannot win
     in s_β(k+2) by playing a rule of the form (3) or (4),
   so she is forced to use a rule from (5), , to play a transition of the form
  
      s_β(k+2) -(m-2)(k')
  
  			where D(β_1,β_2,β_3)=β
  		and k'=k-m+4≥ 5. By this, she chooses a triple
     (β_1,β_2,β_3) where β_1, β_2,
  		β_3 are symbols supposedly occurring on
  		positions k-m-1,
  		k-m, and k-m+1 in .
     Now Adam can challenge some of the symbols β_1, β_2, β_3
     by choosing ℓ∈{1,2,3} and playing
  		
      (k') -(4-ℓ)
      		s_β_ℓ(k”)
  
  		where
  		k”= k-m+ℓ≥ 2.
     Either β is correct (, (k)=β), and then Eve can choose correct
     β_1, β_2, β_3, or
     β is incorrect (, (k)≠β), and then at least one of
     β_1, β_2, β_3 must be also incorrect.
     Since, by the induction hypothesis, Adam can win in (k')  iff one of
     β_1, β_2, β_3 is incorrect (by choosing
     the corresponding move for this incorrect β_ℓ), Eve can
     win in s_β(k+2) iff β is correct.
     From this we derive that
  	s_β(k+2)∈ iff (k)=β.
     
  
  
  Hence,
  for a given -instance , β_0
  (where =(Δ,D,m)) there is i∈
  such that (i)=β_0 iff there is k∈ such that
  s_β_0(k)∈ for . Moreover,
   (n_0)=β_0 iff s_β_0(n_0+2)∈.
  Recalling Proposition <ref>,
  we have thus established the lower bounds in
  Theorems <ref> and <ref>.
  
  
  
  
  
  
  
  § REACHABILITY GAME REDUCES
  TO (BI)SIMULATION GAME
  
  
  
  
  
  
  
  We show a reduction for general r-games,
  and then apply it to the case of socn-r-games.
  This yields a logspace reduction of to behavioural
  relations between bisimulation equivalence and simulation preorder.
  
  Recalling the -hardness
  of (from <cit.>, or
  from the stronger statement of Theorem <ref>),
  the respective lemmas (Lemma <ref>
  and <ref>) will yield the following theorem (which also
  answers the respective open question from <cit.>):
  
  
  	For succinct labelled one-counter net (SOCNs),
          deciding membership problem in any relation
          containing bisimulation equivalence and contained in simulation preorder
          (of the associated LTSs) is -hard.
  
  
  
  
  
   §.§ Reduction in a General Framework
  
  
  
  We start with an informal introduction to the reduction, which is an
  application of the technique
  called “Defender's forcing” in <cit.>.
  
  Any r-game =(V,V_∃, , ) gives rise to the LTS
  =(V,Act,(a)_a∈ Act) where
  Act={a_⟨ s,s̅⟩|
  ss̅} ∪ {a_win},
  a_⟨ s,s̅⟩={(s,s̅)}, and
  a_win={(s,s)| s∈}; hence each
  transition gets its unique action-label, and each target state gets a
  loop labelled by Eve's winning action a_win.
  Let ' be a copy of  with
  the state set V'={s'| s∈ V} but without the action a_win.
  We thus have
  sa_⟨ s,s̅⟩s̅ in  iff
  s'a_⟨ s,s̅⟩s̅' in ',
  and  for s∈ we have
  s s'
  in the disjoint union of  and '
  (since a_win is enabled in
  s but not in s').
  If V_∃=V (in each state it is Eve who chooses the next
  transition), then we easily observe that
  
      s∈ entails s s'
      	and  s∉ entails s s'.
  
  	A technical problem is how to achieve (<ref>) in
  	the case V_∃≠ V; in this case also Adam's choices
  	in the r-game have to be faithfully mimicked in the
  	(bi)simulation game, where it is now Defender who should force
  	the outcome of the relevant game rounds.
  	This is accomplished by adding “intermediate” states and
  	transitions, and the
  	“choice action” a_c, as
  	depicted in Figure <ref> (and discussed later
  	in detail); Attacker must let Defender to really choose since
  	otherwise Defender wins by reaching a pair (s,s) with the equal
  	sides (where s s).
  
  
  Now we formalize the above sketch.
  We assume an r-game , and we define a “mimicking” LTS
  () (the enhanced union of the above LTSs  and ').
  In illustrating Figures <ref> and <ref> we now
  ignore the bracketed parts of transition-labels;
  hence, e.g., in Figure <ref> we can see the
  transition s_1s_2 in  on the left
  and the (corresponding) transitions  s_1a^1_2s_2
  and s'_1a^1_2s'_2
  in () on the right.
  Let =(V,V_∃, , ),
  where V_∀ = V∖ V_∃;
  we define ()=(S,Act,(a)_a∈ Act) as follows.
  We put
  
  
  	S=V∪ V'∪{⟨ s,s̅⟩| s∈ V_∀,
  	ss̅}∪{⟨ s,X⟩|
  s∈ V_∀, X={s̅| ss̅}≠∅}
  
  
  where V'={s'| s∈ V} is a “copy” of V.
  (In Figure <ref>
  we write, e.g., s^1_3 instead of
  ⟨ s_1,s_3⟩,
  and s^1_23 instead of
  ⟨ s_1,{s_2,s_3}⟩.)
  
  We put
  Act={a_c,a_win}∪{a_⟨ s,s̅⟩|
  ss̅}
  and define a for a∈ Act as follows.
  If s∈ V_∃ and ss̅, then
  		sa_⟨ s,s̅⟩s̅ and
  		s'a_⟨ s,s̅⟩s̅'
  		(in Figure <ref> we write, e.g., a^1_3 instead of
  	a_⟨ s_1,s_3⟩).
  If s∈ V_∀ and
   X={s̅| ss̅}≠∅,
   then:
  
  	
    * 
  
   sa_c⟨ s,X⟩,
  		and sa_c⟨ s,s̅⟩,
  		s'a_c⟨ s,s̅⟩
  		for all s̅∈ X
  	(cf. Figure <ref>
  	where s=s_1 and X={s_2,s_3};
          a_c is a “choice-action”);
  
  
    * for each s̅∈ X we have
  ⟨ s,X⟩a_⟨
  s,s̅⟩s̅
  and ⟨ s,s̅⟩a_⟨
  s,s̅⟩s̅';
  moreover, for each s̅̅̅∈ X∖{s̅}
  we have ⟨ s,s̅⟩a_⟨
  s,s̅̅̅⟩s̅̅̅
  (e.g., in Figure <ref> we thus have
  s^1_2a^1_2s'_2 and s^1_2a^1_3s_3).
  
  
  For each s∈ we have sa_win s
  (for special a_win that is not enabled in s').
  
  
  
  
  
  
  
  
  For an r-game =(V,V_∃, , ),
  and the LTS ()=(S,Act,(a)_a∈ Act), the following conditions
  hold for every
  s∈ V and every relation
  	ρ satisfying
  	⊆ρ⊆:
  	
  		
    * if	s∈ (in ), then s s' (in
  ()) and thus (s,s')∉ρ;
  
    * if s∉, then s s' and thus (s,s')∈ρ.
   
  
  
  a) For the sake of contradiction suppose that there is s∈
  such that s s'; we consider such s∈ with
  the least rank.
  We note that (s)>0,
  since s∈ entails s s' due to the
  	transition sa_win s.
  If s∈ V_∃, then let ss̅ be a rank-reducing
  transition. Attacker's move sa_⟨ s,s̅⟩s̅, from the pair (s,s'),
  must be responded with s'a_⟨ s,s̅⟩s̅';
  but we have s̅s̅' by the “least-rank”
  assumption,
  which contradicts the assumption s s'.
  If s∈ V_∀, then X={s̅| ss̅} is
  nonempty (since s∈) and
  (s̅)<(s) for all s̅∈ X.
  For the pair  (s,s')
  we now consider Attacker's move
  sa_c⟨ s,X ⟩. Defender can choose
  s'a_c⟨ s,s̅⟩ for any s̅∈ X
  (recall that (s̅)<(s)).
  In the current pair (⟨ s,X ⟩, ⟨ s,s̅⟩)
  Attacker can play ⟨ s,X ⟩a_⟨ s,s̅⟩s̅, and this must be responded by
  ⟨ s,s̅⟩a_⟨ s,s̅⟩s̅'. But we again have
  s̅s̅' by the “least-rank” assumption,
  which contradicts s s'.
  
  
  b) It is easy to verify that the following set
  is a bisimulation in ():
  
  
  I∪{(s,s')| s∈ V∖}∪{(⟨ s,X ⟩, ⟨ s,s̅⟩)|
   s∈ V_∀∖, s̅∈ V∖}
  
  
  where I={(s,s)| s∈ S}.
  
  
  We note that the transitions
  s_1a_cs^1_2 and s_1a_cs^1_3
  in Figure <ref>
  could be omitted if we only wanted to show
  that s∈ iff s s'.
  
  
  
   §.§ Socn-Rg Reduces to Behavioural Relations on SOCNs
  
  
  We now note that the LTS (_)
  “mimicking” the r-game _
  associated with a socn-r-game 
   (recall (<ref>)) can be presented as
   _' for
  a SOCN ' (recall (<ref>))
   that is efficiently constructible from :
  
   
  There is a logspace algorithm that,
  given
  a socn-r-game ,
  constructs a SOCN ' such that
  the LTSs (_) and _' are
  isomorphic.
  
  
  We again use Figures <ref>
  and <ref> for illustration;
  now s_i are viewed as control states
  and the bracketed parts of edge-labels are counter-changes (in binary).
  
  Given a socn-r-game =(Q,Q_∃, δ, ), we
  first consider
  the r-game
  
      ^csg=(Q,Q_∃, , {})
  
  (“the control-state game of ”) arising from  by
  forgetting the counter-changes; hence qq̅ iff
  there is a rule qzq̅. In fact, we will assume that
  there is at most one rule  qzq̅ in δ (of )
  for any pair (q,q̅)∈ Q× Q; this can be achieved by
  harmless modifications.
  
  We construct the (finite) LTS (^csg)
  (“mimicking” ). Hence each q∈ Q has the copies q,q' in
  (^csg), and other states are added
  (as also depicted in Figure <ref> where s_i are
  now in the role of control states); there are also the
  respective labelled transitions in (^csg), with labels
  a_⟨ q,q̅⟩, a_c, a_win.
  
  It remains to add the counter changes (integer increments and
  decrements in binary), to create the required SOCN '.
  For q∈ Q_∃ this adding is simple, as
  depicted in Figure <ref>: if qzq̅ (in ),
  then we
  simply extend the label a_⟨ q,q̅⟩
  in (^csg)
  with z;
  for qa_⟨ q,q̅⟩q̅ and
  q'a_⟨ q,q̅⟩q̅' in (^csg)
  we get
   qa_⟨ q,q̅⟩,zq̅
   and  q'a_⟨ q,q̅⟩,zq̅' in '.
  
   For q∈ Q_∀ (where Q_∀=Q∖
   Q_∃) it is tempting to the same, i.e. to extend
  the label a_⟨ q,q̅⟩ with z when
  qzq̅, and extend a_c with 0.
   But this might allow cheating for Defender: she could thus
   mimic choosing a
   transition
   q(k)xq̅(k+x) even if k+x<0. This is avoided by the
   modification that is demonstrated in Figure <ref>
   (by x=x'+x”, etc.); put simply: Defender must immediately prove
   that the transition she is choosing to mimic is indeed performable.
   Formally, if   X={q̅| qq̅}≠∅
   (in (^csg)), then in '
   we put qa_c,0⟨ q,X ⟩ and
   ⟨ q,X ⟩a_⟨ q,q̅⟩,zq̅
   for each qzq̅ (in );
   for  each qzq̅ we also define z'=min{z,0},
    z”=max{z,0} and
   put q'a_c,z'⟨ q,q̅⟩,
   ⟨ q,q̅⟩a_⟨
   q,q̅⟩,z”q̅'.
   Then for any pair qz̅q̅,
   qz̅̅̅q̅̅̅
   where q̅≠q̅̅̅ we put
  ⟨ q,q̅⟩a_⟨
  q,q̅̅̅⟩,z̅̅̅-z̅'q̅̅̅.
  
  Finally, p_wina_winp_win in (^csg)
  is extended to p_wina_win,0p_win in '.
  
  
  We have thus finished the proof of Theorem <ref>.
  
  
  
  
  
  
  
  
  § STRUCTURE OF SIMULATION PREORDER
  ON ONE-COUNTER NETS
  
  
  In this section we give a new self-contained proof clarifying
  the structure of simulation preorder  on the LTS _
  associated with a given one-counter net ;
  this will also
  yield a polynomial-space algorithm  generating a description
  	of  on _ that can be used to decide if p(m) q(n).
  
  We first show
  a natural graphic presentation
  of the relation , and in Section <ref> we
  show
  its linear-belt form; the result
  is captured  by the belt theorem.
  The proof is inspired
  by <cit.> but is substantially
  different.
  A main new ingredient is the notion of so called down-black and up-white
  lines, and their limits in which we do not a priori exclude lines with
  irrational slopes; this allows us to avoid many technicalities used in
  previous proofs, while the presented “geometric” ideas should be
  straightforward, and transparent due to the respective figures.
  
  
  In Section <ref> we prove that
  the slopes and the widths of belts are presented/bounded by small
  integers.
  Though this quantitative belt theorem is in principle equivalent to the respective
  theorem proved in <cit.>, our proof is
  again conceptually different;
  using the novel notions, the quantitative characteristics
  are derived
  from the (qualitative) belt theorem easily.
  
  For completeness,
  in Section <ref> we briefly recall the idea
  from the previous papers that shows how the achieved structural
  results yield a polynomial-space algorithm generating a description
  of  for a given one-counter net.
  
  
  In the sequel we assume a fixed OCN =(Q,Act,δ) if not said otherwise.
  By
  , _≥ 0, _>0 we denote the sets of
  reals, of nonnegative reals, and of positive reals, respectively.
  We also use ∞ for an infinite amount (in particular for the
  slope of a vertical line); hence α<∞ for all
  	α∈. By ⟨γ,γ'⟩, where
  γ∈_≥ 0 and γ'∈_≥
  	0∪{∞},
  	we denote the set {α∈_≥ 0∪{∞}|γ≤α≤γ'}; in particular,
   ⟨ 0,∞⟩=_≥ 0∪{∞}.
  
  
  
  
    
  Monotonic black-white presentation of the simulation
  preorder <=
  For each pair  (p,q)∈ Q× Q
  we define the (black-white)
  colouring C_p,q
   of the integer points in the first quadrant of the plane
  ×; we put
   C_p,q: ×→black,white where
  
      C_p,q(m, n)    =
      		black    p(m)  q(n), 
      white    p(m)  q(n).
  
  We recall the definition of (s,s') in
  the paragraph “Stratified simulation, and ranks of pairs of states”
  in Section <ref>; this yields
  the definition of (p(m),q(n)) for our fixed  OCN
  =(Q,Act,δ). Hence
  for each (p,q)∈ Q× Q we have
  that each white point (m,n) in
  C_p,q has an associated finite rank, namely
  (p(m),q(n))∈.
  
  
  The next proposition captures the trivial fact
  that “black is upwards- and leftwards-closed” and
   “white is downwards- and rightwards-closed”
  (as is also depicted in Figure <ref> in Introduction, which also
  shows the “linear-belt form” of the colourings).
  
  
  
  
   If C_p,q(m,n) = black, then
  C_p,q(m',n') = black for all m' ≤ m
   and n'≥ n.
  Hence	if C_p,q(m,n) = white,
  then			   C_p,q(m',n') = white for all
  m'≥ m and  n' ≤ n.
  
  
  Since OCNs are monotonic in the sense that p(m)aq(n) implies
  p(m+i)aq(n+i) for all i∈, we will easily verify
  that the relation
  
      R={(p(m'),q(n'))|
      p(m) q(n)  for some  m≥ m'
       and  n≤ n' }
   is a simulation relation.
  	Since
  	⊆ R, we will thus get R=, and the proof
  	will be finished.
  To verify that R is indeed a simulation,
  we consider (p(m'),q(n'))∈ R and fix m≥ m' and n≤ n'
  so that p(m) q(n).
  If p(m')ap'(m'+i) (for i∈{-1,0,+1}), then p(m)ap'(m+i). Since
  	p(m) q(n), we have q(n)aq'(n+j) where
  j∈{-1,0,+1} and
  p'(m+i) q'(n+j). Hence  q(n')aq'(n'+j),
  and (p'(m'+i),q'(n'+j))∈ R.
  
  
  
  
  
  
   §.§ Belt theorem
  
  
  	Below we state the (qualitative) belt theorem, illustrated in
  	Figure <ref>,
  after
  introducing the needed notions.
  We can remark that the validity of the belt theorem can be easily intuitively
  anticipated (by a quick thought about the problem) but it has turned out
  surprisingly hard to be rigorously
  proven. (It can be also intuitively anticipated that the colouring
  inside the belt determined by the lines ℓ_L, ℓ_R in
  Figure <ref> is ultimately periodic, but this is
  only used in Section <ref>.)
  
  
  
  
  
  
  
  
    
  Lines, slopes, axes, points, points above or below lines,
  	points on
  	the left of or on the right of vertical lines. (See
  	Figure <ref>.)
  A vertical line ℓ (in the plane ×) is the set
  ℓ={(x,y)| y∈} for a fixed x∈; we put
  (ℓ)=∞. A non-vertical line ℓ is
  the set
  ℓ={(x,y)| y=γ· x + c} for some fixed
  γ∈ and c∈; here (ℓ)=γ.
  A line  is either
  a vertical line or a non-vertical line.
  By a γ-line, γ∈∪{∞}, we mean a
  	line whose slope is γ.
  	As expected, by the horizontal axis, h-axis,
  we mean the 0-line that goes through the origin (0,0);
  the vertical axis, v-axis, is the ∞-line that  goes through (0,0).
  
  By points we mean the pairs (m,n)∈× (hence only the
  integer points in the first quadrant of the plane
  ×), unless explicitly stated that we consider all
  integer points (elements of ×).
  Given a non-vertical line  ℓ={(x,y)| y=γ· x + c},
  a point (m,n) is above ℓ if n≥γ· m
  + c,
  and it is
   below ℓ if n≤γ· m + c.
  Given a vertical line  ℓ={(x,y)|
  y∈},
  	a point (m,n) is above ℓ, or also
  	on the left of ℓ, if m≤ x, and it is
   below ℓ, or also
  	on the right of ℓ, if m≥ x.
  	A point p is strictly above ℓ if
  	p is above ℓ but not on ℓ; similarly,
  	p is strictly below ℓ if
  	p is below ℓ but not on ℓ.
  
  
  
  
  
  
  
  	For each (p,q)∈ Q× Q, and its respective
  	colouring C=C_p,q, there are (a slope) γ∈⟨ 0,∞⟩
  	that is rational or ∞, and
  	two (parallel) γ-lines ℓ_L and ℓ_R
  	such that all points above ℓ_L are black in C and all
  	points below ℓ_R are white in C. (See
  	Figure <ref>.)
  
  
  We recall that we do not discuss how the mapping C_p,q
  looks inside the belt
  depicted in Figure <ref>;
  only in Section <ref> we refer to the
  fact that it is ultimately periodic there.
  
  
  Now we introduce further notions useful in the proof of the belt theorem.
  
  
    
  Down-black and up-white lines and slopes,
  down-limits alpha_C and up-limits beta_C.
  	A line ℓ, with (ℓ)∈⟨ 0,∞⟩, is down-black in a colouring
  	C=C_p,q if there are
  	infinitely many points below ℓ that are black in C.
  	A (nonnegative) slope γ∈⟨ 0,∞⟩ is
  down-black in C if there is a γ-line
  	ℓ that is down-black in C.
  
  By the down-limit of C we mean the value
  
  
  α_C=inf { γ|γ is down-black in C }
  
  
  (where inf∅ =∞).
  We say that α is a down-limit if
  	α=α_C for some C=C_p,q.  For a down-limit α, by
  	α-colourings we mean the colourings C
  	such that α_C=α.
  
  		A line ℓ is up-white in a colouring
  	C=C_p,q if there are
  	infinitely many points above ℓ that are white in C.
  	A (nonnegative) slope γ∈⟨ 0,∞⟩ is
  up-white in C if there is a γ-line
  	ℓ that is up-white in C.
  By the up-limit of C we mean the value
  
  
  β_C=sup { γ|γ is up-white in C }
  
  
  (where sup∅ =0).
  
  We highlight the following trivial fact.
  
  
    
    * If γ is down-black in C,
      then each γ'∈⟨γ,∞⟩ is down-black in
      C; moreover, if γ'>γ, then each γ'-line
      is down-black in C.
    
    * If γ is up-white in C,
      then each γ'∈⟨ 0,γ⟩ is up-white in
      C; moreover, if γ'<γ, then each γ'-line
      is up-white in C.
    
  
  
  We note that we cannot a priori exclude that some α_C is irrational
  and/or not down-black;
   similarly we cannot exclude
  that β_C differs from α_C, and that it is irrational
  and/or not up-white.
  But we immediately note a simple fact:
  
  	For each (p,q)∈ Q× Q,	β_C_p,q≥α_C_p,q.
  
  
  Let α_C>β_C for C=C_p,q, and let
  α_C>γ>β_C; hence
  γ is not down-black and not up-white.
  Thus for each γ-line ℓ we have that almost all points
  	(i.e., all but finitely many)
  below
   ℓ are white and
  almost
  all points above ℓ are black; by an obvious shift of
  	ℓ we deduce that γ is up-white and/or
  down-black after all, which is a contradiction.
  
  
  We now state a lemma that trivially entails
  Theorem <ref>: the slope γ claimed for C in
  Theorem <ref> is equal to α_C (which is claimed
  to be equal to β_C by the lemma).
  
  
  
    For each (p,q)∈ Q× Q and the respective
    colouring C=C_p,q the following conditions hold:
    
    
    * α_C is rational or
      ∞,
    
    * α_C=β_C, and
    
    * there are α_C-lines ℓ_L and ℓ_R such that
      all points above ℓ_L are black in C, and all
      points below ℓ_R are white in C.
    
  
  
  Before proving the lemma
  we introduce
  a main technical ingredient of the proof,
  namely Proposition <ref> and Corollary <ref>,
  preceded by
   the needed notions and by a simple, yet very useful, observation
   (Proposition <ref>).
  
   We can remark that these technical ingredients can hardly be
   “intuitively anticipated”; they have been “distilled” from the
   overall nontrivial proof, as useful technical claims.
   Some intuition about a possible proof
   strategy might be perhaps got by
   looking at the simulation games described in the papers <cit.>
  and <cit.>, but our proof is, in fact, not so
  tightly related to the simulation problem and could be given in a
  more general framework of specific tiling problems (as we also recall
  in Section <ref>).
  
  
  
  
  
  
    
  Vectors, their slopes and d-sizes. (See
  Figure <ref>.)
  We view a vector v as a pair ((v),(v)) where
  (v)∈× is the start-point of v and
  (v)∈× is the
  end-point of v. The slope of a vector v, (v), is defined when
  (v)≠(v), in which case it is the slope of the line going
  through both  (v) and (v).
  The d-size of v (“d” stands for direction) is the Euclidean distance of
  the points (v) and (v) with the positive sign (+) or the
  negative sign (-) : if (v)≠(v), then we consider
   the line ℓ that is
  perpendicular to v and goes through (v); if
  (ℓ)≠∞ and (v) is above ℓ, or
  (ℓ)=∞ and (v) is to the right of ℓ, then
  the d-size of v is positive, and otherwise  the d-size of v is
  negative.
  
  
  
    
  Black-white vectors.
  
  A vector v is black-white in a colouring C if (v)
  is black and (v) is white in C.
  
  
  
    
  Neighbour points and vectors.
  A point (m',n') is a neighbour of a point (m,n) if
  |m'-m|≤ 1 and |n'-n|≤ 1 (which includes the case m'=m,
  n'=n).
  A vector v' is a neighbour vector of a vector v
  if (v') is a neighbour
  of (v) and v,v' have the same slopes and
  sizes (hence v' is a “small shift” of v).
  
  
  
  The next proposition is the announced simple observation. It states that
  for any vector v where
  	(v) is not on the vertical axis,
  (v) is not on
  	the horizontal axis, and v is black-white in some
   C_p,q there is its neighbour vector v' that is
  black-white in some C_p',q' and the rank of the white
  end-point of v' in  C_p',q'
  is smaller than the rank of the white end-point of v
  in C_p,q.
  (Recall the vectors v_0,v_1 in Figure <ref>a in
  Introduction, and the discussion of ranks (p(m),q(n))
  between the definition of C_p,q(m,n) and
  Proposition <ref>.)
  
  
  Let
  	
  
  	C_p,q(m,n)=black,
  C_p,q(m',n')=white
  	
  
  		where m>0 and n'>0.
  Then there are p',q'∈ Q and i,j∈{-1,0,1} such that
  
  
  C_p',q'(m+i,n+j)=black,
  C_p',q'(m'+i,n'+j)=white,
  
  
  and   (p'(m'+i),q'(n'+j))<(p(m'),q(n')).
  
  
    Let the assumptions hold; we put (p(m'),q(n'))=r∈.
  We can thus fix a transition  p(m')ap'(m'+i)
  (related to a rule pa,ip')
  such that for each
   q(n')aq'(n'+j) we have
   (p'(m'+i),q'(n'+j))<r.
  Since m>0, we have p(m)ap'(m+i), and since
  p(m) q(n), there is a transition q(n)aq'(n+j) such
  that p'(m+i) q'(n+j); since n'>0, we also have
  q(n')aq'(n'+j).
  Hence C_p',q'(m+i,n+j)=black,
  and C_p',q'(m'+i,n'+j)=white, and
  	(p'(m'+i),q'(n'+j))<r.
  
  
  
  
  
  Now we aim to formulate a crucial ingredient of the proof of
  Lemma <ref>, namely Proposition <ref>
  and its corollary,
  for which we need further notions.
  
  
  
    
  Point-to-line distance, perpendicular lines l^bot_b.
  For an integer point p (in ×) and a line ℓ,
  by (p,ℓ) we mean the standard (Euclidean) distance
  of p to ℓ.
  Given
  a line ℓ where (ℓ)∈⟨ 0,∞⟩
  and a level
  (which might be also called a bottom-level)
  b∈_≥ 0,
  by ℓ^_b we denote
  the line that is perpendicular to ℓ, intersects the horizontal
  and/or vertical axis in the first quadrant, and
  	((0,0),ℓ^_b)=b. (Hence
  	(ℓ')^_b=ℓ^_b for any ℓ' that is
  	parallel with ℓ.
  See
  	Figure <ref>a.)
  
  
  
  
  
    
  Areas,
  	border and interior points of areas.
  By an area we mean just a set A⊆× of
  	points.
  	A point p∈ A is a border point of A if
  	it has a neighbour point outside A (hence in
  	(×)∖ A);
  	we put (A)={p|p is a border
  	point of A}.
  	Each point p∈ A∖(A)
  is an interior point of A.
  (E.g., (0,0) is an interior point of A={(0,0), (0,1), (1,0),
  (1,1)}.)
  
  
  
  
  
  
  
  
  
    
  Line-level-line areas
  Area((l,b),l') and
  Area(l,(b,l')). (See
  Figure <ref>b.)
  Given two lines ℓ,ℓ' where
  ∞≥(ℓ)≥(ℓ')≥ 0,
  and
  a bottom-level b∈_≥ 0,
  we define
  	((ℓ,b),ℓ')
  as the set of points (in ×)
  that are below ℓ, above ℓ', and also above
  	the line ℓ^_b; an exception is the case with
  	(ℓ)=0 (hence (ℓ')=0 as well)
  	where the points
  	in ((ℓ,b),ℓ') are to the right of
  	(the vertical line) ℓ^_b.
  
  
  By (ℓ,(b,ℓ')) we mean the set of points
  that are below ℓ, above ℓ', and also above
  the line (ℓ')^_b; again, an exception is the case
  with (ℓ')=0, where the points in (ℓ,(b,ℓ')) are to the right of
  (the vertical line) (ℓ')^_b.
  
  In fact, we will not encounter the “pathological” case
   where (ℓ)=(ℓ') and ℓ' is
  strictly above (to the left of) ℓ,
  in which case the sets ((ℓ,b),ℓ') and (ℓ,(b,ℓ')) are
  empty. In the special case where (ℓ)=∞ and
  (ℓ')=0, we only consider
  the sets ((ℓ,b),ℓ') where  (ℓ)^_b coincides with
   ℓ', and the sets (ℓ,(b,ℓ')) where  (ℓ')^_b coincides with
   ℓ.
  
  
  
  
    
  Special cases of line-level-line areas:
  Area((<-l)) and
  Area(l->).
  Given a line ℓ, with (ℓ)∈⟨ 0,∞⟩, we put
  	(ℓ)={ p∈×|p
  	is above ℓ }, and
  		(ℓ)={ p∈×|p
  	is below ℓ }.
  (Hence (ℓ)=((v-axis,0),ℓ)
  and (ℓ)=(ℓ,(0,h-axis)).)
  
  
  
    
  Border points of area((l,b),l') along l,
  along l', and along l^bot_b.
  (See the dotted boundaries in Figure <ref>b.)
  Given  a point p∈(((ℓ,b),ℓ')),
  we say that p
  lies along
  ℓ if p∈((ℓ)), hence if
  p has a neighbour point (integer point in the first quadrant)
  strictly above ℓ; p lies along
  ℓ' if p∈((ℓ')).
  If p∈(((ℓ,b),ℓ')) does not lie along
  ℓ nor along ℓ', then we say that p lies
  along ℓ^_b.
  
  
  
  
  
    
  D-sizes of vectors related to gamma € <0,infty>, gamma-d-size and
  co-gamma-d-size. (See Figure <ref>.)
  For
  γ∈⟨ 0,∞⟩,
  the γ-d-size of v and
  the co-γ-d-size of v are the following real numbers.
  If (v)=(v), then both γ-d-size and
  co-γ-d-size of v are 0.
  If (v)≠(v), then
  we consider the γ-line ℓ going through (v), and the
  line ℓ' that is perpendicular to ℓ and goes through
  (v).
  The γ-d-size of v is ((v),ℓ')
  (hence nonnegative)
  if (ℓ')≠∞ (hence γ=(ℓ)>0) and (v) is
  below ℓ', or if (ℓ')=∞ and (v) is
  to the left of ℓ'; the γ-d-size of v is
  -((v),ℓ') (hence nonpositive)
  otherwise.
  The co-γ-d-size of v
  is ((v),ℓ) (hence nonnegative)
  if (ℓ)≠∞ (hence 0≤γ=(ℓ)<∞)
  and
  (v) is above ℓ, or if
   (ℓ)=∞ and (v) is
  to the left of ℓ;
   the co-γ-d-size of v is
  -((v),ℓ) (hence nonpositive)
  otherwise.
  (If γ=(v), then the  γ-d-size of
  v coincides with
  the previously defined d-size of v.)
  
  
  
  
  
  
  
  
  	The following crucial technical proposition is illustrated in
  	Figure <ref>. It will be used several times
  	later to bound the up-limits under the described
  	circumstances.
  
  	 
  
  	We assume a nonempty set  of colourings (from the set
  	{C_p,q| p,q∈ Q}),
  	two lines ℓ,ℓ' and a level b∈_≥ 0
  		such that the following conditions are satisfied
  		(cf. Figure <ref>):
  	
  		
    * ∞≥(ℓ)≥(ℓ')≥
  			0,
  			and ((ℓ,b),ℓ') has no point on
  			the vertical axis;
  		
    * each colouring C∉ is
  			monochromatic (all-black or all-white) inside
  			((ℓ,b),ℓ');
  
    * for each  C∈:
  			
  				
    * the points in
  					(((ℓ,b),ℓ')) that
  					lie along ℓ' are white in C,
  				
    * we can fix a point P_C
  such that C(P_C)=black,
  					P_C is an interior point of ((ℓ,b),ℓ'),
  and (p_C,ℓ)≥bd_C where we put
  
      bd_C=sup { (p,ℓ)|p∈(((ℓ,b),ℓ')), C(p)=black}.
  
  					(Hence there is no point
  					in
  					(((ℓ,b),ℓ'))
  					that is black in C and has
  				a larger distance from ℓ
  					than P_C.)
  
  	
  	Then there is a line ℓ̅
  	with (ℓ̅)=(ℓ)
  	such that all points above
  	ℓ̅ are black in each C∈.
  
  Before proving the proposition, we
   note its trivial corollary:
  
  Under the conditions in Proposition <ref>,
   (ℓ)≥β_C for each C∈.
  
   To prove Proposition <ref>, we let
  its assumptions hold, and we put ρ=(ℓ).
  	If ρ=∞, then the claim is trivial: there are no
  	points above, i.e. left of, any vertical line ℓ̅
  	that does not intersect the first quadrant; such  ℓ̅
  	trivially satisfies the claim.
  Hence we further
  	assume
  	
      ∞>ρ=(ℓ)≥(ℓ')≥ 0.
  
  
  We also note that for almost all m∈ there is n such that
  	(m,n)∈((ℓ,b),ℓ'); this is obvious if
  	(ℓ)>(ℓ'), and in the case
  	ρ=(ℓ)=(ℓ') it is guaranteed by the
  	existence of interior
  	points of ((ℓ,b),ℓ') (they exist due to the
  	points P_C): if p=(m,n) is
  	interior in ((ℓ,b),ℓ'), then
  	we have (m,n+1)∈((ℓ,b),ℓ')
  and
  	for any m'≥ m
  	there is n' such that (m',n') lies below
   ℓ and above the
  	parallel ρ-line going through p.
  
  	We call a vector v
  	eligible if (v)∈((ℓ,b),ℓ'),
  v is black-white in some colouring,
  and both the ρ-d-size of v and
  the co-ρ-d-size of v are nonnegative.
  (We note that (v) can be outside
   ((ℓ,b),ℓ'), but then it necessarily lies
  	strictly
  	above ℓ.)
  E.g., v in Figure <ref>
  	is eligible.
  
  	To finish the proof, it suffices to show that the  co-ρ-d-sizes
  	of eligible vectors are bounded by some	B_0∈_≥
  	0; the claimed line ℓ̅ then surely exists
  	(as is illustrated in Figure <ref>):
  	we can take ℓ̅ above ℓ in the distance (to
  	ℓ) greater
  	than B_0 so that, moreover, ℓ̅ intersects
  	v-axis above the vertical coordinates of all P_C,
  	C∈.
  
  For the sake of contradiction, we assume  that the  co-ρ-d-sizes
  	of eligible vectors are not bounded; hence
  for every B∈_≥ 0
  	the set
  	
  
  	E_B={ v| v is
  	eligible and the co-ρ-d-size of v is greater than B }
  	
  
  is nonempty.
  	We first note that there is some B'∈_≥ 0 such that for each
  B≥ B' and each v∈ E_B we have that
  	v is not black-white in any C∉
  	(and thus must be black-white in some C∈).
  
  We verify this claim by considering a fixed colouring
  	C∉, which is
   monochromatic in ((ℓ,b),ℓ'), and by noting that for
  	each B∈_≥ 0 and each v∈ E_B we have:
  	
  		
    * If
  	C is all-white in ((ℓ,b),ℓ'), then
  			C((v))=white (and thus v is not
  			black-white in C).
  
    * If C is  all-black in
  			((ℓ,b),ℓ') (and thus
  			C((v))=black), and
  			C((v))=white,
  			then (v) is outside  ((ℓ,b),ℓ'),
  			hence strictly above ℓ; let us consider
  			this case, where
  			(v)=(m,n). Then
  			C(m,n')=white for all n'≤ n
  			 (by
  			Proposition <ref>). This
  			entails that for this m there is no n'
  			such that (m,n')∈((ℓ,b),ℓ').
  			As discussed above, this can be the case only
  			for finitely many m, which entails that
  			there are only finitely many eligible vectors
  			that are black-white in some C∉.
  			Hence the existence of B' is clear.
  	
  
  Now for each B≥ B' we fix a vector v_B∈ E_B
  	with the least possible rank of its white end;
  thus v_B is black-white in some C_p,q∈,
  	(v_B)=(m,n),
  	and
  (p(m),q(n)) is the least possible, when considering all v∈ E_B and all
  	C∈.
  	Since  (v_B) is in ((ℓ,b),ℓ'), it is
  	not on the vertical axis, and thus
  Proposition <ref> entails that
  	(v_B)∈(((ℓ,b),ℓ')) (otherwise v_B
  	has a neighbour
  	vector that is also in E_B and its white end has a lesser rank).
  
  
          
  
  For any fixed B≥ B', by 3(b) we thus have
  	((v_B),ℓ)≤(p_C,ℓ) for the
  	respective colouring C=C_p,q∈ (in which (v_B)
  	has the least possible rank);
  the vector (p_C,(v_B)), which is also black-white in
  	C, thus has the co-ρ-d-size also greater than B (since
  	it is not smaller than the co-ρ-d-size of v_B).
  If the vector (p_C,(v_B)) were eligible
  (as is depicted in Figure <ref>), thus
  belonging to E_B,
  	Proposition <ref> would yield a contradiction
  	(since p_C is an interior point of
  	((ℓ,b),ℓ'), the vector (p_C,(v_B))
   would have a neighbour vector
  	that is also in E_B
  	and its white end has a lesser rank).
  Hence the ρ-d-size of
  	(p_C,(v_B)) is negative
  	(as depicted in Figure <ref>); this entails that
  ρ=(ℓ)>0 (since in the case ρ=0 the fact
  C(p_C)=black would entail C((v_B))=black, by
  Proposition <ref>, which contradicts the
  assumption C((v_B))=white).
  
  The fact that ρ=(ℓ)>0 and the ρ-d-size of
  	(p_C,(v_B)) is negative entails that
  (v_B) is strictly below the line
  that is	perpendicular to
  	ℓ and goes through p_C; moreover,
  (v_B) is below the horizontal line going through p_C
  since C(p_C)=black and  C((v_B))=white
  (see Figure <ref>).
  There are thus only finitely many points that can be
  (v_B), independently of the chosen  B≥ B'.
  In other words, the set {(v_B)| B≥ B'} is
  finite, which also entails that the set
   {v_B| B≥ B'} is finite (recall that v_B is
   eligible, and thus the
   ρ-d-size of v_B is nonnegative).
   This contradicts our choice of v_B that entails
   that the co-ρ-d-size of v_B is greater than B, for each
   B∈_≥ 0.
  
   The  co-ρ-d-sizes
  	of eligible vectors are thus indeed bounded by some
  	B_0∈_≥ 0.
  
  
  Besides Corollary <ref>, which is trivial,
  we also derive the next corollary, showing that if the assumptions of 	Proposition <ref> are slightly
  strengthened, then we get a strict upper bound on the up-limits
  β_C.
  
  
  
  	If ,ℓ,ℓ',b satisfy the conditions of
  	Proposition <ref>
  	and, moreover, (ℓ)>(ℓ') and
  	for each C∈ we can choose
  	p_C (which is an interior point of
  	((ℓ,b),ℓ')) so that it has no neighbour point on ℓ and
  	the inequality  in 3(b) is strict
  	((p_C,ℓ)>bd_C),
  	then (ℓ)>β_C for each C∈.
  
  
  	Let the described conditions be satisfied (in fact, such a
  	situation is
  	depicted already in Figure <ref>;
  	Figure <ref> makes clear that all neighbour points
  	of p_C are strictly below ℓ).
  
  	Since ρ=(ℓ)>(ℓ')≥ 0,
  	we can very slightly rotate ℓ to the
  	right around the intersection-point of ℓ and
  	ℓ^_b (see Figure <ref>), by which we get
  	ℓ” with a slope ρ”,
  	ρ>ρ”≥(ℓ'),
  	so that the resulting ((ℓ”,b”),ℓ')
  	(ℓ^_b has rotated to (ℓ”)^_b”)
  	is a subset of ((ℓ,b),ℓ')
  	(in other words, the rotation of ℓ^_b to (ℓ”)^_b”
  	is so small that there is no [integer] point in
  	((ℓ”,b”),ℓ')∖((ℓ,b),ℓ'), i.e. in the grey triangle in Figure <ref>)
  	 and so that the original points p_C
  	are interior points also in ((ℓ”,b”),ℓ')
  while the
  	conditions of Proposition <ref>
  	(in particular (p_C,ℓ)≥bd_C)
  	are kept. (To be very precise, in the case where
  	(ℓ)=∞ and (ℓ')=0 we recall our
  	stipulation that
  	ℓ^_b coincides with ℓ'; the discussed
  	slight rotation then trivially has the property
  that there is no point in ((ℓ”,b”),ℓ')∖((ℓ,b),ℓ').)
  	Hence
   Proposition <ref> entails that
  	ρ”≥β_C, and thus
  	ρ>β_C (since ρ>ρ”).
  
  
  
  
  
  
  
    
  Proof of Lemma <ref>.
  
  We denote the down-limits, i.e. the elements of the set
  {α_C| C=C_p,q, (p,q)∈ Q× Q})
  by α_1,α_2,⋯,α_k  (k≤ |Q|^2)
  so that
  
      0≤α_1<α_2⋯ <α_k≤∞.
  
  We now assume that the statement of Lemma <ref>
  holds for the
  colourings related to α_1,α_2,…,α_i-1
  (i∈{1,2,…,k}), and
  prove the statement for
  the α_i-colourings.
  The proof is given by Claims <ref> – <ref>.
  
  
  
  	For each α_i-colouring C we have β_C=α_i
  	(hence the down-limit α_C=α_i and the up-limit β_C
  	coincide).
  
  
  If α_i=∞, then the claim is trivial
  	(since ∞≥β_C≥α_C, by
  	Proposition <ref>);
  	hence we assume
  	∞>α_i.
  	We fix some slope ρ where ∞>ρ>α_i and
  	α_i+1>ρ if i<k.
  	If α_i=0, then we put ρ'=0,
  	and if α_i>0, then we fix ρ' so that α_i>ρ'>0 and
   ρ'>α_i-1 if i>1.
  We fix
  a ρ-line ℓ and a ρ'-line ℓ',
  	both going through the origin (0,0). (We can recall ℓ
  	and ℓ' from
  	Figure <ref>, and imagine that they go through
  	(0,0).)
  	By  we denote the set of all α_i-colourings, and
  	note:
  	
  		
    * for each C∈ (where α_C=α_i), there are
  	infinitely many black points
  			in ((ℓ,0),ℓ'), since
  the ρ-line ℓ must be down-black in C due to the fact
  			ρ>α_i=α_C (recall
  			Proposition <ref>),
  			but almost all
  			border points of ((ℓ,0),ℓ') along
  			ℓ' (i.e. those having neighbours strictly
  			below ℓ')
  			are white:
  if α_i=α_C>ρ',
  			then no ρ'-line can be down-black (in
  			particular, no shift of ℓ' to the left can
  			be down-black), and if
  			α_i=ρ'=0, then
  ℓ' is the horizontal axis
  and almost all points on ℓ' are
  			interior, having no neighbours (i.e.
  			neighbour integer points in the first quadrant)
  			outside ((ℓ,0),ℓ'), since
  			ρ=(ℓ)>0;
  
    * for each C∉ (where α_C≠α_i)
  			 we have:
  			
  				
    * if α_C>α_i, hence α_C=α_j for some
  					j>i,
  					then only finitely many points of
  					((ℓ,0),ℓ') are
  					black in C
   (since	α_C>ρ=(ℓ), and thus ℓ cannot be
  					down-black in C);
  				
    * if α_C<α_i,
  hence  α_C=α_j for some
  					j<i,
  					then only finitely many points of
  					((ℓ,0),ℓ') are
  					white in C
  					(here
  					α_i>ρ'=(ℓ')>α_C=α_j,
  					and we use that
  					β_C=α_C=α_j by
  					the induction hypothesis of
  	our proof of Lemma <ref>,
  					which entails that ℓ' is
  					not up-white in C).
  			
  	
  Hence we can choose a sufficiently large level b∈_≥ 0 so that the set
   (of α_i-colourings) and ℓ,ℓ',b
  satisfy the conditions 1, 2, and 3(a) of
  Proposition <ref>;
  in particular, the value
  
      bd_C=sup { (p,ℓ)|p∈(((ℓ,b),ℓ')), C(p)=black}
  
  is
  finite for each C∈.
  
  Since (ℓ)=ρ>α_i,
  we can fix some
  ρ” satisfying
  ρ>ρ”>α_i and also
  fix the ρ”-line ℓ” going through (0,0).
  The line ℓ” is down-black
  	in all C∈ (by Proposition <ref>)
  	and the fact
  	(ℓ)>(ℓ”)>(ℓ') entails
  that for each C∈
  there are infinitely many points in ((ℓ,b),ℓ')
  that are below ℓ” and black
  	in C.
  Hence for
  each C∈
  	the value sup { (p,ℓ)|p∈((ℓ,b),ℓ'), C(p)=black} is
  	infinite
  (in each C∈, the distance of
  	the black points in ((ℓ,b),ℓ')
  	to ℓ increases above any bound when the level
  	increases).
  
  
  Thus the condition 3(b) of
  Proposition <ref> is also satisfied
  (for each C∈, the point p_C can be chosen in a bigger distance from ℓ than
  the finite value bd_C,
  as is also depicted in Figure <ref>,
  so even the assumptions of Corollary <ref> are satisfied);
  Proposition <ref> thus
  entails that
  	ρ≥β_C for each C∈.
  In fact,  ρ>α_i could be chosen arbitrarily close to
  α_i;
  we have thus shown  ρ≥β_C for each ρ>α_i.
  By recalling that β_C≥α_C
  (Proposition <ref>), we derive that
  β_C=α_C=α_i for each α_i-colouring C.
  
  
  
  There is an α_i-line ℓ_R such that all points below ℓ_R
  are white
  	in all α_i-colourings.
  
  
  	If α_i=0 (which can happen for i=1), then the claim
  	is trivial (we can consider a horizontal line ℓ_R strictly
  	below h-axis, below which there are no points
  	[i.e. integer points in the first quadrant]).
  
  	So we assume α_i>0 and
  we fix an α_i-line ℓ such that all points below ℓ
  	are white in the maximum number  of α_i-colourings.
  Let  be the set of remaining α_i-colourings; hence
  	each α_i-line is down-black in each
  	C∈ (which has not been so far excluded though
  	α_C=α_i is the down-limit of C).
  	We assume
  	≠∅ (otherwise we are done by putting
  	ℓ_R=ℓ), and show a
  	contradiction.
  
  Each C∈ has black points below ℓ in unbounded
  	distances from ℓ (since each α_i-line is down-black in each
  	C∈).
  	We fix some ℓ' such that
  	α_i=(ℓ)>(ℓ')≥ 0, and
  	(ℓ')>α_i-1 if i>1. (We can again look at
  	Figure <ref>.)
  It is now a routine to verify that
  there is
  	some b∈_≥ 0 such that  and ℓ,ℓ',b
  	satisfy the assumptions of Proposition <ref>,
  	and even the assumptions of Corollary <ref>.
  	This entails that
  	(ℓ)=α_i>β_C, for each C∈.
  But since  is a set of α_i-colourings (hence
  	α_C=α_i for each C∈), we must have
  	 β_C≥α_i, for each C∈ (by
  	 Proposition <ref>).
  	 Hence =∅ after all.
  
  
  We note that ℓ_R from Claim <ref> can be
  shifted to the right, which entails a useful corollary
  (for which we recall that
  (ℓ)=((v-axis,0),ℓ) and that
  all border points of (ℓ) lie along ℓ):
  
  
  
  There is an α_i-line ℓ_R such that all border points of
  	(ℓ_R) are white
  	in all α_i-colourings.
  
  We note that the claim also comprises the case α_i=0 with ℓ_R being below
  h-axis, in which case (ℓ_R)
  has no border points at all.
  
  
  Now we aim to show that there is an α_i-line ℓ_L
  such that all points above ℓ_L
  are black
  	in all α_i-colourings, and that α_i is rational or
  	∞. (By this the proof of Lemma <ref> will be
  	finished.)
  Since the case α_i=∞ is trivial, we further assume that
  ∞>α_i.
  
  We will use the notion of the
  rightmost down-black
  α_i-lines ℓ_C for α_i-colourings C, after which we
  again apply Proposition <ref>.
  But, in fact, we can not a priori assume that the rightmost down-black
  α_i-lines exist and that α_i is rational,
  so we partition and analyse the class  of
  α_i-colourings without any such assumptions. We define the line ℓ_C
  as the “right-hand limit” for the respective down-black lines, if some
  α_i-lines that are down-black in C exist, which does not
  exclude
  the case that ℓ_C itself is not down-black.
  
  
  
  
    
  Partition of alpha_i-colourings by rightmost down-black
  lines l_C.
  Let  be the set of all α_i-colourings.
  For technical convenience we use a fixed α_i-line ℓ_R
  guaranteed by
  Claim <ref> (or Corollary <ref>), to define the partition of  into the
  following classes:
  	
  		
    * _1
  	contains each C∈ for which there is an
  	α_i-line that is down-black in C;
  
  
  			for each C∈_1 we define the rightmost
  			down-black line ℓ_C as the α_i-line
  	whose distance from ℓ_R is the infimum of distances of
  	the α_i-lines that are down-black in C.
  We further partition _1 as follows:
  			
  				
    * _11 contains all
  					C∈_1 for
  	which ℓ_C is down-black;
  
    * _12
  contains all C∈_1 for which ℓ_C is not down-black.
  			
  
    * _2=∖_1; hence for each
  	C∈_2 and each 	α_i-line ℓ
  	only finitely many points below ℓ are black in C.
  
  
  We now show that there is a desired “left-bound-line” for all C∈_1, by
  Claim <ref> that is preceded by a simple auxiliary fact in
  Claim <ref>; it turns out that _12 is empty, while
  we still do not exclude that  _11 is empty as well.
  Then we show that _2 is empty (by
  Claim <ref>); hence the (nonempty) set  of α_i-colourings
  is equal to _11, and Claim <ref> thus  finishes
  the proof of Lemma <ref> (including the fact that
  α_i is rational or ∞).
  
  
  [auxiliary]
  		
    * If γ∈_≥ 0 is rational,
  			then for any γ-line ℓ we have:
  
  				
    * ℓ either contains infinitely many
  		integer points (in ×), or no
  		integer point;
  	
    * there exists the least value μ∈_>0 such that
  		μ=(p,ℓ) for some integer point
  		p that is not on ℓ.
  			
  		
    * If γ∈_> 0 is irrational, then for each
  	B∈_> 0 there
  	is a (tiny) real number μ>0 such that for any two γ-lines
          ℓ,ℓ' whose (Euclidean) distance is μ we have that
  	the distance of any two different integer points lying
  	between the lines ℓ and ℓ' is larger than B.
  	
  
  1.
  	For γ=0 both parts of the claim are obvious; so we assume
  that γ=Δ_y/Δ_x for Δ_x,
  	Δ_y∈_>0, and consider a γ-line ℓ.
  We note that
  	if an integer point (z_1,z_2)∈× is
  	on ℓ, then the integer points
  	(z_1+i·Δ_x,z_2+i·Δ_y),  for all
  	i∈, are on ℓ as well.
  	Hence 1(a) is clear.
  	Now we note that for any integer point  p=(z_1,z_2)∈×
  outside ℓ we have that
  	(p,ℓ)=(p',ℓ) for all
  	(integer) points
  	p'=(z_1+i·Δ_x,z_2+i·Δ_y) where
  	i∈. Hence μ claimed in 1(b) is the least value in
  	the set
  
      { (p,ℓ)|p=(z_1,z_2)∈×,
      	p∉ℓ, 0≤ z_2≤Δ_y },
  
  which
  	obviously exists (since it exists for each fixed
  	z_2∈{0,1,…,Δ_y}).
  
  	2.
  We fix an irrational γ∈_> 0
  and some B∈_>0.
  	We note that for each vector v=(p,p')
  where p,p' are two different integer points and
  	(p,p')≤ B
  	(by (p,p') we refer to the Euclidean
  	distance of points)
  we have that the absolute value of the co-γ-d-size of v is
  	greater than zero (since (v) is rational and thus differs from
  	γ). Moreover, the set
  	
      M_γ,B = {μ' | [ μ'  is the absolute value of the co-γ-d-size of some (p,p');   where p,p' are two different integer points and (p,p')≤ B ]}
  
  is obviously finite. We can thus choose μ satisfying 0<μ<min
  	M_γ,B; such μ satisfies the claim.
  	Indeed:
  if there were two γ-lines
  ℓ,ℓ'
  			whose (Euclidean) distance
  is μ and two different integer points p,p'
  lying 	between ℓ and ℓ' and satisfying
  (p,p')≤ B, then the absolute value of the
  	co-γ-d-size of the vector (p,p')
  	would belong to  M_γ,B and would be not bigger than
  	μ — a contradiction.
  
  
  
  
  If _1≠∅, then there is an α_i-line ℓ'_L such
  	that all points above ℓ'_L
  are black
  	in all colourings from _1; moreover,
  	α_i is rational and _12 is empty. (We recall that
  	∞>α_i, as stipulated after
  	Corollary <ref>.)
  
  
  
  
  We fix an α_i-line ℓ_R so that
  all points in
  	( (ℓ_R) ) are white in each
  	C∈=_1∪_2
  	(such ℓ_R exists by Corollary <ref>).
  We assume that
  	_1≠∅, and we fix an α_i-line
  	ℓ sufficiently above all rightmost down-black lines
  	ℓ_C, C∈_1 (defined after Corollary <ref>),
  	so that ((ℓ,0),ℓ_C) has infinitely many interior
  	points for each C∈_1.	(See
  	Figure <ref>.)
  	Finally we choose (a sufficiently large) b∈_≥ 0 so
  	that ((ℓ,b),ℓ_R) does not intersect with the
  	vertical axis and is monochromatic in each
  	colouring
  	C∉_1; we can easily verify that such b exists
  	since we have:
  	
  		
    * for each (α_i-colouring) C∈_2
  and for each colouring C for which
   α_C>α_i
  			there are 	only finitely many points
  			below the α_i-line ℓ that are black in C (and we
  			choose b
  			so that these colourings are all-white in
  			((ℓ,b),ℓ_R));
  		
    * for each colouring C for which
  			α_C<α_i,
  			hence α_C=α_j
  			for some j∈{0,1,…,i-1},
  			we have α_C=β_C  by the
  	induction hypothesis of our proof of
  			Lemma <ref>, and there are
  			thus only finitely many points above the
  			α_i-line ℓ_R that are white in C (and we
  			choose b
  			so that these colourings are all-black in
  			((ℓ,b),ℓ_R)).
  	
  	Figure <ref> depicts ((ℓ,b),ℓ_R),
  and ℓ_C just for one C∈_1; let us ignore the additional dark-grey
  	belt and the line ℓ_C,μ for this moment.
  
  	Let us now assume that α_i (the slope of ℓ, ℓ_C,
  	ℓ_R) is rational. By using Claim <ref>(1)
  we easily deduce that for each C∈_1 the rightmost down-black line
  ℓ_C must be down-black; moreover, it contains
  infinitely many  points that are
  	black in C, while only finitely many points strictly below
  	ℓ_C can be black in C.
  	(If ℓ_C was not down-black then also a line arising by
  a tiny shift of ℓ_C to the left, by less
  	than μ in Claim <ref>(1b), would be not
  	down-black; this would contradict the definition of
  	ℓ_C. On the other hand, if there were infinitely many points strictly below
  	ℓ_C that are black in C, then a tiny shift of ℓ_C
  	to the right would give us a down-black line, which also
  	contradicts the definition of ℓ_C.)
  
  Hence if α_i is rational, then _12 is empty, and thus
  _1=_11. Moreover,
  we can simply increase
  b so that for each C∈_1 all the infinitely many points
  in ((ℓ_C,b),ℓ_R) that are black in C are on
  the line ℓ_C.
  We can thus apply
  Proposition <ref> (depicted in
  Figure <ref>) to
  	 _1,ℓ,ℓ_R,b; for each C∈_1, the point
  	 p_C can be chosen as one of the infinitely many points
  	 on ℓ_C that are black in
  	 C and interior in ((ℓ,b),ℓ_R) (hence not
  	 close to ℓ^_b). Proposition <ref>
  	 gives us
   the claimed ℓ'_L.
  
  To finish the proof, we now assume that
  	α_i is irrational (which entails that any α_i-line
  	contains at most one integer
  	point), and we will lead this assumption to a contradiction
  	with the assumption _1≠∅.
  Recalling Figure <ref>, we aim to increase b so that
  not only Proposition <ref>, but even
  Corollary <ref>, could be applied; this will entail that
  α_C>β_C for some C∈_1, which is the desired
  contradiction.
  
  Now we cannot assume that  _12=∅, but
  the colourings C∈_12 (where ℓ_C are not down-black)
  create no problem for our aim:
  We can increase b so that for each  C∈_12
  there are no
  points in ((ℓ_C,b),ℓ_R) that are black in C.
  By definition of ℓ_C, now
  for each point p in  ((ℓ,b),ℓ_R) that is black in some
  C∈_12 (hence p is strictly above ℓ_C) there
  are infinitely many interior points p' in ((ℓ,b),ℓ_R) that
  are black in C and for which
  (p',ℓ_C)<(p,ℓ_C), hence
  (p,ℓ)<(p',ℓ).
  (Figure <ref> aims to illustrate this, by depicting black points
  strictly above ℓ_C
  that
  “converge” to ℓ_C.) Hence for each C∈_12 and each
  sufficiently large b there surely is some p_C,
  C(p_C)=black, such that
  (p,ℓ)<(p_C,ℓ) for all points
  p∈(((ℓ,b),ℓ_R)) that are black in C.
  
  
  Now we look at the set _11, considering a fixed colouring C∈_11.
  By definition, the line ℓ_C (with the irrational slope
  α_i) is down-black in C; hence infinitely many points in
  ((ℓ_C,b),ℓ_R)
  (recall Figure <ref>) are black in C, while there is at
  most one (integer) point on ℓ_C.
  By definition of ℓ_C, for any (however tiny) μ∈_>0 there are
  only finitely many points in ((ℓ_C,μ,b),ℓ_R)
  that are black in C,
  where
  ℓ_C,μ arises by shifting ℓ_C by μ to the right
  (see Figure <ref>); Figure <ref>
   aims to illustrate this “converging” of black points to ℓ_C from below.
  Hence for any chosen μ∈_>0 we can surely increase b so
  that all the infinitely many points in  ((ℓ_C,b),ℓ_R)
  that are black in C are in  ((ℓ_C,b),ℓ_C,μ)
  (i.e., in the grey belt between ℓ_C and ℓ_C,μ
  in Figure <ref>).
  
  If we manage to choose the above discussed μ and b so that
  for each C∈_11 there is no border point of
  ((ℓ,b),ℓ_R) that is below ℓ_C and black in C
  (such a point could only be in the grey belt, i.e. in
  ((ℓ_C,b),ℓ_C,μ), close to ℓ^_b), then
  we can
  surely choose the points
  p_C, required by Corollary <ref>
  for _1,ℓ,ℓ_R,b, not only for all C∈_12 but
  also for all
  C∈_11 (for each C∈_11 we let p_C be
  one of the infinitely points in the grey belt that are black in C).
  But this yields a contradiction
   since
  Corollary <ref> in this case
  entails that (ℓ)=α_i=α_C>β_C for all C∈_1
  (which contradicts β_C≥α_C established by
  Proposition <ref>).
  
  Now we show that we can indeed choose μ and b that yield
  the described contradiction. We can choose
   μ∈_>0 sufficiently small
  so that any two different integer points in
  ((ℓ_C,b),ℓ_C,μ) (i.e. in the grey belt)
  have very large distances, for any C∈_11.
  (This follows from Claim <ref>(2).)
  We can thus surely choose b so that there is no (integer) point
  that is a border point of ((ℓ,b),ℓ_R) and lies in a grey
  belt (i.e. in ((ℓ_C,b),ℓ_C,μ) for some
  C∈_11).
  
  The assumptions that α_i is irrational and _1≠∅
  have thus yielded a contradiction.
  Hence the assumption _1≠∅ entails
  that α_i is rational, _12=∅ (hence
  _1=_11),
  and there is the claimed line
  ℓ'_L.
  
  
  
  
  _2=∅, and thus Claim <ref> finishes the proof
  	of Lemma <ref>.
  
  
  
  
  
  
  
  For the sake of contradiction, we assume
  	_2≠∅, and recall that
  for each C∈_2 there is no α_i-line that is down-black
  	in C (hence there are only finitely many points below any given
  	α_i-line that are black in C).
  We also recall our assumption ∞>α_i (stipulated  after
  	Corollary <ref>).
  
  	Now we fix an α_i-line ℓ so that all points above
  	ℓ are black in all C∈_1; the existence of such
  	ℓ is trivial if _1=∅, and otherwise it is
  	guaranteed by
  	Claim <ref>.
  We also fix a line ℓ' where ∞>
  (ℓ')>(ℓ)=α_i, and
  α_i+1>(ℓ') if i<k (where k is the number of
  	all down-limits, recall (<ref>));
  finally we fix some
  	b∈_≥ 0 so that the following conditions
  are satisfied (see
  	Figure <ref>):
  	
  		
    * (ℓ',(b,ℓ)) is monochromatic for all
  C∉_2;
  
    * all border points of (ℓ',(b,ℓ))
  	along ℓ' (having neighbours strictly above ℓ')
  	are black in all C∈_2;
  
    * all border points of (ℓ',(b,ℓ))
  	along ℓ (having neighbours strictly below ℓ)
  	are white in all C∈_2.
  	
  Any sufficiently large b will satisfy these conditions since we have:
  	
  		
    * for each colouring C for which
  			α_C>α_i, in which case
  			α_C>(ℓ'),
  			there are 	only finitely many points
  			below ℓ' that are black in C
  			(and we
  			choose b
  			so that these colourings are all-white in
  			(ℓ',(b,ℓ)));
  		
    * for each (α_i-colouring) C∈_1
  all points in  (ℓ',(b,ℓ)) are black in C by our
  			choice of ℓ;
  		
    * for each colouring C for which
  			α_C<α_i,
   in which case
  			(ℓ)>α_C and α_C=β_C  by the
  	induction hypothesis of our proof of
  			Lemma <ref>,
  			there are only finitely many points above
  			 ℓ that are white in C
  			 (and we
  			choose b
  			so that these colourings are all-black in
  			(ℓ',(b,ℓ)));
  		
    * for each (α_i-colouring) C∈_2 we have
  			α_i=α_C=β_C (by
  			Claim <ref>); hence above any
  			line that is parallel with ℓ' (and whose
  			slope is thus greater than β_C) there
  			are only finitely many points that are white
  			in C (and we can thus
  			choose b
  			so that the border points of (ℓ',(b,ℓ))
  			along ℓ' are all black in all
  			C∈_2);
  		
    * by definition of _2, for any C∈_2 and any α_i-line
  			ℓ̅ (which is thus parallel with
  			ℓ)
  			there are only finitely many points below
  	ℓ̅ that are black in C (and we can thus
  			choose b
  			so that the border points of (ℓ',(b,ℓ))
  			along ℓ are all white in all
  			C∈_2).
  	
  Let us now call a vector v to be
  a (B,μ)-vector,
  for B∈_≥ 0 and μ∈_>0, if B is the
  α_i-d-size of v
  and μ is the co-α_i-d-size of v.
  We can see (looking at Figure <ref> and recalling
  that each α_i-line is not down-black in any C∈_2)
  that we can fix some μ_0>0 such that for any B∈_>0
  there is B_0≥ B and
  a  (B_0,μ_0)-vector v
  where (v)∈((ℓ',(b,ℓ)))
  and C((v))=C((v))=white for some C∈_2
  (which entails that (v) is in (ℓ',(b,ℓ))).
  Moreover, we can even choose a  sufficiently large B_0
  so that
  
  	
    * there is
  a  (B_0,μ_0)-vector v
  where (v)∈((ℓ',(b,ℓ)))
  and C((v))=C((v))=white for some C∈_2;
  
    * the slope of 	 (B_0,μ_0)-vectors is strictly between
  		(ℓ') and (ℓ);
  	
    * for each (B_0,μ_0)-vector v
  where (v)∈((ℓ',(b,ℓ))), and for each colouring
  C we have
  	
      if C((v))=white,
      		then 	C((v))=white.
  
  
  	But then each (B_0,μ_0)-vector v with (v)∈(ℓ',(b,ℓ))
  	(not only with (v)∈((ℓ',(b,ℓ))))
  	satisfies (<ref>).
  	Indeed, a violating (B_0,μ_0)-vector v with the least
  	rank of its white start-point (v), where (v) is necessarily an interior
  	point of (ℓ',(b,ℓ)), leads to a
  	contradiction by Proposition <ref> applied to
  	the opposite black-white vector (which would yield a
  violating (B_0,μ_0)-vector with a smaller rank of its start-point).
  
  	This entails that the slope of (B_0,μ_0)-vectors, which is larger
  than α_i, is up-white in each C∈_2 (consider the line
  containing white-white vectors v_1,v_2,v_3,…
  in	Figure <ref>); this is a contradiction
  since β_C=α_i for all C∈_2 (by Claim <ref>).
  Hence _2=∅ after all.
  
  
  
  
  
  
  
  
   §.§ Quantitative belt theorem
  
  
  
  We have proven the belt theorem (Theorem <ref>),
  but we have not derived anything specific about the slopes, widths,
  and positions of the belts (one of which is depicted in
  Figure <ref>).
  Now we show that these parameters can be presented by
  polynomially bounded integers (in the size of the underlying
  one-counter net =(Q,Act,δ) that we have fixed).
  
  We start with the belt-slopes, which is another
  name for the down-limits α_C (that coincide with the up-limits
  β_C by Lemma <ref>);
  we recall that we have ordered the set {α_C| C=C_p,q,
  (p,q)∈ Q× Q}, denoting its elements
  (in (<ref>)) as
  
      0≤α_1<α_2⋯ <α_k≤∞.
  
  Hence when we refer to a belt-slope α, we understand that
  α=α_i for some i∈[1,k].
  We can also recall that by an α-colouring we mean a colouring
  C (C=C_p,q for some (p,q)∈ Q× Q) for which
  α_C=α.
  Before clarifying that the belt-slopes are fractions of small integers
  (or ∞), which is shown by
  Proposition <ref>,  we formulate a useful
  corollary of Proposition <ref>, which captures
  the black-white vector travel discussed around Figure <ref> in
  Introduction. (The black-white vectors in
  Figure <ref> are directed upwards but the
  corollary also handles the vectors directed downwards, like v_i_1
  in Figure <ref>.)
  
  
  
  Any
  	vector v_0 that is black-white in some C_0 gives rise to a sequence
  	v_0,v_1,…,v_n where (v_n)∈v-axis or
  	(v_n)∈h-axis, and
   for i=0,1,2,…,n-1 we have that v_i+1 is a neighbour vector of
  	v_i that is black-white in some C_i+1 and the rank of
  	the white end of  v_i+1
  	in C_i+1 is smaller than the rank
  	of the white end of v_i in
  	C_i.
  
  
  
  
  
  
  	If α, ∞>α>0, is a belt-slope, then
  α=Δ_y/Δ_x
  for some integers Δ_x, Δ_y from {1,2,⋯,||}
  	where  is the set of
  	α-colourings.
  
  
  Let  be the set of α-colourings, for some fixed
  	belt-slope α where
  ∞>α>0, and
  let ℓ_L,ℓ_R be some α-lines such that
  all points above ℓ_L are black in all C∈ and
  all points below ℓ_R are white in all C∈;
  the belt theorem (Theorem <ref>) guarantees that
  	such lines exist, and that α is rational.
  
  	By reasoning as in the proof of Claim <ref> (when assuming that
  	α_i is rational) we derive that
  for each C∈ there is the rightmost α-line ℓ_C
  	that is down-black in C; we also recall that there are infinitely
  	many points on ℓ_C that are black in C (but only
  	finitely many points strictly below ℓ_C are black in C).
  Analogously we derive that there is the leftmost α-line ℓ'_C
  	that is up-white in C;  there are infinitely
  	many points on ℓ'_C that are white in C.
  	(The colourings depicted in Figure <ref>, related
  	to the simple net
  in Figure <ref>, might suggest that
  ℓ'_C is below ℓ_C, but
  Figure <ref> depicts a more typical situation.)
  By _C we denote the distance of ℓ_C and
  	ℓ'_C, with the negative sign if ℓ'_C is below
   ℓ_C.
  	We put
  	
  
  	s=max { _C| C∈ }, and
  	_ms={ C∈|_C=s}
  	
  
  	(where ms refers to “Maximal Span”).
  
  Now we choose v_0 so that v_0 is black-white in some
  	C_0∈_ms, (v_0)∈ℓ_C_0, and
  	(v_0)∈ℓ'_C_0; moreover, we choose v_0 sufficiently
  	high in the respective α-belt so that each v_i in the prefix
  	v_0,v_1,v_2,…,v_|_ms| of the sequence
  	guaranteed by Corollary <ref> must necessarily
  	satisfy that (v_i)∈ℓ_C_i and
  	(v_i)∈ℓ'_C_i for some C_i∈_ms.
  Figure <ref> depicts this “sufficiently high”, where
  b is chosen so that
  	
  		
    * for each  C∈
  	the points strictly above ℓ'_C in
  	(v-axis,(b,ℓ'_C))
  	are black in C
  and the points strictly below ℓ_C
  in ((ℓ_C,b),h-axis)
  	are white in C,
  
    * and each colouring C∉ (for which
  α_C≠α) is
  	monochromatic in
  ((ℓ_L,b),ℓ_R).
  	
  
  
  By the pigeonhole principle,
  in the above discussed sequence v_0,v_1,v_2,…,v_|_ms|
  	we have some i_1,i_2 such that 0≤ i_1<i_2≤
  	|_ms| and both (v_i_1) and
  	(v_i_2) are on ℓ_C for the same
  	C∈_ms
  	(and (v_i_1) and
  	(v_i_2) are on ℓ'_C).
  Since (ℓ_C)=α, and (v_i_1),
  	(v_i_2) are two different points on ℓ_C,
  we deduce that α is the slope of the vector
  	((v_i_1),(v_i_2)).
          This entails
  	that  α=Δ_y/Δ_x
  	where Δ_x, Δ_y∈{1,2,⋯,i_2-i_1};
  Δ_x is the absolute value of the 0-d-size [horizontal
  	d-size] of the vector ((v_i_1),(v_i_2)),
  	and Δ_y is the absolute value of its
  	co-0-d-size [vertical d-size] (see Figure
  	<ref>).
  
  
  To deal with the belt-widths and the belt positions, it is useful to
  define two quasi-orders on the set of colourings {C|
  C=C_p,q, (p,q)∈ Q× Q},
  based on the belt-slopes and the lines  ℓ^C_L, ℓ^C_R
  defined below (which can differ from the lines
  ℓ_L, ℓ_R in Theorem <ref> and
  ℓ'_C, ℓ_C used in the proof of
  Proposition <ref>).
  For technical reasons we also extend the notion
  of border points to almost-border points of particular areas.
  
  
  
  
    
  Lines  l^C_L (leftmost with a white point) and
  l^C_R (rightmost with a black point).
  For each colouring C we define ℓ^C_L as
  the leftmost α_C-line that contains a point that is white in
  C, and ℓ^C_R as
  the rightmost α_C-line that contains a point that is black in
  C; we put ℓ^C_L=ℓ^C_R=h-axis if C is all-black
  (in which case α_C=0), and
  ℓ^C_L=ℓ^C_R=v-axis if C is all-white (in which case
  α_C=∞).
  We note that Theorem <ref>
  (depicted in Figure <ref>), which includes the
  fact
  that the belt-slopes α_C are rational or ∞,
  entails that the lines
  ℓ^C_L
  and
  ℓ^C_R
  are well-defined.
  
  We again note that the simulation preorder depicted
  in Figure <ref>,
  related to our simple example in Figure <ref>, can give an
  impression that ℓ^C_L is typically below (to the right of)
  ℓ^C_R; in this case
  (whenever ℓ^C_L is below ℓ^C_R), the distance between
  ℓ^C_L and
  ℓ^C_R is clearly at most 1 (and the distance 1 is achieved
  in the colouring C_p_2,p_1 in Figure <ref>).
  In more complicated examples, ℓ^C_L can be surely above (to
  the left of) ℓ^C_R; in Figure <ref>, ℓ^C_L
  would be between ℓ_L and ℓ'_C, and
   ℓ^C_R
  would be between ℓ_C and ℓ_R. In the case when ℓ^C_L
  is above ℓ^C_R
   the distance between
  ℓ^C_L and ℓ^C_R can be surely larger than 1; nevertheless
  it is polynomially bounded (in the size of Q of our fixed OCN
  =(Q,Act,δ)), as we discuss below.
  
  
  
    
  A counterclockwise quasi-order <=_L and a clockwise
  quasi-order
  <=_R on the set of colourings.
  The quasi-orders  and  on the set { C|
  C=C_p,q, (p,q)∈ Q× Q }
   are defined as follows:
  
  
  C C' if either α_C<α_C', or
  α_C=α_C' and ℓ^C_L is below (to the right of)
  ℓ^C'_L;
  
  
  
  
  C C' if either α_C>α_C', or
  α_C=α_C' and ℓ^C_R is above (to the left of)
  ℓ^C'_R.
  
  
  By C C' we denote that C C' and  C'C;
  the case C C' is analogous.
  
  We can recall the order α_1<α_2⋯ <α_k
  of belt-slopes (<ref>).
  Hence C C' iff α_C=α_i and α_C'=α_j
  where i<j, or i=j and ℓ^C_L is below (to the right of)
  ℓ^C'_L; analogously we can express  C C'.
  
  
  
  
  
  
    
  Almost-border points of
  Area(<-l)
  and Area(l->).
  
  We say that p∈(ℓ) is an
  almost-border point of (ℓ) if p has a neighbour point
  in (ℓ) (hence p is a border point
  of (ℓ) or has a neighbour point on ℓ).
  Similarly,  p∈(ℓ) is an
  almost-border point of (ℓ) if p has a neighbour point
  in (ℓ).
  
  
  
  The next proposition (Proposition <ref>) and its
  corollary (Corollary <ref>)
  show that the distances of lines
  ℓ^C_L and  ℓ^C_R to the origin  (0,0) are “small”,
  bounded by a polynomial in the number of colourings (hence in |Q× Q| for
  the underlying OCN  =(Q,Act,δ)); this also yields the
  announced polynomial bound on the distance between ℓ^C_L and
  ℓ^C_R (for any colouring C=C_p,q).
  
  Figure <ref> (the notation on which will be explained below)
  aims to illustrate that ℓ^C_R cannot intersect h-axis in a
  large distance to the right from the origin (0,0).
  This follows by Proposition <ref>(1) that entails
  that if the intersection of some ℓ^C_R with h-axis is
  to the right of (0,0), then the distance of this intersection
  to (0,0) is bounded by the product of a small number with the
  cardinality of the set {C'| C' C } (as follows by a
  repeated use of Proposition <ref>(1)).
  
  
  
  
  
  For each colouring C, and its respective lines  ℓ^C_L and
  	ℓ^C_R, we have:
  	
  		
    * If (0,0) is strictly above ℓ^C_R,
  			then there is C' C
  such that (ℓ^C'_R) contains a point that is
  			an almost-border point of
  			(ℓ^C_R).
  		
    * If (0,0) is strictly below ℓ^C_L,
  			then there is C' C
  such that (ℓ^C'_L) contains a point that is
  			an almost-border point of
  			(ℓ^C_L).
  	
  	
  
  1.
  Let us fix some C_0
  	such that (0,0) is strictly above ℓ^C_0_R (see
  	Figure <ref>); we will show that there is
  C'_0 C_0
  such that (ℓ^C'_0_R) contains a point that is
  			an almost-border point of
  			(ℓ^C_0_R).
  
  We put α=α_C_0, and
  	={C|α_C=α and C_0 C}.
  	Let ℓ be the leftmost α-line that is up-white in some
  	C∈; we fix such C̅∈.
  	Hence ℓ contains infinitely many points
  that are white in C̅ but only
  	finitely many points strictly above ℓ can be white
  	in any colouring C such that C_0 C (which includes all
  	C∈).
  	We can thus choose b∈_≥ 0 so that
   all points in
  	(v-axis,(b,ℓ))
  	(i.e., in the grey area in Figure <ref>)
  	that are strictly above
  	ℓ are black in all C such that C_0 C
  	(hence those points can be white only in some C C_0).
  
  	In C̅ we
  	consider a black-white vector v_0 such that
  	(v_0)∈(ℓ^C_0_R) (there must be a respective point that is  black in C̅
  	since C_0C̅) and
  	(v_0)∈ℓ; we have infinitely many possibilities on
  	ℓ for
  	such (v_0) (see Figure <ref>).
  
  We fix a sequence v_0,v_1,…,v_n guaranteed by
  	Corollary <ref>. There must be the least
  	i∈[1,n]
  	such that (v_i) is strictly above ℓ^C_0_R
  	(since (v_n) is on v-axis and thus strictly
  	above ℓ^C_0_R);
  hence (v_i)
  	is an almost-border point of
  	(ℓ^C_0_R)
  	(see again Figure <ref>).
  We could choose v_0 with
  	a sufficiently large α-d-size,
  	so that (v_i) is necessarily in (v-axis,(b,ℓ))
  	(in the grey area in Figure <ref>); moreover,
  (v_i) is strictly above ℓ. Hence v_i is black-white in
  	some C'_0 C_0, which entails that (v_i) (which is
  	an almost-border point of
  	(ℓ^C_0_R)) is in
  	(ℓ^C'_0_R).
  
  
  
  
  
  2. This condition is shown analogously as 1.
  Here we assume that
   (0,0) is strictly below ℓ^C_0_L, and put
  α=α_C_0 and
  	={C|α_C=α and C_0 C}.
  Now ℓ is the rightmost α-line that is down-black in some
  	C̅∈.
  We choose v_0, with a sufficiently large absolute value of α-d-size,
  so that	(v_0) is in (ℓ^C_0_L) and
  	white in C̅, and (v_0) is on ℓ and black in
  	C̅.
  
  
  To formulate the announced corollary,
  we introduce further technical notions (that also appear in
  Figure <ref>).
  
  
  
    
  Horizontal and vertical distances,
  values Step(alpha), H-Step(alpha), V-Step(alpha),
  and sigma_R(alpha),
  sigma_L(alpha),
  tau_R(C), tau_L(C).
  
  	
    * For a slope (a belt-slope in particular) α, 0<α<∞, let ℓ and ℓ'
  be two α-lines such that a unit square fits between them, with
  		its top-left corner on ℓ and its bottom-right
  		corner on ℓ' (see a grey square in Figure <ref>).
  By (α) we mean the (Euclidean) distance
  of the lines ℓ and ℓ', by (α) their horizontal
  		distance (i.e., the distance of their intersections
  		with h-axis), and by
   (α) their vertical distance.
  		We put (∞)=(∞)=1,
  		and  (0)=(0)=1.
  	
    * By ((0,0),ℓ) (((0,0),ℓ))
  		we mean the distance of
  		(0,0) to the intersection of ℓ with
  		h-axis (with v-axis).
  	
    * For a belt-slope α,
  by σ_R(α) we denote the number of equivalence classes of
  the equivalence ≡_R=∩⊒_R in the
  set of α-colourings.
  The value σ_L(α) is the number of classes of
  ≡_L=∩⊒_L in the set of
  		α-colourings.
  
    * For an α-colouring C, we define τ_R(C) to be the number of
  equivalence classes of ≡_R in the set
  { C' | C'  C'  C}.
  The value τ_L(C) is the number of classes of
  		≡_L in the set
  { C' | C'  C'  C}.
  		
  We note that (α)≤√(2) (with the equality for α = 1).
  If α is a belt-slope and  is the set of
  α-colourings,
  then Proposition <ref>
  entails that
  
      (α)≤ 1+|| if α>0 and
      	(α)≤ 1+|| if α<∞.
  
  Now we state the announced corollary of
  Proposition <ref>;
  we recall the order
   α_1<α_2⋯ <α_k
  of belt-slopes (<ref>) and look
  at Figure <ref>.
  
  
  
  
  	For each α_i-colouring C (where i∈[1,k]) we have:
    
      
    * if (0,0) is above ℓ^C_R and α_i>0, then
  
      ((0,0),ℓ^C_R)  ≤ (∑_j=i+1^k(α_j)·σ_R(α_j))+
      	(α_i)·τ_R(C);
  
  		  
    * if (0,0) is below ℓ_L^C and
  			  α_i<∞, then
  
      ((0,0),ℓ^C_L)  ≤ (∑_j=1^i-1(α_j)·σ_L(α_j))+
      	(α_i)·τ_L(C).
  
   
  
  
  By Proposition <ref>,
  Corollary <ref>, and the
  fact (<ref>) we get:
  
  
  
  
  
  	The slopes, widths, and positions of belts from
  	Theorem <ref> can be presented by integers that
  	are polynomial in |Q|, referring to the underlying OCN
  	=(Q,Act,δ).
  
  
  We could describe the respective polynomials more specifically,
  but this is not necessary for deriving the -membership for the
  simulation problem on one-counter nets, which is sketched in the next
  subsection.
  
  
  
  
  
  
  
  
   §.§ Polynomial-space algorithm
  
  
  Based on the basic belt theorem, a straightforward algorithm that
  decides
  whether p(m) q(n) for a given OCN ,
  or more generally constructs a description of  on the LTS
  _, was given
  in <cit.>;
  taking the “polynomial” slopes and widths of belts into account, we
  get polynomial-space algorithms <cit.>.
  In principle, we can use “brute force” and simply construct an initial rectangle of the
  planes ×, first assuming that all points are black in
  all colourings, and
  stepwise recolouring to white when finding points with ranks
  1,2,3,…. It is easy to note that the colouring inside the belts is
  (ultimately) periodic, i.e., after a possible initial segment another segment
  repeats forever.
  The belt periods can be (and sometimes are)
  exponential, hence the above “brute-force” algorithm would also use
  exponential space to discover the repeated belt-segments and provide
  a complete description of the relation  (on the LTS
  _).
  Nevertheless, it is a technical routine to modify
  the algorithm so that it uses only
  a polynomial work-space.
  
  
  
  
  
  
  
  § REMARK ON DOUBLE-EXPONENTIAL PERIODS
  
  
  We have mentioned the periodic colouring of the
  simulation-belts for OCNs, where the periods can be exponential.
  It is not so surprising then that these periods
  for SOCNs can be double-exponential, which we now discuss in more
  detail.
  In fact, by our constructions this is a corollary of the fact that
  the periods of sequences  given by sequence descriptions
  =(Δ,D,m) can be double-exponential w.r.t. the size
  of  (where m is presented in binary); this also entails that
  the period in the sequence W(0),W(1),W(2),… for the countdown
  games (recall Section <ref>) can be double-exponential.
  Hence we concentrate just on the sequences .
  
  Given =(Δ,D,m) (where D:Δ^3→Δ), we recall
  that :→Δ satisfies
  (0)=, (1)=(2)=⋯=(m)=,
  and (i)=D((i-m-1),(i-m),(i-m+1))
  for i>m.
  It is thus obvious that there are  i_0,d ≤Δ^m+1, where d≥ 1,
  such that (i+d)=(i) for each i≥ i_0
  (in , after an initial segment of length i_0, a segment of the
  period-length d is repeated forever). We now show that the least
  such d can be double-exponential.
  
  
  
  For each n∈ there is a sequence description  of size polynomial
  in n such that for some d≥ 2^2^n we have (i)=
  iff i is a multiple of d; moreover,
  	(i+d)=(i) for each i≥ 0.
  
  
  We fix a Turing machine
  =(Q,Σ,Γ,δ,q_0,{}),
  	with Σ={0} and Γ⊇{0,1,,$}  that behaves as follows.
  	Starting from the configuration q_00^n, 
  	writes the word $0^m$ on the tape, where  m=2^n,
  	while visiting only the cells 0,1,…,m+1.
  	Now, inside this space (the cells 0,1,…,m+1), all
  	w∈{0,1}^m are stepwise generated;
  the tape content, always of length m+2,
  	will stepwise become $0⋯000$,
  	$0⋯001$,
  	$0⋯010$,
  	$0⋯011$, ⋯⋯,
  	 $1⋯1$.
  Finally  rewrites all cells
  with , and halts at the cell 0 in .
  Hence  uses only cells 0,1,…, m+1 and performs
   t steps where t>2^m=2^2^n.
  
  Now for each n∈ we consider
  a Turing machine _n that, when starting in q'_0 on the empty
  tape, first
  	 writes 0^n, then invokes the computation of 
  	on 0^n, and when  halts (in ), then _n
   restores its initial configuration with the empty tape; the initial
  	state q'_0 will be visited only at the start and at the end
  	of the described computation.
  
  Hence the computation C_0,C_1,C_2,… of _n from q'_0 and the empty tape is
  	infinite, visits only the cells 0,1,…,m+1 for m=2^n,
  and there is d_0≥ 2^2^n such that
  	the control state q_0' is visited
  exactly in the configurations C_i where i is a multiple of d_0.
  We also note
  	that the size of _n is (n).
  
  	The infinite word C_0C_1C_2… (each C_i of length m+2)
  	can be viewed as  for
   a sequence description  of size polynomial with respect to n
  	(recall the proof of
  	Proposition <ref>).
  	For 	d=d_0·(m+2) we thus have
  	(i)=(i+d) for all i∈.
  Moreover, we identify  with the pair (q_0',), which entails
  that (i)= iff i is a multiple of d.
  
  
  
  
  
  
  
  
  § ADDITIONAL REMARKS
  
  
  One particular application of countdown games was shown by
  Kiefer <cit.> who
  modified them
  to show -hardness of
  bisimilarity on BPA processes.
  Our -complete modification does
  not seem easily implementable by BPA processes, hence
  the -hardness result
  in <cit.> has not been improved here.
  (The known upper bound for bisimilarity on BPA is .)
  
  
  
  We also mention that the involved result
  in <cit.>
  shows that, given any fixed language L in , for any word w
  (in the alphabet of L) we can construct
  a succinct one-counter automaton that performs a computation which
  is accepting iff w∈ L.
  Such a computation needs to access
  concrete bits in the (reversed) binary presentation of the counter value.
  A straightforward direct access to such bits is destructive (the counter
  value is lost after the bit is read) but this can be avoided:
  instead of a “destructive reading” the computation just “guesses”
  the respective bits, and it is forced to guess correctly by a carefully
  constructed CTL formula that is required to be satisfied by the
  computation.
  This result is surely deeper than
  the -hardness of existential countdown games, though the
  former does not seem to entail the latter immediately.
  
  Finally we note that the theorems and proofs in Section <ref>
  could be formulated for specific tiling problems, without a direct
  reference to one-counter nets.
  
  
  
  
  § ACKNOWLEDGEMENTS.
  
  We thank the anonymous reviewers for their helpful comments.
  
  
  
  
  
  alphaurl
  
  
  