{"header":{"message":"WIP","description":null,"timestamp":"2023-06-22T10:02:16.621259212Z","authors":[{}]},"hash":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC","authors":[{"login":"paradyx","key":"6haf2odGMeVaBH1hYPXKBZAYaktbbMcbxkvUdyZKMhVc"}],"deps":{"hashes":[["A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC","WIP"],["AA",null],["Y5TDO2A5LSBCUOIN3366WGQ5QQAOBRUI672Q7KCIXAZZCQCUC2KQC","WIP"],["KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC","WIP"],["JCK77YLTPL6VV5ZOTMGUJSFZ5DNMS3MZGP5UQLXYW6WSMEK6GAQAC","WIP"],["X7SPUV4CXRX7D5KKL6UVGHC7JWRWCA4QAJVVQISE64UEU7GXJNRQC","WIP"],["DDNESFMD4LGNTDGTCW27FQPCOR5Y5MJWN2TWCSIRNBK6QGBITBRQC","some more theory"],["RVA3DOCNBWFBWA2MLC2TVQOEY25AUCYGEJSWMD72QRQ26AFLVZUAC","More stochastic"],["6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC","WIP"],["HF25ZQRDZXNE2IM3YGE3NAPWGDE3U252H764IBIJSIZS3LRLYIMAC","WIP"],["567NUQ633R5ESTE2LWXVUGM7XEZGJ65IRKPOCDZJS3JE5RAMR5KAC","Initial"],["QCVDPRXH57UFLU4YV3P2I5RQZGCBUKROYUZHDWOCHL43KDYN7MPAC","WIP"],["KUEZAMEH2M3K6EDHWMYXQMHZ2QTTH4KBM5CO7A7EB64ABEWRE6WQC","WIP"],["UVN5HOW3H2OVESJ62UFNQNS6VXHI5TRV22HQ44EOYU42453SDD2QC","WIP"],["B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC","WIP"],["EIPHTX56WTRFBMBNA4VYMKK4L7GWHA4Q2AQ3BCG2ZGZB3DBRENBQC","WIP"],["QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC","WIP"]],"deps":["Y5TDO2A5LSBCUOIN3366WGQ5QQAOBRUI672Q7KCIXAZZCQCUC2KQC","KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC"],"known":["567NUQ633R5ESTE2LWXVUGM7XEZGJ65IRKPOCDZJS3JE5RAMR5KAC","KUEZAMEH2M3K6EDHWMYXQMHZ2QTTH4KBM5CO7A7EB64ABEWRE6WQC","EIPHTX56WTRFBMBNA4VYMKK4L7GWHA4Q2AQ3BCG2ZGZB3DBRENBQC","B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC","UVN5HOW3H2OVESJ62UFNQNS6VXHI5TRV22HQ44EOYU42453SDD2QC","JCK77YLTPL6VV5ZOTMGUJSFZ5DNMS3MZGP5UQLXYW6WSMEK6GAQAC","X7SPUV4CXRX7D5KKL6UVGHC7JWRWCA4QAJVVQISE64UEU7GXJNRQC","QCVDPRXH57UFLU4YV3P2I5RQZGCBUKROYUZHDWOCHL43KDYN7MPAC","HF25ZQRDZXNE2IM3YGE3NAPWGDE3U252H764IBIJSIZS3LRLYIMAC","DDNESFMD4LGNTDGTCW27FQPCOR5Y5MJWN2TWCSIRNBK6QGBITBRQC","RVA3DOCNBWFBWA2MLC2TVQOEY25AUCYGEJSWMD72QRQ26AFLVZUAC","6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC","QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC"]},"hunks":[{"Replacement":{"inode":{"change":4,"pos":6845},"path":"main.tex","line":16,"ins":{"up_context":[{"change":4,"pos":81}],"down_context":[{"change":4,"pos":166}],"flag":"BLOCK","start":0,"end":149,"inode":{"change":4,"pos":6845}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":4,"pos":81},"to":{"change":4,"start":81,"end":225},"introduced_by":4}],"inode":{"change":4,"pos":6845}},"ins_contents":[{"Add":{"text":"\\usetikzlibrary{external,shapes.symbols,calc,automata,positioning,arrows.meta,decorations.pathmorphing,datavisualization.formats.functions,patterns}","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:148"}}],"del_contents":[{"Del":{"text":"\\usetikzlibrary{external,shapes.symbols,automata,positioning,arrows.meta,decorations.pathmorphing,datavisualization.formats.functions,patterns}","pos":"DDNESFMD4LGNTDGTCW27FQPCOR5Y5MJWN2TWCSIRNBK6QGBITBRQC:224"}}]}},{"FileDel":{"deleted_names":[{"basename":"ch4_scc1.tex","metadata":0}],"del":{"EdgeMap":{"edges":[{"previous":"BLOCK | FOLDER","flag":"BLOCK | FOLDER | DELETED","from":{"change":4,"pos":7550},"to":{"change":2,"start":0,"end":36},"introduced_by":2},{"previous":"BLOCK | FOLDER","flag":"BLOCK | FOLDER | DELETED","from":{"change":2,"pos":36},"to":{"change":2,"start":37,"end":37},"introduced_by":2}],"inode":{"change":2,"pos":37}}},"content_edges":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":37},"to":{"change":2,"start":38,"end":1569},"introduced_by":2}],"inode":{"change":2,"pos":37}},"content":[{"Del":{"text":"% TeX root = ../main.tex","pos":"Y5TDO2A5LSBCUOIN3366WGQ5QQAOBRUI672Q7KCIXAZZCQCUC2KQC:62"}},{"Del":{"text":"","pos":"Y5TDO2A5LSBCUOIN3366WGQ5QQAOBRUI672Q7KCIXAZZCQCUC2KQC:63"}},{"Del":{"text":"\\centering","pos":"Y5TDO2A5LSBCUOIN3366WGQ5QQAOBRUI672Q7KCIXAZZCQCUC2KQC:74"}},{"Del":{"text":"\\begin{tikzpicture}[","pos":"Y5TDO2A5LSBCUOIN3366WGQ5QQAOBRUI672Q7KCIXAZZCQCUC2KQC:95"}},{"Del":{"text":" shorten >=1pt,","pos":"Y5TDO2A5LSBCUOIN3366WGQ5QQAOBRUI672Q7KCIXAZZCQCUC2KQC:118"}},{"Del":{"text":" >={Stealth[round]},","pos":"Y5TDO2A5LSBCUOIN3366WGQ5QQAOBRUI672Q7KCIXAZZCQCUC2KQC:146"}},{"Del":{"text":" node distance=2cm,","pos":"Y5TDO2A5LSBCUOIN3366WGQ5QQAOBRUI672Q7KCIXAZZCQCUC2KQC:173"}},{"Del":{"text":" semithick,","pos":"Y5TDO2A5LSBCUOIN3366WGQ5QQAOBRUI672Q7KCIXAZZCQCUC2KQC:192"}},{"Del":{"text":" on grid,","pos":"Y5TDO2A5LSBCUOIN3366WGQ5QQAOBRUI672Q7KCIXAZZCQCUC2KQC:209"}},{"Del":{"text":" auto,","pos":"Y5TDO2A5LSBCUOIN3366WGQ5QQAOBRUI672Q7KCIXAZZCQCUC2KQC:223"}},{"Del":{"text":" initial text=,","pos":"Y5TDO2A5LSBCUOIN3366WGQ5QQAOBRUI672Q7KCIXAZZCQCUC2KQC:246"}},{"Del":{"text":" initial above,","pos":"Y5TDO2A5LSBCUOIN3366WGQ5QQAOBRUI672Q7KCIXAZZCQCUC2KQC:269"}},{"Del":{"text":" ]","pos":"Y5TDO2A5LSBCUOIN3366WGQ5QQAOBRUI672Q7KCIXAZZCQCUC2KQC:275"}},{"Del":{"text":" \\draw[helplines] (-3,1) grid (3,-7);","pos":"Y5TDO2A5LSBCUOIN3366WGQ5QQAOBRUI672Q7KCIXAZZCQCUC2KQC:316"}},{"Del":{"text":"","pos":"Y5TDO2A5LSBCUOIN3366WGQ5QQAOBRUI672Q7KCIXAZZCQCUC2KQC:317"}},{"Del":{"text":" \\node[state,initial] (l0) {$l_0$};","pos":"Y5TDO2A5LSBCUOIN3366WGQ5QQAOBRUI672Q7KCIXAZZCQCUC2KQC:386"}},{"Del":{"text":" \\node[state] (li1) [below left = of l0] {$l_{i_1}$};","pos":"Y5TDO2A5LSBCUOIN3366WGQ5QQAOBRUI672Q7KCIXAZZCQCUC2KQC:459"}},{"Del":{"text":" \\node[state] (lin) [below right = of l0] {$l_{i_n}$};","pos":"Y5TDO2A5LSBCUOIN3366WGQ5QQAOBRUI672Q7KCIXAZZCQCUC2KQC:532"}},{"Del":{"text":" \\node[state] (li1') [below = of li1] {$l_{i_1}'$};","pos":"Y5TDO2A5LSBCUOIN3366WGQ5QQAOBRUI672Q7KCIXAZZCQCUC2KQC:606"}},{"Del":{"text":" \\node[state] (lin') [below = of lin] {$l_{i_n}'$};","pos":"Y5TDO2A5LSBCUOIN3366WGQ5QQAOBRUI672Q7KCIXAZZCQCUC2KQC:680"}},{"Del":{"text":" \\node[state] (lo1) [below = of li1'] {$l_{o_1}$};","pos":"Y5TDO2A5LSBCUOIN3366WGQ5QQAOBRUI672Q7KCIXAZZCQCUC2KQC:753"}},{"Del":{"text":" \\node[state] (lom) [below = of lin'] {$l_{o_m}$};","pos":"Y5TDO2A5LSBCUOIN3366WGQ5QQAOBRUI672Q7KCIXAZZCQCUC2KQC:826"}},{"Del":{"text":" \\node[state] (lo1') [below = of lo1] {$l_{o_1}'$};","pos":"Y5TDO2A5LSBCUOIN3366WGQ5QQAOBRUI672Q7KCIXAZZCQCUC2KQC:900"}},{"Del":{"text":" \\node[state] (lom') [below = of lom] {$l_{o_m}'$};","pos":"Y5TDO2A5LSBCUOIN3366WGQ5QQAOBRUI672Q7KCIXAZZCQCUC2KQC:974"}},{"Del":{"text":"","pos":"Y5TDO2A5LSBCUOIN3366WGQ5QQAOBRUI672Q7KCIXAZZCQCUC2KQC:975"}},{"Del":{"text":" \\node (center)[below=4.2cm of l0] {};","pos":"Y5TDO2A5LSBCUOIN3366WGQ5QQAOBRUI672Q7KCIXAZZCQCUC2KQC:1017"}},{"Del":{"text":" \\draw[color=gray] (center) ellipse [x radius=3cm,y radius=3cm];","pos":"Y5TDO2A5LSBCUOIN3366WGQ5QQAOBRUI672Q7KCIXAZZCQCUC2KQC:1085"}},{"Del":{"text":"","pos":"Y5TDO2A5LSBCUOIN3366WGQ5QQAOBRUI672Q7KCIXAZZCQCUC2KQC:1086"}},{"Del":{"text":" \\path[->] (li1) edge node {$t_{i_1}$} (li1')","pos":"Y5TDO2A5LSBCUOIN3366WGQ5QQAOBRUI672Q7KCIXAZZCQCUC2KQC:1150"}},{"Del":{"text":" (lin) edge node {$t_{i_n}$} (lin')","pos":"Y5TDO2A5LSBCUOIN3366WGQ5QQAOBRUI672Q7KCIXAZZCQCUC2KQC:1214"}},{"Del":{"text":" (lo1) edge node {$t_{o_1}$} (lo1')","pos":"Y5TDO2A5LSBCUOIN3366WGQ5QQAOBRUI672Q7KCIXAZZCQCUC2KQC:1278"}},{"Del":{"text":" (lom) edge node {$t_{o_m}$} (lom');","pos":"Y5TDO2A5LSBCUOIN3366WGQ5QQAOBRUI672Q7KCIXAZZCQCUC2KQC:1343"}},{"Del":{"text":"","pos":"Y5TDO2A5LSBCUOIN3366WGQ5QQAOBRUI672Q7KCIXAZZCQCUC2KQC:1344"}},{"Del":{"text":" %todo: squigilly line ","pos":"Y5TDO2A5LSBCUOIN3366WGQ5QQAOBRUI672Q7KCIXAZZCQCUC2KQC:1371"}},{"Del":{"text":" \\draw[->,decorate,decoration={snake,pre length=5pt,post length=10pt}] (l0) -- (li1);","pos":"Y5TDO2A5LSBCUOIN3366WGQ5QQAOBRUI672Q7KCIXAZZCQCUC2KQC:1460"}},{"Del":{"text":" \\draw[->,decorate,decoration={snake,pre length=5pt,post length=10pt}] (l0) -- (lin);","pos":"Y5TDO2A5LSBCUOIN3366WGQ5QQAOBRUI672Q7KCIXAZZCQCUC2KQC:1549"}},{"Del":{"text":"","pos":"Y5TDO2A5LSBCUOIN3366WGQ5QQAOBRUI672Q7KCIXAZZCQCUC2KQC:1550"}},{"Del":{"text":"\\end{tikzpicture}","pos":"Y5TDO2A5LSBCUOIN3366WGQ5QQAOBRUI672Q7KCIXAZZCQCUC2KQC:1568"}}]}},{"Edit":{"inode":{"change":4,"pos":7792},"path":"ch4_implementation.tex","line":97,"atom":{"EdgeMap":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":4,"pos":10084},"to":{"change":4,"start":10084,"end":10111},"introduced_by":4},{"previous":"","flag":"DELETED","from":{"change":4,"pos":10111},"to":{"change":4,"start":37047,"end":37061},"introduced_by":4},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":4,"pos":37047},"to":{"change":4,"start":37047,"end":37061},"introduced_by":4}],"inode":{"change":4,"pos":7792}}},"contents":[{"Del":{"text":"\\begin{comment}","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:10099"}},{"Del":{"text":" cfr --","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:10110"}},{"Del":{"text":"\\end{comment}","pos":"JCK77YLTPL6VV5ZOTMGUJSFZ5DNMS3MZGP5UQLXYW6WSMEK6GAQAC:37060"}}]}},{"Edit":{"inode":{"change":4,"pos":7792},"path":"ch4_implementation.tex","line":98,"atom":{"EdgeMap":{"edges":[{"previous":"","flag":"DELETED","from":{"change":4,"pos":10153},"to":{"change":4,"start":427,"end":569},"introduced_by":4},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":4,"pos":37061},"to":{"change":4,"start":427,"end":569},"introduced_by":4}],"inode":{"change":4,"pos":7792}}},"contents":[{"Del":{"text":"\\subsection{SCCs}","pos":"X7SPUV4CXRX7D5KKL6UVGHC7JWRWCA4QAJVVQISE64UEU7GXJNRQC:444"}},{"Del":{"text":"\\begin{figure}","pos":"X7SPUV4CXRX7D5KKL6UVGHC7JWRWCA4QAJVVQISE64UEU7GXJNRQC:459"}},{"Del":{"text":" \\input{figures/ch4_scc1}","pos":"X7SPUV4CXRX7D5KKL6UVGHC7JWRWCA4QAJVVQISE64UEU7GXJNRQC:488"}},{"Del":{"text":" \\caption{Visualization of partial evaluation for a single SCC}","pos":"X7SPUV4CXRX7D5KKL6UVGHC7JWRWCA4QAJVVQISE64UEU7GXJNRQC:555"}},{"Del":{"text":"\\end{figure}","pos":"X7SPUV4CXRX7D5KKL6UVGHC7JWRWCA4QAJVVQISE64UEU7GXJNRQC:568"}}]}},{"Replacement":{"inode":{"change":4,"pos":7949},"path":"ch3_theory.tex","line":142,"ins":{"up_context":[{"change":3,"pos":6800}],"down_context":[{"change":3,"pos":6927}],"flag":"BLOCK","start":150,"end":377,"inode":{"change":4,"pos":7949}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":6800},"to":{"change":3,"start":6800,"end":6927},"introduced_by":3}],"inode":{"change":4,"pos":7949}},"ins_contents":[{"Add":{"text":" For any assignment $s,s'\\in\\Sigma$, and probabilistic update $\\eta: \\PV","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:225"}},{"Add":{"text":" \\rightarrow \\Z[\\V \\union D]$ holds $s'(x_i) = k_i \\in","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:283"}},{"Add":{"text":" \\text{supp}([\\eta(x_i)](s))$ implies $s'\\models \\tilde{\\eta}()$","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:351"}},{"Add":{"text":"","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:352"}},{"Add":{"text":" and values $k_i \\in","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:376"}}],"del_contents":[{"Del":{"text":" For any assignment $s\\in\\Sigma$, non-probabilistic update $\\eta: \\PV","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:6872"}},{"Del":{"text":" \\rightarrow \\Z[\\V \\union D]$, and values $k_i \\in","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:6926"}}]}},{"Edit":{"inode":{"change":4,"pos":7949},"path":"ch3_theory.tex","line":459,"atom":{"NewVertex":{"up_context":[{"change":3,"pos":9516}],"down_context":[{"change":4,"pos":1784}],"flag":"BLOCK","start":378,"end":5775,"inode":{"change":4,"pos":7949}}},"contents":[{"Add":{"text":"\\begin{definition}[Equivalent \\glspl{pip}]","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:420"}},{"Add":{"text":" Let $\\Prog_1,\\Prog_2$ be \\glspl{pip} with $\\Prog_1 = (\\PV, \\Loc_1, \\GT_1,","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:498"}},{"Add":{"text":" l_0)$, $\\Prog_2 = (\\PV, \\Loc_2, \\GT_2, l_0)$ and their respective","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:568"}},{"Add":{"text":" probability spaces $(\\runs_1, \\F_1, \\PrSs^1)$ and $(\\runs_2, \\F_2,","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:639"}},{"Add":{"text":" \\PrSs^2)$. Besides $\\T_1$ and $\\T_2$ denote the set of transitions of","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:713"}},{"Add":{"text":" $\\Prog_1$ and $\\Prog_2$; $\\fpath_1$ and $\\fpath_2$ the set of finite paths,","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:793"}},{"Add":{"text":" etc. ","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:803"}},{"Add":{"text":"","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:804"}},{"Add":{"text":" The two programs are equivalent if the two random variables $\\Rt_{\\Prog_1}$","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:884"}},{"Add":{"text":" and $\\Rt_{\\Prog_2}$ have the same probability distributions $\\mu_1$ and","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:960"}},{"Add":{"text":" $\\mu_2$ with $\\mu_1(k) = \\mu_2(k)$ for all $k\\in\\overline{\\N}$.","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:1028"}},{"Add":{"text":"\\end{definition}","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:1045"}},{"Add":{"text":"","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:1046"}},{"Add":{"text":"\\begin{theorem}","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:1062"}},{"Add":{"text":" If $\\Prog_1$ and $\\Prog_2$ are equivalent then:","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:1114"}},{"Add":{"text":" \\begin{enumerate}","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:1136"}},{"Add":{"text":" \\item A total runtime-complexity bound for the $\\Prog_1$ is a total","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:1212"}},{"Add":{"text":" runtime complexity bound for $\\Prog_2$ and vice-versa. ","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:1280"}},{"Add":{"text":" \\item $\\Prog_1$ and $\\Prog_2$ have the same expected runtime-complexity. ","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:1362"}},{"Add":{"text":" \\end{enumerate}","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:1382"}},{"Add":{"text":"","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:1383"}},{"Add":{"text":" \\proof{","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:1395"}},{"Add":{"text":" Let $\\RB_P$ ","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:1416"}},{"Add":{"text":" }","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:1422"}},{"Add":{"text":"\\end{theorem}","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:1436"}},{"Add":{"text":"","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:1437"}},{"Add":{"text":"\\begin{rem}","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:1449"}},{"Add":{"text":" The probability distribution doesn't care about the underlying probability","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:1528"}},{"Add":{"text":" space making it the perfect tool to compare the semantics of two different","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:1607"}},{"Add":{"text":" \\glspl{pip}.","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:1624"}},{"Add":{"text":"\\end{rem}","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:1634"}},{"Add":{"text":"","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:1635"}},{"Add":{"text":"We will show the partial evaluation $\\Prog'$ is equivalent to the original","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:1710"}},{"Add":{"text":"\\gls{pip} $\\Prog$. In a first step we will show that for every admissible finite","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:1791"}},{"Add":{"text":"prefix in $\\Prog$ there exists an admissible finite prefix in $\\Prog'$ with the","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:1871"}},{"Add":{"text":"same probability and intermediate states and vice versa. This in turn will be","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:1949"}},{"Add":{"text":"expanded for all admissible runs and finally we will show that this proves an","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:2027"}},{"Add":{"text":"equal probability distribution of the total runtime complexity. ","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:2092"}},{"Add":{"text":"","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:2093"}},{"Add":{"text":"","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:2094"}},{"Add":{"text":"\\subsection{Induction}","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:2117"}},{"Add":{"text":"Given an admissible run $f^*= c_0c_1\\dots \\in \\runs$ of the original program","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:2194"}},{"Add":{"text":"$\\Prog$ with $c_i = (l_i,s_i,t_i)$ for all $i = 0,1,\\dots$ and a scheduler","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:2269"}},{"Add":{"text":"$\\scheduler$ for the very same program. ","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:2310"}},{"Add":{"text":"","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:2311"}},{"Add":{"text":"\\textbf{Induction hypothesis.} We can find an arbitrarily long prefix","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:2381"}},{"Add":{"text":"$f'_n=c'_0c'_1\\cdots{}c_n \\in \\fpath'$ of length $n \\in \\N$ and scheduler","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:2455"}},{"Add":{"text":"$\\scheduler'_n$ such that:","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:2482"}},{"Add":{"text":"\\begin{enumerate}","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:2500"}},{"Add":{"text":" \\item $\\prSs(c_0\\dots{}c_n) = \\prSns'(c'_0\\dots{}c'_n)$","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:2560"}},{"Add":{"text":" \\item $c'_i = (\\langle l_i, \\varphi_i\\rangle,s_i,t'_i)$ for some","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:2630"}},{"Add":{"text":" $\\varphi_i \\in \\C$, $t'_i \\in \\T'$, and $i = 1, \\dots, n$ \\label{itm:location_in_version}","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:2728"}},{"Add":{"text":" \\item $s_i \\models \\varphi_i$ \\label{itm:si_models_phi}","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:2788"}},{"Add":{"text":"\\end{enumerate}","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:2804"}},{"Add":{"text":"","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:2805"}},{"Add":{"text":"Items \\ref{itm:location_in_version} and \\ref{itm:si_models_phi} are only","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:2878"}},{"Add":{"text":"required for the induction, but are unimportant for the final result. ","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:2949"}},{"Add":{"text":"","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:2950"}},{"Add":{"text":"\\textbf{Induction start n=0.}","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:2980"}},{"Add":{"text":"Since $f^*$ is an admissible run, $c_0 = (l_0, s_0,t_\\text{in})$. Set","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:3050"}},{"Add":{"text":"$f'_0=(\\langle l_0,\\textit{true}\\rangle,s_0,t_\\text{in})$. $\\langle l_0,","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:3123"}},{"Add":{"text":"\\textit{true}$ is a location in $\\Prog'$ since it is added at first by the","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:3198"}},{"Add":{"text":"evaluation algorithm. $s_0 \\models \\textit{true}$ trivially. $\\prSs(c_0) =","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:3273"}},{"Add":{"text":"\\prSs'(c'_0) = 1$ since both $c_0$ and $c'_0$ are valid starting configurations","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:3353"}},{"Add":{"text":"in $\\Prog$ and $\\Prog'$ respectively.","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:3391"}},{"Add":{"text":"","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:3392"}},{"Add":{"text":"\\textbf{Induction step.} ","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:3418"}},{"Add":{"text":"Assume the induction hypothesis holds for $n$ we will construct a prefix of","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:3494"}},{"Add":{"text":"length $n+1$ for that the hypothesis equally holds. ","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:3547"}},{"Add":{"text":"","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:3548"}},{"Add":{"text":"Since the run is admissible, so is its prefix $f_i = c_0c_1\\dots{}c_nc_{n+1}$","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:3626"}},{"Add":{"text":"and by definition \\todo{ref}","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:3655"}},{"Add":{"text":"\\begin{equation*}","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:3673"}},{"Add":{"text":" \\prSs(f) = \\prSs(c_0) \\cdot \\prod_{i=1,\\dots,n+1} \\prSs(c_{i-1} \\rightarrow","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:3753"}},{"Add":{"text":" c_i) > 0","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:3766"}},{"Add":{"text":"\\end{equation*}","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:3782"}},{"Add":{"text":"","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:3783"}},{"Add":{"text":"Let $\\scheduler(c_n) = (g_{n+1},\\tilde{s}_n)$, by definition \\todo{ref}","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:3855"}},{"Add":{"text":"\\begin{equation*}","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:3873"}},{"Add":{"text":" \\prSs(c_n \\rightarrow c_{n+1}) = p \\cdot","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:3918"}},{"Add":{"text":" \\prod_{x\\in\\PV}[\\eta(x)](\\tilde{s}_n)(s_{n+1}(x)) \\cdot \\prod_{u\\in\\V\\backslash\\PV}","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:4006"}},{"Add":{"text":" \\delta_{\\tilde{s}_n(u),s_n(u)} > 0","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:4045"}},{"Add":{"text":"\\end{equation*}","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:4061"}},{"Add":{"text":"","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:4062"}},{"Add":{"text":"Since $f'_n$ is an admissible path, $\\langle l_n, \\varphi_n \\rangle$ is a valid","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:4142"}},{"Add":{"text":"location (version) in $\\Prog'$, every version is unfolded by the evaluation","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:4218"}},{"Add":{"text":"algorithm immediately after being added to the new program in (\\todo{ref}). As","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:4297"}},{"Add":{"text":"$g_i$ is selected by the scheduler, $g_{n+1}$ is a general transition with","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:4372"}},{"Add":{"text":"$l_{g_{n+1}} = l_n$. As such $g_{n+1}$ is unfolded by the algorithm in","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:4443"}},{"Add":{"text":"(\\todo{ref}) and so is the transition $t_{n+1}$ as part of unfolding of the","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:4519"}},{"Add":{"text":"general transition $g_{n+1}$.","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:4549"}},{"Add":{"text":"","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:4550"}},{"Add":{"text":"With $g'_{n+1}=\\text{unfold*}(\\varphi_n, g_{i+1})$, define the next","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:4618"}},{"Add":{"text":"$\\scheduler'_{n+1}$ as ","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:4642"}},{"Add":{"text":"\\begin{equation*}","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:4660"}},{"Add":{"text":" \\scheduler'_{n+1}(c) = \\begin{cases}","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:4701"}},{"Add":{"text":" (g'_{n+1}, \\tilde{s}_n) & \\text{if } c = c'_n \\\\","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:4758"}},{"Add":{"text":" \\scheduler'_n & \\text{otherwise}","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:4799"}},{"Add":{"text":" \\end{cases}","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:4815"}},{"Add":{"text":"\\end{equation*}","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:4831"}},{"Add":{"text":"","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:4832"}},{"Add":{"text":"Select $t'_{n+1} = \\text{unfold*}(\\varphi_n, t_{n+1}) \\in g'_{n+1}$","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:4900"}},{"Add":{"text":"","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:4901"}},{"Add":{"text":"Recall definition (\\todo{ref}), by construction $t'_{n+1}=(\\langle l_n,","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:4973"}},{"Add":{"text":"\\varphi\\rangle,p,\\tau_i,\\eta,\\langle l_{n+1}, \\varphi_{n+1}\\rangle)$","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:5042"}},{"Add":{"text":"for some formula $\\varphi_{n+1}$.","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:5076"}},{"Add":{"text":"","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:5077"}},{"Add":{"text":"\\begin{equation*}","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:5095"}},{"Add":{"text":" \\prSnns(c'_n \\rightarrow c'_{n+1}) = p \\cdot","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:5144"}},{"Add":{"text":" \\prod_{x\\in\\PV}[\\eta(x)](\\tilde{s'}_n)(s'_{n+1}(x)) \\cdot \\prod_{u\\in\\V\\backslash\\PV}","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:5234"}},{"Add":{"text":" \\delta_{\\tilde{s}(u),s(u)} > 0","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:5269"}},{"Add":{"text":"\\end{equation*}","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:5285"}},{"Add":{"text":"","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:5286"}},{"Add":{"text":"By lemma (\\todo{ref}) $s_{n+1} \\models \\varphi_{n+1}$, fulfilling (3) of the","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:5363"}},{"Add":{"text":"induction hypothesis. We fulfill (2) of the induction hypothesis, by","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:5432"}},{"Add":{"text":"constructing $c'_{n+1} = (\\langle l_{n+1}, \\varphi_n\\rangle, s_{n+1},","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:5502"}},{"Add":{"text":"t'_{n+1})$. By setting $s'_{n+1} = s_{n+1}$ we get $\\prSnns(c'_n\\rightarrow","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:5578"}},{"Add":{"text":"c'_{n+1})= \\prSs(c_n \\rightarrow c_{n+1})$ and with the induction hypothesis","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:5655"}},{"Add":{"text":"\\begin{equation*}","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:5673"}},{"Add":{"text":" \\prSs(f_n) = \\prSnns(f'_nc'_{n+1})","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:5712"}},{"Add":{"text":"\\end{equation*}","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:5728"}},{"Add":{"text":"and fulfill (1) of the induction hypothesis.","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:5773"}},{"Add":{"text":"","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:5774"}}]}},{"Edit":{"inode":{"change":4,"pos":7949},"path":"ch3_theory.tex","line":622,"atom":{"NewVertex":{"up_context":[{"change":3,"pos":11374}],"down_context":[{"change":3,"pos":11374}],"flag":"BLOCK","start":5776,"end":7475,"inode":{"change":4,"pos":7949}}},"contents":[{"Add":{"text":"","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:5776"}},{"Add":{"text":"\\begin{figure}[h]","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:5794"}},{"Add":{"text":" \\centering","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:5809"}},{"Add":{"text":" \\begin{subcaptionblock}[t]{0.45\\textwidth}","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:5856"}},{"Add":{"text":" \\centering","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:5875"}},{"Add":{"text":" \\input{figures/ch4_scc_prog}","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:5912"}},{"Add":{"text":" \\caption{The original program}","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:5951"}},{"Add":{"text":" \\end{subcaptionblock}","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:5977"}},{"Add":{"text":" \\begin{subcaptionblock}[t]{0.45\\textwidth}","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:6024"}},{"Add":{"text":" \\centering","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:6043"}},{"Add":{"text":" \\input{figures/ch4_scc_lift}","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:6080"}},{"Add":{"text":" \\caption{Copy and lift}","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:6112"}},{"Add":{"text":" \\end{subcaptionblock}","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:6138"}},{"Add":{"text":" \\begin{subcaptionblock}[t]{0.45\\textwidth}","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:6185"}},{"Add":{"text":" \\centering","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:6204"}},{"Add":{"text":" \\input{figures/ch4_scc_remove}","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:6243"}},{"Add":{"text":" \\caption{Remove SCC}","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:6272"}},{"Add":{"text":" \\end{subcaptionblock}","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:6298"}},{"Add":{"text":" \\begin{subcaptionblock}[t]{0.45\\textwidth}","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:6345"}},{"Add":{"text":" \\centering","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:6364"}},{"Add":{"text":" \\input{figures/ch4_scc_evaluate}","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:6405"}},{"Add":{"text":" \\caption{Evaluate entry transitions}","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:6450"}},{"Add":{"text":" \\end{subcaptionblock}","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:6476"}},{"Add":{"text":" \\caption{Visualization of partial evaluation for a single","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:6538"}},{"Add":{"text":" SCC\\label{fig:evaluate_scc}}","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:6571"}},{"Add":{"text":"\\end{figure}","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:6584"}},{"Add":{"text":"","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:6585"}},{"Add":{"text":"\\begin{algorithm}","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:6603"}},{"Add":{"text":" \\caption{$evaluate_{SCC}(P, A)$}","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:6640"}},{"Add":{"text":" \\KwData{ A PIP $P$, a \\gls{scc} $A\\subset\\T$ }","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:6691"}},{"Add":{"text":" \\KwResult{A Graph $G$}","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:6718"}},{"Add":{"text":"","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:6719"}},{"Add":{"text":" $\\Tin \\leftarrow \\Tin(A)$\\;","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:6751"}},{"Add":{"text":" $\\Tout \\leftarrow \\Tout(A)$\\;","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:6785"}},{"Add":{"text":"","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:6786"}},{"Add":{"text":" \\SetKwFunction{FEvaluate}{evaluate}","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:6826"}},{"Add":{"text":" \\SetKwProg{Fn}{Function}{:}{end}","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:6863"}},{"Add":{"text":" \\Fn{\\FEvaluate{$G$, $v$, $t$}}{","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:6899"}},{"Add":{"text":" $N = \\unfold^*(v)$\\;","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:6928"}},{"Add":{"text":" \\For{$t = (v, \\tau, \\eta, p, v') \\in N $}{","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:6979"}},{"Add":{"text":" \\uIf {$(l_v, \\tau, \\eta,p, l_{v'}) \\in \\Tout$}{","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:7039"}},{"Add":{"text":" $G \\leftarrow G + (v, \\tau, \\eta, p, \\langle v_{l'},","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:7108"}},{"Add":{"text":" \\textit{true}\\rangle)$\\;","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:7149"}},{"Add":{"text":" }","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:7163"}},{"Add":{"text":" \\uElseIf {$v' \\not\\in G$}{","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:7202"}},{"Add":{"text":" $G \\leftarrow G + t$\\;","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:7241"}},{"Add":{"text":" $G \\leftarrow evaluate(P, G, v')$\\;","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:7293"}},{"Add":{"text":" }","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:7307"}},{"Add":{"text":" \\Else {","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:7327"}},{"Add":{"text":" $G \\leftarrow G + t$\\;","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:7366"}},{"Add":{"text":" }","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:7380"}},{"Add":{"text":" }","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:7390"}},{"Add":{"text":" \\Return {$G$}","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:7412"}},{"Add":{"text":" }","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:7418"}},{"Add":{"text":"","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:7419"}},{"Add":{"text":" $G \\leftarrow \\text{lift}(P - A - \\Tin - \\Tout)$\\;","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:7474"}}]}},{"Edit":{"inode":{"change":4,"pos":7949},"path":"ch3_theory.tex","line":679,"atom":{"NewVertex":{"up_context":[{"change":3,"pos":11375}],"down_context":[{"change":3,"pos":11375}],"flag":"BLOCK","start":7476,"end":7681,"inode":{"change":4,"pos":7949}}},"contents":[{"Add":{"text":" \\For{$t_i = (l_\\text{i}, \\_, \\_ ,\\_, l_\\text{i}') \\in \\Tin $}{","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:7542"}},{"Add":{"text":" $ G \\leftarrow \\text{evaluate}(P, G, \\langle l_i, \\textit{true}\\rangle,","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:7622"}},{"Add":{"text":" t_i)$\\;","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:7638"}},{"Add":{"text":" }","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:7644"}},{"Add":{"text":" \\Return {$G$}\\;","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:7664"}},{"Add":{"text":"\\end{algorithm}","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:7680"}}]}},{"Edit":{"inode":{"change":4,"pos":8115},"path":"ch2_preliminaries.tex","line":9,"atom":{"NewVertex":{"up_context":[{"change":4,"pos":174}],"down_context":[{"change":3,"pos":11377}],"flag":"BLOCK","start":7682,"end":7740,"inode":{"change":4,"pos":8115}}},"contents":[{"Add":{"text":"\\newcommand{\\D}[0]{\\mathcal{D}} % variable distributions ","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:7739"}}]}},{"Edit":{"inode":{"change":4,"pos":8115},"path":"ch2_preliminaries.tex","line":49,"atom":{"NewVertex":{"up_context":[{"change":3,"pos":12266}],"down_context":[{"change":3,"pos":12266}],"flag":"BLOCK","start":7741,"end":7860,"inode":{"change":4,"pos":8115}}},"contents":[{"Add":{"text":"\\newcommand{\\prSns}[0]{\\textit{pr}_{\\scheduler'_n, s_0}}","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:7797"}},{"Add":{"text":"\\newcommand{\\prSnns}[0]{\\textit{pr}_{\\scheduler'_{n+1}, s_0}}","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:7859"}}]}},{"Replacement":{"inode":{"change":4,"pos":8115},"path":"ch2_preliminaries.tex","line":58,"ins":{"up_context":[{"change":4,"pos":11494}],"down_context":[{"change":4,"pos":10458}],"flag":"BLOCK","start":7861,"end":9739,"inode":{"change":4,"pos":8115}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":4,"pos":11494},"to":{"change":4,"start":11494,"end":11592},"introduced_by":4}],"inode":{"change":4,"pos":8115}},"ins_contents":[{"Add":{"text":"This thesis uses a lot of notation. For ease of reading, the reader is provided","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:7940"}},{"Add":{"text":"with this overview of commonly encountered symbols and their usage.","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:8008"}},{"Add":{"text":"\\begin{center}","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:8023"}},{"Add":{"text":" \\begin{tabular}{|l|l|}","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:8050"}},{"Add":{"text":" \\hline","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:8065"}},{"Add":{"text":" Symbols & Usage \\\\ ","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:8093"}},{"Add":{"text":" \\hline","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:8108"}},{"Add":{"text":" $a,i,j,l,k,m,n$ & integer values \\\\","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:8152"}},{"Add":{"text":" $e$ & polynomial expressions \\\\","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:8192"}},{"Add":{"text":" $s$ & assignments \\\\","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:8221"}},{"Add":{"text":" $p$ & probability \\\\","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:8250"}},{"Add":{"text":" $x,y,z$ & program variables \\\\","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:8289"}},{"Add":{"text":" $D$ & distributions \\\\","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:8320"}},{"Add":{"text":" $d$ & temporary variable replacing a distribution \\\\","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:8381"}},{"Add":{"text":" $\\psi, $ & constraints \\\\","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:8415"}},{"Add":{"text":" $\\varphi, $ & formulas\\\\","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:8448"}},{"Add":{"text":" $l$ & locations \\\\","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:8475"}},{"Add":{"text":" $t$ & transitions \\\\","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:8504"}},{"Add":{"text":" $g$ & general transitions \\\\","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:8541"}},{"Add":{"text":" $\\tau$ & guards of transitions \\\\","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:8583"}},{"Add":{"text":" $u$ & non-probabilistic update functions\\\\","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:8634"}},{"Add":{"text":" $\\eta$ & probabilistic update functions\\\\","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:8684"}},{"Add":{"text":" $\\vartheta$ & probabilistic polynomial.\\\\","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:8734"}},{"Add":{"text":" $\\mu$ & probability distributions \\\\","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:8779"}},{"Add":{"text":" $f$ & finite prefixes \\\\","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:8812"}},{"Add":{"text":" $\\scheduler$ & scheduler \\\\","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:8848"}},{"Add":{"text":" $\\B$ & set of bounds \\\\","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:8880"}},{"Add":{"text":" $\\C$ & set of constraints \\\\","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:8917"}},{"Add":{"text":" $\\D$ & set of distributions \\\\","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:8956"}},{"Add":{"text":" $\\G$ & set of graphs \\\\","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:8988"}},{"Add":{"text":" $\\GT$ & set of general transitions \\\\","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:9034"}},{"Add":{"text":" $\\Lin$ & set of linear constraints\\\\","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:9079"}},{"Add":{"text":" $\\PV$ & set of program variables \\\\","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:9123"}},{"Add":{"text":" $\\T$ & set of transitions \\\\","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:9160"}},{"Add":{"text":" $\\TV$ & set of temporary variables \\\\","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:9206"}},{"Add":{"text":" $\\V$ & set of variables \\\\","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:9241"}},{"Add":{"text":" \\hline","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:9256"}},{"Add":{"text":" \\end{tabular}","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:9274"}},{"Add":{"text":"\\end{center}","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:9287"}},{"Add":{"text":"","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:9288"}},{"Add":{"text":"Let $\\overline{\\N} = \\N \\union \\{\\infty\\}$. Let $[\\cdot\\backslash{}\\cdot]$","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:9363"}},{"Add":{"text":"denote the syntactical substitution where one symbols is replaced by","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:9432"}},{"Add":{"text":"another. For example $(x 0}","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:15127"}},{"Add":{"text":"\\end{align}","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:15139"}},{"Add":{"text":"","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:15140"}},{"Add":{"text":"The expected total runtime complexity is the expected value of the random","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:15214"}},{"Add":{"text":"variable $\\ESs(\\Rt_\\Prog)$","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:15241"}},{"Add":{"text":"","pos":"A5NVU6DZYOG6GRXJU6DZLCUQTKA7LPUWOGQ4NCJSY6FJB6GSP3OAC:15242"}}]}}],"owner":"paradyx","repo":"ma-tex","token":"GfHLRQHURYq/+mdarHxwB+wvcSguL3G+0Ruzoh/TwNQ=","login":null}

…

Dependencies

Change contents

Review