time.

\[lem:correctness\] If $G$ contains a cycle of length at most $R$ then ${\textsc{GirthApprox}}(G,R)$ (\[algo:girth3\]) returns a cycle of length at most $3R$.

Assume $G$ contains a cycle $C$ of length at most $R$. Let $v$ be a vertex in $C$. If the algorithm returns a cycle in line \[line:returncycledetected\] of ${\textsc{SimilarSet}}$ (\[alg:similar\_vertices\]) then since this cycle has length at most $3R$, the algorithm works as desired.

Consequently, we assume that this is not the case. Our goal is now to show that $A_v^{\mathrm{out}}$ contains all vertices $c \in C$ such that $d(v,c)\leq R/2$ and that $A_v^{\mathrm{in}}$ contains all vertices $c \in C$ such that $d(c,v)\leq R/2$. Since for all $c \in C$ either $d(v,c)\leq R/2$ or $d(c,v)\leq R/2$ this will imply that $C \subseteq A_v^{\mathrm{out}}\cup A_v^{\mathrm{in}}$ and therefore a cycle of length at most $R$ will be found in Line \[line:search\_union\] of ${\textsc{GirthApprox}}(G,R)$ (\[algo:girth3\]) and the algorithm works as desired. Further, note that it suffices to show that $A_v^{\mathrm{out}}$ contains all vertices $c \in C$ such that $d(v,c)\leq R/2$ as this will imply the desired claimed regarding $A_v^{\mathrm{in}}$ by symmetry.

Consider the execution of ${\textsc{SimilarSet}}$ (\[alg:similar\_vertices\]) from Line \[line:similar\_search\_1\] of ${\textsc{GirthApprox}}(G,R)$ (\[algo:girth3\]). Further, consider a vertex $t \in T_i(v)$ 