equal
deleted
inserted
replaced
132 @{thm (lhs) injval.simps(4)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1"]} & $\dn$ & |
132 @{thm (lhs) injval.simps(4)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1"]} & $\dn$ & |
133 @{thm (rhs) injval.simps(4)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1"]}\\ |
133 @{thm (rhs) injval.simps(4)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1"]}\\ |
134 @{thm (lhs) injval.simps(5)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]} & $\dn$ & |
134 @{thm (lhs) injval.simps(5)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]} & $\dn$ & |
135 @{thm (rhs) injval.simps(5)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]}\\ |
135 @{thm (rhs) injval.simps(5)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]}\\ |
136 @{thm (lhs) injval.simps(6)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]} & $\dn$ |
136 @{thm (lhs) injval.simps(6)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]} & $\dn$ |
137 & @{thm (rhs) injval.simps(6)[of "r\<^sub>1" "c" "v\<^sub>1" "v\<^sub>2"]}\\ |
137 & @{thm (rhs) injval.simps(6)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]}\\ |
138 @{thm (lhs) injval.simps(7)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]} & $\dn$ |
138 @{thm (lhs) injval.simps(7)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]} & $\dn$ |
139 & @{thm (rhs) injval.simps(7)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]}\\ |
139 & @{thm (rhs) injval.simps(7)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]}\\ |
140 @{thm (lhs) injval.simps(8)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]} & $\dn$ |
140 @{thm (lhs) injval.simps(8)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]} & $\dn$ |
141 & @{thm (rhs) injval.simps(8)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]}\\ |
141 & @{thm (rhs) injval.simps(8)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]}\\ |
142 @{thm (lhs) injval.simps(9)[of "r" "c" "v" "vs"]} & $\dn$ |
142 @{thm (lhs) injval.simps(9)[of "r" "c" "v" "vs"]} & $\dn$ |
258 \mbox{}\bigskip |
258 \mbox{}\bigskip |
259 *} |
259 *} |
260 |
260 |
261 text {* |
261 text {* |
262 \noindent |
262 \noindent |
|
263 Things we have proved about our version of the Sulzmann ordering |
|
264 |
|
265 \begin{center} |
|
266 \begin{tabular}{c} |
|
267 @{thm[mode=IfThen] ValOrd_refl[of "v" "r"]}\medskip\\ |
|
268 @{thm[mode=IfThen] ValOrd_total[of "v\<^sub>1" "r" "v\<^sub>2"]} |
|
269 \end{tabular} |
|
270 \end{center}\bigskip |
|
271 |
|
272 \noindent |
263 Things we like to prove, but cannot:\bigskip |
273 Things we like to prove, but cannot:\bigskip |
264 |
274 |
265 If @{term "s \<in> r \<rightarrow> v\<^sub>1"}, @{term "\<turnstile> v\<^sub>2 : r"}, then @{term "v\<^sub>1 \<succ>r v\<^sub>2"} |
275 If @{term "s \<in> r \<rightarrow> v\<^sub>1"}, @{term "\<turnstile> v\<^sub>2 : r"}, then @{term "v\<^sub>1 \<succ>r v\<^sub>2"} |
266 |
276 |
267 *} |
277 *} |