diff options
author | Camil Staps | 2016-02-02 19:24:50 +0100 |
---|---|---|
committer | Camil Staps | 2016-02-02 19:24:50 +0100 |
commit | a7d7542dc646a5fd124ef71e71ce260889f1701b (patch) | |
tree | 04ed89503bbb3cc9933273a1326a53ca724c3492 /1415/files/practicum/BewijsPeano.icl | |
parent | week6 camil: working positioning of lines by putting empties at left and righ... (diff) |
Diffstat (limited to '1415/files/practicum/BewijsPeano.icl')
-rw-r--r-- | 1415/files/practicum/BewijsPeano.icl | 35 |
1 files changed, 35 insertions, 0 deletions
diff --git a/1415/files/practicum/BewijsPeano.icl b/1415/files/practicum/BewijsPeano.icl new file mode 100644 index 0000000..9d1bbe3 --- /dev/null +++ b/1415/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: +------- |