From d43bb6423992abad010f1fe814ef79212e1f8f8a Mon Sep 17 00:00:00 2001
From: navid <navid>
Date: Thu, 18 Sep 2008 18:46:22 +0000
Subject: [PATCH] *** empty log message ***

---
 Robust/Transactions/Notes/sysgurantees.dvi | Bin 19624 -> 27184 bytes
 Robust/Transactions/Notes/sysgurantees.tex |  74 +++++++++++----------
 2 files changed, 40 insertions(+), 34 deletions(-)

diff --git a/Robust/Transactions/Notes/sysgurantees.dvi b/Robust/Transactions/Notes/sysgurantees.dvi
index 78947073abebe9f86c9b64c6c2d2bafad3566c7a..1eba1520f06bd2b699678040cb02059dc930be3c 100644
GIT binary patch
delta 12549
zcmb7K3w#t;x!>%}k`N%2R|zGhgaS<@L=q^E1gI&9O(~B;TC8owVRw=p%+9Pk6GH06
zY1OvAx-y)099b!%^yQ=F;q|(r?Y6;cy|q_cZ@pFuB9<1dijQB_+KT`0oSE4Pp!NFu
z*`_<^@tyDS|Nh^1&V!$=*!Sa#?bAmrY-?$mH~*8dSge9|Ou2Oby2plHCJ(=5)Am(I
zRhCn;In`A4?FZ^DHN_Ouk%tdhX_XCjmy9fHudJKy$|bqjRFJ1#fnV<0U9tC;M_co(
z*yPC5mNqvxH+eMBuAF(vu*ykYX_XcjWnjI27rPkUESocWa!Q6BJY1QtXp`>m#&3qM
zGQ&$I`*LiPr*<1Tl_|Zwj5ap1o|;oE&CnSJ@?Y?eTyvi7s{XI#J*s7lFjcEzWUrc1
z&16o?T1Kw1$&G)ttv{z(>UqE7m`W<8SW1JY8{3&ZVuGFDbC=T`i}5+Zmz}GQrqm`k
zvFt~Dl_n>#?Acyb@3GR2O)P0-GMY8mQ*3ss9v#2IIdh?^y7KQYO{uzJ;ncsMMw>*$
zH=#{`7y81Nba8w|PqExsUm!;R#f4x8FB&-_J`7@A5sR^HH8)o5VMl5vvl%rv+6C$9
zAIzKWNKZfg<T5UXBiCHfshgIfTdrKQlok;m*qW?+CR<c<jH}Rz{bWS3%}KoNOC6X!
zXyp{$RFb4zPn^fh?;Z8ookA69RWC?~muQwF9bT&G_Z+C-!i@Jb)wDfWz?&v!Omp$o
z$ddO6Gc`Mj1xYM_`0~i|tklI_<#8?VR5ng5YNlr@T8dc)UuU+j7-$sh?Y~d43ex_)
z8b1-aA}d+pbSX9I1$dkEHB0N}>N51+0S|v`7Gpa{*DYb2FlE3KTJ$9gHsD$?UFn&P
z8V>i&`^cZ*I_7|BsTpSEJofw17q`(DKHX$nG*jEutCFBJwm)t3s=lydk{dtsJveM3
ze&)O6vUdH1#q#YJ7nNjEH8s75dn`GWr&vrJXlL|5o1qW&*`nE(^wJL2*fH}myV>8M
zquWw*uDo`+!Xm0H$ZMBHtw95XDd22nGaw#sIYc6dQ*}?(Q}9AKhi(K4N2s~d%oEX>
z?FDJ(FS!oOa}j--$x?{ZW=B4FQ-|&uS%gOrnS-s4RQ*6{jmKWO;4*u}ldUi?BLh2F
z$}%We0t>*zu6)tdi0v5uj=IN({#x{%vDq26Xv8w^;lA#;Gbn%u1Q|24y_#hyFb@v9
zpa%Y$RN)0dEGt>A4kc&0@}&D9g#mTs3i71Ap-K$hgn?igGM%uvN2}-5Q7Yk|rjz|V
zcnA~L_SI$?03MD)dqjXPSG%3~*H2zPyAc1n{qmD*b3E!;lBo=UfPXns4O_?5Ug3ag
zE$hVg{Q;pUcTef;_DXADxV3Qc?>+pux>Zf~Ve`B*eeMIrC8Ssmz5;6J<OzRE?S+cx
zS_1fO$+J?s*Vfk74y)X?+Xf^*uIHV^gKGzSNUEYh^}qrg+@X^dNgSaduSi9WZ?a&2
z&oo%Kl56PB85z=#H$-c>K3#`<H$wAzl3WUF`O2|1J*C0>-T09=#m;=kLj1@Z7=$28
zsX328KjN*X7i`PKwjNZk=$>LG;j|P-8AT5dpyrwgIs4%aq~DRq9ziYwz}U_(<F>*2
z0(qpbqQ?<tRU@;-24uG+C5lFJIue_}gFB$+E%r7$vCnTQBK$(5y7J&>=FetNUay&(
zG<e$pfW6b`#y_v#K<UMFVkc{1#>(0&I!v=K13|j%5UQ#gvJ?o4&iZuW(&SVTJ^C7h
zAg=VcU-2M-2Z*8M0gazY7r8bSY{j7jxvn7n?blFWFe<tpYp~LWZK_^>T1x_F(k!ib
zTfD$B5!k?nPfaCr1TYSBlmogEAikm+ApX?Ev$7Z~ZE~gMcMi5PL_2xx{#PF-XkXa&
zgqF`cBhyCFUe)0u8{R;(*Q~yV-Qb_nqy%}ijy4sc*1$zn^d7QDMoFni{sZ6#+(f!(
z`H3*<C#<BfB9B-zjX*6YRMY6ok<Y;`7WZpb8gjB?$Li(qTsRb=QQsyfRyed-O<DkR
z!8in;=r($LIYA*eW8WP2hAqGN;tD!~k;}mG2N<%={oN(SrBJNL%7KFvml?U7(W~SJ
z9BIkE7G&flk36~BaHUV&y<RO)-X#R-!hu&fXBsE=S$$T{Q=QnednocB`fz7=0rLhI
zg>H)M2;Z&q;dFyrar^b_woiDl(~14;FJ0`NPHfK(c6{uG_J|{YFT!cO$W%%s+5Lm9
zzOqX+k5A}We$T3-YuMVm9IWPN;mt7Bm<PT=X$LWsE+npRBc(ct>lc+YH}S%I2Im)-
zu+nBH@!BJNqo{<#udwHm8X~bZ{9DUm6;-DNG{9NpQ}sKNG+216BjtZE7z;!+vT6>v
z$06|?PpaCzrYNGE$C>XR@aX|oYK^Q<VI3v}Rn@r<g#tjKQtE|bv&LSWvv4L*nqAJr
zp8lF2271Jd$CIsW*Tj$7ukIp0g@<v!Vx?Rd)WfdrFCt?MVI<hWk$0c&)LBw7fdO#R
zv|_Rhl-t*9X<6hC?((_7yG_%`!6)IvaJoPrkv%57c2%)KP{~w5axw}$+tJzQYS%5i
zXE$jYnB`H@5}Y{0vlbz>2Y@g|rt_DDVRctp{T?=TQr%2P+W1;YDM+htC?XsMq=;bj
z6%3X);IRwp#}6Nw-YEPKyVkKilP1~MCI3hs!_p3xBYz15553A69(#mNUXXY0g_N$m
z^S&Mc2*Aq<fF_d2r+HvrJOS%bbyl9Si@X}KAWT1lP3feLeC^Kr&V^2jbyxoLD}g7=
ze?Aq(3zLDKKdY{RFu8us1W`y_b5%+4#Oc}esr8lqA)ubg#JmLbD_b=qgBX2kfq->a
z+IA6HmC&4+ok>_hw9b*XO+MEf02sI5gn`I)G!S^h9gcp!nP(iKbARhi<khY;AlpE1
z6I5X!5jm*OPy~<z&Ipi!Hv@@sM(OvAzTOmgFBlnp0ciy(f=fR0t*eL>H3fz$v*^Tg
zPvJ0bT>qV}CgHSj#NL6a4A!y~R14%ZoD^kLa$>$R9F`^OZe@*A+T)|X&6Jv28x>QL
z(=J#3(03?cd|$$WBN0=1;@+ZwcOJeNhZs3u`U08w+L7R($z;yJfl{-}B?)v1+Ootl
zz*-hVqY|6vu~8S-t|qpCWg|ol)bZQOdW{YbhSD1H%fqopTk_7>J9qE^#T;KXft#W<
zxQA`Mc#7>v&)n^cVo(ar<ut@2DaN9pLzdd28GR<Q15Oe!6Odaq<;D+~QTr9*2T*4b
zLn1gZo1FNGCFFu+Nb-(|riM*iRpe1T(heynqd=wNgOo;S%@bzmshzqjj~mTlr<F_R
z$m1@+Xey!ce;;;+#svL1bmPkYUlGpx@C2!9IEZO_IXdd>LgI$+g--1z;{ORVr_^p$
z*TV9=Tu`D9P{y;Wo_x_vmz@;AirSbn%d!cC@3_*D)xueD)`5a_WEKA%^kgKtx2Q4U
ziP=lWUn-sYE(r~!#VV{<0m>NNo(}~+d)Tvdf?bd+pEr2@D$K~$$qPgaIZLkmUtXZ0
z#EXbr*}Jc}i4AzXXaKK{Yz~i_+FDX*Vi9!!Rx<#*D%r?aSH>_cq9R0P^z9R<;0u^1
zfS*V~sf+#3oC^=Wcj}4?yAXe4*239N{Ea4*^SPjOuynwTPcP+<l{)Y}W~v|Pqksl|
z_ADhA6z?vk!q~i|CSgP`CyDAtLtV?+Hwt85HfYS1R$dbjUxn3JhNU2rfR~dyvJ0m*
z*~nvo>G@*7zY753sI@dRts*6D8_gpjrDm`Tyd4nF3uIHtsAB)L0s|sO(0UM`1jDCZ
zgGgGwJbpi@xlmd8(3Pr~Wn-EvzxNCZYhuq)?X!%EriCMKjFHXBa8&qHwk4lx_Lh@G
zK|FHFIBG1q5yK1eqMJxSfs|>5Tmm~maMp){Xwi*)ZDbpp_ntiNrP0mNwGduxT3T<f
ze*l=?l`r`+i9?GQ<V(IJ#NwF5bhRHL?AuMa>Hy>w?no0cAL$%?7Ym>n(+69C!UsnX
z6T@&{jph>a(&5(uf39ThUQm#%&r=Xkf>{V0MCk=%a3r9n$Pnqts-bgaI6DDe@lwk_
zOOLh%R#R;-hQ*a6HI>vb*S}ey`o%!q2Oew5=iTAEK3Z&;(-<jM%irha(KF;9sc_|d
zuKcmZ=3h&Cv2n16BngNrKNdqfggn+4nb(tKW9iVn<XB}0GFgM#+~Y`xcB6n^0~Q>q
zSA>WKh*)ZOP)id*4vU#O`vZ@)=JQ^u-Nh#=tl1hAN0AY+*b_Q9bhR^Hh<NDUB6Lg5
zOJ;1c6iuf(51G-I5r4W;{VibxP(c!gCz2u>5HKO=0szB8-nRGWyWkCKuhxU^lV+hT
z0@hN>^w1hOtDFh;K;3bFH&#W^WGIj^BP6!0h0SEGp%-!Inep%<RJQAQr=l0DixwgL
z$zC%*%Yv4n=}6Xx;GHN2t@o{08TUu@GyEcE*KJ5Z(u{{egl0U#{w_}nx-Y_GoW#JB
z)Wi5wHqygrIZqD*E#znqBih2C*79|aDg<K#uH5>SXrW3Tjll0k^O(F|vrOBOTfdt1
z3{xZ}K@1RpL*vPnjm!FUPCpTnfO2CdxIVbLAk<_Yn1!cW?7n9M#U=+rq6B~pngC~0
zL?Vj@8CyNB(heu{g0ukuMNonUnl=K7nMzwih{n(!epG+)zj^g|>zH?LP4c}N0pQRU
zE>^sC%#}E?-UA~$(ybT3&g3lX3D~-*&djkZXN;TXyG3WWD;G{i3!<v3FAugB<S+h^
z{d{a~UHj!c@s|fYI*SO>OP39{dQ>t%pFdsE4`ra|rV<ZAg9yD!A|Z}kc)2_e9hO+>
zd~4NoTu&za=?atRm@k&Pg_eZt4EzQtWu>9<a9#8nDchR7$!GhUAwm!ZQQMmoZef-I
zxBl?6FcUZr){5e@Zn*Ny&D7m6G@c77|EBOaHD@u_rw@vjapajAet<%=eWE95WbNSk
zfp6!lorYj9|15<1u4KO$fgTJH9YTn8=MD@lNcK^&yPDJeY>V86T*X_&;C9#;O-)bu
zIk_P!Pi$b*wFII%iFwfCw!0~R%j-TxYs%|B8FWhk(+GpGyXf(iDWza#<li7KP?10t
zURn4MlL$SAaI_3yZ2N)AdI4uUnwD17fb>sf4_`XXb`o9V(C<iejU8MVb%EjS_YStY
ziRTAP0x%;z2Wk(ESc{_GNj$bKG7F81>c!6l4W-BgYEq26)<zc~G6C(e_vanE`t|Ej
zoF<+>%)3y*B>pk)j2c~8Y(jxd;+-vAJthr`AH`DD{r8d6mWzz&$ExN<=Qa}M?&_(c
zH32Px$py^_(YzU~=NDj$rq{94bH+CZ9QQ1uJXjx8n#FZ}z3`s<yIW_oPWFG7ZnM#R
zqT3{NrTRI1@Fi#zKs?Cw3qt7N)8potxxjLQ4P7BzaN|FmwKl*&_|h`4G~SUyYgyZ(
z0#o4DxRL-H3pwWUxqM&S?|L~{)Q_&PMS%l@pPK=l0Xxr;qh^s?17?n1He2h+zZy%h
zpE@)I_8s234s&WmacI(%+OZIFu#N7u#z6?cfggGL4TkD|TbnL`PQ4awHIeq8a;amH
zIux=MpHhfy?MEwF+m)VprEE98*_aRB22_;VX4(Giz^Nck2A(+XV12+s9O;Quoc)$`
zj~Zo;)b_SghD7@Q@baqY$6YpfK0F*NFD0@-s{ry4jsohb!XS%*`|74Is|JoIZU_Uq
zuJfzXa^td}U<~k(;^_`xmd*AKv~lOU;dQhmU3tNFv>D|E&Jf9zTye==j`W7-H|Fxr
z?0Fv-!rFnZg%QRs`E4+insrEHd1p%1H)(9S&*u-_N>>fYbE1wC@s+rA2ciFsKciqN
zS0VT>+&sy*U8kX0bXymS>RuJ~8{p6871t2rN(?oq;Nbz)jeA88SX7LJ#2#ndynGw7
z?KegbIrho7lia>?%U^^8y!<UPi)%yUbh~su+mLBQ<h}bxKWv@tN;UgCyK%L%@9ec!
zzR8t_8wk<o$UCzped8==;Jw~pSg6~{_HRy|JJ9@u(5z?{M2{%Vt|HCS9R}BF;5n#g
zuAUR96}Z8*T9B`P`w+4cQEUciyZTQ>%cc&;TWi*wRz5Ra{gLXkgeIK^5l3qMx3r3@
z?ySw*K1MgHoS(eh5%kbpY3B#g_mOtqLWRyE#M<Xx^kab+PLWelw&Ok#z!dtd)Ozrx
zNuu)N5m%7EFxKaExaOsT^9y5;D$#`FjbD&KUS|8$B$x$X{`nhegP}3G1tb}JIhaR8
z0zKFs+yG&3e<zArSH9!=A&UC-98#1c-?5?mGxxu--~9@@WIGSo=x_&|CrUX5Poe%G
z=2B~i<m9jrIeUm4gio$KZ59S;=sI(3;b@PC8*dZ(39C|24=>b8%0}z#+NP_*6XL)f
zlR0(6)LBu5d0K!|{G`(1yZK!l8arUE1O#|KaL*9oV78|(DI*wNRH1)sfNb>w`ha9T
zs%|5bpyVN%0!*-iElg@Bpi7F2m=K`gcO%{rHkRo6s?5j(+6EOdq(olUQmGJa=$GRt
zOsA_28<y@bNGtcF(G8YM$y8do4|?<(qC4}9MU`VH4YwkZ-A1s#=-}Xks5Haz;%cJN
z3sV4ZV|li(VjP!uPtfX#>>Gp>WrnU%@T7v&RilYZ%*Z&t<(PYtMG?qRK(6ZFjr$88
zG`QFH{HG5M{Dv1Eh4>SlO)t{13XA}^bEOwLIlC@MFI-J7NbDDOeHj!3%}^3mLtFXP
z;w*+b;-U{eiq?$iIUq9d>PAh`<>J7{x+tzhzeT(?Nco*a+tB?(Vs$tE+`G!B7pEG(
z>ui$?j77=_jE)leGut}!6nd?1-U?(q&k{uZc}0!ltUM7rbHWV|c4c`>kaU2JRq|oV
zW0U_1oeQKb$Z{X85~MEjYp(7g-9johBFl^%zKGj|oE=5PxfyG+{a2hjP(iufD!u+`
z!oSz^<(j?~@{Im$`D_S>jar}^zahz}6$!VeJ|y)SM3oDy!YQy#SdU>i$mYtUR@z3%
z;7BWvm1|gN^Razhq5&-`Kk8lpQE3>ZO21Fe9hV*rtvu%Uv^Wfp%s~QbQ2S<mi!ic-
za49xYw5R&$@y(D<M#E}@tyfVog?FnLs(qH#ms86XHPK>6-j|w(e<Ww0)#adTgkzs4
z=Z$h?bP}l4wj<A_<YT)x0H8GV*v0tuDz!_7^g#Smy~~Ffx>8Zf(8}p?`C{GV*XEA=
zY4C%yUUnc_I6b!Cf*=1YdW>2M)k(mlF>>?vEmd5fqp!T<pL1#d2*Q(ye^X6X`$tZP
z5(iFkyHZK)Bo4eHidbI$qRNIFktgHQc$oFvVz${Cw*I|E!gQz%GfBl^7H$x}hw=V?
zc!HI9b-Ldus=DD*P|2_#&$s{oC4-Q7=*j<S3Gr4cX?qaQW{QoVs&3-d891QFfep0=
zFIq`N+_L9)Pl?6u+7UapY;JL0KL06tPnn?ilnMONgw9Y+?Pe72<+DU<nsY2nGKrfh
z*a^EMu-Bzwj)FWVPISSQ=TwAo4&zk0BgGXd^&==ePG4DTi=c+ey{w|;$^~sX-U9a!
zkB2C}lJ7&RrUByV5VhUJAS5v`b1Auz;#*;~;y-^vfyaY-%JwS|L?tg)=OU-_hlD^5
z3S`O?4A1A#2D5SqY9a~n8@#Dl3cnfh@CH``L|8xpE7!jyo>ms*<657IisATX^fLPR
zn?*{q7>axiCg$4o35us@I9X10m_nZGfA?r>n$9<mDASjcJG*@ILz_5_2wRH4dZ4uC
z%8Mt67ZK9O^Mf%beySGT>1L-=y1#?J`*CIa=7*qrN51(%eo|^oIEi1JDWbiEJ{3-j
z3t0^BL^cAP@a0<ky)jRB<Hu)#0wvW#{CHCc`*g(ei8$pWQ$*NBU{lAAaFHSY#7*gu
z9V2gGa7{$3`2v&+NLM;pOHU(DP83E&W`9k_Ku|S{h!I1V`D871T{$XvDB5swOvMuM
zCeEu<$nT%~12DRuCQHQO9L(Xz2sXruuGH|0h#8#9{BOtx>}&%Rq=pk@gUwES{7r)~
zx59j>q&pSn$-x*awqT2nH+8bH-S2^uWArcJ6AT{V(aY6_6VSZJZ6$xLlE0|LwGQ6<
ztU8L0G3vR%1h`Ya`D55b`uJ9C5<e9$>5Lm%!X~c#$+e-ZezAM+(V~{gs3{GNXFNb9
z-o&4lm06e{Nlny%3oT0bb7hPAyHkiu&;Nl`UXY&u<J>Y~!5USI-#kxk<&3TE<oXKg
zR2v;xpXiH7gc*#F@Dsz*p!mT+jDyxrOb8EzMw^IKx)Y~R<t6}Ki$no`qX5rkTofJ?
z;?Hmu8yy&;<GKMmL^KoLd=5Djz`Fd<t}B8Nei6mVO6X>|p2LO8zd#IVZkXyM`d*sL
zj!xe?Bk}HM0?xHLU#RMQrRYC%Gx5Cm#4)^dl1?0Dzin=^?Hh~ynGNS-)TTXg6fbD#
z8X1H*j1GG0jf;KhbW5bi%c)=F8BpbQ)j@{{3RlWcgkZzUUw^f<6t6$_mS14dyQJAR
zuizZ%^c;e&a;^mTHbKL~R7vp?Kb_%*30vOcu0nO<r*;1lm0yPdZJ???PE#QT@EC!B
zG4x!>f6f7(j7LI1B6f1-1#H92(c}3GxAHq4Zk~f|W;Vf&%^Ajiw)~ERzicYS+40V{
z_~MO}-Pi+fFUs^-oGEj@b8tq>?ZfG<I#M2sx8tq)L8X0Ve0(HJ&i9jKWsoGVc^S)G
z$o^wW^}&Nnnn%jJr`_7Y=3dS4&i(sW-x-~{z@J(bOnuMqFtv_tSUID9A-?@37E5~-
lAK6i=Ye({pNw35oeEMjGi$4>ws)M^$#w#kd>i9AI?;n0_Muq?Y

delta 5060
zcmZu#e{dA_6~DXPOSpva!;$bSBqaU-BnjpR6au0#l!6)(0Rg4jZtnJSOYe4%-92JZ
zdd~Q3s&Zxh%FW8Dz=#NS{DHyh3e^i~siV?C@sCceFlxoZ;MCD}re&=3^S*nVT-q`r
zx!c=)?|t9<ywCf*d*vhlfhYYtt}OpSTT@Hx{6~F0pWkY#J9KNlWM1IH^F2E{Ps_Q$
zh5fpm)MZ0fcf49_$`K|Rwi%PzP&D7Qv-5QK_TBz{TiFN7<#XR^%H+hn=+s-n#P{=E
z%>C%C=8WysXN8F;8XFtyS-uNqyV>2PSJ#NUzg-)Xv+z)%!FC^fJ+DPsQrCKQDPa%%
zrZnRZiTAJ5qLz67ZS2-iWtv`)b1iAhx@0Pv%J2lPWbuK9zj~upYQDHqrE9o(-B{f)
zGkdpNjXqykGUS|a@F#scU#*ob;ox0;OiRThwjr^8I+2}U%g-{XWUSJ03mqIfEJtKx
z`1+<y+8Q%naU?ZjD=Jx_rwlo)sS(2_^F_Df&RD_3hy^86h=puqh5gZDm*qD&VF~By
zF=TzqF2u;Bc%06`<Z?M|8Z04&A~Nf-`*D$dH*<Q~ri>*<%bdo{UiM(<^<bZ_m@>P*
zta5^=2X$GBL?lz1t*F{Ac3;_~G~=Ip*X)Q~UkFAkH)In<8=M-K)m}3;XQ<a{w1P9f
zS#Mpcl##O|LlIfkOgSqYIYxGoe!_-Z0K=9HMpwBRM#=Gf)0={iKD`vd(UAwPE-w$T
zmnt^0wu%jF_EkK&i&w{pNxGu;TDU`(wUi!~4V(*=yWZzpCP%YE`oq?SoRI$Dc!!oq
zD5fR+KE6^lOi48@f9Sl^W{K~zc1uXV!(JXYc|*xxUT_qH8IlrVrpD^R{GmEqGMU1k
zA}|+X%bUY>7b1TGe1qXZC7KPEy@L32!LpY%HQvvZsI8bbn>oH}vE75G``vunqjCY`
z1f_!Ev2oexH%vK^6*lkGbW7O$1nVC^qfiMWhxc0)L+Odj6eCr-FQ&x-DgF?PYC1un
zU@Rdg;FUL}Zsf!XUuw~;IN@x5trg5(=SX2B4EZA~Hr06Kq=36=duIe>#%$d3wPU2h
zEQU~}(I3?{<(FE*(ODxIDNPLm3?(z}YFE9ZHWVV_{g)Nae>l`^3HKi2oy`IhXH|`T
zq}EG*PB?!GXLHj}Ib_`vr=+`HblfWjaP~r-Thae5jHClGyB`7ca>DLk7|FO|ni8@F
ztnN7%lhv@y6q89wjz&p0kVTu505f$-HKZ^R1g_$glt`O5fWf4+?o~*aD`apQ;Zot8
z!B8_+$iJ!e%1Ea^3Wwr?i}M@U@l~27Y8TeXxl2h0<fDBB%2{q*nlm|NrgU4jd>`%w
zB!icN?S_#`;En|sM|wSNmF7-ShS2UQ6`4@b8^GyE&_$iYAA9GeK{sJ?BxB7@H#>?N
zQNofb8@b@;zebSR;ODQQi-`@r8|@-{jaK>2_u8%C=XKPZGe<SB*9ARRF#RP;8BG6`
z`LCH${dR}b*`5Uh+-?PHp6FV23!@jzkm0Q6AME-`l?lB6dqQ$aiC()5RNN86#<OB;
z(BYM!PM3)?47bf$pJK*xVyl?%VNUz1WtQ0TsT4OfM*W-Wv3$8Bo4|iI8=N$)v|x|@
zdD3_3(2w%VDLze4pt}7Gjk|4LUP5%GP7I_ZvA72C_c2+gYsp=mr!_<2Lj!@R2zU$+
z2stCy06@OWrlED{!XS-;g>A<`*jB|`>zwNferf2z44-W2tr&O~A9#eH!gS*X_H7+h
zGgk0G_fW6LVGc;l680Wj(172A$Gi0`A%}&T%s{UAlM~K9x0=au-c?3SN!sXt8&{YV
zX;@FxZg(Yd6z1Mw`O;^n5bJ&Xs0%SNo9`hPKvp4KDJv|Sr=#LIVOe8wSqNV&FX7Oj
zZ<okMVFDet{*-qQ{@RovUbx}9G4}3?%hKyl<)wnN;eiR3{(>S&pLJ%V975UiL$%1T
zGsgz2;wk`|jQ4}AY^uDC#IX5r_%L@u0mZ$#MQl@}CxAJwIot-u#e&OxS|6tFlFq+5
zgvDIo+$7G=R^VJ^UIKZE&m8NbKJHTtqK<Lj<a@lJ+>eLQxdbDZJnW>T=!Ol|0RzQJ
z!!@1Hwgxv21kpjlf<QzFh-eH{#YU&eK$<;oaJxTBqaWGuu1U`0Q!D*VZ1U6xg5R%0
zm@L1d>W-Rkfksjkyhs4E75IKV@qa3ADoIe3Cr%6vv_~F^`}0NF2w&^WcBi&Cf+Zs>
z99YffO<Uc3-~=40IpM$>CCXKXE20t%oynrQmVl~(;3#k@dWC@zCbN^%f)!ro(Popc
zU}vUHDzk!<>w2J9`Wfr4yF4`R4_^_9Y;J|8D%LuEYI=SBQJOb)%w=Ma2Qi95+Zw1-
z3pR<ygz81T04#{j^oDj}F2I9X$N2m+?LJ$Up}?va0xP3<lMn^gAZK3b8u%0diF2JX
zf&?lCwE)0HGeTww4NlnywbNMOno1m2WIwG6u{T@F(!q${fk~o7z$C)CL#~oM_ev8#
z5aD%nJ&;A4vIwp;2}r}C@JI@Q@Z@I2osEExniF?65RAazHZVKOsJFzEXE4+?J))>-
zjCGBnPwZAc#}F)#k%UHqJS7A`kU)>cHJblkZ_rpVX|{>6XNo2PCT{7K_q&wAyizEc
zT<M8EK9NXAa3Mh=!V+UoBd9w(^#En;DkSmAxg*zXdQg?aNDFWn?=Kt>bu=YP*i+SX
zM2@pjBE}M)s$oB$ao;k$sOICm2nfMYi`!*5Q7#y2F2eR0wSsp#z(A<u*|1rrx-uP<
zzKBVn{4ESKD%67f=^8SF6c#0h)TG!wzsbdtOo0(a_Ji3fFlR7`A@0TQ1q6u^H2@9t
z@l9(KXbzNS>%rm7{nkfQ;4<q`0C}2=BMx9sBmu}-!J5bx*HlknG0EOyV|$_Bx~{OF
z)l83}N*L-cIE(8<@Fc1*V?ch&z~%(3QlS6U>802kIM_yFr5Vjb0ZPyblG+O~&Ay+p
zI54i2Rc)NPbfuaVpM8kKSbX-uW)5S@Bf6ik>vfJRpIoZpUL}-zm<vkM;%6s3h!*8H
zB1dJFkJ+raQq-b3aivgnuws@feen}a723kwVsLhK35c>^pnF$gP_11B=QR*(+fbf1
zvVoHoG`dHYHy5ITix((;&;evBE}^&4iJ%4;idlh^<G6LS=Ex@LA_s**Taj5W22)lG
zKB*~kf!wVaOMzTBFxf`iFKvt^zPXNzN8Z?@b65|5NAk!X1SPg-jS6J58CA7@oB4k@
zWgt+u+@H=0NAF#T73b(ZSYwWEG33oDE^$E#rlfmvmKUh7*0^mC!3S!>n!y)z%vc)k
zc422J#4Tk--<zgpN^u58kx|T?=sPmZ`ouHrvny)S*kV<;6b!(XdOQ@z6(dG6dC7B}
zr6O_yK2cQgv?VOrM~O0|1eQ~XBRM7^#ak5GUfksO*dy2IcGs`B=nu>54vm#h4W;)-
zn;~mH`Q-R*NmAFEiWTF02jAaV`;Iq$9JhSGTpnkgGR$K5!I)QjSNUeF+WB3_*SN6i
zh8VZQ_z#il-R5rL*ejt}h#s_Pn^jVKk1GP=k+_D2>oc<Aiup=HmLm#I33bVPjI_!^
z%C9A^SU_(Ufft5uS{nlc;s@dl0u5HF!9C1C#&La08lzFk?A<+M^@HqS{S{-V!<!nI
z!d5hHyYp8fCzq_S^fhibCoDZIt44~XG6oFrM5!&T++e8xuT{%W3!V%E>@@@5b1XfK
zn=`jpR)+3;gT5+oSL)TNxNHSeUo^A28}GiVq_NCP4lRg>A9e~0vr(55SKSMFBd*%U
z-o9}Xz5qG=kkjC%a@0~X=iEid)f?{DLl}KD`4D;mf^KmDqJZ{v5gi!0fc6Y#%*Z&g
zf*<vfUZ6hZ8|v_9n=<U$2~(;X7=fDu9g}y|NU>S_&6l%(b&PM|)4jk6bf&RMXSTaC
z0<8UzOq_M#219htK-IEjkgcy@>|ewlTQWr?Y_LerR*}A*7^t}Ey?}o&yQcF9exK|7
z-N4JM9tf3Zc31m++aLFx>1bgamt5<=3{Ot?J8aR0jqYPRH{2X3Eu?#3$;QU9?2os!
zO=)xX1P;7^di$P#r&{Xv1mgVV>n(K*BZ@!A0<nin+#<10V^@V1WHOKa)8||HH5;!?
T_LmIIQUd<a&G!Y)@PGdSY$S6W

diff --git a/Robust/Transactions/Notes/sysgurantees.tex b/Robust/Transactions/Notes/sysgurantees.tex
index 7c38f895..e2329d4d 100644
--- a/Robust/Transactions/Notes/sysgurantees.tex
+++ b/Robust/Transactions/Notes/sysgurantees.tex
@@ -14,80 +14,86 @@ Transaction is like below:
 This is adopted from dstm and can and may be changed. Within this block which 
 represents a member of set $T$. The functions beginTransction and endTransaction are implicitly called by the system without the intervention of the programmer.However, the programmer can read and write from TransactionalFile Objects within the blocks of a member of $T$. To provide consisteny the read and write from ordinary Java object files should be prohibited, otherwise the semantics of transactions would not be preserved. Hence, the sequence of operations provided to the programmer within a member of $T$ is the set \{TransactionalFile.Read(), TransactionalFile.Write()i, TransactionalFile.Seek()\}. However, always a beginTransaction() and commitTransaction() (if the transaction does not abort prior to this point) are performed too. \\ 
 
-A Transaction consists of a sequence of operations. Thus, a transaction can be represented as the \{$OP_1$, $OP_2$, ..., $OP_n$\}. The flow of program should be in a manner that we could have an arbitrary serial order of the members of $T$ (e.g. $T_5,T_6,T_1$,...) or any other order. The serial order should be in such a way that for any given two members of the set $T$, it looks all the operations of one occur before all the operation of the other. In the first case we would say the $T_i$ precedes $T_j$ and in the seconds case $T_j$ preceds $T_i$ and $T_i$ can observe all the effects made by the operations in $T_j$. \\
+A Transaction consists of a sequence of operations. Thus, a transaction can be represented as the \{$op_1$, $op_2$, ..., $op_n$\}. The flow of program should be in a manner that we could have an arbitrary serial order of the members of $T$ (e.g. $T_5,T_6,T_1$,...) or any other order. The serial order should be in such a way that for any given two members of the set $T$, it looks all the operations of one occur before all the operation of the other. %In the first case we would say the $T_i$ precedes $T_j$ and in the seconds case $T_j$ preceds $T_i$ and $T_i$ can observe all the effects made by the operations in $T_j$. \\
 
 \subsection{Defenitions}
 
-Def 1- \emph{Set of Operations}: Operations are taken from the set \{readoffset(fildescriptor), writeoffset(filedescriptor), readdata(inode, offset, length), writedata(inode, offset, length)\}. We denote read operations as readoffset and readdata and write operations as writeoffset and writedata.\\
-
-%Def 1- 1-An operation in $T_i$ is said to have "changed" or "affected" some data structure in correspondece to all members of $OP_{T- T_i}$ , when it reflects the changes in the filesystem in such a way that the modification is durable and irreversible. A transaction with such an operation $T_i$ in its operation set is said to have changed the data 2- An operation in $T_i$ is said to have "changed or affeced the data in correspondence to all the operations in $OP_{T_i}$ as soon as the operation is encountered \\
+Def 1- \emph{Set of Operations}: Operations are taken from the set \{readoffset(fildescriptor), getoffset(filedescriptor), writeoffset(filedescriptor), readdata(inode, offset, length), writedata(inode, offset, length), commit\}. We denote read operations as readoffset and readdata and write operations as writeoffset and writedata.\\
 
 Def 2- \emph{Operations Sharing Resources} 1- A readoffset operation and writeoffset operations are said to be sharing resources if they both operate on the same filedescriptor. 2- A readdata and writedata operations are said to be sharing resources if they both operate on the same inode AND the range of (offset, offset + length) within one overlaps with that of the other.\\ 
 
 Def 3- A read operation can only see the writes made by write operations sharing reources.\\ 
 
-Def 4- \emph{Commit Instant}: A transaction $T_i$ is said to "commit" at instant $t_i$, if and only if it reflects its "writes" mabe by write operations in the filesystem or equivalently makes it writes visible to the whole system for all members of $T$ accesing the data at instant $t_j$ such that $t_j > t_i$ . An operation $\in OP_{T_i}$ is said to commit if and only if $T_i$ commits. Commit instant are not splittable, hence it appears to other transactions that all writes are refleted in the file system together.\\ 
-
-Def 5- \emph{No See In Future}: Assume $T_i$ is an uncomiited transaction and $T_{commited}$ indicates the set of commited transaction. A read operation $b \in OP_{T_i}$ MAY ONLY see the writes(changes) made by write operation $b$ that shares resources with $b$ AND also is subject to one of the following conditions:\\
+Def 4- \emph{Commit Instant and Commit Operation}: A transaction commits when it invokes the "commit" operation. A transaction $T_i$ is said to "commit" at instant $t_i$, if and only if it reflects its "writes" mabe by write operations in the filesystem or equivalently makes it writes visible to the whole system for all members of $T$ accesing the data at instant $t_j$ such that $t_j > t_i$. After a transaction invokes commit operation, the transactin ends and no more operation by transaction is done. An operation $\in OP_{T_i}$ is said to commit if and only if $T_i$ commits. Commit instant are not splittable, hence it appears to other transactions that all writes are refleted in the file system together.\\ 
 
-\hspace{7mm} 1- $a \in OP_{T_j}$ ($j \neq i$)  such that $T_j \in T_{commited}$ \\
+Def 5- \emph{Precedence Relationship}: If $OP_{executed} = \{op_0, op_1, ..., op_n\}$ represnts the operations executed so far(from all transactions running), and the indices represnt the order of operations executed so far in an ascending manner, we define $op_i \rightarrow op_j$ (precedes) if and only if $i<j$.\\ 
 
-\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{Visbility of Writes}: Assume $T_i$ is an uncommitted transaction and $T_{commited}$ indicates the set of commited transaction (those which have invoked the "commit" operation). A read operation $b \in OP_{T_i}$ MAY ONLY see the writes(changes) made by precedent write operation $a$ that shares resources with $b$ AND also is subject to one of the following conditions:\\
 
+\hspace{7mm} 1- $a \in OP_{T_j}$ ($j \neq i$) such that $T_j \in T_{commited}$ \\
 
-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$.\\
+\hspace{7mm} 2- $a \in OP_{T_i}$ and $a$ happens before $b$ in the natural order of the transaction. Formally, $a \rightarrow b$\\
+ 
 
+Corrolary 1- \emph{No See in The Fututre}: If $ \exists op_i \in WRITEOP_{T_i}$ and $\exists op_j \in READOP{T_j}$ such that $i \neq j$ and $op_i \rightarrow op_j$ then if $op_j \rightarrow commit-operation_{T_i}$, writes made by $op_j$ are not seen by $op_i$.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: Follows immediately from Def 5 and Def 6.\\
 
-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.\\
+Corrolary 2- \emph{Read Must See Most Recent Comitted Write}: If $a \in OP{T_i}$ reads the resource $r_i$ at $t_i$. In case $a$ has multiple writer 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" less than $t_i$ between all transaction with such operations . Otherwise, $a$ sees the most recent precedessor in $OP_{T_i}$. \\
 
-In case 2 that there are operations preceding $a$ in $OP_{T_i}$, according to defenition of transaction $r_i$ should be read from the writes made by write operations in $T_i$, and as the last of such write operation overrides the written data to $r_i$ by other operations, $a$ gets to see the most recent precedessor in $T_i$.\\   
+axiom: Assume $a$ is accessing data at $t_i$, according to Def 6, only writes by those transactions that have already committed would be visble. Hence, $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 4 been already reflected in the file system. Since, $T_{i-1}$ has the greatest commit instant its changes have overriden that of previously commited transactions and thus, $a$ reading $r_i$ from file system sees these changes.\\
 
+In case 2 that there are writer operations writng $r_i$ and preceding $a$ in $OP_{T_i}$, according to defenition of transaction, $r_i$ should be read from the writes made by write operations in $T_i$, and as the last of such write operation overrides the written data to $r_i$ by other operations, $a$ gets to see the most recent precedessor in $T_i$.\\   
 
-%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 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 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.\\ 
+Def 8- \emph{Correctness}: 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 execution of the program. Behavior for an operation means the data it has read. Demonstrating the same behavior thus means all the read operations should still see the same data in the new sequence as they have seen in the actual sequence.\\
 
-Corrolary 2: \emph{Upon Commit All Mebers of $T_{commit}$ Should Precede $T_i$}
+Note: Def 7 and Def 8 indicate that if operations can be commuted in a given sequnce of $OP_{executed} = \{op_{T_1}(0), op_{T_4}(0), ... op_{T_1}(n)\}$ such that a total ordering of transactions (e.g \{$OP_{T_1}, OP_{T_2}, ..., OP_{T_n}) $\} can be obtained then the execution is consistent and correct. The eligiblity to commute is subject to conforming to Corrolary 1 \& 2.\\
 
-proof: Follows imeediately from Def 8 and Def 9. This is later proven formally.i\\
+Def 9- \emph{Relocation Operations in A Sequence}: In a sequence of operations $OP = \{op_1, op_2, ...,op_n\}$, any operation can relocate its position in the sequence unless as a result of this change, the behavior of a read operation changes (it reads different data).\\
 
-%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. \\   
+Note: \emph{No Exchange for Operations Belonging to The Same Transaction}: If $op_i \in OP_{T_i}$ and $op_{i+1} \in OP_{T_i}$, we never exchange $op_i$ and $op_{i+1}$, since even if this exchange does not change any operations behavior, there is still no point in doing this as the aim is to put all operations belonging to the same transaction together, the internal order among these is not any of our concern, and the precedence relationship among these as indicated by the execution should be maintained.\\ 
 
-%Def 4-  $\forall op_i \in OP_{T_i}$, $\forall op_j in OP{T_i}$, $op_i$ precedes $op_j$ if and only if $op_j$ does not use the data changed by $op_i$ OR if it does, then $op_j$ sees the changes made by $op_i$ unless data has been changed by a more recent precedessor. Furthermore  \\ 
 
-%Def 5- Succeds relationship is defined similarly.  \\
+%Def 9- A pair of operations are said to be conflictant if they form a pair of (read, write) or (write, read) acting on the same resource $r_n$.  
 
-%Def 5- \emph{Precedence Relationship for Operations}: Assume $b$ is a read operation and $a$ is a write operation, and $a$ and $b$ share resource $r_i$, 1- if $b$ see the writes made by the $a$ to $r_i$ and their relationship conforms to Def 4, then $a$ precedes $b$ ($a \rightarrow b$) 2- if $b$ does not see the changes written by $a$, however their relatioship conforms to Def 4,   $r_i$ has been changed by operation $c$ such that $t_{a-commit-instant}<t_{c-commint-instant}$ and $b$ sees the write made by $c$, then $a \rightarrow b$. 3- If $b$ does not see the changes made by $a$ and $r_i$ has been changed by operation $c$ such that 3- Otherwise $b$ precedes $a$. Precedence is only defined for a read and write operation sharing resources.\\ 
+%Corrolary 3: \emph{For $T_i$ to Commit All Members of $T_{commit}$ Should Precede $T_i$}
 
-%Def 6- If operation $a$ both precedes and succeds operation $b$ since they do not share any resources so the changes can be made visible, $a$ both precedes and succeds $b$. \\ 
+%proof: Follows immediately from Def 7 and Def 8. This is later proven formally.\\
 
+\subsection{Rules}
 
+Rule 1- $\forall op_i \in  OP{T_i}$, $\forall op_j \in  OP{T_j}$, $\forall op_k \in  OP{T_k}$, if $op_i \rightarrow op_k$ and  $op_k \rightarrow op_j$, then $op_i \rightarrow op_j$ \\
 
-\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: \\ 
+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$ \\
+
+proof: Follws from Rule 1 and Def 7. \\ 
+
+Rule 3- \emph{Exchnaging Position of Consecutive Operations}: Formally having the sequence of operations $OP = \{op_1,...,op_i,op_{i+1},...,op_n\}$, if $op_i \in OP_{T_n}$ and $op_{i+1} \in OP{T_m}$ such that $ n\neq m$, $op_i$ and $op_{i+1}$ can exchange positions if and only if none of the follwing conditions apply:\\
 
-%Rule 1- for any pair of operations (transactions) $a$ and $b$ their relationship is taken from the set \{$\rightarrow$, $\leftarrow$, $\leftarrow$ and $\rightarrow$\} \\
+\hspace{8mm} 1- If $op_i = {commit}$ and $op_{i+1} = {read}$ and $op_{i+1}$ reads $r_k$, then if there is at least another operation in $T_n$ that writes the data $r_k$, $op_i$ and $op_{i+1}$ can not exchange positions.\\ 
 
-%proof: Follows from defenition. \\
+\hspace{8mm} 2- If $op_{i+1} = {commit}$ and $op_{i} = {read}$ and $op_{i}$ reads $r_k$, then if there is at least another operation in $T_m$ that writes the data $r_k$, $op_i$ and $op_{i+1}$ can not exchange positions.\\ 
 
-%Rule 2) If an operation $a \in OP{T_i}$ has multiple prcedecors (denoted as $OP_{precedesors}$) that their changes overlap each other, then if all of them are from sets other than $OP{T_i}$, $a$ sees the "changes" made by the $op_i \in OP_{predecesors}$ such that $op_i$ has the greatest "commit instant"  . Otherwise, $a$ sees the most recent precedesor in $OP{T_i}$. \\  
 
-%proof: the first part follows from Def 4 , second derives from Def 4 and second part of Def 1.\\
+proof: According to Def 9, none of the operatios in the sequence should change behavior as the result of this exchange, however in this argument only $op_i$ and $op_{i+1}$ may change behavior as those are the only operations that their postions in the sequence is changed. However, since behavior is only defined for read operations, one of these without losing generality lets say $op_i$ should be a read operation on agiven resource $r_k$.\\
 
-%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$ \\
+Now changing the $(op_i, op_{i+1})$ to $(op_{i+1}, op_i)$ changes the behavior of $op_i$ if and inly if $op_{i+1}$ writes $r_k$ at the file system (all the previous precedessors are still the same, only $op{i+1}$ has been added). This means by defenition the $op_{i+1}$ should be a commit operation. And, if $op_{i+1}$ is a commit operation for $T_m$, and there is at least one write operation in $T_m$ writing to $r_k$, then according to Corrolary 2, $op_i$ should see the most recent results and hence sees these changes. These changes could not have been seen in the first case $(op_i, op_{i+1})$ due to Corrolary 1 (No See in The Futture).\\ 
 
-%proof: Follows from the defenition of $\rightarrow$ \\
 
+Rule 4 -\emph{Relocating the Position of an Operation Within the Sequence}: Given a sequence of operations $OP = \{op_1, ..., op_i, op_{i+1}, ..., op_j, op_{j+1}, ..., op_n\}$, $op_j$ can be put into the standing $i<j$ within the sequence (resulting in $OP = \{op_1, ..., op_i,op_j,op_{i+1},..., op_{j+1},...,op_n\}$) if and only if $\forall op \in \{op_{i+1}, ..., op_{j-1}\}$, $op$ and $op_j$ belong to different transactions and the pair $(op_j, op)$ or $(op,op_j)$ is not a pair subject to one of the conditions in Rule 3. The same holds true for $i>j$.\\
 
-Rule 1- if $T_i \rightarrow T_k$ and $T_k \rightarrow T_j$ then $T_i \rightarrow T_j$ \\
+proof: We use induction to prove if assumptions above hold true $op_j$ can be relocated to $i = j-n$. Assume the same $OP$ as before. If $n = 1$ then since according to assumption the pair $(op_j, op_{j-1})$ is not subject to the conditions in Rule 3, these two can be easily exchanged. Now, lets assume the $op_j$ can be relocated to $j-n-1$, now we prove it for $n$.  After relocation to $j-n-1$, $op_{i+1}$ immediately precedes $op_j$, as according to assumption and Rule 3 $op_j$ and $op_{i+1}$ can exchange positions. After this exchange, $op_j$ has been relocated by $n$ and to $i$ and $op_i$ now immediately precedes $op_j$.\\
 
-proof: Since Def 9 ensures all operations in $OP_{T_i}$ precede those in $OP_{T_j}$. \\ 
+The same argument can be used for $i > j$.\\
 
-Rule 2-  \emph{Committed transaction Should Precede the About to Commit Transaction}: $T_j$ "commits" at instant $t_j$ - $T_{commited}$ denotes the set of all commited transactions at $t_i$ such that $t_j > t_i$- only if all members of $T_{commited}$ precede $T_j$ (hence they should succed)\\
+%proof: If the sequence of operations $OP$ is a consistent one, exchanging the position of $a$ and $b$ does not violate this property as no difference in the bahvior of neither $op_i$ nor $op_{i+1}$ is made. If ($op_i, op_{i+1}) is changed to ($op_{i+1}, op_i) they would still both read the same data (if they are reads), since there is no other operation in the middle and Corrolary 2 says the read from $r_n$ reads the most commited write to $r-n$ and as no writes are reflected before the commit operation for that transaction is invoked, and none of these operations is a write, consequently exchanging their positions does not change the data read by them and hence the behavior.\\ 
+Rule 3-  \emph{Committed transaction Should Precede the About to Commit Transaction}: $T_j$ "commits" at instant $t_j$ - $T_{commited}$ denoting the set of all commited transactions at $t_i$ such that $t_j > t_i$- only if a sequence preseving the behavior of the program can be found that in it all members of $T_{commited}$ precede $T_j$.\\
 
 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$.\\
 
@@ -105,7 +111,7 @@ The same reasoning could be done for $T_i$ and $T_{i-1}$, $T_{i-1}$ the last com
 
 Rule 3-\emph{Operation in the Committed Transactions Precede Those in The Transaction About to Commit}: $T_j$ "commits" at instant $t_j$ - $T_{commited}$ denoting the set of all commited transactions at $t_i$ such that $t_j > t_i$- only if $\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}$, $op_{all}$  should precede $op_{i}$.\\
 
-proof: Follows immediately from Rul2 and Def 7.
+proof: Follows immediately from Rul2 and Def 7.\\
 
 Rule 4- \emph{If All committed Transactions Precede A Transaction About to Commit, It Commits}: $T_i$ commits if at its commit instant, $\forall T_j \in T_ccommitted T_j \rightarrow T_i$.
 
-- 
2.34.1