File #1: atoe-tcsJH.tex
File #2: atoe-tcsJG.tex

Nonmatching lines (File "atoe-tcsJH.tex"; Line 1410:1411; File "atoe-tcsJG.tex"; Line 1410:1411)
1410	It remains to note that [FD] and the other family axioms except [FFD]
1411	are satisfied too. Note that the DRS $\calR$ is stable.

1410	It remains to note that [FD] and the other family axioms but [FFD]
1411	 are satisfied too. Note that the DRS $\calR$ is stable.


Extra lines in 1st before 1969 in 2nd (File "atoe-tcsJH.tex"; Line 1969:1971; File "atoe-tcsJG.tex"; Line Æ1969)
1969	\john{The phrase "exactly as the correctness of" above does not make sense.
1970	Please rephrase. (I don't know what you mean, so I cannot choose a better
1971	phrase).}


Nonmatching lines (File "atoe-tcsJH.tex"; Line 2013; File "atoe-tcsJG.tex"; Line 2010)
2013	Note that if $P\staeq P'$, then $Pv$ is canonical iff so is $P'v$. So the

2010	Note that if $P\staeq P'$, then $Pv$ is canonical iff so is $P'v$. So


Nonmatching lines (File "atoe-tcsJH.tex"; Line 2026; File "atoe-tcsJG.tex"; Line 2023)
2026	extraction procedure from $P'u'$. Now, if the last step, say $w$, of

2023	extraction procedure from $P'u'$. Now, if the last step, call it $w$, of


Nonmatching lines (File "atoe-tcsJH.tex"; Line 2212; File "atoe-tcsJG.tex"; Line 2209)
2212	$P/Q$ coincides with $v$, i.e., $P/Q=v$. Thus $P$ contracts a redex $v''$

2209	$P/Q$ coincides with $v$, i..e., $P/Q=v$. Thus $P$ contracts a redex $v''$


Nonmatching lines (File "atoe-tcsJH.tex"; Line 2379:2380; File "atoe-tcsJG.tex"; Line 2376:2378)
2379	
2380	\section{Affine Zig-Zag and Separable Families}

2376	\john{Checked to here now.}
2377	
2378	\section{Affine Zig-zag and Separable Families}


Nonmatching lines (File "atoe-tcsJH.tex"; Line 2427:2428; File "atoe-tcsJG.tex"; Line 2425:2426)
2427	As already mentioned in the introduction, non-separable families (not using
2428	that name) for Interaction Systems are studied in~\cite{[AL]}, where it is

2425	As already mentioned in the introduction, non-separable families (without
2426	the name) are studied in~\cite{[AL]} for Interaction Systems, where it is


Extra lines in 1st before 2440 in 2nd (File "atoe-tcsJH.tex"; Line 2442:2444; File "atoe-tcsJG.tex"; Line Æ2440)
2442	\john{Does linear need more motivation? It was introduced briefly earlier
2443	on but here we seem to say no nesting of redexes (which presumably implies
2444	linearity).}


Nonmatching lines (File "atoe-tcsJH.tex"; Line 2448; File "atoe-tcsJG.tex"; Line 2443)
2448	$\lambda_{LV}$~\cite{[Plo75]}, which is obtained from the \lc\ by allowing

2443	$\lambda_{LV}$~\cite{[Plo75]}. It is obtained from the \lc\ by allowing


Nonmatching lines (File "atoe-tcsJH.tex"; Line 2526; File "atoe-tcsJG.tex"; Line 2521)
2526	Let $Q^*:t\dored{P}s\red{u}e$ where $u$ creates $v\subt e$. Then, for any

2521	Let $Q^*:t\dored{P}s\red{u}e$ and $u$ create $v\subt e$. Then, for any


Nonmatching lines (File "atoe-tcsJH.tex"; Line 2564; File "atoe-tcsJG.tex"; Line 2559)
2564	Let $Q:e\dored{P}t\red{u}s$ where $u$ creates $v\subt s$. Then

2559	Let $Q:e\dored{P}t\red{u}s$ and let $u$ create $v\subt s$. Then


Nonmatching lines (File "atoe-tcsJH.tex"; Line 2622; File "atoe-tcsJG.tex"; Line 2617)
2622	Lemmas~\ref{L.dec.fam.ex.} and~\ref{L.dif.re.sa.his.} allow us to obtain

2617	Lemmas~\ref{L.dec.fam.ex.} and ~\ref{L.dif.re.sa.his.} allow us to obtain


Nonmatching lines (File "atoe-tcsJH.tex"; Line 2861:2862; File "atoe-tcsJG.tex"; Line 2856:2857)
2861	\john{That section is very heavy! Maybe the reader needs to be warned.}
2862	

2856	
2857	


Nonmatching lines (File "atoe-tcsJH.tex"; Line 2867; File "atoe-tcsJG.tex"; Line 2862)
2867	whose reduction steps correspond to complete family-reductions in $\calF$,

2862	whose reductions correspond to complete family-reductions in $\calF$,


Nonmatching lines (File "atoe-tcsJH.tex"; Line 2875:2877; File "atoe-tcsJG.tex"; Line 2870:2871)
2875	\john{Do we call it L\'evy-implementation because he introduced the
2876	idea? If not, I would leave it out.}
2877	

2870	
2871	


Nonmatching lines (File "atoe-tcsJH.tex"; Line 2886; File "atoe-tcsJG.tex"; Line 2880)
2886	each edge (i.e., reduction step) being a multi-step contracting a family

2880	each edge (i.e., a reduction step) being a multi-step contracting a family


Nonmatching lines (File "atoe-tcsJH.tex"; Line 2941; File "atoe-tcsJG.tex"; Line 2935)
2941	viewed as reductions in $\calF$ (by considering multi-steps as

2935	viewed as reduction in $\calF$ (by considering multi-steps as


Nonmatching lines (File "atoe-tcsJH.tex"; Line 2978:2979; File "atoe-tcsJG.tex"; Line 2972:2973)
2978	Qu$ iff $P'v'\fami  Q'u'$, where $P'$ and $Q'$ are reductions in
2979	$\calR$ corresponding to $P$ and $Q$, and $v'$ and $u'$ are

2972	Qu$ iff $P'v'\fami  Q'u'$, where $P'$ and $Q'$ are (any) reductions in
2973	$\calR$ corresponding to $P$ and $Q$, and $v'$ and $u'$ are any


Extra lines in 2nd before 3046 in 1st (File "atoe-tcsJH.tex"; Line Æ3046; File "atoe-tcsJG.tex"; Line 3040)
3040	\el


Extra lines in 1st before 3069 in 2nd (File "atoe-tcsJH.tex"; Line 3074; File "atoe-tcsJG.tex"; Line Æ3069)
3074	\el


Nonmatching lines (File "atoe-tcsJH.tex"; Line 3106:3109; File "atoe-tcsJG.tex"; Line 3100:3102)
3106	which was used earlier by L\'evy in~\cite{[levy],[le80]}. It would be
3107	interesting to investigate whether it is possible to prove our second theorem
3108	in the context of stable DRS, without invoking family axioms, but possibly
3109	using some much

3100	which was used already by L\'evy in~\cite{[levy],[le80]}. It would be
3101	interesting to investigate whether it is possible to prove our second theorem
3102	already for stable DRSs, i.e., without family axioms, but possibly some much


Nonmatching lines (File "atoe-tcsJH.tex"; Line 3121:3122; File "atoe-tcsJG.tex"; Line 3114:3115)
3121	two different members of the same family simultaneously. Finally, we have
3122	shown that sharing is compositional. In particular, any

3114	simultaneously two different members of the same family. Finally, we have
3115	shown that sharing is (de)compositional. In particular, any


*** EOF on both files at the same time ***