LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-12

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Reversal is an involution and reverses concatenation

Statement

For words $u, v$ over a fixed alphabet and languages $L, K$ over that alphabet:

$(u v)^{R} = v^{R} u^{R}$ .
$(w^{R})^{R} = w$ for every word $w$ .
$(L K)^{R} = K^{R} L^{R}$ and $(L^{R})^{R} = L$ .

Facts & Assumptions

Given: Words $u, v, w$ and languages $L, K$ over a fixed alphabet $Σ$ .

[L1]

Word reversal is defined by $w^{R} (i) = w (n - 1 - i)$ for a word $w : n \to Σ$ , and language reversal is $L^{R} = {x^{R} : x \in L}$ , by Word reversal and language reversal.

[L2]

Word concatenation is the offset construction and language concatenation is $A B = {a b : a \in A and b \in B}$ by Computation alphabets, words, the empty word, and $Σ^{*}$ and Language concatenation, powers, and Kleene star.

Proof

technique · direct

1.1

Let $∣ u ∣ = m$ and $∣ v ∣ = n$ . For $i < n$ , the $i$ th letter of $(u v)^{R}$ is the $(m + n - 1 - i)$ th letter of $u v$ , hence the $(n - 1 - i)$ th letter of $v$ by [L2], so $(u v)^{R} (i) = v^{R} (i)$ .

givenL1L2

1.2

For $n \leq i < m + n$ , write $i = n + j$ with $j < m$ . Then the $i$ th letter of $(u v)^{R}$ is the $(m - 1 - j)$ th letter of $u$ , so $(u v)^{R} (i) = u^{R} (j)$ ; this is exactly the offset rule for the concatenation $v^{R} u^{R}$ . Therefore $(u v)^{R} = v^{R} u^{R}$ .

L1L2algebra

1.3

Let $∣ w ∣ = n$ . For each $i < n$ , $(w^{R})^{R} (i) = w^{R} (n - 1 - i) = w (n - 1 - (n - 1 - i)) = w (i) .$ So $(w^{R})^{R} = w$ .

L1algebra

2.1

If $x \in (L K)^{R}$ , then $x = y^{R}$ for some $y \in L K$ by [L1]. By [L2] we may write $y = u v$ with $u \in L$ and $v \in K$ , and then step 1.2 gives $x = (u v)^{R} = v^{R} u^{R} \in K^{R} L^{R}$ . Hence $(L K)^{R} \subseteq K^{R} L^{R}$ .

L1L2step 1.2

2.2

Conversely, if $x \in K^{R} L^{R}$ , then $x = v^{R} u^{R}$ with $u \in L$ and $v \in K$ by [L1] and [L2]. Step 1.2 gives $x = (u v)^{R}$ , and $u v \in L K$ , so $x \in (L K)^{R}$ . Thus $(L K)^{R} = K^{R} L^{R}$ .

L1L2step 1.2

3.1

By [L1], $x \in (L^{R})^{R}$ exactly when $x = y^{R}$ for some $y \in L^{R}$ , that is, for some $y = z^{R}$ with $z \in L$ . Step 1.3 then gives $x = (z^{R})^{R} = z \in L$ . Conversely, if $z \in L$ then step 1.3 gives $z = (z^{R})^{R} \in (L^{R})^{R}$ . So $(L^{R})^{R} = L$ .

L1step 1.3∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

7 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Jean Gallier and Jocelyn Quaintance, Introduction to the Theory of Computation: Some Notes for CIS511 (standard reference, not scraped)