:: Abstract Reduction Systems and Idea of {K}nuth {B}endix Completion Algorithm
:: by Grzegorz Bancerek
::
:: Copyright (c) 2014-2021 Association of Mizar Users

definition
attr c1 is strict ;
struct ARS -> 1-sorted ;
aggr ARS(# carrier, reduction #) -> ARS ;
sel reduction c1 -> Relation of the carrier of c1;
end;

registration
let A be non empty set ;
let r be Relation of A;
cluster ARS(# A,r #) -> non empty ;
coherence
not ARS(# A,r #) is empty
;
end;

registration
cluster non empty strict for ARS ;
existence
ex b1 being ARS st
( not b1 is empty & b1 is strict )
proof end;
end;

definition
let X be ARS ;
let x, y be Element of X;
pred x ==> y means :: ABSRED_0:def 1
[x,y] in the reduction of X;
end;

:: deftheorem defines ==> ABSRED_0:def 1 :
for X being ARS
for x, y being Element of X holds
( x ==> y iff [x,y] in the reduction of X );

notation
let X be ARS ;
let x, y be Element of X;
synonym y <== x for x ==> y;
end;

definition
let X be ARS ;
let x, y be Element of X;
pred x =01=> y means :: ABSRED_0:def 2
( x = y or x ==> y );
reflexivity
for x being Element of X holds
( x = x or x ==> x )
;
pred x =*=> y means :: ABSRED_0:def 3
the reduction of X reduces x,y;
reflexivity
for x being Element of X holds the reduction of X reduces x,x
by REWRITE1:12;
end;

:: deftheorem defines =01=> ABSRED_0:def 2 :
for X being ARS
for x, y being Element of X holds
( x =01=> y iff ( x = y or x ==> y ) );

:: deftheorem defines =*=> ABSRED_0:def 3 :
for X being ARS
for x, y being Element of X holds
( x =*=> y iff the reduction of X reduces x,y );

theorem :: ABSRED_0:1
for X being ARS
for a, b being Element of X st a ==> b holds
not X is empty ;

theorem Th2: :: ABSRED_0:2
for X being ARS
for x, y being Element of X st x ==> y holds
x =*=> y by REWRITE1:15;

theorem Th3: :: ABSRED_0:3
for X being ARS
for x, y, z being Element of X st x =*=> y & y =*=> z holds
x =*=> z by REWRITE1:16;

scheme :: ABSRED_0:sch 1
Star{ F1() -> ARS , P1[ object ] } :
for x, y being Element of F1() st x =*=> y & P1[x] holds
P1[y]
provided
A1: for x, y being Element of F1() st x ==> y & P1[x] holds
P1[y]
proof end;

scheme :: ABSRED_0:sch 2
Star1{ F1() -> ARS , P1[ object ], F2() -> Element of F1(), F3() -> Element of F1() } :
P1[F3()]
provided
A1: F2() =*=> F3() and
A2: P1[F2()] and
A3: for x, y being Element of F1() st x ==> y & P1[x] holds
P1[y]
proof end;

scheme :: ABSRED_0:sch 3
StarBack{ F1() -> ARS , P1[ object ] } :
for x, y being Element of F1() st x =*=> y & P1[y] holds
P1[x]
provided
A1: for x, y being Element of F1() st x ==> y & P1[y] holds
P1[x]
proof end;

scheme :: ABSRED_0:sch 4
StarBack1{ F1() -> ARS , P1[ object ], F2() -> Element of F1(), F3() -> Element of F1() } :
P1[F2()]
provided
A1: F2() =*=> F3() and
A2: P1[F3()] and
A3: for x, y being Element of F1() st x ==> y & P1[y] holds
P1[x]
proof end;

definition
let X be ARS ;
let x, y be Element of X;
pred x =+=> y means :: ABSRED_0:def 4
ex z being Element of X st
( x ==> z & z =*=> y );
end;

:: deftheorem defines =+=> ABSRED_0:def 4 :
for X being ARS
for x, y being Element of X holds
( x =+=> y iff ex z being Element of X st
( x ==> z & z =*=> y ) );

theorem Th4: :: ABSRED_0:4
for X being ARS
for x, y being Element of X holds
( x =+=> y iff ex z being Element of X st
( x =*=> z & z ==> y ) )
proof end;

notation
let X be ARS ;
let x, y be Element of X;
synonym y <=01= x for x =01=> y;
synonym y <=*= x for x =*=> y;
synonym y <=+= x for x =+=> y;
end;

:: x ==> y implies x =+=> y;
:: x =+=> y implies x =*=> y;
:: x =+=> y & y =*=> z implies x =+=> z;
:: x =*=> y & y =+=> z implies x =+=> z;
definition
let X be ARS ;
let x, y be Element of X;
pred x <==> y means :: ABSRED_0:def 5
( x ==> y or x <== y );
symmetry
for x, y being Element of X holds
( ( not x ==> y & not x <== y ) or y ==> x or y <== x )
;
end;

:: deftheorem defines <==> ABSRED_0:def 5 :
for X being ARS
for x, y being Element of X holds
( x <==> y iff ( x ==> y or x <== y ) );

theorem :: ABSRED_0:5
for X being ARS
for x, y being Element of X holds
( x <==> y iff [x,y] in the reduction of X \/ ( the reduction of X ~) )
proof end;

definition
let X be ARS ;
let x, y be Element of X;
pred x <=01=> y means :: ABSRED_0:def 6
( x = y or x <==> y );
reflexivity
for x being Element of X holds
( x = x or x <==> x )
;
symmetry
for x, y being Element of X holds
( ( not x = y & not x <==> y ) or y = x or y <==> x )
;
pred x <=*=> y means :: ABSRED_0:def 7
x,y are_convertible_wrt the reduction of X;
reflexivity
for x being Element of X holds x,x are_convertible_wrt the reduction of X
by REWRITE1:26;
symmetry
for x, y being Element of X st x,y are_convertible_wrt the reduction of X holds
y,x are_convertible_wrt the reduction of X
by REWRITE1:31;
end;

:: deftheorem defines <=01=> ABSRED_0:def 6 :
for X being ARS
for x, y being Element of X holds
( x <=01=> y iff ( x = y or x <==> y ) );

:: deftheorem defines <=*=> ABSRED_0:def 7 :
for X being ARS
for x, y being Element of X holds
( x <=*=> y iff x,y are_convertible_wrt the reduction of X );

theorem Th6: :: ABSRED_0:6
for X being ARS
for x, y being Element of X st x <==> y holds
x <=*=> y
proof end;

theorem Th7: :: ABSRED_0:7
for X being ARS
for x, y, z being Element of X st x <=*=> y & y <=*=> z holds
x <=*=> z by REWRITE1:30;

scheme :: ABSRED_0:sch 5
Star2{ F1() -> ARS , P1[ object ] } :
for x, y being Element of F1() st x <=*=> y & P1[x] holds
P1[y]
provided
A1: for x, y being Element of F1() st x <==> y & P1[x] holds
P1[y]
proof end;

scheme :: ABSRED_0:sch 6
Star2A{ F1() -> ARS , P1[ object ], F2() -> Element of F1(), F3() -> Element of F1() } :
P1[F3()]
provided
A1: F2() <=*=> F3() and
A2: P1[F2()] and
A3: for x, y being Element of F1() st x <==> y & P1[x] holds
P1[y]
proof end;

definition
let X be ARS ;
let x, y be Element of X;
pred x <=+=> y means :Def8: :: ABSRED_0:def 8
ex z being Element of X st
( x <==> z & z <=*=> y );
symmetry
for x, y being Element of X st ex z being Element of X st
( x <==> z & z <=*=> y ) holds
ex z being Element of X st
( y <==> z & z <=*=> x )
proof end;
end;

:: deftheorem Def8 defines <=+=> ABSRED_0:def 8 :
for X being ARS
for x, y being Element of X holds
( x <=+=> y iff ex z being Element of X st
( x <==> z & z <=*=> y ) );

theorem Th8: :: ABSRED_0:8
for X being ARS
for x, y being Element of X holds
( x <=+=> y iff ex z being Element of X st
( x <=*=> z & z <==> y ) )
proof end;

theorem Lem1: :: ABSRED_0:9
for X being ARS
for x, y being Element of X st x =01=> y holds
x =*=> y by Th2;

theorem Lem2: :: ABSRED_0:10
for X being ARS
for x, y being Element of X st x =+=> y holds
x =*=> y
proof end;

theorem :: ABSRED_0:11
for X being ARS
for x, y being Element of X st x ==> y holds
x =+=> y ;

theorem Lem3: :: ABSRED_0:12
for X being ARS
for x, y, z being Element of X st x ==> y & y ==> z holds
x =*=> z
proof end;

theorem Lem4: :: ABSRED_0:13
for X being ARS
for x, y, z being Element of X st x ==> y & y =01=> z holds
x =*=> z
proof end;

theorem Lem5: :: ABSRED_0:14
for X being ARS
for x, y, z being Element of X st x ==> y & y =*=> z holds
x =*=> z
proof end;

theorem Lem5A: :: ABSRED_0:15
for X being ARS
for x, y, z being Element of X st x ==> y & y =+=> z holds
x =*=> z
proof end;

theorem :: ABSRED_0:16
for X being ARS
for x, y, z being Element of X st x =01=> y & y ==> z holds
x =*=> z
proof end;

theorem :: ABSRED_0:17
for X being ARS
for x, y, z being Element of X st x =01=> y & y =01=> z holds
x =*=> z
proof end;

theorem Lem8: :: ABSRED_0:18
for X being ARS
for x, y, z being Element of X st x =01=> y & y =*=> z holds
x =*=> z
proof end;

theorem :: ABSRED_0:19
for X being ARS
for x, y, z being Element of X st x =01=> y & y =+=> z holds
x =*=> z
proof end;

theorem Lem10: :: ABSRED_0:20
for X being ARS
for x, y, z being Element of X st x =*=> y & y ==> z holds
x =*=> z
proof end;

theorem Lem11: :: ABSRED_0:21
for X being ARS
for x, y, z being Element of X st x =*=> y & y =01=> z holds
x =*=> z
proof end;

theorem Lem11A: :: ABSRED_0:22
for X being ARS
for x, y, z being Element of X st x =*=> y & y =+=> z holds
x =*=> z
proof end;

theorem :: ABSRED_0:23
for X being ARS
for x, y, z being Element of X st x =+=> y & y ==> z holds
x =*=> z
proof end;

theorem :: ABSRED_0:24
for X being ARS
for x, y, z being Element of X st x =+=> y & y =01=> z holds
x =*=> z
proof end;

theorem :: ABSRED_0:25
for X being ARS
for x, y, z being Element of X st x =+=> y & y =+=> z holds
x =*=> z
proof end;

theorem :: ABSRED_0:26
for X being ARS
for x, y, z being Element of X st x ==> y & y ==> z holds
x =+=> z by Th2;

theorem :: ABSRED_0:27
for X being ARS
for x, y, z being Element of X st x ==> y & y =01=> z holds
x =+=> z by Lem1;

theorem :: ABSRED_0:28
for X being ARS
for x, y, z being Element of X st x ==> y & y =+=> z holds
x =+=> z by Lem2;

theorem :: ABSRED_0:29
for X being ARS
for x, y, z being Element of X st x =01=> y & y ==> z holds
x =+=> z by ;

theorem :: ABSRED_0:30
for X being ARS
for x, y, z being Element of X st x =01=> y & y =+=> z holds
x =+=> z
proof end;

theorem :: ABSRED_0:31
for X being ARS
for x, y, z being Element of X st x =*=> y & y =+=> z holds
x =+=> z
proof end;

theorem :: ABSRED_0:32
for X being ARS
for x, y, z being Element of X st x =+=> y & y ==> z holds
x =+=> z by Lem10;

theorem :: ABSRED_0:33
for X being ARS
for x, y, z being Element of X st x =+=> y & y =01=> z holds
x =+=> z by Lem11;

theorem :: ABSRED_0:34
for X being ARS
for x, y, z being Element of X st x =+=> y & y =*=> z holds
x =+=> z by Th3;

theorem :: ABSRED_0:35
for X being ARS
for x, y, z being Element of X st x =+=> y & y =+=> z holds
x =+=> z by Lem11A;

theorem Lem1A: :: ABSRED_0:36
for X being ARS
for x, y being Element of X st x <=01=> y holds
x <=*=> y by Th6;

theorem Lem2A: :: ABSRED_0:37
for X being ARS
for x, y being Element of X st x <=+=> y holds
x <=*=> y
proof end;

theorem LemB: :: ABSRED_0:38
for X being ARS
for x, y being Element of X st x <==> y holds
x <=+=> y ;

theorem :: ABSRED_0:39
for X being ARS
for x, y, z being Element of X st x <==> y & y <==> z holds
x <=*=> z
proof end;

theorem Lem4A: :: ABSRED_0:40
for X being ARS
for x, y, z being Element of X st x <==> y & y <=01=> z holds
x <=*=> z
proof end;

theorem :: ABSRED_0:41
for X being ARS
for x, y, z being Element of X st x <=01=> y & y <==> z holds
x <=*=> z by Lem4A;

theorem Lem5a: :: ABSRED_0:42
for X being ARS
for x, y, z being Element of X st x <==> y & y <=*=> z holds
x <=*=> z
proof end;

theorem :: ABSRED_0:43
for X being ARS
for x, y, z being Element of X st x <=*=> y & y <==> z holds
x <=*=> z by Lem5a;

theorem Lem5B: :: ABSRED_0:44
for X being ARS
for x, y, z being Element of X st x <==> y & y <=+=> z holds
x <=*=> z
proof end;

theorem :: ABSRED_0:45
for X being ARS
for x, y, z being Element of X st x <=+=> y & y <==> z holds
x <=*=> z by Lem5B;

theorem :: ABSRED_0:46
for X being ARS
for x, y, z being Element of X st x <=01=> y & y <=01=> z holds
x <=*=> z
proof end;

theorem Lm8: :: ABSRED_0:47
for X being ARS
for x, y, z being Element of X st x <=01=> y & y <=*=> z holds
x <=*=> z
proof end;

theorem :: ABSRED_0:48
for X being ARS
for x, y, z being Element of X st x <=*=> y & y <=01=> z holds
x <=*=> z by Lm8;

theorem Lem9: :: ABSRED_0:49
for X being ARS
for x, y, z being Element of X st x <=01=> y & y <=+=> z holds
x <=*=> z
proof end;

theorem :: ABSRED_0:50
for X being ARS
for x, y, z being Element of X st x <=+=> y & y <=01=> z holds
x <=*=> z by Lem9;

theorem Lem11A: :: ABSRED_0:51
for X being ARS
for x, y, z being Element of X st x <=*=> y & y <=+=> z holds
x <=*=> z
proof end;

theorem :: ABSRED_0:52
for X being ARS
for x, y, z being Element of X st x <=+=> y & y <=+=> z holds
x <=*=> z
proof end;

theorem :: ABSRED_0:53
for X being ARS
for x, y, z being Element of X st x <==> y & y <==> z holds
x <=+=> z by Th6;

theorem :: ABSRED_0:54
for X being ARS
for x, y, z being Element of X st x <==> y & y <=01=> z holds
x <=+=> z by Lem1A;

theorem :: ABSRED_0:55
for X being ARS
for x, y, z being Element of X st x <==> y & y <=+=> z holds
x <=+=> z by Lem2A;

theorem Lem18: :: ABSRED_0:56
for X being ARS
for x, y, z being Element of X st x <=01=> y & y <=+=> z holds
x <=+=> z
proof end;

theorem :: ABSRED_0:57
for X being ARS
for x, y, z being Element of X st x <=*=> y & y <=+=> z holds
x <=+=> z
proof end;

theorem :: ABSRED_0:58
for X being ARS
for x, y, z being Element of X st x <=+=> y & y <=+=> z holds
x <=+=> z by Lem11A;

theorem Lem31: :: ABSRED_0:59
for X being ARS
for x, y being Element of X holds
( not x <=01=> y or x <== y or x = y or x ==> y )
proof end;

theorem :: ABSRED_0:60
for X being ARS
for x, y being Element of X st ( x <== y or x = y or x ==> y ) holds
x <=01=> y
proof end;

theorem :: ABSRED_0:61
for X being ARS
for x, y being Element of X holds
( not x <=01=> y or x <=01= y or x ==> y )
proof end;

theorem :: ABSRED_0:62
for X being ARS
for x, y being Element of X st ( x <=01= y or x ==> y ) holds
x <=01=> y
proof end;

theorem :: ABSRED_0:63
for X being ARS
for x, y being Element of X holds
( not x <=01=> y or x <=01= y or x =+=> y )
proof end;

theorem :: ABSRED_0:64
for X being ARS
for x, y being Element of X holds
( not x <=01=> y or x <=01= y or x <==> y ) ;

theorem :: ABSRED_0:65
for X being ARS
for x, y being Element of X st ( x <=01= y or x <==> y ) holds
x <=01=> y
proof end;

theorem :: ABSRED_0:66
for X being ARS
for x, y, z being Element of X st x <=*=> y & y ==> z holds
x <=+=> z
proof end;

theorem :: ABSRED_0:67
for X being ARS
for x, y, z being Element of X st x <=+=> y & y ==> z holds
x <=+=> z
proof end;

theorem :: ABSRED_0:68
for X being ARS
for x, y being Element of X holds
( not x <=01=> y or x <=01= y or x ==> y )
proof end;

theorem :: ABSRED_0:69
for X being ARS
for x, y being Element of X holds
( not x <=01=> y or x <=01= y or x =+=> y )
proof end;

theorem Lem43: :: ABSRED_0:70
for X being ARS
for x, y being Element of X st ( x <=01= y or x ==> y ) holds
x <=01=> y
proof end;

theorem :: ABSRED_0:71
for X being ARS
for x, y being Element of X st ( x <=01= y or x <==> y ) holds
x <=01=> y
proof end;

theorem :: ABSRED_0:72
for X being ARS
for x, y being Element of X holds
( not x <=01=> y or x <=01= y or x <==> y ) ;

theorem :: ABSRED_0:73
for X being ARS
for x, y, z being Element of X st x <=+=> y & y ==> z holds
x <=+=> z
proof end;

theorem :: ABSRED_0:74
for X being ARS
for x, y, z being Element of X st x <=*=> y & y ==> z holds
x <=+=> z
proof end;

theorem :: ABSRED_0:75
for X being ARS
for x, y, z being Element of X st x <=01=> y & y ==> z holds
x <=+=> z
proof end;

theorem :: ABSRED_0:76
for X being ARS
for x, y, z being Element of X st x <=+=> y & y =01=> z holds
x <=+=> z
proof end;

theorem :: ABSRED_0:77
for X being ARS
for x, y, z being Element of X st x <==> y & y =01=> z holds
x <=+=> z
proof end;

theorem :: ABSRED_0:78
for X being ARS
for u, x, y, z being Element of X st x ==> y & y ==> z & z ==> u holds
x =+=> u by Lem3;

theorem :: ABSRED_0:79
for X being ARS
for u, x, y, z being Element of X st x ==> y & y =01=> z & z ==> u holds
x =+=> u by ;

theorem :: ABSRED_0:80
for X being ARS
for u, x, y, z being Element of X st x ==> y & y =*=> z & z ==> u holds
x =+=> u by ;

theorem :: ABSRED_0:81
for X being ARS
for u, x, y, z being Element of X st x ==> y & y =+=> z & z ==> u holds
x =+=> u
proof end;

theorem LemZ: :: ABSRED_0:82
for X being ARS
for x, y being Element of X st x =*=> y holds
x <=*=> y
proof end;

theorem :: ABSRED_0:83
for X being ARS
for z being Element of X st ( for x, y being Element of X st x ==> z & x ==> y holds
y ==> z ) holds
for x, y being Element of X st x ==> z & x =*=> y holds
y ==> z
proof end;

theorem :: ABSRED_0:84
for X being ARS st ( for x, y being Element of X st x ==> y holds
y ==> x ) holds
for x, y being Element of X st x <=*=> y holds
x =*=> y
proof end;

theorem LemN: :: ABSRED_0:85
for X being ARS
for x, y being Element of X holds
( not x =*=> y or x = y or x =+=> y )
proof end;

theorem :: ABSRED_0:86
for X being ARS st ( for x, y, z being Element of X st x ==> y & y ==> z holds
x ==> z ) holds
for x, y being Element of X st x =+=> y holds
x ==> y
proof end;

scheme :: ABSRED_0:sch 7
ARSex{ F1() -> non empty set , P1[ object , object ] } :
ex X being non empty strict ARS st
( the carrier of X = F1() & ( for x, y being Element of X holds
( x ==> y iff P1[x,y] ) ) )
proof end;

definition
func ARS_01 -> strict ARS means :Def18: :: ABSRED_0:def 9
( the carrier of it = {0,1} & the reduction of it = [:,{0,1}:] );
existence
ex b1 being strict ARS st
( the carrier of b1 = {0,1} & the reduction of b1 = [:,{0,1}:] )
proof end;
uniqueness
for b1, b2 being strict ARS st the carrier of b1 = {0,1} & the reduction of b1 = [:,{0,1}:] & the carrier of b2 = {0,1} & the reduction of b2 = [:,{0,1}:] holds
b1 = b2
;
func ARS_02 -> strict ARS means :Def19: :: ABSRED_0:def 10
( the carrier of it = {0,1,2} & the reduction of it = [:,{0,1,2}:] );
existence
ex b1 being strict ARS st
( the carrier of b1 = {0,1,2} & the reduction of b1 = [:,{0,1,2}:] )
proof end;
uniqueness
for b1, b2 being strict ARS st the carrier of b1 = {0,1,2} & the reduction of b1 = [:,{0,1,2}:] & the carrier of b2 = {0,1,2} & the reduction of b2 = [:,{0,1,2}:] holds
b1 = b2
;
end;

:: deftheorem Def18 defines ARS_01 ABSRED_0:def 9 :
for b1 being strict ARS holds
( b1 = ARS_01 iff ( the carrier of b1 = {0,1} & the reduction of b1 = [:,{0,1}:] ) );

:: deftheorem Def19 defines ARS_02 ABSRED_0:def 10 :
for b1 being strict ARS holds
( b1 = ARS_02 iff ( the carrier of b1 = {0,1,2} & the reduction of b1 = [:,{0,1,2}:] ) );

registration
cluster ARS_01 -> non empty strict ;
coherence
not ARS_01 is empty
by Def18;
cluster ARS_02 -> non empty strict ;
coherence
not ARS_02 is empty
by Def19;
end;

theorem ThA1: :: ABSRED_0:87
for s being set holds
( s is Element of ARS_01 iff ( s = 0 or s = 1 ) )
proof end;

theorem :: ABSRED_0:88
for i, j being Element of ARS_01 holds
( i ==> j iff i = 0 )
proof end;

theorem ThB1: :: ABSRED_0:89
for s being set holds
( s is Element of ARS_02 iff ( s = 0 or s = 1 or s = 2 ) )
proof end;

theorem :: ABSRED_0:90
for m, n being Element of ARS_02 holds
( m ==> n iff m = 0 )
proof end;

definition
let X be ARS ;
let x be Element of X;
attr x is normform means :: ABSRED_0:def 11
for y being Element of X holds not x ==> y;
end;

:: deftheorem defines normform ABSRED_0:def 11 :
for X being ARS
for x being Element of X holds
( x is normform iff for y being Element of X holds not x ==> y );

theorem Ch1: :: ABSRED_0:91
for X being ARS
for x being Element of X holds
( x is normform iff x is_a_normal_form_wrt the reduction of X )
proof end;

definition
let X be ARS ;
let x, y be Element of X;
pred x is_normform_of y means :: ABSRED_0:def 12
( x is normform & y =*=> x );
end;

:: deftheorem defines is_normform_of ABSRED_0:def 12 :
for X being ARS
for x, y being Element of X holds
( x is_normform_of y iff ( x is normform & y =*=> x ) );

theorem Ch2: :: ABSRED_0:92
for X being ARS
for x, y being Element of X holds
( x is_normform_of y iff x is_a_normal_form_of y, the reduction of X )
proof end;

definition
let X be ARS ;
let x be Element of X;
attr x is normalizable means :: ABSRED_0:def 13
ex y being Element of X st y is_normform_of x;
end;

:: deftheorem defines normalizable ABSRED_0:def 13 :
for X being ARS
for x being Element of X holds
( x is normalizable iff ex y being Element of X st y is_normform_of x );

theorem Ch3: :: ABSRED_0:93
for X being ARS
for x being Element of X holds
( x is normalizable iff x has_a_normal_form_wrt the reduction of X )
proof end;

definition
let X be ARS ;
attr X is WN means :: ABSRED_0:def 14
for x being Element of X holds x is normalizable ;
attr X is SN means :: ABSRED_0:def 15
for f being Function of NAT, the carrier of X holds
not for i being Nat holds f . i ==> f . (i + 1);
attr X is UN* means :: ABSRED_0:def 16
for x, y, z being Element of X st y is_normform_of x & z is_normform_of x holds
y = z;
attr X is UN means :: ABSRED_0:def 17
for x, y being Element of X st x is normform & y is normform & x <=*=> y holds
x = y;
attr X is N.F. means :: ABSRED_0:def 18
for x, y being Element of X st x is normform & x <=*=> y holds
y =*=> x;
end;

:: deftheorem defines WN ABSRED_0:def 14 :
for X being ARS holds
( X is WN iff for x being Element of X holds x is normalizable );

:: deftheorem defines SN ABSRED_0:def 15 :
for X being ARS holds
( X is SN iff for f being Function of NAT, the carrier of X holds
not for i being Nat holds f . i ==> f . (i + 1) );

:: deftheorem defines UN* ABSRED_0:def 16 :
for X being ARS holds
( X is UN* iff for x, y, z being Element of X st y is_normform_of x & z is_normform_of x holds
y = z );

:: deftheorem defines UN ABSRED_0:def 17 :
for X being ARS holds
( X is UN iff for x, y being Element of X st x is normform & y is normform & x <=*=> y holds
x = y );

:: deftheorem defines N.F. ABSRED_0:def 18 :
for X being ARS holds
( X is N.F. iff for x, y being Element of X st x is normform & x <=*=> y holds
y =*=> x );

theorem :: ABSRED_0:94
for X being ARS holds
( X is WN iff the reduction of X is weakly-normalizing )
proof end;

theorem Ch7: :: ABSRED_0:95
for X being ARS st X is SN holds
the reduction of X is strongly-normalizing
proof end;

theorem Ch8: :: ABSRED_0:96
for X being ARS st not X is empty & the reduction of X is strongly-normalizing holds
X is SN
proof end;

theorem ThSN: :: ABSRED_0:97
for X being ARS holds
( X is SN iff for A being set
for z being Element of X holds
( not z in A or ex x being Element of X st
( x in A & ( for y being Element of X holds
( not y in A or not x ==> y ) ) ) ) )
proof end;

scheme :: ABSRED_0:sch 8
notSN{ F1() -> ARS , P1[ object ] } :
not F1() is SN
provided
A1: ex x being Element of F1() st P1[x] and
A2: for x being Element of F1() st P1[x] holds
ex y being Element of F1() st
( P1[y] & x ==> y )
proof end;

theorem :: ABSRED_0:98
for X being ARS holds
( X is UN iff the reduction of X is with_UN_property )
proof end;

theorem :: ABSRED_0:99
for X being ARS holds
( X is N.F. iff the reduction of X is with_NF_property )
proof end;

definition
let X be ARS ;
let x be Element of X;
assume that
A: ex y being Element of X st y is_normform_of x and
B: for y, z being Element of X st y is_normform_of x & z is_normform_of x holds
y = z ;
func nf x -> Element of X means :Def17: :: ABSRED_0:def 19
it is_normform_of x;
existence
ex b1 being Element of X st b1 is_normform_of x
by A;
uniqueness
for b1, b2 being Element of X st b1 is_normform_of x & b2 is_normform_of x holds
b1 = b2
by B;
end;

:: deftheorem Def17 defines nf ABSRED_0:def 19 :
for X being ARS
for x being Element of X st ex y being Element of X st y is_normform_of x & ( for y, z being Element of X st y is_normform_of x & z is_normform_of x holds
y = z ) holds
for b3 being Element of X holds
( b3 = nf x iff b3 is_normform_of x );

theorem :: ABSRED_0:100
for X being ARS
for x being Element of X st ex y being Element of X st y is_normform_of x & ( for y, z being Element of X st y is_normform_of x & z is_normform_of x holds
y = z ) holds
nf x = nf (x, the reduction of X)
proof end;

theorem LemN1: :: ABSRED_0:101
for X being ARS
for x, y being Element of X st x is normform & x =*=> y holds
x = y
proof end;

theorem LemN2: :: ABSRED_0:102
for X being ARS
for x being Element of X st x is normform holds
x is_normform_of x ;

theorem :: ABSRED_0:103
for X being ARS
for x, y being Element of X st x is normform & y ==> x holds
x is_normform_of y by Th2;

theorem :: ABSRED_0:104
for X being ARS
for x, y being Element of X st x is normform & y =01=> x holds
x is_normform_of y by Lem1;

theorem :: ABSRED_0:105
for X being ARS
for x, y being Element of X st x is normform & y =+=> x holds
x is_normform_of y by Lem2;

theorem :: ABSRED_0:106
for X being ARS
for x, y being Element of X st x is_normform_of y & y is_normform_of x holds
x = y by LemN1;

theorem LemN6: :: ABSRED_0:107
for X being ARS
for x, y, z being Element of X st x is_normform_of y & z ==> y holds
x is_normform_of z by Lem5;

theorem LemN7: :: ABSRED_0:108
for X being ARS
for x, y, z being Element of X st x is_normform_of y & z =*=> y holds
x is_normform_of z by Th3;

theorem :: ABSRED_0:109
for X being ARS
for x, y, z being Element of X st x is_normform_of y & z =*=> x holds
x is_normform_of z ;

registration
let X be ARS ;
cluster normform -> normalizable for Element of the carrier of X;
coherence
for b1 being Element of X st b1 is normform holds
b1 is normalizable
proof end;
end;

theorem LemN5: :: ABSRED_0:110
for X being ARS
for x, y being Element of X st x is normalizable & y ==> x holds
y is normalizable by LemN6;

theorem ThWN1: :: ABSRED_0:111
for X being ARS holds
( X is WN iff for x being Element of X ex y being Element of X st y is_normform_of x )
proof end;

theorem :: ABSRED_0:112
for X being ARS st ( for x being Element of X holds x is normform ) holds
X is WN
proof end;

registration
cluster SN -> WN for ARS ;
coherence
for b1 being ARS st b1 is SN holds
b1 is WN
proof end;
end;

theorem LmA: :: ABSRED_0:113
for X being ARS
for x, y being Element of X st x <> y & ( for a, b being Element of X holds
( a ==> b iff a = x ) ) holds
( y is normform & x is normalizable )
proof end;

theorem :: ABSRED_0:114
ex X being ARS st
( X is WN & not X is SN )
proof end;

registration
cluster N.F. -> UN* for ARS ;
coherence
for b1 being ARS st b1 is N.F. holds
b1 is UN*
proof end;
cluster N.F. -> UN for ARS ;
coherence
for b1 being ARS st b1 is N.F. holds
b1 is UN
by LemN1;
cluster UN -> UN* for ARS ;
coherence
for b1 being ARS st b1 is UN holds
b1 is UN*
proof end;
end;

theorem LemN12: :: ABSRED_0:115
for X being ARS
for x, y being Element of X st X is WN & X is UN* & x is normform & x <=*=> y holds
y =*=> x
proof end;

registration
cluster WN UN* -> N.F. for ARS ;
coherence
for b1 being ARS st b1 is WN & b1 is UN* holds
b1 is N.F.
by LemN12;
cluster WN UN* -> UN for ARS ;
coherence
for b1 being ARS st b1 is WN & b1 is UN* holds
b1 is UN
;
end;

theorem Lem21: :: ABSRED_0:116
for X being ARS
for x, y, z being Element of X st y is_normform_of x & z is_normform_of x & y <> z holds
x =+=> y
proof end;

theorem Lem22: :: ABSRED_0:117
for X being ARS
for x being Element of X st X is WN & X is UN* holds
nf x is_normform_of x
proof end;

theorem Lem23: :: ABSRED_0:118
for X being ARS
for x, y being Element of X st X is WN & X is UN* & y is_normform_of x holds
y = nf x
proof end;

theorem Lem24: :: ABSRED_0:119
for X being ARS
for x being Element of X st X is WN & X is UN* holds
nf x is normform
proof end;

theorem :: ABSRED_0:120
for X being ARS
for x being Element of X st X is WN & X is UN* holds
nf (nf x) = nf x
proof end;

theorem Lem26: :: ABSRED_0:121
for X being ARS
for x, y being Element of X st X is WN & X is UN* & x =*=> y holds
nf x = nf y
proof end;

theorem Lem27: :: ABSRED_0:122
for X being ARS
for x, y being Element of X st X is WN & X is UN* & x <=*=> y holds
nf x = nf y
proof end;

theorem :: ABSRED_0:123
for X being ARS
for x, y being Element of X st X is WN & X is UN* & nf x = nf y holds
x <=*=> y
proof end;

definition
let X be ARS ;
let x, y be Element of X;
pred x <<>> y means :: ABSRED_0:def 20
ex z being Element of X st
( x <=*= z & z =*=> y );
symmetry
for x, y being Element of X st ex z being Element of X st
( x <=*= z & z =*=> y ) holds
ex z being Element of X st
( y <=*= z & z =*=> x )
;
reflexivity
for x being Element of X ex z being Element of X st
( x <=*= z & z =*=> x )
;
pred x >><< y means :DEF2: :: ABSRED_0:def 21
ex z being Element of X st
( x =*=> z & z <=*= y );
symmetry
for x, y being Element of X st ex z being Element of X st
( x =*=> z & z <=*= y ) holds
ex z being Element of X st
( y =*=> z & z <=*= x )
;
reflexivity
for x being Element of X ex z being Element of X st
( x =*=> z & z <=*= x )
;
pred x <<01>> y means :: ABSRED_0:def 22
ex z being Element of X st
( x <=01= z & z =01=> y );
symmetry
for x, y being Element of X st ex z being Element of X st
( x <=01= z & z =01=> y ) holds
ex z being Element of X st
( y <=01= z & z =01=> x )
;
reflexivity
for x being Element of X ex z being Element of X st
( x <=01= z & z =01=> x )
;
pred x >>01<< y means :: ABSRED_0:def 23
ex z being Element of X st
( x =01=> z & z <=01= y );
symmetry
for x, y being Element of X st ex z being Element of X st
( x =01=> z & z <=01= y ) holds
ex z being Element of X st
( y =01=> z & z <=01= x )
;
reflexivity
for x being Element of X ex z being Element of X st
( x =01=> z & z <=01= x )
;
end;

:: deftheorem defines <<>> ABSRED_0:def 20 :
for X being ARS
for x, y being Element of X holds
( x <<>> y iff ex z being Element of X st
( x <=*= z & z =*=> y ) );

:: deftheorem DEF2 defines >><< ABSRED_0:def 21 :
for X being ARS
for x, y being Element of X holds
( x >><< y iff ex z being Element of X st
( x =*=> z & z <=*= y ) );

:: deftheorem defines <<01>> ABSRED_0:def 22 :
for X being ARS
for x, y being Element of X holds
( x <<01>> y iff ex z being Element of X st
( x <=01= z & z =01=> y ) );

:: deftheorem defines >>01<< ABSRED_0:def 23 :
for X being ARS
for x, y being Element of X holds
( x >>01<< y iff ex z being Element of X st
( x =01=> z & z <=01= y ) );

theorem Ch11: :: ABSRED_0:124
for X being ARS
for x, y being Element of X holds
( x <<>> y iff x,y are_divergent_wrt the reduction of X )
proof end;

theorem Ch12: :: ABSRED_0:125
for X being ARS
for x, y being Element of X holds
( x >><< y iff x,y are_convergent_wrt the reduction of X )
proof end;

theorem :: ABSRED_0:126
for X being ARS
for x, y being Element of X holds
( x <<01>> y iff x,y are_divergent<=1_wrt the reduction of X )
proof end;

theorem Ch14: :: ABSRED_0:127
for X being ARS
for x, y being Element of X holds
( x >>01<< y iff x,y are_convergent<=1_wrt the reduction of X )
proof end;

definition
let X be ARS ;
attr X is DIAMOND means :: ABSRED_0:def 24
for x, y being Element of X st x <<01>> y holds
x >>01<< y;
attr X is CONF means :: ABSRED_0:def 25
for x, y being Element of X st x <<>> y holds
x >><< y;
attr X is CR means :: ABSRED_0:def 26
for x, y being Element of X st x <=*=> y holds
x >><< y;
attr X is WCR means :: ABSRED_0:def 27
for x, y being Element of X st x <<01>> y holds
x >><< y;
end;

:: deftheorem defines DIAMOND ABSRED_0:def 24 :
for X being ARS holds
( X is DIAMOND iff for x, y being Element of X st x <<01>> y holds
x >>01<< y );

:: deftheorem defines CONF ABSRED_0:def 25 :
for X being ARS holds
( X is CONF iff for x, y being Element of X st x <<>> y holds
x >><< y );

:: deftheorem defines CR ABSRED_0:def 26 :
for X being ARS holds
( X is CR iff for x, y being Element of X st x <=*=> y holds
x >><< y );

:: deftheorem defines WCR ABSRED_0:def 27 :
for X being ARS holds
( X is WCR iff for x, y being Element of X st x <<01>> y holds
x >><< y );

definition
let X be ARS ;
attr X is COMP means :: ABSRED_0:def 28
( X is SN & X is CONF );
end;

:: deftheorem defines COMP ABSRED_0:def 28 :
for X being ARS holds
( X is COMP iff ( X is SN & X is CONF ) );

scheme :: ABSRED_0:sch 9
isCR{ F1() -> non empty ARS , F2( Element of F1()) -> Element of F1() } :
F1() is CR
provided
A1: for x being Element of F1() holds x =*=> F2(x) and
A2: for x, y being Element of F1() st x <=*=> y holds
F2(x) = F2(y)
proof end;

Lm3: for X being ARS
for x, y being Element of X st x =*=> y holds
x <=*=> y

proof end;

Lm2: for X being ARS
for x, y being Element of X st x <<>> y holds
x <=*=> y

proof end;

Lm1: for X being ARS st X is CR holds
X is CONF

by Lm2;

scheme :: ABSRED_0:sch 10
isCOMP{ F1() -> non empty ARS , F2( Element of F1()) -> Element of F1() } :
F1() is COMP
provided
A1: F1() is SN and
A2: for x being Element of F1() holds x =*=> F2(x) and
A3: for x, y being Element of F1() st x <=*=> y holds
F2(x) = F2(y)
proof end;

theorem Lem18: :: ABSRED_0:128
for X being ARS
for x, y being Element of X st x <<01>> y holds
x <<>> y
proof end;

theorem Lem18a: :: ABSRED_0:129
for X being ARS
for x, y being Element of X st x >>01<< y holds
x >><< y
proof end;

theorem :: ABSRED_0:130
for X being ARS
for x, y being Element of X st x ==> y holds
x <<01>> y
proof end;

theorem Th17: :: ABSRED_0:131
for X being ARS
for x, y being Element of X st x ==> y holds
x >>01<< y
proof end;

theorem :: ABSRED_0:132
for X being ARS
for x, y being Element of X st x =01=> y holds
x <<01>> y ;

theorem :: ABSRED_0:133
for X being ARS
for x, y being Element of X st x =01=> y holds
x >>01<< y ;

theorem :: ABSRED_0:134
for X being ARS
for x, y being Element of X st x <==> y holds
x <<01>> y
proof end;

theorem :: ABSRED_0:135
for X being ARS
for x, y being Element of X st x <==> y holds
x >>01<< y
proof end;

theorem :: ABSRED_0:136
for X being ARS
for x, y being Element of X st x <=01=> y holds
x <<01>> y
proof end;

theorem :: ABSRED_0:137
for X being ARS
for x, y being Element of X st x <=01=> y holds
x >>01<< y
proof end;

theorem Th17a: :: ABSRED_0:138
for X being ARS
for x, y being Element of X st x ==> y holds
x >><< y by ;

theorem Lem17: :: ABSRED_0:139
for X being ARS
for x, y being Element of X st x =*=> y holds
x >><< y ;

theorem :: ABSRED_0:140
for X being ARS
for x, y being Element of X st x =*=> y holds
x <<>> y ;

theorem :: ABSRED_0:141
for X being ARS
for x, y being Element of X st x =+=> y holds
x >><< y
proof end;

theorem :: ABSRED_0:142
for X being ARS
for x, y being Element of X st x =+=> y holds
x <<>> y
proof end;

theorem Lm11: :: ABSRED_0:143
for X being ARS
for x, y, z being Element of X st x ==> y & x ==> z holds
y <<01>> z
proof end;

theorem :: ABSRED_0:144
for X being ARS
for x, y, z being Element of X st x ==> y & z ==> y holds
x >>01<< z
proof end;

theorem :: ABSRED_0:145
for X being ARS
for x, y, z being Element of X st x >><< z & z <== y holds
x >><< y
proof end;

theorem :: ABSRED_0:146
for X being ARS
for x, y, z being Element of X st x >><< z & z <=01= y holds
x >><< y
proof end;

theorem Lm5: :: ABSRED_0:147
for X being ARS
for x, y, z being Element of X st x >><< z & z <=*= y holds
x >><< y
proof end;

theorem Lem19: :: ABSRED_0:148
for X being ARS
for x, y being Element of X st x <<>> y holds
x <=*=> y
proof end;

theorem :: ABSRED_0:149
for X being ARS
for x, y being Element of X st x >><< y holds
x <=*=> y
proof end;

theorem :: ABSRED_0:150
for X being ARS holds
( X is DIAMOND iff the reduction of X is subcommutative )
proof end;

theorem Ch17: :: ABSRED_0:151
for X being ARS holds
( X is CONF iff the reduction of X is confluent )
proof end;

theorem :: ABSRED_0:152
for X being ARS holds
( X is CR iff the reduction of X is with_Church-Rosser_property )
proof end;

theorem :: ABSRED_0:153
for X being ARS holds
( X is WCR iff the reduction of X is locally-confluent )
proof end;

theorem :: ABSRED_0:154
for X being non empty ARS holds
( X is COMP iff the reduction of X is complete )
proof end;

theorem LemA: :: ABSRED_0:155
for X being ARS
for x, y, z being Element of X st X is DIAMOND & x <=*= z & z =01=> y holds
ex u being Element of X st
( x =01=> u & u <=*= y )
proof end;

theorem :: ABSRED_0:156
for X being ARS
for x, y, z being Element of X st X is DIAMOND & x <=01= y & y =*=> z holds
ex u being Element of X st
( x =*=> u & u <=01= z )
proof end;

registration
cluster DIAMOND -> CONF for ARS ;
coherence
for b1 being ARS st b1 is DIAMOND holds
b1 is CONF
proof end;
end;

registration
cluster DIAMOND -> CR for ARS ;
coherence
for b1 being ARS st b1 is DIAMOND holds
b1 is CR
proof end;
end;

registration
cluster CR -> WCR for ARS ;
coherence
for b1 being ARS st b1 is CR holds
b1 is WCR
proof end;
end;

registration
cluster CR -> CONF for ARS ;
coherence
for b1 being ARS st b1 is CR holds
b1 is CONF
by Lm1;
end;

registration
cluster CONF -> CR for ARS ;
coherence
for b1 being ARS st b1 is CONF holds
b1 is CR
proof end;
end;

theorem :: ABSRED_0:157
for X being ARS st not X is CONF & X is WN holds
ex x, y, z being Element of X st
( y is_normform_of x & z is_normform_of x & y <> z )
proof end;

registration
cluster SN WCR -> CR for ARS ;
coherence
for b1 being ARS st b1 is SN & b1 is WCR holds
b1 is CR
proof end;
end;

registration
cluster CR -> N.F. for ARS ;
coherence
for b1 being ARS st b1 is CR holds
b1 is N.F.
proof end;
end;

registration
cluster WN UN -> CR for ARS ;
coherence
for b1 being ARS st b1 is WN & b1 is UN holds
b1 is CR
proof end;
end;

registration
cluster SN CR -> COMP for ARS ;
coherence
for b1 being ARS st b1 is SN & b1 is CR holds
b1 is COMP
;
coherence
for b1 being ARS st b1 is COMP holds
( b1 is CR & b1 is WCR & b1 is N.F. & b1 is UN & b1 is UN* & b1 is WN )
;
end;

theorem :: ABSRED_0:158
for X being ARS st X is COMP holds
for x, y being Element of X st x <=*=> y holds
nf x = nf y by Lem27;

registration
cluster WN UN* -> CR for ARS ;
coherence
for b1 being ARS st b1 is WN & b1 is UN* holds
b1 is CR
;
cluster SN UN* -> COMP for ARS ;
coherence
for b1 being ARS st b1 is SN & b1 is UN* holds
b1 is COMP
;
end;

definition
attr c1 is strict ;
struct TRSStr -> ARS , UAStr ;
end;

registration
existence
( not b1 is empty & b1 is non-empty & b1 is strict )
proof end;
end;

definition
let S be non empty UAStr ;
attr S is Group-like means :: ABSRED_0:def 29
( Seg 3 c= dom the charact of S & ( for f being non empty homogeneous PartFunc of ( the carrier of S *), the carrier of S holds
( ( f = the charact of S . 1 implies arity f = 0 ) & ( f = the charact of S . 2 implies arity f = 1 ) & ( f = the charact of S . 3 implies arity f = 2 ) ) ) );
end;

:: deftheorem defines Group-like ABSRED_0:def 29 :
for S being non empty UAStr holds
( S is Group-like iff ( Seg 3 c= dom the charact of S & ( for f being non empty homogeneous PartFunc of ( the carrier of S *), the carrier of S holds
( ( f = the charact of S . 1 implies arity f = 0 ) & ( f = the charact of S . 2 implies arity f = 1 ) & ( f = the charact of S . 3 implies arity f = 2 ) ) ) ) );

theorem Th01: :: ABSRED_0:159
for X being non empty set
for f1, f2, f3 being non empty homogeneous PartFunc of (X *),X st arity f1 = 0 & arity f2 = 1 & arity f3 = 2 holds
for S being non empty UAStr st the carrier of S = X & <*f1,f2,f3*> c= the charact of S holds
S is Group-like
proof end;

theorem Th02: :: ABSRED_0:160
for X being non empty set
for f1, f2, f3 being non empty homogeneous quasi_total PartFunc of (X *),X
for S being non empty UAStr st the carrier of S = X & <*f1,f2,f3*> = the charact of S holds
( S is quasi_total & S is partial )
proof end;

definition
let S be non empty non-empty UAStr ;
let o be operation of S;
let a be Element of dom o;
:: original: .
redefine func o . a -> Element of S;
coherence
o . a is Element of S
proof end;
end;

registration
let S be non empty non-empty UAStr ;
cluster -> non empty for Element of rng the charact of S;
coherence
for b1 being operation of S holds not b1 is empty
by RELAT_1:def 9;
let o be operation of S;
coherence
for b1 being Element of dom o holds
( b1 is Relation-like & b1 is Function-like )
proof end;
end;

registration
let S be non empty partial non-empty UAStr ;
cluster -> homogeneous for Element of rng the charact of S;
coherence
for b1 being operation of S holds b1 is homogeneous
proof end;
end;

registration
let S be non empty quasi_total non-empty UAStr ;
cluster -> quasi_total for Element of rng the charact of S;
coherence
for b1 being operation of S holds b1 is quasi_total
proof end;
end;

theorem ThA: :: ABSRED_0:161
for S being non empty non-empty UAStr st S is Group-like holds
( 1 is OperSymbol of S & 2 is OperSymbol of S & 3 is OperSymbol of S )
proof end;

theorem ThB: :: ABSRED_0:162
for S being non empty partial non-empty UAStr st S is Group-like holds
( arity (Den ((In (1,(dom the charact of S))),S)) = 0 & arity (Den ((In (2,(dom the charact of S))),S)) = 1 & arity (Den ((In (3,(dom the charact of S))),S)) = 2 )
proof end;

definition
let S be non empty non-empty TRSStr ;
attr S is invariant means :DEF2: :: ABSRED_0:def 30
for o being OperSymbol of S
for a, b being Element of dom (Den (o,S))
for i being Nat st i in dom a holds
for x, y being Element of S st x = a . i & b = a +* (i,y) & x ==> y holds
(Den (o,S)) . a ==> (Den (o,S)) . b;
end;

:: deftheorem DEF2 defines invariant ABSRED_0:def 30 :
for S being non empty non-empty TRSStr holds
( S is invariant iff for o being OperSymbol of S
for a, b being Element of dom (Den (o,S))
for i being Nat st i in dom a holds
for x, y being Element of S st x = a . i & b = a +* (i,y) & x ==> y holds
(Den (o,S)) . a ==> (Den (o,S)) . b );

definition
let S be non empty non-empty TRSStr ;
attr S is compatible means :: ABSRED_0:def 31
for o being OperSymbol of S
for a, b being Element of dom (Den (o,S)) st ( for i being Nat st i in dom a holds
for x, y being Element of S st x = a . i & y = b . i holds
x ==> y ) holds
(Den (o,S)) . a =*=> (Den (o,S)) . b;
end;

:: deftheorem defines compatible ABSRED_0:def 31 :
for S being non empty non-empty TRSStr holds
( S is compatible iff for o being OperSymbol of S
for a, b being Element of dom (Den (o,S)) st ( for i being Nat st i in dom a holds
for x, y being Element of S st x = a . i & y = b . i holds
x ==> y ) holds
(Den (o,S)) . a =*=> (Den (o,S)) . b );

theorem Th0: :: ABSRED_0:163
for n being natural number
for X being non empty set
for x being Element of X ex f being non empty homogeneous quasi_total PartFunc of (X *),X st
( arity f = n & f = () --> x )
proof end;

registration
let X be non empty set ;
let O be PFuncFinSequence of X;
let r be Relation of X;
cluster TRSStr(# X,O,r #) -> non empty ;
coherence
not TRSStr(# X,O,r #) is empty
;
end;

registration
let X be non empty set ;
let O be non-empty non empty PFuncFinSequence of X;
let r be Relation of X;
cluster TRSStr(# X,O,r #) -> non-empty ;
coherence
proof end;
end;

definition
let X be non empty set ;
let x be Element of X;
func TotalTRS (X,x) -> non empty non-empty strict TRSStr means :DEF3: :: ABSRED_0:def 32
( the carrier of it = X & the charact of it = <*(() --> x),(() --> x),(() --> x)*> & the reduction of it = nabla X );
uniqueness
for b1, b2 being non empty non-empty strict TRSStr st the carrier of b1 = X & the charact of b1 = <*(() --> x),(() --> x),(() --> x)*> & the reduction of b1 = nabla X & the carrier of b2 = X & the charact of b2 = <*(() --> x),(() --> x),(() --> x)*> & the reduction of b2 = nabla X holds
b1 = b2
;
existence
ex b1 being non empty non-empty strict TRSStr st
( the carrier of b1 = X & the charact of b1 = <*(() --> x),(() --> x),(() --> x)*> & the reduction of b1 = nabla X )
proof end;
end;

:: deftheorem DEF3 defines TotalTRS ABSRED_0:def 32 :
for X being non empty set
for x being Element of X
for b3 being non empty non-empty strict TRSStr holds
( b3 = TotalTRS (X,x) iff ( the carrier of b3 = X & the charact of b3 = <*(() --> x),(() --> x),(() --> x)*> & the reduction of b3 = nabla X ) );

registration
let X be non empty set ;
let x be Element of X;
coherence
( TotalTRS (X,x) is quasi_total & TotalTRS (X,x) is partial & TotalTRS (X,x) is Group-like & TotalTRS (X,x) is invariant )
proof end;
end;

registration
existence
ex b1 being non empty non-empty TRSStr st
( b1 is strict & b1 is quasi_total & b1 is partial & b1 is Group-like & b1 is invariant )
proof end;
end;

definition
let S be non empty partial quasi_total non-empty Group-like TRSStr ;
func 1. S -> Element of S equals :: ABSRED_0:def 33
(Den ((In (1,(dom the charact of S))),S)) . {};
coherence
(Den ((In (1,(dom the charact of S))),S)) . {} is Element of S
proof end;
let a be Element of S;
func a " -> Element of S equals :: ABSRED_0:def 34
(Den ((In (2,(dom the charact of S))),S)) . <*a*>;
coherence
(Den ((In (2,(dom the charact of S))),S)) . <*a*> is Element of S
proof end;
let b be Element of S;
func a * b -> Element of S equals :: ABSRED_0:def 35
(Den ((In (3,(dom the charact of S))),S)) . <*a,b*>;
coherence
(Den ((In (3,(dom the charact of S))),S)) . <*a,b*> is Element of S
proof end;
end;

:: deftheorem defines 1. ABSRED_0:def 33 :
for S being non empty partial quasi_total non-empty Group-like TRSStr holds 1. S = (Den ((In (1,(dom the charact of S))),S)) . {};

:: deftheorem defines " ABSRED_0:def 34 :
for S being non empty partial quasi_total non-empty Group-like TRSStr
for a being Element of S holds a " = (Den ((In (2,(dom the charact of S))),S)) . <*a*>;

:: deftheorem defines * ABSRED_0:def 35 :
for S being non empty partial quasi_total non-empty Group-like TRSStr
for a, b being Element of S holds a * b = (Den ((In (3,(dom the charact of S))),S)) . <*a,b*>;

theorem :: ABSRED_0:164
for S being non empty partial quasi_total non-empty Group-like invariant TRSStr
for a, b being Element of S st a ==> b holds
a " ==> b "
proof end;

theorem ThI2: :: ABSRED_0:165
for S being non empty partial quasi_total non-empty Group-like invariant TRSStr
for a, b, c being Element of S st a ==> b holds
a * c ==> b * c
proof end;

theorem ThI3: :: ABSRED_0:166
for S being non empty partial quasi_total non-empty Group-like invariant TRSStr
for a, b, c being Element of S st a ==> b holds
c * a ==> c * b
proof end;

definition
let S be non empty partial quasi_total non-empty Group-like TRSStr ;
attr S is (R1) means :: ABSRED_0:def 36
for a being Element of S holds (1. S) * a ==> a;
attr S is (R2) means :: ABSRED_0:def 37
for a being Element of S holds (a ") * a ==> 1. S;
attr S is (R3) means :: ABSRED_0:def 38
for a, b, c being Element of S holds (a * b) * c ==> a * (b * c);
attr S is (R4) means :: ABSRED_0:def 39
for a, b being Element of S holds (a ") * (a * b) ==> b;
attr S is (R5) means :: ABSRED_0:def 40
for a being Element of S holds ((1. S) ") * a ==> a;
attr S is (R6) means :: ABSRED_0:def 41
for a being Element of S holds ((a ") ") * (1. S) ==> a;
attr S is (R7) means :: ABSRED_0:def 42
for a, b being Element of S holds ((a ") ") * b ==> a * b;
attr S is (R8) means :: ABSRED_0:def 43
for a being Element of S holds a * (1. S) ==> a;
attr S is (R9) means :: ABSRED_0:def 44
for a being Element of S holds (a ") " ==> a;
attr S is (R10) means :: ABSRED_0:def 45
(1. S) " ==> 1. S;
attr S is (R11) means :: ABSRED_0:def 46
for a being Element of S holds a * (a ") ==> 1. S;
attr S is (R12) means :: ABSRED_0:def 47
for a, b being Element of S holds a * ((a ") * b) ==> b;
attr S is (R13) means :: ABSRED_0:def 48
for a, b being Element of S holds a * (b * ((a * b) ")) ==> 1. S;
attr S is (R14) means :: ABSRED_0:def 49
for a, b being Element of S holds a * ((b * a) ") ==> b " ;
attr S is (R15) means :: ABSRED_0:def 50
for a, b being Element of S holds (a * b) " ==> (b ") * (a ");
end;

:: deftheorem defines (R1) ABSRED_0:def 36 :
for S being non empty partial quasi_total non-empty Group-like TRSStr holds
( S is (R1) iff for a being Element of S holds (1. S) * a ==> a );

:: deftheorem defines (R2) ABSRED_0:def 37 :
for S being non empty partial quasi_total non-empty Group-like TRSStr holds
( S is (R2) iff for a being Element of S holds (a ") * a ==> 1. S );

:: deftheorem defines (R3) ABSRED_0:def 38 :
for S being non empty partial quasi_total non-empty Group-like TRSStr holds
( S is (R3) iff for a, b, c being Element of S holds (a * b) * c ==> a * (b * c) );

:: deftheorem defines (R4) ABSRED_0:def 39 :
for S being non empty partial quasi_total non-empty Group-like TRSStr holds
( S is (R4) iff for a, b being Element of S holds (a ") * (a * b) ==> b );

:: deftheorem defines (R5) ABSRED_0:def 40 :
for S being non empty partial quasi_total non-empty Group-like TRSStr holds
( S is (R5) iff for a being Element of S holds ((1. S) ") * a ==> a );

:: deftheorem defines (R6) ABSRED_0:def 41 :
for S being non empty partial quasi_total non-empty Group-like TRSStr holds
( S is (R6) iff for a being Element of S holds ((a ") ") * (1. S) ==> a );

:: deftheorem defines (R7) ABSRED_0:def 42 :
for S being non empty partial quasi_total non-empty Group-like TRSStr holds
( S is (R7) iff for a, b being Element of S holds ((a ") ") * b ==> a * b );

:: deftheorem defines (R8) ABSRED_0:def 43 :
for S being non empty partial quasi_total non-empty Group-like TRSStr holds
( S is (R8) iff for a being Element of S holds a * (1. S) ==> a );

:: deftheorem defines (R9) ABSRED_0:def 44 :
for S being non empty partial quasi_total non-empty Group-like TRSStr holds
( S is (R9) iff for a being Element of S holds (a ") " ==> a );

:: deftheorem defines (R10) ABSRED_0:def 45 :
for S being non empty partial quasi_total non-empty Group-like TRSStr holds
( S is (R10) iff (1. S) " ==> 1. S );

:: deftheorem defines (R11) ABSRED_0:def 46 :
for S being non empty partial quasi_total non-empty Group-like TRSStr holds
( S is (R11) iff for a being Element of S holds a * (a ") ==> 1. S );

:: deftheorem defines (R12) ABSRED_0:def 47 :
for S being non empty partial quasi_total non-empty Group-like TRSStr holds
( S is (R12) iff for a, b being Element of S holds a * ((a ") * b) ==> b );

:: deftheorem defines (R13) ABSRED_0:def 48 :
for S being non empty partial quasi_total non-empty Group-like TRSStr holds
( S is (R13) iff for a, b being Element of S holds a * (b * ((a * b) ")) ==> 1. S );

:: deftheorem defines (R14) ABSRED_0:def 49 :
for S being non empty partial quasi_total non-empty Group-like TRSStr holds
( S is (R14) iff for a, b being Element of S holds a * ((b * a) ") ==> b " );

:: deftheorem defines (R15) ABSRED_0:def 50 :
for S being non empty partial quasi_total non-empty Group-like TRSStr holds
( S is (R15) iff for a, b being Element of S holds (a * b) " ==> (b ") * (a ") );

theorem :: ABSRED_0:167
for S being non empty partial quasi_total non-empty Group-like invariant TRSStr
for a, b being Element of S st S is (R1) & S is (R2) & S is (R3) holds
(a ") * (a * b) <<>> b
proof end;

theorem :: ABSRED_0:168
for S being non empty partial quasi_total non-empty Group-like invariant TRSStr
for a being Element of S st S is (R1) & S is (R4) holds
((1. S) ") * a <<>> a
proof end;

theorem :: ABSRED_0:169
for S being non empty partial quasi_total non-empty Group-like invariant TRSStr
for a being Element of S st S is (R2) & S is (R4) holds
((a ") ") * (1. S) <<>> a
proof end;

theorem :: ABSRED_0:170
for S being non empty partial quasi_total non-empty Group-like invariant TRSStr
for a, b being Element of S st S is (R1) & S is (R3) & S is (R6) holds
((a ") ") * b <<>> a * b
proof end;

theorem :: ABSRED_0:171
for S being non empty partial quasi_total non-empty Group-like invariant TRSStr
for a being Element of S st S is (R6) & S is (R7) holds
a * (1. S) <<>> a
proof end;

theorem :: ABSRED_0:172
for S being non empty partial quasi_total non-empty Group-like invariant TRSStr
for a being Element of S st S is (R6) & S is (R8) holds
(a ") " <<>> a
proof end;

theorem :: ABSRED_0:173
for S being non empty partial quasi_total non-empty Group-like invariant TRSStr st S is (R5) & S is (R8) holds
(1. S) " <<>> 1. S
proof end;

theorem :: ABSRED_0:174
for S being non empty partial quasi_total non-empty Group-like invariant TRSStr
for a being Element of S st S is (R2) & S is (R9) holds
a * (a ") <<>> 1. S
proof end;

theorem :: ABSRED_0:175
for S being non empty partial quasi_total non-empty Group-like invariant TRSStr
for a, b being Element of S st S is (R1) & S is (R3) & S is (R11) holds
a * ((a ") * b) <<>> b
proof end;

theorem :: ABSRED_0:176
for S being non empty partial quasi_total non-empty Group-like invariant TRSStr
for a, b being Element of S st S is (R3) & S is (R11) holds
a * (b * ((a * b) ")) <<>> 1. S
proof end;

theorem :: ABSRED_0:177
for S being non empty partial quasi_total non-empty Group-like invariant TRSStr
for a, b being Element of S st S is (R4) & S is (R8) & S is (R13) holds
a * ((b * a) ") <<>> b "
proof end;

theorem :: ABSRED_0:178
for S being non empty partial quasi_total non-empty Group-like invariant TRSStr
for a, b being Element of S st S is (R4) & S is (R14) holds
(a * b) " <<>> (b ") * (a ")
proof end;

theorem :: ABSRED_0:179
for S being non empty partial quasi_total non-empty Group-like invariant TRSStr
for a being Element of S st S is (R1) & S is (R10) holds
((1. S) ") * a =*=> a
proof end;

theorem :: ABSRED_0:180
for S being non empty partial quasi_total non-empty Group-like invariant TRSStr
for a being Element of S st S is (R8) & S is (R9) holds
((a ") ") * (1. S) =*=> a
proof end;

theorem :: ABSRED_0:181
for S being non empty partial quasi_total non-empty Group-like invariant TRSStr
for a, b being Element of S st S is (R9) holds
((a ") ") * b =*=> a * b
proof end;

theorem :: ABSRED_0:182
for S being non empty partial quasi_total non-empty Group-like invariant TRSStr
for a, b being Element of S st S is (R11) & S is (R14) holds
a * (b * ((a * b) ")) =*=> 1. S
proof end;

theorem :: ABSRED_0:183
for S being non empty partial quasi_total non-empty Group-like invariant TRSStr
for a, b being Element of S st S is (R12) & S is (R15) holds
a * ((b * a) ") =*=> b "
proof end;