diff --git a/src/ltlast/formula.hh b/src/ltlast/formula.hh
index cd73a513e..ba79ed952 100644
--- a/src/ltlast/formula.hh
+++ b/src/ltlast/formula.hh
@@ -1076,12 +1076,12 @@ namespace spot
       {
 	return ptr_->end();
       }
-#endif
 
-      formula nth(unsigned i) const
+      formula operator[](unsigned i) const
       {
 	return formula(ptr_->nth(i)->clone());
       }
+#endif
 
       static formula ff()
       {
@@ -1206,7 +1206,7 @@ namespace spot
 	  case op::Closure:
 	  case op::NegClosure:
 	  case op::NegClosureMarked:
-	    return unop(o, trans(nth(0)));
+	    return unop(o, trans((*this)[0]));
 	  case op::Xor:
 	  case op::Implies:
 	  case op::Equiv:
@@ -1218,8 +1218,8 @@ namespace spot
 	  case op::EConcatMarked:
 	  case op::UConcat:
 	    {
-	      formula tmp = trans(nth(0));
-	      return binop(o, tmp, trans(nth(1)));
+	      formula tmp = trans((*this)[0]);
+	      return binop(o, tmp, trans((*this)[1]));
 	    }
 	  case op::Or:
 	  case op::OrRat:
@@ -1237,7 +1237,7 @@ namespace spot
 	    }
 	  case op::Star:
 	  case op::FStar:
-	    return bunop(o, trans(nth(0)), min(), max());
+	    return bunop(o, trans((*this)[0]), min(), max());
 	  }
 	SPOT_UNREACHABLE();
       }
diff --git a/src/ltlvisit/mark.cc b/src/ltlvisit/mark.cc
index 2df7ef966..195eff603 100644
--- a/src/ltlvisit/mark.cc
+++ b/src/ltlvisit/mark.cc
@@ -63,10 +63,10 @@ namespace spot
 	  res = f;
 	  break;
 	case op::NegClosure:
-	  res = ltl::formula::NegClosureMarked(f.nth(0));
+	  res = ltl::formula::NegClosureMarked(f[0]);
 	  break;
 	case op::EConcat:
-	  res = ltl::formula::EConcatMarked(f.nth(0), f.nth(1));
+	  res = ltl::formula::EConcatMarked(f[0], f[1]);
 	  break;
 	case op::Or:
 	case op::And:
@@ -138,7 +138,7 @@ namespace spot
 	      {
 		if (c.is(op::EConcatMarked))
 		  {
-		    empairs.emplace(c.nth(0), c.nth(1));
+		    empairs.emplace(c[0], c[1]);
 		    v.push_back(c.map(recurse));
 		  }
 		else if (c.is(op::EConcat))
@@ -147,7 +147,7 @@ namespace spot
 		  }
 		else if (c.is(op::NegClosureMarked))
 		  {
-		    nmset.insert(c.nth(0));
+		    nmset.insert(c[0]);
 		    v.push_back(c.map(recurse));
 		  }
 		else if (c.is(op::NegClosure))
@@ -162,13 +162,13 @@ namespace spot
 	    // Keep only the non-marked EConcat for which we
 	    // have not seen a similar EConcatMarked.
 	    for (auto e:  elist)
-	      if (empairs.find(std::make_pair(e.nth(0), e.nth(1)))
+	      if (empairs.find(std::make_pair(e[0], e[1]))
 		  == empairs.end())
 		v.push_back(e);
 	    // Keep only the non-marked NegClosure for which we
 	    // have not seen a similar NegClosureMarked.
 	    for (auto n: nlist)
-	      if (nmset.find(n.nth(0)) == nmset.end())
+	      if (nmset.find(n[0]) == nmset.end())
 		v.push_back(n);
 	    res = ltl::formula::And(v);
 	  }
diff --git a/src/ltlvisit/mutation.cc b/src/ltlvisit/mutation.cc
index 7b48e322e..981d7544d 100644
--- a/src/ltlvisit/mutation.cc
+++ b/src/ltlvisit/mutation.cc
@@ -86,7 +86,7 @@ namespace spot
 	    case op::G:
 	      if ((opts_ & Mut_Remove_Ops)
 		  && mutation_counter_-- == 0)
-		return f.nth(0);
+		return f[0];
 	      // fall through
 	    case op::Closure:
 	    case op::NegClosure:
@@ -118,7 +118,7 @@ namespace spot
 		      {
 			vec v1;
 			vec v2;
-			v1.push_back(f.nth(0));
+			v1.push_back(f[0]);
 			bool reverse = false;
 			int i = 1;
 			while (i < mos)
@@ -130,10 +130,10 @@ namespace spot
 				reverse = true;
 				break;
 			      }
-			    v1.push_back(f.nth(i++));
+			    v1.push_back(f[i++]);
 			  }
 			for (; i < mos; ++i)
-			  v2.push_back(f.nth(i));
+			  v2.push_back(f[i]);
 			formula first = AndNLM_(v1);
 			formula second = AndNLM_(v2);
 			formula ost = formula::one_star();
@@ -164,8 +164,8 @@ namespace spot
 	    case op::EConcatMarked:
 	    case op::UConcat:
 	      {
-		formula first = f.nth(0);
-		formula second = f.nth(1);
+		formula first = f[0];
+		formula second = f[1];
 		op o = f.kind();
 		bool left_is_sere = o == op::EConcat
 		  || o == op::EConcatMarked
@@ -242,7 +242,7 @@ namespace spot
 	    case op::Star:
 	    case op::FStar:
 	      {
-		formula c = f.nth(0);
+		formula c = f[0];
 		op o = f.kind();
 		if (opts_ & Mut_Remove_Ops && mutation_counter_-- == 0)
 		  return c;
diff --git a/src/ltlvisit/print.cc b/src/ltlvisit/print.cc
index 97ac7788b..84398fe4e 100644
--- a/src/ltlvisit/print.cc
+++ b/src/ltlvisit/print.cc
@@ -348,10 +348,10 @@ namespace spot
       match_goto(formula mo, unsigned i)
       {
 	assert(i + 1 < mo.size());
-	formula b = strip_star_not(mo.nth(i));
+	formula b = strip_star_not(mo[i]);
 	if (b == nullptr || !b.is_boolean())
 	  return nullptr;
-	if (mo.nth(i + 1) == b)
+	if (mo[i + 1] == b)
 	  return b;
 	return nullptr;
       }
@@ -482,7 +482,7 @@ namespace spot
 	      break;
 	    case op::Not:
 	      {
-		formula c = f.nth(0);
+		formula c = f[0];
 		if (c.is(op::AP))
 		  {
 		    // If we negate a single letter in UTF-8, use a
@@ -514,15 +514,15 @@ namespace spot
 	      }
 	    case op::X:
 	      emit(KX);
-	      visit(f.nth(0));
+	      visit(f[0]);
 	      break;
 	    case op::F:
 	      emit(KF);
-	      visit(f.nth(0));
+	      visit(f[0]);
 	      break;
 	    case op::G:
 	      emit(KG);
-	      visit(f.nth(0));
+	      visit(f[0]);
 	      break;
 	    case op::NegClosure:
 	    case op::NegClosureMarked:
@@ -534,45 +534,45 @@ namespace spot
 	      os_ << '{';
 	      in_ratexp_ = true;
 	      top_level_ = true;
-	      visit(f.nth(0));
+	      visit(f[0]);
 	      os_ << '}';
 	      in_ratexp_ = false;
 	      top_level_ = false;
 	      break;
 	    case op::Xor:
-	      visit(f.nth(0));
+	      visit(f[0]);
 	      emit(KXor);
-	      visit(f.nth(1));
+	      visit(f[1]);
 	      break;
 	    case op::Implies:
-	      visit(f.nth(0));
+	      visit(f[0]);
 	      emit(KImplies);
-	      visit(f.nth(1));
+	      visit(f[1]);
 	      break;
 	    case op::Equiv:
-	      visit(f.nth(0));
+	      visit(f[0]);
 	      emit(KEquiv);
-	      visit(f.nth(1));
+	      visit(f[1]);
 	      break;
 	    case op::U:
-	      visit(f.nth(0));
+	      visit(f[0]);
 	      emit(KU);
-	      visit(f.nth(1));
+	      visit(f[1]);
 	      break;
 	    case op::R:
-	      visit(f.nth(0));
+	      visit(f[0]);
 	      emit(KR);
-	      visit(f.nth(1));
+	      visit(f[1]);
 	      break;
 	    case op::W:
-	      visit(f.nth(0));
+	      visit(f[0]);
 	      emit(KW);
-	      visit(f.nth(1));
+	      visit(f[1]);
 	      break;
 	    case op::M:
-	      visit(f.nth(0));
+	      visit(f[0]);
 	      emit(KM);
-	      visit(f.nth(1));
+	      visit(f[1]);
 	      break;
 	    case op::EConcat:
 	    case op::EConcatMarked:
@@ -581,11 +581,11 @@ namespace spot
 		in_ratexp_ = true;
 		openp();
 		top_level_ = true;
-		formula left = f.nth(0);
-		formula right = f.nth(1);
+		formula left = f[0];
+		formula right = f[1];
 		unsigned last = left.size() - 1;
 		bool onelast = false;
-		if (left.is(op::Concat) && left.nth(last).is(op::True))
+		if (left.is(op::Concat) && left[last].is_true())
 		  {
 		    visit(left.all_but(last));
 		    onelast = true;
@@ -609,7 +609,7 @@ namespace spot
 		  }
 		else if (o == op::EConcat)
 		  {
-		    if (f.nth(1).is(op::True))
+		    if (f[1].is(op::True))
 		      {
 			os_ << '!';
 			// No recursion on right.
@@ -633,7 +633,7 @@ namespace spot
 	    case op::AndNLM:
 	    case op::Fusion:
 	      {
-		visit(f.nth(0));
+		visit(f[0]);
 		keyword k = KFalse; // Initialize to something to please GCC.
 		switch (o)
 		  {
@@ -664,7 +664,7 @@ namespace spot
 		for (unsigned n = 1; n < max; ++n)
 		  {
 		    emit(k);
-		    visit(f.nth(n));
+		    visit(f[n]);
 		  }
 		break;
 	      }
@@ -686,7 +686,7 @@ namespace spot
 
 			    // Wait... maybe we are looking at (!b)[*];b;(!b)[*]
 			    // in which case it's b[=1].
-			    if (i + 2 < max && f.nth(i) == f.nth(i + 2))
+			    if (i + 2 < max && f[i] == f[i + 2])
 			      {
 				emit(KEqualBunop);
 				os_ << '1';
@@ -702,12 +702,12 @@ namespace spot
 			    continue;
 			  }
 			// Try to match ((!b)[*];b)[*i..j];(!b)[*]
-			formula fi = f.nth(i);
+			formula fi = f[i];
 			if (fi.is(op::Star))
 			  {
-			    if (formula b2 = strip_star_not(f.nth(i + 1)))
+			    if (formula b2 = strip_star_not(f[i + 1]))
 			      {
-				formula fic = fi.nth(0);
+				formula fic = fi[0];
 				if (fic.is(op::Concat))
 				  if (formula b1 = match_goto(fic, 0))
 				    if (b1 == b2)
@@ -730,14 +730,14 @@ namespace spot
 			      }
 			  }
 		      }
-		    visit(f.nth(i));
+		    visit(f[i]);
 		  }
 		break;
 	      }
 	    case op::Star:
 	    case op::FStar:
 	      {
-		formula c = f.nth(0);
+		formula c = f[0];
 		enum { Star, FStar, Goto } sugar = Star;
 		unsigned default_min = 0;
 		unsigned default_max = formula::unbounded();
diff --git a/src/ltlvisit/relabel.cc b/src/ltlvisit/relabel.cc
index b02bd4e97..d715fc38c 100644
--- a/src/ltlvisit/relabel.cc
+++ b/src/ltlvisit/relabel.cc
@@ -280,24 +280,24 @@ namespace spot
 		visit(b);
 	    }
 	  for (; i < sz; ++i)
-	    visit(f.nth(i));
+	    visit(f[i]);
 	  if (sz > 1 && f.is_boolean())
 	    {
 	      // For Boolean nodes, connect all children in a
 	      // loop.  This way the node can only be a cut-point
 	      // if it separates all children from the reset of
 	      // the graph (not only one).
-	      formula pred = f.nth(0);
+	      formula pred = f[0];
 	      for (i = 1; i < sz; ++i)
 		{
-		  formula next = f.nth(i);
+		  formula next = f[i];
 		  // Note that we only add an edge in one
 		  // direction, because we are building a cycle
 		  // between all children anyway.
 		  g[pred].push_back(next);
 		  pred = next;
 		}
-	      g[pred].push_back(f.nth(0));
+	      g[pred].push_back(f[0]);
 	    }
 	  s.pop();
 	}
@@ -446,7 +446,7 @@ namespace spot
 	      res.reserve(sz);
 	    }
 	  for (; i < sz; ++i)
-	    res.push_back(visit(f.nth(i)));
+	    res.push_back(visit(f[i]));
 	  return formula::multop(f.kind(), res);
 	}
       };
diff --git a/src/ltlvisit/remove_x.cc b/src/ltlvisit/remove_x.cc
index eec440c13..81491f894 100644
--- a/src/ltlvisit/remove_x.cc
+++ b/src/ltlvisit/remove_x.cc
@@ -41,7 +41,7 @@ namespace spot
 	if (!f.is(op::X))
 	  return f.map(rec);
 
-	formula c = rec(f.nth(0));
+	formula c = rec(f[0]);
 
 	std::vector<formula> vo;
 	for (auto i: aps)
diff --git a/src/ltlvisit/simpfg.cc b/src/ltlvisit/simpfg.cc
index cc9fb818b..d5a15bf64 100644
--- a/src/ltlvisit/simpfg.cc
+++ b/src/ltlvisit/simpfg.cc
@@ -29,17 +29,17 @@ namespace spot
     formula simplify_f_g(formula p)
     {
       // 1 U p = Fp
-      if (p.is(op::U) && p.nth(0).is_true())
-	return formula::F(p.nth(1));
+      if (p.is(op::U) && p[0].is_true())
+	return formula::F(p[1]);
       // 0 R p = Gp
-      if (p.is(op::R) && p.nth(0).is_false())
-	return formula::G(p.nth(1));
+      if (p.is(op::R) && p[0].is_false())
+	return formula::G(p[1]);
       // p W 0 = Gp
-      if (p.is(op::W) && p.nth(1).is_false())
-	return formula::G(p.nth(0));
+      if (p.is(op::W) && p[1].is_false())
+	return formula::G(p[0]);
       // p M 1 = Fp
-      if (p.is(op::M) && p.nth(1).is_true())
-	return formula::F(p.nth(0));
+      if (p.is(op::M) && p[1].is_true())
+	return formula::F(p[0]);
       return p.map(simplify_f_g);
     }
 
diff --git a/src/ltlvisit/simplify.cc b/src/ltlvisit/simplify.cc
index b61cd64c3..479cd0004 100644
--- a/src/ltlvisit/simplify.cc
+++ b/src/ltlvisit/simplify.cc
@@ -110,16 +110,16 @@ namespace spot
 	    result = bdd_ithvar(dict->register_proposition(f, this));
 	    break;
 	  case op::Not:
-	    result = !as_bdd(f.nth(0));
+	    result = !as_bdd(f[0]);
 	    break;
 	  case op::Xor:
-	    result = bdd_apply(as_bdd(f.nth(0)), as_bdd(f.nth(1)), bddop_xor);
+	    result = bdd_apply(as_bdd(f[0]), as_bdd(f[1]), bddop_xor);
 	    break;
 	  case op::Implies:
-	    result = bdd_apply(as_bdd(f.nth(0)), as_bdd(f.nth(1)), bddop_imp);
+	    result = bdd_apply(as_bdd(f[0]), as_bdd(f[1]), bddop_imp);
 	    break;
 	  case op::Equiv:
-	    result = bdd_apply(as_bdd(f.nth(0)), as_bdd(f.nth(1)), bddop_biimp);
+	    result = bdd_apply(as_bdd(f[0]), as_bdd(f[1]), bddop_biimp);
 	    break;
 	  case op::And:
 	    {
@@ -361,7 +361,7 @@ namespace spot
 	if (f.is(op::Not))
 	  {
 	    negated = !negated;
-	    f = f.nth(0);
+	    f = f[0];
 	  }
 
 	formula key = f;
@@ -398,83 +398,83 @@ namespace spot
 		break;
 	      case op::X:
 		// !Xa == X!a
-		result = formula::X(rec(f.nth(0), negated));
+		result = formula::X(rec(f[0], negated));
 		break;
 	      case op::F:
 		// !Fa == G!a
 		result = formula::unop(negated ? op::G : op::F,
-				       rec(f.nth(0), negated));
+				       rec(f[0], negated));
 		break;
 	      case op::G:
 		// !Ga == F!a
 		result = formula::unop(negated ? op::F : op::G,
-				       rec(f.nth(0), negated));
+				       rec(f[0], negated));
 		break;
 	      case op::Closure:
 		result = formula::unop(negated ?
 				       op::NegClosure : op::Closure,
-				       rec(f.nth(0), false));
+				       rec(f[0], false));
 		break;
 	      case op::NegClosure:
 	      case op::NegClosureMarked:
 		result = formula::unop(negated ? op::Closure : o,
-				       rec(f.nth(0), false));
+				       rec(f[0], false));
 		break;
 
 	      case op::Implies:
 		if (negated)
 		  // !(a => b) == a & !b
 		  {
-		    auto f2 = rec(f.nth(1), true);
-		    result = formula::And({rec(f.nth(0), false), f2});
+		    auto f2 = rec(f[1], true);
+		    result = formula::And({rec(f[0], false), f2});
 		  }
 		else // a => b == !a | b
 		  {
-		    auto f2 = rec(f.nth(1), false);
-		    result = formula::Or({rec(f.nth(0), true), f2});
+		    auto f2 = rec(f[1], false);
+		    result = formula::Or({rec(f[0], true), f2});
 		  }
 		break;
 	      case op::Xor:
 		{
 		  // !(a ^ b) == a <=> b
-		  result = equiv_or_xor(negated, f.nth(0), f.nth(1), c);
+		  result = equiv_or_xor(negated, f[0], f[1], c);
 		  break;
 		}
 	      case op::Equiv:
 		{
 		  // !(a <=> b) == a ^ b
-		  result = equiv_or_xor(!negated, f.nth(0), f.nth(1), c);
+		  result = equiv_or_xor(!negated, f[0], f[1], c);
 		  break;
 		}
 	      case op::U:
 		{
 		  // !(a U b) == !a R !b
-		  auto f1 = rec(f.nth(0), negated);
-		  auto f2 = rec(f.nth(1), negated);
+		  auto f1 = rec(f[0], negated);
+		  auto f2 = rec(f[1], negated);
 		  result = formula::binop(negated ? op::R : op::U, f1, f2);
 		  break;
 		}
 	      case op::R:
 		{
 		  // !(a R b) == !a U !b
-		  auto f1 = rec(f.nth(0), negated);
-		  auto f2 = rec(f.nth(1), negated);
+		  auto f1 = rec(f[0], negated);
+		  auto f2 = rec(f[1], negated);
 		  result = formula::binop(negated ? op::U : op::R, f1, f2);
 		  break;
 		}
 	      case op::W:
 		{
 		  // !(a W b) == !a M !b
-		  auto f1 = rec(f.nth(0), negated);
-		  auto f2 = rec(f.nth(1), negated);
+		  auto f1 = rec(f[0], negated);
+		  auto f2 = rec(f[1], negated);
 		  result = formula::binop(negated ? op::M : op::W, f1, f2);
 		  break;
 		}
 	      case op::M:
 		{
 		  // !(a M b) == !a W !b
-		  auto f1 = rec(f.nth(0), negated);
-		  auto f2 = rec(f.nth(1), negated);
+		  auto f1 = rec(f[0], negated);
+		  auto f2 = rec(f[1], negated);
 		  result = formula::binop(negated ? op::W : op::M, f1, f2);
 		  break;
 		}
@@ -484,7 +484,7 @@ namespace spot
 		  unsigned mos = f.size();
 		  vec v;
 		  for (unsigned i = 0; i < mos; ++i)
-		    v.push_back(rec(f.nth(i), negated));
+		    v.push_back(rec(f[i], negated));
 		  op on = o;
 		  if (negated)
 		    on = o == op::Or ? op::And : op::Or;
@@ -511,8 +511,8 @@ namespace spot
 	      case op::EConcatMarked:
 		{
 		  // !(a <>-> b) == a[]-> !b
-		  auto f1 = f.nth(0);
-		  auto f2 = f.nth(1);
+		  auto f1 = f[0];
+		  auto f2 = f[1];
 		  result = formula::binop(negated ? op::UConcat : o,
 					  rec(f1, false), rec(f2, negated));
 		  break;
@@ -520,8 +520,8 @@ namespace spot
 	      case op::UConcat:
 		{
 		  // !(a []-> b) == a<>-> !b
-		  auto f1 = f.nth(0);
-		  auto f2 = f.nth(1);
+		  auto f1 = f[0];
+		  auto f2 = f[1];
 		  result = formula::binop(negated ? op::EConcat : op::UConcat,
 					  rec(f1, false), rec(f2, negated));
 		  break;
@@ -553,10 +553,10 @@ namespace spot
       {
 	if (!f.is(op::R, op::M))
 	  return nullptr;
-	auto left = f.nth(0);
+	auto left = f[0];
 	if (!left.is(op::X))
 	  return nullptr;
-	return left.nth(0);
+	return left[0];
       }
 
       // X(a) W b   or   X(a) U b
@@ -566,10 +566,10 @@ namespace spot
       {
 	if (!f.is(op::W, op::U))
 	  return nullptr;
-	auto left = f.nth(0);
+	auto left = f[0];
 	if (!left.is(op::X))
 	  return nullptr;
-	return left.nth(0);
+	return left[0];
       }
 
       // b & X(b W a)  or   b & X(b U a)
@@ -582,14 +582,14 @@ namespace spot
 	unsigned s = f.size();
 	for (unsigned pos = 0; pos < s; ++pos)
 	  {
-	    auto p = f.nth(pos);
+	    auto p = f[pos];
 	    if (!(p.is(op::X)))
 	      continue;
-	    auto c = p.nth(0);
+	    auto c = p[0];
 	    if (!c.is(op::U, op::W))
 	      continue;
 	    formula b = f.all_but(pos);
-	    if (b == c.nth(0))
+	    if (b == c[0])
 	      return c;
 	  }
 	return nullptr;
@@ -605,14 +605,14 @@ namespace spot
 	unsigned s = f.size();
 	for (unsigned pos = 0; pos < s; ++pos)
 	  {
-	    auto p = f.nth(pos);
+	    auto p = f[pos];
 	    if (!(p.is(op::X)))
 	      continue;
-	    auto c = p.nth(0);
+	    auto c = p[0];
 	    if (!c.is(op::R, op::M))
 	      continue;
 	    formula b = f.all_but(pos);
-	    if (b == c.nth(0))
+	    if (b == c[0])
 	      return c;
 	  }
 	return nullptr;
@@ -691,7 +691,7 @@ namespace spot
 	  unsigned mos = mo.size();
 	  for (unsigned i = 0; i < mos; ++i)
 	    {
-	      formula f = simplify_recursively(mo.nth(i), cache);
+	      formula f = simplify_recursively(mo[i], cache);
 	      process(f);
 	    }
 	}
@@ -706,17 +706,17 @@ namespace spot
 	    case op::X:
 	      if (res_X && !eu)
 		{
-		  res_X->push_back(f.nth(0));
+		  res_X->push_back(f[0]);
 		  return;
 		}
 	      break;
 	    case op::F:
 	      {
-		formula c = f.nth(0);
+		formula c = f[0];
 		if (res_FG && u && c.is(op::G))
 		  {
 		    res_FG->push_back(((split_ & Strip_FG) == Strip_FG
-				       ? c.nth(0) : f));
+				       ? c[0] : f));
 		    return;
 		  }
 		if (res_F && !eu)
@@ -729,11 +729,11 @@ namespace spot
 	      }
 	    case op::G:
 	      {
-		formula c = f.nth(0);
+		formula c = f[0];
 		if (res_GF && e && c.is(op::F))
 		  {
 		    res_GF->push_back(((split_ & Strip_GF) == Strip_GF
-				       ? c.nth(0) : f));
+				       ? c[0] : f));
 		    return;
 		  }
 		if (res_G && !eu)
@@ -858,7 +858,7 @@ namespace spot
 		return f;
 	      case op::X:
 		{
-		  formula c = f.nth(0);
+		  formula c = f[0];
 		  // Xf = f if f is both eventual and universal.
 		  if (c.is_universal() && c.is_eventual())
 		    {
@@ -907,7 +907,7 @@ namespace spot
 		}
 	      case op::F:
 		{
-		  formula c = f.nth(0);
+		  formula c = f[0];
 		  // If f is a pure eventuality formula then F(f)=f.
 		  if (opt_.event_univ && c.is_eventual())
 		    return c;
@@ -916,30 +916,30 @@ namespace spot
 		    {
 		      // F(a U b) = F(b)
 		      if (c.is(op::U))
-			return recurse(formula::F(c.nth(1)));
+			return recurse(formula::F(c[1]));
 
 		      // F(a M b) = F(a & b)
 		      if (c.is(op::M))
 			return recurse(unop_multop(op::F, op::And,
-						   {c.nth(0), c.nth(1)}));
+						   {c[0], c[1]}));
 
 		      // FX(a) = XF(a)
 		      // FXX(a) = XXF(a) ...
 		      // FXG(a) = XFG(a) = FG(a) ...
 		      if (c.is(op::X))
-			return recurse(unop_unop(op::X, op::F, c.nth(0)));
+			return recurse(unop_unop(op::X, op::F, c[0]));
 
 		      // FG(a & Xb) = FG(a & b)
 		      // FG(a & Gb) = FG(a & b)
 		      if (c.is({op::G, op::And}))
 			{
-			  formula m = c.nth(0);
+			  formula m = c[0];
 			  if (!m.is_boolean())
 			    {
 			      formula out = m.map([](formula f)
 						  {
 						    if (f.is(op::X, op::G))
-						      return f.nth(0);
+						      return f[0];
 						    return f;
 						  });
 			      if (out != m)
@@ -1012,7 +1012,7 @@ namespace spot
 			  // Strip any F.
 			  for (auto& g: *s.res_Univ)
 			    if (g.is(op::F))
-			      g = g.nth(0);
+			      g = g[0];
 			  formula fu = unop_multop(op::F, op::Or,
 						   std::move(*s.res_Univ));
 			  res = formula::Or({res, fu});
@@ -1024,7 +1024,7 @@ namespace spot
 		return f;
 	      case op::G:
 		{
-		  formula c = f.nth(0);
+		  formula c = f[0];
 		  // If f is a pure universality formula then G(f)=f.
 		  if (opt_.event_univ && c.is_universal())
 		    return c;
@@ -1033,18 +1033,18 @@ namespace spot
 		    {
 		      // G(a R b) = G(b)
 		      if (c.is(op::R))
-			return recurse(formula::G(c.nth(1)));
+			return recurse(formula::G(c[1]));
 
 		      // G(a W b) = G(a | b)
 		      if (c.is(op::W))
 			return recurse(unop_multop(op::G, op::Or,
-						   {c.nth(0), c.nth(1)}));
+						   {c[0], c[1]}));
 
 		      // GX(a) = XG(a)
 		      // GXX(a) = XXG(a) ...
 		      // GXF(a) = XGF(a) = GF(a) ...
 		      if (c.is(op::X))
-			return recurse(unop_unop(op::X, op::G, c.nth(0)));
+			return recurse(unop_unop(op::X, op::G, c[0]));
 
 		      // G(f1|f2|GF(f3)|GF(f4)|f5|f6) =
 		      //                        G(f1|f2) | GF(f3|f4) | f5 | f6
@@ -1089,7 +1089,7 @@ namespace spot
 			      // Strip any G.
 			      for (auto& g: *s.res_Event)
 				if (g.is(op::G))
-				  g = g.nth(0);
+				  g = g[0];
 			      formula ge =
 				unop_multop(op::G, op::And,
 					    std::move(*s.res_Event));
@@ -1103,13 +1103,13 @@ namespace spot
 		      // GF(a | Fb) = GF(a | b)
 		      if (c.is({op::F, op::Or}))
 			{
-			  formula m = c.nth(0);
+			  formula m = c[0];
 			  if (!m.is_boolean())
 			    {
 			      formula out = m.map([](formula f)
 						  {
 						    if (f.is(op::X, op::F))
-						      return f.nth(0);
+						      return f[0];
 						    return f;
 						  });
 			      if (out != m)
@@ -1127,11 +1127,11 @@ namespace spot
 	      case op::NegClosure:
 	      case op::NegClosureMarked:
 		{
-		  formula c = f.nth(0);
+		  formula c = f[0];
 		  // {e[*]} = {e}
 		  // !{e[*]} = !{e}
 		  if (c.accepts_eword() && c.is(op::Star))
-		    return recurse(formula::unop(o, c.nth(0)));
+		    return recurse(formula::unop(o, c[0]));
 
 		  if (!opt_.reduce_size_strictly)
 		    if (c.is(op::OrRat))
@@ -1141,7 +1141,7 @@ namespace spot
 			unsigned s = c.size();
 			vec v;
 			for (unsigned n = 0; n < s; ++n)
-			  v.push_back(formula::unop(o, c.nth(n)));
+			  v.push_back(formula::unop(o, c[n]));
 			return recurse(formula::multop(o == op::Closure
 						       ? op::Or : op::And, v));
 		      }
@@ -1158,7 +1158,7 @@ namespace spot
 			  unsigned end = c.size();
 			  v.reserve(end);
 			  for (unsigned i = 0; i < end; ++i)
-			    v.push_back(formula::unop(o, c.nth(i)));
+			    v.push_back(formula::unop(o, c[i]));
 			  return recurse(formula::multop(o == op::Closure ?
 							 op::Or : op::And, v));
 			}
@@ -1171,12 +1171,12 @@ namespace spot
 		      //    = !b₁|X(!b₂|X(!{e₁;f₁;e₂;f₂}))
 		      // if e denotes a term that accepts [*0]
 		      // and b denotes a Boolean formula.
-		      while (c.nth(end).accepts_eword())
+		      while (c[end].accepts_eword())
 			--end;
 		      unsigned start = 0;
 		      while (start <= end)
 			{
-			  formula r = c.nth(start);
+			  formula r = c[start];
 			  if (r.is_boolean() && !opt_.reduce_size_strictly)
 			    ++start;
 			  else
@@ -1192,7 +1192,7 @@ namespace spot
 			      vec v;
 			      v.reserve(s);
 			      for (unsigned n = start; n <= end; ++n)
-				v.push_back(c.nth(n));
+				v.push_back(c[n]);
 			      tail = formula::Concat(v);
 			      tail = formula::unop(o, tail);
 			    }
@@ -1204,7 +1204,7 @@ namespace spot
 			  for (unsigned n = start; n > 0;)
 			    {
 			      --n;
-			      formula e = c.nth(n);
+			      formula e = c[n];
 			      // {b;f} = b & X{f}
 			      // !{b;f} = !b | X!{f}
 			      if (e.is_boolean())
@@ -1222,10 +1222,10 @@ namespace spot
 		      // {b[*i..j];c} = b&X(b&X(... b&X{b[*0..j-i];c}))
 		      // !{b[*i..j];c} = !b&X(!b&X(... !b&X!{b[*0..j-i];c}))
 		      if (!opt_.reduce_size_strictly)
-			if (c.nth(0).is(op::Star))
+			if (c[0].is(op::Star))
 			  {
-			    formula s = c.nth(0);
-			    formula sc = s.nth(0);
+			    formula s = c[0];
+			    formula sc = s[0];
 			    unsigned min = s.min();
 			    if (sc.is_boolean() && min > 0)
 			      {
@@ -1237,7 +1237,7 @@ namespace spot
 				v.reserve(ss);
 				v.push_back(formula::Star(sc, 0, max));
 				for (unsigned n = 1; n < ss; ++n)
-				  v.push_back(c.nth(n));
+				  v.push_back(c[n]);
 				formula tail = formula::Concat(v);
 				tail = // {b[*0..j-i]} or !{b[*0..j-i]}
 				  formula::unop(o, tail);
@@ -1253,7 +1253,7 @@ namespace spot
 		  if (!opt_.reduce_size_strictly)
 		    if (c.is(op::Star))
 		      {
-			formula cs = c.nth(0);
+			formula cs = c[0];
 			if (cs.is_boolean())
 			  {
 			    unsigned min = c.min();
@@ -1292,7 +1292,7 @@ namespace spot
 		return f;
 	      case op::Star:
 		{
-		  formula h = f.nth(0);
+		  formula h = f[0];
 		  auto min = f.min();
 		  if (h.accepts_eword())
 		    min = 0;
@@ -1309,8 +1309,8 @@ namespace spot
 	formula reduce_sere_ltl(formula orig)
 	{
 	  op bindop = orig.kind();
-	  formula a = orig.nth(0);
-	  formula b = orig.nth(1);
+	  formula a = orig[0];
+	  formula b = orig[1];
 
 	  auto recurse = [this](formula f)
 	    {
@@ -1350,7 +1350,7 @@ namespace spot
 	      if (a == formula::one_star())
 		return recurse(formula::unop(op_g, b));
 
-	      formula s = a.nth(0);
+	      formula s = a[0];
 	      unsigned min = a.min();
 	      unsigned max = a.max();
 	      // {s[*]}[]->b = b W !s   if s is Boolean.
@@ -1384,13 +1384,13 @@ namespace spot
 	  else if (a.is(op::Concat))
 	    {
 	      unsigned s = a.size() - 1;
-	      formula last = a.nth(s);
+	      formula last = a[s];
 	      // {r;[*]}[]->b = {r}[]->Gb
 	      if (last == formula::one_star())
 		  return recurse(formula::binop(bindop, a.all_but(s),
 						formula::unop(op_g, b)));
 
-	      formula first = a.nth(0);
+	      formula first = a[0];
 	      // {[*];r}[]->b = G({r}[]->b)
 	      if (first == formula::one_star())
 		return recurse(formula::unop(op_g,
@@ -1403,13 +1403,13 @@ namespace spot
 	      // {r;s[*]}[]->b = {r}[]->(b & X(b W !s))
 	      // if s is Boolean and r does not accept [*0];
 	      if (last.is_Kleene_star()) // l = s[*]
-		if (last.nth(0).is_boolean())
+		if (last[0].is_boolean())
 		  {
 		    formula r = a.all_but(s);
 		    if (!r.accepts_eword())
 		      {
 			formula ns = // !s
-			  doneg ? formula::Not(last.nth(0)) : last.nth(0);
+			  doneg ? formula::Not(last[0]) : last[0];
 			formula w = // b W !s
 			  formula::binop(op_w, b, ns);
 			formula x = // X(b W !s)
@@ -1423,15 +1423,15 @@ namespace spot
 	      // {s[*];r}[]->b = !s R ({r}[]->b)
 	      // if s is Boolean and r does not accept [*0];
 	      if (first.is_Kleene_star())
-		if (first.nth(0).is_boolean())
+		if (first[0].is_boolean())
 		  {
 		    formula r = a.all_but(0);
 		    if (!r.accepts_eword())
 		      {
 			formula ns = // !s
 			  doneg
-			  ? formula::Not(first.nth(0))
-			  : first.nth(0);
+			  ? formula::Not(first[0])
+			  : first[0];
 			formula u = // {r}[]->b
 			  formula::binop(bindop, r, b);
 			// !s R ({r}[]->b)
@@ -1445,7 +1445,7 @@ namespace spot
 		{
 		  unsigned count = 0;
 		  for (unsigned n = 0; n <= s; ++n)
-		    count += !a.nth(n).accepts_eword();
+		    count += !a[n].accepts_eword();
 		  assert(count > 0);
 		  if (count == 1)
 		    return orig;
@@ -1464,7 +1464,7 @@ namespace spot
 		  // (i.e., r₂ before r₁.)
 		  vec r;
 		  do
-		    r.insert(r.begin(), a.nth(--pos));
+		    r.insert(r.begin(), a[--pos]);
 		  while (r.front().accepts_eword());
 		  formula tail = // {r₂}[]->b
 		    formula::binop(bindop, formula::Concat(r), b);
@@ -1472,14 +1472,14 @@ namespace spot
 		    {
 		      vec r;
 		      do
-			r.insert(r.begin(), a.nth(--pos));
+			r.insert(r.begin(), a[--pos]);
 		      while (r.front().accepts_eword());
 		      // If it's the last block, take all leading
 		      // formulae as well.
 		      if (count == 1)
 			while (pos > 0)
 			  {
-			    r.insert(r.begin(), a.nth(--pos));
+			    r.insert(r.begin(), a[--pos]);
 			    assert(r.front().accepts_eword());
 			  }
 
@@ -1503,7 +1503,7 @@ namespace spot
 	      do
 		{
 		  --s;
-		  tail = formula::binop(bindop, a.nth(s), tail);
+		  tail = formula::binop(bindop, a[s], tail);
 		}
 	      while (s != 0);
 	      return recurse(tail);
@@ -1515,7 +1515,7 @@ namespace spot
 	      vec v;
 	      for (unsigned n = 0; n < s; ++n)
 		// {r₁}[]->b
-		v.push_back(formula::binop(bindop, a.nth(n), b));
+		v.push_back(formula::binop(bindop, a[n], b));
 	      return recurse(formula::multop(op_and, v));
 	    }
 	  return orig;
@@ -1529,7 +1529,7 @@ namespace spot
 	      return simplify_recursively(f, c_);
 	    };
 	  op o = bo.kind();
-	  formula b = bo.nth(1);
+	  formula b = bo[1];
 	  if (opt_.event_univ)
 	    {
 	      trace << "bo: trying eventuniv rules" << std::endl;
@@ -1540,7 +1540,7 @@ namespace spot
 		return b;
 	    }
 
-	  formula a = bo.nth(0);
+	  formula a = bo[0];
 	  if (opt_.event_univ)
 	    {
 	      /* If a is a pure eventuality formula then a M b = a & b.
@@ -1650,27 +1650,27 @@ namespace spot
 		    return formula::F(b);
 		  // if a => b, then a U (b U c) = (b U c)
 		  // if a => b, then a U (b W c) = (b W c)
-		  if (b.is(op::U, op::W) && c_->implication(a, b.nth(0)))
+		  if (b.is(op::U, op::W) && c_->implication(a, b[0]))
 		    return b;
 		  // if b => a, then a U (b U c) = (a U c)
-		  if (b.is(op::U) && c_->implication(b.nth(0), a))
-		    return recurse(formula::U(a, b.nth(1)));
+		  if (b.is(op::U) && c_->implication(b[0], a))
+		    return recurse(formula::U(a, b[1]));
 		  // if a => c, then a U (b R (c U d)) = (b R (c U d))
 		  // if a => c, then a U (b R (c W d)) = (b R (c W d))
 		  // if a => c, then a U (b M (c U d)) = (b M (c U d))
 		  // if a => c, then a U (b M (c W d)) = (b M (c W d))
 		  if (b.is(op::R, op::M))
 		    {
-		      auto c1 = b.nth(1);
-		      if (c1.is(op::U, op::W) && c_->implication(a, c1.nth(0)))
+		      auto c1 = b[1];
+		      if (c1.is(op::U, op::W) && c_->implication(a, c1[0]))
 			return b;
 		    }
 		  // if a => b, then (a U c) U b = c U b
 		  // if a => b, then (a W c) U b = c U b
-		  if (a.is(op::U, op::W) && c_->implication(a.nth(0), b))
-		    return recurse(formula::U(a.nth(1), b));
+		  if (a.is(op::U, op::W) && c_->implication(a[0], b))
+		    return recurse(formula::U(a[1], b));
 		  // if c => b, then (a U c) U b = (a U c) | b
-		  if (a.is(op::U) && c_->implication(a.nth(1), b))
+		  if (a.is(op::U) && c_->implication(a[1], b))
 		    return recurse(formula::Or({a, b}));
 		  break;
 
@@ -1683,22 +1683,22 @@ namespace spot
 		    return recurse(formula::G(b));
 		  // if b => a, then a R (b R c) = b R c
 		  // if b => a, then a R (b M c) = b M c
-		  if (b.is(op::R, op::M) && c_->implication(b.nth(0), a))
+		  if (b.is(op::R, op::M) && c_->implication(b[0], a))
 		    return b;
 		  // if a => b, then a R (b R c) = a R c
-		  if (b.is(op::R) && c_->implication(a, b.nth(0)))
-		    return recurse(formula::R(a, b.nth(1)));
+		  if (b.is(op::R) && c_->implication(a, b[0]))
+		    return recurse(formula::R(a, b[1]));
 		  // if b => a, then (a R c) R b = c R b
 		  // if b => a, then (a M c) R b = c R b
 		  // if c => b, then (a R c) R b = (a & c) R b
 		  // if c => b, then (a M c) R b = (a & c) R b
 		  if (a.is(op::R, op::M))
 		    {
-		      if (c_->implication(b, a.nth(0)))
-			return recurse(formula::R(a.nth(1), b));
-		      if (c_->implication(a.nth(1), b))
+		      if (c_->implication(b, a[0]))
+			return recurse(formula::R(a[1], b));
+		      if (c_->implication(a[1], b))
 			{
-			  formula ac = formula::And({a.nth(0), a.nth(1)});
+			  formula ac = formula::And({a[0], a[1]});
 			  return recurse(formula::R(ac, b));
 			}
 		    }
@@ -1716,19 +1716,19 @@ namespace spot
 		    return formula::tt();
 		  // if a => b, then a W (b W c) = b W c
 		  // (Beware: even if a => b we do not have a W (b U c) = b U c)
-		  if (b.is(op::W) && c_->implication(a, b.nth(0)))
+		  if (b.is(op::W) && c_->implication(a, b[0]))
 		    return b;
 		  // if b => a, then a W (b U c) = a W c
 		  // if b => a, then a W (b W c) = a W c
-		  if (b.is(op::U, op::W) && c_->implication(b.nth(0), a))
-		    return recurse(formula::W(a, b.nth(1)));
+		  if (b.is(op::U, op::W) && c_->implication(b[0], a))
+		    return recurse(formula::W(a, b[1]));
 		  // if a => b, then (a U c) W b = c W b
 		  // if a => b, then (a W c) W b = c W b
-		  if (a.is(op::U, op::W) && c_->implication(a.nth(0), b))
-		    return recurse(formula::W(a.nth(1), b));
+		  if (a.is(op::U, op::W) && c_->implication(a[0], b))
+		    return recurse(formula::W(a[1], b));
 		  // if c => b, then (a W c) W b = (a W c) | b
 		  // if c => b, then (a U c) W b = (a U c) | b
-		  if (a.is(op::U, op::W) && c_->implication(a.nth(1), b))
+		  if (a.is(op::U, op::W) && c_->implication(a[1], b))
 		    return recurse(formula::Or({a, b}));
 		  break;
 
@@ -1740,20 +1740,20 @@ namespace spot
 		  if (c_->implication_neg(b, a, true))
 		    return formula::ff();
 		  // if b => a, then a M (b M c) = b M c
-		  if (b.is(op::M) && c_->implication(b.nth(0), a))
+		  if (b.is(op::M) && c_->implication(b[0], a))
 		    return b;
 		  // if a => b, then a M (b M c) = a M c
 		  // if a => b, then a M (b R c) = a M c
-		  if (b.is(op::M, op::R) && c_->implication(a, b.nth(0)))
-		    return recurse(formula::M(a, b.nth(1)));
+		  if (b.is(op::M, op::R) && c_->implication(a, b[0]))
+		    return recurse(formula::M(a, b[1]));
 		  // if b => a, then (a R c) M b = c M b
 		  // if b => a, then (a M c) M b = c M b
-		  if (a.is(op::R, op::M) && c_->implication(b, a.nth(0)))
-		    return recurse(formula::M(a.nth(1), b));
+		  if (a.is(op::R, op::M) && c_->implication(b, a[0]))
+		    return recurse(formula::M(a[1], b));
 		  // if c => b, then (a M c) M b = (a & c) M b
-		  if (a.is(op::M) && c_->implication(a.nth(1), b))
+		  if (a.is(op::M) && c_->implication(a[1], b))
 		    return
-		      recurse(formula::M(formula::And({a.nth(0), a.nth(1)}),
+		      recurse(formula::M(formula::And({a[0], a[1]}),
 					 b));
 		  break;
 
@@ -1792,28 +1792,28 @@ namespace spot
 	      // X(a) M X(b) = X(a M b)
 	      if (a.is(op::X) && b.is(op::X))
 		return recurse(formula::X(formula::binop(o,
-							 a.nth(0), b.nth(0))));
+							 a[0], b[0])));
 
 	      if (bo.is(op::U, op::W))
 		{
 		  // a U Ga = Ga
 		  // a W Ga = Ga
-		  if (b.is(op::G) && a == b.nth(0))
+		  if (b.is(op::G) && a == b[0])
 		    return b;
 		  // a U (b | c | G(a)) = a W (b | c)
 		  // a W (b | c | G(a)) = a W (b | c)
 		  if (b.is(op::Or))
 		    for (int i = 0, s = b.size(); i < s; ++i)
 		      {
-			formula c = b.nth(i);
-			if (c.is(op::G) && c.nth(0) == a)
+			formula c = b[i];
+			if (c.is(op::G) && c[0] == a)
 			  return recurse(formula::W(a, b.all_but(i)));
 		      }
 		  // a U (b & a & c) == (b & c) M a
 		  // a W (b & a & c) == (b & c) R a
 		  if (b.is(op::And))
 		    for (int i = 0, s = b.size(); i < s; ++i)
-		      if (b.nth(i) == a)
+		      if (b[i] == a)
 			return recurse(formula::binop(o == op::U ?
 						      op::M : op::R,
 						      b.all_but(i), a));
@@ -1825,7 +1825,7 @@ namespace spot
 		    {
 		      formula x = formula::X(formula::binop(o == op::U ?
 							    op::M : op::R,
-							    b, a.nth(0)));
+							    b, a[0]));
 		      return recurse(formula::Or({b, x}));
 		    }
 		}
@@ -1833,7 +1833,7 @@ namespace spot
 		{
 		  // a R Fa = Fa
 		  // a M Fa = Fa
-		  if (b.is(op::F) && b.nth(0) == a)
+		  if (b.is(op::F) && b[0] == a)
 		    return b;
 
 		  // a R (b & c & F(a)) = a M (b & c)
@@ -1841,15 +1841,15 @@ namespace spot
 		  if (b.is(op::And))
 		    for (int i = 0, s = b.size(); i < s; ++i)
 		      {
-			formula c = b.nth(i);
-			if (c.is(op::F) && c.nth(0) == a)
+			formula c = b[i];
+			if (c.is(op::F) && c[0] == a)
 			  return recurse(formula::M(a, b.all_but(i)));
 		      }
 		  // a M (b | a | c) == (b | c) U a
 		  // a R (b | a | c) == (b | c) W a
 		  if (b.is(op::Or))
 		    for (int i = 0, s = b.size(); i < s; ++i)
-		      if (b.nth(i) == a)
+		      if (b[i] == a)
 			return recurse(formula::binop(o == op::M ?
 						      op::U : op::W,
 						      b.all_but(i), a));
@@ -1861,7 +1861,7 @@ namespace spot
 		    {
 		      formula x =
 			formula::X(formula::binop(o == op::M ? op::U : op::W,
-						  b, a.nth(0)));
+						  b, a[0]));
 		      return recurse(formula::And({b, x}));
 		    }
 		}
@@ -1885,7 +1885,7 @@ namespace spot
 	      && mo.is(op::Or, op::And))
 	    for (unsigned i = 0; i < mos; ++i)
 	      {
-		formula fi = mo.nth(i);
+		formula fi = mo[i];
 		formula fo = mo.all_but(i);
 		// if fi => fo, then fi | fo = fo
 		// if fo => fi, then fi & fo = fo
@@ -1954,17 +1954,17 @@ namespace spot
 			    // - b | X(b M ...)
 			    if (formula barg = is_bXbRM(res[n]))
 			      {
-				wuset[barg.nth(1)].insert(n);
+				wuset[barg[1]].insert(n);
 				continue;
 			      }
 
 			    if (!res[n].is(op::X))
 			      continue;
 
-			    formula c = res[n].nth(0);
+			    formula c = res[n][0];
 			    auto handle_G = [&xgset](formula c)
 			      {
-				formula a2 = c.nth(0);
+				formula a2 = c[0];
 				if (a2.is(op::And))
 				  for (auto c: a2)
 				    xgset.insert(c);
@@ -2011,9 +2011,9 @@ namespace spot
 				    // a & (Xa W b) = b R a
 				    // a & (Xa U b) = b M a
 				    op t = wu.is(op::U) ? op::M : op::R;
-				    assert(wu.nth(0).is(op::X));
-				    formula a = wu.nth(0).nth(0);
-				    formula b = wu.nth(1);
+				    assert(wu[0].is(op::X));
+				    formula a = wu[0][0];
+				    formula b = wu[1];
 				    res[pos] = formula::binop(t, b, a);
 				  }
 				else
@@ -2109,7 +2109,7 @@ namespace spot
 				if (f.is(op::G))
 				  {
 				    seen_g = true;
-				    eu.push_back(f.nth(0));
+				    eu.push_back(f[0]);
 				  }
 				else
 				  {
@@ -2160,7 +2160,7 @@ namespace spot
 		    for (auto i = s.res_U_or_W->begin();
 			 i != s.res_U_or_W->end(); ++i)
 		      {
-			formula b = i->nth(1);
+			formula b = (*i)[1];
 			auto j = uwmap.find(b);
 			if (j == uwmap.end())
 			  {
@@ -2173,7 +2173,7 @@ namespace spot
 			op o = op::W;
 			if (i->is(op::U) || old.is(op::U))
 			  o = op::U;
-			formula fst_arg = formula::And({old.nth(0), i->nth(0)});
+			formula fst_arg = formula::And({old[0], (*i)[0]});
 			*j->second = formula::binop(o, fst_arg, b);
 			assert(j->second->is(o));
 			*i = nullptr;
@@ -2184,7 +2184,7 @@ namespace spot
 		    for (auto i = s.res_R_or_M->begin();
 			 i != s.res_R_or_M->end(); ++i)
 		      {
-			formula a = i->nth(0);
+			formula a = (*i)[0];
 			auto j = rmmap.find(a);
 			if (j == rmmap.end())
 			  {
@@ -2197,7 +2197,7 @@ namespace spot
 			op o = op::R;
 			if (i->is(op::M) || old.is(op::M))
 			  o = op::M;
-			formula snd_arg = formula::And({old.nth(1), i->nth(1)});
+			formula snd_arg = formula::And({old[1], (*i)[1]});
 			*j->second = formula::binop(o, a, snd_arg);
 			assert(j->second->is(o));
 			*i = nullptr;
@@ -2209,7 +2209,7 @@ namespace spot
 		    for (auto& f: *s.res_F)
 		      {
 			bool superfluous = false;
-			formula c = f.nth(0);
+			formula c = f[0];
 
 			fmap_t::iterator j = uwmap.find(c);
 			if (j != uwmap.end())
@@ -2218,7 +2218,7 @@ namespace spot
 			    formula bo = *j->second;
 			    if (bo.is(op::W))
 			      {
-				*j->second = formula::U(bo.nth(0), bo.nth(1));
+				*j->second = formula::U(bo[0], bo[1]);
 				assert(j->second->is(op::U));
 			      }
 			  }
@@ -2229,7 +2229,7 @@ namespace spot
 			    formula bo = *j->second;
 			    if (bo.is(op::R))
 			      {
-				*j->second = formula::M(bo.nth(0), bo.nth(1));
+				*j->second = formula::M(bo[0], bo[1]);
 				assert(j->second->is(op::M));
 			      }
 			  }
@@ -2303,7 +2303,7 @@ namespace spot
 			      //               = 0      otherwise
 			      if (f.min() > 1 || f.max() < 1)
 				return formula::ff();
-			      ares.push_back(f.nth(0));
+			      ares.push_back(f[0]);
 			      f = nullptr;
 			      break;
 			    case op::Fusion:
@@ -2325,7 +2325,7 @@ namespace spot
 				unsigned rs = f.size();
 				for (unsigned j = 0; j < rs; ++j)
 				  {
-				    formula jf = f.nth(j);
+				    formula jf = f[j];
 				    if (!jf.accepts_eword())
 				      {
 					ri = jf;
@@ -2380,7 +2380,7 @@ namespace spot
 			  continue;
 			if (!i.is(op::Concat, op::Fusion))
 			  continue;
-			formula h = i.nth(0);
+			formula h = i[0];
 			if (!h.is_boolean())
 			  continue;
 			if (i.is(op::Concat))
@@ -2423,7 +2423,7 @@ namespace spot
 			if (!i.is(op::Concat, op::Fusion))
 			  continue;
 			unsigned s = i.size() - 1;
-			formula t = i.nth(s);
+			formula t = i[s];
 			if (!t.is_boolean())
 			  continue;
 			if (i.is(op::Concat))
@@ -2498,18 +2498,18 @@ namespace spot
 			    // - b & X(b U ...)
 			    if (formula barg = is_bXbWU(res[n]))
 			      {
-				rmset[barg.nth(1)].insert(n);
+				rmset[barg[1]].insert(n);
 				continue;
 			      }
 
 			    if (!res[n].is(op::X))
 			      continue;
 
-			    formula c = res[n].nth(0);
+			    formula c = res[n][0];
 
 			    auto handle_F = [&xfset](formula c)
 			      {
-				formula a2 = c.nth(0);
+				formula a2 = c[0];
 				if (a2.is(op::Or))
 				  for (auto c: a2)
 				    xfset.insert(c);
@@ -2562,9 +2562,9 @@ namespace spot
 				    // a | (Xa R b) = b W a
 				    // a | (Xa M b) = b U a
 				    op t = rm.is(op::M) ? op::U : op::W;
-				    assert(rm.nth(0).is(op::X));
-				    formula a = rm.nth(0).nth(0);
-				    formula b = rm.nth(1);
+				    assert(rm[0].is(op::X));
+				    formula a = rm[0][0];
+				    formula b = rm[1];
 				    res[pos] = formula::binop(t, b, a);
 				  }
 				else
@@ -2699,7 +2699,7 @@ namespace spot
 			      if (f.is(op::F))
 				{
 				  seen_f = true;
-				  f = f.nth(0);
+				  f = f[0];
 				}
 			    if (seen_f)
 			      {
@@ -2745,7 +2745,7 @@ namespace spot
 		    for (auto i = s.res_U_or_W->begin();
 			 i != s.res_U_or_W->end(); ++i)
 		      {
-			formula a = i->nth(0);
+			formula a = (*i)[0];
 			auto j = uwmap.find(a);
 			if (j == uwmap.end())
 			  {
@@ -2758,7 +2758,7 @@ namespace spot
 			op o = op::U;
 			if (i->is(op::W) || old.is(op::W))
 			  o = op::W;
-			formula snd_arg = formula::Or({old.nth(1), i->nth(1)});
+			formula snd_arg = formula::Or({old[1], (*i)[1]});
 			*j->second = formula::binop(o, a, snd_arg);
 			assert(j->second->is(o));
 			*i = nullptr;
@@ -2769,7 +2769,7 @@ namespace spot
 		    for (auto i = s.res_R_or_M->begin();
 			 i != s.res_R_or_M->end(); ++i)
 		      {
-			formula b = i->nth(1);
+			formula b = (*i)[1];
 			auto j = rmmap.find(b);
 			if (j == rmmap.end())
 			  {
@@ -2782,7 +2782,7 @@ namespace spot
 			op o = op::M;
 			if (i->is(op::R) || old.is(op::R))
 			  o = op::R;
-			formula fst_arg = formula::Or({old.nth(0), i->nth(0)});
+			formula fst_arg = formula::Or({old[0], (*i)[0]});
 			*j->second = formula::binop(o, fst_arg, b);
 			assert(j->second->is(o));
 			*i = nullptr;
@@ -2794,7 +2794,7 @@ namespace spot
 		    for (auto& f: *s.res_G)
 		      {
 			bool superfluous = false;
-			formula c = f.nth(0);
+			formula c = f[0];
 
 			fmap_t::iterator j = uwmap.find(c);
 			if (j != uwmap.end())
@@ -2803,7 +2803,7 @@ namespace spot
 			    formula bo = *j->second;
 			    if (bo.is(op::U))
 			      {
-				*j->second = formula::W(bo.nth(0), bo.nth(1));
+				*j->second = formula::W(bo[0], bo[1]);
 				assert(j->second->is(op::W));
 			      }
 			  }
@@ -2814,7 +2814,7 @@ namespace spot
 			    formula bo = *j->second;
 			    if (bo.is(op::M))
 			      {
-				*j->second = formula::R(bo.nth(0), bo.nth(1));
+				*j->second = formula::R(bo[0], bo[1]);
 				assert(j->second->is(op::R));
 			      }
 			  }
@@ -2922,7 +2922,7 @@ namespace spot
 			  continue;
 			if (!i.is(op::Concat, op::Fusion))
 			  continue;
-			formula h = i.nth(0);
+			formula h = i[0];
 			if (!h.is_boolean())
 			  continue;
 			if (i.is(op::Concat))
@@ -3052,45 +3052,45 @@ namespace spot
 	switch (f.kind())
 	  {
 	  case op::X:
-	    if (g.is_eventual() && syntactic_implication(f.nth(0), g))
+	    if (g.is_eventual() && syntactic_implication(f[0], g))
 	      return true;
-	    if (g.is(op::X) && syntactic_implication(f.nth(0), g.nth(0)))
+	    if (g.is(op::X) && syntactic_implication(f[0], g[0]))
 	      return true;
 	    break;
 
 	  case op::F:
-	    if (g.is_eventual() && syntactic_implication(f.nth(0), g))
+	    if (g.is_eventual() && syntactic_implication(f[0], g))
 	      return true;
 	    break;
 
 	  case op::G:
-	    if (g.is(op::U, op::R) && syntactic_implication(f.nth(0), g.nth(1)))
+	    if (g.is(op::U, op::R) && syntactic_implication(f[0], g[1]))
 	      return true;
-	    if (g.is(op::W) && (syntactic_implication(f.nth(0), g.nth(0))
-				|| syntactic_implication(f.nth(0), g.nth(1))))
+	    if (g.is(op::W) && (syntactic_implication(f[0], g[0])
+				|| syntactic_implication(f[0], g[1])))
 	      return true;
-	    if (g.is(op::M) && (syntactic_implication(f.nth(0), g.nth(0))
-				&& syntactic_implication(f.nth(0), g.nth(1))))
+	    if (g.is(op::M) && (syntactic_implication(f[0], g[0])
+				&& syntactic_implication(f[0], g[1])))
 	      return true;
 	    // First column.
-	    if (syntactic_implication(f.nth(0), g))
+	    if (syntactic_implication(f[0], g))
 	      return true;
 	    break;
 
 	  case op::U:
 	    {
-	      formula f1 = f.nth(0);
-	      formula f2 = f.nth(1);
+	      formula f1 = f[0];
+	      formula f2 = f[1];
 	      if (g.is(op::U, op::W)
-		  && syntactic_implication(f1, g.nth(0))
-		  && syntactic_implication(f2, g.nth(1)))
+		  && syntactic_implication(f1, g[0])
+		  && syntactic_implication(f2, g[1]))
 		return true;
 	      if (g.is(op::M, op::R)
-		  && syntactic_implication(f1, g.nth(1))
-		  && syntactic_implication(f2, g.nth(0))
-		  && syntactic_implication(f2, g.nth(1)))
+		  && syntactic_implication(f1, g[1])
+		  && syntactic_implication(f2, g[0])
+		  && syntactic_implication(f2, g[1]))
 		return true;
-	      if (g.is(op::F) && syntactic_implication(f2, g.nth(0)))
+	      if (g.is(op::F) && syntactic_implication(f2, g[0]))
 		return true;
 	      // First column.
 	      if (syntactic_implication(f1, g) && syntactic_implication(f2, g))
@@ -3099,20 +3099,20 @@ namespace spot
 	    }
 	  case op::W:
 	    {
-	      formula f1 = f.nth(0);
-	      formula f2 = f.nth(1);
-	      if (g.is(op::U) && (syntactic_implication(f1, g.nth(1))
-				  && syntactic_implication(f2, g.nth(1))))
+	      formula f1 = f[0];
+	      formula f2 = f[1];
+	      if (g.is(op::U) && (syntactic_implication(f1, g[1])
+				  && syntactic_implication(f2, g[1])))
 		return true;
-	      if (g.is(op::W) && (syntactic_implication(f1, g.nth(0))
-				  && syntactic_implication(f2, g.nth(1))))
+	      if (g.is(op::W) && (syntactic_implication(f1, g[0])
+				  && syntactic_implication(f2, g[1])))
 		return true;
-	      if (g.is(op::R) && (syntactic_implication(f1, g.nth(1))
-				  && syntactic_implication(f2, g.nth(0))
-				  && syntactic_implication(f2, g.nth(1))))
+	      if (g.is(op::R) && (syntactic_implication(f1, g[1])
+				  && syntactic_implication(f2, g[0])
+				  && syntactic_implication(f2, g[1])))
 		return true;
-	      if (g.is(op::F) && (syntactic_implication(f1, g.nth(0))
-				  && syntactic_implication(f2, g.nth(0))))
+	      if (g.is(op::F) && (syntactic_implication(f1, g[0])
+				  && syntactic_implication(f2, g[0])))
 		return true;
 	      // First column.
 	      if (syntactic_implication(f1, g) && syntactic_implication(f2, g))
@@ -3121,18 +3121,18 @@ namespace spot
 	    }
 	  case op::R:
 	    {
-	      formula f1 = f.nth(0);
-	      formula f2 = f.nth(1);
-	      if (g.is(op::W) && (syntactic_implication(f1, g.nth(1))
-				  && syntactic_implication(f2, g.nth(0))))
+	      formula f1 = f[0];
+	      formula f2 = f[1];
+	      if (g.is(op::W) && (syntactic_implication(f1, g[1])
+				  && syntactic_implication(f2, g[0])))
 		return true;
-	      if (g.is(op::R) && (syntactic_implication(f1, g.nth(0))
-				  && syntactic_implication(f2, g.nth(1))))
+	      if (g.is(op::R) && (syntactic_implication(f1, g[0])
+				  && syntactic_implication(f2, g[1])))
 		return true;
-	      if (g.is(op::M) && (syntactic_implication(f2, g.nth(0))
-				  && syntactic_implication(f2, g.nth(1))))
+	      if (g.is(op::M) && (syntactic_implication(f2, g[0])
+				  && syntactic_implication(f2, g[1])))
 		return true;
-	      if (g.is(op::F) && syntactic_implication(f2, g.nth(0)))
+	      if (g.is(op::F) && syntactic_implication(f2, g[0]))
 		return true;
 	      // First column.
 	      if (syntactic_implication(f2, g))
@@ -3141,18 +3141,18 @@ namespace spot
 	    }
 	  case op::M:
 	    {
-	      formula f1 = f.nth(0);
-	      formula f2 = f.nth(1);
-	      if (g.is(op::U, op::W) && (syntactic_implication(f1, g.nth(1))
+	      formula f1 = f[0];
+	      formula f2 = f[1];
+	      if (g.is(op::U, op::W) && (syntactic_implication(f1, g[1])
 					 && syntactic_implication(f2,
-								  g.nth(0))))
+								  g[0])))
 		return true;
-	      if (g.is(op::R, op::M) && (syntactic_implication(f1, g.nth(0))
+	      if (g.is(op::R, op::M) && (syntactic_implication(f1, g[0])
 					 && syntactic_implication(f2,
-								  g.nth(1))))
+								  g[1])))
 		return true;
-	      if (g.is(op::F) && (syntactic_implication(f1, g.nth(0))
-				  || syntactic_implication(f2, g.nth(0))))
+	      if (g.is(op::F) && (syntactic_implication(f1, g[0])
+				  || syntactic_implication(f2, g[0])))
 		return true;
 	      // First column.
 	      if (syntactic_implication(f2, g))
@@ -3173,7 +3173,7 @@ namespace spot
 	      bool b = true;
 	      unsigned fs = f.size();
 	      for (; i < fs; ++i)
-		if (!syntactic_implication(f.nth(i), g))
+		if (!syntactic_implication(f[i], g))
 		  {
 		    b = false;
 		    break;
@@ -3195,7 +3195,7 @@ namespace spot
 		  return true;
 	      unsigned fs = f.size();
 	      for (; i < fs; ++i)
-		if (syntactic_implication(f.nth(i), g))
+		if (syntactic_implication(f[i], g))
 		  return true;
 	      break;
 	    }
@@ -3208,26 +3208,26 @@ namespace spot
 	switch (g.kind())
 	  {
 	  case op::F:
-	    if (syntactic_implication(f, g.nth(0)))
+	    if (syntactic_implication(f, g[0]))
 	      return true;
 	    break;
 
 	  case op::G:
 	  case op::X:
-	    if (f.is_universal() && syntactic_implication(f, g.nth(0)))
+	    if (f.is_universal() && syntactic_implication(f, g[0]))
 	      return true;
 	    break;
 
 	  case op::U:
 	  case op::W:
-	    if (syntactic_implication(f, g.nth(1)))
+	    if (syntactic_implication(f, g[1]))
 	      return true;
 	    break;
 
 	  case op::M:
 	  case op::R:
-	    if (syntactic_implication(f, g.nth(0))
-		&& syntactic_implication(f, g.nth(1)))
+	    if (syntactic_implication(f, g[0])
+		&& syntactic_implication(f, g[1]))
 	      return true;
 	    break;
 
@@ -3245,7 +3245,7 @@ namespace spot
 	      bool b = true;
 	      unsigned gs = g.size();
 	      for (; i < gs; ++i)
-		if (!syntactic_implication(f, g.nth(i)))
+		if (!syntactic_implication(f, g[i]))
 		  {
 		    b = false;
 		    break;
@@ -3268,7 +3268,7 @@ namespace spot
 		  return true;
 	      unsigned gs = g.size();
 	      for (; i < gs; ++i)
-		if (syntactic_implication(f, g.nth(i)))
+		if (syntactic_implication(f, g[i]))
 		  return true;
 	      break;
 	    }
diff --git a/src/ltlvisit/snf.cc b/src/ltlvisit/snf.cc
index b4fe0539a..b563d9174 100644
--- a/src/ltlvisit/snf.cc
+++ b/src/ltlvisit/snf.cc
@@ -56,9 +56,9 @@ namespace spot
 	      break;
 	    case op::Star:
 	      if (!bounded)
-		out = visit(f.nth(0)); // Strip the star.
+		out = visit(f[0]); // Strip the star.
 	      else
-		out = formula::Star(visit(f.nth(0)),
+		out = formula::Star(visit(f[0]),
 				    std::max(unsigned(f.min()), 1U), f.max());
 	      break;
 	    case op::Concat:
@@ -91,7 +91,7 @@ namespace spot
 		std::vector<formula> v;
 		v.reserve(s);
 		for (unsigned pos = 0; pos < s; ++pos)
-		  v.emplace_back(visit(f.nth(pos)));
+		  v.emplace_back(visit(f[pos]));
 		out = formula::OrRat(v);
 		break;
 	      }
diff --git a/src/ltlvisit/unabbrev.cc b/src/ltlvisit/unabbrev.cc
index 0b1ec74d1..51ad9a519 100644
--- a/src/ltlvisit/unabbrev.cc
+++ b/src/ltlvisit/unabbrev.cc
@@ -119,7 +119,7 @@ namespace spot
 	    //  F f = true U f
 	    if (!re_f_)
 	      break;
-	    out = formula::U(formula::tt(), out.nth(0));
+	    out = formula::U(formula::tt(), out[0]);
 	    break;
 	  case op::G:
 	    //  G f = false R f
@@ -130,16 +130,16 @@ namespace spot
 	      break;
 	    if (!re_r_)
 	      {
-		out = formula::R(formula::ff(), out.nth(0));
+		out = formula::R(formula::ff(), out[0]);
 		break;
 	      }
 	    if (!re_w_)
 	      {
-		out = formula::W(out.nth(0), formula::ff());
+		out = formula::W(out[0], formula::ff());
 		break;
 	      }
 	    {
-	      auto nc = formula::Not(out.nth(0));
+	      auto nc = formula::Not(out[0]);
 	      if (!re_f_)
 		{
 		  out = formula::Not(formula::F(nc));
@@ -154,8 +154,8 @@ namespace spot
 	    if (!re_xor_)
 	      break;
 	    {
-	      auto f1 = out.nth(0);
-	      auto f2 = out.nth(1);
+	      auto f1 = out[0];
+	      auto f2 = out[1];
 	      if (!re_e_)
 		{
 		  out = formula::Not(formula::Equiv(f1, f2));
@@ -172,15 +172,15 @@ namespace spot
 	    // f1 => f2  ==  !f1 | f2
 	    if (!re_i_)
 	      break;
-	    out = formula::Or({formula::Not(out.nth(0)), out.nth(1)});
+	    out = formula::Or({formula::Not(out[0]), out[1]});
 	    break;
 	  case op::Equiv:
 	    // f1 <=> f2  ==  (f1 & f2) | (!f1 & !f2)
 	    if (!re_e_)
 	      break;
 	    {
-	      auto f1 = out.nth(0);
-	      auto f2 = out.nth(1);
+	      auto f1 = out[0];
+	      auto f2 = out[1];
 	      auto nf1 = formula::Not(f1);
 	      auto nf2 = formula::Not(f2);
 	      auto term1 = formula::And({f1, f2});
@@ -196,8 +196,8 @@ namespace spot
 	    if (!re_r_)
 	      break;
 	    {
-	      auto f1 = out.nth(0);
-	      auto f2 = out.nth(1);
+	      auto f1 = out[0];
+	      auto f2 = out[1];
 	      auto f12 = formula::And({f1, f2});
 	      if (!re_w_)
 		{
@@ -218,8 +218,8 @@ namespace spot
 	    if (!re_w_)
 	      break;
 	    {
-	      auto f1 = out.nth(0);
-	      auto f2 = out.nth(1);
+	      auto f1 = out[0];
+	      auto f2 = out[1];
 	      if (!re_r_)
 		{
 		  out = formula::R(f2, formula::Or({f2, f1}));
@@ -236,8 +236,8 @@ namespace spot
 	    if (!re_m_)
 	      break;
 	    {
-	      auto f2 = out.nth(1);
-	      out = formula::U(f2, formula::And({f2, out.nth(0)}));
+	      auto f2 = out[1];
+	      out = formula::U(f2, formula::And({f2, out[0]}));
 	      break;
 	    }
 	}
diff --git a/src/twa/formula2bdd.cc b/src/twa/formula2bdd.cc
index 414f708ad..86fc439fe 100644
--- a/src/twa/formula2bdd.cc
+++ b/src/twa/formula2bdd.cc
@@ -101,13 +101,13 @@ namespace spot
       case op::AP:
 	return bdd_ithvar(d->register_proposition(f, owner));
       case op::Not:
-	return bdd_not(recurse(f.nth(0)));
+	return bdd_not(recurse(f[0]));
       case op::Xor:
-	return bdd_apply(recurse(f.nth(0)), recurse(f.nth(1)), bddop_xor);
+	return bdd_apply(recurse(f[0]), recurse(f[1]), bddop_xor);
       case op::Implies:
-	return bdd_apply(recurse(f.nth(0)), recurse(f.nth(1)), bddop_imp);
+	return bdd_apply(recurse(f[0]), recurse(f[1]), bddop_imp);
       case op::Equiv:
-	return bdd_apply(recurse(f.nth(0)), recurse(f.nth(1)), bddop_biimp);
+	return bdd_apply(recurse(f[0]), recurse(f[1]), bddop_biimp);
       case op::And:
       case op::Or:
 	{
@@ -120,7 +120,7 @@ namespace spot
 	    }
 	  unsigned s = f.size();
 	  for (unsigned n = 0; n < s; ++n)
-	    res = bdd_apply(res, recurse(f.nth(n)), op);
+	    res = bdd_apply(res, recurse(f[n]), op);
 	  return res;
 	}
       }
diff --git a/src/twaalgos/compsusp.cc b/src/twaalgos/compsusp.cc
index f5e1e1043..e0a8c24cb 100644
--- a/src/twaalgos/compsusp.cc
+++ b/src/twaalgos/compsusp.cc
@@ -64,7 +64,7 @@ namespace spot
 	      unsigned mos = f.size();
 	      for (unsigned i = 0; i < mos; ++i)
 		{
-		  ltl::formula c = f.nth(i);
+		  ltl::formula c = f[i];
 		  if (c.is_boolean())
 		    res.push_back(c);
 		  else if (oblig_ && c.is_syntactic_obligation())
@@ -91,7 +91,7 @@ namespace spot
 		    {
 		      // res || susp -> (res && G![susp]) || G[susp])
 		      auto r = ltl::formula::multop(op, res);
-		      auto gn = ltl::formula::G(ltl::formula::Not(g.nth(0)));
+		      auto gn = ltl::formula::G(ltl::formula::Not(g[0]));
 		      return ltl::formula::Or({ltl::formula::And({r, gn}), g});
 		    }
 		}
diff --git a/src/twaalgos/ltl2taa.cc b/src/twaalgos/ltl2taa.cc
index 7fe956b3b..1285c66a2 100644
--- a/src/twaalgos/ltl2taa.cc
+++ b/src/twaalgos/ltl2taa.cc
@@ -86,7 +86,7 @@ namespace spot
 	    }
 	  case op::X:
 	    {
-	      ltl2taa_visitor v = recurse(f.nth(0));
+	      ltl2taa_visitor v = recurse(f[0]);
 	      std::vector<formula> dst;
 	      std::vector<formula> a;
 	      if (v.succ_.empty()) // Handle X(0)
@@ -104,7 +104,7 @@ namespace spot
 	  case op::Not:
 	    {
 	      negated_ = true;
-	      ltl2taa_visitor v = recurse(f.nth(0));
+	      ltl2taa_visitor v = recurse(f[0]);
 	      // Done in recurse
 	      succ_ = v.succ_;
 	      return;
@@ -143,8 +143,8 @@ namespace spot
       void
       visit_binop(formula f)
       {
-	ltl2taa_visitor v1 = recurse(f.nth(0));
-	ltl2taa_visitor v2 = recurse(f.nth(1));
+	ltl2taa_visitor v1 = recurse(f[0]);
+	ltl2taa_visitor v2 = recurse(f[1]);
 
 	std::vector<succ_state>::iterator i1;
 	std::vector<succ_state>::iterator i2;
@@ -159,7 +159,7 @@ namespace spot
 	  // fall thru
 	case op::W:
 	  if (refined_)
-	    contained = lcc_->contained(f.nth(0), f.nth(1));
+	    contained = lcc_->contained(f[0], f[1]);
 	  for (i1 = v1.succ_.begin(); i1 != v1.succ_.end(); ++i1)
 	    {
 	      // Refined rule
@@ -169,11 +169,11 @@ namespace spot
 
 	      i1->Q.push_back(init_); // Add the initial state
 	      if (strong)
-		i1->acc.push_back(f.nth(1));
+		i1->acc.push_back(f[1]);
 	      t = res_->create_transition(init_, i1->Q);
 	      res_->add_condition(t, i1->condition);
 	      if (strong)
-		res_->add_acceptance_condition(t, f.nth(1));
+		res_->add_acceptance_condition(t, f[1]);
 	      else
 		for (unsigned i = 0; i < i1->acc.size(); ++i)
 		  res_->add_acceptance_condition(t, i1->acc[i]);
@@ -190,7 +190,7 @@ namespace spot
 	  strong = true;
 	case op::R: // Weak Release
 	  if (refined_)
-	    contained = lcc_->contained(f.nth(0), f.nth(1));
+	    contained = lcc_->contained(f[0], f[1]);
 
 	  for (i2 = v2.succ_.begin(); i2 != v2.succ_.end(); ++i2)
 	    {
@@ -222,8 +222,8 @@ namespace spot
 
 	      if (strong)
 		{
-		  i2->acc.push_back(f.nth(0));
-		  res_->add_acceptance_condition(t, f.nth(0));
+		  i2->acc.push_back(f[0]);
+		  res_->add_acceptance_condition(t, f[0]);
 		}
 	      else if (refined_)
 		for (unsigned i = 0; i < i2->acc.size(); ++i)
@@ -244,7 +244,7 @@ namespace spot
 	std::vector<ltl2taa_visitor> vs;
 	for (unsigned n = 0, s = f.size(); n < s; ++n)
 	{
-	  vs.push_back(recurse(f.nth(n)));
+	  vs.push_back(recurse(f[n]));
 	  if (vs[n].succ_.empty()) // Handle 0
 	    ok = false;
 	}
diff --git a/src/twaalgos/ltl2tgba_fm.cc b/src/twaalgos/ltl2tgba_fm.cc
index a5147d691..fbf706bdc 100644
--- a/src/twaalgos/ltl2tgba_fm.cc
+++ b/src/twaalgos/ltl2tgba_fm.cc
@@ -69,28 +69,28 @@ namespace spot
       unsigned s = f.size();
       for (unsigned n = 0; n < s; ++n)
 	{
-	  formula sub = f.nth(n);
+	  formula sub = f[n];
 	  // Recurring is set if we are under "G(...)" or "0 R (...)"
 	  // or (...) W 0".
 	  if (recurring)
 	    rec.insert(sub);
 	  if (sub.is(op::G))
 	    {
-	      implied_subformulae(sub.nth(0), rec, true);
+	      implied_subformulae(sub[0], rec, true);
 	    }
 	  else if (sub.is(op::W))
 	    {
 	      // f W 0 = Gf
-	      if (sub.nth(1).is_false())
-		implied_subformulae(sub.nth(0), rec, true);
+	      if (sub[1].is_false())
+		implied_subformulae(sub[0], rec, true);
 	    }
 	  else
 	    while (sub.is(op::R, op::M))
 	      {
 		// in 'f R g' and 'f M g' always evaluate 'g'.
 		formula b = sub;
-		sub = b.nth(1);
-		if (b.nth(0).is_false())
+		sub = b[1];
+		if (b[0].is_false())
 		  {
 		    assert(b.is(op::R)); // because 0 M g = 0
 		    // 0 R f = Gf
@@ -305,12 +305,12 @@ namespace spot
 	    if (f.is(op::U))
 	      {
 		// P(a U b) = P(b)
-		f = f.nth(1);
+		f = f[1];
 	      }
 	    else if (f.is(op::M))
 	      {
 		// P(a M b) = P(a & b)
-		formula g = formula::And({f.nth(0), f.nth(1)});
+		formula g = formula::And({f[0], f[1]});
 		int num = dict->register_acceptance_variable(g, this);
 		a_set &= bdd_ithvar(num);
 
@@ -322,7 +322,7 @@ namespace spot
 	    else if (f.is(op::F))
 	      {
 		// P(F(a)) = P(a)
-		f = f.nth(0);
+		f = f[0];
 	      }
 	    else
 	      {
@@ -596,7 +596,7 @@ namespace spot
 	    {
 	      // Not can only appear in front of Boolean
 	      // expressions.
-	      formula g = f.nth(0);
+	      formula g = f[0];
 	      assert(g.is_boolean());
 	      return (!recurse(g)) & next_to_concat();
 	    }
@@ -619,7 +619,7 @@ namespace spot
 	      unsigned min2 = (min == 0) ? 0 : (min - 1);
 	      unsigned max2 =
 		max == formula::unbounded() ? formula::unbounded() : (max - 1);
-	      f = formula::bunop(o, f.nth(0), min2, max2);
+	      f = formula::bunop(o, f[0], min2, max2);
 
 	      // If we have something to append, we can actually append it
 	      // to f.  This is correct even in the case of FStar, as f
@@ -629,13 +629,13 @@ namespace spot
 
 	      if (o == op::Star)
 		{
-		  if (!bo.nth(0).accepts_eword())
+		  if (!bo[0].accepts_eword())
 		    {
 		      //   f*;g  ->  f;f*;g | g
 		      //
 		      // If f does not accept the empty word, we can easily
 		      // add "f*;g" as to_concat_ when translating f.
-		      bdd res = recurse(bo.nth(0), f);
+		      bdd res = recurse(bo[0], f);
 		      if (min == 0)
 			res |= now_to_concat();
 		      return res;
@@ -651,7 +651,7 @@ namespace spot
 		      //  1. translate f,
 		      //  2. append f*;g to all destinations
 		      //  3. add |g
-		      bdd res = recurse(bo.nth(0));
+		      bdd res = recurse(bo[0]);
 		      //   f*;g  ->  f;f*;g
 		      minato_isop isop(res);
 		      bdd cube;
@@ -682,7 +682,7 @@ namespace spot
 		  bdd tail_bdd;
 		  bool tail_computed = false;
 
-		  minato_isop isop(recurse(bo.nth(0)));
+		  minato_isop isop(recurse(bo[0]));
 		  bdd cube;
 		  bdd res = bddfalse;
 		  if (min == 0)
@@ -779,7 +779,7 @@ namespace spot
 		  vec conj;
 		  for (unsigned m = 0; m < s; ++m)
 		    {
-		      formula g = f.nth(m);
+		      formula g = f[m];
 		      if (n != m)
 			g = formula::Concat({g, star});
 		      conj.push_back(g);
@@ -815,17 +815,17 @@ namespace spot
 	      unsigned s = f.size();
 	      v.reserve(s);
 	      for (unsigned n = 1; n < s; ++n)
-		v.push_back(f.nth(n));
+		v.push_back(f[n]);
 	      if (to_concat_)
 		v.push_back(to_concat_);
-	      return recurse(f.nth(0), formula::Concat(std::move(v)));
+	      return recurse(f[0], formula::Concat(std::move(v)));
 	    }
 	  case op::Fusion:
 	    {
 	      assert(f.size() >= 2);
 
 	      // the head
-	      bdd res = recurse(f.nth(0));
+	      bdd res = recurse(f[0]);
 
 	      // the tail
 	      formula tail = f.all_but(0);
@@ -1129,7 +1129,7 @@ namespace spot
 	    {
 	      // r(Fy) = r(y) + a(y)X(Fy)   if not recurring
 	      // r(Fy) = r(y) + a(y)        if recurring (see comment in G)
-	      formula child = node.nth(0);
+	      formula child = node[0];
 	      bdd y = recurse(child);
 	      bdd a = bdd_ithvar(dict_.register_a_variable(child));
 	      if (!recurring_)
@@ -1172,13 +1172,13 @@ namespace spot
 
 	      // r(Gy) = r(y)X(Gy)
 	      int x = dict_.register_next_variable(node);
-	      bdd y = recurse(node.nth(0), /* recurring = */ true);
+	      bdd y = recurse(node[0], /* recurring = */ true);
 	      return y & bdd_ithvar(x);
 	    }
 	  case op::Not:
 	    {
 	      // r(!y) = !r(y)
-	      return bdd_not(recurse(node.nth(0)));
+	      return bdd_not(recurse(node[0]));
 	    }
 	  case op::X:
 	    {
@@ -1201,7 +1201,7 @@ namespace spot
 	      // effect is less clear.  Benchmarks show that it
 	      // reduces the number of states and transitions, but it
 	      // increases the number of non-deterministic states...
-	      formula y = node.nth(0);
+	      formula y = node[0];
 	      bdd res;
 	      if (y.is(op::And))
 		{
@@ -1226,7 +1226,7 @@ namespace spot
 	  case op::Closure:
 	    {
 	      // rat_seen_ = true;
-	      formula f = node.nth(0);
+	      formula f = node[0];
 	      auto p = dict_.transdfa.succ(f);
 	      bdd res = bddfalse;
 	      auto aut = std::get<0>(p);
@@ -1267,7 +1267,7 @@ namespace spot
 		  has_marked_ = true;
 		}
 
-	      formula f = node.nth(0);
+	      formula f = node[0];
 	      auto p = dict_.transdfa.succ(f);
 	      auto aut = std::get<0>(p);
 
@@ -1316,15 +1316,15 @@ namespace spot
 	    SPOT_UNREACHABLE();
 	  case op::U:
 	    {
-	      bdd f1 = recurse(node.nth(0));
-	      bdd f2 = recurse(node.nth(1));
+	      bdd f1 = recurse(node[0]);
+	      bdd f2 = recurse(node[1]);
 	      // r(f1 U f2) = r(f2) + a(f2)r(f1)X(f1 U f2) if not recurring
 	      // r(f1 U f2) = r(f2) + a(f2)r(f1)           if recurring
-	      f1 &= bdd_ithvar(dict_.register_a_variable(node.nth(1)));
+	      f1 &= bdd_ithvar(dict_.register_a_variable(node[1]));
 	      if (!recurring_)
 		f1 &= bdd_ithvar(dict_.register_next_variable(node));
 	      if (dict_.unambiguous)
-		f1 &= neg_of(node.nth(1));
+		f1 &= neg_of(node[1]);
 	      return f2 | f1;
 	    }
 	  case op::W:
@@ -1333,36 +1333,36 @@ namespace spot
 	      // r(f1 W f2) = r(f2) + r(f1)           if recurring
 	      //
 	      // also f1 W 0 = G(f1), so we can enable recurring on f1
-	      bdd f1 = recurse(node.nth(0), node.nth(1).is_false());
-	      bdd f2 = recurse(node.nth(1));
+	      bdd f1 = recurse(node[0], node[1].is_false());
+	      bdd f2 = recurse(node[1]);
 	      if (!recurring_)
 		f1 &= bdd_ithvar(dict_.register_next_variable(node));
 	      if (dict_.unambiguous)
-		f1 &= neg_of(node.nth(1));
+		f1 &= neg_of(node[1]);
 	      return f2 | f1;
 	    }
 	  case op::R:
 	    {
 	      // r(f2) is in factor, so we can propagate the recurring_ flag.
 	      // if f1=false, we can also turn it on (0 R f = Gf).
-	      bdd res = recurse(node.nth(1),
-				recurring_ || node.nth(0).is_false());
+	      bdd res = recurse(node[1],
+				recurring_ || node[0].is_false());
 	      // r(f1 R f2) = r(f2)(r(f1) + X(f1 R f2))  if not recurring
 	      // r(f1 R f2) = r(f2)                      if recurring
 	      if (recurring_ && !dict_.unambiguous)
 		return res;
-	      bdd f1 = recurse(node.nth(0));
+	      bdd f1 = recurse(node[0]);
 	      bdd f2 = bddtrue;
 	      if (!recurring_)
 		f2 = bdd_ithvar(dict_.register_next_variable(node));
 	      if (dict_.unambiguous)
-		f2 &= neg_of(node.nth(0));
+		f2 &= neg_of(node[0]);
 	      return res & (f1 | f2);
 	    }
 	  case op::M:
 	    {
-	      bdd res = recurse(node.nth(1), recurring_);
-	      bdd f1 = recurse(node.nth(0));
+	      bdd res = recurse(node[1], recurring_);
+	      bdd f1 = recurse(node[0]);
 	      // r(f1 M f2) = r(f2)(r(f1) + a(f1&f2)X(f1 M f2)) if not recurring
 	      // r(f1 M f2) = r(f2)(r(f1) + a(f1&f2))           if recurring
 	      //
@@ -1383,7 +1383,7 @@ namespace spot
 	      if (!recurring_)
 		a &= bdd_ithvar(dict_.register_next_variable(node));
 	      if (dict_.unambiguous)
-		a &= neg_of(node.nth(0));
+		a &= neg_of(node[0]);
 	      return res & (f1 | a);
 	    }
 	  case op::EConcatMarked:
@@ -1394,8 +1394,8 @@ namespace spot
 	    {
 	      // Recognize f2 on transitions going to destinations
 	      // that accept the empty word.
-	      bdd f2 = recurse(node.nth(1));
-	      bdd f1 = translate_ratexp(node.nth(0), dict_);
+	      bdd f2 = recurse(node[1]);
+	      bdd f1 = translate_ratexp(node[0], dict_);
 	      bdd res = bddfalse;
 
 	      if (mark_all_)
@@ -1417,7 +1417,7 @@ namespace spot
 			dict_.bdd_to_sere(bdd_exist(f1 & label,
 						    dict_.var_set));
 
-		      formula dest2 = formula::binop(o, dest, node.nth(1));
+		      formula dest2 = formula::binop(o, dest, node[1]);
 		      bool unamb = dict_.unambiguous;
 		      if (!dest2.is(op::False))
 			{
@@ -1426,13 +1426,13 @@ namespace spot
 			  // deterministic automaton at no additional
 			  // cost.  You can test this on
 			  //   G({{1;1}*}<>->a)
-			  if (node.nth(1).is_boolean())
+			  if (node[1].is_boolean())
 			    unamb = true;
 
 			  bdd toadd = label &
 			    bdd_ithvar(dict_.register_next_variable(dest2));
 			  if (dest.accepts_eword() && unamb)
-			    toadd &= neg_of(node.nth(1));
+			    toadd &= neg_of(node[1]);
 			  res |= toadd;
 			}
 		      if (dest.accepts_eword())
@@ -1462,7 +1462,7 @@ namespace spot
 			}
 		      else
 			{
-			  formula dest2 = formula::binop(o, dest, node.nth(1));
+			  formula dest2 = formula::binop(o, dest, node[1]);
 			  if (!dest2.is(op::False))
 			    res |= label &
 			      bdd_ithvar(dict_.register_next_variable(dest2));
@@ -1483,8 +1483,8 @@ namespace spot
 	      // interpretation of first() as a universal automaton,
 	      // and using implication to encode it)  was explained
 	      // to me (adl) by Felix Klaedtke.
-	      bdd f2 = recurse(node.nth(1));
-	      bdd f1 = translate_ratexp(node.nth(0), dict_);
+	      bdd f2 = recurse(node[1]);
+	      bdd f1 = translate_ratexp(node[0], dict_);
 
 	      if (exprop_)
 		{
@@ -1500,7 +1500,7 @@ namespace spot
 		      formula dest =
 			dict_.bdd_to_sere(bdd_exist(f1 & label, dict_.var_set));
 
-		      formula dest2 = formula::binop(o, dest, node.nth(1));
+		      formula dest2 = formula::binop(o, dest, node[1]);
 
 		      bdd udest =
 			bdd_ithvar(dict_.register_next_variable(dest2));
@@ -1526,7 +1526,7 @@ namespace spot
 		      bdd label = bdd_exist(cube, dict_.next_set);
 		      bdd dest_bdd = bdd_existcomp(cube, dict_.next_set);
 		      formula dest = dict_.conj_bdd_to_sere(dest_bdd);
-		      formula dest2 = formula::binop(o, dest, node.nth(1));
+		      formula dest2 = formula::binop(o, dest, node[1]);
 
 		      bdd udest =
 			bdd_ithvar(dict_.register_next_variable(dest2));
@@ -1930,10 +1930,10 @@ namespace spot
 		  {
 		    if (f.is(op::F))
 		      all_promises &=
-			bdd_ithvar(d.register_a_variable(f.nth(0)));
+			bdd_ithvar(d.register_a_variable(f[0]));
 		    else if (f.is(op::U))
 		      all_promises &=
-			bdd_ithvar(d.register_a_variable(f.nth(1)));
+			bdd_ithvar(d.register_a_variable(f[1]));
 		    else if (f.is(op::M))
 		      all_promises &=
 			bdd_ithvar(d.register_a_variable(f));
diff --git a/wrap/python/spot_impl.i b/wrap/python/spot_impl.i
index a85fbfe7d..ec47c9499 100644
--- a/wrap/python/spot_impl.i
+++ b/wrap/python/spot_impl.i
@@ -310,7 +310,7 @@ namespace std {
   int __cmp__(spot::ltl::formula b) { return self->id() - b.id(); }
   size_t __hash__() { return self->id(); }
   unsigned __len__() { return self->size(); }
-  formula __getitem__(unsigned pos) { return self->nth(pos); }
+  formula __getitem__(unsigned pos) { return (*self)[pos]; }
 
   std::string __repr__() { return spot::ltl::str_psl(*self); }
   std::string _repr_latex_()