From c21e25cf6b13b01af1fbd84b23f91f30cf20ad0c Mon Sep 17 00:00:00 2001
From: navid <navid>
Date: Wed, 17 Sep 2008 17:51:18 +0000
Subject: [PATCH] *** empty log message ***

---
 Robust/Transactions/Notes/sysgurantees.dvi | Bin 35100 -> 33064 bytes
 Robust/Transactions/Notes/sysgurantees.tex |  32 ++++++++++-----------
 2 files changed, 16 insertions(+), 16 deletions(-)

diff --git a/Robust/Transactions/Notes/sysgurantees.dvi b/Robust/Transactions/Notes/sysgurantees.dvi
index 3e9ee9f850bd5d72a929a36e8631d17eac7f9f19..d47df79c63d3ca5f958e03df7a5460fa13fb832f 100644
GIT binary patch
delta 3271
zcmZuz4Qw3M5x(2qvz-{H3c-H_lAN6ooA~?}J26KZVu(@)8XW8xH-##Bcl(Z8cW?Ky
zyJyD`dJ!s6wTk8KsF!VyHdsy_hyEz!(yFVv^sp&KX+zZ?DOJ^&qEb|lP$~3BsZ`Q=
zyL-N~WXn4H-p<av`R1E%=7q0wv(Ipon=5yQJKDS3zvlD#{1A+6etEFA+P?$7Sgm|!
zZ<|JmnC17js>#U%i&P_qq$)rZ5%L6VNw)}$X_7&q^m&WP5C5)UgMTdu)-<NsVV+D(
zoibZ}K0B$=C>5!m<<o!7M@&BbuHBR;8GiNog&^c3cC#hLGI$zQ6G?eoQl7BJBqMI^
zr7`G6|Ib_bh#Oy))o)x1jsX=dLuGI1lv+ldy7$uY&<&aP<+W31{pX&1Rhlr%4*cCt
z5RqoN_o^e4mxALa_g+n&*sZ4U?fHIuTN{&figDI_l#diH<vw26XWp!#s%ELo%t{hT
z(=9c|9F$^!XPU*p3px1c6FqL?Mw}QKekLZWpr{7uaiUSssII28DAf_wLNp9J6SEnL
zAJ%N7CjWM{BZQxk*9S5;lQsn`ix6x(kkSoP2(}JVpw<D^{W1U)qCgeHdO%G`23AL8
zHp8q?rth~?cGwIIUfUmI?()Rs<^L>n;^)6Xu5Ao(pFC>Bp}A)L<0ilHV@ZK1(Wz7I
zIMGe+li>v7m68o9DN`s^QCBtH$ps4qr8r01?Iw|8rd0GQPxK5wI{@qI2G-7AMF^EF
zKRYPJfXFhyXx%11z@Kle4ON`&w_Chd5R^b|qm6~tp;%d91vCS-4UsdjSXZ}Z&6^)!
z8i8Y7`F^A-aP{qN!!2{Ro{Cy=e2o~8Kjac%WWrqabjZehya4Dl!*93;j@EDEHuS)$
z`o=28bG_Ajo|~_Khllfb4hZL}zIg_2+<DADl~Xn({Q^G^J9GQ)+T(AYJJA!$@^er1
zn*7|TPLHLi62-QNSq9M*okZQn(WnI%x32eF@T;w<bcWyc9p`2uO<*_!+l%TZzv~>!
zQYQ%tku%tJae|PKN~#9L1t4M-&zQLyb8ty&>Ju7C;H{Bs_xXGesG6qAL>o7eN}XX-
zxPJZhp=1{6qbeEx{r7=39UUnPKIJkR8|e%-lAaOzx}^lAqJ+1R$04Sv31EHK!}{J7
z`gX7{_q3X23lAQOOFH1MjHVj0LA6FLs(7fyR4sv39cTU0Dosqm|C$<C4WwkmdM4HZ
z@ogtVFA0MZ!j$26|Il%o<#%7Eik`xTV1%&LB+K7b9UZRr*Vk4q@&)a{oK+n=WA|lb
z>5<L#>+Ge>ohaPDZgj%w?k_i<_#Pr#r~xX@iSIHp7)3RB`#IRXV*|QceSX=g&G_js
zGeH^cBaQ~Lc6Yh-#t&XaeZm$)c6&+NdR$G(B1_S0j#AoH+>(UvhwkuC!PU@79&O-Y
zYh4-zsl0NJEvn4D?&!kG?>cgTS3+WyaJfAB@<Nc^y>N#9c=3-#H1@|bLe~+@1*Hay
zh23ZhT}KHp?Lvm8p@|7qOI8@Z?ub=0Ak~_je_Kppc#%DAZn2nFvHmWom6vg$-4*Pr
zhks;CNUfO|Be3D<GHNn@E#lw8sH!a8AMXlxZ&{r#wkBd^lW0`cL>A0Y9q#RPW{yj|
z0=+RU{@Q|*mdRh6XF`h2jvS6Jn?^dy_&c|EgnBI_i)Jz<x`E!7*;r{d&RCwh!*{DR
zsgvt4sY0?$TMjNUry@}4$Wm5#u^lgx5nk+Y<=zn|a7N3DBN9}lG)7?6>_MD=IQ9Te
zbk?PX#p$>=)<%J9UU1#%6`|pmg+il{Rea_5IEG;a=Rj6yxI!33)s%s_SuQmha26@T
z>5R}WtZVOIysIK`7Mn#H4S9jmRWyp6&Inf?Hzd?$&y$1_MHB?sXfXrp4tqo-rf}s8
zc9gN+p>CWo5kPN5bX2JX5YK%CU5sah<6GGbcQoaAQxx^j5lzdG$J5TdS+O4?rf|Fo
zqbU}0N|aDm8A*_BMAuV^BvaW!sfv_ZsYA-kKVswlPp|b4nEZ5YXDGu@*Z1NynyypR
zrOQs9SXlp3!m?MrtPtixJCx2nX2C{x=|+GXi+3}pM-G#cDwh9D_SolmOXDt(;SWcU
z5J=wm8>Q`l=Y;h^cNPs;4E$nsJAf6Yv9lYovNL==6ur<`=Vj7F>=tnAh>)VfxuD*+
z0;&k|@)5ccsGjV=#!#5Uc}mvY0r~AuZedf?S^FHR%<#=Gl?XzXZ@$1-3;mz2-isBv
zy#HYpZ!!i;S>p}|8qN*aj%eKfg3|`Ydc5X)rDMWeJ92YrE?n%YPge&E@G^BB|8L<T
zu2@UF$O^I52(Zxp>*bm%xh`*gbabV+ETm1@-Bp7)p0h&rCgi!UDvX6}8%`!=iHZ<|
z2fIJ(-<~_&{jR?arv#BF>mHIP%&HH5?hS~->I8W;xg;kJeDK!JZMU!i2A!_xK~2vd
z|ApLePdzW3Z8+Hr^Y;$<XJGxVFX0yQtzG{NK=R%&x9uXrT?aqz`&2pZEe!G8%>Azf
zVEVST@Qc33(DbhTLK%pCVJ`eRW-72X9NPPboTVoBT>qN^=p48$_tT**0XQ@i=Jx%=
zDd68eA9F4GADb&HbGKNCMn=%%Zz5j}KxHJ%4O}RCB=N(p{ZHaO<pukPl2Nq3l>9>g
zK32or(T1Y^<meIC{=?Ds3b3DP%biP~4#1{#m{T5cZqWOz=vvG?`v}K9&E;-9f4jfp
Kq@R0>{rn$lNN>IX

delta 5473
zcmb7Ie{dA_70=!7T@n&hG=xAgatR<25(5E*vqDg-#1MlKsh}vEyYF#}ce}^#9%(3Y
zpolHXmF1P2HD?DiGTKfl3bB-(I`lABas1KIwpvlC6$|6gb~@-E)ftDrw?FPS5ocQd
zAa}d(`@Zk{-sgSZ=X*bY$p7RX|L&<(^TTsm+vYu1R#xVNCH0Mmdg{jeu7d~0OG`gq
zqc9-~a%!OK6jKCElqC?PsLp+SUqJv<R6&3~MbsFY7>>a#o%`1ZXar>87{ip>#!Pl_
zm)=rVRuFRBv05{wun3DXHP0OzU+4vMMnTZIIa7v1_<yL-Yc_!xGa_;_mFO3xb<ihj
zak!bqjCtt)Wq+a9uy#)*<h_SOeZZoICX-*4F++<pJ1W)Ll3qR294jch_WAa2Ixc4Q
z@~U<-DMT6c?misq$571{o&V^gZd|JLi7J}~{S&TQ)2#FPqp$SjE~HEbLNw36k?%^Y
zn$ExR<edzd(IwkodVoO$n4}pu$w^VebVSMK`;-~I?43a~tOrkQ>xhv%JU;*Q!^3j`
zzMjyS;m;0Gv<g$@v=U)C{%qb8B^Nzu&e8+doe?F72r9iEpsdCP6_OZuI-!ZF1Oqph
zs;sCwx=`bSLP_(us#vC(Goq~7$%rItESlp2FYG{9@MK-jxT9k+5DAkGLL!mpUU&p9
z)J<9D)~p)=upF~@=pV;d;GYHIm&9yVuh`d(@$vWWqC+jX%EaWWfNpetLA?bF46~GE
zxGXfj>Yf{h=jhzm+Y8+W4AxD6!HE-FR(2gV)pP_86vx$q1_jy!3$;G$>`y1oas9uh
zT)}4(XZrh(K<%W)%iZG;FjcF9L$^%&l=BV3HT6BPwSEJ?f9w+jL+9&Lz92t${eotI
z)cBeVpVYBr2@B6^TukYFa!*WF46FRc3jIRUg#HvT%w=+q95cG{vjVoYUUsGq%Nh9c
z@3-g|YMGo!^kLkx8wh4S7pR$}q!XA4L1EB+`!cdyr3bEfkx94-f<A*;)&n&Yow7+0
z0zfGmz_!BrK$K}LDM~ErB%zm@P_yCAB%OP2rv`l><A=ve-G}}3-p*d=r>E2|^IP=5
zhR)f|9Wlers+d9if0t2j7N4!hV&1UV#E6ZeQ%w;hRft%*HF|e<oszY<6AJdFh4W~R
zfB#q1ntA^H1NK7@B~=q7Op0d6F;6M=%Ed=aa>Fu&&2`8u8dI=Y1q8R{&nPW*_K{<`
zz{H!2fn$(c>P-u$!wU*>s@TpI@8^f-<O169!nXpoaJ}yP<7{hLwTmvj^5pAKy|6A*
zx#s9-cOfV~!Q}9<F~|^=^ZVvtCi57RT?g5aQ+tclX!Js{!4fhefq(TrP0sVLt|8p2
zLXv?er`Xt+=B=}6nK(0K3EvX<WlT{dl2%k;f|3w1McDn4prsWd;ig52G9|~Qr^zv$
zOHcPWEm8rsAz;Cnf^G4p+SUvmrD7lf22Yj|f!c}BAQ=#^d#hFcK`R*`5NA2Nj!b#*
zlO9Yt_uvoyr<4~nUVfUm54+#XCQ!dHIJySpe?$%Pb`1gtcFt|iap!Ks^GFP#hpp)W
zNcr-qL>4-CuG2mno=lQUChN0?=^luZuXEd0SqHnR2&SOCjZQY^+5huosY4gT5_ubO
z4hu^-#C|j^#&Wnjoq%D_=ecdGo%3MQ4Z$rX(t}d~FG=LNw(V9k6$!zx@tUy*T+mo!
zH@Mp+2;%Z5vSxRW&b7rv%@9>*fn!f$>U3z&0z2dUZ}!Y<##IlOrlZc?wgr7888U<u
zoGK?-j_cf&kyF&;wphSJb!HL1o&p7*U+2z#gVq3&gcg@oLb+>3u^uug{t}FhK4d<D
zh^=#%pvY+{>Xs2n6~}vwoIpxgA!6qcea3}>!=a5tH8@+0_$Z3ih-C#;71trbB2)K@
z*hPw%=qI*r$qu4cSzK0z44UI!f`vn|Deb;%?!JF^Yjd8vd+idPySr0m8`6xp8z+P&
zC@xi6tPg((ea8oIE|k8!=<6m~QRIZ6^uwDC$^sM{?f{XIEBkP~Jrfg?j73GH#Y8{E
z6gf$P2NqhLNuOr7wq)TKjg1+Ra*pBk;F!_*Cf0^Rr71SDKg&D*L@56BD+k58?~#?x
zSf$ZjwcHxrw@ve`q9M@9yY1;&fOA-{z9U1ko)%<mjGQ=l{DG`qS@HPj71oQaKK9ab
zdj;YggLH9Dp*rApr)HG$nCG`I^&(v7x8HhEgzwMT67I8*2jNaI&z>|@giQ|D7J*E1
z?{8g*Zho`sjXcn}hvNHffpCUm(+$uNF4}L;#N22yBsiJm^pCxB#cTiZL}O_ey`nnh
zdFI%)EF2D5<T9$yX3_qxPft&J$B+X{SUPp=;)~(O!VJ1W=@4U*XvuYKui=o3XOj>^
zNSh0PZroaPF&{9lb;5E7{+2agvw7Z#=|M2rw8Lz$`BiN|W#k$9P|%8GPyB%yZuLWG
zTJ6-P=e{(t(x^Nwkq9coVHb09jiNKhJzouLSJg<^n5Y3AH)1wlUUO!YJ}hlfzV(&D
zBAuJ`V$s~N1%ii5Dr##@H7=(UGzv6$rCaxvgXsvfEDX*J`>#9#!X<Sfyq>t^L|GCf
zq>z3{vZSSd7&6O->9t(blG9KzeX^x3VcPVqsNxCTI7}_sgFJ#aiWS8yRCdXxEG7E$
z{MneR)Qj&CoTTzw^oplWu81QiS)2+&BqA$OA}>ugu$pik-2?VxmYjTfuVfjUJdi)_
zv1+4-t~jnB2Uf)*+6XmHbctify9f(wF}{nI4kW+F5y5%x@uOZ=FF{hoLr&hX_;<63
zQ6`5?5dqwd^iRXxj>5jeaQcUW6@g9pQ9%=ow2H)QU%%S#safNs3;)=c3+J5ZGRH;h
zy<VL#afEJIOFe@Lyt3Hr>#d0FfVRA9Mo?T*&ELNEicIOvn9ui_sz}^T>p|48bS^sL
z0?wI@fL#);$Mi{L;=~fcH>g(E(WUj^4VK70xJcA6kmuXtGHP*#>l7-N&K+FTW~ex>
zaIR@N{1%lnG!|9MSi?f&0LJX&4cEbprs55jHZyQ4rIRU_8>xv=!~b-0HzwlrbTqJK
z9nLo#fqCxyO1!dN^!Q)DW!gyxYtCjU>rl$N&Yhk{>!^nNHyxuARy=atw0Q`u^f>1p
zWmWana*|kiPRn9ybDZ`QH&0;Q;V46R%q=@;9o573p3$q1eC`&+a2mmid{hJ^Sldb6
zk-GM12~3w8kgM_?q+k6*=cGFK(o+Hkg^~*A_TUI~XG*wv?K!ltDx1dzHV@IY7x$w(
zmY`U79^7wKM_s+i>^0CkNi(-T^dm-&dv`HbBhS6N2(<=2!8&4hS(2vM4)EcOstotZ
zJTx?LcN=_Ee?%2&4+IPO!G5P2+aR!t?;N@V>mS}v(6N3Czzi>+O_pBuPd85V7-1<b
zjpsqJ6n<K?HegBw5tEVD3B3u188*+`{v5?gzb?3X%0pe{uRmql7I}{CZLklgHsm;#
zLrv{|H)w#m%+~NtYU5Ab_&r;ww>Tn>9H4%5{CQf;DqT@B!Iv{PW$a&#@VbdVSn$iv
zdXAgtmz}X@GAcm!&258k-*>yEtwypb-OZs5$I`|f7RZYWX|5gqH%%I>pz1z`uV!7A
z8TXEx6cQ5~4~#ZCF1}ob9hARh$x0e{vkuq=b{CQ7z7M};k%8nNoD#YduZKE6?rppl
ztFlDQPXaZS!W&=|9&NteHy=(--9EIsrPtT%A^2|_Yi>OpYC!QJBzD(zCQz3B^Y`Wq
zJ3b^nXD;HvP2k4(-8y{}oV#{rwUw#4mi&xDLu<Ql-%zA=A_pDeu)nzl2j&FW*0zG*
zSM$pY@NU}{`?r?6=6(@?r)$RXDwc6*D10mcpWG7mU!S1?3qK2A3J<m4W1F68=Yv7J
zyb!+iF5ln~-1=4k271E&rFiyBYGHHzn4x&roB&y&-i7l$F|@k(&KHAl#oDm{t_V5h
zX=+3L>h-qQAFtkN+2d1qVC^cjKe2W}Iov3P{k@Y)_Q80>wqGCrOVNHnx*y)UJUHZ+
zXI8-Ho5TK;zqF!n(=>a<s=k3@M4b;tafhJ?@9_IG*A4}@PV!Yg`i1|m*1!J(;*LL`

diff --git a/Robust/Transactions/Notes/sysgurantees.tex b/Robust/Transactions/Notes/sysgurantees.tex
index b50b389d..b980b0e8 100644
--- a/Robust/Transactions/Notes/sysgurantees.tex
+++ b/Robust/Transactions/Notes/sysgurantees.tex
@@ -34,12 +34,11 @@ Def 5- \emph{No See In Future}: Assume $T_i$ is an uncomiited transaction and $T
 
 \hspace{7mm} 2- $a \in OP_{T_i}$ and $a$ happens before $b$ in the natural order of the transaction. Formally, $a$ has a lower position than that of $b$ in $OP_{T_i}$ = \{$OP_1$, ..., $OP_n$\} \\
 
-Def 6- \emph{Precedence Relationship for Read-Write Operations}:
 
-Def 7- \emph{Precedence Relationship for Read-Write Operations}: Assume $b$ is a read operation and $a$ is a write operation, and $a$ and $b$ share resource $r_i$, $a$ precedes $b$ ($a \rightarrow b$) if complying with Def 5, $b$ is allowed to see the writes to $r_i$ made by $a$. Otherwise, $b \rightarrow a$. For other pairs of operations or read-writes that do not share resources $a \rightarrow b$ and $b \rightarrow a$.\\
+Def 6- \emph{Precedence Relationship for Read-Write Operations}: Assume $b$ is a read operation and $a$ is a write operation, and $a$ and $b$ share resource $r_i$, $a$ precedes $b$ ($a \rightarrow b$) if complying with Def 5, $b$ is allowed to see the writes to $r_i$ made by $a$. Otherwise, $b \rightarrow a$. For other pairs of operations or read-writes that do not share resources $a \rightarrow b$ and $b \rightarrow a$.\\
 
 
-Corrolary- \emph{Read Must See Most Recent Comitted Write}: If $a \in OP{T_i}$ reads the resource $r_i$, in case $a$ has multiple precedessors sharing $r_i$ (denoted as $OP_{precedessors-for-r_i}$), then if all of them are from sets other than $OP_{T_i}$, $a$ sees the writes made by $op_{T_j} \in OP_{precedessors-for-r_i}$ such that $T_j$ has the greatest "commit instant" between all transaction with such operations. Otherwise, $a$ sees the most recent precedessor in $OP_{T_i}$. \\
+Corrolary 1- \emph{Read Must See Most Recent Comitted Write}: If $a \in OP{T_i}$ reads the resource $r_i$, in case $a$ has multiple precedessors sharing $r_i$ (denoted as $OP_{precedessors-for-r_i}$), then if all of them are from sets other than $OP_{T_i}$, $a$ sees the writes made by $op_{T_j} \in OP_{precedessors-for-r_i}$ such that $T_j$ has the greatest "commit instant" between all transaction with such operations. Otherwise, $a$ sees the most recent precedessor in $OP_{T_i}$. \\
 
 proof: Consider case 1 that all precedessors are from sets of operations other than that of $a$'s, according to Def 4 all these prcedessors belong to comitted transactions. Assume $T_i$ is accessing data at $t_i$, $t_i$ is neccasarily gretaer than all members of \{$committime_{T_1}, ..., commitime_{T_{i-1}}$\},and hence the writes to $r_i$ made by these commited transaction, have accroding to Def 1 been already reflected in the file system. Since, $T_{i-1}$ has the greatest commit instant its changes have overriiden that of previously commited transactions and thus, $a$ reading $r_i$ from file system sees these changes.\\
 
@@ -48,13 +47,13 @@ In case 2 that there are operations preceding $a$ in $OP_{T_i}$, according to de
 
 %Def 8- \emph{Precedence Relationship for Other Types of Operations}:  Follwoing rules are ONLY enforced if precedence relationship is not detemined between two operations by Def 6. 1-If $T_i$ and $T_j$ are two transactions both committed with commit instant of $T_j$ being greater than commit instant of $T_i$ then $\forall op_i \in OP_{T_i}, \forall op_j \in OP_{T_j} op_i \rightarrow op_j$. 2-If two operation belong to the same transaction, then the one that occurs earlier in natural order of transaction precedes the other. 3- If $T_i$ is committed and $T_j$ is not, $\forall op_i \in OP_{T_i}, \forall op_j \in OP_{T_j} op_i \rightarrow op_j$. 4- If neither $T_i$ has commited nor $T_j$, then  $\forall op_i \in OP_{T_i}, \forall op_j \in OP_{T_j} op_i \rightarrow op_j$, if there is either not a precedence relationship between $op_i$ and $op_j$ OR it is $op_i \rightarrow op_j$. 5- Otherwise, it means some operations in $T_i$ precede some of thos in $T_j$ and the other way around, for thos pairs not having such relationship it is assigned arbitrarily.\\
 
-Def 8- $\forall$ $op_{T_i}$ $\in OP_{T_i}$ and $\forall op_{T_j}\in OP_{T_j}$ if and only if $op_{T_i} \rightarrow op_{T_j}$ then $T_i$ $\rightarrow T_j$ \hspace{8mm} (this defines precedes relationship for members of $T$) \\
+Def 7- $\forall$ $op_{T_i}$ $\in OP_{T_i}$ and $\forall op_{T_j}\in OP_{T_j}$ if and only if $op_{T_i} \rightarrow op_{T_j}$ then $T_i$ $\rightarrow T_j$ \hspace{8mm} (this defines precedes relationship for members of $T$) \\
 
-Def 9- A sequence of tarnsaction are said to be consistent if and only if a total ordeing of them according to precedence relationship can be established.\\ 
+Def 8- A sequence of tarnsaction are said to be consistent if and only if a total ordeing of them according to precedence relationship can be established that demonstrates the same behavior as the behavior of the program.\\ 
 
-Corrolary: \emph{Upon Commit All Mebers of $T_{commit}$ Should Precede $T_i$}
+Corrolary 2: \emph{Upon Commit All Mebers of $T_{commit}$ Should Precede $T_i$}
 
-proof: Follows imeediately from Def 8 and Def 9.
+proof: Follows imeediately from Def 8 and Def 9. This is later proven formally.i\\
 
 %Def 2- An operation in $T_i$ is said to have "used" the data when it has read some data and has done some actions that is potentially irreversible. hence if the data in question was to change, $op$ would have different results. A transaction with such an operation in its operations set is said to have used that data. Any data read and used within a transaction at its commit instant does not count as using. "Use" can just be attributed to the operations actually reading data before commit instant. \\   
 
@@ -71,7 +70,7 @@ proof: Follows imeediately from Def 8 and Def 9.
 \subsection{Rules}
 %If we denote $\rightarrow$ as the relation precedes between operations and $OP_{T_i}$ as the set of all operation within $T_i$ from the set \{BeginTransaction, TransactionaFile.Read, TransactionalFile.Write, EndTransactioni\} we would have: \\ 
 
-i%Rule 1- for any pair of operations (transactions) $a$ and $b$ their relationship is taken from the set \{$\rightarrow$, $\leftarrow$, $\leftarrow$ and $\rightarrow$\} \\
+%Rule 1- for any pair of operations (transactions) $a$ and $b$ their relationship is taken from the set \{$\rightarrow$, $\leftarrow$, $\leftarrow$ and $\rightarrow$\} \\
 
 %proof: Follows from defenition. \\
 
@@ -81,14 +80,14 @@ i%Rule 1- for any pair of operations (transactions) $a$ and $b$ their relationsh
 
 %Rule 1- $\forall op_i \in  OP{T_i}$, $\forall op_j \in  OP{T_j}$, $\forall op_k \in  OP{T_k}$, if there is a precedence relationship between $op_i$ and $op_k$ sand $op_i \rightarrow op_k$, and if there is a relationship between $op_k$ and $op_j$ and $op_k \rightarrow op_j$, then $op_i \rightarrow op_j$ \\
 
-proof: Follows from the defenition of $\rightarrow$ \\
+%proof: Follows from the defenition of $\rightarrow$ \\
 
 
-Rule 2- if $T_i \rightarrow T_k$ and $T_k \rightarrow T_j$ then $T_i \rightarrow T_j$ \\
+Rule 1- if $T_i \rightarrow T_k$ and $T_k \rightarrow T_j$ then $T_i \rightarrow T_j$ \\
 
 proof: Since Def 9 ensures all operations in $OP_{T_i}$ precede those in $OP_{T_j}$. \\ 
 
-Rule 5- If $T_j$ "commits" at instant $t_j$, and $T_{commited}$ denotes the set of all commited transactions at $t_i$ such that $t_j > t_i$ then all members of $T_{commited}$ should precede $T_j$ (hence they should succed)\\
+Rule 2- If $T_j$ "commits" at instant $t_j$, and $T_{commited}$ denotes the set of all commited transactions at $t_i$ such that $t_j > t_i$ then all members of $T_{commited}$ should precede $T_j$ (hence they should succed)\\
 
 proof: $T_i$ denotes the last commited member of $T_{commited}$. Lets assume on the contrary $T_i$ does not precede $T_j$ and hence $T_j \rightarrow T_i$.\\
 
@@ -96,16 +95,17 @@ If there is not a pair of (read, write) or (write, read), sharing resource $r_n$
 
 If there are such operations, 1-At least an operation $a$ reads from $r_n$ in $OP_i$ sees the writes made by a write operation on $r_n$($b$) in $OP_j$, however since $T_j$ is just about to commit and acording to Def 4, writes are not reflected till commit instant, hence $a$ could not have read the writes made by $b$ and consequently $a$ does not precede $b$ contradicting the assumption $T_j \rightarrow T_i$ . OR 2- An operation $a$ in $T_i$ writes to resource $r_i$ and operation $b$ in $T_j$ reads resource $b$, according to Def 5 and Def 5 $a$ precedes $b$ and $b$ does not precede $a$, hence contradicting the assumption that $T_j \rightarrow T_i$.\\ 
 
-If
-If an operation $op_{i_1}$ in $OP_i$, writes some data used by an operation $op_{j_i}$ in $OP_j$, then $op_{j_1}$ can not precede $op_{i_1}$ since then it could not have seen the changes by it, however def 3 says it does, this is in contrats to the assumption. On the other hand, if $op_{j_1}$ affects some data used by $op{i_1}$, then since $op{i_1}$ has not seen the change, $op{j_1}$ can not precede $op{i_1}$. If no operations in $OP_i$ affects another in $OP_j$, then the set of all opeartions in $OP_i$ both precede and succed those in $OP_j$, and hence the contraray to the assumption. In this case, the transaction are conceptually interchangable. In either case, $T_j$ either "succeds" or "succeds and precedes" $T_i$. Either way it succeds the other. \\
 
+The same reasoning could be done for $T_i$ and $T_{i-1}$, $T_{i-1}$ the last commited transaction before $T_{i}$. Now according to rule 3, since $T_{i-1}$ precedes $T_i$ and $T_i$ precedes $T_{j}$, hence $T_{i-1}$ precedes $T_{j}$. Same reasoning is applied for all the members of $T_{commited}$. \\
 
-The same reasoning could be done for $T_i$ and $T_{i-1}$, $T_{i-1}$ the last commited transaction before $T_{i}$. Now according to rule 3, since $T_j$ succeds $T_i$ and $T_i$ succeds $T_{i-1}$, hence $T_j$ succeds $T_{i-1}$. Same reasoning is applied for all the members of $T_{commited}$. \\ 
+%If an operation $op_{i_1}$ in $OP_i$, writes some data used by an operation $op_{j_i}$ in $OP_j$, then $op_{j_1}$ can not precede $op_{i_1}$ since then it could not have seen the changes by it, however def 3 says it does, this is in contrats to the assumption. On the other hand, if $op_{j_1}$ affects some data used by $op{i_1}$, then since $op{i_1}$ has not seen the change, $op{j_1}$ can not precede $op{i_1}$. If no operations in $OP_i$ affects another in $OP_j$, then the set of all opeartions in $OP_i$ both precede and succed those in $OP_j$, and hence the contraray to the assumption. In this case, the transaction are conceptually interchangable. In either case, $T_j$ either "succeds" or "succeds and precedes" $T_i$. Either way it succeds the other. \\
 
 
-Rule 6- If $T_j$ "commits" at instant $t_j$, and $T_{commited}$ denotes the set of all commited transactions at $t_i$ such that $t_j > t_i$ then $\forall op_i \in OP_{T_i}$, $\forall op_{all} \in$ the union of $OP_j$, such that $OP_j$ is the set of operations  for every $T_j \in T_{commited}$, then $op_i$  should not \emph ONLY precede $op_{all}$ (hence it should at least succed)\\
 
-Follows immediately from rule 4 and def 7. 
+
+Rule 3- If $T_j$ "commits" at instant $t_j$, and $T_{commited}$ denotes the set of all commited transactions at $t_i$ such that $t_j > t_i$ then $\forall op_i \in OP_{T_i}$, $\forall op_{all} \in$ the union of $OP_j$, such that $OP_j$ is the set of operations  for every $T_j \in T_{commited}$, then $op_{all}$  should precede $op_{i}$.\\
+
+Follows immediately from Rule 2 and Def 7. 
 
 \subsection{TransactionalFile Opeartions}
 TransactioalFiles can be either created inside or outside $T$. The TransactionalFile object ensures transactional access no matter where it is created and accessed. Meaning the first time $T_i$ \emph {uses} $tf_j$ the flow of the program should look like no other piece of code (i.e Transactional and non-transactional) outside $T_i$ will \emph {modify} $tf_j$ before $OP(endtransaction)_{T_i}$. Otherwise, $T_i$ has to abort. \\
-- 
2.34.1