Confluence: Confluence of untyped lambda calculus π§
module plfa.part2.Confluence where
Introduction
In this chapter we prove that beta reduction is confluent, a
property also known as ChurchRosser. That is, if there are
reduction sequences from any term L
to two different terms Mβ
and
Mβ
, then there exist reduction sequences from those two terms to
some common term N
. In pictures:
L
/ \
/ \
/ \
Mβ Mβ
\ /
\ /
\ /
N
where downward lines are instances of ββ
.
Confluence is studied in many other kinds of rewrite systems besides
the lambda calculus, and it is well known how to prove confluence in
rewrite systems that enjoy the diamond property, a singlestep
version of confluence. Let β
be a relation. Then β
has the
diamond property if whenever L β Mβ
and L β Mβ
, then there exists
an N
such that Mβ β N
and Mβ β N
. This is just an instance of
the same picture above, where downward lines are now instance of β
.
If we write β*
for the reflexive and transitive closure of β
, then
confluence of β*
follows immediately from the diamond property.
Unfortunately, reduction in the lambda calculus does not satisfy the diamond property. Here is a counter example.
(Ξ» x. x x)((Ξ» x. x) a) ββ (Ξ» x. x x) a
(Ξ» x. x x)((Ξ» x. x) a) ββ ((Ξ» x. x) a) ((Ξ» x. x) a)
Both terms can reduce to a a
, but the second term requires two steps
to get there, not one.
To sidestep this problem, weβll define an auxilliary reduction relation, called parallel reduction, that can perform many reductions simultaneously and thereby satisfy the diamond property. Furthermore, we show that a parallel reduction sequence exists between any two terms if and only if a beta reduction sequence exists between them. Thus, we can reduce the proof of confluence for beta reduction to confluence for parallel reduction.
Imports
open import Relation.Binary.PropositionalEquality using (_β‘_; refl) open import Function using (_β_) open import Data.Product using (_Γ_; Ξ£; Ξ£syntax; β; βsyntax; projβ; projβ) renaming (_,_ to β¨_,_β©) open import plfa.part2.Substitution using (Rename; Subst) open import plfa.part2.Untyped using (_ββ_; Ξ²; ΞΎβ; ΞΎβ; ΞΆ; _ββ _; begin_; _βββ¨_β©_; _ββ β¨_β©_; _β; abscong; appLcong; appRcong; ββ trans; _β’_; _β_; `_; #_; _,_; β ; Ζ_; _Β·_; _[_]; rename; ext; exts; Z; S_; subst; substzero)
Parallel Reduction
The parallel reduction relation is defined as follows.
infix 2 _β_ data _β_ : β {Ξ A} β (Ξ β’ A) β (Ξ β’ A) β Set where pvar : β{Ξ A}{x : Ξ β A}  β (` x) β (` x) pabs : β{Ξ}{N Nβ² : Ξ , β β’ β } β N β Nβ²  β Ζ N β Ζ Nβ² papp : β{Ξ}{L Lβ² M Mβ² : Ξ β’ β } β L β Lβ² β M β Mβ²  β L Β· M β Lβ² Β· Mβ² pbeta : β{Ξ}{N Nβ² : Ξ , β β’ β }{M Mβ² : Ξ β’ β } β N β Nβ² β M β Mβ²  β (Ζ N) Β· M β Nβ² [ Mβ² ]
The first three rules are congruences that reduce each of their parts simultaneously. The last rule reduces a lambda term and term in parallel followed by a beta step.
We remark that the pabs
, papp
, and pbeta
rules perform reduction
on all their subexpressions simultaneously. Also, the pabs
rule is
akin to the ΞΆ
rule and pbeta
is akin to Ξ²
.
Parallel reduction is reflexive.
parrefl : β{Ξ A}{M : Ξ β’ A} β M β M parrefl {Ξ} {A} {` x} = pvar parrefl {Ξ} {β } {Ζ N} = pabs parrefl parrefl {Ξ} {β } {L Β· M} = papp parrefl parrefl
We define the sequences of parallel reduction as follows.
infix 2 _β*_ infixr 2 _ββ¨_β©_ infix 3 _β data _β*_ : β {Ξ A} β (Ξ β’ A) β (Ξ β’ A) β Set where _β : β {Ξ A} (M : Ξ β’ A)  β M β* M _ββ¨_β©_ : β {Ξ A} (L : Ξ β’ A) {M N : Ξ β’ A} β L β M β M β* N  β L β* N
Exercise pardiamondeg
(practice)
Revisit the counter example to the diamond property for reduction by showing that the diamond property holds for parallel reduction in that case.
 Your code goes here
Equivalence between parallel reduction and reduction
Here we prove that for any M
and N
, M β* N
if and only if M ββ N
.
The onlyif direction is particularly easy. We start by showing
that if M ββ N
, then M β N
. The proof is by induction on
the reduction M ββ N
.
betapar : β{Ξ A}{M N : Ξ β’ A} β M ββ N  β M β N betapar {Ξ} {β } {L Β· M} (ΞΎβ r) = papp (betapar {M = L} r) parrefl betapar {Ξ} {β } {L Β· M} (ΞΎβ r) = papp parrefl (betapar {M = M} r) betapar {Ξ} {β } {(Ζ N) Β· M} Ξ² = pbeta parrefl parrefl betapar {Ξ} {β } {Ζ N} (ΞΆ r) = pabs (betapar r)
With this lemma in hand we complete the onlyif direction,
that M ββ N
implies M β* N
. The proof is a straightforward
induction on the reduction sequence M ββ N
.
betaspars : β{Ξ A} {M N : Ξ β’ A} β M ββ N  β M β* N betaspars {Ξ} {A} {Mβ} {.Mβ} (Mβ β) = Mβ β betaspars {Ξ} {A} {.L} {N} (L βββ¨ b β© bs) = L ββ¨ betapar b β© betaspars bs
Now for the other direction, that M β* N
implies M ββ N
. The
proof of this direction is a bit different because itβs not the case
that M β N
implies M ββ N
. After all, M β N
performs many
reductions. So instead we shall prove that M β N
implies M ββ N
.
parbetas : β{Ξ A}{M N : Ξ β’ A} β M β N  β M ββ N parbetas {Ξ} {A} {.(` _)} (pvar{x = x}) = (` x) β parbetas {Ξ} {β } {Ζ N} (pabs p) = abscong (parbetas p) parbetas {Ξ} {β } {L Β· M} (papp {L = L}{Lβ²}{M}{Mβ²} pβ pβ) = begin L Β· M ββ β¨ appLcong{M = M} (parbetas pβ) β© Lβ² Β· M ββ β¨ appRcong (parbetas pβ) β© Lβ² Β· Mβ² β parbetas {Ξ} {β } {(Ζ N) Β· M} (pbeta{Nβ² = Nβ²}{Mβ² = Mβ²} pβ pβ) = begin (Ζ N) Β· M ββ β¨ appLcong{M = M} (abscong (parbetas pβ)) β© (Ζ Nβ²) Β· M ββ β¨ appRcong{L = Ζ Nβ²} (parbetas pβ) β© (Ζ Nβ²) Β· Mβ² βββ¨ Ξ² β© Nβ² [ Mβ² ] β
The proof is by induction on M β N
.

Suppose
x β x
. We immediately havex ββ x
. 
Suppose
Ζ N β Ζ Nβ²
becauseN β Nβ²
. By the induction hypothesis we haveN ββ Nβ²
. We conclude thatΖ N ββ Ζ Nβ²
becauseββ
is a congruence. 
Suppose
L Β· M β Lβ² Β· Mβ²
becauseL β Lβ²
andM β Mβ²
. By the induction hypothesis, we haveL ββ Lβ²
andM ββ Mβ²
. SoL Β· M ββ Lβ² Β· M
and thenLβ² Β· M ββ Lβ² Β· Mβ²
becauseββ
is a congruence. 
Suppose
(Ζ N) Β· M β Nβ² [ Mβ² ]
becauseN β Nβ²
andM β Mβ²
. By similar reasoning, we have(Ζ N) Β· M ββ (Ζ Nβ²) Β· Mβ²
which we can following with the Ξ² reduction(Ζ Nβ²) Β· Mβ² ββ Nβ² [ Mβ² ]
.
With this lemma in hand, we complete the proof that M β* N
implies
M ββ N
with a simple induction on M β* N
.
parsbetas : β{Ξ A} {M N : Ξ β’ A} β M β* N  β M ββ N parsbetas (Mβ β) = Mβ β parsbetas (L ββ¨ p β© ps) = ββ trans (parbetas p) (parsbetas ps)
Substitution lemma for parallel reduction
Our next goal is the prove the diamond property for parallel
reduction. But to do that, we need to prove that substitution
respects parallel reduction. That is, if
N β Nβ²
and M β Mβ²
, then N [ M ] β Nβ² [ Mβ² ]
.
We cannot prove this directly by induction, so we
generalize it to: if N β Nβ²
and
the substitution Ο
pointwise parallel reduces to Ο
,
then subst Ο N β subst Ο Nβ²
. We define the notion
of pointwise parallel reduction as follows.
parsubst : β{Ξ Ξ} β Subst Ξ Ξ β Subst Ξ Ξ β Set parsubst {Ξ}{Ξ} Ο Οβ² = β{A}{x : Ξ β A} β Ο x β Οβ² x
Because substitution depends on the extension function exts
, which
in turn relies on rename
, we start with a version of the
substitution lemma, called parrename
, that is specialized to
renamings. The proof of parrename
relies on the fact that renaming
and substitution commute with one another, which is a lemma that we
import from Chapter Substitution
and restate here.
renamesubstcommute : β{Ξ Ξ}{N : Ξ , β β’ β }{M : Ξ β’ β }{Ο : Rename Ξ Ξ } β (rename (ext Ο) N) [ rename Ο M ] β‘ rename Ο (N [ M ]) renamesubstcommute {N = N} = plfa.part2.Substitution.renamesubstcommute {N = N}
Now for the parrename
lemma.
parrename : β{Ξ Ξ A} {Ο : Rename Ξ Ξ} {M Mβ² : Ξ β’ A} β M β Mβ²  β rename Ο M β rename Ο Mβ² parrename pvar = pvar parrename (pabs p) = pabs (parrename p) parrename (papp pβ pβ) = papp (parrename pβ) (parrename pβ) parrename {Ξ}{Ξ}{A}{Ο} (pbeta{Ξ}{N}{Nβ²}{M}{Mβ²} pβ pβ) with pbeta (parrename{Ο = ext Ο} pβ) (parrename{Ο = Ο} pβ) ...  G rewrite renamesubstcommute{Ξ}{Ξ}{Nβ²}{Mβ²}{Ο} = G
The proof is by induction on M β Mβ²
. The first four cases
are straightforward so we just consider the last one for pbeta
.
 Suppose
(Ζ N) Β· M β Nβ² [ Mβ² ]
becauseN β Nβ²
andM β Mβ²
. By the induction hypothesis, we haverename (ext Ο) N β rename (ext Ο) Nβ²
andrename Ο M β rename Ο Mβ²
. So bypbeta
we have(Ζ rename (ext Ο) N) Β· (rename Ο M) β (rename (ext Ο) N) [ rename Ο M ]
. However, to conclude we instead need parallel reduction torename Ο (N [ M ])
. But thankfully, renaming and substitution commute with one another.
With the parrename
lemma in hand, it is straightforward to show
that extending substitutions preserves the pointwise parallel
reduction relation.
parsubstexts : β{Ξ Ξ} {Ο Ο : Subst Ξ Ξ} β parsubst Ο Ο  β β{B} β parsubst (exts Ο {B = B}) (exts Ο) parsubstexts s {x = Z} = pvar parsubstexts s {x = S x} = parrename s
The next lemma that we need for proving that substitution respects parallel reduction is the following which states that simultaneoous substitution commutes with single substitution. We import this lemma from Chapter Substitution and restate it below.
substcommute : β{Ξ Ξ}{N : Ξ , β β’ β }{M : Ξ β’ β }{Ο : Subst Ξ Ξ } β subst (exts Ο) N [ subst Ο M ] β‘ subst Ο (N [ M ]) substcommute {N = N} = plfa.part2.Substitution.substcommute {N = N}
We are ready to prove that substitution respects parallel reduction.
substpar : β{Ξ Ξ A} {Ο Ο : Subst Ξ Ξ} {M Mβ² : Ξ β’ A} β parsubst Ο Ο β M β Mβ²  β subst Ο M β subst Ο Mβ² substpar {Ξ} {Ξ} {A} {Ο} {Ο} {` x} s pvar = s substpar {Ξ} {Ξ} {A} {Ο} {Ο} {Ζ N} s (pabs p) = pabs (substpar {Ο = exts Ο} {Ο = exts Ο} (Ξ» {A}{x} β parsubstexts s {x = x}) p) substpar {Ξ} {Ξ} {β } {Ο} {Ο} {L Β· M} s (papp pβ pβ) = papp (substpar s pβ) (substpar s pβ) substpar {Ξ} {Ξ} {β } {Ο} {Ο} {(Ζ N) Β· M} s (pbeta{Nβ² = Nβ²}{Mβ² = Mβ²} pβ pβ) with pbeta (substpar{Ο = exts Ο}{Ο = exts Ο}{M = N} (Ξ»{A}{x} β parsubstexts s {x = x}) pβ) (substpar {Ο = Ο} s pβ) ...  G rewrite substcommute{N = Nβ²}{M = Mβ²}{Ο = Ο} = G
We proceed by induction on M β Mβ²
.

Suppose
x β x
. We conclude thatΟ x β Ο x
using the premiseparsubst Ο Ο
. 
Suppose
Ζ N β Ζ Nβ²
becauseN β Nβ²
. To use the induction hypothesis, we needparsubst (exts Ο) (exts Ο)
, which we obtain byparsubstexts
. So we havesubst (exts Ο) N β subst (exts Ο) Nβ²
and conclude by rulepabs
. 
Suppose
L Β· M β Lβ² Β· Mβ²
becauseL β Lβ²
andM β Mβ²
. By the induction hypothesis we havesubst Ο L β subst Ο Lβ²
andsubst Ο M β subst Ο Mβ²
, so we conclude by rulepapp
. 
Suppose
(Ζ N) Β· M β Nβ² [ Mβ² ]
becauseN β Nβ²
andM β Mβ²
. Again we obtainparsubst (exts Ο) (exts Ο)
byparsubstexts
. So by the induction hypothesis, we havesubst (exts Ο) N β subst (exts Ο) Nβ²
andsubst Ο M β subst Ο Mβ²
. Then by rulepbeta
, we have parallel reduction tosubst (exts Ο) Nβ² [ subst Ο Mβ² ]
. Substitution commutes with itself in the following sense. For any Ο, N, and M, we have(subst (exts Ο) N) [ subst Ο M ] β‘ subst Ο (N [ M ])
So we have parallel reduction to
subst Ο (Nβ² [ Mβ² ])
.
Of course, if M β Mβ²
, then substzero M
pointwise parallel reduces
to substzero Mβ²
.
parsubstzero : β{Ξ}{A}{M Mβ² : Ξ β’ A} β M β Mβ² β parsubst (substzero M) (substzero Mβ²) parsubstzero {M} {Mβ²} p {A} {Z} = p parsubstzero {M} {Mβ²} p {A} {S x} = pvar
We conclude this section with the desired corollary, that substitution respects parallel reduction.
subpar : β{Ξ A B} {N Nβ² : Ξ , A β’ B} {M Mβ² : Ξ β’ A} β N β Nβ² β M β Mβ²  β N [ M ] β Nβ² [ Mβ² ] subpar pn pm = substpar (parsubstzero pm) pn
Parallel reduction satisfies the diamond property
The heart of the confluence proof is made of stone, or rather, of
diamond! We show that parallel reduction satisfies the diamond
property: that if M β N
and M β Nβ²
, then N β L
and Nβ² β L
for
some L
. The proof is relatively easy; it is parallel reductionβs
raison dβetre.
pardiamond : β{Ξ A} {M N Nβ² : Ξ β’ A} β M β N β M β Nβ²  β Ξ£[ L β Ξ β’ A ] (N β L) Γ (Nβ² β L) pardiamond (pvar{x = x}) pvar = β¨ ` x , β¨ pvar , pvar β© β© pardiamond (pabs p1) (pabs p2) with pardiamond p1 p2 ...  β¨ Lβ² , β¨ p3 , p4 β© β© = β¨ Ζ Lβ² , β¨ pabs p3 , pabs p4 β© β© pardiamond{Ξ}{A}{L Β· M}{N}{Nβ²} (papp{Ξ}{L}{Lβ}{M}{Mβ} p1 p3) (papp{Ξ}{L}{Lβ}{M}{Mβ} p2 p4) with pardiamond p1 p2 ...  β¨ Lβ , β¨ p5 , p6 β© β© with pardiamond p3 p4 ...  β¨ Mβ , β¨ p7 , p8 β© β© = β¨ (Lβ Β· Mβ) , β¨ (papp p5 p7) , (papp p6 p8) β© β© pardiamond (papp (pabs p1) p3) (pbeta p2 p4) with pardiamond p1 p2 ...  β¨ Nβ , β¨ p5 , p6 β© β© with pardiamond p3 p4 ...  β¨ Mβ , β¨ p7 , p8 β© β© = β¨ Nβ [ Mβ ] , β¨ pbeta p5 p7 , subpar p6 p8 β© β© pardiamond (pbeta p1 p3) (papp (pabs p2) p4) with pardiamond p1 p2 ...  β¨ Nβ , β¨ p5 , p6 β© β© with pardiamond p3 p4 ...  β¨ Mβ , β¨ p7 , p8 β© β© = β¨ (Nβ [ Mβ ]) , β¨ subpar p5 p7 , pbeta p6 p8 β© β© pardiamond {Ξ}{A} (pbeta p1 p3) (pbeta p2 p4) with pardiamond p1 p2 ...  β¨ Nβ , β¨ p5 , p6 β© β© with pardiamond p3 p4 ...  β¨ Mβ , β¨ p7 , p8 β© β© = β¨ Nβ [ Mβ ] , β¨ subpar p5 p7 , subpar p6 p8 β© β©
The proof is by induction on both premises.

Suppose
x β x
andx β x
. We chooseL = x
and immediately havex β x
andx β x
. 
Suppose
Ζ N β Ζ Nβ
andΖ N β Ζ Nβ
. By the induction hypothesis, there existsLβ²
such thatNβ β Lβ²
andNβ β Lβ²
. We chooseL = Ζ Lβ²
and bypabs
conclude thatΖ Nβ β Ζ Lβ²
and `Ζ Nβ β Ζ Lβ². 
Suppose that
L Β· M β Lβ Β· Mβ
andL Β· M β Lβ Β· Mβ
. By the induction hypothesis we haveLβ β Lβ
andLβ β Lβ
for someLβ
. Likewise, we haveMβ β Mβ
andMβ β Mβ
for someMβ
. We chooseL = Lβ Β· Mβ
and conclude with two uses ofpapp
. 
Suppose that
(Ζ N) Β· M β (Ζ Nβ) Β· Mβ
and(Ζ N) Β· M β Nβ [ Mβ ]
By the induction hypothesis we haveNβ β Nβ
andNβ β Nβ
for someNβ
. Likewise, we haveMβ β Mβ
andMβ β Mβ
for someMβ
. We chooseL = Nβ [ Mβ ]
. We have(Ζ Nβ) Β· Mβ β Nβ [ Mβ ]
by rulepbeta
and conclude thatNβ [ Mβ ] β Nβ [ Mβ ]
because substitution respects parallel reduction. 
Suppose that
(Ζ N) Β· M β Nβ [ Mβ ]
and(Ζ N) Β· M β (Ζ Nβ) Β· Mβ
. The proof of this case is the mirror image of the last one. 
Suppose that
(Ζ N) Β· M β Nβ [ Mβ ]
and(Ζ N) Β· M β Nβ [ Mβ ]
. By the induction hypothesis we haveNβ β Nβ
andNβ β Nβ
for someNβ
. Likewise, we haveMβ β Mβ
andMβ β Mβ
for someMβ
. We chooseL = Nβ [ Mβ ]
. We have both(Ζ Nβ) Β· Mβ β Nβ [ Mβ ]
and(Ζ Nβ) Β· Mβ β Nβ [ Mβ ]
by rulepbeta
Exercise (practice)
Draw pictures that represent the proofs of each of the six cases in
the above proof of pardiamond
. The pictures should consist of nodes
and directed edges, where each node is labeled with a term and each
edge represents parallel reduction.
Proof of confluence for parallel reduction
As promised at the beginning, the proof that parallel reduction is
confluent is easy now that we know it satisfies the diamond property.
We just need to prove the strip lemma, which states that
if M β N
and M β* Nβ²
, then
N β* L
and Nβ² β L
for some L
.
The following diagram illustrates the strip lemma
M
/ \
1 *
/ \
N Nβ²
\ /
* 1
\ /
L
where downward lines are instances of β
or β*
, depending on how
they are marked.
The proof of the strip lemma is a straightforward induction on M β* Nβ²
,
using the diamond property in the induction step.
strip : β{Ξ A} {M N Nβ² : Ξ β’ A} β M β N β M β* Nβ²  β Ξ£[ L β Ξ β’ A ] (N β* L) Γ (Nβ² β L) strip{Ξ}{A}{M}{N}{Nβ²} mn (M β) = β¨ N , β¨ N β , mn β© β© strip{Ξ}{A}{M}{N}{Nβ²} mn (M ββ¨ mm' β© m'n') with pardiamond mn mm' ...  β¨ L , β¨ nl , m'l β© β© with strip m'l m'n' ...  β¨ Lβ² , β¨ ll' , n'l' β© β© = β¨ Lβ² , β¨ (N ββ¨ nl β© ll') , n'l' β© β©
The proof of confluence for parallel reduction is now proved by
induction on the sequence M β* N
, using the above lemma in the
induction step.
parconfluence : β{Ξ A} {L Mβ Mβ : Ξ β’ A} β L β* Mβ β L β* Mβ  β Ξ£[ N β Ξ β’ A ] (Mβ β* N) Γ (Mβ β* N) parconfluence {Ξ}{A}{L}{.L}{N} (L β) Lβ*N = β¨ N , β¨ Lβ*N , N β β© β© parconfluence {Ξ}{A}{L}{Mββ²}{Mβ} (L ββ¨ LβMβ β© Mββ*Mββ²) Lβ*Mβ with strip LβMβ Lβ*Mβ ...  β¨ N , β¨ Mββ*N , MββN β© β© with parconfluence Mββ*Mββ² Mββ*N ...  β¨ Nβ² , β¨ Mββ²β*Nβ² , Nβ*Nβ² β© β© = β¨ Nβ² , β¨ Mββ²β*Nβ² , (Mβ ββ¨ MββN β© Nβ*Nβ²) β© β©
The step case may be illustrated as follows:
L
/ \
1 *
/ \
Mβ (a) Mβ
/ \ /
* * 1
/ \ /
Mββ²(b) N
\ /
* *
\ /
Nβ²
where downward lines are instances of β
or β*
, depending on how
they are marked. Here (a)
holds by strip
and (b)
holds by
induction.
Proof of confluence for reduction
Confluence of reduction is a corollary of confluence for parallel
reduction. From
L ββ Mβ
and L ββ Mβ
we have
L β* Mβ
and L β* Mβ
by betaspars
.
Then by confluence we obtain some L
such that
Mβ β* N
and Mβ β* N
, from which we conclude that
Mβ ββ N
and Mβ ββ N
by parsbetas
.
confluence : β{Ξ A} {L Mβ Mβ : Ξ β’ A} β L ββ Mβ β L ββ Mβ  β Ξ£[ N β Ξ β’ A ] (Mβ ββ N) Γ (Mβ ββ N) confluence Lβ Mβ Lβ Mβ with parconfluence (betaspars Lβ Mβ) (betaspars Lβ Mβ) ...  β¨ N , β¨ MββN , MββN β© β© = β¨ N , β¨ parsbetas MββN , parsbetas MββN β© β©
Notes
Broadly speaking, this proof of confluence, based on parallel
reduction, is due to W. Tait and P. MartinLof (see Barendredgt 1984,
Section 3.2). Details of the mechanization come from several sources.
The substpar
lemma is the βstrong substitutivityβ lemma of Shafer,
Tebbi, and Smolka (ITP 2015). The proofs of pardiamond
, strip
,
and parconfluence
are based on Pfenningβs 1992 technical report
about the ChurchRosser theorem. In addition, we consulted Nipkow and
Berghoferβs mechanization in Isabelle, which is based on an earlier
article by Nipkow (JAR 1996). We opted not to use the βcomplete
developmentsβ approach of Takahashi (1995) because we felt that the
proof was simple enough based solely on parallel reduction. There are
many more mechanizations of the ChurchRosser theorem that we have not
yet had the time to read, including Shankarβs (J. ACM 1988) and
Homeierβs (TPHOLs 2001).
Unicode
This chapter uses the following unicode:
β U+3015 RIGHTWARDS TRIPLE ARROW (\r== or \Rrightarrow)