# Blatt 5
Lukas Bruns
Robin Faeseke

Aufgabe 1
1.
not(true) = false
not(false) = true
2.
a)
Gilt, da succ(succ(succ(zero)))= zero nach Axiomen. Daher folgt succ(succ(succ(succ(zero)))) = succ(zero) wenn man den Teil nach dem ersten succ mit dem Axiom ersetzt.
b)
Sei succ(zero) = m und zero = n, dann folgt:
mult(succ(succ(zero)),zero) = zero
⇔
mult(succ(m),n) = zero
⇔
add(mult(succ(zero),n),n) = zero
⇔
add(add(mult(zero,n),n),n) = zero
⇔
add(add(zero,n),n) = zero
⇔
add(zero,n) = zero
⇔
n = zero
Und das ist eine wahre Aussage.

c)
iszero(add(succ(succ(zero)), succ(zero))) = false
⇔
iszero(succ(add(succ(zero),succ(zero)))) = false
⇔
iszero(succ(succ(add(zero,succ(zero))))) = false
⇔
iszero(succ(succ(succ(zero)))) = false
⇔
iszero(zero) = false
⇔
true = false

Also ist die Aussage falsch.

3.
Modulo 3, erkennbar an der succesor Spezifikation.

4.
n,m,z ∈ ℕ0
b ∈ B
iszero^ℳ = n -> b : {n -> true, falls n = zero
n-> false, falls n ≠ zero}
add^ℳ = ℕ0> : {n,m -> succ(n), falls m = succ(zero)
n,m -> succ(add(n,z)), falls m = succ(z) und m≠ succ(zero) }

mult^ℳ =ℕ0*ℕ0 -> ℕ0: {n,m -> n, falls m = succ(zero)
n,m -> add(mult(n,z)), falls m = succ(z) und m≠succ(zero) }

succ^ℳ = ℕ0 -> ℕ0:{n-> n+1 }

5.
Ja es gilt das Erzeugerprinzip, weil alle in mNat befindlichen Elemente mit einer endlichen Anzahl an Operationen dargestellt werden können.

Aufgabe 2

Die Funktion intersect gibt die Menge zurück, welche in den beiden übergebenen Mengen übereinstimmt. Also die Schnittmenge der beiden übergebenen Mengen.
Dabei geben die Axiome intersect(emptyset,s*)= emptyset und intersect(s, emptyset) = emptyset jeweils an, dass die Schnittmenge mit der leeren Menge wieder die leere Menge ergibt.
Das Axiom intersect(add(s,n), add(s',n)) = add(intersect(s,s'),n) besagt, dass das hinzufügen eines Elements auf beiden Stacks und danach die Bildung der Schnittmenge das gleiche ist wie die Schnittmenge der beiden Stacks mit dem Element n zu bilden.
Das letzte Axiom unter der Bedingung n ≠ n besagt, dass die Schnittmenge aus dem oberen Fall das gleiche ist wie die Vereinigung der jeweiligen Schnittmengen.

Aufgabe 3

spec NatArray = Bool and Nat then

sorts
array = empty | set(array,nat, nat)

ops
set: (array,nat,nat) array
defined: (array, nat) bool
get: (array, nat) nat
remove: (array, nat) array
merge: (array, array) array
sum: (array) nat

vars
a, a': array
x,y,z: nat

axioms

set(remove(a,x),x,get(a,x)) = a

defined(empty,x) = false
defined(set(a,x,y), x) = true

get(empty,x) = undefined
get(set(a,x,y), x) = y

remove(empty,x) = empty
remove(a,x) = undefined

merge(set(a,y,z),set(a',y,x)) = set(a,y,z)

sum(add(get(a,x), get(a,succ(x)))) = a'