## Common factor of two words

If ab = ba then the words a and b are powers of a common word.

Topics: Words

Tools: Why3

see also the index (by topic, by tool, by reference, by year)

## Common factor of two words

If `a ++ b = b ++ a` then `a` and `b` are powers of a common word.

Authors: Jean-Christophe Filliâtre (CNRS) Andrei Paskevich (Univ Paris-Sud)

```use int.Int
use seq.Seq
use seq.FreeMonoid

type char
type word = seq char

let rec function power (w: word) (n: int) : word
requires { n >= 0 }
variant  { n }
= if n = 0 then empty else w ++ power w (n - 1)

let rec lemma power_add (w: word) (n1 n2: int)
requires { n1 >= 0 && n2 >= 0 }
variant  { n1 }
ensures  { power w (n1 + n2) == power w n1 ++ power w n2 }
= if n1 > 0 then power_add w (n1 - 1) n2

let rec common_factor (a b: word) : (w: word, ka: int, kb: int)
requires { a ++ b == b ++ a }
ensures  { ka >= 0 /\ a == power w ka }
ensures  { kb >= 0 /\ b == power w kb }
variant  { length a, length b }
= if length a = 0 then b, 0, 1
else if length b = 0 then a, 1, 0
else if length a <= length b then begin
let c = b[length a ..] ensures { b == a ++ result } in
let w, ka, kc = common_factor a c in
w, ka, ka + kc
end else
let w, ka, kb = common_factor b a in
w, kb, ka
```