mod! PNAT {
  [Nat]
  op 0 : -> Nat
  op s : Nat -> Nat
  op _+_ : Nat Nat -> Nat {comm assoc}
  op _*_ : Nat Nat -> Nat {comm assoc}
  op sigma : Nat -> Nat
  op _=_ : Nat Nat -> Bool
  vars X Y : Nat
  eq X + 0 = X .
  eq X + s(Y) = s(X + Y) .
  eq X * 0 = 0 .
  eq X * s(Y) = X + (X * Y) .
  eq sigma(0) = 0 .
  eq sigma(s(X)) = sigma(X) + s(X) .  
  eq (0 = 0) = true .
  eq (0 = s(X)) = false .
  eq (s(X) = s(Y)) = (X = Y) .
  eq (X = X) = true .
}

mod LEMMA {
  pr(PNAT)
  op x : -> Nat
  op lemma1 : Nat -> Bool
--
-- 2*(1 + ... + x) = (1 + x)*x
--
  vars X Y Z : Nat
  eq lemma1(X) = ((s(s(0)) * sigma(X)) = (s(0) + X) * X) .
}

open LEMMA
 eq x = 0 .
 red lemma1(x) .
close
open LEMMA
  op y : -> Nat .
  eq x = s(y) .
  eq ((sigma(y) + sigma(y)) = (y + (y * y))) = false  .
  red lemma1(y) implies lemma1(x) .
close
open LEMMA
  op y : -> Nat .
  eq x = s(y) .
  eq (sigma(y) + sigma(y)) = (y + (y * y)) .
  red lemma1(y) implies lemma1(x) .
close