Are Infinite Time Turing Machines able to determine whether an arbitrary (well-founded) system of fundamental sequences is, in fact, well-founded? Suppose that a particular Infinite Time Turing Machine (ITTM) is given two reals $(r_1, r_2)$, where $r_1$ encodes an arbitrary well-order $W$ and $r_2$ contains the answers for all of the following questions:  

Is the number $x$ an $y$-th element of the number $z$?

That is, natural numbers $x$ and $z$ correspond to ordinals in $W$, and $r_2$ is supposed to encode a system of fundamental sequences for $W$.  
Does there exist a number $i$ such that an $i$-th ITTM is always able to determine whether $r_2$ corresponds to a well-founded (valid) system of fundamental sequences for an arbitrary $W$? Do there exist a system $S$ of fundamental sequences that can be considered “well-founded” (for a particular well-order $W$ such that the order type of $W$ is a countable ordinal) from the mathematical point of view, but the definition of $S$ is so complex that the mere fact that $S$ is well-founded is not decidable by ITTMs?
 A: The answer to your question is "yes". So let's denote the representation of (fundamental) sequences (under $W$) by the function $f:\mathbb{N}^2 \rightarrow \mathbb{N}$. So $f(x,n)$ would mean that: "the number (under $W$) denoting the $n$-th term of the limit element denoted by the number $x$ (under $W$) is $f(x,n)$." However, we need to decide whether we want to set up some conventions on $f(x,n)$ when $x$ doesn't denote a limit element. It is fine not to place any convention (for the purposes of the question). 
Now given any valid well-order relation and a function $f:\mathbb{N}^2 \rightarrow \mathbb{N}$, the first thing to observe is that we can (without much difficulty) obtain the predicate-function $isLimit:\mathbb{N} \rightarrow 0,1$. If $x$ denotes a limit element (under $W$) then $isLimit(x)=1$ (and otherwise it is $0$). 
Now for each arbitrary number $i \in \mathbb{N}$ (essentially a loop from $i:=0$ to $i<\omega$) first test whether $isLimit(i)=1$ or not. If that's true then we need a second loop from some $j:=0$ to $j<\omega$. For each $j$ we want to determine whether: (1) $f(i,j)$ denotes an ordinal smaller than the ordinal denoted by the number $i$. (2) $f(i,j+1)$ denotes a bigger ordinal than $f(i,j)$ or not.
[Edit1:] We also need to add a third condition after testing the first two this would be that the supremem of ordinals denoted by $f(i,j)$ (as $j$ approaches $\omega$) is equal to the ordinal denoted by $i$. This can also be tested.[End]
If any of the conditions (1),(2) or (3) in the previous paragraphs turn out to be false (for some values of $i,j$ then $f$ isn't a valid representation. If not, then $f$ is a valid representation. All the above steps can be carried out by any ITTM (given the well-order relation for $W$ and the function $f$). 
