From a7d7542dc646a5fd124ef71e71ce260889f1701b Mon Sep 17 00:00:00 2001 From: Camil Staps Date: Tue, 2 Feb 2016 19:24:50 +0100 Subject: Moved to 1415 directory --- 1415/files/practicum/BewijsPeano.icl | 35 +++++++++++++++++++++++++++++++++++ 1 file changed, 35 insertions(+) create mode 100644 1415/files/practicum/BewijsPeano.icl (limited to '1415/files/practicum/BewijsPeano.icl') 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: +------- -- cgit v1.2.3