Challenge: Proof Loops !

Olá,

Estou com uma dúvida sobre o mecanismo de funcionamento do Z/EVES e irei de compartilhá-la com vocês. O problema que irei descrever ocorre quando existem duas regras de reescrita, tal que o que a primeira regra reescreve A por B, e a segunda regra reescreve B por A. Eu esperava que o provador entrasse em loop caso eu deixasse as duas regras abilitadas e tentasse provar um outro teorema que tivesse o predicado A.

Por que eu esperava isso?

Porque o provador iria usar a regra 1 para reescrever A por B; depois usar a regra 2 para reescrever B por A; depois usar a regra 1 para reescrever A por B; e assim por diante (infinitamente).

Consegui simular esta situação no Z/EVES em dois arquivos de prova. No primeiro, o provador não entra em loop; no segundo, o provador entra em loop. Minha dúvida é: por que, no primeiro caso, o provador não entra em loop?

PRIMEIRO ARQUIVO: NoProofLoops.tex

% A regra de reescrita rUnflex reescreve x \subseteq y por x \in \power y

\begin{theorem}{rule rUnflex}
\forall x, y: \power \num @ x \subseteq y \iff x \in \power y
\end{theorem}

% A regra de reescrita rUnflex2 reescreve x \in \power y por x \subseteq y

\begin{theorem}{rule rUnflex2}
\forall x, y: \power \num @ x \in \power y \iff x \subseteq y
\end{theorem}

% O teorema Test possui o padrão que permitirá a regra de
% reescrita rUnflex ser ativada.
\begin{theorem}{Test}
\forall x, y: \power \num | x \subseteq y @ x = y
\end{theorem}

SEGUNDO ARQUIVO: ProofLoops.tex

\begin{theorem}{rule rUnflex}
\forall x, y: \power \num @ x \subseteq y \iff x \in \power y
\end{theorem}

\begin{theorem}{rule rUnflex2}
\forall x, y: \power \num @ x \in \power y \iff (\exists w: \power \num | w = y @ x\subseteq w)
\end{theorem}

\begin{theorem}{Test}
\forall x, y: \power \num | x \subseteq y @ x = y
\end{theorem}


LOOP: Tente provar Test usando rewrite


Minha suposição é que o provador guarda três estados: BeforeLastRewriteRule, AfterLastRewriteRule, AfterThisRewriteRule.

IF (AfterThisRewriteRule = BeforeLastRewriteRule) THEN
NotApplyThisRule
ELSE
ApllyThisRule


Se alguém aqui já trabalhou com implementação de um provador de teoremas, ou conhece alguém que já, serei muito grato se procurar saber o real mecanismo usados para evitar proof loops e descrever este mecanismo para os leitores do blog.