. draft
authornipkow
Tue, 25 Jul 2017 11:29:03 +0200
changeset 69868 00f70c27c44b
parent 69867 bfc159ba9b26
child 69869 0bba9c6b2a17
child 69870 1f5cd3af3d78
.
Exercises/exam.pdf
Exercises/exam/Q_Induction.thy
Binary file Exercises/exam.pdf has changed
--- a/Exercises/exam/Q_Induction.thy	Tue Jul 25 11:22:03 2017 +0200
+++ b/Exercises/exam/Q_Induction.thy	Tue Jul 25 11:29:03 2017 +0200
@@ -21,8 +21,8 @@
 "lvs (Nd r s t) = lvs r + lvs s + lvs t"
 
 text \<open>There is a linear relationship between the size (\<open>sz\<close>) and the number of
-leaves (\<open>lvs\<close>). Find a linear function \<open>f :: nat \<Rightarrow> nat\<close> such that
-\<open>lfs t = f (sz t)\<close> and prove this property.\<close>
+leaves (\<open>lvs\<close>) of a tree. Find this relationship and prove \<open>lfs t = a * sz t + b\<close>
+for the correct \<open>a\<close> and \<open>b\<close>.\<close>
 
 (*<*)
 lemma "lvs t = 2 * sz t + 1"