equal
deleted
inserted
replaced
6 by (unfold inj_on_def) blast |
6 by (unfold inj_on_def) blast |
7 |
7 |
8 lemma Ex1_eq: "\<exists>!x. P x \<Longrightarrow> P x \<Longrightarrow> P y \<Longrightarrow> x = y" |
8 lemma Ex1_eq: "\<exists>!x. P x \<Longrightarrow> P x \<Longrightarrow> P y \<Longrightarrow> x = y" |
9 by auto |
9 by auto |
10 |
10 |
11 section "Define the state space" |
11 subsection {* Define the state space *} |
12 |
12 |
13 text {* |
13 text {* |
14 |
14 |
15 We introduce the state space on which the algorithm operates. |
15 We introduce the state space on which the algorithm operates. |
16 |
16 |