exercise: THEORY
BEGIN
 
  T: TYPE+
  x, y: VAR T

  p(x): bool
  r(x): bool
  s(x): bool

  q(x, y): bool
  c: T

  A: LEMMA
    p(c) AND (FORALL x: p(x) => r(x)) =>
      (EXISTS x: r(x)) 

  B: LEMMA
    (EXISTS y: FORALL x: q(x,y)) =>
    (FORALL x: EXISTS y: q(x,y))

  C: LEMMA
    (EXISTS x: p(x)) AND
    (FORALL x: p(x) => EXISTS y: q(x,y)) =>
    (EXISTS x, y: q(x,y))
 
  D: LEMMA
   (EXISTS x: p(x)) OR (EXISTS x: r(x)) =>
     (EXISTS x: p(x) OR r(x))

  E: LEMMA
   (FORALL x: r(x) => p(x)) AND (FORALL x: s(x) => p(x)) AND 
   (FORALL x: r(x) OR s(x)) =>
     (FORALL x: p(x))

  m: VAR nat
  n: VAR nat
  o: VAR nat

  exp(m, n): RECURSIVE nat = 
    IF n = 0
      THEN 1
      ELSE m * exp(m, n-1)
    ENDIF
    MEASURE abs(n)

  T: LEMMA
    FORALL m, n: exp(m,n+1) = m*exp(m,n)

  S: LEMMA
    FORALL m, n, o:
      exp(m, n)*exp(m, o) = exp(m, n+o)

END exercise