let T be non empty reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured commutative TAS-structure ; ( T @--> is with_Church-Rosser_property & T @--> is with_UN_property )
set R = T @--> ;
T @--> is locally-confluent
proof
let a,
b,
c be
object ;
REWRITE1:def 24 ( not [a,b] in T @--> or not [a,c] in T @--> or b,c are_convergent_wrt T @--> )
assume that A1:
[a,b] in T @-->
and A2:
[a,c] in T @-->
;
b,c are_convergent_wrt T @-->
reconsider t =
a,
t1 =
b,
t2 =
c as
type of
T by A1, A2, ZFMISC_1:87;
consider a2 being
adjective of
T such that
not
a2 in adjs t1
and A3:
a2 is_properly_applicable_to t1
and A4:
a2 ast t1 = t
by A1, Def31;
set tt =
t1 "\/" t2;
take
t1 "\/" t2
;
REWRITE1:def 7 ( T @--> reduces b,t1 "\/" t2 & T @--> reduces c,t1 "\/" t2 )
consider a3 being
adjective of
T such that
not
a3 in adjs t2
and A5:
a3 is_properly_applicable_to t2
and A6:
a3 ast t2 = t
by A2, Def31;
a3 is_applicable_to t2
by A5;
then
t <= t2
by A6, Th20;
then A7:
ex
B being
finite Subset of the
adjectives of
T st
(
B is_properly_applicable_to t1 "\/" t2 &
B ast (t1 "\/" t2) = t2 )
by A3, A4, Def30;
a2 is_applicable_to t1
by A3;
then
t <= t1
by A4, Th20;
then
ex
A being
finite Subset of the
adjectives of
T st
(
A is_properly_applicable_to t1 "\/" t2 &
A ast (t1 "\/" t2) = t1 )
by A5, A6, Def30;
hence
(
T @--> reduces b,
t1 "\/" t2 &
T @--> reduces c,
t1 "\/" t2 )
by A7, Th72;
verum
end;
then
T @--> is strongly-normalizing locally-confluent Relation
by Th69;
hence
( T @--> is with_Church-Rosser_property & T @--> is with_UN_property )
; verum