blob: 9d1bbe38be8b76332e8e9c328f9b3b88bb1b7c9f (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
|
Zij gegeven:
:: Nat = Zero | Suc Nat
(##) :: Nat -> Int
(##) Zero = 0 (1)
(##) (Suc n) = 1 + ##n (2)
1. Zij bovendien gegeven:
add :: Nat Nat -> Nat
add Zero n = n (3)
add (Suc m) n = Suc (add m n) (4)
Bewijs de volgende stelling voor alle Nat m en n:
## (add m n) = ##m + ##n
Bewijs:
-------
2. Zij bovendien gegeven:
mul :: Nat Nat -> Nat
mul m Zero = Zero (5)
mul m (Suc n) = add (mul m n) m (6)
Bewijs de volgende stelling voor alle Nat m en n:
## (mul m n) = ##m * ##n
Bewijs:
-------
|