msualg_6.miz



    begin

    definition

      let S be non empty ManySortedSign;

      let A be MSAlgebra over S;

      let s be SortSymbol of S;

      mode Element of A,s is Element of (the Sorts of A . s);

    end

    definition

      let I be set;

      let A be ManySortedSet of I;

      let h1,h2 be ManySortedFunction of A, A;

      :: original: **

      redefine

      func h2 ** h1 -> ManySortedFunction of A, A ;

      coherence

      proof

        set h = (h2 ** h1);

        

         A1: ( dom h2) = I by PARTFUN1:def 2;

        ( dom h1) = I by PARTFUN1:def 2;

        

        then

         A2: ( dom h) = (I /\ I) by A1, PBOOLE:def 19

        .= I;

        then

        reconsider h as ManySortedSet of I by PARTFUN1:def 2, RELAT_1:def 18;

        h is ManySortedFunction of A, A

        proof

          let i be object;

          assume

           A3: i in I;

          then

          reconsider f = (h1 . i), g = (h2 . i) as Function of (A . i), (A . i) by PBOOLE:def 15;

          (h . i) = (g * f) by A2, A3, PBOOLE:def 19;

          hence thesis;

        end;

        hence thesis;

      end;

    end

    theorem :: MSUALG_6:1

    

     Th1: for S be non empty non void ManySortedSign holds for A be MSAlgebra over S holds for o be OperSymbol of S, a be set st a in ( Args (o,A)) holds a is Function

    proof

      let S be non empty non void ManySortedSign;

      let A be MSAlgebra over S;

      let o be OperSymbol of S;

      let x be set;

      assume x in ( Args (o,A));

      then x in ( product (the Sorts of A * ( the_arity_of o))) by PRALG_2: 3;

      then ex f be Function st x = f & ( dom f) = ( dom (the Sorts of A * ( the_arity_of o))) & for y be object st y in ( dom (the Sorts of A * ( the_arity_of o))) holds (f . y) in ((the Sorts of A * ( the_arity_of o)) . y) by CARD_3:def 5;

      hence thesis;

    end;

    theorem :: MSUALG_6:2

    

     Th2: for S be non empty non void ManySortedSign holds for A be MSAlgebra over S holds for o be OperSymbol of S, a be Function st a in ( Args (o,A)) holds ( dom a) = ( dom ( the_arity_of o)) & for i be set st i in ( dom ( the_arity_of o)) holds (a . i) in (the Sorts of A . (( the_arity_of o) /. i))

    proof

      let S be non empty non void ManySortedSign;

      let A be MSAlgebra over S;

      let o be OperSymbol of S;

      let x be Function;

      assume x in ( Args (o,A));

      then x in ( product (the Sorts of A * ( the_arity_of o))) by PRALG_2: 3;

      then

       A1: ex f be Function st x = f & ( dom f) = ( dom (the Sorts of A * ( the_arity_of o))) & for y be object st y in ( dom (the Sorts of A * ( the_arity_of o))) holds (f . y) in ((the Sorts of A * ( the_arity_of o)) . y) by CARD_3:def 5;

      hence

       A2: ( dom x) = ( dom ( the_arity_of o)) by PARTFUN1:def 2;

      let y be set;

      assume

       A3: y in ( dom ( the_arity_of o));

      then

       A4: (( the_arity_of o) . y) = (( the_arity_of o) /. y) by PARTFUN1:def 6;

      (x . y) in ((the Sorts of A * ( the_arity_of o)) . y) by A1, A2, A3;

      hence thesis by A3, A4, FUNCT_1: 13;

    end;

    definition

      let S be non empty non void ManySortedSign;

      let A be MSAlgebra over S;

      :: MSUALG_6:def1

      attr A is feasible means

      : Def1: for o be OperSymbol of S st ( Args (o,A)) <> {} holds ( Result (o,A)) <> {} ;

    end

    theorem :: MSUALG_6:3

    

     Th3: for S be non empty non void ManySortedSign holds for o be OperSymbol of S holds for A be MSAlgebra over S holds ( Args (o,A)) <> {} iff for i be Element of NAT st i in ( dom ( the_arity_of o)) holds (the Sorts of A . (( the_arity_of o) /. i)) <> {}

    proof

      let S be non empty non void ManySortedSign;

      let o be OperSymbol of S;

      let A be MSAlgebra over S;

      

       A1: ( dom (the Sorts of A * ( the_arity_of o))) = ( dom ( the_arity_of o)) by PRALG_2: 3;

      

       A2: ( Args (o,A)) = ( product (the Sorts of A * ( the_arity_of o))) by PRALG_2: 3;

      hereby

        assume

         A3: ( Args (o,A)) <> {} ;

        let i be Element of NAT ;

        assume

         A4: i in ( dom ( the_arity_of o));

        then

         A5: (the Sorts of A . (( the_arity_of o) . i)) = ((the Sorts of A * ( the_arity_of o)) . i) by FUNCT_1: 13;

        

         A6: (( the_arity_of o) /. i) = (( the_arity_of o) . i) by A4, PARTFUN1:def 6;

        ((the Sorts of A * ( the_arity_of o)) . i) in ( rng (the Sorts of A * ( the_arity_of o))) by A1, A4, FUNCT_1:def 3;

        hence (the Sorts of A . (( the_arity_of o) /. i)) <> {} by A2, A3, A5, A6, CARD_3: 26;

      end;

      assume

       A7: for i be Element of NAT st i in ( dom ( the_arity_of o)) holds (the Sorts of A . (( the_arity_of o) /. i)) <> {} ;

      assume ( Args (o,A)) = {} ;

      then {} in ( rng (the Sorts of A * ( the_arity_of o))) by A2, CARD_3: 26;

      then

      consider x be object such that

       A8: x in ( dom ( the_arity_of o)) and

       A9: {} = ((the Sorts of A * ( the_arity_of o)) . x) by A1, FUNCT_1:def 3;

      reconsider x as Element of NAT by A8;

      

       A10: (( the_arity_of o) /. x) = (( the_arity_of o) . x) by A8, PARTFUN1:def 6;

      (the Sorts of A . (( the_arity_of o) /. x)) <> {} by A7, A8;

      hence thesis by A8, A9, A10, FUNCT_1: 13;

    end;

    registration

      let S be non empty non void ManySortedSign;

      cluster non-empty -> feasible for MSAlgebra over S;

      coherence ;

    end

    registration

      let S be non empty non void ManySortedSign;

      cluster non-empty for MSAlgebra over S;

      existence

      proof

        set A = the non-empty MSAlgebra over S;

        take A;

        thus thesis;

      end;

    end

    definition

      let S be non empty non void ManySortedSign;

      let A be MSAlgebra over S;

      :: MSUALG_6:def2

      mode Endomorphism of A -> ManySortedFunction of A, A means

      : Def2: it is_homomorphism (A,A);

      existence

      proof

        take ( id the Sorts of A);

        thus thesis by MSUALG_3: 9;

      end;

    end

    reserve S for non empty non void ManySortedSign,

A for MSAlgebra over S;

    theorem :: MSUALG_6:4

    

     Th4: ( id the Sorts of A) is Endomorphism of A

    proof

      thus ( id the Sorts of A) is_homomorphism (A,A) by MSUALG_3: 9;

    end;

    theorem :: MSUALG_6:5

    

     Th5: for h1,h2 be ManySortedFunction of A, A holds for o be OperSymbol of S holds for a be Element of ( Args (o,A)) st a in ( Args (o,A)) holds (h2 # (h1 # a)) = ((h2 ** h1) # a)

    proof

      let h1,h2 be ManySortedFunction of A, A;

      set h = (h2 ** h1);

      let o be OperSymbol of S;

      let a be Element of ( Args (o,A));

      assume

       A1: a in ( Args (o,A));

      then

      reconsider f = a, b = (h1 # a), c = (h2 # (h1 # a)) as Function by Th1;

      

       A2: ( dom f) = ( dom ( the_arity_of o)) by A1, Th2;

      now

        

         A3: ( dom (the Sorts of A * ( the_arity_of o))) = ( dom ( the_arity_of o)) by PRALG_2: 3;

        

         A4: ( Args (o,A)) = ( product (the Sorts of A * ( the_arity_of o))) by PRALG_2: 3;

        let i be Nat;

        reconsider f1 = (h1 . (( the_arity_of o) /. i)), f2 = (h2 . (( the_arity_of o) /. i)) as Function of (the Sorts of A . (( the_arity_of o) /. i)), (the Sorts of A . (( the_arity_of o) /. i));

        

         A5: (h . (( the_arity_of o) /. i)) = (f2 * f1) by MSUALG_3: 2;

        assume

         A6: i in ( dom f);

        then

         A7: (f1 . (f . i)) = (b . i) by A1, MSUALG_3: 24;

        ( dom b) = ( dom ( the_arity_of o)) by A1, Th2;

        then

         A8: (f2 . (b . i)) = (c . i) by A1, A2, A6, MSUALG_3: 24;

        

         A9: (the Sorts of A . (( the_arity_of o) . i)) = ((the Sorts of A * ( the_arity_of o)) . i) by A2, A6, FUNCT_1: 13;

        (( the_arity_of o) /. i) = (( the_arity_of o) . i) by A2, A6, PARTFUN1:def 6;

        then (f . i) in (the Sorts of A . (( the_arity_of o) /. i)) by A1, A2, A6, A4, A3, A9, CARD_3: 9;

        hence (c . i) = ((h . (( the_arity_of o) /. i)) . (f . i)) by A5, A7, A8, FUNCT_2: 15;

      end;

      hence thesis by A1, MSUALG_3: 24;

    end;

    theorem :: MSUALG_6:6

    

     Th6: for h1,h2 be Endomorphism of A holds (h2 ** h1) is Endomorphism of A

    proof

      let h1,h2 be Endomorphism of A;

      let o be OperSymbol of S such that

       A1: ( Args (o,A)) <> {} ;

      set h = (h2 ** h1);

      let x be Element of ( Args (o,A));

      

       A2: ( Result (o,A)) = (the Sorts of A . ( the_result_sort_of o)) by PRALG_2: 3;

      

       A3: h2 is_homomorphism (A,A) by Def2;

      reconsider f1 = (h1 . ( the_result_sort_of o)), f2 = (h2 . ( the_result_sort_of o)), f = (h . ( the_result_sort_of o)) as Function of (the Sorts of A . ( the_result_sort_of o)), (the Sorts of A . ( the_result_sort_of o));

      

       A4: h1 is_homomorphism (A,A) by Def2;

      per cases ;

        suppose

         A5: (the Sorts of A . ( the_result_sort_of o)) = {} ;

        then ( dom f) = {} ;

        then

         A6: (f . (( Den (o,A)) . x)) = {} by FUNCT_1:def 2;

        ( dom ( Den (o,A))) = {} by A2, A5;

        hence thesis by A6, FUNCT_1:def 2;

      end;

        suppose

         A7: (the Sorts of A . ( the_result_sort_of o)) <> {} ;

        (h . ( the_result_sort_of o)) = (f2 * f1) by MSUALG_3: 2;

        

        then ((h . ( the_result_sort_of o)) . (( Den (o,A)) . x)) = (f2 . (f1 . (( Den (o,A)) . x))) by A1, A2, A7, FUNCT_2: 5, FUNCT_2: 15

        .= ((h2 . ( the_result_sort_of o)) . (( Den (o,A)) . (h1 # x))) by A4, A1

        .= (( Den (o,A)) . (h2 # (h1 # x))) by A3, A1;

        hence thesis by A1, Th5;

      end;

    end;

    definition

      let S be non empty non void ManySortedSign;

      let A be MSAlgebra over S;

      let h1,h2 be Endomorphism of A;

      :: original: **

      redefine

      func h2 ** h1 -> Endomorphism of A ;

      coherence by Th6;

    end

    definition

      let S be non empty non void ManySortedSign;

      :: MSUALG_6:def3

      func TranslationRel S -> Relation of the carrier of S means

      : Def3: for s1,s2 be SortSymbol of S holds [s1, s2] in it iff ex o be OperSymbol of S st ( the_result_sort_of o) = s2 & ex i be Element of NAT st i in ( dom ( the_arity_of o)) & (( the_arity_of o) /. i) = s1;

      existence

      proof

        defpred P[ set, set] means ex o be OperSymbol of S st ( the_result_sort_of o) = $2 & ex i be Element of NAT st i in ( dom ( the_arity_of o)) & (( the_arity_of o) /. i) = $1;

        ex R be Relation of the carrier of S, the carrier of S st for x be SortSymbol of S, y be SortSymbol of S holds [x, y] in R iff P[x, y] from RELSET_1:sch 2;

        hence thesis;

      end;

      correctness

      proof

        defpred P[ set, set] means ex o be OperSymbol of S st ( the_result_sort_of o) = $2 & ex i be Element of NAT st i in ( dom ( the_arity_of o)) & (( the_arity_of o) /. i) = $1;

        for R1,R2 be Relation of the carrier of S, the carrier of S st (for x be SortSymbol of S, y be SortSymbol of S holds [x, y] in R1 iff P[x, y]) & (for x be SortSymbol of S, y be SortSymbol of S holds [x, y] in R2 iff P[x, y]) holds R1 = R2 from PUA2MSS1:sch 2;

        hence thesis;

      end;

    end

    theorem :: MSUALG_6:7

    

     Th7: for S be non empty non void ManySortedSign, o be OperSymbol of S holds for A be MSAlgebra over S, a be Function st a in ( Args (o,A)) holds for i be Nat, x be Element of A, (( the_arity_of o) /. i) holds (a +* (i,x)) in ( Args (o,A))

    proof

      let S be non empty non void ManySortedSign, o be OperSymbol of S;

      let A be MSAlgebra over S;

      

       A1: ( dom (the Sorts of A * ( the_arity_of o))) = ( dom ( the_arity_of o)) by PRALG_2: 3;

      let a be Function such that

       A2: a in ( Args (o,A));

      

       A3: ( dom a) = ( dom ( the_arity_of o)) by A2, Th2;

      let i be Nat;

      let x be Element of A, (( the_arity_of o) /. i);

      

       A4: ( Args (o,A)) = ( product (the Sorts of A * ( the_arity_of o))) by PRALG_2: 3;

       A5:

      now

        let j be object;

        assume

         A6: j in ( dom a);

        then

        reconsider k = j as Element of NAT by A3;

        

         A7: ((the Sorts of A * ( the_arity_of o)) . k) = (the Sorts of A . (( the_arity_of o) . k)) by A3, A6, FUNCT_1: 13;

        

         A8: (( the_arity_of o) /. k) = (( the_arity_of o) . k) by A3, A6, PARTFUN1:def 6;

        then

         A9: ((the Sorts of A * ( the_arity_of o)) . j) <> {} by A2, A3, A6, A7, Th3;

        per cases ;

          suppose

           A10: j = i;

          then ((a +* (i,x)) . j) = x by A6, FUNCT_7: 31;

          hence ((a +* (i,x)) . j) in ((the Sorts of A * ( the_arity_of o)) . j) by A8, A7, A9, A10;

        end;

          suppose j <> i;

          then ((a +* (i,x)) . j) = (a . j) by FUNCT_7: 32;

          hence ((a +* (i,x)) . j) in ((the Sorts of A * ( the_arity_of o)) . j) by A2, A4, A1, A3, A6, CARD_3: 9;

        end;

      end;

      ( dom (a +* (i,x))) = ( dom a) by FUNCT_7: 30;

      hence thesis by A4, A1, A3, A5, CARD_3: 9;

    end;

    theorem :: MSUALG_6:8

    

     Th8: for A1,A2 be MSAlgebra over S, h be ManySortedFunction of A1, A2 holds for o be OperSymbol of S st ( Args (o,A1)) <> {} & ( Args (o,A2)) <> {} holds for i be Element of NAT st i in ( dom ( the_arity_of o)) holds for x be Element of A1, (( the_arity_of o) /. i) holds ((h . (( the_arity_of o) /. i)) . x) in (the Sorts of A2 . (( the_arity_of o) /. i))

    proof

      let A1,A2 be MSAlgebra over S, h be ManySortedFunction of A1, A2;

      let o be OperSymbol of S such that

       A1: ( Args (o,A1)) <> {} and

       A2: ( Args (o,A2)) <> {} ;

      let i be Element of NAT ;

      assume

       A3: i in ( dom ( the_arity_of o));

      then

       A4: (the Sorts of A2 . (( the_arity_of o) /. i)) <> {} by A2, Th3;

      (the Sorts of A1 . (( the_arity_of o) /. i)) <> {} by A1, A3, Th3;

      hence thesis by A4, FUNCT_2: 5;

    end;

    theorem :: MSUALG_6:9

    

     Th9: for S be non empty non void ManySortedSign, o be OperSymbol of S holds for i be Element of NAT st i in ( dom ( the_arity_of o)) holds for A1,A2 be MSAlgebra over S holds for h be ManySortedFunction of A1, A2 holds for a,b be Element of ( Args (o,A1)) st a in ( Args (o,A1)) & (h # a) in ( Args (o,A2)) holds for f,g1,g2 be Function st f = a & g1 = (h # a) & g2 = (h # b) holds for x be Element of A1, (( the_arity_of o) /. i) st b = (f +* (i,x)) holds (g2 . i) = ((h . (( the_arity_of o) /. i)) . x) & (h # b) = (g1 +* (i,(g2 . i)))

    proof

      let S be non empty non void ManySortedSign, o be OperSymbol of S;

      let i be Element of NAT such that

       A1: i in ( dom ( the_arity_of o));

      let A1,A2 be MSAlgebra over S;

      let h be ManySortedFunction of A1, A2;

      let a,b be Element of ( Args (o,A1)) such that

       A2: a in ( Args (o,A1)) and

       A3: (h # a) in ( Args (o,A2));

      reconsider f2 = b as Function by A2, Th1;

      

       A4: ( dom f2) = ( dom ( the_arity_of o)) by A2, Th2;

      let f,g1,g2 be Function such that

       A5: f = a and

       A6: g1 = (h # a) and

       A7: g2 = (h # b);

      reconsider g3 = (g1 +* (i,(g2 . i))) as Function;

      

       A8: ( dom f) = ( dom ( the_arity_of o)) by A2, A5, Th2;

      let x be Element of A1, (( the_arity_of o) /. i) such that

       A9: b = (f +* (i,x));

      (f2 . i) = x by A1, A9, A8, FUNCT_7: 31;

      hence (g2 . i) = ((h . (( the_arity_of o) /. i)) . x) by A1, A2, A3, A7, A4, MSUALG_3: 24;

      then (g2 . i) in (the Sorts of A2 . (( the_arity_of o) /. i)) by A1, A2, A3, Th8;

      then (g1 +* (i,(g2 . i))) in ( Args (o,A2)) by A3, A6, Th7;

      then

       A10: ( dom g3) = ( dom ( the_arity_of o)) by Th2;

       A11:

      now

        let z be set;

        assume that

         A12: z in ( dom ( the_arity_of o)) and

         A13: z <> i;

        reconsider j = z as Element of NAT by A12;

        

         A14: (f2 . j) = (f . j) by A9, A13, FUNCT_7: 32;

        (g2 . j) = ((h . (( the_arity_of o) /. j)) . (f2 . j)) by A2, A3, A7, A4, A12, MSUALG_3: 24;

        hence (g2 . z) = (g1 . z) by A2, A3, A5, A6, A8, A12, A14, MSUALG_3: 24;

      end;

      

       A15: ( dom g1) = ( dom ( the_arity_of o)) by A3, A6, Th2;

       A16:

      now

        let z be object;

        assume

         A17: z in ( dom ( the_arity_of o));

        per cases ;

          suppose z = i;

          hence (g2 . z) = ((g1 +* (i,(g2 . i))) . z) by A1, A15, FUNCT_7: 31;

        end;

          suppose

           A18: z <> i;

          then (g2 . z) = (g1 . z) by A11, A17;

          hence (g2 . z) = ((g1 +* (i,(g2 . i))) . z) by A18, FUNCT_7: 32;

        end;

      end;

      ( dom g2) = ( dom ( the_arity_of o)) by A3, A7, Th2;

      hence thesis by A7, A10, A16, FUNCT_1: 2;

    end;

    definition

      let S be non empty non void ManySortedSign, o be OperSymbol of S;

      let i be Nat;

      let A be MSAlgebra over S;

      let a be Function;

      :: MSUALG_6:def4

      func transl (o,i,a,A) -> Function means

      : Def4: ( dom it ) = (the Sorts of A . (( the_arity_of o) /. i)) & for x be object st x in (the Sorts of A . (( the_arity_of o) /. i)) holds (it . x) = (( Den (o,A)) . (a +* (i,x)));

      existence

      proof

        deffunc F( object) = (( Den (o,A)) . (a +* (i,$1)));

        ex f be Function st ( dom f) = (the Sorts of A . (( the_arity_of o) /. i)) & for x be object st x in (the Sorts of A . (( the_arity_of o) /. i)) holds (f . x) = F(x) from FUNCT_1:sch 3;

        hence thesis;

      end;

      uniqueness

      proof

        let f1,f2 be Function such that

         A1: ( dom f1) = (the Sorts of A . (( the_arity_of o) /. i)) and

         A2: for x be object st x in (the Sorts of A . (( the_arity_of o) /. i)) holds (f1 . x) = (( Den (o,A)) . (a +* (i,x))) and

         A3: ( dom f2) = (the Sorts of A . (( the_arity_of o) /. i)) and

         A4: for x be object st x in (the Sorts of A . (( the_arity_of o) /. i)) holds (f2 . x) = (( Den (o,A)) . (a +* (i,x)));

        now

          let x be object;

          assume

           A5: x in (the Sorts of A . (( the_arity_of o) /. i));

          then (f1 . x) = (( Den (o,A)) . (a +* (i,x))) by A2;

          hence (f1 . x) = (f2 . x) by A4, A5;

        end;

        hence thesis by A1, A3;

      end;

    end

    theorem :: MSUALG_6:10

    

     Th10: for S be non empty non void ManySortedSign, o be OperSymbol of S holds for i be Element of NAT holds for A be feasible MSAlgebra over S, a be Function st a in ( Args (o,A)) holds ( transl (o,i,a,A)) is Function of (the Sorts of A . (( the_arity_of o) /. i)), (the Sorts of A . ( the_result_sort_of o))

    proof

      let S be non empty non void ManySortedSign, o be OperSymbol of S;

      let i be Element of NAT ;

      let A be feasible MSAlgebra over S;

      let a be Function;

      assume

       A1: a in ( Args (o,A));

      then

       A2: ( Result (o,A)) <> {} by Def1;

      

       A3: ( dom ( transl (o,i,a,A))) = (the Sorts of A . (( the_arity_of o) /. i)) by Def4;

      

       A4: ( rng ( transl (o,i,a,A))) c= (the Sorts of A . ( the_result_sort_of o))

      proof

        let x be object;

        assume x in ( rng ( transl (o,i,a,A)));

        then

        consider y be object such that

         A5: y in ( dom ( transl (o,i,a,A))) and

         A6: x = (( transl (o,i,a,A)) . y) by FUNCT_1:def 3;

        reconsider y as Element of A, (( the_arity_of o) /. i) by A5, Def4;

        set b = (a +* (i,y));

        

         A7: (( Den (o,A)) . b) in ( Result (o,A)) by A1, A2, Th7, FUNCT_2: 5;

        x = (( Den (o,A)) . b) by A3, A5, A6, Def4;

        hence thesis by A7, PRALG_2: 3;

      end;

      ( Result (o,A)) = (the Sorts of A . ( the_result_sort_of o)) by PRALG_2: 3;

      hence thesis by A2, A3, A4, FUNCT_2:def 1, RELSET_1: 4;

    end;

    definition

      let S be non empty non void ManySortedSign, s1,s2 be SortSymbol of S;

      let A be MSAlgebra over S;

      let f be Function;

      :: MSUALG_6:def5

      pred f is_e.translation_of A,s1,s2 means ex o be OperSymbol of S st ( the_result_sort_of o) = s2 & ex i be Element of NAT st i in ( dom ( the_arity_of o)) & (( the_arity_of o) /. i) = s1 & ex a be Function st a in ( Args (o,A)) & f = ( transl (o,i,a,A));

    end

    theorem :: MSUALG_6:11

    

     Th11: for S be non empty non void ManySortedSign, s1,s2 be SortSymbol of S holds for A be feasible MSAlgebra over S, f be Function st f is_e.translation_of (A,s1,s2) holds f is Function of (the Sorts of A . s1), (the Sorts of A . s2) & (the Sorts of A . s1) <> {} & (the Sorts of A . s2) <> {}

    proof

      let S be non empty non void ManySortedSign, s1,s2 be SortSymbol of S;

      let A be feasible MSAlgebra over S;

      let f be Function;

      assume f is_e.translation_of (A,s1,s2);

      then

      consider o be OperSymbol of S such that

       A1: ( the_result_sort_of o) = s2 and

       A2: ex i be Element of NAT st i in ( dom ( the_arity_of o)) & (( the_arity_of o) /. i) = s1 & ex a be Function st a in ( Args (o,A)) & f = ( transl (o,i,a,A));

      ( Result (o,A)) = (the Sorts of A . ( the_result_sort_of o)) by PRALG_2: 3;

      hence thesis by A1, A2, Def1, Th3, Th10;

    end;

    theorem :: MSUALG_6:12

    

     Th12: for S be non empty non void ManySortedSign, s1,s2 be SortSymbol of S holds for A be MSAlgebra over S, f be Function st f is_e.translation_of (A,s1,s2) holds [s1, s2] in ( TranslationRel S) by Def3;

    theorem :: MSUALG_6:13

    for S be non empty non void ManySortedSign, s1,s2 be SortSymbol of S holds for A be non-empty MSAlgebra over S st [s1, s2] in ( TranslationRel S) holds ex f be Function st f is_e.translation_of (A,s1,s2)

    proof

      let S be non empty non void ManySortedSign, s1,s2 be SortSymbol of S;

      let A be non-empty MSAlgebra over S;

      assume [s1, s2] in ( TranslationRel S);

      then

      consider o be OperSymbol of S such that

       A1: ( the_result_sort_of o) = s2 and

       A2: ex i be Element of NAT st i in ( dom ( the_arity_of o)) & (( the_arity_of o) /. i) = s1 by Def3;

      set a = the Element of ( Args (o,A));

      consider i be Element of NAT such that

       A3: i in ( dom ( the_arity_of o)) and

       A4: (( the_arity_of o) /. i) = s1 by A2;

      take ( transl (o,i,a,A)), o;

      thus thesis by A1, A3, A4;

    end;

    theorem :: MSUALG_6:14

    

     Th14: for S be non empty non void ManySortedSign holds for A be feasible MSAlgebra over S holds for s1,s2 be SortSymbol of S holds for q be RedSequence of ( TranslationRel S), p be Function-yielding FinSequence st ( len q) = (( len p) + 1) & s1 = (q . 1) & s2 = (q . ( len q)) & for i be Element of NAT , f be Function, s1,s2 be SortSymbol of S st i in ( dom p) & f = (p . i) & s1 = (q . i) & s2 = (q . (i + 1)) holds f is_e.translation_of (A,s1,s2) holds ( compose (p,(the Sorts of A . s1))) is Function of (the Sorts of A . s1), (the Sorts of A . s2) & (p <> {} implies (the Sorts of A . s1) <> {} & (the Sorts of A . s2) <> {} )

    proof

      let S be non empty non void ManySortedSign;

      let A be feasible MSAlgebra over S;

      let s1,s2 be SortSymbol of S;

      let q be RedSequence of ( TranslationRel S), p be Function-yielding FinSequence such that

       A1: ( len q) = (( len p) + 1) and

       A2: s1 = (q . 1) and

       A3: s2 = (q . ( len q)) and

       A4: for i be Element of NAT , f be Function, s1,s2 be SortSymbol of S st i in ( dom p) & f = (p . i) & s1 = (q . i) & s2 = (q . (i + 1)) holds f is_e.translation_of (A,s1,s2);

      per cases ;

        suppose

         A5: p = {} ;

        then

         A6: ( len p) = 0 ;

        ( compose (p,(the Sorts of A . s1))) = ( id (the Sorts of A . s1)) by A5, FUNCT_7: 39;

        hence thesis by A1, A2, A3, A6;

      end;

        suppose p <> {} ;

        then

         A7: ( rng p) <> {} ;

        then

         A8: 1 in ( dom p) by FINSEQ_3: 32;

        then

         A9: (1 + 1) in ( dom q) by A1, FUNCT_7: 22;

        1 in ( dom q) by A1, A8, FUNCT_7: 22;

        then [(q . 1), (q . (1 + 1))] in ( TranslationRel S) by A9, REWRITE1:def 2;

        then

        reconsider q1 = (q . 1), q2 = (q . (1 + 1)) as SortSymbol of S by ZFMISC_1: 87;

        deffunc F( set) = (the Sorts of A . (q . $1));

        reconsider f = (p . 1) as Function;

        

         A10: ( dom q) = ( Seg ( len q)) by FINSEQ_1:def 3;

        consider pp be FinSequence such that

         A11: ( len pp) = ( len q) and

         A12: for i be Nat st i in ( dom pp) holds (pp . i) = F(i) from FINSEQ_1:sch 2;

        defpred P[ Nat] means $1 in ( dom pp) implies not (pp . $1) is empty;

        

         A13: ( dom pp) = ( Seg ( len q)) by A11, FINSEQ_1:def 3;

        f is_e.translation_of (A,q1,q2) by A4, A7, FINSEQ_3: 32;

        then

         A14: (the Sorts of A . q1) <> {} by Th11;

        

         A15: for i be Nat st P[i] holds P[(i + 1)]

        proof

          let i be Nat such that i in ( dom pp) implies not (pp . i) is empty and

           A16: (i + 1) in ( dom pp);

          

           A17: i <= (i + 1) by NAT_1: 11;

          (i + 1) <= ( len pp) by A16, FINSEQ_3: 25;

          then

           A18: i <= ( len pp) by A17, XXREAL_0: 2;

          per cases ;

            suppose i = 0 ;

            hence thesis by A14, A12, A16;

          end;

            suppose i > 0 ;

            then i >= ( 0 + 1) by NAT_1: 13;

            then

             A19: i in ( dom pp) by A18, FINSEQ_3: 25;

            then [(q . i), (q . (i + 1))] in ( TranslationRel S) by A10, A13, A16, REWRITE1:def 2;

            then

            reconsider s1 = (q . i), s2 = (q . (i + 1)) as SortSymbol of S by ZFMISC_1: 87;

            reconsider f = (p . i) as Function;

            i in ( dom p) by A1, A11, A16, A19, FUNCT_7: 22;

            then

             A20: f is_e.translation_of (A,s1,s2) by A4;

            (pp . (i + 1)) = (the Sorts of A . s2) by A12, A16;

            hence thesis by A20, Th11;

          end;

        end;

        

         A21: P[ 0 ] by FINSEQ_3: 25;

        

         A22: for i be Nat holds P[i] from NAT_1:sch 2( A21, A15);

        

         A23: pp is non-empty by A22;

        

         A24: ( dom pp) = ( Seg ( len q)) by A11, FINSEQ_1:def 3;

        reconsider pp as non empty non-empty FinSequence by A11, A23;

        

         A25: ( dom p) = ( Seg ( len p)) by FINSEQ_1:def 3;

        p is FuncSequence of pp

        proof

          thus (( len p) + 1) = ( len pp) by A1, A11;

          let j be Nat;

          reconsider f = (p . j) as Function;

          assume

           A26: j in ( dom p);

          then

           A27: j >= 1 by A25, FINSEQ_1: 1;

          then

           A28: (j + 1) >= 1 by NAT_1: 13;

          

           A29: j <= ( len p) by A25, A26, FINSEQ_1: 1;

          then j <= ( len q) by A1, NAT_1: 13;

          then

           A30: j in ( Seg ( len q)) by A27, FINSEQ_1: 1;

          (j + 1) <= ( len q) by A1, A29, XREAL_1: 6;

          then

           A31: (j + 1) in ( Seg ( len q)) by A28, FINSEQ_1: 1;

          then [(q . j), (q . (j + 1))] in ( TranslationRel S) by A10, A30, REWRITE1:def 2;

          then

          reconsider s1 = (q . j), s2 = (q . (j + 1)) as SortSymbol of S by ZFMISC_1: 87;

          

           A32: (pp . (j + 1)) = (the Sorts of A . s2) by A12, A24, A31;

          

           A33: f is_e.translation_of (A,s1,s2) by A4, A26;

          then

           A34: (p . j) is Function of (the Sorts of A . s1), (the Sorts of A . s2) by Th11;

          

           A35: (the Sorts of A . s2) <> {} by A33, Th11;

          (pp . j) = (the Sorts of A . s1) by A12, A24, A30;

          hence thesis by A34, A35, A32, FUNCT_2: 8;

        end;

        then

        reconsider p9 = p as FuncSequence of pp;

        

         A36: 1 in ( dom q) by FINSEQ_5: 6;

        then

         A37: (pp . 1) = (the Sorts of A . s1) by A2, A10, A12, A13;

        then

         A38: ( dom ( compose (p9,(the Sorts of A . s1)))) = (the Sorts of A . s1) by FUNCT_7: 67;

        

         A39: ( len q) in ( dom q) by FINSEQ_5: 6;

        then

         A40: (pp . ( len pp)) = (the Sorts of A . s2) by A3, A10, A11, A12, A13;

        then ( rng ( compose (p9,(the Sorts of A . s1)))) c= (the Sorts of A . s2) by A37, FUNCT_7: 67;

        hence ( compose (p,(the Sorts of A . s1))) is Function of (the Sorts of A . s1), (the Sorts of A . s2) by A10, A11, A13, A39, A40, A38, FUNCT_2:def 1, RELSET_1: 4;

        thus thesis by A10, A11, A13, A36, A39, A37, A40;

      end;

    end;

    definition

      let S be non empty non void ManySortedSign;

      let A be non-empty MSAlgebra over S;

      let s1,s2 be SortSymbol of S;

      :: MSUALG_6:def6

      mode Translation of A,s1,s2 -> Function of (the Sorts of A . s1), (the Sorts of A . s2) means

      : Def6: ex q be RedSequence of ( TranslationRel S), p be Function-yielding FinSequence st it = ( compose (p,(the Sorts of A . s1))) & ( len q) = (( len p) + 1) & s1 = (q . 1) & s2 = (q . ( len q)) & for i be Element of NAT , f be Function, s1,s2 be SortSymbol of S st i in ( dom p) & f = (p . i) & s1 = (q . i) & s2 = (q . (i + 1)) holds f is_e.translation_of (A,s1,s2);

      existence

      proof

        consider q be RedSequence of ( TranslationRel S) such that

         A2: (q . 1) = s1 and

         A3: (q . ( len q)) = s2 by A1;

        defpred Z[ object, object] means ex f be Function, s1,s2 be SortSymbol of S, i be Element of NAT st $2 = f & i = $1 & s1 = (q . i) & s2 = (q . (i + 1)) & f is_e.translation_of (A,s1,s2);

        ( len q) >= ( 0 + 1) by NAT_1: 13;

        then

        consider n be Nat such that

         A4: ( len q) = (1 + n) by NAT_1: 10;

        reconsider n as Element of NAT by ORDINAL1:def 12;

        

         A5: ( dom q) = ( Seg ( len q)) by FINSEQ_1:def 3;

        

         A6: for x be object st x in ( Seg n) holds ex y be object st Z[x, y]

        proof

          let x be object;

          assume

           A7: x in ( Seg n);

          then

          reconsider i = x as Element of NAT ;

          

           A8: i <= n by A7, FINSEQ_1: 1;

          then

           A9: (i + 1) <= ( len q) by A4, XREAL_1: 6;

          

           A10: i >= 1 by A7, FINSEQ_1: 1;

          then (i + 1) >= 1 by NAT_1: 13;

          then

           A11: (i + 1) in ( dom q) by A5, A9, FINSEQ_1: 1;

          i <= (n + 1) by A8, NAT_1: 13;

          then i in ( dom q) by A4, A5, A10, FINSEQ_1: 1;

          then

           A12: [(q . i), (q . (i + 1))] in ( TranslationRel S) by A11, REWRITE1:def 2;

          then

          reconsider s1 = (q . i), s2 = (q . (i + 1)) as SortSymbol of S by ZFMISC_1: 87;

          consider o be OperSymbol of S such that

           A13: ( the_result_sort_of o) = s2 and

           A14: ex i be Element of NAT st i in ( dom ( the_arity_of o)) & (( the_arity_of o) /. i) = s1 by A12, Def3;

          set a = the Element of ( Args (o,A));

          consider j be Element of NAT such that

           A15: j in ( dom ( the_arity_of o)) and

           A16: (( the_arity_of o) /. j) = s1 by A14;

          take ( transl (o,j,a,A));

          take ( transl (o,j,a,A)), s1, s2, i;

          thus thesis by A13, A15, A16;

        end;

        consider p be Function such that

         A17: ( dom p) = ( Seg n) & for x be object st x in ( Seg n) holds Z[x, (p . x)] from CLASSES1:sch 1( A6);

        p is Function-yielding

        proof

          let j be object;

          assume j in ( dom p);

          then ex f be Function, s1,s2 be SortSymbol of S, i be Element of NAT st (p . j) = f & i = j & s1 = (q . i) & s2 = (q . (i + 1)) & f is_e.translation_of (A,s1,s2) by A17;

          hence thesis;

        end;

        then

        reconsider p as Function-yielding FinSequence by A17, FINSEQ_1:def 2;

         A18:

        now

          let i be Element of NAT ;

          let f be Function, s1,s2 be SortSymbol of S;

          assume i in ( dom p);

          then ex f be Function, s1,s2 be SortSymbol of S, j be Element of NAT st (p . i) = f & j = i & s1 = (q . j) & s2 = (q . (j + 1)) & f is_e.translation_of (A,s1,s2) by A17;

          hence f = (p . i) & s1 = (q . i) & s2 = (q . (i + 1)) implies f is_e.translation_of (A,s1,s2);

        end;

        ( len p) = n by A17, FINSEQ_1:def 3;

        then

        reconsider t = ( compose (p,(the Sorts of A . s1))) as Function of (the Sorts of A . s1), (the Sorts of A . s2) by A2, A3, A4, A18, Th14;

        take t, q, p;

        thus thesis by A2, A3, A4, A17, A18, FINSEQ_1:def 3;

      end;

    end

    theorem :: MSUALG_6:15

    for S be non empty non void ManySortedSign holds for A be non-empty MSAlgebra over S holds for s1,s2 be SortSymbol of S st ( TranslationRel S) reduces (s1,s2) holds for q be RedSequence of ( TranslationRel S), p be Function-yielding FinSequence st ( len q) = (( len p) + 1) & s1 = (q . 1) & s2 = (q . ( len q)) & for i be Element of NAT , f be Function, s1,s2 be SortSymbol of S st i in ( dom p) & f = (p . i) & s1 = (q . i) & s2 = (q . (i + 1)) holds f is_e.translation_of (A,s1,s2) holds ( compose (p,(the Sorts of A . s1))) is Translation of A, s1, s2

    proof

      let S be non empty non void ManySortedSign;

      let A be non-empty MSAlgebra over S;

      let s1,s2 be SortSymbol of S such that

       A1: ( TranslationRel S) reduces (s1,s2);

      let q be RedSequence of ( TranslationRel S), p be Function-yielding FinSequence such that

       A2: ( len q) = (( len p) + 1) and

       A3: s1 = (q . 1) and

       A4: s2 = (q . ( len q)) and

       A5: for i be Element of NAT , f be Function, s1,s2 be SortSymbol of S st i in ( dom p) & f = (p . i) & s1 = (q . i) & s2 = (q . (i + 1)) holds f is_e.translation_of (A,s1,s2);

      ( compose (p,(the Sorts of A . s1))) is Function of (the Sorts of A . s1), (the Sorts of A . s2) by A2, A3, A4, A5, Th14;

      hence thesis by A1, A2, A3, A4, A5, Def6;

    end;

    reserve A for non-empty MSAlgebra over S;

    theorem :: MSUALG_6:16

    

     Th16: for s be SortSymbol of S holds ( id (the Sorts of A . s)) is Translation of A, s, s

    proof

      let s be SortSymbol of S;

      thus ( TranslationRel S) reduces (s,s) by REWRITE1: 12;

      

       A1: <*s*> is RedSequence of ( TranslationRel S) by REWRITE1: 6;

      

       A2: ( len <*s*>) = ( 0 + 1) by FINSEQ_1: 40;

      

       A3: ( len {} ) = 0 ;

      

       A4: for i be Element of NAT , f be Function, s1,s2 be SortSymbol of S st i in ( dom {} ) & f = ( {} . i) & s1 = ( <*s*> . i) & s2 = ( <*s*> . (i + 1)) holds f is_e.translation_of (A,s1,s2);

      

       A5: ( <*s*> . 1) = s by FINSEQ_1: 40;

      ( id (the Sorts of A . s)) = ( compose ( {} ,(the Sorts of A . s))) by FUNCT_7: 39;

      hence thesis by A1, A2, A3, A5, A4;

    end;

    theorem :: MSUALG_6:17

    

     Th17: for s1,s2 be SortSymbol of S, f be Function st f is_e.translation_of (A,s1,s2) holds ( TranslationRel S) reduces (s1,s2) & f is Translation of A, s1, s2

    proof

      let s1,s2 be SortSymbol of S, f be Function;

      

       A1: ( len <*s1, s2*>) = (1 + 1) by FINSEQ_1: 44;

      

       A2: ( len <*f*>) = 1 by FINSEQ_1: 40;

      assume

       A3: f is_e.translation_of (A,s1,s2);

      then

      reconsider g = f as Function of (the Sorts of A . s1), (the Sorts of A . s2) by Th11;

      

       A4: ( <*s1, s2*> . 2) = s2 by FINSEQ_1: 44;

      

       A5: ( <*s1, s2*> . 1) = s1 by FINSEQ_1: 44;

       A6:

      now

        let i be Element of NAT ;

        let g be Function, w1,w2 be SortSymbol of S;

        assume i in ( dom <*f*>);

        then i in {1} by FINSEQ_1: 2, FINSEQ_1: 38;

        then i = 1 by TARSKI:def 1;

        hence g = ( <*f*> . i) & w1 = ( <*s1, s2*> . i) & w2 = ( <*s1, s2*> . (i + 1)) implies g is_e.translation_of (A,w1,w2) by A3, A5, A4, FINSEQ_1: 40;

      end;

      ( dom g) = (the Sorts of A . s1) by FUNCT_2:def 1;

      then

       A7: g = ( compose ( <*f*>,(the Sorts of A . s1))) by FUNCT_7: 46;

      

       A8: [s1, s2] in ( TranslationRel S) by A3, Th12;

      hence

       A9: ( TranslationRel S) reduces (s1,s2) by REWRITE1: 15;

       <*s1, s2*> is RedSequence of ( TranslationRel S) by A8, REWRITE1: 7;

      hence thesis by A7, A9, A1, A2, A5, A4, A6, Def6;

    end;

    theorem :: MSUALG_6:18

    

     Th18: for s1,s2,s3 be SortSymbol of S st ( TranslationRel S) reduces (s1,s2) & ( TranslationRel S) reduces (s2,s3) holds for t1 be Translation of A, s1, s2 holds for t2 be Translation of A, s2, s3 holds (t2 * t1) is Translation of A, s1, s3

    proof

      let s1,s2,s3 be SortSymbol of S such that

       A1: ( TranslationRel S) reduces (s1,s2) and

       A2: ( TranslationRel S) reduces (s2,s3);

      let t1 be Translation of A, s1, s2;

      let t2 be Translation of A, s2, s3;

      thus ( TranslationRel S) reduces (s1,s3) by A1, A2, REWRITE1: 16;

      consider q1 be RedSequence of ( TranslationRel S), p1 be Function-yielding FinSequence such that

       A3: t1 = ( compose (p1,(the Sorts of A . s1))) and

       A4: ( len q1) = (( len p1) + 1) and

       A5: s1 = (q1 . 1) and

       A6: s2 = (q1 . ( len q1)) and

       A7: for i be Element of NAT , f be Function, s1,s2 be SortSymbol of S st i in ( dom p1) & f = (p1 . i) & s1 = (q1 . i) & s2 = (q1 . (i + 1)) holds f is_e.translation_of (A,s1,s2) by A1, Def6;

      consider q2 be RedSequence of ( TranslationRel S), p2 be Function-yielding FinSequence such that

       A8: t2 = ( compose (p2,(the Sorts of A . s2))) and

       A9: ( len q2) = (( len p2) + 1) and

       A10: s2 = (q2 . 1) and

       A11: s3 = (q2 . ( len q2)) and

       A12: for i be Element of NAT , f be Function, s1,s2 be SortSymbol of S st i in ( dom p2) & f = (p2 . i) & s1 = (q2 . i) & s2 = (q2 . (i + 1)) holds f is_e.translation_of (A,s1,s2) by A2, Def6;

      reconsider q = (q1 $^ q2) as RedSequence of ( TranslationRel S) by A6, A10, REWRITE1: 8;

      take q, p = (p1 ^ p2);

      ( rng t1) c= (the Sorts of A . s2) by RELAT_1:def 19;

      hence (t2 * t1) = ( compose (p,(the Sorts of A . s1))) by A3, A8, FUNCT_7: 48;

      

       A13: ( len p) = (( len p1) + ( len p2)) by FINSEQ_1: 22;

      consider x2 be object, r2 be FinSequence such that

       A14: q2 = ( <*x2*> ^ r2) and ( len q2) = (( len r2) + 1) by REWRITE1: 5;

      

       A15: x2 = s2 by A10, A14, FINSEQ_1: 41;

      consider r1 be FinSequence, x1 be object such that

       A16: q1 = (r1 ^ <*x1*>) by FINSEQ_1: 46;

      

       A17: q = (r1 ^ q2) by A16, REWRITE1: 2;

      ( len <*x1*>) = 1 by FINSEQ_1: 40;

      then

       A18: ( len q1) = (( len r1) + 1) by A16, FINSEQ_1: 22;

      then

       A19: ( len q) = (( len p1) + ( len q2)) by A4, A17, FINSEQ_1: 22;

      hence ( len q) = (( len p) + 1) by A9, A13;

      x1 = s2 by A6, A16, A18, FINSEQ_1: 42;

      then

       A20: q = (q1 ^ r2) by A16, A14, A17, A15, FINSEQ_1: 32;

      1 <= ( len r1) or ( 0 + 1) > ( len r1);

      then 1 in ( Seg ( len r1)) & ( Seg ( len r1)) = ( dom r1) or 0 <= ( len r1) & 0 >= ( len r1) by FINSEQ_1: 1, FINSEQ_1:def 3, NAT_1: 13;

      then

       A21: (q . 1) = (r1 . 1) & (r1 . 1) = (q1 . 1) or r1 = {} & ( {} ^ q2) = q2 by A16, A17, FINSEQ_1: 34, FINSEQ_1:def 7;

      thus s1 = (q . 1) by A5, A6, A10, A16, A18, A21, REWRITE1: 2;

      ( len q2) in ( dom q2) by FINSEQ_5: 6;

      hence s3 = (q . ( len q)) by A4, A11, A18, A17, A19, FINSEQ_1:def 7;

      let i be Element of NAT ;

      let f be Function, s1,s2 be SortSymbol of S;

      assume that

       A22: i in ( dom p) and

       A23: f = (p . i) and

       A24: s1 = (q . i) and

       A25: s2 = (q . (i + 1));

      per cases ;

        suppose

         A26: i in ( dom p1);

        then (i + 1) in ( dom q1) by A4, FUNCT_7: 22;

        then

         A27: s2 = (q1 . (i + 1)) by A20, A25, FINSEQ_1:def 7;

        i in ( dom q1) by A4, A26, FUNCT_7: 22;

        then

         A28: s1 = (q1 . i) by A20, A24, FINSEQ_1:def 7;

        f = (p1 . i) by A23, A26, FINSEQ_1:def 7;

        hence thesis by A7, A26, A28, A27;

      end;

        suppose not i in ( dom p1);

        then not (i <= ( len p1) & i >= 1) by FINSEQ_3: 25;

        then i >= (( len p1) + 1) by A22, FINSEQ_3: 25, NAT_1: 13;

        then

        consider k be Nat such that

         A29: i = ((( len p1) + 1) + k) by NAT_1: 10;

        

         A30: (( len p1) + ((k + 1) + 1)) = (i + 1) by A29;

        

         A31: (k + 1) >= 1 by NAT_1: 11;

        

         A32: i = (( len p1) + (1 + k)) by A29;

        i <= ( len p) by A22, FINSEQ_3: 25;

        then (k + 1) <= ( len p2) by A13, A32, XREAL_1: 6;

        then

         A33: (k + 1) in ( dom p2) by A31, FINSEQ_3: 25;

        then (k + 1) in ( dom q2) by A9, FUNCT_7: 22;

        then

         A34: s1 = (q2 . (k + 1)) by A4, A18, A17, A24, A32, FINSEQ_1:def 7;

        ((k + 1) + 1) in ( dom q2) by A9, A33, FUNCT_7: 22;

        then

         A35: s2 = (q2 . ((k + 1) + 1)) by A4, A18, A17, A25, A30, FINSEQ_1:def 7;

        f = (p2 . (k + 1)) by A23, A32, A33, FINSEQ_1:def 7;

        hence thesis by A12, A33, A34, A35;

      end;

    end;

    theorem :: MSUALG_6:19

    

     Th19: for s1,s2,s3 be SortSymbol of S st ( TranslationRel S) reduces (s1,s2) holds for t be Translation of A, s1, s2 holds for f be Function st f is_e.translation_of (A,s2,s3) holds (f * t) is Translation of A, s1, s3

    proof

      let s1,s2,s3 be SortSymbol of S such that

       A1: ( TranslationRel S) reduces (s1,s2);

      let t be Translation of A, s1, s2;

      let f be Function;

      assume

       A2: f is_e.translation_of (A,s2,s3);

      then

       A3: f is Translation of A, s2, s3 by Th17;

      ( TranslationRel S) reduces (s2,s3) by A2, Th17;

      hence thesis by A1, A3, Th18;

    end;

    theorem :: MSUALG_6:20

    for s1,s2,s3 be SortSymbol of S st ( TranslationRel S) reduces (s2,s3) holds for f be Function st f is_e.translation_of (A,s1,s2) holds for t be Translation of A, s2, s3 holds (t * f) is Translation of A, s1, s3

    proof

      let s1,s2,s3 be SortSymbol of S such that

       A1: ( TranslationRel S) reduces (s2,s3);

      let f be Function;

      assume

       A2: f is_e.translation_of (A,s1,s2);

      then

       A3: f is Translation of A, s1, s2 by Th17;

      ( TranslationRel S) reduces (s1,s2) by A2, Th17;

      hence thesis by A1, A3, Th18;

    end;

    scheme :: MSUALG_6:sch1

    TranslationInd { S() -> non empty non void ManySortedSign , A() -> non-empty MSAlgebra over S() , P[ set, set, set] } :

for s1,s2 be SortSymbol of S() st ( TranslationRel S()) reduces (s1,s2) holds for t be Translation of A(), s1, s2 holds P[t, s1, s2]

      provided

       A1: for s be SortSymbol of S() holds P[( id (the Sorts of A() . s)), s, s]

       and

       A2: for s1,s2,s3 be SortSymbol of S() st ( TranslationRel S()) reduces (s1,s2) holds for t be Translation of A(), s1, s2 st P[t, s1, s2] holds for f be Function st f is_e.translation_of (A(),s2,s3) holds P[(f * t), s1, s3];

      set S = S(), A = A();

      let s1,s2 be SortSymbol of S such that

       A3: ( TranslationRel S) reduces (s1,s2);

      let t be Translation of A, s1, s2;

      consider q be RedSequence of ( TranslationRel S), p be Function-yielding FinSequence such that

       A4: t = ( compose (p,(the Sorts of A . s1))) and

       A5: ( len q) = (( len p) + 1) and

       A6: s1 = (q . 1) and

       A7: s2 = (q . ( len q)) and

       A8: for i be Element of NAT , f be Function, s1,s2 be SortSymbol of S st i in ( dom p) & f = (p . i) & s1 = (q . i) & s2 = (q . (i + 1)) holds f is_e.translation_of (A,s1,s2) by A3, Def6;

      defpred Q[ Nat] means $1 in ( dom p) implies ex s be SortSymbol of S, t be Translation of A, s1, s, p9 be Function-yielding FinSequence st p9 = (p | ( Seg $1)) & s = (q . ($1 + 1)) & ( TranslationRel S) reduces (s1,s) & t = ( compose (p9,(the Sorts of A . s1))) & P[t, s1, s];

      

       A9: for i be Nat st Q[i] holds Q[(i + 1)]

      proof

        let i be Nat such that

         A10: i in ( dom p) implies ex s be SortSymbol of S, t be Translation of A, s1, s, p9 be Function-yielding FinSequence st p9 = (p | ( Seg i)) & s = (q . (i + 1)) & ( TranslationRel S) reduces (s1,s) & t = ( compose (p9,(the Sorts of A . s1))) & P[t, s1, s] and

         A11: (i + 1) in ( dom p);

        

         A12: ((i + 1) + 1) in ( dom q) by A5, A11, FUNCT_7: 22;

        (i + 1) in ( dom q) by A5, A11, FUNCT_7: 22;

        then [(q . (i + 1)), (q . ((i + 1) + 1))] in ( TranslationRel S) by A12, REWRITE1:def 2;

        then

        reconsider v1 = (q . (i + 1)), v2 = (q . ((i + 1) + 1)) as SortSymbol of S by ZFMISC_1: 87;

        reconsider f = (p . (i + 1)) as Function;

        

         A13: f is_e.translation_of (A,v1,v2) by A8, A11;

        then

        reconsider t = f as Translation of A, v1, v2 by Th17;

        per cases ;

          suppose

           A14: i = 0 ;

          then

          reconsider t as Translation of A, s1, v2 by A6;

          reconsider p9 = (p | ( Seg 1)) as Function-yielding FinSequence by FINSEQ_1: 15;

          

           A15: (t * ( id (the Sorts of A . s1))) = t by FUNCT_2: 17;

          take v2, t, p9;

          thus p9 = (p | ( Seg (i + 1))) & v2 = (q . ((i + 1) + 1)) by A14;

          thus ( TranslationRel S) reduces (s1,v2) by A6, A13, A14, Th17;

          

           A16: ( dom t) = (the Sorts of A . s1) by FUNCT_2:def 1;

          1 in ( Seg 1) by FINSEQ_1: 2, TARSKI:def 1;

          then

           A17: (p9 . 1) = t by A14, FUNCT_1: 49;

          ( 0 + 1) <= ( len p) by A11, A14, FINSEQ_3: 25;

          then ( len p9) = 1 by FINSEQ_1: 17;

          then p9 = <*t*> by A17, FINSEQ_1: 40;

          hence t = ( compose (p9,(the Sorts of A . s1))) by A16, FUNCT_7: 46;

          

           A18: ( TranslationRel S) reduces (s1,s1) by REWRITE1: 12;

          

           A19: P[( id (the Sorts of A . s1)), s1, s1] by A1;

          ( id (the Sorts of A . s1)) is Translation of A, s1, s1 by Th16;

          hence thesis by A2, A6, A8, A11, A14, A18, A15, A19;

        end;

          suppose

           A20: i > 0 ;

          reconsider pp = (p | ( Seg (i + 1))) as FinSequence by FINSEQ_1: 15;

          take v2;

          

           A21: (i + 1) <= ( len p) by A11, FINSEQ_3: 25;

          then

           A22: i <= ( len p) by NAT_1: 13;

          i >= ( 0 + 1) by A20, NAT_1: 13;

          then

          consider s be SortSymbol of S, t9 be Translation of A, s1, s, p9 be Function-yielding FinSequence such that

           A23: p9 = (p | ( Seg i)) and

           A24: s = (q . (i + 1)) and

           A25: ( TranslationRel S) reduces (s1,s) and

           A26: t9 = ( compose (p9,(the Sorts of A . s1))) and

           A27: P[t9, s1, s] by A10, A22, FINSEQ_3: 25;

          reconsider T = (t * t9) as Translation of A, s1, v2 by A8, A11, A24, A25, Th19;

          take T, y = (p9 ^ <*f*>);

          i <= ( len p) by A21, NAT_1: 13;

          then

           A28: ( len p9) = i by A23, FINSEQ_1: 17;

          (i + 1) <= ( len p) by A11, FINSEQ_3: 25;

          then

           A29: ( dom pp) = ( Seg (i + 1)) by FINSEQ_1: 17;

           A30:

          now

            let k be Nat;

            assume

             A31: k in ( Seg (i + 1));

            then k <= (i + 1) by FINSEQ_1: 1;

            then k <= i & k >= 1 or k = (i + 1) by A31, FINSEQ_1: 1, NAT_1: 8;

            then k in ( dom p9) or k = (i + 1) by A28, FINSEQ_3: 25;

            then (y . k) = (p9 . k) & (p9 . k) = (p . k) or (y . k) = (p . k) by A23, A28, FINSEQ_1: 42, FINSEQ_1:def 7, FUNCT_1: 47;

            hence (y . k) = (pp . k) by A29, A31, FUNCT_1: 47;

          end;

          ( len <*f*>) = 1 by FINSEQ_1: 40;

          then ( len y) = (( len p9) + 1) by FINSEQ_1: 22;

          then ( dom y) = ( Seg (i + 1)) by A28, FINSEQ_1:def 3;

          hence y = (p | ( Seg (i + 1))) by A29, A30;

          thus v2 = (q . ((i + 1) + 1));

          ( TranslationRel S) reduces (v1,v2) by A13, Th17;

          hence ( TranslationRel S) reduces (s1,v2) by A24, A25, REWRITE1: 16;

          thus T = ( compose (y,(the Sorts of A . s1))) by A26, FUNCT_7: 41;

          thus thesis by A2, A8, A11, A24, A25, A27;

        end;

      end;

      

       A32: Q[ 0 ] by FINSEQ_3: 25;

      

       A33: for i be Nat holds Q[i] from NAT_1:sch 2( A32, A9);

      per cases ;

        suppose

         A34: p = {} ;

        then

         A35: ( len p) = 0 ;

        t = ( id (the Sorts of A . s1)) by A4, A34, FUNCT_7: 39;

        hence thesis by A1, A5, A6, A7, A35;

      end;

        suppose p <> {} ;

        then ( len p) >= ( 0 + 1) by NAT_1: 13;

        then

         A36: ( len p) in ( dom p) by FINSEQ_3: 25;

        

         A37: (p | ( dom p)) = p;

        ( dom p) = ( Seg ( len p)) by FINSEQ_1:def 3;

        then ex s be SortSymbol of S, t be Translation of A, s1, s, p9 be Function-yielding FinSequence st p9 = p & s = (q . (( len p) + 1)) & ( TranslationRel S) reduces (s1,s) & t = ( compose (p9,(the Sorts of A . s1))) & P[t, s1, s] by A33, A36, A37;

        hence thesis by A4, A5, A7;

      end;

    end;

    theorem :: MSUALG_6:21

    

     Th21: for A1,A2 be non-empty MSAlgebra over S holds for h be ManySortedFunction of A1, A2 st h is_homomorphism (A1,A2) holds for o be OperSymbol of S, i be Element of NAT st i in ( dom ( the_arity_of o)) holds for a be Element of ( Args (o,A1)) holds ((h . ( the_result_sort_of o)) * ( transl (o,i,a,A1))) = (( transl (o,i,(h # a),A2)) * (h . (( the_arity_of o) /. i)))

    proof

      let A1,A2 be non-empty MSAlgebra over S;

      let h be ManySortedFunction of A1, A2 such that

       A1: h is_homomorphism (A1,A2);

      let o be OperSymbol of S, i be Element of NAT such that

       A2: i in ( dom ( the_arity_of o));

      let a be Element of ( Args (o,A1));

      set s1 = (( the_arity_of o) /. i), s2 = ( the_result_sort_of o);

      reconsider T = ( transl (o,i,(h # a),A2)) as Function of (the Sorts of A2 . s1), (the Sorts of A2 . s2) by Th10;

      reconsider t = ( transl (o,i,a,A1)) as Function of (the Sorts of A1 . s1), (the Sorts of A1 . s2) by Th10;

      now

        let x be Element of A1, s1;

        reconsider b = (a +* (i,x)) as Element of ( Args (o,A1)) by Th7;

        

         A3: (h # b) = ((h # a) +* (i,((h # b) . i))) by A2, Th9;

        (h # a) in ( Args (o,A2));

        then

         A4: ((h # b) . i) = ((h . s1) . x) by A2, Th9;

        

        thus (((h . s2) * t) . x) = ((h . s2) . (t . x)) by FUNCT_2: 15

        .= ((h . s2) . (( Den (o,A1)) . b)) by Def4

        .= (( Den (o,A2)) . ((h # a) +* (i,((h . s1) . x)))) by A1, A4, A3

        .= (T . ((h . s1) . x)) by Def4

        .= ((T * (h . s1)) . x) by FUNCT_2: 15;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: MSUALG_6:22

    for h be Endomorphism of A holds for o be OperSymbol of S, i be Element of NAT st i in ( dom ( the_arity_of o)) holds for a be Element of ( Args (o,A)) holds ((h . ( the_result_sort_of o)) * ( transl (o,i,a,A))) = (( transl (o,i,(h # a),A)) * (h . (( the_arity_of o) /. i))) by Def2, Th21;

    theorem :: MSUALG_6:23

    

     Th23: for A1,A2 be non-empty MSAlgebra over S holds for h be ManySortedFunction of A1, A2 st h is_homomorphism (A1,A2) holds for s1,s2 be SortSymbol of S, t be Function st t is_e.translation_of (A1,s1,s2) holds ex T be Function of (the Sorts of A2 . s1), (the Sorts of A2 . s2) st T is_e.translation_of (A2,s1,s2) & (T * (h . s1)) = ((h . s2) * t)

    proof

      let A1,A2 be non-empty MSAlgebra over S;

      let h be ManySortedFunction of A1, A2 such that

       A1: h is_homomorphism (A1,A2);

      let s1,s2 be SortSymbol of S, t be Function;

      assume t is_e.translation_of (A1,s1,s2);

      then

      consider o be OperSymbol of S such that

       A2: ( the_result_sort_of o) = s2 and

       A3: ex i be Element of NAT st i in ( dom ( the_arity_of o)) & (( the_arity_of o) /. i) = s1 & ex a be Function st a in ( Args (o,A1)) & t = ( transl (o,i,a,A1));

      consider i be Element of NAT , a be Function such that

       A4: i in ( dom ( the_arity_of o)) and

       A5: (( the_arity_of o) /. i) = s1 and

       A6: a in ( Args (o,A1)) and

       A7: t = ( transl (o,i,a,A1)) by A3;

      reconsider a as Element of ( Args (o,A1)) by A6;

      reconsider T = ( transl (o,i,(h # a),A2)) as Function of (the Sorts of A2 . s1), (the Sorts of A2 . s2) by A2, A5, Th10;

      take T;

      thus T is_e.translation_of (A2,s1,s2) by A2, A4, A5;

      thus thesis by A1, A2, A4, A5, A7, Th21;

    end;

    theorem :: MSUALG_6:24

    for h be Endomorphism of A holds for s1,s2 be SortSymbol of S, t be Function st t is_e.translation_of (A,s1,s2) holds ex T be Function of (the Sorts of A . s1), (the Sorts of A . s2) st T is_e.translation_of (A,s1,s2) & (T * (h . s1)) = ((h . s2) * t) by Def2, Th23;

    theorem :: MSUALG_6:25

    

     Th25: for A1,A2 be non-empty MSAlgebra over S holds for h be ManySortedFunction of A1, A2 st h is_homomorphism (A1,A2) holds for s1,s2 be SortSymbol of S st ( TranslationRel S) reduces (s1,s2) holds for t be Translation of A1, s1, s2 holds ex T be Translation of A2, s1, s2 st (T * (h . s1)) = ((h . s2) * t)

    proof

      let A1,A2 be non-empty MSAlgebra over S;

      let h be ManySortedFunction of A1, A2 such that

       A1: h is_homomorphism (A1,A2);

      defpred P[ Function, SortSymbol of S, SortSymbol of S] means ex T be Translation of A2, $2, $3 st (T * (h . $2)) = ((h . $3) * $1);

      

       A2: for s1,s2,s3 be SortSymbol of S st ( TranslationRel S) reduces (s1,s2) holds for t be Translation of A1, s1, s2 st P[t, s1, s2] holds for f be Function st f is_e.translation_of (A1,s2,s3) holds P[(f * t), s1, s3]

      proof

        let s1,s2,s3 be SortSymbol of S such that

         A3: ( TranslationRel S) reduces (s1,s2);

        let t be Translation of A1, s1, s2;

        given T be Translation of A2, s1, s2 such that

         A4: (T * (h . s1)) = ((h . s2) * t);

        let f be Function;

        assume f is_e.translation_of (A1,s2,s3);

        then

        consider T1 be Function of (the Sorts of A2 . s2), (the Sorts of A2 . s3) such that

         A5: T1 is_e.translation_of (A2,s2,s3) and

         A6: (T1 * (h . s2)) = ((h . s3) * f) by A1, Th23;

        reconsider T2 = (T1 * T) as Translation of A2, s1, s3 by A3, A5, Th19;

        take T2;

        

        thus (T2 * (h . s1)) = (T1 * (T * (h . s1))) by RELAT_1: 36

        .= (((h . s3) * f) * t) by A4, A6, RELAT_1: 36

        .= ((h . s3) * (f * t)) by RELAT_1: 36;

      end;

      

       A7: for s be SortSymbol of S holds P[( id (the Sorts of A1 . s)), s, s]

      proof

        let s be SortSymbol of S;

        

         A8: (( id (the Sorts of A2 . s)) * (h . s)) = (h . s) by FUNCT_2: 17;

        

         A9: ((h . s) * ( id (the Sorts of A1 . s))) = (h . s) by FUNCT_2: 17;

        ( id (the Sorts of A2 . s)) is Translation of A2, s, s by Th16;

        hence thesis by A8, A9;

      end;

      thus for s1,s2 be SortSymbol of S st ( TranslationRel S) reduces (s1,s2) holds for t be Translation of A1, s1, s2 holds P[t, s1, s2] from TranslationInd( A7, A2);

    end;

    theorem :: MSUALG_6:26

    

     Th26: for h be Endomorphism of A holds for s1,s2 be SortSymbol of S st ( TranslationRel S) reduces (s1,s2) holds for t be Translation of A, s1, s2 holds ex T be Translation of A, s1, s2 st (T * (h . s1)) = ((h . s2) * t) by Def2, Th25;

    begin

    definition

      let S be non empty non void ManySortedSign;

      let A be MSAlgebra over S;

      let R be ManySortedRelation of A;

      :: MSUALG_6:def7

      attr R is compatible means for o be OperSymbol of S, a,b be Function st a in ( Args (o,A)) & b in ( Args (o,A)) & (for n be Element of NAT st n in ( dom ( the_arity_of o)) holds [(a . n), (b . n)] in (R . (( the_arity_of o) /. n))) holds [(( Den (o,A)) . a), (( Den (o,A)) . b)] in (R . ( the_result_sort_of o));

      :: MSUALG_6:def8

      attr R is invariant means

      : Def8: for s1,s2 be SortSymbol of S holds for t be Function st t is_e.translation_of (A,s1,s2) holds for a,b be set st [a, b] in (R . s1) holds [(t . a), (t . b)] in (R . s2);

      :: MSUALG_6:def9

      attr R is stable means

      : Def9: for h be Endomorphism of A holds for s be SortSymbol of S holds for a,b be set st [a, b] in (R . s) holds [((h . s) . a), ((h . s) . b)] in (R . s);

    end

    theorem :: MSUALG_6:27

    for R be MSEquivalence-like ManySortedRelation of A holds R is compatible iff R is MSCongruence of A

    proof

      let R be MSEquivalence-like ManySortedRelation of A;

      hereby

        assume

         A1: R is compatible;

        now

          let o be OperSymbol of S, x,y be Element of ( Args (o,A)) such that

           A2: for n be Nat st n in ( dom x) holds [(x . n), (y . n)] in (R . (( the_arity_of o) /. n));

          now

            let n be Element of NAT ;

            assume n in ( dom ( the_arity_of o));

            then n in ( dom x) by MSUALG_3: 6;

            hence [(x . n), (y . n)] in (R . (( the_arity_of o) /. n)) by A2;

          end;

          hence [(( Den (o,A)) . x), (( Den (o,A)) . y)] in (R . ( the_result_sort_of o)) by A1;

        end;

        hence R is MSCongruence of A by MSUALG_4:def 4;

      end;

      assume

       A3: R is MSCongruence of A;

      let o be OperSymbol of S, x,y be Function such that

       A4: x in ( Args (o,A)) and

       A5: y in ( Args (o,A)) and

       A6: for n be Element of NAT st n in ( dom ( the_arity_of o)) holds [(x . n), (y . n)] in (R . (( the_arity_of o) /. n));

      reconsider x, y as Element of ( Args (o,A)) by A4, A5;

      now

        let n be Nat;

        assume n in ( dom x);

        then n in ( dom ( the_arity_of o)) by MSUALG_3: 6;

        hence [(x . n), (y . n)] in (R . (( the_arity_of o) /. n)) by A6;

      end;

      hence thesis by A3, MSUALG_4:def 4;

    end;

    theorem :: MSUALG_6:28

    

     Th28: for R be ManySortedRelation of A holds R is invariant iff for s1,s2 be SortSymbol of S st ( TranslationRel S) reduces (s1,s2) holds for f be Translation of A, s1, s2 holds for a,b be set st [a, b] in (R . s1) holds [(f . a), (f . b)] in (R . s2)

    proof

      let R be ManySortedRelation of A;

      hereby

        defpred P[ Function, set, set] means for a,b be set st [a, b] in (R . $2) holds [($1 . a), ($1 . b)] in (R . $3);

        deffunc i( SortSymbol of S) = ( id (the Sorts of A . $1));

        assume

         A1: R is invariant;

        

         A2: for s1,s2,s3 be SortSymbol of S st ( TranslationRel S) reduces (s1,s2) holds for t be Translation of A, s1, s2 st P[t, s1, s2] holds for f be Function st f is_e.translation_of (A,s2,s3) holds P[(f * t), s1, s3]

        proof

          let s1,s2,s3 be SortSymbol of S such that ( TranslationRel S) reduces (s1,s2);

          let t be Translation of A, s1, s2 such that

           A3: for a,b be set st [a, b] in (R . s1) holds [(t . a), (t . b)] in (R . s2);

          let f be Function such that

           A4: f is_e.translation_of (A,s2,s3);

          let a,b be set;

          assume

           A5: [a, b] in (R . s1);

          then

          reconsider a9 = a, b9 = b as Element of A, s1 by ZFMISC_1: 87;

           [(t . a9), (t . b9)] in (R . s2) by A3, A5;

          then

           A6: [(f . (t . a9)), (f . (t . b9))] in (R . s3) by A1, A4;

          (f . (t . a9)) = ((f * t) . a9) by FUNCT_2: 15;

          hence thesis by A6, FUNCT_2: 15;

        end;

        

         A7: for s be SortSymbol of S holds P[( id (the Sorts of A . s)), s, s]

        proof

          let s be SortSymbol of S;

          let a,b be set;

          assume

           A8: [a, b] in (R . s);

          then a in (the Sorts of A . s) by ZFMISC_1: 87;

          then

           A9: ( i(s) . a) = a by FUNCT_1: 17;

          b in (the Sorts of A . s) by A8, ZFMISC_1: 87;

          hence thesis by A8, A9, FUNCT_1: 17;

        end;

        thus for s1,s2 be SortSymbol of S st ( TranslationRel S) reduces (s1,s2) holds for t be Translation of A, s1, s2 holds P[t, s1, s2] from TranslationInd( A7, A2);

      end;

      assume

       A10: for s1,s2 be SortSymbol of S st ( TranslationRel S) reduces (s1,s2) holds for f be Translation of A, s1, s2 holds for a,b be set st [a, b] in (R . s1) holds [(f . a), (f . b)] in (R . s2);

      let s1,s2 be SortSymbol of S;

      let t be Function;

      assume

       A11: t is_e.translation_of (A,s1,s2);

      then t is Translation of A, s1, s2 by Th17;

      hence thesis by A10, A11, Th17;

    end;

    registration

      let S be non empty non void ManySortedSign;

      let A be non-empty MSAlgebra over S;

      cluster invariant -> compatible for MSEquivalence-like ManySortedRelation of A;

      coherence

      proof

        let R be MSEquivalence-like ManySortedRelation of A such that

         A1: for s1,s2 be SortSymbol of S holds for t be Function st t is_e.translation_of (A,s1,s2) holds for a,b be set st [a, b] in (R . s1) holds [(t . a), (t . b)] in (R . s2);

        let o be OperSymbol of S, a,b be Function such that

         A2: a in ( Args (o,A)) and

         A3: b in ( Args (o,A)) and

         A4: for n be Element of NAT st n in ( dom ( the_arity_of o)) holds [(a . n), (b . n)] in (R . (( the_arity_of o) /. n));

        

         A5: ( dom ( the_arity_of o)) = ( Seg ( len ( the_arity_of o))) by FINSEQ_1:def 3;

        reconsider a9 = a as Element of ( Args (o,A)) by A2;

        defpred P[ set, set, set] means ex c be Element of ( Args (o,A)) st c = $2 & $3 = (c +* ($1,(b . $1)));

        

         A6: for n be Nat st 1 <= n & n < (( len ( the_arity_of o)) + 1) holds for x be Element of ( Args (o,A)) holds ex y be Element of ( Args (o,A)) st P[n, x, y]

        proof

          let n be Nat;

          assume that

           A7: 1 <= n and

           A8: n < (( len ( the_arity_of o)) + 1);

          let x be Element of ( Args (o,A));

          n <= ( len ( the_arity_of o)) by A8, NAT_1: 13;

          then n in ( dom ( the_arity_of o)) by A7, FINSEQ_3: 25;

          then (b . n) in (the Sorts of A . (( the_arity_of o) /. n)) by A3, Th2;

          then (x +* (n,(b . n))) in ( Args (o,A)) by Th7;

          hence thesis;

        end;

        consider p be FinSequence of ( Args (o,A)) such that

         A9: ( len p) = (( len ( the_arity_of o)) + 1) and

         A10: (p . 1) = a9 or (( len ( the_arity_of o)) + 1) = 0 and

         A11: for i be Nat st 1 <= i & i < (( len ( the_arity_of o)) + 1) holds P[i, (p . i), (p . (i + 1))] from RECDEF_1:sch 4( A6);

        (( len ( the_arity_of o)) + 1) >= 1 by NAT_1: 11;

        then

         A12: (( len ( the_arity_of o)) + 1) in ( dom p) by A9, FINSEQ_3: 25;

        defpred P[ Nat] means $1 <= ( len ( the_arity_of o)) implies ex c be Element of ( Args (o,A)) st c = (p . ($1 + 1)) & (for j be Element of NAT st j in ( dom ( the_arity_of o)) & j > $1 holds (c . j) = (a . j)) & for j be Nat st j in ( Seg $1) holds (c . j) = (b . j);

        

         A13: ( dom ( the_arity_of o)) = ( Seg ( len ( the_arity_of o))) by FINSEQ_1:def 3;

        

         A14: for n be Nat st P[n] holds P[(n + 1)]

        proof

          let i be Nat such that

           A15: i <= ( len ( the_arity_of o)) implies ex c be Element of ( Args (o,A)) st c = (p . (i + 1)) & (for j be Element of NAT st j in ( dom ( the_arity_of o)) & j > i holds (c . j) = (a . j)) & for j be Nat st j in ( Seg i) holds (c . j) = (b . j) and

           A16: (i + 1) <= ( len ( the_arity_of o));

          (i + 1) < (( len ( the_arity_of o)) + 1) by A16, NAT_1: 13;

          then

          consider c be Element of ( Args (o,A)) such that

           A17: c = (p . (i + 1)) and

           A18: (p . ((i + 1) + 1)) = (c +* ((i + 1),(b . (i + 1)))) by A11, NAT_1: 11;

          (i + 1) >= 1 by NAT_1: 11;

          then (i + 1) in ( dom ( the_arity_of o)) by A16, FINSEQ_3: 25;

          then (b . (i + 1)) in (the Sorts of A . (( the_arity_of o) /. (i + 1))) by A3, Th2;

          then

          reconsider d = (p . ((i + 1) + 1)) as Element of ( Args (o,A)) by A18, Th7;

          take d;

          thus d = (p . ((i + 1) + 1));

          ( Seg (i + 1)) c= ( dom ( the_arity_of o)) by A13, A16, FINSEQ_1: 5;

          then

           A19: ( Seg (i + 1)) c= ( dom c) by MSUALG_3: 6;

          i <= (i + 1) by NAT_1: 11;

          then

          consider ci be Element of ( Args (o,A)) such that

           A20: ci = (p . (i + 1)) and

           A21: for j be Element of NAT st j in ( dom ( the_arity_of o)) & j > i holds (ci . j) = (a . j) and

           A22: for j be Nat st j in ( Seg i) holds (ci . j) = (b . j) by A15, A16, XXREAL_0: 2;

          hereby

            let j be Element of NAT ;

            assume that

             A23: j in ( dom ( the_arity_of o)) and

             A24: j > (i + 1);

            j > i by A24, NAT_1: 13;

            then (ci . j) = (a . j) by A21, A23;

            hence (d . j) = (a . j) by A20, A17, A18, A24, FUNCT_7: 32;

          end;

          let j be Nat;

          assume

           A25: j in ( Seg (i + 1));

          then j in (( Seg i) \/ {(i + 1)}) by FINSEQ_1: 9;

          then

           A26: j in ( Seg i) or j in {(i + 1)} by XBOOLE_0:def 3;

          per cases ;

            suppose j = (i + 1);

            hence thesis by A18, A25, A19, FUNCT_7: 31;

          end;

            suppose

             A27: j <> (i + 1);

            then (d . j) = (c . j) by A18, FUNCT_7: 32;

            hence thesis by A20, A22, A17, A26, A27, TARSKI:def 1;

          end;

        end;

        

         A28: P[ 0 ]

        proof

          assume 0 <= ( len ( the_arity_of o));

          take a9;

          thus thesis by A10;

        end;

        

         A29: for i be Nat holds P[i] from NAT_1:sch 2( A28, A14);

        then

        consider c be Element of ( Args (o,A)) such that

         A30: c = (p . (( len ( the_arity_of o)) + 1)) and for j be Element of NAT st j in ( dom ( the_arity_of o)) & j > ( len ( the_arity_of o)) holds (c . j) = (a . j) and

         A31: for j be Nat st j in ( Seg ( len ( the_arity_of o))) holds (c . j) = (b . j);

        defpred P[ Nat] means $1 in ( dom p) implies [(( Den (o,A)) . a9), (( Den (o,A)) . (p . $1))] in (R . ( the_result_sort_of o));

        

         A32: for k be Nat st P[k] holds P[(k + 1)]

        proof

          

           A33: ( Result (o,A)) = (the Sorts of A . ( the_result_sort_of o)) by PRALG_2: 3;

          let i be Nat such that

           A34: i in ( dom p) implies [(( Den (o,A)) . a9), (( Den (o,A)) . (p . i))] in (R . ( the_result_sort_of o)) and

           A35: (i + 1) in ( dom p);

          

           A36: (i + 1) <= ( len p) by A35, FINSEQ_3: 25;

          i <= (i + 1) by NAT_1: 11;

          then

           A37: i <= ( len p) by A36, XXREAL_0: 2;

          per cases ;

            suppose i = 0 ;

            hence thesis by A10, A33, EQREL_1: 5;

          end;

            suppose i > 0 ;

            then

             A38: i >= ( 0 + 1) by NAT_1: 13;

            then

            consider j be Nat such that

             A39: i = (1 + j) by NAT_1: 10;

            reconsider j as Element of NAT by ORDINAL1:def 12;

            i < (( len ( the_arity_of o)) + 1) by A9, A36, NAT_1: 13;

            then

            consider c be Element of ( Args (o,A)) such that

             A40: c = (p . i) and

             A41: (p . (i + 1)) = (c +* (i,(b . i))) by A11, A38;

            

             A42: i <= ( len ( the_arity_of o)) by A9, A36, XREAL_1: 6;

            then

             A43: i in ( dom ( the_arity_of o)) by A38, FINSEQ_3: 25;

            then

            reconsider bi = (b . i), ci = (c . i) as Element of A, (( the_arity_of o) /. i) by A3, Th2;

            j <= i by A39, NAT_1: 11;

            then

             A44: ex c be Element of ( Args (o,A)) st c = (p . (j + 1)) & (for k be Element of NAT st k in ( dom ( the_arity_of o)) & k > j holds (c . k) = (a . k)) & for k be Nat st k in ( Seg j) holds (c . k) = (b . k) by A29, A42, XXREAL_0: 2;

            j < i by A39, NAT_1: 13;

            then (c . i) = (a . i) by A40, A43, A39, A44;

            then

             A45: [ci, bi] in (R . (( the_arity_of o) /. i)) by A4, A43;

            reconsider d = (c +* (i,bi)) as Element of ( Args (o,A)) by Th7;

            

             A46: (( Den (o,A)) . d) = (( transl (o,i,c,A)) . bi) by Def4;

            c = (c +* (i,ci)) by FUNCT_7: 35;

            then

             A47: (( Den (o,A)) . c) = (( transl (o,i,c,A)) . ci) by Def4;

            ( transl (o,i,c,A)) is_e.translation_of (A,(( the_arity_of o) /. i),( the_result_sort_of o)) by A43;

            then [(( Den (o,A)) . c), (( Den (o,A)) . d)] in (R . ( the_result_sort_of o)) by A1, A46, A47, A45;

            hence thesis by A34, A37, A38, A40, A41, EQREL_1: 7, FINSEQ_3: 25;

          end;

        end;

        

         A48: ( dom b) = ( dom ( the_arity_of o)) by A3, MSUALG_3: 6;

        

         A49: P[ 0 ] by FINSEQ_3: 25;

        

         A50: for i be Nat holds P[i] from NAT_1:sch 2( A49, A32);

        

         A51: ( dom c) = ( dom ( the_arity_of o)) by MSUALG_3: 6;

        c = b by A31, A51, A48, A5;

        hence [(( Den (o,A)) . a), (( Den (o,A)) . b)] in (R . ( the_result_sort_of o)) by A50, A30, A12;

      end;

      cluster compatible -> invariant for MSEquivalence-like ManySortedRelation of A;

      coherence

      proof

        let R be MSEquivalence-like ManySortedRelation of A such that

         A52: for o be OperSymbol of S, a,b be Function st a in ( Args (o,A)) & b in ( Args (o,A)) & (for n be Element of NAT st n in ( dom ( the_arity_of o)) holds [(a . n), (b . n)] in (R . (( the_arity_of o) /. n))) holds [(( Den (o,A)) . a), (( Den (o,A)) . b)] in (R . ( the_result_sort_of o));

        let s1,s2 be SortSymbol of S;

        let f be Function;

        given o be OperSymbol of S such that

         A53: ( the_result_sort_of o) = s2 and

         A54: ex i be Element of NAT st i in ( dom ( the_arity_of o)) & (( the_arity_of o) /. i) = s1 & ex a be Function st a in ( Args (o,A)) & f = ( transl (o,i,a,A));

        consider i be Element of NAT , a be Function such that i in ( dom ( the_arity_of o)) and

         A55: (( the_arity_of o) /. i) = s1 and

         A56: a in ( Args (o,A)) and

         A57: f = ( transl (o,i,a,A)) by A54;

        let x,y be set;

        assume

         A58: [x, y] in (R . s1);

        then

         A59: y in (the Sorts of A . s1) by ZFMISC_1: 87;

        

         A60: x in (the Sorts of A . s1) by A58, ZFMISC_1: 87;

        then

        reconsider ax = (a +* (i,x)), ay = (a +* (i,y)) as Element of ( Args (o,A)) by A55, A56, A59, Th7;

        

         A61: (f . y) = (( Den (o,A)) . ay) by A55, A57, A59, Def4;

        

         A62: ( dom a) = ( dom ( the_arity_of o)) by A56, MSUALG_3: 6;

         A63:

        now

          let n be Element of NAT ;

          

           A64: ( dom (the Sorts of A * ( the_arity_of o))) = ( dom ( the_arity_of o)) by PARTFUN1:def 2;

          assume

           A65: n in ( dom ( the_arity_of o));

          then (( the_arity_of o) /. n) = (( the_arity_of o) . n) by PARTFUN1:def 6;

          then

           A66: (the Sorts of A . (( the_arity_of o) /. n)) = ((the Sorts of A * ( the_arity_of o)) . n) by A65, FUNCT_1: 13;

          n = i or n <> i;

          then (ax . n) = x & (ay . n) = y & n = i or (ax . n) = (a . n) & (ay . n) = (a . n) by A62, A65, FUNCT_7: 31, FUNCT_7: 32;

          hence [(ax . n), (ay . n)] in (R . (( the_arity_of o) /. n)) by A55, A58, A65, A64, A66, EQREL_1: 5, MSUALG_3: 6;

        end;

        (f . x) = (( Den (o,A)) . ax) by A55, A57, A60, Def4;

        hence [(f . x), (f . y)] in (R . s2) by A52, A53, A61, A63;

      end;

    end

    registration

      let X be non empty set;

      cluster ( id X) -> non empty;

      coherence ;

    end

    scheme :: MSUALG_6:sch2

    MSRExistence { I() -> non empty set , A() -> non-empty ManySortedSet of I() , P[ object, object, object] } :

ex R be ManySortedRelation of A() st for i be Element of I() holds for a,b be Element of (A() . i) holds [a, b] in (R . i) iff P[i, a, b];

      defpred Q[ object, object] means P[$1, ($2 `1 ), ($2 `2 )];

      deffunc F( object) = [:(A() . $1), (A() . $1):];

      consider R be Function such that

       A1: ( dom R) = I() and

       A2: for i be object st i in I() holds for a be object holds a in (R . i) iff a in F(i) & Q[i, a] from CARD_3:sch 2;

      reconsider R as ManySortedSet of I() by A1, PARTFUN1:def 2, RELAT_1:def 18;

      R is ManySortedRelation of A()

      proof

        let i be set;

        assume

         A3: i in I();

        (R . i) c= [:(A() . i), (A() . i):] by A2, A3;

        hence thesis;

      end;

      then

      reconsider R as ManySortedRelation of A();

      take R;

      let i be Element of I();

      let a,b be Element of (A() . i);

      

       A4: ( [a, b] `2 ) = b;

      

       A5: [a, b] in [:(A() . i), (A() . i):] by ZFMISC_1: 87;

      ( [a, b] `1 ) = a;

      hence thesis by A2, A4, A5;

    end;

    scheme :: MSUALG_6:sch3

    MSRLambdaU { I() -> set , A() -> ManySortedSet of I() , F( object) -> set } :

(ex R be ManySortedRelation of A() st for i be object st i in I() holds (R . i) = F(i)) & for R1,R2 be ManySortedRelation of A() st (for i be object st i in I() holds (R1 . i) = F(i)) & (for i be object st i in I() holds (R2 . i) = F(i)) holds R1 = R2

      provided

       A1: for i be set st i in I() holds F(i) is Relation of (A() . i), (A() . i);

      consider R be ManySortedSet of I() such that

       A2: for i be object st i in I() holds (R . i) = F(i) from PBOOLE:sch 4;

      R is ManySortedRelation of A()

      proof

        let i be set;

        assume

         A3: i in I();

        then F(i) is Relation of (A() . i), (A() . i) by A1;

        hence thesis by A2, A3;

      end;

      hence ex R be ManySortedRelation of A() st for i be object st i in I() holds (R . i) = F(i) by A2;

      let R1,R2 be ManySortedRelation of A() such that

       A4: for i be object st i in I() holds (R1 . i) = F(i) and

       A5: for i be object st i in I() holds (R2 . i) = F(i);

      now

        let i be object;

        assume

         A6: i in I();

        then (R1 . i) = F(i) by A4;

        hence (R1 . i) = (R2 . i) by A5, A6;

      end;

      hence thesis;

    end;

    definition

      let I be set, A be ManySortedSet of I;

      :: MSUALG_6:def10

      func id (I,A) -> ManySortedRelation of A means

      : Def10: for i be object st i in I holds (it . i) = ( id (A . i));

      correctness

      proof

        deffunc F( object) = ( id (A . $1));

        

         A1: for i be set st i in I holds F(i) is Relation of (A . i), (A . i);

        (ex R be ManySortedRelation of A st for i be object st i in I holds (R . i) = F(i)) & for R1,R2 be ManySortedRelation of A st (for i be object st i in I holds (R1 . i) = F(i)) & (for i be object st i in I holds (R2 . i) = F(i)) holds R1 = R2 from MSRLambdaU( A1);

        hence thesis;

      end;

    end

    registration

      let S be non empty non void ManySortedSign;

      let A be non-empty MSAlgebra over S;

      cluster MSEquivalence-like -> non-empty for ManySortedRelation of A;

      coherence

      proof

        let R be ManySortedRelation of A;

        assume

         A1: for i be set, P be Relation of (the Sorts of A . i) st i in the carrier of S & (R . i) = P holds P is Equivalence_Relation of (the Sorts of A . i);

        let i be object;

        assume i in the carrier of S;

        then

        reconsider i as SortSymbol of S;

        (R . i) is Equivalence_Relation of (the Sorts of A . i) by A1;

        hence thesis;

      end;

    end

    registration

      let S be non empty non void ManySortedSign;

      let A be non-empty MSAlgebra over S;

      cluster invariant stable MSEquivalence-like for ManySortedRelation of A;

      existence

      proof

        reconsider R = ( id (the carrier of S,the Sorts of A)) as ManySortedRelation of A;

        take R;

        thus R is invariant

        proof

          let s1,s2 be SortSymbol of S;

          let t be Function;

          assume t is_e.translation_of (A,s1,s2);

          then

          reconsider f = t as Function of (the Sorts of A . s1), (the Sorts of A . s2) by Th11;

          let a,b be set;

          assume

           A1: [a, b] in (R . s1);

          then a in (the Sorts of A . s1) by ZFMISC_1: 87;

          then

           A2: (f . a) in (the Sorts of A . s2) by FUNCT_2: 5;

          (R . s1) = ( id (the Sorts of A . s1)) by Def10;

          then

           A3: a = b by A1, RELAT_1:def 10;

          (R . s2) = ( id (the Sorts of A . s2)) by Def10;

          hence thesis by A3, A2, RELAT_1:def 10;

        end;

        thus R is stable

        proof

          let h be Endomorphism of A;

          let s be SortSymbol of S;

          let a,b be set;

          

           A4: (R . s) = ( id (the Sorts of A . s)) by Def10;

          assume

           A5: [a, b] in (R . s);

          then a in (the Sorts of A . s) by A4, RELAT_1:def 10;

          then

           A6: ((h . s) . a) in (the Sorts of A . s) by FUNCT_2: 5;

          a = b by A4, A5, RELAT_1:def 10;

          hence thesis by A4, A6, RELAT_1:def 10;

        end;

        let i be set, P be Relation of (the Sorts of A . i);

        assume i in the carrier of S;

        then

        reconsider s = i as SortSymbol of S;

        assume (R . i) = P;

        then P = ( id (the Sorts of A . s)) by Def10;

        hence thesis;

      end;

    end

    begin

    reserve S for non empty non void ManySortedSign,

A for non-empty MSAlgebra over S,

R for ManySortedRelation of the Sorts of A;

    scheme :: MSUALG_6:sch4

    MSRelCl { S() -> non empty non void ManySortedSign , A() -> non-empty MSAlgebra over S() , P[ set, set, set], R[ set], R,Q() -> ManySortedRelation of A() } :

R[Q()] & R() c= Q() & for P be ManySortedRelation of A() st R[P] & R() c= P holds Q() c= P

      provided

       A1: for R be ManySortedRelation of A() holds R[R] iff for s1,s2 be SortSymbol of S() holds for f be Function of (the Sorts of A() . s1), (the Sorts of A() . s2) st P[f, s1, s2] holds for a,b be set st [a, b] in (R . s1) holds [(f . a), (f . b)] in (R . s2)

       and

       A2: for s1,s2,s3 be SortSymbol of S() holds for f1 be Function of (the Sorts of A() . s1), (the Sorts of A() . s2) holds for f2 be Function of (the Sorts of A() . s2), (the Sorts of A() . s3) st P[f1, s1, s2] & P[f2, s2, s3] holds P[(f2 * f1), s1, s3]

       and

       A3: for s be SortSymbol of S() holds P[( id (the Sorts of A() . s)), s, s]

       and

       A4: for s be SortSymbol of S(), a,b be Element of A(), s holds [a, b] in (Q() . s) iff ex s9 be SortSymbol of S(), f be Function of (the Sorts of A() . s9), (the Sorts of A() . s), x,y be Element of A(), s9 st P[f, s9, s] & [x, y] in (R() . s9) & a = (f . x) & b = (f . y);

      now

        let s1,s2 be SortSymbol of S();

        set R = Q();

        let f be Function of (the Sorts of A() . s1), (the Sorts of A() . s2);

        assume

         A5: P[f, s1, s2];

        let a,b be set;

        assume

         A6: [a, b] in (R . s1);

        then

         A7: b in (the Sorts of A() . s1) by ZFMISC_1: 87;

        a in (the Sorts of A() . s1) by A6, ZFMISC_1: 87;

        then

        consider s9 be SortSymbol of S(), f9 be Function of (the Sorts of A() . s9), (the Sorts of A() . s1), x,y be Element of A(), s9 such that

         A8: P[f9, s9, s1] and

         A9: [x, y] in (R() . s9) and

         A10: a = (f9 . x) and

         A11: b = (f9 . y) by A4, A6, A7;

        

         A12: (f . a) = ((f * f9) . x) by A10, FUNCT_2: 15;

        

         A13: (f . b) = ((f * f9) . y) by A11, FUNCT_2: 15;

        P[(f * f9), s9, s2] by A2, A5, A8;

        hence [(f . a), (f . b)] in (R . s2) by A4, A9, A12, A13;

      end;

      hence R[Q()] by A1;

      thus R() c= Q()

      proof

        let i be object;

        assume i in the carrier of S();

        then

        reconsider s = i as SortSymbol of S();

        (R() . s) c= (Q() . s)

        proof

          set f = ( id (the Sorts of A() . s));

          let x,y be object;

          assume

           A14: [x, y] in (R() . s);

          then

          reconsider a = x, b = y as Element of A(), s by ZFMISC_1: 87;

          

           A15: (f . b) = b;

          

           A16: P[f, s, s] by A3;

          (f . a) = a;

          hence thesis by A4, A14, A16, A15;

        end;

        hence thesis;

      end;

      let P be ManySortedRelation of A();

      assume that

       A17: R[P] and

       A18: R() c= P;

      let i be object;

      assume i in the carrier of S();

      then

      reconsider s = i as SortSymbol of S();

      (Q() . s) c= (P . s)

      proof

        let x,y be object;

        assume

         A19: [x, y] in (Q() . s);

        then

        reconsider a = x, b = y as Element of A(), s by ZFMISC_1: 87;

        consider s9 be SortSymbol of S(), f be Function of (the Sorts of A() . s9), (the Sorts of A() . s), u,v be Element of A(), s9 such that

         A20: P[f, s9, s] and

         A21: [u, v] in (R() . s9) and

         A22: a = (f . u) and

         A23: b = (f . v) by A4, A19;

        (R() . s9) c= (P . s9) by A18;

        hence thesis by A1, A17, A20, A21, A22, A23;

      end;

      hence thesis;

    end;

     Lm1:

    now

      let S be non empty non void ManySortedSign;

      let A be non-empty MSAlgebra over S;

      let R,Q be ManySortedRelation of A;

      defpred R[ ManySortedRelation of A] means $1 is invariant;

      defpred P[ Function, SortSymbol of S, SortSymbol of S] means ( TranslationRel S) reduces ($2,$3) & $1 is Translation of A, $2, $3;

      assume that

       A1: for s be SortSymbol of S, a,b be Element of A, s holds [a, b] in (Q . s) iff ex s9 be SortSymbol of S, f be Function of (the Sorts of A . s9), (the Sorts of A . s), x,y be Element of A, s9 st P[f, s9, s] & [x, y] in (R . s9) & a = (f . x) & b = (f . y);

      

       A2: for s be SortSymbol of S holds P[( id (the Sorts of A . s)), s, s] by Th16, REWRITE1: 12;

       A3:

      now

        let R be ManySortedRelation of A;

        thus R[R] implies for s1,s2 be SortSymbol of S holds for f be Function of (the Sorts of A . s1), (the Sorts of A . s2) st P[f, s1, s2] holds for a,b be set st [a, b] in (R . s1) holds [(f . a), (f . b)] in (R . s2) by Th28;

        assume for s1,s2 be SortSymbol of S holds for f be Function of (the Sorts of A . s1), (the Sorts of A . s2) st P[f, s1, s2] holds for a,b be set st [a, b] in (R . s1) holds [(f . a), (f . b)] in (R . s2);

        then for s1,s2 be SortSymbol of S st ( TranslationRel S) reduces (s1,s2) holds for f be Translation of A, s1, s2 holds for a,b be set st [a, b] in (R . s1) holds [(f . a), (f . b)] in (R . s2);

        hence R[R] by Th28;

      end;

      

       A4: for s1,s2,s3 be SortSymbol of S holds for f1 be Function of (the Sorts of A . s1), (the Sorts of A . s2) holds for f2 be Function of (the Sorts of A . s2), (the Sorts of A . s3) st P[f1, s1, s2] & P[f2, s2, s3] holds P[(f2 * f1), s1, s3] by Th18, REWRITE1: 16;

      thus R[Q] & R c= Q & for P be ManySortedRelation of A st R[P] & R c= P holds Q c= P from MSRelCl( A3, A4, A2, A1);

    end;

    definition

      let S be non empty non void ManySortedSign;

      let A be non-empty MSAlgebra over S;

      let R be ManySortedRelation of the Sorts of A;

      :: MSUALG_6:def11

      func InvCl R -> invariant ManySortedRelation of A means

      : Def11: R c= it & for Q be invariant ManySortedRelation of A st R c= Q holds it c= Q;

      uniqueness

      proof

        let Q1,Q2 be invariant ManySortedRelation of A such that

         A1: R c= Q1 and

         A2: for Q be invariant ManySortedRelation of A st R c= Q holds Q1 c= Q and

         A3: R c= Q2 and

         A4: for Q be invariant ManySortedRelation of A st R c= Q holds Q2 c= Q;

        Q1 c= Q2 & Q2 c= Q1 by A1, A2, A3, A4;

        hence thesis by PBOOLE: 146;

      end;

      existence

      proof

        defpred P[ Function, SortSymbol of S, SortSymbol of S] means ( TranslationRel S) reduces ($2,$3) & $1 is Translation of A, $2, $3;

        defpred Z[ SortSymbol of S, set, set] means ex s9 be SortSymbol of S, f be Function of (the Sorts of A . s9), (the Sorts of A . $1), x,y be Element of A, s9 st P[f, s9, $1] & [x, y] in (R . s9) & $2 = (f . x) & $3 = (f . y);

        consider Q be ManySortedRelation of the Sorts of A such that

         A5: for s be SortSymbol of S, a,b be Element of A, s holds [a, b] in (Q . s) iff Z[s, a, b] from MSRExistence;

        reconsider Q as ManySortedRelation of A;

        reconsider Q as invariant ManySortedRelation of A by A5, Lm1;

        take Q;

        thus thesis by A5, Lm1;

      end;

    end

    theorem :: MSUALG_6:29

    

     Th29: for R be ManySortedRelation of the Sorts of A holds for s be SortSymbol of S holds for a,b be Element of A, s holds [a, b] in (( InvCl R) . s) iff ex s9 be SortSymbol of S, x,y be Element of A, s9 st ex t be Translation of A, s9, s st ( TranslationRel S) reduces (s9,s) & [x, y] in (R . s9) & a = (t . x) & b = (t . y)

    proof

      let P be ManySortedRelation of the Sorts of A;

      defpred Z[ SortSymbol of S, set, set] means ex s9 be SortSymbol of S, f be Function of (the Sorts of A . s9), (the Sorts of A . $1), x,y be Element of A, s9 st ( TranslationRel S) reduces (s9,$1) & f is Translation of A, s9, $1 & [x, y] in (P . s9) & $2 = (f . x) & $3 = (f . y);

      let s be SortSymbol of S;

      let a,b be Element of A, s;

      consider Q be ManySortedRelation of the Sorts of A such that

       A1: for s be SortSymbol of S, a,b be Element of A, s holds [a, b] in (Q . s) iff Z[s, a, b] from MSRExistence;

      reconsider R = P, Q as ManySortedRelation of A;

      

       A2: R c= Q by A1, Lm1;

      reconsider Q as invariant ManySortedRelation of A by A1, Lm1;

      R c= ( InvCl R) by Def11;

      then

       A3: Q c= ( InvCl R) by A1, Lm1;

      ( InvCl R) c= Q by A2, Def11;

      then

       A4: ( InvCl R) = Q by A3, PBOOLE: 146;

      hereby

        assume [a, b] in (( InvCl P) . s);

        then ex s9 be SortSymbol of S, f be Function of (the Sorts of A . s9), (the Sorts of A . s), x,y be Element of A, s9 st ( TranslationRel S) reduces (s9,s) & f is Translation of A, s9, s & [x, y] in (P . s9) & a = (f . x) & b = (f . y) by A1, A4;

        hence ex s9 be SortSymbol of S, x,y be Element of A, s9 st ex t be Translation of A, s9, s st ( TranslationRel S) reduces (s9,s) & [x, y] in (P . s9) & a = (t . x) & b = (t . y);

      end;

      thus thesis by A1, A4;

    end;

    theorem :: MSUALG_6:30

    

     Th30: for R be stable ManySortedRelation of A holds ( InvCl R) is stable

    proof

      let R be stable ManySortedRelation of A;

      let h be Endomorphism of A;

      let s be SortSymbol of S;

      let a,b be set;

      assume

       A1: [a, b] in (( InvCl R) . s);

      then

       A2: b in (the Sorts of A . s) by ZFMISC_1: 87;

      a in (the Sorts of A . s) by A1, ZFMISC_1: 87;

      then

      consider s9 be SortSymbol of S, x,y be Element of A, s9, t be Translation of A, s9, s such that

       A3: ( TranslationRel S) reduces (s9,s) and

       A4: [x, y] in (R . s9) and

       A5: a = (t . x) and

       A6: b = (t . y) by A1, A2, Th29;

      consider T be Translation of A, s9, s such that

       A7: (T * (h . s9)) = ((h . s) * t) by A3, Th26;

      ((T * (h . s9)) . y) = (T . ((h . s9) . y)) by FUNCT_2: 15;

      then

       A8: (T . ((h . s9) . y)) = ((h . s) . b) by A6, A7, FUNCT_2: 15;

      ((T * (h . s9)) . x) = (T . ((h . s9) . x)) by FUNCT_2: 15;

      then

       A9: (T . ((h . s9) . x)) = ((h . s) . a) by A5, A7, FUNCT_2: 15;

       [((h . s9) . x), ((h . s9) . y)] in (R . s9) by A4, Def9;

      hence thesis by A3, A9, A8, Th29;

    end;

     Lm2:

    now

      let S be non empty non void ManySortedSign;

      let A be non-empty MSAlgebra over S;

      let R,Q be ManySortedRelation of A;

      defpred R[ ManySortedRelation of A] means $1 is stable;

      defpred P[ Function, SortSymbol of S, SortSymbol of S] means $2 = $3 & ex h be Endomorphism of A st $1 = (h . $2);

      

       A1: for s1,s2,s3 be SortSymbol of S holds for f1 be Function of (the Sorts of A . s1), (the Sorts of A . s2) holds for f2 be Function of (the Sorts of A . s2), (the Sorts of A . s3) st P[f1, s1, s2] & P[f2, s2, s3] holds P[(f2 * f1), s1, s3]

      proof

        let s1,s2,s3 be SortSymbol of S;

        let f1 be Function of (the Sorts of A . s1), (the Sorts of A . s2);

        let f2 be Function of (the Sorts of A . s2), (the Sorts of A . s3);

        assume

         A2: s1 = s2;

        given h1 be Endomorphism of A such that

         A3: f1 = (h1 . s1);

        assume

         A4: s2 = s3;

        given h2 be Endomorphism of A such that

         A5: f2 = (h2 . s2);

        thus s1 = s3 by A2, A4;

        reconsider h = (h2 ** h1) as Endomorphism of A;

        take h;

        thus thesis by A2, A3, A5, MSUALG_3: 2;

      end;

      

       A6: for R be ManySortedRelation of A holds R[R] iff for s1,s2 be SortSymbol of S holds for f be Function of (the Sorts of A . s1), (the Sorts of A . s2) st P[f, s1, s2] holds for a,b be set st [a, b] in (R . s1) holds [(f . a), (f . b)] in (R . s2)

      proof

        let R be ManySortedRelation of A;

        thus R is stable implies for s1,s2 be SortSymbol of S holds for f be Function of (the Sorts of A . s1), (the Sorts of A . s2) st s1 = s2 & (ex h be Endomorphism of A st f = (h . s1)) holds for a,b be set st [a, b] in (R . s1) holds [(f . a), (f . b)] in (R . s2);

        assume

         A7: for s1,s2 be SortSymbol of S holds for f be Function of (the Sorts of A . s1), (the Sorts of A . s2) st P[f, s1, s2] holds for a,b be set st [a, b] in (R . s1) holds [(f . a), (f . b)] in (R . s2);

        thus R is stable by A7;

      end;

      

       A8: for s be SortSymbol of S holds P[( id (the Sorts of A . s)), s, s]

      proof

        reconsider h = ( id the Sorts of A) as Endomorphism of A by Th4;

        let s be SortSymbol of S;

        thus s = s;

        take h;

        thus thesis by MSUALG_3:def 1;

      end;

      assume that

       A9: for s be SortSymbol of S, a,b be Element of A, s holds [a, b] in (Q . s) iff ex s9 be SortSymbol of S, f be Function of (the Sorts of A . s9), (the Sorts of A . s), x,y be Element of A, s9 st P[f, s9, s] & [x, y] in (R . s9) & a = (f . x) & b = (f . y);

      thus R[Q] & R c= Q & for P be ManySortedRelation of A st R[P] & R c= P holds Q c= P from MSRelCl( A6, A1, A8, A9);

    end;

    definition

      let S be non empty non void ManySortedSign;

      let A be non-empty MSAlgebra over S;

      let R be ManySortedRelation of the Sorts of A;

      :: MSUALG_6:def12

      func StabCl R -> stable ManySortedRelation of A means

      : Def12: R c= it & for Q be stable ManySortedRelation of A st R c= Q holds it c= Q;

      uniqueness

      proof

        let Q1,Q2 be stable ManySortedRelation of A such that

         A1: R c= Q1 and

         A2: for Q be stable ManySortedRelation of A st R c= Q holds Q1 c= Q and

         A3: R c= Q2 and

         A4: for Q be stable ManySortedRelation of A st R c= Q holds Q2 c= Q;

        Q1 c= Q2 & Q2 c= Q1 by A1, A2, A3, A4;

        hence thesis by PBOOLE: 146;

      end;

      existence

      proof

        defpred P[ Function, SortSymbol of S, SortSymbol of S] means $2 = $3 & ex h be Endomorphism of A st $1 = (h . $2);

        defpred Z[ SortSymbol of S, set, set] means ex s9 be SortSymbol of S, f be Function of (the Sorts of A . s9), (the Sorts of A . $1), x,y be Element of A, s9 st P[f, s9, $1] & [x, y] in (R . s9) & $2 = (f . x) & $3 = (f . y);

        consider Q be ManySortedRelation of the Sorts of A such that

         A5: for s be SortSymbol of S, a,b be Element of A, s holds [a, b] in (Q . s) iff Z[s, a, b] from MSRExistence;

        reconsider Q as ManySortedRelation of A;

        reconsider Q as stable ManySortedRelation of A by A5, Lm2;

        take Q;

        thus thesis by A5, Lm2;

      end;

    end

    theorem :: MSUALG_6:31

    

     Th31: for R be ManySortedRelation of the Sorts of A holds for s be SortSymbol of S holds for a,b be Element of A, s holds [a, b] in (( StabCl R) . s) iff ex x,y be Element of A, s, h be Endomorphism of A st [x, y] in (R . s) & a = ((h . s) . x) & b = ((h . s) . y)

    proof

      let P be ManySortedRelation of the Sorts of A;

      defpred Z[ SortSymbol of S, set, set] means ex s9 be SortSymbol of S, f be Function of (the Sorts of A . s9), (the Sorts of A . $1), x,y be Element of A, s9 st s9 = $1 & (ex h be Endomorphism of A st f = (h . s9)) & [x, y] in (P . s9) & $2 = (f . x) & $3 = (f . y);

      let s be SortSymbol of S;

      let a,b be Element of A, s;

      consider Q be ManySortedRelation of the Sorts of A such that

       A1: for s be SortSymbol of S, a,b be Element of A, s holds [a, b] in (Q . s) iff Z[s, a, b] from MSRExistence;

      reconsider R = P, Q as ManySortedRelation of A;

      

       A2: R c= Q by A1, Lm2;

      reconsider Q as stable ManySortedRelation of A by A1, Lm2;

      R c= ( StabCl R) by Def12;

      then

       A3: Q c= ( StabCl R) by A1, Lm2;

      ( StabCl R) c= Q by A2, Def12;

      then

       A4: ( StabCl R) = Q by A3, PBOOLE: 146;

      hereby

        assume [a, b] in (( StabCl P) . s);

        then ex s9 be SortSymbol of S, f be Function of (the Sorts of A . s9), (the Sorts of A . s), x,y be Element of A, s9 st s9 = s & (ex h be Endomorphism of A st f = (h . s9)) & [x, y] in (P . s9) & a = (f . x) & b = (f . y) by A1, A4;

        hence ex x,y be Element of A, s, h be Endomorphism of A st [x, y] in (P . s) & a = ((h . s) . x) & b = ((h . s) . y);

      end;

      thus thesis by A1, A4;

    end;

    theorem :: MSUALG_6:32

    ( InvCl ( StabCl R)) is stable by Th30;

    definition

      let S be non empty non void ManySortedSign;

      let A be non-empty MSAlgebra over S;

      let R be ManySortedRelation of the Sorts of A;

      :: MSUALG_6:def13

      func TRS R -> invariant stable ManySortedRelation of A means

      : Def13: R c= it & for Q be invariant stable ManySortedRelation of A st R c= Q holds it c= Q;

      uniqueness

      proof

        let Q1,Q2 be invariant stable ManySortedRelation of A such that

         A1: R c= Q1 and

         A2: for Q be invariant stable ManySortedRelation of A st R c= Q holds Q1 c= Q and

         A3: R c= Q2 and

         A4: for Q be invariant stable ManySortedRelation of A st R c= Q holds Q2 c= Q;

        Q1 c= Q2 & Q2 c= Q1 by A1, A2, A3, A4;

        hence thesis by PBOOLE: 146;

      end;

      existence

      proof

        reconsider Q = ( InvCl ( StabCl R)) as invariant stable ManySortedRelation of A by Th30;

        take Q;

        

         A5: ( StabCl R) c= ( InvCl ( StabCl R)) by Def11;

        R c= ( StabCl R) by Def12;

        hence R c= Q by A5, PBOOLE: 13;

        let P be invariant stable ManySortedRelation of A;

        assume R c= P;

        then ( StabCl R) c= P by Def12;

        hence thesis by Def11;

      end;

    end

    registration

      let S be non empty non void ManySortedSign;

      let A be non-empty MSAlgebra over S;

      let R be non-empty ManySortedRelation of A;

      cluster ( InvCl R) -> non-empty;

      coherence

      proof

        let i be object;

        assume i in the carrier of S;

        then

        reconsider s = i as SortSymbol of S;

        set x = the Element of (R . s);

        R c= ( InvCl R) by Def11;

        then

         A1: (R . s) c= (( InvCl R) . s);

        x in (R . s);

        hence thesis by A1;

      end;

      cluster ( StabCl R) -> non-empty;

      coherence

      proof

        let i be object;

        assume i in the carrier of S;

        then

        reconsider s = i as SortSymbol of S;

        set x = the Element of (R . s);

        R c= ( StabCl R) by Def12;

        then

         A2: (R . s) c= (( StabCl R) . s);

        x in (R . s);

        hence thesis by A2;

      end;

      cluster ( TRS R) -> non-empty;

      coherence

      proof

        let i be object;

        assume i in the carrier of S;

        then

        reconsider s = i as SortSymbol of S;

        set x = the Element of (R . s);

        R c= ( TRS R) by Def13;

        then

         A3: (R . s) c= (( TRS R) . s);

        x in (R . s);

        hence thesis by A3;

      end;

    end

    theorem :: MSUALG_6:33

    for R be invariant ManySortedRelation of A holds ( InvCl R) = R

    proof

      let R be invariant ManySortedRelation of A;

      ( InvCl R) c= R & R c= ( InvCl R) by Def11;

      hence thesis by PBOOLE: 146;

    end;

    theorem :: MSUALG_6:34

    for R be stable ManySortedRelation of A holds ( StabCl R) = R

    proof

      let R be stable ManySortedRelation of A;

      ( StabCl R) c= R & R c= ( StabCl R) by Def12;

      hence thesis by PBOOLE: 146;

    end;

    theorem :: MSUALG_6:35

    for R be invariant stable ManySortedRelation of A holds ( TRS R) = R

    proof

      let R be invariant stable ManySortedRelation of A;

      ( TRS R) c= R & R c= ( TRS R) by Def13;

      hence thesis by PBOOLE: 146;

    end;

    theorem :: MSUALG_6:36

    ( StabCl R) c= ( TRS R) & ( InvCl R) c= ( TRS R) & ( StabCl ( InvCl R)) c= ( TRS R)

    proof

      R c= ( TRS R) by Def13;

      hence ( StabCl R) c= ( TRS R) & ( InvCl R) c= ( TRS R) by Def11, Def12;

      hence thesis by Def12;

    end;

    theorem :: MSUALG_6:37

    

     Th37: ( InvCl ( StabCl R)) = ( TRS R)

    proof

      

       A1: ( StabCl R) c= ( InvCl ( StabCl R)) by Def11;

      R c= ( TRS R) by Def13;

      then ( StabCl R) c= ( TRS R) by Def12;

      then

       A2: ( InvCl ( StabCl R)) c= ( TRS R) by Def11;

      

       A3: ( InvCl ( StabCl R)) is invariant stable ManySortedRelation of A by Th30;

      R c= ( StabCl R) by Def12;

      then R c= ( InvCl ( StabCl R)) by A1, PBOOLE: 13;

      then ( TRS R) c= ( InvCl ( StabCl R)) by A3, Def13;

      hence thesis by A2, PBOOLE: 146;

    end;

    theorem :: MSUALG_6:38

    for R be ManySortedRelation of the Sorts of A holds for s be SortSymbol of S, a,b be Element of A, s holds [a, b] in (( TRS R) . s) iff ex s9 be SortSymbol of S st ( TranslationRel S) reduces (s9,s) & ex l,r be Element of A, s9, h be Endomorphism of A, t be Translation of A, s9, s st [l, r] in (R . s9) & a = (t . ((h . s9) . l)) & b = (t . ((h . s9) . r))

    proof

      let R be ManySortedRelation of the Sorts of A;

      let s be SortSymbol of S, a,b be Element of A, s;

      

       A1: ( InvCl ( StabCl R)) = ( TRS R) by Th37;

      hereby

        assume [a, b] in (( TRS R) . s);

        then

        consider s9 be SortSymbol of S, x,y be Element of A, s9, t be Translation of A, s9, s such that

         A2: ( TranslationRel S) reduces (s9,s) and

         A3: [x, y] in (( StabCl R) . s9) and

         A4: a = (t . x) and

         A5: b = (t . y) by A1, Th29;

        take s9;

        thus ( TranslationRel S) reduces (s9,s) by A2;

        reconsider t as Translation of A, s9, s;

        consider u,v be Element of A, s9, h be Endomorphism of A such that

         A6: [u, v] in (R . s9) and

         A7: x = ((h . s9) . u) and

         A8: y = ((h . s9) . v) by A3, Th31;

        take u, v, h;

        take t;

        thus [u, v] in (R . s9) & a = (t . ((h . s9) . u)) & b = (t . ((h . s9) . v)) by A4, A5, A6, A7, A8;

      end;

      given s9 be SortSymbol of S such that

       A9: ( TranslationRel S) reduces (s9,s) and

       A10: ex l,r be Element of A, s9, h be Endomorphism of A, t be Translation of A, s9, s st [l, r] in (R . s9) & a = (t . ((h . s9) . l)) & b = (t . ((h . s9) . r));

      consider l,r be Element of A, s9, h be Endomorphism of A, t be Translation of A, s9, s such that

       A11: [l, r] in (R . s9) and

       A12: a = (t . ((h . s9) . l)) and

       A13: b = (t . ((h . s9) . r)) by A10;

       [((h . s9) . l), ((h . s9) . r)] in (( StabCl R) . s9) by A11, Th31;

      hence thesis by A1, A9, A12, A13, Th29;

    end;

    begin

    theorem :: MSUALG_6:39

    

     Th39: for A be set holds for R,E be Relation of A st for a,b be set st a in A & b in A holds [a, b] in E iff (a,b) are_convertible_wrt R holds E is total symmetric transitive

    proof

      let A be set;

      let R,E be Relation of A;

      set X = A;

      assume

       A1: for a,b be set st a in A & b in A holds [a, b] in E iff (a,b) are_convertible_wrt R;

      now

        let x be object;

        (x,x) are_convertible_wrt R by REWRITE1: 26;

        hence x in X implies [x, x] in E by A1;

      end;

      then

       A2: E is_reflexive_in X by RELAT_2:def 1;

      then

       A3: ( field E) = X by ORDERS_1: 13;

      ( dom E) = X by A2, ORDERS_1: 13;

      hence E is total by PARTFUN1:def 2;

      now

        let x,y be object;

        assume that

         A4: x in X and

         A5: y in X;

        assume [x, y] in E;

        then (x,y) are_convertible_wrt R by A1, A4, A5;

        then (y,x) are_convertible_wrt R by REWRITE1: 31;

        hence [y, x] in E by A1, A4, A5;

      end;

      then E is_symmetric_in X by RELAT_2:def 3;

      hence E is symmetric by A3, RELAT_2:def 11;

      now

        let x,y,z be object;

        assume that

         A6: x in X and

         A7: y in X and

         A8: z in X;

        assume that

         A9: [x, y] in E and

         A10: [y, z] in E;

        

         A11: (y,z) are_convertible_wrt R by A1, A7, A8, A10;

        (x,y) are_convertible_wrt R by A1, A6, A7, A9;

        then (x,z) are_convertible_wrt R by A11, REWRITE1: 30;

        hence [x, z] in E by A1, A6, A8;

      end;

      then E is_transitive_in X by RELAT_2:def 8;

      hence thesis by A3, RELAT_2:def 16;

    end;

    theorem :: MSUALG_6:40

    

     Th40: for A be set, R be Relation of A holds for E be Equivalence_Relation of A st R c= E holds for a,b be object st a in A & (a,b) are_convertible_wrt R holds [a, b] in E

    proof

      let A be set, R be Relation of A;

      let E be Equivalence_Relation of A such that

       A1: R c= E;

      let a,b be object such that

       A2: a in A;

      assume (R \/ (R ~ )) reduces (a,b);

      then

      consider p be RedSequence of (R \/ (R ~ )) such that

       A3: (p . 1) = a and

       A4: (p . ( len p)) = b;

      defpred Q[ Nat] means $1 in ( dom p) implies [a, (p . $1)] in E;

      

       A5: for k be Nat st Q[k] holds Q[(k + 1)]

      proof

        let i be Nat such that

         A6: i in ( dom p) implies [a, (p . i)] in E and

         A7: (i + 1) in ( dom p);

        

         A8: i <= (i + 1) by NAT_1: 11;

        (i + 1) <= ( len p) by A7, FINSEQ_3: 25;

        then

         A9: i <= ( len p) by A8, XXREAL_0: 2;

        per cases ;

          suppose i = 0 ;

          hence thesis by A2, A3, EQREL_1: 5;

        end;

          suppose i > 0 ;

          then

           A10: i >= ( 0 + 1) by NAT_1: 13;

          then i in ( dom p) by A9, FINSEQ_3: 25;

          then

           A11: [(p . i), (p . (i + 1))] in (R \/ (R ~ )) by A7, REWRITE1:def 2;

          then

          reconsider ppi = (p . i), pj = (p . (i + 1)) as Element of A by ZFMISC_1: 87;

           [(p . i), (p . (i + 1))] in R or [(p . i), (p . (i + 1))] in (R ~ ) by A11, XBOOLE_0:def 3;

          then [(p . i), (p . (i + 1))] in R or [(p . (i + 1)), (p . i)] in R by RELAT_1:def 7;

          then [ppi, pj] in E by A1, EQREL_1: 6;

          hence thesis by A6, A9, A10, EQREL_1: 7, FINSEQ_3: 25;

        end;

      end;

      

       A12: ( len p) in ( dom p) by FINSEQ_5: 6;

      

       A13: Q[ 0 ] by FINSEQ_3: 25;

      for i be Nat holds Q[i] from NAT_1:sch 2( A13, A5);

      hence thesis by A4, A12;

    end;

    theorem :: MSUALG_6:41

    

     Th41: for A be non empty set, R be Relation of A holds for a,b be Element of A holds [a, b] in ( EqCl R) iff (a,b) are_convertible_wrt R

    proof

      let A be non empty set, R be Relation of A;

      defpred Z[ object, object] means ($1,$2) are_convertible_wrt R;

      consider Q be Relation of A such that

       A1: for a,b be object holds [a, b] in Q iff a in A & b in A & Z[a, b] from RELSET_1:sch 1;

      for a,b be set st a in A & b in A holds [a, b] in Q iff (a,b) are_convertible_wrt R by A1;

      then

      reconsider Q as Equivalence_Relation of A by Th39;

       A2:

      now

        let E be Equivalence_Relation of A;

        assume

         A3: R c= E;

        thus Q c= E

        proof

          let x,y be object;

          assume

           A4: [x, y] in Q;

          then

           A5: (x,y) are_convertible_wrt R by A1;

          x in A by A1, A4;

          hence thesis by A3, A5, Th40;

        end;

      end;

      R c= Q

      proof

        let a,b be object;

        assume

         A6: [a, b] in R;

        then

         A7: b in A by ZFMISC_1: 87;

        

         A8: (a,b) are_convertible_wrt R by A6, REWRITE1: 29;

        a in A by A6, ZFMISC_1: 87;

        hence thesis by A1, A7, A8;

      end;

      then Q = ( EqCl R) by A2, MSUALG_5:def 1;

      hence thesis by A1;

    end;

    theorem :: MSUALG_6:42

    

     Th42: for S be non empty set, A be non-empty ManySortedSet of S holds for R be ManySortedRelation of A holds for s be Element of S holds for a,b be Element of (A . s) holds [a, b] in (( EqCl R) . s) iff (a,b) are_convertible_wrt (R . s)

    proof

      let S be non empty set, A be non-empty ManySortedSet of S;

      let R be ManySortedRelation of A;

      let s be Element of S;

      (( EqCl R) . s) = ( EqCl (R . s)) by MSUALG_5:def 3;

      hence thesis by Th41;

    end;

    definition

      let S be non empty non void ManySortedSign;

      let A be non-empty MSAlgebra over S;

      mode EquationalTheory of A is stable invariant MSEquivalence-like ManySortedRelation of A;

      let R be ManySortedRelation of A;

      :: MSUALG_6:def14

      func EqCl (R,A) -> MSEquivalence-like ManySortedRelation of A equals ( EqCl R);

      coherence by MSUALG_4:def 3;

    end

    theorem :: MSUALG_6:43

    

     Th43: for R be ManySortedRelation of A holds R c= ( EqCl (R,A))

    proof

      let R be ManySortedRelation of A;

      let i be object;

      assume i in the carrier of S;

      then

      reconsider s = i as SortSymbol of S;

      (( EqCl (R,A)) . s) = ( EqCl (R . s)) by MSUALG_5:def 3;

      hence thesis by MSUALG_5:def 1;

    end;

    theorem :: MSUALG_6:44

    

     Th44: for R be ManySortedRelation of A holds for E be MSEquivalence-like ManySortedRelation of A st R c= E holds ( EqCl (R,A)) c= E

    proof

      let R be ManySortedRelation of A;

      let E be MSEquivalence-like ManySortedRelation of A such that

       A1: R c= E;

      let i be object;

      assume i in the carrier of S;

      then

      reconsider s = i as SortSymbol of S;

      

       A2: (( EqCl (R,A)) . s) = ( EqCl (R . s)) by MSUALG_5:def 3;

      (R . s) c= (E . s) by A1;

      hence thesis by A2, MSUALG_5:def 1;

    end;

    theorem :: MSUALG_6:45

    

     Th45: for R be stable ManySortedRelation of A holds for s be SortSymbol of S holds for a,b be Element of A, s st (a,b) are_convertible_wrt (R . s) holds for h be Endomorphism of A holds (((h . s) . a),((h . s) . b)) are_convertible_wrt (R . s)

    proof

      let R be stable ManySortedRelation of A;

      let s be SortSymbol of S;

      let a,b be Element of A, s;

      assume ((R . s) \/ ((R . s) ~ )) reduces (a,b);

      then

      consider p be RedSequence of ((R . s) \/ ((R . s) ~ )) such that

       A1: (p . 1) = a and

       A2: (p . ( len p)) = b;

      let h be Endomorphism of A;

      defpred P[ Nat] means $1 in ( dom p) implies (((h . s) . a),((h . s) . (p . $1))) are_convertible_wrt (R . s);

      

       A3: for i be Nat st P[i] holds P[(i + 1)]

      proof

        let i be Nat such that

         A4: i in ( dom p) implies (((h . s) . a),((h . s) . (p . i))) are_convertible_wrt (R . s) and

         A5: (i + 1) in ( dom p);

        

         A6: i <= (i + 1) by NAT_1: 11;

        (i + 1) <= ( len p) by A5, FINSEQ_3: 25;

        then

         A7: i <= ( len p) by A6, XXREAL_0: 2;

        per cases ;

          suppose i = 0 ;

          hence thesis by A1, REWRITE1: 26;

        end;

          suppose i > 0 ;

          then

           A8: i >= ( 0 + 1) by NAT_1: 13;

          then i in ( dom p) by A7, FINSEQ_3: 25;

          then

           A9: [(p . i), (p . (i + 1))] in ((R . s) \/ ((R . s) ~ )) by A5, REWRITE1:def 2;

          then

          reconsider ppi = (p . i), pj = (p . (i + 1)) as Element of A, s by ZFMISC_1: 87;

           [(p . i), (p . (i + 1))] in (R . s) or [(p . i), (p . (i + 1))] in ((R . s) ~ ) by A9, XBOOLE_0:def 3;

          then [(p . i), (p . (i + 1))] in (R . s) or [(p . (i + 1)), (p . i)] in (R . s) by RELAT_1:def 7;

          then [((h . s) . ppi), ((h . s) . pj)] in (R . s) or [((h . s) . pj), ((h . s) . ppi)] in (R . s) by Def9;

          then (((h . s) . ppi),((h . s) . pj)) are_convertible_wrt (R . s) or (((h . s) . pj),((h . s) . ppi)) are_convertible_wrt (R . s) by REWRITE1: 29;

          then (((h . s) . ppi),((h . s) . pj)) are_convertible_wrt (R . s) by REWRITE1: 31;

          hence thesis by A4, A7, A8, FINSEQ_3: 25, REWRITE1: 30;

        end;

      end;

      

       A10: ( len p) in ( dom p) by FINSEQ_5: 6;

      

       A11: P[ 0 ] by FINSEQ_3: 25;

      for i be Nat holds P[i] from NAT_1:sch 2( A11, A3);

      hence thesis by A2, A10;

    end;

    theorem :: MSUALG_6:46

    

     Th46: for R be stable ManySortedRelation of A holds ( EqCl (R,A)) is stable

    proof

      let R be stable ManySortedRelation of A;

      let h be Endomorphism of A;

      let s be SortSymbol of S;

      let a,b be set;

      assume

       A1: [a, b] in (( EqCl (R,A)) . s);

      then

      reconsider a, b as Element of A, s by ZFMISC_1: 87;

      (a,b) are_convertible_wrt (R . s) by A1, Th42;

      then (((h . s) . a),((h . s) . b)) are_convertible_wrt (R . s) by Th45;

      hence thesis by Th42;

    end;

    registration

      let S, A;

      let R be stable ManySortedRelation of A;

      cluster ( EqCl (R,A)) -> stable;

      coherence by Th46;

    end

    theorem :: MSUALG_6:47

    

     Th47: for R be invariant ManySortedRelation of A holds for s1,s2 be SortSymbol of S holds for a,b be Element of A, s1 st (a,b) are_convertible_wrt (R . s1) holds for t be Function st t is_e.translation_of (A,s1,s2) holds ((t . a),(t . b)) are_convertible_wrt (R . s2)

    proof

      let R be invariant ManySortedRelation of A;

      let s1,s2 be SortSymbol of S;

      let a,b be Element of A, s1;

      assume ((R . s1) \/ ((R . s1) ~ )) reduces (a,b);

      then

      consider p be RedSequence of ((R . s1) \/ ((R . s1) ~ )) such that

       A1: (p . 1) = a and

       A2: (p . ( len p)) = b;

      let t be Function such that

       A3: t is_e.translation_of (A,s1,s2);

      defpred P[ Nat] means $1 in ( dom p) implies ((t . a),(t . (p . $1))) are_convertible_wrt (R . s2);

      

       A4: for i be Nat st P[i] holds P[(i + 1)]

      proof

        let i be Nat such that

         A5: i in ( dom p) implies ((t . a),(t . (p . i))) are_convertible_wrt (R . s2) and

         A6: (i + 1) in ( dom p);

        

         A7: i <= (i + 1) by NAT_1: 11;

        (i + 1) <= ( len p) by A6, FINSEQ_3: 25;

        then

         A8: i <= ( len p) by A7, XXREAL_0: 2;

        per cases ;

          suppose i = 0 ;

          hence thesis by A1, REWRITE1: 26;

        end;

          suppose i > 0 ;

          then

           A9: i >= ( 0 + 1) by NAT_1: 13;

          then i in ( dom p) by A8, FINSEQ_3: 25;

          then

           A10: [(p . i), (p . (i + 1))] in ((R . s1) \/ ((R . s1) ~ )) by A6, REWRITE1:def 2;

          then

          reconsider ppi = (p . i), pj = (p . (i + 1)) as Element of A, s1 by ZFMISC_1: 87;

           [(p . i), (p . (i + 1))] in (R . s1) or [(p . i), (p . (i + 1))] in ((R . s1) ~ ) by A10, XBOOLE_0:def 3;

          then [(p . i), (p . (i + 1))] in (R . s1) or [(p . (i + 1)), (p . i)] in (R . s1) by RELAT_1:def 7;

          then [(t . ppi), (t . pj)] in (R . s2) or [(t . pj), (t . ppi)] in (R . s2) by A3, Def8;

          then ((t . ppi),(t . pj)) are_convertible_wrt (R . s2) or ((t . pj),(t . ppi)) are_convertible_wrt (R . s2) by REWRITE1: 29;

          then ((t . ppi),(t . pj)) are_convertible_wrt (R . s2) by REWRITE1: 31;

          hence thesis by A5, A8, A9, FINSEQ_3: 25, REWRITE1: 30;

        end;

      end;

      

       A11: ( len p) in ( dom p) by FINSEQ_5: 6;

      

       A12: P[ 0 ] by FINSEQ_3: 25;

      for i be Nat holds P[i] from NAT_1:sch 2( A12, A4);

      hence thesis by A2, A11;

    end;

    theorem :: MSUALG_6:48

    

     Th48: for R be invariant ManySortedRelation of A holds ( EqCl (R,A)) is invariant

    proof

      let R be invariant ManySortedRelation of A;

      let s1,s2 be SortSymbol of S;

      let t be Function;

      assume

       A1: t is_e.translation_of (A,s1,s2);

      then

      reconsider t as Function of (the Sorts of A . s1), (the Sorts of A . s2) by Th11;

      let a,b be set;

      assume

       A2: [a, b] in (( EqCl (R,A)) . s1);

      then

      reconsider a, b as Element of A, s1 by ZFMISC_1: 87;

      (a,b) are_convertible_wrt (R . s1) by A2, Th42;

      then ((t . a),(t . b)) are_convertible_wrt (R . s2) by A1, Th47;

      hence thesis by Th42;

    end;

    registration

      let S, A;

      let R be invariant ManySortedRelation of A;

      cluster ( EqCl (R,A)) -> invariant;

      coherence by Th48;

    end

    theorem :: MSUALG_6:49

    

     Th49: for S be non empty set, A be non-empty ManySortedSet of S holds for R,E be ManySortedRelation of A st for s be Element of S holds for a,b be Element of (A . s) holds [a, b] in (E . s) iff (a,b) are_convertible_wrt (R . s) holds E is MSEquivalence_Relation-like

    proof

      let S be non empty set, A be non-empty ManySortedSet of S;

      let R,E be ManySortedRelation of A;

      assume

       A1: for s be Element of S holds for a,b be Element of (A . s) holds [a, b] in (E . s) iff (a,b) are_convertible_wrt (R . s);

      let i be set, P be Relation of (A . i);

      assume i in S;

      then

      reconsider s = i as Element of S;

      for a,b be set st a in (A . s) & b in (A . s) holds [a, b] in (E . s) iff (a,b) are_convertible_wrt (R . s) by A1;

      hence thesis by Th39;

    end;

    theorem :: MSUALG_6:50

    

     Th50: for R,E be ManySortedRelation of A st for s be SortSymbol of S, a,b be Element of A, s holds [a, b] in (E . s) iff (a,b) are_convertible_wrt (( TRS R) . s) holds E is EquationalTheory of A

    proof

      let R,E be ManySortedRelation of A;

      assume

       A1: for s be SortSymbol of S, a,b be Element of A, s holds [a, b] in (E . s) iff (a,b) are_convertible_wrt (( TRS R) . s);

      

       A2: E is stable

      proof

        let h be Endomorphism of A;

        let s be SortSymbol of S;

        let a,b be set;

        assume

         A3: [a, b] in (E . s);

        then

        reconsider x = a, y = b as Element of A, s by ZFMISC_1: 87;

        reconsider a9 = ((h . s) . x), b9 = ((h . s) . y) as Element of A, s;

        (x,y) are_convertible_wrt (( TRS R) . s) by A1, A3;

        then (a9,b9) are_convertible_wrt (( TRS R) . s) by Th45;

        hence thesis by A1;

      end;

      

       A4: E is invariant

      proof

        let s1,s2 be SortSymbol of S;

        let t be Function;

        assume

         A5: t is_e.translation_of (A,s1,s2);

        then

        reconsider f = t as Function of (the Sorts of A . s1), (the Sorts of A . s2) by Th11;

        let a,b be set;

        assume

         A6: [a, b] in (E . s1);

        then

        reconsider x = a, y = b as Element of A, s1 by ZFMISC_1: 87;

        (x,y) are_convertible_wrt (( TRS R) . s1) by A1, A6;

        then

         A7: ((t . x),(t . y)) are_convertible_wrt (( TRS R) . s2) by A5, Th47;

        

         A8: (t . y) = (f . y);

        (t . x) = (f . x);

        hence thesis by A1, A8, A7;

      end;

      E is MSEquivalence_Relation-like by A1, Th49;

      hence thesis by A2, A4, MSUALG_4:def 3;

    end;

    theorem :: MSUALG_6:51

    

     Th51: for S be non empty set, A be non-empty ManySortedSet of S holds for R be ManySortedRelation of A holds for E be MSEquivalence_Relation-like ManySortedRelation of A st R c= E holds for s be Element of S holds for a,b be Element of (A . s) st (a,b) are_convertible_wrt (R . s) holds [a, b] in (E . s)

    proof

      let S be non empty set, A be non-empty ManySortedSet of S;

      let R be ManySortedRelation of A;

      let E be MSEquivalence_Relation-like ManySortedRelation of A such that

       A1: R c= E;

      let s be Element of S;

      

       A2: (E . s) is Equivalence_Relation of (A . s) by MSUALG_4:def 2;

      (R . s) c= (E . s) by A1;

      hence thesis by A2, Th40;

    end;

    definition

      let S be non empty non void ManySortedSign;

      let A be non-empty MSAlgebra over S;

      let R be ManySortedRelation of the Sorts of A;

      :: MSUALG_6:def15

      func EqTh R -> EquationalTheory of A means

      : Def15: R c= it & for Q be EquationalTheory of A st R c= Q holds it c= Q;

      uniqueness

      proof

        let Q1,Q2 be EquationalTheory of A such that

         A1: R c= Q1 and

         A2: for Q be EquationalTheory of A st R c= Q holds Q1 c= Q and

         A3: R c= Q2 and

         A4: for Q be EquationalTheory of A st R c= Q holds Q2 c= Q;

        Q1 c= Q2 & Q2 c= Q1 by A1, A2, A3, A4;

        hence thesis by PBOOLE: 146;

      end;

      existence

      proof

        defpred Z[ SortSymbol of S, set, set] means ($2,$3) are_convertible_wrt (( TRS R) . $1);

        consider P be ManySortedRelation of the Sorts of A such that

         A5: for s be SortSymbol of S holds for a,b be Element of A, s holds [a, b] in (P . s) iff Z[s, a, b] from MSRExistence;

        reconsider P as ManySortedRelation of A;

        reconsider P as EquationalTheory of A by A5, Th50;

        take P;

        thus R c= P

        proof

          let i be object;

          assume i in the carrier of S;

          then

          reconsider s = i as SortSymbol of S;

          (R . s) c= (P . s)

          proof

            let x,y be object;

            assume

             A6: [x, y] in (R . s);

            then

            reconsider a = x, b = y as Element of A, s by ZFMISC_1: 87;

            R c= ( TRS R) by Def13;

            then (R . s) c= (( TRS R) . s);

            then (a,b) are_convertible_wrt (( TRS R) . s) by A6, REWRITE1: 29;

            hence thesis by A5;

          end;

          hence thesis;

        end;

        let Q be EquationalTheory of A;

        assume

         A7: R c= Q;

        let i be object;

        assume i in the carrier of S;

        then

        reconsider s = i as SortSymbol of S;

        

         A8: ( TRS R) c= Q by A7, Def13;

        (P . s) c= (Q . s)

        proof

          let x,y be object;

          assume

           A9: [x, y] in (P . s);

          then

          reconsider a = x, b = y as Element of A, s by ZFMISC_1: 87;

          (a,b) are_convertible_wrt (( TRS R) . s) by A5, A9;

          hence thesis by A8, Th51;

        end;

        hence thesis;

      end;

    end

    theorem :: MSUALG_6:52

    for R be ManySortedRelation of A holds ( EqCl (R,A)) c= ( EqTh R) & ( InvCl R) c= ( EqTh R) & ( StabCl R) c= ( EqTh R) & ( TRS R) c= ( EqTh R)

    proof

      let R be ManySortedRelation of A;

      

       A1: R c= ( EqTh R) by Def15;

      hence ( EqCl (R,A)) c= ( EqTh R) by Th44;

      thus thesis by A1, Def11, Def12, Def13;

    end;

    theorem :: MSUALG_6:53

    for R be ManySortedRelation of A holds for s be SortSymbol of S, a,b be Element of A, s holds [a, b] in (( EqTh R) . s) iff (a,b) are_convertible_wrt (( TRS R) . s)

    proof

      let R be ManySortedRelation of A;

      let s be SortSymbol of S, a,b be Element of A, s;

      defpred Z[ SortSymbol of S, set, set] means ($2,$3) are_convertible_wrt (( TRS R) . $1);

      consider P be ManySortedRelation of the Sorts of A such that

       A1: for s be SortSymbol of S holds for a,b be Element of A, s holds [a, b] in (P . s) iff Z[s, a, b] from MSRExistence;

      reconsider P as ManySortedRelation of A;

      reconsider P as EquationalTheory of A by A1, Th50;

      R c= P

      proof

        let i be object;

        assume i in the carrier of S;

        then

        reconsider s = i as SortSymbol of S;

        (R . s) c= (P . s)

        proof

          let x,y be object;

          assume

           A2: [x, y] in (R . s);

          then

          reconsider a = x, b = y as Element of A, s by ZFMISC_1: 87;

          R c= ( TRS R) by Def13;

          then (R . s) c= (( TRS R) . s);

          then (a,b) are_convertible_wrt (( TRS R) . s) by A2, REWRITE1: 29;

          hence thesis by A1;

        end;

        hence thesis;

      end;

      then ( EqTh R) c= P by Def15;

      then (( EqTh R) . s) c= (P . s);

      hence [a, b] in (( EqTh R) . s) implies (a,b) are_convertible_wrt (( TRS R) . s) by A1;

      R c= ( EqTh R) by Def15;

      then ( TRS R) c= ( EqTh R) by Def13;

      hence thesis by Th51;

    end;

    theorem :: MSUALG_6:54

    for R be ManySortedRelation of A holds ( EqTh R) = ( EqCl (( TRS R),A))

    proof

      let R be ManySortedRelation of A;

      

       A1: ( TRS R) c= ( EqCl (( TRS R),A)) by Th43;

      R c= ( TRS R) by Def13;

      then R c= ( EqCl (( TRS R),A)) by A1, PBOOLE: 13;

      then

       A2: ( EqTh R) c= ( EqCl (( TRS R),A)) by Def15;

      R c= ( EqTh R) by Def15;

      then ( TRS R) c= ( EqTh R) by Def13;

      then ( EqCl (( TRS R),A)) c= ( EqTh R) by Th44;

      hence thesis by A2, PBOOLE: 146;

    end;