:: REWRITE1 semantic presentation

definition

let c₁, c₂ be FinSequence;
func c₁ $^ c₂ -> FinSequence means :Def1: :: REWRITE1:def 1
a₃ = a₁ ^ a₂ if ( a₁ = {} or a₂ = {} )
otherwise ex b₁ being Natex b₂ being FinSequence st
( len a₁ = b₁ + 1 & b₂ = a₁ | (Seg b₁) & a₃ = b₂ ^ a₂ );
existence

proof end;

uniqueness ;
consistency ;

end;

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

E2: now

let c₁ be FinSequence;
let c₂ be Nat;
assume c₂ in dom c₁ ;
then c₂ in Seg (len c₁) by FINSEQ_1:def 3;
hence ( c₂ <= len c₁ & c₂ >= 0 + 1 ) by FINSEQ_1:3;
hence c₂ > 0 ;

end;

E3: now

let c₁ be FinSequence;
let c₂ be Nat;
assume c₂ + 1 in dom c₁ ;
then c₂ + 1 <= len c₁ by Lemma2;
hence c₂ < len c₁ by NAT_1:38;

end;

E4: now

let c₁ be FinSequence;
let c₂ be Nat;
assume ( ( c₂ <= len c₁ or c₂ < len c₁ ) & ( c₂ >= 1 or c₂ > 0 ) ) ;
then ( c₂ <= len c₁ & c₂ >= 0 + 1 ) by NAT_1:38;
then c₂ in Seg (len c₁) by FINSEQ_1:3;
hence c₂ in dom c₁ by FINSEQ_1:def 3;

end;

E5: now

let c₁ be FinSequence;
let c₂ be Nat;
assume c₂ < len c₁ ;
then ( c₂ + 1 <= len c₁ & c₂ + 1 >= 1 ) by NAT_1:29, NAT_1:38;
hence c₂ + 1 in dom c₁ by Lemma4;

end;

theorem Th1: :: REWRITE1:1

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

proof end;

theorem Th2: :: REWRITE1:2

for b₁, b₂ being FinSequence
for b₃ being set st b₁ <> {} holds
(b₂ ^ <*b₃*>) $^ b₁ = b₂ ^ b₁

proof end;

theorem Th3: :: REWRITE1:3

for b₁, b₂ being FinSequence
for b₃, b₄ being set holds (b₁ ^ <*b₃*>) $^ (<*b₄*> ^ b₂) = (b₁ ^ <*b₄*>) ^ b₂

proof end;

theorem Th4: :: REWRITE1:4

for b₁ being FinSequence
for b₂ being set st b₁ <> {} holds
<*b₂*> $^ b₁ = b₁

proof end;

theorem Th5: :: REWRITE1:5

for b₁ being FinSequence st b₁ <> {} holds
ex b₂ being set ex b₃ being FinSequence st
( b₁ = <*b₂*> ^ b₃ & len b₁ = (len b₃) + 1 )

proof end;

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

for b₁ being Nat st b₁ in dom (F₁() $^ F₂()) & b₁ + 1 in dom (F₁() $^ F₂()) holds
for b₂, b₃ being set st b₂ = (F₁() $^ F₂()) . b₁ & b₃ = (F₁() $^ F₂()) . (b₁ + 1) holds
P₁[b₂,b₃]

provided

E7: for b₁ being Nat st b₁ in dom F₁() & b₁ + 1 in dom F₁() holds
P₁[F₁() . b₁,F₁() . (b₁ + 1)] and
E8: for b₁ being Nat st b₁ in dom F₂() & b₁ + 1 in dom F₂() holds
P₁[F₂() . b₁,F₂() . (b₁ + 1)] and
E9: ( len F₁() > 0 & len F₂() > 0 & F₁() . (len F₁()) = F₂() . 1 )

proof end;

definition

let c₁ be Relation;
mode RedSequence of c₁ -> FinSequence means :Def2: :: REWRITE1:def 2
( len a₂ > 0 & ( for b₁ being Nat st b₁ in dom a₂ & b₁ + 1 in dom a₂ holds
[(a₂ . b₁),(a₂ . (b₁ + 1))] in a₁ ) );
existence

proof end;

end;

:: deftheorem Def2 defines RedSequence REWRITE1:def 2 :

registration

let c₁ be Relation;
cluster -> non empty RedSequence of a₁;
coherence

proof end;

end;

theorem Th6: :: REWRITE1:6

canceled;

theorem Th7: :: REWRITE1:7

for b₁ being Relation
for b₂ being set holds <*b₂*> is RedSequence of b₁

proof end;

theorem Th8: :: REWRITE1:8

for b₁ being Relation
for b₂, b₃ being set st [b₂,b₃] in b₁ holds
<*b₂,b₃*> is RedSequence of b₁

proof end;

theorem Th9: :: REWRITE1:9

for b₁ being Relation
for b₂, b₃ being RedSequence of b₁ st b₂ . (len b₂) = b₃ . 1 holds
b₂ $^ b₃ is RedSequence of b₁

proof end;

theorem Th10: :: REWRITE1:10

for b₁ being Relation
for b₂ being RedSequence of b₁ holds Rev b₂ is RedSequence of b₁ ~

proof end;

theorem Th11: :: REWRITE1:11

for b₁, b₂ being Relation st b₁ c= b₂ holds
for b₃ being RedSequence of b₁ holds b₃ is RedSequence of b₂

proof end;

definition

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

end;

:: deftheorem Def3 defines reduces REWRITE1:def 3 :

definition

let c₁ be Relation;
let c₂, c₃ be set ;
pred c₂,c₃ are_convertible_wrt c₁ means :Def4: :: REWRITE1:def 4
a₁ \/ (a₁ ~ ) reduces a₂,a₃;

end;

:: deftheorem Def4 defines are_convertible_wrt REWRITE1:def 4 :

theorem Th12: :: REWRITE1:12

for b₁ being Relation
for b₂, b₃ being set holds
( b₁ reduces b₂,b₃ iff ex b₄ being FinSequence st
( len b₄ > 0 & b₄ . 1 = b₂ & b₄ . (len b₄) = b₃ & ( for b₅ being Nat st b₅ in dom b₄ & b₅ + 1 in dom b₄ holds
[(b₄ . b₅),(b₄ . (b₅ + 1))] in b₁ ) ) )

proof end;

theorem Th13: :: REWRITE1:13

for b₁ being Relation
for b₂ being set holds b₁ reduces b₂,b₂

proof end;

theorem Th14: :: REWRITE1:14

for b₁, b₂ being set st {} reduces b₁,b₂ holds
b₁ = b₂

proof end;

theorem Th15: :: REWRITE1:15

for b₁ being Relation
for b₂, b₃ being set st b₁ reduces b₂,b₃ & not b₂ in field b₁ holds
b₂ = b₃

proof end;

theorem Th16: :: REWRITE1:16

for b₁ being Relation
for b₂, b₃ being set st [b₂,b₃] in b₁ holds
b₁ reduces b₂,b₃

proof end;

theorem Th17: :: REWRITE1:17

for b₁ being Relation
for b₂, b₃, b₄ being set st b₁ reduces b₂,b₃ & b₁ reduces b₃,b₄ holds
b₁ reduces b₂,b₄

proof end;

theorem Th18: :: REWRITE1:18

for b₁ being Relation
for b₂ being RedSequence of b₁
for b₃, b₄ being Nat st b₃ in dom b₂ & b₄ in dom b₂ & b₃ <= b₄ holds
b₁ reduces b₂ . b₃,b₂ . b₄

proof end;

theorem Th19: :: REWRITE1:19

for b₁ being Relation
for b₂, b₃ being set st b₁ reduces b₂,b₃ & b₂ <> b₃ holds
( b₂ in field b₁ & b₃ in field b₁ )

proof end;

theorem Th20: :: REWRITE1:20

for b₁ being Relation
for b₂, b₃ being set st b₁ reduces b₂,b₃ holds
( b₂ in field b₁ iff b₃ in field b₁ ) by Th19;

theorem Th21: :: REWRITE1:21

for b₁ being Relation
for b₂, b₃ being set holds
( b₁ reduces b₂,b₃ iff ( b₂ = b₃ or [b₂,b₃] in b₁ [*] ) )

proof end;

theorem Th22: :: REWRITE1:22

for b₁ being Relation
for b₂, b₃ being set holds
( b₁ reduces b₂,b₃ iff b₁ [*] reduces b₂,b₃ )

proof end;

theorem Th23: :: REWRITE1:23

for b₁, b₂ being Relation st b₁ c= b₂ holds
for b₃, b₄ being set st b₁ reduces b₃,b₄ holds
b₂ reduces b₃,b₄

proof end;

theorem Th24: :: REWRITE1:24

for b₁ being Relation
for b₂, b₃, b₄ being set holds
( b₁ reduces b₃,b₄ iff b₁ \/ (id b₂) reduces b₃,b₄ )

proof end;

theorem Th25: :: REWRITE1:25

for b₁ being Relation
for b₂, b₃ being set st b₁ reduces b₂,b₃ holds
b₁ ~ reduces b₃,b₂

proof end;

Lemma28: for b₁ being Relation
for b₂, b₃ being set st b₂,b₃ are_convertible_wrt b₁ holds
b₃,b₂ are_convertible_wrt b₁

proof end;

theorem Th26: :: REWRITE1:26

for b₁ being Relation
for b₂, b₃ being set st b₁ reduces b₂,b₃ holds
( b₂,b₃ are_convertible_wrt b₁ & b₃,b₂ are_convertible_wrt b₁ )

proof end;

theorem Th27: :: REWRITE1:27

for b₁ being Relation
for b₂ being set holds b₂,b₂ are_convertible_wrt b₁

proof end;

theorem Th28: :: REWRITE1:28

for b₁, b₂ being set st b₁,b₂ are_convertible_wrt {} holds
b₁ = b₂

proof end;

theorem Th29: :: REWRITE1:29

for b₁ being Relation
for b₂, b₃ being set st b₂,b₃ are_convertible_wrt b₁ & not b₂ in field b₁ holds
b₂ = b₃

proof end;

theorem Th30: :: REWRITE1:30

for b₁ being Relation
for b₂, b₃ being set st [b₂,b₃] in b₁ holds
b₂,b₃ are_convertible_wrt b₁

proof end;

theorem Th31: :: REWRITE1:31

for b₁ being Relation
for b₂, b₃, b₄ being set st b₂,b₃ are_convertible_wrt b₁ & b₃,b₄ are_convertible_wrt b₁ holds
b₂,b₄ are_convertible_wrt b₁

proof end;

theorem Th32: :: REWRITE1:32

for b₁ being Relation
for b₂, b₃ being set st b₂,b₃ are_convertible_wrt b₁ holds
b₃,b₂ are_convertible_wrt b₁ by Lemma28;

theorem Th33: :: REWRITE1:33

for b₁ being Relation
for b₂, b₃ being set st b₂,b₃ are_convertible_wrt b₁ & b₂ <> b₃ holds
( b₂ in field b₁ & b₃ in field b₁ )

proof end;

definition

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

end;

:: deftheorem Def5 defines is_a_normal_form_wrt REWRITE1:def 5 :

theorem Th34: :: REWRITE1:34

for b₁ being Relation
for b₂, b₃ being set st b₂ is_a_normal_form_wrt b₁ & b₁ reduces b₂,b₃ holds
b₂ = b₃

proof end;

theorem Th35: :: REWRITE1:35

for b₁ being Relation
for b₂ being set st not b₂ in field b₁ holds
b₂ is_a_normal_form_wrt b₁

proof end;

definition

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

end;

:: deftheorem Def6 defines is_a_normal_form_of REWRITE1:def 6 :

:: deftheorem Def7 defines are_convergent_wrt REWRITE1:def 7 :

:: deftheorem Def8 defines are_divergent_wrt REWRITE1:def 8 :

:: deftheorem Def9 defines are_convergent<=1_wrt REWRITE1:def 9 :

:: deftheorem Def10 defines are_divergent<=1_wrt REWRITE1:def 10 :

theorem Th36: :: REWRITE1:36

for b₁ being Relation
for b₂ being set st not b₂ in field b₁ holds
b₂ is_a_normal_form_of b₂,b₁

proof end;

theorem Th37: :: REWRITE1:37

for b₁ being Relation
for b₂, b₃ being set st b₁ reduces b₂,b₃ holds
( b₂,b₃ are_convergent_wrt b₁ & b₂,b₃ are_divergent_wrt b₁ & b₃,b₂ are_convergent_wrt b₁ & b₃,b₂ are_divergent_wrt b₁ )

proof end;

theorem Th38: :: REWRITE1:38

for b₁ being Relation
for b₂, b₃ being set st ( b₂,b₃ are_convergent_wrt b₁ or b₂,b₃ are_divergent_wrt b₁ ) holds
b₂,b₃ are_convertible_wrt b₁

proof end;

theorem Th39: :: REWRITE1:39

for b₁ being Relation
for b₂ being set holds
( b₂,b₂ are_convergent_wrt b₁ & b₂,b₂ are_divergent_wrt b₁ )

proof end;

theorem Th40: :: REWRITE1:40

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

proof end;

theorem Th41: :: REWRITE1:41

for b₁ being Relation
for b₂, b₃ being set st b₂,b₃ are_convergent_wrt b₁ holds
b₃,b₂ are_convergent_wrt b₁

proof end;

theorem Th42: :: REWRITE1:42

for b₁ being Relation
for b₂, b₃ being set st b₂,b₃ are_divergent_wrt b₁ holds
b₃,b₂ are_divergent_wrt b₁

proof end;

theorem Th43: :: REWRITE1:43

for b₁ being Relation
for b₂, b₃, b₄ being set st ( ( b₁ reduces b₂,b₃ & b₃,b₄ are_convergent_wrt b₁ ) or ( b₂,b₃ are_convergent_wrt b₁ & b₁ reduces b₄,b₃ ) ) holds
b₂,b₄ are_convergent_wrt b₁

proof end;

theorem Th44: :: REWRITE1:44

for b₁ being Relation
for b₂, b₃, b₄ being set st ( ( b₁ reduces b₃,b₂ & b₃,b₄ are_divergent_wrt b₁ ) or ( b₂,b₃ are_divergent_wrt b₁ & b₁ reduces b₃,b₄ ) ) holds
b₂,b₄ are_divergent_wrt b₁

proof end;

theorem Th45: :: REWRITE1:45

for b₁ being Relation
for b₂, b₃ being set st b₂,b₃ are_convergent<=1_wrt b₁ holds
b₂,b₃ are_convergent_wrt b₁

proof end;

theorem Th46: :: REWRITE1:46

for b₁ being Relation
for b₂, b₃ being set st b₂,b₃ are_divergent<=1_wrt b₁ holds
b₂,b₃ are_divergent_wrt b₁

proof end;

definition

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

end;

:: deftheorem Def11 defines has_a_normal_form_wrt REWRITE1:def 11 :

theorem Th47: :: REWRITE1:47

for b₁ being Relation
for b₂ being set st not b₂ in field b₁ holds
b₂ has_a_normal_form_wrt b₁

proof end;

definition

let c₁ be Relation;
let c₂ be set ;
assume that
E52: c₂ has_a_normal_form_wrt c₁ and
E53: for b₁, b₂ being set st b₁ is_a_normal_form_of c₂,c₁ & b₂ is_a_normal_form_of c₂,c₁ holds
b₁ = b₂ ;
func nf c₂,c₁ -> set means :Def12: :: REWRITE1:def 12
a₃ is_a_normal_form_of a₂,a₁;
existence by E52, Def11;
uniqueness by E53;

end;

:: deftheorem Def12 defines nf REWRITE1:def 12 :

definition

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

end;

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

:: deftheorem Def14 defines weakly-normalizing REWRITE1:def 14 :

:: deftheorem Def15 defines strongly-normalizing REWRITE1:def 15 :

definition

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

proof end;

end;

:: deftheorem Def16 defines co-well_founded REWRITE1:def 16 :

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

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

provided

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

proof end;

registration

cluster strongly-normalizing -> irreflexive co-well_founded set ;
coherence

proof end;

cluster irreflexive co-well_founded -> strongly-normalizing set ;
coherence

proof end;

end;

registration

cluster empty -> irreflexive co-well_founded weakly-normalizing strongly-normalizing set ;
coherence

proof end;

end;

registration

cluster empty irreflexive co-well_founded weakly-normalizing strongly-normalizing set ;
existence

proof end;

end;

theorem Th48: :: REWRITE1:48

for b₁ being co-well_founded Relation
for b₂ being Relation st b₂ c= b₁ holds
b₂ is co-well_founded

proof end;

registration

cluster strongly-normalizing -> weakly-normalizing set ;
coherence

proof end;

end;

definition

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

proof end;

pred c₁ commutes_with c₂ means :Def18: :: REWRITE1:def 18
for b₁, b₂, b₃ being set st a₁ reduces b₁,b₂ & a₂ reduces b₁,b₃ holds
ex b₄ being set st
( a₂ reduces b₂,b₄ & a₁ reduces b₃,b₄ );
symmetry

proof end;

end;

:: deftheorem Def17 defines commutes-weakly_with REWRITE1:def 17 :

:: deftheorem Def18 defines commutes_with REWRITE1:def 18 :

theorem Th49: :: REWRITE1:49

for b₁, b₂ being Relation st b₁ commutes_with b₂ holds
b₁ commutes-weakly_with b₂

proof end;

definition

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

end;

:: deftheorem Def19 defines with_UN_property REWRITE1:def 19 :

:: deftheorem Def20 defines with_NF_property REWRITE1:def 20 :

:: deftheorem Def21 defines subcommutative REWRITE1:def 21 :

:: deftheorem Def22 defines confluent REWRITE1:def 22 :

:: deftheorem Def23 defines with_Church-Rosser_property REWRITE1:def 23 :

:: deftheorem Def24 defines locally-confluent REWRITE1:def 24 :

notation

let c₁ be Relation;
synonym c₁ has_diamond_property for subcommutative c₁;
synonym c₁ has_Church-Rosser_property for with_Church-Rosser_property c₁;
synonym c₁ has_weak-Church-Rosser_property for locally-confluent c₁;

end;

theorem Th50: :: REWRITE1:50

for b₁ being Relation st b₁ is subcommutative holds
for b₂, b₃, b₄ being set st b₁ reduces b₂,b₃ & [b₂,b₄] in b₁ holds
b₃,b₄ are_convergent_wrt b₁

proof end;

theorem Th51: :: REWRITE1:51

for b₁ being Relation holds
( b₁ is confluent iff b₁ commutes_with b₁ )

proof end;

theorem Th52: :: REWRITE1:52

for b₁ being Relation holds
( b₁ is confluent iff for b₂, b₃, b₄ being set st b₁ reduces b₂,b₃ & [b₂,b₄] in b₁ holds
b₃,b₄ are_convergent_wrt b₁ )

proof end;

theorem Th53: :: REWRITE1:53

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

proof end;

registration

cluster with_Church-Rosser_property -> confluent set ;
coherence

proof end;

cluster confluent -> with_Church-Rosser_property locally-confluent set ;
coherence

proof end;

cluster subcommutative -> confluent set ;
coherence

proof end;

cluster with_Church-Rosser_property -> with_NF_property set ;
coherence

proof end;

cluster with_NF_property -> with_UN_property set ;
coherence

proof end;

cluster weakly-normalizing with_UN_property -> with_Church-Rosser_property set ;
coherence

proof end;

end;

registration

cluster empty -> with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent set ;
coherence

proof end;

end;

registration

cluster empty irreflexive co-well_founded weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent set ;
existence

proof end;

end;

theorem Th54: :: REWRITE1:54

for b₁ being with_UN_property Relation
for b₂, b₃, b₄ being set st b₃ is_a_normal_form_of b₂,b₁ & b₄ is_a_normal_form_of b₂,b₁ holds
b₃ = b₄

proof end;

theorem Th55: :: REWRITE1:55

for b₁ being weakly-normalizing with_UN_property Relation
for b₂ being set holds nf b₂,b₁ is_a_normal_form_of b₂,b₁

proof end;

theorem Th56: :: REWRITE1:56

for b₁ being weakly-normalizing with_UN_property Relation
for b₂, b₃ being set st b₂,b₃ are_convertible_wrt b₁ holds
nf b₂,b₁ = nf b₃,b₁

proof end;

registration

cluster strongly-normalizing locally-confluent -> with_UN_property with_NF_property confluent with_Church-Rosser_property locally-confluent set ;
coherence

proof end;

end;

definition

let c₁ be Relation;
attr a₁ is complete means :: REWRITE1:def 25
( a₁ is confluent & a₁ is strongly-normalizing );

end;

:: deftheorem Def25 defines complete REWRITE1:def 25 :

registration

cluster complete -> irreflexive co-well_founded weakly-normalizing strongly-normalizing with_UN_property with_NF_property confluent with_Church-Rosser_property locally-confluent set ;
coherence

proof end;

cluster strongly-normalizing confluent -> complete set ;
coherence

proof end;

end;

registration

proof end;

end;

registration

cluster non empty irreflexive co-well_founded weakly-normalizing strongly-normalizing with_UN_property with_NF_property confluent with_Church-Rosser_property locally-confluent complete set ;
existence

proof end;

end;

theorem Th57: :: REWRITE1:57

for b₁, b₂ being with_Church-Rosser_property Relation st b₁ commutes_with b₂ holds
b₁ \/ b₂ has_Church-Rosser_property

proof end;

theorem Th58: :: REWRITE1:58

for b₁ being Relation holds
( b₁ is confluent iff b₁ [*] has_weak-Church-Rosser_property )

proof end;

theorem Th59: :: REWRITE1:59

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

proof end;

definition

let c₁, c₂ be Relation;
pred c₁,c₂ are_equivalent means :: REWRITE1:def 26
for b₁, b₂ being set holds
( b₁,b₂ are_convertible_wrt a₁ iff b₁,b₂ are_convertible_wrt a₂ );
symmetry ;

end;

:: deftheorem Def26 defines are_equivalent REWRITE1:def 26 :

definition

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

end;

:: deftheorem Def27 defines are_critical_wrt REWRITE1:def 27 :

theorem Th60: :: REWRITE1:60

for b₁ being Relation
for b₂, b₃ being set st b₂,b₃ are_critical_wrt b₁ holds
b₂,b₃ are_convertible_wrt b₁

proof end;

theorem Th61: :: REWRITE1:61

for b₁ being Relation st ( for b₂, b₃ being set holds not b₂,b₃ are_critical_wrt b₁ ) holds
b₁ is locally-confluent

proof end;

theorem Th62: :: REWRITE1:62

for b₁, b₂ being Relation st ( for b₃, b₄ being set st [b₃,b₄] in b₂ holds
b₃,b₄ are_critical_wrt b₁ ) holds
b₁,b₁ \/ b₂ are_equivalent

proof end;

theorem Th63: :: REWRITE1:63

for b₁ being Relation ex b₂ being complete Relation st
( field b₂ c= field b₁ & ( for b₃, b₄ being set holds
( b₃,b₄ are_convertible_wrt b₁ iff b₃,b₄ are_convergent_wrt b₂ ) ) )

proof end;

definition

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

proof end;

end;

:: deftheorem Def28 defines Completion REWRITE1:def 28 :

theorem Th64: :: REWRITE1:64

for b₁ being Relation
for b₂ being Completion of b₁ holds b₁,b₂ are_equivalent

proof end;

theorem Th65: :: REWRITE1:65

for b₁ being Relation
for b₂ being complete Relation st b₁,b₂ are_equivalent holds
b₂ is Completion of b₁

proof end;

theorem Th66: :: REWRITE1:66

for b₁ being Relation
for b₂ being Completion of b₁
for b₃, b₄ being set holds
( b₃,b₄ are_convertible_wrt b₁ iff nf b₃,b₂ = nf b₄,b₂ )

proof end;