```;; Aufbau des Beweisbaums

(define proof-stack ())

(define proof-push
(lambda (rule)
(set! proof-stack (cons rule proof-stack))))

(define proof-stack-to-tree
(lambda ()
(let ((rule (car proof-stack)))
(begin
(set! proof-stack (cdr proof-stack))
(case rule
((var lit abs)
rule)
((if-f if-t op)
(let ((subtree2 (proof-stack-to-tree)))
(let ((subtree1 (proof-stack-to-tree)))
(list rule subtree1 subtree2))))
((app)
(let ((subtree3 (proof-stack-to-tree)))
(let ((subtree2 (proof-stack-to-tree)))
(let ((subtree1 (proof-stack-to-tree)))
(list rule subtree1 subtree2 subtree3))))))))))

;; Transitionsregeln

(define literal?
(lambda (a)
(or (integer? a) (boolean? a))))
(define interpret-literal
(lambda (a u)
(proof-push 'lit)
a))

(define variable? ...)
(define interpret-variable ...)

(define conditional? ...)
(define interpret-conditional ...)

(define abstraction? ...)
(define interpret-abstraction ...)

(define application? ...)
(define interpret-application ...)

;; Hauptfunktionen

(define interpret
(lambda (a u)
(cond ((literal?     a) (interpret-literal     a u))
((variable?    a) (interpret-variable    a u))
((conditional? a) (interpret-conditional a u))
((abstraction? a) (interpret-abstraction a u))
((application? a) (interpret-application a u))
(else
(error "illegal expression syntax")))))

(define global-environment
(list (cons '+ (lambda (x) (lambda (y) (+ x y))))
(cons '- (lambda (x) (lambda (y) (- x y))))
(cons '* (lambda (x) (lambda (y) (* x y))))
(cons '< (lambda (x) (lambda (y) (< x y))))))

(define start
(lambda (a)
(set! proof-stack ())
(let ((res (interpret a global-environment)))
(list res (proof-stack-to-tree)))))
```