###### Cookies disclaimer

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.

# Exercise 1 (Inductive Paths)

This is the task corresponding to exercise 1.

## Resources

Download Files

### Definitions File

```theory Defs imports Main begin

inductive path :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> bool" for r where
path0: "path r x 0 x" |
path1: "r x y \<Longrightarrow> path r y n z \<Longrightarrow> path r x (Suc n) z"

end```

### Template File

```theory Submission imports Defs begin

lemma Q1: "path r x m y \<Longrightarrow> path r y n z \<Longrightarrow> path r x (m+n) z"
sorry

lemma Q2: "path r x n y \<Longrightarrow> path R y n x"
oops

lemma Q3: "path r x k x \<Longrightarrow> path r x (n*k) x"
sorry

end```

### Check File

```theory Check imports Submission begin

theorem Q1: "path r x m y \<Longrightarrow> path r y n z \<Longrightarrow> path r x (m+n) z"
by (rule Submission.Q1)

theorem Q3: "path r x k x \<Longrightarrow> path r x (n*k) x"
by (rule Submission.Q3)

end```

Terms and Conditions