916 Their central definition is an ``ordering relation'' defined by the |
916 Their central definition is an ``ordering relation'' defined by the |
917 rules (slightly adapted to fit our notation): |
917 rules (slightly adapted to fit our notation): |
918 |
918 |
919 \begin{center} |
919 \begin{center} |
920 \begin{tabular}{@ {}c@ {\hspace{4mm}}c@ {}} |
920 \begin{tabular}{@ {}c@ {\hspace{4mm}}c@ {}} |
921 @{thm[mode=Rule] C2[of "v\<^sub>1" "r\<^sub>1" "v\<^sub>1'" "v\<^sub>2" "r\<^sub>2" "v\<^sub>2'"]}(C2) & |
921 @{thm[mode=Rule] C2[of "v\<^sub>1" "r\<^sub>1" "v\<^sub>1\<iota>" "v\<^sub>2" "r\<^sub>2" "v\<^sub>2\<iota>"]}\,(C2) & |
922 @{thm[mode=Rule] C1[of "v\<^sub>2" "r\<^sub>2" "v\<^sub>2'" "v\<^sub>1" "r\<^sub>1"]}(C1)\smallskip\\ |
922 @{thm[mode=Rule] C1[of "v\<^sub>2" "r\<^sub>2" "v\<^sub>2\<iota>" "v\<^sub>1" "r\<^sub>1"]}\,(C1)\smallskip\\ |
923 |
923 |
924 @{thm[mode=Rule] A1[of "v\<^sub>1" "v\<^sub>2" "r\<^sub>1" "r\<^sub>2"]}(A1) & |
924 @{thm[mode=Rule] A1[of "v\<^sub>1" "v\<^sub>2" "r\<^sub>1" "r\<^sub>2"]}\,(A1) & |
925 @{thm[mode=Rule] A2[of "v\<^sub>2" "v\<^sub>1" "r\<^sub>1" "r\<^sub>2"]}(A2)\smallskip\\ |
925 @{thm[mode=Rule] A2[of "v\<^sub>2" "v\<^sub>1" "r\<^sub>1" "r\<^sub>2"]}\,(A2)\smallskip\\ |
926 |
926 |
927 @{thm[mode=Rule] A3[of "v\<^sub>1" "r\<^sub>2" "v\<^sub>2" "r\<^sub>1"]}(A3) & |
927 @{thm[mode=Rule] A3[of "v\<^sub>1" "r\<^sub>2" "v\<^sub>2" "r\<^sub>1"]}\,(A3) & |
928 @{thm[mode=Rule] A4[of "v\<^sub>1" "r\<^sub>1" "v\<^sub>2" "r\<^sub>2"]}(A4)\smallskip\\ |
928 @{thm[mode=Rule] A4[of "v\<^sub>1" "r\<^sub>1" "v\<^sub>2" "r\<^sub>2"]}\,(A4)\smallskip\\ |
929 |
929 |
930 @{thm[mode=Rule] K1[of "v" "vs" "r"]}(K1) & |
930 @{thm[mode=Rule] K1[of "v" "vs" "r"]}\,(K1) & |
931 @{thm[mode=Rule] K2[of "v" "vs" "r"]}(K2)\smallskip\\ |
931 @{thm[mode=Rule] K2[of "v" "vs" "r"]}\,(K2)\smallskip\\ |
932 |
932 |
933 @{thm[mode=Rule] K3[of "v\<^sub>1" "r" "v\<^sub>2" "vs\<^sub>1" "vs\<^sub>2"]}(K3) & |
933 @{thm[mode=Rule] K3[of "v\<^sub>1" "r" "v\<^sub>2" "vs\<^sub>1" "vs\<^sub>2"]}\,(K3) & |
934 @{thm[mode=Rule] K4[of "vs\<^sub>1" "r" "vs\<^sub>2" "v"]}(K4) |
934 @{thm[mode=Rule] K4[of "vs\<^sub>1" "r" "vs\<^sub>2" "v"]}\,(K4) |
935 \end{tabular} |
935 \end{tabular} |
936 \end{center} |
936 \end{center} |
937 |
937 |
938 \noindent The idea behind the rules (A1) and (A2), for example, is that a |
938 \noindent The idea behind the rules (A1) and (A2), for example, is that a |
939 @{text Left}-value is bigger than a @{text Right}-value, if the underlying |
939 @{text Left}-value is bigger than a @{text Right}-value, if the underlying |