:: ALGSTR_0 semantic presentation

begin

definition
attr c1 is strict ;
struct addMagma -> ( ( ) ( ) 1-sorted ) ;
aggr addMagma(# carrier, addF #) -> ( ( strict ) ( strict ) addMagma ) ;
sel addF c1 -> ( ( V6() V18([: the carrier of c1 : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) , the carrier of c1 : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of c1 : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) ) ) ( V6() V18([: the carrier of c1 : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) , the carrier of c1 : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of c1 : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) ) ) BinOp of the carrier of c1 : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) ) ;
end;

registration
let D be ( ( non empty ) ( non empty ) set ) ;
let o be ( ( V6() V18([:D : ( ( non empty ) ( non empty ) set ) ,D : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,D : ( ( non empty ) ( non empty ) set ) ) ) ( V6() V18([:D : ( ( non empty ) ( non empty ) set ) ,D : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,D : ( ( non empty ) ( non empty ) set ) ) ) BinOp of D : ( ( non empty ) ( non empty ) set ) ) ;
cluster addMagma(# D : ( ( non empty ) ( non empty ) set ) ,o : ( ( V6() V18([:D : ( ( non empty ) ( non empty ) set ) ,D : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,D : ( ( non empty ) ( non empty ) set ) ) ) ( V6() V18([:D : ( ( non empty ) ( non empty ) set ) ,D : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,D : ( ( non empty ) ( non empty ) set ) ) ) Element of bool [:[:D : ( ( non empty ) ( non empty ) set ) ,D : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,D : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) #) : ( ( strict ) ( strict ) addMagma ) -> non empty strict ;
end;

registration
let T be ( ( trivial ) ( trivial ) set ) ;
let f be ( ( V6() V18([:T : ( ( trivial ) ( trivial ) set ) ,T : ( ( trivial ) ( trivial ) set ) :] : ( ( ) ( ) set ) ,T : ( ( trivial ) ( trivial ) set ) ) ) ( V6() V18([:T : ( ( trivial ) ( trivial ) set ) ,T : ( ( trivial ) ( trivial ) set ) :] : ( ( ) ( ) set ) ,T : ( ( trivial ) ( trivial ) set ) ) ) BinOp of T : ( ( trivial ) ( trivial ) set ) ) ;
cluster addMagma(# T : ( ( trivial ) ( trivial ) set ) ,f : ( ( V6() V18([:T : ( ( trivial ) ( trivial ) set ) ,T : ( ( trivial ) ( trivial ) set ) :] : ( ( ) ( ) set ) ,T : ( ( trivial ) ( trivial ) set ) ) ) ( V6() V18([:T : ( ( trivial ) ( trivial ) set ) ,T : ( ( trivial ) ( trivial ) set ) :] : ( ( ) ( ) set ) ,T : ( ( trivial ) ( trivial ) set ) ) ) Element of bool [:[:T : ( ( trivial ) ( trivial ) set ) ,T : ( ( trivial ) ( trivial ) set ) :] : ( ( ) ( ) set ) ,T : ( ( trivial ) ( trivial ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) #) : ( ( strict ) ( strict ) addMagma ) -> trivial strict ;
end;

registration
let N be ( ( non trivial ) ( non empty non trivial ) set ) ;
let b be ( ( V6() V18([:N : ( ( non trivial ) ( non empty non trivial ) set ) ,N : ( ( non trivial ) ( non empty non trivial ) set ) :] : ( ( ) ( ) set ) ,N : ( ( non trivial ) ( non empty non trivial ) set ) ) ) ( V6() V18([:N : ( ( non trivial ) ( non empty non trivial ) set ) ,N : ( ( non trivial ) ( non empty non trivial ) set ) :] : ( ( ) ( ) set ) ,N : ( ( non trivial ) ( non empty non trivial ) set ) ) ) BinOp of N : ( ( non trivial ) ( non empty non trivial ) set ) ) ;
cluster addMagma(# N : ( ( non trivial ) ( non empty non trivial ) set ) ,b : ( ( V6() V18([:N : ( ( non trivial ) ( non empty non trivial ) set ) ,N : ( ( non trivial ) ( non empty non trivial ) set ) :] : ( ( ) ( ) set ) ,N : ( ( non trivial ) ( non empty non trivial ) set ) ) ) ( V6() V18([:N : ( ( non trivial ) ( non empty non trivial ) set ) ,N : ( ( non trivial ) ( non empty non trivial ) set ) :] : ( ( ) ( ) set ) ,N : ( ( non trivial ) ( non empty non trivial ) set ) ) ) Element of bool [:[:N : ( ( non trivial ) ( non empty non trivial ) set ) ,N : ( ( non trivial ) ( non empty non trivial ) set ) :] : ( ( ) ( ) set ) ,N : ( ( non trivial ) ( non empty non trivial ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) #) : ( ( strict ) ( non empty strict ) addMagma ) -> non trivial strict ;
end;

definition
let M be ( ( ) ( ) addMagma ) ;
let x, y be ( ( ) ( ) Element of ( ( ) ( ) set ) ) ;
func x + y -> ( ( ) ( ) Element of ( ( ) ( ) set ) ) equals :: ALGSTR_0:def 1
 the addF of M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) : ( ( V6() V18([: the carrier of M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) : ( ( ) ( ) set ) , the carrier of M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) : ( ( ) ( ) set ) ) ) ( V6() V18([: the carrier of M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) : ( ( ) ( ) set ) , the carrier of M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) : ( ( ) ( ) set ) ) ) BinOp of the carrier of M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) : ( ( ) ( ) set ) ) . (x : ( ( V6() V18([:M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ) ) ( V6() V18([:M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ) ) Element of bool [:[:M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,y : ( ( ) ( V24() V25() V26() ) Element of M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ) ) : ( ( ) ( ) Element of the carrier of M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) : ( ( ) ( ) set ) ) ;
end;

definition
func Trivial-addMagma -> ( ( ) ( ) addMagma ) equals :: ALGSTR_0:def 2
 addMagma(# 1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) ,op2 : ( ( V6() V18([:1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) ,1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) :] : ( ( ) ( ) set ) ,1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) ) ) ( V6() V18([:1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) ,1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) :] : ( ( ) ( ) set ) ,1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) ) ) Element of bool [:[:1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) ,1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) :] : ( ( ) ( ) set ) ,1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) #) : ( ( strict ) ( non empty strict ) addMagma ) ;
end;

registration
cluster Trivial-addMagma : ( ( ) ( ) addMagma ) -> 1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) -element strict ;
end;

registration
cluster 1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) -element strict for ( ( ) ( ) addMagma ) ;
end;

definition
let M be ( ( ) ( ) addMagma ) ;
let x be ( ( ) ( ) Element of ( ( ) ( ) set ) ) ;
attr x is left_add-cancelable means :: ALGSTR_0:def 3
 for y, z being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st x : ( ( V6() V18([:M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ) ) ( V6() V18([:M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ) ) Element of bool [:[:M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) + y : ( ( ) ( ) Element of ( ( ) ( ) set ) ) : ( ( ) ( ) Element of ( ( ) ( ) set ) ) = x : ( ( V6() V18([:M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ) ) ( V6() V18([:M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ) ) Element of bool [:[:M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) + z : ( ( ) ( ) Element of ( ( ) ( ) set ) ) : ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds
y : ( ( ) ( ) Element of ( ( ) ( ) set ) ) = z : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ;
attr x is right_add-cancelable means :: ALGSTR_0:def 4
 for y, z being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st y : ( ( ) ( ) Element of ( ( ) ( ) set ) ) + x : ( ( V6() V18([:M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ) ) ( V6() V18([:M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ) ) Element of bool [:[:M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of ( ( ) ( ) set ) ) = z : ( ( ) ( ) Element of ( ( ) ( ) set ) ) + x : ( ( V6() V18([:M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ) ) ( V6() V18([:M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ) ) Element of bool [:[:M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds
y : ( ( ) ( ) Element of ( ( ) ( ) set ) ) = z : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ;
end;

definition
let M be ( ( ) ( ) addMagma ) ;
let x be ( ( ) ( ) Element of ( ( ) ( ) set ) ) ;
attr x is add-cancelable means :: ALGSTR_0:def 5
( x : ( ( V6() V18([:M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ) ) ( V6() V18([:M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ) ) Element of bool [:[:M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) is right_add-cancelable & x : ( ( V6() V18([:M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ) ) ( V6() V18([:M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ) ) Element of bool [:[:M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) is left_add-cancelable );
end;

registration
let M be ( ( ) ( ) addMagma ) ;
cluster left_add-cancelable right_add-cancelable -> add-cancelable for ( ( ) ( ) Element of the carrier of M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) : ( ( ) ( ) set ) ) ;
cluster add-cancelable -> left_add-cancelable right_add-cancelable for ( ( ) ( ) Element of the carrier of M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) : ( ( ) ( ) set ) ) ;
end;

definition
let M be ( ( ) ( ) addMagma ) ;
attr M is left_add-cancelable means :: ALGSTR_0:def 6
 for x being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is left_add-cancelable ;
attr M is right_add-cancelable means :: ALGSTR_0:def 7
 for x being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is right_add-cancelable ;
end;

definition
let M be ( ( ) ( ) addMagma ) ;
attr M is add-cancelable means :: ALGSTR_0:def 8
( M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) is right_add-cancelable & M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) is left_add-cancelable );
end;

registration
cluster left_add-cancelable right_add-cancelable -> add-cancelable for ( ( ) ( ) addMagma ) ;
cluster add-cancelable -> left_add-cancelable right_add-cancelable for ( ( ) ( ) addMagma ) ;
end;

registration
cluster Trivial-addMagma : ( ( ) ( non empty trivial V46() 1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) -element strict ) addMagma ) -> add-cancelable ;
end;

registration
cluster 1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) -element strict add-cancelable for ( ( ) ( ) addMagma ) ;
end;

registration
let M be ( ( left_add-cancelable ) ( left_add-cancelable ) addMagma ) ;
cluster -> left_add-cancelable for ( ( ) ( ) Element of the carrier of M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) : ( ( ) ( ) set ) ) ;
end;

registration
let M be ( ( right_add-cancelable ) ( right_add-cancelable ) addMagma ) ;
cluster -> right_add-cancelable for ( ( ) ( ) Element of the carrier of M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) : ( ( ) ( ) set ) ) ;
end;

definition
attr c1 is strict ;
struct addLoopStr -> ( ( ) ( ) ZeroStr ) , ( ( ) ( ) addMagma ) ;
aggr addLoopStr(# carrier, addF, ZeroF #) -> ( ( strict ) ( strict ) addLoopStr ) ;
end;

registration
let D be ( ( non empty ) ( non empty ) set ) ;
let o be ( ( V6() V18([:D : ( ( non empty ) ( non empty ) set ) ,D : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,D : ( ( non empty ) ( non empty ) set ) ) ) ( V6() V18([:D : ( ( non empty ) ( non empty ) set ) ,D : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,D : ( ( non empty ) ( non empty ) set ) ) ) BinOp of D : ( ( non empty ) ( non empty ) set ) ) ;
let d be ( ( ) ( ) Element of D : ( ( non empty ) ( non empty ) set ) ) ;
cluster addLoopStr(# D : ( ( non empty ) ( non empty ) set ) ,o : ( ( V6() V18([:D : ( ( non empty ) ( non empty ) set ) ,D : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,D : ( ( non empty ) ( non empty ) set ) ) ) ( V6() V18([:D : ( ( non empty ) ( non empty ) set ) ,D : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,D : ( ( non empty ) ( non empty ) set ) ) ) Element of bool [:[:D : ( ( non empty ) ( non empty ) set ) ,D : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,D : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,d : ( ( ) ( ) Element of D : ( ( non empty ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) addLoopStr ) -> non empty strict ;
end;

registration
let T be ( ( trivial ) ( trivial ) set ) ;
let f be ( ( V6() V18([:T : ( ( trivial ) ( trivial ) set ) ,T : ( ( trivial ) ( trivial ) set ) :] : ( ( ) ( ) set ) ,T : ( ( trivial ) ( trivial ) set ) ) ) ( V6() V18([:T : ( ( trivial ) ( trivial ) set ) ,T : ( ( trivial ) ( trivial ) set ) :] : ( ( ) ( ) set ) ,T : ( ( trivial ) ( trivial ) set ) ) ) BinOp of T : ( ( trivial ) ( trivial ) set ) ) ;
let t be ( ( ) ( ) Element of T : ( ( trivial ) ( trivial ) set ) ) ;
cluster addLoopStr(# T : ( ( trivial ) ( trivial ) set ) ,f : ( ( V6() V18([:T : ( ( trivial ) ( trivial ) set ) ,T : ( ( trivial ) ( trivial ) set ) :] : ( ( ) ( ) set ) ,T : ( ( trivial ) ( trivial ) set ) ) ) ( V6() V18([:T : ( ( trivial ) ( trivial ) set ) ,T : ( ( trivial ) ( trivial ) set ) :] : ( ( ) ( ) set ) ,T : ( ( trivial ) ( trivial ) set ) ) ) Element of bool [:[:T : ( ( trivial ) ( trivial ) set ) ,T : ( ( trivial ) ( trivial ) set ) :] : ( ( ) ( ) set ) ,T : ( ( trivial ) ( trivial ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,t : ( ( ) ( ) Element of T : ( ( trivial ) ( trivial ) set ) ) #) : ( ( strict ) ( strict ) addLoopStr ) -> trivial strict ;
end;

registration
let N be ( ( non trivial ) ( non empty non trivial ) set ) ;
let b be ( ( V6() V18([:N : ( ( non trivial ) ( non empty non trivial ) set ) ,N : ( ( non trivial ) ( non empty non trivial ) set ) :] : ( ( ) ( ) set ) ,N : ( ( non trivial ) ( non empty non trivial ) set ) ) ) ( V6() V18([:N : ( ( non trivial ) ( non empty non trivial ) set ) ,N : ( ( non trivial ) ( non empty non trivial ) set ) :] : ( ( ) ( ) set ) ,N : ( ( non trivial ) ( non empty non trivial ) set ) ) ) BinOp of N : ( ( non trivial ) ( non empty non trivial ) set ) ) ;
let m be ( ( ) ( ) Element of N : ( ( non trivial ) ( non empty non trivial ) set ) ) ;
cluster addLoopStr(# N : ( ( non trivial ) ( non empty non trivial ) set ) ,b : ( ( V6() V18([:N : ( ( non trivial ) ( non empty non trivial ) set ) ,N : ( ( non trivial ) ( non empty non trivial ) set ) :] : ( ( ) ( ) set ) ,N : ( ( non trivial ) ( non empty non trivial ) set ) ) ) ( V6() V18([:N : ( ( non trivial ) ( non empty non trivial ) set ) ,N : ( ( non trivial ) ( non empty non trivial ) set ) :] : ( ( ) ( ) set ) ,N : ( ( non trivial ) ( non empty non trivial ) set ) ) ) Element of bool [:[:N : ( ( non trivial ) ( non empty non trivial ) set ) ,N : ( ( non trivial ) ( non empty non trivial ) set ) :] : ( ( ) ( ) set ) ,N : ( ( non trivial ) ( non empty non trivial ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,m : ( ( ) ( ) Element of N : ( ( non trivial ) ( non empty non trivial ) set ) ) #) : ( ( strict ) ( non empty strict ) addLoopStr ) -> non trivial strict ;
end;

definition
func Trivial-addLoopStr -> ( ( ) ( ) addLoopStr ) equals :: ALGSTR_0:def 9
 addLoopStr(# 1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) ,op2 : ( ( V6() V18([:1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) ,1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) :] : ( ( ) ( ) set ) ,1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) ) ) ( V6() V18([:1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) ,1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) :] : ( ( ) ( ) set ) ,1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) ) ) Element of bool [:[:1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) ,1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) :] : ( ( ) ( ) set ) ,1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,op0 : ( ( ) ( V24() V25() V26() ) Element of 1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) ) #) : ( ( strict ) ( non empty strict ) addLoopStr ) ;
end;

registration
cluster Trivial-addLoopStr : ( ( ) ( ) addLoopStr ) -> 1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) -element strict ;
end;

registration
cluster 1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) -element strict for ( ( ) ( ) addLoopStr ) ;
end;

definition
let M be ( ( ) ( ) addLoopStr ) ;
let x be ( ( ) ( ) Element of ( ( ) ( ) set ) ) ;
attr x is left_complementable means :: ALGSTR_0:def 10
 ex y being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st y : ( ( ) ( ) Element of ( ( ) ( ) set ) ) + x : ( ( V6() V18([:M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ) ) ( V6() V18([:M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ) ) Element of bool [:[:M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of ( ( ) ( ) set ) ) = 0. M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) : ( ( ) ( ) Element of the carrier of M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) : ( ( ) ( ) set ) ) ;
attr x is right_complementable means :: ALGSTR_0:def 11
 ex y being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st x : ( ( V6() V18([:M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ) ) ( V6() V18([:M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ) ) Element of bool [:[:M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) + y : ( ( ) ( ) Element of ( ( ) ( ) set ) ) : ( ( ) ( ) Element of ( ( ) ( ) set ) ) = 0. M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) : ( ( ) ( ) Element of the carrier of M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) : ( ( ) ( ) set ) ) ;
end;

definition
let M be ( ( ) ( ) addLoopStr ) ;
let x be ( ( ) ( ) Element of ( ( ) ( ) set ) ) ;
attr x is complementable means :: ALGSTR_0:def 12
( x : ( ( V6() V18([:M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ) ) ( V6() V18([:M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ) ) Element of bool [:[:M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) is right_complementable & x : ( ( V6() V18([:M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ) ) ( V6() V18([:M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ) ) Element of bool [:[:M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) is left_complementable );
end;

registration
let M be ( ( ) ( ) addLoopStr ) ;
cluster left_complementable right_complementable -> complementable for ( ( ) ( ) Element of the carrier of M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) : ( ( ) ( ) set ) ) ;
cluster complementable -> left_complementable right_complementable for ( ( ) ( ) Element of the carrier of M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) : ( ( ) ( ) set ) ) ;
end;

definition
let M be ( ( ) ( ) addLoopStr ) ;
let x be ( ( ) ( ) Element of ( ( ) ( ) set ) ) ;
assume ( x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is left_complementable & x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is right_add-cancelable ) ;
func - x -> ( ( ) ( ) Element of ( ( ) ( ) set ) ) means :: ALGSTR_0:def 13
it : ( ( ) ( V24() V25() V26() ) Element of M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ) + x : ( ( V6() V18([:M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ) ) ( V6() V18([:M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ) ) Element of bool [:[:M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of ( ( ) ( ) set ) ) = 0. M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) : ( ( ) ( ) Element of the carrier of M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) : ( ( ) ( ) set ) ) ;
end;

definition
let V be ( ( ) ( ) addLoopStr ) ;
let v, w be ( ( ) ( ) Element of ( ( ) ( ) set ) ) ;
func v - w -> ( ( ) ( ) Element of ( ( ) ( ) set ) ) equals :: ALGSTR_0:def 14
v : ( ( V6() V18([:V : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ,V : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) ,V : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ) ) ( V6() V18([:V : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ,V : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) ,V : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ) ) Element of bool [:[:V : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ,V : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) ,V : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) + (- w : ( ( ) ( V24() V25() V26() ) Element of V : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( ) set ) ) : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ;
end;

registration
cluster Trivial-addLoopStr : ( ( ) ( non empty trivial V46() 1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) -element strict ) addLoopStr ) -> add-cancelable ;
end;

definition
let M be ( ( ) ( ) addLoopStr ) ;
attr M is left_complementable means :: ALGSTR_0:def 15
 for x being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is left_complementable ;
attr M is right_complementable means :: ALGSTR_0:def 16
 for x being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is right_complementable ;
end;

definition
let M be ( ( ) ( ) addLoopStr ) ;
attr M is complementable means :: ALGSTR_0:def 17
( M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) is right_complementable & M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) is left_complementable );
end;

registration
cluster left_complementable right_complementable -> complementable for ( ( ) ( ) addLoopStr ) ;
cluster complementable -> left_complementable right_complementable for ( ( ) ( ) addLoopStr ) ;
end;

registration
cluster Trivial-addLoopStr : ( ( ) ( non empty trivial V46() 1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) -element left_add-cancelable right_add-cancelable add-cancelable strict ) addLoopStr ) -> complementable ;
end;

registration
cluster 1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) -element add-cancelable strict complementable for ( ( ) ( ) addLoopStr ) ;
end;

registration
let M be ( ( left_complementable ) ( left_complementable ) addLoopStr ) ;
cluster -> left_complementable for ( ( ) ( ) Element of the carrier of M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) : ( ( ) ( ) set ) ) ;
end;

registration
let M be ( ( right_complementable ) ( right_complementable ) addLoopStr ) ;
cluster -> right_complementable for ( ( ) ( ) Element of the carrier of M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) : ( ( ) ( ) set ) ) ;
end;

begin

definition
attr c1 is strict ;
struct multMagma -> ( ( ) ( ) 1-sorted ) ;
aggr multMagma(# carrier, multF #) -> ( ( strict ) ( strict ) multMagma ) ;
sel multF c1 -> ( ( V6() V18([: the carrier of c1 : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) : ( ( ) ( ) set ) , the carrier of c1 : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of c1 : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) : ( ( ) ( ) set ) ) ) ( V6() V18([: the carrier of c1 : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) : ( ( ) ( ) set ) , the carrier of c1 : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of c1 : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) : ( ( ) ( ) set ) ) ) BinOp of the carrier of c1 : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) : ( ( ) ( ) set ) ) ;
end;

registration
let D be ( ( non empty ) ( non empty ) set ) ;
let o be ( ( V6() V18([:D : ( ( non empty ) ( non empty ) set ) ,D : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,D : ( ( non empty ) ( non empty ) set ) ) ) ( V6() V18([:D : ( ( non empty ) ( non empty ) set ) ,D : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,D : ( ( non empty ) ( non empty ) set ) ) ) BinOp of D : ( ( non empty ) ( non empty ) set ) ) ;
cluster multMagma(# D : ( ( non empty ) ( non empty ) set ) ,o : ( ( V6() V18([:D : ( ( non empty ) ( non empty ) set ) ,D : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,D : ( ( non empty ) ( non empty ) set ) ) ) ( V6() V18([:D : ( ( non empty ) ( non empty ) set ) ,D : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,D : ( ( non empty ) ( non empty ) set ) ) ) Element of bool [:[:D : ( ( non empty ) ( non empty ) set ) ,D : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,D : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) #) : ( ( strict ) ( strict ) multMagma ) -> non empty strict ;
end;

registration
let T be ( ( trivial ) ( trivial ) set ) ;
let f be ( ( V6() V18([:T : ( ( trivial ) ( trivial ) set ) ,T : ( ( trivial ) ( trivial ) set ) :] : ( ( ) ( ) set ) ,T : ( ( trivial ) ( trivial ) set ) ) ) ( V6() V18([:T : ( ( trivial ) ( trivial ) set ) ,T : ( ( trivial ) ( trivial ) set ) :] : ( ( ) ( ) set ) ,T : ( ( trivial ) ( trivial ) set ) ) ) BinOp of T : ( ( trivial ) ( trivial ) set ) ) ;
cluster multMagma(# T : ( ( trivial ) ( trivial ) set ) ,f : ( ( V6() V18([:T : ( ( trivial ) ( trivial ) set ) ,T : ( ( trivial ) ( trivial ) set ) :] : ( ( ) ( ) set ) ,T : ( ( trivial ) ( trivial ) set ) ) ) ( V6() V18([:T : ( ( trivial ) ( trivial ) set ) ,T : ( ( trivial ) ( trivial ) set ) :] : ( ( ) ( ) set ) ,T : ( ( trivial ) ( trivial ) set ) ) ) Element of bool [:[:T : ( ( trivial ) ( trivial ) set ) ,T : ( ( trivial ) ( trivial ) set ) :] : ( ( ) ( ) set ) ,T : ( ( trivial ) ( trivial ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) #) : ( ( strict ) ( strict ) multMagma ) -> trivial strict ;
end;

registration
let N be ( ( non trivial ) ( non empty non trivial ) set ) ;
let b be ( ( V6() V18([:N : ( ( non trivial ) ( non empty non trivial ) set ) ,N : ( ( non trivial ) ( non empty non trivial ) set ) :] : ( ( ) ( ) set ) ,N : ( ( non trivial ) ( non empty non trivial ) set ) ) ) ( V6() V18([:N : ( ( non trivial ) ( non empty non trivial ) set ) ,N : ( ( non trivial ) ( non empty non trivial ) set ) :] : ( ( ) ( ) set ) ,N : ( ( non trivial ) ( non empty non trivial ) set ) ) ) BinOp of N : ( ( non trivial ) ( non empty non trivial ) set ) ) ;
cluster multMagma(# N : ( ( non trivial ) ( non empty non trivial ) set ) ,b : ( ( V6() V18([:N : ( ( non trivial ) ( non empty non trivial ) set ) ,N : ( ( non trivial ) ( non empty non trivial ) set ) :] : ( ( ) ( ) set ) ,N : ( ( non trivial ) ( non empty non trivial ) set ) ) ) ( V6() V18([:N : ( ( non trivial ) ( non empty non trivial ) set ) ,N : ( ( non trivial ) ( non empty non trivial ) set ) :] : ( ( ) ( ) set ) ,N : ( ( non trivial ) ( non empty non trivial ) set ) ) ) Element of bool [:[:N : ( ( non trivial ) ( non empty non trivial ) set ) ,N : ( ( non trivial ) ( non empty non trivial ) set ) :] : ( ( ) ( ) set ) ,N : ( ( non trivial ) ( non empty non trivial ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) #) : ( ( strict ) ( non empty strict ) multMagma ) -> non trivial strict ;
end;

definition
let M be ( ( ) ( ) multMagma ) ;
let x, y be ( ( ) ( ) Element of ( ( ) ( ) set ) ) ;
func x * y -> ( ( ) ( ) Element of ( ( ) ( ) set ) ) equals :: ALGSTR_0:def 18
 the multF of M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) : ( ( V6() V18([: the carrier of M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) : ( ( ) ( ) set ) , the carrier of M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) : ( ( ) ( ) set ) ) ) ( V6() V18([: the carrier of M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) : ( ( ) ( ) set ) , the carrier of M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) : ( ( ) ( ) set ) ) ) BinOp of the carrier of M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) : ( ( ) ( ) set ) ) . (x : ( ( V6() V18([:M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ) ) ( V6() V18([:M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ) ) Element of bool [:[:M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,y : ( ( ) ( V24() V25() V26() ) Element of M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ) ) : ( ( ) ( ) Element of the carrier of M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) : ( ( ) ( ) set ) ) ;
end;

definition
func Trivial-multMagma -> ( ( ) ( ) multMagma ) equals :: ALGSTR_0:def 19
 multMagma(# 1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) ,op2 : ( ( V6() V18([:1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) ,1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) :] : ( ( ) ( ) set ) ,1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) ) ) ( V6() V18([:1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) ,1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) :] : ( ( ) ( ) set ) ,1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) ) ) Element of bool [:[:1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) ,1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) :] : ( ( ) ( ) set ) ,1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) #) : ( ( strict ) ( non empty strict ) multMagma ) ;
end;

registration
cluster Trivial-multMagma : ( ( ) ( ) multMagma ) -> 1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) -element strict ;
end;

registration
cluster 1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) -element strict for ( ( ) ( ) multMagma ) ;
end;

definition
let M be ( ( ) ( ) multMagma ) ;
let x be ( ( ) ( ) Element of ( ( ) ( ) set ) ) ;
attr x is left_mult-cancelable means :: ALGSTR_0:def 20
 for y, z being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st x : ( ( V6() V18([:M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ) ) ( V6() V18([:M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ) ) Element of bool [:[:M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) * y : ( ( ) ( ) Element of ( ( ) ( ) set ) ) : ( ( ) ( ) Element of ( ( ) ( ) set ) ) = x : ( ( V6() V18([:M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ) ) ( V6() V18([:M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ) ) Element of bool [:[:M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) * z : ( ( ) ( ) Element of ( ( ) ( ) set ) ) : ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds
y : ( ( ) ( ) Element of ( ( ) ( ) set ) ) = z : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ;
attr x is right_mult-cancelable means :: ALGSTR_0:def 21
 for y, z being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st y : ( ( ) ( ) Element of ( ( ) ( ) set ) ) * x : ( ( V6() V18([:M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ) ) ( V6() V18([:M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ) ) Element of bool [:[:M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of ( ( ) ( ) set ) ) = z : ( ( ) ( ) Element of ( ( ) ( ) set ) ) * x : ( ( V6() V18([:M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ) ) ( V6() V18([:M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ) ) Element of bool [:[:M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds
y : ( ( ) ( ) Element of ( ( ) ( ) set ) ) = z : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ;
end;

definition
let M be ( ( ) ( ) multMagma ) ;
let x be ( ( ) ( ) Element of ( ( ) ( ) set ) ) ;
attr x is mult-cancelable means :: ALGSTR_0:def 22
( x : ( ( V6() V18([:M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ) ) ( V6() V18([:M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ) ) Element of bool [:[:M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) is right_mult-cancelable & x : ( ( V6() V18([:M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ) ) ( V6() V18([:M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ) ) Element of bool [:[:M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) is left_mult-cancelable );
end;

registration
let M be ( ( ) ( ) multMagma ) ;
cluster left_mult-cancelable right_mult-cancelable -> mult-cancelable for ( ( ) ( ) Element of the carrier of M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) : ( ( ) ( ) set ) ) ;
cluster mult-cancelable -> left_mult-cancelable right_mult-cancelable for ( ( ) ( ) Element of the carrier of M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) : ( ( ) ( ) set ) ) ;
end;

definition
let M be ( ( ) ( ) multMagma ) ;
attr M is left_mult-cancelable means :: ALGSTR_0:def 23
 for x being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is left_mult-cancelable ;
attr M is right_mult-cancelable means :: ALGSTR_0:def 24
 for x being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is right_mult-cancelable ;
end;

definition
let M be ( ( ) ( ) multMagma ) ;
attr M is mult-cancelable means :: ALGSTR_0:def 25
( M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) is left_mult-cancelable & M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) is right_mult-cancelable );
end;

registration
cluster left_mult-cancelable right_mult-cancelable -> mult-cancelable for ( ( ) ( ) multMagma ) ;
cluster mult-cancelable -> left_mult-cancelable right_mult-cancelable for ( ( ) ( ) multMagma ) ;
end;

registration
cluster Trivial-multMagma : ( ( ) ( non empty trivial V46() 1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) -element strict ) multMagma ) -> mult-cancelable ;
end;

registration
cluster 1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) -element strict mult-cancelable for ( ( ) ( ) multMagma ) ;
end;

registration
let M be ( ( left_mult-cancelable ) ( left_mult-cancelable ) multMagma ) ;
cluster -> left_mult-cancelable for ( ( ) ( ) Element of the carrier of M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) : ( ( ) ( ) set ) ) ;
end;

registration
let M be ( ( right_mult-cancelable ) ( right_mult-cancelable ) multMagma ) ;
cluster -> right_mult-cancelable for ( ( ) ( ) Element of the carrier of M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) : ( ( ) ( ) set ) ) ;
end;

definition
attr c1 is strict ;
struct multLoopStr -> ( ( ) ( ) OneStr ) , ( ( ) ( ) multMagma ) ;
aggr multLoopStr(# carrier, multF, OneF #) -> ( ( strict ) ( strict ) multLoopStr ) ;
end;

registration
let D be ( ( non empty ) ( non empty ) set ) ;
let o be ( ( V6() V18([:D : ( ( non empty ) ( non empty ) set ) ,D : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,D : ( ( non empty ) ( non empty ) set ) ) ) ( V6() V18([:D : ( ( non empty ) ( non empty ) set ) ,D : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,D : ( ( non empty ) ( non empty ) set ) ) ) BinOp of D : ( ( non empty ) ( non empty ) set ) ) ;
let d be ( ( ) ( ) Element of D : ( ( non empty ) ( non empty ) set ) ) ;
cluster multLoopStr(# D : ( ( non empty ) ( non empty ) set ) ,o : ( ( V6() V18([:D : ( ( non empty ) ( non empty ) set ) ,D : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,D : ( ( non empty ) ( non empty ) set ) ) ) ( V6() V18([:D : ( ( non empty ) ( non empty ) set ) ,D : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,D : ( ( non empty ) ( non empty ) set ) ) ) Element of bool [:[:D : ( ( non empty ) ( non empty ) set ) ,D : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,D : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,d : ( ( ) ( ) Element of D : ( ( non empty ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) multLoopStr ) -> non empty strict ;
end;

registration
let T be ( ( trivial ) ( trivial ) set ) ;
let f be ( ( V6() V18([:T : ( ( trivial ) ( trivial ) set ) ,T : ( ( trivial ) ( trivial ) set ) :] : ( ( ) ( ) set ) ,T : ( ( trivial ) ( trivial ) set ) ) ) ( V6() V18([:T : ( ( trivial ) ( trivial ) set ) ,T : ( ( trivial ) ( trivial ) set ) :] : ( ( ) ( ) set ) ,T : ( ( trivial ) ( trivial ) set ) ) ) BinOp of T : ( ( trivial ) ( trivial ) set ) ) ;
let t be ( ( ) ( ) Element of T : ( ( trivial ) ( trivial ) set ) ) ;
cluster multLoopStr(# T : ( ( trivial ) ( trivial ) set ) ,f : ( ( V6() V18([:T : ( ( trivial ) ( trivial ) set ) ,T : ( ( trivial ) ( trivial ) set ) :] : ( ( ) ( ) set ) ,T : ( ( trivial ) ( trivial ) set ) ) ) ( V6() V18([:T : ( ( trivial ) ( trivial ) set ) ,T : ( ( trivial ) ( trivial ) set ) :] : ( ( ) ( ) set ) ,T : ( ( trivial ) ( trivial ) set ) ) ) Element of bool [:[:T : ( ( trivial ) ( trivial ) set ) ,T : ( ( trivial ) ( trivial ) set ) :] : ( ( ) ( ) set ) ,T : ( ( trivial ) ( trivial ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,t : ( ( ) ( ) Element of T : ( ( trivial ) ( trivial ) set ) ) #) : ( ( strict ) ( strict ) multLoopStr ) -> trivial strict ;
end;

registration
let N be ( ( non trivial ) ( non empty non trivial ) set ) ;
let b be ( ( V6() V18([:N : ( ( non trivial ) ( non empty non trivial ) set ) ,N : ( ( non trivial ) ( non empty non trivial ) set ) :] : ( ( ) ( ) set ) ,N : ( ( non trivial ) ( non empty non trivial ) set ) ) ) ( V6() V18([:N : ( ( non trivial ) ( non empty non trivial ) set ) ,N : ( ( non trivial ) ( non empty non trivial ) set ) :] : ( ( ) ( ) set ) ,N : ( ( non trivial ) ( non empty non trivial ) set ) ) ) BinOp of N : ( ( non trivial ) ( non empty non trivial ) set ) ) ;
let m be ( ( ) ( ) Element of N : ( ( non trivial ) ( non empty non trivial ) set ) ) ;
cluster multLoopStr(# N : ( ( non trivial ) ( non empty non trivial ) set ) ,b : ( ( V6() V18([:N : ( ( non trivial ) ( non empty non trivial ) set ) ,N : ( ( non trivial ) ( non empty non trivial ) set ) :] : ( ( ) ( ) set ) ,N : ( ( non trivial ) ( non empty non trivial ) set ) ) ) ( V6() V18([:N : ( ( non trivial ) ( non empty non trivial ) set ) ,N : ( ( non trivial ) ( non empty non trivial ) set ) :] : ( ( ) ( ) set ) ,N : ( ( non trivial ) ( non empty non trivial ) set ) ) ) Element of bool [:[:N : ( ( non trivial ) ( non empty non trivial ) set ) ,N : ( ( non trivial ) ( non empty non trivial ) set ) :] : ( ( ) ( ) set ) ,N : ( ( non trivial ) ( non empty non trivial ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,m : ( ( ) ( ) Element of N : ( ( non trivial ) ( non empty non trivial ) set ) ) #) : ( ( strict ) ( non empty strict ) multLoopStr ) -> non trivial strict ;
end;

definition
func Trivial-multLoopStr -> ( ( ) ( ) multLoopStr ) equals :: ALGSTR_0:def 26
 multLoopStr(# 1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) ,op2 : ( ( V6() V18([:1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) ,1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) :] : ( ( ) ( ) set ) ,1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) ) ) ( V6() V18([:1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) ,1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) :] : ( ( ) ( ) set ) ,1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) ) ) Element of bool [:[:1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) ,1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) :] : ( ( ) ( ) set ) ,1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,op0 : ( ( ) ( V24() V25() V26() ) Element of 1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) ) #) : ( ( strict ) ( non empty strict ) multLoopStr ) ;
end;

registration
cluster Trivial-multLoopStr : ( ( ) ( ) multLoopStr ) -> 1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) -element strict ;
end;

registration
cluster 1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) -element strict for ( ( ) ( ) multLoopStr ) ;
end;

registration
cluster Trivial-multLoopStr : ( ( ) ( non empty trivial V46() 1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) -element strict ) multLoopStr ) -> mult-cancelable ;
end;

definition
let M be ( ( ) ( ) multLoopStr ) ;
let x be ( ( ) ( ) Element of ( ( ) ( ) set ) ) ;
attr x is left_invertible means :: ALGSTR_0:def 27
 ex y being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st y : ( ( ) ( ) Element of ( ( ) ( ) set ) ) * x : ( ( V6() V18([:M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ) ) ( V6() V18([:M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ) ) Element of bool [:[:M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of ( ( ) ( ) set ) ) = 1. M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) : ( ( ) ( ) Element of the carrier of M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) : ( ( ) ( ) set ) ) ;
attr x is right_invertible means :: ALGSTR_0:def 28
 ex y being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st x : ( ( V6() V18([:M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ) ) ( V6() V18([:M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ) ) Element of bool [:[:M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) * y : ( ( ) ( ) Element of ( ( ) ( ) set ) ) : ( ( ) ( ) Element of ( ( ) ( ) set ) ) = 1. M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) : ( ( ) ( ) Element of the carrier of M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) : ( ( ) ( ) set ) ) ;
end;

definition
let M be ( ( ) ( ) multLoopStr ) ;
let x be ( ( ) ( ) Element of ( ( ) ( ) set ) ) ;
attr x is invertible means :: ALGSTR_0:def 29
( x : ( ( V6() V18([:M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ) ) ( V6() V18([:M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ) ) Element of bool [:[:M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) is right_invertible & x : ( ( V6() V18([:M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ) ) ( V6() V18([:M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ) ) Element of bool [:[:M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) is left_invertible );
end;

registration
let M be ( ( ) ( ) multLoopStr ) ;
cluster left_invertible right_invertible -> invertible for ( ( ) ( ) Element of the carrier of M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) : ( ( ) ( ) set ) ) ;
cluster invertible -> left_invertible right_invertible for ( ( ) ( ) Element of the carrier of M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) : ( ( ) ( ) set ) ) ;
end;

definition
let M be ( ( ) ( ) multLoopStr ) ;
let x be ( ( ) ( ) Element of ( ( ) ( ) set ) ) ;
assume ( x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is left_invertible & x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is right_mult-cancelable ) ;
func / x -> ( ( ) ( ) Element of ( ( ) ( ) set ) ) means :: ALGSTR_0:def 30
it : ( ( ) ( V24() V25() V26() ) Element of M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ) * x : ( ( V6() V18([:M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ) ) ( V6() V18([:M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ) ) Element of bool [:[:M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of ( ( ) ( ) set ) ) = 1. M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) : ( ( ) ( ) Element of the carrier of M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) : ( ( ) ( ) set ) ) ;
end;

definition
let M be ( ( ) ( ) multLoopStr ) ;
attr M is left_invertible means :: ALGSTR_0:def 31
 for x being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is left_invertible ;
attr M is right_invertible means :: ALGSTR_0:def 32
 for x being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is right_invertible ;
end;

definition
let M be ( ( ) ( ) multLoopStr ) ;
attr M is invertible means :: ALGSTR_0:def 33
( M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) is right_invertible & M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) is left_invertible );
end;

registration
cluster left_invertible right_invertible -> invertible for ( ( ) ( ) multLoopStr ) ;
cluster invertible -> left_invertible right_invertible for ( ( ) ( ) multLoopStr ) ;
end;

registration
cluster Trivial-multLoopStr : ( ( ) ( non empty trivial V46() 1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) -element left_mult-cancelable right_mult-cancelable mult-cancelable strict ) multLoopStr ) -> invertible ;
end;

registration
cluster 1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) -element mult-cancelable strict invertible for ( ( ) ( ) multLoopStr ) ;
end;

registration
let M be ( ( left_invertible ) ( left_invertible ) multLoopStr ) ;
cluster -> left_invertible for ( ( ) ( ) Element of the carrier of M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) : ( ( ) ( ) set ) ) ;
end;

registration
let M be ( ( right_invertible ) ( right_invertible ) multLoopStr ) ;
cluster -> right_invertible for ( ( ) ( ) Element of the carrier of M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) : ( ( ) ( ) set ) ) ;
end;

begin

definition
attr c1 is strict ;
struct multLoopStr_0 -> ( ( ) ( ) multLoopStr ) , ( ( ) ( ) ZeroOneStr ) ;
aggr multLoopStr_0(# carrier, multF, ZeroF, OneF #) -> ( ( strict ) ( strict ) multLoopStr_0 ) ;
end;

registration
let D be ( ( non empty ) ( non empty ) set ) ;
let o be ( ( V6() V18([:D : ( ( non empty ) ( non empty ) set ) ,D : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,D : ( ( non empty ) ( non empty ) set ) ) ) ( V6() V18([:D : ( ( non empty ) ( non empty ) set ) ,D : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,D : ( ( non empty ) ( non empty ) set ) ) ) BinOp of D : ( ( non empty ) ( non empty ) set ) ) ;
let d, e be ( ( ) ( ) Element of D : ( ( non empty ) ( non empty ) set ) ) ;
cluster multLoopStr_0(# D : ( ( non empty ) ( non empty ) set ) ,o : ( ( V6() V18([:D : ( ( non empty ) ( non empty ) set ) ,D : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,D : ( ( non empty ) ( non empty ) set ) ) ) ( V6() V18([:D : ( ( non empty ) ( non empty ) set ) ,D : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,D : ( ( non empty ) ( non empty ) set ) ) ) Element of bool [:[:D : ( ( non empty ) ( non empty ) set ) ,D : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,D : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,d : ( ( ) ( ) Element of D : ( ( non empty ) ( non empty ) set ) ) ,e : ( ( ) ( ) Element of D : ( ( non empty ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) multLoopStr_0 ) -> non empty strict ;
end;

registration
let T be ( ( trivial ) ( trivial ) set ) ;
let f be ( ( V6() V18([:T : ( ( trivial ) ( trivial ) set ) ,T : ( ( trivial ) ( trivial ) set ) :] : ( ( ) ( ) set ) ,T : ( ( trivial ) ( trivial ) set ) ) ) ( V6() V18([:T : ( ( trivial ) ( trivial ) set ) ,T : ( ( trivial ) ( trivial ) set ) :] : ( ( ) ( ) set ) ,T : ( ( trivial ) ( trivial ) set ) ) ) BinOp of T : ( ( trivial ) ( trivial ) set ) ) ;
let s, t be ( ( ) ( ) Element of T : ( ( trivial ) ( trivial ) set ) ) ;
cluster multLoopStr_0(# T : ( ( trivial ) ( trivial ) set ) ,f : ( ( V6() V18([:T : ( ( trivial ) ( trivial ) set ) ,T : ( ( trivial ) ( trivial ) set ) :] : ( ( ) ( ) set ) ,T : ( ( trivial ) ( trivial ) set ) ) ) ( V6() V18([:T : ( ( trivial ) ( trivial ) set ) ,T : ( ( trivial ) ( trivial ) set ) :] : ( ( ) ( ) set ) ,T : ( ( trivial ) ( trivial ) set ) ) ) Element of bool [:[:T : ( ( trivial ) ( trivial ) set ) ,T : ( ( trivial ) ( trivial ) set ) :] : ( ( ) ( ) set ) ,T : ( ( trivial ) ( trivial ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,s : ( ( ) ( ) Element of T : ( ( trivial ) ( trivial ) set ) ) ,t : ( ( ) ( ) Element of T : ( ( trivial ) ( trivial ) set ) ) #) : ( ( strict ) ( strict ) multLoopStr_0 ) -> trivial strict ;
end;

registration
let N be ( ( non trivial ) ( non empty non trivial ) set ) ;
let b be ( ( V6() V18([:N : ( ( non trivial ) ( non empty non trivial ) set ) ,N : ( ( non trivial ) ( non empty non trivial ) set ) :] : ( ( ) ( ) set ) ,N : ( ( non trivial ) ( non empty non trivial ) set ) ) ) ( V6() V18([:N : ( ( non trivial ) ( non empty non trivial ) set ) ,N : ( ( non trivial ) ( non empty non trivial ) set ) :] : ( ( ) ( ) set ) ,N : ( ( non trivial ) ( non empty non trivial ) set ) ) ) BinOp of N : ( ( non trivial ) ( non empty non trivial ) set ) ) ;
let m, n be ( ( ) ( ) Element of N : ( ( non trivial ) ( non empty non trivial ) set ) ) ;
cluster multLoopStr_0(# N : ( ( non trivial ) ( non empty non trivial ) set ) ,b : ( ( V6() V18([:N : ( ( non trivial ) ( non empty non trivial ) set ) ,N : ( ( non trivial ) ( non empty non trivial ) set ) :] : ( ( ) ( ) set ) ,N : ( ( non trivial ) ( non empty non trivial ) set ) ) ) ( V6() V18([:N : ( ( non trivial ) ( non empty non trivial ) set ) ,N : ( ( non trivial ) ( non empty non trivial ) set ) :] : ( ( ) ( ) set ) ,N : ( ( non trivial ) ( non empty non trivial ) set ) ) ) Element of bool [:[:N : ( ( non trivial ) ( non empty non trivial ) set ) ,N : ( ( non trivial ) ( non empty non trivial ) set ) :] : ( ( ) ( ) set ) ,N : ( ( non trivial ) ( non empty non trivial ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,m : ( ( ) ( ) Element of N : ( ( non trivial ) ( non empty non trivial ) set ) ) ,n : ( ( ) ( ) Element of N : ( ( non trivial ) ( non empty non trivial ) set ) ) #) : ( ( strict ) ( non empty strict ) multLoopStr_0 ) -> non trivial strict ;
end;

definition
func Trivial-multLoopStr_0 -> ( ( ) ( ) multLoopStr_0 ) equals :: ALGSTR_0:def 34
 multLoopStr_0(# 1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) ,op2 : ( ( V6() V18([:1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) ,1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) :] : ( ( ) ( ) set ) ,1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) ) ) ( V6() V18([:1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) ,1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) :] : ( ( ) ( ) set ) ,1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) ) ) Element of bool [:[:1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) ,1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) :] : ( ( ) ( ) set ) ,1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,op0 : ( ( ) ( V24() V25() V26() ) Element of 1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) ) ,op0 : ( ( ) ( V24() V25() V26() ) Element of 1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) ) #) : ( ( strict ) ( non empty strict ) multLoopStr_0 ) ;
end;

registration
cluster Trivial-multLoopStr_0 : ( ( ) ( ) multLoopStr_0 ) -> 1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) -element strict ;
end;

registration
cluster 1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) -element strict for ( ( ) ( ) multLoopStr_0 ) ;
end;

definition
let M be ( ( ) ( ) multLoopStr_0 ) ;
let x be ( ( ) ( ) Element of ( ( ) ( ) set ) ) ;
func x " -> ( ( ) ( ) Element of ( ( ) ( ) set ) ) means :: ALGSTR_0:def 35
it : ( ( ) ( V24() V25() V26() ) Element of M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ) * x : ( ( V6() V18([:M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ) ) ( V6() V18([:M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ) ) Element of bool [:[:M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of ( ( ) ( ) set ) ) = 1. M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) : ( ( ) ( ) Element of the carrier of M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) : ( ( ) ( ) set ) ) if ( x : ( ( V6() V18([:M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ) ) ( V6() V18([:M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ) ) Element of bool [:[:M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) is left_invertible & x : ( ( V6() V18([:M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ) ) ( V6() V18([:M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ) ) Element of bool [:[:M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) ,M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) is right_mult-cancelable )
otherwise it : ( ( ) ( V24() V25() V26() ) Element of M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) ) = 0. M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) : ( ( ) ( ) Element of the carrier of M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) : ( ( ) ( ) set ) ) ;
end;

definition
let M be ( ( ) ( ) multLoopStr_0 ) ;
attr M is almost_left_cancelable means :: ALGSTR_0:def 36
 for x being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> 0. M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) : ( ( ) ( ) Element of the carrier of M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) : ( ( ) ( ) set ) ) holds
x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is left_mult-cancelable ;
attr M is almost_right_cancelable means :: ALGSTR_0:def 37
 for x being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> 0. M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) : ( ( ) ( ) Element of the carrier of M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) : ( ( ) ( ) set ) ) holds
x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is right_mult-cancelable ;
end;

definition
let M be ( ( ) ( ) multLoopStr_0 ) ;
attr M is almost_cancelable means :: ALGSTR_0:def 38
( M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) is almost_left_cancelable & M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) is almost_right_cancelable );
end;

registration
cluster almost_left_cancelable almost_right_cancelable -> almost_cancelable for ( ( ) ( ) multLoopStr_0 ) ;
cluster almost_cancelable -> almost_left_cancelable almost_right_cancelable for ( ( ) ( ) multLoopStr_0 ) ;
end;

registration
cluster Trivial-multLoopStr_0 : ( ( ) ( non empty trivial V46() 1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) -element strict ) multLoopStr_0 ) -> almost_cancelable ;
end;

registration
cluster 1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) -element strict almost_cancelable for ( ( ) ( ) multLoopStr_0 ) ;
end;

definition
let M be ( ( ) ( ) multLoopStr_0 ) ;
attr M is almost_left_invertible means :: ALGSTR_0:def 39
 for x being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> 0. M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) : ( ( ) ( ) Element of the carrier of M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) : ( ( ) ( ) set ) ) holds
x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is left_invertible ;
attr M is almost_right_invertible means :: ALGSTR_0:def 40
 for x being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> 0. M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) : ( ( ) ( ) Element of the carrier of M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) : ( ( ) ( ) set ) ) holds
x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is right_invertible ;
end;

definition
let M be ( ( ) ( ) multLoopStr_0 ) ;
attr M is almost_invertible means :: ALGSTR_0:def 41
( M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) is almost_right_invertible & M : ( ( cardinal ) ( V24() V25() V26() cardinal ) set ) is almost_left_invertible );
end;

registration
cluster almost_left_invertible almost_right_invertible -> almost_invertible for ( ( ) ( ) multLoopStr_0 ) ;
cluster almost_invertible -> almost_left_invertible almost_right_invertible for ( ( ) ( ) multLoopStr_0 ) ;
end;

registration
cluster Trivial-multLoopStr_0 : ( ( ) ( non empty trivial V46() 1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) -element strict almost_left_cancelable almost_right_cancelable almost_cancelable ) multLoopStr_0 ) -> almost_invertible ;
end;

registration
cluster 1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) -element strict almost_cancelable almost_invertible for ( ( ) ( ) multLoopStr_0 ) ;
end;

begin

definition
attr c1 is strict ;
struct doubleLoopStr -> ( ( ) ( ) addLoopStr ) , ( ( ) ( ) multLoopStr_0 ) ;
aggr doubleLoopStr(# carrier, addF, multF, OneF, ZeroF #) -> ( ( strict ) ( strict ) doubleLoopStr ) ;
end;

registration
let D be ( ( non empty ) ( non empty ) set ) ;
let o, o1 be ( ( V6() V18([:D : ( ( non empty ) ( non empty ) set ) ,D : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,D : ( ( non empty ) ( non empty ) set ) ) ) ( V6() V18([:D : ( ( non empty ) ( non empty ) set ) ,D : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,D : ( ( non empty ) ( non empty ) set ) ) ) BinOp of D : ( ( non empty ) ( non empty ) set ) ) ;
let d, e be ( ( ) ( ) Element of D : ( ( non empty ) ( non empty ) set ) ) ;
cluster doubleLoopStr(# D : ( ( non empty ) ( non empty ) set ) ,o : ( ( V6() V18([:D : ( ( non empty ) ( non empty ) set ) ,D : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,D : ( ( non empty ) ( non empty ) set ) ) ) ( V6() V18([:D : ( ( non empty ) ( non empty ) set ) ,D : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,D : ( ( non empty ) ( non empty ) set ) ) ) Element of bool [:[:D : ( ( non empty ) ( non empty ) set ) ,D : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,D : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,o1 : ( ( V6() V18([:D : ( ( non empty ) ( non empty ) set ) ,D : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,D : ( ( non empty ) ( non empty ) set ) ) ) ( V6() V18([:D : ( ( non empty ) ( non empty ) set ) ,D : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,D : ( ( non empty ) ( non empty ) set ) ) ) Element of bool [:[:D : ( ( non empty ) ( non empty ) set ) ,D : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,D : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,d : ( ( ) ( ) Element of D : ( ( non empty ) ( non empty ) set ) ) ,e : ( ( ) ( ) Element of D : ( ( non empty ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) doubleLoopStr ) -> non empty strict ;
end;

registration
let T be ( ( trivial ) ( trivial ) set ) ;
let f, f1 be ( ( V6() V18([:T : ( ( trivial ) ( trivial ) set ) ,T : ( ( trivial ) ( trivial ) set ) :] : ( ( ) ( ) set ) ,T : ( ( trivial ) ( trivial ) set ) ) ) ( V6() V18([:T : ( ( trivial ) ( trivial ) set ) ,T : ( ( trivial ) ( trivial ) set ) :] : ( ( ) ( ) set ) ,T : ( ( trivial ) ( trivial ) set ) ) ) BinOp of T : ( ( trivial ) ( trivial ) set ) ) ;
let s, t be ( ( ) ( ) Element of T : ( ( trivial ) ( trivial ) set ) ) ;
cluster doubleLoopStr(# T : ( ( trivial ) ( trivial ) set ) ,f : ( ( V6() V18([:T : ( ( trivial ) ( trivial ) set ) ,T : ( ( trivial ) ( trivial ) set ) :] : ( ( ) ( ) set ) ,T : ( ( trivial ) ( trivial ) set ) ) ) ( V6() V18([:T : ( ( trivial ) ( trivial ) set ) ,T : ( ( trivial ) ( trivial ) set ) :] : ( ( ) ( ) set ) ,T : ( ( trivial ) ( trivial ) set ) ) ) Element of bool [:[:T : ( ( trivial ) ( trivial ) set ) ,T : ( ( trivial ) ( trivial ) set ) :] : ( ( ) ( ) set ) ,T : ( ( trivial ) ( trivial ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,f1 : ( ( V6() V18([:T : ( ( trivial ) ( trivial ) set ) ,T : ( ( trivial ) ( trivial ) set ) :] : ( ( ) ( ) set ) ,T : ( ( trivial ) ( trivial ) set ) ) ) ( V6() V18([:T : ( ( trivial ) ( trivial ) set ) ,T : ( ( trivial ) ( trivial ) set ) :] : ( ( ) ( ) set ) ,T : ( ( trivial ) ( trivial ) set ) ) ) Element of bool [:[:T : ( ( trivial ) ( trivial ) set ) ,T : ( ( trivial ) ( trivial ) set ) :] : ( ( ) ( ) set ) ,T : ( ( trivial ) ( trivial ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,s : ( ( ) ( ) Element of T : ( ( trivial ) ( trivial ) set ) ) ,t : ( ( ) ( ) Element of T : ( ( trivial ) ( trivial ) set ) ) #) : ( ( strict ) ( strict ) doubleLoopStr ) -> trivial strict ;
end;

registration
let N be ( ( non trivial ) ( non empty non trivial ) set ) ;
let b, b1 be ( ( V6() V18([:N : ( ( non trivial ) ( non empty non trivial ) set ) ,N : ( ( non trivial ) ( non empty non trivial ) set ) :] : ( ( ) ( ) set ) ,N : ( ( non trivial ) ( non empty non trivial ) set ) ) ) ( V6() V18([:N : ( ( non trivial ) ( non empty non trivial ) set ) ,N : ( ( non trivial ) ( non empty non trivial ) set ) :] : ( ( ) ( ) set ) ,N : ( ( non trivial ) ( non empty non trivial ) set ) ) ) BinOp of N : ( ( non trivial ) ( non empty non trivial ) set ) ) ;
let m, n be ( ( ) ( ) Element of N : ( ( non trivial ) ( non empty non trivial ) set ) ) ;
cluster doubleLoopStr(# N : ( ( non trivial ) ( non empty non trivial ) set ) ,b : ( ( V6() V18([:N : ( ( non trivial ) ( non empty non trivial ) set ) ,N : ( ( non trivial ) ( non empty non trivial ) set ) :] : ( ( ) ( ) set ) ,N : ( ( non trivial ) ( non empty non trivial ) set ) ) ) ( V6() V18([:N : ( ( non trivial ) ( non empty non trivial ) set ) ,N : ( ( non trivial ) ( non empty non trivial ) set ) :] : ( ( ) ( ) set ) ,N : ( ( non trivial ) ( non empty non trivial ) set ) ) ) Element of bool [:[:N : ( ( non trivial ) ( non empty non trivial ) set ) ,N : ( ( non trivial ) ( non empty non trivial ) set ) :] : ( ( ) ( ) set ) ,N : ( ( non trivial ) ( non empty non trivial ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,b1 : ( ( V6() V18([:N : ( ( non trivial ) ( non empty non trivial ) set ) ,N : ( ( non trivial ) ( non empty non trivial ) set ) :] : ( ( ) ( ) set ) ,N : ( ( non trivial ) ( non empty non trivial ) set ) ) ) ( V6() V18([:N : ( ( non trivial ) ( non empty non trivial ) set ) ,N : ( ( non trivial ) ( non empty non trivial ) set ) :] : ( ( ) ( ) set ) ,N : ( ( non trivial ) ( non empty non trivial ) set ) ) ) Element of bool [:[:N : ( ( non trivial ) ( non empty non trivial ) set ) ,N : ( ( non trivial ) ( non empty non trivial ) set ) :] : ( ( ) ( ) set ) ,N : ( ( non trivial ) ( non empty non trivial ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,m : ( ( ) ( ) Element of N : ( ( non trivial ) ( non empty non trivial ) set ) ) ,n : ( ( ) ( ) Element of N : ( ( non trivial ) ( non empty non trivial ) set ) ) #) : ( ( strict ) ( non empty strict ) doubleLoopStr ) -> non trivial strict ;
end;

definition
func Trivial-doubleLoopStr -> ( ( ) ( ) doubleLoopStr ) equals :: ALGSTR_0:def 42
 doubleLoopStr(# 1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) ,op2 : ( ( V6() V18([:1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) ,1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) :] : ( ( ) ( ) set ) ,1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) ) ) ( V6() V18([:1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) ,1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) :] : ( ( ) ( ) set ) ,1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) ) ) Element of bool [:[:1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) ,1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) :] : ( ( ) ( ) set ) ,1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,op2 : ( ( V6() V18([:1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) ,1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) :] : ( ( ) ( ) set ) ,1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) ) ) ( V6() V18([:1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) ,1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) :] : ( ( ) ( ) set ) ,1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) ) ) Element of bool [:[:1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) ,1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) :] : ( ( ) ( ) set ) ,1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,op0 : ( ( ) ( V24() V25() V26() ) Element of 1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) ) ,op0 : ( ( ) ( V24() V25() V26() ) Element of 1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) ) #) : ( ( strict ) ( non empty strict ) doubleLoopStr ) ;
end;

registration
cluster Trivial-doubleLoopStr : ( ( ) ( ) doubleLoopStr ) -> 1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) -element strict ;
end;

registration
cluster 1 : ( ( ) ( non empty V24() V25() V26() V30() V31() cardinal ) Element of K92() : ( ( ) ( non empty V24() V25() V26() V31() cardinal limit_cardinal ) set ) ) -element strict for ( ( ) ( ) doubleLoopStr ) ;
end;