From db79726d58a308d23acd6da7a33cf38392a48ec2 Mon Sep 17 00:00:00 2001
From: navid <navid>
Date: Fri, 19 Sep 2008 00:09:13 +0000
Subject: [PATCH] *** empty log message ***

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

diff --git a/Robust/Transactions/Notes/sysgurantees.dvi b/Robust/Transactions/Notes/sysgurantees.dvi
index 1eba1520f06bd2b699678040cb02059dc930be3c..1543b3d88d4336eca9419e9f23ebcea54fc0da37 100644
GIT binary patch
delta 8741
zcma)C3vd*5nxCY5@{%_~f(GsqG$fD&5}t;a2@4TjNF>>C=(%fWrju!y=^na!^3Ywz
zU5i>v$w>Rx*_QEC?tHGYDp90Sa4;0yF5F%zUUBR5$~}CYp1Znw)^6=`zwh5YlSyQ+
z&MK>5`v3Tzzwh^bf1Z6K@82KJ+dHpl`J!ca`Fy@StD*9_>$erJ{qpk5zNqZ-m3+C_
zSAyRQ0+H^4hD9g8Bljfp&wRh3E|sr-{$=@}ee;@f*O*GfqEj8R$=KQAn#*lTmu*wp
zvG-twtlB-g7O~BcY#Xv^4_{WYCNECMSp|J38|za32Y-L6Et<R#b!44MrlP4v(*IIf
zM@Z5YwU=$-Ukoj#vjCF~t6+DD(@<wOTmA=k>arBnE}>Jk=-y55$~xbUFJDM%FtLBg
zs`vT&b;XqVqNMo#o!+{*drwMy|1L<%3`q$xQ?tA25N5bH+qz7*24sUNJq+Rx+THs$
zy{nlarbTU8uk$XDOgSl>xlL1PO-eWuH>8NnCWPgnYy@;AYHE7D<!_(gSjU<z;Y=S1
z9S=&T#2}>2#p8d=Rl#5o%R8ThONtvxO)VvEnEBU5BnuC+?)$iiFbE@a$h1>a=^M0+
z$hM+tP%<8rS@Y)acsJl<QXCl4CAC*hi316(hgEZn)mq|#GX5vFzz)l5uNkUg{fZe<
zR9jPJrrme2q7V0krKn-k?{thAlHd<+G4FhsOxEiY`{9taJ|DUM8cV$Y#>I6>;lddQ
zM!E0;83kq?bz(}ma5^BVOjE;y%#aaH(107uU=a!8cO$k2ZMLT3vQi@{Jl5lRjp?%M
zwE6`5#l$TQk4(IOU-nwdfA(LNAmXMrom!_wB8r*xuXu5zYM7F0k~b{>io>jKQn_3>
zyc+>F<y{jtF{A(mr5(^B8JA<HkrX>#=?}>&Q%p<jNGmG0g|-7RN}ovFN^HT>$}x)7
zTLtGoZpM~-*fW#L;)nM+ijfIG&t92*N#XOElF1Y<;J$+uCQF+`59K{_%W)-P3BflV
z_$RLg!3oh_Ln%F$@Oi0X!U_}RfQiV(|CO%UDq%M_db;gF*OZC<^LdWs8XnRg`9R^p
zOhIf68m1g!n$FnZ<k`zJF6dJXr8_JmX(;MFx%)#}7`YJsz}wWL=_w)np%f0Yyx^sA
zOZ;M$BL$F9$ZPITHw!Wv!hoio(QtdhDt!HSju8v6kcA^Ds=RA*mK6D)POq_qhyHP_
zU65~|6gT&nvX0pLrGzm1m8r+Gu7pK%oQ03BpT@Werkz<yPRxdY%49WYcrw7^Nnx-{
z)l$OX_aYiFB-e&saAvmx8{p*krWE;qeXdz$?9(Z$ubfc!NXGNtnWmN$(+!?1N>55m
zFJkReOXEdXmN@ROM!i+EV9h!nRbE&i3rs>=rfMcLqG81}B{-(mI}-sKfJ+W+Q_Pfb
z;07tmQ%uqgf;*m<qY46e;Y=hiIm}BnoV*o4I8ip`Aa3MdLsWRDyMDHieWunc!&+mr
zJcW9(w9Z1kIMuFm7$*p4LCC~po2{KTqo}2FV-GE06RYO2+omnSABPW3Tb6eNFA(A%
zdzaOv#Lk7Mx)h^ZfpUXM@y;^<m#u{AhUNR9%xSU;uF{$fBL;L!cV_dW&?$y}EwOWv
zq}nmnH6XOGhg&W^mVfifb(*egVM!mf3MzisP-po&Po3JVCH;NxbjT?xMo`!C_r2YT
z7}#K4s40z^F;ll?%lG<z+*#E0FeJyOk*m^LG<$3Ds?#HlmjB%E*-fRjlP3P5)Ip?p
z)?!xabTK8AJkFjft&C58>@tdO_%D<cI`@&`Euk}&R_u{w&T2co-4ec<O1oL^`32gK
zM=I>>FO(%m9(7=Ol{Nzk#(auCM~hw6t-RA+BR)@*w8q-Xj>L0}Ancgj2v>dc*(tZ+
zG6?~G-Ih%;!(<tQY|`+TEw*e2Y#D%wI7GC`cF^^PXBhFP739)yK1(C-N**6+Wa&1*
zdi#)-x4SFro&*Upym!_U0=qDKW!~p(&#KGWn%T#TUA#u!W?ScU=j|UpI%mBwi3fx5
z&F_|@VwjuQ<jR>P$qCaR7-{6z%$q;6n31LU$IX?cY|7<gp3U;+PoK3tk+3Gb?so_n
z&F_*mc|n1prdG}<xa7&NVIbCCIV1mdKRaD{i_1%duZmXGrG)55s1kZ6a7|S<G65%!
z%t6(PzG=uiV{U>)Kh%0ac=SxQp!#i(r4<3>mjW<VDP=uBC_PEBLd}Sk5@%Ov1m{Rj
zQwjrggECPdx0pt3_RicZ;@(cw#-wobE5t}-lpIQW#RwruDUgt25!?p+L6Q(aTf)u9
zI4$Y6<&Xpc`V=6##J@3lKn}#H#Ni_EbZklHpASZLtyh;K^_KV#KW%Y0uB4r*{PO{T
zJL=9D*s~)tFqZCP9N87q4&e@}?feLK<cfFVCpT-RY>9h<4NaE+mdhRDmBJr(FXu%J
ze_<<-ctIrq(Oq3&5G_h-y6nziL<^t?qqv4DF(h@yoUqA>-%6}k>B9%gi4*@xJ^}`k
z5h)Pa)T-%4Jp;~aOIY2{YO8K+rA4Eec;dI*fKtW~<cOqj?=$2J&PT}^qpZMS)pC8W
zCEWWgJ6&~i{N87rjC5MJDJg1JG)mE=xb`+O&Zxl^BPFhlkBJO!hXCRZ^&4E_$pxJt
z&T?4kMZHx_uz*1-x}>`e%~4l8NsU;yHOZHHX*>22AHpIwJg>@)Xn$4fRdtqlOP813
zVVvM{?UZ=nd>e5^k9vdgq56YfiwA}~WX9v0Wk9cB_tA|ij@c?DaaJb!$+Vg3mtjbp
z##=&5g`a0XySu53g{v1$6uK5llmLTCd}B{m&xy0Btr-drKbLi6^vUMd(E~9RM8rr5
zN1sMGNeCz-7WOzM>S_SRJVe~J))Gc`!N4w$4@rz-H7OiD00AXbv2hfWU&OAfY0Sjr
zWp_3<S>o9+)dAt$3&6JsOq>$VJx{?tu1B$3<gljpB0p&@sww=$I*4L-Qnk=6)DX@%
za!q3S&Rs$U%l_d;Wd7}kT(rK{WpsuAaRX|Hcxyb}hH!63O?mFq<Aj(inqF0aV-x54
z$JK*l3mOvEw3q*lZ@VqsX1BA~I%doVcX_F}AE5$PAornF84Z_gc>sef{OE4BYyPaV
zjKLL76~1!hKH3VJa&Ug@T(LL-i)Nb<1zdZ>_Y6}3MIiFCp)0zV%~~+0%$Af0ksO3w
zGzKyq4x<Hu8mxW6%=O+4I4CI$IRr#0Vd!v98eyBuAK=1!p1?X_0HOp0PW5n5x7kw*
z$}{K(ik}o)eul&eU<ve99w89L#+2A%N0B?|z9{Q;IqbH2AtlNrfFdWJh79aOE9AmV
z(4}j+LO#|rnxjTYi-l<oA?=3Rsd2B3;W*}BZ!d;FUtV$%hLaLcez}F^2w;gPzi5%o
zejtEqQ*;3!b92w`;8%Hqv;ejDEcJ+!A?tlWRV%OJ=bI2f;?Lz~cw%h~$*?n~=yF6>
zd4tdoT<o{Ocuev{NV4I64#=Q~gzy~PatxnfTWg#0XYZu?8+TB&lESo*tGgUb3DXeY
zv>lzhu4Fx-M2JOd2C5D3!f1t}Q-cJJvQWSw0J#739oLX6Y7^Pg?k*&d8UyTcj_kx^
z$Dw<+b!-j;i(C82%|h#d9s?=>Orv2Av^G3VFa|E%EkQPPs9bc3s9}^#!#hX#ossW6
zGdGePRcvuBYvW{@_8>k?fJ#3@gab+0AZN`6x>~Lz<JFSSI7kNE6f^B^HfRUs9tp?<
zc^{g+WjA}Wc23pFEm&ds|Mf$nm=n*9tjNv4qLX)zG$#GhA@*7A?CHG+bH0Mv6`xA8
z*>&aEJ^JOJe{p<A!YbL_%6XMN%BuJWV8rA?bcNUe!h`F^Ubc6n!tzTmxIcO)H7JBB
ziT!MU-M%TVuwvs-BZ$^xJq~NFe|o<Aqwwsti|Z_5X~n7a1A&k#xxn|67ur4WwuGNN
z&t@*1*Y#)<*z!zS(<8uuLE7OGjtmSEV2US~!pdmtUHXK)Si);aZj~oAvkJ5)QK`jG
zI+(R^TiidX8fszl7`58!MjAa|rrR+6$N^5D?^PARIr*Axq-08bal`0Nj-At|ognOd
zO-r}2QCk9zBiMH7<GZrFKzwn%8K>STjr#YRN)(-Mi%<{#ryq?To3M(?|K_4F{mlcM
z8^{Bk^HaU@q;`{umq0$rAO@I2R8>A{0qbBNE~<?G-B%-sB%$%2P(XynM{+MlZ{VyR
zvOu~$%Ac?ntbXcZvP`}1&zY4v!I~6ISmjgSy695lj}BE%gQazpqPQD2{<-%+abe@H
zNYIgGbf?z_xpC-@-W&y#=Z?EP{+}&p@CuoC>LtAy^CIU!THTg2CEl?I(8X`dy-Ykl
z1DD0USsd7PS{?wMHhA-eg<%x5N4v<Iw<j)gBaeew50AOgv%h;U=S&Dn&RoaePN1Mt
zZ&jV`^a?Mz`l9yw@MZ31*4$V*VcV=8%A~H=jXjL%jdSy*Hukf|E3YYE3ao|Y#(3|g
zid;jxsuvBu$rpax#8%PZZydI&d{*2G@`=vt8Re2f^|2g_q7tNp>Q~0=WC_jhkq`<R
z7pm~=+XgMD)nHHxD7S?h@50GX-S2dJO>C|YJ;UNyvg*YxnydT&!<NG@E}kdMop(1R
zP6_i8nJ#Yh6rRshL+4rE@=NDkSK%O_aKDXV1@p#H)il?j-@p&R3}XfxUbXzLJV~s1
znP#gsFJ(spV;obMNIEVDKoxY0X#|Zh_+-HC<vczLW{P>PTSJtdMB<@2KHtzizW3HG
zW;d={m|qujYb>{QQoOMnWC;vPyixM#ieZ3c644yh2_c<cg)Cy3xrPet7Y;g#X~<!6
zTQ+N`+JDQz;vEm;HXgT`u#NK*p@%VAj<F^wu80LdAUKV72dtL3qK^iJ`08e6wy^6U
z5-EJmkt+h&6HhqkSMDw8r21)RK@R+!^C#4Gghd05<U<l4zv0$3Z*f{B<GeL*Ln_S4
zycv@Y3kOif8QXhRO`HW|m;h@SIe0@GyMa}2*6a>AL{YtP!^Jd;;^ha!8eOi*5(lra
zohVphiC3I=>c+J}RFZyhEi_GuKe#Sa(a_d_NO9U<KKeFcZ{_1}%Uurv*l>H(g}ee6
z@z@iqhA_0aYW0I+d^1hQ`%|L)Q9q_#Xr&oO<&<jf+|4$WApXdc4^*NT<16qLRFnID
zNq)7Fmf1i687Mma1>uU@+93AATBe{<ryR6I{V4@j)Spf(RFWQjc>*UB&}$Z`0_3W=
z8WW|--6KAX+dg&BH<bP*G18k}$(-ukd&Hg+{H8^n8XH_6r^0Wx#G;a-vvq6d#_@>K
zNf*7}LBxhF#zfM3^t&>~%$#R&1%V}sLDDnCZthI3sI@+WQEu?k)hn&MvkjRM8Z?Cj
z{BqB$Xf=-yR}ZD#LKP2E6+(d~JpbE>m0pRt(phh4ny{+QT22kGp0G3TdO%3sX>V8y
z!~Pfu9)CU}?cglr_^{-Kc1|c0@tSwk$>fuJl~>P#vA9mt)ueE2ItQX-(_k96+o1Gy
zUvqR0h3=nuL&Ou4A7mBxbUQ(fYA$8JX}dLy(mrD^Pwl_b1I8yzxq~Y2t#9ES2jOK2
zJ6B+cB<viWLPCMUb1gJmrYJ!YQFve(G|INx*sy{J3J%Kke&M-wPCw4&8S5#Qau4Sd
zHhVe8w~UNh6!R9<p;nXc$l#+lJoexN0~U>yFD`4PFrGi)RD&kVs@w8|_IYgsjeeGR
z2Up<*<-fAIo)SAgZRB3{(Dm76GvkDk_UO$4Oq%%XRmZ0o5umTiF|v0kv6!T=ix2hr
zER5=sCG47u4Sb9SC&;Xt0*6;DJ}*Eg!hhx%MvLJzv{m=T`NJ0-hZU5#*+&pMIw>4V
z(IZ)JN;tF+&;@ixzvn?0YpB8d#H3p{^3>;<MbBmbS1K^XziXz1b*1lS#C#k<?@_m$
zgs8mwRj0;N7ZOqN<(fhjLsKCS%Q`oxWx=u2UCCc>&^~b_;>{!<W%0H*M!g;dkgmBM
zWgJ%G0Kf~DLX+M#Y`Z0Hc-xT-LSZzb;c)f}uZQ^hhfC|mz4a!ABkurDgd=a0;qib>
zwpc$P({lk{324L>9MdGzh88*Q&R*P_kozu&7f<X2*WYm1ox=bPycayc*#^gLu`#@1
z&3h03J#yI{*J$?G7YbV18A6Lo-69M$eyCGV{iJ7Ueh`g&&;}-j2mZwC6t%)uUhyZ?
ztPkJLpEvGbSRO|K_dn4-f|=3v&w}nD#SE83xMNd1Wn04a&%p#TAIfIOhguY!O=bd`
z65e3lj0dJAym62FK8Rv7=Jl+o=>ejSF8qQ`^7vs7$_4S-AO9wMH8Tw=Nl6^TpV2ev
zI670!85W>BIdj2{Lwv_m_g}#M@SJD##L()w6B5dn+($e@bA<c#k0ab&7PI!2;{*hY
z@jR3B3^$Z{r$|_}`)+bBHcw0nZT|zp!(M5bQI#q@l;_k@+KrN<?Fl>cPG$*hU%N|7
z<Kx<?%*pORAWI(H*3lBxvs7kN`5*rX7Pj&~-bMPtwlrl%EZCCWj|t?U4b54I7cp9t
z)3{@>MvpWYD-dnow`mD)Na27^RI2)>tocyC>VN%x!t%-MbG8$DN1tPRww1LO-*ni?
zyyIm-+B?32v+{9Ovp$z}E=?r%eB<-2+QB9(r3?HQ{}&q<`?nr!rSji}ZRPpz;lKX{
DGdI%w

literal 27184
zcmd6Qdwdk--S4t9OTtw_5!6<NR!syV2`Cpq8$mRJfDoZxs!nz%WMH!!cQ?f7vD#W~
z-zr<ik#Xu)(MnrUTNGP$OTkE#>M8ZKw$)ZeYpp0=PE}fO)pEYS-}5{(&xX*KbI$w6
z%jbiJ-I?d|yMBL{=gEih0oUHt^SM)E_+z|r<T1_mmygMI7CJf$$23fuG_7vZ^t$?K
zGwSQ7oO}bG7(kExXMgtM&mHl*cf7Rvj?X$LkGmtD<{uxPJZ|-Bw=NdjbMUrj7u*pW
z-r5=)im?VJ+gmQLZ`fR4bmz|h)nfayPA6x#+nF^t?kMDo>&86yo_uX2zecZUuWhNX
z!;ABKV$JTq{v69$nY@)OIN40TxZ%)y_lo(3&wKCE?%3cxlVgMNaw6HDtDjU}=I%Yr
zwoAr?54TxsH;rB8*@5L64?dE&3qiIuXl~2dRw^It88zgNmQ%x*vDkK}eo{}fo0vYl
zY+FgMEy&p&IXiD>yn>Ti9#}ykT18!Rn@xizvun<IDP;$(*<4^1*AM&dt-P{kT0``-
zZ~U;;$$M#M<*l2>+FlFZvD4Y0Yew<T)o$unqr{r(QrV_LO~&qW@%U^jowi!ic5O}V
zo-t#`O}JHGX}-IDQg5q#xqRY@G`?Jkhn0BRLghof%jt*HVzF{_o0Ip=xhtG}$(*~=
zN@Y6=cFJqbW!t?}zR(_6nUt5bGW`E`Yt5#y-D15#5<j<DndNq>&K<br&1FuZ%>ijJ
z91RWjx1@;}Nzi;{$sG0dt~Limbj?xMMs&=BitTp07%}JLJ8*;;1G*2mZfO}Kk8c2J
zz1Gf*;C8^oTJB^*lJe(rN-WklThn$X6@D$Gq-3_Pv~srRw0ESPq*F+DV^irgcG^N)
z3JRDb-<>aDEnV0M6oWr<GWfP&=O)VWS79^E|7^xLAA2m@iv8MNM=rZOXSKK6xw^Bm
zc%sX*A!WG<Zld}Yd{0kCj}S3E5;>13+m&+)wj7*j?wfC}?Xz?%J=aOw-oh3)R@%J6
zP8RaKM5Z-lM-Uluv@-8yTV3-_-||3GL8lx(@<Lix-?M_p&dLd~C{hR~1??DrcM`hf
zfC3q>+c(Dl2n&b6TPb3Ez{_Nz2(r19ld*E$!Pz7XtK7Y*IaZJj7v~L4+xZ|53Z_$X
z8s?a9zI+(wYjaw#;S@+Su`!D&a$Qc|CL+4#%cJskyOqIC3Qm&tqKhr|9MF*TSSDK#
z0t3R^iZgjTw~CYr!Z_GD?<_l$v@yv){)nOd#MQ+-tPOoe!)7~3-*OgP4>xi3cd)L2
zsF3ms***-FTOgTmGJe81+;S7f5uh*j&ihgn9{8<}GE^GVd5~YPx3%2tSLnQ8W8Gqq
zw5AqIyI^j!7g+?g4f)hEeixLgsdXll%=eGdpOw!nvF(*LwY|%sBvl{(t3vPsE8XQ;
zUU%L#H~!MXf41+VHQ|J;J~g#40iS18&%*8%`iNjntykj+S=UU7m&)D>LgqbUh}8ng
zD1akQHYbTz$dVl*gWz@G!K_fGT95RwBd~L@OzlkbAX`_wQ<$Sh*SPoWKC}DAz4N7T
zl30|Cd*@joa>&r2f}wS;`F63n4gBfMPjHR<uCsJGl1qaQ`sSc3m?}_4Vb)pIp_ZW9
zpl)JhZ);DsWA(ZL>#x{z$p5(V{Hj<rybAp_;aR3_tuOj!k68wP#+{}f+}cp|$`f33
z+^KbSbrS;h@t(t;8!);dd>@{v-I?}SrsyW_Uc?+6Sao<aDZ!xbVOgxBi&h6wm1e{1
zN1u#K4|g&p<I*Fb?p7va=U}j`g4cz&?I20I;wgXU<5{xcIp|&vste-f94k$#Y?J)5
zsncazS#Yu^a}wkOpSq}AW7jQ*J$`6&PczeG>q)%-o>NK#epfF)I=SfeoD#@?)DtN{
zhT0Nd%EG$O8EBC`?WRFl`8{4i9el7|!e?Sx;zMadq_1%@l5zP?@+WO2v-l?Dy11Lg
zoOe$DVy_GP6)bmPfHU+FDB@)`9|K=k+%2|Djz$?ru<WV9P9b1xnuRHab0D(FX|p82
z%4CpKlNrgtngq#YXU=O0Y)oy_OKbtMB;IUa*o;Axc)NAQb)PrR6d(t1rh(zi9J|%d
zI0DK1ko{&EANldj-|8oNdyf1pcKi(8)fWItwlA>@etgHpSj55(e{V+_T$I)<wrfmz
zhHIWaZlP}EXf)Egg0+&wBO}~9iMX^?WazU)@Q<3I>6D#M=A4c~Hdi}AZhyI5P~Y16
z*M9uRGuSos`z?F9lvS{5oQ!})6Fh!!f(H-1ywDbo&ts@3LFtq|!B5Qot$5f?%zj2a
z?<LthvC33$JybwD-+b>2DH}!z`t#m6cC8Tuz)2;|;U<ZJWb5bynl<vomA(P53J1*#
ziJqc&LW{-Bdho7>iQe`;%<zpN-jX&e2e9ZZW;W%s5SFB8=UwBwo6GeR{rH1-HM;Q!
z?Qm%o3y5Y^)|waM8%IvA5J<MDdCOt{1zCi-5VHcUV#Xv)w6NZQZUH0_ldyb3ED5kF
zA<tXwwr}iiga?n9T<0c!n8xN{n0KG36Rc$H{!+-die&@TLDpzJ0sJZ3Sf#yUUA}SU
z;C_}yKB97Qu5slcmQt+DgAfHN+iP4f$2G3lOCQ61E+>yJN3Rj`!s<z~?2T7)rT`PG
zEI}U6&ZVu6JUvRT9YlcXggVivQdOlxV)njp;$)&g{P}+p1u8a6aIO@8p)Q*Nq|Dol
zWrWb=VV4mJFuoL@RJ^F9Qu2y0e$E!$f@~Gn9TkhMzA5(d?8)`T;*AuN#qsw*{+zI%
zkc`njwo@{8{Cdhn*VwUR`)t-G*BpLYQzl=qG6mlpeky5(_@a+>abwR7fpJNka1VrG
zN3Vti;BN>u<fDM6tIdXUdVH2saE-@Lbuvu!>`I6}S=C^icwwB6FLmz?X`7nF=#QVI
zjSd^l4(Bna=vLK^2Fwbiu=6-dH?RPV_rMRVLdkewy~7)VwS$Q-gs&T^=i!}=pBA7G
zv`^w%fS;WLjKMI**4Rccjs-hE4jdE^K?Di>sbZp<Rv2F2c={4@$4_5MB19Ni1QQ4Y
zDb5uz8CHzYEd-_AS{aa5VyRDGDkk$*Ie7;G9xy2T<F2-BI@C-a%#ZJV5^kmx-}_5)
zG!+h;gcp9=yzcX5D+z@sn?oxhQx!nA1vzN;kQ^&OP5YTLJZjM9VocTnMJxKU<AI)2
zU1RW%D#-`oWG~g&inz!(7tN`_S0!`NY@OTmfZ(;F8`BH!_KMB4zL3qC06`m!HJFl7
z@ku*;s&5?ksxBcV<G8;Hl?q>l5d*|bLAinb9=xbA13(zLYp=I~Hqo;%SOhV6;O)mq
zn5NCxGy33PZ+$v85E?~)8Ihg5%_$b$A=?`W$&-k=m<%Qi8&KSakoo2j$7te1rd1cv
zuYO#X+5oULeaLLq3`u_$M>39tnDdB43k8blL5-=yp)d$foPs2;)xi$j$^oz({sSz6
z%~Huce7&}BiZ{Sqk_I6}Y<WqNDTWsjVgO;3p{*RckcB@-=%u?bH~!GBlO~qp552y9
zQI35T`6&->75{UM;of4;P76_Qb2{AE{qGaZXg#W_HRxH0aEfUA<WC;6FSnDOn7inH
zaq^GKvxxA$A&A~ONdt@$SOY{8Vw^E!#wp;M&{GAAX-#DT&K3DN9H(?e5*t9i0@(^J
zmh;r~K|brXTDcm|Vla}6BCWia>&#@J9|*$C46HZ2X6OQ)Ov-`w`0*D%6BF}<rTB}V
zlCUybMb4-~l=Fd_)f2M@pgW=Md=e5(dI)$Pt{+(eb~*&ZK;5ChkSazX^ENR1wcfEM
z5?4hGC}Q={j&cn`lq9+3T9P+qx>)v{U}mtwjoq=TtTWU%dv7@zm}IGwZ*d@K0Nw93
z5uShV>}8a5$h!h6R*gBWF`w^*f7OJzx`u;UBr1@0VF4z2(gaTlDbg**Ki}jx!F};4
zaliJKwldSw!c1(4;EzkjKi>lJ)KmI+UJY_Cc{`vS5sXxu*JcH)0%iU*gM#^<I)-?m
zJP3FZ>3S{v$K1j2A5V>zjylBQJuSX5=bOC^USC7NIzO~6TRx|eg6{L_<%J98d*{nN
z!l(P@OP`}Tg^tzm3JH3E8RX&ts=6r^LHx-C2snto6*A)WSYDY`mAt*JTz`mxLLAc5
z;*|k#pwW;eGD4kEVufq~g&YE<v}V(YRS+qXgdsXki4X!AM40EL?%4W?B_N6(%O@42
zT}vem4dAvFuyw=CqslcsD-d*lzW3zvEU(8Y*9Pzi7`Tn2DkS2BQVNGaBhd#svw6m4
z8{aQCOe~pCOvRMu8~5>)YlU5irX=$^EOmVu@*DJ6LAec94slvOXz@6J3VK=s$PGh;
zj8*8&sUVdSwUL%;f(VPhbLU)Q9Fhsp^llICJ>2(Luct+27Rs};xm-4l@YgkF-Cqv?
zG;8Db1xQhR`{pHfiGnCHn9X4GTz7Bn=*~iC0lwRfJ#!~nx(#1%0&tpjfA92AGo`u;
z@3PECx^nTFQFk}Fu@^pS_Rer)ciyxw&Dp=a_%9}aHk2Z+6uBN6h(~Cg0~#*$7Okdi
zXvm48JK{%=kmDvcl@d#5kZ8GyrPF&HKk@tpf|D!U#0MJ%rIjtgiU*xGxffJXpJ3ua
zznBBjM6ita9awYitHEDN(!)YwU8DHx-k4fpw!_XrqSzxq9x7Q}y>4Mym^rpIQc0lK
z-4!#FT??I|ji{9LD4ZXQCA3!OC<Y=If*G@|;09Pu33a6cjN={TUsDe34P=1rKA^65
z5}Qi;>EzHjYI5*OvH^1NO3QW;o_SWPWR5-YoX&i~HOJO1u~8~GCoBE||3@A%QwU~f
z0Ro`l$VHB=V_PbPB(dbVrdArR$8wGIhlD%QA4tX1_y-w~RD^Rw<-w1?eH&R9WevQZ
zoKQIuuyec0aPSJ1DVn(Ex_6s02tANHCDYP|K$S9*o#}$p0e8<9D5q>vKA+9Ol!(|%
zF;JW1gR{ytB7RPl47c3^Io(WXFrexkxwSK;`@v9Ne$U}s=RG+@&t~Pjr#&8ftksRZ
z@=H8`A8Gh$GuXB+9`)Tae66u|9f=uS7P6CRX~s}q02(58Q8EVEJv<Vo4^dq3jRhBk
zE9pnbT;q}tdaRPM;QTV|wD2^-N=u<b+|ey%I(nTf-_W*86fl&Qv7e3ZcTeXf_mKXf
zoPh<B_9?Q4I_eIJZ6v;w%v;xEQ@(lY50-=7aEAruyEITZE<nV<XfC5OyK3*%Wez|J
z*axZ#a4(>pi?K8lD5s`4);B+VLzxBh!`+qOsLri^#$HGSrkp!6(DTnC8?5LSv_sM%
zgg`Bjq(Yzo2XQ=1zx^9tg!*M&?qu7cq)$y1z`{4KI)a20?u<i|Jb5gNOI+isBli_<
zNXm5=;X$r5Ac)C&tiJT|S2)NP{FS?IA*<pW-6rD)*XT}Yl#%dQU<vqCQa4!t?u4*t
zglR-oK_n^Y8w6nh<nSs_|KcpJAt=TcLY++f?kVhrQfe7H2^B=D1ttf~Em+9IK^Or4
z`U}qhgyp<WyB*og&t10X&~l@7cNmILa{1&(5%s%+Zu>^hDL%5R1dk<ds(6<)Y|jyw
z-FfVg@NEP#`R<dSi17d;M;wGy*#x-TqLxr-kO>6?anAw#8MbAA2?f;n${e=%=2xG9
zU`c>PJkxAg)vLFc1x#WOfahSf1SKj#CGhx9UsTLWCfVGlCPq00$PJMHtU?yRe<lgV
z6j9`YQIWib_)-vWrwD^%A}#hoFt){7;&55W%rq!i<2)Wi2;z?X=1puw@s4D;QdR`^
zYsF%vx?&Rur(vrQHZurxji+yxt40|KfHQ|u5={@;23Uh0t#Y!RdB_OHQGozlh@JA|
zoASE2mg1Wbr%*gXwj9-q_^Y!>MM-W+X*8k^9DPoi&1MwcQTB<mD@0yG2E4jZEt^pB
zIOHI984bKR*F5B4>=*WzY_N10l_rBetem&1>rKKG(zWoSNVPLcP5OsC3<yez^Pdd$
z+E2uP1~Ey6$!~TDQIv+#N#vobmlw;T0wU{vM369tEvFV{!8cx9AcPGR=q?#Ap2MG4
zpmF3~U}dGHmM#_MW%n;>WALOPikG%v45=0^Kvo}2ueeBA`;uApESFJ{QzXud1Q*SU
zQmSiK{ee?3Na|=Cs!HEqZb6xX-Cbq*3QBNH0{{eGEF(<EXj!;MTSLEOrzv0vO||al
z``KD30Z<v=*yc?|WU%d~-f0qQMQ)M6=}_yH-Ui>8{=NNJ`k~fe1bCe$fLio6JJnm7
z|4poM%-Lm!S3q=DnYX^fFhc(0TfJjlV|uCYmmIPjGmr7AlDLSERYSf+uOWDjyzscr
zf0Pkh!d`=79B-o-DX|Q!MU>LuK8gNPYSe~Mt1u`?Sc-o-e%eGg{^<myPjf0)Qpmu6
z%aGdqRu6K;pT<;)l7km3ry5p#yb6uu942vBWEjKhJ3C)T<+MR6-<UU_9Ule$u&o6P
z=n0iOQa%w3wv%Ix{G|#-kxr`EA#xp(XgnqS^1(nONI*IHHXG3Is)N{OrR;We0>CZ-
ztB}|s6V^^?Y!txSxa5xtFVuv;5~&Yp0cAxZ<0;FQb)~AR4W~zM`R2uYk-!8duh2(i
zGSSWBnwP|AHc}VL#}cL`J+BMq(1Mi8@xs^>OurD1m(1xG(fWj85Cu=H4~z3Uktdpd
zA&<?76HjwPL&e;xRl&;_oOD`}2m0olN8d}Up|MNm(f5c|u~YHTkpo*R%Fjsi(7wB|
zTv1n`7x6xDE{Cz;OraAD%ZH5$;=NEQ7ocnfu=MyRteu5*Q%gqS4pI>O+nWYIhJ+M2
z!4{h`)s+SsEDhzSog)D0{4BW@6ha|THh}cZDq6E_fe5u5pjV}@`pMZz?f%?lgeH8z
zk#fzXT2b)jFfsamN)g3g{*rQeeZIuY__8NcMz;bjM1`)rDJ9c#!JK0w{u-NaCz*;|
zLf)eav}<f$*W22&urjwGR#;-d<N`2J$Q(wc_!5vO(4f>pq>Qu&VzF%**uKH;p<;!b
zZ!d$e2uG1^X(?DvhHwgij$9&s^o_AsgtAYGnoxZi9uWVakgziaK*<M+&5$HJ?JP%r
zA2sG~0!V}@0;Ed&WO>vS+&Y0lp)T#D=y-#y4d*Ysdha-|A(S8%oMV479mzfs#-=g4
zs0Txqu3m@?OIRK@3SWg>Ho8XP(j~UXqKNda%yHcIHDCne*q;EHAG=WrIGLCVnUgCN
z667Yjw^N$;?;YTY%pAzR2u)1ZUqNjV`%CjuyTo~0MQ4C-Hr%Ht^klOXdgE9L0J~hX
z;l~|8HqYrU@^;|HKHBA*+2cDi98y6);Y_o~A-YC%EDR>`3w&aLgvsw*Mq@|=hen`m
zj$XjNEjB<E+n2i!UuVBk!{sA{@?Odr0zgGcKr$G$A&;b%-}NibI9)U1jLVZeJA0jd
z%Es4>I34YP88o>;+^;zpye9!#LS_!FF}0&}F49$D1EeU+$%Qqw`etdDVg;p?tE=zr
zZ77*{{U+4;$Y+zY9d^n|jOe0wwvH!6{Mzxo4N-2t@*T!=uKB0AT_7W>88*RQWZxwu
zcFof3(QsHotf#*zhBq!H-v4QCo?yA$fX!W8ki+hGVC}ehC>$3x9`Zt>;YiL!srGKL
zC`tn7NpV9@1z`8}XTV=TT(DiY@|mn}9=C#Cl$}W=O)30Ll`}jmk)Y+YyXJ8YJ^&xk
zEz7~3-d}*(B(vxVOeJ?huERI3-l>@|JRnLhSk*Ug!lNbQ>X%fHVMh9OC@cIOm+ye&
zF)xZmXu=~r%gWfP5+pDWNjsMT39q`DaDut`MjFywe8YYaK)?f&<Ho@7;L5pZO^}KU
zT*rZ5C)iX0z1v|938Ju7gnVmp<zyLGng<Y6;*q0<?<cP0@*?_UCUbwx;!fysah>Y%
zEz`f<MDroY;3k?!_DUSO{tA-yL8sgf^qP3Kw?|m`%B-6^WD)X`ZsO6aw6~A}9X#`C
zMy)6iYA-OJJ@;xPGPM`rE?44(PtHT`DDmv$TuV^z@ORLsgR06CkmaJ)=}JIr8;h5E
z#fNgFt{;$QL@}=ZWp&;3eTzY6>tK;v1s4&;sBA4Z&$S~xf2%-i`9H~=a<&x1^@+xM
z$A$wC%}El_2hvng?TqSG1i8hYs-OBuXuI|i?L;pnQ0iA~AcF65{ULS_XYY6UU2J)I
z>9jidL<O3rhE|uC9nX(I^Tu|vxEYH~svrN&_(jTrz{<}C+T{WODwobGG}=;g3~J`o
zTdolOoXH~LENToc#*_vo!+q39gkU#_J@d+KBJ#|!=LAksePghu-Xhn0b0m4p)aDA0
z>7tWR11K6>kp%BK1qM#$pV&CVa^f@23aKwLMcGS8k?aS0BA-O#DW8&^sm*<TfIvP{
z>4|Fy5Z{P|iYFU!<=5aqj2YwQ%Szs%a_#URhdek|;W^jXwwptUo=iYR2-lc#LQgw2
zT>Q^L(V*xoIKH<(e=yQKm2el00+SCTBU~g^cqO~?a-|eTiWV*v7-jmD#`=`SJQSMJ
z-J&>l{wJvZ_~z6#sOXqe-HL@-x$>;luJLIgQ*}jm;*|gBcdfJjw|bK5Ac#|n?ori0
zr$-|dbc83poT}J##DFsZLP-)|xQTq<g)fj60N2Zn;a_NZFu!&lb>n}n85yLsjZ6g0
zKc@;Rpa|u-RHO^;53XG=N{k{ALXIflsAb<-A33OE)4NWjWy=*r-w5Wv{tMy>ksC`O
z7vC>mgvx#Sx4&ta=o`Zypfbqt`}+<x?=vPD;&YKuE4t$kf20p_*^H^jLdqWb&hCAm
z%YR#tRiwpqvKkYsiL6u|XM!rJK|px+Bt=u$3#MtwJo`i);1UW@WNk-6WWnDLl&tx2
z(T*YH8wdAUGZ9oS<-lo*BO03hd+zl{73urNtydxyYTSASMT*m*WZ&B<wSYr&ZBOLs
zSss*iLNQ3|&*zR>N*0#P?~jx)7~M$JvHSfIGSC<BS(IS`NgxLZcNKvC^QUcDwAu2Z
z2TbMSH9}CR?JP%Q0j8F_CS~=_>z7uL>8(jbCfB@vS@f~cn_u3CyfFYK5~m{7T7l68
zK10(0y-FEOu$r?<6-uHk2AL(_95)^hIVg;=Nns0*=Is*%br40!mU1jT+#VfnId{TY
z;r^hsjYl$I#hc@GY6aoJ7v87w_|2SeLZT8W4>ADghg++0B}47$JC2SF7xh1&h=a2y
zUK$1u5OBGTzHSRKBZI#*(t(nac|M3kS{V@yA~)nqVV;!ma1_A6qp?E+fjl@tkrTk8
zM0;po4GJCT0zS=BGUh#iQWqqIyr(hmeh@LJ(I;jfMRB+CM#AzDz^?`7)gNZovj3`h
zUKD$4qeDfUR_U8{LPA!XR_PLXgXUonqLR@(+@U_q3il`M*xF=S7)IR+S9h&Ld6m@#
zdGtW`?A4%r!=I_ty<Q7b9Dv06#`8@aP?U`4&nD?3#1Edn4n%=P&`KSYiQX=c_YhDW
zaphK|w8V~}6X-m)Q`E20{jFw-HbkCEbhf3!thn4F2KVE?J2Tq5*wdl6^<}rLR7Bwk
z(hs*>)tJG7oA_tfz#jH91SYpQ9f2q|dQr{{+4W6xm1YpD&Bw`e9r-Z`F3fAmG&^Y!
z<*Z1enbsAV?Y?$(&~#=9hg-5<q}y;zfL&+gGQ#|(Z+!9{vU;BsqjX3EmUGZ|qn$w!
zE^!oPWbWLntZtI%BOL$}g-u|ZF#N>h0G9J!!rZVd#=MuKNFStp^!{d1y^^ILkd4kH
z;W2WKvIxXBfx2Jky(|-fY<q|1P*I@ri`>!yD-daUs+0OcD^fr;3$or4^c%x?VNuky
za+uv&K+lXFr5!j{GVf1Kan1Xa6Z@oxsG9cj9oVR+qhaK|D)SLIakXw4%o2`2$;X%2
z)F4=qJd%4lQ)L_Jyg_7783^kEI>k+{`5oYaJ{^M4lmA~JjDQX?k_MSqtXWmf`f||e
z*Y6)S%N>MLL~-GmJ?y6wn|3o#Df)L4o8AxsusA73UDKjA=lBB)znkf;a0f2AxJ-5&
z1jCy|-_Wtt2(g3A%jwWEoOt_-GM83;{*55Wz~7(z{}dVQv+vLb_ucdX5u_HN)K9#9
zEVdU&kR5Q?%nL+5HEK{VPmzIt;=ls`39b7H{OQnWwD-rf4TME-<zQ$JqI3(cQjOa+
z7q@|VC38}o@Puzp8ldyC+8-)9DJWG#E=gwUD3wu>WM+#1rUf0AlZ)c=NLv-1>C{uU
zqg?A7$xGqj>4B()RXhae2OMuCFCpt-c{JkwJNnQ=ubTKsr#Yyd3{TA25NJ4=0dg=N
z`ofWEEaYGk2w9-#3ni~pA$S!npb==STJoAa0&TwHbmkFWys`qBpH4pbN2I``s&;{I
zkoKg0&<;jNIMzo{Nqim9%=9+Ttx;Dll9k2$%7zxk9w<GDtS!6*?7QQeGe=Q}A({>U
zqu3jB<GaV8B2ed689!{~22>xfg7B{SmAiSLY$OtY*;_^;4mmdL6@3|anlccuMLb%)
zoEq<C{P-*5^OQ*}#b22aIt<!iv>^tG#0L$MD2D2Iq(Z!yjREmcYsaLcEtpl#AMwsN
zc8#Hf0J}yD4gwE+faVl<lRz}_AhW+~43`%uZVV9KQTvDnsDU^W-+Ld{y^G#82=%#m
zg*Tz*!+^d~^B0W=ZdLIeVu06|`X!_0Rbs#jH-6|vy)l14{<WTrJ0QQSH|CY=F-7BN
z8HRZQ5Ii3K3&g>rL-KTVqvlnRJzzeWKds`Hf7H;#kz)pwivH-y_{z7Kx0hp%`0jX5
z#$zTMn8P=3SQIW*2F16(RMtB7LWC9JJE=kwC{Y=5lj@}rH|6A{?#8q46TM5uvwJ2-
zAO~Yq&-|>PFw7k}rirPw-+<OlWUuA@g3E{pwC6ywS4V~0L7GsgDD{t!jxzlL@HF}7
zCM5{1$17oN5I=^aAV)*s9VeW+a6~<7WDHBy;ggaqAw+N1EQ5@<*rtUNhB_$9SO3OR
zFi1#rzBU;N)y}`lGeHIR@u^Z`ZF7MNw(_zCH?elf5{?~%MM(I|GXnG}Br<4R^T<Ul
z9^x1NAWNN+=yQ?u*>B~-O?>%jg)dhWOVv$plx1^w9_M*peHpE-#;eGZldI*escy&>
z#h^TK-+pAb_Ua4E+|S6^l9KGNzC_2t5Iq3d%jF29j2;~0-FhuU&oEX^KwLR*u*z;h
z5Ui*b6MU$8>&J9J=DPI-nVS<q%tVetUE|$JWJ@FG4_@Zc3KaT&(&6~K?JO^0xk41E
zY&ZUH26{-h3UCPw_75!VWW<d{z&}7c@r>4Jh7gYr%`+*1q}2vP`INH6?a^V9m9SED
zZU9qKIRq`XiBn%tJRvHa@~EIFf#YXi!^%a2jGDtWp8c!roxn0^5BsdbJ+^cetbHPT
z!F(7r;bW9F6J-V(6?T+Z%!icq`Jo$n?MH4U%+rvbQ!}vw^ZFM!##GrAg8gt~vC1z~
z$!y9cm|c{JVCP+P%B9j>V=Dk{Rtkr_m+j=BrWVZ?UJd^U(6Q_#`nGlgjw@Flxs+n2
zntqU=8?@jdG)j?)pq+-!0RN0?+!M&BMENHym9ye~np$|TDi1{7l`=q6!vy&B&^Tag
z#&f;AHP?7<8)Zq*&_t!r$|MO)+Fy^TpV%1SjK*`@IOT}ZDxN{Vz9;i-+;^sL?3zRR
z=>QWInSp~=a))UtzJ3kX;m6mzA`IvLTtvf^-m&EU5_)n3N)&cXfp|D4j}C$sa>XEz
z>N3L|(jFqd{o~j+_G2Os<zgmA1Bwxm$XEaT2{zVd^JXQ$o<*nGLa`x{FRx{J603F1
z=ARSw2n47eL)-#`Hcv4ER;A37Iy22trEhE<M*YcKhvHBe9m%Hw!d4M{Nz%i)h6<{1
z(u>Z5kVHc#L;w-s<e-b8h!av9<mNCc3is-a5Dq<fm`-XE`bX%x8WJoG*@asrJJyee
z4E%N++G=ika^Yfh160ug;7WNw-?^Neh5B60T;RC>&t$U2HO_q=@>!W^V#x@2Z#u{6
zSz0+UIAT`S!>>uP>t_&FWC(9dZ-@}&qHy<w`R9Y77bWx0BTm9%160Ap2`Z3BOiq(Y
zIx@PG4?xlpP9*BCU=9*27bZy~q?{x|B0{UlJ!mWMhpZKbry2TS&N-XFE^a?)f+*y(
z8Df<X6^=OrI@U<uJFK3OY;O1>Q%_AMn^<K%edV@3pO3um4l1?<+|vkoRjpK_2i2&(
zM>9Yrqjm#NOmI8gjWU^N&}~}4r;ehIGXlans=!SKBToMw>s<7rh|xx@*sGCWk_gQQ
z5;<|aHfn6RZ0xZ6lYL(RIN<81Yfk!K%$vT`j9j{^zqbNN^1u^@Enzy3IwqnsrKnLC
zas)n7Oiibijqax%P*gdU*(eIHraTEFDP!9gCr|8i6#!Cb9T00U!8OgxX3G<Gbm%B0
zJ30_{N{E&B7UA4cki=gcEo-J@ab)u#EOLPYNKpzVe5Yh)4vD~*nK=|NS<K=N81yEc
z+5TrtQI{ZADXu{*bION+Smu<EA{!Q-LD(<E`b{SQff6K`ABZiw?e4@5(UJFkfwrhq
zLY@q-Z1g6O73d)A_A4tuR`?zH_12L9S!Qfdp%P@Nq=cS`I7#Lq=s@oQ{F!;lzso~R
z3n4do;isCofQn-=07zQvm^|Ym8e)vyzfhe80AN;n&6s&<Gz8p>_5##~`Iwb!ym&@u
z2Bl>NN#abh?!_>KY&oVU1>)47sy=-I4j-VpjPEG1L|2%Fep>65=jff}n1H{{`F`B{
z63GA?eQ|V+)KSNaEYlNY5T)<qohMXMHN;;k9it3{(gXlW${QT;SuJQzLx^803;3>i
z{Q0=9z&!rT+o@n{-AIC-c4Oa}n|4j>h9oJ1R46YM2<3<Z7W9i*H)x>>df!Z|z3)@>
zP^dpJXj0RJ3c;);e$oWEz2jo>LD&^=`Zz^U?4OQ>BzYlxHiWRhJSV^(>IlKbwJ8vk
z&{g>4fg@%>9+F66)^)4%B6cc#)T6EpP6?^kBhvGIZW`tHUPNaWA3jc>%B{MwMACSi
ztKOGWNfJgg;mPmO=|4HOoCd_$d>(GTqb_7|e-Jbu&3UNWKYXn4SXxi9Tq?Ih=DFy`
z$x=VQ@d^@ODMp;K*?46|uQCB23T^}}3Zj;N3AoVaDhJn{SE6l<0#~ZgLe2B&kwvpT
zK`p9;>YkMRF&cdS_zmIfLli-I27rfP8qyEpCgk;K0B78PA7*u-f!ZR}O=a?^0{9{B
z7Ng657GD=${xhY&y9~w6UaomfY+=WmOJlZ`V?B;;I4nbQwTlGB^N_b&@?pGRir<p6
zk$wi8O=8O+6p0=VCLnIX6>0_k5m!Zs>-EfQZ)^r9Du)f5t;P7h;XSNf@P_lcC^EnX
zc@JsZM)Mk|M~B!lSzvn{e#m*a1cYL$0xF~7TEJLIQ1Lij*k=BA&^c%UCm&*5{U(-<
zwz%C~FDc--lP-b-|Ju79`3z`vYrLn>DqI3V*w?5^ZwKP?EEz;oVv{52ifVV7L)?|V
zx#jz~e-Y4*P`ztzxl?plbT~kXG(eJXo2hZ?;Ip^f*@r;1TSzGC?Gr0#fP(_8oRZGI
zvE_J8fvU#EP#J(!Z*R|13unq{#j*UK)#y8^{=%d(rvwB5qe2OBs-_2*3E)6-=<>_8
z*!;d-nTW8*9lemaFAn(`+n%jhzyOMTl;&h97a%gcxk4B;qC5DFd-vHd>Z88##xFuK
zLkj@{A}A^KD&mbTd~+YJ!0Bv}-XDw5E+VAdgq$}LzMVTMLZuEv8jFKpaYGdMYKjS%
z7$RDRCQE1rOau+hLZ`-E(<pRmGp^IZwW3XY!K3Kj@)ND>|7ayk_zD&6meDN@@;=cs
zMUkDfPJg*5FXIw;7k2L`l$HJXr?+eL9B6e{0CAGUmJJ9hIL;GVi1Q-r*otukMjbh#
zJ%e}z5JP7)V3&CO(ENl9@{J8=5~?g28|DfJIhhR`WR>$m!r?%Jc6~LfB1?ZyZAH57
zR1F_1?uLQ>R20E?{7IBXNa8{kg{oCO;P2QFrSxf$w;L^;uzn?R=Yv2l)dT*aJfBL`
z>+`aWr8mRA1A;ZKQF=>Jl3*TYp%WhzAGcF=W~hz2YUwRv9nnm#OXN>r0bpGzbD&00
z-bw#}5~?DS;v&6t9HE#up&z89PMC(0*)frw7tN2;gN(aEZjh)E6THcRKvLXUMBo;*
zK%T;`Jp7^=1X$*WHlrF4f9U755vdr0X*^Gq`BBbL-@(8m*Ouu<3~aTHY^YFG%o!pS
zF%<an$m#T-M%j+=Q)<!hjh}AR*240F?MXxqLs4CBCIiie2DN{AIb2>KYivu>T<@*+
z<GcQZcn{YXvEigmX;ZlIUC*a%v`=P`e#HX?k6I~M?!!In&&vq}5B&He7fV1;ia&yU
z95$?t?Sa;WGgv}IkQq@vM8NDW;p1seIeIv=Z%%$+A5g!&Qcmoeli%aKSJ*GZLshPX
z%Ij?8`(8V7&1*0aM%OnmH@Q7jZMv@G(MWk@{|#M3A}{2qypM>l;~4sfS!7RWkcwr{
zNZM5%ecnVM?G8QccPfOEt0NiqjhoksY!T}((=NpB$bMj@QL+U(H1OjrS4Bt*!{<Wm
zDRRZG`P@5AOkfWCxi%+mBGE)wu7S=;8|8n|aDokV%&fe(n}i1yQFu`Jg2ZXfD!I&-
zF$x~Tmw+^ZF3_DTq>i*k#h&sK=sG<PJXywpRR<6R;*t5U_a6s}+nec*WB>^eki(e=
zk6PG5<xp{?*EJUHM!e>=`NpC*gx$hH73v%=;Tx4Pl(&E3K0MkoJ|$$*f`fOsHU<z+
z5-ZED(89$<=uE*z=~M%i2!-T?c54yt6HL-A557_OeSNJu^n->X(0a>4QJwKx#Em9P
z>9`0Q$Y4T|PVgwkDWHpl$}(OPrz{IHLts8}2>If|?^*D~yo$!OAv*6)qQs_=FImL(
zX!$JQ8JXwsXfjf@)uT@<bIzPwxWv~8h4|SXh~(fO&GZU-%!ykTa4`|Cj=&F)NcwMX
z&CJL&7Tw&L7tkrrN|pAFKj1KvO1sw56%((VK{u-X;c8(~1OkUOBD_kyO0w09eXyRt
zzUpZRY9PEs#H$J`B98I-#?srP1J@;E={idJ{a<dT^R|!5H9{S<ppeQ6dSo(i^X2Ri
zLsP#GPJ;}|7<=FeDe%sme-B7hGUsn#j=*S<wGa0Lbt9poJJnFy75!#pCbcGExO1vg
z{QYB|nH^%-fkhAo2bz6zXHi(+Fn=Rbe3X2wbE~gCk8ucJvyFo~@bl)*)uNz4SVxy=
zPE(W5mqTkdn>OGZt6vl|(XNcuFOb(~lhJ?LmM=oV_gtuu#w(9GD2@GxjeM~X`c_3?
zWM!1jX&UC6bf&gsrno*sSy}ypcVdsF&Ub;3?D*^4s?jetYLyrY8oeoD2|%ky_~u9)
zXeyZ_-{u^*YRToEL46+7l<J0K$FR%TCmbH9ro*UKnNb(Rp=&_d4(!`E5B`Xw*phkh
zhZsP+1Aq_slQ4v(3nANdJ%a3cr0b@TuGmKlB%P>v_SDg0@{)P#VUgY;wYvUqXYo}T
zu9=F{qFHdL&xQ`Kqqwu5R+}IL5>uaK9|t3+TtclJzIoc=+V|Bz_@YWdDT<WL(~gk0
zKhVR9J|LrgW`78d0EsSzayII2n|fP6**!W2G;Hm8YFgzL`MMFPZ~xbc$@6g+zNuHF
zu%rv$q8<xOv=Tvb7kN8UMr5IJ@i4Og5jTBv?zuYdf-tz|+(p9rrm}Q*WQC8ma3ux`
zWKuI>rX`l<><1~9r>?Y=`=x{m$5PQ%9i;jwQA%KqQX3R!=T5=ekVyaujH}@#BCj6$
zrsn?^6%BL#>l)63LEOa>DFSLKY%*Yg^#1nZz7-9^`#D+BFjrkKi5f|1^`>_TYvH;#
z*q3lTNm#~j=7?vaFWjnC_wD;UTg{Rz*-W^PH8&iM0-~-L_wy2$GmaTc<qX#x@msx|
z!N*+w%gPxM(ujZa*9|zNzQDEHJKE5HwU|OyuQ7){g>OC$jB%Jv7{hC%)L13F2nwjo
zK6W%oV4swNq}ObbGR5d0+(qfiO;54_`o^ZG_{<K~!@`Al_4JE1LNbvsj=rnRhKsI|
zBR4N%H>5nH>q7>9<2cH$9zCyT@#;0B?v6O-4)a!&DMXQL5pHMAAd1LK#+t$X#+Yb~
zl;=ow->SkYm;{ALfJbh=78^$+)c$k5Vd9+<nr_XH&s1`=qPTCWm&8J}IgsiKk<o3O
zXd0YSK_3o+`EuS+OC#W5u2>D4#~-EpWc~P~+Zi~}?m7R$^=%D5C=ieMD%xZGon73z
zE|0}VfK}3zBKB*x5dVSeahiE6*DIokNX8F*wg8GJAwOj;H65nR!?)&E*xqP(GjY8l
z8VSUTOO+iY8!IlLQ_jN2vl7-|Id+Dw0R8+q1S-NJJGpi^B@wq$?M*I2$HLs_rB<WO
zEvvg)P6|g@WloBI(al=?q8pA5TqLFz(k0ZZ9J>oSsmpHQfU+#lTbRe+13%%L$8Vr)
zA<BSsAv>>|0ULar$fb)Qn=)%i?4q@lQ(PQl&>bFmx^x+<2lA)mIg()Dgm0YjD=WP`
z3)-}yy+~X#0I-g>`ZIPAr_?W7@mAm_Je&#*r^hh@<9zxx5f~AK!sYuiyeD&+mowm3
zK!^Z^$wV>Ga$Mxd`2ahWstDAk%0P{Nr@{gJx!`a82WsLM*@#~^A;^SH(dOZwJE2!v
zuktj^_)#p@7U;hWiGGFA03QoT#H#zhalhY7w)(vWum4}p)9-D={r*yj{(lWoe^-R{
f_d6-}^!uxm`u{yld;0rrNgu~z&fxgV`15}N6mG_H

diff --git a/Robust/Transactions/Notes/sysgurantees.tex b/Robust/Transactions/Notes/sysgurantees.tex
index e2329d4d..ae99b4e0 100644
--- a/Robust/Transactions/Notes/sysgurantees.tex
+++ b/Robust/Transactions/Notes/sysgurantees.tex
@@ -18,44 +18,47 @@ A Transaction consists of a sequence of operations. Thus, a transaction can be r
 
 \subsection{Defenitions}
 
-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.\\
+\textbf{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.\\ 
+\textbf{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.\\ 
+\textbf{Def 3-} A read operation can only see the writes made by write operations sharing reources.\\ 
 
-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.\\ 
+\textbf{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.\\ 
 
-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$.\\ 
+\textbf{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$.\\ 
 
-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:\\
+\textbf{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}$ \\
 
 \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\\
+\textbf{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\\
 
 proof: Follows immediately from Def 5 and Def 6.\\
 
-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}$. \\
+\textbf{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}$. \\
 
 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 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$) \\
+\textbf{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- \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.\\
+\textbf{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.\\
 
-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.\\
+\textbf{Note 1:} 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.\\
 
-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).\\
+\textbf{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).\\
 
-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.\\ 
+\textbf{Note 2:} \emph{No Commute for Operations Belonging to The Same Transaction}: If $op_i \in OP_{T_i}$ and $op_{i+1} \in OP_{T_i}$, we never commute $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.\\ 
 
+\textbf{Note 3:} \emph{Precedence Relationship Between Commit Operations Should Be Preserved}: As a rquirement we want to have the notion that transaction are executed in the serial order imposed by their commit operations. Hence, commit operations can not be commuted.\\
+
+All the rules explained later are based on the assumptions made in Note 2 \& 3, hence these two types of commution are ruled out by default.\\
 
 %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$.  
 
@@ -65,57 +68,42 @@ Note: \emph{No Exchange for Operations Belonging to The Same Transaction}: If $o
 
 \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$ \\
+\textbf{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$ \\
 
 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$ \\
+\textbf{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:\\
+\textbf{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:\\
 
-\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.\\ 
+\hspace{8mm} 1- If $op_i = {commit}$ and $op_{i+1} = {read}$ and $op_{i+1}$ reads $r_k$, and $\not \exists op_k$ in $OP_{T_m}$ such that writes to $r_k$, and if there  $exists op_l \in OP_{T_n}$ such that writes the data $r_k$, then $op_i$ and $op_{i+1}$ can not exchange positions.\\ 
 
-\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.\\ 
+\hspace{8mm} 2- If $op_{i+1} = {commit}$ and $op_{i} = {read}$ and $op_{i}$ reads $r_k$ and $\not \exists op_k$ in $OP_{T_n}$ such that writes to $r_k$, and if there $exists op_l \in OP_{T_m}$ such that writes the data $r_k$, $op_i$ and $op_{i+1}$ can not exchange positions.\\ 
 
 
 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$.\\
 
-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).\\ 
+Now changing the $(op_i, op_{i+1})$ to $(op_{i+1}, op_i)$ changes the behavior of $op_i$ if and only 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 $op_i$ should see the most recent results and hence if there is no precedessor for $op_i$ in $T_n$ itself that writes to $r_k$, then $op_i$ sees the changes made by the write operarion in $T_m$. These changes could not have been seen in the first case $(op_i, op_{i+1})$ due to Corrolary 1 (No See in The Future).\\ 
 
 
-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$.\\
+\textbf{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$.\\
 
 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$.\\
 
-The same argument can be used for $i > j$.\\
-
-%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$.\\
-
-If there is not a pair of (read, write) or (write, read), sharing resource $r_n$ in the two transaction, then $T_i \rightarrow T_j$ according to Def 7 and Def 9.\\
-
-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$ has commited after $T_i$ and 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 $r_i$, according to Def 5 $a$ precedes $b$ and $b$ does not precede $a$, hence contradicting the assumption that $T_j \rightarrow T_i$.\\ 
-
-
-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}$. \\
-
-%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. \\
-
+Now we prove the other side of the argument, that if $op_j$ can be relocated in $i$, $\forall op \in \{op_{i+1}, ..., op{j-1}\}, (op_j, op)$ is not a pair subject to the condition in Rule 3. Lets assume there is $op$ in $T_i$ such that $(op, op_{j})$ is a $({read r_n}, {commit})$  and the commit invlolves making a write in $T_j$ to $r_n$ durable and a precedessor writer that writes to $r_n$ does not exists for $op$ in $OP_{T_i}$ , now if $op_j$ is relocated to position $i$, $op_j$ would precede $op$ and hence $op$ would see the writes by the operation in $T_j$ (defenition of commit Def 4 \& Corrolary  2) and hence the behavior of $op$ would change as it does not read the same data as before (the data read before could not have been the same thing due to Corrolary 1). If the pair of $(op, op_j)$ is $({commit}, {read r_n})$ the same reasoning would do.\\   
 
+The whole argument can be used to prove the Rule for $i > j$ as well.\\
 
+\textbf{Rule 5-}\emph{Operation in the Set of Execeuted Operations Belongin to Committed Transactions Should Be Able To Precede Those in The Transaction About to Commit}: $OP_{executed} = \{op_1,..., op_n\}$ represents the set of executed operations before instant $t_j$ and $T_{committed}$ represents the set of committed transactions committed successfully before $t_j$. If $T_j$ invokes ${commit}$ operation at instant $t_j$ - then $T_j$ commits at instant $t_j$ if and only if operations in $OP$ can be commuted in a way such that $\forall op_i \in OP_{T{committed}}$, $\forall op_j \in OP_{T_j}$, $op_i \rightarrow op_j$.\\
 
-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: If all those operations can be commuted tp precede those in $T_j$ we could have $OP_{executed} = \{op_1,...,OP{T_j}\}$. This by defenition of transaction means $T_j$ can commit (it is executed in its whole entierty).\\
 
-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$.
+Now we have to prove $T_j$ commits only if $\forall T_i \in T_{committed} T_i \rightarrow T_j$. Now we'll show that if all committed operations can not precede operation of $T_j$ the $T_j$ can not commit. $OP = \{op_{T_j}(1), ..., op{T_j}(m)} represent the operations in $T_j$ excluding the ${commit}$ in the order they have occured in $OP_{executed}$. Assume \{op_{T_j}(k),...op{T_j}(m)\} can be relocated in $OP_{executed}$ in the standing \{n-(m-k), ...,n-1) but op_{T_j}(k-1) can not. This means first of all op_{T_j}(k-1) is a ${read}$ operation reading $r_n$(each transaction has only one ${commit$} operation). Furthermore, this implies there is a ${commit}$ operation by some transactione $T_i$ between $op{T_j}(k-1)$ and commit operation by $T_j$ and $ \exists op in OP{T_i}$ such that writes $r_n$ and $\not \exists op_i \in OP{T_j}$ such that $op_i \rightarrow op_{T_i}(k-1)$. On the other hand since there is a ${commit}$ by $T_i$ in the middle, the commit by $T_J$ can not be commuted in a way so $OP$ precedes it without any operation belonging to other transaction in the middle (two ${commits}$ can not commute). Hence we can not have a sequence where all operations belonging to $T_j$ are located next to each other, this contradicts the defenition of transaction, hence the transaction can not commit.  
 
-proof: If $\forall T_j \in T_committed T_j \rightarrow T_i$, a total ordering can be established corresponding the precedence relationship and all writes made by committed transaction have been seen by reads in $T_i$, hence according to Def 8, a consistent sequence of transactions would be provided. 
 
 \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