From 77b4700a27ff005e557d45ac07f93cdbce0f7e83 Mon Sep 17 00:00:00 2001
From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Mon, 29 Nov 2021 16:35:55 -0300
Subject: [PATCH] [Calculus] Clarify lack of confluence for ITE_simp
---
spec/rule_list.tex | 10 ++++++++--
1 file changed, 8 insertions(+), 2 deletions(-)
diff --git a/spec/rule_list.tex b/spec/rule_list.tex
index a272e80..791852c 100644
--- a/spec/rule_list.tex
+++ b/spec/rule_list.tex
@@ -1136,8 +1136,14 @@ The possible transformations are:
\label{sec:ite-simp-rules}
\begin{proof-rule}{ite_simplify}{veriT}
-This rule simplifies an if-then-else term by applying equivalent
-transformations as long as possible. Depending on the sort of the
+ This rule simplifies an if-then-else term by applying equivalent
+ transformations until fix point\footnote{Note however that the order of the
+ application is important, since the set of rules is not confluent. For
+ example, the term $(\operatorname{ite} \top \; t_1 \; t_2 \leftrightarrow
+ t_1)$ can be simplified into both $p$ and $(not (not p))$ depending on the
+ order of applications.}
+ %
+Depending on the sort of the
$\operatorname{ite}$-term the rule can have one of two forms. If the sort
is $\mathbf{Bool}$ it has the form
\begin{plContainer}
--
GitLab