Tekst źródłowy strony Algorithmic logic

Are you ready?
'''A challenge'''<br />
Given the following piece of software prove or disprove the following formula<br />
<math> \vdash \forall_{n_0 \in Node} \forall_{e \in T}\,[\textbf{call } insert(n_0,e)]contains(n_0,e)   </math>
tzn, że jest logiczną konsekwencją przyjęcia definicji klasy $BST$ iż dla każdego węzła $n_0$ i każdego elementu $e$ typu $T$ po wykonaniu instrukcji $insert(n_),e)$ zachodzi $contains(n_0,e)$.