|
|
@@ -7842,7 +7842,7 @@ We then delegate to \code{explicate\_pred}, passing the condition \code{(eq? y
|
|
|
[(Let x rhs body) ___]
|
|
|
[(Prim 'not (list e)) ___]
|
|
|
[(Prim op es) #:when (or (eq? op 'eq?) (eq? op '<))
|
|
|
- (IfStmt (Prim op arg*) (create_block thn)
|
|
|
+ (IfStmt (Prim op es) (create_block thn)
|
|
|
(create_block els))]
|
|
|
[(Bool b) (if b thn els)]
|
|
|
[(If cnd^ thn^ els^) ___]
|
|
|
@@ -9837,8 +9837,7 @@ follows.\index{subject}{Kleene Fixed-Point Theorem}
|
|
|
\]
|
|
|
When a lattice contains only finitely-long ascending chains, then
|
|
|
every Kleene chain tops out at some fixed point after a number of
|
|
|
-iterations of $f$. So that fixed point is also a least upper
|
|
|
-bound of the chain.
|
|
|
+iterations of $f$.
|
|
|
\[
|
|
|
\bot \sqsubseteq f(\bot) \sqsubseteq f(f(\bot)) \sqsubseteq \cdots
|
|
|
\sqsubseteq f^k(\bot) = f^{k+1}(\bot) = m_s
|
Jeremy Siek