In mathematics, more specifically in computational algebra, a straight-line program (SLP) for a finite group G = 〈S〉 is a finite sequence L of elements of G such that every element of L either belongs to S, is the inverse of a preceding element, or the product of two preceding elements. An SLP L is said to compute a group element g ∈ G if g ∈ L, where g is encoded by a word in S and its inverses. Claim 1 — If i < s then |K(i+1)| = 2|K(i)|.It is immediate that |K(i+1)| ≤ 2|K(i)|. Now suppose for a contradiction that |K(i+1)| < 2|K(i)|. By the pigeonhole principle there are k1,k2 ∈ K(i+1) with k1 = z1α1·z2α2·…·zi+1αi+1 = z1β1·z2β2·…·zi+1βi+1 = k2 for some αj,βj ∈ {0,1}. Let r be the largest integer such that αr ≠ βr. Assume WLOG that αr = 1. It follows that zr = zp−αp·zp-1−αp-1·…·z1−α1·z1β1·z2β2·…·zqβq, with p,q < r. Hence zr ∈ K(r−1)−1K(r − 1), a contradiction.Claim 2 — c(i) ≤ i 2 − i.Since c(0)=0 it suffices to show that c(i+1) - c(i) ≤ 2i. The Cayley graph of G is connected and if i < s, K(i)−1K(i) ≠ G, then there is an element of the form g1·g2 ∈ G K(i)−1K(i) with g1 ∈ K(i)−1K(i) and g2 ∈ S. In mathematics, more specifically in computational algebra, a straight-line program (SLP) for a finite group G = 〈S〉 is a finite sequence L of elements of G such that every element of L either belongs to S, is the inverse of a preceding element, or the product of two preceding elements. An SLP L is said to compute a group element g ∈ G if g ∈ L, where g is encoded by a word in S and its inverses. Intuitively, an SLP computing some g ∈ G is an efficient way of storing g as a group word over S; observe that if g is constructed in i steps, the word length of g may be exponential in i, but the length of the corresponding SLP is linear in i. This has important applications in computational group theory, by using SLPs to efficiently encode group elements as words over a given generating set. Straight-line programs were introduced by Babai and Szemerédi in 1984 as a tool for studying the computational complexity of certain matrix group properties. Babai and Szemerédi prove that every element of a finite group G has an SLP of length O(log2|G|) in every generating set. An efficient solution to the constructive membership problem is crucial to many group-theoretic algorithms. It can be stated in terms of SLPs as follows. Given a finite group G = 〈S〉 and g ∈ G, find a straight-line program computing g over S. The constructive membership problem is often studied in the setting of black box groups. The elements are encoded by bit strings of a fixed length. Three oracles are provided for the group-theoretic functions of multiplication, inversion, and checking for equality with the identity. A black box algorithm is one which uses only these oracles. Hence, straight-line programs for black box groups are black box algorithms. Explicit straight-line programs are given for a wealth of finite simple groups in the online ATLAS of Finite Groups. Let G be a finite group and let S be a subset of G. A sequence L = (g1,…,gm) of elements of G is a straight-line program over S if each gi can be obtained by one of the following three rules: The straight-line cost c(g|S) of an element g ∈ G is the length of a shortest straight-line program over S computing g. The cost is infinite if g is not in the subgroup generated by S. A straight-line program is similar to a derivation in predicate logic. The elements of S correspond to axioms and the group operations correspond to the rules of inference. Let G be a finite group and let S be a subset of G. A straight-line program of length m over S computing some g ∈ G is a sequence of expressions (w1,…,wm) such that for each i, wi is a symbol for some element of S, or wi = (wj,-1) for some j < i, or wi = (wj,wk) for some j,k < i, such that wm takes upon the value g when evaluated in G in the obvious manner.