lexing: thys/notes.tex@7093e600ec2c (annotated)

55 c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1	\documentclass[11pt]{article}
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	2
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	3	\begin{document}
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	4
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	5	\noindent
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	6	A lemma which might be true, but can also be false, is as follows:
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	7
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	8	\begin{center}
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	9	\begin{tabular}{lll}
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	10	If & (1) & $v_1 \succ_{der\;c\;r} v_2$,\\
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	11	& (2) & $\vdash v_1 : der\;c\;r$, and\\
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	12	& (3) & $\vdash v_2 : der\;c\;r$ holds,\\
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	13	then & & $inj\;r\;c\;v_1 \succ_r inj\;r\;c\;v_2$ also holds.
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	14	\end{tabular}
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	15	\end{center}
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	16
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	17	\noindent It essentially states that if one value $v_1$ is
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	18	bigger than $v_2$ then this ordering is preserved under
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	19	injections. This is proved by induction (on the definition of
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	20	$der$\ldots this is very similar to an induction on $r$).
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	21	\bigskip
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	22
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	23	\noindent
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	24	The case that is still unproved is the sequence case where we
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	25	assume $r = r_1\cdot r_2$ and also $r_1$ being nullable.
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	26	The derivative $der\;c\;r$ is then
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	27
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	28	\begin{center}
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	29	$der\;c\;r = ((der\;c\;r_1) \cdot r_2) + (der\;c\;r_2)$
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	30	\end{center}
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	31
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	32	\noindent
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	33	or without the parentheses
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	34
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	35	\begin{center}
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	36	$der\;c\;r = (der\;c\;r_1) \cdot r_2 + der\;c\;r_2$
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	37	\end{center}
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	38
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	39	\noindent
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	40	In this case the assumptions are
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	41
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	42	\begin{center}
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	43	\begin{tabular}{ll}
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	44	(a) & $v_1 \succ_{(der\;c\;r_1) \cdot r_2 + der\;c\;r_2} v_2$\\
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	45	(b) & $\vdash v_1 : (der\;c\;r_1) \cdot r_2 + der\;c\;r_2$\\
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	46	(c) & $\vdash v_2 : (der\;c\;r_1) \cdot r_2 + der\;c\;r_2$\\
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	47	(d) & $nullable(r_1)$
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	48	\end{tabular}
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	49	\end{center}
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	50
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	51	\noindent
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	52	The induction hypotheses are
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	53
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	54	\begin{center}
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	55	\begin{tabular}{ll}
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	56	(IH1) & $\forall v_1 v_2.\;v_1 \succ_{der\;c\;r_1} v_2
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	57	\;\wedge\; \vdash v_1 : der\;c\;r_1 \;\wedge\;
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	58	\vdash v_2 : der\;c\;r_1\qquad$\\
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	59	& $\hfill\longrightarrow
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	60	inj\;r_1\;c\;v_1 \succ{r_1} \;inj\;r_1\;c\;v_2$\smallskip\\
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	61	(IH2) & $\forall v_1 v_2.\;v_1 \succ_{der\;c\;r_2} v_2
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	62	\;\wedge\; \vdash v_2 : der\;c\;r_2 \;\wedge\;
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	63	\vdash v_2 : der\;c\;r_2\qquad$\\
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	64	& $\hfill\longrightarrow
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	65	inj\;r_2\;c\;v_1 \succ{r_2} \;inj\;r_2\;c\;v_2$\\
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	66	\end{tabular}
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	67	\end{center}
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	68
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	69	\noindent
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	70	The goal is
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	71
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	72	\[
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	73	(goal)\qquad
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	74	inj\; (r_1 \cdot r_2)\;c\;v_1 \succ_{r_1 \cdot r_2}
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	75	inj\; (r_1 \cdot r_2)\;c\;v_2
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	76	\]
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	77
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	78	\noindent
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	79	If we analyse how (a) could have arisen (that is make a case
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	80	distinction), then we will find four cases:
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	81
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	82	\begin{center}
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	83	\begin{tabular}{ll}
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	84	LL & $v_1 = Left(w_1)$, $v_2 = Left(w_2)$\\
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	85	LR & $v_1 = Left(w_1)$, $v_2 = Right(w_2)$\\
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	86	RL & $v_1 = Right(w_1)$, $v_2 = Left(w_2)$\\
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	87	RR & $v_1 = Right(w_1)$, $v_2 = Right(w_2)$\\
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	88	\end{tabular}
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	89	\end{center}
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	90
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	91
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	92	\noindent
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	93	We have to establish our goal in all four cases.
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	94
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	95
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	96	\subsubsection*{Case LR}
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	97
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	98	The corresponding rule (instantiated) is:
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	99
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	100	\begin{center}
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	101	\begin{tabular}{c}
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	102	$len\,\|w_1\| \geq len\,\|w_2\|$\\
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	103	\hline
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	104	$Left(w_1) \succ_{(der\;c\;r_1) \cdot r_2 + der\;c\;r_2} Right(w_2)$
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	105	\end{tabular}
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	106	\end{center}
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	107
57 7093e600ec2c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 55 diff changeset	108	\noindent
7093e600ec2c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 55 diff changeset	109	This means we can also assume in this case
7093e600ec2c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 55 diff changeset	110
7093e600ec2c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 55 diff changeset	111	\[
7093e600ec2c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 55 diff changeset	112	(e)\quad len\,\|w_1\| \geq len\,\|w_2\|
7093e600ec2c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 55 diff changeset	113	\]
7093e600ec2c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 55 diff changeset	114
7093e600ec2c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 55 diff changeset	115	\noindent
7093e600ec2c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 55 diff changeset	116	which is the premise of the rule above.
7093e600ec2c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 55 diff changeset	117	Instantiating $v_1$ and $v_2$ in the assumptions (b) and (c)
7093e600ec2c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 55 diff changeset	118	gives us
7093e600ec2c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 55 diff changeset	119
7093e600ec2c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 55 diff changeset	120	\begin{center}
7093e600ec2c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 55 diff changeset	121	\begin{tabular}{ll}
7093e600ec2c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 55 diff changeset	122	(b*) & $\vdash Left(w_1) : (der\;c\;r_1) \cdot r_2 + der\;c\;r_2$\\
7093e600ec2c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 55 diff changeset	123	(c*) & $\vdash Right(w_2) : (der\;c\;r_1) \cdot r_2 + der\;c\;r_2$\\
7093e600ec2c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 55 diff changeset	124	\end{tabular}
7093e600ec2c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 55 diff changeset	125	\end{center}
7093e600ec2c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 55 diff changeset	126
7093e600ec2c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 55 diff changeset	127	\noindent Since these are assumptions, we can further analyse
7093e600ec2c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 55 diff changeset	128	how they could have arisen according to the rules of $\vdash
7093e600ec2c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 55 diff changeset	129	\_ : \_\,$. This gives us two new assumptions
7093e600ec2c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 55 diff changeset	130
7093e600ec2c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 55 diff changeset	131	\begin{center}
7093e600ec2c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 55 diff changeset	132	\begin{tabular}{ll}
7093e600ec2c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 55 diff changeset	133	(b**) & $\vdash w_1 : (der\;c\;r_1) \cdot r_2$\\
7093e600ec2c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 55 diff changeset	134	(c**) & $\vdash w_2 : der\;c\;r_2$\\
7093e600ec2c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 55 diff changeset	135	\end{tabular}
7093e600ec2c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 55 diff changeset	136	\end{center}
7093e600ec2c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 55 diff changeset	137
7093e600ec2c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 55 diff changeset	138	\noindent
7093e600ec2c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 55 diff changeset	139	Looking at (b**) we can further analyse how this
7093e600ec2c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 55 diff changeset	140	judgement could have arisen. This tells us that $w_1$
7093e600ec2c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 55 diff changeset	141	must have been a sequence, say $u_1\cdot u_2$, with
7093e600ec2c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 55 diff changeset	142
7093e600ec2c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 55 diff changeset	143	\begin{center}
7093e600ec2c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 55 diff changeset	144	\begin{tabular}{ll}
7093e600ec2c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 55 diff changeset	145	(b***) & $\vdash u_1 : der\;c\;r_1$\\
7093e600ec2c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 55 diff changeset	146	& $\vdash u_2 : r_2$\\
7093e600ec2c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 55 diff changeset	147	\end{tabular}
7093e600ec2c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 55 diff changeset	148	\end{center}
7093e600ec2c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 55 diff changeset	149
7093e600ec2c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 55 diff changeset	150	\noindent
7093e600ec2c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 55 diff changeset	151	Instantiating the goal means we need to prove
7093e600ec2c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 55 diff changeset	152
7093e600ec2c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 55 diff changeset	153	\[
7093e600ec2c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 55 diff changeset	154	inj\; (r_1 \cdot r_2)\;c\;(Left(u_1\cdot u_2)) \succ_{r_1 \cdot r_2}
7093e600ec2c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 55 diff changeset	155	inj\; (r_1 \cdot r_2)\;c\;(Right(w_2))
7093e600ec2c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 55 diff changeset	156	\]
7093e600ec2c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 55 diff changeset	157
7093e600ec2c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 55 diff changeset	158	\noindent
7093e600ec2c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 55 diff changeset	159	We can simplify this according to the rules of $inj$:
7093e600ec2c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 55 diff changeset	160
7093e600ec2c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 55 diff changeset	161	\[
7093e600ec2c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 55 diff changeset	162	(inj\; r_1\;c\;u_1)\cdot u_2 \succ_{r_1 \cdot r_2}
7093e600ec2c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 55 diff changeset	163	(mkeps\;r_1) \cdot (inj\; r_2\;c\;w_2)
7093e600ec2c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 55 diff changeset	164	\]
7093e600ec2c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 55 diff changeset	165
7093e600ec2c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 55 diff changeset	166	\noindent
7093e600ec2c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 55 diff changeset	167	This is what we need to prove.
7093e600ec2c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 55 diff changeset	168
7093e600ec2c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 55 diff changeset	169
55 c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	170	\subsubsection*{Case RL}
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	171
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	172	The corresponding rule (instantiated) is:
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	173
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	174	\begin{center}
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	175	\begin{tabular}{c}
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	176	$len\,\|w_1\| > len\,\|w_2\|$\\
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	177	\hline
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	178	$Right(w_1) \succ_{(der\;c\;r_1) \cdot r_2 + der\;c\;r_2} Left(w_2)$
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	179	\end{tabular}
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	180	\end{center}
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	181
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	182
c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	183	\end{document}

author	Christian Urban <christian dot urban at kcl dot ac dot uk>
	Fri, 30 Jan 2015 11:42:53 +0000
changeset 57	7093e600ec2c
parent 55	c33cfa1e813a
child 58	1769b702d4dc
permissions	-rw-r--r--