algstr_0.miz



    begin

    reserve D for non empty set,

d,e for Element of D,

o,o1 for BinOp of D;

    reserve T for trivial set,

s,t for Element of T,

f,f1 for BinOp of T;

    reserve N for non trivial set,

n,m for Element of N,

b,b1 for BinOp of N;

    definition

      struct ( 1-sorted) addMagma (# the carrier -> set,

the addF -> BinOp of the carrier #)

       attr strict strict;

    end

    registration

      let D, o;

      cluster addMagma (# D, o #) -> non empty;

      coherence ;

    end

    registration

      let T, f;

      cluster addMagma (# T, f #) -> trivial;

      coherence ;

    end

    registration

      let N, b;

      cluster addMagma (# N, b #) -> non trivial;

      coherence ;

    end

    definition

      let M be addMagma;

      let x,y be Element of M;

      :: ALGSTR_0:def1

      func x + y -> Element of M equals (the addF of M . (x,y));

      coherence ;

    end

    definition

      :: ALGSTR_0:def2

      func Trivial-addMagma -> addMagma equals addMagma (# { 0 }, op2 #);

      coherence ;

    end

    registration

      cluster Trivial-addMagma -> 1 -element strict;

      coherence ;

    end

    registration

      cluster strict1 -element for addMagma;

      existence

      proof

        take Trivial-addMagma ;

        thus thesis;

      end;

    end

    definition

      let M be addMagma, x be Element of M;

      :: ALGSTR_0:def3

      attr x is left_add-cancelable means for y,z be Element of M st (x + y) = (x + z) holds y = z;

      :: ALGSTR_0:def4

      attr x is right_add-cancelable means for y,z be Element of M st (y + x) = (z + x) holds y = z;

    end

    definition

      let M be addMagma, x be Element of M;

      :: ALGSTR_0:def5

      attr x is add-cancelable means x is right_add-cancelable left_add-cancelable;

    end

    registration

      let M be addMagma;

      cluster right_add-cancelable left_add-cancelable -> add-cancelable for Element of M;

      coherence ;

      cluster add-cancelable -> right_add-cancelable left_add-cancelable for Element of M;

      coherence ;

    end

    definition

      let M be addMagma;

      :: ALGSTR_0:def6

      attr M is left_add-cancelable means

      : Def6: for x be Element of M holds x is left_add-cancelable;

      :: ALGSTR_0:def7

      attr M is right_add-cancelable means

      : Def7: for x be Element of M holds x is right_add-cancelable;

    end

    definition

      let M be addMagma;

      :: ALGSTR_0:def8

      attr M is add-cancelable means M is right_add-cancelable left_add-cancelable;

    end

    registration

      cluster right_add-cancelable left_add-cancelable -> add-cancelable for addMagma;

      coherence ;

      cluster add-cancelable -> right_add-cancelable left_add-cancelable for addMagma;

      coherence ;

    end

    registration

      cluster Trivial-addMagma -> add-cancelable;

      coherence

      proof

        set M = Trivial-addMagma ;

        thus M is right_add-cancelable

        proof

          let x,y,z be Element of M;

          assume (y + x) = (z + x);

          thus thesis by STRUCT_0:def 10;

        end;

        let x,y,z be Element of M;

        assume (x + y) = (x + z);

        thus thesis by STRUCT_0:def 10;

      end;

    end

    registration

      cluster add-cancelable strict1 -element for addMagma;

      existence

      proof

        take Trivial-addMagma ;

        thus thesis;

      end;

    end

    registration

      let M be left_add-cancelable addMagma;

      cluster -> left_add-cancelable for Element of M;

      coherence by Def6;

    end

    registration

      let M be right_add-cancelable addMagma;

      cluster -> right_add-cancelable for Element of M;

      coherence by Def7;

    end

    definition

      struct ( ZeroStr, addMagma) addLoopStr (# the carrier -> set,

the addF -> BinOp of the carrier,

the ZeroF -> Element of the carrier #)

       attr strict strict;

    end

    registration

      let D, o, d;

      cluster addLoopStr (# D, o, d #) -> non empty;

      coherence ;

    end

    registration

      let T, f, t;

      cluster addLoopStr (# T, f, t #) -> trivial;

      coherence ;

    end

    registration

      let N, b, m;

      cluster addLoopStr (# N, b, m #) -> non trivial;

      coherence ;

    end

    definition

      :: ALGSTR_0:def9

      func Trivial-addLoopStr -> addLoopStr equals addLoopStr (# { 0 }, op2 , op0 #);

      coherence ;

    end

    registration

      cluster Trivial-addLoopStr -> 1 -element strict;

      coherence ;

    end

    registration

      cluster strict1 -element for addLoopStr;

      existence

      proof

        take Trivial-addLoopStr ;

        thus thesis;

      end;

    end

    definition

      let M be addLoopStr, x be Element of M;

      :: ALGSTR_0:def10

      attr x is left_complementable means ex y be Element of M st (y + x) = ( 0. M);

      :: ALGSTR_0:def11

      attr x is right_complementable means ex y be Element of M st (x + y) = ( 0. M);

    end

    definition

      let M be addLoopStr, x be Element of M;

      :: ALGSTR_0:def12

      attr x is complementable means x is right_complementable left_complementable;

    end

    registration

      let M be addLoopStr;

      cluster right_complementable left_complementable -> complementable for Element of M;

      coherence ;

      cluster complementable -> right_complementable left_complementable for Element of M;

      coherence ;

    end

    definition

      let M be addLoopStr, x be Element of M;

      assume

       A1: x is left_complementable right_add-cancelable;

      :: ALGSTR_0:def13

      func - x -> Element of M means (it + x) = ( 0. M);

      existence by A1;

      uniqueness by A1;

    end

    definition

      let V be addLoopStr;

      let v,w be Element of V;

      :: ALGSTR_0:def14

      func v - w -> Element of V equals (v + ( - w));

      correctness ;

    end

    registration

      cluster Trivial-addLoopStr -> add-cancelable;

      coherence

      proof

        set M = Trivial-addLoopStr ;

        thus M is right_add-cancelable

        proof

          let x,y,z be Element of M;

          assume (y + x) = (z + x);

          thus thesis by STRUCT_0:def 10;

        end;

        let x,y,z be Element of M;

        assume (x + y) = (x + z);

        thus thesis by STRUCT_0:def 10;

      end;

    end

    definition

      let M be addLoopStr;

      :: ALGSTR_0:def15

      attr M is left_complementable means

      : Def15: for x be Element of M holds x is left_complementable;

      :: ALGSTR_0:def16

      attr M is right_complementable means

      : Def16: for x be Element of M holds x is right_complementable;

    end

    definition

      let M be addLoopStr;

      :: ALGSTR_0:def17

      attr M is complementable means M is right_complementable left_complementable;

    end

    registration

      cluster right_complementable left_complementable -> complementable for addLoopStr;

      coherence ;

      cluster complementable -> right_complementable left_complementable for addLoopStr;

      coherence ;

    end

    registration

      cluster Trivial-addLoopStr -> complementable;

      coherence

      proof

        set M = Trivial-addLoopStr ;

        thus M is right_complementable

        proof

          let x be Element of M;

          take x;

          thus thesis by STRUCT_0:def 10;

        end;

        let x be Element of M;

        take x;

        thus thesis by STRUCT_0:def 10;

      end;

    end

    registration

      cluster complementable add-cancelable strict1 -element for addLoopStr;

      existence

      proof

        take Trivial-addLoopStr ;

        thus thesis;

      end;

    end

    registration

      let M be left_complementable addLoopStr;

      cluster -> left_complementable for Element of M;

      coherence by Def15;

    end

    registration

      let M be right_complementable addLoopStr;

      cluster -> right_complementable for Element of M;

      coherence by Def16;

    end

    begin

    definition

      struct ( 1-sorted) multMagma (# the carrier -> set,

the multF -> BinOp of the carrier #)

       attr strict strict;

    end

    registration

      let D, o;

      cluster multMagma (# D, o #) -> non empty;

      coherence ;

    end

    registration

      let T, f;

      cluster multMagma (# T, f #) -> trivial;

      coherence ;

    end

    registration

      let N, b;

      cluster multMagma (# N, b #) -> non trivial;

      coherence ;

    end

    definition

      let M be multMagma;

      let x,y be Element of M;

      :: ALGSTR_0:def18

      func x * y -> Element of M equals (the multF of M . (x,y));

      coherence ;

    end

    definition

      :: ALGSTR_0:def19

      func Trivial-multMagma -> multMagma equals multMagma (# { 0 }, op2 #);

      coherence ;

    end

    registration

      cluster Trivial-multMagma -> 1 -element strict;

      coherence ;

    end

    registration

      cluster strict1 -element for multMagma;

      existence

      proof

        take Trivial-multMagma ;

        thus thesis;

      end;

    end

    definition

      let M be multMagma, x be Element of M;

      :: ALGSTR_0:def20

      attr x is left_mult-cancelable means for y,z be Element of M st (x * y) = (x * z) holds y = z;

      :: ALGSTR_0:def21

      attr x is right_mult-cancelable means for y,z be Element of M st (y * x) = (z * x) holds y = z;

    end

    definition

      let M be multMagma, x be Element of M;

      :: ALGSTR_0:def22

      attr x is mult-cancelable means x is right_mult-cancelable left_mult-cancelable;

    end

    registration

      let M be multMagma;

      cluster right_mult-cancelable left_mult-cancelable -> mult-cancelable for Element of M;

      coherence ;

      cluster mult-cancelable -> right_mult-cancelable left_mult-cancelable for Element of M;

      coherence ;

    end

    definition

      let M be multMagma;

      :: ALGSTR_0:def23

      attr M is left_mult-cancelable means

      : Def23: for x be Element of M holds x is left_mult-cancelable;

      :: ALGSTR_0:def24

      attr M is right_mult-cancelable means

      : Def24: for x be Element of M holds x is right_mult-cancelable;

    end

    definition

      let M be multMagma;

      :: ALGSTR_0:def25

      attr M is mult-cancelable means M is left_mult-cancelable right_mult-cancelable;

    end

    registration

      cluster right_mult-cancelable left_mult-cancelable -> mult-cancelable for multMagma;

      coherence ;

      cluster mult-cancelable -> right_mult-cancelable left_mult-cancelable for multMagma;

      coherence ;

    end

    registration

      cluster Trivial-multMagma -> mult-cancelable;

      coherence

      proof

        set M = Trivial-multMagma ;

        thus M is left_mult-cancelable

        proof

          let x,y,z be Element of M;

          assume (x * y) = (x * z);

          thus thesis by STRUCT_0:def 10;

        end;

        let x,y,z be Element of M;

        assume (y * x) = (z * x);

        thus thesis by STRUCT_0:def 10;

      end;

    end

    registration

      cluster mult-cancelable strict1 -element for multMagma;

      existence

      proof

        take Trivial-multMagma ;

        thus thesis;

      end;

    end

    registration

      let M be left_mult-cancelable multMagma;

      cluster -> left_mult-cancelable for Element of M;

      coherence by Def23;

    end

    registration

      let M be right_mult-cancelable multMagma;

      cluster -> right_mult-cancelable for Element of M;

      coherence by Def24;

    end

    definition

      struct ( OneStr, multMagma) multLoopStr (# the carrier -> set,

the multF -> BinOp of the carrier,

the OneF -> Element of the carrier #)

       attr strict strict;

    end

    registration

      let D, o, d;

      cluster multLoopStr (# D, o, d #) -> non empty;

      coherence ;

    end

    registration

      let T, f, t;

      cluster multLoopStr (# T, f, t #) -> trivial;

      coherence ;

    end

    registration

      let N, b, m;

      cluster multLoopStr (# N, b, m #) -> non trivial;

      coherence ;

    end

    definition

      :: ALGSTR_0:def26

      func Trivial-multLoopStr -> multLoopStr equals multLoopStr (# { 0 }, op2 , op0 #);

      coherence ;

    end

    registration

      cluster Trivial-multLoopStr -> 1 -element strict;

      coherence ;

    end

    registration

      cluster strict1 -element for multLoopStr;

      existence

      proof

        take Trivial-multLoopStr ;

        thus thesis;

      end;

    end

    registration

      cluster Trivial-multLoopStr -> mult-cancelable;

      coherence

      proof

        set M = Trivial-multLoopStr ;

        thus M is left_mult-cancelable

        proof

          let x,y,z be Element of M;

          assume (x * y) = (x * z);

          thus thesis by STRUCT_0:def 10;

        end;

        let x,y,z be Element of M;

        assume (y * x) = (z * x);

        thus thesis by STRUCT_0:def 10;

      end;

    end

    definition

      let M be multLoopStr, x be Element of M;

      :: ALGSTR_0:def27

      attr x is left_invertible means ex y be Element of M st (y * x) = ( 1. M);

      :: ALGSTR_0:def28

      attr x is right_invertible means ex y be Element of M st (x * y) = ( 1. M);

    end

    definition

      let M be multLoopStr, x be Element of M;

      :: ALGSTR_0:def29

      attr x is invertible means x is right_invertible left_invertible;

    end

    registration

      let M be multLoopStr;

      cluster right_invertible left_invertible -> invertible for Element of M;

      coherence ;

      cluster invertible -> right_invertible left_invertible for Element of M;

      coherence ;

    end

    definition

      let M be multLoopStr, x be Element of M;

      assume that

       A1: x is left_invertible and

       A2: x is right_mult-cancelable;

      :: ALGSTR_0:def30

      func / x -> Element of M means (it * x) = ( 1. M);

      existence by A1;

      uniqueness by A2;

    end

    definition

      let M be multLoopStr;

      :: ALGSTR_0:def31

      attr M is left_invertible means

      : Def31: for x be Element of M holds x is left_invertible;

      :: ALGSTR_0:def32

      attr M is right_invertible means

      : Def32: for x be Element of M holds x is right_invertible;

    end

    definition

      let M be multLoopStr;

      :: ALGSTR_0:def33

      attr M is invertible means M is right_invertible left_invertible;

    end

    registration

      cluster right_invertible left_invertible -> invertible for multLoopStr;

      coherence ;

      cluster invertible -> right_invertible left_invertible for multLoopStr;

      coherence ;

    end

    registration

      cluster Trivial-multLoopStr -> invertible;

      coherence

      proof

        set M = Trivial-multLoopStr ;

        thus M is right_invertible

        proof

          let x be Element of M;

          take x;

          thus thesis by STRUCT_0:def 10;

        end;

        let x be Element of M;

        take x;

        thus thesis by STRUCT_0:def 10;

      end;

    end

    registration

      cluster invertible mult-cancelable strict1 -element for multLoopStr;

      existence

      proof

        take Trivial-multLoopStr ;

        thus thesis;

      end;

    end

    registration

      let M be left_invertible multLoopStr;

      cluster -> left_invertible for Element of M;

      coherence by Def31;

    end

    registration

      let M be right_invertible multLoopStr;

      cluster -> right_invertible for Element of M;

      coherence by Def32;

    end

    begin

    definition

      struct ( multLoopStr, ZeroOneStr) multLoopStr_0 (# the carrier -> set,

the multF -> BinOp of the carrier,

the ZeroF, OneF -> Element of the carrier #)

       attr strict strict;

    end

    registration

      let D, o, d, e;

      cluster multLoopStr_0 (# D, o, d, e #) -> non empty;

      coherence ;

    end

    registration

      let T, f, s, t;

      cluster multLoopStr_0 (# T, f, s, t #) -> trivial;

      coherence ;

    end

    registration

      let N, b, m, n;

      cluster multLoopStr_0 (# N, b, m, n #) -> non trivial;

      coherence ;

    end

    definition

      :: ALGSTR_0:def34

      func Trivial-multLoopStr_0 -> multLoopStr_0 equals multLoopStr_0 (# { 0 }, op2 , op0 , op0 #);

      coherence ;

    end

    registration

      cluster Trivial-multLoopStr_0 -> 1 -element strict;

      coherence ;

    end

    registration

      cluster strict1 -element for multLoopStr_0;

      existence

      proof

        take Trivial-multLoopStr_0 ;

        thus thesis;

      end;

    end

    ::$Canceled

    definition

      let M be multLoopStr_0;

      :: ALGSTR_0:def35

      attr M is almost_left_cancelable means for x be Element of M st x <> ( 0. M) holds x is left_mult-cancelable;

      :: ALGSTR_0:def36

      attr M is almost_right_cancelable means for x be Element of M st x <> ( 0. M) holds x is right_mult-cancelable;

    end

    definition

      let M be multLoopStr_0;

      :: ALGSTR_0:def37

      attr M is almost_cancelable means M is almost_left_cancelable almost_right_cancelable;

    end

    registration

      cluster almost_right_cancelable almost_left_cancelable -> almost_cancelable for multLoopStr_0;

      coherence ;

      cluster almost_cancelable -> almost_right_cancelable almost_left_cancelable for multLoopStr_0;

      coherence ;

    end

    registration

      cluster Trivial-multLoopStr_0 -> almost_cancelable;

      coherence

      proof

        set M = Trivial-multLoopStr_0 ;

        thus M is almost_left_cancelable by STRUCT_0:def 10;

        let x be Element of M;

        assume x <> ( 0. M);

        let y,z be Element of M;

        assume (y * x) = (z * x);

        thus thesis by STRUCT_0:def 10;

      end;

    end

    registration

      cluster almost_cancelable strict1 -element for multLoopStr_0;

      existence

      proof

        take Trivial-multLoopStr_0 ;

        thus thesis;

      end;

    end

    definition

      let M be multLoopStr_0;

      :: ALGSTR_0:def38

      attr M is almost_left_invertible means for x be Element of M st x <> ( 0. M) holds x is left_invertible;

      :: ALGSTR_0:def39

      attr M is almost_right_invertible means for x be Element of M st x <> ( 0. M) holds x is right_invertible;

    end

    definition

      let M be multLoopStr_0;

      :: ALGSTR_0:def40

      attr M is almost_invertible means M is almost_right_invertible almost_left_invertible;

    end

    registration

      cluster almost_right_invertible almost_left_invertible -> almost_invertible for multLoopStr_0;

      coherence ;

      cluster almost_invertible -> almost_right_invertible almost_left_invertible for multLoopStr_0;

      coherence ;

    end

    registration

      cluster Trivial-multLoopStr_0 -> almost_invertible;

      coherence

      proof

        set M = Trivial-multLoopStr_0 ;

        thus M is almost_right_invertible by STRUCT_0:def 10;

        let x be Element of M;

        assume x <> ( 0. M);

        take x;

        thus thesis by STRUCT_0:def 10;

      end;

    end

    registration

      cluster almost_invertible almost_cancelable strict1 -element for multLoopStr_0;

      existence

      proof

        take Trivial-multLoopStr_0 ;

        thus thesis;

      end;

    end

    begin

    definition

      struct ( addLoopStr, multLoopStr_0) doubleLoopStr (# the carrier -> set,

the addF, multF -> BinOp of the carrier,

the OneF, ZeroF -> Element of the carrier #)

       attr strict strict;

    end

    registration

      let D, o, o1, d, e;

      cluster doubleLoopStr (# D, o, o1, d, e #) -> non empty;

      coherence ;

    end

    registration

      let T, f, f1, s, t;

      cluster doubleLoopStr (# T, f, f1, s, t #) -> trivial;

      coherence ;

    end

    registration

      let N, b, b1, m, n;

      cluster doubleLoopStr (# N, b, b1, m, n #) -> non trivial;

      coherence ;

    end

    definition

      :: ALGSTR_0:def41

      func Trivial-doubleLoopStr -> doubleLoopStr equals doubleLoopStr (# { 0 }, op2 , op2 , op0 , op0 #);

      coherence ;

    end

    registration

      cluster Trivial-doubleLoopStr -> 1 -element strict;

      coherence ;

    end

    registration

      cluster strict1 -element for doubleLoopStr;

      existence

      proof

        take Trivial-doubleLoopStr ;

        thus thesis;

      end;

    end

    definition

      let M be multLoopStr, x,y be Element of M;

      :: ALGSTR_0:def42

      func x / y -> Element of M equals (x * ( / y));

      coherence ;

    end