:: Reduction Relations
:: by Grzegorz Bancerek
::
:: Received November 14, 1995
:: Copyright (c) 1995 Association of Mizar Users
:: deftheorem Def1 defines $^ REWRITE1:def 1 :
theorem :: REWRITE1:1
theorem Th2: :: REWRITE1:2
theorem :: REWRITE1:3
theorem :: REWRITE1:4
theorem :: REWRITE1:5
:: deftheorem Def2 defines RedSequence REWRITE1:def 2 :
theorem :: REWRITE1:6
canceled;
theorem Th7: :: REWRITE1:7
theorem Th8: :: REWRITE1:8
theorem Th9: :: REWRITE1:9
theorem Th10: :: REWRITE1:10
theorem Th11: :: REWRITE1:11
:: deftheorem Def3 defines reduces REWRITE1:def 3 :
:: deftheorem Def4 defines are_convertible_wrt REWRITE1:def 4 :
theorem Th12: :: REWRITE1:12
theorem Th13: :: REWRITE1:13
theorem Th14: :: REWRITE1:14
theorem Th15: :: REWRITE1:15
theorem Th16: :: REWRITE1:16
theorem Th17: :: REWRITE1:17
theorem Th18: :: REWRITE1:18
theorem Th19: :: REWRITE1:19
theorem :: REWRITE1:20
theorem Th21: :: REWRITE1:21
theorem Th22: :: REWRITE1:22
theorem Th23: :: REWRITE1:23
theorem :: REWRITE1:24
theorem Th25: :: REWRITE1:25
Lm5:
for R being Relation
for a, b being set st a,b are_convertible_wrt R holds
b,a are_convertible_wrt R
theorem Th26: :: REWRITE1:26
theorem Th27: :: REWRITE1:27
theorem Th28: :: REWRITE1:28
theorem :: REWRITE1:29
theorem Th30: :: REWRITE1:30
theorem Th31: :: REWRITE1:31
theorem :: REWRITE1:32
theorem Th33: :: REWRITE1:33
:: deftheorem defines is_a_normal_form_wrt REWRITE1:def 5 :
theorem Th34: :: REWRITE1:34
theorem Th35: :: REWRITE1:35
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 :
:: 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
theorem Th37: :: REWRITE1:37
theorem Th38: :: REWRITE1:38
theorem Th39: :: REWRITE1:39
theorem Th40: :: REWRITE1:40
theorem :: REWRITE1:41
theorem :: REWRITE1:42
theorem Th43: :: REWRITE1:43
theorem :: REWRITE1:44
theorem Th45: :: REWRITE1:45
theorem Th46: :: REWRITE1:46
:: deftheorem Def11 defines has_a_normal_form_wrt REWRITE1:def 11 :
theorem Th47: :: REWRITE1:47
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 b1 being set st b1 is_a_normal_form_of a,R
by A1, Def11;
uniqueness
for b1, b2 being set st b1 is_a_normal_form_of a,R & b2 is_a_normal_form_of a,R holds
b1 = b2
by A2;
end;
:: deftheorem Def12 defines nf REWRITE1:def 12 :
:: deftheorem Def13 defines co-well_founded REWRITE1:def 13 :
:: deftheorem Def14 defines weakly-normalizing REWRITE1:def 14 :
:: deftheorem defines strongly-normalizing REWRITE1:def 15 :
:: deftheorem Def16 defines co-well_founded REWRITE1:def 16 :
theorem :: REWRITE1:48
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 )
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 )
end;
:: deftheorem defines commutes-weakly_with REWRITE1:def 17 :
:: deftheorem Def18 defines commutes_with REWRITE1:def 18 :
theorem :: REWRITE1:49
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 :
:: deftheorem 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 :
theorem Th50: :: REWRITE1:50
theorem :: REWRITE1:51
theorem Th52: :: REWRITE1:52
theorem :: REWRITE1:53
theorem Th54: :: REWRITE1:54
theorem Th55: :: REWRITE1:55
theorem Th56: :: REWRITE1:56
:: deftheorem defines complete REWRITE1:def 25 :
theorem :: REWRITE1:57
theorem :: REWRITE1:58
theorem :: REWRITE1:59
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 :
:: deftheorem Def27 defines are_critical_wrt REWRITE1:def 27 :
theorem Th60: :: REWRITE1:60
theorem :: REWRITE1:61
theorem :: REWRITE1:62
theorem Th63: :: REWRITE1:63
:: deftheorem Def28 defines Completion REWRITE1:def 28 :
theorem :: REWRITE1:64
theorem :: REWRITE1:65
theorem :: REWRITE1:66