| Rank | Theorem | Name |
| 5 | Thm*  G:Graph. (x,y:Vertices(G). Dec(x = y))   (s:traversal(G). paren(Vertices(G);s) no_repeats(Vertices(G)+Vertices(G);s) df-traversal(G;s) depthfirst-traversal(G;s)) | [paren-df-traversal] |
| cites |
| 3 | Thm* (x,y:T. Dec(x = y)) (s:(T+T) List, i:T. Dec((inl(i)  s))) | [decidable__l_member_paren] |
| 2 | Thm* s:T List, z:T. (z s) ( s1,s2:T List. s = (s1 @ [z / s2])) | [l_member_decomp] |
| 2 | Thm* s:(T+T) List. paren(T;s) (i:T, s1,s2:(T+T) List. s = (s1 @ [inl(i)] @ s2) (inr(i) s2)) | [paren_order1] |
| 4 | Thm* s:(T+T) List. paren(T;s) no_repeats(T+T;s) (s1,s2,s3:(T+T) List, x:T. s = (s1 @ [inl(x)] @ s2 @ [inr(x)] @ s3) paren(T;s2)) | [paren_interval] |
| 3 | Thm* s':(T+T) List. paren(T;s') (i:T. (inr(i) s') (inl(i) s')) | [paren_balance2] |
| 0 | Thm* as,bs,cs:T List. ((as @ bs) @ cs) = (as @ (bs @ cs)) | [append_assoc] |