Korrektheitsbeweis (1)

• Implementierung:

  init         empty-queue
  append(q,e)     (add-element e q)
  is_empty(q)     (is_empty-queue? q)
  next(q)         (first-of q)
  remove(q)       (remove-from q)
  

• next(append(init, e)) = e

  (first-of (add-element e empty-queue)) = e

• next(append(append(q, e'),e) = next(append(q, e'))

  (first-of (add-element e (add-element e' q)))
= (first-of (add-element e' q))

• Damalige Implementierung:

  (define (add-element element queue)
     (cond ((is-empty-queue? queue) 
                 (cons element empty-queue))
           (else (cons (first-of queue)
                       (add-element element 
                                    (remove-from queue)
  )  )     )     )     )
  
  (define (first-of queue)
     (cond ((is-empty-queue? queue) 
                 (queue-error 1))
           (else (car queue))
  )  )