osalg_1.miz



    begin

    registration

      let I be set, f be ManySortedSet of I, p be FinSequence of I;

      cluster (f * p) -> FinSequence-like;

      coherence

      proof

        ( rng p) c= I;

        then ( rng p) c= ( dom f) by PARTFUN1:def 2;

        

        then ( dom (f * p)) = ( dom p) by RELAT_1: 27

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

        hence thesis by FINSEQ_1:def 2;

      end;

    end

    

     Lm1: for I be set, f be ManySortedSet of I, p be FinSequence of I holds ( dom (f * p)) = ( dom p) & ( len (f * p)) = ( len p)

    proof

      let I be set, f be ManySortedSet of I, p be FinSequence of I;

      reconsider q = (f * p) as FinSequence;

      ( rng p) c= I;

      then ( rng p) c= ( dom f) by PARTFUN1:def 2;

      then ( len q) = ( len p) by FINSEQ_2: 29;

      hence thesis by FINSEQ_3: 29;

    end;

    definition

      let S be non empty ManySortedSign;

      mode SortSymbol of S is Element of S;

    end

    definition

      let S be non empty ManySortedSign;

      mode OperSymbol of S is Element of the carrier' of S;

    end

    definition

      struct ( ManySortedSign) OverloadedMSSign (# the carrier -> set,

the carrier' -> set,

the Overloading -> Equivalence_Relation of the carrier',

the Arity -> Function of the carrier', ( the carrier * ),

the ResultSort -> Function of the carrier', the carrier #)

       attr strict strict;

    end

    definition

      struct ( ManySortedSign, RelStr) RelSortedSign (# the carrier -> set,

the InternalRel -> Relation of the carrier,

the carrier' -> set,

the Arity -> Function of the carrier', ( the carrier * ),

the ResultSort -> Function of the carrier', the carrier #)

       attr strict strict;

    end

    definition

      struct ( OverloadedMSSign, RelSortedSign) OverloadedRSSign (# the carrier -> set,

the InternalRel -> Relation of the carrier,

the carrier' -> set,

the Overloading -> Equivalence_Relation of the carrier',

the Arity -> Function of the carrier', ( the carrier * ),

the ResultSort -> Function of the carrier', the carrier #)

       attr strict strict;

    end

    reserve A,O for non empty set,

R for Order of A,

Ol for Equivalence_Relation of O,

f for Function of O, (A * ),

g for Function of O, A;

    theorem :: OSALG_1:1

    

     Th1: OverloadedRSSign (# A, R, O, Ol, f, g #) is non empty non void reflexive transitive antisymmetric

    proof

      set RS0 = OverloadedRSSign (# A, R, O, Ol, f, g #);

      

       A1: ( field the InternalRel of RS0) = the carrier of RS0 by ORDERS_1: 12;

      then

       A2: the InternalRel of RS0 is_antisymmetric_in the carrier of RS0 by RELAT_2:def 12;

      the InternalRel of RS0 is_reflexive_in the carrier of RS0 & the InternalRel of RS0 is_transitive_in the carrier of RS0 by A1, RELAT_2:def 9, RELAT_2:def 16;

      hence thesis by A2, ORDERS_2:def 2, ORDERS_2:def 3, ORDERS_2:def 4;

    end;

    registration

      let A, R, O, Ol, f, g;

      cluster OverloadedRSSign (# A, R, O, Ol, f, g #) -> strict non empty reflexive transitive antisymmetric;

      coherence by Th1;

    end

    begin

    reserve S for OverloadedRSSign;

    definition

      let S;

      :: OSALG_1:def1

      attr S is order-sorted means

      : Def1: S is reflexive transitive antisymmetric;

    end

    registration

      cluster order-sorted -> reflexive transitive antisymmetric for OverloadedRSSign;

      coherence ;

      cluster strict non empty non void order-sorted for OverloadedRSSign;

      existence

      proof

        set A = the non empty set, R = the Order of A, O = the non empty set, Ol = the Equivalence_Relation of O, f = the Function of O, (A * ), g = the Function of O, A;

        take OverloadedRSSign (# A, R, O, Ol, f, g #);

        thus thesis;

      end;

    end

    registration

      cluster non empty non void for OverloadedMSSign;

      existence

      proof

        set X = the non empty non void OverloadedRSSign;

        take X;

        thus thesis;

      end;

    end

    definition

      let S be non empty non void OverloadedMSSign;

      let x,y be OperSymbol of S;

      :: OSALG_1:def2

      pred x ~= y means

      : Def2: [x, y] in the Overloading of S;

      symmetry

      proof

        let x,y be OperSymbol of S;

        ( field the Overloading of S) = the carrier' of S by ORDERS_1: 12;

        then the Overloading of S is_symmetric_in the carrier' of S by RELAT_2:def 11;

        hence thesis by RELAT_2:def 3;

      end;

      reflexivity

      proof

        let x be OperSymbol of S;

        ( field the Overloading of S) = the carrier' of S by ORDERS_1: 12;

        then the Overloading of S is_reflexive_in the carrier' of S by RELAT_2:def 9;

        hence thesis by RELAT_2:def 1;

      end;

    end

    theorem :: OSALG_1:2

    

     Th2: for S be non empty non void OverloadedMSSign, o,o1,o2 be OperSymbol of S holds o ~= o1 & o1 ~= o2 implies o ~= o2

    proof

      let S be non empty non void OverloadedMSSign;

      let o,o1,o2 be OperSymbol of S;

      ( field the Overloading of S) = the carrier' of S by ORDERS_1: 12;

      then

       A1: the Overloading of S is_transitive_in the carrier' of S by RELAT_2:def 16;

      assume o ~= o1 & o1 ~= o2;

      then [o, o1] in the Overloading of S & [o1, o2] in the Overloading of S;

      then [o, o2] in the Overloading of S by A1, RELAT_2:def 8;

      hence thesis;

    end;

    definition

      let S be non empty non void OverloadedMSSign;

      :: OSALG_1:def3

      attr S is discernable means

      : Def3: for x,y be OperSymbol of S st x ~= y & ( the_arity_of x) = ( the_arity_of y) & ( the_result_sort_of x) = ( the_result_sort_of y) holds x = y;

      :: OSALG_1:def4

      attr S is op-discrete means the Overloading of S = ( id the carrier' of S);

    end

    theorem :: OSALG_1:3

    

     Th3: for S be non empty non void OverloadedMSSign holds S is op-discrete iff for x,y be OperSymbol of S st x ~= y holds x = y

    proof

      let S be non empty non void OverloadedMSSign;

      set d = ( id the carrier' of S);

      set opss = the carrier' of S;

      set ol = the Overloading of S;

      thus S is op-discrete implies for x,y be OperSymbol of S st x ~= y holds x = y by RELAT_1:def 10;

      assume

       A1: for x,y be OperSymbol of S st x ~= y holds x = y;

      now

        let x,y be object;

        thus [x, y] in ol implies x in opss & x = y

        proof

          assume

           A2: [x, y] in ol;

          then ex x1,y1 be object st [x, y] = [x1, y1] & x1 in opss & y1 in opss by RELSET_1: 2;

          then

          reconsider x2 = x, y2 = y as OperSymbol of S by XTUPLE_0: 1;

          x2 ~= y2 by A2;

          hence thesis by A1;

        end;

        assume x in opss & x = y;

        hence [x, y] in ol by Def2;

      end;

      hence the Overloading of S = d by RELAT_1:def 10;

    end;

    theorem :: OSALG_1:4

    

     Th4: for S be non empty non void OverloadedMSSign holds S is op-discrete implies S is discernable by Th3;

    begin

    reserve S0 for non empty non void ManySortedSign;

    definition

      let S0;

      :: OSALG_1:def5

      func OSSign S0 -> strict non empty non void order-sorted OverloadedRSSign means

      : Def5: the carrier of S0 = the carrier of it & ( id the carrier of S0) = the InternalRel of it & the carrier' of S0 = the carrier' of it & ( id the carrier' of S0) = the Overloading of it & the Arity of S0 = the Arity of it & the ResultSort of S0 = the ResultSort of it ;

      existence

      proof

        set s = OverloadedRSSign (# the carrier of S0, ( id the carrier of S0), the carrier' of S0, ( id the carrier' of S0), the Arity of S0, the ResultSort of S0 #);

        reconsider s1 = s as strict non empty non void order-sorted OverloadedRSSign by Def1;

        take s1;

        thus thesis;

      end;

      uniqueness ;

    end

    theorem :: OSALG_1:5

    

     Th5: ( OSSign S0) is discrete op-discrete

    proof

      set s = ( OSSign S0);

      set ol = the Overloading of s;

      the carrier of S0 = the carrier of ( OSSign S0) & ( id the carrier of S0) = the InternalRel of ( OSSign S0) by Def5;

      hence ( OSSign S0) is discrete by ORDERS_3:def 1;

      the Overloading of ( OSSign S0) = ( id the carrier' of S0) by Def5;

      then for x,y be OperSymbol of s st x ~= y holds x = y by RELAT_1:def 10;

      hence thesis by Th3;

    end;

    registration

      cluster discrete op-discrete discernable for strict non empty non void order-sorted OverloadedRSSign;

      existence

      proof

        set S0 = the non empty non void ManySortedSign;

        take s = ( OSSign S0);

        thus s is discrete op-discrete by Th5;

        hence thesis by Th4;

      end;

    end

    registration

      cluster op-discrete -> discernable for non empty non void OverloadedRSSign;

      coherence by Th4;

    end

    registration

      let S0;

      cluster ( OSSign S0) -> discrete op-discrete;

      coherence by Th5;

    end

    definition

      mode OrderSortedSign is discernable non empty non void order-sorted OverloadedRSSign;

    end

    reserve S for non empty Poset;

    reserve s1,s2 for Element of S;

    reserve w1,w2 for Element of (the carrier of S * );

    definition

      let S;

      let w1,w2 be Element of (the carrier of S * );

      :: OSALG_1:def6

      pred w1 <= w2 means ( len w1) = ( len w2) & for i be set st i in ( dom w1) holds for s1, s2 st s1 = (w1 . i) & s2 = (w2 . i) holds s1 <= s2;

      reflexivity ;

    end

    theorem :: OSALG_1:6

    

     Th6: for w1,w2 be Element of (the carrier of S * ) holds w1 <= w2 & w2 <= w1 implies w1 = w2

    proof

      let w1,w2 be Element of (the carrier of S * );

      assume that

       A1: w1 <= w2 and

       A2: w2 <= w1;

      ( len w1) = ( len w2) by A1;

      then

       A3: ( dom w1) = ( dom w2) by FINSEQ_3: 29;

      for i be object st i in ( dom w1) holds (w1 . i) = (w2 . i)

      proof

        let i be object such that

         A4: i in ( dom w1);

        reconsider s3 = (w1 . i), s4 = (w2 . i) as Element of S by A3, A4, PARTFUN1: 4;

        s3 <= s4 & s4 <= s3 by A1, A2, A3, A4;

        hence thesis by ORDERS_2: 2;

      end;

      hence thesis by A3, FUNCT_1: 2;

    end;

    theorem :: OSALG_1:7

    

     Th7: S is discrete & w1 <= w2 implies w1 = w2

    proof

      assume that

       A1: S is discrete and

       A2: w1 <= w2;

      reconsider S1 = S as discrete non empty Poset by A1;

      ( len w1) = ( len w2) by A2;

      then

       A3: ( dom w1) = ( dom w2) by FINSEQ_3: 29;

      for i be object st i in ( dom w1) holds (w1 . i) = (w2 . i)

      proof

        let i be object such that

         A4: i in ( dom w1);

        reconsider s3 = (w1 . i), s4 = (w2 . i) as Element of S by A3, A4, PARTFUN1: 4;

        reconsider s5 = s3, s6 = s4 as Element of S1;

        s3 <= s4 by A2, A4;

        then s5 = s6 by ORDERS_3: 1;

        hence thesis;

      end;

      hence thesis by A3, FUNCT_1: 2;

    end;

    reserve S for OrderSortedSign;

    reserve o,o1,o2 for OperSymbol of S;

    reserve w1 for Element of (the carrier of S * );

    theorem :: OSALG_1:8

    

     Th8: S is discrete & o1 ~= o2 & ( the_arity_of o1) <= ( the_arity_of o2) & ( the_result_sort_of o1) <= ( the_result_sort_of o2) implies o1 = o2

    proof

      assume

       A1: S is discrete;

      then

      reconsider S1 = S as discrete OrderSortedSign;

      reconsider s1 = ( the_result_sort_of o1), s2 = ( the_result_sort_of o2) as SortSymbol of S1;

      assume that

       A2: o1 ~= o2 and

       A3: ( the_arity_of o1) <= ( the_arity_of o2) and

       A4: ( the_result_sort_of o1) <= ( the_result_sort_of o2);

      

       A5: s1 = s2 by A4, ORDERS_3: 1;

      ( the_arity_of o1) = ( the_arity_of o2) by A1, A3, Th7;

      hence thesis by A2, A5, Def3;

    end;

    definition

      let S;

      let o;

      :: OSALG_1:def7

      attr o is monotone means

      : Def7: for o2 st o ~= o2 & ( the_arity_of o) <= ( the_arity_of o2) holds ( the_result_sort_of o) <= ( the_result_sort_of o2);

    end

    definition

      let S;

      :: OSALG_1:def8

      attr S is monotone means

      : Def8: for o be OperSymbol of S holds o is monotone;

    end

    theorem :: OSALG_1:9

    

     Th9: S is op-discrete implies S is monotone

    proof

      set ol = the Overloading of S;

      assume S is op-discrete;

      then

       A1: ol = ( id the carrier' of S);

      let o be OperSymbol of S;

      let o2 be OperSymbol of S;

      assume o ~= o2;

      then [o, o2] in ol;

      hence thesis by A1, RELAT_1:def 10;

    end;

    registration

      cluster monotone for OrderSortedSign;

      existence

      proof

        set S = the op-discrete OrderSortedSign;

        take S;

        thus thesis by Th9;

      end;

    end

    registration

      let S be monotone OrderSortedSign;

      cluster monotone for OperSymbol of S;

      existence

      proof

        set o = the OperSymbol of S;

        take o;

        thus thesis by Def8;

      end;

    end

    registration

      let S be monotone OrderSortedSign;

      cluster -> monotone for OperSymbol of S;

      coherence by Def8;

    end

    registration

      cluster op-discrete -> monotone for OrderSortedSign;

      coherence by Th9;

    end

    theorem :: OSALG_1:10

    S is monotone & ( the_arity_of o1) = {} & o1 ~= o2 & ( the_arity_of o2) = {} implies o1 = o2

    proof

      assume that

       A1: S is monotone and

       A2: ( the_arity_of o1) = {} & o1 ~= o2 & ( the_arity_of o2) = {} ;

      ( the_result_sort_of o1) <= ( the_result_sort_of o2) & ( the_result_sort_of o2) <= ( the_result_sort_of o1) by A1, A2, Def7;

      then ( the_result_sort_of o1) = ( the_result_sort_of o2) by ORDERS_2: 2;

      hence thesis by A2, Def3;

    end;

    definition

      let S, o, o1, w1;

      :: OSALG_1:def9

      pred o1 has_least_args_for o,w1 means o ~= o1 & w1 <= ( the_arity_of o1) & for o2 st o ~= o2 & w1 <= ( the_arity_of o2) holds ( the_arity_of o1) <= ( the_arity_of o2);

      :: OSALG_1:def10

      pred o1 has_least_sort_for o,w1 means o ~= o1 & w1 <= ( the_arity_of o1) & for o2 st o ~= o2 & w1 <= ( the_arity_of o2) holds ( the_result_sort_of o1) <= ( the_result_sort_of o2);

    end

    definition

      let S, o, o1, w1;

      :: OSALG_1:def11

      pred o1 has_least_rank_for o,w1 means o1 has_least_args_for (o,w1) & o1 has_least_sort_for (o,w1);

    end

    definition

      let S, o;

      :: OSALG_1:def12

      attr o is regular means

      : Def12: o is monotone & for w1 st w1 <= ( the_arity_of o) holds ex o1 st o1 has_least_args_for (o,w1);

    end

    definition

      let SM be monotone OrderSortedSign;

      :: OSALG_1:def13

      attr SM is regular means

      : Def13: for om be OperSymbol of SM holds om is regular;

    end

    reserve SM for monotone OrderSortedSign,

o,o1,o2 for OperSymbol of SM,

w1 for Element of (the carrier of SM * );

    theorem :: OSALG_1:11

    

     Th11: SM is regular iff for o, w1 st w1 <= ( the_arity_of o) holds ex o1 st o1 has_least_rank_for (o,w1)

    proof

      hereby

        assume

         A1: SM is regular;

        let o, w1;

        assume

         A2: w1 <= ( the_arity_of o);

        o is regular by A1;

        then

        consider o1 such that

         A3: o1 has_least_args_for (o,w1) by A2;

        take o1;

        o1 has_least_sort_for (o,w1)

        proof

          thus

           A4: o ~= o1 & w1 <= ( the_arity_of o1) by A3;

          let o2;

          assume that

           A5: o ~= o2 and

           A6: w1 <= ( the_arity_of o2);

          

           A7: o1 ~= o2 by A4, A5, Th2;

          ( the_arity_of o1) <= ( the_arity_of o2) by A3, A5, A6;

          hence thesis by A7, Def7;

        end;

        hence o1 has_least_rank_for (o,w1) by A3;

      end;

      assume

       A8: for o, w1 st w1 <= ( the_arity_of o) holds ex o1 st o1 has_least_rank_for (o,w1);

      let o;

      thus o is monotone;

      let w1;

      assume w1 <= ( the_arity_of o);

      then

      consider o1 such that

       A9: o1 has_least_rank_for (o,w1) by A8;

      take o1;

      thus thesis by A9;

    end;

    theorem :: OSALG_1:12

    

     Th12: for SM be monotone OrderSortedSign holds SM is op-discrete implies SM is regular

    proof

      let SM be monotone OrderSortedSign;

      assume

       A1: SM is op-discrete;

      let om be OperSymbol of SM;

      thus om is monotone;

      let wm1 be Element of (the carrier of SM * ) such that

       A2: wm1 <= ( the_arity_of om);

      om has_least_args_for (om,wm1) by A2, A1, Th3;

      hence thesis;

    end;

    registration

      cluster regular for monotone OrderSortedSign;

      existence

      proof

        set SM = the op-discrete OrderSortedSign;

        take SM;

        thus thesis by Th12;

      end;

    end

    registration

      cluster op-discrete -> regular for monotone OrderSortedSign;

      coherence by Th12;

    end

    registration

      let SR be regular monotone OrderSortedSign;

      cluster -> regular for OperSymbol of SR;

      coherence by Def13;

    end

    reserve SR for regular monotone OrderSortedSign,

o,o1,o3,o4 for OperSymbol of SR,

w1 for Element of (the carrier of SR * );

    theorem :: OSALG_1:13

    

     Th13: o3 has_least_args_for (o,w1) & o4 has_least_args_for (o,w1) implies o3 = o4

    proof

      assume that

       A1: o3 has_least_args_for (o,w1) and

       A2: o4 has_least_args_for (o,w1);

      

       A3: o ~= o3 by A1;

      

       A4: o ~= o4 by A2;

      then

       A5: o3 ~= o4 by A3, Th2;

      w1 <= ( the_arity_of o3) by A1;

      then

       A6: ( the_arity_of o4) <= ( the_arity_of o3) by A2, A3;

      then

       A7: ( the_result_sort_of o4) <= ( the_result_sort_of o3) by A5, Def7;

      w1 <= ( the_arity_of o4) by A2;

      then

       A8: ( the_arity_of o3) <= ( the_arity_of o4) by A1, A4;

      then

       A9: ( the_arity_of o3) = ( the_arity_of o4) by A6, Th6;

      ( the_result_sort_of o3) <= ( the_result_sort_of o4) by A5, A8, Def7;

      then ( the_result_sort_of o3) = ( the_result_sort_of o4) by A7, ORDERS_2: 2;

      hence thesis by A5, A9, Def3;

    end;

    definition

      let SR, o, w1;

      assume

       A1: w1 <= ( the_arity_of o);

      :: OSALG_1:def14

      func LBound (o,w1) -> OperSymbol of SR means

      : Def14: it has_least_args_for (o,w1);

      existence by A1, Def12;

      uniqueness by Th13;

    end

    theorem :: OSALG_1:14

    

     Th14: for w1 st w1 <= ( the_arity_of o) holds ( LBound (o,w1)) has_least_rank_for (o,w1)

    proof

      let w1;

      assume

       A1: w1 <= ( the_arity_of o);

      then

      consider o1 such that

       A2: o1 has_least_rank_for (o,w1) by Th11;

      thus thesis by A1, A2, Def14;

    end;

    reserve R for non empty Poset;

    reserve z for non empty set;

    definition

      let R, z;

      :: OSALG_1:def15

      func ConstOSSet (R,z) -> ManySortedSet of the carrier of R equals (the carrier of R --> z);

      correctness

      proof

        the carrier of R = ( dom (the carrier of R --> z)) by FUNCT_2:def 1;

        hence thesis by PARTFUN1:def 2;

      end;

    end

    theorem :: OSALG_1:15

    

     Th15: ( ConstOSSet (R,z)) is non-empty & for s1,s2 be Element of R st s1 <= s2 holds (( ConstOSSet (R,z)) . s1) c= (( ConstOSSet (R,z)) . s2)

    proof

      set x = ( ConstOSSet (R,z));

      set D = (the carrier of R --> z);

      for s be object st s in the carrier of R holds (x . s) is non empty by FUNCOP_1: 7;

      hence x is non-empty by PBOOLE:def 13;

      let s1,s2 be Element of R;

      (D . s1) = z by FUNCOP_1: 7

      .= (D . s2) by FUNCOP_1: 7;

      hence thesis;

    end;

    definition

      let R;

      let M be ManySortedSet of R;

      :: OSALG_1:def16

      attr M is order-sorted means

      : Def16: for s1,s2 be Element of R st s1 <= s2 holds (M . s1) c= (M . s2);

    end

    theorem :: OSALG_1:16

    

     Th16: ( ConstOSSet (R,z)) is order-sorted by Th15;

    registration

      let R;

      cluster order-sorted for ManySortedSet of R;

      existence

      proof

        set z = the non empty set;

        take ( ConstOSSet (R,z));

        thus thesis by Th16;

      end;

    end

    registration

      let R, z;

      cluster ( ConstOSSet (R,z)) -> order-sorted;

      coherence by Th16;

    end

    definition

      let R be non empty Poset;

      mode OrderSortedSet of R is order-sorted ManySortedSet of R;

    end

    registration

      let R be non empty Poset;

      cluster non-empty for OrderSortedSet of R;

      existence

      proof

        take ( ConstOSSet (R, { {} }));

        thus thesis by Th15;

      end;

    end

    reserve s1,s2 for SortSymbol of S,

o,o1,o2,o3 for OperSymbol of S,

w1,w2 for Element of (the carrier of S * );

    definition

      let S;

      let M be MSAlgebra over S;

      :: OSALG_1:def17

      attr M is order-sorted means

      : Def17: for s1, s2 st s1 <= s2 holds (the Sorts of M . s1) c= (the Sorts of M . s2);

    end

    theorem :: OSALG_1:17

    

     Th17: for M be MSAlgebra over S holds M is order-sorted iff the Sorts of M is OrderSortedSet of S by Def16;

    reserve CH for ManySortedFunction of ((( ConstOSSet (S,z)) # ) * the Arity of S), (( ConstOSSet (S,z)) * the ResultSort of S);

    definition

      let S, z, CH;

      :: OSALG_1:def18

      func ConstOSA (S,z,CH) -> strict non-empty MSAlgebra over S means

      : Def18: the Sorts of it = ( ConstOSSet (S,z)) & the Charact of it = CH;

      existence

      proof

        for i be object st i in the carrier of S holds (( ConstOSSet (S,z)) . i) is non empty by FUNCOP_1: 7;

        then ( ConstOSSet (S,z)) is non-empty by PBOOLE:def 13;

        then

        reconsider T = MSAlgebra (# ( ConstOSSet (S,z)), CH #) as strict non-empty MSAlgebra over S by MSUALG_1:def 3;

        take T;

        thus thesis;

      end;

      uniqueness ;

    end

    theorem :: OSALG_1:18

    

     Th18: ( ConstOSA (S,z,CH)) is order-sorted

    proof

      the Sorts of ( ConstOSA (S,z,CH)) = ( ConstOSSet (S,z)) by Def18;

      hence thesis by Th17;

    end;

    registration

      let S;

      cluster strict non-empty order-sorted for MSAlgebra over S;

      existence

      proof

        set z = the non empty set, CH = the ManySortedFunction of ((( ConstOSSet (S,z)) # ) * the Arity of S), (( ConstOSSet (S,z)) * the ResultSort of S);

        take ( ConstOSA (S,z,CH));

        thus thesis by Th18;

      end;

    end

    registration

      let S, z, CH;

      cluster ( ConstOSA (S,z,CH)) -> order-sorted;

      coherence by Th18;

    end

    definition

      let S;

      mode OSAlgebra of S is order-sorted MSAlgebra over S;

    end

    theorem :: OSALG_1:19

    

     Th19: for S be discrete OrderSortedSign, M be MSAlgebra over S holds M is order-sorted by ORDERS_3: 1;

    registration

      let S be discrete OrderSortedSign;

      cluster -> order-sorted for MSAlgebra over S;

      coherence by Th19;

    end

    reserve A for OSAlgebra of S;

    theorem :: OSALG_1:20

    

     Th20: w1 <= w2 implies ((the Sorts of A # ) . w1) c= ((the Sorts of A # ) . w2)

    proof

      set iw1 = (the Sorts of A * w1), iw2 = (the Sorts of A * w2);

      assume

       A1: w1 <= w2;

      then

       A2: ( len w1) = ( len w2);

      let x be object;

      assume x in ((the Sorts of A # ) . w1);

      then x in ( product iw1) by FINSEQ_2:def 5;

      then

      consider g be Function such that

       A3: x = g and

       A4: ( dom g) = ( dom iw1) and

       A5: for y be object st y in ( dom iw1) holds (g . y) in (iw1 . y) by CARD_3:def 5;

      

       A6: ( dom iw1) = ( dom w1) by Lm1

      .= ( dom w2) by A2, FINSEQ_3: 29

      .= ( dom iw2) by Lm1;

      for y be object st y in ( dom iw2) holds (g . y) in (iw2 . y)

      proof

        let y be object such that

         A7: y in ( dom iw2);

        

         A8: y in ( dom w1) by A6, A7, Lm1;

        then

         A9: (iw1 . y) = (the Sorts of A . (w1 . y)) by FUNCT_1: 13;

        

         A10: y in ( dom w2) by A7, Lm1;

        then

         A11: (iw2 . y) = (the Sorts of A . (w2 . y)) by FUNCT_1: 13;

        reconsider s1 = (w1 . y), s2 = (w2 . y) as SortSymbol of S by A8, A10, PARTFUN1: 4;

        s1 <= s2 by A1, A8;

        then

         A12: (the Sorts of A . (w1 . y)) c= (the Sorts of A . (w2 . y)) by Def17;

        (g . y) in (iw1 . y) by A5, A6, A7;

        hence thesis by A9, A11, A12;

      end;

      then g in ( product iw2) by A4, A6, CARD_3:def 5;

      hence thesis by A3, FINSEQ_2:def 5;

    end;

    reserve M for MSAlgebra over S0;

    definition

      let S0, M;

      :: OSALG_1:def19

      func OSAlg M -> strict OSAlgebra of ( OSSign S0) means the Sorts of it = the Sorts of M & the Charact of it = the Charact of M;

      uniqueness ;

      existence

      proof

        set S1 = ( OSSign S0), s0 = the Sorts of M, c0 = the Charact of M;

        

         A1: the carrier of S0 = the carrier of S1 by Def5;

        then

        reconsider s1 = s0 as ManySortedSet of S1;

        the Arity of S0 = the Arity of S1 & the ResultSort of S1 = the ResultSort of S0 by Def5;

        then

        reconsider c1 = c0 as ManySortedFunction of ((s1 # ) * the Arity of S1), (s1 * the ResultSort of S1) by A1, Def5;

         MSAlgebra (# s1, c1 #) is order-sorted;

        hence thesis;

      end;

    end

    reserve A for OSAlgebra of S;

    theorem :: OSALG_1:21

    

     Th21: for w1,w2,w3 be Element of (the carrier of S * ) holds w1 <= w2 & w2 <= w3 implies w1 <= w3

    proof

      let w1,w2,w3 be Element of (the carrier of S * );

      assume that

       A1: w1 <= w2 and

       A2: w2 <= w3;

      

       A3: ( len w1) = ( len w2) by A1;

      then

       A4: ( dom w1) = ( dom w2) by FINSEQ_3: 29;

      

       A5: ( len w2) = ( len w3) by A2;

      then

       A6: ( dom w2) = ( dom w3) by FINSEQ_3: 29;

      for i be set st i in ( dom w1) holds for s1, s2 st s1 = (w1 . i) & s2 = (w3 . i) holds s1 <= s2

      proof

        let i be set such that

         A7: i in ( dom w1);

        reconsider s3 = (w1 . i), s4 = (w2 . i), s5 = (w3 . i) as SortSymbol of S by A4, A6, A7, PARTFUN1: 4;

        

         A8: s3 <= s4 & s4 <= s5 by A1, A2, A4, A7;

        let s1, s2;

        assume s1 = (w1 . i) & s2 = (w3 . i);

        hence thesis by A8, ORDERS_2: 3;

      end;

      hence thesis by A3, A5;

    end;

    definition

      let S, o1, o2;

      :: OSALG_1:def20

      pred o1 <= o2 means o1 ~= o2 & ( the_arity_of o1) <= ( the_arity_of o2) & ( the_result_sort_of o1) <= ( the_result_sort_of o2);

      reflexivity ;

    end

    theorem :: OSALG_1:22

    o1 <= o2 & o2 <= o1 implies o1 = o2

    proof

      assume that

       A1: o1 <= o2 and

       A2: o2 <= o1;

      ( the_result_sort_of o1) <= ( the_result_sort_of o2) & ( the_result_sort_of o2) <= ( the_result_sort_of o1) by A1, A2;

      then

       A3: ( the_result_sort_of o1) = ( the_result_sort_of o2) by ORDERS_2: 2;

      ( the_arity_of o1) <= ( the_arity_of o2) & ( the_arity_of o2) <= ( the_arity_of o1) by A1, A2;

      then

       A4: ( the_arity_of o1) = ( the_arity_of o2) by Th6;

      o1 ~= o2 by A1;

      hence thesis by A4, A3, Def3;

    end;

    theorem :: OSALG_1:23

    o1 <= o2 & o2 <= o3 implies o1 <= o3 by Th2, Th21, ORDERS_2: 3;

    theorem :: OSALG_1:24

    

     Th24: ( the_result_sort_of o1) <= ( the_result_sort_of o2) implies ( Result (o1,A)) c= ( Result (o2,A))

    proof

      reconsider M = the Sorts of A as OrderSortedSet of S by Th17;

      

       A1: ( Result (o2,A)) = ((the Sorts of A * the ResultSort of S) . o2) by MSUALG_1:def 5

      .= (the Sorts of A . (the ResultSort of S . o2)) by FUNCT_2: 15

      .= (the Sorts of A . ( the_result_sort_of o2)) by MSUALG_1:def 2;

      assume ( the_result_sort_of o1) <= ( the_result_sort_of o2);

      then

       A2: (M . ( the_result_sort_of o1)) c= (M . ( the_result_sort_of o2)) by Def16;

      ( Result (o1,A)) = ((the Sorts of A * the ResultSort of S) . o1) by MSUALG_1:def 5

      .= (the Sorts of A . (the ResultSort of S . o1)) by FUNCT_2: 15

      .= (the Sorts of A . ( the_result_sort_of o1)) by MSUALG_1:def 2;

      hence thesis by A2, A1;

    end;

    theorem :: OSALG_1:25

    

     Th25: ( the_arity_of o1) <= ( the_arity_of o2) implies ( Args (o1,A)) c= ( Args (o2,A))

    proof

      reconsider M = the Sorts of A as OrderSortedSet of S by Th17;

      

       A1: ((M # ) . ( the_arity_of o1)) = ((M # ) . (the Arity of S . o1)) by MSUALG_1:def 1

      .= (((M # ) * the Arity of S) . o1) by FUNCT_2: 15

      .= ( Args (o1,A)) by MSUALG_1:def 4;

      

       A2: ((M # ) . ( the_arity_of o2)) = ((M # ) . (the Arity of S . o2)) by MSUALG_1:def 1

      .= (((M # ) * the Arity of S) . o2) by FUNCT_2: 15

      .= ( Args (o2,A)) by MSUALG_1:def 4;

      assume ( the_arity_of o1) <= ( the_arity_of o2);

      hence thesis by A1, A2, Th20;

    end;

    theorem :: OSALG_1:26

    o1 <= o2 implies ( Args (o1,A)) c= ( Args (o2,A)) & ( Result (o1,A)) c= ( Result (o2,A)) by Th24, Th25;

    definition

      let S, A;

      :: OSALG_1:def21

      attr A is monotone means for o1, o2 st o1 <= o2 holds (( Den (o2,A)) | ( Args (o1,A))) = ( Den (o1,A));

    end

    theorem :: OSALG_1:27

    

     Th27: for A be non-empty OSAlgebra of S holds A is monotone iff for o1, o2 st o1 <= o2 holds ( Den (o1,A)) c= ( Den (o2,A))

    proof

      let A be non-empty OSAlgebra of S;

      hereby

        assume

         A1: A is monotone;

        let o1, o2;

        assume o1 <= o2;

        then (( Den (o2,A)) | ( Args (o1,A))) = ( Den (o1,A)) by A1;

        hence ( Den (o1,A)) c= ( Den (o2,A)) by RELAT_1: 59;

      end;

      assume

       A2: for o1, o2 st o1 <= o2 holds ( Den (o1,A)) c= ( Den (o2,A));

      let o1, o2 such that

       A3: o1 <= o2;

      ( dom ( Den (o1,A))) = ( Args (o1,A)) by FUNCT_2:def 1;

      

      hence (( Den (o2,A)) | ( Args (o1,A))) = (( Den (o1,A)) | ( Args (o1,A))) by A2, A3, GRFUNC_1: 27

      .= ( Den (o1,A));

    end;

    theorem :: OSALG_1:28

    (S is discrete or S is op-discrete) implies A is monotone

    proof

      assume

       A1: S is discrete or S is op-discrete;

      let o1, o2;

      assume that

       A2: o1 ~= o2 and

       A3: ( the_arity_of o1) <= ( the_arity_of o2) & ( the_result_sort_of o1) <= ( the_result_sort_of o2);

      o1 = o2

      proof

        per cases by A1;

          suppose S is discrete;

          hence thesis by A2, A3, Th8;

        end;

          suppose S is op-discrete;

          hence thesis by A2, Th3;

        end;

      end;

      hence thesis;

    end;

    definition

      let S, z;

      let z1 be Element of z;

      :: OSALG_1:def22

      func TrivialOSA (S,z,z1) -> strict OSAlgebra of S means

      : Def22: the Sorts of it = ( ConstOSSet (S,z)) & for o holds ( Den (o,it )) = (( Args (o,it )) --> z1);

      existence

      proof

        set c = ( ConstOSSet (S,z));

        deffunc ch1( Element of the carrier' of S) = ((((c # ) * the Arity of S) . $1) --> z1 qua set);

        consider ch2 be Function such that

         A1: ( dom ch2) = the carrier' of S & for x be Element of the carrier' of S holds (ch2 . x) = ch1(x) from FUNCT_1:sch 4;

        reconsider ch4 = ch2 as ManySortedSet of the carrier' of S by A1, PARTFUN1:def 2, RELAT_1:def 18;

        for i be object st i in the carrier' of S holds (ch4 . i) is Function of (((( ConstOSSet (S,z)) # ) * the Arity of S) . i), ((( ConstOSSet (S,z)) * the ResultSort of S) . i)

        proof

          let i be object;

          assume i in the carrier' of S;

          then

          reconsider o = i as OperSymbol of S;

          (the ResultSort of S . o) in the carrier of S;

          then

           A2: o in (the ResultSort of S " the carrier of S) by FUNCT_2: 38;

          ((( ConstOSSet (S,z)) * the ResultSort of S) . o) = (((the ResultSort of S " the carrier of S) --> z) . o) by FUNCOP_1: 19

          .= z by A2, FUNCOP_1: 7;

          then

           A3: {z1} c= ((( ConstOSSet (S,z)) * the ResultSort of S) . i) by ZFMISC_1: 31;

          (ch4 . i) = ch1(o) by A1;

          hence thesis by A3, FUNCT_2: 7;

        end;

        then

        reconsider ch3 = ch4 as ManySortedFunction of ((( ConstOSSet (S,z)) # ) * the Arity of S), (( ConstOSSet (S,z)) * the ResultSort of S) by PBOOLE:def 15;

        take T = ( ConstOSA (S,z,ch3));

        thus

         A4: the Sorts of T = ( ConstOSSet (S,z)) by Def18;

        let o;

        ( Den (o,T)) = (the Charact of T . o) by MSUALG_1:def 6

        .= (ch3 . o) by Def18

        .= ((((c # ) * the Arity of S) . o) --> z1) by A1

        .= (( Args (o,T)) --> z1) by A4, MSUALG_1:def 4;

        hence thesis;

      end;

      uniqueness

      proof

        let T1,T2 be strict OSAlgebra of S;

        assume that

         A5: the Sorts of T1 = ( ConstOSSet (S,z)) and

         A6: for o holds ( Den (o,T1)) = (( Args (o,T1)) --> z1);

        assume that

         A7: the Sorts of T2 = ( ConstOSSet (S,z)) and

         A8: for o holds ( Den (o,T2)) = (( Args (o,T2)) --> z1);

        now

          let o1 be object;

          assume o1 in the carrier' of S;

          then

          reconsider o = o1 as OperSymbol of S;

          

          thus (the Charact of T1 . o1) = ( Den (o,T1)) by MSUALG_1:def 6

          .= (( Args (o,T1)) --> z1) by A6

          .= ((((( ConstOSSet (S,z)) # ) * the Arity of S) . o) --> z1) by A5, MSUALG_1:def 4

          .= (( Args (o,T2)) --> z1) by A7, MSUALG_1:def 4

          .= ( Den (o,T2)) by A8

          .= (the Charact of T2 . o1) by MSUALG_1:def 6;

        end;

        hence thesis by A5, A7, PBOOLE: 3;

      end;

    end

    theorem :: OSALG_1:29

    

     Th29: for z1 be Element of z holds ( TrivialOSA (S,z,z1)) is non-empty & ( TrivialOSA (S,z,z1)) is monotone

    proof

      let z1 be Element of z;

      set A = ( TrivialOSA (S,z,z1));

      the Sorts of A = ( ConstOSSet (S,z)) by Def22;

      then

       A1: the Sorts of A is non-empty by Th15;

      hence A is non-empty by MSUALG_1:def 3;

      reconsider A1 = A as non-empty OSAlgebra of S by A1, MSUALG_1:def 3;

      for o1, o2 st o1 <= o2 holds ( Den (o1,A1)) c= ( Den (o2,A1))

      proof

        let o1, o2;

        

         A2: ( Args (o1,A)) = (((the Sorts of A # ) * the Arity of S) . o1) by MSUALG_1:def 4

        .= ((the Sorts of A # ) . (the Arity of S . o1)) by FUNCT_2: 15

        .= ((the Sorts of A # ) . ( the_arity_of o1)) by MSUALG_1:def 1;

        

         A3: ( Args (o2,A)) = (((the Sorts of A # ) * the Arity of S) . o2) by MSUALG_1:def 4

        .= ((the Sorts of A # ) . (the Arity of S . o2)) by FUNCT_2: 15

        .= ((the Sorts of A # ) . ( the_arity_of o2)) by MSUALG_1:def 1;

        assume o1 <= o2;

        then

         A4: ( the_arity_of o1) <= ( the_arity_of o2);

        ( Den (o1,A)) = (( Args (o1,A)) --> z1) & ( Den (o2,A)) = (( Args (o2,A)) --> z1) by Def22;

        hence thesis by A4, A2, A3, Th20, FUNCT_4: 4;

      end;

      hence thesis by Th27;

    end;

    registration

      let S;

      cluster monotone strict non-empty for OSAlgebra of S;

      existence

      proof

        set z = the non empty set;

        set z1 = the Element of z;

        take ( TrivialOSA (S,z,z1));

        thus thesis by Th29;

      end;

    end

    registration

      let S, z;

      let z1 be Element of z;

      cluster ( TrivialOSA (S,z,z1)) -> monotone non-empty;

      coherence by Th29;

    end

    reserve op1,op2 for OperSymbol of S;

    definition

      let S;

      :: OSALG_1:def23

      func OperNames S -> non empty Subset-Family of the carrier' of S equals ( Class the Overloading of S);

      coherence ;

    end

    registration

      let S;

      cluster -> non empty for Element of ( OperNames S);

      coherence

      proof

        let X be Element of ( OperNames S);

        ex x be object st x in the carrier' of S & X = ( Class (the Overloading of S,x)) by EQREL_1:def 3;

        hence thesis by EQREL_1: 20;

      end;

    end

    definition

      let S;

      mode OperName of S is Element of ( OperNames S);

    end

    definition

      let S, op1;

      :: OSALG_1:def24

      func Name op1 -> OperName of S equals ( Class (the Overloading of S,op1));

      coherence by EQREL_1:def 3;

    end

    theorem :: OSALG_1:30

    

     Th30: op1 ~= op2 iff op2 in ( Class (the Overloading of S,op1))

    proof

      op1 ~= op2 iff [op2, op1] in the Overloading of S by Def2;

      hence thesis by EQREL_1: 19;

    end;

    theorem :: OSALG_1:31

    

     Th31: op1 ~= op2 iff ( Name op1) = ( Name op2)

    proof

      op2 in ( Class (the Overloading of S,op1)) iff ( Class (the Overloading of S,op1)) = ( Class (the Overloading of S,op2)) by EQREL_1: 23;

      hence thesis by Th30;

    end;

    theorem :: OSALG_1:32

    for X be set holds X is OperName of S iff ex op1 st X = ( Name op1)

    proof

      let X be set;

      hereby

        assume X is OperName of S;

        then

        consider x be object such that

         A1: x in the carrier' of S and

         A2: X = ( Class (the Overloading of S,x)) by EQREL_1:def 3;

        reconsider x1 = x as OperSymbol of S by A1;

        take x1;

        thus X = ( Name x1) by A2;

      end;

      given op1 such that

       A3: X = ( Name op1);

      thus thesis by A3;

    end;

    definition

      let S;

      let o be OperName of S;

      :: original: Element

      redefine

      mode Element of o -> OperSymbol of S ;

      coherence

      proof

        let x be Element of o;

        thus thesis;

      end;

    end

    theorem :: OSALG_1:33

    

     Th33: for on be OperName of S, op be OperSymbol of S holds op is Element of on iff ( Name op) = on

    proof

      let on be OperName of S, op1 be OperSymbol of S;

      hereby

        assume op1 is Element of on;

        then

        reconsider op = op1 as Element of on;

        (ex op2 be object st op2 in the carrier' of S & on = ( Class (the Overloading of S,op2))) & ( Name op) = ( Class (the Overloading of S,op)) by EQREL_1:def 3;

        hence ( Name op1) = on by EQREL_1: 23;

      end;

      assume ( Name op1) = on;

      hence thesis by EQREL_1: 20;

    end;

    theorem :: OSALG_1:34

    

     Th34: for SR be regular monotone OrderSortedSign, op1,op2 be OperSymbol of SR, w be Element of (the carrier of SR * ) st op1 ~= op2 & w <= ( the_arity_of op1) & w <= ( the_arity_of op2) holds ( LBound (op1,w)) = ( LBound (op2,w))

    proof

      let SR be regular monotone OrderSortedSign, op1,op2 be OperSymbol of SR, w be Element of (the carrier of SR * ) such that

       A1: op1 ~= op2 and

       A2: w <= ( the_arity_of op1) and

       A3: w <= ( the_arity_of op2);

      set Lo1 = ( LBound (op1,w)), Lo2 = ( LBound (op2,w));

      

       A4: ( LBound (op1,w)) has_least_args_for (op1,w) by A2, Def14;

      then

       A5: op1 ~= Lo1;

      

       A6: ( LBound (op2,w)) has_least_args_for (op2,w) by A3, Def14;

      then

       A7: for o2 be OperSymbol of SR st op2 ~= o2 & w <= ( the_arity_of o2) holds ( the_arity_of Lo2) <= ( the_arity_of o2);

      op2 ~= Lo2 by A6;

      then

       A8: op1 ~= Lo2 by A1, Th2;

      then

       A9: Lo1 ~= Lo2 by A5, Th2;

      w <= ( the_arity_of Lo1) by A4;

      then

       A10: ( the_arity_of Lo2) <= ( the_arity_of Lo1) by A1, A5, A7, Th2;

      then

       A11: ( the_result_sort_of Lo2) <= ( the_result_sort_of Lo1) by A9, Def7;

      w <= ( the_arity_of Lo2) by A6;

      then

       A12: ( the_arity_of Lo1) <= ( the_arity_of Lo2) by A4, A8;

      then

       A13: ( the_arity_of Lo1) = ( the_arity_of Lo2) by A10, Th6;

      ( the_result_sort_of Lo1) <= ( the_result_sort_of Lo2) by A9, A12, Def7;

      then ( the_result_sort_of Lo1) = ( the_result_sort_of Lo2) by A11, ORDERS_2: 2;

      hence thesis by A9, A13, Def3;

    end;

    definition

      let SR be regular monotone OrderSortedSign, on be OperName of SR, w be Element of (the carrier of SR * );

      assume

       A1: ex op be Element of on st w <= ( the_arity_of op);

      :: OSALG_1:def25

      func LBound (on,w) -> Element of on means for op be Element of on st w <= ( the_arity_of op) holds it = ( LBound (op,w));

      existence

      proof

        consider op be Element of on such that

         A2: w <= ( the_arity_of op) by A1;

        set Lo = ( LBound (op,w));

        ( LBound (op,w)) has_least_args_for (op,w) by A2, Def14;

        then op ~= Lo;

        then

         A3: ( Name op) = ( Name Lo) by Th31;

        then

         A4: ( Name Lo) = on by Th33;

        then

        reconsider Lo as Element of on by Th33;

        take Lo;

        let op1 be Element of on such that

         A5: w <= ( the_arity_of op1);

        ( Name op1) = on by Th33;

        then op1 ~= op by A3, A4, Th31;

        hence thesis by A2, A5, Th34;

      end;

      uniqueness

      proof

        let op1,op2 be Element of on such that

         A6: for op3 be Element of on st w <= ( the_arity_of op3) holds op1 = ( LBound (op3,w)) and

         A7: for op3 be Element of on st w <= ( the_arity_of op3) holds op2 = ( LBound (op3,w));

        consider op be Element of on such that

         A8: w <= ( the_arity_of op) by A1;

        op1 = ( LBound (op,w)) by A8, A6;

        hence thesis by A8, A7;

      end;

    end

    theorem :: OSALG_1:35

    for S be regular monotone OrderSortedSign, o be OperSymbol of S, w1 be Element of (the carrier of S * ) st w1 <= ( the_arity_of o) holds ( LBound (o,w1)) <= o

    proof

      let S be regular monotone OrderSortedSign, o be OperSymbol of S, w1 be Element of (the carrier of S * ) such that

       A1: w1 <= ( the_arity_of o);

      set lo = ( LBound (o,w1));

      

       A2: lo has_least_rank_for (o,w1) by A1, Th14;

      then lo has_least_sort_for (o,w1);

      then

       A3: ( the_result_sort_of lo) <= ( the_result_sort_of o) by A1;

      

       A4: lo has_least_args_for (o,w1) by A2;

      then

       A5: o ~= lo;

      ( the_arity_of lo) <= ( the_arity_of o) by A1, A4;

      hence thesis by A5, A3;

    end;