% Case 1:  u = x * y

formulas(goals).

    ( Power(u * u1,x)
       & Power(u * u2,y)
       & u = x * u3
       & u = y * u4
       & -Shorter(u, x * y)
       & u = x * y              % Case 1
    )
    ->
    (x * y = y * x) # label("Case 1").

end_of_list.

formulas(assumptions).

   % general lemmas (proved).

   (x * y = u * v) -> ( Prefix(x,u) | Prefix(u,x) | x = u ) # label("Lemma 1").

   Prefix(x,y) -> Shorter(x,y) # label("Lemma 2").

end_of_list.
