equal
deleted
inserted
replaced
174 @{thm[mode=Axiom] PMatch.intros(1)} \qquad |
174 @{thm[mode=Axiom] PMatch.intros(1)} \qquad |
175 @{thm[mode=Axiom] PMatch.intros(2)}\medskip\\ |
175 @{thm[mode=Axiom] PMatch.intros(2)}\medskip\\ |
176 @{thm[mode=Rule] PMatch.intros(3)[of "s" "r\<^sub>1" "v" "r\<^sub>2"]}\qquad |
176 @{thm[mode=Rule] PMatch.intros(3)[of "s" "r\<^sub>1" "v" "r\<^sub>2"]}\qquad |
177 @{thm[mode=Rule] PMatch.intros(4)[of "s" "r\<^sub>2" "v" "r\<^sub>1"]}\medskip\\ |
177 @{thm[mode=Rule] PMatch.intros(4)[of "s" "r\<^sub>2" "v" "r\<^sub>1"]}\medskip\\ |
178 \multicolumn{1}{p{5cm}}{@{thm[mode=Rule] PMatch.intros(5)[of "s\<^sub>1" "r\<^sub>1" "v\<^sub>1" "s\<^sub>2" "r\<^sub>2" "v\<^sub>2"]}}\medskip\\ |
178 \multicolumn{1}{p{5cm}}{@{thm[mode=Rule] PMatch.intros(5)[of "s\<^sub>1" "r\<^sub>1" "v\<^sub>1" "s\<^sub>2" "r\<^sub>2" "v\<^sub>2"]}}\medskip\\ |
179 @{thm[mode=Rule] PMatch.intros(6)[of "s\<^sub>1" "r" "v" "s\<^sub>2" "vs"]} \qquad |
179 @{thm[mode=Rule] PMatch.intros(6)[of "s\<^sub>1" "r" "v" "s\<^sub>2" "vs"]}\medskip\\ |
180 @{thm[mode=Axiom] PMatch.intros(7)}\medskip\\ |
180 @{thm[mode=Axiom] PMatch.intros(7)}\medskip\\ |
181 \end{tabular} |
181 \end{tabular} |
182 \end{center} |
182 \end{center} |
183 |
183 |
184 \noindent |
184 \noindent |
247 |
247 |
248 @{thm[mode=IfThen] PMatch1(2)} |
248 @{thm[mode=IfThen] PMatch1(2)} |
249 |
249 |
250 @{thm[mode=IfThen] PMatch1N} |
250 @{thm[mode=IfThen] PMatch1N} |
251 |
251 |
|
252 @{thm[mode=IfThen] PMatch_determ(1)[of "s" "r" "v\<^sub>1" "v\<^sub>2"]} |
|
253 |
|
254 \medskip |
252 \noindent |
255 \noindent |
253 This is the main theorem that lets us prove that the algorithm is correct according to |
256 This is the main theorem that lets us prove that the algorithm is correct according to |
254 @{term "s \<in> r \<rightarrow> v"}: |
257 @{term "s \<in> r \<rightarrow> v"}: |
255 |
258 |
256 @{thm[mode=IfThen] PMatch2} |
259 @{thm[mode=IfThen] PMatch2} |