:: Reduction Relations
:: by Grzegorz Bancerek
::
:: Received November 14, 1995
:: Copyright (c) 1995 Association of Mizar Users

begin

definition

let p, q be FinSequence;
func p $^ q -> FinSequence means :Def1: :: REWRITE1:def 1
it = p ^ q if ( p = {} or q = {} )
otherwise ex i being Element of NAT ex r being FinSequence st
( len p = i + 1 & r = p | (Seg i) & it = r ^ q );
existence
( ( ( p = {} or q = {} ) implies ex b₁ being FinSequence st b₁ = p ^ q ) & ( p = {} or q = {} or ex b₁ being FinSequence ex i being Element of NAT ex r being FinSequence st
( len p = i + 1 & r = p | (Seg i) & b₁ = r ^ q ) ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence holds
( ( ( p = {} or q = {} ) & b₁ = p ^ q & b₂ = p ^ q implies b₁ = b₂ ) & ( p = {} or q = {} or for i being Element of NAT
for r being FinSequence holds
( not len p = i + 1 or not r = p | (Seg i) or not b₁ = r ^ q ) or for i being Element of NAT
for r being FinSequence holds
( not len p = i + 1 or not r = p | (Seg i) or not b₂ = r ^ q ) or b₁ = b₂ ) ) ;
consistency
for b₁ being FinSequence holds verum ;

end;

:: deftheorem Def1 defines $^ REWRITE1:def 1 :
for p, q, b₃ being FinSequence holds
( ( ( p = {} or q = {} ) implies ( b₃ = p $^ q iff b₃ = p ^ q ) ) & ( p = {} or q = {} or ( b₃ = p $^ q iff ex i being Element of NAT ex r being FinSequence st
( len p = i + 1 & r = p | (Seg i) & b₃ = r ^ q ) ) ) );

Lm1: now

let p be FinSequence; :: thesis: for x being Nat st x in dom p holds
( x <= len p & x >= 0 + 1 & x > 0 )
let x be Nat; :: thesis: ( x in dom p implies ( x <= len p & x >= 0 + 1 & x > 0 ) )
assume x in dom p ; :: thesis: ( x <= len p & x >= 0 + 1 & x > 0 )
then A1: x in Seg (len p) by FINSEQ_1:def 3;
hence ( x <= len p & x >= 0 + 1 ) by FINSEQ_1:3; :: thesis: x > 0
thus x > 0 by A1, FINSEQ_1:3; :: thesis: verum

end;

Lm2: now

let p be FinSequence; :: thesis: for x being Nat st x + 1 in dom p holds
x < len p
let x be Nat; :: thesis: ( x + 1 in dom p implies x < len p )
assume x + 1 in dom p ; :: thesis: x < len p
then x + 1 <= len p by Lm1;
hence x < len p by NAT_1:13; :: thesis: verum

end;

Lm3: now

let p be FinSequence; :: thesis: for x being Nat st ( x <= len p or x < len p ) & ( x >= 1 or x > 0 ) holds
x in dom p
let x be Nat; :: thesis: ( ( x <= len p or x < len p ) & ( x >= 1 or x > 0 ) implies x in dom p )
assume that
A1: ( x <= len p or x < len p ) and
A2: ( x >= 1 or x > 0 ) ; :: thesis: x in dom p
x >= 0 + 1 by A2, NAT_1:13;
then x in Seg (len p) by A1, FINSEQ_1:3;
hence x in dom p by FINSEQ_1:def 3; :: thesis: verum

end;

Lm4: now

let p be FinSequence; :: thesis: for x being Nat st x < len p holds
x + 1 in dom p
let x be Nat; :: thesis: ( x < len p implies x + 1 in dom p )
assume x < len p ; :: thesis: x + 1 in dom p
then x + 1 <= len p by NAT_1:13;
hence x + 1 in dom p by Lm3; :: thesis: verum

end;

theorem :: REWRITE1:1

for p being FinSequence holds
( {} $^ p = p & p $^ {} = p )

proof end;

theorem Th2: :: REWRITE1:2

for q, p being FinSequence
for x being set st q <> {} holds
(p ^ <*x*>) $^ q = p ^ q

proof end;

theorem :: REWRITE1:3

for p, q being FinSequence
for x, y being set holds (p ^ <*x*>) $^ (<*y*> ^ q) = (p ^ <*y*>) ^ q

proof end;

theorem :: REWRITE1:4

for q being FinSequence
for x being set st q <> {} holds
<*x*> $^ q = q

proof end;

theorem :: REWRITE1:5

for p being FinSequence st p <> {} holds
ex x being set ex q being FinSequence st
( p = <*x*> ^ q & len p = (len q) + 1 )

proof end;

scheme :: REWRITE1:sch 1
PathCatenation{ P₁[ set , set ], F₁() -> FinSequence, F₂() -> FinSequence } :

for i being Element of NAT st i in dom (F₁() $^ F₂()) & i + 1 in dom (F₁() $^ F₂()) holds
for x, y being set st x = (F₁() $^ F₂()) . i & y = (F₁() $^ F₂()) . (i + 1) holds
P₁[x,y]

provided

A1: for i being Element of NAT st i in dom F₁() & i + 1 in dom F₁() holds
P₁[F₁() . i,F₁() . (i + 1)] and
A2: for i being Element of NAT st i in dom F₂() & i + 1 in dom F₂() holds
P₁[F₂() . i,F₂() . (i + 1)] and
A3: ( len F₁() > 0 & len F₂() > 0 & F₁() . (len F₁()) = F₂() . 1 )

proof end;

definition

let R be Relation;
mode RedSequence of R -> FinSequence means :Def2: :: REWRITE1:def 2
( len it > 0 & ( for i being Element of NAT st i in dom it & i + 1 in dom it holds
[(it . i),(it . (i + 1))] in R ) );
existence
ex b₁ being FinSequence st
( len b₁ > 0 & ( for i being Element of NAT st i in dom b₁ & i + 1 in dom b₁ holds
[(b₁ . i),(b₁ . (i + 1))] in R ) )

proof end;

end;

:: deftheorem Def2 defines RedSequence REWRITE1:def 2 :
for R being Relation
for b₂ being FinSequence holds
( b₂ is RedSequence of R iff ( len b₂ > 0 & ( for i being Element of NAT st i in dom b₂ & i + 1 in dom b₂ holds
[(b₂ . i),(b₂ . (i + 1))] in R ) ) );

registration

let R be Relation;
cluster -> non empty RedSequence of R;
coherence
for b₁ being RedSequence of R holds not b₁ is empty by Def2, CARD_1:47;

end;

theorem :: REWRITE1:6

canceled;

theorem Th7: :: REWRITE1:7

for R being Relation
for a being set holds <*a*> is RedSequence of R

proof end;

theorem Th8: :: REWRITE1:8

for R being Relation
for a, b being set st [a,b] in R holds
<*a,b*> is RedSequence of R

proof end;

theorem Th9: :: REWRITE1:9

for R being Relation
for p, q being RedSequence of R st p . (len p) = q . 1 holds
p $^ q is RedSequence of R

proof end;

theorem Th10: :: REWRITE1:10

for R being Relation
for p being RedSequence of R holds Rev p is RedSequence of R ~

proof end;

theorem Th11: :: REWRITE1:11

for R, Q being Relation st R c= Q holds
for p being RedSequence of R holds p is RedSequence of Q

proof end;

begin

definition

let R be Relation;
let a, b be set ;
pred R reduces a,b means :Def3: :: REWRITE1:def 3
ex p being RedSequence of R st
( p . 1 = a & p . (len p) = b );

end;

:: deftheorem Def3 defines reduces REWRITE1:def 3 :
for R being Relation
for a, b being set holds
( R reduces a,b iff ex p being RedSequence of R st
( p . 1 = a & p . (len p) = b ) );

definition

let R be Relation;
let a, b be set ;
pred a,b are_convertible_wrt R means :Def4: :: REWRITE1:def 4
R \/ (R ~) reduces a,b;

end;

:: deftheorem Def4 defines are_convertible_wrt REWRITE1:def 4 :
for R being Relation
for a, b being set holds
( a,b are_convertible_wrt R iff R \/ (R ~) reduces a,b );

theorem Th12: :: REWRITE1:12

for R being Relation
for a, b being set holds
( R reduces a,b iff ex p being FinSequence st
( len p > 0 & p . 1 = a & p . (len p) = b & ( for i being Element of NAT st i in dom p & i + 1 in dom p holds
[(p . i),(p . (i + 1))] in R ) ) )

proof end;

theorem Th13: :: REWRITE1:13

for R being Relation
for a being set holds R reduces a,a

proof end;

theorem Th14: :: REWRITE1:14

for a, b being set st {} reduces a,b holds
a = b

proof end;

theorem Th15: :: REWRITE1:15

for R being Relation
for a, b being set st R reduces a,b & not a in field R holds
a = b

proof end;

theorem Th16: :: REWRITE1:16

for R being Relation
for a, b being set st [a,b] in R holds
R reduces a,b

proof end;

theorem Th17: :: REWRITE1:17

for R being Relation
for a, b, c being set st R reduces a,b & R reduces b,c holds
R reduces a,c

proof end;

theorem Th18: :: REWRITE1:18

for R being Relation
for p being RedSequence of R
for i, j being Element of NAT st i in dom p & j in dom p & i <= j holds
R reduces p . i,p . j

proof end;

theorem Th19: :: REWRITE1:19

for R being Relation
for a, b being set st R reduces a,b & a <> b holds
( a in field R & b in field R )

proof end;

theorem :: REWRITE1:20

for R being Relation
for a, b being set st R reduces a,b holds
( a in field R iff b in field R ) by Th19;

theorem Th21: :: REWRITE1:21

for R being Relation
for a, b being set holds
( R reduces a,b iff ( a = b or [a,b] in R [*] ) )

proof end;

theorem Th22: :: REWRITE1:22

for R being Relation
for a, b being set holds
( R reduces a,b iff R [*] reduces a,b )

proof end;

theorem Th23: :: REWRITE1:23

for R, Q being Relation st R c= Q holds
for a, b being set st R reduces a,b holds
Q reduces a,b

proof end;

theorem :: REWRITE1:24

for R being Relation
for X, a, b being set holds
( R reduces a,b iff R \/ (id X) reduces a,b )

proof end;

theorem Th25: :: REWRITE1:25

for R being Relation
for a, b being set st R reduces a,b holds
R ~ reduces b,a

proof end;

Lm5: for R being Relation
for a, b being set st a,b are_convertible_wrt R holds
b,a are_convertible_wrt R

proof end;

theorem Th26: :: REWRITE1:26

for R being Relation
for a, b being set st R reduces a,b holds
( a,b are_convertible_wrt R & b,a are_convertible_wrt R )

proof end;

theorem Th27: :: REWRITE1:27

for R being Relation
for a being set holds a,a are_convertible_wrt R

proof end;

theorem Th28: :: REWRITE1:28

for a, b being set st a,b are_convertible_wrt {} holds
a = b

proof end;

theorem :: REWRITE1:29

for R being Relation
for a, b being set st a,b are_convertible_wrt R & not a in field R holds
a = b

proof end;

theorem Th30: :: REWRITE1:30

for R being Relation
for a, b being set st [a,b] in R holds
a,b are_convertible_wrt R

proof end;

theorem Th31: :: REWRITE1:31

for R being Relation
for a, b, c being set st a,b are_convertible_wrt R & b,c are_convertible_wrt R holds
a,c are_convertible_wrt R

proof end;

theorem :: REWRITE1:32

for R being Relation
for a, b being set st a,b are_convertible_wrt R holds
b,a are_convertible_wrt R by Lm5;

theorem Th33: :: REWRITE1:33

for R being Relation
for a, b being set st a,b are_convertible_wrt R & a <> b holds
( a in field R & b in field R )

proof end;

definition

let R be Relation;
let a be set ;
pred a is_a_normal_form_wrt R means :: REWRITE1:def 5
for b being set holds not [a,b] in R;

end;

:: deftheorem defines is_a_normal_form_wrt REWRITE1:def 5 :
for R being Relation
for a being set holds
( a is_a_normal_form_wrt R iff for b being set holds not [a,b] in R );

theorem Th34: :: REWRITE1:34

for R being Relation
for a, b being set st a is_a_normal_form_wrt R & R reduces a,b holds
a = b

proof end;

theorem Th35: :: REWRITE1:35

for R being Relation
for a being set st not a in field R holds
a is_a_normal_form_wrt R

proof end;

definition

let R be Relation;
let a, b be set ;
pred b is_a_normal_form_of a,R means :Def6: :: REWRITE1:def 6
( b is_a_normal_form_wrt R & R reduces a,b );
pred a,b are_convergent_wrt R means :Def7: :: REWRITE1:def 7
ex c being set st
( R reduces a,c & R reduces b,c );
pred a,b are_divergent_wrt R means :Def8: :: REWRITE1:def 8
ex c being set st
( R reduces c,a & R reduces c,b );
pred a,b are_convergent<=1_wrt R means :Def9: :: REWRITE1:def 9
ex c being set st
( ( [a,c] in R or a = c ) & ( [b,c] in R or b = c ) );
pred a,b are_divergent<=1_wrt R means :Def10: :: REWRITE1:def 10
ex c being set st
( ( [c,a] in R or a = c ) & ( [c,b] in R or b = c ) );

end;

:: deftheorem Def6 defines is_a_normal_form_of REWRITE1:def 6 :
for R being Relation
for a, b being set holds
( b is_a_normal_form_of a,R iff ( b is_a_normal_form_wrt R & R reduces a,b ) );

:: deftheorem Def7 defines are_convergent_wrt REWRITE1:def 7 :
for R being Relation
for a, b being set holds
( a,b are_convergent_wrt R iff ex c being set st
( R reduces a,c & R reduces b,c ) );

:: deftheorem Def8 defines are_divergent_wrt REWRITE1:def 8 :
for R being Relation
for a, b being set holds
( a,b are_divergent_wrt R iff ex c being set st
( R reduces c,a & R reduces c,b ) );

:: deftheorem Def9 defines are_convergent<=1_wrt REWRITE1:def 9 :
for R being Relation
for a, b being set holds
( a,b are_convergent<=1_wrt R iff ex c being set st
( ( [a,c] in R or a = c ) & ( [b,c] in R or b = c ) ) );

:: deftheorem Def10 defines are_divergent<=1_wrt REWRITE1:def 10 :
for R being Relation
for a, b being set holds
( a,b are_divergent<=1_wrt R iff ex c being set st
( ( [c,a] in R or a = c ) & ( [c,b] in R or b = c ) ) );

theorem Th36: :: REWRITE1:36

for R being Relation
for a being set st not a in field R holds
a is_a_normal_form_of a,R

proof end;

theorem Th37: :: REWRITE1:37

for R being Relation
for a, b being set st R reduces a,b holds
( a,b are_convergent_wrt R & a,b are_divergent_wrt R & b,a are_convergent_wrt R & b,a are_divergent_wrt R )

proof end;

theorem Th38: :: REWRITE1:38

for R being Relation
for a, b being set st ( a,b are_convergent_wrt R or a,b are_divergent_wrt R ) holds
a,b are_convertible_wrt R

proof end;

theorem Th39: :: REWRITE1:39

for R being Relation
for a being set holds
( a,a are_convergent_wrt R & a,a are_divergent_wrt R )

proof end;

theorem Th40: :: REWRITE1:40

for a, b being set st ( a,b are_convergent_wrt {} or a,b are_divergent_wrt {} ) holds
a = b

proof end;

theorem :: REWRITE1:41

for R being Relation
for a, b being set st a,b are_convergent_wrt R holds
b,a are_convergent_wrt R

proof end;

theorem :: REWRITE1:42

for R being Relation
for a, b being set st a,b are_divergent_wrt R holds
b,a are_divergent_wrt R

proof end;

theorem Th43: :: REWRITE1:43

for R being Relation
for a, b, c being set st ( ( R reduces a,b & b,c are_convergent_wrt R ) or ( a,b are_convergent_wrt R & R reduces c,b ) ) holds
a,c are_convergent_wrt R

proof end;

theorem :: REWRITE1:44

for R being Relation
for a, b, c being set st ( ( R reduces b,a & b,c are_divergent_wrt R ) or ( a,b are_divergent_wrt R & R reduces b,c ) ) holds
a,c are_divergent_wrt R

proof end;

theorem Th45: :: REWRITE1:45

for R being Relation
for a, b being set st a,b are_convergent<=1_wrt R holds
a,b are_convergent_wrt R

proof end;

theorem Th46: :: REWRITE1:46

for R being Relation
for a, b being set st a,b are_divergent<=1_wrt R holds
a,b are_divergent_wrt R

proof end;

definition

let R be Relation;
let a be set ;
pred a has_a_normal_form_wrt R means :Def11: :: REWRITE1:def 11
ex b being set st b is_a_normal_form_of a,R;

end;

:: deftheorem Def11 defines has_a_normal_form_wrt REWRITE1:def 11 :
for R being Relation
for a being set holds
( a has_a_normal_form_wrt R iff ex b being set st b is_a_normal_form_of a,R );

theorem Th47: :: REWRITE1:47

for R being Relation
for a being set st not a in field R holds
a has_a_normal_form_wrt R

proof end;

definition

let R be Relation;
let a be set ;
assume that
A1: a has_a_normal_form_wrt R and
A2: for b, c being set st b is_a_normal_form_of a,R & c is_a_normal_form_of a,R holds
b = c ;
func nf (a,R) -> set means :Def12: :: REWRITE1:def 12
it is_a_normal_form_of a,R;
existence
ex b₁ being set st b₁ is_a_normal_form_of a,R by A1, Def11;
uniqueness
for b₁, b₂ being set st b₁ is_a_normal_form_of a,R & b₂ is_a_normal_form_of a,R holds
b₁ = b₂ by A2;

end;

:: deftheorem Def12 defines nf REWRITE1:def 12 :
for R being Relation
for a being set st a has_a_normal_form_wrt R & ( for b, c being set st b is_a_normal_form_of a,R & c is_a_normal_form_of a,R holds
b = c ) holds
for b₃ being set holds
( b₃ = nf (a,R) iff b₃ is_a_normal_form_of a,R );

begin

definition

let R be Relation;
attr R is co-well_founded means :Def13: :: REWRITE1:def 13
R ~ is well_founded ;
attr R is weakly-normalizing means :Def14: :: REWRITE1:def 14
for a being set st a in field R holds
a has_a_normal_form_wrt R;
attr R is strongly-normalizing means :: REWRITE1:def 15
for f being ManySortedSet of NAT holds
not for i being Element of NAT holds [(f . i),(f . (i + 1))] in R;

end;

:: deftheorem Def13 defines co-well_founded REWRITE1:def 13 :
for R being Relation holds
( R is co-well_founded iff R ~ is well_founded );

:: deftheorem Def14 defines weakly-normalizing REWRITE1:def 14 :
for R being Relation holds
( R is weakly-normalizing iff for a being set st a in field R holds
a has_a_normal_form_wrt R );

:: deftheorem defines strongly-normalizing REWRITE1:def 15 :
for R being Relation holds
( R is strongly-normalizing iff for f being ManySortedSet of NAT holds
not for i being Element of NAT holds [(f . i),(f . (i + 1))] in R );

definition

let R be Relation;
redefine attr R is co-well_founded means :Def16: :: REWRITE1:def 16
for Y being set st Y c= field R & Y <> {} holds
ex a being set st
( a in Y & ( for b being set st b in Y & a <> b holds
not [a,b] in R ) );
compatibility
( R is co-well_founded iff for Y being set st Y c= field R & Y <> {} holds
ex a being set st
( a in Y & ( for b being set st b in Y & a <> b holds
not [a,b] in R ) ) )

proof end;

end;

:: deftheorem Def16 defines co-well_founded REWRITE1:def 16 :
for R being Relation holds
( R is co-well_founded iff for Y being set st Y c= field R & Y <> {} holds
ex a being set st
( a in Y & ( for b being set st b in Y & a <> b holds
not [a,b] in R ) ) );

scheme :: REWRITE1:sch 2
coNoetherianInduction{ F₁() -> Relation, P₁[ set ] } :

for a being set st a in field F₁() holds
P₁[a]

provided

A1: F₁() is co-well_founded and
A2: for a being set st ( for b being set st [a,b] in F₁() & a <> b holds
P₁[b] ) holds
P₁[a]

proof end;

registration

cluster Relation-like strongly-normalizing -> irreflexive co-well_founded set ;
coherence
for b₁ being Relation st b₁ is strongly-normalizing holds
( b₁ is irreflexive & b₁ is co-well_founded )

proof end;

cluster Relation-like irreflexive co-well_founded -> strongly-normalizing set ;
coherence
for b₁ being Relation st b₁ is co-well_founded & b₁ is irreflexive holds
b₁ is strongly-normalizing

proof end;

end;

registration

cluster empty Relation-like -> weakly-normalizing strongly-normalizing set ;
coherence
for b₁ being Relation st b₁ is empty holds
( b₁ is weakly-normalizing & b₁ is strongly-normalizing )

proof end;

end;

theorem :: REWRITE1:48

for Q being co-well_founded Relation
for R being Relation st R c= Q holds
R is co-well_founded

proof end;

registration

cluster Relation-like strongly-normalizing -> weakly-normalizing set ;
coherence
for b₁ being Relation st b₁ is strongly-normalizing holds
b₁ is weakly-normalizing

proof end;

end;

begin

definition

let R, Q be Relation;
pred R commutes-weakly_with Q means :: REWRITE1:def 17
for a, b, c being set st [a,b] in R & [a,c] in Q holds
ex d being set st
( Q reduces b,d & R reduces c,d );
symmetry
for R, Q being Relation st ( for a, b, c being set st [a,b] in R & [a,c] in Q holds
ex d being set st
( Q reduces b,d & R reduces c,d ) ) holds
for a, b, c being set st [a,b] in Q & [a,c] in R holds
ex d being set st
( R reduces b,d & Q reduces c,d )

proof end;

pred R commutes_with Q means :Def18: :: REWRITE1:def 18
for a, b, c being set st R reduces a,b & Q reduces a,c holds
ex d being set st
( Q reduces b,d & R reduces c,d );
symmetry
for R, Q being Relation st ( for a, b, c being set st R reduces a,b & Q reduces a,c holds
ex d being set st
( Q reduces b,d & R reduces c,d ) ) holds
for a, b, c being set st Q reduces a,b & R reduces a,c holds
ex d being set st
( R reduces b,d & Q reduces c,d )

proof end;

end;

:: deftheorem defines commutes-weakly_with REWRITE1:def 17 :
for R, Q being Relation holds
( R commutes-weakly_with Q iff for a, b, c being set st [a,b] in R & [a,c] in Q holds
ex d being set st
( Q reduces b,d & R reduces c,d ) );

:: deftheorem Def18 defines commutes_with REWRITE1:def 18 :
for R, Q being Relation holds
( R commutes_with Q iff for a, b, c being set st R reduces a,b & Q reduces a,c holds
ex d being set st
( Q reduces b,d & R reduces c,d ) );

theorem :: REWRITE1:49

for R, Q being Relation st R commutes_with Q holds
R commutes-weakly_with Q

proof end;

definition

let R be Relation;
attr R is with_UN_property means :Def19: :: REWRITE1:def 19
for a, b being set st a is_a_normal_form_wrt R & b is_a_normal_form_wrt R & a,b are_convertible_wrt R holds
a = b;
attr R is with_NF_property means :: REWRITE1:def 20
for a, b being set st a is_a_normal_form_wrt R & a,b are_convertible_wrt R holds
R reduces b,a;
attr R is subcommutative means :Def21: :: REWRITE1:def 21
for a, b, c being set st [a,b] in R & [a,c] in R holds
b,c are_convergent<=1_wrt R;
attr R is confluent means :Def22: :: REWRITE1:def 22
for a, b being set st a,b are_divergent_wrt R holds
a,b are_convergent_wrt R;
attr R is with_Church-Rosser_property means :Def23: :: REWRITE1:def 23
for a, b being set st a,b are_convertible_wrt R holds
a,b are_convergent_wrt R;
attr R is locally-confluent means :Def24: :: REWRITE1:def 24
for a, b, c being set st [a,b] in R & [a,c] in R holds
b,c are_convergent_wrt R;

end;

:: deftheorem Def19 defines with_UN_property REWRITE1:def 19 :
for R being Relation holds
( R is with_UN_property iff for a, b being set st a is_a_normal_form_wrt R & b is_a_normal_form_wrt R & a,b are_convertible_wrt R holds
a = b );

:: deftheorem defines with_NF_property REWRITE1:def 20 :
for R being Relation holds
( R is with_NF_property iff for a, b being set st a is_a_normal_form_wrt R & a,b are_convertible_wrt R holds
R reduces b,a );

:: deftheorem Def21 defines subcommutative REWRITE1:def 21 :
for R being Relation holds
( R is subcommutative iff for a, b, c being set st [a,b] in R & [a,c] in R holds
b,c are_convergent<=1_wrt R );

:: deftheorem Def22 defines confluent REWRITE1:def 22 :
for R being Relation holds
( R is confluent iff for a, b being set st a,b are_divergent_wrt R holds
a,b are_convergent_wrt R );

:: deftheorem Def23 defines with_Church-Rosser_property REWRITE1:def 23 :
for R being Relation holds
( R is with_Church-Rosser_property iff for a, b being set st a,b are_convertible_wrt R holds
a,b are_convergent_wrt R );

:: deftheorem Def24 defines locally-confluent REWRITE1:def 24 :
for R being Relation holds
( R is locally-confluent iff for a, b, c being set st [a,b] in R & [a,c] in R holds
b,c are_convergent_wrt R );

theorem Th50: :: REWRITE1:50

for R being Relation st R is subcommutative holds
for a, b, c being set st R reduces a,b & [a,c] in R holds
b,c are_convergent_wrt R

proof end;

theorem :: REWRITE1:51

for R being Relation holds
( R is confluent iff R commutes_with R )

proof end;

theorem Th52: :: REWRITE1:52

for R being Relation holds
( R is confluent iff for a, b, c being set st R reduces a,b & [a,c] in R holds
b,c are_convergent_wrt R )

proof end;

theorem :: REWRITE1:53

for R being Relation holds
( R is locally-confluent iff R commutes-weakly_with R )

proof end;

registration

cluster Relation-like with_Church-Rosser_property -> confluent set ;
coherence
for b₁ being Relation st b₁ is with_Church-Rosser_property holds
b₁ is confluent

proof end;

cluster Relation-like confluent -> with_Church-Rosser_property locally-confluent set ;
coherence
for b₁ being Relation st b₁ is confluent holds
( b₁ is locally-confluent & b₁ is with_Church-Rosser_property )

proof end;

cluster Relation-like subcommutative -> confluent set ;
coherence
for b₁ being Relation st b₁ is subcommutative holds
b₁ is confluent

proof end;

cluster Relation-like with_Church-Rosser_property -> with_NF_property set ;
coherence
for b₁ being Relation st b₁ is with_Church-Rosser_property holds
b₁ is with_NF_property

proof end;

cluster Relation-like with_NF_property -> with_UN_property set ;
coherence
for b₁ being Relation st b₁ is with_NF_property holds
b₁ is with_UN_property

proof end;

cluster Relation-like weakly-normalizing with_UN_property -> with_Church-Rosser_property set ;
coherence
for b₁ being Relation st b₁ is with_UN_property & b₁ is weakly-normalizing holds
b₁ is with_Church-Rosser_property

proof end;

end;

registration

cluster empty Relation-like -> subcommutative set ;
coherence
for b₁ being Relation st b₁ is empty holds
b₁ is subcommutative

proof end;

end;

theorem Th54: :: REWRITE1:54

for R being with_UN_property Relation
for a, b, c being set st b is_a_normal_form_of a,R & c is_a_normal_form_of a,R holds
b = c

proof end;

theorem Th55: :: REWRITE1:55

for R being weakly-normalizing with_UN_property Relation
for a being set holds nf (a,R) is_a_normal_form_of a,R

proof end;

theorem Th56: :: REWRITE1:56

for R being weakly-normalizing with_UN_property Relation
for a, b being set st a,b are_convertible_wrt R holds
nf (a,R) = nf (b,R)

proof end;

registration

cluster Relation-like strongly-normalizing locally-confluent -> confluent set ;
coherence
for b₁ being Relation st b₁ is strongly-normalizing & b₁ is locally-confluent holds
b₁ is confluent

proof end;

end;

definition

let R be Relation;
attr R is complete means :Def25: :: REWRITE1:def 25
( R is confluent & R is strongly-normalizing );

end;

:: deftheorem Def25 defines complete REWRITE1:def 25 :
for R being Relation holds
( R is complete iff ( R is confluent & R is strongly-normalizing ) );

registration

cluster Relation-like complete -> strongly-normalizing confluent set ;
coherence
for b₁ being Relation st b₁ is complete holds
( b₁ is confluent & b₁ is strongly-normalizing ) by Def25;
cluster Relation-like strongly-normalizing confluent -> complete set ;
coherence
for b₁ being Relation st b₁ is confluent & b₁ is strongly-normalizing holds
b₁ is complete by Def25;

end;

registration

cluster non empty Relation-like complete set ;
existence
ex b₁ being non empty Relation st b₁ is complete

proof end;

end;

theorem :: REWRITE1:57

for R, Q being with_Church-Rosser_property Relation st R commutes_with Q holds
R \/ Q is with_Church-Rosser_property

proof end;

theorem :: REWRITE1:58

for R being Relation holds
( R is confluent iff R [*] is locally-confluent )

proof end;

theorem :: REWRITE1:59

for R being Relation holds
( R is confluent iff R [*] is subcommutative )

proof end;

begin

definition

let R, Q be Relation;
pred R,Q are_equivalent means :: REWRITE1:def 26
for a, b being set holds
( a,b are_convertible_wrt R iff a,b are_convertible_wrt Q );
symmetry
for R, Q being Relation st ( for a, b being set holds
( a,b are_convertible_wrt R iff a,b are_convertible_wrt Q ) ) holds
for a, b being set holds
( a,b are_convertible_wrt Q iff a,b are_convertible_wrt R ) ;

end;

:: deftheorem defines are_equivalent REWRITE1:def 26 :
for R, Q being Relation holds
( R,Q are_equivalent iff for a, b being set holds
( a,b are_convertible_wrt R iff a,b are_convertible_wrt Q ) );

definition

let R be Relation;
let a, b be set ;
pred a,b are_critical_wrt R means :Def27: :: REWRITE1:def 27
( a,b are_divergent<=1_wrt R & not a,b are_convergent_wrt R );

end;

:: deftheorem Def27 defines are_critical_wrt REWRITE1:def 27 :
for R being Relation
for a, b being set holds
( a,b are_critical_wrt R iff ( a,b are_divergent<=1_wrt R & not a,b are_convergent_wrt R ) );

theorem Th60: :: REWRITE1:60

for R being Relation
for a, b being set st a,b are_critical_wrt R holds
a,b are_convertible_wrt R

proof end;

theorem :: REWRITE1:61

for R being Relation st ( for a, b being set holds not a,b are_critical_wrt R ) holds
R is locally-confluent

proof end;

theorem :: REWRITE1:62

for R, Q being Relation st ( for a, b being set st [a,b] in Q holds
a,b are_critical_wrt R ) holds
R,R \/ Q are_equivalent

proof end;

theorem Th63: :: REWRITE1:63

for R being Relation ex Q being complete Relation st
( field Q c= field R & ( for a, b being set holds
( a,b are_convertible_wrt R iff a,b are_convergent_wrt Q ) ) )

proof end;

definition

let R be Relation;
mode Completion of R -> complete Relation means :Def28: :: REWRITE1:def 28
for a, b being set holds
( a,b are_convertible_wrt R iff a,b are_convergent_wrt it );
existence
ex b₁ being complete Relation st
for a, b being set holds
( a,b are_convertible_wrt R iff a,b are_convergent_wrt b₁ )

proof end;

end;

:: deftheorem Def28 defines Completion REWRITE1:def 28 :
for R being Relation
for b₂ being complete Relation holds
( b₂ is Completion of R iff for a, b being set holds
( a,b are_convertible_wrt R iff a,b are_convergent_wrt b₂ ) );

theorem :: REWRITE1:64

for R being Relation
for C being Completion of R holds R,C are_equivalent

proof end;

theorem :: REWRITE1:65

for R being Relation
for Q being complete Relation st R,Q are_equivalent holds
Q is Completion of R

proof end;

theorem :: REWRITE1:66

for R being Relation
for C being Completion of R
for a, b being set holds
( a,b are_convertible_wrt R iff nf (a,C) = nf (b,C) )

proof end;