Oopm1516 Ex06

Zielsetzung für die Übung

  • Beweis durch Induktion
add über nat ist kommutativ:
add(x,y) = add(y,x)

Induktion über x:
Induktionsanfang: x = zero

add(zero,y) = add(y,zero)

add(zero,y)
->[1] y
<-[2] add(y, zero)   q.e.d.

------------------
Induktionsschritt: x = k

Induktionsvoraussetzung:
add(k,y) = add(y,k)

Induktionsbehauptung:
add(succ(k),y) = add(y,succ(k))

       add(succ(k),y)
->[3]  succ(add(k,y))
->[IV] succ(add(y,k))
<-[4]  add(y,succ(k))   q.e.d.

===================

noch zu zeigen:
add(zero,y) = add(y,zero)

Induktionsanfang: y = zero
add(zero,zero) = add(zero,zero)

----------------
Induktionsschritt: y = k

Induktionsvoraussetzung:
add(zero,k) = add(k,zero)

Induktionsbehauptung:
add(zero,succ(k)) = add(succ(k),zero)

       add(zero,succ(k))
->[4]  succ(add(k,zero))
->[IV] succ(add(zero,k))
<-[3]  add(succ(k),zero)   q.e.d.

Axiome:
[1] add(zero, n) = n
[2] add(n, zero) = n
[3] add(succ(n1), n2) = succ(add(n1, n2))
[4] add(n1, succ(n2)) = succ(add(n1, n2))

Zielsetzung für das Programmierpraktikum

  • Implementation von verketteten Listen
    • speziell: Binärbäume (Liste mit zwei Nachfolgern)