Beispiel 1a:

  Functions:
	div(a,b)    = divh(a,b,0)
	divh(a,b,0) = if lt?(minus(a,b), 0) then c else divh(minus(a,b), b, plus(c,1))

  Theorem:
    forall ω in ENV: I(δ, ω, div(a,b)) = ω(a) / ω(b) (+  R, with R ... Rest of integer division)

  Proof:
    ω(a) = n, with n >= 0
	ω(b) = m, with m > 0

      I(δ, ω, div(a,b))
    = I(δ, ω', divh(a, b, 0))                      with
        ω'(a) = I(δ, ω, a) = ω(a) = n
        ω'(b) = I(δ, ω, b) = ω(b) = m
		ω'(c) = I(δ, ω, 0) = 0
    = ω'(a) / ω'(b) + ω'(c)                        lr Lemma 1
    = n / m + 0
    = n / m
    q.e.d.

  Lemma 1:
    forall ω in ENV: I(δ, ω, divh(a, b, c)) = ω(a) / ω(b) + ω(c)

  Base case of Lemma 1:
    ω(a) = 0
    ω(b) = m, with arbitrary value in N \ {0}
	ω(c) = k, with arbitrary value in N^0

      I(δ, ω, divh(a, b, c))
    = I(δ, ω', if lt?(minus(a,b), 0) then c
		else divh(minus(a,b), b, plus(c,1)))
                                                   with
        ω'(a) = I(δ, ω, a) = ω(a) = 0
        ω'(b) = I(δ, ω, b) = ω(b) = m
		ω'(c) = I(δ, ω, c) = ω(c) = k
    = I(δ, ω', c)                                  since I(δ, ω', lt?(minus(a, b), 0)) = T
    = ω'(c)
    = k
    = 0 / m + k
    = ω(a) / ω(b) + ω(c)
    q.e.d.

  Induction step of Lemma 1:
    ω(a) = n + 1, n >= 0
	ω(b) = m, m > 0
    ω(c) = k, with arbitrary value in N^0

      I(δ, ω, divh(a, b, c))
    = I(δ, ω', if lt?(minus(a,b), 0) then c
		else divh(minus(a,b), b, plus(c,1)))
                                                   with
        ω'(a) = I(δ, ω, a) = ω(a) = n + 1
        ω'(b) = I(δ, ω, b) = ω(b) = m
		ω'(c) = I(δ, ω, c) = ω(c) = k

CASE  I: I(δ, ω', lt?(minus(a,b), 0)) = F   => n + 1 > m (ω'(a) >= ω'(b))

    = I(δ, ω', divh(minus(a,b), b, plus(c,1)))

    = I(δ, ω'', divh(a, b, c))                     with
        ω''(a) = I(δ, ω', minus(a, b)) = ω'(a) - ω'(b) = n + 1 - m
        ω''(b) = I(δ, ω', b) = ω'(b) = m
		ω''(c) = I(δ, ω', plus(c, 1)) = ω'(c) + 1 = k + 1
    = ω''(a) / ω''(b) + ω''(c)                     hypothesis
    = (n + 1 - m )/ m + k + 1
    = (n + 1) / m + k
    = ω(a)/ ω(b) + ω(c)
    q.e.d.


CASE II: I(δ, ω', lt?(minus(a,b), 0)) = T   => n + 1 < m (ω'(a) < ω'(b))

    = I(δ, ω', c)

    = ω'(c) = I(δ, ω, c) = ω(c) = k
    = k
    = 0 + k
    = n / m + k                                    with n < m (since n+1 < m)
    = ω(a) / ω(b) + ω(c)
    q.e.d.

Beispiel 1b:

  Functions:
	mod(a,b) = if lt?(minus(a, b), 0) then a else mod(minus(a,b), b)

	#Note: No helper function necessary => proof lemma directly for mod(a,b)

  Theorem:
    forall ω in ENV: I(δ, ω, mod(a,b)) = ω(a) % ω(b)

  Proof:
    ω(a) = n, with n >= 0
	ω(b) = m, with m > 0

      I(δ, ω, mod(a,b))
    = I(δ, ω, if lt?(minus(a, b), 0) then a
		else mod(minus(a,b), b))                   with
        ω(a) = n
        ω(b) = m
    = ω(a) % ω(b)                                  lr Lemma 1
    = n % m
    q.e.d.

  Lemma 1:
    forall ω in ENV: I(δ, ω, mod(a, b)) = ω(a) % ω(b)

  Base case of Lemma 1:
    ω(a) = 0
    ω(b) = m, with arbitrary value in N \ {0}

      I(δ, ω, mod(a, b))
    = I(δ, ω, if lt?(minus(a, b), 0) then a
		else mod(minus(a,b), b))
                                                with
        ω(a) = 0
        ω(b) = m
    = I(δ, ω, a)                               since I(δ, ω, lt?(minus(a, b), 0)) = T
    = ω(a)
    = 0
    = 0 % m
    = ω(a) % ω(b)
    q.e.d.

  Induction step of Lemma 1:
    ω(a) = n + 1, n >= 0
	ω(b) = m, m in N \ {0}

      I(δ, ω, mod(a, b))
    = I(δ, ω, if lt?(minus(a, b), 0) then a
		else mod(minus(a,b), b))
                                                with
        ω(a) = n + 1
        ω(b) = m

CASE  I: I(δ, ω, lt?(minus(a,b), 0)) = F   => n + 1 > m    (ω(a) >= ω(b))

    = I(δ, ω, mod(minus(a,b), b))

    = I(δ, ω', mod(a, b))                       with
        ω'(a) = I(δ, ω, minus(a, b)) = ω'(a) - ω'(a) = n + 1 - m
        ω'(b) = I(δ, ω, b) = ω(b) = m

    = ω'(a) % ω'(b)                             hypothesis
    = (n + 1 - m ) % m
    = (n + 1) % m
    = ω(a) % ω(b)
    q.e.d.


CASE II: I(δ, ω, lt?(minus(a,b), 0)) =  T   => n + 1 < m   (ω'(a) < ω'(b))

    = I(δ, ω, a)

    = ω(a) = n + 1
    = n + 1
    = n + 1 % m                                 since n+1 < m
    = ω(a) % ω(b)
    q.e.d.


------------------------------------------------------------------------------------------

Beispiel 3:

  1) max(x1, x2) soll immer die Liste mit der größeren Verschachtelungstiefe zurückgeben.
		Dafür wird die Funktion rest(x1) benötigt, welche im Übungsskriptum definiert ist.
		Die Definition von rest(x1) besagt allerdings, dass wenn x1 eine Liste ist, die
		leere Liste [] als Ergebnis von rest zurückgegeben werden soll. Dadurch wird die
		eigentliche Tiefe von l in max ignoriert (sofern die Tiefe einer Liste >= 2
		und die der anderen > 2 ist).

		In max wird zunächst überprüft ob einer der zwei Parameter x1, x2 nil ist. In diesem
		Fall könnte gleich der jeweils andere Parameter zurückgegeben werden (im Falle,
		dass dieser ebenfalls nil ist, stimmt liefert max ebenfalls eine korrekte Lösung).
		Sind weder x1, noch x2 nil, wird eine "neue" Liste aufgebaut (mit build), die
		mithilfe vom Rekursionsaufruf von max mit den Parametern rest(x1) und rest(x2),
		letztendlich dieselbe Verschachtelungstiefe wie die größere der zwei
		Eingangslisten aufweisen soll. Da rest aber bei Listen mit
		einer Verschachtelungstiefe >= 2 das falsche Ergebnis liefert, kann hat die neue
		Liste, die von max zurückgegeben wird, nicht die richtige Tiefe (sondern maximal [],
		also "1") haben, sofern eine der Listen eine Tiefe >= 2 und die andere eine Tiefe
		von > 2 hat.

	2) Beispiel: max([[]], [[[]]])
		ω(x1) = [[]]
		ω(x2) = [[[]]]
		ω(x3) = nil

		  I(δ, ω, max(x1, x2))
		= I(δ, ω, if eq?(x1, nil) then x2
			else if eq?(x2, nil) then x1
			else build(max(rest(x1), rest(x2)), x3))    with
			  ω(x1) = [[]]
			  ω(x2) = [[[]]]
			  ω(x3) = nil
		= 	I(δ, ω, build(max(rest(x1), rest(x2)), x3))

		=   I(δ, ω', build(max(x1, x2), x3))            with
			  ω'(x1) = I(δ, ω, rest(x1)) = []
			  ω'(x2) = I(δ, ω, rest(x2)) = []           !Here is the problem!
			  ω'(x3) = ω(x3) = nil = []                 nil = "empty list" = []
		= 	I(δ, ω', if eq?(x1, nil) then x2
			else if eq?(x2, nil) then x1
			else build(max(rest(x1), rest(x2)), x3))
		=   I(δ, ω', build(x2, x3))                     with
			  ω'(x2) = []
			  ω'(x3) = []

		=   [[]]                                        which is obviously wrong.

	3) Korrektur von max

		δmax = if eq?(x1, nil) then x2
				else if eq?(x2, nil) then x1
				else build(max(first(x1), first(x2)), nil)

		Durch die Verwendung von first anstelle von rest wird sichergestellt,
		dass die Verschachtelungstiefe auch für Listen mit einer Tiefe > 2 korrekt
        in max bestimmt wird. Laut der Definition von first im Skriptum wird immer
		das erste Element in der mitgegebenen Liste zurückgegeben. Dadurch wird
		auch im Falle von einer Listentife > 2 oft genug build aufgerufen, um
		die korrekte maximale Verschachtelungstiefe zu bestimmen.

	4) 	Beispiel: max([[]], [[[]]])
		ω(x1) = [[]]
		ω(x2) = [[[]]]
		ω(x3) = nil

		  I(δ, ω, max(x1, x2))
		= I(δ, ω, if eq?(x1, nil) then x2
			else if eq?(x2, nil) then x1
			else build(max(first(x1), first(x2)), x3))    with
			  ω(x1) = [[]]
			  ω(x2) = [[[]]]
			  ω(x3) = nil
		= 	I(δ, ω, build(max(first(x1), first(x2)), x3))

		=   I(δ, ω', build(max(x1, x2), x3))            with
			  ω'(x1) = I(δ, ω, first(x1)) = []
			  ω'(x2) = I(δ, ω, first(x2)) = [[]]
			  ω'(x3) = ω(x3) = nil = []                 nil = "empty list" = []
		= 	I(δ, ω', if eq?(x1, nil) then x2
			else if eq?(x2, nil) then x1
			else build(max(first(x1), first(x2)), x3))
		=   I(δ, ω', build(x2, x3))                     with
			  ω'(x2) = [[]]
			  ω'(x3) = []

		=   [[[]]]                                      which is correct.