There are interesting results of the form $PCP[a(n), b(n)] = \texttt{SOMECLASS(n)}$ for multiple classes in the exponential hierarchy: the most famous one is probably $PCP[O(log(n)), O(1)] = NP$.
Are there similar theorems for larger complexity classes, such as PR, $F_\omega$, and other beyond ELEMENTARY? Do these theorems cover the complexity classes implied by proof assistants that only accept total functions?
