author nipkow Tue, 25 Jul 2017 11:29:03 +0200 changeset 69868 00f70c27c44b parent 69867 bfc159ba9b26 child 69869 0bba9c6b2a17 child 69870 1f5cd3af3d78
.
 Exercises/exam.pdf file | annotate | diff | comparison | revisions Exercises/exam/Q_Induction.thy file | annotate | diff | comparison | revisions
`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"```