summaryrefslogtreecommitdiff
path: root/files/practicum/BewijsPeano.icl
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:
-------