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

definition

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

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 b₁ being ARS st
( not b₁ is empty & b₁ 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{ F₁() -> ARS , P₁[ object ] } :

for x, y being Element of F₁() st x =*=> y & P₁[x] holds
P₁[y]

provided

A1: for x, y being Element of F₁() st x ==> y & P₁[x] holds
P₁[y]

proof end;

scheme :: ABSRED_0:sch 2
Star1{ F₁() -> ARS , P₁[ object ], F₂() -> Element of F₁(), F₃() -> Element of F₁() } :

P₁[F₃()]

provided

A1: F₂() =*=> F₃() and
A2: P₁[F₂()] and
A3: for x, y being Element of F₁() st x ==> y & P₁[x] holds
P₁[y]

proof end;

scheme :: ABSRED_0:sch 3
StarBack{ F₁() -> ARS , P₁[ object ] } :

for x, y being Element of F₁() st x =*=> y & P₁[y] holds
P₁[x]

provided

A1: for x, y being Element of F₁() st x ==> y & P₁[y] holds
P₁[x]

proof end;

scheme :: ABSRED_0:sch 4
StarBack1{ F₁() -> ARS , P₁[ object ], F₂() -> Element of F₁(), F₃() -> Element of F₁() } :

P₁[F₂()]

provided

A1: F₂() =*=> F₃() and
A2: P₁[F₃()] and
A3: for x, y being Element of F₁() st x ==> y & P₁[y] holds
P₁[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{ F₁() -> ARS , P₁[ object ] } :

for x, y being Element of F₁() st x <=*=> y & P₁[x] holds
P₁[y]

provided

A1: for x, y being Element of F₁() st x <==> y & P₁[x] holds
P₁[y]

proof end;

scheme :: ABSRED_0:sch 6
Star2A{ F₁() -> ARS , P₁[ object ], F₂() -> Element of F₁(), F₃() -> Element of F₁() } :

P₁[F₃()]

provided

A1: F₂() <=*=> F₃() and
A2: P₁[F₂()] and
A3: for x, y being Element of F₁() st x <==> y & P₁[x] holds
P₁[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 Lem1, Th4;

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 Lem4, Th4;

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 Lem5, Th4;

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{ F₁() -> non empty set , P₁[ object , object ] } :

ex X being non empty strict ARS st
( the carrier of X = F₁() & ( for x, y being Element of X holds
( x ==> y iff P₁[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},{0,1}:] );

existence
ex b₁ being strict ARS st
( the carrier of b₁ = {0,1} & the reduction of b₁ = [:{0},{0,1}:] )

proof end;

uniqueness
for b₁, b₂ being strict ARS st the carrier of b₁ = {0,1} & the reduction of b₁ = [:{0},{0,1}:] & the carrier of b₂ = {0,1} & the reduction of b₂ = [:{0},{0,1}:] holds
b₁ = b₂ ;

func ARS_02 -> strict ARS means :Def19: :: ABSRED_0:def 10
( the carrier of it = {0,1,2} & the reduction of it = [:{0},{0,1,2}:] );

existence
ex b₁ being strict ARS st
( the carrier of b₁ = {0,1,2} & the reduction of b₁ = [:{0},{0,1,2}:] )

proof end;

uniqueness
for b₁, b₂ being strict ARS st the carrier of b₁ = {0,1,2} & the reduction of b₁ = [:{0},{0,1,2}:] & the carrier of b₂ = {0,1,2} & the reduction of b₂ = [:{0},{0,1,2}:] holds
b₁ = b₂ ;

end;

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

:: deftheorem Def19 defines ARS_02 ABSRED_0:def 10 :
for b₁ being strict ARS holds
( b₁ = ARS_02 iff ( the carrier of b₁ = {0,1,2} & the reduction of b₁ = [:{0},{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{ F₁() -> ARS , P₁[ object ] } :

not F₁() is SN

provided

A1: ex x being Element of F₁() st P₁[x] and
A2: for x being Element of F₁() st P₁[x] holds
ex y being Element of F₁() st
( P₁[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 b₁ being Element of X st b₁ is_normform_of x by A;
uniqueness
for b₁, b₂ being Element of X st b₁ is_normform_of x & b₂ is_normform_of x holds
b₁ = b₂ 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 b₃ being Element of X holds
( b₃ = nf x iff b₃ 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 b₁ being Element of X st b₁ is normform holds
b₁ 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 b₁ being ARS st b₁ is SN holds
b₁ 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 b₁ being ARS st b₁ is N.F. holds
b₁ is UN*

proof end;

cluster N.F. -> UN for ARS ;

coherence
for b₁ being ARS st b₁ is N.F. holds
b₁ is UN by LemN1;

cluster UN -> UN* for ARS ;

coherence
for b₁ being ARS st b₁ is UN holds
b₁ 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 b₁ being ARS st b₁ is WN & b₁ is UN* holds
b₁ is N.F. by LemN12;

cluster WN UN* -> UN for ARS ;

coherence
for b₁ being ARS st b₁ is WN & b₁ is UN* holds
b₁ 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{ F₁() -> non empty ARS , F₂( Element of F₁()) -> Element of F₁() } :

F₁() is CR

provided

A1: for x being Element of F₁() holds x =*=> F₂(x) and
A2: for x, y being Element of F₁() st x <=*=> y holds
F₂(x) = F₂(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{ F₁() -> non empty ARS , F₂( Element of F₁()) -> Element of F₁() } :

F₁() is COMP

provided

A1: F₁() is SN and
A2: for x being Element of F₁() holds x =*=> F₂(x) and
A3: for x, y being Element of F₁() st x <=*=> y holds
F₂(x) = F₂(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 Th17, Lem18a;

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 b₁ being ARS st b₁ is DIAMOND holds
b₁ is CONF

proof end;

end;

registration

cluster DIAMOND -> CR for ARS ;

coherence
for b₁ being ARS st b₁ is DIAMOND holds
b₁ is CR

proof end;

end;

registration

cluster CR -> WCR for ARS ;

coherence
for b₁ being ARS st b₁ is CR holds
b₁ is WCR

proof end;

end;

registration

cluster CR -> CONF for ARS ;

coherence
for b₁ being ARS st b₁ is CR holds
b₁ is CONF by Lm1;

end;

registration

cluster CONF -> CR for ARS ;

coherence
for b₁ being ARS st b₁ is CONF holds
b₁ 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 b₁ being ARS st b₁ is SN & b₁ is WCR holds
b₁ is CR

proof end;

end;

registration

cluster CR -> N.F. for ARS ;

coherence
for b₁ being ARS st b₁ is CR holds
b₁ is N.F.

proof end;

end;

registration

cluster WN UN -> CR for ARS ;

coherence
for b₁ being ARS st b₁ is WN & b₁ is UN holds
b₁ is CR

proof end;

end;

registration

cluster SN CR -> COMP for ARS ;

coherence
for b₁ being ARS st b₁ is SN & b₁ is CR holds
b₁ is COMP ;

cluster COMP -> WN UN* UN N.F. CR WCR for ARS ;

coherence
for b₁ being ARS st b₁ is COMP holds
( b₁ is CR & b₁ is WCR & b₁ is N.F. & b₁ is UN & b₁ is UN* & b₁ 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 b₁ being ARS st b₁ is WN & b₁ is UN* holds
b₁ is CR ;

cluster SN UN* -> COMP for ARS ;

coherence
for b₁ being ARS st b₁ is SN & b₁ is UN* holds
b₁ is COMP ;

end;

definition

attr c₁ is strict ;
struct TRSStr -> ARS , UAStr ;
aggr TRSStr(# carrier, charact, reduction #) -> TRSStr ;

end;

registration

cluster non empty non-empty strict for TRSStr ;

existence
ex b₁ being TRSStr st
( not b₁ is empty & b₁ is non-empty & b₁ 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 b₁ being operation of S holds not b₁ is empty by RELAT_1:def 9;
let o be operation of S;

cluster -> Relation-like Function-like for Element of dom o;

coherence
for b₁ being Element of dom o holds
( b₁ is Relation-like & b₁ 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 b₁ being operation of S holds b₁ 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 b₁ being operation of S holds b₁ 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 = (n -tuples_on X) --> 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
TRSStr(# X,O,r #) is non-empty

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 = <*((0 -tuples_on X) --> x),((1 -tuples_on X) --> x),((2 -tuples_on X) --> x)*> & the reduction of it = nabla X );

uniqueness
for b₁, b₂ being non empty non-empty strict TRSStr st the carrier of b₁ = X & the charact of b₁ = <*((0 -tuples_on X) --> x),((1 -tuples_on X) --> x),((2 -tuples_on X) --> x)*> & the reduction of b₁ = nabla X & the carrier of b₂ = X & the charact of b₂ = <*((0 -tuples_on X) --> x),((1 -tuples_on X) --> x),((2 -tuples_on X) --> x)*> & the reduction of b₂ = nabla X holds
b₁ = b₂ ;
existence
ex b₁ being non empty non-empty strict TRSStr st
( the carrier of b₁ = X & the charact of b₁ = <*((0 -tuples_on X) --> x),((1 -tuples_on X) --> x),((2 -tuples_on X) --> x)*> & the reduction of b₁ = 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 b₃ being non empty non-empty strict TRSStr holds
( b₃ = TotalTRS (X,x) iff ( the carrier of b₃ = X & the charact of b₃ = <*((0 -tuples_on X) --> x),((1 -tuples_on X) --> x),((2 -tuples_on X) --> x)*> & the reduction of b₃ = nabla X ) );

registration

let X be non empty set ;
let x be Element of X;

cluster TotalTRS (X,x) -> non empty partial quasi_total non-empty strict Group-like invariant ;

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

cluster non empty partial quasi_total non-empty strict Group-like invariant for TRSStr ;

existence
ex b₁ being non empty non-empty TRSStr st
( b₁ is strict & b₁ is quasi_total & b₁ is partial & b₁ is Group-like & b₁ 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;