:: by Grzegorz Bancerek

::

:: Received March 31, 2014

:: Copyright (c) 2014-2018 Association of Mizar Users

definition

attr c_{1} is strict ;

struct ARS -> 1-sorted ;

aggr ARS(# carrier, reduction #) -> ARS ;

sel reduction c_{1} -> Relation of the carrier of c_{1};

end;
struct ARS -> 1-sorted ;

aggr ARS(# carrier, reduction #) -> ARS ;

sel reduction c

registration
end;

registration
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 );

for X being ARS

for x, y being Element of X holds

( x ==> y iff [x,y] in the reduction of X );

definition

let X be ARS ;

let x, y be Element of X;

reflexivity

for x being Element of X holds

( x = x or x ==> x ) ;

reflexivity

for x being Element of X holds the reduction of X reduces x,x by REWRITE1:12;

end;
let x, y be Element of X;

reflexivity

for x being Element of X holds

( x = x or x ==> x ) ;

reflexivity

for x being Element of X holds the reduction of X reduces x,x by REWRITE1:12;

:: 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 ) );

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 );

for X being ARS

for x, y being Element of X holds

( x =*=> y iff the reduction of X reduces x,y );

:: 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 ) );

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 ) )

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;
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;

definition

let X be ARS ;

let x, y be Element of X;

symmetry

for x, y being Element of X holds

( ( not x ==> y & not x <== y ) or y ==> x or y <== x ) ;

end;
let x, y be Element of X;

symmetry

for x, y being Element of X holds

( ( not x ==> y & not x <== y ) or y ==> x or y <== x ) ;

:: 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 ) );

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 ~) )

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;

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 ) ;

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;
let x, y be Element of X;

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 ) ;

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;

:: 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 ) );

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 );

for X being ARS

for x, y being Element of X holds

( x <=*=> y iff x,y are_convertible_wrt the reduction of X );

definition

let X be ARS ;

let x, y be Element of X;

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 )

end;
let x, y be Element of X;

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;

:: 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 ) );

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 ) )

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 :: ABSRED_0:26

theorem :: ABSRED_0:27

theorem :: ABSRED_0:28

theorem :: ABSRED_0:29

theorem :: ABSRED_0:32

theorem :: ABSRED_0:33

theorem :: ABSRED_0:34

theorem :: ABSRED_0:35

theorem :: ABSRED_0:41

theorem :: ABSRED_0:43

theorem :: ABSRED_0:45

theorem :: ABSRED_0:48

theorem :: ABSRED_0:50

theorem :: ABSRED_0:53

theorem :: ABSRED_0:54

theorem :: ABSRED_0:55

theorem :: ABSRED_0:58

theorem :: ABSRED_0:64

theorem :: ABSRED_0:72

theorem :: ABSRED_0:78

theorem :: ABSRED_0:79

theorem :: ABSRED_0:80

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

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

y ==> x ) holds

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

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

x ==> z ) holds

for x, y being Element of X st x =+=> y holds

x ==> y

proof end;

definition

ex b_{1} being strict ARS st

( the carrier of b_{1} = {0,1} & the reduction of b_{1} = [:{0},{0,1}:] )

for b_{1}, b_{2} being strict ARS st the carrier of b_{1} = {0,1} & the reduction of b_{1} = [:{0},{0,1}:] & the carrier of b_{2} = {0,1} & the reduction of b_{2} = [:{0},{0,1}:] holds

b_{1} = b_{2}
;

ex b_{1} being strict ARS st

( the carrier of b_{1} = {0,1,2} & the reduction of b_{1} = [:{0},{0,1,2}:] )

for b_{1}, b_{2} being strict ARS st the carrier of b_{1} = {0,1,2} & the reduction of b_{1} = [:{0},{0,1,2}:] & the carrier of b_{2} = {0,1,2} & the reduction of b_{2} = [:{0},{0,1,2}:] holds

b_{1} = b_{2}
;

end;

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 ( the carrier of it = {0,1} & the reduction of it = [:{0},{0,1}:] );

ex b

( the carrier of b

proof end;

uniqueness for 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 ( the carrier of it = {0,1,2} & the reduction of it = [:{0},{0,1,2}:] );

ex b

( the carrier of b

proof end;

uniqueness for b

b

:: deftheorem Def18 defines ARS_01 ABSRED_0:def 9 :

for b_{1} being strict ARS holds

( b_{1} = ARS_01 iff ( the carrier of b_{1} = {0,1} & the reduction of b_{1} = [:{0},{0,1}:] ) );

for b

( b

:: deftheorem Def19 defines ARS_02 ABSRED_0:def 10 :

for b_{1} being strict ARS holds

( b_{1} = ARS_02 iff ( the carrier of b_{1} = {0,1,2} & the reduction of b_{1} = [:{0},{0,1,2}:] ) );

for b

( b

:: 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 );

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 )

for x being Element of X holds

( x is normform iff x is_a_normal_form_wrt the reduction of X )

proof 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 ) );

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 )

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;

:: 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 );

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 )

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 ;

end;
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);

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;

for x, y, z being Element of X st y is_normform_of x & z is_normform_of x holds

y = z;

:: 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 );

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) );

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 );

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 );

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 );

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 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 ) ) ) ) )

( 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;

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 ;

existence

ex b_{1} being Element of X st b_{1} is_normform_of x
by A;

uniqueness

for b_{1}, b_{2} being Element of X st b_{1} is_normform_of x & b_{2} is_normform_of x holds

b_{1} = b_{2}
by B;

end;
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 ;

existence

ex b

uniqueness

for b

b

:: 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_{3} being Element of X holds

( b_{3} = nf x iff b_{3} is_normform_of x );

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

( b

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)

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 :: ABSRED_0:103

theorem :: ABSRED_0:104

theorem :: ABSRED_0:105

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;

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;

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;

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 ;

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 ;

coherence

for b_{1} being Element of X st b_{1} is normform holds

b_{1} is normalizable

end;
coherence

for b

b

proof 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;

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 )

( 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 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 )

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;

registration

coherence

for b_{1} being ARS st b_{1} is N.F. holds

b_{1} is UN*

for b_{1} being ARS st b_{1} is N.F. holds

b_{1} is UN
by LemN1;

coherence

for b_{1} being ARS st b_{1} is UN holds

b_{1} is UN*

end;
for b

b

proof end;

coherence for b

b

coherence

for b

b

proof 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

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

coherence

for b_{1} being ARS st b_{1} is WN & b_{1} is UN* holds

b_{1} is N.F.
by LemN12;

coherence

for b_{1} being ARS st b_{1} is WN & b_{1} is UN* holds

b_{1} is UN
;

end;
for b

b

coherence

for b

b

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

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 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

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;

definition

let X be ARS ;

let x, y be Element of X;

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 ) ;

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 ) ;

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 ) ;

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;
let x, y be Element of X;

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 ) ;

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 ) ;

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 ) ;

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 ) ;

:: 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 ) );

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 ) );

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 ) );

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 ) );

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 )

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 )

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 )

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 )

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 ;

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 );

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 );

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 );

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 );

for X being ARS holds

( X is WCR iff for x, y being Element of X st x <<01>> y holds

x >><< y );

:: deftheorem defines COMP ABSRED_0:def 28 :

for X being ARS holds

( X is COMP iff ( X is SN & X is CONF ) );

for X being ARS holds

( X is COMP iff ( X is SN & X is CONF ) );

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;

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 )

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 )

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;

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 )

ex x, y, z being Element of X st

( y is_normform_of x & z is_normform_of x & y <> z )

proof end;

registration
end;

registration
end;

registration

coherence

for b_{1} being ARS st b_{1} is SN & b_{1} is CR holds

b_{1} is COMP
;

coherence

for b_{1} being ARS st b_{1} is COMP holds

( b_{1} is CR & b_{1} is WCR & b_{1} is N.F. & b_{1} is UN & b_{1} is UN* & b_{1} is WN )
;

end;
for b

b

coherence

for b

( b

theorem :: ABSRED_0:158

registration

coherence

for b_{1} being ARS st b_{1} is WN & b_{1} is UN* holds

b_{1} is CR
;

coherence

for b_{1} being ARS st b_{1} is SN & b_{1} is UN* holds

b_{1} is COMP
;

end;
for b

b

coherence

for b

b

definition

attr c_{1} is strict ;

struct TRSStr -> ARS , UAStr ;

aggr TRSStr(# carrier, charact, reduction #) -> TRSStr ;

end;
struct TRSStr -> ARS , UAStr ;

aggr TRSStr(# carrier, charact, reduction #) -> TRSStr ;

registration

existence

ex b_{1} being TRSStr st

( not b_{1} is empty & b_{1} is non-empty & b_{1} is strict )

end;
ex b

( not b

proof end;

definition

let S be non empty UAStr ;

end;
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 ) ) ) );

( 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 ) ) ) );

:: 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 ) ) ) ) );

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

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 )

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

end;
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;

registration

let S be non empty non-empty UAStr ;

coherence

for b_{1} being operation of S holds not b_{1} is empty
by RELAT_1:def 9;

let o be operation of S;

coherence

for b_{1} being Element of dom o holds

( b_{1} is Relation-like & b_{1} is Function-like )

end;
coherence

for b

let o be operation of S;

coherence

for b

( b

proof end;

registration

let S be non empty partial non-empty UAStr ;

coherence

for b_{1} being operation of S holds b_{1} is homogeneous

end;
coherence

for b

proof end;

registration

let S be non empty quasi_total non-empty UAStr ;

coherence

for b_{1} being operation of S holds b_{1} is quasi_total

end;
coherence

for b

proof 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 )

( 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 )

( 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;

:: 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 );

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 );

:: 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 );

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 )

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;

coherence

not TRSStr(# X,O,r #) is empty ;

end;
let O be PFuncFinSequence of X;

let r be Relation of X;

coherence

not TRSStr(# X,O,r #) is empty ;

registration

let X be non empty set ;

let O be non-empty non empty PFuncFinSequence of X;

let r be Relation of X;

coherence

TRSStr(# X,O,r #) is non-empty

end;
let O be non-empty non empty PFuncFinSequence of X;

let r be Relation of X;

coherence

TRSStr(# X,O,r #) is non-empty

proof end;

definition

let X be non empty set ;

let x be Element of X;

for b_{1}, b_{2} being non empty non-empty strict TRSStr st the carrier of b_{1} = X & the charact of b_{1} = <*((0 -tuples_on X) --> x),((1 -tuples_on X) --> x),((2 -tuples_on X) --> x)*> & the reduction of b_{1} = nabla X & the carrier of b_{2} = X & the charact of b_{2} = <*((0 -tuples_on X) --> x),((1 -tuples_on X) --> x),((2 -tuples_on X) --> x)*> & the reduction of b_{2} = nabla X holds

b_{1} = b_{2}
;

existence

ex b_{1} being non empty non-empty strict TRSStr st

( the carrier of b_{1} = X & the charact of b_{1} = <*((0 -tuples_on X) --> x),((1 -tuples_on X) --> x),((2 -tuples_on X) --> x)*> & the reduction of b_{1} = nabla X )

end;
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 ( 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 );

for b

b

existence

ex b

( the carrier of b

proof end;

:: deftheorem DEF3 defines TotalTRS ABSRED_0:def 32 :

for X being non empty set

for x being Element of X

for b_{3} being non empty non-empty strict TRSStr holds

( b_{3} = TotalTRS (X,x) iff ( the carrier of b_{3} = X & the charact of b_{3} = <*((0 -tuples_on X) --> x),((1 -tuples_on X) --> x),((2 -tuples_on X) --> x)*> & the reduction of b_{3} = nabla X ) );

for X being non empty set

for x being Element of X

for b

( b

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 )

end;
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;

registration

existence

ex b_{1} being non empty non-empty TRSStr st

( b_{1} is strict & b_{1} is quasi_total & b_{1} is partial & b_{1} is Group-like & b_{1} is invariant )

end;
ex b

( b

proof end;

definition

let S be non empty partial quasi_total non-empty Group-like TRSStr ;

coherence

(Den ((In (1,(dom the charact of S))),S)) . {} is Element of S

(Den ((In (2,(dom the charact of S))),S)) . <*a*> is Element of S

(Den ((In (3,(dom the charact of S))),S)) . <*a,b*> is Element of S

end;
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*>;

(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*>;

(Den ((In (3,(dom the charact of S))),S)) . <*a,b*> is Element of S

proof 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)) . {};

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*>;

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*>;

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 "

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

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

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 ;

end;
attr S is (R3) means :: ABSRED_0:def 38

for a, b, c being Element of S holds (a * b) * c ==> a * (b * c);

for a, b, c being Element of S holds (a * b) * c ==> a * (b * c);

attr S is (R13) means :: ABSRED_0:def 48

for a, b being Element of S holds a * (b * ((a * b) ")) ==> 1. S;

for a, b being Element of S holds a * (b * ((a * b) ")) ==> 1. S;

:: 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 );

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 );

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) );

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 );

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 );

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 );

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 );

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 );

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 );

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 );

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 );

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 );

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 );

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 " );

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 ") );

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

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

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

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

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

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

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

(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

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

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

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 "

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 ")

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

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

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

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

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 "

for a, b being Element of S st S is (R12) & S is (R15) holds

a * ((b * a) ") =*=> b "

proof end;

:: x =+=> y implies x =*=> y;

:: x =+=> y & y =*=> z implies x =+=> z;

:: x =*=> y & y =+=> z implies x =+=> z;