## Common factor of two words

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

**Authors:** Jean-Christophe Filliâtre / Andrei Paskevich

**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

download ZIP archive

# Why3 Proof Results for Project "word_common_factor"

## Theory "word_common_factor.Top": fully verified

Obligations | Alt-Ergo 2.2.0 | Alt-Ergo 2.4.1 | CVC4 1.6 | ||

VC for power | --- | --- | 0.05 | ||

VC for power_add | 0.14 | --- | --- | ||

VC for common_factor | --- | --- | --- | ||

split_vc | |||||

precondition | 0.01 | --- | --- | ||

postcondition | --- | --- | 0.14 | ||

variant decrease | --- | --- | 0.05 | ||

precondition | --- | --- | --- | ||

split_all_full | |||||

precondition | --- | --- | 0.06 | ||

variant decrease | --- | --- | --- | ||

split_all_full | |||||

variant decrease | --- | --- | 0.05 | ||

variant decrease | --- | --- | 0.05 | ||

variant decrease | --- | --- | 0.04 | ||

variant decrease | --- | --- | 0.04 | ||

variant decrease | --- | --- | 0.04 | ||

variant decrease | --- | --- | 0.03 | ||

precondition | --- | --- | 0.03 | ||

postcondition | --- | --- | 0.06 | ||

postcondition | --- | 0.10 | --- |