FDL
>
PVS
>
Graphs
>
ramsey
new
> j
: var-decl
j: VAR T