1010 \begin{center} |
1010 \begin{center} |
1011 \begin{tabular}{@ {}cc@ {}} |
1011 \begin{tabular}{@ {}cc@ {}} |
1012 \begin{tabular}{@ {}ll@ {}} |
1012 \begin{tabular}{@ {}ll@ {}} |
1013 IH $r_1$:\\ |
1013 IH $r_1$:\\ |
1014 $\forall v_1, v_2, v_3.$ |
1014 $\forall v_1, v_2, v_3.$ |
1015 & $\vdash v_1 : r_1\;\wedge$\\ |
1015 & $v_1 : r_1\;\wedge$\\ |
1016 & $\vdash v_2 : r_1\;\wedge$\\ |
1016 & $v_2 : r_1\;\wedge$\\ |
1017 & $\vdash v_3 : r_1\;\wedge$\\ |
1017 & $v_3 : r_1\;\wedge$\\ |
1018 & $|v_1|=|v_2|=|v_3|\;\wedge$\\ |
1018 & $|v_1|=|v_2|=|v_3|\;\wedge$\\ |
1019 & $v_1 \posix^{r_1} v_2\;\wedge\; v_2 \posix^{r_1} v_3$\medskip\\ |
1019 & $v_1 \posix_{r_1} v_2\;\wedge\; v_2 \posix_{r_1} v_3$\medskip\\ |
1020 & $\;\;\Rightarrow v_1 \posix^{r_1} v_3$ |
1020 & $\;\;\Rightarrow v_1 \posix_{r_1} v_3$ |
1021 \end{tabular} & |
1021 \end{tabular} & |
1022 \begin{tabular}{@ {}ll@ {}} |
1022 \begin{tabular}{@ {}ll@ {}} |
1023 IH $r_2$:\\ |
1023 IH $r_2$:\\ |
1024 $\forall v_1, v_2, v_3.$ |
1024 $\forall v_1, v_2, v_3.$ |
1025 & $\vdash v_1 : r_2\;\wedge$\\ |
1025 & $v_1 : r_2\;\wedge$\\ |
1026 & $\vdash v_2 : r_2\;\wedge$\\ |
1026 & $v_2 : r_2\;\wedge$\\ |
1027 & $\vdash v_3 : r_2\;\wedge$\\ |
1027 & $v_3 : r_2\;\wedge$\\ |
1028 & $|v_1|=|v_2|=|v_3|\;\wedge$\\ |
1028 & $|v_1|=|v_2|=|v_3|\;\wedge$\\ |
1029 & $v_1 \posix^{r_2} v_2\;\wedge\; v_2 \posix^{r_2} v_3$\medskip\\ |
1029 & $v_1 \posix_{r_2} v_2\;\wedge\; v_2 \posix_{r_2} v_3$\medskip\\ |
1030 & $\;\;\Rightarrow v_1 \posix^{r_2} v_3$ |
1030 & $\;\;\Rightarrow v_1 \posix_{r_2} v_3$ |
1031 \end{tabular} |
1031 \end{tabular} |
1032 \end{tabular} |
1032 \end{tabular} |
1033 \end{center} |
1033 \end{center} |
1034 |
1034 |
1035 \noindent |
1035 \noindent |