From 059f9724c44202f9a16244b517855724bcbaf5eb Mon Sep 17 00:00:00 2001
From: WGAVermeer <w.g.a.vermeer@student.tue.nl>
Date: Sun, 1 Mar 2026 18:26:27 +0100
Subject: [PATCH] first exercises

---
 chap_3/e3_1.dfy | 62 +++++++++++++++++++++++++++++++++++++++++++++++++
 chap_3/e3_2.dfy |  0
 chap_3/e3_3.dfy |  0
 3 files changed, 62 insertions(+)
 create mode 100644 chap_3/e3_1.dfy
 create mode 100644 chap_3/e3_2.dfy
 create mode 100644 chap_3/e3_3.dfy

diff --git a/chap_3/e3_1.dfy b/chap_3/e3_1.dfy
new file mode 100644
index 0000000..8ed69cd
--- /dev/null
+++ b/chap_3/e3_1.dfy
@@ -0,0 +1,62 @@
+function F(x: int): int 
+    decreases x
+{
+    if x < 10 then x else F(x - 1)
+}
+
+function G(x: int): int 
+    decreases x
+{
+    if 0 <= x then G(x - 2) else x
+}
+
+function H(x: int): int 
+    decreases x + 60
+{
+    if x < -60 then x else H(x - 1)
+}
+
+function I(x: nat, y: nat): int 
+    decreases x + y
+{
+    if x == 0 || y == 0 then
+        12
+    else if x % 2 == y % 2 then
+        I(x - 1, y)
+    else   
+        I(x, y - 1)
+}
+
+function J(x: nat, y: nat): int 
+    decreases x, y
+{
+    if x == 0 then
+        y
+    else if y == 0 then
+        J(x - 1, 3)
+    else
+        J(x, y - 1)
+}
+
+function K(x: nat, y: nat, z: nat): int 
+    decreases x, y, z
+{
+    if x < 10 || y < 5 then
+        x + y
+    else if z == 0 then 
+        K(x - 1, y, 5)
+    else
+        K(x, y - 1, z - 1)
+}
+
+function L(x: int): int 
+    decreases 100 - x
+{
+    if x < 100 then L(x+1) + 10 else x
+}
+
+function G'(n: nat): nat 
+    decreases n
+{
+    if n == 0 then 0 else n - G'(G'(n - 1))
+}
\ No newline at end of file
diff --git a/chap_3/e3_2.dfy b/chap_3/e3_2.dfy
new file mode 100644
index 0000000..e69de29
diff --git a/chap_3/e3_3.dfy b/chap_3/e3_3.dfy
new file mode 100644
index 0000000..e69de29