Our site saves small pieces of text information (cookies) on your device in order to deliver better content and for statistical purposes. You can disable the usage of cookies by changing the settings of your browser. By browsing our website without changing the browser settings you grant us permission to store that information on your device.

# Homework 8

This is the task corresponding to homework 8.

## Resources

### Definitions File

```theory Defs
imports Complex_Main "HOL-Data_Structures.Tree23_Set" "HOL-Data_Structures.Set_Specs"
begin

fun size1 :: "'a tree23 \<Rightarrow> nat" where
"size1 \<langle>\<rangle> = 1"
| "size1 \<langle>l,_,r\<rangle> = size1 l + size1 r"
| "size1 \<langle>l,_,m,_,r\<rangle> = size1 l + size1 m + size1 r"

fun is_3_tree :: "'a tree23 \<Rightarrow> bool" where
"is_3_tree \<langle>\<rangle> = True"
| "is_3_tree \<langle>l,_,m,_,r\<rangle> = (is_3_tree l \<and> is_3_tree m \<and> is_3_tree r)"
| "is_3_tree _ = False"

type_synonym bv = "bool list"

definition bv_set :: "bv \<Rightarrow> nat set"
where "bv_set l = { i. i<length l \<and> l!i }"

end```

### Template File

```theory Submission
imports Defs
begin

theorem complete_3_tree_height: "complete t \<Longrightarrow> is_3_tree t \<longleftrightarrow> size1 t = 3^height t"
sorry

end```

### Check File

```theory Check
imports Submission
begin

theorem complete_3_tree_height: "complete t \<Longrightarrow> is_3_tree t \<longleftrightarrow> size1 t = 3^height t"
by (rule Submission.complete_3_tree_height)

end```

Terms and Conditions