Mathematics and Computation Exam 1, June 3, 1998

Exercise 1. Let A ^{·} be shorthand for

⟨⟨⟨x + y | x:=x + 2⟩ | y:=x + 3⟩ | x:=⟨x + x | x:=5⟩⟩ ^{·}.

(a) Draw a syntax tree for A ^{·}.

(b) Draw a binding diagram for A ^{·}.

(c) Compute A ^{·}.

Exercise 2. Which of the following hold? Prove those that hold. Give counterexamples to those that fail. For each use of Tautology ^{·} draw the corresponding truth table.

(a) x ∈ B → y ∈ B → x ∧ y ∨ ¬y ⇔ x ∨ ¬y ^{·}.

(b) x ∈ B → y ∈ B → x ∧ (y ∨ ¬y) ≡ x ^{·}.

(c) if(x, if(y, T, F), if(y, F, F)) ≡ if(y, if(x, T, F), if(x, F, F)) ^{·}

Exercise 3. The algebraic system S ^{·} has the following five rules:

S rule A: a + b  ≡ b + a
S rule B: a + 0  ≡ a
S rule C: a − 0  ≡ a
S rule D: −(a − b) ≡ b − a
S rule E: a^{2} − b^{2} ≡ (a − b) · (a + b)

Algebraically prove the following within S ^{·}:

(a) −−(x − y) ≡ x − y ^{·}.

(b) −−x ≡ x ^{·}.

(c) −(x · x) ≡ (−x) · x ^{·}.

Exercise 4. I define

h(x, y) ≐ y = 0\{ \begin{matrix}−x \\ h(x, y − 1) + x \end{matrix} .

In addition to the rules in the text book, you may use the Mac ^{·} rules F ^{·}, G ^{·}, H ^{·}, and I ^{·} below in this exercise. You are not supposed to prove these rules.

Mac rule F: x ∈ Z → y ∈ N → h(x, y) ∈ Z
Mac rule G: (y = 0) ∈ T → −x = x · (y − 1)
Mac rule H: a · (b − 1) + a ≡ a · b
Mac rule I: a = b ⊢ a + c = b + c

(a) Prove ∀x∈Z∀y∈N: h(x, y) = x · (y − 1) ^{·}.

(b) What is the value of ∀u∈N∃x∈N∃y∈N: h(x, y) = u^{2} ^{·}? Explain your answer.

(c) What is the value of ∀u∈Z∃x∈N: h(x, x) ≤ u ^{·}? Explain your answer.

Exercise 1. Let A ^{·} be shorthand for

⟨⟨⟨x ∧ y | x:=¬x⟩ | y:=x ∨ y⟩ | x:=⟨x ∧ x | x:=F⟩⟩ ^{·}.

(a) Draw a syntax tree for A ^{·}.

(b) Draw a binding diagram for A ^{·}.

(c) Compute A ^{·}.

Exercise 2. The algebraic system S ^{·} has the following six rules:

S rule A: ⟨A ∧ B | x:=C⟩ ≡ ⟨A | x:=C⟩ ∧ ⟨B | x:=C⟩
S rule B: ⟨T | x:=C⟩ ≡ T
S rule C: ⟨F | x:=C⟩ ≡ F
S rule D: ⟨x | x:=C⟩ ≡ C
S rule E: ⟨y | x:=C⟩ ≡ y
S rule F: ⟨⟨A | x:=B⟩ | y:=⟨C | x:=T⟩⟩ ≡
⟨⟨A | y:=⟨C | x:=T⟩⟩ | x:=⟨B | y:=⟨C | x:=T⟩⟩⟩

Above, A, B, and C denote arbitrary terms whereas x og y denote arbitrary, distinct variables. Algebraically prove the following within S ^{·}:

(a) ⟨x ∧ y | x:=F⟩ ≡ F ∧ y ^{·}.

(b) ⟨u ∧ F | v:=T⟩ ≡ u ∧ F ^{·}.

(c) ⟨⟨x ∨ y | x:=y⟩ | y:=u ∧ F⟩ ≡ ⟨⟨x ∨ y | y:=u ∧ F⟩ | x:=u ∧ F⟩ ^{·}.

Exercise 3. Which of the following hold? Prove those that hold. Give counterexamples to those that fail. For each use of Tautology ^{·} draw the corresponding truth table.

(a) x ∈ B → y ∈ B → ¬(x ⇒ y) ⇔ ¬x ∧ y ^{·}.

(b) x ∈ B → y ∈ B → ¬(x ⇒ y) ⇔ x ∧ ¬y ^{·}.

(c) x ∈ B → y ∈ B → x ⇒ x ∧ y ≡ y ^{·}.

Exercise 4. I define

h(x) ≐ x = 0\{ \begin{matrix}1 \\ 3 · h(x − 1) \end{matrix} .

In addition to the rules in the text book, you may use the Mac ^{·} rules G ^{·} and H ^{·} below in this exercise. You are not supposed to prove these rules.

Mac rule G: a ∈ Z → a ≥ 0 → a ∈ N
Mac rule H: a ≥ 0 → b ≥ 0 → a · b ≥ 0

(a) Prove x∈N → h(x) ∈ Z ^{·}.

(b) Prove x∈N → h(x) ≥ 0 ^{·}.

(c) Prove x∈N → h(x) ∈ N ^{·}.

Mathematics and Computation Exam 3, January 21, 2000

Exercise 1. Let A ^{·} be shorthand for

⟨⟨⟨x : : y | x:=x ’ y⟩ | y:=x : : x⟩ | x:=⊥ : : N⟩ ^{·}.

(a) Draw a syntax tree for A ^{·}.

(b) Draw a binding diagram for A ^{·}.

(c) Compute A ^{·}.

Exercise 2.

(a) Write the representation of 1 ^{·} using only N ^{·} and x ˙. . y ^{·}.

(b) Write the representation of 1000 ^{·} using only N ^{·} and x ˙. . y ^{·}. The algebraic system S ^{·} has the following five rules:

S rule A: N′ x  ≡ N
S rule B: ⊥′ x  ≡ ⊥
S rule C: (x ˙. . y)′ N  ≡ x
S rule D: (x ˙. . y)′(u ˙. . v) ≡ y
S rule E: (x ˙. . y)′ ⊥  ≡ ⊥

(c) Prove 1 ’ (⊥ ˙. . ⊥) ’ N ≡ 1000 ’ (⊥ ˙. . ⊥) ’ N ^{·} algebraically within S ^{·}.

Exercise 3. Which of the following hold? Prove those that hold. Give counterexamples to those that fail. For each use of Tautology ^{·} draw the corresponding truth table.

(a) x ∈ B → ¬(x ∧ x) ⇔ ¬(x ∨ x) ^{·}.

(b) x ∈ B → ¬¬(x ∧ x) ≡ x ^{·}.

(c) x ∈ B → y ∈ B → (¬x) = y ⇔ ¬x = y ^{·}.

Exercise 4. I define

h(x) ≐ x = 0\{ \begin{matrix}0 \\ h(x − 2) + 1 \end{matrix} .

In addition to the rules in the text book, you may use the Mac ^{·} rules F ^{·} and G ^{·} below in this exercise. You are not supposed to prove these rules.

Mac rule F: a = 0 ≡ 2 · a = 0
Mac rule G: 2 · (a − 1) ≡ 2 · a − 2

(a) Prove x∈N → (x = 0) ∈ F → h(2 · x) ≡ h(2 · (x − 1)) + 1 ^{·}.

(b) Prove x∈N → (x = 0) ∈ T → h(2 · x) ≡ 0 ^{·}.

(c) Prove x∈N → h(2 · x) ∈ Z ^{·}.

Exercise 1. Let A ^{·} be shorthand for

⟨x′ x | x:=λx.λy.x′(y′ y)⟩ ^{·}.

(a) Draw a syntax tree for A ^{·}.

(b) Draw a binding diagram for A ^{·}.

(c) Compute A ^{·}.

Exercise 2. Which of the following hold? Prove those that hold. Give counterexamples to those that fail. For each use of Tautology ^{·} draw the corresponding truth table.

(a) a ∈ B → b ∈ B → c ∈ B → a∧b∨b∧c∨c∧a ⇔ (c∨b)∧(b∨a)∧(a∨c) ^{·}.

(b) a ∈ B → b ∈ B → if(a, b, ¬b) ⇔ if(b, a, ¬a) ^{·}.

(c) a ∈ B → b ∈ B → c ∈ B → d ∈ B → e ∈ B → f ∈ B → a ∧ ¬b ∧ ¬c ∧ d ∧ ¬e ∧ f ⇔ a ∧ ¬b ∧ ¬c ∧ d ∧ ¬e ^{·}.

Exercise 3. Let B ^{·} be shorthand for

/ 0.15F : : 1.3F ^{·}.

(a) Write the representation of B ^{·} using only N ^{·} and x ˙. . y ^{·}.

(b) What does B Tail Head ^{·} represent?

(c) Compute (λx.x head + x tail)′ B ^{·}.

Exercise 4. I define

f(x, y) ≐ x = 0\{ \begin{matrix}0 \\ y + f(x − 1, y) \end{matrix} .

(a) Compute f(4, 3) ^{·}.

(b) Prove y ∈ Z → x ∈ N → f(x, y) ∈ Z ^{·}.

(c) Prove ∃y∈Z: f(4, y) = 12 ^{·}.

Exercise 1. Let A ^{·} be shorthand for

(λx.⟨x′ x | x:=λy.x′(y′ y)⟩)′(λx.λy.y + 1)′ 3 ^{·}.

(a) Draw a syntax tree for A ^{·}.

(b) Draw a binding diagram for A ^{·}.

(c) Compute A ^{·}.

Exercise 2. I define

g(x, y) ≐ if(x ≤ 0, ⟨ ⟩, x : : g(x − y, y))
h(x, y) ≐ x : : h(x − y, y)

(a) Compute g(5, 2) ^{·}.

(b) Compute g(5, / 0.5F) ^{·}.

(c) Prove h(x, y) tail head ≡ x − y ^{·}.

Exercise 3. Which of the following hold? Prove those that hold. Give counterexamples to those that fail. For each use of Tautology ^{·} draw the corresponding truth table.

(a) if(x, F, y) ⇔ if(y, F, x) ^{·}.

(b) x ∈ B → y ∈ B → x ∧ y ∨ x ∧ ¬y ∨ ¬x ∧ y ⇔ x ∨ y ^{·}.

(c) x ∈ B → y ∈ B → (x ⇔ (y ⇔ (x ⇔ y))) ⇔ (x ⇔ (¬y ⇔ (¬x ⇔ y))) ^{·}.

Exercise 4. I define

f(x, y) ≐ x = 0\{ \begin{matrix}y \\ f(x − 1, −y) \end{matrix} .

(a) Compute f(2000, 2001) ^{·}.

(b) Prove x ∈ N → ∀y∈Z: f(x, y) ∈ Z ^{·}.

(c) Prove ∃x∈N: f(x, 4) = −4 ^{·}.

Exercise 1. Let A ^{·} be shorthand for

⟨x′ x′ F | x:=λx.λy.λz.case(y, z′ x′ x, x′ z′(y′ T))⟩ ^{·}.

(a) Draw a syntax tree for A ^{·}.

(b) Draw a binding diagram for A ^{·}.

(c) Compute A ^{·}.

Exercise 2. Which of the following hold? Prove those that hold. Give counterexamples to those that fail. For each use of Tautology ^{·} draw the corresponding truth table.

(a) x ∈ B → y ∈ B → z ∈ B → (x ∧ y ⇒ z) ⇒ (x ⇒ z) ^{·}.

(b) x ∈ B → y ∈ B → z ∈ B → (x ⇒ y) ∧ (y ⇒ z) ⇒ (x ⇒ z) ^{·}.

(c) x ∈ Z → x = 0 ∨ ¬ x = 0 ^{·}. Hint: Prove y ∈ B → y ∨ ¬y ^{·} first.

Exercise 3. I define that a term f ^{·} is a “counterexample” to A ⪯ B ^{·} if f ′ A ≡ T ^{·} and f ′ B ≡ ⊥ ^{·}. As an example, λx.x ^{·} is a counterexample to T ⪯ ⊥ ^{·}.

(a) Prove ⟨2, 3⟩ ⪯ ⟨2, 3, 4⟩ ^{·} or give a counterexample.

(b) Prove ⟨2, ⊥⟩ ⪯ ⟨2, 3⟩ ^{·} or give a counterexample.

(c) Draw a diagram of ⪯ ^{·} applied to ⊥ ^{·}, ⊥ : : ⊥ ^{·}, ⟨⊥⟩ ^{·}, 2 : : ⊥ ^{·}, and ⟨2⟩ ^{·}.

Exercise 4. I define

f(x) ≐ x = 0\{ \begin{matrix}4 \\ 15 − 2 · f(x − 1) \end{matrix} .

Prove or disprove the following:

(a) ∀x∈N: f(x) ∈ Z ^{·}.

(b) ∀x∈N: f(x) ∈ D ^{·}.

(c) ∀x∈N: f(x) ≥ 0 ^{·}.

Exercise 1. Let A ^{·} be shorthand for

((λx. x′ x)′(λx.λy. y′(x′ x))′(λx. T : : x)) head ^{·}.

(a) Draw a syntax tree for A ^{·}.

(b) Draw a binding diagram for A ^{·}.

(c) Compute A ^{·}.

Exercise 2. Prove or disprove the following. For each use of Tautology ^{·} draw the corresponding truth table.

(a) Mac lemma 2a: x ∈ B → y ∈ B → x ∧ y ∨ x ⇔ x ^{·}.

(b) Mac lemma 2b: ∀x∈B: x ∨ ¬x ^{·}.

(c) Mac lemma 2c: ∀x∈B: ¬x ^{·}. (Replace “lemma” by “antilemma” where appropriate).

Exercise 3. Let S ^{·} be an algebraic system with constructs 1 ^{·}, 2 ^{·}, 4 ^{·}, x + y ^{·}, x · y ^{·}, x^{y} ^{·}, and lg(x) ^{·}, and contradiction 1 ≡ 2 ^{·}. Associativity and priority of x + y ^{·}, x · y ^{·}, and x^{y} ^{·} are like in the text book. The system S ^{·} has the following algebraic rules:

S rule S1: 1 + 1  ≡ 2  S rule S5: x^{1}  ≡ x
S rule S2: 2 + 2  ≡ 4  S rule S6: x^{y+z} ≡ x^{y} · x^{z}
S rule S3: x · y  ≡ y · x  S rule S7: lg(2^{x}) ≡ x
S rule S4: (x · y) · z ≡ x · (y · z)

Prove the following:

(a) S lemma 3a: y^{2} ≡ y · y ^{·}.

(b) S lemma 3b: y^{4} ≡ y · y · y · y ^{·}.

(c) S lemma 3c: x + y ≡ y + x ^{·}.

Exercise 4. I define

f(n) ≐ n : : if(n = 0, ⟨ ⟩, f(n − 1)) .

Furthermore, I extend the Mac ^{·} system thus:

Mac rule NReflexive: x ∈ N → x = x

(a) Compute f(4) ^{·}.

(b) Prove Mac lemma 4b: ∀n∈N: f(n) ∈ N^{∗} .

(c) Prove Mac lemma 4c: ∀x∈N: ∃y∈N: f(y) head = x . Hint for 4c: Prove ∃y∈N: x = f(y) head ^{·} inside a block which starts with the hypothesis x∈N ^{·}. Then use Gen ^{·} to prove the lemma.

Mathematics and Computation Exam 8, May 28, 2002

Exercise 1. Let A ^{·} be shorthand for 1F#2F#3F#4F#5F#6F ^{·} where x#y ^{·} is defined thus:

construct x#y  x#y#z ˘→ x#(y#z)
x#y#z →^{∘} x · y + z  x#y ¨= x · y

(a) Draw a parse tree for A ^{·}.

(b) Draw a syntax tree for A ^{·}.

(c) Compute A ^{·}.

Exercise 2. The algebraic system S ^{·} has the following axioms:

ComP : x + y ≡ y + x  ComT : x · y ≡ y · x
AssocP : (x + y) + z ≡ x + (y + z) AssocT : (x · y) · z ≡ x · (y · z)
Dist :  x · (y + z) ≡ x · y + x · z Minus : x − y ≡ x + (−1) · y
SelfP : x + x ≡ 2 · x  SelfT : x · x ≡ x^{2}
Fail :  (x + y)^{2} ≡ x^{2} + y^{2}

The associativity and priority of the operators are as usual.

(a) Prove x − (y + z) ≡ x − y − z ^{·}.

(b) Prove (x + y)^{2} ≡ x^{2} + 2 · x · y + y^{2} ^{·}.

(c) Prove 0 ≡ 2 ^{·}. The proof may use Computation ^{·} and numerals. (The last question essentially says: Disprove Fail ^{·}).

Exercise 3. Which of the following hold? Prove those that hold. Give counterexamples to those that fail. For each use of Tautology ^{·} draw the corresponding truth table.

(a) x ∈ B → y ∈ B → ¬(x ⇒ y) ∨ ¬(y ⇒ x) ⇔ (x ⇔ ¬y) ^{·}.

(b) x ∈ B → x Tail ^{·}.

(c) x ∈ N → y ∈ N → (x = 0 ⇒ y = 0) ∨ (y = 0 ⇒ x = 0) ^{·}.

Exercise 4. I define

f(x, g) ≐ x = 0\{ \begin{matrix}0 \\ g′ f(x − 1, g) \end{matrix} .

(a) Compute f(117, λy.y+1) ^{·}.

(b) Prove ∀z∈N: g′ z ∈ N → x ∈ N → f(x, g) ∈ N ^{·}.

(c) Prove f(g, 2) ≠ 1 ^{·} or give a counterexample.

Exercise 1. Let A ^{·} be shorthand for

⟨⟨f′(x′ x) | x:=λf.λx.f′ x⟩ | f:=λf.f′ λx.117⟩ ^{·}.

(a) Draw a syntax tree for A ^{·}.

(b) Draw a binding diagram for A ^{·}.

(c) Compute A ^{·}.

Exercise 2. Which of the following hold? Prove those that hold. Give counterexamples to those that fail. For each use of Tautology ^{·} draw the corresponding truth table.

(a) x ∈ B → (x ⇒ x) ⇒ x ^{·}.

(b) x ∈ B → y ∈ B → (x ⇔ y) ⇒ (x ⇒ y) ^{·}.

(c) x ∈ B → y ∈ B → z ∈ B → (x ⇒ y) ∧ (y ⇒ z) ∧ (z ⇒ x) ⇔ (z ⇒ y) ∧ (y ⇒ x) ∧ (x ⇒ z) ^{·}.

Exercise 3. I define

f ≐ λx.λy.if(y = 0, T, x′ y)

What are the values of the following?

(a) Y′ λx.5 ^{·}.

(b) Y′ f ′ 0 ^{·}.

(c) Y′ f ′ 1 ^{·}.

Exercise 4. I define

f(x, y) ≐ x = 0\{ \begin{matrix}y \\ f(x − 1, y − 2) \end{matrix} .

(a) Compute f(100, 1000) ^{·}.

(b) Apply Induction ^{·} backwards to x ∈ N → ∀y∈Z: f(x, y) ∈ Z ^{·}.

(c) Prove x ∈ N → ∀y∈Z: f(x, y) ∈ Z ^{·}.

Exercise 1. Let A ^{·} be shorthand for

⟨x′ x | x:=λx.N ˙. . x′ x⟩\{ \begin{matrix}2 \\ 3 \end{matrix}

(a) Draw a syntax tree for A ^{·}.

(b) Draw a binding diagram for A ^{·}.

(c) Compute A ^{·}.

Exercise 2. The algebraic system S ^{·} has the constructs K ^{·}, x′ y ^{·}, and x ∘ y ^{·}, the contradiction K′ K ≡ K ^{·}, and the following axioms, priority rules, and associativity rules:

[ S rule K : K′ x′ y ≡ x  ]
[ S rule C : (f ∘ g)′ x ≡ f′(g′ x) ]
[  x′ y  ˘> x ∘ y  ]
[  x′ y′ z  ˘→ (x′ y)′ z ]
[  x ∘ y ∘ z ˘→ (x ∘ y) ∘ z ]

Parentheses (x) ¨= x are as usual. Prove the following:

(a) S lemma 2a : (K ∘ K ∘ K)′ u′ v′ w′ x ≡ u ^{·}.

(b) S lemma 2b : ((K ∘ K) ∘ K)′ u′ v′ w′ x ≡ (K ∘ (K ∘ K))′ u′ v′ w′ x ^{·}.

(c) S lemma 2c : ((K∘K∘K)∘(K∘K))′ u′ v′ w′ x′ y′ z ≡ ((K∘K)∘(K∘K∘K))′ u′ v′ w′ x′ y′ z ^{·}. (Hint: You can reduce the size of the proofs by inventing your own auxiliary lemmas).

Exercise 3. Which of the following hold? Prove those that hold. Give counterexamples to those that fail. For each use of Tautology ^{·} draw the corresponding truth table.

(a) x ∈ B → y ∈ B → x ≤ y ⇒ x < y ^{·}.

(b) x ∈ B → y ∈ B → x < y ⇒ x ≤ y ^{·}.

(c) x ∈ Z → if(x ∈ N, 1, 2) ∈ N ^{·}.

Exercise 4. I define

f(x, y) ≐ x = 0\{ \begin{matrix}y \\ f(x − 1, x) \end{matrix} .

(a) Compute f(100, 200) ^{·}.

(b) Prove ∀x∈N: ∀y∈N: f(x, y) ∈ N ^{·}.

(c) Prove ∃x∈N: f(x, x) = x ^{·}.

Exercise 1. Let A be shorthand for

(λx.λy.x′(x′ y))′(λx.λy.x′ y)′(λx.x + 1.4F)′ 10F

(a) Draw a syntax tree of A.

(b) Draw a binding diagram for A.

(c) Compute A.

Exercise 2. The algebraic system V ^{·} has the constructs ∗ ^{·}, ∘x ^{·}, {x} ^{·}, a ^{·}, b ^{·}, c ^{·}, x + y ^{·}, s(u, v, x, y) ^{·} and ⟨x | y:=z⟩ ^{·}, the contradiction ∗ ≡ ∘∗ ^{·}, and the following axioms:

A: a ≡ {∗} v_{∗∗}: s(∗, ∗, x, y) ≡ x v_{∘∘}: s(∘u, ∘v, x, y) ≡ s(u, v, x, y)
B: b ≡ {∘∗} v_{∗∘}: s(∗, ∘v, x, y) ≡ y S: ⟨{x} | {y}:=z⟩ ≡ s(x, y, z, {x})
C: c ≡ {∘∘∗} v_{∘∗}: s(∘u, ∗, x, y) ≡ y P: ⟨u+v | x:=y⟩ ≡ ⟨u | x:=y⟩+⟨v | x:=y⟩

Prove the following:

(a) V lemma 2a: ⟨a | b:=c⟩ ≡ a ^{·}.

(b) V lemma 2b: ⟨b | b:=c⟩ ≡ c ^{·}.

(c) V lemma 2c: ⟨a + b | b:=c⟩ ≡ a + c ^{·}.

Exercise 3. I define a ≐ Y′ λx.λy.x′ T .

(a) Prove Mac lemma 3a: a ⪯ λx.⊥ .

(b) Prove Mac lemma 3b: λx.⊥ ⪯ a .

(c) Prove Mac lemma 3c: a ≡ λx.⊥ .

Exercise 4. I define f(x, y) ≐ if(x = 0, y = 0, f(x − 1, y − 1)) .

(a) Prove Mac lemma 4a: x ∈ N → f(x, x) .

(b) Prove Mac lemma 4b: x ∈ N → (x = 0) ∈ F → ∀y∈Z: f(x − 1, y) ∈ B → ∀y∈Z: f(x, y) ∈ B .

(c) Prove Mac lemma 4c: x ∈ N → ∀y∈Z: f(x, y) ∈ B .

Exercise 1. Draw the parse trees of the three expressions below. If the expression is a term then draw the syntax tree and compute the value.

(a) 1, 2, 3 ≤ 3 < ⟨3⟩ head tail ⇒ T.

(b) ((1, 2 ≤ 3) < ⟨3⟩ head) ⇒ T.

(c) 1′ 2 ⇒ T.

Exercise 2. The algebraic system S ^{·} has the constructs x · y ^{·}, x + y ^{·}, −x ^{·}, ⟨x, y⟩ ^{·}, ⟨x; y⟩ ^{·}, 0 ^{·}, and 1 ^{·}. The only associativity rule is x·y·z ˘→ (x · y) · z , and the only priority rule is x · y ˘> x + y . The axioms are:

[S rule CommT: x · y ≡ y · x] [S rule MinusT: −(x · y) ≡ x · (−y)]
[S rule CommP: x+y ≡ y+x] [S rule ColT:  ⟨x, y⟩ · ⟨z; w⟩ ≡ x · z + y · w]
[S rule ZeroT: x · 0 ≡ 0]  [S rule RowT: x · ⟨y, z⟩ ≡ ⟨x · y, x · z⟩]
[S rule OneT: x · 1 ≡ x] [S rule RowP: ⟨x, y⟩+⟨z, w⟩ ≡ ⟨x+z, y+w⟩]
[S rule ZeroP: x + 0 ≡ x] [S rule Cancel: (−x) + x ≡ 0]
[S rule Nullary: nullary ≡ ⟨⟨0, 1⟩; ⟨−1, 0⟩⟩]

Prove the following:

(a) S lemma Orthogonal: ⟨a, b⟩ · nullary · ⟨a; b⟩ ≡ 0 ^{·}. Question 2a above constitutes 25% of the exam. All other questions constitute about 8%.

Exercise 3. Prove the following or give counterexamples. Draw a truth table for each use of Tautology.

(a) Mac lemma 3a: x ∈ B → y ∈ B → x + y = x · y .

(b) Mac lemma 3b: x ∈ B → y ∈ B → z ∈ B → x + (y + z) = (x + y) + z .

(c) Mac lemma 3c: x ∈ D → y ∈ D → z ∈ D → x + (y + z) = (x + y) + z .

Exercise 4. I define f(x) ≐ g(x, 0) and g(x, y) ≐ if(x = 0, y, g(x−1, x+y)) .

(a) Prove Mac lemma 4a: x ∈ N → ∀y∈N: g(x, y) ∈ N .

(b) Prove Mac lemma 4b: y ∈ N → x ∈ N → g(x, y) ∈ N .

(c) Prove Mac lemma 4c: x ∈ N → f(x) ∈ N .

Hint. Lemma 4b and 4c have comparatively short proofs. When solving 4b one may assume lemma 4a and when solving 4c one may assume lemma 4a and 4b.