:: by Grzegorz Bancerek

::

:: Received November 14, 1995

:: Copyright (c) 1995-2012 Association of Mizar Users

begin

definition

let p, q be FinSequence;

( ( ( p = {} or q = {} ) implies ex b_{1} being FinSequence st b_{1} = p ^ q ) & ( p = {} or q = {} or ex b_{1} being FinSequence ex i being Element of NAT ex r being FinSequence st

( len p = i + 1 & r = p | (Seg i) & b_{1} = r ^ q ) ) )

for b_{1}, b_{2} being FinSequence holds

( ( ( p = {} or q = {} ) & b_{1} = p ^ q & b_{2} = p ^ q implies b_{1} = b_{2} ) & ( 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_{1} = 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_{2} = r ^ q ) or b_{1} = b_{2} ) )
;

consistency

for b_{1} being FinSequence holds verum
;

end;
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 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 );

( ( ( p = {} or q = {} ) implies ex b

( len p = i + 1 & r = p | (Seg i) & b

proof end;

uniqueness for b

( ( ( p = {} or q = {} ) & b

for r being FinSequence holds

( not len p = i + 1 or not r = p | (Seg i) or not b

for r being FinSequence holds

( not len p = i + 1 or not r = p | (Seg i) or not b

consistency

for b

:: deftheorem Def1 defines $^ REWRITE1:def 1 :

for p, q, b_{3} being FinSequence holds

( ( ( p = {} or q = {} ) implies ( b_{3} = p $^ q iff b_{3} = p ^ q ) ) & ( p = {} or q = {} or ( b_{3} = p $^ q iff ex i being Element of NAT ex r being FinSequence st

( len p = i + 1 & r = p | (Seg i) & b_{3} = r ^ q ) ) ) );

for p, q, b

( ( ( p = {} or q = {} ) implies ( b

( len p = i + 1 & r = p | (Seg i) & b

Lm1: now :: thesis: for p being FinSequence

for x being Nat st x in dom p holds

( x <= len p & x >= 0 + 1 & x > 0 )

for x being Nat st x in dom p holds

( x <= len p & x >= 0 + 1 & x > 0 )

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:1; :: thesis: x > 0

thus x > 0 by A1, FINSEQ_1:1; :: thesis: verum

end;
( 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:1; :: thesis: x > 0

thus x > 0 by A1, FINSEQ_1:1; :: thesis: verum

Lm2: now :: thesis: for p being FinSequence

for x being Nat st x + 1 in dom p holds

x < len p

for x being Nat st x + 1 in dom p holds

x < len p

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;
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

Lm3: now :: thesis: for p being FinSequence

for x being Nat st ( x <= len p or x < len p ) & ( x >= 1 or x > 0 ) holds

x in dom p

for x being Nat st ( x <= len p or x < len p ) & ( x >= 1 or x > 0 ) holds

x in dom p

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:1;

hence x in dom p by FINSEQ_1:def 3; :: thesis: verum

end;
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:1;

hence x in dom p by FINSEQ_1:def 3; :: thesis: verum

Lm4: now :: thesis: for p being FinSequence

for x being Nat st x < len p holds

x + 1 in dom p

for x being Nat st x < len p holds

x + 1 in dom p

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;
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

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 )

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_{1}[ set , set ], F_{1}() -> FinSequence, F_{2}() -> FinSequence } :

PathCatenation{ P

for i being Element of NAT st i in dom (F_{1}() $^ F_{2}()) & i + 1 in dom (F_{1}() $^ F_{2}()) holds

for x, y being set st x = (F_{1}() $^ F_{2}()) . i & y = (F_{1}() $^ F_{2}()) . (i + 1) holds

P_{1}[x,y]

providedfor x, y being set st x = (F

P

A1:
for i being Element of NAT st i in dom F_{1}() & i + 1 in dom F_{1}() holds

P_{1}[F_{1}() . i,F_{1}() . (i + 1)]
and

A2: for i being Element of NAT st i in dom F_{2}() & i + 1 in dom F_{2}() holds

P_{1}[F_{2}() . i,F_{2}() . (i + 1)]
and

A3: ( len F_{1}() > 0 & len F_{2}() > 0 & F_{1}() . (len F_{1}()) = F_{2}() . 1 )

P

A2: for i being Element of NAT st i in dom F

P

A3: ( len F

proof end;

definition

let R be Relation;

ex b_{1} being FinSequence st

( len b_{1} > 0 & ( for i being Element of NAT st i in dom b_{1} & i + 1 in dom b_{1} holds

[(b_{1} . i),(b_{1} . (i + 1))] in R ) )

end;
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 ( 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 ) );

ex b

( len b

[(b

proof end;

:: deftheorem Def2 defines RedSequence REWRITE1:def 2 :

for R being Relation

for b_{2} being FinSequence holds

( b_{2} is RedSequence of R iff ( len b_{2} > 0 & ( for i being Element of NAT st i in dom b_{2} & i + 1 in dom b_{2} holds

[(b_{2} . i),(b_{2} . (i + 1))] in R ) ) );

for R being Relation

for b

( b

[(b

registration

let R be Relation;

coherence

for b_{1} being RedSequence of R holds not b_{1} is empty
by Def2, CARD_1:27;

end;
coherence

for b

theorem Th8: :: REWRITE1:8

for R being Relation

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

p $^ q is RedSequence of R

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

p $^ q is RedSequence of R

proof end;

begin

definition

let R be Relation;

let a, b be set ;

end;
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 );

ex p being RedSequence of R st

( p . 1 = a & p . (len p) = b );

:: 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 ) );

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 ) );

:: 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 );

for R being Relation

for a, b being set holds

( a,b are_convertible_wrt R iff R \/ (R ~) reduces a,b );

theorem Th11: :: REWRITE1:11

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 ) ) )

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 Th17: :: REWRITE1:17

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

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 Th18: :: REWRITE1:18

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 )

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:19

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 Th25: :: REWRITE1:25

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 )

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 Th30: :: REWRITE1:30

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

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:31

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;

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

b,a are_convertible_wrt R by Lm5;

theorem Th32: :: REWRITE1:32

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 )

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;

:: 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 );

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 );

definition

let R be Relation;

let a, b be set ;

end;
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 );

( 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 );

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 );

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 ) );

ex c being set st

( ( [a,c] in R or a = c ) & ( [b,c] in R or b = c ) );

:: 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 ) );

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 ) );

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 ) );

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 ) ) );

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 ) ) );

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, 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 )

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 Th37: :: REWRITE1:37

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

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 Th42: :: REWRITE1:42

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

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:43

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

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 Th44: :: REWRITE1:44

for R being Relation

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

a,b are_convergent_wrt R

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

a,b are_convergent_wrt R

proof end;

definition

let R be Relation;

let a be set ;

end;
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;

ex b being set st b is_a_normal_form_of a,R;

:: 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 );

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 );

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 ;

existence

ex b_{1} being set st b_{1} is_a_normal_form_of a,R
by A1, Def11;

uniqueness

for b_{1}, b_{2} being set st b_{1} is_a_normal_form_of a,R & b_{2} is_a_normal_form_of a,R holds

b_{1} = b_{2}
by A2;

end;
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 ;

existence

ex b

uniqueness

for b

b

:: 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_{3} being set holds

( b_{3} = nf (a,R) iff b_{3} is_a_normal_form_of a,R );

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

( b

begin

definition

let R be Relation;

end;
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;

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;

for f being ManySortedSet of NAT holds

not for i being Element of NAT holds [(f . i),(f . (i + 1))] in R;

:: deftheorem Def13 defines co-well_founded REWRITE1:def 13 :

for R being Relation holds

( R is co-well_founded iff R ~ is well_founded );

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 );

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 );

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;

( 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 ) ) )

end;
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 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 ) );

( 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;

:: 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 ) ) );

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 ) ) );

registration

coherence

for b_{1} being Relation st b_{1} is strongly-normalizing holds

( b_{1} is irreflexive & b_{1} is co-well_founded )

for b_{1} being Relation st b_{1} is co-well_founded & b_{1} is irreflexive holds

b_{1} is strongly-normalizing

end;
for b

( b

proof end;

coherence for b

b

proof end;

registration

coherence

for b_{1} being Relation st b_{1} is empty holds

( b_{1} is weakly-normalizing & b_{1} is strongly-normalizing )

end;
for b

( b

proof end;

registration

coherence

for b_{1} being Relation st b_{1} is strongly-normalizing holds

b_{1} is weakly-normalizing

end;
for b

b

proof end;

begin

definition

let R, Q be Relation;

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 )

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 )

end;
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 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 );

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 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 );

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;

:: 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 ) );

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 ) );

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 ) );

definition

let R be Relation;

end;
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;

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;

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;

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;

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;

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;

for a, b, c being set st [a,b] in R & [a,c] in R holds

b,c are_convergent_wrt R;

:: 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 );

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 );

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 );

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 );

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 );

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 );

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 Th49: :: REWRITE1:49

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

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 Th51: :: REWRITE1:51

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 )

( 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;

registration

coherence

for b_{1} being Relation st b_{1} is with_Church-Rosser_property holds

b_{1} is confluent

for b_{1} being Relation st b_{1} is confluent holds

( b_{1} is locally-confluent & b_{1} is with_Church-Rosser_property )

for b_{1} being Relation st b_{1} is subcommutative holds

b_{1} is confluent

for b_{1} being Relation st b_{1} is with_Church-Rosser_property holds

b_{1} is with_NF_property

for b_{1} being Relation st b_{1} is with_NF_property holds

b_{1} is with_UN_property

for b_{1} being Relation st b_{1} is with_UN_property & b_{1} is weakly-normalizing holds

b_{1} is with_Church-Rosser_property

end;
for b

b

proof end;

coherence for b

( b

proof end;

coherence for b

b

proof end;

coherence for b

b

proof end;

coherence for b

b

proof end;

coherence for b

b

proof end;

registration
end;

theorem Th53: :: REWRITE1:53

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

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 Th54: :: REWRITE1:54

for R being weakly-normalizing with_UN_property Relation

for a being set holds nf (a,R) is_a_normal_form_of a,R

for a being set holds nf (a,R) is_a_normal_form_of a,R

proof end;

theorem Th55: :: REWRITE1:55

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)

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

nf (a,R) = nf (b,R)

proof end;

registration

coherence

for b_{1} being Relation st b_{1} is strongly-normalizing & b_{1} is locally-confluent holds

b_{1} is confluent

end;
for b

b

proof end;

:: deftheorem Def25 defines complete REWRITE1:def 25 :

for R being Relation holds

( R is complete iff ( R is confluent & R is strongly-normalizing ) );

for R being Relation holds

( R is complete iff ( R is confluent & R is strongly-normalizing ) );

registration

coherence

for b_{1} being Relation st b_{1} is complete holds

( b_{1} is confluent & b_{1} is strongly-normalizing )
by Def25;

coherence

for b_{1} being Relation st b_{1} is confluent & b_{1} is strongly-normalizing holds

b_{1} is complete
by Def25;

end;
for b

( b

coherence

for b

b

theorem :: REWRITE1:56

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

R \/ Q is with_Church-Rosser_property

R \/ Q is with_Church-Rosser_property

proof end;

begin

definition

let R, Q be Relation;

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;
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 a, b being set holds

( a,b are_convertible_wrt R iff a,b are_convertible_wrt Q );

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 ) ;

:: 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 ) );

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 ;

end;
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 );

( a,b are_divergent<=1_wrt R & not a,b are_convergent_wrt R );

:: 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 ) );

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 :: REWRITE1:60

for R being Relation st ( for a, b being set holds not a,b are_critical_wrt R ) holds

R is locally-confluent

R is locally-confluent

proof end;

theorem :: REWRITE1:61

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

a,b are_critical_wrt R ) holds

R,R \/ Q are_equivalent

proof end;

theorem Th62: :: REWRITE1:62

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 ) ) )

( 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;

ex b_{1} being complete Relation st

for a, b being set holds

( a,b are_convertible_wrt R iff a,b are_convergent_wrt b_{1} )

end;
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 for a, b being set holds

( a,b are_convertible_wrt R iff a,b are_convergent_wrt it );

ex b

for a, b being set holds

( a,b are_convertible_wrt R iff a,b are_convergent_wrt b

proof end;

:: deftheorem Def28 defines Completion REWRITE1:def 28 :

for R being Relation

for b_{2} being complete Relation holds

( b_{2} is Completion of R iff for a, b being set holds

( a,b are_convertible_wrt R iff a,b are_convergent_wrt b_{2} ) );

for R being Relation

for b

( b

( a,b are_convertible_wrt R iff a,b are_convergent_wrt b

theorem :: REWRITE1:65

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) )

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;