equal
deleted
inserted
replaced
84 following induction principle. |
84 following induction principle. |
85 |
85 |
86 \begin{center}\small |
86 \begin{center}\small |
87 \mprset{flushleft} |
87 \mprset{flushleft} |
88 \mbox{\inferrule{ |
88 \mbox{\inferrule{ |
89 @{thm_style prem1 trcl\<iota>\<iota>.induct[where P=P, where z=R, where za=x, where zb=y]}\\\\ |
89 @{thm (prem1) trcl\<iota>\<iota>.induct[where P=P, where z=R, where za=x, where zb=y]}\\\\ |
90 @{thm_style prem2 trcl\<iota>\<iota>.induct[where P=P, where z=R, where za=x, where zb=y]}\\\\ |
90 @{thm (prem2) trcl\<iota>\<iota>.induct[where P=P, where z=R, where za=x, where zb=y]}\\\\ |
91 @{thm_style prem3 trcl\<iota>\<iota>.induct[where P=P, where z=R, where za=x, where zb=y]}} |
91 @{thm (prem3) trcl\<iota>\<iota>.induct[where P=P, where z=R, where za=x, where zb=y]}} |
92 {@{thm_style concl trcl\<iota>\<iota>.induct[where P=P, where z=R, where za=x, where zb=y]}}} |
92 {@{thm (concl) trcl\<iota>\<iota>.induct[where P=P, where z=R, where za=x, where zb=y]}}} |
93 \end{center} |
93 \end{center} |
94 |
94 |
95 But this does not correspond to the induction principle we derived by hand, which |
95 But this does not correspond to the induction principle we derived by hand, which |
96 was |
96 was |
97 |
97 |