summaryrefslogtreecommitdiff
path: root/files/practicum/BewijsPeano.icl
diff options
context:
space:
mode:
Diffstat (limited to 'files/practicum/BewijsPeano.icl')
-rw-r--r--files/practicum/BewijsPeano.icl35
1 files changed, 35 insertions, 0 deletions
diff --git a/files/practicum/BewijsPeano.icl b/files/practicum/BewijsPeano.icl
new file mode 100644
index 0000000..9d1bbe3
--- /dev/null
+++ b/files/practicum/BewijsPeano.icl
@@ -0,0 +1,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:
+-------