single: THEORY
  BEGIN
  
  time: TYPE = int
  j, k, m, n, t, t1, t2: VAR time
  value: TYPE = {x: nat | x <= 1}
  signal: TYPE = [time -> value]
  i, o, x, a, b, y, f: VAR signal
  -((a: value)): value = (1 - a)
      ;
  delay(i, o): bool = (FORALL t: (o(t + 1) = i(t)))
      
  bubble_and(a, b, y): bool = (FORALL t: (y(t) = (-a(t)) * b(t)))

  inv(i, o): bool = (FORALL t: o(t) = -i(t))
      
  env1(f): bool = (FORALL t: (EXISTS t1: t1 < t AND f(t1) = 0))
      
  env2(f): bool = (FORALL t: (EXISTS t1: t < t1 AND f(t1) = 0))
      
  imp(i, o): bool = (EXISTS x: (delay(i, x) AND bubble_and(i, x, o)))
      
  Pulse(f, n, m):
    bool
      =
        (n < m
           AND f(n - 1) = 0
             AND f(m) = 0 AND (FORALL t: (n <= t AND t < m IMPLIES f(t) = 1)))
      
  SinglePulse(f, n): bool = Pulse(f, n, n + 1)
      
  spec1(i, o):
    bool
      =
        (FORALL n, m:
           Pulse(i, n, m)
             IMPLIES
             (EXISTS k:
                n <= k
                  AND k <= m
                    AND o(k) = 1
                      AND
                      (FORALL j:
                         (n <= j AND j <= m AND o(j) = 1 IMPLIES j = k))))


  spec1_insufficient: lemma inv(i,o) => spec1(i,o)  
    
  spec2(i, o):
    bool
      =
        (FORALL k:
           o(k) = 1
             IMPLIES SinglePulse(o, k)
               AND (EXISTS n, m: n <= k AND k <= m AND Pulse(i, n, m)))
      
  IMPORTING bounds
  env1_lemma:
    LEMMA
      env1(f)
        IMPLIES
        (EXISTS (t1: time):
           t1 < t
             AND f(t1) = 0
               AND
               (FORALL (t2: time): t1 < t2 AND t2 < t IMPLIES NOT (f(t2) = 0)))
    
  sp_in_lemma: LEMMA o(k) = 1 AND imp(i, o) IMPLIES i(k) = 0 AND i(k - 1) = 1
    
  single_pulse1: LEMMA imp(i, o) IMPLIES spec1(i, o)
    
  single_pulse2: LEMMA env1(i) IMPLIES (imp(i, o) IMPLIES spec2(i, o))
    
  single_pulse: LEMMA env1(i) AND imp(i, o) IMPLIES spec1(i, o) AND spec2(i, o)
    
  END single